使用z3解决约束系统后,我得到了一个模型,其中某些变量设置为None(我正在使用Pyz3)。这是否意味着这些变量已被消除?
谢谢!
未分配的变量应解释为“无关”。也就是说,任何赋值都将满足输入公式。这是一个小示例(也在此处提供)。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)
本文收集自互联网,转载请注明来源。
如有侵权,请联系[email protected] 删除。
我来说两句