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 ***********************************************************************/
Msat_ClauseVecAlloc(int nCap)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 ***********************************************************************/
Msat_ClauseVecFree(Msat_ClauseVec_t * p)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 ***********************************************************************/
Msat_ClauseVecReadArray(Msat_ClauseVec_t * p)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 ***********************************************************************/
Msat_ClauseVecReadSize(Msat_ClauseVec_t * p)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 ***********************************************************************/
Msat_ClauseVecGrow(Msat_ClauseVec_t * p,int nCapMin)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 ***********************************************************************/
Msat_ClauseVecShrink(Msat_ClauseVec_t * p,int nSizeNew)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 ***********************************************************************/
Msat_ClauseVecClear(Msat_ClauseVec_t * p)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 ***********************************************************************/
Msat_ClauseVecPush(Msat_ClauseVec_t * p,Msat_Clause_t * Entry)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 ***********************************************************************/
Msat_ClauseVecPop(Msat_ClauseVec_t * p)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 ***********************************************************************/
Msat_ClauseVecWriteEntry(Msat_ClauseVec_t * p,int i,Msat_Clause_t * Entry)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 ***********************************************************************/
Msat_ClauseVecReadEntry(Msat_ClauseVec_t * p,int i)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
238