From 75ff9d58c504b2b3719581e187a485dad3258c0a Mon Sep 17 00:00:00 2001 From: David Overton Date: Fri, 10 Mar 2000 05:17:23 +0000 Subject: [PATCH] Import Peter Schachte's ROBDD package into the Mercury repository as Estimated hours taken: 0.2 Import Peter Schachte's ROBDD package into the Mercury repository as `mercury/robdd'. Vendor tag is `robdd'. Release tag is `REL_1_0'. --- robdd/Makefile | 244 ++++ robdd/README | 25 + robdd/bryant.c | 3044 +++++++++++++++++++++++++++++++++++++++++ robdd/bryant.h | 405 ++++++ robdd/bryantPrint.c | 64 + robdd/bryantPrint.h | 0 robdd/runall | 27 + robdd/table.c | 148 ++ robdd/table.h | 6 + robdd/test_abexit.c | 177 +++ robdd/test_abunify.c | 205 +++ robdd/test_glb.c | 195 +++ robdd/test_iff.c | 156 +++ robdd/test_rename.c | 168 +++ robdd/test_restrict.c | 167 +++ robdd/test_rglb.c | 207 +++ robdd/test_upclose.c | 155 +++ robdd/test_var.c | 189 +++ robdd/test_vars.c | 193 +++ robdd/timing.c | 40 + robdd/timing.h | 13 + robdd/var.h | 13 + 22 files changed, 5841 insertions(+) create mode 100644 robdd/Makefile create mode 100644 robdd/README create mode 100644 robdd/bryant.c create mode 100644 robdd/bryant.h create mode 100644 robdd/bryantPrint.c create mode 100644 robdd/bryantPrint.h create mode 100755 robdd/runall create mode 100644 robdd/table.c create mode 100644 robdd/table.h create mode 100644 robdd/test_abexit.c create mode 100644 robdd/test_abunify.c create mode 100644 robdd/test_glb.c create mode 100644 robdd/test_iff.c create mode 100644 robdd/test_rename.c create mode 100644 robdd/test_restrict.c create mode 100644 robdd/test_rglb.c create mode 100644 robdd/test_upclose.c create mode 100644 robdd/test_var.c create mode 100644 robdd/test_vars.c create mode 100644 robdd/timing.c create mode 100644 robdd/timing.h create mode 100644 robdd/var.h diff --git a/robdd/Makefile b/robdd/Makefile new file mode 100644 index 000000000..7ed677ac2 --- /dev/null +++ b/robdd/Makefile @@ -0,0 +1,244 @@ +# 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 + + +TESTS= test_abexit test_abunify test_iff test_glb test_rglb test_rename \ + test_restrict test_var test_vars +TESTOS= test_abexit.o test_abunify.o test_iff.o test_glb.o test_rglb.o \ + test_rename.o test_restrict.o test_var.o test_vars.o + +COMMONOS=bryant.o bryantPrint.o +SOOS=$(COMMONOS) +OS=$(COMMONOS) timing.o +RELFILES=bryant.c bryant.h bryantPrint.c var.h Makefile \ + test_abexit.c test_iff.c test_rglb.c test_abunify.c test_rename.c \ + test_var.c test_glb.c test_restrict.c test_vars.c test_upclose.c +GENFILES=$(COMMONOS) $(TESTOS) + +# Amiga options +#LINKSW=LINK PNAME +#DEF=DEFINE= +#MSGS= +#RM=delete quiet +#MV=move clone +#MKDIR=makedir +#DEBUG=DEBUG=SF NOOPT DEFINE=DEBUGALL +#OPTIMIZE=OPTIMIZE NODEBUG DEFINE=NDEBUG +#MAKE=smake +#LIBS= +#SOLIBS= + +# Unix options +LINKSW=-o +DEF=-D +MSGS=-Wall +RM=rm -f +MV=mv +MKDIR=mkdir +DEBUG=-g -DDEBUGALL +OPTIMIZE=-O3 -DNDEBUG -funroll-loops +CC=gcc -I../mylib -I/usr/ucbinclude -I. -ansi +LIBDIRS=-L/home/staff/pets/quintus/bin3.2/sun4-5 +#LIBS= -L/usr/ucblib -lucb +LIBS= +SOLIBS= +OLIBS=-lqp +SOOPTS=-fpic + + +# General options + +CHOSENOPTIM=$(OPTIMIZE) +#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)STATISTICS +#WHICH=NAIVE +#WHICH=OLD +#WHICH=USE_THRESH +#WHICH=USE_RGLB +WHICH=NEW + +QOPT= +#QOPT=$(DEF)QUINTUS + +RSET=$(DEF)RESTRICT_SET + + +# Main makefile + +CFLAGS=$(CHOSENOPTIM) $(DEF)$(WHICH) $(OPTS) $(RSET) $(QOPT) $(MSGS) $(EXTRAOPTS) + +all: $(TESTS) + +everything: alltests allsos + +alltests: naive old thresh rglb new + +naive-enum: naive-enumtests + $(MAKE) clean + $(MAKE) WHICH=NAIVE RSET= all + $(RM) naive-enumtests/* + $(MV) $(TESTS) naive-enumtests + +old-enum: old-enumtests + $(MAKE) clean + $(MAKE) WHICH=OLD RSET= all + $(RM) old-enumtests/* + $(MV) $(TESTS) old-enumtests + +naive: naivetests + $(MAKE) clean + $(MAKE) WHICH=NAIVE all + $(RM) naivetests/* + $(MV) $(TESTS) naivetests + +old: oldtests + $(MAKE) clean + $(MAKE) WHICH=OLD all + $(RM) oldtests/* + $(MV) $(TESTS) oldtests + +thresh: threshtests + $(MAKE) clean + $(MAKE) WHICH=USE_THRESH all + $(RM) threshtests/* + $(MV) $(TESTS) threshtests + +rglb: rglbtests + $(MAKE) clean + $(MAKE) WHICH=USE_RGLB all + $(RM) rglbtests/* + $(MV) $(TESTS) rglbtests + +new: newtests + $(MAKE) clean + $(MAKE) WHICH=NEW all + $(RM) newtests/* + $(MV) $(TESTS) newtests + + +allsos: naiveso oldso threshso rglbso newso bryant.so + +naiveso: naivetests + $(MAKE) clean + $(MAKE) WHICH=NAIVE QOPT=$(DEF)QUINTUS EXTRAOPTS=$(SOOPTS) rep.so + $(RM) naivetests/rep.so + $(MV) rep.so naivetests + +oldso: oldtests + $(MAKE) clean + $(MAKE) WHICH=OLD QOPT=$(DEF)QUINTUS EXTRAOPTS=$(SOOPTS) rep.so + $(RM) oldtests/rep.so + $(MV) rep.so oldtests + +threshso: threshtests + $(MAKE) clean + $(MAKE) WHICH=USE_THRESH QOPT=$(DEF)QUINTUS EXTRAOPTS=$(SOOPTS) rep.so + $(RM) threshtests/rep.so + $(MV) rep.so threshtests + +rglbso: rglbtests + $(MAKE) clean + $(MAKE) WHICH=USE_RGLB QOPT=$(DEF)QUINTUS EXTRAOPTS=$(SOOPTS) rep.so + $(RM) rglbtests/rep.so + $(MV) rep.so rglbtests + +newso: newtests + $(MAKE) clean + $(MAKE) WHICH=NEW QOPT=$(DEF)QUINTUS EXTRAOPTS=$(SOOPTS) rep.so + $(RM) newtests/rep.so + $(MV) rep.so newtests + + +bryant.so: + $(MAKE) clean + $(MAKE) WHICH=NEW QOPT=$(DEF)QUINTUS EXTRAOPTS=$(SOOPTS) $(SOOS) + gcc -shared -o $@ $(SOOS) $(SOLIBS) + + +naive-enumtests old-enumtests naivetests oldtests threshtests rglbtests newtests: + $(MKDIR) $@ + + +bryantPrint.o: bryantPrint.c bryant.h bryantPrint.h + +bryant.o: bryant.c bryant.h + +test_abexit.o: test_abexit.c bryant.h timing.h + +test_abunify.o: test_abunify.c bryant.h timing.h + +test_iff.o: test_iff.c bryant.h timing.h + +test_glb.o: test_glb.c bryant.h timing.h + +test_rglb.o: test_rglb.c bryant.h timing.h + +test_rename.o: test_rename.c bryant.h timing.h + +test_restrict.o: test_restrict.c bryant.h timing.h + +test_var.o: test_var.c bryant.h timing.h + +test_vars.o: test_vars.c bryant.h timing.h + + +rep.so: $(SOOS) + gcc -shared -o $@ $(SOOS) $(SOLIBS) + +rep.o: $(SOOS) + gcc -o $@ $(LIBDIRS) $(SOOS) $(OLIBS) + +test: test.o $(OS) + $(CC) $(LINKSW) $@ test.o $(OS) $(LIBS) LINK + +test_abexit: test_abexit.o $(OS) + $(CC) $(LINKSW) $@ test_abexit.o $(OS) $(LIBS) + +test_abunify: test_abunify.o $(OS) + $(CC) $(LINKSW) $@ test_abunify.o $(OS) $(LIBS) + +test_iff: test_iff.o $(OS) + $(CC) $(LINKSW) $@ test_iff.o $(OS) $(LIBS) + +test_glb: test_glb.o $(OS) + $(CC) $(LINKSW) $@ test_glb.o $(OS) $(LIBS) + +test_rglb: test_rglb.o $(OS) + $(CC) $(LINKSW) $@ test_rglb.o $(OS) $(LIBS) + +test_rename: test_rename.o $(OS) + $(CC) $(LINKSW) $@ test_rename.o $(OS) $(LIBS) + +test_restrict: test_restrict.o $(OS) + $(CC) $(LINKSW) $@ test_restrict.o $(OS) $(LIBS) + +test_var: test_var.o $(OS) + $(CC) $(LINKSW) $@ test_var.o $(OS) $(LIBS) + +test_vars: test_vars.o $(OS) + $(CC) $(LINKSW) $@ test_vars.o $(OS) $(LIBS) + +test_upclose: test_upclose.o $(OS) + $(CC) $(LINKSW) $@ test_upclose.o $(OS) $(LIBS) + +abex: $(OS) abex.o + $(CC) $(LINKSW) $@ $@.o $(OS) $(LIBS) + +clean: + - $(RM) $(GENFILES) + +distrib: bryant.tgz + +bryant.tgz: $(RELFILES) + -$(RM) $@ + tar cvfz $@ $(RELFILES) + +tidy: clean + - $(RM) $(TESTS) + - $(RM) *~ diff --git a/robdd/README b/robdd/README new file mode 100644 index 000000000..d1adbe32b --- /dev/null +++ b/robdd/README @@ -0,0 +1,25 @@ +This directory contains source code for handling Reduced Ordered +Binary Decision Diagrams (ROBDDs). bryant.c contains almost all of +the code; bryantPrint.c contains only code for printing ROBDDs. + +This code could really use a good spring cleaning. My apologies for +not taking the time to do that yet. Much of the complication of the +code stems from maintaining several different versions of the code in +a single file. For users of this code these versions are probably not +very interesting. They are there for experimenting with various +implementations. + + +Building the ROBDD code: + +A Makefile is provided; if you just wish to link the ROBDD code with +your own code, making bryant.o and maybe bryantPrint.o should be +enough. + +If you wish to use this ROBDD code as part of my groundness analyzer, +then you just want to do + + make bryant.so + +and then move bryant.so to ../analyzer/rep.so + diff --git a/robdd/bryant.c b/robdd/bryant.c new file mode 100644 index 000000000..0680d9d57 --- /dev/null +++ b/robdd/bryant.c @@ -0,0 +1,3044 @@ +/***************************************************************** + File : bryant.c + RCS : $Id: bryant.c,v 1.1 2000-03-10 05:17:21 dmo Exp $ + Author : Peter Schachte, based on code by Tania Armstrong + Purpose : Manipulation of boolean functions + Copyright: © 1995 Peter Schachte. All rights reserved. + +*****************************************************************/ + +/***************************************************************** + + Controlling #defined Symbols + + + This code is conditionalized on a number of #defined symbols. They are: + + STATISTICS Controls collecting of computed and unique + table hash performance. If defined, + concludeRep() prints out a bunch of + statistics. + + CLEAR_CACHES If defined, all computed and unique tables are + cleared on a call to initRep(). This makes + running a number of tests in sequence more + fair. + + NAIVE If defined, uses very naive algorithms for + iff_conj_array, renameArray, lub, glb, + and probably some I've forgotten. + + OLD If defined, use slightly less naive algorithms for + restrictThresh, restricted_glb, vars_entailed, + and iff_conj_array. + + USE_THRESH Like OLD, except that it does use the new code + for restrictThresh. Implies OLD. + + USE_RGLB Like USE_THRESH, except that it also uses the + new code for restricted_glb. Implies USE_THRESH. + + NEW Like USE_RGLB, but uses all the lastest and greatest + algorithms. Implies USE_RGLB. + + USE_ITE_CONSTANT Include the ite_constant function, and use it + to speed up the non-NEW version of + var_entailed (and vars_entailed). + + SHARING Include algorithms useful in sharing analysis + performed using Boolean functions. + + RESTRICT_SET Only meaningful if OLD && !USE_THRESH. If + defined, then we restrict by making a first pass + over the ROBDD finding the set of variables + present that are greater than the threshold, and + then restrict away each variable in that set. + + WHICH Is defined to "NAIVE", "OLD", "USE_THRESH", + "USE_RGLB", or "NEW", depending on which of + the NAIVE, OLD, USE_THRESH, and USE_RGLB + variables are defined. This is automatically + defined by bryant.h based on the above + variables. + + VE_GLB (only when OLD is defined) if defined, + var_entailed(fn, v) compares the fn to + glb(variableRep(v), fn). The var is entailed + if they are equal. Otherwise computes + variableRep(v) -> fn. The variable is + entailed if this is 'one'. + + ELIM_DUPS If defined, iff_conj_array will not assume + that the input array has no duplicates. It + will still assume that it's sorted. + + COMPUTED_TABLE Enables the computed table in lub, glb, ite, + and restricted_glb. + + EQUAL_TEST If defined, lub(), glb(), and restricted_glb + compare their arguments for equality, and if + equal return it as value. ite and ite_var + always do this with their last 2 args. The + equality test is pretty cheap, and the savings + will sometimes be huge, so this should + probably always be defined. + + NO_CHEAP_SHIFT If defined, shifting an integer variable number + of places is relatively expensive on this platform, + and so should be avoided. In this case we use a + table where possible to avoid shifting. + + +*****************************************************************/ + +#include +#include +#include +#include +#include +#include "bryant.h" + + +#define UNUSED_MAPPING -1 /* this MUST BE -1 */ + +#if !defined(max) +#define max(a,b) ((a)<(b) ? (b) : (a)) +#endif +#if !defined(min) +#define min(a,b) ((a)<(b) ? (a) : (b)) +#endif + +#define PERCENTAGE(x,y) ((100.0 * (float)(x)) / (float)(y)) + +typedef struct pool { + node data[POOL_SIZE]; + struct pool *prev; +} pool; + + +#if defined(NO_CHEAP_SHIFT) && BITS_PER_WORD == 32 +bitmask following_bits[BITS_PER_WORD] = + { 0xffffffff, 0xfffffffe, 0xfffffffc, 0xfffffff8, + 0xfffffff0, 0xffffffe0, 0xffffffc0, 0xffffff80, + 0xffffff00, 0xfffffe00, 0xfffffc00, 0xfffff800, + 0xfffff000, 0xffffe000, 0xffffc000, 0xffff8000, + 0xffff0000, 0xfffe0000, 0xfffc0000, 0xfff80000, + 0xfff00000, 0xffe00000, 0xffc00000, 0xff800000, + 0xff000000, 0xfe000000, 0xfc000000, 0xf8000000, + 0xf0000000, 0xe0000000, 0xc0000000, 0x80000000 + }; + +bitmask preceding_bits[BITS_PER_WORD] = + { 0x00000001, 0x00000003, 0x00000007, 0x0000000f, + 0x0000001f, 0x0000003f, 0x0000007f, 0x000000ff, + 0x000001ff, 0x000003ff, 0x000007ff, 0x00000fff, + 0x00001fff, 0x00003fff, 0x00007fff, 0x0000ffff, + 0x0001ffff, 0x0003ffff, 0x0007ffff, 0x000fffff, + 0x001fffff, 0x003fffff, 0x007fffff, 0x00ffffff, + 0x01ffffff, 0x03ffffff, 0x07ffffff, 0x0fffffff, + 0x1fffffff, 0x3fffffff, 0x7fffffff, 0xffffffff + }; +#endif + + +unsigned char first_one_bit[256] = + {255, 0, 1, 0, 2, 0, 1, 0, 3, 0, 1, 0, 2, 0, 1, 0, /* 16 */ + 4, 0, 1, 0, 2, 0, 1, 0, 3, 0, 1, 0, 2, 0, 1, 0, /* 32 */ + 5, 0, 1, 0, 2, 0, 1, 0, 3, 0, 1, 0, 2, 0, 1, 0, /* 48 */ + 4, 0, 1, 0, 2, 0, 1, 0, 3, 0, 1, 0, 2, 0, 1, 0, /* 64 */ + 6, 0, 1, 0, 2, 0, 1, 0, 3, 0, 1, 0, 2, 0, 1, 0, /* 80 */ + 4, 0, 1, 0, 2, 0, 1, 0, 3, 0, 1, 0, 2, 0, 1, 0, /* 96 */ + 5, 0, 1, 0, 2, 0, 1, 0, 3, 0, 1, 0, 2, 0, 1, 0, /* 112 */ + 4, 0, 1, 0, 2, 0, 1, 0, 3, 0, 1, 0, 2, 0, 1, 0, /* 128 */ + 7, 0, 1, 0, 2, 0, 1, 0, 3, 0, 1, 0, 2, 0, 1, 0, /* 144 */ + 4, 0, 1, 0, 2, 0, 1, 0, 3, 0, 1, 0, 2, 0, 1, 0, /* 160 */ + 5, 0, 1, 0, 2, 0, 1, 0, 3, 0, 1, 0, 2, 0, 1, 0, /* 176 */ + 4, 0, 1, 0, 2, 0, 1, 0, 3, 0, 1, 0, 2, 0, 1, 0, /* 192 */ + 6, 0, 1, 0, 2, 0, 1, 0, 3, 0, 1, 0, 2, 0, 1, 0, /* 208 */ + 4, 0, 1, 0, 2, 0, 1, 0, 3, 0, 1, 0, 2, 0, 1, 0, /* 224 */ + 5, 0, 1, 0, 2, 0, 1, 0, 3, 0, 1, 0, 2, 0, 1, 0, /* 240 */ + 4, 0, 1, 0, 2, 0, 1, 0, 3, 0, 1, 0, 2, 0, 1, 0, /* 256 */ + }; + +unsigned char last_one_bit[256] = + {255, 0, 1, 1, 2, 2, 2, 2, 3, 3, 3, 3, 3, 3, 3, 3, /* 16 */ + 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, /* 32 */ + 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, /* 48 */ + 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, /* 64 */ + 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, /* 80 */ + 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, /* 96 */ + 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, /* 112 */ + 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, /* 128 */ + 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, /* 144 */ + 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, /* 160 */ + 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, /* 176 */ + 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, /* 192 */ + 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, /* 208 */ + 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, /* 224 */ + 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, /* 240 */ + 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, /* 256 */ + }; + + +/* automatically initialized to all 0 bits: */ +bitset emptyset; + +/**************************************************************** + + Macros to avoid #ifdefs + + ****************************************************************/ + + +#if defined(COMPUTED_TABLE) && defined(CLEAR_CACHES) +#define CLEAR_CACHE(op) \ +memset(op##_computed_cache, 0, sizeof(op##_computed_cache)) +#else /* !CLEAR_CACHES || !COMPUTED_TABLE */ +#define CLEAR_CACHE(op) +#endif + + +#if defined(STATISTICS) + +/* The largest bucket size to be separately counted. Larger buckets + * will be listed as "> MAX_COUNT." + */ +#define MAX_COUNT 1000 + +int unique_table_hits, unique_table_misses; + +#define DECLARE_FN_COUNT(op) int op##_count; + +#define COUNT_FN(fn) (++fn##_count) + +#define INIT_FN_COUNT(fn) fn##_count = 0 +#define PRINT_FN_COUNT(fn) \ + if (fn##_count!=0) printf("%6d calls to " #fn "\n", fn##_count); + +#define COUNT_UNIQUE_HIT (++unique_table_hits) +#define COUNT_UNIQUE_MISS (++unique_table_misses) + +#if defined(COMPUTED_TABLE) + +#define COUNT_HIT(op) (++op##_computed_hits) +#define COUNT_MISS(op) (++op##_computed_misses, ++cache->count) +#define INIT_CACHE(op) \ + do { \ + op##_computed_misses = 0; \ + op##_computed_hits = 0; \ + CLEAR_CACHE(op); \ + } while (0) + +#define CACHE_COUNT_MEMBER int count; +#define PRINT_CACHE_PERFORMANCE(op) \ +do { \ + if (op##_computed_misses > 0 ) { \ + int i, size_count[MAX_COUNT+2]; \ + printf(#op " computed table: %d hits, %d misses, %.2f%% hit rate\n",\ + op##_computed_hits, op##_computed_misses, \ + PERCENTAGE(op##_computed_hits, \ + op##_computed_hits + op##_computed_misses)); \ + memset(size_count, 0, sizeof(size_count)); \ + for (i=0; iprev; \ + free(curr_pool); \ + curr_pool = p; \ + } \ + curr_pool_ptr = curr_pool_end_ptr = NULL; \ + pool_count = 0; \ + } while (0) +#else /* !CLEAR_CACHES */ +#define INIT_UNIQUE_TABLE +#endif /* CLEAR_CACHES */ + + + +/******************************************************************** + + Caching of computed values + + For improved efficiency, if COMPUTED_TABLE is defined we maintain a + cache of previously computed values to certain functions, and use + this to avoid costly computations when possible. This is + particularly important for ROBDDs, because the high degree of fan-in + causes frequent repeated computations. + + Because caching is in many ways extraneous to the functions being + cached, we put the caching code here as macros, so that the + presentation of the algorithms is minimally impacted by caching. + + ********************************************************************/ + +#if defined(COMPUTED_TABLE) + +#if defined(STATISTICS) +#define DECLARE_CACHE(op,type) \ +static int op##_computed_hits; \ +static int op##_computed_misses; \ +static type op##_computed_cache[COMPUTED_TABLE_SIZE] +#else /* !STATISTICS */ +#define DECLARE_CACHE(op,type) \ +static type op##_computed_cache[COMPUTED_TABLE_SIZE] +#endif /* STATISTICS */ + +/**************************** the cache for ite **************************/ + +#define TERNARY_NODE_HASH(f,g,h) \ + (((INTCAST(f)>>4)+INTCAST(g)+(INTCAST(h)<<1)) % COMPUTED_TABLE_SIZE) + +typedef struct { + node *f; + node *g; + node *h; + node *result; + CACHE_COUNT_MEMBER +} ite_cache_entry; + +DECLARE_CACHE(ite, ite_cache_entry); +#if defined(USE_ITE_CONSTANT) +DECLARE_CACHE(ite_constant, ite_cache_entry); +#endif /* USE_ITE_CONSTANT */ + +#define DECLARE_ITE_CACHE_ENTRY ite_cache_entry *cache; + +#define TRY_ITE_CACHE(n1,n2,n3,op) \ +do { \ + cache = &op##_computed_cache[TERNARY_NODE_HASH(n1,n2,n3)]; \ + if (cache->f==n1 && cache->g==n2 && cache->h==n3) { \ + COUNT_HIT(op); \ + return cache->result; \ + } \ +} while (0) + +#define UPDATE_ITE_CACHE(n1,n2,n3,node,op) \ +do { \ + cache->f = n1; \ + cache->g = n2; \ + cache->h = n3; \ + cache->result = node; \ + COUNT_MISS(op); \ +} while (0) + + +/******************** the cache for unary operations ************/ + +#define UNARY_NODE_HASH(a) \ + (INTCAST(a) % COMPUTED_TABLE_SIZE) + +typedef struct { + node *f; + node *result; + CACHE_COUNT_MEMBER +} unary_cache_entry; + +#if defined(SHARING) +DECLARE_CACHE(upclose, unary_cache_entry); +#if defined(NEW) +DECLARE_CACHE(complete_one, unary_cache_entry); +#endif /* NEW */ +#endif /* SHARING */ + +#define DECLARE_UNARY_CACHE_ENTRY unary_cache_entry *cache; + +#define UPDATE_UNARY_CACHE(n,node,op) \ +do { \ + cache->f = n; \ + cache->result = node; \ + COUNT_MISS(op); \ +} while (0) + +#define TRY_UNARY_CACHE(n,op) \ +do { \ + cache = &((op##_computed_cache)[UNARY_NODE_HASH(n)]); \ + if (cache->f==(n)) { \ + COUNT_HIT(op); \ + return cache->result; \ + } \ +} while (0) + + +/******************** the cache for var_entailed ************/ + +#define VAR_ENTAILED_HASH(a,n) \ + ((INTCAST(a)+n) % COMPUTED_TABLE_SIZE) + +typedef struct { + node *f; + int n; + int result; + CACHE_COUNT_MEMBER +} var_entailed_cache_entry; + +#if defined(USE_RGLB) +DECLARE_CACHE(var_entailed, var_entailed_cache_entry); +#endif /* USE_RGLB */ + +#define DECLARE_VAR_ENTAILED_CACHE_ENTRY var_entailed_cache_entry *cache; + +#define UPDATE_VAR_ENTAILED_CACHE(node,var,val) \ +do { \ + cache->f = node; \ + cache->n = var; \ + cache->result = val; \ + COUNT_MISS(var_entailed); \ +} while (0) + +#define TRY_VAR_ENTAILED_CACHE(node,var) \ +do { \ + cache = &((var_entailed_computed_cache) \ + [VAR_ENTAILED_HASH(node,var)]); \ + if (cache->f==(node) && cache->n==(var)) { \ + COUNT_HIT(op); \ + return cache->result; \ + } \ +} while (0) + + +/**************** the cache for unary set-valued operations ********/ + +typedef struct { + node *f; + bitset result; + CACHE_COUNT_MEMBER +} unary_bitset_cache_entry; + +#if defined(NEW) +DECLARE_CACHE(vars_entailed, unary_bitset_cache_entry); +#endif + +#define DECLARE_UNARY_BITSET_CACHE_ENTRY \ + unary_bitset_cache_entry *cache; + + +#define UPDATE_UNARY_BITSET_CACHE(n,set,op) \ +do { \ + cache->f = n; \ + cache->result = set; \ + COUNT_MISS(op); \ +} while (0) + +#define TRY_UNARY_BITSET_CACHE(n,op) \ +do { \ + cache = &((op##_computed_cache)[UNARY_NODE_HASH(n)]); \ + if (cache->f==(n)) { \ + COUNT_HIT(op); \ + return &cache->result; \ + } \ +} while (0) + + +/******************** the cache for symmetric binary operations ************/ + +/* NB: Since glb and lub are commutative, cache entries will work both + * ways round, so we want a symmetrical cache, ie, (a,b) should hash + * to the same value as (b,a). We achieve this by first exchanging a and b + * if a > b (comparing their addresses) in TRY_BIN_CACHE. We assume that + * they won't be changed (or exchanged) before UPDATE_BIN_CACHE is called. + */ + +#define BINARY_NODE_HASH(a,b) \ + ((INTCAST(a)+(INTCAST(b)<<1)) % COMPUTED_TABLE_SIZE) + +typedef struct { + node *f; + node *g; + node *result; + CACHE_COUNT_MEMBER +} bin_cache_entry; + +DECLARE_CACHE(glb, bin_cache_entry); +DECLARE_CACHE(lub, bin_cache_entry); +#if defined(SHARING) +DECLARE_CACHE(bin, bin_cache_entry); +DECLARE_CACHE(complete, bin_cache_entry); +#endif + +#define DECLARE_BIN_CACHE_ENTRY bin_cache_entry *cache; + +#define UPDATE_BIN_CACHE(n1,n2,node,op) \ +do { \ + cache->f = n1; \ + cache->g = n2; \ + cache->result = node; \ + COUNT_MISS(op); \ +} while (0) + +#define TRY_BIN_CACHE(n1,n2,op) \ +do { \ + if (n2 < n1) { node *temp = (n2); (n2) = (n1); (n1) = temp; } \ + cache = &((op##_computed_cache)[BINARY_NODE_HASH(n1,n2)]); \ + if (cache->f==(n1) && cache->g==(n2)) { \ + COUNT_HIT(op); \ + return cache->result; \ + } \ +} while (0) + +/******************** the cache for asymmetric binary operations ************/ + +#if defined(SHARING) && defined(NEW) +DECLARE_CACHE(complete_one_or, bin_cache_entry); + +#define DECLARE_ASYM_BIN_CACHE_ENTRY bin_cache_entry *cache; + +#define UPDATE_ASYM_BIN_CACHE(n1,n2,node,op) \ + UPDATE_BIN_CACHE(n1,n2,node,op) + +#define TRY_ASYM_BIN_CACHE(n1,n2,op) \ +do { \ + cache = &((op##_computed_cache)[BINARY_NODE_HASH(n1,n2)]); \ + if (cache->f==(n1) && cache->g==(n2)) { \ + COUNT_HIT(op); \ + return cache->result; \ + } \ +} while (0) +#endif /* SHARING && NEW */ + +/**************************** the cache for rglb ***********************/ + +#if defined(USE_RGLB) + +typedef struct { + node *f; + node *g; + node *result; + int thresh; + CACHE_COUNT_MEMBER +} rglb_cache_entry; + +DECLARE_CACHE(rglb, rglb_cache_entry); + +#define DECLARE_RGLB_CACHE_ENTRY rglb_cache_entry *cache; + +#define TRY_RGLB_CACHE(n1,n2,th) \ +do { \ + if (n2 < n1) { node *temp = (n2); (n2) = (n1); (n1) = temp; } \ + cache = &rglb_computed_cache[BINARY_NODE_HASH(n1,n2)]; \ + if (cache->f==(n1) && cache->g==(n2) && \ + cache->thresh >= th) { \ + COUNT_HIT(rglb); \ + if (cache->thresh == th) return cache->result; \ + return restrictThresh(th, cache->result); \ + } \ +} while (0) + +#define UPDATE_RGLB_CACHE(n1,n2,th,node) \ +do { \ + cache->f = n1; \ + cache->g = n2; \ + cache->thresh = th; \ + cache->result = node; \ + COUNT_MISS(rglb); \ +} while (0) + +#endif /* USE_RGLB */ + +/************************ the cache for complete_or *******************/ + +#if defined(SHARING) && defined(NEW) +typedef struct { + node *f; + node *g; + node *prev; + node *result; + CACHE_COUNT_MEMBER +} complete_or_cache_entry; + +DECLARE_CACHE(complete_or, complete_or_cache_entry); + +#define DECLARE_COMPLETE_OR_CACHE_ENTRY complete_or_cache_entry *cache; + +#define TRY_COMPLETE_OR_CACHE(n1,n2,pr) \ +do { \ + if (n2 < n1) { node *temp = (n2); (n2) = (n1); (n1) = temp; } \ + cache = &complete_or_computed_cache[TERNARY_NODE_HASH(n1,n2,pr)]; \ + if ((cache->f==n1 && cache->g==n2 && cache->prev==pr)) { \ + COUNT_HIT(complete_or); \ + return cache->result; \ + } \ +} while (0) + +#define UPDATE_COMPLETE_OR_CACHE(n1,n2,pr,node) \ +do { \ + cache->f = n1; \ + cache->g = n2; \ + cache->prev = pr; \ + cache->result = node; \ + COUNT_MISS(complete_or); \ +} while (0) + +#endif /* SHARING && NEW */ + +/**************************** the cache for ite_var ***********************/ + +#if defined(NEW) + +#define ITE_VAR_COMPUTED_HASH(f,g,h) \ + ((f+INTCAST(g)+(INTCAST(h)<<1)) % COMPUTED_TABLE_SIZE) + +typedef struct { + int f; + node *g; + node *h; + node *result; + CACHE_COUNT_MEMBER +} ite_var_cache_entry; + +DECLARE_CACHE(ite_var, ite_var_cache_entry); + +#define DECLARE_ITE_VAR_CACHE_ENTRY ite_var_cache_entry *cache; + +#define TRY_ITE_VAR_CACHE(n1,n2,h) \ +do { \ + cache = \ + &ite_var_computed_cache[ITE_VAR_COMPUTED_HASH(n1,n2,h)];\ + if (cache->f==n1 && cache->g==n2 && cache->h==h) { \ + COUNT_HIT(ite_var); \ + return cache->result; \ + } \ +} while (0) + +#define UPDATE_ITE_VAR_CACHE(n1,n2,h,node)\ +do { \ + cache->f = n1; \ + cache->g = n2; \ + cache->h = h; \ + cache->result = node; \ + COUNT_MISS(ite_var); \ +} while (0) + +#endif /* NEW */ + + +#else /* !COMPUTED_TABLE */ +/**************************** no caching at all **************************/ +#define DECLARE_ITE_CACHE_ENTRY +#define TRY_ITE_CACHE(n1,n2,n3,op) +#define UPDATE_ITE_CACHE(n1,n2,n3,node,op) +#define DECLARE_BIN_CACHE_ENTRY +#define TRY_BIN_CACHE(n1,n2,op) +#define UPDATE_BIN_CACHE(n1,n2,node,op) +#define DECLARE_UNARY_CACHE_ENTRY +#define UPDATE_UNARY_CACHE(n,node,op) +#define TRY_UNARY_CACHE(n,op) +#define DECLARE_ASYM_BIN_CACHE_ENTRY +#define UPDATE_ASYM_BIN_CACHE(n1,n2,node,op) +#define TRY_ASYM_BIN_CACHE(n1,n2,op) +#define DECLARE_RGLB_CACHE_ENTRY +#define TRY_RGLB_CACHE(n1,n2,th) +#define UPDATE_RGLB_CACHE(n1,n2,th,node) +#define DECLARE_ITE_VAR_CACHE_ENTRY +#define TRY_ITE_VAR_CACHE(n1,n2,h) +#define UPDATE_ITE_VAR_CACHE(n1,n2,h,node) +#define DECLARE_COMPLETE_OR_CACHE_ENTRY +#define TRY_COMPLETE_OR_CACHE(n1,n2,pr) +#define UPDATE_COMPLETE_OR_CACHE(n1,n2,pr,node) + +#undef COMPUTED_TABLE_SIZE +#define COMPUTED_TABLE_SIZE 0 +#endif /* COMPUTED_TABLE */ + + + +/**************************************************************** + + The Unique Table + + ****************************************************************/ + + +static node *unique_table[UNIQUE_TABLE_SIZE]; + +#define UNIQUE_HASH(var,tr,fa) \ + (((var)+INTCAST(tr)+(INTCAST(fa)<<1)) % UNIQUE_TABLE_SIZE) + + + +/**************************************************************** + + Prototypes + + ****************************************************************/ + +extern void printBryant(node *a); + +node *ite(node *f,node *g,node *h); /* if then else algorithm */ +node *restricted_iff_conj_array(int v0, int n, int arr[], int thresh); + + +node *renameArray(node *in, int count, int mappping[]); +node *reverseRenameArray(node *in, int count, int rev_mappping[]); + +node *complete(node *f, node *g); +node *bin_univ(node *f); + +static int intcompare(const void *i, const void *j); + +/**************************************************************** + + Inline Bit Set Stuff + + ****************************************************************/ + +/* next_element() finds the next element in set beginning with var, + * and updates var, word, and mask to refer to it. + * prev_element() finds the next earlier element in set. + * next_nonelement() finds the next potential element of set that is in + * fact not an element of set. + * prev_nonelement() finds the next earlier non-element of set. + * + * NB: if the initally supplied element is a member of the set, next_element + * and prev_element will happily return that one. Similarly, + * next_nonelement and prev_nonelement will happily return the initial + * input if it fits the bill. That is, these find the next or next + * earlier element INLCUDING THE INITIAL ONE that meets the criterion. + */ + +#if defined(NO_CHEAP_SHIFT) +__inline int next_element(bitset *set, int *var, int *word, bitmask *mask) + { + int vr = *var; + int wd = *word; + bitmask f = FOLLOWING_BITS(vr&(BITS_PER_WORD-1)); + bitmask *ptr = &(set->bits[wd]); + bitmask bits = *ptr; + bitmask msk = *mask; + + assert(vr >= 0 && vr < MAXVAR); + + if ((bits&f) == 0) { + do { + if (++wd > ((MAXVAR-1)/BITS_PER_WORD)) return FALSE; + } while ((bits=*++ptr) == 0); + vr = wd<bits[wd]); + bitmask bits = *ptr&FOLLOWING_BITS(vr&(BITS_PER_WORD-1)); + + assert(vr >= 0 && vr < MAXVAR); + + while (bits == 0) { + if (++wd > (MAXVAR-1)/BITS_PER_WORD) return FALSE; + bits = *++ptr; + } + vr = wd<>= BITS_PER_CHAR; + vr += BITS_PER_CHAR; + assert(vr < (wd+1)<= 0 && vr < MAXVAR); + + bitmask f = PRECEDING_BITS(vr&(BITS_PER_WORD-1)); + bitmask *ptr = &(set->bits[wd]); + bitmask bits = *ptr; + bitmask msk = *mask; + + if ((bits&f) == 0) { + do { + if (--wd < 0) return FALSE; + } while ((bits=*--ptr) == 0); + vr = (wd<>= 1; + assert(vr >= 0); + } + *var = vr; + *word = wd; + *mask = msk; + return TRUE; + } +#else /* !NO_CHEAP_SHIFT */ +__inline int prev_element(bitset *set, int *var, int *word, bitmask *mask) + { + int vr = *var; + int wd = *word; + bitmask *ptr = &(set->bits[wd]); + bitmask bits = *ptr&PRECEDING_BITS(vr&(BITS_PER_WORD-1)); + bitmask temp; + + assert(vr >= 0 && vr < MAXVAR); + + while (bits == 0) { + if (--wd < 0) return FALSE; + bits = *--ptr; + } + + vr = BITS_PER_WORD - BITS_PER_CHAR; + /* I know there's an earlier bit set in bits, so this is safe */ + while ((temp=((bits>>vr)&CHAR_MASK)) == 0) { + vr -= BITS_PER_CHAR; + assert(vr >= 0); + } + vr += (int)last_one_bit[(int)temp]; + vr += (int)wd<bits[wd]); + bitmask bits = *ptr; + bitmask msk = *mask; + + assert(vr >= 0 && vr < MAXVAR); + + if ((bits&f) == f) { + do { + if (++wd >= MAXVAR/BITS_PER_WORD) return FALSE; + } while ((bits=*++ptr) == ~0); + vr = wd<bits[wd]); + bitmask bits = *ptr; + bitmask msk = *mask; + + assert(vr >= 0 && vr < MAXVAR); + + if ((bits&f) == f) { + do { + if (--wd < 0) return FALSE; + } while ((bits=*--ptr) == ~0); + vr = (wd<>= 1; + } + *var = vr; + *word = wd; + *mask = msk; + return TRUE; + } + + + +/* returns 1 if set1 is identical to set2 */ +__inline int bitset_equal(bitset *set1, bitset *set2) + { + bitmask *ptr1 = &set1->bits[0]; + bitmask *ptr2 = &set2->bits[0]; + bitmask *ptr1end = &set1->bits[((MAXVAR-1)/BITS_PER_WORD)+1]; + + for (;;) { + if (*ptr1 != *ptr2) return 0; + if (++ptr1 >= ptr1end) return 1; + ++ptr2; + } + + } + +/* returns 1 if 2 sets are disjoint, else 0 */ +__inline int bitset_disjoint(bitset *set1, bitset *set2) + { + bitmask *ptr1 = &set1->bits[0]; + bitmask *ptr2 = &set2->bits[0]; + bitmask *ptr1end = &set1->bits[((MAXVAR-1)/BITS_PER_WORD)+1]; + + for (;;) { + if ((*ptr1 & *ptr2) != 0) return 0; + if (++ptr1 >= ptr1end) return 1; + ++ptr2; + } + } + + +/* returns 1 if set1 is a subset of set2 */ +__inline int bitset_subset(bitset *set1, bitset *set2) + { + bitmask *ptr1 = &set1->bits[0]; + bitmask *ptr2 = &set2->bits[0]; + bitmask *ptr1end = &set1->bits[((MAXVAR-1)/BITS_PER_WORD)+1]; + + for (;;) { + if ((*ptr1 | *ptr2) != *ptr2) return 0; + if (++ptr1 >= ptr1end) return 1; + ++ptr2; + } + + } + + +/* returns 1 if set1 is a subset of set2 */ +__inline int bitset_empty(bitset *set) + { + bitmask *ptr = &set->bits[0]; + bitmask *ptrend = &set->bits[((MAXVAR-1)/BITS_PER_WORD)+1]; + + for (;;) { + if ((*ptr) != 0) return 0; + if (++ptr >= ptrend) return 1; + } + + } + + +/**************************************************************** + + Making Nodes + + ****************************************************************/ + +static pool *curr_pool = NULL; +static node *curr_pool_ptr = NULL; +static node *curr_pool_end_ptr = NULL; +static int pool_count = 0; + +static node *alloc_node(int value, node* tr, node* fa) + { + pool *newpool; + node *n; + + if (curr_pool_ptr >= curr_pool_end_ptr) { + /* allocate a new pool */ + newpool = 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++; + n->value = value; + n->tr = tr; + n->fa = fa; + return n; + } + +/* 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); + } + + +DECLARE_FN_COUNT(make_node) + +node *make_node(int var, node *tr, node *fa) + { + node **bucket; + node *ptr; + + assert(var>=0); + assert(varvalue > var); + assert(IS_TERMINAL(fa) || fa->value > var); + + COUNT_FN(make_node); + + 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 (ptr!=NULL) { + COUNT_UNIQUE_HIT; + return ptr; + } + + /* node doesn't exist so create it and put in bucket */ + COUNT_UNIQUE_MISS; + ptr = alloc_node(var, tr, fa); + ptr->unique = *bucket; + *bucket = ptr; + return ptr; + } + + +void free_rep(node *n) + { + /* never free ROBDD nodes */ + } + + + +/**************************************************************** + + The Basic Algorithms + + ****************************************************************/ + +int max_variable(void) + { + return MAXVAR; + } + + +node *trueVar(void) + { + return one; + } + + +node *falseVar(void) + { + return zero; + } + + +DECLARE_FN_COUNT(variableRep) + +node *variableRep(int var) + { + COUNT_FN(variableRep); + return make_node(var,one,zero); + } + + +DECLARE_FN_COUNT(ite) + +node *ite(node *f,node *g,node *h) + { + node *f_tr, *f_fa; + node *g_tr, *g_fa; + node *h_tr, *h_fa; + node *newnode; + int top; + DECLARE_ITE_CACHE_ENTRY + + COUNT_FN(ite); + /* terminal cases */ + if (f == one) + return g; + if (f == zero) + return h; + if ((g == one) && (h == zero)) + return f; + if (g == h) + return g; + + /* look it up in computed table; finished if found */ + TRY_ITE_CACHE(f, g, h, ite); + + /* find top variable */ + top = f->value; /* we know f is not terminal */ + if (!IS_TERMINAL(g) && (g->value < top)) top = g->value; + if (!IS_TERMINAL(h) && (h->value < top)) top = h->value; + + /* find then and else branches for recursive calls */ + if (f->value==top) { + f_tr = f->tr; f_fa = f->fa; + } else { + f_tr = f; f_fa = f; + } + if (!IS_TERMINAL(g) && g->value==top) { + g_tr = g->tr; g_fa = g->fa; + } else { + g_tr = g; g_fa = g; + } + if (!IS_TERMINAL(h) && h->value==top) { + h_tr = h->tr; h_fa = h->fa; + } else { + h_tr = h; h_fa = h; + } + + /* create new node and add to table */ + newnode = make_node(top, + ite(f_tr, g_tr, h_tr), + ite(f_fa, g_fa, h_fa)); + UPDATE_ITE_CACHE(f,g,h,newnode,ite); + return newnode; + } + + +#if defined(USE_ITE_CONSTANT) + +/* 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. + */ +node *ite_constant(node *f,node *g,node *h) + { + node *f_tr, *f_fa; + node *g_tr, *g_fa; + node *h_tr, *h_fa; + node *tr_part, *fa_part; + node *result; + int top; + DECLARE_ITE_CACHE_ENTRY + + COUNT_FN(ite); + /* terminal cases */ + if (f == one) + return g; + if (f == zero) + return h; + if (g == h) + return g; + if (IS_TERMINAL(g) && IS_TERMINAL(h)) + /* either f or ~f, which is nonterminal since f is */ + return nonterminal; + + /* look it up in computed table; finished if found */ + TRY_ITE_CACHE(f, g, h, ite_constant); + + /* find top variable */ + top = f->value; /* we know f is not terminal */ + if (!IS_TERMINAL(g) && (g->value < top)) top = g->value; + if (!IS_TERMINAL(h) && (h->value < top)) top = h->value; + + /* find then and else branches for recursive calls */ + if (f->value==top) { + f_tr = f->tr; f_fa = f->fa; + } else { + f_tr = f; f_fa = f; + } + if (!IS_TERMINAL(g) && g->value==top) { + g_tr = g->tr; g_fa = g->fa; + } else { + g_tr = g; g_fa = g; + } + if (!IS_TERMINAL(h) && h->value==top) { + h_tr = h->tr; h_fa = h->fa; + } else { + h_tr = h; h_fa = h; + } + + tr_part = ite_constant(f_tr, g_tr, h_tr); + fa_part = ite_constant(f_fa, g_fa, h_fa); + if (tr_part == fa_part) { + result = tr_part; + } else { + result = nonterminal; + } + + UPDATE_ITE_CACHE(f,g,h,result,ite_constant); + return result; + } +#endif /* USE_ITE_CONSTANT */ + + +DECLARE_FN_COUNT(implies) + +node *implies(node *a, node *b) + { + COUNT_FN(implies); + return ite(a,b,one); + } + + +node *copy(node *a) /* returns a copy of graph a */ + { + return a; + } + + +int equiv(node *a, node *b) /* returns true if graph a and b are equiv */ + { + return (a == b); + } + + +DECLARE_FN_COUNT(lub) +DECLARE_FN_COUNT(glb) + +#if defined(NAIVE) +node *glb(node *a, node *b) + { + COUNT_FN(glb); + return ite(a,b,zero); + } + + +node *lub(node *a, node *b) + { + COUNT_FN(lub); + return ite(a,one,b); + } + +#else /* !NAIVE */ + +node *lub(node *f, node *g) + { + COUNT_FN(lub); + if (IS_TERMINAL(f)) { + return f == one ? one : g; + } else if (IS_TERMINAL(g)) { + return g == one ? one : f; + } ELSE_TRY_EQUAL_TEST(f,g,f) + else { + node *result; + DECLARE_BIN_CACHE_ENTRY + + TRY_BIN_CACHE(f, g, lub); + + if (f->value < g->value) { + result = make_node(f->value, lub(f->tr, g), lub(f->fa, g)); + } else if (f->value > g->value) { + result = make_node(g->value, lub(f, g->tr), lub(f, g->fa)); + } else /* f->value == g->value */{ + result = make_node(f->value, + lub(f->tr, g->tr), + lub(f->fa, g->fa)); + } + UPDATE_BIN_CACHE(f, g, result, lub); + return result; + } + } + + +node *glb(node *f, node *g) + { + COUNT_FN(glb); + if (IS_TERMINAL(f)) { + return f == one ? g : zero; + } else if (IS_TERMINAL(g)) { + return g == one ? f : zero; + } ELSE_TRY_EQUAL_TEST(f,g,f) + else { + node *result; + DECLARE_BIN_CACHE_ENTRY + + TRY_BIN_CACHE(f, g, glb); + + if (f->value < g->value) { + result = make_node(f->value, glb(f->tr, g), glb(f->fa, g)); + } else if (f->value > g->value) { + result = make_node(g->value, glb(f, g->tr), glb(f, g->fa)); + } else /* f->value == g->value */{ + result = make_node(f->value, + glb(f->tr, g->tr), + glb(f->fa, g->fa)); + } + UPDATE_BIN_CACHE(f, g, result, glb); + return result; + } + } + +#endif /* NAIVE */ + + + +#if defined(NAIVE) +node *glb_array(int n, int arr[]) + { + int i; + node *result = one; + + for (i=0; i=0; --i) { + result = make_node(arr[i], result, zero); + } + return result; + } +#endif /* NAIVE */ + +/**************************************************************** + + Restriction (Projection, Existential Quantification) + + ****************************************************************/ + +DECLARE_FN_COUNT(restrict) + +/* restricts c in f. */ +node *restrict(int c, node *f) + { + COUNT_FN(restrict); + if (IS_TERMINAL(f) || (f->value > c)) { + return f; + } else if (f->value < c) { + return make_node(f->value, restrict(c,f->tr), restrict(c,f->fa)); + } else { + return lub(f->tr, f->fa); + } + } + + +DECLARE_FN_COUNT(restrictThresh) + +#if !defined(USE_THRESH) && !defined(RESTRICT_SET) +node *restrictThresh(int lo, int hi, node *a) + { + int i; + + COUNT_FN(restrictThresh); + for(i=lo+1; i<=hi; ++i) a = restrict(i, a); + return a; + } + +#elif !defined(USE_THRESH) /* && defined(RESTRICT_SET) */ + +/* union vars with the set of all variables greater than thresh appearing in + * the ROBDD rooted at f. + */ +static void vars_present(node *f, int thresh, bitset *vars) + { + while (!IS_TERMINAL(f)) { + if (f->value > thresh) { + BITSET_ADD_ELEMENT(*vars, f->value); + } + vars_present(f->tr, thresh, vars); + f = f->fa; + } + } + +node *restrictThresh(int thresh, node *f) + { + bitset vars; + int var; + int word; + bitmask mask; + + COUNT_FN(restrictThresh); + BITSET_CLEAR(vars); + vars_present(f, thresh, &vars); + REV_FOREACH_ELEMENT(vars, var, word, mask) { + f = restrict(var, f); + } + return f; + } +#else /* USE_THRESH */ +node *restrictThresh(int thresh, node *f) + { + /* restricts all variables greater than thresh. */ + + COUNT_FN(restrictThresh); + if (IS_TERMINAL(f)) { + return f; + } else if (f->value <= thresh) { + return make_node(f->value, + restrictThresh(thresh, f->tr), + restrictThresh(thresh, f->fa)); + } else { + return one; + } + } +#endif /* USE_THRESH */ + + +#if !defined(USE_THRESH) && !defined(RESTRICT_SET) +node *restricted_glb(int lo, int hi, node *f, node *g) + { + return restrictThresh(lo, hi, glb(f, g)); + } +#elif !defined(USE_RGLB) /* && ( USE_THRESH || RESTRICT_SET ) */ +node *restricted_glb(int thresh, node *f, node *g) + { + return restrictThresh(thresh, glb(f, g)); + } +#else /* USE_RGLB */ +/* returns true iff glb(f,g) is not 'zero' */ +static int exists_glb(node *f, node *g) + { + if (f == zero) { + return FALSE; + } else if (g == zero) { + return FALSE; + } else if (f == one) { + /* since we know that g != zero... */ + return TRUE; + } else if (g == one) { + /* likewise f... */ + return TRUE; + } else if (f->value < g->value) { + return exists_glb(f->tr, g) || exists_glb(f->fa, g); + } else if (f->value > g->value) { + return exists_glb(f, g->tr) || exists_glb(f, g->fa); + } else { + return exists_glb(f->tr, g->tr) || exists_glb(f->fa, g->fa); + } + } + + +node *restricted_glb(int c, node *f, node *g) + { + if (IS_TERMINAL(f)) { + return (f == one) ? restrictThresh(c, g) : zero; + } else if (IS_TERMINAL(g)) { + return (g == one) ? restrictThresh(c, f) : zero; + } ELSE_TRY_EQUAL_TEST(f,g,restrictThresh(c, f)) + else { + int v; + node *tr1, *tr2, *fa1, *fa2; + node *result; + + DECLARE_RGLB_CACHE_ENTRY + + TRY_RGLB_CACHE(f, g, c); + + if (f->value < g->value) { + v = f->value; + tr1 = f->tr; + tr2 = g; + fa1 = f->fa; + fa2 = g; + } else if (f->value > g->value) { + v = g->value; + tr1 = f; + tr2 = g->tr; + fa1 = f; + fa2 = g->fa; + } else /* f->value == g->value */{ + v = f->value; + tr1 = f->tr; + tr2 = g->tr; + fa1 = f->fa; + fa2 = g->fa; + } + if (v > c) { + result = + (exists_glb(tr1,tr2)||exists_glb(fa1,fa2)) ? one : zero; + } else { + result = make_node(v, + restricted_glb(c, tr1, tr2), + restricted_glb(c, fa1, fa2)); + } + UPDATE_RGLB_CACHE(f,g,c,result); + return result; + } + } +#endif /* USE_THRESH */ + + + +/**************************************************************** + + Renaming + + ****************************************************************/ + +DECLARE_FN_COUNT(renameArray) +DECLARE_FN_COUNT(reverseRenameArray) + +#if defined(NEW) + +DECLARE_FN_COUNT(ite_var) + +/* A special case version of ite_var, where we know that f < g->value */ +static node *ite_var_g(int f, node *g, node *h) + { + COUNT_FN(ite_var); + + assert(IS_TERMINAL(g) || f < g->value); + + if (IS_TERMINAL(h) || f < h->value) { + /* f < g && f < h */ + return make_node(f, g, h); + } else if (f == h->value) { + return make_node(f, g, h->fa); + } else { + /* h < f < g */ + node *result; + DECLARE_ITE_VAR_CACHE_ENTRY + + TRY_ITE_VAR_CACHE(f, g, h); + + result = make_node(h->value, + ite_var_g(f, g, h->tr), + ite_var_g(f, g, h->fa)); + UPDATE_ITE_VAR_CACHE(f, g, h, result); + return result; + } + } + + +/* A special case version of ite_var, where we know that f < h->value */ +static node *ite_var_h(int f, node *g, node *h) + { + COUNT_FN(ite_var); + + assert(IS_TERMINAL(h) || f < h->value); + + if (IS_TERMINAL(g) || f < g->value) { + /* f < g && f < h */ + return make_node(f, g, h); + } else if (f == g->value) { + return make_node(f, g->tr, h); + } else { + /* h < f < g */ + node *result; + DECLARE_ITE_VAR_CACHE_ENTRY + + TRY_ITE_VAR_CACHE(f, g, h); + result = make_node(g->value, + ite_var_h(f, g->tr, h), + ite_var_h(f, g->fa, h)); + UPDATE_ITE_VAR_CACHE(f, g, h, result); + return result; + } + } + + +/* A special case version of ite, where we know that !IS_TERMINAL(f) && + * f->tr == one && f->fa == zero. In fact, we refine this further and + * make f be just (what would have been) f->value. + * + * Recall the code for ite: it finds the minimum value of f, g, and h (call + * it top), and sets each of ft, gt and ht to the tr branch of the + * corresponding arg if its value == top, else sets it to the arg itself, and + * correspondingly for ff, gf, and hf. Then the value of ite is: + * + * mn(top, i(ft, gt, ht), i(ff, gf, hf)) + * + * (abbreviating make_node as mn and ite as i). Given this, we can simplify + * things in several cases. Here are all the cases, and the simplified value. + * (We introduce ig for ite_var_g and ih for ite_var_h as special cases where + * we know f < g or f < h, respectively.) + * + * a) f = g = h (1) mn(f, g->tr, h->fa) *** Impossible + * + * b) f < g < h (2) mn(f, g, h) + * c) f < g = h (2) mn(f, g, h) + * d) f < h < g (2) mn(f, g, h) + * e) f = g < h (3) mn(f, g->tr, h) *** Impossible + * f) f = h < g (4) mn(f, g, h->fa) *** Impossible + * + * g) g < f < h (5) mn(gv, ih(f, g->tr, h), ih(f, g->fa, h)) + * h) g < f = h (6) mn(gv, i(f, g->tr, h), i(f, g->fa, h)) *** Impossible + * i) g < h < f (6) mn(gv, i(f, g->tr, h), i(f, g->fa, h)) + * j) g = h < f (7) mn(gv, i(f, g->tr, h->tr), i(f, g->fa, h->fa)) + * + * k) h < f < g (8) mn(hv, ig(f, g, h->tr), ig(f, g, h->fa)) + * l) h < f = g (9) mn(hv, i(f, g, h->tr), i(f, g, h->fa)) *** Impossible + * m) h < g < f (9) mn(hv, i(f, g, h->tr), i(f, g, h->fa)) + */ + +node *ite_var(int f,node *g,node *h) + { + int g_val = MAXVAR; + int h_val = MAXVAR; + node *result; + DECLARE_ITE_VAR_CACHE_ENTRY + + COUNT_FN(ite_var); + DIRECT_EQUAL_TEST(g,h,g); + TRY_ITE_VAR_CACHE(f, g, h); + + if (!IS_TERMINAL(g)) g_val = g->value; + if (!IS_TERMINAL(h)) h_val = h->value; + + if (f < g_val) { + if (f < h_val) /* case 2 (b,c,d): f < g && f < h */ { + result = make_node(f, g, h); + } else /* case 8 (k): h < f < g */ { + result = make_node(h_val, + ite_var_g(f, g, h->tr), + ite_var_g(f, g, h->fa)); + } + /* g < f */ + } else if (f < h_val) /* g < f < h */ { + result = make_node(g_val, + ite_var_h(f, g->tr, h), + ite_var_h(f, g->fa, h)); + /* g < f && h < f */ + } else if (h_val < g_val) /* case 9 (l,m): h < g < f */ { + result = make_node(h_val, + ite_var(f, g, h->tr), + ite_var(f, g, h->fa)); + /* g < f && g <= h */ + } else if (g_val == h_val) /* g == h < f */ { + result = make_node(g_val, + ite_var(f, g->tr, h->tr), + ite_var(f, g->fa, h->fa)); + } else /* case 6 (h,i): g < h < f */ { + result = make_node(g_val, + ite_var(f, g->tr, h), + ite_var(f, g->fa, h)); + } + + UPDATE_ITE_VAR_CACHE(f, g, h, result); + return result; + } + +#else /* ! NEW */ +#define ite_var(v,f,g) ite(variableRep(v), f, g) +#endif /* !NEW */ + +node *renameArray(node *f, int count, int mapping[]) + { + int newval; + + COUNT_FN(renameArray); + if (IS_TERMINAL(f)) { + return f; + } else if (f->value > count) { + return one; + } else if (UNUSED_MAPPING==(newval=mapping[f->value])) { + return lub(renameArray(f->tr, count, mapping), + renameArray(f->fa, count, mapping)); + } else { + return ite_var(newval, + renameArray(f->tr, count, mapping), + renameArray(f->fa, count, mapping)); + } + } + +node *reverseRenameArray(node *f, int count, int mapping[]) + { + int i, val, max; + int rev_map[MAXVAR]; + + COUNT_FN(reverseRenameArray); + /* NB: four -1 bytes is the same as a -1 word */ + memset(rev_map, -1, sizeof(rev_map)); + for (i=1,max=-1; i<=count; ++i) { + rev_map[(val=mapping[i])] = i; + if (max < val) max = val; + } + + return renameArray(f, max, rev_map); + } + + + +/**************************************************************** + + Abstract Exit (renaming + conjunction + restriction) + + ****************************************************************/ + +#if !defined(USE_THRESH) && !defined(RESTRICT_SET) +node *abstract_exit(node *context, node *f, int count, int mapping[], + int lo, int hi) + { + return restricted_glb(lo, hi, context, renameArray(f, count, mapping)); + } +#elif 1 /* ( USE_THRESH || RESTRICT_SET ) */ +node *abstract_exit(node *context, node *f, int count, int mapping[], + int thresh) + { + return restricted_glb(thresh, context, renameArray(f, count, mapping)); + } +#else /* 0 (this code not used) */ + +/* returns FALSE iff the function f restricted so that all variables in trues + * are set to true and all in falses are set to false evaluates to zero. + */ +int exists_restrict_sets(node *f, bitset *trues, bitset *falses, int hielt) + { + for (;;) { + if (IS_TERMINAL(f)) { + return f == one; + } else if (f->value > hielt) { + return TRUE; + } else { + int word = BITSET_WORD(f->value); + bitmask mask = BITSET_MASK(f->value); + + if (BITSET_MEMBER(*trues,word,mask)) { + f = f->tr; /* continue loop */ + } else if (BITSET_MEMBER(*falses,word,mask)) { + f = f->fa; /* continue loop */ + } else if (exists_restrict_sets(f->tr, trues, falses, hielt)) { + return TRUE; + } else { + f = f->fa; + } + } + } + } + + +/* computes the function f restricted so that all variables in trues + * are set to true and all in falses are set to false. + */ +node *restrict_sets(node *f, bitset *trues, bitset *falses, int hielt, + int thresh) + { + for (;;) { + if (IS_TERMINAL(f)) { + return f; + } else if (f->value > hielt) { + return restrictThresh(thresh, f); + } else if (f->value > thresh) { + return + exists_restrict_sets(f, trues, falses, hielt) ? one : zero; + } else { + int word = BITSET_WORD(f->value); + bitmask mask = BITSET_MASK(f->value); + + if (BITSET_MEMBER(*trues,word,mask)) { + f = f->tr; /* continue loop */ + } else if (BITSET_MEMBER(*falses,word,mask)) { + f = f->fa; /* continue loop */ + } else { + return make_node(f->value, + restrict_sets(f->tr, trues, falses, hielt, + thresh), + restrict_sets(f->fa, trues, falses, hielt, + thresh)); + } + } + } + } + + +/* if f->value > thresh, returns one, else if f->value is in either + * trues (or falses), this returns + * follow_path(f->tr (or fa), trues, falses} + * else it returns f. + */ +node *follow_path(node *f, bitset *trues, bitset *falses) + { + + while (!IS_TERMINAL(f)) { + int word = BITSET_WORD(f->value); + bitmask mask = BITSET_MASK(f->value); + + if (BITSET_MEMBER(*trues,word,mask)) { + f = f->tr; + } else if (BITSET_MEMBER(*falses,word,mask)) { + f = f->fa; + } else { + break; + } + } + return f; + } + + +/* This function computes + * + * restrictThresh(renameArray(f, count, mapping), thresh) + * + */ +node *restricted_rename(node *f, int count, int mapping[], int thresh) + { + if (IS_TERMINAL(f)) { + return f; + } else { + int newval = mapping[f->value]; + node *tr, *fa; + + tr = restricted_rename(f->tr, count, mapping, thresh); + fa = restricted_rename(f->fa, count, mapping, thresh); + + if (newval > thresh) { + return lub(tr, fa); + } else { + return ite_var(newval, tr, fa); + } + } + } + + + +/* This function computes + * + * restrictThresh(glb(context1, renameArray(f, count, mapping)), thresh) + * + * where context1 is context restricted by the settings in trues and + * falses. We know that !IS_TERMINAL(context). + */ +node *abexit(node *context, node *f, int count, int mapping[], int thresh, + bitset *trues, bitset *falses, int hielt) + { + if (IS_TERMINAL(f)) { + if (f==one) { + return restrict_sets(context, trues, falses, hielt, thresh); + } else { + return f; + } + } else { + int newval = mapping[f->value]; + node *tr, *fa; + + if (newval == context->value) { + tr = follow_path(context->tr, trues, falses); + fa = follow_path(context->fa, trues, falses); + + if (tr == one) { + tr = restricted_rename(f->tr, count, mapping, thresh); + } else if (tr != zero) { + tr = abexit(tr, f->tr, count, mapping, thresh, + trues, falses, hielt); + } + if (fa == one) { + fa = restricted_rename(f->fa, count, mapping, thresh); + } else if (fa != zero) { + fa = abexit(fa, f->fa, count, mapping, thresh, + trues, falses, hielt); + } + } else { + int word = BITSET_WORD(newval); + bitmask mask = BITSET_MASK(newval); + int newhi = (newval>hielt ? newval : hielt); + + BITSET_ADD(*trues,word,mask); /* turn on true bit */ + tr = abexit(context, f->tr, count, mapping, thresh, + trues, falses, newhi); + BITSET_TOGGLE(*trues,word,mask); /* turn off true bit */ + BITSET_ADD(*falses,word,mask); /* turn on false bit */ + fa = abexit(context, f->fa, count, mapping, thresh, + trues, falses, newhi); + BITSET_TOGGLE(*falses,word,mask); /* turn off false bit */ + } + if (newval > thresh) { + return lub(tr, fa); + } else { + return ite_var(newval, tr, fa); + } + } + } + + +node *abstract_exit(node *context, node *f, int count, int mapping[], + int thresh) + { + bitset trues; + bitset falses; + + if (context == zero) return zero; + if (context == one) return restricted_rename(f, count, mapping, thresh); + + BITSET_CLEAR(trues); + BITSET_CLEAR(falses); + + return abexit(context, f, count, mapping, thresh, &trues, &falses, -1); +} +#endif /* 0 (end of unused code) */ + + +/**************************************************************** + + Abstract Unification + + ****************************************************************/ + +/* NB: iff_conj_array, and so all the functions that call it, now + * allow v0 to apear in the array of variables arr[]. This makes the + * analyzer robust for handling goals like X = f(X,Y). Since it's + * cheaper and easier to check this in C, I do it here. + */ + +#if defined(ELIM_DUPS) +#define DECLARE_PREV(init) int prev = (init); +#define HANDLE_DUP(this,rel) \ + if ((this) == prev) continue; \ + assert((this) rel prev); \ + prev = (this); +#elif !defined(NDEBUG) +#define DECLARE_PREV(init) int prev = (init); +#define HANDLE_DUP(this,rel) \ + assert((this) != prev); \ + assert((this) rel prev); \ + prev = (this); +#else +#define DECLARE_PREV(init) +#define HANDLE_DUP(this,rel) +#endif + + +DECLARE_FN_COUNT(iff_conj) + +#if defined(NAIVE) +node *iff_conj_array(int v0, int n, int arr[]) + { + node *conj = one; + node *v_rep = variableRep(v0); + int i; + DECLARE_PREV(-1) + + COUNT_FN(iff_conj); + /* We construct the conjunction from the lowest var up to the highest. + * This is a quadratic process, while the other way is linear. + */ + for (i=0; i) + if (arr[i] != v0) conj = glb(conj, variableRep(arr[i])); + } + return glb(implies(conj,v_rep), implies(v_rep,conj)); + } + +#elif !defined(USE_THRESH) + +node *iff_conj_array(int v0, int n, int arr[]) + { + node *conj = one; + node *pos_v = variableRep(v0); + node *neg_v = ite(pos_v, zero, one); + int *ptr; + DECLARE_PREV(MAXVAR) + + COUNT_FN(iff_conj); + /* Note that to be efficient, we construct the conjunction + * from the highest var down to the lowest. This is a linear + * process, while the other way is n squared. + */ + for (ptr=&arr[n-1]; ptr>=arr; --ptr) { + int vi = *ptr; + HANDLE_DUP(vi, <) + if (vi != v0) conj = glb(conj, variableRep(vi)); + } + return ite(conj, pos_v, neg_v); + } + +#else /* USE_THRESH */ + +node *iff_conj_array(int v0, int n, int arr[]) + { + node *thens = one, *elses = zero; + int *ptr; + int vi = 0; /* this value doesn't matter */ + DECLARE_PREV(MAXVAR) + + COUNT_FN(iff_conj); + /* first build part of graph below v0. For this, we build two + * subgraphs: one for when v0 is true, and one for false. + * These are called thens and elses. + */ + + for (ptr=&arr[n-1]; ptr>=arr && v0<(vi=*ptr); --ptr) { + HANDLE_DUP(vi, <) + thens = make_node(vi, thens, zero); + elses = make_node(vi, elses, one); + } + + if (v0 == vi) --ptr; + + /* make v0 node */ + thens = make_node(v0,thens,elses); + + /* Finally build part of graph above v0. For this, we build + * only one graph, whose then branch is the graph we've built + * so far and whose else branch is ~v0. + */ + + if (ptr >= arr) { + DECLARE_PREV(MAXVAR) + /* make ~v0 */ + elses = make_node(v0,zero,one); + + do { + vi = *ptr; + HANDLE_DUP(vi, <) + thens = make_node(vi, thens, elses); + } while (--ptr >= arr); + } + + return thens; + } +#endif /* OLD */ + + +node *restricted_iff_conj_array(int v0, int n, int arr[], int thresh) + { + if (v0 > thresh) return one; + while (--n>=0 && arr[n]>thresh); + return iff_conj_array(v0, n+1, arr); + } + + + +#if !defined(USE_THRESH) && !defined(RESTRICT_SET) +node *abstract_unify(node *f, int v0, int n, int arr[], int lo, int hi) + { + return restricted_glb(lo, hi, f, iff_conj_array(v0, n, arr)); + } +#elif 1 /* ( USE_THRESH || RESTRICT_SET ) */ +node *abstract_unify(node *f, int v0, int n, int arr[], int thresh) + { + return restricted_glb(thresh, f, iff_conj_array(v0, n, arr)); + } +#else /* !1 (this code is unused) */ + + +static node *build_and(int n, int arr[], node *tr, node *fa) + { + if (n<=0) { + return tr; + } else { + return make_node(arr[0], + build_and(n-1, &arr[1], tr, fa), + fa); + } + } + + +static node *glb_and(node *f, int n, int arr[]) + { + if (f == zero) { + return zero; + } else if (f == one) { + return build_and(n, arr, one, zero); + } else if (n == 0) { + return f; + } else { + node *result; + if (f->value < arr[0]) { + result = make_node(f->value, + glb_and(f->tr, n, arr), + glb_and(f->fa, n, arr)); + } else if (f->value > arr[0]) { + result = make_node(arr[0], + glb_and(f, n-1, &arr[1]), + zero); + } else /* f->value == arr[0] */{ + result = make_node(f->value, + glb_and(f->tr, n-1, &arr[1]), + zero); + } + return result; + } + } + + +static node *glb_nand(node *f, int n, int arr[]) + { + if (f == zero) { + return zero; + } else if (f == one) { + return build_and(n, arr, zero, one); + } else if (n == 0) { + return zero; + } else { + node *result; + if (f->value < arr[0]) { + result = make_node(f->value, + glb_nand(f->tr, n, arr), + glb_nand(f->fa, n, arr)); + } else if (f->value > arr[0]) { + result = make_node(arr[0], + glb_nand(f, n-1, &arr[1]), + f); + } else /* f->value == arr[0] */{ + result = make_node(f->value, + glb_nand(f->tr, n-1, &arr[1]), + f); + } + return result; + } + } + + +/* returns zero != glb(f, build_and(n, arr, one, zero)) */ +static int exists_glb_and(node *f, int n, int arr[]) + { + if (f == zero) { + return FALSE; + } else if (f == one || n == 0) { + return TRUE; + } else if (f->value < arr[0]) { + return (exists_glb_and(f->tr, n, arr) || + exists_glb_and(f->fa, n, arr)); + } else { + if (f->value == arr[0]) { + f = f->tr; + } + return exists_glb_and(f, n-1, arr+1); + } + } + + +/* returns zero != glb(f, build_and(n, arr, zero, one)) */ +static int exists_glb_nand(node *f, int n, int arr[]) + { + if (f == zero || n == 0) { + return FALSE; + } else if (f == one || f->value > arr[0]) { + /* if f->value > arr[0], then the else branch of the node we'd + * build would be one, so we know the graph couldn't == zero. + */ + return TRUE; + } else if (f->value < arr[0]) { + return glb_nand(f->tr, n, arr) || glb_nand(f->fa, n, arr); + } else if (f->fa != zero) /* && f->value == arr[0] */ { + /* if f->fa isn't zero, then conjoined with one it won't be zero, + * so the node we'd build won't == zero. + */ + return TRUE; + } else /* f->value == arr[0] && f->fa == zero */ { + return exists_glb_nand(f->tr, n-1, arr+1); + } + } + + +/* returns zero != glb(f, iff_conj_array(v0, n, arr)) */ +static int exists_glb_iffconj(node *f, int v0, int n, int arr[]) + { + if (f == zero) { + return FALSE; + } else if (f == one) { + return TRUE; + } else { + int v = (n>0 && arr[0]value < v) { + return (exists_glb_iffconj(f->tr, v0, n, arr) || + exists_glb_iffconj(f->fa, v0, n, arr)); + } else /* f->value >= v */ { + node *tr, *fa; + + if (f->value == v) { + tr = f->tr; fa = f->fa; + } else /* f->value > v */ { + tr = f; fa = f; + } + + if (v == v0) { + return (exists_glb_nand(fa, n, arr) || + exists_glb_and(tr, n, arr)); + } else { + return (!var_entailed(fa, v0) || + exists_glb_iffconj(tr, v0, n-1, &arr[1])); + } + } + } + } + + + +/* returns restricted_glb(f, build_and(n, arr, one, zero), thresh) */ +static node *rglb_and(node *f, int n, int arr[], int thresh) + { + if (f == zero) { + return zero; + } else if (f == one) { + while (--n>=0 && arr[n]>thresh); + return build_and(n+1, arr, one, zero); + } else if (n == 0) { + return restrictThresh(thresh, f); + } else { + if (f->value < arr[0]) { + if (f->value > thresh) { + return + (exists_glb_and(f->tr, n, arr) || + exists_glb_and(f->fa, n, arr)) ? one : zero; + } else { + return make_node(f->value, + rglb_and(f->tr, n, arr, thresh), + rglb_and(f->fa, n, arr, thresh)); + } + } else /* arr[0] <= f->value */ { + int v = arr[0]; + + if (v == f->value) { + f = f->tr; + } + if (v > thresh) { + return exists_glb_and(f, n-1, arr+1) ? one : zero; + } else { + return make_node(v, + rglb_and(f, n-1, arr+1, thresh), + zero); + } + } + } + } + + +/* returns restricted_glb(f, build_and(n, arr, zero, one), thresh) */ +static node *rglb_nand(node *f, int n, int arr[], int thresh) + { + if (f == zero || n == 0) { + return zero; + } else if (f == one) { + /* just restrictThresh(thresh, build_and(n, arr, zero, one)). + * Note that if anything is restricted away, then the whole graph + * degenerates to one. So... + */ + if (arr[n-1]>thresh) { + return one; + } else { + return build_and(n, arr, zero, one); + } + } else { + if (f->value < arr[0]) { + if (f->value > thresh) { + return (exists_glb_nand(f->tr, n, arr)|| + exists_glb_nand(f->fa, n, arr)) ? one : zero; + } else { + return make_node(f->value, + rglb_nand(f->tr, n, arr, thresh), + rglb_nand(f->fa, n, arr, thresh)); + } + } else if (f->value > arr[0]) { + if (arr[0] > thresh) { + /* because f != zero, restricting all vars yields one */ + return one; + } else { + return make_node(arr[0], + rglb_nand(f, n-1, arr+1, thresh), + restrictThresh(thresh, f)); + } + } else /* f->value == arr[0] */{ + if (arr[0] > thresh) { + return (f->fa != zero || + exists_glb_nand(f->tr, n-1, arr+1)) ? one : zero; + } else { + return make_node(arr[0], + rglb_nand(f->tr, n-1, arr+1, thresh), + restrictThresh(thresh, f->fa)); + } + } + } + } + + +/* returns restricted_glb(thresh, f, make_node(v, zero, one)) */ +static node *rglb_notvar(node *f, int v, int thresh) + { + if (f == zero) { + return zero; + } else if (f == one) { + if (v > thresh) return one; + return make_node(v, zero, one); + } else { + if (f->value < v) { + if (f->value > thresh) { + return + (!var_entailed(f->tr, v) || + !var_entailed(f->fa, v)) ? one : zero; + } else { + return make_node(f->value, + rglb_notvar(f->tr, v, thresh), + rglb_notvar(f->fa, v, thresh)); + } + } else { + if (f->value == v) { + f = f->fa; + } + if (v > thresh) { + return f==zero ? zero : one; + } else { + return make_node(v, zero, restrictThresh(thresh, f)); + } + } + } + } + + + +node *abstract_unify(node *f, int v0, int n, int arr[], int thresh) + { + if (f == zero) { + return zero; + } else if (f == one) { + return restricted_iff_conj_array(v0, n, arr, thresh); + } else { + int v = (n>0 && arr[0]value < v) { + if (f->value > thresh) { + result = + (exists_glb_iffconj(f->tr, v0, n, arr) || + exists_glb_iffconj(f->fa, v0, n, arr)) ? one : zero; + } else { + result = + make_node(f->value, + abstract_unify(f->tr, v0, n, arr, thresh), + abstract_unify(f->fa, v0, n, arr, thresh)); + } + } else /* f->value >= v */ { + node *tr = f, *fa = f; + + if (f->value == v) { + tr = f->tr; fa = f->fa; + } + if (v > thresh) { + int value; + + if (v == v0) { + value = (exists_glb_nand(fa, n, arr) || + exists_glb_and(tr, n, arr)); + } else { + value = + (!var_entailed(fa, v0) || + exists_glb_iffconj(tr, v0, n-1, &arr[1])); + } + result = value ? one : zero; + } else { + if (v == v0) { + tr = rglb_and(tr, n, arr, thresh); + fa = rglb_nand(fa, n, arr, thresh); + } else { + tr = abstract_unify(tr, v0, n-1, arr+1, thresh); + fa = rglb_notvar(fa, v0, thresh); + } + result = make_node(v, tr, fa); + } + } + return result; + } + } + +#endif /* (end of unused code) */ + + + +/**************************************************************** + + Finding Entailed Variables + + ****************************************************************/ + +/* returns TRUE iff var is implied by the boolean function specified by f */ +int var_entailed(node *f, int var) + { +#if defined(NAIVE) + return f == glb(f, variableRep(var)); +#elif !defined(USE_THRESH) && !defined(USE_ITE_CONSTANT) + return one == implies(f, variableRep(var)); +#elif !defined(USE_RGLB) + return one == ite_constant(f, variableRep(var), one); +#else /* USE_RGLB */ + if (IS_TERMINAL(f)) { + return f==zero; + } else { + DECLARE_VAR_ENTAILED_CACHE_ENTRY + int result; + + TRY_VAR_ENTAILED_CACHE(f, var); + if (f->value < var) { + result = var_entailed(f->tr, var) + && var_entailed(f->fa, var); + } else if (f->value == var) { + result = (f->fa==zero); + } else /* f->value > var */ { + result = FALSE; + } + UPDATE_VAR_ENTAILED_CACHE(f, var, result); + return result; + } +#endif /* NEW */ + } + + +/* returns a bitset of all the variables implied by f. A variable i + * is implied by f iff + * + * BITSET_IS_MEMBER(*result, i) + */ + +#if !defined(NEW) +bitset *vars_entailed(node *f, int topvar) + { + static bitset def_vars; + int i; + + BITSET_CLEAR(def_vars); + + for (i=0; itr, f->value); + if (n1 > n) n = n1; + return topvar(f->fa, n); + } + +bitset *vars_entailed(node *f) + { + static bitset def_vars; + int i = topvar(f, 0); + + BITSET_CLEAR(def_vars); + + for (; i >= 0; --i) { + if (var_entailed(f, i)) BITSET_ADD_ELEMENT(def_vars,i); + } + return &def_vars; + } +#else /* NEW */ +/* According to Roberto Bagnara's benchmarking, this version is slower + * than the simpler version below. + */ +#if defined(OLD_VARS_ENTAILED) + +/* these variables should be local to both vars_entailed and + * vars_entailed_aux, but that isn't possible in C, so I have to make + * them global. They should not be use by any other functions. + */ +static bitset this_path; +static bitset entailed; + +void vars_entailed_aux(node *f) + { + while (!IS_TERMINAL(f)) { + int word = BITSET_WORD(f->value); + bitmask mask = BITSET_MASK(f->value); + + /* turn on bit for then branch */ + BITSET_ADD(this_path,word,mask); + vars_entailed_aux(f->tr); + /* turn it off for the else branch */ + BITSET_TOGGLE(this_path,word,mask); + f = f->fa; + } + /* needn't do anything for false terminals */ + if (f == one) { + BITSET_INTERSECTION(entailed, entailed, this_path); + } + } + + +/* returns a bitset of all the variables implied by f. A variable i + * is implied by f iff + * + * BITSET_IS_MEMBER(*result, i) + */ +bitset *vars_entailed(node *f) + { + + BITSET_CLEAR(this_path); + BITSET_UNIVERSE(entailed); + + vars_entailed_aux(f); + return &entailed; + } +#else /* NEW && !OLD_VARS_ENTAILED */ +/* returns a bitset of all the variables implied by f. A variable i + * is implied by f iff + * + * BITSET_IS_MEMBER(*result, i) + */ + +bitset *vars_entailed(node *f) + { + static bitset tmp_bitset; + DECLARE_UNARY_BITSET_CACHE_ENTRY + + if (f == zero) { + BITSET_UNIVERSE(tmp_bitset); + } else if (f == one) { + BITSET_CLEAR(tmp_bitset); + } else { + bitset bs; + + TRY_UNARY_BITSET_CACHE(f, vars_entailed); + tmp_bitset = *vars_entailed(f->tr); + bs = *vars_entailed(f->fa); + BITSET_INTERSECTION(tmp_bitset, tmp_bitset, bs); + if (f->fa == zero) BITSET_ADD_ELEMENT(tmp_bitset, f->value); + UPDATE_UNARY_BITSET_CACHE(f, tmp_bitset, vars_entailed); + } + return &tmp_bitset; + } +#endif /* NEW && !OLD_VARS_ENTAILED */ +#endif /* NEW */ + + + +/**************************************************************** + + Set Sharing Operations + + ****************************************************************/ +#if defined(SHARING) + +/* returns the Boolean function + * ~1&~2&...~n | 1&~2&...~n | ~1&2&...~n | ~1&~2&...n + */ +node *init_set_sharing(int n) + { + node *result = one; + node *other = one; + + while (n>1) { + other = make_node(n, zero, other); + result = make_node(--n, other, result); + } + + return result; + } + + +#if defined(NEW) + +DECLARE_FN_COUNT(complete_one_or) + +/* the same as lub(complete_one(f), prev) */ +node *complete_one_or(node *f, node *prev) + { + node *result; + node *complete_one(node *f); + DECLARE_ASYM_BIN_CACHE_ENTRY + + COUNT_FN(complete_one_or); + + if (IS_TERMINAL(prev)) return (prev==one) ? one : complete_one(f); + if (IS_TERMINAL(f)) return (f==one) ? one : prev; + + TRY_ASYM_BIN_CACHE(f, prev, complete_one_or); + + /* we want to return: + * lub(make_node(f->value, lub(complete_one(f->tr), + * complete_one(f->fa)), + * complete_one(f->fa)), + * prev); + * but we want to unfold the outer lub call, so we compare + * prev->value and f->value. Actually, this isn't right when + * f->value <= prev->value, because the make_node call may return + * a node whose label is > prev->value, but in that case, + * lub(that, prev) = make_node(prev->value, lub(that, prev->tr), + * lub(that, prev->fa)) + */ + + if (f->value < prev->value) { + node *cfa = complete_one_or(f->fa, prev); + result = make_node(f->value, complete_one_or(f->tr, cfa), cfa); + } else if (f->value == prev->value) { + result = make_node(f->value, + complete_one_or(f->tr, + complete_one_or(f->fa, + prev->tr)), + complete_one_or(f->fa, prev->fa)); + } else { + result = make_node(prev->value, + complete_one_or(f, prev->tr), + complete_one_or(f, prev->fa)); + } + UPDATE_ASYM_BIN_CACHE(f, prev, result, complete_one_or); + return result; + } + + +DECLARE_FN_COUNT(complete_one) + +node *complete_one(node *f) + { + node *result, *cfa; + DECLARE_UNARY_CACHE_ENTRY + + COUNT_FN(complete_one); + + if (IS_TERMINAL(f)) return f; + TRY_UNARY_CACHE(f, complete_one); + cfa = complete_one(f->fa); + result = make_node(f->value, complete_one_or(f->tr, cfa), cfa); + UPDATE_UNARY_CACHE(f, result, complete_one); + return result; + } + + +DECLARE_FN_COUNT(complete_or) + +/* the same as lub(complete(f, g), prev) */ +node *complete_or(node *f, node *g, node *prev) + { + node *result; + node *lo, *hi; + DECLARE_COMPLETE_OR_CACHE_ENTRY + + COUNT_FN(complete_or); + + if (prev == one) return one; + if (f == g) return lub(f, prev); + if (f == zero || g == zero) return prev; + + if (f == one) return complete_one_or(g, prev); + if (g == one) return complete_one_or(f, prev); + if (prev == zero) return complete(f, g); + + TRY_COMPLETE_OR_CACHE(f, g, prev); + + if (f->value > g->value) lo=g, hi=f; else lo=f, hi=g; + + if (prev->value < lo->value) { + result = make_node(prev->value, + complete_or(lo, hi, prev->tr), + complete_or(lo, hi, prev->fa)); + } else if (prev->value == lo->value) { + if (lo->value == hi->value) { + node *n = complete_or(lo->tr, hi->tr, prev->tr); + n = complete_or(lo->tr, hi->fa, n); + n = complete_or(lo->fa, hi->tr, n); + result = make_node(lo->value, n, + complete_or(lo->fa, hi->fa, prev->fa)); + } else { + node *n = complete_or(lo->fa, hi, prev->tr); + n = complete_or(lo->tr, hi, n); + result = make_node(lo->value, n, + complete_or(lo->fa, hi, prev->fa)); + } + } else if (lo->value == hi->value) { + node *n = complete_or(lo->tr, hi->tr, prev); + n = complete_or(lo->tr, hi->fa, n); + n = complete_or(lo->fa, hi->tr, n); + result = make_node(lo->value, n, + complete_or(lo->fa, hi->fa, prev)); + } else { + node *n = complete_or(lo->fa, hi, prev); + result = make_node(lo->value, complete_or(lo->tr, hi, n), n); + } + UPDATE_COMPLETE_OR_CACHE(f, g, prev, result); + + return result; + } +#else /* !NEW */ +#define complete_or(x, y, z) lub(complete((x),(y)),(z)) +#endif + +DECLARE_FN_COUNT(complete) + +node *complete(node *f, node *g) + { + node *result; + int fvar, gvar; + DECLARE_BIN_CACHE_ENTRY + + COUNT_FN(complete); + + if (f == g) return f; + if (f == zero || g == zero) return zero; + + TRY_BIN_CACHE(f, g, complete); + + fvar = (f == one) ? MAXVAR : f->value; + gvar = (g == one) ? MAXVAR : g->value; + if (fvar == gvar) { + result = make_node(fvar, + complete_or(f->fa, g->tr, + complete_or(f->tr, g->tr, + complete(f->tr,g->fa))), + complete(f->fa,g->fa)); + } else if (fvar < gvar) { + node *cfa = complete(f->fa, g); + + result = make_node(fvar, complete_or(f->tr, g, cfa), cfa); + } else /* fvar > gvar */ { + node *cfa = complete(f, g->fa); + + result = make_node(gvar, complete_or(f, g->tr, cfa), cfa); + } + UPDATE_BIN_CACHE(f, g, result, complete); + return result; + } + +DECLARE_FN_COUNT(upclose) + +node *upclose(node *f) + { + node *utr, *ufa, *result; + DECLARE_UNARY_CACHE_ENTRY + + COUNT_FN(upclose); + + if (IS_TERMINAL(f)) return f; + TRY_UNARY_CACHE(f, upclose); + utr = upclose(f->tr); + ufa = upclose(f->fa); + result = make_node(f->value, complete_or(utr, ufa, utr), ufa); + UPDATE_UNARY_CACHE(f, result, upclose); + return result; + } + +/* + * bin(f, g) + * + * We note that the set of Boolean functions of n variables is + * isomorphic to the powerset of the set of n variables. Thus we can + * use a Boolean function to represent a subset of the powerset. We + * choose to let the *absence* of a variable from the set be indicated + * by that variable being true in the boolean function. + * + * This function computes the set of all possible unions of sets from + * f and g. + */ + +node *bin(node *f, node *g) + { + if (f == zero || g == zero) { + return zero; + } else if (f == one) { + return bin_univ(g); + } else if (g == one) { + return bin_univ(f); + } else { + node *result; + DECLARE_BIN_CACHE_ENTRY + + TRY_BIN_CACHE(f, g, bin); + + if (f->value == g->value) { + node *th = bin(f->tr, g->tr); + node *el = bin(f->tr, g->fa); + + if (el != one) { + el = lub(el, bin(f->fa, g->tr)); + if (el != one) { + el = lub(el, bin(f->fa, g->fa)); + } + } + result = make_node(f->value, th, el); + } else { + node *tmp; + + if (f->value > g->value) { tmp = f; f = g; g = tmp; } + /* now f->value < g->value */ + tmp = bin(f->tr, g); + if (tmp == one) return one; + result = make_node(f->value, tmp, lub(tmp, bin(f->fa, g))); + } + UPDATE_BIN_CACHE(f, g, result, bin); + return result; + } + } + + +/* Auxilliary function for bin: special case code for bin(f, one). */ +node *bin_univ(node *f) + { + node *g; + + if (IS_TERMINAL(f)) return f; + g = bin_univ(f->tr); + if (g == one) return one; + return make_node(f->value, g, lub(g, bin_univ(f->fa))); + } + +#endif /* SHARING */ + +/**************************************************************** + + Initialization and Cleanup + + ****************************************************************/ + + +#if defined(STATISTICS) +void print_distribution(int array[], int max) + { + int count; + int sum; + int total, zero_count; + + for (count=0, total=0; count<=max; ++count) { total += array[count]; } + zero_count = array[0]; + for (count=0, sum=0; count<=max; ++count) { + if (array[count] > 0) { + sum += array[count]; + printf("%5d nodes:%6d %5.2f%% (cum = %6d %5.1f%%, >0 = %6d %5.1f%%)\n", + count, array[count], PERCENTAGE(array[count],total), + sum, PERCENTAGE(sum,total), sum-zero_count, + total==zero_count ? 999.999 + : PERCENTAGE(sum-zero_count, total-zero_count)); + } + } + if (array[max+1] > 0) { + printf(">%4d nodes:%6d %2.2f%%\n", + max, array[max], PERCENTAGE(array[max],total)); + } + printf("\n"); + } +#endif /* STATISTICS */ + +void initRep(void) + { + INIT_FN_COUNT(make_node); + INIT_FN_COUNT(variableRep); + INIT_FN_COUNT(implies); + INIT_FN_COUNT(lub); + INIT_FN_COUNT(glb); + INIT_FN_COUNT(restrict); + INIT_FN_COUNT(restrictThresh); + INIT_FN_COUNT(renameArray); + INIT_FN_COUNT(reverseRenameArray); + INIT_FN_COUNT(ite); +#if defined(USE_ITE_CONSTANT) + INIT_FN_COUNT(ite_constant); +#endif /* USE_ITE_CONSTANT */ + INIT_FN_COUNT(iff_conj); +#if defined(NEW) + INIT_FN_COUNT(ite_var); + INIT_FN_COUNT(vars_entailed); +#endif +#if defined(SHARING) +#if defined(NEW) + INIT_FN_COUNT(complete_one_or); + INIT_FN_COUNT(complete_one); + INIT_FN_COUNT(complete_or); +#endif /* NEW */ + INIT_FN_COUNT(complete); + INIT_FN_COUNT(upclose); +#endif /* SHARING */ + /* This code clears the unique table and all the computed + * caches. This should make it possible to time repeated + * execution of computations without the effect that after the + * first time the appropriate cache will probably hold the + * right result, so after the first time through the timing is + * useless. Even if this isn't the case, after the first time + * performing a computation no new nodes will ever be created + * because they will already exist in the unique table. + * + * After this, all old pointers to ROBDDs *must* be forgotten, + * because we free all allocated nodes, thus giving us a fresh + * start. + */ + + INIT_UNIQUE_TABLE; + + INIT_CACHE(ite); +#if defined(USE_ITE_CONSTANT) + INIT_CACHE(ite_constant); +#endif /* USE_ITE_CONSTANT */ +#if defined(SHARING) + INIT_CACHE(upclose); + INIT_CACHE(complete); +#if defined(NEW) + INIT_CACHE(complete_one); + INIT_CACHE(complete_or); + INIT_CACHE(complete_one_or); +#endif /* NEW */ + INIT_CACHE(bin); +#endif /* SHARING */ + INIT_CACHE(glb); + INIT_CACHE(lub); +#if defined(USE_RGLB) + INIT_CACHE(rglb); +#endif /* USE_RGLB */ +#if defined(NEW) + INIT_CACHE(ite_var); + INIT_CACHE(vars_entailed); +#endif /* NEW */ + } + + +void concludeRep(void) + { +#if defined(STATISTICS) + node *ptr; + int size_count[MAX_COUNT+2]; + int i, count; + + printf("\n\n\n================ Operation Counts ================\n\n"); + PRINT_FN_COUNT(make_node); + PRINT_FN_COUNT(variableRep); + PRINT_FN_COUNT(implies); + PRINT_FN_COUNT(lub); + PRINT_FN_COUNT(glb); + PRINT_FN_COUNT(restrict); + PRINT_FN_COUNT(restrictThresh); + PRINT_FN_COUNT(renameArray); + PRINT_FN_COUNT(reverseRenameArray); + PRINT_FN_COUNT(ite); +#if defined(USE_ITE_CONSTANT) + PRINT_FN_COUNT(ite_constant); +#endif /* USE_ITE_CONSTANT */ + PRINT_FN_COUNT(iff_conj); +#if defined(NEW) + PRINT_FN_COUNT(ite_var); + PRINT_FN_COUNT(vars_entailed); +#endif +#if defined(SHARING) +#if defined(NEW) + PRINT_FN_COUNT(complete_one_or); + PRINT_FN_COUNT(complete_one); + PRINT_FN_COUNT(complete_or); +#endif /* NEW */ + PRINT_FN_COUNT(complete); + PRINT_FN_COUNT(upclose); +#endif /* SHARING */ + printf("\n================ Cache Performance ================\n\n"); + printf("%d nodes extant\n\n", nodes_in_use()); + printf("Unique table: %d hits, %d misses, %f%% hits\n", + unique_table_hits, unique_table_misses, + PERCENTAGE(unique_table_hits, + unique_table_hits+unique_table_misses)); + memset(size_count, 0, sizeof(size_count)); + for (i=0; iunique,++count); + ++size_count[(count<=MAX_COUNT ? count : MAX_COUNT+1)]; + } + print_distribution(size_count, MAX_COUNT); + + PRINT_CACHE_PERFORMANCE(ite); +#if defined(USE_ITE_CONSTANT) + PRINT_CACHE_PERFORMANCE(ite_constant); +#endif /* USE_ITE_CONSTANT */ + PRINT_CACHE_PERFORMANCE(lub); + PRINT_CACHE_PERFORMANCE(glb); +#if defined(SHARING) + PRINT_CACHE_PERFORMANCE(upclose); + PRINT_CACHE_PERFORMANCE(complete); +#if defined(NEW) + PRINT_CACHE_PERFORMANCE(complete_or); + PRINT_CACHE_PERFORMANCE(complete_one_or); + PRINT_CACHE_PERFORMANCE(complete_one); +#endif /* NEW */ +#endif /* SHARING */ +#if defined(USE_RGLB) + PRINT_CACHE_PERFORMANCE(rglb); +#endif /* USE_RGLB */ +#if defined(NEW) + PRINT_CACHE_PERFORMANCE(ite_var); + PRINT_CACHE_PERFORMANCE(vars_entailed); +#endif /* NEW */ +#endif /* STATISTICS */ + } + + + +/**************************************************************** + + Testing Support + + ****************************************************************/ + +/* special version of iff_conj_array() that is the fast version no matter + * which options are selected. I hope this gives more reliable test times. + */ + +node *testing_iff_conj_array(int v0, int n, int arr[]) + { + node *thens = one, *elses = zero; + int *ptr; + int vi; + + /* first build part of graph below v0. For this, we build two + * subgraphs: one for when v0 is true, and one for false. + * These are called thens and elses. + */ + + for (ptr=&arr[n-1]; ptr>=arr && v0<(vi=*ptr); --ptr) { + thens = make_node(vi, thens, zero); + elses = make_node(vi, elses, one); + } + + /* make v0 node */ + thens = make_node(v0,thens,elses); + + /* Finally build part of graph above v0. For this, we build + * only one graph, whose then branch is the graph we've built + * so far and whose else branch is ~v0. + */ + + if (ptr >= arr) { + /* make ~v0 */ + elses = make_node(v0,zero,one); + + do { + vi = *ptr; + thens = make_node(vi, thens, elses); + } while (--ptr >= arr); + } + + return thens; + } + +static int intcompare(const void *a, const void *b) + { + return (*((int *)a) - *((int *)b)); + } diff --git a/robdd/bryant.h b/robdd/bryant.h new file mode 100644 index 000000000..6c8388a2d --- /dev/null +++ b/robdd/bryant.h @@ -0,0 +1,405 @@ +/***************************************************************** + File : bryant.h + RCS : $Id: bryant.h,v 1.1 2000-03-10 05:17:21 dmo Exp $ + Author : Peter Schachte + Origin : Sun Jul 30 15:08:53 1995 + Purpose : header file for users of bryant.c ROBDD package + Copyright: © 1995 Peter Schachte. All rights reserved. + +*****************************************************************/ + +#if defined(QUINTUS) +#include +#endif +#include +#include +#include "var.h" + +/***************************************************************** + Tunable Parameters +*****************************************************************/ + +#if defined(AMIGA) + +/* number of buckets in unique table */ +#define UNIQUE_TABLE_SIZE 4096 + +/* number of entries in ite computed table */ +#define ITE_COMPUTED_TABLE_SIZE 4096 + +/* number of entries in computed table for binary functions (and, or) */ +#define BINARY_CACHE_SIZE 4096 + +/* allocate bryant nodes this many at a time */ +#define POOL_SIZE 4096 + +#else + +/* number of buckets in unique table */ +#define UNIQUE_TABLE_SIZE 65537 /* first prime number > 64K */ + +/* number of entries in ite computed table */ +#define COMPUTED_TABLE_SIZE 16411 /* first prime number > 16K */ + +/* allocate bryant nodes this many at a time */ +#define POOL_SIZE 65535 +#endif + +/* number of bits in an unsigned long, and the log (base 2) of that */ +#define BITS_PER_WORD 32 +#define LOG_BITS_PER_WORD 5 + +/* number of bits in an unsigned char, and a bitmask the size of a char */ +#define BITS_PER_CHAR 8 +#define CHAR_MASK ((1<>LOG_BITS_PER_WORD) +#define BITSET_MASK(elt) (1 << ((elt)&(BITS_PER_WORD-1))) +#define BITSET_CLEAR(set) memset(&set, 0, sizeof(bitset)) +#define BITSET_UNIVERSE(set) memset(&set, ~0, sizeof(bitset)) +#define BITSET_MEMBER(set,word,mask) (0!=((set).bits[(word)]&(mask))) +#define BITSET_ADD(set,word,mask) (set).bits[(word)] |= (mask) +#define BITSET_REMOVE(set,word,mask) (set).bits[(word)] &= ~(mask) +#define BITSET_TOGGLE(set,word,mask) (set).bits[(word)] ^= (mask) + +/* important bit masks */ +#if defined(NO_CHEAP_SHIFT) && BITS_PER_WORD == 32 +#define FOLLOWING_BITS(n) following_bits[n] +#define PRECEDING_BITS(n) preceding_bits[n] +#else /* ! NO_CHEAP_SHIFT */ +#define FOLLOWING_BITS(n) ((~0UL)<<(n)) +#define PRECEDING_BITS(n) ((~0UL)>>(BITS_PER_WORD-1-(n))) +#endif /* NO_CHEAP_SHIFT */ + +#define BITSET_IS_MEMBER(set,n) \ + BITSET_MEMBER(set, BITSET_WORD(n), BITSET_MASK(n)) +#define BITSET_ADD_ELEMENT(set,n) \ + BITSET_ADD(set, BITSET_WORD(n), BITSET_MASK(n)) +#define BITSET_REMOVE_ELEMENT(set,n) \ + BITSET_REMOVE(set, BITSET_WORD(n), BITSET_MASK(n)) +#define BITSET_TOGGLE_ELEMENT(set,n) \ + BITSET_TOGGLE(set, BITSET_WORD(n), BITSET_MASK(n)) + +/* Macros for operations on sets. These are destructive: the first + * argument is modified to hold the result. The i parameter is just a + * usable integer variable that will be destroyed by the macro. These + * should probably be __inline functions, but I don't trust that, + * either. Portability, you know. + */ +#define BITSET_INTERSECTION(set,set1,set2) \ + do { int i; for (i=0; i<=((MAXVAR-1)/BITS_PER_WORD); ++i) \ + (set).bits[i] = (set1).bits[i] & (set2).bits[i];} while (0) +#define BITSET_DIFFERENCE(set,set1,set2) \ + do { int i; for (i=0; i<=((MAXVAR-1)/BITS_PER_WORD); ++i) \ + (set).bits[i] = (set1).bits[i] & ~((set2).bits[i]); } while (0) +#define BITSET_UNION(set,set1,set2) \ + do { int i; for (i=0; i<=((MAXVAR-1)/BITS_PER_WORD); ++i) \ + (set).bits[i] = (set1).bits[i] | (set2).bits[i]; } while (0) +#define BITSET_EXCLUSIVE_UNION(set,set1,set2) \ + do { int i; for (i=0; i<=((MAXVAR-1)/BITS_PER_WORD); ++i) \ + (set).bits[i] = (set1).bits[i] ^ (set2).bits[i]; } while (0) + +#define BITSET_EQUAL(set1, set2) bitset_equal(&set1, &set2) +#define BITSET_DISJOINT(set1, set2) bitset_disjoint(&set1, &set2) +#define BITSET_SUBSET(set1, set2) bitset_subset(&set1, &set2) +#define BITSET_EMPTY(set) bitset_empty(&set) + + +/* Successor and predecessor for possible set elements. These are + * expressions that are false if there are no more possible elements. + */ +#define NEXT_POSSIBLE_ELEMENT(var,word,mask) \ + (++var=0 && ((mask>>=1) || (mask=1<<(BITS_PER_WORD-1),--word))) + + +/* Enumerating sets. Use these like for loops: follow the macro call with + * a statement (or an open brace, some statements, and a close brace). The + * first three iterate from low to high, the last three from high to low. + */ +#define FOREACH_POSSIBLE_ELEMENT(var,word,mask) \ + for (var=0,word=0,mask=1; var0; (void) PREV_POSSIBLE_ELEMENT(var,word,mask)) +#define REV_FOREACH_ELEMENT(set,var,word,mask) \ + for (var=MAXVAR-1,word=((MAXVAR-1)/BITS_PER_WORD),mask=1<<(BITS_PER_WORD-1); \ + prev_element(&set,&var,&word,&mask); \ + (void) PREV_POSSIBLE_ELEMENT(var,word,mask)) +#define REV_FOREACH_NONELEMENT(set,var,word,mask) \ + for (var=MAXVAR-1,word=((MAXVAR-1)/BITS_PER_WORD),mask=1<<(BITS_PER_WORD-1); \ + prev_nonelement(&set,&var,&word,&mask); \ + (void) PREV_POSSIBLE_ELEMENT(var,word,mask)) + + +/***************************************************************** + Other Definitions +*****************************************************************/ + + +#define TRUE 1 +#define FALSE 0 + +/* sneaky trick to make NEW the default */ +#if !defined(USE_RGLB) \ + && !defined(USE_THRESH) \ + && !defined(OLD) \ + && !defined(NAIVE) \ + && !defined(NEW) +#define NEW +#endif + +#if defined(NEW) +#define USE_RGLB +#endif /* NEW */ + +#if defined(USE_RGLB) +#define USE_THRESH +#endif /* USE_RGLB */ + +#if defined(USE_THRESH) +#define OLD +#if !defined(NEW) +#define USE_ITE_CONSTANT /* for var_entailed */ +#endif /* !NEW */ +#endif /* USE_THRESH */ + +#if defined(NEW) +#define WHICH "NEW" +#elif defined(USE_RGLB) +#define WHICH "RGLB" +#elif defined(USE_THRESH) +#define WHICH "THRESH" +#elif defined(OLD) +#define WHICH "OLD" +#elif defined(NAIVE) +#define WHICH "NAIVE" +#else +#error "must define one of NEW, USE_RGLB, USE_THRESH, OLD, or NAIVE." +#endif + + +/***************************************************************** + Public Data +*****************************************************************/ + +extern unsigned char first_one_bit[256]; +extern unsigned char last_one_bit[256]; + +#if defined(NO_CHEAP_SHIFT) && BITS_PER_WORD == 32 +extern bitmask following_bits[BITS_PER_WORD]; +extern bitmask preceding_bits[BITS_PER_WORD]; +#endif + +/***************************************************************** + Prototypes +*****************************************************************/ + +/* this must be called before any other function in this file */ +extern void initRep(void); + +/* this should be called when you're done calling functions in this file */ +/* to clean up memory used by ROBDDs. After calling this, you must call */ +/* InitRep() again before calling any other functions in this file */ +extern void concludeRep(void); + + +/* the basic make a node or return an existing node operation */ +extern node *make_node(int var, node *tr, node *fa); + +/* returns one (the Boolean function true) */ +extern node *trueVar(void); +/* returns zero (the Boolean function false) */ +extern node *falseVar(void); +/* returns var, as an ROBDD. */ +extern node *variableRep(int var); + + +/* returns a \wedge b */ +extern node *glb(node *a, node *b); +/* returns a \vee b */ +extern node *lub(node *a, node *b); +/* returns a \rightarrow b */ +extern node *implies(node *a, node *b); + +/* returns \exists c . a */ +/* extern node *restrict(int c, node *a); */ + +/* returns \bigglb_{0 \leq i \leq n} array[i] */ +extern node *glb_array(int n, int arr[]); + +/* returns a with variable o renamed to n */ +extern node *changename(int o, int n, node *a); +/* returns a with variable 1 renamed to v1, 2 renamed to v2, ... n renamed */ +/* to v_n. Here n is the number of variables to rename */ +extern node *renameList(node *a, int n, int v1, int v2, int v3, int v4, int v5, + int v6, int v7, int v8, int v9, int v10, int v11, int v12, + int v13, int v14, int v15, int v16); +/* returns a with variable v1 renamed to 1, v2 renamed to 2, ... v_n renamed */ +/* to n. Here n is the number of variables to rename */ +extern node *reverseRenameList(node *a, int n, int v1, int v2, int v3, int v4, + int v5, int v6, int v7, int v8, int v9, int v10, + int v11, int v12, int v13, int v14, int v15, int v16); +/* returns a with variable 0 renamed to mapping[0], 1 renamed to */ +/* mapping[1], ... count renamed to mapping[count]. */ +extern node *renameArray(node *in, int count, int mappping[]); +/* returns a with variable mapping[0] renamed to 0, mapping[1] renamed to */ +/* 1, ... mapping[count] renamed to count. */ +extern node *reverseRenameArray(node *in, int count, int rev_mappping[]); + +/* returns v0 \leftrightarrow \bigwedge_{i=0}^{n} arr[i] */ +extern node *iff_conj_array(int v0, int n, int arr[]); +/* returns v0 \leftrightarrow \bigwedge_{i=0}^{n} v_i */ +extern node *iff_conj(int v0, int n, int v1, int v2, int v3, int v4, int v5, + int v6, int v7, int v8, int v9, int v10, int v11, + int v12, int v13, int v14, int v15, int v16); +/* returns non-zero iff f entails variable number var */ +extern int var_entailed(node *f, int var); + +/* Finds the smallest n such that n \in set and n \geq *var. word and */ +/* mask must be as set by BITSET_WORD(*var) and BITSET_MASK(*var), */ +/* respectively. The resulting n is placed in *var, and *word and *mask */ +/* are updated correspondingly. Returns TRUE iff there is such an n. */ +int next_element(bitset *set, int *var, int *word, bitmask *mask); + +/* Finds the largest n such that n \in set and n \leq *var. word and */ +/* mask must be as set by BITSET_WORD(*var) and BITSET_MASK(*var), */ +/* respectively. The resulting n is placed in *var, and *word and *mask */ +/* are updated correspondingly. Returns TRUE iff there is such an n. */ +int prev_element(bitset *set, int *var, int *word, bitmask *mask); + +/* Finds the smallest n such that n \not \in set and n \geq *var. word and */ +/* mask must be as set by BITSET_WORD(*var) and BITSET_MASK(*var), */ +/* respectively. The resulting n is placed in *var, and *word and *mask */ +/* are updated correspondingly. Returns TRUE iff there is such an n. */ +int next_nonelement(bitset *set, int *var, int *word, bitmask *mask); + +/* Finds the largest n such that n \not \in set and n \leq *var. word and */ +/* mask must be as set by BITSET_WORD(*var) and BITSET_MASK(*var), */ +/* respectively. The resulting n is placed in *var, and *word and *mask */ +/* are updated correspondingly. Returns TRUE iff there is such an n. */ +int prev_nonelement(bitset *set, int *var, int *word, bitmask *mask); + + +#if !defined(USE_THRESH) && !defined(RESTRICT_SET) + +/* returns a with all variables lo \leq v \leq hi restricted away */ +extern node *restrictThresh(int lo, int hi, node *a); + +/* returns f \wedge g with all variables lo \leq v \leq hi restricted away */ +extern node *restricted_glb(int lo, int hi, node *f, node *g); + +/* computes g = f with variable 0 renamed to mapping[0], 1 renamed to */ +/* mapping[1], ... count renamed to mapping[count]. Returns context */ +/* \wedge g with all variables lo \leq v \leq hi restricted away */ +extern node *abstract_exit(node *context, node *f, int count, int mapping[], + int lo, int hi); +/* returns f \wedge (v0 \leftrightarrow \bigwedge_{i=0}^{n} arr[i]), */ +/* with all variables lo \leq v \leq hi restricted away */ +extern node *abstract_unify(node *f, int v0, int n, int arr[], int lo, int hi); +#else /* USE_THRESH || RESTRICT_SET */ + +/* returns a with all variables lo \leq v \leq hi restricted away */ +extern node *restrictThresh(int c,node *a); + +/* returns f \wedge g with all variables v \geq c restricted away */ +extern node *restricted_glb(int c, node *f, node *g); + +/* computes g = f with variable 0 renamed to mapping[0], 1 renamed to */ +/* mapping[1], ... count renamed to mapping[count]. Returns context */ +/* \wedge g with all variables v \geq thresh restricted away */ +extern node *abstract_exit(node *context, node *f, int count, int mapping[], + int thresh); + +/* returns f \wedge (v0 \leftrightarrow \bigwedge_{i=0}^{n} arr[i]), */ +/* with all variables v \eq thresh restricted away */ +extern node *abstract_unify(node *f, int v0, int n, int arr[], int thresh); +#endif /* !OLD || USE_THRESH */ + +#if !defined(NEW) +/* returns the set of all v entailed by f where v \leq topvar */ +extern bitset *vars_entailed(node *f, int topvar); +#else /* NEW */ +/* returns the set of all v entailed by f */ +extern bitset *vars_entailed(node *f); +#endif /* NEW */ + +/* return the initial set sharing representation for n variables */ +extern node *init_set_sharing(int n); +/* computes the set sharing upward closure of f */ +extern node *upclose(node *f); +/* performs Langen's bin operation, used for set sharing analysis */ +extern node *bin(node *f, node *g); + +/* prints out the bryant graph a */ +extern void printOut(node *a); + +/* for profiling purposes: return the number of ROBDD nodes in use */ +extern int nodes_in_use(void); +/* for profiling only: the same as iff_conj_array(), but as efficient */ +/* as possible, whatever variables are #defined */ +node *testing_iff_conj_array(int v0, int n, int arr[]); + + +/* These are not really useful for ROBDDs but are needed for other */ +/* representations of Boolean functions. */ +/* free n */ +extern void free_rep(node *n); +/* free n if it doesn't share with m */ +extern void free_rep_if_diff(node *n, node *m); +/* returns a copy of a. For ROBDDs this is just a */ +extern node *copy(node *a); +/* returns non-zero iff a = b; for ROBDDs, use a==b instead */ +extern int equiv(node *a, node *b); + +/* for a more efficient interface from Quintus Prolog. */ +#if defined(QUINTUS) +extern node *renameTerm(node *in, QP_term_ref term); +extern node *reverseRenameTerm(node *in, QP_term_ref term); +#endif /* QUINTUS */ diff --git a/robdd/bryantPrint.c b/robdd/bryantPrint.c new file mode 100644 index 000000000..7f33572be --- /dev/null +++ b/robdd/bryantPrint.c @@ -0,0 +1,64 @@ +#include +#include +#ifdef QUINTUS +#include +#endif +#include "bryant.h" +#include "bryantPrint.h" + + +int print_bryant(node *f, bitset *trues, bitset *falses, int terms); + + +/* Print out an ROBDD in some readable format. We display it in disjunctive + * form. + */ + +void printOut(node *f) + { + bitset trues, falses; + + if (f == one) { + printf("TRUE"); + } else if (f == zero) { + printf("FALSE"); + } else { + BITSET_CLEAR(trues); + BITSET_CLEAR(falses); + (void)print_bryant(f, &trues, &falses, 0); + } + } + + +int print_bryant(node *f, bitset *trues, bitset *falses, int terms) + { + if (f == one) { + bitset all; + int var; + int word; + bitmask mask; + char sep = '('; + + if (terms>0) printf(" "); + BITSET_UNION(all, *trues, *falses); + FOREACH_ELEMENT(all, var, word, mask) { + if (BITSET_MEMBER(*trues, word, mask)) { + printf("%c%d", sep, var); + } else { + printf("%c~%d", sep, var); + } + sep = ' '; + } + printf(")"); + ++terms; + } else if (f != zero) { + BITSET_ADD_ELEMENT(*trues, f->value); + terms += print_bryant(f->tr, trues, falses, terms); + BITSET_TOGGLE_ELEMENT(*trues, f->value); + BITSET_ADD_ELEMENT(*falses, f->value); + terms += print_bryant(f->fa, trues, falses, terms); + BITSET_TOGGLE_ELEMENT(*falses, f->value); + } + /* don't do anything for zero terminal */ + return terms; + } diff --git a/robdd/bryantPrint.h b/robdd/bryantPrint.h new file mode 100644 index 000000000..e69de29bb diff --git a/robdd/runall b/robdd/runall new file mode 100755 index 000000000..b51ebc40a --- /dev/null +++ b/robdd/runall @@ -0,0 +1,27 @@ +#!/bin/sh + +echo "Timing run on `hostname` begun `date`" + +run=1 +runs=10 +reps="naive old thresh rglb new" + +while [ $run -le $runs ] ; do + echo "beginning run $run of $runs" + for rep in $reps ; do + uptime + echo "testing $rep version..." + ${rep}tests/test_glb 24 26 + ${rep}tests/test_iff 26 30 + ${rep}tests/test_restrict 22 25 + ${rep}tests/test_rglb 14 16 + ${rep}tests/test_abunify 13 15 + ${rep}tests/test_rename 8 9 + ${rep}tests/test_abexit 8 9 + ${rep}tests/test_var 30 32 + ${rep}tests/test_vars 30 32 + done + run=`expr $run + 1` +done + +echo "Timing run completed `date`" diff --git a/robdd/table.c b/robdd/table.c new file mode 100644 index 000000000..5c5d6a151 --- /dev/null +++ b/robdd/table.c @@ -0,0 +1,148 @@ +#include +#include +#include "bryant.h" +#include "table.h" + +#define TABLESIZE 4096 + +node *lookupUniqueTable(int val, node *tr, node *fa); +void insertUniqueTable(node *newnode); + +node *checkComputed(node *f,node *g, node *h); +void insertComputed(node *f, node *g, node *h, node *result); + +void printUnique(); /* prints no. of entries in Unique table */ + +static node *unique[TABLESIZE]; +static iteEntry computed[TABLESIZE]; + +static int findHashUnique(int var, node *tr, node *fa); +static int findHashComputed(node *f, node *g, node *h); + +node *lookupUniqueTable(int val, node *tr, node *fa) +/* checks to see if node (val,tr,fa) exists, and if so returns pointer to +that node, otherwise returns null */ +{ + extern node *unique[]; + node *entry; + node *result; + int hash; + + result = NULL; + /* find hash value - get 12 bits, ie. 4096, size of unique */ + hash = findHashUnique(val,tr,fa); + entry = unique[hash]; + while(entry!=NULL) + { + if((entry->tr==tr) && (entry->fa ==fa) && (entry->value==val)) + { + result=entry; + break; + } + entry=entry->unique; + } + return result; +} +void insertUniqueTable(node *newnode) +{ +/* inserts the node newnode into the unique table */ +/* insertion is at head of list */ + extern node *unique[]; + node *first; + node *newentry; + int hash; + + /* find hash value - get 12 bits, ie. 4096, size of unique */ + hash = findHashUnique(newnode->value,newnode->tr,newnode->fa); + + newnode->unique = unique[hash]; + unique[hash] = newnode; +} + +void printUnique() +{ + node *t; + int i; + int cnt; + int total; + int longest; + + total = 0; + longest = 0; + for (i=0; i longest) + longest = cnt; + t= t->unique; + } + if(total > 130000) + { + if (cnt != 0) + printf("unique[%d]: %d\n",i,cnt); + } + total = total+cnt; + } + printf("total nodes is %d: longest string is %d\n",total,longest); +} + +node *checkComputed(node *f,node *g, node *h) +{ + extern iteEntry computed[]; + int hash; + + hash = findHashComputed(f,g,h); + + if ((computed[hash].f == f) && + (computed[hash].g == g) && + (computed[hash].h == h)) + { + return computed[hash].where; + } + return NULL; +} +void insertComputed(node *f, node *g, node *h, node *result) +{ + extern iteEntry computed[]; + int hash; + int i; + + /* find hash value - get 12 bits, ie. 4096, size of computed */ + /* check hashing function, g or h is always zero or one */ + + hash = findHashComputed(f,g,h); + + computed[hash].f = f; + computed[hash].g = g; + computed[hash].h = h; + computed[hash].where = result; + +/* + printf("in computed \n"); + for (i=0; i> 2)) & 0xfff; +} + +static int findHashComputed(node *f, node *g, node *h) +{ + /* find hash value - get 12 bits, ie. 4096, size of computed */ + return (((long)h) + ((long)g << 1) + + ((long)f >> 2)) & 0xfff; +} + diff --git a/robdd/table.h b/robdd/table.h new file mode 100644 index 000000000..9b130c860 --- /dev/null +++ b/robdd/table.h @@ -0,0 +1,6 @@ +typedef struct IteEntry{ + node *f; + node *g; + node *h; + node *where; + }iteEntry; diff --git a/robdd/test_abexit.c b/robdd/test_abexit.c new file mode 100644 index 000000000..728b0e7ee --- /dev/null +++ b/robdd/test_abexit.c @@ -0,0 +1,177 @@ +/***************************************************************** + File : test_abexit.c + RCS : $Id: test_abexit.c,v 1.1 2000-03-10 05:17:22 dmo Exp $ + Author : Peter Schachte + Origin : Tue Aug 1 11:27:35 1995 + Purpose : Timing test for bryant graph abstract_exit code + +*****************************************************************/ + +#include +#include +#include "bryant.h" +#include "timing.h" + + +int opcount; + +void usage(char *progname) + { + printf("usage: %s size maxvar [repetitions]\n", progname); + printf(" does all possible renamings of a certain boolean function of the specified\n"); + printf(" size using variables 0..maxvar inclusive. If repetitions is >0, this will\n"); + printf(" be done that many times.\n"); + } + + +void init_array(int top, int array[], bitset *usedvars) + { + int i, word; + bitmask mask; + + BITSET_CLEAR(*usedvars); + FOREACH_POSSIBLE_ELEMENT(i, word, mask) { + if (i >= top) break; + array[i] = i; + BITSET_ADD(*usedvars, word, mask); + } + } + + + +int next_array(int n, int varmax, int array[], bitset *usedvars) + { + int i, word; + bitmask mask; + int elt; + + /* Search backward for first cell with "room" to be incremented. */ + for (i=n-1;; --i) { + if (i<0) return FALSE; /* no more combinations possible */ + elt=array[i]; + word = BITSET_WORD(elt); + mask = BITSET_MASK(elt); + BITSET_REMOVE(*usedvars, word, mask); + (void) NEXT_POSSIBLE_ELEMENT(elt, word, mask); + if (next_nonelement(usedvars, &elt, &word, &mask) && elt=MAXVAR) { + usage(argv[0]); + printf("\n varmax must be between 4 <= varmax < %d\n", MAXVAR); + return 20; + } + if ((size=atoi(argv[1]))<0 || size>varmax) { + usage(argv[0]); + printf("\n size must be between 0 <= size <= varmax\n"); + return 20; + } + repetitions=(argc>3 ? atoi(argv[3]) : 1); + if (repetitions <= 0) repetitions = 1; + + for (i=0; i0; --reps) { + init_array(size, array, &set); + doit(size, array, varmax, f, g, thresh); + while (next_array(size, varmax, array, &set)) { + doit(size, array, varmax, f, g, thresh); + } + } + clock1 = milli_time(); + test_nodes = nodes_in_use(); + initRep(); + + for (i=0; i<(size-1)/2; ++i) array[i] = i*2+1; + f = testing_iff_conj_array(0, (size-1)/2, array); + for (i=0; i<(size-2)/2; ++i) array[i] = i*2+2; + f = glb(f, testing_iff_conj_array(size-1, (size-2)/2, array)); + + clock2 = milli_time(); + for (reps=repetitions; reps>0; --reps) { + init_array(size, array, &set); + dont_doit(size, array, varmax, f, g, thresh); + while (next_array(size, varmax, array, &set)) { + dont_doit(size, array, varmax, f, g, thresh); + } + } + clock3 = milli_time(); + overhead_nodes = nodes_in_use(); + runtime = (float)(clock1-clock0)/1000; + overhead = (float)(clock3-clock2)/1000; + rate = ((float)opcount)/(runtime-overhead); + printf("%s %d %d %d: %.3f - %.3f = %.3f secs, %d ops, %d nodes, %.1f ops/sec\n", + argv[0], size, varmax, repetitions, + runtime, overhead, (runtime-overhead), opcount, + test_nodes-overhead_nodes, rate); + return 0; + } diff --git a/robdd/test_abunify.c b/robdd/test_abunify.c new file mode 100644 index 000000000..19b809af0 --- /dev/null +++ b/robdd/test_abunify.c @@ -0,0 +1,205 @@ +/***************************************************************** + File : test_abunify.c + RCS : $Id: test_abunify.c,v 1.1 2000-03-10 05:17:22 dmo Exp $ + Author : Peter Schachte + Origin : Fri Aug 4 14:39:44 1995 + Purpose : Timing test for bryant graph abstract_unify code + +*****************************************************************/ + +#include +#include +#include "bryant.h" +#include "timing.h" + + +int opcount; + +void usage(char *progname) + { + printf("usage: %s size maxvar [repetitions]\n", progname); + printf(" for all possible v <-> v1 & v2 & ... & vsize functions, computes the glb\n"); + printf(" of that and each possible v <-> v1 & v2 & ... & vsize function, restricted\n"); + printf(" to each threshold between 0 and maxvar. Each v and the vi are between 0\n"); + printf(" and maxvar inclusive. If repetitions is >0, this will be done that many\n"); + printf(" times.\n"); + } + + +void init_array(int top, int v0, int array[]) + { + int i, val; + + for (i=0, val=0; i0) { + printf("%d", arr[0]); + for (i=1; i=MAXVAR) { + usage(argv[0]); + printf("\n varmax must be between 1 <= varmax < %d\n", MAXVAR); + return 20; + } + if ((size=atoi(argv[1]))<0 || size>=varmax) { + usage(argv[0]); + printf("\n size must be between 0 <= size < varmax\n"); + return 20; + } + repetitions=(argc>3 ? atoi(argv[3]) : 1); + if (repetitions <= 0) repetitions = 1; + + opcount = 0; + clock0 = milli_time(); + for (reps=repetitions; reps>0; --reps) { + for (thresh=0; thresh<=varmax; ++thresh) { + for (vf=0; vf0; --reps) { + for (thresh=0; thresh<=varmax; ++thresh) { + for (vf=0; vf +#include +#include "bryant.h" +#include "timing.h" + +#define VARLIMIT 1024 + +int opcount; + +void usage(char *progname) + { + printf("usage: %s size maxvar [repetitions]\n", progname); + printf(" creates all possible pairs of v <-> v1 & v2 & ... & vsize functions and\n"); + printf(" computes their glb. Each V and the vi are between 0 and maxvar inclusive.\n"); + printf(" If repetitions is >0, this will be done that many times.\n"); + } + + +void init_array(int top, int v0, int array[]) + { + int i, val; + + for (i=0, val=0; i=VARLIMIT) { + usage(argv[0]); + printf("\n varmax must be between 1 <= varmax < %d\n", VARLIMIT); + return 20; + } + if ((size=atoi(argv[1]))<0 || size>=varmax) { + usage(argv[0]); + printf("\n size must be between 0 <= size < varmax\n"); + return 20; + } + repetitions=(argc>3 ? atoi(argv[3]) : 1); + if (repetitions <= 0) repetitions = 1; + + opcount = 0; + clock0 = milli_time(); + for (reps=repetitions; reps>0; --reps) { + for (vf=0; vf0; --reps) { + for (vf=0; vf +#include +#include "bryant.h" +#include "timing.h" + + +#define VARLIMIT 1024 + +int opcount; + +void usage(char *progname) + { + printf("usage: %s size maxvar [repetitions]\n", progname); + printf(" creates all possible v <-> v1 & v2 & ... & vsize functions where v and\n"); + printf(" v and the vi are between 0 and maxvar inclusive. If repetitions is >0,\n"); + printf(" this will be done that many times.\n"); + } + + +void init_array(int top, int v0, int array[]) + { + int i, val; + + for (i=0, val=0; i ", v0); + for (i=0; i "); + printOut(f); + printf("\n"); +#endif /* DEBUGALL */ +#endif /* !OVERHEAD */ + ++opcount; + } + +void dont_doit(int v0, int top, int array[]) + { + } + +int main(int argc, char **argv) + { + int varmax, size, repetitions; + int array[VARLIMIT]; + int reps, v0; + millisec clock0, clock1, clock2, clock3; + float runtime, overhead, rate; + int test_nodes, overhead_nodes; + + if (argc < 3) { + usage(argv[0]); + return 20; + } + if ((varmax=atoi(argv[2]))<1 || varmax>=VARLIMIT) { + usage(argv[0]); + printf("\n varmax must be between 1 <= varmax < %d\n", VARLIMIT); + return 20; + } + if ((size=atoi(argv[1]))<0 || size>=varmax) { + usage(argv[0]); + printf("\n size must be between 0 <= size < varmax\n"); + return 20; + } + repetitions=(argc>3 ? atoi(argv[3]) : 1); + if (repetitions <= 0) repetitions = 1; + + opcount = 0; + clock0 = milli_time(); + for (reps=repetitions; reps>0; --reps) { + for (v0=0; v00; --reps) { + for (v0=0; v0 +#include +#include "bryant.h" +#include "timing.h" + + +int opcount; + +void usage(char *progname) + { + printf("usage: %s size maxvar [repetitions]\n", progname); + printf(" does all possible renamings of a certain boolean function of the specified\n"); + printf(" size using variables 0..maxvar inclusive. If repetitions is >0, this will\n"); + printf(" be done that many times.\n"); + } + + +void init_array(int top, int array[], bitset *usedvars) + { + int i, word; + bitmask mask; + + BITSET_CLEAR(*usedvars); + FOREACH_POSSIBLE_ELEMENT(i, word, mask) { + if (i >= top) break; + array[i] = i; + BITSET_ADD(*usedvars, word, mask); + } + } + + + +int next_array(int n, int varmax, int array[], bitset *usedvars) + { + int i, word; + bitmask mask; + int elt; + + /* Search backward for first cell with "room" to be incremented. */ + for (i=n-1;; --i) { + if (i<0) return FALSE; /* no more combinations possible */ + elt=array[i]; + word = BITSET_WORD(elt); + mask = BITSET_MASK(elt); + BITSET_REMOVE(*usedvars, word, mask); + (void) NEXT_POSSIBLE_ELEMENT(elt, word, mask); + if (next_nonelement(usedvars, &elt, &word, &mask) && elt=MAXVAR) { + usage(argv[0]); + printf("\n varmax must be between 2 <= varmax < %d\n", MAXVAR); + return 20; + } + if ((size=atoi(argv[1]))<0 || size>varmax) { + usage(argv[0]); + printf("\n size must be between 0 <= size <= varmax\n"); + return 20; + } + repetitions=(argc>3 ? atoi(argv[3]) : 1); + if (repetitions <= 0) repetitions = 1; + + for (i=0; i<(size-1)/2; ++i) array[i] = i*2+1; + f = testing_iff_conj_array(0, (size-1)/2, array); + for (i=0; i<(size-2)/2; ++i) array[i] = i*2+2; + f = glb(f, testing_iff_conj_array(size-1, (size-2)/2, array)); + + opcount = 0; + clock0 = milli_time(); + for (reps=repetitions; reps>0; --reps) { + init_array(size, array, &set); + doit(size, array, varmax, f); + while (next_array(size, varmax, array, &set)) { + doit(size, array, varmax, f); + } + } + clock1 = milli_time(); + test_nodes = nodes_in_use(); + initRep(); + + for (i=0; i<(size-1)/2; ++i) array[i] = i*2+1; + f = testing_iff_conj_array(0, (size-1)/2, array); + for (i=0; i<(size-2)/2; ++i) array[i] = i*2+2; + f = glb(f, testing_iff_conj_array(size-1, (size-2)/2, array)); + + clock2 = milli_time(); + for (reps=repetitions; reps>0; --reps) { + init_array(size, array, &set); + dont_doit(size, array, varmax, f); + while (next_array(size, varmax, array, &set)) { + dont_doit(size, array, varmax, f); + } + } + clock3 = milli_time(); + overhead_nodes = nodes_in_use(); + runtime = (float)(clock1-clock0)/1000; + overhead = (float)(clock3-clock2)/1000; + rate = ((float)opcount)/(runtime-overhead); + printf("%s %d %d %d: %.3f - %.3f = %.3f secs, %d ops, %d nodes, %.1f ops/sec\n", + argv[0], size, varmax, repetitions, + runtime, overhead, (runtime-overhead), opcount, + test_nodes-overhead_nodes, rate); + return 0; + } diff --git a/robdd/test_restrict.c b/robdd/test_restrict.c new file mode 100644 index 000000000..77432ec85 --- /dev/null +++ b/robdd/test_restrict.c @@ -0,0 +1,167 @@ +/***************************************************************** + File : test_restrict.c + RCS : $Id: test_restrict.c,v 1.1 2000-03-10 05:17:22 dmo Exp $ + Author : Peter Schachte + Origin : Mon Jul 17 19:54:11 1995 + Purpose : Timing test for bryant graph restrictThresh code + +*****************************************************************/ + + +#include +#include +#include "bryant.h" +#include "timing.h" + + +#define VARLIMIT 1024 + +int opcount; + +void usage(char *progname) + { + printf("usage: %s size maxvar [repetitions]\n", progname); + printf(" creates all possible v <-> v1 & v2 & ... & vsize functions and restricts by\n"); + printf(" all possible thresholds between 0 and maxvar. V and the vi are between 0 and\n"); + printf(" maxvar inclusive. If repetitions is >0, this will be done that many times.\n"); + } + + +void init_array(int top, int v0, int array[]) + { + int i, val; + + for (i=0, val=0; i=VARLIMIT) { + usage(argv[0]); + printf("\n varmax must be between 1 <= varmax < %d\n", VARLIMIT); + return 20; + } + if ((size=atoi(argv[1]))<0 || size>=varmax) { + usage(argv[0]); + printf("\n size must be between 0 <= size < varmax\n"); + return 20; + } + repetitions=(argc>3 ? atoi(argv[3]) : 1); + if (repetitions <= 0) repetitions = 1; + + opcount = 0; + clock0 = milli_time(); + for (reps=repetitions; reps>0; --reps) { + for (v0=0; v00; --reps) { + for (v0=0; v0 +#include +#include "bryant.h" +#include "timing.h" + + +#define VARLIMIT 1024 + +int opcount; + +void usage(char *progname) + { + printf("usage: %s size maxvar [repetitions]\n", progname); + printf(" creates all possible pairs of v <-> v1 & v2 & ... & vsize functions, computes\n"); + printf(" their glb, and restricts this to each threshold between 0 and maxvar. Each V\n"); + printf(" and the vi are between 0 and maxvar inclusive. If repetitions is >0, this\n"); + printf(" will be done that many times.\n"); + } + + +void init_array(int top, int v0, int array[]) + { + int i, val; + + for (i=0, val=0; i=VARLIMIT) { + usage(argv[0]); + printf("\n varmax must be between 1 <= varmax < %d\n", VARLIMIT); + return 20; + } + if ((size=atoi(argv[1]))<0 || size>=varmax) { + usage(argv[0]); + printf("\n size must be between 0 <= size < varmax\n"); + return 20; + } + repetitions=(argc>3 ? atoi(argv[3]) : 1); + if (repetitions <= 0) repetitions = 1; + + opcount = 0; + clock0 = milli_time(); + for (reps=repetitions; reps>0; --reps) { + for (thresh=0; thresh<=varmax; ++thresh) { + for (vf=0; vf0; --reps) { + for (thresh=0; thresh<=varmax; ++thresh) { + for (vf=0; vf +#include +#include "bryant.h" +#include "timing.h" + + +int opcount; + +void usage(char *progname) + { + printf("usage: %s depth [repetitions]\n", progname); + printf(" creates random boolean functions of depth depth (or less) and\n"); + printf(" computes their upward closure. If repetitions is >0,\n"); + printf(" this will be done that many times.\n"); + } + + +#if 0 +node *boolfn(unsigned long n) + { + int d; + unsigned long tr, fa; + node *trfn, *fafn; + + if (n == 0) return zero; + if (n == 1) return one; + + for (d = LOG_BITS_PER_WORD-1; (fa=(n>>(1<= 0; --d); + tr = n & ((1<<(1<>=1) ++rand_bits; + bits = 0; + srand(4242); + } + + +node *randboolfn(int depth, int level) + { + node *result; + + if (bits <= 0) rnd = rand(), bits = rand_bits; + + if (level == 0) { + result = (rnd&1) ? one : zero; + bits--; rnd >>= 1; + } else { + result = make_node(depth-level, + randboolfn(depth, level-1), + randboolfn(depth, level-1)); + } + return result; + } + +void doit(int depth, int num) + { + node *f = randboolfn(depth, depth); + node *uf; + +#ifdef DEBUGALL + printf("%6d upclose(", num); + printOut(f); + printf(") ==> "); + fflush(stdout); +#endif /* DEBUGALL */ +#ifndef OVERHEAD + uf = upclose(f); +#ifdef DEBUGALL + if (f == uf) { + printf("UNCHANGED"); + } else { + printOut(uf); + } + printf("\n"); +#endif /* DEBUGALL */ +#endif /* !OVERHEAD */ + ++opcount; + } + + +void dont_doit(int depth, int num) + { + (void) randboolfn(depth, depth); + } + + +int main(int argc, char **argv) + { + int depth, repetitions; + int reps; + millisec clock0, clock1, clock2, clock3; + float runtime, overhead, rate; + int test_nodes, overhead_nodes; + + if (argc < 2) { + usage(argv[0]); + return 20; + } + if ((depth=atoi(argv[1]))<1 || depth>=MAXVAR) { + usage(argv[0]); + printf("\n depth must be between 1 <= depth < %d\n", MAXVAR); + return 20; + } + repetitions=(argc>2 ? atoi(argv[2]) : 1); + if (repetitions <= 0) repetitions = 1; + + opcount = 0; + initRep(); + init_random(); + clock0 = milli_time(); + for (reps=0; reps +#include +#include "bryant.h" +#include "timing.h" + + +#define VARLIMIT 1024 + +int opcount; + +void usage(char *progname) + { + printf("usage: %s size maxvar [repetitions]\n", progname); + printf(" creates all possible v <-> v1 & v2 & ... & vsize functions and conjoins this\n"); + printf(" with each variable between 0 and maxvar, and then determines for each variable\n"); + printf(" between 0 and maxvar if that variable is entailed by this function.\n"); + printf(" V and the vi are between 0 and maxvar inclusive. If repetitions is >0,\n"); + printf(" this will be done that many times.\n"); + } + + +void init_array(int top, int v0, int array[]) + { + int i, val; + + for (i=0, val=0; i=VARLIMIT) { + usage(argv[0]); + printf("\n varmax must be between 1 <= varmax < %d\n", VARLIMIT); + return 20; + } + if ((size=atoi(argv[1]))<0 || size>=varmax) { + usage(argv[0]); + printf("\n size must be between 0 <= size < varmax\n"); + return 20; + } + repetitions=(argc>3 ? atoi(argv[3]) : 1); + if (repetitions <= 0) repetitions = 1; + + opcount = 0; + clock0 = milli_time(); + for (reps=repetitions; reps>0; --reps) { + for (v0=0; v00; --reps) { + for (v0=0; v0 +#include +#include "bryant.h" +#include "timing.h" + + +#define VARLIMIT 1024 + +int opcount; + +void usage(char *progname) + { + printf("usage: %s size maxvar [repetitions]\n", progname); + printf(" creates all possible v <-> v1 & v2 & ... & vsize functions and conjoins this\n"); + printf(" with each variable between 0 and maxvar, and then determines the set of\n"); + printf(" variables entailed by this function. V and the vi are between 0 and maxvar\n"); + printf(" inclusive. If repetitions is >0, this will be done that many times.\n"); + } + + +void init_array(int top, int v0, int array[]) + { + int i, val; + + for (i=0, val=0; i=VARLIMIT) { + usage(argv[0]); + printf("\n varmax must be between 1 <= varmax < %d\n", VARLIMIT); + return 20; + } + if ((size=atoi(argv[1]))<0 || size>=varmax) { + usage(argv[0]); + printf("\n size must be between 0 <= size < varmax\n"); + return 20; + } + repetitions=(argc>3 ? atoi(argv[3]) : 1); + if (repetitions <= 0) repetitions = 1; + + opcount = 0; + clock0 = milli_time(); + for (reps=repetitions; reps>0; --reps) { + for (v0=0; v00; --reps) { + for (v0=0; v0 + +millisec milli_time(void) + { + return (millisec) (clock()/1000); + } +#else +/* assume it's unix, and we'll be using getrusage() */ + +#include +#include + +#if 0 +#include +#else +void getrusage(int, struct rusage *); +#endif + +millisec milli_time(void) + { + struct rusage p; + + getrusage(RUSAGE_SELF, &p); + return (millisec)(p.ru_utime.tv_sec * 1000) + + (millisec)(p.ru_utime.tv_usec / 1000); + } +#endif diff --git a/robdd/timing.h b/robdd/timing.h new file mode 100644 index 000000000..8035b148f --- /dev/null +++ b/robdd/timing.h @@ -0,0 +1,13 @@ +/***************************************************************** + File : timing.h + RCS : $Id: timing.h,v 1.1 2000-03-10 05:17:23 dmo Exp $ + Author : Peter Schachte + Origin : Sat Aug 12 15:28:57 1995 + Purpose : header file for timing support + Copyright: © 1995 Peter Schachte. All rights reserved. + +*****************************************************************/ + +typedef unsigned long millisec; + +millisec milli_time(void); diff --git a/robdd/var.h b/robdd/var.h new file mode 100644 index 000000000..5c3ee32ef --- /dev/null +++ b/robdd/var.h @@ -0,0 +1,13 @@ +/***************************************************************** + File : var.h + RCS : $Id: var.h,v 1.1 2000-03-10 05:17:22 dmo Exp $ + Author : Peter Schachte + Origin : Mon Oct 12 06:09:27 1998 + Purpose : Definitions common to all representations of Boolean variables + Copyright: © 1998 . All rights reserved. + +*****************************************************************/ + + +/* the most variables we can support */ +#define MAXVAR 64