Repair/RepairInterpreter/omodel.cc

   1 // Defines the Internal Constraint Language
   2
   3 #include <stdio.h>
   4 #include "omodel.h"
   5 #include "common.h"
   6 #include "model.h"
   7 #include "Hashtable.h"
   8 #include "dmodel.h"
   9 #include "element.h"
  10 #include "set.h"
  11 #include "Relation.h"
  12
  13
  14 // class Literal
  15
  16 Literal::Literal(char *s) {
  17   str=s;
  18 }
  19
  20
  21 // there are three types of literals: numbers, bools, and tokens
  22 int Literal::gettype() {
  23   int val;
  24   if (sscanf(str,"%d",&val)==1)
  25     return LITERAL_NUMBER;
  26   else {
  27     if (equivalentstrings(str,"true")||
  28         equivalentstrings(str,"false"))
  29       return LITERAL_BOOL;
  30     return LITERAL_TOKEN;
  31   }
  32 }
  33
  34 bool Literal::getbool() {
  35   if (equivalentstrings(str,"true"))
  36     return true;
  37   else
  38     return false;
  39 }
  40
  41 int Literal::number() {
  42   int val;
  43   sscanf(str,"%d",&val);
  44   return val;
  45 }
  46
  47 char * Literal::token() {
  48   return str;
  49 }
  50
  51 void Literal::print() {
  52   printf("%s",str);
  53 }
  54
  55 void Literal::fprint(FILE *f) {
  56   fprintf(f,"%s",str);
  57 }
  58
  59
  60
  61
  62
  63
  64 // class Setlabel
  65
  66 Setlabel::Setlabel(char *s) {
  67   str=s;
  68 }
  69
  70 char * Setlabel::getname() {
  71   return str;
  72 }
  73
  74 void Setlabel::print() {
  75   printf("%s",str);
  76 }
  77
  78 void Setlabel::fprint(FILE *f) {
  79   fprintf(f,"%s",str);
  80 }
  81
  82
  83
  84
  85
  86 // class Set
  87
  88 // a set is either a label or a set of literals
  89
  90 Set::Set(Setlabel *sl) {
  91   type=SET_label;
  92   setlabel=sl;
  93 }
  94
  95 int Set::getnumliterals() {
  96   return numliterals;
  97 }
  98
  99 Literal * Set::getliteral(int i) {
 100   return literals[i];
 101 }
 102
 103 Set::Set(Literal **l, int nl) {
 104   type=SET_literal;
 105   literals=l;
 106   numliterals=nl;
 107 }
 108
 109 Set::~Set() {
 110   if (type==SET_label)
 111     delete(setlabel);
 112   if (type==SET_literal) {
 113     for(int i=0;i<numliterals;i++)
 114       delete(literals[i]);
 115     delete(literals);
 116   }
 117 }
 118
 119 int Set::gettype() {
 120   return type;
 121 }
 122
 123 char * Set::getname() {
 124   return setlabel->getname();
 125 }
 126
 127 void Set::print() {
 128   switch(type) {
 129   case SET_label:
 130     setlabel->print();
 131     break;
 132   case SET_literal:
 133     printf("{");
 134     for(int i=0;i<numliterals;i++) {
 135       if (i!=0)
 136         printf(",");
 137       literals[i]->print();
 138     }
 139     printf("}");
 140     break;
 141   }
 142 }
 143
 144 void Set::fprint(FILE *f) {
 145   switch(type) {
 146   case SET_label:
 147     setlabel->fprint(f);
 148     break;
 149   case SET_literal:
 150     fprintf(f,"{");
 151     for(int i=0;i<numliterals;i++) {
 152       if (i!=0)
 153         fprintf(f,",");
 154       literals[i]->fprint(f);
 155     }
 156     fprintf(f,"}");
 157     break;
 158   }
 159 }
 160
 161
 162
 163
 164
 165
 166 // class Label
 167
 168 Label::Label(char *s) {
 169   str=s;
 170 }
 171
 172 void Label::print() {
 173   printf("%s",str);
 174 }
 175
 176 void Label::fprint(FILE *f) {
 177   fprintf(f,"%s",str);
 178 }
 179
 180
 181
 182
 183
 184 // class Relation
 185
 186 Relation::Relation(char * r) {
 187   str=r;
 188 }
 189
 190 char * Relation::getname() {
 191   return str;
 192 }
 193
 194 void Relation::print() {
 195   printf("%s",str);
 196 }
 197
 198 void Relation::fprint(FILE *f) {
 199   fprintf(f,"%s",str);
 200 }
 201
 202
 203
 204
 205
 206 // class Quantifier
 207
 208 Quantifier::Quantifier(Label *l, Set *s) {
 209   label=l;
 210   set=s;
 211 }
 212
 213 Label * Quantifier::getlabel() {
 214   return label;
 215 }
 216
 217 Set * Quantifier::getset() {
 218   return set;
 219 }
 220
 221 void Quantifier::print() {
 222   printf("forall ");
 223   label->print();
 224   printf(" in ");
 225   set->print();
 226 }
 227
 228 void Quantifier::fprint(FILE *f) {
 229   fprintf(f,"forall ");
 230   label->fprint(f);
 231   fprintf(f," in ");
 232   set->fprint(f);
 233 }
 234
 235
 236
 237
 238
 239
 240 // class Setexpr
 241
 242 Setexpr::Setexpr(Setlabel *sl) {
 243   setlabel=sl;
 244   type=SETEXPR_LABEL;
 245 }
 246
 247 Setexpr::Setexpr(Label *l, bool invert, Relation *r) {
 248   label=l;
 249   type=invert?SETEXPR_INVREL:SETEXPR_REL;
 250   relation=r;
 251 }
 252
 253 void Setexpr::print() {
 254   switch(type) {
 255   case SETEXPR_LABEL:
 256     setlabel->print();
 257     break;
 258   case SETEXPR_REL:
 259     label->print();
 260     printf(".");
 261     relation->print();
 262     break;
 263   case SETEXPR_INVREL:
 264     label->print();
 265     printf(".~");
 266     relation->print();
 267     break;
 268   }
 269 }
 270
 271 void Setexpr::fprint(FILE *f) {
 272   switch(type) {
 273   case SETEXPR_LABEL:
 274     setlabel->fprint(f);
 275     break;
 276   case SETEXPR_REL:
 277     label->fprint(f);
 278     fprintf(f,".");
 279     relation->fprint(f);
 280     break;
 281   case SETEXPR_INVREL:
 282     label->fprint(f);
 283     fprintf(f,".~");
 284     relation->fprint(f);
 285     break;
 286   }
 287 }
 288
 289
 290 void Setexpr::print_size(Hashtable *stateenv, model *m)
 291 {
 292   switch(type) {
 293   case SETEXPR_LABEL:{
 294     printf("sizeof(");
 295     setlabel->print();
 296     printf(")=");
 297
 298     DomainRelation *dr = m->getdomainrelation();
 299     Hashtable *env = m->gethashtable();
 300     DomainSet *dset = dr->getset(setlabel->getname());
 301     WorkSet *ws = dset->getset();
 302
 303     if (ws != NULL)
 304       printf("%d", ws->size());
 305     else printf("0");
 306     break;
 307   }
 308
 309   case SETEXPR_REL:{
 310     printf("sizeof(");
 311     label->print();
 312     printf(".");
 313     relation->print();
 314     printf(")=");
 315
 316     Element *key = (Element *) stateenv->get(label->label());
 317
 318     DomainRelation *dr = m->getdomainrelation();
 319     Hashtable *env = m->gethashtable();
 320     DRelation *rel = dr->getrelation(relation->getname());
 321     WorkRelation *wr = rel->getrelation();
 322
 323     WorkSet *ws = wr->getset(key);
 324
 325     if (ws != NULL)
 326       printf("%d", ws->size());
 327     else printf("0");
 328     break;
 329   }
 330
 331   case SETEXPR_INVREL:{
 332     printf("sizeof(");
 333     label->print();
 334     printf(".~");
 335     relation->print();
 336     printf(")=");
 337
 338     Element *key = (Element *) stateenv->get(label->label());
 339
 340     DomainRelation *dr = m->getdomainrelation();
 341
 342     Hashtable *env = m->gethashtable();
 343     DRelation *rel = dr->getrelation(relation->getname());
 344     WorkRelation *wr = rel->getrelation();
 345
 346     WorkSet *ws = wr->invgetset(key);
 347
 348     if (ws != NULL)
 349       printf("%d", ws->size());
 350     else printf("0");
 351     break;
 352   }
 353   }
 354 }
 355
 356
 357 void Setexpr::print_value(Hashtable *stateenv, model *m)
 358 {
 359   switch(type) {
 360   case SETEXPR_LABEL:{
 361     //printf("   ");
 362     setlabel->print();
 363     printf("=");
 364
 365     DomainRelation *dr = m->getdomainrelation();
 366     Hashtable *env = m->gethashtable();
 367     DomainSet *dset = dr->getset(setlabel->getname());
 368
 369     WorkSet *ws = dset->getset();
 370     ws->print();
 371     break;
 372   }
 373
 374   case SETEXPR_REL:{
 375     /*
 376     printf("   sizeof(");
 377     label->print();
 378     printf(".");
 379     relation->print();
 380     printf(") = ");
 381
 382     Element *key = (Element *) stateenv->get(label->label());
 383
 384     DomainRelation *dr = m->getdomainrelation();
 385     Hashtable *env = m->gethashtable();
 386     DRelation *rel = dr->getrelation(relation->getname());
 387     WorkRelation *wr = rel->getrelation();
 388
 389     WorkSet *ws = wr->getset(key);
 390
 391     printf("%d\n", ws->size());
 392     */
 393     break;
 394   }
 395
 396   case SETEXPR_INVREL:{
 397     /*
 398     printf("   sizeof(");
 399     label->print();
 400     printf(".~");
 401     relation->print();
 402     printf(") = ");
 403
 404     Element *key = (Element *) stateenv->get(label->label());
 405
 406     DomainRelation *dr = m->getdomainrelation();
 407
 408     Hashtable *env = m->gethashtable();
 409     DRelation *rel = dr->getrelation(relation->getname());
 410     WorkRelation *wr = rel->getrelation();
 411
 412     WorkSet *ws = wr->invgetset(key);
 413
 414     printf("%d\n", ws->size());
 415     */
 416     break;
 417   }
 418   }
 419 }
 420
 421
 422 Setlabel * Setexpr::getsetlabel() {
 423   return setlabel;
 424 }
 425
 426 Relation * Setexpr::getrelation() {
 427   return relation;
 428 }
 429
 430 Label * Setexpr::getlabel() {
 431   return label;
 432 }
 433
 434 int Setexpr::gettype() {
 435   return type;
 436 }
 437
 438
 439
 440
 441
 442 // class Valueexpr
 443
 444 Label * Valueexpr::getlabel() {
 445   return label;
 446 }
 447
 448 int Valueexpr::gettype() {
 449   return type;
 450 }
 451
 452 Relation * Valueexpr::getrelation() {
 453   return relation;
 454 }
 455
 456 Valueexpr::Valueexpr(Label *l,Relation *r, bool inv) {
 457   label=l;relation=r;
 458   type=0;inverted=inv;
 459 }
 460
 461 Valueexpr::Valueexpr(Valueexpr *ve,Relation *r,bool inv) {
 462   valueexpr=ve;relation=r;
 463   type=1;inverted=inv;
 464 }
 465
 466 bool Valueexpr::getinverted() {
 467   return inverted;
 468 }
 469
 470 void Valueexpr::print() {
 471   switch(type) {
 472   case 0:
 473     label->print();
 474     printf(".");
 475     if (inverted)
 476       printf("~");
 477     relation->print();
 478     break;
 479   case 1:
 480     valueexpr->print();
 481     printf(".");
 482     if (inverted)
 483       printf("~");
 484     relation->print();
 485     break;
 486   }
 487 }
 488
 489 void Valueexpr::fprint(FILE *f) {
 490   switch(type) {
 491   case 0:
 492     label->fprint(f);
 493     fprintf(f,".");
 494     if (inverted)
 495       fprintf(f,"~");
 496     relation->fprint(f);
 497     break;
 498   case 1:
 499     valueexpr->fprint(f);
 500     fprintf(f,".");
 501     if (inverted)
 502       fprintf(f,"~");
 503     relation->fprint(f);
 504     break;
 505   }
 506 }
 507
 508 Element * Valueexpr::get_value(Hashtable *stateenv, model *m) {
 509   Element *key=NULL;
 510   if (type==0) {
 511     key = (Element *) stateenv->get(label->label());
 512   } else
 513     key = valueexpr->get_value(stateenv,m);
 514
 515   DomainRelation *dr = m->getdomainrelation();
 516   Hashtable *env = m->gethashtable();
 517   DRelation *rel = dr->getrelation(relation->getname());
 518   WorkRelation *wr = rel->getrelation();
 519
 520   if (inverted)
 521     return (Element *) wr->invgetobj(key);
 522   else
 523     return (Element *) wr->getobj(key);
 524
 525 }
 526
 527 void Valueexpr::print_value(Hashtable *stateenv, model *m) {
 528   this->print();
 529   printf("=");
 530   Element *elem = this->get_value(stateenv,m);
 531   elem->print();
 532   //printf("\n");
 533 }
 534
 535 Valueexpr * Valueexpr::getvalueexpr() {
 536   return valueexpr;
 537 }
 538
 539
 540
 541
 542
 543 // class Elementexpr
 544
 545 int Elementexpr::gettype() {
 546   return type;
 547 }
 548
 549 Relation * Elementexpr::getrelation() {
 550   return relation;
 551 }
 552
 553 Elementexpr::Elementexpr(Elementexpr *l,Relation *r) {
 554   type=ELEMENTEXPR_RELATION;
 555   left=l;
 556   relation=r;
 557 }
 558
 559 Setexpr * Elementexpr::getsetexpr() {
 560   return setexpr;
 561 }
 562
 563 Elementexpr::Elementexpr(Setexpr *se) {
 564   setexpr=se;
 565   type=ELEMENTEXPR_SETSIZE;
 566 }
 567
 568 Label * Elementexpr::getlabel() {
 569   return label;
 570 }
 571
 572 Elementexpr * Elementexpr::getleft() {
 573   return left;
 574 }
 575
 576 Elementexpr * Elementexpr::getright() {
 577   return right;
 578 }
 579
 580 Literal * Elementexpr::getliteral() {
 581   return literal;
 582 }
 583
 584 Elementexpr::Elementexpr(Elementexpr *l, Elementexpr *r, int op) {
 585   left=l;right=r;type=op;
 586 }
 587
 588 Elementexpr::Elementexpr(Literal *lit) {
 589   literal=lit;
 590   type=ELEMENTEXPR_LIT;
 591 }
 592
 593 Elementexpr::Elementexpr(Label *lab) {
 594   label=lab;
 595   type=ELEMENTEXPR_LABEL;
 596 }
 597
 598 void Elementexpr::print() {
 599   switch(type) {
 600   case ELEMENTEXPR_LABEL:
 601     label->print();
 602     break;
 603   case ELEMENTEXPR_SUB:
 604     left->print();
 605     printf("-");
 606     right->print();
 607     break;
 608   case ELEMENTEXPR_ADD:
 609     left->print();
 610     printf("+");
 611     right->print();
 612     break;
 613   case ELEMENTEXPR_MULT:
 614     left->print();
 615     printf("*");
 616     right->print();
 617     break;
 618   case ELEMENTEXPR_LIT:
 619     literal->print();
 620     break;
 621   case ELEMENTEXPR_SETSIZE:
 622     printf("sizeof(");
 623     setexpr->print();
 624     printf(")");
 625     break;
 626   case ELEMENTEXPR_RELATION:
 627     left->print();
 628     printf(".");
 629     relation->print();
 630     break;
 631   }
 632 }
 633
 634 void Elementexpr::fprint(FILE *f) {
 635   switch(type) {
 636   case ELEMENTEXPR_LABEL:
 637     label->fprint(f);
 638     break;
 639   case ELEMENTEXPR_SUB:
 640     left->fprint(f);
 641     fprintf(f,"-");
 642     right->fprint(f);
 643     break;
 644   case ELEMENTEXPR_ADD:
 645     left->fprint(f);
 646     fprintf(f,"+");
 647     right->fprint(f);
 648     break;
 649   case ELEMENTEXPR_MULT:
 650     left->fprint(f);
 651     fprintf(f,"*");
 652     right->fprint(f);
 653     break;
 654   case ELEMENTEXPR_LIT:
 655     literal->fprint(f);
 656     break;
 657   case ELEMENTEXPR_SETSIZE:
 658     fprintf(f,"sizeof(");
 659     setexpr->fprint(f);
 660     fprintf(f,")");
 661     break;
 662   case ELEMENTEXPR_RELATION:
 663     left->fprint(f);
 664     fprintf(f,".");
 665     relation->fprint(f);
 666     break;
 667   }
 668 }
 669
 670
 671 void Elementexpr::print_value(Hashtable *stateenv, model *m) {
 672   switch(type) {
 673   case ELEMENTEXPR_SUB:
 674   case ELEMENTEXPR_ADD:
 675   case ELEMENTEXPR_MULT:
 676     left->print_value(stateenv, m);
 677     right->print_value(stateenv, m);
 678     break;
 679   case ELEMENTEXPR_SETSIZE:
 680     setexpr->print_size(stateenv, m);
 681     break;
 682   case ELEMENTEXPR_RELATION:
 683     /*
 684     left->print();
 685     printf(".");
 686     relation->print();
 687     */
 688     break;
 689   }
 690 }
 691
 692
 693
 694 // class Predicate
 695
 696 Predicate::Predicate(Valueexpr *ve, int t, Elementexpr *ee) {
 697   valueexpr=ve;
 698   type=t;
 699   elementexpr=ee;
 700 }
 701
 702 Predicate::Predicate(Label *l,Setexpr *se) {
 703   label=l;
 704   setexpr=se;
 705   type=PREDICATE_SET;
 706 }
 707
 708 Predicate::Predicate(bool greaterthan, Setexpr *se) {
 709   if (greaterthan)
 710     type=PREDICATE_GTE1;
 711   else
 712     type=PREDICATE_EQ1;
 713   setexpr=se;
 714 }
 715
 716 Valueexpr * Predicate::getvalueexpr() {
 717   return valueexpr;
 718 }
 719
 720 Elementexpr * Predicate::geteleexpr() {
 721   return elementexpr;
 722 }
 723
 724 Label * Predicate::getlabel() {
 725   return label;
 726 }
 727
 728 Setexpr * Predicate::getsetexpr() {
 729   return setexpr;
 730 }
 731
 732 int Predicate::gettype() {
 733   return type;
 734 }
 735
 736 void Predicate::print() {
 737   switch(type) {
 738   case PREDICATE_LT:
 739     valueexpr->print();
 740     printf("<");
 741     elementexpr->print();
 742     break;
 743   case PREDICATE_LTE:
 744     valueexpr->print();
 745     printf("<=");
 746     elementexpr->print();
 747     break;
 748   case PREDICATE_EQUALS:
 749     valueexpr->print();
 750     printf("=");
 751     elementexpr->print();
 752     break;
 753   case PREDICATE_GTE:
 754     valueexpr->print();
 755     printf(">=");
 756     elementexpr->print();
 757     break;
 758   case PREDICATE_GT:
 759     valueexpr->print();
 760     printf(">");
 761     elementexpr->print();
 762     break;
 763   case PREDICATE_SET:
 764     label->print();
 765     printf(" in ");
 766     setexpr->print();
 767     break;
 768   case PREDICATE_EQ1:
 769   case PREDICATE_GTE1:
 770     printf("sizeof(");
 771     setexpr->print();
 772     if (type==PREDICATE_EQ1)
 773       printf(")=1");
 774     if (type==PREDICATE_GTE1)
 775       printf(")>=1");
 776     break;
 777   }
 778 }
 779
 780 void Predicate::fprint(FILE *f) {
 781   switch(type) {
 782   case PREDICATE_LT:
 783     valueexpr->fprint(f);
 784     fprintf(f,"<");
 785     elementexpr->fprint(f);
 786     break;
 787   case PREDICATE_LTE:
 788     valueexpr->fprint(f);
 789     fprintf(f,"<=");
 790     elementexpr->fprint(f);
 791     break;
 792   case PREDICATE_EQUALS:
 793     valueexpr->fprint(f);
 794     fprintf(f,"=");
 795     elementexpr->fprint(f);
 796     break;
 797   case PREDICATE_GTE:
 798     valueexpr->fprint(f);
 799     fprintf(f,">=");
 800     elementexpr->fprint(f);
 801     break;
 802   case PREDICATE_GT:
 803     valueexpr->fprint(f);
 804     fprintf(f,">");
 805     elementexpr->fprint(f);
 806     break;
 807   case PREDICATE_SET:
 808     label->fprint(f);
 809     fprintf(f," in ");
 810     setexpr->fprint(f);
 811     break;
 812   case PREDICATE_EQ1:
 813   case PREDICATE_GTE1:
 814     fprintf(f,"sizeof(");
 815     setexpr->fprint(f);
 816     if (type==PREDICATE_EQ1)
 817       fprintf(f,")=1");
 818     if (type==PREDICATE_GTE1)
 819       fprintf(f,")>=1");
 820     break;
 821   }
 822 }
 823
 824
 825
 826 void Predicate::print_sets(Hashtable *stateenv, model *m) {
 827   switch(type) {
 828   case PREDICATE_LT:
 829   case PREDICATE_LTE:
 830   case PREDICATE_EQUALS:
 831   case PREDICATE_GTE:
 832   case PREDICATE_GT:
 833     valueexpr->print_value(stateenv, m);
 834     printf("; ");
 835     elementexpr->print_value(stateenv, m);
 836     break;
 837   case PREDICATE_SET:
 838     setexpr->print_value(stateenv, m);
 839     break;
 840   case PREDICATE_EQ1:
 841   case PREDICATE_GTE1:
 842     setexpr->print_size(stateenv, m);
 843     break;
 844   }
 845 }
 846
 847
 848
 849
 850
 851 // class Statement
 852
 853 Statement::Statement(Statement *l, Statement *r, int t) {
 854   left=l;
 855   right=r;
 856   type=t;
 857 }
 858
 859 Statement::Statement(Statement *l) {
 860   type=STATEMENT_NOT;
 861   left=l;
 862 }
 863
 864 Statement::Statement(Predicate *p) {
 865   pred=p;
 866   type=STATEMENT_PRED;
 867 }
 868
 869 void Statement::print() {
 870   switch(type) {
 871   case STATEMENT_OR:
 872     left->print();
 873     printf(" OR ");
 874     right->print();
 875     break;
 876   case STATEMENT_AND:
 877     left->print();
 878     printf(" AND ");
 879     right->print();
 880     break;
 881   case STATEMENT_NOT:
 882     printf("!");
 883     left->print();
 884     break;
 885   case STATEMENT_PRED:
 886     pred->print();
 887     break;
 888   }
 889 }
 890
 891 void Statement::fprint(FILE *f) {
 892   switch(type) {
 893   case STATEMENT_OR:
 894     left->fprint(f);
 895     fprintf(f," OR ");
 896     right->fprint(f);
 897     break;
 898   case STATEMENT_AND:
 899     left->fprint(f);
 900     fprintf(f," AND ");
 901     right->fprint(f);
 902     break;
 903   case STATEMENT_NOT:
 904     fprintf(f,"!");
 905     left->fprint(f);
 906     break;
 907   case STATEMENT_PRED:
 908     pred->fprint(f);
 909     break;
 910   }
 911 }
 912
 913
 914 void Statement::print_sets(Hashtable *stateenv, model *m) {
 915   switch(type) {
 916   case STATEMENT_OR:
 917   case STATEMENT_AND:
 918     left->print_sets(stateenv, m);
 919     printf("; ");
 920     right->print_sets(stateenv, m);
 921     break;
 922   case STATEMENT_NOT:
 923     left->print_sets(stateenv, m);
 924     break;
 925   case STATEMENT_PRED:
 926     pred->print_sets(stateenv, m);
 927     break;
 928   }
 929   //printf("\n");
 930 }
 931
 932
 933 int Statement::gettype() {
 934   return type;
 935 }
 936
 937 Statement* Statement::getleft() {
 938   return left;
 939 }
 940
 941 Statement* Statement::getright() {
 942   return right;
 943 }
 944
 945 Predicate * Statement::getpredicate() {
 946   return pred;
 947 }
 948
 949
 950
 951
 952
 953
 954 // class Constraint
 955
 956 Constraint::Constraint() {
 957   quantifiers=NULL;
 958   numquantifiers=0;
 959   statement=NULL;
 960 }
 961
 962 void Constraint::setcrash(bool c) {
 963   crash=c;
 964 }
 965
 966 bool Constraint::getcrash() {
 967   return crash;
 968 }
 969
 970 Constraint::Constraint(Quantifier **q, int nq) {
 971   quantifiers=q;
 972   numquantifiers=nq;
 973   statement=NULL;
 974 }
 975
 976 void Constraint::setstatement(Statement *s) {
 977   statement=s;
 978 }
 979
 980 int Constraint::numquants() {
 981   return numquantifiers;
 982 }
 983
 984 Quantifier * Constraint::getquant(int i) {
 985   return quantifiers[i];
 986 }
 987
 988 Statement * Constraint::getstatement() {
 989   return statement;
 990 }
 991
 992 void Constraint::print() {
 993   printf("[");
 994   for(int i=0;i<numquantifiers;i++) {
 995     if (i!=0)
 996       printf(",");
 997     quantifiers[i]->print();
 998   }
 999   printf("], ");
1000   if (statement!=NULL) {
1001     statement->print();
1002   }
1003   printf("\n");
1004 }
1005
1006 void Constraint::fprint(FILE *f) {
1007   printf("[");
1008   for(int i=0;i<numquantifiers;i++) {
1009     if (i!=0)
1010       fprintf(f,",");
1011     quantifiers[i]->fprint(f);
1012   }
1013   printf("],");
1014   if (statement!=NULL) {
1015     statement->fprint(f);
1016   }
1017 }