1 #ifndef _limit_hpp_INCLUDED 2 #define _limit_hpp_INCLUDED 3 4 namespace CaDiCaL { 5 6 struct Limit { 7 8 bool initialized; 9 10 int64_t conflicts; // conflict limit if non-negative 11 int64_t decisions; // decision limit if non-negative 12 int64_t preprocessing; // limit on preprocessing rounds 13 int64_t localsearch; // limit on local search rounds 14 15 int64_t compact; // conflict limit for next 'compact' 16 int64_t elim; // conflict limit for next 'elim' 17 int64_t flush; // conflict limit for next 'flush' 18 int64_t probe; // conflict limit for next 'probe' 19 int64_t reduce; // conflict limit for next 'reduce' 20 int64_t rephase; // conflict limit for next 'rephase' 21 int64_t report; // report limit for header 22 int64_t restart; // conflict limit for next 'restart' 23 int64_t stabilize; // conflict limit for next 'stabilize' 24 int64_t subsume; // conflict limit for next 'subsume' 25 26 int keptsize; // maximum kept size in 'reduce' 27 int keptglue; // maximum kept glue in 'reduce' 28 29 // How often rephased during (1) or out (0) of stabilization. 30 // 31 int64_t rephased[2]; 32 33 // Current elimination bound per eliminated variable. 34 // 35 int64_t elimbound; 36 37 Limit (); 38 }; 39 40 struct Last { 41 struct { int64_t propagations; } transred, vivify; 42 struct { int64_t fixed, subsumephases, marked; } elim; 43 struct { int64_t propagations, reductions; } probe; 44 struct { int64_t conflicts; } reduce, rephase; 45 struct { int64_t marked; } ternary; 46 struct { int64_t fixed; } collect; 47 Last (); 48 }; 49 50 struct Inc { 51 int64_t flush; // flushing interval in terms of conflicts 52 int64_t stabilize; // stabilization interval increment 53 int64_t conflicts; // next conflict limit if non-negative 54 int64_t decisions; // next decision limit if non-negative 55 int64_t preprocessing; // next preprocessing limit if non-negative 56 int64_t localsearch; // next local search limit if non-negative 57 Inc (); 58 }; 59 60 } 61 62 #endif 63