# A conjunctive normal form of a logical expression.
class CNF
	# The conjunction of disjunction of units.
	var data = new Set[Set[LExpr]]

	# Simplify `self` by removing some useless clauses.
	#
	# * trivially clauses (with both a variable and its negation)
	# * subsumed clauses
	fun simplify: CNF
	do
		var cs2 = new Set[Set[LExpr]]

		# First pass to remove clauses with a variable and its negation.
		# These clauses become trivially `true`, thus useless in the conjunction.
		for c in data do
			for i in c do
				var nn = ~i
				if c.has(nn) then continue label
			end
			cs2.add c
		end label

		# Second pass to remove clauses subsumed by an other one.
		var cs3 = new Set[Set[LExpr]]
		for c in cs2 do
			for c2 in cs2 do
				if c2 != c and c2.has_all(c) then continue label
			end
			cs3.add c
		end label

		var res = new CNF
		res.data = cs3
		return res
	end

	# Merge two CNF
	fun &(o: CNF): CNF
	do
		var res = new CNF
		res.data.add_all self.data
		res.data.add_all o.data
		return res
	end

	redef fun to_s do return [for c in data do "(" + c.join("|") + ")"].join(" & ")

	redef fun ==(o) do return o isa CNF and data == o.data
	redef fun hash do return data.hash
end