diff options
Diffstat (limited to 'src/proof/dch/dchMan.c')
| -rw-r--r-- | src/proof/dch/dchMan.c | 191 |
1 files changed, 191 insertions, 0 deletions
diff --git a/src/proof/dch/dchMan.c b/src/proof/dch/dchMan.c new file mode 100644 index 00000000..dc856309 --- /dev/null +++ b/src/proof/dch/dchMan.c @@ -0,0 +1,191 @@ +/**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 + |