Как получить существующие ограничения из объекта Z3 Solver в z3py? - PullRequest
Новая
       81

Как получить существующие ограничения из объекта Z3 Solver в z3py?

0 голосов
/ 14 апреля 2020

Например, я хочу получить существующие ограничения из 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

1 Ответ

2 голосов
/ 14 апреля 2020

Если требуется получить вектор всех ограничений, добавленных к экземпляру 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]

[source : z3 документы]

Пример: 

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