00001 #include "synnaeve.guillame.bert.h"
00002 #include "unification.h"
00003 #include <assert.h>
00004 #include <iostream>
00005 #include <string>
00006 #include <climits>
00007
00008 namespace Solver
00009 {
00010
00011 bool Vertex::setBounds(int min,int max)
00012 {
00013 bool ch = false;
00014 if(min>this->min)
00015 { this->min = min; ch = true; }
00016 if(max<this->max)
00017 { this->max = max; ch = true; }
00018 return ch;
00019 }
00020
00021 bool Vertex::setBoundMin(int min)
00022 {
00023 if(min>this->min)
00024 { this->min = min; return true; }
00025 return false;
00026 }
00027
00028 bool Vertex::setBoundMax(int max)
00029 {
00030 if(max<this->max)
00031 { this->max = max; return true; }
00032 return false;
00033 }
00034
00035 Graph::Graph(Node* node,Unification *unification)
00036 {
00037 this->unification = unification;
00038 solus = new SolverSolution();
00039 solus->unification = unification;
00040
00041
00042
00043 Vertex *v0 = addVertex(0);
00044 Vertex *v1 = addVertex(1);
00045 Vertex *v2 = addVertex(2);
00046 Vertex *v3 = addVertex(3);
00047 Vertex *v4 = addVertex(4);
00048 Vertex *v5 = addVertex(5);
00049 Vertex *v6 = addVertex(-1);
00050 Vertex *v7 = addVertex(-2);
00051
00052 addEdge(v0,v1,2,0);
00053
00054 addEdge(v1,v7,1,0);
00055 addEdge(v2,v7,1,0);
00056 addEdge(v3,v7,-1,0);
00057
00058 addEdge(v0,v6,1,0);
00059 addEdge(v5,v6,1,0);
00060 addEdge(v4,v6,-1,0);
00061
00062 addEdge(v4,v3,1,2);
00063
00064 success = true;
00065 solus->ndvar = 0;
00066 return;
00067
00068 solus->ndvar = unification->parser->variabletab.size();
00069 solus->variableSolution = new VariableSolution[solus->ndvar];
00070 success = explo(node);
00071 }
00072
00073 Vertex* Graph::addVertex(int id)
00074 {
00075 if(id>=0)
00076 {
00077 list<Vertex*>::iterator it = vertexs.begin();
00078 while(it!=vertexs.end())
00079 {
00080 if((*it)->variable==id)
00081 return *it;
00082 it++;
00083 }
00084 }
00085
00086 Vertex *v = new Vertex();
00087 v->count = 0;
00088 v->variable = id;
00089 v->min = (unification->configuration->NcanbeZero)?0:1;
00090 v->max = INT_MAX;
00091 v->father = NULL;
00092 v->visited = false;
00093 this->vertexs.push_back(v);
00094 return v;
00095 }
00096
00097 Edge* Graph::addEdge(Vertex *v1,Vertex *v2,int a,int b)
00098 {
00099 Edge *e = new Edge();
00100 e->a = a;
00101 e->b = b;
00102 e->n1 = v1;
00103 e->n2 = v2;
00104 v1->out.push_back(e);
00105 v2->in.push_back(e);
00106 this->edges.push_back(e);
00107 return e;
00108 }
00109
00110 bool Graph::explo(Node* n)
00111 {
00112 bool val = true;
00113 int first = (unification->configuration->NcanbeZero)?0:1;
00114
00115 if(typeid(*n)==typeid(Clash))
00116 val = false;
00117 else if(typeid(*n)==typeid(Trivial))
00118 val = true;
00119 else if(typeid(*n)==typeid(Equal))
00120 {
00121 Equal *e = (Equal*)n;
00122 val = true;
00123 if(typeid(*e->n1)==typeid(Variable))
00124 solus->variableSolution[((Variable*)(e->n1))->id].definition = e->n2;
00125 else
00126 return false;
00127
00128 if(!explo(e->n2))
00129 val = false;
00130 }
00131 else if(typeid(*n)==typeid(And))
00132 {
00133 And *a = (And*)n;
00134 val = true;
00135 list<Node*>::iterator it = a->branchs.begin();
00136 while(it!=a->branchs.end())
00137 {
00138 if(!explo(*it))
00139 {
00140 val = false;
00141 break;
00142 }
00143 it++;
00144 }
00145 list<Condition*>::iterator it2 = a->conditions.begin();
00146 while(it2!=a->conditions.end())
00147 {
00148 Vertex *v = addVertex((*it2)->n1->id);
00149
00150 if(typeid(**it2)==typeid(CondANplusB))
00151 {
00152 Edge *e = addEdge(addVertex(((CondANplusB*)(*it2))->n2->id),v,((CondANplusB*)(*it2))->a,((CondANplusB*)(*it2))->b);
00153 if((e->a<0)&&(e->b<=0))
00154 {
00155 e->n1->setBoundMax(-(e->b-first)/e->a);
00156 e->n2->setBoundMax(e->b + e->a*first);
00157 }
00158 else
00159 if((e->a<0)&&(e->b<0))
00160 if(first==0)
00161 {
00162 e->n1->setBounds(0,0);
00163 e->n2->setBounds(0,0);
00164 }
00165 else
00166 return false;
00167 }
00168 else if(typeid(**it2)==typeid(CondNplusN))
00169 {
00170 Vertex *onode = addVertex(-1);
00171 addEdge(v,onode,-1,0);
00172 addEdge(addVertex(((CondNplusN*)(*it2))->n2->id),onode,1,0);
00173 addEdge(addVertex(((CondNplusN*)(*it2))->n3->id),onode,1,0);
00174 }
00175 else if(typeid(**it2)==typeid(CondN))
00176 addEdge(addVertex(((CondANplusB*)(*it2))->n2->id),v,1,0);
00177 else if(typeid(**it2)==typeid(CondA))
00178 v->setBounds(((CondA*)(*it2))->a,((CondA*)(*it2))->a);
00179 it2++;
00180 }
00181 }
00182 else if(typeid(*n)==typeid(Function))
00183 {
00184 Function *f = (Function*)n;
00185 vector<Node*>::iterator it = f->arguments.begin();
00186 val = true;
00187 while(it!=f->arguments.end())
00188 {
00189 if(!explo(*it))
00190 {
00191 val = false;
00192 break;
00193 }
00194 it++;
00195 }
00196 }
00197 else if(typeid(*n)==typeid(Or))
00198 {
00199 assert(false);
00200 }
00201 else if(typeid(*n)==typeid(Expo))
00202 {
00203 Expo *e = (Expo*)n;
00204 val = explo(e->n1);
00205 if(!explo(e->n2))
00206 val = false;
00207 if(e->free)
00208 addVertex(e->var->id);
00209
00210 }
00211 else if(typeid(*n)==typeid(Variable))
00212 {
00213 Variable *v = (Variable*)n;
00214 solus->variableSolution[v->id].seeoutside = true;
00215 val = true;
00216 }
00217 return val;
00218 }
00219
00220 SolverSolution *Graph::run()
00221 {
00222 if(!success)
00223 {
00224 solus->success = false;
00225 return solus;
00226 }
00227
00228 cout << "NDNoeuds:" << this->vertexs.size() << endl;
00229 cout << "NDarcs:" << this->edges.size() << endl;
00230 cout << endl;
00231
00232 print();
00233
00234 list<Vertex*> vertexs;
00235 list<Edge*> edges;
00236 while(seekCycle(vertexs,edges))
00237 {
00238 cout << "Cycle : " << vertexs.size() << " "<< edges.size() <<endl;
00239 cout << " ";
00240 list<Vertex*>::iterator it;
00241 it = vertexs.begin();
00242 while(it!=vertexs.end())
00243 {
00244 cout << (*it)->variable;
00245 it++;
00246 }
00247 cout << endl;
00248
00249 list<Contribution> contribution;
00250 list<Contribution>::iterator it3;
00251
00252 list<Edge*>::iterator it2 = edges.begin();
00253 float a = 1;
00254 float b = 0;
00255 Vertex *prec;
00256
00257 it = vertexs.end();
00258 it--;
00259 it--;
00260 Vertex *cur = *it;
00261
00262 it = vertexs.begin();
00263 while(it2!=edges.end())
00264 {
00265 prec = cur;
00266 cur = *it;
00267 it++;
00268
00269 if(cur->variable<0)
00270 {
00271 list<Edge*>::iterator it4;
00272 it4 = cur->in.begin();
00273 while(it4!=cur->in.end())
00274 {
00275 if((((*it4)->n1)!=prec)&&(((*it4)->n1)!=(*(it))))
00276 {
00277 Contribution tmp;
00278 tmp.a = (float)(*it4)->a;
00279 b += (float)(*it4)->b;
00280 tmp.v = cur;
00281 contribution.push_back(tmp);
00282 }
00283 it4++;
00284 }
00285
00286 it4 = cur->out.begin();
00287 while(it4!=cur->out.end())
00288 {
00289 if((((*it4)->n2)!=prec)&&(((*it4)->n2)!=(*(it))))
00290 {
00291 Contribution tmp;
00292 tmp.a = (float)-(*it4)->a;
00293 b += (float)-(*it4)->b;
00294 tmp.v = cur;
00295 contribution.push_back(tmp);
00296 }
00297 it4++;
00298 }
00299 }
00300
00301 float way = (cur==(*it2)->n1)?1.f:-1.f;
00302
00303
00304 if(way==1)
00305 {
00306 a *= (*it2)->a;
00307 b *= (*it2)->a;
00308 b += (*it2)->b;
00309 }
00310 else
00311 {
00312 a /= (*it2)->a;
00313 b /= (*it2)->a;
00314 b -= (*it2)->b/(*it2)->a;
00315 }
00316
00317 it3 = contribution.begin();
00318 while(it3!=contribution.end())
00319 {
00320 if(way==1)
00321 (*it3).a *= (*it2)->a;
00322 else
00323 (*it3).a /= (*it2)->a;
00324 it3++;
00325 }
00326
00327 it2++;
00328 }
00329 a--;
00330
00331 if(contribution.empty())
00332 {
00333 if(b!=0)
00334 {
00335 solus->success = false;
00336 return solus;
00337 }
00338 if(a!=1)
00339 {
00340 solus->success = false;
00341 return solus;
00342 }
00343 else
00344 {
00345 if(!unification->configuration->NcanbeZero)
00346 {
00347 solus->success = false;
00348 return solus;
00349 }
00350 else
00351 {
00352 vertexs.front()->setBounds(0,0);
00353
00354 }
00355 }
00356 }
00357 else
00358 {
00359
00360
00361 }
00362
00363 contribution.clear();
00364 vertexs.clear();
00365 edges.clear();
00366 }
00367
00368 cout << "Plus de cycle" << endl;
00369 print();
00370
00371 return solus;
00372 }
00373
00374 bool SolverSolution::check()
00375 {
00376 return success;
00377 }
00378
00379 void SolverSolution::display(ostream &o)
00380 {
00381 unsigned int i;
00382 for(i=0;i<ndvar;i++)
00383 {
00384 o << " " << unification->parser->variabletab[i].name << " = ";
00385 if(!variableSolution[i].definition)
00386 o << "*free*";
00387 else
00388 variableSolution[i].definition->print(o);
00389 o << endl;
00390 }
00391 }
00392
00393 Graph::~Graph()
00394 {
00395 }
00396
00397 bool Graph::seekCycle(list<Vertex*> &ver,list<Edge*> &ed)
00398 {
00399 if(vertexs.empty())
00400 return false;
00401
00402 resetVisited();
00403
00404 list<Vertex*> tovisit;
00405 vertexs.front()->visited = true;
00406 tovisit.push_back(vertexs.front());
00407 Vertex *v;
00408 Vertex *v2;
00409 Edge *e;
00410
00411 while(!tovisit.empty())
00412 {
00413 v = tovisit.back();
00414 tovisit.pop_back();
00415
00416 list<Edge*>::iterator it2;
00417
00418 it2 = v->in.begin();
00419 while(it2!=v->in.end())
00420 {
00421 if(*it2!=v->father)
00422 {
00423 tovisit.push_back((*it2)->n1);
00424 if((*it2)->n1->visited)
00425 {
00426 e = *it2;
00427 v2 = (*it2)->n1;
00428 goto buildpath;
00429 }
00430 (*it2)->n1->father = *it2;
00431 (*it2)->n1->visited = true;
00432 }
00433 it2++;
00434 }
00435
00436 it2 = v->out.begin();
00437 while(it2!=v->out.end())
00438 {
00439 if(*it2!=v->father)
00440 {
00441 tovisit.push_back((*it2)->n2);
00442 if((*it2)->n2->visited)
00443 {
00444 e = *it2;
00445 v2 = (*it2)->n2;
00446 goto buildpath;
00447 }
00448 (*it2)->n2->father = *it2;
00449 (*it2)->n2->visited = true;
00450 }
00451 it2++;
00452 }
00453 }
00454 return false;
00455 buildpath:;
00456
00457 ed.push_back(e);
00458 resetVisited();
00459
00460 Vertex *cur = v2;
00461 while(cur)
00462 {
00463 cur->visited = true;
00464 if(cur->father)
00465 cur = (cur==cur->father->n1)?cur->father->n2:cur->father->n1;
00466 else
00467 cur = NULL;
00468 }
00469
00470 cur = v;
00471 while(!cur->visited)
00472 cur = (cur==cur->father->n1)?cur->father->n2:cur->father->n1;
00473
00474 while(v2!=cur)
00475 {
00476 ver.push_front(v2);
00477 ed.push_front(v2->father);
00478 v2 = (v2==v2->father->n1)?v2->father->n2:v2->father->n1;
00479 }
00480
00481 while(v!=cur)
00482 {
00483 ver.push_back(v);
00484 ed.push_back(v->father);
00485 v = (v==v->father->n1)?v->father->n2:v->father->n1;
00486 }
00487
00488 ver.push_front(cur);
00489 ver.push_back(cur);
00490 return true;
00491 }
00492
00493 void Graph::resetVisited()
00494 {
00495 list<Vertex*>::iterator it = vertexs.begin();
00496 while(it!=vertexs.end())
00497 (*(it++))->visited = false;
00498 }
00499
00500 void Graph::print()
00501 {
00502 cout << " Vertex:" << endl;
00503 list<Vertex*>::iterator it = vertexs.begin();
00504 while(it!=vertexs.end())
00505 {
00506 cout << " " << (*it)->variable << "[" << (*it)->min << "," << (*it)->max << "]" << endl;
00507 it++;
00508 }
00509
00510 cout << " Edges:" << endl;
00511 list<Edge*>::iterator it2 = edges.begin();
00512 while(it2!=edges.end())
00513 {
00514 cout << " " << (*it2)->n1->variable << "\t-[" << (*it2)->a << ";" << (*it2)->b << "]->\t" << (*it2)->n2->variable << endl;
00515 it2++;
00516 }
00517 }
00518
00519 };
00520