您知道如何为每个 z3 Array 元素设置“弱”初始值吗？

Question

例如，Z3中是否有类似以下的weak_Store函数？

from z3 import * 

a = Array('a', IntSort(), IntSort()) 
a = weak_Store(a, 0, 0) 
a = weak_Store(a, 1, 1) 


s = Solver() 
s.add(a[0] == 100) 
print(s.check()) # should print "sat"

print(s.model().eval(a[0]))  # should print "100"
print(s.model().eval(a[1]))  # should print "1" which is stored as weak_Store. 

由于 a[1] 不参与上述约束求解，因此即使在 s.check() 之后也不应计算和更改。

我认为这与z3_model_eval 中的model_completion 变量有关， 但 z3_model_eval 不适用于 z3 Array 元素。 虽然这个例子是用 Python 写的，但我想用 z3 C api 来做。

谁能帮帮我？

提前谢谢你。

Answer 1

这种约束被称为“软”约束，即那些在必要时可以被违反的约束，但求解器将尝试在其他情况下满足它们。请注意，您必须使用Optimize 对象（而不是Solver），这通常会降低容量。 （即，更慢，更有可能说unknown等）

要添加软约束，请在 z3py 中使用 add_soft 而不是 add。您可以像这样在 Python 中编写示例代码：

from z3 import *

a = Array('a', IntSort(), IntSort())

s = Optimize()

s.add_soft(a[0] == 0)
s.add_soft(a[1] == 1)

s.add(a[0] == 100)
print(s.check())

print(s.model().eval(a[0]))
print(s.model().eval(a[1]))

打印出来：

sat
100
1

如您所愿。

在C-API中，对应的调用是Z3_optimize_assert_soft。