toebs toebs - 2 months ago 21
C++ Question

Z3 C++ API: set parameter for tactic

I'm using the Z3 C++ API of the SMT Solver and I'd like to change parameters of the "ctx-solver-simplify". I don't know how to input them to the tactic. I tried:

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


And

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


Example code:

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


The result is

(goal (not (= x 4)))


And not

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


Same applies for arith_lhs. Any help?
Thanks!

Answer

Change: z3::tactic t(c, "ctx-solver-simplify"); to z3::tactic t = with(z3::tactic(c, "simplify"), params);

This will instruct Z3 to apply the simplify tactic with the selected parameters. In the SMT-LIB API this is accomplished with the "using-params" combinator. I got the above C++ equivalent from example.cpp shipped with the Z3 source.

So there were two problems: (1) You need to tell Z3 to apply the given tactic with the selected parameters. (2) the ctx-solver-simplify tactic does not have an eq2ineq option. Other tactics do, though, including simplify.

Comments