z3py:如何在z3py中表示整数或字符数组

Question

我是z3py和SMT的新手，我还没有找到一个关于z3py的好教程。

以下是我的问题设置：

给定输入整数数组I=1,2,3,4,5和输出整数数组O=1,2,4,5。

我想为操作符Delete推断k，它在数组中的位置k处删除元素，其中

Delete(I,O) =  (ForAll 0<=x<k, O[x] = I[x] ) and (ForAll k<=x<length(I)-1, O[x] = I[x+1]) is true

我应该使用数组或IntVector或其他任何东西来表示输入/输出数组吗？

编辑：

我的代码如下：

from z3 import *

k=Int('k')
s=Solver()

x = Int('x')
y = Int('y')

s.add(k >= 0)
s.add(k < 4)    
s.add(x >= 0)
s.add(x < k)
s.add(y >= k)
s.add(y < 4)

I = Array('I',IntSort(),IntSort())
O = Array('O',IntSort(),IntSort())
Store(I, 0, 1)
Store(I, 1, 2)
Store(I, 2, 3)
Store(I, 3, 4)
Store(I, 4, 5)

Store(O, 0, 1)
Store(O, 1, 2)
Store(O, 2, 4)
Store(O, 3, 5)

s.add(And(ForAll(x,Select(O,x) == Select(I,x)),ForAll(y,Select(O,y) == Select(I,y+1))))
print s.check()
print s.model()

它回来了

sat
[I = [2 -> 2, else -> 2],
 O = [2 -> 2, else -> 2],
 y = 1,
 k = 1,
 x = 0,
 elem!0 = 2,
 elem!1 = 2,
 k!4 = [2 -> 2, else -> 2]]

我不明白我，O，elem!0，elem!1和k!4的意思，这显然不是我所期望的。

Answer 1

免责声明:我以前很少使用Z3py，但我使用过相当多的Z3。

我有一种感觉，你对编码逻辑问题也有点陌生--这会是吗？你的问题中有几件(奇怪的)事情正在发生。

1. 您在x和y上设置了约束，但实际上从未使用它们--而是在量化的断言中绑定不同的x和y。后两者可能具有相同的名称，但它们与您约束的x和y完全无关(因为每个变量都绑定了自己的变量，您也可以在这两个变量中使用x )。因此，量化的x和y范围涵盖了所有Int，而您可能希望将它们限制在间隔[0..4)上。为此，请在forall中使用一种含义。
2. 根据文档，Store(a, i, v)返回一个与a相同的新数组a'，但x[i] == v除外。也就是说，您需要调用I = Store(I, 0, 1)等，以便最终获得存储所需值的数组I。
3. 由于没有这样做，Z3可以自由选择满足约束的模型。从输出中可以看到，I的模型是[2 -> 2, else -> 2]，它表示I[2] == 2，对于任何i != 2都是I[i] == 2。我不知道Z3为什么选择这个特定的模型，但是它(连同O的模型)满足了您的需求。
4. 您可能会忽略elem!0、elem!1和k!4，它们是内部生成的符号。
5. 下面是一个简化的示例版本，它不会验证： X= Int('x') i= Array('O'，IntSort()，IntSort()O= Array('O'，IntSort()，IntSort()i= Store(I，0，1) I= Store(I，1，2) s.add(和ForAll(x，Select(O，x) == Select(I，x))，ForAll(x，Select(O，x) == Select(I，x+1)打印s.check() 它不能满足的原因是I[0] == 1 && I[1] == 2，它与你的福尔斯相矛盾。如果使用0实例化两个量化的O[0] == I[0] && O[0] == I[1]，则得到O[0] == I[0] && O[0] == I[1]--这是一个无法满足的约束，即O没有满足它的模型。

编辑(处理评论)：

如果你不明白为什么，给出一个片段，比如

I = Array('O',IntSort(),IntSort())
I = Store(I, 0, 1)
I = Store(I, 1, 2)
# print(I)
s.check()
s.model()

Z3报告sat并返回模型I = []，然后回顾每个Store(...)返回一个表示存储操作的新Z3表达式，每个表达式依次返回一个新数组(与初始数组相等，对更新进行模块化)。正如print所示，I的最终值是表达式Store(Store(I, 0, 1), 1, 2)。因此，让I本身成为空数组就足够了，即I --每个更新( Stores)都会产生一个新的数组(在本例中是I1和I2 )，但是由于它们是匿名的，所以它们不会(或者至少不必)出现在模型中。

如果您想在模型中显式地看到数组的“最终”值，可以通过给上一个Store创建的数组命名来实现这一点，例如

I = Array('I',IntSort(),IntSort())
I = Store(I, 0, 1)
I = Store(I, 1, 2)

II = Array('II',IntSort(),IntSort())
s.add(I == II)

s.check()
s.model() # includes II = [1 -> 2, 0 -> 1, else -> 3]

Answer 2

这是我的问题的正确答案：

from z3 import *

x = Int('x')  
y = Int('y')
k = Int('k')

s = Solver()

I = Array('I',IntSort(),IntSort())
O = Array('O',IntSort(),IntSort())
I = Store(I, 0, 1)
I = Store(I, 1, 2)
I = Store(I, 2, 3)
I = Store(I, 3, 4)
I = Store(I, 4, 5)

O = Store(O, 0, 1)
O = Store(O, 1, 2)
O = Store(O, 2, 4)
O = Store(O, 3, 5)

s.add(k >= 0)
s.add(k < 4)
s.add(And(ForAll([x],Implies(And(x>=0,x<k),Select(O,x) == Select(I,x))),ForAll([y],Implies(And(y>=k,y<4),Select(O,y) == Select(I,y+1)))))
print s.check()
if s.check() == z3.sat:
    print s.model()

答案是

sat
[I = [2 -> 2, else -> 2],
 k = 2,
 O = [2 -> 2, else -> 2],
 k!17 = [2 -> 2, else -> 2]]