Version abc80403

28 files changed, 782 insertions, 607 deletions

diff --git a/abc.dsp b/abc.dsp
index 009d7847..f6771b7f 100644
--- a/abc.dsp
+++ b/abc.dsp
@@ -2946,6 +2946,10 @@ SOURCE=.\src\aig\aig\aigDfs.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\aig\aig\aigDup.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\aig\aig\aigFanout.c
 # End Source File
 # Begin Source File
diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h
index 38fd5190..18061a9c 100644
--- a/src/aig/aig/aig.h
+++ b/src/aig/aig/aig.h
@@ -445,14 +445,13 @@ extern Aig_ManCut_t *  Aig_ComputeCuts( Aig_Man_t * pAig, int nCutsMax, int nLea
 extern void            Aig_ManCutStop( Aig_ManCut_t * p );
 /*=== aigDfs.c ==========================================================*/
 extern int             Aig_ManVerifyTopoOrder( Aig_Man_t * p );
-extern Vec_Ptr_t *     Aig_ManDfs( Aig_Man_t * p );
+extern Vec_Ptr_t *     Aig_ManDfs( Aig_Man_t * p, int fNodesOnly );
 extern Vec_Vec_t *     Aig_ManLevelize( Aig_Man_t * p );
-extern Vec_Ptr_t *     Aig_ManDfsPio( Aig_Man_t * p );
 extern Vec_Ptr_t *     Aig_ManDfsNodes( Aig_Man_t * p, Aig_Obj_t ** ppNodes, int nNodes );
 extern Vec_Ptr_t *     Aig_ManDfsChoices( Aig_Man_t * p );
 extern Vec_Ptr_t *     Aig_ManDfsReverse( Aig_Man_t * p );
 extern int             Aig_ManLevelNum( Aig_Man_t * p );
-extern int             Aig_ManCountLevels( Aig_Man_t * p );
+extern int             Aig_ManChoiceLevel( Aig_Man_t * p );
 extern int             Aig_DagSize( Aig_Obj_t * pObj );
 extern int             Aig_SupportSize( Aig_Man_t * p, Aig_Obj_t * pObj );
 extern void            Aig_ConeUnmark_rec( Aig_Obj_t * pObj );
@@ -460,6 +459,13 @@ extern Aig_Obj_t *     Aig_Transfer( Aig_Man_t * pSour, Aig_Man_t * pDest, Aig_O
 extern Aig_Obj_t *     Aig_Compose( Aig_Man_t * p, Aig_Obj_t * pRoot, Aig_Obj_t * pFunc, int iVar );
 extern void            Aig_ObjCollectCut( Aig_Obj_t * pRoot, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vNodes );
 extern int             Aig_ObjCollectSuper( Aig_Obj_t * pObj, Vec_Ptr_t * vSuper );
+/*=== aigDup.c ==========================================================*/
+extern Aig_Man_t *     Aig_ManDupOrdered( Aig_Man_t * p );
+extern Aig_Man_t *     Aig_ManDupExor( Aig_Man_t * p );
+extern Aig_Man_t *     Aig_ManDupDfs( Aig_Man_t * p );
+extern Aig_Man_t *     Aig_ManDupDfsOrder( Aig_Man_t * p, Aig_Man_t * pOrder );
+extern Aig_Man_t *     Aig_ManDupLevelized( Aig_Man_t * p );
+extern Aig_Man_t *     Aig_ManDupWithoutPos( Aig_Man_t * p );
 /*=== aigFanout.c ==========================================================*/
 extern void            Aig_ObjAddFanout( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pFanout );
 extern void            Aig_ObjRemoveFanout( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pFanout );
@@ -472,10 +478,6 @@ extern void            Aig_ManHaigRecord( Aig_Man_t * p );
 /*=== aigMan.c ==========================================================*/
 extern Aig_Man_t *     Aig_ManStart( int nNodesMax );
 extern Aig_Man_t *     Aig_ManStartFrom( Aig_Man_t * p );
-extern Aig_Man_t *     Aig_ManDupExor( Aig_Man_t * p );
-extern Aig_Obj_t *     Aig_ManDup_rec( Aig_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t * pObj );
-extern Aig_Man_t *     Aig_ManDup( Aig_Man_t * p, int fOrdered );
-extern Aig_Man_t *     Aig_ManDupWithoutPos( Aig_Man_t * p );
 extern Aig_Man_t *     Aig_ManExtractMiter( Aig_Man_t * p, Aig_Obj_t * pNode1, Aig_Obj_t * pNode2 );
 extern void            Aig_ManStop( Aig_Man_t * p );
 extern int             Aig_ManCleanup( Aig_Man_t * p );
diff --git a/src/aig/aig/aigDfs.c b/src/aig/aig/aigDfs.c
index 95ed1c3a..9e43d7fd 100644
--- a/src/aig/aig/aigDfs.c
+++ b/src/aig/aig/aigDfs.c
@@ -43,7 +43,7 @@
 int Aig_ManVerifyTopoOrder( Aig_Man_t * p )
 {
     Aig_Obj_t * pObj, * pNext;
-    int i, iBox, iTerm1, nTerms;
+    int i, k, iBox, iTerm1, nTerms;
     Aig_ManSetPioNumbers( p );
     Aig_ManIncrementTravId( p );
     Aig_ManForEachObj( p, pObj, i )
@@ -63,7 +63,7 @@ int Aig_ManVerifyTopoOrder( Aig_Man_t * p )
                 return 0;
             }
         }
-        else if ( Aig_ObjIsPo(pObj) )
+        else if ( Aig_ObjIsPo(pObj) || Aig_ObjIsBuf(pObj) )
         {
             pNext = Aig_ObjFanin0(pObj);
             if ( !Aig_ObjIsTravIdCurrent(p,pNext) )
@@ -81,9 +81,9 @@ int Aig_ManVerifyTopoOrder( Aig_Man_t * p )
                 {
                     iTerm1 = Tim_ManBoxInputFirst( p->pManTime, iBox );
                     nTerms = Tim_ManBoxInputNum( p->pManTime, iBox );
-                    for ( i = 0; i < nTerms; i++ )
+                    for ( k = 0; k < nTerms; k++ )
                     {
-                        pNext = Aig_ManPo( p, iTerm1 + i );
+                        pNext = Aig_ManPo( p, iTerm1 + k );
                         assert( Tim_ManBoxForCo( p->pManTime, Aig_ObjPioNum(pNext) ) == iBox ); 
                         if ( !Aig_ObjIsTravIdCurrent(p,pNext) )
                         {
@@ -94,7 +94,7 @@ int Aig_ManVerifyTopoOrder( Aig_Man_t * p )
                 }
             }
         }
-        else
+        else if ( !Aig_ObjIsConst1(pObj) )
             assert( 0 );
         Aig_ObjSetTravIdCurrent( p, pObj );
     }
@@ -120,49 +120,53 @@ void Aig_ManDfs_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vNodes )
     assert( !Aig_IsComplement(pObj) );
     if ( Aig_ObjIsTravIdCurrent(p, pObj) )
         return;
-//    if ( Aig_ObjIsPi(pObj) )
-//        return;
-//    assert( Aig_ObjIsNode(pObj) || Aig_ObjIsBuf(pObj) );
     Aig_ObjSetTravIdCurrent(p, pObj);
+    if ( p->pEquivs && p->pEquivs[pObj->Id] )
+        Aig_ManDfs_rec( p, p->pEquivs[pObj->Id], vNodes );
     Aig_ManDfs_rec( p, Aig_ObjFanin0(pObj), vNodes );
     Aig_ManDfs_rec( p, Aig_ObjFanin1(pObj), vNodes );
-//    assert( !Aig_ObjIsTravIdCurrent(p, pObj) ); // loop detection
-//    Aig_ObjSetTravIdCurrent(p, pObj);
     Vec_PtrPush( vNodes, pObj );
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Collects internal nodes in the DFS order.]
+  Synopsis    [Collects objects of the AIG in the DFS order.]
 
-  Description []
+  Description [Works with choice nodes.]
                
   SideEffects []
 
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Ptr_t * Aig_ManDfs( Aig_Man_t * p )
+Vec_Ptr_t * Aig_ManDfs( Aig_Man_t * p, int fNodesOnly )
 {
     Vec_Ptr_t * vNodes;
     Aig_Obj_t * pObj;
     int i;
     Aig_ManIncrementTravId( p );
-    // mark constant and PIs
     Aig_ObjSetTravIdCurrent( p, Aig_ManConst1(p) );
-    Aig_ManForEachPi( p, pObj, i )
-        Aig_ObjSetTravIdCurrent( p, pObj );
-    // go through the nodes
-    vNodes = Vec_PtrAlloc( Aig_ManNodeNum(p) );
-    Aig_ManForEachObj( p, pObj, i )
-        if ( Aig_ObjIsNode(pObj) || Aig_ObjIsBuf(pObj) )
-            Aig_ManDfs_rec( p, pObj, vNodes );
+    // start the array of nodes
+    vNodes = Vec_PtrAlloc( Aig_ManObjNumMax(p) );
+    // mark PIs if they should not be collected
+    if ( fNodesOnly )
+        Aig_ManForEachPi( p, pObj, i )
+            Aig_ObjSetTravIdCurrent( p, pObj );
+    else
+        Vec_PtrPush( vNodes, Aig_ManConst1(p) );
+    // collect nodes reachable in the DFS order
+    Aig_ManForEachPo( p, pObj, i )
+        Aig_ManDfs_rec( p, fNodesOnly? Aig_ObjFanin0(pObj): pObj, vNodes );
+    if ( fNodesOnly )
+        assert( Vec_PtrSize(vNodes) == Aig_ManNodeNum(p) );
+    else
+        assert( Vec_PtrSize(vNodes) == Aig_ManObjNum(p) );
     return vNodes;
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Levelizes the nodes
+  Synopsis    [Levelizes the nodes.]
 
   Description []
                
@@ -178,7 +182,7 @@ Vec_Vec_t * Aig_ManLevelize( Aig_Man_t * p )
     int nLevels, i;
     nLevels = Aig_ManLevelNum( p );
     vLevels = Vec_VecStart( nLevels + 1 );
-    Aig_ManForEachNode( p, pObj, i )
+    Aig_ManForEachObj( p, pObj, i )
     {
         assert( (int)pObj->Level <= nLevels );
         Vec_VecPush( vLevels, pObj->Level, pObj );
@@ -188,29 +192,6 @@ Vec_Vec_t * Aig_ManLevelize( Aig_Man_t * p )
 
 /**Function*************************************************************
 
-  Synopsis    [Collects internal nodes in the DFS order.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Vec_Ptr_t * Aig_ManDfsPio( Aig_Man_t * p )
-{
-    Vec_Ptr_t * vNodes;
-    Aig_Obj_t * pObj;
-    int i;
-    Aig_ManIncrementTravId( p );
-    vNodes = Vec_PtrAlloc( Aig_ManObjNumMax(p) );
-    Aig_ManForEachPo( p, pObj, i )
-        Aig_ManDfs_rec( p, pObj, vNodes );
-    return vNodes;
-}
-
-/**Function*************************************************************
-
   Synopsis    [Collects internal nodes and PIs in the DFS order.]
 
   Description []
@@ -368,9 +349,11 @@ int Aig_ManLevelNum( Aig_Man_t * p )
     return LevelsMax;
 }
 
+//#if 0
+
 /**Function*************************************************************
 
-  Synopsis    [Computes the max number of levels in the manager.]
+  Synopsis    [Computes levels for AIG with choices and white boxes.]
 
   Description []
                
@@ -379,31 +362,100 @@ int Aig_ManLevelNum( Aig_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-int Aig_ManCountLevels( Aig_Man_t * p )
+void Aig_ManChoiceLevel_rec( Aig_Man_t * p, Aig_Obj_t * pObj )
 {
-    Vec_Ptr_t * vNodes;
-    Aig_Obj_t * pObj;
-    int i, LevelsMax, Level0, Level1;
-    // initialize the levels
-    Aig_ManConst1(p)->iData = 0;
-    Aig_ManForEachPi( p, pObj, i )
-        pObj->iData = 0;
-    // compute levels in a DFS order
-    vNodes = Aig_ManDfs( p );
-    Vec_PtrForEachEntry( vNodes, pObj, i )
+    Aig_Obj_t * pNext;
+    int i, iBox, iTerm1, nTerms, LevelMax = 0;
+    if ( Aig_ObjIsTravIdCurrent( p, pObj ) )
+        return;
+    Aig_ObjSetTravIdCurrent( p, pObj );
+    if ( Aig_ObjIsPi(pObj) )
     {
-        Level0 = Aig_ObjFanin0(pObj)->iData;
-        Level1 = Aig_ObjFanin1(pObj)->iData;
-        pObj->iData = 1 + Aig_ObjIsExor(pObj) + AIG_MAX(Level0, Level1);
+        if ( p->pManTime )
+        {
+            iBox = Tim_ManBoxForCi( p->pManTime, Aig_ObjPioNum(pObj) );
+            if ( iBox >= 0 ) // this is not a true PI
+            {
+                iTerm1 = Tim_ManBoxInputFirst( p->pManTime, iBox );
+                nTerms = Tim_ManBoxInputNum( p->pManTime, iBox );
+                for ( i = 0; i < nTerms; i++ )
+                {
+                    pNext = Aig_ManPo(p, iTerm1 + i);
+                    Aig_ManChoiceLevel_rec( p, pNext );
+                    if ( LevelMax < Aig_ObjLevel(pNext) )
+                        LevelMax = Aig_ObjLevel(pNext);
+                }
+                LevelMax++;
+            }
+        }
+//        printf( "%d ", pObj->Level );
     }
-    Vec_PtrFree( vNodes );
-    // get levels of the POs
-    LevelsMax = 0;
+    else if ( Aig_ObjIsPo(pObj) )
+    {
+        pNext = Aig_ObjFanin0(pObj);
+        Aig_ManChoiceLevel_rec( p, pNext );
+        if ( LevelMax < Aig_ObjLevel(pNext) )
+            LevelMax = Aig_ObjLevel(pNext);
+    }
+    else if ( Aig_ObjIsNode(pObj) )
+    { 
+        // get the maximum level of the two fanins
+        pNext = Aig_ObjFanin0(pObj);
+        Aig_ManChoiceLevel_rec( p, pNext );
+        if ( LevelMax < Aig_ObjLevel(pNext) )
+            LevelMax = Aig_ObjLevel(pNext);
+        pNext = Aig_ObjFanin1(pObj);
+        Aig_ManChoiceLevel_rec( p, pNext );
+        if ( LevelMax < Aig_ObjLevel(pNext) )
+            LevelMax = Aig_ObjLevel(pNext);
+        LevelMax++;
+
+        // get the level of the nodes in the choice node
+        if ( p->pEquivs && (pNext = p->pEquivs[pObj->Id]) )
+        {
+            Aig_ManChoiceLevel_rec( p, pNext );
+            if ( LevelMax < Aig_ObjLevel(pNext) )
+                LevelMax = Aig_ObjLevel(pNext);
+        }
+    }
+    else
+        assert( 0 );
+    Aig_ObjSetLevel( pObj, LevelMax );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes levels for AIG with choices and white boxes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Aig_ManChoiceLevel( Aig_Man_t * p )
+{
+    Aig_Obj_t * pObj;
+    int i, LevelMax = 0;
+    Aig_ManForEachObj( p, pObj, i )
+        Aig_ObjSetLevel( pObj, 0 );
+    Aig_ManSetPioNumbers( p );
+    Aig_ManIncrementTravId( p );
     Aig_ManForEachPo( p, pObj, i )
-        LevelsMax = AIG_MAX( LevelsMax, Aig_ObjFanin0(pObj)->iData );
-    return LevelsMax;
+    {
+        Aig_ManChoiceLevel_rec( p, pObj );
+        if ( LevelMax < Aig_ObjLevel(pObj) )
+            LevelMax = Aig_ObjLevel(pObj);
+    }
+    Aig_ManCleanPioNumbers( p );
+    Aig_ManForEachNode( p, pObj, i )
+        assert( Aig_ObjLevel(pObj) > 0 );
+    return LevelMax;
 }
 
+//#endif
+
 /**Function*************************************************************
 
   Synopsis    [Counts the number of AIG nodes rooted at this cone.]
diff --git a/src/aig/aig/aigDup.c b/src/aig/aig/aigDup.c
new file mode 100644
index 00000000..043a95a8
--- /dev/null
+++ b/src/aig/aig/aigDup.c
@@ -0,0 +1,489 @@
+/**CFile****************************************************************
+
+  FileName    [aigDup.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [AIG package.]
+
+  Synopsis    [AIG duplication (re-strashing).]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - April 28, 2007.]
+
+  Revision    [$Id: aigDup.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "aig.h"
+#include "tim.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Duplicates the AIG manager.]
+
+  Description [Assumes topological ordering of the nodes.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Aig_ManDupOrdered( Aig_Man_t * p )
+{
+    Aig_Man_t * pNew;
+    Aig_Obj_t * pObj, * pObjNew;
+    int i, nNodes;
+    // create the new manager
+    pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
+    pNew->pName = Aig_UtilStrsav( p->pName );
+    pNew->pSpec = Aig_UtilStrsav( p->pSpec );
+    pNew->nRegs = p->nRegs;
+    pNew->nAsserts = p->nAsserts;
+    if ( p->vFlopNums )
+        pNew->vFlopNums = Vec_IntDup( p->vFlopNums );
+    // create the PIs
+    Aig_ManCleanData( p );
+    // duplicate internal nodes
+    Aig_ManForEachObj( p, pObj, i )
+    {
+        if ( Aig_ObjIsBuf(pObj) )
+        {
+            pObjNew = Aig_ObjChild0Copy(pObj);
+        }
+        else if ( Aig_ObjIsNode(pObj) )
+        {
+            pObjNew = Aig_Oper( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj), Aig_ObjType(pObj) );
+        }
+        else if ( Aig_ObjIsPi(pObj) )
+        {
+            pObjNew = Aig_ObjCreatePi( pNew );
+            pObjNew->Level = pObj->Level;
+        }
+        else if ( Aig_ObjIsPo(pObj) )
+        {
+            pObjNew = Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
+        }
+        else if ( Aig_ObjIsConst1(pObj) )
+        {
+            pObjNew = Aig_ManConst1(pNew);
+        }
+        else
+            assert( 0 );
+        Aig_Regular(pObjNew)->pHaig = pObj->pHaig;
+        pObj->pData = pObjNew;
+    }
+    assert( Aig_ManBufNum(p) != 0 || Aig_ManNodeNum(p) == Aig_ManNodeNum(pNew) );
+    if ( (nNodes = Aig_ManCleanup( pNew )) )
+        printf( "Aig_ManDupOrdered(): Cleanup after AIG duplication removed %d nodes.\n", nNodes );
+    // duplicate the timing manager
+    if ( p->pManTime )
+        pNew->pManTime = Tim_ManDup( p->pManTime, 0 );
+    // check the resulting network
+    if ( !Aig_ManCheck(pNew) )
+        printf( "Aig_ManDupOrdered(): The check has failed.\n" );
+    return pNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Duplicates the AIG manager to have EXOR gates.]
+
+  Description [Assumes topological ordering of the nodes.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Aig_ManDupExor( Aig_Man_t * p )
+{
+    Aig_Man_t * pNew;
+    Aig_Obj_t * pObj, * pObjNew;
+    int i;
+    // create the new manager
+    pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
+    pNew->fCatchExor = 1;
+    pNew->pName = Aig_UtilStrsav( p->pName );
+    pNew->pSpec = Aig_UtilStrsav( p->pSpec );
+    pNew->nRegs = p->nRegs;
+    pNew->nAsserts = p->nAsserts;
+    if ( p->vFlopNums )
+        pNew->vFlopNums = Vec_IntDup( p->vFlopNums );
+    // create the PIs
+    Aig_ManCleanData( p );
+    // duplicate internal nodes
+    Aig_ManForEachObj( p, pObj, i )
+    {
+        if ( Aig_ObjIsBuf(pObj) )
+        {
+            pObjNew = Aig_ObjChild0Copy(pObj);
+        }
+        else if ( Aig_ObjIsNode(pObj) )
+        {
+            pObjNew = Aig_Oper( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj), Aig_ObjType(pObj) );
+        }
+        else if ( Aig_ObjIsPi(pObj) )
+        {
+            pObjNew = Aig_ObjCreatePi( pNew );
+            pObjNew->Level = pObj->Level;
+        }
+        else if ( Aig_ObjIsPo(pObj) )
+        {
+            pObjNew = Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
+        }
+        else if ( Aig_ObjIsConst1(pObj) )
+        {
+            pObjNew = Aig_ManConst1(pNew);
+        }
+        else
+            assert( 0 );
+        Aig_Regular(pObjNew)->pHaig = pObj->pHaig;
+        pObj->pData = pObjNew;
+    }
+    Aig_ManCleanup( pNew );
+    // duplicate the timing manager
+    if ( p->pManTime )
+        pNew->pManTime = Tim_ManDup( p->pManTime, 0 );
+    // check the resulting network
+    if ( !Aig_ManCheck(pNew) )
+        printf( "Aig_ManDupExor(): The check has failed.\n" );
+    return pNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Duplicates the AIG manager recursively.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Obj_t * Aig_ManDupDfs_rec( Aig_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t * pObj )
+{
+    Aig_Obj_t * pObjNew, * pEquivNew = NULL;
+    if ( pObj->pData )
+        return pObj->pData;
+    if ( p->pEquivs && p->pEquivs[pObj->Id] )
+        pEquivNew = Aig_ManDupDfs_rec( pNew, p, p->pEquivs[pObj->Id] );
+    Aig_ManDupDfs_rec( pNew, p, Aig_ObjFanin0(pObj) );
+    if ( Aig_ObjIsBuf(pObj) )
+        return pObj->pData = Aig_ObjChild0Copy(pObj);
+    Aig_ManDupDfs_rec( pNew, p, Aig_ObjFanin1(pObj) );
+    pObjNew = Aig_Oper( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj), Aig_ObjType(pObj) );
+    if ( pObj->pHaig )
+        Aig_Regular(pObjNew)->pHaig = pObj->pHaig;
+    if ( pEquivNew )
+    {
+        if ( pNew->pEquivs )
+            pNew->pEquivs[Aig_Regular(pObjNew)->Id] = Aig_Regular(pEquivNew);        
+        if ( pNew->pReprs )
+            pNew->pReprs[Aig_Regular(pEquivNew)->Id] = Aig_Regular(pObjNew);
+    }
+    return pObj->pData = pObjNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Duplicates the AIG manager.]
+
+  Description [This duplicator works for AIGs with choices.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Aig_ManDupDfs( Aig_Man_t * p )
+{
+    Aig_Man_t * pNew;
+    Aig_Obj_t * pObj, * pObjNew;
+    int i, nNodes;
+    // create the new manager
+    pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
+    pNew->pName = Aig_UtilStrsav( p->pName );
+    pNew->pSpec = Aig_UtilStrsav( p->pSpec );
+    pNew->nRegs = p->nRegs;
+    pNew->nAsserts = p->nAsserts;
+    if ( p->vFlopNums )
+        pNew->vFlopNums = Vec_IntDup( p->vFlopNums );
+    // duplicate representation of choice nodes
+    if ( p->pEquivs )
+    {
+        pNew->pEquivs = ALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p) );
+        memset( pNew->pEquivs, 0, sizeof(Aig_Obj_t *) * Aig_ManObjNumMax(p) );
+    }
+    if ( p->pReprs )
+    {
+        pNew->pReprs = ALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p) );
+        memset( pNew->pReprs, 0, sizeof(Aig_Obj_t *) * Aig_ManObjNumMax(p) );
+    }
+    // create the PIs
+    Aig_ManCleanData( p );
+    // duplicate internal nodes
+    Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
+    Aig_ManConst1(pNew)->pHaig = Aig_ManConst1(p)->pHaig;
+    Aig_ManForEachObj( p, pObj, i )
+    {
+        if ( Aig_ObjIsPi(pObj) )
+        {
+            pObjNew = Aig_ObjCreatePi( pNew );
+            pObjNew->Level = pObj->Level;
+            Aig_Regular(pObjNew)->pHaig = pObj->pHaig;
+            pObj->pData = pObjNew;
+        }
+        else if ( Aig_ObjIsPo(pObj) )
+        {
+            Aig_ManDupDfs_rec( pNew, p, Aig_ObjFanin0(pObj) );        
+//            assert( pObj->Level == ((Aig_Obj_t*)pObj->pData)->Level );
+            pObjNew = Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
+            Aig_Regular(pObjNew)->pHaig = pObj->pHaig;
+            pObj->pData = pObjNew;
+        }
+    }
+    assert( Aig_ManBufNum(p) != 0 || Aig_ManNodeNum(p) == Aig_ManNodeNum(pNew) );
+    if ( p->pEquivs == NULL && p->pReprs == NULL && (nNodes = Aig_ManCleanup( pNew )) )
+        printf( "Aig_ManDupDfs(): Cleanup after AIG duplication removed %d nodes.\n", nNodes );
+    // duplicate the timing manager
+    if ( p->pManTime )
+        pNew->pManTime = Tim_ManDup( p->pManTime, 0 );
+    // check the resulting network
+    if ( !Aig_ManCheck(pNew) )
+        printf( "Aig_ManDupDfs(): The check has failed.\n" );
+    return pNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Duplicates the AIG manager.]
+
+  Description [This duplicator works for AIGs with choices.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Aig_ManOrderPios( Aig_Man_t * p, Aig_Man_t * pOrder )
+{
+    Vec_Ptr_t * vPios;
+    Aig_Obj_t * pObj;
+    int i;
+    assert( Aig_ManPiNum(p) == Aig_ManPiNum(pOrder) );
+    assert( Aig_ManPoNum(p) == Aig_ManPoNum(pOrder) );
+    Aig_ManSetPioNumbers( pOrder );
+    vPios = Vec_PtrAlloc( Aig_ManPiNum(p) + Aig_ManPoNum(p) );
+    Aig_ManForEachObj( pOrder, pObj, i )
+    {
+        if ( Aig_ObjIsPi(pObj) )
+            Vec_PtrPush( vPios, Aig_ManPi(p, Aig_ObjPioNum(pObj)) );
+        else if ( Aig_ObjIsPo(pObj) )
+            Vec_PtrPush( vPios, Aig_ManPo(p, Aig_ObjPioNum(pObj)) );
+    }
+    Aig_ManCleanPioNumbers( pOrder );
+    return vPios;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Duplicates the AIG manager.]
+
+  Description [This duplicator works for AIGs with choices.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Aig_ManDupDfsOrder( Aig_Man_t * p, Aig_Man_t * pOrder )
+{
+    Vec_Ptr_t * vPios;
+    Aig_Man_t * pNew;
+    Aig_Obj_t * pObj, * pObjNew;
+    int i, nNodes;
+    // create the new manager
+    pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
+    pNew->pName = Aig_UtilStrsav( p->pName );
+    pNew->pSpec = Aig_UtilStrsav( p->pSpec );
+    pNew->nRegs = p->nRegs;
+    pNew->nAsserts = p->nAsserts;
+    if ( p->vFlopNums )
+        pNew->vFlopNums = Vec_IntDup( p->vFlopNums );
+    // duplicate representation of choice nodes
+    if ( p->pEquivs )
+    {
+        pNew->pEquivs = ALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p) );
+        memset( pNew->pEquivs, 0, sizeof(Aig_Obj_t *) * Aig_ManObjNumMax(p) );
+    }
+    if ( p->pReprs )
+    {
+        pNew->pReprs = ALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p) );
+        memset( pNew->pReprs, 0, sizeof(Aig_Obj_t *) * Aig_ManObjNumMax(p) );
+    }
+    // create the PIs
+    Aig_ManCleanData( p );
+    // duplicate internal nodes
+    Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
+    Aig_ManConst1(pNew)->pHaig = Aig_ManConst1(p)->pHaig;
+    vPios = Aig_ManOrderPios( p, pOrder );
+    Vec_PtrForEachEntry( vPios, pObj, i )
+    {
+        if ( Aig_ObjIsPi(pObj) )
+        {
+            pObjNew = Aig_ObjCreatePi( pNew );
+            pObjNew->Level = pObj->Level;
+            Aig_Regular(pObjNew)->pHaig = pObj->pHaig;
+            pObj->pData = pObjNew;
+        }
+        else if ( Aig_ObjIsPo(pObj) )
+        {
+            Aig_ManDupDfs_rec( pNew, p, Aig_ObjFanin0(pObj) );        
+//            assert( pObj->Level == ((Aig_Obj_t*)pObj->pData)->Level );
+            pObjNew = Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
+            Aig_Regular(pObjNew)->pHaig = pObj->pHaig;
+            pObj->pData = pObjNew;
+        }
+    }
+    Vec_PtrFree( vPios );
+    assert( Aig_ManBufNum(p) != 0 || Aig_ManNodeNum(p) == Aig_ManNodeNum(pNew) );
+    if ( p->pEquivs == NULL && p->pReprs == NULL && (nNodes = Aig_ManCleanup( pNew )) )
+        printf( "Aig_ManDupDfs(): Cleanup after AIG duplication removed %d nodes.\n", nNodes );
+    // duplicate the timing manager
+    if ( p->pManTime )
+        pNew->pManTime = Tim_ManDup( p->pManTime, 0 );
+    // check the resulting network
+    if ( !Aig_ManCheck(pNew) )
+        printf( "Aig_ManDupDfs(): The check has failed.\n" );
+    return pNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Duplicates the AIG manager.]
+
+  Description [This duplicator works for AIGs with choices.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Aig_ManDupLevelized( Aig_Man_t * p )
+{
+    Vec_Vec_t * vLevels;
+    Aig_Man_t * pNew;
+    Aig_Obj_t * pObj, * pObjNew;
+    int i, k;
+    // create the new manager
+    pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
+    pNew->pName = Aig_UtilStrsav( p->pName );
+    pNew->pSpec = Aig_UtilStrsav( p->pSpec );
+    pNew->nRegs = p->nRegs;
+    pNew->nAsserts = p->nAsserts;
+    if ( p->vFlopNums )
+        pNew->vFlopNums = Vec_IntDup( p->vFlopNums );
+    // duplicate representation of choice nodes
+    if ( p->pEquivs )
+    {
+        pNew->pEquivs = ALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p) );
+        memset( pNew->pEquivs, 0, sizeof(Aig_Obj_t *) * Aig_ManObjNumMax(p) );
+    }
+    if ( p->pReprs )
+    {
+        pNew->pReprs = ALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p) );
+        memset( pNew->pReprs, 0, sizeof(Aig_Obj_t *) * Aig_ManObjNumMax(p) );
+    }
+    // create the PIs
+    Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
+    Aig_ManConst1(pNew)->pHaig = Aig_ManConst1(p)->pHaig;
+    Aig_ManForEachPi( p, pObj, i )
+    {
+        pObjNew = Aig_ObjCreatePi( pNew );
+        pObjNew->pHaig = pObj->pHaig;
+        pObjNew->Level = pObj->Level;
+        pObj->pData = pObjNew;
+    }
+    // duplicate internal nodes
+    vLevels = Aig_ManLevelize( p );
+    Vec_VecForEachEntry( vLevels, pObj, i, k )
+    {
+        pObjNew = Aig_Oper( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj), Aig_ObjType(pObj) );
+        Aig_Regular(pObjNew)->pHaig = pObj->pHaig;
+        pObj->pData = pObjNew;
+    }
+    Vec_VecFree( vLevels );
+    // duplicate POs
+    Aig_ManForEachPo( p, pObj, i )
+    {
+        pObjNew = Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
+        pObjNew->pHaig = pObj->pHaig;
+        pObj->pData = pObjNew;
+    }
+    assert( Aig_ManBufNum(p) != 0 || Aig_ManNodeNum(p) == Aig_ManNodeNum(pNew) );
+//    if ( (nNodes = Aig_ManCleanup( pNew )) )
+//        printf( "Aig_ManDupLevelized(): Cleanup after AIG duplication removed %d nodes.\n", nNodes );
+    // duplicate the timing manager
+    if ( p->pManTime )
+        pNew->pManTime = Tim_ManDup( p->pManTime, 0 );
+    // check the resulting network
+    if ( !Aig_ManCheck(pNew) )
+        printf( "Aig_ManDupLevelized(): The check has failed.\n" );
+    return pNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Duplicates the AIG manager.]
+
+  Description [Assumes topological ordering of nodes.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Aig_ManDupWithoutPos( Aig_Man_t * p )
+{
+    Aig_Man_t * pNew;
+    Aig_Obj_t * pObj;
+    int i;
+    // create the new manager
+    pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
+    pNew->pName = Aig_UtilStrsav( p->pName );
+    pNew->pSpec = Aig_UtilStrsav( p->pSpec );
+    // create the PIs
+    Aig_ManCleanData( p );
+    Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
+    Aig_ManForEachPi( p, pObj, i )
+        pObj->pData = Aig_ObjCreatePi( pNew );
+    // duplicate internal nodes
+    Aig_ManForEachObj( p, pObj, i )
+    {
+        assert( !Aig_ObjIsBuf(pObj) );
+        if ( Aig_ObjIsNode(pObj) )
+            pObj->pData = Aig_Oper( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj), Aig_ObjType(pObj) );
+    }
+    assert( Aig_ManBufNum(p) != 0 || Aig_ManNodeNum(p) == Aig_ManNodeNum(pNew) );
+    return pNew;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/aig/aigHaig.c b/src/aig/aig/aigHaig.c
index dc083465..e465a07a 100644
--- a/src/aig/aig/aigHaig.c
+++ b/src/aig/aig/aigHaig.c
@@ -250,7 +250,7 @@ void Aig_ManHaigRecord( Aig_Man_t * p )
     Aig_Obj_t * pObj;
     int i;
     // start the HAIG
-    p->pManHaig = Aig_ManDup( p, 1 );
+    p->pManHaig = Aig_ManDupOrdered( p );
     // set the pointers to the HAIG nodes
     Aig_ManForEachObj( p, pObj, i )
         pObj->pHaig = pObj->pData;
diff --git a/src/aig/aig/aigMan.c b/src/aig/aig/aigMan.c
index 3dddc687..0d5dfca9 100644
--- a/src/aig/aig/aigMan.c
+++ b/src/aig/aig/aigMan.c
@@ -105,74 +105,6 @@ Aig_Man_t * Aig_ManStartFrom( Aig_Man_t * p )
 
 /**Function*************************************************************
 
-  Synopsis    [Duplicates the AIG manager to have EXOR gates.]
-
-  Description [Assumes topological ordering of the nodes.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Aig_Man_t * Aig_ManDupExor( Aig_Man_t * p )
-{
-    Aig_Man_t * pNew;
-    Aig_Obj_t * pObj, * pObjNew;
-    int i;
-    // create the new manager
-    pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
-    pNew->fCatchExor = 1;
-    pNew->pName = Aig_UtilStrsav( p->pName );
-    pNew->pSpec = Aig_UtilStrsav( p->pSpec );
-    pNew->nRegs = p->nRegs;
-    pNew->nAsserts = p->nAsserts;
-    if ( p->vFlopNums )
-        pNew->vFlopNums = Vec_IntDup( p->vFlopNums );
-    // create the PIs
-    Aig_ManCleanData( p );
-    // duplicate internal nodes
-    Aig_ManForEachObj( p, pObj, i )
-    {
-        if ( Aig_ObjIsBuf(pObj) )
-        {
-            pObjNew = Aig_ObjChild0Copy(pObj);
-        }
-        else if ( Aig_ObjIsNode(pObj) )
-        {
-            pObjNew = Aig_Oper( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj), Aig_ObjType(pObj) );
-        }
-        else if ( Aig_ObjIsPi(pObj) )
-        {
-            pObjNew = Aig_ObjCreatePi( pNew );
-            pObjNew->Level = pObj->Level;
-        }
-        else if ( Aig_ObjIsPo(pObj) )
-        {
-            pObjNew = Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
-        }
-        else if ( Aig_ObjIsConst1(pObj) )
-        {
-            pObjNew = Aig_ManConst1(pNew);
-        }
-        else
-            assert( 0 );
-        Aig_Regular(pObjNew)->pHaig = pObj->pHaig;
-        pObj->pData = pObjNew;
-    }
-    Aig_ManCleanup( pNew );
-    // duplicate the timing manager
-    if ( p->pManTime )
-        pNew->pManTime = Tim_ManDup( p->pManTime, 0 );
-    // check the resulting network
-    if ( !Aig_ManCheck(pNew) )
-        printf( "Aig_ManDup(): The check has failed.\n" );
-    return pNew;
-}
-
-//#if 0
-
-/**Function*************************************************************
-
   Synopsis    [Duplicates the AIG manager recursively.]
 
   Description []
@@ -198,311 +130,6 @@ Aig_Obj_t * Aig_ManDup_rec( Aig_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t * pObj )
 
 /**Function*************************************************************
 
-  Synopsis    [Duplicates the AIG manager.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Aig_Man_t * Aig_ManDup( Aig_Man_t * p, int fOrdered )
-{
-    Aig_Man_t * pNew;
-    Aig_Obj_t * pObj, * pObjNew;
-    int i;
-    // create the new manager
-    pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
-    pNew->pName = Aig_UtilStrsav( p->pName );
-    pNew->pSpec = Aig_UtilStrsav( p->pSpec );
-    pNew->nRegs = p->nRegs;
-    pNew->nAsserts = p->nAsserts;
-    if ( p->vFlopNums )
-        pNew->vFlopNums = Vec_IntDup( p->vFlopNums );
-    // create the PIs
-    Aig_ManCleanData( p );
-    // duplicate internal nodes
-    if ( fOrdered )
-    {
-        Aig_ManForEachObj( p, pObj, i )
-        {
-            if ( Aig_ObjIsBuf(pObj) )
-            {
-                pObjNew = Aig_ObjChild0Copy(pObj);
-            }
-            else if ( Aig_ObjIsNode(pObj) )
-            {
-                pObjNew = Aig_Oper( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj), Aig_ObjType(pObj) );
-            }
-            else if ( Aig_ObjIsPi(pObj) )
-            {
-                pObjNew = Aig_ObjCreatePi( pNew );
-                pObjNew->Level = pObj->Level;
-            }
-            else if ( Aig_ObjIsPo(pObj) )
-            {
-                pObjNew = Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
-            }
-            else if ( Aig_ObjIsConst1(pObj) )
-            {
-                pObjNew = Aig_ManConst1(pNew);
-            }
-            else
-                assert( 0 );
-            Aig_Regular(pObjNew)->pHaig = pObj->pHaig;
-            pObj->pData = pObjNew;
-        }
-    }
-    else
-    {
-/*
-        Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
-        Aig_ManConst1(pNew)->pHaig = Aig_ManConst1(p)->pHaig;
-        Aig_ManForEachObj( p, pObj, i )
-        {
-            if ( Aig_ObjIsPi(pObj) )
-            {
-                pObjNew = Aig_ObjCreatePi( pNew );
-                pObjNew->Level = pObj->Level;
-                Aig_Regular(pObjNew)->pHaig = pObj->pHaig;
-                pObj->pData = pObjNew;
-            }
-            else if ( Aig_ObjIsPo(pObj) )
-            {
-                Aig_ManDup_rec( pNew, p, Aig_ObjFanin0(pObj) );        
-//                assert( pObj->Level == ((Aig_Obj_t*)pObj->pData)->Level );
-                pObjNew = Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
-                Aig_Regular(pObjNew)->pHaig = pObj->pHaig;
-                pObj->pData = pObjNew;
-            }
-        }
-*/
-
-        Vec_Vec_t * vLevels;
-        int k;
-
-        Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
-        Aig_ManConst1(pNew)->pHaig = Aig_ManConst1(p)->pHaig;
-        Aig_ManForEachPi( p, pObj, i )
-        {
-            pObjNew = Aig_ObjCreatePi( pNew );
-            pObjNew->pHaig = pObj->pHaig;
-            pObjNew->Level = pObj->Level;
-            pObj->pData = pObjNew;
-        }
-
-        vLevels = Aig_ManLevelize( p );
-        Vec_VecForEachEntry( vLevels, pObj, i, k )
-        {
-            pObjNew = Aig_Oper( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj), Aig_ObjType(pObj) );
-            Aig_Regular(pObjNew)->pHaig = pObj->pHaig;
-            pObj->pData = pObjNew;
-        }
-        Vec_VecFree( vLevels );
-
-        // add the POs
-        Aig_ManForEachPo( p, pObj, i )
-        {
-            pObjNew = Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
-            pObjNew->pHaig = pObj->pHaig;
-            pObj->pData = pObjNew;
-        }
-
-
-/*
-        Aig_ManForEachObj( p, pObj, i )
-        {
-            if ( Aig_ObjIsPi(pObj) )
-            {
-                pObjNew = Aig_ObjCreatePi( pNew );
-                pObjNew->Level = pObj->Level;
-            }
-            else if ( Aig_ObjIsPo(pObj) )
-            {
-//                pObjNew = Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
-            }
-            else if ( Aig_ObjIsConst1(pObj) )
-            {
-                pObjNew = Aig_ManConst1(pNew);
-            }
-            else 
-            {
-                pObjNew = Aig_ManDup_rec( pNew, p, pObj );        
-            }
-            Aig_Regular(pObjNew)->pHaig = pObj->pHaig;
-            pObj->pData = pObjNew;
-        }
-        // add the POs
-        Aig_ManForEachPo( p, pObj, i )
-        {
-            pObjNew = Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
-            pObjNew->pHaig = pObj->pHaig;
-            pObj->pData = pObjNew;
-        }
-*/
-    }
-    // add the POs
-//    assert( Aig_ManBufNum(p) != 0 || Aig_ManNodeNum(p) == Aig_ManNodeNum(pNew) );
-
-    // duplicate the timing manager
-    if ( p->pManTime )
-        pNew->pManTime = Tim_ManDup( p->pManTime, 0 );
-    // check the resulting network
-    if ( !Aig_ManCheck(pNew) )
-        printf( "Aig_ManDup(): The check has failed.\n" );
-    return pNew;
-}
-
-//#endif
-
-#if 0
-
-/**Function*************************************************************
-
-  Synopsis    [Duplicates the AIG manager recursively.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Aig_Obj_t * Aig_ManDup_rec( Aig_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t * pObj )
-{
-    Aig_Obj_t * pObjNew;
-    if ( pObj->pData )
-        return pObj->pData;
-    Aig_ManDup_rec( pNew, p, Aig_ObjFanin0(pObj) );
-    if ( Aig_ObjIsBuf(pObj) )
-        return pObj->pData = Aig_ObjChild0Copy(pObj);
-    Aig_ManDup_rec( pNew, p, Aig_ObjFanin1(pObj) );
-    pObjNew = Aig_Oper( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj), Aig_ObjType(pObj) );
-    Aig_Regular(pObjNew)->pHaig = pObj->pHaig;
-    return pObj->pData = pObjNew;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Duplicates the AIG manager.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Aig_Man_t * Aig_ManDup( Aig_Man_t * p, int fOrdered )
-{
-    Aig_Man_t * pNew;
-    Aig_Obj_t * pObj, * pObjNew;
-    int i;
-    // create the new manager
-    pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
-    pNew->pName = Aig_UtilStrsav( p->pName );
-    pNew->pSpec = Aig_UtilStrsav( p->pSpec );
-    pNew->nRegs = p->nRegs;
-    pNew->nAsserts = p->nAsserts;
-    if ( p->vFlopNums )
-        pNew->vFlopNums = Vec_IntDup( p->vFlopNums );
-    // create the PIs
-    Aig_ManCleanData( p );
-    Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
-    Aig_ManConst1(pNew)->pHaig = Aig_ManConst1(p)->pHaig;
-    Aig_ManForEachPi( p, pObj, i )
-    {
-        pObjNew = Aig_ObjCreatePi( pNew );
-        pObjNew->pHaig = pObj->pHaig;
-        pObjNew->Level = pObj->Level;
-        pObj->pData = pObjNew;
-    }
-    // duplicate internal nodes
-    if ( fOrdered )
-    {
-        Aig_ManForEachObj( p, pObj, i )
-            if ( Aig_ObjIsBuf(pObj) )
-            {
-                pObj->pData = Aig_ObjChild0Copy(pObj);
-            }
-            else if ( Aig_ObjIsNode(pObj) )
-            {
-                pObj->pData = Aig_Oper( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj), Aig_ObjType(pObj) );
-            }
-    }
-    else
-    {
-        Aig_ManForEachObj( p, pObj, i )
-            if ( !Aig_ObjIsPo(pObj) )
-            {
-                Aig_ManDup_rec( pNew, p, pObj );        
-                assert( pObj->Level == ((Aig_Obj_t*)pObj->pData)->Level );
-            }
-    }
-    // add the POs
-    Aig_ManForEachPo( p, pObj, i )
-    {
-        pObjNew = Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
-        pObjNew->pHaig = pObj->pHaig;
-        pObj->pData = pObjNew;
-    }
-    assert( Aig_ManBufNum(p) != 0 || Aig_ManNodeNum(p) == Aig_ManNodeNum(pNew) );
-/*
-    printf( "PIs : " );
-    Aig_ManForEachPi( p, pObj, i )
-        printf( "%d ", pObj->Id );
-    printf( "\n" );
-    printf( "PIs : " );
-    Aig_ManForEachPo( p, pObj, i )
-        printf( "%d ", pObj->Id );
-    printf( "\n" );
-*/
-    // check the resulting network
-    if ( !Aig_ManCheck(pNew) )
-        printf( "Aig_ManDup(): The check has failed.\n" );
-    return pNew;
-}
-
-#endif
-
-/**Function*************************************************************
-
-  Synopsis    [Duplicates the AIG manager.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Aig_Man_t * Aig_ManDupWithoutPos( Aig_Man_t * p )
-{
-    Aig_Man_t * pNew;
-    Aig_Obj_t * pObj;
-    int i;
-    // create the new manager
-    pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
-    pNew->pName = Aig_UtilStrsav( p->pName );
-    pNew->pSpec = Aig_UtilStrsav( p->pSpec );
-    // create the PIs
-    Aig_ManCleanData( p );
-    Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
-    Aig_ManForEachPi( p, pObj, i )
-        pObj->pData = Aig_ObjCreatePi( pNew );
-    // duplicate internal nodes
-    Aig_ManForEachObj( p, pObj, i )
-    {
-        assert( !Aig_ObjIsBuf(pObj) );
-        if ( Aig_ObjIsNode(pObj) )
-            pObj->pData = Aig_Oper( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj), Aig_ObjType(pObj) );
-    }
-    return pNew;
-}
-
-/**Function*************************************************************
-
   Synopsis    [Extracts the miter composed of XOR of the two nodes.]
 
   Description []
@@ -670,7 +297,7 @@ void Aig_ManPrintStats( Aig_Man_t * p )
     printf( "buf = %5d  ",    Aig_ManBufNum(p) );
 //    printf( "Cre = %6d  ",  p->nCreated );
 //    printf( "Del = %6d  ",  p->nDeleted );
-//    printf( "Lev = %3d  ",  Aig_ManCountLevels(p) );
+//    printf( "Lev = %3d  ",  Aig_ManLevelNum(p) );
 //    printf( "Max = %7d  ",  Aig_ManObjNumMax(p) );
     printf( "lev = %3d",  Aig_ManLevels(p) );
     printf( "\n" );
diff --git a/src/aig/aig/aigPart.c b/src/aig/aig/aigPart.c
index 4ce36245..f129ae23 100644
--- a/src/aig/aig/aigPart.c
+++ b/src/aig/aig/aigPart.c
@@ -1162,7 +1162,7 @@ Aig_Man_t * Aig_ManChoicePartitioned( Vec_Ptr_t * vAigs, int nPartSize, int nCon
     extern Aig_Man_t * Fra_FraigChoice( Aig_Man_t * pManAig, int nConfMax, int nLevelMax );
 
     Vec_Ptr_t * vOutsTotal, * vOuts;
-    Aig_Man_t * pAigTotal, * pAigPart, * pAig;
+    Aig_Man_t * pAigTotal, * pAigPart, * pAig, * pTemp;
     Vec_Int_t * vPart, * vPartSupp;
     Vec_Ptr_t * vParts;
     Aig_Obj_t * pObj;
@@ -1272,6 +1272,15 @@ Aig_Man_t * Aig_ManChoicePartitioned( Vec_Ptr_t * vAigs, int nPartSize, int nCon
     pAig = Aig_ManRehash( pAigTotal );
     // create the equivalent nodes lists
     Aig_ManMarkValidChoices( pAig );
+    // reconstruct the network
+    pAig = Aig_ManDupDfsOrder( pTemp = pAig, Vec_PtrEntry( vAigs, 0 ) );
+    Aig_ManStop( pTemp );
+    // duplicate the timing manager
+    pTemp = Vec_PtrEntry( vAigs, 0 );
+    if ( pTemp->pManTime )
+        pAig->pManTime = Tim_ManDup( pTemp->pManTime, 0 );
+    // reset levels
+    Aig_ManChoiceLevel( pAig );
     return pAig;
 }
 
@@ -1437,107 +1446,6 @@ void Aig_ManChoiceConstructiveOne( Aig_Man_t * pNew, Aig_Man_t * pPrev, Aig_Man_
 
 /**Function*************************************************************
 
-  Synopsis    [Computes levels for AIG with choices and white boxes.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Aig_ManChoiceLevel_rec( Aig_Man_t * pNew, Aig_Obj_t * pObj )
-{
-    Aig_Obj_t * pNext;
-    int i, iBox, iTerm1, nTerms, LevelMax = 0;
-    if ( Aig_ObjIsTravIdCurrent( pNew, pObj ) )
-        return;
-    Aig_ObjSetTravIdCurrent( pNew, pObj );
-    if ( Aig_ObjIsPi(pObj) )
-    {
-        if ( pNew->pManTime )
-        {
-            iBox = Tim_ManBoxForCi( pNew->pManTime, Aig_ObjPioNum(pObj) );
-            if ( iBox >= 0 ) // this is not a true PI
-            {
-                iTerm1 = Tim_ManBoxInputFirst( pNew->pManTime, iBox );
-                nTerms = Tim_ManBoxInputNum( pNew->pManTime, iBox );
-                for ( i = 0; i < nTerms; i++ )
-                {
-                    pNext = Aig_ManPo(pNew, iTerm1 + i);
-                    Aig_ManChoiceLevel_rec( pNew, pNext );
-                    if ( LevelMax < Aig_ObjLevel(pNext) )
-                        LevelMax = Aig_ObjLevel(pNext);
-                }
-                LevelMax++;
-            }
-        }
-    }
-    else if ( Aig_ObjIsPo(pObj) )
-    {
-        pNext = Aig_ObjFanin0(pObj);
-        Aig_ManChoiceLevel_rec( pNew, pNext );
-        if ( LevelMax < Aig_ObjLevel(pNext) )
-            LevelMax = Aig_ObjLevel(pNext);
-    }
-    else if ( Aig_ObjIsNode(pObj) )
-    { 
-        // get the maximum level of the two fanins
-        pNext = Aig_ObjFanin0(pObj);
-        Aig_ManChoiceLevel_rec( pNew, pNext );
-        if ( LevelMax < Aig_ObjLevel(pNext) )
-            LevelMax = Aig_ObjLevel(pNext);
-        pNext = Aig_ObjFanin1(pObj);
-        Aig_ManChoiceLevel_rec( pNew, pNext );
-        if ( LevelMax < Aig_ObjLevel(pNext) )
-            LevelMax = Aig_ObjLevel(pNext);
-        LevelMax++;
-
-        // get the level of the nodes in the choice node
-        if ( pNew->pEquivs && (pNext = pNew->pEquivs[pObj->Id]) )
-        {
-            Aig_ManChoiceLevel_rec( pNew, pNext );
-            if ( LevelMax < Aig_ObjLevel(pNext) )
-                LevelMax = Aig_ObjLevel(pNext);
-        }
-    }
-    else
-        assert( 0 );
-    Aig_ObjSetLevel( pObj, LevelMax );
-    assert( !Aig_ObjIsNode(pObj) || LevelMax > 0 );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Computes levels for AIG with choices and white boxes.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Aig_ManChoiceLevel( Aig_Man_t * pNew )
-{
-    Aig_Obj_t * pObj;
-    int i, LevelMax = 0;
-    Aig_ManForEachObj( pNew, pObj, i )
-        Aig_ObjSetLevel( pObj, 0 );
-    Aig_ManSetPioNumbers( pNew );
-    Aig_ManIncrementTravId( pNew );
-    Aig_ManForEachPo( pNew, pObj, i )
-    {
-        Aig_ManChoiceLevel_rec( pNew, pObj );
-        if ( LevelMax < Aig_ObjLevel(pObj) )
-            LevelMax = Aig_ObjLevel(pObj);
-    }
-    Aig_ManCleanPioNumbers( pNew );
-    return LevelMax;
-}
-
-/**Function*************************************************************
-
   Synopsis    [Constructively accumulates choices.]
 
   Description []
@@ -1593,7 +1501,7 @@ Aig_Man_t * Aig_ManChoiceConstructive( Vec_Ptr_t * vAigs, int fVerbose )
     int i;
     // start AIG with choices
     pPrev = Vec_PtrEntry( vAigs, 0 );
-    pNew = Aig_ManDup( pPrev, 1 );
+    pNew = Aig_ManDupOrdered( pPrev );
     // create room for equivalent nodes and representatives
     assert( pNew->pReprs == NULL );
     pNew->nReprsAlloc = Vec_PtrSize(vAigs) * Aig_ManObjNumMax(pNew);
diff --git a/src/aig/aig/aigRetF.c b/src/aig/aig/aigRetF.c
index e52283b1..f045cac8 100644
--- a/src/aig/aig/aigRetF.c
+++ b/src/aig/aig/aigRetF.c
@@ -199,7 +199,7 @@ Aig_Man_t * Aig_ManRetimeFrontier( Aig_Man_t * p, int nStepsMax )
     // remove useless registers
     Aig_ManSeqCleanup( p );
     // rehash the nodes
-    return Aig_ManDup( p, 1 ); 
+    return Aig_ManDupOrdered( p ); 
 }
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/aig/aigUtil.c b/src/aig/aig/aigUtil.c
index dcc0a118..e9382468 100644
--- a/src/aig/aig/aigUtil.c
+++ b/src/aig/aig/aigUtil.c
@@ -593,6 +593,12 @@ void Aig_ObjPrintVerbose( Aig_Obj_t * pObj, int fHaig )
         printf( "constant 1" );
     else if ( Aig_ObjIsPi(pObj) )
         printf( "PI" );
+    else if ( Aig_ObjIsPo(pObj) )
+    {
+        printf( "PO" );
+        printf( "%p%s", 
+            Aig_ObjFanin0(pObj), (Aig_ObjFaninC0(pObj)? "\'" : " ") );
+    }
     else
         printf( "AND( %p%s, %p%s )", 
             Aig_ObjFanin0(pObj), (Aig_ObjFaninC0(pObj)? "\'" : " "), 
@@ -620,7 +626,7 @@ void Aig_ManPrintVerbose( Aig_Man_t * p, int fHaig )
     Aig_ManForEachPi( p, pObj, i )
         printf( " %p", pObj );
     printf( "\n" );
-    vNodes = Aig_ManDfs( p );
+    vNodes = Aig_ManDfs( p, 0 );
     Vec_PtrForEachEntry( vNodes, pObj, i )
         Aig_ObjPrintVerbose( pObj, fHaig ), printf( "\n" );
     printf( "\n" );
@@ -674,7 +680,7 @@ void Aig_ManDumpBlif( Aig_Man_t * p, char * pFileName )
         if ( Aig_ObjIsConst1(Aig_ObjFanin0(pObj)) )
             pConst1 = Aig_ManConst1(p);
     // collect nodes in the DFS order
-    vNodes = Aig_ManDfs( p );
+    vNodes = Aig_ManDfs( p, 1 );
     // assign IDs to objects
     Aig_ManConst1(p)->iData = Counter++;
     Aig_ManForEachPi( p, pObj, i )
@@ -758,7 +764,7 @@ void Aig_ManDumpVerilog( Aig_Man_t * p, char * pFileName )
         if ( Aig_ObjIsConst1(Aig_ObjFanin0(pObj)) )
             pConst1 = Aig_ManConst1(p);
     // collect nodes in the DFS order
-    vNodes = Aig_ManDfs( p );
+    vNodes = Aig_ManDfs( p, 1 );
     // assign IDs to objects
     Aig_ManConst1(p)->iData = Counter++;
     Aig_ManForEachPi( p, pObj, i )
diff --git a/src/aig/aig/module.make b/src/aig/aig/module.make
index ddb12e6e..f1d018af 100644
--- a/src/aig/aig/module.make
+++ b/src/aig/aig/module.make
@@ -1,6 +1,7 @@
 SRC +=    src/aig/aig/aigCheck.c \
     src/aig/aig/aigCuts.c \
     src/aig/aig/aigDfs.c \
+    src/aig/aig/aigDup.c \
     src/aig/aig/aigFanout.c \
     src/aig/aig/aigFrames.c \
     src/aig/aig/aigInter.c \
diff --git a/src/aig/dar/darMan.c b/src/aig/dar/darMan.c
index 0a5a36b1..9ab504c0 100644
--- a/src/aig/dar/darMan.c
+++ b/src/aig/dar/darMan.c
@@ -122,6 +122,7 @@ void Dar_ManPrintStats( Dar_Man_t * p )
 //        PRTP( "T", p->ClassTimes[i], p->timeEval );
         printf( "\n" );
     }
+    fflush( stdout );
 }
 
 
diff --git a/src/aig/dar/darScript.c b/src/aig/dar/darScript.c
index 7d78bf40..69810125 100644
--- a/src/aig/dar/darScript.c
+++ b/src/aig/dar/darScript.c
@@ -45,9 +45,9 @@ Aig_Man_t * Dar_ManRewriteDefault( Aig_Man_t * pAig )
     Aig_Man_t * pTemp;
     Dar_RwrPar_t Pars, * pPars = &Pars;
     Dar_ManDefaultRwrParams( pPars );
-    pAig = Aig_ManDup( pAig, 0 ); 
+    pAig = Aig_ManDupDfs( pAig ); 
     Dar_ManRewrite( pAig, pPars );
-    pAig = Aig_ManDup( pTemp = pAig, 0 ); 
+    pAig = Aig_ManDupDfs( pTemp = pAig ); 
     Aig_ManStop( pTemp );
     return pAig;
 }
@@ -80,18 +80,18 @@ Aig_Man_t * Dar_ManRwsat( Aig_Man_t * pAig, int fBalance, int fVerbose )
     pParsRwr->fVerbose = fVerbose;
     pParsRef->fVerbose = fVerbose;
 
-    pAig = Aig_ManDup( pAig, 0 ); 
+    pAig = Aig_ManDupDfs( pAig ); 
     if ( fVerbose ) Aig_ManPrintStats( pAig );
     
     // rewrite
     Dar_ManRewrite( pAig, pParsRwr );
-    pAig = Aig_ManDup( pTemp = pAig, 0 ); 
+    pAig = Aig_ManDupDfs( pTemp = pAig ); 
     Aig_ManStop( pTemp );
     if ( fVerbose ) Aig_ManPrintStats( pAig );
 /*    
     // refactor
     Dar_ManRefactor( pAig, pParsRef );
-    pAig = Aig_ManDup( pTemp = pAig, 0 ); 
+    pAig = Aig_ManDupDfs( pTemp = pAig ); 
     Aig_ManStop( pTemp );
     if ( fVerbose ) Aig_ManPrintStats( pAig );
 */
@@ -105,7 +105,7 @@ Aig_Man_t * Dar_ManRwsat( Aig_Man_t * pAig, int fBalance, int fVerbose )
     
     // rewrite
     Dar_ManRewrite( pAig, pParsRwr );
-    pAig = Aig_ManDup( pTemp = pAig, 0 ); 
+    pAig = Aig_ManDupDfs( pTemp = pAig ); 
     Aig_ManStop( pTemp );
     if ( fVerbose ) Aig_ManPrintStats( pAig );
 
@@ -161,7 +161,7 @@ Aig_Man_t * Dar_ManCompress( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, i
     pParsRwr->fVerbose = 0;//fVerbose;
     pParsRef->fVerbose = 0;//fVerbose;
 
-    pAig = Aig_ManDup( pAig, 0 ); 
+    pAig = Aig_ManDupDfs( pAig ); 
     if ( fVerbose ) Aig_ManPrintStats( pAig );
 
     // balance
@@ -174,13 +174,13 @@ Aig_Man_t * Dar_ManCompress( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, i
     
     // rewrite
     Dar_ManRewrite( pAig, pParsRwr );
-    pAig = Aig_ManDup( pTemp = pAig, 0 ); 
+    pAig = Aig_ManDupDfs( pTemp = pAig ); 
     Aig_ManStop( pTemp );
     if ( fVerbose ) Aig_ManPrintStats( pAig );
     
     // refactor
     Dar_ManRefactor( pAig, pParsRef );
-    pAig = Aig_ManDup( pTemp = pAig, 0 ); 
+    pAig = Aig_ManDupDfs( pTemp = pAig ); 
     Aig_ManStop( pTemp );
     if ( fVerbose ) Aig_ManPrintStats( pAig );
 
@@ -197,7 +197,7 @@ Aig_Man_t * Dar_ManCompress( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, i
     
     // rewrite
     Dar_ManRewrite( pAig, pParsRwr );
-    pAig = Aig_ManDup( pTemp = pAig, 0 ); 
+    pAig = Aig_ManDupDfs( pTemp = pAig ); 
     Aig_ManStop( pTemp );
     if ( fVerbose ) Aig_ManPrintStats( pAig );
 
@@ -233,7 +233,7 @@ Aig_Man_t * Dar_ManCompress2( Aig_Man_t * pAig, int fBalance, int fUpdateLevel,
     pParsRwr->fVerbose = 0;//fVerbose;
     pParsRef->fVerbose = 0;//fVerbose;
 
-    pAig = Aig_ManDup( pAig, 0 ); 
+    pAig = Aig_ManDupDfs( pAig ); 
     if ( fVerbose ) Aig_ManPrintStats( pAig );
 
     // balance
@@ -247,13 +247,13 @@ Aig_Man_t * Dar_ManCompress2( Aig_Man_t * pAig, int fBalance, int fUpdateLevel,
 
     // rewrite
     Dar_ManRewrite( pAig, pParsRwr );
-    pAig = Aig_ManDup( pTemp = pAig, 0 ); 
+    pAig = Aig_ManDupDfs( pTemp = pAig ); 
     Aig_ManStop( pTemp );
     if ( fVerbose ) Aig_ManPrintStats( pAig );
     
     // refactor
     Dar_ManRefactor( pAig, pParsRef );
-    pAig = Aig_ManDup( pTemp = pAig, 0 ); 
+    pAig = Aig_ManDupDfs( pTemp = pAig ); 
     Aig_ManStop( pTemp );
     if ( fVerbose ) Aig_ManPrintStats( pAig );
 
@@ -267,7 +267,7 @@ Aig_Man_t * Dar_ManCompress2( Aig_Man_t * pAig, int fBalance, int fUpdateLevel,
     
     // rewrite
     Dar_ManRewrite( pAig, pParsRwr );
-    pAig = Aig_ManDup( pTemp = pAig, 0 ); 
+    pAig = Aig_ManDupDfs( pTemp = pAig ); 
     Aig_ManStop( pTemp );
     if ( fVerbose ) Aig_ManPrintStats( pAig );
 
@@ -276,7 +276,7 @@ Aig_Man_t * Dar_ManCompress2( Aig_Man_t * pAig, int fBalance, int fUpdateLevel,
     
     // rewrite
     Dar_ManRewrite( pAig, pParsRwr );
-    pAig = Aig_ManDup( pTemp = pAig, 0 ); 
+    pAig = Aig_ManDupDfs( pTemp = pAig ); 
     Aig_ManStop( pTemp );
     if ( fVerbose ) Aig_ManPrintStats( pAig );
 
@@ -290,13 +290,13 @@ Aig_Man_t * Dar_ManCompress2( Aig_Man_t * pAig, int fBalance, int fUpdateLevel,
     
     // refactor
     Dar_ManRefactor( pAig, pParsRef );
-    pAig = Aig_ManDup( pTemp = pAig, 0 ); 
+    pAig = Aig_ManDupDfs( pTemp = pAig ); 
     Aig_ManStop( pTemp );
     if ( fVerbose ) Aig_ManPrintStats( pAig );
     
     // rewrite
     Dar_ManRewrite( pAig, pParsRwr );
-    pAig = Aig_ManDup( pTemp = pAig, 0 ); 
+    pAig = Aig_ManDupDfs( pTemp = pAig ); 
     Aig_ManStop( pTemp );
     if ( fVerbose ) Aig_ManPrintStats( pAig );
 
@@ -330,7 +330,7 @@ Vec_Ptr_t * Dar_ManChoiceSynthesis( Aig_Man_t * pAig, int fBalance, int fUpdateL
     int i;
 
     vAigs = Vec_PtrAlloc( 3 );
-    pAig = Aig_ManDup(pAig, 0);
+    pAig = Aig_ManDupDfs(pAig);
     Vec_PtrPush( vAigs, pAig );
 
     Aig_ManForEachObj( pAig, pObj, i )
diff --git a/src/aig/fra/fraCec.c b/src/aig/fra/fraCec.c
index aead8c9e..779337bf 100644
--- a/src/aig/fra/fraCec.c
+++ b/src/aig/fra/fraCec.c
@@ -166,7 +166,7 @@ PRT( "Time", clock() - clk );
 
     // duplicate the AIG
 clk = clock();
-//    pAig = Aig_ManDup( pTemp = pAig );
+//    pAig = Aig_ManDupDfs( pTemp = pAig );
     pAig = Dar_ManRwsat( pTemp = pAig, 0, 0 );
     Aig_ManStop( pTemp );
     if ( fVerbose )
diff --git a/src/aig/fra/fraCore.c b/src/aig/fra/fraCore.c
index 444157f0..80799e3e 100644
--- a/src/aig/fra/fraCore.c
+++ b/src/aig/fra/fraCore.c
@@ -369,7 +369,7 @@ Aig_Man_t * Fra_FraigPerform( Aig_Man_t * pManAig, Fra_Par_t * pPars )
     Aig_Man_t * pManAigNew;
     int clk;
     if ( Aig_ManNodeNum(pManAig) == 0 )
-        return Aig_ManDup(pManAig, 1);
+        return Aig_ManDupOrdered(pManAig);
 clk = clock();
     p = Fra_ManStart( pManAig, pPars );
     p->pManFraig = Fra_ManPrepareComb( p );
diff --git a/src/aig/fra/fraInd.c b/src/aig/fra/fraInd.c
index 8b9e863e..03d03ea1 100644
--- a/src/aig/fra/fraInd.c
+++ b/src/aig/fra/fraInd.c
@@ -343,7 +343,7 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, Fra_Ssw_t * pParams )
     if ( Aig_ManNodeNum(pManAig) == 0 )
     {
         pParams->nIters = 0;
-        return Aig_ManDup(pManAig, 1);
+        return Aig_ManDupOrdered(pManAig);
     }
     assert( Aig_ManRegNum(pManAig) > 0 );
     assert( pParams->nFramesK > 0 );
@@ -563,7 +563,7 @@ clk2 = clock();
         Aig_Man_t * pNew;
         char * pFileName = Ioa_FileNameGenericAppend( p->pManAig->pName, "_care.aig" );
         printf( "Care one-hotness clauses will be written into file \"%s\".\n", pFileName );
-        pManAigNew = Aig_ManDup( pManAig, 1 );
+        pManAigNew = Aig_ManDupOrdered( pManAig );
         pNew = Fra_OneHotCreateExdc( p, p->vOneHots );
         Ioa_WriteAiger( pNew, pFileName, 0, 1 );
         Aig_ManStop( pNew );
diff --git a/src/aig/fra/fraLcr.c b/src/aig/fra/fraLcr.c
index 9149aca4..145bafae 100644
--- a/src/aig/fra/fraLcr.c
+++ b/src/aig/fra/fraLcr.c
@@ -251,6 +251,31 @@ int Fra_LcrNodeIsConst( Aig_Obj_t * pObj )
 
 /**Function*************************************************************
 
+  Synopsis    [Duplicates the AIG manager recursively.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Obj_t * Fra_LcrManDup_rec( Aig_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t * pObj )
+{
+    Aig_Obj_t * pObjNew;
+    if ( pObj->pData )
+        return pObj->pData;
+    Fra_LcrManDup_rec( pNew, p, Aig_ObjFanin0(pObj) );
+    if ( Aig_ObjIsBuf(pObj) )
+        return pObj->pData = Aig_ObjChild0Copy(pObj);
+    Fra_LcrManDup_rec( pNew, p, Aig_ObjFanin1(pObj) );
+    pObjNew = Aig_Oper( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj), Aig_ObjType(pObj) );
+    Aig_Regular(pObjNew)->pHaig = pObj->pHaig;
+    return pObj->pData = pObjNew;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Give the AIG and classes, reduces AIG for partitioning.]
 
   Description [Ignores registers that are not in the classes. 
@@ -290,7 +315,7 @@ Aig_Man_t * Fra_LcrDeriveAigForPartitioning( Fra_Lcr_t * pLcr )
         {
             assert( Aig_ObjIsPi(ppClass[c]) );
             pObjPo  = Aig_ManPo( pLcr->pAig, Offset+(long)ppClass[c]->pNext );
-            pObjNew = Aig_ManDup_rec( pNew, pLcr->pAig, Aig_ObjFanin0(pObjPo) );
+            pObjNew = Fra_LcrManDup_rec( pNew, pLcr->pAig, Aig_ObjFanin0(pObjPo) );
             pMiter  = Aig_Exor( pNew, pMiter, pObjNew );
         }
         Aig_ObjCreatePo( pNew, pMiter );
@@ -300,7 +325,7 @@ Aig_Man_t * Fra_LcrDeriveAigForPartitioning( Fra_Lcr_t * pLcr )
     {
         assert( Aig_ObjIsPi(pObj) );
         pObjPo = Aig_ManPo( pLcr->pAig, Offset+(long)pObj->pNext );
-        pMiter = Aig_ManDup_rec( pNew, pLcr->pAig, Aig_ObjFanin0(pObjPo) );
+        pMiter = Fra_LcrManDup_rec( pNew, pLcr->pAig, Aig_ObjFanin0(pObjPo) );
         Aig_ObjCreatePo( pNew, pMiter );
     }
     return pNew;
@@ -514,7 +539,7 @@ Aig_Man_t * Fra_FraigLatchCorrespondence( Aig_Man_t * pAig, int nFramesP, int nC
     if ( Aig_ManNodeNum(pAig) == 0 )
     {
         if ( pnIter ) *pnIter = 0;
-        return Aig_ManDup(pAig, 1);
+        return Aig_ManDupOrdered(pAig);
     }
     assert( Aig_ManRegNum(pAig) > 0 );
 
diff --git a/src/aig/fra/fraMan.c b/src/aig/fra/fraMan.c
index 720260a5..da7c37a3 100644
--- a/src/aig/fra/fraMan.c
+++ b/src/aig/fra/fraMan.c
@@ -298,6 +298,7 @@ void Fra_ManPrint( Fra_Man_t * p )
     if ( p->time1 ) { PRT( "time1           ", p->time1 ); }
     if ( p->nSpeculs )
     printf( "Speculations = %d.\n", p->nSpeculs );
+    fflush( stdout );
 }
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/fra/fraSec.c b/src/aig/fra/fraSec.c
index bbad2a6e..83a551b8 100644
--- a/src/aig/fra/fraSec.c
+++ b/src/aig/fra/fraSec.c
@@ -52,7 +52,8 @@ int Fra_FraigSec( Aig_Man_t * p, int nFramesMax, int fRetimeFirst, int fFraiging
     pPars->fLatchCorr  = fLatchCorr;
     pPars->fVerbose = fVeryVerbose;
 
-    pNew = Aig_ManDup( p, 1 );
+    pNew = Aig_ManDupOrdered( p );
+//    pNew = Aig_ManDupDfs( p );
     if ( fVerbose )
     {
         printf( "Original miter:       Latches = %5d. Nodes = %6d.\n", 
@@ -91,7 +92,8 @@ PRT( "Time", clock() - clk );
 clk = clock();
     if ( pNew->nRegs )
     {
-    pNew = Aig_ManDup( pTemp = pNew, 1 );
+    pNew = Aig_ManDupOrdered( pTemp = pNew );
+//    pNew = Aig_ManDupDfs( pTemp = pNew );
     Aig_ManStop( pTemp );
     pNew = Fra_FraigLatchCorrespondence( pTemp = pNew, 0, 100000, 1, fVeryVerbose, &nIter );
     p->pSeqModel = pTemp->pSeqModel; pTemp->pSeqModel = NULL;
@@ -147,7 +149,7 @@ PRT( "Time", clock() - clk );
 
         // perform rewriting
 clk = clock();
-        pNew = Aig_ManDup( pTemp = pNew, 1 );
+        pNew = Aig_ManDupOrdered( pTemp = pNew );
         Aig_ManStop( pTemp );
         pNew = Dar_ManRewriteDefault( pTemp = pNew );
         Aig_ManStop( pTemp );
@@ -165,7 +167,7 @@ PRT( "Time", clock() - clk );
 clk = clock();
         pNew = Rtm_ManRetime( pTemp = pNew, 1, 1000, 0 );
         Aig_ManStop( pTemp );
-        pNew = Aig_ManDup( pTemp = pNew, 1 );
+        pNew = Aig_ManDupOrdered( pTemp = pNew );
         Aig_ManStop( pTemp );
         if ( fVerbose )
         {
diff --git a/src/aig/ivy/ivyMan.c b/src/aig/ivy/ivyMan.c
index 07faef85..66c279cf 100644
--- a/src/aig/ivy/ivyMan.c
+++ b/src/aig/ivy/ivyMan.c
@@ -462,6 +462,7 @@ void Ivy_ManPrintStats( Ivy_Man_t * p )
 //    printf( "Del = %d. ",     p->nDeleted );
     printf( "Lev = %3d. ",     Ivy_ManLatchNum(p)? -1 : Ivy_ManLevels(p) );
     printf( "\n" );
+    fflush( stdout );
 }
 
 /**Function*************************************************************
diff --git a/src/aig/ntl/ntlCore.c b/src/aig/ntl/ntlCore.c
index ed0f057b..fb4bb620 100644
--- a/src/aig/ntl/ntlCore.c
+++ b/src/aig/ntl/ntlCore.c
@@ -39,16 +39,18 @@
   SeeAlso     []
 
 ***********************************************************************/
-Aig_Man_t * Ntl_ManPerformSynthesis( Aig_Man_t * pAig )
+Aig_Man_t * Ntl_ManPerformSynthesis( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fConstruct, int nConfMax, int nLevelMax, int fVerbose )
 {
     extern Aig_Man_t * Dar_ManBalance( Aig_Man_t * pAig, int fUpdateLevel );
     extern Aig_Man_t * Dar_ManCompress( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fVerbose );
+    extern Aig_Man_t * Dar_ManChoice( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fConstruct, int nConfMax, int nLevelMax, int fVerbose );
     Aig_Man_t * pTemp;
     // perform synthesis
 //printf( "Pre-synthesis AIG:  " );
 //Aig_ManPrintStats( pAig );
 //    pTemp = Dar_ManBalance( pAig, 1 );
-    pTemp = Dar_ManCompress( pAig, 1, 1, 0 );
+//    pTemp = Dar_ManCompress( pAig, 1, 1, 0 );
+    pTemp = Dar_ManChoice( pAig, fBalance, fUpdateLevel, fConstruct, nConfMax, nLevelMax, fVerbose );
 //printf( "Post-synthesis AIG: " );
 //Aig_ManPrintStats( pTemp );
     return pTemp;
diff --git a/src/aig/nwk/nwkDfs.c b/src/aig/nwk/nwkDfs.c
index bf669086..308f4693 100644
--- a/src/aig/nwk/nwkDfs.c
+++ b/src/aig/nwk/nwkDfs.c
@@ -66,9 +66,9 @@ int Nwk_ManVerifyTopoOrder( Nwk_Man_t * pNtk )
                 {
                     iTerm1 = Tim_ManBoxInputFirst( pNtk->pManTime, iBox );
                     nTerms = Tim_ManBoxInputNum( pNtk->pManTime, iBox );
-                    for ( i = 0; i < nTerms; i++ )
+                    for ( k = 0; k < nTerms; k++ )
                     {
-                        pNext = Nwk_ManCo( pNtk, iTerm1 + i );
+                        pNext = Nwk_ManCo( pNtk, iTerm1 + k );
                         if ( !Nwk_ObjIsTravIdCurrent(pNext) )
                         {
                             printf( "Box %d has input %d that is not in a topological order.\n", iBox, pNext->Id );
diff --git a/src/aig/nwk/nwkMap.c b/src/aig/nwk/nwkMap.c
index eae3bd24..44aecc03 100644
--- a/src/aig/nwk/nwkMap.c
+++ b/src/aig/nwk/nwkMap.c
@@ -115,9 +115,13 @@ If_Man_t * Nwk_ManToIf( Aig_Man_t * p, If_Par_t * pPars, Vec_Ptr_t * vAigToIf )
         {
             pIfObj = If_ManCreateCi( pIfMan );
             If_ObjSetLevel( pIfObj, Aig_ObjLevel(pNode) );
+//            printf( "pi=%d ", pIfObj->Level );
         }
         else if ( Aig_ObjIsPo(pNode) )
+        {
             pIfObj = If_ManCreateCo( pIfMan, If_NotCond( Aig_ObjFanin0(pNode)->pData, Aig_ObjFaninC0(pNode) ) );
+//            printf( "po=%d ", pIfObj->Level );
+        }
         else if ( Aig_ObjIsConst1(pNode) )
             pIfObj = If_ManConst1( pIfMan );
         else // add the node to the mapper
@@ -130,11 +134,11 @@ If_Man_t * Nwk_ManToIf( Aig_Man_t * p, If_Par_t * pPars, Vec_Ptr_t * vAigToIf )
         if ( Aig_ObjIsChoice( p, pNode ) )
         {
             pIfMan->nChoices++;
-            for ( pPrev = pNode, pFanin = pNode->pData; pFanin; pPrev = pFanin, pFanin = pFanin->pData )
+            for ( pPrev = pNode, pFanin = p->pEquivs[pNode->Id]; pFanin; pPrev = pFanin, pFanin = p->pEquivs[pFanin->Id] )
                 If_ObjSetChoice( pPrev->pData, pFanin->pData );
             If_ManCreateChoice( pIfMan, pNode->pData );
         }
-        assert( If_ObjLevel(pIfObj) == Aig_ObjLevel(pNode) );
+//        assert( If_ObjLevel(pIfObj) == Aig_ObjLevel(pNode) );
     }
     return pIfMan;
 }
diff --git a/src/aig/nwk/nwkStrash.c b/src/aig/nwk/nwkStrash.c
index 627bfa67..3bcfcd41 100644
--- a/src/aig/nwk/nwkStrash.c
+++ b/src/aig/nwk/nwkStrash.c
@@ -127,7 +127,7 @@ Aig_Man_t * Nwk_ManStrash( Nwk_Man_t * pNtk )
         pObj->pCopy = pObjNew;
     }
     Aig_ManCleanup( pMan );
-//    pMan = Aig_ManDup( pTemp = pMan, 1 );
+//    pMan = Aig_ManDupOrdered( pTemp = pMan );
 //    Aig_ManStop( pTemp );
     return pMan;
 }
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index f77c90e5..f0f7fb56 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -14986,15 +14986,56 @@ usage:
 int Abc_CommandAbc8DChoice( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     Aig_Man_t * pAigNew;
-    int c;
-    extern Aig_Man_t * Ntl_ManPerformSynthesis( Aig_Man_t * pAig );
+    int fBalance, fVerbose, fUpdateLevel, fConstruct, c;
+    int nConfMax, nLevelMax;
+    extern Aig_Man_t * Ntl_ManPerformSynthesis( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fConstruct, int nConfMax, int nLevelMax, int fVerbose );
 
     // set defaults
+    fBalance     = 1;
+    fUpdateLevel = 1;
+    fConstruct   = 0;
+    nConfMax     = 1000;
+    nLevelMax    = 0;
+    fVerbose     = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "CLblcvh" ) ) != EOF )
     {
         switch ( c )
         {
+        case 'C':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( stdout, "Command line switch \"-C\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nConfMax = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nConfMax < 0 ) 
+                goto usage;
+            break;
+        case 'L':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( stdout, "Command line switch \"-L\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nLevelMax = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nLevelMax < 0 ) 
+                goto usage;
+            break;
+        case 'b':
+            fBalance ^= 1;
+            break;
+        case 'l':
+            fUpdateLevel ^= 1;
+            break;
+        case 'c':
+            fConstruct ^= 1;
+            break;
+        case 'v':
+            fVerbose ^= 1;
+            break;
         case 'h':
             goto usage;
         default:
@@ -15008,7 +15049,7 @@ int Abc_CommandAbc8DChoice( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
 
     // get the input file name
-    pAigNew = Ntl_ManPerformSynthesis( pAbc->pAbc8Aig );
+    pAigNew = Ntl_ManPerformSynthesis( pAbc->pAbc8Aig, fBalance, fUpdateLevel, fConstruct, nConfMax, nLevelMax, fVerbose );
     if ( pAigNew == NULL )
     {
         printf( "Abc_CommandAbc8DChoice(): Tranformation of the AIG has failed.\n" );
@@ -15019,9 +15060,15 @@ int Abc_CommandAbc8DChoice( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( stdout, "usage: *dchoice [-h]\n" );
-    fprintf( stdout, "\t        performs AIG-based synthesis and derives choices\n" );
-    fprintf( stdout, "\t-h    : print the command usage\n");
+    fprintf( stdout, "usage: *dchoice [-C num] [-L num] [-blcvh]\n" );
+    fprintf( stdout, "\t         performs AIG-based synthesis and derives choices\n" );
+    fprintf( stdout, "\t-C num : the max number of conflicts at a node [default = %d]\n", nConfMax );
+    fprintf( stdout, "\t-L num : the max level of nodes to consider (0 = not used) [default = %d]\n", nLevelMax );
+    fprintf( stdout, "\t-b     : toggle internal balancing [default = %s]\n", fBalance? "yes": "no" );
+    fprintf( stdout, "\t-l     : toggle updating level [default = %s]\n", fUpdateLevel? "yes": "no" );
+    fprintf( stdout, "\t-c     : toggle constructive computation of choices [default = %s]\n", fConstruct? "yes": "no" );
+    fprintf( stdout, "\t-v     : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" );
+    fprintf( stdout, "\t-h     : print the command usage\n");
     return 1;
 }
 
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index 2737de32..9be147f4 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -169,7 +169,7 @@ Abc_Ntk_t * Abc_NtkFromDar( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan )
     Aig_ManForEachPi( pMan, pObj, i )
         pObj->pData = Abc_NtkCi(pNtkNew, i);
     // rebuild the AIG
-    vNodes = Aig_ManDfs( pMan );
+    vNodes = Aig_ManDfs( pMan, 1 );
     Vec_PtrForEachEntry( vNodes, pObj, i )
         if ( Aig_ObjIsBuf(pObj) )
             pObj->pData = (Abc_Obj_t *)Aig_ObjChild0Copy(pObj);
@@ -246,7 +246,7 @@ Abc_Ntk_t * Abc_NtkFromDarSeqSweep( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan )
         Abc_LatchSetInit0( pObjNew );
     }
     // rebuild the AIG
-    vNodes = Aig_ManDfs( pMan );
+    vNodes = Aig_ManDfs( pMan, 1 );
     Vec_PtrForEachEntry( vNodes, pObj, i )
         if ( Aig_ObjIsBuf(pObj) )
             pObj->pData = (Abc_Obj_t *)Aig_ObjChild0Copy(pObj);
@@ -411,7 +411,7 @@ Abc_Ntk_t * Abc_NtkFromDarSeq( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan )
     }
     Abc_NtkAddDummyBoxNames( pNtkNew );
     // rebuild the AIG
-    vNodes = Aig_ManDfs( pMan );
+    vNodes = Aig_ManDfs( pMan, 1 );
     Vec_PtrForEachEntry( vNodes, pObj, i )
     {
         // add the first fanin
@@ -629,7 +629,7 @@ Abc_Ntk_t * Abc_NtkDRewrite( Abc_Ntk_t * pNtk, Dar_RwrPar_t * pPars )
 //    Aig_ManStop( pTemp );
 
 clk = clock();
-    pMan = Aig_ManDup( pTemp = pMan, 0 ); 
+    pMan = Aig_ManDupDfs( pTemp = pMan ); 
     Aig_ManStop( pTemp );
 //PRT( "time", clock() - clk );
 
@@ -666,7 +666,7 @@ Abc_Ntk_t * Abc_NtkDRefactor( Abc_Ntk_t * pNtk, Dar_RefPar_t * pPars )
 //    Aig_ManStop( pTemp );
 
 clk = clock();
-    pMan = Aig_ManDup( pTemp = pMan, 0 ); 
+    pMan = Aig_ManDupDfs( pTemp = pMan ); 
     Aig_ManStop( pTemp );
 //PRT( "time", clock() - clk );
 
diff --git a/src/base/abci/abcPrint.c b/src/base/abci/abcPrint.c
index e5f028fe..fafcb52d 100644
--- a/src/base/abci/abcPrint.c
+++ b/src/base/abci/abcPrint.c
@@ -293,6 +293,7 @@ void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored, int fSave
 //    if ( Abc_NtkHasSop(pNtk) )
 //        printf( "The total number of cube pairs = %d.\n", Abc_NtkGetCubePairNum(pNtk) );
    
+    fflush( stdout );
 }
 
 /**Function*************************************************************
diff --git a/src/misc/hash/hashInt.h b/src/misc/hash/hashInt.h
index 3b91f5df..b7ec8a8c 100644
--- a/src/misc/hash/hashInt.h
+++ b/src/misc/hash/hashInt.h
@@ -90,7 +90,7 @@ static inline Hash_Int_t * Hash_IntAlloc( int nBins )
   p->nBins = nBins;
   p->fHash = Hash_DefaultHashFunc;
   p->nSize  = 0;
-  p->pArray = ALLOC( Hash_Int_Entry_t *, nBins );
+  p->pArray = ALLOC( Hash_Int_Entry_t *, nBins+1 );
   for(i=0; i<nBins; i++)
     p->pArray[i] = NULL;
 
@@ -270,17 +270,18 @@ static inline int* Hash_IntEntryPtr( Hash_Int_t *p, int key )
 ***********************************************************************/
 static inline void Hash_IntFree( Hash_Int_t *p ) {
   int bin;
-  Hash_Int_Entry_t *pEntry;
+  Hash_Int_Entry_t *pEntry, *pTemp;
 
   // free bins
   for(bin = 0; bin < p->nBins; bin++) {
     pEntry = p->pArray[bin];
     while(pEntry) {
+      pTemp = pEntry;
       pEntry = pEntry->pNext;
-      FREE( pEntry );
+      FREE( pTemp );
     }
   }
- 
+
   // free hash
   FREE( p->pArray );
   FREE( p );
diff --git a/src/sat/fraig/fraigMan.c b/src/sat/fraig/fraigMan.c
index 7fd937d5..12cb5c45 100644
--- a/src/sat/fraig/fraigMan.c
+++ b/src/sat/fraig/fraigMan.c
@@ -369,6 +369,7 @@ void Fraig_ManPrintStats( Fraig_Man_t * p )
     if ( p->time4 > 0 ) { Fraig_PrintTime( "time4", p->time4 ); }
 //    PRT( "Selection ", timeSelect );
 //    PRT( "Assignment", timeAssign );
+    fflush( stdout );
 }
 
 /**Function*************************************************************