logic :: CNF :: defaultinit
# 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
lib/logic/lexpr.nit:329,1--379,3