python - Z3中的变量消除

Question

在使用 z3 解决约束系统后，我得到了一个模型，其中一些变量设置为 None（我使用的是 Pyz3）。这是否意味着这些变量已被消除？

谢谢！

Answer 1

未分配的变量应被解释为“不关心”。也就是说，任何赋值都会满足输入公式。这是一个小例子（也可以在这里找到）。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)