From 01ad71b26f983b61ea0faae7eacb2cc60a285793 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Mon, 23 Oct 2023 09:38:08 -0700 Subject: [PATCH] Experiments with verification. --- src/base/abci/abc.c | 34 +++++- src/base/io/ioUtil.c | 2 +- src/proof/cec/cecProve.c | 216 +++++++++++++++++++++++++++++++-------- 3 files changed, 204 insertions(+), 48 deletions(-) diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index f93d03ff0..0558eefa4 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -46383,10 +46383,10 @@ usage: ***********************************************************************/ int Abc_CommandAbc9SProve( Abc_Frame_t * pAbc, int argc, char ** argv ) { - extern int Cec_GiaProveTest( Gia_Man_t * p, int nProcs, int nTimeOut, int fVerbose, int fVeryVerbose, int fSilent ); - int c, nProcs = 5, nTimeOut = 3, fVerbose = 0, fVeryVerbose = 0, fSilent = 0; + extern int Cec_GiaProveTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nTimeOut2, int nTimeOut3, int fVerbose, int fVeryVerbose, int fSilent ); + int c, nProcs = 5, nTimeOut = 3, nTimeOut2 = 10, nTimeOut3 = 100, fVerbose = 0, fVeryVerbose = 0, fSilent = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "PTsvwh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "PTUWsvwh" ) ) != EOF ) { switch ( c ) { @@ -46412,6 +46412,28 @@ int Abc_CommandAbc9SProve( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( nTimeOut <= 0 ) goto usage; break; + case 'U': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-U\" should be followed by a positive integer.\n" ); + goto usage; + } + nTimeOut2 = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nTimeOut2 <= 0 ) + goto usage; + break; + case 'W': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-W\" should be followed by a positive integer.\n" ); + goto usage; + } + nTimeOut3 = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nTimeOut3 <= 0 ) + goto usage; + break; case 's': fSilent ^= 1; break; @@ -46437,15 +46459,17 @@ int Abc_CommandAbc9SProve( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( -1, "Abc_CommandAbc9SProve(): The problem is combinational.\n" ); return 1; } - pAbc->Status = Cec_GiaProveTest( pAbc->pGia, nProcs, nTimeOut, fVerbose, fVeryVerbose, fSilent ); + pAbc->Status = Cec_GiaProveTest( pAbc->pGia, nProcs, nTimeOut, nTimeOut2, nTimeOut3, fVerbose, fVeryVerbose, fSilent ); Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexSeq ); return 0; usage: - Abc_Print( -2, "usage: &sprove [-PT num] [-svwh]\n" ); + Abc_Print( -2, "usage: &sprove [-PTUW num] [-svwh]\n" ); Abc_Print( -2, "\t proves CEC problem by case-splitting\n" ); Abc_Print( -2, "\t-P num : the number of concurrent processes [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-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" ); diff --git a/src/base/io/ioUtil.c b/src/base/io/ioUtil.c index e57fa9574..d11ee7408 100644 --- a/src/base/io/ioUtil.c +++ b/src/base/io/ioUtil.c @@ -944,7 +944,7 @@ char * Io_ConvertNumsToSop( Vec_Wec_t * vNums, int nVars ) Vec_IntForEachEntry( vLevel, Num, k ) pCube[Abc_Lit2Var(Num)] = '0' + Abc_LitIsCompl(Num); pCube[nVars+0] = ' '; - pCube[nVars+1] = '1'; + pCube[nVars+1] = '0'; pCube[nVars+2] = '\n'; } return pStr; diff --git a/src/proof/cec/cecProve.c b/src/proof/cec/cecProve.c index 748f506f9..b3ddcd8a1 100644 --- a/src/proof/cec/cecProve.c +++ b/src/proof/cec/cecProve.c @@ -22,6 +22,11 @@ #include "aig/gia/gia.h" #include "aig/gia/giaAig.h" +#include "sat/bmc/bmc.h" +#include "proof/pdr/pdr.h" +#include "proof/cec/cec.h" +#include "proof/ssw/ssw.h" + #ifdef ABC_USE_PTHREADS @@ -41,9 +46,12 @@ ABC_NAMESPACE_IMPL_START /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// +extern int Ssw_RarSimulateGia( Gia_Man_t * p, Ssw_RarPars_t * pPars ); +extern int Bmcg_ManPerform( Gia_Man_t * pGia, Bmc_AndPar_t * pPars ); + #ifndef ABC_USE_PTHREADS -int Cec_GiaProveTest( Gia_Man_t * p, int nProcs, int nTimeOut, int fVerbose, int fVeryVerbose, int fSilent ) { return -1; } +int Cec_GiaProveTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nTimeOut2, int nTimeOut3, int fVerbose, int fVeryVerbose, int fSilent ) { return -1; } #else // pthreads are used @@ -62,28 +70,106 @@ int Cec_GiaProveTest( Gia_Man_t * p, int nProcs, int nTimeOut, int fVerbose, int SeeAlso [] ***********************************************************************/ -int Cec_GiaProveOne( Gia_Man_t * p, int iEngine, int nTimeOut, Abc_Cex_t ** ppCex ) +int Cec_GiaProveOne( Gia_Man_t * p, int iEngine, int nTimeOut, int fVerbose ) { - abctime clk = Abc_Clock(); + abctime clk = Abc_Clock(); + int RetValue = -1; //abctime clkStop = nTimeOut * CLOCKS_PER_SEC + Abc_Clock(); + if ( fVerbose ) printf( "Calling engine %d with timeout %d sec.\n", iEngine, nTimeOut ); + Abc_CexFreeP( &p->pCexSeq ); if ( iEngine == 0 ) { + Ssw_RarPars_t Pars, * pPars = &Pars; + Ssw_RarSetDefaultParams( pPars ); + pPars->TimeOut = nTimeOut; + pPars->fSilent = 1; + RetValue = Ssw_RarSimulateGia( p, pPars ); } else if ( iEngine == 1 ) { - } + Saig_ParBmc_t Pars, * pPars = &Pars; + Saig_ParBmcSetDefaultParams( pPars ); + pPars->nTimeOut = nTimeOut; + pPars->fSilent = 1; + Aig_Man_t * pAig = Gia_ManToAigSimple( p ); + RetValue = Saig_ManBmcScalable( pAig, pPars ); + p->pCexSeq = pAig->pSeqModel; pAig->pSeqModel = NULL; + Aig_ManStop( pAig ); + } else if ( iEngine == 2 ) { - } + Pdr_Par_t Pars, * pPars = &Pars; + Pdr_ManSetDefaultParams( pPars ); + pPars->nTimeOut = nTimeOut; + pPars->fSilent = 1; + Aig_Man_t * pAig = Gia_ManToAigSimple( p ); + RetValue = Pdr_ManSolve( pAig, pPars ); + p->pCexSeq = pAig->pSeqModel; pAig->pSeqModel = NULL; + Aig_ManStop( pAig ); + } else if ( iEngine == 3 ) { + Saig_ParBmc_t Pars, * pPars = &Pars; + Saig_ParBmcSetDefaultParams( pPars ); + pPars->fUseGlucose = 1; + pPars->nTimeOut = nTimeOut; + pPars->fSilent = 1; + Aig_Man_t * pAig = Gia_ManToAigSimple( p ); + RetValue = Saig_ManBmcScalable( pAig, pPars ); + p->pCexSeq = pAig->pSeqModel; pAig->pSeqModel = NULL; + Aig_ManStop( pAig ); + } + else if ( iEngine == 4 ) + { + Pdr_Par_t Pars, * pPars = &Pars; + Pdr_ManSetDefaultParams( pPars ); + pPars->fUseAbs = 1; + pPars->nTimeOut = nTimeOut; + pPars->fSilent = 1; + Aig_Man_t * pAig = Gia_ManToAigSimple( p ); + RetValue = Pdr_ManSolve( pAig, pPars ); + p->pCexSeq = pAig->pSeqModel; pAig->pSeqModel = NULL; + Aig_ManStop( pAig ); + } + else if ( iEngine == 5 ) + { + Bmc_AndPar_t Pars, * pPars = &Pars; + memset( pPars, 0, sizeof(Bmc_AndPar_t) ); + pPars->nProcs = 1; // the number of parallel solvers + pPars->nFramesAdd = 1; // the number of additional frames + pPars->fNotVerbose = 1; // silent + pPars->nTimeOut = nTimeOut; // timeout in seconds + RetValue = Bmcg_ManPerform( p, pPars ); } else assert( 0 ); //while ( Abc_Clock() < clkStop ); - printf( "Engine %d finished. ", iEngine ); - Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); - return 0; + if ( fVerbose ) { + printf( "Engine %d finished and %ssolved the problem. ", iEngine, RetValue != -1 ? " " : "not " ); + Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); + } + return RetValue; +} +Gia_Man_t * Cec_GiaScorrOld( Gia_Man_t * p ) +{ + Ssw_Pars_t Pars, * pPars = &Pars; + Ssw_ManSetDefaultParams( pPars ); + Aig_Man_t * pAig = Gia_ManToAigSimple( p ); + Aig_Man_t * pAig2 = Ssw_SignalCorrespondence( pAig, pPars ); + Gia_Man_t * pGia2 = Gia_ManFromAigSimple( pAig2 ); + Aig_ManStop( pAig2 ); + Aig_ManStop( pAig ); + return pGia2; +} +Gia_Man_t * Cec_GiaScorrNew( Gia_Man_t * p ) +{ + Cec_ParCor_t Pars, * pPars = &Pars; + Cec_ManCorSetDefaultParams( pPars ); + pPars->nBTLimit = 100; + pPars->nLevelMax = 100; + pPars->fVerbose = 0; + pPars->fUseCSat = 1; + return Cec_ManLSCorrespondence( p, pPars ); } /**Function************************************************************* @@ -101,11 +187,11 @@ int Cec_GiaProveOne( Gia_Man_t * p, int iEngine, int nTimeOut, Abc_Cex_t ** ppCe typedef struct Par_ThData_t_ { Gia_Man_t * p; - Abc_Cex_t * pCex; int iEngine; int fWorking; int nTimeOut; int Result; + int fVerbose; } Par_ThData_t; void * Cec_GiaProveWorkerThread( void * pArg ) { @@ -121,73 +207,119 @@ void * Cec_GiaProveWorkerThread( void * pArg ) assert( 0 ); return NULL; } - pThData->Result = Cec_GiaProveOne( pThData->p, pThData->iEngine, pThData->nTimeOut, &pThData->pCex ); + pThData->Result = Cec_GiaProveOne( pThData->p, pThData->iEngine, pThData->nTimeOut, pThData->fVerbose ); pThData->fWorking = 0; } assert( 0 ); return NULL; } -int Cec_GiaProveTest( Gia_Man_t * p, int nProcs, int nTimeOut, int fVerbose, int fVeryVerbose, int fSilent ) +void Cec_GiaInitThreads( Par_ThData_t * ThData, int nProcs, Gia_Man_t * p, int nTimeOut, int fVerbose, pthread_t * WorkerThread ) { - abctime clkTotal = Abc_Clock(); - Par_ThData_t ThData[PAR_THR_MAX]; - pthread_t WorkerThread[PAR_THR_MAX]; - int i, status, RetValue = -1; - Abc_CexFreeP( &p->pCexComb ); - Abc_CexFreeP( &p->pCexSeq ); - if ( fVerbose ) - printf( "Solving verification problem with the following parameters:\n" ); - if ( fVerbose ) - printf( "Processes = %d TimeOut = %d sec Verbose = %d.\n", nProcs, nTimeOut, fVerbose ); - fflush( stdout ); - if ( nProcs == 1 ) - return -1; - // subtract manager thread - nProcs--; - assert( (nProcs == 4 || nProcs == 8) && nProcs <= PAR_THR_MAX ); - // start threads + int i, status; + assert( nProcs <= PAR_THR_MAX ); for ( i = 0; i < nProcs; i++ ) { ThData[i].p = Gia_ManDup(p); - ThData[i].pCex = NULL; ThData[i].iEngine = i; ThData[i].nTimeOut = nTimeOut; ThData[i].fWorking = 0; ThData[i].Result = -1; + ThData[i].fVerbose = fVerbose; + if ( !WorkerThread ) + continue; status = pthread_create( WorkerThread + i, NULL,Cec_GiaProveWorkerThread, (void *)(ThData + i) ); assert( status == 0 ); } - for ( i = 0; i < nProcs; i++ ) ThData[i].fWorking = 1; - - // wait till threads finish +} +int Cec_GiaWaitThreads( Par_ThData_t * ThData, int nProcs, Gia_Man_t * p, int RetValue, int * pRetEngine ) +{ + int i; for ( i = 0; i < nProcs; i++ ) + { + if ( RetValue == -1 && !ThData[i].fWorking && ThData[i].Result != -1 ) { + RetValue = ThData[i].Result; + *pRetEngine = i; + if ( !p->pCexSeq && ThData[i].p->pCexSeq ) + p->pCexSeq = Abc_CexDup( ThData[i].p->pCexSeq, -1 ); + } if ( ThData[i].fWorking ) i = -1; + } + return RetValue; +} + +int Cec_GiaProveTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nTimeOut2, int nTimeOut3, int fVerbose, int fVeryVerbose, int fSilent ) +{ + abctime clkScorr = 0, clkTotal = Abc_Clock(); + Par_ThData_t ThData[PAR_THR_MAX]; + pthread_t WorkerThread[PAR_THR_MAX]; + int i, RetValue = -1, RetEngine = -2; + 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 ); + + assert( nProcs == 3 || nProcs == 5 ); + Cec_GiaInitThreads( ThData, nProcs, p, nTimeOut, fVerbose, WorkerThread ); + + // meanwhile, perform scorr + Gia_Man_t * pScorr = Cec_GiaScorrNew( p ); + clkScorr = Abc_Clock() - clkTotal; + if ( Gia_ManAndNum(pScorr) == 0 ) + RetValue = 1, RetEngine = -1; + + RetValue = Cec_GiaWaitThreads( ThData, nProcs, 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, nProcs, pScorr, nTimeOut2, fVerbose, NULL ); + + // meanwhile, perform scorr + Gia_Man_t * pScorr2 = Cec_GiaScorrOld( pScorr ); + clkScorr2 = Abc_Clock() - clkStart; + if ( Gia_ManAndNum(pScorr2) == 0 ) + RetValue = 1; + + RetValue = Cec_GiaWaitThreads( ThData, nProcs, p, RetValue, &RetEngine ); + 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, nProcs, pScorr2, nTimeOut3, fVerbose, NULL ); + + RetValue = Cec_GiaWaitThreads( ThData, nProcs, p, RetValue, &RetEngine ); + // do something else + } + Gia_ManStop( pScorr2 ); + } + Gia_ManStop( pScorr ); // stop threads for ( i = 0; i < nProcs; i++ ) { - assert( !ThData[i].fWorking ); - // cleanup - Gia_ManStopP( &ThData[i].p ); - if ( !p->pCexSeq && ThData[i].pCex ) - p->pCexSeq = Abc_CexDup( ThData[i].pCex, -1 ); - Abc_CexFreeP( &ThData[i].pCex ); - // stop ThData[i].p = NULL; ThData[i].fWorking = 1; } if ( !fSilent ) { if ( RetValue == 0 ) - printf( "Problem is SAT " ); + printf( "Problem is SAT (solved by %d) ", RetEngine ); else if ( RetValue == 1 ) - printf( "Problem is UNSAT " ); + printf( "Problem is UNSAT (solved by %d) ", RetEngine ); else if ( RetValue == -1 ) printf( "Problem is UNDECIDED " ); else assert( 0 ); - printf( ". " ); + printf( " " ); Abc_PrintTime( 1, "Time", Abc_Clock() - clkTotal ); fflush( stdout ); }