(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?

Bevash

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

Rondo

I also would like to ask, is the same possible in Z3's SMT language extension? – Bevash

No, it is not. However, I think it is a good idea to add this command in the SMT 2.0 front-end. – Rondo

Could you add a note to explain why uninterpreted functions and arrays are not supported using this method? Is it an accidental limitation (the data structures aren't ExprRefs, or something) or a more fundamental one? – Latarsha

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

Nunciata

yield from all_smt_rec(terms[i+1:]) is incorrect, rather it should be yield from all_smt_rec(terms[i:]) I pointed this bug out to Nikolaj in his previous implementation too. Keeping all terms upto i to be the same, [i:] since we still have to vary and find all solutions for term[i] term[i+1:] essentially implies that we take only a single assignment for the term[i] keeping all term[:i] fixed – Dorcy

Good catch! Corrected. – Nunciata

This answer seems to be identical to the answer by @HimanshuSheoran. If you have just a minor correction to another answer, wouldn't it be better to simply edit it? – Artisan

@HimanshuSheoran: I have strong doubts that this one is actually a bug: Inductively assume that all_smt_rec enumerats all distinguished models for n terms. The base cases for n=0,1 are trivial. Now consider n+1 terms for a model of s. Any further model of s must be distinguishable in at least one term. By induction follows that the for loop over i enumerates all model by blocking the term i (to disinguish from the initial model) and fixing the terms j<i (to make models disjoint) can be done by calling all_smt_rec(terms[i+1:]), i.e., calling all_smt_rec with n or less terms. – Mola

@WillemHagemann you can follow the discussion (and a trivial example) here github.com/Z3Prover/z3/issues/5765#issuecomment-1009760596 Your reasoning is fine if the terms are boolean, but if they are not, you are effectively blocking a single evaluation of terms[i] thus skipping all possible solutions for terms[i] As I have run this piece of code thousands of times myself, I can assure you its correct – Dorcy

@HimanshuSheoran thank you for explaining and the discussion link. So far I thought of boolean terms only. But of course for non boolean valued terms the term[i+1:] optimization is incomplete. I thank you for this insight. – Mola

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)

Wallaroo

For generic use I'd pass the formula-enhanced solver to models() instead of the formula, and wrap the while loop with push/pop. – Stores

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

Dorcy

Great find! This is indeed a lot faster in my experiments too. – Nunciata

Minor nit: use yield from … instead of for x in …: yield x. – Stores

Note that there's a bug in the implementation of all_smt in that paper. See github.com/Z3Prover/z3/issues/5765#issuecomment-1009135689 for the fix. – Nunciata