Say given a formula
(t1>=2 or t2>=3) and (t3>=1)
I wish to get its disjunctive normal form (t1>=2 and t3>=1) or (t2>=3 and t3>=1)
How to achieve this in Z3?
Z3 does not have an API or tactic for converting formulas into DNF. However, it has support for breaking a goal into many subgoals using the tactic split-clause
. Given an input formula in CNF, if we apply this tactic exhaustively, each output subgoal can be viewed as a big conjunction. Here is an example on how to do it.
Here is the command:
(apply (then simplify (repeat (or-else split-clause skip))))
The repeat
combinator keeps applying the tactic until it does not perform any modification.
The tactic split-clause
fails if the input does not have a clause. That is why we use an or-else
combinator with the skip
(do nothing) tactic. We can improve the command by using tactics that apply simplifications (e.g., simplify
, solve-eqs
) after each clause is split into cases.
Note that, the script above assumes the input formula is in CNF.