[m-rev.] diff: bryant cleanup
Zoltan Somogyi
zs at csse.unimelb.edu.au
Mon Nov 9 19:01:06 AEDT 2009
robdd/bryant.c:
Fix some deviations from our C programming style.
Zoltan.
cvs diff: Diffing .
Index: bryant.c
===================================================================
RCS file: /home/mercury/mercury1/repository/mercury/robdd/bryant.c,v
retrieving revision 1.3
diff -u -b -r1.3 bryant.c
--- bryant.c 15 Aug 2006 04:19:38 -0000 1.3
+++ bryant.c 9 Nov 2009 01:34:39 -0000
@@ -133,13 +133,13 @@
#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))
+ #define MR_ROBDD_max(a, b) ((a)<(b) ? (b) : (a))
#endif
#if !defined(MR_ROBDD_min)
- #define MR_ROBDD_min(a,b) ((a)<(b) ? (a) : (b))
+ #define MR_ROBDD_min(a, b) ((a)<(b) ? (a) : (b))
#endif
-#define MR_ROBDD_PERCENTAGE(x,y) ((100.0 * (float)(x)) / (float)(y))
+#define MR_ROBDD_PERCENTAGE(x, y) ((100.0 * (float)(x)) / (float)(y))
#ifdef MR_ROBDD_POOL
typedef struct pool {
@@ -302,13 +302,13 @@
#endif /* MR_ROBDD_STATISTICS */
#if defined(MR_ROBDD_EQUAL_TEST)
- #define MR_ROBDD_DIRECT_EQUAL_TEST(f,g,result) \
+ #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);
+ #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)
+ #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)
@@ -353,18 +353,18 @@
#if defined(MR_ROBDD_COMPUTED_TABLE)
#if defined(MR_ROBDD_STATISTICS)
- #define MR_ROBDD_DECLARE_CACHE(op,MR_ROBDD_type) \
+ #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) \
+ #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) \
+ #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)
@@ -383,7 +383,7 @@
#define MR_ROBDD_DECLARE_ITE_CACHE_ENTRY ite_cache_entry *cache;
- #define MR_ROBDD_TRY_ITE_CACHE(n1,n2,n3,op) \
+ #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) { \
@@ -392,7 +392,7 @@
} \
} while (0)
- #define MR_ROBDD_UPDATE_ITE_CACHE(n1,n2,n3,MR_ROBDD_node,op) \
+ #define MR_ROBDD_UPDATE_ITE_CACHE(n1, n2, n3, MR_ROBDD_node, op) \
do { \
cache->f = n1; \
cache->g = n2; \
@@ -421,14 +421,14 @@
#define MR_ROBDD_DECLARE_UNARY_CACHE_ENTRY unary_cache_entry *cache;
- #define MR_ROBDD_UPDATE_UNARY_CACHE(n,MR_ROBDD_node,op) \
+ #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) \
+ #define MR_ROBDD_TRY_UNARY_CACHE(n, op) \
do { \
cache = &((op##_computed_cache)[MR_ROBDD_UNARY_NODE_HASH(n)]); \
if (cache->f==(n)) { \
@@ -439,7 +439,7 @@
/******************** the cache for MR_ROBDD_var_entailed ************/
- #define MR_ROBDD_VAR_ENTAILED_HASH(a,n) \
+ #define MR_ROBDD_VAR_ENTAILED_HASH(a, n) \
((MR_ROBDD_INTCAST(a)+n) % MR_ROBDD_COMPUTED_TABLE_SIZE)
typedef struct {
@@ -456,7 +456,7 @@
#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) \
+ #define MR_ROBDD_UPDATE_VAR_ENTAILED_CACHE(MR_ROBDD_node, var, val) \
do { \
cache->f = MR_ROBDD_node; \
cache->n = var; \
@@ -464,10 +464,10 @@
MR_ROBDD_COUNT_MISS(MR_ROBDD_var_entailed); \
} while (0)
- #define MR_ROBDD_TRY_VAR_ENTAILED_CACHE(MR_ROBDD_node,var) \
+ #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)]); \
+ [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; \
@@ -489,14 +489,14 @@
#define MR_ROBDD_DECLARE_UNARY_BITSET_CACHE_ENTRY \
unary_bitset_cache_entry *cache;
- #define MR_ROBDD_UPDATE_UNARY_BITSET_CACHE(n,set,op) \
+ #define MR_ROBDD_UPDATE_UNARY_BITSET_CACHE(n, set, op) \
do { \
cache->f = n; \
cache->result = set; \
MR_ROBDD_COUNT_MISS(op); \
} while (0)
- #define MR_ROBDD_TRY_UNARY_BITSET_CACHE(n,op) \
+ #define MR_ROBDD_TRY_UNARY_BITSET_CACHE(n, op) \
do { \
cache = &((op##_computed_cache)[MR_ROBDD_UNARY_NODE_HASH(n)]); \
if (cache->f==(n)) { \
@@ -509,14 +509,14 @@
/*
** 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
+** 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) \
+ #define MR_ROBDD_BINARY_NODE_HASH(a, b) \
((MR_ROBDD_INTCAST(a)+(MR_ROBDD_INTCAST(b)<<1)) % MR_ROBDD_COMPUTED_TABLE_SIZE)
typedef struct {
@@ -535,7 +535,7 @@
#define MR_ROBDD_DECLARE_BIN_CACHE_ENTRY bin_cache_entry *cache;
- #define MR_ROBDD_UPDATE_BIN_CACHE(n1,n2,MR_ROBDD_node,op) \
+ #define MR_ROBDD_UPDATE_BIN_CACHE(n1, n2, MR_ROBDD_node, op) \
do { \
cache->f = n1; \
cache->g = n2; \
@@ -543,7 +543,7 @@
MR_ROBDD_COUNT_MISS(op); \
} while (0)
- #define MR_ROBDD_TRY_BIN_CACHE(n1,n2,op) \
+ #define MR_ROBDD_TRY_BIN_CACHE(n1, n2, op) \
do { \
if (n2 < n1) { \
MR_ROBDD_node *temp = (n2); \
@@ -571,10 +571,10 @@
#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_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) \
+ #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)) { \
@@ -601,7 +601,7 @@
#define MR_ROBDD_DECLARE_RGLB_CACHE_ENTRY rglb_cache_entry *cache;
- #define MR_ROBDD_TRY_RGLB_CACHE(n1,n2,th) \
+ #define MR_ROBDD_TRY_RGLB_CACHE(n1, n2, th) \
do { \
if (n2 < n1) { \
MR_ROBDD_node *temp = (n2); \
@@ -617,7 +617,7 @@
} \
} while (0)
- #define MR_ROBDD_UPDATE_RGLB_CACHE(n1,n2,th,MR_ROBDD_node) \
+ #define MR_ROBDD_UPDATE_RGLB_CACHE(n1, n2, th,MR_ROBDD_node) \
do { \
cache->f = n1; \
cache->g = n2; \
@@ -644,7 +644,7 @@
#define MR_ROBDD_DECLARE_COMPLETE_OR_CACHE_ENTRY \
complete_or_cache_entry *cache;
- #define MR_ROBDD_TRY_COMPLETE_OR_CACHE(n1,n2,pr) \
+ #define MR_ROBDD_TRY_COMPLETE_OR_CACHE(n1, n2, pr) \
do { \
if (n2 < n1) { \
MR_ROBDD_node *temp = (n2); \
@@ -659,7 +659,7 @@
} \
} while (0)
- #define MR_ROBDD_UPDATE_COMPLETE_OR_CACHE(n1,n2,pr,MR_ROBDD_node) \
+ #define MR_ROBDD_UPDATE_COMPLETE_OR_CACHE(n1, n2, pr, MR_ROBDD_node) \
do { \
cache->f = n1; \
cache->g = n2; \
@@ -674,7 +674,7 @@
#if defined(MR_ROBDD_NEW)
- #define MR_ROBDD_ITE_VAR_COMPUTED_HASH(f,g,h) \
+ #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)
@@ -690,7 +690,7 @@
#define MR_ROBDD_DECLARE_ITE_VAR_CACHE_ENTRY ite_var_cache_entry *cache;
- #define MR_ROBDD_TRY_ITE_VAR_CACHE(n1,n2,h) \
+ #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)]; \
@@ -700,7 +700,7 @@
} \
} while (0)
- #define MR_ROBDD_UPDATE_ITE_VAR_CACHE(n1,n2,h,MR_ROBDD_node) \
+ #define MR_ROBDD_UPDATE_ITE_VAR_CACHE(n1, n2, h, MR_ROBDD_node) \
do { \
cache->f = n1; \
cache->g = n2; \
@@ -716,40 +716,40 @@
/**************************** no caching at all **************************/
#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_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_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_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_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_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_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_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_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)
+ #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
@@ -765,7 +765,7 @@
static MR_ROBDD_BRYANT_hidden_node_pointer
MR_ROBDD_unique_table[MR_ROBDD_UNIQUE_TABLE_SIZE];
-#define MR_ROBDD_UNIQUE_HASH(var,tr,fa) \
+#define MR_ROBDD_UNIQUE_HASH(var, tr, fa) \
(((var)+MR_ROBDD_INTCAST(tr)+(MR_ROBDD_INTCAST(fa)<<1)) \
% MR_ROBDD_UNIQUE_TABLE_SIZE)
@@ -778,7 +778,8 @@
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_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);
@@ -1214,7 +1215,7 @@
return tr;
}
- bucket = &MR_ROBDD_unique_table[MR_ROBDD_UNIQUE_HASH(var,tr,fa)];
+ bucket = &MR_ROBDD_unique_table[MR_ROBDD_UNIQUE_HASH(var, tr, fa)];
/*
** The following check avoids the need to initialise the table
@@ -1287,13 +1288,13 @@
MR_ROBDD_variableRep(int var)
{
MR_ROBDD_COUNT_FN(MR_ROBDD_variableRep);
- return MR_ROBDD_make_node(var,MR_ROBDD_one,MR_ROBDD_zero);
+ return MR_ROBDD_make_node(var, MR_ROBDD_one, MR_ROBDD_zero);
}
MR_ROBDD_DECLARE_FN_COUNT(MR_ROBDD_ite)
MR_ROBDD_node *
-MR_ROBDD_ite(MR_ROBDD_node *f,MR_ROBDD_node *g,MR_ROBDD_node *h)
+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;
@@ -1350,7 +1351,7 @@
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);
+ MR_ROBDD_UPDATE_ITE_CACHE(f, g, h, newnode, MR_ROBDD_ite);
return newnode;
}
@@ -1364,7 +1365,7 @@
*/
MR_ROBDD_node *
-MR_ROBDD_ite_constant(MR_ROBDD_node *f,MR_ROBDD_node *g,MR_ROBDD_node *h)
+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;
@@ -1427,7 +1428,7 @@
result = MR_ROBDD_nonterminal;
}
- MR_ROBDD_UPDATE_ITE_CACHE(f,g,h,result,MR_ROBDD_ite_constant);
+ MR_ROBDD_UPDATE_ITE_CACHE(f, g, h, result, MR_ROBDD_ite_constant);
return result;
}
#endif /* MR_ROBDD_USE_ITE_CONSTANT */
@@ -1438,7 +1439,7 @@
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);
+ return MR_ROBDD_ite(a, b, MR_ROBDD_one);
}
/* returns a copy of graph a */
@@ -1465,14 +1466,14 @@
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);
+ 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);
+ return MR_ROBDD_ite(a, MR_ROBDD_one, b);
}
#else /* !MR_ROBDD_NAIVE */
@@ -1485,7 +1486,7 @@
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)
+ } MR_ROBDD_ELSE_TRY_EQUAL_TEST(f, g, f)
else {
MR_ROBDD_node *result;
MR_ROBDD_DECLARE_BIN_CACHE_ENTRY
@@ -1515,7 +1516,7 @@
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)
+ } MR_ROBDD_ELSE_TRY_EQUAL_TEST(f, g, f)
else {
MR_ROBDD_node *result;
MR_ROBDD_DECLARE_BIN_CACHE_ENTRY
@@ -1587,7 +1588,7 @@
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));
+ MR_ROBDD_restrict(c, f->tr), MR_ROBDD_restrict(c, f->fa));
} else {
return MR_ROBDD_lub(f->tr, f->fa);
}
@@ -1658,12 +1659,14 @@
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);
+ 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);
+ MR_ROBDD_UPDATE_ASYM_BIN_CACHE((MR_ROBDD_node *) thresh, f, result,
+ MR_ROBDD_restrictThresh);
return result;
} else {
return MR_ROBDD_one;
@@ -1690,7 +1693,7 @@
#else /* MR_ROBDD_USE_RGLB */
-/* returns true iff MR_ROBDD_glb(f,g) is not 'MR_ROBDD_zero' */
+/* 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)
{
@@ -1722,7 +1725,7 @@
} 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))
+ } MR_ROBDD_ELSE_TRY_EQUAL_TEST(f, g, MR_ROBDD_restrictThresh(c, f))
else {
int v;
MR_ROBDD_node *tr1, *tr2, *fa1, *fa2;
@@ -1753,14 +1756,14 @@
}
if (v > c) {
result =
- (MR_ROBDD_exists_glb(tr1,tr2)||MR_ROBDD_exists_glb(fa1,fa2)) ?
+ (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);
+ MR_ROBDD_UPDATE_RGLB_CACHE(f, g, c, result);
return result;
}
}
@@ -1876,7 +1879,7 @@
*/
MR_ROBDD_node *
-MR_ROBDD_ite_var(int f,MR_ROBDD_node *g,MR_ROBDD_node *h)
+MR_ROBDD_ite_var(int f, MR_ROBDD_node *g, MR_ROBDD_node *h)
{
int g_val = INT_MAX;
int h_val = INT_MAX;
@@ -1885,7 +1888,7 @@
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_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;
@@ -1905,7 +1908,7 @@
}
if (f < g_val) {
- if (f < h_val) /* case 2 (b,c,d): f < g && f < h */ {
+ 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,
@@ -1918,7 +1921,7 @@
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 */ {
+ } 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));
@@ -1927,7 +1930,7 @@
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 */ {
+ } 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));
@@ -1939,7 +1942,7 @@
#else /* ! MR_ROBDD_NEW */
-#define MR_ROBDD_ite_var(v,f,g) MR_ROBDD_ite(MR_ROBDD_variableRep(v), f, g)
+#define MR_ROBDD_ite_var(v, f, g) MR_ROBDD_ite(MR_ROBDD_variableRep(v), f, g)
#endif /* !MR_ROBDD_NEW */
@@ -1972,7 +1975,7 @@
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) {
+ 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;
}
@@ -2027,9 +2030,9 @@
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)) {
+ if (MR_ROBDD_BITSET_MEMBER(*trues, word, mask)) {
f = f->tr; /* continue loop */
- } else if (MR_ROBDD_BITSET_MEMBER(*falses,word,mask)) {
+ } 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))
@@ -2063,9 +2066,9 @@
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)) {
+ if (MR_ROBDD_BITSET_MEMBER(*trues, word, mask)) {
f = f->tr; /* continue loop */
- } else if (MR_ROBDD_BITSET_MEMBER(*falses,word,mask)) {
+ } else if (MR_ROBDD_BITSET_MEMBER(*falses, word, mask)) {
f = f->fa; /* continue loop */
} else {
return MR_ROBDD_make_node(f->value,
@@ -2094,9 +2097,9 @@
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)) {
+ if (MR_ROBDD_BITSET_MEMBER(*trues, word, mask)) {
f = f->tr;
- } else if (MR_ROBDD_BITSET_MEMBER(*falses,word,mask)) {
+ } else if (MR_ROBDD_BITSET_MEMBER(*falses, word, mask)) {
f = f->fa;
} else {
break;
@@ -2180,14 +2183,14 @@
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 */
+ 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 */
+ 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 */
+ MR_ROBDD_BITSET_TOGGLE(*falses, word, mask); /* turn off false bit */
}
if (newval > thresh) {
return MR_ROBDD_lub(tr, fa);
@@ -2227,25 +2230,25 @@
/*
** 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
+** 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) \
+ #define MR_ROBDD_HANDLE_DUP(this, rel) \
if ((this) == prev) continue; \
assert((this) rel prev); \
prev = (this);
#elif !defined(NDEBUG)
#define MR_ROBDD_DECLARE_PREV(init) int prev = (init);
- #define MR_ROBDD_HANDLE_DUP(this,rel) \
+ #define MR_ROBDD_HANDLE_DUP(this, rel) \
assert((this) != prev); \
assert((this) rel prev); \
prev = (this);
#else
#define MR_ROBDD_DECLARE_PREV(init)
- #define MR_ROBDD_HANDLE_DUP(this,rel)
+ #define MR_ROBDD_HANDLE_DUP(this, rel)
#endif
MR_ROBDD_DECLARE_FN_COUNT(iff_conj)
@@ -2268,8 +2271,8 @@
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));
+ return MR_ROBDD_glb(MR_ROBDD_implies(conj, v_rep),
+ MR_ROBDD_implies(v_rep, conj));
}
#elif !defined(MR_ROBDD_USE_THRESH)
@@ -2324,7 +2327,7 @@
}
/* make v0 MR_ROBDD_node */
- thens = MR_ROBDD_make_node(v0,thens,elses);
+ 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
@@ -2334,7 +2337,7 @@
if (ptr >= arr) {
MR_ROBDD_DECLARE_PREV(MR_ROBDD_MAXVAR)
/* make ~v0 */
- elses = MR_ROBDD_make_node(v0,MR_ROBDD_zero,MR_ROBDD_one);
+ elses = MR_ROBDD_make_node(v0, MR_ROBDD_zero, MR_ROBDD_one);
do {
vi = *ptr;
@@ -2791,7 +2794,7 @@
for (i=0; i<MR_ROBDD_topvar; ++i) {
if (MR_ROBDD_var_entailed(f, i)) {
- MR_ROBDD_BITSET_ADD_ELEMENT(def_vars,i);
+ MR_ROBDD_BITSET_ADD_ELEMENT(def_vars, i);
}
}
return &def_vars;
@@ -2823,7 +2826,7 @@
for (; i >= 0; --i) {
if (MR_ROBDD_var_entailed(f, i)) {
- MR_ROBDD_BITSET_ADD_ELEMENT(def_vars,i);
+ MR_ROBDD_BITSET_ADD_ELEMENT(def_vars, i);
}
}
return &def_vars;
@@ -2855,10 +2858,10 @@
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_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);
+ MR_ROBDD_BITSET_TOGGLE(MR_ROBDD_this_path, word, mask);
f = f->fa;
}
/* needn't do anything for false terminals */
@@ -3134,8 +3137,8 @@
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));
+ 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);
@@ -3277,8 +3280,8 @@
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,
+ 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));
}
@@ -3286,7 +3289,7 @@
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));
+ MR_ROBDD_PERCENTAGE(array[MR_ROBDD_max], total));
}
printf("\n");
}
@@ -3484,7 +3487,7 @@
}
/* make v0 MR_ROBDD_node */
- thens = MR_ROBDD_make_node(v0,thens,elses);
+ thens = MR_ROBDD_make_node(v0, thens, elses);
/*
** Finally build part of graph above v0. For this, we build
@@ -3494,7 +3497,7 @@
if (ptr >= arr) {
/* make ~v0 */
- elses = MR_ROBDD_make_node(v0,MR_ROBDD_zero,MR_ROBDD_one);
+ elses = MR_ROBDD_make_node(v0, MR_ROBDD_zero, MR_ROBDD_one);
do {
vi = *ptr;
--------------------------------------------------------------------------
mercury-reviews mailing list
Post messages to: mercury-reviews at csse.unimelb.edu.au
Administrative Queries: owner-mercury-reviews at csse.unimelb.edu.au
Subscriptions: mercury-reviews-request at csse.unimelb.edu.au
--------------------------------------------------------------------------
More information about the reviews
mailing list