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

2 files changed, 25 insertions, 23 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;
 }