如何使用 z3 中的变量列表

Question

我是 z3 的新手，不知道如何做一些简单的事情。拿这个简单的代码：

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

这很好用。但是，如果我有更多变量，我不确定如何执行以下操作：

如何定义 20 个或更多变量而不必将它们显式列为 a,b,c,d,e ... = z3.Ints('a b c d ...')?
如何计算包含 20 个或更多变量的列表的最大值？
如果我有一个包含 20 个或更多变量的列表，我该怎么做Or(x != s.model()[x], y != s.model()[y])？

Answer 1

您的问题与 z3 无关；但关于常规 python 编程。在这种情况下，z3 真的没有什么特别之处，您只需使用常规的编程结构：函数、递归、循环等。

这是一个让您入门的示例。它会完成您要问的所有事情（尽管使用更简单的约束），您可以自己设置可变数量的参数：

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

当我运行这个时，我得到：

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

希望您能够根据自己的需要调整此程序。询问有关你在哪里卡住的具体问题通常比询问笼统的问题更有效率；但随时 post 遇到新问题。

如何使用 z3 中的变量列表

How to work with a list of variables in z3

python

z3

z3py