1 #include "internal.hpp"
2
3 namespace CaDiCaL {
4
Limit()5 Limit::Limit () {
6 memset (this, 0, sizeof *this);
7 }
8
9 /*------------------------------------------------------------------------*/
10
scale(double v) const11 double Internal::scale (double v) const {
12 const double ratio = clause_variable_ratio ();
13 const double factor = (ratio <= 2) ? 1.0 : log (ratio) / log (2);
14 double res = factor * v;
15 if (res < 1) res = 1;
16 return res;
17 }
18
19 /*------------------------------------------------------------------------*/
20
terminating()21 bool Internal::terminating () {
22
23 if (external->terminator && external->terminator->terminate ()) {
24 LOG ("connected terminator forces termination");
25 return true;
26 }
27
28 if (termination_forced) {
29 LOG ("termination forced");
30 return true;
31 }
32
33 if (!preprocessing &&
34 !localsearching &&
35 lim.conflicts >= 0 &&
36 stats.conflicts >= lim.conflicts) {
37 LOG ("conflict limit %" PRId64 " reached", lim.conflicts);
38 return true;
39 }
40
41 if (!preprocessing &&
42 !localsearching &&
43 lim.decisions >= 0 &&
44 stats.decisions >= lim.decisions) {
45 LOG ("decision limit %" PRId64 " reached", lim.decisions);
46 return true;
47 }
48
49 return false;
50 }
51
52 /*------------------------------------------------------------------------*/
53
Last()54 Last::Last () {
55 memset (this, 0, sizeof *this);
56 }
57
58 /*------------------------------------------------------------------------*/
59
Inc()60 Inc::Inc () {
61 memset (this, 0, sizeof *this);
62 decisions = conflicts = -1; // unlimited
63 }
64
limit_conflicts(int l)65 void Internal::limit_conflicts (int l) {
66 if (l < 0 && inc.conflicts < 0) {
67 LOG ("keeping unbounded conflict limit");
68 } else if (l < 0) {
69 LOG ("reset conflict limit to be unbounded");
70 inc.conflicts = -1;
71 } else {
72 inc.conflicts = l;
73 LOG ("new conflict limit of %d conflicts", l);
74 }
75 }
76
limit_decisions(int l)77 void Internal::limit_decisions (int l) {
78 if (l < 0 && inc.decisions < 0) {
79 LOG ("keeping unbounded decision limit");
80 } else if (l < 0) {
81 LOG ("reset decision limit to be unbounded");
82 inc.decisions = -1;
83 } else {
84 inc.decisions = stats.decisions + l;
85 LOG ("new decision limit of %d decisions", l);
86 }
87 }
88
limit_preprocessing(int l)89 void Internal::limit_preprocessing (int l) {
90 if (l < 0) {
91 LOG ("ignoring invalid preprocessing limit %d", l);
92 } else if (!l) {
93 LOG ("reset preprocessing limit to no preprocessing");
94 inc.preprocessing = 0;
95 } else {
96 inc.preprocessing = l;
97 LOG ("new preprocessing limit of %d preprocessing rounds", l);
98 }
99 }
100
limit_local_search(int l)101 void Internal::limit_local_search (int l) {
102 if (l < 0) {
103 LOG ("ignoring invalid local search limit %d", l);
104 } else if (!l) {
105 LOG ("reset local search limit to no local search");
106 inc.localsearch = 0;
107 } else {
108 inc.localsearch = l;
109 LOG ("new local search limit of %d local search rounds", l);
110 }
111 }
112
is_valid_limit(const char * name)113 bool Internal::is_valid_limit (const char * name) {
114 if (!strcmp (name, "conflicts")) return true;
115 if (!strcmp (name, "decisions")) return true;
116 if (!strcmp (name, "preprocessing")) return true;
117 if (!strcmp (name, "localsearch")) return true;
118 return false;
119 }
120
limit(const char * name,int l)121 bool Internal::limit (const char * name, int l) {
122 bool res = true;
123 if (!strcmp (name, "conflicts")) limit_conflicts (l);
124 else if (!strcmp (name, "decisions")) limit_decisions (l);
125 else if (!strcmp (name, "preprocessing")) limit_preprocessing (l);
126 else if (!strcmp (name, "localsearch")) limit_local_search (l);
127 else res = false;
128 return res;
129 }
130
reset_limits()131 void Internal::reset_limits () {
132 LOG ("reset limits");
133 limit_conflicts (-1);
134 limit_decisions (-1);
135 limit_preprocessing (0);
136 limit_local_search (0);
137 }
138
139 }
140
141