Version abc70608

23 files changed, 1099 insertions, 210 deletions

diff --git a/src/aig/dar/dar.h b/src/aig/dar/dar.h
index 7c77bea5..9bb79262 100644
--- a/src/aig/dar/dar.h
+++ b/src/aig/dar/dar.h
@@ -65,7 +65,8 @@ typedef enum {
     DAR_AIG_BUF,                     // 4: buffer node
     DAR_AIG_AND,                     // 5: AND node
     DAR_AIG_EXOR,                    // 6: EXOR node
-    DAR_AIG_VOID                     // 7: unused object
+    DAR_AIG_LATCH,                   // 7: latch
+    DAR_AIG_VOID                     // 8: unused object
 } Dar_Type_t;
 
 // the parameters
@@ -179,11 +180,13 @@ static inline Dar_Obj_t *  Dar_ManObj( Dar_Man_t * p, int i )     { return p->vO
 
 static inline int          Dar_ManPiNum( Dar_Man_t * p )          { return p->nObjs[DAR_AIG_PI];                    }
 static inline int          Dar_ManPoNum( Dar_Man_t * p )          { return p->nObjs[DAR_AIG_PO];                    }
+static inline int          Dar_ManBufNum( Dar_Man_t * p )         { return p->nObjs[DAR_AIG_BUF];                   }
 static inline int          Dar_ManAndNum( Dar_Man_t * p )         { return p->nObjs[DAR_AIG_AND];                   }
 static inline int          Dar_ManExorNum( Dar_Man_t * p )        { return p->nObjs[DAR_AIG_EXOR];                  }
-static inline int          Dar_ManNodeNum( Dar_Man_t * p )        { return p->nObjs[DAR_AIG_AND]+p->nObjs[DAR_AIG_EXOR];}
+static inline int          Dar_ManLatchNum( Dar_Man_t * p )       { return p->nObjs[DAR_AIG_LATCH];                 }
+static inline int          Dar_ManNodeNum( Dar_Man_t * p )        { return p->nObjs[DAR_AIG_AND]+p->nObjs[DAR_AIG_EXOR];   }
 static inline int          Dar_ManGetCost( Dar_Man_t * p )        { return p->nObjs[DAR_AIG_AND]+3*p->nObjs[DAR_AIG_EXOR]; }
-static inline int          Dar_ManObjNum( Dar_Man_t * p )         { return p->nCreated - p->nDeleted;           }
+static inline int          Dar_ManObjNum( Dar_Man_t * p )         { return p->nCreated - p->nDeleted;               }
 
 static inline Dar_Type_t   Dar_ObjType( Dar_Obj_t * pObj )        { return (Dar_Type_t)pObj->Type;               }
 static inline int          Dar_ObjIsNone( Dar_Obj_t * pObj )      { return pObj->Type == DAR_AIG_NONE;   }
@@ -193,19 +196,20 @@ static inline int          Dar_ObjIsPo( Dar_Obj_t * pObj )        { return pObj-
 static inline int          Dar_ObjIsBuf( Dar_Obj_t * pObj )       { return pObj->Type == DAR_AIG_BUF;    }
 static inline int          Dar_ObjIsAnd( Dar_Obj_t * pObj )       { return pObj->Type == DAR_AIG_AND;    }
 static inline int          Dar_ObjIsExor( Dar_Obj_t * pObj )      { return pObj->Type == DAR_AIG_EXOR;   }
+static inline int          Dar_ObjIsLatch( Dar_Obj_t * pObj )     { return pObj->Type == DAR_AIG_LATCH;  }
 static inline int          Dar_ObjIsNode( Dar_Obj_t * pObj )      { return pObj->Type == DAR_AIG_AND || pObj->Type == DAR_AIG_EXOR;   }
-static inline int          Dar_ObjIsTerm( Dar_Obj_t * pObj )      { return pObj->Type == DAR_AIG_PI  || pObj->Type == DAR_AIG_PO || pObj->Type == DAR_AIG_CONST1; }
-static inline int          Dar_ObjIsHash( Dar_Obj_t * pObj )      { return pObj->Type == DAR_AIG_AND || pObj->Type == DAR_AIG_EXOR;   }
+static inline int          Dar_ObjIsTerm( Dar_Obj_t * pObj )      { return pObj->Type == DAR_AIG_PI  || pObj->Type == DAR_AIG_PO || pObj->Type == DAR_AIG_CONST1;  }
+static inline int          Dar_ObjIsHash( Dar_Obj_t * pObj )      { return pObj->Type == DAR_AIG_AND || pObj->Type == DAR_AIG_EXOR || pObj->Type == DAR_AIG_LATCH; }
 
 static inline int          Dar_ObjIsMarkA( Dar_Obj_t * pObj )     { return pObj->fMarkA;  }
 static inline void         Dar_ObjSetMarkA( Dar_Obj_t * pObj )    { pObj->fMarkA = 1;     }
 static inline void         Dar_ObjClearMarkA( Dar_Obj_t * pObj )  { pObj->fMarkA = 0;     }
  
-static inline void         Dar_ObjSetTravId( Dar_Obj_t * pObj, int TravId )                { pObj->pData = (void *)TravId;                       }
-static inline void         Dar_ObjSetTravIdCurrent( Dar_Man_t * p, Dar_Obj_t * pObj )      { pObj->pData = (void *)p->nTravIds;                  }
-static inline void         Dar_ObjSetTravIdPrevious( Dar_Man_t * p, Dar_Obj_t * pObj )     { pObj->pData = (void *)(p->nTravIds - 1);            }
-static inline int          Dar_ObjIsTravIdCurrent( Dar_Man_t * p, Dar_Obj_t * pObj )       { return (int )((int)pObj->pData == p->nTravIds);     }
-static inline int          Dar_ObjIsTravIdPrevious( Dar_Man_t * p, Dar_Obj_t * pObj )      { return (int )((int)pObj->pData == p->nTravIds - 1); }
+static inline void         Dar_ObjSetTravId( Dar_Obj_t * pObj, int TravId )                { pObj->TravId = TravId;                         }
+static inline void         Dar_ObjSetTravIdCurrent( Dar_Man_t * p, Dar_Obj_t * pObj )      { pObj->TravId = p->nTravIds;                    }
+static inline void         Dar_ObjSetTravIdPrevious( Dar_Man_t * p, Dar_Obj_t * pObj )     { pObj->TravId = p->nTravIds - 1;                }
+static inline int          Dar_ObjIsTravIdCurrent( Dar_Man_t * p, Dar_Obj_t * pObj )       { return (int)(pObj->TravId == p->nTravIds);     }
+static inline int          Dar_ObjIsTravIdPrevious( Dar_Man_t * p, Dar_Obj_t * pObj )      { return (int)(pObj->TravId == p->nTravIds - 1); }
 
 static inline int          Dar_ObjTravId( Dar_Obj_t * pObj )      { return (int)pObj->pData;                       }
 static inline int          Dar_ObjPhase( Dar_Obj_t * pObj )       { return pObj->fPhase;                           }
@@ -247,7 +251,7 @@ static inline Dar_Obj_t *  Dar_ObjCreateGhost( Dar_Man_t * p, Dar_Obj_t * p0, Da
     assert( Type == DAR_AIG_PI || Dar_Regular(p0) != Dar_Regular(p1) );
     pGhost = Dar_ManGhost(p);
     pGhost->Type = Type;
-    if ( Dar_Regular(p0)->Id < Dar_Regular(p1)->Id )
+    if ( p1 == NULL || Dar_Regular(p0)->Id < Dar_Regular(p1)->Id )
     {
         pGhost->pFanin0 = p0;
         pGhost->pFanin1 = p1;
@@ -274,7 +278,8 @@ static inline Dar_Obj_t * Dar_ManFetchMemory( Dar_Man_t * p )
 static inline void Dar_ManRecycleMemory( Dar_Man_t * p, Dar_Obj_t * pEntry )
 {
     extern void Dar_MmFixedEntryRecycle( Dar_MmFixed_t * p, char * pEntry );
-    pEntry->Type = DAR_AIG_NONE; // distinquishes dead node from live node
+    p->nDeleted++;
+    pEntry->Type = DAR_AIG_NONE; // distinquishes a dead node from a live node
     Dar_MmFixedEntryRecycle( p->pMemObjs, (char *)pEntry );
 }
 
@@ -291,7 +296,7 @@ static inline void Dar_ManRecycleMemory( Dar_Man_t * p, Dar_Obj_t * pEntry )
     Vec_PtrForEachEntry( p->vPos, pObj, i )
 // iterator over all objects, including those currently not used
 #define Dar_ManForEachObj( p, pObj, i )                                         \
-    Vec_PtrForEachEntry( p->vObjs, pObj, i )
+    Vec_PtrForEachEntry( p->vObjs, pObj, i ) if ( (pObj) == NULL ) {} else
 
 ////////////////////////////////////////////////////////////////////////
 ///                    FUNCTION DECLARATIONS                         ///
@@ -313,7 +318,6 @@ extern Vec_Int_t *     Dar_LibReadNodes();
 extern Vec_Int_t *     Dar_LibReadOuts();
 /*=== darDfs.c ==========================================================*/
 extern Vec_Ptr_t *     Dar_ManDfs( Dar_Man_t * p );
-extern Vec_Ptr_t *     Dar_ManDfsNode( Dar_Man_t * p, Dar_Obj_t * pNode );
 extern int             Dar_ManCountLevels( Dar_Man_t * p );
 extern void            Dar_ManCreateRefs( Dar_Man_t * p );
 extern int             Dar_DagSize( Dar_Obj_t * pObj );
@@ -342,11 +346,13 @@ extern void            Dar_ObjConnect( Dar_Man_t * p, Dar_Obj_t * pObj, Dar_Obj_
 extern void            Dar_ObjDisconnect( Dar_Man_t * p, Dar_Obj_t * pObj );
 extern void            Dar_ObjDelete( Dar_Man_t * p, Dar_Obj_t * pObj );
 extern void            Dar_ObjDelete_rec( Dar_Man_t * p, Dar_Obj_t * pObj, int fFreeTop );
-extern void            Dar_ObjReplace( Dar_Man_t * p, Dar_Obj_t * pObjOld, Dar_Obj_t * pObjNew );
+extern void            Dar_ObjPatchFanin0( Dar_Man_t * p, Dar_Obj_t * pObj, Dar_Obj_t * pFaninNew );
+extern void            Dar_ObjReplace( Dar_Man_t * p, Dar_Obj_t * pObjOld, Dar_Obj_t * pObjNew, int fNodesOnly );
 /*=== darOper.c =========================================================*/
 extern Dar_Obj_t *     Dar_IthVar( Dar_Man_t * p, int i );
 extern Dar_Obj_t *     Dar_Oper( Dar_Man_t * p, Dar_Obj_t * p0, Dar_Obj_t * p1, Dar_Type_t Type );
 extern Dar_Obj_t *     Dar_And( Dar_Man_t * p, Dar_Obj_t * p0, Dar_Obj_t * p1 );
+extern Dar_Obj_t *     Dar_Latch( Dar_Man_t * p, Dar_Obj_t * pObj, int fInitOne );
 extern Dar_Obj_t *     Dar_Or( Dar_Man_t * p, Dar_Obj_t * p0, Dar_Obj_t * p1 );
 extern Dar_Obj_t *     Dar_Exor( Dar_Man_t * p, Dar_Obj_t * p0, Dar_Obj_t * p1 );
 extern Dar_Obj_t *     Dar_Mux( Dar_Man_t * p, Dar_Obj_t * pC, Dar_Obj_t * p1, Dar_Obj_t * p0 );
@@ -355,6 +361,8 @@ extern Dar_Obj_t *     Dar_Miter( Dar_Man_t * p, Vec_Ptr_t * vPairs );
 extern Dar_Obj_t *     Dar_CreateAnd( Dar_Man_t * p, int nVars );
 extern Dar_Obj_t *     Dar_CreateOr( Dar_Man_t * p, int nVars );
 extern Dar_Obj_t *     Dar_CreateExor( Dar_Man_t * p, int nVars );
+/*=== darSeq.c ========================================================*/
+extern int             Dar_ManSeqStrash( Dar_Man_t * p, int nLatches, int * pInits );
 /*=== darTable.c ========================================================*/
 extern Dar_Obj_t *     Dar_TableLookup( Dar_Man_t * p, Dar_Obj_t * pGhost );
 extern void            Dar_TableInsert( Dar_Man_t * p, Dar_Obj_t * pObj );
diff --git a/src/aig/dar/darCheck.c b/src/aig/dar/darCheck.c
index 6cfba787..5c7a2390 100644
--- a/src/aig/dar/darCheck.c
+++ b/src/aig/dar/darCheck.c
@@ -89,15 +89,24 @@ int Dar_ManCheck( Dar_Man_t * p )
         }
     }
     // count the total number of nodes
-    if ( Dar_ManObjNum(p) != 1 + Dar_ManPiNum(p) + Dar_ManPoNum(p) + Dar_ManAndNum(p) + Dar_ManExorNum(p) )
+    if ( Dar_ManObjNum(p) != 1 + Dar_ManPiNum(p) + Dar_ManPoNum(p) + Dar_ManBufNum(p) + Dar_ManAndNum(p) + Dar_ManExorNum(p) + Dar_ManLatchNum(p) )
     {
         printf( "Dar_ManCheck: The number of created nodes is wrong.\n" );
+        printf( "C1 = %d. Pi = %d. Po = %d. Buf = %d. And = %d. Xor = %d. Lat = %d. Total = %d.\n",
+            1, Dar_ManPiNum(p), Dar_ManPoNum(p), Dar_ManBufNum(p), Dar_ManAndNum(p), Dar_ManExorNum(p), Dar_ManLatchNum(p), 
+            1 + Dar_ManPiNum(p) + Dar_ManPoNum(p) + Dar_ManBufNum(p) + Dar_ManAndNum(p) + Dar_ManExorNum(p) + Dar_ManLatchNum(p) );
+        printf( "Created = %d. Deleted = %d. Existing = %d.\n",
+            p->nCreated, p->nDeleted, p->nCreated - p->nDeleted );
         return 0;
     }
     // count the number of nodes in the table
-    if ( Dar_TableCountEntries(p) != Dar_ManAndNum(p) + Dar_ManExorNum(p) )
+    if ( Dar_TableCountEntries(p) != Dar_ManAndNum(p) + Dar_ManExorNum(p) + Dar_ManLatchNum(p) )
     {
         printf( "Dar_ManCheck: The number of nodes in the structural hashing table is wrong.\n" );
+        printf( "Entries = %d. And = %d. Xor = %d. Lat = %d. Total = %d.\n", 
+            Dar_TableCountEntries(p), Dar_ManAndNum(p), Dar_ManExorNum(p), Dar_ManLatchNum(p),
+            Dar_ManAndNum(p) + Dar_ManExorNum(p) + Dar_ManLatchNum(p) );
+
         return 0;
     }
 //    if ( !Dar_ManIsAcyclic(p) )
diff --git a/src/aig/dar/darCore.c b/src/aig/dar/darCore.c
index 9f0f58f6..d56cca45 100644
--- a/src/aig/dar/darCore.c
+++ b/src/aig/dar/darCore.c
@@ -76,7 +76,7 @@ int Dar_ManRewrite( Dar_Man_t * p )
         pObjNew = Dar_LibBuildBest( p );
         pObjNew = Dar_NotCond( pObjNew, pObjNew->fPhase ^ pObj->fPhase );
         // remove the old nodes
-        Dar_ObjReplace( p, pObj, pObjNew );
+        Dar_ObjReplace( p, pObj, pObjNew, 1 );
         // compare the gains
         nNodeAfter = Dar_ManNodeNum( p );
         assert( p->GainBest == nNodeBefore - nNodeAfter );
@@ -99,6 +99,8 @@ int Dar_ManRewrite( Dar_Man_t * p )
     return 1;
 }
 
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/dar/darDfs.c b/src/aig/dar/darDfs.c
index 1c2ab057..bdb23c9d 100644
--- a/src/aig/dar/darDfs.c
+++ b/src/aig/dar/darDfs.c
@@ -39,15 +39,18 @@
   SeeAlso     []
 
 ***********************************************************************/
-void Dar_ManDfs_rec( Dar_Obj_t * pObj, Vec_Ptr_t * vNodes )
+void Dar_ManDfs_rec( Dar_Man_t * p, Dar_Obj_t * pObj, Vec_Ptr_t * vNodes )
 {
     assert( !Dar_IsComplement(pObj) );
-    if ( !Dar_ObjIsNode(pObj) || Dar_ObjIsMarkA(pObj) )
+    if ( pObj == NULL )
         return;
-    Dar_ManDfs_rec( Dar_ObjFanin0(pObj), vNodes );
-    Dar_ManDfs_rec( Dar_ObjFanin1(pObj), vNodes );
-    assert( !Dar_ObjIsMarkA(pObj) ); // loop detection
-    Dar_ObjSetMarkA(pObj);
+    if ( Dar_ObjIsTravIdCurrent(p, pObj) )
+        return;
+    assert( Dar_ObjIsNode(pObj) || Dar_ObjIsBuf(pObj) );
+    Dar_ManDfs_rec( p, Dar_ObjFanin0(pObj), vNodes );
+    Dar_ManDfs_rec( p, Dar_ObjFanin1(pObj), vNodes );
+    assert( !Dar_ObjIsTravIdCurrent(p, pObj) ); // loop detection
+    Dar_ObjSetTravIdCurrent(p, pObj);
     Vec_PtrPush( vNodes, pObj );
 }
 
@@ -67,35 +70,21 @@ Vec_Ptr_t * Dar_ManDfs( Dar_Man_t * p )
     Vec_Ptr_t * vNodes;
     Dar_Obj_t * pObj;
     int i;
+    Dar_ManIncrementTravId( p );
+    // mark constant and PIs
+    Dar_ObjSetTravIdCurrent( p, Dar_ManConst1(p) );
+    Dar_ManForEachPi( p, pObj, i )
+        Dar_ObjSetTravIdCurrent( p, pObj );
+    // if there are latches, mark them
+    if ( Dar_ManLatchNum(p) > 0 )
+        Dar_ManForEachObj( p, pObj, i )
+            if ( Dar_ObjIsLatch(pObj) )
+                Dar_ObjSetTravIdCurrent( p, pObj );
+    // go through the nodes
     vNodes = Vec_PtrAlloc( Dar_ManNodeNum(p) );
     Dar_ManForEachObj( p, pObj, i )
-        Dar_ManDfs_rec( pObj, vNodes );
-    Dar_ManForEachObj( p, pObj, i )
-        Dar_ObjClearMarkA(pObj);
-    return vNodes;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Collects internal nodes in the DFS order.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Vec_Ptr_t * Dar_ManDfsNode( Dar_Man_t * p, Dar_Obj_t * pNode )
-{
-    Vec_Ptr_t * vNodes;
-    Dar_Obj_t * pObj;
-    int i;
-    assert( !Dar_IsComplement(pNode) );
-    vNodes = Vec_PtrAlloc( 16 );
-    Dar_ManDfs_rec( pNode, vNodes );
-    Vec_PtrForEachEntry( vNodes, pObj, i )
-        Dar_ObjClearMarkA(pObj);
+        if ( Dar_ObjIsNode(pObj) || Dar_ObjIsBuf(pObj) )
+            Dar_ManDfs_rec( p, pObj, vNodes );
     return vNodes;
 }
 
diff --git a/src/aig/dar/darMan.c b/src/aig/dar/darMan.c
index bbac1360..1b40bb39 100644
--- a/src/aig/dar/darMan.c
+++ b/src/aig/dar/darMan.c
@@ -55,6 +55,7 @@ Dar_Man_t * Dar_ManStart( int nNodesMax )
     // allocate arrays for nodes
     p->vPis = Vec_PtrAlloc( 100 );
     p->vPos = Vec_PtrAlloc( 100 );
+    p->vObjs = Vec_PtrAlloc( 1000 );
     // prepare the internal memory manager
     p->pMemObjs = Dar_MmFixedStart( sizeof(Dar_Obj_t), nNodesMax );
     p->pMemCuts = Dar_MmFlexStart();
@@ -66,7 +67,7 @@ Dar_Man_t * Dar_ManStart( int nNodesMax )
     p->pConst1 = Dar_ManFetchMemory( p );
     p->pConst1->Type = DAR_AIG_CONST1;
     p->pConst1->fPhase = 1;
-    p->nCreated = 1;
+    p->nObjs[DAR_AIG_CONST1]++;
     // start the table
     p->nTableSize = nNodesMax;
     p->pTable = ALLOC( Dar_Obj_t *, p->nTableSize );
@@ -100,10 +101,10 @@ void Dar_ManStop( Dar_Man_t * p )
 //    Dar_TableProfile( p );
     Dar_MmFixedStop( p->pMemObjs, 0 );
     Dar_MmFlexStop( p->pMemCuts, 0 );
-    if ( p->vPis )      Vec_PtrFree( p->vPis );
-    if ( p->vPos )      Vec_PtrFree( p->vPos );
-    if ( p->vObjs )     Vec_PtrFree( p->vObjs );
-    if ( p->vRequired ) Vec_IntFree( p->vRequired );
+    if ( p->vPis )        Vec_PtrFree( p->vPis );
+    if ( p->vPos )        Vec_PtrFree( p->vPos );
+    if ( p->vObjs )       Vec_PtrFree( p->vObjs );
+    if ( p->vRequired )   Vec_IntFree( p->vRequired );
     if ( p->vLeavesBest ) Vec_PtrFree( p->vLeavesBest );
     free( p->pTable );
     free( p );
@@ -151,12 +152,15 @@ int Dar_ManCleanup( Dar_Man_t * p )
 ***********************************************************************/
 void Dar_ManPrintStats( Dar_Man_t * p )
 {
-    printf( "PI/PO = %d/%d. ", Dar_ManPiNum(p), Dar_ManPoNum(p) );
-    printf( "A = %7d. ",       Dar_ManAndNum(p) );
-    printf( "X = %5d. ",       Dar_ManExorNum(p) );
-    printf( "Cre = %7d. ",     p->nCreated );
-    printf( "Del = %7d. ",     p->nDeleted );
-    printf( "Lev = %3d. ",     Dar_ManCountLevels(p) );
+    printf( "PI/PO/Lat = %5d/%5d/%5d   ", Dar_ManPiNum(p), Dar_ManPoNum(p), Dar_ManLatchNum(p) );
+    printf( "A = %6d. ",    Dar_ManAndNum(p) );
+    if ( Dar_ManExorNum(p) )
+        printf( "X = %5d. ",    Dar_ManExorNum(p) );
+    if ( Dar_ManBufNum(p) )
+        printf( "B = %3d. ",    Dar_ManBufNum(p) );
+    printf( "Cre = %6d. ",  p->nCreated );
+    printf( "Del = %6d. ",  p->nDeleted );
+//    printf( "Lev = %3d. ",  Dar_ManCountLevels(p) );
     printf( "\n" );
 }
 
diff --git a/src/aig/dar/darObj.c b/src/aig/dar/darObj.c
index faf9336e..2db13c71 100644
--- a/src/aig/dar/darObj.c
+++ b/src/aig/dar/darObj.c
@@ -89,7 +89,7 @@ Dar_Obj_t * Dar_ObjCreate( Dar_Man_t * p, Dar_Obj_t * pGhost )
 {
     Dar_Obj_t * pObj;
     assert( !Dar_IsComplement(pGhost) );
-    assert( Dar_ObjIsNode(pGhost) );
+    assert( Dar_ObjIsHash(pGhost) );
     assert( pGhost == &p->Ghost );
     // get memory for the new object
     pObj = Dar_ManFetchMemory( p );
@@ -116,7 +116,7 @@ Dar_Obj_t * Dar_ObjCreate( Dar_Man_t * p, Dar_Obj_t * pGhost )
 void Dar_ObjConnect( Dar_Man_t * p, Dar_Obj_t * pObj, Dar_Obj_t * pFan0, Dar_Obj_t * pFan1 )
 {
     assert( !Dar_IsComplement(pObj) );
-    assert( Dar_ObjIsNode(pObj) );
+    assert( !Dar_ObjIsPi(pObj) );
     // add the first fanin
     pObj->pFanin0 = pFan0;
     pObj->pFanin1 = pFan1;
@@ -137,7 +137,7 @@ void Dar_ObjConnect( Dar_Man_t * p, Dar_Obj_t * pObj, Dar_Obj_t * pFan0, Dar_Obj
         pObj->fPhase = Dar_ObjFaninPhase(pFan0);
     }
     // add the node to the structural hash table
-    if ( Dar_ObjIsNode(pObj) )
+    if ( Dar_ObjIsHash(pObj) )
         Dar_TableInsert( p, pObj );
 }
 
@@ -161,7 +161,7 @@ void Dar_ObjDisconnect( Dar_Man_t * p, Dar_Obj_t * pObj )
     if ( pObj->pFanin1 != NULL )
         Dar_ObjDeref(Dar_ObjFanin1(pObj));
     // remove the node from the structural hash table
-    if ( Dar_ObjIsNode(pObj) )
+    if ( Dar_ObjIsHash(pObj) )
         Dar_TableDelete( p, pObj );
     // add the first fanin
     pObj->pFanin0 = NULL;
@@ -184,7 +184,7 @@ void Dar_ObjDelete( Dar_Man_t * p, Dar_Obj_t * pObj )
     assert( !Dar_IsComplement(pObj) );
     assert( !Dar_ObjIsTerm(pObj) );
     assert( Dar_ObjRefs(pObj) == 0 );
-    p->nDeleted++;
+    p->nObjs[pObj->Type]--;
     Vec_PtrWriteEntry( p->vObjs, pObj->Id, NULL );
     Dar_ManRecycleMemory( p, pObj );
 }
@@ -206,11 +206,10 @@ void Dar_ObjDelete_rec( Dar_Man_t * p, Dar_Obj_t * pObj, int fFreeTop )
     assert( !Dar_IsComplement(pObj) );
     if ( Dar_ObjIsConst1(pObj) || Dar_ObjIsPi(pObj) )
         return;
-    assert( Dar_ObjIsNode(pObj) );
+    assert( !Dar_ObjIsPo(pObj) );
     pFanin0 = Dar_ObjFanin0(pObj);
     pFanin1 = Dar_ObjFanin1(pObj);
     Dar_ObjDisconnect( p, pObj );
-    p->nObjs[pObj->Type]--;
     if ( fFreeTop )
         Dar_ObjDelete( p, pObj );
     if ( pFanin0 && !Dar_ObjIsNone(pFanin0) && Dar_ObjRefs(pFanin0) == 0 )
@@ -221,6 +220,33 @@ void Dar_ObjDelete_rec( Dar_Man_t * p, Dar_Obj_t * pObj, int fFreeTop )
 
 /**Function*************************************************************
 
+  Synopsis    [Replaces the first fanin of the node by the new fanin.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Dar_ObjPatchFanin0( Dar_Man_t * p, Dar_Obj_t * pObj, Dar_Obj_t * pFaninNew )
+{
+    Dar_Obj_t * pFaninOld;
+    assert( !Dar_IsComplement(pObj) );
+    pFaninOld = Dar_ObjFanin0(pObj);
+    // decrement ref and remove fanout
+    Dar_ObjDeref( pFaninOld );
+    // update the fanin
+    pObj->pFanin0 = pFaninNew;
+    // increment ref and add fanout
+    Dar_ObjRef( Dar_Regular(pFaninNew) );
+    // get rid of old fanin
+    if ( !Dar_ObjIsPi(pFaninOld) && !Dar_ObjIsConst1(pFaninOld) && Dar_ObjRefs(pFaninOld) == 0 )
+        Dar_ObjDelete_rec( p, pFaninOld, 1 );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Replaces one object by another.]
 
   Description [Both objects are currently in the manager. The new object
@@ -232,27 +258,27 @@ void Dar_ObjDelete_rec( Dar_Man_t * p, Dar_Obj_t * pObj, int fFreeTop )
   SeeAlso     []
 
 ***********************************************************************/
-void Dar_ObjReplace( Dar_Man_t * p, Dar_Obj_t * pObjOld, Dar_Obj_t * pObjNew )
+void Dar_ObjReplace( Dar_Man_t * p, Dar_Obj_t * pObjOld, Dar_Obj_t * pObjNew, int fNodesOnly )
 {
     Dar_Obj_t * pObjNewR = Dar_Regular(pObjNew);
     // the object to be replaced cannot be complemented
     assert( !Dar_IsComplement(pObjOld) );
     // the object to be replaced cannot be a terminal
     assert( !Dar_ObjIsPi(pObjOld) && !Dar_ObjIsPo(pObjOld) );
-    // the object to be used cannot be a buffer
+    // the object to be used cannot be a buffer or a PO
     assert( !Dar_ObjIsBuf(pObjNewR) && !Dar_ObjIsPo(pObjNewR) );
     // the object cannot be the same
     assert( pObjOld != pObjNewR );
     // make sure object is not pointing to itself
-    assert( pObjOld != Dar_ObjFanin0(pObjNewR) );
+//    assert( pObjOld != Dar_ObjFanin0(pObjNewR) );
     assert( pObjOld != Dar_ObjFanin1(pObjNewR) );
-    // delete the old node
+    // recursively delete the old node - but leave the object there
     Dar_ObjDelete_rec( p, pObjOld, 0 );
     // if the new object is complemented or already used, create a buffer
-    if ( Dar_IsComplement(pObjNew) || Dar_ObjRefs(pObjNew) > 0 || !Dar_ObjIsNode(pObjNew) )
+    p->nObjs[pObjOld->Type]--;
+    if ( Dar_IsComplement(pObjNew) || Dar_ObjRefs(pObjNew) > 0 || (fNodesOnly && !Dar_ObjIsNode(pObjNew)) )
     {
         pObjOld->Type = DAR_AIG_BUF;
-        p->nObjs[pObjOld->Type]++;
         Dar_ObjConnect( p, pObjOld, pObjNew, NULL );
     }
     else
@@ -261,9 +287,10 @@ void Dar_ObjReplace( Dar_Man_t * p, Dar_Obj_t * pObjOld, Dar_Obj_t * pObjNew )
         Dar_Obj_t * pFanin1 = pObjNew->pFanin1;
         pObjOld->Type = pObjNew->Type;
         Dar_ObjDisconnect( p, pObjNew );
-        Dar_ObjDelete( p, pObjNew );
         Dar_ObjConnect( p, pObjOld, pFanin0, pFanin1 );
+        Dar_ObjDelete( p, pObjNew );
     }
+    p->nObjs[pObjOld->Type]++;
 }
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/dar/darOper.c b/src/aig/dar/darOper.c
index 8921fe33..cfb89e31 100644
--- a/src/aig/dar/darOper.c
+++ b/src/aig/dar/darOper.c
@@ -89,6 +89,43 @@ Dar_Obj_t * Dar_Oper( Dar_Man_t * p, Dar_Obj_t * p0, Dar_Obj_t * p1, Dar_Type_t
 
 /**Function*************************************************************
 
+  Synopsis    [Creates the canonical form of the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Dar_Obj_t * Dar_CanonPair_rec( Dar_Man_t * p, Dar_Obj_t * pGhost )
+{
+    Dar_Obj_t * pResult, * pLat0, * pLat1;
+    int fCompl0, fCompl1;
+    Dar_Type_t Type;
+    assert( Dar_ObjIsNode(pGhost) );
+    // consider the case when the pair is canonical
+    if ( !Dar_ObjIsLatch(Dar_ObjFanin0(pGhost)) || !Dar_ObjIsLatch(Dar_ObjFanin1(pGhost)) )
+    {
+        if ( pResult = Dar_TableLookup( p, pGhost ) )
+            return pResult;
+        return Dar_ObjCreate( p, pGhost );
+    }
+    /// remember the latches
+    pLat0 = Dar_ObjFanin0(pGhost);
+    pLat1 = Dar_ObjFanin1(pGhost);
+    // remember type and compls
+    Type = Dar_ObjType(pGhost);
+    fCompl0 = Dar_ObjFaninC0(pGhost);
+    fCompl1 = Dar_ObjFaninC1(pGhost);
+    // call recursively
+    pResult = Dar_Oper( p, Dar_NotCond(Dar_ObjChild0(pLat0), fCompl0), Dar_NotCond(Dar_ObjChild0(pLat1), fCompl1), Type );
+    // build latch on top of this
+    return Dar_Latch( p, pResult, (Type == DAR_AIG_AND)? fCompl0 & fCompl1 : fCompl0 ^ fCompl1 );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Performs canonicization step.]
 
   Description [The argument nodes can be complemented.]
@@ -114,11 +151,30 @@ Dar_Obj_t * Dar_And( Dar_Man_t * p, Dar_Obj_t * p0, Dar_Obj_t * p1 )
     // check if it can be an EXOR gate
 //    if ( Dar_ObjIsExorType( p0, p1, &pFan0, &pFan1 ) )
 //        return Dar_Exor( p, pFan0, pFan1 );
-    // check the table
     pGhost = Dar_ObjCreateGhost( p, p0, p1, DAR_AIG_AND );
-    if ( pResult = Dar_TableLookup( p, pGhost ) )
-        return pResult;
-    return Dar_ObjCreate( p, pGhost );
+    pResult = Dar_CanonPair_rec( p, pGhost );
+    return pResult;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates the canonical form of the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Dar_Obj_t * Dar_Latch( Dar_Man_t * p, Dar_Obj_t * pObj, int fInitOne )
+{
+    Dar_Obj_t * pGhost, * pResult;
+    pGhost = Dar_ObjCreateGhost( p, Dar_NotCond(pObj, fInitOne), NULL, DAR_AIG_LATCH );
+    pResult = Dar_TableLookup( p, pGhost );
+    if ( pResult == NULL )
+        pResult = Dar_ObjCreate( p, pGhost );
+    return Dar_NotCond( pResult, fInitOne );
 }
 
 /**Function*************************************************************
diff --git a/src/aig/dar/darSeq.c b/src/aig/dar/darSeq.c
new file mode 100644
index 00000000..bf3807f4
--- /dev/null
+++ b/src/aig/dar/darSeq.c
@@ -0,0 +1,471 @@
+/**CFile****************************************************************
+
+  FileName    [darSeq.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [DAG-aware AIG rewriting.]
+
+  Synopsis    []
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - April 28, 2007.]
+
+  Revision    [$Id: darSeq.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "dar.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Converts combinational AIG manager into a sequential one.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Dar_ManSeqStrashConvert( Dar_Man_t * p, int nLatches, int * pInits )
+{
+    Dar_Obj_t * pObjLi, * pObjLo, * pLatch;
+    int i;
+    // collect the POs to be converted into latches
+    for ( i = 0; i < nLatches; i++ )
+    {
+        // get the corresponding PI/PO pair
+        pObjLi = Dar_ManPo( p, Dar_ManPoNum(p) - nLatches + i );
+        pObjLo = Dar_ManPi( p, Dar_ManPiNum(p) - nLatches + i );
+        // create latch
+        pLatch = Dar_Latch( p, Dar_ObjChild0(pObjLi), pInits? pInits[i] : 0 );
+        // recycle the old PO object
+        Dar_ObjDisconnect( p, pObjLi );
+        Vec_PtrWriteEntry( p->vObjs, pObjLi->Id, NULL );
+        Dar_ManRecycleMemory( p, pObjLi );
+        // convert the corresponding PI to be a buffer and connect it to the latch
+        pObjLo->Type = DAR_AIG_BUF;
+        Dar_ObjConnect( p, pObjLo, pLatch, NULL );
+    }
+    // shrink the arrays
+    Vec_PtrShrink( p->vPis, Dar_ManPiNum(p) - nLatches );
+    Vec_PtrShrink( p->vPos, Dar_ManPoNum(p) - nLatches );
+    // update the counters of different objects
+    p->nObjs[DAR_AIG_PI]  -= nLatches;
+    p->nObjs[DAR_AIG_PO]  -= nLatches;
+    p->nObjs[DAR_AIG_BUF] += nLatches;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collects internal nodes in the DFS order.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Dar_ManDfsSeq_rec( Dar_Man_t * p, Dar_Obj_t * pObj, Vec_Ptr_t * vNodes )
+{
+    assert( !Dar_IsComplement(pObj) );
+    if ( pObj == NULL )
+        return;
+    if ( Dar_ObjIsTravIdCurrent( p, pObj ) )
+        return;
+    Dar_ObjSetTravIdCurrent( p, pObj );
+    if ( Dar_ObjIsPi(pObj) )
+        return;
+    Dar_ManDfsSeq_rec( p, Dar_ObjFanin0(pObj), vNodes );
+    Dar_ManDfsSeq_rec( p, Dar_ObjFanin1(pObj), vNodes );
+    Vec_PtrPush( vNodes, pObj );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collects internal nodes in the DFS order.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Dar_ManDfsSeq( Dar_Man_t * p )
+{
+    Vec_Ptr_t * vNodes;
+    Dar_Obj_t * pObj;
+    int i;
+    Dar_ManIncrementTravId( p );
+    vNodes = Vec_PtrAlloc( Dar_ManNodeNum(p) );
+    Dar_ManForEachPo( p, pObj, i )
+        Dar_ManDfsSeq_rec( p, Dar_ObjFanin0(pObj), vNodes );
+    return vNodes;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collects internal nodes in the DFS order.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Dar_ManDfsUnreach_rec( Dar_Man_t * p, Dar_Obj_t * pObj, Vec_Ptr_t * vNodes )
+{
+    assert( !Dar_IsComplement(pObj) );
+    if ( pObj == NULL )
+        return;
+    if ( Dar_ObjIsTravIdPrevious(p, pObj) || Dar_ObjIsTravIdCurrent(p, pObj) )
+        return;
+    Dar_ObjSetTravIdPrevious( p, pObj ); // assume unknown
+    Dar_ManDfsUnreach_rec( p, Dar_ObjFanin0(pObj), vNodes );
+    Dar_ManDfsUnreach_rec( p, Dar_ObjFanin1(pObj), vNodes );
+    if ( Dar_ObjIsTravIdPrevious(p, Dar_ObjFanin0(pObj)) && 
+        (Dar_ObjFanin1(pObj) == NULL || Dar_ObjIsTravIdPrevious(p, Dar_ObjFanin1(pObj))) )
+        Vec_PtrPush( vNodes, pObj );
+    else
+        Dar_ObjSetTravIdCurrent( p, pObj );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collects internal nodes unreachable from PIs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Dar_ManDfsUnreach( Dar_Man_t * p )
+{
+    Vec_Ptr_t * vNodes;
+    Dar_Obj_t * pObj, * pFanin;
+    int i, k;//, RetValue;
+    // collect unreachable nodes
+    Dar_ManIncrementTravId( p ); 
+    Dar_ManIncrementTravId( p ); 
+    // mark the constant and PIs
+    Dar_ObjSetTravIdPrevious( p, Dar_ManConst1(p) );
+    Dar_ManForEachPi( p, pObj, i )
+        Dar_ObjSetTravIdCurrent( p, pObj );
+    // curr marks visited nodes reachable from PIs
+    // prev marks visited nodes unreachable or unknown
+
+    // collect the unreachable nodes
+    vNodes = Vec_PtrAlloc( 32 );
+    Dar_ManForEachPo( p, pObj, i )
+        Dar_ManDfsUnreach_rec( p, Dar_ObjFanin0(pObj), vNodes );
+
+    // refine resulting nodes
+    do 
+    {
+        k = 0;
+        Vec_PtrForEachEntry( vNodes, pObj, i )
+        {
+            assert( Dar_ObjIsTravIdPrevious(p, pObj) );
+            if ( Dar_ObjIsLatch(pObj) || Dar_ObjIsBuf(pObj) )
+            {
+                pFanin = Dar_ObjFanin0(pObj);
+                assert( Dar_ObjIsTravIdPrevious(p, pFanin) || Dar_ObjIsTravIdCurrent(p, pFanin) );
+                if ( Dar_ObjIsTravIdCurrent(p, pFanin) )
+                {
+                    Dar_ObjSetTravIdCurrent( p, pObj );
+                    continue;
+                }
+            }
+            else // AND gate
+            {
+                assert( Dar_ObjIsNode(pObj) );
+                pFanin = Dar_ObjFanin0(pObj);
+                assert( Dar_ObjIsTravIdPrevious(p, pFanin) || Dar_ObjIsTravIdCurrent(p, pFanin) );
+                if ( Dar_ObjIsTravIdCurrent(p, pFanin) )
+                {
+                    Dar_ObjSetTravIdCurrent( p, pObj );
+                    continue;
+                }
+                pFanin = Dar_ObjFanin1(pObj);
+                assert( Dar_ObjIsTravIdPrevious(p, pFanin) || Dar_ObjIsTravIdCurrent(p, pFanin) );
+                if ( Dar_ObjIsTravIdCurrent(p, pFanin) )
+                {
+                    Dar_ObjSetTravIdCurrent( p, pObj );
+                    continue;
+                }
+            }
+            // write it back
+            Vec_PtrWriteEntry( vNodes, k++, pObj );
+        }
+        Vec_PtrShrink( vNodes, k );
+    } 
+    while ( k < i );
+
+    if ( Vec_PtrSize(vNodes) > 0 )
+        printf( "Found %d unreachable.\n", Vec_PtrSize(vNodes) ); 
+    return vNodes;
+
+/*
+    // the resulting array contains all unreachable nodes except const 1
+    if ( Vec_PtrSize(vNodes) == 0 )
+    {
+        Vec_PtrFree( vNodes );
+        return 0;
+    }
+    RetValue = Vec_PtrSize(vNodes);
+
+    // mark these nodes
+    Dar_ManIncrementTravId( p ); 
+    Vec_PtrForEachEntry( vNodes, pObj, i )
+        Dar_ObjSetTravIdCurrent( p, pObj );
+    Vec_PtrFree( vNodes );
+    return RetValue;
+*/
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Removes nodes that do not fanout into POs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Dar_ManRemoveUnmarked( Dar_Man_t * p )
+{
+    Vec_Ptr_t * vNodes;
+    Dar_Obj_t * pObj;
+    int i, RetValue;
+    // collect unmarked nodes
+    vNodes = Vec_PtrAlloc( 100 );
+    Dar_ManForEachObj( p, pObj, i )
+    {
+        if ( Dar_ObjIsTerm(pObj) )
+            continue;
+        if ( Dar_ObjIsTravIdCurrent(p, pObj) )
+            continue;
+//Dar_ObjPrintVerbose( pObj, 0 );
+        Dar_ObjDisconnect( p, pObj );
+        Vec_PtrPush( vNodes, pObj );
+    }
+    if ( Vec_PtrSize(vNodes) == 0 )
+    {
+        Vec_PtrFree( vNodes );
+        return 0;
+    }
+    // remove the dangling objects
+    RetValue = Vec_PtrSize(vNodes);
+    Vec_PtrForEachEntry( vNodes, pObj, i )
+        Dar_ObjDelete( p, pObj );
+    printf( "Removes %d dangling.\n", Vec_PtrSize(vNodes) ); 
+    Vec_PtrFree( vNodes );
+    return RetValue;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline Dar_Obj_t * Dar_ObjReal_rec( Dar_Obj_t * pObj )
+{
+    Dar_Obj_t * pObjNew, * pObjR = Dar_Regular(pObj);
+    if ( !Dar_ObjIsBuf(pObjR) )
+        return pObj;
+    pObjNew = Dar_ObjReal_rec( Dar_ObjChild0(pObjR) );
+    return Dar_NotCond( pObjNew, Dar_IsComplement(pObj) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Rehashes the nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Dar_ManSeqRehashOne( Dar_Man_t * p, Vec_Ptr_t * vNodes, Vec_Ptr_t * vUnreach )
+{
+    Dar_Obj_t * pObj, * pObjNew, * pFanin0, * pFanin1;
+    int i, RetValue = 0;
+    // mark the unreachable nodes
+    Dar_ManIncrementTravId( p );
+    Vec_PtrForEachEntry( vUnreach, pObj, i )
+        Dar_ObjSetTravIdCurrent(p, pObj);
+    // go through the nodes while skipping unreachable
+    Vec_PtrForEachEntry( vNodes, pObj, i )
+    {
+        // skip nodes unreachable from the PIs
+        if ( Dar_ObjIsTravIdCurrent(p, pObj) )
+            continue;
+        // process the node
+        if ( Dar_ObjIsPo(pObj) )
+        {
+            if ( !Dar_ObjIsBuf(Dar_ObjFanin0(pObj)) )
+                continue;
+            pFanin0 = Dar_ObjReal_rec( Dar_ObjChild0(pObj) );
+            Dar_ObjPatchFanin0( p, pObj, pFanin0 );
+            continue;
+        }
+        if ( Dar_ObjIsLatch(pObj) )
+        {
+            if ( !Dar_ObjIsBuf(Dar_ObjFanin0(pObj)) )
+                continue;
+            pObjNew = Dar_ObjReal_rec( Dar_ObjChild0(pObj) );
+            pObjNew = Dar_Latch( p, pObjNew, 0 );
+            Dar_ObjReplace( p, pObj, pObjNew, 1 );
+            RetValue = 1;
+            continue;
+        }
+        if ( Dar_ObjIsNode(pObj) )
+        {
+            if ( !Dar_ObjIsBuf(Dar_ObjFanin0(pObj)) && !Dar_ObjIsBuf(Dar_ObjFanin1(pObj)) )
+                continue;
+            pFanin0 = Dar_ObjReal_rec( Dar_ObjChild0(pObj) );
+            pFanin1 = Dar_ObjReal_rec( Dar_ObjChild1(pObj) );
+            pObjNew = Dar_And( p, pFanin0, pFanin1 );
+            Dar_ObjReplace( p, pObj, pObjNew, 1 );
+            RetValue = 1;
+            continue;
+        }
+    }
+    return RetValue;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [If AIG contains buffers, this procedure removes them.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Dar_ManRemoveBuffers( Dar_Man_t * p )
+{
+    Dar_Obj_t * pObj, * pObjNew, * pFanin0, * pFanin1;
+    int i;
+    if ( Dar_ManBufNum(p) == 0 )
+        return;
+    Dar_ManForEachObj( p, pObj, i )
+    {
+        if ( Dar_ObjIsPo(pObj) )
+        {
+            if ( !Dar_ObjIsBuf(Dar_ObjFanin0(pObj)) )
+                continue;
+            pFanin0 = Dar_ObjReal_rec( Dar_ObjChild0(pObj) );
+            Dar_ObjPatchFanin0( p, pObj, pFanin0 );
+        }
+        else if ( Dar_ObjIsLatch(pObj) )
+        {
+            if ( !Dar_ObjIsBuf(Dar_ObjFanin0(pObj)) )
+                continue;
+            pFanin0 = Dar_ObjReal_rec( Dar_ObjChild0(pObj) );
+            pObjNew = Dar_Latch( p, pFanin0, 0 );
+            Dar_ObjReplace( p, pObj, pObjNew, 0 );
+        }
+        else if ( Dar_ObjIsAnd(pObj) )
+        {
+            if ( !Dar_ObjIsBuf(Dar_ObjFanin0(pObj)) && !Dar_ObjIsBuf(Dar_ObjFanin1(pObj)) )
+                continue;
+            pFanin0 = Dar_ObjReal_rec( Dar_ObjChild0(pObj) );
+            pFanin1 = Dar_ObjReal_rec( Dar_ObjChild1(pObj) );
+            pObjNew = Dar_And( p, pFanin0, pFanin1 );
+            Dar_ObjReplace( p, pObj, pObjNew, 0 );
+        }
+    }
+    assert( Dar_ManBufNum(p) == 0 );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Dar_ManSeqStrash( Dar_Man_t * p, int nLatches, int * pInits )
+{
+    Vec_Ptr_t * vNodes, * vUnreach;
+    Dar_Obj_t * pObj;
+    int i;
+    int RetValue = 1;
+    // create latches out of the additional PI/PO pairs
+    Dar_ManSeqStrashConvert( p, nLatches, pInits );
+    // iteratively rehash the network
+    while ( RetValue )
+    {
+        Dar_ManPrintStats( p );
+
+        Dar_ManForEachObj( p, pObj, i )
+            assert( pObj->Type > 0 );
+
+        // mark nodes unreachable from the PIs
+        vUnreach = Dar_ManDfsUnreach( p );
+        // collect nodes reachable from the POs
+        vNodes = Dar_ManDfsSeq( p );
+        // remove nodes unreachable from the POs
+        Dar_ManRemoveUnmarked( p );
+        // continue rehashing as long as there are changes
+        RetValue = Dar_ManSeqRehashOne( p, vNodes, vUnreach );
+        Vec_PtrFree( vNodes );
+        Vec_PtrFree( vUnreach );
+    }
+    // perform the final cleanup
+    Dar_ManIncrementTravId( p );
+    vNodes = Dar_ManDfsSeq( p );
+    Dar_ManRemoveUnmarked( p );
+    Vec_PtrFree( vNodes );
+    // remove buffers if they are left
+//    Dar_ManRemoveBuffers( p );
+    // clean up
+    if ( !Dar_ManCheck( p ) )
+    {
+        printf( "Dar_ManSeqStrash: The network check has failed.\n" );
+        return 0;
+    }
+    return 1;
+
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/dar/darTable.c b/src/aig/dar/darTable.c
index 8b4bfaf3..af9956ec 100644
--- a/src/aig/dar/darTable.c
+++ b/src/aig/dar/darTable.c
@@ -39,8 +39,15 @@ static unsigned long Dar_Hash( Dar_Obj_t * pObj, int TableSize )
 static Dar_Obj_t ** Dar_TableFind( Dar_Man_t * p, Dar_Obj_t * pObj )
 {
     Dar_Obj_t ** ppEntry;
-    assert( Dar_ObjChild0(pObj) && Dar_ObjChild1(pObj) );
-    assert( Dar_ObjFanin0(pObj)->Id < Dar_ObjFanin1(pObj)->Id );
+    if ( Dar_ObjIsLatch(pObj) )
+    {
+        assert( Dar_ObjChild0(pObj) && Dar_ObjChild1(pObj) == NULL );
+    }
+    else
+    {
+        assert( Dar_ObjChild0(pObj) && Dar_ObjChild1(pObj) );
+        assert( Dar_ObjFanin0(pObj)->Id < Dar_ObjFanin1(pObj)->Id );
+    }
     for ( ppEntry = p->pTable + Dar_Hash(pObj, p->nTableSize); *ppEntry; ppEntry = &(*ppEntry)->pNext )
         if ( *ppEntry == pObj )
             return ppEntry;
@@ -70,10 +77,20 @@ Dar_Obj_t * Dar_TableLookup( Dar_Man_t * p, Dar_Obj_t * pGhost )
 {
     Dar_Obj_t * pEntry;
     assert( !Dar_IsComplement(pGhost) );
-    assert( Dar_ObjChild0(pGhost) && Dar_ObjChild1(pGhost) );
-    assert( Dar_ObjFanin0(pGhost)->Id < Dar_ObjFanin1(pGhost)->Id );
-    if ( !Dar_ObjRefs(Dar_ObjFanin0(pGhost)) || !Dar_ObjRefs(Dar_ObjFanin1(pGhost)) )
-        return NULL;
+    if ( pGhost->Type == DAR_AIG_LATCH )
+    {
+        assert( Dar_ObjChild0(pGhost) && Dar_ObjChild1(pGhost) == NULL );
+        if ( !Dar_ObjRefs(Dar_ObjFanin0(pGhost)) )
+            return NULL;
+    }
+    else
+    {
+        assert( pGhost->Type == DAR_AIG_AND );
+        assert( Dar_ObjChild0(pGhost) && Dar_ObjChild1(pGhost) );
+        assert( Dar_ObjFanin0(pGhost)->Id < Dar_ObjFanin1(pGhost)->Id );
+        if ( !Dar_ObjRefs(Dar_ObjFanin0(pGhost)) || !Dar_ObjRefs(Dar_ObjFanin1(pGhost)) )
+            return NULL;
+    }
     for ( pEntry = p->pTable[Dar_Hash(pGhost, p->nTableSize)]; pEntry; pEntry = pEntry->pNext )
     {
         if ( Dar_ObjChild0(pEntry) == Dar_ObjChild0(pGhost) && 
diff --git a/src/base/abc/abcDfs.c b/src/base/abc/abcDfs.c
index b682f8ae..39e985c0 100644
--- a/src/base/abc/abcDfs.c
+++ b/src/base/abc/abcDfs.c
@@ -55,7 +55,10 @@ void Abc_NtkDfs_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes )
     assert( Abc_ObjIsNode( pNode ) || Abc_ObjIsBox( pNode ) );
     // visit the transitive fanin of the node
     Abc_ObjForEachFanin( pNode, pFanin, i )
+    {
+//        pFanin = Abc_ObjFanin( pNode, Abc_ObjFaninNum(pNode)-1-i );
         Abc_NtkDfs_rec( Abc_ObjFanin0Ntk(pFanin), vNodes );
+    }
     // add the node after the fanins have been added
     Vec_PtrPush( vNodes, pNode );
 }
diff --git a/src/base/abc/abcNtk.c b/src/base/abc/abcNtk.c
index ce187f60..7d8d0f0f 100644
--- a/src/base/abc/abcNtk.c
+++ b/src/base/abc/abcNtk.c
@@ -987,7 +987,7 @@ void Abc_NtkFixNonDrivenNets( Abc_Ntk_t * pNtk )
     Abc_Obj_t * pNet, * pNode;
     int i;
 
-    if ( Abc_NtkNodeNum(pNtk) == 0 )
+    if ( Abc_NtkNodeNum(pNtk) == 0 && Abc_NtkBoxNum(pNtk) == 0 )
         return;
 
     // check for non-driven nets
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 1e0fed0c..d5321e6d 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -330,7 +330,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
 //    Kit_TruthCountMintermsPrecomp();
 //    Kit_DsdPrecompute4Vars();
 
-    Dar_LibStart();
+//    Dar_LibStart();
 } 
 
 /**Function*************************************************************
@@ -346,7 +346,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
 ***********************************************************************/
 void Abc_End()
 {
-    Dar_LibStop();
+//    Dar_LibStop();
 
     Abc_NtkFraigStoreClean();
 //    Rwt_Man4ExplorePrint();
@@ -5931,7 +5931,7 @@ usage:
 int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
-    Abc_Ntk_t * pNtk;//, * pNtkRes;
+    Abc_Ntk_t * pNtk, * pNtkRes;
     int c;
     int nLevels;
 //    extern Abc_Ntk_t * Abc_NtkNewAig( Abc_Ntk_t * pNtk );
@@ -5940,6 +5940,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
 //    extern int Pr_ManProofTest( char * pFileName );
     extern void Abc_NtkCompareSupports( Abc_Ntk_t * pNtk );
     extern void Abc_NtkCompareCones( Abc_Ntk_t * pNtk );
+    extern Abc_Ntk_t * Abc_NtkDar( Abc_Ntk_t * pNtk );
 
     pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
@@ -6049,8 +6050,21 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
 //    Abc_Ntk4VarTable( pNtk );
 //    Dat_NtkGenerateArrays( pNtk );
 
-    return 0;
+    if ( !Abc_NtkIsStrash(pNtk) )
+    {
+        fprintf( pErr, "Network should be strashed. Command has failed.\n" );
+        return 1;
+    }
+    pNtkRes = Abc_NtkDar( pNtk );
+    if ( pNtkRes == NULL )
+    {
+        fprintf( pErr, "Command has failed.\n" );
+        return 1;
+    }
+    // replace the current network
+    Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
 
+    return 0;
 usage:
     fprintf( pErr, "usage: test [-h]\n" );
     fprintf( pErr, "\t         testbench for new procedures\n" );
@@ -7286,6 +7300,7 @@ int Abc_CommandFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
     int fAllNodes;
     int fExdc;
     int c;
+    int fPartition = 0;
 
     pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
@@ -7307,7 +7322,7 @@ int Abc_CommandFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
     pParams->fVerbose   =    0; // the verbosiness flag
     pParams->fVerboseP  =    0; // the verbosiness flag
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "RDCrscpvaeh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "RDCrscptvaeh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -7360,6 +7375,9 @@ int Abc_CommandFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'v':
             pParams->fVerbose ^= 1;
             break;
+        case 't':
+            fPartition ^= 1;
+            break;
         case 'a':
             fAllNodes ^= 1;
             break;
@@ -7388,13 +7406,28 @@ int Abc_CommandFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
     pParams->fVerboseP = pParams->fTryProve;
 
     // get the new network
-    if ( Abc_NtkIsStrash(pNtk) )
-        pNtkRes = Abc_NtkFraig( pNtk, &Params, fAllNodes, fExdc );
+    if ( fPartition )
+    {
+        pNtkRes = Abc_NtkDup( pNtk );
+        if ( Abc_NtkIsStrash(pNtk) )
+            Abc_NtkFraigPartitionedTime( pNtk, &Params );
+        else
+        {
+            pNtk = Abc_NtkStrash( pNtk, fAllNodes, !fAllNodes, 0 );
+            Abc_NtkFraigPartitionedTime( pNtk, &Params );
+            Abc_NtkDelete( pNtk );
+        }
+    }
     else
     {
-        pNtk = Abc_NtkStrash( pNtk, fAllNodes, !fAllNodes, 0 );
-        pNtkRes = Abc_NtkFraig( pNtk, &Params, fAllNodes, fExdc );
-        Abc_NtkDelete( pNtk );
+        if ( Abc_NtkIsStrash(pNtk) )
+            pNtkRes = Abc_NtkFraig( pNtk, &Params, fAllNodes, fExdc );
+        else
+        {
+            pNtk = Abc_NtkStrash( pNtk, fAllNodes, !fAllNodes, 0 );
+            pNtkRes = Abc_NtkFraig( pNtk, &Params, fAllNodes, fExdc );
+            Abc_NtkDelete( pNtk );
+        }
     }
     if ( pNtkRes == NULL )
     {
@@ -7411,7 +7444,7 @@ int Abc_CommandFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
 
 usage:
     sprintf( Buffer, "%d", pParams->nBTLimit );
-    fprintf( pErr, "usage: fraig [-R num] [-D num] [-C num] [-rscpvah]\n" );
+    fprintf( pErr, "usage: fraig [-R num] [-D num] [-C num] [-rscpvtah]\n" );
     fprintf( pErr, "\t         transforms a logic network into a functionally reduced AIG\n" );
     fprintf( pErr, "\t-R num : number of random patterns (127 < num < 32769) [default = %d]\n",     pParams->nPatsRand );
     fprintf( pErr, "\t-D num : number of systematic patterns (127 < num < 32769) [default = %d]\n", pParams->nPatsDyna );
@@ -7423,6 +7456,7 @@ usage:
     fprintf( pErr, "\t-v     : toggle verbose output [default = %s]\n",                       pParams->fVerbose?  "yes": "no" );
     fprintf( pErr, "\t-e     : toggle functional sweeping using EXDC [default = %s]\n",       fExdc? "yes": "no" );
     fprintf( pErr, "\t-a     : toggle between all nodes and DFS nodes [default = %s]\n",      fAllNodes? "all": "dfs" );
+    fprintf( pErr, "\t-t     : toggle using partitioned representation [default = %s]\n",     fPartition? "yes": "no" );
     fprintf( pErr, "\t-h     : print the command usage\n");
     return 1;
 }
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index 0863061b..81278515 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -25,62 +25,12 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-static Dar_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk );
-static Abc_Ntk_t * Abc_NtkFromDar( Abc_Ntk_t * pNtkOld, Dar_Man_t * pMan );
-
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
 
-  Synopsis    [Gives the current ABC network to AIG manager for processing.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Abc_Ntk_t * Abc_NtkDar( Abc_Ntk_t * pNtk )
-{
-    Abc_Ntk_t * pNtkAig;
-    Dar_Man_t * pMan;//, * pTemp;
-    assert( Abc_NtkIsStrash(pNtk) );
-    // convert to the AIG manager
-    pMan = Abc_NtkToDar( pNtk );
-    if ( pMan == NULL )
-        return NULL;
-    if ( !Dar_ManCheck( pMan ) )
-    {
-        printf( "Abc_NtkDar: AIG check has failed.\n" );
-        Dar_ManStop( pMan );
-        return NULL;
-    }
-    // perform balance
-    Dar_ManPrintStats( pMan );
-//    Dar_ManDumpBlif( pMan, "aig_temp.blif" );
-    pMan->pPars = Dar_ManDefaultParams();
-    Dar_ManRewrite( pMan );
-    Dar_ManPrintStats( pMan );
-    // convert from the AIG manager
-    pNtkAig = Abc_NtkFromDar( pNtk, pMan );
-    if ( pNtkAig == NULL )
-        return NULL;
-    Dar_ManStop( pMan );
-    // make sure everything is okay
-    if ( !Abc_NtkCheck( pNtkAig ) )
-    {
-        printf( "Abc_NtkDar: The network check has failed.\n" );
-        Abc_NtkDelete( pNtkAig );
-        return NULL;
-    }
-    return pNtkAig;
-}
-
-/**Function*************************************************************
-
   Synopsis    [Converts the network from the AIG manager into ABC.]
 
   Description []
@@ -96,7 +46,7 @@ Dar_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk )
     Abc_Obj_t * pObj;
     int i;
     // create the manager
-    pMan = Dar_ManStart( Abc_NtkNodeNum(pNtk) );
+    pMan = Dar_ManStart( Abc_NtkNodeNum(pNtk) + 100 );
     // transfer the pointers to the basic nodes
     Abc_AigConst1(pNtk)->pCopy = (Abc_Obj_t *)Dar_ManConst1(pMan);
     Abc_NtkForEachCi( pNtk, pObj, i )
@@ -122,14 +72,14 @@ Dar_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk )
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Ntk_t * Abc_NtkFromDar( Abc_Ntk_t * pNtk, Dar_Man_t * pMan )
+Abc_Ntk_t * Abc_NtkFromDar( Abc_Ntk_t * pNtkOld, Dar_Man_t * pMan )
 {
     Vec_Ptr_t * vNodes;
     Abc_Ntk_t * pNtkNew;
     Dar_Obj_t * pObj;
     int i;
     // perform strashing
-    pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_STRASH, ABC_FUNC_AIG );
+    pNtkNew = Abc_NtkStartFrom( pNtkOld, ABC_NTK_STRASH, ABC_FUNC_AIG );
     // transfer the pointers to the basic nodes
     Dar_ManConst1(pMan)->pData = Abc_AigConst1(pNtkNew);
     Dar_ManForEachPi( pMan, pObj, i )
@@ -147,6 +97,159 @@ Abc_Ntk_t * Abc_NtkFromDar( Abc_Ntk_t * pNtk, Dar_Man_t * pMan )
     return pNtkNew;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Converts the network from the AIG manager into ABC.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkFromDarSeq( Abc_Ntk_t * pNtkOld, Dar_Man_t * pMan )
+{
+    Vec_Ptr_t * vNodes;
+    Abc_Ntk_t * pNtkNew;
+    Abc_Obj_t * pObjNew, * pFaninNew, * pFaninNew0, * pFaninNew1;
+    Dar_Obj_t * pObj;
+    int i;
+//    assert( Dar_ManLatchNum(pMan) > 0 );
+    // perform strashing
+    pNtkNew = Abc_NtkStartFromNoLatches( pNtkOld, ABC_NTK_STRASH, ABC_FUNC_AIG );
+    // transfer the pointers to the basic nodes
+    Dar_ManConst1(pMan)->pData = Abc_AigConst1(pNtkNew);
+    Dar_ManForEachPi( pMan, pObj, i )
+        pObj->pData = Abc_NtkPi(pNtkNew, i);
+    // create latches of the new network
+    Dar_ManForEachObj( pMan, pObj, i )
+    {
+        if ( !Dar_ObjIsLatch(pObj) )
+            continue;
+        pObjNew = Abc_NtkCreateLatch( pNtkNew );
+        pFaninNew0 = Abc_NtkCreateBi( pNtkNew );
+        pFaninNew1 = Abc_NtkCreateBo( pNtkNew );
+        Abc_ObjAddFanin( pObjNew, pFaninNew0 );
+        Abc_ObjAddFanin( pFaninNew1, pObjNew );
+        Abc_LatchSetInit0( pObjNew );
+        pObj->pData = Abc_ObjFanout0( pObjNew );
+    }
+    Abc_NtkAddDummyBoxNames( pNtkNew );
+    // rebuild the AIG
+    vNodes = Dar_ManDfs( pMan );
+    Vec_PtrForEachEntry( vNodes, pObj, i )
+    {
+        // add the first fanin
+        pObj->pData = pFaninNew0 = (Abc_Obj_t *)Dar_ObjChild0Copy(pObj);
+        if ( Dar_ObjIsBuf(pObj) )
+            continue;
+        // add the second fanin
+        pFaninNew1 = (Abc_Obj_t *)Dar_ObjChild1Copy(pObj);
+        // create the new node
+        if ( Dar_ObjIsExor(pObj) )
+            pObj->pData = pObjNew = Abc_AigXor( pNtkNew->pManFunc, pFaninNew0, pFaninNew1 );
+        else
+            pObj->pData = pObjNew = Abc_AigAnd( pNtkNew->pManFunc, pFaninNew0, pFaninNew1 );
+    }
+    Vec_PtrFree( vNodes );
+    // connect the PO nodes
+    Dar_ManForEachPo( pMan, pObj, i )
+    {
+        pFaninNew = (Abc_Obj_t *)Dar_ObjChild0Copy( pObj );
+        Abc_ObjAddFanin( Abc_NtkPo(pNtkNew, i), pFaninNew );
+    }
+    // connect the latches
+    Dar_ManForEachObj( pMan, pObj, i )
+    {
+        if ( !Dar_ObjIsLatch(pObj) )
+            continue;
+        pFaninNew = (Abc_Obj_t *)Dar_ObjChild0Copy( pObj );
+        Abc_ObjAddFanin( Abc_ObjFanin0(Abc_ObjFanin0(pObj->pData)), pFaninNew );
+    }
+    if ( !Abc_NtkCheck( pNtkNew ) )
+        fprintf( stdout, "Abc_NtkFromIvySeq(): Network check has failed.\n" );
+    return pNtkNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collect latch values.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int * Abc_NtkGetLatchValues( Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pLatch;
+    int i, * pArray;
+    pArray = ALLOC( int, Abc_NtkLatchNum(pNtk) );
+    Abc_NtkForEachLatch( pNtk, pLatch, i )
+        pArray[i] = Abc_LatchIsInit1(pLatch);
+    return pArray;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Gives the current ABC network to AIG manager for processing.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkDar( Abc_Ntk_t * pNtk )
+{
+    Abc_Ntk_t * pNtkAig;
+    Dar_Man_t * pMan;//, * pTemp;
+    int * pArray;
+
+    assert( Abc_NtkIsStrash(pNtk) );
+    // convert to the AIG manager
+    pMan = Abc_NtkToDar( pNtk );
+    if ( pMan == NULL )
+        return NULL;
+    if ( !Dar_ManCheck( pMan ) )
+    {
+        printf( "Abc_NtkDar: AIG check has failed.\n" );
+        Dar_ManStop( pMan );
+        return NULL;
+    }
+    // perform balance
+    Dar_ManPrintStats( pMan );
+
+    pArray = Abc_NtkGetLatchValues(pNtk);
+    Dar_ManSeqStrash( pMan, Abc_NtkLatchNum(pNtk), pArray );
+    free( pArray );
+
+//    Dar_ManDumpBlif( pMan, "aig_temp.blif" );
+//    pMan->pPars = Dar_ManDefaultParams();
+//    Dar_ManRewrite( pMan );
+    Dar_ManPrintStats( pMan );
+    // convert from the AIG manager
+    if ( Dar_ManLatchNum(pMan) )
+        pNtkAig = Abc_NtkFromDarSeq( pNtk, pMan );
+    else
+        pNtkAig = Abc_NtkFromDar( pNtk, pMan );
+    if ( pNtkAig == NULL )
+        return NULL;
+    Dar_ManStop( pMan );
+    // make sure everything is okay
+    if ( !Abc_NtkCheck( pNtkAig ) )
+    {
+        printf( "Abc_NtkDar: The network check has failed.\n" );
+        Abc_NtkDelete( pNtkAig );
+        return NULL;
+    }
+    return pNtkAig;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abci/abcFraig.c b/src/base/abci/abcFraig.c
index 30e49af2..fa6771b3 100644
--- a/src/base/abci/abcFraig.c
+++ b/src/base/abci/abcFraig.c
@@ -687,7 +687,7 @@ int Abc_NtkFraigStore( Abc_Ntk_t * pNtk )
         // set the number of networks stored
         Abc_FrameSetNtkStoreSize( Abc_FrameReadNtkStoreSize() + 1 );
     }
-//    printf( "The number of AIG nodes added to storage = %5d.\n", Abc_NtkNodeNum(pStore) - nAndsOld );
+    printf( "The number of AIG nodes added to storage = %5d.\n", Abc_NtkNodeNum(pStore) - nAndsOld );
     return 1;
 }
 
@@ -734,7 +734,7 @@ Abc_Ntk_t * Abc_NtkFraigRestore()
     Fraig_ParamsSetDefault( &Params );
     Params.nPatsRand  = nWordsMin * 32; // the number of words of random simulation info
     Params.nPatsDyna  = nWordsMin * 32; // the number of words of dynamic simulation info
-    Params.nBTLimit   = 99;             // the max number of backtracks to perform
+    Params.nBTLimit   = 999999;             // the max number of backtracks to perform
     Params.fFuncRed   =  1;             // performs only one level hashing
     Params.fFeedBack  =  1;             // enables solver feedback
     Params.fDist1Pats =  1;             // enables distance-1 patterns
diff --git a/src/base/abci/abcPart.c b/src/base/abci/abcPart.c
index 748868de..787e3f88 100644
--- a/src/base/abci/abcPart.c
+++ b/src/base/abci/abcPart.c
@@ -698,12 +698,67 @@ Abc_Ntk_t * Abc_NtkFraigPartitioned( Abc_Ntk_t * pNtk, void * pParams )
     // derive the final network
     pNtkFraig = Abc_NtkPartStitchChoices( pNtk, vFraigs );
     Vec_PtrForEachEntry( vFraigs, pNtkAig, i )
+    {
+//        Abc_NtkPrintStats( stdout, pNtkAig, 0 );
         Abc_NtkDelete( pNtkAig );
+    }
     Vec_PtrFree( vFraigs );
 
     return pNtkFraig;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Stitches together several networks with choice nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkFraigPartitionedTime( Abc_Ntk_t * pNtk, void * pParams )
+{
+    extern int Cmd_CommandExecute( void * pAbc, char * sCommand );
+    extern void * Abc_FrameGetGlobalFrame();
+
+    Vec_Vec_t * vParts;
+    Vec_Ptr_t * vFraigs, * vOne;
+    Abc_Ntk_t * pNtkAig, * pNtkFraig;
+    int i;
+    int clk = clock();
+
+    // perform partitioning
+    assert( Abc_NtkIsStrash(pNtk) );
+//    vParts = Abc_NtkPartitionNaive( pNtk, 20 );
+    vParts = Abc_NtkPartitionSmart( pNtk, 0, 0 );
+
+    Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), "unset progressbar" );
+
+    // fraig each partition
+    vFraigs = Vec_PtrAlloc( Vec_VecSize(vParts) );
+    Vec_VecForEachLevel( vParts, vOne, i )
+    {
+        pNtkAig = Abc_NtkCreateConeArray( pNtk, vOne, 0 );
+        pNtkFraig = Abc_NtkFraig( pNtkAig, pParams, 0, 0 );
+        Vec_PtrPush( vFraigs, pNtkFraig );
+        Abc_NtkDelete( pNtkAig );
+
+        printf( "Finished part %d (out of %d)\r", i+1, Vec_VecSize(vParts) );
+    }
+    Vec_VecFree( vParts );
+
+    Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), "set progressbar" );
+
+    // derive the final network
+    Vec_PtrForEachEntry( vFraigs, pNtkAig, i )
+        Abc_NtkDelete( pNtkAig );
+    Vec_PtrFree( vFraigs );
+
+    PRT( "Partitioned fraiging time", clock() - clk );
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/io/ioReadAiger.c b/src/base/io/ioReadAiger.c
index a54a00fe..fe519476 100644
--- a/src/base/io/ioReadAiger.c
+++ b/src/base/io/ioReadAiger.c
@@ -96,7 +96,7 @@ Abc_Ntk_t * Io_ReadAiger( char * pFileName, int fCheck )
 
     // prepare the array of nodes
     vNodes = Vec_PtrAlloc( 1 + nInputs + nLatches + nAnds );
-    Vec_PtrPush( vNodes, Abc_AigConst1(pNtkNew) );
+    Vec_PtrPush( vNodes, Abc_ObjNot( Abc_AigConst1(pNtkNew) ) );
 
     // create the PIs
     for ( i = 0; i < nInputs; i++ )
@@ -122,6 +122,8 @@ Abc_Ntk_t * Io_ReadAiger( char * pFileName, int fCheck )
         Vec_PtrPush( vNodes, pNode1 );
         // assign names to latch and its input
         Abc_ObjAssignName( pObj, Abc_ObjNameDummy("_L", i, nDigits), NULL );
+
+        printf( "Creating latch %s with input %d and output %d.\n", Abc_ObjName(pObj), pNode0->Id, pNode1->Id );
     } 
     
     // remember the beginning of latch/PO literals
@@ -156,14 +158,17 @@ Abc_Ntk_t * Io_ReadAiger( char * pFileName, int fCheck )
     Abc_NtkForEachLatchInput( pNtkNew, pObj, i )
     {
         uLit0 = atoi( pCur );  while ( *pCur++ != '\n' );
-        pNode0 = Abc_ObjNotCond( Vec_PtrEntry(vNodes, uLit0 >> 1), (uLit0 & 1) ^ (uLit0 < 2) );
+        pNode0 = Abc_ObjNotCond( Vec_PtrEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );//^ (uLit0 < 2) );
         Abc_ObjAddFanin( pObj, pNode0 );
+
+        printf( "Adding input %d to latch input %d.\n", pNode0->Id, pObj->Id );
+
     }
     // read the PO driver literals
     Abc_NtkForEachPo( pNtkNew, pObj, i )
     {
         uLit0 = atoi( pCur );  while ( *pCur++ != '\n' );
-        pNode0 = Abc_ObjNotCond( Vec_PtrEntry(vNodes, uLit0 >> 1), (uLit0 & 1) ^ (uLit0 < 2) );
+        pNode0 = Abc_ObjNotCond( Vec_PtrEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );//^ (uLit0 < 2) );
         Abc_ObjAddFanin( pObj, pNode0 );
     }
 
@@ -204,7 +209,7 @@ Abc_Ntk_t * Io_ReadAiger( char * pFileName, int fCheck )
             Abc_ObjAssignName( Abc_ObjFanin0(Abc_ObjFanin0(pObj)), Abc_ObjName(pObj), "L" );
         // mark the node as named
         pObj->pCopy = (Abc_Obj_t *)Abc_ObjName(pObj);
-    }
+    } 
     // skipping the comments
     free( pContents );
     Vec_PtrFree( vNodes );
diff --git a/src/base/io/ioReadBench.c b/src/base/io/ioReadBench.c
index 2730ba69..ba622e40 100644
--- a/src/base/io/ioReadBench.c
+++ b/src/base/io/ioReadBench.c
@@ -118,7 +118,13 @@ Abc_Ntk_t * Io_ReadBenchNetwork( Extra_FileReader_t * p )
             if ( strncmp(pType, "DFF", 3) == 0 ) // works for both DFF and DFFRSE
             {
                 pNode = Io_ReadCreateLatch( pNtk, vTokens->pArray[2], vTokens->pArray[0] );
-                Abc_LatchSetInit0( pNode );
+//                Abc_LatchSetInit0( pNode );
+                if ( pType[3] == '0' )
+                    Abc_LatchSetInit0( pNode );
+                else if ( pType[3] == '1' )
+                    Abc_LatchSetInit1( pNode );
+                else
+                    Abc_LatchSetInitDc( pNode );
             }
             else if ( strcmp(pType, "LUT") == 0 )
             {
diff --git a/src/base/io/ioWriteVerilog.c b/src/base/io/ioWriteVerilog.c
index a02d53fd..a4eeb78f 100644
--- a/src/base/io/ioWriteVerilog.c
+++ b/src/base/io/ioWriteVerilog.c
@@ -113,7 +113,12 @@ void Io_WriteVerilogInt( FILE * pFile, Abc_Ntk_t * pNtk )
 {
     // write inputs and outputs
 //    fprintf( pFile, "module %s ( gclk,\n   ", Abc_NtkName(pNtk) );
-    fprintf( pFile, "module %s ( \n   ", Abc_NtkName(pNtk) );
+    fprintf( pFile, "module %s ( ", Abc_NtkName(pNtk) );
+    // add the clock signal if it does not exist
+    if ( Abc_NtkLatchNum(pNtk) > 0 && Nm_ManFindIdByName(pNtk->pManName, "clock", ABC_OBJ_PI) == -1 )
+        fprintf( pFile, "clock, " );
+    // write other primary inputs
+    fprintf( pFile, "\n   " );
     if ( Abc_NtkPiNum(pNtk) > 0  )
     {
         Io_WriteVerilogPis( pFile, pNtk, 3 );
@@ -435,7 +440,8 @@ void Io_WriteVerilogLatches( FILE * pFile, Abc_Ntk_t * pNtk )
         return;
     // write the latches
 //    fprintf( pFile, "  always @(posedge %s) begin\n", Io_WriteVerilogGetName(Abc_ObjFanout0(Abc_NtkPi(pNtk,0))) );
-    fprintf( pFile, "  always begin\n" );
+//    fprintf( pFile, "  always begin\n" );
+    fprintf( pFile, "  always @ (posedge clock) begin\n" );
     Abc_NtkForEachLatch( pNtk, pLatch, i )
     {
         fprintf( pFile, "    %s", Io_WriteVerilogGetName(Abc_ObjName(Abc_ObjFanout0(Abc_ObjFanout0(pLatch)))) );
diff --git a/src/base/io/ioWriteVerilog.zip b/src/base/io/ioWriteVerilog.zip
new file mode 100644
index 00000000..19e68a89
--- /dev/null
+++ b/src/base/io/ioWriteVerilog.zip
diff --git a/src/base/ver/ver.h b/src/base/ver/ver.h
index cf2b7497..9c538ac4 100644
--- a/src/base/ver/ver.h
+++ b/src/base/ver/ver.h
@@ -66,6 +66,7 @@ struct Ver_Man_t_
     Vec_Ptr_t *     vNames;  
     Vec_Ptr_t *     vStackFn;
     Vec_Int_t *     vStackOp;
+    Vec_Int_t *     vPerm;
 };
 
 
diff --git a/src/base/ver/verCore.c b/src/base/ver/verCore.c
index 12c54dba..6d7d230e 100644
--- a/src/base/ver/verCore.c
+++ b/src/base/ver/verCore.c
@@ -110,6 +110,7 @@ Ver_Man_t * Ver_ParseStart( char * pFileName, Abc_Lib_t * pGateLib )
     p->vNames    = Vec_PtrAlloc( 100 );
     p->vStackFn  = Vec_PtrAlloc( 100 );
     p->vStackOp  = Vec_IntAlloc( 100 );
+    p->vPerm     = Vec_IntAlloc( 100 );
     // create the design library and assign the technology library
     p->pDesign   = Abc_LibCreate( pFileName );
     p->pDesign->pLibrary = pGateLib;
@@ -136,6 +137,7 @@ void Ver_ParseStop( Ver_Man_t * p )
     Vec_PtrFree( p->vNames   );
     Vec_PtrFree( p->vStackFn );
     Vec_IntFree( p->vStackOp );
+    Vec_IntFree( p->vPerm );
     free( p );
 }
  
@@ -1193,6 +1195,12 @@ int Ver_ParseAssign( Ver_Man_t * pMan, Abc_Ntk_t * pNtk )
                     pFunc = (Hop_Obj_t *)Mio_LibraryReadConst1(Abc_FrameReadLibGen());
                 else
                 {
+                    // "assign foo = \bar ;"
+                    if ( *pEquation == '\\' )
+                    {
+                        pEquation++;
+                        pEquation[strlen(pEquation) - 1] = 0;
+                    }
                     if ( Ver_ParseFindNet(pNtk, pEquation) == NULL )
                     {
                         sprintf( pMan->sError, "Cannot read Verilog with non-trivial assignments in the mapped netlist." );
@@ -1358,6 +1366,29 @@ int Ver_ParseGateStandard( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Ver_GateType_t Ga
 
 /**Function*************************************************************
 
+  Synopsis    [Returns the index of the given pin the gate.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ver_FindGateInput( Mio_Gate_t * pGate, char * pName )
+{
+    Mio_Pin_t * pGatePin;
+    int i;
+    for ( i = 0, pGatePin = Mio_GateReadPins(pGate); pGatePin != NULL; pGatePin = Mio_PinReadNext(pGatePin), i++ )
+        if ( strcmp(pName, Mio_PinReadName(pGatePin)) == 0 )
+            return i;
+    if ( strcmp(pName, Mio_GateReadOutName(pGate)) == 0 )
+        return i;
+    return -1;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Parses one directive.]
 
   Description []
@@ -1369,10 +1400,10 @@ int Ver_ParseGateStandard( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Ver_GateType_t Ga
 ***********************************************************************/
 int Ver_ParseGate( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Mio_Gate_t * pGate )
 {
-    Mio_Pin_t * pGatePin;
     Ver_Stream_t * p = pMan->pReader;
     Abc_Obj_t * pNetActual, * pNode;
     char * pWord, Symbol;
+    int Input, i, nFanins = Mio_GateReadInputs(pGate);
 
     // convert from the blackbox into the network with local functions representated by gates
     if ( 1 != pMan->fMapped )
@@ -1404,7 +1435,7 @@ int Ver_ParseGate( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Mio_Gate_t * pGate )
     pNode->pData = pGate;
 
     // parse pairs of formal/actural inputs
-    pGatePin = Mio_GateReadPins(pGate);
+    Vec_IntClear( pMan->vPerm );
     while ( 1 )
     {
         // process one pair of formal/actual parameters
@@ -1420,24 +1451,13 @@ int Ver_ParseGate( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Mio_Gate_t * pGate )
         if ( pWord == NULL )
             return 0;
 
-        // make sure that the formal name is the same as the gate's
-        if ( Mio_GateReadInputs(pGate) == Abc_ObjFaninNum(pNode) ) 
-        {
-            if ( strcmp(pWord, Mio_GateReadOutName(pGate)) )
-            {
-                sprintf( pMan->sError, "Formal output name listed %s is different from the name of the gate output %s.", pWord, Mio_GateReadOutName(pGate) );
-                Ver_ParsePrintErrorMessage( pMan );
-                return 0;
-            }
-        }
-        else
+        // find the corresponding pin of the gate
+        Input = Ver_FindGateInput( pGate, pWord );
+        if ( Input == -1 )
         {
-            if ( strcmp(pWord, Mio_PinReadName(pGatePin)) )
-            {
-                sprintf( pMan->sError, "Formal input name listed %s is different from the name of the corresponding pin %s.", pWord, Mio_PinReadName(pGatePin) );
-                Ver_ParsePrintErrorMessage( pMan );
-                return 0;
-            }
+            sprintf( pMan->sError, "Formal input name %s cannot be found in the gate %s.", pWord, Mio_GateReadOutName(pGate) );
+            Ver_ParsePrintErrorMessage( pMan );
+            return 0;
         }
 
         // open the paranthesis
@@ -1482,10 +1502,13 @@ int Ver_ParseGate( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Mio_Gate_t * pGate )
         }
 
         // add the fanin
-        if ( Mio_GateReadInputs(pGate) == Abc_ObjFaninNum(pNode) )
-            Abc_ObjAddFanin( pNetActual, pNode ); // fanout
-        else
+        if ( Input < nFanins )
+        {
+            Vec_IntPush( pMan->vPerm, Input );
             Abc_ObjAddFanin( pNode, pNetActual ); // fanin
+        }
+        else
+            Abc_ObjAddFanin( pNetActual, pNode ); // fanout
 
         // check if it is the end of gate
         Ver_ParseSkipComments( pMan );
@@ -1501,13 +1524,10 @@ int Ver_ParseGate( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Mio_Gate_t * pGate )
             return 0;
         }
         Ver_ParseSkipComments( pMan );
-
-        // get the next pin
-        pGatePin = Mio_PinReadNext(pGatePin);
     }
 
     // check that the gate as the same number of input
-    if ( !(Abc_ObjFaninNum(pNode) == Mio_GateReadInputs(pGate) && Abc_ObjFanoutNum(pNode) == 1) )
+    if ( !(Abc_ObjFaninNum(pNode) == nFanins && Abc_ObjFanoutNum(pNode) == 1) )
     {
         sprintf( pMan->sError, "Parsing of gate %s has failed.", Mio_GateReadName(pGate) );
         Ver_ParsePrintErrorMessage( pMan );
@@ -1522,6 +1542,20 @@ int Ver_ParseGate( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Mio_Gate_t * pGate )
         Ver_ParsePrintErrorMessage( pMan );
         return 0;
     }
+    
+    // check if we need to permute the inputs
+    Vec_IntForEachEntry( pMan->vPerm, Input, i )
+        if ( Input != i )
+            break;
+    if ( i < Vec_IntSize(pMan->vPerm) )
+    {
+        // add the fanin numnbers to the end of the permuation array
+        for ( i = 0; i < nFanins; i++ )
+            Vec_IntPush( pMan->vPerm, Abc_ObjFaninId(pNode, i) );
+        // write the fanin numbers into their corresponding places (according to the gate) 
+        for ( i = 0; i < nFanins; i++ )
+            Vec_IntWriteEntry( &pNode->vFanins, Vec_IntEntry(pMan->vPerm, i), Vec_IntEntry(pMan->vPerm, i+nFanins) );
+    }
     return 1;
 }
 
@@ -1546,6 +1580,7 @@ int Ver_ParseBox( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkBox )
     Abc_Obj_t * pNode;
     char * pWord, Symbol;
     int fCompl, fFormalIsGiven;
+    int i, k, Bit, Limit, nMsb, nLsb, fQuit, flag;
 
     // gate the name of the box
     pWord = Ver_ParseGetName( pMan );
@@ -1613,8 +1648,6 @@ int Ver_ParseBox( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkBox )
         // consider the case of vector-inputs
         if ( Symbol == '{' )
         {
-            int i, k, Bit, Limit, nMsb, nLsb, fQuit;
-
             // skip this char
             Ver_StreamPopChar(p);
 
@@ -1673,7 +1706,8 @@ int Ver_ParseBox( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkBox )
                         pNetActual = Ver_ParseFindNet( pNtk, pWord );
                         if ( pNetActual == NULL )
                         {
-                            if ( !strncmp(pWord, "Open_", 5) ) 
+                            if ( !strncmp(pWord, "Open_", 5) ||
+                                !strncmp(pWord, "dct_unconnected", 15) ) 
                                 pNetActual = Abc_NtkCreateNet( pNtk );
                             else
                             {
@@ -1697,7 +1731,8 @@ int Ver_ParseBox( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkBox )
                             pNetActual = Ver_ParseFindNet( pNtk, Buffer );
                             if ( pNetActual == NULL )
                             {
-                                if ( !strncmp(pWord, "Open_", 5) ) 
+                                if ( !strncmp(pWord, "Open_", 5) ||
+                                    !strncmp(pWord, "dct_unconnected", 15) ) 
                                     pNetActual = Abc_NtkCreateNet( pNtk );
                                 else
                                 {
@@ -1738,34 +1773,72 @@ int Ver_ParseBox( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkBox )
             if ( pWord[0] == 0 )
             {
                 pNetActual = Abc_NtkCreateNet( pNtk );
+                Vec_PtrPush( pBundle->vNetsActual, Abc_ObjNotCond( pNetActual, fCompl ) );
             }
             else
             {
-/*
-            // check if the name is complemented
-            fCompl = (pWord[0] == '~');
-            if ( fCompl )
-            {
-                pWord++;
-                if ( pNtk->pData == NULL )
-                    pNtk->pData = Extra_MmFlexStart();
-            }
-*/
                 // get the actual net
+                flag=0;
                 pNetActual = Ver_ParseFindNet( pNtk, pWord );
-                if ( pNetActual == NULL )
+                if ( pNetActual == NULL ) 
                 {
-                    if ( !strncmp(pWord, "Open_", 5) ) 
-                        pNetActual = Abc_NtkCreateNet( pNtk );
-                    else
+                    Ver_ParseLookupSuffix( pMan, pWord, &nMsb, &nLsb );
+                    if ( nMsb == -1 && nLsb == -1 ) 
                     {
-                        sprintf( pMan->sError, "Actual net \"%s\" is missing in box \"%s\".", pWord, Abc_ObjName(pNode) );
-                        Ver_ParsePrintErrorMessage( pMan );
-                        return 0;
+                        Ver_ParseSignalSuffix( pMan, pWord, &nMsb, &nLsb );
+                        if ( nMsb == -1 && nLsb == -1 ) 
+                        {
+                            if ( !strncmp(pWord, "Open_", 5) ||
+                                !strncmp(pWord, "dct_unconnected", 15) ) 
+                            {
+                                pNetActual = Abc_NtkCreateNet( pNtk );
+                                Vec_PtrPush( pBundle->vNetsActual, pNetActual );
+                            } 
+                            else 
+                            {
+                                sprintf( pMan->sError, "Actual net \"%s\" is missing in box \"%s\".", pWord, Abc_ObjName(pNode) );
+                                Ver_ParsePrintErrorMessage( pMan );
+                                return 0;
+                            }
+                        } 
+                        else 
+                        {
+                            flag=1;
+                        }
+                    } 
+                    else 
+                    {
+                        flag=1;
                     }
+                    if (flag) 
+                    {
+                        Limit = (nMsb > nLsb) ? nMsb - nLsb + 1: nLsb - nMsb + 1;  
+                        for ( Bit = nMsb, k = Limit - 1; k >= 0; Bit = (nMsb > nLsb ? Bit - 1: Bit + 1), k--)
+                        {
+                            // get the actual net
+                            sprintf( Buffer, "%s[%d]", pWord, Bit );
+                            pNetActual = Ver_ParseFindNet( pNtk, Buffer );
+                            if ( pNetActual == NULL )
+                            {
+                                if ( !strncmp(pWord, "Open_", 5) ||
+                                    !strncmp(pWord, "dct_unconnected", 15)) 
+                                    pNetActual = Abc_NtkCreateNet( pNtk );
+                                else
+                                {
+                                    sprintf( pMan->sError, "Actual net \"%s\" is missing in box \"%s\".", pWord, Abc_ObjName(pNode) );
+                                    Ver_ParsePrintErrorMessage( pMan );
+                                    return 0;
+                                }
+                            }
+                            Vec_PtrPush( pBundle->vNetsActual, pNetActual );
+                        }
+                    }
+                } 
+                else 
+                {
+                    Vec_PtrPush( pBundle->vNetsActual, Abc_ObjNotCond( pNetActual, fCompl ) );
                 }
             }
-            Vec_PtrPush( pBundle->vNetsActual, Abc_ObjNotCond( pNetActual, fCompl ) );
         }
 
         if ( fFormalIsGiven )
@@ -2000,8 +2073,8 @@ int Ver_ParseConnectBox( Ver_Man_t * pMan, Abc_Obj_t * pBox )
             }
             if ( pBundle == NULL )
             {
-                printf( "Warning: The formal output %s is not driven when instantiating network %s in box %s.", 
-                    pNameFormal, pNtkBox->pName, Abc_ObjName(pBox) );
+//                printf( "Warning: The formal output %s is not driven when instantiating network %s in box %s.", 
+//                    pNameFormal, pNtkBox->pName, Abc_ObjName(pBox) );
                 continue;
             }
         }
diff --git a/src/base/ver/verCore.zip b/src/base/ver/verCore.zip
index 45574008..cdfcf5a4 100644
--- a/src/base/ver/verCore.zip
+++ b/src/base/ver/verCore.zip
diff --git a/src/map/if/ifUtil.c b/src/map/if/ifUtil.c
index f4ffa4c1..f3fa049e 100644
--- a/src/map/if/ifUtil.c
+++ b/src/map/if/ifUtil.c
@@ -427,6 +427,26 @@ int If_ManCrossCut( If_Man_t * p )
     return nCutSizeMax;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Computes cross-cut of the circuit.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int If_ManCountTrueArea( If_Man_t * p )
+{
+    If_Obj_t * pObj;
+    int i, Area = 0;
+    Vec_PtrForEachEntry( p->vMapped, pObj, i )
+        Area += 1 + (If_ObjCutBest(pObj)->nLeaves > (unsigned)p->pPars->nLutSize / 2);
+    return Area;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////