1 #ifndef _level_hpp_INCLUDED
 2 #define _level_hpp_INCLUDED
 3 
 4 #include <climits>
 5
 
 
 6 namespace CaDiCaL {
 7 
 8 // For each new decision we increase the decision level and push a 'Level'
 9 // on the 'control' stack.  The information gathered here is used in
10 // 'reuse_trail' and for early aborts in clause minimization.
11 
12 struct Level {
13 
14   int decision;         // decision literal of this level
 

15   int trail;            // trail start of this level
16 
17   struct {
18     int count;          // how many variables seen during 'analyze'
19     int trail;          // smallest trail position seen on this level
20   } seen;
21 
22   void reset () { seen.count = 0; seen.trail = INT_MAX; }
23 
24   Level (int
 
 d, int t) : decision (d), trail (t) { reset (); }
25   Level () { }
26 };
27 
28 }
29 
30 #endif