[m-rev.] diff/for review: constraint based mode analysis (part 1)
Zoltan Somogyi
zs at cs.mu.OZ.AU
Thu Dec 16 13:53:19 AEDT 2004
Index: compiler/mode_robdd.check.m
===================================================================
RCS file: compiler/mode_robdd.check.m
diff -N compiler/mode_robdd.check.m
--- /dev/null 1 Jan 1970 00:00:00 -0000
+++ compiler/mode_robdd.check.m 6 May 2003 04:18:46 -0000
@@ -0,0 +1,294 @@
+%---------------------------------------------------------------------------%
+% Copyright (C) 2001-2003 The University of Melbourne.
+% 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_robbd.check.m.
+% Main author: dmo
+% Stability: low
+
+% This module implements every one of its operations on two robdds,
+% compares their results, and reports an error if they differ. This makes
+% it easier to debug a new, potantially faster mode_robdd implementation
+% by comparing its operation to the operation of an existing, trusted
+% implementation.
+
+%-----------------------------------------------------------------------------%
+%-----------------------------------------------------------------------------%
+
+:- module mode_robdd__check.
+
+:- interface.
+
+:- import_module mode_robdd__tfeirn.
+:- import_module term, robdd.
+
+:- type check_robdd(T).
+:- type check_robdd == check_robdd(generic).
+
+:- inst check_robdd == ground. % XXX the robdd parts should be unique
+
+:- mode di_check_robdd == in. % XXX the robdd parts should be di
+:- mode uo_check_robdd == out. % XXX the robdd parts should be uo
+
+:- inst norm_check_robdd ---> mode_robdd(ground, norm_tfeirn).
+:- mode ni_check_robdd == in(norm_check_robdd).
+:- mode no_check_robdd == out(norm_check_robdd).
+
+% Constants.
+:- func one = check_robdd(T).
+:- func zero = check_robdd(T).
+
+% Conjunction.
+:- func check_robdd(T) * check_robdd(T) = check_robdd(T).
+
+% Disjunction.
+:- func check_robdd(T) + check_robdd(T) = check_robdd(T).
+
+%-----------------------------------------------------------------------------%
+
+:- func var(var(T)::in, check_robdd(T)::in(check_robdd)) =
+ (check_robdd(T)::out(check_robdd)) is det.
+
+:- func not_var(var(T)::in, check_robdd(T)::in(check_robdd)) =
+ (check_robdd(T)::out(check_robdd)) is det.
+
+:- func eq_vars(var(T)::in, var(T)::in, check_robdd(T)::di_check_robdd) =
+ (check_robdd(T)::uo_check_robdd) is det.
+
+:- func neq_vars(var(T)::in, var(T)::in, check_robdd(T)::di_check_robdd) =
+ (check_robdd(T)::uo_check_robdd) is det.
+
+:- func imp_vars(var(T)::in, var(T)::in, check_robdd(T)::di_check_robdd) =
+ (check_robdd(T)::uo_check_robdd) is det.
+
+:- func conj_vars(vars(T)::in, check_robdd(T)::di_check_robdd) =
+ (check_robdd(T)::uo_check_robdd) is det.
+
+:- func conj_not_vars(vars(T)::in, check_robdd(T)::di_check_robdd) =
+ (check_robdd(T)::uo_check_robdd) is det.
+
+:- func disj_vars(vars(T)::in, check_robdd(T)::di_check_robdd) =
+ (check_robdd(T)::uo_check_robdd) is det.
+
+:- func at_most_one_of(vars(T)::in, check_robdd(T)::di_check_robdd) =
+ (check_robdd(T)::uo_check_robdd) is det.
+
+:- func not_both(var(T)::in, var(T)::in, check_robdd(T)::di_check_robdd) =
+ (check_robdd(T)::uo_check_robdd) is det.
+
+:- func io_constraint(var(T)::in, var(T)::in, var(T)::in,
+
+check_robdd(T)::di_check_robdd)
+ = (check_robdd(T)::uo_check_robdd) is det.
+
+ % disj_vars_eq(Vars, Var) <=> (disj_vars(Vars) =:= Var).
+:- func disj_vars_eq(vars(T)::in, var(T)::in, check_robdd(T)::di_check_robdd) =
+ (check_robdd(T)::uo_check_robdd) is det.
+
+:- func var_restrict_true(var(T)::in, check_robdd(T)::di_check_robdd) =
+ (check_robdd(T)::uo_check_robdd) is det.
+
+:- func var_restrict_false(var(T)::in, check_robdd(T)::di_check_robdd) =
+ (check_robdd(T)::uo_check_robdd) is det.
+
+%-----------------------------------------------------------------------------%
+
+ % Succeed iff the var is entailed by the mode_robdd.
+:- pred var_entailed(check_robdd(T)::ni_check_robdd, var(T)::in) is semidet.
+
+ % Return the set of vars entailed by the mode_robdd.
+:- func vars_entailed(check_robdd(T)::ni_check_robdd) =
+ (vars_entailed_result(T)::out) is det.
+
+% Return the set of vars disentailed by the mode_robdd.
+:- func vars_disentailed(check_robdd(T)::ni_check_robdd) =
+ (vars_entailed_result(T)::out) is det.
+
+% Existentially quantify away the var in the mode_robdd.
+:- func restrict(var(T)::in, check_robdd(T)::ni_check_robdd) =
+ (check_robdd(T)::no_check_robdd) is det.
+
+% Existentially quantify away all vars greater than the specified var.
+:- func restrict_threshold(var(T)::in, check_robdd(T)::ni_check_robdd) =
+ (check_robdd(T)::no_check_robdd) is det.
+
+:- func restrict_filter(pred(var(T))::(pred(in) is semidet),
+ check_robdd(T)::ni_check_robdd) =
+ (check_robdd(T)::no_check_robdd) is det.
+
+%-----------------------------------------------------------------------------%
+
+ % labelling(Vars, ModeRobdd, TrueVars, FalseVars)
+ % Takes a set of Vars and an ModeRobdd and returns a value
+ % assignment for those Vars that is a model of the
+ % Boolean function represented by the ModeRobdd.
+ % The value assignment is returned in the two sets TrueVars (set
+ % of variables assigned the value 1) and FalseVars (set of
+ % variables assigned the value 0).
+ %
+ % XXX should try using sparse_bitset here.
+:- pred labelling(vars(T)::in, check_robdd(T)::in, vars(T)::out, vars(T)::out)
+ is nondet.
+
+ % minimal_model(Vars, ModeRobdd, TrueVars, FalseVars)
+ % Takes a set of Vars and an ModeRobdd and returns a value
+ % assignment for those Vars that is a minimal model of the
+ % Boolean function represented by the ModeRobdd.
+ % The value assignment is returned in the two sets TrueVars (set
+ % of variables assigned the value 1) and FalseVars (set of
+ % variables assigned the value 0).
+ %
+ % XXX should try using sparse_bitset here.
+:- pred minimal_model(vars(T)::in, check_robdd(T)::in, vars(T)::out,
+ vars(T)::out) is nondet.
+
+%-----------------------------------------------------------------------------%
+
+:- func ensure_normalised(check_robdd(T)::in) =
+ (check_robdd(T)::no_check_robdd) is det.
+
+%-----------------------------------------------------------------------------%
+
+% XXX
+:- func robdd(check_robdd(T)) = robdd(T).
+
+%-----------------------------------------------------------------------------%
+%-----------------------------------------------------------------------------%
+
+:- implementation.
+
+:- import_module mode_robdd__r.
+:- import_module mode_robdd__tfer.
+:- import_module mode_robdd__tfeir.
+:- import_module mode_robdd__tfeirn.
+
+:- import_module robdd, sparse_bitset, require.
+
+% Uncomment these for debugging.
+% :- import_module io, pprint.
+% :- import_module unsafe.
+
+% The two fields of this type represent the two mode_robdd implementations
+% being compared.
+:- type check_robdd(T)
+ ---> mode_robdd(
+ x1 :: tfeir(T),
+ x2 :: tfeirn(T)
+ ).
+
+:- func check_robdd(tfeir(T), tfeirn(T)) = check_robdd(T).
+% :- pragma promise_pure(check_robdd/2).
+
+check_robdd(X1, X2) = mode_robdd(X1, X2) :-
+ R1 = to_robdd(X1),
+ R2 = to_robdd(X2),
+ ( R1 = R2 ->
+ true
+ ;
+ error("ROBDD representations differ")
+ % impure unsafe_perform_io(report_robdd_error(R1, R2))
+ ).
+
+% :- pred report_robdd_error(robdd(T)::in, robdd(T)::in, io__state::di,
+% io__state::uo) is det.
+%
+% report_robdd_error(R1, R2) -->
+% % { R12 = R1 * (~ R2) },
+% % { R21 = R2 * (~ R1) },
+% io__write_string("ROBDD representations differ\n"),
+% { P = (pred(V::in, di, uo) is det --> io__write_int(var_to_int(V))) },
+% robdd_to_dot(R1, P, "r1.dot"),
+% robdd_to_dot(R2, P, "r2.dot").
+% % io__write_string("R1 - R2:\n"),
+% % pprint__write(80, to_doc(R12)),
+% % io__write_string("\nR2 - R1:\n"),
+% % pprint__write(80, to_doc(R21)),
+% % io__nl.
+
+%-----------------------------------------------------------------------------%
+
+one = mode_robdd(one, one).
+
+zero = mode_robdd(zero, zero).
+
+X * Y = check_robdd(X ^ x1 * Y ^ x1, X ^ x2 * Y ^ x2).
+
+X + Y = check_robdd(X ^ x1 + Y ^ x1, X ^ x2 + Y ^ x2).
+
+var_entailed(X, V) :-
+ var_entailed(X ^ x1, V).
+
+vars_entailed(X) =
+ vars_entailed(X ^ x1).
+
+vars_disentailed(X) =
+ vars_disentailed(X ^ x1).
+
+restrict(V, X) =
+ check_robdd(restrict(V, X ^ x1), restrict(V, X ^ x2)).
+
+restrict_threshold(V, X) =
+ check_robdd(restrict_threshold(V, X ^ x1),
+ restrict_threshold(V, X ^ x2)).
+
+var(V, X) = check_robdd(var(V, X ^ x1), var(V, X ^ x2)).
+
+not_var(V, X) = check_robdd(not_var(V, X ^ x1), not_var(V, X ^ x2)).
+
+eq_vars(VarA, VarB, X) =
+ check_robdd(eq_vars(VarA, VarB, X ^ x1), eq_vars(VarA, VarB, X ^ x2)).
+
+neq_vars(VarA, VarB, X) =
+ check_robdd(neq_vars(VarA, VarB, X ^ x1), neq_vars(VarA, VarB, X ^ x2)).
+
+imp_vars(VarA, VarB, X) =
+ check_robdd(imp_vars(VarA, VarB, X ^ x1), imp_vars(VarA, VarB, X ^ x2)).
+
+conj_vars(Vars, X) =
+ check_robdd(conj_vars(Vars, X ^ x1), conj_vars(Vars, X ^ x2)).
+
+conj_not_vars(Vars, X) =
+ check_robdd(conj_not_vars(Vars, X ^ x1), conj_not_vars(Vars, X ^ x2)).
+
+disj_vars(Vars, X) =
+ check_robdd(disj_vars(Vars, X ^ x1), disj_vars(Vars, X ^ x2)).
+
+at_most_one_of(Vars, X) =
+ check_robdd(at_most_one_of(Vars, X ^ x1), at_most_one_of(Vars, X ^ x2)).
+
+not_both(VarA, VarB, X) =
+ check_robdd(not_both(VarA, VarB, X ^ x1), not_both(VarA, VarB, X ^ x2)).
+
+io_constraint(V_in, V_out, V_, X) =
+ check_robdd(io_constraint(V_in, V_out, V_, X ^ x1),
+ io_constraint(V_in, V_out, V_, X ^ x2)).
+
+disj_vars_eq(Vars, Var, X) =
+ check_robdd(disj_vars_eq(Vars, Var, X ^ x1),
+ disj_vars_eq(Vars, Var, X ^ x2)).
+
+var_restrict_true(V, X) =
+ check_robdd(var_restrict_true(V, X ^ x1), var_restrict_true(V, X ^ x2)).
+
+var_restrict_false(V, X) =
+ check_robdd(var_restrict_false(V, X ^ x1),
+ var_restrict_false(V, X ^ x2)).
+
+restrict_filter(P, X) =
+ check_robdd(restrict_filter(P, X ^ x1), restrict_filter(P, X ^ x2)).
+
+labelling(Vars, X, TrueVars, FalseVars) :-
+ labelling(Vars, X ^ x1, TrueVars, FalseVars).
+
+minimal_model(Vars, X, TrueVars, FalseVars) :-
+ minimal_model(Vars, X ^ x1, TrueVars, FalseVars).
+
+%-----------------------------------------------------------------------------%
+
+robdd(X) = X ^ x1 ^ robdd.
+
+%-----------------------------------------------------------------------------%
+
+ensure_normalised(mode_robdd(X1, X2)) = mode_robdd(X1, ensure_normalised(X2)).
Index: compiler/mode_robdd.equiv_vars.m
===================================================================
RCS file: compiler/mode_robdd.equiv_vars.m
diff -N compiler/mode_robdd.equiv_vars.m
--- /dev/null 1 Jan 1970 00:00:00 -0000
+++ compiler/mode_robdd.equiv_vars.m 16 Dec 2004 02:29:18 -0000
@@ -0,0 +1,362 @@
+%---------------------------------------------------------------------------%
+% Copyright (C) 2001-2003 The University of Melbourne.
+% 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.equiv_vars.m.
+% Main author: dmo
+
+:- module mode_robdd__equiv_vars.
+
+:- interface.
+
+:- import_module check_hlds.
+:- import_module check_hlds__mode_constraint_robdd.
+:- import_module robdd, bool, term.
+
+:- func init_equiv_vars = equiv_vars(T).
+
+:- func add_equality(var(T), var(T), equiv_vars(T)) = equiv_vars(T).
+
+:- func add_equalities(vars(T), equiv_vars(T)) = equiv_vars(T).
+
+:- pred vars_are_equivalent(equiv_vars(T)::in, var(T)::in, var(T)::in)
+ is semidet.
+
+:- pred vars_are_not_equivalent(equiv_vars(T)::in, var(T)::in, var(T)::in)
+ is semidet.
+
+:- func leader(var(T), equiv_vars(T)) = var(T) is semidet.
+:- pragma type_spec(leader/2, T = mc_type).
+
+:- func det_leader(var(T), equiv_vars(T)) = var(T).
+
+:- pred empty(equiv_vars(T)::in) is semidet.
+
+:- func equiv_vars(T) * equiv_vars(T) = equiv_vars(T).
+
+:- func equiv_vars(T) + equiv_vars(T) = equiv_vars(T).
+
+:- func equiv_vars(T) `difference` equiv_vars(T) = equiv_vars(T).
+
+:- func delete(equiv_vars(T), var(T)) = equiv_vars(T).
+
+:- func restrict_threshold(var(T), equiv_vars(T)) = equiv_vars(T).
+
+:- func filter(pred(var(T)), equiv_vars(T)) = equiv_vars(T).
+:- mode filter(pred(in) is semidet, in) = out is det.
+
+:- pred normalise_known_equivalent_vars(bool::out, vars(T)::in, vars(T)::out,
+ equiv_vars(T)::in, equiv_vars(T)::out) is det.
+:- pragma type_spec(normalise_known_equivalent_vars/5, T = mc_type).
+
+:- pred label(equiv_vars(T)::in, vars(T)::in, vars(T)::out, vars(T)::in,
+ vars(T)::out) is det.
+
+:- func equivalent_vars_in_robdd(robdd(T)) = equiv_vars(T) is semidet.
+
+:- func remove_equiv(equiv_vars(T), robdd(T)) = robdd(T).
+
+%---------------------------------------------------------------------------%
+
+:- implementation.
+
+:- import_module map, list, set, assoc_list, std_util, require, sparse_bitset.
+
+init_equiv_vars = equiv_vars(map__init).
+
+add_equality(VarA, VarB, EQVars0) = EQVars :-
+ ( LeaderA = EQVars0 ^ leader(VarA) ->
+ ( LeaderB = EQVars0 ^ leader(VarB) ->
+ compare(R, LeaderA, LeaderB),
+ (
+ R = (=),
+ EQVars = EQVars0
+ ;
+ R = (<),
+ EQVars = add_equality_2(LeaderA, LeaderB,
+ EQVars0)
+ ;
+ R = (>),
+ EQVars = add_equality_2(LeaderB, LeaderA,
+ EQVars0)
+ )
+ ;
+ compare(R, LeaderA, VarB),
+ (
+ R = (=),
+ EQVars = EQVars0
+ ;
+ R = (<),
+ EQVars = EQVars0 ^ leader(VarB) := LeaderA
+ ;
+ R = (>),
+ EQVars = add_equality_2(VarB, LeaderA, EQVars0)
+ )
+ )
+ ;
+ ( LeaderB = EQVars0 ^ leader(VarB) ->
+ compare(R, LeaderB, VarA),
+ (
+ R = (=),
+ EQVars = EQVars0
+ ;
+ R = (<),
+ EQVars = EQVars0 ^ leader(VarA) := LeaderB
+ ;
+ R = (>),
+ EQVars = add_equality_2(VarA, LeaderB, EQVars0)
+ )
+ ;
+ compare(R, VarA, VarB),
+ (
+ R = (=),
+ EQVars = EQVars0
+ ;
+ R = (<),
+ EQVars = (EQVars0 ^ leader(VarB) := VarA)
+ ^ leader(VarA) := VarA
+ ;
+ R = (>),
+ EQVars = (EQVars0 ^ leader(VarB) := VarB)
+ ^ leader(VarA) := VarB
+ )
+ )
+ ).
+
+:- func add_equality_2(var(T), var(T), equiv_vars(T)) = equiv_vars(T).
+
+add_equality_2(A, B, EQVars) =
+ EQVars ^ leader_map :=
+ normalise_leader_map((EQVars ^ leader(B) := A) ^ leader_map).
+
+add_equalities(Vars0, EQVars) =
+ ( remove_least(Vars0, Var, Vars) ->
+ foldl(add_equality(Var), Vars, EQVars)
+ ;
+ EQVars
+ ).
+
+vars_are_equivalent(_, V, V).
+vars_are_equivalent(EQVars, VA, VB) :-
+ EQVars ^ leader(VA) = EQVars ^ leader(VB).
+
+vars_are_not_equivalent(EQVars, VA, VB) :-
+ \+ vars_are_equivalent(EQVars, VA, VB).
+
+leader(Var, EQVars) = EQVars ^ leader_map ^ elem(Var).
+
+det_leader(Var, EQVars) = ( L = EQVars ^ leader(Var) -> L ; Var).
+
+:- func 'leader :='(var(T), equiv_vars(T), var(T)) = equiv_vars(T).
+
+'leader :='(Var0, EQVars0, Var) =
+ EQVars0 ^ leader_map ^ elem(Var0) := Var.
+
+empty(equiv_vars(LM)) :- is_empty(LM).
+
+equiv_vars(MA) * equiv_vars(MB) = equiv_vars(M) :-
+ M1 = map__foldl(func(Var, LeaderA, M0) =
+ ( LeaderB = M0 ^ elem(Var) ->
+ ( compare(<, LeaderA, LeaderB) ->
+ M0 ^ elem(LeaderB) := LeaderA
+ ; compare(<, LeaderB, LeaderA) ->
+ M0 ^ elem(LeaderA) := LeaderB
+ ;
+ M0
+ )
+ ;
+ M0 ^ elem(Var) := LeaderA
+ ),
+ MA, MB),
+ M = normalise_leader_map(M1).
+
+:- func normalise_leader_map(leader_map(T)) = leader_map(T).
+
+normalise_leader_map(Map) =
+ map__foldl(func(Var, Leader, M0) =
+ ( Leader = Var ->
+ M0
+ ; LeaderLeader = M0 ^ elem(Leader) ->
+ M0 ^ elem(Var) := LeaderLeader
+ ;
+ ( M0 ^ elem(Var) := Leader ) ^ elem(Leader) := Leader
+ ),
+ Map, map__init).
+
+EA + EB = E :-
+ VarsA = set__sorted_list_to_set(map__sorted_keys(EA ^ leader_map)),
+ VarsB = set__sorted_list_to_set(map__sorted_keys(EB ^ leader_map)),
+ Vars = set__to_sorted_list(VarsA `intersect` VarsB),
+ disj_2(Vars, EA, EB, init_equiv_vars, E).
+
+:- pred disj_2(list(var(T))::in, equiv_vars(T)::in, equiv_vars(T)::in,
+ equiv_vars(T)::in, equiv_vars(T)::out) is det.
+
+disj_2([], _, _) --> [].
+disj_2([V | Vs0], EA, EB) -->
+ { Match = no },
+ disj_3(Vs0, Vs, V, EA^det_leader(V), EB^det_leader(V), Match, EA, EB),
+ disj_2(Vs, EA, EB).
+
+:- pred disj_3(list(var(T))::in, list(var(T))::out, var(T)::in, var(T)::in,
+ var(T)::in, bool::in, equiv_vars(T)::in, equiv_vars(T)::in,
+ equiv_vars(T)::in, equiv_vars(T)::out) is det.
+
+disj_3([], [], _, _, _, _, _, _) --> [].
+disj_3([V | Vs0], Vs, L, LA, LB, Match, EA, EB) -->
+ (
+ { EA ^ leader(V) = LA },
+ { EB ^ leader(V) = LB }
+ ->
+ ^ leader(V) := L,
+ (
+ { Match = yes }
+ ;
+ { Match = no },
+ ^ leader(L) := L
+ ),
+ disj_3(Vs0, Vs, L, LA, LB, yes, EA, EB)
+ ;
+ disj_3(Vs0, Vs1, L, LA, LB, Match, EA, EB),
+ { Vs = [V | Vs1] }
+ ).
+
+% XXX I don't think this implementation of difference is correct, but it should
+% work for the purpose we use it for in 'mode_robdd:+' since it never removes
+% any equivalences which it shouldn't.
+EA `difference` EB = E :-
+ Vars = map__sorted_keys(EA ^ leader_map),
+ diff_2(Vars, EA, EB, init_equiv_vars, E).
+
+:- pred diff_2(list(var(T))::in, equiv_vars(T)::in, equiv_vars(T)::in,
+ equiv_vars(T)::in, equiv_vars(T)::out) is det.
+
+diff_2([], _, _) --> [].
+diff_2([V | Vs0], EA, EB) -->
+ { Match = no },
+ diff_3(Vs0, Vs, V, EA^det_leader(V), EB^det_leader(V), Match, EA, EB),
+ diff_2(Vs, EA, EB).
+
+:- pred diff_3(list(var(T))::in, list(var(T))::out, var(T)::in, var(T)::in,
+ var(T)::in, bool::in, equiv_vars(T)::in, equiv_vars(T)::in,
+ equiv_vars(T)::in, equiv_vars(T)::out) is det.
+
+diff_3([], [], _, _, _, _, _, _) --> [].
+diff_3([V | Vs0], Vs, L, LA, LB, Match, EA, EB) -->
+ (
+ { EA ^ leader(V) = LA },
+ { \+ EB ^ leader(V) = LB }
+ ->
+ ^ leader(V) := L,
+ (
+ { Match = yes }
+ ;
+ { Match = no },
+ ^ leader(L) := L
+ ),
+ diff_3(Vs0, Vs, L, LA, LB, yes, EA, EB)
+ ;
+ diff_3(Vs0, Vs1, L, LA, LB, Match, EA, EB),
+ { Vs = [V | Vs1] }
+ ).
+
+delete(E0, V) = E :-
+ ( L = E0 ^ leader(V) ->
+ ( L = V ->
+ M0 = map__delete(E0 ^ leader_map, V),
+ Vars = solutions(map__inverse_search(M0, V)),
+ ( Vars = [NewLeader | _] ->
+ M = list__foldl(
+ func(V1, M1) =
+ M1 ^ elem(V1) := NewLeader,
+ Vars, M0),
+ E = equiv_vars(M)
+ ;
+ error("mode_robdd:equiv_vars:delete: malformed leader map")
+ )
+ ;
+ E = equiv_vars(map__delete(E0 ^ leader_map, V))
+ )
+ ;
+ E = E0
+ ).
+
+restrict_threshold(Th, E) = equiv_vars(normalise_leader_map(LM)) :-
+ LL0 = map__to_assoc_list(E ^ leader_map),
+ list__takewhile((pred((V - _)::in) is semidet :-
+ \+ compare(>, V, Th)
+ ), LL0, LL, _),
+ LM = map__from_assoc_list(LL).
+
+% XXX not terribly efficient.
+filter(P, equiv_vars(LM0)) = equiv_vars(LM) :-
+ list__filter(P, map__keys(LM0), _, Vars),
+ LM = list__foldl(func(V, M) = delete(M, V), Vars, LM0).
+
+normalise_known_equivalent_vars(Changed, Vars0, Vars, EQVars0, EQVars) :-
+ ( ( empty(Vars0) ; empty(EQVars0) ) ->
+ Vars = Vars0,
+ EQVars = EQVars0,
+ Changed = no
+ ;
+ Vars1 = foldl(normalise_known_equivalent_vars_1(EQVars0),
+ Vars0, Vars0),
+ EQVars0 = equiv_vars(LeaderMap0),
+ foldl(normalise_known_equivalent_vars_2, LeaderMap0,
+ {no, Vars1, LeaderMap0}, {Changed, Vars, LeaderMap}),
+ EQVars = equiv_vars(LeaderMap)
+ ).
+
+:- func normalise_known_equivalent_vars_1(equiv_vars(T), var(T),
+ vars(T)) = vars(T).
+:- pragma type_spec(normalise_known_equivalent_vars_1/3, T = mc_type).
+
+normalise_known_equivalent_vars_1(EQVars, V, Vs) =
+ ( L = EQVars ^ leader(V) ->
+ Vs `insert` L
+ ;
+ Vs
+ ).
+
+:- pred normalise_known_equivalent_vars_2(var(T)::in, var(T)::in,
+ {bool, vars(T), leader_map(T)}::in,
+ {bool, vars(T), leader_map(T)}::out) is det.
+
+normalise_known_equivalent_vars_2(Var, Leader, {Changed0, Vars0, LM0},
+ {Changed, Vars, LM}) :-
+ ( Vars0 `contains` Leader ->
+ Vars = Vars0 `insert` Var,
+ LM = LM0 `delete` Var,
+ Changed = yes
+ ;
+ Vars = Vars0,
+ LM = LM0,
+ Changed = Changed0
+ ).
+
+label(E, True0, True, False0, False) :-
+ map__foldl2(
+ (pred(V::in, L::in, T0::in, T::out, F0::in, F::out) is det :-
+ ( T0 `contains` L ->
+ T = T0 `insert` V,
+ F = F0
+ ; F0 `contains` L ->
+ T = T0,
+ F = F0 `insert` V
+ ;
+ T = T0,
+ F = F0
+ )
+ ), E ^ leader_map, True0, True, False0, False).
+
+equivalent_vars_in_robdd(Robdd) = LeaderMap :-
+ some_vars(LeaderMap) = robdd__equivalent_vars(Robdd).
+
+remove_equiv(EQVars, Robdd) =
+ ( is_empty(EQVars ^ leader_map) ->
+ Robdd
+ ;
+ rename_vars(func(V) = EQVars ^ det_leader(V), Robdd)
+ ).
Index: compiler/mode_robdd.implications.m
===================================================================
RCS file: compiler/mode_robdd.implications.m
diff -N compiler/mode_robdd.implications.m
--- /dev/null 1 Jan 1970 00:00:00 -0000
+++ compiler/mode_robdd.implications.m 19 May 2003 07:55:31 -0000
@@ -0,0 +1,579 @@
+%---------------------------------------------------------------------------%
+% Copyright (C) 2001-2003 The University of Melbourne.
+% 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
+
+% This module
+
+:- module mode_robdd__implications.
+
+:- interface.
+
+:- import_module robdd, bool, 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(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 map, require, assoc_list, std_util, term, list, sparse_bitset.
+
+% Uncomment these for debugging.
+% :- import_module unsafe, io.
+
+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) =
+ ( compare((>), V, Threshold) ->
+ IM
+ ;
+ 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(pred(in) is semidet, in) = out is det.
+
+filter_imp_map(P, IM) =
+ map__foldl(func(V, Vs, M) =
+ ( P(V) ->
+ M ^ entry(V) := filter(P, Vs)
+ ;
+ M `delete` V
+ ),
+ IM, IM).
+
+neq_vars(A, B, ImpVars) =
+ ImpVars ^ add_clause({neg(A), neg(B)}) ^ add_clause({pos(A), pos(B)}).
+
+imp_vars(A, B, ImpVars) =
+ ImpVars ^ add_clause({neg(A), pos(B)}).
+
+at_most_one_of(Vars0, ImpVars) =
+ ( remove_least(Vars0, Var, Vars) ->
+ ImpVars ^ foldl(not_both(Var), Vars) ^ at_most_one_of(Vars)
+ ;
+ ImpVars
+ ).
+
+not_both(A, B, ImpVars) =
+ ImpVars ^ add_clause({neg(A), neg(B)}).
+
+either(A, B, ImpVars) =
+ ImpVars ^ add_clause({pos(A), pos(B)}).
+
+normalise_true_false_implication_vars(Changed, TrueVars0, TrueVars,
+ FalseVars0, FalseVars, ImpVars0, ImpVars) :-
+ (
+ empty(TrueVars0),
+ empty(FalseVars0)
+ ->
+ TrueVars = TrueVars0,
+ FalseVars = FalseVars0,
+ ImpVars = ImpVars0,
+ Changed = no
+ ;
+ 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)
+ ;
+ 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} :-
+ (
+ ( IsDisImp = yes -> Fs0 ; Ts0 ) `contains` V
+ ->
+ Ts = Ts0 `union` Vs,
+ Fs = Fs0,
+ IMs = IMs0 `delete` V,
+ C = yes
+ ;
+ ( IsDisImp = yes -> Ts0 ; Fs0 ) `contains` V
+ ->
+ Ts = Ts0,
+ Fs = Fs0,
+ IMs = IMs0 `delete` V,
+ C = yes
+ ;
+ FVs = Fs0 `intersect` Vs,
+ \+ empty(FVs)
+ ->
+ Ts = ( IsDisImp = yes -> Ts0 `insert` V ; Ts0 ),
+ Fs = ( IsDisImp = yes -> Fs0 ; Fs0 `insert` V ),
+ IMs = IMs0 `delete` V,
+ C = yes
+ ;
+ TVs = Ts0 `intersect` Vs,
+ \+ empty(TVs)
+ ->
+ Ts = Ts0,
+ Fs = Fs0,
+ UTVs = Vs `difference` TVs,
+ IMs = ( empty(UTVs) ->
+ IMs0 `delete` V
+ ;
+ IMs0 ^ elem(V) := UTVs
+ ),
+ C = yes
+ ;
+ 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,
+ ( is_empty(Intersect) ->
+ Changed = no,
+ FalseVars = FalseVars0
+ ;
+ 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, ( Vs = Vs0 -> C ; 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),
+
+ ( ( is_empty(Imps0) ; is_empty(RevImps0) ) ->
+ Changed = no,
+ EQVars = EQVars0,
+ ImpVars = ImpVars0
+ ;
+ {Changed, EQVars, Imps, RevImps} = foldl(
+ ( func(V, IVs, {C0, E0, I0, R0}) = {C, E, I, R} :-
+ (
+ RVs = R0 ^ elem(V),
+ EVs = IVs `intersect` RVs,
+ \+ empty(EVs)
+ ->
+ C = yes,
+ E = add_equalities(EVs `insert` V, E0),
+ I = I0 ^ entry(V) := IVs `difference` RVs,
+ R = R0 ^ entry(V) := RVs `difference` IVs
+ ;
+ C = C0, E = E0, I = I0, R = R0
+ )
+ ), Imps0, {no, EQVars0, Imps0, RevImps0}),
+ ImpVars = imp_vars(Imps, RevImps, DisImps, RevDisImps)
+ ).
+
+%------------------------------------------------------------------------%
+
+% XXX
+%:- pragma promise_pure(extract_implication_vars_from_robdd/5).
+
+extract_implication_vars_from_robdd(Changed, Robdd0, Robdd,
+ ImpVars0, ImpVars) :-
+ % ImpVars1 = add_backwards_relations(extract_implications(Robdd0)),
+ ImpVars1 = extract_implications(Robdd0),
+ ImpVars = ImpVars0 * ImpVars1,
+
+ % XXX
+ /*
+ P = (pred(V::in, di, uo) is det --> io__write_int(var_to_int(V))), % XXX
+ impure unsafe_perform_io(robdd_to_dot(Robdd0, P, "extract_impl_before.dot")), % XXX
+ */
+
+ Robdd = remove_implications(ImpVars, Robdd0),
+
+ /*
+ impure unsafe_perform_io(robdd_to_dot(Robdd, P, "extract_impl_after.dot")), % XXX
+ */
+
+ Changed = ( Robdd = Robdd0, empty(ImpVars1) -> no ; 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) =
+ ( Vs = M ^ elem(V) ->
+ Vs
+ ;
+ init
+ ).
+
+:- func 'entry :='(var(T), imp_map(T), vars(T)) = imp_map(T).
+
+'entry :='(V, M, Vs) =
+ ( empty(Vs) ->
+ M `delete` V
+ ;
+ M ^ elem(V) := Vs
+ ).
+
+:- func 'new_relation :='(var(T), imp_map(T), var(T)) = imp_map(T).
+
+'new_relation :='(VA, M, VB) =
+ ( Vs = M ^ elem(VA) ->
+ M ^ elem(VA) := Vs `insert` VB
+ ;
+ 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 :-
+ ( Vs = M0 ^ elem(VA) ->
+ \+ ( Vs `contains` VB ),
+ M = M0 ^ elem(VA) := Vs `insert` VB
+ ;
+ M = M0 ^ elem(VA) := make_singleton_set(VB)
+ ).
+
+:- func 'new_relations :='(var(T), imp_map(T), vars(T)) = imp_map(T).
+
+'new_relations :='(V, M, NewVs) =
+ ( Vs = M ^ elem(V) ->
+ M ^ elem(V) := Vs `union` NewVs
+ ;
+ M ^ elem(V) := NewVs
+ ).
+
+:- 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) `union` imp_map(T) = imp_map(T).
+
+IMA `union` IMB = union(union, IMA, IMB).
+
+:- 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 =
+ ( is_empty(IMA) ->
+ IMA
+ ;
+ map__foldl(func(V, VsB, M) =
+ ( VsA = M ^ elem(V) ->
+ M ^ entry(V) := VsA `difference` VsB
+ ;
+ M
+ ),
+ IMB, IMA)
+ ).
+
+:- func remove_empty_sets(imp_map(T)) = imp_map(T).
+
+remove_empty_sets(IM) =
+ map__foldl(func(V, Vs, M) =
+ ( empty(Vs) ->
+ M `delete` V
+ ;
+ 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) =
+ ( Vs `contains` Var ->
+ M ^ entry(V) := Vs `delete` Var
+ ;
+ M
+ ),
+ IM1, IM1) :-
+ IM1 = IM0 `delete` Var.
+
+%------------------------------------------------------------------------%
+
+:- func add_backwards_relations(imp_vars(T)) = imp_vars(T).
+
+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_clause(bin_clause(T), imp_vars(T)) = imp_vars(T).
+
+add_clause(Clause, ImpVars) =
+ add_clauses([Clause], ImpVars).
+
+:- func add_clauses(list(bin_clause(T)), imp_vars(T)) = imp_vars(T).
+
+add_clauses([], ImpVars) = ImpVars.
+add_clauses([Clause | Clauses], ImpVars0) = ImpVars :-
+ ( ImpVars1 = add_clause_2(Clause, ImpVars0) ->
+ Resolvents = get_resolvents(Clause, ImpVars1),
+ ImpVars = add_clauses(Resolvents ++ Clauses, ImpVars1)
+ ;
+ ImpVars = add_clauses(Clauses, ImpVars0)
+ ).
+
+ % Add a new clause to the imp_vars. Fail if the clause is already
+ % present.
+:- func add_clause_2(bin_clause(T), imp_vars(T)) = imp_vars(T) is semidet.
+
+add_clause_2({neg(VA), pos(VB)}, ImpVars) =
+ (ImpVars ^ imps ^ maybe_new_relation(VA) := VB)
+ ^ rev_imps ^ maybe_new_relation(VB) := VA.
+add_clause_2({pos(VA), neg(VB)}, ImpVars) =
+ (ImpVars ^ rev_imps ^ maybe_new_relation(VA) := VB)
+ ^ imps ^ maybe_new_relation(VB) := VA.
+add_clause_2({neg(VA), neg(VB)}, ImpVars) =
+ (ImpVars ^ dis_imps ^ maybe_new_relation(VA) := VB)
+ ^ dis_imps ^ maybe_new_relation(VB) := VA.
+add_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_clause({MkLitA(VarA), MkLitB(VarB)}, IVs1),
+ Vars, IVs0),
+ IM, ImpVars).
Index: compiler/mode_robdd.r.m
===================================================================
RCS file: compiler/mode_robdd.r.m
diff -N compiler/mode_robdd.r.m
--- /dev/null 1 Jan 1970 00:00:00 -0000
+++ compiler/mode_robdd.r.m 11 Mar 2003 06:04:14 -0000
@@ -0,0 +1,219 @@
+%---------------------------------------------------------------------------%
+% Copyright (C) 2001-2003 The University of Melbourne.
+% 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.r.m.
+% Main author: dmo
+% Stability: low
+
+%-----------------------------------------------------------------------------%
+%-----------------------------------------------------------------------------%
+
+:- module mode_robdd__r.
+
+:- interface.
+
+:- import_module term, robdd.
+
+:- type r(T).
+:- type r == r(generic).
+
+:- inst r == ground. % XXX
+
+:- mode di_r == in. % XXX
+:- mode uo_r == out. % XXX
+
+% Constants.
+:- func one = r(T).
+:- func zero = r(T).
+
+% Conjunction.
+:- func r(T) * r(T) = r(T).
+
+% Disjunction.
+:- func r(T) + r(T) = r(T).
+
+%-----------------------------------------------------------------------------%
+
+:- func var(var(T)::in, r(T)::in(r)) = (r(T)::out(r)) is det.
+
+:- func not_var(var(T)::in, r(T)::in(r)) = (r(T)::out(r)) is det.
+
+:- func eq_vars(var(T)::in, var(T)::in, r(T)::di_r) = (r(T)::uo_r) is det.
+
+:- func neq_vars(var(T)::in, var(T)::in, r(T)::di_r) = (r(T)::uo_r) is det.
+
+:- func imp_vars(var(T)::in, var(T)::in, r(T)::di_r) = (r(T)::uo_r) is det.
+
+:- func conj_vars(vars(T)::in, r(T)::di_r) = (r(T)::uo_r) is det.
+
+:- func disj_vars(vars(T)::in, r(T)::di_r) = (r(T)::uo_r) is det.
+
+:- func at_most_one_of(vars(T)::in, r(T)::di_r) = (r(T)::uo_r) is det.
+
+:- func not_both(var(T)::in, var(T)::in, r(T)::di_r) = (r(T)::uo_r) is det.
+
+:- func io_constraint(var(T)::in, var(T)::in, var(T)::in, r(T)::di_r) =
+ (r(T)::uo_r) is det.
+
+ % disj_vars_eq(Vars, Var) <=> (disj_vars(Vars) =:= Var).
+:- func disj_vars_eq(vars(T)::in, var(T)::in, r(T)::di_r) = (r(T)::uo_r)
+ is det.
+
+:- func var_restrict_true(var(T)::in, r(T)::di_r) = (r(T)::uo_r) is det.
+
+:- func var_restrict_false(var(T)::in, r(T)::di_r) = (r(T)::uo_r) is det.
+
+%-----------------------------------------------------------------------------%
+
+ % Succeed iff the var is entailed by the xROBDD.
+:- pred var_entailed(r(T)::in, var(T)::in) is semidet.
+
+ % Return the set of vars entailed by the xROBDD.
+:- func vars_entailed(r(T)) = vars_entailed_result(T).
+
+ % Return the set of vars disentailed by the xROBDD.
+:- func vars_disentailed(r(T)) = vars_entailed_result(T).
+
+ % Existentially quantify away the var in the xROBDD.
+:- func restrict(var(T), r(T)) = r(T).
+
+ % Existentially quantify away all vars greater than the specified var.
+:- func restrict_threshold(var(T), r(T)) = r(T).
+
+:- func restrict_filter(pred(var(T))::(pred(in) is semidet), r(T)::di_r) =
+ (r(T)::uo_r) is det.
+
+%-----------------------------------------------------------------------------%
+
+ % labelling(Vars, xROBDD, TrueVars, FalseVars)
+ % Takes a set of Vars and an xROBDD and returns a value assignment
+ % for those Vars that is a model of the Boolean function
+ % represented by the xROBDD.
+ % The value assignment is returned in the two sets TrueVars (set
+ % of variables assigned the value 1) and FalseVars (set of
+ % variables assigned the value 0).
+ %
+ % XXX should try using sparse_bitset here.
+:- pred labelling(vars(T)::in, r(T)::in, vars(T)::out, vars(T)::out) is nondet.
+
+ % minimal_model(Vars, xROBDD, TrueVars, FalseVars)
+ % Takes a set of Vars and an xROBDD and returns a value assignment
+ % for those Vars that is a minimal model of the Boolean function
+ % represented by the xROBDD.
+ % The value assignment is returned in the two sets TrueVars (set
+ % of variables assigned the value 1) and FalseVars (set of
+ % variables assigned the value 0).
+ %
+ % XXX should try using sparse_bitset here.
+:- pred minimal_model(vars(T)::in, r(T)::in, vars(T)::out, vars(T)::out)
+ is nondet.
+
+%-----------------------------------------------------------------------------%
+
+% XXX
+:- func robdd(r(T)) = robdd(T).
+
+:- func to_robdd(r(T)) = robdd(T).
+
+%-----------------------------------------------------------------------------%
+%-----------------------------------------------------------------------------%
+
+:- implementation.
+
+:- import_module robdd, sparse_bitset.
+
+% T - true vars, F - False Vars, E - equivalent vars, N -
+% non-equivalent vars, R - ROBDD.
+%
+% Combinations to try:
+% R (straight ROBDD)
+% TER (Peter Schachte's extension)
+% TFENR (Everything)
+
+:- type r(T)
+ ---> mode_robdd(
+ robdd :: robdd(T)
+ ).
+
+one = mode_robdd(one).
+
+zero = mode_robdd(zero).
+
+X * Y = mode_robdd(X ^ robdd * Y ^ robdd).
+
+X + Y = mode_robdd(X ^ robdd + Y ^ robdd).
+
+var_entailed(X, V) :-
+ var_entailed(X ^ robdd, V).
+
+vars_entailed(X) =
+ vars_entailed(X ^ robdd).
+
+vars_disentailed(X) =
+ vars_disentailed(X ^ robdd).
+
+restrict(V, F) =
+ mode_robdd(restrict(V, F ^ robdd)).
+
+restrict_threshold(V, F) =
+ mode_robdd(restrict_threshold(V, F ^ robdd)).
+
+var(V, X) = X ^ robdd :=
+ X ^ robdd * var(V).
+
+not_var(V, X) = X ^ robdd :=
+ X ^ robdd * not_var(V).
+
+eq_vars(VarA, VarB, X) = X ^ robdd :=
+ X ^ robdd * eq_vars(VarA, VarB).
+
+neq_vars(VarA, VarB, X) = X ^ robdd :=
+ X ^ robdd * neq_vars(VarA, VarB).
+
+imp_vars(VarA, VarB, X) = X ^ robdd :=
+ X ^ robdd * imp_vars(VarA, VarB).
+
+conj_vars(Vars, X) = X ^ robdd :=
+ X ^ robdd * conj_vars(Vars).
+
+disj_vars(Vars, X) = X ^ robdd :=
+ X ^ robdd * disj_vars(Vars).
+
+at_most_one_of(Vars, X) = X ^ robdd :=
+ X ^ robdd * at_most_one_of(Vars).
+
+not_both(VarA, VarB, X) = X ^ robdd :=
+ X ^ robdd * ~(var(VarA) * var(VarB)).
+
+io_constraint(V_in, V_out, V_, X) = X ^ robdd :=
+ X ^ robdd *
+ ( var(V_out) =:= var(V_in) + var(V_) ) *
+ ( ~(var(V_in) * var(V_)) ).
+
+disj_vars_eq(Vars, Var, X) = X ^ robdd :=
+ X ^ robdd * ( disj_vars(Vars) =:= var(Var) ).
+
+var_restrict_true(V, X) = X ^ robdd :=
+ var_restrict_true(V, X ^ robdd).
+
+var_restrict_false(V, X) = X ^ robdd :=
+ var_restrict_false(V, X ^ robdd).
+
+restrict_filter(P, X) = X ^ robdd :=
+ restrict_filter(P, X ^ robdd).
+
+labelling(Vars, X, TrueVars, FalseVars) :-
+ labelling(Vars, X ^ robdd, TrueVars, FalseVars).
+
+minimal_model(Vars, X, TrueVars, FalseVars) :-
+ minimal_model(Vars, X ^ robdd, TrueVars, FalseVars).
+
+%-----------------------------------------------------------------------------%
+
+to_robdd(X) = X ^ robdd.
+
+%-----------------------------------------------------------------------------%
+
Index: compiler/mode_robdd.tfeir.m
===================================================================
RCS file: compiler/mode_robdd.tfeir.m
diff -N compiler/mode_robdd.tfeir.m
--- /dev/null 1 Jan 1970 00:00:00 -0000
+++ compiler/mode_robdd.tfeir.m 19 May 2003 08:24:54 -0000
@@ -0,0 +1,680 @@
+%---------------------------------------------------------------------------%
+% Copyright (C) 2001-2003 The University of Melbourne.
+% 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.tfeir.m.
+% Main author: dmo
+% Stability: low
+
+%-----------------------------------------------------------------------------%
+
+:- module mode_robdd__tfeir.
+
+:- interface.
+
+:- import_module check_hlds, check_hlds__mode_constraint_robdd.
+:- import_module term, robdd.
+
+:- type tfeir(T).
+:- type tfeir == tfeir(generic).
+
+:- inst tfeir == ground. % XXX
+
+:- mode di_tfeir == in. % XXX
+:- mode uo_tfeir == out. % XXX
+
+% Constants.
+:- func one = tfeir(T).
+:- pragma type_spec(one/0, T = mc_type).
+
+:- func zero = tfeir(T).
+:- pragma type_spec(zero/0, T = mc_type).
+
+% Conjunction.
+:- func tfeir(T) * tfeir(T) = tfeir(T).
+:- pragma type_spec(('*')/2, T = mc_type).
+
+% Disjunction.
+:- func tfeir(T) + tfeir(T) = tfeir(T).
+:- pragma type_spec(('+')/2, T = mc_type).
+
+%-----------------------------------------------------------------------------%
+
+:- func var(var(T)::in, tfeir(T)::in(tfeir)) = (tfeir(T)::out(tfeir)) is det.
+:- pragma type_spec(var/2, T = mc_type).
+
+:- func not_var(var(T)::in, tfeir(T)::in(tfeir)) = (tfeir(T)::out(tfeir))
+ is det.
+:- pragma type_spec(not_var/2, T = mc_type).
+
+:- func eq_vars(var(T)::in, var(T)::in, tfeir(T)::di_tfeir) =
+ (tfeir(T)::uo_tfeir) is det.
+:- pragma type_spec(eq_vars/3, T = mc_type).
+
+:- func neq_vars(var(T)::in, var(T)::in, tfeir(T)::di_tfeir) =
+ (tfeir(T)::uo_tfeir) is det.
+:- pragma type_spec(neq_vars/3, T = mc_type).
+
+:- func imp_vars(var(T)::in, var(T)::in, tfeir(T)::di_tfeir) =
+ (tfeir(T)::uo_tfeir) is det.
+:- pragma type_spec(imp_vars/3, T = mc_type).
+
+:- func conj_vars(vars(T)::in, tfeir(T)::di_tfeir) = (tfeir(T)::uo_tfeir)
+ is det.
+:- pragma type_spec(conj_vars/2, T = mc_type).
+
+:- func conj_not_vars(vars(T)::in, tfeir(T)::di_tfeir) =
+ (tfeir(T)::uo_tfeir) is det.
+:- pragma type_spec(conj_not_vars/2, T = mc_type).
+
+:- func disj_vars(vars(T)::in, tfeir(T)::di_tfeir) = (tfeir(T)::uo_tfeir)
+ is det.
+:- pragma type_spec(disj_vars/2, T = mc_type).
+
+:- func at_most_one_of(vars(T)::in, tfeir(T)::di_tfeir) = (tfeir(T)::uo_tfeir)
+ is det.
+:- pragma type_spec(at_most_one_of/2, T = mc_type).
+
+:- func not_both(var(T)::in, var(T)::in, tfeir(T)::di_tfeir) =
+ (tfeir(T)::uo_tfeir) is det.
+:- pragma type_spec(not_both/3, T = mc_type).
+
+:- func io_constraint(var(T)::in, var(T)::in, var(T)::in, tfeir(T)::di_tfeir)
+ = (tfeir(T)::uo_tfeir) is det.
+:- pragma type_spec(io_constraint/4, T = mc_type).
+
+ % disj_vars_eq(Vars, Var) <=> (disj_vars(Vars) =:= Var).
+:- func disj_vars_eq(vars(T)::in, var(T)::in, tfeir(T)::di_tfeir) =
+ (tfeir(T)::uo_tfeir) is det.
+:- pragma type_spec(disj_vars_eq/3, T = mc_type).
+
+:- func var_restrict_true(var(T)::in, tfeir(T)::di_tfeir) =
+ (tfeir(T)::uo_tfeir) is det.
+:- pragma type_spec(var_restrict_true/2, T = mc_type).
+
+:- func var_restrict_false(var(T)::in, tfeir(T)::di_tfeir) =
+ (tfeir(T)::uo_tfeir) is det.
+:- pragma type_spec(var_restrict_false/2, T = mc_type).
+
+%-----------------------------------------------------------------------------%
+
+ % Succeed iff the var is entailed by the xROBDD.
+:- pred var_entailed(tfeir(T)::in, var(T)::in) is semidet.
+
+ % Return the set of vars entailed by the xROBDD.
+:- func vars_entailed(tfeir(T)) = vars_entailed_result(T) is det.
+
+ % Return the set of vars disentailed by the xROBDD.
+:- func vars_disentailed(tfeir(T)) = vars_entailed_result(T) is det.
+
+ % Existentially quantify away the var in the xROBDD.
+:- func restrict(var(T), tfeir(T)) = tfeir(T) is det.
+
+ % Existentially quantify away all vars greater than the specified var.
+:- func restrict_threshold(var(T), tfeir(T)) = tfeir(T) is det.
+
+:- func restrict_filter(pred(var(T))::(pred(in) is semidet),
+ tfeir(T)::di_tfeir) = (tfeir(T)::uo_tfeir) is det.
+
+%-----------------------------------------------------------------------------%
+
+ % labelling(Vars, xROBDD, TrueVars, FalseVars)
+ % Takes a set of Vars and an xROBDD and returns a value assignment
+ % for those Vars that is a model of the Boolean function
+ % represented by the xROBDD.
+ % The value assignment is returned in the two sets TrueVars (set
+ % of variables assigned the value 1) and FalseVars (set of
+ % variables assigned the value 0).
+ %
+ % XXX should try using sparse_bitset here.
+:- pred labelling(vars(T)::in, tfeir(T)::in, vars(T)::out, vars(T)::out)
+ is nondet.
+
+ % minimal_model(Vars, xROBDD, TrueVars, FalseVars)
+ % Takes a set of Vars and an xROBDD and returns a value assignment
+ % for those Vars that is a minimal model of the Boolean function
+ % represented by the xROBDD.
+ % The value assignment is returned in the two sets TrueVars (set
+ % of variables assigned the value 1) and FalseVars (set of
+ % variables assigned the value 0).
+ %
+ % XXX should try using sparse_bitset here.
+:- pred minimal_model(vars(T)::in, tfeir(T)::in, vars(T)::out, vars(T)::out)
+ is nondet.
+
+%-----------------------------------------------------------------------------%
+
+% XXX
+% Extract the ROBDD component of the TFEIR.
+:- func robdd(tfeir(T)) = robdd(T).
+
+% Convert the TFEIR to an ROBDD.
+:- func to_robdd(tfeir(T)) = robdd(T).
+
+%-----------------------------------------------------------------------------%
+
+:- func robdd_to_mode_robdd(robdd(T)) = tfeir(T).
+
+%-----------------------------------------------------------------------------%
+
+:- implementation.
+
+:- import_module mode_robdd__equiv_vars.
+:- import_module mode_robdd__implications.
+:- import_module robdd, sparse_bitset, bool, int, list, map.
+
+% T - true vars, F - False Vars, E - equivalent vars, N -
+% non-equivalent vars, I - implications, R - ROBDD.
+%
+% Combinations to try:
+% R (straight ROBDD)
+% TFR
+% TER (Peter Schachte's extension)
+% TFEIR
+% TFENIR
+
+:- type tfeir(T)
+ ---> mode_robdd(
+ true_vars :: vars(T),
+ false_vars :: vars(T),
+ equiv_vars :: equiv_vars(T),
+ imp_vars :: imp_vars(T),
+ robdd :: robdd(T)
+ ).
+
+one = mode_robdd(init, init, init_equiv_vars, init_imp_vars, one).
+
+zero = mode_robdd(init, init, init_equiv_vars, init_imp_vars, zero).
+
+mode_robdd(TA, FA, EA, IA, RA) * mode_robdd(TB, FB, EB, IB, RB) =
+ normalise(mode_robdd(TA1 `union` TB1, FA1 `union` FB1,
+ EA1 * EB1, IA1 * IB1, RA1 * RB1)) :-
+ TU = TA `union` TB,
+ FU = FA `union` FB,
+ EU = EA * EB,
+ IU = IA * IB,
+ mode_robdd(TA1, FA1, EA1, IA1, RA1) =
+ normalise(mode_robdd(TU, FU, EU, IU, RA)),
+ mode_robdd(TB1, FB1, EB1, IB1, RB1) =
+ normalise(mode_robdd(TU, FU, EU, IU, RB)).
+
+mode_robdd(TA0, FA0, EA0, IA0, RA0) + mode_robdd(TB0, FB0, EB0, IB0, RB0) = X :-
+ ( RA0 = zero ->
+ X = mode_robdd(TB0, FB0, EB0, IB0, RB0)
+ ; RB0 = zero ->
+ X = mode_robdd(TA0, FA0, EA0, IA0, RA0)
+ ;
+ X = normalise(mode_robdd(T, F, E, I, R)),
+ T = TA0 `intersect` TB0,
+ F = FA0 `intersect` FB0,
+ E = EA + EB,
+ I = IA + IB,
+ R = RA + RB,
+
+ TAB = TA0 `difference` TB0,
+ FAB = FA0 `difference` FB0,
+ EA = EA0 ^ add_equalities(TAB) ^ add_equalities(FAB),
+
+ TBA = TB0 `difference` TA0,
+ FBA = FB0 `difference` FA0,
+ EB = EB0 ^ add_equalities(TBA) ^ add_equalities(FBA),
+
+ EAB = EA `difference` EB,
+ IA = IA0 ^ add_equalities_to_imp_vars(EAB),
+
+ EBA = EB `difference` EA,
+ IB = IB0 ^ add_equalities_to_imp_vars(EBA),
+
+ RA1 = foldl(
+ func(V, R0) = R0 * var(E ^ det_leader(V)), TAB, RA0),
+ RA2 = foldl(func(V, R0) = R0 *
+ not_var(E ^ det_leader(V)), FAB, RA1),
+ EA1 = (EA `difference` EB) + EA0,
+ RA3 = add_equivalences(EA1, RA2),
+ IA1 = (IA `difference` IB) + IA0,
+ RA = add_implications(IA1, RA3),
+
+ RB1 = foldl(
+ func(V, R0) = R0 * var(E ^ det_leader(V)), TBA, RB0),
+ RB2 = foldl(
+ func(V, R0) = R0 *
+ not_var(E ^ det_leader(V)), FBA, RB1),
+ EB1 = (EB `difference` EA) + EB0,
+ RB3 = add_equivalences(EB1, RB2),
+ IB1 = (IB `difference` IA) + IB0,
+ RB = add_implications(IB1, RB3)
+ ).
+
+var_entailed(X, V) :-
+ (
+ X ^ robdd = zero
+ ;
+ X ^ true_vars `contains` V
+ ).
+
+vars_entailed(X) =
+ ( X ^ robdd = zero ->
+ all_vars
+ ;
+ some_vars(X ^ true_vars)
+ ).
+
+vars_disentailed(X) =
+ ( X ^ robdd = zero ->
+ all_vars
+ ;
+ some_vars(X ^ false_vars)
+ ).
+
+restrict(V, mode_robdd(T, F, E, I, R)) =
+ ( T `contains` V ->
+ mode_robdd(T `delete` V, F, E, I, R)
+ ; F `contains` V ->
+ mode_robdd(T, F `delete` V, E, I, R)
+ ; L = E ^ leader(V) ->
+ ( L \= V ->
+ mode_robdd(T, F, E `delete` V, I, R)
+ ;
+ mode_robdd(T, F, E `delete` V, I `delete` V,
+ restrict(V, R))
+ )
+ ;
+ mode_robdd(T, F, E, I `delete` V, restrict(V, R))
+ ).
+
+restrict_threshold(V, mode_robdd(T, F, E, I, R)) =
+ mode_robdd(remove_gt(T, V), remove_gt(F, V), restrict_threshold(V, E),
+ restrict_threshold(V, I), restrict_threshold(V, R)).
+
+var(V, X) = Res :-
+ X = mode_robdd(T, F, E, I, R),
+ ( T `contains` V ->
+ Res = X
+ ; F `contains` V ->
+ Res = zero
+ ;
+ Res = normalise(mode_robdd(T `insert` V, F, E, I, R))
+ ).
+
+not_var(V, X) = Res :-
+ X = mode_robdd(T, F, E, I, R),
+ ( F `contains` V ->
+ Res = X
+ ; T `contains` V ->
+ Res = zero
+ ;
+ Res = normalise(mode_robdd(T, F `insert` V, E, I, R))
+ ).
+
+eq_vars(VarA, VarB, X) = Res :-
+ X = mode_robdd(T, F, E, I, R),
+ (
+ ( T `contains` VarA, T `contains` VarB
+ ; F `contains` VarA, F `contains` VarB
+ )
+ ->
+ Res = X
+ ;
+ ( T `contains` VarA, F `contains` VarB
+ ; F `contains` VarA, T `contains` VarB
+ )
+ ->
+ Res = zero
+ ;
+ Res = normalise(
+ mode_robdd(T, F, add_equality(VarA, VarB, E), I, R))
+ ).
+
+neq_vars(VarA, VarB, X) = Res :-
+ X = mode_robdd(T, F, E, I, R),
+ (
+ ( T `contains` VarA, T `contains` VarB
+ ; F `contains` VarA, F `contains` VarB
+ )
+ ->
+ Res = zero
+ ;
+ ( T `contains` VarA, F `contains` VarB
+ ; F `contains` VarA, T `contains` VarB
+ )
+ ->
+ Res = X
+ ;
+ Res = normalise(
+ mode_robdd(T, F, E, I ^ neq_vars(VarA, VarB), R))
+ ).
+
+imp_vars(VarA, VarB, X) = Res :-
+ X = mode_robdd(T, F, E, I, R),
+ ( T `contains` VarA, F `contains` VarB ->
+ Res = zero
+ ; T `contains` VarB ->
+ Res = X
+ ; F `contains` VarA ->
+ Res = X
+ ;
+ Res = normalise(
+ mode_robdd(T, F, E, I ^ imp_vars(VarA, VarB), R))
+ ).
+
+conj_vars(Vars, X) = Res :-
+ X = mode_robdd(T, F, E, I, R),
+ ( Vars `subset` T ->
+ Res = X
+ ; \+ empty(Vars `intersect` F) ->
+ Res = zero
+ ;
+ Res = normalise(mode_robdd(T `union` Vars, F, E, I, R))
+ ).
+
+conj_not_vars(Vars, X) = Res :-
+ X = mode_robdd(T, F, E, I, R),
+ ( Vars `subset` F ->
+ Res = X
+ ; \+ empty(Vars `intersect` T) ->
+ Res = zero
+ ;
+ Res = normalise(mode_robdd(T, F `union` Vars, E, I, R))
+ ).
+
+disj_vars(Vars, X) = Res :-
+ X = mode_robdd(T, F, _E, _I, _R),
+ ( \+ empty(Vars `intersect` T) ->
+ Res = X
+ ; Vars `subset` F ->
+ Res = zero
+ ;
+ Res = X `x` disj_vars(Vars)
+ ).
+
+at_most_one_of(Vars, X) = Res :-
+ X = mode_robdd(T, F, E, I, R),
+ ( count(Vars `difference` F) =< 1 ->
+ Res = X
+ ; count(Vars `intersect` T) > 1 ->
+ Res = zero
+ ;
+ Res = normalise(
+ mode_robdd(T, F, E, I ^ at_most_one_of(Vars), R))
+ ).
+
+not_both(VarA, VarB, X) = Res :-
+ X = mode_robdd(T, F, E, I, R),
+ ( F `contains` VarA ->
+ Res = X
+ ; F `contains` VarB ->
+ Res = X
+ ; T `contains` VarA ->
+ Res = not_var(VarB, X)
+ ; T `contains` VarB ->
+ Res = not_var(VarA, X)
+ ;
+ Res = normalise(
+ mode_robdd(T, F, E, I ^ not_both(VarA, VarB), R))
+ ).
+
+io_constraint(V_in, V_out, V_, X) = Res :-
+ Vars = list_to_set([V_in, V_]),
+ Res = X ^ not_both(V_in, V_) ^ disj_vars_eq(Vars, V_out).
+
+disj_vars_eq(Vars, Var, X) = Res :-
+ X = mode_robdd(T, F, _E, _I, _R),
+ ( F `contains` Var ->
+ ( Vars `subset` F ->
+ Res = X
+ ;
+ Res = X ^ conj_not_vars(Vars)
+ )
+ ; T `contains` Var ->
+ ( Vars `subset` F ->
+ Res = zero
+ ;
+ Res = X ^ disj_vars(Vars)
+ )
+ ;
+ Res = X `x` (disj_vars(Vars) =:= var(Var))
+ ).
+
+var_restrict_true(V, mode_robdd(T, F, E, I, R)) = X :-
+ ( F `contains` V ->
+ X = zero
+ ; T `contains` V ->
+ X = mode_robdd(T `delete` V, F, E, I, R)
+ ;
+ X0 = normalise(mode_robdd(T `insert` V, F, E, I, R)),
+ X = X0 ^ true_vars := X0 ^ true_vars `delete` V
+ ).
+
+var_restrict_false(V, mode_robdd(T, F, E, I, R)) = X :-
+ ( T `contains` V ->
+ X = zero
+ ; F `contains` V ->
+ X = mode_robdd(T, F `delete` V, E, I, R)
+ ;
+ X0 = normalise(mode_robdd(T, F `insert` V, E, I, R)),
+ X = X0 ^ false_vars := X0 ^ false_vars `delete` V
+ ).
+
+restrict_filter(P, mode_robdd(T, F, E, I, R)) =
+ mode_robdd(filter(P, T), filter(P, F), filter(P, E), filter(P, I),
+ restrict_filter(P, R)).
+
+labelling(Vars0, mode_robdd(T, F, E, I, R), TrueVars, FalseVars) :-
+ TrueVars0 = T `intersect` Vars0,
+ FalseVars0 = F `intersect` Vars0,
+ Vars = Vars0 `difference` TrueVars0 `difference` FalseVars0,
+
+ ( empty(Vars) ->
+ TrueVars = TrueVars0,
+ FalseVars = FalseVars0
+ ;
+ labelling_2(Vars, mode_robdd(init, init, E, I, R), TrueVars1,
+ FalseVars1),
+ TrueVars = TrueVars0 `union` TrueVars1,
+ FalseVars = FalseVars0 `union` FalseVars1
+ ).
+
+:- pred labelling_2(vars(T)::in, tfeir(T)::in, vars(T)::out, vars(T)::out)
+ is nondet.
+
+labelling_2(Vars0, X0, TrueVars, FalseVars) :-
+ ( remove_least(Vars0, V, Vars) ->
+ (
+ X = var_restrict_false(V, X0),
+ X ^ robdd \= zero,
+ labelling_2(Vars, X, TrueVars, FalseVars0),
+ FalseVars = FalseVars0 `insert` V
+ ;
+ X = var_restrict_true(V, X0),
+ X ^ robdd \= zero,
+ labelling_2(Vars, X, TrueVars0, FalseVars),
+ TrueVars = TrueVars0 `insert` V
+ )
+ ;
+ TrueVars = init,
+ FalseVars = init
+ ).
+
+minimal_model(Vars, X0, TrueVars, FalseVars) :-
+ ( empty(Vars) ->
+ TrueVars = init,
+ FalseVars = init
+ ;
+ minimal_model_2(Vars, X0, TrueVars0, FalseVars0),
+ (
+ TrueVars = TrueVars0,
+ FalseVars = FalseVars0
+ ;
+ X = X0 `x` (~conj_vars(TrueVars0)),
+ minimal_model(Vars, X, TrueVars, FalseVars)
+ )
+ ).
+
+:- pred minimal_model_2(vars(T)::in, tfeir(T)::in, vars(T)::out, vars(T)::out)
+ is semidet.
+
+minimal_model_2(Vars0, X0, TrueVars, FalseVars) :-
+ ( remove_least(Vars0, V, Vars) ->
+ X1 = var_restrict_false(V, X0),
+ ( X1 ^ robdd \= zero ->
+ minimal_model_2(Vars, X1, TrueVars, FalseVars0),
+ FalseVars = FalseVars0 `insert` V
+ ;
+ X2 = var_restrict_true(V, X0),
+ X2 ^ robdd \= zero,
+ minimal_model_2(Vars, X2, TrueVars0, FalseVars),
+ TrueVars = TrueVars0 `insert` V
+ )
+ ;
+ TrueVars = init,
+ FalseVars = init
+ ).
+
+%-----------------------------------------------------------------------------%
+
+:- func normalise(tfeir(T)::di_tfeir) = (tfeir(T)::uo_tfeir) is det.
+:- pragma type_spec(normalise/1, T = mc_type).
+
+normalise(mode_robdd(TrueVars0, FalseVars0, EQVars0, ImpVars0, Robdd0)) = X :-
+ % T <-> F
+ ( \+ empty(TrueVars0 `intersect` FalseVars0) ->
+ X = zero
+ ;
+ % TF <-> E
+ normalise_true_false_equivalent_vars(Changed0, TrueVars0,
+ TrueVars1, FalseVars0, FalseVars1, EQVars0, EQVars1),
+
+ % TF <-> I
+ normalise_true_false_implication_vars(Changed1, TrueVars1,
+ TrueVars2, FalseVars1, FalseVars2, ImpVars0, ImpVars1),
+ Changed2 = Changed0 `bool__or` Changed1,
+
+ % TF -> R
+ Robdd1 = restrict_true_false_vars(TrueVars2, FalseVars2,
+ Robdd0),
+ Changed3 = Changed2 `bool__or` ( Robdd1 \= Robdd0 -> yes ; no),
+
+ (
+ % TF <- R
+ definite_vars(Robdd1, some_vars(NewTrueVars),
+ some_vars(NewFalseVars))
+ ->
+ (
+ empty(NewTrueVars),
+ empty(NewFalseVars)
+ ->
+ Changed4 = Changed3,
+ TrueVars = TrueVars2,
+ FalseVars = FalseVars2
+ ;
+ Changed4 = yes,
+ TrueVars = TrueVars2 `union` NewTrueVars,
+ FalseVars = FalseVars2 `union` NewFalseVars
+ ),
+
+ % E <-> I
+ (
+ propagate_equivalences_into_implications(
+ EQVars1, Changed5, ImpVars1, ImpVars2)
+ ->
+ propagate_implications_into_equivalences(
+ Changed6, EQVars1, EQVars2,
+ ImpVars2, ImpVars3),
+ Changed7 = Changed4 `bool__or`
+ Changed5 `bool__or` Changed6,
+
+ % E <-> R
+ extract_equivalent_vars_from_robdd(Changed8,
+ Robdd1, Robdd2,
+ EQVars2, EQVars),
+ Changed9 = Changed7 `bool__or` Changed8,
+
+ % I <-> R
+ extract_implication_vars_from_robdd(Changed10,
+ Robdd2,
+ Robdd, ImpVars3, ImpVars),
+ Changed = Changed9 `bool__or` Changed10,
+
+ X0 = mode_robdd(TrueVars, FalseVars, EQVars,
+ ImpVars, Robdd),
+ ( Changed = yes ->
+ X = normalise(X0)
+ ;
+ X = X0
+ )
+ ;
+ X = zero
+ )
+ ;
+ X = zero
+ )
+ ).
+
+:- pred normalise_true_false_equivalent_vars(bool::out, vars(T)::in,
+ vars(T)::out, vars(T)::in, vars(T)::out, equiv_vars(T)::in,
+ equiv_vars(T)::out) is det.
+:- pragma type_spec(normalise_true_false_equivalent_vars/7, T = mc_type).
+
+normalise_true_false_equivalent_vars(Changed, T0, T, F0, F) -->
+ normalise_known_equivalent_vars(Changed0, T0, T),
+ normalise_known_equivalent_vars(Changed1, F0, F),
+ { Changed = Changed0 `bool__or` Changed1 }.
+
+:- pred extract_equivalent_vars_from_robdd(bool::out, robdd(T)::in,
+ robdd(T)::out, equiv_vars(T)::in, equiv_vars(T)::out) is det.
+
+extract_equivalent_vars_from_robdd(Changed, Robdd0, Robdd, EQVars0, EQVars) :-
+ ( RobddEQVars = equivalent_vars_in_robdd(Robdd0) ->
+ ( empty(RobddEQVars) ->
+ Changed0 = no,
+ Robdd1 = Robdd0,
+ EQVars = EQVars0
+ ;
+ Changed0 = yes,
+
+ % Remove any equalities we have just found from the
+ % ROBDD.
+ Robdd1 = squeeze_equiv(RobddEQVars, Robdd0),
+
+ EQVars = EQVars0 * RobddEQVars
+ )
+ ;
+ EQVars = init_equiv_vars,
+ Changed0 = ( EQVars = EQVars0 -> no ; yes ),
+ Robdd1 = Robdd0
+ ),
+
+ % Remove any other equalities from the ROBDD.
+ % Note that we can use EQVars0 here since we have already removed the
+ % equivalences in RobddEQVars using squeeze_equiv.
+ Robdd = remove_equiv(EQVars0, Robdd1),
+ Changed = Changed0 `bool__or` ( Robdd \= Robdd1 -> yes ; no ).
+
+:- func x(tfeir(T)::di_tfeir, robdd(T)::in) = (tfeir(T)::uo_tfeir) is det.
+:- pragma type_spec(x/2, T = mc_type).
+
+x(X, R) = X * mode_robdd(init, init, init_equiv_vars, init_imp_vars, R).
+
+%---------------------------------------------------------------------------%
+
+robdd_to_mode_robdd(R) =
+ normalise(mode_robdd(init, init, init_equiv_vars, init_imp_vars, R)).
+
+%---------------------------------------------------------------------------%
+
+to_robdd(X) =
+ (X ^ robdd * conj_vars(X ^ true_vars) * conj_not_vars(X ^ false_vars))
+ ^ map__foldl(func(A, B, R) = R * eq_vars(A, B),
+ X ^ equiv_vars ^ leader_map)
+ ^ add_implications(X ^ imp_vars).
+
+/*
+to_robdd(X) =
+ (X ^ robdd * conj_vars(X ^ true_vars) * conj_not_vars(X ^ false_vars))
+ ^ add_equivalences(X ^ equiv_vars)
+ ^ add_implications(X ^ imp_vars).
+*/
+
+%---------------------------------------------------------------------------%
Index: compiler/mode_robdd.tfeirn.m
===================================================================
RCS file: compiler/mode_robdd.tfeirn.m
diff -N compiler/mode_robdd.tfeirn.m
--- /dev/null 1 Jan 1970 00:00:00 -0000
+++ compiler/mode_robdd.tfeirn.m 19 May 2003 08:20:43 -0000
@@ -0,0 +1,760 @@
+%---------------------------------------------------------------------------%
+% Copyright (C) 2001-2003 The University of Melbourne.
+% 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.tfeirn.m.
+% Main author: dmo
+% Stability: low
+
+%-----------------------------------------------------------------------------%
+
+:- module mode_robdd__tfeirn.
+
+:- interface.
+
+:- import_module check_hlds.
+:- import_module check_hlds__mode_constraint_robdd.
+:- import_module term, robdd.
+
+:- type tfeirn(T).
+:- type tfeirn == tfeirn(generic).
+
+:- inst tfeirn == ground. % XXX
+:- inst norm_tfeirn --->
+ mode_robdd(ground, ground, ground, ground, ground, bound(yes)).
+
+:- mode di_tfeirn == in. % XXX
+:- mode uo_tfeirn == out. % XXX
+
+:- mode ni_tfeirn == in(norm_tfeirn).
+:- mode no_tfeirn == out(norm_tfeirn).
+
+% Constants.
+:- func one = tfeirn(T).
+:- pragma type_spec(one/0, T = mc_type).
+
+:- func zero = tfeirn(T).
+:- pragma type_spec(zero/0, T = mc_type).
+
+% Conjunction.
+:- func tfeirn(T) * tfeirn(T) = tfeirn(T).
+:- pragma type_spec(('*')/2, T = mc_type).
+
+% Disjunction.
+:- func tfeirn(T) + tfeirn(T) = tfeirn(T).
+:- pragma type_spec(('+')/2, T = mc_type).
+
+%-----------------------------------------------------------------------------%
+
+:- func var(var(T)::in, tfeirn(T)::in(tfeirn)) =
+(tfeirn(T)::out(tfeirn))
+ is det.
+:- pragma type_spec(var/2, T = mc_type).
+
+:- func not_var(var(T)::in, tfeirn(T)::in(tfeirn)) = (tfeirn(T)::out(tfeirn))
+ is det.
+:- pragma type_spec(not_var/2, T = mc_type).
+
+:- func eq_vars(var(T)::in, var(T)::in, tfeirn(T)::di_tfeirn) =
+ (tfeirn(T)::uo_tfeirn) is det.
+:- pragma type_spec(eq_vars/3, T = mc_type).
+
+:- func neq_vars(var(T)::in, var(T)::in, tfeirn(T)::di_tfeirn) =
+ (tfeirn(T)::uo_tfeirn) is det.
+:- pragma type_spec(neq_vars/3, T = mc_type).
+
+:- func imp_vars(var(T)::in, var(T)::in, tfeirn(T)::di_tfeirn) =
+ (tfeirn(T)::uo_tfeirn) is det.
+:- pragma type_spec(imp_vars/3, T = mc_type).
+
+:- func conj_vars(vars(T)::in, tfeirn(T)::di_tfeirn) = (tfeirn(T)::uo_tfeirn)
+ is det.
+:- pragma type_spec(conj_vars/2, T = mc_type).
+
+:- func conj_not_vars(vars(T)::in, tfeirn(T)::di_tfeirn) =
+ (tfeirn(T)::uo_tfeirn) is det.
+:- pragma type_spec(conj_not_vars/2, T = mc_type).
+
+:- func disj_vars(vars(T)::in, tfeirn(T)::di_tfeirn) = (tfeirn(T)::uo_tfeirn)
+ is det.
+:- pragma type_spec(disj_vars/2, T = mc_type).
+
+:- func at_most_one_of(vars(T)::in, tfeirn(T)::di_tfeirn) =
+ (tfeirn(T)::uo_tfeirn) is det.
+:- pragma type_spec(at_most_one_of/2, T = mc_type).
+
+:- func not_both(var(T)::in, var(T)::in, tfeirn(T)::di_tfeirn) =
+ (tfeirn(T)::uo_tfeirn) is det.
+:- pragma type_spec(not_both/3, T = mc_type).
+
+:- func io_constraint(var(T)::in, var(T)::in, var(T)::in, tfeirn(T)::di_tfeirn)
+ = (tfeirn(T)::uo_tfeirn) is det.
+:- pragma type_spec(io_constraint/4, T = mc_type).
+
+ % disj_vars_eq(Vars, Var) <=> (disj_vars(Vars) =:= Var).
+:- func disj_vars_eq(vars(T)::in, var(T)::in, tfeirn(T)::di_tfeirn) =
+ (tfeirn(T)::uo_tfeirn) is det.
+:- pragma type_spec(disj_vars_eq/3, T = mc_type).
+
+:- func var_restrict_true(var(T)::in, tfeirn(T)::di_tfeirn) =
+ (tfeirn(T)::no_tfeirn) is det.
+:- pragma type_spec(var_restrict_true/2, T = mc_type).
+
+:- func var_restrict_false(var(T)::in, tfeirn(T)::di_tfeirn) =
+ (tfeirn(T)::no_tfeirn) is det.
+:- pragma type_spec(var_restrict_false/2, T = mc_type).
+
+%-----------------------------------------------------------------------------%
+
+ % Succeed iff the var is entailed by the xROBDD.
+:- pred var_entailed(tfeirn(T)::ni_tfeirn, var(T)::in) is semidet.
+:- pragma type_spec(var_entailed/2, T = mc_type).
+
+ % Return the set of vars entailed by the xROBDD.
+:- func vars_entailed(tfeirn(T)::ni_tfeirn) =
+ (vars_entailed_result(T)::out) is det.
+:- pragma type_spec(vars_entailed/1, T = mc_type).
+
+ % Return the set of vars disentailed by the xROBDD.
+:- func vars_disentailed(tfeirn(T)::ni_tfeirn) =
+ (vars_entailed_result(T)::out) is det.
+:- pragma type_spec(vars_disentailed/1, T = mc_type).
+
+:- pred known_vars(tfeirn(T)::ni_tfeirn, vars(T)::out, vars(T)::out) is det.
+:- pragma type_spec(known_vars/3, T = mc_type).
+
+ % Existentially quantify away the var in the xROBDD.
+:- func restrict(var(T)::in, tfeirn(T)::ni_tfeirn) =
+ (tfeirn(T)::no_tfeirn) is det.
+:- pragma type_spec(restrict/2, T = mc_type).
+
+ % Existentially quantify away all vars greater than the specified var.
+:- func restrict_threshold(var(T)::in, tfeirn(T)::ni_tfeirn) =
+ (tfeirn(T)::no_tfeirn) is det.
+:- pragma type_spec(restrict_threshold/2, T = mc_type).
+
+:- func restrict_filter(pred(var(T))::(pred(in) is semidet),
+ tfeirn(T)::ni_tfeirn) = (tfeirn(T)::no_tfeirn) is det.
+:- pragma type_spec(restrict_filter/2, T = mc_type).
+
+%-----------------------------------------------------------------------------%
+
+ % labelling(Vars, xROBDD, TrueVars, FalseVars)
+ % Takes a set of Vars and an xROBDD and returns a value assignment
+ % for those Vars that is a model of the Boolean function
+ % represented by the xROBDD.
+ % The value assignment is returned in the two sets TrueVars (set
+ % of variables assigned the value 1) and FalseVars (set of
+ % variables assigned the value 0).
+ %
+ % XXX should try using sparse_bitset here.
+:- pred labelling(vars(T)::in, tfeirn(T)::in, vars(T)::out, vars(T)::out)
+ is nondet.
+
+ % minimal_model(Vars, xROBDD, TrueVars, FalseVars)
+ % Takes a set of Vars and an xROBDD and returns a value assignment
+ % for those Vars that is a minimal model of the Boolean function
+ % represented by the xROBDD.
+ % The value assignment is returned in the two sets TrueVars (set
+ % of variables assigned the value 1) and FalseVars (set of
+ % variables assigned the value 0).
+ %
+ % XXX should try using sparse_bitset here.
+:- pred minimal_model(vars(T)::in, tfeirn(T)::in, vars(T)::out, vars(T)::out)
+ is nondet.
+
+%-----------------------------------------------------------------------------%
+
+:- func ensure_normalised(tfeirn(T)::di_tfeirn) = (tfeirn(T)::no_tfeirn) is det.
+:- pragma type_spec(ensure_normalised/1, T = mc_type).
+
+%-----------------------------------------------------------------------------%
+
+% XXX
+% Extract the ROBDD component of the tfeirn.
+:- func robdd(tfeirn(T)) = robdd(T).
+
+% Convert the tfeirn to an ROBDD.
+:- func to_robdd(tfeirn(T)) = robdd(T).
+
+%-----------------------------------------------------------------------------%
+
+:- func robdd_to_mode_robdd(robdd(T)) = tfeirn(T).
+
+%-----------------------------------------------------------------------------%
+
+:- implementation.
+
+:- import_module mode_robdd__equiv_vars.
+:- import_module mode_robdd__implications.
+:- import_module robdd, sparse_bitset, bool, int, list, map.
+
+% T - true vars, F - False Vars, E - equivalent vars, N -
+% non-equivalent vars, I - implications, R - ROBDD.
+%
+% Combinations to try:
+% R (straight ROBDD)
+% TFR
+% TER (Peter Schachte's extension)
+% tfeirn
+% TFENIR
+
+:- type tfeirn(T)
+ ---> mode_robdd(
+ true_vars :: vars(T),
+ false_vars :: vars(T),
+ equiv_vars :: equiv_vars(T),
+ imp_vars :: imp_vars(T),
+ robdd :: robdd(T),
+ normalised :: bool
+ ).
+
+one = mode_robdd(init, init, init_equiv_vars, init_imp_vars, one, yes).
+
+zero = mode_robdd(init, init, init_equiv_vars, init_imp_vars, zero, yes).
+
+mode_robdd(TA, FA, EA, IA, RA, _) * mode_robdd(TB, FB, EB, IB, RB, _) =
+ mode_robdd(TA1 `union` TB1, FA1 `union` FB1,
+ EA1 * EB1, IA1 * IB1, RA1 * RB1, no) :-
+ TU = TA `union` TB,
+ FU = FA `union` FB,
+ EU = EA * EB,
+ IU = IA * IB,
+ mode_robdd(TA1, FA1, EA1, IA1, RA1, _) =
+ normalise(mode_robdd(TU, FU, EU, IU, RA, no)),
+ mode_robdd(TB1, FB1, EB1, IB1, RB1, _) =
+ normalise(mode_robdd(TU, FU, EU, IU, RB, no)).
+
+mode_robdd(TA0, FA0, EA0, IA0, RA0, NA0)
+ + mode_robdd(TB0, FB0, EB0, IB0, RB0, NB0) = X :-
+ ( RA0 = zero ->
+ X = mode_robdd(TB0, FB0, EB0, IB0, RB0, NB0)
+ ; RB0 = zero ->
+ X = mode_robdd(TA0, FA0, EA0, IA0, RA0, NA0)
+ ;
+ X = mode_robdd(T, F, E, I, R, no),
+ T = TA0 `intersect` TB0,
+ F = FA0 `intersect` FB0,
+ E = EA + EB,
+ I = IA + IB,
+ R = RA + RB,
+
+ TAB = TA0 `difference` TB0,
+ FAB = FA0 `difference` FB0,
+ EA = EA0 ^ add_equalities(TAB) ^ add_equalities(FAB),
+
+ TBA = TB0 `difference` TA0,
+ FBA = FB0 `difference` FA0,
+ EB = EB0 ^ add_equalities(TBA) ^ add_equalities(FBA),
+
+ EAB = EA `difference` EB,
+ IA = IA0 ^ add_equalities_to_imp_vars(EAB),
+
+ EBA = EB `difference` EA,
+ IB = IB0 ^ add_equalities_to_imp_vars(EBA),
+
+ RA1 = foldl(
+ func(V, R0) = R0 * var(E ^ det_leader(V)), TAB, RA0),
+ RA2 = foldl(
+ func(V, R0) = R0 *
+ not_var(E ^ det_leader(V)), FAB, RA1),
+ EA1 = (EA `difference` EB) + EA0,
+ RA3 = add_equivalences(EA1, RA2),
+ IA1 = (IA `difference` IB) + IA0,
+ RA = add_implications(IA1, RA3),
+
+ RB1 = foldl(
+ func(V, R0) = R0 * var(E ^ det_leader(V)), TBA, RB0),
+ RB2 = foldl(
+ func(V, R0) = R0 *
+ not_var(E ^ det_leader(V)), FBA, RB1),
+ EB1 = (EB `difference` EA) + EB0,
+ RB3 = add_equivalences(EB1, RB2),
+ IB1 = (IB `difference` IA) + IB0,
+ RB = add_implications(IB1, RB3)
+ ).
+
+var_entailed(X, V) :-
+ (X ^ robdd = zero ; X ^ true_vars `contains` V).
+
+vars_entailed(X) =
+ (X ^ robdd = zero ->
+ all_vars
+ ;
+ some_vars(X ^ true_vars)
+ ).
+
+vars_disentailed(X) =
+ (X ^ robdd = zero ->
+ all_vars
+ ;
+ some_vars(X ^ false_vars)
+ ).
+
+known_vars(X, TrueVars, FalseVars) :-
+ ( X ^ robdd = zero ->
+ TrueVars = init,
+ FalseVars = init
+ ;
+ TrueVars = X ^ true_vars,
+ FalseVars = X ^ false_vars
+ ).
+
+restrict(V, mode_robdd(T, F, E, I, R, N)) =
+ ( T `contains` V ->
+ mode_robdd(T `delete` V, F, E, I, R, N)
+ ; F `contains` V ->
+ mode_robdd(T, F `delete` V, E, I, R, N)
+ ; L = E ^ leader(V) ->
+ ( L \= V ->
+ mode_robdd(T, F, E `delete` V, I, R, N)
+ ;
+ mode_robdd(T, F, E `delete` V, I `delete` V,
+ restrict(V, R), N)
+ )
+ ;
+ mode_robdd(T, F, E, I `delete` V, restrict(V, R), N)
+ ).
+
+restrict_threshold(V, mode_robdd(T, F, E, I, R, N)) =
+ mode_robdd(remove_gt(T, V), remove_gt(F, V), restrict_threshold(V, E),
+ restrict_threshold(V, I), restrict_threshold(V, R), N).
+
+var(V, X) =
+ ( T `contains` V ->
+ X
+ ; F `contains` V ->
+ zero
+ ;
+ mode_robdd(T `insert` V, F, E, I, R, no)
+ ) :-
+ X = mode_robdd(T, F, E, I, R, _).
+
+not_var(V, X) =
+ ( F `contains` V ->
+ X
+ ; T `contains` V ->
+ zero
+ ;
+ mode_robdd(T, F `insert` V, E, I, R, no)
+ ) :-
+ X = mode_robdd(T, F, E, I, R, _).
+
+eq_vars(VarA, VarB, X) =
+ (
+ ( T `contains` VarA, T `contains` VarB
+ ; F `contains` VarA, F `contains` VarB
+ )
+ ->
+ X
+ ;
+ ( T `contains` VarA, F `contains` VarB
+ ; F `contains` VarA, T `contains` VarB
+ )
+ ->
+ zero
+ ;
+ mode_robdd(T, F, add_equality(VarA, VarB, E), I, R, no)
+ ) :-
+ X = mode_robdd(T, F, E, I, R, _).
+
+neq_vars(VarA, VarB, X) =
+ (
+ ( T `contains` VarA, T `contains` VarB
+ ; F `contains` VarA, F `contains` VarB
+ )
+ ->
+ zero
+ ;
+ ( T `contains` VarA, F `contains` VarB
+ ; F `contains` VarA, T `contains` VarB
+ )
+ ->
+ X
+ ;
+ mode_robdd(T, F, E, I ^ neq_vars(VarA, VarB), R, no)
+ ) :-
+ X = mode_robdd(T, F, E, I, R, _).
+
+imp_vars(VarA, VarB, X) =
+ ( T `contains` VarA, F `contains` VarB ->
+ zero
+ ; T `contains` VarB ->
+ X
+ ; F `contains` VarA ->
+ X
+ ;
+ mode_robdd(T, F, E, I ^ imp_vars(VarA, VarB), R, no)
+ ) :-
+ X = mode_robdd(T, F, E, I, R, _).
+
+conj_vars(Vars, X) =
+ ( Vars `subset` T ->
+ X
+ ; \+ empty(Vars `intersect` F) ->
+ zero
+ ;
+ mode_robdd(T `union` Vars, F, E, I, R, no)
+ ) :-
+ X = mode_robdd(T, F, E, I, R, _).
+
+conj_not_vars(Vars, X) =
+ ( Vars `subset` F ->
+ X
+ ; \+ empty(Vars `intersect` T) ->
+ zero
+ ;
+ mode_robdd(T, F `union` Vars, E, I, R, no)
+ ) :-
+ X = mode_robdd(T, F, E, I, R, _).
+
+disj_vars(Vars, X0) = X :-
+ X0 = mode_robdd(T, F, E, I, R, _N),
+ ( \+ empty(Vars `intersect` T) ->
+ X = X0
+ ; Vars `subset` F ->
+ X = zero
+ ;
+ VarsNF = Vars `difference` F,
+ ( remove_least(VarsNF, Var1, VarsNF1) ->
+ ( remove_least(VarsNF1, Var2, VarsNF2) ->
+ ( empty(VarsNF2) ->
+ X = mode_robdd(T, F, E,
+ I ^ either(Var1, Var2),
+ R, no)
+ ;
+ X = X0 `x` disj_vars(VarsNF)
+ )
+ ;
+ X = X0 ^ var(Var1)
+ )
+ ;
+ X = zero
+ )
+ ).
+
+at_most_one_of(Vars, X) =
+ ( count(Vars `difference` F) =< 1 ->
+ X
+ ; count(Vars `intersect` T) > 1 ->
+ zero
+ ;
+ mode_robdd(T, F, E, I ^ at_most_one_of(Vars), R, no)
+ ) :-
+ X = mode_robdd(T, F, E, I, R, _).
+
+not_both(VarA, VarB, X) =
+ ( F `contains` VarA ->
+ X
+ ; F `contains` VarB ->
+ X
+ ; T `contains` VarA ->
+ not_var(VarB, X)
+ ; T `contains` VarB ->
+ not_var(VarA, X)
+ ;
+ mode_robdd(T, F, E, I ^ not_both(VarA, VarB), R, no)
+ ) :-
+ X = mode_robdd(T, F, E, I, R, _).
+
+io_constraint(V_in, V_out, V_, X) =
+ X ^ not_both(V_in, V_) ^ disj_vars_eq(Vars, V_out) :-
+ Vars = list_to_set([V_in, V_]).
+
+disj_vars_eq(Vars, Var, X) =
+ ( F `contains` Var ->
+ ( Vars `subset` F ->
+ X
+ ;
+ X ^ conj_not_vars(Vars)
+ )
+ ; T `contains` Var ->
+ ( Vars `subset` F ->
+ zero
+ ;
+ X ^ disj_vars(Vars)
+ )
+ ; \+ empty(Vars `intersect` T) ->
+ X ^ var(Var)
+ ; Vars `subset` F ->
+ X ^ not_var(Var)
+ ; remove_least(Vars, Var1, Vars1) ->
+ ( empty(Vars1) ->
+ X ^ eq_vars(Var, Var1)
+ ;
+ (X ^ imp_vars_set(Vars, Var)) `x`
+ (var(Var) =< disj_vars(Vars))
+ )
+ ;
+ X ^ not_var(Var)
+ ) :-
+ X = mode_robdd(T, F, _E, _I, _R, _N).
+
+ % imp_vars_set({V1, ..., Vn}, V) <===> (V1 =< V) * ... * (Vn % =< V)
+:- func imp_vars_set(vars(T)::in, var(T)::in, tfeirn(T)::di_tfeirn) =
+ (tfeirn(T)::uo_tfeirn) is det.
+:- pragma type_spec(imp_vars_set/3, T = mc_type).
+
+imp_vars_set(Vars, Var, mode_robdd(T, F, E, I0, R, _)) =
+ mode_robdd(T, F, E, I, R, no) :-
+ I = I0 ^ foldl(func(VarA, I1) = I1 ^ imp_vars(VarA, Var), Vars).
+
+var_restrict_true(V, mode_robdd(T, F, E, I, R, N)) = X :-
+ ( F `contains` V ->
+ X = zero
+ ; T `contains` V ->
+ X = mode_robdd(T `delete` V, F, E, I, R, N)
+ ;
+ X0 = normalise(mode_robdd(T `insert` V, F, E, I, R, no)),
+ X = X0 ^ true_vars := X0 ^ true_vars `delete` V
+ ).
+
+var_restrict_false(V, mode_robdd(T, F, E, I, R, N)) = X :-
+ ( T `contains` V ->
+ X = zero
+ ; F `contains` V ->
+ X = mode_robdd(T, F `delete` V, E, I, R, N)
+ ;
+ X0 = normalise(mode_robdd(T, F `insert` V, E, I, R, no)),
+ X = X0 ^ false_vars := X0 ^ false_vars `delete` V
+ ).
+
+restrict_filter(P, mode_robdd(T, F, E, I, R, N)) =
+ mode_robdd(filter(P, T), filter(P, F), filter(P, E), filter(P, I),
+ restrict_filter(P, R), N).
+
+labelling(Vars0, mode_robdd(T, F, E, I, R, N), TrueVars, FalseVars) :-
+ TrueVars0 = T `intersect` Vars0,
+ FalseVars0 = F `intersect` Vars0,
+ Vars = Vars0 `difference` TrueVars0 `difference` FalseVars0,
+
+ ( empty(Vars) ->
+ TrueVars = TrueVars0,
+ FalseVars = FalseVars0
+ ;
+ labelling_2(Vars, mode_robdd(init, init, E, I, R, N),
+ TrueVars1, FalseVars1),
+ TrueVars = TrueVars0 `union` TrueVars1,
+ FalseVars = FalseVars0 `union` FalseVars1
+ ).
+
+:- pred labelling_2(vars(T)::in, tfeirn(T)::in, vars(T)::out, vars(T)::out)
+ is nondet.
+
+labelling_2(Vars0, X0, TrueVars, FalseVars) :-
+ ( remove_least(Vars0, V, Vars) ->
+ (
+ X = var_restrict_false(V, X0),
+ X ^ robdd \= zero,
+ labelling_2(Vars, X, TrueVars, FalseVars0),
+ FalseVars = FalseVars0 `insert` V
+ ;
+ X = var_restrict_true(V, X0),
+ X ^ robdd \= zero,
+ labelling_2(Vars, X, TrueVars0, FalseVars),
+ TrueVars = TrueVars0 `insert` V
+ )
+ ;
+ TrueVars = init,
+ FalseVars = init
+ ).
+
+minimal_model(Vars, X0, TrueVars, FalseVars) :-
+ ( empty(Vars) ->
+ TrueVars = init,
+ FalseVars = init
+ ;
+ minimal_model_2(Vars, X0, TrueVars0, FalseVars0),
+ (
+ TrueVars = TrueVars0,
+ FalseVars = FalseVars0
+ ;
+ X = X0 `x` (~conj_vars(TrueVars0)),
+ minimal_model(Vars, X, TrueVars, FalseVars)
+ )
+ ).
+
+:- pred minimal_model_2(vars(T)::in, tfeirn(T)::in, vars(T)::out, vars(T)::out)
+ is semidet.
+
+minimal_model_2(Vars0, X0, TrueVars, FalseVars) :-
+ ( remove_least(Vars0, V, Vars) ->
+ X1 = var_restrict_false(V, X0),
+ ( X1 ^ robdd \= zero ->
+ minimal_model_2(Vars, X1, TrueVars, FalseVars0),
+ FalseVars = FalseVars0 `insert` V
+ ;
+ X2 = var_restrict_true(V, X0),
+ X2 ^ robdd \= zero,
+ minimal_model_2(Vars, X2, TrueVars0, FalseVars),
+ TrueVars = TrueVars0 `insert` V
+ )
+ ;
+ TrueVars = init,
+ FalseVars = init
+ ).
+
+%-----------------------------------------------------------------------------%
+
+ensure_normalised(X) = normalise(X).
+
+:- func normalise(tfeirn(T)::di_tfeirn) = (tfeirn(T)::no_tfeirn) is det.
+:- pragma type_spec(normalise/1, T = mc_type).
+
+normalise(X) = X :-
+ X ^ normalised = yes.
+normalise(mode_robdd(TrueVars0, FalseVars0, EQVars0, ImpVars0, Robdd0, no))
+ = X :-
+ % T <-> F
+ ( \+ empty(TrueVars0 `intersect` FalseVars0) ->
+ X = zero
+ ;
+ % TF <-> E
+ normalise_true_false_equivalent_vars(Changed0,
+ TrueVars0, TrueVars1, FalseVars0, FalseVars1,
+ EQVars0, EQVars1),
+
+ % TF <-> I
+ normalise_true_false_implication_vars(Changed1,
+ TrueVars1, TrueVars2, FalseVars1, FalseVars2,
+ ImpVars0, ImpVars1),
+ Changed2 = Changed0 `bool__or` Changed1,
+
+ % TF -> R
+ Robdd1 = restrict_true_false_vars(TrueVars2, FalseVars2,
+ Robdd0),
+ Changed3 = Changed2 `bool__or` ( Robdd1 \= Robdd0 -> yes ; no),
+
+ (
+ % TF <- R
+ definite_vars(Robdd1,
+ some_vars(NewTrueVars), some_vars(NewFalseVars))
+ ->
+ (
+ empty(NewTrueVars),
+ empty(NewFalseVars)
+ ->
+ Changed4 = Changed3,
+ TrueVars = TrueVars2,
+ FalseVars = FalseVars2
+ ;
+ Changed4 = yes,
+ TrueVars = TrueVars2 `union` NewTrueVars,
+ FalseVars = FalseVars2 `union` NewFalseVars
+ ),
+
+ % E <-> I
+ (
+ propagate_equivalences_into_implications(
+ EQVars1, Changed5, ImpVars1, ImpVars2)
+ ->
+ propagate_implications_into_equivalences(
+ Changed6, EQVars1, EQVars2,
+ ImpVars2, ImpVars3),
+ Changed7 = Changed4 `bool__or` Changed5
+ `bool__or` Changed6,
+
+ % E <-> R
+ extract_equivalent_vars_from_robdd(Changed8,
+ Robdd1, Robdd2, EQVars2, EQVars),
+ Changed9 = Changed7 `bool__or` Changed8,
+
+ % I <-> R
+ extract_implication_vars_from_robdd(Changed10,
+ Robdd2, Robdd, ImpVars3, ImpVars),
+ Changed = Changed9 `bool__or` Changed10,
+
+ X0 = mode_robdd(TrueVars, FalseVars, EQVars,
+ ImpVars, Robdd, bool__not(Changed)),
+ ( Changed = yes ->
+ X = normalise(X0)
+ ;
+ X = X0
+ )
+ ;
+ X = zero
+ )
+ ;
+ X = zero
+ )
+ ).
+
+:- pred normalise_true_false_equivalent_vars(bool::out, vars(T)::in,
+ vars(T)::out, vars(T)::in, vars(T)::out, equiv_vars(T)::in,
+ equiv_vars(T)::out) is det.
+:- pragma type_spec(normalise_true_false_equivalent_vars/7, T = mc_type).
+
+normalise_true_false_equivalent_vars(Changed, T0, T, F0, F) -->
+ normalise_known_equivalent_vars(Changed0, T0, T),
+ normalise_known_equivalent_vars(Changed1, F0, F),
+ { Changed = Changed0 `bool__or` Changed1 }.
+
+:- pred extract_equivalent_vars_from_robdd(bool::out, robdd(T)::in,
+ robdd(T)::out, equiv_vars(T)::in, equiv_vars(T)::out) is det.
+:- pragma type_spec(extract_equivalent_vars_from_robdd/5, T = mc_type).
+
+extract_equivalent_vars_from_robdd(Changed, Robdd0, Robdd, EQVars0, EQVars) :-
+ ( RobddEQVars = equivalent_vars_in_robdd(Robdd0) ->
+ ( empty(RobddEQVars) ->
+ Changed0 = no,
+ Robdd1 = Robdd0,
+ EQVars = EQVars0
+ ;
+ Changed0 = yes,
+
+ % Remove any equalities we have just found from the
+ % ROBDD.
+ Robdd1 = squeeze_equiv(RobddEQVars, Robdd0),
+
+ EQVars = EQVars0 * RobddEQVars
+ )
+ ;
+ EQVars = init_equiv_vars,
+ Changed0 = ( EQVars = EQVars0 -> no ; yes ),
+ Robdd1 = Robdd0
+ ),
+
+ % Remove any other equalities from the ROBDD.
+ % Note that we can use EQVars0 here since we have already removed the
+ % equivalences in RobddEQVars using squeeze_equiv.
+ Robdd = remove_equiv(EQVars0, Robdd1),
+ Changed = Changed0 `bool__or` ( Robdd \= Robdd1 -> yes ; no ).
+
+:- func x(tfeirn(T)::di_tfeirn, robdd(T)::in) = (tfeirn(T)::uo_tfeirn) is det.
+:- pragma type_spec(x/2, T = mc_type).
+
+%/*
+x(mode_robdd(TA, FA, EA, IA, RA, _), RB) =
+ mode_robdd(TA `union` T1, FA `union` F1, EA * E1, IA * I1,
+ RA * R1, no) :-
+ mode_robdd(T1, F1, E1, I1, R1, _) =
+ normalise(mode_robdd(TA, FA, EA, IA, RB, no)).
+%*/
+
+/*
+x(mode_robdd(TA, FA, EA, IA, RA, _), RB) =
+ mode_robdd(TA, FA, EA, IA, RA * RB, no).
+*/
+
+%---------------------------------------------------------------------------%
+
+robdd_to_mode_robdd(R) =
+ normalise(mode_robdd(init, init, init_equiv_vars, init_imp_vars,
+ R, no)).
+
+%---------------------------------------------------------------------------%
+
+to_robdd(X) =
+ (X ^ robdd * conj_vars(X ^ true_vars) * conj_not_vars(X ^ false_vars))
+ ^ map__foldl(func(A, B, R) = R * eq_vars(A, B),
+ X ^ equiv_vars ^ leader_map)
+ ^ add_implications(X ^ imp_vars).
+
+% to_robdd(X) =
+% (X ^ robdd * conj_vars(X ^ true_vars) * conj_not_vars(X ^ false_vars))
+% ^ expand_equiv(X ^ equiv_vars ^ leader_map)
+% ^ add_implications(X ^ imp_vars).
+
+%---------------------------------------------------------------------------%
Index: compiler/mode_robdd.tfer.m
===================================================================
RCS file: compiler/mode_robdd.tfer.m
diff -N compiler/mode_robdd.tfer.m
--- /dev/null 1 Jan 1970 00:00:00 -0000
+++ compiler/mode_robdd.tfer.m 19 May 2003 08:20:52 -0000
@@ -0,0 +1,580 @@
+%---------------------------------------------------------------------------%
+% Copyright (C) 2001-2003 The University of Melbourne.
+% 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.tfer.m.
+% Main author: dmo
+% Stability: low
+
+%-----------------------------------------------------------------------------%
+
+:- module mode_robdd__tfer.
+
+:- interface.
+
+:- import_module term, robdd.
+
+:- type tfer(T).
+:- type tfer == tfer(generic).
+
+:- inst tfer == ground. % XXX
+
+:- mode di_tfer == in. % XXX
+:- mode uo_tfer == out. % XXX
+
+% Constants.
+:- func one = tfer(T).
+:- func zero = tfer(T).
+
+% Conjunction.
+:- func tfer(T) * tfer(T) = tfer(T).
+
+% Disjunction.
+:- func tfer(T) + tfer(T) = tfer(T).
+
+%-----------------------------------------------------------------------------%
+
+:- func var(var(T)::in, tfer(T)::in(tfer)) = (tfer(T)::out(tfer))
+ is det.
+
+:- func not_var(var(T)::in, tfer(T)::in(tfer)) = (tfer(T)::out(tfer))
+ is det.
+
+:- func eq_vars(var(T)::in, var(T)::in, tfer(T)::di_tfer) =
+ (tfer(T)::uo_tfer) is det.
+
+:- func neq_vars(var(T)::in, var(T)::in, tfer(T)::di_tfer) =
+ (tfer(T)::uo_tfer) is det.
+
+:- func imp_vars(var(T)::in, var(T)::in, tfer(T)::di_tfer) =
+ (tfer(T)::uo_tfer) is det.
+
+:- func conj_vars(vars(T)::in, tfer(T)::di_tfer) = (tfer(T)::uo_tfer)
+ is det.
+
+:- func conj_not_vars(vars(T)::in, tfer(T)::di_tfer) =
+ (tfer(T)::uo_tfer) is det.
+
+:- func disj_vars(vars(T)::in, tfer(T)::di_tfer) = (tfer(T)::uo_tfer)
+ is det.
+
+:- func at_most_one_of(vars(T)::in, tfer(T)::di_tfer) =
+ (tfer(T)::uo_tfer) is det.
+
+:- func not_both(var(T)::in, var(T)::in, tfer(T)::di_tfer) =
+ (tfer(T)::uo_tfer) is det.
+
+:- func io_constraint(var(T)::in, var(T)::in, var(T)::in, tfer(T)::di_tfer)
+ = (tfer(T)::uo_tfer) is det.
+
+ % disj_vars_eq(Vars, Var) <=> (disj_vars(Vars) =:= Var).
+:- func disj_vars_eq(vars(T)::in, var(T)::in, tfer(T)::di_tfer) =
+ (tfer(T)::uo_tfer) is det.
+
+:- func var_restrict_true(var(T)::in, tfer(T)::di_tfer) =
+ (tfer(T)::uo_tfer) is det.
+
+:- func var_restrict_false(var(T)::in, tfer(T)::di_tfer) =
+ (tfer(T)::uo_tfer) is det.
+
+%-----------------------------------------------------------------------------%
+
+ % Succeed iff the var is entailed by the xROBDD.
+:- pred var_entailed(tfer(T)::in, var(T)::in) is semidet.
+
+ % Return the set of vars entailed by the xROBDD.
+:- func vars_entailed(tfer(T)) = vars_entailed_result(T).
+
+ % Return the set of vars disentailed by the xROBDD.
+:- func vars_disentailed(tfer(T)) = vars_entailed_result(T).
+
+ % Existentially quantify away the var in the xROBDD.
+:- func restrict(var(T), tfer(T)) = tfer(T).
+
+ % Existentially quantify away all vars greater than the specified var.
+:- func restrict_threshold(var(T), tfer(T)) = tfer(T).
+
+:- func restrict_filter(pred(var(T))::(pred(in) is semidet),
+ tfer(T)::di_tfer) = (tfer(T)::uo_tfer) is det.
+
+%-----------------------------------------------------------------------------%
+
+ % labelling(Vars, xROBDD, TrueVars, FalseVars)
+ % Takes a set of Vars and an xROBDD and returns a value assignment
+ % for those Vars that is a model of the Boolean function
+ % represented by the xROBDD.
+ % The value assignment is returned in the two sets TrueVars (set
+ % of variables assigned the value 1) and FalseVars (set of
+ % variables assigned the value 0).
+ %
+ % XXX should try using sparse_bitset here.
+:- pred labelling(vars(T)::in, tfer(T)::in, vars(T)::out, vars(T)::out)
+ is nondet.
+
+ % minimal_model(Vars, xROBDD, TrueVars, FalseVars)
+ % Takes a set of Vars and an xROBDD and returns a value assignment
+ % for those Vars that is a minimal model of the Boolean function
+ % represented by the xROBDD.
+ % The value assignment is returned in the two sets TrueVars (set
+ % of variables assigned the value 1) and FalseVars (set of
+ % variables assigned the value 0).
+ %
+ % XXX should try using sparse_bitset here.
+:- pred minimal_model(vars(T)::in, tfer(T)::in, vars(T)::out, vars(T)::out)
+ is nondet.
+
+%-----------------------------------------------------------------------------%
+
+% XXX
+% Extract the ROBDD component of the TFER.
+:- func robdd(tfer(T)) = robdd(T).
+
+% Convert the TFER to an ROBDD.
+:- func to_robdd(tfer(T)) = robdd(T).
+
+%-----------------------------------------------------------------------------%
+
+:- implementation.
+
+:- import_module mode_robdd__equiv_vars.
+:- import_module robdd, sparse_bitset, bool, int, list, map.
+
+% T - true vars, F - False Vars, E - equivalent vars, N -
+% non-equivalent vars, R - ROBDD.
+%
+% Combinations to try:
+% R (straight ROBDD)
+% TER (Peter Schachte's extension)
+% TFENR (Everything)
+
+:- type tfer(T)
+ ---> mode_robdd(
+ true_vars :: vars(T),
+ false_vars :: vars(T),
+ equiv_vars :: equiv_vars(T),
+ robdd :: robdd(T)
+ ).
+
+one = mode_robdd(init, init, init_equiv_vars, one).
+
+zero = mode_robdd(init, init, init_equiv_vars, zero).
+
+mode_robdd(TA, FA, EA, RA) * mode_robdd(TB, FB, EB, RB) =
+ normalise(mode_robdd(TA1 `union` TB1, FA1 `union` FB1,
+ EA1 * EB1, RA1 * RB1)) :-
+ TU = TA `union` TB,
+ FU = FA `union` FB,
+ EU = EA * EB,
+ mode_robdd(TA1, FA1, EA1, RA1) = normalise(mode_robdd(TU, FU, EU, RA)),
+ mode_robdd(TB1, FB1, EB1, RB1) = normalise(mode_robdd(TU, FU, EU, RB)).
+
+mode_robdd(TA0, FA0, EA0, RA0) + mode_robdd(TB0, FB0, EB0, RB0) = X :-
+ ( RA0 = zero ->
+ X = mode_robdd(TB0, FB0, EB0, RB0)
+ ; RB0 = zero ->
+ X = mode_robdd(TA0, FA0, EA0, RA0)
+ ;
+ X = mode_robdd(T, F, E, R),
+ T = TA0 `intersect` TB0,
+ F = FA0 `intersect` FB0,
+ E = EA + EB,
+ R = RA + RB,
+
+ TAB = TA0 `difference` TB0,
+ FAB = FA0 `difference` FB0,
+ EA = EA0 ^ add_equalities(TAB) ^ add_equalities(FAB),
+
+ TBA = TB0 `difference` TA0,
+ FBA = FB0 `difference` FA0,
+ EB = EB0 ^ add_equalities(TBA) ^ add_equalities(FBA),
+
+ RA1 = foldl(
+ func(V, R0) = R0 * var(E ^ det_leader(V)), TAB, RA0),
+ RA2 = foldl(
+ func(V, R0) = R0 *
+ not_var(E ^ det_leader(V)), FAB, RA1),
+ EA1 = (EA `difference` EB) + EA0,
+ RA = add_equivalences(EA1, RA2),
+
+ RB1 = foldl(
+ func(V, R0) = R0 * var(E ^ det_leader(V)), TBA, RB0),
+ RB2 = foldl(
+ func(V, R0) = R0 *
+ not_var(E ^ det_leader(V)), FBA, RB1),
+ EB1 = (EB `difference` EA) + EB0,
+ RB = add_equivalences(EB1, RB2)
+ ).
+
+var_entailed(X, V) :-
+ (X ^ robdd = zero ; X ^ true_vars `contains` V).
+
+vars_entailed(X) =
+ (X ^ robdd = zero ->
+ all_vars
+ ;
+ some_vars(X ^ true_vars)
+ ).
+
+vars_disentailed(X) =
+ (X ^ robdd = zero ->
+ all_vars
+ ;
+ some_vars(X ^ false_vars)
+ ).
+
+restrict(V, mode_robdd(T, F, E, R)) =
+ mode_robdd(T `delete` V, F `delete` V, E `delete` V, restrict(V, R)).
+
+restrict_threshold(V, mode_robdd(T, F, E, R)) =
+ mode_robdd(filter(P, T), filter(P, F), restrict_threshold(V, E),
+ restrict_threshold(V, R)) :-
+ P = (pred(U::in) is semidet :- \+ compare((>), U, V)).
+
+var(V, X) =
+ ( T `contains` V ->
+ X
+ ; F `contains` V ->
+ zero
+ ;
+ normalise(mode_robdd(T `insert` V, F, E, R))
+ ) :-
+ X = mode_robdd(T, F, E, R).
+
+not_var(V, X) =
+ ( F `contains` V ->
+ X
+ ; T `contains` V ->
+ zero
+ ;
+ normalise(mode_robdd(T, F `insert` V, E, R))
+ ) :-
+ X = mode_robdd(T, F, E, R).
+
+eq_vars(VarA, VarB, X) =
+ (
+ ( T `contains` VarA, T `contains` VarB
+ ; F `contains` VarA, F `contains` VarB
+ )
+ ->
+ X
+ ;
+ ( T `contains` VarA, F `contains` VarB
+ ; F `contains` VarA, T `contains` VarB
+ )
+ ->
+ zero
+ ;
+ normalise(mode_robdd(T, F, add_equality(VarA, VarB, E), R))
+ ) :-
+ X = mode_robdd(T, F, E, R).
+
+neq_vars(VarA, VarB, X) =
+ (
+ ( T `contains` VarA, T `contains` VarB
+ ; F `contains` VarA, F `contains` VarB
+ )
+ ->
+ zero
+ ;
+ ( T `contains` VarA, F `contains` VarB
+ ; F `contains` VarA, T `contains` VarB
+ )
+ ->
+ X
+ ;
+ X `x` neq_vars(VarA, VarB)
+ ) :-
+ X = mode_robdd(T, F, _E, _R).
+
+imp_vars(VarA, VarB, X) =
+ ( T `contains` VarA, F `contains` VarB ->
+ zero
+ ; T `contains` VarB ->
+ X
+ ; F `contains` VarA ->
+ X
+ ;
+ X `x` imp_vars(VarA, VarB)
+ ) :-
+ X = mode_robdd(T, F, _E, _R).
+
+conj_vars(Vars, X) =
+ ( Vars `subset` T ->
+ X
+ ; \+ empty(Vars `intersect` F) ->
+ zero
+ ;
+ normalise(mode_robdd(T `union` Vars, F, E, R))
+ ) :-
+ X = mode_robdd(T, F, E, R).
+
+conj_not_vars(Vars, X) =
+ ( Vars `subset` F ->
+ X
+ ; \+ empty(Vars `intersect` T) ->
+ zero
+ ;
+ normalise(mode_robdd(T, F `union` Vars, E, R))
+ ) :-
+ X = mode_robdd(T, F, E, R).
+
+disj_vars(Vars, X) =
+ ( \+ empty(Vars `intersect` T) ->
+ X
+ ; Vars `subset` F ->
+ zero
+ ;
+ X `x` disj_vars(Vars)
+ ) :-
+ X = mode_robdd(T, F, _E, _R).
+
+at_most_one_of(Vars, X) =
+ ( count(Vars `difference` F) =< 1 ->
+ X
+ ; count(Vars `intersect` T) > 1 ->
+ zero
+ ;
+ X `x` at_most_one_of(Vars)
+ ) :-
+ X = mode_robdd(T, F, _E, _R).
+
+not_both(VarA, VarB, X) =
+ ( F `contains` VarA ->
+ X
+ ; F `contains` VarB ->
+ X
+ ; T `contains` VarA ->
+ not_var(VarB, X)
+ ; T `contains` VarB ->
+ not_var(VarA, X)
+ ;
+ X `x` (not_var(VarA) + not_var(VarB))
+ ) :-
+ X = mode_robdd(T, F, _E, _R).
+
+io_constraint(V_in, V_out, V_, X) =
+ X ^ not_both(V_in, V_) ^ disj_vars_eq(Vars, V_out) :-
+ Vars = list_to_set([V_in, V_]).
+
+disj_vars_eq(Vars, Var, X) =
+ ( F `contains` Var ->
+ ( Vars `subset` F ->
+ X
+ ;
+ X ^ conj_not_vars(Vars)
+ )
+ ; T `contains` Var ->
+ ( Vars `subset` F ->
+ zero
+ ;
+ X ^ disj_vars(Vars)
+ )
+ ;
+ X `x` (disj_vars(Vars) =:= var(Var))
+ ) :-
+ X = mode_robdd(T, F, _E, _R).
+
+var_restrict_true(V, mode_robdd(T, F, E, R)) = X :-
+ ( F `contains` V ->
+ X = zero
+ ; T `contains` V ->
+ X = mode_robdd(T `delete` V, F, E, R)
+ ;
+ X0 = normalise(mode_robdd(T `insert` V, F, E, R)),
+ X = X0 ^ true_vars := X0 ^ true_vars `delete` V
+ ).
+
+var_restrict_false(V, mode_robdd(T, F, E, R)) = X :-
+ ( T `contains` V ->
+ X = zero
+ ; F `contains` V ->
+ X = mode_robdd(T, F `delete` V, E, R)
+ ;
+ X0 = normalise(mode_robdd(T, F `insert` V, E, R)),
+ X = X0 ^ false_vars := X0 ^ false_vars `delete` V
+ ).
+
+restrict_filter(P, mode_robdd(T, F, E, R)) =
+ mode_robdd(filter(P, T), filter(P, F), filter(P, E), restrict_filter(P, R)).
+
+labelling(Vars0, mode_robdd(T, F, E, R), TrueVars, FalseVars) :-
+ TrueVars0 = T `intersect` Vars0,
+ FalseVars0 = F `intersect` Vars0,
+ Vars = Vars0 `difference` TrueVars0 `difference` FalseVars0,
+
+ ( empty(Vars) ->
+ TrueVars = TrueVars0,
+ FalseVars = FalseVars0
+ ;
+ labelling_2(Vars, mode_robdd(init, init, E, R),
+ TrueVars1, FalseVars1),
+ TrueVars = TrueVars0 `union` TrueVars1,
+ FalseVars = FalseVars0 `union` FalseVars1
+ ).
+
+:- pred labelling_2(vars(T)::in, tfer(T)::in, vars(T)::out, vars(T)::out)
+ is nondet.
+
+labelling_2(Vars0, X0, TrueVars, FalseVars) :-
+ ( remove_least(Vars0, V, Vars) ->
+ (
+ X = var_restrict_false(V, X0),
+ X ^ robdd \= zero,
+ labelling_2(Vars, X, TrueVars, FalseVars0),
+ FalseVars = FalseVars0 `insert` V
+ ;
+ X = var_restrict_true(V, X0),
+ X ^ robdd \= zero,
+ labelling_2(Vars, X, TrueVars0, FalseVars),
+ TrueVars = TrueVars0 `insert` V
+ )
+ ;
+ TrueVars = init,
+ FalseVars = init
+ ).
+
+minimal_model(Vars, X0, TrueVars, FalseVars) :-
+ ( empty(Vars) ->
+ TrueVars = init,
+ FalseVars = init
+ ;
+ minimal_model_2(Vars, X0, TrueVars0, FalseVars0),
+ (
+ TrueVars = TrueVars0,
+ FalseVars = FalseVars0
+ ;
+ X = X0 `x` (~conj_vars(TrueVars0)),
+ minimal_model(Vars, X, TrueVars, FalseVars)
+ )
+ ).
+
+:- pred minimal_model_2(vars(T)::in, tfer(T)::in, vars(T)::out, vars(T)::out)
+ is semidet.
+
+minimal_model_2(Vars0, X0, TrueVars, FalseVars) :-
+ ( remove_least(Vars0, V, Vars) ->
+ X1 = var_restrict_false(V, X0),
+ ( X1 ^ robdd \= zero ->
+ minimal_model_2(Vars, X1, TrueVars, FalseVars0),
+ FalseVars = FalseVars0 `insert` V
+ ;
+ X2 = var_restrict_true(V, X0),
+ X2 ^ robdd \= zero,
+ minimal_model_2(Vars, X2, TrueVars0, FalseVars),
+ TrueVars = TrueVars0 `insert` V
+ )
+ ;
+ TrueVars = init,
+ FalseVars = init
+ ).
+
+%-----------------------------------------------------------------------------%
+
+:- func normalise(tfer(T)::di_tfer) = (tfer(T)::uo_tfer) is det.
+
+normalise(mode_robdd(TrueVars0, FalseVars0, EQVars0, Robdd0)) = X :-
+ %( some [V] (V `member` TrueVars0, V `member` FalseVars0) ->
+ ( \+ empty(TrueVars0 `intersect` FalseVars0) ->
+ X = zero
+ ;
+ % Lines 4, 5
+ normalise_true_false_equivalent_vars(Changed0, TrueVars0,
+ TrueVars1, FalseVars0, FalseVars1, EQVars0, EQVars1),
+
+ % Line 6
+ Robdd1 = restrict_true_false_vars(TrueVars1, FalseVars1,
+ Robdd0),
+ Changed1 = Changed0 `bool__or` ( Robdd1 \= Robdd0 -> yes ; no),
+
+ % Line 7
+ (
+ definite_vars(Robdd1,
+ some_vars(NewTrueVars), some_vars(NewFalseVars))
+ ->
+ (
+ empty(NewTrueVars),
+ empty(NewFalseVars)
+ ->
+ Changed2 = Changed1,
+ TrueVars2 = TrueVars1,
+ FalseVars2 = FalseVars1
+ ;
+ Changed2 = yes,
+ TrueVars2 = TrueVars1 `union` NewTrueVars,
+ FalseVars2 = FalseVars1 `union` NewFalseVars
+ ),
+
+ % Lines 8, 9, 10
+ extract_equivalent_vars_from_robdd(Changed3, Robdd1,
+ Robdd2, EQVars1, EQVars2),
+ Changed = Changed2 `bool__or` Changed3,
+
+ % Line 11
+ X0 = mode_robdd(TrueVars2, FalseVars2, EQVars2, Robdd2),
+ X = ( Changed = yes ->
+ normalise(X0)
+ ;
+ X0
+ )
+ ;
+ X = zero
+ )
+ ).
+
+:- pred normalise_true_false_equivalent_vars(bool::out, vars(T)::in,
+ vars(T)::out, vars(T)::in, vars(T)::out, equiv_vars(T)::in,
+ equiv_vars(T)::out) is det.
+
+normalise_true_false_equivalent_vars(Changed, T0, T, F0, F) -->
+ normalise_known_equivalent_vars(Changed0, T0, T),
+ normalise_known_equivalent_vars(Changed1, F0, F),
+ { Changed = Changed0 `bool__or` Changed1 }.
+
+:- pred extract_equivalent_vars_from_robdd(bool::out, robdd(T)::in,
+ robdd(T)::out, equiv_vars(T)::in, equiv_vars(T)::out) is det.
+
+extract_equivalent_vars_from_robdd(Changed, Robdd0, Robdd, EQVars0, EQVars) :-
+ ( RobddEQVars = equivalent_vars_in_robdd(Robdd0) ->
+ ( empty(RobddEQVars) ->
+ Changed0 = no,
+ Robdd1 = Robdd0,
+ EQVars = EQVars0
+ ;
+ Changed0 = yes,
+
+ % Remove any equalities we have just found from the
+ % ROBDD.
+ Robdd1 = squeeze_equiv(RobddEQVars, Robdd0),
+
+ EQVars = EQVars0 * RobddEQVars
+ )
+ ;
+ EQVars = init_equiv_vars,
+ Changed0 = ( EQVars = EQVars0 -> no ; yes ),
+ Robdd1 = Robdd0
+ ),
+
+ % Remove any other equalities from the ROBDD.
+ % Note that we can use EQVars0 here since we have already removed the
+ % equivalences in RobddEQVars using squeeze_equiv.
+ Robdd = remove_equiv(EQVars0, Robdd1),
+ Changed = Changed0 `bool__or` ( Robdd \= Robdd1 -> yes ; no ).
+
+:- func x(tfer(T)::di_tfer, robdd(T)::in) = (tfer(T)::uo_tfer) is det.
+
+x(X, R) = X * mode_robdd(init, init, init_equiv_vars, R).
+
+%---------------------------------------------------------------------------%
+
+% to_robdd(X) = expand_equiv(X ^ equiv_vars,
+% X ^ robdd * conj_vars(X ^ true_vars)
+% * conj_not_vars(X ^ false_vars)).
+
+to_robdd(X) = map__foldl(func(A, B, R) = R * eq_vars(A, B),
+ X ^ equiv_vars ^ leader_map,
+ X ^ robdd * conj_vars(X ^ true_vars)
+ * conj_not_vars(X ^ false_vars)).
+
+%---------------------------------------------------------------------------%
Index: compiler/mode_robdd.tfern.m
===================================================================
RCS file: compiler/mode_robdd.tfern.m
diff -N compiler/mode_robdd.tfern.m
--- /dev/null 1 Jan 1970 00:00:00 -0000
+++ compiler/mode_robdd.tfern.m 19 May 2003 08:21:03 -0000
@@ -0,0 +1,387 @@
+%---------------------------------------------------------------------------%
+% Copyright (C) 2001-2003 The University of Melbourne.
+% 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.tfern.m.
+% Main author: dmo
+% Stability: low
+
+%-----------------------------------------------------------------------------%
+
+:- module mode_robdd__tfern.
+
+:- interface.
+
+:- import_module term, robdd.
+
+:- type mode_robdd(T).
+:- type mode_robdd == mode_robdd(generic).
+
+:- inst mode_robdd == ground. % XXX
+
+:- mode di_mode_robdd == in. % XXX
+:- mode uo_mode_robdd == out. % XXX
+
+% Constants.
+:- func one = mode_robdd(T).
+:- func zero = mode_robdd(T).
+
+% Conjunction.
+:- func mode_robdd(T) * mode_robdd(T) = mode_robdd(T).
+
+% Disjunction.
+:- func mode_robdd(T) + mode_robdd(T) = mode_robdd(T).
+
+%-----------------------------------------------------------------------------%
+
+:- func var(var(T)::in, mode_robdd(T)::in(mode_robdd)) =
+ (mode_robdd(T)::out(mode_robdd)) is det.
+
+:- func not_var(var(T)::in, mode_robdd(T)::in(mode_robdd)) =
+ (mode_robdd(T)::out(mode_robdd)) is det.
+
+:- func eq_vars(var(T)::in, var(T)::in, mode_robdd(T)::di_mode_robdd) =
+ (mode_robdd(T)::uo_mode_robdd) is det.
+
+:- func neq_vars(var(T)::in, var(T)::in, mode_robdd(T)::di_mode_robdd) =
+ (mode_robdd(T)::uo_mode_robdd) is det.
+
+:- func imp_vars(var(T)::in, var(T)::in, mode_robdd(T)::di_mode_robdd) =
+ (mode_robdd(T)::uo_mode_robdd) is det.
+
+:- func conj_vars(vars(T)::in, mode_robdd(T)::di_mode_robdd) =
+ (mode_robdd(T)::uo_mode_robdd) is det.
+
+:- func conj_not_vars(vars(T)::in, mode_robdd(T)::di_mode_robdd) =
+ (mode_robdd(T)::uo_mode_robdd) is det.
+
+:- func disj_vars(vars(T)::in, mode_robdd(T)::di_mode_robdd) =
+ (mode_robdd(T)::uo_mode_robdd) is det.
+
+:- func at_most_one_of(vars(T)::in, mode_robdd(T)::di_mode_robdd) =
+ (mode_robdd(T)::uo_mode_robdd) is det.
+
+:- func not_both(var(T)::in, var(T)::in, mode_robdd(T)::di_mode_robdd) =
+ (mode_robdd(T)::uo_mode_robdd) is det.
+
+:- func io_constraint(var(T)::in, var(T)::in, var(T)::in,
+ mode_robdd(T)::di_mode_robdd) = (mode_robdd(T)::uo_mode_robdd) is det.
+
+ % disj_vars_eq(Vars, Var) <=> (disj_vars(Vars) =:= Var).
+:- func disj_vars_eq(vars(T)::in, var(T)::in, mode_robdd(T)::di_mode_robdd) =
+ (mode_robdd(T)::uo_mode_robdd) is det.
+
+:- func var_restrict_true(var(T)::in, mode_robdd(T)::di_mode_robdd) =
+ (mode_robdd(T)::uo_mode_robdd) is det.
+
+:- func var_restrict_false(var(T)::in, mode_robdd(T)::di_mode_robdd) =
+ (mode_robdd(T)::uo_mode_robdd) is det.
+
+%-----------------------------------------------------------------------------%
+
+ % Succeed iff the var is entailed by the xROBDD.
+:- pred var_entailed(mode_robdd(T)::in, var(T)::in) is semidet.
+
+ % Return the set of vars entailed by the xROBDD.
+:- func vars_entailed(mode_robdd(T)) = vars_entailed_result(T).
+
+ % Return the set of vars disentailed by the xROBDD.
+:- func vars_disentailed(mode_robdd(T)) = vars_entailed_result(T).
+
+ % Existentially quantify away the var in the xROBDD.
+:- func restrict(var(T), mode_robdd(T)) = mode_robdd(T).
+
+ % Existentially quantify away all vars greater than the specified var.
+:- func restrict_threshold(var(T), mode_robdd(T)) = mode_robdd(T).
+
+:- func restrict_filter(pred(var(T))::(pred(in) is semidet),
+ mode_robdd(T)::di_mode_robdd) = (mode_robdd(T)::uo_mode_robdd) is det.
+
+%-----------------------------------------------------------------------------%
+
+ % labelling(Vars, xROBDD, TrueVars, FalseVars)
+ % Takes a set of Vars and an xROBDD and returns a value assignment
+ % for those Vars that is a model of the Boolean function
+ % represented by the xROBDD.
+ % The value assignment is returned in the two sets TrueVars (set
+ % of variables assigned the value 1) and FalseVars (set of
+ % variables assigned the value 0).
+ %
+ % XXX should try using sparse_bitset here.
+:- pred labelling(vars(T)::in, mode_robdd(T)::in, vars(T)::out, vars(T)::out)
+ is nondet.
+
+ % minimal_model(Vars, xROBDD, TrueVars, FalseVars)
+ % Takes a set of Vars and an xROBDD and returns a value assignment
+ % for those Vars that is a minimal model of the Boolean function
+ % represented by the xROBDD.
+ % The value assignment is returned in the two sets TrueVars (set
+ % of variables assigned the value 1) and FalseVars (set of
+ % variables assigned the value 0).
+ %
+ % XXX should try using sparse_bitset here.
+:- pred minimal_model(vars(T)::in, mode_robdd(T)::in, vars(T)::out,
+ vars(T)::out) is nondet.
+
+%-----------------------------------------------------------------------------%
+
+:- implementation.
+
+:- import_module robdd, sparse_bitset, bool, int.
+
+% T - true vars, F - False Vars, E - equivalent vars, N -
+% non-equivalent vars, R - ROBDD.
+%
+% Combinations to try:
+% R (straight ROBDD)
+% TER (Peter Schachte's extension)
+% TFENR (Everything)
+
+:- type mode_robdd(T)
+ ---> mode_robdd(
+ true_vars :: vars(T),
+ false_vars :: vars(T),
+ robdd :: robdd(T)
+ ).
+
+one = mode_robdd(init, init, one).
+
+zero = mode_robdd(init, init, zero).
+
+mode_robdd(TA, FA, RA) * mode_robdd(TB, FB, RB) =
+ normalise(mode_robdd(TA `union` TB, FA `union` FB, RA * RB)).
+
+mode_robdd(TA, FA, RA0) + mode_robdd(TB, FB, RB0) = X :-
+ ( RA0 = zero ->
+ X = mode_robdd(TB, FB, RB0)
+ ; RB0 = zero ->
+ X = mode_robdd(TA, FA, RA0)
+ ;
+ RA = RA0 * conj_vars(TA `difference` TB) *
+ conj_not_vars(FA `difference` FB),
+ RB = RB0 * conj_vars(TB `difference` TA) *
+ conj_not_vars(FB `difference` FA),
+ X = mode_robdd(TA `intersect` TB, FA `intersect` FB, RA + RB)
+ ).
+
+var_entailed(X, V) :-
+ (X ^ robdd = zero ; X ^ true_vars `contains` V).
+
+vars_entailed(X) =
+ (X ^ robdd = zero ->
+ all_vars
+ ;
+ some_vars(X ^ true_vars)
+ ).
+
+vars_disentailed(X) =
+ (X ^ robdd = zero ->
+ all_vars
+ ;
+ some_vars(X ^ false_vars)
+ ).
+
+restrict(V, mode_robdd(T, F, R)) =
+ mode_robdd(T `delete` V, F `delete` V, restrict(V, R)).
+
+restrict_threshold(V, mode_robdd(T, F, R)) =
+ mode_robdd(filter(P, T), filter(P, F),
+ restrict_threshold(V, R)) :-
+ P = (pred(U::in) is semidet :- \+ compare((>), U, V)).
+
+var(V, X) =
+ ( T `contains` V ->
+ X
+ ; F `contains` V ->
+ zero
+ ;
+ normalise(mode_robdd(T `insert` V, F, R))
+ ) :-
+ X = mode_robdd(T, F, R).
+
+not_var(V, X) =
+ ( F `contains` V ->
+ X
+ ; T `contains` V ->
+ zero
+ ;
+ normalise(mode_robdd(T, F `insert` V, R))
+ ) :-
+ X = mode_robdd(T, F, R).
+
+eq_vars(VarA, VarB, X) =
+ (
+ ( T `contains` VarA, T `contains` VarB
+ ; F `contains` VarA, F `contains` VarB
+ )
+ ->
+ X
+ ;
+ ( T `contains` VarA, F `contains` VarB
+ ; F `contains` VarA, T `contains` VarB
+ )
+ ->
+ zero
+ ;
+ normalise(mode_robdd(T, F, R * eq_vars(VarA, VarB)))
+ ) :-
+ X = mode_robdd(T, F, R).
+
+neq_vars(VarA, VarB, X) =
+ (
+ ( T `contains` VarA, T `contains` VarB
+ ; F `contains` VarA, F `contains` VarB
+ )
+ ->
+ zero
+ ;
+ ( T `contains` VarA, F `contains` VarB
+ ; F `contains` VarA, T `contains` VarB
+ )
+ ->
+ X
+ ;
+ normalise(mode_robdd(T, F, R * neq_vars(VarA, VarB)))
+ ) :-
+ X = mode_robdd(T, F, R).
+
+imp_vars(VarA, VarB, X) =
+ ( T `contains` VarA, F `contains` VarB ->
+ zero
+ ; T `contains` VarB ->
+ X
+ ; F `contains` VarA ->
+ X
+ ;
+ normalise(mode_robdd(T, F, R * imp_vars(VarA, VarB)))
+ ) :-
+ X = mode_robdd(T, F, R).
+
+conj_vars(Vars, X) =
+ ( Vars `subset` T ->
+ X
+ ; \+ empty(Vars `intersect` F) ->
+ zero
+ ;
+ normalise(mode_robdd(T `union` Vars, F, R))
+ ) :-
+ X = mode_robdd(T, F, R).
+
+conj_not_vars(Vars, X) =
+ ( Vars `subset` F ->
+ X
+ ; \+ empty(Vars `intersect` T) ->
+ zero
+ ;
+ normalise(mode_robdd(T, F `union` Vars, R))
+ ) :-
+ X = mode_robdd(T, F, R).
+
+disj_vars(Vars, mode_robdd(T, F, R)) =
+ ( \+ empty(Vars `intersect` T) ->
+ mode_robdd(T, F, R)
+ ; Vars `subset` F ->
+ zero
+ ;
+ normalise(mode_robdd(T, F, R * disj_vars(Vars)))
+ ).
+
+at_most_one_of(Vars, X) =
+ ( count(Vars `difference` F) =< 1 ->
+ X
+ ; count(Vars `intersect` T) > 1 ->
+ zero
+ ;
+ normalise(mode_robdd(T, F, R * at_most_one_of(Vars)))
+ ) :-
+ X = mode_robdd(T, F, R).
+
+not_both(VarA, VarB, X) =
+ normalise(X ^ robdd := X ^ robdd * ~(var(VarA) * var(VarB))).
+
+io_constraint(V_in, V_out, V_, X) =
+ normalise(X ^ robdd :=
+ X ^ robdd *
+ ( var(V_out) =:= var(V_in) + var(V_) ) *
+ ( ~(var(V_in) * var(V_)) )).
+
+disj_vars_eq(Vars, Var, X) =
+ ( F `contains` Var ->
+ ( Vars `subset` F ->
+ X
+ ;
+ X ^ conj_not_vars(Vars)
+ )
+ ; T `contains` Var ->
+ ( Vars `subset` F ->
+ zero
+ ;
+ X ^ disj_vars(Vars)
+ )
+ ;
+ normalise(mode_robdd(T, F, R * (disj_vars(Vars) =:= var(Var))))
+ ) :-
+ X = mode_robdd(T, F, R).
+
+var_restrict_true(V, mode_robdd(T, F, R)) =
+ ( F `contains` V ->
+ zero
+ ; T `contains` V ->
+ mode_robdd(T `delete` V, F, R)
+ ;
+ normalise(mode_robdd(T, F, var_restrict_true(V, R)))
+ ).
+
+var_restrict_false(V, mode_robdd(T, F, R)) =
+ ( T `contains` V ->
+ zero
+ ; F `contains` V ->
+ mode_robdd(T, F `delete` V, R)
+ ;
+ normalise(mode_robdd(T, F, var_restrict_false(V, R)))
+ ).
+
+restrict_filter(P, mode_robdd(T, F, R)) =
+ mode_robdd(filter(P, T), filter(P, F), restrict_filter(P, R)).
+
+labelling(Vars, mode_robdd(T, F, R), TrueVars `intersect` Vars `union` T,
+ FalseVars `intersect` Vars `union` F) :-
+ labelling(Vars, R, TrueVars, FalseVars).
+
+minimal_model(Vars, mode_robdd(T, F, R), TrueVars `intersect` Vars `union` T,
+ FalseVars `intersect` Vars `union` F) :-
+ minimal_model(Vars, R, TrueVars, FalseVars).
+
+%-----------------------------------------------------------------------------%
+
+:- func normalise(mode_robdd(T)::di_mode_robdd) =
+ (mode_robdd(T)::uo_mode_robdd) is det.
+
+normalise(mode_robdd(TrueVars0, FalseVars0, Robdd0)) = X :-
+ % ( some [V] (V `member` TrueVars0, V `member` FalseVars0) ->
+ ( \+ empty(TrueVars0 `intersect` FalseVars0) ->
+ X = zero
+ ;
+ Robdd1 = restrict_true_false_vars(TrueVars0, FalseVars0,
+ Robdd0),
+ (
+ definite_vars(Robdd1,
+ some_vars(TrueVars1), some_vars(FalseVars1))
+ ->
+ (
+ empty(TrueVars1),
+ empty(FalseVars1)
+ ->
+ X = mode_robdd(TrueVars0, FalseVars0, Robdd1)
+ ;
+ X = mode_robdd(TrueVars0 `union` TrueVars1,
+ FalseVars0 `union` FalseVars1,
+ restrict_true_false_vars(TrueVars1,
+ FalseVars1, Robdd1))
+ )
+ ;
+ X = zero
+ )
+ ).
Index: compiler/mode_robdd.tfr.m
===================================================================
RCS file: compiler/mode_robdd.tfr.m
diff -N compiler/mode_robdd.tfr.m
--- /dev/null 1 Jan 1970 00:00:00 -0000
+++ compiler/mode_robdd.tfr.m 19 May 2003 08:21:10 -0000
@@ -0,0 +1,413 @@
+%---------------------------------------------------------------------------%
+% Copyright (C) 2001-2003 The University of Melbourne.
+% 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.tfr.m.
+% Main author: dmo
+% Stability: low
+
+%-----------------------------------------------------------------------------%
+
+:- module mode_robdd__tfr.
+
+:- interface.
+
+:- import_module term, robdd.
+
+:- type tfr(T).
+:- type tfr == tfr(generic).
+
+:- inst tfr == ground. % XXX
+
+:- mode di_tfr == in. % XXX
+:- mode uo_tfr == out. % XXX
+
+% Constants.
+:- func one = tfr(T).
+:- func zero = tfr(T).
+
+% Conjunction.
+:- func tfr(T) * tfr(T) = tfr(T).
+
+% Disjunction.
+:- func tfr(T) + tfr(T) = tfr(T).
+
+%-----------------------------------------------------------------------------%
+
+:- func var(var(T)::in, tfr(T)::in(tfr)) = (tfr(T)::out(tfr))
+ is det.
+
+:- func not_var(var(T)::in, tfr(T)::in(tfr)) = (tfr(T)::out(tfr))
+ is det.
+
+:- func eq_vars(var(T)::in, var(T)::in, tfr(T)::di_tfr) =
+ (tfr(T)::uo_tfr) is det.
+
+:- func neq_vars(var(T)::in, var(T)::in, tfr(T)::di_tfr) =
+ (tfr(T)::uo_tfr) is det.
+
+:- func imp_vars(var(T)::in, var(T)::in, tfr(T)::di_tfr) =
+ (tfr(T)::uo_tfr) is det.
+
+:- func conj_vars(vars(T)::in, tfr(T)::di_tfr) = (tfr(T)::uo_tfr)
+ is det.
+
+:- func conj_not_vars(vars(T)::in, tfr(T)::di_tfr) =
+ (tfr(T)::uo_tfr) is det.
+
+:- func disj_vars(vars(T)::in, tfr(T)::di_tfr) = (tfr(T)::uo_tfr)
+ is det.
+
+:- func at_most_one_of(vars(T)::in, tfr(T)::di_tfr) =
+ (tfr(T)::uo_tfr) is det.
+
+:- func not_both(var(T)::in, var(T)::in, tfr(T)::di_tfr) =
+ (tfr(T)::uo_tfr) is det.
+
+:- func io_constraint(var(T)::in, var(T)::in, var(T)::in, tfr(T)::di_tfr)
+ = (tfr(T)::uo_tfr) is det.
+
+ % disj_vars_eq(Vars, Var) <=> (disj_vars(Vars) =:= Var).
+:- func disj_vars_eq(vars(T)::in, var(T)::in, tfr(T)::di_tfr) =
+ (tfr(T)::uo_tfr) is det.
+
+:- func var_restrict_true(var(T)::in, tfr(T)::di_tfr) =
+ (tfr(T)::uo_tfr) is det.
+
+:- func var_restrict_false(var(T)::in, tfr(T)::di_tfr) =
+ (tfr(T)::uo_tfr) is det.
+
+%-----------------------------------------------------------------------------%
+
+ % Succeed iff the var is entailed by the xROBDD.
+:- pred var_entailed(tfr(T)::in, var(T)::in) is semidet.
+
+ % Return the set of vars entailed by the xROBDD.
+:- func vars_entailed(tfr(T)) = vars_entailed_result(T).
+
+ % Return the set of vars disentailed by the xROBDD.
+:- func vars_disentailed(tfr(T)) = vars_entailed_result(T).
+
+ % Existentially quantify away the var in the xROBDD.
+:- func restrict(var(T), tfr(T)) = tfr(T).
+
+ % Existentially quantify away all vars greater than the specified var.
+:- func restrict_threshold(var(T), tfr(T)) = tfr(T).
+
+:- func restrict_filter(pred(var(T))::(pred(in) is semidet),
+ tfr(T)::di_tfr) = (tfr(T)::uo_tfr) is det.
+
+%-----------------------------------------------------------------------------%
+
+ % labelling(Vars, xROBDD, TrueVars, FalseVars)
+ % Takes a set of Vars and an xROBDD and returns a value assignment
+ % for those Vars that is a model of the Boolean function
+ % represented by the xROBDD.
+ % The value assignment is returned in the two sets TrueVars (set
+ % of variables assigned the value 1) and FalseVars (set of
+ % variables assigned the value 0).
+ %
+ % XXX should try using sparse_bitset here.
+:- pred labelling(vars(T)::in, tfr(T)::in, vars(T)::out, vars(T)::out)
+ is nondet.
+
+ % minimal_model(Vars, xROBDD, TrueVars, FalseVars)
+ % Takes a set of Vars and an xROBDD and returns a value assignment
+ % for those Vars that is a minimal model of the Boolean function
+ % represented by the xROBDD.
+ % The value assignment is returned in the two sets TrueVars (set
+ % of variables assigned the value 1) and FalseVars (set of
+ % variables assigned the value 0).
+ %
+ % XXX should try using sparse_bitset here.
+:- pred minimal_model(vars(T)::in, tfr(T)::in, vars(T)::out, vars(T)::out)
+ is nondet.
+%-----------------------------------------------------------------------------%
+
+% XXX
+:- func robdd(tfr(T)) = robdd(T).
+
+%-----------------------------------------------------------------------------%
+
+:- implementation.
+
+:- import_module robdd, sparse_bitset, bool, int, list.
+
+% T - true vars, F - False Vars, E - equivalent vars, N -
+% non-equivalent vars, R - ROBDD.
+%
+% Combinations to try:
+% R (straight ROBDD)
+% TER (Peter Schachte's extension)
+% TFENR (Everything)
+
+:- type tfr(T)
+ ---> mode_robdd(
+ true_vars :: vars(T),
+ false_vars :: vars(T),
+ robdd :: robdd(T)
+ ).
+
+one = mode_robdd(init, init, one).
+
+zero = mode_robdd(init, init, zero).
+
+mode_robdd(TA, FA, RA) * mode_robdd(TB, FB, RB) =
+ normalise(mode_robdd(TA1 `union` TB1, FA1 `union` FB1, RA1 * RB1)) :-
+
+ TU = TA `union` TB,
+ FU = FA `union` FB,
+ mode_robdd(TA1, FA1, RA1) = normalise(mode_robdd(TU, FU, RA)),
+ mode_robdd(TB1, FB1, RB1) = normalise(mode_robdd(TU, FU, RB)).
+
+mode_robdd(TA, FA, RA0) + mode_robdd(TB, FB, RB0) = X :-
+ ( RA0 = zero ->
+ X = mode_robdd(TB, FB, RB0)
+ ; RB0 = zero ->
+ X = mode_robdd(TA, FA, RA0)
+ ;
+ RA = RA0 * conj_vars(TA `difference` TB) *
+ conj_not_vars(FA `difference` FB),
+ RB = RB0 * conj_vars(TB `difference` TA) *
+ conj_not_vars(FB `difference` FA),
+ X = mode_robdd(TA `intersect` TB, FA `intersect` FB, RA + RB)
+ ).
+
+var_entailed(X, V) :-
+ (X ^ robdd = zero ; X ^ true_vars `contains` V).
+
+vars_entailed(X) =
+ (X ^ robdd = zero ->
+ all_vars
+ ;
+ some_vars(X ^ true_vars)
+ ).
+
+vars_disentailed(X) =
+ (X ^ robdd = zero ->
+ all_vars
+ ;
+ some_vars(X ^ false_vars)
+ ).
+
+restrict(V, mode_robdd(T, F, R)) =
+ mode_robdd(T `delete` V, F `delete` V, restrict(V, R)).
+
+restrict_threshold(V, mode_robdd(T, F, R)) =
+ mode_robdd(filter(P, T), filter(P, F), restrict_threshold(V, R)) :-
+ P = (pred(U::in) is semidet :- \+ compare((>), U, V)).
+
+var(V, X) =
+ ( T `contains` V ->
+ X
+ ; F `contains` V ->
+ zero
+ ;
+ normalise(mode_robdd(T `insert` V, F, R))
+ ) :-
+ X = mode_robdd(T, F, R).
+
+not_var(V, X) =
+ ( F `contains` V ->
+ X
+ ; T `contains` V ->
+ zero
+ ;
+ normalise(mode_robdd(T, F `insert` V, R))
+ ) :-
+ X = mode_robdd(T, F, R).
+
+eq_vars(VarA, VarB, X) =
+ (
+ ( T `contains` VarA, T `contains` VarB
+ ; F `contains` VarA, F `contains` VarB
+ )
+ ->
+ X
+ ;
+ ( T `contains` VarA, F `contains` VarB
+ ; F `contains` VarA, T `contains` VarB
+ )
+ ->
+ zero
+ ;
+ X `x` eq_vars(VarA, VarB)
+ ) :-
+ X = mode_robdd(T, F, _R).
+
+neq_vars(VarA, VarB, X) =
+ (
+ ( T `contains` VarA, T `contains` VarB
+ ; F `contains` VarA, F `contains` VarB
+ )
+ ->
+ zero
+ ;
+ ( T `contains` VarA, F `contains` VarB
+ ; F `contains` VarA, T `contains` VarB
+ )
+ ->
+ X
+ ;
+ X `x` neq_vars(VarA, VarB)
+ ) :-
+ X = mode_robdd(T, F, _R).
+
+imp_vars(VarA, VarB, X) =
+ ( T `contains` VarA, F `contains` VarB ->
+ zero
+ ; T `contains` VarB ->
+ X
+ ; F `contains` VarA ->
+ X
+ ;
+ X `x` imp_vars(VarA, VarB)
+ ) :-
+ X = mode_robdd(T, F, _R).
+
+conj_vars(Vars, X) =
+ ( Vars `subset` T ->
+ X
+ ; \+ empty(Vars `intersect` F) ->
+ zero
+ ;
+ normalise(mode_robdd(T `union` Vars, F, R))
+ ) :-
+ X = mode_robdd(T, F, R).
+
+conj_not_vars(Vars, X) =
+ ( Vars `subset` F ->
+ X
+ ; \+ empty(Vars `intersect` T) ->
+ zero
+ ;
+ normalise(mode_robdd(T, F `union` Vars, R))
+ ) :-
+ X = mode_robdd(T, F, R).
+
+disj_vars(Vars, X) =
+ ( \+ empty(Vars `intersect` T) ->
+ X
+ ; Vars `subset` F ->
+ zero
+ ;
+ X `x` disj_vars(Vars)
+ ) :-
+ X = mode_robdd(T, F, _R).
+
+at_most_one_of(Vars, X) =
+ ( count(Vars `difference` F) =< 1 ->
+ X
+ ; count(Vars `intersect` T) > 1 ->
+ zero
+ ;
+ X `x` at_most_one_of(Vars)
+ ) :-
+ X = mode_robdd(T, F, _R).
+
+/*
+not_both(VarA, VarB, X) =
+ normalise(X ^ robdd := X ^ robdd * ~(var(VarA) * var(VarB))).
+*/
+not_both(VarA, VarB, X) =
+ ( F `contains` VarA ->
+ X
+ ; F `contains` VarB ->
+ X
+ ; T `contains` VarA ->
+ not_var(VarB, X)
+ ; T `contains` VarB ->
+ not_var(VarA, X)
+ ;
+ X `x` (not_var(VarA) + not_var(VarB))
+ ) :-
+ X = mode_robdd(T, F, _R).
+
+io_constraint(V_in, V_out, V_, X) =
+ X ^ not_both(V_in, V_) ^ disj_vars_eq(Vars, V_out) :-
+ Vars = list_to_set([V_in, V_]).
+
+disj_vars_eq(Vars, Var, X) =
+ ( F `contains` Var ->
+ ( Vars `subset` F ->
+ X
+ ;
+ X ^ conj_not_vars(Vars)
+ )
+ ; T `contains` Var ->
+ ( Vars `subset` F ->
+ zero
+ ;
+ X ^ disj_vars(Vars)
+ )
+ ;
+ X `x` (disj_vars(Vars) =:= var(Var))
+ ) :-
+ X = mode_robdd(T, F, _R).
+
+var_restrict_true(V, mode_robdd(T, F, R)) =
+ ( F `contains` V ->
+ zero
+ ; T `contains` V ->
+ mode_robdd(T `delete` V, F, R)
+ ;
+ normalise(mode_robdd(T, F, var_restrict_true(V, R)))
+ ).
+
+var_restrict_false(V, mode_robdd(T, F, R)) =
+ ( T `contains` V ->
+ zero
+ ; F `contains` V ->
+ mode_robdd(T, F `delete` V, R)
+ ;
+ normalise(mode_robdd(T, F, var_restrict_false(V, R)))
+ ).
+
+restrict_filter(P, mode_robdd(T, F, R)) =
+ mode_robdd(filter(P, T), filter(P, F), restrict_filter(P, R)).
+
+labelling(Vars, mode_robdd(T, F, R), T `intersect` Vars `union` TrueVars,
+ F `intersect` Vars `union` FalseVars) :-
+ labelling(Vars `difference` T `difference` F, R, TrueVars, FalseVars).
+
+minimal_model(Vars, mode_robdd(T, F, R), T `intersect` Vars `union` TrueVars,
+ F `intersect` Vars `union` FalseVars) :-
+ minimal_model(Vars `difference` T `difference` F, R,
+ TrueVars, FalseVars).
+
+%-----------------------------------------------------------------------------%
+
+:- func normalise(tfr(T)::di_tfr) = (tfr(T)::uo_tfr) is det.
+
+normalise(mode_robdd(TrueVars0, FalseVars0, Robdd0)) = X :-
+ %( some [V] (V `member` TrueVars0, V `member` FalseVars0) ->
+ ( \+ empty(TrueVars0 `intersect` FalseVars0) ->
+ X = zero
+ ;
+ Robdd1 = restrict_true_false_vars(TrueVars0, FalseVars0,
+ Robdd0),
+ (
+ definite_vars(Robdd1,
+ some_vars(TrueVars1), some_vars(FalseVars1))
+ ->
+ (
+ empty(TrueVars1),
+ empty(FalseVars1)
+ ->
+ X = mode_robdd(TrueVars0, FalseVars0, Robdd1)
+ ;
+ X = mode_robdd(TrueVars0 `union` TrueVars1,
+ FalseVars0 `union` FalseVars1,
+ restrict_true_false_vars(TrueVars1,
+ FalseVars1, Robdd1))
+ )
+ ;
+ X = zero
+ )
+ ).
+
+:- func x(tfr(T)::di_tfr, robdd(T)::in) = (tfr(T)::uo_tfr) is det.
+
+x(X, R) = X * mode_robdd(init, init, R).
Index: compiler/options.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/options.m,v
retrieving revision 1.437
diff -u -b -r1.437 options.m
--- compiler/options.m 30 Nov 2004 06:54:32 -0000 1.437
+++ compiler/options.m 6 Dec 2004 05:02:46 -0000
@@ -171,6 +171,10 @@
; generate_schemas
; dump_rl
; dump_rl_bytecode
+ ; mode_constraints
+ ; simple_mode_constraints
+ ; benchmark_modes
+ ; benchmark_modes_repeat
; sign_assembly
; separate_assemblies
% Language semantics options
@@ -835,6 +839,10 @@
verbose_dump_mlds - accumulating([]),
dump_rl - bool(no),
dump_rl_bytecode - bool(no),
+ mode_constraints - bool(no),
+ simple_mode_constraints - bool(no),
+ benchmark_modes - bool(no),
+ benchmark_modes_repeat - int(1),
sign_assembly - bool(no),
% XXX should default to no but currently broken
separate_assemblies - bool(yes),
@@ -1491,6 +1499,10 @@
long_option("sign-assembly", sign_assembly).
long_option("separate-assemblies", separate_assemblies).
long_option("generate-schemas", generate_schemas).
+long_option("mode-constraints", mode_constraints).
+long_option("simple-mode-constraints", simple_mode_constraints).
+long_option("benchmark-modes", benchmark_modes).
+long_option("benchmark-modes-repeat", benchmark_modes_repeat).
% language semantics options
long_option("reorder-conj", reorder_conj).
Index: compiler/top_level.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/top_level.m,v
retrieving revision 1.4
diff -u -b -r1.4 top_level.m
--- compiler/top_level.m 23 Mar 2004 10:52:13 -0000 1.4
+++ compiler/top_level.m 23 Mar 2004 10:57:37 -0000
@@ -16,6 +16,7 @@
% the front-end phases
:- import_module check_hlds.
:- import_module hlds.
+:- import_module mode_robdd.
:- import_module parse_tree.
:- import_module transform_hlds.
cvs diff: Diffing compiler/notes
cvs diff: Diffing debian
cvs diff: Diffing deep_profiler
cvs diff: Diffing deep_profiler/notes
cvs diff: Diffing doc
Index: doc/user_guide.texi
===================================================================
RCS file: /home/mercury1/repository/mercury/doc/user_guide.texi,v
retrieving revision 1.402
diff -u -b -r1.402 user_guide.texi
--- doc/user_guide.texi 14 Dec 2004 07:04:38 -0000 1.402
+++ doc/user_guide.texi 16 Dec 2004 02:45:14 -0000
@@ -5135,6 +5135,7 @@
u - unification categories and other implementation details of unifications,
v - variable numbers in variable names,
A - argument passing information,
+B - mode constraint information,
C - clause information,
D - instmap deltas of goals,
G - compile-time garbage collection information,
@@ -5168,6 +5169,37 @@
Dump the internal compiler representation of the MLDS,
after the specified stage number or stage name, to
@file{@var{module}.mlds_dump. at var{num}- at var{name}}.
+
+ at sp 1
+ at item --mode-constraints
+ at findex --mode-constraints
+Perform constraint based mode analysis on the given modules.
+At the moment, the only effect of this
+is to include more information in HDLS dumps,
+to allow the constraint based mode analysis algorithm to be debugged.
+
+ at sp 1
+ at item --simple-mode-constraints
+ at findex --simple-mode-constraints
+Ask for the simplified variant of constraint based mode analysis,
+in which there is only one constraint variable per program variable,
+rather than one constraint variable
+per node in the inst graph of a program variable.
+This option is ignored unless --mode-constraints is also given.
+
+ at sp 1
+ at item --benchmark-modes
+ at findex --benchmark-modes
+Output information about the performance
+of the constraint based mode analysis algorithm.
+
+ at sp 1
+ at item --benchmark-modes-repeat @var{num}
+ at findex --benchmark-modes-repeat @var{num}
+Specifies the number of times the mode analysis algorithm should run.
+More repetitions may smooth out fluctuations
+due to background load or clock granularity.
+This option is ignored unless --benchmark-modes is also given.
@ifset aditi
@sp 1
cvs diff: Diffing extras
cvs diff: Diffing extras/aditi
cvs diff: Diffing extras/cgi
cvs diff: Diffing extras/complex_numbers
cvs diff: Diffing extras/complex_numbers/samples
cvs diff: Diffing extras/complex_numbers/tests
cvs diff: Diffing extras/concurrency
cvs diff: Diffing extras/curs
cvs diff: Diffing extras/curs/samples
cvs diff: Diffing extras/curses
cvs diff: Diffing extras/curses/sample
cvs diff: Diffing extras/dynamic_linking
cvs diff: Diffing extras/error
cvs diff: Diffing extras/graphics
cvs diff: Diffing extras/graphics/easyx
cvs diff: Diffing extras/graphics/easyx/samples
cvs diff: Diffing extras/graphics/mercury_glut
cvs diff: Diffing extras/graphics/mercury_opengl
cvs diff: Diffing extras/graphics/mercury_tcltk
cvs diff: Diffing extras/graphics/samples
cvs diff: Diffing extras/graphics/samples/calc
cvs diff: Diffing extras/graphics/samples/gears
cvs diff: Diffing extras/graphics/samples/maze
cvs diff: Diffing extras/graphics/samples/pent
cvs diff: Diffing extras/lazy_evaluation
cvs diff: Diffing extras/lex
cvs diff: Diffing extras/lex/samples
cvs diff: Diffing extras/lex/tests
cvs diff: Diffing extras/logged_output
cvs diff: Diffing extras/moose
cvs diff: Diffing extras/moose/samples
cvs diff: Diffing extras/moose/tests
cvs diff: Diffing extras/morphine
cvs diff: Diffing extras/morphine/non-regression-tests
cvs diff: Diffing extras/morphine/scripts
cvs diff: Diffing extras/morphine/source
cvs diff: Diffing extras/odbc
cvs diff: Diffing extras/posix
cvs diff: Diffing extras/quickcheck
cvs diff: Diffing extras/quickcheck/tutes
cvs diff: Diffing extras/references
cvs diff: Diffing extras/references/samples
cvs diff: Diffing extras/references/tests
cvs diff: Diffing extras/stream
cvs diff: Diffing extras/trailed_update
cvs diff: Diffing extras/trailed_update/samples
cvs diff: Diffing extras/trailed_update/tests
cvs diff: Diffing extras/xml
cvs diff: Diffing extras/xml/samples
cvs diff: Diffing extras/xml_stylesheets
cvs diff: Diffing java
cvs diff: Diffing java/runtime
cvs diff: Diffing library
cvs diff: Diffing profiler
cvs diff: Diffing robdd
cvs diff: Diffing runtime
cvs diff: Diffing runtime/GETOPT
cvs diff: Diffing runtime/machdeps
cvs diff: Diffing samples
cvs diff: Diffing samples/c_interface
cvs diff: Diffing samples/c_interface/c_calls_mercury
cvs diff: Diffing samples/c_interface/cplusplus_calls_mercury
cvs diff: Diffing samples/c_interface/mercury_calls_c
cvs diff: Diffing samples/c_interface/mercury_calls_cplusplus
cvs diff: Diffing samples/c_interface/mercury_calls_fortran
cvs diff: Diffing samples/c_interface/simpler_c_calls_mercury
cvs diff: Diffing samples/c_interface/simpler_cplusplus_calls_mercury
cvs diff: Diffing samples/diff
cvs diff: Diffing samples/muz
cvs diff: Diffing samples/rot13
cvs diff: Diffing samples/solutions
cvs diff: Diffing samples/tests
cvs diff: Diffing samples/tests/c_interface
cvs diff: Diffing samples/tests/c_interface/c_calls_mercury
cvs diff: Diffing samples/tests/c_interface/cplusplus_calls_mercury
cvs diff: Diffing samples/tests/c_interface/mercury_calls_c
cvs diff: Diffing samples/tests/c_interface/mercury_calls_cplusplus
cvs diff: Diffing samples/tests/c_interface/mercury_calls_fortran
cvs diff: Diffing samples/tests/c_interface/simpler_c_calls_mercury
cvs diff: Diffing samples/tests/c_interface/simpler_cplusplus_calls_mercury
cvs diff: Diffing samples/tests/diff
cvs diff: Diffing samples/tests/muz
cvs diff: Diffing samples/tests/rot13
cvs diff: Diffing samples/tests/solutions
cvs diff: Diffing samples/tests/toplevel
cvs diff: Diffing scripts
cvs diff: Diffing tests
cvs diff: Diffing tests/benchmarks
cvs diff: Diffing tests/debugger
cvs diff: Diffing tests/debugger/declarative
cvs diff: Diffing tests/dppd
cvs diff: Diffing tests/general
cvs diff: Diffing tests/general/accumulator
cvs diff: Diffing tests/general/string_format
cvs diff: Diffing tests/general/structure_reuse
cvs diff: Diffing tests/grade_subdirs
cvs diff: Diffing tests/hard_coded
cvs diff: Diffing tests/hard_coded/exceptions
cvs diff: Diffing tests/hard_coded/purity
cvs diff: Diffing tests/hard_coded/sub-modules
cvs diff: Diffing tests/hard_coded/typeclasses
cvs diff: Diffing tests/invalid
cvs diff: Diffing tests/invalid/purity
cvs diff: Diffing tests/misc_tests
cvs diff: Diffing tests/mmc_make
cvs diff: Diffing tests/mmc_make/lib
cvs diff: Diffing tests/recompilation
cvs diff: Diffing tests/tabling
cvs diff: Diffing tests/term
cvs diff: Diffing tests/valid
cvs diff: Diffing tests/warnings
cvs diff: Diffing tools
cvs diff: Diffing trace
cvs diff: Diffing util
cvs diff: Diffing vim
cvs diff: Diffing vim/after
cvs diff: Diffing vim/ftplugin
cvs diff: Diffing vim/syntax
--------------------------------------------------------------------------
mercury-reviews mailing list
post: mercury-reviews at cs.mu.oz.au
administrative address: owner-mercury-reviews at cs.mu.oz.au
unsubscribe: Address: mercury-reviews-request at cs.mu.oz.au Message: unsubscribe
subscribe: Address: mercury-reviews-request at cs.mu.oz.au Message: subscribe
--------------------------------------------------------------------------
More information about the reviews
mailing list