Version abc70726

35 files changed, 2591 insertions, 507 deletions

diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h
index 8c9400be..230c354f 100644
--- a/src/aig/aig/aig.h
+++ b/src/aig/aig/aig.h
@@ -106,6 +106,16 @@ struct Aig_Man_t_
     int              nBufReplaces;   // the number of times replacement led to a buffer
     int              nBufFixes;      // the number of times buffers were propagated
     int              nBufMax;        // the maximum number of buffers during computation
+    // topological order
+    unsigned *       pOrderData;
+    int              nOrderAlloc;
+    int              iPrev;
+    int              iNext;
+    int              nAndTotal;
+    int              nAndPrev;
+    // representatives
+    Aig_Obj_t **     pRepr;
+    int              nReprAlloc;
     // various data members
     Aig_MmFixed_t *  pMemObjs;       // memory manager for objects
     Vec_Int_t *      vLevelR;        // the reverse level of the nodes
@@ -113,6 +123,7 @@ struct Aig_Man_t_
     void *           pData;          // the temporary data
     int              nTravIds;       // the current traversal ID
     int              fCatchExor;     // enables EXOR nodes
+    Aig_Obj_t **     pReprs;         // linked list of equivalent nodes (when choices are used)
     // timing statistics
     int              time1;
     int              time2;
@@ -124,6 +135,7 @@ struct Aig_Man_t_
 
 #define AIG_MIN(a,b)       (((a) < (b))? (a) : (b))
 #define AIG_MAX(a,b)       (((a) > (b))? (a) : (b))
+#define AIG_ABS(a)         (((a) >= 0)?  (a) :-(a))
 #define AIG_INFINITY       (100000000)
 
 #ifndef PRT
@@ -197,7 +209,7 @@ static inline Aig_Obj_t *  Aig_ObjChild0( Aig_Obj_t * pObj )      { return pObj-
 static inline Aig_Obj_t *  Aig_ObjChild1( Aig_Obj_t * pObj )      { return pObj->pFanin1;                          }
 static inline Aig_Obj_t *  Aig_ObjChild0Copy( Aig_Obj_t * pObj ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin0(pObj)? Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj)) : NULL;  }
 static inline Aig_Obj_t *  Aig_ObjChild1Copy( Aig_Obj_t * pObj ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin1(pObj)? Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin1(pObj)->pData, Aig_ObjFaninC1(pObj)) : NULL;  }
-static inline int          Aig_ObjLevel( Aig_Obj_t * pObj )       { return pObj->nRefs;                            }
+static inline int          Aig_ObjLevel( Aig_Obj_t * pObj )       { return pObj->Level;                            }
 static inline int          Aig_ObjLevelNew( Aig_Obj_t * pObj )    { return Aig_ObjFanin1(pObj)? 1 + Aig_ObjIsExor(pObj) + AIG_MAX(Aig_ObjFanin0(pObj)->Level, Aig_ObjFanin1(pObj)->Level) : Aig_ObjFanin0(pObj)->Level; }
 static inline int          Aig_ObjFaninPhase( Aig_Obj_t * pObj )  { return pObj? Aig_Regular(pObj)->fPhase ^ Aig_IsComplement(pObj) : 0;                              }
 static inline void         Aig_ObjClean( Aig_Obj_t * pObj )       { memset( pObj, 0, sizeof(Aig_Obj_t) );                                                             }
@@ -277,6 +289,11 @@ static inline void Aig_ManRecycleMemory( Aig_Man_t * p, Aig_Obj_t * pEntry )
 // iterator over the nodes whose IDs are stored in the array
 #define Aig_ManForEachNodeVec( p, vIds, pObj, i )                               \
     for ( i = 0; i < Vec_IntSize(vIds) && ((pObj) = Aig_ManObj(p, Vec_IntEntry(vIds,i))); i++ )
+// iterator over the nodes in the topological order
+#define Aig_ManForEachNodeInOrder( p, pObj )                                    \
+    for ( assert(p->pOrderData), p->iPrev = 0, p->iNext = p->pOrderData[1];     \
+          p->iNext && (((pObj) = Aig_ManObj(p, p->iNext)), 1);                  \
+          p->iNext = p->pOrderData[2*p->iPrev+1] )
 
 // these two procedures are only here for the use inside the iterator
 static inline int     Aig_ObjFanout0Int( Aig_Man_t * p, int ObjId )  { assert(ObjId < p->nFansAlloc);  return p->pFanData[5*ObjId];                         }
@@ -296,22 +313,25 @@ extern int             Aig_ManCheck( Aig_Man_t * p );
 /*=== aigDfs.c ==========================================================*/
 extern Vec_Ptr_t *     Aig_ManDfs( 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_ManCountLevels( Aig_Man_t * p );
 extern int             Aig_DagSize( Aig_Obj_t * pObj );
 extern void            Aig_ConeUnmark_rec( Aig_Obj_t * pObj );
 extern Aig_Obj_t *     Aig_Transfer( Aig_Man_t * pSour, Aig_Man_t * pDest, Aig_Obj_t * pObj, int nVars );
 extern Aig_Obj_t *     Aig_Compose( Aig_Man_t * p, Aig_Obj_t * pRoot, Aig_Obj_t * pFunc, int iVar );
-extern void            Aig_ManCollectCut( Aig_Obj_t * pRoot, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vNodes );
+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 );
 /*=== 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 );
-extern void            Aig_ManCreateFanout( Aig_Man_t * p );
-extern void            Aig_ManDeleteFanout( Aig_Man_t * p );
+extern void            Aig_ManFanoutStart( Aig_Man_t * p );
+extern void            Aig_ManFanoutStop( Aig_Man_t * p );
 /*=== aigMan.c ==========================================================*/
-extern Aig_Man_t *     Aig_ManStart();
+extern Aig_Man_t *     Aig_ManStart( int nNodesMax );
 extern Aig_Man_t *     Aig_ManStartFrom( Aig_Man_t * p );
 extern Aig_Man_t *     Aig_ManDup( Aig_Man_t * p, int fOrdered );
+extern Aig_Man_t *     Aig_ManExtractMiter( Aig_Man_t * p, Aig_Obj_t ** ppNodes, int nNodes );
 extern void            Aig_ManStop( Aig_Man_t * p );
 extern int             Aig_ManCleanup( Aig_Man_t * p );
 extern void            Aig_ManPrintStats( Aig_Man_t * p );
@@ -345,9 +365,25 @@ extern Aig_Obj_t *     Aig_Exor( Aig_Man_t * p, Aig_Obj_t * p0, Aig_Obj_t * p1 )
 extern Aig_Obj_t *     Aig_Mux( Aig_Man_t * p, Aig_Obj_t * pC, Aig_Obj_t * p1, Aig_Obj_t * p0 );
 extern Aig_Obj_t *     Aig_Maj( Aig_Man_t * p, Aig_Obj_t * pA, Aig_Obj_t * pB, Aig_Obj_t * pC );
 extern Aig_Obj_t *     Aig_Miter( Aig_Man_t * p, Vec_Ptr_t * vPairs );
+extern Aig_Obj_t *     Aig_MiterTwo( Aig_Man_t * p, Vec_Ptr_t * vNodes1, Vec_Ptr_t * vNodes2 );
 extern Aig_Obj_t *     Aig_CreateAnd( Aig_Man_t * p, int nVars );
 extern Aig_Obj_t *     Aig_CreateOr( Aig_Man_t * p, int nVars );
 extern Aig_Obj_t *     Aig_CreateExor( Aig_Man_t * p, int nVars );
+/*=== aigOrder.c =========================================================*/
+extern void            Aig_ManOrderStart( Aig_Man_t * p );
+extern void            Aig_ManOrderStop( Aig_Man_t * p );
+extern void            Aig_ObjOrderInsert( Aig_Man_t * p, int ObjId );
+extern void            Aig_ObjOrderRemove( Aig_Man_t * p, int ObjId );
+extern void            Aig_ObjOrderAdvance( Aig_Man_t * p );
+/*=== aigPart.c =========================================================*/
+extern Vec_Vec_t *     Aig_ManSupports( Aig_Man_t * pMan );
+extern Vec_Vec_t *     Aig_ManPartitionSmart( Aig_Man_t * p, int nPartSizeLimit, int fVerbose, Vec_Vec_t ** pvPartSupps );
+extern Vec_Vec_t *     Aig_ManPartitionNaive( Aig_Man_t * p, int nPartSize );
+/*=== aigRepr.c =========================================================*/
+extern void            Aig_ManReprStart( Aig_Man_t * p, int nIdMax );
+extern void            Aig_ManReprStop( Aig_Man_t * p );
+extern void            Aig_ManTransferRepr( Aig_Man_t * pNew, Aig_Man_t * p );
+extern Aig_Man_t *     Aig_ManCreateChoices( Aig_Man_t * p );
 /*=== aigSeq.c ========================================================*/
 extern int             Aig_ManSeqStrash( Aig_Man_t * p, int nLatches, int * pInits );
 /*=== aigTable.c ========================================================*/
@@ -358,11 +394,14 @@ extern void            Aig_TableDelete( Aig_Man_t * p, Aig_Obj_t * pObj );
 extern int             Aig_TableCountEntries( Aig_Man_t * p );
 extern void            Aig_TableProfile( Aig_Man_t * p );
 /*=== aigTiming.c ========================================================*/
+extern void            Aig_ObjClearReverseLevel( Aig_Man_t * p, Aig_Obj_t * pObj );
 extern int             Aig_ObjRequiredLevel( Aig_Man_t * p, Aig_Obj_t * pObj );
 extern void            Aig_ManStartReverseLevels( Aig_Man_t * p, int nMaxLevelIncrease );
 extern void            Aig_ManStopReverseLevels( Aig_Man_t * p );
 extern void            Aig_ManUpdateLevel( Aig_Man_t * p, Aig_Obj_t * pObjNew );
 extern void            Aig_ManUpdateReverseLevel( Aig_Man_t * p, Aig_Obj_t * pObjNew );
+extern void            Aig_ManVerifyLevel( Aig_Man_t * p );
+extern void            Aig_ManVerifyReverseLevel( Aig_Man_t * p );
 /*=== aigTruth.c ========================================================*/
 extern unsigned *      Aig_ManCutTruth( Aig_Obj_t * pRoot, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vNodes, Vec_Ptr_t * vTruthElem, Vec_Ptr_t * vTruthStore );
 /*=== aigUtil.c =========================================================*/
@@ -370,6 +409,8 @@ extern unsigned        Aig_PrimeCudd( unsigned p );
 extern void            Aig_ManIncrementTravId( Aig_Man_t * p );
 extern int             Aig_ManLevels( Aig_Man_t * p );
 extern void            Aig_ManCheckMarkA( Aig_Man_t * p );
+extern void            Aig_ManCleanMarkA( Aig_Man_t * p );
+extern void            Aig_ManCleanMarkB( Aig_Man_t * p );
 extern void            Aig_ManCleanData( Aig_Man_t * p );
 extern void            Aig_ObjCleanData_rec( Aig_Obj_t * pObj );
 extern void            Aig_ObjCollectMulti( Aig_Obj_t * pFunc, Vec_Ptr_t * vSuper );
diff --git a/src/aig/aig/aigDfs.c b/src/aig/aig/aigDfs.c
index 62900bb5..a9d3d860 100644
--- a/src/aig/aig/aigDfs.c
+++ b/src/aig/aig/aigDfs.c
@@ -41,9 +41,9 @@
 ***********************************************************************/
 void Aig_ManDfs_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vNodes )
 {
-    assert( !Aig_IsComplement(pObj) );
     if ( pObj == NULL )
         return;
+    assert( !Aig_IsComplement(pObj) );
     if ( Aig_ObjIsTravIdCurrent(p, pObj) )
         return;
     assert( Aig_ObjIsNode(pObj) || Aig_ObjIsBuf(pObj) );
@@ -119,6 +119,62 @@ Vec_Ptr_t * Aig_ManDfsNodes( Aig_Man_t * p, Aig_Obj_t ** ppNodes, int nNodes )
 
 /**Function*************************************************************
 
+  Synopsis    [Collects internal nodes in the DFS order.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_ManDfsChoices_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vNodes )
+{
+    if ( pObj == NULL )
+        return;
+    assert( !Aig_IsComplement(pObj) );
+    if ( Aig_ObjIsTravIdCurrent(p, pObj) )
+        return;
+    assert( Aig_ObjIsNode(pObj) );
+    Aig_ManDfsChoices_rec( p, Aig_ObjFanin0(pObj), vNodes );
+    Aig_ManDfsChoices_rec( p, Aig_ObjFanin1(pObj), vNodes );
+    Aig_ManDfsChoices_rec( p, p->pReprs[pObj->Id], 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.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Aig_ManDfsChoices( Aig_Man_t * p )
+{
+    Vec_Ptr_t * vNodes;
+    Aig_Obj_t * pObj;
+    int i;
+    assert( p->pReprs != NULL );
+    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_ManForEachPo( p, pObj, i )
+        Aig_ManDfsChoices_rec( p, Aig_ObjFanin0(pObj), vNodes );
+    return vNodes;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Collects internal nodes in the reverse DFS order.]
 
   Description []
@@ -444,7 +500,7 @@ Aig_Obj_t * Aig_Compose( Aig_Man_t * p, Aig_Obj_t * pRoot, Aig_Obj_t * pFunc, in
   SeeAlso     []
 
 ***********************************************************************/
-void Aig_ManCollectCut_rec( Aig_Obj_t * pNode, Vec_Ptr_t * vNodes )
+void Aig_ObjCollectCut_rec( Aig_Obj_t * pNode, Vec_Ptr_t * vNodes )
 {
 //    Aig_Obj_t * pFan0 = Aig_ObjFanin0(pNode);
 //    Aig_Obj_t * pFan1 = Aig_ObjFanin1(pNode);
@@ -452,8 +508,8 @@ void Aig_ManCollectCut_rec( Aig_Obj_t * pNode, Vec_Ptr_t * vNodes )
         return;
     pNode->fMarkA = 1;
     assert( Aig_ObjIsNode(pNode) );
-    Aig_ManCollectCut_rec( Aig_ObjFanin0(pNode), vNodes );
-    Aig_ManCollectCut_rec( Aig_ObjFanin1(pNode), vNodes );
+    Aig_ObjCollectCut_rec( Aig_ObjFanin0(pNode), vNodes );
+    Aig_ObjCollectCut_rec( Aig_ObjFanin1(pNode), vNodes );
     Vec_PtrPush( vNodes, pNode );
 //printf( "added %d  ", pNode->Id );
 }
@@ -469,7 +525,7 @@ void Aig_ManCollectCut_rec( Aig_Obj_t * pNode, Vec_Ptr_t * vNodes )
   SeeAlso     []
 
 ***********************************************************************/
-void Aig_ManCollectCut( Aig_Obj_t * pRoot, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vNodes )
+void Aig_ObjCollectCut( Aig_Obj_t * pRoot, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vNodes )
 {
     Aig_Obj_t * pObj;
     int i;
@@ -483,7 +539,7 @@ void Aig_ManCollectCut( Aig_Obj_t * pRoot, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vNod
     }
 //printf( "\n" );
     // collect and mark the nodes
-    Aig_ManCollectCut_rec( pRoot, vNodes );
+    Aig_ObjCollectCut_rec( pRoot, vNodes );
     // clean the nodes
     Vec_PtrForEachEntry( vNodes, pObj, i )
         pObj->fMarkA = 0;
@@ -491,6 +547,83 @@ void Aig_ManCollectCut( Aig_Obj_t * pRoot, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vNod
         pObj->fMarkA = 0;
 }
 
+
+/**Function*************************************************************
+
+  Synopsis    [Collects the nodes of the supergate.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Aig_ObjCollectSuper_rec( Aig_Obj_t * pRoot, Aig_Obj_t * pObj, Vec_Ptr_t * vSuper )
+{
+    int RetValue1, RetValue2, i;
+    // check if the node is visited
+    if ( Aig_Regular(pObj)->fMarkA )
+    {
+        // check if the node occurs in the same polarity
+        for ( i = 0; i < vSuper->nSize; i++ )
+            if ( vSuper->pArray[i] == pObj )
+                return 1;
+        // check if the node is present in the opposite polarity
+        for ( i = 0; i < vSuper->nSize; i++ )
+            if ( vSuper->pArray[i] == Aig_Not(pObj) )
+                return -1;
+        assert( 0 );
+        return 0;
+    }
+    // if the new node is complemented or a PI, another gate begins
+    if ( pObj != pRoot && (Aig_IsComplement(pObj) || Aig_ObjType(pObj) != Aig_ObjType(pRoot) || Aig_ObjRefs(pObj) > 1) )
+    {
+        Vec_PtrPush( vSuper, pObj );
+        Aig_Regular(pObj)->fMarkA = 1;
+        return 0;
+    }
+    assert( !Aig_IsComplement(pObj) );
+    assert( Aig_ObjIsNode(pObj) );
+    // go through the branches
+    RetValue1 = Aig_ObjCollectSuper_rec( pRoot, Aig_ObjReal_rec( Aig_ObjChild0(pObj) ), vSuper );
+    RetValue2 = Aig_ObjCollectSuper_rec( pRoot, Aig_ObjReal_rec( Aig_ObjChild1(pObj) ), vSuper );
+    if ( RetValue1 == -1 || RetValue2 == -1 )
+        return -1;
+    // return 1 if at least one branch has a duplicate
+    return RetValue1 || RetValue2;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collects the nodes of the supergate.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Aig_ObjCollectSuper( Aig_Obj_t * pObj, Vec_Ptr_t * vSuper )
+{
+    int RetValue, i;
+    assert( !Aig_IsComplement(pObj) );
+    assert( Aig_ObjIsNode(pObj) );
+    // collect the nodes in the implication supergate
+    Vec_PtrClear( vSuper );
+    RetValue = Aig_ObjCollectSuper_rec( pObj, pObj, vSuper );
+    assert( Vec_PtrSize(vSuper) > 1 );
+    // unmark the visited nodes
+    Vec_PtrForEachEntry( vSuper, pObj, i )
+        Aig_Regular(pObj)->fMarkA = 0;
+    // if we found the node and its complement in the same implication supergate, 
+    // return empty set of nodes (meaning that we should use constant-0 node)
+    if ( RetValue == -1 )
+        vSuper->nSize = 0;
+    return RetValue;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/aig/aigFanout.c b/src/aig/aig/aigFanout.c
index e7d5f216..9aff0fd5 100644
--- a/src/aig/aig/aigFanout.c
+++ b/src/aig/aig/aigFanout.c
@@ -39,6 +39,56 @@ static inline int * Aig_FanoutNext( int * pData, int iFan )   { return pData + 5
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
+/**Function*************************************************************
+
+  Synopsis    [Create fanout for all objects in the manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_ManFanoutStart( Aig_Man_t * p )
+{
+    Aig_Obj_t * pObj;
+    int i;
+    assert( Aig_ManBufNum(p) == 0 );
+    // allocate fanout datastructure
+    assert( p->pFanData == NULL );
+    p->nFansAlloc = 2 * Aig_ManObjIdMax(p);
+    if ( p->nFansAlloc < (1<<12) )
+        p->nFansAlloc = (1<<12);
+    p->pFanData = ALLOC( int, 5 * p->nFansAlloc );
+    memset( p->pFanData, 0, sizeof(int) * 5 * p->nFansAlloc );
+    // add fanouts for all objects
+    Aig_ManForEachObj( p, pObj, i )
+    {
+        if ( Aig_ObjChild0(pObj) )
+            Aig_ObjAddFanout( p, Aig_ObjFanin0(pObj), pObj );
+        if ( Aig_ObjChild1(pObj) )
+            Aig_ObjAddFanout( p, Aig_ObjFanin1(pObj), pObj );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Deletes fanout for all objects in the manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_ManFanoutStop( Aig_Man_t * p )
+{
+    assert( p->pFanData != NULL );
+    FREE( p->pFanData );
+    p->nFansAlloc = 0;
+}
 
 /**Function*************************************************************
 
@@ -132,56 +182,6 @@ void Aig_ObjRemoveFanout( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pFanout )
     *pNextC = 0;
 }
 
-/**Function*************************************************************
-
-  Synopsis    [Create fanout for all objects in the manager.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Aig_ManCreateFanout( Aig_Man_t * p )
-{
-    Aig_Obj_t * pObj;
-    int i;
-    // allocate fanout datastructure
-    assert( p->pFanData == NULL );
-    p->nFansAlloc = 2 * Aig_ManObjIdMax(p);
-    if ( p->nFansAlloc < (1<<12) )
-        p->nFansAlloc = (1<<12);
-    p->pFanData = ALLOC( int, 5 * p->nFansAlloc );
-    memset( p->pFanData, 0, sizeof(int) * 5 * p->nFansAlloc );
-    // add fanouts for all objects
-    Aig_ManForEachObj( p, pObj, i )
-    {
-        if ( Aig_ObjChild0(pObj) )
-            Aig_ObjAddFanout( p, Aig_ObjFanin0(pObj), pObj );
-        if ( Aig_ObjChild1(pObj) )
-            Aig_ObjAddFanout( p, Aig_ObjFanin1(pObj), pObj );
-    }
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Deletes fanout for all objects in the manager.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Aig_ManDeleteFanout( Aig_Man_t * p )
-{
-    assert( p->pFanData != NULL );
-    FREE( p->pFanData );
-    p->nFansAlloc = 0;
-}
-
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/aig/aigMan.c b/src/aig/aig/aigMan.c
index 562260d3..b235119f 100644
--- a/src/aig/aig/aigMan.c
+++ b/src/aig/aig/aigMan.c
@@ -153,11 +153,15 @@ Aig_Man_t * Aig_ManDup( Aig_Man_t * p, int fOrdered )
     {
         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 )
         Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
+    assert( Aig_ManBufNum(p) != 0 || Aig_ManNodeNum(p) == Aig_ManNodeNum(pNew) );
     // check the resulting network
     if ( !Aig_ManCheck(pNew) )
         printf( "Aig_ManDup(): The check has failed.\n" );
@@ -166,6 +170,45 @@ Aig_Man_t * Aig_ManDup( Aig_Man_t * p, int fOrdered )
 
 /**Function*************************************************************
 
+  Synopsis    [Extracts the miter composed of XOR of the two nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Aig_ManExtractMiter( Aig_Man_t * p, Aig_Obj_t ** ppNodes, int nNodes )
+{
+    Aig_Man_t * pNew;
+    Aig_Obj_t * pObj;
+    int i;
+    assert( nNodes == 2 );
+    // create the new manager
+    pNew = Aig_ManStart( Aig_ManObjIdMax(p) + 1 );
+    // create the PIs
+    Aig_ManCleanData( p );
+    Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
+    Aig_ManForEachPi( p, pObj, i )
+        pObj->pData = Aig_ObjCreatePi(pNew);
+    // dump the nodes
+    for ( i = 0; i < nNodes; i++ )
+        Aig_ManDup_rec( pNew, p, ppNodes[i] );   
+    // construct the EXOR
+    pObj = Aig_Exor( pNew, ppNodes[0]->pData, ppNodes[1]->pData ); 
+    pObj = Aig_NotCond( pObj, Aig_Regular(pObj)->fPhase ^ Aig_IsComplement(pObj) );
+    // add the PO
+    Aig_ObjCreatePo( pNew, pObj );
+    // check the resulting network
+    if ( !Aig_ManCheck(pNew) )
+        printf( "Aig_ManDup(): The check has failed.\n" );
+    return pNew;
+}
+
+
+/**Function*************************************************************
+
   Synopsis    [Stops the AIG manager.]
 
   Description []
@@ -184,7 +227,7 @@ void Aig_ManStop( Aig_Man_t * p )
     if ( p->time2 ) { PRT( "time2", p->time2 ); }
     // delete fanout
     if ( p->pFanData ) 
-        Aig_ManDeleteFanout( p );
+        Aig_ManFanoutStop( p );
     // make sure the nodes have clean marks
     Aig_ManForEachObj( p, pObj, i )
         assert( !pObj->fMarkA && !pObj->fMarkB );
@@ -196,6 +239,7 @@ void Aig_ManStop( Aig_Man_t * p )
     if ( p->vBufs )    Vec_PtrFree( p->vBufs );
     if ( p->vLevelR )  Vec_IntFree( p->vLevelR );
     if ( p->vLevels )  Vec_VecFree( p->vLevels );
+    FREE( p->pReprs );
     free( p->pTable );
     free( p );
 }
diff --git a/src/aig/aig/aigObj.c b/src/aig/aig/aigObj.c
index f2296e01..a017ff2d 100644
--- a/src/aig/aig/aigObj.c
+++ b/src/aig/aig/aigObj.c
@@ -139,6 +139,9 @@ void Aig_ObjConnect( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pFan0, Aig_Obj
     // add the node to the structural hash table
     if ( Aig_ObjIsHash(pObj) )
         Aig_TableInsert( p, pObj );
+    // add the node to the dynamically updated topological order
+    if ( p->pOrderData && Aig_ObjIsNode(pObj) )
+        Aig_ObjOrderInsert( p, pObj->Id );
 }
 
 /**Function*************************************************************
@@ -174,6 +177,9 @@ void Aig_ObjDisconnect( Aig_Man_t * p, Aig_Obj_t * pObj )
     // add the first fanin
     pObj->pFanin0 = NULL;
     pObj->pFanin1 = NULL;
+    // remove the node from the dynamically updated topological order
+    if ( p->pOrderData && Aig_ObjIsNode(pObj) )
+        Aig_ObjOrderRemove( p, pObj->Id );
 }
 
 /**Function*************************************************************
@@ -243,6 +249,7 @@ void Aig_ObjPatchFanin0( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pFaninNew
 {
     Aig_Obj_t * pFaninOld;
     assert( !Aig_IsComplement(pObj) );
+    assert( Aig_ObjIsPo(pObj) );
     pFaninOld = Aig_ObjFanin0(pObj);
     // decrement ref and remove fanout
     if ( p->pFanData )
@@ -386,7 +393,10 @@ void Aig_ObjReplace( Aig_Man_t * p, Aig_Obj_t * pObjOld, Aig_Obj_t * pObjNew, in
             Aig_ManUpdateLevel( p, pObjOld );
         }
         if ( fUpdateLevel )
+        {
+            Aig_ObjClearReverseLevel( p, pObjOld );
             Aig_ManUpdateReverseLevel( p, pObjOld );
+        }
     }
     p->nObjs[pObjOld->Type]++;
     // store buffers if fanout is allocated
diff --git a/src/aig/aig/aigOper.c b/src/aig/aig/aigOper.c
index 55ab5862..d13d4bed 100644
--- a/src/aig/aig/aigOper.c
+++ b/src/aig/aig/aigOper.c
@@ -352,7 +352,6 @@ Aig_Obj_t * Aig_Miter( Aig_Man_t * p, Vec_Ptr_t * vPairs )
     int i;
     assert( vPairs->nSize > 0 );
     assert( vPairs->nSize % 2 == 0 );
-    // go through the cubes of the node's SOP
     for ( i = 0; i < vPairs->nSize; i += 2 )
         vPairs->pArray[i/2] = Aig_Not( Aig_Exor( p, vPairs->pArray[i], vPairs->pArray[i+1] ) );
     vPairs->nSize = vPairs->nSize/2;
@@ -361,6 +360,27 @@ Aig_Obj_t * Aig_Miter( Aig_Man_t * p, Vec_Ptr_t * vPairs )
 
 /**Function*************************************************************
 
+  Synopsis    [Implements the miter.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Obj_t * Aig_MiterTwo( Aig_Man_t * p, Vec_Ptr_t * vNodes1, Vec_Ptr_t * vNodes2 )
+{
+    int i;
+    assert( vNodes1->nSize > 0 && vNodes1->nSize > 0 );
+    assert( vNodes1->nSize == vNodes2->nSize );
+    for ( i = 0; i < vNodes1->nSize; i++ )
+        vNodes1->pArray[i] = Aig_Not( Aig_Exor( p, vNodes1->pArray[i], vNodes2->pArray[i] ) );
+    return Aig_Not( Aig_Multi_rec( p, (Aig_Obj_t **)vNodes1->pArray, vNodes1->nSize, AIG_OBJ_AND ) );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Creates AND function with nVars inputs.]
 
   Description []
diff --git a/src/aig/aig/aigOrder.c b/src/aig/aig/aigOrder.c
new file mode 100644
index 00000000..8aef67c8
--- /dev/null
+++ b/src/aig/aig/aigOrder.c
@@ -0,0 +1,171 @@
+/**CFile****************************************************************
+
+  FileName    [aigOrder.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [AIG package.]
+
+  Synopsis    [Dynamically updated topological order.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - April 28, 2007.]
+
+  Revision    [$Id: aigOrder.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "aig.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Initializes the order datastructure.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_ManOrderStart( Aig_Man_t * p )
+{
+    Aig_Obj_t * pObj;
+    int i;
+    assert( Aig_ManBufNum(p) == 0 );
+    // allocate order datastructure
+    assert( p->pOrderData == NULL );
+    p->nOrderAlloc = 2 * Aig_ManObjIdMax(p);
+    if ( p->nOrderAlloc < (1<<12) )
+        p->nOrderAlloc = (1<<12);
+    p->pOrderData = ALLOC( unsigned, 2 * p->nOrderAlloc );
+    memset( p->pOrderData, 0xFF, sizeof(unsigned) * 2 * p->nOrderAlloc );
+    // add the constant node
+    p->pOrderData[0] = p->pOrderData[1] = 0;
+    p->iPrev = p->iNext = 0;
+    // add the internal nodes
+    Aig_ManForEachNode( p, pObj, i )
+        Aig_ObjOrderInsert( p, pObj->Id );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Deletes the order datastructure.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_ManOrderStop( Aig_Man_t * p )
+{
+    assert( p->pOrderData );
+    FREE( p->pOrderData );
+    p->nOrderAlloc = 0;
+    p->iPrev = p->iNext = 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Inserts an entry before iNext.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_ObjOrderInsert( Aig_Man_t * p, int ObjId )
+{
+    int iPrev;
+    assert( ObjId != 0 );
+    assert( Aig_ObjIsNode( Aig_ManObj(p, ObjId) ) );
+    if ( ObjId >= p->nOrderAlloc )
+    {
+        int nOrderAlloc = 2 * ObjId; 
+        p->pOrderData = REALLOC( unsigned, p->pOrderData, 2 * nOrderAlloc );
+        memset( p->pOrderData + 2 * p->nOrderAlloc, 0xFF, sizeof(unsigned) * 2 * (nOrderAlloc - p->nOrderAlloc) );
+        p->nOrderAlloc = nOrderAlloc;
+    }
+    assert( p->pOrderData[2*ObjId] == 0xFFFFFFFF );   // prev
+    assert( p->pOrderData[2*ObjId+1] == 0xFFFFFFFF ); // next
+    iPrev = p->pOrderData[2*p->iNext];
+    assert( p->pOrderData[2*iPrev+1] == (unsigned)p->iNext );
+    p->pOrderData[2*ObjId] = iPrev;
+    p->pOrderData[2*iPrev+1] = ObjId;
+    p->pOrderData[2*p->iNext] = ObjId;
+    p->pOrderData[2*ObjId+1] = p->iNext;
+    p->nAndTotal++;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Removes the entry.]
+
+  Description [If iPrev is removed, it slides backward. 
+  If iNext is removed, it slides forward.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_ObjOrderRemove( Aig_Man_t * p, int ObjId )
+{
+    int iPrev, iNext;
+    assert( ObjId != 0 );
+    assert( Aig_ObjIsNode( Aig_ManObj(p, ObjId) ) );
+    iPrev = p->pOrderData[2*ObjId];
+    iNext = p->pOrderData[2*ObjId+1];
+    p->pOrderData[2*ObjId] = 0xFFFFFFFF;
+    p->pOrderData[2*ObjId+1] = 0xFFFFFFFF;
+    p->pOrderData[2*iNext] = iPrev;
+    p->pOrderData[2*iPrev+1] = iNext;
+    if ( p->iPrev == ObjId )
+    {
+        p->nAndPrev--;
+        p->iPrev = iPrev;
+    }
+    if ( p->iNext == ObjId )
+        p->iNext = iNext;
+    p->nAndTotal--;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Advances the order forward.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_ObjOrderAdvance( Aig_Man_t * p )
+{
+    assert( p->pOrderData );
+    assert( p->pOrderData[2*p->iPrev+1] == (unsigned)p->iNext );
+    p->iPrev = p->iNext;
+    p->nAndPrev++;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/aig/aigPart.c b/src/aig/aig/aigPart.c
new file mode 100644
index 00000000..371e8773
--- /dev/null
+++ b/src/aig/aig/aigPart.c
@@ -0,0 +1,928 @@
+/**CFile****************************************************************
+
+  FileName    [aigPart.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [AIG package.]
+
+  Synopsis    [AIG partitioning package.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - April 28, 2007.]
+
+  Revision    [$Id: aigPart.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "aig.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Part_Man_t_     Part_Man_t;
+struct Part_Man_t_
+{
+    int              nChunkSize;    // the size of one chunk of memory (~1 Mb)
+    int              nStepSize;     // the step size in saving memory (~64 bytes)
+    char *           pFreeBuf;      // the pointer to free memory
+    int              nFreeSize;     // the size of remaining free memory
+    Vec_Ptr_t *      vMemory;       // the memory allocated
+    Vec_Ptr_t *      vFree;         // the vector of free pieces of memory
+};
+
+typedef struct Part_One_t_     Part_One_t;
+struct Part_One_t_
+{
+    int              nRefs;         // the number of references
+    int              nOuts;         // the number of outputs
+    int              nOutsAlloc;    // the array size
+    int              pOuts[0];      // the array of outputs
+};
+
+static inline int    Part_SizeType( int nSize, int nStepSize )     { return nSize / nStepSize + ((nSize % nStepSize) > 0); }
+static inline char * Part_OneNext( char * pPart )                  { return *((char **)pPart);                             }
+static inline void   Part_OneSetNext( char * pPart, char * pNext ) { *((char **)pPart) = pNext;                            }
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Start the memory manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Part_Man_t * Part_ManStart( int nChunkSize, int nStepSize )
+{
+    Part_Man_t * p;
+    p = ALLOC( Part_Man_t, 1 );
+    memset( p, 0, sizeof(Part_Man_t) );
+    p->nChunkSize = nChunkSize;
+    p->nStepSize  = nStepSize;
+    p->vMemory    = Vec_PtrAlloc( 1000 );
+    p->vFree      = Vec_PtrAlloc( 1000 );
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Stops the memory manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Part_ManStop( Part_Man_t * p )
+{
+    void * pMemory;
+    int i;
+    Vec_PtrForEachEntry( p->vMemory, pMemory, i )
+        free( pMemory );
+    Vec_PtrFree( p->vMemory );
+    Vec_PtrFree( p->vFree );
+    free( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Fetches the memory entry of the given size.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+char * Part_ManFetch( Part_Man_t * p, int nSize )
+{
+    int Type, nSizeReal;
+    char * pMemory;
+    assert( nSize > 0 );
+    Type = Part_SizeType( nSize, p->nStepSize );
+    Vec_PtrFillExtra( p->vFree, Type + 1, NULL );
+    if ( pMemory = Vec_PtrEntry( p->vFree, Type ) )
+    {
+        Vec_PtrWriteEntry( p->vFree, Type, Part_OneNext(pMemory) );
+        return pMemory;
+    }
+    nSizeReal = p->nStepSize * Type;
+    if ( p->nFreeSize < nSizeReal )
+    {
+        p->pFreeBuf = ALLOC( char, p->nChunkSize );
+        p->nFreeSize = p->nChunkSize;
+        Vec_PtrPush( p->vMemory, p->pFreeBuf );
+    }
+    assert( p->nFreeSize >= nSizeReal );
+    pMemory = p->pFreeBuf;
+    p->pFreeBuf  += nSizeReal;
+    p->nFreeSize -= nSizeReal;
+    return pMemory;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Recycles the memory entry of the given size.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Part_ManRecycle( Part_Man_t * p, char * pMemory, int nSize )
+{
+    int Type;
+    Type = Part_SizeType( nSize, p->nStepSize );
+    Vec_PtrFillExtra( p->vFree, Type + 1, NULL );
+    Part_OneSetNext( pMemory, Vec_PtrEntry(p->vFree, Type) );
+    Vec_PtrWriteEntry( p->vFree, Type, pMemory );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Fetches the memory entry of the given size.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline Part_One_t * Part_ManFetchEntry( Part_Man_t * p, int nWords, int nRefs )
+{
+    Part_One_t * pPart;
+    pPart = (Part_One_t *)Part_ManFetch( p, sizeof(Part_One_t) + sizeof(int) * nWords );
+    pPart->nRefs = nRefs;
+    pPart->nOuts = 0;
+    pPart->nOutsAlloc = nWords;
+    return pPart;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Recycles the memory entry of the given size.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Part_ManRecycleEntry( Part_Man_t * p, Part_One_t * pEntry )
+{
+    assert( pEntry->nOuts <= pEntry->nOutsAlloc );
+    assert( pEntry->nOuts >= pEntry->nOutsAlloc/2 );
+    Part_ManRecycle( p, (char *)pEntry, sizeof(Part_One_t) + sizeof(int) * pEntry->nOutsAlloc );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Merges two entries.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Part_One_t * Part_ManMergeEntry( Part_Man_t * pMan, Part_One_t * p1, Part_One_t * p2, int nRefs )
+{
+    Part_One_t * p = Part_ManFetchEntry( pMan, p1->nOuts + p2->nOuts, nRefs );
+    int * pBeg1 = p1->pOuts;
+    int * pBeg2 = p2->pOuts;
+    int * pBeg  = p->pOuts;
+    int * pEnd1 = p1->pOuts + p1->nOuts;
+    int * pEnd2 = p2->pOuts + p2->nOuts;
+    while ( pBeg1 < pEnd1 && pBeg2 < pEnd2 )
+    {
+        if ( *pBeg1 == *pBeg2 )
+            *pBeg++ = *pBeg1++, pBeg2++;
+        else if ( *pBeg1 < *pBeg2 )
+            *pBeg++ = *pBeg1++;
+        else 
+            *pBeg++ = *pBeg2++;
+    }
+    while ( pBeg1 < pEnd1 )
+        *pBeg++ = *pBeg1++;
+    while ( pBeg2 < pEnd2 )
+        *pBeg++ = *pBeg2++;
+    p->nOuts = pBeg - p->pOuts;
+    assert( p->nOuts <= p->nOutsAlloc );
+    assert( p->nOuts >= p1->nOuts );
+    assert( p->nOuts >= p2->nOuts );
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Tranfers the entry.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Part_ManTransferEntry( Part_One_t * p )
+{
+    Vec_Int_t * vSupp;
+    int i;
+    vSupp = Vec_IntAlloc( p->nOuts );
+    for ( i = 0; i < p->nOuts; i++ )
+        Vec_IntPush( vSupp, p->pOuts[i] );
+    return vSupp;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes supports of the POs in the multi-output AIG.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Vec_t * Aig_ManSupports( Aig_Man_t * pMan )
+{
+    Vec_Vec_t * vSupps;
+    Vec_Int_t * vSupp;
+    Part_Man_t * p;
+    Part_One_t * pPart0, * pPart1;
+    Aig_Obj_t * pObj;
+    int i, iIns = 0, iOut = 0;
+    // start the support computation manager
+    p = Part_ManStart( 1 << 20, 1 << 6 );
+    // consider objects in the topological order
+    vSupps = Vec_VecAlloc( Aig_ManPoNum(pMan) );
+    Aig_ManCleanData(pMan);
+    Aig_ManForEachObj( pMan, pObj, i )
+    {
+        if ( Aig_ObjIsNode(pObj) )
+        {
+            pPart0 = Aig_ObjFanin0(pObj)->pData;
+            pPart1 = Aig_ObjFanin1(pObj)->pData;
+            pObj->pData = Part_ManMergeEntry( p, pPart0, pPart1, pObj->nRefs );
+            assert( pPart0->nRefs > 0 );
+            if ( --pPart0->nRefs == 0 )
+                Part_ManRecycleEntry( p, pPart0 );
+            assert( pPart1->nRefs > 0 );
+            if ( --pPart1->nRefs == 0 )
+                Part_ManRecycleEntry( p, pPart1 );
+            continue;
+        }
+        if ( Aig_ObjIsPo(pObj) )
+        {
+            pPart0 = Aig_ObjFanin0(pObj)->pData;
+            vSupp = Part_ManTransferEntry(pPart0);
+            Vec_IntPush( vSupp, iOut++ );
+            Vec_PtrPush( (Vec_Ptr_t *)vSupps, vSupp );
+            assert( pPart0->nRefs > 0 );
+            if ( --pPart0->nRefs == 0 )
+                Part_ManRecycleEntry( p, pPart0 );
+            continue;
+        }
+        if ( Aig_ObjIsPi(pObj) )
+        {
+            if ( pObj->nRefs )
+            {
+                pPart0 = Part_ManFetchEntry( p, 1, pObj->nRefs );
+                pPart0->pOuts[ pPart0->nOuts++ ] = iIns++;
+                pObj->pData = pPart0;
+            }
+            continue;
+        }
+        if ( Aig_ObjIsConst1(pObj) )
+        {
+            if ( pObj->nRefs )
+                pObj->pData = Part_ManFetchEntry( p, 0, pObj->nRefs );
+            continue;
+        }
+        assert( 0 );
+    }
+printf( "Memory usage = %d Mb.\n", Vec_PtrSize(p->vMemory) * p->nChunkSize / (1<<20) );
+    Part_ManStop( p );
+    // sort supports by size
+    Vec_VecSort( vSupps, 1 );
+/*
+    Aig_ManForEachPo( pMan, pObj, i )
+        printf( "%d ", Vec_IntSize( (Vec_Int_t *)Vec_VecEntry(vSupps, i) ) );
+    printf( "\n" );
+*/
+    return vSupps;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Start char-bases support representation.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+char * Aig_ManSuppCharStart( Vec_Int_t * vOne, int nPis )
+{
+    char * pBuffer;
+    int i, Entry;
+    pBuffer = ALLOC( char, nPis );
+    memset( pBuffer, 0, sizeof(char) * nPis );
+    Vec_IntForEachEntry( vOne, Entry, i )
+    {
+        assert( Entry < nPis );
+        pBuffer[Entry] = 1;
+    }
+    return pBuffer;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Add to char-bases support representation.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_ManSuppCharAdd( char * pBuffer, Vec_Int_t * vOne, int nPis )
+{
+    int i, Entry;
+    Vec_IntForEachEntry( vOne, Entry, i )
+    {
+        assert( Entry < nPis );
+        pBuffer[Entry] = 1;
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Find the common variables using char-bases support representation.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Aig_ManSuppCharCommon( char * pBuffer, Vec_Int_t * vOne )
+{
+    int i, Entry, nCommon = 0;
+    Vec_IntForEachEntry( vOne, Entry, i )
+        nCommon += pBuffer[Entry];
+    return nCommon;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Find the best partition.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Aig_ManPartitionSmartFindPart( Vec_Ptr_t * vPartSuppsAll, Vec_Ptr_t * vPartsAll, Vec_Ptr_t * vPartSuppsChar, int nPartSizeLimit, Vec_Int_t * vOne )
+{
+    Vec_Int_t * vPartSupp, * vPart;
+    int Attract, Repulse, Value, ValueBest;
+    int i, nCommon, iBest;
+    iBest = -1;
+    ValueBest = 0;
+    Vec_PtrForEachEntry( vPartSuppsAll, vPartSupp, i )
+    {
+        vPart = Vec_PtrEntry( vPartsAll, i );
+        if ( nPartSizeLimit > 0 && Vec_IntSize(vPart) >= nPartSizeLimit )
+            continue;
+//        nCommon = Vec_IntTwoCountCommon( vPartSupp, vOne );
+        nCommon = Aig_ManSuppCharCommon( Vec_PtrEntry(vPartSuppsChar, i), vOne );
+        if ( nCommon == 0 )
+            continue;
+        if ( nCommon == Vec_IntSize(vOne) )
+            return i;
+        Attract = 1000 * nCommon / Vec_IntSize(vOne);
+        if ( Vec_IntSize(vPartSupp) < 100 )
+            Repulse = 1;
+        else
+            Repulse = 1+Extra_Base2Log(Vec_IntSize(vPartSupp)-100);
+        Value = Attract/Repulse;
+        if ( ValueBest < Value )
+        {
+            ValueBest = Value;
+            iBest = i;
+        }
+    }
+    if ( ValueBest < 75 )
+        return -1;
+    return iBest;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Perform the smart partitioning.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_ManPartitionPrint( Aig_Man_t * p, Vec_Ptr_t * vPartsAll, Vec_Ptr_t * vPartSuppsAll )
+{
+    Vec_Int_t * vOne;
+    int i, nOutputs, Counter;
+
+    Counter = 0;
+    Vec_PtrForEachEntry( vPartSuppsAll, vOne, i )
+    {
+        nOutputs = Vec_IntSize(Vec_PtrEntry(vPartsAll, i));
+        printf( "%d=(%d,%d) ", i, Vec_IntSize(vOne), nOutputs );
+        Counter += nOutputs;
+        if ( i == Vec_PtrSize(vPartsAll) - 1 )
+            break;
+    }
+    assert( Counter == Aig_ManPoNum(p) );
+    printf( "\nTotal = %d. Outputs = %d.\n", Counter, Aig_ManPoNum(p) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Perform the smart partitioning.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_ManPartitionCompact( Vec_Ptr_t * vPartsAll, Vec_Ptr_t * vPartSuppsAll, int nPartSizeLimit )
+{
+    Vec_Int_t * vOne, * vPart, * vPartSupp, * vTemp;
+    int i, iPart;
+
+    if ( nPartSizeLimit == 0 )
+        nPartSizeLimit = 200;
+
+    // pack smaller partitions into larger blocks
+    iPart = 0;
+    vPart = vPartSupp = NULL;
+    Vec_PtrForEachEntry( vPartSuppsAll, vOne, i )
+    {
+        if ( Vec_IntSize(vOne) < nPartSizeLimit )
+        {
+            if ( vPartSupp == NULL )
+            {
+                assert( vPart == NULL );
+                vPartSupp = Vec_IntDup(vOne);
+                vPart = Vec_PtrEntry(vPartsAll, i);
+            }
+            else
+            {
+                vPartSupp = Vec_IntTwoMerge( vTemp = vPartSupp, vOne );
+                Vec_IntFree( vTemp );
+                vPart = Vec_IntTwoMerge( vTemp = vPart, Vec_PtrEntry(vPartsAll, i) );
+                Vec_IntFree( vTemp );
+                Vec_IntFree( Vec_PtrEntry(vPartsAll, i) );
+            }
+            if ( Vec_IntSize(vPartSupp) < nPartSizeLimit )
+                continue;
+        }
+        else
+            vPart = Vec_PtrEntry(vPartsAll, i);
+        // add the partition 
+        Vec_PtrWriteEntry( vPartsAll, iPart, vPart );  
+        vPart = NULL;
+        if ( vPartSupp ) 
+        {
+            Vec_IntFree( Vec_PtrEntry(vPartSuppsAll, iPart) );
+            Vec_PtrWriteEntry( vPartSuppsAll, iPart, vPartSupp );  
+            vPartSupp = NULL;
+        }
+        iPart++;
+    }
+    // add the last one
+    if ( vPart )
+    {
+        Vec_PtrWriteEntry( vPartsAll, iPart, vPart );  
+        vPart = NULL;
+
+        assert( vPartSupp != NULL );
+        Vec_IntFree( Vec_PtrEntry(vPartSuppsAll, iPart) );
+        Vec_PtrWriteEntry( vPartSuppsAll, iPart, vPartSupp );  
+        vPartSupp = NULL;
+        iPart++;
+    }
+    Vec_PtrShrink( vPartsAll, iPart );
+    Vec_PtrShrink( vPartsAll, iPart );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Perform the smart partitioning.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Vec_t * Aig_ManPartitionSmart( Aig_Man_t * p, int nPartSizeLimit, int fVerbose, Vec_Vec_t ** pvPartSupps )
+{
+    Vec_Ptr_t * vPartSuppsChar;
+    Vec_Ptr_t * vSupps, * vPartsAll, * vPartsAll2, * vPartSuppsAll;//, * vPartPtr;
+    Vec_Int_t * vOne, * vPart, * vPartSupp, * vTemp;
+    int i, iPart, iOut, clk;
+
+    // compute the supports for all outputs
+clk = clock();
+    vSupps = (Vec_Ptr_t *)Aig_ManSupports( p );
+if ( fVerbose )
+{
+PRT( "Supps", clock() - clk );
+}
+    // start char-based support representation
+    vPartSuppsChar = Vec_PtrAlloc( 1000 );
+
+    // create partitions
+clk = clock();
+    vPartsAll = Vec_PtrAlloc( 256 );
+    vPartSuppsAll = Vec_PtrAlloc( 256 );
+    Vec_PtrForEachEntry( vSupps, vOne, i )
+    {
+        // get the output number
+        iOut = Vec_IntPop(vOne);
+        // find closely matching part
+        iPart = Aig_ManPartitionSmartFindPart( vPartSuppsAll, vPartsAll, vPartSuppsChar, nPartSizeLimit, vOne );
+//printf( "%4d->%4d  ", i, iPart );
+        if ( iPart == -1 )
+        {
+            // create new partition
+            vPart = Vec_IntAlloc( 32 );
+            Vec_IntPush( vPart, iOut );
+            // create new partition support
+            vPartSupp = Vec_IntDup( vOne );
+            // add this partition and its support
+            Vec_PtrPush( vPartsAll, vPart );
+            Vec_PtrPush( vPartSuppsAll, vPartSupp );
+
+            Vec_PtrPush( vPartSuppsChar, Aig_ManSuppCharStart(vOne, Aig_ManPiNum(p)) );
+        }
+        else
+        {
+            // add output to this partition
+            vPart = Vec_PtrEntry( vPartsAll, iPart );
+            Vec_IntPush( vPart, iOut );
+            // merge supports
+            vPartSupp = Vec_PtrEntry( vPartSuppsAll, iPart );
+            vPartSupp = Vec_IntTwoMerge( vTemp = vPartSupp, vOne );
+            Vec_IntFree( vTemp );
+            // reinsert new support
+            Vec_PtrWriteEntry( vPartSuppsAll, iPart, vPartSupp );
+
+            Aig_ManSuppCharAdd( Vec_PtrEntry(vPartSuppsChar, iPart), vOne, Aig_ManPiNum(p) );
+        }
+    }
+
+    // stop char-based support representation
+    Vec_PtrForEachEntry( vPartSuppsChar, vTemp, i )
+        free( vTemp );
+    Vec_PtrFree( vPartSuppsChar );
+
+//printf( "\n" );
+if ( fVerbose )
+{
+PRT( "Parts", clock() - clk );
+}
+
+clk = clock();
+    // reorder partitions in the decreasing order of support sizes
+    // remember partition number in each partition support
+    Vec_PtrForEachEntry( vPartSuppsAll, vOne, i )
+        Vec_IntPush( vOne, i );
+    // sort the supports in the decreasing order
+    Vec_VecSort( (Vec_Vec_t *)vPartSuppsAll, 1 );
+    // reproduce partitions
+    vPartsAll2 = Vec_PtrAlloc( 256 );
+    Vec_PtrForEachEntry( vPartSuppsAll, vOne, i )
+        Vec_PtrPush( vPartsAll2, Vec_PtrEntry(vPartsAll, Vec_IntPop(vOne)) );
+    Vec_PtrFree( vPartsAll );
+    vPartsAll = vPartsAll2;
+
+    // compact small partitions
+//    Aig_ManPartitionPrint( p, vPartsAll, vPartSuppsAll );
+    Aig_ManPartitionCompact( vPartsAll, vPartSuppsAll, nPartSizeLimit );
+    if ( fVerbose )
+//    Aig_ManPartitionPrint( p, vPartsAll, vPartSuppsAll );
+    printf( "Created %d partitions.\n", Vec_PtrSize(vPartsAll) );
+
+if ( fVerbose )
+{
+//PRT( "Comps", clock() - clk );
+}
+
+    // cleanup
+    Vec_VecFree( (Vec_Vec_t *)vSupps );
+    if ( pvPartSupps == NULL )
+        Vec_VecFree( (Vec_Vec_t *)vPartSuppsAll );
+    else
+        *pvPartSupps = (Vec_Vec_t *)vPartSuppsAll;
+/*
+    // converts from intergers to nodes
+    Vec_PtrForEachEntry( vPartsAll, vPart, iPart )
+    {
+        vPartPtr = Vec_PtrAlloc( Vec_IntSize(vPart) );
+        Vec_IntForEachEntry( vPart, iOut, i )
+            Vec_PtrPush( vPartPtr, Aig_ManPo(p, iOut) );
+        Vec_IntFree( vPart );
+        Vec_PtrWriteEntry( vPartsAll, iPart, vPartPtr );
+    }
+*/
+    return (Vec_Vec_t *)vPartsAll;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Perform the naive partitioning.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Vec_t * Aig_ManPartitionNaive( Aig_Man_t * p, int nPartSize )
+{
+    Vec_Vec_t * vParts;
+    Aig_Obj_t * pObj;
+    int nParts, i;
+    nParts = (Aig_ManPoNum(p) / nPartSize) + ((Aig_ManPoNum(p) % nPartSize) > 0);
+    vParts = Vec_VecStart( nParts );
+    Aig_ManForEachPo( p, pObj, i )
+        Vec_VecPush( vParts, i / nPartSize, pObj );
+    return vParts;
+}
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Adds internal nodes in the topological order.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Obj_t * Aig_ManDupPart_rec( Aig_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t * pObj )
+{
+    assert( !Aig_IsComplement(pObj) );
+    if ( Aig_ObjIsTravIdCurrent(p, pObj) )
+        return pObj->pData;
+    assert( Aig_ObjIsNode(pObj) );
+    Aig_ManDupPart_rec( pNew, p, Aig_ObjFanin0(pObj) );
+    Aig_ManDupPart_rec( pNew, p, Aig_ObjFanin1(pObj) );
+    pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
+    assert( !Aig_ObjIsTravIdCurrent(p, pObj) ); // loop detection
+    Aig_ObjSetTravIdCurrent(p, pObj);
+    return pObj->pData;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Adds internal nodes in the topological order.]
+
+  Description [Returns the array of new outputs.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Aig_ManDupPart( Aig_Man_t * pNew, Aig_Man_t * p, Vec_Int_t * vPart, Vec_Int_t * vPartSupp, int fInverse )
+{
+    Vec_Ptr_t * vOutputs;
+    Aig_Obj_t * pObj, * pObjNew;
+    int Entry, k;
+    // create the PIs
+    Aig_ManIncrementTravId( p );
+    Aig_ObjSetTravIdCurrent( p, Aig_ManConst1(p) );
+    Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
+    if ( !fInverse )
+    {
+        Vec_IntForEachEntry( vPartSupp, Entry, k )
+        {
+            pObj = Aig_ManPi( p, Entry );
+            pObj->pData = Aig_ManPi( pNew, k );
+            Aig_ObjSetTravIdCurrent( p, pObj );
+        }
+    }
+    else
+    {
+        Vec_IntForEachEntry( vPartSupp, Entry, k )
+        {
+            pObj = Aig_ManPi( p, k );
+            pObj->pData = Aig_ManPi( pNew, Entry );
+            Aig_ObjSetTravIdCurrent( p, pObj );
+        }
+    }
+    // create the internal nodes
+    vOutputs = Vec_PtrAlloc( Vec_IntSize(vPart) );
+    Vec_IntForEachEntry( vPart, Entry, k )
+    {
+        pObj = Aig_ManPo( p, Entry );
+        pObjNew = Aig_ManDupPart_rec( pNew, p, Aig_ObjFanin0(pObj) );
+        pObjNew = Aig_NotCond( pObjNew, Aig_ObjFaninC0(pObj) );
+        Vec_PtrPush( vOutputs, pObjNew );
+    }
+    return vOutputs; 
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Create partitioned miter of the two AIGs.]
+
+  Description [Assumes that each output in the second AIG cannot have 
+  more supp vars than the same output in the first AIG.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Aig_ManMiterPartitioned( Aig_Man_t * p1, Aig_Man_t * p2, int nPartSize )
+{
+    Aig_Man_t * pNew;
+    Aig_Obj_t * pMiter;
+    Vec_Ptr_t * vMiters, * vNodes1, * vNodes2;
+    Vec_Vec_t * vParts, * vPartSupps;
+    Vec_Int_t * vPart, * vPartSupp;
+    int i, k;
+    // partition the first manager
+    vParts = Aig_ManPartitionSmart( p1, nPartSize, 0, &vPartSupps );
+    // derive miters
+    vMiters = Vec_PtrAlloc( Vec_VecSize(vParts) );
+    for ( i = 0; i < Vec_VecSize(vParts); i++ )
+    {
+        // get partitions and their support
+        vPart     = Vec_PtrEntry( (Vec_Ptr_t *)vParts, i );
+        vPartSupp = Vec_PtrEntry( (Vec_Ptr_t *)vPartSupps, i );
+        // create the new miter
+        pNew = Aig_ManStart( 1000 );
+        // create the PIs
+        for ( k = 0; k < Vec_IntSize(vPartSupp); k++ )
+            Aig_ObjCreatePi( pNew );
+        // copy the components
+        vNodes1 = Aig_ManDupPart( pNew, p1, vPart, vPartSupp, 0 );
+        vNodes2 = Aig_ManDupPart( pNew, p2, vPart, vPartSupp, 0 );
+        // create the miter
+        pMiter = Aig_MiterTwo( pNew, vNodes1, vNodes2 );
+        // create the output
+        Aig_ObjCreatePo( pNew, pMiter );
+        // clean up
+        Aig_ManCleanup( pNew );
+        Vec_PtrPush( vMiters, pNew );
+    }
+    Vec_VecFree( vParts );
+    Vec_VecFree( vPartSupps );
+    return vMiters;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs partitioned choice computation.]
+
+  Description [Assumes that each output in the second AIG cannot have 
+  more supp vars than the same output in the first AIG.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Aig_ManChoicePartitioned( Vec_Ptr_t * vAigs, int nPartSize )
+{
+    Aig_Man_t * pChoice, * pNew, * pAig, * p;
+    Aig_Obj_t * pObj;
+    Vec_Ptr_t * vMiters, * vNodes;
+    Vec_Vec_t * vParts, * vPartSupps;
+    Vec_Int_t * vPart, * vPartSupp;
+    int i, k, m;
+
+    // partition the first AIG
+    assert( Vec_PtrSize(vAigs) > 1 );
+    pAig = Vec_PtrEntry( vAigs, 0 );
+    vParts = Aig_ManPartitionSmart( pAig, nPartSize, 0, &vPartSupps );
+
+    // derive the AIG partitions
+    vMiters = Vec_PtrAlloc( Vec_VecSize(vParts) );
+    for ( i = 0; i < Vec_VecSize(vParts); i++ )
+    {
+        // get partitions and their support
+        vPart     = Vec_PtrEntry( (Vec_Ptr_t *)vParts, i );
+        vPartSupp = Vec_PtrEntry( (Vec_Ptr_t *)vPartSupps, i );
+        // create the new miter
+        pNew = Aig_ManStart( 1000 );
+        // create the PIs
+        for ( k = 0; k < Vec_IntSize(vPartSupp); k++ )
+            Aig_ObjCreatePi( pNew );
+        // copy the components
+        Vec_PtrForEachEntry( vAigs, p, k )
+        {
+            vNodes = Aig_ManDupPart( pNew, p, vPart, vPartSupp, 0 );
+            Vec_PtrForEachEntry( vNodes, pObj, m )
+                Aig_ObjCreatePo( pNew, pObj );
+            Vec_PtrFree( vNodes );
+        }
+        // add to the partitions
+        Vec_PtrPush( vMiters, pNew );
+    }
+
+    // perform choicing for each derived AIG
+    Vec_PtrForEachEntry( vMiters, pNew, i )
+    {
+        extern Aig_Man_t * Fra_Choice( Aig_Man_t * pManAig );
+        pNew = Fra_Choice( p = pNew );
+        Vec_PtrWriteEntry( vMiters, i, pNew );
+        Aig_ManStop( p );
+    }
+
+    // combine the resulting AIGs
+    pNew = Aig_ManStartFrom( pAig );
+    Vec_PtrForEachEntry( vMiters, p, i )
+    {
+        // get partitions and their support
+        vPart     = Vec_PtrEntry( (Vec_Ptr_t *)vParts, i );
+        vPartSupp = Vec_PtrEntry( (Vec_Ptr_t *)vPartSupps, i );
+        // copy the component
+        vNodes = Aig_ManDupPart( pNew, p, vPart, vPartSupp, 1 );
+        assert( Vec_PtrSize(vNodes) == Vec_VecSize(vParts) * Vec_PtrSize(vAigs) );
+        // create choice node
+        for ( k = 0; k < Vec_VecSize(vParts); k++ )
+        {
+            for ( m = 0; m < Vec_PtrSize(vAigs); m++ )
+            {
+                pObj = Aig_ObjChild0( Vec_PtrEntry(vNodes, k * Vec_PtrSize(vAigs) + m) );
+                break;
+            }
+            Aig_ObjCreatePo( pNew, pObj );
+        }
+        Vec_PtrFree( vNodes );
+    }
+    Vec_VecFree( vParts );
+    Vec_VecFree( vPartSupps );
+
+    // trasfer representatives
+    Aig_ManReprStart( pNew, Aig_ManObjIdMax(pNew)+1 );
+    Vec_PtrForEachEntry( vMiters, p, i )
+    {
+        Aig_ManTransferRepr( pNew, p );
+        Aig_ManStop( p );
+    }
+    Vec_PtrFree( vMiters );
+
+    // derive the result of choicing
+    pChoice = Aig_ManCreateChoices( pNew );
+    if ( pChoice != pNew )
+        Aig_ManStop( pNew );
+    return pChoice;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/aig/aigRepr.c b/src/aig/aig/aigRepr.c
new file mode 100644
index 00000000..fa6bf60e
--- /dev/null
+++ b/src/aig/aig/aigRepr.c
@@ -0,0 +1,343 @@
+/**CFile****************************************************************
+
+  FileName    [aigRepr.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [AIG package.]
+
+  Synopsis    [Handing node representatives.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - April 28, 2007.]
+
+  Revision    [$Id: aigRepr.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "aig.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Starts the array of representatives.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_ManReprStart( Aig_Man_t * p, int nIdMax )
+{
+    assert( Aig_ManBufNum(p) == 0 );
+    assert( p->pRepr == NULL );
+    p->nReprAlloc = nIdMax;
+    p->pRepr = ALLOC( Aig_Obj_t *, p->nReprAlloc );
+    memset( p->pRepr, 0, sizeof(Aig_Obj_t *) * p->nReprAlloc );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Stop the array of representatives.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_ManReprStop( Aig_Man_t * p )
+{
+    assert( p->pRepr != NULL );
+    FREE( p->pRepr );
+    p->nReprAlloc = 0;    
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Set the representative.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Aig_ObjSetRepr( Aig_Man_t * p, Aig_Obj_t * pNode1, Aig_Obj_t * pNode2 )
+{
+    assert( p->pRepr != NULL );
+    assert( !Aig_IsComplement(pNode1) );
+    assert( !Aig_IsComplement(pNode2) );
+    assert( pNode1->Id < p->nReprAlloc );
+    assert( pNode2->Id < p->nReprAlloc );
+    if ( pNode1 == pNode2 )
+        return;
+    if ( pNode1->Id < pNode2->Id )
+        p->pRepr[pNode2->Id] = pNode1;
+    else
+        p->pRepr[pNode1->Id] = pNode2;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Find representative.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline Aig_Obj_t * Aig_ObjFindRepr( Aig_Man_t * p, Aig_Obj_t * pNode )
+{
+    assert( p->pRepr != NULL );
+    assert( !Aig_IsComplement(pNode) );
+    assert( pNode->Id < p->nReprAlloc );
+    assert( !p->pRepr[pNode->Id] || p->pRepr[pNode->Id]->Id < pNode->Id );
+    return p->pRepr[pNode->Id];
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Find representative transitively.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline Aig_Obj_t * Aig_ObjFindReprTrans( Aig_Man_t * p, Aig_Obj_t * pNode )
+{
+    Aig_Obj_t * pPrev, * pRepr;
+    for ( pPrev = NULL, pRepr = Aig_ObjFindRepr(p, pNode); pRepr; pPrev = pRepr, pRepr = Aig_ObjFindRepr(p, pRepr) );
+    return pPrev;    
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns representatives of fanin in approapriate polarity.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline Aig_Obj_t * Aig_ObjRepr( Aig_Man_t * p, Aig_Obj_t * pObj )
+{
+    Aig_Obj_t * pRepr;
+    if ( pRepr = Aig_ObjFindRepr(p, pObj) )
+        return Aig_NotCond( pRepr->pData, pObj->fPhase ^ pRepr->fPhase );
+    return pObj->pData;
+}
+static inline Aig_Obj_t * Aig_ObjChild0Repr( Aig_Man_t * p, Aig_Obj_t * pObj ) { return Aig_NotCond( Aig_ObjRepr(p, Aig_ObjFanin0(pObj)), Aig_ObjFaninC0(pObj) ); }
+static inline Aig_Obj_t * Aig_ObjChild1Repr( Aig_Man_t * p, Aig_Obj_t * pObj ) { return Aig_NotCond( Aig_ObjRepr(p, Aig_ObjFanin1(pObj)), Aig_ObjFaninC1(pObj) ); }
+
+/**Function*************************************************************
+
+  Synopsis    [Duplicates AIG while substituting representatives.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_ManTransferRepr( Aig_Man_t * pNew, Aig_Man_t * p )
+{
+    Aig_Obj_t * pObj, * pRepr;
+    int k;
+    assert( pNew->pRepr != NULL );
+    // go through the nodes which have representatives
+    Aig_ManForEachObj( p, pObj, k )
+        if ( pRepr = Aig_ObjFindRepr(p, pObj) )
+            Aig_ObjSetRepr( pNew, Aig_Regular(pRepr->pData), Aig_Regular(pObj->pData) ); 
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Duplicates AIG while substituting representatives.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Aig_ManDupRepr( Aig_Man_t * p )
+{
+    Aig_Man_t * pNew;
+    Aig_Obj_t * pObj, * pRepr;
+    int i;
+    // start the HOP package
+    pNew = Aig_ManStart( Aig_ManObjIdMax(p) + 1 );
+    Aig_ManReprStart( pNew, Aig_ManObjIdMax(p)+1 );
+    // map the const and primary inputs
+    Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
+    Aig_ManForEachPi( p, pObj, i )
+        pObj->pData = Aig_ObjCreatePi(pNew);
+    // map the internal nodes
+    Aig_ManForEachNode( p, pObj, i )
+    {
+        pObj->pData = Aig_And( pNew, Aig_ObjChild0Repr(p, pObj), Aig_ObjChild1Repr(p, pObj) );
+        if ( pRepr = Aig_ObjFindRepr(p, pObj) ) // member of the class
+            Aig_ObjSetRepr( pNew, Aig_Regular(pRepr->pData), Aig_Regular(pObj->pData) );
+    }
+    // transfer the POs
+    Aig_ManForEachPo( p, pObj, i )
+        Aig_ObjCreatePo( pNew, Aig_ObjChild0Repr(p, pObj) );
+    // check the new manager
+    if ( !Aig_ManCheck(pNew) )
+        printf( "Aig_ManDupRepr: Check has failed.\n" );
+    return pNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Transfer representatives and return the number of critical fanouts.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Aig_ManRemapRepr( Aig_Man_t * p )
+{
+    Aig_Obj_t * pObj, * pRepr;
+    int i, nFanouts = 0;
+    Aig_ManForEachNode( p, pObj, i )
+    {
+        pRepr = Aig_ObjFindReprTrans( p, pObj );
+        if ( pRepr == NULL )
+            continue;
+        assert( pRepr->Id < pObj->Id );
+        Aig_ObjSetRepr( p, pObj, pRepr );
+        nFanouts += (pObj->nRefs > 0);
+    }
+    return nFanouts;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if pOld is in the TFI of pNew.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Aig_ObjCheckTfi_rec( Aig_Man_t * p, Aig_Obj_t * pNode, Aig_Obj_t * pOld )
+{
+    // check the trivial cases
+    if ( pNode == NULL )
+        return 0;
+//    if ( pNode->Id < pOld->Id ) // cannot use because of choices of pNode
+//        return 0;
+    if ( pNode == pOld )
+        return 1;
+    // skip the visited node
+    if ( Aig_ObjIsTravIdCurrent( p, pNode ) )
+        return 0;
+    Aig_ObjSetTravIdCurrent( p, pNode );
+    // check the children
+    if ( Aig_ObjCheckTfi_rec( p, Aig_ObjFanin0(pNode), pOld ) )
+        return 1;
+    if ( Aig_ObjCheckTfi_rec( p, Aig_ObjFanin1(pNode), pOld ) )
+        return 1;
+    // check equivalent nodes
+    return Aig_ObjCheckTfi_rec( p, pNode->pData, pOld );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if pOld is in the TFI of pNew.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Aig_ObjCheckTfi( Aig_Man_t * p, Aig_Obj_t * pNew, Aig_Obj_t * pOld )
+{
+    assert( !Aig_IsComplement(pNew) );
+    assert( !Aig_IsComplement(pOld) );
+    Aig_ManIncrementTravId( p );
+    return Aig_ObjCheckTfi_rec( p, pNew, pOld );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates choices.]
+
+  Description [The input AIG is assumed to have representatives assigned.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Aig_ManCreateChoices( Aig_Man_t * p )
+{
+    Aig_Man_t * pTemp;
+    Aig_Obj_t * pObj, * pRepr;
+    int i;
+    assert( p->pRepr != NULL );
+    // iteratively reconstruct the HOP manager while transfering the fanouts
+    while ( Aig_ManRemapRepr( p ) )
+    {
+        p = Aig_ManDupRepr( pTemp = p );
+        Aig_ManStop( pTemp );
+    }
+    // create choices in this manager
+    Aig_ManCleanData( p );
+    // make the choice nodes
+    Aig_ManForEachNode( p, pObj, i )
+    {
+        pRepr = Aig_ObjFindRepr( p, pObj );
+        if ( pRepr == NULL )
+            continue;
+        // skip constant and PI classes
+        if ( !Aig_ObjIsNode(pRepr) )
+            continue;
+        // skip choices with combinatinal loops
+        if ( Aig_ObjCheckTfi( p, pRepr, pObj ) )
+            continue;
+        // add choice to the choice node
+        pObj->pData = pRepr->pData;
+        pRepr->pData = pObj;
+    }
+    return p;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/aig/aigTable.c b/src/aig/aig/aigTable.c
index ba359c09..0d4ffd1f 100644
--- a/src/aig/aig/aigTable.c
+++ b/src/aig/aig/aigTable.c
@@ -99,7 +99,7 @@ clk = clock();
     }
     nEntries = Aig_ManNodeNum(p);
     assert( Counter == nEntries );
-    printf( "Increasing the structural table size from %6d to %6d. ", nTableSizeOld, p->nTableSize );
+//    printf( "Increasing the structural table size from %6d to %6d. ", nTableSizeOld, p->nTableSize );
     PRT( "Time", clock() - clk );
     // replace the table and the parameters
     free( pTableOld );
diff --git a/src/aig/aig/aigTiming.c b/src/aig/aig/aigTiming.c
index dfb4c306..14ee4f2c 100644
--- a/src/aig/aig/aigTiming.c
+++ b/src/aig/aig/aigTiming.c
@@ -68,6 +68,22 @@ static inline void Aig_ObjSetReverseLevel( Aig_Man_t * p, Aig_Obj_t * pObj, int
 
 /**Function*************************************************************
 
+  Synopsis    [Resets reverse level of the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_ObjClearReverseLevel( Aig_Man_t * p, Aig_Obj_t * pObj )
+{
+    Aig_ObjSetReverseLevel( p, pObj, 0 );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Returns required level of the node.]
 
   Description [Converts the reverse levels of the node into its required 
@@ -178,6 +194,7 @@ void Aig_ManUpdateLevel( Aig_Man_t * p, Aig_Obj_t * pObjNew )
     Aig_Obj_t * pFanout, * pTemp;
     int iFanout, LevelOld, Lev, k, m;
     assert( p->pFanData != NULL );
+    assert( Aig_ObjIsNode(pObjNew) );
     // allocate level if needed
     if ( p->vLevels == NULL )
         p->vLevels = Vec_VecAlloc( Aig_ManLevels(p) + 8 );
@@ -203,8 +220,9 @@ void Aig_ManUpdateLevel( Aig_Man_t * p, Aig_Obj_t * pObjNew )
         // schedule fanout for level update
         Aig_ObjForEachFanout( p, pTemp, pFanout, iFanout, m )
         {
-            if ( !Aig_ObjIsPo(pFanout) && !pFanout->fMarkA )
+            if ( Aig_ObjIsNode(pFanout) && !pFanout->fMarkA )
             {
+                assert( Aig_ObjLevel(pFanout) >= Lev );
                 Vec_VecPush( p->vLevels, Aig_ObjLevel(pFanout), pFanout );
                 pFanout->fMarkA = 1;
             }
@@ -226,8 +244,9 @@ void Aig_ManUpdateLevel( Aig_Man_t * p, Aig_Obj_t * pObjNew )
 void Aig_ManUpdateReverseLevel( Aig_Man_t * p, Aig_Obj_t * pObjNew )
 {
     Aig_Obj_t * pFanin, * pTemp;
-    int LevelOld, Lev, k;
+    int LevelOld, LevFanin, Lev, k;
     assert( p->vLevelR != NULL );
+    assert( Aig_ObjIsNode(pObjNew) );
     // allocate level if needed
     if ( p->vLevels == NULL )
         p->vLevels = Vec_VecAlloc( Aig_ManLevels(p) + 8 );
@@ -253,20 +272,77 @@ void Aig_ManUpdateReverseLevel( Aig_Man_t * p, Aig_Obj_t * pObjNew )
             continue;
         // schedule fanins for level update
         pFanin = Aig_ObjFanin0(pTemp);
-        if ( pFanin && !Aig_ObjIsPi(pFanin) && !pFanin->fMarkA )
+        if ( Aig_ObjIsNode(pFanin) && !pFanin->fMarkA )
         {
-            Vec_VecPush( p->vLevels, Aig_ObjReverseLevel(p, pFanin), pFanin );
+            LevFanin = Aig_ObjReverseLevel( p, pFanin );
+            assert( LevFanin >= Lev );
+            Vec_VecPush( p->vLevels, LevFanin, pFanin );
             pFanin->fMarkA = 1;
         }
         pFanin = Aig_ObjFanin1(pTemp);
-        if ( pFanin && !Aig_ObjIsPi(pFanin) && !pFanin->fMarkA )
+        if ( Aig_ObjIsNode(pFanin) && !pFanin->fMarkA )
         {
-            Vec_VecPush( p->vLevels, Aig_ObjReverseLevel(p, pFanin), pFanin );
+            LevFanin = Aig_ObjReverseLevel( p, pFanin );
+            assert( LevFanin >= Lev );
+            Vec_VecPush( p->vLevels, LevFanin, pFanin );
             pFanin->fMarkA = 1;
         }
     }
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Verifies direct level of the nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_ManVerifyLevel( Aig_Man_t * p )
+{
+    Aig_Obj_t * pObj;
+    int i, Counter = 0;
+    assert( p->pFanData );
+    Aig_ManForEachNode( p, pObj, i )
+        if ( Aig_ObjLevel(pObj) != Aig_ObjLevelNew(pObj) )
+        {
+            printf( "Level of node %6d should be %4d instead of %4d.\n", 
+                pObj->Id, Aig_ObjLevelNew(pObj), Aig_ObjLevel(pObj) );
+            Counter++;
+        }
+    if ( Counter )
+    printf( "Levels of %d nodes are incorrect.\n", Counter );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Verifies reverse level of the nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_ManVerifyReverseLevel( Aig_Man_t * p )
+{
+    Aig_Obj_t * pObj;
+    int i, Counter = 0;
+    assert( p->vLevelR );
+    Aig_ManForEachNode( p, pObj, i )
+        if ( Aig_ObjLevel(pObj) != Aig_ObjLevelNew(pObj) )
+        {
+            printf( "Reverse level of node %6d should be %4d instead of %4d.\n", 
+                pObj->Id, Aig_ObjReverseLevelNew(p, pObj), Aig_ObjReverseLevel(p, pObj) );
+            Counter++;
+        }
+    if ( Counter )
+    printf( "Reverse levels of %d nodes are incorrect.\n", Counter );
+}
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
diff --git a/src/aig/aig/aigUtil.c b/src/aig/aig/aigUtil.c
index a1c68371..364c32a3 100644
--- a/src/aig/aig/aigUtil.c
+++ b/src/aig/aig/aigUtil.c
@@ -123,6 +123,44 @@ void Aig_ManCheckMarkA( Aig_Man_t * p )
 
 /**Function*************************************************************
 
+  Synopsis    [Checks if the markA is reset.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_ManCleanMarkA( Aig_Man_t * p )
+{
+    Aig_Obj_t * pObj;
+    int i;
+    Aig_ManForEachObj( p, pObj, i )
+        pObj->fMarkA = 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Checks if the markA is reset.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_ManCleanMarkB( Aig_Man_t * p )
+{
+    Aig_Obj_t * pObj;
+    int i;
+    Aig_ManForEachObj( p, pObj, i )
+        pObj->fMarkB = 0;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Cleans the data pointers for the nodes.]
 
   Description []
diff --git a/src/aig/aig/module.make b/src/aig/aig/module.make
index 83e4c413..d4737278 100644
--- a/src/aig/aig/module.make
+++ b/src/aig/aig/module.make
@@ -2,10 +2,13 @@ SRC +=    src/aig/aig/aigCheck.c \
     src/aig/aig/aigDfs.c \
     src/aig/aig/aigFanout.c \
     src/aig/aig/aigMan.c \
-    src/aig/aig/aigMffc.c \
     src/aig/aig/aigMem.c \
+    src/aig/aig/aigMffc.c \
     src/aig/aig/aigObj.c \
     src/aig/aig/aigOper.c \
+    src/aig/aig/aigOrder.c \
+    src/aig/aig/aigPart.c \
+    src/aig/aig/aigRepr.c \
     src/aig/aig/aigSeq.c \
     src/aig/aig/aigTable.c \
     src/aig/aig/aigTiming.c \
diff --git a/src/aig/cnf/cnf.h b/src/aig/cnf/cnf.h
index c758867c..2f121752 100644
--- a/src/aig/cnf/cnf.h
+++ b/src/aig/cnf/cnf.h
@@ -83,8 +83,16 @@ struct Cnf_Man_t_
     int             nMergeLimit;     // the limit on the size of merged cut
     unsigned *      pTruths[4];      // temporary truth tables
     Vec_Int_t *     vMemory;         // memory for intermediate ISOP representation
+    int             timeCuts; 
+    int             timeMap;
+    int             timeSave;
 };
 
+
+static inline Dar_Cut_t *  Dar_ObjBestCut( Aig_Obj_t * pObj ) { Dar_Cut_t * pCut; int i; Dar_ObjForEachCut( pObj, pCut, i ) if ( pCut->fBest ) return pCut; return NULL; }
+
+static inline int          Cnf_CutSopCost( Cnf_Man_t * p, Dar_Cut_t * pCut ) { return p->pSopSizes[pCut->uTruth] + p->pSopSizes[0xFFFF & ~pCut->uTruth]; }
+
 static inline int          Cnf_CutLeaveNum( Cnf_Cut_t * pCut )    { return pCut->nFanins;                               }
 static inline int *        Cnf_CutLeaves( Cnf_Cut_t * pCut )      { return pCut->pFanins;                               }
 static inline unsigned *   Cnf_CutTruth( Cnf_Cut_t * pCut )       { return (unsigned *)(pCut->pFanins + pCut->nFanins); }
@@ -109,7 +117,9 @@ static inline void         Cnf_ObjSetBestCut( Aig_Obj_t * pObj, Cnf_Cut_t * pCut
 ////////////////////////////////////////////////////////////////////////
 
 /*=== cnfCore.c ========================================================*/
-extern Cnf_Dat_t *     Cnf_Derive( Cnf_Man_t * p, Aig_Man_t * pAig );
+extern Cnf_Dat_t *     Cnf_Derive( Aig_Man_t * pAig );
+extern Cnf_Man_t *     Cnf_ManRead();
+extern void            Cnf_ClearMemory();
 /*=== cnfCut.c ========================================================*/
 extern Cnf_Cut_t *     Cnf_CutCreate( Cnf_Man_t * p, Aig_Obj_t * pObj );
 extern void            Cnf_CutPrint( Cnf_Cut_t * pCut );
@@ -121,10 +131,12 @@ extern void            Cnf_ReadMsops( char ** ppSopSizes, char *** ppSops );
 /*=== cnfMan.c ========================================================*/
 extern Cnf_Man_t *     Cnf_ManStart();
 extern void            Cnf_ManStop( Cnf_Man_t * p );
+extern Vec_Int_t *     Cnf_DataCollectPiSatNums( Cnf_Dat_t * pCnf, Aig_Man_t * p );
 extern void            Cnf_DataFree( Cnf_Dat_t * p );
 extern void            Cnf_DataWriteIntoFile( Cnf_Dat_t * p, char * pFileName );
 void *                 Cnf_DataWriteIntoSolver( Cnf_Dat_t * p );
 /*=== cnfMap.c ========================================================*/
+extern void            Cnf_DeriveMapping( Cnf_Man_t * p );
 extern int             Cnf_ManMapForCnf( Cnf_Man_t * p );
 /*=== cnfPost.c ========================================================*/
 extern void            Cnf_ManTransferCuts( Cnf_Man_t * p );
@@ -132,7 +144,7 @@ extern void            Cnf_ManFreeCuts( Cnf_Man_t * p );
 extern void            Cnf_ManPostprocess( Cnf_Man_t * p );
 /*=== cnfUtil.c ========================================================*/
 extern Vec_Ptr_t *     Aig_ManScanMapping( Cnf_Man_t * p, int fCollect );
-extern Vec_Ptr_t *     Cnf_ManScanMapping( Cnf_Man_t * p, int fCollect );
+extern Vec_Ptr_t *     Cnf_ManScanMapping( Cnf_Man_t * p, int fCollect, int fPreorder );
 /*=== cnfWrite.c ========================================================*/
 extern void            Cnf_SopConvertToVector( char * pSop, int nCubes, Vec_Int_t * vCover );
 extern Cnf_Dat_t *     Cnf_ManWriteCnf( Cnf_Man_t * p, Vec_Ptr_t * vMapped );
diff --git a/src/aig/cnf/cnfCore.c b/src/aig/cnf/cnfCore.c
index a3a7efaa..7480d45d 100644
--- a/src/aig/cnf/cnfCore.c
+++ b/src/aig/cnf/cnfCore.c
@@ -24,13 +24,15 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
+static Cnf_Man_t * s_pManCnf = NULL;
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
 
-  Synopsis    []
+  Synopsis    [Converts AIG into the SAT solver.]
 
   Description []
                
@@ -39,21 +41,97 @@
   SeeAlso     []
 
 ***********************************************************************/
-Cnf_Dat_t * Cnf_Derive( Cnf_Man_t * p, Aig_Man_t * pAig )
+Cnf_Dat_t * Cnf_Derive( Aig_Man_t * pAig )
 {
-    Aig_MmFixed_t * pMemCuts;
-    Cnf_Dat_t * pCnf = NULL;
+    Cnf_Man_t * p;
+    Cnf_Dat_t * pCnf;
     Vec_Ptr_t * vMapped;
-    int nIters = 2;
+    Aig_MmFixed_t * pMemCuts;
     int clk;
-
+    // allocate the CNF manager
+    if ( s_pManCnf == NULL )
+        s_pManCnf = Cnf_ManStart();
     // connect the managers
+    p = s_pManCnf;
     p->pManAig = pAig;
 
     // generate cuts for all nodes, assign cost, and find best cuts
 clk = clock();
-    pMemCuts = Dar_ManComputeCuts( pAig );
-PRT( "Cuts", clock() - clk );
+    pMemCuts = Dar_ManComputeCuts( pAig, 10 );
+p->timeCuts = clock() - clk;
+
+    // find the mapping
+clk = clock();
+    Cnf_DeriveMapping( p );
+p->timeMap = clock() - clk;
+//    Aig_ManScanMapping( p, 1 );
+
+    // convert it into CNF
+clk = clock();
+    Cnf_ManTransferCuts( p );
+    vMapped = Cnf_ManScanMapping( p, 1, 1 );
+    pCnf = Cnf_ManWriteCnf( p, vMapped );
+    Vec_PtrFree( vMapped );
+    Aig_MmFixedStop( pMemCuts, 0 );
+p->timeSave = clock() - clk;
+
+PRT( "Cuts   ", p->timeCuts );
+PRT( "Map    ", p->timeMap  );
+PRT( "Saving ", p->timeSave );
+    return pCnf;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Cnf_Man_t * Cnf_ManRead()
+{
+    return s_pManCnf;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cnf_ClearMemory()
+{
+    if ( s_pManCnf == NULL )
+        return;
+    Cnf_ManStop( s_pManCnf );
+    s_pManCnf = NULL;
+}
+
+
+#if 0
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Cnf_Dat_t * Cnf_Derive_old( Aig_Man_t * pAig )
+{
 /*
     // iteratively improve area flow
     for ( i = 0; i < nIters; i++ )
@@ -95,6 +173,9 @@ PRT( "Ext ", clock() - clk );
     return NULL;
 }
 
+#endif
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/cnf/cnfCut.c b/src/aig/cnf/cnfCut.c
index afe5920a..17ab0c78 100644
--- a/src/aig/cnf/cnfCut.c
+++ b/src/aig/cnf/cnfCut.c
@@ -87,15 +87,14 @@ Cnf_Cut_t * Cnf_CutCreate( Cnf_Man_t * p, Aig_Obj_t * pObj )
     Cnf_Cut_t * pCut;
     unsigned * pTruth;
     assert( Aig_ObjIsNode(pObj) );
-//    pCutBest = Aig_ObjBestCut( pObj );
-        pCutBest = NULL;
+    pCutBest = Dar_ObjBestCut( pObj );
     assert( pCutBest != NULL );
     assert( pCutBest->nLeaves <= 4 );
     pCut = Cnf_CutAlloc( p, pCutBest->nLeaves );
     memcpy( pCut->pFanins, pCutBest->pLeaves, sizeof(int) * pCutBest->nLeaves );
     pTruth = Cnf_CutTruth(pCut);
     *pTruth = (pCutBest->uTruth << 16) | pCutBest->uTruth;
-    pCut->Cost = p->pSopSizes[0xFFFF & *pTruth] + p->pSopSizes[0xFFFF & ~*pTruth];
+    pCut->Cost = Cnf_CutSopCost( p, pCutBest );
     return pCut;
 }
 
diff --git a/src/aig/cnf/cnfMan.c b/src/aig/cnf/cnfMan.c
index e978e322..77bf8650 100644
--- a/src/aig/cnf/cnfMan.c
+++ b/src/aig/cnf/cnfMan.c
@@ -86,6 +86,28 @@ void Cnf_ManStop( Cnf_Man_t * p )
 
 /**Function*************************************************************
 
+  Synopsis    [Returns the array of CI IDs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Cnf_DataCollectPiSatNums( Cnf_Dat_t * pCnf, Aig_Man_t * p )
+{
+    Vec_Int_t * vCiIds;
+    Aig_Obj_t * pObj;
+    int i;
+    vCiIds = Vec_IntAlloc( Aig_ManPiNum(p) );
+    Aig_ManForEachPi( p, pObj, i )
+        Vec_IntPush( vCiIds, pCnf->pVarNums[pObj->Id] );
+    return vCiIds;
+}
+
+/**Function*************************************************************
+
   Synopsis    []
 
   Description []
diff --git a/src/aig/cnf/cnfMap.c b/src/aig/cnf/cnfMap.c
index a9ba41a0..ad728412 100644
--- a/src/aig/cnf/cnfMap.c
+++ b/src/aig/cnf/cnfMap.c
@@ -28,6 +28,126 @@
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
+/**Function*************************************************************
+
+  Synopsis    [Computes area flow of the cut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cnf_CutAssignAreaFlow( Cnf_Man_t * p, Dar_Cut_t * pCut, int * pAreaFlows )
+{
+    Aig_Obj_t * pLeaf;
+    int i;
+    pCut->Value = 0;
+    pCut->uSign = 100 * Cnf_CutSopCost( p, pCut );
+    Dar_CutForEachLeaf( p->pManAig, pCut, pLeaf, i )
+    {
+        pCut->Value += pLeaf->nRefs;
+        if ( !Aig_ObjIsNode(pLeaf) )
+            continue;
+        assert( pLeaf->nRefs > 0 );
+        pCut->uSign += pAreaFlows[pLeaf->Id] / (pLeaf->nRefs? pLeaf->nRefs : 1);
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes area flow of the supergate.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Cnf_CutSuperAreaFlow( Vec_Ptr_t * vSuper, int * pAreaFlows )
+{
+    Aig_Obj_t * pLeaf;
+    int i, nAreaFlow;
+    nAreaFlow = 100 * (Vec_PtrSize(vSuper) + 1);
+    Vec_PtrForEachEntry( vSuper, pLeaf, i )
+    {
+        pLeaf = Aig_Regular(pLeaf);
+        if ( !Aig_ObjIsNode(pLeaf) )
+            continue;
+        assert( pLeaf->nRefs > 0 );
+        nAreaFlow += pAreaFlows[pLeaf->Id] / (pLeaf->nRefs? pLeaf->nRefs : 1);
+    }
+    return nAreaFlow;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cnf_DeriveMapping( Cnf_Man_t * p )
+{
+    Vec_Ptr_t * vSuper;
+    Aig_Obj_t * pObj;
+    Dar_Cut_t * pCut, * pCutBest;
+    int i, k, AreaFlow, * pAreaFlows;
+    // allocate area flows
+    pAreaFlows = ALLOC( int, Aig_ManObjIdMax(p->pManAig) + 1 );
+    memset( pAreaFlows, 0, sizeof(int) * (Aig_ManObjIdMax(p->pManAig) + 1) );
+    // visit the nodes in the topological order and update their best cuts
+    vSuper = Vec_PtrAlloc( 100 );
+    Aig_ManForEachNode( p->pManAig, pObj, i )
+    {
+        // go through the cuts
+        pCutBest = NULL;
+        Dar_ObjForEachCut( pObj, pCut, k )
+        {
+            pCut->fBest = 0;
+            if ( k == 0 )
+                continue;
+            Cnf_CutAssignAreaFlow( p, pCut, pAreaFlows );
+            if ( pCutBest == NULL || pCutBest->uSign > pCut->uSign || 
+                (pCutBest->uSign == pCut->uSign && pCutBest->Value < pCut->Value) )
+                 pCutBest = pCut;
+        }
+        // check the big cut
+//        Aig_ObjCollectSuper( pObj, vSuper );
+        // get the area flow of this cut
+//        AreaFlow = Cnf_CutSuperAreaFlow( vSuper, pAreaFlows );
+        AreaFlow = AIG_INFINITY;
+        if ( AreaFlow >= (int)pCutBest->uSign )
+        {
+            pAreaFlows[pObj->Id] = pCutBest->uSign;
+            pCutBest->fBest = 1;
+        }
+        else
+        {
+            pAreaFlows[pObj->Id] = AreaFlow;
+            pObj->fMarkB = 1; // mark the special node
+        }
+    }
+    Vec_PtrFree( vSuper );
+    free( pAreaFlows );
+
+/*
+    // compute the area of mapping
+    AreaFlow = 0;
+    Aig_ManForEachPo( p->pManAig, pObj, i )
+        AreaFlow += Dar_ObjBestCut(Aig_ObjFanin0(pObj))->uSign / 100 / Aig_ObjFanin0(pObj)->nRefs;
+    printf( "Area of the network = %d.\n", AreaFlow );
+*/
+}
+
+
+
 #if 0
 
 /**Function*************************************************************
@@ -160,45 +280,6 @@ Dar_Cut_t * Cnf_ObjFindBestCut( Aig_Obj_t * pObj )
   SeeAlso     []
 
 ***********************************************************************/
-void Cnf_CutAssignAreaFlow( Cnf_Man_t * p, Dar_Cut_t * pCut )
-{
-    Aig_Obj_t * pLeaf;
-    int i;
-    pCut->Cost    = p->pSopSizes[pCut->uTruth] + p->pSopSizes[0xFFFF & ~pCut->uTruth];
-    pCut->Area    = (float)pCut->Cost;
-    pCut->NoRefs  = 0;
-    pCut->FanRefs = 0;
-    Dar_CutForEachLeaf( p->pManAig, pCut, pLeaf, i )
-    {
-        if ( !Aig_ObjIsNode(pLeaf) )
-            continue;
-        if ( pLeaf->nRefs == 0 )
-        {
-            pCut->Area += Aig_ObjBestCut(pLeaf)->Area;
-            pCut->NoRefs++;
-        }
-        else
-        {
-            pCut->Area += Aig_ObjBestCut(pLeaf)->Area / pLeaf->nRefs;
-            if ( pCut->FanRefs + pLeaf->nRefs > 15 )
-                pCut->FanRefs = 15;
-            else
-                pCut->FanRefs += pLeaf->nRefs;
-        }
-    }
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Computes area flow of the cut.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
 void Cnf_CutAssignArea( Cnf_Man_t * p, Dar_Cut_t * pCut )
 {
     Aig_Obj_t * pLeaf;
diff --git a/src/aig/cnf/cnfUtil.c b/src/aig/cnf/cnfUtil.c
index da5edef2..22b30262 100644
--- a/src/aig/cnf/cnfUtil.c
+++ b/src/aig/cnf/cnfUtil.c
@@ -51,11 +51,24 @@ int Aig_ManScanMapping_rec( Cnf_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vMapped
     if ( vMapped )
         Vec_PtrPush( vMapped, pObj );
     // visit the transitive fanin of the selected cut
-//    pCutBest = Aig_ObjBestCut(pObj);
-        pCutBest = NULL;
-    aArea = pCutBest->Value;
-    Dar_CutForEachLeaf( p->pManAig, pCutBest, pLeaf, i )
-        aArea += Aig_ManScanMapping_rec( p, pLeaf, vMapped );
+    if ( pObj->fMarkB )
+    {
+        Vec_Ptr_t * vSuper = Vec_PtrAlloc( 100 );
+        Aig_ObjCollectSuper( pObj, vSuper );
+        aArea = Vec_PtrSize(vSuper) + 1;
+        Vec_PtrForEachEntry( vSuper, pLeaf, i )
+            aArea += Aig_ManScanMapping_rec( p, Aig_Regular(pLeaf), vMapped );
+        Vec_PtrFree( vSuper );
+        ////////////////////////////
+        pObj->fMarkB = 1;
+    }
+    else
+    {
+        pCutBest = Dar_ObjBestCut( pObj );
+        aArea = Cnf_CutSopCost( p, pCutBest );
+        Dar_CutForEachLeaf( p->pManAig, pCutBest, pLeaf, i )
+            aArea += Aig_ManScanMapping_rec( p, pLeaf, vMapped );
+    }
     return aArea;
 }
 
@@ -85,7 +98,7 @@ Vec_Ptr_t * Aig_ManScanMapping( Cnf_Man_t * p, int fCollect )
     p->aArea = 0;
     Aig_ManForEachPo( p->pManAig, pObj, i )
         p->aArea += Aig_ManScanMapping_rec( p, Aig_ObjFanin0(pObj), vMapped );
-    printf( "Variables = %6d. Clauses = %8d.\n", vMapped? Vec_PtrSize(vMapped) : 0, p->aArea );
+    printf( "Variables = %6d. Clauses = %8d.\n", vMapped? Vec_PtrSize(vMapped) + Aig_ManPiNum(p->pManAig) + 1 : 0, p->aArea + 2 );
     return vMapped;
 }
 
@@ -100,7 +113,7 @@ Vec_Ptr_t * Aig_ManScanMapping( Cnf_Man_t * p, int fCollect )
   SeeAlso     []
 
 ***********************************************************************/
-int Cnf_ManScanMapping_rec( Cnf_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vMapped )
+int Cnf_ManScanMapping_rec( Cnf_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vMapped, int fPreorder )
 {
     Aig_Obj_t * pLeaf;
     Cnf_Cut_t * pCutBest;
@@ -109,15 +122,32 @@ int Cnf_ManScanMapping_rec( Cnf_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vMapped
         return 0;
     assert( Aig_ObjIsAnd(pObj) );
     assert( pObj->pData != NULL );
+    // add the node to the mapping
+    if ( vMapped && fPreorder )
+         Vec_PtrPush( vMapped, pObj );
     // visit the transitive fanin of the selected cut
-    pCutBest = pObj->pData;
-    assert( pCutBest->Cost < 127 );
-    aArea = pCutBest->Cost;
-    Cnf_CutForEachLeaf( p->pManAig, pCutBest, pLeaf, i )
-        aArea += Cnf_ManScanMapping_rec( p, pLeaf, vMapped );
-    // collect the node first to derive pre-order
-    if ( vMapped )
-        Vec_PtrPush( vMapped, pObj );
+    if ( pObj->fMarkB )
+    {
+        Vec_Ptr_t * vSuper = Vec_PtrAlloc( 100 );
+        Aig_ObjCollectSuper( pObj, vSuper );
+        aArea = Vec_PtrSize(vSuper) + 1;
+        Vec_PtrForEachEntry( vSuper, pLeaf, i )
+            aArea += Cnf_ManScanMapping_rec( p, Aig_Regular(pLeaf), vMapped, fPreorder );
+        Vec_PtrFree( vSuper );
+        ////////////////////////////
+        pObj->fMarkB = 1;
+    }
+    else
+    {
+        pCutBest = pObj->pData;
+        assert( pCutBest->Cost < 127 );
+        aArea = pCutBest->Cost;
+        Cnf_CutForEachLeaf( p->pManAig, pCutBest, pLeaf, i )
+            aArea += Cnf_ManScanMapping_rec( p, pLeaf, vMapped, fPreorder );
+    }
+    // add the node to the mapping
+    if ( vMapped && !fPreorder )
+         Vec_PtrPush( vMapped, pObj );
     return aArea;
 }
 
@@ -132,7 +162,7 @@ int Cnf_ManScanMapping_rec( Cnf_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vMapped
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Ptr_t * Cnf_ManScanMapping( Cnf_Man_t * p, int fCollect )
+Vec_Ptr_t * Cnf_ManScanMapping( Cnf_Man_t * p, int fCollect, int fPreorder )
 {
     Vec_Ptr_t * vMapped = NULL;
     Aig_Obj_t * pObj;
@@ -146,8 +176,8 @@ Vec_Ptr_t * Cnf_ManScanMapping( Cnf_Man_t * p, int fCollect )
     // collect nodes reachable from POs in the DFS order through the best cuts
     p->aArea = 0;
     Aig_ManForEachPo( p->pManAig, pObj, i )
-        p->aArea += Cnf_ManScanMapping_rec( p, Aig_ObjFanin0(pObj), vMapped );
-    printf( "Variables = %6d. Clauses = %8d.\n", vMapped? Vec_PtrSize(vMapped) : 0, p->aArea );
+        p->aArea += Cnf_ManScanMapping_rec( p, Aig_ObjFanin0(pObj), vMapped, fPreorder );
+    printf( "Variables = %6d. Clauses = %8d.\n", vMapped? Vec_PtrSize(vMapped) + Aig_ManPiNum(p->pManAig) + 1 : 0, p->aArea + 2 );
     return vMapped;
 }
 
diff --git a/src/aig/cnf/cnfWrite.c b/src/aig/cnf/cnfWrite.c
index 22c4240a..41a00732 100644
--- a/src/aig/cnf/cnfWrite.c
+++ b/src/aig/cnf/cnfWrite.c
@@ -127,42 +127,15 @@ int Cnf_IsopCountLiterals( Vec_Int_t * vIsop, int nVars )
   SeeAlso     []
 
 ***********************************************************************/
-int Cnf_SopWriteCube( char Cube, int * pVars, int fCompl, int * pLiterals )
-{
-    int nLits = 4, b;
-    for ( b = 0; b < 4; b++ )
-    {
-        if ( Cube % 3 == 0 )
-            *pLiterals++ = 2 * pVars[b] + !fCompl;
-        else if ( Cube % 3 == 1 )
-            *pLiterals++ = 2 * pVars[b] + fCompl;
-        else
-            nLits--;
-        Cube = Cube / 3;
-    }
-    return nLits;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Writes the cube and returns the number of literals in it.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Cnf_IsopWriteCube( int Cube, int nVars, int * pVars, int fCompl, int * pLiterals )
+int Cnf_IsopWriteCube( int Cube, int nVars, int * pVars, int * pLiterals )
 {
     int nLits = nVars, b;
     for ( b = 0; b < nVars; b++ )
     {
-        if ( (Cube & 3) == 1 )
-            *pLiterals++ = 2 * pVars[b] + !fCompl;
-        else if ( (Cube & 3) == 2 )
-            *pLiterals++ = 2 * pVars[b] + fCompl;
+        if ( (Cube & 3) == 1 ) // value 0 --> write positive literal
+            *pLiterals++ = 2 * pVars[b];
+        else if ( (Cube & 3) == 2 ) // value 1 --> write negative literal
+            *pLiterals++ = 2 * pVars[b] + 1;
         else
             nLits--;
         Cube >>= 2;
@@ -186,9 +159,10 @@ Cnf_Dat_t * Cnf_ManWriteCnf( Cnf_Man_t * p, Vec_Ptr_t * vMapped )
     Aig_Obj_t * pObj;
     Cnf_Dat_t * pCnf;
     Cnf_Cut_t * pCut;
+    Vec_Int_t * vCover, * vSopTemp;
     int OutVar, pVars[32], * pLits, ** pClas;
     unsigned uTruth;
-    int i, k, nLiterals, nClauses, nCubes, Cube, Number;
+    int i, k, nLiterals, nClauses, Cube, Number;
 
     // count the number of literals and clauses
     nLiterals = 1 + Aig_ManPoNum( p->pManAig );
@@ -249,6 +223,7 @@ Cnf_Dat_t * Cnf_ManWriteCnf( Cnf_Man_t * p, Vec_Ptr_t * vMapped )
     pCnf->nVars = Number;
 
     // assign the clauses
+    vSopTemp = Vec_IntAlloc( 1 << 16 );
     pLits = pCnf->pClauses[0];
     pClas = pCnf->pClauses;
     Vec_PtrForEachEntry( vMapped, pObj, i )
@@ -267,48 +242,36 @@ Cnf_Dat_t * Cnf_ManWriteCnf( Cnf_Man_t * p, Vec_Ptr_t * vMapped )
         if ( pCut->nFanins < 5 )
         {
             uTruth = 0xFFFF & *Cnf_CutTruth(pCut);
-            nCubes = p->pSopSizes[uTruth];
-            for ( k = 0; k < nCubes; k++ )
-            {
-                *pClas++ = pLits;
-                *pLits++ = 2 * OutVar + 1; 
-                pLits += Cnf_SopWriteCube( p->pSops[uTruth][k], pVars, 0, pLits );
-            }
+            Cnf_SopConvertToVector( p->pSops[uTruth], p->pSopSizes[uTruth], vSopTemp );
+            vCover = vSopTemp;
         }
         else
+            vCover = pCut->vIsop[1];
+        Vec_IntForEachEntry( vCover, Cube, k )
         {
-            Vec_IntForEachEntry( pCut->vIsop[1], Cube, k )
-            {
-                *pClas++ = pLits;
-                *pLits++ = 2 * OutVar + 1; 
-                pLits += Cnf_IsopWriteCube( Cube, pCut->nFanins, pVars, 0, pLits );
-            }
+            *pClas++ = pLits;
+            *pLits++ = 2 * OutVar; 
+            pLits += Cnf_IsopWriteCube( Cube, pCut->nFanins, pVars, pLits );
         }
 
         // negative polarity of the cut
         if ( pCut->nFanins < 5 )
         {
             uTruth = 0xFFFF & ~*Cnf_CutTruth(pCut);
-            nCubes = p->pSopSizes[uTruth];
-            for ( k = 0; k < nCubes; k++ )
-            {
-                *pClas++ = pLits;
-                *pLits++ = 2 * OutVar; 
-                pLits += Cnf_SopWriteCube( p->pSops[uTruth][k], pVars, 1, pLits );
-            }
+            Cnf_SopConvertToVector( p->pSops[uTruth], p->pSopSizes[uTruth], vSopTemp );
+            vCover = vSopTemp;
         }
         else
+            vCover = pCut->vIsop[0];
+        Vec_IntForEachEntry( vCover, Cube, k )
         {
-            Vec_IntForEachEntry( pCut->vIsop[0], Cube, k )
-            {
-                *pClas++ = pLits;
-                *pLits++ = 2 * OutVar; 
-                pLits += Cnf_IsopWriteCube( Cube, pCut->nFanins, pVars, 1, pLits );
-            }
+            *pClas++ = pLits;
+            *pLits++ = 2 * OutVar + 1; 
+            pLits += Cnf_IsopWriteCube( Cube, pCut->nFanins, pVars, pLits );
         }
-//printf( "%d ", pClas-pCnf->pClauses );
     }
-
+    Vec_IntFree( vSopTemp );
+ 
     // write the constant literal
     OutVar = pCnf->pVarNums[ Aig_ManConst1(p->pManAig)->Id ];
     assert( OutVar <= Aig_ManObjIdMax(p->pManAig) );
diff --git a/src/aig/dar/dar.h b/src/aig/dar/dar.h
index 3106c7ad..44dd2788 100644
--- a/src/aig/dar/dar.h
+++ b/src/aig/dar/dar.h
@@ -44,6 +44,7 @@ struct Dar_RwrPar_t_
 {
     int              nCutsMax;       // the maximum number of cuts to try
     int              nSubgMax;       // the maximum number of subgraphs to try
+    int              fFanout;        // support fanout representation
     int              fUpdateLevel;   // update level 
     int              fUseZeros;      // performs zero-cost replacement
     int              fVerbose;       // enables verbose output
@@ -79,12 +80,13 @@ extern Aig_Man_t *     Dar_ManBalance( Aig_Man_t * p, int fUpdateLevel );
 /*=== darCore.c ========================================================*/
 extern void            Dar_ManDefaultRwrParams( Dar_RwrPar_t * pPars );
 extern int             Dar_ManRewrite( Aig_Man_t * pAig, Dar_RwrPar_t * pPars );
-extern Aig_MmFixed_t * Dar_ManComputeCuts( Aig_Man_t * pAig );
+extern Aig_MmFixed_t * Dar_ManComputeCuts( Aig_Man_t * pAig, int nCutsMax );
 /*=== darRefact.c ========================================================*/
 extern void            Dar_ManDefaultRefParams( Dar_RefPar_t * pPars );
 extern int             Dar_ManRefactor( Aig_Man_t * pAig, Dar_RefPar_t * pPars );
 /*=== darScript.c ========================================================*/
-extern Aig_Man_t *     Dar_ManCompress2( Aig_Man_t * pAig, int fVerbose );
+extern Aig_Man_t *     Dar_ManCompress2( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fVerbose );
+extern Aig_Man_t *     Dar_ManRwsat( Aig_Man_t * pAig, int fBalance, int fVerbose );
 
 #ifdef __cplusplus
 }
diff --git a/src/aig/dar/darBalance.c b/src/aig/dar/darBalance.c
index 969e5253..097f1a4d 100644
--- a/src/aig/dar/darBalance.c
+++ b/src/aig/dar/darBalance.c
@@ -53,7 +53,7 @@ Aig_Man_t * Dar_ManBalance( Aig_Man_t * p, int fUpdateLevel )
     Vec_Vec_t * vStore;
     int i;
     // create the new manager 
-    pNew = Aig_ManStart();
+    pNew = Aig_ManStart( Aig_ManObjIdMax(p) + 1 );
     // map the PI nodes
     Aig_ManCleanData( p );
     Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
diff --git a/src/aig/dar/darCore.c b/src/aig/dar/darCore.c
index 7546df0b..b74f570c 100644
--- a/src/aig/dar/darCore.c
+++ b/src/aig/dar/darCore.c
@@ -44,6 +44,7 @@ void Dar_ManDefaultRwrParams( Dar_RwrPar_t * pPars )
     memset( pPars, 0, sizeof(Dar_RwrPar_t) );
     pPars->nCutsMax     =  8;
     pPars->nSubgMax     =  5; // 5 is a "magic number"
+    pPars->fFanout      =  1;
     pPars->fUpdateLevel =  0;
     pPars->fUseZeros    =  0;
     pPars->fVerbose     =  0;
@@ -76,7 +77,8 @@ int Dar_ManRewrite( Aig_Man_t * pAig, Dar_RwrPar_t * pPars )
     // remove dangling nodes
     Aig_ManCleanup( pAig );
     // if updating levels is requested, start fanout and timing
-    Aig_ManCreateFanout( pAig );
+    if ( p->pPars->fFanout )
+        Aig_ManFanoutStart( pAig );
     if ( p->pPars->fUpdateLevel )
         Aig_ManStartReverseLevels( pAig, 0 );
     // set elementary cuts for the PIs
@@ -85,19 +87,27 @@ int Dar_ManRewrite( Aig_Man_t * pAig, Dar_RwrPar_t * pPars )
     clkStart = clock();
     p->nNodesInit = Aig_ManNodeNum(pAig);
     nNodesOld = Vec_PtrSize( pAig->vObjs );
+
     pProgress = Extra_ProgressBarStart( stdout, nNodesOld );
     Aig_ManForEachObj( pAig, pObj, i )
+//    pProgress = Extra_ProgressBarStart( stdout, 100 );
+//    Aig_ManOrderStart( pAig );
+//    Aig_ManForEachNodeInOrder( pAig, pObj )
     {
+//        Extra_ProgressBarUpdate( pProgress, 100*pAig->nAndPrev/pAig->nAndTotal, NULL );
+
         Extra_ProgressBarUpdate( pProgress, i, NULL );
         if ( !Aig_ObjIsNode(pObj) )
             continue;
         if ( i > nNodesOld )
             break;
+
         // consider freeing the cuts
 //        if ( (i & 0xFFF) == 0 && Aig_MmFixedReadMemUsage(p->pMemCuts)/(1<<20) > 100 )
 //            Dar_ManCutsStart( p );
 
         // compute cuts for the node
+        p->nNodesTried++;
 clk = clock();
         Dar_ObjComputeCuts_rec( p, pObj );
 p->timeCuts += clock() - clk;
@@ -133,7 +143,10 @@ p->timeCuts += clock() - clk;
             Dar_LibEval( p, pObj, pCut, Required );
         // check the best gain
         if ( !(p->GainBest > 0 || (p->GainBest == 0 && p->pPars->fUseZeros)) )
+        {
+//            Aig_ObjOrderAdvance( pAig );
             continue;
+        }
         // remove the old cuts
         Dar_ObjSetCuts( pObj, NULL );
         // if we end up here, a rewriting step is accepted
@@ -149,6 +162,8 @@ p->timeCuts += clock() - clk;
         // count gains of this class
         p->ClassGains[p->ClassBest] += nNodeBefore - nNodeAfter;
     }
+//    Aig_ManOrderStop( pAig );
+
 p->timeTotal = clock() - clkStart;
 p->timeOther = p->timeTotal - p->timeCuts - p->timeEval;
 
@@ -158,9 +173,14 @@ p->timeOther = p->timeTotal - p->timeCuts - p->timeEval;
     // put the nodes into the DFS order and reassign their IDs
 //    Aig_NtkReassignIds( p );
     // fix the levels
-    Aig_ManDeleteFanout( pAig );
+//    Aig_ManVerifyLevel( pAig );
+    if ( p->pPars->fFanout )
+        Aig_ManFanoutStop( pAig );
     if ( p->pPars->fUpdateLevel )
+    {
+//        Aig_ManVerifyReverseLevel( pAig );
         Aig_ManStopReverseLevels( pAig );
+    }
     // stop the rewriting manager
     Dar_ManStop( p );
     // check
@@ -183,28 +203,25 @@ p->timeOther = p->timeTotal - p->timeCuts - p->timeEval;
   SeeAlso     []
 
 ***********************************************************************/
-Aig_MmFixed_t * Dar_ManComputeCuts( Aig_Man_t * pAig )
+Aig_MmFixed_t * Dar_ManComputeCuts( Aig_Man_t * pAig, int nCutsMax )
 {
     Dar_Man_t * p;
+    Dar_RwrPar_t Pars, * pPars = &Pars; 
     Aig_Obj_t * pObj;
     Aig_MmFixed_t * pMemCuts;
     int i, clk = 0, clkStart = clock();
-    int nCutsMax = 0, nCutsTotal = 0;
-    // create rewriting manager
-    p = Dar_ManStart( pAig, NULL );
     // remove dangling nodes
     Aig_ManCleanup( pAig );
+    // create default parameters
+    Dar_ManDefaultRwrParams( pPars );
+    pPars->nCutsMax = nCutsMax;
+    // create rewriting manager
+    p = Dar_ManStart( pAig, pPars );
     // set elementary cuts for the PIs
     Dar_ManCutsStart( p );
     // compute cuts for each nodes in the topological order
-    Aig_ManForEachObj( pAig, pObj, i )
-    {
-        if ( !Aig_ObjIsNode(pObj) )
-            continue;
+    Aig_ManForEachNode( pAig, pObj, i )
         Dar_ObjComputeCuts( p, pObj );
-        nCutsTotal += pObj->nCuts - 1;
-        nCutsMax = AIG_MAX( nCutsMax, (int)pObj->nCuts - 1 );
-    }
     // free the cuts
     pMemCuts = p->pMemCuts;
     p->pMemCuts = NULL;
diff --git a/src/aig/dar/darInt.h b/src/aig/dar/darInt.h
index 0acd272c..b14d5c30 100644
--- a/src/aig/dar/darInt.h
+++ b/src/aig/dar/darInt.h
@@ -55,7 +55,8 @@ struct Dar_Cut_t_  // 6 words
 {
     unsigned         uSign;          // cut signature
     unsigned         uTruth  : 16;   // the truth table of the cut function
-    unsigned         Value   : 12;   // the value of the cut 
+    unsigned         Value   : 11;   // the value of the cut 
+    unsigned         fBest   :  1;   // marks the best cut
     unsigned         fUsed   :  1;   // marks the cut currently in use
     unsigned         nLeaves :  3;   // the number of leaves
     int              pLeaves[4];     // the array of leaves
@@ -85,6 +86,7 @@ struct Dar_Man_t_
     int              nCutMemUsed;    // memory used for cuts
     // rewriting statistics
     int              nNodesInit;     // the original number of nodes
+    int              nNodesTried;    // the number of nodes attempted
     int              nCutsAll;       // all cut pairs
     int              nCutsTried;     // computed cuts
     int              nCutsUsed;      // used cuts
diff --git a/src/aig/dar/darLib.c b/src/aig/dar/darLib.c
index 72ce0cde..e159f35a 100644
--- a/src/aig/dar/darLib.c
+++ b/src/aig/dar/darLib.c
@@ -798,9 +798,13 @@ void Dar_LibEvalAssignNums( Dar_Man_t * p, int Class )
         pFanin0 = Aig_NotCond( pData0->pFunc, pObj->fCompl0 );
         pFanin1 = Aig_NotCond( pData1->pFunc, pObj->fCompl1 );
         pData->pFunc = Aig_TableLookupTwo( p->pAig, pFanin0, pFanin1 );
-        // clear the node if it is part of MFFC
-        if ( pData->pFunc != NULL && Aig_ObjIsTravIdCurrent(p->pAig, pData->pFunc) )
-            pData->fMffc = 1;
+        if ( pData->pFunc )
+        {
+            // update the level to be more accurate
+            pData->Level = Aig_Regular(pData->pFunc)->Level;
+            // mark the node if it is part of MFFC
+            pData->fMffc = Aig_ObjIsTravIdCurrent(p->pAig, pData->pFunc);
+        }
     }
 }
 
@@ -823,10 +827,10 @@ int Dar_LibEval_rec( Dar_LibObj_t * pObj, int Out, int nNodesSaved, int Required
         return 0;
     assert( pObj->Num > 3 );
     pData = s_DarLib->pDatas + pObj->Num;
-    if ( pData->pFunc && !pData->fMffc )
-        return 0;
     if ( pData->Level > Required )
         return 0xff;
+    if ( pData->pFunc && !pData->fMffc )
+        return 0;
     if ( pData->TravId == Out )
         return 0;
     pData->TravId = Out;
@@ -894,6 +898,7 @@ void Dar_LibEval( Dar_Man_t * p, Aig_Obj_t * pRoot, Dar_Cut_t * pCut, int Requir
         p->LevelBest  = s_DarLib->pDatas[pObj->Num].Level;
         p->GainBest   = nNodesGained;
         p->ClassBest  = Class;
+        assert( p->LevelBest <= Required );
     }
 clk = clock() - clk;
 p->ClassTimes[Class] += clk;
@@ -943,6 +948,7 @@ Aig_Obj_t * Dar_LibBuildBest_rec( Dar_Man_t * p, Dar_LibObj_t * pObj )
     pFanin0 = Aig_NotCond( pFanin0, pObj->fCompl0 );
     pFanin1 = Aig_NotCond( pFanin1, pObj->fCompl1 );
     pData->pFunc = Aig_And( p->pAig, pFanin0, pFanin1 );
+//    assert( pData->Level == (int)Aig_Regular(pData->pFunc)->Level );
     return pData->pFunc;
 }
 
diff --git a/src/aig/dar/darMan.c b/src/aig/dar/darMan.c
index ef898ea2..155d48bd 100644
--- a/src/aig/dar/darMan.c
+++ b/src/aig/dar/darMan.c
@@ -94,14 +94,14 @@ void Dar_ManPrintStats( Dar_Man_t * p )
     extern void Kit_DsdPrintFromTruth( unsigned * pTruth, int nVars );
 
     Gain = p->nNodesInit - Aig_ManNodeNum(p->pAig);
-    printf( "NodesBeg = %8d. NodesEnd = %8d. Gain = %6d. (%6.2f %%).  Cut mem = %d Mb\n", 
-        p->nNodesInit, Aig_ManNodeNum(p->pAig), Gain, 100.0*Gain/p->nNodesInit, p->nCutMemUsed );
+    printf( "Tried = %8d. Beg = %8d. End = %8d. Gain = %6d. (%6.2f %%).  Cut mem = %d Mb\n", 
+        p->nNodesTried, p->nNodesInit, Aig_ManNodeNum(p->pAig), Gain, 100.0*Gain/p->nNodesInit, p->nCutMemUsed );
     printf( "Cuts = %8d. Tried = %8d. Used = %8d. Bad = %5d. Skipped = %5d. Ave = %.2f.\n", 
         p->nCutsAll, p->nCutsTried, p->nCutsUsed, p->nCutsBad, p->nCutsSkipped,
         (float)p->nCutsUsed/Aig_ManNodeNum(p->pAig) );
 
-    printf( "Bufs = %5d. BufMax = %5d. BufReplace = %6d. BufFix = %6d.\n", 
-        Aig_ManBufNum(p->pAig), p->pAig->nBufMax, p->pAig->nBufReplaces, p->pAig->nBufFixes );
+    printf( "Bufs = %5d. BufMax = %5d. BufReplace = %6d. BufFix = %6d.  Levels = %4d.\n", 
+        Aig_ManBufNum(p->pAig), p->pAig->nBufMax, p->pAig->nBufReplaces, p->pAig->nBufFixes, Aig_ManLevels(p->pAig) );
     PRT( "Cuts  ", p->timeCuts );
     PRT( "Eval  ", p->timeEval );
     PRT( "Other ", p->timeOther );
diff --git a/src/aig/dar/darRefact.c b/src/aig/dar/darRefact.c
index cdfbaa01..fbd12cae 100644
--- a/src/aig/dar/darRefact.c
+++ b/src/aig/dar/darRefact.c
@@ -130,8 +130,8 @@ void Dar_ManRefPrintStats( Ref_Man_t * p )
     int Gain = p->nNodesInit - Aig_ManNodeNum(p->pAig);
     printf( "NodesBeg = %8d. NodesEnd = %8d. Gain = %6d. (%6.2f %%).\n", 
         p->nNodesInit, Aig_ManNodeNum(p->pAig), Gain, 100.0*Gain/p->nNodesInit );
-    printf( "Tried = %6d. Below = %5d. Extended = %5d.  Used = %5d.\n", 
-        p->nNodesTried, p->nNodesBelow, p->nNodesExten, p->nCutsUsed );
+    printf( "Tried = %6d. Below = %5d. Extended = %5d.  Used = %5d.  Levels = %4d.\n", 
+        p->nNodesTried, p->nNodesBelow, p->nNodesExten, p->nCutsUsed, Aig_ManLevels(p->pAig) );
     PRT( "Cuts  ", p->timeCuts );
     PRT( "Eval  ", p->timeEval );
     PRT( "Other ", p->timeOther );
@@ -358,7 +358,7 @@ int Dar_ManRefactorTryCuts( Ref_Man_t * p, Aig_Obj_t * pObj, int nNodesSaved, in
 
         p->nCutsTried++;
         // get the cut nodes
-        Aig_ManCollectCut( pObj, vCut, p->vCutNodes );
+        Aig_ObjCollectCut( pObj, vCut, p->vCutNodes );
         // get the truth table
         pTruth = Aig_ManCutTruth( pObj, vCut, p->vCutNodes, p->vTruthElem, p->vTruthStore );
         // try the positive phase
@@ -460,7 +460,7 @@ int Dar_ManRefactor( Aig_Man_t * pAig, Dar_RefPar_t * pPars )
     // remove dangling nodes
     Aig_ManCleanup( pAig );
     // if updating levels is requested, start fanout and timing
-    Aig_ManCreateFanout( pAig );
+    Aig_ManFanoutStart( pAig );
     if ( p->pPars->fUpdateLevel )
         Aig_ManStartReverseLevels( pAig, 0 );
 
@@ -480,11 +480,6 @@ int Dar_ManRefactor( Aig_Man_t * pAig, Dar_RefPar_t * pPars )
             break;
         Vec_VecClear( p->vCuts );
 
-        if ( pObj->Id == 738 )
-        {
-            int x = 0;
-        }
-
 //printf( "\nConsidering node %d.\n", pObj->Id );
         // get the bounded MFFC size
 clk = clock();
@@ -558,7 +553,7 @@ p->timeOther = p->timeTotal - p->timeCuts - p->timeEval;
     // put the nodes into the DFS order and reassign their IDs
 //    Aig_NtkReassignIds( p );
     // fix the levels
-    Aig_ManDeleteFanout( pAig );
+    Aig_ManFanoutStop( pAig );
     if ( p->pPars->fUpdateLevel )
         Aig_ManStopReverseLevels( pAig );
 
diff --git a/src/aig/dar/darScript.c b/src/aig/dar/darScript.c
index 8423a4e6..75076981 100644
--- a/src/aig/dar/darScript.c
+++ b/src/aig/dar/darScript.c
@@ -39,11 +39,10 @@
   SeeAlso     []
 
 ***********************************************************************/
-Aig_Man_t * Dar_ManCompress2_old( Aig_Man_t * pAig, int fVerbose )
+Aig_Man_t * Dar_ManCompress2( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fVerbose )
 //alias compress2   "b -l; rw -l; rf -l; b -l; rw -l; rwz -l; b -l; rfz -l; rwz -l; b -l"
 {
     Aig_Man_t * pTemp;
-    int fBalance = 0;
 
     Dar_RwrPar_t ParsRwr, * pParsRwr = &ParsRwr;
     Dar_RefPar_t ParsRef, * pParsRef = &ParsRef;
@@ -51,12 +50,18 @@ Aig_Man_t * Dar_ManCompress2_old( Aig_Man_t * pAig, int fVerbose )
     Dar_ManDefaultRwrParams( pParsRwr );
     Dar_ManDefaultRefParams( pParsRef );
 
+    pParsRwr->fUpdateLevel = fUpdateLevel;
+    pParsRef->fUpdateLevel = fUpdateLevel;
+
     pParsRwr->fVerbose = fVerbose;
     pParsRef->fVerbose = fVerbose;
 
     // balance
-    pAig = Dar_ManBalance( pTemp = pAig, fBalance );
-    Aig_ManStop( pTemp );
+    if ( fBalance )
+    {
+//    pAig = Dar_ManBalance( pTemp = pAig, fUpdateLevel );
+//    Aig_ManStop( pTemp );
+    }
     
     // rewrite
     Dar_ManRewrite( pAig, pParsRwr );
@@ -69,8 +74,11 @@ Aig_Man_t * Dar_ManCompress2_old( Aig_Man_t * pAig, int fVerbose )
     Aig_ManStop( pTemp );
 
     // balance
-    pAig = Dar_ManBalance( pTemp = pAig, fBalance );
+//    if ( fBalance )
+    {
+    pAig = Dar_ManBalance( pTemp = pAig, fUpdateLevel );
     Aig_ManStop( pTemp );
+    }
     
     // rewrite
     Dar_ManRewrite( pAig, pParsRwr );
@@ -86,8 +94,11 @@ Aig_Man_t * Dar_ManCompress2_old( Aig_Man_t * pAig, int fVerbose )
     Aig_ManStop( pTemp );
 
     // balance
-    pAig = Dar_ManBalance( pTemp = pAig, fBalance );
+    if ( fBalance )
+    {
+    pAig = Dar_ManBalance( pTemp = pAig, fUpdateLevel );
     Aig_ManStop( pTemp );
+    }
     
     // refactor
     Dar_ManRefactor( pAig, pParsRef );
@@ -100,8 +111,11 @@ Aig_Man_t * Dar_ManCompress2_old( Aig_Man_t * pAig, int fVerbose )
     Aig_ManStop( pTemp );
 
     // balance
-    pAig = Dar_ManBalance( pTemp = pAig, fBalance );
+    if ( fBalance )
+    {
+    pAig = Dar_ManBalance( pTemp = pAig, fUpdateLevel );
     Aig_ManStop( pTemp );
+    }
     return pAig;
 }
 
@@ -116,11 +130,10 @@ Aig_Man_t * Dar_ManCompress2_old( Aig_Man_t * pAig, int fVerbose )
   SeeAlso     []
 
 ***********************************************************************/
-Aig_Man_t * Dar_ManCompress2_no_z( Aig_Man_t * pAig, int fVerbose )
-//alias compress2   "b -l; rw -l; rf -l; b -l; rw -l; rwz -l; b -l; rfz -l; rwz -l; b -l"
+Aig_Man_t * Dar_ManRwsat( Aig_Man_t * pAig, int fBalance, int fVerbose )
+//alias rwsat       "st; rw -l; b -l; rw -l; rf -l"
 {
     Aig_Man_t * pTemp;
-    int fBalance = 0;
 
     Dar_RwrPar_t ParsRwr, * pParsRwr = &ParsRwr;
     Dar_RefPar_t ParsRef, * pParsRef = &ParsRef;
@@ -128,71 +141,8 @@ Aig_Man_t * Dar_ManCompress2_no_z( Aig_Man_t * pAig, int fVerbose )
     Dar_ManDefaultRwrParams( pParsRwr );
     Dar_ManDefaultRefParams( pParsRef );
 
-    pParsRwr->fVerbose = fVerbose;
-    pParsRef->fVerbose = fVerbose;
-    
-    // rewrite
-    Dar_ManRewrite( pAig, pParsRwr );
-    pAig = Aig_ManDup( pTemp = pAig, 0 ); 
-    Aig_ManStop( pTemp );
-    
-    // refactor
-    Dar_ManRefactor( pAig, pParsRef );
-    pAig = Aig_ManDup( pTemp = pAig, 0 ); 
-    Aig_ManStop( pTemp );
-
-    // balance
-    pAig = Dar_ManBalance( pTemp = pAig, fBalance );
-    Aig_ManStop( pTemp );
-    
-    // rewrite
-    Dar_ManRewrite( pAig, pParsRwr );
-    pAig = Aig_ManDup( pTemp = pAig, 0 ); 
-    Aig_ManStop( pTemp );
-    
-    // refactor
-    Dar_ManRefactor( pAig, pParsRef );
-    pAig = Aig_ManDup( pTemp = pAig, 0 ); 
-    Aig_ManStop( pTemp );
-
-    // balance
-    pAig = Dar_ManBalance( pTemp = pAig, fBalance );
-    Aig_ManStop( pTemp );
-    
-    // rewrite
-    Dar_ManRewrite( pAig, pParsRwr );
-    pAig = Aig_ManDup( pTemp = pAig, 0 ); 
-    Aig_ManStop( pTemp );
-    
-    // refactor
-    Dar_ManRefactor( pAig, pParsRef );
-    pAig = Aig_ManDup( pTemp = pAig, 0 ); 
-    Aig_ManStop( pTemp );
-    return pAig;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Reproduces script "compress2".]
-
-  Description []
-               
-  SideEffects [This procedure does not tighten level during restructuring.]
-
-  SeeAlso     []
-
-***********************************************************************/
-Aig_Man_t * Dar_ManCompress2( Aig_Man_t * pAig, int fVerbose )
-//alias compress2   "b -l; rw -l; rf -l; b -l; rw -l; rwz -l; b -l; rfz -l; rwz -l; b -l"
-{
-    Aig_Man_t * pTemp;
-    int fBalance = 0;
-
-    Dar_RwrPar_t ParsRwr, * pParsRwr = &ParsRwr;
-    Dar_RefPar_t ParsRef, * pParsRef = &ParsRef;
-
-    Dar_ManDefaultRwrParams( pParsRwr );
-    Dar_ManDefaultRefParams( pParsRef );
+    pParsRwr->fUpdateLevel = 0;
+    pParsRef->fUpdateLevel = 0;
 
     pParsRwr->fVerbose = fVerbose;
     pParsRef->fVerbose = fVerbose;
@@ -206,37 +156,19 @@ Aig_Man_t * Dar_ManCompress2( Aig_Man_t * pAig, int fVerbose )
     Dar_ManRefactor( pAig, pParsRef );
     pAig = Aig_ManDup( pTemp = pAig, 0 ); 
     Aig_ManStop( pTemp );
-/*
-    // balance
-    pAig = Dar_ManBalance( pTemp = pAig, fBalance );
-    Aig_ManStop( pTemp );
-*/    
-    // rewrite
-    Dar_ManRewrite( pAig, pParsRwr );
-    pAig = Aig_ManDup( pTemp = pAig, 0 ); 
-    Aig_ManStop( pTemp );
-
-    pParsRwr->fUseZeros = 1;
-    pParsRef->fUseZeros = 1;
-    
-    // rewrite
-    Dar_ManRewrite( pAig, pParsRwr );
-    pAig = Aig_ManDup( pTemp = pAig, 0 ); 
-    Aig_ManStop( pTemp );
 
     // balance
-    pAig = Dar_ManBalance( pTemp = pAig, fBalance );
-    Aig_ManStop( pTemp );
-    
-    // refactor
-    Dar_ManRefactor( pAig, pParsRef );
-    pAig = Aig_ManDup( pTemp = pAig, 0 ); 
+    if ( fBalance )
+    {
+    pAig = Dar_ManBalance( pTemp = pAig, 0 );
     Aig_ManStop( pTemp );
+    }
     
     // rewrite
     Dar_ManRewrite( pAig, pParsRwr );
     pAig = Aig_ManDup( pTemp = pAig, 0 ); 
     Aig_ManStop( pTemp );
+
     return pAig;
 }
 
diff --git a/src/aig/fra/fra.h b/src/aig/fra/fra.h
index 7f2df105..127882ea 100644
--- a/src/aig/fra/fra.h
+++ b/src/aig/fra/fra.h
@@ -60,6 +60,7 @@ struct Fra_Par_t_
     int              MaxScore;          // max score after which resimulation is used
     double           dActConeRatio;     // the ratio of cone to be bumped
     double           dActConeBumpMax;   // the largest bump in activity
+    int              fChoicing;         // enables choicing
     int              fSpeculate;        // use speculative reduction
     int              fProve;            // prove the miter outputs
     int              fVerbose;          // verbose output
@@ -101,6 +102,7 @@ struct Fra_Man_t_
     // various data members
     Aig_Obj_t **     pMemFraig;         // memory allocated for points to the fraig nodes
     Aig_Obj_t **     pMemRepr;          // memory allocated for points to the node representatives
+    Aig_Obj_t **     pMemReprFra;       // memory allocated for points to the node representatives in the FRAIG
     Vec_Ptr_t **     pMemFanins;        // the arrays of fanins
     int *            pMemSatNums;       // the array of SAT numbers
     int              nSizeAlloc;        // allocated size of the arrays
@@ -118,7 +120,9 @@ struct Fra_Man_t_
     int              nSatProof;
     int              nSatFails;
     int              nSatFailsReal;
-    int              nSpeculs;         
+    int              nSpeculs;   
+    int              nChoices;
+    int              nChoicesFake;
     // runtime
     int              timeSim;
     int              timeTrav;
@@ -141,11 +145,13 @@ static inline unsigned     Fra_ObjRandomSim()               { return (rand() <<
 
 static inline Aig_Obj_t *  Fra_ObjFraig( Aig_Obj_t * pObj )                              { return ((Fra_Man_t *)pObj->pData)->pMemFraig[pObj->Id];       }
 static inline Aig_Obj_t *  Fra_ObjRepr( Aig_Obj_t * pObj )                               { return ((Fra_Man_t *)pObj->pData)->pMemRepr[pObj->Id];        }
+static inline Aig_Obj_t *  Fra_ObjReprFra( Aig_Obj_t * pObj )                            { return ((Fra_Man_t *)pObj->pData)->pMemReprFra[pObj->Id];     }
 static inline Vec_Ptr_t *  Fra_ObjFaninVec( Aig_Obj_t * pObj )                           { return ((Fra_Man_t *)pObj->pData)->pMemFanins[pObj->Id];      }
 static inline int          Fra_ObjSatNum( Aig_Obj_t * pObj )                             { return ((Fra_Man_t *)pObj->pData)->pMemSatNums[pObj->Id];     }
 
 static inline void         Fra_ObjSetFraig( Aig_Obj_t * pObj, Aig_Obj_t * pNode )        { ((Fra_Man_t *)pObj->pData)->pMemFraig[pObj->Id]   = pNode;    }
 static inline void         Fra_ObjSetRepr( Aig_Obj_t * pObj, Aig_Obj_t * pNode )         { ((Fra_Man_t *)pObj->pData)->pMemRepr[pObj->Id]    = pNode;    }
+static inline void         Fra_ObjSetReprFra( Aig_Obj_t * pObj, Aig_Obj_t * pNode )      { ((Fra_Man_t *)pObj->pData)->pMemReprFra[pObj->Id] = pNode;    }
 static inline void         Fra_ObjSetFaninVec( Aig_Obj_t * pObj, Vec_Ptr_t * vFanins )   { ((Fra_Man_t *)pObj->pData)->pMemFanins[pObj->Id]  = vFanins;  }
 static inline void         Fra_ObjSetSatNum( Aig_Obj_t * pObj, int Num )                 { ((Fra_Man_t *)pObj->pData)->pMemSatNums[pObj->Id] = Num;      }
 
@@ -160,8 +166,6 @@ static inline Aig_Obj_t *  Fra_ObjChild1Fra( Aig_Obj_t * pObj ) { assert( !Aig_I
 ///                    FUNCTION DECLARATIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
-/*=== fraAnd.c ========================================================*/
-extern void                Fra_Sweep( Fra_Man_t * p );
 /*=== fraClass.c ========================================================*/
 extern void                Fra_PrintClasses( Fra_Man_t * p );
 extern void                Fra_CreateClasses( Fra_Man_t * p );
@@ -170,7 +174,10 @@ extern int                 Fra_RefineClasses1( Fra_Man_t * p );
 /*=== fraCnf.c ========================================================*/
 extern void                Fra_NodeAddToSolver( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew );
 /*=== fraCore.c ========================================================*/
-extern Aig_Man_t *         Fra_Perform( Aig_Man_t * pManAig, Fra_Par_t * pParams );
+extern Aig_Man_t *         Fra_Perform( Aig_Man_t * pManAig, Fra_Par_t * pPars );
+extern Aig_Man_t *         Fra_Choice( Aig_Man_t * pManAig );
+/*=== fraDfs.c ========================================================*/
+extern int                 Fra_CheckTfi( Fra_Man_t * p, Aig_Obj_t * pNew, Aig_Obj_t * pOld );
 /*=== fraMan.c ========================================================*/
 extern void                Fra_ParamsDefault( Fra_Par_t * pParams );
 extern Fra_Man_t *         Fra_ManStart( Aig_Man_t * pManAig, Fra_Par_t * pParams );
diff --git a/src/aig/fra/fraAnd.c b/src/aig/fra/fraAnd.c
deleted file mode 100644
index 36b4ccc3..00000000
--- a/src/aig/fra/fraAnd.c
+++ /dev/null
@@ -1,156 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [fraAnd.c]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [Fraig FRAIG package.]
-
-  Synopsis    []
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - June 30, 2007.]
-
-  Revision    [$Id: fraAnd.c,v 1.00 2007/06/30 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "fra.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-
-/**Function*************************************************************
-
-  Synopsis    [Performs fraiging for one node.]
-
-  Description [Returns the fraiged node.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Aig_Obj_t * Fra_And( Fra_Man_t * p, Aig_Obj_t * pObjOld )
-{ 
-    Aig_Obj_t * pObjOldRepr, * pObjFraig, * pFanin0Fraig, * pFanin1Fraig, * pObjOldReprFraig;
-    int RetValue;
-    assert( !Aig_IsComplement(pObjOld) );
-    assert( Aig_ObjIsNode(pObjOld) );
-    // get the fraiged fanins
-    pFanin0Fraig = Fra_ObjChild0Fra(pObjOld);
-    pFanin1Fraig = Fra_ObjChild1Fra(pObjOld);
-    // get the fraiged node
-    pObjFraig = Aig_And( p->pManFraig, pFanin0Fraig, pFanin1Fraig );
-    if ( Aig_ObjIsConst1(Aig_Regular(pObjFraig)) )
-        return pObjFraig;
-    Aig_Regular(pObjFraig)->pData = p;
-    // get representative of this class
-    pObjOldRepr = Fra_ObjRepr(pObjOld);
-    if ( pObjOldRepr == NULL || // this is a unique node
-       (!p->pPars->fDoSparse && pObjOldRepr == Aig_ManConst1(p->pManAig)) ) // this is a sparse node
-    {
-        assert( Aig_Regular(pFanin0Fraig) != Aig_Regular(pFanin1Fraig) );
-        assert( Aig_Regular(pObjFraig) != Aig_Regular(pFanin0Fraig) );
-        assert( Aig_Regular(pObjFraig) != Aig_Regular(pFanin1Fraig) );
-        return pObjFraig;
-    }
-    // get the fraiged representative
-    pObjOldReprFraig = Fra_ObjFraig(pObjOldRepr);
-    // if the fraiged nodes are the same, return
-    if ( Aig_Regular(pObjFraig) == Aig_Regular(pObjOldReprFraig) )
-        return pObjFraig;
-    assert( Aig_Regular(pObjFraig) != Aig_ManConst1(p->pManFraig) );
-//    printf( "Node = %d. Repr = %d.\n", pObjOld->Id, pObjOldRepr->Id );
-
-    // if they are proved different, the c-ex will be in p->pPatWords
-    RetValue = Fra_NodesAreEquiv( p, Aig_Regular(pObjOldReprFraig), Aig_Regular(pObjFraig) );
-    if ( RetValue == 1 )  // proved equivalent
-    {
-//        pObjOld->fMarkA = 1;
-        return Aig_NotCond( pObjOldReprFraig, pObjOld->fPhase ^ pObjOldRepr->fPhase );
-    }
-    if ( RetValue == -1 ) // failed
-    {
-        Aig_Obj_t * ppNodes[2] = { Aig_Regular(pObjOldReprFraig), Aig_Regular(pObjFraig) };
-        Vec_Ptr_t * vNodes;
-
-        if ( !p->pPars->fSpeculate )
-            return pObjFraig;
-        // substitute the node
-//        pObjOld->fMarkB = 1;
-        p->nSpeculs++;
-
-        vNodes = Aig_ManDfsNodes( p->pManFraig, ppNodes, 2 );
-        printf( "%d ", Vec_PtrSize(vNodes) );
-        Vec_PtrFree( vNodes );
-
-        return Aig_NotCond( pObjOldReprFraig, pObjOld->fPhase ^ pObjOldRepr->fPhase );
-    }
-//    printf( "Disproved %d and %d.\n", pObjOldRepr->Id, pObjOld->Id );
-    // simulate the counter-example and return the Fraig node
-//    printf( "Representaive before = %d.\n", Fra_ObjRepr(pObjOld)? Fra_ObjRepr(pObjOld)->Id : -1 );
-    Fra_Resimulate( p );
-//    printf( "Representaive after  = %d.\n", Fra_ObjRepr(pObjOld)? Fra_ObjRepr(pObjOld)->Id : -1 );
-    assert( Fra_ObjRepr(pObjOld) != pObjOldRepr );
-    return pObjFraig;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Performs fraiging for the internal nodes.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fra_Sweep( Fra_Man_t * p )
-{
-    Aig_Obj_t * pObj, * pObjNew;
-    int i, k = 0;
-p->nClassesZero = Vec_PtrSize(p->vClasses1);
-p->nClassesBeg  = Vec_PtrSize(p->vClasses) + (int)(Vec_PtrSize(p->vClasses1) > 0);
-    // duplicate internal nodes
-//    p->pProgress = Extra_ProgressBarStart( stdout, Aig_ManNodeNum(p->pManAig) );
-    Aig_ManForEachNode( p->pManAig, pObj, i )
-    {
-//        Extra_ProgressBarUpdate( p->pProgress, k++, NULL );
-        // default to simple strashing if simulation detected a counter-example for a PO
-        if ( p->pManFraig->pData )
-            pObjNew = Aig_And( p->pManFraig, Fra_ObjChild0Fra(pObj), Fra_ObjChild1Fra(pObj) );
-        else
-            pObjNew = Fra_And( p, pObj ); // pObjNew can be complemented
-        Fra_ObjSetFraig( pObj, pObjNew );
-        assert( Fra_ObjFraig(pObj) != NULL );
-    }
-//    Extra_ProgressBarStop( p->pProgress );
-p->nClassesEnd = Vec_PtrSize(p->vClasses) + (int)(Vec_PtrSize(p->vClasses1) > 0);
-    // try to prove the outputs of the miter
-    p->nNodesMiter = Aig_ManNodeNum(p->pManFraig);
-//    Fra_MiterStatus( p->pManFraig );
-//    if ( p->pPars->fProve && p->pManFraig->pData == NULL )
-//        Fra_MiterProve( p );
-    // add the POs
-    Aig_ManForEachPo( p->pManAig, pObj, i )
-        Aig_ObjCreatePo( p->pManFraig, Fra_ObjChild0Fra(pObj) );
-    // remove dangling nodes 
-    Aig_ManCleanup( p->pManFraig );
-}
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/aig/fra/fraCore.c b/src/aig/fra/fraCore.c
index 9e1a9a1a..ca2d0fb4 100644
--- a/src/aig/fra/fraCore.c
+++ b/src/aig/fra/fraCore.c
@@ -30,6 +30,177 @@
 
 /**Function*************************************************************
 
+  Synopsis    [Performs fraiging for one node.]
+
+  Description [Returns the fraiged node.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Obj_t * Fra_And( Fra_Man_t * p, Aig_Obj_t * pObjOld )
+{ 
+    Aig_Obj_t * pObjOldRepr, * pObjFraig, * pFanin0Fraig, * pFanin1Fraig, * pObjOldReprFraig;
+    int RetValue;
+    assert( !Aig_IsComplement(pObjOld) );
+    assert( Aig_ObjIsNode(pObjOld) );
+    // get the fraiged fanins
+    pFanin0Fraig = Fra_ObjChild0Fra(pObjOld);
+    pFanin1Fraig = Fra_ObjChild1Fra(pObjOld);
+    // get the fraiged node
+    pObjFraig = Aig_And( p->pManFraig, pFanin0Fraig, pFanin1Fraig );
+    if ( Aig_ObjIsConst1(Aig_Regular(pObjFraig)) )
+        return pObjFraig;
+    Aig_Regular(pObjFraig)->pData = p;
+    // get representative of this class
+    pObjOldRepr = Fra_ObjRepr(pObjOld);
+    if ( pObjOldRepr == NULL || // this is a unique node
+       (!p->pPars->fDoSparse && pObjOldRepr == Aig_ManConst1(p->pManAig)) ) // this is a sparse node
+    {
+        assert( Aig_Regular(pFanin0Fraig) != Aig_Regular(pFanin1Fraig) );
+        assert( Aig_Regular(pObjFraig) != Aig_Regular(pFanin0Fraig) );
+        assert( Aig_Regular(pObjFraig) != Aig_Regular(pFanin1Fraig) );
+        return pObjFraig;
+    }
+    // get the fraiged representative
+    pObjOldReprFraig = Fra_ObjFraig(pObjOldRepr);
+    // if the fraiged nodes are the same, return
+    if ( Aig_Regular(pObjFraig) == Aig_Regular(pObjOldReprFraig) )
+        return pObjFraig;
+    assert( Aig_Regular(pObjFraig) != Aig_ManConst1(p->pManFraig) );
+//    printf( "Node = %d. Repr = %d.\n", pObjOld->Id, pObjOldRepr->Id );
+
+    // if they are proved different, the c-ex will be in p->pPatWords
+    RetValue = Fra_NodesAreEquiv( p, Aig_Regular(pObjOldReprFraig), Aig_Regular(pObjFraig) );
+    if ( RetValue == 1 )  // proved equivalent
+    {
+//        pObjOld->fMarkA = 1;
+        if ( p->pPars->fChoicing && !Fra_CheckTfi( p, Aig_Regular(pObjFraig), Aig_Regular(pObjOldReprFraig) ) )
+        {
+//            Fra_ObjSetReprFra( Aig_Regular(pObjFraig), Aig_Regular(pObjOldReprFraig) );
+            Aig_Obj_t * pObjNew = Aig_Regular(pObjFraig);
+            Aig_Obj_t * pObjOld = Aig_Regular(pObjOldReprFraig);
+            Aig_Obj_t * pTemp;
+            assert( pObjNew != pObjOld );
+            for ( pTemp = Fra_ObjReprFra(pObjOld); pTemp; pTemp = Fra_ObjReprFra(pTemp) )
+                if ( pTemp == pObjNew )
+                    break;
+            if ( pTemp == NULL )
+            {
+                Fra_ObjSetReprFra( pObjNew, Fra_ObjReprFra(pObjOld) );
+                Fra_ObjSetReprFra( pObjOld, pObjNew );
+                assert( pObjOld != Fra_ObjReprFra(pObjOld) );
+                assert( pObjNew != Fra_ObjReprFra(pObjNew) );
+                p->nChoices++;
+
+                assert( pObjOld->Id < pObjNew->Id );
+            }
+            else
+                p->nChoicesFake++;
+        }
+        return Aig_NotCond( pObjOldReprFraig, pObjOld->fPhase ^ pObjOldRepr->fPhase );
+    }
+    if ( RetValue == -1 ) // failed
+    {
+        static int Counter = 0;
+        char FileName[20];
+        Aig_Man_t * pTemp;
+        Aig_Obj_t * pObj;
+        int i;
+
+        Aig_Obj_t * ppNodes[2] = { Aig_Regular(pObjOldReprFraig), Aig_Regular(pObjFraig) };
+//        Vec_Ptr_t * vNodes;
+
+        if ( !p->pPars->fSpeculate )
+            return pObjFraig;
+        // substitute the node
+//        pObjOld->fMarkB = 1;
+        p->nSpeculs++;
+
+        pTemp = Aig_ManExtractMiter( p->pManFraig, ppNodes, 2 );
+        sprintf( FileName, "aig\\%03d.blif", ++Counter );
+        Aig_ManDumpBlif( pTemp, FileName );
+        printf( "Speculation cone with %d nodes was written into file \"%s\".\n", Aig_ManNodeNum(pTemp), FileName );
+        Aig_ManStop( pTemp );
+
+        Aig_ManForEachObj( p->pManFraig, pObj, i )
+            pObj->pData = p;
+
+//        vNodes = Aig_ManDfsNodes( p->pManFraig, ppNodes, 2 );
+//        printf( "Cone=%d ", Vec_PtrSize(vNodes) );
+//        Vec_PtrFree( vNodes );
+
+        return Aig_NotCond( pObjOldReprFraig, pObjOld->fPhase ^ pObjOldRepr->fPhase );
+    }
+//    printf( "Disproved %d and %d.\n", pObjOldRepr->Id, pObjOld->Id );
+    // simulate the counter-example and return the Fraig node
+//    printf( "Representaive before = %d.\n", Fra_ObjRepr(pObjOld)? Fra_ObjRepr(pObjOld)->Id : -1 );
+    Fra_Resimulate( p );
+//    printf( "Representaive after  = %d.\n", Fra_ObjRepr(pObjOld)? Fra_ObjRepr(pObjOld)->Id : -1 );
+    assert( Fra_ObjRepr(pObjOld) != pObjOldRepr );
+    return pObjFraig;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs fraiging for the internal nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Fra_Sweep( Fra_Man_t * p )
+{
+    ProgressBar * pProgress;
+    Aig_Obj_t * pObj, * pObjNew;
+    int i, k = 0;
+p->nClassesZero = Vec_PtrSize(p->vClasses1);
+p->nClassesBeg  = Vec_PtrSize(p->vClasses) + (int)(Vec_PtrSize(p->vClasses1) > 0);
+    // duplicate internal nodes
+    pProgress = Extra_ProgressBarStart( stdout, Aig_ManObjIdMax(p->pManAig) );
+    Aig_ManForEachNode( p->pManAig, pObj, i )
+    {
+        Extra_ProgressBarUpdate( pProgress, i, NULL );
+        // default to simple strashing if simulation detected a counter-example for a PO
+        if ( p->pManFraig->pData )
+            pObjNew = Aig_And( p->pManFraig, Fra_ObjChild0Fra(pObj), Fra_ObjChild1Fra(pObj) );
+        else
+            pObjNew = Fra_And( p, pObj ); // pObjNew can be complemented
+        Fra_ObjSetFraig( pObj, pObjNew );
+        assert( Fra_ObjFraig(pObj) != NULL );
+    }
+    Extra_ProgressBarStop( pProgress );
+p->nClassesEnd = Vec_PtrSize(p->vClasses) + (int)(Vec_PtrSize(p->vClasses1) > 0);
+    // try to prove the outputs of the miter
+    p->nNodesMiter = Aig_ManNodeNum(p->pManFraig);
+//    Fra_MiterStatus( p->pManFraig );
+//    if ( p->pPars->fProve && p->pManFraig->pData == NULL )
+//        Fra_MiterProve( p );
+    // add the POs
+    Aig_ManForEachPo( p->pManAig, pObj, i )
+        Aig_ObjCreatePo( p->pManFraig, Fra_ObjChild0Fra(pObj) );
+    // postprocess
+    Aig_ManCleanMarkB( p->pManFraig );
+    if ( p->pPars->fChoicing )
+    {
+        // transfer the representative info
+        p->pManFraig->pReprs = p->pMemReprFra;
+        p->pMemReprFra = NULL;
+//        printf( "The number of choices = %d. Fake choices = %d.\n", p->nChoices, p->nChoicesFake );
+    }
+    else
+    {
+        // remove dangling nodes 
+        Aig_ManCleanup( p->pManFraig );
+    }
+}
+
+/**Function*************************************************************
+
   Synopsis    [Performs fraiging of the AIG.]
 
   Description []
@@ -57,6 +228,30 @@ p->timeTotal = clock() - clk;
     return pManAigNew;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Performs choicing of the AIG.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Fra_Choice( Aig_Man_t * pManAig )
+{
+    Fra_Par_t Pars, * pPars = &Pars; 
+    Fra_ParamsDefault( pPars );
+    pPars->nBTLimitNode = 1000;
+    pPars->fVerbose     = 0;
+    pPars->fProve       = 0;
+    pPars->fDoSparse    = 1;
+    pPars->fSpeculate   = 0;
+    pPars->fChoicing    = 1;
+    return Fra_Perform( pManAig, pPars );
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/fra/fraDfs.c b/src/aig/fra/fraDfs.c
new file mode 100644
index 00000000..cd0985e0
--- /dev/null
+++ b/src/aig/fra/fraDfs.c
@@ -0,0 +1,87 @@
+/**CFile****************************************************************
+
+  FileName    [fraDfs.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Fraig FRAIG package.]
+
+  Synopsis    []
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 30, 2007.]
+
+  Revision    [$Id: fraDfs.c,v 1.00 2007/06/30 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "fra.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if pOld is in the TFI of pNew.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Fra_CheckTfi_rec( Fra_Man_t * p, Aig_Obj_t * pNode, Aig_Obj_t * pOld )
+{
+    // check the trivial cases
+    if ( pNode == NULL )
+        return 0;
+//    if ( pNode->Id < pOld->Id ) // cannot use because of choicesof pNode
+//        return 0;
+    if ( pNode == pOld )
+        return 1;
+    // skip the visited node
+    if ( Aig_ObjIsTravIdCurrent(p->pManFraig, pNode) )
+        return 0;
+    Aig_ObjSetTravIdCurrent(p->pManFraig, pNode);
+    // check the children
+    if ( Fra_CheckTfi_rec( p, Aig_ObjFanin0(pNode), pOld ) )
+        return 1;
+    if ( Fra_CheckTfi_rec( p, Aig_ObjFanin1(pNode), pOld ) )
+        return 1;
+    // check equivalent nodes
+    return Fra_CheckTfi_rec( p, Fra_ObjReprFra(pNode), pOld );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if pOld is in the TFI of pNew.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Fra_CheckTfi( Fra_Man_t * p, Aig_Obj_t * pNew, Aig_Obj_t * pOld )
+{
+    assert( !Aig_IsComplement(pNew) );
+    assert( !Aig_IsComplement(pOld) );
+    Aig_ManIncrementTravId( p->pManFraig );
+    return Fra_CheckTfi_rec( p, pNew, pOld );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/fra/fraMan.c b/src/aig/fra/fraMan.c
index 78246a8c..0e583d6c 100644
--- a/src/aig/fra/fraMan.c
+++ b/src/aig/fra/fraMan.c
@@ -97,6 +97,8 @@ Fra_Man_t * Fra_ManStart( Aig_Man_t * pManAig, Fra_Par_t * pPars )
     memset( p->pMemFraig, 0, p->nSizeAlloc * sizeof(Aig_Obj_t *) );
     p->pMemRepr  = ALLOC( Aig_Obj_t *, p->nSizeAlloc );
     memset( p->pMemRepr, 0, p->nSizeAlloc * sizeof(Aig_Obj_t *) );
+    p->pMemReprFra  = ALLOC( Aig_Obj_t *, p->nSizeAlloc );
+    memset( p->pMemReprFra, 0, p->nSizeAlloc * sizeof(Aig_Obj_t *) );
     p->pMemFanins  = ALLOC( Vec_Ptr_t *, p->nSizeAlloc );
     memset( p->pMemFanins, 0, p->nSizeAlloc * sizeof(Vec_Ptr_t *) );
     p->pMemSatNums  = ALLOC( int, p->nSizeAlloc );
@@ -166,6 +168,7 @@ void Fra_ManStop( Fra_Man_t * p )
     FREE( p->pMemSatNums );
     FREE( p->pMemFanins );
     FREE( p->pMemRepr );
+    FREE( p->pMemReprFra );
     FREE( p->pMemFraig );
     FREE( p->pMemClasses );
     FREE( p->pPatScores );
diff --git a/src/aig/fra/fraSat.c b/src/aig/fra/fraSat.c
index 66b1ba5a..8ab10c40 100644
--- a/src/aig/fra/fraSat.c
+++ b/src/aig/fra/fraSat.c
@@ -54,8 +54,7 @@ int Fra_NodesAreEquiv( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew )
     // if the backtrack limit is small, simply skip this node
     // if the backtrack limit is > 10, take the quare root of the limit
     nBTLimit = p->pPars->nBTLimitNode;
-/*
-    if ( nBTLimit > 0 && (pOld->fFailTfo || pNew->fFailTfo) )
+    if ( !p->pPars->fSpeculate && (nBTLimit > 0 && (pOld->fMarkB || pNew->fMarkB)) )
     {
         p->nSatFails++;
         // fail immediately
@@ -64,7 +63,7 @@ int Fra_NodesAreEquiv( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew )
             return -1;
         nBTLimit = (int)pow(nBTLimit, 0.7);
     }
-*/
+
     p->nSatCalls++;
 
     // make sure the solver is allocated and has enough variables
@@ -112,9 +111,9 @@ p->timeSatSat += clock() - clk;
     {
 p->timeSatFail += clock() - clk;
         // mark the node as the failed node
-//        if ( pOld != p->pManFraig->pConst1 ) 
-//            pOld->fFailTfo = 1;
-//        pNew->fFailTfo = 1;
+        if ( pOld != p->pManFraig->pConst1 ) 
+            pOld->fMarkB = 1;
+        pNew->fMarkB = 1;
         p->nSatFailsReal++;
         return -1;
     }
@@ -155,8 +154,8 @@ p->timeSatSat += clock() - clk;
     {
 p->timeSatFail += clock() - clk;
         // mark the node as the failed node
-//        pOld->fFailTfo = 1;
-//        pNew->fFailTfo = 1;
+        pOld->fMarkB = 1;
+        pNew->fMarkB = 1;
         p->nSatFailsReal++;
         return -1;
     }
@@ -240,7 +239,7 @@ p->timeSatSat += clock() - clk;
     {
 p->timeSatFail += clock() - clk;
         // mark the node as the failed node
-//        pNew->fFailTfo = 1;
+        pNew->fMarkB = 1;
         p->nSatFailsReal++;
         return -1;
     }
diff --git a/src/aig/fra/module.make b/src/aig/fra/module.make
index 934fbdac..df690700 100644
--- a/src/aig/fra/module.make
+++ b/src/aig/fra/module.make
@@ -1,7 +1,7 @@
-SRC +=    src/aig/fra/fraAnd.c \
-    src/aig/fra/fraClass.c \
+SRC +=    src/aig/fra/fraClass.c \
     src/aig/fra/fraCnf.c \
     src/aig/fra/fraCore.c \
+    src/aig/fra/fraDfs.c \
     src/aig/fra/fraMan.c \
     src/aig/fra/fraSat.c \
     src/aig/fra/fraSim.c