Making &cec use precomputed simulation info.

4 files changed, 42 insertions, 12 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index d1ed5901..3219cd9e 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -37156,6 +37156,11 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
             Abc_Print( 0, "The verification miter is written into file \"%s\".\n", "cec_miter.aig" );
             Gia_AigerWrite( pMiter, "cec_miter.aig", 0, 0, 0 );
         }
+        if ( pGias[0]->vSimsPi )
+        {
+            pMiter->vSimsPi = Vec_WrdDup(pGias[0]->vSimsPi); 
+            pMiter->nSimWords = pGias[0]->nSimWords;
+        }
         pAbc->Status = Cec_ManVerify( pMiter, pPars );
         Abc_FrameReplaceCex( pAbc, &pGias[0]->pCexComb );
         Gia_ManStop( pMiter );
diff --git a/src/proof/cec/cecCec.c b/src/proof/cec/cecCec.c
index ee45aa6c..d450cead 100644
--- a/src/proof/cec/cecCec.c
+++ b/src/proof/cec/cecCec.c
@@ -349,6 +349,11 @@ int Cec_ManVerify( Gia_Man_t * pInit, Cec_ParCec_t * pPars )
         Gia_ManStop( p );
         return RetValue;
     }
+    if ( pInit->vSimsPi )
+    {
+        p->vSimsPi = Vec_WrdDup(pInit->vSimsPi); 
+        p->nSimWords = pInit->nSimWords;
+    }
     // sweep for equivalences
     Cec_ManFraSetDefaultParams( pParsFra );
     pParsFra->nItersMax    = 1000;
diff --git a/src/proof/cec/cecClass.c b/src/proof/cec/cecClass.c
index 2d820c39..be88b9be 100644
--- a/src/proof/cec/cecClass.c
+++ b/src/proof/cec/cecClass.c
@@ -878,19 +878,34 @@ int Cec_ManSimClassesPrepare( Cec_ManSim_t * p, int LevelMax )
             if ( pObj->Value )
                 Gia_ObjSetRepr( p->pAig, Gia_ObjId(p->pAig, pObj), 0 );
     // perform simulation
-    p->nWords = 1;
-    do {
+    if ( p->pAig->nSimWords )
+    {
+        p->nWords = 2*p->pAig->nSimWords;
+        assert( Vec_WrdSize(p->pAig->vSimsPi) == Gia_ManCiNum(p->pAig) * p->pAig->nSimWords ); 
+        //Cec_ManSimCreateInfo( p, p->vCiSimInfo, p->vCoSimInfo );
+        for ( i = 0; i < Gia_ManCiNum(p->pAig); i++ )
+            memmove( Vec_PtrEntry(p->vCiSimInfo, i), Vec_WrdEntryP(p->pAig->vSimsPi, i*p->pAig->nSimWords), sizeof(word)*p->pAig->nSimWords );
+        if ( Cec_ManSimSimulateRound( p, p->vCiSimInfo, p->vCoSimInfo ) )
+            return 1;
         if ( p->pPars->fVerbose )
             Gia_ManEquivPrintClasses( p->pAig, 0, Cec_MemUsage(p) );
-        for ( i = 0; i < 4; i++ )
-        {
-            Cec_ManSimCreateInfo( p, p->vCiSimInfo, p->vCoSimInfo );
-            if ( Cec_ManSimSimulateRound( p, p->vCiSimInfo, p->vCoSimInfo ) )
-                return 1;
+    }
+    else
+    {
+        p->nWords = 1;
+        do {
+            if ( p->pPars->fVerbose )
+                Gia_ManEquivPrintClasses( p->pAig, 0, Cec_MemUsage(p) );
+            for ( i = 0; i < 4; i++ )
+            {
+                Cec_ManSimCreateInfo( p, p->vCiSimInfo, p->vCoSimInfo );
+                if ( Cec_ManSimSimulateRound( p, p->vCiSimInfo, p->vCoSimInfo ) )
+                    return 1;
+            }
+            p->nWords = 2 * p->nWords + 1;
         }
-        p->nWords = 2 * p->nWords + 1;
+        while ( p->nWords <= p->pPars->nWords );
     }
-    while ( p->nWords <= p->pPars->nWords );
     return 0;
 }
 
diff --git a/src/proof/cec/cecCore.c b/src/proof/cec/cecCore.c
index b9529658..9f218dd3 100644
--- a/src/proof/cec/cecCore.c
+++ b/src/proof/cec/cecCore.c
@@ -360,6 +360,11 @@ Gia_Man_t * Cec_ManSatSweeping( Gia_Man_t * pAig, Cec_ParFra_t * pPars, int fSil
         Vec_IntFreeP( &pAig->vIdsEquiv );
         pAig->vIdsEquiv = Vec_IntAlloc( 1000 );
     }
+    if ( pAig->vSimsPi )
+    {
+        pIni->vSimsPi = Vec_WrdDup(pAig->vSimsPi); 
+        pIni->nSimWords = pAig->nSimWords;
+    }
 
     // prepare the managers
     // SAT sweeping
@@ -368,12 +373,12 @@ Gia_Man_t * Cec_ManSatSweeping( Gia_Man_t * pAig, Cec_ParFra_t * pPars, int fSil
         pPars->fColorDiff = 1;
     // simulation
     Cec_ManSimSetDefaultParams( pParsSim );
-    pParsSim->nWords      = pPars->nWords;
+    pParsSim->nWords      = Abc_MaxInt(2*pAig->nSimWords, pPars->nWords);
     pParsSim->nFrames     = pPars->nRounds;
     pParsSim->fCheckMiter = pPars->fCheckMiter;
     pParsSim->fDualOut    = pPars->fDualOut;
     pParsSim->fVerbose    = pPars->fVerbose;
-    pSim = Cec_ManSimStart( p->pAig, pParsSim );
+    pSim = Cec_ManSimStart( pIni, pParsSim );
     // SAT solving
     Cec_ManSatSetDefaultParams( pParsSat );
     pParsSat->nBTLimit = pPars->nBTLimit;
@@ -386,7 +391,7 @@ Gia_Man_t * Cec_ManSatSweeping( Gia_Man_t * pAig, Cec_ParFra_t * pPars, int fSil
 clk = Abc_Clock();
     if ( p->pAig->pReprs == NULL )
     {
-        if ( Cec_ManSimClassesPrepare(pSim, -1) || Cec_ManSimClassesRefine(pSim) )
+        if ( Cec_ManSimClassesPrepare(pSim, -1) || (!p->pAig->nSimWords && Cec_ManSimClassesRefine(pSim)) )
         {
             Gia_ManStop( p->pAig );
             p->pAig = NULL;