1 #ifndef engine_h
2 #define engine_h
3
4 #include <chuffed/support/misc.h>
5 #include <string>
6
7 #define DEBUG 0
8
9
10 enum OPT_TYPE { OPT_MIN = 0, OPT_MAX = 1 };
11 enum RESULT { RES_SAT, RES_LUN, RES_GUN, RES_UNK, RES_SEA };
12
13 class BranchGroup;
14 class Branching;
15 class BTPos;
16 class Checker;
17 class DecInfo;
18 class IntVar;
19 class Problem;
20 class Propagator;
21 class PseudoProp;
22 class TrailElem;
23
24 //-----
25
26 class Engine {
27
28 public:
29 static const int num_queues = 6;
30
31 // Problem setup
32 vec<IntVar*> vars; // List of int vars
33 vec<Branching*> outputs; // List of output vars
34 vec<Propagator*> propagators; // List of propagators
35 vec<PseudoProp*> pseudo_props; // List of pseudo propagators
36 vec<Checker*> checkers; // List of constraint checkers
37 vec<int> assumptions; // List of assumption literals
38 bool finished_init;
39
40
41 Problem *problem;
42 BranchGroup *branching;
43 IntVar *opt_var;
44 int opt_type;
45 int best_sol;
46 RESULT status;
47 time_point time_out;
48
49 // Intermediate propagation state
50 vec<IntVar*> v_queue; // List of changed vars
51 vec<vec<Propagator*> > p_queue; // Queue of propagators to run
52 Propagator *last_prop; // Last propagator run, set for idempotent propagators
53 bool async_fail; // Asynchronous failure
54
55 // Decision stack
56 vec<DecInfo> dec_info;
57
58 // Trails
59 vec<TrailElem> trail; // Raw data changes
60 vec<int> trail_lim;
61
62 // Statistics
63 time_point start_time;
64 duration init_time, opt_time;
65 double base_memory;
66 long long int conflicts, nodes, propagations, solutions, next_simp_db;
67 int peak_depth;
68 int restart_count;
69
70 std::ostream* output_stream;
71 private:
72
73 // Init
74 void init();
75 void initMPI();
76
77 // Engine core
78 void newDecisionLevel();
79 void doFixPointStuff();
80 void makeDecision(DecInfo& di, int alt);
81 bool constrain();
82 bool propagate();
83 void clearPropState();
84 void topLevelCleanUp();
85 void simplifyDB();
86 void blockCurrentSol();
87 unsigned int getRestartLimit(unsigned int i); // Return the restart limit for restart i
88 void toggleVSIDS();
89
90 public:
91
92 // Constructor
93 Engine();
94
95 // Trail methods
96 void btToPos(int pos);
97 void btToLevel(int level);
98
99 // Interface methods
100 RESULT search(const std::string& problemLabel = "chuffed");
101 void solve(Problem *p, const std::string& problemLabel = "chuffed");
102
103 // Stats
104 void printStats();
105 void checkMemoryUsage();
106
decisionLevel()107 int decisionLevel() const { return trail_lim.size(); }
trailPos()108 int trailPos() const { return trail.size(); }
tpToLevel(int tp)109 int tpToLevel(int tp) const {
110 for (int i = trail_lim.size(); i--; ) if (tp >= trail_lim[i]) return i+1;
111 return 0;
112 }
113
setOutputStream(std::ostream & os)114 void setOutputStream(std::ostream& os) {
115 output_stream = &os;
116 }
117
118 };
119
120 extern Engine engine;
121
122 void optimize(IntVar* v, int t);
123
124 //-----
125
126 class TrailElem {
127 public:
128 int *pt; int x; int sz;
TrailElem(int * _pt,int _sz)129 TrailElem(int *_pt, int _sz) : pt(_pt), x(_sz == 1 ? *((char*) pt) : _sz == 2 ? *((short*) pt) : *pt), sz(_sz) {}
undo()130 void undo() {
131 switch (sz) {
132 case 1: *((char*) pt) = x; break;
133 case 2: *((short*) pt) = x; break;
134 default: *pt = x; break;
135 }
136 }
137 };
138
139 template <class T, class U>
trailChange(T & v,const U u)140 static inline void trailChange(T& v, const U u) {
141 int *pt = (int*) &v;
142 engine.trail.push(TrailElem(pt, sizeof(T)));
143 if (sizeof(T) == 8) {
144 engine.trail.push(TrailElem(pt+1, sizeof(T)));
145 }
146 v = u;
147 }
148
149
150
151 //------
152
153 // Auto-trailed int
154
155 #define AUTOTRAIL(t) \
156 class T##t { \
157 public: \
158 t v; \
159 T##t() {} \
160 T##t(t _v) : v(_v) {} \
161 operator t () const { return v; } \
162 t operator = (t o); \
163 t operator = (T##t o) { return *this = o.v; } \
164 t operator += (t o) { return *this = v + o; } \
165 t operator -= (t o) { return *this = v - o; } \
166 t operator *= (t o) { return *this = v * o; } \
167 t operator /= (t o) { return *this = v / o; } \
168 t operator %= (t o) { return *this = v % o; } \
169 t operator ^= (t o) { return *this = v ^ o; } \
170 t operator &= (t o) { return *this = v & o; } \
171 t operator |= (t o) { return *this = v | o; } \
172 t operator <<= (t o) { return *this = v << o; } \
173 t operator >>= (t o) { return *this = v >> o; } \
174 t operator ++ () { return *this = v + 1; } \
175 t operator -- () { return *this = v - 1; } \
176 t operator ++ (int dummy) { int tmp = v; *this = v + 1; return tmp; } \
177 t operator -- (int dummy) { int tmp = v; *this = v - 1; return tmp; } \
178 };
179
180 AUTOTRAIL(char)
181 AUTOTRAIL(int)
182 AUTOTRAIL(int64_t)
183
184 cassert(sizeof(Tchar) == 1);
185 cassert(sizeof(Tint) == 4);
186 cassert(sizeof(Tint64_t) == 8);
187
188 inline char Tchar::operator = (char o) {
189 int *pt = (int*) this;
190 engine.trail.push(TrailElem(pt, 1));
191 return v = o;
192 }
193
194 inline int Tint::operator = (int o) {
195 int *pt = (int*) this;
196 engine.trail.push(TrailElem(pt, 4));
197 return v = o;
198 }
199
200 inline int64_t Tint64_t::operator = (int64_t o) {
201 int *pt = (int*) this;
202 engine.trail.push(TrailElem(pt, 4));
203 engine.trail.push(TrailElem(pt+1, 4));
204 return v = o;
205 }
206
207 //-----
208
209 class Problem {
210 public:
211 virtual void print(std::ostream&) = 0;
restrict_learnable()212 virtual void restrict_learnable() {};
213 };
214
215
216 #endif
217