[m-rev.] for review: changes to the library from the mode-constraints branch
Zoltan Somogyi
zs at cs.mu.OZ.AU
Mon Aug 19 14:02:23 AEST 2002
For review by anyone.
Zoltan.
Move changes in the library on the mode-constraints branch onto the trunk.
library/eqvclass.m:
Add some utility functions and predicates.
library/map.m:
Add some utility functions and predicates, and some type
specialization directives.
library/robdd.m:
Add this module, which provides a Mercury interface to the C code in
robdd/bryant.c. In some places, robustness has been sacrificed for
speed, and the module is not (yet) as well documented as it could be;
therefore it is not (yet) included in the documentation.
library/pprint.m:
Print robdds nicely, since this is essential to debugging code handling
robdds. (This is why adding robdd.m in some other directory, e.g. the
compiler, wouldn't really work.)
library/term.m:
Add a function that returns the highest numbered vars created from
a var_supply.
library/varset.m:
Add a function that returns the highest numbered vars created from
a varset.
library/unsafe.m:
Add this module here, since it may be needed to debug code in the
library (e.g. in robdd.m.)
library/library.m:
Add a reference to the robdd module, and a commented out reference
to the unsafe module. If a developer needs to use unsafe.m anywhere
in the Mercury implementation, they can uncomment this reference
in the relevant workspace.
NEWS:
Mention the new predicates and functions.
deep_profiler/canonical.m:
Comment out the calls to unsafe.
deep_profiler/unsafe.m:
Remove this module from this directory.
doc/Mmakefile:
Do not include the robdd and unsafe modules in the documentation.
The robdd module because (in its present state) it is not stable
enough, the unsafe module because it is not enabled in installed
versions of the library.
Index: NEWS
===================================================================
RCS file: /home/mercury1/repository/mercury/NEWS,v
retrieving revision 1.266
diff -u -b -r1.266 NEWS
--- NEWS 2002/08/12 08:02:41 1.266
+++ NEWS 2002/08/19 04:00:10
@@ -167,6 +167,19 @@
which construct lists may need to be updated.
* We've added the predicate list__is_empty/1 and list__is_not_empty/1.
+* We've added functions get_equivalent_elements, get_minimum_element and
+ remove_equivalent_elements, and their predicate versions, to eqvclass.m
+
+* We've added semidet functions max_key and min_key to return the maximum and
+ minimum keys in maps and 2-3-4 trees.
+
+* We've added predicates member, remove_leq, remove_gt, foldl and filter
+ to sparse_bitset.m.
+
+* We've added a function var_supply_max_var to term.m.
+
+* We've added a function max_var to varset.m.
+
* We've added a function version of error/1, called func_error/1, to require.m.
* ops.m now defines a typeclass which can be used to define operator
cvs diff: Diffing library
Index: library/eqvclass.m
===================================================================
RCS file: /home/mercury1/repository/mercury/library/eqvclass.m,v
retrieving revision 1.11
diff -u -b -r1.11 eqvclass.m
--- library/eqvclass.m 2000/11/12 08:51:33 1.11
+++ library/eqvclass.m 2002/08/19 03:31:44
@@ -1,5 +1,5 @@
%---------------------------------------------------------------------------%
-% Copyright (C) 1995-1997, 1999 The University of Melbourne.
+% Copyright (C) 1995-1997, 1999, 2001 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.
%---------------------------------------------------------------------------%
@@ -106,6 +106,30 @@
:- func eqvclass__partition_list_to_eqvclass(list(set(T))) = eqvclass(T).
+ % Return the set of elements equivalent to the given element.
+ % This set will of course include the given element.
+
+:- pred eqvclass__get_equivalent_elements(eqvclass(T), T, set(T)).
+:- mode eqvclass__get_equivalent_elements(in, in, out) is det.
+
+:- func eqvclass__get_equivalent_elements(eqvclass(T), T) = set(T).
+
+ % Return the smallest element equivalent to the given element.
+ % This may or may not be the given element.
+
+:- pred eqvclass__get_minimum_element(eqvclass(T), T, T).
+:- mode eqvclass__get_minimum_element(in, in, out) is det.
+
+:- func eqvclass__get_minimum_element(eqvclass(T), T) = T.
+
+ % Remove the given element and all other elements equivalent to it
+ % from the given equivalence class.
+
+:- pred eqvclass__remove_equivalent_elements(eqvclass(T), T, eqvclass(T)).
+:- mode eqvclass__remove_equivalent_elements(in, in, out) is det.
+
+:- func eqvclass__remove_equivalent_elements(eqvclass(T), T) = eqvclass(T).
+
%---------------------------------------------------------------------------%
:- implementation.
@@ -315,6 +339,23 @@
eqvclass__make_partition(Elements, Id, ElementMap1, ElementMap).
%---------------------------------------------------------------------------%
+
+eqvclass__get_equivalent_elements(EC, X,
+ eqvclass__get_equivalent_elements(EC, X)).
+
+eqvclass__get_minimum_element(EC, X, eqvclass__get_minimum_element(EC, X)).
+
+eqvclass__remove_equivalent_elements(eqvclass(Id, P0, E0), X,
+ eqvclass(Id, P, E)) :-
+ ( map__search(E0, X, Partition) ->
+ map__det_remove(P0, Partition, Eq, P),
+ map__delete_list(E0, set__to_sorted_list(Eq), E)
+ ;
+ P = P0,
+ E = E0
+ ).
+
+%---------------------------------------------------------------------------%
%---------------------------------------------------------------------------%
% Ralph Becket <rwab1 at cl.cam.ac.uk> 29/04/99
% Function forms added.
@@ -345,3 +386,17 @@
eqvclass__partition_list_to_eqvclass(Xs) = EC :-
eqvclass__partition_list_to_eqvclass(Xs, EC).
+
+eqvclass__get_equivalent_elements(eqvclass(_, PartitionMap, ElementMap), X) =
+ ( Eqv = map__search(PartitionMap, map__search(ElementMap, X)) ->
+ Eqv
+ ;
+ set__make_singleton_set(X)
+ ).
+
+eqvclass__get_minimum_element(EC, X) =
+ list__det_head(set__to_sorted_list(
+ eqvclass__get_equivalent_elements(EC, X))).
+
+eqvclass__remove_equivalent_elements(EC0, X) = EC :-
+ eqvclass__remove_equivalent_elements(EC0, X, EC).
Index: library/library.m
===================================================================
RCS file: /home/mercury1/repository/mercury/library/library.m,v
retrieving revision 1.64
diff -u -b -r1.64 library.m
--- library/library.m 2002/06/14 10:18:49 1.64
+++ library/library.m 2002/08/16 01:12:10
@@ -37,15 +37,21 @@
:- import_module float, gc, getopt, graph, group, hash_table.
:- import_module int, integer, io, lexer, list, map, math, multi_map, ops.
:- import_module parser, pprint, pqueue, prolog, queue.
-:- import_module random, rational, rbtree, relation, require.
+:- import_module random, rational, rbtree, relation, require, robdd.
:- import_module set, set_bbbtree, set_ordlist, set_unordlist, sparse_bitset.
:- import_module stack, std_util, store, string.
:- import_module term, term_io, tree234, time, type_desc, varset.
% The modules intended for Mercury system implementors.
-:- import_module private_builtin, table_builtin, profiling_builtin.
+:- import_module private_builtin, profiling_builtin, table_builtin.
:- import_module rtti_implementation.
+% Uncomment this temporarily (in your own workspace) if you need access to
+% unsafe predicates. In MLDS grades, you would also have to add unsafe to
+% the list in mercury_std_library_module in the compiler you use to compile
+% the library.
+% :- import_module unsafe.
+
% library__version must be implemented using pragma c_code,
% so we can get at the MR_VERSION and MR_FULLARCH configuration
% parameters. We can't just generate library.m from library.m.in
@@ -53,7 +59,8 @@
% might not have a Mercury compiler around to compile library.m with.
:- pragma foreign_proc("C",
- library__version(Version::out), [will_not_call_mercury, promise_pure],
+ library__version(Version::out),
+ [will_not_call_mercury, promise_pure],
"
MR_ConstString version_string =
MR_VERSION "", configured for "" MR_FULLARCH;
@@ -69,7 +76,8 @@
").
:- pragma foreign_proc("MC++",
- library__version(Version::out), [will_not_call_mercury, promise_pure],
+ library__version(Version::out),
+ [will_not_call_mercury, promise_pure],
"
// XXX we should use string literals with an S at the start
// so this code uses just managed types.
Index: library/map.m
===================================================================
RCS file: /home/mercury1/repository/mercury/library/map.m,v
retrieving revision 1.80
diff -u -b -r1.80 map.m
--- library/map.m 2001/05/24 02:32:28 1.80
+++ library/map.m 2002/08/14 00:36:37
@@ -72,6 +72,10 @@
:- pred map__upper_bound_lookup(map(K,V), K, K, V).
:- mode map__upper_bound_lookup(in, in, out, out) is det.
+:- func map__max_key(map(K,V)) = K is semidet.
+
+:- func map__min_key(map(K,V)) = K is semidet.
+
% Search map for data.
:- pred map__inverse_search(map(K,V), V, K).
:- mode map__inverse_search(in, in, out) is nondet.
@@ -399,6 +403,19 @@
:- pragma type_spec(map__select/2, K = var(_)).
:- pragma type_spec(map__select/3, K = var(_)).
+:- pragma type_spec(map__elem/2, K = int).
+:- pragma type_spec(map__elem/2, K = var(_)).
+
+:- pragma type_spec(map__det_elem/2, K = int).
+:- pragma type_spec(map__det_elem/2, K = var(_)).
+
+:- pragma type_spec('map__elem :='/3, K = int).
+:- pragma type_spec('map__elem :='/3, K = var(_)).
+
+:- pragma type_spec('map__det_elem :='/3, K = int).
+:- pragma type_spec('map__det_elem :='/3, K = var(_)).
+
+
:- implementation.
:- import_module std_util, require, string.
@@ -450,6 +467,10 @@
report_lookup_error("map__upper_bound_lookup: key not found",
SearchK, V)
).
+
+map__max_key(M) = tree234__max_key(M).
+
+map__min_key(M) = tree234__min_key(M).
map__insert(Map0, K, V, Map) :-
tree234__insert(Map0, K, V, Map).
Index: library/pprint.m
===================================================================
RCS file: /home/mercury1/repository/mercury/library/pprint.m,v
retrieving revision 1.11
diff -u -b -r1.11 pprint.m
--- library/pprint.m 2002/07/16 08:10:44 1.11
+++ library/pprint.m 2002/08/14 00:36:42
@@ -372,6 +372,7 @@
:- implementation.
:- import_module array, map, sparse_bitset, enum, term, exception.
+:- import_module robdd.
:- type doc
---> 'NIL'
@@ -676,6 +677,9 @@
else if dynamic_cast_to_map_pair(X, MapPair)
then map_pair_to_doc(Depth, MapPair)
+ else if dynamic_cast_to_robdd(X, Robdd)
+ then robdd_to_doc(Depth, Robdd)
+
else generic_term_to_doc(Depth, X)
).
@@ -835,6 +839,26 @@
%-----------------------------------------------------------------------------%
+:- some [T2] pred dynamic_cast_to_robdd(T1, robdd(T2)).
+:- mode dynamic_cast_to_robdd(in, out) is semidet.
+
+dynamic_cast_to_robdd(X, R) :-
+
+ % If X is a robdd then it has a type with one type argument.
+ %
+ [ArgTypeDesc] = type_args(type_of(X)),
+
+ % Convert ArgTypeDesc to a type variable ArgType.
+ %
+ (_ `with_type` ArgType) `has_type` ArgTypeDesc,
+
+ % Constrain the type of R to be robdd(ArgType) and do the
+ % cast.
+ %
+ dynamic_cast(X, R `with_type` robdd(ArgType)).
+
+%-----------------------------------------------------------------------------%
+
:- func var_to_doc(int, var(T)) = doc.
var_to_doc(Depth, V) =
@@ -898,5 +922,12 @@
map_pair_to_doc(Depth, map_pair(Key, Value)) =
to_doc(Depth - 1, Key) ++ text(" -> ") ++
group(nest(2, line ++ to_doc(Depth - 1, Value))).
+
+%-----------------------------------------------------------------------------%
+
+:- func robdd_to_doc(int, robdd(T)) = doc.
+
+robdd_to_doc(Depth, R) =
+ "robdd_dnf" ++ parentheses(list_to_doc(Depth, dnf(R))).
%-----------------------------------------------------------------------------%
Index: library/robdd.m
===================================================================
RCS file: robdd.m
diff -N robdd.m
--- /dev/null Tue Aug 6 19:10:00 2002
+++ robdd.m Mon Aug 19 10:10:46 2002
@@ -0,0 +1,1484 @@
+%---------------------------------------------------------------------------%
+% Copyright (C) 2001-2002 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: robdd.m.
+% Main author: dmo
+% Stability: low
+
+% This module contains a Mercury interface to Peter Schachte's C
+% implementation of Reduced Ordered Binary Decision Diagrams (ROBDDs).
+% ROBDDs are an efficent representation for Boolean constraints.
+
+% Boolean variables are represented using the type var(T) from the
+% `term' library module (see the `term' module documentation for
+% more information).
+
+% Example usage:
+% % Create some variables.
+% term__init_var_supply(VarSupply0),
+% term__create_var(VarSupply0, A, VarSupply1),
+% term__create_var(VarSupply1, B, VarSupply2),
+% term__create_var(VarSupply2, C, VarSupply),
+%
+% % Create some ROBDDs.
+% R1 = ( var(A) =:= var(B) * (~var(C)) ),
+% R2 = ( var(A) =< var(B) ),
+%
+% % Test if R1 entails R2 (should succeed).
+% R1 `entails` R2,
+%
+% % Project R1 onto A and B.
+% R3 = restrict(C, R1),
+%
+% % Test R2 and R3 for equivalence (should succeed).
+% R2 = R3.
+
+% ROBDDs are implemented so that two ROBDDs, R1 and R2, represent
+% the same Boolean constraint if and only iff `R1 = R2'. Checking
+% equivalence of ROBDDs is fast since it involves only a single
+% pointer comparison.
+
+%-----------------------------------------------------------------------------%
+%-----------------------------------------------------------------------------%
+
+:- module robdd.
+
+:- interface.
+
+:- import_module term, io, sparse_bitset, list, map.
+
+:- type robdd(T).
+:- type robdd == robdd(generic).
+
+:- type vars(T) == sparse_bitset(var(T)). % XXX experiment with different reps.
+
+:- func empty_vars_set = vars(T).
+
+% Constants.
+:- func one = robdd(T).
+:- func zero = robdd(T).
+
+% If-then-else.
+:- func ite(robdd(T), robdd(T), robdd(T)) = robdd(T).
+
+% The functions *, +, =<, =:=, =\= and ~ correspond to the names
+% used in the SICStus clp(B) library.
+
+% Conjunction.
+:- func robdd(T) * robdd(T) = robdd(T).
+
+% Disjunction.
+:- func robdd(T) + robdd(T) = robdd(T).
+
+% Implication.
+:- func (robdd(T) =< robdd(T)) = robdd(T).
+
+% Equivalence.
+:- func (robdd(T) =:= robdd(T)) = robdd(T).
+
+% Non-equivalence (XOR).
+:- func (robdd(T) =\= robdd(T)) = robdd(T).
+
+% Negation.
+:- func (~ robdd(T)) = robdd(T).
+
+%-----------------------------------------------------------------------------%
+
+ % var(X) is the ROBDD that is true iff X is true.
+:- func var(var(T)) = robdd(T).
+
+% The following functions operate on individual variables and are
+% more efficient than the more generic versions above that take
+% ROBDDs as input.
+
+ % not_var(V) = ~ var(V).
+:- func not_var(var(T)) = robdd(T).
+
+ % ite_var(V, FA, FB) = ite(var(V), FA, FB).
+:- func ite_var(var(T), robdd(T), robdd(T)) = robdd(T).
+
+ % eq_vars(X, Y) = ( var(X) =:= var(Y) ).
+:- func eq_vars(var(T), var(T)) = robdd(T).
+
+ % neq_vars(X, Y) = ( var(X) =\= var(Y) ).
+:- func neq_vars(var(T), var(T)) = robdd(T).
+
+ % imp_vars(X, Y) = ( var(X) =< var(Y) ).
+:- func imp_vars(var(T), var(T)) = robdd(T).
+
+ % conj_vars([V1, V2, ..., Vn]) = var(V1) * var(V2) * ... * var(Vn).
+:- func conj_vars(vars(T)) = robdd(T).
+
+ % conj_not_vars([V1, V2, ..., Vn]) = not_var(V1) * ... * not_var(Vn).
+:- func conj_not_vars(vars(T)) = robdd(T).
+
+ % disj_vars([V1, V2, ..., Vn]) = var(V1) + var(V2) + ... + var(Vn).
+:- func disj_vars(vars(T)) = robdd(T).
+
+ % at_most_one_of(Vs) =
+ % foreach pair Vi, Vj in Vs where Vi \= Vj. ~(var(Vi) * var(Vj)).
+:- func at_most_one_of(vars(T)) = robdd(T).
+
+ % var_restrict_true(V, F) = restrict(V, F * var(V)).
+:- func var_restrict_true(var(T), robdd(T)) = robdd(T).
+
+ % var_restrict_false(V, F) = restrict(V, F * not_var(V)).
+:- func var_restrict_false(var(T), robdd(T)) = robdd(T).
+
+%-----------------------------------------------------------------------------%
+
+ % X `entails` Y
+ % Succeed iff X entails Y.
+ % Does not create any new ROBDD nodes.
+:- pred robdd(T) `entails` robdd(T).
+:- mode in `entails` in is semidet.
+
+ % Succeed iff the var is entailed by the ROBDD.
+:- pred var_entailed(robdd(T)::in, var(T)::in) is semidet.
+
+ % Return the set of vars entailed by the ROBDD.
+:- func vars_entailed(robdd(T)) = vars_entailed_result(T).
+
+ % Return the set of vars disentailed by the ROBDD.
+:- func vars_disentailed(robdd(T)) = vars_entailed_result(T).
+
+ % definite_vars(R, T, F) <=> T = vars_entailed(R) /\
+ % F = vars_disentailed(R)
+:- pred definite_vars(robdd(T)::in, vars_entailed_result(T)::out,
+ vars_entailed_result(T)::out) is det.
+
+:- func equivalent_vars(robdd(T)) = equivalent_result(T).
+
+:- type entailment_result(T)
+ ---> all_vars
+ ; some_vars(vars :: T).
+
+:- type vars_entailed_result(T) == entailment_result(vars(T)).
+
+:- type equivalent_result(T) == entailment_result(map(var(T), var(T))).
+
+:- func extract_implications(robdd(T)) = imp_vars(T).
+
+ % Existentially quantify away the var in the ROBDD.
+:- func restrict(var(T), robdd(T)) = robdd(T).
+
+ % Existentially quantify away all vars greater than the specified var.
+:- func restrict_threshold(var(T), robdd(T)) = robdd(T).
+
+ % Existentially quantify away all vars for which the predicate fails.
+:- func restrict_filter(pred(var(T)), robdd(T)) = robdd(T).
+:- mode restrict_filter(pred(in) is semidet, in) = out is det.
+
+ % restrict_filter(P, D, R)
+ % Existentially quantify away all vars for which P fails,
+ % except, if D fails for a var, do not existentially quantify
+ % away that var or any greater than it. This means that D can be
+ % used to set a depth limit on the existential quantification.
+:- func restrict_filter(pred(var(T)), pred(var(T)), robdd(T)) = robdd(T).
+:- mode restrict_filter(pred(in) is semidet, pred(in) is semidet, in) = out
+ is det.
+
+:- func restrict_true_false_vars(vars(T), vars(T), robdd(T)) = robdd(T).
+
+ % Given a leader map, remove all but the least variable in each
+ % equivalence class from the ROBDD.
+ % Note: the leader map MUST correspond to actual equivalences within the
+ % ROBDD, (e.g. have been produced by 'equivalent_vars/1').
+:- func squeeze_equiv(map(var(T), var(T)), robdd(T)) = robdd(T).
+
+:- func make_equiv(map(var(T), var(T))) = robdd(T).
+
+:- func expand_equiv(map(var(T), var(T)), robdd(T)) = robdd(T).
+
+:- func expand_implications(imp_vars(T), robdd(T)) = robdd(T).
+
+:- type imp_vars(T)
+ ---> imp_vars(
+ imps :: imp_map(T), % K => V (~K \/ V)
+ rev_imps ::imp_map(T), % ~K => ~V ( K \/ ~V)
+ dis_imps :: imp_map(T), % K => ~V (~K \/ ~V)
+ rev_dis_imps :: imp_map(T) % ~K => V ( K \/ V)
+ ).
+
+:- type imp_map(T) == map(var(T), vars(T)).
+
+:- func remove_implications(imp_vars(T), robdd(T)) = robdd(T).
+
+%-----------------------------------------------------------------------------%
+
+:- type literal(T)
+ ---> pos(var(T))
+ ; neg(var(T)).
+
+ % Convert the ROBDD to disjunctive normal form.
+:- func dnf(robdd(T)) = list(list(literal(T))).
+
+% % Convert the ROBDD to conjunctive normal form.
+% :- func cnf(robdd(T)) = list(list(literal(T))).
+
+ % Print out the ROBDD in disjunctive normal form.
+:- pred print_robdd(robdd(T)::in, io__state::di, io__state::uo) is det.
+
+ % robdd_to_dot(ROBDD, WriteVar, FileName, IO0, IO).
+ % Output the ROBDD in a format that can be processed by the
+ % graph-drawing program `dot'.
+:- pred robdd_to_dot(robdd(T)::in, write_var(T)::in(write_var),
+ string::in, io__state::di, io__state::uo) is det.
+
+ % robdd_to_dot(ROBDD, WriteVar, IO0, IO).
+ % Output the ROBDD in a format that can be processed by the
+ % graph-drawing program `dot'.
+:- pred robdd_to_dot(robdd(T)::in, write_var(T)::in(write_var),
+ io__state::di, io__state::uo) is det.
+
+:- type write_var(T) == pred(var(T), io__state, io__state).
+:- inst write_var = (pred(in, di, uo) is det).
+
+ % Apply the variable substitution to the ROBDD.
+:- func rename_vars(func(var(T)) = var(T), robdd(T)) = robdd(T).
+
+ % Succeed iff ROBDD = one or ROBDD = zero.
+:- pred is_terminal(robdd(T)::in) is semidet.
+
+ % Output the number of nodes and the depth of the ROBDD.
+:- pred size(robdd(T)::in, int::out, int::out) is det.
+
+ % Output the number of nodes, the depth of the ROBDD and the
+ % variables it contains.
+:- pred size(robdd(T)::in, int::out, int::out, list(var(T))::out) is det.
+
+ % Succeed iff the var is constrained by the ROBDD.
+:- pred var_is_constrained(robdd(T)::in, var(T)::in) is semidet.
+
+ % Succeed iff all the vars in the set are constrained by the ROBDD.
+:- pred vars_are_constrained(robdd(T)::in, vars(T)::in) is semidet.
+
+%-----------------------------------------------------------------------------%
+
+ % labelling(Vars, ROBDD, TrueVars, FalseVars)
+ % Takes a set of Vars and an ROBDD and returns a value assignment
+ % for those Vars that is a model of the Boolean function
+ % represented by the ROBDD.
+ % 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, robdd(T)::in, vars(T)::out,
+ vars(T)::out) is nondet.
+
+ % minimal_model(Vars, ROBDD, TrueVars, FalseVars)
+ % Takes a set of Vars and an ROBDD and returns a value assignment
+ % for those Vars that is a minimal model of the Boolean function
+ % represented by the ROBDD.
+ % 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, robdd(T)::in, vars(T)::out,
+ vars(T)::out) is nondet.
+
+%-----------------------------------------------------------------------------%
+
+ % Zero the internal caches used for ROBDD operations.
+ % This allows nodes in the caches to be garbage-collected.
+ % This operation is pure and does not perform any I/O, but we need
+ % to either declare it impure or pass io__states to ensure that
+ % the compiler won't try to optimise away the call.
+
+:- pred clear_caches(io__state::di, io__state::uo) is det.
+
+:- impure pred clear_caches is det.
+
+%-----------------------------------------------------------------------------%
+%-----------------------------------------------------------------------------%
+
+:- implementation.
+
+:- import_module set_unordlist, list, string, map, bool, set_bbbtree, int.
+:- import_module multi_map, require.
+:- import_module hash_table.
+
+% :- import_module unsafe.
+
+:- type robdd(T) ---> robdd(int).
+% :- type robdd(T) ---> robdd(c_pointer).
+% Can't use a c_pointer since we want to memo ROBDD operations and
+% pragma memo does not support c_pointers.
+
+empty_vars_set = sparse_bitset__init.
+
+:- pragma foreign_decl("C", "
+
+#define NDEBUG
+#define CLEAR_CACHES
+#define COMPUTED_TABLE
+#define EQUAL_TEST
+#define USE_ITE_CONSTANT
+#define NEW
+#define RESTRICT_SET
+
+#include ""../robdd/bryant.h""
+").
+
+:- pragma foreign_code("C", "
+#include ""../robdd/bryant.c""
+").
+
+:- pragma foreign_proc("C",
+ one = (F::out),
+ [will_not_call_mercury, promise_pure],
+"
+ F = (MR_Word) trueVar();
+").
+
+:- pragma foreign_proc("C",
+ zero = (F::out),
+ [will_not_call_mercury, promise_pure],
+"
+ F = (MR_Word) falseVar();
+").
+
+:- pragma foreign_proc("C",
+ var(V::in) = (F::out),
+ [will_not_call_mercury, promise_pure],
+"
+ F = (MR_Word) variableRep(V);
+").
+
+:- pragma foreign_proc("C",
+ ite(F::in, G::in, H::in) = (ITE::out),
+ [will_not_call_mercury, promise_pure],
+"
+ ITE = (MR_Word) ite((node *) F, (node *) G, (node *) H);
+").
+
+:- pragma foreign_proc("C",
+ ite_var(V::in, G::in, H::in) = (ITE::out),
+ [will_not_call_mercury, promise_pure],
+"
+ ITE = (MR_Word) ite_var(V, (node *) G, (node *) H);
+").
+
+:- pragma promise_pure('*'/2).
+X * Y = R :-
+ R = glb(X, Y),
+
+ % XXX debugging code.
+ %( R = zero ->
+ ( (X = zero ; Y = zero) ->
+ impure report_zero_constraint
+ ;
+ true
+ ).
+
+% XXX :- pragma c_code((X::in) * (Y::in) = (F::out), [will_not_call_mercury],
+:- func glb(robdd(T), robdd(T)) = robdd(T).
+:- pragma foreign_proc("C",
+ glb(X::in, Y::in) = (F::out),
+ [will_not_call_mercury, promise_pure],
+"
+ F = (MR_Word) glb((node *) X, (node *) Y);
+").
+
+% XXX
+:- impure pred report_zero_constraint is det.
+:- pragma foreign_proc("C",
+ report_zero_constraint,
+ [will_not_call_mercury],
+"
+ fprintf(stderr, ""Zero constraint!!!\\n"");
+").
+
+:- pragma foreign_proc("C",
+ (X::in) + (Y::in) = (F::out),
+ [will_not_call_mercury, promise_pure],
+"
+ F = (MR_Word) lub((node *) X, (node *) Y);
+").
+
+:- pragma foreign_proc("C",
+ ((X::in) =< (Y::in)) = (F::out),
+ [will_not_call_mercury, promise_pure],
+"
+ F = (MR_Word) implies((node *) X, (node *) Y);
+").
+
+(F =:= G) = ite(F, G, ~G).
+
+(F =\= G) = ite(F, ~G, G).
+
+(~F) = ite(F, zero, one).
+
+:- pragma foreign_proc("C",
+ entails(X::in, Y::in),
+ [will_not_call_mercury, promise_pure],
+"
+ SUCCESS_INDICATOR = (ite_constant((node *) X, (node *) Y, one) == one);
+").
+
+:- pragma foreign_proc("C",
+ var_entailed(F::in, V::in),
+ [will_not_call_mercury, promise_pure],
+"
+ SUCCESS_INDICATOR = var_entailed((node *) F, (int) V);
+").
+
+:- pragma memo(vars_entailed/1).
+
+vars_entailed(R) =
+ ( R = one ->
+ some_vars(empty_vars_set)
+ ; R = zero ->
+ all_vars
+ ;
+ (
+ R^fa = zero
+ ->
+ (vars_entailed(R^tr) `intersection` vars_entailed(R^fa))
+ `insert` R^value
+ ;
+ vars_entailed(R^tr) `intersection` vars_entailed(R^fa)
+ )
+ ).
+
+:- pragma memo(vars_disentailed/1).
+
+vars_disentailed(R) =
+ ( R = one ->
+ some_vars(empty_vars_set)
+ ; R = zero ->
+ all_vars
+ ;
+ (
+ R^tr = zero
+ ->
+ (vars_disentailed(R^tr) `intersection`
+ vars_disentailed(R^fa)) `insert` R^value
+ ;
+ vars_disentailed(R^tr) `intersection`
+ vars_disentailed(R^fa)
+ )
+ ).
+
+:- pragma memo(definite_vars/3).
+
+definite_vars(R, T, F) :-
+ ( R = one ->
+ T = some_vars(empty_vars_set),
+ F = some_vars(empty_vars_set)
+ ; R = zero ->
+ T = all_vars,
+ F = all_vars
+ ;
+ definite_vars(R^tr, T_tr, F_tr),
+ definite_vars(R^fa, T_fa, F_fa),
+ T0 = T_tr `intersection` T_fa,
+ F0 = F_tr `intersection` F_fa,
+ ( R^fa = zero ->
+ T = T0 `insert` R^value,
+ F = F0
+ ; R^tr = zero ->
+ T = T0,
+ F = F0 `insert` R^value
+ ;
+ T = T0,
+ F = F0
+ )
+ ).
+
+equivalent_vars(R) = rev_map(equivalent_vars_2(R)).
+
+:- type equivalent_vars_map(T) ---> equivalent_vars_map(map(var(T), vars(T))).
+
+:- func equivalent_vars_2(robdd(T)) = entailment_result(equivalent_vars_map(T)).
+
+:- pragma memo(equivalent_vars_2/1).
+
+equivalent_vars_2(R) = EQ :-
+ ( R = one ->
+ EQ = some_vars(equivalent_vars_map(map__init))
+ ; R = zero ->
+ EQ = all_vars
+ ;
+ EQVars = vars_entailed(R ^ tr) `intersection`
+ vars_disentailed(R ^ fa),
+ EQ0 = equivalent_vars_2(R ^ tr) `intersection`
+ equivalent_vars_2(R ^ fa),
+ (
+ EQVars = all_vars,
+ error("equivalent_vars: unexpected result")
+ % If this condition occurs it means the ROBDD
+ % invariants have been violated somewhere since
+ % both branches of R must have been zero.
+ ;
+ EQVars = some_vars(Vars),
+ ( empty(Vars) ->
+ EQ = EQ0
+ ;
+ (
+ EQ0 = all_vars,
+ error("equivalent_vars: unexpected result")
+ % If this condition occurs it means
+ % the ROBDD invariants have been
+ % violated somewhere since both
+ % branches of R must have been zero.
+ ;
+ EQ0 = some_vars(
+ equivalent_vars_map(M0)),
+ map__det_insert(M0, R ^ value, Vars,
+ M),
+ EQ = some_vars(equivalent_vars_map(M))
+ )
+ )
+ )
+ ).
+
+:- func rev_map(entailment_result(equivalent_vars_map(T))) =
+ equivalent_result(T).
+
+rev_map(all_vars) = all_vars.
+rev_map(some_vars(equivalent_vars_map(EQ0))) = some_vars(EQ) :-
+ map__foldl2(
+ ( pred(V::in, Vs::in, Seen0::in, Seen::out, in, out) is det -->
+ ( { Seen0 `contains` V } ->
+ { Seen = Seen0 }
+ ;
+ ^ elem(V) := V,
+ sparse_bitset__foldl((pred(Ve::in, in, out) is det -->
+ ^ elem(Ve) := V
+ ), Vs),
+ { Seen = Seen0 `sparse_bitset__union` Vs }
+ )
+ ), EQ0, sparse_bitset__init, _, map__init, EQ).
+
+extract_implications(R) = implication_result_to_imp_vars(implications_2(R)).
+
+:- type implication_result(T)
+ ---> implication_result(
+ imp_res(T), % K -> V
+ imp_res(T), % ~K -> ~V
+ imp_res(T), % K -> ~V
+ imp_res(T) % ~K -> V
+ ).
+
+:- type imp_res(T) == entailment_result(imp_res_2(T)).
+:- type imp_res_2(T) ---> imps(map(var(T), vars_entailed_result(T))).
+
+:- func implications_2(robdd(T)) = implication_result(T).
+:- pragma memo(implications_2/1).
+
+implications_2(R) = implication_result(Imps, RevImps, DisImps, RevDisImps) :-
+ ( R = one ->
+ Imps = some_vars(imps(map__init)),
+ RevImps = Imps,
+ DisImps = Imps,
+ RevDisImps = Imps
+ ; R = zero ->
+ Imps = all_vars,
+ RevImps = Imps,
+ DisImps = Imps,
+ RevDisImps = Imps
+ ;
+ TTVars = vars_entailed(R ^ tr),
+ FFVars = vars_disentailed(R ^ fa),
+ TFVars = vars_disentailed(R ^ tr),
+ FTVars = vars_entailed(R ^ fa),
+
+ implications_2(R ^ tr) =
+ implication_result(Imps0, RevImps0, DisImps0,
+ RevDisImps0),
+ implications_2(R ^ fa) =
+ implication_result(Imps1, RevImps1, DisImps1,
+ RevDisImps1),
+
+ Imps2 = merge_imp_res(TTVars, FTVars, Imps0, Imps1),
+ RevImps2 = merge_imp_res(TFVars, FFVars, RevImps0, RevImps1),
+ DisImps2 = merge_imp_res(TFVars, FFVars, DisImps0, DisImps1),
+ RevDisImps2 = merge_imp_res(TTVars, FTVars, RevDisImps0,
+ RevDisImps1),
+
+ % Imps2 = Imps0 `intersection` Imps1,
+ % RevImps2 = RevImps0 `intersection` RevImps1,
+ % DisImps2 = DisImps0 `intersection` DisImps1,
+ % RevDisImps2 = RevDisImps0 `intersection` RevDisImps1,
+
+ Imps = Imps2 ^ elem(R ^ value) := TTVars,
+ RevImps = RevImps2 ^ elem(R ^ value) := FFVars,
+ DisImps = DisImps2 ^ elem(R ^ value) := TFVars,
+ RevDisImps = RevDisImps2 ^ elem(R ^ value) := FTVars
+ ).
+
+:- func merge_imp_res(vars_entailed_result(T), vars_entailed_result(T),
+ imp_res(T), imp_res(T)) = imp_res(T).
+
+merge_imp_res(_, _, all_vars, all_vars) = all_vars.
+merge_imp_res(_, _, some_vars(Imps), all_vars) = some_vars(Imps).
+merge_imp_res(_, _, all_vars, some_vars(Imps)) = some_vars(Imps).
+merge_imp_res(TVars, FVars, some_vars(ImpsA), some_vars(ImpsB)) =
+ some_vars(merge_imp_res_2(TVars, FVars, ImpsA, ImpsB)).
+
+:- func merge_imp_res_2(vars_entailed_result(T), vars_entailed_result(T),
+ imp_res_2(T), imp_res_2(T)) = imp_res_2(T).
+
+merge_imp_res_2(EntailedVarsA, EntailedVarsB, imps(ImpsA), imps(ImpsB)) =
+ imps(Imps) :-
+ KeysA = map__sorted_keys(ImpsA),
+ KeysB = map__sorted_keys(ImpsB),
+ Keys = list__merge_and_remove_dups(KeysA, KeysB),
+ Imps = list__foldl((func(V, M) =
+ M ^ elem(V) := VsA `intersection` VsB :-
+ VsA = ( VsA0 = ImpsA ^ elem(V) -> VsA0 ; EntailedVarsA ),
+ VsB = ( VsB0 = ImpsB ^ elem(V) -> VsB0 ; EntailedVarsB )
+ ), Keys, map__init).
+
+:- func implication_result_to_imp_vars(implication_result(T)) = imp_vars(T).
+
+implication_result_to_imp_vars(ImpRes) = ImpVars :-
+ ImpRes = implication_result(I0, RI0, DI0, RDI0),
+ I = imp_res_to_imp_map(I0),
+ RI = imp_res_to_imp_map(RI0),
+ DI = imp_res_to_imp_map(DI0),
+ RDI = imp_res_to_imp_map(RDI0),
+ ImpVars = imp_vars(I, RI, DI, RDI).
+
+:- func imp_res_to_imp_map(imp_res(T)) = imp_map(T).
+
+imp_res_to_imp_map(all_vars) = map__init.
+imp_res_to_imp_map(some_vars(imps(IRMap))) =
+ map__foldl(func(V, MaybeVs, M) =
+ (
+ MaybeVs = some_vars(Vs),
+ \+ empty(Vs)
+ ->
+ M ^ elem(V) := Vs
+ ;
+ M
+ ),
+ IRMap, init).
+
+remove_implications(ImpRes, R0) = R :-
+ remove_implications_2(ImpRes, sparse_bitset__init, sparse_bitset__init,
+ R0, R, map__init, _).
+
+:- pred remove_implications_2(imp_vars(T)::in, vars(T)::in,
+ vars(T)::in, robdd(T)::in, robdd(T)::out,
+ robdd_cache(T)::in, robdd_cache(T)::out) is det.
+
+remove_implications_2(ImpRes, True, False, R0, R) -->
+ ( { is_terminal(R0) } ->
+ { R = R0 }
+ ; { True `contains` R0 ^ value } ->
+ remove_implications_2(ImpRes, True, False, R0 ^ tr, R)
+ ; { False `contains` R0 ^ value } ->
+ remove_implications_2(ImpRes, True, False, R0 ^ fa, R)
+ ; R1 =^ elem(R0) ->
+ { R = R1 }
+ ;
+ { TrueT = True `union` ImpRes ^ imps ^ get(R0 ^ value) },
+ { FalseT = False `union` ImpRes ^ dis_imps ^ get(R0 ^ value) },
+ remove_implications_2(ImpRes, TrueT, FalseT, R0 ^ tr, RT),
+
+ { TrueF = True `union` ImpRes ^ rev_dis_imps ^ get(R0 ^ value)},
+ { FalseF = False `union` ImpRes ^ rev_imps ^ get(R0 ^ value) },
+ remove_implications_2(ImpRes, TrueF, FalseF, R0 ^ fa, RF),
+
+ { R = make_node(R0 ^ value, RT, RF) },
+ ^ elem(R0) := R
+ ).
+
+:- func get(var(T), imp_map(T)) = vars(T).
+
+get(V, IM) = ( Vs = IM ^ elem(V) -> Vs ; init ).
+
+:- typeclass intersectable(T) where [
+ func T `intersection` T = T
+].
+
+:- instance intersectable(sparse_bitset(T)) where [
+ func(intersection/2) is sparse_bitset__intersect
+].
+
+:- instance intersectable(entailment_result(T)) <= intersectable(T) where [
+ ( all_vars `intersection` R = R ),
+ ( some_vars(Vs) `intersection` all_vars = some_vars(Vs) ),
+ ( some_vars(Vs0) `intersection` some_vars(Vs1) =
+ some_vars(Vs0 `intersection` Vs1) )
+].
+
+:- instance intersectable(equivalent_vars_map(T)) where [
+ ( equivalent_vars_map(MapA) `intersection` equivalent_vars_map(MapB) =
+ equivalent_vars_map(map__foldl((func(V, VsA, M) =
+ ( Vs = VsA `intersect` (MapB ^ elem(V)) ->
+ ( empty(Vs) ->
+ M
+ ;
+ M ^ elem(V) := Vs
+ )
+ ;
+ M
+ )), MapA, map__init))
+ )
+].
+
+:- instance intersectable(imp_res_2(T)) where [
+ imps(MapA) `intersection` imps(MapB) =
+ imps(map__intersect(intersection, MapA, MapB))
+].
+
+:- func 'elem :='(var(T), imp_res(T), vars_entailed_result(T)) = imp_res(T).
+
+'elem :='(_, all_vars, _) = all_vars.
+'elem :='(V, some_vars(imps(M0)), Vs) = some_vars(imps(M0 ^ elem(V) := Vs)).
+
+:- func vars_entailed_result(T) `insert` var(T) = vars_entailed_result(T).
+
+all_vars `insert` _ = all_vars.
+some_vars(Vs) `insert` V = some_vars(Vs `insert` V).
+
+% Access to the struct members.
+% WARNING! These functions are unsafe. You must not call these functions
+% on the terminal robdds (i.e. `zero' and `one').
+:- func value(robdd(T)) = var(T).
+:- func tr(robdd(T)) = robdd(T).
+:- func fa(robdd(T)) = robdd(T).
+
+:- pragma foreign_proc("C",
+ value(F::in) = (Value::out),
+ [will_not_call_mercury, promise_pure],
+"
+ Value = (MR_Word) ((node *) F)->value;
+").
+
+:- pragma foreign_proc("C",
+ tr(F::in) = (Tr::out),
+ [will_not_call_mercury, promise_pure],
+"
+ Tr = (MR_Word) ((node *) F)->tr;
+").
+
+:- pragma foreign_proc("C",
+ fa(F::in) = (Fa::out),
+ [will_not_call_mercury, promise_pure],
+"
+ Fa = (MR_Word) ((node *) F)->fa;
+").
+
+:- pragma inline(value/1).
+:- pragma inline(tr/1).
+:- pragma inline(fa/1).
+
+%------------------------------------------------------------------------%
+
+:- pragma memo(dnf/1).
+
+dnf(R) =
+ ( R = zero ->
+ []
+ ; R = one ->
+ [[]]
+ ;
+ list__map(func(L) = [pos(R ^ value) | L], dnf(R ^ tr)) ++
+ list__map(func(L) = [neg(R ^ value) | L], dnf(R ^ fa))
+ ).
+
+% cnf(R) =
+% ( R = zero ->
+% [[]]
+% ; R = one ->
+% []
+% ;
+% [pos(R ^ value) | cnf(R ^ tr)] `merge_cnf`
+% [neg(R ^ value) | cnf(R ^ fa)]
+% ).
+%
+% :- func merge_cnf(list(list(literal(T))), list(list(literal(T)))) =
+% list(list(literal(T))).
+%
+% merge_cnf(As, Bs) =
+% ( As = [] ->
+% Bs
+% ; Bs = [] ->
+% As
+% ; As = [[]] ->
+% As
+% ; Bs = [[]] % XXX check
+% ;
+% foldl(func(A, Cs0) =
+% foldl(func(B, Cs1) = [A ++ B | Cs1], Bs, Cs0),
+% As, [])
+% ).
+
+% :- pragma foreign_proc("C",
+% print_robdd(F::in, IO0::di, IO::uo),
+% [will_not_call_mercury],
+% "
+% printOut((node *) F);
+% update_io(IO0, IO);
+% ").
+
+print_robdd(F) -->
+ ( { F = one } ->
+ io__write_string("TRUE\n")
+ ; { F = zero } ->
+ io__write_string("FALSE\n")
+ ;
+ { init(Trues) },
+ { init(Falses) },
+ print_robdd_2(F, Trues, Falses)
+ ).
+
+:- pred print_robdd_2(robdd(T)::in, set_unordlist(var(T))::in,
+ set_unordlist(var(T))::in, io__state::di, io__state::uo) is det.
+
+print_robdd_2(F, Trues, Falses) -->
+ ( { F = one } ->
+ { All = to_sorted_list(Trues `union` Falses) },
+ io__write_string("("),
+ list__foldl((pred(Var::in, di, uo) is det -->
+ { Var `set_unordlist__member` Trues ->
+ C = ' '
+ ;
+ C = ('~')
+ },
+ { term__var_to_int(Var, N) },
+ io__format(" %c%02d", [c(C), i(N)])
+ ), All),
+ io__write_string(")\n")
+ ; { F \= zero } ->
+ print_robdd_2(F^tr, Trues `insert` F^value, Falses),
+ print_robdd_2(F^fa, Trues, Falses `insert` F^value)
+ ;
+ % Don't do anything for zero terminal
+ []
+ ).
+
+:- pragma foreign_proc("C",
+ restrict(V::in, F::in) = (R::out),
+ [will_not_call_mercury, promise_pure],
+"
+ R = (MR_Word) restrict(V, (node *) F);
+").
+
+:- pragma foreign_proc("C",
+ restrict_threshold(V::in, F::in) = (R::out),
+ [will_not_call_mercury, promise_pure],
+"
+ R = (MR_Word) restrictThresh(V, (node *) F);
+").
+
+:- pragma memo(rename_vars/2).
+
+rename_vars(Subst, F) =
+ ( is_terminal(F) ->
+ F
+ ;
+ ite(var(Subst(F^value)),
+ rename_vars(Subst, F^tr),
+ rename_vars(Subst, F^fa))
+ ).
+
+% make_node(Var, Then, Else).
+% The make_node() function. WARNING!! If you use this function you are
+% responsible for making sure that the ROBDD invariant holds that all the
+% variables in both the Then and Else sub graphs are > Var.
+
+:- func make_node(var(T), robdd(T), robdd(T)) = robdd(T).
+:- pragma foreign_proc("C",
+ make_node(Var::in, Then::in, Else::in) = (Node::out),
+ [will_not_call_mercury, promise_pure],
+"
+ Node = (MR_Word) make_node((int) Var, (node *) Then, (node *) Else);
+").
+
+not_var(V) = make_node(V, zero, one).
+
+eq_vars(VarA, VarB) = F :-
+ compare(R, VarA, VarB),
+ (
+ R = (=),
+ F = one
+ ;
+ R = (<),
+ F = make_node(VarA, var(VarB), not_var(VarB))
+ ;
+ R = (>),
+ F = make_node(VarB, var(VarA), not_var(VarA))
+ ).
+
+neq_vars(VarA, VarB) = F :-
+ compare(R, VarA, VarB),
+ (
+ R = (=),
+ F = zero
+ ;
+ R = (<),
+ F = make_node(VarA, not_var(VarB), var(VarB))
+ ;
+ R = (>),
+ F = make_node(VarB, not_var(VarA), var(VarA))
+ ).
+
+imp_vars(VarA, VarB) = F :-
+ compare(R, VarA, VarB),
+ (
+ R = (=),
+ F = one
+ ;
+ R = (<),
+ F = make_node(VarA, var(VarB), one)
+ ;
+ R = (>),
+ F = make_node(VarB, one, not_var(VarA))
+ ).
+
+conj_vars(Vars) = foldr(func(V, R) = make_node(V, R, zero), Vars, one).
+
+conj_not_vars(Vars) = foldr(func(V, R) = make_node(V, zero, R), Vars, one).
+
+disj_vars(Vars) = foldr(func(V, R) = make_node(V, one, R), Vars, zero).
+
+at_most_one_of(Vars) = at_most_one_of_2(Vars, one, one).
+
+:- func at_most_one_of_2(vars(T), robdd(T), robdd(T)) = robdd(T).
+
+at_most_one_of_2(Vars, OneOf0, NoneOf0) = R :-
+ list__foldl2(
+ (pred(V::in, One0::in, One::out, None0::in, None::out) is det :-
+ None = make_node(V, zero, None0),
+ One = make_node(V, None0, One0)
+ ), list__reverse(to_sorted_list(Vars)),
+ OneOf0, R, NoneOf0, _).
+
+:- pragma memo(var_restrict_true/2).
+
+var_restrict_true(V, F0) = F :-
+ ( is_terminal(F0) ->
+ F = F0
+ ;
+ compare(R, F0^value, V),
+ (
+ R = (<),
+ F = make_node(F0^value,
+ var_restrict_true(V, F0^tr),
+ var_restrict_true(V, F0^fa))
+ ;
+ R = (=),
+ F = F0^tr
+ ;
+ R = (>),
+ F = F0
+ )
+ ).
+
+:- pragma memo(var_restrict_false/2).
+
+var_restrict_false(V, F0) = F :-
+ ( is_terminal(F0) ->
+ F = F0
+ ;
+ compare(R, F0^value, V),
+ (
+ R = (<),
+ F = make_node(F0^value,
+ var_restrict_false(V, F0^tr),
+ var_restrict_false(V, F0^fa))
+ ;
+ R = (=),
+ F = F0^fa
+ ;
+ R = (>),
+ F = F0
+ )
+ ).
+
+% restrict_true_false_vars(TrueVars, FalseVars, R0) = R :-
+% size(R0, _Nodes, _Depth), % XXX
+% P = (pred(V::in, di, uo) is det --> io__write_int(var_to_int(V))), % XXX
+% unsafe_perform_io(robdd_to_dot(R0, P, "rtf.dot")), % XXX
+% restrict_true_false_vars_2(TrueVars, FalseVars, R0, R).
+%
+% :- pred restrict_true_false_vars_2(vars(T)::in, vars(T)::in,
+% robdd(T)::in, robdd(T)::out) is det.
+%
+% - pragma memo(restrict_true_false_vars_2/4).
+%
+% restrict_true_false_vars_2(TrueVars0, FalseVars0, R0, R) :-
+% ( is_terminal(R0) ->
+% R = R0
+% ; empty(TrueVars0), empty(FalseVars0) ->
+% R = R0
+% ;
+% Var = R0 ^ value,
+% TrueVars = TrueVars0 `remove_leq` Var,
+% FalseVars = FalseVars0 `remove_leq` Var,
+% ( TrueVars0 `contains` Var ->
+% restrict_true_false_vars_2(TrueVars, FalseVars, R0 ^ tr, R)
+% ; FalseVars0 `contains` Var ->
+% restrict_true_false_vars_2(TrueVars, FalseVars, R0 ^ fa, R)
+% ;
+% restrict_true_false_vars_2(TrueVars, FalseVars, R0 ^ tr, R_tr),
+% restrict_true_false_vars_2(TrueVars, FalseVars, R0 ^ fa, R_fa),
+% R = make_node(R0 ^ value, R_tr, R_fa)
+% )
+% ).
+
+restrict_true_false_vars(TrueVars, FalseVars, R0) = R :-
+ restrict_true_false_vars_2(TrueVars, FalseVars, R0, R,
+% hash_table__new(robdd_double_hash, 12, 0.9),
+ init, _).
+
+:- pred restrict_true_false_vars_2(vars(T)::in, vars(T)::in,
+ robdd(T)::in, robdd(T)::out,
+% hash_table(robdd(T), robdd(T))::hash_table_di,
+% hash_table(robdd(T), robdd(T))::hash_table_uo
+ robdd_cache(T)::in, robdd_cache(T)::out) is det.
+
+restrict_true_false_vars_2(TrueVars0, FalseVars0, R0, R, Seen0, Seen) :-
+ ( is_terminal(R0) ->
+ R = R0,
+ Seen = Seen0
+ ; empty(TrueVars0), empty(FalseVars0) ->
+ R = R0,
+ Seen = Seen0
+ ; search(Seen0, R0, R1) ->
+ R = R1,
+ Seen = Seen0
+ ;
+ Var = R0 ^ value,
+ TrueVars = TrueVars0 `remove_leq` Var,
+ FalseVars = FalseVars0 `remove_leq` Var,
+ ( TrueVars0 `contains` Var ->
+ restrict_true_false_vars_2(TrueVars, FalseVars,
+ R0 ^ tr, R, Seen0, Seen2)
+ ; FalseVars0 `contains` Var ->
+ restrict_true_false_vars_2(TrueVars, FalseVars,
+ R0 ^ fa, R, Seen0, Seen2)
+ ;
+ restrict_true_false_vars_2(TrueVars, FalseVars,
+ R0 ^ tr, R_tr, Seen0, Seen1),
+ restrict_true_false_vars_2(TrueVars, FalseVars,
+ R0 ^ fa, R_fa, Seen1, Seen2),
+ R = make_node(R0 ^ value, R_tr, R_fa)
+ ),
+ Seen = det_insert(Seen2, R0, R)
+ ).
+
+:- pred robdd_double_hash(robdd(T)::in, int::out, int::out) is det.
+
+robdd_double_hash(R, H1, H2) :-
+ int_double_hash(node_num(R), H1, H2).
+
+restrict_filter(P, F0) =
+ restrict_filter(P, (pred(_::in) is semidet :- true), F0).
+
+restrict_filter(P, D, F0) = F :-
+ filter_2(P, D, F0, F, map__init, _, map__init, _).
+
+:- type robdd_cache(T) == map(robdd(T), robdd(T)).
+:- type var_cache(T) == map(var(T), bool).
+
+:- pred filter_2(pred(var(T)), pred(var(T)), robdd(T), robdd(T),
+ var_cache(T), var_cache(T), robdd_cache(T), robdd_cache(T)).
+:- mode filter_2(pred(in) is semidet, pred(in) is semidet, in, out, in, out,
+ in, out) is det.
+
+filter_2(P, D, F0, F, SeenVars0, SeenVars, SeenNodes0, SeenNodes) :-
+ ( is_terminal(F0) ->
+ F = F0,
+ SeenVars = SeenVars0,
+ SeenNodes = SeenNodes0
+ ; \+ D(F0^value) ->
+ F = F0,
+ SeenVars = SeenVars0,
+ SeenNodes = SeenNodes0
+ ; map__search(SeenNodes0, F0, F1) ->
+ F = F1,
+ SeenVars = SeenVars0,
+ SeenNodes = SeenNodes0
+ ;
+ filter_2(P, D, F0^tr, Ftrue, SeenVars0, SeenVars1, SeenNodes0,
+ SeenNodes1),
+ filter_2(P, D, F0^fa, Ffalse, SeenVars1, SeenVars2, SeenNodes1,
+ SeenNodes2),
+ V = F0^value,
+ ( map__search(SeenVars0, V, SeenF) ->
+ SeenVars = SeenVars2,
+ (
+ SeenF = yes,
+ F = make_node(V, Ftrue, Ffalse)
+ ;
+ SeenF = no,
+ F = Ftrue + Ffalse
+ )
+ ; P(V) ->
+ F = make_node(V, Ftrue, Ffalse),
+ map__det_insert(SeenVars2, V, yes, SeenVars)
+ ;
+ F = Ftrue + Ffalse,
+ map__det_insert(SeenVars2, V, no, SeenVars)
+ ),
+ map__det_insert(SeenNodes2, F0, F, SeenNodes)
+ ).
+
+squeeze_equiv(LeaderMap, R0) =
+ ( Max = map__max_key(LeaderMap) ->
+ restrict_filter(
+ ( pred(V::in) is semidet :-
+ map__search(LeaderMap, V, L) => L = V
+ ),
+ ( pred(V::in) is semidet :-
+ \+ compare(>, V, Max)
+ ), R0)
+ ;
+ R0
+ ).
+
+make_equiv(LeaderMap) =
+ make_equiv_2(map__sorted_keys(LeaderMap), LeaderMap, init).
+
+:- func make_equiv_2(list(var(T)), map(var(T), var(T)), vars(T)) = robdd(T).
+
+make_equiv_2([], _, _) = one.
+make_equiv_2([V | Vs], LM, Trues) =
+ ( L = V ->
+ make_node(V, make_equiv_2(Vs, LM, Trues `insert` V),
+ make_equiv_2(Vs, LM, Trues))
+ ; Trues `contains` L ->
+ make_node(V, make_equiv_2(Vs, LM, Trues), zero)
+ ;
+ make_node(V, zero, make_equiv_2(Vs, LM, Trues))
+ ) :-
+ L = LM ^ det_elem(V).
+
+expand_equiv(LeaderMap, R0) = R :-
+ expand_equiv_2(map__sorted_keys(LeaderMap), LeaderMap, init, R0, R,
+ map__init, _).
+
+:- pred expand_equiv_2(list(var(T))::in, map(var(T), var(T))::in, vars(T)::in,
+ robdd(T)::in, robdd(T)::out,
+ robdd_cache(T)::in, robdd_cache(T)::out) is det.
+
+expand_equiv_2([], _, _, R, R) --> [].
+expand_equiv_2([V | Vs], LM, Trues, R0, R) -->
+ { L = LM ^ det_elem(V) },
+ ( { R0 = zero } ->
+ { R = zero }
+ ; R1 =^ elem(R0) ->
+ { R = R1 }
+ ; { R0 = one } ->
+ { R = make_equiv_2([V | Vs], LM, Trues) },
+ ^ elem(R0) := R
+ ; { compare((<), R0 ^ value, V) } ->
+ expand_equiv_2([V | Vs], LM, Trues, R0 ^ tr, Rtr),
+ expand_equiv_2([V | Vs], LM, Trues, R0 ^ fa, Rfa),
+ { R = make_node(R0 ^ value, Rtr, Rfa) },
+ ^ elem(R0) := R
+ ; { compare((<), V, R0 ^ value) } ->
+ ( { L = V } ->
+ expand_equiv_2(Vs, LM, Trues `insert` V, R0, Rtr),
+ expand_equiv_2(Vs, LM, Trues, R0, Rfa),
+ { R = make_node(V, Rtr, Rfa) },
+ ^ elem(R0) := R
+ ; { Trues `contains` L } ->
+ expand_equiv_2(Vs, LM, Trues, R0, Rtr),
+ { R = make_node(V, Rtr, zero) },
+ ^ elem(R0) := R
+ ;
+ expand_equiv_2(Vs, LM, Trues, R0, Rfa),
+ { R = make_node(V, zero, Rfa) },
+ ^ elem(R0) := R
+ )
+ ; { L = V } ->
+ expand_equiv_2(Vs, LM, Trues `insert` V, R0 ^ tr, Rtr),
+ expand_equiv_2(Vs, LM, Trues, R0 ^ fa, Rfa),
+ { R = make_node(V, Rtr, Rfa) },
+ ^ elem(R0) := R
+ ; { Trues `contains` L } ->
+ expand_equiv_2(Vs, LM, Trues, R0 ^ tr, Rtr),
+ { R = make_node(V, Rtr, zero) },
+ ^ elem(R0) := R
+ ;
+ expand_equiv_2(Vs, LM, Trues, R0 ^ fa, Rfa),
+ { R = make_node(V, zero, Rfa) },
+ ^ elem(R0) := R
+ ).
+
+%------------------------------------------------------------------------%
+
+% XXX this could be made much more efficient by doing something similar
+% to what we do in expand_equiv.
+
+expand_implications(ImpVars, R) = R ^
+ expand_implications_2(not_var, var, Imps) ^
+ expand_implications_2(var, not_var, RevImps) ^
+ expand_implications_2(not_var, not_var, DisImps) ^
+ expand_implications_2(var, var, RevDisImps) :-
+ ImpVars = imp_vars(Imps, RevImps, DisImps, RevDisImps).
+
+:- func expand_implications_2(func(var(T)) = robdd(T), func(var(T)) = robdd(T),
+ imp_map(T), robdd(T)) = robdd(T).
+
+expand_implications_2(FA, FB, IM, R0) =
+ map__foldl(func(VA, Vs, R1) =
+ foldl(func(VB, R2) =
+ R2 * (FA(VA) + FB(VB)),
+ Vs, R1),
+ IM, R0).
+
+%------------------------------------------------------------------------%
+:- pragma foreign_proc("C",
+ is_terminal(F::in),
+ [will_not_call_mercury, thread_safe, promise_pure],
+"
+ SUCCESS_INDICATOR = IS_TERMINAL(F);
+").
+
+size(F, Nodes, Depth) :-
+ size(F, Nodes, Depth, _).
+
+size(F, Nodes, Depth, Vars) :-
+ size_2(F, 0, Nodes, 0, Depth, 0, set_bbbtree__init, Seen),
+ Vars = sort_and_remove_dups(list__map(value, to_sorted_list(Seen))).
+
+ % XXX should see if sparse_bitset is more efficient than set_bbbtree.
+:- pred size_2(robdd(T)::in, int::in, int::out, int::in, int::out, int::in,
+ set_bbbtree(robdd(T))::in, set_bbbtree(robdd(T))::out) is det.
+
+size_2(F, Nodes0, Nodes, Depth0, Depth, Val0, Seen0, Seen) :-
+
+ ( is_terminal(F) ->
+ Nodes = Nodes0, Depth = Depth0, Seen = Seen0
+ ; term__var_to_int(F^value) =< Val0 ->
+ error("robdd invariant broken (possible loop)")
+ ; F `member` Seen0 ->
+ Nodes = Nodes0, Depth = Depth0, Seen = Seen0
+ ;
+ Val = term__var_to_int(F^value),
+ size_2(F^tr, Nodes0+1, Nodes1, Depth0, Depth1, Val,
+ Seen0, Seen1),
+ size_2(F^fa, Nodes1, Nodes, Depth0, Depth2, Val,
+ Seen1, Seen2),
+ max(Depth1, Depth2, Max),
+ Depth = Max + 1,
+ Seen = Seen2 `insert` F
+ ).
+
+var_is_constrained(F, V) :-
+ ( is_terminal(F) ->
+ fail
+ ;
+ compare(R, F^value, V),
+ (
+ R = (<),
+ ( var_is_constrained(F^tr, V)
+ ; var_is_constrained(F^fa, V)
+ )
+ ;
+ R = (=)
+ )
+ ).
+
+vars_are_constrained(F, Vs) :-
+ vars_are_constrained_2(F, to_sorted_list(Vs)).
+
+:- pred vars_are_constrained_2(robdd(T)::in, list(var(T))::in) is semidet.
+
+vars_are_constrained_2(_, []).
+vars_are_constrained_2(F, Vs) :-
+ Vs = [V | Vs1],
+ ( is_terminal(F) ->
+ fail
+ ;
+ compare(R, F^value, V),
+ (
+ R = (<),
+ Vs2 = Vs
+ ;
+ R = (=),
+ Vs2 = Vs1
+ ),
+ ( vars_are_constrained_2(F^tr, Vs2)
+ ; vars_are_constrained_2(F^fa, Vs2)
+ )
+ ).
+
+robdd_to_dot(Robdd, WV, Filename) -->
+ io__tell(Filename, Result),
+ (
+ { Result = ok },
+ robdd_to_dot(Robdd, WV),
+ io__told
+ ;
+ { Result = error(Err) },
+ io__stderr_stream(StdErr),
+ io__nl(StdErr),
+ io__write_string(StdErr, io__error_message(Err)),
+ io__nl(StdErr)
+ ).
+
+robdd_to_dot(Robdd, WV) -->
+ io__write_string(
+"digraph G{
+ center=true;
+ size=""7,11"";
+ ordering=out;
+ node [shape=record,height=.1];
+ concentrate=true;
+"),
+ { multi_map__init(Ranks0) },
+ robdd_to_dot_2(Robdd, WV, set_bbbtree__init, _, Ranks0, Ranks),
+ map__foldl((pred(_::in, Nodes::in, di, uo) is det -->
+ io__write_string("{rank = same; "),
+ list__foldl((pred(Node::in, di, uo) is det -->
+ io__format("%s; ", [s(node_name(Node))])), Nodes),
+ io__write_string("}\n")
+ ), Ranks),
+ io__write_string("}\n").
+
+ % XXX should see if sparse_bitset is more efficient than set_bbbtree.
+:- pred robdd_to_dot_2(robdd(T)::in, write_var(T)::in(write_var),
+ set_bbbtree(robdd(T))::in, set_bbbtree(robdd(T))::out,
+ multi_map(var(T), robdd(T))::in,
+ multi_map(var(T), robdd(T))::out,
+ io__state::di, io__state::uo) is det.
+
+robdd_to_dot_2(Robdd, WV, Seen0, Seen, Ranks0, Ranks) -->
+ ( { is_terminal(Robdd) } ->
+ { Seen = Seen0 },
+ { Ranks = Ranks0 }
+ ; { Robdd `member` Seen0 } ->
+ { Seen = Seen0 },
+ { Ranks = Ranks0 }
+ ;
+ robdd_to_dot_2(Robdd^tr, WV, Seen0, Seen1, Ranks0, Ranks1),
+ robdd_to_dot_2(Robdd^fa, WV, Seen1, Seen2, Ranks1, Ranks2),
+ write_node(Robdd, WV),
+ write_edge(Robdd, Robdd^tr, yes),
+ write_edge(Robdd, Robdd^fa, no),
+ { Seen = Seen2 `insert` Robdd },
+ { multi_map__set(Ranks2, Robdd^value, Robdd, Ranks) }
+ ).
+
+:- pred write_node(robdd(T)::in, write_var(T)::in(write_var),
+ io__state::di, io__state::uo) is det.
+
+write_node(R, WV) -->
+ io__format("%s [label=""<f0> %s|<f1> ",
+ [s(node_name(R)), s(terminal_name(R^tr))]),
+ WV(R^value),
+ io__format("|<f2> %s", [s(terminal_name(R^fa))]),
+ io__write_string("""];\n").
+
+:- func node_name(robdd(T)) = string.
+
+node_name(R) =
+ ( R = one ->
+ "true"
+ ; R = zero ->
+ "false"
+ ;
+ string__format("node%d", [i(node_num(R))])
+ ).
+
+:- func node_num(robdd(T)) = int.
+:- pragma foreign_proc("C",
+ node_num(R::in) = (N::out),
+ [will_not_call_mercury, promise_pure],
+"
+ N = (Integer) R;
+").
+
+:- func terminal_name(robdd(T)) = string.
+
+terminal_name(R) =
+ ( R = zero ->
+ "0"
+ ; R = one ->
+ "1"
+ ;
+ ""
+ ).
+
+:- pred write_edge(robdd(T)::in, robdd(T)::in, bool::in,
+ io__state::di, io__state::uo) is det.
+
+write_edge(R0, R1, Arc) -->
+ ( { is_terminal(R1) } ->
+ []
+ ;
+ io__format("""%s"":%s -> ""%s"":f1 [label=""%s""];\n",
+ [s(node_name(R0)), s(Arc = yes -> "f0" ; "f2"),
+ s(node_name(R1)), s(Arc = yes -> "t" ; "f")])
+ ).
+
+labelling(Vars, R, TrueVars, FalseVars) :-
+ labelling_2(to_sorted_list(Vars), R, empty_vars_set, TrueVars,
+ empty_vars_set, FalseVars).
+
+:- pred labelling_2(list(var(T))::in, robdd(T)::in, vars(T)::in,
+ vars(T)::out, vars(T)::in, vars(T)::out) is nondet.
+
+labelling_2([], _, TrueVars, TrueVars, FalseVars, FalseVars).
+labelling_2([V | Vs], R0, TrueVars0, TrueVars, FalseVars0, FalseVars) :-
+ R = var_restrict_false(V, R0),
+ R \= zero,
+ labelling_2(Vs, R, TrueVars0, TrueVars, FalseVars0 `insert` V,
+ FalseVars).
+labelling_2([V | Vs], R0, TrueVars0, TrueVars, FalseVars0, FalseVars) :-
+ R = var_restrict_true(V, R0),
+ R \= zero,
+ labelling_2(Vs, R, TrueVars0 `insert` V, TrueVars, FalseVars0,
+ FalseVars).
+
+minimal_model(Vars, R, TrueVars, FalseVars) :-
+ ( empty(Vars) ->
+ TrueVars = empty_vars_set,
+ FalseVars = empty_vars_set
+ ;
+ minimal_model_2(to_sorted_list(Vars), R, empty_vars_set,
+ TrueVars0, empty_vars_set, FalseVars0),
+ (
+ TrueVars = TrueVars0,
+ FalseVars = FalseVars0
+ ;
+ minimal_model(Vars, R * (~conj_vars(TrueVars0)),
+ TrueVars, FalseVars)
+ )
+ ).
+
+:- pred minimal_model_2(list(var(T))::in, robdd(T)::in, vars(T)::in,
+ vars(T)::out, vars(T)::in, vars(T)::out) is semidet.
+
+minimal_model_2([], _, TrueVars, TrueVars, FalseVars, FalseVars).
+minimal_model_2([V | Vs], R0, TrueVars0, TrueVars, FalseVars0, FalseVars) :-
+ R1 = var_restrict_false(V, R0),
+ ( R1 \= zero ->
+ minimal_model_2(Vs, R1, TrueVars0, TrueVars,
+ FalseVars0 `insert` V, FalseVars)
+ ;
+ R2 = var_restrict_true(V, R0),
+ R2 \= zero,
+ minimal_model_2(Vs, R2, TrueVars0 `insert` V, TrueVars,
+ FalseVars0, FalseVars)
+ ).
+
+%-----------------------------------------------------------------------------%
+
+:- pragma promise_pure(clear_caches/2).
+clear_caches -->
+ { impure clear_caches }.
+
+:- pragma foreign_proc("C",
+ clear_caches,
+ [will_not_call_mercury],
+"
+ init_caches();
+").
+
+%-----------------------------------------------------------------------------%
+%-----------------------------------------------------------------------------%
Index: library/sparse_bitset.m
===================================================================
RCS file: /home/mercury1/repository/mercury/library/sparse_bitset.m,v
retrieving revision 1.16
diff -u -b -r1.16 sparse_bitset.m
--- library/sparse_bitset.m 2002/07/23 08:26:27 1.16
+++ library/sparse_bitset.m 2002/08/19 03:44:05
@@ -114,6 +114,12 @@
:- pred contains(sparse_bitset(T), T) <= enum(T).
:- mode contains(in, in) is semidet.
+ % 'member(X, Set) is true iff 'X' is a member of 'Set'.
+ % For the (in, in) mode, use 'contains/2' instead since it is more
+ % efficient.
+:- pred member(T, sparse_bitset(T)) <= enum(T).
+:- mode member(out, in) is nondet.
+
% `insert(Set, X)' returns the union
% of `Set' and the set containing only `X'.
% Takes O(rep_size(Set)) time and space.
@@ -168,6 +174,20 @@
:- pred remove_list(sparse_bitset(T), list(T), sparse_bitset(T)) <= enum(T).
:- mode remove_list(in, in, out) is semidet.
+ % `remove_leq(Set, X)' returns the list Set with all elements less than
+ % or equal to X removed.
+:- func remove_leq(sparse_bitset(T), T) = sparse_bitset(T) <= enum(T).
+
+:- pred remove_leq(sparse_bitset(T), T, sparse_bitset(T)) <= enum(T).
+:- mode remove_leq(in, in, out) is det.
+
+ % `remove_gt(Set, X)' returns the list Set with all elements greater
+ % than X removed.
+:- func remove_gt(sparse_bitset(T), T) = sparse_bitset(T) <= enum(T).
+
+:- pred remove_gt(sparse_bitset(T), T, sparse_bitset(T)) <= enum(T).
+:- mode remove_gt(in, in, out) is det.
+
% `remove_least(Set0, X, Set)' is true iff `X' is the
% least element in `Set0', and `Set' is the set which
% contains all the elements of `Set0' except `X'.
@@ -214,6 +234,9 @@
% Takes O(card(Set)) time.
:- func foldl(func(T, U) = U, sparse_bitset(T), U) = U <= enum(T).
+:- pred foldl(pred(T, U, U), sparse_bitset(T), U, U) <= enum(T).
+:- mode foldl(pred(in, in, out) is det, in, in, out) is det.
+
% `foldr(Func, Set, Start)' calls Func with each element
% of `Set' (in reverse sorted order) and an accumulator
% (with the initial value of `Start'), and returns
@@ -221,6 +244,10 @@
% Takes O(card(Set)) time.
:- func foldr(func(T, U) = U, sparse_bitset(T), U) = U <= enum(T).
+ % `filter(Pred, Set)' removes element from Set for which Pred fails.
+:- func filter(pred(T), sparse_bitset(T)) = sparse_bitset(T) <= enum(T).
+:- mode filter(pred(in) is semidet, in) = out is det.
+
%-----------------------------------------------------------------------------%
:- implementation.
@@ -330,6 +357,10 @@
foldl(F, sparse_bitset(Set), Acc0) = foldl_2(F, Set, Acc0).
+foldl(P, S, Acc0, Acc) :-
+ F = (func(E, A0) = A :- P(E, A0, A)),
+ Acc = foldl(F, S, Acc0).
+
:- func foldl_2(func(T, U) = U, bitset_impl, U) = U <= enum(T).
:- pragma type_spec(foldl_2/3, T = int).
:- pragma type_spec(foldl_2/3, T = var(_)).
@@ -412,6 +443,12 @@
%-----------------------------------------------------------------------------%
+% XXX could make this more efficient.
+
+filter(P, S) = S ^ to_sorted_list ^ list__filter(P) ^ sorted_list_to_set.
+
+%-----------------------------------------------------------------------------%
+
count(Set) = foldl((func(_, Acc) = Acc + 1), Set, 0).
%-----------------------------------------------------------------------------%
@@ -461,6 +498,62 @@
%-----------------------------------------------------------------------------%
+remove_leq(sparse_bitset(Set), Elem) =
+ sparse_bitset(remove_leq_2(Set, enum__to_int(Elem))).
+
+:- func remove_leq_2(bitset_impl, int) = bitset_impl.
+
+remove_leq_2([], _) = [].
+remove_leq_2([Data | Rest], Index) = Result :-
+ Offset = Data ^ offset,
+ Result =
+ ( Offset + bits_per_int =< Index ->
+ remove_leq_2(Rest, Index)
+ ; Offset =< Index ->
+ (
+ Bits = Data ^ bits /\
+ unchecked_left_shift(\ 0,
+ Index - Offset + 1),
+ Bits \= 0
+ ->
+ [make_bitset_elem(Offset, Bits) | Rest]
+ ;
+ Rest
+ )
+ ;
+ [Data | Rest]
+ ).
+
+%-----------------------------------------------------------------------------%
+
+remove_gt(sparse_bitset(Set), Elem) =
+ sparse_bitset(remove_gt_2(Set, enum__to_int(Elem))).
+
+:- func remove_gt_2(bitset_impl, int) = bitset_impl.
+
+remove_gt_2([], _) = [].
+remove_gt_2([Data | Rest], Index) = Result :-
+ Offset = Data ^ offset,
+ Result =
+ ( Offset + bits_per_int - 1 =< Index ->
+ [Data | remove_gt_2(Rest, Index)]
+ ; Offset =< Index ->
+ (
+ Bits = Data ^ bits /\
+ \ unchecked_left_shift(\ 0,
+ Index - Offset + 1),
+ Bits \= 0
+ ->
+ [make_bitset_elem(Offset, Bits)]
+ ;
+ []
+ )
+ ;
+ []
+ ).
+
+%-----------------------------------------------------------------------------%
+
remove_least(sparse_bitset(Set0), Elem, sparse_bitset(Set)) :-
Set0 = [First | Rest],
Bits0 = First ^ bits,
@@ -625,6 +718,16 @@
%-----------------------------------------------------------------------------%
+member(X, Set0) :-
+ remove_least(Set0, X0, Set),
+ (
+ X = X0
+ ;
+ member(X, Set)
+ ).
+
+%-----------------------------------------------------------------------------%
+
:- func rest(bitset_impl::in(bound([ground | ground]))) =
(bitset_impl::out) is det.
rest([_ | Rest]) = Rest.
@@ -799,6 +902,10 @@
remove(A, B, remove(A, B)).
remove_list(A, B, remove_list(A, B)).
+
+remove_leq(A, B, remove_leq(A, B)).
+
+remove_gt(A, B, remove_gt(A, B)).
list_to_set(A, list_to_set(A)).
Index: library/term.m
===================================================================
RCS file: /home/mercury1/repository/mercury/library/term.m,v
retrieving revision 1.101
diff -u -b -r1.101 term.m
--- library/term.m 2002/07/09 01:30:24 1.101
+++ library/term.m 2002/08/19 03:47:05
@@ -1,5 +1,5 @@
%---------------------------------------------------------------------------%
-% Copyright (C) 1993-2000 The University of Melbourne.
+% Copyright (C) 1993-2001 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.
%---------------------------------------------------------------------------%
@@ -299,6 +299,11 @@
% Different variables map to different ints.
% Other than that, the mapping is unspecified.
+:- func term__var_supply_max_var(var_supply(T)) = var(T).
+% term__var_supply_max_var(VarSupply):
+% returns the highest numbered variable returned from this
+% var_supply.
+
%-----------------------------------------------------------------------------%
% Given a term context, return the source line number.
@@ -1077,7 +1082,7 @@
% We number variables using sequential numbers,
term__create_var(var_supply(V0), var(V), var_supply(V)) :-
- V is V0 + 1.
+ V = V0 + 1.
%------------------------------------------------------------------------------%
@@ -1095,6 +1100,8 @@
% Cast an integer to a var(T), subverting the type-checking.
:- func unsafe_int_to_var(int) = var(T).
term__unsafe_int_to_var(Var) = var(Var).
+
+term__var_supply_max_var(var_supply(V)) = var(V).
%-----------------------------------------------------------------------------%
Index: library/tree234.m
===================================================================
RCS file: /home/mercury1/repository/mercury/library/tree234.m,v
retrieving revision 1.35
diff -u -b -r1.35 tree234.m
--- library/tree234.m 2002/03/28 03:44:40 1.35
+++ library/tree234.m 2002/08/19 03:51:00
@@ -1,5 +1,5 @@
%---------------------------------------------------------------------------%
-% Copyright (C) 1994-1997,1999-2000,2002 The University of Melbourne.
+% Copyright (C) 1994-1997,1999-2002 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.
%---------------------------------------------------------------------------%
@@ -52,6 +52,10 @@
:- pred tree234__upper_bound_lookup(tree234(K, V), K, K, V).
:- mode tree234__upper_bound_lookup(in, in, out, out) is det.
+:- func tree234__max_key(tree234(K, V)) = K is semidet.
+
+:- func tree234__min_key(tree234(K, V)) = K is semidet.
+
:- pred tree234__insert(tree234(K, V), K, V, tree234(K, V)).
:- mode tree234__insert(in, in, in, out) is semidet.
% :- mode tree234__insert(di_tree234, in, in, uo_tree234) is semidet.
@@ -622,6 +626,30 @@
;
report_lookup_error("tree234__upper_bound_lookup: key not found.",
SearchK, V)
+ ).
+
+%------------------------------------------------------------------------------%
+
+tree234__max_key(T0) = MaxKey :-
+ ( T0 = two(NodeMaxKey, _, _, NodeMaxSubtree)
+ ; T0 = three(_, _, NodeMaxKey, _, _, _, NodeMaxSubtree)
+ ; T0 = four(_, _, _, _, NodeMaxKey, _, _, _, _, NodeMaxSubtree)
+ ),
+ ( MaxSubtreeKey = tree234__max_key(NodeMaxSubtree) ->
+ MaxKey = MaxSubtreeKey
+ ;
+ MaxKey = NodeMaxKey
+ ).
+
+tree234__min_key(T0) = MinKey :-
+ ( T0 = two(NodeMinKey, _, NodeMinSubtree, _)
+ ; T0 = three(NodeMinKey, _, _, _, NodeMinSubtree, _, _)
+ ; T0 = four(NodeMinKey, _, _, _, _, _, NodeMinSubtree, _, _, _)
+ ),
+ ( MinSubtreeKey = tree234__min_key(NodeMinSubtree) ->
+ MinKey = MinSubtreeKey
+ ;
+ MinKey = NodeMinKey
).
%------------------------------------------------------------------------------%
Index: library/varset.m
===================================================================
RCS file: /home/mercury1/repository/mercury/library/varset.m,v
retrieving revision 1.66
diff -u -b -r1.66 varset.m
--- library/varset.m 2002/07/09 01:30:26 1.66
+++ library/varset.m 2002/08/14 00:38:36
@@ -229,6 +229,8 @@
:- func varset__coerce(varset(T)) = varset(U).
+:- func varset__max_var(varset(T)) = var(T).
+
:- implementation.
%-----------------------------------------------------------------------------%
@@ -599,6 +601,10 @@
% generated by the compiler, but type coercion by
% copying was taking about 3% of the compiler's runtime.
private_builtin__unsafe_type_cast(A, B).
+
+%-----------------------------------------------------------------------------%
+
+varset__max_var(varset(VarSupply, _, _)) = term__var_supply_max_var(VarSupply).
%-----------------------------------------------------------------------------%
%-----------------------------------------------------------------------------%
cvs diff: Diffing deep_profiler
Index: deep_profiler/canonical.m
===================================================================
RCS file: /home/mercury1/repository/mercury/deep_profiler/canonical.m,v
retrieving revision 1.2
diff -u -b -r1.2 canonical.m
--- deep_profiler/canonical.m 2001/07/03 08:16:17 1.2
+++ deep_profiler/canonical.m 2002/08/19 03:20:53
@@ -1,5 +1,5 @@
%-----------------------------------------------------------------------------%
-% Copyright (C) 2001 The University of Melbourne.
+% Copyright (C) 2002 The University of Melbourne.
% This file may only be copied under the terms of the GNU General
% Public License - see the file COPYING in the Mercury distribution.
%-----------------------------------------------------------------------------%
@@ -22,8 +22,8 @@
:- implementation.
:- import_module measurements, callgraph, array_util.
-:- import_module unsafe, io.
-:- import_module std_util, bool, int, array, list, map, set, require.
+:- import_module io, std_util, bool, int, array, list, map, set, require.
+% :- import_module unsafe.
:- type merge_info
---> merge_info(
@@ -525,16 +525,16 @@
),
lookup_multi_sites(RestArrays, SlotNum, CSDLists).
-:- pragma promise_pure(record_pd_redirect/4).
+% :- pragma promise_pure(record_pd_redirect/4).
:- pred record_pd_redirect(list(proc_dynamic_ptr)::in, proc_dynamic_ptr::in,
redirect::in, redirect::out) is det.
record_pd_redirect(RestPDPtrs, PrimePDPtr, Redirect0, Redirect) :-
- impure unsafe_perform_io(io__write_string("pd redirect: ")),
- impure unsafe_perform_io(io__print(RestPDPtrs)),
- impure unsafe_perform_io(io__write_string(" -> ")),
- impure unsafe_perform_io(io__print(PrimePDPtr)),
- impure unsafe_perform_io(io__nl),
+ % impure unsafe_perform_io(io__write_string("pd redirect: ")),
+ % impure unsafe_perform_io(io__print(RestPDPtrs)),
+ % impure unsafe_perform_io(io__write_string(" -> ")),
+ % impure unsafe_perform_io(io__print(PrimePDPtr)),
+ % impure unsafe_perform_io(io__nl),
lookup_pd_redirect(Redirect0 ^ pd_redirect, PrimePDPtr, OldRedirect),
( OldRedirect = proc_dynamic_ptr(0) ->
record_pd_redirect_2(RestPDPtrs, PrimePDPtr,
@@ -560,16 +560,16 @@
Redirect1 = Redirect0 ^ pd_redirect := ProcRedirect,
record_pd_redirect_2(RestPDPtrs, PrimePDPtr, Redirect1, Redirect).
-:- pragma promise_pure(record_csd_redirect/4).
+% :- pragma promise_pure(record_csd_redirect/4).
:- pred record_csd_redirect(list(call_site_dynamic_ptr)::in,
call_site_dynamic_ptr::in, redirect::in, redirect::out) is det.
record_csd_redirect(RestCSDPtrs, PrimeCSDPtr, Redirect0, Redirect) :-
- impure unsafe_perform_io(io__write_string("csd redirect: ")),
- impure unsafe_perform_io(io__print(RestCSDPtrs)),
- impure unsafe_perform_io(io__write_string(" -> ")),
- impure unsafe_perform_io(io__print(PrimeCSDPtr)),
- impure unsafe_perform_io(io__nl),
+ % impure unsafe_perform_io(io__write_string("csd redirect: ")),
+ % impure unsafe_perform_io(io__print(RestCSDPtrs)),
+ % impure unsafe_perform_io(io__write_string(" -> ")),
+ % impure unsafe_perform_io(io__print(PrimeCSDPtr)),
+ % impure unsafe_perform_io(io__nl),
lookup_csd_redirect(Redirect0 ^ csd_redirect, PrimeCSDPtr, OldRedirect),
( OldRedirect = call_site_dynamic_ptr(0) ->
record_csd_redirect_2(RestCSDPtrs, PrimeCSDPtr,
Index: deep_profiler/unsafe.m
===================================================================
RCS file: unsafe.m
diff -N unsafe.m
--- /tmp/cvsSBoof1 Mon Aug 19 14:00:47 2002
+++ /dev/null Tue Aug 6 19:10:00 2002
@@ -1,84 +0,0 @@
-%-----------------------------------------------------------------------------%
-% Copyright (C) 1997 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: unsafe.m
-% Author: fjh
-% Stability: low
-%-----------------------------------------------------------------------------%
-
-/*
-** WARNING: the procedures defined in this module are non-logical.
-** They may have side effects, they may violate type safety,
-** they may interfere with certain memory management strategies,
-** and in general they may do lots of nasty things.
-** They may not work with future release of the Mercury compiler,
-** or with other Mercury implementations.
-** Use only as a last resort, and only with great care!
-**
-** You have been warned.
-*/
-
-%-----------------------------------------------------------------------------%
-
-:- module unsafe.
-:- interface.
-:- import_module io.
-
-/*
-** unsafe_perform_io/1 performs I/O, in an unsafe manner.
-** It can be used to call a goal that does I/O or has
-** side effects from a context where you do not have an io__state.
-** It can be useful for printf-style debugging.
-** But backtracking over a call to `unsafe_perform_io'
-** can be very dangerous indeed, because with certain
-** memory allocation policies it can result in dangling pointers.
-*/
-:- impure pred unsafe_perform_io(pred(io__state, io__state)).
-:- mode unsafe_perform_io(pred(di, uo) is det) is det.
-:- mode unsafe_perform_io(pred(di, uo) is cc_multi) is det.
-
-/*
-** The function unsafe_promise_ground/1 can be used to assert to the
-** compiler that a particular value of inst `any' is in fact ground.
-** The assertion is *not* checked. If it is false, all hell may break out.
-*/
-:- func unsafe_promise_ground(T::in(any)) = (T::out) is det.
-
-%-----------------------------------------------------------------------------%
-%-----------------------------------------------------------------------------%
-
-:- implementation.
-
-%-----------------------------------------------------------------------------%
-
-:- pragma c_code(unsafe_promise_ground(X::in(any)) = (Y::out), "Y = X;").
-
-%-----------------------------------------------------------------------------%
-
-:- pragma c_code(
-unsafe_perform_io(P::(pred(di, uo) is det)),
- may_call_mercury,
-"{
- call_io_pred_det(P);
-}").
-:- pragma c_code(
-unsafe_perform_io(P::(pred(di, uo) is cc_multi)),
- may_call_mercury,
-"{
- call_io_pred_cc_multi(P);
-}").
-
-:- pred call_io_pred(pred(io__state, io__state), io__state, io__state).
-:- mode call_io_pred(pred(di, uo) is det, di, uo) is det.
-:- mode call_io_pred(pred(di, uo) is cc_multi, di, uo) is cc_multi.
-
-:- pragma export(call_io_pred(pred(di, uo) is det, di, uo),
- "call_io_pred_det").
-:- pragma export(call_io_pred(pred(di, uo) is cc_multi, di, uo),
- "call_io_pred_cc_multi").
-
-call_io_pred(P) --> P.
-
-%-----------------------------------------------------------------------------%
cvs diff: Diffing deep_profiler/notes
cvs diff: Diffing doc
Index: doc/Mmakefile
===================================================================
RCS file: /home/mercury1/repository/mercury/doc/Mmakefile,v
retrieving revision 1.31
diff -u -b -r1.31 Mmakefile
--- doc/Mmakefile 2002/05/13 08:09:39 1.31
+++ doc/Mmakefile 2002/08/19 00:13:50
@@ -192,6 +192,10 @@
;; \
$(LIBRARY_DIR)/table_builtin.m) \
;; \
+ $(LIBRARY_DIR)/robdd.m) \
+ ;; \
+ $(LIBRARY_DIR)/unsafe.m) \
+ ;; \
*) \
echo "* `basename $$filename .m`::"; \
;; \
@@ -211,6 +215,10 @@
$(LIBRARY_DIR)/rtti_implementation.m) \
;; \
$(LIBRARY_DIR)/table_builtin.m) \
+ ;; \
+ $(LIBRARY_DIR)/robdd.m) \
+ ;; \
+ $(LIBRARY_DIR)/unsafe.m) \
;; \
*) \
file="`basename $$filename .m`"; \
--------------------------------------------------------------------------
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