diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2021-07-31 15:34:46 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2021-07-31 15:34:46 -0700 |
| commit | 692dd763190d2e2682c0eeabdcd81f16aaaabe94 (patch) | |
| tree | a62ab7910e947f5967b90b527fdbaaf4785ee607 /src/proof | |
| parent | d925e4802cdbd89b1c7cee4fa1041b08cf0d32f7 (diff) | |
| download | abc-692dd763190d2e2682c0eeabdcd81f16aaaabe94.tar.gz abc-692dd763190d2e2682c0eeabdcd81f16aaaabe94.tar.bz2 abc-692dd763190d2e2682c0eeabdcd81f16aaaabe94.zip | |
Upgrading choice computation.
Diffstat (limited to 'src/proof')
| -rw-r--r-- | src/proof/cec/cecChoice.c | 6 | ||||
| -rw-r--r-- | src/proof/cec/cecSatG2.c | 3 |
2 files changed, 5 insertions, 4 deletions
diff --git a/src/proof/cec/cecChoice.c b/src/proof/cec/cecChoice.c index 780a1196..db0059fd 100644 --- a/src/proof/cec/cecChoice.c +++ b/src/proof/cec/cecChoice.c @@ -412,11 +412,11 @@ Aig_Man_t * Cec_ComputeChoices( Gia_Man_t * pGia, Dch_Pars_t * pPars ) SeeAlso [] ***********************************************************************/ -Aig_Man_t * Cec_ComputeChoicesNew( Gia_Man_t * pGia, int fVerbose ) +Aig_Man_t * Cec_ComputeChoicesNew( Gia_Man_t * pGia, int nConfs, int fVerbose ) { - extern void Cec4_ManSimulateTest2( Gia_Man_t * p, int fVerbose ); + extern void Cec4_ManSimulateTest2( Gia_Man_t * p, int nConfs, int fVerbose ); Aig_Man_t * pAig; - Cec4_ManSimulateTest2( pGia, fVerbose ); + Cec4_ManSimulateTest2( pGia, nConfs, fVerbose ); pGia = Gia_ManEquivToChoices( pGia, 3 ); Gia_ManSetRegNum( pGia, Gia_ManRegNum(pGia) ); pAig = Gia_ManToAig( pGia, 1 ); diff --git a/src/proof/cec/cecSatG2.c b/src/proof/cec/cecSatG2.c index 19349986..ae90e7fc 100644 --- a/src/proof/cec/cecSatG2.c +++ b/src/proof/cec/cecSatG2.c @@ -1794,13 +1794,14 @@ Gia_Man_t * Cec4_ManSimulateTest( Gia_Man_t * p, Cec_ParFra_t * pPars ) Cec4_ManPerformSweeping( p, pPars, &pNew, 0 ); return pNew; } -void Cec4_ManSimulateTest2( Gia_Man_t * p, int fVerbose ) +void Cec4_ManSimulateTest2( Gia_Man_t * p, int nConfs, int fVerbose ) { abctime clk = Abc_Clock(); Cec_ParFra_t ParsFra, * pPars = &ParsFra; Cec4_ManSetParams( pPars ); Cec4_ManPerformSweeping( p, pPars, NULL, 0 ); pPars->fVerbose = fVerbose; + pPars->nBTLimit = nConfs; if ( fVerbose ) Abc_PrintTime( 1, "New choice computation time", Abc_Clock() - clk ); } |