CODEWITHSUNDEEP
pythonvariablesz3solversmt
user2800940
user2800940

Reputation: 55

Variable elimination in Z3

After solving a constraint system using z3 I get a model where some variables are set to None (I'm using Pyz3). Does it mean that those variables have been eliminated?

Thanks!

Upvotes: 2

Views: 595

Answers (1)

Leonardo de Moura
Leonardo de Moura

Reputation: 21475

Unassigned variables should be interpreted as "don't cares". That is, any assignment would satisfy the input formula. Here is a small example (also available here). The assignment produced by Z3 only assigns x to 1. The value of y doesn't matter.

(set-option :auto-config false)
(declare-const x Int)
(declare-const y Int)
(assert (or (= x 1) (= y 1)))
(check-sat)
(get-model)

Upvotes: 2

Related Questions