From 7ae0f4966a68ba3190b03a16810ae3daf23d14c0 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sun, 8 Mar 2026 12:04:25 -0700 Subject: [PATCH] Adding gla to sprove. --- src/base/abci/abc.c | 2 +- src/proof/abs/abs.h | 3 ++- src/proof/abs/absGla.c | 10 +++++++++- src/proof/abs/absUtil.c | 3 ++- src/proof/cec/cecProve.c | 36 +++++++++++++++++++++++++++++++++--- 5 files changed, 47 insertions(+), 7 deletions(-) diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index f1bef5e23..63847c88b 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -51398,7 +51398,7 @@ int Abc_CommandAbc9SProve( Abc_Frame_t * pAbc, int argc, char ** argv ) { Gia_Man_t * pGiaUse = pAbc->pGia, * pGiaTemp = NULL; Wlc_Ntk_t * pWlc = (Wlc_Ntk_t *)pAbc->pAbcWlc; - int c, nProcs = 5, nTimeOut = 3, nTimeOut2 = 10, nTimeOut3 = 100, fUseUif = 0, fVerbose = 0, fVeryVerbose = 0, fSilent = 0; + int c, nProcs = 6, nTimeOut = 3, nTimeOut2 = 10, nTimeOut3 = 100, fUseUif = 0, fVerbose = 0, fVeryVerbose = 0, fSilent = 0; Extra_UtilGetoptReset(); while ( ( c = Extra_UtilGetopt( argc, argv, "PTUWusvwh" ) ) != EOF ) { diff --git a/src/proof/abs/abs.h b/src/proof/abs/abs.h index 1c31e7cc6..782afebdf 100644 --- a/src/proof/abs/abs.h +++ b/src/proof/abs/abs.h @@ -74,6 +74,8 @@ struct Abs_Par_t_ char * pFileVabs; // dumps the abstracted model into this file int fVerbose; // verbose flag int fVeryVerbose; // print additional information + int RunId; // id in this run + int (*pFuncStop)(int); // callback to terminate int iFrame; // the number of frames covered int iFrameProved; // the number of frames proved int nFramesNoChange; // the number of last frames without changes @@ -174,4 +176,3 @@ ABC_NAMESPACE_HEADER_END //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// - diff --git a/src/proof/abs/absGla.c b/src/proof/abs/absGla.c index 75f991d3b..9f1a8a31e 100644 --- a/src/proof/abs/absGla.c +++ b/src/proof/abs/absGla.c @@ -1576,6 +1576,8 @@ int Gia_ManPerformGla( Gia_Man_t * pAig, Abs_Par_t * pPars ) for ( i = f = 0; !pPars->nFramesMax || f < pPars->nFramesMax; i++ ) { int nAbsOld; + if ( pPars->pFuncStop && pPars->pFuncStop(pPars->RunId) ) + goto finish; // remember the timeframe p->pPars->iFrame = -1; // create new SAT solver @@ -1585,6 +1587,8 @@ int Gia_ManPerformGla( Gia_Man_t * pAig, Abs_Par_t * pPars ) // unroll the circuit for ( f = 0; !pPars->nFramesMax || f < pPars->nFramesMax; f++ ) { + if ( pPars->pFuncStop && pPars->pFuncStop(pPars->RunId) ) + goto finish; // remember current limits int nConflsBeg = sat_solver2_nconflicts(p->pSat); int nAbs = Vec_IntSize(p->vAbs); @@ -1618,6 +1622,11 @@ int Gia_ManPerformGla( Gia_Man_t * pAig, Abs_Par_t * pPars ) nVarsOld = p->nSatVars; for ( c = 0; ; c++ ) { + if ( pPars->pFuncStop && pPars->pFuncStop(pPars->RunId) ) + { + Status = l_Undef; + goto finish; + } // consider the special case when the target literal is implied false // by implications which happened as a result of previous refinements // note that incremental UNSAT core cannot be computed because there is no learned clauses @@ -1898,4 +1907,3 @@ finish: ABC_NAMESPACE_IMPL_END - diff --git a/src/proof/abs/absUtil.c b/src/proof/abs/absUtil.c index 286d1091b..d0d85ae41 100644 --- a/src/proof/abs/absUtil.c +++ b/src/proof/abs/absUtil.c @@ -59,6 +59,8 @@ void Abs_ParSetDefaults( Abs_Par_t * p ) p->fUseRollback = 0; // use rollback to the starting number of frames p->fPropFanout = 1; // propagate fanouts during refinement p->fVerbose = 0; // verbose flag + p->RunId = -1; // id in this run + p->pFuncStop = NULL; // callback to terminate p->iFrame = -1; // the number of frames covered p->iFrameProved = -1; // the number of frames proved p->nFramesNoChangeLim = 2; // the number of frames without change to dump abstraction @@ -254,4 +256,3 @@ int Gia_GlaCountNodes( Gia_Man_t * p, Vec_Int_t * vGla ) ABC_NAMESPACE_IMPL_END - diff --git a/src/proof/cec/cecProve.c b/src/proof/cec/cecProve.c index 017296540..c3ed1fad7 100644 --- a/src/proof/cec/cecProve.c +++ b/src/proof/cec/cecProve.c @@ -26,6 +26,7 @@ #include "proof/pdr/pdr.h" #include "proof/cec/cec.h" #include "proof/ssw/ssw.h" +#include "proof/abs/abs.h" #ifdef ABC_USE_PTHREADS @@ -66,6 +67,7 @@ int Cec_GiaProveTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nTimeOut2, in #define PAR_ENGINE_UFAR 6 #define PAR_ENGINE_SCORR1 7 #define PAR_ENGINE_SCORR2 8 +#define PAR_ENGINE_GLA 9 struct Par_Share_t_ { volatile int fSolved; @@ -90,6 +92,7 @@ typedef struct Cec_ScorrStop_t_ abctime TimeToStop; } Cec_ScorrStop_t; static volatile Par_Share_t * g_pUfarShare = NULL; +static volatile Par_Share_t * g_pGlaShare = NULL; static inline const char * Cec_SolveEngineName( int iEngine ) { if ( iEngine == 0 ) return "rar"; @@ -101,6 +104,7 @@ static inline const char * Cec_SolveEngineName( int iEngine ) if ( iEngine == PAR_ENGINE_UFAR ) return "ufar"; if ( iEngine == PAR_ENGINE_SCORR1 ) return "scorr-new"; if ( iEngine == PAR_ENGINE_SCORR2 ) return "scorr-old"; + if ( iEngine == PAR_ENGINE_GLA ) return "gla-q"; return "unknown"; } static inline void Cec_CopyGiaName( Gia_Man_t * pSrc, Gia_Man_t * pDst ) @@ -128,6 +132,11 @@ static int Cec_SProveStopUfar( int RunId ) (void)RunId; return g_pUfarShare && g_pUfarShare->fSolved != 0; } +static int Cec_SProveStopGla( int RunId ) +{ + (void)RunId; + return g_pGlaShare && g_pGlaShare->fSolved != 0; +} static int Cec_ScorrStop( void * pUser ) { Cec_ScorrStop_t * p = (Cec_ScorrStop_t *)pUser; @@ -177,7 +186,7 @@ int Cec_GiaProveOne( Gia_Man_t * p, int iEngine, int nTimeOut, int fVerbose, Par { abctime clk = Abc_Clock(); int RetValue = -1; - if ( iEngine != PAR_ENGINE_UFAR && Gia_ManRegNum(p) == 0 ) + if ( iEngine != PAR_ENGINE_UFAR && iEngine != PAR_ENGINE_GLA && Gia_ManRegNum(p) == 0 ) { if ( fVerbose ) printf( "Engine %d skipped because the current miter is combinational.\n", iEngine ); @@ -294,6 +303,22 @@ int Cec_GiaProveOne( Gia_Man_t * p, int iEngine, int nTimeOut, int fVerbose, Par g_pUfarShare = NULL; } } + else if ( iEngine == PAR_ENGINE_GLA ) + { + if ( Gia_ManPoNum(p) != 1 ) + return -1; + Abs_Par_t Pars, * pPars = &Pars; + Abs_ParSetDefaults( pPars ); + pPars->nTimeOut = nTimeOut; + pPars->fCallProver = 1; // emulate "&gla -q" + pPars->fVerbose = 0; + pPars->fVeryVerbose = 0; + pPars->RunId = 0; + pPars->pFuncStop = Cec_SProveStopGla; + g_pGlaShare = pThData ? pThData->pShare : NULL; + RetValue = Gia_ManPerformGla( p, pPars ); + g_pGlaShare = NULL; + } else assert( 0 ); //while ( Abc_Clock() < clkStop ); if ( pThData && pThData->pShare && RetValue != -1 ) @@ -379,7 +404,12 @@ void Cec_GiaInitThreads( Par_ThData_t * ThData, int nWorkers, Gia_Man_t * p, int { ThData[i].p = Gia_ManDup(p); Cec_CopyGiaName( p, ThData[i].p ); - ThData[i].iEngine = (fUseUif && i == nWorkers - 1) ? PAR_ENGINE_UFAR : i; + if ( fUseUif && i == nWorkers - 1 ) + ThData[i].iEngine = PAR_ENGINE_UFAR; + else if ( !fUseUif && nWorkers == 6 && i == 5 ) + ThData[i].iEngine = PAR_ENGINE_GLA; + else + ThData[i].iEngine = i; ThData[i].nTimeOut = nTimeOut; ThData[i].fWorking = 0; ThData[i].Result = -1; @@ -427,7 +457,7 @@ int Cec_GiaProveTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nTimeOut2, in printf( "Processes = %d TimeOut = %d sec Verbose = %d.\n", nProcs, nTimeOut, fVerbose ); fflush( stdout ); - assert( nProcs == 3 || nProcs == 5 ); + assert( nProcs == 3 || nProcs == 5 || nProcs == 6 ); assert( nWorkers <= PAR_THR_MAX ); Cec_GiaInitThreads( ThData, nWorkers, p, nTimeOut, nTimeOut3, pWlc, fUseUif, fVerbose, WorkerThread, &Share );