summaryrefslogtreecommitdiffstats
path: root/src/misc
diff options
context:
space:
mode:
Diffstat (limited to 'src/misc')
-rw-r--r--src/misc/extra/extraBdd.h2
-rw-r--r--src/misc/extra/extraBddMisc.c44
-rw-r--r--src/misc/extra/extraUtilMisc.c2
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()
{