Search code examples
z3smt

How to use tactics in z3's SMT2 syntax?

I am interacting with z3 through its smt2 interface. Suppose, I write the following commands:

(declare-fun p () Int)
(declare-fun q () Int)
(declare-fun r () Int)

(assert (and (<= (+ (* 4 p) (* 3 q)) (- r 10)) (<= (+ (* 4 p) (* 3 q)) (- r 12))))

(apply simplify)

Now, I get a list of goals in the form

(goals
(goal …)
(goal …)
…
)

What do I do with it?

Another question, is there any documentation on this? Where should I look for it?

Solution

  • Tactics are a z3 invention; so you will not find any official documentation on how they should be used from an SMTLib perspective.

    In general, you don't just use apply. Instead, you use the method check-sat-using, that takes a tactic as an argument. In general, check-sat is equivalent to (check-sat-using smt), i.e., using the smt tactic.

    For your example, you can say:

    (check-sat-using (then simplify smt))

    this would reduce the problem to sat. The idea is that you can use these "tactics" to guide the solver to find a solution (or go faster).

    Tactics are usually intended to be used from higher-level interfaces, such as C/C++/Java etc., and unfortunately they aren't all that well documented. Read through http://www.cs.tau.ac.il/~msagiv/courses/asv/z3py/strategies-examples.htm, which is using the Python interface, but you can use the same ideas directly from smtLib as well.

    Tactics are also documented at https://theory.stanford.edu/~nikolaj/programmingz3.html#sec-tactics, though again it uses the Python interface not SMTLib.