Search code examples
pythonz3z3py

(Z3Py) checking all solutions for equation


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?


Solution

  • 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