Adding specialized flop ordering before generalization in 'pdr'.

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 )