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?
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
andy = 1
. Then, we can block this model by adding the constraintOr(x != 0, y != 1)
. The following script does the trick. You can try it online at: http://rise4fun.com/Z3Py/4blBNote that the following script has a couple of limitations. The input formula cannot include uninterpreted functions, arrays or uninterpreted sorts.