/**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 ] 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" ABC_NAMESPACE_IMPL_START //////////////////////////////////////////////////////////////////////// /// 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 = ABC_ALLOC( Msat_ClauseVec_t, 1 ); if ( nCap > 0 && nCap < 16 ) nCap = 16; p->nSize = 0; p->nCap = nCap; p->pArray = p->nCap? ABC_ALLOC( Msat_Clause_t *, p->nCap ) : NULL; return p; } /**Function************************************************************* Synopsis [] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Msat_ClauseVecFree( Msat_ClauseVec_t * p ) { ABC_FREE( p->pArray ); ABC_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 = ABC_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 /// //////////////////////////////////////////////////////////////////////// ABC_NAMESPACE_IMPL_END