ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
msatClauseVec.c
Go to the documentation of this file.
1
20
21#include "msatInt.h"
22
24
25
29
33
46{
49 if ( nCap > 0 && nCap < 16 )
50 nCap = 16;
51 p->nSize = 0;
52 p->nCap = nCap;
53 p->pArray = p->nCap? ABC_ALLOC( Msat_Clause_t *, p->nCap ) : NULL;
54 return p;
55}
56
69{
70 ABC_FREE( p->pArray );
71 ABC_FREE( p );
72}
73
86{
87 return p->pArray;
88}
89
102{
103 return p->nSize;
104}
105
118{
119 if ( p->nCap >= nCapMin )
120 return;
121 p->pArray = ABC_REALLOC( Msat_Clause_t *, p->pArray, nCapMin );
122 p->nCap = nCapMin;
123}
124
137{
138 assert( p->nSize >= nSizeNew );
139 p->nSize = nSizeNew;
140}
141
154{
155 p->nSize = 0;
156}
157
170{
171 if ( p->nSize == p->nCap )
172 {
173 if ( p->nCap < 16 )
174 Msat_ClauseVecGrow( p, 16 );
175 else
176 Msat_ClauseVecGrow( p, 2 * p->nCap );
177 }
178 p->pArray[p->nSize++] = Entry;
179}
180
193{
194 return p->pArray[--p->nSize];
195}
196
209{
210 assert( i >= 0 && i < p->nSize );
211 p->pArray[i] = Entry;
212}
213
226{
227 assert( i >= 0 && i < p->nSize );
228 return p->pArray[i];
229}
230
234
235
237
#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_ClauseVecWriteEntry(Msat_ClauseVec_t *p, int i, Msat_Clause_t *Entry)
void Msat_ClauseVecClear(Msat_ClauseVec_t *p)
void Msat_ClauseVecFree(Msat_ClauseVec_t *p)
ABC_NAMESPACE_IMPL_START Msat_ClauseVec_t * Msat_ClauseVecAlloc(int nCap)
DECLARATIONS ///.
void Msat_ClauseVecGrow(Msat_ClauseVec_t *p, int nCapMin)
Msat_Clause_t * Msat_ClauseVecReadEntry(Msat_ClauseVec_t *p, int i)
int Msat_ClauseVecReadSize(Msat_ClauseVec_t *p)
Msat_Clause_t ** Msat_ClauseVecReadArray(Msat_ClauseVec_t *p)
Msat_Clause_t * Msat_ClauseVecPop(Msat_ClauseVec_t *p)
void Msat_ClauseVecPush(Msat_ClauseVec_t *p, Msat_Clause_t *Entry)
void Msat_ClauseVecShrink(Msat_ClauseVec_t *p, int nSizeNew)
typedefABC_NAMESPACE_HEADER_START struct Msat_Clause_t_ Msat_Clause_t
INCLUDES ///.
Definition msatInt.h:57
struct Msat_ClauseVec_t_ Msat_ClauseVec_t
Definition msat.h:46
#define assert(ex)
Definition util_old.h:213