'z3py: How to convert a formula into NNF format?

I wanted to convert a formula to its NNF format using z3py. For e.g.,

Given

Or(Not(And(i1, Not(And(i0, i4, i1, i2)))), And(i3, i1, i2))

I want

Or(Not(i1), And(i0, i4, i1, i2), And(i3, i1, i2))

Thanks

z3pynegation


Solution 1:[1]

You can use the nnf tactic, followed by simplify:

from z3 import *

i0, i1, i2, i3, i4 = Bools("i0 i1 i2 i3 i4")
g = Goal()
g.add(Or(Not(And(i1, Not(And(i0, i4, i1, i2)))), And(i3, i1, i2)))
print(g)
t = Then(Tactic('nnf'), Tactic('simplify'))
print(t(g))

This prints:

[Or(Not(And(i1, Not(And(i0, i4, i1, i2)))), And(i3, i1, i2))]
[[Or(And(i0, i4, i1, i2), And(i3, i1, i2), Not(i1))]]

the result is a list of goals; but a singleton goal is the same as your formula. (A goal can split a formula into many parts, and hence the list output.)

Sources

This article follows the attribution requirements of Stack Overflow and is licensed under CC BY-SA 3.0.

Source: Stack Overflow

Solution Source
Solution 1 alias

Related Questions