[m-rev.] diff/for review: library changes from mode_constraints branch (part 1)
Zoltan Somogyi
zs at cs.mu.OZ.AU
Wed Dec 15 16:34:16 AEDT 2004
Move changes in the library on the mode-constraints branch onto the trunk.
This was reviewed a while ago. I wanted to hold off committing it until
after the release, but Richard will need this soon. Unless I hear an
objection, I plan to commit this tomorrow, and the changes on the
mode_constraints branch in the compiler early next week.
Zoltan.
library/eqvclass.m:
Add some utility functions and predicates.
library/map.m:
Add some utility functions and predicates, and some type
specialization directives.
library/tree234.m:
Add some utility functions and predicates.
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.
Make the list of modules easier to maintain (especially in the case
of CVS conflicts) by listing one module per line.
Fix formatting of some foreign_procs.
NEWS:
Mention the new predicates and functions.
Mmake.workspace:
Add a new make variable that specifies the location of the robdd
subdirectory.
Mmakefile:
Add rules for handling the robdd subdirectory.
configure.in:
Check whether the compiler can handle local foreign_decls, since
robdd.m now needs this.
tools/bootcheck:
Add the robdd subdirectory to the stage 2 & 3 directories.
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.
robdd/Makefile:
Update the set of default compilation flags. The main code in this
directory, bryant.c, is #included in library/robdd.m, and the only
other programs in this directory are test programs.
robdd/Mmakefile:
New file. Includes a mechanism to compile bryant.c in the robdd
subdirectory, since this can give cleaner error messages than
compiling library/robdd.m.
robdd/bryant.[ch]:
Huge cleanup of these files. Add MR_ROBDD_ prefixes to global symbols,
make the formatting conform to our standards, and fix irregularities
in the uses of the macros that control the use of optional facilities.
robdd/bryantPrint.[ch]:
robdd/table.[ch]:
robdd/test_abexit.c:
robdd/test_abunify.c:
robdd/test_abglb.c:
robdd/test_iff.c:
robdd/test_rename.c:
robdd/test_restrict.c:
robdd/test_rglb.c:
robdd/test_upclose.c:
robdd/test_var.c:
robdd/test_vars.c:
robdd/timing.[ch]:
robdd/var.h:
Conform to the changes in bryant.h. Note that since the code in these
files won't end up in Mercury program code, they don't need to be
namespace clean.
runtime/mercury.h:
runtime/mercury_heap.h:
runtime/mercury_init.h:
runtime/mercury_memory.h:
#define GC_I_HIDE_POINTERS before each #include of gc.h (bryant.c
hides pointers). This impact of this #define is so small that it is
not measurable.
runtime/RESERVED_MACRO_NAMES:
library/RESERVED_MACRO_NAMES:
Add HIDE_POINTER and REVEAL_POINTER, since defining GC_I_HIDE_POINTERS
makes these macros from gc.h visible.
runtime/mercury_reg_workarounds.[ch]:
Add the MR_memset function.
tests/debugger/declarative/if_then_else.{inp,exp}:
tests/debugger/declarative/ite_2.{inp,exp,exp2}:
Avoid a name conflict with the predicate ite in robdd.m.
cvs diff: Diffing .
Index: Mmake.workspace
===================================================================
RCS file: /home/mercury1/repository/mercury/Mmake.workspace,v
retrieving revision 1.15
diff -u -r1.15 Mmake.workspace
--- Mmake.workspace 27 Oct 2003 06:00:27 -0000 1.15
+++ Mmake.workspace 27 Oct 2003 06:02:45 -0000
@@ -54,6 +54,7 @@
MPS_GC_DIR = $(WORKSPACE)/mps_gc/code
COMPILER_DIR = $(WORKSPACE)/compiler
UTIL_DIR = $(WORKSPACE)/util
+ROBDD_DIR = $(WORKSPACE)/robdd
ANALYSIS_DIR = $(WORKSPACE)/analysis
# Specify the MPS "platform"
Index: Mmakefile
===================================================================
RCS file: /home/mercury1/repository/mercury/Mmakefile,v
retrieving revision 1.105
diff -u -r1.105 Mmakefile
--- Mmakefile 8 Feb 2004 11:16:44 -0000 1.105
+++ Mmakefile 11 Feb 2004 03:41:26 -0000
@@ -27,6 +27,7 @@
util \
boehm_gc \
runtime \
+ robdd \
library \
trace \
browser \
@@ -173,6 +174,10 @@
.PHONY: runtime
runtime: scripts boehm_gc
+cd runtime && $(SUBDIR_MMAKE)
+
+.PHONY: robdd
+robdd: scripts boehm_gc
+ cd robdd && $(SUBDIR_MMAKE)
.PHONY: library
library: dep_library scripts util boehm_gc runtime
Index: NEWS
===================================================================
RCS file: /home/mercury1/repository/mercury/NEWS,v
retrieving revision 1.353
diff -u -r1.353 NEWS
--- NEWS 14 Dec 2004 07:33:28 -0000 1.353
+++ NEWS 14 Dec 2004 07:36:27 -0000
@@ -259,6 +259,18 @@
These have been replaced by cc_multi versions in which success or failure
is indicated by returning a maybe type.
+* We've added functions get_equivalent_elements, get_minimum_element and
+ remove_equivalent_elements 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.
+
+* builtin.m now contains types and insts `unify' and `compare' for use
+ in defining user-defined equality and comparison predicates.
+
* The following predicates, which were added in 0.11.0, have been deprecated:
io.current_input_stream/3
io.current_output_stream/3
Index: configure.in
===================================================================
RCS file: /home/mercury1/repository/mercury/configure.in,v
retrieving revision 1.408
diff -u -r1.408 configure.in
--- configure.in 11 Dec 2004 01:59:50 -0000 1.408
+++ configure.in 13 Dec 2004 02:14:09 -0000
@@ -208,6 +208,8 @@
:- pred return_rtti_version(int::out) is det.
+ :- pragma foreign_decl("C", local, "").
+
:- type x ---> x.
:- pragma foreign_type("C", x, "MR_Integer",
[[can_pass_as_mercury_type, stable]]).
cvs diff: Diffing analysis
cvs diff: Diffing bindist
cvs diff: Diffing boehm_gc
cvs diff: Diffing boehm_gc/Mac_files
cvs diff: Diffing boehm_gc/cord
cvs diff: Diffing boehm_gc/cord/private
cvs diff: Diffing boehm_gc/doc
cvs diff: Diffing boehm_gc/include
cvs diff: Diffing boehm_gc/include/private
cvs diff: Diffing boehm_gc/tests
cvs diff: Diffing browser
Index: browser/RESERVED_MACRO_NAMES
===================================================================
RCS file: /home/mercury1/repository/mercury/browser/RESERVED_MACRO_NAMES,v
retrieving revision 1.2
diff -u -r1.2 RESERVED_MACRO_NAMES
--- browser/RESERVED_MACRO_NAMES 20 May 2003 03:18:05 -0000 1.2
+++ browser/RESERVED_MACRO_NAMES 31 Aug 2003 12:32:35 -0000
@@ -30,6 +30,8 @@
# These are defined by boehm_gc/gc.h.
__GC
_GC_H
+HIDE_POINTER
+REVEAL_POINTER
#-----------------------------------------------------------------------------#
# This is defined by mps_gc/code/mercury_mps.h,
# which uses this macro for its header guard.
cvs diff: Diffing bytecode
cvs diff: Diffing debian
cvs diff: Diffing deep_profiler
Index: deep_profiler/unsafe.m
===================================================================
RCS file: deep_profiler/unsafe.m
diff -N deep_profiler/unsafe.m
--- deep_profiler/unsafe.m 7 Aug 2002 01:43:29 -0000 1.2
+++ /dev/null 1 Jan 1970 00:00:00 -0000
@@ -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.37
diff -u -r1.37 Mmakefile
--- doc/Mmakefile 21 Jan 2004 05:05:34 -0000 1.37
+++ doc/Mmakefile 22 Jan 2004 21:02:30 -0000
@@ -236,6 +236,10 @@
;; \
$(LIBRARY_DIR)/table_builtin.m) \
;; \
+ $(LIBRARY_DIR)/robdd.m) \
+ ;; \
+ $(LIBRARY_DIR)/unsafe.m) \
+ ;; \
$(LIBRARY_DIR)/term_size_prof_builtin.m) \
;; \
*) \
@@ -257,6 +261,10 @@
$(LIBRARY_DIR)/rtti_implementation.m) \
;; \
$(LIBRARY_DIR)/table_builtin.m) \
+ ;; \
+ $(LIBRARY_DIR)/robdd.m) \
+ ;; \
+ $(LIBRARY_DIR)/unsafe.m) \
;; \
$(LIBRARY_DIR)/term_size_prof_builtin.m) \
;; \
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
Index: library/Mmakefile
===================================================================
RCS file: /home/mercury1/repository/mercury/library/Mmakefile,v
retrieving revision 1.136
diff -u -r1.136 Mmakefile
--- library/Mmakefile 1 Nov 2004 04:46:20 -0000 1.136
+++ library/Mmakefile 6 Dec 2004 04:32:54 -0000
@@ -102,7 +102,7 @@
#-----------------------------------------------------------------------------#
-CFLAGS += $(DLL_CFLAGS) -I$(TRACE_DIR)
+CFLAGS += $(DLL_CFLAGS) -I$(TRACE_DIR) -I$(ROBDD_DIR)
MLFLAGS += -R$(FINAL_INSTALL_MERC_LIB_DIR) \
-R$(FINAL_INSTALL_MERC_GC_LIB_DIR)
MCFLAGS += -R$(FINAL_INSTALL_MERC_LIB_DIR) \
Index: library/RESERVED_MACRO_NAMES
===================================================================
RCS file: /home/mercury1/repository/mercury/library/RESERVED_MACRO_NAMES,v
retrieving revision 1.2
diff -u -r1.2 RESERVED_MACRO_NAMES
--- library/RESERVED_MACRO_NAMES 20 May 2003 03:18:09 -0000 1.2
+++ library/RESERVED_MACRO_NAMES 31 Aug 2003 12:31:40 -0000
@@ -30,6 +30,8 @@
# These are defined by boehm_gc/gc.h.
__GC
_GC_H
+HIDE_POINTER
+REVEAL_POINTER
#-----------------------------------------------------------------------------#
# This is defined by mps_gc/code/mercury_mps.h,
# which uses this macro for its header guard.
Index: library/eqvclass.m
===================================================================
RCS file: /home/mercury1/repository/mercury/library/eqvclass.m,v
retrieving revision 1.13
diff -u -r1.13 eqvclass.m
--- library/eqvclass.m 17 Aug 2003 13:30:11 -0000 1.13
+++ library/eqvclass.m 19 Aug 2003 00:54:01 -0000
@@ -106,6 +106,21 @@
:- 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.
+
+:- 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.
+
+:- 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.
+
+:- func eqvclass__remove_equivalent_elements(eqvclass(T), T) = eqvclass(T).
+
%---------------------------------------------------------------------------%
:- implementation.
@@ -334,3 +349,24 @@
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(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
+ ).
Index: library/library.m
===================================================================
RCS file: /home/mercury1/repository/mercury/library/library.m,v
retrieving revision 1.77
diff -u -r1.77 library.m
--- library/library.m 14 Dec 2004 07:33:32 -0000 1.77
+++ library/library.m 14 Dec 2004 07:36:32 -0000
@@ -87,6 +87,7 @@
:- import_module rbtree.
:- import_module relation.
:- import_module require.
+:- import_module robdd.
:- import_module set.
:- import_module set_bbbtree.
:- import_module set_ordlist.
@@ -118,6 +119,12 @@
:- import_module table_builtin.
:- import_module term_size_prof_builtin.
+% If you need access to unsafe predicates, then in your own workspace,
+% temporarily uncomment this import and the line for unsafe in the definition
+% of mercury_std_library_module.
+
+% :- import_module unsafe.
+
% library__version must be implemented using pragma foreign_proc,
% so we can get at the MR_VERSION and MR_FULLARCH configuration
% parameters. We can't just generate library.m from library.m.in
@@ -204,6 +211,7 @@
mercury_std_library_module("rbtree").
mercury_std_library_module("relation").
mercury_std_library_module("require").
+mercury_std_library_module("robdd").
mercury_std_library_module("rtti_implementation").
mercury_std_library_module("set").
mercury_std_library_module("set_bbbtree").
@@ -223,6 +231,7 @@
mercury_std_library_module("time").
mercury_std_library_module("tree234").
mercury_std_library_module("type_desc").
+% mercury_std_library_module("unsafe").
mercury_std_library_module("varset").
mercury_std_library_module("version_array").
mercury_std_library_module("version_array2d").
Index: library/map.m
===================================================================
RCS file: /home/mercury1/repository/mercury/library/map.m,v
retrieving revision 1.89
diff -u -r1.89 map.m
--- library/map.m 12 Jan 2004 06:04:09 -0000 1.89
+++ library/map.m 12 Jan 2004 06:56:34 -0000
@@ -72,6 +72,12 @@
% Aborts if there is no key with the given or higher value.
:- pred map__upper_bound_lookup(map(K, V)::in, K::in, K::out, V::out) is det.
+ % Return the largest key in the map, if there is one.
+:- func map__max_key(map(K,V)) = K is semidet.
+
+ % Return the smallest key in the map, if there is one.
+:- func map__min_key(map(K,V)) = K is semidet.
+
% Search map for data.
:- pred map__inverse_search(map(K, V)::in, V::in, K::out) is nondet.
@@ -281,6 +287,14 @@
:- mode map__map_foldl(pred(in, in, out, in, out) is semidet, in, out, in, out)
is semidet.
+ % As map__map_foldl, but with two accumulators.
+:- pred map__map_foldl2(pred(K, V, W, A, A, B, B), map(K, V), map(K, W),
+ A, A, B, B).
+:- mode map__map_foldl2(pred(in, in, out, in, out, in, out) is det,
+ in, out, in, out, in, out) is det.
+:- mode map__map_foldl2(pred(in, in, out, in, out, in, out) is semidet,
+ in, out, in, out, in, out) is semidet.
+
% Given two maps M1 and M2, create a third map M3 that has only the
% keys that occur in both M1 and M2. For keys that occur in both M1
% and M2, compute the value in the final map by applying the supplied
@@ -390,6 +404,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.
@@ -442,6 +469,10 @@
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).
@@ -643,8 +674,11 @@
map__map_values(Pred, Map0, Map) :-
tree234__map_values(Pred, Map0, Map).
-map__map_foldl(Pred, Map0, Map, Acc0, Acc) :-
- tree234__map_foldl(Pred, Map0, Map, Acc0, Acc).
+map__map_foldl(Pred, !Map, !Acc) :-
+ tree234__map_foldl(Pred, !Map, !Acc).
+
+map__map_foldl2(Pred, !Map, !Acc1, !Acc2) :-
+ tree234__map_foldl2(Pred, !Map, !Acc1, !Acc2).
%-----------------------------------------------------------------------------%
Index: library/pprint.m
===================================================================
RCS file: /home/mercury1/repository/mercury/library/pprint.m,v
retrieving revision 1.15
diff -u -r1.15 pprint.m
--- library/pprint.m 15 Mar 2004 06:50:16 -0000 1.15
+++ library/pprint.m 15 Mar 2004 06:56:48 -0000
@@ -369,7 +369,8 @@
:- implementation.
-:- import_module array, map, sparse_bitset, enum, term, exception, ops.
+:- import_module array, map, sparse_bitset, enum, term, exception.
+:- import_module ops, robdd.
:- type doc
---> 'NIL'
@@ -685,6 +686,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, Priority, X)
).
@@ -947,6 +951,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) =
@@ -1010,5 +1034,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 - 1, dnf(R))).
%-----------------------------------------------------------------------------%
Index: library/robdd.m
===================================================================
RCS file: library/robdd.m
diff -N library/robdd.m
--- /dev/null 1 Jan 1970 00:00:00 -0000
+++ library/robdd.m 25 May 2004 21:11:40 -0000
@@ -0,0 +1,1549 @@
+%---------------------------------------------------------------------------%
+% 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: 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.
+
+% XXX This module is not yet sufficiently well tested or documented to be
+% included in the publically available part of the library, so at the moment
+% it is not included in the list of modules mentioned in the library manual.
+
+%-----------------------------------------------------------------------------%
+%-----------------------------------------------------------------------------%
+
+:- 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.
+
+:- type entailment_result(T)
+ ---> all_vars
+ ; some_vars(vars :: T).
+
+:- type vars_entailed_result(T) == entailment_result(vars(T)).
+
+ % 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.
+
+%---------------------------------------------------------------------------%
+
+% We use this type to represent equivalence classes. Each equivalence class
+% has a leader, which represents the entire class; this will be variable
+% in the equivalence class that has the smallest variable number.
+%
+% The map maps each variable to its leader. This specifically includes the
+% leader itself, i.e. there will be an entry mapping the leader to itself.
+% Several of the predicates below depend on this invariant.
+
+:- type leader_map(T) == map(var(T), var(T)).
+
+:- type equiv_vars(T) --->
+ equiv_vars(
+ leader_map :: leader_map(T)
+ ).
+
+:- type equivalent_result(T) == entailment_result(equiv_vars(T)).
+
+:- func equivalent_vars(robdd(T)) = equivalent_result(T).
+
+%---------------------------------------------------------------------------%
+
+% It is an invariant in all maps in an imp_vars that all keys are
+% less than or equal to all the values they map to.
+%
+% There is no requirement that a key of the any of the maps, including
+% imps and rev_imps, appears among the values it maps to, although logically
+% both K => K and ~K => ~K hold.
+
+:- type imp_map(T) == map(var(T), vars(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)
+ ).
+
+:- 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(equiv_vars(T), robdd(T)) = robdd(T).
+
+ % make_equiv(Equivalences) = Robdd:
+ % Robdd is the constraint representing all the equivalences
+ % in Equivalences.
+:- func make_equiv(equiv_vars(T)) = robdd(T).
+
+ % add_equivalences(Equivalences, Robbd0) = Robdd:
+ % Robdd is the constraint Robdd0 conjoined with
+ % robdds representing all the equivalences in Equivalences.
+:- func add_equivalences(equiv_vars(T), robdd(T)) = robdd(T).
+
+ % add_implications(Implications, Robbd0) = Robdd:
+ % Robdd is the constraint Robdd0 conjoined with
+ % robdds representing all the implications in Implications.
+:- func add_implications(imp_vars(T), robdd(T)) = robdd(T).
+
+ % remove_implications_from_robdd(Implications, Robbd0) = Robdd:
+ % Robdd is the constraint Robdd0 conjoined with
+ % robdds representing all the implications in Implications.
+:- 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 bool, int, string, std_util, require.
+:- import_module list, assoc_list, map, multi_map.
+:- import_module set_unordlist, set_bbbtree, 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", local, "
+#define MR_ROBDD_CLEAR_CACHES
+#define MR_ROBDD_COMPUTED_TABLE
+#define MR_ROBDD_EQUAL_TEST
+#define MR_ROBDD_USE_ITE_CONSTANT
+#define MR_ROBDD_NEW
+#define MR_ROBDD_RESTRICT_SET
+
+#include ""bryant.h""
+
+#ifdef MR_HIGHLEVEL_DATA
+ typedef MR_Box MR_ROBDD_NODE_TYPE;
+#else
+ typedef MR_Word MR_ROBDD_NODE_TYPE;
+#endif
+").
+
+:- pragma foreign_code("C", "
+#define NDEBUG
+#include ""bryant.c""
+").
+
+:- pragma no_inline(one/0).
+:- pragma foreign_proc("C",
+ one = (F::out),
+ [will_not_call_mercury, promise_pure],
+"
+ F = (MR_ROBDD_NODE_TYPE) MR_ROBDD_trueVar();
+").
+
+:- pragma no_inline(zero/0).
+:- pragma foreign_proc("C",
+ zero = (F::out),
+ [will_not_call_mercury, promise_pure],
+"
+ F = (MR_ROBDD_NODE_TYPE) MR_ROBDD_falseVar();
+").
+
+:- pragma no_inline(var/1).
+:- pragma foreign_proc("C",
+ var(V::in) = (F::out),
+ [will_not_call_mercury, promise_pure],
+"
+ F = (MR_ROBDD_NODE_TYPE) MR_ROBDD_variableRep(V);
+").
+
+:- pragma no_inline(ite/3).
+:- pragma foreign_proc("C",
+ ite(F::in, G::in, H::in) = (ITE::out),
+ [will_not_call_mercury, promise_pure],
+"
+ ITE = (MR_ROBDD_NODE_TYPE) MR_ROBDD_ite((MR_ROBDD_node *) F,
+ (MR_ROBDD_node *) G, (MR_ROBDD_node *) H);
+").
+
+:- pragma no_inline(ite_var/3).
+:- pragma foreign_proc("C",
+ ite_var(V::in, G::in, H::in) = (ITE::out),
+ [will_not_call_mercury, promise_pure],
+"
+ ITE = (MR_ROBDD_NODE_TYPE) MR_ROBDD_ite_var(V, (MR_ROBDD_node *) G,
+ (MR_ROBDD_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
+ ).
+
+:- 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_ROBDD_NODE_TYPE) MR_ROBDD_glb((MR_ROBDD_node *) X,
+ (MR_ROBDD_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 no_inline((+)/2).
+:- pragma foreign_proc("C",
+ (X::in) + (Y::in) = (F::out),
+ [will_not_call_mercury, promise_pure],
+"
+ F = (MR_ROBDD_NODE_TYPE) MR_ROBDD_lub((MR_ROBDD_node *) X,
+ (MR_ROBDD_node *) Y);
+").
+
+:- pragma no_inline((=<)/2).
+:- pragma foreign_proc("C",
+ ((X::in) =< (Y::in)) = (F::out),
+ [will_not_call_mercury, promise_pure],
+"
+ F = (MR_ROBDD_NODE_TYPE) MR_ROBDD_implies((MR_ROBDD_node *) X,
+ (MR_ROBDD_node *) Y);
+").
+
+(F =:= G) = ite(F, G, ~G).
+
+(F =\= G) = ite(F, ~G, G).
+
+(~F) = ite(F, zero, one).
+
+:- pragma no_inline(entails/2).
+:- pragma foreign_proc("C",
+ entails(X::in, Y::in),
+ [will_not_call_mercury, promise_pure],
+"
+ SUCCESS_INDICATOR = (MR_ROBDD_ite_constant((MR_ROBDD_node *) X,
+ (MR_ROBDD_node *) Y, MR_ROBDD_one) == MR_ROBDD_one);
+").
+
+:- pragma no_inline(var_entailed/2).
+:- pragma foreign_proc("C",
+ var_entailed(F::in, V::in),
+ [will_not_call_mercury, promise_pure],
+"
+ SUCCESS_INDICATOR = MR_ROBDD_var_entailed((MR_ROBDD_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 leader_to_eqvclass(T) ---> leader_to_eqvclass(map(var(T), vars(T))).
+
+:- func equivalent_vars_2(robdd(T)) =
+ entailment_result(leader_to_eqvclass(T)).
+
+:- pragma memo(equivalent_vars_2/1).
+
+equivalent_vars_2(R) = EQ :-
+ ( R = one ->
+ EQ = some_vars(leader_to_eqvclass(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(
+ leader_to_eqvclass(M0)),
+ map__det_insert(M0, R ^ value, Vars,
+ M),
+ EQ = some_vars(leader_to_eqvclass(M))
+ )
+ )
+ )
+ ).
+
+:- func rev_map(entailment_result(leader_to_eqvclass(T))) =
+ equivalent_result(T).
+
+rev_map(all_vars) = all_vars.
+rev_map(some_vars(leader_to_eqvclass(EQ0))) = some_vars(equiv_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(K, IM) =
+ ( Vs = IM ^ elem(K) ->
+ % In case Vs doesn't already contain K
+ Vs `insert` K
+ ;
+ 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(leader_to_eqvclass(T)) where [
+ ( leader_to_eqvclass(MapA) `intersection` leader_to_eqvclass(MapB) =
+ leader_to_eqvclass(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 inline(value/1).
+:- pragma foreign_proc("C",
+ value(F::in) = (Value::out),
+ [will_not_call_mercury, promise_pure],
+"
+ Value = (MR_ROBDD_NODE_TYPE) ((MR_ROBDD_node *) F)->value;
+").
+
+:- pragma inline(tr/1).
+:- pragma foreign_proc("C",
+ tr(F::in) = (Tr::out),
+ [will_not_call_mercury, promise_pure],
+"
+ Tr = (MR_ROBDD_NODE_TYPE) ((MR_ROBDD_node *) F)->tr;
+").
+
+:- pragma inline(fa/1).
+:- pragma foreign_proc("C",
+ fa(F::in) = (Fa::out),
+ [will_not_call_mercury, promise_pure],
+"
+ Fa = (MR_ROBDD_NODE_TYPE) ((MR_ROBDD_node *) F)->fa;
+").
+
+%------------------------------------------------------------------------%
+
+:- 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((MR_ROBDD_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_ROBDD_NODE_TYPE) MR_ROBDD_restrict(V, (MR_ROBDD_node *) F);
+").
+
+:- pragma foreign_proc("C",
+ restrict_threshold(V::in, F::in) = (R::out),
+ [will_not_call_mercury, promise_pure],
+"
+ R = (MR_ROBDD_NODE_TYPE) MR_ROBDD_restrictThresh(V,
+ (MR_ROBDD_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_ROBDD_NODE_TYPE) MR_ROBDD_make_node((int) Var,
+ (MR_ROBDD_node *) Then, (MR_ROBDD_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 :-
+% The following code may be useful during debugging, but it is commented out
+% since it should not be needed otherwise.
+% 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,
+ init, _).
+
+:- pred restrict_true_false_vars_2(vars(T)::in, vars(T)::in,
+ robdd(T)::in, robdd(T)::out,
+ 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(equiv_vars(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(equiv_vars(LeaderMap)) =
+ make_equiv_2(map__to_sorted_assoc_list(LeaderMap), init).
+
+:- func make_equiv_2(assoc_list(var(T)), vars(T)) = robdd(T).
+
+make_equiv_2([], _) = one.
+make_equiv_2([Var - LeaderVar | Vs], Trues) = Robdd :-
+ ( Var = LeaderVar ->
+ Robdd = make_node(Var, make_equiv_2(Vs, Trues `insert` Var),
+ make_equiv_2(Vs, Trues))
+ ; Trues `contains` LeaderVar ->
+ Robdd = make_node(Var, make_equiv_2(Vs, Trues), zero)
+ ;
+ var_to_int(Var, VarNum),
+ var_to_int(LeaderVar, LeaderVarNum),
+ require(LeaderVarNum < VarNum, "make_equiv_2: unordered vars"),
+ % Since LeaderVar < Var, and every leader must
+ % appear in an equivalence with itself, an ancestor
+ % invocation of this predicate must already have seen
+ % LeaderVar. If it is not in Trues, it must
+ % therefore be false.
+ Robdd = make_node(Var, zero, make_equiv_2(Vs, Trues))
+ ).
+
+add_equivalences(equiv_vars(LeaderMap), R0) = R :-
+ add_equivalences_2(map__to_sorted_assoc_list(LeaderMap), init, R0, R,
+ map__init, _).
+
+:- pred add_equivalences_2(assoc_list(var(T))::in, vars(T)::in,
+ robdd(T)::in, robdd(T)::out,
+ robdd_cache(T)::in, robdd_cache(T)::out) is det.
+
+add_equivalences_2([], _, R, R, !Cache).
+add_equivalences_2([Var - LeaderVar | Vs], Trues, R0, R, !Cache) :-
+ ( R0 = zero ->
+ R = zero
+ ; R1 = !.Cache ^ elem(R0) ->
+ R = R1
+ ; R0 = one ->
+ R = make_equiv_2([Var - LeaderVar | Vs], Trues),
+ !:Cache = !.Cache ^ elem(R0) := R
+ ; compare((<), R0 ^ value, Var) ->
+ add_equivalences_2([Var - LeaderVar | Vs], Trues,
+ R0 ^ tr, Rtr, !Cache),
+ add_equivalences_2([Var - LeaderVar | Vs], Trues,
+ R0 ^ fa, Rfa, !Cache),
+ % This step can make R exponentially bigger than R0.
+ R = make_node(R0 ^ value, Rtr, Rfa),
+ !:Cache = !.Cache ^ elem(R0) := R
+ ; compare((<), Var, R0 ^ value) ->
+ ( LeaderVar = Var ->
+ add_equivalences_2(Vs, Trues `insert` Var,
+ R0, Rtr, !Cache),
+ add_equivalences_2(Vs, Trues, R0, Rfa, !Cache),
+ % This step can make R exponentially bigger than R0.
+ R = make_node(Var, Rtr, Rfa),
+ !:Cache = !.Cache ^ elem(R0) := R
+ ; Trues `contains` LeaderVar ->
+ add_equivalences_2(Vs, Trues, R0, Rtr, !Cache),
+ R = make_node(Var, Rtr, zero),
+ !:Cache = !.Cache ^ elem(R0) := R
+ ;
+ add_equivalences_2(Vs, Trues, R0, Rfa, !Cache),
+ % Since LeaderVar < Var, and every leader must
+ % appear in an equivalence with itself, an ancestor
+ % invocation of this predicate must already have seen
+ % LeaderVar. If it is not in Trues, it must
+ % therefore be false.
+ R = make_node(Var, zero, Rfa),
+ !:Cache = !.Cache ^ elem(R0) := R
+ )
+ ; LeaderVar = Var ->
+ add_equivalences_2(Vs, Trues `insert` Var,
+ R0 ^ tr, Rtr, !Cache),
+ add_equivalences_2(Vs, Trues, R0 ^ fa, Rfa, !Cache),
+ R = make_node(Var, Rtr, Rfa),
+ !:Cache = !.Cache ^ elem(R0) := R
+ ; Trues `contains` LeaderVar ->
+ add_equivalences_2(Vs, Trues, R0 ^ tr, Rtr, !Cache),
+ R = make_node(Var, Rtr, zero),
+ !:Cache = !.Cache ^ elem(R0) := R
+ ;
+ add_equivalences_2(Vs, Trues, R0 ^ fa, Rfa, !Cache),
+ % Since LeaderVar < Var, and every leader must
+ % appear in an equivalence with itself, an ancestor
+ % invocation of this predicate must already have seen
+ % LeaderVar. If it is not in Trues, it must
+ % therefore be false.
+ R = make_node(Var, zero, Rfa),
+ !:Cache = !.Cache ^ elem(R0) := R
+ ).
+
+%------------------------------------------------------------------------%
+
+% XXX this could be made much more efficient by doing something similar
+% to what we do in add_equivalences.
+
+add_implications(ImpVars, R) = R ^
+ add_implications_2(not_var, var, Imps) ^
+ add_implications_2(var, not_var, RevImps) ^
+ add_implications_2(not_var, not_var, DisImps) ^
+ add_implications_2(var, var, RevDisImps) :-
+ ImpVars = imp_vars(Imps, RevImps, DisImps, RevDisImps).
+
+:- func add_implications_2(func(var(T)) = robdd(T), func(var(T)) = robdd(T),
+ imp_map(T), robdd(T)) = robdd(T).
+
+add_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 no_inline(is_terminal/1).
+:- pragma foreign_proc("C",
+ is_terminal(F::in),
+ [will_not_call_mercury, thread_safe, promise_pure],
+"
+ SUCCESS_INDICATOR = MR_ROBDD_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 no_inline(clear_caches/0).
+:- pragma foreign_proc("C",
+ clear_caches,
+ [will_not_call_mercury],
+"
+ MR_ROBDD_init_caches();
+").
+
+%-----------------------------------------------------------------------------%
+%-----------------------------------------------------------------------------%
Index: library/sparse_bitset.m
===================================================================
RCS file: /home/mercury1/repository/mercury/library/sparse_bitset.m,v
retrieving revision 1.20
diff -u -r1.20 sparse_bitset.m
--- library/sparse_bitset.m 15 Jan 2004 05:19:16 -0000 1.20
+++ library/sparse_bitset.m 15 Jan 2004 07:22:01 -0000
@@ -186,6 +186,22 @@
:- 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 `Set' with all elements less than
+ % or equal to `X' removed. In other words, it returns the set
+ % containing all the elements of `Set' which are greater than `X'.
+:- 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 `Set' with all elements greater
+ % than `X' removed. In other words, it returns the set containing
+ % all the elements of `Set' which are less than or equal to `X'.
+:- 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'.
@@ -255,6 +271,12 @@
:- mode foldr(pred(in, di, uo) is cc_multi, in, di, uo) is cc_multi.
:- mode foldr(pred(in, in, out) is cc_multi, in, in, out) is cc_multi.
+ % `filter(Pred, Set)' removes those elements from `Set' for which
+ % `Pred' fails. In other words, it returns the set consisting of those
+ % elements of `Set' for which `Pred' succeeds.
+:- func filter(pred(T), sparse_bitset(T)) = sparse_bitset(T) <= enum(T).
+:- mode filter(pred(in) is semidet, in) = out is det.
+
%-----------------------------------------------------------------------------%
:- implementation.
@@ -490,6 +512,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).
%-----------------------------------------------------------------------------%
@@ -539,6 +567,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,
@@ -928,6 +1012,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.108
diff -u -r1.108 term.m
--- library/term.m 14 Dec 2004 01:07:21 -0000 1.108
+++ library/term.m 14 Dec 2004 01:11:49 -0000
@@ -378,6 +378,9 @@
:- pred term__term_to_type_with_int_instead_of_char(term(U)::in, T::out)
is semidet.
+ % Returns the highest numbered variable returned from this var_supply.
+:- func term__var_supply_max_var(var_supply(T)) = var(T).
+
%-----------------------------------------------------------------------------%
%-----------------------------------------------------------------------------%
@@ -998,6 +1001,8 @@
:- 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.42
diff -u -r1.42 tree234.m
--- library/tree234.m 28 Sep 2004 02:09:14 -0000 1.42
+++ library/tree234.m 28 Sep 2004 02:32:51 -0000
@@ -64,6 +64,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.
@@ -174,6 +178,13 @@
:- mode tree234__map_foldl(pred(in, in, out, in, out) is semidet,
in, out, in, out) is semidet.
+:- pred tree234__map_foldl2(pred(K, V, W, A, A, B, B),
+ tree234(K, V), tree234(K, W), A, A, B, B).
+:- mode tree234__map_foldl2(pred(in, in, out, in, out, in, out) is det,
+ in, out, in, out, in, out) is det.
+:- mode tree234__map_foldl2(pred(in, in, out, in, out, in, out) is semidet,
+ in, out, in, out, in, out) is semidet.
+
%------------------------------------------------------------------------------%
%------------------------------------------------------------------------------%
@@ -653,6 +664,30 @@
%------------------------------------------------------------------------------%
+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
+ ).
+
+%------------------------------------------------------------------------------%
+
tree234__update(Tin, K, V, Tout) :-
(
Tin = empty,
@@ -2478,31 +2513,57 @@
%------------------------------------------------------------------------------%
-tree234__map_foldl(_Pred, empty, empty, A, A).
-tree234__map_foldl(Pred, Tree0, Tree, A0, A) :-
+tree234__map_foldl(_Pred, empty, empty, !A).
+tree234__map_foldl(Pred, Tree0, Tree, !A) :-
+ Tree0 = two(K0, V0, Left0, Right0),
+ Tree = two(K0, W0, Left, Right),
+ tree234__map_foldl(Pred, Left0, Left, !A),
+ call(Pred, K0, V0, W0, !A),
+ tree234__map_foldl(Pred, Right0, Right, !A).
+tree234__map_foldl(Pred, Tree0, Tree, !A) :-
+ Tree0 = three(K0, V0, K1, V1, Left0, Middle0, Right0),
+ Tree = three(K0, W0, K1, W1, Left, Middle, Right),
+ tree234__map_foldl(Pred, Left0, Left, !A),
+ call(Pred, K0, V0, W0, !A),
+ tree234__map_foldl(Pred, Middle0, Middle, !A),
+ call(Pred, K1, V1, W1, !A),
+ tree234__map_foldl(Pred, Right0, Right, !A).
+tree234__map_foldl(Pred, Tree0, Tree, !A) :-
+ Tree0 = four(K0, V0, K1, V1, K2, V2, Left0, LMid0, RMid0, Right0),
+ Tree = four(K0, W0, K1, W1, K2, W2, Left, LMid, RMid, Right),
+ tree234__map_foldl(Pred, Left0, Left, !A),
+ call(Pred, K0, V0, W0, !A),
+ tree234__map_foldl(Pred, LMid0, LMid, !A),
+ call(Pred, K1, V1, W1, !A),
+ tree234__map_foldl(Pred, RMid0, RMid, !A),
+ call(Pred, K2, V2, W2, !A),
+ tree234__map_foldl(Pred, Right0, Right, !A).
+
+tree234__map_foldl2(_Pred, empty, empty, !A, !B).
+tree234__map_foldl2(Pred, Tree0, Tree, !A, !B) :-
Tree0 = two(K0, V0, Left0, Right0),
Tree = two(K0, W0, Left, Right),
- tree234__map_foldl(Pred, Left0, Left, A0, A1),
- call(Pred, K0, V0, W0, A1, A2),
- tree234__map_foldl(Pred, Right0, Right, A2, A).
-tree234__map_foldl(Pred, Tree0, Tree, A0, A) :-
+ tree234__map_foldl2(Pred, Left0, Left, !A, !B),
+ call(Pred, K0, V0, W0, !A, !B),
+ tree234__map_foldl2(Pred, Right0, Right, !A, !B).
+tree234__map_foldl2(Pred, Tree0, Tree, !A, !B) :-
Tree0 = three(K0, V0, K1, V1, Left0, Middle0, Right0),
Tree = three(K0, W0, K1, W1, Left, Middle, Right),
- tree234__map_foldl(Pred, Left0, Left, A0, A1),
- call(Pred, K0, V0, W0, A1, A2),
- tree234__map_foldl(Pred, Middle0, Middle, A2, A3),
- call(Pred, K1, V1, W1, A3, A4),
- tree234__map_foldl(Pred, Right0, Right, A4, A).
-tree234__map_foldl(Pred, Tree0, Tree, A0, A) :-
+ tree234__map_foldl2(Pred, Left0, Left, !A, !B),
+ call(Pred, K0, V0, W0, !A, !B),
+ tree234__map_foldl2(Pred, Middle0, Middle, !A, !B),
+ call(Pred, K1, V1, W1, !A, !B),
+ tree234__map_foldl2(Pred, Right0, Right, !A, !B).
+tree234__map_foldl2(Pred, Tree0, Tree, !A, !B) :-
Tree0 = four(K0, V0, K1, V1, K2, V2, Left0, LMid0, RMid0, Right0),
Tree = four(K0, W0, K1, W1, K2, W2, Left, LMid, RMid, Right),
- tree234__map_foldl(Pred, Left0, Left, A0, A1),
- call(Pred, K0, V0, W0, A1, A2),
- tree234__map_foldl(Pred, LMid0, LMid, A2, A3),
- call(Pred, K1, V1, W1, A3, A4),
- tree234__map_foldl(Pred, RMid0, RMid, A4, A5),
- call(Pred, K2, V2, W2, A5, A6),
- tree234__map_foldl(Pred, Right0, Right, A6, A).
+ tree234__map_foldl2(Pred, Left0, Left, !A, !B),
+ call(Pred, K0, V0, W0, !A, !B),
+ tree234__map_foldl2(Pred, LMid0, LMid, !A, !B),
+ call(Pred, K1, V1, W1, !A, !B),
+ tree234__map_foldl2(Pred, RMid0, RMid, !A, !B),
+ call(Pred, K2, V2, W2, !A, !B),
+ tree234__map_foldl2(Pred, Right0, Right, !A, !B).
%------------------------------------------------------------------------------%
Index: library/unsafe.m
===================================================================
RCS file: library/unsafe.m
diff -N library/unsafe.m
--- /dev/null 1 Jan 1970 00:00:00 -0000
+++ library/unsafe.m 16 Aug 2002 01:12:10 -0000
@@ -0,0 +1,89 @@
+%-----------------------------------------------------------------------------%
+% 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 foreign_proc("C",
+ unsafe_promise_ground(X::in(any)) = (Y::out),
+ [will_not_call_mercury, promise_pure],
+"
+ Y = X;
+").
+
+%-----------------------------------------------------------------------------%
+
+:- pragma foreign_proc("C",
+ unsafe_perform_io(P::(pred(di, uo) is det)),
+ [may_call_mercury],
+"{
+ call_io_pred_det(P);
+}").
+:- pragma foreign_proc("C",
+ 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.
+
+%-----------------------------------------------------------------------------%
Index: library/varset.m
===================================================================
RCS file: /home/mercury1/repository/mercury/library/varset.m,v
retrieving revision 1.70
diff -u -r1.70 varset.m
--- library/varset.m 21 Dec 2003 05:00:41 -0000 1.70
+++ library/varset.m 21 Dec 2003 05:42:49 -0000
@@ -217,6 +217,15 @@
:- implementation.
+% Everything below here is not intended to be part of the public interface,
+% and will not be included in the Mercury library reference manual.
+
+:- interface.
+
+ % Returns the highest numbered variable returned from this varset's
+ % var_supply.
+:- func varset__max_var(varset(T)) = var(T).
+
%-----------------------------------------------------------------------------%
:- implementation.
@@ -574,6 +583,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 profiler
cvs diff: Diffing robdd
Index: robdd/Makefile
===================================================================
RCS file: /home/mercury1/repository/mercury/robdd/Makefile,v
retrieving revision 1.1
diff -u -r1.1 Makefile
--- robdd/Makefile 10 Mar 2000 05:17:20 -0000 1.1
+++ robdd/Makefile 27 Feb 2003 02:12:35 -0000
@@ -1,5 +1,9 @@
+#-----------------------------------------------------------------------------#
+# Copyright (C) 2001-2003 University of Melbourne.
+# This file may only be copied under the terms of the GNU General
+# Public Licence - see the file COPYING in the Mercury distribution.
+#-----------------------------------------------------------------------------#
# File : Makefile
-# RCS : $Id: Makefile,v 1.1 2000/03/10 05:17:20 dmo Exp $
# Author : Peter Schachte
# Origin : 1995
# Purpose : Makefile for bryant graph (ROBDD) manipulation code
@@ -39,7 +43,8 @@
MV=mv
MKDIR=mkdir
DEBUG=-g -DDEBUGALL
-OPTIMIZE=-O3 -DNDEBUG -funroll-loops
+#OPTIMIZE=-O3 -DNDEBUG -funroll-loops
+OPTIMIZE=-DNDEBUG
CC=gcc -I../mylib -I/usr/ucbinclude -I. -ansi
LIBDIRS=-L/home/staff/pets/quintus/bin3.2/sun4-5
#LIBS= -L/usr/ucblib -lucb
@@ -55,7 +60,11 @@
#CHOSENOPTIM=$(DEBUG)
#OPTS=$(DEF)COMPUTED_TABLE $(DEF)EQUAL_TEST
-OPTS=$(DEF)CLEAR_CACHES $(DEF)COMPUTED_TABLE $(DEF)EQUAL_TEST
+OPTS= \
+ $(DEF)CLEAR_CACHES \
+ $(DEF)COMPUTED_TABLE \
+ $(DEF)EQUAL_TEST \
+ $(DEF)USE_ITE_CONSTANT
#OPTS=$(DEF)CLEAR_CACHES $(DEF)COMPUTED_TABLE $(DEF)EQUAL_TEST $(DEF)STATISTICS
#WHICH=NAIVE
#WHICH=OLD
Index: robdd/Mmakefile
===================================================================
RCS file: robdd/Mmakefile
diff -N robdd/Mmakefile
--- /dev/null 1 Jan 1970 00:00:00 -0000
+++ robdd/Mmakefile 19 May 2003 06:04:25 -0000
@@ -0,0 +1,28 @@
+#-----------------------------------------------------------------------------#
+# Copyright (C) 2003 University of Melbourne.
+# This file may only be copied under the terms of the GNU General
+# Public Licence - see the file COPYING in the Mercury distribution.
+#-----------------------------------------------------------------------------#
+
+# Mmakefile for Peter Schachte's ROBDD package.
+
+MAIN_TARGET=robdd
+
+MERCURY_DIR=..
+include $(MERCURY_DIR)/Mmake.common
+
+
+MGNUC = $(SCRIPTS_DIR)/mgnuc
+
+EXTRA_CFLAGS = -I$(BROWSER_DIR) -I$(LIBRARY_DIR) -I$(RUNTIME_DIR) \
+ -I$(BOEHM_GC_DIR) -I$(BOEHM_GC_DIR)/include
+
+CFILES = bryant.c
+
+OBJS = $(CFILES:.c=.$O)
+PIC_OBJS = $(CFILES:.c=.$(EXT_FOR_PIC_OBJECTS))
+
+.PHONY: robdd
+robdd: $(OBJS) $(PIC_OBJS)
+
+include Makefile
--------------------------------------------------------------------------
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