diff options
Diffstat (limited to 'src/proof/cec')
| -rw-r--r-- | src/proof/cec/cecChoice.c | 23 | ||||
| -rw-r--r-- | src/proof/cec/cecSatG2.c | 44 |
2 files changed, 67 insertions, 0 deletions
diff --git a/src/proof/cec/cecChoice.c b/src/proof/cec/cecChoice.c index 49025630..47d6a478 100644 --- a/src/proof/cec/cecChoice.c +++ b/src/proof/cec/cecChoice.c @@ -401,6 +401,29 @@ Aig_Man_t * Cec_ComputeChoices( Gia_Man_t * pGia, Dch_Pars_t * pPars ) return pAig; } +/**Function************************************************************* + + Synopsis [Performs computation of AIGs with choices.] + + Description [Takes several AIGs and performs choicing.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Cec_ComputeChoicesNew( Gia_Man_t * pGia, int fVerbose ) +{ + extern void Cec4_ManSimulateTest2( Gia_Man_t * p, int fVerbose ); + Aig_Man_t * pAig; + Cec4_ManSimulateTest2( pGia, fVerbose ); + pGia = Gia_ManEquivToChoices( pGia, 3 ); + Gia_ManSetRegNum( pGia, Gia_ManRegNum(pGia) ); + pAig = Gia_ManToAig( pGia, 1 ); + Gia_ManStop( pGia ); + return pAig; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/proof/cec/cecSatG2.c b/src/proof/cec/cecSatG2.c index 51654cba..122f33d0 100644 --- a/src/proof/cec/cecSatG2.c +++ b/src/proof/cec/cecSatG2.c @@ -145,6 +145,30 @@ static inline void Cec4_ObjCleanSatId( Gia_Man_t * p, Gia_Obj_t * pObj ) /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// +/**Function************************************************************* + + Synopsis [Default parameter settings.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Cec4_ManSetParams( Cec_ParFra_t * pPars ) +{ + memset( pPars, 0, sizeof(Cec_ParFra_t) ); + pPars->jType = 2; // solver type + pPars->fSatSweeping = 1; // conflict limit at a node + pPars->nWords = 4; // simulation words + pPars->nRounds = 10; // simulation rounds + pPars->nItersMax = 2000; // this is a miter + pPars->nBTLimit = 1000000; // use logic cones + pPars->nSatVarMax = 1000; // the max number of SAT variables before recycling SAT solver + pPars->nCallsRecycle = 500; // calls to perform before recycling SAT solver + pPars->nGenIters = 100; // pattern generation iterations +} /**Function************************************************************* @@ -1768,6 +1792,26 @@ Gia_Man_t * Cec4_ManSimulateTest( Gia_Man_t * p, Cec_ParFra_t * pPars ) Cec4_ManPerformSweeping( p, pPars, &pNew ); return pNew; } +void Cec4_ManSimulateTest2( Gia_Man_t * p, int fVerbose ) +{ + abctime clk = Abc_Clock(); + Cec_ParFra_t ParsFra, * pPars = &ParsFra; + Cec4_ManSetParams( pPars ); + Cec4_ManPerformSweeping( p, pPars, NULL ); + pPars->fVerbose = fVerbose; + //if ( fVerbose ) + Abc_PrintTime( 1, "New choice computation time", Abc_Clock() - clk ); +} +Gia_Man_t * Cec4_ManSimulateTest3( Gia_Man_t * p, int fVerbose ) +{ + abctime clk = Abc_Clock(); + Gia_Man_t * pNew = NULL; + Cec_ParFra_t ParsFra, * pPars = &ParsFra; + Cec4_ManSetParams( pPars ); + pPars->fVerbose = fVerbose; + Cec4_ManPerformSweeping( p, pPars, &pNew ); + return pNew; +} //////////////////////////////////////////////////////////////////////// /// END OF FILE /// |