# A logical disjunction operation
class LOr
	super LExpr

	# The first operand
	var e1: LExpr

	# The second operand
	var e2: LExpr

	redef fun to_s do return "({e1} | {e2})"
	redef fun nnf do return e1.nnf | e2.nnf
	redef fun nnnf do return e1.nnnf & e2.nnnf

	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

	redef fun size do return e1.size + e2.size + 1
end