Version abc70822

9 files changed, 380 insertions, 78 deletions

diff --git a/src/aig/fra/fra.h b/src/aig/fra/fra.h
index c8617d84..217d1fba 100644
--- a/src/aig/fra/fra.h
+++ b/src/aig/fra/fra.h
@@ -73,6 +73,7 @@ struct Fra_Par_t_
     int              nBTLimitMiter;     // conflict limit at an output
     int              nFramesP;          // the number of timeframes to in the prefix
     int              nFramesK;          // the number of timeframes to unroll
+    int              nMaxImps;          // the maximum number of implications to consider
     int              fRewrite;          // use rewriting for constraint reduction
     int              fLatchCorr;        // computes latch correspondence only
     int              fUseImps;          // use implications
@@ -133,6 +134,7 @@ struct Fra_Man_t_
     // counter example storage
     int              nPatWords;         // the number of words in the counter example
     unsigned *       pPatWords;         // the counter example
+    Vec_Int_t *      vCex;
     // satisfiability solving
     sat_solver *     pSat;              // SAT solver
     int              nSatVars;          // the number of variables currently used
@@ -226,6 +228,8 @@ extern int                 Fra_ClassesCountPairs( Fra_Cla_t * p );
 extern void                Fra_ClassesTest( Fra_Cla_t * p, int Id1, int Id2 );
 extern void                Fra_ClassesLatchCorr( Fra_Man_t * p );
 extern void                Fra_ClassesPostprocess( Fra_Cla_t * p );
+extern void                Fra_ClassesSelectRepr( Fra_Cla_t * p );
+extern Aig_Man_t *         Fra_ClassesDeriveAig( Fra_Cla_t * p, int nFramesK );
 /*=== fraCnf.c ========================================================*/
 extern void                Fra_CnfNodeAddToSolver( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew );
 /*=== fraCore.c ========================================================*/
@@ -240,7 +244,7 @@ extern int                 Fra_ImpCheckForNode( Fra_Man_t * p, Vec_Int_t * vImps
 extern int                 Fra_ImpRefineUsingCex( Fra_Man_t * p, Vec_Int_t * vImps );
 extern void                Fra_ImpCompactArray( Vec_Int_t * vImps );
 /*=== fraInd.c ========================================================*/
-extern Aig_Man_t *         Fra_FraigInduction( Aig_Man_t * p, int nFramesP, int nFramesK, int fRewrite, int fUseImps, int fLatchCorr, int fVerbose, int * pnIter );
+extern Aig_Man_t *         Fra_FraigInduction( Aig_Man_t * p, int nFramesP, int nFramesK, int nMaxImps, int fRewrite, int fUseImps, int fLatchCorr, int fVerbose, int * pnIter );
 /*=== fraMan.c ========================================================*/
 extern void                Fra_ParamsDefault( Fra_Par_t * pParams );
 extern void                Fra_ParamsDefaultSeq( Fra_Par_t * pParams );
diff --git a/src/aig/fra/fraClass.c b/src/aig/fra/fraClass.c
index a9d727da..d6db125b 100644
--- a/src/aig/fra/fraClass.c
+++ b/src/aig/fra/fraClass.c
@@ -114,9 +114,18 @@ void Fra_ClassesCopyReprs( Fra_Cla_t * p, Vec_Ptr_t * vFailed )
     int i;
     Aig_ManReprStart( p->pAig, Aig_ManObjIdMax(p->pAig) + 1 );
     memmove( p->pAig->pReprs, p->pMemRepr, sizeof(Aig_Obj_t *) * (Aig_ManObjIdMax(p->pAig) + 1) );
+    if ( Vec_PtrSize(p->vClasses1) == 0 && Vec_PtrSize(p->vClasses) == 0 )
+    {
+        Aig_ManForEachObj( p->pAig, pObj, i )
+        {
+            if ( p->pAig->pReprs[i] != NULL )
+                printf( "Classes are not cleared!\n" );
+            assert( p->pAig->pReprs[i] == NULL );
+        }
+    }
     if ( vFailed )
-    Vec_PtrForEachEntry( vFailed, pObj, i )
-        p->pAig->pReprs[pObj->Id] = NULL;
+        Vec_PtrForEachEntry( vFailed, pObj, i )
+            p->pAig->pReprs[pObj->Id] = NULL;
 }
 
 /**Function*************************************************************
@@ -206,7 +215,7 @@ void Fra_PrintClass( Aig_Obj_t ** pClass )
         assert( Fra_ClassObjRepr(pTemp) == pClass[0] );
     printf( "{ " );
     for ( i = 0; pTemp = pClass[i]; i++ )
-        printf( "%d ", pTemp->Id, Fra_ClassObjRepr(pTemp)? Fra_ClassObjRepr(pTemp)->Id : -1 );
+        printf( "%d(%d) ", pTemp->Id, pTemp->Level );
     printf( "}\n" );
 }
 
@@ -227,8 +236,11 @@ void Fra_ClassesPrint( Fra_Cla_t * p, int fVeryVerbose )
     Aig_Obj_t * pObj;
     int i;
 
-    printf( "Const = %5d. Class = %5d. Lit = %5d.\n", 
+    printf( "Const = %5d. Class = %5d. Lit = %5d. ", 
         Vec_PtrSize(p->vClasses1), Vec_PtrSize(p->vClasses), Fra_ClassesCountLits(p) );
+    if ( p->vImps && Vec_IntSize(p->vImps) > 0 )
+        printf( "Imp = %5d. ", Vec_IntSize(p->vImps) );
+    printf( "\n" );
 
     if ( fVeryVerbose )
     {
@@ -283,10 +295,10 @@ void Fra_ClassesPrepare( Fra_Cla_t * p, int fLatchCorr )
         {
             if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsPi(pObj) )
                 continue;
+            // skip the node with more that the given number of levels
+//            if ( pObj->Level > 3 )
+//                continue;
         }
-//printf( "%3d : ", pObj->Id );
-//Extra_PrintBinary( stdout, Fra_ObjSim(pObj), 32 );
-//printf( "\n" );
         // hash the node by its simulation info
         iEntry = p->pFuncNodeHash( pObj, nTableSize );
         // check if the node belongs to the class of constant 1
@@ -494,7 +506,6 @@ int Fra_ClassesRefine( Fra_Cla_t * p )
     vTemp = p->vClassesTemp;
     p->vClassesTemp = p->vClasses;
     p->vClasses = vTemp;
-    p->fRefinement = (nRefis > 0);
     return nRefis;
 }
 
@@ -531,7 +542,6 @@ int Fra_ClassesRefine1( Fra_Cla_t * p )
     Vec_PtrShrink( p->vClasses1, k );
     if ( Vec_PtrSize(p->vClassNew) == 0 )
         return 0;
-    p->fRefinement = 1;
 /*
     printf( "Refined const-1 class: {" );
     Vec_PtrForEachEntry( p->vClassNew, pObj, i )
@@ -677,6 +687,95 @@ void Fra_ClassesPostprocess( Fra_Cla_t * p )
 
 /**Function*************************************************************
 
+  Synopsis    [Postprocesses the classes by selecting representative lowest in top order.]
+
+  Description []
+               
+  SideEffects [] 
+
+  SeeAlso     []
+
+***********************************************************************/
+void Fra_ClassesSelectRepr( Fra_Cla_t * p )
+{
+    Aig_Obj_t ** pClass, * pNodeMin;
+    int i, c, cMinSupp, nSuppSizeMin, nSuppSizeCur;
+    // reassign representatives in each class
+    Vec_PtrForEachEntry( p->vClasses, pClass, i )
+    {
+        // collect support sizes and find the min-support node
+        pNodeMin = NULL;
+        nSuppSizeMin = AIG_INFINITY;
+        for ( c = 0; pClass[c]; c++ )
+        {
+            nSuppSizeCur = Aig_SupportSize( p->pAig, pClass[c] );
+//            nSuppSizeCur = 1;
+            if ( nSuppSizeMin > nSuppSizeCur || 
+                (nSuppSizeMin == nSuppSizeCur && pNodeMin->Level > pClass[c]->Level) )
+            {
+                nSuppSizeMin = nSuppSizeCur;
+                pNodeMin = pClass[c];
+                cMinSupp = c; 
+            }
+        }
+        // skip the case when the repr did not change
+        if ( cMinSupp == 0 )
+            continue;
+        // make the new node the representative of the class
+        pClass[cMinSupp] = pClass[0];
+        pClass[0] = pNodeMin;
+        // set the representative
+        for ( c = 0; pClass[c]; c++ )
+            Fra_ClassObjSetRepr( pClass[c], c? pClass[0] : NULL );
+    }
+}
+
+
+
+static inline Aig_Obj_t * Fra_ObjEqu( Aig_Obj_t ** ppEquivs, Aig_Obj_t * pObj )                       { return ppEquivs[pObj->Id];  }
+static inline void        Fra_ObjSetEqu( Aig_Obj_t ** ppEquivs, Aig_Obj_t * pObj, Aig_Obj_t * pNode ) { ppEquivs[pObj->Id] = pNode; }
+
+static inline Aig_Obj_t * Fra_ObjChild0Equ( Aig_Obj_t ** ppEquivs, Aig_Obj_t * pObj ) { return Aig_NotCond(Fra_ObjEqu(ppEquivs,Aig_ObjFanin0(pObj)), Aig_ObjFaninC0(pObj));  }
+static inline Aig_Obj_t * Fra_ObjChild1Equ( Aig_Obj_t ** ppEquivs, Aig_Obj_t * pObj ) { return Aig_NotCond(Fra_ObjEqu(ppEquivs,Aig_ObjFanin1(pObj)), Aig_ObjFaninC1(pObj));  }
+
+/**Function*************************************************************
+
+  Synopsis    [Add the node and its constraints to the new AIG.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Fra_ClassesDeriveNode( Aig_Man_t * pManFraig, Aig_Obj_t * pObj, Aig_Obj_t ** ppEquivs )
+{
+    Aig_Obj_t * pObjNew, * pObjRepr, * pObjReprNew, * pMiter;//, * pObjNew2;
+    // skip nodes without representative
+    if ( (pObjRepr = Fra_ClassObjRepr(pObj)) == NULL )
+        return;
+    assert( pObjRepr->Id < pObj->Id );
+    // get the new node 
+    pObjNew = Fra_ObjEqu( ppEquivs, pObj );
+    // get the new node of the representative
+    pObjReprNew = Fra_ObjEqu( ppEquivs, pObjRepr );
+    // if this is the same node, no need to add constraints
+    if ( Aig_Regular(pObjNew) == Aig_Regular(pObjReprNew) )
+        return;
+    // these are different nodes - perform speculative reduction
+//    pObjNew2 = Aig_NotCond( pObjReprNew, pObj->fPhase ^ pObjRepr->fPhase );
+    // set the new node
+//    Fra_ObjSetEqu( ppEquivs, pObj, pObjNew2 );
+    // add the constraint
+    pMiter = Aig_Exor( pManFraig, Aig_Regular(pObjNew), Aig_Regular(pObjReprNew) );
+    pMiter = Aig_NotCond( pMiter, Aig_Regular(pMiter)->fPhase ^ Aig_IsComplement(pMiter) );
+    pMiter = Aig_Not( pMiter );
+    Aig_ObjCreatePo( pManFraig, pMiter );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Derives AIG for the partitioned problem.]
 
   Description []
@@ -688,7 +787,60 @@ void Fra_ClassesPostprocess( Fra_Cla_t * p )
 ***********************************************************************/
 Aig_Man_t * Fra_ClassesDeriveAig( Fra_Cla_t * p, int nFramesK )
 {
-
+    Aig_Man_t * pManFraig;
+    Aig_Obj_t * pObj, * pObjNew;
+    Aig_Obj_t ** pLatches, ** ppEquivs;
+    int i, k, f, nFramesAll = nFramesK + 1;
+    assert( Aig_ManRegNum(p->pAig) > 0 );
+    assert( Aig_ManRegNum(p->pAig) < Aig_ManPiNum(p->pAig) );
+    assert( nFramesK > 0 );
+    // start the fraig package
+    pManFraig = Aig_ManStart( (Aig_ManObjIdMax(p->pAig) + 1) * nFramesAll );
+    // allocate place for the node mapping
+    ppEquivs = ALLOC( Aig_Obj_t *, Aig_ManObjIdMax(p->pAig) + 1 );
+    Fra_ObjSetEqu( ppEquivs, Aig_ManConst1(p->pAig), Aig_ManConst1(pManFraig) );
+    // create latches for the first frame
+    Aig_ManForEachLoSeq( p->pAig, pObj, i )
+        Fra_ObjSetEqu( ppEquivs, pObj, Aig_ObjCreatePi(pManFraig) );
+    // add timeframes
+    pLatches = ALLOC( Aig_Obj_t *, Aig_ManRegNum(p->pAig) );
+    for ( f = 0; f < nFramesAll; f++ )
+    {
+        // create PIs for this frame
+        Aig_ManForEachPiSeq( p->pAig, pObj, i )
+            Fra_ObjSetEqu( ppEquivs, pObj, Aig_ObjCreatePi(pManFraig) );
+        // set the constraints on the latch outputs
+        Aig_ManForEachLoSeq( p->pAig, pObj, i )
+            Fra_ClassesDeriveNode( pManFraig, pObj, ppEquivs );
+        // add internal nodes of this frame
+        Aig_ManForEachNode( p->pAig, pObj, i )
+        {
+            pObjNew = Aig_And( pManFraig, Fra_ObjChild0Equ(ppEquivs, pObj), Fra_ObjChild1Equ(ppEquivs, pObj) );
+            Fra_ObjSetEqu( ppEquivs, pObj, pObjNew );
+            Fra_ClassesDeriveNode( pManFraig, pObj, ppEquivs );
+        }
+        if ( f == nFramesAll - 1 )
+            break;
+        if ( f == nFramesAll - 2 )
+            pManFraig->nAsserts = Aig_ManPoNum(pManFraig);
+        // save the latch input values
+        k = 0;
+        Aig_ManForEachLiSeq( p->pAig, pObj, i )
+            pLatches[k++] = Fra_ObjChild0Equ( ppEquivs, pObj );
+        // insert them to the latch output values
+        k = 0;
+        Aig_ManForEachLoSeq( p->pAig, pObj, i )
+            Fra_ObjSetEqu( ppEquivs, pObj, pLatches[k++] );
+    }
+    free( pLatches );
+    free( ppEquivs );
+    // mark the asserts
+    assert( Aig_ManPoNum(pManFraig) % nFramesAll == 0 );
+printf( "Assert miters = %6d. Output miters = %6d.\n", 
+       pManFraig->nAsserts, Aig_ManPoNum(pManFraig) - pManFraig->nAsserts );
+    // remove dangling nodes
+    Aig_ManCleanup( pManFraig );
+    return pManFraig;
 }
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/fra/fraCore.c b/src/aig/fra/fraCore.c
index 3c76af03..9adbb7a9 100644
--- a/src/aig/fra/fraCore.c
+++ b/src/aig/fra/fraCore.c
@@ -24,6 +24,23 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
+/* 
+    Speculating reduction in the sequential case leads to an interesting 
+    situation when a counter-ex may not refine any classes. This happens
+    for non-constant equivalence classes. In such cases the representative
+    of the class (proved by simulation to be non-constant) may be reduced 
+    to a constant during the speculative reduction. The fraig-representative 
+    of this representative node is a constant node, even though this is a 
+    non-constant class. Experiments have shown that this situation happens 
+    very often at the beginning of the refinement iteration when there are 
+    many spurious candidate equivalence classes (especially if heavy-duty 
+    simulatation of BMC was node used at the beginning). As a result, the 
+    SAT solver run may return a counter-ex that  distinguishes the given 
+    representative node from the constant-1 node but this counter-ex
+    does not distinguish the nodes in the non-costant class... This is why 
+    there is no check of refinment after a counter-ex in the sequential case.
+*/
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
@@ -117,6 +134,54 @@ static inline void Fra_FraigNodeSpeculate( Fra_Man_t * p, Aig_Obj_t * pObj, Aig_
 
 /**Function*************************************************************
 
+  Synopsis    [Verifies the generated counter-ex.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Fra_FraigVerifyCounterEx( Fra_Man_t * p, Vec_Int_t * vCex )
+{
+    Aig_Obj_t * pObj, ** ppClass;
+    int i, c;
+    assert( Aig_ManPiNum(p->pManAig) == Vec_IntSize(vCex) );
+    // make sure the input pattern is not used
+    Aig_ManForEachObj( p->pManAig, pObj, i )
+        assert( !pObj->fMarkB );
+    // simulate the cex through the AIG
+    Aig_ManConst1(p->pManAig)->fMarkB = 1;
+    Aig_ManForEachPi( p->pManAig, pObj, i )
+        pObj->fMarkB = Vec_IntEntry(vCex, i);
+    Aig_ManForEachNode( p->pManAig, pObj, i )
+        pObj->fMarkB = (Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj)) & 
+                       (Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj));
+    Aig_ManForEachPo( p->pManAig, pObj, i )
+        pObj->fMarkB = Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj);
+    // check if the classes hold
+    Vec_PtrForEachEntry( p->pCla->vClasses1, pObj, i )
+    {
+        if ( pObj->fPhase != pObj->fMarkB )
+            printf( "The node %d is not constant under cex!\n", pObj->Id );
+    }
+    Vec_PtrForEachEntry( p->pCla->vClasses, ppClass, i )
+    {
+        for ( c = 1; ppClass[c]; c++ )
+            if ( (ppClass[0]->fPhase ^ ppClass[c]->fPhase) != (ppClass[0]->fMarkB ^ ppClass[c]->fMarkB) )
+                printf( "The nodes %d and %d are not equal under cex!\n", ppClass[0]->Id, ppClass[c]->Id );
+//        for ( c = 0; ppClass[c]; c++ )
+//            if ( Fra_ObjFraig(ppClass[c],p->pPars->nFramesK) == Aig_ManConst1(p->pManFraig) )
+//                printf( "A member of non-constant class has a constant repr!\n" );
+    }
+    // clean the simulation pattern
+    Aig_ManForEachObj( p->pManAig, pObj, i )
+        pObj->fMarkB = 0;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Performs fraiging for one node.]
 
   Description [Returns the fraiged node.]
@@ -173,47 +238,20 @@ static inline void Fra_FraigNode( Fra_Man_t * p, Aig_Obj_t * pObj )
         Fra_FraigNodeSpeculate( p, pObj, Aig_Regular(pObjFraig), Aig_Regular(pObjReprFraig) );
         return;
     }
-//printf( "Disproved %d and %d.\n", pObj->Id, pObjRepr->Id );
     // disprove the nodes
+    p->pCla->fRefinement = 1;
     // if we do not include the node into those disproved, we may end up 
     // merging this node with another representative, for which proof has timed out
     if ( p->vTimeouts )
         Vec_PtrPush( p->vTimeouts, pObj );
+    // verify that the counter-example satisfies all the constraints
+//    if ( p->vCex )
+//    Fra_FraigVerifyCounterEx( p, p->vCex );
     // simulate the counter-example and return the Fraig node
     Fra_SmlResimulate( p );
-/*
-printf( "%d -> %d.\n", pObj->Id, pObjRepr->Id );
-Fra_ClassesPrint( p->pCla, 1 );
-printf( "%3d : ", 19 );
-Extra_PrintBinary( stdout, Fra_ObjSim(p->pSml, 19), 32 * p->pSml->nWordsTotal );
-printf( "\n" );
-printf( "%3d : ", 27 );
-Extra_PrintBinary( stdout, Fra_ObjSim(p->pSml, 27), 32 * p->pSml->nWordsTotal );
-printf( "\n" );
-printf( "%3d : ", 30 );
-Extra_PrintBinary( stdout, Fra_ObjSim(p->pSml, 30), 32 * p->pSml->nWordsTotal );
-printf( "\n" );
-printf( "\n\n" );
-*/
-    if ( Fra_ClassObjRepr(pObj) == pObjRepr )
-    {
-/*
-//Fra_ClassesPrint( p->pCla, 1 );
-//printf( "\n\n" );
-printf( "%3d : ", pObj->Id );
-Extra_PrintBinary( stdout, Fra_ObjSim(p->pSml, pObj->Id), 32 * p->pSml->nWordsTotal );
-printf( "\n" );
-printf( "%3d : ", pObjRepr->Id );
-Extra_PrintBinary( stdout, Fra_ObjSim(p->pSml, pObjRepr->Id), 32 * p->pSml->nWordsTotal );
-printf( "\n" );
-*/
-        if ( Aig_ObjIsPi(pObj) )
-            printf( "primary input\n" );
-        else
-            printf( "NOT primary input\n" );
+    if ( !p->pPars->nFramesK && Fra_ClassObjRepr(pObj) == pObjRepr )
         printf( "Fra_FraigNode(): Error in class refinement!\n" );
-    }
-    assert( Fra_ClassObjRepr(pObj) != pObjRepr );
+    assert( p->pPars->nFramesK || Fra_ClassObjRepr(pObj) != pObjRepr );
 }
 
 /**Function*************************************************************
diff --git a/src/aig/fra/fraImp.c b/src/aig/fra/fraImp.c
index 25b34e03..8af11b78 100644
--- a/src/aig/fra/fraImp.c
+++ b/src/aig/fra/fraImp.c
@@ -205,7 +205,7 @@ Vec_Ptr_t * Fra_SmlSortUsingOnes( Fra_Sml_t * p, int fLatchCorr )
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Int_t * Fra_SmlSelectMaxCost( Vec_Int_t * vImps, int * pCosts, int nCostMax, int nImpLimit )
+Vec_Int_t * Fra_SmlSelectMaxCost( Vec_Int_t * vImps, int * pCosts, int nCostMax, int nImpLimit, int * pCostRange )
 {
     Vec_Int_t * vImpsNew;
     int * pCostCount, nImpCount, Imp, i, c;
@@ -239,6 +239,8 @@ Vec_Int_t * Fra_SmlSelectMaxCost( Vec_Int_t * vImps, int * pCosts, int nCostMax,
             break;
     }
     free( pCostCount );
+    if ( pCostRange )
+        *pCostRange = c;
     return vImpsNew;
 }
 
@@ -290,7 +292,7 @@ Vec_Int_t * Fra_ImpDerive( Fra_Man_t * p, int nImpMaxLimit, int nImpUseLimit, in
     int * pImpCosts, * pNodesI, * pNodesK;
     int nImpsTotal = 0, nImpsTried = 0, nImpsNonSeq = 0, nImpsComb = 0, nImpsCollected = 0;
     int CostMin = AIG_INFINITY, CostMax = 0;
-    int i, k, Imp, clk = clock();
+    int i, k, Imp, CostRange, clk = clock();
     assert( nImpMaxLimit > 0 && nImpUseLimit > 0 && nImpUseLimit <= nImpMaxLimit );
     // normalize both managers
     pComb = Fra_SmlSimulateComb( p->pManAig, nSimWords );
@@ -350,9 +352,10 @@ finish:
     Fra_SmlStop( pSeq );
 
     // select implications with the highest cost
+    CostRange = CostMin;
     if ( Vec_IntSize(vImps) > nImpUseLimit )
     {
-        vImps = Fra_SmlSelectMaxCost( vTemp = vImps, pImpCosts, nSimWords * 32, nImpUseLimit );
+        vImps = Fra_SmlSelectMaxCost( vTemp = vImps, pImpCosts, nSimWords * 32, nImpUseLimit, &CostRange );
         Vec_IntFree( vTemp );  
     }
 
@@ -365,8 +368,8 @@ finish:
             (int (*)(const void *, const void *)) Sml_CompareMaxId );
 if ( p->pPars->fVerbose )
 {
-printf( "Tot = %d. Try = %d. NonS = %d. C = %d. Found = %d.  Cost = [%d - %d]  ", 
-    nImpsTotal, nImpsTried, nImpsNonSeq, nImpsComb, nImpsCollected, CostMin, CostMax );
+printf( "Tot = %d. Try = %d. NonS = %d. C = %d. Found = %d.  Cost = [%d < %d < %d] ", 
+    nImpsTotal, nImpsTried, nImpsNonSeq, nImpsComb, nImpsCollected, CostMin, CostRange, CostMax );
 PRT( "Time", clock() - clk );
 }
     return vImps;
@@ -381,7 +384,7 @@ PRT( "Time", clock() - clk );
 
   Synopsis    [Add implication clauses to the SAT solver.]
 
-  Description []
+  Description [Note that implications should be checked in the first frame!]
                
   SideEffects []
 
@@ -540,7 +543,6 @@ int Fra_ImpRefineUsingCex( Fra_Man_t * p, Vec_Int_t * vImps )
         {
             Vec_IntWriteEntry( vImps, i, 0 );
             RetValue = 1;
-            p->pCla->fRefinement = 1;
         }
     }
     return RetValue;
diff --git a/src/aig/fra/fraInd.c b/src/aig/fra/fraInd.c
index d754f3ae..6d8305c0 100644
--- a/src/aig/fra/fraInd.c
+++ b/src/aig/fra/fraInd.c
@@ -50,11 +50,9 @@ void Fra_FraigInductionRewrite( Fra_Man_t * p )
     pTemp = Aig_ManDup( p->pManFraig, 0 );
 //    pTemp = Dar_ManRwsat( pTemp, 1, 0 );
     pTemp = Dar_ManRewriteDefault( pTemp );
-
 //    printf( "Before = %6d.  After = %6d.\n", Aig_ManNodeNum(p->pManFraig), Aig_ManNodeNum(pTemp) ); 
 //Aig_ManDumpBlif( p->pManFraig, "1.blif" );
 //Aig_ManDumpBlif( pTemp, "2.blif" );
-
 //    Fra_FramesWriteCone( pTemp );
 //    Aig_ManStop( pTemp );
     // transfer PI/register pointers
@@ -128,8 +126,7 @@ static inline void Fra_FramesConstrainNode( Aig_Man_t * pManFraig, Aig_Obj_t * p
 Aig_Man_t * Fra_FramesWithClasses( Fra_Man_t * p )
 {
     Aig_Man_t * pManFraig;
-    Aig_Obj_t * pObj, * pObjNew;
-    Aig_Obj_t ** pLatches;
+    Aig_Obj_t * pObj, * pObjLi, * pObjLo, * pObjNew;
     int i, k, f;
     assert( p->pManFraig == NULL );
     assert( Aig_ManRegNum(p->pManAig) > 0 );
@@ -149,7 +146,6 @@ Aig_Man_t * Fra_FramesWithClasses( Fra_Man_t * p )
         Fra_ObjSetFraig( pObj, 0, Aig_ObjCreatePi(pManFraig) );
 
     // add timeframes
-    pLatches = ALLOC( Aig_Obj_t *, Aig_ManRegNum(p->pManAig) );
     for ( f = 0; f < p->nFramesAll - 1; f++ )
     {
         // set the constraints on the latch outputs
@@ -162,23 +158,15 @@ Aig_Man_t * Fra_FramesWithClasses( Fra_Man_t * p )
             Fra_ObjSetFraig( pObj, f, pObjNew );
             Fra_FramesConstrainNode( pManFraig, pObj, f );
         }
-        // save the latch input values
-        k = 0;
-        Aig_ManForEachLiSeq( p->pManAig, pObj, i )
-            pLatches[k++] = Fra_ObjChild0Fra(pObj,f);
-        assert( k == Aig_ManRegNum(p->pManAig) );
-        // insert them to the latch output values
-        k = 0;
-        Aig_ManForEachLoSeq( p->pManAig, pObj, i )
-            Fra_ObjSetFraig( pObj, f+1, pLatches[k++] );
-        assert( k == Aig_ManRegNum(p->pManAig) );
+        // transfer latch input to the latch outputs 
+        Aig_ManForEachLiLoSeq( p->pManAig, pObjLi, pObjLo, k )
+            Fra_ObjSetFraig( pObjLo, f+1, Fra_ObjChild0Fra(pObjLi,f) );
     }
-    free( pLatches );
     // mark the asserts
     pManFraig->nAsserts = Aig_ManPoNum(pManFraig);
-    // add the POs for the latch inputs
-    Aig_ManForEachLiSeq( p->pManAig, pObj, i )
-        Aig_ObjCreatePo( pManFraig, Fra_ObjChild0Fra(pObj,f-1) );
+    // add the POs for the latch outputs of the last frame
+    Aig_ManForEachLoSeq( p->pManAig, pObj, i )
+        Aig_ObjCreatePo( pManFraig, Fra_ObjFraig(pObj,p->nFramesAll-1) );
 
     // remove dangling nodes
     Aig_ManCleanup( pManFraig );
@@ -198,7 +186,7 @@ Aig_Man_t * Fra_FramesWithClasses( Fra_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesP, int nFramesK, int fRewrite, int fUseImps, int fLatchCorr, int fVerbose, int * pnIter )
+Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesP, int nFramesK, int nMaxImps, int fRewrite, int fUseImps, int fLatchCorr, int fVerbose, int * pnIter )
 {
     int fUseSimpleCnf = 0;
     int fUseOldSimulation = 0;
@@ -229,6 +217,7 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesP, int nFramesK,
     Fra_ParamsDefaultSeq( pPars );
     pPars->nFramesP   = nFramesP;
     pPars->nFramesK   = nFramesK;
+    pPars->nMaxImps   = nMaxImps;
     pPars->fVerbose   = fVerbose;
     pPars->fRewrite   = fRewrite;
     pPars->fLatchCorr = fLatchCorr;
@@ -249,9 +238,16 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesP, int nFramesK,
     }
     else
     {
+        // bug:  r iscas/blif/s5378.blif    ; st; ssw -v
         // bug:  r iscas/blif/s1238.blif    ; st; ssw -v
         // refine the classes with more simulation rounds
-        p->pSml = Fra_SmlSimulateSeq( pManAig, pPars->nFramesP, 32, 2 ); //pPars->nFramesK + 1, 6 );  // 32, 2 );
+if ( fVerbose )
+printf( "Simulating %d AIG nodes for %d cycles ... ", Aig_ManNodeNum(pManAig), pPars->nFramesP + 32 );
+        p->pSml = Fra_SmlSimulateSeq( pManAig, pPars->nFramesP, 32, 1 ); //pPars->nFramesK + 1, 1 );  
+if ( fVerbose ) 
+{
+PRT( "Time", clock() - clk );
+}
         Fra_ClassesPrepare( p->pCla, p->pPars->fLatchCorr );
 //        Fra_ClassesPostprocess( p->pCla );
         // allocate new simulation manager for simulating counter-examples
@@ -259,19 +255,26 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesP, int nFramesK,
         p->pSml = Fra_SmlStart( pManAig, 0, pPars->nFramesK + 1, pPars->nSimWords );
     }
 
-    // perform BMC
-    Fra_BmcPerform( p, pPars->nFramesP, pPars->nFramesK + 1 );
+    // perform BMC (for the min number of frames)
+    Fra_BmcPerform( p, pPars->nFramesP, pPars->nFramesK );
 //Fra_ClassesPrint( p->pCla, 1 );
+//    p->vCex = Vec_IntAlloc( 1000 );
 
     // select the most expressive implications
     if ( pPars->fUseImps )
-        p->pCla->vImps = Fra_ImpDerive( p, 5000000, 5000, pPars->fLatchCorr );
+        p->pCla->vImps = Fra_ImpDerive( p, 5000000, pPars->nMaxImps, pPars->fLatchCorr );
  
     p->nLitsZero = Vec_PtrSize( p->pCla->vClasses1 );
     p->nLitsBeg  = Fra_ClassesCountLits( p->pCla );
     p->nNodesBeg = Aig_ManNodeNum(pManAig);
     p->nRegsBeg  = Aig_ManRegNum(pManAig);
 
+    // dump AIG of the timeframes
+//    pManAigNew = Fra_ClassesDeriveAig( p->pCla, pPars->nFramesK );
+//    Aig_ManDumpBlif( pManAigNew, "frame_aig.blif" );
+//    Fra_ManPartitionTest2( pManAigNew );
+//    Aig_ManStop( pManAigNew );
+
     // iterate the inductive case
     p->pCla->fRefinement = 1;
     for ( nIter = 0; p->pCla->fRefinement; nIter++ )
@@ -341,7 +344,11 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesP, int nFramesK,
 
         // cleanup
         Fra_ManClean( p );
+//        if ( nIter == 3 )
+//            break;
     }
+//    Fra_ClassesPrint( p->pCla, 1 );
+//    Fra_ClassesSelectRepr( p->pCla );
     // move the classes into representatives and reduce AIG
 clk2 = clock();
     Fra_ClassesCopyReprs( p->pCla, p->vTimeouts );
diff --git a/src/aig/fra/fraMan.c b/src/aig/fra/fraMan.c
index 2b8e0a68..0116bbc4 100644
--- a/src/aig/fra/fraMan.c
+++ b/src/aig/fra/fraMan.c
@@ -248,6 +248,7 @@ void Fra_ManStop( Fra_Man_t * p )
     if ( p->pSat )      sat_solver_delete( p->pSat );
     if ( p->pCla  )     Fra_ClassesStop( p->pCla );
     if ( p->pSml )      Fra_SmlStop( p->pSml );
+    if ( p->vCex )      Vec_IntFree( p->vCex );
     FREE( p->pMemFraig );
     FREE( p->pMemFanins );
     FREE( p->pMemSatNums );
diff --git a/src/aig/fra/fraPart.c b/src/aig/fra/fraPart.c
index d3fdbcfd..6e593694 100644
--- a/src/aig/fra/fraPart.c
+++ b/src/aig/fra/fraPart.c
@@ -170,6 +170,92 @@ PRT( "Scanning", clock() - clk );
 
 
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Fra_ManPartitionTest2( Aig_Man_t * p )
+{
+    Vec_Vec_t * vSupps, * vSuppsIn;
+    Vec_Int_t * vSup, * vSup2, * vSup3;
+    Aig_Obj_t * pObj;
+    int Entry, Entry2, Entry3, Counter;
+    int i, k, m, n, clk;
+    char * pSupp;
+ 
+    // compute supports
+clk = clock();
+    vSupps = Aig_ManSupports( p );
+PRT( "Supports", clock() - clk );
+    // remove last entry
+    Aig_ManForEachPo( p, pObj, i )
+    {
+        vSup = Vec_VecEntry( vSupps, i );
+        Vec_IntPop( vSup );
+        // remember support
+//        pObj->pNext = (Aig_Obj_t *)vSup;
+    }
+
+    // create reverse supports
+clk = clock();
+    vSuppsIn = Vec_VecStart( Aig_ManPiNum(p) );
+    Aig_ManForEachPo( p, pObj, i )
+    {
+        if ( i == p->nAsserts )
+            break;
+        vSup = Vec_VecEntry( vSupps, i );
+        Vec_IntForEachEntry( vSup, Entry, k )
+            Vec_VecPush( vSuppsIn, Entry, (void *)i );
+    }
+PRT( "Inverse ", clock() - clk );
+
+    // create affective supports
+clk = clock();
+    pSupp = ALLOC( char, Aig_ManPiNum(p) );
+    Aig_ManForEachPo( p, pObj, i )
+    {
+        if ( i % 50 != 0 )
+            continue;
+        vSup = Vec_VecEntry( vSupps, i );
+        memset( pSupp, 0, sizeof(char) * Aig_ManPiNum(p) );
+        // go through each input of this output
+        Vec_IntForEachEntry( vSup, Entry, k )
+        {
+            pSupp[Entry] = 1;
+            vSup2 = Vec_VecEntry( vSuppsIn, Entry );
+            // go though each assert of this input
+            Vec_IntForEachEntry( vSup2, Entry2, m )
+            {
+                vSup3 = Vec_VecEntry( vSupps, Entry2 );
+                // go through each input of this assert
+                Vec_IntForEachEntry( vSup3, Entry3, n )
+                {
+                    pSupp[Entry3] = 1;
+                }
+            }
+        }
+        // count the entries
+        Counter = 0;
+        for ( m = 0; m < Aig_ManPiNum(p); m++ )
+            Counter += pSupp[m];
+        printf( "%d(%d) ", Vec_IntSize(vSup), Counter );
+    }
+    printf( "\n" );
+PRT( "Extension ", clock() - clk );
+
+    free( pSupp );
+    Vec_VecFree( vSupps );
+    Vec_VecFree( vSuppsIn );
+}
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/fra/fraSec.c b/src/aig/fra/fraSec.c
index 2a0d06b5..8b9258cb 100644
--- a/src/aig/fra/fraSec.c
+++ b/src/aig/fra/fraSec.c
@@ -43,11 +43,12 @@ int Fra_FraigSec( Aig_Man_t * p, int nFramesFix, int fVerbose, int fVeryVerbose
 {
     Aig_Man_t * pNew;
     int nFrames, RetValue, nIter, clk, clkTotal = clock();
+    int fLatchCorr = 0;
     if ( nFramesFix )
     {
         nFrames = nFramesFix;
         // perform seq sweeping for one frame number
-        pNew = Fra_FraigInduction( p, 0, nFrames, 0, 0, 0, fVeryVerbose, &nIter );
+        pNew = Fra_FraigInduction( p, 0, nFrames, 0, 0, 0, fLatchCorr, fVeryVerbose, &nIter );
     }
     else
     {
@@ -55,7 +56,7 @@ int Fra_FraigSec( Aig_Man_t * p, int nFramesFix, int fVerbose, int fVeryVerbose
         for ( nFrames = 1; ; nFrames++ )
         {
 clk = clock();
-            pNew = Fra_FraigInduction( p, 0, nFrames, 0, 0, 0, fVeryVerbose, &nIter );
+            pNew = Fra_FraigInduction( p, 0, nFrames, 0, 0, 0, fLatchCorr, fVeryVerbose, &nIter );
             RetValue = Fra_FraigMiterStatus( pNew );
             if ( fVerbose )
             {
diff --git a/src/aig/fra/fraSim.c b/src/aig/fra/fraSim.c
index b31fcb7f..3463ee0d 100644
--- a/src/aig/fra/fraSim.c
+++ b/src/aig/fra/fraSim.c
@@ -200,6 +200,17 @@ void Fra_SmlSavePattern( Fra_Man_t * p )
         if ( p->pSat->model.ptr[Fra_ObjSatNum(pObj)] == l_True )
             Aig_InfoSetBit( p->pPatWords, i );
 /*
+    if ( p->vCex )
+    {
+        Vec_IntClear( p->vCex );
+        for ( i = 0; i < Aig_ManPiNum(p->pManAig) - Aig_ManRegNum(p->pManAig); i++ )
+            Vec_IntPush( p->vCex, Aig_InfoHasBit( p->pPatWords, i ) );
+        for ( i = Aig_ManPiNum(p->pManFraig) - Aig_ManRegNum(p->pManFraig); i < Aig_ManPiNum(p->pManFraig); i++ )
+            Vec_IntPush( p->vCex, Aig_InfoHasBit( p->pPatWords, i ) );
+    }
+*/
+
+/*
     printf( "Pattern: " );
     Aig_ManForEachPi( p->pManFraig, pObj, i )
         printf( "%d", Aig_InfoHasBit( p->pPatWords, i ) );
@@ -601,7 +612,7 @@ clk = clock();
     if ( p->pCla->vImps )
         nChanges += Fra_ImpRefineUsingCex( p, p->pCla->vImps );
 p->timeRef += clock() - clk;
-    if ( nChanges < 1 )
+    if ( !p->pPars->nFramesK && nChanges < 1 )
         printf( "Error: A counter-example did not refine classes!\n" );
 //    assert( nChanges >= 1 );
 //printf( "Refined classes = %5d.   Changes = %4d.\n", Vec_PtrSize(p->vClasses), nChanges );