c++ - Z3 C++ API : set parameter for tactic

Question

我正在使用 SMT 求解器的 Z3 C++ API，我想更改“ctx-solver-simplify”的参数。我不知道如何将它们输入到策略中。我试过了:

z3::context c; 
c.set("arith_lhs",false);
c.set("eq2ineq",true);

和

z3::params params(c);
params.set("arith_lhs",true);
params.set("eq2ineq",true);

示例代码:

z3::expr x = c.int_const("x");
z3::expr cond1 = !(x==4);

z3::goal g(c);
g.add(cond1);

z3::tactic t(c, "ctx-solver-simplify");
z3::apply_result r = t(g);

结果是

(goal (not (= x 4)))

不是

(goal and  (< x 4) (> x 4)

同样适用于 arith_lhs。有什么帮助吗？ 谢谢!

Answer 1

变化: z3::tactic t(c, "ctx-solver-simplify"); 到 z3::tactic t = with(z3::tactic(c, "simplify"), params);

这将指示 Z3 对所选参数应用简化策略。在 SMT-LIB API 中，这是通过“using-params”组合器完成的。我从 Z3 源代码附带的 example.cpp 获得了上面的 C++ 等价物。

因此存在两个问题:(1) 您需要告诉 Z3 使用选定的参数应用给定的策略。 (2) ctx-solver-simplify 策略没有 eq2ineq 选项。不过，其他策略也可以，包括简化。