From 0871bffae307e0553e0c5186336189e8b55cf6a6 Mon Sep 17 00:00:00 2001
From: Alan Mishchenko <alanmi@berkeley.edu>
Date: Sun, 15 Feb 2009 08:01:00 -0800
Subject: Version abc90215
---
src/sat/proof/pr.c | 61 ++++++++++++++++++++++++++----------------------------
src/sat/proof/pr.h | 8 +++----
2 files changed, 33 insertions(+), 36 deletions(-)
(limited to 'src/sat/proof')
diff --git a/src/sat/proof/pr.c b/src/sat/proof/pr.c
index 2d1ab2d1..a951071a 100644
--- a/src/sat/proof/pr.c
+++ b/src/sat/proof/pr.c
@@ -24,6 +24,7 @@
#include <assert.h>
#include <time.h>
//#include "vec.h"
+#include "abc_global.h"
#include "pr.h"
////////////////////////////////////////////////////////////////////////
@@ -91,10 +92,6 @@ struct Pr_Man_t_
int timeTotal;
};
-#ifndef PRT
-#define PRT(a,t) printf("%s = ", (a)); printf("%6.2f sec\n", (float)(t)/(float)(CLOCKS_PER_SEC))
-#endif
-
// variable assignments
static const lit LIT_UNDEF = 0xffffffff;
@@ -143,7 +140,7 @@ Pr_Man_t * Pr_ManAlloc( int nVarsAlloc )
{
Pr_Man_t * p;
// allocate the manager
- p = (Pr_Man_t *)malloc( sizeof(Pr_Man_t) );
+ p = (Pr_Man_t *)ABC_ALLOC( char, sizeof(Pr_Man_t) );
memset( p, 0, sizeof(Pr_Man_t) );
// allocate internal arrays
Pr_ManResize( p, nVarsAlloc? nVarsAlloc : 256 );
@@ -153,7 +150,7 @@ Pr_Man_t * Pr_ManAlloc( int nVarsAlloc )
p->nChunkSize = (1<<16); // use 64K chunks
// verification
p->nResLitsAlloc = (1<<16);
- p->pResLits = malloc( sizeof(lit) * p->nResLitsAlloc );
+ p->pResLits = ABC_ALLOC( lit, p->nResLitsAlloc );
// parameters
p->fProofWrite = 0;
p->fProofVerif = 0;
@@ -183,13 +180,13 @@ void Pr_ManResize( Pr_Man_t * p, int nVarsNew )
while ( p->nVarsAlloc < nVarsNew )
p->nVarsAlloc *= 2;
// resize the arrays
- p->pTrail = (lit *) realloc( p->pTrail, sizeof(lit) * p->nVarsAlloc );
- p->pAssigns = (lit *) realloc( p->pAssigns, sizeof(lit) * p->nVarsAlloc );
- p->pSeens = (char *) realloc( p->pSeens, sizeof(char) * p->nVarsAlloc );
- p->pVarTypes = (char *) realloc( p->pVarTypes, sizeof(char) * p->nVarsAlloc );
- p->pReasons = (Pr_Cls_t **)realloc( p->pReasons, sizeof(Pr_Cls_t *) * p->nVarsAlloc );
- p->pWatches = (Pr_Cls_t **)realloc( p->pWatches, sizeof(Pr_Cls_t *) * p->nVarsAlloc*2 );
- // clean the free space
+ p->pTrail = ABC_REALLOC(lit, p->pTrail, p->nVarsAlloc );
+ p->pAssigns = ABC_REALLOC(lit, p->pAssigns, p->nVarsAlloc );
+ p->pSeens = ABC_REALLOC(char, p->pSeens, p->nVarsAlloc );
+ p->pVarTypes = ABC_REALLOC(char, p->pVarTypes, p->nVarsAlloc );
+ p->pReasons = ABC_REALLOC(Pr_Cls_t *, p->pReasons, p->nVarsAlloc );
+ p->pWatches = ABC_REALLOC(Pr_Cls_t *, p->pWatches, p->nVarsAlloc*2 );
+ // clean the ABC_FREE space
memset( p->pAssigns + nVarsAllocOld, 0xff, sizeof(lit) * (p->nVarsAlloc - nVarsAllocOld) );
memset( p->pSeens + nVarsAllocOld, 0, sizeof(char) * (p->nVarsAlloc - nVarsAllocOld) );
memset( p->pVarTypes + nVarsAllocOld, 0, sizeof(char) * (p->nVarsAlloc - nVarsAllocOld) );
@@ -215,20 +212,20 @@ void Pr_ManResize( Pr_Man_t * p, int nVarsNew )
void Pr_ManFree( Pr_Man_t * p )
{
printf( "Runtime stats:\n" );
-PRT( "Reading ", p->timeRead );
-PRT( "BCP ", p->timeBcp );
-PRT( "Trace ", p->timeTrace );
-PRT( "TOTAL ", p->timeTotal );
+ABC_PRT( "Reading ", p->timeRead );
+ABC_PRT( "BCP ", p->timeBcp );
+ABC_PRT( "Trace ", p->timeTrace );
+ABC_PRT( "TOTAL ", p->timeTotal );
Pr_ManMemoryStop( p );
- free( p->pTrail );
- free( p->pAssigns );
- free( p->pSeens );
- free( p->pVarTypes );
- free( p->pReasons );
- free( p->pWatches );
- free( p->pResLits );
- free( p );
+ ABC_FREE( p->pTrail );
+ ABC_FREE( p->pAssigns );
+ ABC_FREE( p->pSeens );
+ ABC_FREE( p->pVarTypes );
+ ABC_FREE( p->pReasons );
+ ABC_FREE( p->pWatches );
+ ABC_FREE( p->pResLits );
+ ABC_FREE( p );
}
/**Function*************************************************************
@@ -348,7 +345,7 @@ char * Pr_ManMemoryFetch( Pr_Man_t * p, int nBytes )
char * pMem;
if ( p->pChunkLast == NULL || nBytes > p->nChunkSize - p->nChunkUsed )
{
- pMem = (char *)malloc( p->nChunkSize );
+ pMem = (char *)ABC_ALLOC( char, p->nChunkSize );
*(char **)pMem = p->pChunkLast;
p->pChunkLast = pMem;
p->nChunkUsed = sizeof(char *);
@@ -375,8 +372,8 @@ void Pr_ManMemoryStop( Pr_Man_t * p )
if ( p->pChunkLast == NULL )
return;
for ( pMem = p->pChunkLast; pNext = *(char **)pMem; pMem = pNext )
- free( pMem );
- free( pMem );
+ ABC_FREE( pMem );
+ ABC_FREE( pMem );
}
/**Function*************************************************************
@@ -1124,7 +1121,7 @@ Pr_Man_t * Pr_ManProofRead( char * pFileName )
}
// read the file
- pBuffer = (char *)malloc( (1<<16) );
+ pBuffer = (char *)ABC_ALLOC( char, (1<<16) );
for ( Counter = 0; fgets( pBuffer, (1<<16), pFile ); )
{
if ( pBuffer[0] == 'c' )
@@ -1139,7 +1136,7 @@ Pr_Man_t * Pr_ManProofRead( char * pFileName )
printf( "Wrong input file format.\n" );
}
p = Pr_ManAlloc( nVars );
- pArray = (int *)malloc( sizeof(int) * (nVars + 10) );
+ pArray = (int *)ABC_ALLOC( char, sizeof(int) * (nVars + 10) );
continue;
}
// skip empty lines
@@ -1178,8 +1175,8 @@ Pr_Man_t * Pr_ManProofRead( char * pFileName )
printf( "Expected %d clauses but read %d.\n", nClauses, Counter );
// finish
- if ( pArray ) free( pArray );
- if ( pBuffer ) free( pBuffer );
+ if ( pArray ) ABC_FREE( pArray );
+ if ( pBuffer ) ABC_FREE( pBuffer );
fclose( pFile );
return p;
}
diff --git a/src/sat/proof/pr.h b/src/sat/proof/pr.h
index 1e71a2d3..bc55e016 100644
--- a/src/sat/proof/pr.h
+++ b/src/sat/proof/pr.h
@@ -21,10 +21,6 @@
#ifndef __PR_H__
#define __PR_H__
-#ifdef __cplusplus
-extern "C" {
-#endif
-
#ifdef _WIN32
#define inline __inline // compatible with MS VS 6.0
#endif
@@ -37,6 +33,10 @@ extern "C" {
/// PARAMETERS ///
////////////////////////////////////////////////////////////////////////
+#ifdef __cplusplus
+extern "C" {
+#endif
+
////////////////////////////////////////////////////////////////////////
/// BASIC TYPES ///
////////////////////////////////////////////////////////////////////////
--
cgit v1.2.3