Bug fix in CBA and PBA.

7 files changed, 45 insertions, 21 deletions

diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index 2f07e0e9..8bef0e1d 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -600,7 +600,7 @@ static inline int         Gia_ObjLutFanin( Gia_Man_t * p, int Id, int i )   { re
 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 );
-extern int                 Gia_ManPbaPerform( Gia_Man_t * pGia, int nFrames, int nConfLimit, int fVerbose, int * piFrame );
+extern int                 Gia_ManPbaPerform( Gia_Man_t * pGia, int nStart, int nFrames, int nConfLimit, int fVerbose, int * piFrame );
 extern int                 Gia_ManCbaPerform( Gia_Man_t * pGia, void * pPars );
 /*=== giaAiger.c ===========================================================*/
 extern int                 Gia_FileSize( char * pFileName );
diff --git a/src/aig/gia/giaAbs.c b/src/aig/gia/giaAbs.c
index e08d63fc..ecbf603e 100644
--- a/src/aig/gia/giaAbs.c
+++ b/src/aig/gia/giaAbs.c
@@ -316,7 +316,7 @@ int Gia_ManCbaPerform( Gia_Man_t * pGia, void * pPars )
   SeeAlso     []
 
 ***********************************************************************/
-int Gia_ManPbaPerform( Gia_Man_t * pGia, int nFrames, int nConfLimit, int fVerbose, int * piFrame )
+int Gia_ManPbaPerform( Gia_Man_t * pGia, int nStart, int nFrames, int nConfLimit, int fVerbose, int * piFrame )
 {
     Gia_Man_t * pAbs;
     Aig_Man_t * pAig, * pOrig;
@@ -332,7 +332,7 @@ int Gia_ManPbaPerform( Gia_Man_t * pGia, int nFrames, int nConfLimit, int fVerbo
     // refine abstraction using PBA
     pAig = Gia_ManToAigSimple( pAbs );
     Gia_ManStop( pAbs );
-    vFlopsNew = Saig_ManPbaDerive( pAig, Gia_ManPiNum(pGia), nFrames, nConfLimit, fVerbose, piFrame );
+    vFlopsNew = Saig_ManPbaDerive( pAig, Gia_ManPiNum(pGia), nStart, nFrames, nConfLimit, fVerbose, piFrame );
     // derive new classes
     if ( pAig->pSeqModel == NULL )
     {
diff --git a/src/aig/saig/saig.h b/src/aig/saig/saig.h
index 505fd6ee..fa68bf95 100644
--- a/src/aig/saig/saig.h
+++ b/src/aig/saig/saig.h
@@ -135,7 +135,7 @@ extern Abc_Cex_t *       Saig_ManCbaFindCexCareBits( Aig_Man_t * pAig, Abc_Cex_t
 extern Vec_Int_t *       Saig_ManCbaFilterInputs( Aig_Man_t * pAig, int iFirstFlopPi, Abc_Cex_t * pCex, int fVerbose );
 extern Vec_Int_t *       Saig_ManCbaPerform( Aig_Man_t * pAig, int nInputs, Saig_ParBmc_t * pPars );
 /*=== sswAbsPba.c ==========================================================*/
-extern Vec_Int_t *       Saig_ManPbaDerive( Aig_Man_t * pAig, int nInputs, int nFrames, int nConfLimit, int fVerbose, int * piFrame );
+extern Vec_Int_t *       Saig_ManPbaDerive( Aig_Man_t * pAig, int nInputs, int nStart, int nFrames, int nConfLimit, 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 Vec_Int_t *       Saig_ManCexAbstractionFlops( Aig_Man_t * p, Gia_ParAbs_t * pPars );
diff --git a/src/aig/saig/saigAbsCba.c b/src/aig/saig/saigAbsCba.c
index 02d01852..f79cbf09 100644
--- a/src/aig/saig/saigAbsCba.c
+++ b/src/aig/saig/saigAbsCba.c
@@ -609,7 +609,7 @@ ABC_PRT( "Time", clock() - clk );
 
 ***********************************************************************/
 Vec_Int_t * Saig_ManCbaPerform( Aig_Man_t * pAbs, int nInputs, Saig_ParBmc_t * pPars )
-{    
+{
     Vec_Int_t * vAbsFfsToAdd;
     int RetValue, clk = clock();
 //    assert( pAbs->nRegs > 0 );
@@ -617,6 +617,7 @@ Vec_Int_t * Saig_ManCbaPerform( Aig_Man_t * pAbs, int nInputs, Saig_ParBmc_t * p
     RetValue = Saig_ManBmcScalable( pAbs, pPars );
     if ( RetValue == -1 ) // time out - nothing to add
     {
+        printf( "Resource limit is reached during BMC.\n" );
         assert( pAbs->pSeqModel == NULL );
         return Vec_IntAlloc( 0 );
     }
@@ -631,7 +632,7 @@ Vec_Int_t * Saig_ManCbaPerform( Aig_Man_t * pAbs, int nInputs, Saig_ParBmc_t * p
     }
     if ( pPars->fVerbose )
     {
-        printf( "Adding %d registers to the abstraction.  ", Vec_IntSize(vAbsFfsToAdd) );
+        printf( "Adding %d registers to the abstraction (total = %d).  ", Vec_IntSize(vAbsFfsToAdd), Aig_ManRegNum(pAbs)+Vec_IntSize(vAbsFfsToAdd) );
         Abc_PrintTime( 1, "Time", clock() - clk );
     }
     return vAbsFfsToAdd;
diff --git a/src/aig/saig/saigAbsPba.c b/src/aig/saig/saigAbsPba.c
index edc9b6fd..e3c49142 100644
--- a/src/aig/saig/saigAbsPba.c
+++ b/src/aig/saig/saigAbsPba.c
@@ -72,7 +72,7 @@ void Saig_ManUnrollForPba_rec( Aig_Man_t * pAig, Aig_Obj_t * pObj, Vec_Int_t * v
   SeeAlso     []
  
 ***********************************************************************/
-Aig_Man_t * Saig_ManUnrollForPba( Aig_Man_t * pAig, int nFrames, Vec_Int_t ** pvPiVarMap )
+Aig_Man_t * Saig_ManUnrollForPba( Aig_Man_t * pAig, int nStart, int nFrames, Vec_Int_t ** pvPiVarMap )
 {
     Aig_Man_t * pFrames;     // unrolled timeframes
     Vec_Vec_t * vFrameCos;   // the list of COs per frame
@@ -80,6 +80,7 @@ Aig_Man_t * Saig_ManUnrollForPba( Aig_Man_t * pAig, int nFrames, Vec_Int_t ** pv
     Vec_Int_t * vRoots, * vObjs;
     Aig_Obj_t * pObj, * pObjNew;
     int i, f;
+    assert( nStart <= nFrames );
     // collect COs and Objs visited in each frame
     vFrameCos  = Vec_VecStart( nFrames );
     vFrameObjs = Vec_VecStart( nFrames );
@@ -130,8 +131,11 @@ Aig_Man_t * Saig_ManUnrollForPba( Aig_Man_t * pAig, int nFrames, Vec_Int_t ** pv
                 assert( 0 );
         }
         // create output
-        Saig_ManForEachPo( pAig, pObj, i )
-            pObjNew = Aig_Or( pFrames, pObjNew, pObj->pData );
+        if ( f >= nStart )
+        {
+            Saig_ManForEachPo( pAig, pObj, i )
+                pObjNew = Aig_Or( pFrames, pObjNew, pObj->pData );
+        }
         // transfer
         if ( f == nFrames - 1 )
             break;
@@ -243,7 +247,7 @@ Abc_Cex_t * Saig_ManPbaDeriveCex( Aig_Man_t * pAig, sat_solver * pSat, Cnf_Dat_t
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Int_t * Saig_ManPbaDerive( Aig_Man_t * pAig, int nInputs, int nFrames, int nConfLimit, int fVerbose, int * piFrame )
+Vec_Int_t * Saig_ManPbaDerive( Aig_Man_t * pAig, int nInputs, int nStart, int nFrames, int nConfLimit, int fVerbose, int * piFrame )
 {
     Vec_Int_t * vFlops = NULL, * vMapVar2FF, * vAssumps, * vPiVarMap;
     Aig_Man_t * pFrames;
@@ -252,10 +256,11 @@ Vec_Int_t * Saig_ManPbaDerive( Aig_Man_t * pAig, int nInputs, int nFrames, int n
     Aig_Obj_t * pObj;
     int nCoreLits, * pCoreLits;
     int i, iVar, RetValue, clk;
-
+if ( fVerbose )
+printf( "Performing abstraction with starting frame %d and total number of frames %d.\n", nStart, nFrames );
     // create SAT solver
 clk = clock();
-    pFrames = Saig_ManUnrollForPba( pAig, nFrames, &vPiVarMap );
+    pFrames = Saig_ManUnrollForPba( pAig, nStart, nFrames, &vPiVarMap );
 if ( fVerbose )
 Aig_ManPrintStats( pFrames );
 //    pCnf = Cnf_DeriveSimple( pFrames, 0 );
@@ -306,7 +311,7 @@ Abc_PrintTime( 1, "Solving", clock() - clk );
             }
             if ( fVerbose )
             {
-                printf( "Adding %d registers to the abstraction.  ", Vec_IntSize(vAbsFfsToAdd) );
+                printf( "Adding %d registers to the abstraction (total = %d).  ", Vec_IntSize(vAbsFfsToAdd), Aig_ManRegNum(pAig)+Vec_IntSize(vAbsFfsToAdd) );
                 Abc_PrintTime( 1, "Time", clock() - clk );
             }
             vFlops = vAbsFfsToAdd;
diff --git a/src/aig/saig/saigAbsStart.c b/src/aig/saig/saigAbsStart.c
index ec933512..5f7042c8 100644
--- a/src/aig/saig/saigAbsStart.c
+++ b/src/aig/saig/saigAbsStart.c
@@ -139,7 +139,7 @@ Aig_Man_t * Saig_ManCexRefine( Aig_Man_t * p, Aig_Man_t * pAbs, Vec_Int_t * vFlo
     }
     // vFlopsNew contains PI numbers that should be kept in pAbs
     if ( fVerbose )
-        printf( "Adding %d registers to the abstraction.\n\n", Vec_IntSize(vFlopsNew) );
+        printf( "Adding %d registers to the abstraction (total = %d).\n\n", Vec_IntSize(vFlopsNew), Aig_ManRegNum(pAbs)+Vec_IntSize(vFlopsNew) );
     // add to the abstraction
     Vec_IntForEachEntry( vFlopsNew, Entry, i )
     {
@@ -195,7 +195,7 @@ int Saig_ManCexRefineStep( Aig_Man_t * p, Vec_Int_t * vFlops, Abc_Cex_t * pCex,
     }
     if ( fVerbose )
     {
-        printf( "Adding %d registers to the abstraction.  ", Vec_IntSize(vFlopsNew) );
+        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
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 637d0cd4..63d22148 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -28438,17 +28438,29 @@ usage:
 ***********************************************************************/
 int Abc_CommandAbc9AbsPba( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
+    int nStart     =        0;
     int nFramesMax = (pAbc->nFrames >= 0) ? pAbc->nFrames : 20;
-    int nConfMax   = 100000;
-    int fVerbose   =      0;
-    int iFrame     =     -1;
+    int nConfMax   = 10000000;
+    int fVerbose   =        0;
+    int iFrame     =       -1;
     int c;
 
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "FCvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "SFCvh" ) ) != EOF )
     {
         switch ( c )
         {
+        case 'S':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-S\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nStart = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nStart < 0 ) 
+                goto usage;
+            break;
         case 'F':
             if ( globalUtilOptind >= argc )
             {
@@ -28495,15 +28507,21 @@ int Abc_CommandAbc9AbsPba( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_Print( -1, "The flop map is not given.\n" );
         return 0;
     }
-    Gia_ManPbaPerform( pAbc->pGia, nFramesMax, nConfMax, fVerbose, &iFrame );
+    if ( nStart >= nFramesMax )
+    {
+        Abc_Print( -1, "The starting frame (%d) should be less than the total number of frames (%d).\n", nStart, nFramesMax );
+        return 0;
+    }
+    Gia_ManPbaPerform( pAbc->pGia, nStart, nFramesMax, nConfMax, fVerbose, &iFrame );
     if ( iFrame >= 0 )
         pAbc->nFrames = iFrame;
     Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexSeq );
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &abs_pba [-FC num] [-vh]\n" );
+    Abc_Print( -2, "usage: &abs_pba [-SFC num] [-vh]\n" );
     Abc_Print( -2, "\t         refines abstracted flop map with proof-based abstraction\n" );
+    Abc_Print( -2, "\t-S num : the starting timeframe for SAT check [default = %d]\n", nStart );
     Abc_Print( -2, "\t-F num : the max number of timeframes to unroll [default = %d]\n", nFramesMax );
     Abc_Print( -2, "\t-C num : the max number of SAT solver conflicts [default = %d]\n", nConfMax );
     Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );