Added generation of values of internal nodes for GIA manager.

1 files changed, 0 insertions, 91 deletions

diff --git a/src/aig/gia/giaUtil.c b/src/aig/gia/giaUtil.c
index 6f01e5cd..43ef3e08 100644
--- a/src/aig/gia/giaUtil.c
+++ b/src/aig/gia/giaUtil.c
@@ -1183,97 +1183,6 @@ void Gia_ObjPrint( Gia_Man_t * p, Gia_Obj_t * pObj )
 
 /**Function*************************************************************
 
-  Synopsis    [Resimulates the counter-example.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Gia_ManVerifyCex( Gia_Man_t * pAig, Abc_Cex_t * p, int fDualOut )
-{
-    Gia_Obj_t * pObj, * pObjRi, * pObjRo;
-    int RetValue, i, k, iBit = 0;
-    Gia_ManCleanMark0(pAig);
-    Gia_ManForEachRo( pAig, pObj, i )
-        pObj->fMark0 = Abc_InfoHasBit(p->pData, iBit++);
-    for ( i = 0; i <= p->iFrame; i++ )
-    {
-        Gia_ManForEachPi( pAig, pObj, k )
-            pObj->fMark0 = Abc_InfoHasBit(p->pData, iBit++);
-        Gia_ManForEachAnd( pAig, pObj, k )
-            pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) & 
-                           (Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj));
-        Gia_ManForEachCo( pAig, pObj, k )
-            pObj->fMark0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj);
-        if ( i == p->iFrame )
-            break;
-        Gia_ManForEachRiRo( pAig, pObjRi, pObjRo, k )
-        {
-            pObjRo->fMark0 = pObjRi->fMark0;
-        }
-    }
-    assert( iBit == p->nBits );
-    if ( fDualOut )
-        RetValue = Gia_ManPo(pAig, 2*p->iPo)->fMark0 ^ Gia_ManPo(pAig, 2*p->iPo+1)->fMark0;
-    else
-        RetValue = Gia_ManPo(pAig, p->iPo)->fMark0;
-    Gia_ManCleanMark0(pAig);
-    return RetValue;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Resimulates the counter-example.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Gia_ManFindFailedPoCex( Gia_Man_t * pAig, Abc_Cex_t * p, int nOutputs )
-{
-    Gia_Obj_t * pObj, * pObjRi, * pObjRo;
-    int RetValue, i, k, iBit = 0;
-    assert( Gia_ManPiNum(pAig) == p->nPis );
-    Gia_ManCleanMark0(pAig);
-//    Gia_ManForEachRo( pAig, pObj, i )
-//       pObj->fMark0 = Abc_InfoHasBit(p->pData, iBit++);
-    iBit = p->nRegs;
-    for ( i = 0; i <= p->iFrame; i++ )
-    {
-        Gia_ManForEachPi( pAig, pObj, k )
-            pObj->fMark0 = Abc_InfoHasBit(p->pData, iBit++);
-        Gia_ManForEachAnd( pAig, pObj, k )
-            pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) & 
-                           (Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj));
-        Gia_ManForEachCo( pAig, pObj, k )
-            pObj->fMark0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj);
-        Gia_ManForEachRiRo( pAig, pObjRi, pObjRo, k )
-            pObjRo->fMark0 = pObjRi->fMark0;
-    }
-    assert( iBit == p->nBits );
-    // figure out the number of failed output
-    RetValue = -1;
-//    for ( i = Gia_ManPoNum(pAig) - 1; i >= nOutputs; i-- )
-    for ( i = nOutputs; i < Gia_ManPoNum(pAig); i++ )
-    {
-        if ( Gia_ManPo(pAig, i)->fMark0 )
-        {
-            RetValue = i;
-            break;
-        }
-    }
-    Gia_ManCleanMark0(pAig);
-    return RetValue;
-}
-
-/**Function*************************************************************
-
   Synopsis    [Complements the constraint outputs.]
 
   Description []