Sum array in z3 solver

Question

I am trying to express the sum of the range of an unbounded Array in z3. For instance in Python:

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

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

........

Is there any way to complete the definition of 'sum'? Otherwise, is there a more plausible alternative?

Thanks!

Answer 1

Here is how to constrain the sum of the Array that I think

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])))

Suppose if you know the length of the Array is 2, and the sum of the Array is 4, you can constrain the sum as follows

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

If the length of the Array is to be inferred, then constrain the sum of Array like this

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