[m-rev.] diff/for review: library changes from mode_constraints branch (part 2)
Zoltan Somogyi
zs at cs.mu.OZ.AU
Wed Dec 15 16:35:13 AEDT 2004
Index: robdd/bryant.c
===================================================================
RCS file: /home/mercury1/repository/mercury/robdd/bryant.c,v
retrieving revision 1.1
diff -u -r1.1 bryant.c
--- robdd/bryant.c 10 Mar 2000 05:17:21 -0000 1.1
+++ robdd/bryant.c 31 Aug 2003 14:48:22 -0000
@@ -1,96 +1,110 @@
+/*
+** vim: ts=4 sw=4 expandtab
+*/
+/*
+** Copyright (C) 1995, 2001-2003 Peter Schachte and The University of Melbourne.
+** This file may only be copied under the terms of the GNU Library General
+** Public License - see the file COPYING.LIB in the Mercury distribution.
+*/
+
/*****************************************************************
File : 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
-
+ 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.
-
+ MR_ROBDD_STATISTICS Controls collecting of computed and unique
+ table hash performance. If defined,
+ MR_ROBDD_concludeRep() prints out a bunch of
+ statistics.
+
+ MR_ROBDD_CLEAR_CACHES If defined, all computed and unique tables are
+ cleared on a call to MR_ROBDD_initRep(). This makes
+ running a number of tests in sequence more
+ fair.
+
+ MR_ROBDD_NAIVE If defined, uses very naive algorithms for
+ MR_ROBDD_iff_conj_array, MR_ROBDD_renameArray,
+ MR_ROBDD_lub, MR_ROBDD_glb, and probably some I've
+ forgotten.
+
+ MR_ROBDD_OLD If defined, use slightly less naive algorithms for
+ MR_ROBDD_restrictThresh, MR_ROBDD_restricted_glb,
+ MR_ROBDD_vars_entailed, and
+ MR_ROBDD_iff_conj_array.
+
+ MR_ROBDD_USE_THRESH Like MR_ROBDD_OLD, except that it does use the new
+ code for MR_ROBDD_restrictThresh. Implies
+ MR_ROBDD_OLD.
+
+ MR_ROBDD_USE_RGLB Like MR_ROBDD_USE_THRESH, except that it also uses
+ the new code for MR_ROBDD_restricted_glb. Implies
+ MR_ROBDD_USE_THRESH.
+
+ MR_ROBDD_NEW Like MR_ROBDD_USE_RGLB, but uses all the lastest
+ and greatest algorithms. Implies MR_ROBDD_USE_RGLB.
+
+ MR_ROBDD_USE_ITE_CONSTANT
+ Include the MR_ROBDD_ite_constant function, and'
+ use it to speed up the non-MR_ROBDD_NEW version of
+ MR_ROBDD_var_entailed (and MR_ROBDD_vars_entailed).
+
+ MR_ROBDD_SHARING Include algorithms useful in sharing analysis
+ performed using Boolean functions.
+
+ MR_ROBDD_RESTRICT_SET Only meaningful if MR_ROBDD_OLD &&
+ !MR_ROBDD_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.
+
+ MR_ROBDD_WHICH Is defined to "MR_ROBDD_NAIVE", "MR_ROBDD_OLD",
+ "MR_ROBDD_USE_THRESH", "MR_ROBDD_USE_RGLB", or
+ "MR_ROBDD_NEW", depending on which of the
+ MR_ROBDD_NAIVE, MR_ROBDD_OLD, MR_ROBDD_USE_THRESH,
+ and MR_ROBDD_USE_RGLB variables are defined. This
+ is automatically defined by bryant.h based on the
+ above variables.
+
+ MR_ROBDD_VE_GLB (only when MR_ROBDD_OLD is defined) if defined,
+ MR_ROBDD_var_entailed(fn, v) compares the fn to
+ MR_ROBDD_glb(MR_ROBDD_variableRep(v), fn). The var
+ is entailed if they are equal. Otherwise computes
+ MR_ROBDD_variableRep(v) -> fn. The variable is
+ entailed if this is 'MR_ROBDD_one'.
+
+ MR_ROBDD_ELIM_DUPS If defined, MR_ROBDD_iff_conj_array will not assume
+ that the input array has no duplicates. It will
+ still assume that it's sorted.
+
+ MR_ROBDD_COMPUTED_TABLE Enables the computed table in MR_ROBDD_lub,
+ MR_ROBDD_glb, MR_ROBDD_ite, and
+ MR_ROBDD_restricted_glb.
+
+ MR_ROBDD_EQUAL_TEST If defined, MR_ROBDD_lub(), MR_ROBDD_glb(), and
+ MR_ROBDD_restricted_glb compare their arguments for
+ equality, and if equal return it as value.
+ MR_ROBDD_ite and MR_ROBDD_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.
+
+ MR_ROBDD_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 "mercury_imp.h"
#include <stdio.h>
#include <stdlib.h>
#include <math.h>
@@ -98,26 +112,44 @@
#include <limits.h>
#include "bryant.h"
+#ifdef MR_ROBDD_BRYANT_CONSERVATIVE_GC
+
+ /* Don't use pools of nodes with the conservative GC. */
+ #undef MR_ROBDD_POOL
+
+ /* Redefine malloc() and free() to use the GC versions */
+ #define malloc(n) GC_malloc(n)
+ #define free(p) GC_free(p)
-#define UNUSED_MAPPING -1 /* this MUST BE -1 */
+#else /* !MR_ROBDD_BRYANT_CONSERVATIVE_GC */
-#if !defined(max)
-#define max(a,b) ((a)<(b) ? (b) : (a))
+ #define MR_ROBDD_POOL
+
+#endif /* MR_ROBDD_BRYANT_CONSERVATIVE_GC */
+
+#define MR_ROBDD_REVEAL_NODE_POINTER(p) \
+ ((MR_ROBDD_node *) MR_ROBDD_REVEAL_POINTER(p))
+
+#define MR_ROBDD_UNUSED_MAPPING -1 /* this MUST BE -1 */
+
+#if !defined(MR_ROBDD_max)
+ #define MR_ROBDD_max(a,b) ((a)<(b) ? (b) : (a))
#endif
-#if !defined(min)
-#define min(a,b) ((a)<(b) ? (a) : (b))
+#if !defined(MR_ROBDD_min)
+ #define MR_ROBDD_min(a,b) ((a)<(b) ? (a) : (b))
#endif
-#define PERCENTAGE(x,y) ((100.0 * (float)(x)) / (float)(y))
+#define MR_ROBDD_PERCENTAGE(x,y) ((100.0 * (float)(x)) / (float)(y))
-typedef struct pool {
- node data[POOL_SIZE];
+#ifdef MR_ROBDD_POOL
+ typedef struct pool {
+ MR_ROBDD_node data[MR_ROBDD_POOL_SIZE];
struct pool *prev;
-} pool;
+ } pool;
+#endif /* MR_ROBDD_POOL */
-
-#if defined(NO_CHEAP_SHIFT) && BITS_PER_WORD == 32
-bitmask following_bits[BITS_PER_WORD] =
+#if defined(MR_ROBDD_NO_CHEAP_SHIFT) && MR_ROBDD_BITS_PER_WORD == 32
+ MR_ROBDD_bitmask MR_ROBDD_following_bits[MR_ROBDD_BITS_PER_WORD] =
{ 0xffffffff, 0xfffffffe, 0xfffffffc, 0xfffffff8,
0xfffffff0, 0xffffffe0, 0xffffffc0, 0xffffff80,
0xffffff00, 0xfffffe00, 0xfffffc00, 0xfffff800,
@@ -128,7 +160,7 @@
0xf0000000, 0xe0000000, 0xc0000000, 0x80000000
};
-bitmask preceding_bits[BITS_PER_WORD] =
+ MR_ROBDD_bitmask MR_ROBDD_preceding_bits[MR_ROBDD_BITS_PER_WORD] =
{ 0x00000001, 0x00000003, 0x00000007, 0x0000000f,
0x0000001f, 0x0000003f, 0x0000007f, 0x000000ff,
0x000001ff, 0x000003ff, 0x000007ff, 0x00000fff,
@@ -140,8 +172,7 @@
};
#endif
-
-unsigned char first_one_bit[256] =
+unsigned char MR_ROBDD_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 */
@@ -160,7 +191,7 @@
4, 0, 1, 0, 2, 0, 1, 0, 3, 0, 1, 0, 2, 0, 1, 0, /* 256 */
};
-unsigned char last_one_bit[256] =
+unsigned char MR_ROBDD_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 */
@@ -179,125 +210,135 @@
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;
+MR_ROBDD_bitset MR_ROBDD_emptyset;
/****************************************************************
- Macros to avoid #ifdefs
+ 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)
+#if defined(MR_ROBDD_COMPUTED_TABLE) && defined(MR_ROBDD_CLEAR_CACHES)
+ #define MR_ROBDD_CLEAR_CACHE(op) \
+ MR_memset(op##_computed_cache, 0, sizeof(op##_computed_cache))
+#else /* !MR_ROBDD_CLEAR_CACHES || !MR_ROBDD_COMPUTED_TABLE */
+ #define MR_ROBDD_CLEAR_CACHE(op)
#endif
+#if defined(MR_ROBDD_STATISTICS)
-#if defined(STATISTICS)
+ /* The largest bucket size to be separately counted. Larger buckets
+ * will be listed as "> MR_ROBDD_MAX_COUNT."
+ */
+ #define MR_ROBDD_MAX_COUNT 1000
-/* The largest bucket size to be separately counted. Larger buckets
- * will be listed as "> MAX_COUNT."
- */
-#define MAX_COUNT 1000
+ int MR_ROBDD_unique_table_hits, MR_ROBDD_unique_table_misses;
-int unique_table_hits, unique_table_misses;
+ #define MR_ROBDD_DECLARE_FN_COUNT(op) int op##_count;
-#define DECLARE_FN_COUNT(op) int op##_count;
+ #define MR_ROBDD_COUNT_FN(fn) (++fn##_count)
-#define COUNT_FN(fn) (++fn##_count)
+ #define MR_ROBDD_INIT_FN_COUNT(fn) fn##_count = 0
+ #define MR_ROBDD_PRINT_FN_COUNT(fn) \
+ if (fn##_count!=0) printf("%6d calls to " #fn "\n", 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 MR_ROBDD_COUNT_UNIQUE_HIT (++MR_ROBDD_unique_table_hits)
+ #define MR_ROBDD_COUNT_UNIQUE_MISS (++MR_ROBDD_unique_table_misses)
-#define COUNT_UNIQUE_HIT (++unique_table_hits)
-#define COUNT_UNIQUE_MISS (++unique_table_misses)
+ #if defined(MR_ROBDD_COMPUTED_TABLE)
-#if defined(COMPUTED_TABLE)
+ #define MR_ROBDD_COUNT_HIT(op) (++op##_computed_hits)
+ #define MR_ROBDD_COUNT_MISS(op) (++op##_computed_misses, ++cache->count)
+ #define MR_ROBDD_INIT_CACHE(op) \
+ do { \
+ op##_computed_misses = 0; \
+ op##_computed_hits = 0; \
+ MR_ROBDD_CLEAR_CACHE(op); \
+ } while (0)
-#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); \
+ #define MR_ROBDD_CACHE_COUNT_MEMBER int count;
+ #define MR_ROBDD_PRINT_CACHE_PERFORMANCE(op) \
+ do { \
+ if (op##_computed_misses > 0 ) { \
+ int i, size_count[MR_ROBDD_MAX_COUNT+2]; \
+ printf( \
+ #op " computed table: %d hits, %d misses, %.2f%% hit rate\n",\
+ op##_computed_hits, op##_computed_misses, \
+ MR_ROBDD_PERCENTAGE(op##_computed_hits, \
+ op##_computed_hits + op##_computed_misses)); \
+ MR_memset(size_count, 0, sizeof(size_count)); \
+ for (i=0; i<MR_ROBDD_COMPUTED_TABLE_SIZE; ++i) { \
+ int count = op##_computed_cache[i].count; \
+ ++size_count[(count<=MR_ROBDD_MAX_COUNT ? count : \
+ MR_ROBDD_MAX_COUNT+1)]; \
+ } \
+ MR_ROBDD_print_distribution(size_count, MR_ROBDD_MAX_COUNT); \
+ } \
} 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; i<COMPUTED_TABLE_SIZE; ++i) { \
- int count = op##_computed_cache[i].count; \
- ++size_count[(count<=MAX_COUNT ? count : MAX_COUNT+1)]; \
- } \
- print_distribution(size_count, MAX_COUNT); \
- } \
-} while (0)
-#else /* !COMPUTED_TABLE */
-#define PRINT_CACHE_PERFORMANCE(op)
-#endif /* COMPUTED_TABLE */
-#else /* ! STATISTICS */
-#define DECLARE_FN_COUNT(op)
-#define COUNT_FN(fn)
-#define INIT_FN_COUNT(fn)
-#define PRINT_FN_COUNT(fn)
-#define COUNT_UNIQUE_HIT
-#define COUNT_UNIQUE_MISS
-#define INIT_CACHE(op) CLEAR_CACHE(op)
-#define PRINT_CACHE_PERFORMANCE(op)
-#if defined(COMPUTED_TABLE)
-#define COUNT_HIT(fn)
-#define COUNT_MISS(fn)
-#define CACHE_COUNT_MEMBER
-#endif /* COMPUTED_TABLE */
-#endif /* STATISTICS */
-
-
-#if defined(EQUAL_TEST)
-#define DIRECT_EQUAL_TEST(f,g,result) if ((f) == (g)) return (result)
-#define ELSE_TRY_EQUAL_TEST(f,g,result) \
- else DIRECT_EQUAL_TEST(f,g,result);
-#else /* ! EQUAL_TEST */
-#define DIRECT_EQUAL_TEST(f,g,result)
-#define ELSE_TRY_EQUAL_TEST(f,g,result)
-#endif
+ #else /* !MR_ROBDD_COMPUTED_TABLE */
-#if defined(CLEAR_CACHES)
-#define INIT_UNIQUE_TABLE \
- do { \
- memset(unique_table, 0, sizeof(unique_table)); \
- while (curr_pool!=NULL) { \
- pool *p = curr_pool->prev; \
- free(curr_pool); \
- curr_pool = p; \
- } \
- curr_pool_ptr = curr_pool_end_ptr = NULL; \
- pool_count = 0; \
- } while (0)
-#else /* !CLEAR_CACHES */
-#define INIT_UNIQUE_TABLE
-#endif /* CLEAR_CACHES */
+ #define MR_ROBDD_PRINT_CACHE_PERFORMANCE(op)
+ #endif /* MR_ROBDD_COMPUTED_TABLE */
+#else /* ! MR_ROBDD_STATISTICS */
+ #define MR_ROBDD_DECLARE_FN_COUNT(op)
+ #define MR_ROBDD_COUNT_FN(fn)
+ #define MR_ROBDD_INIT_FN_COUNT(fn)
+ #define MR_ROBDD_PRINT_FN_COUNT(fn)
+ #define MR_ROBDD_COUNT_UNIQUE_HIT
+ #define MR_ROBDD_COUNT_UNIQUE_MISS
+ #define MR_ROBDD_INIT_CACHE(op) MR_ROBDD_CLEAR_CACHE(op)
+ #define MR_ROBDD_PRINT_CACHE_PERFORMANCE(op)
+
+ #if defined(MR_ROBDD_COMPUTED_TABLE)
+ #define MR_ROBDD_COUNT_HIT(fn)
+ #define MR_ROBDD_COUNT_MISS(fn)
+ #define MR_ROBDD_CACHE_COUNT_MEMBER
+ #endif /* MR_ROBDD_COMPUTED_TABLE */
+
+#endif /* MR_ROBDD_STATISTICS */
+
+#if defined(MR_ROBDD_EQUAL_TEST)
+ #define MR_ROBDD_DIRECT_EQUAL_TEST(f,g,result) \
+ if ((f) == (g)) return (result)
+ #define MR_ROBDD_ELSE_TRY_EQUAL_TEST(f,g,result) \
+ else MR_ROBDD_DIRECT_EQUAL_TEST(f,g,result);
+#else /* ! MR_ROBDD_EQUAL_TEST */
+ #define MR_ROBDD_DIRECT_EQUAL_TEST(f,g,result)
+ #define MR_ROBDD_ELSE_TRY_EQUAL_TEST(f,g,result)
+#endif
+
+#if defined(MR_ROBDD_CLEAR_CACHES)
+ #if defined(MR_ROBDD_POOL)
+ #define MR_ROBDD_INIT_UNIQUE_TABLE \
+ do { \
+ MR_memset(MR_ROBDD_unique_table, (char) 0, \
+ sizeof(MR_ROBDD_unique_table)); \
+ while (MR_ROBDD_curr_pool!=NULL) { \
+ pool *p = MR_ROBDD_curr_pool->prev; \
+ free(MR_ROBDD_curr_pool); \
+ MR_ROBDD_curr_pool = p; \
+ } \
+ MR_ROBDD_curr_pool_ptr = MR_ROBDD_curr_pool_end_ptr = NULL; \
+ MR_ROBDD_node_count = 0; \
+ } while (0)
+
+ #else /* !MR_ROBDD_POOL */
+ #define MR_ROBDD_INIT_UNIQUE_TABLE \
+ MR_memset(MR_ROBDD_unique_table, (char) 0, sizeof(MR_ROBDD_unique_table));
+ #endif /* MR_ROBDD_POOL */
+#else /* !MR_ROBDD_CLEAR_CACHES */
+ #define MR_ROBDD_INIT_UNIQUE_TABLE
+#endif /* MR_ROBDD_CLEAR_CACHES */
/********************************************************************
- Caching of computed values
+ Caching of computed values
- For improved efficiency, if COMPUTED_TABLE is defined we maintain a
+ For improved efficiency, if MR_ROBDD_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
@@ -309,2736 +350,3162 @@
********************************************************************/
-#if defined(COMPUTED_TABLE)
+#if defined(MR_ROBDD_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)
+ #if defined(MR_ROBDD_STATISTICS)
+ #define MR_ROBDD_DECLARE_CACHE(op,MR_ROBDD_type) \
+ static int op##_computed_hits; \
+ static int op##_computed_misses; \
+ static MR_ROBDD_type op##_computed_cache[MR_ROBDD_COMPUTED_TABLE_SIZE]
+ #else /* !MR_ROBDD_STATISTICS */
+ #define MR_ROBDD_DECLARE_CACHE(op,MR_ROBDD_type) \
+ static MR_ROBDD_type op##_computed_cache[MR_ROBDD_COMPUTED_TABLE_SIZE]
+ #endif /* MR_ROBDD_STATISTICS */
+
+/********************* the cache for MR_ROBDD_ite **************************/
+
+ #define MR_ROBDD_TERNARY_NODE_HASH(f,g,h) \
+ (((MR_ROBDD_INTCAST(f)>>4)+MR_ROBDD_INTCAST(g)+(MR_ROBDD_INTCAST(h)<<1)) \
+ % MR_ROBDD_COMPUTED_TABLE_SIZE)
+
+ typedef struct {
+ MR_ROBDD_node *f;
+ MR_ROBDD_node *g;
+ MR_ROBDD_node *h;
+ MR_ROBDD_node *result;
+ MR_ROBDD_CACHE_COUNT_MEMBER
+ } ite_cache_entry;
+
+ MR_ROBDD_DECLARE_CACHE(MR_ROBDD_ite, ite_cache_entry);
+ #if defined(MR_ROBDD_USE_ITE_CONSTANT)
+ MR_ROBDD_DECLARE_CACHE(MR_ROBDD_ite_constant, ite_cache_entry);
+ #endif /* MR_ROBDD_USE_ITE_CONSTANT */
+
+ #define MR_ROBDD_DECLARE_ITE_CACHE_ENTRY ite_cache_entry *cache;
+
+ #define MR_ROBDD_TRY_ITE_CACHE(n1,n2,n3,op) \
+ do { \
+ cache = &op##_computed_cache[MR_ROBDD_TERNARY_NODE_HASH(n1,n2,n3)]; \
+ if (cache->f==n1 && cache->g==n2 && cache->h==n3) { \
+ MR_ROBDD_COUNT_HIT(op); \
+ return cache->result; \
+ } \
+ } while (0)
+ #define MR_ROBDD_UPDATE_ITE_CACHE(n1,n2,n3,MR_ROBDD_node,op) \
+ do { \
+ cache->f = n1; \
+ cache->g = n2; \
+ cache->h = n3; \
+ cache->result = MR_ROBDD_node; \
+ MR_ROBDD_COUNT_MISS(op); \
+ } while (0)
/******************** the cache for unary operations ************/
-#define UNARY_NODE_HASH(a) \
- (INTCAST(a) % COMPUTED_TABLE_SIZE)
+ #define MR_ROBDD_UNARY_NODE_HASH(a) \
+ (MR_ROBDD_INTCAST(a) % MR_ROBDD_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)
+ typedef struct {
+ MR_ROBDD_node *f;
+ MR_ROBDD_node *result;
+ MR_ROBDD_CACHE_COUNT_MEMBER
+ } unary_cache_entry;
+
+ #if defined(MR_ROBDD_SHARING)
+ MR_ROBDD_DECLARE_CACHE(MR_ROBDD_upclose, unary_cache_entry);
+ #if defined(MR_ROBDD_NEW)
+ MR_ROBDD_DECLARE_CACHE(MR_ROBDD_complete_one, unary_cache_entry);
+ #endif /* MR_ROBDD_NEW */
+ #endif /* MR_ROBDD_SHARING */
+
+ #define MR_ROBDD_DECLARE_UNARY_CACHE_ENTRY unary_cache_entry *cache;
+
+ #define MR_ROBDD_UPDATE_UNARY_CACHE(n,MR_ROBDD_node,op) \
+ do { \
+ cache->f = n; \
+ cache->result = MR_ROBDD_node; \
+ MR_ROBDD_COUNT_MISS(op); \
+ } while (0)
+ #define MR_ROBDD_TRY_UNARY_CACHE(n,op) \
+ do { \
+ cache = &((op##_computed_cache)[MR_ROBDD_UNARY_NODE_HASH(n)]); \
+ if (cache->f==(n)) { \
+ MR_ROBDD_COUNT_HIT(op); \
+ return cache->result; \
+ } \
+ } while (0)
-/******************** the cache for var_entailed ************/
+/******************** the cache for MR_ROBDD_var_entailed ************/
-#define VAR_ENTAILED_HASH(a,n) \
- ((INTCAST(a)+n) % COMPUTED_TABLE_SIZE)
+ #define MR_ROBDD_VAR_ENTAILED_HASH(a,n) \
+ ((MR_ROBDD_INTCAST(a)+n) % MR_ROBDD_COMPUTED_TABLE_SIZE)
-typedef struct {
- node *f;
+ typedef struct {
+ MR_ROBDD_node *f;
int n;
int result;
- CACHE_COUNT_MEMBER
-} var_entailed_cache_entry;
+ MR_ROBDD_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)
+ #if defined(MR_ROBDD_USE_RGLB)
+ MR_ROBDD_DECLARE_CACHE(MR_ROBDD_var_entailed, var_entailed_cache_entry);
+ #endif /* MR_ROBDD_USE_RGLB */
+
+ #define MR_ROBDD_DECLARE_VAR_ENTAILED_CACHE_ENTRY \
+ var_entailed_cache_entry *cache;
+
+ #define MR_ROBDD_UPDATE_VAR_ENTAILED_CACHE(MR_ROBDD_node,var,val) \
+ do { \
+ cache->f = MR_ROBDD_node; \
+ cache->n = var; \
+ cache->result = val; \
+ MR_ROBDD_COUNT_MISS(MR_ROBDD_var_entailed); \
+ } while (0)
+ #define MR_ROBDD_TRY_VAR_ENTAILED_CACHE(MR_ROBDD_node,var) \
+ do { \
+ cache = &((MR_ROBDD_var_entailed_computed_cache) \
+ [MR_ROBDD_VAR_ENTAILED_HASH(MR_ROBDD_node,var)]); \
+ if (cache->f==(MR_ROBDD_node) && cache->n==(var)) { \
+ MR_ROBDD_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;
+ typedef struct {
+ MR_ROBDD_node *f;
+ MR_ROBDD_bitset result;
+ MR_ROBDD_CACHE_COUNT_MEMBER
+ } unary_bitset_cache_entry;
+
+ #if defined(MR_ROBDD_NEW)
+ MR_ROBDD_DECLARE_CACHE(MR_ROBDD_vars_entailed, unary_bitset_cache_entry);
+ #endif
+
+ #define MR_ROBDD_DECLARE_UNARY_BITSET_CACHE_ENTRY \
+ unary_bitset_cache_entry *cache;
+
+ #define MR_ROBDD_UPDATE_UNARY_BITSET_CACHE(n,set,op) \
+ do { \
+ cache->f = n; \
+ cache->result = set; \
+ MR_ROBDD_COUNT_MISS(op); \
+ } while (0)
-#if defined(NEW)
-DECLARE_CACHE(vars_entailed, unary_bitset_cache_entry);
-#endif
+ #define MR_ROBDD_TRY_UNARY_BITSET_CACHE(n,op) \
+ do { \
+ cache = &((op##_computed_cache)[MR_ROBDD_UNARY_NODE_HASH(n)]); \
+ if (cache->f==(n)) { \
+ MR_ROBDD_COUNT_HIT(op); \
+ return &cache->result; \
+ } \
+ } while (0)
-#define DECLARE_UNARY_BITSET_CACHE_ENTRY \
- unary_bitset_cache_entry *cache;
+/******************** the cache for symmetric binary operations ************/
+/*
+** NB: Since MR_ROBDD_glb and MR_ROBDD_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 MR_ROBDD_TRY_BIN_CACHE.
+** We assume that they won't be changed (or exchanged) before
+** MR_ROBDD_UPDATE_BIN_CACHE is called.
+*/
+
+ #define MR_ROBDD_BINARY_NODE_HASH(a,b) \
+ ((MR_ROBDD_INTCAST(a)+(MR_ROBDD_INTCAST(b)<<1)) % MR_ROBDD_COMPUTED_TABLE_SIZE)
+
+ typedef struct {
+ MR_ROBDD_node *f;
+ MR_ROBDD_node *g;
+ MR_ROBDD_node *result;
+ MR_ROBDD_CACHE_COUNT_MEMBER
+ } bin_cache_entry;
+
+ MR_ROBDD_DECLARE_CACHE(MR_ROBDD_glb, bin_cache_entry);
+ MR_ROBDD_DECLARE_CACHE(MR_ROBDD_lub, bin_cache_entry);
+ #if defined(MR_ROBDD_SHARING)
+ MR_ROBDD_DECLARE_CACHE(MR_ROBDD_bin, bin_cache_entry);
+ MR_ROBDD_DECLARE_CACHE(MR_ROBDD_complete, bin_cache_entry);
+ #endif
+
+ #define MR_ROBDD_DECLARE_BIN_CACHE_ENTRY bin_cache_entry *cache;
+
+ #define MR_ROBDD_UPDATE_BIN_CACHE(n1,n2,MR_ROBDD_node,op) \
+ do { \
+ cache->f = n1; \
+ cache->g = n2; \
+ cache->result = MR_ROBDD_node; \
+ MR_ROBDD_COUNT_MISS(op); \
+ } while (0)
-#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)
+ #define MR_ROBDD_TRY_BIN_CACHE(n1,n2,op) \
+ do { \
+ if (n2 < n1) { \
+ MR_ROBDD_node *temp = (n2); \
+ (n2) = (n1); \
+ (n1) = temp; \
+ } \
+ cache = &((op##_computed_cache)[MR_ROBDD_BINARY_NODE_HASH(n1,n2)]); \
+ if (cache->f==(n1) && cache->g==(n2)) { \
+ MR_ROBDD_COUNT_HIT(op); \
+ return cache->result; \
+ } \
+ } while (0)
+/******************** the cache for asymmetric binary operations ************/
-/******************** the cache for symmetric binary operations ************/
+ #if defined(MR_ROBDD_SHARING) && defined(MR_ROBDD_NEW)
+ MR_ROBDD_DECLARE_CACHE(MR_ROBDD_complete_one_or, bin_cache_entry);
+ #endif /* MR_ROBDD_SHARING && MR_ROBDD_NEW */
+
+ #if defined(MR_ROBDD_USE_THRESH)
+ MR_ROBDD_DECLARE_CACHE(MR_ROBDD_restrictThresh, bin_cache_entry);
+ #endif /* MR_ROBDD_USE_THRESH */
+
+ #if (defined(MR_ROBDD_SHARING) && defined(MR_ROBDD_NEW)) || defined(MR_ROBDD_USE_THRESH)
+
+ #define MR_ROBDD_DECLARE_ASYM_BIN_CACHE_ENTRY bin_cache_entry *cache;
+
+ #define MR_ROBDD_UPDATE_ASYM_BIN_CACHE(n1,n2,MR_ROBDD_node,op) \
+ MR_ROBDD_UPDATE_BIN_CACHE(n1,n2,MR_ROBDD_node,op)
+
+ #define MR_ROBDD_TRY_ASYM_BIN_CACHE(n1,n2,op) \
+ do { \
+ cache = &((op##_computed_cache)[MR_ROBDD_BINARY_NODE_HASH(n1,n2)]); \
+ if (cache->f==(n1) && cache->g==(n2)) { \
+ MR_ROBDD_COUNT_HIT(op); \
+ return cache->result; \
+ } \
+ } while (0)
-/* 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
+ #endif /* (MR_ROBDD_SHARING && MR_ROBDD_NEW) || MR_ROBDD_USE_THRESH */
-#define DECLARE_BIN_CACHE_ENTRY bin_cache_entry *cache;
+/**************************** the cache for rglb ***********************/
-#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)
+ #if defined(MR_ROBDD_USE_RGLB)
-/******************** the cache for asymmetric binary operations ************/
+ typedef struct {
+ MR_ROBDD_node *f;
+ MR_ROBDD_node *g;
+ MR_ROBDD_node *result;
+ int thresh;
+ MR_ROBDD_CACHE_COUNT_MEMBER
+ } rglb_cache_entry;
-#if defined(SHARING) && defined(NEW)
-DECLARE_CACHE(complete_one_or, bin_cache_entry);
+ MR_ROBDD_DECLARE_CACHE(rglb, rglb_cache_entry);
-#define DECLARE_ASYM_BIN_CACHE_ENTRY bin_cache_entry *cache;
+ #define MR_ROBDD_DECLARE_RGLB_CACHE_ENTRY rglb_cache_entry *cache;
-#define UPDATE_ASYM_BIN_CACHE(n1,n2,node,op) \
- UPDATE_BIN_CACHE(n1,n2,node,op)
+ #define MR_ROBDD_TRY_RGLB_CACHE(n1,n2,th) \
+ do { \
+ if (n2 < n1) { \
+ MR_ROBDD_node *temp = (n2); \
+ (n2) = (n1); \
+ (n1) = temp; \
+ } \
+ cache = &rglb_computed_cache[MR_ROBDD_BINARY_NODE_HASH(n1,n2)]; \
+ if (cache->f==(n1) && cache->g==(n2) && \
+ cache->thresh >= th) { \
+ MR_ROBDD_COUNT_HIT(rglb); \
+ if (cache->thresh == th) return cache->result; \
+ return MR_ROBDD_restrictThresh(th, cache->result); \
+ } \
+ } while (0)
-#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 */
+ #define MR_ROBDD_UPDATE_RGLB_CACHE(n1,n2,th,MR_ROBDD_node) \
+ do { \
+ cache->f = n1; \
+ cache->g = n2; \
+ cache->thresh = th; \
+ cache->result = MR_ROBDD_node; \
+ MR_ROBDD_COUNT_MISS(rglb); \
+ } while (0)
-/**************************** the cache for rglb ***********************/
+ #endif /* MR_ROBDD_USE_RGLB */
-#if defined(USE_RGLB)
+/************************ the cache for MR_ROBDD_complete_or *******************/
-typedef struct {
- node *f;
- node *g;
- node *result;
- int thresh;
- CACHE_COUNT_MEMBER
-} rglb_cache_entry;
+ #if defined(MR_ROBDD_SHARING) && defined(MR_ROBDD_NEW)
+ typedef struct {
+ MR_ROBDD_node *f;
+ MR_ROBDD_node *g;
+ MR_ROBDD_node *prev;
+ MR_ROBDD_node *result;
+ MR_ROBDD_CACHE_COUNT_MEMBER
+ } complete_or_cache_entry;
+
+ MR_ROBDD_DECLARE_CACHE(MR_ROBDD_complete_or, complete_or_cache_entry);
+
+ #define MR_ROBDD_DECLARE_COMPLETE_OR_CACHE_ENTRY \
+ complete_or_cache_entry *cache;
+
+ #define MR_ROBDD_TRY_COMPLETE_OR_CACHE(n1,n2,pr) \
+ do { \
+ if (n2 < n1) { \
+ MR_ROBDD_node *temp = (n2); \
+ (n2) = (n1); \
+ (n1) = temp; \
+ } \
+ cache = &complete_or_computed_cache \
+ [MR_ROBDD_TERNARY_NODE_HASH(n1,n2,pr)]; \
+ if ((cache->f==n1 && cache->g==n2 && cache->prev==pr)) { \
+ MR_ROBDD_COUNT_HIT(MR_ROBDD_complete_or); \
+ return cache->result; \
+ } \
+ } while (0)
-DECLARE_CACHE(rglb, rglb_cache_entry);
+ #define MR_ROBDD_UPDATE_COMPLETE_OR_CACHE(n1,n2,pr,MR_ROBDD_node) \
+ do { \
+ cache->f = n1; \
+ cache->g = n2; \
+ cache->prev = pr; \
+ cache->result = MR_ROBDD_node; \
+ MR_ROBDD_COUNT_MISS(MR_ROBDD_complete_or); \
+ } while (0)
-#define DECLARE_RGLB_CACHE_ENTRY rglb_cache_entry *cache;
+ #endif /* MR_ROBDD_SHARING && MR_ROBDD_NEW */
-#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)
+/********************* the cache for MR_ROBDD_ite_var ***********************/
-#endif /* NEW */
+ #if defined(MR_ROBDD_NEW)
+ #define MR_ROBDD_ITE_VAR_COMPUTED_HASH(f,g,h) \
+ ((f+MR_ROBDD_INTCAST(g)+(MR_ROBDD_INTCAST(h)<<1)) \
+ % MR_ROBDD_COMPUTED_TABLE_SIZE)
+
+ typedef struct {
+ int f;
+ MR_ROBDD_node *g;
+ MR_ROBDD_node *h;
+ MR_ROBDD_node *result;
+ MR_ROBDD_CACHE_COUNT_MEMBER
+ } ite_var_cache_entry;
+
+ MR_ROBDD_DECLARE_CACHE(MR_ROBDD_ite_var, ite_var_cache_entry);
+
+ #define MR_ROBDD_DECLARE_ITE_VAR_CACHE_ENTRY ite_var_cache_entry *cache;
+
+ #define MR_ROBDD_TRY_ITE_VAR_CACHE(n1,n2,h) \
+ do { \
+ cache = &MR_ROBDD_ite_var_computed_cache[ \
+ MR_ROBDD_ITE_VAR_COMPUTED_HASH(n1,n2,h)]; \
+ if (cache->f==n1 && cache->g==n2 && cache->h==h) { \
+ MR_ROBDD_COUNT_HIT(MR_ROBDD_ite_var); \
+ return cache->result; \
+ } \
+ } while (0)
+
+ #define MR_ROBDD_UPDATE_ITE_VAR_CACHE(n1,n2,h,MR_ROBDD_node) \
+ do { \
+ cache->f = n1; \
+ cache->g = n2; \
+ cache->h = h; \
+ cache->result = MR_ROBDD_node; \
+ MR_ROBDD_COUNT_MISS(MR_ROBDD_ite_var); \
+ } while (0)
+
+ #endif /* MR_ROBDD_NEW */
+
+#else /* !MR_ROBDD_COMPUTED_TABLE */
-#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 */
+ #define MR_ROBDD_DECLARE_ITE_CACHE_ENTRY
+ #define MR_ROBDD_TRY_ITE_CACHE(n1,n2,n3,op)
+ #define MR_ROBDD_UPDATE_ITE_CACHE(n1,n2,n3,MR_ROBDD_node,op)
+
+ #define MR_ROBDD_DECLARE_UNARY_CACHE_ENTRY
+ #define MR_ROBDD_UPDATE_UNARY_CACHE(n,MR_ROBDD_node,op)
+ #define MR_ROBDD_TRY_UNARY_CACHE(n,op)
+
+ #define MR_ROBDD_DECLARE_VAR_ENTAILED_CACHE_ENTRY
+ #define MR_ROBDD_UPDATE_VAR_ENTAILED_CACHE(MR_ROBDD_node,var,val)
+ #define MR_ROBDD_TRY_VAR_ENTAILED_CACHE(MR_ROBDD_node,var)
+
+ #define MR_ROBDD_DECLARE_UNARY_BITSET_CACHE_ENTRY
+ #define MR_ROBDD_UPDATE_UNARY_BITSET_CACHE(n,set,op)
+ #define MR_ROBDD_TRY_UNARY_BITSET_CACHE(n,op)
+
+ #define MR_ROBDD_DECLARE_BIN_CACHE_ENTRY
+ #define MR_ROBDD_TRY_BIN_CACHE(n1,n2,op)
+ #define MR_ROBDD_UPDATE_BIN_CACHE(n1,n2,MR_ROBDD_node,op)
+
+ #define MR_ROBDD_DECLARE_ASYM_BIN_CACHE_ENTRY
+ #define MR_ROBDD_UPDATE_ASYM_BIN_CACHE(n1,n2,MR_ROBDD_node,op)
+ #define MR_ROBDD_TRY_ASYM_BIN_CACHE(n1,n2,op)
+
+ #define MR_ROBDD_DECLARE_RGLB_CACHE_ENTRY
+ #define MR_ROBDD_TRY_RGLB_CACHE(n1,n2,th)
+ #define MR_ROBDD_UPDATE_RGLB_CACHE(n1,n2,th,MR_ROBDD_node)
+
+ #define MR_ROBDD_DECLARE_COMPLETE_OR_CACHE_ENTRY
+ #define MR_ROBDD_TRY_COMPLETE_OR_CACHE(n1,n2,pr)
+ #define MR_ROBDD_UPDATE_COMPLETE_OR_CACHE(n1,n2,pr,MR_ROBDD_node)
+
+ #define MR_ROBDD_DECLARE_ITE_VAR_CACHE_ENTRY
+ #define MR_ROBDD_TRY_ITE_VAR_CACHE(n1,n2,h)
+ #define MR_ROBDD_UPDATE_ITE_VAR_CACHE(n1,n2,h,MR_ROBDD_node)
+
+ #undef MR_ROBDD_COMPUTED_TABLE_SIZE
+ #define MR_ROBDD_COMPUTED_TABLE_SIZE 0
+#endif /* MR_ROBDD_COMPUTED_TABLE */
/****************************************************************
- The Unique Table
+ The Unique Table
****************************************************************/
+static MR_ROBDD_BRYANT_hidden_node_pointer
+ MR_ROBDD_unique_table[MR_ROBDD_UNIQUE_TABLE_SIZE];
-static node *unique_table[UNIQUE_TABLE_SIZE];
+#define MR_ROBDD_UNIQUE_HASH(var,tr,fa) \
+ (((var)+MR_ROBDD_INTCAST(tr)+(MR_ROBDD_INTCAST(fa)<<1)) \
+ % MR_ROBDD_UNIQUE_TABLE_SIZE)
-#define UNIQUE_HASH(var,tr,fa) \
- (((var)+INTCAST(tr)+(INTCAST(fa)<<1)) % UNIQUE_TABLE_SIZE)
+/****************************************************************
+
+ Prototypes
+ ****************************************************************/
+extern void MR_ROBDD_printBryant(MR_ROBDD_node *a);
+
+/* if then else algorithm */
+MR_ROBDD_node *MR_ROBDD_ite(MR_ROBDD_node *f,MR_ROBDD_node *g,MR_ROBDD_node *h);
+MR_ROBDD_node *MR_ROBDD_restricted_iff_conj_array(int v0, int n, int arr[],
+ int thresh);
+
+MR_ROBDD_node *MR_ROBDD_renameArray(MR_ROBDD_node *in, int count,
+ int mappping[]);
+MR_ROBDD_node *MR_ROBDD_reverseRenameArray(MR_ROBDD_node *in, int count,
+ int rev_mappping[]);
+
+MR_ROBDD_node *MR_ROBDD_complete(MR_ROBDD_node *f, MR_ROBDD_node *g);
+MR_ROBDD_node *MR_ROBDD_bin_univ(MR_ROBDD_node *f);
+
+static int MR_ROBDD_intcompare(const void *i, const void *j);
/****************************************************************
- Prototypes
+ Inline Bit Set Stuff
****************************************************************/
-extern void printBryant(node *a);
+/*
+** MR_ROBDD_next_element()
+** finds the next element in set beginning with var,
+** and updates var, word, and mask to refer to it.
+** MR_ROBDD_prev_element()
+** finds the next earlier element in set.
+** MR_ROBDD_next_nonelement()
+** finds the next potential element of set that is in fact not an element
+** of set.
+** MR_ROBDD_prev_nonelement()
+** finds the next earlier non-element of set.
+**
+** NB: if the initally supplied element is a member of the set,
+** MR_ROBDD_next_element and MR_ROBDD_prev_element will happily return
+** that MR_ROBDD_one. Similarly, MR_ROBDD_next_nonelement and
+** MR_ROBDD_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(MR_ROBDD_NO_CHEAP_SHIFT)
+
+__inline int
+MR_ROBDD_next_element(MR_ROBDD_bitset *set, int *var, int *word,
+ MR_ROBDD_bitmask *mask)
+{
+ int vr = *var;
+ int wd = *word;
+ MR_ROBDD_bitmask f = MR_ROBDD_FOLLOWING_BITS(vr&(MR_ROBDD_BITS_PER_WORD-1));
+ MR_ROBDD_bitmask *ptr = &(set->bits[wd]);
+ MR_ROBDD_bitmask bits = *ptr;
+ MR_ROBDD_bitmask msk = *mask;
+
+ assert(vr >= 0 && vr < MR_ROBDD_MAXVAR);
+
+ if ((bits&f) == 0) {
+ do {
+ if (++wd > ((MR_ROBDD_MAXVAR-1)/MR_ROBDD_BITS_PER_WORD)) return MR_FALSE;
+ } while ((bits=*++ptr) == 0);
+ vr = wd<<MR_ROBDD_LOG_BITS_PER_WORD;
+ msk = 1;
+ }
+ /* I know there's a later bit set in bits, so this is safe */
+ while ((bits&msk) == 0) {
+ ++vr;
+ msk <<= 1;
+ assert(vr < (wd+1)<<MR_ROBDD_LOG_BITS_PER_WORD);
+ }
+ *var = vr;
+ *word = wd;
+ *mask = msk;
+ return MR_TRUE;
+}
-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);
+#else /* !MR_ROBDD_NO_CHEAP_SHIFT */
+__inline int
+MR_ROBDD_next_element(MR_ROBDD_bitset *set, int *var, int *word,
+ MR_ROBDD_bitmask *mask)
+{
+ int vr = *var;
+ int wd = *word;
+ MR_ROBDD_bitmask *ptr = &(set->bits[wd]);
+ MR_ROBDD_bitmask bits = *ptr&MR_ROBDD_FOLLOWING_BITS(vr&(MR_ROBDD_BITS_PER_WORD-1));
+
+ assert(vr >= 0 && vr < MR_ROBDD_MAXVAR);
+
+ while (bits == 0) {
+ if (++wd > (MR_ROBDD_MAXVAR-1)/MR_ROBDD_BITS_PER_WORD) return MR_FALSE;
+ bits = *++ptr;
+ }
+ vr = wd<<MR_ROBDD_LOG_BITS_PER_WORD;
+ /* I know there's a later bit set in bits, so this is safe */
+ while ((bits & MR_ROBDD_CHAR_MASK) == 0) {
+ bits >>= MR_ROBDD_BITS_PER_CHAR;
+ vr += MR_ROBDD_BITS_PER_CHAR;
+ assert(vr < (wd+1)<<MR_ROBDD_LOG_BITS_PER_WORD);
+ }
+ vr += MR_ROBDD_first_one_bit[bits & MR_ROBDD_CHAR_MASK];
+
+ *var = vr;
+ *word = wd;
+ *mask = 1<<(vr&(MR_ROBDD_BITS_PER_WORD-1));
+ return MR_TRUE;
+}
-node *renameArray(node *in, int count, int mappping[]);
-node *reverseRenameArray(node *in, int count, int rev_mappping[]);
+#endif /* MR_ROBDD_NO_CHEAP_SHIFT */
-node *complete(node *f, node *g);
-node *bin_univ(node *f);
+#if defined(MR_ROBDD_NO_CHEAP_SHIFT)
-static int intcompare(const void *i, const void *j);
+__inline int
+MR_ROBDD_prev_element(MR_ROBDD_bitset *set, int *var, int *word,
+ MR_ROBDD_bitmask *mask)
+{
+ int vr = *var;
+ int wd = *word;
+
+ assert(vr >= 0 && vr < MR_ROBDD_MAXVAR);
+
+ MR_ROBDD_bitmask f = MR_ROBDD_PRECEDING_BITS(vr&(MR_ROBDD_BITS_PER_WORD-1));
+ MR_ROBDD_bitmask *ptr = &(set->bits[wd]);
+ MR_ROBDD_bitmask bits = *ptr;
+ MR_ROBDD_bitmask msk = *mask;
+
+ if ((bits&f) == 0) {
+ do {
+ if (--wd < 0) {
+ return MR_FALSE;
+ }
+ } while ((bits=*--ptr) == 0);
+ vr = (wd<<MR_ROBDD_LOG_BITS_PER_WORD) + MR_ROBDD_BITS_PER_WORD-1;
+ msk = 1<<(MR_ROBDD_BITS_PER_WORD-1);
+ }
+ /* I know there's an earlier bit set in bits, so this is safe */
+ while ((bits&msk) == 0) {
+ --vr;
+ msk >>= 1;
+ assert(vr >= 0);
+ }
+ *var = vr;
+ *word = wd;
+ *mask = msk;
+ return MR_TRUE;
+}
-/****************************************************************
+#else /* !MR_ROBDD_NO_CHEAP_SHIFT */
- Inline Bit Set Stuff
+__inline int
+MR_ROBDD_prev_element(MR_ROBDD_bitset *set, int *var, int *word,
+ MR_ROBDD_bitmask *mask)
+{
+ int vr = *var;
+ int wd = *word;
+ MR_ROBDD_bitmask *ptr = &(set->bits[wd]);
+ MR_ROBDD_bitmask bits = *ptr&MR_ROBDD_PRECEDING_BITS(vr&(MR_ROBDD_BITS_PER_WORD-1));
+ MR_ROBDD_bitmask temp;
+
+ assert(vr >= 0 && vr < MR_ROBDD_MAXVAR);
+
+ while (bits == 0) {
+ if (--wd < 0) {
+ return MR_FALSE;
+ }
+ bits = *--ptr;
+ }
- ****************************************************************/
+ vr = MR_ROBDD_BITS_PER_WORD - MR_ROBDD_BITS_PER_CHAR;
+ /* I know there's an earlier bit set in bits, so this is safe */
+ while ((temp=((bits>>vr)&MR_ROBDD_CHAR_MASK)) == 0) {
+ vr -= MR_ROBDD_BITS_PER_CHAR;
+ assert(vr >= 0);
+ }
+ vr += (int)MR_ROBDD_last_one_bit[(int)temp];
+ vr += (int)wd<<MR_ROBDD_LOG_BITS_PER_WORD;
+
+ *var = vr;
+ *word = wd;
+ *mask = 1<<(vr&(MR_ROBDD_BITS_PER_WORD-1));
+ return MR_TRUE;
+}
-/* 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<<LOG_BITS_PER_WORD;
- msk = 1;
- }
- /* I know there's a later bit set in bits, so this is safe */
- while ((bits&msk) == 0) {
- ++vr;
- msk <<= 1;
- assert(vr < (wd+1)<<LOG_BITS_PER_WORD);
- }
- *var = vr;
- *word = wd;
- *mask = msk;
- return TRUE;
- }
-#else /* !NO_CHEAP_SHIFT */
-__inline int next_element(bitset *set, int *var, int *word, bitmask *mask)
- {
- int vr = *var;
- int wd = *word;
- bitmask *ptr = &(set->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<<LOG_BITS_PER_WORD;
- /* I know there's a later bit set in bits, so this is safe */
- while ((bits & CHAR_MASK) == 0) {
- bits >>= BITS_PER_CHAR;
- vr += BITS_PER_CHAR;
- assert(vr < (wd+1)<<LOG_BITS_PER_WORD);
- }
- vr += first_one_bit[bits & CHAR_MASK];
-
- *var = vr;
- *word = wd;
- *mask = 1<<(vr&(BITS_PER_WORD-1));
- return TRUE;
- }
-#endif /* NO_CHEAP_SHIFT */
-
-
-#if defined(NO_CHEAP_SHIFT)
-__inline int prev_element(bitset *set, int *var, int *word, bitmask *mask)
- {
- int vr = *var;
- int wd = *word;
-
- assert(vr >= 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<<LOG_BITS_PER_WORD) + BITS_PER_WORD-1;
- msk = 1<<(BITS_PER_WORD-1);
- }
- /* I know there's an earlier bit set in bits, so this is safe */
- while ((bits&msk) == 0) {
- --vr;
- msk >>= 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<<LOG_BITS_PER_WORD;
-
- *var = vr;
- *word = wd;
- *mask = 1<<(vr&(BITS_PER_WORD-1));
- return TRUE;
- }
-#endif /* NO_CHEAP_SHIFT */
-
-
-__inline int next_nonelement(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) == f) {
- do {
- if (++wd >= MAXVAR/BITS_PER_WORD) return FALSE;
- } while ((bits=*++ptr) == ~0);
- vr = wd<<LOG_BITS_PER_WORD;
- msk = 1;
- }
- /* I know there's a later bit clear in bits, so this is safe */
- while ((bits&msk) != 0) {
- ++vr;
- msk <<= 1;
- }
- *var = vr;
- *word = wd;
- *mask = msk;
- return TRUE;
- }
-
-
-__inline int prev_nonelement(bitset *set, int *var, int *word, bitmask *mask)
- {
- int vr = *var;
- int wd = *word;
- bitmask f = PRECEDING_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) == f) {
- do {
- if (--wd < 0) return FALSE;
- } while ((bits=*--ptr) == ~0);
- vr = (wd<<LOG_BITS_PER_WORD) + BITS_PER_WORD-1;
- msk = 1<<(BITS_PER_WORD-1);
- }
- /* I know there's an earlier bit clear in bits, so this is safe */
- while ((bits&msk) != 0) {
- --vr;
- msk >>= 1;
- }
- *var = vr;
- *word = wd;
- *mask = msk;
- return TRUE;
- }
+#endif /* MR_ROBDD_NO_CHEAP_SHIFT */
+__inline int
+MR_ROBDD_next_nonelement(MR_ROBDD_bitset *set, int *var, int *word,
+ MR_ROBDD_bitmask *mask)
+{
+ int vr = *var;
+ int wd = *word;
+ MR_ROBDD_bitmask f = MR_ROBDD_FOLLOWING_BITS(vr&(MR_ROBDD_BITS_PER_WORD-1));
+ MR_ROBDD_bitmask *ptr = &(set->bits[wd]);
+ MR_ROBDD_bitmask bits = *ptr;
+ MR_ROBDD_bitmask msk = *mask;
+
+ assert(vr >= 0 && vr < MR_ROBDD_MAXVAR);
+
+ if ((bits&f) == f) {
+ do {
+ if (++wd >= MR_ROBDD_MAXVAR/MR_ROBDD_BITS_PER_WORD) {
+ return MR_FALSE;
+ }
+ } while ((bits=*++ptr) == ~0);
+ vr = wd<<MR_ROBDD_LOG_BITS_PER_WORD;
+ msk = 1;
+ }
+ /* I know there's a later bit clear in bits, so this is safe */
+ while ((bits&msk) != 0) {
+ ++vr;
+ msk <<= 1;
+ }
+ *var = vr;
+ *word = wd;
+ *mask = msk;
+ return MR_TRUE;
+}
+__inline int
+MR_ROBDD_prev_nonelement(MR_ROBDD_bitset *set, int *var, int *word,
+ MR_ROBDD_bitmask *mask)
+{
+ int vr = *var;
+ int wd = *word;
+ MR_ROBDD_bitmask f = MR_ROBDD_PRECEDING_BITS(vr&(MR_ROBDD_BITS_PER_WORD-1));
+ MR_ROBDD_bitmask *ptr = &(set->bits[wd]);
+ MR_ROBDD_bitmask bits = *ptr;
+ MR_ROBDD_bitmask msk = *mask;
+
+ assert(vr >= 0 && vr < MR_ROBDD_MAXVAR);
+
+ if ((bits&f) == f) {
+ do {
+ if (--wd < 0) {
+ return MR_FALSE;
+ }
+ } while ((bits=*--ptr) == ~0);
+ vr = (wd<<MR_ROBDD_LOG_BITS_PER_WORD) + MR_ROBDD_BITS_PER_WORD-1;
+ msk = 1<<(MR_ROBDD_BITS_PER_WORD-1);
+ }
+ /* I know there's an earlier bit clear in bits, so this is safe */
+ while ((bits&msk) != 0) {
+ --vr;
+ msk >>= 1;
+ }
+ *var = vr;
+ *word = wd;
+ *mask = msk;
+ return MR_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;
- }
-
+__inline int
+MR_ROBDD_bitset_equal(MR_ROBDD_bitset *set1, MR_ROBDD_bitset *set2);
+
+__inline int
+MR_ROBDD_bitset_equal(MR_ROBDD_bitset *set1, MR_ROBDD_bitset *set2)
+{
+ MR_ROBDD_bitmask *ptr1 = &set1->bits[0];
+ MR_ROBDD_bitmask *ptr2 = &set2->bits[0];
+ MR_ROBDD_bitmask *ptr1end =
+ &set1->bits[((MR_ROBDD_MAXVAR-1)/MR_ROBDD_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;
- }
- }
+__inline int
+MR_ROBDD_bitset_disjoint(MR_ROBDD_bitset *set1, MR_ROBDD_bitset *set2);
+__inline int
+MR_ROBDD_bitset_disjoint(MR_ROBDD_bitset *set1, MR_ROBDD_bitset *set2)
+{
+ MR_ROBDD_bitmask *ptr1 = &set1->bits[0];
+ MR_ROBDD_bitmask *ptr2 = &set2->bits[0];
+ MR_ROBDD_bitmask *ptr1end =
+ &set1->bits[((MR_ROBDD_MAXVAR-1)/MR_ROBDD_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;
- }
-
- }
+__inline int
+MR_ROBDD_bitset_subset(MR_ROBDD_bitset *set1, MR_ROBDD_bitset *set2);
+__inline int
+MR_ROBDD_bitset_subset(MR_ROBDD_bitset *set1, MR_ROBDD_bitset *set2)
+{
+ MR_ROBDD_bitmask *ptr1 = &set1->bits[0];
+ MR_ROBDD_bitmask *ptr2 = &set2->bits[0];
+ MR_ROBDD_bitmask *ptr1end =
+ &set1->bits[((MR_ROBDD_MAXVAR-1)/MR_ROBDD_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;
- }
-
- }
+__inline int MR_ROBDD_bitset_empty(MR_ROBDD_bitset *set);
+__inline int MR_ROBDD_bitset_empty(MR_ROBDD_bitset *set)
+{
+ MR_ROBDD_bitmask *ptr = &set->bits[0];
+ MR_ROBDD_bitmask *ptrend =
+ &set->bits[((MR_ROBDD_MAXVAR-1)/MR_ROBDD_BITS_PER_WORD)+1];
+
+ for (;;) {
+ if ((*ptr) != 0) {
+ return 0;
+ }
+ if (++ptr >= ptrend) {
+ return 1;
+ }
+ }
+}
/****************************************************************
- Making Nodes
+ 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;
+#if defined(MR_ROBDD_BRYANT_CONSERVATIVE_GC)
+
+static int MR_ROBDD_removed_nodes = 0;
+
+void MR_ROBDD_remove_node(GC_PTR obj, GC_PTR client_data);
+void MR_ROBDD_remove_node(GC_PTR obj, GC_PTR client_data)
+{
+ MR_ROBDD_node *n = (MR_ROBDD_node *) obj;
+ MR_ROBDD_BRYANT_hidden_node_pointer *bucket =
+ (MR_ROBDD_BRYANT_hidden_node_pointer *) client_data;
+
+ if (MR_ROBDD_REVEAL_NODE_POINTER(n->unique) != NULL) {
+ MR_ROBDD_REVEAL_NODE_POINTER(n->unique)->uprev = n->uprev;
}
-/* 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);
+ if (MR_ROBDD_REVEAL_NODE_POINTER(n->uprev) != NULL) {
+ MR_ROBDD_REVEAL_NODE_POINTER(n->uprev)->unique = n->unique;
}
+ if (MR_ROBDD_REVEAL_NODE_POINTER(*bucket) == n) {
+ *bucket = n->unique;
+ }
-DECLARE_FN_COUNT(make_node)
+ MR_ROBDD_removed_nodes++;
+}
-node *make_node(int var, node *tr, node *fa)
- {
- node **bucket;
- node *ptr;
+#endif /* MR_ROBDD_BRYANT_CONSERVATIVE_GC */
- assert(var>=0);
- assert(var<MAXVAR);
- assert(IS_TERMINAL(tr) || tr->value > var);
- assert(IS_TERMINAL(fa) || fa->value > var);
+#if defined(MR_ROBDD_POOL)
+ static pool *MR_ROBDD_curr_pool = NULL;
+ static MR_ROBDD_node *MR_ROBDD_curr_pool_ptr = NULL;
+ static MR_ROBDD_node *MR_ROBDD_curr_pool_end_ptr = NULL;
+#endif /* MR_ROBDD_POOL */
+
+static int MR_ROBDD_node_count = 0;
+
+static MR_ROBDD_node *
+MR_ROBDD_alloc_node(int value, MR_ROBDD_node* tr, MR_ROBDD_node* fa,
+ MR_ROBDD_BRYANT_hidden_node_pointer *bucket)
+{
+ MR_ROBDD_node *n;
+#if defined(MR_ROBDD_POOL)
+ pool *newpool;
+
+ if (MR_ROBDD_curr_pool_ptr >= MR_ROBDD_curr_pool_end_ptr) {
+ /* allocate a new pool */
+ newpool = (pool *) malloc(sizeof(pool));
+ newpool->prev = MR_ROBDD_curr_pool;
+ MR_ROBDD_curr_pool = newpool;
+ MR_ROBDD_curr_pool_ptr = &(newpool->data[0]);
+ MR_ROBDD_curr_pool_end_ptr = &(newpool->data[MR_ROBDD_POOL_SIZE]);
+ }
+ n = MR_ROBDD_curr_pool_ptr++;
+#else /* !MR_ROBDD_POOL */
+ n = (MR_ROBDD_node *) malloc(sizeof(MR_ROBDD_node));
+ #if defined(MR_ROBDD_BRYANT_CONSERVATIVE_GC)
+ GC_register_finalizer(n, MR_ROBDD_remove_node, bucket, 0, 0);
+ #endif
+#endif /* MR_ROBDD_POOL */
+ MR_ROBDD_node_count++;
+ n->value = value;
+ n->tr = tr;
+ n->fa = fa;
+ return n;
+}
+
+/* return the number of graph nodes that have been created. */
+int
+MR_ROBDD_nodes_in_use(void)
+{
+ return MR_ROBDD_node_count;
+}
- COUNT_FN(make_node);
+MR_ROBDD_DECLARE_FN_COUNT(MR_ROBDD_make_node)
- if (tr == fa) return tr;
+MR_ROBDD_node *
+MR_ROBDD_make_node(int var, MR_ROBDD_node *tr, MR_ROBDD_node *fa)
+{
+ MR_ROBDD_BRYANT_hidden_node_pointer *bucket;
+ MR_ROBDD_node *ptr;
- 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;
+ assert(var>=0);
+ assert(var<MR_ROBDD_MAXVAR);
+ assert(MR_ROBDD_IS_TERMINAL(tr) || tr->value > var);
+ assert(MR_ROBDD_IS_TERMINAL(fa) || fa->value > var);
- if (ptr!=NULL) {
- COUNT_UNIQUE_HIT;
- return ptr;
- }
+ MR_ROBDD_COUNT_FN(MR_ROBDD_make_node);
- /* 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;
+ if (tr == fa) {
+ return tr;
}
+ bucket = &MR_ROBDD_unique_table[MR_ROBDD_UNIQUE_HASH(var,tr,fa)];
-void free_rep(node *n)
- {
- /* never free ROBDD nodes */
+ /*
+ ** The following check avoids the need to initialise the table
+ ** elements to MR_ROBDD_HIDE_POINTER(NULL).
+ */
+ if (*bucket == 0) {
+ *bucket = MR_ROBDD_HIDE_POINTER(NULL);
}
+ ptr = MR_ROBDD_REVEAL_NODE_POINTER(*bucket);
+ while (ptr != NULL && (var!=ptr->value || tr!=ptr->tr || fa!=ptr->fa)) {
+ ptr = MR_ROBDD_REVEAL_NODE_POINTER(ptr->unique);
+ }
+ if (ptr != NULL) {
+ MR_ROBDD_COUNT_UNIQUE_HIT;
+ return ptr;
+ }
+
+ /* MR_ROBDD_node doesn't exist so create it and put in bucket */
+ MR_ROBDD_COUNT_UNIQUE_MISS;
+ ptr = MR_ROBDD_alloc_node(var, tr, fa, bucket);
+ ptr->unique = *bucket;
+ *bucket = MR_ROBDD_HIDE_POINTER(ptr);
+#ifdef MR_ROBDD_BRYANT_CONSERVATIVE_GC
+ ptr->uprev = MR_ROBDD_HIDE_POINTER(NULL);
+ if (MR_ROBDD_REVEAL_NODE_POINTER(ptr->unique) != NULL) {
+ MR_ROBDD_REVEAL_NODE_POINTER(ptr->unique)->uprev =
+ MR_ROBDD_HIDE_POINTER(ptr);
+ }
+#endif
+ return ptr;
+}
+
+void
+MR_ROBDD_free_rep(MR_ROBDD_node *n)
+{
+ /* never free ROBDD nodes */
+}
/****************************************************************
- The Basic Algorithms
+ The Basic Algorithms
****************************************************************/
-int max_variable(void)
- {
- return MAXVAR;
- }
+int MR_ROBDD_max_variable(void);
+int
+MR_ROBDD_max_variable(void)
+{
+ return MR_ROBDD_MAXVAR;
+}
+
+MR_ROBDD_node *
+MR_ROBDD_trueVar(void)
+{
+ return MR_ROBDD_one;
+}
+
+MR_ROBDD_node *
+MR_ROBDD_falseVar(void)
+{
+ return MR_ROBDD_zero;
+}
+
+MR_ROBDD_DECLARE_FN_COUNT(MR_ROBDD_variableRep)
+
+MR_ROBDD_node *
+MR_ROBDD_variableRep(int var)
+{
+ MR_ROBDD_COUNT_FN(MR_ROBDD_variableRep);
+ return MR_ROBDD_make_node(var,MR_ROBDD_one,MR_ROBDD_zero);
+}
+
+MR_ROBDD_DECLARE_FN_COUNT(MR_ROBDD_ite)
-node *trueVar(void)
- {
- return one;
+MR_ROBDD_node *
+MR_ROBDD_ite(MR_ROBDD_node *f,MR_ROBDD_node *g,MR_ROBDD_node *h)
+{
+ MR_ROBDD_node *f_tr, *f_fa;
+ MR_ROBDD_node *g_tr, *g_fa;
+ MR_ROBDD_node *h_tr, *h_fa;
+ MR_ROBDD_node *newnode;
+ int top;
+ MR_ROBDD_DECLARE_ITE_CACHE_ENTRY
+
+ MR_ROBDD_COUNT_FN(MR_ROBDD_ite);
+ /* terminal cases */
+ if (f == MR_ROBDD_one) {
+ return g;
+ }
+ if (f == MR_ROBDD_zero) {
+ return h;
+ }
+ if ((g == MR_ROBDD_one) && (h == MR_ROBDD_zero)) {
+ return f;
+ }
+ if (g == h) {
+ return g;
+ }
+
+ /* look it up in computed table; finished if found */
+ MR_ROBDD_TRY_ITE_CACHE(f, g, h, MR_ROBDD_ite);
+
+ /* find top variable */
+ top = f->value; /* we know f is not terminal */
+ if (!MR_ROBDD_IS_TERMINAL(g) && (g->value < top)) {
+ top = g->value;
}
+ if (!MR_ROBDD_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 (!MR_ROBDD_IS_TERMINAL(g) && g->value==top) {
+ g_tr = g->tr; g_fa = g->fa;
+ } else {
+ g_tr = g; g_fa = g;
+ }
+ if (!MR_ROBDD_IS_TERMINAL(h) && h->value==top) {
+ h_tr = h->tr; h_fa = h->fa;
+ } else {
+ h_tr = h; h_fa = h;
+ }
+
+ /* create new MR_ROBDD_node and add to table */
+ newnode = MR_ROBDD_make_node(top,
+ MR_ROBDD_ite(f_tr, g_tr, h_tr),
+ MR_ROBDD_ite(f_fa, g_fa, h_fa));
+ MR_ROBDD_UPDATE_ITE_CACHE(f,g,h,newnode,MR_ROBDD_ite);
+ return newnode;
+}
+#if defined(MR_ROBDD_USE_ITE_CONSTANT)
-node *falseVar(void)
- {
- return zero;
+/*
+** This is sort of an "approximate MR_ROBDD_ite()." It returns MR_ROBDD_zero
+** or MR_ROBDD_one if that's what MR_ROBDD_ite() would do. Otherwise it just
+** returns the pseudo-MR_ROBDD_node `MR_ROBDD_nonterminal' or some real
+** MR_ROBDD_node. In any case, it does not create any new nodes.
+*/
+
+MR_ROBDD_node *
+MR_ROBDD_ite_constant(MR_ROBDD_node *f,MR_ROBDD_node *g,MR_ROBDD_node *h)
+{
+ MR_ROBDD_node *f_tr, *f_fa;
+ MR_ROBDD_node *g_tr, *g_fa;
+ MR_ROBDD_node *h_tr, *h_fa;
+ MR_ROBDD_node *tr_part, *fa_part;
+ MR_ROBDD_node *result;
+ int top;
+ MR_ROBDD_DECLARE_ITE_CACHE_ENTRY
+
+ MR_ROBDD_COUNT_FN(MR_ROBDD_ite);
+ /* terminal cases */
+ if (f == MR_ROBDD_one) {
+ return g;
+ }
+ if (f == MR_ROBDD_zero) {
+ return h;
+ }
+ if (g == h) {
+ return g;
+ }
+ if (MR_ROBDD_IS_TERMINAL(g) && MR_ROBDD_IS_TERMINAL(h)) {
+ /* either f or ~f, which is MR_ROBDD_nonterminal since f is */
+ return MR_ROBDD_nonterminal;
+ }
+
+ /* look it up in computed table; finished if found */
+ MR_ROBDD_TRY_ITE_CACHE(f, g, h, MR_ROBDD_ite_constant);
+
+ /* find top variable */
+ top = f->value; /* we know f is not terminal */
+ if (!MR_ROBDD_IS_TERMINAL(g) && (g->value < top)) {
+ top = g->value;
+ }
+ if (!MR_ROBDD_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 (!MR_ROBDD_IS_TERMINAL(g) && g->value==top) {
+ g_tr = g->tr; g_fa = g->fa;
+ } else {
+ g_tr = g; g_fa = g;
+ }
+ if (!MR_ROBDD_IS_TERMINAL(h) && h->value==top) {
+ h_tr = h->tr; h_fa = h->fa;
+ } else {
+ h_tr = h; h_fa = h;
}
+ tr_part = MR_ROBDD_ite_constant(f_tr, g_tr, h_tr);
+ fa_part = MR_ROBDD_ite_constant(f_fa, g_fa, h_fa);
+ if (tr_part == fa_part) {
+ result = tr_part;
+ } else {
+ result = MR_ROBDD_nonterminal;
+ }
+
+ MR_ROBDD_UPDATE_ITE_CACHE(f,g,h,result,MR_ROBDD_ite_constant);
+ return result;
+}
+#endif /* MR_ROBDD_USE_ITE_CONSTANT */
+
+MR_ROBDD_DECLARE_FN_COUNT(MR_ROBDD_implies)
+
+MR_ROBDD_node *
+MR_ROBDD_implies(MR_ROBDD_node *a, MR_ROBDD_node *b)
+{
+ MR_ROBDD_COUNT_FN(MR_ROBDD_implies);
+ return MR_ROBDD_ite(a,b,MR_ROBDD_one);
+}
+
+/* returns a copy of graph a */
+
+MR_ROBDD_node *
+MR_ROBDD_copy(MR_ROBDD_node *a)
+{
+ return a;
+}
-DECLARE_FN_COUNT(variableRep)
+/* returns true if graph a and b are equiv */
-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<n; ++i) {
- result = glb(result, variableRep(arr[i]));
- }
- return result;
- }
-#else /* !NAIVE */
-node *glb_array(int n, int arr[])
- {
- int i;
- node *result = one;
-
- qsort((char *)arr, n, sizeof(int), intcompare);
- for (i=n-1; i>=0; --i) {
- result = make_node(arr[i], result, zero);
- }
- return result;
+int
+MR_ROBDD_equiv(MR_ROBDD_node *a, MR_ROBDD_node *b)
+{
+ return (a == b);
+}
+
+MR_ROBDD_DECLARE_FN_COUNT(MR_ROBDD_lub)
+MR_ROBDD_DECLARE_FN_COUNT(MR_ROBDD_glb)
+
+#if defined(MR_ROBDD_NAIVE)
+MR_ROBDD_node *
+MR_ROBDD_glb(MR_ROBDD_node *a, MR_ROBDD_node *b)
+{
+ MR_ROBDD_COUNT_FN(MR_ROBDD_glb);
+ return MR_ROBDD_ite(a,b,MR_ROBDD_zero);
+}
+
+MR_ROBDD_node *
+MR_ROBDD_lub(MR_ROBDD_node *a, MR_ROBDD_node *b)
+{
+ MR_ROBDD_COUNT_FN(MR_ROBDD_lub);
+ return MR_ROBDD_ite(a,MR_ROBDD_one,b);
+}
+
+#else /* !MR_ROBDD_NAIVE */
+
+MR_ROBDD_node *
+MR_ROBDD_lub(MR_ROBDD_node *f, MR_ROBDD_node *g)
+{
+ MR_ROBDD_COUNT_FN(MR_ROBDD_lub);
+ if (MR_ROBDD_IS_TERMINAL(f)) {
+ return f == MR_ROBDD_one ? MR_ROBDD_one : g;
+ } else if (MR_ROBDD_IS_TERMINAL(g)) {
+ return g == MR_ROBDD_one ? MR_ROBDD_one : f;
+ } MR_ROBDD_ELSE_TRY_EQUAL_TEST(f,g,f)
+ else {
+ MR_ROBDD_node *result;
+ MR_ROBDD_DECLARE_BIN_CACHE_ENTRY
+
+ MR_ROBDD_TRY_BIN_CACHE(f, g, MR_ROBDD_lub);
+
+ if (f->value < g->value) {
+ result = MR_ROBDD_make_node(f->value,
+ MR_ROBDD_lub(f->tr, g), MR_ROBDD_lub(f->fa, g));
+ } else if (f->value > g->value) {
+ result = MR_ROBDD_make_node(g->value,
+ MR_ROBDD_lub(f, g->tr), MR_ROBDD_lub(f, g->fa));
+ } else /* f->value == g->value */{
+ result = MR_ROBDD_make_node(f->value,
+ MR_ROBDD_lub(f->tr, g->tr), MR_ROBDD_lub(f->fa, g->fa));
+ }
+ MR_ROBDD_UPDATE_BIN_CACHE(f, g, result, MR_ROBDD_lub);
+ return result;
}
-#endif /* NAIVE */
+}
+
+MR_ROBDD_node *
+MR_ROBDD_glb(MR_ROBDD_node *f, MR_ROBDD_node *g)
+{
+ MR_ROBDD_COUNT_FN(MR_ROBDD_glb);
+ if (MR_ROBDD_IS_TERMINAL(f)) {
+ return f == MR_ROBDD_one ? g : MR_ROBDD_zero;
+ } else if (MR_ROBDD_IS_TERMINAL(g)) {
+ return g == MR_ROBDD_one ? f : MR_ROBDD_zero;
+ } MR_ROBDD_ELSE_TRY_EQUAL_TEST(f,g,f)
+ else {
+ MR_ROBDD_node *result;
+ MR_ROBDD_DECLARE_BIN_CACHE_ENTRY
+
+ MR_ROBDD_TRY_BIN_CACHE(f, g, MR_ROBDD_glb);
+
+ if (f->value < g->value) {
+ result = MR_ROBDD_make_node(f->value,
+ MR_ROBDD_glb(f->tr, g), MR_ROBDD_glb(f->fa, g));
+ } else if (f->value > g->value) {
+ result = MR_ROBDD_make_node(g->value,
+ MR_ROBDD_glb(f, g->tr), MR_ROBDD_glb(f, g->fa));
+ } else /* f->value == g->value */{
+ result = MR_ROBDD_make_node(f->value,
+ MR_ROBDD_glb(f->tr, g->tr), MR_ROBDD_glb(f->fa, g->fa));
+ }
+ MR_ROBDD_UPDATE_BIN_CACHE(f, g, result, MR_ROBDD_glb);
+ return result;
+ }
+}
+
+#endif /* MR_ROBDD_NAIVE */
+
+#if defined(MR_ROBDD_NAIVE)
+
+MR_ROBDD_node *
+MR_ROBDD_glb_array(int n, int arr[])
+{
+ int i;
+ MR_ROBDD_node *result = MR_ROBDD_one;
+
+ for (i = 0; i < n; ++i) {
+ result = MR_ROBDD_glb(result, MR_ROBDD_variableRep(arr[i]));
+ }
+ return result;
+}
+
+#else /* !MR_ROBDD_NAIVE */
+
+MR_ROBDD_node *
+MR_ROBDD_glb_array(int n, int arr[])
+{
+ int i;
+ MR_ROBDD_node *result = MR_ROBDD_one;
+
+ qsort((char *)arr, n, sizeof(int), MR_ROBDD_intcompare);
+ for (i = n-1; i >= 0; --i) {
+ result = MR_ROBDD_make_node(arr[i], result, MR_ROBDD_zero);
+ }
+ return result;
+}
+
+#endif /* MR_ROBDD_NAIVE */
/****************************************************************
- Restriction (Projection, Existential Quantification)
+ Restriction (Projection, Existential Quantification)
****************************************************************/
-DECLARE_FN_COUNT(restrict)
+MR_ROBDD_DECLARE_FN_COUNT(MR_ROBDD_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);
- }
+MR_ROBDD_node *
+MR_ROBDD_restrict(int c, MR_ROBDD_node *f)
+{
+ MR_ROBDD_COUNT_FN(MR_ROBDD_restrict);
+ if (MR_ROBDD_IS_TERMINAL(f) || (f->value > c)) {
+ return f;
+ } else if (f->value < c) {
+ return MR_ROBDD_make_node(f->value,
+ MR_ROBDD_restrict(c,f->tr), MR_ROBDD_restrict(c,f->fa));
+ } else {
+ return MR_ROBDD_lub(f->tr, f->fa);
+ }
+}
+
+MR_ROBDD_DECLARE_FN_COUNT(MR_ROBDD_restrictThresh)
+
+#if !defined(MR_ROBDD_USE_THRESH) && !defined(MR_ROBDD_RESTRICT_SET)
+MR_ROBDD_node *
+MR_ROBDD_restrictThresh(int lo, int hi, MR_ROBDD_node *a)
+{
+ int i;
+
+ MR_ROBDD_COUNT_FN(MR_ROBDD_restrictThresh);
+ for(i = lo+1; i <= hi; ++i) {
+ a = MR_ROBDD_restrict(i, a);
+ }
+ return a;
+}
+
+#elif !defined(MR_ROBDD_USE_THRESH) /* && defined(MR_ROBDD_RESTRICT_SET) */
+
+/*
+** union vars with the set of all variables greater than thresh appearing in
+** the ROBDD rooted at f.
+*/
+
+static void
+MR_ROBDD_vars_present(MR_ROBDD_node *f, int thresh, MR_ROBDD_bitset *vars)
+{
+ while (!MR_ROBDD_IS_TERMINAL(f)) {
+ if (f->value > thresh) {
+ MR_ROBDD_BITSET_ADD_ELEMENT(*vars, f->value);
+ }
+ MR_ROBDD_vars_present(f->tr, thresh, vars);
+ f = f->fa;
}
+}
+MR_ROBDD_node *
+MR_ROBDD_restrictThresh(int thresh, MR_ROBDD_node *f)
+{
+ MR_ROBDD_bitset vars;
+ int var;
+ int word;
+ MR_ROBDD_bitmask mask;
+
+ MR_ROBDD_COUNT_FN(MR_ROBDD_restrictThresh);
+ MR_ROBDD_BITSET_CLEAR(vars);
+ MR_ROBDD_vars_present(f, thresh, &vars);
+ MR_ROBDD_REV_FOREACH_ELEMENT(vars, var, word, mask) {
+ f = MR_ROBDD_restrict(var, f);
+ }
+ return f;
+}
-DECLARE_FN_COUNT(restrictThresh)
+#else /* MR_ROBDD_USE_THRESH */
-#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;
- }
+MR_ROBDD_node *
+MR_ROBDD_restrictThresh(int thresh, MR_ROBDD_node *f)
+{
+ /* restricts all variables greater than thresh. */
+
+ MR_ROBDD_COUNT_FN(MR_ROBDD_restrictThresh);
+ if (MR_ROBDD_IS_TERMINAL(f)) {
+ return f;
+ } else if (f->value <= thresh) {
+ MR_ROBDD_node *result;
+ MR_ROBDD_DECLARE_ASYM_BIN_CACHE_ENTRY;
+
+ MR_ROBDD_TRY_ASYM_BIN_CACHE((MR_ROBDD_node *) thresh, f, MR_ROBDD_restrictThresh);
+
+ result = MR_ROBDD_make_node(f->value,
+ MR_ROBDD_restrictThresh(thresh, f->tr),
+ MR_ROBDD_restrictThresh(thresh, f->fa));
+ MR_ROBDD_UPDATE_ASYM_BIN_CACHE((MR_ROBDD_node *) thresh, f, result, MR_ROBDD_restrictThresh);
+ return result;
+ } else {
+ return MR_ROBDD_one;
}
-#endif /* USE_THRESH */
+}
-
+#endif /* MR_ROBDD_USE_THRESH */
+
+#if !defined(MR_ROBDD_USE_THRESH) && !defined(MR_ROBDD_RESTRICT_SET)
+
+MR_ROBDD_node *
+MR_ROBDD_restricted_glb(int lo, int hi, MR_ROBDD_node *f, MR_ROBDD_node *g)
+{
+ return MR_ROBDD_restrictThresh(lo, hi, MR_ROBDD_glb(f, g));
+}
+
+#elif !defined(MR_ROBDD_USE_RGLB) /* && ( MR_ROBDD_USE_THRESH || MR_ROBDD_RESTRICT_SET ) */
+
+MR_ROBDD_node *
+MR_ROBDD_restricted_glb(int thresh, MR_ROBDD_node *f, MR_ROBDD_node *g)
+{
+ return MR_ROBDD_restrictThresh(thresh, MR_ROBDD_glb(f, g));
+}
+
+#else /* MR_ROBDD_USE_RGLB */
+
+/* returns true iff MR_ROBDD_glb(f,g) is not 'MR_ROBDD_zero' */
+static int
+MR_ROBDD_exists_glb(MR_ROBDD_node *f, MR_ROBDD_node *g)
+{
+ if (f == MR_ROBDD_zero) {
+ return MR_FALSE;
+ } else if (g == MR_ROBDD_zero) {
+ return MR_FALSE;
+ } else if (f == MR_ROBDD_one) {
+ /* since we know that g != MR_ROBDD_zero... */
+ return MR_TRUE;
+ } else if (g == MR_ROBDD_one) {
+ /* likewise f... */
+ return MR_TRUE;
+ } else if (f->value < g->value) {
+ return MR_ROBDD_exists_glb(f->tr, g) || MR_ROBDD_exists_glb(f->fa, g);
+ } else if (f->value > g->value) {
+ return MR_ROBDD_exists_glb(f, g->tr) || MR_ROBDD_exists_glb(f, g->fa);
+ } else {
+ return MR_ROBDD_exists_glb(f->tr, g->tr) || MR_ROBDD_exists_glb(f->fa, g->fa);
+ }
+}
+
+MR_ROBDD_node *
+MR_ROBDD_restricted_glb(int c, MR_ROBDD_node *f, MR_ROBDD_node *g)
+{
+ if (MR_ROBDD_IS_TERMINAL(f)) {
+ return (f == MR_ROBDD_one) ? MR_ROBDD_restrictThresh(c, g)
+ : MR_ROBDD_zero;
+ } else if (MR_ROBDD_IS_TERMINAL(g)) {
+ return (g == MR_ROBDD_one) ? MR_ROBDD_restrictThresh(c, f)
+ : MR_ROBDD_zero;
+ } MR_ROBDD_ELSE_TRY_EQUAL_TEST(f,g,MR_ROBDD_restrictThresh(c, f))
+ else {
+ int v;
+ MR_ROBDD_node *tr1, *tr2, *fa1, *fa2;
+ MR_ROBDD_node *result;
+
+ MR_ROBDD_DECLARE_RGLB_CACHE_ENTRY
+
+ MR_ROBDD_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 =
+ (MR_ROBDD_exists_glb(tr1,tr2)||MR_ROBDD_exists_glb(fa1,fa2)) ?
+ MR_ROBDD_one : MR_ROBDD_zero;
+ } else {
+ result = MR_ROBDD_make_node(v,
+ MR_ROBDD_restricted_glb(c, tr1, tr2),
+ MR_ROBDD_restricted_glb(c, fa1, fa2));
+ }
+ MR_ROBDD_UPDATE_RGLB_CACHE(f,g,c,result);
+ return result;
+ }
+}
+#endif /* MR_ROBDD_USE_THRESH */
/****************************************************************
- Renaming
+ Renaming
****************************************************************/
-DECLARE_FN_COUNT(renameArray)
-DECLARE_FN_COUNT(reverseRenameArray)
+MR_ROBDD_DECLARE_FN_COUNT(MR_ROBDD_renameArray)
+MR_ROBDD_DECLARE_FN_COUNT(MR_ROBDD_reverseRenameArray)
-#if defined(NEW)
+#if defined(MR_ROBDD_NEW)
-DECLARE_FN_COUNT(ite_var)
+MR_ROBDD_DECLARE_FN_COUNT(MR_ROBDD_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;
- }
+/* A special case version of MR_ROBDD_ite_var, where we know that f < g->value */
+static MR_ROBDD_node *
+MR_ROBDD_ite_var_g(int f, MR_ROBDD_node *g, MR_ROBDD_node *h)
+{
+ MR_ROBDD_COUNT_FN(MR_ROBDD_ite_var);
+
+ assert(MR_ROBDD_IS_TERMINAL(g) || f < g->value);
+
+ if (MR_ROBDD_IS_TERMINAL(h) || f < h->value) {
+ /* f < g && f < h */
+ return MR_ROBDD_make_node(f, g, h);
+ } else if (f == h->value) {
+ return MR_ROBDD_make_node(f, g, h->fa);
+ } else {
+ /* h < f < g */
+ MR_ROBDD_node *result;
+ MR_ROBDD_DECLARE_ITE_VAR_CACHE_ENTRY
+
+ MR_ROBDD_TRY_ITE_VAR_CACHE(f, g, h);
+
+ result = MR_ROBDD_make_node(h->value,
+ MR_ROBDD_ite_var_g(f, g, h->tr),
+ MR_ROBDD_ite_var_g(f, g, h->fa));
+ MR_ROBDD_UPDATE_ITE_VAR_CACHE(f, g, h, result);
+ return result;
+ }
+}
+
+/*
+** A special case version of MR_ROBDD_ite_var, where we know that
+** f < h->value
+*/
+
+static MR_ROBDD_node *
+MR_ROBDD_ite_var_h(int f, MR_ROBDD_node *g, MR_ROBDD_node *h)
+{
+ MR_ROBDD_COUNT_FN(MR_ROBDD_ite_var);
+
+ assert(MR_ROBDD_IS_TERMINAL(h) || f < h->value);
+
+ if (MR_ROBDD_IS_TERMINAL(g) || f < g->value) {
+ /* f < g && f < h */
+ return MR_ROBDD_make_node(f, g, h);
+ } else if (f == g->value) {
+ return MR_ROBDD_make_node(f, g->tr, h);
+ } else {
+ /* h < f < g */
+ MR_ROBDD_node *result;
+ MR_ROBDD_DECLARE_ITE_VAR_CACHE_ENTRY
+
+ MR_ROBDD_TRY_ITE_VAR_CACHE(f, g, h);
+ result = MR_ROBDD_make_node(g->value,
+ MR_ROBDD_ite_var_h(f, g->tr, h),
+ MR_ROBDD_ite_var_h(f, g->fa, h));
+ MR_ROBDD_UPDATE_ITE_VAR_CACHE(f, g, h, result);
+ return result;
+ }
+}
- return renameArray(f, max, rev_map);
+/*
+** A special case version of MR_ROBDD_ite, where we know that
+** !MR_ROBDD_IS_TERMINAL(f) && f->tr == MR_ROBDD_one && f->fa == MR_ROBDD_zero.
+** In fact, we refine this further and make f be just (what would have been)
+** f->value.
+**
+** Recall the code for MR_ROBDD_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 MR_ROBDD_ite is:
+**
+** mn(top, i(ft, gt, ht), i(ff, gf, hf))
+**
+** (abbreviating MR_ROBDD_make_node as mn and MR_ROBDD_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 MR_ROBDD_ite_var_g and ih for
+** MR_ROBDD_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))
+*/
+
+MR_ROBDD_node *
+MR_ROBDD_ite_var(int f,MR_ROBDD_node *g,MR_ROBDD_node *h)
+{
+ int g_val = INT_MAX;
+ int h_val = INT_MAX;
+ MR_ROBDD_node *result;
+ MR_ROBDD_node *g_tr, *g_fa, *h_tr, *h_fa;
+ MR_ROBDD_DECLARE_ITE_VAR_CACHE_ENTRY
+
+ MR_ROBDD_COUNT_FN(MR_ROBDD_ite_var);
+ MR_ROBDD_DIRECT_EQUAL_TEST(g,h,g);
+ MR_ROBDD_TRY_ITE_VAR_CACHE(f, g, h);
+
+ if (!MR_ROBDD_IS_TERMINAL(g)) g_val = g->value;
+ if (!MR_ROBDD_IS_TERMINAL(h)) h_val = h->value;
+
+ if (MR_ROBDD_IS_TERMINAL(g)) {
+ g_tr = g_fa = g;
+ } else {
+ g_tr = g->tr;
+ g_fa = g->fa;
+ }
+ if (MR_ROBDD_IS_TERMINAL(h)) {
+ h_tr = h_fa = h;
+ } else {
+ h_tr = h->tr;
+ h_fa = h->fa;
+ }
+
+ if (f < g_val) {
+ if (f < h_val) /* case 2 (b,c,d): f < g && f < h */ {
+ result = MR_ROBDD_make_node(f, g, h);
+ } else /* case 8 (k): h < f < g */ {
+ result = MR_ROBDD_make_node(h_val,
+ MR_ROBDD_ite_var_g(f, g, h_tr),
+ MR_ROBDD_ite_var_g(f, g, h_fa));
+ }
+ /* g < f */
+ } else if (f < h_val) /* g < f < h */ {
+ result = MR_ROBDD_make_node(g_val,
+ MR_ROBDD_ite_var_h(f, g_tr, h),
+ MR_ROBDD_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 = MR_ROBDD_make_node(h_val,
+ MR_ROBDD_ite_var(f, g, h_tr),
+ MR_ROBDD_ite_var(f, g, h_fa));
+ /* g < f && g <= h */
+ } else if (g_val == h_val) /* g == h < f */ {
+ result = MR_ROBDD_make_node(g_val,
+ MR_ROBDD_ite_var(f, g_tr, h_tr),
+ MR_ROBDD_ite_var(f, g_fa, h_fa));
+ } else /* case 6 (h,i): g < h < f */ {
+ result = MR_ROBDD_make_node(g_val,
+ MR_ROBDD_ite_var(f, g_tr, h),
+ MR_ROBDD_ite_var(f, g_fa, h));
}
+ MR_ROBDD_UPDATE_ITE_VAR_CACHE(f, g, h, result);
+ return result;
+}
+
+#else /* ! MR_ROBDD_NEW */
+
+#define MR_ROBDD_ite_var(v,f,g) MR_ROBDD_ite(MR_ROBDD_variableRep(v), f, g)
+#endif /* !MR_ROBDD_NEW */
+
+MR_ROBDD_node *
+MR_ROBDD_renameArray(MR_ROBDD_node *f, int count, int mapping[])
+{
+ int newval;
+
+ MR_ROBDD_COUNT_FN(MR_ROBDD_renameArray);
+ if (MR_ROBDD_IS_TERMINAL(f)) {
+ return f;
+ } else if (f->value > count) {
+ return MR_ROBDD_one;
+ } else if (MR_ROBDD_UNUSED_MAPPING==(newval=mapping[f->value])) {
+ return MR_ROBDD_lub(MR_ROBDD_renameArray(f->tr, count, mapping),
+ MR_ROBDD_renameArray(f->fa, count, mapping));
+ } else {
+ return MR_ROBDD_ite_var(newval,
+ MR_ROBDD_renameArray(f->tr, count, mapping),
+ MR_ROBDD_renameArray(f->fa, count, mapping));
+ }
+}
+
+MR_ROBDD_node *
+MR_ROBDD_reverseRenameArray(MR_ROBDD_node *f, int count, int mapping[])
+{
+ int i, val, MR_ROBDD_max;
+ int rev_map[MR_ROBDD_MAXVAR];
+
+ MR_ROBDD_COUNT_FN(MR_ROBDD_reverseRenameArray);
+ /* NB: four -1 bytes is the same as a -1 word */
+ MR_memset(rev_map, ~((char) 0), sizeof(rev_map));
+ for (i=1,MR_ROBDD_max=-1; i<=count; ++i) {
+ rev_map[(val=mapping[i])] = i;
+ if (MR_ROBDD_max < val) MR_ROBDD_max = val;
+ }
+
+ return MR_ROBDD_renameArray(f, MR_ROBDD_max, rev_map);
+}
/****************************************************************
- Abstract Exit (renaming + conjunction + restriction)
+ 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));
- }
+#if !defined(MR_ROBDD_USE_THRESH) && !defined(MR_ROBDD_RESTRICT_SET)
+
+MR_ROBDD_node *
+MR_ROBDD_abstract_exit(MR_ROBDD_node *context, MR_ROBDD_node *f, int count,
+ int mapping[], int lo, int hi)
+{
+ return MR_ROBDD_restricted_glb(lo, hi, context,
+ MR_ROBDD_renameArray(f, count, mapping));
+}
+
+#elif 1 /* ( MR_ROBDD_USE_THRESH || MR_ROBDD_RESTRICT_SET ) */
+
+MR_ROBDD_node *
+MR_ROBDD_abstract_exit(MR_ROBDD_node *context, MR_ROBDD_node *f, int count,
+ int mapping[], int thresh)
+{
+ return MR_ROBDD_restricted_glb(thresh, context,
+ MR_ROBDD_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;
+/*
+** returns MR_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
+** MR_ROBDD_zero.
+*/
+
+int
+MR_ROBDD_exists_restrict_sets(MR_ROBDD_node *f, MR_ROBDD_bitset *trues,
+ MR_ROBDD_bitset *falses, int hielt)
+{
+ for (;;) {
+ if (MR_ROBDD_IS_TERMINAL(f)) {
+ return f == MR_ROBDD_one;
+ } else if (f->value > hielt) {
+ return MR_TRUE;
+ } else {
+ int word = MR_ROBDD_BITSET_WORD(f->value);
+ MR_ROBDD_bitmask mask = MR_ROBDD_BITSET_MASK(f->value);
- if (context == zero) return zero;
- if (context == one) return restricted_rename(f, count, mapping, thresh);
+ if (MR_ROBDD_BITSET_MEMBER(*trues,word,mask)) {
+ f = f->tr; /* continue loop */
+ } else if (MR_ROBDD_BITSET_MEMBER(*falses,word,mask)) {
+ f = f->fa; /* continue loop */
+ } else if (MR_ROBDD_exists_restrict_sets(f->tr, trues, falses,
+ hielt))
+ {
+ return MR_TRUE;
+ } else {
+ f = f->fa;
+ }
+ }
+ }
+}
- BITSET_CLEAR(trues);
- BITSET_CLEAR(falses);
+/*
+** computes the function f restricted so that all variables in trues
+** are set to true and all in falses are set to false.
+*/
+
+MR_ROBDD_node *
+MR_ROBDD_restrict_sets(MR_ROBDD_node *f, MR_ROBDD_bitset *trues,
+ MR_ROBDD_bitset *falses, int hielt, int thresh)
+{
+ for (;;) {
+ if (MR_ROBDD_IS_TERMINAL(f)) {
+ return f;
+ } else if (f->value > hielt) {
+ return MR_ROBDD_restrictThresh(thresh, f);
+ } else if (f->value > thresh) {
+ return MR_ROBDD_exists_restrict_sets(f, trues, falses, hielt)
+ ? MR_ROBDD_one : MR_ROBDD_zero;
+ } else {
+ int word = MR_ROBDD_BITSET_WORD(f->value);
+ MR_ROBDD_bitmask mask = MR_ROBDD_BITSET_MASK(f->value);
- return abexit(context, f, count, mapping, thresh, &trues, &falses, -1);
+ if (MR_ROBDD_BITSET_MEMBER(*trues,word,mask)) {
+ f = f->tr; /* continue loop */
+ } else if (MR_ROBDD_BITSET_MEMBER(*falses,word,mask)) {
+ f = f->fa; /* continue loop */
+ } else {
+ return MR_ROBDD_make_node(f->value,
+ MR_ROBDD_restrict_sets(f->tr, trues, falses, hielt,
+ thresh),
+ MR_ROBDD_restrict_sets(f->fa, trues, falses, hielt,
+ thresh));
+ }
+ }
+ }
+}
+
+/*
+** if f->value > thresh, returns MR_ROBDD_one, else if f->value is in either
+** trues (or falses), this returns
+** MR_ROBDD_follow_path(f->tr (or fa), trues, falses}
+** else it returns f.
+*/
+
+MR_ROBDD_node *
+MR_ROBDD_follow_path(MR_ROBDD_node *f, MR_ROBDD_bitset *trues,
+ MR_ROBDD_bitset *falses)
+{
+
+ while (!MR_ROBDD_IS_TERMINAL(f)) {
+ int word = MR_ROBDD_BITSET_WORD(f->value);
+ MR_ROBDD_bitmask mask = MR_ROBDD_BITSET_MASK(f->value);
+
+ if (MR_ROBDD_BITSET_MEMBER(*trues,word,mask)) {
+ f = f->tr;
+ } else if (MR_ROBDD_BITSET_MEMBER(*falses,word,mask)) {
+ f = f->fa;
+ } else {
+ break;
+ }
+ }
+ return f;
}
-#endif /* 0 (end of unused code) */
+/*
+** This function computes
+**
+** MR_ROBDD_restrictThresh(MR_ROBDD_renameArray(f, count, mapping), thresh)
+**
+*/
+
+MR_ROBDD_node *
+MR_ROBDD_restricted_rename(MR_ROBDD_node *f, int count, int mapping[],
+ int thresh)
+{
+ if (MR_ROBDD_IS_TERMINAL(f)) {
+ return f;
+ } else {
+ int newval = mapping[f->value];
+ MR_ROBDD_node *tr, *fa;
+
+ tr = MR_ROBDD_restricted_rename(f->tr, count, mapping, thresh);
+ fa = MR_ROBDD_restricted_rename(f->fa, count, mapping, thresh);
+
+ if (newval > thresh) {
+ return MR_ROBDD_lub(tr, fa);
+ } else {
+ return MR_ROBDD_ite_var(newval, tr, fa);
+ }
+ }
+}
+
+/*
+** This function computes
+**
+** MR_ROBDD_restrictThresh(MR_ROBDD_glb(context1,
+** MR_ROBDD_renameArray(f, count, mapping)), thresh)
+**
+** where context1 is context restricted by the settings in trues and
+** falses. We know that !MR_ROBDD_IS_TERMINAL(context).
+*/
+
+MR_ROBDD_node *
+MR_ROBDD_abexit(MR_ROBDD_node *context, MR_ROBDD_node *f, int count,
+ int mapping[], int thresh, MR_ROBDD_bitset *trues,
+ MR_ROBDD_bitset *falses, int hielt)
+{
+ if (MR_ROBDD_IS_TERMINAL(f)) {
+ if (f==MR_ROBDD_one) {
+ return MR_ROBDD_restrict_sets(context, trues, falses, hielt,
+ thresh);
+ } else {
+ return f;
+ }
+ } else {
+ int newval = mapping[f->value];
+ MR_ROBDD_node *tr, *fa;
+
+ if (newval == context->value) {
+ tr = MR_ROBDD_follow_path(context->tr, trues, falses);
+ fa = MR_ROBDD_follow_path(context->fa, trues, falses);
+
+ if (tr == MR_ROBDD_one) {
+ tr = MR_ROBDD_restricted_rename(f->tr, count, mapping, thresh);
+ } else if (tr != MR_ROBDD_zero) {
+ tr = MR_ROBDD_abexit(tr, f->tr, count, mapping, thresh,
+ trues, falses, hielt);
+ }
+ if (fa == MR_ROBDD_one) {
+ fa = MR_ROBDD_restricted_rename(f->fa, count, mapping, thresh);
+ } else if (fa != MR_ROBDD_zero) {
+ fa = MR_ROBDD_abexit(fa, f->fa, count, mapping, thresh,
+ trues, falses, hielt);
+ }
+ } else {
+ int word = MR_ROBDD_BITSET_WORD(newval);
+ MR_ROBDD_bitmask mask = MR_ROBDD_BITSET_MASK(newval);
+ int newhi = (newval>hielt ? newval : hielt);
+
+ MR_ROBDD_BITSET_ADD(*trues,word,mask); /* turn on true bit */
+ tr = MR_ROBDD_abexit(context, f->tr, count, mapping, thresh,
+ trues, falses, newhi);
+ MR_ROBDD_BITSET_TOGGLE(*trues,word,mask); /* turn off true bit */
+ MR_ROBDD_BITSET_ADD(*falses,word,mask); /* turn on false bit */
+ fa = MR_ROBDD_abexit(context, f->fa, count, mapping, thresh,
+ trues, falses, newhi);
+ MR_ROBDD_BITSET_TOGGLE(*falses,word,mask); /* turn off false bit */
+ }
+ if (newval > thresh) {
+ return MR_ROBDD_lub(tr, fa);
+ } else {
+ return MR_ROBDD_ite_var(newval, tr, fa);
+ }
+ }
+}
+
+MR_ROBDD_node *
+MR_ROBDD_abstract_exit(MR_ROBDD_node *context, MR_ROBDD_node *f, int count,
+ int mapping[], int thresh)
+{
+ MR_ROBDD_bitset trues;
+ MR_ROBDD_bitset falses;
+
+ if (context == MR_ROBDD_zero)
+ return MR_ROBDD_zero;
+ if (context == MR_ROBDD_one)
+ return MR_ROBDD_restricted_rename(f, count, mapping, thresh);
+
+ MR_ROBDD_BITSET_CLEAR(trues);
+ MR_ROBDD_BITSET_CLEAR(falses);
+
+ return MR_ROBDD_abexit(context, f, count, mapping, thresh,
+ &trues, &falses, -1);
+}
+
+#endif /* 0 (end of unused code) */
/****************************************************************
- Abstract Unification
+ 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);
+/*
+** NB: MR_ROBDD_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(MR_ROBDD_ELIM_DUPS)
+ #define MR_ROBDD_DECLARE_PREV(init) int prev = (init);
+ #define MR_ROBDD_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);
+ #define MR_ROBDD_DECLARE_PREV(init) int prev = (init);
+ #define MR_ROBDD_HANDLE_DUP(this,rel) \
+ assert((this) != prev); \
+ assert((this) rel prev); \
+ prev = (this);
#else
-#define DECLARE_PREV(init)
-#define HANDLE_DUP(this,rel)
+ #define MR_ROBDD_DECLARE_PREV(init)
+ #define MR_ROBDD_HANDLE_DUP(this,rel)
#endif
+MR_ROBDD_DECLARE_FN_COUNT(iff_conj)
-DECLARE_FN_COUNT(iff_conj)
+#if defined(MR_ROBDD_NAIVE)
+MR_ROBDD_node *MR_ROBDD_iff_conj_array(int v0, int n, int arr[])
+{
+ MR_ROBDD_node *conj = MR_ROBDD_one;
+ MR_ROBDD_node *v_rep = MR_ROBDD_variableRep(v0);
+ int i;
+ MR_ROBDD_DECLARE_PREV(-1)
+
+ MR_ROBDD_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<n; ++i) {
+ MR_ROBDD_HANDLE_DUP(arr[i], >)
+ if (arr[i] != v0) {
+ conj = MR_ROBDD_glb(conj, MR_ROBDD_variableRep(arr[i]));
+ }
+ }
+ return MR_ROBDD_glb(MR_ROBDD_implies(conj,v_rep),
+ MR_ROBDD_implies(v_rep,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<n; ++i) {
- HANDLE_DUP(arr[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));
+#elif !defined(MR_ROBDD_USE_THRESH)
+
+MR_ROBDD_node *MR_ROBDD_iff_conj_array(int v0, int n, int arr[])
+{
+ MR_ROBDD_node *conj = MR_ROBDD_one;
+ MR_ROBDD_node *pos_v = MR_ROBDD_variableRep(v0);
+ MR_ROBDD_node *neg_v = MR_ROBDD_ite(pos_v, MR_ROBDD_zero, MR_ROBDD_one);
+ int *ptr;
+ MR_ROBDD_DECLARE_PREV(MR_ROBDD_MAXVAR)
+
+ MR_ROBDD_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;
+ MR_ROBDD_HANDLE_DUP(vi, <)
+ if (vi != v0) {
+ conj = MR_ROBDD_glb(conj, MR_ROBDD_variableRep(vi));
+ }
}
+ return MR_ROBDD_ite(conj, pos_v, neg_v);
+}
+
+#else /* MR_ROBDD_USE_THRESH */
+
+MR_ROBDD_node *MR_ROBDD_iff_conj_array(int v0, int n, int arr[])
+{
+ MR_ROBDD_node *thens = MR_ROBDD_one, *elses = MR_ROBDD_zero;
+ int *ptr;
+ int vi = 0; /* this value doesn't matter */
+ MR_ROBDD_DECLARE_PREV(MR_ROBDD_MAXVAR)
+
+ MR_ROBDD_COUNT_FN(iff_conj);
+ /*
+ ** first build part of graph below v0. For this, we build two subgraphs:
+ ** MR_ROBDD_one for when v0 is true, and MR_ROBDD_one for false.
+ ** These are called thens and elses.
+ */
+
+ for (ptr=&arr[n-1]; ptr>=arr && v0<(vi=*ptr); --ptr) {
+ MR_ROBDD_HANDLE_DUP(vi, <)
+ thens = MR_ROBDD_make_node(vi, thens, MR_ROBDD_zero);
+ elses = MR_ROBDD_make_node(vi, elses, MR_ROBDD_one);
+ }
+
+ if (v0 == vi) {
+ --ptr;
+ }
+
+ /* make v0 MR_ROBDD_node */
+ thens = MR_ROBDD_make_node(v0,thens,elses);
+
+ /* Finally build part of graph above v0. For this, we build
+ * only MR_ROBDD_one graph, whose then branch is the graph we've built
+ * so far and whose else branch is ~v0.
+ */
+
+ if (ptr >= arr) {
+ MR_ROBDD_DECLARE_PREV(MR_ROBDD_MAXVAR)
+ /* make ~v0 */
+ elses = MR_ROBDD_make_node(v0,MR_ROBDD_zero,MR_ROBDD_one);
+
+ do {
+ vi = *ptr;
+ MR_ROBDD_HANDLE_DUP(vi, <)
+ thens = MR_ROBDD_make_node(vi, thens, elses);
+ } while (--ptr >= arr);
+ }
+
+ return thens;
+}
+#endif /* MR_ROBDD_OLD */
+
+MR_ROBDD_node *MR_ROBDD_restricted_iff_conj_array(int v0, int n, int arr[],
+ int thresh)
+{
+ if (v0 > thresh) {
+ return MR_ROBDD_one;
+ }
+ while (--n>=0 && arr[n]>thresh)
+ ;
+ return MR_ROBDD_iff_conj_array(v0, n+1, arr);
+}
+
+#if !defined(MR_ROBDD_USE_THRESH) && !defined(MR_ROBDD_RESTRICT_SET)
+MR_ROBDD_node *MR_ROBDD_abstract_unify(MR_ROBDD_node *f, int v0, int n,
+ int arr[], int lo, int hi)
+{
+ return MR_ROBDD_restricted_glb(lo, hi, f,
+ MR_ROBDD_iff_conj_array(v0, n, arr));
+}
+
+#elif 1 /* ( MR_ROBDD_USE_THRESH || MR_ROBDD_RESTRICT_SET ) */
+
+MR_ROBDD_node *MR_ROBDD_abstract_unify(MR_ROBDD_node *f, int v0, int n,
+ int arr[], int thresh)
+{
+ return MR_ROBDD_restricted_glb(thresh, f,
+ MR_ROBDD_iff_conj_array(v0, n, arr));
+}
+
#else /* !1 (this code is unused) */
+static MR_ROBDD_node *
+MR_ROBDD_build_and(int n, int arr[], MR_ROBDD_node *tr, MR_ROBDD_node *fa)
+{
+ if (n<=0) {
+ return tr;
+ } else {
+ return MR_ROBDD_make_node(arr[0],
+ MR_ROBDD_build_and(n-1, &arr[1], tr, fa), fa);
+ }
+}
-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]<v0) ? arr[0] : v0;
-
- if (f->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]<v0) ? arr[0] : v0;
- node *result;
-
- if (f->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;
- }
+static MR_ROBDD_node *MR_ROBDD_glb_and(MR_ROBDD_node *f, int n, int arr[])
+{
+ if (f == MR_ROBDD_zero) {
+ return MR_ROBDD_zero;
+ } else if (f == MR_ROBDD_one) {
+ return MR_ROBDD_build_and(n, arr, MR_ROBDD_one, MR_ROBDD_zero);
+ } else if (n == 0) {
+ return f;
+ } else {
+ MR_ROBDD_node *result;
+ if (f->value < arr[0]) {
+ result = MR_ROBDD_make_node(f->value,
+ MR_ROBDD_glb_and(f->tr, n, arr),
+ MR_ROBDD_glb_and(f->fa, n, arr));
+ } else if (f->value > arr[0]) {
+ result = MR_ROBDD_make_node(arr[0],
+ MR_ROBDD_glb_and(f, n-1, &arr[1]),
+ MR_ROBDD_zero);
+ } else /* f->value == arr[0] */{
+ result = MR_ROBDD_make_node(f->value,
+ MR_ROBDD_glb_and(f->tr, n-1, &arr[1]),
+ MR_ROBDD_zero);
+ }
+ return result;
}
+}
-#endif /* (end of unused code) */
+static MR_ROBDD_node *
+MR_ROBDD_glb_nand(MR_ROBDD_node *f, int n, int arr[])
+{
+ if (f == MR_ROBDD_zero) {
+ return MR_ROBDD_zero;
+ } else if (f == MR_ROBDD_one) {
+ return MR_ROBDD_build_and(n, arr, MR_ROBDD_zero, MR_ROBDD_one);
+ } else if (n == 0) {
+ return MR_ROBDD_zero;
+ } else {
+ MR_ROBDD_node *result;
+ if (f->value < arr[0]) {
+ result = MR_ROBDD_make_node(f->value,
+ MR_ROBDD_glb_nand(f->tr, n, arr),
+ MR_ROBDD_glb_nand(f->fa, n, arr));
+ } else if (f->value > arr[0]) {
+ result = MR_ROBDD_make_node(arr[0],
+ MR_ROBDD_glb_nand(f, n-1, &arr[1]),
+ f);
+ } else /* f->value == arr[0] */{
+ result = MR_ROBDD_make_node(f->value,
+ MR_ROBDD_glb_nand(f->tr, n-1, &arr[1]),
+ f);
+ }
+ return result;
+ }
+}
+
+/*
+** returns MR_ROBDD_zero != MR_ROBDD_glb(f,
+** MR_ROBDD_build_and(n, arr, MR_ROBDD_one, MR_ROBDD_zero))
+*/
+
+static int
+MR_ROBDD_exists_glb_and(MR_ROBDD_node *f, int n, int arr[])
+{
+ if (f == MR_ROBDD_zero) {
+ return MR_FALSE;
+ } else if (f == MR_ROBDD_one || n == 0) {
+ return MR_TRUE;
+ } else if (f->value < arr[0]) {
+ return (MR_ROBDD_exists_glb_and(f->tr, n, arr) ||
+ MR_ROBDD_exists_glb_and(f->fa, n, arr));
+ } else {
+ if (f->value == arr[0]) {
+ f = f->tr;
+ }
+ return MR_ROBDD_exists_glb_and(f, n-1, arr+1);
+ }
+}
+/*
+** returns MR_ROBDD_zero != MR_ROBDD_glb(f,
+** MR_ROBDD_build_and(n, arr, MR_ROBDD_zero, MR_ROBDD_one))
+*/
+
+static int
+MR_ROBDD_exists_glb_nand(MR_ROBDD_node *f, int n, int arr[])
+{
+ if (f == MR_ROBDD_zero || n == 0) {
+ return MR_FALSE;
+ } else if (f == MR_ROBDD_one || f->value > arr[0]) {
+ /*
+ ** if f->value > arr[0], then the else branch of the MR_ROBDD_node we'd
+ ** build would be MR_ROBDD_one, so we know the graph couldn't ==
+ ** MR_ROBDD_zero.
+ */
+ return MR_TRUE;
+ } else if (f->value < arr[0]) {
+ return MR_ROBDD_glb_nand(f->tr, n, arr)
+ || MR_ROBDD_glb_nand(f->fa, n, arr);
+ } else if (f->fa != MR_ROBDD_zero) /* && f->value == arr[0] */ {
+ /*
+ ** if f->fa isn't MR_ROBDD_zero, then conjoined with MR_ROBDD_one
+ ** it won't be MR_ROBDD_zero, so the MR_ROBDD_node we'd build won't
+ ** == MR_ROBDD_zero.
+ */
+ return MR_TRUE;
+ } else /* f->value == arr[0] && f->fa == MR_ROBDD_zero */ {
+ return MR_ROBDD_exists_glb_nand(f->tr, n-1, arr+1);
+ }
+}
+
+/*
+** returns MR_ROBDD_zero != MR_ROBDD_glb(f,
+** MR_ROBDD_iff_conj_array(v0, n, arr))
+*/
+
+static int
+MR_ROBDD_exists_glb_iffconj(MR_ROBDD_node *f, int v0, int n, int arr[])
+{
+ if (f == MR_ROBDD_zero) {
+ return MR_FALSE;
+ } else if (f == MR_ROBDD_one) {
+ return MR_TRUE;
+ } else {
+ int v = (n>0 && arr[0]<v0) ? arr[0] : v0;
+
+ if (f->value < v) {
+ return (MR_ROBDD_exists_glb_iffconj(f->tr, v0, n, arr) ||
+ MR_ROBDD_exists_glb_iffconj(f->fa, v0, n, arr));
+ } else /* f->value >= v */ {
+ MR_ROBDD_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 (MR_ROBDD_exists_glb_nand(fa, n, arr) ||
+ MR_ROBDD_exists_glb_and(tr, n, arr));
+ } else {
+ return (!MR_ROBDD_var_entailed(fa, v0) ||
+ MR_ROBDD_exists_glb_iffconj(tr, v0, n-1, &arr[1]));
+ }
+ }
+ }
+}
+/*
+** returns MR_ROBDD_restricted_glb(f,
+** MR_ROBDD_build_and(n, arr, MR_ROBDD_one, MR_ROBDD_zero), thresh)
+*/
+
+static MR_ROBDD_node *
+MR_ROBDD_rglb_and(MR_ROBDD_node *f, int n, int arr[], int thresh)
+{
+ if (f == MR_ROBDD_zero) {
+ return MR_ROBDD_zero;
+ } else if (f == MR_ROBDD_one) {
+ while (--n>=0 && arr[n]>thresh);
+ return MR_ROBDD_build_and(n+1, arr, MR_ROBDD_one, MR_ROBDD_zero);
+ } else if (n == 0) {
+ return MR_ROBDD_restrictThresh(thresh, f);
+ } else {
+ if (f->value < arr[0]) {
+ if (f->value > thresh) {
+ return (MR_ROBDD_exists_glb_and(f->tr, n, arr) ||
+ MR_ROBDD_exists_glb_and(f->fa, n, arr))
+ ? MR_ROBDD_one : MR_ROBDD_zero;
+ } else {
+ return MR_ROBDD_make_node(f->value,
+ MR_ROBDD_rglb_and(f->tr, n, arr, thresh),
+ MR_ROBDD_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 MR_ROBDD_exists_glb_and(f, n-1, arr+1)
+ ? MR_ROBDD_one : MR_ROBDD_zero;
+ } else {
+ return MR_ROBDD_make_node(v,
+ MR_ROBDD_rglb_and(f, n-1, arr+1, thresh),
+ MR_ROBDD_zero);
+ }
+ }
+ }
+}
+
+/*
+** returns MR_ROBDD_restricted_glb(f,
+** MR_ROBDD_build_and(n, arr, MR_ROBDD_zero, MR_ROBDD_one), thresh)
+*/
+
+static MR_ROBDD_node *
+MR_ROBDD_rglb_nand(MR_ROBDD_node *f, int n, int arr[], int thresh)
+{
+ if (f == MR_ROBDD_zero || n == 0) {
+ return MR_ROBDD_zero;
+ } else if (f == MR_ROBDD_one) {
+ /*
+ ** just MR_ROBDD_restrictThresh(thresh,
+ ** MR_ROBDD_build_and(n, arr, MR_ROBDD_zero, MR_ROBDD_one)).
+ ** Note that if anything is restricted away, then the whole graph
+ ** degenerates to MR_ROBDD_one. So...
+ */
+ if (arr[n-1]>thresh) {
+ return MR_ROBDD_one;
+ } else {
+ return MR_ROBDD_build_and(n, arr, MR_ROBDD_zero, MR_ROBDD_one);
+ }
+ } else {
+ if (f->value < arr[0]) {
+ if (f->value > thresh) {
+ return (MR_ROBDD_exists_glb_nand(f->tr, n, arr)||
+ MR_ROBDD_exists_glb_nand(f->fa, n, arr))
+ ? MR_ROBDD_one : MR_ROBDD_zero;
+ } else {
+ return MR_ROBDD_make_node(f->value,
+ MR_ROBDD_rglb_nand(f->tr, n, arr, thresh),
+ MR_ROBDD_rglb_nand(f->fa, n, arr, thresh));
+ }
+ } else if (f->value > arr[0]) {
+ if (arr[0] > thresh) {
+ /* because f != MR_ROBDD_zero, restricting all vars yields MR_ROBDD_one */
+ return MR_ROBDD_one;
+ } else {
+ return MR_ROBDD_make_node(arr[0],
+ MR_ROBDD_rglb_nand(f, n-1, arr+1, thresh),
+ MR_ROBDD_restrictThresh(thresh, f));
+ }
+ } else /* f->value == arr[0] */ {
+ if (arr[0] > thresh) {
+ return (f->fa != MR_ROBDD_zero ||
+ MR_ROBDD_exists_glb_nand(f->tr, n-1, arr+1))
+ ? MR_ROBDD_one : MR_ROBDD_zero;
+ } else {
+ return MR_ROBDD_make_node(arr[0],
+ MR_ROBDD_rglb_nand(f->tr, n-1, arr+1, thresh),
+ MR_ROBDD_restrictThresh(thresh, f->fa));
+ }
+ }
+ }
+}
+
+/*
+** returns MR_ROBDD_restricted_glb(thresh, f,
+** MR_ROBDD_make_node(v, MR_ROBDD_zero, MR_ROBDD_one))
+*/
+
+static MR_ROBDD_node *
+MR_ROBDD_rglb_notvar(MR_ROBDD_node *f, int v, int thresh)
+{
+ if (f == MR_ROBDD_zero) {
+ return MR_ROBDD_zero;
+ } else if (f == MR_ROBDD_one) {
+ if (v > thresh) return MR_ROBDD_one;
+ return MR_ROBDD_make_node(v, MR_ROBDD_zero, MR_ROBDD_one);
+ } else {
+ if (f->value < v) {
+ if (f->value > thresh) {
+ return (!MR_ROBDD_var_entailed(f->tr, v) ||
+ !MR_ROBDD_var_entailed(f->fa, v))
+ ? MR_ROBDD_one : MR_ROBDD_zero;
+ } else {
+ return MR_ROBDD_make_node(f->value,
+ MR_ROBDD_rglb_notvar(f->tr, v, thresh),
+ MR_ROBDD_rglb_notvar(f->fa, v, thresh));
+ }
+ } else {
+ if (f->value == v) {
+ f = f->fa;
+ }
+ if (v > thresh) {
+ return f==MR_ROBDD_zero ? MR_ROBDD_zero : MR_ROBDD_one;
+ } else {
+ return MR_ROBDD_make_node(v, MR_ROBDD_zero,
+ MR_ROBDD_restrictThresh(thresh, f));
+ }
+ }
+ }
+}
+
+MR_ROBDD_node *
+MR_ROBDD_abstract_unify(MR_ROBDD_node *f, int v0, int n, int arr[], int thresh)
+{
+ if (f == MR_ROBDD_zero) {
+ return MR_ROBDD_zero;
+ } else if (f == MR_ROBDD_one) {
+ return MR_ROBDD_restricted_iff_conj_array(v0, n, arr, thresh);
+ } else {
+ int v = (n>0 && arr[0]<v0) ? arr[0] : v0;
+ MR_ROBDD_node *result;
+
+ if (f->value < v) {
+ if (f->value > thresh) {
+ result = (MR_ROBDD_exists_glb_iffconj(f->tr, v0, n, arr) ||
+ MR_ROBDD_exists_glb_iffconj(f->fa, v0, n, arr))
+ ? MR_ROBDD_one : MR_ROBDD_zero;
+ } else {
+ result =
+ MR_ROBDD_make_node(f->value,
+ MR_ROBDD_abstract_unify(f->tr, v0, n, arr, thresh),
+ MR_ROBDD_abstract_unify(f->fa, v0, n, arr, thresh));
+ }
+ } else /* f->value >= v */ {
+ MR_ROBDD_node *tr = f, *fa = f;
+
+ if (f->value == v) {
+ tr = f->tr; fa = f->fa;
+ }
+ if (v > thresh) {
+ int value;
+
+ if (v == v0) {
+ value = (MR_ROBDD_exists_glb_nand(fa, n, arr) ||
+ MR_ROBDD_exists_glb_and(tr, n, arr));
+ } else {
+ value =
+ (!MR_ROBDD_var_entailed(fa, v0) ||
+ MR_ROBDD_exists_glb_iffconj(tr, v0, n-1, &arr[1]));
+ }
+ result = value ? MR_ROBDD_one : MR_ROBDD_zero;
+ } else {
+ if (v == v0) {
+ tr = MR_ROBDD_rglb_and(tr, n, arr, thresh);
+ fa = MR_ROBDD_rglb_nand(fa, n, arr, thresh);
+ } else {
+ tr = MR_ROBDD_abstract_unify(tr, v0, n-1, arr+1, thresh);
+ fa = MR_ROBDD_rglb_notvar(fa, v0, thresh);
+ }
+ result = MR_ROBDD_make_node(v, tr, fa);
+ }
+ }
+ return result;
+ }
+}
+
+#endif /* (end of unused code) */
/****************************************************************
- Finding Entailed Variables
+ 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; i<topvar; ++i) {
- if (var_entailed(f, i)) BITSET_ADD_ELEMENT(def_vars,i);
- }
- return &def_vars;
- }
-#elif 0 /* not using this version */
-int topvar(node *f, int n)
- {
- int n1;
-
- if (IS_TERMINAL(f)) return n;
-
- n1 = topvar(f->tr, 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.
- */
+/*
+** returns MR_TRUE iff var is implied by the boolean function specified by f
+*/
+
+int
+MR_ROBDD_var_entailed(MR_ROBDD_node *f, int var)
+{
+#if defined(MR_ROBDD_NAIVE)
+ return f == MR_ROBDD_glb(f, MR_ROBDD_variableRep(var));
+#elif !defined(MR_ROBDD_USE_THRESH) && !defined(MR_ROBDD_USE_ITE_CONSTANT)
+ return MR_ROBDD_one == MR_ROBDD_implies(f, MR_ROBDD_variableRep(var));
+#elif !defined(MR_ROBDD_USE_RGLB)
+ return MR_ROBDD_one == MR_ROBDD_ite_constant(f, MR_ROBDD_variableRep(var),
+ MR_ROBDD_one);
+#else /* MR_ROBDD_USE_RGLB */
+ if (MR_ROBDD_IS_TERMINAL(f)) {
+ return f==MR_ROBDD_zero;
+ } else {
+ MR_ROBDD_DECLARE_VAR_ENTAILED_CACHE_ENTRY
+ int result;
+
+ MR_ROBDD_TRY_VAR_ENTAILED_CACHE(f, var);
+ if (f->value < var) {
+ result = MR_ROBDD_var_entailed(f->tr, var)
+ && MR_ROBDD_var_entailed(f->fa, var);
+ } else if (f->value == var) {
+ result = (f->fa==MR_ROBDD_zero);
+ } else /* f->value > var */ {
+ result = MR_FALSE;
+ }
+ MR_ROBDD_UPDATE_VAR_ENTAILED_CACHE(f, var, result);
+ return result;
+ }
+#endif /* MR_ROBDD_NEW */
+}
+
+/*
+** returns a MR_ROBDD_bitset of all the variables implied by f. A variable i
+** is implied by f iff
+**
+** MR_ROBDD_BITSET_IS_MEMBER(*result, i)
+*/
+
+#if !defined(MR_ROBDD_NEW)
+MR_ROBDD_bitset *
+MR_ROBDD_vars_entailed(MR_ROBDD_node *f, int MR_ROBDD_topvar)
+{
+ static MR_ROBDD_bitset def_vars;
+ int i;
+
+ MR_ROBDD_BITSET_CLEAR(def_vars);
+
+ for (i=0; i<MR_ROBDD_topvar; ++i) {
+ if (MR_ROBDD_var_entailed(f, i)) {
+ MR_ROBDD_BITSET_ADD_ELEMENT(def_vars,i);
+ }
+ }
+ return &def_vars;
+}
+
+#elif 0 /* not using this version */
+
+int
+MR_ROBDD_topvar(MR_ROBDD_node *f, int n)
+{
+ int n1;
+
+ if (MR_ROBDD_IS_TERMINAL(f)) return n;
+
+ n1 = MR_ROBDD_topvar(f->tr, f->value);
+ if (n1 > n) {
+ n = n1;
+ }
+ return MR_ROBDD_topvar(f->fa, n);
+}
+
+MR_ROBDD_bitset *
+MR_ROBDD_vars_entailed(MR_ROBDD_node *f)
+{
+ static MR_ROBDD_bitset def_vars;
+ int i = MR_ROBDD_topvar(f, 0);
+
+ MR_ROBDD_BITSET_CLEAR(def_vars);
+
+ for (; i >= 0; --i) {
+ if (MR_ROBDD_var_entailed(f, i)) {
+ MR_ROBDD_BITSET_ADD_ELEMENT(def_vars,i);
+ }
+ }
+ return &def_vars;
+}
+
+#else /* MR_ROBDD_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;
+/*
+** these variables should be local to both MR_ROBDD_vars_entailed and
+** MR_ROBDD_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 MR_ROBDD_bitset MR_ROBDD_this_path;
+static MR_ROBDD_bitset MR_ROBDD_entailed;
+
+void
+MR_ROBDD_vars_entailed_aux(MR_ROBDD_node *f)
+{
+ while (!MR_ROBDD_IS_TERMINAL(f)) {
+ int word = MR_ROBDD_BITSET_WORD(f->value);
+ MR_ROBDD_bitmask mask = MR_ROBDD_BITSET_MASK(f->value);
+
+ /* turn on bit for then branch */
+ MR_ROBDD_BITSET_ADD(MR_ROBDD_this_path,word,mask);
+ MR_ROBDD_vars_entailed_aux(f->tr);
+ /* turn it off for the else branch */
+ MR_ROBDD_BITSET_TOGGLE(MR_ROBDD_this_path,word,mask);
+ f = f->fa;
+ }
+ /* needn't do anything for false terminals */
+ if (f == MR_ROBDD_one) {
+ MR_ROBDD_BITSET_INTERSECTION(MR_ROBDD_entailed, MR_ROBDD_entailed,
+ MR_ROBDD_this_path);
}
-#endif /* NEW && !OLD_VARS_ENTAILED */
-#endif /* NEW */
+}
+
+/*
+** returns a MR_ROBDD_bitset of all the variables implied by f. A variable i
+** is implied by f iff
+**
+** MR_ROBDD_BITSET_IS_MEMBER(*result, i)
+*/
+
+MR_ROBDD_bitset *
+MR_ROBDD_vars_entailed(MR_ROBDD_node *f)
+{
+ MR_ROBDD_BITSET_CLEAR(MR_ROBDD_this_path);
+ MR_ROBDD_BITSET_UNIVERSE(MR_ROBDD_entailed);
+
+ MR_ROBDD_vars_entailed_aux(f);
+ return &MR_ROBDD_entailed;
+}
+#else /* MR_ROBDD_NEW && !OLD_VARS_ENTAILED */
+/*
+** returns a MR_ROBDD_bitset of all the variables implied by f. A variable i
+** is implied by f iff
+**
+** MR_ROBDD_BITSET_IS_MEMBER(*result, i)
+*/
+
+MR_ROBDD_bitset *
+MR_ROBDD_vars_entailed(MR_ROBDD_node *f)
+{
+ static MR_ROBDD_bitset tmp_bitset;
+ MR_ROBDD_DECLARE_UNARY_BITSET_CACHE_ENTRY
+
+ if (f == MR_ROBDD_zero) {
+ MR_ROBDD_BITSET_UNIVERSE(tmp_bitset);
+ } else if (f == MR_ROBDD_one) {
+ MR_ROBDD_BITSET_CLEAR(tmp_bitset);
+ } else {
+ MR_ROBDD_bitset bs;
+
+ MR_ROBDD_TRY_UNARY_BITSET_CACHE(f, MR_ROBDD_vars_entailed);
+ tmp_bitset = *MR_ROBDD_vars_entailed(f->tr);
+ bs = *MR_ROBDD_vars_entailed(f->fa);
+ MR_ROBDD_BITSET_INTERSECTION(tmp_bitset, tmp_bitset, bs);
+ if (f->fa == MR_ROBDD_zero) {
+ MR_ROBDD_BITSET_ADD_ELEMENT(tmp_bitset, f->value);
+ }
+ MR_ROBDD_UPDATE_UNARY_BITSET_CACHE(f, tmp_bitset,
+ MR_ROBDD_vars_entailed);
+ }
+ return &tmp_bitset;
+}
+
+#endif /* MR_ROBDD_NEW && !OLD_VARS_ENTAILED */
+#endif /* MR_ROBDD_NEW */
/****************************************************************
- Set Sharing Operations
+ Set Sharing Operations
****************************************************************/
-#if defined(SHARING)
+#if defined(MR_ROBDD_SHARING)
+
+/*
+** returns the Boolean function
+** ~1&~2&...~n | 1&~2&...~n | ~1&2&...~n | ~1&~2&...n
+*/
+
+MR_ROBDD_node *
+MR_ROBDD_init_set_sharing(int n)
+{
+ MR_ROBDD_node *result = MR_ROBDD_one;
+ MR_ROBDD_node *other = MR_ROBDD_one;
+
+ while (n>1) {
+ other = MR_ROBDD_make_node(n, MR_ROBDD_zero, other);
+ result = MR_ROBDD_make_node(--n, other, result);
+ }
+
+ return result;
+}
+
+#if defined(MR_ROBDD_NEW)
+
+MR_ROBDD_DECLARE_FN_COUNT(MR_ROBDD_complete_one_or)
+
+/* the same as MR_ROBDD_lub(MR_ROBDD_complete_one(f), prev) */
+MR_ROBDD_node *
+MR_ROBDD_complete_one_or(MR_ROBDD_node *f, MR_ROBDD_node *prev)
+{
+ MR_ROBDD_node *result;
+ MR_ROBDD_node *MR_ROBDD_complete_one(MR_ROBDD_node *f);
+ MR_ROBDD_DECLARE_ASYM_BIN_CACHE_ENTRY
+
+ MR_ROBDD_COUNT_FN(MR_ROBDD_complete_one_or);
+
+ if (MR_ROBDD_IS_TERMINAL(prev)) {
+ return (prev==MR_ROBDD_one) ? MR_ROBDD_one : MR_ROBDD_complete_one(f);
+ }
+ if (MR_ROBDD_IS_TERMINAL(f)) {
+ return (f==MR_ROBDD_one) ? MR_ROBDD_one : prev;
+ }
+
+ MR_ROBDD_TRY_ASYM_BIN_CACHE(f, prev, MR_ROBDD_complete_one_or);
+
+ /*
+ ** we want to return:
+ ** MR_ROBDD_lub(MR_ROBDD_make_node(f->value,
+ ** MR_ROBDD_lub(MR_ROBDD_complete_one(f->tr),
+ ** MR_ROBDD_complete_one(f->fa)),
+ ** MR_ROBDD_complete_one(f->fa)),
+ ** prev);
+ ** but we want to unfold the outer MR_ROBDD_lub call, so we compare
+ ** prev->value and f->value. Actually, this isn't right when
+ ** f->value <= prev->value, because the MR_ROBDD_make_node call may return
+ ** a MR_ROBDD_node whose label is > prev->value, but in that case,
+ ** MR_ROBDD_lub(that, prev) = MR_ROBDD_make_node(prev->value,
+ ** MR_ROBDD_lub(that, prev->tr), MR_ROBDD_lub(that, prev->fa))
+ */
+
+ if (f->value < prev->value) {
+ MR_ROBDD_node *cfa = MR_ROBDD_complete_one_or(f->fa, prev);
+ result = MR_ROBDD_make_node(f->value,
+ MR_ROBDD_complete_one_or(f->tr, cfa), cfa);
+ } else if (f->value == prev->value) {
+ result = MR_ROBDD_make_node(f->value,
+ MR_ROBDD_complete_one_or(f->tr,
+ MR_ROBDD_complete_one_or(f->fa,
+ prev->tr)),
+ MR_ROBDD_complete_one_or(f->fa, prev->fa));
+ } else {
+ result = MR_ROBDD_make_node(prev->value,
+ MR_ROBDD_complete_one_or(f, prev->tr),
+ MR_ROBDD_complete_one_or(f, prev->fa));
+ }
+ MR_ROBDD_UPDATE_ASYM_BIN_CACHE(f, prev, result, MR_ROBDD_complete_one_or);
+ return result;
+}
+
+MR_ROBDD_DECLARE_FN_COUNT(MR_ROBDD_complete_one)
+
+MR_ROBDD_node *
+MR_ROBDD_complete_one(MR_ROBDD_node *f)
+{
+ MR_ROBDD_node *result, *cfa;
+ MR_ROBDD_DECLARE_UNARY_CACHE_ENTRY
+
+ MR_ROBDD_COUNT_FN(MR_ROBDD_complete_one);
+
+ if (MR_ROBDD_IS_TERMINAL(f)) {
+ return f;
+ }
+ MR_ROBDD_TRY_UNARY_CACHE(f, MR_ROBDD_complete_one);
+ cfa = MR_ROBDD_complete_one(f->fa);
+ result = MR_ROBDD_make_node(f->value,
+ MR_ROBDD_complete_one_or(f->tr, cfa), cfa);
+ MR_ROBDD_UPDATE_UNARY_CACHE(f, result, MR_ROBDD_complete_one);
+ return result;
+}
+
+MR_ROBDD_DECLARE_FN_COUNT(MR_ROBDD_complete_or)
+
+/* the same as MR_ROBDD_lub(MR_ROBDD_complete(f, g), prev) */
+MR_ROBDD_node *
+MR_ROBDD_complete_or(MR_ROBDD_node *f, MR_ROBDD_node *g, MR_ROBDD_node *prev)
+{
+ MR_ROBDD_node *result;
+ MR_ROBDD_node *lo, *hi;
+ MR_ROBDD_DECLARE_COMPLETE_OR_CACHE_ENTRY
-/* 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);
+ MR_ROBDD_COUNT_FN(MR_ROBDD_complete_or);
- return result;
+ if (prev == MR_ROBDD_one) {
+ return MR_ROBDD_one;
}
-#else /* !NEW */
-#define complete_or(x, y, z) lub(complete((x),(y)),(z))
+ if (f == g) {
+ return MR_ROBDD_lub(f, prev);
+ }
+ if (f == MR_ROBDD_zero || g == MR_ROBDD_zero) {
+ return prev;
+ }
+
+ if (f == MR_ROBDD_one) {
+ return MR_ROBDD_complete_one_or(g, prev);
+ }
+ if (g == MR_ROBDD_one) {
+ return MR_ROBDD_complete_one_or(f, prev);
+ }
+ if (prev == MR_ROBDD_zero) {
+ return MR_ROBDD_complete(f, g);
+ }
+
+ MR_ROBDD_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 = MR_ROBDD_make_node(prev->value,
+ MR_ROBDD_complete_or(lo, hi, prev->tr),
+ MR_ROBDD_complete_or(lo, hi, prev->fa));
+ } else if (prev->value == lo->value) {
+ if (lo->value == hi->value) {
+ MR_ROBDD_node *n = MR_ROBDD_complete_or(lo->tr, hi->tr, prev->tr);
+ n = MR_ROBDD_complete_or(lo->tr, hi->fa, n);
+ n = MR_ROBDD_complete_or(lo->fa, hi->tr, n);
+ result = MR_ROBDD_make_node(lo->value, n,
+ MR_ROBDD_complete_or(lo->fa, hi->fa, prev->fa));
+ } else {
+ MR_ROBDD_node *n = MR_ROBDD_complete_or(lo->fa, hi, prev->tr);
+ n = MR_ROBDD_complete_or(lo->tr, hi, n);
+ result = MR_ROBDD_make_node(lo->value, n,
+ MR_ROBDD_complete_or(lo->fa, hi, prev->fa));
+ }
+ } else if (lo->value == hi->value) {
+ MR_ROBDD_node *n = MR_ROBDD_complete_or(lo->tr, hi->tr, prev);
+ n = MR_ROBDD_complete_or(lo->tr, hi->fa, n);
+ n = MR_ROBDD_complete_or(lo->fa, hi->tr, n);
+ result = MR_ROBDD_make_node(lo->value, n,
+ MR_ROBDD_complete_or(lo->fa, hi->fa, prev));
+ } else {
+ MR_ROBDD_node *n = MR_ROBDD_complete_or(lo->fa, hi, prev);
+ result = MR_ROBDD_make_node(lo->value,
+ MR_ROBDD_complete_or(lo->tr, hi, n), n);
+ }
+ MR_ROBDD_UPDATE_COMPLETE_OR_CACHE(f, g, prev, result);
+
+ return result;
+}
+
+#else /* !MR_ROBDD_NEW */
+
+#define MR_ROBDD_complete_or(x, y, z) \
+ MR_ROBDD_lub(MR_ROBDD_complete((x),(y)),(z))
#endif
-DECLARE_FN_COUNT(complete)
+MR_ROBDD_DECLARE_FN_COUNT(MR_ROBDD_complete)
+
+MR_ROBDD_node *
+MR_ROBDD_complete(MR_ROBDD_node *f, MR_ROBDD_node *g)
+{
+ MR_ROBDD_node *result;
+ int fvar, gvar;
+ MR_ROBDD_DECLARE_BIN_CACHE_ENTRY
+
+ MR_ROBDD_COUNT_FN(MR_ROBDD_complete);
+
+ if (f == g) {
+ return f;
+ }
+ if (f == MR_ROBDD_zero || g == MR_ROBDD_zero) {
+ return MR_ROBDD_zero;
+ }
+
+ MR_ROBDD_TRY_BIN_CACHE(f, g, MR_ROBDD_complete);
+
+ fvar = (f == MR_ROBDD_one) ? MR_ROBDD_MAXVAR : f->value;
+ gvar = (g == MR_ROBDD_one) ? MR_ROBDD_MAXVAR : g->value;
+ if (fvar == gvar) {
+ result = MR_ROBDD_make_node(fvar,
+ MR_ROBDD_complete_or(f->fa, g->tr,
+ MR_ROBDD_complete_or(f->tr, g->tr,
+ MR_ROBDD_complete(f->tr,g->fa))),
+ MR_ROBDD_complete(f->fa,g->fa));
+ } else if (fvar < gvar) {
+ MR_ROBDD_node *cfa = MR_ROBDD_complete(f->fa, g);
+
+ result = MR_ROBDD_make_node(fvar, MR_ROBDD_complete_or(f->tr, g, cfa),
+ cfa);
+ } else /* fvar > gvar */ {
+ MR_ROBDD_node *cfa = MR_ROBDD_complete(f, g->fa);
+
+ result = MR_ROBDD_make_node(gvar, MR_ROBDD_complete_or(f, g->tr, cfa),
+ cfa);
+ }
+ MR_ROBDD_UPDATE_BIN_CACHE(f, g, result, MR_ROBDD_complete);
+ return result;
+}
+
+MR_ROBDD_DECLARE_FN_COUNT(MR_ROBDD_upclose)
+
+MR_ROBDD_node *
+MR_ROBDD_upclose(MR_ROBDD_node *f)
+{
+ MR_ROBDD_node *utr, *ufa, *result;
+ MR_ROBDD_DECLARE_UNARY_CACHE_ENTRY
+
+ MR_ROBDD_COUNT_FN(MR_ROBDD_upclose);
+
+ if (MR_ROBDD_IS_TERMINAL(f)) {
+ return f;
+ }
+ MR_ROBDD_TRY_UNARY_CACHE(f, MR_ROBDD_upclose);
+ utr = MR_ROBDD_upclose(f->tr);
+ ufa = MR_ROBDD_upclose(f->fa);
+ result = MR_ROBDD_make_node(f->value, MR_ROBDD_complete_or(utr, ufa, utr),
+ ufa);
+ MR_ROBDD_UPDATE_UNARY_CACHE(f, result, MR_ROBDD_upclose);
+ return result;
+}
+
+/*
+** MR_ROBDD_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.
+*/
+
+MR_ROBDD_node *
+MR_ROBDD_bin(MR_ROBDD_node *f, MR_ROBDD_node *g)
+{
+ if (f == MR_ROBDD_zero || g == MR_ROBDD_zero) {
+ return MR_ROBDD_zero;
+ } else if (f == MR_ROBDD_one) {
+ return MR_ROBDD_bin_univ(g);
+ } else if (g == MR_ROBDD_one) {
+ return MR_ROBDD_bin_univ(f);
+ } else {
+ MR_ROBDD_node *result;
+ MR_ROBDD_DECLARE_BIN_CACHE_ENTRY
+
+ MR_ROBDD_TRY_BIN_CACHE(f, g, MR_ROBDD_bin);
+
+ if (f->value == g->value) {
+ MR_ROBDD_node *th = MR_ROBDD_bin(f->tr, g->tr);
+ MR_ROBDD_node *el = MR_ROBDD_bin(f->tr, g->fa);
+
+ if (el != MR_ROBDD_one) {
+ el = MR_ROBDD_lub(el, MR_ROBDD_bin(f->fa, g->tr));
+ if (el != MR_ROBDD_one) {
+ el = MR_ROBDD_lub(el, MR_ROBDD_bin(f->fa, g->fa));
+ }
+ }
+ result = MR_ROBDD_make_node(f->value, th, el);
+ } else {
+ MR_ROBDD_node *tmp;
+
+ if (f->value > g->value) {
+ tmp = f; f = g; g = tmp;
+ }
+ /* now f->value < g->value */
+ tmp = MR_ROBDD_bin(f->tr, g);
+ if (tmp == MR_ROBDD_one)
+ return MR_ROBDD_one;
+ result = MR_ROBDD_make_node(f->value, tmp,
+ MR_ROBDD_lub(tmp, MR_ROBDD_bin(f->fa, g)));
+ }
+ MR_ROBDD_UPDATE_BIN_CACHE(f, g, result, MR_ROBDD_bin);
+ return result;
+ }
+}
-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)));
+/*
+** Auxilliary function for MR_ROBDD_bin: special case code for
+** MR_ROBDD_bin(f, MR_ROBDD_one).
+*/
+
+MR_ROBDD_node *
+MR_ROBDD_bin_univ(MR_ROBDD_node *f)
+{
+ MR_ROBDD_node *g;
+
+ if (MR_ROBDD_IS_TERMINAL(f)) {
+ return f;
+ }
+ g = MR_ROBDD_bin_univ(f->tr);
+ if (g == MR_ROBDD_one) {
+ return MR_ROBDD_one;
}
+ return MR_ROBDD_make_node(f->value, g,
+ MR_ROBDD_lub(g, MR_ROBDD_bin_univ(f->fa)));
+}
-#endif /* SHARING */
+#endif /* MR_ROBDD_SHARING */
/****************************************************************
- Initialization and Cleanup
+ Initialization and Cleanup
****************************************************************/
+#if defined(MR_ROBDD_STATISTICS)
+
+void
+MR_ROBDD_print_distribution(int array[], int MR_ROBDD_max)
+{
+ int count;
+ int sum;
+ int total, zero_count;
+
+ for (count=0, total=0; count<=MR_ROBDD_max; ++count) {
+ total += array[count];
+ }
+ zero_count = array[0];
+ for (count=0, sum=0; count<=MR_ROBDD_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], MR_ROBDD_PERCENTAGE(array[count],total),
+ sum, MR_ROBDD_PERCENTAGE(sum,total), sum-zero_count,
+ total == zero_count ? 999.999
+ : MR_ROBDD_PERCENTAGE(sum-zero_count, total-zero_count));
+ }
+ }
+ if (array[MR_ROBDD_max+1] > 0) {
+ printf(">%4d nodes:%6d %2.2f%%\n",
+ MR_ROBDD_max, array[MR_ROBDD_max],
+ MR_ROBDD_PERCENTAGE(array[MR_ROBDD_max],total));
+ }
+ printf("\n");
+}
+#endif /* MR_ROBDD_STATISTICS */
-#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);
+void
+MR_ROBDD_initRep(void)
+{
+ MR_ROBDD_INIT_FN_COUNT(MR_ROBDD_make_node);
+ MR_ROBDD_INIT_FN_COUNT(MR_ROBDD_variableRep);
+ MR_ROBDD_INIT_FN_COUNT(MR_ROBDD_implies);
+ MR_ROBDD_INIT_FN_COUNT(MR_ROBDD_lub);
+ MR_ROBDD_INIT_FN_COUNT(MR_ROBDD_glb);
+ MR_ROBDD_INIT_FN_COUNT(MR_ROBDD_restrict);
+ MR_ROBDD_INIT_FN_COUNT(MR_ROBDD_restrictThresh);
+ MR_ROBDD_INIT_FN_COUNT(MR_ROBDD_renameArray);
+ MR_ROBDD_INIT_FN_COUNT(MR_ROBDD_reverseRenameArray);
+ MR_ROBDD_INIT_FN_COUNT(MR_ROBDD_ite);
+#if defined(MR_ROBDD_USE_ITE_CONSTANT)
+ MR_ROBDD_INIT_FN_COUNT(MR_ROBDD_ite_constant);
+#endif /* MR_ROBDD_USE_ITE_CONSTANT */
+ MR_ROBDD_INIT_FN_COUNT(iff_conj);
+#if defined(MR_ROBDD_NEW)
+ MR_ROBDD_INIT_FN_COUNT(MR_ROBDD_ite_var);
+ MR_ROBDD_INIT_FN_COUNT(MR_ROBDD_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);
+#if defined(MR_ROBDD_SHARING)
+ #if defined(MR_ROBDD_NEW)
+ MR_ROBDD_INIT_FN_COUNT(MR_ROBDD_complete_one_or);
+ MR_ROBDD_INIT_FN_COUNT(MR_ROBDD_complete_one);
+ MR_ROBDD_INIT_FN_COUNT(MR_ROBDD_complete_or);
+ #endif /* MR_ROBDD_NEW */
+ MR_ROBDD_INIT_FN_COUNT(MR_ROBDD_complete);
+ MR_ROBDD_INIT_FN_COUNT(MR_ROBDD_upclose);
+#endif /* MR_ROBDD_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.
+ */
+
+ MR_ROBDD_INIT_UNIQUE_TABLE;
+
+ MR_ROBDD_init_caches();
+}
+
+void
+MR_ROBDD_init_caches(void)
+{
+ MR_ROBDD_INIT_CACHE(MR_ROBDD_ite);
+#if defined(MR_ROBDD_USE_ITE_CONSTANT)
+ MR_ROBDD_INIT_CACHE(MR_ROBDD_ite_constant);
+#endif /* MR_ROBDD_USE_ITE_CONSTANT */
+#if defined(MR_ROBDD_SHARING)
+ MR_ROBDD_INIT_CACHE(MR_ROBDD_upclose);
+ MR_ROBDD_INIT_CACHE(MR_ROBDD_bin);
+ MR_ROBDD_INIT_CACHE(MR_ROBDD_complete);
+#if defined(MR_ROBDD_NEW)
+ MR_ROBDD_INIT_CACHE(MR_ROBDD_complete_one);
+ MR_ROBDD_INIT_CACHE(MR_ROBDD_complete_or);
+ MR_ROBDD_INIT_CACHE(MR_ROBDD_complete_one_or);
+#endif /* MR_ROBDD_NEW */
+ MR_ROBDD_INIT_CACHE(MR_ROBDD_bin);
+#endif /* MR_ROBDD_SHARING */
+ MR_ROBDD_INIT_CACHE(MR_ROBDD_glb);
+ MR_ROBDD_INIT_CACHE(MR_ROBDD_lub);
+#if defined(MR_ROBDD_USE_RGLB)
+ MR_ROBDD_INIT_CACHE(rglb);
+ MR_ROBDD_INIT_CACHE(MR_ROBDD_var_entailed);
+#endif /* MR_ROBDD_USE_RGLB */
+#if defined(MR_ROBDD_NEW)
+ MR_ROBDD_INIT_CACHE(MR_ROBDD_ite_var);
+ MR_ROBDD_INIT_CACHE(MR_ROBDD_vars_entailed);
+#endif /* MR_ROBDD_NEW */
+}
+
+void
+MR_ROBDD_concludeRep(void)
+{
+#if defined(MR_ROBDD_STATISTICS)
+ MR_ROBDD_node *ptr;
+ int size_count[MR_ROBDD_MAX_COUNT+2];
+
+ int i, count;
+
+ printf("\n\n\n================ Operation Counts ================\n\n");
+ MR_ROBDD_PRINT_FN_COUNT(MR_ROBDD_make_node);
+ MR_ROBDD_PRINT_FN_COUNT(MR_ROBDD_variableRep);
+ MR_ROBDD_PRINT_FN_COUNT(MR_ROBDD_implies);
+ MR_ROBDD_PRINT_FN_COUNT(MR_ROBDD_lub);
+ MR_ROBDD_PRINT_FN_COUNT(MR_ROBDD_glb);
+ MR_ROBDD_PRINT_FN_COUNT(MR_ROBDD_restrict);
+ MR_ROBDD_PRINT_FN_COUNT(MR_ROBDD_restrictThresh);
+ MR_ROBDD_PRINT_FN_COUNT(MR_ROBDD_renameArray);
+ MR_ROBDD_PRINT_FN_COUNT(MR_ROBDD_reverseRenameArray);
+ MR_ROBDD_PRINT_FN_COUNT(MR_ROBDD_ite);
+#if defined(MR_ROBDD_USE_ITE_CONSTANT)
+ MR_ROBDD_PRINT_FN_COUNT(MR_ROBDD_ite_constant);
+#endif /* MR_ROBDD_USE_ITE_CONSTANT */
+ MR_ROBDD_PRINT_FN_COUNT(iff_conj);
+#if defined(MR_ROBDD_NEW)
+ MR_ROBDD_PRINT_FN_COUNT(MR_ROBDD_ite_var);
+ MR_ROBDD_PRINT_FN_COUNT(MR_ROBDD_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; i<UNIQUE_TABLE_SIZE; ++i) {
- for (ptr=unique_table[i],count=0;
- ptr!=NULL;
- ptr=ptr->unique,++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 */
+#if defined(MR_ROBDD_SHARING)
+ #if defined(MR_ROBDD_NEW)
+ MR_ROBDD_PRINT_FN_COUNT(MR_ROBDD_complete_one_or);
+ MR_ROBDD_PRINT_FN_COUNT(MR_ROBDD_complete_one);
+ MR_ROBDD_PRINT_FN_COUNT(MR_ROBDD_complete_or);
+ #endif /* MR_ROBDD_NEW */
+ MR_ROBDD_PRINT_FN_COUNT(MR_ROBDD_complete);
+ MR_ROBDD_PRINT_FN_COUNT(MR_ROBDD_upclose);
+#endif /* MR_ROBDD_SHARING */
+ printf("\n================ Cache Performance ================\n\n");
+ printf("%d nodes extant\n\n", MR_ROBDD_nodes_in_use());
+ printf("Unique table: %d hits, %d misses, %f%% hits\n",
+ MR_ROBDD_unique_table_hits, MR_ROBDD_unique_table_misses,
+ MR_ROBDD_PERCENTAGE(MR_ROBDD_unique_table_hits,
+ MR_ROBDD_unique_table_hits+MR_ROBDD_unique_table_misses));
+ MR_memset(size_count, 0, sizeof(size_count));
+ for (i=0; i<MR_ROBDD_UNIQUE_TABLE_SIZE; ++i) {
+ count = 0;
+ ptr=MR_ROBDD_REVEAL_NODE_POINTER(MR_ROBDD_unique_table[i]);
+ while (ptr!=NULL) {
+ ptr=MR_ROBDD_REVEAL_NODE_POINTER(ptr->unique),++count;
+ }
+ ++size_count[(count <= MR_ROBDD_MAX_COUNT
+ ? count : MR_ROBDD_MAX_COUNT + 1)];
}
+ MR_ROBDD_print_distribution(size_count, MR_ROBDD_MAX_COUNT);
-
+ MR_ROBDD_PRINT_CACHE_PERFORMANCE(MR_ROBDD_ite);
+#if defined(MR_ROBDD_USE_ITE_CONSTANT)
+ MR_ROBDD_PRINT_CACHE_PERFORMANCE(MR_ROBDD_ite_constant);
+#endif /* MR_ROBDD_USE_ITE_CONSTANT */
+ MR_ROBDD_PRINT_CACHE_PERFORMANCE(MR_ROBDD_lub);
+ MR_ROBDD_PRINT_CACHE_PERFORMANCE(MR_ROBDD_glb);
+#if defined(MR_ROBDD_SHARING)
+ MR_ROBDD_PRINT_CACHE_PERFORMANCE(MR_ROBDD_upclose);
+ MR_ROBDD_PRINT_CACHE_PERFORMANCE(MR_ROBDD_complete);
+ #if defined(MR_ROBDD_NEW)
+ MR_ROBDD_PRINT_CACHE_PERFORMANCE(MR_ROBDD_complete_or);
+ MR_ROBDD_PRINT_CACHE_PERFORMANCE(MR_ROBDD_complete_one_or);
+ MR_ROBDD_PRINT_CACHE_PERFORMANCE(MR_ROBDD_complete_one);
+ #endif /* MR_ROBDD_NEW */
+#endif /* MR_ROBDD_SHARING */
+#if defined(MR_ROBDD_USE_RGLB)
+ MR_ROBDD_PRINT_CACHE_PERFORMANCE(rglb);
+#endif /* MR_ROBDD_USE_RGLB */
+#if defined(MR_ROBDD_NEW)
+ MR_ROBDD_PRINT_CACHE_PERFORMANCE(MR_ROBDD_ite_var);
+ MR_ROBDD_PRINT_CACHE_PERFORMANCE(MR_ROBDD_vars_entailed);
+#endif /* MR_ROBDD_NEW */
+#endif /* MR_ROBDD_STATISTICS */
+ }
/****************************************************************
- Testing Support
+ 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;
+/*
+** special version of MR_ROBDD_iff_conj_array() that is the fast version
+** no matter which options are selected. I hope this gives more reliable
+** test times.
+*/
+
+MR_ROBDD_node *
+MR_ROBDD_testing_iff_conj_array(int v0, int n, int arr[])
+{
+ MR_ROBDD_node *thens = MR_ROBDD_one;
+ MR_ROBDD_node *elses = MR_ROBDD_zero;
+ int *ptr;
+ int vi;
+
+ /*
+ ** first build part of graph below v0. For this, we build two
+ ** subgraphs: MR_ROBDD_one for when v0 is true, and MR_ROBDD_one for false.
+ ** These are called thens and elses.
+ **/
+
+ for (ptr=&arr[n-1]; ptr>=arr && v0<(vi=*ptr); --ptr) {
+ thens = MR_ROBDD_make_node(vi, thens, MR_ROBDD_zero);
+ elses = MR_ROBDD_make_node(vi, elses, MR_ROBDD_one);
}
-static int intcompare(const void *a, const void *b)
- {
- return (*((int *)a) - *((int *)b));
+ /* make v0 MR_ROBDD_node */
+ thens = MR_ROBDD_make_node(v0,thens,elses);
+
+ /*
+ ** Finally build part of graph above v0. For this, we build
+ ** only MR_ROBDD_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 = MR_ROBDD_make_node(v0,MR_ROBDD_zero,MR_ROBDD_one);
+
+ do {
+ vi = *ptr;
+ thens = MR_ROBDD_make_node(vi, thens, elses);
+ } while (--ptr >= arr);
}
+
+ return thens;
+}
+
+static int MR_ROBDD_intcompare(const void *a, const void *b)
+{
+ return (* ((int *) a) - * ((int *) b));
+}
--------------------------------------------------------------------------
mercury-reviews mailing list
post: mercury-reviews at cs.mu.oz.au
administrative address: owner-mercury-reviews at cs.mu.oz.au
unsubscribe: Address: mercury-reviews-request at cs.mu.oz.au Message: unsubscribe
subscribe: Address: mercury-reviews-request at cs.mu.oz.au Message: subscribe
--------------------------------------------------------------------------
More information about the reviews
mailing list