diff --git a/src/proof/cec/cecProve.c b/src/proof/cec/cecProve.c index 273791fe4..2de1b68b6 100644 --- a/src/proof/cec/cecProve.c +++ b/src/proof/cec/cecProve.c @@ -64,6 +64,8 @@ int Cec_GiaProveTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nTimeOut2, in #define PAR_THR_MAX 8 #define PAR_ENGINE_UFAR 6 +#define PAR_ENGINE_SCORR1 7 +#define PAR_ENGINE_SCORR2 8 struct Par_Share_t_ { volatile int fSolved; @@ -82,7 +84,25 @@ typedef struct Par_ThData_t_ Wlc_Ntk_t * pWlc; Par_Share_t * pShare; } Par_ThData_t; +typedef struct Cec_ScorrStop_t_ +{ + Par_Share_t * pShare; + abctime TimeToStop; +} Cec_ScorrStop_t; static volatile Par_Share_t * g_pUfarShare = NULL; +static inline const char * Cec_SolveEngineName( int iEngine ) +{ + if ( iEngine == 0 ) return "rar"; + if ( iEngine == 1 ) return "bmc"; + if ( iEngine == 2 ) return "pdr"; + if ( iEngine == 3 ) return "bmc-glucose"; + if ( iEngine == 4 ) return "pdr-abs"; + if ( iEngine == 5 ) return "bmcg"; + if ( iEngine == PAR_ENGINE_UFAR ) return "ufar"; + if ( iEngine == PAR_ENGINE_SCORR1 ) return "scorr-new"; + if ( iEngine == PAR_ENGINE_SCORR2 ) return "scorr-old"; + return "unknown"; +} static inline void Cec_CopyGiaName( Gia_Man_t * pSrc, Gia_Man_t * pDst ) { char * pName = pSrc->pName ? pSrc->pName : pSrc->pSpec; @@ -108,6 +128,17 @@ static int Cec_SProveStopUfar( int RunId ) (void)RunId; return g_pUfarShare && g_pUfarShare->fSolved != 0; } +static int Cec_ScorrStop( void * pUser ) +{ + Cec_ScorrStop_t * p = (Cec_ScorrStop_t *)pUser; + if ( p == NULL ) + return 0; + if ( p->pShare && p->pShare->fSolved ) + return 1; + if ( p->TimeToStop && Abc_Clock() >= p->TimeToStop ) + return 1; + return 0; +} static int Cec_SProveCallback( void * pUser, int fSolved, unsigned Result ) { Par_ThData_t * pThData = (Par_ThData_t *)pUser; @@ -273,12 +304,15 @@ int Cec_GiaProveOne( Gia_Man_t * p, int iEngine, int nTimeOut, int fVerbose, Par } return RetValue; } -Gia_Man_t * Cec_GiaScorrOld( Gia_Man_t * p ) +Gia_Man_t * Cec_GiaScorrOld( Gia_Man_t * p, int nTimeOut, Par_Share_t * pShare ) { + Cec_ScorrStop_t Stop = { pShare, nTimeOut > 0 ? Abc_Clock() + (abctime)nTimeOut * CLOCKS_PER_SEC : 0 }; if ( Gia_ManRegNum(p) == 0 ) return Gia_ManDup( p ); Ssw_Pars_t Pars, * pPars = &Pars; Ssw_ManSetDefaultParams( pPars ); + pPars->pFunc = (void *)Cec_ScorrStop; + pPars->pData = (void *)&Stop; Aig_Man_t * pAig = Gia_ManToAigSimple( p ); Aig_Man_t * pAig2 = Ssw_SignalCorrespondence( pAig, pPars ); Gia_Man_t * pGia2 = Gia_ManFromAigSimple( pAig2 ); @@ -286,8 +320,9 @@ Gia_Man_t * Cec_GiaScorrOld( Gia_Man_t * p ) Aig_ManStop( pAig ); return pGia2; } -Gia_Man_t * Cec_GiaScorrNew( Gia_Man_t * p ) +Gia_Man_t * Cec_GiaScorrNew( Gia_Man_t * p, int nTimeOut, Par_Share_t * pShare ) { + Cec_ScorrStop_t Stop = { pShare, nTimeOut > 0 ? Abc_Clock() + (abctime)nTimeOut * CLOCKS_PER_SEC : 0 }; if ( Gia_ManRegNum(p) == 0 ) return Gia_ManDup( p ); Cec_ParCor_t Pars, * pPars = &Pars; @@ -296,6 +331,8 @@ Gia_Man_t * Cec_GiaScorrNew( Gia_Man_t * p ) pPars->nLevelMax = 100; pPars->fVerbose = 0; pPars->fUseCSat = 1; + pPars->pFunc = (void *)Cec_ScorrStop; + pPars->pData = (void *)&Stop; return Cec_ManLSCorrespondence( p, pPars ); } @@ -376,7 +413,7 @@ int Cec_GiaProveTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nTimeOut2, in Par_ThData_t ThData[PAR_THR_MAX]; pthread_t WorkerThread[PAR_THR_MAX]; Par_Share_t Share; - int i, nWorkers = nProcs + (fUseUif ? 1 : 0), RetValue = -1, RetEngine = -2; + int i, nWorkers = nProcs + (fUseUif ? 1 : 0), RetValue = -1, RetEngine = -1; memset( &Share, 0, sizeof(Par_Share_t) ); Abc_CexFreeP( &p->pCexComb ); Abc_CexFreeP( &p->pCexSeq ); @@ -391,10 +428,10 @@ int Cec_GiaProveTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nTimeOut2, in Cec_GiaInitThreads( ThData, nWorkers, p, nTimeOut, nTimeOut3, pWlc, fUseUif, fVerbose, WorkerThread, &Share ); // meanwhile, perform scorr - Gia_Man_t * pScorr = Cec_GiaScorrNew( p ); + Gia_Man_t * pScorr = Cec_GiaScorrNew( p, nTimeOut, &Share ); clkScorr = Abc_Clock() - clkTotal; if ( Gia_ManAndNum(pScorr) == 0 ) - RetValue = 1, RetEngine = -1; + RetValue = 1, RetEngine = PAR_ENGINE_SCORR1; RetValue = Cec_GiaWaitThreads( ThData, nWorkers, p, RetValue, &RetEngine ); if ( RetValue == -1 ) @@ -406,15 +443,15 @@ int Cec_GiaProveTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nTimeOut2, in } Cec_GiaInitThreads( ThData, nWorkers, pScorr, nTimeOut2, nTimeOut3, pWlc, fUseUif, fVerbose, NULL, &Share ); - // meanwhile, perform scorr - if ( Gia_ManAndNum(pScorr) < 100000 ) + RetValue = Cec_GiaWaitThreads( ThData, nWorkers, p, RetValue, &RetEngine ); + if ( RetValue == -1 && Gia_ManAndNum(pScorr) < 100000 ) { - Gia_Man_t * pScorr2 = Cec_GiaScorrOld( pScorr ); + // Run this reduction only when round-2 did not decide the problem. + Gia_Man_t * pScorr2 = Cec_GiaScorrOld( pScorr, nTimeOut3, &Share ); clkScorr2 = Abc_Clock() - clkStart; if ( Gia_ManAndNum(pScorr2) == 0 ) - RetValue = 1; - - RetValue = Cec_GiaWaitThreads( ThData, nWorkers, p, RetValue, &RetEngine ); + RetValue = 1, RetEngine = PAR_ENGINE_SCORR2; + if ( RetValue == -1 ) { if ( !fSilent && fVerbose ) { @@ -440,11 +477,13 @@ int Cec_GiaProveTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nTimeOut2, in if ( !fSilent ) { char * pProbName = p->pSpec ? p->pSpec : Gia_ManName(p); + if ( RetValue != -1 && RetEngine < 0 ) + RetEngine = PAR_ENGINE_SCORR1; printf( "Problem \"%s\" is ", pProbName ? pProbName : "(none)" ); if ( RetValue == 0 ) - printf( "SATISFIABLE (solved by %d).", RetEngine ); + printf( "SATISFIABLE (solved by %s).", Cec_SolveEngineName(RetEngine) ); else if ( RetValue == 1 ) - printf( "UNSATISFIABLE (solved by %d).", RetEngine ); + printf( "UNSATISFIABLE (solved by %s).", Cec_SolveEngineName(RetEngine) ); else if ( RetValue == -1 ) printf( "UNDECIDED." ); else assert( 0 );