From 6e774ef541114d1cff4926192dc5221c4f43c52e Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sun, 23 Sep 2012 12:01:59 -0700 Subject: Cleaing AIG manager by removing pointers to HAIG. --- src/aig/aig/aig.h | 5 +- src/aig/aig/aigDup.c | 66 ----- src/aig/aig/aigMan.c | 23 -- src/aig/aig/aigObj.c | 40 --- src/aig/aig/aigPart.c | 8 - src/aig/saig/module.make | 1 - src/aig/saig/saigHaig.c | 733 ----------------------------------------------- 7 files changed, 1 insertion(+), 875 deletions(-) delete mode 100644 src/aig/saig/saigHaig.c (limited to 'src/aig') 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); } @@ -359,27 +357,6 @@ int Aig_ManCoCleanup( Aig_Man_t * p ) return nPosOld - Aig_ManCoNum(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.] 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 - -- cgit v1.2.3