Compute a conjunctive normal form.

By default, a unique equivalent formula is computed (but its size might be exponential).

var a = new LVar("a")
var b = new LVar("b")
var c = new LVar("c")

var ex = a | (b & c)
assert ex.cnf.to_s == "(a|b) & (a|c)"
assert (~ex).cnf.to_s == "(~a) & (~b|~c)"

If a parameter vars is given, an equisatisfiable formula is computed. Additional variables, named zzsomething, are created by the transformation and stored in vars.

Property definitions

logic $ LExpr :: cnf
	# Compute a conjunctive normal form.
	#
	# By default, a unique *equivalent* formula is computed (but its size might be exponential).
	#
	# ~~~
	# var a = new LVar("a")
	# var b = new LVar("b")
	# var c = new LVar("c")
	#
	# var ex = a | (b & c)
	# assert ex.cnf.to_s == "(a|b) & (a|c)"
	# assert (~ex).cnf.to_s == "(~a) & (~b|~c)"
	# ~~~
	#
	# If a parameter `vars` is given, an *equisatisfiable* formula is computed.
	# Additional variables, named `zzsomething`, are created by the transformation and stored in `vars`.
	fun cnf(vars: nullable Array[LVar]): CNF do
		var ss = new CNF
		var s = new Set[LExpr]
		ss.data.add s
		s.add self
		return ss
	end
lib/logic/lexpr.nit:181,2--203,4

logic $ LAnd :: cnf
	redef fun cnf(v) do return e1.cnf(v) & e2.cnf(v)
lib/logic/lexpr.nit:223,2--49

logic $ LOr :: cnf
	redef fun cnf(v) do
		var c1 = e1.cnf(v)
		var c2 = e2.cnf(v)

		if c1.data.length > 1 and c2.data.length > 1 and v != null then
			var z = new LVar("zz{v.length}")
			v.add z
			var nz = ~z

			var res = new CNF
			for c in c1.data do
				var set = c.clone
				set.add z
				res.data.add(set)
			end
			for c in c2.data do
				var set = c.clone
				set.add nz
				res.data.add(set)
			end

			return res
		end

		var res = new CNF
		for i in c1.data do for j in c2.data do
			res.data.add i.union(j)
		end
		return res
	end
lib/logic/lexpr.nit:242,2--271,4

logic $ LNot :: cnf
	redef fun cnf(v) do
		if e isa LVar then return super
		return e.nnnf.cnf(v)
	end
lib/logic/lexpr.nit:287,2--290,4