Wie konvertiert man eine Formel in disjunktive Normalform?

Question

Say

eine Formel

(t1> = 2 oder T2> = 3) und (t3> = 1)

Ich wünschte seine disjunktive Normalform (t1> = 2 und t 3> erhalten = 1) oder (t2> = 3 und t3> = 1)

Wie erreicht man dies in Z3?

Answer 1

Z3 hat keine API oder Taktik zum Umwandeln von Formeln in DNF. Es hat jedoch Unterstützung für das Unterbrechen eines Ziels in viele Teilziele mit der Taktik split-clause. Bei einer Eingabeformel in CNF kann jedes Ausgabeunterziel als eine große Konjunktion betrachtet werden, wenn wir diese Taktik erschöpfend anwenden. Hier ist ein Beispiel, wie es geht. Hier

http://rise4fun.com/Z3/zMjO

ist der Befehl:

(apply (then simplify (repeat (or-else split-clause skip)))) 

Die repeat Kombinator hält die Taktik der Anwendung, bis es keine Änderung durchführt. Die Taktik split-clause schlägt fehl, wenn die Eingabe keine Klausel enthält. Deshalb verwenden wir einen or-else Kombinator mit der skip (nichts tun) Taktik. Wir können den Befehl verbessern, indem wir Taktiken verwenden, die Vereinfachungen anwenden (z. B. simplify, solve-eqs), nachdem jede Klausel in Fälle aufgeteilt wurde.

Beachten Sie, dass das obige Skript annimmt, dass die Eingabeformel in CNF ist.