Added command 'cexcut' and 'cexmerge'.

src/aig/gia/giaDup.c

@@ -1234,8 +1234,8 @@ Gia_Man_t * Gia_ManDupWithNewPo( Gia_Man_t * p1, Gia_Man_t * p2 )
     assert( Gia_ManRegNum(p2) == 0 );
     // there is only one PO in p2
     assert( Gia_ManPoNum(p2) == 1 );
-    // flop count of p1 is equal to input count of p2
-    assert( Gia_ManRegNum(p1) == Gia_ManPiNum(p2) );
+    // input count of p2 is equal to flop count of p1 
+    assert( Gia_ManPiNum(p2) == Gia_ManRegNum(p1) );
 
     // start new AIG
     pNew = Gia_ManStart( Gia_ManObjNum(p1)+Gia_ManObjNum(p2) );
@@ -1261,7 +1261,7 @@ Gia_Man_t * Gia_ManDupWithNewPo( Gia_Man_t * p1, Gia_Man_t * p2 )
     Gia_ManForEachRi( p1, pObj, i )
         Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
     Gia_ManHashStop( pNew );
-//    Gia_ManPrintStats( pGiaNew, 0 );
+    Gia_ManSetRegNum( pNew, Gia_ManRegNum(p1) );
     pNew = Gia_ManCleanup( pTemp = pNew );
     Gia_ManStop( pTemp );
     return pNew;

src/misc/util/utilCex.c

@@ -195,14 +195,14 @@ Abc_Cex_t * Abc_CexMerge( Abc_Cex_t * pCex, Abc_Cex_t * pPart, int iFrBeg, int i
         { printf( "Starting frame is more than the last frame of CEX (%d).\n", pCex->iFrame ); return NULL; }
     if ( iFrEnd > pCex->iFrame )
         { printf( "Stopping frame is more than the last frame of CEX (%d).\n", pCex->iFrame ); return NULL; }
-    if ( iFrBeg >= iFrEnd )
+    if ( iFrBeg > iFrEnd )
         { printf( "Starting frame (%d) should be less than stopping frame (%d).\n", iFrBeg, iFrEnd ); return NULL; }
     assert( iFrBeg >= 0 && iFrBeg <= pCex->iFrame );
     assert( iFrEnd >= 0 && iFrEnd <= pCex->iFrame );
-    assert( iFrBeg < iFrEnd );
+    assert( iFrBeg <= iFrEnd );
 
     assert( pCex->nPis == pPart->nPis );
-    assert( iFrEnd - iFrBeg > pPart->iFrame );
+    assert( iFrEnd - iFrBeg >= pPart->iFrame );
 
     nFramesGain = (iFrEnd - iFrBeg) - pPart->iFrame;
     pNew = Abc_CexAlloc( pCex->nRegs, pCex->nPis, pCex->iFrame + 1 - nFramesGain );
@@ -211,20 +211,21 @@ Abc_Cex_t * Abc_CexMerge( Abc_Cex_t * pCex, Abc_Cex_t * pPart, int iFrBeg, int i
 
     for ( iBit = 0; iBit < pCex->nRegs; iBit++ )
         if ( Abc_InfoHasBit(pCex->pData, iBit) )
-            Abc_InfoSetBit( pNew->pData, iBit++ );
+            Abc_InfoSetBit( pNew->pData, iBit );
     for ( f = 0; f < iFrBeg; f++ )
-        for ( i = 0; i < pCex->nPis; i++ )
+        for ( i = 0; i < pCex->nPis; i++, iBit++ )
             if ( Abc_InfoHasBit(pCex->pData, pCex->nRegs + pCex->nPis * f + i) )
-                Abc_InfoSetBit( pNew->pData, iBit++ );
+                Abc_InfoSetBit( pNew->pData, iBit );
     for ( f = 0; f < pPart->iFrame; f++ )
-        for ( i = 0; i < pCex->nPis; i++ )
+        for ( i = 0; i < pCex->nPis; i++, iBit++ )
             if ( Abc_InfoHasBit(pPart->pData, pPart->nRegs + pCex->nPis * f + i) )
-                Abc_InfoSetBit( pNew->pData, iBit++ );
+                Abc_InfoSetBit( pNew->pData, iBit );
     for ( f = iFrEnd; f <= pCex->iFrame; f++ )
-        for ( i = 0; i < pCex->nPis; i++ )
-            if ( Abc_InfoHasBit(pPart->pData, pPart->nRegs + pCex->nPis * f + i) )
-                Abc_InfoSetBit( pNew->pData, iBit++ );
+        for ( i = 0; i < pCex->nPis; i++, iBit++ )
+            if ( Abc_InfoHasBit(pCex->pData, pCex->nRegs + pCex->nPis * f + i) )
+                Abc_InfoSetBit( pNew->pData, iBit );
     assert( iBit == pNew->nBits );
+
     return pNew;
 }
 

src/sat/bmc/bmc.h

@@ -76,6 +76,7 @@ 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 fVerbose );
+extern Aig_Man_t *       Bmc_AigTargetStates( Aig_Man_t * p, Abc_Cex_t * pCex, int iFrBeg, int iFrEnd, int fVerbose );
 /*=== bmcCexMin.c ==========================================================*/
 extern Abc_Cex_t *       Saig_ManCexMinPerform( Aig_Man_t * pAig, Abc_Cex_t * pCex );
 

src/sat/bmc/bmcCexCut.c

@@ -6,7 +6,7 @@
 
   PackageName [SAT-based bounded model checking.]
 
-  Synopsis    []
+  Synopsis    [Derives characterization of bad states.]
 
   Author      [Alan Mishchenko]
   
@@ -19,6 +19,7 @@
 ***********************************************************************/
 
 #include "bmc.h"
+#include "aig/gia/giaAig.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -47,7 +48,7 @@ Gia_Man_t * Bmc_GiaTargetStates( Gia_Man_t * p, Abc_Cex_t * pCex, int iFrBeg, in
     Gia_Man_t * pNew, * pTemp;
     Gia_Obj_t * pObj, * pObjRo, * pObjRi;
     Vec_Bit_t * vInitNew;
-    int i, k, iBit = 0;
+    int i, k, iBit = 0, fCompl0, fCompl1;
 
     if ( iFrBeg < 0 )
         { printf( "Starting frame is less than 0.\n" ); return NULL; }
@@ -57,7 +58,7 @@ Gia_Man_t * Bmc_GiaTargetStates( Gia_Man_t * p, Abc_Cex_t * pCex, int iFrBeg, in
         { printf( "Starting frame is more than the last frame of CEX (%d).\n", pCex->iFrame ); return NULL; }
     if ( iFrEnd > pCex->iFrame )
         { printf( "Stopping frame is more than the last frame of CEX (%d).\n", pCex->iFrame ); return NULL; }
-    if ( iFrBeg >= iFrEnd )
+    if ( iFrBeg > iFrEnd )
         { printf( "Starting frame (%d) should be less than stopping frame (%d).\n", iFrBeg, iFrEnd ); return NULL; }
     assert( iFrBeg >= 0 && iFrBeg <= pCex->iFrame );
     assert( iFrEnd >= 0 && iFrEnd <= pCex->iFrame );
@@ -65,7 +66,7 @@ Gia_Man_t * Bmc_GiaTargetStates( Gia_Man_t * p, Abc_Cex_t * pCex, int iFrBeg, in
 
     // skip trough the first iFrEnd frames
     Gia_ManCleanMark0(p);
-    Gia_ManForEachRo( p, pObj, i )
+    Gia_ManForEachRo( p, pObj, k )
         pObj->fMark0 = Abc_InfoHasBit(pCex->pData, iBit++);
     vInitNew = Vec_BitStart( Gia_ManRegNum(p) );
     for ( i = 0; i < iFrEnd; i++ )
@@ -90,34 +91,38 @@ Gia_Man_t * Bmc_GiaTargetStates( Gia_Man_t * p, Abc_Cex_t * pCex, int iFrBeg, in
 
     // create new AIG manager
     pNew = Gia_ManStart( 10000 );
+    pNew->pName = Abc_UtilStrsav( p->pName );
     Gia_ManConst0(p)->Value = 1;
     Gia_ManForEachPi( p, pObj, k )
         pObj->Value = 1;
-    Gia_ManForEachRo( p, pObjRo, i )
-        pObj->Value = Abc_LitNotCond( Gia_ManAppendCi(pNew), !pObjRo->fMark0 );
-    Gia_ManHashStart( p );
+    Gia_ManForEachRo( p, pObjRo, k )
+        pObjRo->Value = Abc_LitNotCond( Gia_ManAppendCi(pNew), !pObjRo->fMark0 );
+    Gia_ManHashStart( pNew );
     for ( i = iFrEnd; i <= pCex->iFrame; 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));
+            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( p, Gia_ObjFanin0(pObj)->Value, Gia_ObjFanin1(pObj)->Value );
-            else if ( !Gia_ObjFanin0(pObj)->fMark0 && !Gia_ObjFanin1(pObj)->fMark0 )
-                pObj->Value = Gia_ManHashOr( p, Gia_ObjFanin0(pObj)->Value, Gia_ObjFanin1(pObj)->Value );
-            else if ( !Gia_ObjFanin0(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 ( !Gia_ObjFanin1(pObj)->fMark0 )
+            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;
@@ -127,7 +132,7 @@ Gia_Man_t * Bmc_GiaTargetStates( Gia_Man_t * p, Abc_Cex_t * pCex, int iFrBeg, in
             pObjRo->Value = pObjRi->Value;
         }
     }
-    Gia_ManHashStop( p );
+    Gia_ManHashStop( pNew );
     assert( iBit == pCex->nBits );
 
     // create PO
@@ -143,10 +148,40 @@ Gia_Man_t * Bmc_GiaTargetStates( Gia_Man_t * p, Abc_Cex_t * pCex, int iFrBeg, in
     // create new initial state
     pNew = Gia_ManDupFlip( pTemp = pNew, Vec_BitArray(vInitNew) );
     Gia_ManStop( pTemp );
+
     Vec_BitFree( vInitNew );
     return pNew;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Generate AIG for target bad states.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Bmc_AigTargetStates( Aig_Man_t * p, Abc_Cex_t * pCex, int iFrBeg, int iFrEnd, int fVerbose )
+{
+    Aig_Man_t * pAig;
+    Gia_Man_t * pGia, * pRes;
+    pGia = Gia_ManFromAigSimple( p );
+    if ( !Gia_ManVerifyCex( pGia, pCex, 0 ) )
+    {
+        Abc_Print( 1, "Current CEX does not fail AIG \"%s\".\n", p->pName );
+        Gia_ManStop( pGia );
+        return NULL;
+    }
+    pRes = Bmc_GiaTargetStates( pGia, pCex, iFrBeg, iFrEnd, fVerbose );
+    pAig = Gia_ManToAigSimple( pRes );
+    Gia_ManStop( pGia );
+    Gia_ManStop( pRes );
+    return pAig;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////