diff options
Diffstat (limited to 'src/aig/saig')
-rw-r--r-- | src/aig/saig/saig.h | 2 | ||||
-rw-r--r-- | src/aig/saig/saigAbsStart.c | 6 | ||||
-rw-r--r-- | src/aig/saig/saigDup.c | 44 |
3 files changed, 26 insertions, 26 deletions
diff --git a/src/aig/saig/saig.h b/src/aig/saig/saig.h index 93375fd8..d2ef8838 100644 --- a/src/aig/saig/saig.h +++ b/src/aig/saig/saig.h @@ -154,7 +154,7 @@ extern Aig_Man_t * Saig_ManDupUnfoldConstrsFunc( Aig_Man_t * pAig, int nFr /*=== saigDup.c ==========================================================*/ extern Aig_Man_t * Saig_ManDupOrpos( Aig_Man_t * p ); extern Aig_Man_t * Saig_ManCreateEquivMiter( Aig_Man_t * pAig, Vec_Int_t * vPairs ); -extern Aig_Man_t * Saig_ManDeriveAbstraction( Aig_Man_t * pAig, Vec_Int_t * vFlops ); +extern Aig_Man_t * Saig_ManDupAbstraction( Aig_Man_t * pAig, Vec_Int_t * vFlops ); extern int Saig_ManVerifyCex( Aig_Man_t * pAig, Abc_Cex_t * p ); extern int Saig_ManFindFailedPoCex( Aig_Man_t * pAig, Abc_Cex_t * p ); /*=== saigHaig.c ==========================================================*/ diff --git a/src/aig/saig/saigAbsStart.c b/src/aig/saig/saigAbsStart.c index 6ec2c21d..13d11224 100644 --- a/src/aig/saig/saigAbsStart.c +++ b/src/aig/saig/saigAbsStart.c @@ -204,7 +204,7 @@ Aig_Man_t * Saig_ManCexRefine( Aig_Man_t * p, Aig_Man_t * pAbs, Vec_Int_t * vFlo Vec_IntForEachEntryStart( vFlops, Entry, i, 1 ) assert( Vec_IntEntry(vFlops, i-1) != Entry ); - return Saig_ManDeriveAbstraction( p, vFlops ); + return Saig_ManDupAbstraction( p, vFlops ); } /**Function************************************************************* @@ -223,7 +223,7 @@ int Saig_ManCexRefineStep( Aig_Man_t * p, Vec_Int_t * vFlops, Abc_Cex_t * pCex, Aig_Man_t * pAbs; Vec_Int_t * vFlopsNew; int i, Entry, clk = clock(); - pAbs = Saig_ManDeriveAbstraction( p, vFlops ); + pAbs = Saig_ManDupAbstraction( p, vFlops ); if ( fSensePath ) vFlopsNew = Saig_ManExtendCounterExampleTest2( pAbs, Saig_ManCexFirstFlopPi(p, pAbs), pCex, fVerbose ); else @@ -291,7 +291,7 @@ Vec_Int_t * Saig_ManCexAbstractionFlops( Aig_Man_t * p, Gia_ParAbs_t * pPars ) Vec_IntPush( vFlops, iFlop ); */ // create the resulting AIG - pAbs = Saig_ManDeriveAbstraction( p, vFlops ); + pAbs = Saig_ManDupAbstraction( p, vFlops ); if ( !pPars->fVerbose ) { printf( "Init : " ); diff --git a/src/aig/saig/saigDup.c b/src/aig/saig/saigDup.c index b2b33bdb..103cdf7b 100644 --- a/src/aig/saig/saigDup.c +++ b/src/aig/saig/saigDup.c @@ -129,26 +129,6 @@ Aig_Man_t * Saig_ManCreateEquivMiter( Aig_Man_t * pAig, Vec_Int_t * vPairs ) /**Function************************************************************* - Synopsis [Duplicates the AIG manager recursively.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Aig_Obj_t * Saig_ManAbstractionDfs_rec( Aig_Man_t * pNew, Aig_Obj_t * pObj ) -{ - if ( pObj->pData ) - return (Aig_Obj_t *)pObj->pData; - Saig_ManAbstractionDfs_rec( pNew, Aig_ObjFanin0(pObj) ); - Saig_ManAbstractionDfs_rec( pNew, Aig_ObjFanin1(pObj) ); - return (Aig_Obj_t *)(pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) )); -} - -/**Function************************************************************* - Synopsis [Trims the model by removing PIs without fanout.] Description [] @@ -193,6 +173,26 @@ Aig_Man_t * Saig_ManTrimPis( Aig_Man_t * p ) /**Function************************************************************* + Synopsis [Duplicates the AIG manager recursively.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Obj_t * Saig_ManAbstractionDfs_rec( Aig_Man_t * pNew, Aig_Obj_t * pObj ) +{ + if ( pObj->pData ) + return (Aig_Obj_t *)pObj->pData; + Saig_ManAbstractionDfs_rec( pNew, Aig_ObjFanin0(pObj) ); + Saig_ManAbstractionDfs_rec( pNew, Aig_ObjFanin1(pObj) ); + return (Aig_Obj_t *)(pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) )); +} + +/**Function************************************************************* + Synopsis [Performs abstraction of the AIG to preserve the included flops.] Description [] @@ -202,14 +202,14 @@ Aig_Man_t * Saig_ManTrimPis( Aig_Man_t * p ) SeeAlso [] ***********************************************************************/ -Aig_Man_t * Saig_ManDeriveAbstraction( Aig_Man_t * p, Vec_Int_t * vFlops ) +Aig_Man_t * Saig_ManDupAbstraction( Aig_Man_t * p, Vec_Int_t * vFlops ) { Aig_Man_t * pNew;//, * pTemp; Aig_Obj_t * pObj, * pObjLi, * pObjLo; int i, Entry; Aig_ManCleanData( p ); // start the new manager - pNew = Aig_ManStart( Aig_ManNodeNum(p) ); + pNew = Aig_ManStart( 5000 ); pNew->pName = Aig_UtilStrsav( p->pName ); // map the constant node Aig_ManConst1(p)->pData = Aig_ManConst1( pNew ); |