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

5 files changed, 49 insertions, 47 deletions

diff --git a/src/base/abc/abcFunc.c b/src/base/abc/abcFunc.c
index 2778e8d7..88004fab 100644
--- a/src/base/abc/abcFunc.c
+++ b/src/base/abc/abcFunc.c
@@ -356,39 +356,39 @@ char * Abc_ConvertBddToSop( Mem_Flex_t * pMan, DdManager * dd, DdNode * bFuncOn,
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_NtkBddToSop( Abc_Ntk_t * pNtk, int fDirect, int nCubeLimit )
+int Abc_NtkBddToSop( Abc_Ntk_t * pNtk, int fMode, int nCubeLimit )
 {
     extern void Abc_NtkSortSops( Abc_Ntk_t * pNtk );
+    Vec_Int_t * vGuide;
+    Vec_Str_t * vCube;
     Abc_Obj_t * pNode;
     Mem_Flex_t * pManNew;
     DdManager * dd = (DdManager *)pNtk->pManFunc;
     DdNode * bFunc;
-    Vec_Str_t * vCube;
-    int i, fMode, nCubes;
+    int i, nCubes;
 
+    // compute SOP size
+    vGuide = Vec_IntAlloc( Abc_NtkObjNumMax(pNtk) );
+    Vec_IntFill( vGuide, Abc_NtkObjNumMax(pNtk), fMode );
     if ( nCubeLimit < ABC_INFINITY )
     {
         // collect all BDDs into one array
-        Vec_Ptr_t * vFuncs = Vec_PtrAlloc( Abc_NtkNodeNum(pNtk) );
+        Vec_Ptr_t * vFuncs = Vec_PtrStart( Abc_NtkObjNumMax(pNtk) );
         assert( !Cudd_ReorderingStatus(dd, (Cudd_ReorderingType *)&nCubes) );
         Abc_NtkForEachNode( pNtk, pNode, i )
             if ( !Abc_ObjIsBarBuf(pNode) )
-                Vec_PtrPush( vFuncs, pNode->pData );
-        // estimate the number of cubes in the ISOPs
-        nCubes = Extra_bddCountCubes( dd, (DdNode **)Vec_PtrArray(vFuncs), Vec_PtrSize(vFuncs), fDirect, nCubeLimit );
+                Vec_PtrWriteEntry( vFuncs, i, pNode->pData );
+        // compute the number of cubes in the ISOPs and detemine polarity
+        nCubes = Extra_bddCountCubes( dd, (DdNode **)Vec_PtrArray(vFuncs), Vec_PtrSize(vFuncs), fMode, nCubeLimit, Vec_IntArray(vGuide) );
         Vec_PtrFree( vFuncs );
         if ( nCubes == -1 )
+        {
+            Vec_IntFree( vGuide );
             return 0;
+        }
         //printf( "The total number of cubes = %d.\n", nCubes );
     }
 
-    if ( fDirect == 2 ) // negative polarity only
-        fMode = 0;
-    else if ( fDirect == 1 ) // positive polarity only
-        fMode = 1;
-    else // both polarities
-        fMode = -1;
-
     assert( Abc_NtkHasBdd(pNtk) );
     if ( dd->size > 0 )
     Cudd_zddVarsFromBddVars( dd, 2 );
@@ -403,17 +403,19 @@ int Abc_NtkBddToSop( Abc_Ntk_t * pNtk, int fDirect, int nCubeLimit )
             continue;
         assert( pNode->pData );
         bFunc = (DdNode *)pNode->pData;
-        pNode->pNext = (Abc_Obj_t *)Abc_ConvertBddToSop( pManNew, dd, bFunc, bFunc, Abc_ObjFaninNum(pNode), 0, vCube, fMode );
+        pNode->pNext = (Abc_Obj_t *)Abc_ConvertBddToSop( pManNew, dd, bFunc, bFunc, Abc_ObjFaninNum(pNode), 0, vCube, Vec_IntEntry(vGuide, i) );
         if ( pNode->pNext == NULL )
         {
             Mem_FlexStop( pManNew, 0 );
             Abc_NtkCleanNext( pNtk );
 //            printf( "Converting from BDDs to SOPs has failed.\n" );
+            Vec_IntFree( vGuide );
             Vec_StrFree( vCube );
             return 0;
         }
         assert( Abc_ObjFaninNum(pNode) == Abc_SopGetVarNum((char *)pNode->pNext) );
     }
+    Vec_IntFree( vGuide );
     Vec_StrFree( vCube );
 
     // update the network type
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 7ac54f38..acaee90f 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -7889,8 +7889,7 @@ usage:
 int Abc_CommandSop( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
-    int fDirect = 0, nCubeLimit = 1000000;
-    int c;
+    int c, fMode = -1, nCubeLimit = 1000000;
 
     // set defaults
     Extra_UtilGetoptReset();
@@ -7910,10 +7909,10 @@ int Abc_CommandSop( Abc_Frame_t * pAbc, int argc, char ** argv )
                 goto usage;
             break;
         case 'd':
-            fDirect = 1;
+            fMode = 1;
             break;
         case 'n':
-            fDirect = 2;
+            fMode = 0;
             break;
         case 'h':
             goto usage;
@@ -7931,7 +7930,7 @@ int Abc_CommandSop( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_Print( -1, "Converting to SOP is possible only for logic networks.\n" );
         return 1;
     }
-    if ( !Abc_NtkToSop(pNtk, fDirect, nCubeLimit) )
+    if ( !Abc_NtkToSop(pNtk, fMode, nCubeLimit) )
     {
         Abc_Print( -1, "Converting to SOP has failed.\n" );
         return 1;
@@ -7939,10 +7938,11 @@ int Abc_CommandSop( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: sop [-C num] [-dh]\n" );
+    Abc_Print( -2, "usage: sop [-C num] [-dnh]\n" );
     Abc_Print( -2, "\t         converts node functions to SOP\n" );
-    Abc_Print( -2, "\t-C num : the limit on the total cube count of all nodes [default = %d]\n", nCubeLimit );
-    Abc_Print( -2, "\t-d     : toggles using both phases or only positive [default = %s]\n", fDirect? (fDirect == 1? "direct":"negated"): "both" );
+    Abc_Print( -2, "\t-C num : the limit on the number of cubes at a node [default = %d]\n", nCubeLimit );
+    Abc_Print( -2, "\t-d     : toggles using only positive polarity [default = %s]\n", fMode == 1 ? "yes": "no"  );
+    Abc_Print( -2, "\t-n     : toggles using only negative polarity [default = %s]\n", fMode == 0 ? "yes": "no" );
     Abc_Print( -2, "\t-h     : print the command usage\n");
     return 1;
 }
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()
 {