Skip to content

A
abc
Commit 123b4250 by Bruno Schmitt
Options

Fixes to make xSAT compile with old compilers. 

Small typos and variables renaming.
parent cb49c5d0
Showing with 35 additions and 42 deletions
src/sat/xsat/xsatBQueue.h
...@@ -24,7 +24,6 @@ ...@@ -24,7 +24,6 @@
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
/// INCLUDES /// /// INCLUDES ///
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
#include "misc/util/abc_global.h" #include "misc/util/abc_global.h"
ABC_NAMESPACE_HEADER_START ABC_NAMESPACE_HEADER_START
...@@ -32,7 +31,6 @@ ABC_NAMESPACE_HEADER_START ...@@ -32,7 +31,6 @@ ABC_NAMESPACE_HEADER_START
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
/// STRUCTURE DEFINITIONS /// /// STRUCTURE DEFINITIONS ///
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
typedef struct xSAT_BQueue_t_ xSAT_BQueue_t; typedef struct xSAT_BQueue_t_ xSAT_BQueue_t;
struct xSAT_BQueue_t_ struct xSAT_BQueue_t_
{ {
...@@ -41,13 +39,12 @@ struct xSAT_BQueue_t_ ...@@ -41,13 +39,12 @@ struct xSAT_BQueue_t_
int iFirst; int iFirst;
int iEmpty; int iEmpty;
word nSum; word nSum;
word * pData; unsigned * pData;
}; };
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
/// FUNCTION DECLARATIONS /// /// FUNCTION DECLARATIONS ///
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
/**Function************************************************************* /**Function*************************************************************
Synopsis [] Synopsis []
...@@ -63,7 +60,7 @@ static inline xSAT_BQueue_t * xSAT_BQueueNew( int nCap ) ...@@ -63,7 +60,7 @@ static inline xSAT_BQueue_t * xSAT_BQueueNew( int nCap )
{ {
xSAT_BQueue_t * p = ABC_CALLOC( xSAT_BQueue_t, 1 ); xSAT_BQueue_t * p = ABC_CALLOC( xSAT_BQueue_t, 1 );
p->nCap = nCap; p->nCap = nCap;
p->pData = ABC_CALLOC( word, nCap ); p->pData = ABC_CALLOC( unsigned, nCap );
return p; return p;
} }
...@@ -95,7 +92,7 @@ static inline void xSAT_BQueueFree( xSAT_BQueue_t * p ) ...@@ -95,7 +92,7 @@ static inline void xSAT_BQueueFree( xSAT_BQueue_t * p )
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
static inline void xSAT_BQueuePush( xSAT_BQueue_t * p, word Value ) static inline void xSAT_BQueuePush( xSAT_BQueue_t * p, unsigned Value )
{ {
if ( p->nSize == p->nCap ) if ( p->nSize == p->nCap )
{ {
...@@ -128,8 +125,8 @@ static inline void xSAT_BQueuePush( xSAT_BQueue_t * p, word Value ) ...@@ -128,8 +125,8 @@ static inline void xSAT_BQueuePush( xSAT_BQueue_t * p, word Value )
***********************************************************************/ ***********************************************************************/
static inline int xSAT_BQueuePop( xSAT_BQueue_t * p ) static inline int xSAT_BQueuePop( xSAT_BQueue_t * p )
{ {
int RetValue = p->pData[p->iFirst];
assert( p->nSize >= 1 ); assert( p->nSize >= 1 );
int RetValue = p->pData[p->iFirst];
p->nSum -= RetValue; p->nSum -= RetValue;
p->iFirst = ( p->iFirst + 1 ) % p->nCap; p->iFirst = ( p->iFirst + 1 ) % p->nCap;
p->nSize--; p->nSize--;
...@@ -147,9 +144,9 @@ static inline int xSAT_BQueuePop( xSAT_BQueue_t * p ) ...@@ -147,9 +144,9 @@ static inline int xSAT_BQueuePop( xSAT_BQueue_t * p )
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
static inline word xSAT_BQueueAvg( xSAT_BQueue_t * p ) static inline unsigned xSAT_BQueueAvg( xSAT_BQueue_t * p )
{ {
return ( word )( p->nSum / ( ( word ) p->nSize ) ); return ( unsigned )( p->nSum / ( ( word ) p->nSize ) );
} }
/**Function************************************************************* /**Function*************************************************************
......
src/sat/xsat/xsatClause.h
...@@ -39,7 +39,7 @@ struct xSAT_Clause_t_ ...@@ -39,7 +39,7 @@ struct xSAT_Clause_t_
unsigned fReallocd : 1; unsigned fReallocd : 1;
unsigned fCanBeDel : 1; unsigned fCanBeDel : 1;
unsigned nLBD : 28; unsigned nLBD : 28;
unsigned nSize; int nSize;
union { union {
int Lit; int Lit;
unsigned Act; unsigned Act;
...@@ -60,7 +60,7 @@ struct xSAT_Clause_t_ ...@@ -60,7 +60,7 @@ struct xSAT_Clause_t_
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
static int xSAT_ClauseCompare( const void * p1, const void * p2 ) static inline int xSAT_ClauseCompare( const void * p1, const void * p2 )
{ {
xSAT_Clause_t * pC1 = ( xSAT_Clause_t * ) p1; xSAT_Clause_t * pC1 = ( xSAT_Clause_t * ) p1;
xSAT_Clause_t * pC2 = ( xSAT_Clause_t * ) p2; xSAT_Clause_t * pC2 = ( xSAT_Clause_t * ) p2;
...@@ -91,12 +91,12 @@ static int xSAT_ClauseCompare( const void * p1, const void * p2 ) ...@@ -91,12 +91,12 @@ static int xSAT_ClauseCompare( const void * p1, const void * p2 )
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
static void xSAT_ClausePrint( xSAT_Clause_t * pCla ) static inline void xSAT_ClausePrint( xSAT_Clause_t * pCla )
{ {
int i; int i;
printf("{ "); printf("{ ");
for ( i = 0; i < (int)pCla->nSize; i++ ) for ( i = 0; i < pCla->nSize; i++ )
printf("%d ", pCla->pData[i].Lit ); printf("%d ", pCla->pData[i].Lit );
printf("}\n"); printf("}\n");
} }
......
src/sat/xsat/xsatHeap.h
...@@ -48,7 +48,7 @@ struct xSAT_Heap_t_ ...@@ -48,7 +48,7 @@ struct xSAT_Heap_t_
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
static inline int xSAT_HeapSize( xSAT_Heap_t * h ) inline int xSAT_HeapSize( xSAT_Heap_t * h )
{ {
return Vec_IntSize( h->vHeap ); return Vec_IntSize( h->vHeap );
} }
...@@ -64,7 +64,7 @@ static inline int xSAT_HeapSize( xSAT_Heap_t * h ) ...@@ -64,7 +64,7 @@ static inline int xSAT_HeapSize( xSAT_Heap_t * h )
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
static inline int xSAT_HeapInHeap( xSAT_Heap_t * h, int Var ) inline int xSAT_HeapInHeap( xSAT_Heap_t * h, int Var )
{ {
return ( Var < Vec_IntSize( h->vIndices ) ) && ( Vec_IntEntry( h->vIndices, Var ) >= 0 ); return ( Var < Vec_IntSize( h->vIndices ) ) && ( Vec_IntEntry( h->vIndices, Var ) >= 0 );
} }
......
src/sat/xsat/xsatMemory.h
...@@ -77,16 +77,14 @@ static inline void xSAT_MemGrow( xSAT_Mem_t * p, unsigned nCap ) ...@@ -77,16 +77,14 @@ static inline void xSAT_MemGrow( xSAT_Mem_t * p, unsigned nCap )
unsigned nPrevCap = p->nCap; unsigned nPrevCap = p->nCap;
if ( p->nCap >= nCap ) if ( p->nCap >= nCap )
return; return;
while (p->nCap < nCap) while (p->nCap < nCap)
{ {
unsigned delta = ((p->nCap >> 1) + (p->nCap >> 3) + 2) & ~1; unsigned delta = ( ( p->nCap >> 1 ) + ( p->nCap >> 3 ) + 2 ) & ~1;
p->nCap += delta; p->nCap += delta;
assert(p->nCap >= nPrevCap); assert(p->nCap >= nPrevCap);
} }
assert(p->nCap > 0); assert(p->nCap > 0);
p->pData = ABC_REALLOC(unsigned, p->pData, p->nCap); p->pData = ABC_REALLOC( unsigned, p->pData, p->nCap );
} }
/**Function************************************************************* /**Function*************************************************************
...@@ -160,12 +158,10 @@ static inline unsigned xSAT_MemAppend( xSAT_Mem_t * p, int nSize ) ...@@ -160,12 +158,10 @@ static inline unsigned xSAT_MemAppend( xSAT_Mem_t * p, int nSize )
{ {
unsigned nPrevSize; unsigned nPrevSize;
assert(nSize > 0); assert(nSize > 0);
xSAT_MemGrow(p, p->nSize + nSize); xSAT_MemGrow( p, p->nSize + nSize );
nPrevSize = p->nSize; nPrevSize = p->nSize;
p->nSize += nSize; p->nSize += nSize;
assert(p->nSize > nPrevSize); assert(p->nSize > nPrevSize);
return nPrevSize; return nPrevSize;
} }
......
src/sat/xsat/xsatSolver.h
...@@ -81,8 +81,8 @@ struct xSAT_SolverOptions_t_ ...@@ -81,8 +81,8 @@ struct xSAT_SolverOptions_t_
char fVerbose; char fVerbose;
// Limits // Limits
word nConfLimit; // external limit on the number of conflicts iword nConfLimit; // external limit on the number of conflicts
word nInsLimit; // external limit on the number of implications iword nInsLimit; // external limit on the number of implications
abctime nRuntimeLimit; // external limit on runtime abctime nRuntimeLimit; // external limit on runtime
// Constants used for restart heuristic // Constants used for restart heuristic
...@@ -105,13 +105,13 @@ struct xSAT_Stats_t_ ...@@ -105,13 +105,13 @@ struct xSAT_Stats_t_
unsigned nStarts; unsigned nStarts;
unsigned nReduceDB; unsigned nReduceDB;
word nDecisions; iword nDecisions;
word nPropagations; iword nPropagations;
word nInspects; iword nInspects;
word nConflicts; iword nConflicts;
word nClauseLits; iword nClauseLits;
word nLearntLits; iword nLearntLits;
}; };
struct xSAT_Solver_t_ struct xSAT_Solver_t_
...@@ -143,7 +143,7 @@ struct xSAT_Solver_t_ ...@@ -143,7 +143,7 @@ struct xSAT_Solver_t_
int nAssignSimplify; /* Number of top-level assignments since last int nAssignSimplify; /* Number of top-level assignments since last
* execution of 'simplify()'. */ * execution of 'simplify()'. */
word nPropSimplify; /* Remaining number of propagations that must be int64_t nPropSimplify; /* Remaining number of propagations that must be
* made before next execution of 'simplify()'. */ * made before next execution of 'simplify()'. */
/* Temporary data used by Search method */ /* Temporary data used by Search method */
...@@ -203,10 +203,10 @@ static inline xSAT_Clause_t * xSAT_SolverReadClause( xSAT_Solver_t * s, unsigned ...@@ -203,10 +203,10 @@ static inline xSAT_Clause_t * xSAT_SolverReadClause( xSAT_Solver_t * s, unsigned
static inline int xSAT_SolverIsClauseSatisfied( xSAT_Solver_t * s, xSAT_Clause_t * pCla ) static inline int xSAT_SolverIsClauseSatisfied( xSAT_Solver_t * s, xSAT_Clause_t * pCla )
{ {
int i; int i;
int * lits = &( pCla->pData[0].Lit ); int * Lits = &( pCla->pData[0].Lit );
for ( i = 0; i < (int)pCla->nSize; i++ ) for ( i = 0; i < pCla->nSize; i++ )
if ( Vec_StrEntry( s->vAssigns, xSAT_Lit2Var( lits[i] ) ) == xSAT_LitSign( ( lits[i] ) ) ) if ( Vec_StrEntry( s->vAssigns, xSAT_Lit2Var( Lits[i] ) ) == xSAT_LitSign( ( Lits[i] ) ) )
return true; return true;
return false; return false;
......
src/sat/xsat/xsatSolverAPI.c
...@@ -51,6 +51,7 @@ xSAT_SolverOptions_t DefaultConfig = ...@@ -51,6 +51,7 @@ xSAT_SolverOptions_t DefaultConfig =
30 //.nLBDFrozenClause = 30 30 //.nLBDFrozenClause = 30
}; };
/**Function************************************************************* /**Function*************************************************************
Synopsis [] Synopsis []
...@@ -125,7 +126,6 @@ void xSAT_SolverDestroy( xSAT_Solver_t * s ) ...@@ -125,7 +126,6 @@ void xSAT_SolverDestroy( xSAT_Solver_t * s )
xSAT_VecWatchListFree( s->vWatches ); xSAT_VecWatchListFree( s->vWatches );
xSAT_VecWatchListFree( s->vBinWatches ); xSAT_VecWatchListFree( s->vBinWatches );
// delete vectors
xSAT_HeapFree(s->hOrder); xSAT_HeapFree(s->hOrder);
Vec_IntFree( s->vTrailLim ); Vec_IntFree( s->vTrailLim );
Vec_IntFree( s->vTrail ); Vec_IntFree( s->vTrail );
......
src/sat/xsat/xsatWatchList.h
...@@ -118,9 +118,9 @@ static inline void xSAT_WatchListShrink( xSAT_WatchList_t * v, int k ) ...@@ -118,9 +118,9 @@ static inline void xSAT_WatchListShrink( xSAT_WatchList_t * v, int k )
static inline void xSAT_WatchListPush( xSAT_WatchList_t * v, xSAT_Watcher_t e ) static inline void xSAT_WatchListPush( xSAT_WatchList_t * v, xSAT_Watcher_t e )
{ {
assert( v ); assert( v );
if (v->nSize == v->nCap) if ( v->nSize == v->nCap )
{ {
int newsize = (v->nCap < 4) ? 4 : (v->nCap / 2) * 3; int newsize = ( v->nCap < 4 ) ? 4 : ( v->nCap / 2 ) * 3;
v->pArray = ABC_REALLOC( xSAT_Watcher_t, v->pArray, newsize ); v->pArray = ABC_REALLOC( xSAT_Watcher_t, v->pArray, newsize );
if ( v->pArray == NULL ) if ( v->pArray == NULL )
...@@ -167,9 +167,9 @@ static inline void xSAT_WatchListRemove( xSAT_WatchList_t * v, unsigned CRef ) ...@@ -167,9 +167,9 @@ static inline void xSAT_WatchListRemove( xSAT_WatchList_t * v, unsigned CRef )
xSAT_Watcher_t* ws = xSAT_WatchListArray(v); xSAT_Watcher_t* ws = xSAT_WatchListArray(v);
int j = 0; int j = 0;
for (; ws[j].CRef != CRef; j++); for ( ; ws[j].CRef != CRef; j++ );
assert(j < xSAT_WatchListSize(v)); assert( j < xSAT_WatchListSize( v ) );
memmove(v->pArray + j, v->pArray + j + 1, (v->nSize - j - 1) * sizeof(xSAT_Watcher_t)); memmove( v->pArray + j, v->pArray + j + 1, ( v->nSize - j - 1 ) * sizeof( xSAT_Watcher_t ) );
v->nSize -= 1; v->nSize -= 1;
} }
...@@ -190,7 +190,7 @@ static inline xSAT_VecWatchList_t * xSAT_VecWatchListAlloc( int nCap ) ...@@ -190,7 +190,7 @@ static inline xSAT_VecWatchList_t * xSAT_VecWatchListAlloc( int nCap )
v->nCap = 4; v->nCap = 4;
v->nSize = 0; v->nSize = 0;
v->pArray = (xSAT_WatchList_t *) ABC_CALLOC(xSAT_WatchList_t, sizeof( xSAT_WatchList_t ) * v->nCap); v->pArray = ( xSAT_WatchList_t * ) ABC_CALLOC(xSAT_WatchList_t, sizeof( xSAT_WatchList_t ) * v->nCap);
return v; return v;
} }
...@@ -233,7 +233,7 @@ static inline void xSAT_VecWatchListPush( xSAT_VecWatchList_t* v ) ...@@ -233,7 +233,7 @@ static inline void xSAT_VecWatchListPush( xSAT_VecWatchList_t* v )
int newsize = (v->nCap < 4) ? v->nCap * 2 : (v->nCap / 2) * 3; int newsize = (v->nCap < 4) ? v->nCap * 2 : (v->nCap / 2) * 3;
v->pArray = ABC_REALLOC( xSAT_WatchList_t, v->pArray, newsize ); v->pArray = ABC_REALLOC( xSAT_WatchList_t, v->pArray, newsize );
memset( v->pArray + v->nCap, 0, sizeof(xSAT_WatchList_t) * (newsize - v->nCap) ); memset( v->pArray + v->nCap, 0, sizeof( xSAT_WatchList_t ) * ( newsize - v->nCap ) );
if ( v->pArray == NULL ) if ( v->pArray == NULL )
{ {
printf( "Failed to realloc memory from %.1f MB to %.1f MB.\n", printf( "Failed to realloc memory from %.1f MB to %.1f MB.\n",
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment