How to implement a custom simplify tactic in Z3?

Question

In my tool, I use conditions that compare constants to integer variables (for example y < 100). Often, there are multiple conditions for one variable and I want to simplify those cases. For example: y < 100 && y != 99 should become y < 99. The simplify tactic does not do this and none of the arguments for simplify sound like they can help.

In Code:

context c;
goal g(c);
expr x = c.int_const("x");
expr y = c.int_const("y");
solver s(c);
expr F = y < 100 && y != 99;
g.add(F);
tactic t = tactic(c, "simplify");
apply_result r = t(g);
for (unsigned i = 0; i < r.size(); i++) {
    std::cout << "subgoal " << i << "\n" << r[i] << "\n";
}

The output in the end returns: subgoal 0 (goal (not (<= 100 y)) (not (= y 99)))

and not subgoal 0(goal(not(<= 99 y)) or something similar as I want it to be.

Therefore I want to implement my own simplify tactic. Unfortunately I cannot find how to do this. I am aware, that the tactic needs to be implemented in C++, but how can I introduce my tactic to Z3?

Answer 1

The Z3 tactics are stored in the directory: src/tactic. The arithmetic related tactics are in the subdirectory arith. You should use an existing tactic as a "template" for implementing your tactic. A good example is https://z3.codeplex.com/SourceControl/latest#src/tactic/arith/normalize_bounds_tactic.cpp

To make the new tactic available in the API and SMT 2.0 front-end, we have to include a comment containing a ADD_TACTIC command. This command instructs the Z3 mk_make script to glue everything together. The arguments are: name of the tactic, description, and C++ code for creating the tactic.

/*
  ADD_TACTIC("normalize-bounds",
             "replace a variable x with lower bound k <= x with x' = x - k.",
             "mk_normalize_bounds_tactic(m, p)")
*/

BTW, you may also try to implement the new feature by extending an existing tactic such as: https://z3.codeplex.com/SourceControl/latest#src/tactic/arith/propagate_ineqs_tactic.cpp