Simplfying Expression : Z3 SMT Solver

Question

Executing the following query with the Z3 solver:

    (declare-const c0 Int)
    (declare-const c1 Int)
    (declare-const c2 Int)

    (assert (exists ((c0_s Int) (c1_s Int) (c2_s Int))
      (and 
        (= (+ c0 c1 c2) 5) (>= c0 0) (>= c1 1) (>= c2 1)
        (= c0_s c0) (= c1_s (- c1 1)) (= c2_s (+ c2 1))
        (= c2_s 3) (= (+ c0_s c1_s) 2)    
      ))
    )

    (apply (then qe ctx-solver-simplify propagate-ineqs))

produces the following output:

    (goals
     (goal
       (>= c0 0)
       (<= c0 2)
       (>= c1 1)
       (<= c1 3)
       (<= (+ (* (- 1) c0) (* (- 1) c1)) (- 3))
       (<= (+ c1 c0) 3)
       (= c2 2)
       :precision precise :depth 3)
    )

where I was expecting a result from the Z3 solver like this:

    (goals
     (goal
       (>= c0 0)
       (<= c0 2)
       (>= c1 1)
       (<= c1 3)
       (= (+ c1 c0) 3)
       (= c2 2)
       :precision precise :depth 3)
    )

Can anyone explain why Z3 is producing such a complex result instead of what I expected? Is there a way to get Z3 to simplify this output?

Apparently, Z3 does not know to simplify away the negations. Maybe you should post a feature request on GitHub. — usr
Thanks for your quick response, I will request for it as soon as possible if that is the case. However, I was wondering why in the first place it was generating negation when there is no need for it. — Nishanthan Kamaleson

mtrberzi mtrberzi · Accepted Answer · 2015-10-09T15:47:53

You may get a more detailed answer from a member of the core Z3 team, but from my experience working with Z3's integer solver at a low level, I can give a bit of intuition as to why this is happening.

Briefly, in order to solve integer equations, Z3's integer theory solver expects all of its constraints to appear in a very particular and restricted form. Expressions that do not follow this form must be rewritten before they are presented to the solver. Normally this happens internally by a theory rewriter, and any expression can be used in the input constraint set without issue.

The restrictions that apply here (that I am aware of), which help explain why you are seeing this strange-looking output, are as follows:

The integer solver can represent an equality constraint (= a b) as two separate inequality constraints (<= a b) and (>= a b). This is why you're seeing two separate constraints over your variables in the model instead of just one equality.
The integer solver rewrites subtractions, or negated terms, as multiplication by -1. This is why you are seeing these negations in your first constraint, and why the operator is addition instead of subtraction.
Arithmetic expressions are rewritten so that the second argument to a comparison operator is always a constant value.

In short, what you're seeing is likely an artifact of how the arithmetic theory solver represents constraints internally.

Since the output of your instance is a goal and not a model or proof, these expressions may not have been fully simplified yet, as I believe that intermediate goals are not always simplified (but I don't have experience with this part of the solver).

Simplfying Expression : Z3 SMT Solver

1 Answers