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]