CODEWITHSUNDEEP
z3smt
user1779685
user1779685

Reputation: 383

Does z3's SAT solver obtain a complete assignment before doing a theory consistency check?

Does z3's SAT solver(s) obtain a complete assignment to the propositional(ized) part of an SMT problem before doing a theory consistency check? In particular, I am curious to know what is done by default for each of the following background theories/combination (if this is theory-dependent): Linear Real Arithmetic (LRA), Linear Integer Real Arithmetic (LIRA), Non-Linear Integer Real Arithmetic (NIRA)? Also, where in the actual code (codeplex stable z3 v4.3.1) is a propositional literal (heuristically) decided by the SAT solver?

Upvotes: 1

Views: 174

Answers (1)

Leonardo de Moura
Leonardo de Moura

Reputation: 21475

No, Z3 does not obtain a complete assignment before doing theory consistency checks. However, it delays "expensive" checks. "Expensive" checks are performed in a step called final_check that is performed only when a (complete) proprositional assignment is produced. Here the word "expensive" is relative. Linear real arithmetic consistency checks can be quite expensive due to big number arithmetic computations, but they are considered "cheap" in Z3.

Linear real arithmetic checks are done eagerly. Nonlinear and linear integer arithmetic checks are done at the final_check step.

Note that Z3 contains more than one solver. The behavior above is for the one implemented in the directory smt. The nonlinear real arithmetic solver (nlsat directory) works in a completely different way, and it does not use the final_check approach described above.

Upvotes: 1

Related Questions