Added switch 'cexcut -m' to generate bad states for all frames after G.

6 files changed, 164 insertions, 24 deletions

diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index d261e433..9d361fe8 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -316,6 +316,9 @@ static inline void         Gia_ObjSetValue( Gia_Obj_t * pObj, int i )          {
 static inline int          Gia_ObjPhase( Gia_Obj_t * pObj )                    { return pObj->fPhase;                                        }
 static inline int          Gia_ObjPhaseReal( Gia_Obj_t * pObj )                { return Gia_Regular(pObj)->fPhase ^ Gia_IsComplement(pObj);  }
 
+static inline int          Gia_Obj2Lit( Gia_Man_t * p, Gia_Obj_t * pObj )      { return Abc_Var2Lit(Gia_ObjId(p, Gia_Regular(pObj)), Gia_IsComplement(pObj)); }
+static inline Gia_Obj_t *  Gia_Lit2Obj( Gia_Man_t * p, int iLit )              { return Gia_NotCond(Gia_ManObj(p, Abc_Lit2Var(iLit)), Abc_LitIsCompl(iLit));  }
+
 static inline int          Gia_ManIdToCioId( Gia_Man_t * p, int Id )           { return Gia_ObjCioId( Gia_ManObj(p, Id) );                   }
 static inline int          Gia_ManCiIdToId( Gia_Man_t * p, int CiId )          { return Gia_ObjId( p, Gia_ManCi(p, CiId) );                  }
 static inline int          Gia_ManCoIdToId( Gia_Man_t * p, int CoId )          { return Gia_ObjId( p, Gia_ManCo(p, CoId) );                  }
diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c
index eddbd320..3b8980af 100644
--- a/src/aig/gia/giaDup.c
+++ b/src/aig/gia/giaDup.c
@@ -1233,7 +1233,7 @@ Gia_Man_t * Gia_ManDupWithNewPo( Gia_Man_t * p1, Gia_Man_t * p2 )
     // there is no flops in p2
     assert( Gia_ManRegNum(p2) == 0 );
     // there is only one PO in p2
-    assert( Gia_ManPoNum(p2) == 1 );
+//    assert( Gia_ManPoNum(p2) == 1 );
     // input count of p2 is equal to flop count of p1 
     assert( Gia_ManPiNum(p2) == Gia_ManRegNum(p1) );
 
@@ -1255,8 +1255,8 @@ Gia_Man_t * Gia_ManDupWithNewPo( Gia_Man_t * p1, Gia_Man_t * p2 )
     Gia_ManForEachAnd( p2, pObj, i )
         pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
     // add property output
-    pObj = Gia_ManPo( p2, 0 );
-    Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
+    Gia_ManForEachPo( p2, pObj, i )
+        Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
     // add flop inputs
     Gia_ManForEachRi( p1, pObj, i )
         Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index b490d3e3..89d1c6dd 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -22566,6 +22566,9 @@ int Abc_CommandCexLoad( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     ABC_FREE( pAbc->pCex );
     pAbc->pCex = Abc_CexDup( pAbc->pCex2, -1 );
+    // update status
+    pAbc->nFrames = pAbc->pCex2->iFrame;
+    pAbc->Status = 0;
     return 0;
 
 usage:
@@ -22590,13 +22593,14 @@ usage:
 int Abc_CommandCexCut( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     int c;
-    int iFrStart  = 0;
-    int iFrStop   = ABC_INFINITY;
-    int fCombOnly = 0;
-    int fUseOne   = 0;
-    int fVerbose  = 0;
+    int iFrStart   = 0;
+    int iFrStop    = ABC_INFINITY;
+    int fCombOnly  = 0;
+    int fUseOne    = 0;
+    int fAllFrames = 0;
+    int fVerbose   = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "FGcnvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "FGcnmvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -22628,6 +22632,9 @@ int Abc_CommandCexCut( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'n':
             fUseOne ^= 1;
             break;
+        case 'm':
+            fAllFrames ^= 1;
+            break;
         case 'v':
             fVerbose ^= 1;
             break;
@@ -22662,7 +22669,7 @@ int Abc_CommandCexCut( Abc_Frame_t * pAbc, int argc, char ** argv )
         extern Abc_Ntk_t * Abc_NtkFromAigPhase( Aig_Man_t * pMan );
         Abc_Ntk_t * pNtkNew;
         Aig_Man_t * pAig = Abc_NtkToDar( pAbc->pNtkCur, 0, 1 );
-        Aig_Man_t * pAigNew = Bmc_AigTargetStates( pAig, pAbc->pCex, iFrStart, iFrStop, fCombOnly, fUseOne, fVerbose );
+        Aig_Man_t * pAigNew = Bmc_AigTargetStates( pAig, pAbc->pCex, iFrStart, iFrStop, fCombOnly, fUseOne, fAllFrames, fVerbose );
         Aig_ManStop( pAig );
         if ( pAigNew == NULL )
         {
@@ -22687,12 +22694,13 @@ int Abc_CommandCexCut( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: cexcut [-FG num] [-cvh]\n" );
+    Abc_Print( -2, "usage: cexcut [-FG num] [-cnmvh]\n" );
     Abc_Print( -2, "\t         creates logic for bad states using the current CEX\n" );
     Abc_Print( -2, "\t-F num : 0-based number of the starting frame [default = %d]\n", iFrStart );
     Abc_Print( -2, "\t-G num : 0-based number of the ending frame [default = %d]\n",   iFrStop );
     Abc_Print( -2, "\t-c     : toggle outputting unate combinational circuit [default = %s]\n",  fCombOnly? "yes": "no" );
     Abc_Print( -2, "\t-n     : toggle generating only one bad state [default = %s]\n", fUseOne? "yes": "no" );
+    Abc_Print( -2, "\t-m     : toggle generating bad states for all frames after G [default = %s]\n", fAllFrames? "yes": "no" );
     Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n",  fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h     : print the command usage\n");
     return 1;
@@ -22764,7 +22772,7 @@ int Abc_CommandCexMerge( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_Print( 1, "There is no saved cex.\n");
         return 0;
     }
-    if ( iFrStop - iFrStart < pAbc->pCex->iFrame )
+    if ( iFrStop - iFrStart + pAbc->pCex->iPo < pAbc->pCex->iFrame )
     {
         Abc_Print( 1, "Current CEX does not allow to shorten the saved CEX.\n");
         return 0;
diff --git a/src/misc/util/utilCex.c b/src/misc/util/utilCex.c
index edb246b9..01afd489 100644
--- a/src/misc/util/utilCex.c
+++ b/src/misc/util/utilCex.c
@@ -202,9 +202,9 @@ Abc_Cex_t * Abc_CexMerge( Abc_Cex_t * pCex, Abc_Cex_t * pPart, int iFrBeg, int i
     assert( iFrBeg <= iFrEnd );
 
     assert( pCex->nPis == pPart->nPis );
-    assert( iFrEnd - iFrBeg >= pPart->iFrame );
+    assert( iFrEnd - iFrBeg + pPart->iPo >= pPart->iFrame );
 
-    nFramesGain = (iFrEnd - iFrBeg) - pPart->iFrame;
+    nFramesGain = iFrEnd - iFrBeg + pPart->iPo - pPart->iFrame;
     pNew = Abc_CexAlloc( pCex->nRegs, pCex->nPis, pCex->iFrame + 1 - nFramesGain );
     pNew->iPo    = pCex->iPo;
     pNew->iFrame = pCex->iFrame - nFramesGain;
diff --git a/src/sat/bmc/bmc.h b/src/sat/bmc/bmc.h
index 0e37656e..7cc5637b 100644
--- a/src/sat/bmc/bmc.h
+++ b/src/sat/bmc/bmc.h
@@ -75,8 +75,8 @@ extern int               Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFra
 extern void              Saig_ParBmcSetDefaultParams( Saig_ParBmc_t * p );
 extern int               Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars );
 /*=== bmcCexCut.c ==========================================================*/
-extern Gia_Man_t *       Bmc_GiaTargetStates( Gia_Man_t * p, Abc_Cex_t * pCex, int iFrBeg, int iFrEnd, int fCombOnly, int fGenAll, int fVerbose );
-extern Aig_Man_t *       Bmc_AigTargetStates( Aig_Man_t * p, Abc_Cex_t * pCex, int iFrBeg, int iFrEnd, int fCombOnly, int fGenAll, int fVerbose );
+extern Gia_Man_t *       Bmc_GiaTargetStates( Gia_Man_t * p, Abc_Cex_t * pCex, int iFrBeg, int iFrEnd, int fCombOnly, int fGenAll, int fAllFrames, int fVerbose );
+extern Aig_Man_t *       Bmc_AigTargetStates( Aig_Man_t * p, Abc_Cex_t * pCex, int iFrBeg, int iFrEnd, int fCombOnly, int fGenAll, int fAllFrames, int fVerbose );
 /*=== bmcCexMin.c ==========================================================*/
 extern Abc_Cex_t *       Saig_ManCexMinPerform( Aig_Man_t * pAig, Abc_Cex_t * pCex );
 
diff --git a/src/sat/bmc/bmcCexCut.c b/src/sat/bmc/bmcCexCut.c
index 7eafe492..3ce63459 100644
--- a/src/sat/bmc/bmcCexCut.c
+++ b/src/sat/bmc/bmcCexCut.c
@@ -225,7 +225,135 @@ Gia_Man_t * Bmc_GiaGenerateGiaOne( Gia_Man_t * p, Abc_Cex_t * pCex, Vec_Bit_t **
 
 /**Function*************************************************************
 
-  Synopsis    []
+  Synopsis    [Generates all frames from G to the last one.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Man_t * Bmc_GiaGenerateGiaAllFrames( Gia_Man_t * p, Abc_Cex_t * pCex, Vec_Bit_t ** pvInits, int iFrBeg, int iFrEnd )
+{
+    Vec_Bit_t * vInitEnd;
+    Gia_Man_t * pNew, * pTemp;
+    Gia_Obj_t * pObj, * pObjRo, * pObjRi;
+    int f, i, k, iBitOld, iBit = 0, fCompl0, fCompl1;
+
+    // skip trough the first iFrEnd frames
+    Gia_ManCleanMark0(p);
+    Gia_ManForEachRo( p, pObj, k )
+        pObj->fMark0 = Abc_InfoHasBit(pCex->pData, iBit++);
+    *pvInits = Vec_BitStart( Gia_ManRegNum(p) );
+    for ( i = 0; i < iFrEnd; i++ )
+    {
+        // remember values in frame iFrBeg
+        if ( i == iFrBeg )
+            Gia_ManForEachRo( p, pObjRo, k )
+                if ( pObjRo->fMark0 )
+                    Vec_BitWriteEntry( *pvInits, k, 1 );
+        // simulate other values
+        Gia_ManForEachPi( p, pObj, k )
+            pObj->fMark0 = Abc_InfoHasBit(pCex->pData, iBit++);
+        Gia_ManForEachAnd( p, pObj, k )
+            pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) & 
+                           (Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj));
+        Gia_ManForEachCo( p, pObj, k )
+            pObj->fMark0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj);
+        Gia_ManForEachRiRo( p, pObjRi, pObjRo, k )
+            pObjRo->fMark0 = pObjRi->fMark0;
+    }
+    assert( i == iFrEnd );
+    vInitEnd = Vec_BitStart( Gia_ManRegNum(p) );
+    Gia_ManForEachRo( p, pObjRo, k )
+        if ( pObjRo->fMark0 )
+            Vec_BitWriteEntry( vInitEnd, k, 1 );
+
+    // create new AIG manager
+    pNew = Gia_ManStart( 10000 );
+    pNew->pName = Abc_UtilStrsav( p->pName );
+    Gia_ManForEachRo( p, pObjRo, k )
+        Gia_ManAppendCi(pNew);
+    Gia_ManHashStart( pNew );
+
+    Gia_ManConst0(p)->Value = 1;
+    Gia_ManForEachPi( p, pObj, k )
+        pObj->Value = 1;
+
+    iBitOld = iBit;
+    for ( f = iFrEnd; f <= pCex->iFrame; f++ )
+    {
+        // set up correct init state
+        Gia_ManForEachRo( p, pObjRo, k )
+            pObjRo->fMark0 = Vec_BitEntry( vInitEnd, k );
+        // simulate it for a few frames
+        iBit = iBitOld;
+        for ( i = iFrEnd; i < f; i++ )
+        {
+            Gia_ManForEachPi( p, pObj, k )
+                pObj->fMark0 = Abc_InfoHasBit(pCex->pData, iBit++);
+            Gia_ManForEachAnd( p, pObj, k )
+                pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) & 
+                               (Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj));
+            Gia_ManForEachCo( p, pObj, k )
+                pObj->fMark0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj);
+            Gia_ManForEachRiRo( p, pObjRi, pObjRo, k )
+                pObjRo->fMark0 = pObjRi->fMark0;
+        }
+        // start creating values
+        Gia_ManForEachRo( p, pObjRo, k )
+            pObjRo->Value = Abc_LitNotCond( Gia_Obj2Lit(pNew, Gia_ManPi(pNew, k)), !pObjRo->fMark0 );
+        for ( i = f; i <= pCex->iFrame; i++ )
+        {
+            Gia_ManForEachPi( p, pObj, k )
+                pObj->fMark0 = Abc_InfoHasBit(pCex->pData, iBit++);
+            Gia_ManForEachAnd( p, pObj, k )
+            {
+                fCompl0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj);
+                fCompl1 = Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj);
+                pObj->fMark0 = fCompl0 & fCompl1;
+                if ( pObj->fMark0 )
+                    pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0(pObj)->Value, Gia_ObjFanin1(pObj)->Value );
+                else if ( !fCompl0 && !fCompl1 )
+                    pObj->Value = Gia_ManHashOr( pNew, Gia_ObjFanin0(pObj)->Value, Gia_ObjFanin1(pObj)->Value );
+                else if ( !fCompl0 )
+                    pObj->Value = Gia_ObjFanin0(pObj)->Value;
+                else if ( !fCompl1 )
+                    pObj->Value = Gia_ObjFanin1(pObj)->Value;
+                else assert( 0 );
+                assert( pObj->Value > 0 );
+            }
+            Gia_ManForEachCo( p, pObj, k )
+            {
+                pObj->fMark0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj);
+                pObj->Value = Gia_ObjFanin0(pObj)->Value;
+                assert( pObj->Value > 0 );
+            } 
+            if ( i == pCex->iFrame )
+                break;
+            Gia_ManForEachRiRo( p, pObjRi, pObjRo, k )
+            {
+                pObjRo->fMark0 = pObjRi->fMark0;
+                pObjRo->Value = pObjRi->Value;
+            }
+        }
+        assert( iBit == pCex->nBits );
+        // create PO
+        Gia_ManAppendCo( pNew, Gia_ManPo(p, pCex->iPo)->Value );
+    }
+    Gia_ManHashStop( pNew );
+    Vec_BitFree( vInitEnd );
+
+    // cleanup
+    pNew = Gia_ManCleanup( pTemp = pNew );
+    Gia_ManStop( pTemp );
+    return pNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Generates one frame.]
 
   Description []
                
@@ -234,7 +362,7 @@ Gia_Man_t * Bmc_GiaGenerateGiaOne( Gia_Man_t * p, Abc_Cex_t * pCex, Vec_Bit_t **
   SeeAlso     []
 
 ***********************************************************************/
-Gia_Man_t * Bmc_GiaGenerateGiaAll( Gia_Man_t * p, Abc_Cex_t * pCex, Vec_Bit_t ** pvInits, int iFrBeg, int iFrEnd )
+Gia_Man_t * Bmc_GiaGenerateGiaAllOne( Gia_Man_t * p, Abc_Cex_t * pCex, Vec_Bit_t ** pvInits, int iFrBeg, int iFrEnd )
 {
     Gia_Man_t * pNew, * pTemp;
     Gia_Obj_t * pObj, * pObjRo, * pObjRi;
@@ -319,7 +447,6 @@ Gia_Man_t * Bmc_GiaGenerateGiaAll( Gia_Man_t * p, Abc_Cex_t * pCex, Vec_Bit_t **
     return pNew;
 }
 
-
 /**Function*************************************************************
 
   Synopsis    [Generate GIA for target bad states.]
@@ -331,7 +458,7 @@ Gia_Man_t * Bmc_GiaGenerateGiaAll( Gia_Man_t * p, Abc_Cex_t * pCex, Vec_Bit_t **
   SeeAlso     []
 
 ***********************************************************************/
-Gia_Man_t * Bmc_GiaTargetStates( Gia_Man_t * p, Abc_Cex_t * pCex, int iFrBeg, int iFrEnd, int fCombOnly, int fUseOne, int fVerbose )
+Gia_Man_t * Bmc_GiaTargetStates( Gia_Man_t * p, Abc_Cex_t * pCex, int iFrBeg, int iFrEnd, int fCombOnly, int fUseOne, int fAllFrames, int fVerbose )
 {
     Gia_Man_t * pNew, * pTemp;
     Vec_Bit_t * vInitNew;
@@ -352,8 +479,10 @@ Gia_Man_t * Bmc_GiaTargetStates( Gia_Man_t * p, Abc_Cex_t * pCex, int iFrBeg, in
 
     if ( fUseOne )
         pNew = Bmc_GiaGenerateGiaOne( p, pCex, &vInitNew, iFrBeg, iFrEnd );
-    else
-        pNew = Bmc_GiaGenerateGiaAll( p, pCex, &vInitNew, iFrBeg, iFrEnd );
+    else if ( fAllFrames )
+        pNew = Bmc_GiaGenerateGiaAllFrames( p, pCex, &vInitNew, iFrBeg, iFrEnd );
+    else 
+        pNew = Bmc_GiaGenerateGiaAllOne( p, pCex, &vInitNew, iFrBeg, iFrEnd );
 
     if ( !fCombOnly )
     {
@@ -381,7 +510,7 @@ Gia_Man_t * Bmc_GiaTargetStates( Gia_Man_t * p, Abc_Cex_t * pCex, int iFrBeg, in
   SeeAlso     []
 
 ***********************************************************************/
-Aig_Man_t * Bmc_AigTargetStates( Aig_Man_t * p, Abc_Cex_t * pCex, int iFrBeg, int iFrEnd, int fCombOnly, int fUseOne, int fVerbose )
+Aig_Man_t * Bmc_AigTargetStates( Aig_Man_t * p, Abc_Cex_t * pCex, int iFrBeg, int iFrEnd, int fCombOnly, int fUseOne, int fAllFrames, int fVerbose )
 {
     Aig_Man_t * pAig;
     Gia_Man_t * pGia, * pRes;
@@ -392,7 +521,7 @@ Aig_Man_t * Bmc_AigTargetStates( Aig_Man_t * p, Abc_Cex_t * pCex, int iFrBeg, in
         Gia_ManStop( pGia );
         return NULL;
     }
-    pRes = Bmc_GiaTargetStates( pGia, pCex, iFrBeg, iFrEnd, fCombOnly, fUseOne, fVerbose );
+    pRes = Bmc_GiaTargetStates( pGia, pCex, iFrBeg, iFrEnd, fCombOnly, fUseOne, fAllFrames, fVerbose );
     Gia_ManStop( pGia );
     pAig = Gia_ManToAigSimple( pRes );
     Gia_ManStop( pRes );