summaryrefslogtreecommitdiffstats
path: root/src/aig/ssw
diff options
context:
space:
mode:
Diffstat (limited to 'src/aig/ssw')
-rw-r--r--src/aig/ssw/ssw.h8
-rw-r--r--src/aig/ssw/sswAig.c4
-rw-r--r--src/aig/ssw/sswBmc.c4
-rw-r--r--src/aig/ssw/sswClass.c38
-rw-r--r--src/aig/ssw/sswCnf.c8
-rw-r--r--src/aig/ssw/sswCore.c6
-rw-r--r--src/aig/ssw/sswInt.h8
-rw-r--r--src/aig/ssw/sswIslands.c2
-rw-r--r--src/aig/ssw/sswMan.c34
-rw-r--r--src/aig/ssw/sswPairs.c16
-rw-r--r--src/aig/ssw/sswPart.c4
-rw-r--r--src/aig/ssw/sswSat.c4
-rw-r--r--src/aig/ssw/sswSemi.c10
-rw-r--r--src/aig/ssw/sswSim.c10
14 files changed, 78 insertions, 78 deletions
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*************************************************************
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-07 12:40:50 +0000