[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