diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/aig/aig/aig.h | 5 | ||||
-rw-r--r-- | src/aig/aig/aigDup.c | 66 | ||||
-rw-r--r-- | src/aig/aig/aigMan.c | 23 | ||||
-rw-r--r-- | src/aig/aig/aigObj.c | 40 | ||||
-rw-r--r-- | src/aig/aig/aigPart.c | 8 | ||||
-rw-r--r-- | src/aig/saig/module.make | 1 | ||||
-rw-r--r-- | src/aig/saig/saigHaig.c | 733 | ||||
-rw-r--r-- | src/base/abc/abc.h | 1 | ||||
-rw-r--r-- | src/base/abc/abcAig.c | 9 | ||||
-rw-r--r-- | src/base/abc/abcNtk.c | 3 | ||||
-rw-r--r-- | src/base/abci/abcBalance.c | 3 | ||||
-rw-r--r-- | src/base/abci/abcHaig.c | 181 | ||||
-rw-r--r-- | src/base/abci/abcPart.c | 1 | ||||
-rw-r--r-- | src/base/abci/module.make | 2 | ||||
-rw-r--r-- | src/opt/dar/darBalance.c | 23 | ||||
-rw-r--r-- | src/opt/dar/darScript.c | 35 | ||||
-rw-r--r-- | src/proof/fra/fraLcr.c | 1 |
17 files changed, 2 insertions, 1133 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 - diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h index 91f10590..fd93ccec 100644 --- a/src/base/abc/abc.h +++ b/src/base/abc/abc.h @@ -215,7 +215,6 @@ struct Abc_Ntk_t_ void * pExcare; // the EXDC network (if given) void * pData; // misc Abc_Ntk_t * pCopy; // copy of this network - void * pHaig; // history AIG float * pLutTimes; // arrivals/requireds/slacks using LUT-delay model Vec_Ptr_t * vOnehots; // names of one-hot-encoded registers Vec_Int_t * vObjPerm; // permutation saved diff --git a/src/base/abc/abcAig.c b/src/base/abc/abcAig.c index 4e725a01..5fc3ffd3 100644 --- a/src/base/abc/abcAig.c +++ b/src/base/abc/abcAig.c @@ -344,9 +344,6 @@ Abc_Obj_t * Abc_AigAndCreate( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_t * p1 ) // add the node to the list of updated nodes if ( pMan->vAddedCells ) Vec_PtrPush( pMan->vAddedCells, pAnd ); - // create HAIG -// if ( pAnd->pNtk->pHaig ) -// pAnd->pEquiv = Hop_And( pAnd->pNtk->pHaig, Abc_ObjChild0Equiv(pAnd), Abc_ObjChild1Equiv(pAnd) ); return pAnd; } @@ -387,9 +384,6 @@ Abc_Obj_t * Abc_AigAndCreateFrom( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_t * // add the node to the list of updated nodes // if ( pMan->vAddedCells ) // Vec_PtrPush( pMan->vAddedCells, pAnd ); - // create HAIG -// if ( pAnd->pNtk->pHaig ) -// pAnd->pEquiv = Hop_And( pAnd->pNtk->pHaig, Abc_ObjChild0Equiv(pAnd), Abc_ObjChild1Equiv(pAnd) ); return pAnd; } @@ -858,9 +852,6 @@ void Abc_AigReplace( Abc_Aig_t * pMan, Abc_Obj_t * pOld, Abc_Obj_t * pNew, int f Vec_PtrPush( pMan->vStackReplaceOld, pOld ); Vec_PtrPush( pMan->vStackReplaceNew, pNew ); assert( !Abc_ObjIsComplement(pOld) ); - // create HAIG -// if ( pOld->pNtk->pHaig ) -// Hop_ObjCreateChoice( pOld->pEquiv, Abc_ObjRegular(pNew)->pEquiv ); // process the replacements while ( Vec_PtrSize(pMan->vStackReplaceOld) ) { diff --git a/src/base/abc/abcNtk.c b/src/base/abc/abcNtk.c index 5f9c0f0d..db54643d 100644 --- a/src/base/abc/abcNtk.c +++ b/src/base/abc/abcNtk.c @@ -1070,9 +1070,6 @@ void Abc_NtkDelete( Abc_Ntk_t * pNtk ) // int LargePiece = (4 << ABC_NUM_STEPS); if ( pNtk == NULL ) return; - // free the HAIG -// if ( pNtk->pHaig ) -// Abc_NtkHaigStop( pNtk ); // free EXDC Ntk if ( pNtk->pExdc ) Abc_NtkDelete( pNtk->pExdc ); diff --git a/src/base/abci/abcBalance.c b/src/base/abci/abcBalance.c index 2c391e89..9807997c 100644 --- a/src/base/abci/abcBalance.c +++ b/src/base/abci/abcBalance.c @@ -277,9 +277,6 @@ Abc_Obj_t * Abc_NodeBalance_rec( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNodeOld, Vec_ // if ( Abc_ObjRegular(pNodeOld->pCopy) == Abc_AigConst1(pNtkNew) ) // printf( "Constant node\n" ); // assert( pNodeOld->Level >= Abc_ObjRegular(pNodeOld->pCopy)->Level ); - // update HAIG -// if ( Abc_ObjRegular(pNodeOld->pCopy)->pNtk->pHaig ) -// Hop_ObjCreateChoice( pNodeOld->pEquiv, Abc_ObjRegular(pNodeOld->pCopy)->pEquiv ); return pNodeOld->pCopy; } diff --git a/src/base/abci/abcHaig.c b/src/base/abci/abcHaig.c index d6c0ddad..02547de1 100644 --- a/src/base/abci/abcHaig.c +++ b/src/base/abci/abcHaig.c @@ -31,129 +31,6 @@ ABC_NAMESPACE_IMPL_START /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// -#if 0 - -/**Function************************************************************* - - Synopsis [Start history AIG.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Abc_NtkHaigStart( Abc_Ntk_t * pNtk ) -{ - Hop_Man_t * p; - Abc_Obj_t * pObj, * pTemp; - int i; - assert( Abc_NtkIsStrash(pNtk) ); - // check if the package is already started - if ( pNtk->pHaig ) - { - Abc_NtkHaigStop( pNtk ); - assert( pNtk->pHaig == NULL ); - printf( "Warning: Previous history AIG was removed.\n" ); - } - // make sure the data is clean - Abc_NtkForEachObj( pNtk, pObj, i ) - assert( pObj->pEquiv == NULL ); - // start the HOP package - p = Hop_ManStart(); - p->vObjs = Vec_PtrAlloc( 4096 ); - Vec_PtrPush( p->vObjs, Hop_ManConst1(p) ); - // map the constant node - Abc_AigConst1(pNtk)->pEquiv = Hop_ManConst1(p); - // map the CIs - Abc_NtkForEachCi( pNtk, pObj, i ) - pObj->pEquiv = Hop_ObjCreatePi(p); - // map the internal nodes - Abc_NtkForEachNode( pNtk, pObj, i ) - pObj->pEquiv = Hop_And( p, Abc_ObjChild0Equiv(pObj), Abc_ObjChild1Equiv(pObj) ); - // map the choice nodes - if ( Abc_NtkGetChoiceNum( pNtk ) ) - { - // print warning about choice nodes - printf( "Warning: The choice nodes in the original AIG are converted into HAIG.\n" ); - Abc_NtkForEachNode( pNtk, pObj, i ) - { - if ( !Abc_AigNodeIsChoice( pObj ) ) - continue; - for ( pTemp = pObj->pData; pTemp; pTemp = pTemp->pData ) - Hop_ObjCreateChoice( pObj->pEquiv, pTemp->pEquiv ); - } - } - // make sure everything is okay - if ( !Hop_ManCheck(p) ) - { - printf( "Abc_NtkHaigStart: Check for History AIG has failed.\n" ); - Hop_ManStop(p); - return 0; - } - pNtk->pHaig = p; - return 1; -} - -/**Function************************************************************* - - Synopsis [Stops history AIG.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Abc_NtkHaigStop( Abc_Ntk_t * pNtk ) -{ - Abc_Obj_t * pObj; - int i; - assert( Abc_NtkIsStrash(pNtk) ); - if ( pNtk->pHaig == NULL ) - { - printf( "Warning: History AIG is not allocated.\n" ); - return 1; - } - Abc_NtkForEachObj( pNtk, pObj, i ) - pObj->pEquiv = NULL; - Hop_ManStop( pNtk->pHaig ); - pNtk->pHaig = NULL; - return 1; -} - -/**Function************************************************************* - - Synopsis [Transfers the HAIG to the new network.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Abc_NtkHaigTranfer( Abc_Ntk_t * pNtkOld, Abc_Ntk_t * pNtkNew ) -{ - Abc_Obj_t * pObj; - int i; - if ( pNtkOld->pHaig == NULL ) - return; - // transfer the package - assert( pNtkNew->pHaig == NULL ); - pNtkNew->pHaig = pNtkOld->pHaig; - pNtkOld->pHaig = NULL; - // transfer constant pointer - Abc_AigConst1(pNtkOld)->pCopy->pEquiv = Abc_AigConst1(pNtkOld)->pEquiv; - // transfer the CI pointers - Abc_NtkForEachCi( pNtkOld, pObj, i ) - pObj->pCopy->pEquiv = pObj->pEquiv; -} - - -#endif /**Function************************************************************* @@ -642,64 +519,6 @@ int Abc_NtkHaigResetReprs( Hop_Man_t * p ) return nFanouts; } -#if 0 - -/**Function************************************************************* - - Synopsis [Stops history AIG.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Abc_Ntk_t * Abc_NtkHaigUse( Abc_Ntk_t * pNtk ) -{ - Hop_Man_t * pMan, * pManTemp; - Abc_Ntk_t * pNtkAig; - Abc_Obj_t * pObj; - int i; - - // check if HAIG is available - assert( Abc_NtkIsStrash(pNtk) ); - if ( pNtk->pHaig == NULL ) - { - printf( "Warning: History AIG is not available.\n" ); - return NULL; - } - // convert HOP package into AIG with choices - // print HAIG stats -// Hop_ManPrintStats( pMan ); // USES DATA!!! - - // add the POs - Abc_NtkForEachCo( pNtk, pObj, i ) - Hop_ObjCreatePo( pNtk->pHaig, Abc_ObjChild0Equiv(pObj) ); - - // clean the old network - Abc_NtkForEachObj( pNtk, pObj, i ) - pObj->pEquiv = NULL; - pMan = pNtk->pHaig; - pNtk->pHaig = 0; - - // iteratively reconstruct the HOP manager to create choice nodes - while ( Abc_NtkHaigResetReprs( pMan ) ) - { - pMan = Abc_NtkHaigReconstruct( pManTemp = pMan ); - Hop_ManStop( pManTemp ); - } - - // traverse in the topological order and create new AIG - pNtkAig = Abc_NtkHaigRecreateAig( pNtk, pMan ); - Hop_ManStop( pMan ); - - // free HAIG - return pNtkAig; -} - -#endif - /**Function************************************************************* Synopsis [Transform HOP manager into the one without loops.] diff --git a/src/base/abci/abcPart.c b/src/base/abci/abcPart.c index 779c5c7e..c68e0729 100644 --- a/src/base/abci/abcPart.c +++ b/src/base/abci/abcPart.c @@ -1000,7 +1000,6 @@ Hop_Man_t * Abc_NtkPartStartHop( Abc_Ntk_t * pNtk ) Abc_Ntk_t * Abc_NtkPartStitchChoices( Abc_Ntk_t * pNtk, Vec_Ptr_t * vParts ) { extern Abc_Ntk_t * Abc_NtkHopRemoveLoops( Abc_Ntk_t * pNtk, Hop_Man_t * pMan ); - Hop_Man_t * pMan; Vec_Ptr_t * vNodes; Abc_Ntk_t * pNtkNew, * pNtkTemp; diff --git a/src/base/abci/module.make b/src/base/abci/module.make index e25e497d..cb57acaa 100644 --- a/src/base/abci/module.make +++ b/src/base/abci/module.make @@ -21,7 +21,7 @@ SRC += src/base/abci/abc.c \ src/base/abci/abcFraig.c \ src/base/abci/abcFxu.c \ src/base/abci/abcGen.c \ - src/base/abci/abcHaig.c \ + src/base/abci/abcHaig.c \ src/base/abci/abcIf.c \ src/base/abci/abcIfif.c \ src/base/abci/abcIfMux.c \ diff --git a/src/opt/dar/darBalance.c b/src/opt/dar/darBalance.c index 75f0eaf4..f31c6fc7 100644 --- a/src/opt/dar/darBalance.c +++ b/src/opt/dar/darBalance.c @@ -532,19 +532,6 @@ Aig_Obj_t * Dar_Balance_rec( Aig_Man_t * pNew, Aig_Obj_t * pObjOld, Vec_Vec_t * // make sure the balanced node is not assigned // assert( pObjOld->Level >= Aig_Regular(pObjNew)->Level ); assert( pObjOld->pData == NULL ); - if ( pNew->pManHaig != NULL ) - { - Aig_Obj_t * pObjNewR = Aig_Regular(pObjNew); -// printf( "Balancing 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( pNew->pManHaig->vEquPairs != NULL ); - Vec_IntPush( pNew->pManHaig->vEquPairs, pObjNewR->pHaig->Id ); - Vec_IntPush( pNew->pManHaig->vEquPairs, pObjOld->pHaig->Id ); - } - else - Aig_Regular(pObjNew)->pHaig = pObjOld->pHaig; return (Aig_Obj_t *)(pObjOld->pData = pObjNew); } @@ -574,12 +561,6 @@ Aig_Man_t * Dar_ManBalance( Aig_Man_t * p, int fUpdateLevel ) pNew->nConstrs = p->nConstrs; if ( p->vFlopNums ) pNew->vFlopNums = Vec_IntDup( p->vFlopNums ); - // pass the HAIG manager - if ( p->pManHaig != NULL ) - { - pNew->pManHaig = p->pManHaig; p->pManHaig = NULL; - Aig_ManConst1(pNew)->pHaig = Aig_ManConst1(pNew->pManHaig); - } // map the PI nodes Aig_ManCleanData( p ); Aig_ManConst1(p)->pData = Aig_ManConst1(pNew); @@ -598,7 +579,6 @@ Aig_Man_t * Dar_ManBalance( Aig_Man_t * p, int fUpdateLevel ) // copy the PI pObjNew = Aig_ObjCreateCi(pNew); pObj->pData = pObjNew; - pObjNew->pHaig = pObj->pHaig; // set the arrival time of the new PI arrTime = Tim_ManGetCiArrival( (Tim_Man_t *)p->pManTime, Aig_ObjCioId(pObj) ); pObjNew->Level = (int)arrTime; @@ -614,7 +594,6 @@ Aig_Man_t * Dar_ManBalance( Aig_Man_t * p, int fUpdateLevel ) Tim_ManSetCoArrival( (Tim_Man_t *)p->pManTime, Aig_ObjCioId(pObj), arrTime ); // create PO pObjNew = Aig_ObjCreateCo( pNew, pObjNew ); - pObjNew->pHaig = pObj->pHaig; } else assert( 0 ); @@ -629,7 +608,6 @@ Aig_Man_t * Dar_ManBalance( Aig_Man_t * p, int fUpdateLevel ) pObjNew = Aig_ObjCreateCi(pNew); pObjNew->Level = pObj->Level; pObj->pData = pObjNew; - pObjNew->pHaig = pObj->pHaig; } Aig_ManForEachCo( p, pObj, i ) { @@ -637,7 +615,6 @@ Aig_Man_t * Dar_ManBalance( Aig_Man_t * p, int fUpdateLevel ) pObjNew = Dar_Balance_rec( pNew, Aig_Regular(pDriver), vStore, 0, fUpdateLevel ); pObjNew = Aig_NotCond( pObjNew, Aig_IsComplement(pDriver) ); pObjNew = Aig_ObjCreateCo( pNew, pObjNew ); - pObjNew->pHaig = pObj->pHaig; } } Vec_VecFree( vStore ); diff --git a/src/opt/dar/darScript.c b/src/opt/dar/darScript.c index b3830cc3..583ca563 100644 --- a/src/opt/dar/darScript.c +++ b/src/opt/dar/darScript.c @@ -134,27 +134,6 @@ Aig_Man_t * Dar_ManRwsat( Aig_Man_t * pAig, int fBalance, int fVerbose ) /**Function************************************************************* - Synopsis [Performs one iteration of AIG rewriting.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Dar_ManHaigPrintStats( Aig_Man_t * pAig ) -{ - Aig_Obj_t * pObj; - int Counter, i; - Counter = 0; - Aig_ManForEachNode( pAig, pObj, i ) - Counter += (pObj->pHaig != NULL); - printf( "Total nodes = %6d. Equiv nodes = %6d.\n", Aig_ManNodeNum(pAig), Counter ); -} - -/**Function************************************************************* - Synopsis [Reproduces script "compress".] Description [] @@ -352,34 +331,20 @@ Vec_Ptr_t * Dar_ManChoiceSynthesis( Aig_Man_t * pAig, int fBalance, int fUpdateL //alias resyn2 "b; rw; rf; b; rw; rwz; b; rfz; rwz; b" { Vec_Ptr_t * vAigs; - Aig_Obj_t * pObj; - int i; vAigs = Vec_PtrAlloc( 3 ); pAig = Aig_ManDupDfs(pAig); Vec_PtrPush( vAigs, pAig ); - Aig_ManForEachObj( pAig, pObj, i ) - pObj->pHaig = pObj; - pAig = Dar_ManCompress(pAig, fBalance, fUpdateLevel, fPower, fVerbose); Vec_PtrPush( vAigs, pAig ); //Aig_ManPrintStats( pAig ); - Aig_ManForEachObj( pAig, pObj, i ) - { - pObj->pNext = pObj->pHaig; - pObj->pHaig = pObj; - } - pAig = Dar_ManCompress2(pAig, fBalance, fUpdateLevel, 1, fPower, fVerbose); Vec_PtrPush( vAigs, pAig ); //Aig_ManPrintStats( pAig ); pAig = (Aig_Man_t *)Vec_PtrEntry( vAigs, 1 ); - Aig_ManForEachObj( pAig, pObj, i ) - pObj->pHaig = pObj->pNext; - return vAigs; } diff --git a/src/proof/fra/fraLcr.c b/src/proof/fra/fraLcr.c index 2941f24f..9d573bee 100644 --- a/src/proof/fra/fraLcr.c +++ b/src/proof/fra/fraLcr.c @@ -273,7 +273,6 @@ Aig_Obj_t * Fra_LcrManDup_rec( Aig_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t * pObj return (Aig_Obj_t *)(pObj->pData = Aig_ObjChild0Copy(pObj)); Fra_LcrManDup_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); } |