Z3软约束

Question

我对在Z3中使用软约束的使用感到困惑。运行此程序时，我将获得以下输出。

from z3 import *
o = Solver()

expr = f"""
(declare-const v Real)
(declare-const v1 Bool)
(assert-soft v1)
(assert (= v1 (<= 0 v)))
(assert (> 10 v))

"""

p = parse_smt2_string(expr)
o.add(p)

print(o.check())
print(o.model())

输出： [v1 = false，v = -1]

有人会知道为什么在允许它的V值时，软约束不满足？

同样，此程序也不会返回预期的输出：

from z3 import *
o = Optimize()


expr = f"""
(declare-const v1 Real)
(declare-const e Bool)
(assert (= e (<= 6 v1)))
(assert-soft e)
"""

p = parse_smt2_string(expr)
o.add(p)

print(o.check())
print(o.model())

它返回[V1 = 0，e = false]。为什么不能实现软限制？

Answer 1

它出现parse_smt2_string do 不是保留软主张。

如果添加print（o.sexpr（））在调用检查之前，它会打印：

(declare-fun v () Real)
(declare-fun v1 () Bool)
(assert (= v1 (<= (to_real 0) v)))
(assert (> (to_real 10) v))

如您所见，Soft-Constraint已消失。因此，Z3看到的不是您认为的。这解释了意外的输出。

我知道parse_smt2_string并不是完全忠实的，因为它不处理任意的smtlib输入。我不确定是否支持这种特殊情况。将其作为问题归档， https://github.com/z3prover/z3prover/z3/sissues 开发人员可能会看看。