logic :: LOr :: defaultinit
# 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
lib/logic/lexpr.nit:228,1--274,3