mirror of
https://github.com/Mercury-Language/mercury.git
synced 2026-04-15 17:33:38 +00:00
580 lines
19 KiB
Mathematica
580 lines
19 KiB
Mathematica
%---------------------------------------------------------------------------%
|
|
% vim: ft=mercury ts=4 sw=4 et
|
|
%---------------------------------------------------------------------------%
|
|
% Copyright (C) 2001-2006, 2010-2011 The University of Melbourne.
|
|
% Copyright (C) 2014-2015, 2019, 2021-2024 The Mercury team.
|
|
% This file may only be copied under the terms of the GNU Library General
|
|
% Public License - see the file COPYING.LIB in the Mercury distribution.
|
|
%---------------------------------------------------------------------------%
|
|
%
|
|
% File: mode_robdd.implications.m.
|
|
% Main author: dmo.
|
|
%
|
|
%---------------------------------------------------------------------------%
|
|
|
|
:- module mode_robdd.implications.
|
|
:- interface.
|
|
|
|
:- import_module bool.
|
|
:- import_module robdd.
|
|
:- import_module term.
|
|
|
|
%---------------------------------------------------------------------------%
|
|
|
|
:- func init_imp_vars = imp_vars(T).
|
|
|
|
:- func imp_vars(T) * imp_vars(T) = imp_vars(T).
|
|
|
|
:- func imp_vars(T) + imp_vars(T) = imp_vars(T).
|
|
|
|
:- func imp_vars(T) `difference` imp_vars(T) = imp_vars(T).
|
|
|
|
:- func imp_vars(T) `delete` var(T) = imp_vars(T).
|
|
|
|
:- func restrict_threshold(var(T), imp_vars(T)) = imp_vars(T).
|
|
|
|
:- func filter(pred(var(T)), imp_vars(T)) = imp_vars(T).
|
|
:- mode filter(in(pred(in) is semidet), in) = out is det.
|
|
|
|
:- func neq_vars(var(T), var(T), imp_vars(T)) = imp_vars(T).
|
|
|
|
:- func imp_vars(var(T), var(T), imp_vars(T)) = imp_vars(T).
|
|
|
|
:- func at_most_one_of(vars(T), imp_vars(T)) = imp_vars(T).
|
|
|
|
:- func not_both(var(T), var(T), imp_vars(T)) = imp_vars(T).
|
|
|
|
:- func either(var(T), var(T), imp_vars(T)) = imp_vars(T).
|
|
|
|
:- pred normalise_true_false_implication_vars(bool::out, vars(T)::in,
|
|
vars(T)::out, vars(T)::in, vars(T)::out,
|
|
imp_vars(T)::in, imp_vars(T)::out) is det.
|
|
|
|
:- pred propagate_equivalences_into_implications(equiv_vars(T)::in, bool::out,
|
|
imp_vars(T)::in, imp_vars(T)::out) is semidet.
|
|
|
|
:- pred propagate_implications_into_equivalences(bool::out, equiv_vars(T)::in,
|
|
equiv_vars(T)::out, imp_vars(T)::in, imp_vars(T)::out) is det.
|
|
|
|
:- pred extract_implication_vars_from_robdd(bool::out, robdd(T)::in,
|
|
robdd(T)::out, imp_vars(T)::in, imp_vars(T)::out) is det.
|
|
|
|
:- func add_equalities_to_imp_vars(equiv_vars(T), imp_vars(T)) = imp_vars(T).
|
|
|
|
%---------------------------------------------------------------------------%
|
|
%---------------------------------------------------------------------------%
|
|
|
|
:- implementation.
|
|
|
|
:- import_module mode_robdd.equiv_vars.
|
|
|
|
:- import_module assoc_list.
|
|
:- import_module io.
|
|
:- import_module list.
|
|
:- import_module map.
|
|
:- import_module pair.
|
|
:- import_module sparse_bitset.
|
|
:- import_module string.
|
|
|
|
%---------------------------------------------------------------------------%
|
|
|
|
init_imp_vars = imp_vars(init, init, init, init).
|
|
|
|
ImpVars * imp_vars(Imps, RevImps, DisImps, RevDisImps) =
|
|
ImpVars ^ add_imp_map_clauses(mkneg, mkpos, Imps)
|
|
^ add_imp_map_clauses(mkpos, mkneg, RevImps)
|
|
^ add_imp_map_clauses(mkneg, mkneg, DisImps)
|
|
^ add_imp_map_clauses(mkpos, mkpos, RevDisImps).
|
|
|
|
ImpVarsA + ImpVarsB =
|
|
apply_to_coresp_imp_maps(intersect, ImpVarsA, ImpVarsB).
|
|
|
|
ImpVarsA `difference` ImpVarsB =
|
|
apply_to_coresp_imp_maps(imp_map_difference, ImpVarsA, ImpVarsB).
|
|
|
|
ImpVars `delete` Var =
|
|
apply_to_imp_maps(delete_var_from_imp_map(Var), ImpVars).
|
|
% XXX could make this more efficient by using backwards relations.
|
|
|
|
restrict_threshold(Threshold, ImpVars) =
|
|
apply_to_imp_maps(func(IM) =
|
|
restrict_threshold_2(Threshold, to_assoc_list(IM), init),
|
|
ImpVars).
|
|
|
|
:- func restrict_threshold_2(var(T), assoc_list(var(T), vars(T)), imp_map(T))
|
|
= imp_map(T).
|
|
|
|
restrict_threshold_2(_Threshold, [], IM) = IM.
|
|
restrict_threshold_2(Threshold, [V - Vs | AL], IM) =
|
|
( if compare((>), V, Threshold) then
|
|
IM
|
|
else
|
|
restrict_threshold_2(Threshold, AL,
|
|
IM ^ entry(V) := remove_gt(Vs, Threshold))
|
|
).
|
|
|
|
filter(P, ImpVars) = apply_to_imp_maps(filter_imp_map(P), ImpVars).
|
|
|
|
:- func filter_imp_map(pred(var(T)), imp_map(T)) = imp_map(T).
|
|
:- mode filter_imp_map(in(pred(in) is semidet), in) = out is det.
|
|
|
|
filter_imp_map(P, IM) =
|
|
map.foldl(func(V, Vs, M) =
|
|
( if P(V) then
|
|
M ^ entry(V) := filter(P, Vs)
|
|
else
|
|
M `delete` V
|
|
),
|
|
IM, IM).
|
|
|
|
neq_vars(A, B, ImpVars) =
|
|
ImpVars ^ add_robdd_clause({neg(A), neg(B)}) ^
|
|
add_robdd_clause({pos(A), pos(B)}).
|
|
|
|
imp_vars(A, B, ImpVars) =
|
|
ImpVars ^ add_robdd_clause({neg(A), pos(B)}).
|
|
|
|
at_most_one_of(Vars0, ImpVars) =
|
|
( if remove_least(Var, Vars0, Vars) then
|
|
ImpVars ^ foldl(not_both(Var), Vars) ^ at_most_one_of(Vars)
|
|
else
|
|
ImpVars
|
|
).
|
|
|
|
not_both(A, B, ImpVars) =
|
|
ImpVars ^ add_robdd_clause({neg(A), neg(B)}).
|
|
|
|
either(A, B, ImpVars) =
|
|
ImpVars ^ add_robdd_clause({pos(A), pos(B)}).
|
|
|
|
normalise_true_false_implication_vars(Changed, TrueVars0, TrueVars,
|
|
FalseVars0, FalseVars, ImpVars0, ImpVars) :-
|
|
( if
|
|
is_empty(TrueVars0),
|
|
is_empty(FalseVars0)
|
|
then
|
|
TrueVars = TrueVars0,
|
|
FalseVars = FalseVars0,
|
|
ImpVars = ImpVars0,
|
|
Changed = no
|
|
else
|
|
ImpVars0 = imp_vars(Imps0, RevImps0, DisImps0, RevDisImps0),
|
|
normalise_true_false_imp_map(no, Changed0, TrueVars0, TrueVars1,
|
|
FalseVars0, FalseVars1, Imps0, Imps),
|
|
normalise_true_false_imp_map(no, Changed1, FalseVars1, FalseVars2,
|
|
TrueVars1, TrueVars2, RevImps0, RevImps),
|
|
normalise_true_false_imp_map(yes, Changed2, FalseVars2, FalseVars3,
|
|
TrueVars2, TrueVars3, DisImps0, DisImps),
|
|
normalise_true_false_imp_map(yes, Changed3, TrueVars3, TrueVars4,
|
|
FalseVars3, FalseVars4, RevDisImps0, RevDisImps),
|
|
|
|
normalise_pairs(keys, Imps, DisImps, Changed4,
|
|
FalseVars4, FalseVars5),
|
|
normalise_pairs(keys, RevImps, RevDisImps, Changed5,
|
|
TrueVars4, TrueVars5),
|
|
normalise_pairs(values, RevImps, DisImps, Changed6,
|
|
FalseVars5, FalseVars6),
|
|
normalise_pairs(values, Imps, RevDisImps, Changed7,
|
|
TrueVars5, TrueVars6),
|
|
|
|
ImpVars6 = imp_vars(Imps, RevImps, DisImps, RevDisImps),
|
|
Changed = (Changed0 or Changed1 or Changed2 or Changed3 or
|
|
Changed4 or Changed5 or Changed6 or Changed7),
|
|
(
|
|
Changed = yes,
|
|
normalise_true_false_implication_vars(_, TrueVars6, TrueVars,
|
|
FalseVars6, FalseVars, ImpVars6, ImpVars)
|
|
;
|
|
Changed = no,
|
|
TrueVars = TrueVars6,
|
|
FalseVars = FalseVars6,
|
|
ImpVars = ImpVars6
|
|
)
|
|
).
|
|
|
|
:- pred normalise_true_false_imp_map(bool::in, bool::out,
|
|
vars(T)::in, vars(T)::out, vars(T)::in, vars(T)::out,
|
|
imp_map(T)::in, imp_map(T)::out) is det.
|
|
|
|
normalise_true_false_imp_map(IsDisImp, Changed, TrueVars0, TrueVars,
|
|
FalseVars0, FalseVars, ImpMap0, ImpMap) :-
|
|
{TrueVars, FalseVars, ImpMap, Changed} = map.foldl(
|
|
( func(V, Vs, {Ts0, Fs0, IMs0, C0}) = {Ts, Fs, IMs, C} :-
|
|
( if
|
|
( if IsDisImp = yes then Fs0 else Ts0 ) `contains` V
|
|
then
|
|
Ts = Ts0 `union` Vs,
|
|
Fs = Fs0,
|
|
IMs = IMs0 `delete` V,
|
|
C = yes
|
|
else if
|
|
( if IsDisImp = yes then Ts0 else Fs0 ) `contains` V
|
|
then
|
|
Ts = Ts0,
|
|
Fs = Fs0,
|
|
IMs = IMs0 `delete` V,
|
|
C = yes
|
|
else if
|
|
FVs = Fs0 `intersect` Vs,
|
|
is_non_empty(FVs)
|
|
then
|
|
Ts = ( if IsDisImp = yes then Ts0 `insert` V else Ts0 ),
|
|
Fs = ( if IsDisImp = yes then Fs0 else Fs0 `insert` V ),
|
|
IMs = IMs0 `delete` V,
|
|
C = yes
|
|
else if
|
|
TVs = Ts0 `intersect` Vs,
|
|
is_non_empty(TVs)
|
|
then
|
|
Ts = Ts0,
|
|
Fs = Fs0,
|
|
UTVs = Vs `difference` TVs,
|
|
( if is_empty(UTVs) then
|
|
IMs = IMs0 `delete` V
|
|
else
|
|
IMs = IMs0 ^ elem(V) := UTVs
|
|
),
|
|
C = yes
|
|
else
|
|
Ts = Ts0,
|
|
Fs = Fs0,
|
|
IMs = IMs0,
|
|
C = C0
|
|
)
|
|
), ImpMap0, {TrueVars0, FalseVars0, ImpMap0, no}).
|
|
|
|
:- type extract ---> keys ; values.
|
|
|
|
:- pred normalise_pairs(extract::in, imp_map(T)::in, imp_map(T)::in, bool::out,
|
|
vars(T)::in, vars(T)::out) is det.
|
|
|
|
normalise_pairs(Extract, Imps, DisImps, Changed, FalseVars0, FalseVars) :-
|
|
Intersect = Imps `intersect` DisImps,
|
|
( if is_empty(Intersect) then
|
|
Changed = no,
|
|
FalseVars = FalseVars0
|
|
else
|
|
Changed = yes,
|
|
(
|
|
Extract = keys,
|
|
FalseVars = FalseVars0 `union`
|
|
Intersect ^ sorted_keys ^ sorted_list_to_set
|
|
;
|
|
Extract = values,
|
|
Values = list.foldl(union, Intersect ^ values, init),
|
|
FalseVars = FalseVars0 `union` Values
|
|
)
|
|
).
|
|
|
|
%------------------------------------------------------------------------%
|
|
|
|
propagate_equivalences_into_implications(EQVars, Changed, ImpVars0, ImpVars) :-
|
|
ImpVars0 = imp_vars(Imps0, RevImps0, DisImps, RevDisImps),
|
|
|
|
propagate_equivalences_into_disimplications(EQVars, DisImps,
|
|
RevDisImps),
|
|
|
|
propagate_equivalences_into_implications_2(EQVars, Changed0,
|
|
Imps0, Imps),
|
|
propagate_equivalences_into_implications_2(EQVars, Changed1,
|
|
RevImps0, RevImps),
|
|
|
|
ImpVars = imp_vars(Imps, RevImps, DisImps, RevDisImps),
|
|
Changed = Changed0 `bool.or` Changed1.
|
|
|
|
:- pred propagate_equivalences_into_implications_2(equiv_vars(T)::in,
|
|
bool::out, imp_map(T)::in, imp_map(T)::out) is det.
|
|
|
|
propagate_equivalences_into_implications_2(EQVars, Changed, ImpMap0, ImpMap) :-
|
|
{ImpMap, Changed} = map.foldl((func(V, Vs0, {IM, C}) =
|
|
{ IM ^ entry(V) := Vs, ( if Vs = Vs0 then C else yes ) } :-
|
|
Vs = filter(vars_are_not_equivalent(EQVars, V), Vs0)
|
|
), ImpMap0, {init, no}).
|
|
|
|
:- pred propagate_equivalences_into_disimplications(equiv_vars(T)::in,
|
|
imp_map(T)::in, imp_map(T)::in) is semidet.
|
|
|
|
propagate_equivalences_into_disimplications(EQVars, DisImps, RevDisImps) :-
|
|
ImpMap = DisImps `intersect` RevDisImps,
|
|
( all [VA, VB]
|
|
% XXX this could be very slow. May want to do it more
|
|
% efficiently.
|
|
( member(ImpMap, VA, Vs), member(VB, Vs) )
|
|
=>
|
|
vars_are_not_equivalent(EQVars, VA, VB)
|
|
).
|
|
|
|
%------------------------------------------------------------------------%
|
|
|
|
% Look for occurrences of A => B and A <= B and replace then by A <=> B.
|
|
propagate_implications_into_equivalences(Changed, EQVars0, EQVars,
|
|
ImpVars0, ImpVars) :-
|
|
ImpVars0 = imp_vars(Imps0, RevImps0, DisImps, RevDisImps),
|
|
|
|
( if ( is_empty(Imps0) ; is_empty(RevImps0) ) then
|
|
Changed = no,
|
|
EQVars = EQVars0,
|
|
ImpVars = ImpVars0
|
|
else
|
|
{Changed, EQVars, Imps, RevImps} = foldl(
|
|
( func(V, IVs, {C0, E0, I0, R0}) = {C, E, I, R} :-
|
|
( if
|
|
map.search(R0, V, RVs),
|
|
EVs = IVs `intersect` RVs,
|
|
is_non_empty(EVs)
|
|
then
|
|
C = yes,
|
|
E = add_equalities(EVs `insert` V, E0),
|
|
I = I0 ^ entry(V) := IVs `difference` RVs,
|
|
R = R0 ^ entry(V) := RVs `difference` IVs
|
|
else
|
|
C = C0, E = E0, I = I0, R = R0
|
|
)
|
|
), Imps0, {no, EQVars0, Imps0, RevImps0}),
|
|
ImpVars = imp_vars(Imps, RevImps, DisImps, RevDisImps)
|
|
).
|
|
|
|
%------------------------------------------------------------------------%
|
|
|
|
extract_implication_vars_from_robdd(Changed, Robdd0, Robdd,
|
|
ImpVars0, ImpVars) :-
|
|
% ImpVars1 = add_backwards_relations(extract_implications(Robdd0)),
|
|
ImpVars1 = extract_implications(Robdd0),
|
|
ImpVars = ImpVars0 * ImpVars1,
|
|
|
|
Robdd = remove_implications(ImpVars, Robdd0),
|
|
|
|
trace [compile_time(flag("debug_mode_implications")), io(!IO)] (
|
|
VarToString = (func(V) = string.int_to_string(var_to_int(V))),
|
|
robdd_to_dot(Robdd0, VarToString, "extract_impl_before.dot", !IO),
|
|
robdd_to_dot(Robdd, VarToString, "extract_impl_after.dot", !IO)
|
|
),
|
|
|
|
Changed = ( if Robdd = Robdd0, empty(ImpVars1) then no else yes ).
|
|
|
|
%------------------------------------------------------------------------%
|
|
|
|
add_equalities_to_imp_vars(EQVars, ImpVars) =
|
|
map.foldl(func(VA, VB, IVs) =
|
|
IVs ^ imp_vars(VA, VB) ^ imp_vars(VB, VA),
|
|
EQVars ^ leader_map, ImpVars).
|
|
|
|
%------------------------------------------------------------------------%
|
|
|
|
:- func entry(var(T), imp_map(T)) = vars(T).
|
|
|
|
entry(V, M) =
|
|
( if map.search(M, V, Vs) then
|
|
Vs
|
|
else
|
|
init
|
|
).
|
|
|
|
:- func 'entry :='(var(T), imp_map(T), vars(T)) = imp_map(T).
|
|
|
|
'entry :='(V, M, Vs) =
|
|
( if is_empty(Vs) then
|
|
M `delete` V
|
|
else
|
|
M ^ elem(V) := Vs
|
|
).
|
|
|
|
:- func 'new_relation :='(var(T), imp_map(T), var(T)) = imp_map(T).
|
|
|
|
'new_relation :='(VA, M, VB) =
|
|
( if map.search(M, VA, Vs) then
|
|
M ^ elem(VA) := Vs `insert` VB
|
|
else
|
|
M ^ elem(VA) := make_singleton_set(VB)
|
|
).
|
|
|
|
:- func 'maybe_new_relation :='(var(T), imp_map(T), var(T)) = imp_map(T)
|
|
is semidet.
|
|
|
|
'maybe_new_relation :='(VA, M0, VB) = M :-
|
|
( if map.search(M0, VA, Vs) then
|
|
\+ ( Vs `contains` VB ),
|
|
M = M0 ^ elem(VA) := Vs `insert` VB
|
|
else
|
|
M = M0 ^ elem(VA) := make_singleton_set(VB)
|
|
).
|
|
|
|
:- pred empty(imp_vars(T)::in) is semidet.
|
|
|
|
empty(imp_vars(I, RI, DI, RDI)) :-
|
|
is_empty(I),
|
|
is_empty(RI),
|
|
is_empty(DI),
|
|
is_empty(RDI).
|
|
|
|
%------------------------------------------------------------------------%
|
|
|
|
:- func apply_to_imp_maps(func(imp_map(T)) = imp_map(T), imp_vars(T)) =
|
|
imp_vars(T).
|
|
|
|
apply_to_imp_maps(F, ImpVars0) = ImpVars :-
|
|
ImpVars0 = imp_vars(I, RI, DI, RDI),
|
|
ImpVars = imp_vars(F(I), F(RI), F(DI), F(RDI)).
|
|
|
|
:- func apply_to_coresp_imp_maps(func(imp_map(T), imp_map(T)) = imp_map(T),
|
|
imp_vars(T), imp_vars(T)) = imp_vars(T).
|
|
|
|
apply_to_coresp_imp_maps(F, ImpVarsA, ImpVarsB) = ImpVars :-
|
|
ImpVarsA = imp_vars(IA, RIA, DIA, RDIA),
|
|
ImpVarsB = imp_vars(IB, RIB, DIB, RDIB),
|
|
ImpVars = imp_vars(F(IA, IB), F(RIA, RIB), F(DIA, DIB), F(RDIA, RDIB)).
|
|
|
|
:- func imp_map(T) `intersect` imp_map(T) = imp_map(T).
|
|
|
|
IMA `intersect` IMB = remove_empty_sets(intersect(intersect, IMA, IMB)).
|
|
|
|
:- func imp_map(T) `imp_map_difference` imp_map(T) = imp_map(T).
|
|
|
|
IMA `imp_map_difference` IMB =
|
|
( if is_empty(IMA) then
|
|
IMA
|
|
else
|
|
map.foldl(func(V, VsB, M) =
|
|
( if map.search(M, V, VsA) then
|
|
M ^ entry(V) := VsA `difference` VsB
|
|
else
|
|
M
|
|
),
|
|
IMB, IMA)
|
|
).
|
|
|
|
:- func remove_empty_sets(imp_map(T)) = imp_map(T).
|
|
|
|
remove_empty_sets(IM) =
|
|
map.foldl(func(V, Vs, M) =
|
|
( if is_empty(Vs) then
|
|
M `delete` V
|
|
else
|
|
M
|
|
),
|
|
IM, IM).
|
|
|
|
:- func delete_var_from_imp_map(var(T), imp_map(T)) = imp_map(T).
|
|
|
|
delete_var_from_imp_map(Var, IM0) =
|
|
map.foldl(func(V, Vs, M) =
|
|
( if Vs `contains` Var then
|
|
M ^ entry(V) := Vs `delete` Var
|
|
else
|
|
M
|
|
),
|
|
IM1, IM1) :-
|
|
IM1 = IM0 `delete` Var.
|
|
|
|
%------------------------------------------------------------------------%
|
|
|
|
:- func add_backwards_relations(imp_vars(T)) = imp_vars(T).
|
|
:- pragma consider_used(func(add_backwards_relations/1)).
|
|
|
|
add_backwards_relations(imp_vars(Is0, RIs0, DIs0, RDIs0)) =
|
|
imp_vars(
|
|
add_backwards_to_imp_map(Is0, RIs0),
|
|
add_backwards_to_imp_map(RIs0, Is0),
|
|
add_backwards_to_imp_map(DIs0, DIs0),
|
|
add_backwards_to_imp_map(RDIs0, RDIs0)
|
|
).
|
|
|
|
:- func add_backwards_to_imp_map(imp_map(T), imp_map(T)) = imp_map(T).
|
|
|
|
add_backwards_to_imp_map(IM, RIM) =
|
|
map.foldl(func(VA, Vs, M0) =
|
|
foldl(func(VB, M1) =
|
|
M1 ^ new_relation(VB) := VA,
|
|
Vs, M0),
|
|
RIM, IM).
|
|
|
|
%------------------------------------------------------------------------%
|
|
|
|
:- type mklit(T) == (func(var(T)) = literal(T)).
|
|
|
|
:- func mkpos(var(T)) = literal(T).
|
|
|
|
mkpos(V) = pos(V).
|
|
|
|
:- func mkneg(var(T)) = literal(T).
|
|
|
|
mkneg(V) = neg(V).
|
|
|
|
:- type bin_clause(T) == { literal(T), literal(T) }.
|
|
|
|
:- func add_robdd_clause(bin_clause(T), imp_vars(T)) = imp_vars(T).
|
|
|
|
add_robdd_clause(Clause, ImpVars) =
|
|
add_robdd_clauses([Clause], ImpVars).
|
|
|
|
:- func add_robdd_clauses(list(bin_clause(T)), imp_vars(T)) = imp_vars(T).
|
|
|
|
add_robdd_clauses([], ImpVars) = ImpVars.
|
|
add_robdd_clauses([Clause | Clauses], ImpVars0) = ImpVars :-
|
|
( if ImpVars1 = add_robdd_clause_2(Clause, ImpVars0) then
|
|
Resolvents = get_resolvents(Clause, ImpVars1),
|
|
ImpVars = add_robdd_clauses(Resolvents ++ Clauses, ImpVars1)
|
|
else
|
|
ImpVars = add_robdd_clauses(Clauses, ImpVars0)
|
|
).
|
|
|
|
% Add a new clause to the imp_vars. Fail if the clause is already present.
|
|
%
|
|
:- func add_robdd_clause_2(bin_clause(T), imp_vars(T)) = imp_vars(T)
|
|
is semidet.
|
|
|
|
add_robdd_clause_2({neg(VA), pos(VB)}, ImpVars) =
|
|
(ImpVars ^ imps ^ maybe_new_relation(VA) := VB)
|
|
^ rev_imps ^ maybe_new_relation(VB) := VA.
|
|
add_robdd_clause_2({pos(VA), neg(VB)}, ImpVars) =
|
|
(ImpVars ^ rev_imps ^ maybe_new_relation(VA) := VB)
|
|
^ imps ^ maybe_new_relation(VB) := VA.
|
|
add_robdd_clause_2({neg(VA), neg(VB)}, ImpVars) =
|
|
(ImpVars ^ dis_imps ^ maybe_new_relation(VA) := VB)
|
|
^ dis_imps ^ maybe_new_relation(VB) := VA.
|
|
add_robdd_clause_2({pos(VA), pos(VB)}, ImpVars) =
|
|
(ImpVars ^ rev_dis_imps ^ maybe_new_relation(VA) := VB)
|
|
^ rev_dis_imps ^ maybe_new_relation(VB) := VA.
|
|
|
|
:- func get_resolvents(bin_clause(T), imp_vars(T)) = list(bin_clause(T)).
|
|
|
|
get_resolvents({LitA, LitB}, ImpVars) =
|
|
get_resolvents_2(LitA, LitB, ImpVars) ++
|
|
get_resolvents_2(LitB, LitA, ImpVars).
|
|
|
|
:- func get_resolvents_2(literal(T), literal(T), imp_vars(T)) =
|
|
list(bin_clause(T)).
|
|
|
|
get_resolvents_2(LitA, LitB, ImpVars) = Clauses :-
|
|
Literals = get_literals(LitA, ImpVars),
|
|
Clauses = list.map(func(NewLit) = {NewLit, LitB}, Literals).
|
|
|
|
:- func get_literals(literal(T), imp_vars(T)) = list(literal(T)).
|
|
|
|
get_literals(LitA, ImpVars) =
|
|
map(mkpos, to_sorted_list(Pos)) ++
|
|
map(mkneg, to_sorted_list(Neg)) :-
|
|
(
|
|
LitA = pos(VarA),
|
|
Pos = ImpVars ^ imps ^ entry(VarA),
|
|
Neg = ImpVars ^ dis_imps ^ entry(VarA)
|
|
;
|
|
LitA = neg(VarA),
|
|
Pos = ImpVars ^ rev_dis_imps ^ entry(VarA),
|
|
Neg = ImpVars ^ rev_imps ^ entry(VarA)
|
|
).
|
|
|
|
:- func add_imp_map_clauses(mklit(T), mklit(T), imp_map(T), imp_vars(T)) =
|
|
imp_vars(T).
|
|
|
|
add_imp_map_clauses(MkLitA, MkLitB, IM, ImpVars) =
|
|
map.foldl(func(VarA, Vars, IVs0) =
|
|
foldl(func(VarB, IVs1) =
|
|
add_robdd_clause({MkLitA(VarA), MkLitB(VarB)}, IVs1),
|
|
Vars, IVs0),
|
|
IM, ImpVars).
|
|
|
|
%---------------------------------------------------------------------------%
|
|
:- end_module mode_robdd.implications.
|
|
%---------------------------------------------------------------------------%
|