let rec flatten_deps tbl deps conflicts visited l =
Formula.fold
(fun d (l, r) ->
let (l', r') =
Disj.fold
(fun i (l, r) ->
let (l', r') = flatten_dep tbl deps conflicts visited i in
(Formula.disj l' l, PSet.union r r')) d (Formula._false, r)
in
(Formula.conj l' l, r'))
l (Formula._true, PSet.empty)
and flatten_dep tbl deps conflicts visited i =
try
(Hashtbl.find tbl i, PSet.empty)
with Not_found ->
let res =
if List.mem i visited then
(Formula._true, PSet.singleton i)
else begin
let (l, r) =
flatten_deps tbl deps conflicts (i :: visited) (PTbl.get deps i)
in
let l = simplify_formula conflicts l in
let r = PSet.remove i r in
if Conflict.has conflicts i then
(Formula.conj (Formula.lit i) l, r)
else
(l, r)
end
in
if PSet.is_empty (snd res) then Hashtbl.add tbl i (fst res);
res