1 // evaluates model definition rules
7 #include "processabstract.h"
8 #include "processconcrete.h"
12 #include "Hashtable.h"
15 #include "bitreader.h"
21 static int abstractcheck=0;
22 static int abstracttrigger=0;
23 static int paircount=0;
25 // class processabstract
27 processabstract::processabstract(model *m) {
29 br=new bitreader(globalmodel,m->gethashtable());
33 bool processabstract::dirtyflagstatus() {
37 void processabstract::setclean() {
42 bool processabstract::evaluatestatementa(Statementa *sa, Hashtable *env) {
43 switch(sa->gettype()) {
45 return evaluatestatementa(sa->getleft(),env)||evaluatestatementa(sa->getright(),env);
47 return evaluatestatementa(sa->getleft(),env)&&evaluatestatementa(sa->getright(),env);
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);
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)) {
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()) {
76 left->intvalue()==l->number()) {
81 if((left->type()==ELEMENT_TOKEN)&&
82 equivalentstrings(left->gettoken(),l->token())) {
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");
97 if (left->getobject()==NULL) {
99 return new Element(false);
101 char *structuretype=sa->getvalidtype();
102 structure *st=(structuretype==NULL)?left->getstructure():globalmodel->getstructure(structuretype);
103 bool validity=globalmodel->gettypemap()->istype(left->getobject(),st);
105 return new Element(validity);
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");
116 bool tvalue=left->intvalue()<right->intvalue();
121 case STATEMENTA_TRUE:
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);
138 ele->setnewparams(earray,sb->gettleft()->getnumexpr());
142 if (!globalmodel->getdomainrelation()->getset(sb->getsetlabel()->getname())->getset()->contains(ele)) {
144 #ifdef DEBUGMANYMESSAGES
147 printf(" into %s\n",sb->getsetlabel()->getname());
149 globalmodel->getdomainrelation()->abstaddtoset(ele,globalmodel->getdomainrelation()->getset(sb->getsetlabel()->getname()),globalmodel);
155 case STATEMENTB_TUPLE:{
156 Element *left=evaluateexpr(globalmodel,sb->getleft(),env,true,true);
159 Element *right=evaluateexpr(globalmodel,sb->getright(),env,true,true);
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);
169 left->setnewparams(earray,sb->gettleft()->getnumexpr());
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);
176 right->setnewparams(earray,sb->gettright()->getnumexpr());
178 if (!globalmodel->getdomainrelation()->getrelation(sb->getsetlabel()->getname())->getrelation()->contains(left,right)) {
181 #ifdef DEBUGMANYMESSAGES
182 printf("element: <");
186 printf("> into %s\n",sb->getsetlabel()->getname());
188 globalmodel->getdomainrelation()->getrelation(sb->getsetlabel()->getname())->getrelation()->put(left,right);
198 void processabstract::printstats() {
199 printf("Abstraction Rules Checked: %d Triggered: %d\n",abstractcheck,abstracttrigger);
200 printf("Pair count: %d\n",paircount);
203 void processabstract::processrule(Rule *r) {
204 State *st=new State(r, globalmodel->gethashtable());
205 if (st->initializestate(br, globalmodel)) {
208 if (evaluatestatementa(r->getstatementa(),st->env)) {
210 satisfystatementb(r->getstatementb(),st->env);
212 if (!st->increment(br, globalmodel))
219 void processabstract::processrule(Rule *r, Element *ele, char *set) {
223 for(int i=0;i<r->numquants();i++) {
224 AQuantifier *aq=r->getquant(i);
225 switch(aq->gettype()) {
226 case AQUANTIFIER_SING:
234 AQuantifier *aq=r->getquant(count);
235 if (!equivalentstrings(aq->getset()->getname(),set))
238 Hashtable *env=new Hashtable((unsigned int (*)(void *)) & hashstring,(int (*)(void *,void *)) &equivalentstrings);
239 env->setparent(globalmodel->gethashtable());
241 RelationSet **relset=new RelationSet*[r->numquants()-1];
243 for(int i=0;i<r->numquants();i++) {
245 AQuantifier *aq=r->getquant(i);
246 RelationSet *rs=new RelationSet(aq->getleft()->label(),aq->getlower(),aq->getupper());
247 rs->incrementassignment(br,env,globalmodel);
252 env->put(aq->getleft()->label(),ele);
255 if (evaluatestatementa(r->getstatementa(),env))
256 satisfystatementb(r->getstatementb(),env);
257 int i=r->numquants()-2;
259 if (relset[i]->incrementassignment(br,env,globalmodel)) {
262 relset[i]->resetassignment(env);
263 if (!relset[i]->incrementassignment(br,env,globalmodel)) {
272 for(int i=0;i<r->numquants()-1;i++) {
279 processabstract::~processabstract() {
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);
297 switch(aq->gettype()) {
298 case AQUANTIFIER_SING:
299 relset[i]=new RelationSet(aq->getset(),aq->getleft()->label(),aq->gettleft());
301 case AQUANTIFIER_TUPLE:
302 relset[i]=new RelationSet(aq->getset(),aq->getleft()->label(),aq->gettleft(),aq->getright()->label(),aq->gettright());
304 case AQUANTIFIER_RANGE:
305 relset[i]=new RelationSet(aq->getleft()->label(),aq->getlower(),aq->getupper());
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);
328 for(int i=0;i<numrelset;i++)
334 bool State::initializestate(bitreader *br, model * m) {
335 for(int i=0;i<numrelset;i++) {
336 if (!relset[i]->incrementassignment(br,env,m))
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))
353 bool State::initializestate(processconcrete *pc,model * m) {
354 for(int i=0;i<numrelset;i++) {
355 if (!relset[i]->incrementassignment(pc,env,m))
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))
366 relset[i]->resetassignment(env);
367 if (!relset[i]->incrementassignment(br,env,m))
374 bool State::increment(model *m) {
375 for(int i=numrelset-1;i>=0;i--) {
376 if (relset[i]->incrementassignment(env,m))
379 relset[i]->resetassignment(env);
380 if (!relset[i]->incrementassignment(env,m))
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))
392 relset[i]->resetassignment(env);
393 if (!relset[i]->incrementassignment(pc,env,m))
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();
411 if(r->type()==ELEMENT_OBJECT&&
412 r->getobject()!=NULL&&
413 !tm->asserttype(r->getobject(),r->getstructure())) {
419 case AELEMENTEXPR_SUB: {
420 AElementexpr *left=ee->getleft();
421 AElementexpr *right=ee->getright();
422 Element *leftval=evaluateexpr(m,left,env,true,compute);
425 Element *rightval=evaluateexpr(m,right,env,true,compute);
426 if (rightval==NULL) {
430 Element *diff=new Element(leftval->intvalue()-rightval->intvalue());
431 delete(leftval);delete(rightval);
434 case AELEMENTEXPR_ADD: {
435 AElementexpr *left=ee->getleft();
436 AElementexpr *right=ee->getright();
437 Element *leftval=evaluateexpr(m,left,env,true,compute);
440 Element *rightval=evaluateexpr(m,right,env,true,compute);
441 if (rightval==NULL) {
445 Element *sum=new Element(leftval->intvalue()+rightval->intvalue());
446 delete(leftval);delete(rightval);
449 case AELEMENTEXPR_MULT: {
450 AElementexpr *left=ee->getleft();
451 AElementexpr *right=ee->getright();
452 Element *leftval=evaluateexpr(m,left,env,true,compute);
455 Element *rightval=evaluateexpr(m,right,env,true,compute);
456 if (rightval==NULL) {
460 Element *diff=new Element(leftval->intvalue()*rightval->intvalue());
461 delete(leftval);delete(rightval);
464 case AELEMENTEXPR_DIV: {
465 AElementexpr *left=ee->getleft();
466 AElementexpr *right=ee->getright();
467 Element *leftval=evaluateexpr(m,left,env,true,compute);
470 Element *rightval=evaluateexpr(m,right,env,true,compute);
471 if (rightval==NULL) {
475 Element *diff=new Element(leftval->intvalue()/rightval->intvalue());
476 delete(leftval);delete(rightval);
479 case AELEMENTEXPR_LIT: {
480 Literal *l=ee->getliteral();
481 switch(l->gettype()) {
483 return new Element(l->number());
485 return new Element(copystr(l->token()));
487 return new Element(l->getbool());
489 printf("ERROR with lit type\n");
493 case AELEMENTEXPR_FIELD: {
494 Element *e=evaluateexpr(m,ee->getleft(),env,true,compute);
497 Element *r=br->readfieldorarray(e,ee->getfield(),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())) {
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())) {
520 case AELEMENTEXPR_CAST: {
521 Element *e=evaluateexpr(m,ee->getleft(),env,true,compute);
524 typemap *tm=m->gettypemap();
525 if (e->getobject()!=NULL&&compute&&
526 !tm->asserttype(e->getobject(),m->getstructure(ee->getcasttype()))) {
530 Element *r=new Element(e->getobject(),m->getstructure(ee->getcasttype()));
534 case AELEMENTEXPR_FIELDARRAY: {
535 Element *e=evaluateexpr(m,ee->getleft(),env,true,compute);
538 Element *ind=evaluateexpr(m,ee->getright(),env,true,compute);
543 Element *r=br->readfieldorarray(e,ee->getfield(),ind);
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())) {
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())) {
571 // prints the current state
572 void State::print(model *m)
574 for(int i=0; i<numrelset; i++)
576 relset[i]->print(env, m);
586 RelationSet::RelationSet(Set *s, char *l,Type *tl) {
595 RelationSet::RelationSet(Set *s,char *l, Type *tl,char *r,Type *tr) {
604 RelationSet::RelationSet(char *l,AElementexpr *lower,AElementexpr*upper) {
611 int RelationSet::gettype() {
615 void RelationSet::resetassignment(Hashtable *env) {
630 bool RelationSet::incrementassignment(bitreader *br,Hashtable *env, model *m) {
633 if (set->gettype()==SET_label) {
634 DomainSet *ds=m->getdomainrelation()->getset(set->getname());
636 if (!env->contains(left)) {
637 Element *fele=(Element *)ds->getset()->firstelement();
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));
649 Element *ele=(Element *)env->get(left);
650 Element *nextele=(Element *)ds->getset()->getnextelement(ele);
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));
660 env->put(left,nextele);
663 } else if(set->gettype()==SET_literal) {
665 if (!env->contains(left)) {
666 Literal *l=set->getliteral(0);
667 switch(l->gettype()) {
669 env->put(left,new Element(l->number()));
672 env->put(left,new Element(l->token()));
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()) {
683 ele->intvalue()==l->number()) {
684 if ((j+1)<set->getnumliterals()) {
685 env->put(left,new Element(set->getliteral(j+1)->number()));
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()));
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");
714 Tuple t=dr->getrelation()->firstelement();
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));
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));
734 Tuple nextele=dr->getrelation()->getnextelement(eleleft,eleright);
735 if (nextele.isnull())
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));
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));
757 if (!env->contains(left)) {
758 Element *lowerele=(Element *)evaluateexpr(m,lower,env,true,true);
759 env->put(left,lowerele);
762 Element *val=(Element *)env->get(left);
763 Element *upperele=evaluateexpr(m,upper,env,true,true);
764 if (val->intvalue()>=upperele->intvalue()) {
768 Element *nval=new Element(val->intvalue()+1);
777 bool RelationSet::incrementassignment(processconcrete *pc,Hashtable *env, model *m) {
780 if (set->gettype()==SET_label) {
781 DomainSet *ds=m->getdomainrelation()->getset(set->getname());
783 if (!env->contains(left)) {
784 Element *fele=(Element *)ds->getset()->firstelement();
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));
796 Element *ele=(Element *)env->get(left);
797 Element *nextele=(Element *)ds->getset()->getnextelement(ele);
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));
807 env->put(left,nextele);
810 } else if(set->gettype()==SET_literal) {
812 if (!env->contains(left)) {
813 Literal *l=set->getliteral(0);
814 switch(l->gettype()) {
816 env->put(left,new Element(l->number()));
819 env->put(left,new Element(l->token()));
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()) {
830 ele->intvalue()==l->number()) {
831 if ((j+1)<set->getnumliterals()) {
832 env->put(left,new Element(set->getliteral(j+1)->number()));
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()));
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");
861 Tuple t=dr->getrelation()->firstelement();
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));
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));
881 Tuple nextele=dr->getrelation()->getnextelement(eleleft,eleright);
882 if (nextele.isnull())
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));
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));
904 if (!env->contains(left)) {
905 env->put(left,pc->evaluateexpr((CAElementexpr *)lower, env));
908 Element *val=(Element *)env->get(left);
909 Element *upperele=pc->evaluateexpr((CAElementexpr *)upper,env);
910 if (val->intvalue()>=upperele->intvalue()) {
914 Element *nval=new Element(val->intvalue()+1);
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) {
930 if (set->gettype()==SET_label) {
931 DomainSet *ds=m->getdomainrelation()->getset(set->getname());
934 if (!env->contains(left)) {
935 ele=(Element *)ds->getset()->firstelement();
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));
948 ele=(Element *) env->get(left);
949 Element *nextele=(Element *)ds->getset()->getnextelement(ele);
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));
959 env->put(left,nextele);
968 // prints the quantifier and its current state
969 void RelationSet::print(Hashtable *env, model *m)
973 if (set->gettype()==SET_label)
976 DomainSet *ds=m->getdomainrelation()->getset(set->getname());
977 Element *ele = (Element *) env->get(left);