From 8aa7e12dab432202be0f85bb293c202ec83de52f Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sat, 11 Apr 2026 21:14:19 -0700 Subject: [PATCH] Adding trace logging to &sprove. --- src/base/abci/abc.c | 128 ++++++- src/proof/cec/cecProve.c | 804 +++++++++++++++++++++++++++++++++------ 2 files changed, 817 insertions(+), 115 deletions(-) diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index e31b15da4..74fc6e356 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -579,6 +579,7 @@ static int Abc_CommandAbc9GroupProve ( Abc_Frame_t * pAbc, int argc, cha static int Abc_CommandAbc9MultiProve ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9SplitProve ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9SProve ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc9SProve2 ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9SplitSat ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Bmc ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9SBmc ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -684,7 +685,9 @@ extern void Extra_BitMatrixTransposeP( Vec_Wrd_t * vSimsIn, int nWordsIn, Vec_Wr typedef struct Wlc_Ntk_t_ Wlc_Ntk_t; typedef struct Wlc_BstPar_t_ Wlc_BstPar_t; extern Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Wlc_BstPar_t * pPars ); -extern int Cec_GiaProveTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nTimeOut2, int nTimeOut3, int fUseUif, Wlc_Ntk_t * pWlc, int fVerbose, int fVeryVerbose, int fSilent ); +extern int Cec_GiaProveTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nTimeOut2, int nTimeOut3, int fUseUif, Wlc_Ntk_t * pWlc, int fVerbose, int fVeryVerbose, int fSilent, char * pReplayFile ); +extern int Cec_GiaReplayReadParams( char * pFileName, int * pnProcs, int * pnTimeOut, int * pnTimeOut2, int * pnTimeOut3, int * pfUseUif ); +extern int Cec_GiaReplayTest( Gia_Man_t * p, Wlc_Ntk_t * pWlc, char * pFileName, int fVerbose, int fVeryVerbose, int fSilent ); //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// @@ -1421,7 +1424,8 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "ABC9", "&gprove", Abc_CommandAbc9GroupProve, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&mprove", Abc_CommandAbc9MultiProve, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&splitprove", Abc_CommandAbc9SplitProve, 0 ); - Cmd_CommandAdd( pAbc, "ABC9", "&sprove", Abc_CommandAbc9SProve, 0 ); + Cmd_CommandAdd( pAbc, "ABC9", "&sprove", Abc_CommandAbc9SProve, 0 ); + Cmd_CommandAdd( pAbc, "ABC9", "&sprove2", Abc_CommandAbc9SProve2, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&splitsat", Abc_CommandAbc9SplitSat, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&bmc", Abc_CommandAbc9Bmc, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&bmcs", Abc_CommandAbc9SBmc, 0 ); @@ -51553,9 +51557,10 @@ 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; + char * pReplayFile = NULL; int c, nProcs = 6, nProcsNew = 0, nTimeOut = 3, nTimeOut2 = 10, nTimeOut3 = 100, fUseUif = 0, fVerbose = 0, fVeryVerbose = 0, fSilent = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "PTUWusvwh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "PTUWRusvwh" ) ) != EOF ) { switch ( c ) { @@ -51604,6 +51609,15 @@ int Abc_CommandAbc9SProve( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( nTimeOut3 <= 0 ) goto usage; break; + case 'R': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-R\" should be followed by a file name.\n" ); + goto usage; + } + pReplayFile = argv[globalUtilOptind]; + globalUtilOptind++; + break; case 'u': fUseUif ^= 1; break; @@ -51658,19 +51672,20 @@ int Abc_CommandAbc9SProve( Abc_Frame_t * pAbc, int argc, char ** argv ) Gia_ManStop( pGiaUse ); return 1; } - pAbc->Status = Cec_GiaProveTest( pGiaUse, nProcs, nTimeOut, nTimeOut2, nTimeOut3, fUseUif, pWlc, fVerbose, fVeryVerbose, fSilent ); + pAbc->Status = Cec_GiaProveTest( pGiaUse, nProcs, nTimeOut, nTimeOut2, nTimeOut3, fUseUif, pWlc, fVerbose, fVeryVerbose, fSilent, pReplayFile ); Abc_FrameReplaceCex( pAbc, &pGiaUse->pCexSeq ); if ( fUseUif ) Gia_ManStop( pGiaUse ); return 0; usage: - Abc_Print( -2, "usage: &sprove [-PTUW num] [-usvwh]\n" ); + Abc_Print( -2, "usage: &sprove [-PTUW num] [-R file] [-usvwh]\n" ); Abc_Print( -2, "\t proves CEC problem by case-splitting\n" ); Abc_Print( -2, "\t-P num : the number of concurrent processes (1 <= num <= 6) [default = %d]\n", nProcs ); Abc_Print( -2, "\t-T num : runtime limit in seconds per subproblem [default = %d]\n", nTimeOut ); Abc_Print( -2, "\t-U num : runtime limit in seconds per subproblem [default = %d]\n", nTimeOut2 ); Abc_Print( -2, "\t-W num : runtime limit in seconds per subproblem [default = %d]\n", nTimeOut3 ); + Abc_Print( -2, "\t-R str : dump replay/trace file for later execution by &sprove2\n" ); Abc_Print( -2, "\t-u : enable concurrent UFAR on word-level design (uses internal %%blast + &miter -x)\n" ); Abc_Print( -2, "\t-s : enable silent computation (no reporting) [default = %s]\n", fSilent? "yes": "no" ); Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); @@ -51679,6 +51694,109 @@ usage: return 1; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandAbc9SProve2( 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; + char * pTraceFile = NULL; + int c, nProcs = 0, nTimeOut = 0, nTimeOut2 = 0, nTimeOut3 = 0, fUseUif = 0, fVerbose = 0, fVeryVerbose = 0, fSilent = 0; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "svwh" ) ) != EOF ) + { + switch ( c ) + { + case 's': + fSilent ^= 1; + break; + case 'v': + fVerbose ^= 1; + break; + case 'w': + fVeryVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command &sprove2 expects a replay file name.\n" ); + goto usage; + } + pTraceFile = argv[globalUtilOptind]; + globalUtilOptind++; + if ( globalUtilOptind != argc ) + goto usage; + if ( !Cec_GiaReplayReadParams( pTraceFile, &nProcs, &nTimeOut, &nTimeOut2, &nTimeOut3, &fUseUif ) ) + { + Abc_Print( -1, "Abc_CommandAbc9SProve2(): Cannot read replay file \"%s\".\n", pTraceFile ); + return 1; + } + if ( fUseUif ) + { + pGiaUse = NULL; + if ( pWlc == NULL ) + { + Abc_Print( -1, "Abc_CommandAbc9SProve2(): Replay requires word-level design for UIF mode.\n" ); + return 1; + } + pGiaTemp = Wlc_NtkBitBlast( pWlc, NULL ); + if ( pGiaTemp == NULL ) + { + Abc_Print( -1, "Abc_CommandAbc9SProve2(): Word-level bit-blasting has failed.\n" ); + return 1; + } + if ( (Gia_ManPoNum(pGiaTemp) & 1) == 1 ) + { + Abc_Print( -1, "Abc_CommandAbc9SProve2(): Internal \"&miter -x\" requires even number of bit-level outputs.\n" ); + Gia_ManStop( pGiaTemp ); + return 1; + } + pGiaUse = Gia_ManTransformMiter2( pGiaTemp ); + Gia_ManStop( pGiaTemp ); + pGiaTemp = NULL; + } + if ( pGiaUse == NULL ) + { + Abc_Print( -1, "Abc_CommandAbc9SProve2(): There is no AIG.\n" ); + return 1; + } + if ( Gia_ManRegNum(pGiaUse) == 0 ) + { + Abc_Print( -1, "Abc_CommandAbc9SProve2(): The problem is combinational.\n" ); + if ( fUseUif ) + Gia_ManStop( pGiaUse ); + return 1; + } + pAbc->Status = Cec_GiaReplayTest( pGiaUse, pWlc, pTraceFile, fVerbose, fVeryVerbose, fSilent ); + Abc_FrameReplaceCex( pAbc, &pGiaUse->pCexSeq ); + if ( fUseUif ) + Gia_ManStop( pGiaUse ); + return 0; + +usage: + Abc_Print( -2, "usage: &sprove2 [-svwh]\n" ); + Abc_Print( -2, "\t replays &sprove strategy stored in the given trace file\n" ); + Abc_Print( -2, "\t-s : enable silent computation (no reporting) [default = %s]\n", fSilent? "yes": "no" ); + Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); + Abc_Print( -2, "\t-w : toggle printing more verbose information [default = %s]\n", fVeryVerbose? "yes": "no" ); + Abc_Print( -2, "\t-h : print the command usage\n"); + return 1; +} + /**Function************************************************************* Synopsis [] diff --git a/src/proof/cec/cecProve.c b/src/proof/cec/cecProve.c index cf8dfa7ed..8b7aa2868 100644 --- a/src/proof/cec/cecProve.c +++ b/src/proof/cec/cecProve.c @@ -19,6 +19,9 @@ ***********************************************************************/ #include +#include +#include +#include #include "aig/gia/gia.h" #include "aig/gia/giaAig.h" @@ -52,14 +55,23 @@ extern int Bmcg_ManPerform( Gia_Man_t * pGia, Bmc_AndPar_t * pPars ); typedef struct Par_Share_t_ Par_Share_t; typedef struct Par_ThData_t_ Par_ThData_t; -static int Cec_SProveCallback( void * pUser, int fSolved, unsigned Result ); - typedef struct Wlc_Ntk_t_ Wlc_Ntk_t; +struct Cec_ScorrStop_t_; +struct Cec_SproveTrace_t_; +static int Cec_SProveCallback( void * pUser, int fSolved, unsigned Result ); +static Gia_Man_t * Cec_GiaScorrOld( Gia_Man_t * p, int nTimeOut, Par_Share_t * pShare, struct Cec_ScorrStop_t_ * pStopOut ); +static Gia_Man_t * Cec_GiaScorrNew( Gia_Man_t * p, int nTimeOut, Par_Share_t * pShare, struct Cec_ScorrStop_t_ * pStopOut ); +static void Cec_GiaInitThreads( Par_ThData_t * ThData, int nWorkers, Gia_Man_t * p, int nTimeOut, int nTimeOutU, Wlc_Ntk_t * pWlc, int fVerbose, pthread_t * WorkerThread, Par_Share_t * pShare, int * pEngines, int StageId, int NetId, struct Cec_SproveTrace_t_ * pTrace ); +static void Cec_GiaStopThreads( Par_ThData_t * ThData, pthread_t * WorkerThread, int nWorkers ); +static int Cec_GiaWaitThreads( Par_ThData_t * ThData, int nWorkers, Gia_Man_t * p, int RetValue, int * pRetEngine ); + extern int Ufar_ProveWithTimeout( Wlc_Ntk_t * pNtk, int nTimeOut, int fVerbose, int (*pFuncStop)(int), int RunId ); #ifndef ABC_USE_PTHREADS -int Cec_GiaProveTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nTimeOut2, int nTimeOut3, int fUseUif, Wlc_Ntk_t * pWlc, int fVerbose, int fVeryVerbose, int fSilent ) { return -1; } +int Cec_GiaProveTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nTimeOut2, int nTimeOut3, int fUseUif, Wlc_Ntk_t * pWlc, int fVerbose, int fVeryVerbose, int fSilent, char * pReplayFile ) { return -1; } +int Cec_GiaReplayReadParams( char * pFileName, int * pnProcs, int * pnTimeOut, int * pnTimeOut2, int * pnTimeOut3, int * pfUseUif ) { return 0; } +int Cec_GiaReplayTest( Gia_Man_t * p, Wlc_Ntk_t * pWlc, char * pFileName, int fVerbose, int fVeryVerbose, int fSilent ) { return -1; } #else // pthreads are used @@ -68,6 +80,13 @@ int Cec_GiaProveTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nTimeOut2, in #define PAR_ENGINE_SCORR1 7 #define PAR_ENGINE_SCORR2 8 #define PAR_ENGINE_GLA 9 +#define SPROVE_STAGE_MAX 4 +#define SPROVE_NET_ORIG 0 +#define SPROVE_NET_SCNEW 1 +#define SPROVE_NET_SCOLD 2 +typedef struct Cec_SproveTrace_t_ Cec_SproveTrace_t; +typedef struct Cec_SproveStage_t_ Cec_SproveStage_t; +typedef struct Cec_SprovePlan_t_ Cec_SprovePlan_t; struct Par_Share_t_ { volatile int fSolved; @@ -85,7 +104,12 @@ typedef struct Par_ThData_t_ int fVerbose; int nTimeOutU; Wlc_Ntk_t * pWlc; + int WorkerId; + int StageId; + int NetId; + int StopReason; Par_Share_t * pShare; + Cec_SproveTrace_t * pTrace; pthread_mutex_t Mutex; pthread_cond_t Cond; } Par_ThData_t; @@ -93,7 +117,44 @@ typedef struct Cec_ScorrStop_t_ { Par_Share_t * pShare; abctime TimeToStop; + int fStoppedByCallback; + int fStoppedByTimeout; } Cec_ScorrStop_t; +struct Cec_SproveTrace_t_ +{ + FILE * pFile; + int fActive; + abctime clkStart; + pthread_mutex_t Mutex; +}; +struct Cec_SproveStage_t_ +{ + int Id; + int fGuardUnsolved; + int GuardExistsNet; + int GuardAndLimitNet; + int GuardAndLimit; + int fHasRound; + int RoundNet; + int RoundTimeout; + int nRoundEngines; + int RoundEngines[PAR_THR_MAX]; + int fHasReduce; + int ReduceType; + int ReduceNetIn; + int ReduceNetOut; + int ReduceTimeout; +}; +struct Cec_SprovePlan_t_ +{ + int nProcs; + int nTimeOut; + int nTimeOut2; + int nTimeOut3; + int fUseUif; + int nStages; + Cec_SproveStage_t Stages[SPROVE_STAGE_MAX]; +}; static volatile Par_Share_t * g_pUfarShare = NULL; static volatile Par_Share_t * g_pGlaShare = NULL; static inline const char * Cec_SolveEngineName( int iEngine ) @@ -146,9 +207,15 @@ static int Cec_ScorrStop( void * pUser ) if ( p == NULL ) return 0; if ( p->pShare && p->pShare->fSolved ) + { + p->fStoppedByCallback = 1; return 1; + } if ( p->TimeToStop && Abc_Clock() >= p->TimeToStop ) + { + p->fStoppedByTimeout = 1; return 1; + } return 0; } static int Cec_SProveCallback( void * pUser, int fSolved, unsigned Result ) @@ -170,6 +237,547 @@ static int Cec_SProveCallback( void * pUser, int fSolved, unsigned Result ) return pShare->fSolved != 0; } +static inline const char * Cec_SproveNetName( int NetId ) +{ + if ( NetId == SPROVE_NET_ORIG ) + return "orig"; + if ( NetId == SPROVE_NET_SCNEW ) + return "scnew"; + if ( NetId == SPROVE_NET_SCOLD ) + return "scold"; + return "unknown"; +} +static inline int Cec_SproveNetId( const char * pName ) +{ + if ( !strcmp(pName, "orig") ) + return SPROVE_NET_ORIG; + if ( !strcmp(pName, "scnew") ) + return SPROVE_NET_SCNEW; + if ( !strcmp(pName, "scold") ) + return SPROVE_NET_SCOLD; + return -1; +} +static inline const char * Cec_SproveStopName( int StopReason ) +{ + if ( StopReason == 1 ) + return "self"; + if ( StopReason == 2 ) + return "callback"; + if ( StopReason == 3 ) + return "timeout"; + if ( StopReason == 4 ) + return "skip"; + return "unknown"; +} +static inline const char * Cec_SproveResultName( int RetValue ) +{ + if ( RetValue == 0 ) + return "sat"; + if ( RetValue == 1 ) + return "unsat"; + return "undecided"; +} +static inline unsigned long long Cec_SproveClockToMs( abctime Time ) +{ + return (unsigned long long)(1000.0 * (double)Time / (double)CLOCKS_PER_SEC); +} +static int Cec_SproveFindValue( char * pLine, const char * pKey, char * pValue, int nValueSize ) +{ + char * pBeg = strstr( pLine, pKey ); + int i = 0; + if ( pBeg == NULL ) + return 0; + pBeg += strlen(pKey); + while ( *pBeg && *pBeg != ' ' && *pBeg != '\t' && *pBeg != '\r' && *pBeg != '\n' ) + { + if ( i < nValueSize - 1 ) + pValue[i++] = *pBeg; + pBeg++; + } + pValue[i] = 0; + return i > 0; +} +static int Cec_SproveParseEngineName( const char * pName ) +{ + int i; + for ( i = 0; i <= PAR_ENGINE_GLA; i++ ) + if ( !strcmp(pName, Cec_SolveEngineName(i)) ) + return i; + return -1; +} +static void Cec_SproveDeriveEngineList( int nProcs, int fUseUif, int * pEngines, int * pnEngines ) +{ + int i, nEngines = nProcs + (fUseUif ? 1 : 0); + assert( nEngines >= 1 && nEngines <= PAR_THR_MAX ); + for ( i = 0; i < nEngines; i++ ) + { + if ( fUseUif && i == nEngines - 1 ) + pEngines[i] = PAR_ENGINE_UFAR; + else if ( !fUseUif && nEngines == 6 && i == 5 ) + pEngines[i] = PAR_ENGINE_GLA; + else + pEngines[i] = i; + } + *pnEngines = nEngines; +} +static void Cec_SprovePlanDefault( Cec_SprovePlan_t * pPlan, int nProcs, int nTimeOut, int nTimeOut2, int nTimeOut3, int fUseUif ) +{ + int nEngines; + memset( pPlan, 0, sizeof(Cec_SprovePlan_t) ); + { + int i; + for ( i = 0; i < SPROVE_STAGE_MAX; i++ ) + pPlan->Stages[i].GuardExistsNet = pPlan->Stages[i].GuardAndLimitNet = -1; + } + pPlan->nProcs = nProcs; + pPlan->nTimeOut = nTimeOut; + pPlan->nTimeOut2 = nTimeOut2; + pPlan->nTimeOut3 = nTimeOut3; + pPlan->fUseUif = fUseUif; + pPlan->nStages = 4; + Cec_SproveDeriveEngineList( nProcs, fUseUif, pPlan->Stages[0].RoundEngines, &nEngines ); + + pPlan->Stages[0].Id = 1; + pPlan->Stages[0].fHasRound = 1; + pPlan->Stages[0].RoundNet = SPROVE_NET_ORIG; + pPlan->Stages[0].RoundTimeout = nTimeOut; + pPlan->Stages[0].nRoundEngines = nEngines; + pPlan->Stages[0].fHasReduce = 1; + pPlan->Stages[0].ReduceType = PAR_ENGINE_SCORR1; + pPlan->Stages[0].ReduceNetIn = SPROVE_NET_ORIG; + pPlan->Stages[0].ReduceNetOut = SPROVE_NET_SCNEW; + pPlan->Stages[0].ReduceTimeout = nTimeOut; + + pPlan->Stages[1].Id = 2; + pPlan->Stages[1].fGuardUnsolved = 1; + pPlan->Stages[1].fHasRound = 1; + pPlan->Stages[1].RoundNet = SPROVE_NET_SCNEW; + pPlan->Stages[1].RoundTimeout = nTimeOut2; + pPlan->Stages[1].nRoundEngines = nEngines; + memcpy( pPlan->Stages[1].RoundEngines, pPlan->Stages[0].RoundEngines, sizeof(int) * nEngines ); + + pPlan->Stages[2].Id = 3; + pPlan->Stages[2].fGuardUnsolved = 1; + pPlan->Stages[2].GuardAndLimitNet = SPROVE_NET_SCNEW; + pPlan->Stages[2].GuardAndLimit = 100000; + pPlan->Stages[2].fHasReduce = 1; + pPlan->Stages[2].ReduceType = PAR_ENGINE_SCORR2; + pPlan->Stages[2].ReduceNetIn = SPROVE_NET_SCNEW; + pPlan->Stages[2].ReduceNetOut = SPROVE_NET_SCOLD; + pPlan->Stages[2].ReduceTimeout = nTimeOut3; + + pPlan->Stages[3].Id = 4; + pPlan->Stages[3].fGuardUnsolved = 1; + pPlan->Stages[3].GuardExistsNet = SPROVE_NET_SCOLD; + pPlan->Stages[3].fHasRound = 1; + pPlan->Stages[3].RoundNet = SPROVE_NET_SCOLD; + pPlan->Stages[3].RoundTimeout = nTimeOut3; + pPlan->Stages[3].nRoundEngines = nEngines; + memcpy( pPlan->Stages[3].RoundEngines, pPlan->Stages[0].RoundEngines, sizeof(int) * nEngines ); +} +static void Cec_SproveTraceWrite( Cec_SproveTrace_t * pTrace, const char * pFormat, ... ) +{ + va_list args; + if ( pTrace == NULL || !pTrace->fActive || pTrace->pFile == NULL ) + return; + pthread_mutex_lock( &pTrace->Mutex ); + va_start( args, pFormat ); + vfprintf( pTrace->pFile, pFormat, args ); + va_end( args ); + fputc( '\n', pTrace->pFile ); + fflush( pTrace->pFile ); + pthread_mutex_unlock( &pTrace->Mutex ); +} +static abctime Cec_SproveTraceTime( Cec_SproveTrace_t * pTrace ) +{ + return pTrace ? Abc_Clock() - pTrace->clkStart : 0; +} +static void Cec_SproveTraceOpen( Cec_SproveTrace_t * pTrace, Gia_Man_t * p, Cec_SprovePlan_t * pPlan, char * pReplayFile ) +{ + int i, k; + char * pProbName = p->pSpec ? p->pSpec : Gia_ManName(p); + memset( pTrace, 0, sizeof(Cec_SproveTrace_t) ); + if ( pReplayFile == NULL ) + return; + pTrace->pFile = fopen( pReplayFile, "wb" ); + if ( pTrace->pFile == NULL ) + return; + pTrace->fActive = 1; + pTrace->clkStart = Abc_Clock(); + pthread_mutex_init( &pTrace->Mutex, NULL ); + Cec_SproveTraceWrite( pTrace, "SPROVE_REPLAY 1" ); + Cec_SproveTraceWrite( pTrace, "CASE %s", pProbName ? pProbName : "(none)" ); + Cec_SproveTraceWrite( pTrace, "PARAMS P=%d T=%d U=%d W=%d UIF=%d", pPlan->nProcs, pPlan->nTimeOut, pPlan->nTimeOut2, pPlan->nTimeOut3, pPlan->fUseUif ); + Cec_SproveTraceWrite( pTrace, "" ); + Cec_SproveTraceWrite( pTrace, "PLAN_BEGIN" ); + for ( i = 0; i < pPlan->nStages; i++ ) + { + Cec_SproveStage_t * pStage = &pPlan->Stages[i]; + char Buffer[256]; + Buffer[0] = 0; + if ( pStage->fGuardUnsolved ) + strcat( Buffer, "unsolved" ); + if ( pStage->GuardExistsNet >= 0 ) + sprintf( Buffer + strlen(Buffer), "%sexists(%s)", Buffer[0] ? "," : "", Cec_SproveNetName(pStage->GuardExistsNet) ); + if ( pStage->GuardAndLimitNet >= 0 ) + sprintf( Buffer + strlen(Buffer), "%sand_lt(%s,%d)", Buffer[0] ? "," : "", Cec_SproveNetName(pStage->GuardAndLimitNet), pStage->GuardAndLimit ); + if ( !Buffer[0] ) + strcpy( Buffer, "none" ); + if ( pStage->fHasRound ) + { + char EngBuf[128]; + EngBuf[0] = 0; + for ( k = 0; k < pStage->nRoundEngines; k++ ) + { + if ( k > 0 ) + strcat( EngBuf, "," ); + strcat( EngBuf, Cec_SolveEngineName(pStage->RoundEngines[k]) ); + } + Cec_SproveTraceWrite( pTrace, "ROUND stage=%d guard=%s net=%s timeout=%d engines=%s", pStage->Id, Buffer, Cec_SproveNetName(pStage->RoundNet), pStage->RoundTimeout, EngBuf ); + } + if ( pStage->fHasReduce ) + Cec_SproveTraceWrite( pTrace, "REDUCE stage=%d guard=%s name=%s in=%s out=%s timeout=%d stop=callback_or_timeout", pStage->Id, Buffer, Cec_SolveEngineName(pStage->ReduceType), Cec_SproveNetName(pStage->ReduceNetIn), Cec_SproveNetName(pStage->ReduceNetOut), pStage->ReduceTimeout ); + } + Cec_SproveTraceWrite( pTrace, "PLAN_END" ); + Cec_SproveTraceWrite( pTrace, "" ); + Cec_SproveTraceWrite( pTrace, "OBSERVED_BEGIN" ); + Cec_SproveTraceWrite( pTrace, "CHECKPOINT net=orig regs=%d ands=%d pos=%d", Gia_ManRegNum(p), Gia_ManAndNum(p), Gia_ManPoNum(p) ); +} +static void Cec_SproveTraceClose( Cec_SproveTrace_t * pTrace ) +{ + if ( pTrace == NULL || !pTrace->fActive ) + return; + Cec_SproveTraceWrite( pTrace, "OBSERVED_END" ); + pthread_mutex_destroy( &pTrace->Mutex ); + fclose( pTrace->pFile ); + pTrace->pFile = NULL; + pTrace->fActive = 0; +} +static int Cec_SproveReplayReadParamsInt( char * pFileName, Cec_SprovePlan_t * pPlan ) +{ + char Buffer[1024], Value[256]; + FILE * pFile = fopen( pFileName, "rb" ); + if ( pFile == NULL ) + return 0; + memset( pPlan, 0, sizeof(Cec_SprovePlan_t) ); + { + int i; + for ( i = 0; i < SPROVE_STAGE_MAX; i++ ) + pPlan->Stages[i].GuardExistsNet = pPlan->Stages[i].GuardAndLimitNet = -1; + } + while ( fgets( Buffer, sizeof(Buffer), pFile ) != NULL ) + { + if ( strncmp(Buffer, "PARAMS ", 7) == 0 ) + { + if ( !Cec_SproveFindValue(Buffer, "P=", Value, sizeof(Value)) ) break; + pPlan->nProcs = atoi(Value); + if ( !Cec_SproveFindValue(Buffer, "T=", Value, sizeof(Value)) ) break; + pPlan->nTimeOut = atoi(Value); + if ( !Cec_SproveFindValue(Buffer, "U=", Value, sizeof(Value)) ) break; + pPlan->nTimeOut2 = atoi(Value); + if ( !Cec_SproveFindValue(Buffer, "W=", Value, sizeof(Value)) ) break; + pPlan->nTimeOut3 = atoi(Value); + if ( !Cec_SproveFindValue(Buffer, "UIF=", Value, sizeof(Value)) ) break; + pPlan->fUseUif = atoi(Value); + fclose( pFile ); + return 1; + } + } + fclose( pFile ); + return 0; +} +static int Cec_SproveReplayReadPlan( char * pFileName, Cec_SprovePlan_t * pPlan ) +{ + char Buffer[1024], Value[256], Guard[256], Engines[256]; + FILE * pFile; + int fInPlan = 0; + if ( !Cec_SproveReplayReadParamsInt( pFileName, pPlan ) ) + return 0; + pFile = fopen( pFileName, "rb" ); + if ( pFile == NULL ) + return 0; + while ( fgets( Buffer, sizeof(Buffer), pFile ) != NULL ) + { + Cec_SproveStage_t * pStage; + int StageId; + if ( strncmp(Buffer, "PLAN_BEGIN", 10) == 0 ) + { + fInPlan = 1; + continue; + } + if ( strncmp(Buffer, "PLAN_END", 8) == 0 || strncmp(Buffer, "OBSERVED_BEGIN", 14) == 0 ) + break; + if ( !fInPlan ) + continue; + if ( strncmp(Buffer, "ROUND ", 6) == 0 ) + { + char * pTok; + int nEngines = 0; + if ( !Cec_SproveFindValue(Buffer, "stage=", Value, sizeof(Value)) ) + continue; + StageId = atoi(Value); + if ( StageId < 1 || StageId > SPROVE_STAGE_MAX ) + continue; + pStage = &pPlan->Stages[StageId - 1]; + if ( StageId > pPlan->nStages ) + pPlan->nStages = StageId; + memset( Guard, 0, sizeof(Guard) ); + Cec_SproveFindValue(Buffer, "guard=", Guard, sizeof(Guard)); + pStage->Id = StageId; + pStage->fGuardUnsolved = strstr( Guard, "unsolved" ) != NULL; + if ( strstr(Guard, "exists(") ) + { + sscanf( strstr(Guard, "exists("), "exists(%255[^)])", Value ); + pStage->GuardExistsNet = Cec_SproveNetId( Value ); + } + if ( strstr(Guard, "and_lt(") ) + { + sscanf( strstr(Guard, "and_lt("), "and_lt(%255[^,],%d)", Value, &pStage->GuardAndLimit ); + pStage->GuardAndLimitNet = Cec_SproveNetId( Value ); + } + if ( Cec_SproveFindValue(Buffer, "net=", Value, sizeof(Value)) ) + pStage->RoundNet = Cec_SproveNetId( Value ); + if ( Cec_SproveFindValue(Buffer, "timeout=", Value, sizeof(Value)) ) + pStage->RoundTimeout = atoi(Value); + if ( Cec_SproveFindValue(Buffer, "engines=", Engines, sizeof(Engines)) ) + { + pTok = strtok( Engines, "," ); + while ( pTok && nEngines < PAR_THR_MAX ) + { + pStage->RoundEngines[nEngines++] = Cec_SproveParseEngineName( pTok ); + pTok = strtok( NULL, "," ); + } + } + pStage->fHasRound = 1; + pStage->nRoundEngines = nEngines; + } + else if ( strncmp(Buffer, "REDUCE ", 7) == 0 ) + { + if ( !Cec_SproveFindValue(Buffer, "stage=", Value, sizeof(Value)) ) + continue; + StageId = atoi(Value); + if ( StageId < 1 || StageId > SPROVE_STAGE_MAX ) + continue; + pStage = &pPlan->Stages[StageId - 1]; + if ( StageId > pPlan->nStages ) + pPlan->nStages = StageId; + memset( Guard, 0, sizeof(Guard) ); + Cec_SproveFindValue(Buffer, "guard=", Guard, sizeof(Guard)); + pStage->Id = StageId; + pStage->fGuardUnsolved = strstr( Guard, "unsolved" ) != NULL; + if ( strstr(Guard, "exists(") ) + { + sscanf( strstr(Guard, "exists("), "exists(%255[^)])", Value ); + pStage->GuardExistsNet = Cec_SproveNetId( Value ); + } + if ( strstr(Guard, "and_lt(") ) + { + sscanf( strstr(Guard, "and_lt("), "and_lt(%255[^,],%d)", Value, &pStage->GuardAndLimit ); + pStage->GuardAndLimitNet = Cec_SproveNetId( Value ); + } + if ( Cec_SproveFindValue(Buffer, "name=", Value, sizeof(Value)) ) + pStage->ReduceType = Cec_SproveParseEngineName( Value ); + if ( Cec_SproveFindValue(Buffer, "in=", Value, sizeof(Value)) ) + pStage->ReduceNetIn = Cec_SproveNetId( Value ); + if ( Cec_SproveFindValue(Buffer, "out=", Value, sizeof(Value)) ) + pStage->ReduceNetOut = Cec_SproveNetId( Value ); + if ( Cec_SproveFindValue(Buffer, "timeout=", Value, sizeof(Value)) ) + pStage->ReduceTimeout = atoi(Value); + pStage->fHasReduce = 1; + } + } + fclose( pFile ); + return pPlan->nStages > 0; +} +static Gia_Man_t * Cec_SproveGetNet( int NetId, Gia_Man_t * pOrig, Gia_Man_t * pScorr, Gia_Man_t * pScorr2 ) +{ + if ( NetId == SPROVE_NET_ORIG ) + return pOrig; + if ( NetId == SPROVE_NET_SCNEW ) + return pScorr; + if ( NetId == SPROVE_NET_SCOLD ) + return pScorr2; + return NULL; +} +static void Cec_SproveSetNet( int NetId, Gia_Man_t ** ppScorr, Gia_Man_t ** ppScorr2, Gia_Man_t * pNet ) +{ + if ( NetId == SPROVE_NET_SCNEW ) + { + Gia_ManStopP( ppScorr ); + *ppScorr = pNet; + } + else if ( NetId == SPROVE_NET_SCOLD ) + { + Gia_ManStopP( ppScorr2 ); + *ppScorr2 = pNet; + } + else + Gia_ManStop( pNet ); +} +static int Cec_SproveCheckGuard( Cec_SproveStage_t * pStage, int RetValue, Gia_Man_t * pOrig, Gia_Man_t * pScorr, Gia_Man_t * pScorr2 ) +{ + Gia_Man_t * pNet; + if ( pStage->fGuardUnsolved && RetValue != -1 ) + return 0; + if ( pStage->GuardExistsNet >= 0 && Cec_SproveGetNet( pStage->GuardExistsNet, pOrig, pScorr, pScorr2 ) == NULL ) + return 0; + if ( pStage->GuardAndLimitNet >= 0 ) + { + pNet = Cec_SproveGetNet( pStage->GuardAndLimitNet, pOrig, pScorr, pScorr2 ); + if ( pNet == NULL || Gia_ManAndNum(pNet) >= pStage->GuardAndLimit ) + return 0; + } + return 1; +} +static void Cec_SproveTraceCheckpoint( Cec_SproveTrace_t * pTrace, int NetId, Gia_Man_t * pNet ) +{ + if ( pTrace == NULL || !pTrace->fActive || pNet == NULL ) + return; + Cec_SproveTraceWrite( pTrace, "CHECKPOINT net=%s regs=%d ands=%d pos=%d", Cec_SproveNetName(NetId), Gia_ManRegNum(pNet), Gia_ManAndNum(pNet), Gia_ManPoNum(pNet) ); +} +static Gia_Man_t * Cec_SproveRunReduce( Gia_Man_t * pInput, Cec_SproveStage_t * pStage, Par_Share_t * pShare, Cec_SproveTrace_t * pTrace, abctime * pClkUsed, int * pRetValue, int * pRetEngine ) +{ + Cec_ScorrStop_t Stop; + abctime clk = Abc_Clock(); + Gia_Man_t * pOutput = NULL; + int StopReason = 1; + memset( &Stop, 0, sizeof(Stop) ); + if ( pTrace && pTrace->fActive ) + Cec_SproveTraceWrite( pTrace, "START kind=reduce stage=%d name=%s in=%s out=%s timeout=%d t=%llu", + pStage->Id, Cec_SolveEngineName(pStage->ReduceType), Cec_SproveNetName(pStage->ReduceNetIn), Cec_SproveNetName(pStage->ReduceNetOut), pStage->ReduceTimeout, + Cec_SproveClockToMs( Cec_SproveTraceTime(pTrace) ) ); + if ( pStage->ReduceType == PAR_ENGINE_SCORR1 ) + pOutput = Cec_GiaScorrNew( pInput, pStage->ReduceTimeout, pShare, &Stop ); + else if ( pStage->ReduceType == PAR_ENGINE_SCORR2 ) + pOutput = Cec_GiaScorrOld( pInput, pStage->ReduceTimeout, pShare, &Stop ); + else + assert( 0 ); + if ( Gia_ManAndNum(pOutput) == 0 ) + { + pShare->fSolved = 1; + pShare->Result = 1; + pShare->iEngine = pStage->ReduceType; + *pRetValue = 1; + *pRetEngine = pStage->ReduceType; + } + if ( Stop.fStoppedByCallback ) + StopReason = 2; + else if ( Stop.fStoppedByTimeout ) + StopReason = 3; + if ( pClkUsed ) + *pClkUsed = Abc_Clock() - clk; + if ( pTrace && pTrace->fActive ) + { + Cec_SproveTraceWrite( pTrace, "STOP kind=reduce stage=%d name=%s in=%s out=%s result=%s stop=%s t=%llu elapsed=%llu", + pStage->Id, Cec_SolveEngineName(pStage->ReduceType), Cec_SproveNetName(pStage->ReduceNetIn), Cec_SproveNetName(pStage->ReduceNetOut), + *pRetEngine == pStage->ReduceType ? Cec_SproveResultName(*pRetValue) : "undecided", + Cec_SproveStopName(StopReason), Cec_SproveClockToMs( Cec_SproveTraceTime(pTrace) ), Cec_SproveClockToMs( Abc_Clock() - clk ) ); + Cec_SproveTraceCheckpoint( pTrace, pStage->ReduceNetOut, pOutput ); + } + return pOutput; +} +static int Cec_SproveExecutePlan( Gia_Man_t * p, Cec_SprovePlan_t * pPlan, Wlc_Ntk_t * pWlc, int fVerbose, int fVeryVerbose, int fSilent, char * pReplayFile ) +{ + abctime clkTotal = Abc_Clock(), clkStage = 0; + Par_ThData_t ThData[PAR_THR_MAX]; + pthread_t WorkerThread[PAR_THR_MAX]; + Par_Share_t Share; + Cec_SproveTrace_t Trace; + Gia_Man_t * pScorr = NULL, * pScorr2 = NULL; + int i, RetValue = -1, RetEngine = -1, fThreadsStarted = 0; + (void)fVeryVerbose; + memset( &Share, 0, sizeof(Par_Share_t) ); + memset( &Trace, 0, sizeof(Cec_SproveTrace_t) ); + memset( ThData, 0, sizeof(ThData) ); + memset( WorkerThread, 0, sizeof(WorkerThread) ); + Abc_CexFreeP( &p->pCexComb ); + Abc_CexFreeP( &p->pCexSeq ); + if ( !fSilent && fVerbose ) + printf( "Solving verification problem with the following parameters:\n" ); + if ( !fSilent && fVerbose ) + printf( "Processes = %d TimeOut = %d sec Verbose = %d.\n", pPlan->nProcs, pPlan->nTimeOut, fVerbose ); + fflush( stdout ); + Cec_SproveTraceOpen( &Trace, p, pPlan, pReplayFile ); + for ( i = 0; i < pPlan->nStages; i++ ) + { + Cec_SproveStage_t * pStage = &pPlan->Stages[i]; + Gia_Man_t * pRoundNet = NULL, * pReduceNet = NULL, * pReduceOut = NULL; + if ( !Cec_SproveCheckGuard( pStage, RetValue, p, pScorr, pScorr2 ) ) + { + Cec_SproveTraceWrite( &Trace, "SKIP stage=%d reason=guard", pStage->Id ); + continue; + } + if ( pStage->fHasRound ) + { + pRoundNet = Cec_SproveGetNet( pStage->RoundNet, p, pScorr, pScorr2 ); + if ( pRoundNet == NULL ) + { + Cec_SproveTraceWrite( &Trace, "SKIP stage=%d reason=missing_round_net", pStage->Id ); + continue; + } + Cec_SproveTraceWrite( &Trace, "START kind=round stage=%d net=%s timeout=%d t=%llu", + pStage->Id, Cec_SproveNetName(pStage->RoundNet), pStage->RoundTimeout, Cec_SproveClockToMs( Cec_SproveTraceTime(&Trace) ) ); + Cec_GiaInitThreads( ThData, pStage->nRoundEngines, pRoundNet, pStage->RoundTimeout, pPlan->nTimeOut3, pWlc, fVerbose, + fThreadsStarted ? NULL : WorkerThread, &Share, pStage->RoundEngines, pStage->Id, pStage->RoundNet, &Trace ); + fThreadsStarted = 1; + } + if ( pStage->fHasReduce ) + { + pReduceNet = Cec_SproveGetNet( pStage->ReduceNetIn, p, pScorr, pScorr2 ); + if ( pReduceNet == NULL ) + Cec_SproveTraceWrite( &Trace, "SKIP stage=%d reason=missing_reduce_net", pStage->Id ); + else + { + pReduceOut = Cec_SproveRunReduce( pReduceNet, pStage, &Share, &Trace, &clkStage, &RetValue, &RetEngine ); + Cec_SproveSetNet( pStage->ReduceNetOut, &pScorr, &pScorr2, pReduceOut ); + } + } + if ( pStage->fHasRound ) + { + RetValue = Cec_GiaWaitThreads( ThData, pStage->nRoundEngines, p, RetValue, &RetEngine ); + Cec_SproveTraceWrite( &Trace, "STOP kind=round stage=%d net=%s result=%s winner=%s t=%llu", + pStage->Id, Cec_SproveNetName(pStage->RoundNet), Cec_SproveResultName(RetValue), + RetEngine >= 0 ? Cec_SolveEngineName(RetEngine) : "none", Cec_SproveClockToMs( Cec_SproveTraceTime(&Trace) ) ); + } + if ( pStage->fHasReduce && RetValue == -1 && !fSilent && fVerbose ) + { + Gia_Man_t * pAfter = Cec_SproveGetNet( pStage->ReduceNetOut, p, pScorr, pScorr2 ); + if ( pAfter ) + { + printf( "Reduced the miter from %d to %d nodes. ", + Gia_ManAndNum(Cec_SproveGetNet(pStage->ReduceNetIn, p, pScorr, pScorr2)), Gia_ManAndNum(pAfter) ); + Abc_PrintTime( 1, "Time", clkStage ); + } + } + } + if ( fThreadsStarted ) + Cec_GiaStopThreads( ThData, WorkerThread, pPlan->Stages[0].nRoundEngines > 0 ? pPlan->Stages[0].nRoundEngines : pPlan->nProcs + (pPlan->fUseUif ? 1 : 0) ); + Gia_ManStopP( &pScorr2 ); + Gia_ManStopP( &pScorr ); + 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 %s).", Cec_SolveEngineName(RetEngine) ); + else if ( RetValue == 1 ) + printf( "UNSATISFIABLE (solved by %s).", Cec_SolveEngineName(RetEngine) ); + else if ( RetValue == -1 ) + printf( "UNDECIDED." ); + else assert( 0 ); + printf( " " ); + Abc_PrintTime( 1, "Time", Abc_Clock() - clkTotal ); + fflush( stdout ); + } + Cec_SproveTraceWrite( &Trace, "FINAL result=%s winner=%s total=%llu", + Cec_SproveResultName(RetValue), RetEngine >= 0 ? Cec_SolveEngineName(RetEngine) : "none", + Cec_SproveClockToMs( Abc_Clock() - clkTotal ) ); + Cec_SproveTraceClose( &Trace ); + return RetValue; +} + //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// @@ -189,10 +797,18 @@ int Cec_GiaProveOne( Gia_Man_t * p, int iEngine, int nTimeOut, int fVerbose, Par { abctime clk = Abc_Clock(); int RetValue = -1; + if ( pThData && pThData->pTrace ) + Cec_SproveTraceWrite( pThData->pTrace, "START kind=engine stage=%d net=%s engine=%s worker=%d timeout=%d t=%llu", + pThData->StageId, Cec_SproveNetName(pThData->NetId), Cec_SolveEngineName(iEngine), pThData->WorkerId, nTimeOut, + Cec_SproveClockToMs( Cec_SproveTraceTime(pThData->pTrace) ) ); if ( iEngine != PAR_ENGINE_UFAR && iEngine != PAR_ENGINE_GLA && Gia_ManRegNum(p) == 0 ) { if ( fVerbose ) printf( "Engine %d (%-5s) skipped because the current miter is combinational.\n", iEngine, Cec_SolveEngineName(iEngine) ); + if ( pThData && pThData->pTrace ) + Cec_SproveTraceWrite( pThData->pTrace, "STOP kind=engine stage=%d net=%s engine=%s worker=%d result=undecided stop=skip t=%llu", + pThData->StageId, Cec_SproveNetName(pThData->NetId), Cec_SolveEngineName(iEngine), pThData->WorkerId, + Cec_SproveClockToMs( Cec_SproveTraceTime(pThData->pTrace) ) ); return -1; } //abctime clkStop = nTimeOut * CLOCKS_PER_SEC + Abc_Clock(); @@ -326,19 +942,39 @@ int Cec_GiaProveOne( Gia_Man_t * p, int iEngine, int nTimeOut, int fVerbose, Par //while ( Abc_Clock() < clkStop ); if ( pThData && pThData->pShare && RetValue != -1 ) Cec_SProveCallback( (void *)pThData, 1, (unsigned)RetValue ); + if ( pThData ) + { + if ( RetValue != -1 ) + pThData->StopReason = 1; + else if ( pThData->pShare && pThData->pShare->fSolved ) + pThData->StopReason = 2; + else + pThData->StopReason = 3; + } + if ( pThData && pThData->pTrace ) + Cec_SproveTraceWrite( pThData->pTrace, "STOP kind=engine stage=%d net=%s engine=%s worker=%d result=%s stop=%s t=%llu elapsed=%llu", + pThData->StageId, Cec_SproveNetName(pThData->NetId), Cec_SolveEngineName(iEngine), pThData->WorkerId, + Cec_SproveResultName(RetValue), Cec_SproveStopName(pThData->StopReason), + Cec_SproveClockToMs( Cec_SproveTraceTime(pThData->pTrace) ), + Cec_SproveClockToMs( Abc_Clock() - clk ) ); if ( fVerbose ) { printf( "Engine %d (%-5s) finished and %ssolved the problem. ", iEngine, Cec_SolveEngineName(iEngine), RetValue != -1 ? " " : "not " ); Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); } return RetValue; } -Gia_Man_t * Cec_GiaScorrOld( Gia_Man_t * p, int nTimeOut, Par_Share_t * pShare ) +Gia_Man_t * Cec_GiaScorrOld( Gia_Man_t * p, int nTimeOut, Par_Share_t * pShare, Cec_ScorrStop_t * pStopOut ) { Cec_ScorrStop_t Stop; + memset( &Stop, 0, sizeof(Stop) ); Stop.pShare = pShare; Stop.TimeToStop = nTimeOut > 0 ? (abctime)(Abc_Clock() + (abctime)nTimeOut * CLOCKS_PER_SEC) : 0; if ( Gia_ManRegNum(p) == 0 ) + { + if ( pStopOut ) + *pStopOut = Stop; return Gia_ManDup( p ); + } Ssw_Pars_t Pars, * pPars = &Pars; Ssw_ManSetDefaultParams( pPars ); pPars->pFunc = (void *)Cec_ScorrStop; @@ -348,15 +984,22 @@ Gia_Man_t * Cec_GiaScorrOld( Gia_Man_t * p, int nTimeOut, Par_Share_t * pShare ) Gia_Man_t * pGia2 = Gia_ManFromAigSimple( pAig2 ); Aig_ManStop( pAig2 ); Aig_ManStop( pAig ); + if ( pStopOut ) + *pStopOut = Stop; return pGia2; } -Gia_Man_t * Cec_GiaScorrNew( Gia_Man_t * p, int nTimeOut, Par_Share_t * pShare ) +Gia_Man_t * Cec_GiaScorrNew( Gia_Man_t * p, int nTimeOut, Par_Share_t * pShare, Cec_ScorrStop_t * pStopOut ) { Cec_ScorrStop_t Stop; + memset( &Stop, 0, sizeof(Stop) ); Stop.pShare = pShare; Stop.TimeToStop = nTimeOut > 0 ? (abctime)(Abc_Clock() + (abctime)nTimeOut * CLOCKS_PER_SEC) : 0; if ( Gia_ManRegNum(p) == 0 ) + { + if ( pStopOut ) + *pStopOut = Stop; return Gia_ManDup( p ); + } Cec_ParCor_t Pars, * pPars = &Pars; Cec_ManCorSetDefaultParams( pPars ); pPars->nBTLimit = 100; @@ -365,7 +1008,10 @@ Gia_Man_t * Cec_GiaScorrNew( Gia_Man_t * p, int nTimeOut, Par_Share_t * pShare ) pPars->fUseCSat = 1; pPars->pFunc = (void *)Cec_ScorrStop; pPars->pData = (void *)&Stop; - return Cec_ManLSCorrespondence( p, pPars ); + p = Cec_ManLSCorrespondence( p, pPars ); + if ( pStopOut ) + *pStopOut = Stop; + return p; } /**Function************************************************************* @@ -424,7 +1070,7 @@ static void Cec_GiaStartThreads( Par_ThData_t * ThData, int nWorkers ) assert( status == 0 ); } } -static void Cec_GiaInitThreads( Par_ThData_t * ThData, int nWorkers, Gia_Man_t * p, int nTimeOut, int nTimeOutU, Wlc_Ntk_t * pWlc, int fUseUif, int fVerbose, pthread_t * WorkerThread, Par_Share_t * pShare ) +static void Cec_GiaInitThreads( Par_ThData_t * ThData, int nWorkers, Gia_Man_t * p, int nTimeOut, int nTimeOutU, Wlc_Ntk_t * pWlc, int fVerbose, pthread_t * WorkerThread, Par_Share_t * pShare, int * pEngines, int StageId, int NetId, Cec_SproveTrace_t * pTrace ) { int i, status; assert( nWorkers <= PAR_THR_MAX ); @@ -434,12 +1080,7 @@ static void Cec_GiaInitThreads( Par_ThData_t * ThData, int nWorkers, Gia_Man_t * { ThData[i].p = Gia_ManDup( p ); Cec_CopyGiaName( p, ThData[i].p ); - 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].iEngine = pEngines[i]; ThData[i].fWorking = 0; ThData[i].fStop = 0; ThData[i].nTimeOut = nTimeOut; @@ -447,7 +1088,12 @@ static void Cec_GiaInitThreads( Par_ThData_t * ThData, int nWorkers, Gia_Man_t * ThData[i].fVerbose = fVerbose; ThData[i].nTimeOutU= nTimeOutU; ThData[i].pWlc = pWlc; + ThData[i].WorkerId = i; + ThData[i].StageId = StageId; + ThData[i].NetId = NetId; + ThData[i].StopReason = 0; ThData[i].pShare = pShare; + ThData[i].pTrace = pTrace; status = pthread_mutex_init( &ThData[i].Mutex, NULL ); assert( status == 0 ); status = pthread_cond_init( &ThData[i].Cond, NULL ); @@ -463,18 +1109,18 @@ static void Cec_GiaInitThreads( Par_ThData_t * ThData, int nWorkers, Gia_Man_t * Gia_ManStopP( &ThData[i].p ); ThData[i].p = Gia_ManDup( p ); Cec_CopyGiaName( p, ThData[i].p ); - 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].iEngine = pEngines[i]; ThData[i].nTimeOut = nTimeOut; ThData[i].Result = -1; ThData[i].fVerbose = fVerbose; ThData[i].nTimeOutU= nTimeOutU; ThData[i].pWlc = pWlc; + ThData[i].WorkerId = i; + ThData[i].StageId = StageId; + ThData[i].NetId = NetId; + ThData[i].StopReason = 0; ThData[i].pShare = pShare; + ThData[i].pTrace = pTrace; status = pthread_mutex_unlock( &ThData[i].Mutex ); assert( status == 0 ); } @@ -527,99 +1173,37 @@ static int Cec_GiaWaitThreads( Par_ThData_t * ThData, int nWorkers, Gia_Man_t * return RetValue; } -int Cec_GiaProveTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nTimeOut2, int nTimeOut3, int fUseUif, Wlc_Ntk_t * pWlc, int fVerbose, int fVeryVerbose, int fSilent ) +int Cec_GiaReplayReadParams( char * pFileName, int * pnProcs, int * pnTimeOut, int * pnTimeOut2, int * pnTimeOut3, int * pfUseUif ) { - abctime clkScorr = 0, clkTotal = Abc_Clock(); - Par_ThData_t ThData[PAR_THR_MAX]; - pthread_t WorkerThread[PAR_THR_MAX]; - Par_Share_t Share; - int nWorkers = nProcs + (fUseUif ? 1 : 0), RetValue = -1, RetEngine = -1; - memset( &Share, 0, sizeof(Par_Share_t) ); - memset( ThData, 0, sizeof(ThData) ); - memset( WorkerThread, 0, sizeof(WorkerThread) ); - Abc_CexFreeP( &p->pCexComb ); - Abc_CexFreeP( &p->pCexSeq ); - if ( !fSilent && fVerbose ) - printf( "Solving verification problem with the following parameters:\n" ); - if ( !fSilent && fVerbose ) - printf( "Processes = %d TimeOut = %d sec Verbose = %d.\n", nProcs, nTimeOut, fVerbose ); - fflush( stdout ); - + Cec_SprovePlan_t Plan; + if ( !Cec_SproveReplayReadParamsInt( pFileName, &Plan ) ) + return 0; + if ( pnProcs ) + *pnProcs = Plan.nProcs; + if ( pnTimeOut ) + *pnTimeOut = Plan.nTimeOut; + if ( pnTimeOut2 ) + *pnTimeOut2 = Plan.nTimeOut2; + if ( pnTimeOut3 ) + *pnTimeOut3 = Plan.nTimeOut3; + if ( pfUseUif ) + *pfUseUif = Plan.fUseUif; + return 1; +} +int Cec_GiaProveTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nTimeOut2, int nTimeOut3, int fUseUif, Wlc_Ntk_t * pWlc, int fVerbose, int fVeryVerbose, int fSilent, char * pReplayFile ) +{ + Cec_SprovePlan_t Plan; + Cec_SprovePlanDefault( &Plan, nProcs, nTimeOut, nTimeOut2, nTimeOut3, fUseUif ); assert( nProcs >= 1 && nProcs <= 6 ); - assert( nWorkers <= PAR_THR_MAX ); - Cec_GiaInitThreads( ThData, nWorkers, p, nTimeOut, nTimeOut3, pWlc, fUseUif, fVerbose, WorkerThread, &Share ); - - // meanwhile, perform scorr - Gia_Man_t * pScorr = Cec_GiaScorrNew( p, nTimeOut, &Share ); - clkScorr = Abc_Clock() - clkTotal; - if ( Gia_ManAndNum(pScorr) == 0 ) - { - Share.fSolved = 1; - Share.Result = 1; - Share.iEngine = PAR_ENGINE_SCORR1; - RetValue = 1, RetEngine = PAR_ENGINE_SCORR1; - } - - RetValue = Cec_GiaWaitThreads( ThData, nWorkers, p, RetValue, &RetEngine ); - if ( RetValue == -1 ) - { - abctime clkScorr2, clkStart = Abc_Clock(); - if ( !fSilent && fVerbose ) { - printf( "Reduced the miter from %d to %d nodes. ", Gia_ManAndNum(p), Gia_ManAndNum(pScorr) ); - Abc_PrintTime( 1, "Time", clkScorr ); - } - Cec_GiaInitThreads( ThData, nWorkers, pScorr, nTimeOut2, nTimeOut3, pWlc, fUseUif, fVerbose, NULL, &Share ); - - RetValue = Cec_GiaWaitThreads( ThData, nWorkers, p, RetValue, &RetEngine ); - if ( RetValue == -1 && Gia_ManAndNum(pScorr) < 100000 ) - { - // 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 ) - { - Share.fSolved = 1; - Share.Result = 1; - Share.iEngine = PAR_ENGINE_SCORR2; - RetValue = 1, RetEngine = PAR_ENGINE_SCORR2; - } - - if ( RetValue == -1 ) - { - if ( !fSilent && fVerbose ) { - printf( "Reduced the miter from %d to %d nodes. ", Gia_ManAndNum(pScorr), Gia_ManAndNum(pScorr2) ); - Abc_PrintTime( 1, "Time", clkScorr2 ); - } - Cec_GiaInitThreads( ThData, nWorkers, pScorr2, nTimeOut3, nTimeOut3, pWlc, fUseUif, fVerbose, NULL, &Share ); - - RetValue = Cec_GiaWaitThreads( ThData, nWorkers, p, RetValue, &RetEngine ); - // do something else - } - Gia_ManStop( pScorr2 ); - } - } - Gia_ManStop( pScorr ); - - // stop threads - Cec_GiaStopThreads( ThData, WorkerThread, nWorkers ); - 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 %s).", Cec_SolveEngineName(RetEngine) ); - else if ( RetValue == 1 ) - printf( "UNSATISFIABLE (solved by %s).", Cec_SolveEngineName(RetEngine) ); - else if ( RetValue == -1 ) - printf( "UNDECIDED." ); - else assert( 0 ); - printf( " " ); - Abc_PrintTime( 1, "Time", Abc_Clock() - clkTotal ); - fflush( stdout ); - } - return RetValue; + assert( nProcs + (fUseUif ? 1 : 0) <= PAR_THR_MAX ); + return Cec_SproveExecutePlan( p, &Plan, pWlc, fVerbose, fVeryVerbose, fSilent, pReplayFile ); +} +int Cec_GiaReplayTest( Gia_Man_t * p, Wlc_Ntk_t * pWlc, char * pFileName, int fVerbose, int fVeryVerbose, int fSilent ) +{ + Cec_SprovePlan_t Plan; + if ( !Cec_SproveReplayReadPlan( pFileName, &Plan ) ) + return -1; + return Cec_SproveExecutePlan( p, &Plan, pWlc, fVerbose, fVeryVerbose, fSilent, NULL ); } #endif // pthreads are used