[m-dev.] for review: add ROBDD interface to Mercury

David Overton dmo at cs.mu.OZ.AU
Fri Jul 7 11:53:50 AEST 2000


Hi,

Peter Schachte, would you please have a look at this.

Also Tyson or Fergus, when you get a chance, I would appreciate your
comments, particularly on the GC stuff in `robdd/bryant.c' and the
configuration management issues.

At the moment I have included `robdd.m' as part of the standard
library.  I'm not sure if this is appropriate, but I wanted to use it
in the compiler so this seemed like a convenient place to put it.  Is
this okay or should I move somewhere else, e.g. `extras/'?

Estimated hours taken: 10

Add an interface to Peter Schachte's ROBDD package to the Mercury library.

Mmake.common.in:
Mmakefile:
	Add the `robdd' directory and top-level target.

robdd/Mmakefile:
	Add a Mmakefile for the `robdd' directory which sets up some variables
	and a `robdd' target and then includes Peter's Makefile.

robdd/bryant.c:
robdd/bryant.h:
	Enable garbage collection of ROBDDs under the conservative GC by
	implementing weak pointers for links between nodes in the
	`unique_table'.  Register a finaliser with the GC system to remove
	collected nodes from the `unique_table'.
	Export the `ite' and `restrict' functions.
	Add prototypes for some functions to avoid compiler warnings.

library/library.m:
library/robdd.m:
	Add a new module to interface to the ROBDD code in `robdd/bryant.c'.

library/Mmakefile:
	Link `robdd/bryant.o' into the library.

compiler/modules.m:
	Tell the compiler about the new library module.

Index: Mmake.common.in
===================================================================
RCS file: /home/mercury1/repository/mercury/Mmake.common.in,v
retrieving revision 1.45
diff -u -r1.45 Mmake.common.in
--- Mmake.common.in	2000/06/08 13:06:36	1.45
+++ Mmake.common.in	2000/06/27 01:42:15
@@ -117,6 +117,7 @@
 BOEHM_GC_DIR = $(MERCURY_DIR)/boehm_gc
 COMPILER_DIR = $(MERCURY_DIR)/compiler
 UTIL_DIR = $(MERCURY_DIR)/util
+ROBDD_DIR = $(MERCURY_DIR)/robdd
 
 # By default, GRADESTRING is defined as the result of invoking
 # `mmc --output-grade-string' with $(GRADE) and $(GRADEFLAGS).
Index: Mmakefile
===================================================================
RCS file: /home/mercury1/repository/mercury/Mmakefile,v
retrieving revision 1.56
diff -u -r1.56 Mmakefile
--- Mmakefile	2000/06/22 08:50:19	1.56
+++ Mmakefile	2000/07/05 06:28:27
@@ -18,6 +18,7 @@
 		util \
 		boehm_gc \
 		runtime \
+		robdd \
 		library \
 		trace \
 		browser \
@@ -118,8 +119,12 @@
 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
+library: dep_library scripts util boehm_gc runtime robdd
 	cd library && $(SUBDIR_MMAKE)
 
 .PHONY: browser
Index: robdd/Mmakefile
===================================================================
RCS file: Mmakefile
diff -N Mmakefile
--- /dev/null	Fri Jul  7 11:09:32 2000
+++ Mmakefile	Thu Jul  6 12:20:51 2000
@@ -0,0 +1,31 @@
+#-----------------------------------------------------------------------------#
+# Copyright (C) 2000 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
+
+M_ENV		= MERCURY_ALL_C_INCL_DIRS="\
+			-I$(BROWSER_DIR) \
+			-I$(LIBRARY_DIR) \
+			-I$(RUNTIME_DIR) \
+			-I$(BOEHM_GC_DIR) \
+			-I$(BOEHM_GC_DIR)/include \
+		  "
+MGNUC		= $(M_ENV) $(SCRIPTS_DIR)/mgnuc
+
+CFILES	= bryant.c
+
+OBJS		= $(CFILES:.c=.$O)
+PIC_OBJS	= $(CFILES:.c=.$(EXT_FOR_PIC_OBJECTS))
+
+.PHONY: robdd
+robdd: $(OBJS) $(PIC_OBJS)
+
+include Makefile
Index: robdd/bryant.c
===================================================================
RCS file: /home/mercury1/repository/mercury/robdd/bryant.c,v
retrieving revision 1.1.1.1
diff -u -r1.1.1.1 bryant.c
--- robdd/bryant.c	2000/03/10 05:17:21	1.1.1.1
+++ robdd/bryant.c	2000/07/07 00:56:41
@@ -91,6 +91,12 @@
 
 *****************************************************************/
 
+#ifdef CONSERVATIVE_GC
+	/* We need to include mercury_imp.h to get the definition of `Word'. */
+#	include <mercury_imp.h>
+#	define BRYANT_CONSERVATIVE_GC
+#endif
+
 #include <stdio.h>
 #include <stdlib.h>
 #include <math.h>
@@ -99,6 +105,29 @@
 #include "bryant.h"
 
 
+#ifdef BRYANT_CONSERVATIVE_GC
+#include <gc.h>
+
+/* Don't use pools of nodes with the conservative GC. */
+#undef POOL
+
+/* Define a macro to disguise pointers that we want to hide from the
+ * collector.
+ */
+#define MUNGE_(p) (~(p))
+#define MUNGE(p) ((node *) MUNGE_((Word) p))
+
+/* Redefine malloc() and free() to use the GC versions */
+#define malloc(n) GC_malloc(n)
+#define free(p) GC_free(p)
+
+#else /* !BRYANT_CONSERVATIVE_GC */
+#define MUNGE_(p) (p)
+#define MUNGE(p) (MUNGE_(p))
+#define POOL
+#endif /* BRYANT_CONSERVATIVE_GC */
+
+
 #define UNUSED_MAPPING -1	/* this MUST BE -1 */
 
 #if !defined(max)
@@ -110,10 +139,12 @@
 
 #define PERCENTAGE(x,y) ((100.0 * (float)(x)) / (float)(y))
 
+#ifdef POOL
 typedef struct pool {
     node data[POOL_SIZE];
     struct pool *prev;
 } pool;
+#endif POOL
 
 
 #if defined(NO_CHEAP_SHIFT) && BITS_PER_WORD == 32
@@ -276,17 +307,22 @@
 #endif
 
 #if defined(CLEAR_CACHES)
+#if defined(POOL)
 #define INIT_UNIQUE_TABLE				\
     do {						\
-	memset(unique_table, 0, sizeof(unique_table));	\
+	memset(unique_table, MUNGE(0), sizeof(unique_table));	\
 	while (curr_pool!=NULL) {			\
 	    pool *p = curr_pool->prev;			\
 	    free(curr_pool);				\
 	    curr_pool = p;				\
 	}						\
 	curr_pool_ptr = curr_pool_end_ptr = NULL;	\
-	pool_count = 0;					\
+	node_count = 0;					\
     } while (0)
+#else /* !POOL */
+#define INIT_UNIQUE_TABLE				\
+    memset(unique_table, MUNGE_(0), sizeof(unique_table));
+#endif /* POOL */
 #else /* !CLEAR_CACHES */
 #define INIT_UNIQUE_TABLE
 #endif /* CLEAR_CACHES */
@@ -920,6 +956,7 @@
 
 
 /* returns 1 if set1 is identical to set2 */
+__inline int bitset_equal(bitset *set1, bitset *set2);
 __inline int bitset_equal(bitset *set1, bitset *set2)
     {
 	bitmask *ptr1 = &set1->bits[0];
@@ -935,6 +972,7 @@
     }
 
 /* returns 1 if 2 sets are disjoint, else 0 */
+__inline int bitset_disjoint(bitset *set1, bitset *set2);
 __inline int bitset_disjoint(bitset *set1, bitset *set2)
     {
 	bitmask *ptr1 = &set1->bits[0];
@@ -950,6 +988,7 @@
 
 
 /* returns 1 if set1 is a subset of set2 */
+__inline int bitset_subset(bitset *set1, bitset *set2);
 __inline int bitset_subset(bitset *set1, bitset *set2)
     {
 	bitmask *ptr1 = &set1->bits[0];
@@ -966,6 +1005,7 @@
 
 
 /* returns 1 if set1 is a subset of set2 */
+__inline int bitset_empty(bitset *set);
 __inline int bitset_empty(bitset *set)
     {
 	bitmask *ptr = &set->bits[0];
@@ -985,26 +1025,54 @@
 
  ****************************************************************/
 
+#if defined(BRYANT_CONSERVATIVE_GC)
+void remove_node(GC_PTR obj, GC_PTR client_data);
+void remove_node(GC_PTR obj, GC_PTR client_data)
+    {
+    	node *n = (node *) obj;
+    	node **bucket = (node **) client_data;
+
+    	if (MUNGE(n->unique) != NULL)
+	    MUNGE(n->unique)->uprev = n->uprev;
+
+	if (MUNGE(n->uprev) != NULL)
+	    MUNGE(n->uprev)->unique = n->unique;
+
+	if (MUNGE(*bucket) == n)
+	    *bucket = n->unique;
+    }
+#endif /* BRYANT_CONSERVATIVE_GC */
+
+
+#if defined(POOL)
 static pool *curr_pool = NULL;
 static node *curr_pool_ptr = NULL;
 static node *curr_pool_end_ptr = NULL;
-static int pool_count = 0;
+#endif /* POOL */
+static int node_count = 0;
 
-static node *alloc_node(int value, node* tr, node* fa)
+static node *alloc_node(int value, node* tr, node* fa, node** bucket)
     {
-	pool *newpool;
 	node *n;
+#if defined(POOL)
+	pool *newpool;
 
 	if (curr_pool_ptr >= curr_pool_end_ptr) {
 	    /* allocate a new pool */
-            newpool = malloc(sizeof(pool));
+            newpool = (pool *) malloc(sizeof(pool));
             newpool->prev = curr_pool;
             curr_pool = newpool;
             curr_pool_ptr = &(newpool->data[0]);
             curr_pool_end_ptr = &(newpool->data[POOL_SIZE]);
-            ++pool_count;
         }
 	n = curr_pool_ptr++;
+#else /* !POOL */
+	n = (node *) malloc(sizeof(node));
+#if defined(BRYANT_CONSERVATIVE_GC)
+	GC_register_finalizer(n, remove_node, bucket, 0, 0);
+#endif
+#endif /* POOL */
+        node_count++;
         n->value = value;
         n->tr = tr;
         n->fa = fa;
@@ -1014,7 +1082,7 @@
 /* return the number of graph nodes that have been created. */
 int nodes_in_use(void)
     {
-        return pool_count*POOL_SIZE - (curr_pool_end_ptr - curr_pool_ptr);
+        return node_count;
     }
 
 
@@ -1035,9 +1103,12 @@
 	if (tr == fa) return tr;
 
 	bucket = &unique_table[UNIQUE_HASH(var,tr,fa)];
-	ptr = *bucket;
-	while (ptr!=NULL && (var!=ptr->value || tr!=ptr->tr || fa!=ptr->fa))
-	    ptr = ptr->unique;
+	if (*bucket == NULL)
+		*bucket = MUNGE(NULL);
+	ptr = MUNGE(*bucket);
+	while (ptr!=NULL && (var!=ptr->value || tr!=ptr->tr || fa!=ptr->fa)) {
+	    ptr = MUNGE(ptr->unique);
+	}
 
 	if (ptr!=NULL) {
 	    COUNT_UNIQUE_HIT;
@@ -1046,9 +1117,12 @@
 
 	/* node doesn't exist so create it and put in bucket */
 	COUNT_UNIQUE_MISS;
-	ptr = alloc_node(var, tr, fa);
+	ptr = alloc_node(var, tr, fa, bucket);
 	ptr->unique = *bucket;
-	*bucket = ptr;
+	*bucket = MUNGE(ptr);
+	ptr->uprev = MUNGE(NULL);
+	if (MUNGE(ptr->unique) != NULL)
+	    MUNGE(ptr->unique)->uprev = MUNGE(ptr);
 	return ptr;
     }
 
@@ -1066,6 +1140,7 @@
 
  ****************************************************************/
 
+int max_variable(void);
 int max_variable(void)
     {
 	return MAXVAR;
@@ -2957,9 +3032,9 @@
 			  unique_table_hits+unique_table_misses));
 	memset(size_count, 0, sizeof(size_count));
 	for (i=0; i<UNIQUE_TABLE_SIZE; ++i) {
-	    for (ptr=unique_table[i],count=0;
+	    for (ptr=MUNGE(unique_table[i]),count=0;
 		 ptr!=NULL;
-		 ptr=ptr->unique,++count);
+		 ptr=MUNGE(ptr->unique),++count);
 	    ++size_count[(count<=MAX_COUNT ? count : MAX_COUNT+1)];
 	}
 	print_distribution(size_count, MAX_COUNT);
Index: robdd/bryant.h
===================================================================
RCS file: /home/mercury1/repository/mercury/robdd/bryant.h,v
retrieving revision 1.1.1.1
diff -u -r1.1.1.1 bryant.h
--- robdd/bryant.h	2000/03/10 05:17:21	1.1.1.1
+++ robdd/bryant.h	2000/07/06 01:32:28
@@ -1,6 +1,6 @@
 /*****************************************************************
   File     : bryant.h
-  RCS      : $Id: bryant.h,v 1.1.1.1 2000/03/10 05:17:21 dmo Exp $
+  RCS      : $Id: bryant.h,v 1.1.1.1 2000/03/10 05:11:05 dmo Exp $
   Author   : Peter Schachte
   Origin   : Sun Jul 30 15:08:53 1995
   Purpose  : header file for users of bryant.c ROBDD package
@@ -8,6 +8,9 @@
 
 *****************************************************************/
 
+#ifndef BRYANT_H
+#define BRYANT_H
+
 #if defined(QUINTUS)
 #include <quintus/quintus.h>
 #endif
@@ -64,6 +67,7 @@
 	struct graphnode *tr;	/* true (then) child */
 	struct graphnode *fa;	/* false (else) child */
 	struct graphnode *unique;  /* pointer to next elt in unique table */
+	struct graphnode *uprev;   /* pointer to the prev elt in unique table */
 } node, type;
 
 /* zero and one are terminal nodes (sinks). */
@@ -260,6 +264,10 @@
 /* returns var, as an ROBDD.  */
 extern node *variableRep(int var);
 
+/* if then else algorithm */
+extern node *ite(node *f, node *g, node *h);
+
+extern node *ite_var(int f, node *g, node *h);
 
 /* returns a \wedge b */
 extern node *glb(node *a, node *b);
@@ -269,7 +277,7 @@
 extern node *implies(node *a, node *b);
 
 /* returns \exists c . a */
-/* extern node *restrict(int c, node *a); */
+extern node *restrict(int c, node *f);
 
 /* returns \bigglb_{0 \leq i \leq n} array[i] */
 extern node *glb_array(int n, int arr[]);
@@ -403,3 +411,5 @@
 extern node *renameTerm(node *in, QP_term_ref term);
 extern node *reverseRenameTerm(node *in, QP_term_ref term);
 #endif /* QUINTUS */
+
+#endif /* BRYANT_H */
Index: compiler/modules.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/modules.m,v
retrieving revision 1.130
diff -u -r1.130 modules.m
--- compiler/modules.m	2000/06/22 08:50:20	1.130
+++ compiler/modules.m	2000/06/27 01:42:38
@@ -541,6 +541,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("set").
 mercury_std_library_module("set_bbbtree").
 mercury_std_library_module("set_ordlist").
Index: library/Mmakefile
===================================================================
RCS file: /home/mercury1/repository/mercury/library/Mmakefile,v
retrieving revision 1.52
diff -u -r1.52 Mmakefile
--- library/Mmakefile	2000/06/22 08:50:23	1.52
+++ library/Mmakefile	2000/07/07 01:09:37
@@ -58,6 +58,7 @@
 			-I$(RUNTIME_DIR) \
 			-I$(BOEHM_GC_DIR) \
 			-I$(BOEHM_GC_DIR)/include \
+			-I$(ROBDD_DIR) \
 		"
 MCD	=	$(M_ENV) $(MC) --generate-dependencies $(INTERMODULE_OPTS)
 MCI	=	$(M_ENV) $(MC) --make-interface $(INTERMODULE_OPTS) \
@@ -84,6 +85,9 @@
 		    *.gc*)	 echo "-lgc" ;;				\
 		  esac							\
 		`
+ROBDD_OBJS  =	$(ROBDD_DIR)/bryant.$O
+ROBDD_PIC_OBJS = $(ROBDD_DIR)/bryant.$(EXT_FOR_PIC_OBJECTS)
+
 ALL_LDLIBS =	$(LDLIBS) $(EXTRA_LDLIBS)
 
 MTAGS	=	$(SCRIPTS_DIR)/mtags
@@ -193,18 +197,19 @@
 lib_std: lib$(STD_LIB_NAME).$A lib$(STD_LIB_NAME).$(EXT_FOR_SHARED_LIB)
 lib_std: $(STD_LIB_NAME).init
 
-lib$(STD_LIB_NAME)$(DLL_DEF_LIB).$A : $(library.os)
+lib$(STD_LIB_NAME)$(DLL_DEF_LIB).$A : $(library.os) $(ROBDD_OBJS)
 	rm -f lib$(STD_LIB_NAME)$(DLL_DEF_LIB).$A
 	$(AR) $(ALL_ARFLAGS) \
 		$(AR_LIBFILE_OPT)lib$(STD_LIB_NAME)$(DLL_DEF_LIB).$A \
-		$(library.os)
+		$(library.os) $(ROBDD_OBJS)
 	$(RANLIB) lib$(STD_LIB_NAME)$(DLL_DEF_LIB).$A
 
 RPATH_1=$(SHLIB_RPATH_OPT)$(FINAL_INSTALL_MERC_LIB_DIR)
 RPATH_2=$(SHLIB_RPATH_SEP)$(FINAL_INSTALL_MERC_GC_LIB_DIR)
 
-lib$(STD_LIB_NAME).so : $(library.pic_os)
+lib$(STD_LIB_NAME).so : $(library.pic_os) $(ROBDD_PIC_OBJS)
 	$(LINK_SHARED_OBJ) -o lib$(STD_LIB_NAME).so $(library.pic_os)	\
+		$(ROBDD_PIC_OBJS)					\
 		$(RPATH_1)$(RPATH_2)					\
 		$(ALL_LDFLAGS) $(ALL_LDLIBS)				\
 		$(SHARED_LIBS)
Index: library/library.m
===================================================================
RCS file: /home/mercury1/repository/mercury/library/library.m,v
retrieving revision 1.49
diff -u -r1.49 library.m
--- library/library.m	2000/05/15 03:33:06	1.49
+++ library/library.m	2000/07/05 06:28:37
@@ -37,6 +37,7 @@
 :- import_module integer, rational.
 :- import_module exception, gc.
 :- import_module time.
+:- import_module robdd.
 :- import_module pprint.
 
 % library__version must be implemented using pragma c_code,
Index: library/robdd.m
===================================================================
RCS file: robdd.m
diff -N robdd.m
--- /dev/null	Fri Jul  7 11:09:32 2000
+++ robdd.m	Thu Jul  6 17:59:19 2000
@@ -0,0 +1,643 @@
+%---------------------------------------------------------------------------%
+% Copyright (C) 2000 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 functions.
+
+%-----------------------------------------------------------------------------%
+%-----------------------------------------------------------------------------%
+
+:- module robdd.
+
+:- interface.
+
+:- import_module term, io, set.
+
+:- type robdd(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(set(var(T))) = robdd(T).
+
+	% disj_vars([V1, V2, ..., Vn]) = var(V1) + var(V2) + ... + var(Vn).
+:- func disj_vars(set(var(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(set(var(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).
+
+%-----------------------------------------------------------------------------%
+
+	% Succeed iff the var is entailed by the ROBDD.
+:- pred var_entailed(robdd(T)::in, var(T)::in) is semidet.
+
+	% 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.
+
+	% Print out the ROBDD in disjunctive 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.
+
+	% 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, set(var(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).
+:- pred labelling(set(var(T))::in, robdd(T)::in, set(var(T))::out,
+		set(var(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).
+:- pred minimal_model(set(var(T))::in, robdd(T)::in, set(var(T))::out,
+		set(var(T))::out) is nondet.
+
+%-----------------------------------------------------------------------------%
+%-----------------------------------------------------------------------------%
+
+:- implementation.
+
+:- import_module set_unordlist, list, string, map, bool, set_bbbtree, int.
+:- import_module multi_map, require.
+
+:- type robdd(T) ---> robdd(c_pointer).
+
+:- pragma c_header_code("#include <bryant.h>\n").
+
+:- pragma c_code(one = (F::out), [will_not_call_mercury],
+		"F = (Word) trueVar();").
+
+:- pragma c_code(zero = (F::out), [will_not_call_mercury],
+		"F = (Word) falseVar();").
+
+:- pragma c_code(var(V::in) = (F::out), [will_not_call_mercury],
+		"F = (Word) variableRep(V);").
+
+:- pragma c_code(ite(F::in, G::in, H::in) = (ITE::out), [will_not_call_mercury],
+		"ITE = (Word) ite((node *) F, (node *) G, (node *) H);").
+
+:- pragma c_code(ite_var(V::in, G::in, H::in) = (ITE::out), 
+		[will_not_call_mercury],
+		"ITE = (Word) ite_var(V, (node *) G, (node *) H);").
+
+:- pragma c_code((X::in) * (Y::in) = (F::out), [will_not_call_mercury],
+		"F = (Word) glb((node *) X, (node *) Y);").
+
+:- pragma c_code((X::in) + (Y::in) = (F::out), [will_not_call_mercury],
+		"F = (Word) lub((node *) X, (node *) Y);").
+
+:- pragma c_code(((X::in) =< (Y::in)) = (F::out), [will_not_call_mercury],
+		"F = (Word) implies((node *) X, (node *) Y);").
+
+(F =:= G) = ite(F, G, ~G).
+
+(F =\= G) = ite(F, ~G, G).
+
+(~F) = ite(F, zero, one).
+
+:- pragma c_code(var_entailed(F::in, V::in), [will_not_call_mercury],
+		"SUCCESS_INDICATOR = var_entailed((node *) F, (int) V);").
+
+% Access to the struct members.
+% WARNING!  The 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 c_code(value(F::in) = (Value::out), [will_not_call_mercury],
+		"Value = (Word) ((node *) F)->value;").
+:- pragma c_code(tr(F::in) = (Tr::out), [will_not_call_mercury],
+		"Tr = (Word) ((node *) F)->tr;").
+:- pragma c_code(fa(F::in) = (Fa::out), [will_not_call_mercury],
+		"Fa = (Word) ((node *) F)->fa;").
+
+/*
+:- pragma c_code(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")
+	;
+		{ set_unordlist__init(Trues) },
+		{ set_unordlist__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 c_code(restrict(V::in, F::in) = (R::out), [will_not_call_mercury],
+		"R = (Word) restrict(V, (node *) F);").
+
+:- pragma c_code(restrict_threshold(V::in, F::in) = (R::out),
+		[will_not_call_mercury],
+		"R = (Word) restrictThresh(V, (node *) F);").
+
+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 c_code(make_node(Var::in, Then::in, Else::in) = (Node::out),
+		[will_not_call_mercury],
+	"Node = (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) = list__foldr(func(V, R) = make_node(V, R, zero),
+		set__to_sorted_list(Vars), one).
+
+disj_vars(Vars) = list__foldr(func(V, R) = make_node(V, one, R),
+		set__to_sorted_list(Vars), zero).
+
+at_most_one_of(Vars) = at_most_one_of_2(Vars, one, one).
+
+:- func at_most_one_of_2(set(var(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(set__to_sorted_list(Vars)), 
+		OneOf0, R, NoneOf0, _).
+
+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
+		)
+	).
+
+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_filter(P, F0) = F :- filter_2(P, F0, F, map__init, _, map__init, _).
+
+:- pred filter_2(pred(var(T)), robdd(T), robdd(T),
+		map(var(T), bool), map(var(T), bool), map(robdd(T), robdd(T)),
+		map(robdd(T), robdd(T))).
+:- mode filter_2(pred(in) is semidet, in, out, in, out, in, out) is det.
+
+filter_2(P, F0, F, SeenVars0, SeenVars, SeenNodes0, SeenNodes) :-
+	( is_terminal(F0) ->
+		F = F0,
+		SeenVars = SeenVars0,
+		SeenNodes = SeenNodes0
+	; map__search(SeenNodes0, F0, F1) ->
+		F = F1,
+		SeenVars = SeenVars0,
+		SeenNodes = SeenNodes0
+	;
+		filter_2(P, F0^tr, Ftrue, SeenVars0, SeenVars1, SeenNodes0,
+			SeenNodes1),
+		filter_2(P, 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)
+	).
+
+:- pragma c_code(is_terminal(F::in), [will_not_call_mercury, thread_safe],
+	"SUCCESS_INDICATOR = IS_TERMINAL(F);").
+
+
+size(F, Nodes, Depth) :-
+	size_2(F, 0, Nodes, 0, Depth, set_bbbtree__init, _).
+
+:- pred size_2(robdd(T)::in, int::in, int::out, int::in, int::out,
+		set_bbbtree(robdd(T))::in, set_bbbtree(robdd(T))::out) is det.
+
+size_2(F, Nodes0, Nodes, Depth0, Depth, Seen0, Seen) :-
+	( is_terminal(F) ->
+		Nodes = Nodes0, Depth = Depth0, Seen = Seen0
+	; F `member` Seen0 ->
+		Nodes = Nodes0, Depth = Depth0, Seen = Seen0
+	;
+		size_2(F^tr, Nodes0+1, Nodes1, Depth0, Depth1, Seen0, Seen1),
+		size_2(F^fa, Nodes1, Nodes, Depth0, Depth2, 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, set__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];
+"),
+	{ 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").
+
+:- 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 c_code(node_num(R::in) = (N::out), [will_not_call_mercury],
+	"N = (Integer)R;\n").
+
+:- 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 ;\n",
+			[s(node_name(R0)), s(Arc = yes -> "f0" ; "f2"),
+			s(node_name(R1))])
+	).
+
+labelling(Vars, R, TrueVars, FalseVars) :-
+	labelling_2(set__to_sorted_list(Vars), R, set__init, TrueVars,
+		set__init, FalseVars).
+
+:- pred labelling_2(list(var(T))::in, robdd(T)::in, set(var(T))::in,
+		set(var(T))::out, set(var(T))::in, set(var(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) :-
+	( set__empty(Vars) ->
+		TrueVars = set__init,
+		FalseVars = set__init
+	;
+		minimal_model_2(set__to_sorted_list(Vars), R, set__init,
+			TrueVars0, set__init, 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, set(var(T))::in,
+		set(var(T))::out, set(var(T))::in, set(var(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)
+	).
-- 
David Overton      Department of Computer Science & Software Engineering
PhD Student        The University of Melbourne, Victoria 3010, Australia
+61 3 8344 9159    http://www.cs.mu.oz.au/~dmo
--------------------------------------------------------------------------
mercury-developers mailing list
Post messages to:       mercury-developers at cs.mu.oz.au
Administrative Queries: owner-mercury-developers at cs.mu.oz.au
Subscriptions:          mercury-developers-request at cs.mu.oz.au
--------------------------------------------------------------------------



More information about the developers mailing list