Version abc70219

9 files changed, 97 insertions, 70 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index ae00ce5c..cf7cc0e9 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -3395,7 +3395,7 @@ int Abc_CommandLogic( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
 
     // get the new network
-    pNtkRes = Abc_NtkAigToLogicSop( pNtk );
+    pNtkRes = Abc_NtkToLogic( pNtk );
     if ( pNtkRes == NULL )
     {
         fprintf( pErr, "Converting to a logic network has failed.\n" );
@@ -3984,7 +3984,7 @@ int Abc_CommandSop( Abc_Frame_t * pAbc, int argc, char ** argv )
         fprintf( pErr, "Converting to SOP is possible only for logic networks.\n" );
         return 1;
     }
-    if ( !Abc_NtkLogicToSop(pNtk, fDirect) )
+    if ( !Abc_NtkToSop(pNtk, fDirect) )
     {
         fprintf( pErr, "Converting to SOP has failed.\n" );
         return 1;
@@ -4047,7 +4047,7 @@ int Abc_CommandBdd( Abc_Frame_t * pAbc, int argc, char ** argv )
         fprintf( pOut, "The logic network is already in the BDD form.\n" );
         return 0;
     }
-    if ( !Abc_NtkLogicToBdd(pNtk) )
+    if ( !Abc_NtkToBdd(pNtk) )
     {
         fprintf( pErr, "Converting to BDD has failed.\n" );
         return 1;
@@ -4109,7 +4109,7 @@ int Abc_CommandAig( Abc_Frame_t * pAbc, int argc, char ** argv )
         fprintf( pOut, "The logic network is already in the AIG form.\n" );
         return 0;
     }
-    if ( !Abc_NtkLogicToAig(pNtk) )
+    if ( !Abc_NtkToAig(pNtk) )
     {
         fprintf( pErr, "Converting to AIG has failed.\n" );
         return 1;
@@ -7719,7 +7719,7 @@ int Abc_CommandSuperChoiceLut( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
 
     // convert the network into the SOP network
-    pNtkRes = Abc_NtkAigToLogicSop( pNtk );
+    pNtkRes = Abc_NtkToLogic( pNtk );
 
     // get the new network
     if ( !Abc_NtkSuperChoiceLut( pNtkRes, nLutSize, nCutSizeMax, fVerbose ) )
@@ -8716,7 +8716,7 @@ int Abc_CommandRetime( Abc_Frame_t * pAbc, int argc, char ** argv )
             return 0;
         }
         // convert the network into an SOP network
-        pNtkRes = Abc_NtkAigToLogicSop( pNtk );
+        pNtkRes = Abc_NtkToLogic( pNtk );
         // perform the retiming
         Abc_NtkRetime( pNtkRes, Mode, fForward, fBackward, fVerbose );
         // replace the current network
@@ -8725,7 +8725,7 @@ int Abc_CommandRetime( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
 
     // get the network in the SOP form
-    if ( !Abc_NtkLogicToSop(pNtk, 0) )
+    if ( !Abc_NtkToSop(pNtk, 0) )
     {
         printf( "Converting to SOPs has failed.\n" );
         return 0;
@@ -9712,7 +9712,7 @@ int Abc_CommandSat( Abc_Frame_t * pAbc, int argc, char ** argv )
     else
     {
         assert( Abc_NtkIsLogic(pNtk) );
-        Abc_NtkLogicToBdd( pNtk );
+        Abc_NtkToBdd( pNtk );
         RetValue = Abc_NtkMiterSat( pNtk, (sint64)nConfLimit, (sint64)nInsLimit, fVerbose, NULL, NULL );
     }
 
diff --git a/src/base/abci/abcDebug.c b/src/base/abci/abcDebug.c
index 7771148e..95b95d89 100644
--- a/src/base/abci/abcDebug.c
+++ b/src/base/abci/abcDebug.c
@@ -196,7 +196,7 @@ Abc_Ntk_t * Abc_NtkAutoDebugModify( Abc_Ntk_t * pNtkInit, int Step, int fConst1
 
     Abc_NtkSweep( pNtk, 0 );
     Abc_NtkCleanupSeq( pNtk, 0, 0, 0 );
-    Abc_NtkLogicToSop( pNtk, 0 );
+    Abc_NtkToSop( pNtk, 0 );
     Abc_NtkCycleInitStateSop( pNtk, 50, 0 );
     return pNtk;
 }
diff --git a/src/base/abci/abcDress.c b/src/base/abci/abcDress.c
index d7bb70fe..cc9ce0b9 100644
--- a/src/base/abci/abcDress.c
+++ b/src/base/abci/abcDress.c
@@ -63,7 +63,7 @@ void Abc_NtkDress( Abc_Ntk_t * pNtkLogic, char * pFileName, int fVerbose )
     Abc_NtkCleanCopy(pNtkOrig);
 
     // convert it into the logic network
-    pNtkLogicOrig = Abc_NtkNetlistToLogic( pNtkOrig );
+    pNtkLogicOrig = Abc_NtkToLogic( pNtkOrig );
     // check that the networks have the same PIs/POs/latches
     if ( !Abc_NtkCompareSignals( pNtkLogic, pNtkLogicOrig, 1, 1 ) )
     {
diff --git a/src/base/abci/abcFxu.c b/src/base/abci/abcFxu.c
index b6d57a5c..45515dd1 100644
--- a/src/base/abci/abcFxu.c
+++ b/src/base/abci/abcFxu.c
@@ -61,7 +61,7 @@ bool Abc_NtkFastExtract( Abc_Ntk_t * pNtk, Fxu_Data_t * p )
 //        Abc_NtkBddToSop(pNtk);
     }
     // get the network in the SOP form
-    if ( !Abc_NtkLogicToSop(pNtk, 0) )
+    if ( !Abc_NtkToSop(pNtk, 0) )
     {
         printf( "Abc_NtkFastExtract(): Converting to SOPs has failed.\n" );
         return 0;
diff --git a/src/base/abci/abcIvy.c b/src/base/abci/abcIvy.c
index 0f0d9c8b..abcde7ce 100644
--- a/src/base/abci/abcIvy.c
+++ b/src/base/abci/abcIvy.c
@@ -27,9 +27,9 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-static Abc_Ntk_t *  Abc_NtkFromAig( Abc_Ntk_t * pNtkOld, Ivy_Man_t * pMan );
-static Abc_Ntk_t *  Abc_NtkFromAigSeq( Abc_Ntk_t * pNtkOld, Ivy_Man_t * pMan, int fHaig );
-static Ivy_Man_t *  Abc_NtkToAig( Abc_Ntk_t * pNtkOld );
+static Abc_Ntk_t *  Abc_NtkFromIvy( Abc_Ntk_t * pNtkOld, Ivy_Man_t * pMan );
+static Abc_Ntk_t *  Abc_NtkFromIvySeq( Abc_Ntk_t * pNtkOld, Ivy_Man_t * pMan, int fHaig );
+static Ivy_Man_t *  Abc_NtkToIvy( Abc_Ntk_t * pNtkOld );
 
 static void         Abc_NtkStrashPerformAig( Abc_Ntk_t * pNtk, Ivy_Man_t * pMan );
 static Ivy_Obj_t *  Abc_NodeStrashAig( Ivy_Man_t * pMan, Abc_Obj_t * pNode );
@@ -93,7 +93,7 @@ Ivy_Man_t * Abc_NtkIvyBefore( Abc_Ntk_t * pNtk, int fSeq, int fUseDc )
     if ( Abc_NtkGetChoiceNum( pNtk ) )
         printf( "Warning: The choice nodes in the initial AIG are removed by strashing.\n" );
     // convert to the AIG manager
-    pMan = Abc_NtkToAig( pNtk );
+    pMan = Abc_NtkToIvy( pNtk );
     if ( !Ivy_ManCheck( pMan ) )
     {
         printf( "AIG check has failed.\n" );
@@ -130,9 +130,9 @@ Abc_Ntk_t * Abc_NtkIvyAfter( Abc_Ntk_t * pNtk, Ivy_Man_t * pMan, int fSeq, int f
     int nNodes, fCleanup = 1;
     // convert from the AIG manager
     if ( fSeq )
-        pNtkAig = Abc_NtkFromAigSeq( pNtk, pMan, fHaig );
+        pNtkAig = Abc_NtkFromIvySeq( pNtk, pMan, fHaig );
     else
-        pNtkAig = Abc_NtkFromAig( pNtk, pMan );
+        pNtkAig = Abc_NtkFromIvy( pNtk, pMan );
     // report the cleanup results
     if ( !fHaig && fCleanup && (nNodes = Abc_AigCleanup(pNtkAig->pManFunc)) )
         printf( "Warning: AIG cleanup removed %d nodes (this is not a bug).\n", nNodes );
@@ -608,7 +608,7 @@ Abc_Ntk_t * Abc_NtkIvy( Abc_Ntk_t * pNtk )
         printf( "Warning: The choice nodes in the initial AIG are removed by strashing.\n" );
 
     // convert to the AIG manager
-    pMan = Abc_NtkToAig( pNtk );
+    pMan = Abc_NtkToIvy( pNtk );
     if ( !Ivy_ManCheck( pMan ) )
     {
         Vec_IntFree( vInit );
@@ -654,8 +654,8 @@ Abc_Ntk_t * Abc_NtkIvy( Abc_Ntk_t * pNtk )
 
 /*
     // convert from the AIG manager
-    pNtkAig = Abc_NtkFromAig( pNtk, pMan );
-//    pNtkAig = Abc_NtkFromAigSeq( pNtk, pMan );
+    pNtkAig = Abc_NtkFromIvy( pNtk, pMan );
+//    pNtkAig = Abc_NtkFromIvySeq( pNtk, pMan );
     Ivy_ManStop( pMan );
 
     // report the cleanup results
@@ -691,7 +691,7 @@ Abc_Ntk_t * Abc_NtkIvy( Abc_Ntk_t * pNtk )
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Ntk_t * Abc_NtkFromAig( Abc_Ntk_t * pNtkOld, Ivy_Man_t * pMan )
+Abc_Ntk_t * Abc_NtkFromIvy( Abc_Ntk_t * pNtkOld, Ivy_Man_t * pMan )
 {
     Vec_Int_t * vNodes;
     Abc_Ntk_t * pNtk;
@@ -732,7 +732,7 @@ Abc_Ntk_t * Abc_NtkFromAig( Abc_Ntk_t * pNtkOld, Ivy_Man_t * pMan )
     }
     Vec_IntFree( vNodes );
     if ( !Abc_NtkCheck( pNtk ) )
-        fprintf( stdout, "Abc_NtkFromAig(): Network check has failed.\n" );
+        fprintf( stdout, "Abc_NtkFromIvy(): Network check has failed.\n" );
     return pNtk;
 }
 
@@ -747,7 +747,7 @@ Abc_Ntk_t * Abc_NtkFromAig( Abc_Ntk_t * pNtkOld, Ivy_Man_t * pMan )
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Ntk_t * Abc_NtkFromAigSeq( Abc_Ntk_t * pNtkOld, Ivy_Man_t * pMan, int fHaig )
+Abc_Ntk_t * Abc_NtkFromIvySeq( Abc_Ntk_t * pNtkOld, Ivy_Man_t * pMan, int fHaig )
 {
     Vec_Int_t * vNodes, * vLatches;
     Abc_Ntk_t * pNtk;
@@ -830,7 +830,7 @@ Abc_Ntk_t * Abc_NtkFromAigSeq( Abc_Ntk_t * pNtkOld, Ivy_Man_t * pMan, int fHaig
     Vec_IntFree( vLatches );
     Vec_IntFree( vNodes );
     if ( !Abc_NtkCheck( pNtk ) )
-        fprintf( stdout, "Abc_NtkFromAigSeq(): Network check has failed.\n" );
+        fprintf( stdout, "Abc_NtkFromIvySeq(): Network check has failed.\n" );
     return pNtk;
 }
 
@@ -845,7 +845,7 @@ Abc_Ntk_t * Abc_NtkFromAigSeq( Abc_Ntk_t * pNtkOld, Ivy_Man_t * pMan, int fHaig
   SeeAlso     []
 
 ***********************************************************************/
-Ivy_Man_t * Abc_NtkToAig( Abc_Ntk_t * pNtkOld )
+Ivy_Man_t * Abc_NtkToIvy( Abc_Ntk_t * pNtkOld )
 {
     Ivy_Man_t * pMan;
     Abc_Obj_t * pObj;
diff --git a/src/base/abci/abcMini.c b/src/base/abci/abcMini.c
index dc90bee0..92985423 100644
--- a/src/base/abci/abcMini.c
+++ b/src/base/abci/abcMini.c
@@ -24,8 +24,8 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-static Hop_Man_t * Abc_NtkToAig( Abc_Ntk_t * pNtk );
-static Abc_Ntk_t * Abc_NtkFromAig( Abc_Ntk_t * pNtkOld, Hop_Man_t * pMan );
+static Hop_Man_t * Abc_NtkToMini( Abc_Ntk_t * pNtk );
+static Abc_Ntk_t * Abc_NtkFromMini( Abc_Ntk_t * pNtkOld, Hop_Man_t * pMan );
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -48,7 +48,7 @@ Abc_Ntk_t * Abc_NtkMiniBalance( Abc_Ntk_t * pNtk )
     Hop_Man_t * pMan, * pTemp;
     assert( Abc_NtkIsStrash(pNtk) );
     // convert to the AIG manager
-    pMan = Abc_NtkToAig( pNtk );
+    pMan = Abc_NtkToMini( pNtk );
     if ( pMan == NULL )
         return NULL;
     if ( !Hop_ManCheck( pMan ) )
@@ -64,7 +64,7 @@ Abc_Ntk_t * Abc_NtkMiniBalance( Abc_Ntk_t * pNtk )
     Hop_ManStop( pTemp );
     Hop_ManPrintStats( pMan );
     // convert from the AIG manager
-    pNtkAig = Abc_NtkFromAig( pNtk, pMan );
+    pNtkAig = Abc_NtkFromMini( pNtk, pMan );
     if ( pNtkAig == NULL )
         return NULL;
     Hop_ManStop( pMan );
@@ -89,7 +89,7 @@ Abc_Ntk_t * Abc_NtkMiniBalance( Abc_Ntk_t * pNtk )
   SeeAlso     []
 
 ***********************************************************************/
-Hop_Man_t * Abc_NtkToAig( Abc_Ntk_t * pNtk )
+Hop_Man_t * Abc_NtkToMini( Abc_Ntk_t * pNtk )
 {
     Hop_Man_t * pMan;
     Abc_Obj_t * pObj;
@@ -121,7 +121,7 @@ Hop_Man_t * Abc_NtkToAig( Abc_Ntk_t * pNtk )
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Ntk_t * Abc_NtkFromAig( Abc_Ntk_t * pNtk, Hop_Man_t * pMan )
+Abc_Ntk_t * Abc_NtkFromMini( Abc_Ntk_t * pNtk, Hop_Man_t * pMan )
 {
     Vec_Ptr_t * vNodes;
     Abc_Ntk_t * pNtkNew;
@@ -142,7 +142,7 @@ Abc_Ntk_t * Abc_NtkFromAig( Abc_Ntk_t * pNtk, Hop_Man_t * pMan )
     Hop_ManForEachPo( pMan, pObj, i )
         Abc_ObjAddFanin( Abc_NtkCo(pNtkNew, i), (Abc_Obj_t *)Hop_ObjChild0Copy(pObj) );
     if ( !Abc_NtkCheck( pNtkNew ) )
-        fprintf( stdout, "Abc_NtkFromAig(): Network check has failed.\n" );
+        fprintf( stdout, "Abc_NtkFromMini(): Network check has failed.\n" );
     return pNtkNew;
 }
 
diff --git a/src/base/abci/abcQuant.c b/src/base/abci/abcQuant.c
index 77d640c2..8591663e 100644
--- a/src/base/abci/abcQuant.c
+++ b/src/base/abci/abcQuant.c
@@ -30,6 +30,39 @@
 
 /**Function*************************************************************
 
+  Synopsis    [Performs fast synthesis.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkSynthesize( Abc_Ntk_t ** ppNtk, int fMoreEffort )
+{
+    Abc_Ntk_t * pNtk, * pNtkTemp;
+
+    pNtk = *ppNtk;
+
+    Abc_NtkRewrite( pNtk, 0, 0, 0, 0, 0 );
+    Abc_NtkRefactor( pNtk, 10, 16, 0, 0, 0, 0 );
+    pNtk = Abc_NtkBalance( pNtkTemp = pNtk, 0, 0, 0 );          
+    Abc_NtkDelete( pNtkTemp );
+
+    if ( fMoreEffort )
+    {
+        Abc_NtkRewrite( pNtk, 0, 0, 0, 0, 0 );
+        Abc_NtkRefactor( pNtk, 10, 16, 0, 0, 0, 0 );
+        pNtk = Abc_NtkBalance( pNtkTemp = pNtk, 0, 0, 0 );          
+        Abc_NtkDelete( pNtkTemp );
+    }
+
+    *ppNtk = pNtk;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Existentially quantifies one variable.]
 
   Description []
@@ -113,6 +146,7 @@ Abc_Ntk_t * Abc_NtkTransRel( Abc_Ntk_t * pNtk, int fInputs, int fVerbose )
     Abc_Ntk_t * pNtkNew;
     Abc_Obj_t * pObj, * pMiter;
     int i, nLatches;
+    int fSynthesis = 1;
 
     assert( Abc_NtkIsStrash(pNtk) );
     assert( Abc_NtkLatchNum(pNtk) );
@@ -136,7 +170,10 @@ Abc_Ntk_t * Abc_NtkTransRel( Abc_Ntk_t * pNtk, int fInputs, int fVerbose )
     // create PI variables
     Abc_NtkForEachPi( pNtk, pObj, i )
         Abc_NtkDupObj( pNtkNew, pObj, 1 );
+    // create the PO
+    Abc_NtkCreatePo( pNtkNew );
     // restrash the nodes (assuming a topological order of the old network)
+    Abc_AigConst1(pNtk)->pCopy = Abc_AigConst1(pNtkNew);
     Abc_NtkForEachNode( pNtk, pObj, i )
         pObj->pCopy = Abc_AigAnd( pNtkNew->pManFunc, Abc_ObjChild0Copy(pObj), Abc_ObjChild1Copy(pObj) );
     // create the function of the primary output
@@ -150,7 +187,7 @@ Abc_Ntk_t * Abc_NtkTransRel( Abc_Ntk_t * pNtk, int fInputs, int fVerbose )
     pMiter = Abc_AigMiter( pNtkNew->pManFunc, vPairs );
     Vec_PtrFree( vPairs );
     // add the primary output
-    Abc_ObjAddFanin( Abc_NtkCreatePo(pNtkNew), Abc_ObjNot(pMiter) );
+    Abc_ObjAddFanin( Abc_NtkPo(pNtkNew,0), Abc_ObjNot(pMiter) );
     Abc_ObjAssignName( Abc_NtkPo(pNtkNew,0), "rel", NULL );
 
     // quantify inputs
@@ -158,7 +195,20 @@ Abc_Ntk_t * Abc_NtkTransRel( Abc_Ntk_t * pNtk, int fInputs, int fVerbose )
     {
         assert( Abc_NtkPiNum(pNtkNew) == Abc_NtkPiNum(pNtk) + 2*nLatches );
         for ( i = Abc_NtkPiNum(pNtkNew) - 1; i >= 2*nLatches; i-- )
+//        for ( i = 2*nLatches; i < Abc_NtkPiNum(pNtkNew); i++ )
+        {
             Abc_NtkQuantify( pNtkNew, i, fVerbose );
+//            if ( fSynthesis && (i % 3 == 2) )
+            if ( fSynthesis  )
+            {
+                Abc_NtkCleanData( pNtkNew );
+                Abc_AigCleanup( pNtkNew->pManFunc );
+                Abc_NtkSynthesize( &pNtkNew, 1 );
+            }
+//            printf( "Var = %3d. Nodes = %6d. ", Abc_NtkPiNum(pNtkNew) - 1 - i, Abc_NtkNodeNum(pNtkNew) );
+//            printf( "Var = %3d. Nodes = %6d. ", i - 2*nLatches, Abc_NtkNodeNum(pNtkNew) );
+        }
+//        printf( "\n" );
         Abc_NtkCleanData( pNtkNew );
         Abc_AigCleanup( pNtkNew->pManFunc );
         for ( i = Abc_NtkPiNum(pNtkNew) - 1; i >= 2*nLatches; i-- )
@@ -169,7 +219,7 @@ Abc_Ntk_t * Abc_NtkTransRel( Abc_Ntk_t * pNtk, int fInputs, int fVerbose )
         }
     }
 
-    // make sure that everything is okay
+    // check consistency of the network
     if ( !Abc_NtkCheck( pNtkNew ) )
     {
         printf( "Abc_NtkTransRel: The network check has failed.\n" );
@@ -263,6 +313,7 @@ Abc_Ntk_t * Abc_NtkReachability( Abc_Ntk_t * pNtkRel, int nIters, int fVerbose )
     int clk, i, v, nVars, nNodesOld, nNodesNew, nNodesPrev;
     int fFixedPoint = 0;
     int fSynthesis  = 1;
+    int fMoreEffort = 1;
 
     assert( Abc_NtkIsStrash(pNtkRel) );
     assert( Abc_NtkLatchNum(pNtkRel) == 0 );
@@ -273,8 +324,8 @@ Abc_Ntk_t * Abc_NtkReachability( Abc_Ntk_t * pNtkRel, int nIters, int fVerbose )
     pNtkReached = Abc_NtkDup( pNtkFront );
 //Abc_NtkShow( pNtkReached, 0, 0, 0 );
 
-    if ( fVerbose )
-        printf( "Transition relation = %6d.\n", Abc_NtkNodeNum(pNtkRel) );
+//    if ( fVerbose )
+//        printf( "Transition relation = %6d.\n", Abc_NtkNodeNum(pNtkRel) );
 
     // perform iterations of reachability analysis
     nNodesPrev = Abc_NtkNodeNum(pNtkFront);
@@ -293,25 +344,13 @@ Abc_Ntk_t * Abc_NtkReachability( Abc_Ntk_t * pNtkRel, int nIters, int fVerbose )
             {
                 Abc_NtkCleanData( pNtkNext );
                 Abc_AigCleanup( pNtkNext->pManFunc );
-
-                Abc_NtkRewrite( pNtkNext, 0, 0, 0, 0, 0 );
-                pNtkNext = Abc_NtkBalance( pNtkTemp = pNtkNext, 0, 0, 0 );          
-                Abc_NtkDelete( pNtkTemp );
+                Abc_NtkSynthesize( &pNtkNext, fMoreEffort );
             }
         }
         Abc_NtkCleanData( pNtkNext );
         Abc_AigCleanup( pNtkNext->pManFunc );
         if ( fSynthesis )
-        {
-            Abc_NtkRewrite( pNtkNext, 0, 0, 0, 0, 0 );
-            pNtkNext = Abc_NtkBalance( pNtkTemp = pNtkNext, 0, 0, 0 );          
-            Abc_NtkDelete( pNtkTemp );
-
-            Abc_NtkRewrite( pNtkNext, 0, 0, 0, 0, 0 );
-            Abc_NtkRefactor( pNtkReached, 10, 16, 0, 0, 0, 0 );
-            pNtkNext = Abc_NtkBalance( pNtkTemp = pNtkNext, 0, 0, 0 );          
-            Abc_NtkDelete( pNtkTemp );
-        }
+            Abc_NtkSynthesize( &pNtkNext, 1 );
         // map the next states into the current states
         pNtkNext = Abc_NtkSwapVariables( pNtkTemp = pNtkNext );
         Abc_NtkDelete( pNtkTemp );
@@ -333,20 +372,15 @@ Abc_Ntk_t * Abc_NtkReachability( Abc_Ntk_t * pNtkRel, int nIters, int fVerbose )
         nNodesOld = Abc_NtkNodeNum(pNtkFront);
         if ( fSynthesis )
         {
-            Abc_NtkRewrite( pNtkFront, 0, 0, 0, 0, 0 );
-            pNtkFront = Abc_NtkBalance( pNtkTemp = pNtkFront, 0, 0, 0 );          
-            Abc_NtkDelete( pNtkTemp );
-
-            Abc_NtkRewrite( pNtkReached, 0, 0, 0, 0, 0 );
-            pNtkReached = Abc_NtkBalance( pNtkTemp = pNtkReached, 0, 0, 0 );          
-            Abc_NtkDelete( pNtkTemp );
+            Abc_NtkSynthesize( &pNtkFront, fMoreEffort );
+            Abc_NtkSynthesize( &pNtkReached, fMoreEffort );
         }
         nNodesNew = Abc_NtkNodeNum(pNtkFront);
         // print statistics
         if ( fVerbose )
         {
-            printf( "I = %3d : Reached = %6d  Front = %6d  FrontM = %6d  %6.2f %%   ", 
-                i + 1, Abc_NtkNodeNum(pNtkReached), nNodesOld, nNodesNew, 100.0*(nNodesNew-nNodesPrev)/nNodesNew );
+            printf( "I = %3d : Reach = %6d  Fr = %6d  FrM = %6d  %7.2f %%   ", 
+                i + 1, Abc_NtkNodeNum(pNtkReached), nNodesOld, nNodesNew, 100.0*(nNodesNew-nNodesPrev)/nNodesPrev );
             PRT( "T", clock() - clk );
         }
         nNodesPrev = Abc_NtkNodeNum(pNtkFront);
@@ -354,13 +388,6 @@ Abc_Ntk_t * Abc_NtkReachability( Abc_Ntk_t * pNtkRel, int nIters, int fVerbose )
     if ( !fFixedPoint )
         fprintf( stdout, "Reachability analysis stopped after %d iterations.\n", nIters );
 
-    // report the stats
-    if ( fVerbose )
-    {
-//        nMints = 1;
-//        fprintf( stdout, "The estimated number of minterms in the reachable state set = %d. (%6.2f %%)\n", nMints, 100.0*nMints/(1<<Abc_NtkLatchNum(pNtk)) );
-    }
-
     // complement the output to represent the set of unreachable states
     Abc_ObjXorFaninC( Abc_NtkPo(pNtkReached,0), 0 );
 
@@ -372,7 +399,7 @@ Abc_Ntk_t * Abc_NtkReachability( Abc_Ntk_t * pNtkRel, int nIters, int fVerbose )
         Abc_NtkDeleteObj( pObj );
     }
 
-    // make sure that everything is okay
+    // check consistency of the network
     if ( !Abc_NtkCheck( pNtkReached ) )
     {
         printf( "Abc_NtkReachability: The network check has failed.\n" );
diff --git a/src/base/abci/abcStrash.c b/src/base/abci/abcStrash.c
index 88ef009b..45fc9089 100644
--- a/src/base/abci/abcStrash.c
+++ b/src/base/abci/abcStrash.c
@@ -105,7 +105,7 @@ Abc_Ntk_t * Abc_NtkStrash( Abc_Ntk_t * pNtk, bool fAllNodes, bool fCleanup )
     if ( Abc_NtkIsStrash(pNtk) )
         return Abc_NtkRestrash( pNtk, fCleanup );
     // convert the node representation in the logic network to the AIG form
-    if ( !Abc_NtkLogicToAig(pNtk) )
+    if ( !Abc_NtkToAig(pNtk) )
     {
         printf( "Converting to AIGs has failed.\n" );
         return NULL;
@@ -156,7 +156,7 @@ int Abc_NtkAppend( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fAddPos )
     // the first network should be an AIG
     assert( Abc_NtkIsStrash(pNtk1) );
     assert( Abc_NtkIsLogic(pNtk2) || Abc_NtkIsStrash(pNtk2) ); 
-    if ( Abc_NtkIsLogic(pNtk2) && !Abc_NtkLogicToAig(pNtk2) )
+    if ( Abc_NtkIsLogic(pNtk2) && !Abc_NtkToAig(pNtk2) )
     {
         printf( "Converting to AIGs has failed.\n" );
         return 0;
diff --git a/src/base/abci/abcSweep.c b/src/base/abci/abcSweep.c
index 1b63b23c..4791c859 100644
--- a/src/base/abci/abcSweep.c
+++ b/src/base/abci/abcSweep.c
@@ -536,7 +536,7 @@ int Abc_NtkSweep( Abc_Ntk_t * pNtk, int fVerbose )
     int i, nNodesOld;
     assert( Abc_NtkIsLogic(pNtk) ); 
     // convert network to BDD representation
-    if ( !Abc_NtkLogicToBdd(pNtk) )
+    if ( !Abc_NtkToBdd(pNtk) )
     {
         fprintf( stdout, "Converting to BDD has failed.\n" );
         return 1;