Cleaing AIG manager by removing pointers to HAIG.

7 files changed, 1 insertions, 875 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 )
     {
diff --git a/src/aig/saig/module.make b/src/aig/saig/module.make
index edf5798e..a3231929 100644
--- a/src/aig/saig/module.make
+++ b/src/aig/saig/module.make
@@ -7,7 +7,6 @@ SRC +=  src/aig/saig/saigBmc.c \
     src/aig/saig/saigConstr2.c \
     src/aig/saig/saigDual.c \
     src/aig/saig/saigDup.c \
-    src/aig/saig/saigHaig.c \
     src/aig/saig/saigInd.c \
     src/aig/saig/saigIoa.c \
     src/aig/saig/saigIso.c \
diff --git a/src/aig/saig/saigHaig.c b/src/aig/saig/saigHaig.c
deleted file mode 100644
index 7cb34c5d..00000000
--- a/src/aig/saig/saigHaig.c
+++ /dev/null
@@ -1,733 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [saigHaig.c]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [Sequential AIG package.]
-
-  Synopsis    [Experiments with history AIG recording.]
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - April 28, 2007.]
-
-  Revision    [$Id: saigHaig.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "saig.h"
-#include "sat/bsat/satSolver.h"
-#include "sat/cnf/cnf.h"
-
-ABC_NAMESPACE_IMPL_START
-
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Prepares the inductive case with speculative reduction.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Aig_ManHaigSpeculate( Aig_Man_t * pFrames, Aig_Obj_t * pObj )
-{
-    Aig_Obj_t * pObjNew, * pObjNew2, * pObjRepr, * pObjReprNew;//, * pMiter;
-    Aig_Obj_t * pPo;
-    // skip nodes without representative
-    pObjRepr = pObj->pHaig;
-    if ( pObjRepr == NULL )
-        return;
-//    assert( pObjRepr->Id < pObj->Id );
-    // get the new node 
-    pObjNew = (Aig_Obj_t *)pObj->pData;
-    // get the new node of the representative
-    pObjReprNew = (Aig_Obj_t *)pObjRepr->pData;
-    // if this is the same node, no need to add constraints
-    assert( pObjNew != NULL && pObjReprNew != NULL );
-    if ( Aig_Regular(pObjNew) == Aig_Regular(pObjReprNew) )
-        return;
-    // these are different nodes - perform speculative reduction
-    pObjNew2 = Aig_NotCond( pObjReprNew, pObj->fPhase ^ pObjRepr->fPhase );
-    // set the new node
-    pObj->pData = pObjNew2;
-    // add the constraint
-    if ( pObj->fMarkA )
-        return;
-//    pMiter = Aig_Exor( pFrames, pObjNew, pObjReprNew );
-//    pMiter = Aig_NotCond( pMiter, !Aig_ObjPhaseReal(pMiter) );
-//    assert( Aig_ObjPhaseReal(pMiter) == 1 );
-//    Aig_ObjCreateCo( pFrames, pMiter );
-    if ( Aig_ObjPhaseReal(pObjNew) != Aig_ObjPhaseReal(pObjReprNew) )
-        pObjReprNew = Aig_Not(pObjReprNew);
-    pPo = Aig_ObjCreateCo( pFrames, pObjNew );
-    Aig_ObjCreateCo( pFrames, pObjReprNew );
-
-    // remember the node corresponding to this PO
-    pPo->pData = pObj;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Prepares the inductive case with speculative reduction.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Aig_Man_t * Aig_ManHaigFrames( Aig_Man_t * pHaig, int nFrames )
-{
-    Aig_Man_t * pFrames;
-    Aig_Obj_t * pObj, * pObjLi, * pObjLo;
-    int i, f, nAssumptions = 0;
-    assert( nFrames == 1 || nFrames == 2 );
-    assert( nFrames == 1 || Saig_ManRegNum(pHaig) > 0 );
-    // start AIG manager for timeframes
-    pFrames = Aig_ManStart( Aig_ManNodeNum(pHaig) * nFrames );
-    pFrames->pName = Abc_UtilStrsav( pHaig->pName );
-    pFrames->pSpec = Abc_UtilStrsav( pHaig->pSpec );
-    // map the constant node
-    Aig_ManConst1(pHaig)->pData = Aig_ManConst1( pFrames );
-    // create variables for register outputs
-    Saig_ManForEachLo( pHaig, pObj, i )
-        pObj->pData = Aig_ObjCreateCi( pFrames );
-    // add timeframes
-    Aig_ManSetCioIds( pHaig );
-    for ( f = 0; f < nFrames; f++ )
-    {
-        // create primary inputs
-        Saig_ManForEachPi( pHaig, pObj, i )
-            pObj->pData = Aig_ObjCreateCi( pFrames );
-        // create internal nodes
-        Aig_ManForEachNode( pHaig, pObj, i )
-        {        
-            pObj->pData = Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
-            Aig_ManHaigSpeculate( pFrames, pObj );
-        }
-        if ( f == nFrames - 2 )
-            nAssumptions = Aig_ManCoNum(pFrames);
-        if ( f == nFrames - 1 )
-            break;
-        // save register inputs
-        Saig_ManForEachLi( pHaig, pObj, i )
-            pObj->pData = Aig_ObjChild0Copy(pObj);
-        // transfer to register outputs
-        Saig_ManForEachLiLo(  pHaig, pObjLi, pObjLo, i )
-            pObjLo->pData = pObjLi->pData;
-    }
-    Aig_ManCleanup( pFrames );
-    pFrames->nAsserts = Aig_ManCoNum(pFrames) - nAssumptions;
-    Aig_ManSetRegNum( pFrames, 0 );
-    return pFrames;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Aig_ManMapHaigNodes( Aig_Man_t * pHaig )
-{
-    Aig_Obj_t * pObj1, * pObj2;
-    int Id1, Id2, i, Counter = 0;
-    Aig_ManForEachObj( pHaig, pObj1, i )
-        pObj1->pHaig = NULL;
-    Vec_IntForEachEntry( pHaig->vEquPairs, Id1, i )
-    {
-        Id2 = Vec_IntEntry( pHaig->vEquPairs, ++i );
-        pObj1 = Aig_ManObj( pHaig, Id1 );
-        pObj2 = Aig_ManObj( pHaig, Id2 );
-        assert( pObj1 != pObj2 );
-        assert( !Aig_ObjIsCi(pObj1) || !Aig_ObjIsCi(pObj2) );
-        if ( Aig_ObjIsCi(pObj1) )
-        {
-            Counter += (int)(pObj2->pHaig != NULL);
-            pObj2->pHaig = pObj1;
-        }
-        else if ( Aig_ObjIsCi(pObj2) )
-        {
-            Counter += (int)(pObj1->pHaig != NULL);
-            pObj1->pHaig = pObj2;
-        }
-        else if ( pObj1->Id < pObj2->Id )
-        {
-            Counter += (int)(pObj2->pHaig != NULL);
-            pObj2->pHaig = pObj1;
-        }
-        else 
-        {
-            Counter += (int)(pObj1->pHaig != NULL);
-            pObj1->pHaig = pObj2;
-        }
-    }
-//    printf( "Overwrites %d out of %d.\n", Counter, Vec_IntSize(pHaig->vEquPairs)/2 );
-    return Counter;
-}
- 
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Aig_ManHaigVerify( Aig_Man_t * p, Aig_Man_t * pAig, Aig_Man_t * pHaig, int nFrames, clock_t clkSynth )
-{
-    int nBTLimit = 0;
-    Aig_Man_t * pFrames, * pTemp;
-    Cnf_Dat_t * pCnf;
-    sat_solver * pSat;
-    Aig_Obj_t * pObj1, * pObj2;
-    int i, RetValue1, RetValue2, Counter, Lits[2], nOvers;
-    clock_t clk = clock(), clkVerif;
-
-    nOvers = Aig_ManMapHaigNodes( pHaig );
-
-    // create time frames with speculative reduction and convert them into CNF
-clk = clock();
-    pFrames = Aig_ManHaigFrames( pHaig, nFrames );
-    Aig_ManCleanMarkA( pHaig );
-
-    printf( "Frames:     " );
-    Aig_ManPrintStats( pFrames );
-
-    pFrames = Dar_ManRwsat( pTemp = pFrames, 1, 0 );
-    Aig_ManStop( pTemp );
-
-    printf( "Frames synt:" );
-    Aig_ManPrintStats( pFrames );
-
-    printf( "Additional frames stats: Assumptions = %d. Assertions = %d. Pairs = %d. Over = %d.\n", 
-        Aig_ManCoNum(pFrames)/2 - pFrames->nAsserts/2, pFrames->nAsserts/2, Vec_IntSize(pHaig->vEquPairs)/2, nOvers );
-//    pCnf = Cnf_DeriveSimple( pFrames, Aig_ManCoNum(pFrames) );
-    pCnf = Cnf_Derive( pFrames, Aig_ManCoNum(pFrames) );
-
-
-
-//    pCnf = Cnf_Derive( pFrames, Aig_ManCoNum(pFrames) - pFrames->nAsserts );
-//Cnf_DataWriteIntoFile( pCnf, "temp.cnf", 1 );
-//    Saig_ManDumpBlif( pHaig, "haig_temp.blif" );
-//    Saig_ManDumpBlif( pFrames, "haig_temp_frames.blif" );
-    // create the SAT solver to be used for this problem
-    pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
-    if ( pSat == NULL )
-    {
-        printf( "Aig_ManHaigVerify(): Computed CNF is not valid.\n" );
-        return 0;
-    }
-
-    if ( nFrames == 2 )
-    {
-        // add clauses for the first frame
-        Aig_ManForEachCo( pFrames, pObj1, i )
-        {
-            if ( i >= Aig_ManCoNum(pFrames) - pFrames->nAsserts )
-                break;
-
-            pObj2 = Aig_ManCo( pFrames, ++i );
-            assert( pObj1->fPhase == pObj2->fPhase );
-
-            Lits[0] = toLitCond( pCnf->pVarNums[pObj1->Id], 0 );
-            Lits[1] = toLitCond( pCnf->pVarNums[pObj2->Id], 1 );
-            if ( !sat_solver_addclause( pSat, Lits, Lits + 2 ) )
-            {
-                sat_solver_delete( pSat );
-                return 0;
-            }
-            Lits[0]++;
-            Lits[1]--;
-            if ( !sat_solver_addclause( pSat, Lits, Lits + 2 ) )
-            {
-                sat_solver_delete( pSat );
-                return 0;
-            }
-        }
-
-        if ( !sat_solver_simplify(pSat) )
-        {
-            sat_solver_delete( pSat );
-            return 0;
-        }
-    }
-ABC_PRT( "Preparation", clock() - clk );
-
-
-    // check in the second timeframe
-clk = clock();
-    Counter = 0;
-    printf( "Started solving ...\r" );
-    Aig_ManForEachCo( pFrames, pObj1, i )
-    {
-        if ( i < Aig_ManCoNum(pFrames) - pFrames->nAsserts )
-            continue;
-
-        pObj2 = Aig_ManCo( pFrames, ++i );
-        assert( pObj1->fPhase == pObj2->fPhase );
-
-        Lits[0] = toLitCond( pCnf->pVarNums[pObj1->Id], 0 );
-        Lits[1] = toLitCond( pCnf->pVarNums[pObj2->Id], 1 );
-
-        RetValue1 = sat_solver_solve( pSat, Lits, Lits + 2, (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
-        if ( RetValue1 == l_False )
-        {
-            Lits[0] = lit_neg( Lits[0] );
-            Lits[1] = lit_neg( Lits[1] );
-//            RetValue = sat_solver_addclause( pSat, Lits, Lits + 2 );
-//            assert( RetValue );
-        }
-
-        Lits[0]++;
-        Lits[1]--;
-
-        RetValue2 = sat_solver_solve( pSat, Lits, Lits + 2, (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
-        if ( RetValue2 == l_False )
-        {
-            Lits[0] = lit_neg( Lits[0] );
-            Lits[1] = lit_neg( Lits[1] );
-//            RetValue = sat_solver_addclause( pSat, Lits, Lits + 2 );
-//            assert( RetValue );
-        }
-
-        if ( RetValue1 != l_False || RetValue2 != l_False )
-            Counter++;
-
-        if ( i % 50 == 1 )
-            printf( "Solving assertion %6d out of %6d.\r", 
-                (i - (Aig_ManCoNum(pFrames) - pFrames->nAsserts))/2, 
-                pFrames->nAsserts/2 );
-//        if ( nClasses == 1000 )
-//            break;
-    }
-    printf( "                                                          \r" );
-ABC_PRT( "Solving    ", clock() - clk );
-clkVerif = clock() - clk;
-    if ( Counter )
-        printf( "Verification failed for %d out of %d assertions.\n", Counter, pFrames->nAsserts/2 );
-    else
-        printf( "Verification is successful for all %d assertions.\n", pFrames->nAsserts/2 );
-
-    // print the statistic into a file
-    {
-        FILE * pTable;
-        Aig_Man_t * pTemp, * pHaig2;
-
-        pHaig2 = pAig->pManHaig; 
-        pAig->pManHaig = NULL;
-        pTemp = Aig_ManDupDfs( pAig );
-        pAig->pManHaig = pHaig2;
-
-        Aig_ManSeqCleanup( pTemp );
-
-        pTable = fopen( "stats.txt", "a+" );
-        fprintf( pTable, "%s ",  p->pName );
-        fprintf( pTable, "%d ", Saig_ManPiNum(p) );
-        fprintf( pTable, "%d ", Saig_ManPoNum(p) );
-
-        fprintf( pTable, "%d ", Saig_ManRegNum(p) );
-        fprintf( pTable, "%d ", Aig_ManNodeNum(p) );
-        fprintf( pTable, "%d ", Aig_ManLevelNum(p) );
-
-        fprintf( pTable, "%d ", Saig_ManRegNum(pTemp) );
-        fprintf( pTable, "%d ", Aig_ManNodeNum(pTemp) );
-        fprintf( pTable, "%d ", Aig_ManLevelNum(pTemp) );
-
-        fprintf( pTable, "%d ", Saig_ManRegNum(pHaig) );
-        fprintf( pTable, "%d ", Aig_ManNodeNum(pHaig) );
-        fprintf( pTable, "%d ", Aig_ManLevelNum(pHaig) );
-
-        fprintf( pTable, "%.2f", (float)(clkSynth)/(float)(CLOCKS_PER_SEC) );
-        fprintf( pTable, "\n" );
-        fclose( pTable );
-
-
-        pTable = fopen( "stats2.txt", "a+" );
-        fprintf( pTable, "%s ",  p->pName );
-        fprintf( pTable, "%d ", Aig_ManNodeNum(pFrames) );
-        fprintf( pTable, "%d ", Aig_ManLevelNum(pFrames) );
-
-        fprintf( pTable, "%d ", pCnf->nVars );
-        fprintf( pTable, "%d ", pCnf->nClauses );
-        fprintf( pTable, "%d ", pCnf->nLiterals );
-
-        fprintf( pTable, "%d ", Aig_ManCoNum(pFrames)/2 - pFrames->nAsserts/2 );
-        fprintf( pTable, "%d ", pFrames->nAsserts/2 );
-        fprintf( pTable, "%d ", Vec_IntSize(pHaig->vEquPairs)/2 );
-
-        fprintf( pTable, "%.2f", (float)(clkVerif)/(float)(CLOCKS_PER_SEC) );
-        fprintf( pTable, "\n" );
-        fclose( pTable );
-
-        Aig_ManStop( pTemp );
-    }
-
-    // clean up
-    Aig_ManStop( pFrames );
-    Cnf_DataFree( pCnf );
-    sat_solver_delete( pSat );
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Aig_ManHaigVerify2( Aig_Man_t * p, Aig_Man_t * pAig, Aig_Man_t * pHaig, int nFrames )
-{
-    int nBTLimit = 0;
-    Cnf_Dat_t * pCnf;
-    sat_solver * pSat;
-    Aig_Obj_t * pObj1, * pObj2;
-    int i, RetValue1, RetValue2, Counter, Lits[2];
-    clock_t clk = clock();
-    int Delta;
-    int Id1, Id2;
-
-    assert( nFrames == 1 || nFrames == 2 );
-
-clk = clock();
-    pCnf = Cnf_DeriveSimple( pHaig, Aig_ManCoNum(pHaig) );
-//    Aig_ManForEachObj( pHaig, pObj, i )
-//        printf( "%d=%d  ", pObj->Id, pCnf->pVarNums[pObj->Id] );
-//    printf( "\n" );
-
-    // create the SAT solver to be used for this problem
-    pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, nFrames, 0 );
-//Sat_SolverWriteDimacs( pSat, "1.cnf", NULL, NULL, 0 );
-    if ( pSat == NULL )
-    {
-        printf( "Aig_ManHaigVerify(): Computed CNF is not valid.\n" );
-        return -1;
-    }
-
-    if ( nFrames == 2 )
-    {
-        Vec_IntForEachEntry( pHaig->vEquPairs, Id1, i )
-        {
-            Id2 = Vec_IntEntry( pHaig->vEquPairs, ++i );
-            pObj1 = Aig_ManObj( pHaig, Id1 );
-            pObj2 = Aig_ManObj( pHaig, Id2 );
-            if ( pObj1->fPhase ^ pObj2->fPhase )
-            {
-                Lits[0] = toLitCond( pCnf->pVarNums[pObj1->Id], 0 );
-                Lits[1] = toLitCond( pCnf->pVarNums[pObj2->Id], 0 );
-                if ( !sat_solver_addclause( pSat, Lits, Lits + 2 ) )
-                {
-                    sat_solver_delete( pSat );
-                    return 0;
-                }
-                Lits[0]++;
-                Lits[1]++;
-                if ( !sat_solver_addclause( pSat, Lits, Lits + 2 ) )
-                {
-                    sat_solver_delete( pSat );
-                    return 0;
-                }
-            }
-            else
-            {
-                Lits[0] = toLitCond( pCnf->pVarNums[pObj1->Id], 0 );
-                Lits[1] = toLitCond( pCnf->pVarNums[pObj2->Id], 1 );
-                if ( !sat_solver_addclause( pSat, Lits, Lits + 2 ) )
-                {
-                    sat_solver_delete( pSat );
-                    return 0;
-                }
-                Lits[0]++;
-                Lits[1]--;
-                if ( !sat_solver_addclause( pSat, Lits, Lits + 2 ) )
-                {
-                    sat_solver_delete( pSat );
-                    return 0;
-                }
-            }
-        }
-
-        if ( !sat_solver_simplify(pSat) )
-        {
-            sat_solver_delete( pSat );
-            return 0;
-        }
-    }
-ABC_PRT( "Preparation", clock() - clk );
-
-
-    // check in the second timeframe
-clk = clock();
-    Counter = 0;
-    Delta = (nFrames == 2)? pCnf->nVars : 0;
-    Vec_IntForEachEntry( pHaig->vEquPairs, Id1, i )
-    {
-        Id2 = Vec_IntEntry( pHaig->vEquPairs, ++i );
-        pObj1 = Aig_ManObj( pHaig, Id1 );
-        pObj2 = Aig_ManObj( pHaig, Id2 );
-        if ( pObj1->fPhase ^ pObj2->fPhase )
-        {
-            Lits[0] = toLitCond( pCnf->pVarNums[pObj1->Id]+Delta, 0 );
-            Lits[1] = toLitCond( pCnf->pVarNums[pObj2->Id]+Delta, 0 );
-
-            RetValue1 = sat_solver_solve( pSat, Lits, Lits + 2, (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
-
-            Lits[0]++;
-            Lits[1]++;
-
-            RetValue2 = sat_solver_solve( pSat, Lits, Lits + 2, (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
-
-            if ( RetValue1 != l_False || RetValue2 != l_False )
-                Counter++;
-        }
-        else
-        {
-            Lits[0] = toLitCond( pCnf->pVarNums[pObj1->Id]+Delta, 0 );
-            Lits[1] = toLitCond( pCnf->pVarNums[pObj2->Id]+Delta, 1 );
-
-            RetValue1 = sat_solver_solve( pSat, Lits, Lits + 2, (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
-
-            Lits[0]++;
-            Lits[1]--;
-
-            RetValue2 = sat_solver_solve( pSat, Lits, Lits + 2, (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
-
-            if ( RetValue1 != l_False || RetValue2 != l_False )
-                Counter++;
-        }
-        if ( i % 50 == 1 )
-            printf( "Solving assertion %6d out of %6d.\r", i/2, Vec_IntSize(pHaig->vEquPairs)/2 );
-
-//        if ( i / 2 > 1000 )
-//            break;
-    }
-ABC_PRT( "Solving    ", clock() - clk );
-    if ( Counter )
-        printf( "Verification failed for %d out of %d classes.\n", Counter, Vec_IntSize(pHaig->vEquPairs)/2 );
-    else
-        printf( "Verification is successful for all %d classes.\n", Vec_IntSize(pHaig->vEquPairs)/2 );
-
-    Cnf_DataFree( pCnf );
-    sat_solver_delete( pSat );
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Aig_Man_t * Saig_ManHaigDump( Aig_Man_t * pHaig )
-{
-    Vec_Ptr_t * vTemp;
-    Aig_Obj_t * pObj, * pObj1, * pObj2, * pMiter;
-    int Id1, Id2, i;
-    // remove regular POs
-    Aig_ManSetCioIds( pHaig );
-    vTemp = Vec_PtrAlloc( Saig_ManRegNum(pHaig) );
-    Aig_ManForEachCo( pHaig, pObj, i )
-    {
-        if ( Saig_ObjIsPo(pHaig, pObj) )
-        {
-            Aig_ObjDisconnect( pHaig, pObj );
-            Vec_PtrWriteEntry( pHaig->vObjs, pObj->Id, NULL );
-        }
-        else
-        {
-            Vec_PtrPush( vTemp, pObj );
-        }
-    }
-    Vec_PtrShrink( pHaig->vCos, 0 ); 
-    pHaig->nObjs[AIG_OBJ_CO] = Vec_PtrSize( vTemp );
-    // add new POs
-    Vec_IntForEachEntry( pHaig->vEquPairs, Id1, i )
-    {
-        Id2 = Vec_IntEntry( pHaig->vEquPairs, ++i );
-        pObj1 = Aig_ManObj( pHaig, Id1 );
-        pObj2 = Aig_ManObj( pHaig, Id2 );
-        assert( pObj1 != pObj2 );
-        assert( !Aig_ObjIsCi(pObj1) || !Aig_ObjIsCi(pObj2) );
-        pMiter = Aig_Exor( pHaig, pObj1, pObj2 );
-        pMiter = Aig_NotCond( pMiter, Aig_ObjPhaseReal(pMiter) );
-        assert( Aig_ObjPhaseReal(pMiter) == 0 );
-        Aig_ObjCreateCo( pHaig, pMiter );
-    }
-    printf( "Added %d property outputs.\n", Vec_IntSize(pHaig->vEquPairs)/2 );
-    // add the registers
-    Vec_PtrForEachEntry( Aig_Obj_t *, vTemp, pObj, i )
-        Vec_PtrPush( pHaig->vCos, pObj );
-    Vec_PtrFree( vTemp );
-    assert( pHaig->nObjs[AIG_OBJ_CO] ==  Vec_PtrSize(pHaig->vCos) ); 
-    Aig_ManCleanup( pHaig );
-    Aig_ManSetRegNum( pHaig, pHaig->nRegs );
-//    return pHaig;
-
-    printf( "HAIG:       " );
-    Aig_ManPrintStats( pHaig );
-    printf( "HAIG is written into file \"haig.blif\".\n" );
-    Saig_ManDumpBlif( pHaig, "haig.blif" );
-
-    Vec_IntFree( pHaig->vEquPairs );
-    Aig_ManStop( pHaig );
-    return NULL;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Aig_Man_t * Saig_ManHaigRecord( Aig_Man_t * p, int nIters, int nSteps, int fRetimingOnly, int fAddBugs, int fUseCnf, int fVerbose )
-{
-    int fSeqHaig = (int)( Aig_ManRegNum(p) > 0 );
-    Dar_RwrPar_t ParsRwr, * pParsRwr = &ParsRwr;
-    Aig_Man_t * pNew, * pTemp;
-    Aig_Obj_t * pObj;
-    int i, k, nStepsReal;
-    clock_t clk = clock(), clkSynth;
-    Dar_ManDefaultRwrParams( pParsRwr );
-
-clk = clock();
-    // duplicate this manager
-    pNew = Aig_ManDupSimple( p );
-    // create its history AIG
-    pNew->pManHaig = Aig_ManDupSimple( pNew );
-    Aig_ManForEachObj( pNew, pObj, i )
-        pObj->pHaig = (Aig_Obj_t *)pObj->pData;
-    // remove structural hashing table
-    Aig_TableClear( pNew->pManHaig );
-    pNew->pManHaig->vEquPairs = Vec_IntAlloc( 10000 );
-ABC_PRT( "HAIG setup time", clock() - clk );
-
-clk = clock();
-    if ( fSeqHaig )
-    {
-        if ( fRetimingOnly )
-        {
-            // perform retiming
-            nStepsReal = Saig_ManRetimeSteps( pNew, nSteps, 1, fAddBugs ); 
-            pNew = Aig_ManDupSimpleDfs( pTemp = pNew ); 
-            Aig_ManStop( pTemp );
-            printf( "Performed %d retiming moves.\n", nStepsReal );
-        }
-        else
-        {
-            for ( k = 0; k < nIters; k++ )
-            {
-                // perform balancing
-                pNew = Dar_ManBalance( pTemp = pNew, 0 );
-                Aig_ManStop( pTemp );
-
-                // perform rewriting
-                Dar_ManRewrite( pNew, pParsRwr );
-                pNew = Aig_ManDupDfs( pTemp = pNew ); 
-                Aig_ManStop( pTemp );
-
-                // perform retiming
-                nStepsReal = Saig_ManRetimeSteps( pNew, nSteps, 1, fAddBugs ); 
-                pNew = Aig_ManDupSimpleDfs( pTemp = pNew ); 
-                Aig_ManStop( pTemp );
-                printf( "Performed %d retiming moves.\n", nStepsReal );
-            }
-        }
-    }
-    else
-    {
-        for ( k = 0; k < nIters; k++ )
-        {
-            // perform balancing
-            pNew = Dar_ManBalance( pTemp = pNew, 0 );
-            Aig_ManStop( pTemp );
-
-            // perform rewriting
-            Dar_ManRewrite( pNew, pParsRwr );
-            pNew = Aig_ManDupDfs( pTemp = pNew ); 
-            Aig_ManStop( pTemp );
-        }
-    } 
-ABC_PRT( "Synthesis time ", clock() - clk );
-clkSynth = clock() - clk;
-
-    // use the haig for verification
-//    Aig_ManAntiCleanup( pNew->pManHaig );
-    Aig_ManSetRegNum( pNew->pManHaig, pNew->pManHaig->nRegs );
-//Aig_ManShow( pNew->pManHaig, 0, NULL ); 
-
-    printf( "AIG before: " );
-    Aig_ManPrintStats( p );
-    printf( "AIG after:  " );
-    Aig_ManPrintStats( pNew );
-    printf( "HAIG:       " );
-    Aig_ManPrintStats( pNew->pManHaig );
-
-    if ( fUseCnf )
-    {
-        if ( !Aig_ManHaigVerify2( p, pNew, pNew->pManHaig, 1+fSeqHaig ) )
-            printf( "Constructing SAT solver has failed.\n" );         
-    }
-    else
-    {
-        if ( !Aig_ManHaigVerify( p, pNew, pNew->pManHaig, 1+fSeqHaig, clkSynth ) )
-            printf( "Constructing SAT solver has failed.\n" );         
-    }
-
-    Saig_ManHaigDump( pNew->pManHaig );
-    pNew->pManHaig = NULL;
-    return pNew;
-/*
-    // cleanup
-    Vec_IntFree( pNew->pManHaig->vEquPairs );
-    Aig_ManStop( pNew->pManHaig );
-    pNew->pManHaig = NULL;
-    return pNew;
-*/
-}
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
-ABC_NAMESPACE_IMPL_END
-