¿Cómo convertir una fórmula a Disjunctive Normal Form?

Question

Mencione dado una fórmula

(t1> = 2 o t2> = 3) y (t3> = 1)

Deseo obtener su forma normal disyuntiva (t1> = 2 y t3> = 1) o (t2> = 3 y t3> = 1)

¿Cómo lograr esto en Z3?

Answer 1

Z3 no tiene una API o una táctica para convertir fórmulas en DNF. Sin embargo, tiene soporte para dividir un objetivo en muchos objetivos secundarios usando la táctica split-clause. Dada una fórmula de entrada en CNF, si aplicamos esta táctica exhaustivamente, cada subgoal de salida se puede ver como una gran conjunción. Aquí hay un ejemplo de cómo hacerlo.

http://rise4fun.com/Z3/zMjO

Este es el comando:

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

El combinador repeat mantiene la aplicación de la táctica hasta que no realiza ninguna modificación. La táctica split-clause falla si la entrada no tiene una cláusula. Es por eso que utilizamos un combinador or-else con la táctica skip (no hacer nada). Podemos mejorar el comando mediante el uso de tácticas que aplican simplificaciones (por ejemplo, simplify, solve-eqs) después de que cada cláusula se divide en casos.

Tenga en cuenta que, el script anterior asume que la fórmula de entrada está en CNF.