simplification in Z3

Question

(declare-datatypes () ((SE BROKEN ON OFF)))
(declare-const s SE)
(declare-const a Int)
(simplify (or (= s ON) (= s OFF) (= s BROKEN)))
(simplify (and (> a 0) (> a 1)))

The result is:

(or (= s ON) (= s OFF) (= s BROKEN))
(and (not (<= a 0)) (not (<= a 1)))

But the expected result was:

1
> a 1

Is it possible to simplify such expressions (the combinations of such expressions) in Z3? Thank you!

Answer 1

The simplify command is just a bottom-up rewriter. It is fast, but will fail to simplify expressions such as the ones in your post. Z3 allows users to define their own simplification strategies using tactics. They are described in this article, and the Z3 tutorials (Python and SMT 2.0). The following posts also have additional information:

• t>=1 or t>=2 => t>=1
• Asymmetric behavior in ctx-solver-simplify
• what's the difference between "simplify" and "ctx-solver-simplify" in z3

The first query in your example can be simplified using the tactic ctx-solver-simplify (also available online here).

(declare-datatypes () ((SE BROKEN ON OFF)))
(declare-const s SE)
(declare-const a Int)
(assert (or (= s ON) (= s OFF) (= s BROKEN)))
(assert (and (> a 0) (> a 1)))
(apply ctx-solver-simplify)

The command apply applies the tactic ctx-solver-simplify over the set of assertions, and displays the resulting set of goals. Note that, this tactic is way more expensive than the command simplify.