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

Question

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

\n\n

这是我的问题设置：

\n\n

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

\n\n

我想推断运算符Delete的k，它删除数组中位置k处的元素，其中

\n\n

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

\n\n

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

\n\n

编辑：

\n\n

我的代码如下：

\n\n

from z3 import *\n\nk=Int('k')\ns=Solver()\n\nx = Int('x')\ny = Int('y')\n\ns.add(k >= 0)\ns.add(k < 4)    \ns.add(x >= 0)\ns.add(x < k)\ns.add(y >= k)\ns.add(y < 4)\n\nI = Array('I',IntSort(),IntSort())\nO = Array('O',IntSort(),IntSort())\nStore(I, 0, 1)\nStore(I, 1, 2)\nStore(I, 2, 3)\nStore(I, 3, 4)\nStore(I, 4, 5)\n\nStore(O, 0, 1)\nStore(O, 1, 2)\nStore(O, 2, 4)\nStore(O, 3, 5)\n\ns.add(And(ForAll(x,Select(O,x) == Select(I,x)),ForAll(y,Select(O,y) == Select(I,y+1))))\nprint s.check()\nprint s.model()\n

\n\n

它返回

\n\n

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

\n\n

我不明白 I、O、elem!0、elem!1 和 k!4 的含义，这显然不是我所期望的。

\n

Answer 1

免责声明：我以前几乎没有使用过 Z3py，但我已经使用过 Z3 相当多了。

\n\n

我感觉你对编码逻辑问题也有些陌生——可能是这样吗？您的问题中发生了一些（奇怪的）事情。

\n\n

\n

1. x您对和施加了约束y，但实际上您从未使用它们 - 相反，您在量化断言中绑定了不同的 x和。y后两者可能具有相同的名称，但它们与您所约束的x和完全无关y（因为每个 forall 绑定其自己的变量，因此您也可以x在两者中使用）。因此，您对所有内容进行量化x和y范围Int，而您可能希望将它们限制在间隔内[0..4)。为此，请在 forall 中使用暗示。

\n

2. 根据文档，Store(a, i, v) 返回a\'一个与 相同的新数组a，除了x[i] == v。也就是说，您需要调用I = Store(I, 0, 1)etc. 才能最终获得一个I存储所需值的数组。

\n

3. 由于您不这样做，Z3 可以自由选择满足您的约束的模型。正如您从输出中看到的， 的模型I是[2 -> 2, else -> 2]，它表示I[2] == 2，并且I[i] == 2对于任何i != 2。我不知道为什么 Z3 选择了那个特定的型号，但它（连同 的型号O）满足了您的要求。

\n

4. 您可能可以忽略elem!0、elem!1和k!4，它们是内部生成的符号。

\n

5. 这是示例的简化版本，未验证：

   \n\n

   x = Int(\'x\') \xc2\xa0\nI = Array(\'O\',IntSort(),IntSort())\nO = Array(\'O\',IntSort(),IntSort())\n\nI = Store(I, 0, 1)\nI = Store(I, 1, 2)\n\ns.add(\n  And(\n    ForAll(x, Select(O,x) == Select(I,x)),\n    ForAll(x, Select(O,x) == Select(I,x+1))))\n\nprint s.check() # UNSAT\n

   \n\n

   之所以无法满足，是因为I[0] == 1 && I[1] == 2它与你的愿望相矛盾。如果你用 来实例化两者x，0你会得到O[0] == I[0] && O[0] == I[1]一个无法满足的约束，即没有模型O可以满足它。

\n

\n\n

编辑（解决评论）：

\n\n

如果您困惑为什么，给定一个片段，例如

\n\n

I = Array(\'O\',IntSort(),IntSort())\nI = Store(I, 0, 1)\nI = Store(I, 1, 2)\n# print(I)\ns.check()\ns.model()\n

\n\n

Z3 报告sat并返回一个模型I = []，其中 ，然后回想一下，每个模型都Store(...)返回一个代表存储操作的新 Z3 表达式，每个表达式又返回一个新数组（等于初始数组，对更新取模）。如图print所示， 的最终值I是表达式Store(Store(I, 0, 1), 1, 2)。因此，让它I自己成为空数组就足够了，即I- 更新（Stores）将每次产生一个新的数组（想想I1在I2这种情况下），但由于它们是无名的，所以它们不会（或至少不会）不必）出现在模型中。

\n\n

如果您想在模型中显式查看数组的“最终”值，可以通过为最后创建的数组指定名称来实现此目的Store，例如

\n\n

I = Array(\'I\',IntSort(),IntSort())\nI = Store(I, 0, 1)\nI = Store(I, 1, 2)\n\nII = Array(\'II\',IntSort(),IntSort())\ns.add(I == II)\n\ns.check()\ns.model() # includes II = [1 -> 2, 0 -> 1, else -> 3]\n

\n