Version abc70730

7 files changed, 452 insertions, 224 deletions

diff --git a/src/aig/fra/fra.h b/src/aig/fra/fra.h
index 13e79a0e..91a1f8b1 100644
--- a/src/aig/fra/fra.h
+++ b/src/aig/fra/fra.h
@@ -69,7 +69,7 @@ struct Fra_Par_t_
     int              fConeBias;         // bias variables in the cone (good for unsat runs)
     int              nBTLimitNode;      // conflict limit at a node
     int              nBTLimitMiter;     // conflict limit at an output
-    int              nTimeFrames;       // the number of timeframes to unroll
+    int              nFramesK;          // the number of timeframes to unroll
 };
 
 // FRAIG equivalence classes
@@ -97,7 +97,7 @@ struct Fra_Man_t_
     Aig_Man_t *      pManAig;           // the starting AIG manager
     Aig_Man_t *      pManFraig;         // the final AIG manager
     // mapping AIG into FRAIG
-    int              nFrames;           // the number of timeframes used
+    int              nFramesAll;        // the number of timeframes used
     Aig_Obj_t **     pMemFraig;         // memory allocated for points to the fraig nodes
     // simulation info
     unsigned *       pSimWords;         // memory for simulation information
@@ -152,20 +152,20 @@ struct Fra_Man_t_
 ///                      MACRO DEFINITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
 
-static inline unsigned *   Fra_ObjSim( Aig_Obj_t * pObj )   { return ((Fra_Man_t *)pObj->pData)->pSimWords + ((Fra_Man_t *)pObj->pData)->nSimWords * pObj->Id;    }
-static inline unsigned     Fra_ObjRandomSim()               { return (rand() << 24) ^ (rand() << 12) ^ rand(); }
+static inline unsigned *   Fra_ObjSim( Aig_Obj_t * pObj )   { return ((Fra_Man_t *)pObj->pData)->pSimWords + ((Fra_Man_t *)pObj->pData)->nSimWords * pObj->Id;   }
+static inline unsigned     Fra_ObjRandomSim()               { return (rand() << 24) ^ (rand() << 12) ^ rand();                                                   }
 
-static inline Aig_Obj_t *  Fra_ObjFraig( Aig_Obj_t * pObj, int i )                       { return ((Fra_Man_t *)pObj->pData)->pMemFraig[((Fra_Man_t *)pObj->pData)->nFrames*pObj->Id + i];  }
-static inline void         Fra_ObjSetFraig( Aig_Obj_t * pObj, int i, Aig_Obj_t * pNode ) { ((Fra_Man_t *)pObj->pData)->pMemFraig[((Fra_Man_t *)pObj->pData)->nFrames*pObj->Id + i] = pNode; }
+static inline Aig_Obj_t *  Fra_ObjFraig( Aig_Obj_t * pObj, int i )                       { return ((Fra_Man_t *)pObj->pData)->pMemFraig[((Fra_Man_t *)pObj->pData)->nFramesAll*pObj->Id + i];  }
+static inline void         Fra_ObjSetFraig( Aig_Obj_t * pObj, int i, Aig_Obj_t * pNode ) { ((Fra_Man_t *)pObj->pData)->pMemFraig[((Fra_Man_t *)pObj->pData)->nFramesAll*pObj->Id + i] = pNode; }
 
-static inline Vec_Ptr_t *  Fra_ObjFaninVec( Aig_Obj_t * pObj )                           { return ((Fra_Man_t *)pObj->pData)->pMemFanins[pObj->Id];               }
-static inline void         Fra_ObjSetFaninVec( Aig_Obj_t * pObj, Vec_Ptr_t * vFanins )   { ((Fra_Man_t *)pObj->pData)->pMemFanins[pObj->Id]  = vFanins;           }
+static inline Vec_Ptr_t *  Fra_ObjFaninVec( Aig_Obj_t * pObj )                           { return ((Fra_Man_t *)pObj->pData)->pMemFanins[pObj->Id];      }
+static inline void         Fra_ObjSetFaninVec( Aig_Obj_t * pObj, Vec_Ptr_t * vFanins )   { ((Fra_Man_t *)pObj->pData)->pMemFanins[pObj->Id] = vFanins;   }
 
-static inline int          Fra_ObjSatNum( Aig_Obj_t * pObj )                             { return ((Fra_Man_t *)pObj->pData)->pMemSatNums[pObj->Id];              }
-static inline void         Fra_ObjSetSatNum( Aig_Obj_t * pObj, int Num )                 { ((Fra_Man_t *)pObj->pData)->pMemSatNums[pObj->Id] = Num;               }
+static inline int          Fra_ObjSatNum( Aig_Obj_t * pObj )                             { return ((Fra_Man_t *)pObj->pData)->pMemSatNums[pObj->Id];     }
+static inline void         Fra_ObjSetSatNum( Aig_Obj_t * pObj, int Num )                 { ((Fra_Man_t *)pObj->pData)->pMemSatNums[pObj->Id] = Num;      }
 
-static inline Aig_Obj_t *  Fra_ClassObjRepr( Aig_Obj_t * pObj )                          { return ((Fra_Man_t *)pObj->pData)->pCla->pMemRepr[pObj->Id];           }
-static inline void         Fra_ClassObjSetRepr( Aig_Obj_t * pObj, Aig_Obj_t * pNode )    { ((Fra_Man_t *)pObj->pData)->pCla->pMemRepr[pObj->Id]    = pNode;       }
+static inline Aig_Obj_t *  Fra_ClassObjRepr( Aig_Obj_t * pObj )                          { return ((Fra_Man_t *)pObj->pData)->pCla->pMemRepr[pObj->Id];  }
+static inline void         Fra_ClassObjSetRepr( Aig_Obj_t * pObj, Aig_Obj_t * pNode )    { ((Fra_Man_t *)pObj->pData)->pCla->pMemRepr[pObj->Id] = pNode; }
 
 static inline Aig_Obj_t *  Fra_ObjChild0Fra( Aig_Obj_t * pObj, int i ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin0(pObj)? Aig_NotCond(Fra_ObjFraig(Aig_ObjFanin0(pObj),i), Aig_ObjFaninC0(pObj)) : NULL;  }
 static inline Aig_Obj_t *  Fra_ObjChild1Fra( Aig_Obj_t * pObj, int i ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin1(pObj)? Aig_NotCond(Fra_ObjFraig(Aig_ObjFanin1(pObj),i), Aig_ObjFaninC1(pObj)) : NULL;  }
@@ -187,6 +187,8 @@ extern void                Fra_ClassesPrepare( Fra_Cla_t * p );
 extern int                 Fra_ClassesRefine( Fra_Cla_t * p );
 extern int                 Fra_ClassesRefine1( Fra_Cla_t * p );
 extern int                 Fra_ClassesCountLits( Fra_Cla_t * p );
+extern int                 Fra_ClassesCountPairs( Fra_Cla_t * p );
+extern void                Fra_ClassesTest( Fra_Cla_t * p, int Id1, int Id2 );
 /*=== fraCnf.c ========================================================*/
 extern void                Fra_NodeAddToSolver( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew );
 /*=== fraCore.c ========================================================*/
@@ -195,11 +197,12 @@ extern Aig_Man_t *         Fra_FraigChoice( Aig_Man_t * pManAig );
 extern void                Fra_FraigSweep( Fra_Man_t * pManAig );
 /*=== fraDfs.c ========================================================*/
 /*=== fraInd.c ========================================================*/
-extern Aig_Man_t *         Fra_Induction( Aig_Man_t * p, int nFrames, int fVerbose );
+extern Aig_Man_t *         Fra_FraigInduction( Aig_Man_t * p, int nFramesK, int fVerbose );
 /*=== fraMan.c ========================================================*/
 extern void                Fra_ParamsDefault( Fra_Par_t * pParams );
 extern void                Fra_ParamsDefaultSeq( Fra_Par_t * pParams );
 extern Fra_Man_t *         Fra_ManStart( Aig_Man_t * pManAig, Fra_Par_t * pParams );
+extern void                Fra_ManClean( Fra_Man_t * p );
 extern Aig_Man_t *         Fra_ManPrepareComb( Fra_Man_t * p );
 extern void                Fra_ManFinalizeComb( Fra_Man_t * p );
 extern void                Fra_ManStop( Fra_Man_t * p );
diff --git a/src/aig/fra/fraClass.c b/src/aig/fra/fraClass.c
index 170fcd27..05c07889 100644
--- a/src/aig/fra/fraClass.c
+++ b/src/aig/fra/fraClass.c
@@ -62,11 +62,11 @@ Fra_Cla_t * Fra_ClassesStart( Aig_Man_t * pAig )
     p->pAig = pAig;
     p->pMemRepr  = ALLOC( Aig_Obj_t *, (Aig_ManObjIdMax(pAig) + 1) );
     memset( p->pMemRepr, 0, sizeof(Aig_Obj_t *) * (Aig_ManObjIdMax(pAig) + 1) );
-    p->vClasses   = Vec_PtrAlloc( 100 );
-    p->vClasses1  = Vec_PtrAlloc( 100 );
+    p->vClasses     = Vec_PtrAlloc( 100 );
+    p->vClasses1    = Vec_PtrAlloc( 100 );
     p->vClassesTemp = Vec_PtrAlloc( 100 );
-    p->vClassOld  = Vec_PtrAlloc( 100 );
-    p->vClassNew  = Vec_PtrAlloc( 100 );
+    p->vClassOld    = Vec_PtrAlloc( 100 );
+    p->vClassNew    = Vec_PtrAlloc( 100 );
     return p;
 }
 
@@ -83,8 +83,8 @@ Fra_Cla_t * Fra_ClassesStart( Aig_Man_t * pAig )
 ***********************************************************************/
 void Fra_ClassesStop( Fra_Cla_t * p )
 {
-    free( p->pMemClasses );
-    free( p->pMemRepr );
+    FREE( p->pMemClasses );
+    FREE( p->pMemRepr );
     if ( p->vClassesTemp ) Vec_PtrFree( p->vClassesTemp );
     if ( p->vClassNew )    Vec_PtrFree( p->vClassNew );
     if ( p->vClassOld )    Vec_PtrFree( p->vClassOld );
@@ -110,11 +110,9 @@ 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 ( vFailed )
     Vec_PtrForEachEntry( vFailed, pObj, i )
-    {
-//        assert( p->pAig->pReprs[pObj->Id] != NULL );
         p->pAig->pReprs[pObj->Id] = NULL;
-    }
 }
 
 /**Function*************************************************************
@@ -159,7 +157,7 @@ int Fra_ClassCount( Aig_Obj_t ** pClass )
 
 /**Function*************************************************************
 
-  Synopsis    [Count the number of pairs.]
+  Synopsis    [Count the number of literals.]
 
   Description []
                
@@ -168,22 +166,23 @@ int Fra_ClassCount( Aig_Obj_t ** pClass )
   SeeAlso     []
 
 ***********************************************************************/
-int Fra_ClassesCountPairs( Fra_Cla_t * p )
+int Fra_ClassesCountLits( Fra_Cla_t * p )
 {
     Aig_Obj_t ** pClass;
-    int i, nNodes, nPairs = 0;
+    int i, nNodes, nLits = 0;
+    nLits = Vec_PtrSize( p->vClasses1 );
     Vec_PtrForEachEntry( p->vClasses, pClass, i )
     {
         nNodes = Fra_ClassCount( pClass );
         assert( nNodes > 1 );
-        nPairs += nNodes * (nNodes - 1) / 2;
+        nLits += nNodes - 1;
     }
-    return nPairs;
+    return nLits;
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Count the number of literals.]
+  Synopsis    [Count the number of pairs.]
 
   Description []
                
@@ -192,18 +191,17 @@ int Fra_ClassesCountPairs( Fra_Cla_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-int Fra_ClassesCountLits( Fra_Cla_t * p )
+int Fra_ClassesCountPairs( Fra_Cla_t * p )
 {
     Aig_Obj_t ** pClass;
-    int i, nNodes, nLits = 0;
-    nLits = Vec_PtrSize( p->vClasses1 );
+    int i, nNodes, nPairs = 0;
     Vec_PtrForEachEntry( p->vClasses, pClass, i )
     {
         nNodes = Fra_ClassCount( pClass );
         assert( nNodes > 1 );
-        nLits += nNodes - 1;
+        nPairs += nNodes * (nNodes - 1) / 2;
     }
-    return nLits;
+    return nPairs;
 }
 
 /**Function*************************************************************
@@ -220,14 +218,22 @@ int Fra_ClassesCountLits( Fra_Cla_t * p )
 void Fra_ClassesPrint( Fra_Cla_t * p )
 {
     Aig_Obj_t ** pClass;
+    Aig_Obj_t * pObj;
     int i;
-    printf( "Total classes = %d. Total pairs = %d.\n", Vec_PtrSize(p->vClasses), Fra_ClassesCountPairs(p) );
+    printf( "Consts = %6d. Classes = %6d. Literals = %6d.\n", 
+        Vec_PtrSize(p->vClasses1), Vec_PtrSize(p->vClasses), Fra_ClassesCountLits(p) );
+/*
+    printf( "Constants { " );
+    Vec_PtrForEachEntry( p->vClasses1, pObj, i )
+        printf( "%d ", pObj->Id );
+    printf( "}\n" );
     Vec_PtrForEachEntry( p->vClasses, pClass, i )
     {
         printf( "%3d (%3d) : ", i, Fra_ClassCount(pClass) );
         Fra_PrintClass( pClass );
     }
     printf( "\n" );
+*/
 }
 
 /**Function*************************************************************
@@ -259,6 +265,9 @@ void Fra_ClassesPrepare( Fra_Cla_t * p )
     {
         if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsPi(pObj) )
             continue;
+//printf( "%3d : ", pObj->Id );
+//Extra_PrintBinary( stdout, Fra_ObjSim(pObj), 32 );
+//printf( "\n" );
         // hash the node by its simulation info
         iEntry = Fra_NodeHashSims( pObj ) % nTableSize;
         // check if the node belongs to the class of constant 1
@@ -428,6 +437,7 @@ int Fra_RefineClassLastIter( Fra_Cla_t * p, Vec_Ptr_t * vClasses )
             break;
         }
         // othewise, add the class and continue
+        assert( pClass2[0] != NULL );
         Vec_PtrPush( vClasses, pClass2 );
         pClass = pClass2;
     }
@@ -457,6 +467,7 @@ int Fra_ClassesRefine( Fra_Cla_t * p )
     Vec_PtrForEachEntry( p->vClasses, pClass, i )
     {
         // add the class to the new array
+        assert( pClass[0] != NULL );
         Vec_PtrPush( p->vClassesTemp, pClass );
         // refine the class iteratively
         nRefis += Fra_RefineClassLastIter( p, p->vClassesTemp );
@@ -517,12 +528,38 @@ int Fra_ClassesRefine1( Fra_Cla_t * p )
         ppClass[Vec_PtrSize(p->vClassNew)+i] = NULL;
         Fra_ClassObjSetRepr( pObj, i? ppClass[0] : NULL );
     }
+    assert( ppClass[0] != NULL );
     Vec_PtrPush( p->vClasses, ppClass );
     // iteratively refine this class
     nRefis = 1 + Fra_RefineClassLastIter( p, p->vClasses );
     return nRefis;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Starts representation of equivalence classes with one class.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Fra_ClassesTest( Fra_Cla_t * p, int Id1, int Id2 )
+{
+    Aig_Obj_t ** pClass;
+    p->pMemClasses = ALLOC( Aig_Obj_t *, 4 );
+    pClass = p->pMemClasses;
+    assert( Id1 < Id2 );
+    pClass[0] = Aig_ManObj( p->pAig, Id1 );
+    pClass[1] = Aig_ManObj( p->pAig, Id2 );
+    pClass[2] = NULL;
+    pClass[3] = NULL;
+    Fra_ClassObjSetRepr( pClass[1], pClass[0] );
+    Vec_PtrPush( p->vClasses, pClass );
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/fra/fraCore.c b/src/aig/fra/fraCore.c
index 977396dd..9f2b8ca7 100644
--- a/src/aig/fra/fraCore.c
+++ b/src/aig/fra/fraCore.c
@@ -30,6 +30,37 @@
 
 /**Function*************************************************************
 
+  Synopsis    [Write speculative miter for one node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Fra_FraigNodeSpeculate( Fra_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pObjFraig, Aig_Obj_t * pObjReprFraig )
+{ 
+    static int Counter = 0;
+    char FileName[20];
+    Aig_Man_t * pTemp;
+    Aig_Obj_t * pNode;
+    int i;
+    // create manager with the logic for these two nodes
+    Aig_Obj_t * ppNodes[2] = { pObjFraig, pObjReprFraig };
+    pTemp = Aig_ManExtractMiter( p->pManFraig, ppNodes, 2 );
+    // dump the logic into a file
+    sprintf( FileName, "aig\\%03d.blif", ++Counter );
+    Aig_ManDumpBlif( pTemp, FileName );
+    printf( "Speculation cone with %d nodes was written into file \"%s\".\n", Aig_ManNodeNum(pTemp), FileName );
+    // clean up
+    Aig_ManStop( pTemp );
+    Aig_ManForEachObj( p->pManFraig, pNode, i )
+        pNode->pData = p;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Performs fraiging for one node.]
 
   Description [Returns the fraiged node.]
@@ -39,84 +70,59 @@
   SeeAlso     []
 
 ***********************************************************************/
-Aig_Obj_t * Fra_And( Fra_Man_t * p, Aig_Obj_t * pObj )
+void Fra_FraigNode( Fra_Man_t * p, Aig_Obj_t * pObj )
 { 
-    Aig_Obj_t * pObjRepr, * pObjFraig, * pFanin0Fraig, * pFanin1Fraig, * pObjReprFraig;
+    Aig_Obj_t * pObjRepr, * pObjFraig, * pObjFraig2, * pObjReprFraig;
     int RetValue;
     assert( !Aig_IsComplement(pObj) );
-    assert( Aig_ObjIsNode(pObj) );
-    // get the fraiged fanins
-    pFanin0Fraig = Fra_ObjChild0Fra(pObj,0);
-    pFanin1Fraig = Fra_ObjChild1Fra(pObj,0);
-    // get the fraiged node
-    pObjFraig = Aig_And( p->pManFraig, pFanin0Fraig, pFanin1Fraig );
-    if ( Aig_ObjIsConst1(Aig_Regular(pObjFraig)) )
-        return pObjFraig;
-    Aig_Regular(pObjFraig)->pData = p;
     // get representative of this class
-    pObjRepr = Fra_ClassObjRepr(pObj);
+    pObjRepr = Fra_ClassObjRepr( pObj );
     if ( pObjRepr == NULL || // this is a unique node
        (!p->pPars->fDoSparse && pObjRepr == Aig_ManConst1(p->pManAig)) ) // this is a sparse node
-    {
-        assert( Aig_Regular(pFanin0Fraig) != Aig_Regular(pFanin1Fraig) );
-        assert( Aig_Regular(pObjFraig) != Aig_Regular(pFanin0Fraig) );
-        assert( Aig_Regular(pObjFraig) != Aig_Regular(pFanin1Fraig) );
-        return pObjFraig;
-    }
+        return;
+    // get the fraiged node
+    pObjFraig = Fra_ObjFraig( pObj, p->pPars->nFramesK );
     // get the fraiged representative
-    pObjReprFraig = Fra_ObjFraig(pObjRepr,0);
+    pObjReprFraig = Fra_ObjFraig( pObjRepr, p->pPars->nFramesK );
     // if the fraiged nodes are the same, return
     if ( Aig_Regular(pObjFraig) == Aig_Regular(pObjReprFraig) )
-        return pObjFraig;
-    assert( Aig_Regular(pObjFraig) != Aig_ManConst1(p->pManFraig) );
-//    printf( "Node = %d. Repr = %d.\n", pObj->Id, pObjRepr->Id );
-
+        return;
+    assert( p->pPars->nFramesK || Aig_Regular(pObjFraig) != Aig_ManConst1(p->pManFraig) );
     // if they are proved different, the c-ex will be in p->pPatWords
     RetValue = Fra_NodesAreEquiv( p, Aig_Regular(pObjReprFraig), Aig_Regular(pObjFraig) );
     if ( RetValue == 1 )  // proved equivalent
     {
-//        pObj->fMarkA = 1;
 //        if ( p->pPars->fChoicing )
 //            Aig_ObjCreateRepr( p->pManFraig, Aig_Regular(pObjReprFraig), Aig_Regular(pObjFraig) );
-        return Aig_NotCond( pObjReprFraig, pObj->fPhase ^ pObjRepr->fPhase );
+        // the nodes proved equal
+        pObjFraig2 = Aig_NotCond( pObjReprFraig, pObj->fPhase ^ pObjRepr->fPhase );
+        Fra_ObjSetFraig( pObj, p->pPars->nFramesK, pObjFraig2 );
+        return;
     }
     if ( RetValue == -1 ) // failed
     {
-        static int Counter = 0;
-        char FileName[20];
-        Aig_Man_t * pTemp;
-        Aig_Obj_t * pNode;
-        int i;
-
-        Aig_Obj_t * ppNodes[2] = { Aig_Regular(pObjReprFraig), Aig_Regular(pObjFraig) };
-//        Vec_Ptr_t * vNodes;
-
+        if ( p->vTimeouts == NULL )
+            p->vTimeouts = Vec_PtrAlloc( 100 );
         Vec_PtrPush( p->vTimeouts, pObj );
         if ( !p->pPars->fSpeculate )
-            return pObjFraig;
-        // substitute the node
-//        pObj->fMarkB = 1;
+            return;
+        assert( 0 );
+        // speculate
         p->nSpeculs++;
-
-        pTemp = Aig_ManExtractMiter( p->pManFraig, ppNodes, 2 );
-        sprintf( FileName, "aig\\%03d.blif", ++Counter );
-        Aig_ManDumpBlif( pTemp, FileName );
-        printf( "Speculation cone with %d nodes was written into file \"%s\".\n", Aig_ManNodeNum(pTemp), FileName );
-        Aig_ManStop( pTemp );
-
-        Aig_ManForEachObj( p->pManFraig, pNode, i )
-            pNode->pData = p;
-
-//        vNodes = Aig_ManDfsNodes( p->pManFraig, ppNodes, 2 );
-//        printf( "Cone=%d ", Vec_PtrSize(vNodes) );
-//        Vec_PtrFree( vNodes );
-
-        return Aig_NotCond( pObjReprFraig, pObj->fPhase ^ pObjRepr->fPhase );
+        pObjFraig2 = Aig_NotCond( pObjReprFraig, pObj->fPhase ^ pObjRepr->fPhase );
+        Fra_ObjSetFraig( pObj, p->pPars->nFramesK, pObjFraig2 );
+        Fra_FraigNodeSpeculate( p, pObj, Aig_Regular(pObjFraig), Aig_Regular(pObjReprFraig) );
+        return;
     }
+//printf( "Disproved %d and %d.\n", pObj->Id, pObjRepr->Id );
+    // disprove the nodes
+    // 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 );
     // simulate the counter-example and return the Fraig node
     Fra_Resimulate( p );
     assert( Fra_ClassObjRepr(pObj) != pObjRepr );
-    return pObjFraig;
 }
 
 /**Function*************************************************************
@@ -139,15 +145,22 @@ p->nClassesZero = Vec_PtrSize(p->pCla->vClasses1);
 p->nClassesBeg  = Vec_PtrSize(p->pCla->vClasses) + (int)(Vec_PtrSize(p->pCla->vClasses1) > 0);
     // duplicate internal nodes
     pProgress = Extra_ProgressBarStart( stdout, Aig_ManObjIdMax(p->pManAig) );
+    // fraig latch outputs
+    Aig_ManForEachLoSeq( p->pManAig, pObj, i )
+        Fra_FraigNode( p, pObj );
+    // fraig internal nodes
     Aig_ManForEachNode( p->pManAig, pObj, i )
     {
         Extra_ProgressBarUpdate( pProgress, i, NULL );
-        // default to simple strashing if simulation detected a counter-example for a PO
+        // derive and remember the new fraig node
+        pObjNew = Aig_And( p->pManFraig, Fra_ObjChild0Fra(pObj,p->pPars->nFramesK), Fra_ObjChild1Fra(pObj,p->pPars->nFramesK) );
+        Fra_ObjSetFraig( pObj, p->pPars->nFramesK, pObjNew );
+        Aig_Regular(pObjNew)->pData = p;
+        // quit if simulation detected a counter-example for a PO
         if ( p->pManFraig->pData )
-            pObjNew = Aig_And( p->pManFraig, Fra_ObjChild0Fra(pObj,0), Fra_ObjChild1Fra(pObj,0) );
-        else
-            pObjNew = Fra_And( p, pObj ); // pObjNew can be complemented
-        Fra_ObjSetFraig( pObj, 0, pObjNew );
+            continue;
+        // perform fraiging
+        Fra_FraigNode( p, pObj );
     }
     Extra_ProgressBarStop( pProgress );
 p->nClassesEnd = Vec_PtrSize(p->pCla->vClasses) + (int)(Vec_PtrSize(p->pCla->vClasses1) > 0);
@@ -198,6 +211,14 @@ clk = clock();
         Aig_ManCleanup( p->pManFraig );
         pManAigNew = p->pManFraig;
         p->pManFraig = NULL;
+/*
+        Fra_ClassesCopyReprs( p->pCla, p->vTimeouts );
+        pManAigNew = Aig_ManDupRepr( p->pManAig );
+//        Aig_ManCreateChoices( pManAigNew );
+        Aig_ManCleanup( pManAigNew );
+        Aig_ManStop( p->pManFraig );
+        p->pManFraig = NULL;
+*/
     }
 p->timeTotal = clock() - clk;
     Fra_ManStop( p );
diff --git a/src/aig/fra/fraInd.c b/src/aig/fra/fraInd.c
index 1bfe1cb4..71e535f7 100644
--- a/src/aig/fra/fraInd.c
+++ b/src/aig/fra/fraInd.c
@@ -31,6 +31,42 @@
 
 /**Function*************************************************************
 
+  Synopsis    [Performs speculative reduction for one node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Fra_FramesConstrainNode( Aig_Man_t * pManFraig, Aig_Obj_t * pObj, int iFrame )
+{
+    Aig_Obj_t * pObjNew, * pObjNew2, * pObjRepr, * pObjReprNew, * pMiter;
+    // skip nodes without representative
+    if ( (pObjRepr = Fra_ClassObjRepr(pObj)) == NULL )
+        return;
+    assert( pObjRepr->Id < pObj->Id );
+    // get the new node 
+    pObjNew = Fra_ObjFraig( pObj, iFrame );
+    // get the new node of the representative
+    pObjReprNew = Fra_ObjFraig( pObjRepr, iFrame );
+    // 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_ObjSetFraig( pObj, iFrame, 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    [Prepares the inductive case with speculative reduction.]
 
   Description []
@@ -43,77 +79,58 @@
 Aig_Man_t * Fra_FramesWithClasses( Fra_Man_t * p )
 {
     Aig_Man_t * pManFraig;
-    Aig_Obj_t * pObj, * pObjRepr, * pObjNew, * pObjReprNew, * pMiter;
+    Aig_Obj_t * pObj, * pObjNew;
     Aig_Obj_t ** pLatches;
     int i, k, f;
     assert( p->pManFraig == NULL );
-    assert( Aig_ManInitNum(p->pManAig) > 0 );
-    assert( Aig_ManInitNum(p->pManAig) < Aig_ManPiNum(p->pManAig) );
+    assert( Aig_ManRegNum(p->pManAig) > 0 );
+    assert( Aig_ManRegNum(p->pManAig) < Aig_ManPiNum(p->pManAig) );
 
     // start the fraig package
-    pManFraig = Aig_ManStart( (Aig_ManObjIdMax(p->pManAig) + 1) * p->nFrames );
-    pManFraig->vInits = Vec_IntDup(p->pManAig->vInits);
+    pManFraig = Aig_ManStart( (Aig_ManObjIdMax(p->pManAig) + 1) * p->nFramesAll );
+    pManFraig->nRegs = p->pManAig->nRegs;
     // create PI nodes for the frames
-    for ( f = 0; f < p->nFrames; f++ )
-    {
+    for ( f = 0; f < p->nFramesAll; f++ )
         Fra_ObjSetFraig( Aig_ManConst1(p->pManAig), f, Aig_ManConst1(pManFraig) );
+    for ( f = 0; f < p->nFramesAll; f++ )
         Aig_ManForEachPiSeq( p->pManAig, pObj, i )
             Fra_ObjSetFraig( pObj, f, Aig_ObjCreatePi(pManFraig) );
-    }
     // create latches for the first frame
     Aig_ManForEachLoSeq( p->pManAig, pObj, i )
         Fra_ObjSetFraig( pObj, 0, Aig_ObjCreatePi(pManFraig) );
 
     // add timeframes
-    pLatches = ALLOC( Aig_Obj_t *, Aig_ManInitNum(p->pManAig) );
-    for ( f = 0; f < p->nFrames - 1; f++ )
+    pLatches = ALLOC( Aig_Obj_t *, Aig_ManRegNum(p->pManAig) );
+    for ( f = 0; f < p->nFramesAll - 1; f++ )
     {
+        // set the constraints on the latch outputs
+        Aig_ManForEachLoSeq( p->pManAig, pObj, i )
+            Fra_FramesConstrainNode( pManFraig, pObj, f );
         // add internal nodes of this frame
         Aig_ManForEachNode( p->pManAig, pObj, i )
         {
             pObjNew = Aig_And( pManFraig, Fra_ObjChild0Fra(pObj,f), Fra_ObjChild1Fra(pObj,f) );
             Fra_ObjSetFraig( pObj, f, pObjNew );
-            // skip nodes without representative
-            if ( (pObjRepr = Fra_ClassObjRepr(pObj)) == NULL )
-                continue;
-            assert( pObjRepr->Id < pObj->Id );
-            // get the new node of the representative
-            pObjReprNew = Fra_ObjFraig( pObjRepr, f );
-            // if this is the same node, no need to add constraints
-            if ( Aig_Regular(pObjNew) == Aig_Regular(pObjReprNew) )
-                continue;
-            // these are different nodes
-            // perform speculative reduction
-            Fra_ObjSetFraig( pObj, f, Aig_NotCond(pObjReprNew, pObj->fPhase ^ pObjRepr->fPhase) );
-            // add the constraint
-            pMiter = Aig_Exor( pManFraig, pObjNew, pObjReprNew );
-            pMiter = Aig_NotCond( pMiter, Aig_Regular(pMiter)->fPhase ^ Aig_IsComplement(pMiter) );
-            Aig_ObjCreatePo( pManFraig, pMiter );
+            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_ManInitNum(p->pManAig) );
+        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_ManInitNum(p->pManAig) );
+        assert( k == Aig_ManRegNum(p->pManAig) );
     }
     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) );
-
-    // set the pointer to the manager
-    Aig_ManForEachObj( p->pManAig, pObj, i )
-        pObj->pData = p;
-    // set the pointers to the manager
-    Aig_ManForEachObj( pManFraig, pObj, i )
-        pObj->pData = p;
+        Aig_ObjCreatePo( pManFraig, Fra_ObjChild0Fra(pObj,f-1) );
+
     // make sure the satisfying assignment is node assigned
     assert( pManFraig->pData == NULL );
     return pManFraig;
@@ -130,7 +147,7 @@ Aig_Man_t * Fra_FramesWithClasses( Fra_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-Aig_Man_t * Fra_Induction( Aig_Man_t * pManAig, int nFrames, int fVerbose )
+Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesK, int fVerbose )
 {
     Fra_Man_t * p;
     Fra_Par_t Pars, * pPars = &Pars; 
@@ -142,20 +159,23 @@ Aig_Man_t * Fra_Induction( Aig_Man_t * pManAig, int nFrames, int fVerbose )
     if ( Aig_ManNodeNum(pManAig) == 0 )
         return Aig_ManDup(pManAig, 1);
     assert( Aig_ManLatchNum(pManAig) == 0 );
-    assert( Aig_ManInitNum(pManAig) > 0 );
+    assert( Aig_ManRegNum(pManAig) > 0 );
+    assert( nFramesK > 0 );
 
     // get parameters
     Fra_ParamsDefaultSeq( pPars );
-    pPars->nTimeFrames = nFrames;
+    pPars->nFramesK = nFramesK;
     pPars->fVerbose = fVerbose;
 
     // start the fraig manager for this run
     p = Fra_ManStart( pManAig, pPars );
     // derive and refine e-classes using the 1st init frame
     Fra_Simulate( p, 1 );
+//    Fra_ClassesTest( p->pCla, 2, 3 );
+//Aig_ManShow( pManAig, 0, NULL );
 
     // refine e-classes using sequential simulation
-
+ 
     // iterate the inductive case
     p->pCla->fRefinement = 1;
     for ( nIter = 0; p->pCla->fRefinement; nIter++ )
@@ -165,18 +185,32 @@ Aig_Man_t * Fra_Induction( Aig_Man_t * pManAig, int nFrames, int fVerbose )
         // derive non-init K-timeframes while implementing e-classes
         p->pManFraig = Fra_FramesWithClasses( p );
         if ( fVerbose )
-            printf( "Iter = %3d.  Original = %6d. Reduced = %6d.\n", 
-                nIter, Fra_ClassesCountLits(p->pCla), p->pManFraig->nAsserts );
-
+        {
+            printf( "%3d : Const = %6d. Class = %6d.  L = %6d. LR = %6d.  N = %6d. NR = %6d.\n", 
+                nIter, Vec_PtrSize(p->pCla->vClasses1), Vec_PtrSize(p->pCla->vClasses), 
+                Fra_ClassesCountLits(p->pCla), p->pManFraig->nAsserts,
+                Aig_ManNodeNum(p->pManAig), Aig_ManNodeNum(p->pManFraig) );
+        }
         // perform AIG rewriting on the speculated frames
 
         // convert the manager to SAT solver (the last nLatches outputs are inputs)
-        pCnf = Cnf_Derive( p->pManFraig, Aig_ManInitNum(p->pManFraig) );
+//        pCnf = Cnf_Derive( p->pManFraig, Aig_ManRegNum(p->pManFraig) );
+        pCnf = Cnf_DeriveSimple( p->pManFraig, Aig_ManRegNum(p->pManFraig) );
+//Cnf_DataWriteIntoFile( pCnf, "temp.cnf", 1 );
+
         p->pSat = Cnf_DataWriteIntoSolver( pCnf );
-        // transfer variable numbers
-        Aig_ManForEachPi( p->pManAig, pObj, i )
+        p->nSatVars = pCnf->nVars;
+
+        // set the pointers to the manager
+        Aig_ManForEachObj( p->pManFraig, pObj, i )
+            pObj->pData = p;
+        // transfer PI/LO variable numbers
+        pObj = Aig_ManConst1( p->pManFraig );
+        Fra_ObjSetSatNum( pObj, pCnf->pVarNums[pObj->Id] );
+        Aig_ManForEachPi( p->pManFraig, pObj, i )
             Fra_ObjSetSatNum( pObj, pCnf->pVarNums[pObj->Id] );
-        Aig_ManForEachLiSeq( p->pManAig, pObj, i )
+        // transfer LI variable numbers
+        Aig_ManForEachLiSeq( p->pManFraig, pObj, i )
         {
             Fra_ObjSetSatNum( pObj, pCnf->pVarNums[pObj->Id] );
             Fra_ObjSetFaninVec( pObj, (void *)1 );
@@ -185,9 +219,10 @@ Aig_Man_t * Fra_Induction( Aig_Man_t * pManAig, int nFrames, int fVerbose )
 
         // perform sweeping
         Fra_FraigSweep( p );
-        assert( Vec_PtrSize(p->vTimeouts) == 0 );
-        Aig_ManStop( p->pManFraig );   p->pManFraig = NULL;
-        sat_solver_delete( p->pSat );  p->pSat = NULL;
+        assert( p->vTimeouts == NULL );
+
+        // cleanup
+        Fra_ManClean( p );
     }
 
     // move the classes into representatives
diff --git a/src/aig/fra/fraMan.c b/src/aig/fra/fraMan.c
index e109df56..fdd1ccc5 100644
--- a/src/aig/fra/fraMan.c
+++ b/src/aig/fra/fraMan.c
@@ -53,7 +53,7 @@ void Fra_ParamsDefault( Fra_Par_t * pPars )
     pPars->dActConeBumpMax  =    10.0;  // the largest bump of activity
     pPars->nBTLimitNode     =     100;  // conflict limit at a node
     pPars->nBTLimitMiter    =  500000;  // conflict limit at an output
-    pPars->nTimeFrames      =       0;  // the number of timeframes to unroll
+    pPars->nFramesK         =       0;  // the number of timeframes to unroll
     pPars->fConeBias        =       1;
 }
 
@@ -71,7 +71,7 @@ void Fra_ParamsDefault( Fra_Par_t * pPars )
 void Fra_ParamsDefaultSeq( Fra_Par_t * pPars )
 {
     memset( pPars, 0, sizeof(Fra_Par_t) );
-    pPars->nSimWords        =      32;  // the number of words in the simulation info
+    pPars->nSimWords        =       4;  // the number of words in the simulation info
     pPars->dSimSatur        =   0.005;  // the ratio of refined classes when saturation is reached
     pPars->fPatScores       =       0;  // enables simulation pattern scoring
     pPars->MaxScore         =      25;  // max score after which resimulation is used
@@ -82,7 +82,7 @@ void Fra_ParamsDefaultSeq( Fra_Par_t * pPars )
     pPars->dActConeBumpMax  =    10.0;  // the largest bump of activity
     pPars->nBTLimitNode     = 1000000;  // conflict limit at a node
     pPars->nBTLimitMiter    =  500000;  // conflict limit at an output
-    pPars->nTimeFrames      =       1;  // the number of timeframes to unroll
+    pPars->nFramesK         =       1;  // the number of timeframes to unroll
     pPars->fConeBias        =       0;
 }
 
@@ -100,40 +100,76 @@ void Fra_ParamsDefaultSeq( Fra_Par_t * pPars )
 Fra_Man_t * Fra_ManStart( Aig_Man_t * pManAig, Fra_Par_t * pPars )
 {
     Fra_Man_t * p;
+    Aig_Obj_t * pObj;
+    int i;
     // allocate the fraiging manager
     p = ALLOC( Fra_Man_t, 1 );
     memset( p, 0, sizeof(Fra_Man_t) );
     p->pPars      = pPars;
     p->pManAig    = pManAig;
     p->nSizeAlloc = Aig_ManObjIdMax( pManAig ) + 1;
-    p->nFrames    = pPars->nTimeFrames + 1;
+    p->nFramesAll = pPars->nFramesK + 1;
     // allocate simulation info
-    p->nSimWords  = pPars->nSimWords * p->nFrames;
-    p->pSimWords  = ALLOC( unsigned, p->nSizeAlloc * p->nSimWords * p->nFrames );
+    p->nSimWords  = pPars->nSimWords * p->nFramesAll;
+    p->pSimWords  = ALLOC( unsigned, p->nSizeAlloc * p->nSimWords );
     // clean simulation info of the constant node
-    memset( p->pSimWords, 0, sizeof(unsigned) * p->nSizeAlloc * p->nSimWords * p->nFrames );
+    memset( p->pSimWords, 0, sizeof(unsigned) * p->nSizeAlloc * p->nSimWords );
     // allocate storage for sim pattern
-    p->nPatWords  = Aig_BitWordNum( Aig_ManPiNum(pManAig) );
+    p->nPatWords  = Aig_BitWordNum( Aig_ManPiNum(pManAig) * p->nFramesAll );
     p->pPatWords  = ALLOC( unsigned, p->nPatWords ); 
     p->pPatScores = ALLOC( int, 32 * p->nSimWords ); 
     p->vPiVars    = Vec_PtrAlloc( 100 );
-    p->vTimeouts  = Vec_PtrAlloc( 100 );
     // equivalence classes
     p->pCla       = Fra_ClassesStart( pManAig );
     // allocate other members
-    p->pMemFraig  = ALLOC( Aig_Obj_t *, p->nSizeAlloc * p->nFrames );
-    memset( p->pMemFraig, 0, sizeof(Aig_Obj_t *) * p->nSizeAlloc * p->nFrames );
-    p->pMemFanins = ALLOC( Vec_Ptr_t *, p->nSizeAlloc * p->nFrames );
-    memset( p->pMemFanins, 0, sizeof(Vec_Ptr_t *) * p->nSizeAlloc * p->nFrames );
-    p->pMemSatNums = ALLOC( int, p->nSizeAlloc * p->nFrames );
-    memset( p->pMemSatNums, 0, sizeof(int) * p->nSizeAlloc * p->nFrames );
+    p->pMemFraig  = ALLOC( Aig_Obj_t *, p->nSizeAlloc * p->nFramesAll );
+    memset( p->pMemFraig, 0, sizeof(Aig_Obj_t *) * p->nSizeAlloc * p->nFramesAll );
+    p->pMemFanins = ALLOC( Vec_Ptr_t *, p->nSizeAlloc * p->nFramesAll + 10000 );
+    memset( p->pMemFanins, 0, sizeof(Vec_Ptr_t *) * p->nSizeAlloc * p->nFramesAll + 10000 );
+    p->pMemSatNums = ALLOC( int, p->nSizeAlloc * p->nFramesAll + 10000 );
+    memset( p->pMemSatNums, 0, sizeof(int) * p->nSizeAlloc * p->nFramesAll + 10000 );
     // set random number generator
     srand( 0xABCABC );
+    // set the pointer to the manager
+    Aig_ManForEachObj( p->pManAig, pObj, i )
+        pObj->pData = p;
     return p;
 }
 
 /**Function*************************************************************
 
+  Synopsis    [Starts the fraiging manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Fra_ManClean( Fra_Man_t * p )
+{
+    int i, Limit;
+
+    Limit = Aig_ManObjIdMax(p->pManFraig) + 1;
+    for ( i = 0; i < Limit; i++ )
+        if ( p->pMemFanins[i] && p->pMemFanins[i] != (void *)1 )
+            Vec_PtrFree( p->pMemFanins[i] );
+
+    memset( p->pMemFraig, 0, sizeof(Aig_Obj_t *) * p->nSizeAlloc * p->nFramesAll );
+    memset( p->pMemFanins, 0, sizeof(Vec_Ptr_t *) * Limit );
+    memset( p->pMemSatNums, 0, sizeof(int) * Limit );
+
+    Aig_ManStop( p->pManFraig );   
+    p->pManFraig = NULL;
+
+    sat_solver_delete( p->pSat );  
+    p->pSat = NULL; 
+    p->nSatVars = 0;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Prepares the new manager to begin fraiging.]
 
   Description []
@@ -149,9 +185,6 @@ Aig_Man_t * Fra_ManPrepareComb( Fra_Man_t * p )
     Aig_Obj_t * pObj;
     int i;
     assert( p->pManFraig == NULL );
-    // set the pointer to the manager
-    Aig_ManForEachObj( p->pManAig, pObj, i )
-        pObj->pData = p;
     // start the fraig package
     pManFraig = Aig_ManStart( Aig_ManObjIdMax(p->pManAig) + 1 );
     // set the pointers to the available fraig nodes
@@ -204,7 +237,7 @@ void Fra_ManStop( Fra_Man_t * p )
 {
     int i;
     for ( i = 0; i < p->nSizeAlloc; i++ )
-        if ( p->pMemFanins[i] )
+        if ( p->pMemFanins[i] && p->pMemFanins[i] != (void *)1 )
             Vec_PtrFree( p->pMemFanins[i] );
     if ( p->pPars->fVerbose )
         Fra_ManPrint( p );
diff --git a/src/aig/fra/fraSat.c b/src/aig/fra/fraSat.c
index 418e9fee..a728d860 100644
--- a/src/aig/fra/fraSat.c
+++ b/src/aig/fra/fraSat.c
@@ -44,6 +44,7 @@ static int Fra_SetActivityFactors( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t *
 int Fra_NodesAreEquiv( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew )
 {
     int pLits[4], RetValue, RetValue1, nBTLimit, clk, clk2 = clock();
+    int status;
 
     // make sure the nodes are not complemented
     assert( !Aig_IsComplement(pNew) );
@@ -54,7 +55,7 @@ int Fra_NodesAreEquiv( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew )
     // if the backtrack limit is small, simply skip this node
     // if the backtrack limit is > 10, take the quare root of the limit
     nBTLimit = p->pPars->nBTLimitNode;
-    if ( !p->pPars->fSpeculate && p->pPars->nTimeFrames == 0 && (nBTLimit > 0 && (pOld->fMarkB || pNew->fMarkB)) )
+    if ( !p->pPars->fSpeculate && p->pPars->nFramesK == 0 && (nBTLimit > 0 && (pOld->fMarkB || pNew->fMarkB)) )
     {
         p->nSatFails++;
         // fail immediately
@@ -77,6 +78,13 @@ int Fra_NodesAreEquiv( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew )
     // if the nodes do not have SAT variables, allocate them
     Fra_NodeAddToSolver( p, pOld, pNew );
 
+    if ( p->pSat->qtail != p->pSat->qhead )
+    {
+        status = sat_solver_simplify(p->pSat);
+        assert( status != 0 );
+        assert( p->pSat->qtail == p->pSat->qhead );
+    }
+
     // prepare variable activity
     if ( p->pPars->fConeBias )
         Fra_SetActivityFactors( p, pOld, pNew ); 
diff --git a/src/aig/fra/fraSim.c b/src/aig/fra/fraSim.c
index a01bc2e0..4ae8a686 100644
--- a/src/aig/fra/fraSim.c
+++ b/src/aig/fra/fraSim.c
@@ -60,13 +60,13 @@ void Fra_NodeAssignRandom( Fra_Man_t * p, Aig_Obj_t * pObj )
   SeeAlso     []
 
 ***********************************************************************/
-void Fra_NodeAssignConst( Fra_Man_t * p, Aig_Obj_t * pObj, int fConst1 )
+void Fra_NodeAssignConst( Fra_Man_t * p, Aig_Obj_t * pObj, int fConst1, int iFrame )
 {
     unsigned * pSims;
     int i;
     assert( Aig_ObjIsPi(pObj) );
-    pSims = Fra_ObjSim(pObj);
-    for ( i = 0; i < p->nSimWords; i++ )
+    pSims = Fra_ObjSim(pObj) + p->pPars->nSimWords * iFrame;
+    for ( i = 0; i < p->pPars->nSimWords; i++ )
         pSims[i] = fConst1? ~(unsigned)0 : 0;
 }
 
@@ -84,18 +84,17 @@ void Fra_NodeAssignConst( Fra_Man_t * p, Aig_Obj_t * pObj, int fConst1 )
 void Fra_AssignRandom( Fra_Man_t * p, int fInit )
 {
     Aig_Obj_t * pObj;
-    int i, k;
+    int i;
     if ( fInit )
     {
-        assert( Aig_ManInitNum(p->pManAig) > 0 );
-        assert( Aig_ManInitNum(p->pManAig) < Aig_ManPiNum(p->pManAig) );
+        assert( Aig_ManRegNum(p->pManAig) > 0 );
+        assert( Aig_ManRegNum(p->pManAig) < Aig_ManPiNum(p->pManAig) );
         // assign random info for primary inputs
         Aig_ManForEachPiSeq( p->pManAig, pObj, i )
             Fra_NodeAssignRandom( p, pObj );
         // assign the initial state for the latches
-        k = 0;
         Aig_ManForEachLoSeq( p->pManAig, pObj, i )
-            Fra_NodeAssignConst( p, pObj, Vec_IntEntry(p->pManAig->vInits,k++) );
+            Fra_NodeAssignConst( p, pObj, 0, 0 );
     }
     else
     {
@@ -118,33 +117,36 @@ void Fra_AssignRandom( Fra_Man_t * p, int fInit )
 void Fra_AssignDist1( Fra_Man_t * p, unsigned * pPat )
 {
     Aig_Obj_t * pObj;
-    int i, Limit;
-    Aig_ManForEachPi( p->pManAig, pObj, i )
-        Fra_NodeAssignConst( p, pObj, Aig_InfoHasBit(pPat, i) );
-    Limit = AIG_MIN( Aig_ManPiNum(p->pManAig) - Aig_ManInitNum(p->pManAig), p->nSimWords * 32 - 1 );
-    for ( i = 0; i < Limit; i++ )
-        Aig_InfoXorBit( Fra_ObjSim( Aig_ManPi(p->pManAig,i) ), i+1 );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Returns 1 if simulation info is composed of all zeros.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
+    int f, i, k, Limit, nTruePis;
+    if ( p->pPars->nFramesK == 0 )
+    {
+        assert( p->nFramesAll == 1 );
+        // copy the PI info 
+        Aig_ManForEachPi( p->pManAig, pObj, i )
+            Fra_NodeAssignConst( p, pObj, Aig_InfoHasBit(pPat, i), 0 );
+        // flip one bit
+        Limit = AIG_MIN( Aig_ManPiNum(p->pManAig), p->nSimWords * 32 - 1 );
+        for ( i = 0; i < Limit; i++ )
+            Aig_InfoXorBit( Fra_ObjSim( Aig_ManPi(p->pManAig,i) ), i+1 );
+    }
+    else
+    {
+        // copy the PI info for each frame
+        nTruePis = Aig_ManPiNum(p->pManAig) - Aig_ManRegNum(p->pManAig);
+        for ( f = 0; f < p->nFramesAll; f++ )
+            Aig_ManForEachPiSeq( p->pManAig, pObj, i )
+                Fra_NodeAssignConst( p, pObj, Aig_InfoHasBit(pPat, nTruePis * f + i), f );
+        // copy the latch info 
+        k = 0;
+        Aig_ManForEachLoSeq( p->pManAig, pObj, i )
+            Fra_NodeAssignConst( p, pObj, Aig_InfoHasBit(pPat, nTruePis * p->nFramesAll + k++), 0 );
+        assert( p->pManFraig == NULL || nTruePis * p->nFramesAll + k == Aig_ManPiNum(p->pManFraig) );
 
-***********************************************************************/
-void Fra_NodeComplementSim( Aig_Obj_t * pObj )
-{
-    Fra_Man_t * p = pObj->pData;
-    unsigned * pSims;
-    int i;
-    pSims = Fra_ObjSim(pObj);
-    for ( i = 0; i < p->nSimWords; i++ )
-        pSims[i] = ~pSims[i];
+        // flip one bit of the first frame
+        Limit = AIG_MIN( nTruePis, p->pPars->nSimWords * 32 - 1 );
+        for ( i = 0; i < Limit; i++ )
+            Aig_InfoXorBit( Fra_ObjSim( Aig_ManPi(p->pManAig,i) ), i+1 );
+    }
 }
 
 /**Function*************************************************************
@@ -245,16 +247,18 @@ unsigned Fra_NodeHashSims( Aig_Obj_t * pObj )
   SeeAlso     []
 
 ***********************************************************************/
-void Fra_NodeSimulate( Fra_Man_t * p, Aig_Obj_t * pObj )
+void Fra_NodeSimulate( Fra_Man_t * p, Aig_Obj_t * pObj, int iFrame )
 {
     unsigned * pSims, * pSims0, * pSims1;
     int fCompl, fCompl0, fCompl1, i;
+    int nSimWords = p->pPars->nSimWords;
     assert( !Aig_IsComplement(pObj) );
     assert( Aig_ObjIsNode(pObj) );
+    assert( iFrame == 0 || nSimWords < p->nSimWords );
     // get hold of the simulation information
-    pSims  = Fra_ObjSim(pObj);
-    pSims0 = Fra_ObjSim(Aig_ObjFanin0(pObj));
-    pSims1 = Fra_ObjSim(Aig_ObjFanin1(pObj));
+    pSims  = Fra_ObjSim(pObj) + nSimWords * iFrame;
+    pSims0 = Fra_ObjSim(Aig_ObjFanin0(pObj)) + nSimWords * iFrame;
+    pSims1 = Fra_ObjSim(Aig_ObjFanin1(pObj)) + nSimWords * iFrame;
     // get complemented attributes of the children using their random info
     fCompl  = pObj->fPhase;
     fCompl0 = Aig_ObjFaninPhase(Aig_ObjChild0(pObj));
@@ -263,41 +267,103 @@ void Fra_NodeSimulate( Fra_Man_t * p, Aig_Obj_t * pObj )
     if ( fCompl0 && fCompl1 )
     {
         if ( fCompl )
-            for ( i = 0; i < p->nSimWords; i++ )
+            for ( i = 0; i < nSimWords; i++ )
                 pSims[i] = (pSims0[i] | pSims1[i]);
         else
-            for ( i = 0; i < p->nSimWords; i++ )
+            for ( i = 0; i < nSimWords; i++ )
                 pSims[i] = ~(pSims0[i] | pSims1[i]);
     }
     else if ( fCompl0 && !fCompl1 )
     {
         if ( fCompl )
-            for ( i = 0; i < p->nSimWords; i++ )
+            for ( i = 0; i < nSimWords; i++ )
                 pSims[i] = (pSims0[i] | ~pSims1[i]);
         else
-            for ( i = 0; i < p->nSimWords; i++ )
+            for ( i = 0; i < nSimWords; i++ )
                 pSims[i] = (~pSims0[i] & pSims1[i]);
     }
     else if ( !fCompl0 && fCompl1 )
     {
         if ( fCompl )
-            for ( i = 0; i < p->nSimWords; i++ )
+            for ( i = 0; i < nSimWords; i++ )
                 pSims[i] = (~pSims0[i] | pSims1[i]);
         else
-            for ( i = 0; i < p->nSimWords; i++ )
+            for ( i = 0; i < nSimWords; i++ )
                 pSims[i] = (pSims0[i] & ~pSims1[i]);
     }
     else // if ( !fCompl0 && !fCompl1 )
     {
         if ( fCompl )
-            for ( i = 0; i < p->nSimWords; i++ )
+            for ( i = 0; i < nSimWords; i++ )
                 pSims[i] = ~(pSims0[i] & pSims1[i]);
         else
-            for ( i = 0; i < p->nSimWords; i++ )
+            for ( i = 0; i < nSimWords; i++ )
                 pSims[i] = (pSims0[i] & pSims1[i]);
     }
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Simulates one node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Fra_NodeCopyFanin( Fra_Man_t * p, Aig_Obj_t * pObj, int iFrame )
+{
+    unsigned * pSims, * pSims0;
+    int fCompl, fCompl0, i;
+    int nSimWords = p->pPars->nSimWords;
+    assert( !Aig_IsComplement(pObj) );
+    assert( Aig_ObjIsPo(pObj) );
+    assert( iFrame == 0 || nSimWords < p->nSimWords );
+    // get hold of the simulation information
+    pSims  = Fra_ObjSim(pObj) + nSimWords * iFrame;
+    pSims0 = Fra_ObjSim(Aig_ObjFanin0(pObj)) + nSimWords * iFrame;
+    // get complemented attributes of the children using their random info
+    fCompl  = pObj->fPhase;
+    fCompl0 = Aig_ObjFaninPhase(Aig_ObjChild0(pObj));
+    // copy information as it is
+    if ( fCompl0 )
+        for ( i = 0; i < nSimWords; i++ )
+            pSims[i] = ~pSims0[i];
+    else
+        for ( i = 0; i < nSimWords; i++ )
+            pSims[i] = pSims0[i];
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Simulates one node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Fra_NodeTransferNext( Fra_Man_t * p, Aig_Obj_t * pOut, Aig_Obj_t * pIn, int iFrame )
+{
+    unsigned * pSims0, * pSims1;
+    int i, nSimWords = p->pPars->nSimWords;
+    assert( !Aig_IsComplement(pOut) );
+    assert( !Aig_IsComplement(pIn) );
+    assert( Aig_ObjIsPo(pOut) );
+    assert( Aig_ObjIsPi(pIn) );
+    assert( iFrame == 0 || nSimWords < p->nSimWords );
+    // get hold of the simulation information
+    pSims0 = Fra_ObjSim(pOut) + nSimWords * iFrame;
+    pSims1 = Fra_ObjSim(pIn) + nSimWords * (iFrame+1);
+    // copy information as it is
+    for ( i = 0; i < nSimWords; i++ )
+        pSims1[i] = pSims0[i];
+}
+
 
 /**Function*************************************************************
 
@@ -310,7 +376,7 @@ void Fra_NodeSimulate( Fra_Man_t * p, Aig_Obj_t * pObj )
   SeeAlso     []
 
 ***********************************************************************/
-void Fra_SavePattern0( Fra_Man_t * p )
+void Fra_SavePattern0( Fra_Man_t * p, int fInit )
 {
     memset( p->pPatWords, 0, sizeof(unsigned) * p->nPatWords );
 }
@@ -326,9 +392,17 @@ void Fra_SavePattern0( Fra_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-void Fra_SavePattern1( Fra_Man_t * p )
+void Fra_SavePattern1( Fra_Man_t * p, int fInit )
 {
+    Aig_Obj_t * pObj;
+    int i, k, nTruePis;
     memset( p->pPatWords, 0xff, sizeof(unsigned) * p->nPatWords );
+    if ( !fInit )
+        return;
+    nTruePis = Aig_ManPiNum(p->pManAig) - Aig_ManRegNum(p->pManAig);
+    k = 0;
+    Aig_ManForEachLoSeq( p->pManAig, pObj, i )
+        Aig_InfoXorBit( p->pPatWords, nTruePis * p->nFramesAll + k++ );
 }
 
 /**Function*************************************************************
@@ -350,6 +424,12 @@ void Fra_SavePattern( Fra_Man_t * p )
     Aig_ManForEachPi( p->pManFraig, pObj, i )
         if ( p->pSat->model.ptr[Fra_ObjSatNum(pObj)] == l_True )
             Aig_InfoSetBit( p->pPatWords, i );
+/*
+    printf( "Pattern: " );
+    Aig_ManForEachPi( p->pManFraig, pObj, i )
+        printf( "%d", Aig_InfoHasBit( p->pPatWords, i ) );
+    printf( "\n" );
+*/
 }
 
 /**Function*************************************************************
@@ -454,19 +534,22 @@ int Fra_SelectBestPat( Fra_Man_t * p )
 void Fra_SimulateOne( Fra_Man_t * p )
 {
     Aig_Obj_t * pObj;
-    int i, clk;
+    int f, i, clk;
 clk = clock();
-    Aig_ManForEachNode( p->pManAig, pObj, i )
+    for ( f = 0; f < p->nFramesAll; f++ )
     {
-        Fra_NodeSimulate( p, pObj );
-/*
-        if ( Aig_ObjFraig(pObj) == NULL )
-            printf( "%3d --- -- %d  :  ", pObj->Id, pObj->fPhase );
-        else
-            printf( "%3d %3d %2d %d  :  ", pObj->Id, Aig_Regular(Aig_ObjFraig(pObj))->Id, Aig_ObjSatNum(Aig_Regular(Aig_ObjFraig(pObj))), pObj->fPhase );
-        Extra_PrintBinary( stdout, Fra_ObjSim(pObj), 30 );
-        printf( "\n" );
-*/
+        // simulate the nodes
+        Aig_ManForEachNode( p->pManAig, pObj, i )
+            Fra_NodeSimulate( p, pObj, f );
+        if ( f == p->nFramesAll - 1 )
+            break;
+        // copy simulation info into outputs
+        Aig_ManForEachLiSeq( p->pManAig, pObj, i )
+            Fra_NodeCopyFanin( p, pObj, f );
+        // copy simulation info into the inputs
+        for ( i = 0; i < Aig_ManRegNum(p->pManAig); i++ )
+            Fra_NodeTransferNext( p, Aig_ManLi(p->pManAig, i), Aig_ManLo(p->pManAig, i), f );
+
     }
 p->timeSim += clock() - clk;
 p->nSimRounds++;
@@ -536,14 +619,16 @@ p->timeRef += clock() - clk;
 void Fra_Simulate( Fra_Man_t * p, int fInit )
 {
     int nChanges, nClasses, clk;
-    assert( !fInit || Aig_ManInitNum(p->pManAig) );
+    assert( !fInit || Aig_ManRegNum(p->pManAig) );
     // start the classes
     Fra_AssignRandom( p, fInit );
     Fra_SimulateOne( p );
     Fra_ClassesPrepare( p->pCla );
+//    Fra_ClassesPrint( p->pCla );
 //printf( "Starting classes = %5d.   Pairs = %6d.\n", p->lClasses.nItems, Fra_CountPairsClasses(p) );
+
     // refine classes by walking 0/1 patterns
-    Fra_SavePattern0( p );
+    Fra_SavePattern0( p, fInit );
     Fra_AssignDist1( p, p->pPatWords );
     Fra_SimulateOne( p );
     if ( p->pPars->fProve && Fra_CheckOutputSims(p) )
@@ -553,7 +638,7 @@ clk = clock();
     nChanges += Fra_ClassesRefine1( p->pCla );
 p->timeRef += clock() - clk;
 //printf( "Refined classes  = %5d.   Changes = %4d.   Pairs = %6d.\n", p->lClasses.nItems, nChanges, Fra_CountPairsClasses(p) );
-    Fra_SavePattern1( p );
+    Fra_SavePattern1( p, fInit );
     Fra_AssignDist1( p, p->pPatWords );
     Fra_SimulateOne( p );
     if ( p->pPars->fProve && Fra_CheckOutputSims(p) )
@@ -562,6 +647,7 @@ clk = clock();
     nChanges = Fra_ClassesRefine( p->pCla );
     nChanges += Fra_ClassesRefine1( p->pCla );
 p->timeRef += clock() - clk;
+
 //printf( "Refined classes  = %5d.   Changes = %4d.   Pairs = %6d.\n", p->lClasses.nItems, nChanges, Fra_CountPairsClasses(p) );
     // refine classes by random simulation
     do {
@@ -576,6 +662,11 @@ clk = clock();
 p->timeRef += clock() - clk;
 //printf( "Refined classes  = %5d.   Changes = %4d.   Pairs = %6d.\n", p->lClasses.nItems, nChanges, Fra_CountPairsClasses(p) );
     } while ( (double)nChanges / nClasses > p->pPars->dSimSatur );
+
+//    if ( p->pPars->fVerbose )
+//    printf( "Consts = %6d. Classes = %6d. Literals = %6d.\n", 
+//        Vec_PtrSize(p->pCla->vClasses1), Vec_PtrSize(p->pCla->vClasses), Fra_ClassesCountLits(p->pCla) );
+
 //    Fra_ClassesPrint( p->pCla );
 }