1 // Defines the Internal Constraint Language
16 Literal::Literal(char *s) {
21 // there are three types of literals: numbers, bools, and tokens
22 int Literal::gettype() {
24 if (sscanf(str,"%d",&val)==1)
25 return LITERAL_NUMBER;
27 if (equivalentstrings(str,"true")||
28 equivalentstrings(str,"false"))
34 bool Literal::getbool() {
35 if (equivalentstrings(str,"true"))
41 int Literal::number() {
43 sscanf(str,"%d",&val);
47 char * Literal::token() {
51 void Literal::print() {
55 void Literal::fprint(FILE *f) {
66 Setlabel::Setlabel(char *s) {
70 char * Setlabel::getname() {
74 void Setlabel::print() {
78 void Setlabel::fprint(FILE *f) {
88 // a set is either a label or a set of literals
90 Set::Set(Setlabel *sl) {
95 int Set::getnumliterals() {
99 Literal * Set::getliteral(int i) {
103 Set::Set(Literal **l, int nl) {
112 if (type==SET_literal) {
113 for(int i=0;i<numliterals;i++)
123 char * Set::getname() {
124 return setlabel->getname();
134 for(int i=0;i<numliterals;i++) {
137 literals[i]->print();
144 void Set::fprint(FILE *f) {
151 for(int i=0;i<numliterals;i++) {
154 literals[i]->fprint(f);
168 Label::Label(char *s) {
172 void Label::print() {
176 void Label::fprint(FILE *f) {
186 Relation::Relation(char * r) {
190 char * Relation::getname() {
194 void Relation::print() {
198 void Relation::fprint(FILE *f) {
208 Quantifier::Quantifier(Label *l, Set *s) {
213 Label * Quantifier::getlabel() {
217 Set * Quantifier::getset() {
221 void Quantifier::print() {
228 void Quantifier::fprint(FILE *f) {
229 fprintf(f,"forall ");
242 Setexpr::Setexpr(Setlabel *sl) {
247 Setexpr::Setexpr(Label *l, bool invert, Relation *r) {
249 type=invert?SETEXPR_INVREL:SETEXPR_REL;
253 void Setexpr::print() {
271 void Setexpr::fprint(FILE *f) {
290 void Setexpr::print_size(Hashtable *stateenv, model *m)
298 DomainRelation *dr = m->getdomainrelation();
299 Hashtable *env = m->gethashtable();
300 DomainSet *dset = dr->getset(setlabel->getname());
301 WorkSet *ws = dset->getset();
304 printf("%d", ws->size());
316 Element *key = (Element *) stateenv->get(label->label());
318 DomainRelation *dr = m->getdomainrelation();
319 Hashtable *env = m->gethashtable();
320 DRelation *rel = dr->getrelation(relation->getname());
321 WorkRelation *wr = rel->getrelation();
323 WorkSet *ws = wr->getset(key);
326 printf("%d", ws->size());
331 case SETEXPR_INVREL:{
338 Element *key = (Element *) stateenv->get(label->label());
340 DomainRelation *dr = m->getdomainrelation();
342 Hashtable *env = m->gethashtable();
343 DRelation *rel = dr->getrelation(relation->getname());
344 WorkRelation *wr = rel->getrelation();
346 WorkSet *ws = wr->invgetset(key);
349 printf("%d", ws->size());
357 void Setexpr::print_value(Hashtable *stateenv, model *m)
365 DomainRelation *dr = m->getdomainrelation();
366 Hashtable *env = m->gethashtable();
367 DomainSet *dset = dr->getset(setlabel->getname());
369 WorkSet *ws = dset->getset();
382 Element *key = (Element *) stateenv->get(label->label());
384 DomainRelation *dr = m->getdomainrelation();
385 Hashtable *env = m->gethashtable();
386 DRelation *rel = dr->getrelation(relation->getname());
387 WorkRelation *wr = rel->getrelation();
389 WorkSet *ws = wr->getset(key);
391 printf("%d\n", ws->size());
396 case SETEXPR_INVREL:{
404 Element *key = (Element *) stateenv->get(label->label());
406 DomainRelation *dr = m->getdomainrelation();
408 Hashtable *env = m->gethashtable();
409 DRelation *rel = dr->getrelation(relation->getname());
410 WorkRelation *wr = rel->getrelation();
412 WorkSet *ws = wr->invgetset(key);
414 printf("%d\n", ws->size());
422 Setlabel * Setexpr::getsetlabel() {
426 Relation * Setexpr::getrelation() {
430 Label * Setexpr::getlabel() {
434 int Setexpr::gettype() {
444 Label * Valueexpr::getlabel() {
448 int Valueexpr::gettype() {
452 Relation * Valueexpr::getrelation() {
456 Valueexpr::Valueexpr(Label *l,Relation *r, bool inv) {
461 Valueexpr::Valueexpr(Valueexpr *ve,Relation *r,bool inv) {
462 valueexpr=ve;relation=r;
466 bool Valueexpr::getinverted() {
470 void Valueexpr::print() {
489 void Valueexpr::fprint(FILE *f) {
499 valueexpr->fprint(f);
508 Element * Valueexpr::get_value(Hashtable *stateenv, model *m) {
511 key = (Element *) stateenv->get(label->label());
513 key = valueexpr->get_value(stateenv,m);
515 DomainRelation *dr = m->getdomainrelation();
516 Hashtable *env = m->gethashtable();
517 DRelation *rel = dr->getrelation(relation->getname());
518 WorkRelation *wr = rel->getrelation();
521 return (Element *) wr->invgetobj(key);
523 return (Element *) wr->getobj(key);
527 void Valueexpr::print_value(Hashtable *stateenv, model *m) {
530 Element *elem = this->get_value(stateenv,m);
535 Valueexpr * Valueexpr::getvalueexpr() {
545 int Elementexpr::gettype() {
549 Relation * Elementexpr::getrelation() {
553 Elementexpr::Elementexpr(Elementexpr *l,Relation *r) {
554 type=ELEMENTEXPR_RELATION;
559 Setexpr * Elementexpr::getsetexpr() {
563 Elementexpr::Elementexpr(Setexpr *se) {
565 type=ELEMENTEXPR_SETSIZE;
568 Label * Elementexpr::getlabel() {
572 Elementexpr * Elementexpr::getleft() {
576 Elementexpr * Elementexpr::getright() {
580 Literal * Elementexpr::getliteral() {
584 Elementexpr::Elementexpr(Elementexpr *l, Elementexpr *r, int op) {
585 left=l;right=r;type=op;
588 Elementexpr::Elementexpr(Literal *lit) {
590 type=ELEMENTEXPR_LIT;
593 Elementexpr::Elementexpr(Label *lab) {
595 type=ELEMENTEXPR_LABEL;
598 void Elementexpr::print() {
600 case ELEMENTEXPR_LABEL:
603 case ELEMENTEXPR_SUB:
608 case ELEMENTEXPR_ADD:
613 case ELEMENTEXPR_MULT:
618 case ELEMENTEXPR_LIT:
621 case ELEMENTEXPR_SETSIZE:
626 case ELEMENTEXPR_RELATION:
634 void Elementexpr::fprint(FILE *f) {
636 case ELEMENTEXPR_LABEL:
639 case ELEMENTEXPR_SUB:
644 case ELEMENTEXPR_ADD:
649 case ELEMENTEXPR_MULT:
654 case ELEMENTEXPR_LIT:
657 case ELEMENTEXPR_SETSIZE:
658 fprintf(f,"sizeof(");
662 case ELEMENTEXPR_RELATION:
671 void Elementexpr::print_value(Hashtable *stateenv, model *m) {
673 case ELEMENTEXPR_SUB:
674 case ELEMENTEXPR_ADD:
675 case ELEMENTEXPR_MULT:
676 left->print_value(stateenv, m);
677 right->print_value(stateenv, m);
679 case ELEMENTEXPR_SETSIZE:
680 setexpr->print_size(stateenv, m);
682 case ELEMENTEXPR_RELATION:
696 Predicate::Predicate(Valueexpr *ve, int t, Elementexpr *ee) {
702 Predicate::Predicate(Label *l,Setexpr *se) {
708 Predicate::Predicate(bool greaterthan, Setexpr *se) {
716 Valueexpr * Predicate::getvalueexpr() {
720 Elementexpr * Predicate::geteleexpr() {
724 Label * Predicate::getlabel() {
728 Setexpr * Predicate::getsetexpr() {
732 int Predicate::gettype() {
736 void Predicate::print() {
741 elementexpr->print();
746 elementexpr->print();
748 case PREDICATE_EQUALS:
751 elementexpr->print();
756 elementexpr->print();
761 elementexpr->print();
772 if (type==PREDICATE_EQ1)
774 if (type==PREDICATE_GTE1)
780 void Predicate::fprint(FILE *f) {
783 valueexpr->fprint(f);
785 elementexpr->fprint(f);
788 valueexpr->fprint(f);
790 elementexpr->fprint(f);
792 case PREDICATE_EQUALS:
793 valueexpr->fprint(f);
795 elementexpr->fprint(f);
798 valueexpr->fprint(f);
800 elementexpr->fprint(f);
803 valueexpr->fprint(f);
805 elementexpr->fprint(f);
814 fprintf(f,"sizeof(");
816 if (type==PREDICATE_EQ1)
818 if (type==PREDICATE_GTE1)
826 void Predicate::print_sets(Hashtable *stateenv, model *m) {
830 case PREDICATE_EQUALS:
833 valueexpr->print_value(stateenv, m);
835 elementexpr->print_value(stateenv, m);
838 setexpr->print_value(stateenv, m);
842 setexpr->print_size(stateenv, m);
853 Statement::Statement(Statement *l, Statement *r, int t) {
859 Statement::Statement(Statement *l) {
864 Statement::Statement(Predicate *p) {
869 void Statement::print() {
891 void Statement::fprint(FILE *f) {
914 void Statement::print_sets(Hashtable *stateenv, model *m) {
918 left->print_sets(stateenv, m);
920 right->print_sets(stateenv, m);
923 left->print_sets(stateenv, m);
926 pred->print_sets(stateenv, m);
933 int Statement::gettype() {
937 Statement* Statement::getleft() {
941 Statement* Statement::getright() {
945 Predicate * Statement::getpredicate() {
956 Constraint::Constraint() {
962 void Constraint::setcrash(bool c) {
966 bool Constraint::getcrash() {
970 Constraint::Constraint(Quantifier **q, int nq) {
976 void Constraint::setstatement(Statement *s) {
980 int Constraint::numquants() {
981 return numquantifiers;
984 Quantifier * Constraint::getquant(int i) {
985 return quantifiers[i];
988 Statement * Constraint::getstatement() {
992 void Constraint::print() {
994 for(int i=0;i<numquantifiers;i++) {
997 quantifiers[i]->print();
1000 if (statement!=NULL) {
1006 void Constraint::fprint(FILE *f) {
1008 for(int i=0;i<numquantifiers;i++) {
1011 quantifiers[i]->fprint(f);
1014 if (statement!=NULL) {
1015 statement->fprint(f);