CODEWITHSUNDEEP
z3
Georg
Georg

Reputation: 283

Rewriting of Formulas

In this paper (Section 3.2), it says that z3 applies rewriting/simplification of formulas before it does any other steps.

Suppose I have a formula in QF_UF, that consists of multiple assert statements. Is there any rewriting rule that would somehow "break the barrier" between different assert statements? Or, asking the other way round: Can I be sure that rewrite rules are only applied locally, "within" one assert statement?

For example, consider the following formula:

(set-logic QF_UF)
(set-option :auto-config false)
(set-option :PROOF_MODE  2)

(declare-fun a () Bool)
(assert a)
(assert (not a))

(check-sat)
(get-proof)

Can I be sure that the proof will contain a resolution step to prove False, or is it possible that False will be concluded by a rewrite/simplification step?

The reason I am asking is that for my application, every assert statement has a special semantics. Rewriting/Simplification across several assert statements would render the resulting proof of unsatisfiability unusable (or at least: very hard to use) for me.

Upvotes: 2

Views: 353

Answers (1)

Leonardo de Moura
Leonardo de Moura

Reputation: 21475

Z3 3.2 applies several preprocessing steps. Using (set-option :auto-config false) will disable most of them. You should also include the following two options:

(set-option :propagate-booleans false)

(set-option :propagate-values false)

Upvotes: 1

Related Questions