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

src/aig/gia/gia.h

@@ -599,7 +599,7 @@ static inline int         Gia_ObjLutFanin( Gia_Man_t * p, int Id, int i )   { re
 /*=== giaAbs.c ===========================================================*/
 extern void                Gia_ManCexAbstractionStart( Gia_Man_t * p, Gia_ParAbs_t * pPars );
 Gia_Man_t *                Gia_ManCexAbstractionDerive( Gia_Man_t * pGia );
-int                        Gia_ManCexAbstractionRefine( Gia_Man_t * pGia, Abc_Cex_t * pCex, int fTryFour, int fSensePath, int fVerbose );
+int                        Gia_ManCexAbstractionRefine( Gia_Man_t * pGia, Abc_Cex_t * pCex, int nFfToAddMax, int fTryFour, int fSensePath, int fVerbose );
 extern int                 Gia_ManPbaPerform( Gia_Man_t * pGia, int nStart, int nFrames, int nConfLimit, int nTimeLimit, int fVerbose, int * piFrame );
 extern int                 Gia_ManCbaPerform( Gia_Man_t * pGia, void * pPars );
 /*=== giaAiger.c ===========================================================*/

src/aig/gia/giaAbs.c

@@ -177,7 +177,7 @@ void Gia_ManCexAbstractionStart( Gia_Man_t * pGia, Gia_ParAbs_t * pPars )
   SeeAlso     []
 
 ***********************************************************************/
-int Gia_ManCexAbstractionRefine( Gia_Man_t * pGia, Abc_Cex_t * pCex, int fTryFour, int fSensePath, int fVerbose )
+int Gia_ManCexAbstractionRefine( Gia_Man_t * pGia, Abc_Cex_t * pCex, int nFfToAddMax, int fTryFour, int fSensePath, int fVerbose )
 {
     Aig_Man_t * pNew;
     Vec_Int_t * vFlops;
@@ -188,7 +188,7 @@ int Gia_ManCexAbstractionRefine( Gia_Man_t * pGia, Abc_Cex_t * pCex, int fTryFou
     }
     pNew = Gia_ManToAig( pGia, 0 );
     vFlops = Gia_ManClasses2Flops( pGia->vFlopClasses );
-    if ( !Saig_ManCexRefineStep( pNew, vFlops, pCex, fTryFour, fSensePath, fVerbose ) )
+    if ( !Saig_ManCexRefineStep( pNew, vFlops, pGia->vFlopClasses, pCex, nFfToAddMax, fTryFour, fSensePath, fVerbose ) )
     {
         pGia->pCexSeq = pNew->pSeqModel; pNew->pSeqModel = NULL;
         Vec_IntFree( vFlops );

src/aig/saig/saig.h

@@ -139,7 +139,7 @@ extern Vec_Int_t *       Saig_ManCbaPerform( Aig_Man_t * pAig, int nInputs, Saig
 /*=== sswAbsPba.c ==========================================================*/
 extern Vec_Int_t *       Saig_ManPbaDerive( Aig_Man_t * pAig, int nInputs, int nStart, int nFrames, int nConfLimit, int nTimeLimit, int fVerbose, int * piFrame );
 /*=== sswAbsStart.c ==========================================================*/
-extern int               Saig_ManCexRefineStep( Aig_Man_t * p, Vec_Int_t * vFlops, Abc_Cex_t * pCex, int fTryFour, int fSensePath, int fVerbose );
+extern int               Saig_ManCexRefineStep( Aig_Man_t * p, Vec_Int_t * vFlops, Vec_Int_t * vFlopClasses, Abc_Cex_t * pCex, int nFfToAddMax, int fTryFour, int fSensePath, int fVerbose );
 extern Vec_Int_t *       Saig_ManCexAbstractionFlops( Aig_Man_t * p, Gia_ParAbs_t * pPars );
 /*=== saigBmc.c ==========================================================*/
 extern int               Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nBTLimit, int fRewrite, int fVerbose, int * piFrame, int nCofFanLit );

src/aig/saig/saigAbsStart.c

@@ -168,7 +168,7 @@ Aig_Man_t * Saig_ManCexRefine( Aig_Man_t * p, Aig_Man_t * pAbs, Vec_Int_t * vFlo
   SeeAlso     []
 
 ***********************************************************************/
-int Saig_ManCexRefineStep( Aig_Man_t * p, Vec_Int_t * vFlops, Abc_Cex_t * pCex, int fTryFour, int fSensePath, int fVerbose )
+int Saig_ManCexRefineStep( Aig_Man_t * p, Vec_Int_t * vFlops, Vec_Int_t * vFlopClasses, Abc_Cex_t * pCex, int nFfToAddMax, int fTryFour, int fSensePath, int fVerbose )
 {
     Aig_Man_t * pAbs;
     Vec_Int_t * vFlopsNew;
@@ -198,7 +198,25 @@ int Saig_ManCexRefineStep( Aig_Man_t * p, Vec_Int_t * vFlops, Abc_Cex_t * pCex,
         printf( "Adding %d registers to the abstraction (total = %d).  ", Vec_IntSize(vFlopsNew), Aig_ManRegNum(p)+Vec_IntSize(vFlopsNew) );
         Abc_PrintTime( 1, "Time", clock() - clk );
     }
-    // vFlopsNew contains PI number that should be kept in pAbs
+    // vFlopsNew contains PI numbers that should be kept in pAbs
+    // select the most useful flops among those to be added
+    if ( nFfToAddMax > 0 && Vec_IntSize(vFlopsNew) > nFfToAddMax )
+    {
+        Vec_Int_t * vFlopsNewBest;
+        // shift the indices
+        Vec_IntForEachEntry( vFlopsNew, Entry, i )
+            Vec_IntAddToEntry( vFlopsNew, i, -Saig_ManPiNum(p) );
+        // create new flops
+        vFlopsNewBest = Saig_ManCbaFilterFlops( p, pCex, vFlopClasses, vFlopsNew, nFfToAddMax );
+        assert( Vec_IntSize(vFlopsNewBest) == nFfToAddMax );
+        printf( "Filtering flops based on cost (%d -> %d).\n", Vec_IntSize(vFlopsNew), Vec_IntSize(vFlopsNewBest) );
+        // update
+        Vec_IntFree( vFlopsNew );
+        vFlopsNew = vFlopsNewBest;
+        // shift the indices
+        Vec_IntForEachEntry( vFlopsNew, Entry, i )
+            Vec_IntAddToEntry( vFlopsNew, i, Saig_ManPiNum(p) );
+    }
     // add to the abstraction
     Vec_IntForEachEntry( vFlopsNew, Entry, i )
     {

src/base/abci/abc.c

@@ -28408,15 +28408,27 @@ int Abc_CommandAbc9AbsRefine( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     Gia_Man_t * pTemp = NULL;
     int c;
+    int nFfToAddMax = 0;
     int fTryFour    = 1;
     int fSensePath  = 0;
     int fVerbose    = 0;
 
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "tsvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Mtsvh" ) ) != EOF )
     {
         switch ( c )
         {
+        case 'M':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-M\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nFfToAddMax = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nFfToAddMax < 0 ) 
+                goto usage;
+            break;
         case 't':
             fTryFour ^= 1;
             break;
@@ -28447,13 +28459,14 @@ int Abc_CommandAbc9AbsRefine( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_Print( -1, "Abc_CommandAbc9AbsRefine(): There is no counter-example.\n" );
         return 1;
     } 
-    pAbc->Status = Gia_ManCexAbstractionRefine( pAbc->pGia, pAbc->pCex, fTryFour, fSensePath, fVerbose );
+    pAbc->Status = Gia_ManCexAbstractionRefine( pAbc->pGia, pAbc->pCex, nFfToAddMax, fTryFour, fSensePath, fVerbose );
     Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexSeq );
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &abs_refine [-tsvh]\n" );
+    Abc_Print( -2, "usage: &abs_refine [-M <num>] [-tsvh]\n" );
     Abc_Print( -2, "\t         refines the pre-computed flop map using the counter-example\n" );
+    Abc_Print( -2, "\t-M num : the max number of flops to add (0 = not used) [default = %d]\n", nFfToAddMax );
     Abc_Print( -2, "\t-t     : toggle trying four abstractions instead of one [default = %s]\n", fTryFour? "yes": "no" );
     Abc_Print( -2, "\t-s     : toggle using the path sensitization algorithm [default = %s]\n", fSensePath? "yes": "no" );
     Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );