Version abc80921

author: Alan Mishchenko <alanmi@berkeley.edu> 2008-09-21 08:01:00 -0700
committer: Alan Mishchenko <alanmi@berkeley.edu> 2008-09-21 08:01:00 -0700
commit: 4d71c114a3405f0a2c59a8467c82a8da3f785262 (patch)
tree: 1c4a0fdf938e247b03e832f26c74c8a48af2826b /src
parent: 3429e6309d0fc9a2d35d81f6483258c6af2fab50 (diff)
download: abc-4d71c114a3405f0a2c59a8467c82a8da3f785262.tar.gz
abc-4d71c114a3405f0a2c59a8467c82a8da3f785262.tar.bz2
abc-4d71c114a3405f0a2c59a8467c82a8da3f785262.zip
23 files changed, 510 insertions, 527 deletions
diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h
index 093912c3..fcaf41fa 100644
--- a/src/aig/aig/aig.h
+++ b/src/aig/aig/aig.h
@@ -471,6 +471,7 @@ extern int             Aig_ManChoiceLevel( 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 Vec_Ptr_t *     Aig_Support( Aig_Man_t * p, Aig_Obj_t * pObj );
+extern void            Aig_SupportNodes( Aig_Man_t * p, Aig_Obj_t ** ppObjs, int nObjs, Vec_Ptr_t * vSupp );
 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 );
diff --git a/src/aig/aig/aigDfs.c b/src/aig/aig/aigDfs.c
index 3c6658d9..568d6a68 100644
--- a/src/aig/aig/aigDfs.c
+++ b/src/aig/aig/aigDfs.c
@@ -734,6 +734,33 @@ Vec_Ptr_t * Aig_Support( Aig_Man_t * p, Aig_Obj_t * pObj )
 
 /**Function*************************************************************
 
+  Synopsis    [Counts the support size of the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_SupportNodes( Aig_Man_t * p, Aig_Obj_t ** ppObjs, int nObjs, Vec_Ptr_t * vSupp )
+{
+    int i;
+    Vec_PtrClear( vSupp );
+    Aig_ManIncrementTravId( p );
+    Aig_ObjSetTravIdCurrent( p, Aig_ManConst1(p) );
+    for ( i = 0; i < nObjs; i++ )
+    {
+        assert( !Aig_IsComplement(ppObjs[i]) );
+        if ( Aig_ObjIsPo(ppObjs[i]) )
+            Aig_Support_rec( p, Aig_ObjFanin0(ppObjs[i]), vSupp );
+        else
+            Aig_Support_rec( p, ppObjs[i], vSupp );
+    }
+}
+
+/**Function*************************************************************
+
   Synopsis    [Transfers the AIG from one manager into another.]
 
   Description []
diff --git a/src/aig/dch/dchSat.c b/src/aig/dch/dchSat.c
index 66c7f7b9..07196259 100644
--- a/src/aig/dch/dchSat.c
+++ b/src/aig/dch/dchSat.c
@@ -50,13 +50,13 @@ int Dch_NodesAreEquiv( Dch_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew )
     assert( !Aig_IsComplement(pOld) );
     assert( pNew != pOld );
 
-//    p->nCallsSince++;  // experiment with this!!!
+    p->nCallsSince++;  // experiment with this!!!
     
     // check if SAT solver needs recycling
     if ( p->pSat == NULL || 
         (p->pPars->nSatVarMax && 
          p->nSatVars > p->pPars->nSatVarMax && 
-         ++p->nCallsSince > p->pPars->nCallsRecycle) )
+         p->nCallsSince > p->pPars->nCallsRecycle) )
         Dch_ManSatSolverRecycle( p );
 
     // if the nodes do not have SAT variables, allocate them
diff --git a/src/aig/dch/dchSimSat.c b/src/aig/dch/dchSimSat.c
index 7a6865bd..61d2ab93 100644
--- a/src/aig/dch/dchSimSat.c
+++ b/src/aig/dch/dchSimSat.c
@@ -60,10 +60,10 @@ void Dch_ManCollectTfoCands_rec( Dch_Man_t * p, Aig_Obj_t * pObj )
         Vec_PtrPush( p->vSimRoots, pObj );
         return;
     }
-    // pRepr is the representative of the equivalence class
-    if ( Aig_ObjIsTravIdCurrent(p->pAigTotal, pRepr) )
+    // pRepr is the representative of an equivalence class
+    if ( pRepr->fMarkA )
         return;
-    Aig_ObjSetTravIdCurrent(p->pAigTotal, pRepr);
+    pRepr->fMarkA = 1;
     Vec_PtrPush( p->vSimClasses, pRepr );
 }
 
@@ -80,6 +80,8 @@ void Dch_ManCollectTfoCands_rec( Dch_Man_t * p, Aig_Obj_t * pObj )
 ***********************************************************************/
 void Dch_ManCollectTfoCands( Dch_Man_t * p, Aig_Obj_t * pObj1, Aig_Obj_t * pObj2 )
 {
+    Aig_Obj_t * pObj;
+    int i;
     Vec_PtrClear( p->vSimRoots );
     Vec_PtrClear( p->vSimClasses );
     Aig_ManIncrementTravId( p->pAigTotal );
@@ -88,6 +90,8 @@ void Dch_ManCollectTfoCands( Dch_Man_t * p, Aig_Obj_t * pObj1, Aig_Obj_t * pObj2
     Dch_ManCollectTfoCands_rec( p, pObj2 );
     Vec_PtrSort( p->vSimRoots, Aig_ObjCompareIdIncrease );
     Vec_PtrSort( p->vSimClasses, Aig_ObjCompareIdIncrease );
+    Vec_PtrForEachEntry( p->vSimClasses, pObj, i )
+        pObj->fMarkA = 0;
 }
 
 /**Function*************************************************************
@@ -116,6 +120,7 @@ void Dch_ManResimulateSolved_rec( Dch_Man_t * p, Aig_Obj_t * pObj )
         // get the value from the SAT solver
         // (account for the fact that some vars may be minimized away)
         pObj->fMarkB = !nVarNum? 0 : sat_solver_var_value( p->pSat, nVarNum );
+//        pObj->fMarkB = !nVarNum? Aig_ManRandom(0) & 1 : sat_solver_var_value( p->pSat, nVarNum );
         return;
     }
     Dch_ManResimulateSolved_rec( p, Aig_ObjFanin0(pObj) );
diff --git a/src/aig/fra/fraSec.c b/src/aig/fra/fraSec.c
index 677123d8..232a789e 100644
--- a/src/aig/fra/fraSec.c
+++ b/src/aig/fra/fraSec.c
@@ -93,8 +93,6 @@ int Fra_FraigSec( Aig_Man_t * p, Fra_Sec_t * pParSec )
         goto finish;
 
     // prepare parameters
-    Ssw_ManSetDefaultParams( pPars2 );
-    // prepare parameters
     memset( pPars, 0, sizeof(Fra_Ssw_t) );
     pPars->fLatchCorr  = fLatchCorr;
     pPars->fVerbose = pParSec->fVeryVerbose;
@@ -142,7 +140,8 @@ PRT( "Time", clock() - clk );
     if ( pParSec->fRetimeFirst && pNew->nRegs )
     {
 clk = clock();
-    pNew = Rtm_ManRetime( pTemp = pNew, 1, 1000, 0 );
+//    pNew = Rtm_ManRetime( pTemp = pNew, 1, 1000, 0 );
+    pNew = Saig_ManRetimeForward( pTemp = pNew, 100, 0 );
     Aig_ManStop( pTemp );
     if ( pParSec->fVerbose )
     {
@@ -172,11 +171,21 @@ clk = clock();
             goto finish;
         }
     }
-    pNew = Fra_FraigLatchCorrespondence( pTemp = pNew, 0, 1000, 1, pParSec->fVeryVerbose, &nIter, TimeLeft );
+
+
+//    pNew = Fra_FraigLatchCorrespondence( pTemp = pNew, 0, 1000, 1, pParSec->fVeryVerbose, &nIter, TimeLeft );
+//Aig_ManDumpBlif( pNew, "ex.blif", NULL, NULL );
+    Ssw_ManSetDefaultParamsLcorr( pPars2 );
+    pNew = Ssw_LatchCorrespondence( pTemp = pNew, pPars2 );
+    nIter = pPars2->nIters;
+
+    // prepare parameters for scorr
+    Ssw_ManSetDefaultParams( pPars2 );
+
     if ( pTemp->pSeqModel )
     {
         if ( !Ssw_SmlRunCounterExample( pTemp, pTemp->pSeqModel ) )
-            printf( "Fra_FraigLatchCorrespondence(): Counter-example verification has FAILED.\n" );
+            printf( "Fra_FraigSec(): Counter-example verification has FAILED.\n" );
         if ( Saig_ManPiNum(p) != Saig_ManPiNum(pTemp) )
             printf( "The counter-example is invalid because of phase abstraction.\n" );
         else
diff --git a/src/aig/int/intCtrex.c b/src/aig/int/intCtrex.c
index 5e417ce0..4cbe2007 100644
--- a/src/aig/int/intCtrex.c
+++ b/src/aig/int/intCtrex.c
@@ -66,7 +66,10 @@ Aig_Man_t * Inter_ManFramesBmc( Aig_Man_t * pAig, int nFrames )
             break;
         // transfer to register outputs
         Saig_ManForEachLiLo(  pAig, pObjLi, pObjLo, i )
-            pObjLo->pData = pObjLi->pData = Aig_ObjChild0Copy(pObjLi);
+            pObjLi->pData = Aig_ObjChild0Copy(pObjLi);
+        // transfer to register outputs
+        Saig_ManForEachLiLo(  pAig, pObjLi, pObjLo, i )
+            pObjLo->pData = pObjLi->pData;
     }
     // create POs for the output of the last frame
     pObj = Aig_ManPo( pAig, 0 );
diff --git a/src/aig/ntl/ntlFraig.c b/src/aig/ntl/ntlFraig.c
index b1239e47..27d863af 100644
--- a/src/aig/ntl/ntlFraig.c
+++ b/src/aig/ntl/ntlFraig.c
@@ -435,6 +435,7 @@ Ntl_Man_t * Ntl_ManScl( Ntl_Man_t * p, int fLatchConst, int fLatchEqual, int fVe
 ***********************************************************************/
 Ntl_Man_t * Ntl_ManLcorr( Ntl_Man_t * p, int nConfMax, int fVerbose )
 {
+    Ssw_Pars_t Pars, * pPars = &Pars;
     Ntl_Man_t * pNew, * pAux;
     Aig_Man_t * pAig, * pAigCol, * pTemp;
 
@@ -444,7 +445,12 @@ Ntl_Man_t * Ntl_ManLcorr( Ntl_Man_t * p, int nConfMax, int fVerbose )
     pAigCol = Ntl_ManCollapseSeq( pNew, 0 );
 
     // perform SCL for the given design
-    pTemp = Fra_FraigLatchCorrespondence( pAigCol, 0, nConfMax, 0, fVerbose, NULL, 0 );
+//    pTemp = Fra_FraigLatchCorrespondence( pAigCol, 0, nConfMax, 0, fVerbose, NULL, 0 );
+    Ssw_ManSetDefaultParamsLcorr( pPars );
+    pPars->nBTLimit = nConfMax;
+    pPars->fVerbose = fVerbose;
+    pTemp = Ssw_LatchCorrespondence( pAigCol, pPars );
+
     Aig_ManStop( pTemp );
     if ( p->vRegClasses && Vec_IntSize(p->vRegClasses) && pAigCol->pReprs )
         Ntl_ManFilterRegisterClasses( pAigCol, p->vRegClasses, fVerbose );
diff --git a/src/aig/ssw/ssw.h b/src/aig/ssw/ssw.h
index 2917f6d4..8d74f16b 100644
--- a/src/aig/ssw/ssw.h
+++ b/src/aig/ssw/ssw.h
@@ -50,11 +50,12 @@ struct Ssw_Pars_t_
     int              nBTLimit;      // conflict limit at a node
     int              nMinDomSize;   // min clock domain considered for optimization
     int              fPolarFlip;    // uses polarity adjustment
+    int              fSkipCheck;    // do not run equivalence check for unaffected cones
     int              fLatchCorr;    // perform register correspondence
+    // optimized latch correspondence
     int              fLatchCorrOpt; // perform register correspondence (optimized)
     int              nSatVarMax;    // max number of SAT vars before recycling SAT solver (optimized latch corr only)
-    int              nCallsRecycle; // calls to perform before recycling SAT solver (optimized latch corr only)
-    int              fSkipCheck;    // does not run equivalence check for unaffected cones
+    int              nRecycleCalls; // calls to perform before recycling SAT solver (optimized latch corr only)
     int              fVerbose;      // verbose stats
     // internal parameters
     int              nIters;        // the number of iterations performed
@@ -82,7 +83,9 @@ struct Ssw_Cex_t_
 
 /*=== sswCore.c ==========================================================*/
 extern void          Ssw_ManSetDefaultParams( Ssw_Pars_t * p );
-extern Aig_Man_t *   Ssw_SignalCorrespondence( Aig_Man_t * p, Ssw_Pars_t * pPars );
+extern void          Ssw_ManSetDefaultParamsLcorr( Ssw_Pars_t * p );
+extern Aig_Man_t *   Ssw_SignalCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars );
+extern Aig_Man_t *   Ssw_LatchCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars );
 /*=== sswPart.c ==========================================================*/
 extern Aig_Man_t *   Ssw_SignalCorrespondencePart( Aig_Man_t * pAig, Ssw_Pars_t * pPars );
 /*=== sswPairs.c ===================================================*/
diff --git a/src/aig/ssw/sswAig.c b/src/aig/ssw/sswAig.c
index 854a0e12..5a47ba5f 100644
--- a/src/aig/ssw/sswAig.c
+++ b/src/aig/ssw/sswAig.c
@@ -49,9 +49,9 @@ static inline void Ssw_FramesConstrainNode( Ssw_Man_t * p, Aig_Man_t * pFrames,
     p->nConstrTotal++;
     assert( pObjRepr->Id < pObj->Id );
     // get the new node 
-    pObjNew = Ssw_ObjFraig( p, pObj, iFrame );
+    pObjNew = Ssw_ObjFrame( p, pObj, iFrame );
     // get the new node of the representative
-    pObjReprNew = Ssw_ObjFraig( p, pObjRepr, iFrame );
+    pObjReprNew = Ssw_ObjFrame( p, pObjRepr, iFrame );
     // if this is the same node, no need to add constraints
     if ( pObj->fPhase == pObjRepr->fPhase )
     {
@@ -69,7 +69,7 @@ static inline void Ssw_FramesConstrainNode( Ssw_Man_t * p, Aig_Man_t * pFrames,
     // these are different nodes - perform speculative reduction
     pObjNew2 = Aig_NotCond( pObjReprNew, pObj->fPhase ^ pObjRepr->fPhase );
     // set the new node
-    Ssw_ObjSetFraig( p, pObj, iFrame, pObjNew2 );
+    Ssw_ObjSetFrame( p, pObj, iFrame, pObjNew2 );
     // add the constraint
     Aig_ObjCreatePo( pFrames, pObjNew2 );
     Aig_ObjCreatePo( pFrames, pObjNew );
@@ -99,15 +99,15 @@ Aig_Man_t * Ssw_FramesWithClasses( Ssw_Man_t * p )
     pFrames = Aig_ManStart( Aig_ManObjNumMax(p->pAig) * p->nFrames );
     // create latches for the first frame
     Saig_ManForEachLo( p->pAig, pObj, i )
-        Ssw_ObjSetFraig( p, pObj, 0, Aig_ObjCreatePi(pFrames) );
+        Ssw_ObjSetFrame( p, pObj, 0, Aig_ObjCreatePi(pFrames) );
     // add timeframes
     p->nConstrTotal = p->nConstrReduced = 0;
     for ( f = 0; f < p->pPars->nFramesK; f++ )
     {
         // map constants and PIs
-        Ssw_ObjSetFraig( p, Aig_ManConst1(p->pAig), f, Aig_ManConst1(pFrames) );
+        Ssw_ObjSetFrame( p, Aig_ManConst1(p->pAig), f, Aig_ManConst1(pFrames) );
         Aig_ManForEachPiSeq( p->pAig, pObj, i )
-            Ssw_ObjSetFraig( p, pObj, f, Aig_ObjCreatePi(pFrames) );
+            Ssw_ObjSetFrame( p, pObj, f, Aig_ObjCreatePi(pFrames) );
         // set the constraints on the latch outputs
         Aig_ManForEachLoSeq( p->pAig, pObj, i )
             Ssw_FramesConstrainNode( p, pFrames, p->pAig, pObj, f );
@@ -115,16 +115,16 @@ Aig_Man_t * Ssw_FramesWithClasses( Ssw_Man_t * p )
         Aig_ManForEachNode( p->pAig, pObj, i )
         {
             pObjNew = Aig_And( pFrames, Ssw_ObjChild0Fra(p, pObj, f), Ssw_ObjChild1Fra(p, pObj, f) );
-            Ssw_ObjSetFraig( p, pObj, f, pObjNew );
+            Ssw_ObjSetFrame( p, pObj, f, pObjNew );
             Ssw_FramesConstrainNode( p, pFrames, p->pAig, pObj, f );
         }
         // transfer latch input to the latch outputs 
         Saig_ManForEachLiLo( p->pAig, pObjLi, pObjLo, i )
-            Ssw_ObjSetFraig( p, pObjLo, f+1, Ssw_ObjChild0Fra(p, pObjLi,f) );
+            Ssw_ObjSetFrame( p, pObjLo, f+1, Ssw_ObjChild0Fra(p, pObjLi,f) );
     }
     // add the POs for the latch outputs of the last frame
     Saig_ManForEachLo( p->pAig, pObj, i )
-        Aig_ObjCreatePo( pFrames, Ssw_ObjFraig( p, pObj, p->pPars->nFramesK ) );
+        Aig_ObjCreatePo( pFrames, Ssw_ObjFrame( p, pObj, p->pPars->nFramesK ) );
 
     // remove dangling nodes
     Aig_ManCleanup( pFrames );
diff --git a/src/aig/ssw/sswClass.c b/src/aig/ssw/sswClass.c
index 81e8de8b..db593311 100644
--- a/src/aig/ssw/sswClass.c
+++ b/src/aig/ssw/sswClass.c
@@ -286,6 +286,8 @@ int Ssw_ClassesLitNum( Ssw_Cla_t * p )
 ***********************************************************************/
 Aig_Obj_t ** Ssw_ClassesReadClass( Ssw_Cla_t * p, Aig_Obj_t * pRepr, int * pnSize )
 {
+    if ( p->pId2Class[pRepr->Id] == NULL )
+        return NULL;
     assert( p->pId2Class[pRepr->Id] != NULL );
     assert( p->pClassSizes[pRepr->Id] > 1 );
     *pnSize = p->pClassSizes[pRepr->Id];
@@ -333,6 +335,7 @@ void Ssw_ClassesCheck( Ssw_Cla_t * p )
     Ssw_ManForEachClass( p, ppClass, k )
     {
         pPrev = NULL;
+        assert( p->pClassSizes[ppClass[0]->Id] >= 2 );
         Ssw_ClassForEachNode( p, ppClass[0], pObj, i )
         {
             if ( i == 0 )
@@ -423,12 +426,15 @@ void Ssw_ClassesPrint( Ssw_Cla_t * p, int fVeryVerbose )
 void Ssw_ClassesRemoveNode( Ssw_Cla_t * p, Aig_Obj_t * pObj )
 {
     Aig_Obj_t * pRepr, * pTemp;
+    assert( p->pClassSizes[pObj->Id] == 0 );
     assert( p->pId2Class[pObj->Id] == NULL );
     pRepr = Aig_ObjRepr( p->pAig, pObj );
     assert( pRepr != NULL );
     Vec_PtrPush( p->vRefined, pObj );
     if ( Ssw_ObjIsConst1Cand( p->pAig, pObj ) )
     {
+        assert( p->pClassSizes[pRepr->Id] == 0 );
+        assert( p->pId2Class[pRepr->Id] == NULL );
         Aig_ObjSetRepr( p->pAig, pObj, NULL );
         p->nCands1--;
         return;
@@ -439,7 +445,7 @@ void Ssw_ClassesRemoveNode( Ssw_Cla_t * p, Aig_Obj_t * pObj )
     assert( p->pClassSizes[pRepr->Id] >= 2 );
     if ( p->pClassSizes[pRepr->Id] == 2 )
     {
-        p->pId2Class[pObj->Id] = NULL;
+        p->pId2Class[pRepr->Id] = NULL;
         p->nClasses--;
         p->pClassSizes[pRepr->Id] = 0;
         p->nLits--;
@@ -491,7 +497,7 @@ PRT( "Simulation of 32 frames with 4 words", clock() - clk );
 
     // set comparison procedures
 clk = clock();
-    Ssw_ClassesSetData( p, pSml, Ssw_SmlNodeHash, Ssw_SmlNodeIsConst, Ssw_SmlNodesAreEqual );
+    Ssw_ClassesSetData( p, pSml, Ssw_SmlObjHashWord, Ssw_SmlObjIsConstWord, Ssw_SmlObjsAreEqualWord );
 
     // allocate the hash table hashing simulation info into nodes
     nTableSize = Aig_PrimeCudd( Aig_ManObjNumMax(p->pAig)/4 );
@@ -593,38 +599,6 @@ PRT( "Collecting candidate equival classes", clock() - clk );
 
 /**Function*************************************************************
 
-  Synopsis    [Returns 1 if the node appears to be constant 1 candidate.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Ssw_NodeIsConstCex( void * p, Aig_Obj_t * pObj )
-{
-    return pObj->fPhase == pObj->fMarkB;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Returns 1 if the nodes appear equal.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Ssw_NodesAreEqualCex( void * p, Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 )
-{
-    return (pObj0->fPhase == pObj1->fPhase) == (pObj0->fMarkB == pObj1->fMarkB);
-}
-
-/**Function*************************************************************
-
   Synopsis    [Creates initial simulation classes.]
 
   Description [Assumes that simulation info is assigned.]
diff --git a/src/aig/ssw/sswCore.c b/src/aig/ssw/sswCore.c
index 6a3e9264..fc9f5672 100644
--- a/src/aig/ssw/sswCore.c
+++ b/src/aig/ssw/sswCore.c
@@ -50,18 +50,37 @@ void Ssw_ManSetDefaultParams( Ssw_Pars_t * p )
     p->nBTLimit       =  1000;  // conflict limit at a node
     p->nMinDomSize    =   100;  // min clock domain considered for optimization
     p->fPolarFlip     =     0;  // uses polarity adjustment
+    p->fSkipCheck     =     0;  // do not run equivalence check for unaffected cones
     p->fLatchCorr     =     0;  // performs register correspondence
     p->fVerbose       =     0;  // verbose stats
     // latch correspondence
     p->fLatchCorrOpt  =     0;  // performs optimized register correspondence
-    p->nSatVarMax     =  5000;  // the max number of SAT variables
-    p->nCallsRecycle  =   100;  // calls to perform before recycling SAT solver
+    p->nSatVarMax     =  1000;  // the max number of SAT variables
+    p->nRecycleCalls  =    50;  // calls to perform before recycling SAT solver
     // return values
     p->nIters         =     0;  // the number of iterations performed
 }
 
 /**Function*************************************************************
 
+  Synopsis    [This procedure sets default parameters.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ssw_ManSetDefaultParamsLcorr( Ssw_Pars_t * p )
+{
+    Ssw_ManSetDefaultParams( p );
+    p->fLatchCorrOpt = 1;
+    p->nBTLimit      = 10000;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Performs computation of signal correspondence with constraints.]
 
   Description []
@@ -73,6 +92,7 @@ void Ssw_ManSetDefaultParams( Ssw_Pars_t * p )
 ***********************************************************************/
 Aig_Man_t * Ssw_SignalCorrespondenceRefine( Ssw_Man_t * p )
 {
+    int nSatProof, nSatCallsSat, nRecycles, nSatFailsReal;
     Aig_Man_t * pAigNew;
     int RetValue, nIter;
     int clk, clkTotal = clock();
@@ -97,23 +117,40 @@ Aig_Man_t * Ssw_SignalCorrespondenceRefine( Ssw_Man_t * p )
         Ssw_ClassesPrint( p->ppClasses, 0 );
     }
     // refine classes using induction
+    nSatProof = nSatCallsSat = nRecycles = nSatFailsReal = 0;
     for ( nIter = 0; ; nIter++ )
     {
 clk = clock();
         if ( p->pPars->fLatchCorrOpt )
+        {
             RetValue = Ssw_ManSweepLatch( p );
+            if ( p->pPars->fVerbose )
+            {
+                printf( "%3d : Const = %6d. Cl = %6d. Pr = %5d. Cex = %5d. Rcl = %3d. F = %3d. ", 
+                    nIter, Ssw_ClassesCand1Num(p->ppClasses), Ssw_ClassesClassNum(p->ppClasses), 
+                    p->nSatProof-nSatProof, p->nSatCallsSat-nSatCallsSat, 
+                    p->nRecycles-nRecycles, p->nSatFailsReal-nSatFailsReal );
+                PRT( "T", clock() - clk );
+                nSatProof     = p->nSatProof;
+                nSatCallsSat  = p->nSatCallsSat;
+                nRecycles     = p->nRecycles;
+                nSatFailsReal = p->nSatFailsReal;
+            } 
+        }
         else
-            RetValue = Ssw_ManSweep( p );
-        if ( p->pPars->fVerbose )
         {
-            printf( "%3d : Const = %6d. Cl = %6d. LR = %6d. NR = %6d. F = %5d. ", 
-                nIter, Ssw_ClassesCand1Num(p->ppClasses), Ssw_ClassesClassNum(p->ppClasses), 
-                p->nConstrReduced, Aig_ManNodeNum(p->pFrames), p->nSatFailsReal );
-            if ( p->pPars->fSkipCheck )
-                printf( "Use = %5d. Skip = %5d. ", 
-                    p->nRefUse, p->nRefSkip );
-            PRT( "T", clock() - clk );
-        } 
+            RetValue = Ssw_ManSweep( p );
+            if ( p->pPars->fVerbose )
+            {
+                printf( "%3d : Const = %6d. Cl = %6d. LR = %6d. NR = %6d. F = %5d. ", 
+                    nIter, Ssw_ClassesCand1Num(p->ppClasses), Ssw_ClassesClassNum(p->ppClasses), 
+                    p->nConstrReduced, Aig_ManNodeNum(p->pFrames), p->nSatFailsReal );
+                if ( p->pPars->fSkipCheck )
+                    printf( "Use = %5d. Skip = %5d. ", 
+                        p->nRefUse, p->nRefSkip );
+                PRT( "T", clock() - clk );
+            } 
+        }
         Ssw_ManCleanup( p );
         if ( !RetValue )
             break;
@@ -161,7 +198,10 @@ Aig_Man_t * Ssw_SignalCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars )
     }
     // check and update parameters
     if ( pPars->fLatchCorrOpt )
+    {
         pPars->fLatchCorr = 1;
+        pPars->nFramesAddSim = 0;
+    }
     else
     {
         assert( pPars->nFramesK > 0 );
@@ -181,13 +221,13 @@ Aig_Man_t * Ssw_SignalCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars )
         // perform one round of seq simulation and generate candidate equivalence classes
         p->ppClasses = Ssw_ClassesPrepare( pAig, pPars->fLatchCorr, pPars->nMaxLevs, pPars->fVerbose );
         p->pSml = Ssw_SmlStart( pAig, 0, p->nFrames + p->pPars->nFramesAddSim, 1 );
-        Ssw_ClassesSetData( p->ppClasses, p->pSml, Ssw_SmlNodeHash, Ssw_SmlNodeIsConst, Ssw_SmlNodesAreEqual );
+        Ssw_ClassesSetData( p->ppClasses, p->pSml, Ssw_SmlObjHashWord, Ssw_SmlObjIsConstWord, Ssw_SmlObjsAreEqualWord );
     }
     else
     {
         // create trivial equivalence classes with all nodes being candidates for constant 1
         p->ppClasses = Ssw_ClassesPrepareSimple( pAig, pPars->fLatchCorr, pPars->nMaxLevs );
-        Ssw_ClassesSetData( p->ppClasses, NULL, NULL, Ssw_NodeIsConstCex, Ssw_NodesAreEqualCex );
+        Ssw_ClassesSetData( p->ppClasses, NULL, NULL, Ssw_SmlObjIsConstBit, Ssw_SmlObjsAreEqualBit );
     }
     // perform refinement of classes
     pAigNew = Ssw_SignalCorrespondenceRefine( p );    
@@ -196,6 +236,24 @@ Aig_Man_t * Ssw_SignalCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars )
     return pAigNew;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Performs computation of latch correspondence.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Ssw_LatchCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars )
+{
+    Ssw_Pars_t Pars;
+    if ( pPars == NULL )
+        Ssw_ManSetDefaultParamsLcorr( pPars = &Pars );
+    return Ssw_SignalCorrespondence( pAig, pPars );
+}
 
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/ssw/sswInt.h b/src/aig/ssw/sswInt.h
index 5b4377c7..faa3a87d 100644
--- a/src/aig/ssw/sswInt.h
+++ b/src/aig/ssw/sswInt.h
@@ -53,25 +53,31 @@ struct Ssw_Man_t_
     // AIGs used in the package
     Aig_Man_t *      pAig;           // user-given AIG
     Aig_Man_t *      pFrames;        // final AIG
-    Aig_Obj_t **     pNodeToFraig;   // mapping of AIG nodes into FRAIG nodes
+    Aig_Obj_t **     pNodeToFrames;  // mapping of AIG nodes into FRAIG nodes
     // equivalence classes
     Ssw_Cla_t *      ppClasses;      // equivalence classes of nodes
     int              fRefined;       // is set to 1 when refinement happens
-    int              nRefUse;
-    int              nRefSkip;  
+    int              nRefUse;        // the number of equivalences used
+    int              nRefSkip;       // the number of equivalences skipped  
     // SAT solving
     sat_solver *     pSat;           // recyclable SAT solver
     int              nSatVars;       // the counter of SAT variables
     int *            pSatVars;       // mapping of each node into its SAT var
     int              nSatVarsTotal;  // the total number of SAT vars created
     Vec_Ptr_t *      vFanins;        // fanins of the CNF node
-    Vec_Ptr_t *      vSimRoots;      // the roots of cand const 1 nodes to simulate
-    Vec_Ptr_t *      vSimClasses;    // the roots of cand equiv classes to simulate
     // SAT solving (latch corr only)
-    int              nCallsSince;    // the number of calls since last recycling
-    int              nRecycles;      // the number of time SAT solver was recycled
     Vec_Ptr_t *      vUsedNodes;     // the nodes with SAT variables
     Vec_Ptr_t *      vUsedPis;       // the PIs with SAT variables
+    Vec_Ptr_t *      vSimInfo;       // simulation information for the framed PIs
+    int              nPatterns;      // the number of patterns saved
+    int              nSimRounds;     // the number of simulation rounds performed
+    int              nCallsCount;    // the number of calls in this round
+    int              nCallsDelta;    // the number of calls to skip
+    int              nCallsSat;      // the number of SAT calls in this round
+    int              nCallsUnsat;    // the number of UNSAT calls in this round
+    int              nRecycleCalls;  // the number of calls since last recycling
+    int              nRecycles;      // the number of time SAT solver was recycled
+    int              nConeMax;       // the maximum cone size
     // sequential simulator
     Ssw_Sml_t *      pSml;
     // counter example storage
@@ -125,11 +131,11 @@ static inline void Ssw_ObjSetConst1Cand( Aig_Man_t * pAig, Aig_Obj_t * pObj )
     Aig_ObjSetRepr( pAig, pObj, Aig_ManConst1(pAig) );
 }
 
-static inline Aig_Obj_t * Ssw_ObjFraig( Ssw_Man_t * p, Aig_Obj_t * pObj, int i )                       { return p->pNodeToFraig[p->nFrames*pObj->Id + i];  }
-static inline void        Ssw_ObjSetFraig( Ssw_Man_t * p, Aig_Obj_t * pObj, int i, Aig_Obj_t * pNode ) { p->pNodeToFraig[p->nFrames*pObj->Id + i] = pNode; }
+static inline Aig_Obj_t * Ssw_ObjFrame( Ssw_Man_t * p, Aig_Obj_t * pObj, int i )                       { return p->pNodeToFrames[p->nFrames*pObj->Id + i];  }
+static inline void        Ssw_ObjSetFrame( Ssw_Man_t * p, Aig_Obj_t * pObj, int i, Aig_Obj_t * pNode ) { p->pNodeToFrames[p->nFrames*pObj->Id + i] = pNode; }
 
-static inline Aig_Obj_t * Ssw_ObjChild0Fra( Ssw_Man_t * p, Aig_Obj_t * pObj, int i ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin0(pObj)? Aig_NotCond(Ssw_ObjFraig(p, Aig_ObjFanin0(pObj), i), Aig_ObjFaninC0(pObj)) : NULL;  }
-static inline Aig_Obj_t * Ssw_ObjChild1Fra( Ssw_Man_t * p, Aig_Obj_t * pObj, int i ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin1(pObj)? Aig_NotCond(Ssw_ObjFraig(p, Aig_ObjFanin1(pObj), i), Aig_ObjFaninC1(pObj)) : NULL;  }
+static inline Aig_Obj_t * Ssw_ObjChild0Fra( Ssw_Man_t * p, Aig_Obj_t * pObj, int i ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin0(pObj)? Aig_NotCond(Ssw_ObjFrame(p, Aig_ObjFanin0(pObj), i), Aig_ObjFaninC0(pObj)) : NULL;  }
+static inline Aig_Obj_t * Ssw_ObjChild1Fra( Ssw_Man_t * p, Aig_Obj_t * pObj, int i ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin1(pObj)? Aig_NotCond(Ssw_ObjFrame(p, Aig_ObjFanin1(pObj), i), Aig_ObjFaninC1(pObj)) : NULL;  }
 
 ////////////////////////////////////////////////////////////////////////
 ///                    FUNCTION DECLARATIONS                         ///
@@ -161,8 +167,6 @@ extern int           Ssw_ClassesRefine( Ssw_Cla_t * p, int fRecursive );
 extern int           Ssw_ClassesRefineOneClass( Ssw_Cla_t * p, Aig_Obj_t * pRepr, int fRecursive );
 extern int           Ssw_ClassesRefineConst1Group( Ssw_Cla_t * p, Vec_Ptr_t * vRoots, int fRecursive );
 extern int           Ssw_ClassesRefineConst1( Ssw_Cla_t * p, int fRecursive );
-extern int           Ssw_NodeIsConstCex( void * p, Aig_Obj_t * pObj );
-extern int           Ssw_NodesAreEqualCex( void * p, Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 );
 /*=== sswCnf.c ===================================================*/
 extern void          Ssw_CnfNodeAddToSolver( Ssw_Man_t * p, Aig_Obj_t * pObj );
 /*=== sswCore.c ===================================================*/
@@ -178,19 +182,23 @@ extern void          Ssw_ManStartSolver( Ssw_Man_t * p );
 extern int           Ssw_NodesAreEquiv( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew );
 extern int           Ssw_NodesAreConstrained( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew );
 /*=== sswSim.c ===================================================*/
+extern unsigned      Ssw_SmlObjHashWord( Ssw_Sml_t * p, Aig_Obj_t * pObj );
+extern int           Ssw_SmlObjIsConstWord( Ssw_Sml_t * p, Aig_Obj_t * pObj );
+extern int           Ssw_SmlObjsAreEqualWord( Ssw_Sml_t * p, Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 );
+extern int           Ssw_SmlObjIsConstBit( void * p, Aig_Obj_t * pObj );
+extern int           Ssw_SmlObjsAreEqualBit( void * p, Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 );
 extern Ssw_Sml_t *   Ssw_SmlStart( Aig_Man_t * pAig, int nPref, int nFrames, int nWordsFrame );
+extern void          Ssw_SmlClean( Ssw_Sml_t * p );
 extern void          Ssw_SmlStop( Ssw_Sml_t * p );
-extern Ssw_Sml_t *   Ssw_SmlSimulateSeq( Aig_Man_t * pAig, int nPref, int nFrames, int nWords );
-extern unsigned      Ssw_SmlNodeHash( Ssw_Sml_t * p, Aig_Obj_t * pObj );
-extern int           Ssw_SmlNodeIsConst( Ssw_Sml_t * p, Aig_Obj_t * pObj );
-extern int           Ssw_SmlNodesAreEqual( Ssw_Sml_t * p, Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 );
+extern void          Ssw_SmlObjAssignConst( Ssw_Sml_t * p, Aig_Obj_t * pObj, int fConst1, int iFrame );
+extern void          Ssw_SmlObjSetWord( Ssw_Sml_t * p, Aig_Obj_t * pObj, unsigned Word, int iWord, int iFrame );
 extern void          Ssw_SmlAssignDist1Plus( Ssw_Sml_t * p, unsigned * pPat );
 extern void          Ssw_SmlSimulateOne( Ssw_Sml_t * p );
+extern void          Ssw_SmlSimulateOneFrame( Ssw_Sml_t * p );
+extern Ssw_Sml_t *   Ssw_SmlSimulateSeq( Aig_Man_t * pAig, int nPref, int nFrames, int nWords );
 /*=== sswSimSat.c ===================================================*/
-extern int           Ssw_ManOriginalPiValue( Ssw_Man_t * p, Aig_Obj_t * pObj, int f );
-extern void          Ssw_ManResimulateCex( Ssw_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pRepr, int f );
-extern void          Ssw_ManResimulateCexTotal( Ssw_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pRepr, int f );
-extern void          Ssw_ManResimulateCexTotalSim( Ssw_Man_t * p, Aig_Obj_t * pCand, Aig_Obj_t * pRepr, int f );
+extern void          Ssw_ManResimulateBit( Ssw_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pRepr );
+extern void          Ssw_ManResimulateWord( Ssw_Man_t * p, Aig_Obj_t * pCand, Aig_Obj_t * pRepr, int f );
 /*=== sswSweep.c ===================================================*/
 extern int           Ssw_ManSweepBmc( Ssw_Man_t * p );
 extern int           Ssw_ManSweep( Ssw_Man_t * p );
diff --git a/src/aig/ssw/sswLcorr.c b/src/aig/ssw/sswLcorr.c
index dcc4f245..cde9b0c9 100644
--- a/src/aig/ssw/sswLcorr.c
+++ b/src/aig/ssw/sswLcorr.c
@@ -19,7 +19,7 @@
 ***********************************************************************/
 
 #include "sswInt.h"
-#include "bar.h"
+//#include "bar.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
@@ -67,12 +67,13 @@ void Ssw_ManSatSolverRecycle( Ssw_Man_t * p )
     Ssw_ObjSetSatNum( p, Aig_ManConst1(p->pFrames), p->nSatVars++ );
 
     p->nRecycles++;
-    p->nCallsSince = 0;
+    p->nRecycleCalls = 0;
 }
 
+
 /**Function*************************************************************
 
-  Synopsis    [Copy pattern from the solver into the internal storage.]
+  Synopsis    [Tranfers simulation information from FRAIG to AIG.]
 
   Description []
                
@@ -81,19 +82,30 @@ void Ssw_ManSatSolverRecycle( Ssw_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-void Ssw_SmlSavePatternLatch( Ssw_Man_t * p )
+void Ssw_ManSweepTransfer( Ssw_Man_t * p )
 {
-    Aig_Obj_t * pObj;
+    Aig_Obj_t * pObj, * pObjFraig;
+    unsigned * pInfo;
     int i;
-    memset( p->pPatWords, 0, sizeof(unsigned) * p->nPatWords );
+    // transfer simulation information
     Aig_ManForEachPi( p->pAig, pObj, i )
-        if ( Ssw_ManOriginalPiValue( p, pObj, 0 ) )
-            Aig_InfoSetBit( p->pPatWords, i );
+    {
+        pObjFraig = Ssw_ObjFrame( p, pObj, 0 );
+        if ( pObjFraig == Aig_ManConst0(p->pFrames) )
+        {
+            Ssw_SmlObjAssignConst( p->pSml, pObj, 0, 0 );
+            continue;
+        }
+        assert( !Aig_IsComplement(pObjFraig) );
+        assert( Aig_ObjIsPi(pObjFraig) );
+        pInfo = Vec_PtrEntry( p->vSimInfo, Aig_ObjPioNum(pObjFraig) );
+        Ssw_SmlObjSetWord( p->pSml, pObj, pInfo[0], 0, 0 );
+    }
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Copy pattern from the solver into the internal storage.]
+  Synopsis    [Performs one round of simulation with counter-examples.]
 
   Description []
                
@@ -102,14 +114,50 @@ void Ssw_SmlSavePatternLatch( Ssw_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-void Ssw_SmlSavePatternLatchPhase( Ssw_Man_t * p, int f )
+int Ssw_ManSweepResimulate( Ssw_Man_t * p )
+{
+    int RetValue1, RetValue2, clk = clock();
+    // transfer PI simulation information from storage
+    Ssw_ManSweepTransfer( p );
+    // simulate internal nodes
+    Ssw_SmlSimulateOneFrame( p->pSml );
+    // check equivalence classes
+    RetValue1 = Ssw_ClassesRefineConst1( p->ppClasses, 1 );
+    RetValue2 = Ssw_ClassesRefine( p->ppClasses, 1 );
+    // prepare simulation info for the next round
+    Vec_PtrCleanSimInfo( p->vSimInfo, 0, 1 );
+    p->nPatterns = 0;
+    p->nSimRounds++;
+p->timeSimSat += clock() - clk;
+    return RetValue1 > 0 || RetValue2 > 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Saves one counter-example into internal storage.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ssw_SmlAddPattern( Ssw_Man_t * p, Aig_Obj_t * pRepr, Aig_Obj_t * pCand )
 {
     Aig_Obj_t * pObj;
-    int i;
-    memset( p->pPatWords, 0, sizeof(unsigned) * p->nPatWords );
-    Aig_ManForEachPi( p->pAig, pObj, i )
-        if ( Aig_ObjPhaseReal( Ssw_ObjFraig(p, pObj, f) ) )
-            Aig_InfoSetBit( p->pPatWords, i );
+    unsigned * pInfo;
+    int i, nVarNum, Value;
+    Vec_PtrForEachEntry( p->vUsedPis, pObj, i )
+    {
+        nVarNum = Ssw_ObjSatNum( p, pObj );
+        assert( nVarNum > 0 );
+        Value = sat_solver_var_value( p->pSat, nVarNum );
+        if ( Value == 0 )
+            continue;
+        pInfo = Vec_PtrEntry( p->vSimInfo, Aig_ObjPioNum(pObj) );
+        Aig_InfoSetBit( pInfo, p->nPatterns );
+    }
 }
 
 /**Function*************************************************************
@@ -127,13 +175,13 @@ void Ssw_ManBuildCone_rec( Ssw_Man_t * p, Aig_Obj_t * pObj )
 {
     Aig_Obj_t * pObjNew;
     assert( !Aig_IsComplement(pObj) );
-    if ( Ssw_ObjFraig( p, pObj, 0 ) )
+    if ( Ssw_ObjFrame( p, pObj, 0 ) )
         return;
     assert( Aig_ObjIsNode(pObj) );
     Ssw_ManBuildCone_rec( p, Aig_ObjFanin0(pObj) );
     Ssw_ManBuildCone_rec( p, Aig_ObjFanin1(pObj) );
     pObjNew = Aig_And( p->pFrames, Ssw_ObjChild0Fra(p, pObj, 0), Ssw_ObjChild1Fra(p, pObj, 0) );
-    Ssw_ObjSetFraig( p, pObj, 0, pObjNew );
+    Ssw_ObjSetFrame( p, pObj, 0, pObjNew );
 }
 
 /**Function*************************************************************
@@ -149,10 +197,18 @@ void Ssw_ManBuildCone_rec( Ssw_Man_t * p, Aig_Obj_t * pObj )
 ***********************************************************************/
 void Ssw_ManSweepLatchOne( Ssw_Man_t * p, Aig_Obj_t * pObjRepr, Aig_Obj_t * pObj )
 {
-    Aig_Obj_t * pObjFraig, * pObjFraig2, * pObjReprFraig, * pObjLi;
-    int RetValue;
+    Aig_Obj_t * pObjFraig, * pObjReprFraig, * pObjLi;
+    int RetValue, clk;
     assert( Aig_ObjIsPi(pObj) );
     assert( Aig_ObjIsPi(pObjRepr) || Aig_ObjIsConst1(pObjRepr) );
+    // check if it makes sense to skip some calls
+    if ( p->nCallsCount > 100 && p->nCallsUnsat < p->nCallsSat )
+    {
+        if ( ++p->nCallsDelta < 0 )
+            return;
+    }
+    p->nCallsDelta = 0;
+clk = clock();
     // get the fraiged node
     pObjLi = Saig_ObjLoToLi( p->pAig, pObj ); 
     Ssw_ManBuildCone_rec( p, Aig_ObjFanin0(pObjLi) );
@@ -165,43 +221,44 @@ void Ssw_ManSweepLatchOne( Ssw_Man_t * p, Aig_Obj_t * pObjRepr, Aig_Obj_t * pObj
         pObjReprFraig = Ssw_ObjChild0Fra( p, pObjLi, 0 );
     }
     else 
-        pObjReprFraig = Ssw_ObjFraig( p, pObjRepr, 0 );
+        pObjReprFraig = Ssw_ObjFrame( p, pObjRepr, 0 );
+p->timeReduce += clock() - clk;
     // if the fraiged nodes are the same, return
     if ( Aig_Regular(pObjFraig) == Aig_Regular(pObjReprFraig) )
         return;
-    p->nCallsSince++;
+    p->nRecycleCalls++;
+    p->nCallsCount++;
+
     // check equivalence of the two nodes
     if ( (pObj->fPhase == pObjRepr->fPhase) != (Aig_ObjPhaseReal(pObjFraig) == Aig_ObjPhaseReal(pObjReprFraig)) )
     {
+        p->nPatterns++;
         p->nStrangers++;
-        Ssw_SmlSavePatternLatchPhase( p, 0 );
+        p->fRefined = 1;
     }
     else
     { 
         RetValue = Ssw_NodesAreEquiv( p, Aig_Regular(pObjReprFraig), Aig_Regular(pObjFraig) );
-        if ( RetValue == 1 )  // proved equivalent
+        if ( RetValue == 1 )  // proved equivalence
         {
-            pObjFraig2 = Aig_NotCond( pObjReprFraig, pObj->fPhase ^ pObjRepr->fPhase );
-            Ssw_ObjSetFraig( p, pObj, 0, pObjFraig2 );
+            p->nCallsUnsat++;
             return;
         }
-        else if ( RetValue == -1 ) // timed out
+        if ( RetValue == -1 ) // timed out
         {
             Ssw_ClassesRemoveNode( p->ppClasses, pObj );
+            p->nCallsUnsat++;
             p->fRefined = 1;
             return;
         }
-        else // disproved the equivalence
+        else // disproved equivalence
         {       
-            Ssw_SmlSavePatternLatch( p );
+            Ssw_SmlAddPattern( p, pObjRepr, pObj );
+            p->nPatterns++;
+            p->nCallsSat++;
+            p->fRefined = 1;
         }
     }
-    if ( p->pPars->nConstrs == 0 )
-        Ssw_ManResimulateCexTotalSim( p, pObj, pObjRepr, 0 );
-    else
-        Ssw_ManResimulateCexTotal( p, pObj, pObjRepr, 0 );
-    assert( Aig_ObjRepr( p->pAig, pObj ) != pObjRepr );
-    p->fRefined = 1;
 }
 
 /**Function*************************************************************
@@ -217,7 +274,7 @@ void Ssw_ManSweepLatchOne( Ssw_Man_t * p, Aig_Obj_t * pObjRepr, Aig_Obj_t * pObj
 ***********************************************************************/
 int Ssw_ManSweepLatch( Ssw_Man_t * p )
 {
-    Bar_Progress_t * pProgress = NULL;
+//    Bar_Progress_t * pProgress = NULL;
     Vec_Ptr_t * vClass;
     Aig_Obj_t * pObj, * pRepr, * pTemp;
     int i, k;
@@ -225,30 +282,40 @@ int Ssw_ManSweepLatch( Ssw_Man_t * p )
     // start the timeframe
     p->pFrames = Aig_ManStart( Aig_ManObjNumMax(p->pAig) );
     // map constants and PIs
-    Ssw_ObjSetFraig( p, Aig_ManConst1(p->pAig), 0, Aig_ManConst1(p->pFrames) );
+    Ssw_ObjSetFrame( p, Aig_ManConst1(p->pAig), 0, Aig_ManConst1(p->pFrames) );
     Saig_ManForEachPi( p->pAig, pObj, i )
-        Ssw_ObjSetFraig( p, pObj, 0, Aig_ObjCreatePi(p->pFrames) );
+        Ssw_ObjSetFrame( p, pObj, 0, Aig_ObjCreatePi(p->pFrames) );
 
     // implement equivalence classes
     Saig_ManForEachLo( p->pAig, pObj, i )
     {
         pRepr = Aig_ObjRepr( p->pAig, pObj );
         if ( pRepr == NULL )
+        {
             pTemp = Aig_ObjCreatePi(p->pFrames);
+            pTemp->pData = pObj;
+        }
         else
-            pTemp = Aig_NotCond( Ssw_ObjFraig(p, pRepr, 0), pRepr->fPhase ^ pObj->fPhase );
-        Ssw_ObjSetFraig( p, pObj, 0, pTemp );
+            pTemp = Aig_NotCond( Ssw_ObjFrame(p, pRepr, 0), pRepr->fPhase ^ pObj->fPhase );
+        Ssw_ObjSetFrame( p, pObj, 0, pTemp );
     }
+    Aig_ManSetPioNumbers( p->pFrames );
+
+    // prepare simulation info
+    assert( p->vSimInfo == NULL );
+    p->vSimInfo = Vec_PtrAllocSimInfo( Aig_ManPiNum(p->pFrames), 1 );
+    Vec_PtrCleanSimInfo( p->vSimInfo, 0, 1 );
 
     // go through the registers
-    if ( p->pPars->fVerbose )
-        pProgress = Bar_ProgressStart( stdout, Aig_ManRegNum(p->pAig) );
+//    if ( p->pPars->fVerbose )
+//        pProgress = Bar_ProgressStart( stdout, Aig_ManRegNum(p->pAig) );
     vClass = Vec_PtrAlloc( 100 );
     p->fRefined = 0;
+    p->nCallsCount = p->nCallsSat = p->nCallsUnsat = 0;
     Saig_ManForEachLo( p->pAig, pObj, i )
     {
-        if ( p->pPars->fVerbose )
-            Bar_ProgressUpdate( pProgress, i, NULL );
+//        if ( p->pPars->fVerbose )
+//            Bar_ProgressUpdate( pProgress, i, NULL );
         // consider the case of constant candidate
         if ( Ssw_ObjIsConst1Cand( p->pAig, pObj ) )
             Ssw_ManSweepLatchOne( p, Aig_ManConst1(p->pAig), pObj );
@@ -261,21 +328,32 @@ int Ssw_ManSweepLatch( Ssw_Man_t * p )
             // try to prove equivalences in this class
             Vec_PtrForEachEntry( vClass, pTemp, k )
                 if ( Aig_ObjRepr(p->pAig, pTemp) == pObj )
+                {
                     Ssw_ManSweepLatchOne( p, pObj, pTemp );
+                    if ( p->nPatterns == 32 )
+                        break;
+                }
         }
+        // resimulate
+        if ( p->nPatterns == 32 )
+            Ssw_ManSweepResimulate( p );
         // attempt recycling the SAT solver
         if ( p->pPars->nSatVarMax && 
              p->nSatVars > p->pPars->nSatVarMax &&
-             p->nCallsSince > p->pPars->nCallsRecycle )
+             p->nRecycleCalls > p->pPars->nRecycleCalls )
              Ssw_ManSatSolverRecycle( p );
     }
+    // resimulate
+    if ( p->nPatterns > 0 )
+        Ssw_ManSweepResimulate( p );
+    // cleanup
     Vec_PtrFree( vClass );
     p->nSatFailsTotal += p->nSatFailsReal;
-    if ( p->pPars->fVerbose )
-        Bar_ProgressStop( pProgress );
+//    if ( p->pPars->fVerbose )
+//        Bar_ProgressStop( pProgress );
 
     // cleanup
-    Ssw_ClassesCheck( p->ppClasses );
+//    Ssw_ClassesCheck( p->ppClasses );
     return p->fRefined;
 }
 
diff --git a/src/aig/ssw/sswMan.c b/src/aig/ssw/sswMan.c
index 33c716ce..8d2c8c24 100644
--- a/src/aig/ssw/sswMan.c
+++ b/src/aig/ssw/sswMan.c
@@ -52,12 +52,10 @@ Ssw_Man_t * Ssw_ManCreate( Aig_Man_t * pAig, Ssw_Pars_t * pPars )
     p->pPars         = pPars;
     p->pAig          = pAig;
     p->nFrames       = pPars->nFramesK + 1;
-    p->pNodeToFraig  = CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p->pAig) * p->nFrames );
+    p->pNodeToFrames = CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p->pAig) * p->nFrames );
     // SAT solving
     p->pSatVars      = CALLOC( int, Aig_ManObjNumMax(p->pAig) * (p->nFrames+1) );
     p->vFanins       = Vec_PtrAlloc( 100 );
-    p->vSimRoots     = Vec_PtrAlloc( 1000 );
-    p->vSimClasses   = Vec_PtrAlloc( 1000 );
     // SAT solving (latch corr only)
     p->vUsedNodes    = Vec_PtrAlloc( 1000 );
     p->vUsedPis      = Vec_PtrAlloc( 1000 );
@@ -102,13 +100,15 @@ void Ssw_ManPrintStats( Ssw_Man_t * p )
 {
     double nMemory = 1.0*Aig_ManObjNumMax(p->pAig)*p->nFrames*(2*sizeof(int)+2*sizeof(void*))/(1<<20);
 
-    printf( "Parameters: F = %d. AddF = %d. C-lim = %d. Constr = %d. SkipCheck = %d. MaxLev = %d. Mem = %0.2f Mb.\n", 
-        p->pPars->nFramesK, p->pPars->nFramesAddSim, p->pPars->nBTLimit, p->pPars->nConstrs, p->pPars->fSkipCheck, p->pPars->nMaxLevs, nMemory );
+    printf( "Parameters: F = %d. AddF = %d. C-lim = %d. Constr = %d. MaxLev = %d. Mem = %0.2f Mb.\n", 
+        p->pPars->nFramesK, p->pPars->nFramesAddSim, p->pPars->nBTLimit, p->pPars->nConstrs, p->pPars->nMaxLevs, nMemory );
     printf( "AIG       : PI = %d. PO = %d. Latch = %d. Node = %d.  Ave SAT vars = %d.\n", 
         Saig_ManPiNum(p->pAig), Saig_ManPoNum(p->pAig), Saig_ManRegNum(p->pAig), Aig_ManNodeNum(p->pAig), 
         p->nSatVarsTotal/p->pPars->nIters );
     printf( "SAT calls : Proof = %d. Cex = %d. Fail = %d. Equivs = %d. Str = %d.\n", 
         p->nSatProof, p->nSatCallsSat, p->nSatFailsTotal, Ssw_ManCountEquivs(p), p->nStrangers );
+    printf( "SAT solver: Vars = %d. Max cone = %d. Recycles = %d. Rounds = %d.\n", 
+        p->nSatVars, p->nConeMax, p->nRecycles, p->nSimRounds );
     printf( "NBeg = %d. NEnd = %d. (Gain = %6.2f %%).  RBeg = %d. REnd = %d. (Gain = %6.2f %%).\n", 
         p->nNodesBeg, p->nNodesEnd, 100.0*(p->nNodesBeg-p->nNodesEnd)/(p->nNodesBeg?p->nNodesBeg:1), 
         p->nRegsBeg, p->nRegsEnd, 100.0*(p->nRegsBeg-p->nRegsEnd)/(p->nRegsBeg?p->nRegsBeg:1) );
@@ -139,12 +139,11 @@ void Ssw_ManPrintStats( Ssw_Man_t * p )
 ***********************************************************************/
 void Ssw_ManCleanup( Ssw_Man_t * p )
 {
-    Aig_ManCleanMarkB( p->pAig );
     if ( p->pFrames )
     {
         Aig_ManStop( p->pFrames );
         p->pFrames = NULL;
-        memset( p->pNodeToFraig, 0, sizeof(Aig_Obj_t *) * Aig_ManObjNumMax(p->pAig) * p->nFrames );
+        memset( p->pNodeToFrames, 0, sizeof(Aig_Obj_t *) * Aig_ManObjNumMax(p->pAig) * p->nFrames );
     }
     if ( p->pSat )
     {
@@ -154,6 +153,11 @@ void Ssw_ManCleanup( Ssw_Man_t * p )
         p->pSat = NULL;
         memset( p->pSatVars, 0, sizeof(int) * Aig_ManObjNumMax(p->pAig) * (p->nFrames+1) );
     }
+    if ( p->vSimInfo )  
+    {
+        Vec_PtrFree( p->vSimInfo );
+        p->vSimInfo = NULL;
+    }
     p->nConstrTotal = 0;
     p->nConstrReduced = 0;
 }
@@ -172,6 +176,7 @@ void Ssw_ManCleanup( Ssw_Man_t * p )
 void Ssw_ManStop( Ssw_Man_t * p )
 {
     Aig_ManCleanMarkA( p->pAig );
+    Aig_ManCleanMarkB( p->pAig );
     if ( p->pPars->fVerbose )
         Ssw_ManPrintStats( p );
     if ( p->ppClasses )
@@ -179,11 +184,9 @@ void Ssw_ManStop( Ssw_Man_t * p )
     if ( p->pSml )      
         Ssw_SmlStop( p->pSml );
     Vec_PtrFree( p->vFanins );
-    Vec_PtrFree( p->vSimRoots );
-    Vec_PtrFree( p->vSimClasses );
     Vec_PtrFree( p->vUsedNodes );
     Vec_PtrFree( p->vUsedPis );
-    FREE( p->pNodeToFraig );
+    FREE( p->pNodeToFrames );
     FREE( p->pSatVars );
     FREE( p->pPatWords );
     free( p );
diff --git a/src/aig/ssw/sswPairs.c b/src/aig/ssw/sswPairs.c
index a11bdf98..c77ad30d 100644
--- a/src/aig/ssw/sswPairs.c
+++ b/src/aig/ssw/sswPairs.c
@@ -289,7 +289,7 @@ Aig_Man_t * Ssw_SignalCorrespondenceWithPairs( Aig_Man_t * pAig1, Aig_Man_t * pA
     // create equivalence classes using these IDs
     p->ppClasses = Ssw_ClassesPreparePairs( pMiter, pvClasses );
     p->pSml = Ssw_SmlStart( pMiter, 0, p->nFrames + p->pPars->nFramesAddSim, 1 );
-    Ssw_ClassesSetData( p->ppClasses, p->pSml, Ssw_SmlNodeHash, Ssw_SmlNodeIsConst, Ssw_SmlNodesAreEqual );
+    Ssw_ClassesSetData( p->ppClasses, p->pSml, Ssw_SmlObjHashWord, Ssw_SmlObjIsConstWord, Ssw_SmlObjsAreEqualWord );
     // perform refinement of classes
     pAigNew = Ssw_SignalCorrespondenceRefine( p );
     // cleanup
diff --git a/src/aig/ssw/sswSim.c b/src/aig/ssw/sswSim.c
index 769e923c..ba8ad247 100644
--- a/src/aig/ssw/sswSim.c
+++ b/src/aig/ssw/sswSim.c
@@ -57,7 +57,7 @@ static inline unsigned   Ssw_ObjRandomSim()                   { return Aig_ManRa
   SeeAlso     []
 
 ***********************************************************************/
-unsigned Ssw_SmlNodeHash( Ssw_Sml_t * p, Aig_Obj_t * pObj )
+unsigned Ssw_SmlObjHashWord( Ssw_Sml_t * p, Aig_Obj_t * pObj )
 {
     static int s_SPrimes[128] = { 
         1009, 1049, 1093, 1151, 1201, 1249, 1297, 1361, 1427, 1459, 
@@ -96,7 +96,7 @@ unsigned Ssw_SmlNodeHash( Ssw_Sml_t * p, Aig_Obj_t * pObj )
   SeeAlso     []
 
 ***********************************************************************/
-int Ssw_SmlNodeIsConst( Ssw_Sml_t * p, Aig_Obj_t * pObj )
+int Ssw_SmlObjIsConstWord( Ssw_Sml_t * p, Aig_Obj_t * pObj )
 {
     unsigned * pSims;
     int i;
@@ -118,7 +118,7 @@ int Ssw_SmlNodeIsConst( Ssw_Sml_t * p, Aig_Obj_t * pObj )
   SeeAlso     []
 
 ***********************************************************************/
-int Ssw_SmlNodesAreEqual( Ssw_Sml_t * p, Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 )
+int Ssw_SmlObjsAreEqualWord( Ssw_Sml_t * p, Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 )
 {
     unsigned * pSims0, * pSims1;
     int i;
@@ -132,6 +132,39 @@ int Ssw_SmlNodesAreEqual( Ssw_Sml_t * p, Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 )
 
 /**Function*************************************************************
 
+  Synopsis    [Returns 1 if the node appears to be constant 1 candidate.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ssw_SmlObjIsConstBit( void * p, Aig_Obj_t * pObj )
+{
+    return pObj->fPhase == pObj->fMarkB;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if the nodes appear equal.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ssw_SmlObjsAreEqualBit( void * p, Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 )
+{
+    return (pObj0->fPhase == pObj1->fPhase) == (pObj0->fMarkB == pObj1->fMarkB);
+}
+
+
+/**Function*************************************************************
+
   Synopsis    [Counts the number of 1s in the XOR of simulation data.]
 
   Description []
@@ -340,7 +373,7 @@ int * Ssw_SmlCheckOutput( Ssw_Sml_t * p )
     assert( Aig_ObjFanin0(pObj)->fPhase == (unsigned)Aig_ObjFaninC0(pObj) ); 
     Aig_ManForEachPo( p->pAig, pObj, i )
     {
-        if ( !Ssw_SmlNodeIsConst( p, Aig_ObjFanin0(pObj) ) )
+        if ( !Ssw_SmlObjIsConstWord( p, Aig_ObjFanin0(pObj) ) )
         {
             // create the counter-example from this pattern
             return Ssw_SmlCheckOutputSavePattern( p, pObj );
@@ -404,7 +437,7 @@ void Ssw_SmlAssignRandomFrame( Ssw_Sml_t * p, Aig_Obj_t * pObj, int iFrame )
   SeeAlso     []
 
 ***********************************************************************/
-void Ssw_SmlAssignConst( Ssw_Sml_t * p, Aig_Obj_t * pObj, int fConst1, int iFrame )
+void Ssw_SmlObjAssignConst( Ssw_Sml_t * p, Aig_Obj_t * pObj, int fConst1, int iFrame )
 {
     unsigned * pSims;
     int i;
@@ -416,6 +449,25 @@ void Ssw_SmlAssignConst( Ssw_Sml_t * p, Aig_Obj_t * pObj, int fConst1, int iFram
 
 /**Function*************************************************************
 
+  Synopsis    [Assigns constant patterns to the PI node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ssw_SmlObjSetWord( Ssw_Sml_t * p, Aig_Obj_t * pObj, unsigned Word, int iWord, int iFrame )
+{
+    unsigned * pSims;
+    assert( Aig_ObjIsPi(pObj) );
+    pSims = Ssw_ObjSim( p, pObj->Id ) + p->nWordsFrame * iFrame;
+    pSims[iWord] = Word;
+} 
+
+/**Function*************************************************************
+
   Synopsis    [Assings random simulation info for the PIs.]
 
   Description []
@@ -438,7 +490,7 @@ void Ssw_SmlInitialize( Ssw_Sml_t * p, int fInit )
             Ssw_SmlAssignRandom( p, pObj );
         // assign the initial state for the latches
         Saig_ManForEachLo( p->pAig, pObj, i )
-            Ssw_SmlAssignConst( p, pObj, 0, 0 );
+            Ssw_SmlObjAssignConst( p, pObj, 0, 0 );
     }
     else
     {
@@ -467,7 +519,7 @@ void Ssw_SmlAssignDist1( Ssw_Sml_t * p, unsigned * pPat )
     {
         // copy the PI info 
         Aig_ManForEachPi( p->pAig, pObj, i )
-            Ssw_SmlAssignConst( p, pObj, Aig_InfoHasBit(pPat, i), 0 );
+            Ssw_SmlObjAssignConst( p, pObj, Aig_InfoHasBit(pPat, i), 0 );
         // flip one bit
         Limit = AIG_MIN( Aig_ManPiNum(p->pAig), p->nWordsTotal * 32 - 1 );
         for ( i = 0; i < Limit; i++ )
@@ -481,11 +533,11 @@ void Ssw_SmlAssignDist1( Ssw_Sml_t * p, unsigned * pPat )
         nTruePis = Aig_ManPiNum(p->pAig) - Aig_ManRegNum(p->pAig);
         for ( f = 0; f < p->nFrames; f++ )
             Saig_ManForEachPi( p->pAig, pObj, i )
-                Ssw_SmlAssignConst( p, pObj, Aig_InfoHasBit(pPat, nTruePis * f + i), f );
+                Ssw_SmlObjAssignConst( p, pObj, Aig_InfoHasBit(pPat, nTruePis * f + i), f );
         // copy the latch info 
         k = 0;
         Saig_ManForEachLo( p->pAig, pObj, i )
-            Ssw_SmlAssignConst( p, pObj, Aig_InfoHasBit(pPat, nTruePis * p->nFrames + k++), 0 );
+            Ssw_SmlObjAssignConst( p, pObj, Aig_InfoHasBit(pPat, nTruePis * p->nFrames + k++), 0 );
 //        assert( p->pFrames == NULL || nTruePis * p->nFrames + k == Aig_ManPiNum(p->pFrames) );
 
         // flip one bit of the last frame
@@ -517,7 +569,7 @@ void Ssw_SmlAssignDist1Plus( Ssw_Sml_t * p, unsigned * pPat )
 
     // copy the pattern into the primary inputs
     Aig_ManForEachPi( p->pAig, pObj, i )
-        Ssw_SmlAssignConst( p, pObj, Aig_InfoHasBit(pPat, i), 0 );
+        Ssw_SmlObjAssignConst( p, pObj, Aig_InfoHasBit(pPat, i), 0 );
 
     // set distance one PIs for the first frame
     Limit = AIG_MIN( Saig_ManPiNum(p->pAig), p->nWordsFrame * 32 - 1 );
@@ -530,7 +582,6 @@ void Ssw_SmlAssignDist1Plus( Ssw_Sml_t * p, unsigned * pPat )
             Ssw_SmlAssignRandomFrame( p, pObj, f );
 }
 
-
 /**Function*************************************************************
 
   Synopsis    [Simulates one node.]
@@ -746,46 +797,39 @@ p->timeSim += clock() - clk;
 p->nSimRounds++;
 }
 
-
-#if 0
-
 /**Function*************************************************************
 
-  Synopsis    [Resimulates fraiging manager after finding a counter-example.]
+  Synopsis    [Simulates AIG manager.]
 
-  Description []
+  Description [Assumes that the PI simulation info is attached.]
                
   SideEffects []
 
   SeeAlso     []
 
 ***********************************************************************/
-void Ssw_SmlResimulate( Ssw_Man_t * p )
+void Ssw_SmlSimulateOneFrame( Ssw_Sml_t * p )
 {
-    int nChanges, clk;
-    Ssw_SmlAssignDist1( p, p->pPatWords );
-    Ssw_SmlSimulateOne( p );
-//    if ( p->pPars->fPatScores )
-//        Ssw_CleanPatScores( p );
-    if ( p->pPars->fProve && Ssw_SmlCheckOutput(p) )
-        return;
+    Aig_Obj_t * pObj, * pObjLi, * pObjLo;
+    int i, clk;
 clk = clock();
-    nChanges = Ssw_ClassesRefine( p->pCla, 1 );
-    nChanges += Ssw_ClassesRefine1( p->pCla, 1, NULL );
-    if ( p->pCla->vImps )
-        nChanges += Ssw_ImpRefineUsingCex( p, p->pCla->vImps );
-    if ( p->vOneHots )
-        nChanges += Ssw_OneHotRefineUsingCex( p, p->vOneHots );
-p->timeRef += clock() - clk;
-    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 );
+    // simulate the nodes
+    Aig_ManForEachNode( p->pAig, pObj, i )
+        Ssw_SmlNodeSimulate( p, pObj, 0 );
+    // copy simulation info into outputs
+    Saig_ManForEachLi( p->pAig, pObj, i )
+        Ssw_SmlNodeCopyFanin( p, pObj, 0 );
+    // copy simulation info into the inputs
+    Saig_ManForEachLiLo( p->pAig, pObjLi, pObjLo, i )
+        Ssw_SmlNodeTransferNext( p, pObjLi, pObjLo, 0 );
+p->timeSim += clock() - clk;
+p->nSimRounds++;
 }
 
+
 /**Function*************************************************************
 
-  Synopsis    [Performs simulation of the manager.]
+  Synopsis    [Allocates simulation manager.]
 
   Description []
                
@@ -794,69 +838,19 @@ p->timeRef += clock() - clk;
   SeeAlso     []
 
 ***********************************************************************/
-void Ssw_SmlSimulate( Ssw_Man_t * p, int fInit )
+Ssw_Sml_t * Ssw_SmlStart( Aig_Man_t * pAig, int nPref, int nFrames, int nWordsFrame )
 {
-    int fVerbose = 0;
-    int nChanges, nClasses, clk;
-    assert( !fInit || Aig_ManRegNum(p->pAig) );
-    // start the classes
-    Ssw_SmlInitialize( p, fInit );
-    Ssw_SmlSimulateOne( p );
-    if ( p->pPars->fProve && Ssw_SmlCheckOutput(p) )
-        return;
-    Ssw_ClassesPrepare( p->pCla, p->pPars->fLatchCorr, 0 );
-//    Ssw_ClassesPrint( p->pCla, 0 );
-if ( fVerbose )
-printf( "Starting classes = %5d.   Lits = %6d.\n", Vec_PtrSize(p->pCla->vClasses), Ssw_ClassesCountLits(p->pCla) );
-
-//return;
-
-    // refine classes by walking 0/1 patterns
-    Ssw_SmlSavePattern0( p, fInit );
-    Ssw_SmlAssignDist1( p, p->pPatWords );
-    Ssw_SmlSimulateOne( p );
-    if ( p->pPars->fProve && Ssw_SmlCheckOutput(p) )
-        return;
-clk = clock();
-    nChanges = Ssw_ClassesRefine( p->pCla, 1 );
-    nChanges += Ssw_ClassesRefine1( p->pCla, 1, NULL );
-p->timeRef += clock() - clk;
-if ( fVerbose )
-printf( "Refined classes  = %5d.   Changes = %4d.   Lits = %6d.\n", Vec_PtrSize(p->pCla->vClasses), nChanges, Ssw_ClassesCountLits(p->pCla) );
-    Ssw_SmlSavePattern1( p, fInit );
-    Ssw_SmlAssignDist1( p, p->pPatWords );
-    Ssw_SmlSimulateOne( p );
-    if ( p->pPars->fProve && Ssw_SmlCheckOutput(p) )
-        return;
-clk = clock();
-    nChanges = Ssw_ClassesRefine( p->pCla, 1 );
-    nChanges += Ssw_ClassesRefine1( p->pCla, 1, NULL );
-p->timeRef += clock() - clk;
-
-if ( fVerbose )
-printf( "Refined classes  = %5d.   Changes = %4d.   Lits = %6d.\n", Vec_PtrSize(p->pCla->vClasses), nChanges, Ssw_ClassesCountLits(p->pCla) );
-    // refine classes by random simulation
-    do {
-        Ssw_SmlInitialize( p, fInit );
-        Ssw_SmlSimulateOne( p );
-        nClasses = Vec_PtrSize(p->pCla->vClasses);
-        if ( p->pPars->fProve && Ssw_SmlCheckOutput(p) )
-            return;
-clk = clock();
-        nChanges = Ssw_ClassesRefine( p->pCla, 1 );
-        nChanges += Ssw_ClassesRefine1( p->pCla, 1, NULL );
-p->timeRef += clock() - clk;
-if ( fVerbose )
-printf( "Refined classes  = %5d.   Changes = %4d.   Lits = %6d.\n", Vec_PtrSize(p->pCla->vClasses), nChanges, Ssw_ClassesCountLits(p->pCla) );
-    } 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), Ssw_ClassesCountLits(p->pCla) );
-//    Ssw_ClassesPrint( p->pCla, 0 );
+    Ssw_Sml_t * p;
+    p = (Ssw_Sml_t *)malloc( sizeof(Ssw_Sml_t) + sizeof(unsigned) * Aig_ManObjNumMax(pAig) * (nPref + nFrames) * nWordsFrame );
+    memset( p, 0, sizeof(Ssw_Sml_t) + sizeof(unsigned) * (nPref + nFrames) * nWordsFrame );
+    p->pAig        = pAig;
+    p->nPref       = nPref;
+    p->nFrames     = nPref + nFrames;
+    p->nWordsFrame = nWordsFrame;
+    p->nWordsTotal = (nPref + nFrames) * nWordsFrame;
+    p->nWordsPref  = nPref * nWordsFrame;
+    return p;
 }
- 
-#endif
 
 /**Function*************************************************************
 
@@ -869,18 +863,9 @@ printf( "Refined classes  = %5d.   Changes = %4d.   Lits = %6d.\n", Vec_PtrSize(
   SeeAlso     []
 
 ***********************************************************************/
-Ssw_Sml_t * Ssw_SmlStart( Aig_Man_t * pAig, int nPref, int nFrames, int nWordsFrame )
+void Ssw_SmlClean( Ssw_Sml_t * p )
 {
-    Ssw_Sml_t * p;
-    p = (Ssw_Sml_t *)malloc( sizeof(Ssw_Sml_t) + sizeof(unsigned) * Aig_ManObjNumMax(pAig) * (nPref + nFrames) * nWordsFrame );
-    memset( p, 0, sizeof(Ssw_Sml_t) + sizeof(unsigned) * (nPref + nFrames) * nWordsFrame );
-    p->pAig        = pAig;
-    p->nPref       = nPref;
-    p->nFrames     = nPref + nFrames;
-    p->nWordsFrame = nWordsFrame;
-    p->nWordsTotal = (nPref + nFrames) * nWordsFrame;
-    p->nWordsPref  = nPref * nWordsFrame;
-    return p;
+    memset( p->pData, 0, sizeof(unsigned) * Aig_ManObjNumMax(p->pAig) * p->nWordsTotal );
 }
 
 /**Function*************************************************************
@@ -1005,11 +990,11 @@ int Ssw_SmlRunCounterExample( Aig_Man_t * pAig, Ssw_Cex_t * p )
     // assign simulation info for the registers
     iBit = 0;
     Saig_ManForEachLo( pAig, pObj, i )
-        Ssw_SmlAssignConst( pSml, pObj, Aig_InfoHasBit(p->pData, iBit++), 0 );
+        Ssw_SmlObjAssignConst( pSml, pObj, Aig_InfoHasBit(p->pData, iBit++), 0 );
     // assign simulation info for the primary inputs
     for ( i = 0; i <= p->iFrame; i++ )
         Saig_ManForEachPi( pAig, pObj, k )
-            Ssw_SmlAssignConst( pSml, pObj, Aig_InfoHasBit(p->pData, iBit++), i );
+            Ssw_SmlObjAssignConst( pSml, pObj, Aig_InfoHasBit(p->pData, iBit++), i );
     assert( iBit == p->nBits );
     // run random simulation
     Ssw_SmlSimulateOne( pSml );
@@ -1042,11 +1027,11 @@ int Ssw_SmlFindOutputCounterExample( Aig_Man_t * pAig, Ssw_Cex_t * p )
     // assign simulation info for the registers
     iBit = 0;
     Saig_ManForEachLo( pAig, pObj, i )
-        Ssw_SmlAssignConst( pSml, pObj, Aig_InfoHasBit(p->pData, iBit++), 0 );
+        Ssw_SmlObjAssignConst( pSml, pObj, Aig_InfoHasBit(p->pData, iBit++), 0 );
     // assign simulation info for the primary inputs
     for ( i = 0; i <= p->iFrame; i++ )
         Saig_ManForEachPi( pAig, pObj, k )
-            Ssw_SmlAssignConst( pSml, pObj, Aig_InfoHasBit(p->pData, iBit++), i );
+            Ssw_SmlObjAssignConst( pSml, pObj, Aig_InfoHasBit(p->pData, iBit++), i );
     assert( iBit == p->nBits );
     // run random simulation
     Ssw_SmlSimulateOne( pSml );
@@ -1271,13 +1256,13 @@ int Ssw_SmlWriteCounterExample( FILE * pFile, Aig_Man_t * pAig, Ssw_Cex_t * p )
     // assign simulation info for the registers
     iBit = 0;
     Saig_ManForEachLo( pAig, pObj, i )
-//        Ssw_SmlAssignConst( pSml, pObj, Aig_InfoHasBit(p->pData, iBit++), 0 );
-        Ssw_SmlAssignConst( pSml, pObj, 0, 0 );
+//        Ssw_SmlObjAssignConst( pSml, pObj, Aig_InfoHasBit(p->pData, iBit++), 0 );
+        Ssw_SmlObjAssignConst( pSml, pObj, 0, 0 );
     // assign simulation info for the primary inputs
     iBit = p->nRegs;
     for ( i = 0; i <= p->iFrame; i++ )
         Saig_ManForEachPi( pAig, pObj, k )
-            Ssw_SmlAssignConst( pSml, pObj, Aig_InfoHasBit(p->pData, iBit++), i );
+            Ssw_SmlObjAssignConst( pSml, pObj, Aig_InfoHasBit(p->pData, iBit++), i );
     assert( iBit == p->nBits );
     // run random simulation
     Ssw_SmlSimulateOne( pSml );
diff --git a/src/aig/ssw/sswSimSat.c b/src/aig/ssw/sswSimSat.c
index 715750ca..c85b8bcf 100644
--- a/src/aig/ssw/sswSimSat.c
+++ b/src/aig/ssw/sswSimSat.c
@@ -30,157 +30,6 @@
 
 /**Function*************************************************************
 
-  Synopsis    [Collects internal nodes in the reverse DFS order.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Ssw_ManCollectTfoCands_rec( Ssw_Man_t * p, Aig_Obj_t * pObj )
-{
-    Aig_Obj_t * pFanout, * pRepr;
-    int iFanout = -1, i;
-    assert( !Aig_IsComplement(pObj) );
-    if ( Aig_ObjIsTravIdCurrent(p->pAig, pObj) )
-        return;
-    Aig_ObjSetTravIdCurrent(p->pAig, pObj);
-    // traverse the fanouts
-    Aig_ObjForEachFanout( p->pAig, pObj, pFanout, iFanout, i )
-        Ssw_ManCollectTfoCands_rec( p, pFanout );
-    // check if the given node has a representative
-    pRepr = Aig_ObjRepr( p->pAig, pObj );
-    if ( pRepr == NULL )
-        return;
-    // pRepr is the constant 1 node
-    if ( pRepr == Aig_ManConst1(p->pAig) )
-    {
-        Vec_PtrPush( p->vSimRoots, pObj );
-        return;
-    }
-    // pRepr is the representative of the equivalence class
-    if ( Aig_ObjIsTravIdCurrent(p->pAig, pRepr) )
-        return;
-    Aig_ObjSetTravIdCurrent(p->pAig, pRepr);
-    Vec_PtrPush( p->vSimClasses, pRepr );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Collect equivalence classes and const1 cands in the TFO.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
- 
-***********************************************************************/
-void Ssw_ManCollectTfoCands( Ssw_Man_t * p, Aig_Obj_t * pObj1, Aig_Obj_t * pObj2 )
-{
-    Vec_PtrClear( p->vSimRoots );
-    Vec_PtrClear( p->vSimClasses );
-    Aig_ManIncrementTravId( p->pAig );
-    Aig_ObjSetTravIdCurrent( p->pAig, Aig_ManConst1(p->pAig) );    
-    Ssw_ManCollectTfoCands_rec( p, pObj1 );
-    Ssw_ManCollectTfoCands_rec( p, pObj2 );
-    Vec_PtrSort( p->vSimRoots,   Aig_ObjCompareIdIncrease );
-    Vec_PtrSort( p->vSimClasses, Aig_ObjCompareIdIncrease );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Retrives value of the PI in the original AIG.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Ssw_ManOriginalPiValue( Ssw_Man_t * p, Aig_Obj_t * pObj, int f )
-{
-    Aig_Obj_t * pObjFraig;
-    int nVarNum, Value;
-    assert( Aig_ObjIsPi(pObj) );
-    pObjFraig = Ssw_ObjFraig( p, pObj, f );
-    nVarNum = Ssw_ObjSatNum( p, Aig_Regular(pObjFraig) );
-    Value = (!nVarNum)? 0 : (Aig_IsComplement(pObjFraig) ^ sat_solver_var_value( p->pSat, nVarNum ));
-    if ( p->pPars->fPolarFlip )
-    {
-        if ( Aig_Regular(pObjFraig)->fPhase )  Value ^= 1;
-    }
-/*
-    if ( nVarNum==0 )
-        printf( "x" );
-    else if ( Value == 0 )
-        printf( "0" );
-    else
-        printf( "1" );
-*/
-    return Value;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Resimulates the cone of influence of the solved nodes.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
- 
-***********************************************************************/
-void Ssw_ManResimulateSolved_rec( Ssw_Man_t * p, Aig_Obj_t * pObj, int f )
-{
-    if ( Aig_ObjIsTravIdCurrent(p->pAig, pObj) )
-        return;
-    Aig_ObjSetTravIdCurrent(p->pAig, pObj);
-    if ( Aig_ObjIsPi(pObj) )
-    {
-        pObj->fMarkB = Ssw_ManOriginalPiValue( p, pObj, f );
-        return;
-    }
-    Ssw_ManResimulateSolved_rec( p, Aig_ObjFanin0(pObj), f );
-    Ssw_ManResimulateSolved_rec( p, Aig_ObjFanin1(pObj), f );
-    pObj->fMarkB = ( Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj) )
-                 & ( Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj) );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Resimulates the cone of influence of the other nodes.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Ssw_ManResimulateOther_rec( Ssw_Man_t * p, Aig_Obj_t * pObj )
-{
-    if ( Aig_ObjIsTravIdCurrent(p->pAig, pObj) )
-        return;
-    Aig_ObjSetTravIdCurrent(p->pAig, pObj);
-    if ( Aig_ObjIsPi(pObj) )
-    {
-        // set random value
-        pObj->fMarkB = Aig_ManRandom(0) & 1;
-        return;
-    }
-    Ssw_ManResimulateOther_rec( p, Aig_ObjFanin0(pObj) );
-    Ssw_ManResimulateOther_rec( p, Aig_ObjFanin1(pObj) );
-    pObj->fMarkB = ( Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj) )
-                 & ( Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj) );
-}
-
-/**Function*************************************************************
-
   Synopsis    [Handle the counter-example.]
 
   Description []
@@ -190,52 +39,7 @@ void Ssw_ManResimulateOther_rec( Ssw_Man_t * p, Aig_Obj_t * pObj )
   SeeAlso     []
 
 ***********************************************************************/
-void Ssw_ManResimulateCex( Ssw_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pRepr, int f )
-{
-    Aig_Obj_t * pRoot, ** ppClass;
-    int i, k, nSize, RetValue1, RetValue2, clk = clock();
-    // get the equivalence classes
-    Ssw_ManCollectTfoCands( p, pObj, pRepr );
-    // resimulate the cone of influence of the solved nodes
-    Aig_ManIncrementTravId( p->pAig );
-    Aig_ObjSetTravIdCurrent( p->pAig, Aig_ManConst1(p->pAig) );
-    Ssw_ManResimulateSolved_rec( p, pObj, f );
-    Ssw_ManResimulateSolved_rec( p, pRepr, f );
-    // resimulate the cone of influence of the other nodes
-    Vec_PtrForEachEntry( p->vSimRoots, pRoot, i )
-        Ssw_ManResimulateOther_rec( p, pRoot );
-    // refine these nodes
-    RetValue1 = Ssw_ClassesRefineConst1Group( p->ppClasses, p->vSimRoots, 0 );
-    // resimulate the cone of influence of the cand classes
-    RetValue2 = 0;
-    Vec_PtrForEachEntry( p->vSimClasses, pRoot, i )
-    {
-        ppClass = Ssw_ClassesReadClass( p->ppClasses, pRoot, &nSize );
-        for ( k = 0; k < nSize; k++ )
-            Ssw_ManResimulateOther_rec( p, ppClass[k] );
-        // refine this class
-        RetValue2 += Ssw_ClassesRefineOneClass( p->ppClasses, pRoot, 0 );
-    }
-    // make sure refinement happened
-    if ( Aig_ObjIsConst1(pRepr) )
-        assert( RetValue1 );
-    else
-        assert( RetValue2 );
-p->timeSimSat += clock() - clk;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Handle the counter-example.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Ssw_ManResimulateCexTotal( Ssw_Man_t * p, Aig_Obj_t * pCand, Aig_Obj_t * pRepr, int f )
+void Ssw_ManResimulateBit( Ssw_Man_t * p, Aig_Obj_t * pCand, Aig_Obj_t * pRepr )
 {
     Aig_Obj_t * pObj;
     int i, RetValue1, RetValue2, clk = clock();
@@ -255,18 +59,17 @@ void Ssw_ManResimulateCexTotal( Ssw_Man_t * p, Aig_Obj_t * pCand, Aig_Obj_t * pR
     {
         assert( RetValue1 );
         if ( RetValue1 == 0 )
-            printf( "\nSsw_ManResimulateCexTotal() Error: RetValue1 does not hold.\n" );
+            printf( "\nSsw_ManResimulateBit() Error: RetValue1 does not hold.\n" );
     }
     else
     {
         assert( RetValue2 );
         if ( RetValue2 == 0 )
-            printf( "\nSsw_ManResimulateCexTotal() Error: RetValue2 does not hold.\n" );
+            printf( "\nSsw_ManResimulateBit() Error: RetValue2 does not hold.\n" );
     }
 p->timeSimSat += clock() - clk;
 }
 
-
 /**Function*************************************************************
 
   Synopsis    [Handle the counter-example.]
@@ -278,7 +81,7 @@ p->timeSimSat += clock() - clk;
   SeeAlso     []
 
 ***********************************************************************/
-void Ssw_ManResimulateCexTotalSim( Ssw_Man_t * p, Aig_Obj_t * pCand, Aig_Obj_t * pRepr, int f )
+void Ssw_ManResimulateWord( Ssw_Man_t * p, Aig_Obj_t * pCand, Aig_Obj_t * pRepr, int f )
 {
     int RetValue1, RetValue2, clk = clock();
     // set the PI simulation information
@@ -293,18 +96,17 @@ void Ssw_ManResimulateCexTotalSim( Ssw_Man_t * p, Aig_Obj_t * pCand, Aig_Obj_t *
     {
         assert( RetValue1 );
         if ( RetValue1 == 0 )
-            printf( "\nSsw_ManResimulateCexTotalSim() Error: RetValue1 does not hold.\n" );
+            printf( "\nSsw_ManResimulateWord() Error: RetValue1 does not hold.\n" );
     }
     else
     {
         assert( RetValue2 );
         if ( RetValue2 == 0 )
-            printf( "\nSsw_ManResimulateCexTotalSim() Error: RetValue2 does not hold.\n" );
+            printf( "\nSsw_ManResimulateWord() Error: RetValue2 does not hold.\n" );
     }
 p->timeSimSat += clock() - clk;
 }
 
-
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/ssw/sswSweep.c b/src/aig/ssw/sswSweep.c
index 1cf4b81b..9330dafa 100644
--- a/src/aig/ssw/sswSweep.c
+++ b/src/aig/ssw/sswSweep.c
@@ -78,6 +78,33 @@ void Ssw_ManSweepMarkRefinement( Ssw_Man_t * p )
 
 /**Function*************************************************************
 
+  Synopsis    [Retrives value of the PI in the original AIG.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ssw_ManOriginalPiValue( Ssw_Man_t * p, Aig_Obj_t * pObj, int f )
+{
+    Aig_Obj_t * pObjFraig;
+    int nVarNum, Value;
+    assert( Aig_ObjIsPi(pObj) );
+    pObjFraig = Ssw_ObjFrame( p, pObj, f );
+    nVarNum = Ssw_ObjSatNum( p, Aig_Regular(pObjFraig) );
+    Value = (!nVarNum)? 0 : (Aig_IsComplement(pObjFraig) ^ sat_solver_var_value( p->pSat, nVarNum ));
+//    Value = (!nVarNum)? Aig_ManRandom(0) & 1 : (Aig_IsComplement(pObjFraig) ^ sat_solver_var_value( p->pSat, nVarNum ));
+    if ( p->pPars->fPolarFlip )
+    {
+        if ( Aig_Regular(pObjFraig)->fPhase )  Value ^= 1;
+    }
+    return Value;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Copy pattern from the solver into the internal storage.]
 
   Description []
@@ -114,7 +141,7 @@ void Ssw_SmlSavePatternAigPhase( Ssw_Man_t * p, int f )
     int i;
     memset( p->pPatWords, 0, sizeof(unsigned) * p->nPatWords );
     Aig_ManForEachPi( p->pAig, pObj, i )
-        if ( Aig_ObjPhaseReal( Ssw_ObjFraig(p, pObj, f) ) )
+        if ( Aig_ObjPhaseReal( Ssw_ObjFrame(p, pObj, f) ) )
             Aig_InfoSetBit( p->pPatWords, i );
 }
 
@@ -138,9 +165,9 @@ void Ssw_ManSweepNode( Ssw_Man_t * p, Aig_Obj_t * pObj, int f, int fBmc )
     if ( pObjRepr == NULL )
         return;
     // get the fraiged node
-    pObjFraig = Ssw_ObjFraig( p, pObj, f );
+    pObjFraig = Ssw_ObjFrame( p, pObj, f );
     // get the fraiged representative
-    pObjReprFraig = Ssw_ObjFraig( p, pObjRepr, f );
+    pObjReprFraig = Ssw_ObjFrame( p, pObjRepr, f );
     // check if constant 0 pattern distinquishes these nodes
     assert( pObjFraig != NULL && pObjReprFraig != NULL );
     if ( (pObj->fPhase == pObjRepr->fPhase) != (Aig_ObjPhaseReal(pObjFraig) == Aig_ObjPhaseReal(pObjReprFraig)) )
@@ -168,7 +195,7 @@ void Ssw_ManSweepNode( Ssw_Man_t * p, Aig_Obj_t * pObj, int f, int fBmc )
         if ( RetValue == 1 )  // proved equivalent
         {
             pObjFraig2 = Aig_NotCond( pObjReprFraig, pObj->fPhase ^ pObjRepr->fPhase );
-            Ssw_ObjSetFraig( p, pObj, f, pObjFraig2 );
+            Ssw_ObjSetFrame( p, pObj, f, pObjFraig2 );
             return;
         }
         if ( RetValue == -1 ) // timed out
@@ -181,16 +208,15 @@ void Ssw_ManSweepNode( Ssw_Man_t * p, Aig_Obj_t * pObj, int f, int fBmc )
         if ( p->pPars->fSkipCheck && !fBmc && !pObj->fMarkA && !pObjRepr->fMarkA )
         {
             assert( 0 );
-            printf( "\nMistake!!!\n" );
+            printf( "\nSsw_ManSweepNode(): Error!\n" );
         }
         // disproved the equivalence
         Ssw_SmlSavePatternAig( p, f );
     }
-//    Ssw_ManResimulateCex( p, pObj, pObjRepr, f );
     if ( p->pPars->nConstrs == 0 )
-        Ssw_ManResimulateCexTotalSim( p, pObj, pObjRepr, f );
+        Ssw_ManResimulateWord( p, pObj, pObjRepr, f );
     else
-        Ssw_ManResimulateCexTotal( p, pObj, pObjRepr, f );
+        Ssw_ManResimulateBit( p, pObj, pObjRepr );
     assert( Aig_ObjRepr( p->pAig, pObj ) != pObjRepr );
     p->fRefined = 1;
 }
@@ -216,7 +242,7 @@ clk = clock();
     // start initialized timeframes
     p->pFrames = Aig_ManStart( Aig_ManObjNumMax(p->pAig) * p->pPars->nFramesK );
     Saig_ManForEachLo( p->pAig, pObj, i )
-        Ssw_ObjSetFraig( p, pObj, 0, Aig_ManConst0(p->pFrames) );
+        Ssw_ObjSetFrame( p, pObj, 0, Aig_ManConst0(p->pFrames) );
 
     // sweep internal nodes
     p->fRefined = 0;
@@ -226,16 +252,16 @@ clk = clock();
     for ( f = 0; f < p->pPars->nFramesK; f++ )
     {
         // map constants and PIs
-        Ssw_ObjSetFraig( p, Aig_ManConst1(p->pAig), f, Aig_ManConst1(p->pFrames) );
+        Ssw_ObjSetFrame( p, Aig_ManConst1(p->pAig), f, Aig_ManConst1(p->pFrames) );
         Saig_ManForEachPi( p->pAig, pObj, i )
-            Ssw_ObjSetFraig( p, pObj, f, Aig_ObjCreatePi(p->pFrames) );
+            Ssw_ObjSetFrame( p, pObj, f, Aig_ObjCreatePi(p->pFrames) );
         // sweep internal nodes
         Aig_ManForEachNode( p->pAig, pObj, i )
         {
             if ( p->pPars->fVerbose )
                 Bar_ProgressUpdate( pProgress, Aig_ManObjNumMax(p->pAig) * f + i, NULL );
             pObjNew = Aig_And( p->pFrames, Ssw_ObjChild0Fra(p, pObj, f), Ssw_ObjChild1Fra(p, pObj, f) );
-            Ssw_ObjSetFraig( p, pObj, f, pObjNew );
+            Ssw_ObjSetFrame( p, pObj, f, pObjNew );
             Ssw_ManSweepNode( p, pObj, f, 1 );
         }
         // quit if this is the last timeframe
@@ -246,7 +272,7 @@ clk = clock();
         Saig_ManForEachLiLo( p->pAig, pObjLi, pObjLo, i )
         {
             pObjNew = Ssw_ObjChild0Fra(p, pObjLi,f);
-            Ssw_ObjSetFraig( p, pObjLo, f+1, pObjNew );
+            Ssw_ObjSetFrame( p, pObjLo, f+1, pObjNew );
             Ssw_CnfNodeAddToSolver( p, Aig_Regular(pObjNew) );
         }
     }
@@ -307,12 +333,12 @@ p->timeMarkCones += clock() - clk;
 
     // map constants and PIs of the last frame
     f = p->pPars->nFramesK;
-    Ssw_ObjSetFraig( p, Aig_ManConst1(p->pAig), f, Aig_ManConst1(p->pFrames) );
+    Ssw_ObjSetFrame( p, Aig_ManConst1(p->pAig), f, Aig_ManConst1(p->pFrames) );
     Saig_ManForEachPi( p->pAig, pObj, i )
-        Ssw_ObjSetFraig( p, pObj, f, Aig_ObjCreatePi(p->pFrames) );
+        Ssw_ObjSetFrame( p, pObj, f, Aig_ObjCreatePi(p->pFrames) );
     // make sure LOs are assigned
     Saig_ManForEachLo( p->pAig, pObj, i )
-        assert( Ssw_ObjFraig( p, pObj, f ) != NULL );
+        assert( Ssw_ObjFrame( p, pObj, f ) != NULL );
     // sweep internal nodes
     p->fRefined = 0;
     p->nSatFailsReal = 0;
@@ -330,7 +356,7 @@ p->timeMarkCones += clock() - clk;
         { 
             pObj->fMarkA = Aig_ObjFanin0(pObj)->fMarkA | Aig_ObjFanin1(pObj)->fMarkA;
             pObjNew = Aig_And( p->pFrames, Ssw_ObjChild0Fra(p, pObj, f), Ssw_ObjChild1Fra(p, pObj, f) );
-            Ssw_ObjSetFraig( p, pObj, f, pObjNew );
+            Ssw_ObjSetFrame( p, pObj, f, pObjNew );
             Ssw_ManSweepNode( p, pObj, f, 0 );
         }
     }
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 7247f8ed..09fd26ab 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -13888,10 +13888,10 @@ int Abc_CommandLcorr( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     // set defaults
     nFramesP   =     0;
-    nConfMax   = 10000;
-    nVarsMax   =  5000;
+    nConfMax   =  1000;
+    nVarsMax   =  1000;
     fNewAlgor  =     0;
-    fVerbose   =     1;
+    fVerbose   =     0;
     Extra_UtilGetoptReset();
     while ( ( c = Extra_UtilGetopt( argc, argv, "PCSnvh" ) ) != EOF )
     {
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index ac5ee882..71443265 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -1335,7 +1335,6 @@ Abc_Ntk_t * Abc_NtkDarLcorrNew( Abc_Ntk_t * pNtk, int nVarsMax, int nConfMax, in
         return NULL;
     Ssw_ManSetDefaultParams( pPars );
     pPars->fLatchCorrOpt = 1;
-//    pPars->nFramesAddSim = 0;
     pPars->nBTLimit      = nConfMax;
     pPars->nSatVarMax    = nVarsMax;
     pPars->fVerbose      = fVerbose;
diff --git a/src/map/pcm/module.make b/src/map/pcm/module.make
deleted file mode 100644
index e69de29b..00000000
--- a/src/map/pcm/module.make
+++ /dev/null
diff --git a/src/map/ply/module.make b/src/map/ply/module.make
deleted file mode 100644
index e69de29b..00000000
--- a/src/map/ply/module.make
+++ /dev/null
diff --git a/src/sat/bsat/satInterA.c b/src/sat/bsat/satInterA.c
index 967639ae..57628989 100644
--- a/src/sat/bsat/satInterA.c
+++ b/src/sat/bsat/satInterA.c
@@ -544,13 +544,7 @@ int Inta_ManProofTraceOne( Inta_Man_t * p, Sto_Cls_t * pConflict, Sto_Cls_t * pF
     int i, v, Var, PrevId;
     int fPrint = 0;
     int clk = clock();
-/*
-    if ( pFinal->Id == 5187 )
-    {
-        int x = 0;
-        Inta_ManPrintClause( p, pConflict );
-    }
-*/
+
     // collect resolvent literals
     if ( p->fProofVerif )
     {
@@ -579,28 +573,17 @@ int Inta_ManProofTraceOne( Inta_Man_t * p, Sto_Cls_t * pConflict, Sto_Cls_t * pF
         if ( !p->pSeens[Var] )
             continue;
         p->pSeens[Var] = 0;
-/*
-        if ( pFinal->Id == 5187 )
-        {
-            printf( "pivot = %d  ", p->pTrail[i] );
-        }
-*/
+
         // skip literals of the resulting clause
         pReason = p->pReasons[Var];
         if ( pReason == NULL )
             continue;
         assert( p->pTrail[i] == pReason->pLits[0] );
-/*
-        if ( pFinal->Id == 5187 )
-        {
-            Inta_ManPrintClause( p, pReason );
-        }
-*/
+
         // add the variables to seen
         for ( v = 1; v < (int)pReason->nLits; v++ )
             p->pSeens[lit_var(pReason->pLits[v])] = 1;
 
-
         // record the reason clause
         assert( Inta_ManProofGet(p, pReason) > 0 );
         p->Counter++;
@@ -656,7 +639,6 @@ int Inta_ManProofTraceOne( Inta_Man_t * p, Sto_Cls_t * pConflict, Sto_Cls_t * pF
                 printf( "Recording clause %d: Trying to resolve the clause with more than one opposite literal.\n", pFinal->Id );
             }
         }
-
 //        Vec_PtrPush( pFinal->pAntis, pReason );
     }
 
@@ -673,20 +655,6 @@ int Inta_ManProofTraceOne( Inta_Man_t * p, Sto_Cls_t * pConflict, Sto_Cls_t * pF
         int v1, v2; 
         if ( fPrint )
             Inta_ManPrintResolvent( p->pResLits, p->nResLits );
-/*
-        if ( pFinal->Id == 5187 )
-        {
-            Inta_ManPrintResolvent( p->pResLits, p->nResLits );
-            Inta_ManPrintClause( p, pFinal );
-        }
-*/
-/*
-        if ( p->nResLits != pFinal->nLits )
-        {
-            printf( "Recording clause %d: The resolvent is wrong (nRetLits = %d, pFinal->nLits = %d).\n", 
-                pFinal->Id, p->nResLits, pFinal->nLits );
-        }
-*/
         for ( v1 = 0; v1 < p->nResLits; v1++ )
         {
             for ( v2 = 0; v2 < (int)pFinal->nLits; v2++ )
@@ -703,6 +671,27 @@ int Inta_ManProofTraceOne( Inta_Man_t * p, Sto_Cls_t * pConflict, Sto_Cls_t * pF
             Inta_ManPrintResolvent( p->pResLits, p->nResLits );
             Inta_ManPrintClause( p, pFinal );
         }
+
+        // if there are literals in the clause that are not in the resolvent
+        // it means that the derived resolvent is stronger than the clause
+        // we can replace the clause with the resolvent by removing these literals
+        if ( p->nResLits != (int)pFinal->nLits )
+        {
+            for ( v1 = 0; v1 < (int)pFinal->nLits; v1++ )
+            {
+                for ( v2 = 0; v2 < p->nResLits; v2++ )
+                    if ( pFinal->pLits[v1] == p->pResLits[v2] )
+                        break;
+                if ( v2 < p->nResLits )
+                    continue;
+                // remove literal v1 from the final clause
+                pFinal->nLits--;
+                for ( v2 = v1; v2 < (int)pFinal->nLits; v2++ )
+                    pFinal->pLits[v2] = pFinal->pLits[v2+1];
+                v1--;
+            }
+            assert( p->nResLits == (int)pFinal->nLits );
+        }
     }
 p->timeTrace += clock() - clk;
 
@@ -736,9 +725,16 @@ int Inta_ManProofRecordOne( Inta_Man_t * p, Sto_Cls_t * pClause )
     if ( pClause->nLits == 0 )
         printf( "Error: Empty clause is attempted.\n" );
 
-    // add assumptions to the trail
     assert( !pClause->fRoot );
     assert( p->nTrailSize == p->nRootSize );
+
+    // if any of the clause literals are already assumed
+    // it means that the clause is redundant and can be skipped
+    for ( i = 0; i < (int)pClause->nLits; i++ )
+        if ( p->pAssigns[lit_var(pClause->pLits[i])] == pClause->pLits[i] )
+            return 1;
+
+    // add assumptions to the trail
     for ( i = 0; i < (int)pClause->nLits; i++ )
         if ( !Inta_ManEnqueue( p, lit_neg(pClause->pLits[i]), NULL ) )
         {
author	Alan Mishchenko <alanmi@berkeley.edu>	2008-09-21 08:01:00 -0700
committer	Alan Mishchenko <alanmi@berkeley.edu>	2008-09-21 08:01:00 -0700
commit	4d71c114a3405f0a2c59a8467c82a8da3f785262 (patch)
tree	1c4a0fdf938e247b03e832f26c74c8a48af2826b /src
parent	3429e6309d0fc9a2d35d81f6483258c6af2fab50 (diff)
download	abc-4d71c114a3405f0a2c59a8467c82a8da3f785262.tar.gz abc-4d71c114a3405f0a2c59a8467c82a8da3f785262.tar.bz2 abc-4d71c114a3405f0a2c59a8467c82a8da3f785262.zip