From 0398ced8243806439b814f21ca7d6e584cea13a1 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Mon, 22 Jun 2015 23:04:53 -0700 Subject: Version abc90714 committer: Baruch Sterin --- src/aig/dch/dch.h | 3 ++- src/aig/dch/dchCore.c | 29 ++++++++++++++--------------- src/aig/dch/dchInt.h | 4 ++-- src/aig/dch/dchMan.c | 22 ++++++++-------------- 4 files changed, 26 insertions(+), 32 deletions(-) (limited to 'src/aig/dch') diff --git a/src/aig/dch/dch.h b/src/aig/dch/dch.h index 6157a811..38978164 100644 --- a/src/aig/dch/dch.h +++ b/src/aig/dch/dch.h @@ -50,6 +50,7 @@ struct Dch_Pars_t_ int fPower; // uses power-aware rewriting int fUseGia; // uses GIA package int fUseCSat; // uses circuit-based solver + int fLightSynth; // uses lighter version of synthesis int fVerbose; // verbose stats int timeSynth; // synthesis runtime int nNodesAhead; // the lookahead in terms of nodes @@ -66,7 +67,7 @@ struct Dch_Pars_t_ /*=== dchCore.c ==========================================================*/ extern void Dch_ManSetDefaultParams( Dch_Pars_t * p ); -extern Aig_Man_t * Dch_ComputeChoices( Vec_Ptr_t * vAigs, Dch_Pars_t * pPars ); +extern Aig_Man_t * Dch_ComputeChoices( Aig_Man_t * pAig, Dch_Pars_t * pPars ); #ifdef __cplusplus diff --git a/src/aig/dch/dchCore.c b/src/aig/dch/dchCore.c index 8e854355..4a8d8b53 100644 --- a/src/aig/dch/dchCore.c +++ b/src/aig/dch/dchCore.c @@ -49,6 +49,7 @@ void Dch_ManSetDefaultParams( Dch_Pars_t * p ) p->fPolarFlip = 1; // uses polarity adjustment p->fSimulateTfo = 1; // simulate TFO p->fPower = 0; // power-aware rewriting + p->fLightSynth = 0; // uses lighter version of synthesis p->fVerbose = 0; // verbose stats p->nNodesAhead = 1000; // the lookahead in terms of nodes p->nCallsRecycle = 100; // calls to perform before recycling SAT solver @@ -65,37 +66,35 @@ void Dch_ManSetDefaultParams( Dch_Pars_t * p ) SeeAlso [] ***********************************************************************/ -Aig_Man_t * Dch_ComputeChoices( Vec_Ptr_t * vAigs, Dch_Pars_t * pPars ) +Aig_Man_t * Dch_ComputeChoices( Aig_Man_t * pAig, Dch_Pars_t * pPars ) { Dch_Man_t * p; Aig_Man_t * pResult; int clk, clkTotal = clock(); - assert( Vec_PtrSize(vAigs) > 0 ); // reset random numbers Aig_ManRandom(1); // start the choicing manager - p = Dch_ManCreate( vAigs, pPars ); + p = Dch_ManCreate( pAig, pPars ); // compute candidate equivalence classes clk = clock(); - p->ppClasses = Dch_CreateCandEquivClasses( p->pAigTotal, pPars->nWords, pPars->fVerbose ); + p->ppClasses = Dch_CreateCandEquivClasses( pAig, pPars->nWords, pPars->fVerbose ); p->timeSimInit = clock() - clk; // Dch_ClassesPrint( p->ppClasses, 0 ); p->nLits = Dch_ClassesLitNum( p->ppClasses ); // perform SAT sweeping Dch_ManSweep( p ); - // count the number of representatives - p->nReprs = Dch_DeriveChoiceCountReprs( p->pAigTotal ); - // create choices -clk = clock(); - pResult = Dch_DeriveChoiceAig( p->pAigTotal ); -p->timeChoice = clock() - clk; -// Aig_ManCleanup( p->pAigTotal ); -// pResult = Aig_ManDupSimpleDfs( p->pAigTotal ); - // count the number of equivalences and choices - p->nEquivs = Dch_DeriveChoiceCountEquivs( pResult ); - p->nChoices = Aig_ManChoiceNum( pResult ); + // free memory ahead of time p->timeTotal = clock() - clkTotal; Dch_ManStop( p ); + // create choices + ABC_FREE( pAig->pTable ); + pResult = Dch_DeriveChoiceAig( pAig ); + // count the number of representatives + if ( pPars->fVerbose ) + printf( "STATS: Reprs = %6d. Equivs = %6d. Choices = %6d.\n", + Dch_DeriveChoiceCountReprs( pAig ), + Dch_DeriveChoiceCountEquivs( pResult ), + Aig_ManChoiceNum( pResult ) ); return pResult; } diff --git a/src/aig/dch/dchInt.h b/src/aig/dch/dchInt.h index 4e6315a4..a419335d 100644 --- a/src/aig/dch/dchInt.h +++ b/src/aig/dch/dchInt.h @@ -51,7 +51,7 @@ struct Dch_Man_t_ // parameters Dch_Pars_t * pPars; // choicing parameters // AIGs used in the package - Vec_Ptr_t * vAigs; // user-given AIGs +// Vec_Ptr_t * vAigs; // user-given AIGs Aig_Man_t * pAigTotal; // intermediate AIG Aig_Man_t * pAigFraig; // final AIG // equivalence classes @@ -142,7 +142,7 @@ extern int Dch_ClassesRefineConst1Group( Dch_Cla_t * p, Vec_Ptr_t * vR /*=== dchCnf.c ===================================================*/ extern void Dch_CnfNodeAddToSolver( Dch_Man_t * p, Aig_Obj_t * pObj ); /*=== dchMan.c ===================================================*/ -extern Dch_Man_t * Dch_ManCreate( Vec_Ptr_t * vAigs, Dch_Pars_t * pPars ); +extern Dch_Man_t * Dch_ManCreate( Aig_Man_t * pAig, Dch_Pars_t * pPars ); extern void Dch_ManStop( Dch_Man_t * p ); extern void Dch_ManSatSolverRecycle( Dch_Man_t * p ); /*=== dchSat.c ===================================================*/ diff --git a/src/aig/dch/dchMan.c b/src/aig/dch/dchMan.c index caed0ed5..c8bd8533 100644 --- a/src/aig/dch/dchMan.c +++ b/src/aig/dch/dchMan.c @@ -39,15 +39,14 @@ SeeAlso [] ***********************************************************************/ -Dch_Man_t * Dch_ManCreate( Vec_Ptr_t * vAigs, Dch_Pars_t * pPars ) +Dch_Man_t * Dch_ManCreate( Aig_Man_t * pAig, Dch_Pars_t * pPars ) { Dch_Man_t * p; // create interpolation manager p = ABC_ALLOC( Dch_Man_t, 1 ); memset( p, 0, sizeof(Dch_Man_t) ); p->pPars = pPars; - p->vAigs = vAigs; - p->pAigTotal = Dch_DeriveTotalAig( vAigs ); + p->pAigTotal = pAig; //Dch_DeriveTotalAig( vAigs ); Aig_ManFanoutStart( p->pAigTotal ); // SAT solving p->nSatVars = 1; @@ -74,18 +73,14 @@ Dch_Man_t * Dch_ManCreate( Vec_Ptr_t * vAigs, Dch_Pars_t * pPars ) ***********************************************************************/ void Dch_ManPrintStats( Dch_Man_t * p ) { -// Aig_Man_t * pAig; -// int i; -// printf( "Choicing will be performed with %d AIGs:\n", Vec_PtrSize(p->vAigs) ); -// Vec_PtrForEachEntry( p->vAigs, pAig, i ) -// Aig_ManPrintStats( pAig ); + int nNodeNum = Aig_ManNodeNum(p->pAigTotal) / 3; printf( "Parameters: Sim words = %d. Conf limit = %d. SAT var max = %d.\n", p->pPars->nWords, p->pPars->nBTLimit, p->pPars->nSatVarMax ); printf( "AIG nodes : Total = %6d. Dangling = %6d. Main = %6d. (%6.2f %%)\n", Aig_ManNodeNum(p->pAigTotal), - Aig_ManNodeNum(p->pAigTotal)-Aig_ManNodeNum(Vec_PtrEntry(p->vAigs,0)), - Aig_ManNodeNum(Vec_PtrEntry(p->vAigs,0)), - 100.0 * Aig_ManNodeNum(Vec_PtrEntry(p->vAigs,0))/Aig_ManNodeNum(p->pAigTotal) ); + Aig_ManNodeNum(p->pAigTotal)-nNodeNum, + nNodeNum, + 100.0 * nNodeNum/Aig_ManNodeNum(p->pAigTotal) ); printf( "SAT solver: Vars = %d. Max cone = %d. Recycles = %d.\n", p->nSatVars, p->nConeMax, p->nRecycles ); printf( "SAT calls : All = %6d. Unsat = %6d. Sat = %6d. Fail = %6d.\n", @@ -108,7 +103,7 @@ void Dch_ManPrintStats( Dch_Man_t * p ) { ABC_PRT( "Synthesis ", p->pPars->timeSynth ); } -} +} /**Function************************************************************* @@ -123,10 +118,9 @@ void Dch_ManPrintStats( Dch_Man_t * p ) ***********************************************************************/ void Dch_ManStop( Dch_Man_t * p ) { + Aig_ManFanoutStop( p->pAigTotal ); if ( p->pPars->fVerbose ) Dch_ManPrintStats( p ); - if ( p->pAigTotal ) - Aig_ManStop( p->pAigTotal ); if ( p->pAigFraig ) Aig_ManStop( p->pAigFraig ); if ( p->ppClasses ) -- cgit v1.2.3