Jak przekonwertować formułę na Disjunctive Normal Form?

Question

Say podany wzór

(T1> = 2 lub T2> = 3) i (t3> = 1)

życzę aby jego rozłącznego postaci normalnej (T1> = 2 i T3> = 1) lub (t2> = 3 i t3> = 1)

Jak to osiągnąć w Z3?

Answer 1

Z3 nie ma interfejsu API ani taktyki do konwertowania formuł na DNF. Jednak ma wsparcie dla zrzucenia celu na wiele obiektów podrzędnych za pomocą taktyki split-clause. Biorąc pod uwagę formułę wejściową w CNF, jeśli zastosujemy tę taktykę w sposób wyczerpujący, każde wyjście może być postrzegane jako duża koniunkcja. Oto przykład, jak to zrobić.

http://rise4fun.com/Z3/zMjO

Oto polecenie:

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

repeat syntezatora utrzymuje stosując taktykę, dopóki nie wykonywać żadnych modyfikacji. Taktyka split-clause nie powiedzie się, jeśli wejście nie zawiera klauzuli. Dlatego używamy kombinatora or-else z taktyką skip (nic nie rób). Możemy ulepszyć polecenie, stosując taktykę, która stosuje uproszczenia (np. simplify, solve-eqs) po podzieleniu każdej klauzuli na przypadki.

Należy zauważyć, że powyższy skrypt zakłada, że ​​formuła wejściowa znajduje się w CNF.