How to work with a list of variables in z3

Question

I am new to z3 and am not sure how to do some simple things. Take this simple code:

    import z3
    def max(x, y):
       return z3.If(x>=y, x, y)

    x, y, z, w = z3.Ints('x y z w')
    s = z3.Solver()

    s.add(x-2*y==11)
    s.add(z**2-x*y*w**2==1)
    s.add(z>0)
    s.add(w>0)
    max(x, y) < 10
    s.check()
    while s.check() == z3.sat:
        print(s.model())
        s.add(z3.Or(x != s.model()[x], y != s.model()[y]))

This works fine. But if I have more variables I am not sure how to do the following:

1. How can I define 20 or more variables without having to explicitly list them as a,b,c,d,e ... = z3.Ints('a b c d ...')?
2. How can I compute the maximum of a list of 20 or more variables?
3. How can I do Or(x != s.model()[x], y != s.model()[y]) but with a list of 20 or more variables?

Answer 1

Your question isn't really about z3; but about regular python programming. There's really nothing special about z3 in this case, you just use your regular programming constructs: functions, recursion, loops etc.

Here's an example to get you started. It does all the things you're asking about (using simpler constraints though), for a variable number of arguments that you can set yourself:

from z3 import *

# change the number of variables as you wish
# by setting the following variable
no_of_vars = 5

myVars = []

for i in range(no_of_vars):
    myVars += [Int('v%d' % i)]

# compute the max of a set of variables
def max(vs):
  m = vs[0]
  for v in vs[1:]:
    m = If(v > m, v, m)
  return m

s = Solver()

# Some simple constraints:
s.add(myVars[0] >= 0)

for i, j in zip(myVars, myVars[1:]):
    s.add(i < j)

s.add(max(myVars) < no_of_vars+2)

# collect all models
while s.check() == sat:
    model = s.model()

    block       = []
    curSolution = []
    for var in myVars:
        v = model.eval(var, model_completion=True)
        block.append(var != v)
        curSolution += [(var, v)]

    print(curSolution)

    s.add(Or(block))

When I run this, I get:

[(v0, 0), (v1, 1), (v2, 2), (v3, 3), (v4, 4)]
[(v0, 1), (v1, 2), (v2, 3), (v3, 4), (v4, 5)]
[(v0, 1), (v1, 2), (v2, 4), (v3, 5), (v4, 6)]
[(v0, 2), (v1, 3), (v2, 4), (v3, 5), (v4, 6)]
[(v0, 1), (v1, 3), (v2, 4), (v3, 5), (v4, 6)]
[(v0, 0), (v1, 3), (v2, 4), (v3, 5), (v4, 6)]
[(v0, 0), (v1, 1), (v2, 2), (v3, 3), (v4, 6)]
[(v0, 0), (v1, 1), (v2, 2), (v3, 3), (v4, 5)]
[(v0, 0), (v1, 2), (v2, 3), (v3, 4), (v4, 5)]
[(v0, 0), (v1, 1), (v2, 3), (v3, 4), (v4, 5)]
[(v0, 0), (v1, 1), (v2, 2), (v3, 4), (v4, 5)]
[(v0, 1), (v1, 2), (v2, 3), (v3, 5), (v4, 6)]
[(v0, 1), (v1, 2), (v2, 3), (v3, 4), (v4, 6)]
[(v0, 0), (v1, 2), (v2, 4), (v3, 5), (v4, 6)]
[(v0, 0), (v1, 2), (v2, 3), (v3, 5), (v4, 6)]
[(v0, 0), (v1, 1), (v2, 4), (v3, 5), (v4, 6)]
[(v0, 0), (v1, 2), (v2, 3), (v3, 4), (v4, 6)]
[(v0, 0), (v1, 1), (v2, 3), (v3, 5), (v4, 6)]
[(v0, 0), (v1, 1), (v2, 3), (v3, 4), (v4, 6)]
[(v0, 0), (v1, 1), (v2, 2), (v3, 5), (v4, 6)]
[(v0, 0), (v1, 1), (v2, 2), (v3, 4), (v4, 6)]

Hopefully, you should be able to adapt this program for your needs. Asking specific questions about where you get stuck is usually more productive on stack-overflow, than asking over-arching questions; but feel free to post new problems as you come across.