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