如何从z3py中的Z3解算器对象中获取现有约束

Question

例如，我想将现有约束从s中获取并放入Optimize对象中。

from z3 import *
a = Int('a')
x = Int('x')
b = Array('I', IntSort(), IntSort())
s = Solver()
s.add(a >= 0)
s.add(x == 0)
s.add(Select(b, 0) == 10)
s.add(Select(b, x) >= a)
opt = Optimize()
opt.add(s.constraints)
obj1 = opt.maximize(a)
obj2 = opt.minimize(a)
opt.set('priority', 'box')   # Setting Boxed Multi-Objective Optimization
is_sat = opt.check()
assert is_sat
print("Max(a): " + str(obj1.value()))
print("Min(a): " + str(obj2.value()))

那么结果会是这样的。

~$ python test.py 
Max(a): 10
Min(a): 0

Answer 1

如果想要获得添加到Solver(或Optimize(实例的所有约束的向量，可以使用方法assertions():

|  assertions(self)
|      Return an AST vector containing all added constraints.
|      
|      >>> s = Solver()
|      >>> s.assertions()
|      []
|      >>> a = Int('a')
|      >>> s.add(a > 0)
|      >>> s.add(a < 10)
|      >>> s.assertions()
|      [a > 0, a < 10]

【来源：z3 docs】

示例：

from z3 import *
a = Int('a')
x = Int('x')
b = Array('I', IntSort(), IntSort())
s = Solver()
s.add(a >= 0)
s.add(x == 0)
s.add(Select(b, 0) == 10)
s.add(Select(b, x) >= a)
opt = Optimize()
opt.add(s.assertions())
obj1 = opt.maximize(a)
obj2 = opt.minimize(a)
opt.set('priority', 'box')
is_sat = opt.check()
assert is_sat
print("Max(a): " + str(obj1.value()))
print("Min(a): " + str(obj2.value()))

输出：

~$ python test.py 
Max(a): 10
Min(a): 0