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.
# 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