Version abc70817

18 files changed, 2495 insertions, 29 deletions

diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h
index d6a97257..a1abd2b7 100644
--- a/src/aig/aig/aig.h
+++ b/src/aig/aig/aig.h
@@ -126,6 +126,7 @@ struct Aig_Man_t_
     void *           pData;          // the temporary data
     int              nTravIds;       // the current traversal ID
     int              fCatchExor;     // enables EXOR nodes
+    int              fAddStrash;     // performs additional strashing
     // timing statistics
     int              time1;
     int              time2;
@@ -149,7 +150,16 @@ static inline int          Aig_TruthWordNum( int nVars )          { return nVars
 static inline int          Aig_InfoHasBit( unsigned * p, int i )  { return (p[(i)>>5] & (1<<((i) & 31))) > 0;       }
 static inline void         Aig_InfoSetBit( unsigned * p, int i )  { p[(i)>>5] |= (1<<((i) & 31));                   }
 static inline void         Aig_InfoXorBit( unsigned * p, int i )  { p[(i)>>5] ^= (1<<((i) & 31));                   }
+static inline unsigned     Aig_InfoMask( int nVar )               { return (~(unsigned)0) >> (32-nVar);             }
 static inline unsigned     Aig_ObjCutSign( unsigned ObjId )       { return (1 << (ObjId & 31));                     }
+static inline int          Aig_WordCountOnes( unsigned uWord )
+{
+    uWord = (uWord & 0x55555555) + ((uWord>>1) & 0x55555555);
+    uWord = (uWord & 0x33333333) + ((uWord>>2) & 0x33333333);
+    uWord = (uWord & 0x0F0F0F0F) + ((uWord>>4) & 0x0F0F0F0F);
+    uWord = (uWord & 0x00FF00FF) + ((uWord>>8) & 0x00FF00FF);
+    return  (uWord & 0x0000FFFF) + (uWord>>16);
+}
 
 static inline Aig_Obj_t *  Aig_Regular( Aig_Obj_t * p )           { return (Aig_Obj_t *)((unsigned long)(p) & ~01); }
 static inline Aig_Obj_t *  Aig_Not( Aig_Obj_t * p )               { return (Aig_Obj_t *)((unsigned long)(p) ^  01); }
@@ -328,6 +338,10 @@ static inline int     Aig_ObjFanoutNext( Aig_Man_t * p, int iFan )   { assert(iF
 // iterator over the latch inputs
 #define Aig_ManForEachLiSeq( p, pObj, i )                                       \
     Vec_PtrForEachEntryStart( p->vPos, pObj, i, Aig_ManPoNum(p)-Aig_ManRegNum(p) )
+// iterator over the latch input and outputs
+#define Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, k )                           \
+    for ( k = 0; (k < Aig_ManRegNum(p)) && (((pObjLi) = Aig_ManLi(p, k)), 1)    \
+        && (((pObjLo)=Aig_ManLo(p, k)), 1); k++ )
 
 ////////////////////////////////////////////////////////////////////////
 ///                    FUNCTION DECLARATIONS                         ///
@@ -358,10 +372,14 @@ extern void            Aig_ManFanoutStop( Aig_Man_t * p );
 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_ManRemap( Aig_Man_t * p, Vec_Ptr_t * vMap );
 extern Aig_Man_t *     Aig_ManExtractMiter( Aig_Man_t * p, Aig_Obj_t * pNode1, Aig_Obj_t * pNode2 );
 extern void            Aig_ManStop( Aig_Man_t * p );
 extern int             Aig_ManCleanup( Aig_Man_t * p );
+extern int             Aig_ManCountMergeRegs( Aig_Man_t * p );
+extern int             Aig_ManSeqCleanup( Aig_Man_t * p );
 extern void            Aig_ManPrintStats( Aig_Man_t * p );
+extern Aig_Man_t *     Aig_ManReduceLaches( Aig_Man_t * p, int fVerbose );
 /*=== aigMem.c ==========================================================*/
 extern void            Aig_ManStartMemory( Aig_Man_t * p );
 extern void            Aig_ManStopMemory( Aig_Man_t * p );
@@ -414,8 +432,11 @@ extern void            Aig_ManTransferRepr( Aig_Man_t * pNew, Aig_Man_t * p );
 extern Aig_Man_t *     Aig_ManDupRepr( Aig_Man_t * p );
 extern Aig_Man_t *     Aig_ManRehash( Aig_Man_t * p );
 extern void            Aig_ManCreateChoices( Aig_Man_t * p );
+/*=== aigRet.c ========================================================*/
+extern Aig_Man_t *     Rtm_ManRetimeFwd( Aig_Man_t * p, int nStepsMax, int fVerbose );
 /*=== aigSeq.c ========================================================*/
 extern int             Aig_ManSeqStrash( Aig_Man_t * p, int nLatches, int * pInits );
+extern Aig_Man_t *     Aig_ManConstReduce( Aig_Man_t * p, int fVerbose );
 /*=== aigShow.c ========================================================*/
 extern void            Aig_ManShow( Aig_Man_t * pMan, int fHaig, Vec_Ptr_t * vBold );
 /*=== aigTable.c ========================================================*/
diff --git a/src/aig/aig/aigMan.c b/src/aig/aig/aigMan.c
index 818b75fe..d09bf41b 100644
--- a/src/aig/aig/aigMan.c
+++ b/src/aig/aig/aigMan.c
@@ -172,6 +172,54 @@ Aig_Man_t * Aig_ManDup( Aig_Man_t * p, int fOrdered )
 
 /**Function*************************************************************
 
+  Synopsis    [Remaps the manager.]
+
+  Description [Map in the array specifies for each CI nodes the node that
+  should be used after remapping.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Aig_ManRemap( Aig_Man_t * p, Vec_Ptr_t * vMap )
+{
+    Aig_Man_t * pNew;
+    Aig_Obj_t * pObj, * pObjMapped;
+    int i;
+    // create the new manager
+    pNew = Aig_ManStart( Aig_ManObjIdMax(p) + 1 );
+    pNew->nRegs = p->nRegs;
+    pNew->nAsserts = p->nAsserts;
+    // create the PIs
+    Aig_ManCleanData( p );
+    Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
+    Aig_ManForEachPi( p, pObj, i )
+        pObj->pData = Aig_ObjCreatePi(pNew);
+    // implement the mapping
+    Aig_ManForEachPi( p, pObj, i )
+    {
+        pObjMapped = Vec_PtrEntry( vMap, i );
+        pObj->pData = Aig_NotCond( Aig_Regular(pObjMapped)->pData, Aig_IsComplement(pObjMapped) );
+    }
+    // duplicate internal nodes
+    Aig_ManForEachObj( p, pObj, i )
+        if ( Aig_ObjIsBuf(pObj) )
+            pObj->pData = Aig_ObjChild0Copy(pObj);
+        else if ( Aig_ObjIsNode(pObj) )
+            pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
+    // add the POs
+    Aig_ManForEachPo( p, pObj, i )
+        Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
+    assert( Aig_ManNodeNum(p) >= Aig_ManNodeNum(pNew) );
+    // check the resulting network
+    if ( !Aig_ManCheck(pNew) )
+        printf( "Aig_ManDup(): The check has failed.\n" );
+    return pNew;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Extracts the miter composed of XOR of the two nodes.]
 
   Description []
@@ -257,6 +305,110 @@ void Aig_ManStop( Aig_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
+void Aig_ManSeqCleanup_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vNodes )
+{
+    if ( Aig_ObjIsTravIdCurrent(p, pObj) )
+        return;
+    Aig_ObjSetTravIdCurrent(p, pObj);
+    // collect latch input corresponding to unmarked PI (latch output)
+    if ( Aig_ObjIsPi(pObj) )
+    {
+        Vec_PtrPush( vNodes, pObj->pNext );
+        return;
+    }
+    if ( Aig_ObjIsPo(pObj) )
+    {
+        Aig_ManSeqCleanup_rec( p, Aig_ObjFanin0(pObj), vNodes );
+        return;
+    }
+    assert( Aig_ObjIsNode(pObj) );
+    Aig_ManSeqCleanup_rec( p, Aig_ObjFanin0(pObj), vNodes );
+    Aig_ManSeqCleanup_rec( p, Aig_ObjFanin1(pObj), vNodes );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the number of dangling nodes removed.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Aig_ManSeqCleanup( Aig_Man_t * p )
+{
+    Vec_Ptr_t * vNodes, * vCis, * vCos;
+    Aig_Obj_t * pObj, * pObjLi, * pObjLo;
+    int i, nTruePis, nTruePos;
+    assert( Aig_ManBufNum(p) == 0 );
+
+    // mark the PIs
+    Aig_ManIncrementTravId( p );
+    Aig_ObjSetTravIdCurrent( p, Aig_ManConst1(p) );
+    Aig_ManForEachPiSeq( p, pObj, i )
+        Aig_ObjSetTravIdCurrent( p, pObj );
+
+    // prepare to collect nodes reachable from POs
+    vNodes = Vec_PtrAlloc( 100 );
+    Aig_ManForEachPoSeq( p, pObj, i )
+        Vec_PtrPush( vNodes, pObj );
+
+    // remember latch inputs in latch outputs
+    Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i )
+        pObjLo->pNext = pObjLi;
+    // mark the nodes reachable from these nodes
+    Vec_PtrForEachEntry( vNodes, pObj, i )
+        Aig_ManSeqCleanup_rec( p, pObj, vNodes );
+    assert( Vec_PtrSize(vNodes) <= Aig_ManPoNum(p) );
+    // clean latch output pointers
+    Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i )
+        pObjLo->pNext = NULL;
+
+    // if some latches are removed, update PIs/POs
+    if ( Vec_PtrSize(vNodes) < Aig_ManPoNum(p) )
+    {
+        // collect new CIs/COs
+        vCis = Vec_PtrAlloc( Aig_ManPiNum(p) );
+        Aig_ManForEachPi( p, pObj, i )
+            if ( Aig_ObjIsTravIdCurrent(p, pObj) )
+                Vec_PtrPush( vCis, pObj );
+        vCos = Vec_PtrAlloc( Aig_ManPoNum(p) );
+        Aig_ManForEachPo( p, pObj, i )
+            if ( Aig_ObjIsTravIdCurrent(p, pObj) )
+                Vec_PtrPush( vCos, pObj );
+            else
+                Aig_ObjDisconnect( p, pObj );
+        // remember the number of true PIs/POs
+        nTruePis = Aig_ManPiNum(p) - Aig_ManRegNum(p);
+        nTruePos = Aig_ManPoNum(p) - Aig_ManRegNum(p);
+        // set the new number of registers
+        p->nRegs -= Aig_ManPoNum(p) - Vec_PtrSize(vNodes);
+        // create new PIs/POs
+        assert( Vec_PtrSize(vCis) == nTruePis + p->nRegs );
+        assert( Vec_PtrSize(vCos) == nTruePos + p->nRegs );
+        Vec_PtrFree( p->vPis );    p->vPis = vCis;
+        Vec_PtrFree( p->vPos );    p->vPos = vCos;
+        p->nObjs[AIG_OBJ_PI] = Vec_PtrSize( p->vPis );
+        p->nObjs[AIG_OBJ_PO] = Vec_PtrSize( p->vPos );
+    }
+    Vec_PtrFree( vNodes );
+    // remove dangling nodes
+    return Aig_ManCleanup( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the number of dangling nodes removed.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Aig_ManCleanup( Aig_Man_t * p )
 {
     Vec_Ptr_t * vObjs;
@@ -277,6 +429,42 @@ int Aig_ManCleanup( Aig_Man_t * p )
 
 /**Function*************************************************************
 
+  Synopsis    [Returns the number of dangling nodes removed.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Aig_ManCountMergeRegs( Aig_Man_t * p )
+{
+    Aig_Obj_t * pObj, * pFanin;
+    int i, Counter = 0, Const0 = 0, Const1 = 0;
+    Aig_ManIncrementTravId( p );
+    Aig_ManForEachLiSeq( p, pObj, i )
+    {
+        pFanin = Aig_ObjFanin0(pObj);
+        if ( Aig_ObjIsConst1(pFanin) )
+        {
+            if ( Aig_ObjFaninC0(pObj) )
+                Const0++;
+            else
+                Const1++;
+        }
+        if ( Aig_ObjIsTravIdCurrent(p, pFanin) )
+            continue;
+        Aig_ObjSetTravIdCurrent(p, pFanin);
+        Counter++;
+    }
+    printf( "Regs = %d. Fanins = %d. Const0 = %d. Const1 = %d.\n", 
+        Aig_ManRegNum(p), Counter, Const0, Const1 );
+    return 0;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Stops the AIG manager.]
 
   Description []
@@ -302,6 +490,148 @@ void Aig_ManPrintStats( Aig_Man_t * p )
     printf( "\n" );
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Checks how many latches can be reduced.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Aig_ManReduceLachesCount( Aig_Man_t * p )
+{
+    Aig_Obj_t * pObj, * pFanin;
+    int i, Counter = 0;
+    assert( Aig_ManRegNum(p) > 0 );
+    Aig_ManForEachObj( p, pObj, i )
+        assert( !pObj->fMarkA && !pObj->fMarkB );
+    Aig_ManForEachLiSeq( p, pObj, i )
+    {
+        pFanin = Aig_ObjFanin0(pObj);
+        if ( Aig_ObjFaninC0(pObj) )
+        {
+            if ( pFanin->fMarkB )
+                Counter++;
+            else
+                pFanin->fMarkB = 1;
+        }
+        else
+        {
+            if ( pFanin->fMarkA )
+                Counter++;
+            else
+                pFanin->fMarkA = 1;
+        }
+    }
+    Aig_ManForEachLiSeq( p, pObj, i )
+    {
+        pFanin = Aig_ObjFanin0(pObj);
+        pFanin->fMarkA = pFanin->fMarkB = 0;
+    }
+    return Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Reduces the latches.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Aig_ManReduceLachesOnce( Aig_Man_t * p )
+{
+    Vec_Ptr_t * vMap;
+    Aig_Obj_t * pObj, * pObjLi, * pObjLo, * pFanin;
+    int * pMapping, i;
+    // start mapping by adding the true PIs
+    vMap = Vec_PtrAlloc( Aig_ManPiNum(p) );
+    Aig_ManForEachPiSeq( p, pObj, i )
+        Vec_PtrPush( vMap, pObj );
+    // create mapping of fanin nodes into the corresponding latch outputs
+    pMapping = ALLOC( int, 2 * (Aig_ManObjIdMax(p) + 1) );
+    Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i )
+    {
+        pFanin = Aig_ObjFanin0(pObjLi);
+        if ( Aig_ObjFaninC0(pObjLi) )
+        {
+            if ( pFanin->fMarkB )
+            {
+                Vec_PtrPush( vMap, Aig_ManLo(p, pMapping[2*pFanin->Id + 1]) );
+            }
+            else
+            {
+                pFanin->fMarkB = 1;
+                pMapping[2*pFanin->Id + 1] = i;
+                Vec_PtrPush( vMap, pObjLo );
+            }
+        }
+        else
+        {
+            if ( pFanin->fMarkA )
+            {
+                Vec_PtrPush( vMap, Aig_ManLo(p, pMapping[2*pFanin->Id]) );
+            }
+            else
+            {
+                pFanin->fMarkA = 1;
+                pMapping[2*pFanin->Id] = i;
+                Vec_PtrPush( vMap, pObjLo );
+            }
+        }
+    }
+    free( pMapping );
+    Aig_ManForEachLiSeq( p, pObj, i )
+    {
+        pFanin = Aig_ObjFanin0(pObj);
+        pFanin->fMarkA = pFanin->fMarkB = 0;
+    }
+    return vMap;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Reduces the latches.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Aig_ManReduceLaches( Aig_Man_t * p, int fVerbose )
+{
+    Aig_Man_t * pTemp;
+    Vec_Ptr_t * vMap;
+    int nSaved, nCur;
+    for ( nSaved = 0; nCur = Aig_ManReduceLachesCount(p); nSaved += nCur )
+    {
+        if ( fVerbose )
+        {
+        printf( "Saved = %5d.   ", nCur );
+        printf( "RBeg = %5d. NBeg = %6d.   ", Aig_ManRegNum(p), Aig_ManNodeNum(p) );
+        }
+        vMap = Aig_ManReduceLachesOnce( p );
+        p = Aig_ManRemap( pTemp = p, vMap );
+        Aig_ManStop( pTemp );
+        Vec_PtrFree( vMap );
+        Aig_ManSeqCleanup( p );
+        if ( fVerbose )
+        {
+        printf( "REnd = %5d. NEnd = %6d.   ", Aig_ManRegNum(p), Aig_ManNodeNum(p) );
+        printf( "\n" );
+        }
+    }
+    return p;
+}
+
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
diff --git a/src/aig/aig/aigOper.c b/src/aig/aig/aigOper.c
index d13d4bed..68216ee0 100644
--- a/src/aig/aig/aigOper.c
+++ b/src/aig/aig/aigOper.c
@@ -148,6 +148,89 @@ Aig_Obj_t * Aig_And( Aig_Man_t * p, Aig_Obj_t * p0, Aig_Obj_t * p1 )
         return p0 == p->pConst1 ? p1 : Aig_Not(p->pConst1);
     if ( Aig_Regular(p1) == p->pConst1 )
         return p1 == p->pConst1 ? p0 : Aig_Not(p->pConst1);
+    // check not so trivial cases
+    if ( p->fAddStrash && (Aig_ObjIsNode(Aig_Regular(p0)) || Aig_ObjIsNode(Aig_Regular(p1))) )
+    { // http://fmv.jku.at/papers/BrummayerBiere-MEMICS06.pdf
+        Aig_Obj_t * pFanA, * pFanB, * pFanC, * pFanD;
+        pFanA = Aig_ObjChild0(Aig_Regular(p0));
+        pFanB = Aig_ObjChild1(Aig_Regular(p0));
+        pFanC = Aig_ObjChild0(Aig_Regular(p1));
+        pFanD = Aig_ObjChild1(Aig_Regular(p1));
+        if ( Aig_IsComplement(p0) )
+        {
+            if ( pFanA == Aig_Not(p1) || pFanB == Aig_Not(p1) )
+                return p1;
+            if ( pFanB == p1 )
+                return Aig_And( p, Aig_Not(pFanA), pFanB );
+            if ( pFanA == p1 )
+                return Aig_And( p, Aig_Not(pFanB), pFanA );
+        }
+        else
+        {
+            if ( pFanA == Aig_Not(p1) || pFanB == Aig_Not(p1) )
+                return Aig_Not(p->pConst1);
+            if ( pFanA == p1 || pFanB == p1 )
+                return p0;
+        }
+        if ( Aig_IsComplement(p1) )
+        {
+            if ( pFanC == Aig_Not(p0) || pFanD == Aig_Not(p0) )
+                return p0;
+            if ( pFanD == p0 )
+                return Aig_And( p, Aig_Not(pFanC), pFanD );
+            if ( pFanC == p0 )
+                return Aig_And( p, Aig_Not(pFanD), pFanC );
+        }
+        else
+        {
+            if ( pFanC == Aig_Not(p0) || pFanD == Aig_Not(p0) )
+                return Aig_Not(p->pConst1);
+            if ( pFanC == p0 || pFanD == p0 )
+                return p1;
+        }
+        if ( !Aig_IsComplement(p0) && !Aig_IsComplement(p1) ) 
+        {
+            if ( pFanA == Aig_Not(pFanC) || pFanA == Aig_Not(pFanD) || pFanB == Aig_Not(pFanC) || pFanB == Aig_Not(pFanD) )
+                return Aig_Not(p->pConst1);
+            if ( pFanA == pFanC || pFanB == pFanC )
+                return Aig_And( p, p0, pFanD );
+            if ( pFanB == pFanC || pFanB == pFanD )
+                return Aig_And( p, pFanA, p1 );
+            if ( pFanA == pFanD || pFanB == pFanD )
+                return Aig_And( p, p0, pFanC );
+            if ( pFanA == pFanC || pFanA == pFanD )
+                return Aig_And( p, pFanB, p1 );
+        }
+        else if ( Aig_IsComplement(p0) && !Aig_IsComplement(p1) )
+        {
+            if ( pFanA == Aig_Not(pFanC) || pFanA == Aig_Not(pFanD) || pFanB == Aig_Not(pFanC) || pFanB == Aig_Not(pFanD) )
+                return p1;
+            if ( pFanB == pFanC || pFanB == pFanD )
+                return Aig_And( p, Aig_Not(pFanA), p1 );
+            if ( pFanA == pFanC || pFanA == pFanD )
+                return Aig_And( p, Aig_Not(pFanB), p1 );
+        }
+        else if ( !Aig_IsComplement(p0) && Aig_IsComplement(p1) )
+        {
+            if ( pFanC == Aig_Not(pFanA) || pFanC == Aig_Not(pFanB) || pFanD == Aig_Not(pFanA) || pFanD == Aig_Not(pFanB) )
+                return p0;
+            if ( pFanD == pFanA || pFanD == pFanB )
+                return Aig_And( p, Aig_Not(pFanC), p0 );
+            if ( pFanC == pFanA || pFanC == pFanB )
+                return Aig_And( p, Aig_Not(pFanD), p0 );
+        }
+        else // if ( Aig_IsComplement(p0) && Aig_IsComplement(p1) )
+        {
+            if ( pFanA == pFanD && pFanB == Aig_Not(pFanC) )
+                return Aig_Not(pFanA);
+            if ( pFanB == pFanC && pFanA == Aig_Not(pFanD) )
+                return Aig_Not(pFanB);
+            if ( pFanA == pFanC && pFanB == Aig_Not(pFanD) )
+                return Aig_Not(pFanA);
+            if ( pFanB == pFanD && pFanA == Aig_Not(pFanC) )
+                return Aig_Not(pFanB);
+        }
+    }
     // check if it can be an EXOR gate
 //    if ( Aig_ObjIsExorType( p0, p1, &pFan0, &pFan1 ) )
 //        return Aig_Exor( p, pFan0, pFan1 );
diff --git a/src/aig/aig/aigRet.c b/src/aig/aig/aigRet.c
new file mode 100644
index 00000000..eacf756b
--- /dev/null
+++ b/src/aig/aig/aigRet.c
@@ -0,0 +1,552 @@
+/**CFile****************************************************************
+
+  FileName    [aigRet.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [AIG package.]
+
+  Synopsis    [Retiming of AIGs.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - April 28, 2007.]
+
+  Revision    [$Id: aigRet.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "aig.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+// init values
+typedef enum { 
+    RTM_VAL_NONE,                    // 0: non-existent value
+    RTM_VAL_ZERO,                    // 1: initial value 0
+    RTM_VAL_ONE,                     // 2: initial value 1
+    RTM_VAL_VOID                     // 3: unused value
+} Rtm_Init_t;
+
+typedef struct Rtm_Man_t_    Rtm_Man_t;
+struct Rtm_Man_t_
+{
+    // network representation
+    Vec_Ptr_t *      vObjs;          // retiming objects
+    Vec_Ptr_t *      vPis;           // PIs only
+    Vec_Ptr_t *      vPos;           // POs only
+    Aig_MmFlex_t *   pMem;           // the memory manager
+    // storage for overflow latches
+    unsigned *       pExtra;       
+    unsigned *       pExtraFree;
+};
+
+typedef struct Rtm_Edg_t_    Rtm_Edg_t;
+struct Rtm_Edg_t_
+{
+    unsigned long    nLats   :  12;  // the number of latches
+    unsigned long    LData   :  20;  // the latches themselves
+};
+
+typedef struct Rtm_Obj_t_    Rtm_Obj_t;
+struct Rtm_Obj_t_
+{
+    void *           pCopy;          // the copy of this object
+    unsigned long    Type    :  3;   // object type
+    unsigned long    fMark   :  1;   // multipurpose mark
+    unsigned long    fCompl0 :  1;   // complemented attribute of the first edge
+    unsigned long    fCompl1 :  1;   // complemented attribute of the second edge
+    unsigned long    nFanins :  8;   // the number of fanins
+    unsigned         Num     : 18;   // the retiming number of this node
+    int              Id;             // ID of this object
+    int              Temp;           // temporary usage
+    int              nFanouts;       // the number of fanouts
+    void *           pFanio[0];      // fanins and their edges (followed by fanouts and pointers to their edges)
+};
+
+static Rtm_Init_t  Rtm_InitNot( Rtm_Init_t Val )                 { if ( Val == RTM_VAL_ZERO ) return RTM_VAL_ONE; if ( Val == RTM_VAL_ONE ) return RTM_VAL_ZERO; assert( 0 ); return -1; }
+static Rtm_Init_t  Rtm_InitNotCond( Rtm_Init_t Val, int c )      { return c ? Rtm_InitNot(Val) : Val;                         }
+static Rtm_Init_t  Rtm_InitAnd(Rtm_Init_t ValA, Rtm_Init_t ValB) { if ( ValA == RTM_VAL_ONE && ValB == RTM_VAL_ONE ) return RTM_VAL_ONE;  if ( ValA == RTM_VAL_ZERO || ValB == RTM_VAL_ZERO ) return RTM_VAL_ZERO; assert( 0 ); return -1;   }
+
+static Rtm_Obj_t * Rtm_ObjFanin( Rtm_Obj_t * pObj, int i )       { return (Rtm_Obj_t *)pObj->pFanio[2*i];                     }
+static Rtm_Obj_t * Rtm_ObjFanout( Rtm_Obj_t * pObj, int i )      { return (Rtm_Obj_t *)pObj->pFanio[2*(pObj->nFanins+i)];     }
+static Rtm_Edg_t * Rtm_ObjEdge( Rtm_Obj_t * pObj, int i )        { return (Rtm_Edg_t *)(pObj->pFanio + 2*i + 1);              }
+static Rtm_Edg_t * Rtm_ObjFanoutEdge( Rtm_Obj_t * pObj, int i )  { return (Rtm_Edg_t *)pObj->pFanio[2*(pObj->nFanins+i) + 1]; }
+
+static Rtm_Init_t  Rtm_ObjGetFirst( Rtm_Edg_t * pEdge )          { return pEdge->LData & 3;                                    }
+static Rtm_Init_t  Rtm_ObjGetLast( Rtm_Edg_t * pEdge )           { return (pEdge->LData >> (2 *(pEdge->nLats-1))) & 3;         }
+static Rtm_Init_t  Rtm_ObjGetOne( Rtm_Edg_t * pEdge, int i )     { assert( i < (int)pEdge->nLats ); return (pEdge->LData >> (2 * i)) & 3;  }
+static Rtm_Init_t  Rtm_ObjRemFirst( Rtm_Edg_t * pEdge )          { int Val = pEdge->LData & 3; pEdge->LData >>= 2; assert(pEdge->nLats > 0); pEdge->nLats--; return Val;  }
+static Rtm_Init_t  Rtm_ObjRemLast( Rtm_Edg_t * pEdge )           { int Val = (pEdge->LData >> (2 *(pEdge->nLats-1))) & 3; pEdge->LData ^= Val << (2 *(pEdge->nLats-1)); assert(pEdge->nLats > 0); pEdge->nLats--; return Val;  }
+static void        Rtm_ObjAddFirst( Rtm_Edg_t * pEdge, Rtm_Init_t Lat ) { assert( Lat < 4 ); pEdge->LData = (pEdge->LData << 2) | Lat;  pEdge->nLats++;   }
+static void        Rtm_ObjAddLast( Rtm_Edg_t * pEdge, Rtm_Init_t Lat )  { assert( Lat < 4 ); pEdge->LData |= Lat << (2*pEdge->nLats);  pEdge->nLats++;   }
+
+// iterator over the primary inputs
+#define Rtm_ManForEachPi( p, pObj, i )                                          \
+    Vec_PtrForEachEntry( p->vPis, pObj, i )
+// iterator over the primary outputs
+#define Rtm_ManForEachPo( p, pObj, i )                                          \
+    Vec_PtrForEachEntry( p->vPos, pObj, i )
+// iterator over all objects, including those currently not used
+#define Rtm_ManForEachObj( p, pObj, i )                                         \
+    Vec_PtrForEachEntry( p->vObjs, pObj, i ) 
+// iterate through the fanins
+#define Rtm_ObjForEachFanin( pObj, pFanin, i )                                  \
+    for ( i = 0; i < (int)(pObj)->nFanins && ((pFanin = Rtm_ObjFanin(pObj, i)), 1); i++ )
+// iterate through the fanouts
+#define Rtm_ObjForEachFanout( pObj, pFanout, i )                                \
+    for ( i = 0; i < (int)(pObj)->nFanouts && ((pFanout = Rtm_ObjFanout(pObj, i)), 1); i++ )
+// iterate through the fanin edges
+#define Rtm_ObjForEachFaninEdge( pObj, pEdge, i )                               \
+    for ( i = 0; i < (int)(pObj)->nFanins && ((pEdge = Rtm_ObjEdge(pObj, i)), 1); i++ )
+// iterate through the fanout edges
+#define Rtm_ObjForEachFanoutEdge( pObj, pEdge, i )                              \
+    for ( i = 0; i < (int)(pObj)->nFanouts && ((pEdge = Rtm_ObjFanoutEdge(pObj, i)), 1); i++ )
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Allocates the retiming manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Rtm_Man_t * Rtm_ManAlloc( Aig_Man_t * p )
+{
+    Rtm_Man_t * pRtm;
+    // start the manager
+    pRtm = ALLOC( Rtm_Man_t, 1 );
+    memset( pRtm, 0, sizeof(Rtm_Man_t) );
+    // perform initializations
+    pRtm->vObjs = Vec_PtrAlloc( Aig_ManObjNum(p) );
+    pRtm->vPis  = Vec_PtrAlloc( Aig_ManPiNum(p) );
+    pRtm->vPos  = Vec_PtrAlloc( Aig_ManPoNum(p) );
+    pRtm->pMem  = Aig_MmFlexStart();
+    return pRtm;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Allocates the retiming manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Rtm_ManFree( Rtm_Man_t * p )
+{
+    Vec_PtrFree( p->vObjs );
+    Vec_PtrFree( p->vPis );
+    Vec_PtrFree( p->vPos );
+    Aig_MmFlexStop( p->pMem, 0 );
+    free( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Counts the maximum number of latches on an edge.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Rtm_ManLatchMax( Rtm_Man_t * p )
+{
+    Rtm_Obj_t * pObj;
+    Rtm_Edg_t * pEdge;
+    int nLatchMax = 0, i, k;
+    Rtm_ManForEachObj( p, pObj, i )
+    Rtm_ObjForEachFaninEdge( pObj, pEdge, k )
+        nLatchMax = AIG_MAX( nLatchMax, (int)pEdge->nLats );
+    return nLatchMax;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Allocates the retiming object.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Rtm_Obj_t * Rtm_ObjAlloc( Rtm_Man_t * pRtm, int nFanins, int nFanouts )
+{
+    Rtm_Obj_t * pObj;
+    int Size = sizeof(Rtm_Obj_t) + sizeof(Rtm_Obj_t *) * (nFanins + nFanouts) * 2;
+    pObj = (Rtm_Obj_t *)Aig_MmFlexEntryFetch( pRtm->pMem, Size );
+    memset( pObj, 0, sizeof(Rtm_Obj_t) );
+    pObj->Type = (int)(nFanins == 1 && nFanouts == 0); // mark PO
+    pObj->Num  = nFanins;  // temporary
+    pObj->Temp = nFanouts;
+    pObj->Id = Vec_PtrSize(pRtm->vObjs);
+    Vec_PtrPush( pRtm->vObjs, pObj );
+    return pObj;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Allocates the retiming object.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Rtm_ObjAddFanin( Rtm_Obj_t * pObj, Rtm_Obj_t * pFanin, int fCompl )
+{
+    pObj->pFanio[ 2*pObj->nFanins ] = pFanin;
+    pObj->pFanio[ 2*pObj->nFanins + 1 ] = NULL;
+    pFanin->pFanio[ 2*(pFanin->Num + pFanin->nFanouts) ] = pObj;
+    pFanin->pFanio[ 2*(pFanin->Num + pFanin->nFanouts) + 1 ] = pObj->pFanio + 2*pObj->nFanins + 1;
+    if ( pObj->nFanins == 0 )
+        pObj->fCompl0 = fCompl;
+    else if ( pObj->nFanins == 1 )
+        pObj->fCompl1 = fCompl;
+    else
+        assert( 0 );
+    pObj->nFanins++;
+    pFanin->nFanouts++;
+    assert( pObj->nFanins <= pObj->Num );
+    assert( pFanin->nFanouts <= pFanin->Temp );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Check the possibility of forward retiming.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Rtm_ObjCheckRetimeFwd( Rtm_Obj_t * pObj )
+{
+    Rtm_Edg_t * pEdge;
+    int i;
+    Rtm_ObjForEachFaninEdge( pObj, pEdge, i )
+        if ( pEdge->nLats == 0 )
+            return 0;
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Check the possibility of forward retiming.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Rtm_ObjGetDegreeFwd( Rtm_Obj_t * pObj )
+{
+    Rtm_Obj_t * pFanin;
+    int i, Degree = 0;
+    Rtm_ObjForEachFanin( pObj, pFanin, i )
+        Degree = AIG_MAX( Degree, (int)pFanin->Num );
+    return Degree + 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs forward retiming.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Rtm_ObjRetimeFwd( Rtm_Obj_t * pObj )
+{
+    Rtm_Init_t ValTotal, ValCur;
+    Rtm_Edg_t * pEdge;
+    int i;
+    assert( Rtm_ObjCheckRetimeFwd(pObj) );
+    // extract values and compute the result
+    ValTotal = RTM_VAL_ONE;
+    Rtm_ObjForEachFaninEdge( pObj, pEdge, i )
+    {
+        ValCur = Rtm_ObjRemFirst( pEdge );
+        ValCur = Rtm_InitNotCond( ValCur, i? pObj->fCompl1 : pObj->fCompl0 );
+        ValTotal = Rtm_InitAnd( ValTotal, ValCur );
+    }
+    // insert the result in the fanout values
+    Rtm_ObjForEachFanoutEdge( pObj, pEdge, i )
+    {
+        if ( pEdge->nLats >= 10 )
+            printf( "Rtm_ObjRetimeFwd(); More than 10 latches on the edge!\n" );
+        Rtm_ObjAddLast( pEdge, ValTotal );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derive retiming manager from the given AIG manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Rtm_Man_t * Rtm_ManFromAig( Aig_Man_t * p )
+{
+    Rtm_Man_t * pRtm;
+    Aig_Obj_t * pObj, * pObjLi, * pObjLo;
+    int i;
+    assert( Aig_ManRegNum(p) > 0 );
+    assert( Aig_ManBufNum(p) == 0 );
+    // allocate the manager
+    pRtm = Rtm_ManAlloc( p );
+    // allocate objects
+    pObj = Aig_ManConst1(p);
+    pObj->pData = Rtm_ObjAlloc( pRtm, 0, pObj->nRefs );
+    Aig_ManForEachPiSeq( p, pObj, i )
+    {
+        pObj->pData = Rtm_ObjAlloc( pRtm, 0, pObj->nRefs );
+        Vec_PtrPush( pRtm->vPis, pObj->pData );
+    }
+    Aig_ManForEachPoSeq( p, pObj, i )
+    {
+        pObj->pData = Rtm_ObjAlloc( pRtm, 1, 0 );
+        Vec_PtrPush( pRtm->vPos, pObj->pData );
+    }
+    Aig_ManForEachLoSeq( p, pObj, i )
+        pObj->pData = Rtm_ObjAlloc( pRtm, 1, pObj->nRefs );
+    Aig_ManForEachLiSeq( p, pObj, i )
+        pObj->pData = Rtm_ObjAlloc( pRtm, 1, 1 );
+    Aig_ManForEachNode( p, pObj, i )
+        pObj->pData = Rtm_ObjAlloc( pRtm, 2, pObj->nRefs );
+    // connect objects
+    Aig_ManForEachPoSeq( p, pObj, i )
+        Rtm_ObjAddFanin( pObj->pData, Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj) );
+    Aig_ManForEachLiSeq( p, pObj, i )
+        Rtm_ObjAddFanin( pObj->pData, Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj) );
+    Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i )
+        Rtm_ObjAddFanin( pObjLo->pData, pObjLi->pData, 0 );
+    Aig_ManForEachNode( p, pObj, i )
+    {
+        Rtm_ObjAddFanin( pObj->pData, Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj) );
+        Rtm_ObjAddFanin( pObj->pData, Aig_ObjFanin1(pObj)->pData, Aig_ObjFaninC1(pObj) );
+    }
+    // set registers
+    Aig_ManForEachLoSeq( p, pObj, i )
+        Rtm_ObjAddFirst( Rtm_ObjEdge(pObj->pData, 0), RTM_VAL_ZERO );
+    return pRtm;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derive AIG manager after retiming.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Obj_t * Rtm_ManToAig_rec( Aig_Man_t * pNew, Rtm_Obj_t * pObjRtm, int * pLatches )
+{
+    Rtm_Edg_t * pEdge;
+    Aig_Obj_t * pRes, * pFanin;
+    int k, Val;
+    if ( pObjRtm->pCopy )
+        return pObjRtm->pCopy;
+    // get the inputs
+    pRes = Aig_ManConst1( pNew );
+    Rtm_ObjForEachFaninEdge( pObjRtm, pEdge, k )
+    {
+        if ( pEdge->nLats == 0 )
+            pFanin = Rtm_ManToAig_rec( pNew, Rtm_ObjFanin(pObjRtm, k), pLatches );
+        else
+        {
+            Val = Rtm_ObjGetFirst( pEdge );
+            pFanin = Aig_ManPi( pNew, pLatches[2*pObjRtm->Id + k] + pEdge->nLats - 1 );
+            pFanin = Aig_NotCond( pFanin, Val == RTM_VAL_ONE );
+        }
+        pFanin = Aig_NotCond( pFanin, k ? pObjRtm->fCompl1 : pObjRtm->fCompl0 );
+        pRes = Aig_And( pNew, pRes, pFanin );
+    }
+    return pObjRtm->pCopy = pRes;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derive AIG manager after retiming.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Rtm_ManToAig( Rtm_Man_t * pRtm )
+{
+    Aig_Man_t * pNew;
+    Aig_Obj_t * pObjNew;
+    Rtm_Obj_t * pObjRtm;
+    Rtm_Edg_t * pEdge;
+    int i, k, m, Val, nLatches, * pLatches;
+    // count latches and mark the first latch on each edge
+    pLatches = ALLOC( int, 2 * Vec_PtrSize(pRtm->vObjs) );
+    nLatches = 0;
+    Rtm_ManForEachObj( pRtm, pObjRtm, i )
+    Rtm_ObjForEachFaninEdge( pObjRtm, pEdge, k )
+    {
+        pLatches[2*pObjRtm->Id + k] = Vec_PtrSize(pRtm->vPis) + nLatches;
+        nLatches += pEdge->nLats;
+    }
+    // create the new manager
+    pNew = Aig_ManStart( Vec_PtrSize(pRtm->vObjs) + nLatches );
+    // create PIs/POs and latches
+    pObjRtm = Vec_PtrEntry( pRtm->vObjs, 0 );
+    pObjRtm->pCopy = Aig_ManConst1(pNew);
+    Rtm_ManForEachPi( pRtm, pObjRtm, i )
+        pObjRtm->pCopy = Aig_ObjCreatePi(pNew);
+    for ( i = 0; i < nLatches; i++ )
+        Aig_ObjCreatePi(pNew);
+    // create internal nodes
+    Rtm_ManForEachObj( pRtm, pObjRtm, i )
+        Rtm_ManToAig_rec( pNew, pObjRtm, pLatches );
+    // create POs
+    Rtm_ManForEachPo( pRtm, pObjRtm, i )
+        Aig_ObjCreatePo( pNew, pObjRtm->pCopy );
+    // connect latches 
+    Rtm_ManForEachObj( pRtm, pObjRtm, i )
+    Rtm_ObjForEachFaninEdge( pObjRtm, pEdge, k )
+    {
+        if ( pEdge->nLats == 0 )
+            continue;
+        pObjNew = Rtm_ObjFanin( pObjRtm, k )->pCopy;
+        for ( m = 0; m < (int)pEdge->nLats; m++ )
+        {
+            Val = Rtm_ObjGetOne( pEdge, pEdge->nLats - 1 - m );
+            pObjNew = Aig_NotCond( pObjNew, Val == RTM_VAL_ONE );
+            Aig_ObjCreatePo( pNew, pObjNew );
+            pObjNew = Aig_ManPi( pNew, pLatches[2*pObjRtm->Id + k] + m );
+            pObjNew = Aig_NotCond( pObjNew, Val == RTM_VAL_ONE );
+        }
+        assert( Aig_Regular(pObjNew)->nRefs > 0 );
+    }
+    free( pLatches );
+    pNew->nRegs = nLatches;
+    // remove useless nodes
+    Aig_ManCleanup( pNew );
+    if ( !Aig_ManCheck( pNew ) )
+        printf( "Rtm_ManToAig: The network check has failed.\n" );
+    return pNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs forward retiming with the given limit on depth.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Rtm_ManRetimeFwd( Aig_Man_t * p, int nStepsMax, int fVerbose )
+{
+    Vec_Ptr_t * vQueue;
+    Aig_Man_t * pNew;
+    Rtm_Man_t * pRtm;
+    Rtm_Obj_t * pObj, * pFanout;
+    Aig_Obj_t * pObjAig;
+    int i, k, Degree, DegreeMax = 0; 
+    // create the retiming manager
+    pRtm = Rtm_ManFromAig( p );
+    // set the current retiming number
+    Rtm_ManForEachObj( pRtm, pObj, i )
+    {
+        assert( pObj->nFanins == pObj->Num );
+        assert( pObj->nFanouts == pObj->Temp );
+        pObj->Num = 0;
+    }
+
+    // put the LOs on the queue
+    vQueue = Vec_PtrAlloc( 1000 );
+    Aig_ManForEachLoSeq( p, pObjAig, i )
+    {
+        pObj = pObjAig->pData;
+        pObj->fMark = 1;
+        Vec_PtrPush( vQueue, pObj );
+    }
+    // perform retiming 
+    DegreeMax = 0;
+    Vec_PtrForEachEntry( vQueue, pObj, i )
+    {
+        pObj->fMark = 0;
+        // retime the node 
+        Rtm_ObjRetimeFwd( pObj );
+        // check if its fanouts should be retimed
+        Rtm_ObjForEachFanout( pObj, pFanout, k )
+        {
+            if ( pFanout->fMark ) // skip aleady scheduled
+                continue;
+            if ( pFanout->Type ) // skip POs
+                continue;
+            if ( !Rtm_ObjCheckRetimeFwd( pFanout ) ) // skip non-retimable
+                continue;
+            Degree = Rtm_ObjGetDegreeFwd( pFanout );
+            DegreeMax = AIG_MAX( DegreeMax, Degree );
+            if ( Degree > nStepsMax ) // skip nodes with high degree
+                continue;
+            pFanout->fMark = 1;
+            pFanout->Num = Degree;
+            Vec_PtrPush( vQueue, pFanout );
+        }
+    }
+
+    if ( fVerbose )
+        printf( "Performed %d fwd latch moves of max depth %d and max latch count %d.\n", 
+            Vec_PtrSize(vQueue), DegreeMax, Rtm_ManLatchMax(pRtm) );
+    Vec_PtrFree( vQueue );
+
+    // get the new manager
+    pNew = Rtm_ManToAig( pRtm );
+    Rtm_ManFree( pRtm );
+    // group the registers
+    pNew = Aig_ManReduceLaches( pNew, fVerbose );
+    return pNew;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/aig/aigSeq.c b/src/aig/aig/aigSeq.c
index 19466996..5bd5aaa5 100644
--- a/src/aig/aig/aigSeq.c
+++ b/src/aig/aig/aigSeq.c
@@ -24,6 +24,70 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
+#define AIG_XVS0   1
+#define AIG_XVS1   2
+#define AIG_XVSX   3
+
+static inline void Aig_ObjSetXsim( Aig_Obj_t * pObj, int Value )  { pObj->nCuts = Value;  }
+static inline int  Aig_ObjGetXsim( Aig_Obj_t * pObj )             { return pObj->nCuts;   }
+static inline int  Aig_XsimInv( int Value )   
+{ 
+    if ( Value == AIG_XVS0 )
+        return AIG_XVS1;
+    if ( Value == AIG_XVS1 )
+        return AIG_XVS0;
+    assert( Value == AIG_XVSX );       
+    return AIG_XVSX;
+}
+static inline int  Aig_XsimAnd( int Value0, int Value1 )   
+{ 
+    if ( Value0 == AIG_XVS0 || Value1 == AIG_XVS0 )
+        return AIG_XVS0;
+    if ( Value0 == AIG_XVSX || Value1 == AIG_XVSX )
+        return AIG_XVSX;
+    assert( Value0 == AIG_XVS1 && Value1 == AIG_XVS1 );
+    return AIG_XVS1;
+}
+static inline int  Aig_XsimRand2()   
+{
+    return (rand() & 1) ? AIG_XVS1 : AIG_XVS0;
+}
+static inline int  Aig_XsimRand3()   
+{
+    int RetValue;
+    do { 
+        RetValue = rand() & 3; 
+    } while ( RetValue == 0 );
+    return RetValue;
+}
+static inline int  Aig_ObjGetXsimFanin0( Aig_Obj_t * pObj )       
+{ 
+    int RetValue;
+    RetValue = Aig_ObjGetXsim(Aig_ObjFanin0(pObj));
+    return Aig_ObjFaninC0(pObj)? Aig_XsimInv(RetValue) : RetValue;
+}
+static inline int  Aig_ObjGetXsimFanin1( Aig_Obj_t * pObj )       
+{ 
+    int RetValue;
+    RetValue = Aig_ObjGetXsim(Aig_ObjFanin1(pObj));
+    return Aig_ObjFaninC1(pObj)? Aig_XsimInv(RetValue) : RetValue;
+}
+static inline void Aig_XsimPrint( FILE * pFile, int Value )   
+{ 
+    if ( Value == AIG_XVS0 )
+    {
+        fprintf( pFile, "0" );
+        return;
+    }
+    if ( Value == AIG_XVS1 )
+    {
+        fprintf( pFile, "1" );
+        return;
+    }
+    assert( Value == AIG_XVSX );       
+    fprintf( pFile, "x" );
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
@@ -493,6 +557,163 @@ int Aig_ManSeqStrash( Aig_Man_t * p, int nLatches, int * pInits )
 
 }
 
+
+
+/**Function*************************************************************
+
+  Synopsis    [Cycles the circuit to create a new initial state.]
+
+  Description [Simulates the circuit with random input for the given 
+  number of timeframes to get a better initial state.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Aig_ManTernarySimulate( Aig_Man_t * p, int fVerbose )
+{
+    int nRounds = 1000; // limit on the number of ternary simulation rounds
+    Vec_Ptr_t * vMap;
+    Vec_Ptr_t * vStates;
+    Aig_Obj_t * pObj, * pObjLi, * pObjLo;
+    unsigned * pState, * pPrev;
+    int i, k, f, fConstants, Value, nWords, nCounter;
+    // allocate storage for states
+    nWords  = Aig_BitWordNum( 2*Aig_ManRegNum(p) );
+    vStates = Vec_PtrAllocSimInfo( nRounds, nWords );
+    // initialize the values
+    Aig_ObjSetXsim( Aig_ManConst1(p), AIG_XVS1 );
+    Aig_ManForEachPiSeq( p, pObj, i )
+        Aig_ObjSetXsim( pObj, AIG_XVSX );
+    Aig_ManForEachLoSeq( p, pObj, i )
+        Aig_ObjSetXsim( pObj, AIG_XVS0 );
+    // simulate for the given number of timeframes
+    for ( f = 0; f < nRounds; f++ )
+    {
+        // collect this state
+        pState = Vec_PtrEntry( vStates, f );
+        memset( pState, 0, sizeof(unsigned) * nWords );
+        Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i )
+        {
+            Value = Aig_ObjGetXsim(pObjLo);
+            if ( Value & 1 )
+                Aig_InfoSetBit( pState, 2 * i );
+            if ( Value & 2 )
+                Aig_InfoSetBit( pState, 2 * i + 1 );
+//            Aig_XsimPrint( stdout, Value );
+        }
+//        printf( "\n" );
+        // check if this state exists
+        for ( i = f - 1; i >= 0; i-- )
+        {
+            pPrev = Vec_PtrEntry( vStates, i );
+            if ( !memcmp( pPrev, pState, sizeof(unsigned) * nWords ) )
+                break;
+        }
+        if ( i >= 0 )
+            break;
+        // simulate internal nodes
+        Aig_ManForEachNode( p, pObj, i )
+            Aig_ObjSetXsim( pObj, Aig_XsimAnd(Aig_ObjGetXsimFanin0(pObj), Aig_ObjGetXsimFanin1(pObj)) );
+        // transfer the latch values
+        Aig_ManForEachLiSeq( p, pObj, i )
+            Aig_ObjSetXsim( pObj, Aig_ObjGetXsimFanin0(pObj) );
+        Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i )
+            Aig_ObjSetXsim( pObjLo, Aig_ObjGetXsim(pObjLi) );
+    }
+    if ( f == nRounds )
+    {
+        printf( "Aig_ManTernarySimulate(): Did not reach a fixed point.\n" );
+        Vec_PtrFree( vStates );
+        return NULL;
+    }
+    // OR all the states
+    pState = Vec_PtrEntry( vStates, 0 );
+    for ( i = 1; i <= f; i++ )
+    {
+        pPrev = Vec_PtrEntry( vStates, i );
+        for ( k = 0; k < nWords; k++ )
+            pState[k] |= pPrev[k];
+    }
+    // check if there are constants
+    fConstants = 0;
+    if ( 2*Aig_ManRegNum(p) == 32*nWords )
+    {
+        for ( i = 0; i < nWords; i++ )
+            if ( pState[i] != ~0 )
+                fConstants = 1;
+    }
+    else
+    {
+        for ( i = 0; i < nWords - 1; i++ )
+            if ( pState[i] != ~0 )
+                fConstants = 1;
+        if ( pState[i] != Aig_InfoMask( 2*Aig_ManRegNum(p) - 32*(nWords-1) ) )
+            fConstants = 1;
+    }
+    if ( fConstants == 0 )
+    {
+        Vec_PtrFree( vStates );
+        return NULL;
+    }
+
+    // start mapping by adding the true PIs
+    vMap = Vec_PtrAlloc( Aig_ManPiNum(p) );
+    Aig_ManForEachPiSeq( p, pObj, i )
+        Vec_PtrPush( vMap, pObj );
+    // find constant registers
+    nCounter = 0;
+    Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i )
+    {
+        Value = (Aig_InfoHasBit( pState, 2 * i + 1 ) << 1) | Aig_InfoHasBit( pState, 2 * i );
+        nCounter += (Value == 1 || Value == 2);
+        if ( Value == 1 )
+            Vec_PtrPush( vMap, Aig_ManConst0(p) );
+        else if ( Value == 2 )
+            Vec_PtrPush( vMap, Aig_ManConst1(p) );
+        else if ( Value == 3 )
+            Vec_PtrPush( vMap, pObjLo );
+        else
+            assert( 0 );
+//        Aig_XsimPrint( stdout, Value );
+    }
+//    printf( "\n" );
+    Vec_PtrFree( vStates );
+    if ( fVerbose )
+    printf( "Detected %d constants after %d iterations.\n", nCounter, f );
+    return vMap;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Reduces the circuit using ternary simulation.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Aig_ManConstReduce( Aig_Man_t * p, int fVerbose )
+{
+    Aig_Man_t * pTemp;
+    Vec_Ptr_t * vMap;
+    while ( vMap = Aig_ManTernarySimulate( p, fVerbose ) )
+    {
+        if ( fVerbose )
+        printf( "RBeg = %5d. NBeg = %6d.   ", Aig_ManRegNum(p), Aig_ManNodeNum(p) );
+        p = Aig_ManRemap( pTemp = p, vMap );
+        Aig_ManStop( pTemp );
+        Vec_PtrFree( vMap );
+        Aig_ManSeqCleanup( p );
+        if ( fVerbose )
+        printf( "REnd = %5d. NEnd = %6d.  \n", Aig_ManRegNum(p), Aig_ManNodeNum(p) );
+    }
+    return p;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/aig/module.make b/src/aig/aig/module.make
index d4737278..93b25e4a 100644
--- a/src/aig/aig/module.make
+++ b/src/aig/aig/module.make
@@ -13,5 +13,5 @@ SRC +=    src/aig/aig/aigCheck.c \
     src/aig/aig/aigTable.c \
     src/aig/aig/aigTiming.c \
     src/aig/aig/aigTruth.c \
-    src/aig/aig/aigUtil.c \ 
-    src/aig/aig/aigWin.c 
+    src/aig/aig/aigUtil.c \
+    src/aig/aig/aigWin.c
\ No newline at end of file
diff --git a/src/aig/bdc/bdcInt.h b/src/aig/bdc/bdcInt.h
index 65ab9d27..9649f870 100644
--- a/src/aig/bdc/bdcInt.h
+++ b/src/aig/bdc/bdcInt.h
@@ -76,7 +76,6 @@ struct Bdc_Isf_t_
     unsigned *       puOff;        // off-set
 };
 
-typedef struct Bdc_Man_t_ Bdc_Man_t;
 struct Bdc_Man_t_
 {
     // external parameters
diff --git a/src/aig/fra/fra.h b/src/aig/fra/fra.h
index 5d357290..1051aa30 100644
--- a/src/aig/fra/fra.h
+++ b/src/aig/fra/fra.h
@@ -71,6 +71,7 @@ struct Fra_Par_t_
     int              nBTLimitMiter;     // conflict limit at an output
     int              nFramesK;          // the number of timeframes to unroll
     int              fRewrite;          // use rewriting for constraint reduction
+    int              fLatchCorr;        // computes latch correspondence only
 };
 
 // FRAIG equivalence classes
@@ -101,6 +102,7 @@ struct Fra_Man_t_
     int              nFramesAll;        // the number of timeframes used
     Aig_Obj_t **     pMemFraig;         // memory allocated for points to the fraig nodes
     // simulation info
+    void *           pSim;              // the simulation manager
     unsigned *       pSimWords;         // memory for simulation information
     int              nSimWords;         // the number of simulation words
     // counter example storage
@@ -187,21 +189,23 @@ extern Fra_Cla_t *         Fra_ClassesStart( Aig_Man_t * pAig );
 extern void                Fra_ClassesStop( Fra_Cla_t * p );
 extern void                Fra_ClassesCopyReprs( Fra_Cla_t * p, Vec_Ptr_t * vFailed );
 extern void                Fra_ClassesPrint( Fra_Cla_t * p, int fVeryVerbose );
-extern void                Fra_ClassesPrepare( Fra_Cla_t * p );
+extern void                Fra_ClassesPrepare( Fra_Cla_t * p, int fLatchCorr );
 extern int                 Fra_ClassesRefine( Fra_Cla_t * p );
 extern int                 Fra_ClassesRefine1( Fra_Cla_t * p );
 extern int                 Fra_ClassesCountLits( Fra_Cla_t * p );
 extern int                 Fra_ClassesCountPairs( Fra_Cla_t * p );
 extern void                Fra_ClassesTest( Fra_Cla_t * p, int Id1, int Id2 );
+extern void                Fra_ClassesLatchCorr( 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_FraigPerform( Aig_Man_t * pManAig, Fra_Par_t * pPars );
 extern Aig_Man_t *         Fra_FraigChoice( Aig_Man_t * pManAig );
 extern void                Fra_FraigSweep( Fra_Man_t * pManAig );
+extern int                 Fra_FraigMiterStatus( Aig_Man_t * p );
 /*=== fraDfs.c ========================================================*/
 /*=== fraInd.c ========================================================*/
-extern Aig_Man_t *         Fra_FraigInduction( Aig_Man_t * p, int nFramesK, int fRewrite, int fVerbose );
+extern Aig_Man_t *         Fra_FraigInduction( Aig_Man_t * p, int nFramesK, int fRewrite, int fLatchCorr, int fVerbose, int * pnIter );
 /*=== fraMan.c ========================================================*/
 extern void                Fra_ParamsDefault( Fra_Par_t * pParams );
 extern void                Fra_ParamsDefaultSeq( Fra_Par_t * pParams );
@@ -214,6 +218,8 @@ extern void                Fra_ManPrint( Fra_Man_t * p );
 /*=== fraSat.c ========================================================*/
 extern int                 Fra_NodesAreEquiv( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew );
 extern int                 Fra_NodeIsConst( Fra_Man_t * p, Aig_Obj_t * pNew );
+/*=== fraSec.c ========================================================*/
+extern int                 Fra_FraigSec( Aig_Man_t * p, int nFrames, int fVerbose, int fVeryVerbose );
 /*=== fraSim.c ========================================================*/
 extern int                 Fra_NodeHasZeroSim( Aig_Obj_t * pObj );
 extern int                 Fra_NodeCompareSims( Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 );
diff --git a/src/aig/fra/fraCec.c b/src/aig/fra/fraCec.c
new file mode 100644
index 00000000..e705f4fc
--- /dev/null
+++ b/src/aig/fra/fraCec.c
@@ -0,0 +1,48 @@
+/**CFile****************************************************************
+
+  FileName    [fraCec.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [New FRAIG package.]
+
+  Synopsis    [CEC engined based on fraiging.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 30, 2007.]
+
+  Revision    [$Id: fraCec.c,v 1.00 2007/06/30 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "fra.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/fra/fraClass.c b/src/aig/fra/fraClass.c
index 31d6270a..8923c7b0 100644
--- a/src/aig/fra/fraClass.c
+++ b/src/aig/fra/fraClass.c
@@ -250,7 +250,7 @@ void Fra_ClassesPrint( Fra_Cla_t * p, int fVeryVerbose )
   SeeAlso     []
 
 ***********************************************************************/
-void Fra_ClassesPrepare( Fra_Cla_t * p )
+void Fra_ClassesPrepare( Fra_Cla_t * p, int fLatchCorr )
 {
     Aig_Obj_t ** ppTable, ** ppNexts;
     Aig_Obj_t * pObj, * pTemp;
@@ -266,8 +266,16 @@ void Fra_ClassesPrepare( Fra_Cla_t * p )
     Vec_PtrClear( p->vClasses1 );
     Aig_ManForEachObj( p->pAig, pObj, i )
     {
-        if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsPi(pObj) )
-            continue;
+        if ( fLatchCorr )
+        {
+            if ( !Aig_ObjIsPi(pObj) )
+                continue;
+        }
+        else
+        {
+            if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsPi(pObj) )
+                continue;
+        }
 //printf( "%3d : ", pObj->Id );
 //Extra_PrintBinary( stdout, Fra_ObjSim(pObj), 32 );
 //printf( "\n" );
@@ -312,7 +320,7 @@ void Fra_ClassesPrepare( Fra_Cla_t * p )
     // allocate room for classes
     p->pMemClasses = ALLOC( Aig_Obj_t *, 2*(nEntries + Vec_PtrSize(p->vClasses1)) );
     p->pMemClassesFree = p->pMemClasses + 2*nEntries;
-
+ 
     // copy the entries into storage in the topological order
     Vec_PtrClear( p->vClasses );
     nEntries = 0;
@@ -563,6 +571,32 @@ void Fra_ClassesTest( Fra_Cla_t * p, int Id1, int Id2 )
     Vec_PtrPush( p->vClasses, pClass );
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Creates latch correspondence classes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Fra_ClassesLatchCorr( Fra_Man_t * p )
+{
+    Aig_Obj_t * pObj;
+    int i, nEntries = 0;
+    Vec_PtrClear( p->pCla->vClasses1 );
+    Aig_ManForEachLoSeq( p->pManAig, pObj, i )
+    {
+        Vec_PtrPush( p->pCla->vClasses1, pObj );
+        Fra_ClassObjSetRepr( pObj, Aig_ManConst1(p->pManAig) );
+    }
+    // allocate room for classes
+    p->pCla->pMemClasses = ALLOC( Aig_Obj_t *, 2*(nEntries + Vec_PtrSize(p->pCla->vClasses1)) );
+    p->pCla->pMemClassesFree = p->pCla->pMemClasses + 2*nEntries;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/fra/fraCore.c b/src/aig/fra/fraCore.c
index 71e12a75..41d264bb 100644
--- a/src/aig/fra/fraCore.c
+++ b/src/aig/fra/fraCore.c
@@ -30,6 +30,63 @@
 
 /**Function*************************************************************
 
+  Synopsis    [Reports the status of the miter.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Fra_FraigMiterStatus( Aig_Man_t * p )
+{
+    Aig_Obj_t * pObj, * pObjNew;
+    int i, CountConst0 = 0, CountNonConst0 = 0, CountUndecided = 0;
+    if ( p->pData )
+        return 0;
+    Aig_ManForEachPoSeq( p, pObj, i )
+    {
+        pObjNew = Aig_ObjChild0(pObj);
+        // check if the output is constant 0
+        if ( pObjNew == Aig_ManConst0(p) )
+        {
+            CountConst0++;
+            continue;
+        }
+        // check if the output is constant 1
+        if ( pObjNew == Aig_ManConst1(p) )
+        {
+            CountNonConst0++;
+            continue;
+        }
+        // check if the output can be constant 0
+        if ( Aig_Regular(pObjNew)->fPhase != (unsigned)Aig_IsComplement(pObjNew) )
+        {
+            CountNonConst0++;
+            continue;
+        }
+        CountUndecided++;
+    }
+/*
+    if ( p->pParams->fVerbose )
+    {
+        printf( "Miter has %d outputs. ", Aig_ManPoNum(p->pManAig) );
+        printf( "Const0 = %d.  ", CountConst0 );
+        printf( "NonConst0 = %d.  ", CountNonConst0 );
+        printf( "Undecided = %d.  ", CountUndecided );
+        printf( "\n" );
+    }
+*/
+    if ( CountNonConst0 )
+        return 0;
+    if ( CountUndecided )
+        return -1;
+    return 1;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Write speculative miter for one node.]
 
   Description []
@@ -121,9 +178,9 @@ static inline void Fra_FraigNode( Fra_Man_t * p, Aig_Obj_t * pObj )
         Vec_PtrPush( p->vTimeouts, pObj );
     // simulate the counter-example and return the Fraig node
     Fra_Resimulate( p );
-    assert( Fra_ClassObjRepr(pObj) != pObjRepr );
     if ( Fra_ClassObjRepr(pObj) == pObjRepr )
         printf( "Fra_FraigNode(): Error in class refinement!\n" );
+    assert( Fra_ClassObjRepr(pObj) != pObjRepr );
 }
 
 /**Function*************************************************************
@@ -196,7 +253,7 @@ clk = clock();
         Aig_ManReprStart( p->pManFraig, Aig_ManObjIdMax(p->pManAig)+1 );
     // collect initial states
     p->nLitsZero = Vec_PtrSize( p->pCla->vClasses1 );
-    p->nLitsBeg = Fra_ClassesCountLits( p->pCla );
+    p->nLitsBeg  = Fra_ClassesCountLits( p->pCla );
     p->nNodesBeg = Aig_ManNodeNum(pManAig);
     p->nRegsBeg  = Aig_ManRegNum(pManAig);
     // perform fraig sweep
@@ -228,7 +285,7 @@ p->timeTrav += clock() - clk2;
     }
 p->timeTotal = clock() - clk;
     // collect final stats
-    p->nLitsEnd = Fra_ClassesCountLits( p->pCla );
+    p->nLitsEnd  = Fra_ClassesCountLits( p->pCla );
     p->nNodesEnd = Aig_ManNodeNum(pManAigNew);
     p->nRegsEnd  = Aig_ManRegNum(pManAigNew);
     Fra_ManStop( p );
diff --git a/src/aig/fra/fraImp.c b/src/aig/fra/fraImp.c
new file mode 100644
index 00000000..9643b887
--- /dev/null
+++ b/src/aig/fra/fraImp.c
@@ -0,0 +1,826 @@
+/**CFile****************************************************************
+
+  FileName    [fraImp.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [New FRAIG package.]
+
+  Synopsis    [Detecting and proving implications.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 30, 2007.]
+
+  Revision    [$Id: fraImp.c,v 1.00 2007/06/30 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "fra.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+// simulation manager
+typedef struct Sml_Man_t_   Sml_Man_t;
+struct Sml_Man_t_
+{
+    Aig_Man_t *      pAig;
+    int              nFrames;
+    int              nWordsFrame;
+    int              nWordsTotal;
+    unsigned         pData[0];
+};
+
+static inline unsigned * Sml_ObjSim( Sml_Man_t * p, int Id )  { return p->pData + p->nWordsTotal * Id; }
+static inline int        Sml_ImpLeft( int Imp )               { return Imp & 0xFFFF;                   }
+static inline int        Sml_ImpRight( int Imp )              { return Imp >> 16;                      }
+static inline int        Sml_ImpCreate( int Left, int Right ) { return (Right << 16) | Left;           }
+
+static int * s_ImpCost = NULL;
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Allocates simulation manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Sml_Man_t * Sml_ManStart( Aig_Man_t * pAig, int nFrames, int nWordsFrame )
+{
+    Sml_Man_t * p;
+    assert( Aig_ManObjIdMax(pAig) + 1 < (1 << 16) );
+    p = (Sml_Man_t *)malloc( sizeof(Sml_Man_t) + sizeof(unsigned) * (Aig_ManObjIdMax(pAig) + 1) * nFrames * nWordsFrame );
+    memset( p, 0, sizeof(Sml_Man_t) + sizeof(unsigned) * nFrames * nWordsFrame );
+    p->nFrames     = nFrames;
+    p->nWordsFrame = nWordsFrame;
+    p->nWordsTotal = nFrames * nWordsFrame;
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Deallocates simulation manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Sml_ManStop( Sml_Man_t * p )
+{
+    free( p );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Assigns random patterns to the PI node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Sml_ManAssignRandom( Sml_Man_t * p, Aig_Obj_t * pObj )
+{
+    unsigned * pSims;
+    int i;
+    assert( Aig_ObjIsPi(pObj) );
+    pSims = Sml_ObjSim( p, pObj->Id );
+    for ( i = 0; i < p->nWordsTotal; i++ )
+        pSims[i] = Fra_ObjRandomSim();
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Assigns constant patterns to the PI node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Sml_ManAssignConst( Sml_Man_t * p, Aig_Obj_t * pObj, int fConst1, int iFrame )
+{
+    unsigned * pSims;
+    int i;
+    assert( Aig_ObjIsPi(pObj) );
+    pSims = Sml_ObjSim( p, pObj->Id ) + p->nWordsFrame * iFrame;
+    for ( i = 0; i < p->nWordsFrame; i++ )
+        pSims[i] = fConst1? ~(unsigned)0 : 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Assings random simulation info for the PIs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Sml_ManInitialize( Sml_Man_t * p, int fInit )
+{
+    Aig_Obj_t * pObj;
+    int i;
+    if ( fInit )
+    {
+        assert( Aig_ManRegNum(p->pAig) > 0 );
+        assert( Aig_ManRegNum(p->pAig) < Aig_ManPiNum(p->pAig) );
+        // assign random info for primary inputs
+        Aig_ManForEachPiSeq( p->pAig, pObj, i )
+            Sml_ManAssignRandom( p, pObj );
+        // assign the initial state for the latches
+        Aig_ManForEachLoSeq( p->pAig, pObj, i )
+            Sml_ManAssignConst( p, pObj, 0, 0 );
+    }
+    else
+    {
+        Aig_ManForEachPi( p->pAig, pObj, i )
+            Sml_ManAssignRandom( p, pObj );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Assings distance-1 simulation info for the PIs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Sml_ManAssignDist1( Sml_Man_t * p, unsigned * pPat )
+{
+    Aig_Obj_t * pObj;
+    int f, i, k, Limit, nTruePis;
+    assert( p->nFrames > 0 );
+    if ( p->nFrames == 1 )
+    {
+        // copy the PI info 
+        Aig_ManForEachPi( p->pAig, pObj, i )
+            Sml_ManAssignConst( p, pObj, Aig_InfoHasBit(pPat, i), 0 );
+        // flip one bit
+        Limit = AIG_MIN( Aig_ManPiNum(p->pAig), p->nWordsTotal * 32 - 1 );
+        for ( i = 0; i < Limit; i++ )
+            Aig_InfoXorBit( Sml_ObjSim( p, Aig_ManPi(p->pAig,i)->Id ), i+1 );
+    }
+    else
+    {
+        // copy the PI info for each frame
+        nTruePis = Aig_ManPiNum(p->pAig) - Aig_ManRegNum(p->pAig);
+        for ( f = 0; f < p->nFrames; f++ )
+            Aig_ManForEachPiSeq( p->pAig, pObj, i )
+                Sml_ManAssignConst( p, pObj, Aig_InfoHasBit(pPat, nTruePis * f + i), f );
+        // copy the latch info 
+        k = 0;
+        Aig_ManForEachLoSeq( p->pAig, pObj, i )
+            Sml_ManAssignConst( p, pObj, Aig_InfoHasBit(pPat, nTruePis * p->nFrames + k++), 0 );
+//        assert( p->pManFraig == NULL || nTruePis * p->nFrames + k == Aig_ManPiNum(p->pManFraig) );
+
+        // flip one bit of the last frame
+        if ( p->nFrames == 2 )
+        {
+            Limit = AIG_MIN( nTruePis, p->nWordsFrame * 32 - 1 );
+            for ( i = 0; i < Limit; i++ )
+                Aig_InfoXorBit( Sml_ObjSim( p, Aig_ManPi(p->pAig, i)->Id ), i+1 );
+//            Aig_InfoXorBit( Sml_ObjSim( p, Aig_ManPi(p->pAig, nTruePis*(p->nFrames-2) + i)->Id ), i+1 );
+        }
+    }
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Simulates one node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Sml_NodeSimulate( Sml_Man_t * p, Aig_Obj_t * pObj, int iFrame )
+{
+    unsigned * pSims, * pSims0, * pSims1;
+    int fCompl, fCompl0, fCompl1, i;
+    int nSimWords = p->nWordsFrame;
+    assert( !Aig_IsComplement(pObj) );
+    assert( Aig_ObjIsNode(pObj) );
+    assert( iFrame == 0 || nSimWords < p->nWordsTotal );
+    // get hold of the simulation information
+    pSims  = Fra_ObjSim(pObj) + nSimWords * iFrame;
+    pSims0 = Fra_ObjSim(Aig_ObjFanin0(pObj)) + nSimWords * iFrame;
+    pSims1 = Fra_ObjSim(Aig_ObjFanin1(pObj)) + nSimWords * iFrame;
+    // get complemented attributes of the children using their random info
+    fCompl  = pObj->fPhase;
+    fCompl0 = Aig_ObjPhaseReal(Aig_ObjChild0(pObj));
+    fCompl1 = Aig_ObjPhaseReal(Aig_ObjChild1(pObj));
+    // simulate
+    if ( fCompl0 && fCompl1 )
+    {
+        if ( fCompl )
+            for ( i = 0; i < nSimWords; i++ )
+                pSims[i] = (pSims0[i] | pSims1[i]);
+        else
+            for ( i = 0; i < nSimWords; i++ )
+                pSims[i] = ~(pSims0[i] | pSims1[i]);
+    }
+    else if ( fCompl0 && !fCompl1 )
+    {
+        if ( fCompl )
+            for ( i = 0; i < nSimWords; i++ )
+                pSims[i] = (pSims0[i] | ~pSims1[i]);
+        else
+            for ( i = 0; i < nSimWords; i++ )
+                pSims[i] = (~pSims0[i] & pSims1[i]);
+    }
+    else if ( !fCompl0 && fCompl1 )
+    {
+        if ( fCompl )
+            for ( i = 0; i < nSimWords; i++ )
+                pSims[i] = (~pSims0[i] | pSims1[i]);
+        else
+            for ( i = 0; i < nSimWords; i++ )
+                pSims[i] = (pSims0[i] & ~pSims1[i]);
+    }
+    else // if ( !fCompl0 && !fCompl1 )
+    {
+        if ( fCompl )
+            for ( i = 0; i < nSimWords; i++ )
+                pSims[i] = ~(pSims0[i] & pSims1[i]);
+        else
+            for ( i = 0; i < nSimWords; i++ )
+                pSims[i] = (pSims0[i] & pSims1[i]);
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Simulates one node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Sml_NodeCopyFanin( Sml_Man_t * p, Aig_Obj_t * pObj, int iFrame )
+{
+    unsigned * pSims, * pSims0;
+    int fCompl, fCompl0, i;
+    int nSimWords = p->nWordsFrame;
+    assert( !Aig_IsComplement(pObj) );
+    assert( Aig_ObjIsPo(pObj) );
+    assert( iFrame == 0 || nSimWords < p->nWordsTotal );
+    // get hold of the simulation information
+    pSims  = Sml_ObjSim(p, pObj->Id) + nSimWords * iFrame;
+    pSims0 = Sml_ObjSim(p, Aig_ObjFanin0(pObj)->Id) + nSimWords * iFrame;
+    // get complemented attributes of the children using their random info
+    fCompl  = pObj->fPhase;
+    fCompl0 = Aig_ObjPhaseReal(Aig_ObjChild0(pObj));
+    // copy information as it is
+    if ( fCompl0 )
+        for ( i = 0; i < nSimWords; i++ )
+            pSims[i] = ~pSims0[i];
+    else
+        for ( i = 0; i < nSimWords; i++ )
+            pSims[i] = pSims0[i];
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Simulates one node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Sml_NodeTransferNext( Sml_Man_t * p, Aig_Obj_t * pOut, Aig_Obj_t * pIn, int iFrame )
+{
+    unsigned * pSims0, * pSims1;
+    int i, nSimWords = p->nWordsFrame;
+    assert( !Aig_IsComplement(pOut) );
+    assert( !Aig_IsComplement(pIn) );
+    assert( Aig_ObjIsPo(pOut) );
+    assert( Aig_ObjIsPi(pIn) );
+    assert( iFrame == 0 || nSimWords < p->nWordsTotal );
+    // get hold of the simulation information
+    pSims0 = Sml_ObjSim(p, pOut->Id) + nSimWords * iFrame;
+    pSims1 = Sml_ObjSim(p, pIn->Id) + nSimWords * (iFrame+1);
+    // copy information as it is
+    for ( i = 0; i < nSimWords; i++ )
+        pSims1[i] = pSims0[i];
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Simulates AIG manager.]
+
+  Description [Assumes that the PI simulation info is attached.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Sml_SimulateOne( Sml_Man_t * p )
+{
+    Aig_Obj_t * pObj, * pObjLi, * pObjLo;
+    int f, i, clk;
+clk = clock();
+    for ( f = 0; f < p->nFrames; f++ )
+    {
+        // simulate the nodes
+        Aig_ManForEachNode( p->pAig, pObj, i )
+            Sml_NodeSimulate( p, pObj, f );
+        if ( f == p->nFrames - 1 )
+            break;
+        // copy simulation info into outputs
+        Aig_ManForEachLiSeq( p->pAig, pObj, i )
+            Sml_NodeCopyFanin( p, pObj, f );
+        // copy simulation info into the inputs
+//        for ( i = 0; i < Aig_ManRegNum(p->pAig); i++ )
+//            Sml_NodeTransferNext( p, Aig_ManLi(p->pAig, i), Aig_ManLo(p->pAig, i), f );
+        Aig_ManForEachLiLoSeq( p->pAig, pObjLi, pObjLo, i )
+            Sml_NodeTransferNext( p, pObjLi, pObjLo, f );
+    }
+//p->timeSim += clock() - clk;
+//p->nSimRounds++;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs simulation of the uninitialized circuit.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Sml_Man_t * Sml_ManSimulateComb( Aig_Man_t * pAig, int nWords )
+{
+    Sml_Man_t * p;
+    p = Sml_ManStart( pAig, 1, nWords );
+    Sml_ManInitialize( p, 0 );
+    Sml_SimulateOne( p );
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs simulation of the initialized circuit.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Sml_Man_t * Sml_ManSimulateSeq( Aig_Man_t * pAig, int nFrames, int nWords )
+{
+    Sml_Man_t * p;
+    p = Sml_ManStart( pAig, nFrames, nWords );
+    Sml_ManInitialize( p, 1 );
+    Sml_SimulateOne( p );
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Counts the number of 1s in each siminfo of each node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int * Sml_ManCountOnes( Sml_Man_t * p )
+{
+    Aig_Obj_t * pObj;
+    unsigned * pSim;
+    int i, k, * pnBits; 
+    pnBits = ALLOC( int, Aig_ManObjIdMax(p->pAig) + 1 );  
+    memset( pnBits, 0, sizeof(int) * Aig_ManObjIdMax(p->pAig) + 1 );
+    Aig_ManForEachObj( p->pAig, pObj, i )
+    {
+        pSim = Sml_ObjSim( p, i );
+        for ( k = 0; k < p->nWordsTotal; k++ )
+            pnBits[i] += Aig_WordCountOnes( pSim[k] );
+    }
+    return pnBits;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Counts the number of 1s in the reverse implication.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Sml_NodeNotImpCost( Sml_Man_t * p, int Left, int Right )
+{
+    unsigned * pSimL, * pSimR;
+    int k, Counter = 0;
+    pSimL = Sml_ObjSim( p, Left );
+    pSimR = Sml_ObjSim( p, Right );
+    for ( k = 0; k < p->nWordsTotal; k++ )
+        Counter += Aig_WordCountOnes( pSimL[k] & ~pSimR[k] );
+    return Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if implications holds.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Sml_NodeCheckImp( Sml_Man_t * p, int Left, int Right )
+{
+    unsigned * pSimL, * pSimR;
+    int k;
+    pSimL = Sml_ObjSim( p, Left );
+    pSimR = Sml_ObjSim( p, Right );
+    for ( k = 0; k < p->nWordsTotal; k++ )
+        if ( pSimL[k] & ~pSimR[k] )
+            return 0;
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the array of nodes sorted by the number of 1s.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Sml_ManSortUsingOnes( Sml_Man_t * p )
+{
+    Aig_Obj_t * pObj;
+    Vec_Ptr_t * vNodes;
+    int i, nNodes, nTotal, nBits, * pnNodes, * pnBits, * pMemory;
+    // count 1s in each node's siminfo
+    pnBits = Sml_ManCountOnes( p );
+    // count number of nodes having that many 1s
+    nBits = p->nWordsTotal * 32;
+    assert( nBits >= 32 );
+    nNodes = 0;
+    pnNodes = ALLOC( int, nBits );
+    memset( pnNodes, 0, sizeof(int) * nBits );
+    Aig_ManForEachObj( p->pAig, pObj, i )
+    {
+        if ( i == 0 ) continue;
+        assert( pnBits[i] < nBits ); // "<" because of normalized info
+        pnNodes[pnBits[i]]++;
+        nNodes++;
+    }
+    // allocate memory for all the nodes
+    pMemory = ALLOC( int, nNodes + nBits );  
+    // markup the memory for each node
+    vNodes = Vec_PtrAlloc( nBits );
+    Vec_PtrPush( vNodes, pMemory );
+    Aig_ManForEachObj( p->pAig, pObj, i )
+    {
+        if ( i == 0 ) continue;
+        pMemory += pnBits[i-1] + 1;
+        Vec_PtrPush( vNodes, pMemory );
+    }
+    // add the nodes
+    memset( pnNodes, 0, sizeof(int) * nBits );
+    Aig_ManForEachObj( p->pAig, pObj, i )
+    {
+        if ( i == 0 ) continue;
+        pMemory = Vec_PtrEntry( vNodes, pnBits[i] );
+        pMemory[ pnNodes[pnBits[i]]++ ] = i;
+    }
+    // add 0s in the end
+    nTotal = 0;
+    Vec_PtrForEachEntry( vNodes, pMemory, i )
+    {
+        pMemory[ pnNodes[i]++ ] = 0;
+        nTotal += pnNodes[i];
+    }
+    assert( nTotal == nNodes + nBits );
+    return vNodes;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Compares two implications using their cost.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Sml_CompareCost( int * pNum1, int * pNum2 )
+{
+    int Cost1 = s_ImpCost[*pNum1];
+    int Cost2 = s_ImpCost[*pNum2];
+    if ( Cost1 > Cost2 )
+        return -1;
+    if ( Cost1 < Cost2  )
+        return 1;
+    return 0; 
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Compares two implications using their largest ID.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Sml_CompareMaxId( unsigned short * pImp1, unsigned short * pImp2 )
+{
+    int Max1 = AIG_MAX( pImp1[0], pImp1[1] );
+    int Max2 = AIG_MAX( pImp2[0], pImp2[1] );
+    if ( Max1 < Max2 )
+        return -1;
+    if ( Max1 > Max2  )
+        return 1;
+    return 0; 
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derives implication candidates.]
+
+  Description [Implication candidates have the property that 
+  (1) they hold using sequential simulation information
+  (2) they do not hold using combinational simulation information
+  (3) they have as high expressive power as possible (heuristically)
+      - this means they are relatively far in terms of Humming distance
+        meaning their complement covers a larger Boolean space
+      - they are easy to disprove combinationally
+        meaning they cover relatively a larger sequential subspace.]
+               
+  SideEffects [The managers should have the first pattern (000...)]
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Sml_ManImpDerive( Fra_Man_t * p, int nImpMaxLimit, int nImpUseLimit )
+{
+    Sml_Man_t * pSeq, * pComb;
+    Vec_Int_t * vImps, * vTemp;
+    Vec_Ptr_t * vNodes;
+    int * pNodesI, * pNodesK, * pNumbers;
+    int i, k, Imp;
+    assert( nImpMaxLimit > 0 && nImpUseLimit > 0 && nImpUseLimit <= nImpMaxLimit );
+    // normalize both managers
+    pComb = Sml_ManSimulateComb( p->pManAig, 32 );
+    pSeq = Sml_ManSimulateSeq( p->pManAig, 32, 1 );
+    // get the nodes sorted by the number of 1s
+    vNodes = Sml_ManSortUsingOnes( pSeq );
+    // compute implications and their costs
+    s_ImpCost = ALLOC( int, nImpMaxLimit );
+    vImps = Vec_IntAlloc( nImpMaxLimit );
+    for ( k = pSeq->nWordsTotal * 32 - 1; k >= 0; k-- )
+        for ( i = k - 1; i >= 0; i-- )
+        {
+            for ( pNodesI = Vec_PtrEntry( vNodes, i ); *pNodesI; pNodesI++ )
+            for ( pNodesK = Vec_PtrEntry( vNodes, k ); *pNodesK; pNodesK++ )
+            {
+                if ( Sml_NodeCheckImp(pSeq, *pNodesI, *pNodesK) &&
+                    !Sml_NodeCheckImp(pComb, *pNodesI, *pNodesK) )
+                {
+                    Imp = Sml_ImpCreate( *pNodesI, *pNodesK );
+                    s_ImpCost[ Vec_IntSize(vImps) ] = Sml_NodeNotImpCost(pComb, *pNodesI, *pNodesK);
+                    Vec_IntPush( vImps, Imp );
+                }
+                if ( Vec_IntSize(vImps) == nImpMaxLimit )
+                    goto finish;
+            }
+        }
+finish:
+    Sml_ManStop( pComb );
+    Sml_ManStop( pSeq );
+
+    // sort implications by their cost
+    pNumbers = ALLOC( int, Vec_IntSize(vImps) );
+    for ( i = 0; i < Vec_IntSize(vImps); i++ )
+        pNumbers[i] = i;
+    qsort( (void *)pNumbers, Vec_IntSize(vImps), sizeof(int), 
+            (int (*)(const void *, const void *)) Sml_CompareCost );
+    // reorder implications
+    vTemp = Vec_IntAlloc( nImpUseLimit );
+    for ( i = 0; i < nImpUseLimit; i++ )
+        Vec_IntPush( vTemp, Vec_IntEntry( vImps, pNumbers[i] ) );
+    Vec_IntFree( vImps );  vImps = vTemp;
+    // dealloc
+    free( pNumbers );
+    free( s_ImpCost ); s_ImpCost = NULL;
+    free( Vec_PtrEntry(vNodes, 0) );
+    Vec_PtrFree( vNodes );
+    // order implications by the max ID involved
+    qsort( (void *)Vec_IntArray(vImps), Vec_IntSize(vImps), sizeof(int), 
+            (int (*)(const void *, const void *)) Sml_CompareMaxId );
+    return vImps;
+}
+
+// the following three procedures are called to 
+// - add implications to the SAT solver
+// - check implications using the SAT solver
+// - refine implications using after a cex is generated
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Fra_ImpAddToSolver( Fra_Man_t * p, Vec_Int_t * vImps )
+{
+    sat_solver * pSat = p->pSat;
+    Aig_Obj_t * pLeft, * pRight;
+    Aig_Obj_t * pLeftF, * pRightF;
+    int pLits[2], Imp, Left, Right, i, f, status;
+    Vec_IntForEachEntry( vImps, Imp, i )
+    {
+        // get the corresponding nodes
+        pLeft = Aig_ManObj( p->pManAig, Sml_ImpLeft(Imp) );
+        pRight = Aig_ManObj( p->pManAig, Sml_ImpRight(Imp) );
+        // add constraints in each timeframe
+        for ( f = 0; f < p->pPars->nFramesK; f++ )
+        {
+            // map these info fraig
+            pLeftF = Fra_ObjFraig( pLeft, f );
+            pRightF = Fra_ObjFraig( pRight, f );
+            // get the corresponding SAT numbers
+            Left = Fra_ObjSatNum( Aig_Regular(pLeftF) );
+            Right = Fra_ObjSatNum( Aig_Regular(pRightF) );
+            assert( Left > 0  && Left < p->nSatVars );
+            assert( Right > 0 && Right < p->nSatVars );
+            // get the constaint
+            // L => R      L' v R      L & R'
+            pLits[0] = 2 * Left  + !Aig_ObjPhaseReal(pLeftF);
+            pLits[1] = 2 * Right +  Aig_ObjPhaseReal(pRightF);
+            // add contraint to solver
+            if ( !sat_solver_addclause( pSat, pLits, pLits + 2 ) )
+            {
+                sat_solver_delete( pSat );
+                p->pSat = NULL;
+                return;
+            }
+        }
+    }
+    status = sat_solver_simplify(pSat);
+    if ( status == 0 )
+    {
+        sat_solver_delete( pSat );
+        p->pSat = NULL;
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Check implications for the node (if they are present).]
+
+  Description [Returns the new position in the array.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Fra_ImpCheckForNode( Fra_Man_t * p, Vec_Int_t * vImps, Aig_Obj_t * pNode, int Pos )
+{
+    Aig_Obj_t * pLeft, * pRight;
+    int i, Imp, Left, Right, Max;
+    Vec_IntForEachEntryStart( vImps, Imp, i, Pos )
+    {
+        Left = Sml_ImpLeft(Imp);
+        Right = Sml_ImpRight(Imp);
+        Max = AIG_MAX( Left, Right );
+        assert( Max >= pNode->Id );
+        if ( Max > pNode->Id )
+            return i;
+        // get the corresponding nodes
+        pLeft = Aig_ManObj( p->pManAig, Left );
+        pRight = Aig_ManObj( p->pManAig, Right );
+        // check the implication 
+        // - if true, a clause is added
+        // - if false, a cex is simulated
+//        Fra_NodesAreImp( p, pLeft, pRight );
+        // make sure the implication is refined
+        assert( Vec_IntEntry(vImps, Pos) == 0 );
+    }
+    return i;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Removes those implications that no longer hold.]
+
+  Description [Returns 1 if refinement has happened.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Fra_ImpRefineUsingCex( Fra_Man_t * p, Vec_Int_t * vImps )
+{
+    Aig_Obj_t * pLeft, * pRight;
+    int Imp, i, RetValue = 0;
+    Vec_IntForEachEntry( vImps, Imp, i )
+    {
+        if ( Imp == 0 )
+            continue;
+        // get the corresponding nodes
+        pLeft = Aig_ManObj( p->pManAig, Sml_ImpLeft(Imp) );
+        pRight = Aig_ManObj( p->pManAig, Sml_ImpRight(Imp) );
+        // check if implication holds using this simulation info
+        if ( !Sml_NodeCheckImp(p->pSim, pLeft->Id, pRight->Id) )
+        {
+            Vec_IntWriteEntry( vImps, i, 0 );
+            RetValue = 1;
+        }
+    }
+    return RetValue;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Removes empty implications.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Fra_ImpCompactArray( Vec_Int_t * vImps )
+{
+    int i, k, Imp;
+    k = 0;
+    Vec_IntForEachEntry( vImps, Imp, i )
+        if ( Imp )
+            Vec_IntWriteEntry( vImps, k++, Imp );
+    Vec_IntShrink( vImps, k );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/fra/fraInd.c b/src/aig/fra/fraInd.c
index bb4c4287..4a7d7b7e 100644
--- a/src/aig/fra/fraInd.c
+++ b/src/aig/fra/fraInd.c
@@ -198,7 +198,7 @@ Aig_Man_t * Fra_FramesWithClasses( Fra_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesK, int fRewrite, int fVerbose )
+Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesK, int fRewrite, int fLatchCorr, int fVerbose, int * pnIter )
 {
     Fra_Man_t * p;
     Fra_Par_t Pars, * pPars = &Pars; 
@@ -208,7 +208,10 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesK, int fRewrite,
     int nIter, i, clk = clock(), clk2;
 
     if ( Aig_ManNodeNum(pManAig) == 0 )
+    {
+        if ( pnIter ) *pnIter = 0;
         return Aig_ManDup(pManAig, 1);
+    }
     assert( Aig_ManLatchNum(pManAig) == 0 );
     assert( Aig_ManRegNum(pManAig) > 0 );
     assert( nFramesK > 0 );
@@ -216,14 +219,18 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesK, int fRewrite,
 
     // get parameters
     Fra_ParamsDefaultSeq( pPars );
-    pPars->nFramesK = nFramesK;
-    pPars->fVerbose = fVerbose;
-    pPars->fRewrite = fRewrite;
+    pPars->nFramesK   = nFramesK;
+    pPars->fVerbose   = fVerbose;
+    pPars->fRewrite   = fRewrite;
+    pPars->fLatchCorr = fLatchCorr;
 
     // start the fraig manager for this run
     p = Fra_ManStart( pManAig, pPars );
     // derive and refine e-classes using K initialized frames
-    Fra_Simulate( p, 1 );
+//    if ( fLatchCorr )
+//        Fra_ClassesLatchCorr( p );
+//    else
+        Fra_Simulate( p, 1 );
     // refine e-classes using sequential simulation?
  
     p->nLitsZero = Vec_PtrSize( p->pCla->vClasses1 );
@@ -239,6 +246,8 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesK, int fRewrite,
         p->pCla->fRefinement = 0;
         // derive non-init K-timeframes while implementing e-classes
         p->pManFraig = Fra_FramesWithClasses( p );
+//Aig_ManDumpBlif( p->pManFraig, "testaig.blif" );
+
         // perform AIG rewriting
         if ( p->pPars->fRewrite )
             Fra_FraigInductionRewrite( p );
@@ -252,8 +261,8 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesK, int fRewrite,
         }
 
         // convert the manager to SAT solver (the last nLatches outputs are inputs)
-        pCnf = Cnf_Derive( p->pManFraig, Aig_ManRegNum(p->pManFraig) );
-//        pCnf = Cnf_DeriveSimple( p->pManFraig, Aig_ManRegNum(p->pManFraig) );
+//        pCnf = Cnf_Derive( p->pManFraig, Aig_ManRegNum(p->pManFraig) );
+        pCnf = Cnf_DeriveSimple( p->pManFraig, Aig_ManRegNum(p->pManFraig) );
 //Cnf_DataWriteIntoFile( pCnf, "temp.cnf", 1 );
 
         p->pSat = Cnf_DataWriteIntoSolver( pCnf );
@@ -278,7 +287,7 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesK, int fRewrite,
             Fra_ObjSetFaninVec( pObj, (void *)1 );
         }
         Cnf_DataFree( pCnf );
-/*
+/* 
         Aig_ManForEachObj( p->pManFraig, pObj, i )
         {
             Fra_ObjSetSatNum( pObj, pCnf->pVarNums[pObj->Id] );
@@ -300,6 +309,8 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesK, int fRewrite,
 clk2 = clock();
     Fra_ClassesCopyReprs( p->pCla, p->vTimeouts );
     pManAigNew = Aig_ManDupRepr( pManAig );
+    Aig_ManSeqCleanup( pManAigNew );
+//    Aig_ManCountMergeRegs( pManAigNew );
 p->timeTrav += clock() - clk2;
 p->timeTotal = clock() - clk;
     // get the final stats
@@ -309,9 +320,10 @@ p->timeTotal = clock() - clk;
     // free the manager
     Fra_ManStop( p );
     // check the output
-    if ( Aig_ManPoNum(pManAigNew) - Aig_ManRegNum(pManAigNew) == 1 )
-        if ( Aig_ObjChild0( Aig_ManPo(pManAigNew,0) ) == Aig_ManConst0(pManAigNew) )
-            printf( "Proved output constant 0.\n" );
+//    if ( Aig_ManPoNum(pManAigNew) - Aig_ManRegNum(pManAigNew) == 1 )
+//        if ( Aig_ObjChild0( Aig_ManPo(pManAigNew,0) ) == Aig_ManConst0(pManAigNew) )
+//            printf( "Proved output constant 0.\n" );
+    if ( pnIter ) *pnIter = nIter;
     return pManAigNew;
 }
 
diff --git a/src/aig/fra/fraMan.c b/src/aig/fra/fraMan.c
index 95cf28d8..4dcc4988 100644
--- a/src/aig/fra/fraMan.c
+++ b/src/aig/fra/fraMan.c
@@ -86,6 +86,7 @@ void Fra_ParamsDefaultSeq( Fra_Par_t * pPars )
     pPars->nFramesK         =       1;  // the number of timeframes to unroll
     pPars->fConeBias        =       0;
     pPars->fRewrite         =       0;
+    pPars->fLatchCorr       =       0;
 }
 
 /**Function*************************************************************
diff --git a/src/aig/fra/fraPart.c b/src/aig/fra/fraPart.c
new file mode 100644
index 00000000..d3fdbcfd
--- /dev/null
+++ b/src/aig/fra/fraPart.c
@@ -0,0 +1,177 @@
+/**CFile****************************************************************
+
+  FileName    [fraPart.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [New FRAIG package.]
+
+  Synopsis    [Partitioning for induction.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 30, 2007.]
+
+  Revision    [$Id: fraPart.c,v 1.00 2007/06/30 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "fra.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Fra_ManPartitionTest( Aig_Man_t * p, int nComLim )
+{
+    ProgressBar * pProgress;
+    Vec_Vec_t * vSupps, * vSuppsIn;
+    Vec_Ptr_t * vSuppsNew;
+    Vec_Int_t * vSupNew, * vSup, * vSup2, * vTemp;//, * vSupIn;
+    Vec_Int_t * vOverNew, * vQuantNew;
+    Aig_Obj_t * pObj;
+    int i, k, nCommon, CountOver, CountQuant;
+    int nTotalSupp, nTotalSupp2, Entry, Largest;//, iVar;
+    double Ratio, R;
+    int clk;
+
+    nTotalSupp = 0;
+    nTotalSupp2 = 0;
+    Ratio = 0.0;
+ 
+    // compute supports
+clk = clock();
+    vSupps = Aig_ManSupports( p );
+PRT( "Supports", clock() - clk );
+    // remove last entry
+    Aig_ManForEachPo( p, pObj, i )
+    {
+        vSup = Vec_VecEntry( vSupps, i );
+        Vec_IntPop( vSup );
+        // remember support
+//        pObj->pNext = (Aig_Obj_t *)vSup;
+    }
+
+    // create reverse supports
+clk = clock();
+    vSuppsIn = Vec_VecStart( Aig_ManPiNum(p) );
+    Aig_ManForEachPo( p, pObj, i )
+    {
+        vSup = Vec_VecEntry( vSupps, i );
+        Vec_IntForEachEntry( vSup, Entry, k )
+            Vec_VecPush( vSuppsIn, Entry, (void *)i );
+    }
+PRT( "Inverse ", clock() - clk );
+
+clk = clock();
+    // compute extended supports
+    Largest = 0;
+    vSuppsNew = Vec_PtrAlloc( Aig_ManPoNum(p) );
+    vOverNew  = Vec_IntAlloc( Aig_ManPoNum(p) );
+    vQuantNew = Vec_IntAlloc( Aig_ManPoNum(p) );
+    pProgress = Extra_ProgressBarStart( stdout, Aig_ManPoNum(p) );
+    Aig_ManForEachPo( p, pObj, i )
+    {
+        Extra_ProgressBarUpdate( pProgress, i, NULL );
+        // get old supports
+        vSup = Vec_VecEntry( vSupps, i );
+        if ( Vec_IntSize(vSup) < 2 )
+            continue;
+        // compute new supports
+        CountOver = CountQuant = 0;
+        vSupNew = Vec_IntDup( vSup );
+        // go through the nodes where the first var appears
+        Aig_ManForEachPo( p, pObj, k )
+//        iVar = Vec_IntEntry( vSup, 0 );
+//        vSupIn = Vec_VecEntry( vSuppsIn, iVar );
+//        Vec_IntForEachEntry( vSupIn, Entry, k )
+        {
+//            pObj = Aig_ManObj( p, Entry );
+            // get support of this output
+//            vSup2 = (Vec_Int_t *)pObj->pNext;
+            vSup2 = Vec_VecEntry( vSupps, k );
+            // count the number of common vars
+            nCommon = Vec_IntTwoCountCommon(vSup, vSup2);
+            if ( nCommon < 2 )
+                continue;
+            if ( nCommon > nComLim )
+            {
+                vSupNew = Vec_IntTwoMerge( vTemp = vSupNew, vSup2 );
+                Vec_IntFree( vTemp );
+                CountOver++;
+            }
+            else
+                CountQuant++;
+        }
+        // save the results
+        Vec_PtrPush( vSuppsNew, vSupNew );
+        Vec_IntPush( vOverNew, CountOver );
+        Vec_IntPush( vQuantNew, CountQuant );
+
+        if ( Largest < Vec_IntSize(vSupNew) )
+            Largest = Vec_IntSize(vSupNew);
+
+        nTotalSupp  += Vec_IntSize(vSup);
+        nTotalSupp2 += Vec_IntSize(vSupNew);
+        if ( Vec_IntSize(vSup) )
+            R = Vec_IntSize(vSupNew) / Vec_IntSize(vSup);
+        else
+            R = 0;
+        Ratio += R;
+
+        if ( R < 5.0 )
+            continue;
+
+        printf( "%6d : ", i );
+        printf( "S = %5d. ", Vec_IntSize(vSup) );
+        printf( "SNew = %5d. ", Vec_IntSize(vSupNew) );
+        printf( "R = %7.2f. ", R );
+        printf( "Over = %5d. ", CountOver );
+        printf( "Quant = %5d. ", CountQuant );
+        printf( "\n" );
+/*
+        Vec_IntForEachEntry( vSupNew, Entry, k )
+            printf( "%d ", Entry );
+        printf( "\n" );
+*/
+    }
+    Extra_ProgressBarStop( pProgress );
+PRT( "Scanning", clock() - clk );
+
+    // print cumulative statistics
+    printf( "PIs = %6d. POs = %6d. Lim = %3d.   AveS = %3d. SN = %3d. R = %4.2f Max = %5d.\n",
+        Aig_ManPiNum(p), Aig_ManPoNum(p), nComLim,
+        nTotalSupp/Aig_ManPoNum(p), nTotalSupp2/Aig_ManPoNum(p),
+        Ratio/Aig_ManPoNum(p), Largest );
+
+    Vec_VecFree( vSupps );
+    Vec_VecFree( vSuppsIn );
+    Vec_VecFree( (Vec_Vec_t *)vSuppsNew );
+    Vec_IntFree( vOverNew );
+    Vec_IntFree( vQuantNew );
+}
+
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/fra/fraSec.c b/src/aig/fra/fraSec.c
new file mode 100644
index 00000000..6afa6f89
--- /dev/null
+++ b/src/aig/fra/fraSec.c
@@ -0,0 +1,95 @@
+/**CFile****************************************************************
+
+  FileName    [fraSec.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [New FRAIG package.]
+
+  Synopsis    [Performs SEC based on seq sweeping.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 30, 2007.]
+
+  Revision    [$Id: fraSec.c,v 1.00 2007/06/30 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "fra.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Fra_FraigSec( Aig_Man_t * p, int nFramesFix, int fVerbose, int fVeryVerbose )
+{
+    Aig_Man_t * pNew;
+    int nFrames, RetValue, nIter, clk, clkTotal = clock();
+    if ( nFramesFix )
+    {
+        nFrames = nFramesFix;
+        // perform seq sweeping for one frame number
+        pNew = Fra_FraigInduction( p, nFrames, 0, 0, fVeryVerbose, &nIter );
+    }
+    else
+    {
+        // perform seq sweeping while increasing the number of frames
+        for ( nFrames = 1; ; nFrames++ )
+        {
+clk = clock();
+            pNew = Fra_FraigInduction( p, nFrames, 0, 0, fVeryVerbose, &nIter );
+            RetValue = Fra_FraigMiterStatus( pNew );
+            if ( fVerbose )
+            {
+                printf( "FRAMES %3d : Iters = %3d. ", nFrames, nIter );
+                if ( RetValue == 1 )
+                    printf( "UNSAT     " );
+                else
+                    printf( "UNDECIDED " );
+PRT( "Time", clock() - clk );
+            }
+            if ( RetValue != -1 )
+                break;
+            Aig_ManStop( pNew );
+        }
+    }
+
+    // get the miter status
+    RetValue = Fra_FraigMiterStatus( pNew );
+    Aig_ManStop( pNew );
+
+    // report the miter
+    if ( RetValue == 1 )
+        printf( "Networks are equivalent after seq sweeping with K=%d frames (%d iters). ", nFrames, nIter );
+    else if ( RetValue == 0 )
+        printf( "Networks are NOT EQUIVALENT. " );
+    else
+        printf( "Networks are UNDECIDED after seq sweeping with K=%d frames (%d iters). ", nFrames, nIter );
+PRT( "Time", clock() - clkTotal );
+    return RetValue;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/fra/fraSim.c b/src/aig/fra/fraSim.c
index 4a6e0251..c17cea9f 100644
--- a/src/aig/fra/fraSim.c
+++ b/src/aig/fra/fraSim.c
@@ -537,7 +537,7 @@ int Fra_SelectBestPat( Fra_Man_t * p )
 ***********************************************************************/
 void Fra_SimulateOne( Fra_Man_t * p )
 {
-    Aig_Obj_t * pObj;
+    Aig_Obj_t * pObj, * pObjLi, * pObjLo;
     int f, i, clk;
 clk = clock();
     for ( f = 0; f < p->nFramesAll; f++ )
@@ -551,9 +551,10 @@ clk = clock();
         Aig_ManForEachLiSeq( p->pManAig, pObj, i )
             Fra_NodeCopyFanin( p, pObj, f );
         // copy simulation info into the inputs
-        for ( i = 0; i < Aig_ManRegNum(p->pManAig); i++ )
-            Fra_NodeTransferNext( p, Aig_ManLi(p->pManAig, i), Aig_ManLo(p->pManAig, i), f );
-
+//        for ( i = 0; i < Aig_ManRegNum(p->pManAig); i++ )
+//            Fra_NodeTransferNext( p, Aig_ManLi(p->pManAig, i), Aig_ManLo(p->pManAig, i), f );
+        Aig_ManForEachLiLoSeq( p->pManAig, pObjLi, pObjLo, i )
+            Fra_NodeTransferNext( p, pObjLi, pObjLo, f );
     }
 p->timeSim += clock() - clk;
 p->nSimRounds++;
@@ -627,7 +628,7 @@ void Fra_Simulate( Fra_Man_t * p, int fInit )
     // start the classes
     Fra_AssignRandom( p, fInit );
     Fra_SimulateOne( p );
-    Fra_ClassesPrepare( p->pCla );
+    Fra_ClassesPrepare( p->pCla, p->pPars->fLatchCorr );
 //    Fra_ClassesPrint( p->pCla, 0 );
 //printf( "Starting classes = %5d.   Pairs = %6d.\n", p->lClasses.nItems, Fra_CountPairsClasses(p) );
 
diff --git a/src/aig/fra/module.make b/src/aig/fra/module.make
index 191427c9..f2a8b230 100644
--- a/src/aig/fra/module.make
+++ b/src/aig/fra/module.make
@@ -1,7 +1,10 @@
-SRC +=    src/aig/fra/fraClass.c \
+SRC +=    src/aig/fra/fraCec.c \
+    src/aig/fra/fraClass.c \
     src/aig/fra/fraCnf.c \
     src/aig/fra/fraCore.c \
+    src/aig/fra/fraImp.c \
     src/aig/fra/fraInd.c \
     src/aig/fra/fraMan.c \
     src/aig/fra/fraSat.c \
+    src/aig/fra/fraSec.c \
     src/aig/fra/fraSim.c