summaryrefslogtreecommitdiffstats
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/base/abci/abcNtbdd.c3
-rw-r--r--src/bdd/cudd/cuddAddIte.c25
-rw-r--r--src/bdd/cudd/cuddAddNeg.c20
-rw-r--r--src/bdd/cudd/cuddBddAbs.c19
-rw-r--r--src/bdd/cudd/cuddBddIte.c24
-rw-r--r--src/bdd/cudd/cuddClip.c32
-rw-r--r--src/bdd/cudd/cuddMatMult.c21
-rw-r--r--src/bdd/cudd/cuddPriority.c24
-rw-r--r--src/bdd/cudd/cuddSat.c44
-rw-r--r--src/bdd/cudd/cuddZddIsop.c20
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);
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-04 18:54:54 +0000