How to convert a formula to Disjunctive Normal Form?

Question

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?

Answer 1

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.

http://rise4fun.com/Z3/zMjO

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.