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似乎不保留软断言。

如果在调用print(o.sexpr())之前添加check，它会打印：

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

正如你所看到的，软约束已经消失了。所以，z3看到的不是你想象的那样。这解释了意外的输出。

我知道parse_smt2_string并不完全忠实，因为它不处理任意的SMTLib输入。这个案子是否得到支持，我不确定。将其作为一个问题提交给https://github.com/Z3Prover/z3/issues，开发人员可能会看一看。