[m-rev.] bryant.[ch]
Zoltan Somogyi
zs at cs.mu.OZ.AU
Tue May 7 15:08:35 AEST 2002
For review by David.
Zoltan.
robdd/bryant.h:
Make the definitions of TRUE and FALSE conditional.
robdd/bryant.c:
Provide missing trivial definitions if COMPUTED_TABLE is not defined.
Indent the code to match the level of #ifdef nesting, as per our coding
standards.
cvs diff: Diffing .
Index: bryant.c
===================================================================
RCS file: /home/mercury1/repository/mercury/robdd/bryant.c,v
retrieving revision 1.1.12.3
diff -u -r1.1.12.3 bryant.c
--- bryant.c 15 May 2001 01:50:04 -0000 1.1.12.3
+++ bryant.c 6 May 2002 07:52:18 -0000
@@ -16,7 +16,6 @@
Controlling #defined Symbols
-
This code is conditionalized on a number of #defined symbols. They are:
STATISTICS Controls collecting of computed and unique
@@ -93,7 +92,6 @@
and so should be avoided. In this case we use a
table where possible to avoid shifting.
-
*****************************************************************/
#include "mercury_imp.h"
@@ -104,7 +102,6 @@
#include <limits.h>
#include "bryant.h"
-
#ifdef BRYANT_CONSERVATIVE_GC
/* Don't use pools of nodes with the conservative GC. */
@@ -121,8 +118,10 @@
#define BRYANT_memset(d, c, n) MR_memset(d, c, n)
#else /* !BRYANT_CONSERVATIVE_GC */
+
#define POOL
#define BRYANT_memset(d, c, n) memset(d, c, n)
+
#endif /* BRYANT_CONSERVATIVE_GC */
#define REVEAL_NODE_POINTER(p) ((node *) REVEAL_POINTER(p))
@@ -130,24 +129,23 @@
#define UNUSED_MAPPING -1 /* this MUST BE -1 */
#if !defined(max)
-#define max(a,b) ((a)<(b) ? (b) : (a))
+ #define max(a,b) ((a)<(b) ? (b) : (a))
#endif
#if !defined(min)
-#define min(a,b) ((a)<(b) ? (a) : (b))
+ #define min(a,b) ((a)<(b) ? (a) : (b))
#endif
#define PERCENTAGE(x,y) ((100.0 * (float)(x)) / (float)(y))
#ifdef POOL
-typedef struct pool {
+ typedef struct pool {
node data[POOL_SIZE];
struct pool *prev;
-} pool;
+ } pool;
#endif POOL
-
#if defined(NO_CHEAP_SHIFT) && BITS_PER_WORD == 32
-bitmask following_bits[BITS_PER_WORD] =
+ bitmask following_bits[BITS_PER_WORD] =
{ 0xffffffff, 0xfffffffe, 0xfffffffc, 0xfffffff8,
0xfffffff0, 0xffffffe0, 0xffffffc0, 0xffffff80,
0xffffff00, 0xfffffe00, 0xfffffc00, 0xfffff800,
@@ -158,7 +156,7 @@
0xf0000000, 0xe0000000, 0xc0000000, 0x80000000
};
-bitmask preceding_bits[BITS_PER_WORD] =
+ bitmask preceding_bits[BITS_PER_WORD] =
{ 0x00000001, 0x00000003, 0x00000007, 0x0000000f,
0x0000001f, 0x0000003f, 0x0000007f, 0x000000ff,
0x000001ff, 0x000003ff, 0x000007ff, 0x00000fff,
@@ -170,7 +168,6 @@
};
#endif
-
unsigned char first_one_bit[256] =
{255, 0, 1, 0, 2, 0, 1, 0, 3, 0, 1, 0, 2, 0, 1, 0, /* 16 */
4, 0, 1, 0, 2, 0, 1, 0, 3, 0, 1, 0, 2, 0, 1, 0, /* 32 */
@@ -209,7 +206,6 @@
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;
@@ -219,116 +215,117 @@
****************************************************************/
-
#if defined(COMPUTED_TABLE) && defined(CLEAR_CACHES)
-#define CLEAR_CACHE(op) \
-BRYANT_memset(op##_computed_cache, 0, sizeof(op##_computed_cache))
+ #define CLEAR_CACHE(op) \
+ BRYANT_memset(op##_computed_cache, 0, sizeof(op##_computed_cache))
#else /* !CLEAR_CACHES || !COMPUTED_TABLE */
-#define CLEAR_CACHE(op)
+ #define CLEAR_CACHE(op)
#endif
-
#if defined(STATISTICS)
-/* The largest bucket size to be separately counted. Larger buckets
- * will be listed as "> MAX_COUNT."
- */
-#define MAX_COUNT 1000
-
-int unique_table_hits, unique_table_misses;
-
-#define DECLARE_FN_COUNT(op) int op##_count;
+ /* The largest bucket size to be separately counted. Larger buckets
+ * will be listed as "> MAX_COUNT."
+ */
+ #define MAX_COUNT 1000
+
+ int unique_table_hits, unique_table_misses;
+
+ #define DECLARE_FN_COUNT(op) int op##_count;
+
+ #define COUNT_FN(fn) (++fn##_count)
+
+ #define INIT_FN_COUNT(fn) fn##_count = 0
+ #define PRINT_FN_COUNT(fn) \
+ if (fn##_count!=0) printf("%6d calls to " #fn "\n", fn##_count);
+
+ #define COUNT_UNIQUE_HIT (++unique_table_hits)
+ #define COUNT_UNIQUE_MISS (++unique_table_misses)
+
+ #if defined(COMPUTED_TABLE)
+
+ #define COUNT_HIT(op) (++op##_computed_hits)
+ #define COUNT_MISS(op) (++op##_computed_misses, ++cache->count)
+ #define INIT_CACHE(op) \
+ do { \
+ op##_computed_misses = 0; \
+ op##_computed_hits = 0; \
+ CLEAR_CACHE(op); \
+ } while (0)
+
+ #define CACHE_COUNT_MEMBER int count;
+ #define PRINT_CACHE_PERFORMANCE(op) \
+ do { \
+ if (op##_computed_misses > 0 ) { \
+ int i, size_count[MAX_COUNT+2]; \
+ printf(#op " computed table: %d hits, %d misses, %.2f%% hit rate\n",\
+ op##_computed_hits, op##_computed_misses, \
+ PERCENTAGE(op##_computed_hits, \
+ op##_computed_hits + op##_computed_misses));\
+ BRYANT_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)
-#define COUNT_FN(fn) (++fn##_count)
+ #else /* !COMPUTED_TABLE */
-#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 PRINT_CACHE_PERFORMANCE(op)
-#define COUNT_UNIQUE_HIT (++unique_table_hits)
-#define COUNT_UNIQUE_MISS (++unique_table_misses)
+ #endif /* COMPUTED_TABLE */
+#else /* ! STATISTICS */
-#if defined(COMPUTED_TABLE)
+ #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 */
-#define COUNT_HIT(op) (++op##_computed_hits)
-#define COUNT_MISS(op) (++op##_computed_misses, ++cache->count)
-#define INIT_CACHE(op) \
- do { \
- op##_computed_misses = 0; \
- op##_computed_hits = 0; \
- CLEAR_CACHE(op); \
- } while (0)
-
-#define CACHE_COUNT_MEMBER int count;
-#define PRINT_CACHE_PERFORMANCE(op) \
-do { \
- if (op##_computed_misses > 0 ) { \
- int i, size_count[MAX_COUNT+2]; \
- printf(#op " computed table: %d hits, %d misses, %.2f%% hit rate\n",\
- op##_computed_hits, op##_computed_misses, \
- PERCENTAGE(op##_computed_hits, \
- op##_computed_hits + op##_computed_misses)); \
- BRYANT_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);
+ #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)
+ #define DIRECT_EQUAL_TEST(f,g,result)
+ #define ELSE_TRY_EQUAL_TEST(f,g,result)
#endif
#if defined(CLEAR_CACHES)
-#if defined(POOL)
-#define INIT_UNIQUE_TABLE \
- do { \
- BRYANT_memset(unique_table, (char) 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; \
- node_count = 0; \
- } while (0)
-#else /* !POOL */
-#define INIT_UNIQUE_TABLE \
- BRYANT_memset(unique_table, (char) 0, sizeof(unique_table));
-#endif /* POOL */
+ #if defined(POOL)
+ #define INIT_UNIQUE_TABLE \
+ do { \
+ BRYANT_memset(unique_table, (char) 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; \
+ node_count = 0; \
+ } while (0)
+
+ #else /* !POOL */
+ #define INIT_UNIQUE_TABLE \
+ BRYANT_memset(unique_table, (char) 0, sizeof(unique_table));
+ #endif /* POOL */
#else /* !CLEAR_CACHES */
-#define INIT_UNIQUE_TABLE
+ #define INIT_UNIQUE_TABLE
#endif /* CLEAR_CACHES */
-
-
/********************************************************************
Caching of computed values
@@ -347,161 +344,156 @@
#if defined(COMPUTED_TABLE)
-#if defined(STATISTICS)
-#define DECLARE_CACHE(op,type) \
-static int op##_computed_hits; \
-static int op##_computed_misses; \
-static type op##_computed_cache[COMPUTED_TABLE_SIZE]
-#else /* !STATISTICS */
-#define DECLARE_CACHE(op,type) \
-static type op##_computed_cache[COMPUTED_TABLE_SIZE]
-#endif /* STATISTICS */
+ #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)
+ #define TERNARY_NODE_HASH(f,g,h) \
+ (((INTCAST(f)>>4)+INTCAST(g)+(INTCAST(h)<<1)) % COMPUTED_TABLE_SIZE)
-typedef struct {
+ 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)
+ } ite_cache_entry;
+ DECLARE_CACHE(ite, ite_cache_entry);
+ #if defined(USE_ITE_CONSTANT)
+ DECLARE_CACHE(ite_constant, ite_cache_entry);
+ #endif /* USE_ITE_CONSTANT */
+
+ #define DECLARE_ITE_CACHE_ENTRY ite_cache_entry *cache;
+
+ #define TRY_ITE_CACHE(n1,n2,n3,op) \
+ do { \
+ cache = &op##_computed_cache[TERNARY_NODE_HASH(n1,n2,n3)]; \
+ if (cache->f==n1 && cache->g==n2 && cache->h==n3) { \
+ COUNT_HIT(op); \
+ return cache->result; \
+ } \
+ } while (0)
+
+ #define UPDATE_ITE_CACHE(n1,n2,n3,node,op) \
+ do { \
+ cache->f = n1; \
+ cache->g = n2; \
+ cache->h = n3; \
+ cache->result = node; \
+ COUNT_MISS(op); \
+ } while (0)
/******************** the cache for unary operations ************/
-#define UNARY_NODE_HASH(a) \
+ #define UNARY_NODE_HASH(a) \
(INTCAST(a) % COMPUTED_TABLE_SIZE)
-typedef struct {
+ 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)
+ } unary_cache_entry;
+ #if defined(SHARING)
+ DECLARE_CACHE(upclose, unary_cache_entry);
+ #if defined(NEW)
+ DECLARE_CACHE(complete_one, unary_cache_entry);
+ #endif /* NEW */
+ #endif /* SHARING */
+
+ #define DECLARE_UNARY_CACHE_ENTRY unary_cache_entry *cache;
+
+ #define UPDATE_UNARY_CACHE(n,node,op) \
+ do { \
+ cache->f = n; \
+ cache->result = node; \
+ COUNT_MISS(op); \
+ } while (0)
+
+ #define TRY_UNARY_CACHE(n,op) \
+ do { \
+ cache = &((op##_computed_cache)[UNARY_NODE_HASH(n)]); \
+ if (cache->f==(n)) { \
+ COUNT_HIT(op); \
+ return cache->result; \
+ } \
+ } while (0)
/******************** the cache for var_entailed ************/
-#define VAR_ENTAILED_HASH(a,n) \
+ #define VAR_ENTAILED_HASH(a,n) \
((INTCAST(a)+n) % COMPUTED_TABLE_SIZE)
-typedef struct {
+ typedef struct {
node *f;
int n;
int result;
CACHE_COUNT_MEMBER
-} var_entailed_cache_entry;
-
-#if defined(USE_RGLB)
-DECLARE_CACHE(var_entailed, var_entailed_cache_entry);
-#endif /* USE_RGLB */
-
-#define DECLARE_VAR_ENTAILED_CACHE_ENTRY var_entailed_cache_entry *cache;
-
-#define UPDATE_VAR_ENTAILED_CACHE(node,var,val) \
-do { \
- cache->f = node; \
- cache->n = var; \
- cache->result = val; \
- COUNT_MISS(var_entailed); \
-} while (0)
-
-#define TRY_VAR_ENTAILED_CACHE(node,var) \
-do { \
- cache = &((var_entailed_computed_cache) \
- [VAR_ENTAILED_HASH(node,var)]); \
- if (cache->f==(node) && cache->n==(var)) { \
- COUNT_HIT(op); \
- return cache->result; \
- } \
-} while (0)
+ } var_entailed_cache_entry;
+ #if defined(USE_RGLB)
+ DECLARE_CACHE(var_entailed, var_entailed_cache_entry);
+ #endif /* USE_RGLB */
+
+ #define DECLARE_VAR_ENTAILED_CACHE_ENTRY var_entailed_cache_entry *cache;
+
+ #define UPDATE_VAR_ENTAILED_CACHE(node,var,val) \
+ do { \
+ cache->f = node; \
+ cache->n = var; \
+ cache->result = val; \
+ COUNT_MISS(var_entailed); \
+ } while (0)
+
+ #define TRY_VAR_ENTAILED_CACHE(node,var) \
+ do { \
+ cache = &((var_entailed_computed_cache) \
+ [VAR_ENTAILED_HASH(node,var)]); \
+ if (cache->f==(node) && cache->n==(var)) { \
+ COUNT_HIT(op); \
+ return cache->result; \
+ } \
+ } while (0)
/**************** the cache for unary set-valued operations ********/
-typedef struct {
+ typedef struct {
node *f;
bitset result;
CACHE_COUNT_MEMBER
-} unary_bitset_cache_entry;
+ } unary_bitset_cache_entry;
-#if defined(NEW)
-DECLARE_CACHE(vars_entailed, unary_bitset_cache_entry);
-#endif
+ #if defined(NEW)
+ DECLARE_CACHE(vars_entailed, unary_bitset_cache_entry);
+ #endif
-#define DECLARE_UNARY_BITSET_CACHE_ENTRY \
+ #define DECLARE_UNARY_BITSET_CACHE_ENTRY \
unary_bitset_cache_entry *cache;
-
-#define UPDATE_UNARY_BITSET_CACHE(n,set,op) \
-do { \
- cache->f = n; \
- cache->result = set; \
- COUNT_MISS(op); \
-} while (0)
-
-#define TRY_UNARY_BITSET_CACHE(n,op) \
-do { \
- cache = &((op##_computed_cache)[UNARY_NODE_HASH(n)]); \
- if (cache->f==(n)) { \
- COUNT_HIT(op); \
- return &cache->result; \
- } \
-} while (0)
-
+ #define UPDATE_UNARY_BITSET_CACHE(n,set,op) \
+ do { \
+ cache->f = n; \
+ cache->result = set; \
+ COUNT_MISS(op); \
+ } while (0)
+
+ #define TRY_UNARY_BITSET_CACHE(n,op) \
+ do { \
+ cache = &((op##_computed_cache)[UNARY_NODE_HASH(n)]); \
+ if (cache->f==(n)) { \
+ COUNT_HIT(op); \
+ return &cache->result; \
+ } \
+ } while (0)
/******************** the cache for symmetric binary operations ************/
@@ -512,215 +504,231 @@
* they won't be changed (or exchanged) before UPDATE_BIN_CACHE is called.
*/
-#define BINARY_NODE_HASH(a,b) \
+ #define BINARY_NODE_HASH(a,b) \
((INTCAST(a)+(INTCAST(b)<<1)) % COMPUTED_TABLE_SIZE)
-typedef struct {
+ typedef struct {
node *f;
node *g;
node *result;
CACHE_COUNT_MEMBER
-} bin_cache_entry;
-
-DECLARE_CACHE(glb, bin_cache_entry);
-DECLARE_CACHE(lub, bin_cache_entry);
-#if defined(SHARING)
-DECLARE_CACHE(bin, bin_cache_entry);
-DECLARE_CACHE(complete, bin_cache_entry);
-#endif
-
-#define DECLARE_BIN_CACHE_ENTRY bin_cache_entry *cache;
+ } bin_cache_entry;
-#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)
+ DECLARE_CACHE(glb, bin_cache_entry);
+ DECLARE_CACHE(lub, bin_cache_entry);
+ #if defined(SHARING)
+ DECLARE_CACHE(bin, bin_cache_entry);
+ DECLARE_CACHE(complete, bin_cache_entry);
+ #endif
+
+ #define DECLARE_BIN_CACHE_ENTRY bin_cache_entry *cache;
+
+ #define UPDATE_BIN_CACHE(n1,n2,node,op) \
+ do { \
+ cache->f = n1; \
+ cache->g = n2; \
+ cache->result = node; \
+ COUNT_MISS(op); \
+ } while (0)
+
+ #define TRY_BIN_CACHE(n1,n2,op) \
+ do { \
+ if (n2 < n1) { node *temp = (n2); (n2) = (n1); (n1) = temp; }\
+ cache = &((op##_computed_cache)[BINARY_NODE_HASH(n1,n2)]);\
+ if (cache->f==(n1) && cache->g==(n2)) { \
+ COUNT_HIT(op); \
+ return cache->result; \
+ } \
+ } while (0)
/******************** the cache for asymmetric binary operations ************/
-#if defined(SHARING) && defined(NEW)
-DECLARE_CACHE(complete_one_or, bin_cache_entry);
-#endif /* SHARING && NEW */
+ #if defined(SHARING) && defined(NEW)
+ DECLARE_CACHE(complete_one_or, bin_cache_entry);
+ #endif /* SHARING && NEW */
-#if defined(USE_THRESH)
-DECLARE_CACHE(restrictThresh, bin_cache_entry);
-#endif /* USE_THRESH */
+ #if defined(USE_THRESH)
+ DECLARE_CACHE(restrictThresh, bin_cache_entry);
+ #endif /* USE_THRESH */
-#if (defined(SHARING) && defined(NEW)) || defined(USE_THRESH)
+ #if (defined(SHARING) && defined(NEW)) || defined(USE_THRESH)
-#define DECLARE_ASYM_BIN_CACHE_ENTRY bin_cache_entry *cache;
+ #define DECLARE_ASYM_BIN_CACHE_ENTRY bin_cache_entry *cache;
-#define UPDATE_ASYM_BIN_CACHE(n1,n2,node,op) \
+ #define UPDATE_ASYM_BIN_CACHE(n1,n2,node,op) \
UPDATE_BIN_CACHE(n1,n2,node,op)
-#define TRY_ASYM_BIN_CACHE(n1,n2,op) \
-do { \
- cache = &((op##_computed_cache)[BINARY_NODE_HASH(n1,n2)]); \
- if (cache->f==(n1) && cache->g==(n2)) { \
- COUNT_HIT(op); \
- return cache->result; \
- } \
-} while (0)
-#endif /* (SHARING && NEW) || USE_THRESH */
-
-/**************************** the cache for rglb ***********************/
-
-#if defined(USE_RGLB)
+ #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)
-typedef struct {
- node *f;
- node *g;
- node *result;
- int thresh;
- CACHE_COUNT_MEMBER
-} rglb_cache_entry;
+ #endif /* (SHARING && NEW) || USE_THRESH */
-DECLARE_CACHE(rglb, rglb_cache_entry);
+/**************************** the cache for rglb ***********************/
-#define DECLARE_RGLB_CACHE_ENTRY rglb_cache_entry *cache;
+ #if defined(USE_RGLB)
-#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)
+ typedef struct {
+ node *f;
+ node *g;
+ node *result;
+ int thresh;
+ CACHE_COUNT_MEMBER
+ } rglb_cache_entry;
+
+ DECLARE_CACHE(rglb, rglb_cache_entry);
+
+ #define DECLARE_RGLB_CACHE_ENTRY rglb_cache_entry *cache;
+
+ #define TRY_RGLB_CACHE(n1,n2,th) \
+ do { \
+ if (n2 < n1) { node *temp = (n2); (n2) = (n1); (n1) = temp; }\
+ cache = &rglb_computed_cache[BINARY_NODE_HASH(n1,n2)]; \
+ if (cache->f==(n1) && cache->g==(n2) && \
+ cache->thresh >= th) { \
+ COUNT_HIT(rglb); \
+ if (cache->thresh == th) return cache->result; \
+ return restrictThresh(th, cache->result); \
+ } \
+ } while (0)
+
+ #define UPDATE_RGLB_CACHE(n1,n2,th,node) \
+ do { \
+ cache->f = n1; \
+ cache->g = n2; \
+ cache->thresh = th; \
+ cache->result = node; \
+ COUNT_MISS(rglb); \
+ } while (0)
-#endif /* USE_RGLB */
+ #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;
+ #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);
+ DECLARE_CACHE(complete_or, complete_or_cache_entry);
-#define DECLARE_COMPLETE_OR_CACHE_ENTRY complete_or_cache_entry *cache;
+ #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)
+ #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 */
+ #endif /* SHARING && NEW */
/**************************** the cache for ite_var ***********************/
-#if defined(NEW)
+ #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;
+ #define ITE_VAR_COMPUTED_HASH(f,g,h) \
+ ((f+INTCAST(g)+(INTCAST(h)<<1)) % COMPUTED_TABLE_SIZE)
-DECLARE_CACHE(ite_var, ite_var_cache_entry);
+ typedef struct {
+ int f;
+ node *g;
+ node *h;
+ node *result;
+ CACHE_COUNT_MEMBER
+ } ite_var_cache_entry;
-#define DECLARE_ITE_VAR_CACHE_ENTRY ite_var_cache_entry *cache;
+ DECLARE_CACHE(ite_var, ite_var_cache_entry);
-#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)
+ #define DECLARE_ITE_VAR_CACHE_ENTRY ite_var_cache_entry *cache;
-#endif /* NEW */
+ #define TRY_ITE_VAR_CACHE(n1,n2,h) \
+ do { \
+ cache = \
+ &ite_var_computed_cache[ITE_VAR_COMPUTED_HASH(n1,n2,h)];\
+ if (cache->f==n1 && cache->g==n2 && cache->h==h) { \
+ COUNT_HIT(ite_var); \
+ return cache->result; \
+ } \
+ } while (0)
+
+ #define UPDATE_ITE_VAR_CACHE(n1,n2,h,node) \
+ do { \
+ cache->f = n1; \
+ cache->g = n2; \
+ cache->h = h; \
+ cache->result = node; \
+ COUNT_MISS(ite_var); \
+ } while (0)
+ #endif /* NEW */
#else /* !COMPUTED_TABLE */
+
/**************************** no caching at all **************************/
-#define DECLARE_ITE_CACHE_ENTRY
-#define TRY_ITE_CACHE(n1,n2,n3,op)
-#define UPDATE_ITE_CACHE(n1,n2,n3,node,op)
-#define DECLARE_BIN_CACHE_ENTRY
-#define TRY_BIN_CACHE(n1,n2,op)
-#define UPDATE_BIN_CACHE(n1,n2,node,op)
-#define DECLARE_UNARY_CACHE_ENTRY
-#define UPDATE_UNARY_CACHE(n,node,op)
-#define TRY_UNARY_CACHE(n,op)
-#define DECLARE_ASYM_BIN_CACHE_ENTRY
-#define UPDATE_ASYM_BIN_CACHE(n1,n2,node,op)
-#define TRY_ASYM_BIN_CACHE(n1,n2,op)
-#define DECLARE_RGLB_CACHE_ENTRY
-#define TRY_RGLB_CACHE(n1,n2,th)
-#define UPDATE_RGLB_CACHE(n1,n2,th,node)
-#define DECLARE_ITE_VAR_CACHE_ENTRY
-#define TRY_ITE_VAR_CACHE(n1,n2,h)
-#define UPDATE_ITE_VAR_CACHE(n1,n2,h,node)
-#define DECLARE_COMPLETE_OR_CACHE_ENTRY
-#define TRY_COMPLETE_OR_CACHE(n1,n2,pr)
-#define UPDATE_COMPLETE_OR_CACHE(n1,n2,pr,node)
-#undef COMPUTED_TABLE_SIZE
-#define COMPUTED_TABLE_SIZE 0
-#endif /* COMPUTED_TABLE */
+ #define DECLARE_ITE_CACHE_ENTRY
+ #define TRY_ITE_CACHE(n1,n2,n3,op)
+ #define UPDATE_ITE_CACHE(n1,n2,n3,node,op)
+
+ #define DECLARE_UNARY_CACHE_ENTRY
+ #define UPDATE_UNARY_CACHE(n,node,op)
+ #define TRY_UNARY_CACHE(n,op)
+
+ #define DECLARE_VAR_ENTAILED_CACHE_ENTRY
+ #define UPDATE_VAR_ENTAILED_CACHE(node,var,val)
+ #define TRY_VAR_ENTAILED_CACHE(node,var)
+
+ #define DECLARE_UNARY_BITSET_CACHE_ENTRY
+ #define UPDATE_UNARY_BITSET_CACHE(n,set,op)
+ #define TRY_UNARY_BITSET_CACHE(n,op)
+
+ #define DECLARE_BIN_CACHE_ENTRY
+ #define TRY_BIN_CACHE(n1,n2,op)
+ #define UPDATE_BIN_CACHE(n1,n2,node,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_COMPLETE_OR_CACHE_ENTRY
+ #define TRY_COMPLETE_OR_CACHE(n1,n2,pr)
+ #define UPDATE_COMPLETE_OR_CACHE(n1,n2,pr,node)
+
+ #define DECLARE_ITE_VAR_CACHE_ENTRY
+ #define TRY_ITE_VAR_CACHE(n1,n2,h)
+ #define UPDATE_ITE_VAR_CACHE(n1,n2,h,node)
+ #undef COMPUTED_TABLE_SIZE
+ #define COMPUTED_TABLE_SIZE 0
+#endif /* COMPUTED_TABLE */
/****************************************************************
@@ -728,15 +736,11 @@
****************************************************************/
-
static BRYANT_hidden_node_pointer unique_table[UNIQUE_TABLE_SIZE];
-
#define UNIQUE_HASH(var,tr,fa) \
(((var)+INTCAST(tr)+(INTCAST(fa)<<1)) % UNIQUE_TABLE_SIZE)
-
-
/****************************************************************
Prototypes
@@ -748,7 +752,6 @@
node *ite(node *f,node *g,node *h); /* if then else algorithm */
node *restricted_iff_conj_array(int v0, int n, int arr[], int thresh);
-
node *renameArray(node *in, int count, int mappping[]);
node *reverseRenameArray(node *in, int count, int rev_mappping[]);
@@ -837,7 +840,6 @@
}
#endif /* NO_CHEAP_SHIFT */
-
#if defined(NO_CHEAP_SHIFT)
__inline int prev_element(bitset *set, int *var, int *word, bitmask *mask)
{
@@ -901,7 +903,6 @@
}
#endif /* NO_CHEAP_SHIFT */
-
__inline int next_nonelement(bitset *set, int *var, int *word, bitmask *mask)
{
int vr = *var;
@@ -931,7 +932,6 @@
return TRUE;
}
-
__inline int prev_nonelement(bitset *set, int *var, int *word, bitmask *mask)
{
int vr = *var;
@@ -961,8 +961,6 @@
return TRUE;
}
-
-
/* returns 1 if set1 is identical to set2 */
__inline int bitset_equal(bitset *set1, bitset *set2);
__inline int bitset_equal(bitset *set1, bitset *set2)
@@ -994,7 +992,6 @@
}
}
-
/* returns 1 if set1 is a subset of set2 */
__inline int bitset_subset(bitset *set1, bitset *set2);
__inline int bitset_subset(bitset *set1, bitset *set2)
@@ -1011,7 +1008,6 @@
}
-
/* returns 1 if set1 is a subset of set2 */
__inline int bitset_empty(bitset *set);
__inline int bitset_empty(bitset *set)
@@ -1026,7 +1022,6 @@
}
-
/****************************************************************
Making Nodes
@@ -1057,7 +1052,6 @@
}
#endif /* BRYANT_CONSERVATIVE_GC */
-
#if defined(POOL)
static pool *curr_pool = NULL;
static node *curr_pool_ptr = NULL;
@@ -1100,7 +1094,6 @@
return node_count;
}
-
DECLARE_FN_COUNT(make_node)
node *make_node(int var, node *tr, node *fa)
@@ -1148,14 +1141,11 @@
return ptr;
}
-
void free_rep(node *n)
{
/* never free ROBDD nodes */
}
-
-
/****************************************************************
The Basic Algorithms
@@ -1168,19 +1158,16 @@
return MAXVAR;
}
-
node *trueVar(void)
{
return one;
}
-
node *falseVar(void)
{
return zero;
}
-
DECLARE_FN_COUNT(variableRep)
node *variableRep(int var)
@@ -1189,7 +1176,6 @@
return make_node(var,one,zero);
}
-
DECLARE_FN_COUNT(ite)
node *ite(node *f,node *g,node *h)
@@ -1245,7 +1231,6 @@
return newnode;
}
-
#if defined(USE_ITE_CONSTANT)
/* This is sort of an "approximate ite()." It returns zero or one if
@@ -1313,7 +1298,6 @@
}
#endif /* USE_ITE_CONSTANT */
-
DECLARE_FN_COUNT(implies)
node *implies(node *a, node *b)
@@ -1322,19 +1306,16 @@
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)
@@ -1345,7 +1326,6 @@
return ite(a,b,zero);
}
-
node *lub(node *a, node *b)
{
COUNT_FN(lub);
@@ -1382,7 +1362,6 @@
}
}
-
node *glb(node *f, node *g)
{
COUNT_FN(glb);
@@ -1413,8 +1392,6 @@
#endif /* NAIVE */
-
-
#if defined(NAIVE)
node *glb_array(int n, int arr[])
{
@@ -1461,7 +1438,6 @@
}
}
-
DECLARE_FN_COUNT(restrictThresh)
#if !defined(USE_THRESH) && !defined(RESTRICT_SET)
@@ -1530,7 +1506,6 @@
}
#endif /* USE_THRESH */
-
#if !defined(USE_THRESH) && !defined(RESTRICT_SET)
node *restricted_glb(int lo, int hi, node *f, node *g)
{
@@ -1564,7 +1539,6 @@
}
}
-
node *restricted_glb(int c, node *f, node *g)
{
if (IS_TERMINAL(f)) {
@@ -1614,8 +1588,6 @@
}
#endif /* USE_THRESH */
-
-
/****************************************************************
Renaming
@@ -1656,7 +1628,6 @@
}
}
-
/* 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)
{
@@ -1683,7 +1654,6 @@
}
}
-
/* 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.
@@ -1818,8 +1788,6 @@
return renameArray(f, max, rev_map);
}
-
-
/****************************************************************
Abstract Exit (renaming + conjunction + restriction)
@@ -1867,7 +1835,6 @@
}
}
-
/* computes the function f restricted so that all variables in trues
* are set to true and all in falses are set to false.
*/
@@ -1901,7 +1868,6 @@
}
}
-
/* 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}
@@ -1925,7 +1891,6 @@
return f;
}
-
/* This function computes
*
* restrictThresh(renameArray(f, count, mapping), thresh)
@@ -1950,8 +1915,6 @@
}
}
-
-
/* This function computes
*
* restrictThresh(glb(context1, renameArray(f, count, mapping)), thresh)
@@ -2010,7 +1973,6 @@
}
}
-
node *abstract_exit(node *context, node *f, int count, int mapping[],
int thresh)
{
@@ -2027,7 +1989,6 @@
}
#endif /* 0 (end of unused code) */
-
/****************************************************************
Abstract Unification
@@ -2057,7 +2018,6 @@
#define HANDLE_DUP(this,rel)
#endif
-
DECLARE_FN_COUNT(iff_conj)
#if defined(NAIVE)
@@ -2149,7 +2109,6 @@
}
#endif /* OLD */
-
node *restricted_iff_conj_array(int v0, int n, int arr[], int thresh)
{
if (v0 > thresh) return one;
@@ -2157,8 +2116,6 @@
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)
{
@@ -2171,7 +2128,6 @@
}
#else /* !1 (this code is unused) */
-
static node *build_and(int n, int arr[], node *tr, node *fa)
{
if (n<=0) {
@@ -2183,7 +2139,6 @@
}
}
-
static node *glb_and(node *f, int n, int arr[])
{
if (f == zero) {
@@ -2211,7 +2166,6 @@
}
}
-
static node *glb_nand(node *f, int n, int arr[])
{
if (f == zero) {
@@ -2239,7 +2193,6 @@
}
}
-
/* returns zero != glb(f, build_and(n, arr, one, zero)) */
static int exists_glb_and(node *f, int n, int arr[])
{
@@ -2258,7 +2211,6 @@
}
}
-
/* returns zero != glb(f, build_and(n, arr, zero, one)) */
static int exists_glb_nand(node *f, int n, int arr[])
{
@@ -2281,7 +2233,6 @@
}
}
-
/* returns zero != glb(f, iff_conj_array(v0, n, arr)) */
static int exists_glb_iffconj(node *f, int v0, int n, int arr[])
{
@@ -2315,8 +2266,6 @@
}
}
-
-
/* returns restricted_glb(f, build_and(n, arr, one, zero), thresh) */
static node *rglb_and(node *f, int n, int arr[], int thresh)
{
@@ -2355,7 +2304,6 @@
}
}
-
/* returns restricted_glb(f, build_and(n, arr, zero, one), thresh) */
static node *rglb_nand(node *f, int n, int arr[], int thresh)
{
@@ -2403,7 +2351,6 @@
}
}
-
/* returns restricted_glb(thresh, f, make_node(v, zero, one)) */
static node *rglb_notvar(node *f, int v, int thresh)
{
@@ -2436,8 +2383,6 @@
}
}
-
-
node *abstract_unify(node *f, int v0, int n, int arr[], int thresh)
{
if (f == zero) {
@@ -2494,8 +2439,6 @@
#endif /* (end of unused code) */
-
-
/****************************************************************
Finding Entailed Variables
@@ -2533,7 +2476,6 @@
#endif /* NEW */
}
-
/* returns a bitset of all the variables implied by f. A variable i
* is implied by f iff
*
@@ -2609,7 +2551,6 @@
}
}
-
/* returns a bitset of all the variables implied by f. A variable i
* is implied by f iff
*
@@ -2655,8 +2596,6 @@
#endif /* NEW && !OLD_VARS_ENTAILED */
#endif /* NEW */
-
-
/****************************************************************
Set Sharing Operations
@@ -2680,7 +2619,6 @@
return result;
}
-
#if defined(NEW)
DECLARE_FN_COUNT(complete_one_or)
@@ -2730,7 +2668,6 @@
return result;
}
-
DECLARE_FN_COUNT(complete_one)
node *complete_one(node *f)
@@ -2748,7 +2685,6 @@
return result;
}
-
DECLARE_FN_COUNT(complete_or)
/* the same as lub(complete(f, g), prev) */
@@ -2913,7 +2849,6 @@
}
}
-
/* Auxilliary function for bin: special case code for bin(f, one). */
node *bin_univ(node *f)
{
@@ -2933,7 +2868,6 @@
****************************************************************/
-
#if defined(STATISTICS)
void print_distribution(int array[], int max)
{
@@ -3114,8 +3048,6 @@
#endif /* NEW */
#endif /* STATISTICS */
}
-
-
/****************************************************************
Index: bryant.h
===================================================================
RCS file: /home/mercury1/repository/mercury/robdd/bryant.h,v
retrieving revision 1.1.12.1
diff -u -r1.1.12.1 bryant.h
--- bryant.h 14 Feb 2001 04:42:48 -0000 1.1.12.1
+++ bryant.h 6 May 2002 07:26:59 -0000
@@ -209,8 +209,12 @@
*****************************************************************/
+#ifndef TRUE
#define TRUE 1
+#endif
+#ifndef FALSE
#define FALSE 0
+#endif
/* sneaky trick to make NEW the default */
#if !defined(USE_RGLB) \
--------------------------------------------------------------------------
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