diff options
| author | Yen-Sheng Ho <ysho@berkeley.edu> | 2017-02-28 18:05:58 -0800 |
|---|---|---|
| committer | Yen-Sheng Ho <ysho@berkeley.edu> | 2017-02-28 18:05:58 -0800 |
| commit | 902a78eeb883cb97131e03cc31cf0892787e806e (patch) | |
| tree | 6a3a83a72d13c1afbfe9a6da4415ac34dd6bab4b /src/base/wlc/wlcCom.c | |
| parent | d95d51c474fdd5d882b34c8bcbcd27173ba8431c (diff) | |
| download | abc-902a78eeb883cb97131e03cc31cf0892787e806e.tar.gz abc-902a78eeb883cb97131e03cc31cf0892787e806e.tar.bz2 abc-902a78eeb883cb97131e03cc31cf0892787e806e.zip | |
added an option -r to %pdra: proof-based refinement only
Diffstat (limited to 'src/base/wlc/wlcCom.c')
| -rw-r--r-- | src/base/wlc/wlcCom.c | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/src/base/wlc/wlcCom.c b/src/base/wlc/wlcCom.c index 781f4a9a..0c9cdabb 100644 --- a/src/base/wlc/wlcCom.c +++ b/src/base/wlc/wlcCom.c @@ -462,7 +462,7 @@ int Abc_CommandPdrAbs( Abc_Frame_t * pAbc, int argc, char ** argv ) int c; Wlc_ManSetDefaultParams( pPars ); Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "AMXFILabcpmxvwh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "AMXFILabrcpmxvwh" ) ) != EOF ) { switch ( c ) { @@ -538,6 +538,9 @@ int Abc_CommandPdrAbs( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'b': pPars->fProofRefine ^= 1; break; + case 'r': + pPars->fHybrid ^= 1; + break; case 'x': pPars->fXorOutput ^= 1; break; @@ -581,6 +584,7 @@ usage: Abc_Print( -2, "\t-x : toggle XORing outputs of word-level miter [default = %s]\n", pPars->fXorOutput? "yes": "no" ); Abc_Print( -2, "\t-a : toggle running pdr with -nct [default = %s]\n", pPars->fPdra? "yes": "no" ); Abc_Print( -2, "\t-b : toggle using proof-based refinement [default = %s]\n", pPars->fProofRefine? "yes": "no" ); + Abc_Print( -2, "\t-r : toggle using both cex-based and proof-based refinement [default = %s]\n", pPars->fHybrid? "yes": "no" ); Abc_Print( -2, "\t-c : toggle checking clauses in the reloaded trace [default = %s]\n", pPars->fCheckClauses? "yes": "no" ); Abc_Print( -2, "\t-p : toggle pushing clauses in the reloaded trace [default = %s]\n", pPars->fPushClauses? "yes": "no" ); Abc_Print( -2, "\t-m : toggle refining the whole MFFC of a PPI [default = %s]\n", pPars->fMFFC? "yes": "no" ); |