Bug fix in CBA and PBA.

9 files changed, 86 insertions, 33 deletions

diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index 3beed711..2f07e0e9 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 );
+extern int                 Gia_ManPbaPerform( Gia_Man_t * pGia, 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 673d45e8..e08d63fc 100644
--- a/src/aig/gia/giaAbs.c
+++ b/src/aig/gia/giaAbs.c
@@ -268,8 +268,9 @@ void Gia_ManFlopsAddToClasses( Vec_Int_t * vFlopClasses, Vec_Int_t * vAbsFfsToAd
   SeeAlso     []
 
 ***********************************************************************/
-int Gia_ManCbaPerform( Gia_Man_t * pGia, void * p )
+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;
@@ -315,7 +316,7 @@ int Gia_ManCbaPerform( Gia_Man_t * pGia, void * p )
   SeeAlso     []
 
 ***********************************************************************/
-int Gia_ManPbaPerform( Gia_Man_t * pGia, int nFrames, int nConfLimit, int fVerbose )
+int Gia_ManPbaPerform( Gia_Man_t * pGia, int nFrames, int nConfLimit, int fVerbose, int * piFrame )
 {
     Gia_Man_t * pAbs;
     Aig_Man_t * pAig, * pOrig;
@@ -331,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 );
+    vFlopsNew = Saig_ManPbaDerive( pAig, Gia_ManPiNum(pGia), 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 f20641a5..505fd6ee 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 );
+extern Vec_Int_t *       Saig_ManPbaDerive( Aig_Man_t * pAig, int nInputs, 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/saigAbs.c b/src/aig/saig/saigAbs.c
index 19dbe0fd..01b1e6a6 100644
--- a/src/aig/saig/saigAbs.c
+++ b/src/aig/saig/saigAbs.c
@@ -91,9 +91,9 @@ Abc_Cex_t * Saig_ManCexRemap( Aig_Man_t * p, Aig_Man_t * pAbs, Abc_Cex_t * pCexA
     Aig_Obj_t * pObj;
     int i, f;
     if ( !Saig_ManVerifyCex( pAbs, pCexAbs ) )
-        printf( "Saig_ManCexRemap(): The intial counter-example is invalid.\n" );
-    else
-        printf( "Saig_ManCexRemap(): The intial counter-example is correct.\n" );
+        printf( "Saig_ManCexRemap(): The initial counter-example is invalid.\n" );
+//    else
+//        printf( "Saig_ManCexRemap(): The initial counter-example is correct.\n" );
     // start the counter-example
     pCex = Abc_CexAlloc( Aig_ManRegNum(p), Saig_ManPiNum(p), pCexAbs->iFrame+1 );
     pCex->iFrame = pCexAbs->iFrame;
diff --git a/src/aig/saig/saigAbsCba.c b/src/aig/saig/saigAbsCba.c
index 78a77ecb..02d01852 100644
--- a/src/aig/saig/saigAbsCba.c
+++ b/src/aig/saig/saigAbsCba.c
@@ -180,6 +180,8 @@ void Saig_ManCbaFindReason_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Int_t * vPr
     if ( Aig_ObjIsTravIdCurrent(p, pObj) )
         return;
     Aig_ObjSetTravIdCurrent(p, pObj);
+    if ( Aig_ObjIsConst1(pObj) )
+        return;
     if ( Aig_ObjIsPi(pObj) )
     {
         Vec_IntPush( vReasons, Aig_ObjPioNum(pObj) );
@@ -267,7 +269,7 @@ Vec_Int_t * Saig_ManCbaFindReason( Saig_ManCba_t * p )
     Aig_ManIncrementTravId( p->pFrames );
     Saig_ManCbaFindReason_rec( p->pFrames, Aig_ObjFanin0(pObj), vPrios, vReasons );
     Vec_IntFree( vPrios );
-    assert( !Aig_ObjIsTravIdCurrent(p->pFrames, Aig_ManConst1(p->pFrames)) );
+//    assert( !Aig_ObjIsTravIdCurrent(p->pFrames, Aig_ManConst1(p->pFrames)) );
     return vReasons;
 }
 
@@ -630,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) );
-        Abc_PrintTime( 0, "Time", clock() - clk );
+        Abc_PrintTime( 1, "Time", clock() - clk );
     }
     return vAbsFfsToAdd;
 }
diff --git a/src/aig/saig/saigAbsPba.c b/src/aig/saig/saigAbsPba.c
index 21d92f57..edc9b6fd 100644
--- a/src/aig/saig/saigAbsPba.c
+++ b/src/aig/saig/saigAbsPba.c
@@ -171,19 +171,63 @@ Aig_Man_t * Saig_ManUnrollForPba( Aig_Man_t * pAig, int nFrames, Vec_Int_t ** pv
 Abc_Cex_t * Saig_ManPbaDeriveCex( Aig_Man_t * pAig, sat_solver * pSat, Cnf_Dat_t * pCnf, int nFrames, Vec_Int_t * vPiVarMap )
 {
     Abc_Cex_t * pCex;
-    int i, f, Entry;
-    pCex = Abc_CexAlloc( Aig_ManRegNum(pAig), Saig_ManPiNum(pAig), nFrames );   
+    Aig_Obj_t * pObj, * pObjRi, * pObjRo;
+    int i, f, Entry, iBit = 0;
+    pCex = Abc_CexAlloc( Aig_ManRegNum(pAig), Saig_ManPiNum(pAig), nFrames );
+    pCex->iPo = -1;
+    pCex->iFrame = -1;
     Vec_IntForEachEntry( vPiVarMap, Entry, i )
+    {
         if ( Entry >= 0 )
         {
             int iSatVar = pCnf->pVarNums[ Aig_ObjId(Aig_ManPi(pCnf->pMan, Entry)) ];
             if ( sat_solver_var_value( pSat, iSatVar ) )
                 Aig_InfoSetBit( pCex->pData, Aig_ManRegNum(pAig) + i );
         }
+    }
     // check what frame has failed
+    Aig_ManCleanMarkB(pAig);
+    Aig_ManConst1(pAig)->fMarkB = 1;
+    Saig_ManForEachLo( pAig, pObj, i )
+        pObj->fMarkB = Aig_InfoHasBit(pCex->pData, iBit++);
     for ( f = 0; f < nFrames; f++ )
     {
-//        Aig_ManForEach
+        // compute new state
+        Saig_ManForEachPi( pAig, pObj, i )
+            pObj->fMarkB = Aig_InfoHasBit(pCex->pData, iBit++);
+        Aig_ManForEachNode( pAig, pObj, i )
+            pObj->fMarkB = (Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj)) & 
+                           (Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj));
+        Aig_ManForEachPo( pAig, pObj, i )
+            pObj->fMarkB = Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj);
+        Saig_ManForEachLiLo( pAig, pObjRi, pObjRo, i )
+            pObjRo->fMarkB = pObjRi->fMarkB;
+        // check the outputs
+        Saig_ManForEachPo( pAig, pObj, i )
+        {
+            if ( pObj->fMarkB )
+            {
+                pCex->iPo = i;
+                pCex->iFrame = f;
+                pCex->nBits = pCex->nRegs + pCex->nPis * (f+1);
+                break;
+            }
+        }
+        if ( i < Saig_ManPoNum(pAig) )
+            break;        
+    }
+    Aig_ManCleanMarkB(pAig);
+    if ( f == nFrames )
+    {
+        Abc_Print( -1, "Saig_ManPbaDeriveCex(): Internal error! Cannot find a failed primary outputs.\n" );
+        Abc_CexFree( pCex );
+        pCex = NULL;
+    }
+    if ( !Saig_ManVerifyCex( pAig, pCex ) )
+    {
+        Abc_Print( -1, "Saig_ManPbaDeriveCex(): Internal error! Counter-example is invalid.\n" );
+        Abc_CexFree( pCex );
+        pCex = NULL;
     }
     return pCex;
 }
@@ -199,7 +243,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 )
+Vec_Int_t * Saig_ManPbaDerive( Aig_Man_t * pAig, int nInputs, int nFrames, int nConfLimit, int fVerbose, int * piFrame )
 {
     Vec_Int_t * vFlops = NULL, * vMapVar2FF, * vAssumps, * vPiVarMap;
     Aig_Man_t * pFrames;
@@ -248,46 +292,40 @@ Abc_PrintTime( 1, "Solving", clock() - clk );
     {
         if ( RetValue == l_True )
         {
-            printf( "Saig_ManPerformPba(): The eproblem is SAT. Abstraction refinement is still not enabled.\n" );
-/*
             Vec_Int_t * vAbsFfsToAdd;
             ABC_FREE( pAig->pSeqModel );
             pAig->pSeqModel = Saig_ManPbaDeriveCex( pAig, pSat, pCnf, nFrames, vPiVarMap );
+            printf( "The problem is SAT in frame %d. Performing CEX-based refinement.\n", pAig->pSeqModel->iFrame );
+            *piFrame = pAig->pSeqModel->iFrame;
             // CEX is detected - refine the flops
             vAbsFfsToAdd = Saig_ManCbaFilterInputs( pAig, nInputs, pAig->pSeqModel, fVerbose );
             if ( Vec_IntSize(vAbsFfsToAdd) == 0 )
             {
                 Vec_IntFree( vAbsFfsToAdd );
-                return NULL;
+                goto finish;
             }
             if ( fVerbose )
             {
                 printf( "Adding %d registers to the abstraction.  ", Vec_IntSize(vAbsFfsToAdd) );
-                Abc_PrintTime( 0, "Time", clock() - clk );
+                Abc_PrintTime( 1, "Time", clock() - clk );
             }
             vFlops = vAbsFfsToAdd;
-*/
         }
         else
         {
-            printf( "Saig_ManPerformPba(): SAT solver timed out. Abstraction is not changed.\n" );
+            printf( "Saig_ManPerformPba(): SAT solver timed out. Current abstraction is not changed.\n" );
         }
-        Vec_IntFree( vPiVarMap );
-        Vec_IntFree( vAssumps );
-        Vec_IntFree( vMapVar2FF );
-        sat_solver_delete( pSat );
-        Aig_ManStop( pFrames );
-        Cnf_DataFree( pCnf );
-        return NULL;
+        goto finish;
     }
     assert( RetValue == l_False ); // UNSAT
+    *piFrame = nFrames;
 
     // get relevant SAT literals
     nCoreLits = sat_solver_final( pSat, &pCoreLits );
     assert( nCoreLits > 0 );
     if ( fVerbose )
-        printf( "AnalizeFinal selected %d assumptions (out of %d). Conflicts = %d.\n", 
-            nCoreLits, Vec_IntSize(vAssumps), (int)pSat->stats.conflicts );
+        printf( "AnalizeFinal after %d frames selected %d assumptions (out of %d). Conflicts = %d.\n", 
+            nFrames, nCoreLits, Vec_IntSize(vAssumps), (int)pSat->stats.conflicts );
 
     // collect flops
     vFlops = Vec_IntAlloc( nCoreLits );
@@ -300,6 +338,7 @@ Abc_PrintTime( 1, "Solving", clock() - clk );
     Vec_IntSort( vFlops, 0 );
 
     // cleanup
+finish:
     Vec_IntFree( vPiVarMap );
     Vec_IntFree( vAssumps );
     Vec_IntFree( vMapVar2FF );
diff --git a/src/aig/saig/saigAbsStart.c b/src/aig/saig/saigAbsStart.c
index ff813c98..ec933512 100644
--- a/src/aig/saig/saigAbsStart.c
+++ b/src/aig/saig/saigAbsStart.c
@@ -196,7 +196,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) );
-        Abc_PrintTime( 0, "Time", clock() - clk );
+        Abc_PrintTime( 1, "Time", clock() - clk );
     }
     // vFlopsNew contains PI number that should be kept in pAbs
     // add to the abstraction
diff --git a/src/aig/saig/saigBmc3.c b/src/aig/saig/saigBmc3.c
index 4dc0c714..a4567446 100644
--- a/src/aig/saig/saigBmc3.c
+++ b/src/aig/saig/saigBmc3.c
@@ -1292,6 +1292,9 @@ clkOther += clock() - clk2;
             fflush( stdout );
         }
     }
+    // consider the next timeframe
+    if ( RetValue == -1 && pPars->nStart == 0 )
+        pPars->iFrame = f;
 //ABC_PRT( "CNF generation runtime", clkOther );
     if ( pPars->fVerbose )
     {
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 5f680144..637d0cd4 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -881,6 +881,10 @@ void Abc_Init( Abc_Frame_t * pAbc )
         void For_ManFileExperiment();
 //        For_ManFileExperiment();
     }
+    {
+        void Bdc_SpfdDecomposeTest();
+        Bdc_SpfdDecomposeTest();
+    }
 /*
     {
         int i1, i2, i3, i4, i5, i6, N, Counter = 0;
@@ -28437,6 +28441,7 @@ int Abc_CommandAbc9AbsPba( Abc_Frame_t * pAbc, int argc, char ** argv )
     int nFramesMax = (pAbc->nFrames >= 0) ? pAbc->nFrames : 20;
     int nConfMax   = 100000;
     int fVerbose   =      0;
+    int iFrame     =     -1;
     int c;
 
     Extra_UtilGetoptReset();
@@ -28490,8 +28495,10 @@ 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 );
-//    Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexSeq );
+    Gia_ManPbaPerform( pAbc->pGia, nFramesMax, nConfMax, fVerbose, &iFrame );
+    if ( iFrame >= 0 )
+        pAbc->nFrames = iFrame;
+    Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexSeq );
     return 0;
 
 usage:
@@ -28591,7 +28598,8 @@ int Abc_CommandAbc9AbsCba( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 0;
     }
     pAbc->Status = Gia_ManCbaPerform( pAbc->pGia, pPars );
-    pAbc->nFrames = pPars->iFrame;
+    if ( pPars->nStart == 0 )
+        pAbc->nFrames = pPars->iFrame;
     Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexSeq );
     return 0;