diff options
Diffstat (limited to 'src/base')
| -rw-r--r-- | src/base/abci/abc.c | 16 | ||||
| -rw-r--r-- | src/base/abci/abcDar.c | 6 |
2 files changed, 18 insertions, 4 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 22e018ab..e7fe63e9 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -22321,10 +22321,11 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv ) int c; Pdr_ManSetDefaultParams( pPars ); Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "OMFCRTrmsdgvwh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "MFCRTarmsdgvwh" ) ) != EOF ) { switch ( c ) { +/* case 'O': if ( globalUtilOptind >= argc ) { @@ -22336,6 +22337,7 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( pPars->iOutput < 0 ) goto usage; break; +*/ case 'M': if ( globalUtilOptind >= argc ) { @@ -22391,6 +22393,9 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( pPars->nTimeOut < 0 ) goto usage; break; + case 'a': + pPars->fSolveAll ^= 1; + break; case 'r': pPars->fTwoRounds ^= 1; break; @@ -22432,12 +22437,15 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( -2, "The current network is not an AIG (run \"strash\").\n"); return 0; } +/* if ( pPars->iOutput != -1 && (pPars->iOutput < 0 || pPars->iOutput >= Abc_NtkPoNum(pNtk)) ) { Abc_Print( -2, "Output index (%d) is incorrect (can be 0 through %d).\n", pPars->iOutput, Abc_NtkPoNum(pNtk)-1 ); return 0; } +*/ +/* if ( Abc_NtkPoNum(pNtk) != 1 && pPars->fVerbose ) { if ( pPars->iOutput == -1 ) @@ -22446,6 +22454,7 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( -2, "Working on the primary output with zero-based number %d (out of %d).\n", pPars->iOutput, Abc_NtkPoNum(pNtk) ); } +*/ // run the procedure pAbc->Status = Abc_NtkDarPdr( pNtk, pPars, &pCex ); pAbc->nFrames = pPars->iFrame; @@ -22453,16 +22462,17 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: pdr [-OMFCRT<num] [-rmsdgvwh]\n" ); + Abc_Print( -2, "usage: pdr [-MFCRT<num] [-armsdgvwh]\n" ); Abc_Print( -2, "\t model checking using property directed reachability (aka IC3)\n" ); Abc_Print( -2, "\t pioneered by Aaron Bradley (http://ecee.colorado.edu/~bradleya/ic3/)\n" ); Abc_Print( -2, "\t with improvements by Niklas Een (http://een.se/niklas/)\n" ); - Abc_Print( -2, "\t-O num : the zero-based number of the primary output to solve [default = all]\n" ); +// Abc_Print( -2, "\t-O num : the zero-based number of the primary output to solve [default = all]\n" ); Abc_Print( -2, "\t-M num : limit on unused vars to trigger SAT solver recycling [default = %d]\n", pPars->nRecycle ); Abc_Print( -2, "\t-F num : limit on timeframes explored to stop computation [default = %d]\n", pPars->nFrameMax ); Abc_Print( -2, "\t-C num : limit on conflicts in one SAT call (0 = no limit) [default = %d]\n", pPars->nConfLimit ); Abc_Print( -2, "\t-R num : limit on proof obligations before a restart (0 = no limit) [default = %d]\n", pPars->nRestLimit ); Abc_Print( -2, "\t-T num : approximate timeout in seconds (0 = no limit) [default = %d]\n", pPars->nTimeOut ); + Abc_Print( -2, "\t-a : toggle solving all outputs even if one of them is SAT [default = %s]\n", pPars->fSolveAll? "yes": "no" ); Abc_Print( -2, "\t-r : toggle using more effort in generalization [default = %s]\n", pPars->fTwoRounds? "yes": "no" ); Abc_Print( -2, "\t-m : toggle using monolythic CNF computation [default = %s]\n", pPars->fMonoCnf? "yes": "no" ); Abc_Print( -2, "\t-s : toggle creating only shortest counter-examples [default = %s]\n", pPars->fShortest? "yes": "no" ); diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c index cc703490..e427524a 100644 --- a/src/base/abci/abcDar.c +++ b/src/base/abci/abcDar.c @@ -2717,6 +2717,7 @@ int Abc_NtkDarPdr( Abc_Ntk_t * pNtk, Pdr_Par_t * pPars, Abc_Cex_t ** ppCex ) Abc_Print( 1, "Converting network into AIG has failed.\n" ); return -1; } +/* // perform ORing the primary outputs if ( pPars->iOutput == -1 ) { @@ -2728,6 +2729,9 @@ int Abc_NtkDarPdr( Abc_Ntk_t * pNtk, Pdr_Par_t * pPars, Abc_Cex_t ** ppCex ) } else RetValue = Pdr_ManSolve( pMan, pPars, ppCex ); +*/ + RetValue = Pdr_ManSolve( pMan, pPars, ppCex ); + // output the result if ( !pPars->fSilent ) { @@ -2739,7 +2743,7 @@ int Abc_NtkDarPdr( Abc_Ntk_t * pNtk, Pdr_Par_t * pPars, Abc_Cex_t ** ppCex ) Abc_Print( 1, "Property UNDECIDED. " ); else assert( 0 ); - ABC_PRT( "Time", clock() - clk ); + ABC_PRT( "Time", clock() - clk ); } if ( *ppCex && !Saig_ManVerifyCex( pMan, *ppCex ) ) |