1 #include <chuffed/vars/int-var.h>
2 #include <chuffed/core/sat.h>
3 #include <chuffed/core/propagator.h>
4
5 extern std::map<IntVar*, std::string> intVarString;
6
IntVarSL(const IntVar & other,vec<int> & _values)7 IntVarSL::IntVarSL(const IntVar& other, vec<int>& _values)
8 : IntVar(other), values(_values) {
9
10 initVals();
11
12 // handle min, max and vals
13 int l = 0;
14 while (values[l] < min) if (++l == values.size()) TL_FAIL();
15 while (!vals[values[l]]) if (++l == values.size()) TL_FAIL();
16 min = values[l];
17
18 // printf("l = %d\n", l);
19
20 int u = values.size()-1;
21 while (values[u] > max) if (u-- == 0) TL_FAIL();
22 while (!vals[values[u]]) if (u-- == 0) TL_FAIL();
23 max = values[u];
24
25 // printf("u = %d\n", u);
26
27 for (int i = min, k = l; i <= max; i++) {
28 if (i == values[k]) { k++; continue; }
29 vals[i] = false;
30 }
31
32 for (int i = l; i <= u; i++) values[i-l] = values[i];
33 values.resize(u-l+1);
34
35 // for (int i = 0; i < values.size(); i++) printf("%d ", values[i]);
36 // printf("\n");
37
38 // create the IntVarEL
39 IntVar *v = newIntVar(0, values.size()-1);
40 // inherit the name from this SL
41 intVarString[v] = intVarString[this];
42 v->specialiseToEL();
43 el = (IntVarEL*) v;
44
45 // rechannel channel info
46 for (int i = 0; i < values.size(); i++) {
47 Lit p = el->getLit(i, 0);
48 sat.c_info[var(p)].cons_id = var_id;
49 }
50 for (int i = 0; i <= values.size(); i++) {
51 Lit p = el->getLit(i, 2);
52 sat.c_info[var(p)].cons_id = var_id;
53 }
54
55 // transfer pinfo to el
56 for (int i = 0; i < pinfo.size(); i++) {
57 el->pinfo.push(pinfo[i]);
58 }
59 pinfo.clear(true);
60 }
61
attach(Propagator * p,int pos,int eflags)62 void IntVarSL::attach(Propagator *p, int pos, int eflags) {
63 if (isFixed()) p->wakeup(pos, eflags);
64 else el->pinfo.push(PropInfo(p, pos, eflags));
65 }
66
transform(int v,int type)67 int IntVarSL::transform(int v, int type) {
68 int l = 0, u = values.size()-1, m;
69 while (true) {
70 m = (l+u)/2;
71 if (values[m] == v) return m;
72 else if (values[m] < v) l = m+1;
73 else u = m-1;
74 if (u < l) break;
75 }
76 switch (type) {
77 case 0: return u;
78 case 1: return l;
79 case 2: return -1;
80 default: NEVER;
81 }
82 }
83
84 // t = 0: [x != v], t = 1: [x = v], t = 2: [x >= v], t = 3: [x <= v]
getLit(int64_t v,int t)85 Lit IntVarSL::getLit(int64_t v, int t) {
86 int u;
87 switch (t) {
88 case 0:
89 u = transform(v, 2);
90 return (u == -1 ? lit_True : el->getLit(u, 0));
91 case 1:
92 u = transform(v, 2);
93 return (u == -1 ? lit_False : el->getLit(u, 1));
94 case 2: return el->getLit(transform(v, 1), 2);
95 case 3: return el->getLit(transform(v, 0), 3);
96 default: NEVER;
97 }
98 }
99
100
setMin(int64_t v,Reason r,bool channel)101 bool IntVarSL::setMin(int64_t v, Reason r, bool channel) {
102 assert(setMinNotR(v));
103 // debug();
104 // printf("setMin: v = %d, u = %d\n", v, transform(v, 0));
105 if (!el->setMin(transform(v, 1), r, channel)) return false;
106 min = values[el->min];
107 return true;
108 }
109
110
setMax(int64_t v,Reason r,bool channel)111 bool IntVarSL::setMax(int64_t v, Reason r, bool channel) {
112 assert(setMaxNotR(v));
113 // debug();
114 // printf("setMax: v = %d, u = %d\n", v, transform(v, 0));
115 if (!el->setMax(transform(v, 0), r, channel)) return false;
116 max = values[el->max];
117 return true;
118 }
119
setVal(int64_t v,Reason r,bool channel)120 bool IntVarSL::setVal(int64_t v, Reason r, bool channel) {
121 assert(setValNotR(v));
122 int u = transform(v, 2);
123 if (u == -1) {
124 if (channel) sat.cEnqueue(lit_False, r);
125 assert(sat.confl);
126 return false;
127 }
128 if (!el->setVal(u, r, channel)) return false;
129 if (min < v) min = v;
130 if (max > v) max = v;
131 return true;
132 }
133
remVal(int64_t v,Reason r,bool channel)134 bool IntVarSL::remVal(int64_t v, Reason r, bool channel) {
135 assert(remValNotR(v));
136 int u = transform(v, 2);
137 assert(u != -1);
138 if (!el->remVal(u, r, channel)) return false;
139 vals[v] = false;
140 min = values[el->min];
141 max = values[el->max];
142 return true;
143 }
144
channel(int val,int val_type,int sign)145 void IntVarSL::channel(int val, int val_type, int sign) {
146 // fprintf(stderr, "funny channel\n");
147 int type = val_type * 3 ^ sign;
148 el->set(val, type, false);
149 if (type == 0) vals[values[val]] = false;
150 min = values[el->min];
151 max = values[el->max];
152 }
153
debug()154 void IntVarSL::debug() {
155 printf("min = %d, max = %d, el->min = %d, el->max = %d\n", (int) min, (int) max, (int) el->min, (int) el->max);
156 for (int i = 0; i < values.size(); i++) printf("%d ", values[i]);
157 printf("\n");
158 }
159
160