diff options
| -rw-r--r-- | src/base/abci/abc.c | 15 | ||||
| -rw-r--r-- | src/misc/util/utilCex.c | 5 | ||||
| -rw-r--r-- | src/sat/bmc/bmc.h | 1 | ||||
| -rw-r--r-- | src/sat/bmc/bmcBmc3.c | 2 | ||||
| -rw-r--r-- | src/sat/bmc/bmcMulti.c | 32 |
5 files changed, 51 insertions, 4 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 69e8ed84..d94adf08 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -32439,8 +32439,9 @@ int Abc_CommandAbc9MultiProve( Abc_Frame_t * pAbc, int argc, char ** argv ) pPars->TimeOutGlo = 30; pPars->TimeOutLoc = 2; pPars->TimeOutInc = 100; + pPars->TimePerOut = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "TLMsdvwh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "TLMHsdvwh" ) ) != EOF ) { switch ( c ) { @@ -32477,6 +32478,17 @@ int Abc_CommandAbc9MultiProve( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( pPars->TimeOutInc <= 0 ) goto usage; break; + case 'H': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-M\" should be followed by an integer.\n" ); + goto usage; + } + pPars->TimePerOut = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->TimePerOut <= 0 ) + goto usage; + break; case 's': pPars->fUseSyn ^= 1; break; @@ -32512,6 +32524,7 @@ usage: 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-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" ); Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" ); diff --git a/src/misc/util/utilCex.c b/src/misc/util/utilCex.c index b0ce66be..1399f55d 100644 --- a/src/misc/util/utilCex.c +++ b/src/misc/util/utilCex.c @@ -351,7 +351,10 @@ void Abc_CexFreeP( Abc_Cex_t ** p ) { if ( *p == NULL ) return; - ABC_FREE( *p ); + if ( *p == (Abc_Cex_t *)(ABC_PTRINT_T)1 ) + *p = NULL; + else + ABC_FREE( *p ); } /**Function************************************************************* diff --git a/src/sat/bmc/bmc.h b/src/sat/bmc/bmc.h index 5d45c562..74128047 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 TimePerOut; int fUseSyn; int fDumpFinal; int fVerbose; diff --git a/src/sat/bmc/bmcBmc3.c b/src/sat/bmc/bmcBmc3.c index 28b89f7b..72fbcc21 100644 --- a/src/sat/bmc/bmcBmc3.c +++ b/src/sat/bmc/bmcBmc3.c @@ -1649,7 +1649,7 @@ nTimeSat += Abc_Clock() - clk2; Vec_PtrWriteEntry( p->vCexes, k, Abc_CexDup(pCexNew, Saig_ManRegNum(pAig)) ); } Abc_CexFreeP( &pCexNew0 ); - Abc_CexFreeP( &pCexNew ); + Abc_CexFree( pCexNew ); } else { diff --git a/src/sat/bmc/bmcMulti.c b/src/sat/bmc/bmcMulti.c index 699835ca..1968b5a8 100644 --- a/src/sat/bmc/bmcMulti.c +++ b/src/sat/bmc/bmcMulti.c @@ -75,6 +75,34 @@ Vec_Int_t * Gia_ManProcessOutputs( Vec_Ptr_t * vCexesIn, Vec_Ptr_t * vCexesOut, /**Function************************************************************* + Synopsis [Counts the number of constant 0 POs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Gia_ManCountConst0PosGia( Gia_Man_t * p ) +{ + Gia_Obj_t * pObj; + int i, Counter = 0; + Gia_ManForEachPo( p, pObj, i ) + Counter += (Gia_ObjFaninLit0p(p, pObj) == 0); + return Counter; +} +int Gia_ManCountConst0Pos( Aig_Man_t * p ) +{ + Aig_Obj_t * pObj; + int i, Counter = 0; + Saig_ManForEachPo( p, pObj, i ) + Counter += (Aig_ObjChild0(pObj) == Aig_ManConst0(p)); + return Counter; +} + +/**Function************************************************************* + Synopsis [] Description [] @@ -186,7 +214,7 @@ Vec_Ptr_t * Gia_ManMultiProveAig( Aig_Man_t * p, Bmc_MulPar_t * pPars ) pParsBmc->fNotVerbose = 1; pParsBmc->fSilent = !pPars->fVeryVerbose; pParsBmc->nTimeOut = TimeOutLoc; - pParsBmc->nTimeOutOne = 100; + pParsBmc->nTimeOutOne = pPars->TimePerOut; RetValue *= Saig_ManBmcScalable( p, pParsBmc ); if ( pPars->fVeryVerbose ) Abc_Print( 1, "Some outputs are SAT (%d out of %d) after %d frames.\n", @@ -225,6 +253,8 @@ Vec_Ptr_t * Gia_ManMultiProveAig( Aig_Man_t * p, Bmc_MulPar_t * pPars ) TimeOutLoc += TimeOutLoc * pPars->TimeOutInc / 100; } Vec_IntFree( vOutMap ); + if ( pPars->fVerbose ) + printf( "The number of const0 POs = %d.\n", Gia_ManCountConst0Pos(p) ); if ( pPars->fDumpFinal ) { char * pFileName = Extra_FileNameGenericAppend( p->pName, "_out.aig" ); |