By default, a unique equivalent formula is computed (but its size might be exponential).
var a = new LVar("a")
var b = new LVar("b")
var c = new LVar("c")
var ex = a | (b & c)
assert ex.cnf.to_s == "(a|b) & (a|c)"
assert (~ex).cnf.to_s == "(~a) & (~b|~c)"If a parameter vars is given, an equisatisfiable formula is computed.
Additional variables, named zzsomething, are created by the transformation and stored in vars.
# Compute a conjunctive normal form.
#
# By default, a unique *equivalent* formula is computed (but its size might be exponential).
#
# ~~~
# var a = new LVar("a")
# var b = new LVar("b")
# var c = new LVar("c")
#
# var ex = a | (b & c)
# assert ex.cnf.to_s == "(a|b) & (a|c)"
# assert (~ex).cnf.to_s == "(~a) & (~b|~c)"
# ~~~
#
# If a parameter `vars` is given, an *equisatisfiable* formula is computed.
# Additional variables, named `zzsomething`, are created by the transformation and stored in `vars`.
fun cnf(vars: nullable Array[LVar]): CNF do
var ss = new CNF
var s = new Set[LExpr]
ss.data.add s
s.add self
return ss
end
lib/logic/lexpr.nit:181,2--203,4
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
lib/logic/lexpr.nit:242,2--271,4