z3py中一组变量的最大值和最小值

Question

我有一个问题，我想限制一个实变量在另一组实变量的最大值和最小值之间的范围。

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

在z3py中有办法做到这一点吗？

Answer 1

您可以使用Axel的解决方案；不过，这需要您创建一个额外的变量，并且还需要声明比需要更多的约束。此外，它不允许将min和max作为简单函数使用。用一种实用的方式编写这个程序可能会更容易一些，比如：

# 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

另一个不同之处是，在函数样式中，如果向量是空的，我们会抛出一个错误。在另一种风格中，结果基本上是不受约束的。(也就是说，min/max可以取任何值。)您应该考虑哪个语义适合您的应用程序，以防您传递的向量可能是空的。(至少，您应该修改它，以便打印出更好的错误消息。当前，如果给出一个空向量，它将抛出一个IndexError: list index out of range错误。)

现在你可以说：

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

这些指纹：

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

你可以从哈坎·凯勒斯特兰的有用z3py定义的集合中获益

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