toebs - 8 months ago 74

C++ Question

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`

.