Version abc90804

committer: Baruch Sterin <baruchs@gmail.com>

10 files changed, 237 insertions, 73 deletions

diff --git a/src/aig/cec/cec.h b/src/aig/cec/cec.h
index fcadb6ab..7f445970 100644
--- a/src/aig/cec/cec.h
+++ b/src/aig/cec/cec.h
@@ -47,21 +47,23 @@ struct Cec_ParSat_t_
     int              fNonChrono;    // use non-chronological backtracling (for circuit SAT only)
     int              fPolarFlip;    // flops polarity of variables
     int              fCheckMiter;   // the circuit is the miter
-    int              fFirstStop;    // stop on the first sat output
+//    int              fFirstStop;    // stop on the first sat output
     int              fLearnCls;     // perform clause learning
     int              fVerbose;      // verbose stats
 };
 
 // simulation parameters
 typedef struct Cec_ParSim_t_ Cec_ParSim_t;
-struct Cec_ParSim_t_
+struct Cec_ParSim_t_ 
 {
     int              nWords;        // the number of simulation words
+    int              nFrames;       // the number of simulation frames
     int              nRounds;       // the number of simulation rounds
+    int              nNonRefines;   // the max number of rounds without refinement
     int              TimeLimit;     // the runtime limit in seconds
     int              fDualOut;      // miter with separate outputs
     int              fCheckMiter;   // the circuit is the miter
-    int              fFirstStop;    // stop on the first sat output
+//    int              fFirstStop;    // stop on the first sat output
     int              fSeqSimulate;  // performs sequential simulation
     int              fLatchCorr;    // consider only latch outputs
     int              fVeryVerbose;  // verbose stats
@@ -74,12 +76,14 @@ struct Cec_ParSmf_t_
 {
     int              nWords;        // the number of simulation words
     int              nRounds;       // the number of simulation rounds
-    int              nFrames;       // the number of time frames
+    int              nFrames;       // the max number of time frames
+    int              nNonRefines;   // the max number of rounds without refinement
+    int              nMinOutputs;   // the min outputs to accumulate
     int              nBTLimit;      // conflict limit at a node
     int              TimeLimit;     // the runtime limit in seconds
     int              fDualOut;      // miter with separate outputs
     int              fCheckMiter;   // the circuit is the miter
-    int              fFirstStop;    // stop on the first sat output
+//    int              fFirstStop;    // stop on the first sat output
     int              fVerbose;      // verbose stats
 };
 
@@ -96,7 +100,7 @@ struct Cec_ParFra_t_
     int              nDepthMax;     // the depth in terms of steps of speculative reduction
     int              fRewriting;    // enables AIG rewriting
     int              fCheckMiter;   // the circuit is the miter
-    int              fFirstStop;    // stop on the first sat output
+//    int              fFirstStop;    // stop on the first sat output
     int              fDualOut;      // miter with separate outputs
     int              fColorDiff;    // miter with separate outputs
     int              fVeryVerbose;  // verbose stats
@@ -109,7 +113,7 @@ struct Cec_ParCec_t_
 {
     int              nBTLimit;      // conflict limit at a node
     int              TimeLimit;     // the runtime limit in seconds
-    int              fFirstStop;    // stop on the first sat output
+//    int              fFirstStop;    // stop on the first sat output
     int              fUseSmartCnf;  // use smart CNF computation
     int              fRewriting;    // enables AIG rewriting
     int              fVeryVerbose;  // verbose stats
@@ -129,7 +133,7 @@ struct Cec_ParCor_t_
     int              fUseRings;     // use rings
     int              fMakeChoices;  // use equilvaences as choices
     int              fUseCSat;      // use circuit-based solver
-    int              fFirstStop;    // stop on the first sat output
+//    int              fFirstStop;    // stop on the first sat output
     int              fUseSmartCnf;  // use smart CNF computation
     int              fVeryVerbose;  // verbose stats
     int              fVerbose;      // verbose stats
diff --git a/src/aig/cec/cecCec.c b/src/aig/cec/cecCec.c
index a385be3e..1efa9235 100644
--- a/src/aig/cec/cecCec.c
+++ b/src/aig/cec/cecCec.c
@@ -135,7 +135,6 @@ int Cec_ManVerify( Gia_Man_t * p, Cec_ParCec_t * pPars )
     pParsFra->TimeLimit    = pPars->TimeLimit;
     pParsFra->fVerbose     = pPars->fVerbose;
     pParsFra->fCheckMiter  = 1;
-    pParsFra->fFirstStop   = 1;
     pParsFra->fDualOut     = 1;
     pNew = Cec_ManSatSweeping( p, pParsFra );
     if ( pNew == NULL )
diff --git a/src/aig/cec/cecChoice.c b/src/aig/cec/cecChoice.c
index f51d138d..fc316f46 100644
--- a/src/aig/cec/cecChoice.c
+++ b/src/aig/cec/cecChoice.c
@@ -213,7 +213,7 @@ int Cec_ManChoiceComputation_int( Gia_Man_t * pAig, Cec_ParChc_t * pPars )
     // prepare simulation manager
     Cec_ManSimSetDefaultParams( pParsSim );
     pParsSim->nWords     = pPars->nWords;
-    pParsSim->nRounds    = pPars->nRounds;
+    pParsSim->nFrames    = pPars->nRounds;
     pParsSim->fVerbose   = pPars->fVerbose;
     pParsSim->fLatchCorr   = 0;
     pParsSim->fSeqSimulate = 0;
diff --git a/src/aig/cec/cecClass.c b/src/aig/cec/cecClass.c
index fd723f30..749f7f71 100644
--- a/src/aig/cec/cecClass.c
+++ b/src/aig/cec/cecClass.c
@@ -545,7 +545,7 @@ void Cec_ManSimSavePattern( Cec_ManSim_t * p, int iPat )
 void Cec_ManSimFindBestPattern( Cec_ManSim_t * p )
 { 
     unsigned * pInfo;
-    int i, ScoreBest = 0, iPatBest = 1;
+    int i, ScoreBest = 0, iPatBest = 1; // set the first pattern
     // find the best pattern
     for ( i = 0; i < 32 * p->nWords; i++ )
         if ( ScoreBest < p->pScores[i] )
@@ -588,8 +588,8 @@ int Cec_ManSimAnalyzeOutputs( Cec_ManSim_t * p )
     // compare outputs with 0
     if ( p->pPars->fDualOut )
     {
-        assert( (Gia_ManCoNum(p->pAig) & 1) == 0 );
-        for ( i = 0; i < Gia_ManCoNum(p->pAig); i++ )
+        assert( (Gia_ManPoNum(p->pAig) & 1) == 0 );
+        for ( i = 0; i < Gia_ManPoNum(p->pAig); i++ )
         {
             pInfo  = Vec_PtrEntry( p->vCoSimInfo, i );
             pInfo2 = Vec_PtrEntry( p->vCoSimInfo, ++i );
@@ -601,7 +601,7 @@ int Cec_ManSimAnalyzeOutputs( Cec_ManSim_t * p )
                     Cec_ManSimSavePattern( p, Cec_ManSimCompareEqualFirstBit(pInfo, pInfo2, p->nWords) );
                 }
                 if ( p->pCexes == NULL )
-                    p->pCexes = ABC_CALLOC( void *, Gia_ManCoNum(p->pAig)/2 );
+                    p->pCexes = ABC_CALLOC( void *, Gia_ManPoNum(p->pAig)/2 );
                 if ( p->pCexes[i/2] == NULL )
                 {
                     p->nOuts++;
@@ -612,7 +612,7 @@ int Cec_ManSimAnalyzeOutputs( Cec_ManSim_t * p )
     }
     else
     {
-        for ( i = 0; i < Gia_ManCoNum(p->pAig); i++ )
+        for ( i = 0; i < Gia_ManPoNum(p->pAig); i++ )
         {
             pInfo = Vec_PtrEntry( p->vCoSimInfo, i );
             if ( !Cec_ManSimCompareConst( pInfo, p->nWords ) )
@@ -623,7 +623,7 @@ int Cec_ManSimAnalyzeOutputs( Cec_ManSim_t * p )
                     Cec_ManSimSavePattern( p, Cec_ManSimCompareConstFirstBit(pInfo, p->nWords) );
                 }
                 if ( p->pCexes == NULL )
-                    p->pCexes = ABC_CALLOC( void *, Gia_ManCoNum(p->pAig) );
+                    p->pCexes = ABC_CALLOC( void *, Gia_ManPoNum(p->pAig) );
                 if ( p->pCexes[i] == NULL )
                 {
                     p->nOuts++;
@@ -632,7 +632,7 @@ int Cec_ManSimAnalyzeOutputs( Cec_ManSim_t * p )
             }
         }
     }
-    return p->pCexes != NULL && p->pPars->fFirstStop;
+    return p->pCexes != NULL;
 }
 
 /**Function*************************************************************
diff --git a/src/aig/cec/cecCore.c b/src/aig/cec/cecCore.c
index 9820c05c..10c145ec 100644
--- a/src/aig/cec/cecCore.c
+++ b/src/aig/cec/cecCore.c
@@ -48,7 +48,7 @@ void Cec_ManSatSetDefaultParams( Cec_ParSat_t * p )
     p->fNonChrono     =       0;  // use non-chronological backtracling (for circuit SAT only)
     p->fPolarFlip     =       1;  // flops polarity of variables
     p->fCheckMiter    =       0;  // the circuit is the miter
-    p->fFirstStop     =       0;  // stop on the first sat output
+//    p->fFirstStop     =       0;  // stop on the first sat output
     p->fLearnCls      =       0;  // perform clause learning
     p->fVerbose       =       0;  // verbose stats
 }  
@@ -67,11 +67,13 @@ void Cec_ManSatSetDefaultParams( Cec_ParSat_t * p )
 void Cec_ManSimSetDefaultParams( Cec_ParSim_t * p )
 {
     memset( p, 0, sizeof(Cec_ParSim_t) );
-    p->nWords         =      15;  // the number of simulation words
-    p->nRounds        =      15;  // the number of simulation rounds
+    p->nWords         =      31;  // the number of simulation words
+    p->nFrames        =     100;  // the number of simulation frames
+    p->nRounds        =      20;  // the max number of simulation rounds
+    p->nNonRefines    =       3;  // the max number of rounds without refinement
     p->TimeLimit      =       0;  // the runtime limit in seconds
     p->fCheckMiter    =       0;  // the circuit is the miter
-    p->fFirstStop     =       0;  // stop on the first sat output
+//    p->fFirstStop     =       0;  // stop on the first sat output
     p->fDualOut       =       0;  // miter with separate outputs
     p->fSeqSimulate   =       0;  // performs sequential simulation
     p->fVeryVerbose   =       0;  // verbose stats
@@ -93,13 +95,15 @@ void Cec_ManSmfSetDefaultParams( Cec_ParSmf_t * p )
 {
     memset( p, 0, sizeof(Cec_ParSmf_t) );
     p->nWords         =      31;  // the number of simulation words
-    p->nRounds        =       1;  // the number of simulation rounds
-    p->nFrames        =       2;  // the number of time frames
+    p->nRounds        =     200;  // the number of simulation rounds
+    p->nFrames        =     200;  // the max number of time frames
+    p->nNonRefines    =       3;  // the max number of rounds without refinement
+    p->nMinOutputs    =       0;  // the min outputs to accumulate
     p->nBTLimit       =     100;  // conflict limit at a node
     p->TimeLimit      =       0;  // the runtime limit in seconds
     p->fDualOut       =       0;  // miter with separate outputs
     p->fCheckMiter    =       0;  // the circuit is the miter
-    p->fFirstStop     =       0;  // stop on the first sat output
+//    p->fFirstStop     =       0;  // stop on the first sat output
     p->fVerbose       =       0;  // verbose stats
 } 
 
@@ -126,7 +130,7 @@ void Cec_ManFraSetDefaultParams( Cec_ParFra_t * p )
     p->nDepthMax      =       1;  // the depth in terms of steps of speculative reduction
     p->fRewriting     =       0;  // enables AIG rewriting
     p->fCheckMiter    =       0;  // the circuit is the miter
-    p->fFirstStop     =       0;  // stop on the first sat output
+//    p->fFirstStop     =       0;  // stop on the first sat output
     p->fDualOut       =       0;  // miter with separate outputs
     p->fColorDiff     =       0;  // miter with separate outputs
     p->fVeryVerbose   =       0;  // verbose stats
@@ -149,7 +153,7 @@ void Cec_ManCecSetDefaultParams( Cec_ParCec_t * p )
     memset( p, 0, sizeof(Cec_ParCec_t) );
     p->nBTLimit       =    1000;  // conflict limit at a node
     p->TimeLimit      =       0;  // the runtime limit in seconds
-    p->fFirstStop     =       0;  // stop on the first sat output
+//    p->fFirstStop     =       0;  // stop on the first sat output
     p->fUseSmartCnf   =       0;  // use smart CNF computation
     p->fRewriting     =       0;  // enables AIG rewriting
     p->fVeryVerbose   =       0;  // verbose stats
@@ -177,7 +181,7 @@ void Cec_ManCorSetDefaultParams( Cec_ParCor_t * p )
     p->fLatchCorr     =       0;  // consider only latch outputs
     p->fUseRings      =       1;  // combine classes into rings
     p->fUseCSat       =       1;  // use circuit-based solver
-    p->fFirstStop     =       0;  // stop on the first sat output
+//    p->fFirstStop     =       0;  // stop on the first sat output
     p->fUseSmartCnf   =       0;  // use smart CNF computation
     p->fVeryVerbose   =       0;  // verbose stats
     p->fVerbose       =       0;  // verbose stats
@@ -233,31 +237,79 @@ Gia_Man_t * Cec_ManSatSolving( Gia_Man_t * pAig, Cec_ParSat_t * pPars )
 
   Synopsis    [Core procedure for simulation.]
 
-  Description []
+  Description [Returns 1 if refinement has happened.]
                
   SideEffects []
 
   SeeAlso     []
 
 ***********************************************************************/
-void Cec_ManSimulation( Gia_Man_t * pAig, Cec_ParSim_t * pPars )
+int Cec_ManSimulationOne( Gia_Man_t * pAig, Cec_ParSim_t * pPars )
 {
     Cec_ManSim_t * pSim;
-    int RetValue, clkTotal = clock();
-    if ( pPars->fSeqSimulate )
-        printf( "Performing sequential simulation of %d frames with %d words.\n", 
-            pPars->nRounds, pPars->nWords );
-    Gia_ManRandom( 1 );
+    int RetValue = 0, clkTotal = clock();
     pSim = Cec_ManSimStart( pAig, pPars );
-    if ( pAig->pReprs == NULL )
-        RetValue = Cec_ManSimClassesPrepare( pSim );
-    Cec_ManSimClassesRefine( pSim );
-    if ( pPars->fCheckMiter )
-        printf( "The number of failed outputs of the miter = %6d. (Words = %4d. Rounds = %4d.)\n", 
-            pSim->iOut, pSim->nOuts, pPars->nWords, pPars->nRounds );
+    if ( (pAig->pReprs == NULL && (RetValue = Cec_ManSimClassesPrepare( pSim ))) ||
+         (RetValue == 0 &&        (RetValue = Cec_ManSimClassesRefine( pSim ))) )
+        printf( "The number of failed outputs of the miter = %6d. (Words = %4d. Frames = %4d.)\n", 
+            pSim->nOuts, pPars->nWords, pPars->nFrames );
     if ( pPars->fVerbose )
         ABC_PRT( "Time", clock() - clkTotal );
     Cec_ManSimStop( pSim );
+    return RetValue;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Core procedure for simulation.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cec_ManSimulation( Gia_Man_t * pAig, Cec_ParSim_t * pPars )
+{
+    int r, nLitsOld, nLitsNew, nCountNoRef = 0, fStop = 0;
+    Gia_ManRandom( 1 );
+    if ( pPars->fSeqSimulate )
+        printf( "Performing rounds of random simulation of %d frames with %d words.\n", 
+            pPars->nRounds, pPars->nFrames, pPars->nWords );
+    nLitsOld = Gia_ManEquivCountLits( pAig );
+    for ( r = 0; r < pPars->nRounds; r++ )
+    {
+        if ( Cec_ManSimulationOne( pAig, pPars ) )
+        {
+            fStop = 1;
+            break;
+        }
+        // decide when to stop
+        nLitsNew = Gia_ManEquivCountLits( pAig );
+        if ( nLitsOld == 0 || nLitsOld > nLitsNew )
+        {
+            nLitsOld = nLitsNew;
+            nCountNoRef = 0;
+        }
+        else if ( ++nCountNoRef == pPars->nNonRefines )
+        {
+            r++;
+            break;
+        }
+        assert( nLitsOld == nLitsNew );
+    }
+//    if ( pPars->fVerbose )
+    if ( r == pPars->nRounds || fStop )
+        printf( "Random simulation is stopped after %d rounds.\n", r );
+    else
+        printf( "Random simulation saturated after %d rounds.\n", r );
+    if ( pPars->fCheckMiter )
+    {
+        int nNonConsts = Cec_ManCountNonConstOutputs( pAig );
+        if ( nNonConsts )
+            printf( "The number of POs that are not const-0 candidates = %d.\n", nNonConsts );
+    }
 }
 
 /**Function*************************************************************
@@ -297,9 +349,8 @@ Gia_Man_t * Cec_ManSatSweeping( Gia_Man_t * pAig, Cec_ParFra_t * pPars )
     // simulation
     Cec_ManSimSetDefaultParams( pParsSim );
     pParsSim->nWords      = pPars->nWords;
-    pParsSim->nRounds     = pPars->nRounds;
+    pParsSim->nFrames     = pPars->nRounds;
     pParsSim->fCheckMiter = pPars->fCheckMiter;
-    pParsSim->fFirstStop  = pPars->fFirstStop;
     pParsSim->fDualOut = pPars->fDualOut;
     pParsSim->fVerbose    = pPars->fVerbose;
     pSim = Cec_ManSimStart( p->pAig, pParsSim );
diff --git a/src/aig/cec/cecCorr.c b/src/aig/cec/cecCorr.c
index 96af801d..96c45907 100644
--- a/src/aig/cec/cecCorr.c
+++ b/src/aig/cec/cecCorr.c
@@ -545,7 +545,7 @@ int Cec_ManResimulateCounterExamples( Cec_ManSim_t * pSim, Vec_Int_t * vCexStore
     vPairs = Gia_ManCorrCreateRemapping( pSim->pAig );
     Gia_ManSetRefs( pSim->pAig );
 //    pSim->pPars->nWords  = 63;
-    pSim->pPars->nRounds = nFrames;
+    pSim->pPars->nFrames = nFrames;
     vSimInfo = Vec_PtrAllocSimInfo( Gia_ManRegNum(pSim->pAig) + Gia_ManPiNum(pSim->pAig) * nFrames, pSim->pPars->nWords );
     while ( iStart < Vec_IntSize(vCexStore) )
     {
@@ -580,7 +580,7 @@ int Cec_ManResimulateCounterExamplesComb( Cec_ManSim_t * pSim, Vec_Int_t * vCexS
     Vec_Ptr_t * vSimInfo; 
     int RetValue = 0, iStart = 0;
     Gia_ManSetRefs( pSim->pAig );
-    pSim->pPars->nRounds = 1;
+    pSim->pPars->nFrames = 1;
     vSimInfo = Vec_PtrAllocSimInfo( Gia_ManCiNum(pSim->pAig), pSim->pPars->nWords );
     while ( iStart < Vec_IntSize(vCexStore) )
     {
@@ -774,7 +774,7 @@ void Cec_ManLSCorrespondenceBmc( Gia_Man_t * pAig, Cec_ParCor_t * pPars, int nPr
     // prepare simulation manager
     Cec_ManSimSetDefaultParams( pParsSim );
     pParsSim->nWords     = pPars->nWords;
-    pParsSim->nRounds    = pPars->nRounds;
+    pParsSim->nFrames    = pPars->nRounds;
     pParsSim->fVerbose   = pPars->fVerbose;
     pParsSim->fLatchCorr = pPars->fLatchCorr;
     pParsSim->fSeqSimulate = 1;
@@ -853,7 +853,7 @@ int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
     // prepare simulation manager
     Cec_ManSimSetDefaultParams( pParsSim );
     pParsSim->nWords     = pPars->nWords;
-    pParsSim->nRounds    = pPars->nRounds;
+    pParsSim->nFrames    = pPars->nFrames;
     pParsSim->fVerbose   = pPars->fVerbose;
     pParsSim->fLatchCorr = pPars->fLatchCorr;
     pParsSim->fSeqSimulate = 1;
diff --git a/src/aig/cec/cecInt.h b/src/aig/cec/cecInt.h
index 9c012f73..73f108ba 100644
--- a/src/aig/cec/cecInt.h
+++ b/src/aig/cec/cecInt.h
@@ -192,8 +192,10 @@ extern Vec_Ptr_t *          Cec_ManPatCollectPatterns( Cec_ManPat_t *  pMan, int
 extern Vec_Ptr_t *          Cec_ManPatPackPatterns( Vec_Int_t * vCexStore, int nInputs, int nRegs, int nWordsInit );
 /*=== cecSeq.c ============================================================*/
 extern int                  Cec_ManSeqResimulate( Cec_ManSim_t * p, Vec_Ptr_t * vInfo );
-extern int                  Cec_ManSeqResimulateInfo( Gia_Man_t * pAig, Vec_Ptr_t * vSimInfo, Gia_Cex_t * pBestState );
+extern int                  Cec_ManSeqResimulateInfo( Gia_Man_t * pAig, Vec_Ptr_t * vSimInfo, Gia_Cex_t * pBestState, int fCheckMiter );
 extern void                 Cec_ManSeqDeriveInfoInitRandom( Vec_Ptr_t * vInfo, Gia_Man_t * pAig, Gia_Cex_t * pCex );
+extern int                  Cec_ManCountNonConstOutputs( Gia_Man_t * pAig );
+extern int                  Cec_ManCheckNonTrivialCands( Gia_Man_t * pAig );
 /*=== cecSolve.c ============================================================*/
 extern int                  Cec_ObjSatVarValue( Cec_ManSat_t * p, Gia_Obj_t * pObj );
 extern void                 Cec_ManSatSolve( Cec_ManPat_t * pPat, Gia_Man_t * pAig, Cec_ParSat_t * pPars );
diff --git a/src/aig/cec/cecMan.c b/src/aig/cec/cecMan.c
index de71ecc9..70396cca 100644
--- a/src/aig/cec/cecMan.c
+++ b/src/aig/cec/cecMan.c
@@ -76,13 +76,13 @@ void Cec_ManSatPrintStats( Cec_ManSat_t * p )
     printf( "MinVar = %5d  ", p->pPars->nSatVarMax );
     printf( "MinCalls = %5d\n", p->pPars->nCallsRecycle );
     printf( "Unsat calls %6d  (%6.2f %%)   Ave conf = %8.1f   ", 
-        p->nSatUnsat, 100.0*p->nSatUnsat/p->nSatTotal, p->nSatUnsat? 1.0*p->nConfUnsat/p->nSatUnsat :0.0 );
+        p->nSatUnsat, p->nSatTotal? 100.0*p->nSatUnsat/p->nSatTotal : 0.0, p->nSatUnsat? 1.0*p->nConfUnsat/p->nSatUnsat :0.0 );
     ABC_PRTP( "Time", p->timeSatUnsat, p->timeTotal );
     printf( "Sat   calls %6d  (%6.2f %%)   Ave conf = %8.1f   ", 
-        p->nSatSat,   100.0*p->nSatSat/p->nSatTotal, p->nSatSat? 1.0*p->nConfSat/p->nSatSat : 0.0 );
+        p->nSatSat,   p->nSatTotal? 100.0*p->nSatSat/p->nSatTotal : 0.0,   p->nSatSat? 1.0*p->nConfSat/p->nSatSat : 0.0 );
     ABC_PRTP( "Time", p->timeSatSat,   p->timeTotal );
     printf( "Undef calls %6d  (%6.2f %%)   Ave conf = %8.1f   ", 
-        p->nSatUndec, 100.0*p->nSatUndec/p->nSatTotal, p->nSatUndec? 1.0*p->nConfUndec/p->nSatUndec : 0.0 );
+        p->nSatUndec, p->nSatTotal? 100.0*p->nSatUndec/p->nSatTotal : 0.0, p->nSatUndec? 1.0*p->nConfUndec/p->nSatUndec : 0.0 );
     ABC_PRTP( "Time", p->timeSatUndec, p->timeTotal );
     ABC_PRT( "Total time", p->timeTotal );
 }
diff --git a/src/aig/cec/cecSeq.c b/src/aig/cec/cecSeq.c
index b19950b3..49f2a018 100644
--- a/src/aig/cec/cecSeq.c
+++ b/src/aig/cec/cecSeq.c
@@ -125,9 +125,9 @@ void Cec_ManSeqDeriveInfoInitRandom( Vec_Ptr_t * vInfo, Gia_Man_t * pAig, Gia_Ce
 int Cec_ManSeqResimulate( Cec_ManSim_t * p, Vec_Ptr_t * vInfo )
 {
     unsigned * pInfo0, * pInfo1;
-    int f, i, k, w, RetValue = 0;
+    int f, i, k, w;
 //    assert( Gia_ManRegNum(p->pAig) > 0 );
-    assert( Vec_PtrSize(vInfo) == Gia_ManRegNum(p->pAig) + Gia_ManPiNum(p->pAig) * p->pPars->nRounds );
+    assert( Vec_PtrSize(vInfo) == Gia_ManRegNum(p->pAig) + Gia_ManPiNum(p->pAig) * p->pPars->nFrames );
     for ( k = 0; k < Gia_ManRegNum(p->pAig); k++ )
     {
         pInfo0 = Vec_PtrEntry( vInfo, k );
@@ -135,7 +135,7 @@ int Cec_ManSeqResimulate( Cec_ManSim_t * p, Vec_Ptr_t * vInfo )
         for ( w = 0; w < p->nWords; w++ )
             pInfo1[w] = pInfo0[w];
     }
-    for ( f = 0; f < p->pPars->nRounds; f++ )
+    for ( f = 0; f < p->pPars->nFrames; f++ )
     {
         for ( i = 0; i < Gia_ManPiNum(p->pAig); i++ )
         {
@@ -152,13 +152,10 @@ int Cec_ManSeqResimulate( Cec_ManSim_t * p, Vec_Ptr_t * vInfo )
                 pInfo1[w] = pInfo0[w];
         }
         if ( Cec_ManSimSimulateRound( p, p->vCiSimInfo, p->vCoSimInfo ) )
-        {
-            printf( "One of the outputs of the miter is asserted.\n" );
-            RetValue = 1;
-        }
+            return 1;
     }
     assert( k == Vec_PtrSize(vInfo) );
-    return RetValue;
+    return 0;
 }
 
 /**Function*************************************************************
@@ -172,15 +169,16 @@ int Cec_ManSeqResimulate( Cec_ManSim_t * p, Vec_Ptr_t * vInfo )
   SeeAlso     []
 
 ***********************************************************************/
-int Cec_ManSeqResimulateInfo( Gia_Man_t * pAig, Vec_Ptr_t * vSimInfo, Gia_Cex_t * pBestState )
+int Cec_ManSeqResimulateInfo( Gia_Man_t * pAig, Vec_Ptr_t * vSimInfo, Gia_Cex_t * pBestState, int fCheckMiter )
 {
     Cec_ParSim_t ParsSim, * pParsSim = &ParsSim;
     Cec_ManSim_t * pSim;
     int RetValue, clkTotal = clock();
     assert( (Vec_PtrSize(vSimInfo) - Gia_ManRegNum(pAig)) % Gia_ManPiNum(pAig) == 0 );
     Cec_ManSimSetDefaultParams( pParsSim );
-    pParsSim->nRounds = (Vec_PtrSize(vSimInfo) - Gia_ManRegNum(pAig)) / Gia_ManPiNum(pAig);
+    pParsSim->nFrames = (Vec_PtrSize(vSimInfo) - Gia_ManRegNum(pAig)) / Gia_ManPiNum(pAig);
     pParsSim->nWords  = Vec_PtrReadWordsSimInfo( vSimInfo );
+    pParsSim->fCheckMiter = fCheckMiter;
     Gia_ManSetRefs( pAig );
     pSim = Cec_ManSimStart( pAig, pParsSim );
     if ( pBestState )
@@ -228,25 +226,83 @@ int Cec_ManSeqResimulateCounter( Gia_Man_t * pAig, Cec_ParSim_t * pPars, Gia_Cex
         return -1;
     }
     if ( pPars->fVerbose )
-        printf( "Resimulating %d timeframes.\n", pPars->nRounds + pCex->iFrame + 1 );
+        printf( "Resimulating %d timeframes.\n", pPars->nFrames + pCex->iFrame + 1 );
     Gia_ManRandom( 1 );
     vSimInfo = Vec_PtrAllocSimInfo( Gia_ManRegNum(pAig) + 
-        Gia_ManPiNum(pAig) * (pPars->nRounds + pCex->iFrame + 1), 1 );
+        Gia_ManPiNum(pAig) * (pPars->nFrames + pCex->iFrame + 1), 1 );
     Cec_ManSeqDeriveInfoFromCex( vSimInfo, pAig, pCex );
     if ( pPars->fVerbose )
         Gia_ManEquivPrintClasses( pAig, 0, 0 );
-    RetValue = Cec_ManSeqResimulateInfo( pAig, vSimInfo, NULL );
+    RetValue = Cec_ManSeqResimulateInfo( pAig, vSimInfo, NULL, pPars->fCheckMiter );
     if ( pPars->fVerbose )
         Gia_ManEquivPrintClasses( pAig, 0, 0 );
     Vec_PtrFree( vSimInfo );
     if ( pPars->fVerbose )
         ABC_PRT( "Time", clock() - clkTotal );
+    if ( RetValue )
+        printf( "Cec_ManSeqResimulateCounter(): An output of the miter is asserted!\n" );
     return RetValue;
 }
 
 
 /**Function*************************************************************
 
+  Synopsis    [Returns the number of POs that are not const0 cands.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Cec_ManCountNonConstOutputs( Gia_Man_t * pAig )
+{
+    Gia_Obj_t * pObj;
+    int i, Counter = 0;
+    if ( pAig->pReprs == NULL )
+        return -1;
+    Gia_ManForEachPo( pAig, pObj, i )
+        if ( !Gia_ObjIsConst( pAig, Gia_ObjFaninId0p(pAig, pObj) ) )
+            Counter++;
+    return Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the number of POs that are not const0 cands.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Cec_ManCheckNonTrivialCands( Gia_Man_t * pAig )
+{
+    Gia_Obj_t * pObj;
+    int i, RetValue = 0;
+    if ( pAig->pReprs == NULL )
+        return 0;
+    // label internal nodes driving POs
+    Gia_ManForEachPo( pAig, pObj, i )
+        Gia_ObjFanin0(pObj)->fMark0 = 1;
+    // check if there are non-labled equivs
+    Gia_ManForEachObj( pAig, pObj, i )
+        if ( Gia_ObjIsCand(pObj) && !pObj->fMark0 && Gia_ObjRepr(pAig, i) != GIA_VOID )
+        {
+            RetValue = 1;
+            break;
+        }
+    // clean internal nodes driving POs
+    Gia_ManForEachPo( pAig, pObj, i )
+        Gia_ObjFanin0(pObj)->fMark0 = 0;
+    return RetValue;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Performs semiformal refinement of equivalence classes.]
 
   Description []
@@ -258,13 +314,15 @@ int Cec_ManSeqResimulateCounter( Gia_Man_t * pAig, Cec_ParSim_t * pPars, Gia_Cex
 ***********************************************************************/
 int Cec_ManSeqSemiformal( Gia_Man_t * pAig, Cec_ParSmf_t * pPars )
 { 
-    int nAddFrames = 10; // additional timeframes to simulate
+    int nAddFrames = 16; // additional timeframes to simulate
+    int nCountNoRef = 0;
+    int nFramesReal;
     Cec_ParSat_t ParsSat, * pParsSat = &ParsSat;
     Vec_Ptr_t * vSimInfo; 
     Vec_Str_t * vStatus;
     Gia_Cex_t * pState;
-    Gia_Man_t * pSrm;
-    int r, nPats, RetValue = -1;
+    Gia_Man_t * pSrm, * pReduce, * pAux;
+    int r, nPats, RetValue = 0;
     if ( pAig->pReprs == NULL )
     { 
         printf( "Cec_ManSeqSemiformal(): Equivalence classes are not available.\n" );
@@ -290,22 +348,36 @@ int Cec_ManSeqSemiformal( Gia_Man_t * pAig, Cec_ParSmf_t * pPars )
         Gia_ManEquivPrintClasses( pAig, 0, 0 );
     }
     // perform the given number of BMC rounds
+    Gia_ManCleanMark0( pAig );
     for ( r = 0; r < pPars->nRounds; r++ )
     {
+        if ( !Cec_ManCheckNonTrivialCands(pAig) )
+        {
+            printf( "Cec_ManSeqSemiformal: There are only trivial equiv candidates left (PO drivers). Quitting.\n" );
+            break;
+        }
 //        Gia_ManPrintCounterExample( pState );
         // derive speculatively reduced model
-        pSrm = Gia_ManSpecReduceInit( pAig, pState, pPars->nFrames, pPars->fDualOut );
-        assert( Gia_ManRegNum(pSrm) == 0 && Gia_ManPiNum(pSrm) == (Gia_ManPiNum(pAig) * pPars->nFrames) );
+//        pSrm = Gia_ManSpecReduceInit( pAig, pState, pPars->nFrames, pPars->fDualOut );
+        pSrm = Gia_ManSpecReduceInitFrames( pAig, pState, pPars->nFrames, &nFramesReal, pPars->fDualOut, pPars->nMinOutputs );
+        if ( pSrm == NULL )
+        {
+            printf( "Quitting refinement because miter could not be unrolled.\n" );
+            break;
+        }
+        assert( Gia_ManRegNum(pSrm) == 0 && Gia_ManPiNum(pSrm) == (Gia_ManPiNum(pAig) * nFramesReal) );
+        if ( pPars->fVerbose )
+            printf( "Unrolled for %d frames.\n", nFramesReal );
         // allocate room for simulation info
         vSimInfo = Vec_PtrAllocSimInfo( Gia_ManRegNum(pAig) + 
-            Gia_ManPiNum(pAig) * (pPars->nFrames + nAddFrames), pPars->nWords );
+            Gia_ManPiNum(pAig) * (nFramesReal + nAddFrames), pPars->nWords );
         Cec_ManSeqDeriveInfoInitRandom( vSimInfo, pAig, pState );
         // fill in simulation info with counter-examples
         vStatus = Cec_ManSatSolveSeq( vSimInfo, pSrm, pParsSat, Gia_ManRegNum(pAig), &nPats );
         Vec_StrFree( vStatus );
         Gia_ManStop( pSrm );
         // resimulate and refine the classes
-        RetValue = Cec_ManSeqResimulateInfo( pAig, vSimInfo, pState );
+        RetValue = Cec_ManSeqResimulateInfo( pAig, vSimInfo, pState, pPars->fCheckMiter );
         Vec_PtrFree( vSimInfo );
         assert( pState->iPo >= 0 ); // hit counter
         pState->iPo = -1;
@@ -314,11 +386,47 @@ int Cec_ManSeqSemiformal( Gia_Man_t * pAig, Cec_ParSmf_t * pPars )
             printf( "BMC = %3d ", nPats );
             Gia_ManEquivPrintClasses( pAig, 0, 0 );
         }
+
+        // write equivalence classes
+        Gia_WriteAiger( pAig, "gore.aig", 0, 0 );
+        // reduce the model
+        pReduce = Gia_ManSpecReduce( pAig, 0, 0 );
+        if ( pReduce )
+        {
+            pReduce = Gia_ManSeqStructSweep( pAux = pReduce, 1, 1, 0 );
+            Gia_ManStop( pAux );
+            Gia_WriteAiger( pReduce, "gsrm.aig", 0, 0 );
+//            printf( "Speculatively reduced model was written into file \"%s\".\n", "gsrm.aig" );
+//          Gia_ManPrintStatsShort( pReduce );
+            Gia_ManStop( pReduce );
+        }
+
+        if ( RetValue )
+        {
+            printf( "Cec_ManSeqSemiformal(): An output of the miter is asserted. Refinement stopped.\n" );
+            break;
+        }
+        // decide when to stop
+        if ( nPats > 0 )
+            nCountNoRef = 0;
+        else if ( ++nCountNoRef == pPars->nNonRefines )
+            break;
     }
     ABC_FREE( pState );
+    if ( pPars->fCheckMiter )
+    {
+        int nNonConsts = Cec_ManCountNonConstOutputs( pAig );
+        if ( nNonConsts )
+            printf( "The number of POs that are not const-0 candidates = %d.\n", nNonConsts );
+    }
     return RetValue;
 }
 
+//&r s13207.aig; &ps; &equiv; &ps; &semi -R 2 -vm
+//&r bug/50/temp.aig; &ps; &equiv -smv; &semi -v
+//r mentor/1_05c.blif; st; &get; &ps; &equiv -smv; &semi -mv
+//&r bug/50/hdl1.aig; &ps; &equiv -smv; &semi -mv; &srm; &r gsrm.aig; &ps
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/cec/cecSolve.c b/src/aig/cec/cecSolve.c
index 1aaf54ff..fa10d222 100644
--- a/src/aig/cec/cecSolve.c
+++ b/src/aig/cec/cecSolve.c
@@ -718,7 +718,7 @@ clk2 = clock();
             pPat->timeTotalSave += clock() - clk3;
         }
         // quit if one of them is solved
-        if ( pPars->fFirstStop )
+        if ( pPars->fCheckMiter )
             break;
     }
     p->timeTotal = clock() - clk;
@@ -810,12 +810,12 @@ Vec_Str_t * Cec_ManSatSolveSeq( Vec_Ptr_t * vPatts, Gia_Man_t * pAig, Cec_ParSat
         {
             if ( Gia_ObjFaninC0(pObj) )
             {
-                printf( "Constant 1 output of SRM!!!\n" );
+//                printf( "Constant 1 output of SRM!!!\n" );
                 Vec_StrPush( vStatus, 0 );
             }
             else
             {
-                printf( "Constant 0 output of SRM!!!\n" );
+//                printf( "Constant 0 output of SRM!!!\n" );
                 Vec_StrPush( vStatus, 1 );
             }
             continue;