Version abc90313

5 files changed, 15 insertions, 10 deletions

diff --git a/src/aig/cec/cecCec.c b/src/aig/cec/cecCec.c
index 96bddbcb..f3d3dea9 100644
--- a/src/aig/cec/cecCec.c
+++ b/src/aig/cec/cecCec.c
@@ -129,6 +129,7 @@ int Cec_ManVerify( Gia_Man_t * p, Cec_ParCec_t * pPars )
     double clkTotal = clock();
     // sweep for equivalences
     Cec_ManFraSetDefaultParams( pParsFra );
+    pParsFra->nItersMax    = 1000;
     pParsFra->nBTLimit     = pPars->nBTLimit;
     pParsFra->TimeLimit    = pPars->TimeLimit;
     pParsFra->fVerbose     = pPars->fVerbose;
diff --git a/src/aig/cec/cecClass.c b/src/aig/cec/cecClass.c
index 0cac88af..26ff543a 100644
--- a/src/aig/cec/cecClass.c
+++ b/src/aig/cec/cecClass.c
@@ -242,6 +242,7 @@ void Cec_ManSimClassCreate( Gia_Man_t * p, Vec_Int_t * vClass )
         }
         else
         {
+            assert( Repr < Ent );
             Gia_ObjSetRepr( p, Ent, Repr );
             Gia_ObjSetNext( p, EntPrev, Ent );
             EntPrev = Ent;
@@ -500,7 +501,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;
     // find the best pattern
@@ -838,7 +839,7 @@ int Cec_ManSimClassesRefine( Cec_ManSim_t * p )
     p->nWords = p->pPars->nWords;
     for ( i = 0; i < p->pPars->nRounds; i++ )
     {
-        if ( (i % 4) == 0 && p->pPars->fVerbose )
+        if ( (i % (p->pPars->nRounds / 5)) == 0 && p->pPars->fVerbose )
             Gia_ManEquivPrintClasses( p->pAig, 0, Cec_MemUsage(p) );
         Cec_ManSimCreateInfo( p, p->vCiSimInfo, p->vCoSimInfo );
         if ( Cec_ManSimSimulateRound( p, p->vCiSimInfo, p->vCoSimInfo ) )
diff --git a/src/aig/cec/cecCore.c b/src/aig/cec/cecCore.c
index 061c3a7d..8e66179f 100644
--- a/src/aig/cec/cecCore.c
+++ b/src/aig/cec/cecCore.c
@@ -90,10 +90,10 @@ void Cec_ManSimSetDefaultParams( Cec_ParSim_t * p )
 void Cec_ManSmfSetDefaultParams( Cec_ParSmf_t * p )
 {
     memset( p, 0, sizeof(Cec_ParSmf_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->nRounds        =       1;  // the number of simulation rounds
     p->nFrames        =       2;  // the number of time frames
-    p->nBTLimit       =    1000;  // conflict limit at a node
+    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
@@ -118,8 +118,8 @@ void Cec_ManFraSetDefaultParams( Cec_ParFra_t * p )
     p->nWords         =      15;  // the number of simulation words
     p->nRounds        =      15;  // the number of simulation rounds
     p->TimeLimit      =       0;  // the runtime limit in seconds
-    p->nItersMax      =    1000;  // the maximum number of iterations of SAT sweeping
-    p->nBTLimit       =    1000;  // conflict limit at a node
+    p->nItersMax      =      10;  // the maximum number of iterations of SAT sweeping
+    p->nBTLimit       =     100;  // conflict limit at a node
     p->nLevelMax      =       0;  // restriction on the level of nodes to be swept
     p->nDepthMax      =       1;  // the depth in terms of steps of speculative reduction
     p->fRewriting     =       0;  // enables AIG rewriting
@@ -322,6 +322,8 @@ p->timeSat += clock() - clk;
         // update the manager
         pSim->pAig = p->pAig = Gia_ManEquivReduceAndRemap( pTemp = p->pAig, 0, pParsSim->fDualOut );
         Gia_ManStop( pTemp );
+        if ( p->pAig == NULL )
+            break;
         if ( p->pPars->fVerbose )
         {
             printf( "%3d : P =%7d. D =%7d. F =%6d. M = %7d. And =%8d. ", 
@@ -381,7 +383,7 @@ finalize:
     }
 
     pTemp = p->pAig; p->pAig = NULL;
-    if ( pTemp == NULL )
+    if ( pTemp == NULL && pSim->iOut >= 0 )
         printf( "Disproved at least one output of the miter (zero-based number %d).\n", pSim->iOut );
     else if ( pSim->pCexes )
         printf( "Disproved %d outputs of the miter.\n", pSim->nOuts );
diff --git a/src/aig/cec/cecSeq.c b/src/aig/cec/cecSeq.c
index 6cb229ae..1a398e2e 100644
--- a/src/aig/cec/cecSeq.c
+++ b/src/aig/cec/cecSeq.c
@@ -255,7 +255,7 @@ int Cec_ManSeqSemiformal( Gia_Man_t * pAig, Cec_ParSmf_t * pPars )
     Gia_Man_t * pSrm;
     int r, nPats, RetValue = -1;
     if ( pAig->pReprs == NULL )
-    {
+    { 
         printf( "Cec_ManSeqSemiformal(): Equivalence classes are not available.\n" );
         return -1;
     }
diff --git a/src/aig/cec/cecSolve.c b/src/aig/cec/cecSolve.c
index 2b6997e1..24d5c3ed 100644
--- a/src/aig/cec/cecSolve.c
+++ b/src/aig/cec/cecSolve.c
@@ -703,7 +703,8 @@ void Cec_ManSatSolveSeq( Vec_Ptr_t * vPatts, Gia_Man_t * pAig, Cec_ParSat_t * pP
     }
     p->timeTotal = clock() - clk;
     Bar_ProgressStop( pProgress );
-//    Cec_ManSatPrintStats( p );
+    if ( pPars->fVerbose )
+        Cec_ManSatPrintStats( p );
     Cec_ManSatStop( p );
     if ( pnPats )
         *pnPats = iPat-1;