From 0871bffae307e0553e0c5186336189e8b55cf6a6 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sun, 15 Feb 2009 08:01:00 -0800 Subject: Version abc90215 --- src/aig/ssw/ssw.h | 8 ++++---- src/aig/ssw/sswAig.c | 4 ++-- src/aig/ssw/sswBmc.c | 4 ++-- src/aig/ssw/sswClass.c | 38 +++++++++++++++++++------------------- src/aig/ssw/sswCnf.c | 8 ++++---- src/aig/ssw/sswCore.c | 6 +++--- src/aig/ssw/sswInt.h | 8 ++++---- src/aig/ssw/sswIslands.c | 2 +- src/aig/ssw/sswMan.c | 34 +++++++++++++++++----------------- src/aig/ssw/sswPairs.c | 16 ++++++++-------- src/aig/ssw/sswPart.c | 4 ++-- src/aig/ssw/sswSat.c | 4 ++-- src/aig/ssw/sswSemi.c | 10 +++++----- src/aig/ssw/sswSim.c | 10 +++++----- 14 files changed, 78 insertions(+), 78 deletions(-) (limited to 'src/aig/ssw') diff --git a/src/aig/ssw/ssw.h b/src/aig/ssw/ssw.h index b3222fca..adb98401 100644 --- a/src/aig/ssw/ssw.h +++ b/src/aig/ssw/ssw.h @@ -21,10 +21,6 @@ #ifndef __SSW_H__ #define __SSW_H__ -#ifdef __cplusplus -extern "C" { -#endif - //////////////////////////////////////////////////////////////////////// /// INCLUDES /// //////////////////////////////////////////////////////////////////////// @@ -33,6 +29,10 @@ extern "C" { /// PARAMETERS /// //////////////////////////////////////////////////////////////////////// +#ifdef __cplusplus +extern "C" { +#endif + //////////////////////////////////////////////////////////////////////// /// BASIC TYPES /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/ssw/sswAig.c b/src/aig/ssw/sswAig.c index 97f0a755..62e93d2d 100644 --- a/src/aig/ssw/sswAig.c +++ b/src/aig/ssw/sswAig.c @@ -42,7 +42,7 @@ Ssw_Frm_t * Ssw_FrmStart( Aig_Man_t * pAig ) { Ssw_Frm_t * p; - p = ALLOC( Ssw_Frm_t, 1 ); + p = ABC_ALLOC( Ssw_Frm_t, 1 ); memset( p, 0, sizeof(Ssw_Frm_t) ); p->pAig = pAig; p->nObjs = Aig_ManObjNumMax( pAig ); @@ -69,7 +69,7 @@ void Ssw_FrmStop( Ssw_Frm_t * p ) if ( p->pFrames ) Aig_ManStop( p->pFrames ); Vec_PtrFree( p->vAig2Frm ); - free( p ); + ABC_FREE( p ); } /**Function************************************************************* diff --git a/src/aig/ssw/sswBmc.c b/src/aig/ssw/sswBmc.c index 93859c01..86d04424 100644 --- a/src/aig/ssw/sswBmc.c +++ b/src/aig/ssw/sswBmc.c @@ -161,7 +161,7 @@ int Ssw_BmcDynamic( Aig_Man_t * pAig, int nFramesMax, int nConfLimit, int fVerbo printf( "Solving output %2d of frame %3d ... \r", i % Saig_ManPoNum(pAig), i / Saig_ManPoNum(pAig) ); } - status = sat_solver_solve( pSat->pSat, &Lit, &Lit + 1, (sint64)nConfLimit, (sint64)0, (sint64)0, (sint64)0 ); + status = sat_solver_solve( pSat->pSat, &Lit, &Lit + 1, (ABC_INT64_T)nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); if ( status == l_False ) { /* @@ -199,7 +199,7 @@ int Ssw_BmcDynamic( Aig_Man_t * pAig, int nFramesMax, int nConfLimit, int fVerbo printf( "Conf =%8.0f. Var =%8d. AIG=%9d. ", (double)pSat->pSat->stats.conflicts, pSat->nSatVars, Aig_ManNodeNum(pFrm->pFrames) ); - PRT( "T", clock() - clkPart ); + ABC_PRT( "T", clock() - clkPart ); clkPart = clock(); fflush( stdout ); } diff --git a/src/aig/ssw/sswClass.c b/src/aig/ssw/sswClass.c index 3528ae27..5d0be217 100644 --- a/src/aig/ssw/sswClass.c +++ b/src/aig/ssw/sswClass.c @@ -136,11 +136,11 @@ static inline Aig_Obj_t ** Ssw_ObjRemoveClass( Ssw_Cla_t * p, Aig_Obj_t * pRepr Ssw_Cla_t * Ssw_ClassesStart( Aig_Man_t * pAig ) { Ssw_Cla_t * p; - p = ALLOC( Ssw_Cla_t, 1 ); + p = ABC_ALLOC( Ssw_Cla_t, 1 ); memset( p, 0, sizeof(Ssw_Cla_t) ); p->pAig = pAig; - p->pId2Class = CALLOC( Aig_Obj_t **, Aig_ManObjNumMax(pAig) ); - p->pClassSizes = CALLOC( int, Aig_ManObjNumMax(pAig) ); + p->pId2Class = ABC_CALLOC( Aig_Obj_t **, Aig_ManObjNumMax(pAig) ); + p->pClassSizes = ABC_CALLOC( int, Aig_ManObjNumMax(pAig) ); p->vClassOld = Vec_PtrAlloc( 100 ); p->vClassNew = Vec_PtrAlloc( 100 ); p->vRefined = Vec_PtrAlloc( 1000 ); @@ -187,10 +187,10 @@ void Ssw_ClassesStop( Ssw_Cla_t * p ) if ( p->vClassNew ) Vec_PtrFree( p->vClassNew ); if ( p->vClassOld ) Vec_PtrFree( p->vClassOld ); Vec_PtrFree( p->vRefined ); - FREE( p->pId2Class ); - FREE( p->pClassSizes ); - FREE( p->pMemClasses ); - free( p ); + ABC_FREE( p->pId2Class ); + ABC_FREE( p->pClassSizes ); + ABC_FREE( p->pMemClasses ); + ABC_FREE( p ); } /**Function************************************************************* @@ -500,8 +500,8 @@ int Ssw_ClassesPrepareRehash( Ssw_Cla_t * p, Vec_Ptr_t * vCands ) // allocate the hash table hashing simulation info into nodes nTableSize = Aig_PrimeCudd( Vec_PtrSize(vCands)/2 ); - ppTable = CALLOC( Aig_Obj_t *, nTableSize ); - ppNexts = CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p->pAig) ); + ppTable = ABC_CALLOC( Aig_Obj_t *, nTableSize ); + ppNexts = ABC_CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p->pAig) ); // sort through the candidates nEntries = 0; @@ -568,8 +568,8 @@ int Ssw_ClassesPrepareRehash( Ssw_Cla_t * p, Vec_Ptr_t * vCands ) } p->pMemClassesFree += nEntries2; assert( nEntries == nEntries2 ); - free( ppTable ); - free( ppNexts ); + ABC_FREE( ppTable ); + ABC_FREE( ppNexts ); // now it is time to refine the classes return Ssw_ClassesRefine( p, 1 ); } @@ -615,7 +615,7 @@ if ( fVerbose ) printf( "Allocated %.2f Mb to store simulation information.\n", 1.0*(sizeof(unsigned) * Aig_ManObjNumMax(pAig) * nFrames * nWords)/(1<<20) ); printf( "Initial simulation of %d frames with %d words. ", nFrames, nWords ); - PRT( "Time", clock() - clk ); + ABC_PRT( "Time", clock() - clk ); } // set comparison procedures @@ -643,7 +643,7 @@ clk = clock(); } // allocate room for classes - p->pMemClasses = ALLOC( Aig_Obj_t *, Vec_PtrSize(vCands) ); + p->pMemClasses = ABC_ALLOC( Aig_Obj_t *, Vec_PtrSize(vCands) ); p->pMemClassesFree = p->pMemClasses; // now it is time to refine the classes @@ -651,7 +651,7 @@ clk = clock(); if ( fVerbose ) { printf( "Collecting candidate equivalence classes. " ); -PRT( "Time", clock() - clk ); +ABC_PRT( "Time", clock() - clk ); } clk = clock(); @@ -677,7 +677,7 @@ if ( fVerbose ) { printf( "Simulation of %d frames with %d words (%2d rounds). ", nFrames, nWords, i-1 ); - PRT( "Time", clock() - clk ); + ABC_PRT( "Time", clock() - clk ); } Ssw_ClassesCheck( p ); // Ssw_ClassesPrint( p, 0 ); @@ -723,7 +723,7 @@ Ssw_Cla_t * Ssw_ClassesPrepareSimple( Aig_Man_t * pAig, int fLatchCorr, int nMax p->nCands1++; } // allocate room for classes - p->pMemClassesFree = p->pMemClasses = ALLOC( Aig_Obj_t *, p->nCands1 ); + p->pMemClassesFree = p->pMemClasses = ABC_ALLOC( Aig_Obj_t *, p->nCands1 ); // Ssw_ClassesPrint( p, 0 ); return p; } @@ -754,7 +754,7 @@ Ssw_Cla_t * Ssw_ClassesPrepareTargets( Aig_Man_t * pAig ) p->nCands1++; } // allocate room for classes - p->pMemClassesFree = p->pMemClasses = ALLOC( Aig_Obj_t *, p->nCands1 ); + p->pMemClassesFree = p->pMemClasses = ABC_ALLOC( Aig_Obj_t *, p->nCands1 ); // Ssw_ClassesPrint( p, 0 ); return p; } @@ -783,7 +783,7 @@ Ssw_Cla_t * Ssw_ClassesPreparePairs( Aig_Man_t * pAig, Vec_Int_t ** pvClasses ) for ( i = 0; i < Aig_ManObjNumMax(pAig); i++ ) nTotalObjs += pvClasses[i] ? Vec_IntSize(pvClasses[i]) : 0; // allocate memory for classes - p->pMemClasses = ALLOC( Aig_Obj_t *, nTotalObjs ); + p->pMemClasses = ABC_ALLOC( Aig_Obj_t *, nTotalObjs ); // create constant-1 class if ( pvClasses[0] ) Vec_IntForEachEntry( pvClasses[0], Entry, i ) @@ -845,7 +845,7 @@ Ssw_Cla_t * Ssw_ClassesPreparePairsSimple( Aig_Man_t * pMiter, Vec_Int_t * vPair // start the classes p = Ssw_ClassesStart( pMiter ); // allocate memory for classes - p->pMemClasses = ALLOC( Aig_Obj_t *, Vec_IntSize(vPairs) ); + p->pMemClasses = ABC_ALLOC( Aig_Obj_t *, Vec_IntSize(vPairs) ); // create classes for ( i = 0; i < Vec_IntSize(vPairs); i += 2 ) { diff --git a/src/aig/ssw/sswCnf.c b/src/aig/ssw/sswCnf.c index c5ea9b28..73fa0b02 100644 --- a/src/aig/ssw/sswCnf.c +++ b/src/aig/ssw/sswCnf.c @@ -43,7 +43,7 @@ Ssw_Sat_t * Ssw_SatStart( int fPolarFlip ) { Ssw_Sat_t * p; int Lit; - p = ALLOC( Ssw_Sat_t, 1 ); + p = ABC_ALLOC( Ssw_Sat_t, 1 ); memset( p, 0, sizeof(Ssw_Sat_t) ); p->pAig = NULL; p->fPolarFlip = fPolarFlip; @@ -84,7 +84,7 @@ void Ssw_SatStop( Ssw_Sat_t * p ) Vec_IntFree( p->vSatVars ); Vec_PtrFree( p->vFanins ); Vec_PtrFree( p->vUsedPis ); - free( p ); + ABC_FREE( p ); } /**Function************************************************************* @@ -225,7 +225,7 @@ void Ssw_AddClausesSuper( Ssw_Sat_t * p, Aig_Obj_t * pNode, Vec_Ptr_t * vSuper ) assert( Aig_ObjIsNode( pNode ) ); // create storage for literals nLits = Vec_PtrSize(vSuper) + 1; - pLits = ALLOC( int, nLits ); + pLits = ABC_ALLOC( int, nLits ); // suppose AND-gate is A & B = C // add !A => !C or A + !C Vec_PtrForEachEntry( vSuper, pFanin, i ) @@ -256,7 +256,7 @@ void Ssw_AddClausesSuper( Ssw_Sat_t * p, Aig_Obj_t * pNode, Vec_Ptr_t * vSuper ) } RetValue = sat_solver_addclause( p->pSat, pLits, pLits + nLits ); assert( RetValue ); - free( pLits ); + ABC_FREE( pLits ); } /**Function************************************************************* diff --git a/src/aig/ssw/sswCore.c b/src/aig/ssw/sswCore.c index 38a36022..485a5146 100644 --- a/src/aig/ssw/sswCore.c +++ b/src/aig/ssw/sswCore.c @@ -157,7 +157,7 @@ clk = clock(); nIter, Ssw_ClassesCand1Num(p->ppClasses), Ssw_ClassesClassNum(p->ppClasses), p->nSatProof-nSatProof, p->nSatCallsSat-nSatCallsSat, p->nRecycles-nRecycles, p->nSatFailsReal-nSatFailsReal ); - PRT( "T", clock() - clk ); + ABC_PRT( "T", clock() - clk ); } } else @@ -180,7 +180,7 @@ clk = clock(); printf( "R =%4d. ", p->nRecycles-nRecycles ); } printf( "F =%5d. ", p->nSatFailsReal-nSatFailsReal ); - PRT( "T", clock() - clk ); + ABC_PRT( "T", clock() - clk ); } // if ( p->pPars->fDynamic && p->nSatCallsSat-nSatCallsSat < 100 ) // p->pPars->nBTLimit = 10000; @@ -299,7 +299,7 @@ Aig_Man_t * Ssw_SignalCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars ) Ssw_ClassesSetData( p->ppClasses, NULL, NULL, Ssw_SmlObjIsConstBit, Ssw_SmlObjsAreEqualBit ); } if ( p->pPars->fLocalSim ) - p->pVisited = CALLOC( int, Ssw_SmlNumFrames( p->pSml ) * Aig_ManObjNumMax(p->pAig) ); + p->pVisited = ABC_CALLOC( int, Ssw_SmlNumFrames( p->pSml ) * Aig_ManObjNumMax(p->pAig) ); // perform refinement of classes pAigNew = Ssw_SignalCorrespondenceRefine( p ); if ( pPars->fUniqueness ) diff --git a/src/aig/ssw/sswInt.h b/src/aig/ssw/sswInt.h index 930796fc..269bdad7 100644 --- a/src/aig/ssw/sswInt.h +++ b/src/aig/ssw/sswInt.h @@ -21,10 +21,6 @@ #ifndef __SSW_INT_H__ #define __SSW_INT_H__ -#ifdef __cplusplus -extern "C" { -#endif - //////////////////////////////////////////////////////////////////////// /// INCLUDES /// //////////////////////////////////////////////////////////////////////// @@ -37,6 +33,10 @@ extern "C" { /// PARAMETERS /// //////////////////////////////////////////////////////////////////////// +#ifdef __cplusplus +extern "C" { +#endif + //////////////////////////////////////////////////////////////////////// /// BASIC TYPES /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/ssw/sswIslands.c b/src/aig/ssw/sswIslands.c index 64515f3e..8913116c 100644 --- a/src/aig/ssw/sswIslands.c +++ b/src/aig/ssw/sswIslands.c @@ -491,7 +491,7 @@ int Ssw_SecWithSimilarityPairs( Aig_Man_t * p0, Aig_Man_t * p1, Vec_Int_t * vPai else printf( "Verification UNDECIDED. The number of remaining regs = %d (total = %d). ", Aig_ManRegNum(pAigRes), Aig_ManRegNum(p0)+Aig_ManRegNum(p1) ); - PRT( "Time", clock() - clk ); + ABC_PRT( "Time", clock() - clk ); Aig_ManStop( pAigRes ); return RetValue; } diff --git a/src/aig/ssw/sswMan.c b/src/aig/ssw/sswMan.c index 7e6e4473..90cc9028 100644 --- a/src/aig/ssw/sswMan.c +++ b/src/aig/ssw/sswMan.c @@ -47,17 +47,17 @@ Ssw_Man_t * Ssw_ManCreate( Aig_Man_t * pAig, Ssw_Pars_t * pPars ) Aig_ManFanoutStart( pAig ); Aig_ManSetPioNumbers( pAig ); // create interpolation manager - p = ALLOC( Ssw_Man_t, 1 ); + 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 = CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p->pAig) * p->nFrames ); + 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 = Aig_BitWordNum( Saig_ManPiNum(pAig) * p->nFrames + Saig_ManRegNum(pAig) ); - p->pPatWords = ALLOC( unsigned, p->nPatWords ); + p->pPatWords = ABC_ALLOC( unsigned, p->nPatWords ); // other p->vNewLos = Vec_PtrAlloc( 100 ); p->vNewPos = Vec_IntAlloc( 100 ); @@ -117,16 +117,16 @@ void Ssw_ManPrintStats( Ssw_Man_t * p ) 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; - PRTP( "BMC ", p->timeBmc, p->timeTotal ); - PRTP( "Spec reduce", p->timeReduce, p->timeTotal ); - PRTP( "Mark cones ", p->timeMarkCones, p->timeTotal ); - PRTP( "Sim SAT ", p->timeSimSat, p->timeTotal ); - PRTP( "SAT solving", p->timeSat, p->timeTotal ); - PRTP( " unsat ", p->timeSatUnsat, p->timeTotal ); - PRTP( " sat ", p->timeSatSat, p->timeTotal ); - PRTP( " undecided", p->timeSatUndec, p->timeTotal ); - PRTP( "Other ", p->timeOther, p->timeTotal ); - PRTP( "TOTAL ", p->timeTotal, p->timeTotal ); + 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 ); } /**Function************************************************************* @@ -173,7 +173,7 @@ void Ssw_ManCleanup( Ssw_Man_t * p ) ***********************************************************************/ void Ssw_ManStop( Ssw_Man_t * p ) { - FREE( p->pVisited ); + ABC_FREE( p->pVisited ); if ( p->pPars->fVerbose ) Ssw_ManPrintStats( p ); if ( p->ppClasses ) @@ -187,9 +187,9 @@ void Ssw_ManStop( Ssw_Man_t * p ) Vec_PtrFree( p->vNewLos ); Vec_IntFree( p->vNewPos ); Vec_PtrFree( p->vCommon ); - FREE( p->pNodeToFrames ); - FREE( p->pPatWords ); - free( p ); + ABC_FREE( p->pNodeToFrames ); + ABC_FREE( p->pPatWords ); + ABC_FREE( p ); } //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/ssw/sswPairs.c b/src/aig/ssw/sswPairs.c index 1af357f9..3c079922 100644 --- a/src/aig/ssw/sswPairs.c +++ b/src/aig/ssw/sswPairs.c @@ -149,8 +149,8 @@ Vec_Int_t ** Ssw_TransformPairsIntoTempClasses( Vec_Int_t * vPairs, int nObjNumM int * pReprs; // mapping nodes into their representatives int Entry, idObj, idRepr, idReprObj, idReprRepr, i; // allocate data-structures - pvClasses = CALLOC( Vec_Int_t *, nObjNumMax ); - pReprs = ALLOC( int, nObjNumMax ); + pvClasses = ABC_CALLOC( Vec_Int_t *, nObjNumMax ); + pReprs = ABC_ALLOC( int, nObjNumMax ); for ( i = 0; i < nObjNumMax; i++ ) pReprs[i] = -1; // consider pairs @@ -231,7 +231,7 @@ Vec_Int_t ** Ssw_TransformPairsIntoTempClasses( Vec_Int_t * vPairs, int nObjNumM } } } - free( pReprs ); + ABC_FREE( pReprs ); return pvClasses; } @@ -252,7 +252,7 @@ void Ssw_FreeTempClasses( Vec_Int_t ** pvClasses, int nObjNumMax ) for ( i = 0; i < nObjNumMax; i++ ) if ( pvClasses[i] ) Vec_IntFree( pvClasses[i] ); - free( pvClasses ); + ABC_FREE( pvClasses ); } /**Function************************************************************* @@ -356,7 +356,7 @@ Aig_Man_t * Ssw_SignalCorrespondeceTestPairs( Aig_Man_t * pAig ) else printf( "Verification UNDECIDED. Remaining registers %d (total %d). ", Aig_ManRegNum(pAigRes), Aig_ManRegNum(pAig) + Aig_ManRegNum(pAigNew) ); - PRT( "Time", clock() - clk ); + ABC_PRT( "Time", clock() - clk ); // cleanup Aig_ManStop( pAigNew ); return pAigRes; @@ -390,7 +390,7 @@ int Ssw_SecWithPairs( Aig_Man_t * pAig1, Aig_Man_t * pAig2, Vec_Int_t * vIds1, V else printf( "Verification UNDECIDED. The number of remaining regs = %d (total = %d). ", Aig_ManRegNum(pAigRes), Aig_ManRegNum(pAig1) + Aig_ManRegNum(pAig2) ); - PRT( "Time", clock() - clk ); + ABC_PRT( "Time", clock() - clk ); // cleanup Aig_ManStop( pAigRes ); return RetValue; @@ -426,7 +426,7 @@ int Ssw_SecGeneral( Aig_Man_t * pAig1, Aig_Man_t * pAig2, Ssw_Pars_t * pPars ) else printf( "Verification UNDECIDED. The number of remaining regs = %d (total = %d). ", Aig_ManRegNum(pAigRes), Aig_ManRegNum(pAig1) + Aig_ManRegNum(pAig2) ); - PRT( "Time", clock() - clk ); + ABC_PRT( "Time", clock() - clk ); // cleanup Aig_ManStop( pAigRes ); return RetValue; @@ -459,7 +459,7 @@ int Ssw_SecGeneralMiter( Aig_Man_t * pMiter, Ssw_Pars_t * pPars ) else printf( "Verification UNDECIDED. The number of remaining regs = %d (total = %d). ", Aig_ManRegNum(pAigRes), Aig_ManRegNum(pMiter) ); - PRT( "Time", clock() - clk ); + ABC_PRT( "Time", clock() - clk ); // cleanup Aig_ManStop( pAigRes ); return RetValue; diff --git a/src/aig/ssw/sswPart.c b/src/aig/ssw/sswPart.c index 9d2ec34e..f481b457 100644 --- a/src/aig/ssw/sswPart.c +++ b/src/aig/ssw/sswPart.c @@ -106,7 +106,7 @@ Aig_Man_t * Ssw_SignalCorrespondencePart( Aig_Man_t * pAig, Ssw_Pars_t * pPars ) Aig_ManStop( pNew ); } Aig_ManStop( pTemp ); - free( pMapBack ); + ABC_FREE( pMapBack ); } // remap the AIG pNew = Aig_ManDupRepr( pAig, 0 ); @@ -118,7 +118,7 @@ Aig_Man_t * Ssw_SignalCorrespondencePart( Aig_Man_t * pAig, Ssw_Pars_t * pPars ) pPars->fVerbose = fVerbose; if ( fVerbose ) { - PRT( "Total time", clock() - clk ); + ABC_PRT( "Total time", clock() - clk ); } return pNew; } diff --git a/src/aig/ssw/sswSat.c b/src/aig/ssw/sswSat.c index 2fd0fba3..21c5c1f1 100644 --- a/src/aig/ssw/sswSat.c +++ b/src/aig/ssw/sswSat.c @@ -81,7 +81,7 @@ int Ssw_NodesAreEquiv( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew ) clk = clock(); RetValue1 = sat_solver_solve( p->pMSat->pSat, pLits, pLits + nLits, - (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 ); + (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); p->timeSat += clock() - clk; if ( RetValue1 == l_False ) { @@ -143,7 +143,7 @@ p->timeSatUndec += clock() - clk; clk = clock(); RetValue1 = sat_solver_solve( p->pMSat->pSat, pLits, pLits + nLits, - (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 ); + (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); p->timeSat += clock() - clk; if ( RetValue1 == l_False ) { diff --git a/src/aig/ssw/sswSemi.c b/src/aig/ssw/sswSemi.c index 572ab076..5f426093 100644 --- a/src/aig/ssw/sswSemi.c +++ b/src/aig/ssw/sswSemi.c @@ -64,7 +64,7 @@ Ssw_Sem_t * Ssw_SemManStart( Ssw_Man_t * pMan, int nConfMax, int fVerbose ) Aig_Obj_t * pObj; int i; // create interpolation manager - p = ALLOC( Ssw_Sem_t, 1 ); + p = ABC_ALLOC( Ssw_Sem_t, 1 ); memset( p, 0, sizeof(Ssw_Sem_t) ); p->nConfMaxStart = nConfMax; p->nConfMax = nConfMax; @@ -85,9 +85,9 @@ Ssw_Sem_t * Ssw_SemManStart( Ssw_Man_t * pMan, int nConfMax, int fVerbose ) // update arrays of the manager assert( 0 ); /* - free( p->pMan->pNodeToFrames ); + ABC_FREE( p->pMan->pNodeToFrames ); Vec_IntFree( p->pMan->vSatVars ); - p->pMan->pNodeToFrames = CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p->pMan->pAig) * p->nFramesSweep ); + p->pMan->pNodeToFrames = ABC_CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p->pMan->pAig) * p->nFramesSweep ); p->pMan->vSatVars = Vec_IntStart( Aig_ManObjNumMax(p->pMan->pAig) * (p->nFramesSweep+1) ); */ return p; @@ -109,7 +109,7 @@ void Ssw_SemManStop( Ssw_Sem_t * p ) Vec_PtrFree( p->vTargets ); Vec_PtrFree( p->vPatterns ); Vec_IntFree( p->vHistory ); - free( p ); + ABC_FREE( p ); } /**Function************************************************************* @@ -283,7 +283,7 @@ clk = clock(); Iter, Ssw_ClassesCand1Num(p->pMan->ppClasses), Ssw_ClassesClassNum(p->pMan->ppClasses), Aig_ManNodeNum(p->pMan->pFrames), Frames, (int)p->pMan->pMSat->pSat->stats.conflicts, p->nPatterns, p->pMan->nSatFailsReal? "f" : " " ); - PRT( "T", clock() - clk ); + ABC_PRT( "T", clock() - clk ); } Ssw_ManCleanup( p->pMan ); if ( fCheckTargets && Ssw_SemCheckTargets( p ) ) diff --git a/src/aig/ssw/sswSim.c b/src/aig/ssw/sswSim.c index a860199e..7a2f4664 100644 --- a/src/aig/ssw/sswSim.c +++ b/src/aig/ssw/sswSim.c @@ -437,7 +437,7 @@ int * Ssw_SmlCheckOutputSavePattern( Ssw_Sml_t * p, Aig_Obj_t * pObjPo ) // determine the best pattern BestPat = i * 32 + k; // fill in the counter-example data - pModel = ALLOC( int, Aig_ManPiNum(p->pAig)+1 ); + pModel = ABC_ALLOC( int, Aig_ManPiNum(p->pAig)+1 ); Aig_ManForEachPi( p->pAig, pObjPi, i ) { pModel[i] = Aig_InfoHasBit(Ssw_ObjSim(p, pObjPi->Id), BestPat); @@ -1074,7 +1074,7 @@ p->nSimRounds++; Ssw_Sml_t * Ssw_SmlStart( Aig_Man_t * pAig, int nPref, int nFrames, int nWordsFrame ) { Ssw_Sml_t * p; - p = (Ssw_Sml_t *)malloc( sizeof(Ssw_Sml_t) + sizeof(unsigned) * Aig_ManObjNumMax(pAig) * (nPref + nFrames) * nWordsFrame ); + p = (Ssw_Sml_t *)ABC_ALLOC( char, sizeof(Ssw_Sml_t) + sizeof(unsigned) * Aig_ManObjNumMax(pAig) * (nPref + nFrames) * nWordsFrame ); memset( p, 0, sizeof(Ssw_Sml_t) + sizeof(unsigned) * (nPref + nFrames) * nWordsFrame ); p->pAig = pAig; p->nPref = nPref; @@ -1114,7 +1114,7 @@ void Ssw_SmlClean( Ssw_Sml_t * p ) ***********************************************************************/ void Ssw_SmlStop( Ssw_Sml_t * p ) { - free( p ); + ABC_FREE( p ); } @@ -1244,7 +1244,7 @@ Ssw_Cex_t * Ssw_SmlAllocCounterExample( int nRegs, int nRealPis, int nFrames ) { Ssw_Cex_t * pCex; int nWords = Aig_BitWordNum( nRegs + nRealPis * nFrames ); - pCex = (Ssw_Cex_t *)malloc( sizeof(Ssw_Cex_t) + sizeof(unsigned) * nWords ); + pCex = (Ssw_Cex_t *)ABC_ALLOC( char, sizeof(Ssw_Cex_t) + sizeof(unsigned) * nWords ); memset( pCex, 0, sizeof(Ssw_Cex_t) + sizeof(unsigned) * nWords ); pCex->nRegs = nRegs; pCex->nPis = nRealPis; @@ -1265,7 +1265,7 @@ Ssw_Cex_t * Ssw_SmlAllocCounterExample( int nRegs, int nRealPis, int nFrames ) ***********************************************************************/ void Ssw_SmlFreeCounterExample( Ssw_Cex_t * pCex ) { - free( pCex ); + ABC_FREE( pCex ); } /**Function************************************************************* -- cgit v1.2.3