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