From 0080244a89eaaccd64c64af8f394486ab5d3e5b5 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Wed, 2 Apr 2008 08:01:00 -0700 Subject: Version abc80402 --- src/aig/dar/dar.h | 2 +- src/aig/dar/darBalance.c | 33 ++++++++++++++++++++++++++++++++- src/aig/dar/darScript.c | 37 ++++++++----------------------------- 3 files changed, 41 insertions(+), 31 deletions(-) (limited to 'src/aig/dar') diff --git a/src/aig/dar/dar.h b/src/aig/dar/dar.h index 1cc239b1..99c0276d 100644 --- a/src/aig/dar/dar.h +++ b/src/aig/dar/dar.h @@ -80,6 +80,7 @@ extern void Dar_LibStart(); extern void Dar_LibStop(); /*=== darBalance.c ========================================================*/ extern Aig_Man_t * Dar_ManBalance( Aig_Man_t * p, int fUpdateLevel ); +extern Aig_Man_t * Dar_ManBalanceXor( Aig_Man_t * pAig, int fExor, int fUpdateLevel, int fVerbose ); extern void Dar_BalancePrintStats( Aig_Man_t * p ); /*=== darCore.c ========================================================*/ extern void Dar_ManDefaultRwrParams( Dar_RwrPar_t * pPars ); @@ -94,7 +95,6 @@ extern Aig_Man_t * Dar_ManRwsat( Aig_Man_t * pAig, int fBalance, int fVerbos extern Aig_Man_t * Dar_ManCompress( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fVerbose ); extern Aig_Man_t * Dar_ManCompress2( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fFanout, int fVerbose ); extern Aig_Man_t * Dar_ManChoice( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fConstruct, int nConfMax, int nLevelMax, int fVerbose ); -extern Aig_Man_t * Dar_ManBalanceXor( Aig_Man_t * pAig, int fExor, int fUpdateLevel, int fVerbose ); #ifdef __cplusplus } diff --git a/src/aig/dar/darBalance.c b/src/aig/dar/darBalance.c index 63f6f232..6e78041a 100644 --- a/src/aig/dar/darBalance.c +++ b/src/aig/dar/darBalance.c @@ -333,7 +333,7 @@ Aig_Obj_t * Dar_Balance_rec( Aig_Man_t * pNew, Aig_Obj_t * pObjOld, Vec_Vec_t * if ( vSuper->nSize == 0 ) return pObjOld->pData = Aig_ManConst0(pNew); if ( Vec_PtrSize(vSuper) < 2 ) - printf( "BUG!\n" ); + printf( "Dar_Balance_rec: Internal error!\n" ); // for each old node, derive the new well-balanced node for ( i = 0; i < Vec_PtrSize(vSuper); i++ ) { @@ -366,9 +366,11 @@ Aig_Man_t * Dar_ManBalance( Aig_Man_t * p, int fUpdateLevel ) Aig_Obj_t * pObj, * pDriver, * pObjNew; Vec_Vec_t * vStore; int i; + assert( Aig_ManVerifyTopoOrder(p) ); // create the new manager pNew = Aig_ManStart( Aig_ManObjNumMax(p) ); pNew->pName = Aig_UtilStrsav( p->pName ); + pNew->pSpec = Aig_UtilStrsav( p->pSpec ); pNew->nRegs = p->nRegs; pNew->nAsserts = p->nAsserts; if ( p->vFlopNums ) @@ -437,6 +439,35 @@ Aig_Man_t * Dar_ManBalance( Aig_Man_t * p, int fUpdateLevel ) return pNew; } +/**Function************************************************************* + + Synopsis [Reproduces script "compress2".] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Dar_ManBalanceXor( Aig_Man_t * pAig, int fExor, int fUpdateLevel, int fVerbose ) +{ + Aig_Man_t * pAigXor, * pRes; + if ( fExor ) + { + pAigXor = Aig_ManDupExor( pAig ); + if ( fVerbose ) + Dar_BalancePrintStats( pAigXor ); + pRes = Dar_ManBalance( pAigXor, fUpdateLevel ); + Aig_ManStop( pAigXor ); + } + else + { + pRes = Dar_ManBalance( pAig, fUpdateLevel ); + } + return pRes; +} + /**Function************************************************************* Synopsis [Inserts a new node in the order by levels.] diff --git a/src/aig/dar/darScript.c b/src/aig/dar/darScript.c index 2a0aa7d5..7d78bf40 100644 --- a/src/aig/dar/darScript.c +++ b/src/aig/dar/darScript.c @@ -341,11 +341,19 @@ Vec_Ptr_t * Dar_ManChoiceSynthesis( Aig_Man_t * pAig, int fBalance, int fUpdateL //Aig_ManPrintStats( pAig ); Aig_ManForEachObj( pAig, pObj, i ) + { + pObj->pNext = pObj->pHaig; pObj->pHaig = pObj; + } pAig = Dar_ManCompress2(pAig, fBalance, fUpdateLevel, 1, fVerbose); Vec_PtrPush( vAigs, pAig ); //Aig_ManPrintStats( pAig ); + + pAig = Vec_PtrEntry( vAigs, 1 ); + Aig_ManForEachObj( pAig, pObj, i ) + pObj->pHaig = pObj->pNext; + return vAigs; } @@ -399,35 +407,6 @@ PRT( "Choicing time ", clock() - clk ); // return NULL; } -/**Function************************************************************* - - Synopsis [Reproduces script "compress2".] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Aig_Man_t * Dar_ManBalanceXor( Aig_Man_t * pAig, int fExor, int fUpdateLevel, int fVerbose ) -{ - Aig_Man_t * pAigXor, * pRes; - if ( fExor ) - { - pAigXor = Aig_ManDupExor( pAig ); - if ( fVerbose ) - Dar_BalancePrintStats( pAigXor ); - pRes = Dar_ManBalance( pAigXor, fUpdateLevel ); - Aig_ManStop( pAigXor ); - } - else - { - pRes = Dar_ManBalance( pAig, fUpdateLevel ); - } - return pRes; -} - //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// -- cgit v1.2.3