Counter-example depth minimization.

3 files changed, 98 insertions, 6 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) );