diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2015-02-11 12:33:54 -0800 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2015-02-11 12:33:54 -0800 |
| commit | 8cabdcb55d0a390ea45cfed631118af35796dac2 (patch) | |
| tree | d99136a3c378b1115daf236b8d272f9deec4b90d /src/misc/extra | |
| parent | 72dbdee2023a86006f67b95027fe6acb841328c4 (diff) | |
| download | abc-8cabdcb55d0a390ea45cfed631118af35796dac2.tar.gz abc-8cabdcb55d0a390ea45cfed631118af35796dac2.tar.bz2 abc-8cabdcb55d0a390ea45cfed631118af35796dac2.zip | |
Adding resource limit switch -C to 'sop'.
Diffstat (limited to 'src/misc/extra')
| -rw-r--r-- | src/misc/extra/extraBddMisc.c | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/src/misc/extra/extraBddMisc.c b/src/misc/extra/extraBddMisc.c index 4be20a6f..66a0fc23 100644 --- a/src/misc/extra/extraBddMisc.c +++ b/src/misc/extra/extraBddMisc.c @@ -1486,19 +1486,20 @@ int Extra_bddCountCubes( DdManager * dd, DdNode ** pFuncs, int nFuncs, int fDire 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; + 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, nLimit - CounterAll ) ) - break; + if ( NULL == extraBddCountCubes( dd, pFuncs[i], pFuncs[i], table, &Count1, Count0 ) ) + Count1 = Count0; pFuncs[i] = Cudd_Not( pFuncs[i] ); } CounterAll += Abc_MinInt( Count0, Count1 ); |