CODEWITHSUNDEEP
z3smt
DerHipler
DerHipler

Reputation: 1

Simplification with Z3 does not simplify as much as expected

In my application I want to simplify formulas using the Z3 solver. I know that the normal simplify tactic isn't powerful enough, so I'm using ctx-solver-simplify. However, even this tactic does not simplify as much as I was hoping. Particularly in cases concerning inequalities.

Say I have a formula b > 1 || b > 2, i.e.

(declare-const b Real)

(assert (or (> b 1.0) (> b 2.0)))

(apply ctx-solver-simplify)

This is obviously equivalent to just b > 1, but Z3 returns (or (not (<= b 1.0)) (> b 2.0)). However, if the clauses are swapped, i.e. (assert (or (> b 2.0) (> b 1.0))), Z3 returns (> b 1.0) as expected. I don't understand why the order is relevant here.

Moreover, if another clause is added, like

(declare-const a Bool)
(declare-const b Real)

(assert (or a (> b 2.0) (> b 1.0)))

(apply ctx-solver-simplify)

even the swapped order doesn't lead to the simplified result. In fact, Z3 doesn't modify the formula at all. But if the a is at the end instead, (assert (or (> b 2.0) (> b 1.0) a)), this actually works again and we get (or (> b 1.0) a).

Am I missing something here or am I using the wrong tactic? Why does the order of the clauses make a difference? I'm using version 4.12.2. Thanks in advance.

Upvotes: 0

Views: 236

Answers (1)

alias
alias

Reputation: 30525

The short answer is, unfortunately, z3 is not a good tool to use to simplify such terms. It has not been designed to perform such tasks, nor the general SMT-solving strategies allow for solvers to be used for performing arbitrary simplifications.

The search https://stackoverflow.com/search?q=%5Bz3%5D+simplify will show you countless questions/answers that discuss how z3 can be used as a simplifier. It is worthwhile going through them to get a wider view of the problem.

Long story short, what z3 considers "simple" and what we (as humans) consider "simple" won't necessarily match. While z3 does provide tactics, strategies, probes, etc. to allow some level of control, these mechanisms are fragile. (i.e., their behavior isn't guaranteed from version to version.) You might want to review https://microsoft.github.io/z3guide/programming/Example%20Programs/Formula%20Simplification/.

If you want algebraic simplifications, SymPy might also be a good choice. (https://docs.sympy.org/latest/tutorials/intro-tutorial/simplification.html). If you also need general SMT solving capabilities, one can use the two systems in tandem; but this is neither automated nor easy to use. (If your formulas only have a certain shape, it might be possible to automate some of this; but in general it is a hard problem to support arbitrary constructs.)

Upvotes: 2

Related Questions