diff options
Diffstat (limited to 'src/proof/ssw/sswMan.c')
| -rw-r--r-- | src/proof/ssw/sswMan.c | 218 |
1 files changed, 218 insertions, 0 deletions
diff --git a/src/proof/ssw/sswMan.c b/src/proof/ssw/sswMan.c new file mode 100644 index 00000000..c635569d --- /dev/null +++ b/src/proof/ssw/sswMan.c @@ -0,0 +1,218 @@ +/**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" + +ABC_NAMESPACE_IMPL_START + + +//////////////////////////////////////////////////////////////////////// +/// 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; + // prepare the sequential AIG + assert( Saig_ManRegNum(pAig) > 0 ); + Aig_ManFanoutStart( pAig ); + Aig_ManSetPioNumbers( pAig ); + // create interpolation manager + p = ABC_ALLOC( Ssw_Man_t, 1 ); + memset( p, 0, sizeof(Ssw_Man_t) ); + p->pPars = pPars; + p->pAig = pAig; + p->nFrames = pPars->nFramesK + 1; + p->pNodeToFrames = ABC_CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p->pAig) * p->nFrames ); + p->vCommon = Vec_PtrAlloc( 100 ); + p->iOutputLit = -1; + // allocate storage for sim pattern + p->nPatWords = Abc_BitWordNum( Saig_ManPiNum(pAig) * p->nFrames + Saig_ManRegNum(pAig) ); + p->pPatWords = ABC_CALLOC( unsigned, p->nPatWords ); + // other + p->vNewLos = Vec_PtrAlloc( 100 ); + p->vNewPos = Vec_IntAlloc( 100 ); + p->vResimConsts = Vec_PtrAlloc( 100 ); + p->vResimClasses = Vec_PtrAlloc( 100 ); +// p->pPars->fVerbose = 1; + 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 += ( 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 ) +{ + double nMemory = 1.0*Aig_ManObjNumMax(p->pAig)*p->nFrames*(2*sizeof(int)+2*sizeof(void*))/(1<<20); + + printf( "Parameters: F = %d. AddF = %d. C-lim = %d. Constr = %d. MaxLev = %d. Mem = %0.2f Mb.\n", + p->pPars->nFramesK, p->pPars->nFramesAddSim, p->pPars->nBTLimit, Saig_ManConstrNum(p->pAig), p->pPars->nMaxLevs, nMemory ); + printf( "AIG : PI = %d. PO = %d. Latch = %d. Node = %d. Ave SAT vars = %d.\n", + Saig_ManPiNum(p->pAig), Saig_ManPoNum(p->pAig), Saig_ManRegNum(p->pAig), Aig_ManNodeNum(p->pAig), + 0/(p->pPars->nIters+1) ); + printf( "SAT calls : Proof = %d. Cex = %d. Fail = %d. Lits proved = %d.\n", + p->nSatProof, p->nSatCallsSat, p->nSatFailsReal, Ssw_ManCountEquivs(p) ); + printf( "SAT solver: Vars max = %d. Calls max = %d. Recycles = %d. Sim rounds = %d.\n", + p->nVarsMax, p->nCallsMax, p->nRecyclesTotal, p->nSimRounds ); + printf( "NBeg = %d. NEnd = %d. (Gain = %6.2f %%). RBeg = %d. REnd = %d. (Gain = %6.2f %%).\n", + p->nNodesBeg, p->nNodesEnd, 100.0*(p->nNodesBeg-p->nNodesEnd)/(p->nNodesBeg?p->nNodesBeg:1), + p->nRegsBeg, p->nRegsEnd, 100.0*(p->nRegsBeg-p->nRegsEnd)/(p->nRegsBeg?p->nRegsBeg:1) ); + + p->timeOther = p->timeTotal-p->timeBmc-p->timeReduce-p->timeMarkCones-p->timeSimSat-p->timeSat; + ABC_PRTP( "BMC ", p->timeBmc, p->timeTotal ); + ABC_PRTP( "Spec reduce", p->timeReduce, p->timeTotal ); + ABC_PRTP( "Mark cones ", p->timeMarkCones, p->timeTotal ); + ABC_PRTP( "Sim SAT ", p->timeSimSat, p->timeTotal ); + ABC_PRTP( "SAT solving", p->timeSat, p->timeTotal ); + ABC_PRTP( " unsat ", p->timeSatUnsat, p->timeTotal ); + ABC_PRTP( " sat ", p->timeSatSat, p->timeTotal ); + ABC_PRTP( " undecided", p->timeSatUndec, p->timeTotal ); + ABC_PRTP( "Other ", p->timeOther, p->timeTotal ); + ABC_PRTP( "TOTAL ", p->timeTotal, p->timeTotal ); + + // report the reductions + if ( p->pAig->nConstrs ) + { + printf( "Statistics reflecting the use of constraints:\n" ); + printf( "Total cones = %6d. Constraint cones = %6d. (%6.2f %%)\n", + p->nConesTotal, p->nConesConstr, 100.0*p->nConesConstr/p->nConesTotal ); + printf( "Total equivs = %6d. Removed equivs = %6d. (%6.2f %%)\n", + p->nEquivsTotal, p->nEquivsConstr, 100.0*p->nEquivsConstr/p->nEquivsTotal ); + printf( "NBeg = %d. NEnd = %d. (Gain = %6.2f %%). RBeg = %d. REnd = %d. (Gain = %6.2f %%).\n", + p->nNodesBegC, p->nNodesEndC, 100.0*(p->nNodesBegC-p->nNodesEndC)/(p->nNodesBegC?p->nNodesBegC:1), + p->nRegsBegC, p->nRegsEndC, 100.0*(p->nRegsBegC-p->nRegsEndC)/(p->nRegsBegC?p->nRegsBegC:1) ); + } +} + +/**Function************************************************************* + + Synopsis [Frees the manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ssw_ManCleanup( Ssw_Man_t * p ) +{ +// Aig_ManCleanMarkAB( p->pAig ); + assert( p->pMSat == NULL ); + if ( p->pFrames ) + { + Aig_ManCleanMarkAB( p->pFrames ); + Aig_ManStop( p->pFrames ); + p->pFrames = NULL; + memset( p->pNodeToFrames, 0, sizeof(Aig_Obj_t *) * Aig_ManObjNumMax(p->pAig) * p->nFrames ); + } + if ( p->vSimInfo ) + { + Vec_PtrFree( p->vSimInfo ); + p->vSimInfo = NULL; + } + p->nConstrTotal = 0; + p->nConstrReduced = 0; +} + +/**Function************************************************************* + + Synopsis [Frees the manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ssw_ManStop( Ssw_Man_t * p ) +{ + ABC_FREE( p->pVisited ); + if ( p->pPars->fVerbose )//&& p->pPars->nStepsMax == -1 ) + Ssw_ManPrintStats( p ); + if ( p->ppClasses ) + Ssw_ClassesStop( p->ppClasses ); + if ( p->pSml ) + Ssw_SmlStop( p->pSml ); + if ( p->vDiffPairs ) + Vec_IntFree( p->vDiffPairs ); + if ( p->vInits ) + Vec_IntFree( p->vInits ); + Vec_PtrFree( p->vResimConsts ); + Vec_PtrFree( p->vResimClasses ); + Vec_PtrFree( p->vNewLos ); + Vec_IntFree( p->vNewPos ); + Vec_PtrFree( p->vCommon ); + ABC_FREE( p->pNodeToFrames ); + ABC_FREE( p->pPatWords ); + ABC_FREE( p ); +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + |