diff options
Diffstat (limited to 'src/proof/cec/cecChoice.c')
| -rw-r--r-- | src/proof/cec/cecChoice.c | 25 |
1 files changed, 24 insertions, 1 deletions
diff --git a/src/proof/cec/cecChoice.c b/src/proof/cec/cecChoice.c index 49025630..db0059fd 100644 --- a/src/proof/cec/cecChoice.c +++ b/src/proof/cec/cecChoice.c @@ -256,7 +256,7 @@ int Cec_ManChoiceComputation_int( Gia_Man_t * pAig, Cec_ParChc_t * pPars ) // found counter-examples to speculation clk2 = Abc_Clock(); if ( pPars->fUseCSat ) - vCexStore = Cbs_ManSolveMiterNc( pSrm, pPars->nBTLimit, &vStatus, 0 ); + vCexStore = Cbs_ManSolveMiterNc( pSrm, pPars->nBTLimit, &vStatus, 0, 0 ); else vCexStore = Cec_ManSatSolveMiter( pSrm, pParsSat, &vStatus ); Gia_ManStop( pSrm ); @@ -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 nConfs, int fVerbose ) +{ + extern void Cec4_ManSimulateTest2( Gia_Man_t * p, int nConfs, int fVerbose ); + Aig_Man_t * pAig; + Cec4_ManSimulateTest2( pGia, nConfs, 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 /// //////////////////////////////////////////////////////////////////////// |