Version abc61209

4 files changed, 282 insertions, 120 deletions

diff --git a/src/base/abc/abcUtil.c b/src/base/abc/abcUtil.c
index 12bb8341..3ee39955 100644
--- a/src/base/abc/abcUtil.c
+++ b/src/base/abc/abcUtil.c
@@ -218,9 +218,9 @@ int Abc_NtkGetBddNodeNum( Abc_Ntk_t * pNtk )
     Abc_NtkForEachNode( pNtk, pNode, i )
     {
         assert( pNode->pData );
-        if ( Abc_NodeIsConst(pNode) )
+        if ( Abc_ObjFaninNum(pNode) < 2 )
             continue;
-        nNodes += pNode->pData? Cudd_DagSize( pNode->pData ) : 0;
+        nNodes += pNode->pData? -1 + Cudd_DagSize( pNode->pData ) : 0;
     }
     return nNodes;
 }
@@ -244,7 +244,7 @@ int Abc_NtkGetAigNodeNum( Abc_Ntk_t * pNtk )
     Abc_NtkForEachNode( pNtk, pNode, i )
     {
         assert( pNode->pData );
-        if ( Abc_NodeIsConst(pNode) )
+        if ( Abc_ObjFaninNum(pNode) < 2 )
             continue;
         nNodes += pNode->pData? Hop_DagSize( pNode->pData ) : 0;
     }
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 901e1df4..115e9bb8 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -2034,24 +2034,26 @@ int Abc_CommandRenode( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk, * pNtkRes;
-    int nFaninMax, nCubeMax, c;
+    int nLutSize, nCutsMax, c;
+    int fArea;
     int fUseBdds;
     int fUseSops;
     int fVerbose;
-    extern Abc_Ntk_t * Abc_NtkRenode( Abc_Ntk_t * pNtk, int nFaninMax, int nCubeMax, int fUseBdds, int fUseSops, int fVerbose );
+    extern Abc_Ntk_t * Abc_NtkRenode( Abc_Ntk_t * pNtk, int nLutSize, int nCutsMax, int fArea, int fUseBdds, int fUseSops, int fVerbose );
 
     pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
     // set defaults
-    nFaninMax =  5;
-    nCubeMax  =  5;
+    nLutSize  =  8;
+    nCutsMax  =  5;
+    fArea     =  0;
     fUseBdds  =  0;
     fUseSops  =  0;
     fVerbose  =  0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "KCbsvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "KCabsvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -2061,9 +2063,9 @@ int Abc_CommandRenode( Abc_Frame_t * pAbc, int argc, char ** argv )
                 fprintf( pErr, "Command line switch \"-F\" should be followed by an integer.\n" );
                 goto usage;
             }
-            nFaninMax = atoi(argv[globalUtilOptind]);
+            nLutSize = atoi(argv[globalUtilOptind]);
             globalUtilOptind++;
-            if ( nFaninMax < 0 ) 
+            if ( nLutSize < 0 ) 
                 goto usage;
             break;
         case 'C':
@@ -2072,11 +2074,14 @@ int Abc_CommandRenode( Abc_Frame_t * pAbc, int argc, char ** argv )
                 fprintf( pErr, "Command line switch \"-C\" should be followed by an integer.\n" );
                 goto usage;
             }
-            nCubeMax = atoi(argv[globalUtilOptind]);
+            nCutsMax = atoi(argv[globalUtilOptind]);
             globalUtilOptind++;
-            if ( nCubeMax < 0 ) 
+            if ( nCutsMax < 0 ) 
                 goto usage;
             break;
+        case 'a':
+            fArea ^= 1;
+            break;
         case 'b':
             fUseBdds ^= 1;
             break;
@@ -2096,7 +2101,19 @@ int Abc_CommandRenode( Abc_Frame_t * pAbc, int argc, char ** argv )
     if ( fUseBdds && fUseSops )
     {
         fprintf( pErr, "Cannot optimize both BDDs and SOPs at the same time.\n" );
-        goto usage;
+        return 1;
+    }
+
+    if ( nLutSize < 3 || nLutSize > IF_MAX_FUNC_LUTSIZE )
+    {
+        fprintf( pErr, "Incorrect LUT size (%d).\n", nLutSize );
+        return 1;
+    }
+
+    if ( nCutsMax < 2 || nCutsMax >= (1<<12) )
+    {
+        fprintf( pErr, "Incorrect number of cuts.\n" );
+        return 1;
     }
 
     if ( pNtk == NULL )
@@ -2111,7 +2128,7 @@ int Abc_CommandRenode( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
 
     // get the new network
-    pNtkRes = Abc_NtkRenode( pNtk, nFaninMax, nCubeMax, fUseBdds, fUseSops, fVerbose );
+    pNtkRes = Abc_NtkRenode( pNtk, nLutSize, nCutsMax, fArea, fUseBdds, fUseSops, fVerbose );
     if ( pNtkRes == NULL )
     {
         fprintf( pErr, "Renoding has failed.\n" );
@@ -2122,13 +2139,14 @@ int Abc_CommandRenode( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( pErr, "usage: renode [-K num] [-C num] [-bsv]\n" );
+    fprintf( pErr, "usage: renode [-K num] [-C num] [-sbav]\n" );
     fprintf( pErr, "\t          transforms the AIG into a logic network with larger nodes\n" );
     fprintf( pErr, "\t          while minimizing the number of FF literals of the node SOPs\n" );
-    fprintf( pErr, "\t-K num  : the maximum fanin size after renoding [default = %d]\n", nFaninMax );
-    fprintf( pErr, "\t-C num  : the maximum number of cubes used at a node [default = %d]\n", nCubeMax );
-    fprintf( pErr, "\t-b      : toggles minimizing the number of BDD nodes [default = %s]\n", fUseBdds? "yes": "no" );
-    fprintf( pErr, "\t-s      : toggles minimizing the number of SOP cubes [default = %s]\n", fUseSops? "yes": "no" );
+    fprintf( pErr, "\t-K num  : the max cut size for renoding (2 < num < %d) [default = %d]\n", IF_MAX_FUNC_LUTSIZE+1, nLutSize );
+    fprintf( pErr, "\t-C num  : the max number of cuts used at a node (1 < num < 2^12) [default = %d]\n", nCutsMax );
+    fprintf( pErr, "\t-s      : toggles minimizing SOP cubes instead of FF lits [default = %s]\n", fUseSops? "yes": "no" );
+    fprintf( pErr, "\t-b      : toggles minimizing BDD nodes instead of FF lits [default = %s]\n", fUseBdds? "yes": "no" );
+    fprintf( pErr, "\t-a      : toggles area-oriented mapping [default = %s]\n", fArea? "yes": "no" );
     fprintf( pErr, "\t-v      : print verbose information [default = %s]\n", fVerbose? "yes": "no" ); 
     fprintf( pErr, "\t-h      : print the command usage\n");
     return 1;
@@ -2731,18 +2749,18 @@ int Abc_CommandRestructure( Abc_Frame_t * pAbc, int argc, char ** argv )
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk;
     int c;
-    int nCutMax;
+    int nCutsMax;
     bool fUpdateLevel;
     bool fUseZeros;
     bool fVerbose;
-    extern int Abc_NtkRestructure( Abc_Ntk_t * pNtk, int nCutMax, bool fUpdateLevel, bool fUseZeros, bool fVerbose );
+    extern int Abc_NtkRestructure( Abc_Ntk_t * pNtk, int nCutsMax, bool fUpdateLevel, bool fUseZeros, bool fVerbose );
 
     pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
     // set defaults
-    nCutMax      =  5;
+    nCutsMax      =  5;
     fUpdateLevel =  0;
     fUseZeros    =  0;
     fVerbose     =  0;
@@ -2757,9 +2775,9 @@ int Abc_CommandRestructure( Abc_Frame_t * pAbc, int argc, char ** argv )
                 fprintf( pErr, "Command line switch \"-K\" should be followed by an integer.\n" );
                 goto usage;
             }
-            nCutMax = atoi(argv[globalUtilOptind]);
+            nCutsMax = atoi(argv[globalUtilOptind]);
             globalUtilOptind++;
-            if ( nCutMax < 0 ) 
+            if ( nCutsMax < 0 ) 
                 goto usage;
             break;
         case 'l':
@@ -2783,7 +2801,7 @@ int Abc_CommandRestructure( Abc_Frame_t * pAbc, int argc, char ** argv )
         fprintf( pErr, "Empty network.\n" );
         return 1;
     }
-    if ( nCutMax < 4 || nCutMax > CUT_SIZE_MAX )
+    if ( nCutsMax < 4 || nCutsMax > CUT_SIZE_MAX )
     {
         fprintf( pErr, "Can only compute the cuts for %d <= K <= %d.\n", 4, CUT_SIZE_MAX );
         return 1;
@@ -2800,7 +2818,7 @@ int Abc_CommandRestructure( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
 
     // modify the current network
-    if ( !Abc_NtkRestructure( pNtk, nCutMax, fUpdateLevel, fUseZeros, fVerbose ) )
+    if ( !Abc_NtkRestructure( pNtk, nCutsMax, fUpdateLevel, fUseZeros, fVerbose ) )
     {
         fprintf( pErr, "Refactoring has failed.\n" );
         return 1;
@@ -2810,7 +2828,7 @@ int Abc_CommandRestructure( Abc_Frame_t * pAbc, int argc, char ** argv )
 usage:
     fprintf( pErr, "usage: restructure [-K num] [-lzvh]\n" );
     fprintf( pErr, "\t         performs technology-independent restructuring of the AIG\n" );
-    fprintf( pErr, "\t-K num : the max cut size (%d <= num <= %d) [default = %d]\n",   CUT_SIZE_MIN, CUT_SIZE_MAX, nCutMax );  
+    fprintf( pErr, "\t-K num : the max cut size (%d <= num <= %d) [default = %d]\n",   CUT_SIZE_MIN, CUT_SIZE_MAX, nCutsMax );  
     fprintf( pErr, "\t-l     : toggle preserving the number of levels [default = %s]\n", fUpdateLevel? "yes": "no" );
     fprintf( pErr, "\t-z     : toggle using zero-cost replacements [default = %s]\n", fUseZeros? "yes": "no" );
     fprintf( pErr, "\t-v     : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" );
@@ -2836,19 +2854,19 @@ int Abc_CommandResubstitute( Abc_Frame_t * pAbc, int argc, char ** argv )
     int RS_CUT_MIN =  4;
     int RS_CUT_MAX = 16;
     int c;
-    int nCutMax;
+    int nCutsMax;
     int nNodesMax;
     bool fUpdateLevel;
     bool fUseZeros;
     bool fVerbose;
-    extern int Abc_NtkResubstitute( Abc_Ntk_t * pNtk, int nCutMax, int nNodesMax, bool fUpdateLevel, bool fVerbose );
+    extern int Abc_NtkResubstitute( Abc_Ntk_t * pNtk, int nCutsMax, int nNodesMax, bool fUpdateLevel, bool fVerbose );
 
     pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
     // set defaults
-    nCutMax      =  8;
+    nCutsMax      =  8;
     nNodesMax    =  1;
     fUpdateLevel =  1;
     fUseZeros    =  0;
@@ -2864,9 +2882,9 @@ int Abc_CommandResubstitute( Abc_Frame_t * pAbc, int argc, char ** argv )
                 fprintf( pErr, "Command line switch \"-K\" should be followed by an integer.\n" );
                 goto usage;
             }
-            nCutMax = atoi(argv[globalUtilOptind]);
+            nCutsMax = atoi(argv[globalUtilOptind]);
             globalUtilOptind++;
-            if ( nCutMax < 0 ) 
+            if ( nCutsMax < 0 ) 
                 goto usage;
             break;
         case 'N':
@@ -2901,7 +2919,7 @@ int Abc_CommandResubstitute( Abc_Frame_t * pAbc, int argc, char ** argv )
         fprintf( pErr, "Empty network.\n" );
         return 1;
     }
-    if ( nCutMax < RS_CUT_MIN || nCutMax > RS_CUT_MAX )
+    if ( nCutsMax < RS_CUT_MIN || nCutsMax > RS_CUT_MAX )
     {
         fprintf( pErr, "Can only compute the cuts for %d <= K <= %d.\n", RS_CUT_MIN, RS_CUT_MAX );
         return 1;
@@ -2918,7 +2936,7 @@ int Abc_CommandResubstitute( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
 
     // modify the current network
-    if ( !Abc_NtkResubstitute( pNtk, nCutMax, nNodesMax, fUpdateLevel, fVerbose ) )
+    if ( !Abc_NtkResubstitute( pNtk, nCutsMax, nNodesMax, fUpdateLevel, fVerbose ) )
     {
         fprintf( pErr, "Refactoring has failed.\n" );
         return 1;
@@ -2928,7 +2946,7 @@ int Abc_CommandResubstitute( Abc_Frame_t * pAbc, int argc, char ** argv )
 usage:
     fprintf( pErr, "usage: resub [-K num] [-N num] [-lzvh]\n" );
     fprintf( pErr, "\t         performs technology-independent restructuring of the AIG\n" );
-    fprintf( pErr, "\t-K num : the max cut size (%d <= num <= %d) [default = %d]\n", RS_CUT_MIN, RS_CUT_MAX, nCutMax );  
+    fprintf( pErr, "\t-K num : the max cut size (%d <= num <= %d) [default = %d]\n", RS_CUT_MIN, RS_CUT_MAX, nCutsMax );  
     fprintf( pErr, "\t-N num : the max number of nodes to add [default = %d]\n", nNodesMax );  
     fprintf( pErr, "\t-l     : toggle preserving the number of levels [default = %s]\n", fUpdateLevel? "yes": "no" );
     fprintf( pErr, "\t-z     : toggle using zero-cost replacements [default = %s]\n", fUseZeros? "yes": "no" );
@@ -7510,9 +7528,8 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv )
     // set defaults
     memset( pPars, 0, sizeof(If_Par_t) );
     // user-controlable paramters
-    pPars->Mode        =  0;
     pPars->nLutSize    =  4;
-    pPars->nCutsMax    = 20;
+    pPars->nCutsMax    = 10;
     pPars->DelayTarget = -1;
     pPars->fPreprocess =  1;
     pPars->fArea       =  0;
@@ -7522,7 +7539,7 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv )
     pPars->fSeq        =  0;
     pPars->fVerbose    =  0;
     // internal parameters
-    pPars->fTruth      =  1;
+    pPars->fTruth      =  0;
     pPars->nLatches    =  pNtk? Abc_NtkLatchNum(pNtk) : 0;
     pPars->pLutLib     =  NULL; // Abc_FrameReadLibLut();
     pPars->pTimesArr   =  NULL; 
@@ -7530,21 +7547,10 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv )
     pPars->pFuncCost   =  NULL;   
 
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "MKCDpaflrsvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "KCDpaflrsvh" ) ) != EOF )
     {
         switch ( c )
         {
-        case 'M':
-            if ( globalUtilOptind >= argc )
-            {
-                fprintf( pErr, "Command line switch \"-M\" should be followed by a positive integer.\n" );
-                goto usage;
-            }
-            pPars->Mode = atoi(argv[globalUtilOptind]);
-            globalUtilOptind++;
-            if ( pPars->Mode < 0 ) 
-                goto usage;
-            break;
         case 'K':
             if ( globalUtilOptind >= argc )
             {
@@ -7614,19 +7620,33 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv )
     if ( pPars->fSeq )
     {
         fprintf( pErr, "Sequential mapping is currently being implemented.\n" );
-        goto usage;
+        return 1;
     }
 
-    if ( pPars->Mode < 0 || pPars->Mode > 4 )
+    if ( pPars->nLutSize < 3 || pPars->nLutSize > IF_MAX_LUTSIZE )
     {
-        fprintf( pErr, "Incorrect mapping mode.\n" );
-        goto usage;
+        fprintf( pErr, "Incorrect LUT size (%d).\n", pPars->nLutSize );
+        return 1;
     }
 
     if ( pPars->nCutsMax < 2 || pPars->nCutsMax >= (1<<12) )
     {
         fprintf( pErr, "Incorrect number of cuts.\n" );
-        goto usage;
+        return 1;
+    }
+
+    if ( Abc_NtkGetChoiceNum( pNtk ) )
+    {
+        printf( "Performing FPGA mapping with choices.\n" );
+//        printf( "Currently mapping with choices is not enabled.\n" );
+        pPars->fTruth = 1;
+//        return 1;
+    }
+
+    if ( pPars->fTruth && pPars->nLutSize > IF_MAX_FUNC_LUTSIZE )
+    {
+        fprintf( pErr, "Mapping with choices requires computing truth tables. In this case, the LUT size cannot be more than %d.\n", IF_MAX_FUNC_LUTSIZE );
+        return 1;
     }
 
     // set the latch paths
@@ -7686,21 +7706,16 @@ usage:
         sprintf( LutSize, "library" );
     else
         sprintf( LutSize, "%d", pPars->nLutSize );
-    fprintf( pErr, "usage: if [-M num] [-K num] [-C num] [-D float] [-pafrsvh]\n" );
-    fprintf( pErr, "\t           performs FPGA mapping of the network as follows:\n" );
-    fprintf( pErr, "\t               1 - delay only\n" );
-    fprintf( pErr, "\t               2 - area only\n" );
-    fprintf( pErr, "\t               3 - area under delay constraints\n" );
-    fprintf( pErr, "\t               4 - area under delay constraints with area recovery\n" );
-    fprintf( pErr, "\t-M num   : the mapping mode [default = %d]\n", pPars->Mode );
-    fprintf( pErr, "\t-K num   : the number of LUT inputs (2 < num < 32) [default = %s]\n", LutSize );
+    fprintf( pErr, "usage: if [-K num] [-C num] [-D float] [-pafrsvh]\n" );
+    fprintf( pErr, "\t           performs FPGA technology mapping of the network\n" );
+    fprintf( pErr, "\t-K num   : the number of LUT inputs (2 < num < %d) [default = %s]\n", IF_MAX_LUTSIZE+1, LutSize );
     fprintf( pErr, "\t-C num   : the max number of cuts to use (1 < num < 2^12) [default = %d]\n", pPars->nCutsMax );
     fprintf( pErr, "\t-D float : sets the delay constraint for the mapping [default = %s]\n", Buffer );  
     fprintf( pErr, "\t-p       : toggles preprocessing using several starting points [default = %s]\n", pPars->fPreprocess? "yes": "no" );
     fprintf( pErr, "\t-a       : toggles area-oriented mapping [default = %s]\n", pPars->fArea? "yes": "no" );
     fprintf( pErr, "\t-f       : toggles one fancy feature [default = %s]\n", pPars->fFancy? "yes": "no" );
-//    fprintf( pErr, "\t-l       : optimizes latch paths for delay, other paths for area [default = %s]\n", pPars->fLatchPaths? "yes": "no" );
     fprintf( pErr, "\t-r       : enables expansion/reduction of the best cuts [default = %s]\n", pPars->fExpRed? "yes": "no" );
+    fprintf( pErr, "\t-l       : optimizes latch paths for delay, other paths for area [default = %s]\n", pPars->fLatchPaths? "yes": "no" );
     fprintf( pErr, "\t-s       : toggles sequential mapping [default = %s]\n", pPars->fSeq? "yes": "no" );
     fprintf( pErr, "\t-v       : toggles verbose output [default = %s]\n", pPars->fVerbose? "yes": "no" );
     fprintf( pErr, "\t-h       : prints the command usage\n");
diff --git a/src/base/abci/abcIf.c b/src/base/abci/abcIf.c
index 948a1d77..d2129e82 100644
--- a/src/base/abci/abcIf.c
+++ b/src/base/abci/abcIf.c
@@ -28,8 +28,9 @@
 
 static If_Man_t *  Abc_NtkToIf( Abc_Ntk_t * pNtk, If_Par_t * pPars );
 static Abc_Ntk_t * Abc_NtkFromIf( If_Man_t * pIfMan, Abc_Ntk_t * pNtk );
-static Abc_Obj_t * Abc_NodeFromIf_rec( Abc_Ntk_t * pNtkNew, If_Man_t * pIfMan, If_Obj_t * pIfObj );
+static Abc_Obj_t * Abc_NodeFromIf_rec( Abc_Ntk_t * pNtkNew, If_Man_t * pIfMan, If_Obj_t * pIfObj, Vec_Int_t * vCover );
 static Hop_Obj_t * Abc_NodeIfToHop( Hop_Man_t * pHopMan, If_Man_t * pIfMan, If_Obj_t * pIfObj );
+static Vec_Ptr_t * Abc_NtkFindGoodOrder( Abc_Ntk_t * pNtk );
  
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -53,14 +54,6 @@ Abc_Ntk_t * Abc_NtkIf( Abc_Ntk_t * pNtk, If_Par_t * pPars )
 
     assert( Abc_NtkIsStrash(pNtk) );
 
-    // print a warning about choice nodes
-    if ( Abc_NtkGetChoiceNum( pNtk ) )
-    {
-//        printf( "Performing FPGA mapping with choices.\n" );
-        printf( "Currently mapping with choices is not enabled.\n" );
-        return NULL;
-    }
-
     // get timing information
     pPars->pTimesArr = Abc_NtkGetCiArrivalFloats(pNtk);
     pPars->pTimesReq = NULL;
@@ -111,9 +104,12 @@ If_Man_t * Abc_NtkToIf( Abc_Ntk_t * pNtk, If_Par_t * pPars )
     ProgressBar * pProgress;
     If_Man_t * pIfMan;
     Abc_Obj_t * pNode, * pFanin, * pPrev;
+    Vec_Ptr_t * vNodes;
     int i;
 
     assert( Abc_NtkIsStrash(pNtk) );
+//    vNodes = Abc_NtkFindGoodOrder( pNtk );
+    vNodes = Abc_AigDfs( pNtk, 0, 0 );
 
     // start the mapping manager and set its parameters
     pIfMan = If_ManStart( pPars );
@@ -125,19 +121,24 @@ If_Man_t * Abc_NtkToIf( Abc_Ntk_t * pNtk, If_Par_t * pPars )
 
     // load the AIG into the mapper
     pProgress = Extra_ProgressBarStart( stdout, Abc_NtkObjNumMax(pNtk) );
-    Abc_AigForEachAnd( pNtk, pNode, i )
+//    Abc_AigForEachAnd( pNtk, pNode, i )
+    Vec_PtrForEachEntry( vNodes, pNode, i )
     {
-        Extra_ProgressBarUpdate( pProgress, i, NULL );
+        Extra_ProgressBarUpdate( pProgress, i, "Initial" );
         // add the node to the mapper
         pNode->pCopy = (Abc_Obj_t *)If_ManCreateAnd( pIfMan, 
             (If_Obj_t *)Abc_ObjFanin0(pNode)->pCopy, Abc_ObjFaninC0(pNode), 
             (If_Obj_t *)Abc_ObjFanin1(pNode)->pCopy, Abc_ObjFaninC1(pNode) );
         // set up the choice node
         if ( Abc_AigNodeIsChoice( pNode ) )
+        {
             for ( pPrev = pNode, pFanin = pNode->pData; pFanin; pPrev = pFanin, pFanin = pFanin->pData )
                 If_ObjSetChoice( (If_Obj_t *)pPrev->pCopy, (If_Obj_t *)pFanin->pCopy );
+            If_ManCreateChoice( pIfMan, (If_Obj_t *)pNode->pCopy );
+        }
     }
     Extra_ProgressBarStop( pProgress );
+    Vec_PtrFree( vNodes );
 
     // set the primary outputs without copying the phase
     Abc_NtkForEachCo( pNtk, pNode, i )
@@ -161,6 +162,7 @@ Abc_Ntk_t * Abc_NtkFromIf( If_Man_t * pIfMan, Abc_Ntk_t * pNtk )
     ProgressBar * pProgress;
     Abc_Ntk_t * pNtkNew;
     Abc_Obj_t * pNode, * pNodeNew;
+    Vec_Int_t * vCover;
     int i, nDupGates;
     // create the new network
     if ( pIfMan->pPars->fUseBdds )
@@ -177,15 +179,17 @@ Abc_Ntk_t * Abc_NtkFromIf( If_Man_t * pIfMan, Abc_Ntk_t * pNtk )
     Abc_NtkForEachCi( pNtk, pNode, i )
         If_ObjSetCopy( If_ManPi(pIfMan, i), pNode->pCopy );
     // process the nodes in topological order
+    vCover = Vec_IntAlloc( 1 << 16 );
     pProgress = Extra_ProgressBarStart( stdout, Abc_NtkCoNum(pNtk) );
     Abc_NtkForEachCo( pNtk, pNode, i )
     {
-        Extra_ProgressBarUpdate( pProgress, i, NULL );
-        pNodeNew = Abc_NodeFromIf_rec( pNtkNew, pIfMan, If_ObjFanin0(If_ManPo(pIfMan, i)) );
+        Extra_ProgressBarUpdate( pProgress, i, "Final" );
+        pNodeNew = Abc_NodeFromIf_rec( pNtkNew, pIfMan, If_ObjFanin0(If_ManPo(pIfMan, i)), vCover );
         pNodeNew = Abc_ObjNotCond( pNodeNew, If_ObjFaninC0(If_ManPo(pIfMan, i)) );
         Abc_ObjAddFanin( pNode->pCopy, pNodeNew );
     }
     Extra_ProgressBarStop( pProgress );
+    Vec_IntFree( vCover );
     // remove the constant node if not used
     pNodeNew = (Abc_Obj_t *)If_ObjCopy( If_ManConst1(pIfMan) );
     if ( Abc_ObjFanoutNum(pNodeNew) == 0 )
@@ -208,7 +212,7 @@ Abc_Ntk_t * Abc_NtkFromIf( If_Man_t * pIfMan, Abc_Ntk_t * pNtk )
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Obj_t * Abc_NodeFromIf_rec( Abc_Ntk_t * pNtkNew, If_Man_t * pIfMan, If_Obj_t * pIfObj )
+Abc_Obj_t * Abc_NodeFromIf_rec( Abc_Ntk_t * pNtkNew, If_Man_t * pIfMan, If_Obj_t * pIfObj, Vec_Int_t * vCover )
 {
     Abc_Obj_t * pNodeNew;
     If_Cut_t * pCutBest;
@@ -224,40 +228,60 @@ Abc_Obj_t * Abc_NodeFromIf_rec( Abc_Ntk_t * pNtkNew, If_Man_t * pIfMan, If_Obj_t
     pNodeNew = Abc_NtkCreateNode( pNtkNew );
     pCutBest = If_ObjCutBest( pIfObj );
     If_CutForEachLeaf( pIfMan, pCutBest, pIfLeaf, i )
-        Abc_ObjAddFanin( pNodeNew, Abc_NodeFromIf_rec(pNtkNew, pIfMan, pIfLeaf) );
+        Abc_ObjAddFanin( pNodeNew, Abc_NodeFromIf_rec(pNtkNew, pIfMan, pIfLeaf, vCover) );
     // derive the function of this node
     if ( pIfMan->pPars->fTruth )
     {
         if ( pIfMan->pPars->fUseBdds )
         { 
             extern void Abc_NodeBddReorder( void * p, Abc_Obj_t * pNode );
-            extern DdNode * Kit_TruthToBdd( DdManager * dd, unsigned * pTruth, int nVars );
             // transform truth table into the BDD 
-            pNodeNew->pData = Kit_TruthToBdd( pNtkNew->pManFunc, If_CutTruth(pCutBest), pCutBest->nLimit );
-            // reorder the fanins to minimize the BDD size
-            Abc_NodeBddReorder( pIfMan->pPars->pReoMan, pNodeNew );
+            pNodeNew->pData = Kit_TruthToBdd( pNtkNew->pManFunc, If_CutTruth(pCutBest), If_CutLeaveNum(pCutBest), 0 );  Cudd_Ref(pNodeNew->pData); 
+            if ( pNodeNew->pData == Cudd_ReadLogicZero(pNtkNew->pManFunc) || pNodeNew->pData == Cudd_ReadOne(pNtkNew->pManFunc) )
+            {
+                // replace the node by a constant node
+                pNodeNew = pNodeNew->pData == Cudd_ReadOne(pNtkNew->pManFunc) ? Abc_NtkCreateNodeConst1(pNtkNew) : Abc_NtkCreateNodeConst0(pNtkNew);
+            }
+            else
+            {
+                // make sure the node is minimum base
+                Abc_NodeMinimumBase( pNodeNew );
+                // reorder the fanins to minimize the BDD size
+                Abc_NodeBddReorder( pIfMan->pPars->pReoMan, pNodeNew );
+            }
         }
         else if ( pIfMan->pPars->fUseSops ) 
         {
-            Vec_Int_t * vCover = Vec_IntAlloc( 1 << 16 );
             // transform truth table into the SOP
-            int RetValue = Kit_TruthIsop( If_CutTruth(pCutBest), pCutBest->nLimit, vCover, 0 );
-            assert( RetValue == 0 );
-            // derive the AIG for that tree
-            pNodeNew->pData = Abc_SopCreateFromIsop( pNtkNew->pManFunc, pCutBest->nLimit, vCover );
-            Vec_IntFree( vCover );
+            int RetValue = Kit_TruthIsop( If_CutTruth(pCutBest), If_CutLeaveNum(pCutBest), vCover, 1 );
+            assert( RetValue == 0 || RetValue == 1 );
+            // check the case of constant cover
+            if ( Vec_IntSize(vCover) == 0 || (Vec_IntSize(vCover) == 1 && Vec_IntEntry(vCover,0) == 0) )
+            {
+                assert( RetValue == 0 );
+                pNodeNew->pData = Abc_SopCreateAnd( pNtkNew->pManFunc, If_CutLeaveNum(pCutBest), NULL );
+                pNodeNew = (Vec_IntSize(vCover) == 0) ? Abc_NtkCreateNodeConst0(pNtkNew) : Abc_NtkCreateNodeConst1(pNtkNew);
+            }
+            else
+            {
+                // derive the AIG for that tree
+                pNodeNew->pData = Abc_SopCreateFromIsop( pNtkNew->pManFunc, If_CutLeaveNum(pCutBest), vCover );
+                if ( RetValue )
+                    Abc_SopComplement( pNodeNew->pData );
+            }
         }
         else 
         {
             extern Hop_Obj_t * Kit_GraphToHop( Hop_Man_t * pMan, Kit_Graph_t * pGraph );
-            Vec_Int_t * vMemory = Vec_IntAlloc( 1 << 16 );
             // transform truth table into the decomposition tree
-            Kit_Graph_t * pGraph = Kit_TruthToGraph( If_CutTruth(pCutBest), pCutBest->nLimit, vMemory );
+            Kit_Graph_t * pGraph = Kit_TruthToGraph( If_CutTruth(pCutBest), If_CutLeaveNum(pCutBest), vCover );
             // derive the AIG for the decomposition tree
             pNodeNew->pData = Kit_GraphToHop( pNtkNew->pManFunc, pGraph );
             Kit_GraphFree( pGraph );
-            Vec_IntFree( vMemory );
         }
+        // complement the node if the cut was complemented
+        if ( pCutBest->fCompl )
+            Abc_NodeComplement( pNodeNew );
     }
     else
         pNodeNew->pData = Abc_NodeIfToHop( pNtkNew->pManFunc, pIfMan, pIfObj );
@@ -333,6 +357,116 @@ Hop_Obj_t * Abc_NodeIfToHop( Hop_Man_t * pHopMan, If_Man_t * pIfMan, If_Obj_t *
 }
 
 
+/**Function*************************************************************
+
+  Synopsis    [Comparison for two nodes with the flow.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_ObjCompareFlow( Abc_Obj_t ** ppNode0, Abc_Obj_t ** ppNode1 )
+{
+    float Flow0 = Abc_Int2Float((int)(*ppNode0)->pCopy);
+    float Flow1 = Abc_Int2Float((int)(*ppNode1)->pCopy);
+    if ( Flow0 > Flow1 )
+        return -1;
+    if ( Flow0 < Flow1 )
+        return 1;
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Orders AIG nodes so that nodes from larger cones go first.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkFindGoodOrder_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes )
+{
+    if ( !Abc_ObjIsNode(pNode) )
+        return;
+    assert( Abc_ObjIsNode( pNode ) );
+    // if this node is already visited, skip
+    if ( Abc_NodeIsTravIdCurrent( pNode ) )
+        return;
+    // mark the node as visited
+    Abc_NodeSetTravIdCurrent( pNode );
+    // visit the transitive fanin of the node
+    Abc_NtkFindGoodOrder_rec( Abc_ObjFanin0(pNode), vNodes );
+    Abc_NtkFindGoodOrder_rec( Abc_ObjFanin1(pNode), vNodes );
+    // add the node after the fanins have been added
+    Vec_PtrPush( vNodes, pNode );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Orders AIG nodes so that nodes from larger cones go first.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Abc_NtkFindGoodOrder( Abc_Ntk_t * pNtk )
+{
+    Vec_Ptr_t * vNodes, * vCos;
+    Abc_Obj_t * pNode, * pFanin0, * pFanin1;
+    float Flow0, Flow1;
+    int i;
+
+    // initialize the flow
+    Abc_AigConst1(pNtk)->pCopy = NULL;
+    Abc_NtkForEachCi( pNtk, pNode, i )
+        pNode->pCopy = NULL;
+    // compute the flow
+    Abc_AigForEachAnd( pNtk, pNode, i )
+    {
+        pFanin0 = Abc_ObjFanin0(pNode);
+        pFanin1 = Abc_ObjFanin1(pNode);
+        Flow0 = Abc_Int2Float((int)pFanin0->pCopy)/Abc_ObjFanoutNum(pFanin0);
+        Flow1 = Abc_Int2Float((int)pFanin1->pCopy)/Abc_ObjFanoutNum(pFanin1);
+        pNode->pCopy = (Abc_Obj_t *)Abc_Float2Int(Flow0 + Flow1+(float)1.0);
+    }
+    // find the flow of the COs
+    vCos = Vec_PtrAlloc( Abc_NtkCoNum(pNtk) );
+    Abc_NtkForEachCo( pNtk, pNode, i )
+    {
+        pNode->pCopy = Abc_ObjFanin0(pNode)->pCopy;
+//        pNode->pCopy = (Abc_Obj_t *)Abc_Float2Int((float)Abc_ObjFanin0(pNode)->Level);
+        Vec_PtrPush( vCos, pNode );
+    }
+
+    // sort nodes in the increasing order of the flow
+    qsort( (Abc_Obj_t **)Vec_PtrArray(vCos), Abc_NtkCoNum(pNtk), 
+        sizeof(Abc_Obj_t *), (int (*)(const void *, const void *))Abc_ObjCompareFlow );
+    // verify sorting
+    pFanin0 = Vec_PtrEntry(vCos, 0);
+    pFanin1 = Vec_PtrEntryLast(vCos);
+    assert( Abc_Int2Float((int)pFanin0->pCopy) >= Abc_Int2Float((int)pFanin1->pCopy) );
+
+    // collect the nodes in the topological order from the new array
+    Abc_NtkIncrementTravId( pNtk );
+    vNodes = Vec_PtrAlloc( 100 );
+    Vec_PtrForEachEntry( vCos, pNode, i )
+    {
+        Abc_NtkFindGoodOrder_rec( Abc_ObjFanin0(pNode), vNodes );
+//        printf( "%.2f ", Abc_Int2Float((int)pNode->pCopy) );
+    }
+    Vec_PtrFree( vCos );
+    return vNodes;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abci/abcRenode.c b/src/base/abci/abcRenode.c
index 4f3003a6..b8aa49a4 100644
--- a/src/base/abci/abcRenode.c
+++ b/src/base/abci/abcRenode.c
@@ -27,9 +27,9 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-static int Abc_NtkRenodeEvalBdd( unsigned * pTruth, int nVars );
-static int Abc_NtkRenodeEvalSop( unsigned * pTruth, int nVars );
-static int Abc_NtkRenodeEvalAig( unsigned * pTruth, int nVars );
+static int Abc_NtkRenodeEvalBdd( If_Cut_t * pCut );
+static int Abc_NtkRenodeEvalSop( If_Cut_t * pCut );
+static int Abc_NtkRenodeEvalAig( If_Cut_t * pCut );
 
 static reo_man * s_pReo      = NULL;
 static DdManager * s_pDd     = NULL;
@@ -50,7 +50,7 @@ static Vec_Int_t * s_vMemory = NULL;
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Ntk_t * Abc_NtkRenode( Abc_Ntk_t * pNtk, int nFaninMax, int nCubeMax, int fUseBdds, int fUseSops, int fVerbose )
+Abc_Ntk_t * Abc_NtkRenode( Abc_Ntk_t * pNtk, int nFaninMax, int nCubeMax, int fArea, int fUseBdds, int fUseSops, int fVerbose )
 {
     extern Abc_Ntk_t * Abc_NtkIf( Abc_Ntk_t * pNtk, If_Par_t * pPars );
     If_Par_t Pars, * pPars = &Pars;
@@ -59,19 +59,19 @@ Abc_Ntk_t * Abc_NtkRenode( Abc_Ntk_t * pNtk, int nFaninMax, int nCubeMax, int fU
     // set defaults
     memset( pPars, 0, sizeof(If_Par_t) );
     // user-controlable paramters
-    pPars->Mode        =  0;
     pPars->nLutSize    =  nFaninMax;
-    pPars->nCutsMax    = 10;
+    pPars->nCutsMax    =  nCubeMax;
     pPars->DelayTarget = -1;
     pPars->fPreprocess =  1;
-    pPars->fArea       =  0;
+    pPars->fArea       =  fArea;
     pPars->fFancy      =  0;
     pPars->fExpRed     =  0; //
     pPars->fLatchPaths =  0;
     pPars->fSeq        =  0;
-    pPars->fVerbose    =  0;
+    pPars->fVerbose    =  fVerbose;
     // internal parameters
     pPars->fTruth      =  1;
+    pPars->fUsePerm    =  1; //!fUseSops;
     pPars->nLatches    =  0;
     pPars->pLutLib     =  NULL; // Abc_FrameReadLibLut();
     pPars->pTimesArr   =  NULL; 
@@ -130,18 +130,22 @@ Abc_Ntk_t * Abc_NtkRenode( Abc_Ntk_t * pNtk, int nFaninMax, int nCubeMax, int fU
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_NtkRenodeEvalBdd( unsigned * pTruth, int nVars )
+int Abc_NtkRenodeEvalBdd( If_Cut_t * pCut )
 {
+    int pOrder[IF_MAX_LUTSIZE];
     DdNode * bFunc, * bFuncNew;
-    int nNodes, nSupport;
-    bFunc = Kit_TruthToBdd( s_pDd, pTruth, nVars );           Cudd_Ref( bFunc );
-    bFuncNew = Extra_Reorder( s_pReo, s_pDd, bFunc, NULL );   Cudd_Ref( bFuncNew );
-//    nSupport = Cudd_SupportSize( s_pDd, bFuncNew );
-    nSupport = 1;
-    nNodes = Cudd_DagSize( bFuncNew );
+    int i, k, nNodes;
+    for ( i = 0; i < If_CutLeaveNum(pCut); i++ )
+        pCut->pPerm[i] = pOrder[i] = -100;
+    bFunc = Kit_TruthToBdd( s_pDd, If_CutTruth(pCut), If_CutLeaveNum(pCut), 0 );  Cudd_Ref( bFunc );
+    bFuncNew = Extra_Reorder( s_pReo, s_pDd, bFunc, pOrder );                     Cudd_Ref( bFuncNew );
+    for ( i = k = 0; i < If_CutLeaveNum(pCut); i++ )
+        if ( pOrder[i] >= 0 )
+            pCut->pPerm[pOrder[i]] = ++k; // double-check this!
+    nNodes = -1 + Cudd_DagSize( bFuncNew );
     Cudd_RecursiveDeref( s_pDd, bFuncNew );
     Cudd_RecursiveDeref( s_pDd, bFunc );
-    return (nSupport << 16) | nNodes;
+    return nNodes; 
 }
 
 /**Function*************************************************************
@@ -155,13 +159,16 @@ int Abc_NtkRenodeEvalBdd( unsigned * pTruth, int nVars )
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_NtkRenodeEvalSop( unsigned * pTruth, int nVars )
+int Abc_NtkRenodeEvalSop( If_Cut_t * pCut )
 {
-    int nCubes, RetValue;
-    RetValue = Kit_TruthIsop( pTruth, nVars, s_vMemory, 0 );
-    assert( RetValue == 0 );
-    nCubes = Vec_IntSize( s_vMemory );
-    return (1 << 16) | nCubes;
+    int i, RetValue;
+    for ( i = 0; i < If_CutLeaveNum(pCut); i++ )
+        pCut->pPerm[i] = 1;
+    RetValue = Kit_TruthIsop( If_CutTruth(pCut), If_CutLeaveNum(pCut), s_vMemory, 1 );
+    if ( RetValue == -1 )
+        return ABC_INFINITY;
+    assert( RetValue == 0 || RetValue == 1 );
+    return Vec_IntSize( s_vMemory );
 }
 
 /**Function*************************************************************
@@ -175,16 +182,22 @@ int Abc_NtkRenodeEvalSop( unsigned * pTruth, int nVars )
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_NtkRenodeEvalAig( unsigned * pTruth, int nVars )
+int Abc_NtkRenodeEvalAig( If_Cut_t * pCut )
 {
     Kit_Graph_t * pGraph;
-    int nNodes, nDepth;
-    pGraph = Kit_TruthToGraph( pTruth, nVars, s_vMemory );
+    int i, nNodes;
+    pGraph = Kit_TruthToGraph( If_CutTruth(pCut), If_CutLeaveNum(pCut), s_vMemory );
+    if ( pGraph == NULL )
+    {
+        for ( i = 0; i < If_CutLeaveNum(pCut); i++ )
+            pCut->pPerm[i] = 100;
+        return ABC_INFINITY;
+    }
     nNodes = Kit_GraphNodeNum( pGraph );
-//    nDepth = Kit_GraphLevelNum( pGraph );
-    nDepth = 1;
+    for ( i = 0; i < If_CutLeaveNum(pCut); i++ )
+        pCut->pPerm[i] = Kit_GraphLeafDepth_rec( pGraph, Kit_GraphNodeLast(pGraph), Kit_GraphNode(pGraph, i) );
     Kit_GraphFree( pGraph );
-    return (nDepth << 16) | nNodes;
+    return nNodes;
 }
 
 ////////////////////////////////////////////////////////////////////////