| /**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" |
| |
| 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 |
| |
