Simplifying integer formulas in Z3

Question

After applying quantifier elimination in Z3 to a linear arithmetic formula h, I'm getting a 30-line or so formula. It turns out this formula is equivalent to h2=And(n>2, i>=0, i<=n-2), which I would much prefer as an output.

I tried ctx-solver-simplify; I'm getting: And(Not(n <= 2), Or(Not(i >= 1), Not(n + -1*i <= 1)), i >= 0)

Now, Not(n<=2) can be more succinctly expressed as n>=3, Not(n + -1*i <= 1) as n-i>=2, and in this formula i >= 1 is not needed.

Repeat(Then('nnf','ctx-solver-simplify')) does a little better (by getting rid of i>=1).

Is there a better simplification tactic?

Similarly, is there a tactic that would transform Or(x==0, x==1, x==2, x==3) into And(x>=0,x<=3)?

Good question, though I don't think a built-in method will do it. The ctx-solver-simplify method is one of the more aggressive ones and it does not know your intent is to get a conjunction. Maybe one idea is to simplify formulas modulo a set of templates. You could propose literals extracted from your template space (that you extract from the formula itself) and then extract a conjunction. — Nikolaj Bjorner
Unfortunately, the expected formula is not necessarily a conjunction. In that particular example, I conjectured that the result should be equivalent to that formula h2 (h comes from a program analysis problem and I had some intuition about what the final result should be like), which I checked with Z3 (h⇒h2 and h2⇒h), but in general the formula may be more complex. Your idea is interesting, I could, say, conjecture that the formula consists only in a few disjuncts... — David Monniaux

David Monniaux David Monniaux · Accepted Answer · 2014-03-03T19:29:05

My current best solution is to use Repeat(Then(OrElse('split-clause', 'nnf'), 'propagate-ineqs', 'ctx-solver-simplify')), with the latest unstable version of Z3 (where the bug in ctx-solver-simplify has been corrected).

Simplifying integer formulas in Z3

1 Answers