Adding structural flop priority heuristics in 'pdr'.

8 files changed, 214 insertions, 122 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index b8a0a301..319525cf 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, "MFCDRTHGSaxrmusipdegoncvwzh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "MFCDRTHGSaxrmuysipdegoncvwzh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -26126,6 +26126,9 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'u':
             pPars->fNewXSim ^= 1;
             break;
+        case 'y':
+            pPars->fFlopPrio ^= 1;
+            break;
         case 's':
             pPars->fShortest ^= 1;
             break;
@@ -26194,7 +26197,7 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: pdr [-MFCDRTHGS <num>] [-axrmusipdegoncvwzh]\n" );
+    Abc_Print( -2, "usage: pdr [-MFCDRTHGS <num>] [-axrmuysipdegoncvwzh]\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" );
@@ -26212,6 +26215,7 @@ usage:
     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-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-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 9f9ef238..18b059c6 100644
--- a/src/proof/pdr/pdr.h
+++ b/src/proof/pdr/pdr.h
@@ -53,6 +53,7 @@ struct Pdr_Par_t_
     int fTwoRounds;       // use two rounds for generalization
     int fMonoCnf;         // monolythic CNF
     int fNewXSim;         // updated X-valued simulation
+    int fFlopPrio;        // use structural flop priorities
     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 38792ef8..cfc79d85 100644
--- a/src/proof/pdr/pdrCore.c
+++ b/src/proof/pdr/pdrCore.c
@@ -63,6 +63,7 @@ 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->fDumpInv       =       0;  // dump inductive invariant
     pPars->fUseSupp       =       1;  // using support variables in the invariant
@@ -313,7 +314,7 @@ int * Pdr_ManSortByPriority( Pdr_Man_t * p, Pdr_Set_t * pCube )
 int ZPdr_ManSimpleMic( Pdr_Man_t * p, int k, Pdr_Set_t ** ppCube )
 {
     int * pOrder;
-    int i, j, n, Lit, RetValue;
+    int i, j, Lit, RetValue;
     Pdr_Set_t * pCubeTmp;
     // perform generalization
     if ( p->pPars->fSkipGeneral )
@@ -341,19 +342,14 @@ int ZPdr_ManSimpleMic( Pdr_Man_t * p, int k, Pdr_Set_t ** ppCube )
         if ( RetValue == 0 )
             continue;
 
-        // remove j-th entry
-        for ( n = j; n < (*ppCube)->nLits-1; n++ )
-            pOrder[n] = pOrder[n+1];
-        j--;
-
         // success - update the cube
         *ppCube = Pdr_SetCreateFrom( pCubeTmp = *ppCube, i );
         Pdr_SetDeref( pCubeTmp );
         assert( (*ppCube)->nLits > 0 );
-        i--;
 
-        // get the ordering by decreasing priorit
+        // get the ordering by decreasing priority
         pOrder = Pdr_ManSortByPriority( p, *ppCube );
+        j--;
     }
     return 0;
 }
@@ -423,7 +419,7 @@ int ZPdr_ManDown( Pdr_Man_t * p, int k, Pdr_Set_t ** ppCube, Pdr_Set_t * pPred,
             {
                 assert( pCubeMin->Lits[i] >= 0 );
                 assert( (pCubeMin->Lits[i] / 2) < Aig_ManRegNum(p->pAig) );
-                Vec_IntAddToEntry( p->vPrio, pCubeMin->Lits[i] / 2, 1 );
+                Vec_IntAddToEntry( p->vPrio, pCubeMin->Lits[i] / 2, 1 << p->nPrioShift );
             }
 
             Vec_VecPush( p->vClauses, l, pCubeMin );   // consume ref
@@ -456,14 +452,14 @@ int ZPdr_ManDown( Pdr_Man_t * p, int k, Pdr_Set_t ** ppCube, Pdr_Set_t * pPred,
             return 0;
         if ( p->pPars->fVeryVerbose )
         {
-          printf("Intersection:\n");
-          ZPdr_SetPrint( *ppCube );
+            printf("Intersection:\n");
+            ZPdr_SetPrint( *ppCube );
         }
         if ( Pdr_SetIsInit( *ppCube, -1 ) )
         {
-          if ( p->pPars->fVeryVerbose )
-            printf ("Failed initiation\n");
-          return 0;
+            if ( p->pPars->fVeryVerbose )
+                printf ("Failed initiation\n");
+            return 0;
         }
         RetValue = Pdr_ManCheckCube ( p, k, *ppCube, &pPred, p->pPars->nConfLimit, 0 );
         if ( RetValue == -1 )
@@ -497,7 +493,7 @@ int ZPdr_ManDown( Pdr_Man_t * p, int k, Pdr_Set_t ** ppCube, Pdr_Set_t * pPred,
 int Pdr_ManGeneralize( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppPred, Pdr_Set_t ** ppCubeMin )
 {
     Pdr_Set_t * pCubeMin, * pCubeTmp = NULL, * pPred = NULL, * pCubeCpy = NULL;
-    int i, j, n, Lit, RetValue;
+    int i, j, Lit, RetValue;
     abctime clk = Abc_Clock();
     int * pOrder;
     int added = 0;
@@ -546,9 +542,9 @@ int Pdr_ManGeneralize( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppP
             // try removing this literal
             Lit = pCubeMin->Lits[i]; pCubeMin->Lits[i] = -1; 
             if ( p->pPars->fSkipDown )
-              RetValue = Pdr_ManCheckCube( p, k, pCubeMin, NULL, p->pPars->nConfLimit, 1 );
+                RetValue = Pdr_ManCheckCube( p, k, pCubeMin, NULL, p->pPars->nConfLimit, 1 );
             else
-              RetValue = Pdr_ManCheckCube( p, k, pCubeMin, &pPred, p->pPars->nConfLimit, 1 );
+                RetValue = Pdr_ManCheckCube( p, k, pCubeMin, &pPred, p->pPars->nConfLimit, 1 );
             if ( RetValue == -1 )
             {
                 Pdr_SetDeref( pCubeMin );
@@ -557,52 +553,47 @@ int Pdr_ManGeneralize( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppP
             pCubeMin->Lits[i] = Lit;
             if ( RetValue == 0 )
             {
-              if ( p->pPars->fSkipDown )
-                  continue;
-              pCubeCpy = Pdr_SetCreateFrom ( pCubeMin, i );
-              RetValue = ZPdr_ManDown ( p, k, &pCubeCpy, pPred, keep, pCubeMin, &added );
-              if ( p->pPars->fCtgs )
-                //CTG handling code messes up with the internal order array
+                if ( p->pPars->fSkipDown )
+                    continue;
+                pCubeCpy = Pdr_SetCreateFrom ( pCubeMin, i );
+                RetValue = ZPdr_ManDown ( p, k, &pCubeCpy, pPred, keep, pCubeMin, &added );
+                if ( p->pPars->fCtgs )
+                    //CTG handling code messes up with the internal order array
+                    pOrder = Pdr_ManSortByPriority( p, pCubeMin );
+                if ( RetValue == -1 )
+                {
+                    Pdr_SetDeref( pCubeMin );
+                    Pdr_SetDeref( pCubeCpy );
+                    Pdr_SetDeref( pPred );
+                    return -1;
+                }
+                if ( RetValue == 0 )
+                {
+                    if ( keep ) 
+                        Hash_IntWriteEntry( keep, pCubeMin->Lits[i], 0 );
+                    if ( pCubeCpy )
+                        Pdr_SetDeref( pCubeCpy );
+                    continue;
+                }
+                //Inductive subclause
+                added = 0;
+                Pdr_SetDeref( pCubeMin );
+                pCubeMin = pCubeCpy;
+                assert( pCubeMin->nLits > 0 );
                 pOrder = Pdr_ManSortByPriority( p, pCubeMin );
-              if ( RetValue == -1 )
-              {
-                  Pdr_SetDeref( pCubeMin );
-                  Pdr_SetDeref( pCubeCpy );
-                  Pdr_SetDeref( pPred );
-                  return -1;
-              }
-              if ( RetValue == 0 )
-              {
-                if ( keep ) 
-                  Hash_IntWriteEntry( keep, pCubeMin->Lits[i], 0 );
-                if ( pCubeCpy )
-                  Pdr_SetDeref( pCubeCpy );
+                j = -1;
                 continue;
-              }
-              //Inductive subclause
-              added = 0;
-              Pdr_SetDeref( pCubeMin );
-              pCubeMin = pCubeCpy;
-              assert( pCubeMin->nLits > 0 );
-              pOrder = Pdr_ManSortByPriority( p, pCubeMin );
-              j = -1;
-              continue;
             }
             added = 0;
 
-            // remove j-th entry
-            for ( n = j; n < pCubeMin->nLits-1; n++ )
-                pOrder[n] = pOrder[n+1];
-            j--;
-
             // success - update the cube
             pCubeMin = Pdr_SetCreateFrom( pCubeTmp = pCubeMin, i );
             Pdr_SetDeref( pCubeTmp );
             assert( pCubeMin->nLits > 0 );
-            i--;
 
-            // get the ordering by decreasing priorit
+            // get the ordering by decreasing priority
             pOrder = Pdr_ManSortByPriority( p, pCubeMin );
+            j--;
         }
 
         if ( p->pPars->fTwoRounds )
@@ -628,19 +619,14 @@ int Pdr_ManGeneralize( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppP
             if ( RetValue == 0 )
                 continue;
 
-            // remove j-th entry
-            for ( n = j; n < pCubeMin->nLits-1; n++ )
-                pOrder[n] = pOrder[n+1];
-            j--;
-
             // success - update the cube
             pCubeMin = Pdr_SetCreateFrom( pCubeTmp = pCubeMin, i );
             Pdr_SetDeref( pCubeTmp );
             assert( pCubeMin->nLits > 0 );
-            i--;
 
-            // get the ordering by decreasing priorit
+            // get the ordering by decreasing priority
             pOrder = Pdr_ManSortByPriority( p, pCubeMin );
+            j--;
         }
     }
 
@@ -762,7 +748,7 @@ int Pdr_ManBlockCube( Pdr_Man_t * p, Pdr_Set_t * pCube )
             {
                 assert( pCubeMin->Lits[i] >= 0 );
                 assert( (pCubeMin->Lits[i] / 2) < Aig_ManRegNum(p->pAig) );
-                Vec_IntAddToEntry( p->vPrio, pCubeMin->Lits[i] / 2, 1 );
+                Vec_IntAddToEntry( p->vPrio, pCubeMin->Lits[i] / 2, 1 << p->nPrioShift );
             }
             Vec_VecPush( p->vClauses, k, pCubeMin );   // consume ref
             p->nCubes++;
diff --git a/src/proof/pdr/pdrInt.h b/src/proof/pdr/pdrInt.h
index 89b6f0d0..dae20f0c 100644
--- a/src/proof/pdr/pdrInt.h
+++ b/src/proof/pdr/pdrInt.h
@@ -82,6 +82,7 @@ struct Pdr_Man_t_
     Vec_Wec_t * vVLits;    // CNF literals
     // data representation
     int         iOutCur;   // current output
+    int         nPrioShift;// priority shift
     Vec_Ptr_t * vCexes;    // counter-examples for each output
     Vec_Ptr_t * vSolvers;  // SAT solvers
     Vec_Vec_t * vClauses;  // clauses by timeframe
@@ -121,6 +122,8 @@ struct Pdr_Man_t_
     int         nQueCur;
     int         nQueMax;
     int         nQueLim;
+    int         nXsimRuns;
+    int         nXsimLits;
     // runtime
     abctime     timeToStop;
     abctime     timeToStopOne;
diff --git a/src/proof/pdr/pdrInv.c b/src/proof/pdr/pdrInv.c
index 8b04c53b..16d98a36 100644
--- a/src/proof/pdr/pdrInv.c
+++ b/src/proof/pdr/pdrInv.c
@@ -467,6 +467,8 @@ void Pdr_ManReportInvariant( Pdr_Man_t * p )
     Vec_Ptr_t * vCubes;
     int kStart = Pdr_ManFindInvariantStart( p );
     vCubes = Pdr_ManCollectCubes( p, kStart );
+//    Abc_Print( 1, "Invariant F[%d] : %d clauses with %d flops (out of %d) (%.2f)\n", 
+//        kStart, Vec_PtrSize(vCubes), Pdr_ManCountVariables(p, kStart), Aig_ManRegNum(p->pAig), 1.0*p->nXsimLits/p->nXsimRuns );
     Abc_Print( 1, "Invariant F[%d] : %d clauses with %d flops (out of %d)\n", 
         kStart, Vec_PtrSize(vCubes), Pdr_ManCountVariables(p, kStart), Aig_ManRegNum(p->pAig) );
     Vec_PtrFree( vCubes );
diff --git a/src/proof/pdr/pdrMan.c b/src/proof/pdr/pdrMan.c
index 31446290..6fe4c28d 100644
--- a/src/proof/pdr/pdrMan.c
+++ b/src/proof/pdr/pdrMan.c
@@ -19,6 +19,7 @@
 ***********************************************************************/
 
 #include "pdrInt.h"
+#include "aig/gia/giaAig.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -33,6 +34,94 @@ ABC_NAMESPACE_IMPL_START
 
 /**Function*************************************************************
 
+  Synopsis    [Structural analysis.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Pdr_ManDeriveFlopPriorities2( Gia_Man_t * p, int fMuxCtrls, int * pnPrioShift )
+{
+    Vec_Int_t * vRes = NULL;
+    Gia_Obj_t * pObj; 
+    int MaxEntry = 0;
+    int i, * pPerm;
+    // create flop costs
+    Vec_Int_t * vCosts = Vec_IntStart( Gia_ManRegNum(p) );
+    Gia_ManCreateRefs(p);
+    Gia_ManForEachRo( p, pObj, i )
+    {
+        Vec_IntWriteEntry( vCosts, i, Gia_ObjRefNum(p, pObj) );
+        MaxEntry = Abc_MaxInt( MaxEntry, Gia_ObjRefNum(p, pObj) );
+    }
+    MaxEntry++;
+    ABC_FREE( p->pRefs );
+    // add costs due to MUX inputs
+    if ( fMuxCtrls )
+    {
+        int fVerbose = 0;
+        Vec_Bit_t * vCtrls = Vec_BitStart( Gia_ManObjNum(p) );
+        Vec_Bit_t * vDatas = Vec_BitStart( Gia_ManObjNum(p) );
+        Gia_Obj_t * pCtrl, * pData1, * pData0; 
+        int nCtrls = 0, nDatas = 0, nBoth = 0;
+        Gia_ManForEachAnd( p, pObj, i )
+        {
+            if ( !Gia_ObjIsMuxType(pObj) )
+                continue;
+            pCtrl  = Gia_ObjRecognizeMux( pObj, &pData1, &pData0 );
+            pCtrl  = Gia_Regular(pCtrl);
+            pData1 = Gia_Regular(pData1);
+            pData0 = Gia_Regular(pData0);
+            Vec_BitWriteEntry( vCtrls, Gia_ObjId(p, pCtrl), 1 );
+            Vec_BitWriteEntry( vDatas, Gia_ObjId(p, pData1), 1 );
+            Vec_BitWriteEntry( vDatas, Gia_ObjId(p, pData0), 1 );
+        }
+        Gia_ManForEachRo( p, pObj, i )
+            if ( Vec_BitEntry(vCtrls, Gia_ObjId(p, pObj)) )
+                Vec_IntAddToEntry( vCosts, i, 2*MaxEntry );
+            //else if ( Vec_BitEntry(vDatas, Gia_ObjId(p, pObj)) )
+            //    Vec_IntAddToEntry( vCosts, i,   MaxEntry );
+        MaxEntry *= 3;
+        // print out
+        if ( fVerbose )
+        {
+            Gia_ManForEachRo( p, pObj, i )
+            {
+                if ( Vec_BitEntry(vCtrls, Gia_ObjId(p, pObj)) )
+                    nCtrls++;
+                if ( Vec_BitEntry(vDatas, Gia_ObjId(p, pObj)) )
+                    nDatas++;
+                if ( Vec_BitEntry(vCtrls, Gia_ObjId(p, pObj)) && Vec_BitEntry(vDatas, Gia_ObjId(p, pObj)) )
+                    nBoth++;
+            }
+            printf( "%10s : Flops = %5d.  Ctrls = %5d.  Datas = %5d.  Both = %5d.\n", Gia_ManName(p), Gia_ManRegNum(p), nCtrls, nDatas, nBoth );
+        }
+        Vec_BitFree( vCtrls );
+        Vec_BitFree( vDatas );
+    }
+    *pnPrioShift = 1 + Abc_Base2Log( MaxEntry );
+    // create ordering based on costs
+    pPerm = Abc_MergeSortCost( Vec_IntArray(vCosts), Vec_IntSize(vCosts) );
+    vRes = Vec_IntAllocArray( pPerm, Vec_IntSize(vCosts) );
+    Vec_IntFree( vCosts );
+    vCosts = Vec_IntInvert( vRes, -1 );
+    Vec_IntFree( vRes );
+//Vec_IntPrint( vCosts );
+    return vCosts;
+}
+Vec_Int_t * Pdr_ManDeriveFlopPriorities( Aig_Man_t * pAig, int fMuxCtrls, int * pnPrioShift )
+{
+    Gia_Man_t * pGia = Gia_ManFromAigSimple(pAig);
+    Vec_Int_t * vRes = Pdr_ManDeriveFlopPriorities2(pGia, fMuxCtrls, pnPrioShift);
+    Gia_ManStop( pGia );
+    return vRes;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Creates manager.]
 
   Description []
@@ -56,7 +145,13 @@ Pdr_Man_t * Pdr_ManStart( Aig_Man_t * pAig, Pdr_Par_t * pPars, Vec_Int_t * vPrio
     if ( !p->pPars->fMonoCnf )
         p->vVLits   = Vec_WecStart( 1+Abc_MaxInt(1, Aig_ManLevels(pAig)) );
     // internal use
-    p->vPrio    = vPrioInit ? vPrioInit : Vec_IntStart( Aig_ManRegNum(pAig) );  // priority flops
+    p->nPrioShift   = 0;
+    if ( vPrioInit )
+        p->vPrio = vPrioInit;
+    else if ( pPars->fFlopPrio )
+        p->vPrio = Pdr_ManDeriveFlopPriorities(pAig, 0, &p->nPrioShift);
+    else
+        p->vPrio = Vec_IntStart( Aig_ManRegNum(pAig) );
     p->vLits    = Vec_IntAlloc( 100 );  // array of literals
     p->vCiObjs  = Vec_IntAlloc( 100 );  // cone leaves
     p->vCoObjs  = Vec_IntAlloc( 100 );  // cone roots
@@ -69,7 +164,7 @@ Pdr_Man_t * Pdr_ManStart( Aig_Man_t * pAig, Pdr_Par_t * pPars, Vec_Int_t * vPrio
     p->vRes     = Vec_IntAlloc( 100 );  // final result
     p->pCnfMan  = Cnf_ManStart();
     // ternary simulation
-    p->pTxs     = Txs_ManStart( p, pAig, p->vPrio );
+    p->pTxs     = pPars->fNewXSim ? Txs_ManStart( p, pAig, p->vPrio ) : NULL;
     // additional AIG data-members
     if ( pAig->pFanData == NULL )
         Aig_ManFanoutStart( pAig );
@@ -151,7 +246,8 @@ void Pdr_ManStop( Pdr_Man_t * p )
     // CNF manager
     Cnf_ManStop( p->pCnfMan );
     // terminary simulation
-    Txs_ManStop( p->pTxs );
+    if ( p->pPars->fNewXSim )
+        Txs_ManStop( p->pTxs );
     // internal use
     Vec_IntFreeP( &p->vPrio   );  // priority flops
     Vec_IntFree( p->vLits     );  // array of literals
diff --git a/src/proof/pdr/pdrSat.c b/src/proof/pdr/pdrSat.c
index 936a8f90..b9403e6f 100644
--- a/src/proof/pdr/pdrSat.c
+++ b/src/proof/pdr/pdrSat.c
@@ -366,6 +366,8 @@ int Pdr_ManCheckCube( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppPr
             else
                 *ppPred = Pdr_ManTernarySim( p, k, pCube );
             p->tTsim += Abc_Clock() - clk;
+            p->nXsimLits += (*ppPred)->nLits;
+            p->nXsimRuns++;
         }
         RetValue = 0;
     }
diff --git a/src/proof/pdr/pdrTsim.c b/src/proof/pdr/pdrTsim.c
index 43f2ddb0..0bcb6e0c 100644
--- a/src/proof/pdr/pdrTsim.c
+++ b/src/proof/pdr/pdrTsim.c
@@ -404,67 +404,65 @@ Pdr_ManPrintCex( p->pAig, vCiObjs, vCiVals, NULL );
     RetValue = Pdr_ManSimDataInit( p->pAig, vCiObjs, vCiVals, vNodes, vCoObjs, vCoVals, NULL );
     assert( RetValue );
 
-#if 1
-    // try removing high-priority flops
-    Vec_IntClear( vCi2Rem );
-    Aig_ManForEachObjVec( vCiObjs, p->pAig, pObj, i )
+    // iteratively remove flops
+    if ( p->pPars->fFlopPrio )
     {
-        if ( !Saig_ObjIsLo( p->pAig, pObj ) )
-            continue;
-        Entry = Aig_ObjCioId(pObj) - Saig_ManPiNum(p->pAig);
-        if ( vPrio != NULL && Vec_IntEntry( vPrio, Entry ) != 0 )
-            continue;
-        Vec_IntClear( vUndo );
-        if ( Pdr_ManExtendOne( p->pAig, pObj, vUndo, vVisits ) )
-            Vec_IntPush( vCi2Rem, Aig_ObjId(pObj) );
-        else
-            Pdr_ManExtendUndo( p->pAig, vUndo );
-    }
-    // try removing low-priority flops
-    Aig_ManForEachObjVec( vCiObjs, p->pAig, pObj, i )
-    {
-        if ( !Saig_ObjIsLo( p->pAig, pObj ) )
-            continue;
-        Entry = Aig_ObjCioId(pObj) - Saig_ManPiNum(p->pAig);
-        if ( vPrio == NULL || Vec_IntEntry( vPrio, Entry ) == 0 )
-            continue;
-        Vec_IntClear( vUndo );
-        if ( Pdr_ManExtendOne( p->pAig, pObj, vUndo, vVisits ) )
-            Vec_IntPush( vCi2Rem, Aig_ObjId(pObj) );
-        else
-            Pdr_ManExtendUndo( p->pAig, vUndo );
-    }
-#else
-    // try removing low-priority flops
-    Aig_ManForEachObjVec( vCiObjs, p->pAig, pObj, i )
-    {
-        if ( !Saig_ObjIsLo( p->pAig, pObj ) )
-            continue;
-        Entry = Aig_ObjCioId(pObj) - Saig_ManPiNum(p->pAig);
-        if ( vPrio == NULL || Vec_IntEntry( vPrio, Entry ) == 0 )
-            continue;
-        Vec_IntClear( vUndo );
-        if ( Pdr_ManExtendOne( p->pAig, pObj, vUndo, vVisits ) )
-            Vec_IntPush( vCi2Rem, Aig_ObjId(pObj) );
-        else
-            Pdr_ManExtendUndo( p->pAig, vUndo );
+        // collect flops and sort them by priority
+        Vec_IntClear( vRes );
+        Aig_ManForEachObjVec( vCiObjs, p->pAig, pObj, i )
+        {
+            if ( !Saig_ObjIsLo( p->pAig, pObj ) )
+                continue;
+            Entry = Aig_ObjCioId(pObj) - Saig_ManPiNum(p->pAig);
+            Vec_IntPush( vRes, Entry );
+        }
+        Vec_IntSelectSortCost( Vec_IntArray(vRes), Vec_IntSize(vRes), vPrio );
+
+        // try removing flops starting from low-priority to high-priority
+        Vec_IntClear( vCi2Rem );
+        Vec_IntForEachEntry( vRes, Entry, i )
+        {
+            pObj = Aig_ManCi( p->pAig, Saig_ManPiNum(p->pAig) + Entry );
+            assert( Saig_ObjIsLo( p->pAig, pObj ) );
+            Vec_IntClear( vUndo );
+            if ( Pdr_ManExtendOne( p->pAig, pObj, vUndo, vVisits ) )
+                Vec_IntPush( vCi2Rem, Aig_ObjId(pObj) );
+            else
+                Pdr_ManExtendUndo( p->pAig, vUndo );
+        }
     }
-    // try removing high-priority flops
-    Vec_IntClear( vCi2Rem );
-    Aig_ManForEachObjVec( vCiObjs, p->pAig, pObj, i )
+    else
     {
-        if ( !Saig_ObjIsLo( p->pAig, pObj ) )
-            continue;
-        Entry = Aig_ObjCioId(pObj) - Saig_ManPiNum(p->pAig);
-        if ( vPrio != NULL && Vec_IntEntry( vPrio, Entry ) != 0 )
-            continue;
-        Vec_IntClear( vUndo );
-        if ( Pdr_ManExtendOne( p->pAig, pObj, vUndo, vVisits ) )
-            Vec_IntPush( vCi2Rem, Aig_ObjId(pObj) );
-        else
-            Pdr_ManExtendUndo( p->pAig, vUndo );
+        // try removing low-priority flops first
+        Vec_IntClear( vCi2Rem );
+        Aig_ManForEachObjVec( vCiObjs, p->pAig, pObj, i )
+        {
+            if ( !Saig_ObjIsLo( p->pAig, pObj ) )
+                continue;
+            Entry = Aig_ObjCioId(pObj) - Saig_ManPiNum(p->pAig);
+            if ( vPrio != NULL && Vec_IntEntry( vPrio, Entry ) != 0 )
+                continue;
+            Vec_IntClear( vUndo );
+            if ( Pdr_ManExtendOne( p->pAig, pObj, vUndo, vVisits ) )
+                Vec_IntPush( vCi2Rem, Aig_ObjId(pObj) );
+            else
+                Pdr_ManExtendUndo( p->pAig, vUndo );
+        }
+        // try removing high-priority flops next
+        Aig_ManForEachObjVec( vCiObjs, p->pAig, pObj, i )
+        {
+            if ( !Saig_ObjIsLo( p->pAig, pObj ) )
+                continue;
+            Entry = Aig_ObjCioId(pObj) - Saig_ManPiNum(p->pAig);
+            if ( vPrio == NULL || Vec_IntEntry( vPrio, Entry ) == 0 )
+                continue;
+            Vec_IntClear( vUndo );
+            if ( Pdr_ManExtendOne( p->pAig, pObj, vUndo, vVisits ) )
+                Vec_IntPush( vCi2Rem, Aig_ObjId(pObj) );
+            else
+                Pdr_ManExtendUndo( p->pAig, vUndo );
+        }
     }
-#endif
 
 if ( p->pPars->fVeryVerbose )
 Pdr_ManPrintCex( p->pAig, vCiObjs, vCiVals, vCi2Rem );