Version abc90410

1 files changed, 292 insertions, 1 deletions

diff --git a/src/aig/gia/giaEquiv.c b/src/aig/gia/giaEquiv.c
index f802e15d..cdee73d0 100644
--- a/src/aig/gia/giaEquiv.c
+++ b/src/aig/gia/giaEquiv.c
@@ -94,7 +94,8 @@ int * Gia_ManDeriveNexts( Gia_Man_t * p )
 {
     unsigned * pNexts, * pTails;
     int i;
-    assert( p->pReprs );
+    assert( p->pReprs != NULL );
+    assert( p->pNexts == NULL );
     pNexts = ABC_CALLOC( unsigned, Gia_ManObjNum(p) );
     pTails = ABC_ALLOC( unsigned, Gia_ManObjNum(p) );
     for ( i = 0; i < Gia_ManObjNum(p); i++ )
@@ -112,6 +113,37 @@ int * Gia_ManDeriveNexts( Gia_Man_t * p )
 
 /**Function*************************************************************
 
+  Synopsis    [Given points to the next objects, derives representatives.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_ManDeriveReprs( Gia_Man_t * p )
+{
+    int i, iObj;
+    assert( p->pReprs == NULL );
+    assert( p->pNexts != NULL );
+    p->pReprs = ABC_CALLOC( Gia_Rpr_t, Gia_ManObjNum(p) );
+    for ( i = 0; i < Gia_ManObjNum(p); i++ )
+        Gia_ObjSetRepr( p, i, GIA_VOID );
+    for ( i = 0; i < Gia_ManObjNum(p); i++ )
+    {
+        if ( p->pNexts[i] == 0 )
+            continue;
+        if ( p->pReprs[i].iRepr != GIA_VOID )
+            continue;
+        // next is set, repr is not set
+        for ( iObj = p->pNexts[i]; iObj; iObj = p->pNexts[iObj] )
+            p->pReprs[iObj].iRepr = i;
+    }
+}
+
+/**Function*************************************************************
+
   Synopsis    []
 
   Description []
@@ -186,6 +218,25 @@ int Gia_ManEquivCountLitsAll( Gia_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
+int Gia_ManEquivCountClasses( Gia_Man_t * p )
+{
+    int i, Counter = 0;
+    for ( i = 1; i < Gia_ManObjNum(p); i++ )
+        Counter += Gia_ObjIsHead(p, i);
+    return Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Gia_ManEquivCheckLits( Gia_Man_t * p, int nLits )
 {
     int nLitsReal = Gia_ManEquivCountLitsAll( p );
@@ -966,6 +1017,246 @@ void Gia_ManEquivImprove( Gia_Man_t * p )
 //    p->pNexts = Gia_ManDeriveNexts( p );
 }
 
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if pOld is in the TFI of pNode.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Gia_ObjCheckTfi_rec( Gia_Man_t * p, Gia_Obj_t * pOld, Gia_Obj_t * pNode, Vec_Ptr_t * vVisited )
+{
+    // check the trivial cases
+    if ( pNode == NULL )
+        return 0;
+    if ( Gia_ObjIsCi(pNode) )
+        return 0;
+//    if ( pNode->Id < pOld->Id ) // cannot use because of choices of pNode
+//        return 0;
+    if ( pNode == pOld )
+        return 1;
+    // skip the visited node
+    if ( pNode->fMark0 )
+        return 0;
+    pNode->fMark0 = 1;
+    Vec_PtrPush( vVisited, pNode );
+    // check the children
+    if ( Gia_ObjCheckTfi_rec( p, pOld, Gia_ObjFanin0(pNode), vVisited ) )
+        return 1;
+    if ( Gia_ObjCheckTfi_rec( p, pOld, Gia_ObjFanin1(pNode), vVisited ) )
+        return 1;
+    // check equivalent nodes
+    return Gia_ObjCheckTfi_rec( p, pOld, Gia_ObjNextObj(p, Gia_ObjId(p, pNode)), vVisited );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if pOld is in the TFI of pNode.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Gia_ObjCheckTfi( Gia_Man_t * p, Gia_Obj_t * pOld, Gia_Obj_t * pNode )
+{
+    Vec_Ptr_t * vVisited;
+    Gia_Obj_t * pObj;
+    int RetValue, i;
+    assert( !Gia_IsComplement(pOld) );
+    assert( !Gia_IsComplement(pNode) );
+    vVisited = Vec_PtrAlloc( 100 );
+    RetValue = Gia_ObjCheckTfi_rec( p, pOld, pNode, vVisited );
+    Vec_PtrForEachEntry( vVisited, pObj, i )
+        pObj->fMark0 = 0;
+    Vec_PtrFree( vVisited );
+    return RetValue;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Adds the next entry while making choices.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_ManAddNextEntry_rec( Gia_Man_t * p, Gia_Obj_t * pOld, Gia_Obj_t * pNode )
+{
+    if ( Gia_ObjNext(p, Gia_ObjId(p, pOld)) == 0 )
+    {
+        Gia_ObjSetNext( p, Gia_ObjId(p, pOld), Gia_ObjId(p, pNode) );
+        return;
+    }
+    Gia_ManAddNextEntry_rec( p, Gia_ObjNextObj(p, Gia_ObjId(p, pOld)), pNode );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Duplicates the AIG in the DFS order.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_ManEquivToChoices_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj )
+{
+    Gia_Obj_t * pRepr, * pReprNew, * pObjNew;
+    if ( ~pObj->Value )
+        return;
+    if ( (pRepr = Gia_ObjReprObj(p, Gia_ObjId(p, pObj))) )
+    {
+        if ( Gia_ObjIsConst0(pRepr) )
+        {
+            pObj->Value = Gia_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) );
+            return;
+        }
+        Gia_ManEquivToChoices_rec( pNew, p, pRepr );
+        assert( Gia_ObjIsAnd(pObj) );
+        Gia_ManEquivToChoices_rec( pNew, p, Gia_ObjFanin0(pObj) );
+        Gia_ManEquivToChoices_rec( pNew, p, Gia_ObjFanin1(pObj) );
+        pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+        if ( Gia_LitRegular(pObj->Value) == Gia_LitRegular(pRepr->Value) )
+        {
+            assert( (int)pObj->Value == Gia_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) ) );
+            return;
+        }
+        assert( pRepr->Value < pObj->Value );
+        pReprNew = Gia_ManObj( pNew, Gia_Lit2Var(pRepr->Value) );
+        pObjNew  = Gia_ManObj( pNew, Gia_Lit2Var(pObj->Value) );
+        if ( Gia_ObjReprObj( pNew, Gia_ObjId(pNew, pObjNew) ) )
+        {
+            assert( Gia_ObjReprObj( pNew, Gia_ObjId(pNew, pObjNew) ) == pReprNew );
+            pObj->Value = Gia_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) );
+            return;
+        }
+        if ( !Gia_ObjCheckTfi( pNew, pReprNew, pObjNew ) )
+        {
+            assert( Gia_ObjNext(pNew, Gia_ObjId(pNew, pObjNew)) == 0 );
+            Gia_ObjSetRepr( pNew, Gia_ObjId(pNew, pObjNew), Gia_ObjId(pNew, pReprNew) );
+            Gia_ManAddNextEntry_rec( pNew, pReprNew, pObjNew ); 
+        }
+        pObj->Value = Gia_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) );
+        return;
+    }
+    assert( Gia_ObjIsAnd(pObj) );
+    Gia_ManEquivToChoices_rec( pNew, p, Gia_ObjFanin0(pObj) );
+    Gia_ManEquivToChoices_rec( pNew, p, Gia_ObjFanin1(pObj) );
+    pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Removes choices, which contain fanouts.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_ManRemoveBadChoices( Gia_Man_t * p )
+{
+    Gia_Obj_t * pObj;
+    int i, iObj, iPrev, Counter = 0;
+    // mark nodes with fanout
+    Gia_ManForEachObj( p, pObj, i )
+    {
+        pObj->fMark0 = 0;
+        if ( Gia_ObjIsAnd(pObj) )
+        {
+            Gia_ObjFanin0(pObj)->fMark0 = 1;
+            Gia_ObjFanin1(pObj)->fMark0 = 1;
+        }
+        else if ( Gia_ObjIsCo(pObj) )
+            Gia_ObjFanin0(pObj)->fMark0 = 1;
+    }
+    // go through the classes and remove 
+    Gia_ManForEachClass( p, i )
+    {
+        for ( iPrev = i, iObj = Gia_ObjNext(p, i); iObj; iObj = Gia_ObjNext(p, iPrev) )
+        {
+            if ( !Gia_ManObj(p, iObj)->fMark0 )
+            {
+                iPrev = iObj; 
+                continue;
+            }
+            Gia_ObjSetRepr( p, iObj, GIA_VOID );
+            Gia_ObjSetNext( p, iPrev, Gia_ObjNext(p, iObj) );
+            Gia_ObjSetNext( p, iObj, 0 );
+            Counter++;
+        } 
+    }
+    // remove the marks
+    Gia_ManCleanMark0( p );
+//    printf( "Removed %d bad choices.\n", Counter );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Reduces AIG using equivalence classes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Man_t * Gia_ManEquivToChoices( Gia_Man_t * p, int nSnapshots )
+{
+    Gia_Man_t * pNew, * pTemp;
+    Gia_Obj_t * pObj, * pRepr;
+    int i;
+    assert( (Gia_ManCoNum(p) % nSnapshots) == 0 );
+    Gia_ManSetPhase( p );
+    pNew = Gia_ManStart( Gia_ManObjNum(p) );
+    pNew->pName = Gia_UtilStrsav( p->pName );
+    pNew->pReprs = ABC_CALLOC( Gia_Rpr_t, Gia_ManObjNum(p) );
+    pNew->pNexts = ABC_CALLOC( int, Gia_ManObjNum(p) );
+    for ( i = 0; i < Gia_ManObjNum(p); i++ )
+        Gia_ObjSetRepr( pNew, i, GIA_VOID );
+    Gia_ManFillValue( p );
+    Gia_ManConst0(p)->Value = 0;
+    Gia_ManForEachCi( p, pObj, i )
+        pObj->Value = Gia_ManAppendCi(pNew);
+    Gia_ManForEachRo( p, pObj, i )
+        if ( (pRepr = Gia_ObjReprObj(p, Gia_ObjId(p, pObj))) )
+        {
+            assert( Gia_ObjIsConst0(pRepr) || Gia_ObjIsRo(p, pRepr) );
+            pObj->Value = pRepr->Value;
+        }
+    Gia_ManHashAlloc( pNew );
+    Gia_ManForEachCo( p, pObj, i )
+        Gia_ManEquivToChoices_rec( pNew, p, Gia_ObjFanin0(pObj) );
+    Gia_ManForEachCo( p, pObj, i )
+        if ( i % nSnapshots == 0 )
+            Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
+    Gia_ManHashStop( pNew );
+    Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
+    Gia_ManRemoveBadChoices( pNew );
+//    Gia_ManEquivPrintClasses( pNew, 0, 0 );
+    pNew = Gia_ManCleanup( pTemp = pNew );
+    Gia_ManStop( pTemp );
+//    Gia_ManEquivPrintClasses( pNew, 0, 0 );
+    return pNew;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////