abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
msatClauseVec.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [msatClauseVec.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 [Procedures working with arrays of SAT clauses.]
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: msatClauseVec.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 ////////////////////////////////////////////////////////////////////////
31 /// FUNCTION DEFINITIONS ///
32 ////////////////////////////////////////////////////////////////////////
33 
34 /**Function*************************************************************
35 
36  Synopsis [Allocates a vector with the given capacity.]
37 
38  Description []
39 
40  SideEffects []
41 
42  SeeAlso []
43 
44 ***********************************************************************/
45 Msat_ClauseVec_t * Msat_ClauseVecAlloc( int nCap )
46 {
47  Msat_ClauseVec_t * p;
48  p = ABC_ALLOC( Msat_ClauseVec_t, 1 );
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 
57 /**Function*************************************************************
58 
59  Synopsis []
60 
61  Description []
62 
63  SideEffects []
64 
65  SeeAlso []
66 
67 ***********************************************************************/
68 void Msat_ClauseVecFree( Msat_ClauseVec_t * p )
69 {
70  ABC_FREE( p->pArray );
71  ABC_FREE( p );
72 }
73 
74 /**Function*************************************************************
75 
76  Synopsis []
77 
78  Description []
79 
80  SideEffects []
81 
82  SeeAlso []
83 
84 ***********************************************************************/
85 Msat_Clause_t ** Msat_ClauseVecReadArray( Msat_ClauseVec_t * p )
86 {
87  return p->pArray;
88 }
89 
90 /**Function*************************************************************
91 
92  Synopsis []
93 
94  Description []
95 
96  SideEffects []
97 
98  SeeAlso []
99 
100 ***********************************************************************/
101 int Msat_ClauseVecReadSize( Msat_ClauseVec_t * p )
102 {
103  return p->nSize;
104 }
105 
106 /**Function*************************************************************
107 
108  Synopsis [Resizes the vector to the given capacity.]
109 
110  Description []
111 
112  SideEffects []
113 
114  SeeAlso []
115 
116 ***********************************************************************/
117 void Msat_ClauseVecGrow( Msat_ClauseVec_t * p, int nCapMin )
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 
125 /**Function*************************************************************
126 
127  Synopsis []
128 
129  Description []
130 
131  SideEffects []
132 
133  SeeAlso []
134 
135 ***********************************************************************/
136 void Msat_ClauseVecShrink( Msat_ClauseVec_t * p, int nSizeNew )
137 {
138  assert( p->nSize >= nSizeNew );
139  p->nSize = nSizeNew;
140 }
141 
142 /**Function*************************************************************
143 
144  Synopsis []
145 
146  Description []
147 
148  SideEffects []
149 
150  SeeAlso []
151 
152 ***********************************************************************/
153 void Msat_ClauseVecClear( Msat_ClauseVec_t * p )
154 {
155  p->nSize = 0;
156 }
157 
158 /**Function*************************************************************
159 
160  Synopsis []
161 
162  Description []
163 
164  SideEffects []
165 
166  SeeAlso []
167 
168 ***********************************************************************/
169 void Msat_ClauseVecPush( Msat_ClauseVec_t * p, Msat_Clause_t * Entry )
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 
181 /**Function*************************************************************
182 
183  Synopsis []
184 
185  Description []
186 
187  SideEffects []
188 
189  SeeAlso []
190 
191 ***********************************************************************/
192 Msat_Clause_t * Msat_ClauseVecPop( Msat_ClauseVec_t * p )
193 {
194  return p->pArray[--p->nSize];
195 }
196 
197 /**Function*************************************************************
198 
199  Synopsis []
200 
201  Description []
202 
203  SideEffects []
204 
205  SeeAlso []
206 
207 ***********************************************************************/
208 void Msat_ClauseVecWriteEntry( Msat_ClauseVec_t * p, int i, Msat_Clause_t * Entry )
209 {
210  assert( i >= 0 && i < p->nSize );
211  p->pArray[i] = Entry;
212 }
213 
214 /**Function*************************************************************
215 
216  Synopsis []
217 
218  Description []
219 
220  SideEffects []
221 
222  SeeAlso []
223 
224 ***********************************************************************/
225 Msat_Clause_t * Msat_ClauseVecReadEntry( Msat_ClauseVec_t * p, int i )
226 {
227  assert( i >= 0 && i < p->nSize );
228  return p->pArray[i];
229 }
230 
231 ////////////////////////////////////////////////////////////////////////
232 /// END OF FILE ///
233 ////////////////////////////////////////////////////////////////////////
234 
235 
236 ABC_NAMESPACE_IMPL_END
237 
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Msat_ClauseVecReadEntry
Msat_Clause_t * Msat_ClauseVecReadEntry(Msat_ClauseVec_t *p, int i)
Definition: msatClauseVec.c:225
ABC_REALLOC
#define ABC_REALLOC(type, obj, num)
Definition: abc_global.h:233
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
Msat_Clause_t
typedefABC_NAMESPACE_HEADER_START struct Msat_Clause_t_ Msat_Clause_t
INCLUDES ///.
Definition: msatInt.h:57
Msat_ClauseVecReadSize
int Msat_ClauseVecReadSize(Msat_ClauseVec_t *p)
Definition: msatClauseVec.c:101
Msat_ClauseVecShrink
void Msat_ClauseVecShrink(Msat_ClauseVec_t *p, int nSizeNew)
Definition: msatClauseVec.c:136
Msat_ClauseVecGrow
void Msat_ClauseVecGrow(Msat_ClauseVec_t *p, int nCapMin)
Definition: msatClauseVec.c:117
Msat_ClauseVecReadArray
Msat_Clause_t ** Msat_ClauseVecReadArray(Msat_ClauseVec_t *p)
Definition: msatClauseVec.c:85
Msat_ClauseVecPush
void Msat_ClauseVecPush(Msat_ClauseVec_t *p, Msat_Clause_t *Entry)
Definition: msatClauseVec.c:169
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
Msat_ClauseVec_t_::nSize
int nSize
Definition: msatInt.h:158
Msat_ClauseVecClear
void Msat_ClauseVecClear(Msat_ClauseVec_t *p)
Definition: msatClauseVec.c:153
Msat_ClauseVecPop
Msat_Clause_t * Msat_ClauseVecPop(Msat_ClauseVec_t *p)
Definition: msatClauseVec.c:192
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
ABC_FREE
#define ABC_FREE(obj)
Definition: abc_global.h:232
Msat_ClauseVec_t_::pArray
Msat_Clause_t ** pArray
Definition: msatInt.h:157
Msat_ClauseVecAlloc
ABC_NAMESPACE_IMPL_START Msat_ClauseVec_t * Msat_ClauseVecAlloc(int nCap)
DECLARATIONS ///.
Definition: msatClauseVec.c:45
assert
#define assert(ex)
Definition: util_old.h:213
Msat_ClauseVec_t_::nCap
int nCap
Definition: msatInt.h:159
Msat_ClauseVec_t_
Definition: msatInt.h:155
Msat_ClauseVecWriteEntry
void Msat_ClauseVecWriteEntry(Msat_ClauseVec_t *p, int i, Msat_Clause_t *Entry)
Definition: msatClauseVec.c:208
Msat_ClauseVecFree
void Msat_ClauseVecFree(Msat_ClauseVec_t *p)
Definition: msatClauseVec.c:68