0

This might not beyond the scope of z3, I know in Z3 we can simplify expression, but I wonder if z3 can solve the equation instead of giving a model.

For example, I want the following equation always be true for any value of a. Using ForAll quantifier in this case would return unsat. 

     a == b - c + 2

The solution I expect is a formula for one specified variable while simplify doesn't deal with this, like

     b == a + c - 2 or c == b - a + 2

Is there any API for this ? Thanks in advance.

Pounce
  • 25
  • 4

1 Answers1

0

Not sure what exactly the question is here, but it sounds like you want to get all satisfying solutions instead of a single satisfying solution. It is possible to encode that (with quantifiers), but not necessarily easy to solve; depending on the fragment of logic used within the quantifiers, Z3 may be slow, or it may simply give up relatively early (returning unknown). There is no dedicated API for this purpose, but the existing API has all the pieces required to solve the puzzle (e.g., use an uninterpreted function f to encode the solution symbolically and then get the func_interp for f from the model.)

For more information about getting more than one solution, see also Z3: finding all satisfying models and Z3 Enumerating all satisfying assignments.

Community
  • 1
  • 1
Christoph Wintersteiger
  • 8,234
  • 1
  • 16
  • 30
  • Thanks for your reply, maybe the question is confusing. Assume I have a set of expressions, and the goal is to pick some expressions so that the formula x = y + 1 always be true. First expression x = z - 3 is chosen, then I expect z3 gives a solution that maps z to y + 4. If I try to simplify the formula it would not have the exact value of z as a solution. I wonder if function interpretation can be represented in this way. – Pounce Aug 03 '15 at 17:31