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

[David Overton]

On Fri, Jul 07, 2000 at 02:52:52PM +1000, Peter Schachte wrote:
> On Fri, Jul 07, 2000 at 11:53:50AM +1000, David Overton wrote:
> > +/* 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))
> 
> I think it would be worth mentioning why you want to hide robdd nodes from
> GC.

Done.

> 
> Also, bitwise negation is a cute way to munge things, but may not be a
> appropriate on some architectures.  Anyway, using the same macro for munging
> and unmunging is a bit confusing.  I think you should have separate macros
> for each, and use them appropriately.  To test that you've done it right,
> you might try munging by adding 1.

Done.

> 
> 
> > @@ -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);
> > +	}
> 
> A comment explaining the need for the if (*bucket == NULL) statement would
> be good.  I assume this is to avoid the need to initialize the unique table
> to MUNGE(NULL), which raises the initialization problem discussed earlier.
> Added distributed fat deserves an explanation, I think.

Done.

> 
> > ===================================================================
> > 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
> 
> >  #if defined(QUINTUS)
> >  #include <quintus/quintus.h>
> >  #endif
> 
> Feel free to cut out this and any other QUINTUS stuff.

I haven't removed this since it's not doing any harm.  I've tried to
make as little change as possible to these files to make it easier to
import any new versions you produce.

> 
> 
> > @@ -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 */
> 
> Shouldn't that be IFDEF'd on POOL?  There are going to be bazillions of
> these things, so size matters (and small is beautiful).

It should be ifdefd on CONSERVATIVE_GC.  I've done that.

> 
> > ===================================================================
> > 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.
> 
> You might want to say "Boolean constraints" instead, as I think more people
> would understand that.

Done.

> 
> Also, if this is to be added to the library, I think a couple of paragraphs
> explaining what it is about and how to use it, ideally with a simple example
> or two, is important.

Done.

> 
> 
> > +%-----------------------------------------------------------------------------%
> > +%-----------------------------------------------------------------------------%
> > +
> > +:- module robdd.
> > +
> > +:- interface.
> > +
> > +:- import_module term, io, set.
> > +
> > +:- type robdd(T).
> 
> I understand why you might not want to use type classes yet, but you should
> at least document that T here has to support inequality testing.  Perhaps it
> would be better for now to just create a variable type (or use the one you
> have already), and not make robdd parametric at all.

It uses the `var(T)' type from `library/term.m'.  This is represented as
just an integer, the type T is not used at all, so it can be anything.
It is just there to add extra type safety when using different kinds
of vars that you don't want to get mixed up.

I.e.
	:- type var(T) ---> var(int).
	:- type robdd(T) ---> robdd(c_pointer).

> 
> Also, to make this a more generally useful library package, I think you
> should add a predicate to check whether one robdd entails another (without
> building any new structure).  The ite_constant() function can do this.

Done (see `entails/2' in the relative diff).

> 
> 
> > +:- 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);").
> > +
> 
> Long line.
> 

Fixed.

> 
> Otherwise this looks good to me.
> 

Here's a relative diff.  A couple of other things need to be sorted
out before I commit this:
	- should it go in the standard library or somewhere else?
	- need to sort out licensing issues for bryant.[ch] with
	  Peter.

--- log	Tue Jul 11 16:59:58 2000
+++ ../log	Tue Jul 11 17:05:51 2000
@@ -1,6 +1,6 @@
 
 
-Estimated hours taken: 10
+Estimated hours taken: 12
 
 Add an interface to Peter Schachte's ROBDD package to the Mercury library.
 
@@ -12,6 +12,9 @@
 	Add a Mmakefile for the `robdd' directory which sets up some variables
 	and a `robdd' target and then includes Peter's Makefile.
 
+robdd/Makefile:
+	Pass -DUSE_ITE_CONSTANT when compiling bryant.c.
+
 robdd/bryant.c:
 robdd/bryant.h:
 	Enable garbage collection of ROBDDs under the Conservative GC by
@@ -18,7 +21,7 @@
 	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.
+	Export the `ite', `ite_constant' and `restrict' functions.
 	Add prototypes for some functions to avoid compiler warnings.
 
 library/library.m:
--- Makefile	Tue Jul 11 17:03:18 2000
+++ ../mercury/robdd/Makefile	Mon Jul 10 11:58:44 2000
@@ -55,7 +55,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
 library/library.m:
--- bryant.c	Fri Jul  7 16:33:16 2000
+++ ../mercury/robdd/bryant.c	Mon Jul 10 12:05:05 2000
@@ -112,10 +112,14 @@
 #undef POOL
 
 /* Define a macro to disguise pointers that we want to hide from the
- * collector.
+ * GC.  We MUNGE pointers to ROBDD nodes from the `unique_table' so that
+ * the nodes will be GCed when no longer in use, even though they are
+ * still in the table.  This also requires registering a finaliser
+ * (`remove_node()') with the GC to remove the node from the table.
  */
 #define MUNGE_(p) (~(p))
 #define MUNGE(p) ((node *) MUNGE_((Word) p))
+#define UNMUNGE(p) (MUNGE(p))
 
 /* Redefine malloc() and free() to use the GC versions */
 #define malloc(n) GC_malloc(n)
@@ -124,6 +128,7 @@
 #else /* !BRYANT_CONSERVATIVE_GC */
 #define MUNGE_(p) (p)
 #define MUNGE(p) (MUNGE_(p))
+#define UNMUNGE(p) (MUNGE(p))
 #define POOL
 #endif /* BRYANT_CONSERVATIVE_GC */
 
@@ -1032,13 +1037,13 @@
     	node *n = (node *) obj;
     	node **bucket = (node **) client_data;
 
-    	if (MUNGE(n->unique) != NULL)
-	    MUNGE(n->unique)->uprev = n->uprev;
+    	if (UNMUNGE(n->unique) != NULL)
+	    UNMUNGE(n->unique)->uprev = n->uprev;
 
-	if (MUNGE(n->uprev) != NULL)
-	    MUNGE(n->uprev)->unique = n->unique;
+	if (UNMUNGE(n->uprev) != NULL)
+	    UNMUNGE(n->uprev)->unique = n->unique;
 
-	if (MUNGE(*bucket) == n)
+	if (UNMUNGE(*bucket) == n)
 	    *bucket = n->unique;
     }
 #endif /* BRYANT_CONSERVATIVE_GC */
@@ -1103,11 +1108,16 @@
 	if (tr == fa) return tr;
 
 	bucket = &unique_table[UNIQUE_HASH(var,tr,fa)];
+
+	/* The following check avoids the need to initialise the unique_table
+	 * elements to MUNGE(NULL).
+	 */
 	if (*bucket == NULL)
 		*bucket = MUNGE(NULL);
-	ptr = MUNGE(*bucket);
+
+	ptr = UNMUNGE(*bucket);
 	while (ptr!=NULL && (var!=ptr->value || tr!=ptr->tr || fa!=ptr->fa)) {
-	    ptr = MUNGE(ptr->unique);
+	    ptr = UNMUNGE(ptr->unique);
 	}
 
 	if (ptr!=NULL) {
@@ -1120,9 +1130,11 @@
 	ptr = alloc_node(var, tr, fa, bucket);
 	ptr->unique = *bucket;
 	*bucket = MUNGE(ptr);
+#ifdef BRYANT_CONSERVATIVE_GC
 	ptr->uprev = MUNGE(NULL);
-	if (MUNGE(ptr->unique) != NULL)
-	    MUNGE(ptr->unique)->uprev = MUNGE(ptr);
+	if (UNMUNGE(ptr->unique) != NULL)
+	    UNMUNGE(ptr->unique)->uprev = MUNGE(ptr);
+#endif
 	return ptr;
     }
 
@@ -3032,9 +3044,9 @@
 			  unique_table_hits+unique_table_misses));
 	memset(size_count, 0, sizeof(size_count));
 	for (i=0; i<UNIQUE_TABLE_SIZE; ++i) {
-	    for (ptr=MUNGE(unique_table[i]),count=0;
+	    for (ptr=UNMUNGE(unique_table[i]),count=0;
 		 ptr!=NULL;
-		 ptr=MUNGE(ptr->unique),++count);
+		 ptr=UNMUNGE(ptr->unique),++count);
 	    ++size_count[(count<=MAX_COUNT ? count : MAX_COUNT+1)];
 	}
 	print_distribution(size_count, MAX_COUNT);
--- bryant.h	Fri Jul  7 16:33:16 2000
+++ ../mercury/robdd/bryant.h	Mon Jul 10 12:05:05 2000
@@ -67,7 +67,9 @@
 	struct graphnode *tr;	/* true (then) child */
 	struct graphnode *fa;	/* false (else) child */
 	struct graphnode *unique;  /* pointer to next elt in unique table */
+#if defined(CONSERVATIVE_GC)
 	struct graphnode *uprev;   /* pointer to the prev elt in unique table */
+#endif
 } node, type;
 
 /* zero and one are terminal nodes (sinks). */
@@ -267,6 +269,15 @@
 /* if then else algorithm */
 extern node *ite(node *f, node *g, node *h);
 
+/* This is sort of an "approximate ite()."  It returns zero or one if
+ * that's what ite() would do.  Otherwise it just returns the
+ * pseudo-node `nonterminal' or some real node.  In any case, it does
+ * not create any new nodes.
+ */
+#ifdef USE_ITE_CONSTANT
+extern node *ite_constant(node *f,node *g,node *h);
+#endif
+
 extern node *ite_var(int f, node *g, node *h);
 
 /* returns a \wedge b */
--- robdd.m	Fri Jul  7 16:33:41 2000
+++ ../mercury/library/robdd.m	Tue Jul 11 16:14:16 2000
@@ -8,9 +8,38 @@
 % 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.
+% 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.
 
 %-----------------------------------------------------------------------------%
 %-----------------------------------------------------------------------------%
@@ -22,6 +51,7 @@
 :- import_module term, io, set.
 
 :- type robdd(T).
+:- type robdd == robdd(generic).
 
 % Constants.
 :- func one = robdd(T).
@@ -92,6 +122,12 @@
 
 %-----------------------------------------------------------------------------%
 
+	% 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.
 
@@ -170,7 +206,10 @@
 
 :- type robdd(T) ---> robdd(c_pointer).
 
-:- pragma c_header_code("#include <bryant.h>\n").
+:- pragma c_header_code("
+#define USE_ITE_CONSTANT
+#include <bryant.h>
+").
 
 :- pragma c_code(one = (F::out), [will_not_call_mercury],
 		"F = (Word) trueVar();").
@@ -181,7 +220,8 @@
 :- 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],
+:- 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), 
@@ -203,6 +243,10 @@
 
 (~F) = ite(F, zero, one).
 
+:- pragma c_code(entails(X::in, Y::in), [will_not_call_mercury],
+	"SUCCESS_INDICATOR =
+		(ite_constant((node *) X, (node *) Y, one) == one);").
+
 :- pragma c_code(var_entailed(F::in, V::in), [will_not_call_mercury],
 		"SUCCESS_INDICATOR = var_entailed((node *) F, (int) V);").
 
-- 
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
--------------------------------------------------------------------------