Z3 C++ API:设置战术参数

Z3 C++ API: set parameter for tactic

本文关键字：参数 设置 C++ API Z3      更新时间：2023-10-16

我正在使用 SMT 求解器的 Z3 C++ API，我想更改"ctx-solver-simpleplify"的参数。我不知道如何将它们输入到战术中。我试过了： 

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。有什么帮助吗？谢谢！

更改： 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.

相关文章：