The negation normal form (NNF).

In NNF, the negation operator is only applied to variables.

var a = new LVar("a")
var b = new LVar("b")
assert (a&b).nnf.to_s == "(a & b)"
assert (~(a&b)).nnf.to_s == "(~a | ~b)"

Subclasses implement it recursively.

Property definitions

logic $ LExpr :: nnf
	# The negation normal form (NNF).
	#
	# In NNF, the negation operator is only applied to variables.
	#
	# ~~~
	# var a = new LVar("a")
	# var b = new LVar("b")
	# assert (a&b).nnf.to_s == "(a & b)"
	# assert (~(a&b)).nnf.to_s == "(~a | ~b)"
	# ~~~
	#
	# Subclasses implement it recursively.
	fun nnf: LExpr do return self
lib/logic/lexpr.nit:153,2--165,30

logic $ LAnd :: nnf
	redef fun nnf do return e1.nnf & e2.nnf
lib/logic/lexpr.nit:221,2--40

logic $ LOr :: nnf
	redef fun nnf do return e1.nnf | e2.nnf
lib/logic/lexpr.nit:239,2--40

logic $ LNot :: nnf
	redef fun nnf do return e.nnnf
lib/logic/lexpr.nit:285,2--31