00001 #include "unification.h"
00002 #include "exception.h"
00003 #include "display.h"
00004 #include <iostream>
00005 #include <typeinfo>
00006 #include <time.h>
00007 #include "synnaeve.guillame.bert.h"
00008 #include "automata.h"
00009 #include <map>
00010 #include <string.h>
00011
00012 #ifdef WIN32
00013 #include <windows.h>
00014 #else
00015
00016 #endif
00017
00018 Unification::Unification(Configuration *configuration,Parser *parser)
00019 {
00020 this->configuration = configuration;
00021 this->parser = parser;
00022 }
00023
00027 void Unification::debugDisplay(ostream &s)
00028 {
00029 if(globconfig->writeMode==Configuration::LATEX)
00030 s << "$";
00031
00032 if(typeid(*parser->result)==typeid(And))
00033 dynamic_cast<And*>(parser->result)->printNoBracket(s);
00034 else
00035 parser->result->print(s);
00036
00037 if(globconfig->writeMode==Configuration::LATEX)
00038 s << "$\\\\";
00039
00040 s << endl;
00041
00042
00043
00044
00045
00046
00047
00048
00049
00050
00051 }
00052
00056 Node* Unification::SetDisjunctiveSystem(Node *start)
00057 {
00058 if(!start)
00059 start = parser->result;
00060
00061 Node *ret = start;
00062
00063 bool action = false;
00064 bool nothingtodo;
00065 do
00066 {
00067 nothingtodo = true;
00068 NodeIterator it(ret,&ret,NodeIterator::BREADTH_FIRST);
00069 Node *cur;
00070
00071 while((cur=it.next()))
00072 {
00073 if(typeid(*cur)==typeid(And))
00074 {
00075 list<Node*>::iterator it2 = ((And*)cur)->branchs.begin();
00076 while(it2!=((And*)cur)->branchs.end())
00077 {
00078 if(typeid(*(*it2))==typeid(Or))
00079 {
00080
00081 Or *newOr = new Or();
00082 list<Node*>::iterator it3 = ((Or*)(*it2))->branchs.begin();
00083 while(it3!=((Or*)(*it2))->branchs.end())
00084 {
00085 And *newAnd = new And();
00086 bool last = ((*it3)==((Or*)(*it2))->branchs.back());
00087
00088 newAnd->addBranch(*it3);
00089
00090
00091 list<Condition*>::iterator it5 = ((And*)cur)->conditions.begin();
00092 while(it5!=((And*)cur)->conditions.end())
00093 {
00094 newAnd->addCondition((*it5)->duplicate());
00095
00096
00097 it5++;
00098 }
00099
00100
00101 list<Node*>::iterator it4 = ((And*)cur)->branchs.begin();
00102 while(it4!=((And*)cur)->branchs.end())
00103 {
00104 if(it4!=it2)
00105 newAnd->addBranch((*it4)->duplicate());
00106
00107
00108 it4++;
00109 }
00110
00111 newOr->addBranch(newAnd);
00112
00113 if(last)
00114 break;
00115
00116 it3++;
00117 }
00118
00119 it.replaceBy(newOr);
00120 action = true;
00121 nothingtodo = false;
00122 goto endthisloop;
00123 }
00124 it2++;
00125 }
00126 }
00127 }
00128 endthisloop:;
00129 ret = ApplyR0(ret);
00130 }
00131 while(!nothingtodo);
00132 return ret;
00133 }
00134
00138 Node* Unification::ApplyR0(Node *start)
00139 {
00140 if(!start)
00141 start = parser->result;
00142
00143 Node *ret = start;
00144
00145 bool nothingtodo;
00146 do
00147 {
00148 nothingtodo = true;
00149 NodeIterator it(ret,&ret,NodeIterator::DEPTH_FIRST);
00150 it.setUnderEqual(true);
00151 Node *cur;
00152
00153 while((cur=it.next()))
00154 {
00155 if(typeid(*cur)==typeid(And))
00156 {
00157 if((((And*)cur)->branchs.size()==1)&&(((And*)cur)->conditions.empty()))
00158 {
00159 it.replaceBy(((And*)cur)->branchs.front());
00160 delete cur;
00161 nothingtodo = false;
00162 goto endthisloop;
00163 }
00164 list<Node*>::iterator it2 = ((And*)cur)->branchs.begin();
00165 while(it2!=((And*)cur)->branchs.end())
00166 {
00167 if(typeid(*(*it2))==typeid(And))
00168 {
00169 And *subAnd = (And*)(*it2);
00170 ((And*)cur)->branchs.erase(it2);
00171
00172 list<Node*>::iterator it3 = subAnd->branchs.begin();
00173 while(it3!=subAnd->branchs.end())
00174 {
00175 ((And*)cur)->branchs.push_back(*it3);
00176 it3++;
00177 }
00178
00179 list<Condition*>::iterator it4 = subAnd->conditions.begin();
00180 while(it4!=subAnd->conditions.end())
00181 {
00182 ((And*)cur)->conditions.push_back(*it4);
00183 it4++;
00184 }
00185
00186 nothingtodo = false;
00187 goto endthisloop;
00188 }
00189 if(typeid(*(*it2))==typeid(Clash))
00190 {
00191 it.replaceBy(new Clash());
00192 nothingtodo = false;
00193 goto endthisloop;
00194 }
00195 if(typeid(*(*it2))==typeid(Trivial))
00196 {
00197 ((And*)cur)->branchs.erase(it2);
00198 nothingtodo = false;
00199 goto endthisloop;
00200 }
00201 it2++;
00202 }
00203 }
00204
00205 if(typeid(*cur)==typeid(Expo))
00206 if(!((Expo*)cur)->free)
00207 {
00208 if(((Expo*)cur)->expNum==0)
00209 {
00210
00211 it.replaceBy(((Expo*)cur)->n2);
00212 nothingtodo = false;
00213 goto endthisloop;
00214 }
00215 else
00216 {
00217 Node *n = ((Expo*)cur)->build(((Expo*)cur)->expNum,NULL);
00218
00219 it.replaceBy(n);
00220 nothingtodo = false;
00221 goto endthisloop;
00222 }
00223 }
00224
00225 if(typeid(*cur)==typeid(Or))
00226 {
00227 if(((Or*)cur)->branchs.size()==1)
00228 {
00229 it.replaceBy(((Or*)cur)->branchs.front());
00230 delete cur;
00231 nothingtodo = false;
00232 goto endthisloop;
00233 }
00234 list<Node*>::iterator it2 = ((Or*)cur)->branchs.begin();
00235 while(it2!=((Or*)cur)->branchs.end())
00236 {
00237 if(typeid(*(*it2))==typeid(Or))
00238 {
00239 Or *subOr = (Or*)(*it2);
00240 ((Or*)cur)->branchs.erase(it2);
00241
00242 list<Node*>::iterator it3 = subOr->branchs.begin();
00243 while(it3!=subOr->branchs.end())
00244 {
00245 ((Or*)cur)->branchs.push_back(*it3);
00246 it3++;
00247 }
00248
00249 nothingtodo = false;
00250 goto endthisloop;
00251 }
00252 if(typeid(*(*it2))==typeid(Trivial))
00253 {
00254 it.replaceBy(new Clash());
00255 nothingtodo = false;
00256 goto endthisloop;
00257 }
00258 if(typeid(*(*it2))==typeid(Clash))
00259 {
00260 ((And*)cur)->branchs.erase(it2);
00261 nothingtodo = false;
00262 goto endthisloop;
00263 }
00264 it2++;
00265 }
00266 }
00267 }
00268 endthisloop:;
00269 }
00270 while(!nothingtodo);
00271 return ret;
00272 }
00273
00277 bool Unification::tryApplyR1()
00278 {
00279 NodeIterator it(parser->result,&parser->result,NodeIterator::DEPTH_FIRST);
00280 Node *cur;
00281
00282
00283 while((cur=it.next()))
00284 if(typeid(*cur)==typeid(Equal))
00285 {
00286 Equal *e = (Equal*)cur;
00287
00288
00289
00290
00291
00292 if(e->n1->isEqual(e->n2))
00293 {
00294 if(configuration->printRule)
00295 {
00296 Display::texHspace(*mycout);
00297 (*mycout) << "R1 : x = x " << ((configuration->writeMode==Configuration::LATEX)?"\\rightarrow \\top":"-> T") << endl;
00298
00299
00300
00301
00302
00303
00304
00305
00306 }
00307 it.replaceBy(new Trivial());
00308 return true;
00309 }
00310 }
00311
00312
00313 it.reset();
00314 while((cur=it.next()))
00315 if(typeid(*cur)==typeid(Equal))
00316 {
00317 Equal *e = (Equal*)cur;
00318 if((typeid(*e->n1)!=typeid(Variable))&&
00319 (typeid(*e->n2)==typeid(Variable)))
00320 {
00321 if(configuration->printRule)
00322 {
00323 Display::texHspace(*mycout);
00324 (*mycout) << "R1 : s = x " << ((configuration->writeMode==Configuration::LATEX)?"\\rightarrow":"->") << " x = s" << endl;
00325
00326
00327
00328
00329
00330
00331
00332
00333
00334
00335
00336 }
00337 Node *swap = e->n1;
00338 e->n1 = e->n2;
00339 e->n2 = swap;
00340 return true;
00341 }
00342 }
00343
00344
00345 it.reset();
00346 while((cur=it.next()))
00347 if(typeid(*cur)==typeid(Equal))
00348 {
00349 Equal *e = (Equal*)cur;
00350 if((typeid(*e->n1)==typeid(Function))&&
00351 (typeid(*e->n2)==typeid(Function))&&
00352 (((Function*)(e->n1))->id == ((Function*)(e->n2))->id))
00353 {
00354
00355 if(configuration->printRule)
00356 {
00357 Display::texHspace(*mycout);
00358 (*mycout) << "R1 : f(x)=f(y) " << ((configuration->writeMode==Configuration::LATEX)?"\\rightarrow":"->") << " x=y" << endl;
00359
00360
00361
00362
00363
00364
00365
00366
00367
00368
00369
00370 }
00371 And *add = new And();
00372
00373 vector<Node*>::iterator it1 = ((Function*)(e->n1))->arguments.begin();
00374 vector<Node*>::iterator it2 = ((Function*)(e->n2))->arguments.begin();
00375 while(it1!=((Function*)(e->n1))->arguments.end())
00376 {
00377 add->addBranch(new Equal(*it1,*it2));
00378 it1++;
00379 it2++;
00380 }
00381
00382 it.replaceBy(add);
00383 return true;
00384 }
00385 }
00386
00387
00388
00389 it.reset();
00390 while((cur=it.next()))
00391 if(typeid(*cur)==typeid(Equal))
00392 {
00393 Equal *e = (Equal*)cur;
00394 if((typeid(*e->n1)==typeid(Function))&&
00395 (typeid(*e->n2)==typeid(Function))&&
00396 (((Function*)(e->n1))->id != ((Function*)(e->n2))->id))
00397 {
00398 if(configuration->printRule)
00399 {
00400 Display::texHspace(*mycout);
00401 (*mycout) << "R1 : f(x)=g(y) " << ((configuration->writeMode==Configuration::LATEX)?"\\rightarrow \\bot":"-><clash>") << endl;
00402
00403
00404
00405
00406
00407
00408
00409
00410
00411
00412
00413 }
00414 it.replaceBy(new Clash());
00415 return true;
00416 }
00417 }
00418
00419
00420 it.reset();
00421 while((cur=it.next()))
00422 if(typeid(*cur)==typeid(And))
00423 {
00424 And *andd = (And*)cur;
00425
00426 list<Node*>::iterator it1 = andd->branchs.begin();
00427 while(it1!=andd->branchs.end())
00428 {
00429 list<Node*>::iterator it2 = andd->branchs.begin();
00430 while(it2!=andd->branchs.end())
00431 {
00432 if((*it1)!=(*it2))
00433 {
00434 if((typeid(**it1)==typeid(Equal))&&
00435 (typeid(*((Equal*)(*it1))->n1)==typeid(Variable)))
00436 {
00437 Variable *x = (Variable*)((Equal*)(*it1))->n1;
00438 Node *s = ((Equal*)(*it1))->n2;
00439 Node *p = *it2;
00440 if((!s->containVar(x->id))&&
00441 (p->containVar(x->id))&&
00442 ((typeid(*s)!=typeid(Variable))||(p->containVar(((Variable*)(s))->id))))
00443 {
00444 if(configuration->printRule)
00445 {
00446 Display::texHspace(*mycout);
00447 (*mycout) << "R1 : x=s^P " << ((configuration->writeMode==Configuration::LATEX)?"\\rightarrow":"->") << " x=s^P{x->s}" << endl;
00448 Display::texEndl(*mycout);
00449 }
00450 p->replace(x->id,s);
00451 return true;
00452 }
00453 }
00454 }
00455 it2++;
00456 }
00457 it1++;
00458 }
00459 }
00460
00461
00462 it.reset();
00463 while((cur=it.next()))
00464 if(typeid(*cur)==typeid(Equal))
00465 {
00466 Equal *e = (Equal*)cur;
00467 if((typeid(*e->n1)==typeid(Variable))&&
00468 (e->n2->containVar(((Variable*)(e->n1))->id)))
00469 {
00470 if(configuration->printRule)
00471 {
00472 Display::texHspace(*mycout);
00473 (*mycout) << "R1 : x=s et x " << ((configuration->writeMode==Configuration::LATEX)?"\\in s \\rightarrow \\bot":"E s -> <clash>") << endl;
00474
00475
00476
00477
00478
00479
00480
00481
00482
00483
00484
00485 }
00486 it.replaceBy(new Clash());
00487 return true;
00488 }
00489 }
00490 return false;
00491 }
00492
00496 bool Unification::tryApplyR2()
00497 {
00498 NodeIterator it(parser->result,&parser->result,NodeIterator::DEPTH_FIRST);
00499 Node *cur;
00500
00501 while((cur=it.next()))
00502 if(typeid(*cur)==typeid(Equal))
00503 {
00504 Equal *e = (Equal*)cur;
00505 Node *s;
00506 Node *other;
00507 int way = 0;
00508 if((typeid(*(other=e->n2))==typeid(Expo))&&(typeid(*e->n1)!=typeid(Variable)))
00509 s=e->n1;
00510 else if((typeid(*(other=e->n1))==typeid(Expo))&&(typeid(*e->n2)!=typeid(Variable)))
00511 {
00512 s=e->n2;
00513 way = 1;
00514 }
00515 else continue;
00516 rerun:;
00517 Node *curSearchExpo = s;
00518 list<unsigned int>::iterator it2 = other->holePosition->begin();
00519 bool fail = false;
00520
00521 if(typeid(*s)==typeid(Expo))
00522 fail = true;
00523 else
00524 while(it2!=other->holePosition->end())
00525 {
00526 if(typeid(*curSearchExpo)!=typeid(Function))
00527 break;
00528 if(((Function*)curSearchExpo)->arguments.size()<=(*it2))
00529 break;
00530 curSearchExpo = ((Function*)curSearchExpo)->arguments[*it2];
00531 if(typeid(*curSearchExpo)==typeid(Expo))
00532 {
00533 fail = true;
00534 break;
00535 }
00536 it2++;
00537 }
00538
00539 if(fail)
00540 {
00541 if(way==0)
00542 if((typeid(*(other=e->n1))==typeid(Expo))&&(typeid(*e->n2)!=typeid(Variable)))
00543 {
00544 s=e->n2;
00545 way = 1;
00546 goto rerun;
00547 }
00548 continue;
00549 }
00550
00551 if(configuration->printRule)
00552 {
00553 Display::texHspace(*mycout);
00554 (*mycout) << "R2 (Unfold 1) : s = t[@]^N_p.u " << ((configuration->writeMode==Configuration::LATEX)?"\\rightarrow":"->") << " ..." << endl;
00555
00556
00557
00558
00559
00560
00561
00562
00563 }
00564
00565 And *add2 = NULL;
00566 And *add3 = NULL;
00567 int num = (configuration->NcanbeZero)?0:1;
00568 Expo *expoterm = (Expo*)other;
00569
00570 if((expoterm->free)||(expoterm->expNum==num))
00571 {
00572 add2 = new And();
00573 if(expoterm->free)
00574 add2->addCondition(new CondA(expoterm->var->duplicate(),num));
00575
00576 if(configuration->NcanbeZero)
00577 add2->addBranch(new Equal(s->duplicate(),expoterm->n1->duplicate()));
00578 else
00579 add2->addBranch(new Equal(s->duplicate(),expoterm->buildOne()));
00580 }
00581
00582 if((expoterm->free)||(expoterm->expNum>1))
00583 {
00584 add3 = new And();
00585 Expo *newExpo = (Expo *)expoterm->duplicate();
00586
00587 if(newExpo->free)
00588 {
00589 NumericalVar *var = new NumericalVar(parser->genNumericalValName().c_str(),parser);
00590 add3->addCondition(new CondANplusB(expoterm->var->duplicate(),1,var,1));
00591 delete newExpo->var;
00592 newExpo->var = var->duplicate();
00593 }
00594 else
00595 newExpo->expNum--;
00596
00597 add3->addBranch(new Equal(s->duplicate(),expoterm->buildOne(newExpo)));
00598 }
00599
00600
00601 if((add2)&&(!add3))
00602 it.replaceBy(add2);
00603 else if((add3)&&(!add2))
00604 it.replaceBy(add3);
00605 else
00606 {
00607 Or *add = new Or();
00608 add->addBranch(add2);
00609 add->addBranch(add3);
00610 it.replaceBy(add);
00611 }
00612 return true;
00613 }
00614
00615 return false;
00616 }
00617
00618 int Unification::gcd(unsigned int a, unsigned int b)
00619 {
00620 return ( b != 0 ? gcd(b, a % b) : a );
00621 }
00622
00626 bool Unification::prefix(const list<unsigned int> &l1,const list<unsigned int> &l2)
00627 {
00628 if(l1.size()>l2.size())
00629 return false;
00630
00631 list<unsigned int>::const_iterator itp = l1.begin();
00632 list<unsigned int>::const_iterator itq2 = l2.begin();
00633
00634 while(itp!=l1.end())
00635 {
00636 if((*itp)!=(*itq2))
00637 return false;
00638 itq2++;
00639 itp++;
00640 }
00641 return true;
00642 }
00643
00647 list<unsigned int> Unification::append(const list<unsigned int> &l1,const list<unsigned int> &l2)
00648 {
00649 list<unsigned int> ret = l1;
00650 list<unsigned int>::const_iterator it = l2.begin();
00651 while(it!=l2.end())
00652 {
00653 ret.push_back(*it);
00654 it++;
00655 }
00656 return ret;
00657 }
00658
00662 bool Unification::tryApplyR3()
00663 {
00664 NodeIterator it(parser->result,&parser->result,NodeIterator::DEPTH_FIRST);
00665 Node *cur;
00666
00667 while((cur=it.next()))
00668 if(typeid(*cur)==typeid(Equal))
00669 {
00670 int way = 0;
00671 while(way<2)
00672 {
00673 way++;
00674
00675 Equal *e = (Equal*)cur;
00676 Node *u;
00677 Node *v;
00678
00679 if((typeid(*(v=e->n2))==typeid(Expo))&&((u=e->n1)->rhoterm));
00680 else if((typeid(*(v=e->n1))==typeid(Expo))&&((u=e->n2)->rhoterm));
00681 else continue;
00682
00683 NodeIterator it2(u,NULL,NodeIterator::DEPTH_FIRST);
00684 Node *cur2;
00685 while((cur2=it2.next()))
00686 if(typeid(*cur2)==typeid(Expo))
00687 {
00688 const list<unsigned int> p = it2.getPosition();
00689
00690 assert(((Expo*)cur2)->holePosition);
00691 const list<unsigned int> &q1 = *((Expo*)cur2)->holePosition;
00692 const list<unsigned int> &q2 = *v->holePosition;
00693
00694 if((q1.size()!=q2.size())&&(prefix(p,q2)))
00695 {
00696
00697 int i;
00698 int d = gcd((unsigned int)q1.size(),(unsigned int)q2.size());
00699 int alpha1 = (unsigned int)q1.size() / d;
00700 int alpha2 = (unsigned int)q2.size() / d;
00701
00702
00703 if(configuration->printRule)
00704 {
00705 Display::texHspace(*mycout);
00706 (*mycout) << "R3 (Unfold 2) : s[t1[@]^N1_q1.u1]_p = t2[@]^N2_q2.u2 " << ((configuration->writeMode==Configuration::LATEX)?"\\rightarrow":"->") << " ..." << endl;
00707
00708
00709
00710
00711
00712
00713
00714
00715
00716
00717
00718
00719
00720
00721
00722
00723 }
00724
00725 Or *addOr = new Or();
00726
00727 int first = (this->configuration->NcanbeZero)?0:1;
00728
00729 int r1,r2;
00730 for(r1=first;r1<alpha2;r1++)
00731 {
00732 if(((Expo*)cur2)->free)
00733 {
00734 And *addAnd = new And();
00735 addAnd->addCondition(new CondA(((Expo*)cur2)->var->duplicate(),r1));
00736 Node *newTerm = u->duplicate();
00737
00738 Node *curModificationExpNum = newTerm;
00739 list<unsigned int>::const_iterator it3 = p.begin();
00740 while(it3!=p.end())
00741 {
00742 assert(typeid(*curModificationExpNum)==typeid(Function));
00743 curModificationExpNum = ((Function*)curModificationExpNum)->arguments[*it3];
00744 it3++;
00745 }
00746
00747 assert(typeid(*curModificationExpNum)==typeid(Expo));
00748
00749 if(((Expo*)curModificationExpNum)->free)
00750 {
00751 delete ((Expo*)curModificationExpNum)->var;
00752 ((Expo*)curModificationExpNum)->free = false;
00753 }
00754 ((Expo*)curModificationExpNum)->expNum = r1;
00755
00756 addAnd->addBranch(new Equal(newTerm,v->duplicate()));
00757 addOr->addBranch(addAnd);
00758 }
00759 else if(((Expo*)cur2)->expNum==r1)
00760 {
00761 And *addAnd = new And();
00762 addAnd->addBranch(new Equal(u->duplicate(),v->duplicate()));
00763 addOr->addBranch(addAnd);
00764 }
00765 }
00766
00767 for(r2=first;r2<alpha1;r2++)
00768 {
00769 if(((Expo*)v)->free)
00770 {
00771 And *addAnd = new And();
00772 addAnd->addCondition(new CondA(((Expo*)v)->var->duplicate(),r2));
00773
00774 Node *newTerm = v->duplicate();
00775 if(((Expo*)newTerm)->free)
00776 {
00777 delete ((Expo*)newTerm)->var;
00778 ((Expo*)newTerm)->free = false;
00779 }
00780 ((Expo*)newTerm)->expNum = r2;
00781
00782 addAnd->addBranch(new Equal(u->duplicate(),newTerm));
00783 addOr->addBranch(addAnd);
00784 }
00785 else if(((Expo*)v)->expNum==r2)
00786 {
00787 And *addAnd = new And();
00788 addAnd->addBranch(new Equal(u->duplicate(),v->duplicate()));
00789 addOr->addBranch(addAnd);
00790 }
00791 }
00792
00793 for(r2=0;r2<alpha1;r2++)
00794 for(r1=0;r1<alpha2;r1++)
00795 {
00796
00797 And *addAnd = new And();
00798 bool f1 = ((Expo*)cur2)->free;
00799 bool f2 = ((Expo*)v)->free;
00800
00801 NumericalVar *m1;
00802 NumericalVar *m2;
00803
00804 int m1p;
00805 int m2p;
00806
00807 if(f1)
00808 {
00809 m1 = new NumericalVar(parser->genNumericalValName().c_str(),parser);
00810 addAnd->addCondition(new CondANplusB(((Expo*)cur2)->var->duplicate(),alpha2,m1,r1));
00811 }
00812 else
00813 {
00814 m1p = (((Expo*)cur2)->expNum - r1);
00815 if((m1p%alpha2) != 0)
00816 {
00817 delete addAnd;
00818 continue;
00819 }
00820 m1p /= alpha2;
00821 if(m1p<first)
00822 {
00823 delete addAnd;
00824 continue;
00825 }
00826 }
00827
00828 if(f2)
00829 {
00830 m2 = new NumericalVar(parser->genNumericalValName().c_str(),parser);
00831 addAnd->addCondition(new CondANplusB(((Expo*)v)->var->duplicate(),alpha1,m2,r2));
00832 }
00833 else
00834 {
00835 m2p = (((Expo*)v)->expNum - r2) / alpha1;
00836 if((m2p%alpha1) != 0)
00837 {
00838 if(f1)
00839 delete m1;
00840 delete addAnd;
00841 continue;
00842 }
00843 m2p /= alpha1;
00844 if(m2p<first)
00845 {
00846 if(f1)
00847 delete m1;
00848 delete addAnd;
00849 continue;
00850 }
00851 }
00852
00853 Node *t1 = ((Expo*)cur2)->n2->duplicate();
00854 for(i=0;i<r1;i++)
00855 t1 = ((Expo*)cur2)->buildOne(t1);
00856
00857 Node *t2 = ((Expo*)v)->n2->duplicate();
00858 for(i=0;i<r2;i++)
00859 t2 = ((Expo*)v)->buildOne(t2);
00860
00861 Node *h1 = ((Expo*)cur2)->n1->duplicate();
00862 for(i=0;i<alpha2-1;i++)
00863 h1 = ((Expo*)cur2)->buildOne(h1);
00864
00865 Node *h2 = ((Expo*)v)->n1->duplicate();
00866 for(i=0;i<alpha1-1;i++)
00867 h2 = ((Expo*)v)->buildOne(h2);
00868
00869 list<unsigned int> tmp = p;
00870
00871 Node *k;
00872 if(f1)
00873 k = ((Function*)u)->buildOneAndReplace(tmp, new Expo(h1,m1,t1));
00874 else
00875 k = ((Function*)u)->buildOneAndReplace(tmp, new Expo(h1,m1p,t1));
00876
00877 if(f2)
00878 addAnd->addBranch(new Equal(k,new Expo(h2,m2,t2)));
00879 else
00880 addAnd->addBranch(new Equal(k,new Expo(h2,m2p,t2)));
00881
00882 addOr->addBranch(addAnd);
00883 }
00884 it.replaceBy(addOr);
00885 return true;
00886 }
00887 }
00888 }
00889 }
00890 return false;
00891 }
00892
00896 bool Unification::tryApplyR4()
00897 {
00898 NodeIterator it(parser->result,&parser->result,NodeIterator::DEPTH_FIRST);
00899 Node *cur;
00900
00901 while((cur=it.next()))
00902 if(typeid(*cur)==typeid(Equal))
00903 {
00904 int way = 0;
00905 while(way<2)
00906 {
00907 way++;
00908
00909 Equal *e = (Equal*)cur;
00910 Node *u;
00911 Node *v;
00912
00913 if((typeid(*(v=e->n2))==typeid(Expo))&&((u=e->n1)->rhoterm));
00914 else if((typeid(*(v=e->n1))==typeid(Expo))&&((u=e->n2)->rhoterm));
00915 else continue;
00916
00917 NodeIterator it2(u,NULL,NodeIterator::DEPTH_FIRST);
00918 Node *cur2;
00919 while((cur2=it2.next()))
00920 if(typeid(*cur2)==typeid(Expo))
00921 {
00922 const list<unsigned int> p = it2.getPosition();
00923 const list<unsigned int> &q1 = *((Expo*)cur2)->holePosition;
00924 const list<unsigned int> &q2 = *v->holePosition;
00925
00926 if((prefix(p,q2))&&((!prefix(q2,append(p,q1)))||(!prefix(append(p,q1),append(q2,q2)))))
00927 {
00928
00929 if(configuration->printRule)
00930 {
00931 Display::texHspace(*mycout);
00932 (*mycout) << "R4 (Unfold 3) : s[t1[@]^N1_q1.u1]_p = t2[@]^N2_q2.u2 " << ((configuration->writeMode==Configuration::LATEX)?"\\rightarrow":"->") << " ..." << endl;
00933
00934
00935
00936
00937
00938
00939
00940
00941
00942
00943
00944
00945
00946
00947
00948
00949 }
00950
00951 int first = (configuration->NcanbeZero)?0:1;
00952
00953 assert(!configuration->NcanbeZero);
00954
00955 Or *addOr = new Or();
00956
00957 if(((Expo*)v)->free)
00958 {
00959 And *addAnd = new And();
00960 addAnd->addCondition(new CondA(((Expo*)v)->var->duplicate(),1));
00961
00962 addAnd->addBranch(new Equal(((Expo*)v)->buildOne(),((Expo*)u)->duplicate()));
00963 addOr->addBranch(addAnd);
00964 }
00965 else
00966 {
00967 if(((Expo*)v)->expNum==1)
00968 {
00969 And *addAnd = new And();
00970 addAnd->addBranch(new Equal(((Expo*)v)->buildOne(),((Expo*)u)->duplicate()));
00971 addOr->addBranch(addAnd);
00972 }
00973 }
00974
00975 if(((Expo*)cur2)->free)
00976 {
00977 And *addAnd = new And();
00978 addAnd->addCondition(new CondA(((Expo*)cur2)->var->duplicate(),1));
00979
00980 assert(typeid(*u)==typeid(Function));
00981
00982 list<unsigned int> tmp = p;
00983 addAnd->addBranch(new Equal(((Function*)u)->buildOneAndReplace(tmp,((Expo*)cur2)->buildOne()),((Expo*)v)->duplicate()));
00984 addOr->addBranch(addAnd);
00985 }
00986 else
00987 {
00988 if(((Expo*)cur2)->expNum==1)
00989 {
00990 And *addAnd = new And();
00991 list<unsigned int> tmp = p;
00992 addAnd->addBranch(new Equal(((Function*)u)->buildOneAndReplace(tmp,((Expo*)cur2)->buildOne()),((Expo*)v)->duplicate()));
00993 addOr->addBranch(addAnd);
00994 }
00995 }
00996
00997 if(((Expo*)v)->free)
00998 {
00999 And *addAnd = new And();
01000 addAnd->addCondition(new CondA(((Expo*)v)->var->duplicate(),2));
01001
01002 addAnd->addBranch(new Equal(((Expo*)v)->buildTwo(),((Expo*)u)->duplicate()));
01003 addOr->addBranch(addAnd);
01004 }
01005 else
01006 {
01007 if(((Expo*)v)->expNum==2)
01008 {
01009 And *addAnd = new And();
01010 addAnd->addBranch(new Equal(((Expo*)v)->buildOne(),((Expo*)u)->duplicate()));
01011 addOr->addBranch(addAnd);
01012 }
01013 }
01014
01015 bool f1 = ((Expo*)cur2)->free;
01016 bool f2 = ((Expo*)v)->free;
01017
01018 And *addAnd = new And();
01019
01020 NumericalVar *m1 = NULL;
01021 int m1i;
01022 if(f1)
01023 {
01024 m1 = new NumericalVar(parser->genNumericalValName().c_str(),parser);
01025 addAnd->addCondition(new CondANplusB(((Expo*)cur2)->var->duplicate(),1,m1,1));
01026 }
01027 else
01028 {
01029 m1i = ((Expo*)cur2)->expNum-1;
01030 if(m1i<first)
01031 {
01032 delete addAnd;
01033 continue;
01034 }
01035 }
01036
01037 NumericalVar *m2;
01038 int m2i;
01039 if(f2)
01040 {
01041 m2 = new NumericalVar(parser->genNumericalValName().c_str(),parser);
01042 addAnd->addCondition(new CondANplusB(((Expo*)v)->var->duplicate(),1,m2,2));
01043 }
01044 else
01045 {
01046 m2i = ((Expo*)v)->expNum-2;
01047 if(m2i<first)
01048 {
01049 if(f1)
01050 {
01051 delete addAnd->conditions.front();
01052 assert(m1);
01053 delete m1;
01054 }
01055 delete addAnd;
01056 continue;
01057 }
01058 }
01059
01060 Expo *h1 = (Expo*)v->duplicate();
01061 if(f2)
01062 {
01063 delete h1->var;
01064 h1->var = m2;
01065 }
01066 else
01067 h1->expNum = m2i;
01068
01069 Expo *h2 = (Expo*)cur2->duplicate();
01070 if(f1)
01071 {
01072 delete h2->var;
01073 h2->var = m1;
01074 }
01075 else
01076 h2->expNum = m1i;
01077
01078 list<unsigned int> tmp = p;
01079 addAnd->addBranch(new Equal(((Function*)u)->buildOneAndReplace(tmp,((Expo*)cur2)->buildOne(h2)),((Expo*)v)->buildTwo(h1)));
01080 addOr->addBranch(addAnd);
01081
01082 if(addOr->branchs.empty())
01083 {
01084 delete addOr;
01085 continue;
01086 }
01087
01088 it.replaceBy(addOr);
01089 return true;
01090 }
01091 }
01092 }
01093 }
01094 return false;
01095 }
01096
01100 bool Unification::tryApplyR5()
01101 {
01102 NodeIterator it(parser->result,&parser->result,NodeIterator::DEPTH_FIRST);
01103 Node *cur;
01104
01105 while((cur=it.next()))
01106 if(typeid(*cur)==typeid(Equal))
01107 {
01108 Equal *e = (Equal*)cur;
01109 Node *u;
01110 Node *v;
01111
01112 int way = 0;
01113 if((typeid(*(v=e->n2))==typeid(Expo))&&((u=e->n1)->rhoterm))
01114 ;
01115 else if((typeid(*(v=e->n1))==typeid(Expo))&&((u=e->n2)->rhoterm))
01116 way = 1;
01117 else continue;
01118 rerun:;
01119
01120 NodeIterator it2(u,NULL,NodeIterator::DEPTH_FIRST);
01121 Node *cur2;
01122 while((cur2=it2.next()))
01123 if(typeid(*cur2)==typeid(Expo))
01124 {
01125 const list<unsigned int> p = it2.getPosition();
01126 const list<unsigned int> &q1 = *((Expo*)cur2)->holePosition;
01127
01128
01129 if(configuration->printRule)
01130 {
01131 Display::texHspace(*mycout);
01132 (*mycout) << "R5 (Decompose 2) : s[v1[w1[@]_p]^N1_q.u1]_p = (v2[w2[@]_q]_p)^N2.u2 " << ((configuration->writeMode==Configuration::LATEX)?"\\rightarrow":"->") << " ..." << endl;
01133
01134
01135
01136
01137
01138
01139
01140
01141
01142
01143
01144
01145
01146
01147 }
01148
01149 list<unsigned int> qprim;
01150 list<unsigned int>::const_iterator it3 = q1.begin();
01151 int num = q1.size() - p.size();
01152 for(;num>0;num--)
01153 {
01154 qprim.push_back(*it3);
01155 it3++;
01156 }
01157
01158 And *addAnd = new And();
01159
01160 Function *addA = new Function(parser->genContstantValName().c_str(),parser);
01161
01162 list<unsigned int>tmp1;
01163 list<unsigned int>tmp2;
01164 list<unsigned int>tmp3;
01165
01166 Node *w1 = (((Expo*)cur2)->n1)->find(tmp1=qprim);
01167 Node *w2 = (((Expo*)v)->n1)->find(tmp1=p);
01168
01169 addAnd->addBranch(new Equal(
01170 u->buildOneAndReplace(tmp1=p,addA->duplicate()),
01171 w1->buildOneAndReplace(tmp3=p,addA->duplicate())
01172 ));
01173
01174 addAnd->addBranch(new Equal(
01175 u->buildOneAndReplace(tmp1=p,addA->duplicate()),
01176 ((Expo*)v)->n1->buildOneAndReplace(tmp2=p,addA->duplicate())
01177 ));
01178
01179 addAnd->addBranch(new Equal(
01180 ((Expo*)cur2)->n1->buildOneAndReplace(tmp1=qprim,addA->duplicate()),
01181 w2->buildOneAndReplace(tmp2=qprim,addA->duplicate())
01182 ));
01183
01184 Or *addOr = new Or();
01185
01186 bool buildit = true;
01187
01188 And *addAnd2 = new And();
01189 if((!((Expo*)cur2)->free)&&(!((Expo*)v)->free))
01190 {
01191 if(((Expo*)cur2)->expNum==((Expo*)v)->expNum)
01192 ;
01193 else
01194 buildit= false;
01195 }
01196 else
01197 {
01198 if((((Expo*)cur2)->free)&&(((Expo*)v)->free))
01199 addAnd2->addCondition(new CondN(((Expo*)cur2)->var->duplicate(),((Expo*)v)->var->duplicate()));
01200 else if(!((Expo*)cur2)->free)
01201 addAnd2->addCondition(new CondA(((Expo*)v)->var->duplicate(),((Expo*)cur2)->expNum));
01202 else
01203 addAnd2->addCondition(new CondA(((Expo*)cur2)->var->duplicate(),((Expo*)v)->expNum));
01204 }
01205
01206 if(buildit)
01207 {
01208 addAnd2->addBranch(new Equal(u->buildOneAndReplace(tmp1=p,((Expo*)cur2)->n2->duplicate()),((Expo*)v)->n2->duplicate()));
01209 addOr->addBranch(addAnd2);
01210 }
01211 else
01212 delete addAnd2;
01213
01214 int first = (this->configuration->NcanbeZero)?0:1;
01215
01216 addAnd2 = new And();
01217 int m1i;
01218 NumericalVar *m1 = NULL;
01219 if((!((Expo*)cur2)->free)&&(!((Expo*)v)->free))
01220 {
01221 m1i = ((Expo*)cur2)->expNum - ((Expo*)v)->expNum;
01222 if(m1i>=first)
01223 ;
01224 else
01225 buildit= false;
01226 }
01227 else
01228 {
01229 m1 = new NumericalVar(parser->genNumericalValName().c_str(),parser);
01230
01231 if((((Expo*)cur2)->free)&&(((Expo*)v)->free))
01232 addAnd2->addCondition(new CondNplusN(((Expo*)cur2)->var->duplicate(),((Expo*)v)->var->duplicate(),m1->duplicate()));
01233 else if(!((Expo*)cur2)->free)
01234 addAnd2->addCondition(new CondANplusB(((Expo*)v)->var->duplicate(),-1,m1->duplicate(),((Expo*)cur2)->expNum));
01235 else
01236 addAnd2->addCondition(new CondANplusB(((Expo*)cur2)->var->duplicate(),1,m1->duplicate(),((Expo*)v)->expNum));
01237 }
01238
01239 if(buildit)
01240 {
01241 Node *h1 = u->duplicate();
01242
01243 Expo *coup = (Expo*)h1->find(tmp1=p);
01244 assert(typeid(*coup)==typeid(Expo));
01245
01246 coup->free = (m1!=NULL);
01247 if(m1)
01248 coup->var = m1;
01249 else
01250 coup->expNum = m1i;
01251
01252 addAnd2->addBranch(new Equal(h1,((Expo*)v)->n2));
01253 addOr->addBranch(addAnd2);
01254 }
01255 else
01256 delete addAnd2;
01257
01258 addAnd2 = new And();
01259 m1 = NULL;
01260 if((!((Expo*)cur2)->free)&&(!((Expo*)v)->free))
01261 {
01262 m1i = ((Expo*)v)->expNum - ((Expo*)cur2)->expNum;
01263 if(m1i>=first)
01264 ;
01265 else
01266 buildit= false;
01267 }
01268 else
01269 {
01270 m1 = new NumericalVar(parser->genNumericalValName().c_str(),parser);
01271
01272 if((((Expo*)v)->free)&&(((Expo*)cur2)->free))
01273 addAnd2->addCondition(new CondNplusN(((Expo*)v)->var->duplicate(),((Expo*)cur2)->var->duplicate(),m1->duplicate()));
01274 else if(!((Expo*)cur2)->free)
01275 addAnd2->addCondition(new CondANplusB(((Expo*)cur2)->var->duplicate(),-1,m1->duplicate(),((Expo*)v)->expNum));
01276 else
01277 addAnd2->addCondition(new CondANplusB(((Expo*)v)->var->duplicate(),1,m1->duplicate(),((Expo*)cur2)->expNum));
01278 }
01279
01280 if(buildit)
01281 {
01282 Expo *h1 = (Expo*)v->duplicate();
01283
01284 h1->free = (m1!=NULL);
01285 if(m1)
01286 h1->var = m1;
01287 else
01288 h1->expNum = m1i;
01289
01290 addAnd2->addBranch(new Equal(w1->buildOneAndReplace(tmp1=p,((Expo*)cur2)->n2->duplicate()),h1));
01291 addOr->addBranch(addAnd2);
01292 }
01293 else
01294 delete addAnd2;
01295
01296 if(addOr->branchs.empty())
01297 delete addOr;
01298 else
01299 addAnd->addBranch(addOr);
01300
01301
01302 it.replaceBy((Node*)addAnd);
01303 return true;
01304 }
01305
01306 if(way==0)
01307 if((typeid(*(v=e->n1))==typeid(Expo))&&((u=e->n2)->rhoterm))
01308 {
01309 way = 1;
01310 goto rerun;
01311 }
01312 }
01313
01314 return false;
01315 }
01316
01320 bool Unification::exploDefinition(Node *n,SimpleSolution *solution)
01321 {
01322 bool val = true;
01323
01324 if(typeid(*n)==typeid(Clash))
01325 val = false;
01326 else if(typeid(*n)==typeid(Trivial))
01327 val = true;
01328 else if(typeid(*n)==typeid(Equal))
01329 {
01330 Equal *e = (Equal*)n;
01331 val = true;
01332 if(typeid(*e->n1)==typeid(Variable))
01333 solution->variableSolution[((Variable*)(e->n1))->id].definition = e->n2;
01334 else
01335 return false;
01336 if(!exploDefinition(e->n2,solution))
01337 val = false;
01338 }
01339 else if(typeid(*n)==typeid(And))
01340 {
01341 And *a = (And*)n;
01342 val = true;
01343 list<Node*>::iterator it = a->branchs.begin();
01344 while(it!=a->branchs.end())
01345 {
01346 if(!exploDefinition(*it,solution))
01347 {
01348 val = false;
01349 break;
01350 }
01351 it++;
01352 }
01353 list<Condition*>::iterator it2 = a->conditions.begin();
01354 while(it2!=a->conditions.end())
01355 {
01356
01357
01358
01359
01360
01361
01362
01363
01364
01365
01366
01367 solution->numericalvariableSolution[(*it2)->n1->id].definitionc.push_back(*it2);
01368
01369 if(typeid(**it2)==typeid(CondANplusB))
01370 solution->numericalvariableSolution[((CondANplusB*)(*it2))->n2->id].seeoutside = true;
01371 else if(typeid(**it2)==typeid(CondNplusN))
01372 {
01373 solution->numericalvariableSolution[((CondNplusN*)(*it2))->n2->id].seeoutside = true;
01374 solution->numericalvariableSolution[((CondNplusN*)(*it2))->n3->id].seeoutside = true;
01375 }
01376 else if(typeid(**it2)==typeid(CondN))
01377 solution->numericalvariableSolution[((CondN*)(*it2))->n2->id].seeoutside = true;
01378
01379 it2++;
01380 }
01381 }
01382 else if(typeid(*n)==typeid(Function))
01383 {
01384 Function *f = (Function*)n;
01385 vector<Node*>::iterator it = f->arguments.begin();
01386 val = true;
01387 while(it!=f->arguments.end())
01388 {
01389 if(!exploDefinition(*it,solution))
01390 {
01391 val = false;
01392 break;
01393 }
01394 it++;
01395 }
01396 }
01397 else if(typeid(*n)==typeid(Or))
01398 {
01399 assert(false);
01400 }
01401 else if(typeid(*n)==typeid(Expo))
01402 {
01403 Expo *e = (Expo*)n;
01404 val = exploDefinition(e->n1,solution);
01405 if(!exploDefinition(e->n2,solution))
01406 val = false;
01407 if(e->free)
01408 solution->numericalvariableSolution[e->var->id].seeoutside = true;
01409 }
01410 else if(typeid(*n)==typeid(Variable))
01411 {
01412 Variable *v = (Variable*)n;
01413 solution->variableSolution[v->id].seeoutside = true;
01414 val = true;
01415 }
01416 return val;
01417 }
01418
01424 bool Unification::verifValidPresburger(Node* n)
01425 {
01426 #ifdef DEBUG
01427 (*mycout) << "------------------------------------------------------------------------------" << endl;
01428 #endif
01429 if(typeid(*n) == typeid(And)){
01430 list<Automata*> automL;
01431 std::map <int,int> numvars;
01432
01433 list<Condition*>::iterator it = ((And*)n)->conditions.begin();
01434 while(it != ((And*)n)->conditions.end()) {
01435 Condition* tmpc = *it;
01436 if (numvars.find(tmpc->n1->id) == numvars.end())
01437 numvars[tmpc->n1->id] = numvars.size();
01438 if (typeid(*tmpc) == typeid(CondN)) {
01439 if (numvars.find(((CondN*)tmpc)->n2->id) == numvars.end())
01440 numvars[((CondN*)tmpc)->n2->id] = numvars.size();
01441 } else if (typeid(*tmpc) == typeid (CondANplusB)) {
01442 if (numvars.find(((CondANplusB*)tmpc)->n2->id) == numvars.end())
01443 numvars[((CondANplusB*)tmpc)->n2->id] = numvars.size();
01444 } else if (typeid(*tmpc) == typeid (CondNplusN)) {
01445 if (numvars.find(((CondNplusN*)tmpc)->n2->id) == numvars.end())
01446 numvars[((CondNplusN*)tmpc)->n2->id] = numvars.size();
01447 if (numvars.find(((CondNplusN*)tmpc)->n3->id) == numvars.end())
01448 numvars[((CondNplusN*)tmpc)->n3->id] = numvars.size();
01449 }
01450 it++;
01451 }
01452
01453
01454
01455
01456
01457
01458
01459
01460
01461
01462
01463
01464
01465
01466
01467
01468
01469
01470
01471
01472
01473
01474
01475 #ifdef DEBUG
01476 (*mycout) << "==> BITS_SIZE (numvars.size()) : " << numvars.size() << endl;
01477 #endif
01478
01479 it = ((And*)n)->conditions.begin();
01480
01481 while(it != ((And*)n)->conditions.end()) {
01482 Automata* tmp = new Automata(*it, &numvars);
01483 #ifdef DEBUG
01484 tmp->display(*mycout);
01485 #endif
01486 automL.push_back(tmp);
01487 it++;
01488 }
01489
01490
01491
01492
01493
01494 list<Groupe> groupes;
01495 list<Automata*>::iterator it7 = automL.begin();
01496 while(it7!=automL.end())
01497 {
01498 Groupe tmp;
01499 tmp.autos.push_back(*it7);
01500 groupes.push_back(tmp);
01501 it7++;
01502 }
01503
01504 list<Groupe>::iterator itg1,itg2;
01505 list<Automata*>::iterator ita1,ita2;
01506
01507 bool todo;
01508 do
01509 {
01510 todo = false;
01511 itg1 = groupes.begin();
01512 while(itg1!=groupes.end())
01513 {
01514 itg2 = itg1;
01515 if(itg2!=groupes.end())
01516 itg2++;
01517 while(itg2!=groupes.end())
01518 {
01519 ita1 = itg1->autos.begin();
01520 while(ita1!=itg1->autos.end())
01521 {
01522 ita2 = itg2->autos.begin();
01523 while(ita2!=itg2->autos.end())
01524 {
01525 if((*ita1)->isIntersect(*ita2,numvars.size()))
01526 {
01527 todo = true;
01528 (*itg1).autos.push_back(*ita2);
01529 (*itg2).autos.erase(ita2);
01530 if((*itg2).autos.empty())
01531 groupes.erase(itg2);
01532 goto groupeend;
01533 }
01534 ita2++;
01535 }
01536 ita1++;
01537 }
01538 itg2++;
01539 }
01540 itg1++;
01541 }
01542 groupeend:;
01543 }
01544 while(todo);
01545 #ifdef DEBUG
01546 (*mycout) << "NDGroupes : " << groupes.size() << endl;
01547 #endif
01548
01549
01550 itg1 = groupes.begin();
01551 while(itg1!=groupes.end())
01552 {
01553 ExploPara exploPara;
01554 StatePara para;
01555 bool isgooda = false;
01556
01557
01558 list<Automata*>::iterator it2 = itg1->autos.begin();
01559 while(it2!=itg1->autos.end())
01560 {
01561 para.actives.push_back((*it2)->si);
01562 it2++;
01563 }
01564 exploPara.statePara.push_back(para);
01565
01566
01567 while(!exploPara.statePara.empty())
01568 {
01569 para = exploPara.statePara.front();
01570 exploPara.statePara.pop_front();
01571
01572 bool allfinal = true;
01573 list<State*>::iterator it3 = para.actives.begin();
01574 while(it3!=para.actives.end())
01575 {
01576 if((*it3)->value != (*it3)->automata->cvalue)
01577 {
01578 allfinal = false;
01579 break;
01580 }
01581 it3++;
01582 }
01583
01584 if(allfinal)
01585 {
01586 isgooda = true;
01587 goto gooda;
01588 }
01589
01590 State* first = para.actives.front();
01591
01592 if(para.actives.empty())
01593 continue;
01594 if(first->step.empty())
01595 continue;
01596
01597 list<Transition*>::iterator it4 = first->step.begin();
01598 while(it4!=first->step.end())
01599 {
01600 StatePara newPara;
01601 newPara.actives.push_back((*it4)->st);
01602
01603 bool good2 = true;
01604 it3 = para.actives.begin();
01605 it3++;
01606 while(it3!=para.actives.end())
01607 {
01608 bool good = false;
01609 list<Transition*>::iterator it5 = (*it3)->step.begin();
01610 while(it5!=(*it3)->step.end())
01611 {
01612
01613
01614
01615 unsigned int i;
01616 bool err = false;
01617 for(i=0;i<numvars.size();i++)
01618 if(((*it5)->bits[i]==-1)||((*it4)->bits[i]==-1)||((*it4)->bits[i]==(*it5)->bits[i]))
01619 ;
01620 else
01621 err = true;
01622
01623 if(!err)
01624 {
01625 newPara.actives.push_back((*it5)->st);
01626 good = true;
01627 break;
01628 }
01629
01630 it5++;
01631 }
01632
01633 if(!good)
01634 {
01635 good2 = false;
01636 break;
01637 }
01638 it3++;
01639 }
01640
01641 if(!good2)
01642 break;
01643
01644 exploPara.statePara.push_back(newPara);
01645 it4++;
01646 }
01647 }
01648
01649 gooda:;
01650 if(!isgooda)
01651 return false;
01652 itg1++;
01653 }
01654
01655 return true;
01656 }
01657
01658 return true;
01659 }
01660
01664 bool Unification::checkDefinition()
01665 {
01666 if(typeid(*parser->result)==typeid(Or))
01667 {
01668 list<Node*>::iterator it = ((Or*)(parser->result))->branchs.begin();
01669 while(it!=((Or*)(parser->result))->branchs.end())
01670 {
01671 SimpleSolution *sol = new SimpleSolution((unsigned int)parser->variabletab.size(),(unsigned int)parser->numericalvariabletab.size(),this);
01672 solutions.push_back(sol);
01673 sol->fail = !exploDefinition(*it,sol);
01674 if(configuration->presBurgerVerif)
01675 if(!sol->fail)
01676 sol->fail = !verifValidPresburger(*it);
01677
01678
01679
01680
01681 it++;
01682 }
01683 }
01684 else
01685 {
01686 SimpleSolution *sol = new SimpleSolution((unsigned int)parser->variabletab.size(),(unsigned int)parser->numericalvariabletab.size(),this);
01687 solutions.push_back(sol);
01688 sol->fail = !exploDefinition(parser->result,sol);
01689 if(configuration->presBurgerVerif)
01690 if(!sol->fail)
01691 sol->fail = !verifValidPresburger(parser->result);
01692
01693
01694
01695
01696 }
01697
01698 list<Solution*>::iterator it = solutions.begin();
01699 while(it!=solutions.end())
01700 {
01701 if((*it)->check())
01702 it++;
01703 else
01704 it = solutions.erase(it);
01705 }
01706 return !solutions.empty();
01707 }
01708
01712 void SimpleSolution::display(ostream &o)
01713 {
01714 unsigned int i;
01715 for(i=0;i<ndnumvar;i++)
01716 {
01717 if(numericalvariableSolution[i].definitionc.empty())
01718 {
01719 if((numericalvariableSolution[i].seeoutside)||(!unification->parser->numericalvariabletab[i].automatic))
01720 {
01721 o << " " <<unification->parser->numericalvariabletab[i].name << " = *free*";
01722 o << endl;
01723 if(globconfig->writeMode==Configuration::LATEX)
01724 o << endl;
01725 }
01726 }
01727 else
01728 {
01729 list<Condition*>::iterator it = numericalvariableSolution[i].definitionc.begin();
01730 while(it!=numericalvariableSolution[i].definitionc.end())
01731 {
01732 o << " ";
01733 (*it++)->print(o);
01734 o << endl;
01735 if(globconfig->writeMode==Configuration::LATEX)
01736 o << endl;
01737 }
01738 }
01739 }
01740 for(i=0;i<ndvar;i++)
01741 {
01742 o << " " <<unification->parser->variabletab[i].name << " = ";
01743 if(!variableSolution[i].definition)
01744 o << "*free*";
01745 else
01746 variableSolution[i].definition->print(o);
01747 o << endl;
01748 if(globconfig->writeMode==Configuration::LATEX)
01749 o << endl;
01750 }
01751 }
01752
01753 VariableSolution::VariableSolution()
01754 {
01755 seeoutside = false;
01756 definition = NULL;
01757 }
01758
01759 SimpleSolution::SimpleSolution(unsigned int ndvar,unsigned int ndnumvar,Unification *unification)
01760 {
01761 this->unification = unification;
01762 fail = false;
01763 this->ndvar = ndvar;
01764 this->ndnumvar = ndnumvar;
01765 variableSolution = new VariableSolution[ndvar];
01766 numericalvariableSolution = new VariableSolution[ndnumvar];
01767 }
01768
01769 bool SimpleSolution::check()
01770 {
01771 if(fail)
01772 return false;
01773 return true;
01774 }
01775
01776 SimpleSolution::~SimpleSolution()
01777 {
01778 delete[] variableSolution;
01779 delete[] numericalvariableSolution;
01780 }
01781
01785 void Unification::run()
01786 {
01787 result = true;
01788 int step = 0;
01789 long startTime = clock();
01790
01791 Display::texDi(*mycout);
01792 (*mycout) << "Initial set of equation";
01793 Display::texDi(*mycout);
01794 Display::texEndl(*mycout);
01795 (*mycout) << endl;
01796 debugDisplay((*mycout));
01797 Display::texEndl(*mycout);
01798 (*mycout) << endl;
01799
01800 while(true)
01801 {
01802 step++;
01803 if((configuration->pauseEveryStep)||(configuration->printRule))
01804 {
01805 Display::texEndl(*mycout);
01806 (*mycout) << endl;
01807 debugDisplay((*mycout));
01808
01809 (*mycout) << endl;
01810 }
01811
01812 if(configuration->pauseEveryStep)
01813 {
01814 (*mycout) << "==============PAUSE=("<< step <<")===========" << endl;
01815 if(configuration->writeMode==Configuration::LATEX)
01816 (*mycout) << "\\\\";
01817 while(true)
01818 {
01819 (*mycout) << "command:"<<endl;
01820 (*mycout) << " c - continue (default)" << endl;
01821 (*mycout) << " f - finish" << endl;
01822 (*mycout) << " q - quit" << endl;
01823 (*mycout) << " i - info" << endl;
01824
01825 char c = getc(stdin);
01826 fflush(stdin);
01827
01828 if((c=='c')||(c==10))
01829 break;
01830 else if(c=='f')
01831 {
01832 configuration->pauseEveryStep = false;
01833 break;
01834 }
01835 else if(c=='q')
01836 exit(0);
01837 else if(c=='i')
01838 {
01839 (*mycout) << endl;
01840 (*mycout) << " Number of steps : " << step << endl;
01841 (*mycout) << " Number of terms : " << Node::ndterms << endl;
01842 (*mycout) << " Number of variables : " << parser->variabletab.size() << endl;
01843 (*mycout) << " Number of functions : " << parser->fonctiontab.size() << endl;
01844 (*mycout) << " Number of numericals : " << parser->numericalvariabletab.size() << endl;
01845 (*mycout) << endl;
01846 }
01847 else
01848 printf("<Unknow command>\n");
01849 }
01850 }
01851
01852 if(configuration->beep!=0)
01853 Display::beep(Node::ndterms*10,20);
01854
01855 parser->checkSoundness();
01856
01857 if(!tryApplyR1())
01858 if(!tryApplyR2())
01859 if(!tryApplyR3())
01860 if(!tryApplyR4())
01861 if(!tryApplyR5())
01862 break;
01863
01864 parser->checkSoundness();
01865
01866 this->parser->result = ApplyR0();
01867
01868
01869
01870 }
01871
01872 this->parser->result = ApplyR0();
01873
01874 if(configuration->disjonction)
01875 parser->result = SetDisjunctiveSystem();
01876
01877 Display::texDi(*mycout);
01878 (*mycout) << "End of computation";
01879 Display::texDi(*mycout);
01880 Display::texEndl(*mycout);
01881 (*mycout) << endl << endl;
01882
01883
01884 (*mycout) << " Number of steps : " << step << endl;
01885
01886 if(globconfig->writeMode==Configuration::LATEX)
01887 (*mycout) << endl;
01888
01889 (*mycout) << " Computation time : ";
01890 long computationtime = (clock() - startTime) *1000 / CLOCKS_PER_SEC;
01891 Display::displayTime(computationtime);
01892 Display::texEndl(*mycout);
01893 (*mycout) << endl;
01894
01895 if(configuration->printRule)
01896 {
01897 (*mycout) << endl;
01898 debugDisplay((*mycout));
01899 }
01900
01901 if(configuration->disjonction)
01902 if(result)
01903 result = checkDefinition();
01904 }
01905
01906 Unification::~Unification()
01907 {
01908
01909 }