Changing semantics of switch -C in 'sop' to limit cubes at one node.

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()
 {