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