00001
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
00014
00015
00016
00017
00018
00019
00020
00021
00022
00023 #include "qsolver.hh"
00024 #include <climits>
00025
00026 QSolver::QSolver(Implicative* sp) {
00027 this->sp = sp;
00028 nbRanges=new int;
00029 }
00030
00031 Strategy QSolver::solve(unsigned long int& nodes) {
00032 vector<int> plop;
00033 plop.clear();
00034 return rSolve(sp,0,plop,nodes);
00035 }
00036
00037 Strategy QSolver::rSolve(Implicative* qs,int scope, vector<int> assignments, unsigned long int& nodes) {
00038 nodes++;
00039
00040
00041
00043
00045 if (scope == qs->spaces()) {
00046
00047 MySpace* g = qs->getGoal();
00048 if (g == NULL) {return Strategy(StrategyNode::SFalse());}
00049 for (int i=0;i<g->nbVars();i++) {
00050 switch (g->type_of_v[i]) {
00051 case VTYPE_INT :
00052 post(g,*(static_cast<IntVar*>(g->v[i])) == assignments[i]);
00053 break;
00054 case VTYPE_BOOL :
00055 post(g,*(static_cast<BoolVar*>(g->v[i])) == assignments[i]);
00056 break;
00057 default :
00058 cout<<"1Unknown variable type"<<endl;
00059 abort();
00060 }
00061 }
00062 if (g->status() == SS_FAILED) {
00063
00064 delete g;
00065 return Strategy(StrategyNode::SFalse());
00066 }
00067
00068 delete g;
00069 return Strategy(StrategyNode::STrue());
00070 }
00071
00073
00075 else {
00076
00077 MySpace* espace = qs->getSpace(scope);
00078 if (espace == NULL) cout<<"I caught a NULL for scope "<<scope<<". I will crash..."<<endl;
00079
00080 for (int i=0;i<assignments.size();i++) {
00081
00082 switch (espace->type_of_v[i]) {
00083 case VTYPE_INT :
00084 post(espace,*(static_cast<IntVar*>(espace->v[i])) == assignments[i]);
00085 break;
00086 case VTYPE_BOOL :
00087 post(espace,*(static_cast<BoolVar*>(espace->v[i])) == assignments[i]);
00088 break;
00089 default :
00090 cout<<"2Unknown variable type"<<endl;
00091 abort();
00092 }
00093 }
00094
00095
00097 if (qs->quantification(scope)) {
00098
00099
00100 if (espace->status() == SS_FAILED) {
00101
00102 delete espace;
00103 return Strategy(StrategyNode::STrue());
00104 }
00105
00106 DFS<MySpace> solutions(espace);
00107 MySpace* sol = solutions.next();
00108 if (sol == NULL) {
00109
00110 delete espace;
00111 return Strategy(StrategyNode::STrue());
00112 }
00113
00114 Strategy retour = StrategyNode::Dummy();
00115 while (sol != NULL) {
00116
00117 vector<int> assign;
00118 for (int i = 0; i<sol->nbVars();i++) {
00119 switch (sol->type_of_v[i]) {
00120 case VTYPE_INT :
00121 assign.push_back( (static_cast<IntVar*>(sol->v[i]))->val() );
00122 break;
00123 case VTYPE_BOOL :
00124 assign.push_back( (static_cast<BoolVar*>(sol->v[i]))->val() );
00125 break;
00126 default :
00127 cout<<"3Unknown variable type"<<endl;
00128 abort();
00129 }
00130 }
00131
00132 int vmin = ( (scope==0)? 0 : (qs->nbVarInScope(scope-1)) );
00133 int vmax = (qs->nbVarInScope(scope))-1;
00134 vector<int> zevalues;
00135 for (int i = vmin; i<=vmax;i++) {
00136 switch (sol->type_of_v[i]) {
00137 case VTYPE_INT :
00138 zevalues.push_back( (static_cast<IntVar*>(sol->v[i]))->val() );
00139 break;
00140 case VTYPE_BOOL :
00141 zevalues.push_back( (static_cast<BoolVar*>(sol->v[i]))->val() );
00142 break;
00143 default :
00144 cout<<"4Unknown variable type"<<endl;
00145 abort();
00146 }
00147 }
00148 Strategy toAttach(true,vmin,vmax,scope,zevalues);
00149
00150 Strategy son = rSolve(qs,scope+1,assign,nodes);
00151 if (son.isFalse()) {
00152
00153 delete sol;
00154 delete espace;
00155 return Strategy(StrategyNode::SFalse());
00156 }
00157
00158 toAttach.attach(son);
00159 retour.attach(toAttach);
00160 delete sol;
00161 sol = solutions.next();
00162 }
00163 delete espace;
00164 return retour;
00165 }
00166
00167
00169 else {
00170
00171 if ((espace->status()) == SS_FAILED) {
00172
00173 delete espace;
00174 return Strategy(StrategyNode::SFalse());
00175 }
00176
00177 DFS<MySpace> solutions(espace);
00178 MySpace* sol =solutions.next();
00179 if (sol == NULL) {
00180
00181 delete espace;
00182 return Strategy(StrategyNode::SFalse());
00183 }
00184
00185 OptVar* opt = qs->getOptVar(scope);
00186 int opttype = qs->getOptType(scope);
00187 Strategy retour(StrategyNode::SFalse());
00188 int score= ( (opttype == 1) ? INT_MAX : INT_MIN );
00189 while (sol != NULL) {
00190
00191 vector<int> assign;
00192 for (int i = 0; i<sol->nbVars();i++) {
00193 switch (sol->type_of_v[i]) {
00194 case VTYPE_INT :
00195 assign.push_back( (static_cast<IntVar*>(sol->v[i]))->val() );
00196 break;
00197 case VTYPE_BOOL :
00198 assign.push_back( (static_cast<BoolVar*>(sol->v[i]))->val() );
00199 break;
00200 default :
00201 cout<<"5Unknown variable type"<<endl;
00202 abort();
00203 }
00204 }
00205
00206 int vmin = ( (scope==0)?0 : qs->nbVarInScope(scope-1) );
00207 int vmax = qs->nbVarInScope(scope)-1;
00208 vector<int> zevalues;
00209 for (int i = vmin; i<=vmax;i++) {
00210 switch (sol->type_of_v[i]) {
00211 case VTYPE_INT :
00212 zevalues.push_back( (static_cast<IntVar*>(sol->v[i]))->val() );
00213 break;
00214 case VTYPE_BOOL :
00215 zevalues.push_back( (static_cast<BoolVar*>(sol->v[i]))->val() );
00216 break;
00217 default :
00218 cout<<"6unknown Variable type"<<endl;
00219 abort();
00220 }
00221 }
00222 Strategy candidate(false,vmin,vmax,scope,zevalues);
00223
00224 Strategy son_of_candidate = rSolve(qs,scope+1,assign,nodes);
00225 if (son_of_candidate.isFalse()) candidate = Strategy::SFalse();
00226 else candidate.attach(son_of_candidate);
00227
00228 int score_of_candidate;
00229 if (candidate.isFalse()) score_of_candidate = ( (opttype == 1) ? INT_MAX : INT_MIN );
00230 else score_of_candidate = opt->getVal(candidate);
00231
00232
00233 switch (opttype) {
00234 case 0 :
00235
00236 if (!candidate.isFalse()) {
00237 delete sol;
00238 delete espace;
00239 return candidate;
00240 }
00241 break;
00242 case 1 :
00243
00244 if (score_of_candidate < score) {
00245 retour=candidate;
00246 score=score_of_candidate;
00247 }
00248 break;
00249 case 2 :
00250
00251 if (score_of_candidate > score) {
00252 retour=candidate;
00253 score=score_of_candidate;
00254 }
00255 break;
00256 default :
00257 cout<<"Unknown opt type : "<<opttype<<endl;
00258 abort();
00259 break;
00260 }
00261 delete sol;
00262 sol=solutions.next();
00263 }
00264 delete espace;
00265 return retour;
00266 }
00267 }
00268 }