你知道如何设置“弱"吗?每个 z3 Array 元素的初始值? [英] Do you know how to set "weak" initial values to each of z3 Array element?

问题描述

例如，Z3 中是否有类似下面的weak_Store 函数?

For example, is there a something like below weak_Store function in Z3?

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来做.

I think this is related to model_completion variable in z3_model_eval, but z3_model_eval does not work for z3 Array element. Although the example is written in Python, I would like to do it with z3 C api.

有人可以帮我吗?

提前致谢.

推荐答案

这种约束被称为软"约束，即在必要时可以违反的约束，但求解器将尝试满足它们.请注意，您必须使用 Optimize 对象(而不是 Solver)，它通常会降低容量.(即更慢，更有可能说 unknown 等)

This sort of constraints are called "soft" constraints, i.e., those that can be violated if necessary, but the solver will try to satisfy them otherwise. Note that you have to use the Optimize object, (not Solver), which has diminished capacity in general. (i.e., slower, more likely to say unknown etc.)

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

To add a soft constraint, use add_soft instead of add in z3py. You can code your example in Python like this:

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.

In the C-API, the corresponding call is Z3_optimize_assert_soft.

这篇关于你知道如何设置“弱"吗?每个 z3 Array 元素的初始值?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！