this repo has no description
dekker.one
1/**** , [ QSolverUnblockable.cc ],
2Copyright (c) 2008 Universite d'Orleans - Jeremie Vautard
3
4Permission is hereby granted, free of charge, to any person obtaining a copy
5of this software and associated documentation files (the "Software"), to deal
6in the Software without restriction, including without limitation the rights
7to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
8copies of the Software, and to permit persons to whom the Software is
9furnished to do so, subject to the following conditions:
10
11The above copyright notice and this permission notice shall be included in
12all copies or substantial portions of the Software.
13
14THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
15IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
16FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
17AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
18LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
19OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN
20THE SOFTWARE.
21*************************************************************************/
22
23#include "qsolver_unblockable.hh"
24#include <climits>
25
26QSolverUnblockable::QSolverUnblockable(QcspUnblockable* sp) {
27 this->sp = sp;
28 nbRanges=new int;
29}
30
31Strategy QSolverUnblockable::solve(unsigned long int& nodes) {
32 vector<int> plop;
33 plop.clear();
34 return rSolve(sp,0,plop,nodes);
35}
36
37Strategy QSolverUnblockable::rSolve(QcspUnblockable* qs,int scope, vector<int> assignments, unsigned long int& nodes) {
38 nodes++;
39 //cout<<"rSolve for scope "<<scope<<" with assignments ";
40 // for (int i=0;i<assignments.size();i++) cout<<assignments[i]<<" ";
41 // cout<<endl;
42 //////////////////////////////////////////////////////////////////////////////////////////
43 // First case : Unblockable QCSP+ : Goal checking. //
44 // If the goal is failed, even before the end on f the search, we fail. //
45 //////////////////////////////////////////////////////////////////////////////////////////
46 MySpace* g = qs->getGoal();
47 if (g == NULL) {return Strategy(StrategyNode::SFalse());}
48 for (int i=0;i<assignments.size();i++) {
49 switch (g->type_of_v[i]) {
50 case VTYPE_INT :
51 rel(*g,*(static_cast<IntVar*>(g->v[i])) == assignments[i]);
52 break;
53 case VTYPE_BOOL :
54 rel(*g,*(static_cast<BoolVar*>(g->v[i])) == assignments[i]);
55 break;
56 default :
57 cout<<"1Unknown variable type"<<endl;
58 abort();
59 }
60 }
61 if (g->status() == SS_FAILED) {
62 delete g;
63 return Strategy(StrategyNode::SFalse());
64 }
65 delete g;
66
67 if (scope == qs->spaces()) {
68 return Strategy(StrategyNode::STrue());
69 }
70
71 /////////////////////////////////////////////////////////////////////////////////////////
72 // Second case : we are in the middle of the problem... //
73 /////////////////////////////////////////////////////////////////////////////////////////
74 else {
75 MySpace* espace = qs->getSpace(scope);
76 if (espace == NULL) cout<<"I caught a NULL for scope "<<scope<<". I will crash..."<<endl;
77 for (int i=0;i<assignments.size();i++) {
78 switch (espace->type_of_v[i]) {
79 case VTYPE_INT :
80 rel(*espace,*(static_cast<IntVar*>(espace->v[i])) == assignments[i]);
81 break;
82 case VTYPE_BOOL :
83 rel(*espace,*(static_cast<BoolVar*>(espace->v[i])) == assignments[i]);
84 break;
85 default :
86 cout<<"2Unknown variable type"<<endl;
87 abort();
88 }
89 }
90
91 // Second case, first subcase : current scope is universal
92 /////////////////////////////////////////////////////////
93 if (qs->quantification(scope)) {
94 if (espace->status() == SS_FAILED) {
95 delete espace;
96 return Strategy(StrategyNode::STrue());
97 }
98
99 DFS<MySpace> solutions(espace);
100 MySpace* sol = solutions.next();
101 if (sol == NULL) {
102 delete espace;
103 return Strategy(StrategyNode::STrue());
104 }
105
106 Strategy retour = StrategyNode::Dummy();
107 while (sol != NULL) {
108 vector<int> assign;
109 for (int i = 0; i<sp->nbVarInScope(scope);i++) {
110 switch (sol->type_of_v[i]) {
111 case VTYPE_INT :
112 assign.push_back( (static_cast<IntVar*>(sol->v[i]))->val() );
113 break;
114 case VTYPE_BOOL :
115 assign.push_back( (static_cast<BoolVar*>(sol->v[i]))->val() );
116 break;
117 default :
118 cout<<"3Unknown variable type"<<endl;
119 abort();
120 }
121 }
122
123 int vmin = ( (scope==0)? 0 : (qs->nbVarInScope(scope-1)) );
124 int vmax = (qs->nbVarInScope(scope))-1;
125 vector<int> zevalues;
126 for (int i = vmin; i<=vmax;i++) {
127 switch (sol->type_of_v[i]) {
128 case VTYPE_INT :
129 zevalues.push_back( (static_cast<IntVar*>(sol->v[i]))->val() );
130 break;
131 case VTYPE_BOOL :
132 zevalues.push_back( (static_cast<BoolVar*>(sol->v[i]))->val() );
133 break;
134 default :
135 cout<<"4Unknown variable type"<<endl;
136 abort();
137 }
138 }
139 Strategy toAttach(true,vmin,vmax,scope,zevalues);
140
141 Strategy son = rSolve(qs,scope+1,assign,nodes);
142 if (son.isFalse()) {
143 delete sol;
144 delete espace;
145 return Strategy(StrategyNode::SFalse());
146 }
147 toAttach.attach(son);
148 retour.attach(toAttach);
149 delete sol;
150 sol = solutions.next();
151 } // end of while
152 delete espace;
153 return retour;
154 } // end of if(universal)
155
156 // Second case, second subcase : current scope is existential
157 ////////////////////////////////////////////////////////////
158 else {
159 if ((espace->status()) == SS_FAILED) {
160 delete espace;
161 return Strategy(StrategyNode::SFalse());
162 }
163
164 DFS<MySpace> solutions(espace);
165 MySpace* sol =solutions.next();
166 if (sol == NULL) {
167 delete espace;
168 return Strategy(StrategyNode::SFalse());
169 }
170 while (sol != NULL) {
171 vector<int> assign;
172 for (int i = 0; i<sp->nbVarInScope(scope);i++) {
173 // cout << "i = "<<i<<endl;
174 switch (sol->type_of_v[i]) {
175 case VTYPE_INT :
176 assign.push_back( (static_cast<IntVar*>(sol->v[i]))->val() );
177 break;
178 case VTYPE_BOOL :
179 assign.push_back( (static_cast<BoolVar*>(sol->v[i]))->val() );
180 break;
181 default :
182 cout<<"5Unknown variable type"<<endl;
183 abort();
184 }
185 } // end for
186
187 int vmin = ( (scope==0)?0 : qs->nbVarInScope(scope-1) );
188 int vmax = qs->nbVarInScope(scope)-1;
189 vector<int> zevalues;
190 for (int i = vmin; i<=vmax;i++) {
191 switch (sol->type_of_v[i]) {
192 case VTYPE_INT :
193 zevalues.push_back( (static_cast<IntVar*>(sol->v[i]))->val() );
194 break;
195 case VTYPE_BOOL :
196 zevalues.push_back( (static_cast<BoolVar*>(sol->v[i]))->val() );
197 break;
198 default :
199 cout<<"6unknown Variable type"<<endl;
200 abort();
201 }
202 }
203 Strategy candidate(false,vmin,vmax,scope,zevalues);
204
205 Strategy son_of_candidate = rSolve(qs,scope+1,assign,nodes);
206 if (son_of_candidate.isFalse()) candidate = Strategy::SFalse();
207 else candidate.attach(son_of_candidate);
208
209 if (!candidate.isFalse()) {
210 delete sol;
211 delete espace;
212 return candidate;
213 }
214 delete sol;
215 sol=solutions.next();
216 } // end while sol != null
217 delete espace;
218 return Strategy(StrategyNode::SFalse());
219 } // end if..else (existential)
220 }// end "Second case"
221}
222
223
224//////////////////////
225//////////////////////
226//////////////////////
227
228QSolverUnblockable2::QSolverUnblockable2(Qcop* sp) {
229 this->sp = sp;
230 nbRanges=new int;
231}
232
233Strategy QSolverUnblockable2::solve(unsigned long int& nodes) {
234 vector<int> plop;
235 plop.clear();
236 return rSolve(sp,0,plop,nodes);
237}
238
239Strategy QSolverUnblockable2::rSolve(Qcop* qs,int scope, vector<int> assignments, unsigned long int& nodes) {
240 nodes++;
241 //cout<<"rSolve for scope "<<scope<<" with assignments ";
242 // for (int i=0;i<assignments.size();i++) cout<<assignments[i]<<" ";
243 // cout<<endl;
244 //////////////////////////////////////////////////////////////////////////////////////////
245 // First case : Unblockable QCSP+ : Goal checking. //
246 // If the goal is failed, even before the end on f the search, we fail. //
247 //////////////////////////////////////////////////////////////////////////////////////////
248 MySpace* g = qs->getGoal();
249 if (g == NULL) {return Strategy(StrategyNode::SFalse());}
250 for (int i=0;i<assignments.size();i++) {
251 switch (g->type_of_v[i]) {
252 case VTYPE_INT :
253 rel(*g,*(static_cast<IntVar*>(g->v[i])) == assignments[i]);
254 break;
255 case VTYPE_BOOL :
256 rel(*g,*(static_cast<BoolVar*>(g->v[i])) == assignments[i]);
257 break;
258 default :
259 cout<<"1Unknown variable type"<<endl;
260 abort();
261 }
262 }
263 if (g->status() == SS_FAILED) {
264 delete g;
265 return Strategy(StrategyNode::SFalse());
266 }
267 delete g;
268
269 if (scope == qs->spaces()) {
270 return Strategy(StrategyNode::STrue());
271 }
272
273 /////////////////////////////////////////////////////////////////////////////////////////
274 // Second case : we are in the middle of the problem... //
275 /////////////////////////////////////////////////////////////////////////////////////////
276 else {
277 MySpace* espace = qs->getSpace(scope);
278 if (espace == NULL) cout<<"I caught a NULL for scope "<<scope<<". I will crash..."<<endl;
279 for (int i=0;i<assignments.size();i++) {
280 switch (espace->type_of_v[i]) {
281 case VTYPE_INT :
282 rel(*espace,*(static_cast<IntVar*>(espace->v[i])) == assignments[i]);
283 break;
284 case VTYPE_BOOL :
285 rel(*espace,*(static_cast<BoolVar*>(espace->v[i])) == assignments[i]);
286 break;
287 default :
288 cout<<"2Unknown variable type"<<endl;
289 abort();
290 }
291 }
292
293 // Second case, first subcase : current scope is universal
294 /////////////////////////////////////////////////////////
295 if (qs->quantification(scope)) {
296 if (espace->status() == SS_FAILED) {
297 delete espace;
298 return Strategy(StrategyNode::STrue());
299 }
300
301 DFS<MySpace> solutions(espace);
302 MySpace* sol = solutions.next();
303 if (sol == NULL) {
304 delete espace;
305 return Strategy(StrategyNode::STrue());
306 }
307
308 Strategy retour = StrategyNode::Dummy();
309 while (sol != NULL) {
310 vector<int> assign;
311 for (int i = 0; i<sp->nbVarInScope(scope);i++) {
312 switch (sol->type_of_v[i]) {
313 case VTYPE_INT :
314 assign.push_back( (static_cast<IntVar*>(sol->v[i]))->val() );
315 break;
316 case VTYPE_BOOL :
317 assign.push_back( (static_cast<BoolVar*>(sol->v[i]))->val() );
318 break;
319 default :
320 cout<<"3Unknown variable type"<<endl;
321 abort();
322 }
323 }
324
325 int vmin = ( (scope==0)? 0 : (qs->nbVarInScope(scope-1)) );
326 int vmax = (qs->nbVarInScope(scope))-1;
327 vector<int> zevalues;
328 for (int i = vmin; i<=vmax;i++) {
329 switch (sol->type_of_v[i]) {
330 case VTYPE_INT :
331 zevalues.push_back( (static_cast<IntVar*>(sol->v[i]))->val() );
332 break;
333 case VTYPE_BOOL :
334 zevalues.push_back( (static_cast<BoolVar*>(sol->v[i]))->val() );
335 break;
336 default :
337 cout<<"4Unknown variable type"<<endl;
338 abort();
339 }
340 }
341 Strategy toAttach(true,vmin,vmax,scope,zevalues);
342
343 Strategy son = rSolve(qs,scope+1,assign,nodes);
344 if (son.isFalse()) {
345 delete sol;
346 delete espace;
347 return Strategy(StrategyNode::SFalse());
348 }
349 toAttach.attach(son);
350 retour.attach(toAttach);
351 delete sol;
352 sol = solutions.next();
353 } // end of while
354 delete espace;
355 return retour;
356 } // end of if(universal)
357
358 // Second case, second subcase : current scope is existential
359 ////////////////////////////////////////////////////////////
360 else {
361 if ((espace->status()) == SS_FAILED) {
362 delete espace;
363 return Strategy(StrategyNode::SFalse());
364 }
365
366 DFS<MySpace> solutions(espace);
367 MySpace* sol =solutions.next();
368 if (sol == NULL) {
369 delete espace;
370 return Strategy(StrategyNode::SFalse());
371 }
372 while (sol != NULL) {
373 vector<int> assign;
374 for (int i = 0; i<sp->nbVarInScope(scope);i++) {
375 // cout << "i = "<<i<<endl;
376 switch (sol->type_of_v[i]) {
377 case VTYPE_INT :
378 assign.push_back( (static_cast<IntVar*>(sol->v[i]))->val() );
379 break;
380 case VTYPE_BOOL :
381 assign.push_back( (static_cast<BoolVar*>(sol->v[i]))->val() );
382 break;
383 default :
384 cout<<"5Unknown variable type"<<endl;
385 abort();
386 }
387 } // end for
388
389 int vmin = ( (scope==0)?0 : qs->nbVarInScope(scope-1) );
390 int vmax = qs->nbVarInScope(scope)-1;
391 vector<int> zevalues;
392 for (int i = vmin; i<=vmax;i++) {
393 switch (sol->type_of_v[i]) {
394 case VTYPE_INT :
395 zevalues.push_back( (static_cast<IntVar*>(sol->v[i]))->val() );
396 break;
397 case VTYPE_BOOL :
398 zevalues.push_back( (static_cast<BoolVar*>(sol->v[i]))->val() );
399 break;
400 default :
401 cout<<"6unknown Variable type"<<endl;
402 abort();
403 }
404 }
405 Strategy candidate(false,vmin,vmax,scope,zevalues);
406
407 Strategy son_of_candidate = rSolve(qs,scope+1,assign,nodes);
408 if (son_of_candidate.isFalse()) candidate = Strategy::SFalse();
409 else candidate.attach(son_of_candidate);
410
411 if (!candidate.isFalse()) {
412 delete sol;
413 delete espace;
414 return candidate;
415 }
416 delete sol;
417 sol=solutions.next();
418 } // end while sol != null
419 delete espace;
420 return Strategy(StrategyNode::SFalse());
421 } // end if..else (existential)
422 }// end "Second case"
423}