let remove_redundant_conflicts deps confl =
let conj_deps p =
let f = PTbl.get deps p in
Formula.fold
(fun d s -> match Disj.to_lit d with Some p -> PSet.add p s | None -> s)
f PSet.empty
in
Conflict.iter confl
(fun p1 p2 ->
let d1 = conj_deps p1 in
let d2 = conj_deps p2 in
if
PSet.exists
(fun q1 ->
PSet.exists
(fun q2 ->
(p1 <> q1 || p2 <> q2) &&
(p1 <> q2 || p2 <> q1) &&
Conflict.check confl q1 q2)
d2)
d1
then begin
Conflict.remove confl p1 p2
end);
let try_remove_conflict p1 p2 =
let f1 = PTbl.get deps p1 in
let d2 = conj_deps p2 in
if
Formula.exists
(fun d1 ->
Disj.for_all
(fun q1 ->
PSet.exists
(fun q2 ->
(p1 <> q1 || p2 <> q2) &&
(p1 <> q2 || p2 <> q1) &&
Conflict.check confl q1 q2)
d2)
d1)
f1
then begin
Conflict.remove confl p1 p2
end
in
Conflict.iter confl try_remove_conflict;
Conflict.iter confl (fun p1 p2 -> try_remove_conflict p2 p1);
PTbl.map (simplify_formula confl) deps