Disable cube-sort when deriving SOPs.

11 files changed, 31 insertions, 21 deletions

diff --git a/src/aig/gia/giaMinLut.c b/src/aig/gia/giaMinLut.c
index a33f9710..1972c175 100644
--- a/src/aig/gia/giaMinLut.c
+++ b/src/aig/gia/giaMinLut.c
@@ -152,11 +152,11 @@ void Gia_ManSimInfoPrintOne( Gia_Man_t * p, Vec_Wrd_t * vSimsIn, Vec_Wrd_t * vSi
     {
         Gia_ManForEachCiId( p, Id, i )
     //        printf( "%d", Vec_WrdEntry(p->vSims, p->nSimWords*Id) & 1 );
-            printf( "%d", (Vec_WrdEntry(vSimsIn,  nWords*i) >> k) & 1 );
+            printf( "%d", (int)(Vec_WrdEntry(vSimsIn,  nWords*i) >> k) & 1 );
         printf( " " );
         Gia_ManForEachCoId( p, Id, i )
     //        printf( "%d", Vec_WrdEntry(p->vSims, p->nSimWords*Id) & 1 );
-            printf( "%d", (Vec_WrdEntry(vSimsOut, nWords*i) >> k) & 1 );
+            printf( "%d", (int)(Vec_WrdEntry(vSimsOut, nWords*i) >> k) & 1 );
         printf( "\n" );
     }
 }
diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h
index 65ab604c..e7982b02 100644
--- a/src/base/abc/abc.h
+++ b/src/base/abc/abc.h
@@ -671,7 +671,7 @@ extern ABC_DLL Abc_Ntk_t *        Abc_NtkFraigRestore( int nPatsRand, int nPatsD
 extern ABC_DLL void               Abc_NtkFraigStoreClean();
 /*=== abcFunc.c ==========================================================*/
 extern ABC_DLL int                Abc_NtkSopToBdd( Abc_Ntk_t * pNtk );
-extern ABC_DLL int                Abc_NtkBddToSop( Abc_Ntk_t * pNtk, int fMode, int nCubeLimit );
+extern ABC_DLL int                Abc_NtkBddToSop( Abc_Ntk_t * pNtk, int fMode, int nCubeLimit, int fCubeSort );
 extern ABC_DLL void               Abc_NodeBddToCnf( Abc_Obj_t * pNode, Mem_Flex_t * pMmMan, Vec_Str_t * vCube, int fAllPrimes, char ** ppSop0, char ** ppSop1 );
 extern ABC_DLL void               Abc_NtkLogicMakeDirectSops( Abc_Ntk_t * pNtk );
 extern ABC_DLL int                Abc_NtkSopToAig( Abc_Ntk_t * pNtk );
diff --git a/src/base/abc/abcFunc.c b/src/base/abc/abcFunc.c
index 8f68d4be..84ecf7bf 100644
--- a/src/base/abc/abcFunc.c
+++ b/src/base/abc/abcFunc.c
@@ -356,7 +356,7 @@ char * Abc_ConvertBddToSop( Mem_Flex_t * pMan, DdManager * dd, DdNode * bFuncOn,
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_NtkBddToSop( Abc_Ntk_t * pNtk, int fMode, int nCubeLimit )
+int Abc_NtkBddToSop( Abc_Ntk_t * pNtk, int fMode, int nCubeLimit, int fCubeSort )
 {
     Vec_Int_t * vGuide;
     Vec_Str_t * vCube;
@@ -445,6 +445,7 @@ int Abc_NtkBddToSop( Abc_Ntk_t * pNtk, int fMode, int nCubeLimit )
     Extra_StopManager( dd );
 
     // reorder fanins and cubes to make SOPs more human-readable
+    if ( fCubeSort )
     Abc_NtkSortSops( pNtk );
     return 1;
 }
@@ -788,7 +789,7 @@ DdNode * Abc_ConvertAigToBdd( DdManager * dd, Hop_Obj_t * pRoot )
 #else
 
 int  Abc_NtkSopToBdd( Abc_Ntk_t * pNtk ) { return 1; }
-int  Abc_NtkBddToSop( Abc_Ntk_t * pNtk, int fMode, int nCubeLimit ) { return 1; }
+int  Abc_NtkBddToSop( Abc_Ntk_t * pNtk, int fMode, int nCubeLimit, int fCubeSort ) { return 1; }
 void Abc_NodeBddToCnf( Abc_Obj_t * pNode, Mem_Flex_t * pMmMan, Vec_Str_t * vCube, int fAllPrimes, char ** ppSop0, char ** ppSop1 ) {}
 void Abc_NtkLogicMakeDirectSops( Abc_Ntk_t * pNtk ) {}
 int  Abc_NtkAigToBdd( Abc_Ntk_t * pNtk ) { return 1; }
@@ -1178,17 +1179,17 @@ int Abc_NtkToSop( Abc_Ntk_t * pNtk, int fMode, int nCubeLimit )
             return 1;
         if ( !Abc_NtkSopToBdd(pNtk) )
             return 0;
-        return Abc_NtkBddToSop(pNtk, fMode, nCubeLimit);
+        return Abc_NtkBddToSop(pNtk, fMode, nCubeLimit, 1);
     }
     if ( Abc_NtkHasMapping(pNtk) )
         return Abc_NtkMapToSop(pNtk);
     if ( Abc_NtkHasBdd(pNtk) )
-        return Abc_NtkBddToSop(pNtk, fMode, nCubeLimit);
+        return Abc_NtkBddToSop(pNtk, fMode, nCubeLimit, 1);
     if ( Abc_NtkHasAig(pNtk) )
     {
         if ( !Abc_NtkAigToBdd(pNtk) )
             return 0;
-        return Abc_NtkBddToSop(pNtk, fMode, nCubeLimit);
+        return Abc_NtkBddToSop(pNtk, fMode, nCubeLimit, 1);
     }
     assert( 0 );
     return 0;
@@ -1253,7 +1254,7 @@ int Abc_NtkToAig( Abc_Ntk_t * pNtk )
     }
     if ( Abc_NtkHasBdd(pNtk) )
     {
-        if ( !Abc_NtkBddToSop(pNtk, -1, ABC_INFINITY) )
+        if ( !Abc_NtkBddToSop(pNtk, -1, ABC_INFINITY, 1) )
             return 0;
         return Abc_NtkSopToAig(pNtk);
     }
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index ae97e4dd..7fd645ad 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -10706,11 +10706,11 @@ usage:
 int Abc_CommandSop( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
-    int c, fMode = -1, nCubeLimit = 1000000;
+    int c, fCubeSort = 1, fMode = -1, nCubeLimit = 1000000;
 
     // set defaults
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "Cdnh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Csdnh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -10725,6 +10725,9 @@ int Abc_CommandSop( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( nCubeLimit < 0 )
                 goto usage;
             break;
+        case 's':
+            fCubeSort ^= 1;
+            break;
         case 'd':
             fMode = 1;
             break;
@@ -10747,6 +10750,11 @@ 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 ( !fCubeSort && Abc_NtkHasBdd(pNtk) && !Abc_NtkBddToSop(pNtk, -1, ABC_INFINITY, 0) )
+    {
+        Abc_Print( -1, "Converting to SOP has failed.\n" );
+        return 0;
+    }
     if ( !Abc_NtkToSop(pNtk, fMode, nCubeLimit) )
     {
         Abc_Print( -1, "Converting to SOP has failed.\n" );
@@ -10755,9 +10763,10 @@ int Abc_CommandSop( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: sop [-C num] [-dnh]\n" );
+    Abc_Print( -2, "usage: sop [-C num] [-sdnh]\n" );
     Abc_Print( -2, "\t         converts node functions to SOP\n" );
     Abc_Print( -2, "\t-C num : the limit on the number of cubes at a node [default = %d]\n", nCubeLimit );
+    Abc_Print( -2, "\t-s     : toggles cube sort when converting from BDDs [default = %s]\n", fCubeSort ? "yes": "no" );
     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");
diff --git a/src/base/abci/abcEspresso.c b/src/base/abci/abcEspresso.c
index 2da389da..9296b1e7 100644
--- a/src/base/abci/abcEspresso.c
+++ b/src/base/abci/abcEspresso.c
@@ -58,7 +58,7 @@ void Abc_NtkEspresso( Abc_Ntk_t * pNtk, int fVerbose )
         Abc_NtkMapToSop(pNtk);
     else if ( Abc_NtkHasBdd(pNtk) )
     {
-        if ( !Abc_NtkBddToSop(pNtk, -1, ABC_INFINITY) )
+        if ( !Abc_NtkBddToSop(pNtk, -1, ABC_INFINITY, 1) )
         {
             printf( "Abc_NtkEspresso(): Converting to SOPs has failed.\n" );
             return;
diff --git a/src/base/abci/abcFxu.c b/src/base/abci/abcFxu.c
index 8da306bf..99b3a5eb 100644
--- a/src/base/abci/abcFxu.c
+++ b/src/base/abci/abcFxu.c
@@ -88,7 +88,7 @@ int Abc_NtkFastExtract( Abc_Ntk_t * pNtk, Fxu_Data_t * p )
     if ( Abc_NtkIsSopLogic(pNtk) )
     { // to make sure the SOPs are SCC-free
 //        Abc_NtkSopToBdd(pNtk);
-//        Abc_NtkBddToSop(pNtk);
+//        Abc_NtkBddToSop(pNtk, 1);
     }
     // get the network in the SOP form
     if ( !Abc_NtkToSop(pNtk, -1, ABC_INFINITY) )
diff --git a/src/base/abci/abcIvy.c b/src/base/abci/abcIvy.c
index 3f268ea2..c680f85a 100644
--- a/src/base/abci/abcIvy.c
+++ b/src/base/abci/abcIvy.c
@@ -91,7 +91,7 @@ Ivy_Man_t * Abc_NtkIvyBefore( Abc_Ntk_t * pNtk, int fSeq, int fUseDc )
     assert( !Abc_NtkIsNetlist(pNtk) );
     if ( Abc_NtkIsBddLogic(pNtk) )
     {
-        if ( !Abc_NtkBddToSop(pNtk, -1, ABC_INFINITY) )
+        if ( !Abc_NtkBddToSop(pNtk, -1, ABC_INFINITY, 1) )
         {
             printf( "Abc_NtkIvyBefore(): Converting to SOPs has failed.\n" );
             return NULL;
@@ -640,7 +640,7 @@ Abc_Ntk_t * Abc_NtkIvy( Abc_Ntk_t * pNtk )
     assert( !Abc_NtkIsNetlist(pNtk) );
     if ( Abc_NtkIsBddLogic(pNtk) )
     {
-        if ( !Abc_NtkBddToSop(pNtk, -1, ABC_INFINITY) )
+        if ( !Abc_NtkBddToSop(pNtk, -1, ABC_INFINITY, 1) )
         {
             Vec_IntFree( vInit );
             printf( "Abc_NtkIvy(): Converting to SOPs has failed.\n" );
diff --git a/src/base/abci/abcMap.c b/src/base/abci/abcMap.c
index 5389b669..cef96351 100644
--- a/src/base/abci/abcMap.c
+++ b/src/base/abci/abcMap.c
@@ -612,7 +612,7 @@ Abc_Ntk_t * Abc_NtkFromMapSuperChoice( Map_Man_t * pMan, Abc_Ntk_t * pNtk )
     // duplicate the network
     pNtkNew2 = Abc_NtkDup( pNtk );
     pNtkNew  = Abc_NtkMulti( pNtkNew2, 0, 20, 0, 0, 1, 0 );
-    if ( !Abc_NtkBddToSop( pNtkNew, -1, ABC_INFINITY ) )
+    if ( !Abc_NtkBddToSop( pNtkNew, -1, ABC_INFINITY, 1 ) )
     {
         printf( "Abc_NtkFromMapSuperChoice(): Converting to SOPs has failed.\n" );
         return NULL;
diff --git a/src/base/abci/abcPrint.c b/src/base/abci/abcPrint.c
index ad5fba91..4ffb18a9 100644
--- a/src/base/abci/abcPrint.c
+++ b/src/base/abci/abcPrint.c
@@ -1399,7 +1399,7 @@ void Abc_NtkPrintGates( Abc_Ntk_t * pNtk, int fUseLibrary, int fUpdateProfile )
     // transform logic functions from BDD to SOP
     if ( (fHasBdds = Abc_NtkIsBddLogic(pNtk)) )
     {
-        if ( !Abc_NtkBddToSop(pNtk, -1, ABC_INFINITY) )
+        if ( !Abc_NtkBddToSop(pNtk, -1, ABC_INFINITY, 1) )
         {
             printf( "Abc_NtkPrintGates(): Converting to SOPs has failed.\n" );
             return;
diff --git a/src/base/abci/abcUnreach.c b/src/base/abci/abcUnreach.c
index ae4bc84b..5a20e5d8 100644
--- a/src/base/abci/abcUnreach.c
+++ b/src/base/abci/abcUnreach.c
@@ -342,7 +342,7 @@ Abc_Ntk_t * Abc_NtkConstructExdc( DdManager * dd, Abc_Ntk_t * pNtk, DdNode * bUn
     Abc_NtkLogicMakeSimpleCos( pNtkNew, 0 );
 
     // transform the network to the SOP representation
-    if ( !Abc_NtkBddToSop( pNtkNew, -1, ABC_INFINITY ) )
+    if ( !Abc_NtkBddToSop( pNtkNew, -1, ABC_INFINITY, 1 ) )
     {
         printf( "Abc_NtkConstructExdc(): Converting to SOPs has failed.\n" );
         return NULL;
diff --git a/src/base/io/ioWriteDot.c b/src/base/io/ioWriteDot.c
index d9687c6e..0ab3c4d2 100644
--- a/src/base/io/ioWriteDot.c
+++ b/src/base/io/ioWriteDot.c
@@ -100,7 +100,7 @@ void Io_WriteDotNtk( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesSho
     // transform logic functions from BDD to SOP
     if ( (fHasBdds = Abc_NtkIsBddLogic(pNtk)) )
     {
-        if ( !Abc_NtkBddToSop(pNtk, -1, ABC_INFINITY) )
+        if ( !Abc_NtkBddToSop(pNtk, -1, ABC_INFINITY, 1) )
         {
             printf( "Io_WriteDotNtk(): Converting to SOPs has failed.\n" );
             return;
@@ -463,7 +463,7 @@ void Io_WriteDotSeq( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesSho
     // transform logic functions from BDD to SOP
     if ( (fHasBdds = Abc_NtkIsBddLogic(pNtk)) )
     {
-        if ( !Abc_NtkBddToSop(pNtk, -1, ABC_INFINITY) )
+        if ( !Abc_NtkBddToSop(pNtk, -1, ABC_INFINITY, 1) )
         {
             printf( "Io_WriteDotNtk(): Converting to SOPs has failed.\n" );
             return;