summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/base/abc/abcFunc.c15
-rw-r--r--src/misc/extra/extraBdd.h1
-rw-r--r--src/misc/extra/extraBddMisc.c264
3 files changed, 279 insertions, 1 deletions
diff --git a/src/base/abc/abcFunc.c b/src/base/abc/abcFunc.c
index 6e9e3d09..ff18fb13 100644
--- a/src/base/abc/abcFunc.c
+++ b/src/base/abc/abcFunc.c
@@ -364,7 +364,20 @@ int Abc_NtkBddToSop( Abc_Ntk_t * pNtk, int fDirect )
DdManager * dd = (DdManager *)pNtk->pManFunc;
DdNode * bFunc;
Vec_Str_t * vCube;
- int i, fMode;
+ int i, fMode, nCubes;
+
+ // collect all BDDs into one array
+ Vec_Ptr_t * vFuncs = Vec_PtrAlloc( Abc_NtkNodeNum(pNtk) );
+ assert( !Cudd_ReorderingStatus(dd, &nCubes) );
+ Abc_NtkForEachNode( pNtk, pNode, i )
+ if ( !Abc_ObjIsBarBuf(pNode) )
+ Vec_PtrPush( vFuncs, pNode->pData );
+ // estimate the number of cubes in the ISOPs
+ nCubes = Extra_bddCountCubes( dd, (DdNode **)Vec_PtrArray(vFuncs), Vec_PtrSize(vFuncs), fDirect, 100000 );
+ Vec_PtrFree( vFuncs );
+ if ( nCubes == -1 )
+ return 0;
+ printf( "The total number of cubes = %d.\n", nCubes );
if ( fDirect )
fMode = 1;
diff --git a/src/misc/extra/extraBdd.h b/src/misc/extra/extraBdd.h
index fc225e50..87072fd6 100644
--- a/src/misc/extra/extraBdd.h
+++ b/src/misc/extra/extraBdd.h
@@ -195,6 +195,7 @@ extern DdNode * Extra_bddChangePolarity( DdManager * dd, DdNode * bFunc, DdN
extern DdNode * extraBddChangePolarity( DdManager * dd, DdNode * bFunc, DdNode * bVars );
extern int Extra_bddVarIsInCube( DdNode * bCube, int iVar );
extern DdNode * Extra_bddAndPermute( DdManager * ddF, DdNode * bF, DdManager * ddG, DdNode * bG, int * pPermute );
+extern int Extra_bddCountCubes( DdManager * dd, DdNode ** pFuncs, int nFuncs, int fDirect, int nLimit );
#ifndef ABC_PRB
#define ABC_PRB(dd,f) printf("%s = ", #f); Extra_bddPrint(dd,f); printf("\n")
diff --git a/src/misc/extra/extraBddMisc.c b/src/misc/extra/extraBddMisc.c
index 7d9c26d5..4be20a6f 100644
--- a/src/misc/extra/extraBddMisc.c
+++ b/src/misc/extra/extraBddMisc.c
@@ -1246,6 +1246,270 @@ extraDecomposeCover(
}
} /* extraDecomposeCover */
+
+
+/**Function********************************************************************
+
+ Synopsis [Counts the total number of cubes in the ISOPs of the functions.]
+
+ Description [Returns -1 if the number of cubes exceeds the limit.]
+
+ SideEffects [None]
+
+ SeeAlso [Extra_TransferPermute]
+
+******************************************************************************/
+static DdNode * extraBddCountCubes( DdManager * dd, DdNode * L, DdNode * U, st__table *table, int * pnCubes, int Limit )
+{
+ DdNode *one = DD_ONE(dd);
+ DdNode *zero = Cudd_Not(one);
+ int v, top_l, top_u;
+ DdNode *Lsub0, *Usub0, *Lsub1, *Usub1, *Ld, *Ud;
+ DdNode *Lsuper0, *Usuper0, *Lsuper1, *Usuper1;
+ DdNode *Isub0, *Isub1, *Id;
+ DdNode *x;
+ DdNode *term0, *term1, *sum;
+ DdNode *Lv, *Uv, *Lnv, *Unv;
+ DdNode *r;
+ int index;
+ int Count0 = 0, Count1 = 0, Count2 = 0;
+
+ statLine(dd);
+ if (L == zero)
+ return(zero);
+ if (U == one)
+ {
+ *pnCubes = 1;
+ return(one);
+ }
+
+ /* Check cache */
+ r = cuddCacheLookup2(dd, cuddBddIsop, L, U);
+ if (r)
+ {
+ int nCubes = 0;
+ if ( st__lookup( table, (char *)r, (char **)&nCubes ) )
+ *pnCubes = nCubes;
+ else assert( 0 );
+ return r;
+ }
+
+ top_l = dd->perm[Cudd_Regular(L)->index];
+ top_u = dd->perm[Cudd_Regular(U)->index];
+ v = ddMin(top_l, top_u);
+
+ /* Compute cofactors */
+ if (top_l == v) {
+ index = Cudd_Regular(L)->index;
+ Lv = Cudd_T(L);
+ Lnv = Cudd_E(L);
+ if (Cudd_IsComplement(L)) {
+ Lv = Cudd_Not(Lv);
+ Lnv = Cudd_Not(Lnv);
+ }
+ }
+ else {
+ index = Cudd_Regular(U)->index;
+ Lv = Lnv = L;
+ }
+
+ if (top_u == v) {
+ Uv = Cudd_T(U);
+ Unv = Cudd_E(U);
+ if (Cudd_IsComplement(U)) {
+ Uv = Cudd_Not(Uv);
+ Unv = Cudd_Not(Unv);
+ }
+ }
+ else {
+ Uv = Unv = U;
+ }
+
+ Lsub0 = cuddBddAndRecur(dd, Lnv, Cudd_Not(Uv));
+ if (Lsub0 == NULL)
+ return(NULL);
+ Cudd_Ref(Lsub0);
+ Usub0 = Unv;
+ Lsub1 = cuddBddAndRecur(dd, Lv, Cudd_Not(Unv));
+ if (Lsub1 == NULL) {
+ Cudd_RecursiveDeref(dd, Lsub0);
+ return(NULL);
+ }
+ Cudd_Ref(Lsub1);
+ Usub1 = Uv;
+
+ Isub0 = extraBddCountCubes(dd, Lsub0, Usub0, table, &Count0, Limit);
+ if (Isub0 == NULL) {
+ Cudd_RecursiveDeref(dd, Lsub0);
+ Cudd_RecursiveDeref(dd, Lsub1);
+ return(NULL);
+ }
+ Cudd_Ref(Isub0);
+ Isub1 = extraBddCountCubes(dd, Lsub1, Usub1, table, &Count1, Limit);
+ if (Isub1 == NULL) {
+ Cudd_RecursiveDeref(dd, Lsub0);
+ Cudd_RecursiveDeref(dd, Lsub1);
+ Cudd_RecursiveDeref(dd, Isub0);
+ return(NULL);
+ }
+ Cudd_Ref(Isub1);
+ Cudd_RecursiveDeref(dd, Lsub0);
+ Cudd_RecursiveDeref(dd, Lsub1);
+
+ Lsuper0 = cuddBddAndRecur(dd, Lnv, Cudd_Not(Isub0));
+ if (Lsuper0 == NULL) {
+ Cudd_RecursiveDeref(dd, Isub0);
+ Cudd_RecursiveDeref(dd, Isub1);
+ return(NULL);
+ }
+ Cudd_Ref(Lsuper0);
+ Lsuper1 = cuddBddAndRecur(dd, Lv, Cudd_Not(Isub1));
+ if (Lsuper1 == NULL) {
+ Cudd_RecursiveDeref(dd, Isub0);
+ Cudd_RecursiveDeref(dd, Isub1);
+ Cudd_RecursiveDeref(dd, Lsuper0);
+ return(NULL);
+ }
+ Cudd_Ref(Lsuper1);
+ Usuper0 = Unv;
+ Usuper1 = Uv;
+
+ /* Ld = Lsuper0 + Lsuper1 */
+ Ld = cuddBddAndRecur(dd, Cudd_Not(Lsuper0), Cudd_Not(Lsuper1));
+ Ld = Cudd_NotCond(Ld, Ld != NULL);
+ if (Ld == NULL) {
+ Cudd_RecursiveDeref(dd, Isub0);
+ Cudd_RecursiveDeref(dd, Isub1);
+ Cudd_RecursiveDeref(dd, Lsuper0);
+ Cudd_RecursiveDeref(dd, Lsuper1);
+ return(NULL);
+ }
+ Cudd_Ref(Ld);
+ Ud = cuddBddAndRecur(dd, Usuper0, Usuper1);
+ if (Ud == NULL) {
+ Cudd_RecursiveDeref(dd, Isub0);
+ Cudd_RecursiveDeref(dd, Isub1);
+ Cudd_RecursiveDeref(dd, Lsuper0);
+ Cudd_RecursiveDeref(dd, Lsuper1);
+ Cudd_RecursiveDeref(dd, Ld);
+ return(NULL);
+ }
+ Cudd_Ref(Ud);
+ Cudd_RecursiveDeref(dd, Lsuper0);
+ Cudd_RecursiveDeref(dd, Lsuper1);
+
+ Id = extraBddCountCubes(dd, Ld, Ud, table, &Count2, Limit);
+ if (Id == NULL) {
+ Cudd_RecursiveDeref(dd, Isub0);
+ Cudd_RecursiveDeref(dd, Isub1);
+ Cudd_RecursiveDeref(dd, Ld);
+ Cudd_RecursiveDeref(dd, Ud);
+ return(NULL);
+ }
+ Cudd_Ref(Id);
+ Cudd_RecursiveDeref(dd, Ld);
+ Cudd_RecursiveDeref(dd, Ud);
+
+ x = cuddUniqueInter(dd, index, one, zero);
+ if (x == NULL) {
+ Cudd_RecursiveDeref(dd, Isub0);
+ Cudd_RecursiveDeref(dd, Isub1);
+ Cudd_RecursiveDeref(dd, Id);
+ return(NULL);
+ }
+ Cudd_Ref(x);
+ term0 = cuddBddAndRecur(dd, Cudd_Not(x), Isub0);
+ if (term0 == NULL) {
+ Cudd_RecursiveDeref(dd, Isub0);
+ Cudd_RecursiveDeref(dd, Isub1);
+ Cudd_RecursiveDeref(dd, Id);
+ Cudd_RecursiveDeref(dd, x);
+ return(NULL);
+ }
+ Cudd_Ref(term0);
+ Cudd_RecursiveDeref(dd, Isub0);
+ term1 = cuddBddAndRecur(dd, x, Isub1);
+ if (term1 == NULL) {
+ Cudd_RecursiveDeref(dd, Isub1);
+ Cudd_RecursiveDeref(dd, Id);
+ Cudd_RecursiveDeref(dd, x);
+ Cudd_RecursiveDeref(dd, term0);
+ return(NULL);
+ }
+ Cudd_Ref(term1);
+ Cudd_RecursiveDeref(dd, x);
+ Cudd_RecursiveDeref(dd, Isub1);
+ /* sum = term0 + term1 */
+ sum = cuddBddAndRecur(dd, Cudd_Not(term0), Cudd_Not(term1));
+ sum = Cudd_NotCond(sum, sum != NULL);
+ if (sum == NULL) {
+ Cudd_RecursiveDeref(dd, Id);
+ Cudd_RecursiveDeref(dd, term0);
+ Cudd_RecursiveDeref(dd, term1);
+ return(NULL);
+ }
+ Cudd_Ref(sum);
+ Cudd_RecursiveDeref(dd, term0);
+ Cudd_RecursiveDeref(dd, term1);
+ /* r = sum + Id */
+ r = cuddBddAndRecur(dd, Cudd_Not(sum), Cudd_Not(Id));
+ r = Cudd_NotCond(r, r != NULL);
+ if (r == NULL) {
+ Cudd_RecursiveDeref(dd, Id);
+ Cudd_RecursiveDeref(dd, sum);
+ return(NULL);
+ }
+ Cudd_Ref(r);
+ Cudd_RecursiveDeref(dd, sum);
+ Cudd_RecursiveDeref(dd, Id);
+
+ cuddCacheInsert2(dd, cuddBddIsop, L, U, r);
+ *pnCubes = Count0 + Count1 + Count2;
+ if ( st__add_direct( table, (char *)r, (char *)*pnCubes ) == st__OUT_OF_MEM )
+ {
+ Cudd_RecursiveDeref( dd, r );
+ return NULL;
+ }
+ if ( *pnCubes > Limit )
+ {
+ Cudd_RecursiveDeref( dd, r );
+ return NULL;
+ }
+ //printf( "%d ", *pnCubes );
+ Cudd_Deref(r);
+ return r;
+}
+int Extra_bddCountCubes( DdManager * dd, DdNode ** pFuncs, int nFuncs, int fDirect, int nLimit )
+{
+ int i, CounterAll = 0;
+ unsigned int saveLimit = dd->maxLive;
+ st__table *table = st__init_table( st__ptrcmp, st__ptrhash );
+ if ( table == NULL )
+ return -1;
+ dd->maxLive = (dd->keys - dd->dead) + (dd->keysZ - dd->deadZ) + nLimit;
+ for ( i = 0; i < nFuncs; i++ )
+ {
+ int Count0 = 0, Count1 = 0;
+ if ( NULL == extraBddCountCubes( dd, pFuncs[i], pFuncs[i], table, &Count0, nLimit - CounterAll ) )
+ break;
+ if ( fDirect )
+ Count1 = Count0;
+ else
+ {
+ pFuncs[i] = Cudd_Not( pFuncs[i] );
+ if ( NULL == extraBddCountCubes( dd, pFuncs[i], pFuncs[i], table, &Count1, nLimit - CounterAll ) )
+ break;
+ pFuncs[i] = Cudd_Not( pFuncs[i] );
+ }
+ CounterAll += Abc_MinInt( Count0, Count1 );
+ if ( CounterAll > nLimit )
+ break;
+ }
+ dd->maxLive = saveLimit;
+ st__free_table( table );
+ return i == nFuncs ? CounterAll : -1;
+} /* end of Extra_bddCountCubes */
+
/*---------------------------------------------------------------------------*/
/* Definition of static Functions */
/*---------------------------------------------------------------------------*/
generated by cgit v1.2.3 (git 2.25.1) at 2024-11-04 21:02:58 +0000