summaryrefslogtreecommitdiffstats
path: root/src/sat/msat/msatClauseVec.c
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2007-09-30 08:01:00 -0700
committerAlan Mishchenko <alanmi@berkeley.edu>2007-09-30 08:01:00 -0700
commite54d9691616b9a0326e2fdb3156bb4eeb8abfcd7 (patch)
treede3ffe87c3e17950351e3b7d97fa18318bd5ea9a /src/sat/msat/msatClauseVec.c
parent7d7e60f2dc84393cd4c5db22d2eaf7b1fb1a79b2 (diff)
downloadabc-e54d9691616b9a0326e2fdb3156bb4eeb8abfcd7.tar.gz
abc-e54d9691616b9a0326e2fdb3156bb4eeb8abfcd7.tar.bz2
abc-e54d9691616b9a0326e2fdb3156bb4eeb8abfcd7.zip
Version abc70930
Diffstat (limited to 'src/sat/msat/msatClauseVec.c')
-rw-r--r--src/sat/msat/msatClauseVec.c232
1 files changed, 0 insertions, 232 deletions
diff --git a/src/sat/msat/msatClauseVec.c b/src/sat/msat/msatClauseVec.c
deleted file mode 100644
index 04691cf2..00000000
--- a/src/sat/msat/msatClauseVec.c
+++ /dev/null
@@ -1,232 +0,0 @@
-/**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 ///
-////////////////////////////////////////////////////////////////////////
-
-