Max and Min of a set of variables in z3py

Question

I have a problem where I want to limit the range of a real variable between the maximum and minimum value of another set of real variables.

s = Solver()
y = Real('y')
Z = RealVector('z', 10)
s.add(And(y >= min(Z), y <= max(Z)))

Is there a way to do this in z3py?

Answer 1

You can use Axel's solution; though that one requires you to create an extra variable and also asserts more constraints than needed. Moreover, it doesn't let you use min and max as simple functions. It might be easier to just program this in a functional way, like this:

# Return minimum of a vector; error if empty
def min(vs):
  m = vs[0]
  for v in vs[1:]:
    m = If(v < m, v, m)
  return m

# Return maximum of a vector; error if empty
def max(vs):
  m = vs[0]
  for v in vs[1:]:
    m = If(v > m, v, m)
  return m

Another difference is that in the functional style we throw an error if the vector is empty. In the other style, the result will essentially be unconstrained. (i.e., min/max can take any value.) You should consider which semantics is right for your application, in case the vector you're passing might be empty. (At the least, you should change it so it prints out a nicer error message. Currently it'll throw an IndexError: list index out of range error if given an empty vector.)

Now you can say:

s = Solver()
y = Real('y')
Z = RealVector('z', 10)
s.add(And(y >= min(Z), y <= max(Z)))
print (s.check())
print (s.model())

This prints:

sat
[z__7 = -1,
 z__0 = -7/2,
 z__4 = -5/2,
 z__5 = -2,
 z__3 = -9/2,
 z__2 = -4,
 z__8 = -1/2,
 y = 0,
 z__9 = 0,
 z__6 = -3/2,
 z__1 = -3]

Answer 2

You could benefit from Hakan Kjellerstrand's collection of useful z3py definitions:

from z3 import *

#  Functions written by Hakan Kjellerstrand 
#  http://hakank.org/z3/
#  The following can be used by importing http://www.hakank.org/z3/z3_utils_hakank.py

# v is the maximum value of x
def maximum(sol, v, x):
  sol.add(Or([v == x[i] for i in range(len(x))])) # v is an element in x)
  for i in range(len(x)):
    sol.add(v >= x[i]) # and it's the greatest

# v is the minimum value of x
def minimum(sol, v, x):
  sol.add(Or([v == x[i] for i in range(len(x))])) # v is an element in x)
  for i in range(len(x)):
    sol.add(v <= x[i]) # and it's the smallest

s = Solver()
y = Real('y')
zMin = Real('zMin')
zMax = Real('zMax')
Z = RealVector('z', 10)

maximum(s, zMin, Z)
minimum(s, zMax, Z)

s.add(And(y >= zMin, y <= zMax))

print(s.check())
print(s.model())