diff options
Diffstat (limited to 'src/sat/msat/msatClauseVec.c')
-rw-r--r-- | src/sat/msat/msatClauseVec.c | 232 |
1 files changed, 232 insertions, 0 deletions
diff --git a/src/sat/msat/msatClauseVec.c b/src/sat/msat/msatClauseVec.c new file mode 100644 index 00000000..04691cf2 --- /dev/null +++ b/src/sat/msat/msatClauseVec.c @@ -0,0 +1,232 @@ +/**CFile**************************************************************** + + FileName [msatClauseVec.c] + + PackageName [A C version of SAT solver MINISAT, originally developed + in C++ by Niklas Een and Niklas Sorensson, Chalmers University of + Technology, Sweden: http://www.cs.chalmers.se/~een/Satzoo.] + + Synopsis [Procedures working with arrays of SAT clauses.] + + Author [Alan Mishchenko <alanmi@eecs.berkeley.edu>] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - January 1, 2004.] + + Revision [$Id: msatClauseVec.c,v 1.0 2004/01/01 1:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "msatInt.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Allocates a vector with the given capacity.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Msat_ClauseVec_t * Msat_ClauseVecAlloc( int nCap ) +{ + Msat_ClauseVec_t * p; + p = 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; + return p; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Msat_ClauseVecFree( Msat_ClauseVec_t * p ) +{ + FREE( p->pArray ); + FREE( p ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Msat_Clause_t ** Msat_ClauseVecReadArray( Msat_ClauseVec_t * p ) +{ + return p->pArray; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Msat_ClauseVecReadSize( Msat_ClauseVec_t * p ) +{ + return p->nSize; +} + +/**Function************************************************************* + + Synopsis [Resizes the vector to the given capacity.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Msat_ClauseVecGrow( Msat_ClauseVec_t * p, int nCapMin ) +{ + if ( p->nCap >= nCapMin ) + return; + p->pArray = REALLOC( Msat_Clause_t *, p->pArray, nCapMin ); + p->nCap = nCapMin; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Msat_ClauseVecShrink( Msat_ClauseVec_t * p, int nSizeNew ) +{ + assert( p->nSize >= nSizeNew ); + p->nSize = nSizeNew; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Msat_ClauseVecClear( Msat_ClauseVec_t * p ) +{ + p->nSize = 0; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Msat_ClauseVecPush( Msat_ClauseVec_t * p, Msat_Clause_t * Entry ) +{ + if ( p->nSize == p->nCap ) + { + if ( p->nCap < 16 ) + Msat_ClauseVecGrow( p, 16 ); + else + Msat_ClauseVecGrow( p, 2 * p->nCap ); + } + p->pArray[p->nSize++] = Entry; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Msat_Clause_t * Msat_ClauseVecPop( Msat_ClauseVec_t * p ) +{ + return p->pArray[--p->nSize]; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Msat_ClauseVecWriteEntry( Msat_ClauseVec_t * p, int i, Msat_Clause_t * Entry ) +{ + assert( i >= 0 && i < p->nSize ); + p->pArray[i] = Entry; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Msat_Clause_t * Msat_ClauseVecReadEntry( Msat_ClauseVec_t * p, int i ) +{ + assert( i >= 0 && i < p->nSize ); + return p->pArray[i]; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + |