diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2015-02-18 18:41:26 -0800 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2015-02-18 18:41:26 -0800 |
commit | 5ad773eda10692ee1877a04561ef51c06713f519 (patch) | |
tree | 6dc30bcef6e83e236b8d575645b394bd2e33434a /src/misc/extra/extraBddMisc.c | |
parent | 874d394089932a50cc3d9797018f2c398e74444e (diff) | |
download | abc-5ad773eda10692ee1877a04561ef51c06713f519.tar.gz abc-5ad773eda10692ee1877a04561ef51c06713f519.tar.bz2 abc-5ad773eda10692ee1877a04561ef51c06713f519.zip |
Changing semantics of switch -C in 'sop' to limit cubes at one node.
Diffstat (limited to 'src/misc/extra/extraBddMisc.c')
-rw-r--r-- | src/misc/extra/extraBddMisc.c | 44 |
1 files changed, 22 insertions, 22 deletions
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 ); |