(Z3Py) checking all solutions for equation

Question

In Z3Py, how can I check if equation for given constraints have only one solution?

If more than one solution, how can I enumerate them?

Answer 1

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

Answer 2

The answer given by Himanshu Sheoran cites the paper https://theory.stanford.edu/%7Enikolaj/programmingz3.html#sec-blocking-evaluations

Unfortunately there was a bug in the implementation given in the paper at that time which was quoted in that answer. The function has since been corrected.

For posterity, here's the correct version of the code:

def all_smt(s, initial_terms):
    def block_term(s, m, t):
        s.add(t != m.eval(t, model_completion=True))
    def fix_term(s, m, t):
        s.add(t == m.eval(t, model_completion=True))
    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])
               yield from all_smt_rec(terms[i:])
               s.pop()   
    yield from all_smt_rec(list(initial_terms))

Answer 3

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)

Answer 4

Referencing http://theory.stanford.edu/~nikolaj/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])
               yield from all_smt_rec(terms[i:])
               s.pop()   
    yield from all_smt_rec(list(initial_terms))  

This indeed performs quite better from Leonardo's own answer (considering his answer is quite old)

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

Splitting the search space into disjoint models creates a huge difference as far as I have observed