z3py:如何在 z3py 中表示整数或字符数组
z3py: how to represent an array of integers or characters in z3py
我是 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
我应该使用 Array 或 IntVector,还是其他任何东西来表示 input/output 数组?
编辑:
我的代码如下:
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()
它returns
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]]
我不明白 I、O、elem!0、elem!1 和 k!4 的意思,这显然不是我所期望的。
免责声明:我以前几乎没有用过 Z3py,但我用过很多 Z3。
我感觉您对编码逻辑问题也有些陌生 - 是吗?你的问题中有几件(奇怪的)事情发生了。
您对 x
和 y
施加了约束,但实际上您从未使用它们 - 相反,您绑定了 不同的 x
和 y
在你的量化断言中。后两者可能具有相同的名称,但它们与您约束的 x
和 y
完全无关(因为每个 forall 都绑定了自己的变量,您也可以在两者中使用 x
).因此,您量化的 x
和 y
范围涵盖所有 Int
,而您可能希望将它们限制在区间 [0..4)
内。为此使用 forall 中的蕴涵。
根据文档,Store(a, i, v)
returns 与 [=26 相同的新数组 a'
=],除了 x[i] == v
。也就是说,您需要调用 I = Store(I, 0, 1)
等,以便最终得到一个存储您想要的值的数组 I
。
既然你不这样做,Z3可以自由选择满足你约束条件的模型。从输出中可以看出,I
的模型是 [2 -> 2, else -> 2]
,表示 I[2] == 2
,I[i] == 2
表示任何 i != 2
。我不知道为什么 Z3 选择那个特定模型,但它(连同 O
的模型)满足您的要求。
你可以忽略elem!0
、elem!1
和k!4
,它们是内部生成的符号。
这是您示例的简化版本,未验证:
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(
And(
ForAll(x, Select(O,x) == Select(I,x)),
ForAll(x, Select(O,x) == Select(I,x+1))))
print s.check() # UNSAT
之所以不能满足是因为I[0] == 1 && I[1] == 2
,这与你的foralls矛盾。如果你用 0
实例化两个量化的 x
,你会得到 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
和 returns 模型,其中 I = []
,然后回想一下每个 Store(...)
returns 代表存储操作的新 Z3 表达式,其中每个依次 returns 一个新数组(等于初始数组,对更新取模)。正如 print
所示,I
的最终值是表达式 Store(Store(I, 0, 1), 1, 2)
。因此,让 I
本身成为空数组就足够了,即 I
- 更新(Store
s)将各自产生一个新数组(想想 I1
和 I2
在这种情况下),但由于它们是无名的,它们不会(或至少不必)出现在模型中。
如果您想在模型中明确查看数组的 "final" 值,您可以通过为最后一个 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]
这是我问题的正确答案:
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]]
我是 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
我应该使用 Array 或 IntVector,还是其他任何东西来表示 input/output 数组?
编辑:
我的代码如下:
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()
它returns
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]]
我不明白 I、O、elem!0、elem!1 和 k!4 的意思,这显然不是我所期望的。
免责声明:我以前几乎没有用过 Z3py,但我用过很多 Z3。
我感觉您对编码逻辑问题也有些陌生 - 是吗?你的问题中有几件(奇怪的)事情发生了。
您对
x
和y
施加了约束,但实际上您从未使用它们 - 相反,您绑定了 不同的x
和y
在你的量化断言中。后两者可能具有相同的名称,但它们与您约束的x
和y
完全无关(因为每个 forall 都绑定了自己的变量,您也可以在两者中使用x
).因此,您量化的x
和y
范围涵盖所有Int
,而您可能希望将它们限制在区间[0..4)
内。为此使用 forall 中的蕴涵。根据文档,
Store(a, i, v)
returns 与 [=26 相同的新数组a'
=],除了x[i] == v
。也就是说,您需要调用I = Store(I, 0, 1)
等,以便最终得到一个存储您想要的值的数组I
。既然你不这样做,Z3可以自由选择满足你约束条件的模型。从输出中可以看出,
I
的模型是[2 -> 2, else -> 2]
,表示I[2] == 2
,I[i] == 2
表示任何i != 2
。我不知道为什么 Z3 选择那个特定模型,但它(连同O
的模型)满足您的要求。你可以忽略
elem!0
、elem!1
和k!4
,它们是内部生成的符号。这是您示例的简化版本,未验证:
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( And( ForAll(x, Select(O,x) == Select(I,x)), ForAll(x, Select(O,x) == Select(I,x+1)))) print s.check() # UNSAT
之所以不能满足是因为
I[0] == 1 && I[1] == 2
,这与你的foralls矛盾。如果你用0
实例化两个量化的x
,你会得到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
和 returns 模型,其中 I = []
,然后回想一下每个 Store(...)
returns 代表存储操作的新 Z3 表达式,其中每个依次 returns 一个新数组(等于初始数组,对更新取模)。正如 print
所示,I
的最终值是表达式 Store(Store(I, 0, 1), 1, 2)
。因此,让 I
本身成为空数组就足够了,即 I
- 更新(Store
s)将各自产生一个新数组(想想 I1
和 I2
在这种情况下),但由于它们是无名的,它们不会(或至少不必)出现在模型中。
如果您想在模型中明确查看数组的 "final" 值,您可以通过为最后一个 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]
这是我问题的正确答案:
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]]