ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
msatVec.c
Go to the documentation of this file.
1
20
21#include "msatInt.h"
22
24
25
29
30static int Msat_IntVecSortCompare1( int * pp1, int * pp2 );
31static int Msat_IntVecSortCompare2( int * pp1, int * pp2 );
32
36
49{
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}
59
71Msat_IntVec_t * Msat_IntVecAllocArray( int * pArray, int nSize )
72{
75 p->nSize = nSize;
76 p->nCap = nSize;
77 p->pArray = pArray;
78 return p;
79}
80
92Msat_IntVec_t * Msat_IntVecAllocArrayCopy( int * pArray, int nSize )
93{
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}
102
115{
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}
124
137{
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}
148
161{
162 ABC_FREE( p->pArray );
163 ABC_FREE( p );
164}
165
177void Msat_IntVecFill( Msat_IntVec_t * p, int nSize, int Entry )
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}
185
198{
199 int * pArray = p->pArray;
200 p->nCap = 0;
201 p->nSize = 0;
202 p->pArray = NULL;
203 return pArray;
204}
205
218{
219 return p->pArray;
220}
221
234{
235 return p->nSize;
236}
237
250{
251 assert( i >= 0 && i < p->nSize );
252 return p->pArray[i];
253}
254
266void Msat_IntVecWriteEntry( Msat_IntVec_t * p, int i, int Entry )
267{
268 assert( i >= 0 && i < p->nSize );
269 p->pArray[i] = Entry;
270}
271
284{
285 return p->pArray[p->nSize-1];
286}
287
299void Msat_IntVecGrow( Msat_IntVec_t * p, int nCapMin )
300{
301 if ( p->nCap >= nCapMin )
302 return;
303 p->pArray = ABC_REALLOC( int, p->pArray, nCapMin );
304 p->nCap = nCapMin;
305}
306
318void Msat_IntVecShrink( Msat_IntVec_t * p, int nSizeNew )
319{
320 assert( p->nSize >= nSizeNew );
321 p->nSize = nSizeNew;
322}
323
336{
337 p->nSize = 0;
338}
339
351void Msat_IntVecPush( Msat_IntVec_t * p, int Entry )
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}
362
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}
383
395void Msat_IntVecPushUniqueOrder( Msat_IntVec_t * p, int Entry, int fIncrease )
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}
412
413
426{
427 assert( p->nSize > 0 );
428 return p->pArray[--p->nSize];
429}
430
442void Msat_IntVecSort( Msat_IntVec_t * p, int fReverse )
443{
444 if ( fReverse )
445 qsort( (void *)p->pArray, (size_t)p->nSize, sizeof(int),
446 (int (*)(const void *, const void *)) Msat_IntVecSortCompare2 );
447 else
448 qsort( (void *)p->pArray, (size_t)p->nSize, sizeof(int),
449 (int (*)(const void *, const void *)) Msat_IntVecSortCompare1 );
450}
451
463int Msat_IntVecSortCompare1( int * pp1, int * pp2 )
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}
472
484int Msat_IntVecSortCompare2( int * pp1, int * pp2 )
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}
493
497
498
500
#define ABC_ALLOC(type, num)
Definition abc_global.h:264
#define ABC_REALLOC(type, obj, num)
Definition abc_global.h:268
#define ABC_FREE(obj)
Definition abc_global.h:267
#define ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_END
Cube * p
Definition exorList.c:222
void Msat_IntVecGrow(Msat_IntVec_t *p, int nCapMin)
Definition msatVec.c:299
Msat_IntVec_t * Msat_IntVecAllocArray(int *pArray, int nSize)
Definition msatVec.c:71
int Msat_IntVecPop(Msat_IntVec_t *p)
Definition msatVec.c:425
Msat_IntVec_t * Msat_IntVecAllocArrayCopy(int *pArray, int nSize)
Definition msatVec.c:92
int Msat_IntVecPushUnique(Msat_IntVec_t *p, int Entry)
Definition msatVec.c:374
void Msat_IntVecPushUniqueOrder(Msat_IntVec_t *p, int Entry, int fIncrease)
Definition msatVec.c:395
int Msat_IntVecReadEntryLast(Msat_IntVec_t *p)
Definition msatVec.c:283
int Msat_IntVecReadEntry(Msat_IntVec_t *p, int i)
Definition msatVec.c:249
void Msat_IntVecSort(Msat_IntVec_t *p, int fReverse)
Definition msatVec.c:442
Msat_IntVec_t * Msat_IntVecAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition msatVec.c:48
Msat_IntVec_t * Msat_IntVecDup(Msat_IntVec_t *pVec)
Definition msatVec.c:114
Msat_IntVec_t * Msat_IntVecDupArray(Msat_IntVec_t *pVec)
Definition msatVec.c:136
int * Msat_IntVecReleaseArray(Msat_IntVec_t *p)
Definition msatVec.c:197
void Msat_IntVecFill(Msat_IntVec_t *p, int nSize, int Entry)
Definition msatVec.c:177
void Msat_IntVecShrink(Msat_IntVec_t *p, int nSizeNew)
Definition msatVec.c:318
void Msat_IntVecFree(Msat_IntVec_t *p)
Definition msatVec.c:160
void Msat_IntVecWriteEntry(Msat_IntVec_t *p, int i, int Entry)
Definition msatVec.c:266
int Msat_IntVecReadSize(Msat_IntVec_t *p)
Definition msatVec.c:233
void Msat_IntVecClear(Msat_IntVec_t *p)
Definition msatVec.c:335
void Msat_IntVecPush(Msat_IntVec_t *p, int Entry)
Definition msatVec.c:351
int * Msat_IntVecReadArray(Msat_IntVec_t *p)
Definition msatVec.c:217
struct Msat_IntVec_t_ Msat_IntVec_t
Definition msat.h:45
#define assert(ex)
Definition util_old.h:213
char * memcpy()