1 /**CFile****************************************************************
2
3 FileName [msatVec.c]
4
5 PackageName [A C version of SAT solver MINISAT, originally developed
6 in C++ by Niklas Een and Niklas Sorensson, Chalmers University of
7 Technology, Sweden: http://www.cs.chalmers.se/~een/Satzoo.]
8
9 Synopsis [Integer vector borrowed from Extra.]
10
11 Author [Alan Mishchenko <alanmi@eecs.berkeley.edu>]
12
13 Affiliation [UC Berkeley]
14
15 Date [Ver. 1.0. Started - January 1, 2004.]
16
17 Revision [$Id: msatVec.c,v 1.0 2004/01/01 1:00:00 alanmi Exp $]
18
19 ***********************************************************************/
20
21 #include "msatInt.h"
22
23 ABC_NAMESPACE_IMPL_START
24
25
26 ////////////////////////////////////////////////////////////////////////
27 /// DECLARATIONS ///
28 ////////////////////////////////////////////////////////////////////////
29
30 static int Msat_IntVecSortCompare1( int * pp1, int * pp2 );
31 static int Msat_IntVecSortCompare2( int * pp1, int * pp2 );
32
33 ////////////////////////////////////////////////////////////////////////
34 /// FUNCTION DEFINITIONS ///
35 ////////////////////////////////////////////////////////////////////////
36
37 /**Function*************************************************************
38
39 Synopsis [Allocates a vector with the given capacity.]
40
41 Description []
42
43 SideEffects []
44
45 SeeAlso []
46
47 ***********************************************************************/
Msat_IntVecAlloc(int nCap)48 Msat_IntVec_t * Msat_IntVecAlloc( int nCap )
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 }
59
60 /**Function*************************************************************
61
62 Synopsis [Creates the vector from an integer array of the given size.]
63
64 Description []
65
66 SideEffects []
67
68 SeeAlso []
69
70 ***********************************************************************/
Msat_IntVecAllocArray(int * pArray,int nSize)71 Msat_IntVec_t * Msat_IntVecAllocArray( int * pArray, int nSize )
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 }
80
81 /**Function*************************************************************
82
83 Synopsis [Creates the vector from an integer array of the given size.]
84
85 Description []
86
87 SideEffects []
88
89 SeeAlso []
90
91 ***********************************************************************/
Msat_IntVecAllocArrayCopy(int * pArray,int nSize)92 Msat_IntVec_t * Msat_IntVecAllocArrayCopy( int * pArray, int nSize )
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 }
102
103 /**Function*************************************************************
104
105 Synopsis [Duplicates the integer array.]
106
107 Description []
108
109 SideEffects []
110
111 SeeAlso []
112
113 ***********************************************************************/
Msat_IntVecDup(Msat_IntVec_t * pVec)114 Msat_IntVec_t * Msat_IntVecDup( Msat_IntVec_t * pVec )
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 }
124
125 /**Function*************************************************************
126
127 Synopsis [Transfers the array into another vector.]
128
129 Description []
130
131 SideEffects []
132
133 SeeAlso []
134
135 ***********************************************************************/
Msat_IntVecDupArray(Msat_IntVec_t * pVec)136 Msat_IntVec_t * Msat_IntVecDupArray( Msat_IntVec_t * pVec )
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 }
148
149 /**Function*************************************************************
150
151 Synopsis []
152
153 Description []
154
155 SideEffects []
156
157 SeeAlso []
158
159 ***********************************************************************/
Msat_IntVecFree(Msat_IntVec_t * p)160 void Msat_IntVecFree( Msat_IntVec_t * p )
161 {
162 ABC_FREE( p->pArray );
163 ABC_FREE( p );
164 }
165
166 /**Function*************************************************************
167
168 Synopsis [Fills the vector with given number of entries.]
169
170 Description []
171
172 SideEffects []
173
174 SeeAlso []
175
176 ***********************************************************************/
Msat_IntVecFill(Msat_IntVec_t * p,int nSize,int Entry)177 void 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
186 /**Function*************************************************************
187
188 Synopsis []
189
190 Description []
191
192 SideEffects []
193
194 SeeAlso []
195
196 ***********************************************************************/
Msat_IntVecReleaseArray(Msat_IntVec_t * p)197 int * Msat_IntVecReleaseArray( Msat_IntVec_t * p )
198 {
199 int * pArray = p->pArray;
200 p->nCap = 0;
201 p->nSize = 0;
202 p->pArray = NULL;
203 return pArray;
204 }
205
206 /**Function*************************************************************
207
208 Synopsis []
209
210 Description []
211
212 SideEffects []
213
214 SeeAlso []
215
216 ***********************************************************************/
Msat_IntVecReadArray(Msat_IntVec_t * p)217 int * Msat_IntVecReadArray( Msat_IntVec_t * p )
218 {
219 return p->pArray;
220 }
221
222 /**Function*************************************************************
223
224 Synopsis []
225
226 Description []
227
228 SideEffects []
229
230 SeeAlso []
231
232 ***********************************************************************/
Msat_IntVecReadSize(Msat_IntVec_t * p)233 int Msat_IntVecReadSize( Msat_IntVec_t * p )
234 {
235 return p->nSize;
236 }
237
238 /**Function*************************************************************
239
240 Synopsis []
241
242 Description []
243
244 SideEffects []
245
246 SeeAlso []
247
248 ***********************************************************************/
Msat_IntVecReadEntry(Msat_IntVec_t * p,int i)249 int Msat_IntVecReadEntry( Msat_IntVec_t * p, int i )
250 {
251 assert( i >= 0 && i < p->nSize );
252 return p->pArray[i];
253 }
254
255 /**Function*************************************************************
256
257 Synopsis []
258
259 Description []
260
261 SideEffects []
262
263 SeeAlso []
264
265 ***********************************************************************/
Msat_IntVecWriteEntry(Msat_IntVec_t * p,int i,int Entry)266 void 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
272 /**Function*************************************************************
273
274 Synopsis []
275
276 Description []
277
278 SideEffects []
279
280 SeeAlso []
281
282 ***********************************************************************/
Msat_IntVecReadEntryLast(Msat_IntVec_t * p)283 int Msat_IntVecReadEntryLast( Msat_IntVec_t * p )
284 {
285 return p->pArray[p->nSize-1];
286 }
287
288 /**Function*************************************************************
289
290 Synopsis [Resizes the vector to the given capacity.]
291
292 Description []
293
294 SideEffects []
295
296 SeeAlso []
297
298 ***********************************************************************/
Msat_IntVecGrow(Msat_IntVec_t * p,int nCapMin)299 void 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
307 /**Function*************************************************************
308
309 Synopsis []
310
311 Description []
312
313 SideEffects []
314
315 SeeAlso []
316
317 ***********************************************************************/
Msat_IntVecShrink(Msat_IntVec_t * p,int nSizeNew)318 void Msat_IntVecShrink( Msat_IntVec_t * p, int nSizeNew )
319 {
320 assert( p->nSize >= nSizeNew );
321 p->nSize = nSizeNew;
322 }
323
324 /**Function*************************************************************
325
326 Synopsis []
327
328 Description []
329
330 SideEffects []
331
332 SeeAlso []
333
334 ***********************************************************************/
Msat_IntVecClear(Msat_IntVec_t * p)335 void Msat_IntVecClear( Msat_IntVec_t * p )
336 {
337 p->nSize = 0;
338 }
339
340 /**Function*************************************************************
341
342 Synopsis []
343
344 Description []
345
346 SideEffects []
347
348 SeeAlso []
349
350 ***********************************************************************/
Msat_IntVecPush(Msat_IntVec_t * p,int Entry)351 void 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
363 /**Function*************************************************************
364
365 Synopsis [Add the element while ensuring uniqueness.]
366
367 Description [Returns 1 if the element was found, and 0 if it was new. ]
368
369 SideEffects []
370
371 SeeAlso []
372
373 ***********************************************************************/
Msat_IntVecPushUnique(Msat_IntVec_t * p,int Entry)374 int Msat_IntVecPushUnique( Msat_IntVec_t * p, int Entry )
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
384 /**Function*************************************************************
385
386 Synopsis [Inserts the element while sorting in the increasing order.]
387
388 Description []
389
390 SideEffects []
391
392 SeeAlso []
393
394 ***********************************************************************/
Msat_IntVecPushUniqueOrder(Msat_IntVec_t * p,int Entry,int fIncrease)395 void 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
414 /**Function*************************************************************
415
416 Synopsis [Returns the last entry and removes it from the list.]
417
418 Description []
419
420 SideEffects []
421
422 SeeAlso []
423
424 ***********************************************************************/
Msat_IntVecPop(Msat_IntVec_t * p)425 int Msat_IntVecPop( Msat_IntVec_t * p )
426 {
427 assert( p->nSize > 0 );
428 return p->pArray[--p->nSize];
429 }
430
431 /**Function*************************************************************
432
433 Synopsis [Sorting the entries by their integer value.]
434
435 Description []
436
437 SideEffects []
438
439 SeeAlso []
440
441 ***********************************************************************/
Msat_IntVecSort(Msat_IntVec_t * p,int fReverse)442 void 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
452 /**Function*************************************************************
453
454 Synopsis [Comparison procedure for two clauses.]
455
456 Description []
457
458 SideEffects []
459
460 SeeAlso []
461
462 ***********************************************************************/
Msat_IntVecSortCompare1(int * pp1,int * pp2)463 int 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
473 /**Function*************************************************************
474
475 Synopsis [Comparison procedure for two clauses.]
476
477 Description []
478
479 SideEffects []
480
481 SeeAlso []
482
483 ***********************************************************************/
Msat_IntVecSortCompare2(int * pp1,int * pp2)484 int 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
494 ////////////////////////////////////////////////////////////////////////
495 /// END OF FILE ///
496 ////////////////////////////////////////////////////////////////////////
497
498
499 ABC_NAMESPACE_IMPL_END
500
501