1 /**CFile****************************************************************
2
3 FileName [xsatMemory.h]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [xSAT - A SAT solver written in C.
8 Read the license file for more info.]
9
10 Synopsis [Memory management implementation.]
11
12 Author [Bruno Schmitt <boschmitt@inf.ufrgs.br>]
13
14 Affiliation [UC Berkeley / UFRGS]
15
16 Date [Ver. 1.0. Started - November 10, 2016.]
17
18 Revision []
19
20 ***********************************************************************/
21 #ifndef ABC__sat__xSAT__xsatMemory_h
22 #define ABC__sat__xSAT__xsatMemory_h
23
24 ////////////////////////////////////////////////////////////////////////
25 /// INCLUDES ///
26 ////////////////////////////////////////////////////////////////////////
27 #include "misc/util/abc_global.h"
28
29 #include "xsatClause.h"
30
31 ABC_NAMESPACE_HEADER_START
32
33 ////////////////////////////////////////////////////////////////////////
34 /// STRUCTURE DEFINITIONS ///
35 ////////////////////////////////////////////////////////////////////////
36 typedef struct xSAT_Mem_t_ xSAT_Mem_t;
37 struct xSAT_Mem_t_
38 {
39 unsigned nSize;
40 unsigned nCap;
41 unsigned nWasted;
42 unsigned * pData;
43 };
44
45 ////////////////////////////////////////////////////////////////////////
46 /// FUNCTION DECLARATIONS ///
47 ////////////////////////////////////////////////////////////////////////
48 /**Function*************************************************************
49
50 Synopsis []
51
52 Description []
53
54 SideEffects []
55
56 SeeAlso []
57
58 ***********************************************************************/
xSAT_MemClauseHand(xSAT_Mem_t * p,int h)59 static inline xSAT_Clause_t * xSAT_MemClauseHand( xSAT_Mem_t * p, int h )
60 {
61 return h != 0xFFFFFFFF ? ( xSAT_Clause_t * )( p->pData + h ) : NULL;
62 }
63
64 /**Function*************************************************************
65
66 Synopsis []
67
68 Description []
69
70 SideEffects []
71
72 SeeAlso []
73
74 ***********************************************************************/
xSAT_MemGrow(xSAT_Mem_t * p,unsigned nCap)75 static inline void xSAT_MemGrow( xSAT_Mem_t * p, unsigned nCap )
76 {
77 unsigned nPrevCap = p->nCap;
78 if ( p->nCap >= nCap )
79 return;
80 while (p->nCap < nCap)
81 {
82 unsigned delta = ( ( p->nCap >> 1 ) + ( p->nCap >> 3 ) + 2 ) & ~1;
83 p->nCap += delta;
84 assert(p->nCap >= nPrevCap);
85 }
86 assert(p->nCap > 0);
87 p->pData = ABC_REALLOC( unsigned, p->pData, p->nCap );
88 }
89
90 /**Function*************************************************************
91
92 Synopsis [Allocating vector.]
93
94 Description []
95
96 SideEffects []
97
98 SeeAlso []
99
100 ***********************************************************************/
xSAT_MemAlloc(int nCap)101 static inline xSAT_Mem_t * xSAT_MemAlloc( int nCap )
102 {
103 xSAT_Mem_t * p;
104 p = ABC_CALLOC( xSAT_Mem_t, 1 );
105 if (nCap <= 0)
106 nCap = 1024*1024;
107
108 xSAT_MemGrow(p, nCap);
109 return p;
110 }
111
112 /**Function*************************************************************
113
114 Synopsis [Resetting vector.]
115
116 Description []
117
118 SideEffects []
119
120 SeeAlso []
121
122 ***********************************************************************/
xSAT_MemRestart(xSAT_Mem_t * p)123 static inline void xSAT_MemRestart( xSAT_Mem_t * p )
124 {
125 p->nSize = 0;
126 p->nWasted = 0;
127 }
128
129 /**Function*************************************************************
130
131 Synopsis [Freeing vector.]
132
133 Description []
134
135 SideEffects []
136
137 SeeAlso []
138
139 ***********************************************************************/
xSAT_MemFree(xSAT_Mem_t * p)140 static inline void xSAT_MemFree( xSAT_Mem_t * p )
141 {
142 ABC_FREE( p->pData );
143 ABC_FREE( p );
144 }
145
146 /**Function*************************************************************
147
148 Synopsis [Creates new clause.]
149
150 Description [The resulting clause is fully initialized.]
151
152 SideEffects []
153
154 SeeAlso []
155
156 ***********************************************************************/
xSAT_MemAppend(xSAT_Mem_t * p,int nSize)157 static inline unsigned xSAT_MemAppend( xSAT_Mem_t * p, int nSize )
158 {
159 unsigned nPrevSize;
160 assert(nSize > 0);
161 xSAT_MemGrow( p, p->nSize + nSize );
162 nPrevSize = p->nSize;
163 p->nSize += nSize;
164 assert(p->nSize > nPrevSize);
165 return nPrevSize;
166 }
167
168 /**Function*************************************************************
169
170 Synopsis []
171
172 Description []
173
174 SideEffects []
175
176 SeeAlso []
177
178 ***********************************************************************/
xSAT_MemCRef(xSAT_Mem_t * p,unsigned * pC)179 static inline unsigned xSAT_MemCRef( xSAT_Mem_t * p, unsigned * pC )
180 {
181 return ( unsigned )( pC - &(p->pData[0]) );
182 }
183
184 /**Function*************************************************************
185
186 Synopsis []
187
188 Description []
189
190 SideEffects []
191
192 SeeAlso []
193
194 ***********************************************************************/
xSAT_MemCap(xSAT_Mem_t * p)195 static inline unsigned xSAT_MemCap( xSAT_Mem_t * p )
196 {
197 return p->nCap;
198 }
199
200 /**Function*************************************************************
201
202 Synopsis []
203
204 Description []
205
206 SideEffects []
207
208 SeeAlso []
209
210 ***********************************************************************/
xSAT_MemWastedCap(xSAT_Mem_t * p)211 static inline unsigned xSAT_MemWastedCap( xSAT_Mem_t * p )
212 {
213 return p->nWasted;
214 }
215
216 ABC_NAMESPACE_HEADER_END
217
218 #endif
219
220 ////////////////////////////////////////////////////////////////////////
221 /// END OF FILE ///
222 ////////////////////////////////////////////////////////////////////////
223