this repo has no description
dekker.one
1/**** , [ qsolver_qcop.cc ],
2Copyright (c) 2010 Universite de Caen Basse Normandie - 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_qcop.hh"
24#include <climits>
25
26QCOP_solver::QCOP_solver(Qcop* sp) {
27 this->sp = sp;
28 nbRanges=new int;
29}
30
31Strategy QCOP_solver::solve(unsigned long int& nodes) {
32 vector<int> plop;
33 plop.clear();
34 return rSolve(sp,0,plop,nodes);
35}
36
37Strategy QCOP_solver::rSolve(Qcop* 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 : we reached the goal, we just have to check it //
44 //////////////////////////////////////////////////////////////////////////////////////////
45 if (scope == qs->spaces()) {
46// cout<<"First case"<<endl;
47 MySpace* g = qs->getGoal();
48 if (g == NULL) {/*cout<<"the goal was null"<<endl;*/return Strategy::SFalse();}
49 for (int i=0;i<g->nbVars();i++) {
50 switch (g->type_of_v[i]) {
51 case VTYPE_INT :
52 rel(*g,*(static_cast<IntVar*>(g->v[i])) == assignments[i]);
53 break;
54 case VTYPE_BOOL :
55 rel(*g,*(static_cast<BoolVar*>(g->v[i])) == assignments[i]);
56 break;
57 default :
58 cout<<"1Unknown variable type"<<endl;
59 abort();
60 }
61 }
62 if (g->status() == SS_FAILED) {
63// cout<<"goal failed after assignments"<<endl;
64 delete g;
65 return Strategy::SFalse();
66 }
67// cout<<"goal OK"<<endl;
68 delete g;
69 return Strategy(StrategyNode::STrue());
70 }
71
72 /////////////////////////////////////////////////////////////////////////////////////////
73 // Second case : we are in the middle of the problem... //
74 /////////////////////////////////////////////////////////////////////////////////////////
75 else {
76// cout<<"second case "<<endl;
77 MySpace* espace = qs->getSpace(scope);
78 if (espace == NULL) cout<<"I caught a NULL for scope "<<scope<<". I will crash..."<<endl;
79// cout<<"size of assignments "<<assignments.size()<<endl;
80 for (int i=0;i<assignments.size();i++) {
81// cout<<"I assign variable "<<i<<" with value "<<assignments[i]<<endl; cout.flush();
82 switch (espace->type_of_v[i]) {
83 case VTYPE_INT :
84 rel(*espace,*(static_cast<IntVar*>(espace->v[i])) == assignments[i]);
85 break;
86 case VTYPE_BOOL :
87 rel(*espace,*(static_cast<BoolVar*>(espace->v[i])) == assignments[i]);
88 break;
89 default :
90 cout<<"2Unknown variable type"<<endl;
91 abort();
92 }
93 }
94
95 // Second case, first subcase : current scope is universal
96 /////////////////////////////////////////////////////////
97 if (qs->quantification(scope)) {
98// cout<<"universal"<<endl;
99
100 if (espace->status() == SS_FAILED) {
101// cout<<"the scope is failed"<<endl;
102 delete espace;
103 return Strategy::STrue();
104 }
105
106 DFS<MySpace> solutions(espace);
107 MySpace* sol = solutions.next();
108 if (sol == NULL) {
109// cout<<"first sol is null"<<endl;
110 delete espace;
111 return Strategy::STrue();
112 }
113
114 Strategy retour = Strategy::Dummy();
115 while (sol != NULL) {
116// cout<<"a solution"<<endl;
117 vector<int> assign;
118 for (int i = 0; i<sol->nbVars();i++) {
119 switch (sol->type_of_v[i]) {
120 case VTYPE_INT :
121 assign.push_back( (static_cast<IntVar*>(sol->v[i]))->val() );
122 break;
123 case VTYPE_BOOL :
124 assign.push_back( (static_cast<BoolVar*>(sol->v[i]))->val() );
125 break;
126 default :
127 cout<<"3Unknown variable type"<<endl;
128 abort();
129 }
130 }
131
132 int vmin = ( (scope==0)? 0 : (qs->nbVarInScope(scope-1)) );
133 int vmax = (qs->nbVarInScope(scope))-1;
134 vector<int> zevalues;
135 for (int i = vmin; i<=vmax;i++) {
136 switch (sol->type_of_v[i]) {
137 case VTYPE_INT :
138 zevalues.push_back( (static_cast<IntVar*>(sol->v[i]))->val() );
139 break;
140 case VTYPE_BOOL :
141 zevalues.push_back( (static_cast<BoolVar*>(sol->v[i]))->val() );
142 break;
143 default :
144 cout<<"4Unknown variable type"<<endl;
145 abort();
146 }
147 }
148 Strategy toAttach(true,vmin,vmax,scope,zevalues);
149
150 Strategy son = rSolve(qs,scope+1,assign,nodes);
151 if (son.isFalse()) {
152// cout<<"the son is false"<<endl;
153 delete sol;
154 delete espace;
155 return Strategy::SFalse();
156 }
157// cout<<"the son is true"<<endl;
158 toAttach.attach(son);
159 retour.attach(toAttach);
160 delete sol;
161 sol = solutions.next();
162 } // end of while
163 delete espace;
164 return retour;
165 } // end of if(universal)
166
167 // Second case, second subcase : current scope is existential
168 ////////////////////////////////////////////////////////////
169 else {
170// cout<<"existential"<<endl;
171 if ((espace->status()) == SS_FAILED) {
172// cout<<"the Espace is failed"<<endl;
173 delete espace;
174 return Strategy::SFalse();
175 }
176
177 DFS<MySpace> solutions(espace);
178 MySpace* sol =solutions.next();
179 if (sol == NULL) {
180// cout<<"the first sol is null"<<endl;
181 delete espace;
182 return Strategy::SFalse();
183 }
184
185 OptVar* opt = qs->getOptVar(scope);
186 int opttype = qs->getOptType(scope);
187 Strategy retour(StrategyNode::SFalse());
188 int score= ( (opttype == 1) ? INT_MAX : INT_MIN );
189 while (sol != NULL) {
190// cout<<"une solution"<<endl;
191 vector<int> assign;
192 for (int i = 0; i<sol->nbVars();i++) {
193 switch (sol->type_of_v[i]) {
194 case VTYPE_INT :
195 assign.push_back( (static_cast<IntVar*>(sol->v[i]))->val() );
196 break;
197 case VTYPE_BOOL :
198 assign.push_back( (static_cast<BoolVar*>(sol->v[i]))->val() );
199 break;
200 default :
201 cout<<"5Unknown variable type"<<endl;
202 abort();
203 }
204 } // end for
205
206 int vmin = ( (scope==0)?0 : qs->nbVarInScope(scope-1) );
207 int vmax = qs->nbVarInScope(scope)-1;
208 vector<int> zevalues;
209 for (int i = vmin; i<=vmax;i++) {
210 switch (sol->type_of_v[i]) {
211 case VTYPE_INT :
212 zevalues.push_back( (static_cast<IntVar*>(sol->v[i]))->val() );
213 break;
214 case VTYPE_BOOL :
215 zevalues.push_back( (static_cast<BoolVar*>(sol->v[i]))->val() );
216 break;
217 default :
218 cout<<"6unknown Variable type"<<endl;
219 abort();
220 }
221 }
222 Strategy candidate(false,vmin,vmax,scope,zevalues);
223
224 Strategy son_of_candidate = rSolve(qs,scope+1,assign,nodes);
225 if (son_of_candidate.isFalse()) candidate = Strategy::SFalse();
226 else candidate.attach(son_of_candidate);
227
228 int score_of_candidate;
229 if (candidate.isFalse()) score_of_candidate = ( (opttype == 1) ? INT_MAX : INT_MIN );
230 else score_of_candidate = opt->getVal(candidate);
231// cout<<"score of candidate is "<<score_of_candidate<<endl;
232// cout<<"Opt type is";
233 switch (opttype) {
234 case 0 : // ANY
235// cout<<"ANY"<<endl;
236 if (!candidate.isFalse()) {
237 delete sol;
238 delete espace;
239 return candidate;
240 }
241 break;
242 case 1 : // MIN
243// cout<<"MIN"<<endl;
244 if (score_of_candidate < score) {
245 retour=candidate;
246 score=score_of_candidate;
247 }
248 break;
249 case 2 : // MAX
250// cout<<"MAX"<<endl;
251 if (score_of_candidate > score) {
252 retour=candidate;
253 score=score_of_candidate;
254 }
255 break;
256 default :
257 cout<<"Unknown opt type : "<<opttype<<endl;
258 abort();
259 break;
260 } // end switch
261 delete sol;
262 sol=solutions.next();
263 } // end while
264 delete espace;
265 return retour;
266 } // end if..else (existential)
267 }// end "Second case"
268}