1 /**CFile****************************************************************
2
3 FileName [satMem.h]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [SAT solver.]
8
9 Synopsis [Memory management.]
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: satMem.h,v 1.0 2004/01/01 1:00:00 alanmi Exp $]
18
19 ***********************************************************************/
20
21 #ifndef ABC__sat__bsat__satMem_h
22 #define ABC__sat__bsat__satMem_h
23
24 ////////////////////////////////////////////////////////////////////////
25 /// INCLUDES ///
26 ////////////////////////////////////////////////////////////////////////
27
28 #include "misc/util/abc_global.h"
29
30 ABC_NAMESPACE_HEADER_START
31
32 ////////////////////////////////////////////////////////////////////////
33 /// PARAMETERS ///
34 ////////////////////////////////////////////////////////////////////////
35
36 //#define LEARNT_MAX_START_DEFAULT 0
37 #define LEARNT_MAX_START_DEFAULT 10000
38 #define LEARNT_MAX_INCRE_DEFAULT 1000
39 #define LEARNT_MAX_RATIO_DEFAULT 50
40
41 ////////////////////////////////////////////////////////////////////////
42 /// STRUCTURE DEFINITIONS ///
43 ////////////////////////////////////////////////////////////////////////
44
45 //=================================================================================================
46 // Clause datatype + minor functions:
47
48 typedef struct clause_t clause;
49 struct clause_t
50 {
51 unsigned lrn : 1;
52 unsigned mark : 1;
53 unsigned partA : 1;
54 unsigned lbd : 8;
55 unsigned size : 21;
56 lit lits[0];
57 };
58
59 // learned clauses have "hidden" literal (c->lits[c->size]) to store clause ID
60
61 // data-structure for logging entries
62 // memory is allocated in 2^nPageSize word-sized pages
63 // the first 'word' of each page are stores the word limit
64
65 // although clause memory pieces are aligned to 64-bit words
66 // the integer clause handles are in terms of 32-bit unsigneds
67 // allowing for the first bit to be used for labeling 2-lit clauses
68
69
70 typedef struct Sat_Mem_t_ Sat_Mem_t;
71 struct Sat_Mem_t_
72 {
73 int nEntries[2]; // entry count
74 int BookMarkH[2]; // bookmarks for handles
75 int BookMarkE[2]; // bookmarks for entries
76 int iPage[2]; // current memory page
77 int nPageSize; // page log size in terms of ints
78 unsigned uPageMask; // page mask
79 unsigned uLearnedMask; // learned mask
80 int nPagesAlloc; // page count allocated
81 int ** pPages; // page pointers
82 };
83
Sat_MemLimit(int * p)84 static inline int Sat_MemLimit( int * p ) { return p[0]; }
Sat_MemIncLimit(int * p,int nInts)85 static inline int Sat_MemIncLimit( int * p, int nInts ) { return p[0] += nInts; }
Sat_MemWriteLimit(int * p,int nInts)86 static inline void Sat_MemWriteLimit( int * p, int nInts ) { p[0] = nInts; }
87
Sat_MemHandPage(Sat_Mem_t * p,cla h)88 static inline int Sat_MemHandPage( Sat_Mem_t * p, cla h ) { return h >> p->nPageSize; }
Sat_MemHandShift(Sat_Mem_t * p,cla h)89 static inline int Sat_MemHandShift( Sat_Mem_t * p, cla h ) { return h & p->uPageMask; }
90
Sat_MemIntSize(int size,int lrn)91 static inline int Sat_MemIntSize( int size, int lrn ) { return (size + 2 + lrn) & ~01; }
Sat_MemClauseSize(clause * p)92 static inline int Sat_MemClauseSize( clause * p ) { return Sat_MemIntSize(p->size, p->lrn); }
Sat_MemClauseSize2(clause * p)93 static inline int Sat_MemClauseSize2( clause * p ) { return Sat_MemIntSize(p->size, 1); }
94
95 //static inline clause * Sat_MemClause( Sat_Mem_t * p, int i, int k ) { assert(i <= p->iPage[i&1] && k <= Sat_MemLimit(p->pPages[i])); return (clause *)(p->pPages[i] + k ); }
Sat_MemClause(Sat_Mem_t * p,int i,int k)96 static inline clause * Sat_MemClause( Sat_Mem_t * p, int i, int k ) { assert( k ); return (clause *)(p->pPages[i] + k); }
97 //static inline clause * Sat_MemClauseHand( Sat_Mem_t * p, cla h ) { assert(Sat_MemHandPage(p, h) <= p->iPage[(h & p->uLearnedMask) > 0]); assert(Sat_MemHandShift(p, h) >= 2 && Sat_MemHandShift(p, h) < (int)p->uLearnedMask); return Sat_MemClause( p, Sat_MemHandPage(p, h), Sat_MemHandShift(p, h) ); }
Sat_MemClauseHand(Sat_Mem_t * p,cla h)98 static inline clause * Sat_MemClauseHand( Sat_Mem_t * p, cla h ) { return h ? Sat_MemClause( p, Sat_MemHandPage(p, h), Sat_MemHandShift(p, h) ) : NULL; }
Sat_MemEntryNum(Sat_Mem_t * p,int lrn)99 static inline int Sat_MemEntryNum( Sat_Mem_t * p, int lrn ) { return p->nEntries[lrn]; }
100
Sat_MemHand(Sat_Mem_t * p,int i,int k)101 static inline cla Sat_MemHand( Sat_Mem_t * p, int i, int k ) { return (i << p->nPageSize) | k; }
Sat_MemHandCurrent(Sat_Mem_t * p,int lrn)102 static inline cla Sat_MemHandCurrent( Sat_Mem_t * p, int lrn ) { return (p->iPage[lrn] << p->nPageSize) | Sat_MemLimit( p->pPages[p->iPage[lrn]] ); }
103
Sat_MemClauseUsed(Sat_Mem_t * p,cla h)104 static inline int Sat_MemClauseUsed( Sat_Mem_t * p, cla h ) { return h < p->BookMarkH[(h & p->uLearnedMask) > 0]; }
105
Sat_MemMemoryHand(Sat_Mem_t * p,cla h)106 static inline double Sat_MemMemoryHand( Sat_Mem_t * p, cla h ) { return 1.0 * ((Sat_MemHandPage(p, h) + 2)/2 * (1 << (p->nPageSize+2)) + Sat_MemHandShift(p, h) * 4); }
Sat_MemMemoryUsed(Sat_Mem_t * p,int lrn)107 static inline double Sat_MemMemoryUsed( Sat_Mem_t * p, int lrn ) { return Sat_MemMemoryHand( p, Sat_MemHandCurrent(p, lrn) ); }
Sat_MemMemoryAllUsed(Sat_Mem_t * p)108 static inline double Sat_MemMemoryAllUsed( Sat_Mem_t * p ) { return Sat_MemMemoryUsed( p, 0 ) + Sat_MemMemoryUsed( p, 1 ); }
Sat_MemMemoryAll(Sat_Mem_t * p)109 static inline double Sat_MemMemoryAll( Sat_Mem_t * p ) { return 1.0 * (p->iPage[0] + p->iPage[1] + 2) * (1 << (p->nPageSize+2)); }
110
111 // p is memory storage
112 // c is clause pointer
113 // i is page number
114 // k is page offset
115
116 // print problem clauses NOT in proof mode
117 #define Sat_MemForEachClause( p, c, i, k ) \
118 for ( i = 0; i <= p->iPage[0]; i += 2 ) \
119 for ( k = 2; k < Sat_MemLimit(p->pPages[i]) && ((c) = Sat_MemClause( p, i, k )); k += Sat_MemClauseSize(c) ) if ( i == 0 && k == 2 ) {} else
120
121 // print problem clauses in proof mode
122 #define Sat_MemForEachClause2( p, c, i, k ) \
123 for ( i = 0; i <= p->iPage[0]; i += 2 ) \
124 for ( k = 2; k < Sat_MemLimit(p->pPages[i]) && ((c) = Sat_MemClause( p, i, k )); k += Sat_MemClauseSize2(c) ) if ( i == 0 && k == 2 ) {} else
125
126 #define Sat_MemForEachLearned( p, c, i, k ) \
127 for ( i = 1; i <= p->iPage[1]; i += 2 ) \
128 for ( k = 2; k < Sat_MemLimit(p->pPages[i]) && ((c) = Sat_MemClause( p, i, k )); k += Sat_MemClauseSize(c) )
129
130 ////////////////////////////////////////////////////////////////////////
131 /// GLOBAL VARIABLES ///
132 ////////////////////////////////////////////////////////////////////////
133
134 ////////////////////////////////////////////////////////////////////////
135 /// MACRO DEFINITIONS ///
136 ////////////////////////////////////////////////////////////////////////
137
clause_from_lit(lit l)138 static inline int clause_from_lit( lit l ) { return l + l + 1; }
clause_is_lit(cla h)139 static inline int clause_is_lit( cla h ) { return (h & 1); }
clause_read_lit(cla h)140 static inline lit clause_read_lit( cla h ) { return (lit)(h >> 1); }
141
clause_learnt_h(Sat_Mem_t * p,cla h)142 static inline int clause_learnt_h( Sat_Mem_t * p, cla h ) { return (h & p->uLearnedMask) > 0; }
clause_learnt(clause * c)143 static inline int clause_learnt( clause * c ) { return c->lrn; }
clause_id(clause * c)144 static inline int clause_id( clause * c ) { return c->lits[c->size]; }
clause_set_id(clause * c,int id)145 static inline void clause_set_id( clause * c, int id ) { c->lits[c->size] = id; }
clause_size(clause * c)146 static inline int clause_size( clause * c ) { return c->size; }
clause_begin(clause * c)147 static inline lit * clause_begin( clause * c ) { return c->lits; }
clause_end(clause * c)148 static inline lit * clause_end( clause * c ) { return c->lits + c->size; }
clause_print_(clause * c)149 static inline void clause_print_( clause * c )
150 {
151 int i;
152 printf( "{ " );
153 for ( i = 0; i < clause_size(c); i++ )
154 printf( "%d ", (clause_begin(c)[i] & 1)? -(clause_begin(c)[i] >> 1) : clause_begin(c)[i] >> 1 );
155 printf( "}\n" );
156 }
157
158 ////////////////////////////////////////////////////////////////////////
159 /// FUNCTION DECLARATIONS ///
160 ////////////////////////////////////////////////////////////////////////
161
162 /**Function*************************************************************
163
164 Synopsis [Allocating vector.]
165
166 Description []
167
168 SideEffects []
169
170 SeeAlso []
171
172 ***********************************************************************/
Sat_MemCountL(Sat_Mem_t * p)173 static inline int Sat_MemCountL( Sat_Mem_t * p )
174 {
175 clause * c;
176 int i, k, Count = 0;
177 Sat_MemForEachLearned( p, c, i, k )
178 Count++;
179 return Count;
180 }
181
182 /**Function*************************************************************
183
184 Synopsis [Allocating vector.]
185
186 Description []
187
188 SideEffects []
189
190 SeeAlso []
191
192 ***********************************************************************/
Sat_MemAlloc_(Sat_Mem_t * p,int nPageSize)193 static inline void Sat_MemAlloc_( Sat_Mem_t * p, int nPageSize )
194 {
195 assert( nPageSize > 8 && nPageSize < 32 );
196 memset( p, 0, sizeof(Sat_Mem_t) );
197 p->nPageSize = nPageSize;
198 p->uLearnedMask = (unsigned)(1 << nPageSize);
199 p->uPageMask = (unsigned)((1 << nPageSize) - 1);
200 p->nPagesAlloc = 256;
201 p->pPages = ABC_CALLOC( int *, p->nPagesAlloc );
202 p->pPages[0] = ABC_ALLOC( int, (int)(((word)1) << p->nPageSize) );
203 p->pPages[1] = ABC_ALLOC( int, (int)(((word)1) << p->nPageSize) );
204 p->iPage[0] = 0;
205 p->iPage[1] = 1;
206 Sat_MemWriteLimit( p->pPages[0], 2 );
207 Sat_MemWriteLimit( p->pPages[1], 2 );
208 }
Sat_MemAlloc(int nPageSize)209 static inline Sat_Mem_t * Sat_MemAlloc( int nPageSize )
210 {
211 Sat_Mem_t * p;
212 p = ABC_CALLOC( Sat_Mem_t, 1 );
213 Sat_MemAlloc_( p, nPageSize );
214 return p;
215 }
216
217 /**Function*************************************************************
218
219 Synopsis [Resetting vector.]
220
221 Description []
222
223 SideEffects []
224
225 SeeAlso []
226
227 ***********************************************************************/
Sat_MemRestart(Sat_Mem_t * p)228 static inline void Sat_MemRestart( Sat_Mem_t * p )
229 {
230 p->nEntries[0] = 0;
231 p->nEntries[1] = 0;
232 p->iPage[0] = 0;
233 p->iPage[1] = 1;
234 Sat_MemWriteLimit( p->pPages[0], 2 );
235 Sat_MemWriteLimit( p->pPages[1], 2 );
236 }
237
238 /**Function*************************************************************
239
240 Synopsis [Sets the bookmark.]
241
242 Description []
243
244 SideEffects []
245
246 SeeAlso []
247
248 ***********************************************************************/
Sat_MemBookMark(Sat_Mem_t * p)249 static inline void Sat_MemBookMark( Sat_Mem_t * p )
250 {
251 p->BookMarkE[0] = p->nEntries[0];
252 p->BookMarkE[1] = p->nEntries[1];
253 p->BookMarkH[0] = Sat_MemHandCurrent( p, 0 );
254 p->BookMarkH[1] = Sat_MemHandCurrent( p, 1 );
255 }
Sat_MemRollBack(Sat_Mem_t * p)256 static inline void Sat_MemRollBack( Sat_Mem_t * p )
257 {
258 p->nEntries[0] = p->BookMarkE[0];
259 p->nEntries[1] = p->BookMarkE[1];
260 p->iPage[0] = Sat_MemHandPage( p, p->BookMarkH[0] );
261 p->iPage[1] = Sat_MemHandPage( p, p->BookMarkH[1] );
262 Sat_MemWriteLimit( p->pPages[p->iPage[0]], Sat_MemHandShift( p, p->BookMarkH[0] ) );
263 Sat_MemWriteLimit( p->pPages[p->iPage[1]], Sat_MemHandShift( p, p->BookMarkH[1] ) );
264 }
265
266 /**Function*************************************************************
267
268 Synopsis [Freeing vector.]
269
270 Description []
271
272 SideEffects []
273
274 SeeAlso []
275
276 ***********************************************************************/
Sat_MemFree_(Sat_Mem_t * p)277 static inline void Sat_MemFree_( Sat_Mem_t * p )
278 {
279 int i;
280 for ( i = 0; i < p->nPagesAlloc; i++ )
281 ABC_FREE( p->pPages[i] );
282 ABC_FREE( p->pPages );
283 }
Sat_MemFree(Sat_Mem_t * p)284 static inline void Sat_MemFree( Sat_Mem_t * p )
285 {
286 Sat_MemFree_( p );
287 ABC_FREE( p );
288 }
289
290 /**Function*************************************************************
291
292 Synopsis [Creates new clause.]
293
294 Description [The resulting clause is fully initialized.]
295
296 SideEffects []
297
298 SeeAlso []
299
300 ***********************************************************************/
Sat_MemAppend(Sat_Mem_t * p,int * pArray,int nSize,int lrn,int fPlus1)301 static inline int Sat_MemAppend( Sat_Mem_t * p, int * pArray, int nSize, int lrn, int fPlus1 )
302 {
303 clause * c;
304 int * pPage = p->pPages[p->iPage[lrn]];
305 int nInts = Sat_MemIntSize( nSize, lrn | fPlus1 );
306 assert( nInts + 3 < (1 << p->nPageSize) );
307 // need two extra at the begining of the page and one extra in the end
308 if ( Sat_MemLimit(pPage) + nInts + 2 >= (1 << p->nPageSize) )
309 {
310 p->iPage[lrn] += 2;
311 if ( p->iPage[lrn] >= p->nPagesAlloc )
312 {
313 p->pPages = ABC_REALLOC( int *, p->pPages, p->nPagesAlloc * 2 );
314 memset( p->pPages + p->nPagesAlloc, 0, sizeof(int *) * p->nPagesAlloc );
315 p->nPagesAlloc *= 2;
316 }
317 if ( p->pPages[p->iPage[lrn]] == NULL )
318 p->pPages[p->iPage[lrn]] = ABC_ALLOC( int, (int)(((word)1) << p->nPageSize) );
319 pPage = p->pPages[p->iPage[lrn]];
320 Sat_MemWriteLimit( pPage, 2 );
321 }
322 pPage[Sat_MemLimit(pPage)] = 0;
323 c = (clause *)(pPage + Sat_MemLimit(pPage));
324 c->size = nSize;
325 c->lrn = lrn;
326 if ( pArray )
327 memcpy( c->lits, pArray, sizeof(int) * nSize );
328 if ( lrn | fPlus1 )
329 c->lits[c->size] = p->nEntries[lrn];
330 p->nEntries[lrn]++;
331 Sat_MemIncLimit( pPage, nInts );
332 return Sat_MemHandCurrent(p, lrn) - nInts;
333 }
334
335 /**Function*************************************************************
336
337 Synopsis [Shrinking vector size.]
338
339 Description []
340
341 SideEffects [This procedure does not update the number of entries.]
342
343 SeeAlso []
344
345 ***********************************************************************/
Sat_MemShrink(Sat_Mem_t * p,int h,int lrn)346 static inline void Sat_MemShrink( Sat_Mem_t * p, int h, int lrn )
347 {
348 assert( clause_learnt_h(p, h) == lrn );
349 assert( h && h <= Sat_MemHandCurrent(p, lrn) );
350 p->iPage[lrn] = Sat_MemHandPage(p, h);
351 Sat_MemWriteLimit( p->pPages[p->iPage[lrn]], Sat_MemHandShift(p, h) );
352 }
353
354
355 /**Function*************************************************************
356
357 Synopsis [Compacts learned clauses by removing marked entries.]
358
359 Description [Returns the number of remaining entries.]
360
361 SideEffects []
362
363 SeeAlso []
364
365 ***********************************************************************/
Sat_MemCompactLearned(Sat_Mem_t * p,int fDoMove)366 static inline int Sat_MemCompactLearned( Sat_Mem_t * p, int fDoMove )
367 {
368 clause * c, * cPivot = NULL;
369 int i, k, iNew = 1, kNew = 2, nInts, fStartLooking, Counter = 0;
370 int hLimit = Sat_MemHandCurrent(p, 1);
371 if ( hLimit == Sat_MemHand(p, 1, 2) )
372 return 0;
373 if ( fDoMove && p->BookMarkH[1] )
374 {
375 // move the pivot
376 assert( p->BookMarkH[1] >= Sat_MemHand(p, 1, 2) && p->BookMarkH[1] <= hLimit );
377 // get the pivot and remember it may be pointed offlimit
378 cPivot = Sat_MemClauseHand( p, p->BookMarkH[1] );
379 if ( p->BookMarkH[1] < hLimit && !cPivot->mark )
380 {
381 p->BookMarkH[1] = cPivot->lits[cPivot->size];
382 cPivot = NULL;
383 }
384 // else find the next used clause after cPivot
385 }
386 // iterate through the learned clauses
387 fStartLooking = 0;
388 Sat_MemForEachLearned( p, c, i, k )
389 {
390 assert( c->lrn );
391 // skip marked entry
392 if ( c->mark )
393 {
394 // if pivot is a marked clause, start looking for the next non-marked one
395 if ( cPivot && cPivot == c )
396 {
397 fStartLooking = 1;
398 cPivot = NULL;
399 }
400 continue;
401 }
402 // if we started looking before, we found it!
403 if ( fStartLooking )
404 {
405 fStartLooking = 0;
406 p->BookMarkH[1] = c->lits[c->size];
407 }
408 // compute entry size
409 nInts = Sat_MemClauseSize(c);
410 assert( !(nInts & 1) );
411 // check if we need to scroll to the next page
412 if ( kNew + nInts >= (1 << p->nPageSize) )
413 {
414 // set the limit of the current page
415 if ( fDoMove )
416 Sat_MemWriteLimit( p->pPages[iNew], kNew );
417 // move writing position to the new page
418 iNew += 2;
419 kNew = 2;
420 }
421 if ( fDoMove )
422 {
423 // make sure the result is the same as previous dry run
424 assert( c->lits[c->size] == Sat_MemHand(p, iNew, kNew) );
425 // only copy the clause if it has changed
426 if ( i != iNew || k != kNew )
427 {
428 memmove( p->pPages[iNew] + kNew, c, sizeof(int) * nInts );
429 // c = Sat_MemClause( p, iNew, kNew ); // assersions do not hold during dry run
430 c = (clause *)(p->pPages[iNew] + kNew);
431 assert( nInts == Sat_MemClauseSize(c) );
432 }
433 // set the new ID value
434 c->lits[c->size] = Counter;
435 }
436 else // remember the address of the clause in the new location
437 c->lits[c->size] = Sat_MemHand(p, iNew, kNew);
438 // update writing position
439 kNew += nInts;
440 assert( iNew <= i && kNew < (1 << p->nPageSize) );
441 // update counter
442 Counter++;
443 }
444 if ( fDoMove )
445 {
446 // update the counter
447 p->nEntries[1] = Counter;
448 // update the page count
449 p->iPage[1] = iNew;
450 // set the limit of the last page
451 Sat_MemWriteLimit( p->pPages[iNew], kNew );
452 // check if the pivot need to be updated
453 if ( p->BookMarkH[1] )
454 {
455 if ( cPivot )
456 {
457 p->BookMarkH[1] = Sat_MemHandCurrent(p, 1);
458 p->BookMarkE[1] = p->nEntries[1];
459 }
460 else
461 p->BookMarkE[1] = clause_id(Sat_MemClauseHand( p, p->BookMarkH[1] ));
462 }
463
464 }
465 return Counter;
466 }
467
468
469 ABC_NAMESPACE_HEADER_END
470
471 #endif
472
473 ////////////////////////////////////////////////////////////////////////
474 /// END OF FILE ///
475 ////////////////////////////////////////////////////////////////////////
476
477