abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
satClause.h
Go to the documentation of this file.
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 
84 static inline int Sat_MemLimit( int * p ) { return p[0]; }
85 static inline int Sat_MemIncLimit( int * p, int nInts ) { return p[0] += nInts; }
86 static inline void Sat_MemWriteLimit( int * p, int nInts ) { p[0] = nInts; }
87 
88 static inline int Sat_MemHandPage( Sat_Mem_t * p, cla h ) { return h >> p->nPageSize; }
89 static inline int Sat_MemHandShift( Sat_Mem_t * p, cla h ) { return h & p->uPageMask; }
90 
91 static inline int Sat_MemIntSize( int size, int lrn ) { return (size + 2 + lrn) & ~01; }
92 static inline int Sat_MemClauseSize( clause * p ) { return Sat_MemIntSize(p->size, p->lrn); }
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 ); }
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) ); }
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; }
99 static inline int Sat_MemEntryNum( Sat_Mem_t * p, int lrn ) { return p->nEntries[lrn]; }
100 
101 static inline cla Sat_MemHand( Sat_Mem_t * p, int i, int k ) { return (i << p->nPageSize) | k; }
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 
104 static inline int Sat_MemClauseUsed( Sat_Mem_t * p, cla h ) { return h < p->BookMarkH[(h & p->uLearnedMask) > 0]; }
105 
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); }
107 static inline double Sat_MemMemoryUsed( Sat_Mem_t * p, int lrn ) { return Sat_MemMemoryHand( p, Sat_MemHandCurrent(p, lrn) ); }
108 static inline double Sat_MemMemoryAllUsed( Sat_Mem_t * p ) { return Sat_MemMemoryUsed( p, 0 ) + Sat_MemMemoryUsed( p, 1 ); }
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 
138 static inline int clause_from_lit( lit l ) { return l + l + 1; }
139 static inline int clause_is_lit( cla h ) { return (h & 1); }
140 static inline lit clause_read_lit( cla h ) { return (lit)(h >> 1); }
141 
142 static inline int clause_learnt_h( Sat_Mem_t * p, cla h ) { return (h & p->uLearnedMask) > 0; }
143 static inline int clause_learnt( clause * c ) { return c->lrn; }
144 static inline int clause_id( clause * c ) { return c->lits[c->size]; }
145 static inline void clause_set_id( clause * c, int id ) { c->lits[c->size] = id; }
146 static inline int clause_size( clause * c ) { return c->size; }
147 static inline lit * clause_begin( clause * c ) { return c->lits; }
148 static inline lit * clause_end( clause * c ) { return c->lits + c->size; }
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 ***********************************************************************/
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 ***********************************************************************/
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, (1 << p->nPageSize) );
203  p->pPages[1] = ABC_ALLOC( int, (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 }
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 ***********************************************************************/
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 ***********************************************************************/
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 }
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 ***********************************************************************/
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 }
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 ***********************************************************************/
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, (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 ***********************************************************************/
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 ***********************************************************************/
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 
memset
char * memset()
Sat_Mem_t_::pPages
int ** pPages
Definition: satClause.h:81
Sat_MemCountL
static int Sat_MemCountL(Sat_Mem_t *p)
FUNCTION DECLARATIONS ///.
Definition: satClause.h:173
Sat_MemMemoryAll
static double Sat_MemMemoryAll(Sat_Mem_t *p)
Definition: satClause.h:109
clause_end
static lit * clause_end(clause *c)
Definition: satClause.h:148
clause_t::lits
lit lits[0]
Definition: satClause.h:56
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
ABC_REALLOC
#define ABC_REALLOC(type, obj, num)
Definition: abc_global.h:233
clause_t::lbd
unsigned lbd
Definition: satClause.h:54
Sat_MemHandCurrent
static cla Sat_MemHandCurrent(Sat_Mem_t *p, int lrn)
Definition: satClause.h:102
Sat_MemRestart
static void Sat_MemRestart(Sat_Mem_t *p)
Definition: satClause.h:228
Sat_MemHandShift
static int Sat_MemHandShift(Sat_Mem_t *p, cla h)
Definition: satClause.h:89
memcpy
char * memcpy()
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
Sat_MemShrink
static void Sat_MemShrink(Sat_Mem_t *p, int h, int lrn)
Definition: satClause.h:346
clause_set_id
static void clause_set_id(clause *c, int id)
Definition: satClause.h:145
Sat_MemFree_
static void Sat_MemFree_(Sat_Mem_t *p)
Definition: satClause.h:277
clause_id
static int clause_id(clause *c)
Definition: satClause.h:144
Sat_MemClause
static clause * Sat_MemClause(Sat_Mem_t *p, int i, int k)
Definition: satClause.h:96
cla
int cla
Definition: satVec.h:131
lit
int lit
Definition: satVec.h:130
Sat_MemForEachLearned
#define Sat_MemForEachLearned(p, c, i, k)
Definition: satClause.h:126
clause_t
Definition: satClause.h:49
memmove
char * memmove()
clause_print
static void clause_print(clause *c)
Definition: satClause.h:149
clause_t::partA
unsigned partA
Definition: satClause.h:53
clause_size
static int clause_size(clause *c)
Definition: satClause.h:146
Sat_Mem_t_::BookMarkH
int BookMarkH[2]
Definition: satClause.h:74
clause_learnt_h
static int clause_learnt_h(Sat_Mem_t *p, cla h)
Definition: satClause.h:142
Sat_MemHandPage
static int Sat_MemHandPage(Sat_Mem_t *p, cla h)
Definition: satClause.h:88
Sat_MemIntSize
static int Sat_MemIntSize(int size, int lrn)
Definition: satClause.h:91
Sat_MemMemoryAllUsed
static double Sat_MemMemoryAllUsed(Sat_Mem_t *p)
Definition: satClause.h:108
clause_learnt
static int clause_learnt(clause *c)
Definition: satClause.h:143
clause_t::mark
unsigned mark
Definition: satClause.h:52
size
static int size
Definition: cuddSign.c:86
Counter
static int Counter
Definition: extraBddMisc.c:1877
ABC_NAMESPACE_HEADER_START
#define ABC_NAMESPACE_HEADER_START
NAMESPACES ///.
Definition: abc_global.h:105
Sat_MemLimit
static int Sat_MemLimit(int *p)
Definition: satClause.h:84
Sat_Mem_t_::uPageMask
unsigned uPageMask
Definition: satClause.h:78
Sat_MemAlloc
static Sat_Mem_t * Sat_MemAlloc(int nPageSize)
Definition: satClause.h:209
ABC_NAMESPACE_HEADER_END
#define ABC_NAMESPACE_HEADER_END
Definition: abc_global.h:106
Sat_Mem_t_::nPagesAlloc
int nPagesAlloc
Definition: satClause.h:80
Sat_MemFree
static void Sat_MemFree(Sat_Mem_t *p)
Definition: satClause.h:284
Sat_MemMemoryUsed
static double Sat_MemMemoryUsed(Sat_Mem_t *p, int lrn)
Definition: satClause.h:107
clause_is_lit
static int clause_is_lit(cla h)
Definition: satClause.h:139
abc_global.h
Sat_MemClauseHand
static clause * Sat_MemClauseHand(Sat_Mem_t *p, cla h)
Definition: satClause.h:98
clause_begin
static lit * clause_begin(clause *c)
Definition: satClause.h:147
clause_t::size
unsigned size
Definition: satClause.h:55
Sat_MemRollBack
static void Sat_MemRollBack(Sat_Mem_t *p)
Definition: satClause.h:256
clause_read_lit
static lit clause_read_lit(cla h)
Definition: satClause.h:140
ABC_FREE
#define ABC_FREE(obj)
Definition: abc_global.h:232
Sat_Mem_t_::nEntries
int nEntries[2]
Definition: satClause.h:73
ABC_CALLOC
#define ABC_CALLOC(type, num)
Definition: abc_global.h:230
clause_from_lit
static int clause_from_lit(lit l)
GLOBAL VARIABLES ///.
Definition: satClause.h:138
Sat_MemAlloc_
static void Sat_MemAlloc_(Sat_Mem_t *p, int nPageSize)
Definition: satClause.h:193
Sat_Mem_t_::BookMarkE
int BookMarkE[2]
Definition: satClause.h:75
Sat_MemIncLimit
static int Sat_MemIncLimit(int *p, int nInts)
Definition: satClause.h:85
Sat_Mem_t_::iPage
int iPage[2]
Definition: satClause.h:76
Sat_MemEntryNum
static int Sat_MemEntryNum(Sat_Mem_t *p, int lrn)
Definition: satClause.h:99
Sat_MemClauseSize
static int Sat_MemClauseSize(clause *p)
Definition: satClause.h:92
clause_t::lrn
unsigned lrn
Definition: satClause.h:51
Sat_MemAppend
static int Sat_MemAppend(Sat_Mem_t *p, int *pArray, int nSize, int lrn, int fPlus1)
Definition: satClause.h:301
assert
#define assert(ex)
Definition: util_old.h:213
Sat_MemClauseSize2
static int Sat_MemClauseSize2(clause *p)
Definition: satClause.h:93
Sat_Mem_t_::nPageSize
int nPageSize
Definition: satClause.h:77
Sat_MemClauseUsed
static int Sat_MemClauseUsed(Sat_Mem_t *p, cla h)
Definition: satClause.h:104
Sat_MemCompactLearned
static int Sat_MemCompactLearned(Sat_Mem_t *p, int fDoMove)
Definition: satClause.h:366
Sat_Mem_t_
Definition: satClause.h:71
Sat_MemWriteLimit
static void Sat_MemWriteLimit(int *p, int nInts)
Definition: satClause.h:86
Sat_Mem_t_::uLearnedMask
unsigned uLearnedMask
Definition: satClause.h:79
Sat_MemBookMark
static void Sat_MemBookMark(Sat_Mem_t *p)
Definition: satClause.h:249
Sat_MemHand
static cla Sat_MemHand(Sat_Mem_t *p, int i, int k)
Definition: satClause.h:101
Sat_MemMemoryHand
static double Sat_MemMemoryHand(Sat_Mem_t *p, cla h)
Definition: satClause.h:106