# 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
lib/logic/lexpr.nit:334,2--364,4