diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2021-11-27 17:37:34 -0800 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2021-11-27 17:37:34 -0800 |
commit | f26ea1eaea5b51a3aec8107636c9f88eadfdcee0 (patch) | |
tree | 59f90e5e857950020c4108c31dbfbc6e768b5f91 /src/bdd | |
parent | 96bdcd2bb274e2cf01d2362294d5f5fdeb009533 (diff) | |
download | abc-f26ea1eaea5b51a3aec8107636c9f88eadfdcee0.tar.gz abc-f26ea1eaea5b51a3aec8107636c9f88eadfdcee0.tar.bz2 abc-f26ea1eaea5b51a3aec8107636c9f88eadfdcee0.zip |
Changes to make compiler happy.
Diffstat (limited to 'src/bdd')
-rw-r--r-- | src/bdd/cudd/cuddAddIte.c | 25 | ||||
-rw-r--r-- | src/bdd/cudd/cuddAddNeg.c | 20 | ||||
-rw-r--r-- | src/bdd/cudd/cuddBddAbs.c | 19 | ||||
-rw-r--r-- | src/bdd/cudd/cuddBddIte.c | 24 | ||||
-rw-r--r-- | src/bdd/cudd/cuddClip.c | 32 | ||||
-rw-r--r-- | src/bdd/cudd/cuddMatMult.c | 21 | ||||
-rw-r--r-- | src/bdd/cudd/cuddPriority.c | 24 | ||||
-rw-r--r-- | src/bdd/cudd/cuddSat.c | 44 | ||||
-rw-r--r-- | src/bdd/cudd/cuddZddIsop.c | 20 |
9 files changed, 229 insertions, 0 deletions
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); |