[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