Added limit on the number of flops to add in one iteration of &abs_cba.

1 files changed, 16 insertions, 1 deletions

diff --git a/src/aig/gia/giaAbs.c b/src/aig/gia/giaAbs.c
index 37f5e315..2b5414e7 100644
--- a/src/aig/gia/giaAbs.c
+++ b/src/aig/gia/giaAbs.c
@@ -273,7 +273,7 @@ int Gia_ManCbaPerform( Gia_Man_t * pGia, void * pPars )
     Saig_ParBmc_t * p = (Saig_ParBmc_t *)pPars;
     Gia_Man_t * pAbs;
     Aig_Man_t * pAig, * pOrig;
-    Vec_Int_t * vAbsFfsToAdd;
+    Vec_Int_t * vAbsFfsToAdd, * vAbsFfsToAddBest;
     // check if flop classes are given
     if ( pGia->vFlopClasses == NULL )
     {
@@ -298,6 +298,21 @@ int Gia_ManCbaPerform( Gia_Man_t * pGia, void * pPars )
         Aig_ManStop( pAig );
         return 0;
     }
+    // select the most useful flops among those to be added
+    if ( p->nFfToAddMax > 0 && Vec_IntSize(vAbsFfsToAdd) > p->nFfToAddMax )
+    {
+        // compute new flops
+        Aig_Man_t * pAigBig = Gia_ManToAigSimple( pGia );
+        vAbsFfsToAddBest = Saig_ManCbaFilterFlops( pAigBig, pAig->pSeqModel, pGia->vFlopClasses, vAbsFfsToAdd, p->nFfToAddMax );
+        Aig_ManStop( pAigBig );
+        assert( Vec_IntSize(vAbsFfsToAddBest) == p->nFfToAddMax );
+        if ( p->fVerbose )
+            printf( "Filtering flops based on cost (%d -> %d).\n", Vec_IntSize(vAbsFfsToAdd), Vec_IntSize(vAbsFfsToAddBest) );
+        // update
+        Vec_IntFree( vAbsFfsToAdd );
+        vAbsFfsToAdd = vAbsFfsToAddBest;
+
+    }
     Aig_ManStop( pAig );
     // update flop classes
     Gia_ManFlopsAddToClasses( pGia->vFlopClasses, vAbsFfsToAdd );