diff options
Diffstat (limited to 'src/aig/cec/cecCore.c')
-rw-r--r-- | src/aig/cec/cecCore.c | 53 |
1 files changed, 39 insertions, 14 deletions
diff --git a/src/aig/cec/cecCore.c b/src/aig/cec/cecCore.c index e25ddc90..061c3a7d 100644 --- a/src/aig/cec/cecCore.c +++ b/src/aig/cec/cecCore.c @@ -70,12 +70,37 @@ void Cec_ManSimSetDefaultParams( Cec_ParSim_t * p ) 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->fDoubleOuts = 0; // miter with separate outputs + p->fDualOut = 0; // miter with separate outputs p->fSeqSimulate = 0; // performs sequential simulation p->fVeryVerbose = 0; // verbose stats p->fVerbose = 0; // verbose stats } - + +/**Function************ ************************************************* + + Synopsis [This procedure sets default parameters.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +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->nFrames = 2; // the number of time frames + p->nBTLimit = 1000; // 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->fVerbose = 0; // verbose stats +} + /**Function************ ************************************************* Synopsis [This procedure sets default parameters.] @@ -100,7 +125,7 @@ void Cec_ManFraSetDefaultParams( Cec_ParFra_t * p ) p->fRewriting = 0; // enables AIG rewriting p->fCheckMiter = 0; // the circuit is the miter p->fFirstStop = 0; // stop on the first sat output - p->fDoubleOuts = 0; // miter with separate outputs + p->fDualOut = 0; // miter with separate outputs p->fColorDiff = 0; // miter with separate outputs p->fVeryVerbose = 0; // verbose stats p->fVerbose = 0; // verbose stats @@ -177,7 +202,8 @@ void Cec_ManSimulation( Gia_Man_t * pAig, Cec_ParSim_t * pPars ) 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 ); - ABC_PRT( "Time", clock() - clkTotal ); + if ( pPars->fVerbose ) + ABC_PRT( "Time", clock() - clkTotal ); Cec_ManSimStop( pSim ); } @@ -213,7 +239,7 @@ Gia_Man_t * Cec_ManSatSweeping( Gia_Man_t * pAig, Cec_ParFra_t * pPars ) // prepare the managers // SAT sweeping p = Cec_ManFraStart( pIni, pPars ); - if ( pPars->fDoubleOuts ) + if ( pPars->fDualOut ) pPars->fColorDiff = 1; // simulation Cec_ManSimSetDefaultParams( pParsSim ); @@ -221,10 +247,9 @@ Gia_Man_t * Cec_ManSatSweeping( Gia_Man_t * pAig, Cec_ParFra_t * pPars ) pParsSim->nRounds = pPars->nRounds; pParsSim->fCheckMiter = pPars->fCheckMiter; pParsSim->fFirstStop = pPars->fFirstStop; - pParsSim->fDoubleOuts = pPars->fDoubleOuts; + pParsSim->fDualOut = pPars->fDualOut; pParsSim->fVerbose = pPars->fVerbose; pSim = Cec_ManSimStart( p->pAig, pParsSim ); - pSim->nWords = p->pPars->nWords; // SAT solving Cec_ManSatSetDefaultParams( pParsSat ); pParsSat->nBTLimit = pPars->nBTLimit; @@ -250,7 +275,7 @@ p->timeSim += clock() - clk; { clk2 = clock(); nMatches = 0; - if ( pPars->fDoubleOuts ) + if ( pPars->fDualOut ) { nMatches = Gia_ManEquivSetColors( p->pAig, pPars->fVeryVerbose ); // p->pAig->pIso = Cec_ManDetectIsomorphism( p->pAig ); @@ -264,7 +289,7 @@ p->timeSim += clock() - clk; Gia_ManStop( pSrm ); if ( p->pPars->fVerbose ) printf( "Considered all available candidate equivalences.\n" ); - if ( pPars->fDoubleOuts && Gia_ManAndNum(p->pAig) > 0 ) + if ( pPars->fDualOut && Gia_ManAndNum(p->pAig) > 0 ) { if ( pPars->fColorDiff ) { @@ -276,7 +301,7 @@ p->timeSim += clock() - clk; { if ( p->pPars->fVerbose ) printf( "Switching into normal mode.\n" ); - pPars->fDoubleOuts = 0; + pPars->fDualOut = 0; } continue; } @@ -295,7 +320,7 @@ p->timeSat += clock() - clk; Gia_ManStop( pSrm ); // update the manager - pSim->pAig = p->pAig = Gia_ManEquivReduceAndRemap( pTemp = p->pAig, 0, pParsSim->fDoubleOuts ); + pSim->pAig = p->pAig = Gia_ManEquivReduceAndRemap( pTemp = p->pAig, 0, pParsSim->fDualOut ); Gia_ManStop( pTemp ); if ( p->pPars->fVerbose ) { @@ -332,18 +357,18 @@ p->timeSat += clock() - clk; } } } - if ( pPars->fDoubleOuts && pPars->fColorDiff && Gia_ManAndNum(p->pAig) < 100000 ) + if ( pPars->fDualOut && pPars->fColorDiff && Gia_ManAndNum(p->pAig) < 100000 ) { if ( p->pPars->fVerbose ) printf( "Switching into reduced mode.\n" ); pPars->fColorDiff = 0; } - if ( pPars->fDoubleOuts && Gia_ManAndNum(p->pAig) < 20000 ) + if ( pPars->fDualOut && Gia_ManAndNum(p->pAig) < 20000 ) { if ( p->pPars->fVerbose ) printf( "Switching into normal mode.\n" ); pPars->fColorDiff = 0; - pPars->fDoubleOuts = 0; + pPars->fDualOut = 0; } } finalize: |