diff options
Diffstat (limited to 'src/aig/dch/dchMan.c')
| -rw-r--r-- | src/aig/dch/dchMan.c | 191 |
1 files changed, 0 insertions, 191 deletions
diff --git a/src/aig/dch/dchMan.c b/src/aig/dch/dchMan.c deleted file mode 100644 index dc856309..00000000 --- a/src/aig/dch/dchMan.c +++ /dev/null @@ -1,191 +0,0 @@ -/**CFile**************************************************************** - - FileName [dchMan.c] - - SystemName [ABC: Logic synthesis and verification system.] - - PackageName [Choice computation for tech-mapping.] - - Synopsis [Calls to the SAT solver.] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - June 29, 2008.] - - Revision [$Id: dchMan.c,v 1.00 2008/07/29 00:00:00 alanmi Exp $] - -***********************************************************************/ - -#include "dchInt.h" - -ABC_NAMESPACE_IMPL_START - - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [Creates the manager.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -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->pAigTotal = pAig; //Dch_DeriveTotalAig( vAigs ); - Aig_ManFanoutStart( p->pAigTotal ); - // SAT solving - p->nSatVars = 1; - p->pSatVars = ABC_CALLOC( int, Aig_ManObjNumMax(p->pAigTotal) ); - p->vUsedNodes = Vec_PtrAlloc( 1000 ); - p->vFanins = Vec_PtrAlloc( 100 ); - p->vSimRoots = Vec_PtrAlloc( 1000 ); - p->vSimClasses = Vec_PtrAlloc( 1000 ); - // equivalences proved - p->pReprsProved = ABC_CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p->pAigTotal) ); - return p; -} - -/**Function************************************************************* - - Synopsis [Prints stats of the manager.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Dch_ManPrintStats( Dch_Man_t * p ) -{ - int nNodeNum = Aig_ManNodeNum(p->pAigTotal) / 3; - Abc_Print( 1, "Parameters: Sim words = %d. Conf limit = %d. SAT var max = %d.\n", - p->pPars->nWords, p->pPars->nBTLimit, p->pPars->nSatVarMax ); - Abc_Print( 1, "AIG nodes : Total = %6d. Dangling = %6d. Main = %6d. (%6.2f %%)\n", - Aig_ManNodeNum(p->pAigTotal), - Aig_ManNodeNum(p->pAigTotal)-nNodeNum, - nNodeNum, - 100.0 * nNodeNum/Aig_ManNodeNum(p->pAigTotal) ); - Abc_Print( 1, "SAT solver: Vars = %d. Max cone = %d. Recycles = %d.\n", - p->nSatVars, p->nConeMax, p->nRecycles ); - Abc_Print( 1, "SAT calls : All = %6d. Unsat = %6d. Sat = %6d. Fail = %6d.\n", - p->nSatCalls, p->nSatCalls-p->nSatCallsSat-p->nSatFailsReal, - p->nSatCallsSat, p->nSatFailsReal ); - Abc_Print( 1, "Choices : Lits = %6d. Reprs = %5d. Equivs = %5d. Choices = %5d.\n", - p->nLits, p->nReprs, p->nEquivs, p->nChoices ); - Abc_Print( 1, "Choicing runtime statistics:\n" ); - p->timeOther = p->timeTotal-p->timeSimInit-p->timeSimSat-p->timeSat-p->timeChoice; - Abc_PrintTimeP( 1, "Sim init ", p->timeSimInit, p->timeTotal ); - Abc_PrintTimeP( 1, "Sim SAT ", p->timeSimSat, p->timeTotal ); - Abc_PrintTimeP( 1, "SAT solving", p->timeSat, p->timeTotal ); - Abc_PrintTimeP( 1, " sat ", p->timeSatSat, p->timeTotal ); - Abc_PrintTimeP( 1, " unsat ", p->timeSatUnsat, p->timeTotal ); - Abc_PrintTimeP( 1, " undecided", p->timeSatUndec, p->timeTotal ); - Abc_PrintTimeP( 1, "Choice ", p->timeChoice, p->timeTotal ); - Abc_PrintTimeP( 1, "Other ", p->timeOther, p->timeTotal ); - Abc_PrintTimeP( 1, "TOTAL ", p->timeTotal, p->timeTotal ); - if ( p->pPars->timeSynth ) - { - Abc_PrintTime( 1, "Synthesis ", p->pPars->timeSynth ); - } -} - -/**Function************************************************************* - - Synopsis [Frees the manager.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Dch_ManStop( Dch_Man_t * p ) -{ - Aig_ManFanoutStop( p->pAigTotal ); - if ( p->pPars->fVerbose ) - Dch_ManPrintStats( p ); - if ( p->pAigFraig ) - Aig_ManStop( p->pAigFraig ); - if ( p->ppClasses ) - Dch_ClassesStop( p->ppClasses ); - if ( p->pSat ) - sat_solver_delete( p->pSat ); - Vec_PtrFree( p->vUsedNodes ); - Vec_PtrFree( p->vFanins ); - Vec_PtrFree( p->vSimRoots ); - Vec_PtrFree( p->vSimClasses ); - ABC_FREE( p->pReprsProved ); - ABC_FREE( p->pSatVars ); - ABC_FREE( p ); -} - -/**Function************************************************************* - - Synopsis [Recycles the SAT solver.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Dch_ManSatSolverRecycle( Dch_Man_t * p ) -{ - int Lit; - if ( p->pSat ) - { - Aig_Obj_t * pObj; - int i; - Vec_PtrForEachEntry( Aig_Obj_t *, p->vUsedNodes, pObj, i ) - Dch_ObjSetSatNum( p, pObj, 0 ); - Vec_PtrClear( p->vUsedNodes ); -// memset( p->pSatVars, 0, sizeof(int) * Aig_ManObjNumMax(p->pAigTotal) ); - sat_solver_delete( p->pSat ); - } - p->pSat = sat_solver_new(); - sat_solver_setnvars( p->pSat, 1000 ); - // var 0 is not used - // var 1 is reserved for const1 node - add the clause - p->nSatVars = 1; -// p->nSatVars = 0; - Lit = toLit( p->nSatVars ); - if ( p->pPars->fPolarFlip ) - Lit = lit_neg( Lit ); - sat_solver_addclause( p->pSat, &Lit, &Lit + 1 ); - Dch_ObjSetSatNum( p, Aig_ManConst1(p->pAigFraig), p->nSatVars++ ); - - p->nRecycles++; - p->nCallsSince = 0; -} - - - - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - -ABC_NAMESPACE_IMPL_END - |