Several bug fixes.

6 files changed, 163 insertions, 59 deletions

diff --git a/src/aig/gia/giaAbs.c b/src/aig/gia/giaAbs.c
index fca680a5..8c89859c 100644
--- a/src/aig/gia/giaAbs.c
+++ b/src/aig/gia/giaAbs.c
@@ -227,52 +227,6 @@ Vec_Int_t * Gia_ManFlopsSelect( Vec_Int_t * vFlops, Vec_Int_t * vFlopsNew )
 
 /**Function*************************************************************
 
-  Synopsis    [Derive unrolled timeframes.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Gia_ManPbaPerform( Gia_Man_t * pGia, int nFrames, int nConfLimit, int fVerbose )
-{
-    Gia_Man_t * pAbs;
-    Aig_Man_t * pAig;
-    Vec_Int_t * vFlops, * vFlopsNew, * vSelected;
-    if ( pGia->vFlopClasses == NULL )
-    {
-        printf( "Gia_ManPbaPerform(): Abstraction flop map is missing.\n" );
-        return 0;
-    }
-    // derive abstraction
-    pAbs = Gia_ManDupAbstraction( pGia, pGia->vFlopClasses );
-    // refine abstraction using PBA
-    pAig = Gia_ManToAigSimple( pAbs );
-    Gia_ManStop( pAbs );
-    vFlopsNew = Saig_ManPbaDerive( pAig, nFrames, nConfLimit, fVerbose );
-    Aig_ManStop( pAig );
-    // derive new classes
-    if ( vFlopsNew != NULL )
-    {
-        vFlops = Gia_ManClasses2Flops( pGia->vFlopClasses );
-        vSelected = Gia_ManFlopsSelect( vFlops, vFlopsNew );
-        Vec_IntFree( pGia->vFlopClasses );
-        pGia->vFlopClasses = Saig_ManFlops2Classes( Gia_ManRegNum(pGia), vSelected );
-        Vec_IntFree( vSelected );
-
-        Vec_IntFree( vFlopsNew );
-        Vec_IntFree( vFlops );
-        return 1;
-    }
-    // found counter-eample for the abstracted model
-    // or exceeded conflict limit
-    return 0;
-}
-
-/**Function*************************************************************
-
   Synopsis    [Adds flops that should be present in the abstraction.]
 
   Description [The second argument (vAbsFfsToAdd) is the array of numbers
@@ -350,6 +304,71 @@ int Gia_ManCbaPerform( Gia_Man_t * pGia, void * p )
     return -1;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Derive unrolled timeframes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Gia_ManPbaPerform( Gia_Man_t * pGia, int nFrames, int nConfLimit, int fVerbose )
+{
+    Gia_Man_t * pAbs;
+    Aig_Man_t * pAig, * pOrig;
+    Vec_Int_t * vFlops, * vFlopsNew, * vSelected;
+    if ( pGia->vFlopClasses == NULL )
+    {
+        printf( "Gia_ManPbaPerform(): Abstraction flop map is missing.\n" );
+        return 0;
+    }
+    // derive abstraction
+    pAbs = Gia_ManDupAbstraction( pGia, pGia->vFlopClasses );
+    // refine abstraction using PBA
+    pAig = Gia_ManToAigSimple( pAbs );
+    Gia_ManStop( pAbs );
+    vFlopsNew = Saig_ManPbaDerive( pAig, Gia_ManPiNum(pGia), nFrames, nConfLimit, fVerbose );
+    Aig_ManStop( pAig );
+    // derive new classes
+    if ( pAig->pSeqModel == NULL )
+    {
+        // the problem is UNSAT
+        vFlops = Gia_ManClasses2Flops( pGia->vFlopClasses );
+        vSelected = Gia_ManFlopsSelect( vFlops, vFlopsNew );
+        Vec_IntFree( pGia->vFlopClasses );
+        pGia->vFlopClasses = Saig_ManFlops2Classes( Gia_ManRegNum(pGia), vSelected );
+        Vec_IntFree( vSelected );
+
+        Vec_IntFree( vFlopsNew );
+        Vec_IntFree( vFlops );
+        return -1;
+    }
+    else if ( vFlopsNew == NULL )
+    {
+        // found real counter-example
+        assert( pAig->pSeqModel != NULL );
+        printf( "Refinement did not happen. Discovered a true counter-example.\n" );
+        printf( "Remapping counter-example from %d to %d primary inputs.\n", Aig_ManPiNum(pAig), Gia_ManPiNum(pGia) );
+        // derive new counter-example
+        pOrig = Gia_ManToAigSimple( pGia );
+        pGia->pCexSeq = Saig_ManCexRemap( pOrig, pAig, pAig->pSeqModel );
+        Aig_ManStop( pOrig );
+        Aig_ManStop( pAig );
+        return 0;
+    }
+    else
+    {
+        // found counter-eample for the abstracted model
+        // update flop classes
+        Vec_Int_t * vAbsFfsToAdd = vFlopsNew;
+        Gia_ManFlopsAddToClasses( pGia->vFlopClasses, vAbsFfsToAdd );
+        Vec_IntFree( vAbsFfsToAdd );
+        return -1;
+    }
+}
 
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/saig/saig.h b/src/aig/saig/saig.h
index 4437413f..f20641a5 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 nFrames, int nConfLimit, int fVerbose );
+extern Vec_Int_t *       Saig_ManPbaDerive( Aig_Man_t * pAig, int nInputs, int nFrames, int nConfLimit, int fVerbose );
 /*=== 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/saigAbsPba.c b/src/aig/saig/saigAbsPba.c
index a22871b7..3f8fb222 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 )
+Aig_Man_t * Saig_ManUnrollForPba( Aig_Man_t * pAig, int nFrames, Vec_Int_t ** pvPiVarMap )
 {
     Aig_Man_t * pFrames;     // unrolled timeframes
     Vec_Vec_t * vFrameCos;   // the list of COs per frame
@@ -107,6 +107,7 @@ Aig_Man_t * Saig_ManUnrollForPba( Aig_Man_t * pAig, int nFrames )
     Saig_ManForEachLo( pAig, pObj, i )
         pObj->pData = Aig_Mux( pFrames, Aig_ManPi(pFrames,i), Aig_ObjCreatePi(pFrames), Aig_ManConst0(pFrames) );
     // iterate through the frames
+    *pvPiVarMap = Vec_IntStartFull( nFrames * Saig_ManPiNum(pAig) );
     pObjNew = Aig_ManConst0(pFrames);
     for ( f = 0; f < nFrames; f++ )
     {
@@ -119,7 +120,10 @@ Aig_Man_t * Saig_ManUnrollForPba( Aig_Man_t * pAig, int nFrames )
             else if ( Aig_ObjIsPo(pObj) )
                 pObj->pData = Aig_ObjChild0Copy(pObj);
             else if ( Saig_ObjIsPi(pAig, pObj) )
+            {
+                Vec_IntWriteEntry( *pvPiVarMap, f * Saig_ManPiNum(pAig) + Aig_ObjPioNum(pObj), Aig_ManPiNum(pFrames) );
                 pObj->pData = Aig_ObjCreatePi( pFrames );
+            }
             else if ( Aig_ObjIsConst1(pObj) )
                 pObj->pData = Aig_ManConst1(pFrames);
             else if ( !Saig_ObjIsLo(pAig, pObj) )
@@ -155,6 +159,37 @@ Aig_Man_t * Saig_ManUnrollForPba( Aig_Man_t * pAig, int nFrames )
 
 /**Function*************************************************************
 
+  Synopsis    [Derives the counter-example from the SAT solver.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+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 );   
+    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
+    for ( f = 0; f < nFrames; f++ )
+    {
+//        Aig_ManForEach
+    }
+    return pCex;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Derive unrolled timeframes.]
 
   Description []
@@ -164,9 +199,9 @@ Aig_Man_t * Saig_ManUnrollForPba( Aig_Man_t * pAig, int nFrames )
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Int_t * Saig_ManPbaDerive( Aig_Man_t * pAig, int nFrames, int nConfLimit, int fVerbose )
+Vec_Int_t * Saig_ManPbaDerive( Aig_Man_t * pAig, int nInputs, int nFrames, int nConfLimit, int fVerbose )
 {
-    Vec_Int_t * vFlops, * vMapVar2FF, * vAssumps;
+    Vec_Int_t * vFlops, * vMapVar2FF, * vAssumps, * vPiVarMap;
     Aig_Man_t * pFrames;
     sat_solver * pSat;
     Cnf_Dat_t * pCnf;
@@ -176,7 +211,7 @@ Vec_Int_t * Saig_ManPbaDerive( Aig_Man_t * pAig, int nFrames, int nConfLimit, in
 
     // create SAT solver
 clk = clock();
-    pFrames = Saig_ManUnrollForPba( pAig, nFrames );
+    pFrames = Saig_ManUnrollForPba( pAig, nFrames, &vPiVarMap );
 if ( fVerbose )
 Aig_ManPrintStats( pFrames );
 //    pCnf = Cnf_DeriveSimple( pFrames, 0 );
@@ -212,9 +247,29 @@ Abc_PrintTime( 1, "Solving", clock() - clk );
     if ( RetValue != l_False )
     {
         if ( RetValue == l_True )
-            printf( "Saig_ManPerformPba(): Internal Error!!! The resulting problem is SAT.\n" );
+        {
+            Vec_Int_t * vAbsFfsToAdd;
+            ABC_FREE( pAig->pSeqModel );
+            pAig->pSeqModel = Saig_ManPbaDeriveCex( pAig, pSat, pCnf, nFrames, vPiVarMap );
+            // CEX is detected - refine the flops
+            vAbsFfsToAdd = Saig_ManCbaFilterInputs( pAig, nInputs, pAig->pSeqModel, fVerbose );
+            if ( Vec_IntSize(vAbsFfsToAdd) == 0 )
+            {
+                Vec_IntFree( vAbsFfsToAdd );
+                return NULL;
+            }
+            if ( fVerbose )
+            {
+                printf( "Adding %d registers to the abstraction.  ", Vec_IntSize(vAbsFfsToAdd) );
+                Abc_PrintTime( 0, "Time", clock() - clk );
+            }
+            return vAbsFfsToAdd;
+        }
         else
-            printf( "Saig_ManPerformPba(): SAT solver timed out.\n" );
+        {
+            printf( "Saig_ManPerformPba(): SAT solver timed out. Abstraction is not changed.\n" );
+        }
+        Vec_IntFree( vPiVarMap );
         Vec_IntFree( vAssumps );
         Vec_IntFree( vMapVar2FF );
         sat_solver_delete( pSat );
@@ -242,6 +297,7 @@ Abc_PrintTime( 1, "Solving", clock() - clk );
     Vec_IntSort( vFlops, 0 );
 
     // cleanup
+    Vec_IntFree( vPiVarMap );
     Vec_IntFree( vAssumps );
     Vec_IntFree( vMapVar2FF );
     sat_solver_delete( pSat );
diff --git a/src/aig/ssw/sswRarity.c b/src/aig/ssw/sswRarity.c
index 24cfe65d..037dfe55 100644
--- a/src/aig/ssw/sswRarity.c
+++ b/src/aig/ssw/sswRarity.c
@@ -899,7 +899,7 @@ int Ssw_RarSimulate( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, in
     if ( Aig_ManNodeNum(pAig) == 0 )
         return -1;
     // check trivially SAT miters
-    if ( Ssw_RarCheckTrivial( pAig, fVerbose ) )
+    if ( fMiter && Ssw_RarCheckTrivial( pAig, fVerbose ) )
         return 0;
     if ( fVerbose )
         printf( "Rarity simulation with %d words, %d frames, %d rounds, %d seed, and %d sec timeout.\n", 
@@ -1006,7 +1006,7 @@ int Ssw_RarSignalFilter( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize
     if ( Aig_ManNodeNum(pAig) == 0 )
         return -1;
     // check trivially SAT miters
-    if ( Ssw_RarCheckTrivial( pAig, 1 ) )
+    if ( fMiter && Ssw_RarCheckTrivial( pAig, 1 ) )
         return 0;
     if ( fVerbose )
         printf( "Rarity equiv filtering with %d words, %d frames, %d rounds, %d seed, and %d sec timeout.\n", 
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index ebeafa86..3b0cbb06 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -1824,9 +1824,9 @@ int Abc_NtkDarBmc3( Abc_Ntk_t * pNtk, Saig_ParBmc_t * pPars )
                 printf( "(timeout %d sec). ", pPars->nTimeOut );
             else
                 printf( "(conf limit %d). ", pPars->nConfLimit );
-            if ( pNtk->vSeqModelVec )
-                Vec_PtrFreeFree( pNtk->vSeqModelVec );
-            pNtk->vSeqModelVec = pMan->vSeqModelVec;  pMan->vSeqModelVec = NULL;
+//            if ( pNtk->vSeqModelVec )
+//                Vec_PtrFreeFree( pNtk->vSeqModelVec );
+//            pNtk->vSeqModelVec = pMan->vSeqModelVec;  pMan->vSeqModelVec = NULL;
         }
     }
     else // if ( RetValue == 0 )
@@ -1838,7 +1838,17 @@ int Abc_NtkDarBmc3( Abc_Ntk_t * pNtk, Saig_ParBmc_t * pPars )
         }
         else
         {
-            printf( "All %d outputs are proved SAT.    ", Saig_ManPoNum(pMan) - pMan->nConstrs );
+            int nOutputs = Saig_ManPoNum(pMan) - Saig_ManConstrNum(pMan);
+            if ( Vec_PtrCountZero(pMan->vSeqModelVec) == 0 )
+                printf( "All %d outputs are found to be SAT.   ", nOutputs );
+            else if ( Vec_PtrCountZero(pMan->vSeqModelVec) == nOutputs )
+                printf( "None of the %d outputs is found to be SAT.   ", nOutputs );
+            else
+                printf( "Some outputs (%d out of %d) are proved SAT.   ", 
+                    nOutputs - Vec_PtrCountZero(pMan->vSeqModelVec), nOutputs );
+            if ( pNtk->vSeqModelVec )
+                Vec_PtrFreeFree( pNtk->vSeqModelVec );
+            pNtk->vSeqModelVec = pMan->vSeqModelVec;  pMan->vSeqModelVec = NULL;
         }
     }
     ABC_PRT( "Time", clock() - clk );
diff --git a/src/misc/vec/vecPtr.h b/src/misc/vec/vecPtr.h
index 9915f2d6..fe4b00b2 100644
--- a/src/misc/vec/vecPtr.h
+++ b/src/misc/vec/vecPtr.h
@@ -298,6 +298,25 @@ static inline int Vec_PtrSize( Vec_Ptr_t * p )
   SeeAlso     []
 
 ***********************************************************************/
+static inline int Vec_PtrCountZero( Vec_Ptr_t * p ) 
+{
+    int i, Counter = 0;
+    for ( i = 0; i < p->nSize; i++ )
+        Counter += (p->pArray[i] == NULL);
+    return Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 static inline void * Vec_PtrEntry( Vec_Ptr_t * p, int i )
 {
     assert( i >= 0 && i < p->nSize );