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);

この には、選択したパラメータでsimplify戦術を適用するためにZ3を指示します。 SMT-LIB APIでは、これは "using-params"コンビネータで実現されます。私はZ3ソースに同梱されているexample.cppから上記のC++の同等物を手に入れました。

したがって、2つの問題がありました。（1）選択されたパラメータで指定の戦術を適用するようにZ3に指示する必要があります。 （2）ctx-solver-simplify戦術にはeq2ineqオプションがありません。しかし、simplifyを含む他の戦術があります。