Z3 C++ API: 为策略设置参数

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 对所选参数应用 simplify 策略。在 SMT-LIB API 中，这是通过 "using-params" 组合器完成的。我从 Z3 源代码附带的 example.cpp 获得了上述 C++ 等价物。

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

Z3 C++ API: 为策略设置参数

Z3 C++ API: set parameter for tactic

c++

parameters

z3