diff options
Diffstat (limited to 'src/sat/msat')
-rw-r--r-- | src/sat/msat/module.make | 2 | ||||
-rw-r--r-- | src/sat/msat/msat.h | 8 | ||||
-rw-r--r-- | src/sat/msat/msatClause.c | 4 | ||||
-rw-r--r-- | src/sat/msat/msatClauseVec.c | 10 | ||||
-rw-r--r-- | src/sat/msat/msatInt.h | 32 | ||||
-rw-r--r-- | src/sat/msat/msatMem.c | 64 | ||||
-rw-r--r-- | src/sat/msat/msatOrderH.c | 4 | ||||
-rw-r--r-- | src/sat/msat/msatQueue.c | 8 | ||||
-rw-r--r-- | src/sat/msat/msatRead.c | 4 | ||||
-rw-r--r-- | src/sat/msat/msatSolverApi.c | 70 | ||||
-rw-r--r-- | src/sat/msat/msatSolverCore.c | 6 | ||||
-rw-r--r-- | src/sat/msat/msatVec.c | 22 |
12 files changed, 108 insertions, 126 deletions
diff --git a/src/sat/msat/module.make b/src/sat/msat/module.make index 0dadfbe1..33133963 100644 --- a/src/sat/msat/module.make +++ b/src/sat/msat/module.make @@ -2,7 +2,7 @@ SRC += src/sat/msat/msatActivity.c \ src/sat/msat/msatClause.c \ src/sat/msat/msatClauseVec.c \ src/sat/msat/msatMem.c \ - src/sat/msat/msatOrderJ.c \ + src/sat/msat/msatOrderH.c \ src/sat/msat/msatQueue.c \ src/sat/msat/msatRead.c \ src/sat/msat/msatSolverApi.c \ diff --git a/src/sat/msat/msat.h b/src/sat/msat/msat.h index 53353ba6..2b28700c 100644 --- a/src/sat/msat/msat.h +++ b/src/sat/msat/msat.h @@ -21,10 +21,6 @@ #ifndef __MSAT_H__ #define __MSAT_H__ -#ifdef __cplusplus -extern "C" { -#endif - //////////////////////////////////////////////////////////////////////// /// INCLUDES /// //////////////////////////////////////////////////////////////////////// @@ -33,6 +29,10 @@ extern "C" { /// PARAMETERS /// //////////////////////////////////////////////////////////////////////// +#ifdef __cplusplus +extern "C" { +#endif + //////////////////////////////////////////////////////////////////////// /// STRUCTURE DEFINITIONS /// //////////////////////////////////////////////////////////////////////// diff --git a/src/sat/msat/msatClause.c b/src/sat/msat/msatClause.c index 2ba8cd32..ca698866 100644 --- a/src/sat/msat/msatClause.c +++ b/src/sat/msat/msatClause.c @@ -152,7 +152,7 @@ bool Msat_ClauseCreate( Msat_Solver_t * p, Msat_IntVec_t * vLits, bool fLearned, // nBytes = sizeof(unsigned)*(nLits + 1 + (int)fLearned); nBytes = sizeof(unsigned)*(nLits + 2 + (int)fLearned); #ifdef USE_SYSTEM_MEMORY_MANAGEMENT - pC = (Msat_Clause_t *)ALLOC( char, nBytes ); + pC = (Msat_Clause_t *)ABC_ALLOC( char, nBytes ); #else pC = (Msat_Clause_t *)Msat_MmStepEntryFetch( Msat_SolverReadMem(p), nBytes ); #endif @@ -231,7 +231,7 @@ void Msat_ClauseFree( Msat_Solver_t * p, Msat_Clause_t * pC, bool fRemoveWatched } #ifdef USE_SYSTEM_MEMORY_MANAGEMENT - free( pC ); + ABC_FREE( pC ); #else Msat_MmStepEntryRecycle( Msat_SolverReadMem(p), (char *)pC, pC->nSizeAlloc ); #endif diff --git a/src/sat/msat/msatClauseVec.c b/src/sat/msat/msatClauseVec.c index 04691cf2..f29de389 100644 --- a/src/sat/msat/msatClauseVec.c +++ b/src/sat/msat/msatClauseVec.c @@ -42,12 +42,12 @@ Msat_ClauseVec_t * Msat_ClauseVecAlloc( int nCap ) { Msat_ClauseVec_t * p; - p = ALLOC( Msat_ClauseVec_t, 1 ); + p = ABC_ALLOC( Msat_ClauseVec_t, 1 ); if ( nCap > 0 && nCap < 16 ) nCap = 16; p->nSize = 0; p->nCap = nCap; - p->pArray = p->nCap? ALLOC( Msat_Clause_t *, p->nCap ) : NULL; + p->pArray = p->nCap? ABC_ALLOC( Msat_Clause_t *, p->nCap ) : NULL; return p; } @@ -64,8 +64,8 @@ Msat_ClauseVec_t * Msat_ClauseVecAlloc( int nCap ) ***********************************************************************/ void Msat_ClauseVecFree( Msat_ClauseVec_t * p ) { - FREE( p->pArray ); - FREE( p ); + ABC_FREE( p->pArray ); + ABC_FREE( p ); } /**Function************************************************************* @@ -115,7 +115,7 @@ void Msat_ClauseVecGrow( Msat_ClauseVec_t * p, int nCapMin ) { if ( p->nCap >= nCapMin ) return; - p->pArray = REALLOC( Msat_Clause_t *, p->pArray, nCapMin ); + p->pArray = ABC_REALLOC( Msat_Clause_t *, p->pArray, nCapMin ); p->nCap = nCapMin; } diff --git a/src/sat/msat/msatInt.h b/src/sat/msat/msatInt.h index 2ff0e695..b6759a0f 100644 --- a/src/sat/msat/msatInt.h +++ b/src/sat/msat/msatInt.h @@ -31,6 +31,7 @@ #include <assert.h> #include <time.h> #include <math.h> +#include "abc_global.h" #include "msat.h" //////////////////////////////////////////////////////////////////////// @@ -41,25 +42,6 @@ /// STRUCTURE DEFINITIONS /// //////////////////////////////////////////////////////////////////////// -#ifdef _MSC_VER -typedef __int64 int64; -#else -typedef long long int64; -#endif - -// outputs the runtime in seconds -#define PRT(a,t) \ - printf( "%s = ", (a) ); printf( "%6.2f sec\n", (float)(t)/(float)(CLOCKS_PER_SEC) ) - -// memory management macros -#define ALLOC(type, num) \ - ((type *) malloc(sizeof(type) * (num))) -#define REALLOC(type, obj, num) \ - ((obj) ? ((type *) realloc((char *)(obj), sizeof(type) * (num))) : \ - ((type *) malloc(sizeof(type) * (num)))) -#define FREE(obj) \ - ((obj) ? (free((char *)(obj)), (obj) = 0) : 0) - // By default, custom memory management is used // which guarantees constant time allocation/deallocation // for SAT clauses and other frequently modified objects. @@ -92,12 +74,12 @@ typedef int Msat_Var_t; typedef struct Msat_SolverStats_t_ Msat_SolverStats_t; struct Msat_SolverStats_t_ { - int64 nStarts; // the number of restarts - int64 nDecisions; // the number of decisions - int64 nPropagations; // the number of implications - int64 nInspects; // the number of times clauses are vising while watching them - int64 nConflicts; // the number of conflicts - int64 nSuccesses; // the number of sat assignments found + ABC_INT64_T nStarts; // the number of restarts + ABC_INT64_T nDecisions; // the number of decisions + ABC_INT64_T nPropagations; // the number of implications + ABC_INT64_T nInspects; // the number of times clauses are vising while watching them + ABC_INT64_T nConflicts; // the number of conflicts + ABC_INT64_T nSuccesses; // the number of sat assignments found }; typedef struct Msat_SearchParams_t_ Msat_SearchParams_t; diff --git a/src/sat/msat/msatMem.c b/src/sat/msat/msatMem.c index 30bf4a96..439661f4 100644 --- a/src/sat/msat/msatMem.c +++ b/src/sat/msat/msatMem.c @@ -31,7 +31,7 @@ struct Msat_MmFixed_t_ int nEntriesAlloc; // the total number of entries allocated int nEntriesUsed; // the number of entries in use int nEntriesMax; // the max number of entries in use - char * pEntriesFree; // the linked list of free entries + char * pEntriesFree; // the linked list of ABC_FREE entries // this is where the memory is stored int nChunkSize; // the size of one chunk @@ -48,8 +48,8 @@ struct Msat_MmFlex_t_ { // information about individual entries int nEntriesUsed; // the number of entries allocated - char * pCurrent; // the current pointer to free memory - char * pEnd; // the first entry outside the free memory + char * pCurrent; // the current pointer to ABC_FREE memory + char * pEnd; // the first entry outside the ABC_FREE memory // this is where the memory is stored int nChunkSize; // the size of one chunk @@ -91,7 +91,7 @@ Msat_MmFixed_t * Msat_MmFixedStart( int nEntrySize ) { Msat_MmFixed_t * p; - p = ALLOC( Msat_MmFixed_t, 1 ); + p = ABC_ALLOC( Msat_MmFixed_t, 1 ); memset( p, 0, sizeof(Msat_MmFixed_t) ); p->nEntrySize = nEntrySize; @@ -108,7 +108,7 @@ Msat_MmFixed_t * Msat_MmFixedStart( int nEntrySize ) p->nChunksAlloc = 64; p->nChunks = 0; - p->pChunks = ALLOC( char *, p->nChunksAlloc ); + p->pChunks = ABC_ALLOC( char *, p->nChunksAlloc ); p->nMemoryUsed = 0; p->nMemoryAlloc = 0; @@ -139,9 +139,9 @@ void Msat_MmFixedStop( Msat_MmFixed_t * p, int fVerbose ) p->nEntriesUsed, p->nEntriesMax, p->nEntrySize * p->nEntriesUsed, p->nMemoryAlloc ); } for ( i = 0; i < p->nChunks; i++ ) - free( p->pChunks[i] ); - free( p->pChunks ); - free( p ); + ABC_FREE( p->pChunks[i] ); + ABC_FREE( p->pChunks ); + ABC_FREE( p ); } /**Function************************************************************* @@ -160,16 +160,16 @@ char * Msat_MmFixedEntryFetch( Msat_MmFixed_t * p ) char * pTemp; int i; - // check if there are still free entries + // check if there are still ABC_FREE entries if ( p->nEntriesUsed == p->nEntriesAlloc ) { // need to allocate more entries assert( p->pEntriesFree == NULL ); if ( p->nChunks == p->nChunksAlloc ) { p->nChunksAlloc *= 2; - p->pChunks = REALLOC( char *, p->pChunks, p->nChunksAlloc ); + p->pChunks = ABC_REALLOC( char *, p->pChunks, p->nChunksAlloc ); } - p->pEntriesFree = ALLOC( char, p->nEntrySize * p->nChunkSize ); + p->pEntriesFree = ABC_ALLOC( char, p->nEntrySize * p->nChunkSize ); p->nMemoryAlloc += p->nEntrySize * p->nChunkSize; // transform these entries into a linked list pTemp = p->pEntriesFree; @@ -189,7 +189,7 @@ char * Msat_MmFixedEntryFetch( Msat_MmFixed_t * p ) p->nEntriesUsed++; if ( p->nEntriesMax < p->nEntriesUsed ) p->nEntriesMax = p->nEntriesUsed; - // return the first entry in the free entry list + // return the first entry in the ABC_FREE entry list pTemp = p->pEntriesFree; p->pEntriesFree = *((char **)pTemp); return pTemp; @@ -210,7 +210,7 @@ void Msat_MmFixedEntryRecycle( Msat_MmFixed_t * p, char * pEntry ) { // decrement the counter of used entries p->nEntriesUsed--; - // add the entry to the linked list of free entries + // add the entry to the linked list of ABC_FREE entries *((char **)pEntry) = p->pEntriesFree; p->pEntriesFree = pEntry; } @@ -233,7 +233,7 @@ void Msat_MmFixedRestart( Msat_MmFixed_t * p ) // deallocate all chunks except the first one for ( i = 1; i < p->nChunks; i++ ) - free( p->pChunks[i] ); + ABC_FREE( p->pChunks[i] ); p->nChunks = 1; // transform these entries into a linked list pTemp = p->pChunks[0]; @@ -244,7 +244,7 @@ void Msat_MmFixedRestart( Msat_MmFixed_t * p ) } // set the last link *((char **)pTemp) = NULL; - // set the free entry list + // set the ABC_FREE entry list p->pEntriesFree = p->pChunks[0]; // set the correct statistics p->nMemoryAlloc = p->nEntrySize * p->nChunkSize; @@ -286,7 +286,7 @@ Msat_MmFlex_t * Msat_MmFlexStart() { Msat_MmFlex_t * p; - p = ALLOC( Msat_MmFlex_t, 1 ); + p = ABC_ALLOC( Msat_MmFlex_t, 1 ); memset( p, 0, sizeof(Msat_MmFlex_t) ); p->nEntriesUsed = 0; @@ -296,7 +296,7 @@ Msat_MmFlex_t * Msat_MmFlexStart() p->nChunkSize = (1 << 12); p->nChunksAlloc = 64; p->nChunks = 0; - p->pChunks = ALLOC( char *, p->nChunksAlloc ); + p->pChunks = ABC_ALLOC( char *, p->nChunksAlloc ); p->nMemoryUsed = 0; p->nMemoryAlloc = 0; @@ -327,9 +327,9 @@ void Msat_MmFlexStop( Msat_MmFlex_t * p, int fVerbose ) p->nEntriesUsed, p->nMemoryUsed, p->nMemoryAlloc ); } for ( i = 0; i < p->nChunks; i++ ) - free( p->pChunks[i] ); - free( p->pChunks ); - free( p ); + ABC_FREE( p->pChunks[i] ); + ABC_FREE( p->pChunks ); + ABC_FREE( p ); } /**Function************************************************************* @@ -346,13 +346,13 @@ void Msat_MmFlexStop( Msat_MmFlex_t * p, int fVerbose ) char * Msat_MmFlexEntryFetch( Msat_MmFlex_t * p, int nBytes ) { char * pTemp; - // check if there are still free entries + // check if there are still ABC_FREE entries if ( p->pCurrent == NULL || p->pCurrent + nBytes > p->pEnd ) { // need to allocate more entries if ( p->nChunks == p->nChunksAlloc ) { p->nChunksAlloc *= 2; - p->pChunks = REALLOC( char *, p->pChunks, p->nChunksAlloc ); + p->pChunks = ABC_REALLOC( char *, p->pChunks, p->nChunksAlloc ); } if ( nBytes > p->nChunkSize ) { @@ -360,7 +360,7 @@ char * Msat_MmFlexEntryFetch( Msat_MmFlex_t * p, int nBytes ) // (ideally, this should never happen) p->nChunkSize = 2 * nBytes; } - p->pCurrent = ALLOC( char, p->nChunkSize ); + p->pCurrent = ABC_ALLOC( char, p->nChunkSize ); p->pEnd = p->pCurrent + p->nChunkSize; p->nMemoryAlloc += p->nChunkSize; // add the chunk to the chunk storage @@ -410,7 +410,7 @@ int Msat_MmFlexReadMemUsage( Msat_MmFlex_t * p ) are employed internally. Calling this procedure with nSteps equal to 10 results in 10 hierarchically arranged internal memory managers, which can allocate up to 4096 (1Kb) entries. Requests for larger - entries are handed over to malloc() and then free()ed.] + entries are handed over to malloc() and then ABC_FREE()ed.] SideEffects [] @@ -421,15 +421,15 @@ Msat_MmStep_t * Msat_MmStepStart( int nSteps ) { Msat_MmStep_t * p; int i, k; - p = ALLOC( Msat_MmStep_t, 1 ); + p = ABC_ALLOC( Msat_MmStep_t, 1 ); p->nMems = nSteps; // start the fixed memory managers - p->pMems = ALLOC( Msat_MmFixed_t *, p->nMems ); + p->pMems = ABC_ALLOC( Msat_MmFixed_t *, p->nMems ); for ( i = 0; i < p->nMems; i++ ) p->pMems[i] = Msat_MmFixedStart( (8<<i) ); // set up the mapping of the required memory size into the corresponding manager p->nMapSize = (4<<p->nMems); - p->pMap = ALLOC( Msat_MmFixed_t *, p->nMapSize+1 ); + p->pMap = ABC_ALLOC( Msat_MmFixed_t *, p->nMapSize+1 ); p->pMap[0] = NULL; for ( k = 1; k <= 4; k++ ) p->pMap[k] = p->pMems[0]; @@ -457,9 +457,9 @@ void Msat_MmStepStop( Msat_MmStep_t * p, int fVerbose ) int i; for ( i = 0; i < p->nMems; i++ ) Msat_MmFixedStop( p->pMems[i], fVerbose ); - free( p->pMems ); - free( p->pMap ); - free( p ); + ABC_FREE( p->pMems ); + ABC_FREE( p->pMap ); + ABC_FREE( p ); } /**Function************************************************************* @@ -480,7 +480,7 @@ char * Msat_MmStepEntryFetch( Msat_MmStep_t * p, int nBytes ) if ( nBytes > p->nMapSize ) { // printf( "Allocating %d bytes.\n", nBytes ); - return ALLOC( char, nBytes ); + return ABC_ALLOC( char, nBytes ); } return Msat_MmFixedEntryFetch( p->pMap[nBytes] ); } @@ -503,7 +503,7 @@ void Msat_MmStepEntryRecycle( Msat_MmStep_t * p, char * pEntry, int nBytes ) return; if ( nBytes > p->nMapSize ) { - free( pEntry ); + ABC_FREE( pEntry ); return; } Msat_MmFixedEntryRecycle( p->pMap[nBytes], pEntry ); diff --git a/src/sat/msat/msatOrderH.c b/src/sat/msat/msatOrderH.c index 956e7fc6..7d8484d5 100644 --- a/src/sat/msat/msatOrderH.c +++ b/src/sat/msat/msatOrderH.c @@ -75,7 +75,7 @@ extern int timeSelect; Msat_Order_t * Msat_OrderAlloc( Msat_Solver_t * pSat ) { Msat_Order_t * p; - p = ALLOC( Msat_Order_t, 1 ); + p = ABC_ALLOC( Msat_Order_t, 1 ); memset( p, 0, sizeof(Msat_Order_t) ); p->pSat = pSat; p->vIndex = Msat_IntVecAlloc( 0 ); @@ -161,7 +161,7 @@ void Msat_OrderFree( Msat_Order_t * p ) { Msat_IntVecFree( p->vHeap ); Msat_IntVecFree( p->vIndex ); - free( p ); + ABC_FREE( p ); } diff --git a/src/sat/msat/msatQueue.c b/src/sat/msat/msatQueue.c index 5938e042..0bcaf6b2 100644 --- a/src/sat/msat/msatQueue.c +++ b/src/sat/msat/msatQueue.c @@ -50,10 +50,10 @@ struct Msat_Queue_t_ Msat_Queue_t * Msat_QueueAlloc( int nVars ) { Msat_Queue_t * p; - p = ALLOC( Msat_Queue_t, 1 ); + p = ABC_ALLOC( Msat_Queue_t, 1 ); memset( p, 0, sizeof(Msat_Queue_t) ); p->nVars = nVars; - p->pVars = ALLOC( int, nVars ); + p->pVars = ABC_ALLOC( int, nVars ); return p; } @@ -70,8 +70,8 @@ Msat_Queue_t * Msat_QueueAlloc( int nVars ) ***********************************************************************/ void Msat_QueueFree( Msat_Queue_t * p ) { - free( p->pVars ); - free( p ); + ABC_FREE( p->pVars ); + ABC_FREE( p ); } /**Function************************************************************* diff --git a/src/sat/msat/msatRead.c b/src/sat/msat/msatRead.c index 20453fed..ba33278c 100644 --- a/src/sat/msat/msatRead.c +++ b/src/sat/msat/msatRead.c @@ -51,7 +51,7 @@ char * Msat_FileRead( FILE * pFile ) // move the file current reading position to the beginning rewind( pFile ); // load the contents of the file into memory - pBuffer = ALLOC( char, nFileSize + 3 ); + pBuffer = ABC_ALLOC( char, nFileSize + 3 ); fread( pBuffer, nFileSize, 1, pFile ); // terminate the string with '\0' pBuffer[ nFileSize + 0] = '\n'; @@ -257,7 +257,7 @@ bool Msat_SolverParseDimacs( FILE * pFile, Msat_Solver_t ** p, int fVerbose ) bool Value; pText = Msat_FileRead( pFile ); Value = Msat_ReadDimacs( pText, p, fVerbose ); - free( pText ); + ABC_FREE( pText ); return Value; } diff --git a/src/sat/msat/msatSolverApi.c b/src/sat/msat/msatSolverApi.c index ee3507a6..dece390c 100644 --- a/src/sat/msat/msatSolverApi.c +++ b/src/sat/msat/msatSolverApi.c @@ -159,7 +159,7 @@ Msat_Solver_t * Msat_SolverAlloc( int nVarsAlloc, assert(sizeof(Msat_Lit_t) == sizeof(unsigned)); assert(sizeof(float) == sizeof(unsigned)); - p = ALLOC( Msat_Solver_t, 1 ); + p = ABC_ALLOC( Msat_Solver_t, 1 ); memset( p, 0, sizeof(Msat_Solver_t) ); p->nVarsAlloc = nVarsAlloc; @@ -174,31 +174,31 @@ Msat_Solver_t * Msat_SolverAlloc( int nVarsAlloc, p->dVarInc = dVarInc; p->dVarDecay = dVarDecay; - p->pdActivity = ALLOC( double, p->nVarsAlloc ); - p->pFactors = ALLOC( float, p->nVarsAlloc ); + p->pdActivity = ABC_ALLOC( double, p->nVarsAlloc ); + p->pFactors = ABC_ALLOC( float, p->nVarsAlloc ); for ( i = 0; i < p->nVarsAlloc; i++ ) { p->pdActivity[i] = 0.0; p->pFactors[i] = 1.0; } - p->pAssigns = ALLOC( int, p->nVarsAlloc ); - p->pModel = ALLOC( int, p->nVarsAlloc ); + p->pAssigns = ABC_ALLOC( int, p->nVarsAlloc ); + p->pModel = ABC_ALLOC( int, p->nVarsAlloc ); for ( i = 0; i < p->nVarsAlloc; i++ ) p->pAssigns[i] = MSAT_VAR_UNASSIGNED; // p->pOrder = Msat_OrderAlloc( p->pAssigns, p->pdActivity, p->nVarsAlloc ); p->pOrder = Msat_OrderAlloc( p ); - p->pvWatched = ALLOC( Msat_ClauseVec_t *, 2 * p->nVarsAlloc ); + p->pvWatched = ABC_ALLOC( Msat_ClauseVec_t *, 2 * p->nVarsAlloc ); for ( i = 0; i < 2 * p->nVarsAlloc; i++ ) p->pvWatched[i] = Msat_ClauseVecAlloc( 16 ); p->pQueue = Msat_QueueAlloc( p->nVarsAlloc ); p->vTrail = Msat_IntVecAlloc( p->nVarsAlloc ); p->vTrailLim = Msat_IntVecAlloc( p->nVarsAlloc ); - p->pReasons = ALLOC( Msat_Clause_t *, p->nVarsAlloc ); + p->pReasons = ABC_ALLOC( Msat_Clause_t *, p->nVarsAlloc ); memset( p->pReasons, 0, sizeof(Msat_Clause_t *) * p->nVarsAlloc ); - p->pLevel = ALLOC( int, p->nVarsAlloc ); + p->pLevel = ABC_ALLOC( int, p->nVarsAlloc ); for ( i = 0; i < p->nVarsAlloc; i++ ) p->pLevel[i] = -1; p->dRandSeed = 91648253; @@ -215,7 +215,7 @@ Msat_Solver_t * Msat_SolverAlloc( int nVarsAlloc, Msat_IntVecFill( p->vVarsUsed, p->nVarsAlloc, 1 ); - p->pSeen = ALLOC( int, p->nVarsAlloc ); + p->pSeen = ABC_ALLOC( int, p->nVarsAlloc ); memset( p->pSeen, 0, sizeof(int) * p->nVarsAlloc ); p->nSeenId = 1; p->vReason = Msat_IntVecAlloc( p->nVarsAlloc ); @@ -243,38 +243,38 @@ void Msat_SolverResize( Msat_Solver_t * p, int nVarsAlloc ) nVarsAllocOld = p->nVarsAlloc; p->nVarsAlloc = nVarsAlloc; - p->pdActivity = REALLOC( double, p->pdActivity, p->nVarsAlloc ); - p->pFactors = REALLOC( float, p->pFactors, p->nVarsAlloc ); + p->pdActivity = ABC_REALLOC( double, p->pdActivity, p->nVarsAlloc ); + p->pFactors = ABC_REALLOC( float, p->pFactors, p->nVarsAlloc ); for ( i = nVarsAllocOld; i < p->nVarsAlloc; i++ ) { p->pdActivity[i] = 0.0; p->pFactors[i] = 1.0; } - p->pAssigns = REALLOC( int, p->pAssigns, p->nVarsAlloc ); - p->pModel = REALLOC( int, p->pModel, p->nVarsAlloc ); + p->pAssigns = ABC_REALLOC( int, p->pAssigns, p->nVarsAlloc ); + p->pModel = ABC_REALLOC( int, p->pModel, p->nVarsAlloc ); for ( i = nVarsAllocOld; i < p->nVarsAlloc; i++ ) p->pAssigns[i] = MSAT_VAR_UNASSIGNED; // Msat_OrderRealloc( p->pOrder, p->pAssigns, p->pdActivity, p->nVarsAlloc ); Msat_OrderSetBounds( p->pOrder, p->nVarsAlloc ); - p->pvWatched = REALLOC( Msat_ClauseVec_t *, p->pvWatched, 2 * p->nVarsAlloc ); + p->pvWatched = ABC_REALLOC( Msat_ClauseVec_t *, p->pvWatched, 2 * p->nVarsAlloc ); for ( i = 2 * nVarsAllocOld; i < 2 * p->nVarsAlloc; i++ ) p->pvWatched[i] = Msat_ClauseVecAlloc( 16 ); Msat_QueueFree( p->pQueue ); p->pQueue = Msat_QueueAlloc( p->nVarsAlloc ); - p->pReasons = REALLOC( Msat_Clause_t *, p->pReasons, p->nVarsAlloc ); - p->pLevel = REALLOC( int, p->pLevel, p->nVarsAlloc ); + p->pReasons = ABC_REALLOC( Msat_Clause_t *, p->pReasons, p->nVarsAlloc ); + p->pLevel = ABC_REALLOC( int, p->pLevel, p->nVarsAlloc ); for ( i = nVarsAllocOld; i < p->nVarsAlloc; i++ ) { p->pReasons[i] = NULL; p->pLevel[i] = -1; } - p->pSeen = REALLOC( int, p->pSeen, p->nVarsAlloc ); + p->pSeen = ABC_REALLOC( int, p->pSeen, p->nVarsAlloc ); for ( i = nVarsAllocOld; i < p->nVarsAlloc; i++ ) p->pSeen[i] = 0; @@ -304,7 +304,7 @@ void Msat_SolverResize( Msat_Solver_t * p, int nVarsAlloc ) void Msat_SolverClean( Msat_Solver_t * p, int nVars ) { int i; - // free the clauses + // ABC_FREE the clauses int nClauses; Msat_Clause_t ** pClauses; @@ -326,7 +326,7 @@ void Msat_SolverClean( Msat_Solver_t * p, int nVars ) // Msat_ClauseVecFree( p->vLearned ); Msat_ClauseVecClear( p->vLearned ); -// FREE( p->pdActivity ); +// ABC_FREE( p->pdActivity ); for ( i = 0; i < p->nVars; i++ ) p->pdActivity[i] = 0; @@ -337,20 +337,20 @@ void Msat_SolverClean( Msat_Solver_t * p, int nVars ) for ( i = 0; i < 2 * p->nVars; i++ ) // Msat_ClauseVecFree( p->pvWatched[i] ); Msat_ClauseVecClear( p->pvWatched[i] ); -// FREE( p->pvWatched ); +// ABC_FREE( p->pvWatched ); // Msat_QueueFree( p->pQueue ); Msat_QueueClear( p->pQueue ); -// FREE( p->pAssigns ); +// ABC_FREE( p->pAssigns ); for ( i = 0; i < p->nVars; i++ ) p->pAssigns[i] = MSAT_VAR_UNASSIGNED; // Msat_IntVecFree( p->vTrail ); Msat_IntVecClear( p->vTrail ); // Msat_IntVecFree( p->vTrailLim ); Msat_IntVecClear( p->vTrailLim ); -// FREE( p->pReasons ); +// ABC_FREE( p->pReasons ); memset( p->pReasons, 0, sizeof(Msat_Clause_t *) * p->nVars ); -// FREE( p->pLevel ); +// ABC_FREE( p->pLevel ); for ( i = 0; i < p->nVars; i++ ) p->pLevel[i] = -1; // Msat_IntVecFree( p->pModel ); @@ -358,7 +358,7 @@ void Msat_SolverClean( Msat_Solver_t * p, int nVars ) p->dRandSeed = 91648253; p->dProgress = 0.0; -// FREE( p->pSeen ); +// ABC_FREE( p->pSeen ); memset( p->pSeen, 0, sizeof(int) * p->nVars ); p->nSeenId = 1; // Msat_IntVecFree( p->vReason ); @@ -366,7 +366,7 @@ void Msat_SolverClean( Msat_Solver_t * p, int nVars ) // Msat_IntVecFree( p->vTemp ); Msat_IntVecClear( p->vTemp ); // printf(" The number of clauses remaining = %d (%d).\n", p->nClausesAlloc, p->nClausesAllocL ); -// FREE( p ); +// ABC_FREE( p ); } /**Function************************************************************* @@ -384,7 +384,7 @@ void Msat_SolverFree( Msat_Solver_t * p ) { int i; - // free the clauses + // ABC_FREE the clauses int nClauses; Msat_Clause_t ** pClauses; //printf( "clauses = %d. learned = %d.\n", Msat_ClauseVecReadSize( p->vClauses ), @@ -402,21 +402,21 @@ void Msat_SolverFree( Msat_Solver_t * p ) Msat_ClauseFree( p, pClauses[i], 0 ); Msat_ClauseVecFree( p->vLearned ); - FREE( p->pdActivity ); - FREE( p->pFactors ); + ABC_FREE( p->pdActivity ); + ABC_FREE( p->pFactors ); Msat_OrderFree( p->pOrder ); for ( i = 0; i < 2 * p->nVarsAlloc; i++ ) Msat_ClauseVecFree( p->pvWatched[i] ); - FREE( p->pvWatched ); + ABC_FREE( p->pvWatched ); Msat_QueueFree( p->pQueue ); - FREE( p->pAssigns ); - FREE( p->pModel ); + ABC_FREE( p->pAssigns ); + ABC_FREE( p->pModel ); Msat_IntVecFree( p->vTrail ); Msat_IntVecFree( p->vTrailLim ); - FREE( p->pReasons ); - FREE( p->pLevel ); + ABC_FREE( p->pReasons ); + ABC_FREE( p->pLevel ); Msat_MmStepStop( p->pMem, 0 ); @@ -428,10 +428,10 @@ void Msat_SolverFree( Msat_Solver_t * p ) Msat_IntVecFree( p->vConeVars ); Msat_IntVecFree( p->vVarsUsed ); - FREE( p->pSeen ); + ABC_FREE( p->pSeen ); Msat_IntVecFree( p->vReason ); Msat_IntVecFree( p->vTemp ); - FREE( p ); + ABC_FREE( p ); } /**Function************************************************************* diff --git a/src/sat/msat/msatSolverCore.c b/src/sat/msat/msatSolverCore.c index e86ab511..0462f11b 100644 --- a/src/sat/msat/msatSolverCore.c +++ b/src/sat/msat/msatSolverCore.c @@ -139,7 +139,7 @@ bool Msat_SolverSolve( Msat_Solver_t * p, Msat_IntVec_t * vAssumps, int nBackTra Msat_Type_t Status; int timeStart = clock(); -// p->pFreq = ALLOC( int, p->nVarsAlloc ); +// p->pFreq = ABC_ALLOC( int, p->nVarsAlloc ); // memset( p->pFreq, 0, sizeof(int) * p->nVarsAlloc ); if ( vAssumps ) @@ -184,7 +184,7 @@ bool Msat_SolverSolve( Msat_Solver_t * p, Msat_IntVec_t * vAssumps, int nBackTra Msat_SolverCancelUntil( p, 0 ); p->nBackTracks = (int)p->Stats.nConflicts - p->nBackTracks; /* - PRT( "True solver runtime", clock() - timeStart ); + ABC_PRT( "True solver runtime", clock() - timeStart ); // print the statistics { int i, Counter = 0; @@ -197,7 +197,7 @@ bool Msat_SolverSolve( Msat_Solver_t * p, Msat_IntVec_t * vAssumps, int nBackTra if ( Counter ) printf( "\n" ); printf( "Total = %d. Used = %d. Decisions = %d. Imps = %d. Conflicts = %d. ", p->nVars, Counter, (int)p->Stats.nDecisions, (int)p->Stats.nPropagations, (int)p->Stats.nConflicts ); - PRT( "Time", clock() - timeStart ); + ABC_PRT( "Time", clock() - timeStart ); } */ return Status; diff --git a/src/sat/msat/msatVec.c b/src/sat/msat/msatVec.c index 36ad55ba..3716dbf7 100644 --- a/src/sat/msat/msatVec.c +++ b/src/sat/msat/msatVec.c @@ -45,12 +45,12 @@ static int Msat_IntVecSortCompare2( int * pp1, int * pp2 ); Msat_IntVec_t * Msat_IntVecAlloc( int nCap ) { Msat_IntVec_t * p; - p = ALLOC( Msat_IntVec_t, 1 ); + p = ABC_ALLOC( Msat_IntVec_t, 1 ); if ( nCap > 0 && nCap < 16 ) nCap = 16; p->nSize = 0; p->nCap = nCap; - p->pArray = p->nCap? ALLOC( int, p->nCap ) : NULL; + p->pArray = p->nCap? ABC_ALLOC( int, p->nCap ) : NULL; return p; } @@ -68,7 +68,7 @@ Msat_IntVec_t * Msat_IntVecAlloc( int nCap ) Msat_IntVec_t * Msat_IntVecAllocArray( int * pArray, int nSize ) { Msat_IntVec_t * p; - p = ALLOC( Msat_IntVec_t, 1 ); + p = ABC_ALLOC( Msat_IntVec_t, 1 ); p->nSize = nSize; p->nCap = nSize; p->pArray = pArray; @@ -89,10 +89,10 @@ Msat_IntVec_t * Msat_IntVecAllocArray( int * pArray, int nSize ) Msat_IntVec_t * Msat_IntVecAllocArrayCopy( int * pArray, int nSize ) { Msat_IntVec_t * p; - p = ALLOC( Msat_IntVec_t, 1 ); + p = ABC_ALLOC( Msat_IntVec_t, 1 ); p->nSize = nSize; p->nCap = nSize; - p->pArray = ALLOC( int, nSize ); + p->pArray = ABC_ALLOC( int, nSize ); memcpy( p->pArray, pArray, sizeof(int) * nSize ); return p; } @@ -111,10 +111,10 @@ Msat_IntVec_t * Msat_IntVecAllocArrayCopy( int * pArray, int nSize ) Msat_IntVec_t * Msat_IntVecDup( Msat_IntVec_t * pVec ) { Msat_IntVec_t * p; - p = ALLOC( Msat_IntVec_t, 1 ); + p = ABC_ALLOC( Msat_IntVec_t, 1 ); p->nSize = pVec->nSize; p->nCap = pVec->nCap; - p->pArray = p->nCap? ALLOC( int, p->nCap ) : NULL; + p->pArray = p->nCap? ABC_ALLOC( int, p->nCap ) : NULL; memcpy( p->pArray, pVec->pArray, sizeof(int) * pVec->nSize ); return p; } @@ -133,7 +133,7 @@ Msat_IntVec_t * Msat_IntVecDup( Msat_IntVec_t * pVec ) Msat_IntVec_t * Msat_IntVecDupArray( Msat_IntVec_t * pVec ) { Msat_IntVec_t * p; - p = ALLOC( Msat_IntVec_t, 1 ); + p = ABC_ALLOC( Msat_IntVec_t, 1 ); p->nSize = pVec->nSize; p->nCap = pVec->nCap; p->pArray = pVec->pArray; @@ -156,8 +156,8 @@ Msat_IntVec_t * Msat_IntVecDupArray( Msat_IntVec_t * pVec ) ***********************************************************************/ void Msat_IntVecFree( Msat_IntVec_t * p ) { - FREE( p->pArray ); - FREE( p ); + ABC_FREE( p->pArray ); + ABC_FREE( p ); } /**Function************************************************************* @@ -297,7 +297,7 @@ void Msat_IntVecGrow( Msat_IntVec_t * p, int nCapMin ) { if ( p->nCap >= nCapMin ) return; - p->pArray = REALLOC( int, p->pArray, nCapMin ); + p->pArray = ABC_REALLOC( int, p->pArray, nCapMin ); p->nCap = nCapMin; } |