src/sat/msat/msatVec.c File Reference

#include "msatInt.h"
Include dependency graph for msatVec.c:

Go to the source code of this file.

Functions

static int Msat_IntVecSortCompare1 (int *pp1, int *pp2)
static int Msat_IntVecSortCompare2 (int *pp1, int *pp2)
Msat_IntVec_t * Msat_IntVecAlloc (int nCap)
Msat_IntVec_t * Msat_IntVecAllocArray (int *pArray, int nSize)
Msat_IntVec_t * Msat_IntVecAllocArrayCopy (int *pArray, int nSize)
Msat_IntVec_t * Msat_IntVecDup (Msat_IntVec_t *pVec)
Msat_IntVec_t * Msat_IntVecDupArray (Msat_IntVec_t *pVec)
void Msat_IntVecFree (Msat_IntVec_t *p)
void Msat_IntVecFill (Msat_IntVec_t *p, int nSize, int Entry)
int * Msat_IntVecReleaseArray (Msat_IntVec_t *p)
int * Msat_IntVecReadArray (Msat_IntVec_t *p)
int Msat_IntVecReadSize (Msat_IntVec_t *p)
int Msat_IntVecReadEntry (Msat_IntVec_t *p, int i)
void Msat_IntVecWriteEntry (Msat_IntVec_t *p, int i, int Entry)
int Msat_IntVecReadEntryLast (Msat_IntVec_t *p)
void Msat_IntVecGrow (Msat_IntVec_t *p, int nCapMin)
void Msat_IntVecShrink (Msat_IntVec_t *p, int nSizeNew)
void Msat_IntVecClear (Msat_IntVec_t *p)
void Msat_IntVecPush (Msat_IntVec_t *p, int Entry)
int Msat_IntVecPushUnique (Msat_IntVec_t *p, int Entry)
void Msat_IntVecPushUniqueOrder (Msat_IntVec_t *p, int Entry, int fIncrease)
int Msat_IntVecPop (Msat_IntVec_t *p)
void Msat_IntVecSort (Msat_IntVec_t *p, int fReverse)

Function Documentation

Msat_IntVec_t* Msat_IntVecAlloc ( int  nCap  ) 

FUNCTION DEFINITIONS ///Function*************************************************************

Synopsis [Allocates a vector with the given capacity.]

Description []

SideEffects []

SeeAlso []

Definition at line 45 of file msatVec.c.

00046 {
00047     Msat_IntVec_t * p;
00048     p = ALLOC( Msat_IntVec_t, 1 );
00049     if ( nCap > 0 && nCap < 16 )
00050         nCap = 16;
00051     p->nSize  = 0;
00052     p->nCap   = nCap;
00053     p->pArray = p->nCap? ALLOC( int, p->nCap ) : NULL;
00054     return p;
00055 }

Msat_IntVec_t* Msat_IntVecAllocArray ( int *  pArray,
int  nSize 
)

Function*************************************************************

Synopsis [Creates the vector from an integer array of the given size.]

Description []

SideEffects []

SeeAlso []

Definition at line 68 of file msatVec.c.

00069 {
00070     Msat_IntVec_t * p;
00071     p = ALLOC( Msat_IntVec_t, 1 );
00072     p->nSize  = nSize;
00073     p->nCap   = nSize;
00074     p->pArray = pArray;
00075     return p;
00076 }

Msat_IntVec_t* Msat_IntVecAllocArrayCopy ( int *  pArray,
int  nSize 
)

Function*************************************************************

Synopsis [Creates the vector from an integer array of the given size.]

Description []

SideEffects []

SeeAlso []

Definition at line 89 of file msatVec.c.

00090 {
00091     Msat_IntVec_t * p;
00092     p = ALLOC( Msat_IntVec_t, 1 );
00093     p->nSize  = nSize;
00094     p->nCap   = nSize;
00095     p->pArray = ALLOC( int, nSize );
00096     memcpy( p->pArray, pArray, sizeof(int) * nSize );
00097     return p;
00098 }

void Msat_IntVecClear ( Msat_IntVec_t *  p  ) 

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 332 of file msatVec.c.

00333 {
00334     p->nSize = 0;
00335 }

Msat_IntVec_t* Msat_IntVecDup ( Msat_IntVec_t *  pVec  ) 

Function*************************************************************

Synopsis [Duplicates the integer array.]

Description []

SideEffects []

SeeAlso []

Definition at line 111 of file msatVec.c.

00112 {
00113     Msat_IntVec_t * p;
00114     p = ALLOC( Msat_IntVec_t, 1 );
00115     p->nSize  = pVec->nSize;
00116     p->nCap   = pVec->nCap;
00117     p->pArray = p->nCap? ALLOC( int, p->nCap ) : NULL;
00118     memcpy( p->pArray, pVec->pArray, sizeof(int) * pVec->nSize );
00119     return p;
00120 }

Msat_IntVec_t* Msat_IntVecDupArray ( Msat_IntVec_t *  pVec  ) 

Function*************************************************************

Synopsis [Transfers the array into another vector.]

Description []

SideEffects []

SeeAlso []

Definition at line 133 of file msatVec.c.

00134 {
00135     Msat_IntVec_t * p;
00136     p = ALLOC( Msat_IntVec_t, 1 );
00137     p->nSize  = pVec->nSize;
00138     p->nCap   = pVec->nCap;
00139     p->pArray = pVec->pArray;
00140     pVec->nSize  = 0;
00141     pVec->nCap   = 0;
00142     pVec->pArray = NULL;
00143     return p;
00144 }

void Msat_IntVecFill ( Msat_IntVec_t *  p,
int  nSize,
int  Entry 
)

Function*************************************************************

Synopsis [Fills the vector with given number of entries.]

Description []

SideEffects []

SeeAlso []

Definition at line 174 of file msatVec.c.

00175 {
00176     int i;
00177     Msat_IntVecGrow( p, nSize );
00178     p->nSize = nSize;
00179     for ( i = 0; i < p->nSize; i++ )
00180         p->pArray[i] = Entry;
00181 }

void Msat_IntVecFree ( Msat_IntVec_t *  p  ) 

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 157 of file msatVec.c.

00158 {
00159     FREE( p->pArray );
00160     FREE( p );
00161 }

void Msat_IntVecGrow ( Msat_IntVec_t *  p,
int  nCapMin 
)

Function*************************************************************

Synopsis [Resizes the vector to the given capacity.]

Description []

SideEffects []

SeeAlso []

Definition at line 296 of file msatVec.c.

00297 {
00298     if ( p->nCap >= nCapMin )
00299         return;
00300     p->pArray = REALLOC( int, p->pArray, nCapMin ); 
00301     p->nCap   = nCapMin;
00302 }

int Msat_IntVecPop ( Msat_IntVec_t *  p  ) 

Function*************************************************************

Synopsis [Returns the last entry and removes it from the list.]

Description []

SideEffects []

SeeAlso []

Definition at line 422 of file msatVec.c.

00423 {
00424     assert( p->nSize > 0 );
00425     return p->pArray[--p->nSize];
00426 }

void Msat_IntVecPush ( Msat_IntVec_t *  p,
int  Entry 
)

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 348 of file msatVec.c.

00349 {
00350     if ( p->nSize == p->nCap )
00351     {
00352         if ( p->nCap < 16 )
00353             Msat_IntVecGrow( p, 16 );
00354         else
00355             Msat_IntVecGrow( p, 2 * p->nCap );
00356     }
00357     p->pArray[p->nSize++] = Entry;
00358 }

int Msat_IntVecPushUnique ( Msat_IntVec_t *  p,
int  Entry 
)

Function*************************************************************

Synopsis [Add the element while ensuring uniqueness.]

Description [Returns 1 if the element was found, and 0 if it was new. ]

SideEffects []

SeeAlso []

Definition at line 371 of file msatVec.c.

00372 {
00373     int i;
00374     for ( i = 0; i < p->nSize; i++ )
00375         if ( p->pArray[i] == Entry )
00376             return 1;
00377     Msat_IntVecPush( p, Entry );
00378     return 0;
00379 }

void Msat_IntVecPushUniqueOrder ( Msat_IntVec_t *  p,
int  Entry,
int  fIncrease 
)

Function*************************************************************

Synopsis [Inserts the element while sorting in the increasing order.]

Description []

SideEffects []

SeeAlso []

Definition at line 392 of file msatVec.c.

00393 {
00394     int Entry1, Entry2;
00395     int i;
00396     Msat_IntVecPushUnique( p, Entry );
00397     // find the p of the node
00398     for ( i = p->nSize-1; i > 0; i-- )
00399     {
00400         Entry1 = p->pArray[i  ];
00401         Entry2 = p->pArray[i-1];
00402         if ( fIncrease && Entry1 >= Entry2 || 
00403             !fIncrease && Entry1 <= Entry2 )
00404             break;
00405         p->pArray[i  ] = Entry2;
00406         p->pArray[i-1] = Entry1;
00407     }
00408 }

int* Msat_IntVecReadArray ( Msat_IntVec_t *  p  ) 

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 214 of file msatVec.c.

00215 {
00216     return p->pArray;
00217 }

int Msat_IntVecReadEntry ( Msat_IntVec_t *  p,
int  i 
)

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 246 of file msatVec.c.

00247 {
00248     assert( i >= 0 && i < p->nSize );
00249     return p->pArray[i];
00250 }

int Msat_IntVecReadEntryLast ( Msat_IntVec_t *  p  ) 

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 280 of file msatVec.c.

00281 {
00282     return p->pArray[p->nSize-1];
00283 }

int Msat_IntVecReadSize ( Msat_IntVec_t *  p  ) 

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 230 of file msatVec.c.

00231 {
00232     return p->nSize;
00233 }

int* Msat_IntVecReleaseArray ( Msat_IntVec_t *  p  ) 

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 194 of file msatVec.c.

00195 {
00196     int * pArray = p->pArray;
00197     p->nCap = 0;
00198     p->nSize = 0;
00199     p->pArray = NULL;
00200     return pArray;
00201 }

void Msat_IntVecShrink ( Msat_IntVec_t *  p,
int  nSizeNew 
)

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 315 of file msatVec.c.

00316 {
00317     assert( p->nSize >= nSizeNew );
00318     p->nSize = nSizeNew;
00319 }

void Msat_IntVecSort ( Msat_IntVec_t *  p,
int  fReverse 
)

Function*************************************************************

Synopsis [Sorting the entries by their integer value.]

Description []

SideEffects []

SeeAlso []

Definition at line 439 of file msatVec.c.

00440 {
00441     if ( fReverse ) 
00442         qsort( (void *)p->pArray, p->nSize, sizeof(int), 
00443                 (int (*)(const void *, const void *)) Msat_IntVecSortCompare2 );
00444     else
00445         qsort( (void *)p->pArray, p->nSize, sizeof(int), 
00446                 (int (*)(const void *, const void *)) Msat_IntVecSortCompare1 );
00447 }

int Msat_IntVecSortCompare1 ( int *  pp1,
int *  pp2 
) [static]

CFile****************************************************************

FileName [msatVec.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 [Integer vector borrowed from Extra.]

Author [Alan Mishchenko <alanmi@eecs.berkeley.edu>]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - January 1, 2004.]

Revision [

Id
msatVec.c,v 1.0 2004/01/01 1:00:00 alanmi Exp

] DECLARATIONS ///

Function*************************************************************

Synopsis [Comparison procedure for two clauses.]

Description []

SideEffects []

SeeAlso []

Definition at line 460 of file msatVec.c.

00461 {
00462     // for some reason commenting out lines (as shown) led to crashing of the release version
00463     if ( *pp1 < *pp2 )
00464         return -1;
00465     if ( *pp1 > *pp2 ) //
00466         return 1;
00467     return 0; //
00468 }

int Msat_IntVecSortCompare2 ( int *  pp1,
int *  pp2 
) [static]

Function*************************************************************

Synopsis [Comparison procedure for two clauses.]

Description []

SideEffects []

SeeAlso []

Definition at line 481 of file msatVec.c.

00482 {
00483     // for some reason commenting out lines (as shown) led to crashing of the release version
00484     if ( *pp1 > *pp2 )
00485         return -1;
00486     if ( *pp1 < *pp2 ) //
00487         return 1;
00488     return 0; //
00489 }

void Msat_IntVecWriteEntry ( Msat_IntVec_t *  p,
int  i,
int  Entry 
)

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 263 of file msatVec.c.

00264 {
00265     assert( i >= 0 && i < p->nSize );
00266     p->pArray[i] = Entry;
00267 }

Generated on Tue Jan 5 12:19:40 2010 for abc70930 by  doxygen 1.6.1