Z3Py中如何正确声明和使用Array数组与量词Quantifiers？

问题背景 #

作为Z3Py初学者，此前完成的练习均为简单命题公式到Z3Py子句的转换，例如命题公式(n>=4) -> (x = y +2)对应的Z3Py实现为：

n, x, y = Ints('n x y')
s.add(Implies(n>=4, x == y + 2))

现在遇到包含Array和量词的约束条件，查阅相关文档后仍无法正确完成转换，需要转换的约束如下：

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(???)))

正确实现方案 #

首先需要提前声明数组类型变量和所有用到的整数变量，再分别传入两个约束即可：

前置变量声明 #

# 声明Int类型数组A，索引和存储值均为Int类型
A = Array('A', IntSort(), IntSort())
# 声明所有用到的整数变量
i, n, m, j = Ints('i n m j')

约束补全代码 #

• 第一行约束n ≥ 1 ∧ i = 1 ∧ m = A[0]只需将第一个???替换为m == A[0]即可，补全后代码：

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

• 第二行带全称量词的约束需要对原有代码结构做微调，增加ForAll关键字包裹量词逻辑，补全后代码：

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

内容的提问来源于stack exchange，提问作者Rohac