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

[Peter Schachte]

On Fri, Jul 07, 2000 at 11:53:50AM +1000, David Overton wrote:
> 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.
> 
> ===================================================================
> 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 @@


> +/* 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.

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.


> @@ -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.

> ===================================================================
> 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.


> @@ -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).


> ===================================================================
> 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.

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.


> +%-----------------------------------------------------------------------------%
> +%-----------------------------------------------------------------------------%
> +
> +:- 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.

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.


> +:- 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.


Otherwise this looks good to me.

-- 
Peter Schachte <schachte at cs.mu.OZ.AU>  Reality is for those who can't face
http://www.cs.mu.oz.au/~schachte/      Science Fiction. 
Phone:  +61 3 8344 9166                
Fax:    +61 3 9348 1184                
--------------------------------------------------------------------------
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
--------------------------------------------------------------------------