diff options
| -rw-r--r-- | src/base/abci/abc.c | 17 | ||||
| -rw-r--r-- | src/sat/bmc/bmc.h | 1 | ||||
| -rw-r--r-- | src/sat/bmc/bmcMulti.c | 16 |
3 files changed, 30 insertions, 4 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 7af30b0b..0ac0b7cf 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -32439,9 +32439,10 @@ int Abc_CommandAbc9MultiProve( Abc_Frame_t * pAbc, int argc, char ** argv ) pPars->TimeOutGlo = 30; pPars->TimeOutLoc = 2; pPars->TimeOutInc = 100; + pPars->TimeOutGap = 0; pPars->TimePerOut = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "TLMHsdvwh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "TLMGHsdvwh" ) ) != EOF ) { switch ( c ) { @@ -32478,6 +32479,17 @@ int Abc_CommandAbc9MultiProve( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( pPars->TimeOutInc <= 0 ) goto usage; break; + case 'G': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-G\" should be followed by an integer.\n" ); + goto usage; + } + pPars->TimeOutGap = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->TimeOutGap <= 0 ) + goto usage; + break; case 'H': if ( globalUtilOptind >= argc ) { @@ -32519,11 +32531,12 @@ int Abc_CommandAbc9MultiProve( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: &mprove [-TLMH num] [-sdvwh]\n" ); + Abc_Print( -2, "usage: &mprove [-TLMGH num] [-sdvwh]\n" ); Abc_Print( -2, "\t proves multi-output testcase by applying several engines\n" ); Abc_Print( -2, "\t-T num : approximate global runtime limit in seconds [default = %d]\n", pPars->TimeOutGlo ); Abc_Print( -2, "\t-L num : approximate local runtime limit in seconds [default = %d]\n", pPars->TimeOutLoc ); Abc_Print( -2, "\t-M num : percentage of local runtime limit increase [default = %d]\n", pPars->TimeOutInc ); + Abc_Print( -2, "\t-G num : approximate gap runtime limit in seconds [default = %d]\n", pPars->TimeOutGap ); Abc_Print( -2, "\t-H num : timeout per output in miliseconds [default = %d]\n", pPars->TimePerOut ); Abc_Print( -2, "\t-s : toggle using combinational synthesis [default = %s]\n", pPars->fUseSyn? "yes": "no" ); Abc_Print( -2, "\t-d : toggle dumping invariant into a file [default = %s]\n", pPars->fDumpFinal? "yes": "no" ); diff --git a/src/sat/bmc/bmc.h b/src/sat/bmc/bmc.h index 74128047..0cfc9b37 100644 --- a/src/sat/bmc/bmc.h +++ b/src/sat/bmc/bmc.h @@ -100,6 +100,7 @@ struct Bmc_MulPar_t_ int TimeOutGlo; int TimeOutLoc; int TimeOutInc; + int TimeOutGap; int TimePerOut; int fUseSyn; int fDumpFinal; diff --git a/src/sat/bmc/bmcMulti.c b/src/sat/bmc/bmcMulti.c index a86228df..cf04ab62 100644 --- a/src/sat/bmc/bmcMulti.c +++ b/src/sat/bmc/bmcMulti.c @@ -172,12 +172,17 @@ Vec_Ptr_t * Gia_ManMultiProveAig( Aig_Man_t * p, Bmc_MulPar_t * pPars ) int TimeOutLoc = pPars->TimeOutLoc; int i, RetValue = -1; if ( pPars->fVerbose ) - printf( "MultiProve parameters: Global timeout = %d sec. Local timeout = %d sec. Time increase = %d %%.\n", pPars->TimeOutGlo, pPars->TimeOutLoc, pPars->TimeOutInc ); + printf( "MultiProve parameters: Global timeout = %d sec. Local timeout = %d sec. Time increase = %d %%.\n", + pPars->TimeOutGlo, pPars->TimeOutLoc, pPars->TimeOutInc ); + if ( pPars->fVerbose ) + printf( "Gap timout = %d sec. Per-output timeout = %d msec. Use synthesis = %d. Dump final = %d. Verbose = %d.\n", + pPars->TimeOutGap, pPars->TimePerOut, pPars->fUseSyn, pPars->fDumpFinal, pPars->fVerbose ); // create output map vOutMap = Vec_IntStartNatural( Saig_ManPoNum(p) ); // maps current outputs into their original IDs vCexes = Vec_PtrStart( Saig_ManPoNum(p) ); // maps solved outputs into their CEXes (or markers) for ( i = 0; i < 1000; i++ ) { + int nSolved = Vec_PtrCountZero(vCexes); // perform SIM3 Ssw_RarSetDefaultParams( pParsSim ); pParsSim->fSolveAll = 1; @@ -240,6 +245,13 @@ Vec_Ptr_t * Gia_ManMultiProveAig( Aig_Man_t * p, Bmc_MulPar_t * pPars ) break; } + // check gap timeout + if ( pPars->TimeOutGap && pPars->TimeOutGap <= TimeOutLoc && nSolved == Vec_PtrCountZero(vCexes) ) + { + printf( "Gap timeout (%d sec) is reached.\n", pPars->TimeOutGap ); + break; + } + // synthesize if ( pPars->fUseSyn ) { @@ -254,7 +266,7 @@ Vec_Ptr_t * Gia_ManMultiProveAig( Aig_Man_t * p, Bmc_MulPar_t * pPars ) } Vec_IntFree( vOutMap ); if ( pPars->fVerbose ) - printf( "The number of const0 POs = %d.\n", Gia_ManCountConst0Pos(p) ); + printf( "The number of POs proved UNSAT by synthesis = %d.\n", Gia_ManCountConst0Pos(p) ); if ( pPars->fDumpFinal ) { char * pFileName = Extra_FileNameGenericAppend( p->pName, "_out.aig" ); |