The negative negation normal form (NNF).

This method is used to implement nnf. Basically, it returns the NNF of ~self.

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

Subclasses implements it by using De Morgan's laws to push negation inwards.

Property definitions

logic $ LExpr :: nnnf
	# The negative negation normal form (NNF).
	#
	# This method is used to implement `nnf`.
	# Basically, it returns the NNF of `~self`.
	#
	# ~~~
	# var a = new LVar("a")
	# var b = new LVar("b")
	# assert (a&b).nnnf.to_s == "(~a | ~b)"
	# ~~~
	#
	# Subclasses implements it by using De Morgan's laws to push negation inwards.
	fun nnnf: LExpr do return ~self
lib/logic/lexpr.nit:167,2--179,32

logic $ LAnd :: nnnf
	redef fun nnnf do return e1.nnnf | e2.nnnf
lib/logic/lexpr.nit:222,2--43

logic $ LOr :: nnnf
	redef fun nnnf do return e1.nnnf & e2.nnnf
lib/logic/lexpr.nit:240,2--43

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