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?

Accepted Answer

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.

How to convert a formula to Disjunctive Normal Form?

Solution

Problem