toebs toebs - 4 months ago 42
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;


z3::params params(c);

Example code:

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

z3::goal g(c);

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?


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.