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!

Indopacific

add python tag ; z3 is in different lang – Noun

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)

Callboard

Answer 2

The only binding operators supported in Z3 are universal and existential quantifiers. So lambdas that can be used for summations are not supported. You can alternatively define a self-contained function for each summation term and write axioms that characterize that function. Z3 will have to rely on what it can establish by quantifier instantiation to establish properties of your summations.

Asseverate

Answer 3

It has been more than a few years since this question was posted, but I recently ran into it. The top answer by Mark is probably the best, but if you don't want to define the summation function as a z3 function and add its definiton as a formula (which is a thing I didn't want to do in my case), you can do something like this, if you have an upper bound on your array size:

from z3 import *

i = Int('i')
arr = Array('arr', IntSort(), IntSort())
sum_formula = Sum([If(k < i, arr[k], 0) for k in range(ARRAY_LENGTH)])

In this case sum_formula is a formula that reperesents the sum of the first i elements of the array.

Preeminent