CODEWITHSUNDEEP
z3smt
william007
william007

Reputation: 18545

How to convert a formula to Disjunctive Normal Form?

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?

Upvotes: 5

Views: 3878

Answers (1)

Leonardo de Moura
Leonardo de Moura

Reputation: 21475

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.

Upvotes: 8

Related Questions