Cleaing AIG manager by removing pointers to HAIG.

5 files changed, 1 insertions, 141 deletions

diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h
index 3e682391..9953cf6a 100644
--- a/src/aig/aig/aig.h
+++ b/src/aig/aig/aig.h
@@ -66,7 +66,7 @@ typedef enum {
 } Aig_Type_t;
 
 // the AIG node
-struct Aig_Obj_t_  // 9 words
+struct Aig_Obj_t_  // 8 words
 {
     union {                         
         Aig_Obj_t *  pNext;          // strashing table
@@ -74,7 +74,6 @@ struct Aig_Obj_t_  // 9 words
     };
     Aig_Obj_t *      pFanin0;        // fanin
     Aig_Obj_t *      pFanin1;        // fanin
-    Aig_Obj_t *      pHaig;          // pointer to the HAIG node
     unsigned int     Type    :  3;   // object type
     unsigned int     fPhase  :  1;   // value under 000...0 pattern
     unsigned int     fMarkA  :  1;   // multipurpose mask
@@ -156,7 +155,6 @@ struct Aig_Man_t_
     Vec_Ptr_t *      vSeqModelVec;   // vector of counter-examples (for sequential miters)
     Aig_Man_t *      pManExdc;
     Vec_Ptr_t *      vOnehots;
-    Aig_Man_t *      pManHaig;
     int              fCreatePios;
     Vec_Int_t *      vEquPairs;   
     Vec_Vec_t *      vClockDoms; 
@@ -326,7 +324,6 @@ static inline Aig_Obj_t *  Aig_ObjEquiv( Aig_Man_t * p, Aig_Obj_t * pObj )    {
 static inline void         Aig_ObjSetEquiv( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pEqu ) { assert(p->pEquivs); p->pEquivs[pObj->Id] = pEqu;                  }
 static inline Aig_Obj_t *  Aig_ObjRepr( Aig_Man_t * p, Aig_Obj_t * pObj )     { return p->pReprs? p->pReprs[pObj->Id] : NULL;             } 
 static inline void         Aig_ObjSetRepr( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pRepr )     { assert(p->pReprs); p->pReprs[pObj->Id] = pRepr;                                } 
-static inline Aig_Obj_t *  Aig_ObjHaig( Aig_Obj_t * pObj )        { assert( Aig_Regular(pObj)->pHaig ); return Aig_NotCond( Aig_Regular(pObj)->pHaig, Aig_IsComplement(pObj) );      } 
 static inline int          Aig_ObjWhatFanin( Aig_Obj_t * pObj, Aig_Obj_t * pFanin )    
 { 
     if ( Aig_ObjFanin0(pObj) == pFanin ) return 0; 
diff --git a/src/aig/aig/aigDup.c b/src/aig/aig/aigDup.c
index 9d87db92..67b71d61 100644
--- a/src/aig/aig/aigDup.c
+++ b/src/aig/aig/aigDup.c
@@ -49,7 +49,6 @@ Aig_Man_t * Aig_ManDupSimple( Aig_Man_t * p )
     Aig_Obj_t * pObj, * pObjNew;
     int i;
     assert( p->pManTime == NULL );
-    assert( p->pManHaig == NULL || Aig_ManBufNum(p) == 0 );
     // create the new manager
     pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
     pNew->pName = Abc_UtilStrsav( p->pName );
@@ -61,11 +60,9 @@ Aig_Man_t * Aig_ManDupSimple( Aig_Man_t * p )
     // create the PIs
     Aig_ManCleanData( p );
     Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
-    Aig_ManConst1(pNew)->pHaig = Aig_ManConst1(p)->pHaig;
     Aig_ManForEachCi( p, pObj, i )
     {
         pObjNew = Aig_ObjCreateCi( pNew );
-        pObjNew->pHaig = pObj->pHaig;
         pObjNew->Level = pObj->Level;
         pObj->pData = pObjNew;
     }
@@ -74,30 +71,21 @@ Aig_Man_t * Aig_ManDupSimple( Aig_Man_t * p )
         if ( Aig_ObjIsBuf(pObj) )
         {
             pObjNew = Aig_ObjChild0Copy(pObj);
-            Aig_Regular(pObjNew)->pHaig = pObj->pHaig;
             pObj->pData = pObjNew;
         }
         else if ( Aig_ObjIsNode(pObj) )
         {
             pObjNew = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
-            Aig_Regular(pObjNew)->pHaig = pObj->pHaig;
             pObj->pData = pObjNew;
         }
     // add the POs
     Aig_ManForEachCo( p, pObj, i )
     {
         pObjNew = Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) );
-        pObjNew->pHaig = pObj->pHaig;
         pObj->pData = pObjNew;
     }
     assert( Aig_ManBufNum(p) != 0 || Aig_ManNodeNum(p) == Aig_ManNodeNum(pNew) );
     Aig_ManSetRegNum( pNew, Aig_ManRegNum(p) );
-    // pass the HAIG manager
-    if ( p->pManHaig != NULL )
-    {
-        pNew->pManHaig = p->pManHaig;  
-        p->pManHaig = NULL;
-    }
     // check the resulting network
     if ( !Aig_ManCheck(pNew) )
         printf( "Aig_ManDupSimple(): The check has failed.\n" );
@@ -120,7 +108,6 @@ Aig_Man_t * Aig_ManDupSimpleWithHints( Aig_Man_t * p, Vec_Int_t * vHints )
     Aig_Man_t * pNew;
     Aig_Obj_t * pObj;
     int i, Entry;
-    assert( p->pManHaig == NULL || Aig_ManBufNum(p) == 0 );
     assert( p->nAsserts == 0 || p->nConstrs == 0 );
     // create the new manager
     pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
@@ -175,7 +162,6 @@ Aig_Obj_t * Aig_ManDupSimpleDfs_rec( Aig_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t
         return (Aig_Obj_t *)(pObj->pData = Aig_ObjChild0Copy(pObj));
     Aig_ManDupSimpleDfs_rec( pNew, p, Aig_ObjFanin1(pObj) );
     pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
-    Aig_Regular((Aig_Obj_t *)pObj->pData)->pHaig = pObj->pHaig;
     return (Aig_Obj_t *)pObj->pData;
 }
 
@@ -200,7 +186,6 @@ Aig_Man_t * Aig_ManDupSimpleDfs( Aig_Man_t * p )
     Aig_Obj_t * pObj, * pObjNew;
     int i;
     assert( p->pManTime == NULL );
-    assert( p->pManHaig == NULL || Aig_ManBufNum(p) == 0 );
     // create the new manager
     pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
     pNew->pName = Abc_UtilStrsav( p->pName );
@@ -212,11 +197,9 @@ Aig_Man_t * Aig_ManDupSimpleDfs( Aig_Man_t * p )
     // create the PIs
     Aig_ManCleanData( p );
     Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
-    Aig_ManConst1(pNew)->pHaig = Aig_ManConst1(p)->pHaig;
     Aig_ManForEachCi( p, pObj, i )
     {
         pObjNew = Aig_ObjCreateCi( pNew );
-        pObjNew->pHaig = pObj->pHaig;
         pObjNew->Level = pObj->Level;
         pObj->pData = pObjNew;
     }
@@ -231,17 +214,10 @@ Aig_Man_t * Aig_ManDupSimpleDfs( Aig_Man_t * p )
     Aig_ManForEachCo( p, pObj, i )
     {
         pObjNew = Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) );
-        pObjNew->pHaig = pObj->pHaig;
         pObj->pData = pObjNew;
     }
     assert( Aig_ManBufNum(p) != 0 || Aig_ManNodeNum(p) == Aig_ManNodeNum(pNew) );
     Aig_ManSetRegNum( pNew, Aig_ManRegNum(p) );
-    // pass the HAIG manager
-    if ( p->pManHaig != NULL )
-    {
-        pNew->pManHaig = p->pManHaig;  
-        p->pManHaig = NULL;
-    }
     // check the resulting network
     if ( !Aig_ManCheck(pNew) )
         printf( "Aig_ManDupSimple(): The check has failed.\n" );
@@ -337,7 +313,6 @@ Aig_Man_t * Aig_ManDupOrdered( Aig_Man_t * p )
         }
         else
             assert( 0 );
-        Aig_Regular(pObjNew)->pHaig = pObj->pHaig;
         pObj->pData = pObjNew;
     }
     assert( Aig_ManBufNum(p) != 0 || Aig_ManNodeNum(p) == Aig_ManNodeNum(pNew) );
@@ -347,12 +322,6 @@ Aig_Man_t * Aig_ManDupOrdered( Aig_Man_t * p )
     // duplicate the timing manager
     if ( p->pManTime )
         pNew->pManTime = Tim_ManDup( (Tim_Man_t *)p->pManTime, 0 );
-    // pass the HAIG manager
-    if ( p->pManHaig != NULL )
-    {
-        pNew->pManHaig = p->pManHaig;  
-        p->pManHaig = NULL;
-    }
     // check the resulting network
     if ( !Aig_ManCheck(pNew) )
         printf( "Aig_ManDupOrdered(): The check has failed.\n" );
@@ -376,7 +345,6 @@ Aig_Man_t * Aig_ManDupCof( Aig_Man_t * p, int iInput, int Value )
     Aig_Obj_t * pObj, * pObjNew;
     int i;
     assert( p->pManTime == NULL );
-    assert( p->pManHaig == NULL || Aig_ManBufNum(p) == 0 );
     // create the new manager
     pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
     pNew->pName = Abc_UtilStrsav( p->pName );
@@ -388,7 +356,6 @@ Aig_Man_t * Aig_ManDupCof( Aig_Man_t * p, int iInput, int Value )
     // create the PIs
     Aig_ManCleanData( p );
     Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
-    Aig_ManConst1(pNew)->pHaig = Aig_ManConst1(p)->pHaig;
     Aig_ManForEachCi( p, pObj, i )
     {
         if ( i == iInput )
@@ -396,7 +363,6 @@ Aig_Man_t * Aig_ManDupCof( Aig_Man_t * p, int iInput, int Value )
         else
         {
             pObjNew = Aig_ObjCreateCi( pNew );
-            pObjNew->pHaig = pObj->pHaig;
             pObjNew->Level = pObj->Level;
         }
         pObj->pData = pObjNew;
@@ -406,31 +372,22 @@ Aig_Man_t * Aig_ManDupCof( Aig_Man_t * p, int iInput, int Value )
         if ( Aig_ObjIsBuf(pObj) )
         {
             pObjNew = Aig_ObjChild0Copy(pObj);
-            Aig_Regular(pObjNew)->pHaig = pObj->pHaig;
             pObj->pData = pObjNew;
         }
         else if ( Aig_ObjIsNode(pObj) )
         {
             pObjNew = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
-            Aig_Regular(pObjNew)->pHaig = pObj->pHaig;
             pObj->pData = pObjNew;
         }
     // add the POs
     Aig_ManForEachCo( p, pObj, i )
     {
         pObjNew = Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) );
-        pObjNew->pHaig = pObj->pHaig;
         pObj->pData = pObjNew;
     }
 //    assert( Aig_ManBufNum(p) != 0 || Aig_ManNodeNum(p) == Aig_ManNodeNum(pNew) );
     Aig_ManCleanup( pNew );
     Aig_ManSetRegNum( pNew, Aig_ManRegNum(p) );
-    // pass the HAIG manager
-    if ( p->pManHaig != NULL )
-    {
-        pNew->pManHaig = p->pManHaig;  
-        p->pManHaig = NULL;
-    }
     // check the resulting network
     if ( !Aig_ManCheck(pNew) )
         printf( "Aig_ManDupSimple(): The check has failed.\n" );
@@ -539,7 +496,6 @@ Aig_Man_t * Aig_ManDupExor( Aig_Man_t * p )
         }
         else
             assert( 0 );
-        Aig_Regular(pObjNew)->pHaig = pObj->pHaig;
         pObj->pData = pObjNew;
     }
     Aig_ManCleanup( pNew );
@@ -576,10 +532,6 @@ Aig_Obj_t * Aig_ManDupDfs_rec( Aig_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t * pObj
         return (Aig_Obj_t *)(pObj->pData = Aig_ObjChild0Copy(pObj));
     Aig_ManDupDfs_rec( pNew, p, Aig_ObjFanin1(pObj) );
     pObjNew = Aig_Oper( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj), Aig_ObjType(pObj) );
-    if ( p->pManHaig != NULL )
-        Aig_Regular(pObjNew)->pHaig = Aig_NotCond( pObj->pHaig, Aig_IsComplement(pObjNew) );
-    else if ( pObj->pHaig )
-        Aig_Regular(pObjNew)->pHaig = pObj->pHaig;
     if ( pEquivNew )
     {
         assert( Aig_Regular(pEquivNew)->Id < Aig_Regular(pObjNew)->Id );
@@ -624,14 +576,12 @@ Aig_Man_t * Aig_ManDupDfs( Aig_Man_t * p )
     Aig_ManCleanData( p );
     // duplicate internal nodes
     Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
-    Aig_ManConst1(pNew)->pHaig = Aig_ManConst1(p)->pHaig;
     Aig_ManForEachObj( p, pObj, i )
     {
         if ( Aig_ObjIsCi(pObj) )
         {
             pObjNew = Aig_ObjCreateCi( pNew );
             pObjNew->Level = pObj->Level;
-            pObjNew->pHaig = pObj->pHaig;
             pObj->pData = pObjNew;
         }
         else if ( Aig_ObjIsCo(pObj) )
@@ -639,7 +589,6 @@ Aig_Man_t * Aig_ManDupDfs( Aig_Man_t * p )
             Aig_ManDupDfs_rec( pNew, p, Aig_ObjFanin0(pObj) );        
 //            assert( pObj->Level == ((Aig_Obj_t*)pObj->pData)->Level );
             pObjNew = Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) );
-            pObjNew->pHaig = pObj->pHaig;
             pObj->pData = pObjNew;
         }
     }
@@ -650,12 +599,6 @@ Aig_Man_t * Aig_ManDupDfs( Aig_Man_t * p )
     // duplicate the timing manager
     if ( p->pManTime )
         pNew->pManTime = Tim_ManDup( (Tim_Man_t *)p->pManTime, 0 );
-    // pass the HAIG manager
-    if ( p->pManHaig != NULL )
-    {
-        pNew->pManHaig = p->pManHaig;  
-        p->pManHaig = NULL;
-    }
     // check the resulting network
     if ( !Aig_ManCheck(pNew) )
         printf( "Aig_ManDupDfs(): The check has failed.\n" );
@@ -720,8 +663,6 @@ Aig_Obj_t * Aig_ManDupDfsGuided_rec( Aig_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t
     if ( !Aig_ManDupDfsGuided_rec( pNew, p, Aig_ObjFanin1(pObj) ) )
         return NULL;
     pObjNew = Aig_Oper( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj), Aig_ObjType(pObj) );
-    if ( pObj->pHaig )
-        Aig_Regular(pObjNew)->pHaig = pObj->pHaig;
     if ( pEquivNew )
     {
         if ( pNew->pEquivs )
@@ -771,14 +712,12 @@ Aig_Man_t * Aig_ManDupDfsGuided( Aig_Man_t * p, Vec_Ptr_t * vPios )
     Aig_ManCleanData( p );
     // duplicate internal nodes
     Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
-    Aig_ManConst1(pNew)->pHaig = Aig_ManConst1(p)->pHaig;
     Vec_PtrForEachEntry( Aig_Obj_t *, vPios, pObj, i )
     {
         if ( Aig_ObjIsCi(pObj) )
         {
             pObjNew = Aig_ObjCreateCi( pNew );
             pObjNew->Level = pObj->Level;
-            Aig_Regular(pObjNew)->pHaig = pObj->pHaig;
             pObj->pData = pObjNew;
         }
         else if ( Aig_ObjIsCo(pObj) )
@@ -786,7 +725,6 @@ Aig_Man_t * Aig_ManDupDfsGuided( Aig_Man_t * p, Vec_Ptr_t * vPios )
             Aig_ManDupDfsGuided_rec( pNew, p, Aig_ObjFanin0(pObj) );        
 //            assert( pObj->Level == ((Aig_Obj_t*)pObj->pData)->Level );
             pObjNew = Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) );
-            Aig_Regular(pObjNew)->pHaig = pObj->pHaig;
             pObj->pData = pObjNew;
         }
     }
@@ -841,11 +779,9 @@ Aig_Man_t * Aig_ManDupLevelized( Aig_Man_t * p )
     }
     // create the PIs
     Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
-    Aig_ManConst1(pNew)->pHaig = Aig_ManConst1(p)->pHaig;
     Aig_ManForEachCi( p, pObj, i )
     {
         pObjNew = Aig_ObjCreateCi( pNew );
-        pObjNew->pHaig = pObj->pHaig;
         pObjNew->Level = pObj->Level;
         pObj->pData = pObjNew;
     }
@@ -854,7 +790,6 @@ Aig_Man_t * Aig_ManDupLevelized( Aig_Man_t * p )
     Vec_VecForEachEntry( Aig_Obj_t *, vLevels, pObj, i, k )
     {
         pObjNew = Aig_Oper( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj), Aig_ObjType(pObj) );
-        Aig_Regular(pObjNew)->pHaig = pObj->pHaig;
         pObj->pData = pObjNew;
     }
     Vec_VecFree( vLevels );
@@ -862,7 +797,6 @@ Aig_Man_t * Aig_ManDupLevelized( Aig_Man_t * p )
     Aig_ManForEachCo( p, pObj, i )
     {
         pObjNew = Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) );
-        pObjNew->pHaig = pObj->pHaig;
         pObj->pData = pObjNew;
     }
     assert( Aig_ManBufNum(p) != 0 || Aig_ManNodeNum(p) == Aig_ManNodeNum(pNew) );
diff --git a/src/aig/aig/aigMan.c b/src/aig/aig/aigMan.c
index 6a0555a0..230a2b18 100644
--- a/src/aig/aig/aigMan.c
+++ b/src/aig/aig/aigMan.c
@@ -100,7 +100,6 @@ Aig_Man_t * Aig_ManStartFrom( Aig_Man_t * p )
     {
         pObjNew = Aig_ObjCreateCi( pNew );
         pObjNew->Level = pObj->Level;
-        pObjNew->pHaig = pObj->pHaig;
         pObj->pData = pObjNew;
     }
     return pNew;
@@ -127,7 +126,6 @@ Aig_Obj_t * Aig_ManDup_rec( Aig_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t * pObj )
         return (Aig_Obj_t *)(pObj->pData = Aig_ObjChild0Copy(pObj));
     Aig_ManDup_rec( pNew, p, Aig_ObjFanin1(pObj) );
     pObjNew = Aig_Oper( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj), Aig_ObjType(pObj) );
-    Aig_Regular(pObjNew)->pHaig = pObj->pHaig;
     return (Aig_Obj_t *)(pObj->pData = pObjNew);
 }
 
@@ -361,27 +359,6 @@ int Aig_ManCoCleanup( Aig_Man_t * p )
 
 /**Function*************************************************************
 
-  Synopsis    [Performs one iteration of AIG rewriting.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Aig_ManHaigCounter( Aig_Man_t * pAig )
-{
-    Aig_Obj_t * pObj;
-    int Counter, i;
-    Counter = 0;
-    Aig_ManForEachNode( pAig, pObj, i )
-        Counter += (pObj->pHaig != NULL);
-    return Counter;
-}
-
-/**Function*************************************************************
-
   Synopsis    [Stops the AIG manager.]
 
   Description []
diff --git a/src/aig/aig/aigObj.c b/src/aig/aig/aigObj.c
index 41a07823..e1eab364 100644
--- a/src/aig/aig/aigObj.c
+++ b/src/aig/aig/aigObj.c
@@ -49,12 +49,6 @@ Aig_Obj_t * Aig_ObjCreateCi( Aig_Man_t * p )
     pObj->Type = AIG_OBJ_CI;
     Vec_PtrPush( p->vCis, pObj );
     p->nObjs[AIG_OBJ_CI]++;
-    if ( p->pManHaig && p->fCreatePios )
-    {
-        p->pManHaig->nRegs++;
-        pObj->pHaig = Aig_ObjCreateCi( p->pManHaig );
-//        printf( "Creating PI HAIG node %d equivalent to PI %d.\n", pObj->pHaig->Id, pObj->Id );
-    }
     return pObj;
 }
 
@@ -77,11 +71,6 @@ Aig_Obj_t * Aig_ObjCreateCo( Aig_Man_t * p, Aig_Obj_t * pDriver )
     Vec_PtrPush( p->vCos, pObj );
     Aig_ObjConnect( p, pObj, pDriver, NULL );
     p->nObjs[AIG_OBJ_CO]++;
-    if ( p->pManHaig && p->fCreatePios )
-    {
-        pObj->pHaig = Aig_ObjCreateCo( p->pManHaig, Aig_ObjHaig( pDriver ) );
-//        printf( "Creating PO HAIG node %d equivalent to PO %d.\n", pObj->pHaig->Id, pObj->Id );
-    }
     return pObj;
 }
 
@@ -111,14 +100,6 @@ Aig_Obj_t * Aig_ObjCreate( Aig_Man_t * p, Aig_Obj_t * pGhost )
     // update node counters of the manager
     p->nObjs[Aig_ObjType(pObj)]++;
     assert( pObj->pData == NULL );
-    if ( p->pManHaig )
-    {
-        pGhost->pFanin0 = Aig_ObjHaig( pGhost->pFanin0 );
-        pGhost->pFanin1 = Aig_ObjHaig( pGhost->pFanin1 );
-        pObj->pHaig = Aig_ObjCreate( p->pManHaig, pGhost );
-        assert( !Aig_IsComplement(pObj->pHaig) );
-//        printf( "Creating  HAIG node %d equivalent to node %d.\n", pObj->pHaig->Id, pObj->Id );
-    }
     // create the power counter
     if ( p->vProbs )
     {
@@ -384,14 +365,6 @@ void Aig_ObjPrint( Aig_Man_t * p, Aig_Obj_t * pObj )
         }
         return;
     }
-    if ( fHaig )
-    {
-        if ( pObj->pHaig == NULL )
-            printf( " HAIG node not given" );
-        else
-            printf( " HAIG node = %d%s", Aig_Regular(pObj->pHaig)->Id, (Aig_IsComplement(pObj->pHaig)? "\'" : " ") );
-        return;
-    }
     // there are choices
     if ( p->pEquivs && p->pEquivs[pObj->Id] )
     {
@@ -511,19 +484,6 @@ void Aig_ObjReplace( Aig_Man_t * p, Aig_Obj_t * pObjOld, Aig_Obj_t * pObjNew, in
         printf( "Aig_ObjReplace(): Internal error!\n" );
         exit(1);
     }
-    // map the HAIG nodes
-    if ( p->pManHaig != NULL )
-    {
-//        printf( "Setting HAIG node %d equivalent to HAIG node %d (over = %d).\n", 
-//            pObjNewR->pHaig->Id, pObjOld->pHaig->Id, pObjNewR->pHaig->pHaig != NULL );
-        assert( pObjNewR->pHaig != NULL );
-        assert( !Aig_IsComplement(pObjNewR->pHaig) );
-        assert( p->pManHaig->vEquPairs != NULL );
-        Vec_IntPush( p->pManHaig->vEquPairs, pObjNewR->pHaig->Id );
-        Vec_IntPush( p->pManHaig->vEquPairs, pObjOld->pHaig->Id );
-    }
-    else
-        pObjOld->pHaig = pObjNewR->pHaig? pObjNewR->pHaig : pObjOld->pHaig;
     // recursively delete the old node - but leave the object there
     pObjNewR->nRefs++;
     Aig_ObjDelete_rec( p, pObjOld, 0 );
diff --git a/src/aig/aig/aigPart.c b/src/aig/aig/aigPart.c
index d2d92b82..717f3192 100644
--- a/src/aig/aig/aigPart.c
+++ b/src/aig/aig/aigPart.c
@@ -1493,8 +1493,6 @@ void Aig_ManChoiceConstructiveOne( Aig_Man_t * pNew, Aig_Man_t * pPrev, Aig_Man_
     // make sure the nodes of pThis point to pPrev
     Aig_ManForEachObj( pPrev, pObj, i )
         pObj->fMarkB = 1;
-    Aig_ManForEachObj( pThis, pObj, i )
-        assert( pObj->pHaig == NULL || (!Aig_IsComplement(pObj->pHaig) && pObj->pHaig->fMarkB) );
     Aig_ManForEachObj( pPrev, pObj, i )
         pObj->fMarkB = 0;
     // remap nodes of pThis on top of pNew using pPrev
@@ -1506,13 +1504,7 @@ void Aig_ManChoiceConstructiveOne( Aig_Man_t * pNew, Aig_Man_t * pPrev, Aig_Man_
         pObj->pData = Aig_ManCo(pNew, i);
     // go through the nodes in the topological order
     Aig_ManForEachNode( pThis, pObj, i )
-    {
         pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
-        if ( pObj->pHaig == NULL )
-            continue;
-        // pObj->pData and pObj->pHaig->pData are equivalent
-        Aig_ObjSetRepr_( pNew, Aig_Regular((Aig_Obj_t *)pObj->pData), Aig_Regular((Aig_Obj_t *)pObj->pHaig->pData) );
-    }
     // set the inputs of POs as equivalent
     Aig_ManForEachCo( pThis, pObj, i )
     {