如何在 Z3Py 中声明/使用数组和量词？

Question

我是 Z3py 的新手，我发现了一个练习，它会要求检查某些验证条件是否为真。到目前为止，我所做的练习基本上是将简单的命题公式转换为 z3py 子句，例如：

Propositional Formula would be:

(n>=4) -> (x = y +2)

Which would become in Z3Py:

n, x, y = Ints('n x y')

s.add(Implies(n>=5, x == y+3))

我现在提出的条件，介绍数组和量词，在花了几个小时试图在文档中弄明白之后，我仍然无法正确完成它。

例如，我将如何执行上述相同的过程，但条件如下：

n ≥ 1 ∧ i = 1 ∧ m = A[0]
i <= n ∧ ∀j. 0 ≤ j < i → m ≥ A[j]

我认为正确完成的事情的一点点：

i, n = Ints('i n')

s.add(And(n>=1, i == 1, ???)
s.add(And(i<=n,Implies(???))

我应该如何替换???以便将条件正确转换为 Z3Py？

解决方案：

- The constraint

n ≥ 1 ∧ i = 1 ∧ m = A[0]

would become in Z3Py:

A = Array('A', IntSort(), IntSort()) //Array declaration
i, n, m, j = Ints('i n m j') //Ints declaration for both constraints

And(n>=1, i==1, m==A[0])

- The constraint

i <= n ∧ ∀j. 0 ≤ j < i → m ≥ A[j]

would become:

And(i<=n,ForAll(j,Implies(And(j>=0,j<i),m>=A[j])))

Answer 1

你的问题很模糊。请注意，您有以下限制：

n ≥ 1 ∧ i = 1

然后

i <= n

但是这个结果已经被第一个暗示了，因此是多余的。这意味着，如果您像使用 s.add 行一样将它们都添加到求解器中，那么它实际上并没有什么意义。

我猜这两行实际上出现在问题的不同“子部分”中，即它们没有一起用于相同的验证目标。而且，做一个有根据的猜测，你试图说出数组的最大元素；其中i 是某种循环计数器。第一行是循环开始之前发生的事情，第二行是循环体确保的不变量。如果是这种情况，您应该明确说明这一点。

假设是这种情况，那么这类问题通常以该循环的“主体”为模型，即，您需要向我们准确展示您正在处理的“程序”类型。也就是说，这些约束只有在您的程序变量存在某种转换时才有意义。