Added command 'cexcut' and 'cexmerge'.

1 files changed, 102 insertions, 2 deletions

diff --git a/src/sat/bmc/bmcCexCut.c b/src/sat/bmc/bmcCexCut.c
index 79944097..96d46fb3 100644
--- a/src/sat/bmc/bmcCexCut.c
+++ b/src/sat/bmc/bmcCexCut.c
@@ -42,9 +42,109 @@ ABC_NAMESPACE_IMPL_START
   SeeAlso     []
 
 ***********************************************************************/
-Gia_Man_t * Bmc_GiaTargetStates( Gia_Man_t * p, Abc_Cex_t * pCex, int iFrBeg, int iFrEnd )
+Gia_Man_t * Bmc_GiaTargetStates( Gia_Man_t * p, Abc_Cex_t * pCex, int iFrBeg, int iFrEnd, int fVerbose )
 {
-    return NULL;
+    Gia_Man_t * pNew, * pTemp;
+    Gia_Obj_t * pObj, * pObjRo, * pObjRi;
+    Vec_Bit_t * vInitNew;
+    int i, k, iBit = 0;
+
+    if ( iFrBeg < 0 )
+        { printf( "Starting frame is less than 0.\n" ); return NULL; }
+    if ( iFrEnd < 0 )
+        { printf( "Stopping frame is less than 0.\n" ); return NULL; }
+    if ( iFrBeg > pCex->iFrame )
+        { 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 )
+        { 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 );
+
+    // skip trough the first iFrEnd frames
+    Gia_ManCleanMark0(p);
+    Gia_ManForEachRo( p, pObj, i )
+        pObj->fMark0 = Abc_InfoHasBit(pCex->pData, iBit++);
+    vInitNew = 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( vInitNew, 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 );
+
+    // create new AIG manager
+    pNew = Gia_ManStart( 10000 );
+    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 );
+    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));
+            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_ObjFanin0(pObj)->Value;
+            else if ( !Gia_ObjFanin1(pObj)->fMark0 )
+                pObj->Value = Gia_ObjFanin1(pObj)->Value;
+            else assert( 0 );
+        }
+        Gia_ManForEachCo( p, pObj, k )
+        {
+            pObj->fMark0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj);
+            pObj->Value = Gia_ObjFanin0(pObj)->Value;
+        }
+        if ( i == pCex->iFrame )
+            break;
+        Gia_ManForEachRiRo( p, pObjRi, pObjRo, k )
+        {
+            pObjRo->fMark0 = pObjRi->fMark0;
+            pObjRo->Value = pObjRi->Value;
+        }
+    }
+    Gia_ManHashStop( p );
+    assert( iBit == pCex->nBits );
+
+    // create PO
+    Gia_ManAppendCo( pNew, Gia_ManPo(p, pCex->iPo)->Value );
+    // cleanup
+    pNew = Gia_ManCleanup( pTemp = pNew );
+    Gia_ManStop( pTemp );
+
+    // create new GIA
+    pNew = Gia_ManDupWithNewPo( p, pTemp = pNew ); 
+    Gia_ManStop( pTemp );
+
+    // create new initial state
+    pNew = Gia_ManDupFlip( pTemp = pNew, Vec_BitArray(vInitNew) );
+    Gia_ManStop( pTemp );
+    Vec_BitFree( vInitNew );
+    return pNew;
 }
 
 ////////////////////////////////////////////////////////////////////////