Search code examples
unionz3smtsimplification

How to simplify the union of two expressions: Z3 solver

The result produced by the SMT solver is:

(or (and (>= c1 2) (<= c1 4) (= (+ c0 c1 c2) 5) (= (+ c0 c1) 4))
    (and (>= c1 1) (<= c1 3) (= (+ c0 c1 c2) 5) (= (+ c0 c1) 4)))

But I am expecting something like:

(and (>= c1 1) (<= c1 4) (= (+ c0 c1 c2) 5) (= (+ c0 c1) 4)

can someone guide me to achieve this with Z3 solver?

Link : http://rise4fun.com/Z3/1Xz3

Solution

  • Z3 does not support this kind of simplification. It does not support simplification into a "normal form". Recall that the main interface to Z3 is to check whether a formula is satisfiable or unsatisfiable. You can ask many queries to the SMT solver to extract a conjunction which is equivalent to a formula in case you are able to identify which literals should be tested for membership in the conjunction. This is not always possible to do in a syntactic way as your example suggests.