(Z3Py) checking all solutions for equation
The python function below is a generator of models for formulas that contain both constants and functions.
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)
You can do that by adding a new constraint that blocks the model returned by Z3.
For example, suppose that in the model returned by Z3 we have that x = 0
and y = 1
. Then, we can block this model by adding the constraint Or(x != 0, y != 1)
.
The following script does the trick.
You can try it online at: http://rise4fun.com/Z3Py/4blB
Note that the following script has a couple of limitations. The input formula cannot include uninterpreted functions, arrays or uninterpreted sorts.
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