Counter-example depth minimization.

6 files changed, 552 insertions, 16 deletions

diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index 12d255a4..c890b165 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -343,6 +343,7 @@ static inline int          Gia_ManObjIsConst0( Gia_Man_t * p, Gia_Obj_t * 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_ManCiLit( Gia_Man_t * p, int CiId )             { return Gia_Obj2Lit( p, Gia_ManCi(p, CiId) );                }
 
 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) );                  }
@@ -897,13 +898,15 @@ extern Gia_Man_t *         Gia_ManDupOrderDfsReverse( Gia_Man_t * p );
 extern Gia_Man_t *         Gia_ManDupOutputGroup( Gia_Man_t * p, int iOutStart, int iOutStop );
 extern Gia_Man_t *         Gia_ManDupOutputVec( Gia_Man_t * p, Vec_Int_t * vOutPres );
 extern Gia_Man_t *         Gia_ManDupOrderAiger( Gia_Man_t * p );
+extern Gia_Man_t *         Gia_ManDupLastPis( Gia_Man_t * p, int nLastPis );
 extern Gia_Man_t *         Gia_ManDupFlip( Gia_Man_t * p, int * pInitState );
-extern Gia_Man_t *         Gia_ManDupCycled( Gia_Man_t * pAig, int nFrames );
+extern Gia_Man_t *         Gia_ManDupCycled( Gia_Man_t * pAig, Abc_Cex_t * pCex, int nFrames );
 extern Gia_Man_t *         Gia_ManDup( Gia_Man_t * p );  
 extern Gia_Man_t *         Gia_ManDupPerm( Gia_Man_t * p, Vec_Int_t * vPiPerm );
 extern void                Gia_ManDupAppend( Gia_Man_t * p, Gia_Man_t * pTwo );
 extern void                Gia_ManDupAppendShare( Gia_Man_t * p, Gia_Man_t * pTwo );
 extern Gia_Man_t *         Gia_ManDupAppendNew( Gia_Man_t * pOne, Gia_Man_t * pTwo );
+extern Gia_Man_t *         Gia_ManDupAppendCones( Gia_Man_t * p, Gia_Man_t ** ppCones, int nCones, int fOnlyRegs );
 extern Gia_Man_t *         Gia_ManDupSelf( Gia_Man_t * p );
 extern Gia_Man_t *         Gia_ManDupFlopClass( Gia_Man_t * p, int iClass );
 extern Gia_Man_t *         Gia_ManDupMarked( Gia_Man_t * p );
diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c
index 2c7fd59b..d533dc1f 100644
--- a/src/aig/gia/giaDup.c
+++ b/src/aig/gia/giaDup.c
@@ -385,6 +385,36 @@ Gia_Man_t * Gia_ManDupOrderAiger( Gia_Man_t * p )
 
 /**Function*************************************************************
 
+  Synopsis    [Duplicates AIG while putting first PIs, then nodes, then POs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Man_t * Gia_ManDupLastPis( Gia_Man_t * p, int nLastPis )
+{
+    Gia_Man_t * pNew;
+    Gia_Obj_t * pObj;
+    int i;
+    assert( Gia_ManRegNum(p) == 0 );
+    pNew = Gia_ManStart( Gia_ManObjNum(p) );
+    pNew->pName = Abc_UtilStrsav( p->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
+    Gia_ManConst0(p)->Value = 0;
+    Gia_ManForEachCi( p, pObj, i )
+        pObj->Value = (i < Gia_ManCiNum(p) - nLastPis) ? ~0 : Gia_ManAppendCi(pNew);
+    Gia_ManForEachAnd( p, pObj, i )
+        pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+    Gia_ManForEachCo( p, pObj, i )
+        pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
+    return pNew;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Duplicates AIG while complementing the flops.]
 
   Description [The array of initial state contains the init state
@@ -438,16 +468,17 @@ Gia_Man_t * Gia_ManDupFlip( Gia_Man_t * p, int * pInitState )
   SeeAlso     []
 
 ***********************************************************************/
-void Gia_ManCycle( Gia_Man_t * p, int nFrames )
+void Gia_ManCycle( Gia_Man_t * p, Abc_Cex_t * pCex, int nFrames )
 {
     Gia_Obj_t * pObj, * pObjRi, * pObjRo;
     int i, k;
     Gia_ManRandom( 1 );
+    assert( pCex == NULL || nFrames <= pCex->iFrame );
     // iterate for the given number of frames
     for ( i = 0; i < nFrames; i++ )
     {
         Gia_ManForEachPi( p, pObj, k )
-            pObj->fMark0 = (1 & Gia_ManRandom(0));
+            pObj->fMark0 = pCex ? Abc_InfoHasBit(pCex->pData, pCex->nRegs+i*pCex->nPis+k) : (1 & Gia_ManRandom(0));
         Gia_ManForEachAnd( p, pObj, k )
             pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) & 
                            (Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj));
@@ -457,14 +488,14 @@ void Gia_ManCycle( Gia_Man_t * p, int nFrames )
             pObjRo->fMark0 = pObjRi->fMark0;
     }
 }
-Gia_Man_t * Gia_ManDupCycled( Gia_Man_t * p, int nFrames )
+Gia_Man_t * Gia_ManDupCycled( Gia_Man_t * p, Abc_Cex_t * pCex, int nFrames )
 {
     Gia_Man_t * pNew;
     Vec_Bit_t * vInits;
     Gia_Obj_t * pObj;
     int i;
     Gia_ManCleanMark0(p);
-    Gia_ManCycle( p, nFrames );
+    Gia_ManCycle( p, pCex, nFrames );
     vInits = Vec_BitAlloc( Gia_ManRegNum(p) );
     Gia_ManForEachRo( p, pObj, i )
         Vec_BitPush( vInits, pObj->fMark0 );
@@ -651,6 +682,60 @@ Gia_Man_t * Gia_ManDupAppendNew( Gia_Man_t * pOne, Gia_Man_t * pTwo )
 
 /**Function*************************************************************
 
+  Synopsis    [Appends logic cones as additional property outputs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Man_t * Gia_ManDupAppendCones( Gia_Man_t * p, Gia_Man_t ** ppCones, int nCones, int fOnlyRegs )
+{
+    Gia_Man_t * pNew, * pOne;
+    Gia_Obj_t * pObj;
+    int i, k;
+    pNew = Gia_ManStart( Gia_ManObjNum(p) );
+    pNew->pName = Abc_UtilStrsav( p->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
+    Gia_ManHashAlloc( pNew );
+    Gia_ManConst0(p)->Value = 0;
+    Gia_ManForEachCi( p, pObj, i )
+        pObj->Value = Gia_ManAppendCi( pNew );
+    Gia_ManForEachAnd( p, pObj, i )
+        pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+    Gia_ManForEachPo( p, pObj, i )
+        pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
+    for ( k = 0; k < nCones; k++ )
+    {
+        pOne = ppCones[k];
+        assert( Gia_ManPoNum(pOne) == 1 );
+        assert( Gia_ManRegNum(pOne) == 0 );
+        if ( fOnlyRegs )
+            assert( Gia_ManPiNum(pOne) == Gia_ManRegNum(p) );
+        else
+            assert( Gia_ManPiNum(pOne) == Gia_ManCiNum(p) );
+        Gia_ManConst0(pOne)->Value = 0;
+        Gia_ManForEachPi( pOne, pObj, i )
+            pObj->Value = Gia_ManCiLit( pNew, fOnlyRegs ? Gia_ManPiNum(p) + i : i );
+        Gia_ManForEachAnd( pOne, pObj, i )
+            pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+        Gia_ManForEachPo( pOne, pObj, i )
+            pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
+    }
+    Gia_ManForEachRi( p, pObj, i )
+        pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
+    Gia_ManHashStop( pNew );
+    Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
+    pNew = Gia_ManCleanup( pOne = pNew );
+    Gia_ManStop( pOne );
+    return pNew;
+}
+
+
+/**Function*************************************************************
+
   Synopsis    [Duplicates while adding self-loops to the registers.]
 
   Description []
diff --git a/src/aig/gia/giaMan.c b/src/aig/gia/giaMan.c
index 8670993d..5738595b 100644
--- a/src/aig/gia/giaMan.c
+++ b/src/aig/gia/giaMan.c
@@ -245,11 +245,15 @@ void Gia_ManPrintTents( Gia_Man_t * p )
     printf( "Tents:  " );
     for ( t = 1; nSizePrev < Vec_IntSize(vObjs); t++ )
     {
+        int nPis = 0;
         nSizeCurr = Vec_IntSize(vObjs);
         Vec_IntForEachEntryStartStop( vObjs, iObjId, i, nSizePrev, nSizeCurr )
+        {
+            nPis += Gia_ObjIsPi(p, Gia_ManObj(p, iObjId));
             if ( Gia_ObjIsRo(p, Gia_ManObj(p, iObjId)) )
                 Gia_ManPrintTents_rec( p, Gia_ObjRoToRi(p, Gia_ManObj(p, iObjId)), vObjs );
-        printf( "%d=%d  ", t, nSizeCurr - nSizePrev );
+        }
+        printf( "%d=%d(%d)  ", t, nSizeCurr - nSizePrev, nPis );
         nSizePrev = nSizeCurr;
     }
     printf( " Unused=%d\n", Gia_ManObjNum(p) - Vec_IntSize(vObjs) );
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index d28a59ea..f8404f19 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -21460,7 +21460,7 @@ int Abc_CommandBmc3( Abc_Frame_t * pAbc, int argc, char ** argv )
         }
     }
     vStatuses = Abc_FrameDeriveStatusArray( vSeqModelVec );
-    Abc_FrameReplacePoStatuses( pAbc, &vStatuses );
+    Abc_FrameReplacePoStatuses( pAbc, &vStatuses );        
     if ( vSeqModelVec )
         Abc_FrameReplaceCexVec( pAbc, &vSeqModelVec );
     else
@@ -23013,11 +23013,11 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv )
     // run the procedure
     pAbc->Status  = Abc_NtkDarPdr( pNtk, pPars );
     pAbc->nFrames = pNtk->vSeqModelVec ? -1 : pPars->iFrame;
+    Abc_FrameReplacePoStatuses( pAbc, &pPars->vOutMap );
     if ( pNtk->vSeqModelVec )
         Abc_FrameReplaceCexVec( pAbc, &pNtk->vSeqModelVec );
     else
         Abc_FrameReplaceCex( pAbc, &pNtk->pSeqModel );
-    Abc_FrameReplacePoStatuses( pAbc, &pPars->vOutMap );
     return 0;
 
 usage:
@@ -30250,9 +30250,9 @@ usage:
 int Abc_CommandAbc9Cycle( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     Gia_Man_t * pTemp;
-    int c, nFrames = 10, fVerbose = 0;
+    int c, nFrames = 10, fUseCex = 0, fVerbose = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "Fvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Fcvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -30267,6 +30267,9 @@ int Abc_CommandAbc9Cycle( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( nFrames < 0 )
                 goto usage;
             break;
+        case 'c':
+            fUseCex ^= 1;
+            break;
         case 'v':
             fVerbose ^= 1;
             break;
@@ -30281,15 +30284,16 @@ int Abc_CommandAbc9Cycle( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_Print( -1, "Abc_CommandAbc9Cycle(): There is no AIG.\n" );
         return 1;
     }
-    pTemp = Gia_ManDupCycled( pAbc->pGia, nFrames );
+    pTemp = Gia_ManDupCycled( pAbc->pGia, fUseCex ? pAbc->pCex : NULL, nFrames );
     Abc_FrameUpdateGia( pAbc, pTemp );
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &cycle [-F num] [-vh]\n" );
+    Abc_Print( -2, "usage: &cycle [-F num] [-cvh]\n" );
     Abc_Print( -2, "\t         cycles sequential circuit for the given number of timeframes\n" );
     Abc_Print( -2, "\t         to derive a new initial state (which may be on the envelope)\n" );
     Abc_Print( -2, "\t-F num : the number of frames to simulate [default = %d]\n", nFrames );
+    Abc_Print( -2, "\t-c     : toggle using PI values from the current CEX [default = %s]\n", fUseCex? "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;
@@ -31934,6 +31938,7 @@ int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     Gia_Man_t * pTemp = NULL;
     int c, fVerbose = 0;
+    int nFrames = 3;
     int fSwitch = 0;
 //    extern Gia_Man_t * Gia_VtaTest( Gia_Man_t * p );
 //    extern int Gia_ManSuppSizeTest( Gia_Man_t * p );
@@ -31947,13 +31952,26 @@ int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv )
 //    extern int Gia_ManVerify( Gia_Man_t * pGia );
 //    extern Gia_Man_t * Gia_ManOptimizeRing( Gia_Man_t * p );
 //    extern void Gia_ManCollectSeqTest( Gia_Man_t * p );
-    extern Gia_Man_t * Gia_SweeperFraigTest( Gia_Man_t * p, int nWords, int nConfs, int fVerbose );
+//    extern Gia_Man_t * Gia_SweeperFraigTest( Gia_Man_t * p, int nWords, int nConfs, int fVerbose );
+    extern Gia_Man_t * Bmc_CexDepthTest( Gia_Man_t * p, Abc_Cex_t * pCex, int nFrames, int fVerbose );
+    extern Gia_Man_t * Bmc_CexTarget( Gia_Man_t * p, int nFrames );
 
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "svh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Fsvh" ) ) != EOF )
     {
         switch ( c )
         {
+        case 'F':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nFrames = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nFrames < 0 )
+                goto usage;
+            break;
         case 's':
             fSwitch ^= 1;
             break;
@@ -32001,12 +32019,16 @@ int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv )
 //    Gia_ManVerifyWithBoxes( pAbc->pGia );
 //    Gia_ManCollectSeqTest( pAbc->pGia );
 //    pTemp = Gia_ManOptimizeRing( pAbc->pGia );
-    pTemp = Gia_SweeperFraigTest( pAbc->pGia, 4, 1000, 0 );
+//    pTemp = Gia_SweeperFraigTest( pAbc->pGia, 4, 1000, 0 );
+//    Abc_FrameUpdateGia( pAbc, pTemp );
+    pTemp = Bmc_CexDepthTest( pAbc->pGia, pAbc->pCex, nFrames, fVerbose );
+//    pTemp = Bmc_CexTarget( pAbc->pGia, nFrames );
     Abc_FrameUpdateGia( pAbc, pTemp );
     return 0;
 usage:
-    Abc_Print( -2, "usage: &test [-svh]\n" );
+    Abc_Print( -2, "usage: &test [-F num] [-svh]\n" );
     Abc_Print( -2, "\t        testing various procedures\n" );
+    Abc_Print( -2, "\t-F num: the number of timeframes [default = %d]\n", nFrames );
     Abc_Print( -2, "\t-s    : toggle enable (yes) vs. disable (no) [default = %s]\n", fSwitch? "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");
diff --git a/src/sat/bmc/bmcCexDepth.c b/src/sat/bmc/bmcCexDepth.c
new file mode 100644
index 00000000..b28a7ba7
--- /dev/null
+++ b/src/sat/bmc/bmcCexDepth.c
@@ -0,0 +1,421 @@
+/**CFile****************************************************************
+
+  FileName    [bmcCexDepth.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [SAT-based bounded model checking.]
+
+  Synopsis    [CEX depth minimization.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: bmcCexDepth.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "bmc.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+extern Abc_Cex_t * Bmc_CexInnerStates( Gia_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t ** ppCexImpl, int fVerbose );
+extern Abc_Cex_t * Bmc_CexCareBits( Gia_Man_t * p, Abc_Cex_t * pCexState, Abc_Cex_t * pCexImpl, Abc_Cex_t * pCexEss, int fFindAll, int fVerbose );
+extern int Bmc_CexVerify( Gia_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexCare );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+
+/**Function*************************************************************
+
+  Synopsis    [Existentially quantified given variable.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Man_t * Gia_ManDupExist( Gia_Man_t * p, int iVar )
+{
+    Gia_Man_t * pNew, * pTemp;
+    Gia_Obj_t * pObj;
+    int i;
+    assert( iVar >= 0 && iVar < Gia_ManPiNum(p) );
+    assert( Gia_ManPoNum(p) == 1 );
+    assert( Gia_ManRegNum(p) == 0 );
+    Gia_ManFillValue( p );
+    // find the cofactoring variable
+    pNew = Gia_ManStart( Gia_ManObjNum(p) );
+    pNew->pName = Abc_UtilStrsav( p->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
+    Gia_ManHashAlloc( pNew );
+    // compute negative cofactor
+    Gia_ManConst0(p)->Value = 0;
+    Gia_ManForEachCi( p, pObj, i )
+        pObj->Value = Gia_ManAppendCi(pNew);
+    Gia_ManPi( p, iVar )->Value = Abc_Var2Lit( 0, 1 );
+    Gia_ManForEachAnd( p, pObj, i )
+        pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+    Gia_ManForEachPo( p, pObj, i )
+        pObj->Value = Gia_ObjFanin0Copy(pObj);
+    // compute the positive cofactor
+    Gia_ManPi( p, iVar )->Value = Abc_Var2Lit( 0, 0 );
+    Gia_ManForEachAnd( p, pObj, i )
+        pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+    // create OR gate
+    Gia_ManForEachPo( p, pObj, i )
+        pObj->Value = Gia_ManAppendCo( pNew, Gia_ManHashOr(pNew, pObj->Value, Gia_ObjFanin0Copy(pObj)) );
+    Gia_ManHashStop( pNew );
+    pNew = Gia_ManCleanup( pTemp = pNew );
+    Gia_ManStop( pTemp );
+    return pNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs targe enlargement of the given size.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Man_t * Bmc_CexTargetEnlarge( Gia_Man_t * p, int nFrames )
+{
+    Gia_Man_t * pNew, * pOne;
+    Gia_Obj_t * pObj, * pObjRo;
+    int i, k;
+    pNew = Gia_ManStart( Gia_ManObjNum(p) );
+    pNew->pName = Abc_UtilStrsav( p->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
+    Gia_ManHashAlloc( pNew );
+    Gia_ManConst0(p)->Value = 0;
+    for ( k = 0; k < nFrames; k++ )
+        Gia_ManForEachPi( p, pObj, i )
+            Gia_ManAppendCi( pNew );
+    Gia_ManForEachRo( p, pObj, i )
+        pObj->Value = Gia_ManAppendCi( pNew );
+    for ( k = 0; k < nFrames; k++ )
+    {
+        Gia_ManForEachPi( p, pObj, i )
+            pObj->Value = Gia_ManCiLit( pNew, (nFrames - 1 - k) * Gia_ManPiNum(p) + i );
+        Gia_ManForEachAnd( p, pObj, i )
+            pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+        Gia_ManForEachRi( p, pObj, i )
+            pObj->Value = Gia_ObjFanin0Copy(pObj);
+        Gia_ManForEachRiRo( p, pObj, pObjRo, i )
+            pObjRo->Value  = pObj->Value;
+    }
+    pObj = Gia_ManPo( p, 0 );
+    pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
+    Gia_ManHashStop( pNew );
+    pNew = Gia_ManCleanup( pOne = pNew );
+    Gia_ManStop( pOne );
+    return pNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Create target with quantified inputs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Man_t * Bmc_CexTarget( Gia_Man_t * p, int nFrames )
+{
+    Gia_Man_t * pNew, * pTemp;
+    int i, Limit = nFrames * Gia_ManPiNum(p);
+    pNew = Bmc_CexTargetEnlarge( p, nFrames );
+    for ( i = 0; i < Limit; i++ )
+    {
+        printf( "%3d : ", i );
+        if ( i % Gia_ManPiNum(p) == 0 )
+            Gia_ManPrintStats( pNew, 0, 0, 0 );
+        pNew = Gia_ManDupExist( pTemp = pNew, i );
+        Gia_ManStop( pTemp );
+    }
+    Gia_ManPrintStats( pNew, 0, 0, 0 );
+    pNew = Gia_ManDupLastPis( pTemp = pNew, Gia_ManRegNum(p) );
+    Gia_ManStop( pTemp );  
+    Gia_ManPrintStats( pNew, 0, 0, 0 );
+    pTemp = Gia_ManDupAppendCones( p, &pNew, 1, 1 );
+    Gia_ManStop( pNew );
+    Gia_AigerWrite( pTemp, "miter3.aig", 0, 0 );
+    return pTemp;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes CE-induced network.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Man_t * Bmc_CexBuildNetwork2( Gia_Man_t * p, Abc_Cex_t * pCex, int fStart )
+{
+    Gia_Man_t * pNew, * pTemp;
+    Gia_Obj_t * pObj, * pObjRo, * pObjRi;
+    int fCompl0, fCompl1;
+    int i, k, iBit;
+    assert( pCex->nRegs == 0 );
+    assert( pCex->nPis == Gia_ManCiNum(p) );
+    assert( fStart <= pCex->iFrame );
+    // start the manager
+    pNew = Gia_ManStart( 1000 );
+    pNew->pName = Abc_UtilStrsav( "unate" );
+    // set const0
+    Gia_ManConst0(p)->fMark0 = 0; // value
+    Gia_ManConst0(p)->fMark1 = 1; // care
+    Gia_ManConst0(p)->Value  = ~0;
+    // set init state
+    Gia_ManForEachRi( p, pObj, k )
+    {
+        pObj->fMark0 = Abc_InfoHasBit( pCex->pData, pCex->nRegs + fStart * Gia_ManCiNum(p) + Gia_ManPiNum(p) + k );
+        pObj->fMark1 = 0;
+        pObj->Value  = Abc_LitNotCond( Gia_ManAppendCi(pNew), !pObj->fMark0 );
+    }
+    Gia_ManHashAlloc( pNew );
+    iBit = pCex->nRegs + fStart * Gia_ManCiNum(p);
+    for ( i = fStart; i <= pCex->iFrame; i++ )
+    {
+        //  primary inputs
+        Gia_ManForEachPi( p, pObj, k )
+        {
+            pObj->fMark0 = Abc_InfoHasBit( pCex->pData, iBit++ );
+            pObj->fMark1 = 1;
+            pObj->Value  = ~0;
+        }
+        iBit += Gia_ManRegNum(p);
+        // transfer 
+        Gia_ManForEachRiRo( p, pObjRi, pObjRo, k )
+        {
+            pObjRo->fMark0 = pObjRi->fMark0;
+            pObjRo->fMark1 = pObjRi->fMark1;
+            pObjRo->Value  = pObjRi->Value;
+        }
+        // internal nodes
+        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->fMark1 = Gia_ObjFanin0(pObj)->fMark1 & Gia_ObjFanin1(pObj)->fMark1;
+            else if ( !fCompl0 && !fCompl1 )
+                pObj->fMark1 = Gia_ObjFanin0(pObj)->fMark1 | Gia_ObjFanin1(pObj)->fMark1;
+            else if ( !fCompl0 )
+                pObj->fMark1 = Gia_ObjFanin0(pObj)->fMark1;
+            else if ( !fCompl1 )
+                pObj->fMark1 = Gia_ObjFanin1(pObj)->fMark1;
+            else assert( 0 );
+            pObj->Value = ~0;
+            if ( pObj->fMark1 )
+                continue;
+            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 );
+        }
+        // combinational outputs
+        Gia_ManForEachCo( p, pObj, k )
+        {
+            pObj->fMark0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj);
+            pObj->fMark1 = Gia_ObjFanin0(pObj)->fMark1;
+            pObj->Value  = Gia_ObjFanin0(pObj)->Value;
+        }
+    }
+    Gia_ManHashStop( pNew );
+    assert( iBit == pCex->nBits );
+    // create primary output
+    pObj = Gia_ManPo(p, pCex->iPo);
+    assert( pObj->fMark0 == 1 );
+    assert( pObj->fMark1 == 0 );
+    assert( pObj->Value > 0 );
+    Gia_ManAppendCo( pNew, pObj->Value );
+    // cleanup
+    pNew = Gia_ManCleanup( pTemp = pNew );
+    Gia_ManStop( pTemp );
+    return pNew;
+}
+Gia_Man_t * Bmc_CexBuildNetwork2_( Gia_Man_t * p, Abc_Cex_t * pCex, int fStart )
+{
+    Gia_Man_t * pNew, * pTemp;
+    Gia_Obj_t * pObj, * pObjRo, * pObjRi;
+    int fCompl0, fCompl1;
+    int i, k, iBit;
+    assert( pCex->nRegs == 0 );
+    assert( pCex->nPis == Gia_ManCiNum(p) );
+    assert( fStart <= pCex->iFrame );
+    // start the manager
+    pNew = Gia_ManStart( 1000 );
+    pNew->pName = Abc_UtilStrsav( "unate" );
+    // set const0
+    Gia_ManConst0(p)->fMark0 = 0; // value
+    Gia_ManConst0(p)->Value  = 1;
+    // set init state
+    Gia_ManForEachRi( p, pObj, k )
+    {
+        pObj->fMark0 = Abc_InfoHasBit( pCex->pData, pCex->nRegs + fStart * Gia_ManCiNum(p) + Gia_ManPiNum(p) + k );
+        pObj->Value  = Abc_LitNotCond( Gia_ManAppendCi(pNew), !pObj->fMark0 );
+    }
+    Gia_ManHashAlloc( pNew );
+    iBit = pCex->nRegs + fStart * Gia_ManCiNum(p);
+    for ( i = fStart; i <= pCex->iFrame; i++ )
+    {
+        //  primary inputs
+        Gia_ManForEachPi( p, pObj, k )
+        {
+            pObj->fMark0 = Abc_InfoHasBit( pCex->pData, iBit++ );
+            pObj->Value  = 1;
+        }
+        iBit += Gia_ManRegNum(p);
+        // transfer 
+        Gia_ManForEachRiRo( p, pObjRi, pObjRo, k )
+        {
+            pObjRo->fMark0 = pObjRi->fMark0;
+            pObjRo->Value  = pObjRi->Value;
+        }
+        // internal nodes
+        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 );
+        }
+        // combinational outputs
+        Gia_ManForEachCo( p, pObj, k )
+        {
+            pObj->fMark0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj);
+            pObj->Value  = Gia_ObjFanin0(pObj)->Value;
+        }
+    }
+    Gia_ManHashStop( pNew );
+    assert( iBit == pCex->nBits );
+    // create primary output
+    pObj = Gia_ManPo(p, pCex->iPo);
+    assert( pObj->fMark0 == 1 );
+    assert( pObj->Value > 0 );
+    Gia_ManAppendCo( pNew, pObj->Value );
+    // cleanup
+    pNew = Gia_ManCleanup( pTemp = pNew );
+    Gia_ManStop( pTemp );
+    return pNew;
+}
+
+Gia_Man_t * Bmc_CexBuildNetwork2Test( Gia_Man_t * p, Abc_Cex_t * pCex, int nFramesMax )
+{
+    Gia_Man_t * pNew, * pTemp;
+    Vec_Ptr_t * vCones;
+    clock_t clk = clock();
+    int i;
+    nFramesMax = Abc_MinInt( nFramesMax, pCex->iFrame );
+    printf( "Processing CEX in frame %d (max frames %d).\n", pCex->iFrame, nFramesMax );
+    vCones = Vec_PtrAlloc( nFramesMax );
+    for ( i = pCex->iFrame; i > pCex->iFrame - nFramesMax; i-- )
+    {
+        printf( "Frame %5d : ", i );
+        pNew = Bmc_CexBuildNetwork2_( p, pCex, i );
+        Gia_ManPrintStats( pNew, 0, 0, 0 );
+        Vec_PtrPush( vCones, pNew );
+    }
+    pNew = Gia_ManDupAppendCones( p, (Gia_Man_t **)Vec_PtrArray(vCones), Vec_PtrSize(vCones), 1 );
+    Gia_AigerWrite( pNew, "miter2.aig", 0, 0 );
+//Bmc_CexDumpAogStats( pNew, clock() - clk );
+    Vec_PtrForEachEntry( Gia_Man_t *, vCones, pTemp, i )
+        Gia_ManStop( pTemp );
+    Vec_PtrFree( vCones );
+    printf( "GIA with additional properties is written into \"miter2.aig\".\n" );
+//    printf( "CE-induced network is written into file \"unate.aig\".\n" );
+    Abc_PrintTime( 1, "Time", clock() - clk );
+//    Gia_ManStop( pNew );
+    return pNew;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Man_t * Bmc_CexDepthTest( Gia_Man_t * p, Abc_Cex_t * pCex, int nFrames, int fVerbose )
+{
+    Gia_Man_t * pNew;
+    clock_t clk = clock();
+    Abc_Cex_t * pCexImpl   = NULL;
+    Abc_Cex_t * pCexStates = Bmc_CexInnerStates( p, pCex, &pCexImpl, fVerbose );
+    Abc_Cex_t * pCexCare   = Bmc_CexCareBits( p, pCexStates, pCexImpl, NULL, 1, fVerbose );
+//    Abc_Cex_t * pCexEss, * pCexMin;
+
+    if ( !Bmc_CexVerify( p, pCex, pCexCare ) )
+        printf( "Counter-example care-set verification has failed.\n" );
+
+//    pCexEss = Bmc_CexEssentialBits( p, pCexStates, pCexCare, fVerbose );
+//    pCexMin = Bmc_CexCareBits( p, pCexStates, pCexImpl, pCexEss, 0, fVerbose );
+
+//    if ( !Bmc_CexVerify( p, pCex, pCexMin ) )
+//        printf( "Counter-example min-set verification has failed.\n" );
+
+//    Bmc_CexDumpStats( p, pCex, pCexCare, pCexEss, pCexMin, clock() - clk );
+
+    Abc_PrintTime( 1, "Time", clock() - clk );
+    pNew = Bmc_CexBuildNetwork2Test( p, pCexStates, nFrames );
+//    Bmc_CexPerformUnrollingTest( p, pCex );
+
+    Abc_CexFreeP( &pCexStates );
+    Abc_CexFreeP( &pCexImpl );
+    Abc_CexFreeP( &pCexCare );
+//    Abc_CexFreeP( &pCexEss );
+//    Abc_CexFreeP( &pCexMin );
+    return pNew;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/sat/bmc/module.make b/src/sat/bmc/module.make
index fd50ec23..1ac04203 100644
--- a/src/sat/bmc/module.make
+++ b/src/sat/bmc/module.make
@@ -2,6 +2,7 @@ SRC +=    src/sat/bmc/bmcBmc.c \
     src/sat/bmc/bmcBmc2.c \
     src/sat/bmc/bmcBmc3.c \
     src/sat/bmc/bmcCexCut.c \
+    src/sat/bmc/bmcCexDepth.c \
     src/sat/bmc/bmcCexMin1.c \
     src/sat/bmc/bmcCexMin2.c \
     src/sat/bmc/bmcCexTools.c \