1 #ifndef int_var_h
2 #define int_var_h
3
4 #include <new>
5 #include <stdint.h>
6 #include <chuffed/support/misc.h>
7 #include <chuffed/core/sat-types.h>
8 #include <chuffed/core/engine.h>
9 #include <chuffed/vars/vars.h>
10 #include <chuffed/vars/bool-view.h>
11
12 #ifndef INT64_MAX
13 #define INT64_MAX 9223372036854775807LL
14 #endif
15 #ifndef INT64_MIN
16 #define INT64_MIN (-INT64_MAX-1)
17 #endif
18
19 // Controls whether active domain values are stored in a trailed linked list,
20 // to allow fast enumeration of domain values. Also whether a count is kept.
21 // NOTE: Makes search a bit slower, so kept it conditional at this stage,
22 // turning this off selects compatibility routines that scan value-by-value.
23 #define INT_DOMAIN_LIST 0
24
25 /*
26
27 IntVar descriptions
28
29 IntVar: Base class, no lits
30
31 IntVarEL: Eager lit class, lits are eagerly generated
32 supports bounds and/or value lits
33 use for "small" vars, or when we need the lits for clausified propagators
34
35 IntVarLL;: Lazy lit class, lits are lazily generated
36 supports bounds lits only
37 remVal ignored
38 use for large or unbounded vars
39
40 */
41
42 // Bye bye macros
43 #undef min
44 #undef max
45
46 //-----
47
48 class IntVar : public Var {
49 public:
50 int const var_id;
51
52 Tint min;
53 Tint max;
54 int min0; // Initial minimum
55 int max0; // Initial maximum
56 int shadow_val;
57 bool in_scip;
58 bool all_in_scip;
59
60 bool should_be_learnable;
61 bool should_be_decidable;
62
63 Tchar *vals;
64 #if INT_DOMAIN_LIST
65 Tint *vals_list;
66 Tint vals_count;
67 #endif
68
69 PreferredVal preferred_val;
70
71 double activity;
72
73 IntVar(int min, int max);
74
75 friend IntVar* newIntVar(int min, int max);
76
77 #if !INT_DOMAIN_LIST
78 void updateMin();
79 void updateMax();
80 #endif
81 void updateFixed();
82
83
84 public:
85
86 static const int max_limit = 500000000;
87 static const int min_limit = -500000000;
88
89 //--------------------------------------------------
90 // Engine stuff
91
92 struct PropInfo {
93 Propagator *p;
94 int pos; // what is var's id w.r.t. the propagator
95 int eflags; // what var events should wake this propagator
96
PropInfoPropInfo97 PropInfo(Propagator *_p, int _pos, int _eflags)
98 : p(_p), pos(_pos), eflags(_eflags) {}
99 };
100
101 // intermediate state
102 int changes;
103 bool in_queue;
104
105 // persistent state
106 vec<PropInfo> pinfo;
107
108 virtual void attach(Propagator *p, int pos, int eflags);
109
110 void pushInQueue();
111 void wakePropagators();
112 void clearPropState();
113 int simplifyWatches();
114
115 //--------------------------------------------------
116 // Branching stuff
117
finished()118 bool finished() { return isFixed(); }
119 double getScore(VarBranch vb);
setPreferredVal(PreferredVal p)120 void setPreferredVal(PreferredVal p) { preferred_val = p; }
121 DecInfo* branch();
122
123 //--------------------------------------------------
124 // Type specialisation
125
getType()126 VarType getType() { return INT_VAR; }
127
128 void specialiseToEL();
129 void specialiseToLL();
130 void specialiseToSL(vec<int>& values);
131
132 void initVals(bool optional = false);
133
134 //--------------------------------------------------
135 // Read data
136
isFixed()137 bool isFixed() const { return min == max; }
getMin()138 int getMin() const { return min; }
getMax()139 int getMax() const { return max; }
getMin0()140 int getMin0() const { return min0; }
getMax0()141 int getMax0() const { return max0; }
getVal()142 int getVal() const { assert(isFixed()); return min; }
getShadowVal()143 int getShadowVal() const {
144 if (in_scip) return shadow_val;
145 return min;
146 }
147
indomain(int64_t v)148 bool indomain(int64_t v) const {
149 return v >= min && v <= max && (!vals || vals[v]);
150 }
151
152 class iterator {
153 const IntVar* var;
154 int val;
155 public:
iterator()156 iterator() {}
iterator(const IntVar * _var,int _val)157 iterator(const IntVar* _var, int _val) : var(_var), val(_val) {}
158 int operator *() const {
159 assert(val >= var->min && val <= var->max && var->vals && var->vals[val]);
160 return val;
161 }
162 iterator& operator ++() {
163 assert(val >= var->min && val <= var->max && var->vals && var->vals[val]);
164 if (val == var->max)
165 val = static_cast<int>(0x80000000);
166 else
167 #if INT_DOMAIN_LIST
168 val = var->vals_list[2*val+1];
169 #else
170 while (!var->vals[++val])
171 ;
172 #endif
173 return *this;
174 }
175 iterator operator ++(int dummy) {
176 iterator temp = *this;
177 ++*this;
178 return temp;
179 }
180 iterator& operator --() {
181 if (val == static_cast<int>(0x80000000))
182 val = var->max;
183 else {
184 assert(val > var->min && val <= var->max && var->vals && var->vals[val]);
185 #if INT_DOMAIN_LIST
186 val = var->vals_list[2*val];
187 #else
188 while (!var->vals[--val])
189 ;
190 #endif
191 }
192 return *this;
193 }
194 iterator operator --(int dummy) {
195 iterator temp = *this;
196 --*this;
197 return temp;
198 }
199 bool operator ==(const iterator& rhs) const {
200 assert(var == rhs.var);
201 return (val == rhs.val);
202 }
203 bool operator !=(const iterator& rhs) const {
204 assert(var == rhs.var);
205 return (val != rhs.val);
206 }
207 };
208 typedef iterator const_iterator;
begin()209 iterator begin() const { return iterator(this, min); }
end()210 iterator end() const { return iterator(this, static_cast<int>(0x80000000)); }
211
212 class reverse_iterator {
213 iterator forward;
214 public:
reverse_iterator()215 reverse_iterator() {}
reverse_iterator(iterator _forward)216 reverse_iterator(iterator _forward) : forward(_forward) {}
217 int operator *() const {
218 iterator temp = forward;
219 return *--temp;
220 }
221 reverse_iterator& operator ++() {
222 --forward;
223 return *this;
224 }
225 reverse_iterator operator ++(int dummy) {
226 reverse_iterator temp = *this;
227 ++*this;
228 return temp;
229 }
230 reverse_iterator& operator --() {
231 ++forward;
232 return *this;
233 }
234 reverse_iterator operator --(int dummy) {
235 reverse_iterator temp = *this;
236 --*this;
237 return temp;
238 }
base()239 iterator base() const {
240 return forward;
241 }
242 bool operator ==(const reverse_iterator& rhs) const {
243 return (forward == rhs.forward);
244 }
245 bool operator !=(const reverse_iterator& rhs) const {
246 return (forward != rhs.forward);
247 }
248 };
249 typedef reverse_iterator const_reverse_iterator;
rbegin()250 reverse_iterator rbegin() const { return reverse_iterator(end()); }
rend()251 reverse_iterator rend() const { return reverse_iterator(begin()); }
252
size()253 int size() const {
254 assert(vals);
255 #if INT_DOMAIN_LIST
256 return vals_count;
257 #else
258 if (isFixed())
259 return 1;
260 int count = 2;
261 for (int i = min + 1; i < max; ++i)
262 count += vals[i];
263 return count;
264 #endif
265 }
266
267 //--------------------------------------------------
268 // Explanations:
269
getMinLit()270 virtual Lit getMinLit() const { NEVER; }
getMaxLit()271 virtual Lit getMaxLit() const { NEVER; }
getValLit()272 virtual Lit getValLit() const { NEVER; }
getFMinLit(int64_t v)273 virtual Lit getFMinLit(int64_t v) { NEVER; }
getFMaxLit(int64_t v)274 virtual Lit getFMaxLit(int64_t v) { NEVER; }
275
276 // NOTE: No support for INT_VAR_LL vars yet!
277 // t = 0: [x != v], t = 1: [x = v], t = 2: [x >= v], t = 3: [x <= v]
getLit(int64_t v,int t)278 virtual Lit getLit(int64_t v, int t) { NEVER; }
279
280 //--------------------------------------------------
281 // Domain operations
282
283 void set(int val, int type, bool channel = true);
284
setMinNotR(int64_t v)285 bool setMinNotR(int64_t v) const { return v > min; }
setMaxNotR(int64_t v)286 bool setMaxNotR(int64_t v) const { return v < max; }
setValNotR(int64_t v)287 bool setValNotR(int64_t v) const { return v != min || v != max; }
remValNotR(int64_t v)288 bool remValNotR(int64_t v) const { return indomain(v); }
289
290 virtual bool setMin(int64_t v, Reason r = NULL, bool channel = true);
291 virtual bool setMax(int64_t v, Reason r = NULL, bool channel = true);
292 virtual bool setVal(int64_t v, Reason r = NULL, bool channel = true);
293 virtual bool remVal(int64_t v, Reason r = NULL, bool channel = true);
294 virtual bool allowSet(vec<int>& v, Reason r = NULL, bool channel = true);
295
channel(int val,int val_type,int sign)296 virtual void channel(int val, int val_type, int sign) {
297 set(val, val_type * 3 ^ sign, false);
298 }
299
300 Lit operator >= (int val) { return getLit(val, 2); }
301 Lit operator <= (int val) { return getLit(val, 3); }
302 Lit operator > (int val) { return getLit(val+1, 2); }
303 Lit operator < (int val) { return getLit(val-1, 3); }
304 Lit operator = (int val) { return getLit(val, 1); }
305 Lit operator != (int val) { return getLit(val, 0); }
306
BoolView()307 operator BoolView () { assert(min >= 0 && max <= 1); return getLit(1, 2); }
308
309 //--------------------------------------------------
310 // Debug
311
312 void printLit(int val, int type);
313 void print();
314
315 };
316
317 IntVar* newIntVar(int min = IntVar::min_limit, int max = IntVar::max_limit);
318 IntVar* getConstant(int v);
319
pushInQueue()320 inline void IntVar::pushInQueue() {
321 if (!in_queue) {
322 in_queue = true;
323 engine.v_queue.push(this);
324 }
325 }
326
clearPropState()327 inline void IntVar::clearPropState() {
328 changes = 0;
329 in_queue = false;
330 }
331
set(int val,int type,bool channel)332 inline void IntVar::set(int val, int type, bool channel) {
333 switch (type) {
334 case 0: remVal(val, NULL, channel); break;
335 case 1: setVal(val, NULL, channel); break;
336 case 2: setMin(val+1, NULL, channel); break;
337 case 3: setMax(val, NULL, channel); break;
338 default: NEVER;
339 }
340 }
341
printLit(int val,int type)342 inline void IntVar::printLit(int val, int type) {
343 printf("[v%d ", var_id);
344 switch (type) {
345 case 0: printf("!= %d]", val); break;
346 case 1: printf("== %d]", val); break;
347 case 2: printf(">= %d]", val+1); break;
348 case 3: printf("<= %d]", val); break;
349 }
350 }
351
print()352 inline void IntVar::print() {
353 fprintf(stderr, "v%d: min = %d, max = %d\n", var_id, (int) min, (int) max);
354 }
355
356
357 #include <chuffed/vars/int-var-el.h>
358 #include <chuffed/vars/int-var-ll.h>
359 #include <chuffed/vars/int-var-sl.h>
360
361 #endif
362