CODEWITHSUNDEEP
z3
user1487718
user1487718

Reputation:

how to eliminate constraint in Z3

I have a constraint like (t>=0 or t>=1) and (t<=2 or t>=2),in fact the constraint can be simplified into "t>=0", how to use z3 to get the simplified result in CNF form by using z3?

(declare-const t Int)                                                                                  
(assert (and 
            (or
               (>= t 0)
               (>= t 1)
            )
            (or
                (>= t 2)
                 (<= t 2)
            )
            (>= t 0)
            (<= t 1)
        )
)                                                                                         
(apply (par-then (! simplify :elim-and true) tseitin-cnf))

However, the script doesn't work.

Upvotes: 3

Views: 1067

Answers (1)

Leonardo de Moura
Leonardo de Moura

Reputation: 21475

The simplify tactic only perform "local simplifications". That is, when simplifying an expression t, it will ignore the context of t. For example, it can simplify a + 1 - a into 1, but it will not simplify a != 0 or b = a + 1 into a != 0 or b = 1. Contextual simplification is expensive, the simplify tactic is meant to be efficient and simple. Other tactics may be used to achieve what you want.

The tactic propagate-ineqs will propagate inequalities. However, it will not process terms nested in the formula. The tactic split-clause can be used to break the formula in cases\goals. The tactic propagate-values will propagate the value of an assertion, example: a = 0 and b >= a is simplified to a = 0 and b >= 0.

The command (help-tactic) will display all available tactics.

Here is a strategy for simplifying your example into t >= 0 and t <= 1.

(apply (then simplify propagate-values split-clause propagate-ineqs))

Note that the combinator par-then is only useful for combining tactics that produce many sub-goals. (par-then t1 t2) applies t1 to the input goal, and applies t2 (in parallel) to every subgoal produced by t1. The split-clause tactic produces more than one subgoal. Then (for bigger examples) it may be more efficient to use:

(apply (then simplify propagate-values (par-then split-clause propagate-ineqs)))

Upvotes: 4

Related Questions