diff options
| -rw-r--r-- | src/base/abci/abc.c | 8 | ||||
| -rw-r--r-- | src/proof/pdr/pdr.h | 1 | ||||
| -rw-r--r-- | src/proof/pdr/pdrCore.c | 32 |
3 files changed, 38 insertions, 3 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 319525cf..008adbae 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -26008,7 +26008,7 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv ) int c; Pdr_ManSetDefaultParams( pPars ); Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "MFCDRTHGSaxrmuysipdegoncvwzh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "MFCDRTHGSaxrmuyfsipdegoncvwzh" ) ) != EOF ) { switch ( c ) { @@ -26129,6 +26129,9 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'y': pPars->fFlopPrio ^= 1; break; + case 'f': + pPars->fFlopOrder ^= 1; + break; case 's': pPars->fShortest ^= 1; break; @@ -26197,7 +26200,7 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: pdr [-MFCDRTHGS <num>] [-axrmuysipdegoncvwzh]\n" ); + Abc_Print( -2, "usage: pdr [-MFCDRTHGS <num>] [-axrmuyfsipdegoncvwzh]\n" ); Abc_Print( -2, "\t model checking using property directed reachability (aka IC3)\n" ); Abc_Print( -2, "\t pioneered by Aaron R. Bradley (http://theory.stanford.edu/~arbrad/)\n" ); Abc_Print( -2, "\t with improvements by Niklas Een (http://een.se/niklas/)\n" ); @@ -26216,6 +26219,7 @@ usage: Abc_Print( -2, "\t-m : toggle using monolythic CNF computation [default = %s]\n", pPars->fMonoCnf? "yes": "no" ); Abc_Print( -2, "\t-u : toggle updated X-valued simulation [default = %s]\n", pPars->fNewXSim? "yes": "no" ); Abc_Print( -2, "\t-y : toggle using structural flop priorities [default = %s]\n", pPars->fFlopPrio? "yes": "no" ); + Abc_Print( -2, "\t-f : toggle ordering flops by cost before generalization [default = %s]\n", pPars->fFlopOrder? "yes": "no" ); Abc_Print( -2, "\t-s : toggle creating only shortest counter-examples [default = %s]\n", pPars->fShortest? "yes": "no" ); Abc_Print( -2, "\t-i : toggle clause pushing from an intermediate timeframe [default = %s]\n", pPars->fShiftStart? "yes": "no" ); Abc_Print( -2, "\t-p : toggle reusing proof-obligations in the last timeframe [default = %s]\n", pPars->fReuseProofOblig? "yes": "no" ); diff --git a/src/proof/pdr/pdr.h b/src/proof/pdr/pdr.h index 18b059c6..66990bfb 100644 --- a/src/proof/pdr/pdr.h +++ b/src/proof/pdr/pdr.h @@ -54,6 +54,7 @@ struct Pdr_Par_t_ int fMonoCnf; // monolythic CNF int fNewXSim; // updated X-valued simulation int fFlopPrio; // use structural flop priorities + int fFlopOrder; // order flops for 'analyze_final' during generalization int fDumpInv; // dump inductive invariant int fUseSupp; // use support in the invariant int fShortest; // forces bug traces to be shortest diff --git a/src/proof/pdr/pdrCore.c b/src/proof/pdr/pdrCore.c index cfc79d85..74a15e40 100644 --- a/src/proof/pdr/pdrCore.c +++ b/src/proof/pdr/pdrCore.c @@ -63,8 +63,9 @@ void Pdr_ManSetDefaultParams( Pdr_Par_t * pPars ) pPars->fSkipDown = 1; // apply down in generalization pPars->fCtgs = 0; // handle CTGs in down pPars->fMonoCnf = 0; // monolythic CNF - pPars->fFlopPrio = 0; // use structural flop priorities pPars->fNewXSim = 0; // updated X-valued simulation + pPars->fFlopPrio = 0; // use structural flop priorities + pPars->fFlopOrder = 0; // order flops for 'analyze_final' during generalization pPars->fDumpInv = 0; // dump inductive invariant pPars->fUseSupp = 1; // using support variables in the invariant pPars->fShortest = 0; // forces bug traces to be shortest @@ -479,6 +480,31 @@ int ZPdr_ManDown( Pdr_Man_t * p, int k, Pdr_Set_t ** ppCube, Pdr_Set_t * pPred, } return 1; } + +/**Function************************************************************* + + Synopsis [Specialized sorting of flops based on cost.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Vec_IntSelectSortCostReverseLit( int * pArray, int nSize, Vec_Int_t * vCosts ) +{ + int i, j, best_i; + for ( i = 0; i < nSize-1; i++ ) + { + best_i = i; + for ( j = i+1; j < nSize; j++ ) + if ( Vec_IntEntry(vCosts, Abc_Lit2Var(pArray[j])) > Vec_IntEntry(vCosts, Abc_Lit2Var(pArray[best_i])) ) + best_i = j; + ABC_SWAP( int, pArray[i], pArray[best_i] ); + } +} + /**Function************************************************************* Synopsis [Returns 1 if the state could be blocked.] @@ -500,7 +526,11 @@ int Pdr_ManGeneralize( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppP Hash_Int_t * keep = NULL; // if there is no induction, return *ppCubeMin = NULL; + if ( p->pPars->fFlopOrder ) + Vec_IntSelectSortCostReverseLit( pCube->Lits, pCube->nLits, p->vPrio ); RetValue = Pdr_ManCheckCube( p, k, pCube, ppPred, p->pPars->nConfLimit, 0 ); + if ( p->pPars->fFlopOrder ) + Vec_IntSelectSort( pCube->Lits, pCube->nLits ); if ( RetValue == -1 ) return -1; if ( RetValue == 0 ) |