Changes to make compiler happy.

10 files changed, 231 insertions, 1 deletions

diff --git a/src/base/abci/abcNtbdd.c b/src/base/abci/abcNtbdd.c
index cbf4bbb8..9de88980 100644
--- a/src/base/abci/abcNtbdd.c
+++ b/src/base/abci/abcNtbdd.c
@@ -237,7 +237,8 @@ Abc_Obj_t * Abc_NodeBddToMuxes_rec( DdManager * dd, DdNode * bFunc, Abc_Ntk_t *
 {
     Abc_Obj_t * pNodeNew, * pNodeNew0, * pNodeNew1, * pNodeNewC;
     assert( !Cudd_IsComplement(bFunc) );
-    if ( bFunc == b1 || bFunc == a1 )
+    assert( b1 == a1 );
+    if ( bFunc == a1 )
         return Abc_NtkCreateNodeConst1(pNtkNew);
     if ( bFunc == a0 )
         return Abc_NtkCreateNodeConst0(pNtkNew);
diff --git a/src/bdd/cudd/cuddAddIte.c b/src/bdd/cudd/cuddAddIte.c
index 574159c6..5f95bf47 100644
--- a/src/bdd/cudd/cuddAddIte.c
+++ b/src/bdd/cudd/cuddAddIte.c
@@ -359,6 +359,22 @@ Cudd_addCmpl(
 } /* end of Cudd_addCmpl */
 
 
+#ifdef USE_CASH_DUMMY
+/**Function********************************************************************
+
+  Synopsis    We need to declare a function passed to cuddCacheLookup2 as a key
+              that can be casted to DD_CTFP.
+
+******************************************************************************/
+static DdNode *
+Cudd_addLeq_dummy(DdManager * dd, DdNode * f, DdNode * g)
+{
+  assert(0);
+  return 0;
+}
+#endif
+
+
 /**Function********************************************************************
 
   Synopsis    [Determines whether f is less than or equal to g.]
@@ -394,7 +410,11 @@ Cudd_addLeq(
     if (g == DD_MINUS_INFINITY(dd)) return(0); /* since f != g */
 
     /* Check cache. */
+#ifdef USE_CASH_DUMMY
+    tmp = cuddCacheLookup2(dd,(DD_CTFP)Cudd_addLeq_dummy,f,g);
+#else
     tmp = cuddCacheLookup2(dd,(DD_CTFP)Cudd_addLeq,f,g);
+#endif
     if (tmp != NULL) {
         return(tmp == DD_ONE(dd));
     }
@@ -416,8 +436,13 @@ Cudd_addLeq(
     res = Cudd_addLeq(dd,fvn,gvn) && Cudd_addLeq(dd,fv,gv);
 
     /* Store result in cache and return. */
+#ifdef USE_CASH_DUMMY
+    cuddCacheInsert2(dd,(DD_CTFP) Cudd_addLeq_dummy,f,g,
+                     Cudd_NotCond(DD_ONE(dd),res==0));
+#else
     cuddCacheInsert2(dd,(DD_CTFP) Cudd_addLeq,f,g,
                      Cudd_NotCond(DD_ONE(dd),res==0));
+#endif
     return(res);
 
 } /* end of Cudd_addLeq */
diff --git a/src/bdd/cudd/cuddAddNeg.c b/src/bdd/cudd/cuddAddNeg.c
index ab36874d..22d11219 100644
--- a/src/bdd/cudd/cuddAddNeg.c
+++ b/src/bdd/cudd/cuddAddNeg.c
@@ -226,6 +226,22 @@ cuddAddNegateRecur(
 } /* end of cuddAddNegateRecur */
 
 
+#ifdef USE_CASH_DUMMY
+/**Function********************************************************************
+
+  Synopsis    We need to declare a function passed to cuddCacheLookup1 that can
+              be casted to DD_CTFP.
+
+******************************************************************************/
+static DdNode *
+Cudd_addRoundOff_dummy(DdManager * dd, DdNode * f) 
+{
+  assert(0);
+  return 0;
+}
+#endif
+
+
 /**Function********************************************************************
 
   Synopsis    [Implements the recursive step of Cudd_addRoundOff.]
@@ -253,7 +269,11 @@ cuddAddRoundOffRecur(
         res = cuddUniqueConst(dd,n);
         return(res);
     }
+#ifdef USE_CASH_DUMMY
+    cacheOp = (DD_CTFP1) Cudd_addRoundOff_dummy;
+#else
     cacheOp = (DD_CTFP1) Cudd_addRoundOff;
+#endif
     res = cuddCacheLookup1(dd,cacheOp,f);
     if (res != NULL) {
         return(res);
diff --git a/src/bdd/cudd/cuddBddAbs.c b/src/bdd/cudd/cuddBddAbs.c
index bfdd08ba..e2345617 100644
--- a/src/bdd/cudd/cuddBddAbs.c
+++ b/src/bdd/cudd/cuddBddAbs.c
@@ -266,6 +266,21 @@ Cudd_bddBooleanDiff(
 } /* end of Cudd_bddBooleanDiff */
 
 
+#ifdef USE_CASH_DUMMY
+/**Function********************************************************************
+
+  Synopsis    We need to declare a function passed to cuddCacheLookup2 that can
+              be casted to DD_CTFP.
+
+******************************************************************************/
+static DdNode *
+Cudd_bddVarIsDependent_dummy(DdManager *dd, DdNode *f, DdNode *var)
+{
+  assert(0);
+  return 0;
+}
+#endif
+
 /**Function********************************************************************
 
   Synopsis    [Checks whether a variable is dependent on others in a
@@ -305,7 +320,11 @@ Cudd_bddVarIsDependent(
         return(0);
     }
 
+#ifdef USE_CASH_DUMMY
+    cacheOp = (DD_CTFP) Cudd_bddVarIsDependent_dummy;
+#else
     cacheOp = (DD_CTFP) Cudd_bddVarIsDependent;
+#endif
     res = cuddCacheLookup2(dd,cacheOp,f,var);
     if (res != NULL) {
         return(res != zero);
diff --git a/src/bdd/cudd/cuddBddIte.c b/src/bdd/cudd/cuddBddIte.c
index 803d5f19..2901096c 100644
--- a/src/bdd/cudd/cuddBddIte.c
+++ b/src/bdd/cudd/cuddBddIte.c
@@ -520,6 +520,22 @@ Cudd_bddXnor(
 } /* end of Cudd_bddXnor */
 
 
+#ifdef USE_CASH_DUMMY
+/**Function********************************************************************
+
+  Synopsis    We need to declare a function passed to cuddCacheLookup2 that can
+              be casted to DD_CTFP.
+
+******************************************************************************/
+static DdNode *
+Cudd_bddLeq_dummy(DdManager * dd, DdNode * f,  DdNode * g)
+{
+  assert(0);
+  return 0;
+}
+#endif
+
+
 /**Function********************************************************************
 
   Synopsis    [Determines whether f is less than or equal to g.]
@@ -573,7 +589,11 @@ Cudd_bddLeq(
     /* Here neither f nor g is constant. */
 
     /* Check cache. */
+#ifdef USE_CASH_DUMMY
+    tmp = cuddCacheLookup2(dd,(DD_CTFP)Cudd_bddLeq_dummy,f,g);
+#else
     tmp = cuddCacheLookup2(dd,(DD_CTFP)Cudd_bddLeq,f,g);
+#endif
     if (tmp != NULL) {
         return(tmp == one);
     }
@@ -605,7 +625,11 @@ Cudd_bddLeq(
     res = Cudd_bddLeq(dd,fvn,gvn) && Cudd_bddLeq(dd,fv,gv);
 
     /* Store result in cache and return. */
+#ifdef USE_CASH_DUMMY
+    cuddCacheInsert2(dd,(DD_CTFP)Cudd_bddLeq_dummy,f,g,(res ? one : zero));
+#else
     cuddCacheInsert2(dd,(DD_CTFP)Cudd_bddLeq,f,g,(res ? one : zero));
+#endif
     return(res);
 
 } /* end of Cudd_bddLeq */
diff --git a/src/bdd/cudd/cuddClip.c b/src/bdd/cudd/cuddClip.c
index 9e3572f9..32ee7f6e 100644
--- a/src/bdd/cudd/cuddClip.c
+++ b/src/bdd/cudd/cuddClip.c
@@ -250,6 +250,34 @@ cuddBddClippingAndAbstract(
 /*---------------------------------------------------------------------------*/
 /* Definition of static functions                                            */
 /*---------------------------------------------------------------------------*/
+#ifdef USE_CASH_DUMMY
+/**Function********************************************************************
+
+  Synopsis    We need to declare a function passed to cuddCacheLookup2 that can
+              be casted to DD_CTFP.
+
+******************************************************************************/
+static DdNode *
+Cudd_bddClippingAnd_dummy(DdManager *dd, DdNode *f, DdNode *g)
+{
+  assert(0);
+  return 0;
+}
+
+
+/**Function********************************************************************
+
+  Synopsis    We need to declare a function passed to cuddCacheLookup2 that can
+              be casted to DD_CTFP.
+
+******************************************************************************/
+static DdNode *
+cuddBddClippingAnd_dummy(DdManager *dd, DdNode *f, DdNode *g)
+{
+  assert(0);
+  return 0;
+}
+#endif
 
 
 /**Function********************************************************************
@@ -309,8 +337,12 @@ cuddBddClippingAndRecur(
     }
     F = Cudd_Regular(f);
     G = Cudd_Regular(g);
+#ifdef USE_CASH_DUMMY
+    cacheOp = (DD_CTFP) (direction ? Cudd_bddClippingAnd_dummy : cuddBddClippingAnd_dummy);
+#else
     cacheOp = (DD_CTFP)
         (direction ? Cudd_bddClippingAnd : cuddBddClippingAnd);
+#endif
     if (F->ref != 1 || G->ref != 1) {
         r = cuddCacheLookup2(manager, cacheOp, f, g);
         if (r != NULL) return(r);
diff --git a/src/bdd/cudd/cuddMatMult.c b/src/bdd/cudd/cuddMatMult.c
index e8cae2ce..3dafa226 100644
--- a/src/bdd/cudd/cuddMatMult.c
+++ b/src/bdd/cudd/cuddMatMult.c
@@ -319,6 +319,23 @@ Cudd_addOuterSum(
 /* Definition of static functions                                            */
 /*---------------------------------------------------------------------------*/
 
+
+#ifdef USE_CASH_DUMMY
+/**Function********************************************************************
+
+  Synopsis    We need to declare a function passed to cuddCacheLookup2 that can
+              be casted to DD_CTFP.
+
+******************************************************************************/
+static DdNode *
+addMMRecur_dummy(DdManager * dd, DdNode * A, DdNode * B)
+{
+  assert(0);
+  return 0;
+}
+#endif
+
+
 /**Function********************************************************************
 
   Synopsis    [Performs the recursive step of Cudd_addMatrixMultiply.]
@@ -393,7 +410,11 @@ addMMRecur(
     topA = cuddI(dd,A->index); topB = cuddI(dd,B->index);
     topV = ddMin(topA,topB);
 
+#ifdef USE_CASH_DUMMY
+    cacheOp = (DD_CTFP) addMMRecur_dummy;
+#else
     cacheOp = (DD_CTFP) addMMRecur;
+#endif
     res = cuddCacheLookup2(dd,cacheOp,A,B);
     if (res != NULL) {
         /* If the result is 0, there is no need to normalize.
diff --git a/src/bdd/cudd/cuddPriority.c b/src/bdd/cudd/cuddPriority.c
index aae5a732..27da4dc6 100644
--- a/src/bdd/cudd/cuddPriority.c
+++ b/src/bdd/cudd/cuddPriority.c
@@ -1571,6 +1571,22 @@ cuddCProjectionRecur(
 } /* end of cuddCProjectionRecur */
 
 
+#ifdef USE_CASH_DUMMY
+/**Function********************************************************************
+
+  Synopsis    We need to declare a function passed to cuddCacheLookup2 that can
+              be casted to DD_CTFP.
+
+******************************************************************************/
+DdNode *
+Cudd_bddClosestCube_dummy(DdManager *dd, DdNode *f, DdNode *g)
+{
+  assert(0);
+  return 0;
+}
+#endif
+
+
 /**Function********************************************************************
 
   Synopsis    [Performs the recursive step of Cudd_bddClosestCube.]
@@ -1667,7 +1683,11 @@ cuddBddClosestCube(
     F = Cudd_Regular(f);
     G = Cudd_Regular(g);
     if (F->ref != 1 || G->ref != 1) {
+#ifdef USE_CASH_DUMMY
+        res = cuddCacheLookup2(dd,(DD_CTFP) Cudd_bddClosestCube_dummy, f, g);
+#else
         res = cuddCacheLookup2(dd,(DD_CTFP) Cudd_bddClosestCube, f, g);
+#endif
         if (res != NULL) return(res);
     }
 
@@ -1817,7 +1837,11 @@ cuddBddClosestCube(
     /* Only cache results that are different from azero to avoid
     ** storing results that depend on the value of the bound. */
     if ((F->ref != 1 || G->ref != 1) && res != azero)
+#ifdef USE_CASH_DUMMY
+        cuddCacheInsert2(dd,(DD_CTFP) Cudd_bddClosestCube_dummy, f, g, res);
+#else
         cuddCacheInsert2(dd,(DD_CTFP) Cudd_bddClosestCube, f, g, res);
+#endif
 
     cuddDeref(res);
     return(res);
diff --git a/src/bdd/cudd/cuddSat.c b/src/bdd/cudd/cuddSat.c
index 899901dd..976c59ab 100644
--- a/src/bdd/cudd/cuddSat.c
+++ b/src/bdd/cudd/cuddSat.c
@@ -390,6 +390,22 @@ Cudd_ShortestLength(
 } /* end of Cudd_ShortestLength */
 
 
+#ifdef USE_CASH_DUMMY
+/**Function********************************************************************
+
+  Synopsis    We need to declare a function passed to cuddCacheLookup2 that can
+              be casted to DD_CTFP.
+
+******************************************************************************/
+static DdNode *
+Cudd_Decreasing_dummy(DdManager * dd, DdNode * f, DdNode * g)
+{
+  assert(0);
+  return 0;
+}
+#endif
+
+
 /**Function********************************************************************
 
   Synopsis    [Determines whether a BDD is negative unate in a
@@ -434,7 +450,11 @@ Cudd_Decreasing(
     /* From now on, f is not constant. */
 
     /* Check cache. */
+#ifdef USE_CASH_DUMMY
+    cacheOp = (DD_CTFP) Cudd_Decreasing_dummy;
+#else
     cacheOp = (DD_CTFP) Cudd_Decreasing;
+#endif
     res = cuddCacheLookup2(dd,cacheOp,f,dd->vars[i]);
     if (res != NULL) {
         return(res);
@@ -768,6 +788,22 @@ Cudd_bddLeqUnless(
 } /* end of Cudd_bddLeqUnless */
 
 
+#ifdef USE_CASH_DUMMY
+/**Function********************************************************************
+
+  Synopsis    We need to declare a function passed to cuddCacheLookup2 that can
+              be casted to DD_CTFP.
+
+******************************************************************************/
+static DdNode *
+Cudd_EqualSupNorm_dummy(DdManager * dd, DdNode * f, DdNode * g)
+{
+  assert(0);
+  return 0;
+}
+#endif
+
+
 /**Function********************************************************************
 
   Synopsis    [Compares two ADDs for equality within tolerance.]
@@ -817,7 +853,11 @@ Cudd_EqualSupNorm(
 
     /* We only insert the result in the cache if the comparison is
     ** successful. Therefore, if we hit we return 1. */
+#ifdef USE_CASH_DUMMY
+    r = cuddCacheLookup2(dd,(DD_CTFP)Cudd_EqualSupNorm_dummy,f,g);
+#else
     r = cuddCacheLookup2(dd,(DD_CTFP)Cudd_EqualSupNorm,f,g);
+#endif
     if (r != NULL) {
         return(1);
     }
@@ -832,7 +872,11 @@ Cudd_EqualSupNorm(
     if (!Cudd_EqualSupNorm(dd,fv,gv,tolerance,pr)) return(0);
     if (!Cudd_EqualSupNorm(dd,fvn,gvn,tolerance,pr)) return(0);
 
+#ifdef USE_CASH_DUMMY
+    cuddCacheInsert2(dd,(DD_CTFP)Cudd_EqualSupNorm_dummy,f,g,DD_ONE(dd));
+#else
     cuddCacheInsert2(dd,(DD_CTFP)Cudd_EqualSupNorm,f,g,DD_ONE(dd));
+#endif
 
     return(1);
 
diff --git a/src/bdd/cudd/cuddZddIsop.c b/src/bdd/cudd/cuddZddIsop.c
index ace0807b..116b7c2f 100644
--- a/src/bdd/cudd/cuddZddIsop.c
+++ b/src/bdd/cudd/cuddZddIsop.c
@@ -219,6 +219,22 @@ Cudd_MakeBddFromZddCover(
 /*---------------------------------------------------------------------------*/
 
 
+#ifdef USE_CASH_DUMMY
+/**Function********************************************************************
+
+  Synopsis    We need to declare a function passed to cuddCacheLookup2 that can
+              be casted to DD_CTFP.
+
+******************************************************************************/
+static DdNode  *
+cuddZddIsop_dummy(DdManager * dd, DdNode * L, DdNode * U)
+{
+  assert(0);
+  return 0;
+}
+#endif
+
+
 /**Function********************************************************************
 
   Synopsis [Performs the recursive step of Cudd_zddIsop.]
@@ -273,7 +289,11 @@ cuddZddIsop(
     ** Hence we need a double hit in the cache to terminate the
     ** recursion. Clearly, collisions may evict only one of the two
     ** results. */
+#ifdef USE_CASH_DUMMY
+    cacheOp = (DD_CTFP) cuddZddIsop_dummy;
+#else
     cacheOp = (DD_CTFP) cuddZddIsop;
+#endif
     r = cuddCacheLookup2(dd, cuddBddIsop, L, U);
     if (r) {
         *zdd_I = cuddCacheLookup2Zdd(dd, cacheOp, L, U);