search

Z3Prover / z3

The Z3 Theorem Prover
Other
10.3k stars 1.48k forks source link

Translating SMT formula to conjunctive normal form #906

Closed gingeredder closed 7 years ago

gingeredder commented 7 years ago

Hello, I have a problem on how to translate an SMT formula to its conjunctive normal form.

E.g., in the LRA theory, we have the constraint like (in the disjunctive normal form) ((x - i = 0) /\ (y - j = 0)) \/ ((x - i = -1) /\ (y - j = -1)).

I want to translate this formula to its conjunctive normal form, like ((x - i = 0) \/ (x - i = -1)) /\ ((x - i = 0) \/ (y - j = -1)) /\ ((y - j = 0) \/ (x - i = -1)) /\ ((y - j = 0) \/ (y - j = -1)).

Is there any tactic or function to implement this translation?

cheshire commented 7 years ago

There is a tseitin-cnf tactic, which does the conversion at the cost of extra boolean variables. The transformation without introducing extra variables takes exponential space in general (though of course might be still trivially implemented, but not available off-the-shelf).

NikolajBjorner commented 7 years ago

You can use the programmatic API to manipulate formulas. So if you want a particular CNF transformation that, say, does not introduce fresh predicates as the tseitin-cnf tactic does, then you can write it as a recursive function on Z3 ast objects. Examples of functions that walk asts are in the examples directory.