Repair/RepairInterpreter/processabstract.cc

   1 // evaluates model definition rules
   2
   3 #include <stdlib.h>
   4 #include <assert.h>
   5 #include <stdio.h>
   6
   7 #include "processabstract.h"
   8 #include "processconcrete.h"
   9 #include "amodel.h"
  10 #include "omodel.h"
  11 #include "dmodel.h"
  12 #include "Hashtable.h"
  13 #include "element.h"
  14 #include "common.h"
  15 #include "bitreader.h"
  16 #include "model.h"
  17 #include "set.h"
  18 #include "Relation.h"
  19 #include "tmap.h"
  20
  21 static int abstractcheck=0;
  22 static int abstracttrigger=0;
  23 static int paircount=0;
  24
  25 // class processabstract
  26
  27 processabstract::processabstract(model *m) {
  28   globalmodel=m;
  29   br=new bitreader(globalmodel,m->gethashtable());
  30   dirtyflag=false;
  31 }
  32
  33 bool processabstract::dirtyflagstatus() {
  34   return dirtyflag;
  35 }
  36
  37 void processabstract::setclean() {
  38   dirtyflag=false;
  39 }
  40
  41
  42 bool processabstract::evaluatestatementa(Statementa *sa, Hashtable *env) {
  43   switch(sa->gettype()) {
  44   case STATEMENTA_OR:
  45     return evaluatestatementa(sa->getleft(),env)||evaluatestatementa(sa->getright(),env);
  46   case STATEMENTA_AND:
  47     return evaluatestatementa(sa->getleft(),env)&&evaluatestatementa(sa->getright(),env);
  48   case STATEMENTA_NOT:
  49     return !evaluatestatementa(sa->getleft(),env);
  50   case STATEMENTA_EQUALS: {
  51     Element *left=evaluateexpr(globalmodel,sa->getleftee(),env,true,true);
  52     Element *right=evaluateexpr(globalmodel,sa->getrightee(),env,true,true);
  53     bool tvalue=left->equals(right);
  54     delete(left);
  55     delete(right);
  56     return tvalue;
  57   }
  58   case STATEMENTA_SET: {
  59     Element *left=evaluateexpr(globalmodel,sa->getleftee(),env,true,true);
  60     Set *set=sa->getset();
  61     if (set->gettype()==SET_label) {
  62       DomainSet *ds=globalmodel->getdomainrelation()->getset(set->getname());
  63       if (ds->getset()->contains(left)) {
  64         delete(left);
  65         return true;
  66       } else {
  67         delete(left);
  68         return false;
  69       }
  70     } else if (set->gettype()==SET_literal) {
  71       for(int j=0;j<set->getnumliterals();j++) {
  72         Literal *l=set->getliteral(j);
  73         switch(l->gettype()) {
  74         case LITERAL_NUMBER:
  75           if(left->isnumber()&&
  76              left->intvalue()==l->number()) {
  77             delete(left);
  78             return true;
  79           }
  80         case LITERAL_TOKEN:
  81           if((left->type()==ELEMENT_TOKEN)&&
  82              equivalentstrings(left->gettoken(),l->token())) {
  83               delete(left);
  84               return true;
  85             }
  86         }
  87       }
  88       delete(left);
  89       return false;
  90     }
  91   }
  92   case STATEMENTA_VALID: {
  93     Element *left=evaluateexpr(globalmodel,sa->getleftee(),env,true,true);
  94     if (left->type()!=ELEMENT_OBJECT) {
  95       printf("ERROR in processabstract.cc\n");
  96     }
  97     if (left->getobject()==NULL) {
  98       delete(left);
  99       return new Element(false);
 100     }
 101     char *structuretype=sa->getvalidtype();
 102     structure *st=(structuretype==NULL)?left->getstructure():globalmodel->getstructure(structuretype);
 103     bool validity=globalmodel->gettypemap()->istype(left->getobject(),st);
 104     delete(left);
 105     return new Element(validity);
 106   }
 107
 108   case STATEMENTA_LT: {
 109     Element *left=evaluateexpr(globalmodel,sa->getleftee(),env,true,true);
 110     Element *right=evaluateexpr(globalmodel,sa->getrightee(),env,true,true);
 111     if (!left->isnumber()||
 112         !right->isnumber()) {
 113       printf("Bad lt compare\n");
 114       exit(-1);
 115     }
 116     bool tvalue=left->intvalue()<right->intvalue();
 117     delete(left);
 118     delete(right);
 119     return tvalue;
 120   }
 121   case STATEMENTA_TRUE:
 122     return true;
 123   }
 124 }
 125
 126
 127 /* a Statementb is of the type "E in S" or "<E,E> in R" so we just add the
 128    respective element to S or R if the statement is not satisfied */
 129 void processabstract::satisfystatementb(Statementb *sb, Hashtable *env) {
 130   switch(sb->gettype()) {
 131   case STATEMENTB_SING: {
 132     Element *ele=evaluateexpr(globalmodel,sb->getleft(),env,true,true);
 133     /*if (sb->gettleft()!=NULL) {
 134       Element **earray=new Element *[sb->gettleft()->getnumexpr()];
 135       for(int i=0;i<sb->gettleft()->getnumexpr();i++) {
 136         earray[i]=evaluateexpr(br,sb->gettleft()->getexpr(i),env);
 137       }
 138       ele->setnewparams(earray,sb->gettleft()->getnumexpr());
 139       }*/
 140     if (ele==NULL)
 141       break;
 142     if (!globalmodel->getdomainrelation()->getset(sb->getsetlabel()->getname())->getset()->contains(ele)) {
 143       dirtyflag=true;
 144 #ifdef DEBUGMANYMESSAGES
 145       printf("element: ");
 146       ele->print();
 147       printf(" into %s\n",sb->getsetlabel()->getname());
 148 #endif
 149       globalmodel->getdomainrelation()->abstaddtoset(ele,globalmodel->getdomainrelation()->getset(sb->getsetlabel()->getname()),globalmodel);
 150     } else {
 151       delete(ele);
 152     }
 153     break;
 154   }
 155   case STATEMENTB_TUPLE:{
 156     Element *left=evaluateexpr(globalmodel,sb->getleft(),env,true,true);
 157     if (left==NULL)
 158       break;
 159     Element *right=evaluateexpr(globalmodel,sb->getright(),env,true,true);
 160     if (right==NULL) {
 161       delete(left);
 162       break;
 163     }
 164     /*    if (sb->gettleft()!=NULL) {
 165       Element **earray=new Element *[sb->gettleft()->getnumexpr()];
 166       for(int i=0;i<sb->gettleft()->getnumexpr();i++) {
 167         earray[i]=evaluateexpr(br,sb->gettleft()->getexpr(i),env);
 168       }
 169       left->setnewparams(earray,sb->gettleft()->getnumexpr());
 170       }*/
 171     /*    if (sb->gettright()!=NULL) {
 172       Element **earray=new Element *[sb->gettright()->getnumexpr()];
 173       for(int i=0;i<sb->gettright()->getnumexpr();i++) {
 174         earray[i]=evaluateexpr(br,sb->gettright()->getexpr(i),env);
 175       }
 176       right->setnewparams(earray,sb->gettright()->getnumexpr());
 177       }*/
 178     if (!globalmodel->getdomainrelation()->getrelation(sb->getsetlabel()->getname())->getrelation()->contains(left,right)) {
 179       dirtyflag=true;
 180       paircount++;
 181 #ifdef DEBUGMANYMESSAGES
 182       printf("element: <");
 183       left->print();
 184       printf(",");
 185       right->print();
 186       printf("> into %s\n",sb->getsetlabel()->getname());
 187 #endif
 188       globalmodel->getdomainrelation()->getrelation(sb->getsetlabel()->getname())->getrelation()->put(left,right);
 189     } else {
 190       delete(left);
 191       delete(right);
 192     }
 193     break;
 194   }
 195   }
 196 }
 197
 198 void processabstract::printstats() {
 199   printf("Abstraction Rules Checked: %d Triggered: %d\n",abstractcheck,abstracttrigger);
 200   printf("Pair count: %d\n",paircount);
 201 }
 202
 203 void processabstract::processrule(Rule *r) {
 204   State *st=new State(r, globalmodel->gethashtable());
 205   if (st->initializestate(br, globalmodel)) {
 206     while(true) {
 207       abstractcheck++;
 208       if (evaluatestatementa(r->getstatementa(),st->env)) {
 209         abstracttrigger++;
 210         satisfystatementb(r->getstatementb(),st->env);
 211       }
 212       if (!st->increment(br, globalmodel))
 213         break; /* done */
 214     }
 215   }
 216   delete(st);
 217 }
 218
 219 void processabstract::processrule(Rule *r, Element *ele, char *set) {
 220   int count=-1;
 221
 222
 223   for(int i=0;i<r->numquants();i++) {
 224     AQuantifier *aq=r->getquant(i);
 225     switch(aq->gettype()) {
 226     case AQUANTIFIER_SING:
 227       count=i;
 228       break;
 229     default:
 230       break;
 231     }
 232   }
 233
 234   AQuantifier *aq=r->getquant(count);
 235   if (!equivalentstrings(aq->getset()->getname(),set))
 236     return;
 237
 238   Hashtable *env=new Hashtable((unsigned int (*)(void *)) & hashstring,(int (*)(void *,void *)) &equivalentstrings);
 239   env->setparent(globalmodel->gethashtable());
 240
 241   RelationSet **relset=new RelationSet*[r->numquants()-1];
 242   int c=0;
 243   for(int i=0;i<r->numquants();i++) {
 244     if (i!=count) {
 245       AQuantifier *aq=r->getquant(i);
 246       RelationSet *rs=new RelationSet(aq->getleft()->label(),aq->getlower(),aq->getupper());
 247       rs->incrementassignment(br,env,globalmodel);
 248       relset[c++]=rs;
 249     }
 250   }
 251
 252   env->put(aq->getleft()->label(),ele);
 253   bool flag=true;
 254   while(flag) {
 255     if (evaluatestatementa(r->getstatementa(),env))
 256       satisfystatementb(r->getstatementb(),env);
 257     int i=r->numquants()-2;
 258     for(;i>=0;i--) {
 259       if (relset[i]->incrementassignment(br,env,globalmodel)) {
 260         break;
 261       } else {
 262         relset[i]->resetassignment(env);
 263         if (!relset[i]->incrementassignment(br,env,globalmodel)) {
 264           flag=false;
 265           break;
 266         }
 267       }
 268     }
 269     if (i==-1)
 270       flag=false;
 271   }
 272   for(int i=0;i<r->numquants()-1;i++) {
 273     delete(relset[i]);
 274   }
 275   delete(relset);
 276   delete(env);
 277 }
 278
 279 processabstract::~processabstract() {
 280   delete(br);
 281 }
 282
 283
 284
 285
 286
 287 // class State
 288
 289 State::State(Rule *r, Hashtable *oldenv) {
 290   env=new Hashtable((unsigned int (*)(void *)) & hashstring,(int (*)(void *,void *)) &equivalentstrings);;
 291   env->setparent(oldenv);
 292   numrelset=r->numquants();
 293   relset=new RelationSet*[numrelset];
 294   for(int i=0;i<r->numquants();i++) {
 295     AQuantifier *aq=r->getquant(i);
 296
 297     switch(aq->gettype()) {
 298     case AQUANTIFIER_SING:
 299       relset[i]=new RelationSet(aq->getset(),aq->getleft()->label(),aq->gettleft());
 300       break;
 301     case AQUANTIFIER_TUPLE:
 302       relset[i]=new RelationSet(aq->getset(),aq->getleft()->label(),aq->gettleft(),aq->getright()->label(),aq->gettright());
 303       break;
 304     case AQUANTIFIER_RANGE:
 305       relset[i]=new RelationSet(aq->getleft()->label(),aq->getlower(),aq->getupper());
 306       break;
 307     }
 308   }
 309 }
 310
 311
 312
 313 State::State(Constraint *c,Hashtable *oldenv) {
 314   env=new Hashtable((unsigned int (*)(void *)) & hashstring,(int (*)(void *,void *)) &equivalentstrings);;
 315   env->setparent(oldenv);
 316   numrelset=c->numquants();
 317   relset=new RelationSet*[numrelset];
 318   for(int i=0;i<c->numquants();i++) {
 319     Quantifier *q=c->getquant(i);
 320     relset[i]=new RelationSet(q->getset(),q->getlabel()->label(),NULL);
 321   }
 322 }
 323
 324
 325
 326 State::~State() {
 327   delete(env);
 328   for(int i=0;i<numrelset;i++)
 329     delete(relset[i]);
 330   delete[](relset);
 331 }
 332
 333
 334 bool State::initializestate(bitreader *br, model * m) {
 335   for(int i=0;i<numrelset;i++) {
 336     if (!relset[i]->incrementassignment(br,env,m))
 337       return false;
 338   }
 339   return true;
 340 }
 341
 342
 343 /* initializes all quantifiers of this constraint and returns false
 344    if there exists a quantifier that cannot be initialized */
 345 bool State::initializestate(model * m) {
 346   for(int i=0;i<numrelset;i++) {
 347     if (!relset[i]->incrementassignment(env,m))
 348       return false;
 349   }
 350   return true;
 351 }
 352
 353 bool State::initializestate(processconcrete *pc,model * m) {
 354   for(int i=0;i<numrelset;i++) {
 355     if (!relset[i]->incrementassignment(pc,env,m))
 356       return false;
 357   }
 358   return true;
 359 }
 360
 361 bool State::increment(bitreader *br, model *m) {
 362   for(int i=numrelset-1;i>=0;i--) {
 363       if (relset[i]->incrementassignment(br,env,m))
 364         return true;
 365       else {
 366         relset[i]->resetassignment(env);
 367         if (!relset[i]->incrementassignment(br,env,m))
 368           return false;
 369       }
 370   }
 371   return false;
 372 }
 373
 374 bool State::increment(model *m) {
 375   for(int i=numrelset-1;i>=0;i--) {
 376       if (relset[i]->incrementassignment(env,m))
 377         return true;
 378       else {
 379         relset[i]->resetassignment(env);
 380         if (!relset[i]->incrementassignment(env,m))
 381           return false;
 382       }
 383   }
 384   return false;
 385 }
 386
 387 bool State::increment(processconcrete *pc,model *m) {
 388   for(int i=numrelset-1;i>=0;i--) {
 389       if (relset[i]->incrementassignment(pc,env,m))
 390         return true;
 391       else {
 392         relset[i]->resetassignment(env);
 393         if (!relset[i]->incrementassignment(pc,env,m))
 394           return false;
 395       }
 396   }
 397   return false;
 398 }
 399
 400
 401
 402 Element * evaluateexpr(model *m,AElementexpr *ee, Hashtable *env, bool enforcetyping, bool compute) {
 403   bitreader *br=m->getbitreader();
 404   switch(ee->gettype()) {
 405   case AELEMENTEXPR_NULL:
 406     return new Element();
 407   case AELEMENTEXPR_LABEL: {
 408     Element *r=new Element((Element *)env->get(ee->getlabel()->label()));
 409     typemap *tm=m->gettypemap();
 410     if (compute)
 411       if(r->type()==ELEMENT_OBJECT&&
 412          r->getobject()!=NULL&&
 413          !tm->asserttype(r->getobject(),r->getstructure())) {
 414         delete(r);
 415         return NULL;
 416       }
 417     return r;
 418   }
 419   case AELEMENTEXPR_SUB: {
 420     AElementexpr *left=ee->getleft();
 421     AElementexpr *right=ee->getright();
 422     Element *leftval=evaluateexpr(m,left,env,true,compute);
 423     if (leftval==NULL)
 424       return NULL;
 425     Element *rightval=evaluateexpr(m,right,env,true,compute);
 426     if (rightval==NULL) {
 427       delete(leftval);
 428       return NULL;
 429     }
 430     Element *diff=new Element(leftval->intvalue()-rightval->intvalue());
 431     delete(leftval);delete(rightval);
 432     return diff;
 433   }
 434   case AELEMENTEXPR_ADD: {
 435     AElementexpr *left=ee->getleft();
 436     AElementexpr *right=ee->getright();
 437     Element *leftval=evaluateexpr(m,left,env,true,compute);
 438     if (leftval==NULL)
 439       return NULL;
 440     Element *rightval=evaluateexpr(m,right,env,true,compute);
 441     if (rightval==NULL) {
 442       delete(leftval);
 443       return NULL;
 444     }
 445     Element *sum=new Element(leftval->intvalue()+rightval->intvalue());
 446     delete(leftval);delete(rightval);
 447     return sum;
 448   }
 449   case AELEMENTEXPR_MULT: {
 450     AElementexpr *left=ee->getleft();
 451     AElementexpr *right=ee->getright();
 452     Element *leftval=evaluateexpr(m,left,env,true,compute);
 453     if (leftval==NULL)
 454       return NULL;
 455     Element *rightval=evaluateexpr(m,right,env,true,compute);
 456     if (rightval==NULL) {
 457       delete(leftval);
 458       return NULL;
 459     }
 460     Element *diff=new Element(leftval->intvalue()*rightval->intvalue());
 461     delete(leftval);delete(rightval);
 462     return diff;
 463   }
 464   case AELEMENTEXPR_DIV: {
 465     AElementexpr *left=ee->getleft();
 466     AElementexpr *right=ee->getright();
 467     Element *leftval=evaluateexpr(m,left,env,true,compute);
 468     if (leftval==NULL)
 469       return NULL;
 470     Element *rightval=evaluateexpr(m,right,env,true,compute);
 471     if (rightval==NULL) {
 472       delete(leftval);
 473       return NULL;
 474     }
 475     Element *diff=new Element(leftval->intvalue()/rightval->intvalue());
 476     delete(leftval);delete(rightval);
 477     return diff;
 478   }
 479   case AELEMENTEXPR_LIT: {
 480     Literal *l=ee->getliteral();
 481     switch(l->gettype()) {
 482     case LITERAL_NUMBER:
 483       return new Element(l->number());
 484     case LITERAL_TOKEN:
 485       return new Element(copystr(l->token()));
 486     case LITERAL_BOOL:
 487       return new Element(l->getbool());
 488     default:
 489       printf("ERROR with lit type\n");
 490       exit(-1);
 491     }
 492   }
 493   case AELEMENTEXPR_FIELD: {
 494     Element *e=evaluateexpr(m,ee->getleft(),env,true,compute);
 495     if (e==NULL)
 496       return NULL;
 497     Element *r=br->readfieldorarray(e,ee->getfield(),NULL);
 498     delete(e);
 499     if (r==NULL)
 500       return NULL;
 501     if (enforcetyping&&compute) {
 502       typemap *tm=m->gettypemap();
 503       if(r->type()==ELEMENT_OBJECT&&
 504          r->getobject()!=NULL&&
 505          !tm->asserttype(r->getobject(),r->getstructure())) {
 506         delete(r);
 507         return NULL;
 508       }
 509     } else if (compute) {
 510       typemap *tm=m->gettypemap();
 511       if(r->type()==ELEMENT_OBJECT&&
 512          r->getobject()!=NULL&&
 513          !tm->istype(r->getobject(),r->getstructure())) {
 514         delete(r);
 515         return NULL;
 516       }
 517     }
 518     return r;
 519   }
 520   case AELEMENTEXPR_CAST: {
 521     Element *e=evaluateexpr(m,ee->getleft(),env,true,compute);
 522     if (e==NULL)
 523       return NULL;
 524     typemap *tm=m->gettypemap();
 525     if (e->getobject()!=NULL&&compute&&
 526         !tm->asserttype(e->getobject(),m->getstructure(ee->getcasttype()))) {
 527       delete(e);
 528       return NULL;
 529     }
 530     Element *r=new Element(e->getobject(),m->getstructure(ee->getcasttype()));
 531     delete(e);
 532     return r;
 533   }
 534   case AELEMENTEXPR_FIELDARRAY: {
 535     Element *e=evaluateexpr(m,ee->getleft(),env,true,compute);
 536     if (e==NULL)
 537       return NULL;
 538     Element *ind=evaluateexpr(m,ee->getright(),env,true,compute);
 539     if (ind==NULL) {
 540       delete(e);
 541       return NULL;
 542     }
 543     Element *r=br->readfieldorarray(e,ee->getfield(),ind);
 544     delete(ind);
 545     delete(e);
 546     if (r==NULL)
 547       return NULL;
 548     if (enforcetyping&&compute) {
 549       typemap *tm=m->gettypemap();
 550       if(r->type()==ELEMENT_OBJECT&&
 551          r->getobject()!=NULL&&
 552          !tm->asserttype(r->getobject(),r->getstructure())) {
 553         delete(r);
 554         return NULL;
 555       }
 556     } else if (compute) {
 557       typemap *tm=m->gettypemap();
 558       if(r->type()==ELEMENT_OBJECT&&
 559          r->getobject()!=NULL&&
 560          !tm->istype(r->getobject(),r->getstructure())) {
 561         delete(r);
 562         return NULL;
 563       }
 564     }
 565     return r;
 566   }
 567   }
 568 }
 569
 570
 571 // prints the current state
 572 void State::print(model *m)
 573 {
 574   for(int i=0; i<numrelset; i++)
 575     {
 576       relset[i]->print(env, m);
 577       printf(" ");
 578     }
 579 }
 580
 581
 582
 583
 584 // class RelationSet
 585
 586 RelationSet::RelationSet(Set *s, char *l,Type *tl) {
 587   set=s;
 588   type=TYPE_SET;
 589   left=l;
 590   tleft=tl;
 591   tright=NULL;
 592   right=NULL;
 593 }
 594
 595 RelationSet::RelationSet(Set *s,char *l, Type *tl,char *r,Type *tr) {
 596   set=s;
 597   type=TYPE_RELATION;
 598   left=l;
 599   tleft=tl;
 600   tright=tr;
 601   right=r;
 602 }
 603
 604 RelationSet::RelationSet(char *l,AElementexpr *lower,AElementexpr*upper) {
 605   this->lower=lower;
 606   this->upper=upper;
 607   left=l;
 608   type=TYPE_RANGE;
 609 }
 610
 611 int RelationSet::gettype() {
 612   return type;
 613 }
 614
 615 void RelationSet::resetassignment(Hashtable *env) {
 616   switch(type) {
 617   case TYPE_SET:
 618     env->remove(left);
 619     break;
 620   case TYPE_RELATION:
 621     env->remove(left);
 622     env->remove(right);
 623     break;
 624   case TYPE_RANGE:
 625     env->remove(left);
 626     break;
 627   }
 628 }
 629
 630 bool RelationSet::incrementassignment(bitreader *br,Hashtable *env, model *m) {
 631   switch(type) {
 632   case TYPE_SET: {
 633     if (set->gettype()==SET_label) {
 634       DomainSet *ds=m->getdomainrelation()->getset(set->getname());
 635
 636       if (!env->contains(left)) {
 637         Element *fele=(Element *)ds->getset()->firstelement();
 638         if (fele==NULL)
 639           return false;
 640         env->put(left,fele);
 641         /*      if (tleft!=NULL) {
 642           assert(tleft->getnumlabels()==ele->getnumparams());
 643           for (int i=0;i<tleft->getnumlabels();i++) {
 644             env->put(tleft->getlabel(i)->label(),ele->paramvalue(i));
 645           }
 646           }*/
 647         return true;
 648       }
 649       Element *ele=(Element *)env->get(left);
 650       Element *nextele=(Element *)ds->getset()->getnextelement(ele);
 651       if (nextele==NULL)
 652         return false;
 653       else {
 654         /*      if (tleft!=NULL) {
 655           assert(tleft->getnumlabels()==nextele->getnumparams());
 656           for (int i=0;i<tleft->getnumlabels();i++) {
 657             env->put(tleft->getlabel(i)->label(),nextele->paramvalue(i));
 658           }
 659           }*/
 660         env->put(left,nextele);
 661         return true;
 662       }
 663     } else if(set->gettype()==SET_literal) {
 664
 665       if (!env->contains(left)) {
 666         Literal *l=set->getliteral(0);
 667         switch(l->gettype()) {
 668         case LITERAL_NUMBER:
 669           env->put(left,new Element(l->number()));
 670           break;
 671         case LITERAL_TOKEN:
 672           env->put(left,new Element(l->token()));
 673           break;
 674         }
 675         return true;
 676       }
 677       Element *ele=(Element *)env->get(left);
 678       for(int j=0;j<set->getnumliterals();j++) {
 679         Literal *l=set->getliteral(j);
 680         switch(l->gettype()) {
 681         case LITERAL_NUMBER:
 682           if(ele->isnumber()&&
 683             ele->intvalue()==l->number()) {
 684             if ((j+1)<set->getnumliterals()) {
 685               env->put(left,new Element(set->getliteral(j+1)->number()));
 686               delete(ele);
 687               return true;
 688             }
 689             else return false;
 690           }
 691         case LITERAL_TOKEN:
 692           if((ele->type()==ELEMENT_TOKEN)&&
 693             equivalentstrings(ele->gettoken(),l->token())) {
 694             if ((j+1)<set->getnumliterals()) {
 695               env->put(left,new Element(set->getliteral(j+1)->token()));
 696               delete(ele);
 697               return true;
 698             }
 699             else return false;
 700           }
 701         }
 702       }
 703     }
 704   }
 705   case TYPE_RELATION: {
 706     DRelation *dr=m->getdomainrelation()->getrelation(set->getname());
 707     Element *eleleft=(Element *)env->get(left);
 708     Element *eleright=(Element *)env->get(right);
 709     if ((eleleft==NULL)||(eleright==NULL)) {
 710       if((eleleft!=NULL)||(eleright!=NULL)) {
 711         printf("ERROR in TYPE_RELATION in processabstract.cc\n");
 712         exit(-1);
 713       }
 714       Tuple t=dr->getrelation()->firstelement();
 715       if (t.isnull())
 716         return false;
 717       env->put(left,t.left);
 718       env->put(right,t.right);
 719       /*      if (tleft!=NULL) {
 720         assert(tleft->getnumlabels()==((Element *)t.left)->getnumparams());
 721         for (int i=0;i<tleft->getnumlabels();i++) {
 722           env->put(tleft->getlabel(i)->label(),((Element *)t.left)->paramvalue(i));
 723         }
 724         }*/
 725       /*      if (tright!=NULL) {
 726         assert(tright->getnumlabels()==((Element *)t.right)->getnumparams());
 727         for (int i=0;i<tright->getnumlabels();i++) {
 728           env->put(tright->getlabel(i)->label(),((Element *)t.right)->paramvalue(i));
 729         }
 730         }*/
 731
 732       return true;
 733     }
 734     Tuple nextele=dr->getrelation()->getnextelement(eleleft,eleright);
 735     if (nextele.isnull())
 736       return false;
 737     else {
 738       env->put(left,nextele.left);
 739       env->put(right,nextele.right);
 740       /*      if (tleft!=NULL) {
 741         assert(tleft->getnumlabels()==((Element *)nextele.left)->getnumparams());
 742         for (int i=0;i<tleft->getnumlabels();i++) {
 743           env->put(tleft->getlabel(i)->label(),((Element *)nextele.left)->paramvalue(i));
 744         }
 745         }*/
 746       /*      if (tright!=NULL) {
 747         assert(tright->getnumlabels()==((Element *)nextele.right)->getnumparams());
 748         for (int i=0;i<tright->getnumlabels();i++) {
 749           env->put(tright->getlabel(i)->label(),((Element *)nextele.right)->paramvalue(i));
 750         }
 751         }*/
 752       return true;
 753     }
 754   }
 755   case TYPE_RANGE: {
 756
 757     if (!env->contains(left)) {
 758       Element *lowerele=(Element *)evaluateexpr(m,lower,env,true,true);
 759       env->put(left,lowerele);
 760       return true;
 761     }
 762     Element *val=(Element *)env->get(left);
 763     Element *upperele=evaluateexpr(m,upper,env,true,true);
 764     if (val->intvalue()>=upperele->intvalue()) {
 765       delete(upperele);
 766       return false;
 767     } else {
 768       Element *nval=new Element(val->intvalue()+1);
 769       env->put(left,nval);
 770       delete(val);
 771       return true;
 772     }
 773   }
 774   }
 775 }
 776
 777 bool RelationSet::incrementassignment(processconcrete *pc,Hashtable *env, model *m) {
 778   switch(type) {
 779   case TYPE_SET: {
 780     if (set->gettype()==SET_label) {
 781       DomainSet *ds=m->getdomainrelation()->getset(set->getname());
 782
 783       if (!env->contains(left)) {
 784         Element *fele=(Element *)ds->getset()->firstelement();
 785         if (fele==NULL)
 786           return false;
 787         env->put(left,fele);
 788         /*      if (tleft!=NULL) {
 789           assert(tleft->getnumlabels()==ele->getnumparams());
 790           for (int i=0;i<tleft->getnumlabels();i++) {
 791             env->put(tleft->getlabel(i)->label(),ele->paramvalue(i));
 792           }
 793           }*/
 794         return true;
 795       }
 796       Element *ele=(Element *)env->get(left);
 797       Element *nextele=(Element *)ds->getset()->getnextelement(ele);
 798       if (nextele==NULL)
 799         return false;
 800       else {
 801         /*      if (tleft!=NULL) {
 802           assert(tleft->getnumlabels()==nextele->getnumparams());
 803           for (int i=0;i<tleft->getnumlabels();i++) {
 804             env->put(tleft->getlabel(i)->label(),nextele->paramvalue(i));
 805           }
 806           }*/
 807         env->put(left,nextele);
 808         return true;
 809       }
 810     } else if(set->gettype()==SET_literal) {
 811
 812       if (!env->contains(left)) {
 813         Literal *l=set->getliteral(0);
 814         switch(l->gettype()) {
 815         case LITERAL_NUMBER:
 816           env->put(left,new Element(l->number()));
 817           break;
 818         case LITERAL_TOKEN:
 819           env->put(left,new Element(l->token()));
 820           break;
 821         }
 822         return true;
 823       }
 824       Element *ele=(Element *)env->get(left);
 825       for(int j=0;j<set->getnumliterals();j++) {
 826         Literal *l=set->getliteral(j);
 827         switch(l->gettype()) {
 828         case LITERAL_NUMBER:
 829           if(ele->isnumber()&&
 830             ele->intvalue()==l->number()) {
 831             if ((j+1)<set->getnumliterals()) {
 832               env->put(left,new Element(set->getliteral(j+1)->number()));
 833               delete(ele);
 834               return true;
 835             }
 836             else return false;
 837           }
 838         case LITERAL_TOKEN:
 839           if((ele->type()==ELEMENT_TOKEN)&&
 840             equivalentstrings(ele->gettoken(),l->token())) {
 841             if ((j+1)<set->getnumliterals()) {
 842               env->put(left,new Element(set->getliteral(j+1)->token()));
 843               delete(ele);
 844               return true;
 845             }
 846             else return false;
 847           }
 848         }
 849       }
 850     }
 851   }
 852   case TYPE_RELATION: {
 853     DRelation *dr=m->getdomainrelation()->getrelation(set->getname());
 854     Element *eleleft=(Element *)env->get(left);
 855     Element *eleright=(Element *)env->get(right);
 856     if ((eleleft==NULL)||(eleright==NULL)) {
 857       if((eleleft!=NULL)||(eleright!=NULL)) {
 858         printf("ERROR in TYPE_RELATION in processabstract.cc\n");
 859         exit(-1);
 860       }
 861       Tuple t=dr->getrelation()->firstelement();
 862       if (t.isnull())
 863         return false;
 864       env->put(left,t.left);
 865       env->put(right,t.right);
 866       /*      if (tleft!=NULL) {
 867         assert(tleft->getnumlabels()==((Element *)t.left)->getnumparams());
 868         for (int i=0;i<tleft->getnumlabels();i++) {
 869           env->put(tleft->getlabel(i)->label(),((Element *)t.left)->paramvalue(i));
 870         }
 871         }*/
 872       /*      if (tright!=NULL) {
 873         assert(tright->getnumlabels()==((Element *)t.right)->getnumparams());
 874         for (int i=0;i<tright->getnumlabels();i++) {
 875           env->put(tright->getlabel(i)->label(),((Element *)t.right)->paramvalue(i));
 876         }
 877         }*/
 878
 879       return true;
 880     }
 881     Tuple nextele=dr->getrelation()->getnextelement(eleleft,eleright);
 882     if (nextele.isnull())
 883       return false;
 884     else {
 885       env->put(left,nextele.left);
 886       env->put(right,nextele.right);
 887       /*      if (tleft!=NULL) {
 888         assert(tleft->getnumlabels()==((Element *)nextele.left)->getnumparams());
 889         for (int i=0;i<tleft->getnumlabels();i++) {
 890           env->put(tleft->getlabel(i)->label(),((Element *)nextele.left)->paramvalue(i));
 891         }
 892         }*/
 893       /*      if (tright!=NULL) {
 894         assert(tright->getnumlabels()==((Element *)nextele.right)->getnumparams());
 895         for (int i=0;i<tright->getnumlabels();i++) {
 896           env->put(tright->getlabel(i)->label(),((Element *)nextele.right)->paramvalue(i));
 897         }
 898         }*/
 899       return true;
 900     }
 901   }
 902   case TYPE_RANGE: {
 903
 904     if (!env->contains(left)) {
 905       env->put(left,pc->evaluateexpr((CAElementexpr *)lower, env));
 906       return true;
 907     }
 908     Element *val=(Element *)env->get(left);
 909     Element *upperele=pc->evaluateexpr((CAElementexpr *)upper,env);
 910     if (val->intvalue()>=upperele->intvalue()) {
 911       delete(upperele);
 912       return false;
 913     } else {
 914       Element *nval=new Element(val->intvalue()+1);
 915       env->put(left,nval);
 916       delete(val);
 917       return true;
 918     }
 919   }
 920   }
 921 }
 922
 923
 924 /* increments the value of "left" and returns "false" if this is not possible.
 925    When this method is called for the first time, it simply initializes
 926    the value of the quantifier ("left") */
 927 bool RelationSet::incrementassignment(Hashtable *env, model *m) {
 928   switch(type) {
 929   case TYPE_SET: {
 930     if (set->gettype()==SET_label) {
 931       DomainSet *ds=m->getdomainrelation()->getset(set->getname());
 932
 933       Element *ele=NULL;
 934       if (!env->contains(left)) {
 935         ele=(Element *)ds->getset()->firstelement();
 936         if (ele==NULL)
 937           return false;
 938         env->put(left,ele);
 939         /*      if (tleft!=NULL) {
 940           assert(tleft->getnumlabels()==ele->getnumparams());
 941           for (int i=0;i<tleft->getnumlabels();i++) {
 942             env->put(tleft->getlabel(i)->label(),ele->paramvalue(i));
 943           }
 944           }*/
 945         return true;
 946       }
 947
 948       ele=(Element *) env->get(left);
 949       Element *nextele=(Element *)ds->getset()->getnextelement(ele);
 950       if (nextele==NULL)
 951         return false;
 952       else {
 953         /*      if (tleft!=NULL) {
 954           assert(tleft->getnumlabels()==nextele->getnumparams());
 955           for (int i=0;i<tleft->getnumlabels();i++) {
 956             env->put(tleft->getlabel(i)->label(),nextele->paramvalue(i));
 957           }
 958           }*/
 959         env->put(left,nextele);
 960         return true;
 961       }
 962     }
 963   }
 964   }
 965 }
 966
 967
 968 // prints the quantifier and its current state
 969 void RelationSet::print(Hashtable *env, model *m)
 970 {
 971   switch(type) {
 972   case TYPE_SET: {
 973     if (set->gettype()==SET_label)
 974       {
 975         printf("%s=", left);
 976         DomainSet *ds=m->getdomainrelation()->getset(set->getname());
 977         Element *ele = (Element *) env->get(left);
 978         ele->print();
 979         printf("\n");
 980       }
 981   }}
 982 }