使用 z3 求解约束系统后,我得到一个模型,其中一些变量设置为“无”(我使用的是 Pyz3)。这是否意味着这些变量已经被消除了?
谢谢!
最佳答案
未分配的变量应被解释为“不关心”。也就是说,任何赋值都会满足输入公式。
这是一个小例子(也可用 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)
关于python - Z3 中的变量消除,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/18926961/