diff options
Diffstat (limited to 'src/misc')
| -rw-r--r-- | src/misc/extra/extraBdd.h | 2 | ||||
| -rw-r--r-- | src/misc/extra/extraBddMisc.c | 44 | ||||
| -rw-r--r-- | src/misc/extra/extraUtilMisc.c | 2 |
3 files changed, 24 insertions, 24 deletions
diff --git a/src/misc/extra/extraBdd.h b/src/misc/extra/extraBdd.h index 87072fd6..1f86950c 100644 --- a/src/misc/extra/extraBdd.h +++ b/src/misc/extra/extraBdd.h @@ -195,7 +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 ); +extern int Extra_bddCountCubes( DdManager * dd, DdNode ** pFuncs, int nFuncs, int fMode, int nLimit, int * pGuide ); #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 09e13c7c..0ec123f4 100644 --- a/src/misc/extra/extraBddMisc.c +++ b/src/misc/extra/extraBddMisc.c @@ -1479,33 +1479,33 @@ static DdNode * extraBddCountCubes( DdManager * dd, DdNode * L, DdNode * U, st__ Cudd_Deref(r); return r; } -int Extra_bddCountCubes( DdManager * dd, DdNode ** pFuncs, int nFuncs, int fDirect, int nLimit ) +int Extra_bddCountCubes( DdManager * dd, DdNode ** pFuncs, int nFuncs, int fMode, int nLimit, int * pGuide ) { - int i, CounterAll = 0; - unsigned int saveLimit = dd->maxLive; + DdNode * pF0, * pF1; + int i, Count, Count0, Count1, CounterAll = 0; st__table *table = st__init_table( st__ptrcmp, st__ptrhash ); - if ( table == NULL ) - return -1; + unsigned int saveLimit = dd->maxLive; + dd->maxLive = dd->keys - dd->dead + 1000000; // limit on intermediate BDD nodes for ( i = 0; i < nFuncs; i++ ) { - int Count0 = 0, Count1 = 0; - dd->maxLive = (dd->keys - dd->dead) + (dd->keysZ - dd->deadZ) + nLimit; - if ( NULL == extraBddCountCubes( dd, pFuncs[i], pFuncs[i], table, &Count0, nLimit - CounterAll ) ) - break; - if ( fDirect ) - Count1 = Count0; - else - { - dd->maxLive = (dd->keys - dd->dead) + (dd->keysZ - dd->deadZ) + nLimit; - pFuncs[i] = Cudd_Not( pFuncs[i] ); - if ( NULL == extraBddCountCubes( dd, pFuncs[i], pFuncs[i], table, &Count1, Count0 ) ) - Count1 = Count0; - pFuncs[i] = Cudd_Not( pFuncs[i] ); - } - CounterAll += Abc_MinInt( Count0, Count1 ); - if ( CounterAll > nLimit ) + if ( !pFuncs[i] ) + continue; + pF1 = pF0 = NULL; + Count0 = Count1 = nLimit; + if ( fMode == -1 || fMode == 1 ) // both or pos + pF1 = extraBddCountCubes( dd, pFuncs[i], pFuncs[i], table, &Count1, nLimit ); + pFuncs[i] = Cudd_Not( pFuncs[i] ); + if ( fMode == -1 || fMode == 0 ) // both or neg + pF0 = extraBddCountCubes( dd, pFuncs[i], pFuncs[i], table, &Count0, Count1 ); + pFuncs[i] = Cudd_Not( pFuncs[i] ); + if ( !pF1 && !pF0 ) break; - //printf( "Output %d has %d cubes\n", i, Abc_MinInt(Count0, Count1) ); + if ( !pF0 ) pGuide[i] = 1, Count = Count1; // use pos + else if ( !pF1 ) pGuide[i] = 0, Count = Count0; // use neg + else if ( Count1 <= Count0 ) pGuide[i] = 1, Count = Count1; // use pos + else pGuide[i] = 0, Count = Count0; // use neg + CounterAll += Count; + //printf( "Output %5d has %5d cubes (%d) (%5d and %5d)\n", nOuts++, Count, pGuide[i], Count1, Count0 ); } dd->maxLive = saveLimit; st__free_table( table ); diff --git a/src/misc/extra/extraUtilMisc.c b/src/misc/extra/extraUtilMisc.c index 479045f9..b4ba7940 100644 --- a/src/misc/extra/extraUtilMisc.c +++ b/src/misc/extra/extraUtilMisc.c @@ -2547,7 +2547,7 @@ void Extra_NtkPrintBin( word * pT, int nBits ) { int i; for ( i = nBits - 1; i >= 0; i-- ) - printf( "%d", (*pT >> (word)i) & 1 ); + printf( "%d", (int)((*pT >> i) & 1) ); } void Extra_NtkPowerTest() { |