Version abc70822

17 files changed, 1380 insertions, 368 deletions

diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h
index 953d98ac..1ee62ad6 100644
--- a/src/aig/aig/aig.h
+++ b/src/aig/aig/aig.h
@@ -359,6 +359,7 @@ extern Vec_Ptr_t *     Aig_ManDfsChoices( Aig_Man_t * p );
 extern Vec_Ptr_t *     Aig_ManDfsReverse( Aig_Man_t * p );
 extern int             Aig_ManCountLevels( Aig_Man_t * p );
 extern int             Aig_DagSize( Aig_Obj_t * pObj );
+extern int             Aig_SupportSize( Aig_Man_t * p, Aig_Obj_t * pObj );
 extern void            Aig_ConeUnmark_rec( Aig_Obj_t * pObj );
 extern Aig_Obj_t *     Aig_Transfer( Aig_Man_t * pSour, Aig_Man_t * pDest, Aig_Obj_t * pObj, int nVars );
 extern Aig_Obj_t *     Aig_Compose( Aig_Man_t * p, Aig_Obj_t * pRoot, Aig_Obj_t * pFunc, int iVar );
@@ -434,10 +435,9 @@ 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 );
+extern Aig_Man_t *     Rtm_ManRetime( Aig_Man_t * p, int fForward, 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 ========================================================*/
@@ -458,6 +458,8 @@ extern void            Aig_ManVerifyLevel( Aig_Man_t * p );
 extern void            Aig_ManVerifyReverseLevel( Aig_Man_t * p );
 /*=== aigTruth.c ========================================================*/
 extern unsigned *      Aig_ManCutTruth( Aig_Obj_t * pRoot, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vNodes, Vec_Ptr_t * vTruthElem, Vec_Ptr_t * vTruthStore );
+/*=== aigTsim.c ========================================================*/
+extern Aig_Man_t *     Aig_ManConstReduce( Aig_Man_t * p, int fVerbose );
 /*=== aigUtil.c =========================================================*/
 extern unsigned        Aig_PrimeCudd( unsigned p );
 extern void            Aig_ManIncrementTravId( Aig_Man_t * p );
diff --git a/src/aig/aig/aigDfs.c b/src/aig/aig/aigDfs.c
index 5a18c4ac..86509322 100644
--- a/src/aig/aig/aigDfs.c
+++ b/src/aig/aig/aigDfs.c
@@ -380,6 +380,54 @@ int Aig_DagSize( Aig_Obj_t * pObj )
 
 /**Function*************************************************************
 
+  Synopsis    [Counts the support size of the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_SupportSize_rec( Aig_Man_t * p, Aig_Obj_t * pObj, int * pCounter )
+{
+    if ( Aig_ObjIsTravIdCurrent(p, pObj) )
+        return;
+    Aig_ObjSetTravIdCurrent(p, pObj);
+    if ( Aig_ObjIsPi(pObj) )
+    {
+        (*pCounter)++;
+        return;
+    }
+    assert( Aig_ObjIsNode(pObj) || Aig_ObjIsBuf(pObj) );
+    Aig_SupportSize_rec( p, Aig_ObjFanin0(pObj), pCounter );
+    if ( Aig_ObjFanin1(pObj) )
+        Aig_SupportSize_rec( p, Aig_ObjFanin1(pObj), pCounter );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Counts the support size of the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Aig_SupportSize( Aig_Man_t * p, Aig_Obj_t * pObj )
+{
+    int Counter = 0;
+    assert( !Aig_IsComplement(pObj) );
+    assert( !Aig_ObjIsPo(pObj) );
+    Aig_ManIncrementTravId( p );
+    Aig_SupportSize_rec( p, pObj, &Counter );
+    return Counter;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Transfers the AIG from one manager into another.]
 
   Description []
diff --git a/src/aig/aig/aigRepr.c b/src/aig/aig/aigRepr.c
index a862bf97..3e588979 100644
--- a/src/aig/aig/aigRepr.c
+++ b/src/aig/aig/aigRepr.c
@@ -130,7 +130,7 @@ static inline Aig_Obj_t * Aig_ObjFindRepr( Aig_Man_t * p, Aig_Obj_t * pNode )
     assert( p->pReprs != NULL );
     assert( !Aig_IsComplement(pNode) );
     assert( pNode->Id < p->nReprsAlloc );
-    assert( !p->pReprs[pNode->Id] || p->pReprs[pNode->Id]->Id < pNode->Id );
+//    assert( !p->pReprs[pNode->Id] || p->pReprs[pNode->Id]->Id < pNode->Id );
     return p->pReprs[pNode->Id];
 }
 
@@ -210,12 +210,38 @@ void Aig_ManTransferRepr( Aig_Man_t * pNew, Aig_Man_t * p )
     assert( pNew->pReprs != NULL );
     // go through the nodes which have representatives
     Aig_ManForEachObj( p, pObj, k )
-        if ( pRepr = Aig_ObjFindRepr(p, pObj) )
+        if ( (pRepr = Aig_ObjFindRepr(p, pObj)) )
             Aig_ObjSetRepr( pNew, Aig_Regular(pRepr->pData), Aig_Regular(pObj->pData) ); 
 }
 
 /**Function*************************************************************
 
+  Synopsis    [Duplicates the AIG manager recursively.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Obj_t * Aig_ManDupRepr_rec( Aig_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t * pObj )
+{
+    Aig_Obj_t * pRepr;
+    if ( pObj->pData )
+        return pObj->pData;
+    if ( (pRepr = Aig_ObjFindRepr(p, pObj)) )
+    {
+        Aig_ManDupRepr_rec( pNew, p, pRepr );
+        return pObj->pData = Aig_NotCond( pRepr->pData, pRepr->fPhase ^ pObj->fPhase );
+    }
+    Aig_ManDupRepr_rec( pNew, p, Aig_ObjFanin0(pObj) );
+    Aig_ManDupRepr_rec( pNew, p, Aig_ObjFanin1(pObj) );
+    return pObj->pData = Aig_And( pNew, Aig_ObjChild0Repr(p, pObj), Aig_ObjChild1Repr(p, pObj) );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Duplicates AIG while substituting representatives.]
 
   Description []
@@ -227,27 +253,29 @@ void Aig_ManTransferRepr( Aig_Man_t * pNew, Aig_Man_t * p )
 ***********************************************************************/
 Aig_Man_t * Aig_ManDupRepr( Aig_Man_t * p )
 {
+    int fOrdered = 1;
     Aig_Man_t * pNew;
-    Aig_Obj_t * pObj, * pRepr;
+    Aig_Obj_t * pObj;
     int i;
     // start the HOP package
     pNew = Aig_ManStart( Aig_ManObjIdMax(p) + 1 );
     pNew->nRegs = p->nRegs;
     Aig_ManReprStart( pNew, Aig_ManObjIdMax(p)+1 );
     // map the const and primary inputs
+    Aig_ManCleanData( p );
     Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
     Aig_ManForEachPi( p, pObj, i )
         pObj->pData = Aig_ObjCreatePi(pNew);
     // map the internal nodes
-//printf( "\n" );
-    Aig_ManForEachNode( p, pObj, i )
+    if ( fOrdered )
     {
-        pObj->pData = Aig_And( pNew, Aig_ObjChild0Repr(p, pObj), Aig_ObjChild1Repr(p, pObj) );
-        if ( pRepr = Aig_ObjFindRepr(p, pObj) ) // member of the class
-        {
-//printf( "Using node %d for node %d.\n", pRepr->Id, pObj->Id );
-            Aig_ObjSetRepr( pNew, Aig_Regular(pRepr->pData), Aig_Regular(pObj->pData) );
-        }
+        Aig_ManForEachNode( p, pObj, i )
+            pObj->pData = Aig_And( pNew, Aig_ObjChild0Repr(p, pObj), Aig_ObjChild1Repr(p, pObj) );
+    }
+    else
+    {
+        Aig_ManForEachPo( p, pObj, i )
+            Aig_ManDupRepr_rec( pNew, p, Aig_ObjFanin0(pObj) );
     }
     // transfer the POs
     Aig_ManForEachPo( p, pObj, i )
diff --git a/src/aig/aig/aigRet.c b/src/aig/aig/aigRet.c
index eacf756b..38fcc719 100644
--- a/src/aig/aig/aigRet.c
+++ b/src/aig/aig/aigRet.c
@@ -40,9 +40,11 @@ struct Rtm_Man_t_
     Vec_Ptr_t *      vPis;           // PIs only
     Vec_Ptr_t *      vPos;           // POs only
     Aig_MmFlex_t *   pMem;           // the memory manager
+    // autonomous components after cutting off
     // storage for overflow latches
-    unsigned *       pExtra;       
-    unsigned *       pExtraFree;
+    unsigned *       pExtra;   
+    int              nExtraCur;
+    int              nExtraAlloc;
 };
 
 typedef struct Rtm_Edg_t_    Rtm_Edg_t;
@@ -58,32 +60,59 @@ 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    fAuto   :  1;   // this object belongs to an autonomous component
     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
+    unsigned         Num     : 17;   // 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 inline Rtm_Obj_t * Rtm_ObjFanin( Rtm_Obj_t * pObj, int i )        { return (Rtm_Obj_t *)pObj->pFanio[2*i];                     }
+static inline Rtm_Obj_t * Rtm_ObjFanout( Rtm_Obj_t * pObj, int i )       { return (Rtm_Obj_t *)pObj->pFanio[2*(pObj->nFanins+i)];     }
+static inline Rtm_Edg_t * Rtm_ObjEdge( Rtm_Obj_t * pObj, int i )         { return (Rtm_Edg_t *)(pObj->pFanio + 2*i + 1);              }
+static inline Rtm_Edg_t * Rtm_ObjFanoutEdge( Rtm_Obj_t * pObj, int i )   { return (Rtm_Edg_t *)pObj->pFanio[2*(pObj->nFanins+i) + 1]; }
+
+static inline 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 inline Rtm_Init_t  Rtm_InitNotCond( Rtm_Init_t Val, int c )       { return c ? Rtm_InitNot(Val) : Val;                         }
+static inline 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 inline int         Rtm_InitWordsNum( int nLats )                  { return (nLats >> 4) + ((nLats & 15) > 0); }
+static inline int         Rtm_InitGetTwo( unsigned * p, int i )          { return (p[i>>4] >> ((i & 15)<<1)) & 3;    }
+static inline void        Rtm_InitSetTwo( unsigned * p, int i, int val ) { p[i>>4] |= (val << ((i & 15)<<1));        }
+static inline void        Rtm_InitXorTwo( unsigned * p, int i, int val ) { p[i>>4] ^= (val << ((i & 15)<<1));        }
+
+static inline Rtm_Init_t  Rtm_ObjGetFirst1( Rtm_Edg_t * pEdge )          { return pEdge->LData & 3;                                    }
+static inline Rtm_Init_t  Rtm_ObjGetLast1( Rtm_Edg_t * pEdge )           { return (pEdge->LData >> ((pEdge->nLats-1)<<1)) & 3;         }
+static inline Rtm_Init_t  Rtm_ObjGetOne1( Rtm_Edg_t * pEdge, int i )     { assert( i < (int)pEdge->nLats ); return (pEdge->LData >> (i << 1)) & 3;  }
+static inline Rtm_Init_t  Rtm_ObjRemFirst1( Rtm_Edg_t * pEdge )          { int Val = pEdge->LData & 3; pEdge->LData >>= 2; assert(pEdge->nLats > 0); pEdge->nLats--; return Val;  }
+static inline Rtm_Init_t  Rtm_ObjRemLast1( Rtm_Edg_t * pEdge )           { int Val = (pEdge->LData >> ((pEdge->nLats-1)<<1)) & 3; pEdge->LData ^= Val << ((pEdge->nLats-1)<<1); assert(pEdge->nLats > 0); pEdge->nLats--; return Val;  }
+static inline void        Rtm_ObjAddFirst1( Rtm_Edg_t * pEdge, Rtm_Init_t Val ) { assert( Val > 0 && Val < 4 ); pEdge->LData = (pEdge->LData << 2) | Val;  pEdge->nLats++;   }
+static inline void        Rtm_ObjAddLast1( Rtm_Edg_t * pEdge, Rtm_Init_t Val )  { assert( Val > 0 && Val < 4 ); pEdge->LData |= Val << (pEdge->nLats<<1);  pEdge->nLats++;   }
+
+static inline Rtm_Init_t  Rtm_ObjGetFirst2( Rtm_Man_t * p, Rtm_Edg_t * pEdge )                 { return Rtm_InitGetTwo( p->pExtra + pEdge->LData, 0 );                }
+static inline Rtm_Init_t  Rtm_ObjGetLast2( Rtm_Man_t * p, Rtm_Edg_t * pEdge )                  { return Rtm_InitGetTwo( p->pExtra + pEdge->LData, pEdge->nLats - 1 ); }
+static inline Rtm_Init_t  Rtm_ObjGetOne2( Rtm_Man_t * p, Rtm_Edg_t * pEdge, int i )            { return Rtm_InitGetTwo( p->pExtra + pEdge->LData, i );                }
+static        Rtm_Init_t  Rtm_ObjRemFirst2( Rtm_Man_t * p, Rtm_Edg_t * pEdge );
+static inline Rtm_Init_t  Rtm_ObjRemLast2( Rtm_Man_t * p, Rtm_Edg_t * pEdge )                  { Rtm_Init_t Val = Rtm_ObjGetLast2( p, pEdge );    Rtm_InitXorTwo( p->pExtra + pEdge->LData, pEdge->nLats - 1, Val ); pEdge->nLats--; return Val; }
+static        void        Rtm_ObjAddFirst2( Rtm_Man_t * p, Rtm_Edg_t * pEdge, Rtm_Init_t Val );
+static inline void        Rtm_ObjAddLast2( Rtm_Man_t * p, Rtm_Edg_t * pEdge, Rtm_Init_t Val )  { Rtm_InitSetTwo( p->pExtra + pEdge->LData, pEdge->nLats, Val );  pEdge->nLats++;  }
+
+static        void        Rtm_ObjTransferToSmall( Rtm_Man_t * p, Rtm_Edg_t * pEdge );
+static        void        Rtm_ObjTransferToBig( Rtm_Man_t * p, Rtm_Edg_t * pEdge ); 
+static        void        Rtm_ObjTransferToBigger( Rtm_Man_t * p, Rtm_Edg_t * pEdge );
+
+static inline Rtm_Init_t  Rtm_ObjGetFirst( Rtm_Man_t * p, Rtm_Edg_t * pEdge )                  { return pEdge->nLats > 10? Rtm_ObjGetFirst2(p, pEdge)  : Rtm_ObjGetFirst1(pEdge);   }
+static inline Rtm_Init_t  Rtm_ObjGetLast( Rtm_Man_t * p, Rtm_Edg_t * pEdge )                   { return pEdge->nLats > 10? Rtm_ObjGetLast2(p, pEdge)   : Rtm_ObjGetLast1(pEdge);    }
+static inline Rtm_Init_t  Rtm_ObjGetOne( Rtm_Man_t * p, Rtm_Edg_t * pEdge, int i )             { return pEdge->nLats > 10? Rtm_ObjGetOne2(p, pEdge, i) : Rtm_ObjGetOne1(pEdge, i);  }
+static        Rtm_Init_t  Rtm_ObjRemFirst( Rtm_Man_t * p, Rtm_Edg_t * pEdge )                  { Rtm_Init_t Res = pEdge->nLats > 10 ? Rtm_ObjRemFirst2(p, pEdge) : Rtm_ObjRemFirst1(pEdge); if ( pEdge->nLats == 10 ) Rtm_ObjTransferToSmall(p, pEdge); return Res; }
+static        Rtm_Init_t  Rtm_ObjRemLast( Rtm_Man_t * p, Rtm_Edg_t * pEdge )                   { Rtm_Init_t Res = pEdge->nLats > 10 ? Rtm_ObjRemLast2(p, pEdge)  : Rtm_ObjRemLast1(pEdge);  if ( pEdge->nLats == 10 ) Rtm_ObjTransferToSmall(p, pEdge); return Res; }
+static        void        Rtm_ObjAddFirst( Rtm_Man_t * p, Rtm_Edg_t * pEdge, Rtm_Init_t Val )  { if ( pEdge->nLats == 10 ) Rtm_ObjTransferToBig(p, pEdge); else if ( (pEdge->nLats & 15) == 15 ) Rtm_ObjTransferToBigger(p, pEdge); if ( pEdge->nLats >= 10 ) Rtm_ObjAddFirst2(p, pEdge, Val); else Rtm_ObjAddFirst1(pEdge, Val); }
+static        void        Rtm_ObjAddLast( Rtm_Man_t * p, Rtm_Edg_t * pEdge, Rtm_Init_t Val )   { if ( pEdge->nLats == 10 ) Rtm_ObjTransferToBig(p, pEdge); else if ( (pEdge->nLats & 15) == 15 ) Rtm_ObjTransferToBigger(p, pEdge); if ( pEdge->nLats >= 10 ) Rtm_ObjAddLast2(p, pEdge, Val);  else Rtm_ObjAddLast1(pEdge, Val);  }
 
-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 )                                          \
@@ -113,6 +142,149 @@ static void        Rtm_ObjAddLast( Rtm_Edg_t * pEdge, Rtm_Init_t Lat )  { assert
 
 /**Function*************************************************************
 
+  Synopsis    [Transfers from big to small storage.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Rtm_ObjTransferToSmall( Rtm_Man_t * p, Rtm_Edg_t * pEdge ) 
+{
+    assert( pEdge->nLats == 10 );
+    pEdge->LData = p->pExtra[pEdge->LData];
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Transfers from small to big storage.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Rtm_ObjTransferToBig( Rtm_Man_t * p, Rtm_Edg_t * pEdge ) 
+{
+    assert( pEdge->nLats == 10 );
+    if ( p->nExtraCur + 1 > p->nExtraAlloc )
+    {
+        int nExtraAllocNew = AIG_MAX( 2 * p->nExtraAlloc, 1024 );
+        p->pExtra = REALLOC( unsigned, p->pExtra, nExtraAllocNew );
+        p->nExtraAlloc = nExtraAllocNew;
+    }
+    p->pExtra[p->nExtraCur] = pEdge->LData;
+    pEdge->LData = p->nExtraCur++;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Transfers to bigger storage.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Rtm_ObjTransferToBigger( Rtm_Man_t * p, Rtm_Edg_t * pEdge ) 
+{
+    int nWords;
+    assert( (pEdge->nLats & 15) == 15 );
+    nWords = (pEdge->nLats + 1) >> 4;
+    if ( p->nExtraCur + nWords + 1 > p->nExtraAlloc )
+    {
+        int nExtraAllocNew = AIG_MAX( 2 * p->nExtraAlloc, 1024 );
+        p->pExtra = REALLOC( unsigned, p->pExtra, nExtraAllocNew );
+        p->nExtraAlloc = nExtraAllocNew;
+    }
+    memcpy( p->pExtra + p->nExtraCur, p->pExtra + pEdge->LData, sizeof(unsigned) * nWords );
+    p->pExtra[p->nExtraCur + nWords] = 0;
+    pEdge->LData = p->nExtraCur;
+    p->nExtraCur += nWords + 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Rtm_Init_t  Rtm_ObjRemFirst2( Rtm_Man_t * p, Rtm_Edg_t * pEdge )                 
+{ 
+    Rtm_Init_t Val = 0, Temp;   
+    unsigned * pB = p->pExtra + pEdge->LData, * pE = pB + Rtm_InitWordsNum( pEdge->nLats-- ) - 1;  
+    while ( pE >= pB ) 
+    {
+        Temp = *pE & 3;
+        *pE = (*pE >> 2) | (Val << 30);
+        Val = Temp;
+        pE--;
+    }
+    assert( Val != 0 );
+    return Val;  
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Rtm_ObjAddFirst2( Rtm_Man_t * p, Rtm_Edg_t * pEdge, Rtm_Init_t Val ) 
+{
+    unsigned * pB = p->pExtra + pEdge->LData, * pE = pB + Rtm_InitWordsNum( ++pEdge->nLats ); 
+    Rtm_Init_t Temp;
+    assert( Val != 0 );
+    while ( pB < pE ) 
+    {
+        Temp = *pB >> 30;
+        *pB = (*pB << 2) | Val;
+        Val = Temp;
+        pB++;
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Rtm_PrintEdge( Rtm_Man_t * p, Rtm_Edg_t * pEdge ) 
+{
+    unsigned LData = pEdge->LData;
+    printf( "%d : ", pEdge->nLats );
+    if ( pEdge->nLats > 10 )
+        Extra_PrintBinary( stdout, p->pExtra + pEdge->LData, 2*(pEdge->nLats+1) );
+    else
+        Extra_PrintBinary( stdout, &LData, 2*(pEdge->nLats+1) );
+    printf( "\n" );
+}
+
+
+/**Function*************************************************************
+
   Synopsis    [Allocates the retiming manager.]
 
   Description []
@@ -153,6 +325,7 @@ void Rtm_ManFree( Rtm_Man_t * p )
     Vec_PtrFree( p->vPis );
     Vec_PtrFree( p->vPos );
     Aig_MmFlexStop( p->pMem, 0 );
+    FREE( p->pExtra );
     free( p );
 }
 
@@ -171,10 +344,19 @@ int Rtm_ManLatchMax( Rtm_Man_t * p )
 {
     Rtm_Obj_t * pObj;
     Rtm_Edg_t * pEdge;
-    int nLatchMax = 0, i, k;
+    int nLatchMax = 0, i, k;//, c, Val;
     Rtm_ManForEachObj( p, pObj, i )
     Rtm_ObjForEachFaninEdge( pObj, pEdge, k )
+    {
+/*
+        for ( c = 0; c < (int)pEdge->nLats; c++ )
+        {
+            Val = Rtm_ObjGetOne( p, pEdge, c );
+            assert( Val == 1 || Val == 2 );
+        }
+*/
         nLatchMax = AIG_MAX( nLatchMax, (int)pEdge->nLats );
+    }
     return nLatchMax;
 }
 
@@ -264,6 +446,27 @@ int Rtm_ObjCheckRetimeFwd( Rtm_Obj_t * pObj )
   SeeAlso     []
 
 ***********************************************************************/
+int Rtm_ObjCheckRetimeBwd( Rtm_Obj_t * pObj )
+{
+    Rtm_Edg_t * pEdge;
+    int i;
+    Rtm_ObjForEachFanoutEdge( 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;
@@ -275,6 +478,26 @@ int Rtm_ObjGetDegreeFwd( Rtm_Obj_t * pObj )
 
 /**Function*************************************************************
 
+  Synopsis    [Check the possibility of forward retiming.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Rtm_ObjGetDegreeBwd( Rtm_Obj_t * pObj )
+{
+    Rtm_Obj_t * pFanout;
+    int i, Degree = 0;
+    Rtm_ObjForEachFanout( pObj, pFanout, i )
+        Degree = AIG_MAX( Degree, (int)pFanout->Num );
+    return Degree + 1;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Performs forward retiming.]
 
   Description []
@@ -284,7 +507,7 @@ int Rtm_ObjGetDegreeFwd( Rtm_Obj_t * pObj )
   SeeAlso     []
 
 ***********************************************************************/
-void Rtm_ObjRetimeFwd( Rtm_Obj_t * pObj )
+void Rtm_ObjRetimeFwd( Rtm_Man_t * pRtm, Rtm_Obj_t * pObj )
 {
     Rtm_Init_t ValTotal, ValCur;
     Rtm_Edg_t * pEdge;
@@ -294,17 +517,143 @@ void Rtm_ObjRetimeFwd( Rtm_Obj_t * pObj )
     ValTotal = RTM_VAL_ONE;
     Rtm_ObjForEachFaninEdge( pObj, pEdge, i )
     {
-        ValCur = Rtm_ObjRemFirst( pEdge );
+        ValCur = Rtm_ObjRemFirst( pRtm, 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 )
+        Rtm_ObjAddLast( pRtm, pEdge, ValTotal );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs forward retiming.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Rtm_ObjRetimeBwd( Rtm_Man_t * pRtm, Rtm_Obj_t * pObj )
+{
+    Rtm_Edg_t * pEdge;
+    int i;
+    assert( Rtm_ObjCheckRetimeBwd(pObj) );
+    // extract values and compute the result
+    Rtm_ObjForEachFanoutEdge( pObj, pEdge, i )
+        Rtm_ObjRemLast( pRtm, pEdge );
+    // insert the result in the fanout values
+    Rtm_ObjForEachFaninEdge( pObj, pEdge, i )
+        Rtm_ObjAddFirst( pRtm, pEdge, RTM_VAL_VOID );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Rtm_ObjMarkAutoFwd_rec( Rtm_Obj_t * pObj )
+{
+    Rtm_Obj_t * pFanout;
+    int i;
+    if ( pObj->fAuto )
+        return;
+    pObj->fAuto = 1;
+    Rtm_ObjForEachFanout( pObj, pFanout, i )
+        Rtm_ObjMarkAutoFwd_rec( pFanout );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Marks the nodes unreachable from the PIs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Rtm_ManMarkAutoFwd( Rtm_Man_t * pRtm )
+{
+    Rtm_Obj_t * pObjRtm;
+    int i, Counter = 0;
+    // mark nodes reachable from the PIs
+    pObjRtm = Vec_PtrEntry( pRtm->vObjs, 0 );
+    Rtm_ObjMarkAutoFwd_rec( pObjRtm );
+    Rtm_ManForEachPi( pRtm, pObjRtm, i )
+        Rtm_ObjMarkAutoFwd_rec( pObjRtm );
+    // count the number of autonomous nodes
+    Rtm_ManForEachObj( pRtm, pObjRtm, i )
     {
-        if ( pEdge->nLats >= 10 )
-            printf( "Rtm_ObjRetimeFwd(); More than 10 latches on the edge!\n" );
-        Rtm_ObjAddLast( pEdge, ValTotal );
+        pObjRtm->fAuto = !pObjRtm->fAuto;
+        Counter += pObjRtm->fAuto;
     }
+    // mark the fanins of the autonomous nodes
+    return Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Rtm_ObjMarkAutoBwd_rec( Rtm_Obj_t * pObj )
+{
+    Rtm_Obj_t * pFanin;
+    int i;
+    if ( pObj->fAuto )
+        return;
+    pObj->fAuto = 1;
+    Rtm_ObjForEachFanin( pObj, pFanin, i )
+        Rtm_ObjMarkAutoBwd_rec( pFanin );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Marks the nodes unreachable from the POs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Rtm_ManMarkAutoBwd( Rtm_Man_t * pRtm )
+{
+    Rtm_Obj_t * pObjRtm;
+    int i, Counter = 0;
+    // mark nodes reachable from the PIs
+    pObjRtm = Vec_PtrEntry( pRtm->vObjs, 0 );
+    pObjRtm->fAuto = 1;
+    Rtm_ManForEachPi( pRtm, pObjRtm, i )
+        pObjRtm->fAuto = 1;
+    Rtm_ManForEachPo( pRtm, pObjRtm, i )
+        Rtm_ObjMarkAutoBwd_rec( pObjRtm );
+    // count the number of autonomous nodes
+    Rtm_ManForEachObj( pRtm, pObjRtm, i )
+    {
+        pObjRtm->fAuto = !pObjRtm->fAuto;
+        Counter += pObjRtm->fAuto;
+    }
+    // mark the fanins of the autonomous nodes
+    return Counter;
 }
 
 /**Function*************************************************************
@@ -358,9 +707,6 @@ Rtm_Man_t * Rtm_ManFromAig( Aig_Man_t * p )
         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;
 }
 
@@ -375,7 +721,7 @@ Rtm_Man_t * Rtm_ManFromAig( Aig_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-Aig_Obj_t * Rtm_ManToAig_rec( Aig_Man_t * pNew, Rtm_Obj_t * pObjRtm, int * pLatches )
+Aig_Obj_t * Rtm_ManToAig_rec( Aig_Man_t * pNew, Rtm_Man_t * pRtm, Rtm_Obj_t * pObjRtm, int * pLatches )
 {
     Rtm_Edg_t * pEdge;
     Aig_Obj_t * pRes, * pFanin;
@@ -387,10 +733,10 @@ Aig_Obj_t * Rtm_ManToAig_rec( Aig_Man_t * pNew, Rtm_Obj_t * pObjRtm, int * pLatc
     Rtm_ObjForEachFaninEdge( pObjRtm, pEdge, k )
     {
         if ( pEdge->nLats == 0 )
-            pFanin = Rtm_ManToAig_rec( pNew, Rtm_ObjFanin(pObjRtm, k), pLatches );
+            pFanin = Rtm_ManToAig_rec( pNew, pRtm, Rtm_ObjFanin(pObjRtm, k), pLatches );
         else
         {
-            Val = Rtm_ObjGetFirst( pEdge );
+            Val = Rtm_ObjGetFirst( pRtm, pEdge );
             pFanin = Aig_ManPi( pNew, pLatches[2*pObjRtm->Id + k] + pEdge->nLats - 1 );
             pFanin = Aig_NotCond( pFanin, Val == RTM_VAL_ONE );
         }
@@ -438,7 +784,7 @@ Aig_Man_t * Rtm_ManToAig( Rtm_Man_t * pRtm )
         Aig_ObjCreatePi(pNew);
     // create internal nodes
     Rtm_ManForEachObj( pRtm, pObjRtm, i )
-        Rtm_ManToAig_rec( pNew, pObjRtm, pLatches );
+        Rtm_ManToAig_rec( pNew, pRtm, pObjRtm, pLatches );
     // create POs
     Rtm_ManForEachPo( pRtm, pObjRtm, i )
         Aig_ObjCreatePo( pNew, pObjRtm->pCopy );
@@ -451,7 +797,8 @@ Aig_Man_t * Rtm_ManToAig( Rtm_Man_t * pRtm )
         pObjNew = Rtm_ObjFanin( pObjRtm, k )->pCopy;
         for ( m = 0; m < (int)pEdge->nLats; m++ )
         {
-            Val = Rtm_ObjGetOne( pEdge, pEdge->nLats - 1 - m );
+            Val = Rtm_ObjGetOne( pRtm, pEdge, pEdge->nLats - 1 - m );
+            assert( Val == RTM_VAL_ZERO || Val == RTM_VAL_ONE || Val == RTM_VAL_VOID );
             pObjNew = Aig_NotCond( pObjNew, Val == RTM_VAL_ONE );
             Aig_ObjCreatePo( pNew, pObjNew );
             pObjNew = Aig_ManPi( pNew, pLatches[2*pObjRtm->Id + k] + m );
@@ -479,16 +826,33 @@ Aig_Man_t * Rtm_ManToAig( Rtm_Man_t * pRtm )
   SeeAlso     []
 
 ***********************************************************************/
-Aig_Man_t * Rtm_ManRetimeFwd( Aig_Man_t * p, int nStepsMax, int fVerbose )
+Aig_Man_t * Rtm_ManRetime( Aig_Man_t * p, int fForward, int nStepsMax, int fVerbose )
 {
     Vec_Ptr_t * vQueue;
     Aig_Man_t * pNew;
     Rtm_Man_t * pRtm;
-    Rtm_Obj_t * pObj, * pFanout;
+    Rtm_Obj_t * pObj, * pNext;
     Aig_Obj_t * pObjAig;
-    int i, k, Degree, DegreeMax = 0; 
+    int i, k, nAutos, Degree, DegreeMax = 0; 
+    int clk;
+
     // create the retiming manager
+clk = clock();
     pRtm = Rtm_ManFromAig( p );
+    // set registers
+    Aig_ManForEachLoSeq( p, pObjAig, i )
+        Rtm_ObjAddFirst( pRtm, Rtm_ObjEdge(pObjAig->pData, 0), fForward? RTM_VAL_ZERO : RTM_VAL_VOID );
+    // detect and mark the autonomous components
+    if ( fForward )
+        nAutos = Rtm_ManMarkAutoFwd( pRtm );
+    else
+        nAutos = Rtm_ManMarkAutoBwd( pRtm );
+    if ( fVerbose )
+    {
+        printf( "Detected %d autonomous objects. ", nAutos );
+        PRT( "Time", clock() - clk );
+    }
+
     // set the current retiming number
     Rtm_ManForEachObj( pRtm, pObj, i )
     {
@@ -497,13 +861,30 @@ Aig_Man_t * Rtm_ManRetimeFwd( Aig_Man_t * p, int nStepsMax, int fVerbose )
         pObj->Num = 0;
     }
 
+clk = clock();
     // put the LOs on the queue
     vQueue = Vec_PtrAlloc( 1000 );
-    Aig_ManForEachLoSeq( p, pObjAig, i )
+    if ( fForward )
+    {
+        Aig_ManForEachLoSeq( p, pObjAig, i )
+        {
+            pObj = pObjAig->pData;
+            if ( pObj->fAuto )
+                continue;
+            pObj->fMark = 1;
+            Vec_PtrPush( vQueue, pObj );
+        }
+    }
+    else
     {
-        pObj = pObjAig->pData;
-        pObj->fMark = 1;
-        Vec_PtrPush( vQueue, pObj );
+        Aig_ManForEachLiSeq( p, pObjAig, i )
+        {
+            pObj = pObjAig->pData;
+            if ( pObj->fAuto )
+                continue;
+            pObj->fMark = 1;
+            Vec_PtrPush( vQueue, pObj );
+        }
     }
     // perform retiming 
     DegreeMax = 0;
@@ -511,36 +892,69 @@ Aig_Man_t * Rtm_ManRetimeFwd( Aig_Man_t * p, int nStepsMax, int fVerbose )
     {
         pObj->fMark = 0;
         // retime the node 
-        Rtm_ObjRetimeFwd( pObj );
-        // check if its fanouts should be retimed
-        Rtm_ObjForEachFanout( pObj, pFanout, k )
+        if ( fForward )
         {
-            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 );
+            Rtm_ObjRetimeFwd( pRtm, pObj );
+            // check if its fanouts should be retimed
+            Rtm_ObjForEachFanout( pObj, pNext, k )
+            {
+                if ( pNext->fMark ) // skip aleady scheduled
+                    continue;
+                if ( pNext->Type ) // skip POs
+                    continue;
+                if ( !Rtm_ObjCheckRetimeFwd( pNext ) ) // skip non-retimable
+                    continue;
+                Degree = Rtm_ObjGetDegreeFwd( pNext );
+                DegreeMax = AIG_MAX( DegreeMax, Degree );
+                if ( Degree > nStepsMax ) // skip nodes with high degree
+                    continue;
+                pNext->fMark = 1;
+                pNext->Num = Degree;
+                Vec_PtrPush( vQueue, pNext );
+            }
+        }
+        else
+        {
+            Rtm_ObjRetimeBwd( pRtm, pObj );
+            // check if its fanouts should be retimed
+            Rtm_ObjForEachFanin( pObj, pNext, k )
+            {
+                if ( pNext->fMark ) // skip aleady scheduled
+                    continue;
+                if ( pNext->nFanins == 0 ) // skip PIs
+                    continue;
+                if ( !Rtm_ObjCheckRetimeBwd( pNext ) ) // skip non-retimable
+                    continue;
+                Degree = Rtm_ObjGetDegreeBwd( pNext );
+                DegreeMax = AIG_MAX( DegreeMax, Degree );
+                if ( Degree > nStepsMax ) // skip nodes with high degree
+                    continue;
+                pNext->fMark = 1;
+                pNext->Num = Degree;
+                Vec_PtrPush( vQueue, pNext );
+            }
         }
     }
 
     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) );
+    {
+        printf( "Performed %d %s latch moves of max depth %d and max latch count %d.\n", 
+            Vec_PtrSize(vQueue), fForward? "fwd":"bwd", DegreeMax, Rtm_ManLatchMax(pRtm) );
+        printf( "Memory usage = %d.  ", pRtm->nExtraCur );
+        PRT( "Time", clock() - clk );
+    }
     Vec_PtrFree( vQueue );
 
     // get the new manager
     pNew = Rtm_ManToAig( pRtm );
     Rtm_ManFree( pRtm );
     // group the registers
+clk = clock();
     pNew = Aig_ManReduceLaches( pNew, fVerbose );
+    if ( fVerbose )
+    {
+        PRT( "Register sharing time", clock() - clk );
+    }
     return pNew;
 }
 
diff --git a/src/aig/aig/aigSeq.c b/src/aig/aig/aigSeq.c
index 5bd5aaa5..d296d339 100644
--- a/src/aig/aig/aigSeq.c
+++ b/src/aig/aig/aigSeq.c
@@ -24,70 +24,6 @@
 ///                        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                         ///
 ////////////////////////////////////////////////////////////////////////
@@ -559,161 +495,6 @@ 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/aigTsim.c b/src/aig/aig/aigTsim.c
new file mode 100644
index 00000000..b8296cb2
--- /dev/null
+++ b/src/aig/aig/aigTsim.c
@@ -0,0 +1,436 @@
+/**CFile****************************************************************
+
+  FileName    [aigTsim.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [AIG package.]
+
+  Synopsis    [Ternary simulation.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - April 28, 2007.]
+
+  Revision    [$Id: aigTsim.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "aig.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+#define TSI_MAX_ROUNDS    10000
+
+#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" );
+}
+
+// simulation manager
+typedef struct Aig_Tsi_t_ Aig_Tsi_t;
+struct Aig_Tsi_t_
+{
+    Aig_Man_t *      pAig;              // the original AIG manager
+    // ternary state representation
+    int              nWords;            // the number of words in the states
+    Vec_Ptr_t *      vStates;           // the collection of ternary states
+    Aig_MmFixed_t *  pMem;              // memory for ternary states
+    // hash table for terminary states
+    unsigned **      pBins;
+    int              nBins;
+};
+
+static inline unsigned * Aig_TsiNext( unsigned * pState, int nWords )                      { return *((unsigned **)(pState + nWords));  }
+static inline void       Aig_TsiSetNext( unsigned * pState, int nWords, unsigned * pNext ) { *((unsigned **)(pState + nWords)) = pNext; }
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Allocates simulation manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Tsi_t * Aig_TsiStart( Aig_Man_t * pAig )
+{
+    Aig_Tsi_t * p;
+    p = (Aig_Tsi_t *)malloc( sizeof(Aig_Tsi_t) );
+    memset( p, 0, sizeof(Aig_Tsi_t) );
+    p->pAig    = pAig;
+    p->nWords  = Aig_BitWordNum( 2*Aig_ManRegNum(pAig) );
+    p->vStates = Vec_PtrAlloc( 1000 );
+    p->pMem    = Aig_MmFixedStart( sizeof(unsigned) * p->nWords + sizeof(unsigned *), 10000 );
+    p->nBins   = Aig_PrimeCudd(TSI_MAX_ROUNDS/2);
+    p->pBins   = ALLOC( unsigned *, p->nBins );
+    memset( p->pBins, 0, sizeof(unsigned *) * p->nBins );
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Deallocates simulation manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_TsiStop( Aig_Tsi_t * p )
+{
+    Aig_MmFixedStop( p->pMem, 0 );
+    Vec_PtrFree( p->vStates );
+    free( p->pBins );
+    free( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes hash value of the node using its simulation info.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Aig_TsiStateHash( unsigned * pState, int nWords, int nTableSize )
+{
+    static int s_FPrimes[128] = { 
+        1009, 1049, 1093, 1151, 1201, 1249, 1297, 1361, 1427, 1459, 
+        1499, 1559, 1607, 1657, 1709, 1759, 1823, 1877, 1933, 1997, 
+        2039, 2089, 2141, 2213, 2269, 2311, 2371, 2411, 2467, 2543, 
+        2609, 2663, 2699, 2741, 2797, 2851, 2909, 2969, 3037, 3089, 
+        3169, 3221, 3299, 3331, 3389, 3461, 3517, 3557, 3613, 3671, 
+        3719, 3779, 3847, 3907, 3943, 4013, 4073, 4129, 4201, 4243, 
+        4289, 4363, 4441, 4493, 4549, 4621, 4663, 4729, 4793, 4871, 
+        4933, 4973, 5021, 5087, 5153, 5227, 5281, 5351, 5417, 5471, 
+        5519, 5573, 5651, 5693, 5749, 5821, 5861, 5923, 6011, 6073, 
+        6131, 6199, 6257, 6301, 6353, 6397, 6481, 6563, 6619, 6689, 
+        6737, 6803, 6863, 6917, 6977, 7027, 7109, 7187, 7237, 7309, 
+        7393, 7477, 7523, 7561, 7607, 7681, 7727, 7817, 7877, 7933, 
+        8011, 8039, 8059, 8081, 8093, 8111, 8123, 8147
+    };
+    unsigned uHash;
+    int i;
+    uHash = 0;
+    for ( i = 0; i < nWords; i++ )
+        uHash ^= pState[i] * s_FPrimes[i & 0x7F];
+    return uHash % nTableSize;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Inserts value into the table.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Aig_TsiStateLookup( Aig_Tsi_t * p, unsigned * pState, int nWords )
+{
+    unsigned * pEntry;
+    int Hash;
+    Hash = Aig_TsiStateHash( pState, nWords, p->nBins );
+    for ( pEntry = p->pBins[Hash]; pEntry; pEntry = Aig_TsiNext(pEntry, nWords) )
+        if ( !memcmp( pEntry, pState, sizeof(unsigned) * nWords ) )
+            return 1;
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Inserts value into the table.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_TsiStateInsert( Aig_Tsi_t * p, unsigned * pState, int nWords )
+{
+    int Hash = Aig_TsiStateHash( pState, nWords, p->nBins );
+    assert( !Aig_TsiStateLookup( p, pState, nWords ) );
+    Aig_TsiSetNext( pState, nWords, p->pBins[Hash] );
+    p->pBins[Hash] = pState;    
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Inserts value into the table.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+unsigned * Aig_TsiStateNew( Aig_Tsi_t * p )
+{
+    unsigned * pState;
+    pState = (unsigned *)Aig_MmFixedEntryFetch( p->pMem );
+    memset( pState, 0, sizeof(unsigned) * p->nWords );
+    Vec_PtrPush( p->vStates, pState );
+    return pState;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Inserts value into the table.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_TsiStatePrint( Aig_Tsi_t * p, unsigned * pState )
+{
+    int i, Value, nZeros = 0, nOnes = 0, nDcs = 0;
+    for ( i = 0; i < Aig_ManRegNum(p->pAig); i++ )
+    {
+        Value = (Aig_InfoHasBit( pState, 2 * i + 1 ) << 1) | Aig_InfoHasBit( pState, 2 * i );
+        if ( Value == 1 )
+            printf( "0" ), nZeros++;
+        else if ( Value == 2 )
+            printf( "1" ), nOnes++;
+        else if ( Value == 3 )
+            printf( "x" ), nDcs++;
+        else
+            assert( 0 );
+    }
+    printf( " (0=%5d, 1=%5d, x=%5d)\n", nZeros, nOnes, nDcs );
+}
+
+
+/**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 )
+{
+    Aig_Tsi_t * pTsi;
+    Vec_Ptr_t * vMap;
+    Aig_Obj_t * pObj, * pObjLi, * pObjLo;
+    unsigned * pState, * pPrev;
+    int i, k, f, fConstants, Value, nCounter;
+    // allocate the simulation manager
+    pTsi = Aig_TsiStart( p );
+    // 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 < TSI_MAX_ROUNDS; f++ )
+    {
+        // collect this state
+        pState = Aig_TsiStateNew( pTsi );
+        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_TsiStatePrint( pTsi, pState );
+        // check if this state exists
+        if ( Aig_TsiStateLookup( pTsi, pState, pTsi->nWords ) )
+            break;
+        // insert this state
+        Aig_TsiStateInsert( pTsi, pState, pTsi->nWords );
+        // 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 == TSI_MAX_ROUNDS )
+    {
+        printf( "Aig_ManTernarySimulate(): Did not reach a fixed point after %d iterations.\n", TSI_MAX_ROUNDS );
+        Aig_TsiStop( pTsi );
+        return NULL;
+    }
+    // OR all the states
+    pState = Vec_PtrEntry( pTsi->vStates, 0 );
+    Vec_PtrForEachEntry( pTsi->vStates, pPrev, i )
+    {
+        for ( k = 0; k < pTsi->nWords; k++ )
+            pState[k] |= pPrev[k];
+    }
+    // check if there are constants
+    fConstants = 0;
+    if ( 2*Aig_ManRegNum(p) == 32*pTsi->nWords )
+    {
+        for ( i = 0; i < pTsi->nWords; i++ )
+            if ( pState[i] != ~0 )
+                fConstants = 1;
+    }
+    else
+    {
+        for ( i = 0; i < pTsi->nWords - 1; i++ )
+            if ( pState[i] != ~0 )
+                fConstants = 1;
+        if ( pState[i] != Aig_InfoMask( 2*Aig_ManRegNum(p) - 32*(pTsi->nWords-1) ) )
+            fConstants = 1;
+    }
+    if ( fConstants == 0 )
+    {
+        Aig_TsiStop( pTsi );
+        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" );
+    Aig_TsiStop( pTsi );
+    if ( fVerbose )
+    printf( "Detected %d constants after %d iterations of ternary simulation.\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 93b25e4a..45ed62ee 100644
--- a/src/aig/aig/module.make
+++ b/src/aig/aig/module.make
@@ -13,5 +13,6 @@ SRC +=    src/aig/aig/aigCheck.c \
     src/aig/aig/aigTable.c \
     src/aig/aig/aigTiming.c \
     src/aig/aig/aigTruth.c \
+    src/aig/aig/aigTsim.c \
     src/aig/aig/aigUtil.c \
     src/aig/aig/aigWin.c
\ No newline at end of file
diff --git a/src/aig/fra/fra.h b/src/aig/fra/fra.h
index c8617d84..217d1fba 100644
--- a/src/aig/fra/fra.h
+++ b/src/aig/fra/fra.h
@@ -73,6 +73,7 @@ struct Fra_Par_t_
     int              nBTLimitMiter;     // conflict limit at an output
     int              nFramesP;          // the number of timeframes to in the prefix
     int              nFramesK;          // the number of timeframes to unroll
+    int              nMaxImps;          // the maximum number of implications to consider
     int              fRewrite;          // use rewriting for constraint reduction
     int              fLatchCorr;        // computes latch correspondence only
     int              fUseImps;          // use implications
@@ -133,6 +134,7 @@ struct Fra_Man_t_
     // counter example storage
     int              nPatWords;         // the number of words in the counter example
     unsigned *       pPatWords;         // the counter example
+    Vec_Int_t *      vCex;
     // satisfiability solving
     sat_solver *     pSat;              // SAT solver
     int              nSatVars;          // the number of variables currently used
@@ -226,6 +228,8 @@ 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 );
 extern void                Fra_ClassesPostprocess( Fra_Cla_t * p );
+extern void                Fra_ClassesSelectRepr( Fra_Cla_t * p );
+extern Aig_Man_t *         Fra_ClassesDeriveAig( Fra_Cla_t * p, int nFramesK );
 /*=== fraCnf.c ========================================================*/
 extern void                Fra_CnfNodeAddToSolver( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew );
 /*=== fraCore.c ========================================================*/
@@ -240,7 +244,7 @@ extern int                 Fra_ImpCheckForNode( Fra_Man_t * p, Vec_Int_t * vImps
 extern int                 Fra_ImpRefineUsingCex( Fra_Man_t * p, Vec_Int_t * vImps );
 extern void                Fra_ImpCompactArray( Vec_Int_t * vImps );
 /*=== fraInd.c ========================================================*/
-extern Aig_Man_t *         Fra_FraigInduction( Aig_Man_t * p, int nFramesP, int nFramesK, int fRewrite, int fUseImps, int fLatchCorr, int fVerbose, int * pnIter );
+extern Aig_Man_t *         Fra_FraigInduction( Aig_Man_t * p, int nFramesP, int nFramesK, int nMaxImps, int fRewrite, int fUseImps, int fLatchCorr, int fVerbose, int * pnIter );
 /*=== fraMan.c ========================================================*/
 extern void                Fra_ParamsDefault( Fra_Par_t * pParams );
 extern void                Fra_ParamsDefaultSeq( Fra_Par_t * pParams );
diff --git a/src/aig/fra/fraClass.c b/src/aig/fra/fraClass.c
index a9d727da..d6db125b 100644
--- a/src/aig/fra/fraClass.c
+++ b/src/aig/fra/fraClass.c
@@ -114,9 +114,18 @@ void Fra_ClassesCopyReprs( Fra_Cla_t * p, Vec_Ptr_t * vFailed )
     int i;
     Aig_ManReprStart( p->pAig, Aig_ManObjIdMax(p->pAig) + 1 );
     memmove( p->pAig->pReprs, p->pMemRepr, sizeof(Aig_Obj_t *) * (Aig_ManObjIdMax(p->pAig) + 1) );
+    if ( Vec_PtrSize(p->vClasses1) == 0 && Vec_PtrSize(p->vClasses) == 0 )
+    {
+        Aig_ManForEachObj( p->pAig, pObj, i )
+        {
+            if ( p->pAig->pReprs[i] != NULL )
+                printf( "Classes are not cleared!\n" );
+            assert( p->pAig->pReprs[i] == NULL );
+        }
+    }
     if ( vFailed )
-    Vec_PtrForEachEntry( vFailed, pObj, i )
-        p->pAig->pReprs[pObj->Id] = NULL;
+        Vec_PtrForEachEntry( vFailed, pObj, i )
+            p->pAig->pReprs[pObj->Id] = NULL;
 }
 
 /**Function*************************************************************
@@ -206,7 +215,7 @@ void Fra_PrintClass( Aig_Obj_t ** pClass )
         assert( Fra_ClassObjRepr(pTemp) == pClass[0] );
     printf( "{ " );
     for ( i = 0; pTemp = pClass[i]; i++ )
-        printf( "%d ", pTemp->Id, Fra_ClassObjRepr(pTemp)? Fra_ClassObjRepr(pTemp)->Id : -1 );
+        printf( "%d(%d) ", pTemp->Id, pTemp->Level );
     printf( "}\n" );
 }
 
@@ -227,8 +236,11 @@ void Fra_ClassesPrint( Fra_Cla_t * p, int fVeryVerbose )
     Aig_Obj_t * pObj;
     int i;
 
-    printf( "Const = %5d. Class = %5d. Lit = %5d.\n", 
+    printf( "Const = %5d. Class = %5d. Lit = %5d. ", 
         Vec_PtrSize(p->vClasses1), Vec_PtrSize(p->vClasses), Fra_ClassesCountLits(p) );
+    if ( p->vImps && Vec_IntSize(p->vImps) > 0 )
+        printf( "Imp = %5d. ", Vec_IntSize(p->vImps) );
+    printf( "\n" );
 
     if ( fVeryVerbose )
     {
@@ -283,10 +295,10 @@ void Fra_ClassesPrepare( Fra_Cla_t * p, int fLatchCorr )
         {
             if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsPi(pObj) )
                 continue;
+            // skip the node with more that the given number of levels
+//            if ( pObj->Level > 3 )
+//                continue;
         }
-//printf( "%3d : ", pObj->Id );
-//Extra_PrintBinary( stdout, Fra_ObjSim(pObj), 32 );
-//printf( "\n" );
         // hash the node by its simulation info
         iEntry = p->pFuncNodeHash( pObj, nTableSize );
         // check if the node belongs to the class of constant 1
@@ -494,7 +506,6 @@ int Fra_ClassesRefine( Fra_Cla_t * p )
     vTemp = p->vClassesTemp;
     p->vClassesTemp = p->vClasses;
     p->vClasses = vTemp;
-    p->fRefinement = (nRefis > 0);
     return nRefis;
 }
 
@@ -531,7 +542,6 @@ int Fra_ClassesRefine1( Fra_Cla_t * p )
     Vec_PtrShrink( p->vClasses1, k );
     if ( Vec_PtrSize(p->vClassNew) == 0 )
         return 0;
-    p->fRefinement = 1;
 /*
     printf( "Refined const-1 class: {" );
     Vec_PtrForEachEntry( p->vClassNew, pObj, i )
@@ -677,6 +687,95 @@ void Fra_ClassesPostprocess( Fra_Cla_t * p )
 
 /**Function*************************************************************
 
+  Synopsis    [Postprocesses the classes by selecting representative lowest in top order.]
+
+  Description []
+               
+  SideEffects [] 
+
+  SeeAlso     []
+
+***********************************************************************/
+void Fra_ClassesSelectRepr( Fra_Cla_t * p )
+{
+    Aig_Obj_t ** pClass, * pNodeMin;
+    int i, c, cMinSupp, nSuppSizeMin, nSuppSizeCur;
+    // reassign representatives in each class
+    Vec_PtrForEachEntry( p->vClasses, pClass, i )
+    {
+        // collect support sizes and find the min-support node
+        pNodeMin = NULL;
+        nSuppSizeMin = AIG_INFINITY;
+        for ( c = 0; pClass[c]; c++ )
+        {
+            nSuppSizeCur = Aig_SupportSize( p->pAig, pClass[c] );
+//            nSuppSizeCur = 1;
+            if ( nSuppSizeMin > nSuppSizeCur || 
+                (nSuppSizeMin == nSuppSizeCur && pNodeMin->Level > pClass[c]->Level) )
+            {
+                nSuppSizeMin = nSuppSizeCur;
+                pNodeMin = pClass[c];
+                cMinSupp = c; 
+            }
+        }
+        // skip the case when the repr did not change
+        if ( cMinSupp == 0 )
+            continue;
+        // make the new node the representative of the class
+        pClass[cMinSupp] = pClass[0];
+        pClass[0] = pNodeMin;
+        // set the representative
+        for ( c = 0; pClass[c]; c++ )
+            Fra_ClassObjSetRepr( pClass[c], c? pClass[0] : NULL );
+    }
+}
+
+
+
+static inline Aig_Obj_t * Fra_ObjEqu( Aig_Obj_t ** ppEquivs, Aig_Obj_t * pObj )                       { return ppEquivs[pObj->Id];  }
+static inline void        Fra_ObjSetEqu( Aig_Obj_t ** ppEquivs, Aig_Obj_t * pObj, Aig_Obj_t * pNode ) { ppEquivs[pObj->Id] = pNode; }
+
+static inline Aig_Obj_t * Fra_ObjChild0Equ( Aig_Obj_t ** ppEquivs, Aig_Obj_t * pObj ) { return Aig_NotCond(Fra_ObjEqu(ppEquivs,Aig_ObjFanin0(pObj)), Aig_ObjFaninC0(pObj));  }
+static inline Aig_Obj_t * Fra_ObjChild1Equ( Aig_Obj_t ** ppEquivs, Aig_Obj_t * pObj ) { return Aig_NotCond(Fra_ObjEqu(ppEquivs,Aig_ObjFanin1(pObj)), Aig_ObjFaninC1(pObj));  }
+
+/**Function*************************************************************
+
+  Synopsis    [Add the node and its constraints to the new AIG.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Fra_ClassesDeriveNode( Aig_Man_t * pManFraig, Aig_Obj_t * pObj, Aig_Obj_t ** ppEquivs )
+{
+    Aig_Obj_t * pObjNew, * pObjRepr, * pObjReprNew, * pMiter;//, * pObjNew2;
+    // skip nodes without representative
+    if ( (pObjRepr = Fra_ClassObjRepr(pObj)) == NULL )
+        return;
+    assert( pObjRepr->Id < pObj->Id );
+    // get the new node 
+    pObjNew = Fra_ObjEqu( ppEquivs, pObj );
+    // get the new node of the representative
+    pObjReprNew = Fra_ObjEqu( ppEquivs, pObjRepr );
+    // if this is the same node, no need to add constraints
+    if ( Aig_Regular(pObjNew) == Aig_Regular(pObjReprNew) )
+        return;
+    // these are different nodes - perform speculative reduction
+//    pObjNew2 = Aig_NotCond( pObjReprNew, pObj->fPhase ^ pObjRepr->fPhase );
+    // set the new node
+//    Fra_ObjSetEqu( ppEquivs, pObj, pObjNew2 );
+    // add the constraint
+    pMiter = Aig_Exor( pManFraig, Aig_Regular(pObjNew), Aig_Regular(pObjReprNew) );
+    pMiter = Aig_NotCond( pMiter, Aig_Regular(pMiter)->fPhase ^ Aig_IsComplement(pMiter) );
+    pMiter = Aig_Not( pMiter );
+    Aig_ObjCreatePo( pManFraig, pMiter );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Derives AIG for the partitioned problem.]
 
   Description []
@@ -688,7 +787,60 @@ void Fra_ClassesPostprocess( Fra_Cla_t * p )
 ***********************************************************************/
 Aig_Man_t * Fra_ClassesDeriveAig( Fra_Cla_t * p, int nFramesK )
 {
-
+    Aig_Man_t * pManFraig;
+    Aig_Obj_t * pObj, * pObjNew;
+    Aig_Obj_t ** pLatches, ** ppEquivs;
+    int i, k, f, nFramesAll = nFramesK + 1;
+    assert( Aig_ManRegNum(p->pAig) > 0 );
+    assert( Aig_ManRegNum(p->pAig) < Aig_ManPiNum(p->pAig) );
+    assert( nFramesK > 0 );
+    // start the fraig package
+    pManFraig = Aig_ManStart( (Aig_ManObjIdMax(p->pAig) + 1) * nFramesAll );
+    // allocate place for the node mapping
+    ppEquivs = ALLOC( Aig_Obj_t *, Aig_ManObjIdMax(p->pAig) + 1 );
+    Fra_ObjSetEqu( ppEquivs, Aig_ManConst1(p->pAig), Aig_ManConst1(pManFraig) );
+    // create latches for the first frame
+    Aig_ManForEachLoSeq( p->pAig, pObj, i )
+        Fra_ObjSetEqu( ppEquivs, pObj, Aig_ObjCreatePi(pManFraig) );
+    // add timeframes
+    pLatches = ALLOC( Aig_Obj_t *, Aig_ManRegNum(p->pAig) );
+    for ( f = 0; f < nFramesAll; f++ )
+    {
+        // create PIs for this frame
+        Aig_ManForEachPiSeq( p->pAig, pObj, i )
+            Fra_ObjSetEqu( ppEquivs, pObj, Aig_ObjCreatePi(pManFraig) );
+        // set the constraints on the latch outputs
+        Aig_ManForEachLoSeq( p->pAig, pObj, i )
+            Fra_ClassesDeriveNode( pManFraig, pObj, ppEquivs );
+        // add internal nodes of this frame
+        Aig_ManForEachNode( p->pAig, pObj, i )
+        {
+            pObjNew = Aig_And( pManFraig, Fra_ObjChild0Equ(ppEquivs, pObj), Fra_ObjChild1Equ(ppEquivs, pObj) );
+            Fra_ObjSetEqu( ppEquivs, pObj, pObjNew );
+            Fra_ClassesDeriveNode( pManFraig, pObj, ppEquivs );
+        }
+        if ( f == nFramesAll - 1 )
+            break;
+        if ( f == nFramesAll - 2 )
+            pManFraig->nAsserts = Aig_ManPoNum(pManFraig);
+        // save the latch input values
+        k = 0;
+        Aig_ManForEachLiSeq( p->pAig, pObj, i )
+            pLatches[k++] = Fra_ObjChild0Equ( ppEquivs, pObj );
+        // insert them to the latch output values
+        k = 0;
+        Aig_ManForEachLoSeq( p->pAig, pObj, i )
+            Fra_ObjSetEqu( ppEquivs, pObj, pLatches[k++] );
+    }
+    free( pLatches );
+    free( ppEquivs );
+    // mark the asserts
+    assert( Aig_ManPoNum(pManFraig) % nFramesAll == 0 );
+printf( "Assert miters = %6d. Output miters = %6d.\n", 
+       pManFraig->nAsserts, Aig_ManPoNum(pManFraig) - pManFraig->nAsserts );
+    // remove dangling nodes
+    Aig_ManCleanup( pManFraig );
+    return pManFraig;
 }
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/fra/fraCore.c b/src/aig/fra/fraCore.c
index 3c76af03..9adbb7a9 100644
--- a/src/aig/fra/fraCore.c
+++ b/src/aig/fra/fraCore.c
@@ -24,6 +24,23 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
+/* 
+    Speculating reduction in the sequential case leads to an interesting 
+    situation when a counter-ex may not refine any classes. This happens
+    for non-constant equivalence classes. In such cases the representative
+    of the class (proved by simulation to be non-constant) may be reduced 
+    to a constant during the speculative reduction. The fraig-representative 
+    of this representative node is a constant node, even though this is a 
+    non-constant class. Experiments have shown that this situation happens 
+    very often at the beginning of the refinement iteration when there are 
+    many spurious candidate equivalence classes (especially if heavy-duty 
+    simulatation of BMC was node used at the beginning). As a result, the 
+    SAT solver run may return a counter-ex that  distinguishes the given 
+    representative node from the constant-1 node but this counter-ex
+    does not distinguish the nodes in the non-costant class... This is why 
+    there is no check of refinment after a counter-ex in the sequential case.
+*/
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
@@ -117,6 +134,54 @@ static inline void Fra_FraigNodeSpeculate( Fra_Man_t * p, Aig_Obj_t * pObj, Aig_
 
 /**Function*************************************************************
 
+  Synopsis    [Verifies the generated counter-ex.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Fra_FraigVerifyCounterEx( Fra_Man_t * p, Vec_Int_t * vCex )
+{
+    Aig_Obj_t * pObj, ** ppClass;
+    int i, c;
+    assert( Aig_ManPiNum(p->pManAig) == Vec_IntSize(vCex) );
+    // make sure the input pattern is not used
+    Aig_ManForEachObj( p->pManAig, pObj, i )
+        assert( !pObj->fMarkB );
+    // simulate the cex through the AIG
+    Aig_ManConst1(p->pManAig)->fMarkB = 1;
+    Aig_ManForEachPi( p->pManAig, pObj, i )
+        pObj->fMarkB = Vec_IntEntry(vCex, i);
+    Aig_ManForEachNode( p->pManAig, pObj, i )
+        pObj->fMarkB = (Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj)) & 
+                       (Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj));
+    Aig_ManForEachPo( p->pManAig, pObj, i )
+        pObj->fMarkB = Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj);
+    // check if the classes hold
+    Vec_PtrForEachEntry( p->pCla->vClasses1, pObj, i )
+    {
+        if ( pObj->fPhase != pObj->fMarkB )
+            printf( "The node %d is not constant under cex!\n", pObj->Id );
+    }
+    Vec_PtrForEachEntry( p->pCla->vClasses, ppClass, i )
+    {
+        for ( c = 1; ppClass[c]; c++ )
+            if ( (ppClass[0]->fPhase ^ ppClass[c]->fPhase) != (ppClass[0]->fMarkB ^ ppClass[c]->fMarkB) )
+                printf( "The nodes %d and %d are not equal under cex!\n", ppClass[0]->Id, ppClass[c]->Id );
+//        for ( c = 0; ppClass[c]; c++ )
+//            if ( Fra_ObjFraig(ppClass[c],p->pPars->nFramesK) == Aig_ManConst1(p->pManFraig) )
+//                printf( "A member of non-constant class has a constant repr!\n" );
+    }
+    // clean the simulation pattern
+    Aig_ManForEachObj( p->pManAig, pObj, i )
+        pObj->fMarkB = 0;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Performs fraiging for one node.]
 
   Description [Returns the fraiged node.]
@@ -173,47 +238,20 @@ static inline void Fra_FraigNode( Fra_Man_t * p, Aig_Obj_t * pObj )
         Fra_FraigNodeSpeculate( p, pObj, Aig_Regular(pObjFraig), Aig_Regular(pObjReprFraig) );
         return;
     }
-//printf( "Disproved %d and %d.\n", pObj->Id, pObjRepr->Id );
     // disprove the nodes
+    p->pCla->fRefinement = 1;
     // if we do not include the node into those disproved, we may end up 
     // merging this node with another representative, for which proof has timed out
     if ( p->vTimeouts )
         Vec_PtrPush( p->vTimeouts, pObj );
+    // verify that the counter-example satisfies all the constraints
+//    if ( p->vCex )
+//    Fra_FraigVerifyCounterEx( p, p->vCex );
     // simulate the counter-example and return the Fraig node
     Fra_SmlResimulate( p );
-/*
-printf( "%d -> %d.\n", pObj->Id, pObjRepr->Id );
-Fra_ClassesPrint( p->pCla, 1 );
-printf( "%3d : ", 19 );
-Extra_PrintBinary( stdout, Fra_ObjSim(p->pSml, 19), 32 * p->pSml->nWordsTotal );
-printf( "\n" );
-printf( "%3d : ", 27 );
-Extra_PrintBinary( stdout, Fra_ObjSim(p->pSml, 27), 32 * p->pSml->nWordsTotal );
-printf( "\n" );
-printf( "%3d : ", 30 );
-Extra_PrintBinary( stdout, Fra_ObjSim(p->pSml, 30), 32 * p->pSml->nWordsTotal );
-printf( "\n" );
-printf( "\n\n" );
-*/
-    if ( Fra_ClassObjRepr(pObj) == pObjRepr )
-    {
-/*
-//Fra_ClassesPrint( p->pCla, 1 );
-//printf( "\n\n" );
-printf( "%3d : ", pObj->Id );
-Extra_PrintBinary( stdout, Fra_ObjSim(p->pSml, pObj->Id), 32 * p->pSml->nWordsTotal );
-printf( "\n" );
-printf( "%3d : ", pObjRepr->Id );
-Extra_PrintBinary( stdout, Fra_ObjSim(p->pSml, pObjRepr->Id), 32 * p->pSml->nWordsTotal );
-printf( "\n" );
-*/
-        if ( Aig_ObjIsPi(pObj) )
-            printf( "primary input\n" );
-        else
-            printf( "NOT primary input\n" );
+    if ( !p->pPars->nFramesK && Fra_ClassObjRepr(pObj) == pObjRepr )
         printf( "Fra_FraigNode(): Error in class refinement!\n" );
-    }
-    assert( Fra_ClassObjRepr(pObj) != pObjRepr );
+    assert( p->pPars->nFramesK || Fra_ClassObjRepr(pObj) != pObjRepr );
 }
 
 /**Function*************************************************************
diff --git a/src/aig/fra/fraImp.c b/src/aig/fra/fraImp.c
index 25b34e03..8af11b78 100644
--- a/src/aig/fra/fraImp.c
+++ b/src/aig/fra/fraImp.c
@@ -205,7 +205,7 @@ Vec_Ptr_t * Fra_SmlSortUsingOnes( Fra_Sml_t * p, int fLatchCorr )
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Int_t * Fra_SmlSelectMaxCost( Vec_Int_t * vImps, int * pCosts, int nCostMax, int nImpLimit )
+Vec_Int_t * Fra_SmlSelectMaxCost( Vec_Int_t * vImps, int * pCosts, int nCostMax, int nImpLimit, int * pCostRange )
 {
     Vec_Int_t * vImpsNew;
     int * pCostCount, nImpCount, Imp, i, c;
@@ -239,6 +239,8 @@ Vec_Int_t * Fra_SmlSelectMaxCost( Vec_Int_t * vImps, int * pCosts, int nCostMax,
             break;
     }
     free( pCostCount );
+    if ( pCostRange )
+        *pCostRange = c;
     return vImpsNew;
 }
 
@@ -290,7 +292,7 @@ Vec_Int_t * Fra_ImpDerive( Fra_Man_t * p, int nImpMaxLimit, int nImpUseLimit, in
     int * pImpCosts, * pNodesI, * pNodesK;
     int nImpsTotal = 0, nImpsTried = 0, nImpsNonSeq = 0, nImpsComb = 0, nImpsCollected = 0;
     int CostMin = AIG_INFINITY, CostMax = 0;
-    int i, k, Imp, clk = clock();
+    int i, k, Imp, CostRange, clk = clock();
     assert( nImpMaxLimit > 0 && nImpUseLimit > 0 && nImpUseLimit <= nImpMaxLimit );
     // normalize both managers
     pComb = Fra_SmlSimulateComb( p->pManAig, nSimWords );
@@ -350,9 +352,10 @@ finish:
     Fra_SmlStop( pSeq );
 
     // select implications with the highest cost
+    CostRange = CostMin;
     if ( Vec_IntSize(vImps) > nImpUseLimit )
     {
-        vImps = Fra_SmlSelectMaxCost( vTemp = vImps, pImpCosts, nSimWords * 32, nImpUseLimit );
+        vImps = Fra_SmlSelectMaxCost( vTemp = vImps, pImpCosts, nSimWords * 32, nImpUseLimit, &CostRange );
         Vec_IntFree( vTemp );  
     }
 
@@ -365,8 +368,8 @@ finish:
             (int (*)(const void *, const void *)) Sml_CompareMaxId );
 if ( p->pPars->fVerbose )
 {
-printf( "Tot = %d. Try = %d. NonS = %d. C = %d. Found = %d.  Cost = [%d - %d]  ", 
-    nImpsTotal, nImpsTried, nImpsNonSeq, nImpsComb, nImpsCollected, CostMin, CostMax );
+printf( "Tot = %d. Try = %d. NonS = %d. C = %d. Found = %d.  Cost = [%d < %d < %d] ", 
+    nImpsTotal, nImpsTried, nImpsNonSeq, nImpsComb, nImpsCollected, CostMin, CostRange, CostMax );
 PRT( "Time", clock() - clk );
 }
     return vImps;
@@ -381,7 +384,7 @@ PRT( "Time", clock() - clk );
 
   Synopsis    [Add implication clauses to the SAT solver.]
 
-  Description []
+  Description [Note that implications should be checked in the first frame!]
                
   SideEffects []
 
@@ -540,7 +543,6 @@ int Fra_ImpRefineUsingCex( Fra_Man_t * p, Vec_Int_t * vImps )
         {
             Vec_IntWriteEntry( vImps, i, 0 );
             RetValue = 1;
-            p->pCla->fRefinement = 1;
         }
     }
     return RetValue;
diff --git a/src/aig/fra/fraInd.c b/src/aig/fra/fraInd.c
index d754f3ae..6d8305c0 100644
--- a/src/aig/fra/fraInd.c
+++ b/src/aig/fra/fraInd.c
@@ -50,11 +50,9 @@ void Fra_FraigInductionRewrite( Fra_Man_t * p )
     pTemp = Aig_ManDup( p->pManFraig, 0 );
 //    pTemp = Dar_ManRwsat( pTemp, 1, 0 );
     pTemp = Dar_ManRewriteDefault( pTemp );
-
 //    printf( "Before = %6d.  After = %6d.\n", Aig_ManNodeNum(p->pManFraig), Aig_ManNodeNum(pTemp) ); 
 //Aig_ManDumpBlif( p->pManFraig, "1.blif" );
 //Aig_ManDumpBlif( pTemp, "2.blif" );
-
 //    Fra_FramesWriteCone( pTemp );
 //    Aig_ManStop( pTemp );
     // transfer PI/register pointers
@@ -128,8 +126,7 @@ static inline void Fra_FramesConstrainNode( Aig_Man_t * pManFraig, Aig_Obj_t * p
 Aig_Man_t * Fra_FramesWithClasses( Fra_Man_t * p )
 {
     Aig_Man_t * pManFraig;
-    Aig_Obj_t * pObj, * pObjNew;
-    Aig_Obj_t ** pLatches;
+    Aig_Obj_t * pObj, * pObjLi, * pObjLo, * pObjNew;
     int i, k, f;
     assert( p->pManFraig == NULL );
     assert( Aig_ManRegNum(p->pManAig) > 0 );
@@ -149,7 +146,6 @@ Aig_Man_t * Fra_FramesWithClasses( Fra_Man_t * p )
         Fra_ObjSetFraig( pObj, 0, Aig_ObjCreatePi(pManFraig) );
 
     // add timeframes
-    pLatches = ALLOC( Aig_Obj_t *, Aig_ManRegNum(p->pManAig) );
     for ( f = 0; f < p->nFramesAll - 1; f++ )
     {
         // set the constraints on the latch outputs
@@ -162,23 +158,15 @@ Aig_Man_t * Fra_FramesWithClasses( Fra_Man_t * p )
             Fra_ObjSetFraig( pObj, f, pObjNew );
             Fra_FramesConstrainNode( pManFraig, pObj, f );
         }
-        // save the latch input values
-        k = 0;
-        Aig_ManForEachLiSeq( p->pManAig, pObj, i )
-            pLatches[k++] = Fra_ObjChild0Fra(pObj,f);
-        assert( k == Aig_ManRegNum(p->pManAig) );
-        // insert them to the latch output values
-        k = 0;
-        Aig_ManForEachLoSeq( p->pManAig, pObj, i )
-            Fra_ObjSetFraig( pObj, f+1, pLatches[k++] );
-        assert( k == Aig_ManRegNum(p->pManAig) );
+        // transfer latch input to the latch outputs 
+        Aig_ManForEachLiLoSeq( p->pManAig, pObjLi, pObjLo, k )
+            Fra_ObjSetFraig( pObjLo, f+1, Fra_ObjChild0Fra(pObjLi,f) );
     }
-    free( pLatches );
     // mark the asserts
     pManFraig->nAsserts = Aig_ManPoNum(pManFraig);
-    // add the POs for the latch inputs
-    Aig_ManForEachLiSeq( p->pManAig, pObj, i )
-        Aig_ObjCreatePo( pManFraig, Fra_ObjChild0Fra(pObj,f-1) );
+    // add the POs for the latch outputs of the last frame
+    Aig_ManForEachLoSeq( p->pManAig, pObj, i )
+        Aig_ObjCreatePo( pManFraig, Fra_ObjFraig(pObj,p->nFramesAll-1) );
 
     // remove dangling nodes
     Aig_ManCleanup( pManFraig );
@@ -198,7 +186,7 @@ Aig_Man_t * Fra_FramesWithClasses( Fra_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesP, int nFramesK, int fRewrite, int fUseImps, int fLatchCorr, int fVerbose, int * pnIter )
+Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesP, int nFramesK, int nMaxImps, int fRewrite, int fUseImps, int fLatchCorr, int fVerbose, int * pnIter )
 {
     int fUseSimpleCnf = 0;
     int fUseOldSimulation = 0;
@@ -229,6 +217,7 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesP, int nFramesK,
     Fra_ParamsDefaultSeq( pPars );
     pPars->nFramesP   = nFramesP;
     pPars->nFramesK   = nFramesK;
+    pPars->nMaxImps   = nMaxImps;
     pPars->fVerbose   = fVerbose;
     pPars->fRewrite   = fRewrite;
     pPars->fLatchCorr = fLatchCorr;
@@ -249,9 +238,16 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesP, int nFramesK,
     }
     else
     {
+        // bug:  r iscas/blif/s5378.blif    ; st; ssw -v
         // bug:  r iscas/blif/s1238.blif    ; st; ssw -v
         // refine the classes with more simulation rounds
-        p->pSml = Fra_SmlSimulateSeq( pManAig, pPars->nFramesP, 32, 2 ); //pPars->nFramesK + 1, 6 );  // 32, 2 );
+if ( fVerbose )
+printf( "Simulating %d AIG nodes for %d cycles ... ", Aig_ManNodeNum(pManAig), pPars->nFramesP + 32 );
+        p->pSml = Fra_SmlSimulateSeq( pManAig, pPars->nFramesP, 32, 1 ); //pPars->nFramesK + 1, 1 );  
+if ( fVerbose ) 
+{
+PRT( "Time", clock() - clk );
+}
         Fra_ClassesPrepare( p->pCla, p->pPars->fLatchCorr );
 //        Fra_ClassesPostprocess( p->pCla );
         // allocate new simulation manager for simulating counter-examples
@@ -259,19 +255,26 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesP, int nFramesK,
         p->pSml = Fra_SmlStart( pManAig, 0, pPars->nFramesK + 1, pPars->nSimWords );
     }
 
-    // perform BMC
-    Fra_BmcPerform( p, pPars->nFramesP, pPars->nFramesK + 1 );
+    // perform BMC (for the min number of frames)
+    Fra_BmcPerform( p, pPars->nFramesP, pPars->nFramesK );
 //Fra_ClassesPrint( p->pCla, 1 );
+//    p->vCex = Vec_IntAlloc( 1000 );
 
     // select the most expressive implications
     if ( pPars->fUseImps )
-        p->pCla->vImps = Fra_ImpDerive( p, 5000000, 5000, pPars->fLatchCorr );
+        p->pCla->vImps = Fra_ImpDerive( p, 5000000, pPars->nMaxImps, pPars->fLatchCorr );
  
     p->nLitsZero = Vec_PtrSize( p->pCla->vClasses1 );
     p->nLitsBeg  = Fra_ClassesCountLits( p->pCla );
     p->nNodesBeg = Aig_ManNodeNum(pManAig);
     p->nRegsBeg  = Aig_ManRegNum(pManAig);
 
+    // dump AIG of the timeframes
+//    pManAigNew = Fra_ClassesDeriveAig( p->pCla, pPars->nFramesK );
+//    Aig_ManDumpBlif( pManAigNew, "frame_aig.blif" );
+//    Fra_ManPartitionTest2( pManAigNew );
+//    Aig_ManStop( pManAigNew );
+
     // iterate the inductive case
     p->pCla->fRefinement = 1;
     for ( nIter = 0; p->pCla->fRefinement; nIter++ )
@@ -341,7 +344,11 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesP, int nFramesK,
 
         // cleanup
         Fra_ManClean( p );
+//        if ( nIter == 3 )
+//            break;
     }
+//    Fra_ClassesPrint( p->pCla, 1 );
+//    Fra_ClassesSelectRepr( p->pCla );
     // move the classes into representatives and reduce AIG
 clk2 = clock();
     Fra_ClassesCopyReprs( p->pCla, p->vTimeouts );
diff --git a/src/aig/fra/fraMan.c b/src/aig/fra/fraMan.c
index 2b8e0a68..0116bbc4 100644
--- a/src/aig/fra/fraMan.c
+++ b/src/aig/fra/fraMan.c
@@ -248,6 +248,7 @@ void Fra_ManStop( Fra_Man_t * p )
     if ( p->pSat )      sat_solver_delete( p->pSat );
     if ( p->pCla  )     Fra_ClassesStop( p->pCla );
     if ( p->pSml )      Fra_SmlStop( p->pSml );
+    if ( p->vCex )      Vec_IntFree( p->vCex );
     FREE( p->pMemFraig );
     FREE( p->pMemFanins );
     FREE( p->pMemSatNums );
diff --git a/src/aig/fra/fraPart.c b/src/aig/fra/fraPart.c
index d3fdbcfd..6e593694 100644
--- a/src/aig/fra/fraPart.c
+++ b/src/aig/fra/fraPart.c
@@ -170,6 +170,92 @@ PRT( "Scanning", clock() - clk );
 
 
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Fra_ManPartitionTest2( Aig_Man_t * p )
+{
+    Vec_Vec_t * vSupps, * vSuppsIn;
+    Vec_Int_t * vSup, * vSup2, * vSup3;
+    Aig_Obj_t * pObj;
+    int Entry, Entry2, Entry3, Counter;
+    int i, k, m, n, clk;
+    char * pSupp;
+ 
+    // 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 )
+    {
+        if ( i == p->nAsserts )
+            break;
+        vSup = Vec_VecEntry( vSupps, i );
+        Vec_IntForEachEntry( vSup, Entry, k )
+            Vec_VecPush( vSuppsIn, Entry, (void *)i );
+    }
+PRT( "Inverse ", clock() - clk );
+
+    // create affective supports
+clk = clock();
+    pSupp = ALLOC( char, Aig_ManPiNum(p) );
+    Aig_ManForEachPo( p, pObj, i )
+    {
+        if ( i % 50 != 0 )
+            continue;
+        vSup = Vec_VecEntry( vSupps, i );
+        memset( pSupp, 0, sizeof(char) * Aig_ManPiNum(p) );
+        // go through each input of this output
+        Vec_IntForEachEntry( vSup, Entry, k )
+        {
+            pSupp[Entry] = 1;
+            vSup2 = Vec_VecEntry( vSuppsIn, Entry );
+            // go though each assert of this input
+            Vec_IntForEachEntry( vSup2, Entry2, m )
+            {
+                vSup3 = Vec_VecEntry( vSupps, Entry2 );
+                // go through each input of this assert
+                Vec_IntForEachEntry( vSup3, Entry3, n )
+                {
+                    pSupp[Entry3] = 1;
+                }
+            }
+        }
+        // count the entries
+        Counter = 0;
+        for ( m = 0; m < Aig_ManPiNum(p); m++ )
+            Counter += pSupp[m];
+        printf( "%d(%d) ", Vec_IntSize(vSup), Counter );
+    }
+    printf( "\n" );
+PRT( "Extension ", clock() - clk );
+
+    free( pSupp );
+    Vec_VecFree( vSupps );
+    Vec_VecFree( vSuppsIn );
+}
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/fra/fraSec.c b/src/aig/fra/fraSec.c
index 2a0d06b5..8b9258cb 100644
--- a/src/aig/fra/fraSec.c
+++ b/src/aig/fra/fraSec.c
@@ -43,11 +43,12 @@ int Fra_FraigSec( Aig_Man_t * p, int nFramesFix, int fVerbose, int fVeryVerbose
 {
     Aig_Man_t * pNew;
     int nFrames, RetValue, nIter, clk, clkTotal = clock();
+    int fLatchCorr = 0;
     if ( nFramesFix )
     {
         nFrames = nFramesFix;
         // perform seq sweeping for one frame number
-        pNew = Fra_FraigInduction( p, 0, nFrames, 0, 0, 0, fVeryVerbose, &nIter );
+        pNew = Fra_FraigInduction( p, 0, nFrames, 0, 0, 0, fLatchCorr, fVeryVerbose, &nIter );
     }
     else
     {
@@ -55,7 +56,7 @@ int Fra_FraigSec( Aig_Man_t * p, int nFramesFix, int fVerbose, int fVeryVerbose
         for ( nFrames = 1; ; nFrames++ )
         {
 clk = clock();
-            pNew = Fra_FraigInduction( p, 0, nFrames, 0, 0, 0, fVeryVerbose, &nIter );
+            pNew = Fra_FraigInduction( p, 0, nFrames, 0, 0, 0, fLatchCorr, fVeryVerbose, &nIter );
             RetValue = Fra_FraigMiterStatus( pNew );
             if ( fVerbose )
             {
diff --git a/src/aig/fra/fraSim.c b/src/aig/fra/fraSim.c
index b31fcb7f..3463ee0d 100644
--- a/src/aig/fra/fraSim.c
+++ b/src/aig/fra/fraSim.c
@@ -200,6 +200,17 @@ void Fra_SmlSavePattern( Fra_Man_t * p )
         if ( p->pSat->model.ptr[Fra_ObjSatNum(pObj)] == l_True )
             Aig_InfoSetBit( p->pPatWords, i );
 /*
+    if ( p->vCex )
+    {
+        Vec_IntClear( p->vCex );
+        for ( i = 0; i < Aig_ManPiNum(p->pManAig) - Aig_ManRegNum(p->pManAig); i++ )
+            Vec_IntPush( p->vCex, Aig_InfoHasBit( p->pPatWords, i ) );
+        for ( i = Aig_ManPiNum(p->pManFraig) - Aig_ManRegNum(p->pManFraig); i < Aig_ManPiNum(p->pManFraig); i++ )
+            Vec_IntPush( p->vCex, Aig_InfoHasBit( p->pPatWords, i ) );
+    }
+*/
+
+/*
     printf( "Pattern: " );
     Aig_ManForEachPi( p->pManFraig, pObj, i )
         printf( "%d", Aig_InfoHasBit( p->pPatWords, i ) );
@@ -601,7 +612,7 @@ clk = clock();
     if ( p->pCla->vImps )
         nChanges += Fra_ImpRefineUsingCex( p, p->pCla->vImps );
 p->timeRef += clock() - clk;
-    if ( nChanges < 1 )
+    if ( !p->pPars->nFramesK && nChanges < 1 )
         printf( "Error: A counter-example did not refine classes!\n" );
 //    assert( nChanges >= 1 );
 //printf( "Refined classes = %5d.   Changes = %4d.\n", Vec_PtrSize(p->vClasses), nChanges );
diff --git a/src/aig/ivy/ivyMan.c b/src/aig/ivy/ivyMan.c
index 2d99c4f1..07faef85 100644
--- a/src/aig/ivy/ivyMan.c
+++ b/src/aig/ivy/ivyMan.c
@@ -411,7 +411,7 @@ int Ivy_ManLatchIsSelfFeed( Ivy_Obj_t * pLatch )
 int Ivy_ManPropagateBuffers( Ivy_Man_t * p, int fUpdateLevel )
 {
     Ivy_Obj_t * pNode;
-    int LimitFactor = 10;
+    int LimitFactor = 100;
     int NodeBeg = Ivy_ManNodeNum(p);
     int nSteps;
     for ( nSteps = 0; Vec_PtrSize(p->vBufs) > 0; nSteps++ )