【发布时间】：2013-09-26 10:38:29
【问题描述】：
使用 z3 求解约束系统后，我得到一个模型，其中一些变量设置为 None（我使用的是 Pyz3）。是否意味着这些变量已经被消除了？
谢谢！
【问题讨论】：
标签： python variables z3 solver smt
【发布时间】：2013-09-26 10:38:29
【问题描述】：
未分配的变量应被解释为“不关心”。也就是说，任何赋值都会满足输入公式。
这是一个小例子（也可以使用here）。 Z3 产生的赋值只将x 赋值给1。 y 的值无关紧要。
(set-option :auto-config false)
(declare-const x Int)
(declare-const y Int)
(assert (or (= x 1) (= y 1)))
(check-sat)
(get-model)
【讨论】：