logic :: CNF :: defaultinit
core :: Object :: class_factory
Implementation used byget_class
to create the specific class.
core :: Object :: defaultinit
logic :: CNF :: defaultinit
core :: Object :: is_same_instance
Return true ifself
and other
are the same instance (i.e. same identity).
core :: Object :: is_same_serialized
Isself
the same as other
in a serialization context?
core :: Object :: is_same_type
Return true ifself
and other
have the same dynamic type.
core :: Object :: output_class_name
Display class name on stdout (debug only).
# 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