abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
Functions
msatVec.c File Reference
#include "msatInt.h"

Go to the source code of this file.

Functions

static ABC_NAMESPACE_IMPL_START int Msat_IntVecSortCompare1 (int *pp1, int *pp2)
 DECLARATIONS ///. More...
 
static int Msat_IntVecSortCompare2 (int *pp1, int *pp2)
 
Msat_IntVec_t * Msat_IntVecAlloc (int nCap)
 FUNCTION DEFINITIONS ///. More...
 
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 48 of file msatVec.c.

49 {
50  Msat_IntVec_t * p;
51  p = ABC_ALLOC( Msat_IntVec_t, 1 );
52  if ( nCap > 0 && nCap < 16 )
53  nCap = 16;
54  p->nSize = 0;
55  p->nCap = nCap;
56  p->pArray = p->nCap? ABC_ALLOC( int, p->nCap ) : NULL;
57  return p;
58 }
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Msat_IntVec_t_
Definition: msatInt.h:162
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
Msat_IntVec_t_::nSize
int nSize
Definition: msatInt.h:165
Msat_IntVec_t_::nCap
int nCap
Definition: msatInt.h:166
Msat_IntVec_t_::pArray
int * pArray
Definition: msatInt.h:164
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 71 of file msatVec.c.

72 {
73  Msat_IntVec_t * p;
74  p = ABC_ALLOC( Msat_IntVec_t, 1 );
75  p->nSize = nSize;
76  p->nCap = nSize;
77  p->pArray = pArray;
78  return p;
79 }
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Msat_IntVec_t_
Definition: msatInt.h:162
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
Msat_IntVec_t_::nSize
int nSize
Definition: msatInt.h:165
Msat_IntVec_t_::nCap
int nCap
Definition: msatInt.h:166
Msat_IntVec_t_::pArray
int * pArray
Definition: msatInt.h:164
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 92 of file msatVec.c.

93 {
94  Msat_IntVec_t * p;
95  p = ABC_ALLOC( Msat_IntVec_t, 1 );
96  p->nSize = nSize;
97  p->nCap = nSize;
98  p->pArray = ABC_ALLOC( int, nSize );
99  memcpy( p->pArray, pArray, sizeof(int) * nSize );
100  return p;
101 }
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Msat_IntVec_t_
Definition: msatInt.h:162
memcpy
char * memcpy()
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
Msat_IntVec_t_::nSize
int nSize
Definition: msatInt.h:165
Msat_IntVec_t_::nCap
int nCap
Definition: msatInt.h:166
Msat_IntVec_t_::pArray
int * pArray
Definition: msatInt.h:164
void Msat_IntVecClear ( Msat_IntVec_t *  p)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 335 of file msatVec.c.

336 {
337  p->nSize = 0;
338 }
Msat_IntVec_t_::nSize
int nSize
Definition: msatInt.h:165
Msat_IntVec_t* Msat_IntVecDup ( Msat_IntVec_t *  pVec)

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

Synopsis [Duplicates the integer array.]

Description []

SideEffects []

SeeAlso []

Definition at line 114 of file msatVec.c.

115 {
116  Msat_IntVec_t * p;
117  p = ABC_ALLOC( Msat_IntVec_t, 1 );
118  p->nSize = pVec->nSize;
119  p->nCap = pVec->nCap;
120  p->pArray = p->nCap? ABC_ALLOC( int, p->nCap ) : NULL;
121  memcpy( p->pArray, pVec->pArray, sizeof(int) * pVec->nSize );
122  return p;
123 }
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Msat_IntVec_t_
Definition: msatInt.h:162
memcpy
char * memcpy()
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
Msat_IntVec_t_::nSize
int nSize
Definition: msatInt.h:165
Msat_IntVec_t_::nCap
int nCap
Definition: msatInt.h:166
Msat_IntVec_t_::pArray
int * pArray
Definition: msatInt.h:164
Msat_IntVec_t* Msat_IntVecDupArray ( Msat_IntVec_t *  pVec)

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

Synopsis [Transfers the array into another vector.]

Description []

SideEffects []

SeeAlso []

Definition at line 136 of file msatVec.c.

137 {
138  Msat_IntVec_t * p;
139  p = ABC_ALLOC( Msat_IntVec_t, 1 );
140  p->nSize = pVec->nSize;
141  p->nCap = pVec->nCap;
142  p->pArray = pVec->pArray;
143  pVec->nSize = 0;
144  pVec->nCap = 0;
145  pVec->pArray = NULL;
146  return p;
147 }
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Msat_IntVec_t_
Definition: msatInt.h:162
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
Msat_IntVec_t_::nSize
int nSize
Definition: msatInt.h:165
Msat_IntVec_t_::nCap
int nCap
Definition: msatInt.h:166
Msat_IntVec_t_::pArray
int * pArray
Definition: msatInt.h:164
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 177 of file msatVec.c.

178 {
179  int i;
180  Msat_IntVecGrow( p, nSize );
181  p->nSize = nSize;
182  for ( i = 0; i < p->nSize; i++ )
183  p->pArray[i] = Entry;
184 }
Msat_IntVec_t_::nSize
int nSize
Definition: msatInt.h:165
Msat_IntVecGrow
void Msat_IntVecGrow(Msat_IntVec_t *p, int nCapMin)
Definition: msatVec.c:299
Msat_IntVec_t_::pArray
int * pArray
Definition: msatInt.h:164
void Msat_IntVecFree ( Msat_IntVec_t *  p)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 160 of file msatVec.c.

161 {
162  ABC_FREE( p->pArray );
163  ABC_FREE( p );
164 }
ABC_FREE
#define ABC_FREE(obj)
Definition: abc_global.h:232
Msat_IntVec_t_::pArray
int * pArray
Definition: msatInt.h:164
void Msat_IntVecGrow ( Msat_IntVec_t *  p,
int  nCapMin 
)

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

Synopsis [Resizes the vector to the given capacity.]

Description []

SideEffects []

SeeAlso []

Definition at line 299 of file msatVec.c.

300 {
301  if ( p->nCap >= nCapMin )
302  return;
303  p->pArray = ABC_REALLOC( int, p->pArray, nCapMin );
304  p->nCap = nCapMin;
305 }
ABC_REALLOC
#define ABC_REALLOC(type, obj, num)
Definition: abc_global.h:233
Msat_IntVec_t_::nCap
int nCap
Definition: msatInt.h:166
Msat_IntVec_t_::pArray
int * pArray
Definition: msatInt.h:164
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 425 of file msatVec.c.

426 {
427  assert( p->nSize > 0 );
428  return p->pArray[--p->nSize];
429 }
Msat_IntVec_t_::nSize
int nSize
Definition: msatInt.h:165
assert
#define assert(ex)
Definition: util_old.h:213
Msat_IntVec_t_::pArray
int * pArray
Definition: msatInt.h:164
void Msat_IntVecPush ( Msat_IntVec_t *  p,
int  Entry 
)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 351 of file msatVec.c.

352 {
353  if ( p->nSize == p->nCap )
354  {
355  if ( p->nCap < 16 )
356  Msat_IntVecGrow( p, 16 );
357  else
358  Msat_IntVecGrow( p, 2 * p->nCap );
359  }
360  p->pArray[p->nSize++] = Entry;
361 }
Msat_IntVec_t_::nSize
int nSize
Definition: msatInt.h:165
Msat_IntVec_t_::nCap
int nCap
Definition: msatInt.h:166
Msat_IntVecGrow
void Msat_IntVecGrow(Msat_IntVec_t *p, int nCapMin)
Definition: msatVec.c:299
Msat_IntVec_t_::pArray
int * pArray
Definition: msatInt.h:164
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 374 of file msatVec.c.

375 {
376  int i;
377  for ( i = 0; i < p->nSize; i++ )
378  if ( p->pArray[i] == Entry )
379  return 1;
380  Msat_IntVecPush( p, Entry );
381  return 0;
382 }
Msat_IntVecPush
void Msat_IntVecPush(Msat_IntVec_t *p, int Entry)
Definition: msatVec.c:351
Msat_IntVec_t_::nSize
int nSize
Definition: msatInt.h:165
Msat_IntVec_t_::pArray
int * pArray
Definition: msatInt.h:164
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 395 of file msatVec.c.

396 {
397  int Entry1, Entry2;
398  int i;
399  Msat_IntVecPushUnique( p, Entry );
400  // find the p of the node
401  for ( i = p->nSize-1; i > 0; i-- )
402  {
403  Entry1 = p->pArray[i ];
404  Entry2 = p->pArray[i-1];
405  if (( fIncrease && Entry1 >= Entry2) ||
406  (!fIncrease && Entry1 <= Entry2) )
407  break;
408  p->pArray[i ] = Entry2;
409  p->pArray[i-1] = Entry1;
410  }
411 }
Msat_IntVec_t_::nSize
int nSize
Definition: msatInt.h:165
Msat_IntVec_t_::pArray
int * pArray
Definition: msatInt.h:164
Msat_IntVecPushUnique
int Msat_IntVecPushUnique(Msat_IntVec_t *p, int Entry)
Definition: msatVec.c:374
int* Msat_IntVecReadArray ( Msat_IntVec_t *  p)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 217 of file msatVec.c.

218 {
219  return p->pArray;
220 }
Msat_IntVec_t_::pArray
int * pArray
Definition: msatInt.h:164
int Msat_IntVecReadEntry ( Msat_IntVec_t *  p,
int  i 
)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 249 of file msatVec.c.

250 {
251  assert( i >= 0 && i < p->nSize );
252  return p->pArray[i];
253 }
assert
#define assert(ex)
Definition: util_old.h:213
Msat_IntVec_t_::pArray
int * pArray
Definition: msatInt.h:164
int Msat_IntVecReadEntryLast ( Msat_IntVec_t *  p)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 283 of file msatVec.c.

284 {
285  return p->pArray[p->nSize-1];
286 }
Msat_IntVec_t_::nSize
int nSize
Definition: msatInt.h:165
Msat_IntVec_t_::pArray
int * pArray
Definition: msatInt.h:164
int Msat_IntVecReadSize ( Msat_IntVec_t *  p)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 233 of file msatVec.c.

234 {
235  return p->nSize;
236 }
Msat_IntVec_t_::nSize
int nSize
Definition: msatInt.h:165
int* Msat_IntVecReleaseArray ( Msat_IntVec_t *  p)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 197 of file msatVec.c.

198 {
199  int * pArray = p->pArray;
200  p->nCap = 0;
201  p->nSize = 0;
202  p->pArray = NULL;
203  return pArray;
204 }
Msat_IntVec_t_::nSize
int nSize
Definition: msatInt.h:165
Msat_IntVec_t_::nCap
int nCap
Definition: msatInt.h:166
Msat_IntVec_t_::pArray
int * pArray
Definition: msatInt.h:164
void Msat_IntVecShrink ( Msat_IntVec_t *  p,
int  nSizeNew 
)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 318 of file msatVec.c.

319 {
320  assert( p->nSize >= nSizeNew );
321  p->nSize = nSizeNew;
322 }
Msat_IntVec_t_::nSize
int nSize
Definition: msatInt.h:165
assert
#define assert(ex)
Definition: util_old.h:213
void Msat_IntVecSort ( Msat_IntVec_t *  p,
int  fReverse 
)

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

Synopsis [Sorting the entries by their integer value.]

Description []

SideEffects []

SeeAlso []

Definition at line 442 of file msatVec.c.

443 {
444  if ( fReverse )
445  qsort( (void *)p->pArray, p->nSize, sizeof(int),
446  (int (*)(const void *, const void *)) Msat_IntVecSortCompare2 );
447  else
448  qsort( (void *)p->pArray, p->nSize, sizeof(int),
449  (int (*)(const void *, const void *)) Msat_IntVecSortCompare1 );
450 }
Msat_IntVec_t_::nSize
int nSize
Definition: msatInt.h:165
Msat_IntVecSortCompare2
static int Msat_IntVecSortCompare2(int *pp1, int *pp2)
Definition: msatVec.c:484
Msat_IntVec_t_::pArray
int * pArray
Definition: msatInt.h:164
Msat_IntVecSortCompare1
static ABC_NAMESPACE_IMPL_START int Msat_IntVecSortCompare1(int *pp1, int *pp2)
DECLARATIONS ///.
Definition: msatVec.c:463
int Msat_IntVecSortCompare1 ( int *  pp1,
int *  pp2 
)
static

DECLARATIONS ///.

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 alanm.nosp@m.i@ee.nosp@m.cs.be.nosp@m.rkel.nosp@m.ey.ed.nosp@m.u]

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

]

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

Synopsis [Comparison procedure for two clauses.]

Description []

SideEffects []

SeeAlso []

Definition at line 463 of file msatVec.c.

464 {
465  // for some reason commenting out lines (as shown) led to crashing of the release version
466  if ( *pp1 < *pp2 )
467  return -1;
468  if ( *pp1 > *pp2 ) //
469  return 1;
470  return 0; //
471 }
int Msat_IntVecSortCompare2 ( int *  pp1,
int *  pp2 
)
static

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

Synopsis [Comparison procedure for two clauses.]

Description []

SideEffects []

SeeAlso []

Definition at line 484 of file msatVec.c.

485 {
486  // for some reason commenting out lines (as shown) led to crashing of the release version
487  if ( *pp1 > *pp2 )
488  return -1;
489  if ( *pp1 < *pp2 ) //
490  return 1;
491  return 0; //
492 }
void Msat_IntVecWriteEntry ( Msat_IntVec_t *  p,
int  i,
int  Entry 
)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 266 of file msatVec.c.

267 {
268  assert( i >= 0 && i < p->nSize );
269  p->pArray[i] = Entry;
270 }
assert
#define assert(ex)
Definition: util_old.h:213
Msat_IntVec_t_::pArray
int * pArray
Definition: msatInt.h:164