z3 求解器中的求和数组

Question

我试图表达 z3 中一个无界数组的范围之和。例如在 Python 中：

IntArray = ArraySort(IntSort(), IntSort())

sum = Function('sum', IntArray, IntSort())

........

有没有办法完成' sum'的定义？否则，有没有更合理的选择？

谢谢！

Answer 1

以下是如何约束我认为的 Array 的总和

IntArray = Array('IntArray',IntSort(),IntSort())
sumArray = Function('sumArray',IntSort(),IntSort())
s.add(sumArray(-1)==0)
i = Int('i')
s.add(ForAll(i,Implies(And(i>=0,i<3),sumArray(i)==sumArray(i-1)+IntArray[i])))

假设你知道Array的长度是2，Array的和是4，你可以这样约束和

s.add(sumArray(2)==4)

如果要推断 Array 的长度，则像这样约束 Array 的总和

x = Int('x')
s.add(sumArray(x)=4)

Answer 2

Z3 中唯一支持的绑定运算符是通用量词和存在量词。因此不支持可用于求和的 lambda。您也可以为每个求和项定义一个独立的函数，并编写表征该函数的公理。Z3 将必须依靠它通过量词实例化所建立的内容来建立求和的属性。