Как в Z3Py проверить, имеет ли уравнение для заданных ограничений только одно решение?
Если решений несколько, как их перечислить?
Как в Z3Py проверить, имеет ли уравнение для заданных ограничений только одно решение?
Если решений несколько, как их перечислить?
Вы можете сделать это, добавив новое ограничение, которое блокирует модель, возвращаемую Z3. Например, предположим, что в модели, возвращенной Z3, у нас есть эти x = 0
и y = 1
. Затем мы можем заблокировать эту модель, добавив ограничение Or(x != 0, y != 1)
. Следующий сценарий делает свое дело. Вы можете попробовать его в Интернете по адресу: http://rise4fun.com/Z3Py/4blB
Обратите внимание, что следующий сценарий имеет несколько ограничений. Формула ввода не может включать неинтерпретированные функции, массивы или неинтерпретированные сортировки.
from z3 import *
# Return the first "M" models of formula list of formulas F
def get_models(F, M):
result = []
s = Solver()
s.add(F)
while len(result) < M and s.check() == sat:
m = s.model()
result.append(m)
# Create a new constraint the blocks the current model
block = []
for d in m:
# d is a declaration
if d.arity() > 0:
raise Z3Exception("uninterpreted functions are not supported")
# create a constant from declaration
c = d()
if is_array(c) or c.sort().kind() == Z3_UNINTERPRETED_SORT:
raise Z3Exception("arrays and uninterpreted sorts are not supported")
block.append(c != m[d])
s.add(Or(block))
return result
# Return True if F has exactly one model.
def exactly_one_model(F):
return len(get_models(F, 2)) == 1
x, y = Ints('x y')
s = Solver()
F = [x >= 0, x <= 1, y >= 0, y <= 2, y == 2*x]
print get_models(F, 10)
print exactly_one_model(F)
print exactly_one_model([x >= 0, x <= 1, y >= 0, y <= 2, 2*y == x])
# Demonstrate unsupported features
try:
a = Array('a', IntSort(), IntSort())
b = Array('b', IntSort(), IntSort())
print get_models(a==b, 10)
except Z3Exception as ex:
print "Error: ", ex
try:
f = Function('f', IntSort(), IntSort())
print get_models(f(x) == x, 10)
except Z3Exception as ex:
print "Error: ", ex
Функция python ниже представляет собой генератор моделей для формул, содержащих как константы, так и функции.
import itertools
from z3 import *
def models(formula, max=10):
" a generator of up to max models "
solver = Solver()
solver.add(formula)
count = 0
while count<max or max==0:
count += 1
if solver.check() == sat:
model = solver.model()
yield model
# exclude this model
block = []
for z3_decl in model: # FuncDeclRef
arg_domains = []
for i in range(z3_decl.arity()):
domain, arg_domain = z3_decl.domain(i), []
for j in range(domain.num_constructors()):
arg_domain.append( domain.constructor(j) () )
arg_domains.append(arg_domain)
for args in itertools.product(*arg_domains):
block.append(z3_decl(*args) != model.eval(z3_decl(*args)))
solver.add(Or(block))
x, y = Ints('x y')
F = [x >= 0, x <= 1, y >= 0, y <= 2, y == 2*x]
for m in models(F):
print(m)
Ссылка на http://theory.stanford.edu/%7Enikolaj/programmingz3.html#sec-blocking-evaluations
def all_smt(s, initial_terms):
def block_term(s, m, t):
s.add(t != m.eval(t))
def fix_term(s, m, t):
s.add(t == m.eval(t))
def all_smt_rec(terms):
if sat == s.check():
m = s.model()
yield m
for i in range(len(terms)):
s.push()
block_term(s, m, terms[i])
for j in range(i):
fix_term(s, m, terms[j])
for m in all_smt_rec(terms[i:]):
yield m
s.pop()
for m in all_smt_rec(list(initial_terms)):
yield m
Это действительно работает лучше из собственного ответа Леонардо (учитывая, что его ответ довольно старый)
start_time = time.time()
v = [BitVec(f'v{i}',3) for i in range(6)]
models = get_models([Sum(v)==0],8**5)
print(time.time()-start_time)
#211.6482105255127s
start_time = time.time()
s = Solver()
v = [BitVec(f'v{i}',3) for i in range(6)]
s.add(Sum(v)==0)
models = list(all_smt(s,v))
print(time.time()-start_time)
#13.375828742980957s
Насколько я заметил, разделение пространства поиска на непересекающиеся модели создает огромную разницу.