diff options
Diffstat (limited to 'src/aig/ssw/sswMan.c')
| -rw-r--r-- | src/aig/ssw/sswMan.c | 206 |
1 files changed, 206 insertions, 0 deletions
diff --git a/src/aig/ssw/sswMan.c b/src/aig/ssw/sswMan.c new file mode 100644 index 00000000..86144ebb --- /dev/null +++ b/src/aig/ssw/sswMan.c @@ -0,0 +1,206 @@ +/**CFile**************************************************************** + + FileName [sswMan.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Inductive prover with constraints.] + + Synopsis [Calls to the SAT solver.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - September 1, 2008.] + + Revision [$Id: sswMan.c,v 1.00 2008/09/01 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "sswInt.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Creates the manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Ssw_Man_t * Ssw_ManCreate( Aig_Man_t * pAig, Ssw_Pars_t * pPars ) +{ + Ssw_Man_t * p; + // create interpolation manager + p = ALLOC( Ssw_Man_t, 1 ); + memset( p, 0, sizeof(Ssw_Man_t) ); + p->pPars = pPars; + p->pAig = pAig; + p->nFrames = pPars->nFramesK + 1; + Aig_ManFanoutStart( pAig ); + // SAT solving + p->nSatVars = 1; + p->pSatVars = CALLOC( int, Aig_ManObjNumMax(p->pAig) ); + p->vFanins = Vec_PtrAlloc( 100 ); + p->vSimRoots = Vec_PtrAlloc( 1000 ); + p->vSimClasses = Vec_PtrAlloc( 1000 ); + // equivalences proved +// p->pReprsProved = CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p->pAig) ); + p->pNodeToFraig = CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p->pAig) * p->nFrames ); + return p; +} + +/**Function************************************************************* + + Synopsis [Prints stats of the manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ssw_ManCountEquivs( Ssw_Man_t * p ) +{ + Aig_Obj_t * pObj; + int i, nEquivs = 0; + Aig_ManForEachObj( p->pAig, pObj, i ) +// nEquivs += ( p->pReprsProved[i] != NULL ); + nEquivs += ( Aig_ObjRepr(p->pAig, pObj) != NULL ); + return nEquivs; +} + +/**Function************************************************************* + + Synopsis [Prints stats of the manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ssw_ManPrintStats( Ssw_Man_t * p ) +{ + printf( "Parameters: Frames = %d. Conf limit = %d. Constrs = %d.\n", + p->pPars->nFramesK, p->pPars->nBTLimit, p->pPars->nConstrs ); + printf( "AIG : PI = %d. PO = %d. Latch = %d. Node = %d.\n", + Saig_ManPiNum(p->pAig), Saig_ManPoNum(p->pAig), Saig_ManRegNum(p->pAig), Aig_ManNodeNum(p->pAig) ); + printf( "SAT solver: Vars = %d.\n", p->nSatVars ); + printf( "SAT calls : All = %6d. Unsat = %6d. Sat = %6d. Fail = %6d.\n", + p->nSatCalls, p->nSatCalls-p->nSatCallsSat-p->nSatFailsReal, + p->nSatCallsSat, p->nSatFailsReal ); + printf( "Equivs : All = %6d.\n", Ssw_ManCountEquivs(p) ); + printf( "Runtime statistics:\n" ); + p->timeOther = p->timeTotal-p->timeBmc-p->timeReduce-p->timeSimSat-p->timeSat; + PRTP( "BMC ", p->timeBmc, p->timeTotal ); + PRTP( "Spec reduce", p->timeReduce, p->timeTotal ); + PRTP( "Sim SAT ", p->timeSimSat, p->timeTotal ); + PRTP( "SAT solving", p->timeSat, p->timeTotal ); + PRTP( " sat ", p->timeSatSat, p->timeTotal ); + PRTP( " unsat ", p->timeSatUnsat, p->timeTotal ); + PRTP( " undecided", p->timeSatUndec, p->timeTotal ); + PRTP( "Other ", p->timeOther, p->timeTotal ); + PRTP( "TOTAL ", p->timeTotal, p->timeTotal ); +} + +/**Function************************************************************* + + Synopsis [Frees the manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ssw_ManCleanup( Ssw_Man_t * p ) +{ + Aig_ManCleanMarkB( p->pAig ); + if ( p->pFrames ) + { + Aig_ManStop( p->pFrames ); + p->pFrames = NULL; + } + if ( p->pSat ) + { + sat_solver_delete( p->pSat ); + p->pSat = NULL; + p->nSatVars = 0; + } + memset( p->pNodeToFraig, 0, sizeof(Aig_Obj_t *) * Aig_ManObjNumMax(p->pAig) * p->nFrames ); + p->nConstrTotal = 0; + p->nConstrReduced = 0; +} + +/**Function************************************************************* + + Synopsis [Frees the manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ssw_ManStop( Ssw_Man_t * p ) +{ + if ( p->pPars->fVerbose ) + Ssw_ManPrintStats( p ); + if ( p->ppClasses ) + Ssw_ClassesStop( p->ppClasses ); + Vec_PtrFree( p->vFanins ); + Vec_PtrFree( p->vSimRoots ); + Vec_PtrFree( p->vSimClasses ); + FREE( p->pNodeToFraig ); +// FREE( p->pReprsProved ); + FREE( p->pSatVars ); + free( p ); +} + +/**Function************************************************************* + + Synopsis [Starts the SAT solver.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ssw_ManStartSolver( Ssw_Man_t * p ) +{ + int Lit; + assert( p->pSat == NULL ); + p->pSat = sat_solver_new(); + sat_solver_setnvars( p->pSat, 10000 ); + // var 0 is not used + // var 1 is reserved for const1 node - add the clause + Lit = toLit( 1 ); + if ( p->pPars->fPolarFlip ) + Lit = lit_neg( Lit ); + sat_solver_addclause( p->pSat, &Lit, &Lit + 1 ); + p->nSatVars = 2; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + |