Repair/RepairInterpreter/normalizer.cc

   1 // converts constraints into disjunctive normal form
   2
   3 #include <stdlib.h>
   4 #include "normalizer.h"
   5 #include "omodel.h"
   6 #include "processobject.h"
   7 #include "set.h"
   8 #include "amodel.h"
   9 #include "common.h"
  10
  11
  12
  13 // class CoercePredicate
  14
  15 CoercePredicate::CoercePredicate(char *ts, char *lt, char *rs) {
  16   triggerset=ts;
  17   ltype=lt;
  18   rtype=NULL;
  19   relset=rs;
  20   rule=false;
  21   tuple=false;
  22   predicate=NULL;
  23 }
  24
  25 CoercePredicate::CoercePredicate(char *ts, char *lt, char *rt,char *rs) {
  26   triggerset=ts;
  27   ltype=lt;
  28   rtype=rt;
  29   relset=rs;
  30   rule=false;
  31   tuple=true;
  32   predicate=NULL;
  33 }
  34
  35 CoercePredicate::CoercePredicate(bool b, Predicate *p) {
  36   rule=true;
  37   coercebool=b;
  38   predicate=p;
  39 #ifdef REPAIR
  40   if((p->gettype()==PREDICATE_EQ1||
  41       p->gettype()==PREDICATE_GTE1)&&coercebool==false) {
  42     printf("Possible forcing size predicate to be false.  Error!\n");
  43     exit(-1);
  44   }
  45 #endif
  46 }
  47
  48 Predicate * CoercePredicate::getpredicate() {
  49   return predicate;
  50 }
  51
  52 bool CoercePredicate::isrule() {
  53   return rule;
  54 }
  55
  56 bool CoercePredicate::istuple() {
  57   return tuple;
  58 }
  59
  60 bool CoercePredicate::getcoercebool() {
  61   return coercebool;
  62 }
  63
  64 char * CoercePredicate::gettriggerset() {
  65   return triggerset;
  66 }
  67
  68 char * CoercePredicate::getrelset() {
  69   return relset;
  70 }
  71
  72 char * CoercePredicate::getltype() {
  73   return ltype;
  74 }
  75
  76 char * CoercePredicate::getrtype() {
  77   return rtype;
  78 }
  79
  80
  81
  82
  83 // class CoerceSentence
  84
  85 CoerceSentence::CoerceSentence(CoercePredicate **pred, int numpred) {
  86   predicates=pred;
  87   numpreds=numpred;
  88 }
  89
  90
  91 int CoerceSentence::getnumpredicates() {
  92   return numpreds;
  93 }
  94
  95
  96 CoercePredicate * CoerceSentence::getpredicate(int i) {
  97   return predicates[i];
  98 }
  99
 100
 101
 102 // returns true iff the sentence is satisfied
 103 bool CoerceSentence::issatisfied(processobject *po, Hashtable *env)
 104 {
 105   for (int i=0; i<getnumpredicates(); i++)
 106     {
 107       CoercePredicate *cp = getpredicate(i);
 108       Predicate *p = cp->getpredicate();
 109       if (!po->processpredicate(cp->getpredicate(),env))
 110         return false;
 111     }
 112   return true;
 113 }
 114
 115
 116 // returns how much we pay if we satisfy this sentence
 117 int CoerceSentence::cost(processobject *po, Hashtable *env) {
 118   int cost=0;
 119   for(int i=0;i<numpreds;i++) {
 120     CoercePredicate *cp=predicates[i];
 121     bool pvalue;
 122     if (cp->getpredicate()!=NULL)
 123       pvalue=po->processpredicate(cp->getpredicate(),env);
 124     if (pvalue!=cp->getcoercebool())
 125       cost+=costfunction(cp);
 126   }
 127   return cost;
 128 }
 129
 130
 131 CoerceSentence::~CoerceSentence() {
 132   for(int i=0;i<numpreds;i++)
 133     delete(predicates[i]);
 134   delete predicates;
 135 }
 136
 137
 138
 139
 140 // class NormalForm
 141
 142 NormalForm::NormalForm(Constraint *c) {
 143   SentenceArray *sa=computesentences(c->getstatement(),true);
 144   this->length=sa->length;
 145   this->sentences=sa->sentences;
 146   this->c=c;
 147   delete(sa);
 148 }
 149
 150 void NormalForm::fprint(FILE *f) {
 151   if (c!=NULL)
 152     c->fprint(f);
 153 }
 154
 155 NormalForm::NormalForm(Rule *r) {
 156   int count=-1;
 157   char *label, *triggerset;
 158   c=NULL;
 159   for(int i=0;i<r->numquants();i++) {
 160     AQuantifier *aq=r->getquant(i);
 161     switch(aq->gettype()) {
 162     case AQUANTIFIER_SING:
 163       triggerset=aq->getset()->getname();
 164       label=aq->getleft()->label();
 165       break;
 166     default:
 167       break;
 168     }
 169   }
 170   Statementb *sb=r->getstatementb();
 171   CoercePredicate *cp=NULL;
 172   if(sb->gettype()==STATEMENTB_SING) {
 173     cp=new CoercePredicate(triggerset,gettype(label,triggerset,sb->getleft()),sb->getsetlabel()->getname());
 174   } else {
 175     cp=new CoercePredicate(triggerset,gettype(label,triggerset,sb->getleft()),gettype(label,triggerset,sb->getright()),sb->getsetlabel()->getname());
 176   }
 177   CoercePredicate **cpa=new CoercePredicate*[1];
 178   cpa[0]=cp;
 179   CoerceSentence *cs=new CoerceSentence(cpa,1);
 180   sentences=new CoerceSentence*[1];
 181   sentences[0]=cs;
 182   length=1;
 183 }
 184
 185
 186 char * gettype(char *label, char *set,AElementexpr *ae) {
 187   switch(ae->gettype()) {
 188   case AELEMENTEXPR_SUB:
 189   case AELEMENTEXPR_ADD:
 190   case AELEMENTEXPR_MULT:
 191   case AELEMENTEXPR_DIV:
 192     return "int";
 193   case AELEMENTEXPR_NULL:
 194     return NULL;
 195   case AELEMENTEXPR_FIELD:
 196   case AELEMENTEXPR_FIELDARRAY:
 197     return NULL;
 198   case AELEMENTEXPR_LIT:
 199     switch(ae->getliteral()->gettype()) {
 200     case LITERAL_NUMBER:
 201       return "int";
 202     case LITERAL_TOKEN:
 203       return "token";
 204     default:
 205       printf("error in normalizer.gettype()\n");
 206       exit(-1);
 207     }
 208   case AELEMENTEXPR_LABEL:
 209     if (equivalentstrings(ae->getlabel()->label(),label))
 210       return set;
 211     return NULL;
 212   case AELEMENTEXPR_CAST:
 213     return gettype(label,set,ae->getleft());
 214   }
 215 }
 216
 217
 218 int NormalForm::getnumsentences() {
 219   return length;
 220 }
 221
 222
 223 CoerceSentence * NormalForm::getsentence(int i) {
 224   return sentences[i];
 225 }
 226
 227
 228 /* returns the sentence in this constraint that can be satisfied
 229    with a minimum cost, and which is different from any sentence
 230    in the "badsentences" structure */
 231 CoerceSentence * NormalForm::closestmatch(WorkSet *badsentences, processobject *po, Hashtable *env) {
 232   int totalcost=-1; int bestmatch=-1;
 233   for(int i=0;i<length;i++) {
 234     if (badsentences==NULL || !badsentences->contains(sentences[i]))
 235       {
 236         int cost=sentences[i]->cost(po,env);
 237         if ((totalcost==-1)||(totalcost>cost)) {
 238           totalcost=cost;
 239           bestmatch=i;
 240         }
 241       }
 242   }
 243   return sentences[bestmatch];
 244 }
 245
 246 int costfunction(CoercePredicate *p) {
 247   return 1;
 248 }
 249
 250
 251 // computes the normal form of the given statement
 252 SentenceArray * computesentences(Statement *st,bool stat) {
 253   switch(st->gettype()) {
 254   case STATEMENT_OR: {
 255     SentenceArray *left=computesentences(st->getleft(),stat);
 256     SentenceArray *right=computesentences(st->getright(),stat);
 257     if (stat) {
 258       CoerceSentence **combine=new CoerceSentence *[left->length+right->length];
 259       for(int i=0;i<left->length;i++)
 260         combine[i]=left->sentences[i];
 261       for(int i=0;i<right->length;i++)
 262         combine[i+left->length]=right->sentences[i];
 263       SentenceArray *sa=new SentenceArray(combine, left->length+right->length);
 264       delete[](left->sentences);delete[](right->sentences);
 265       delete(left);delete(right);
 266       return sa;
 267     } else {
 268       CoerceSentence **combine=new CoerceSentence *[left->length*right->length];
 269       for(int i=0;i<left->length;i++)
 270         for(int j=0;j<right->length;j++) {
 271           CoerceSentence *leftsent=left->sentences[i];
 272           CoerceSentence *rightsent=right->sentences[j];
 273           CoercePredicate **preds=new CoercePredicate *[leftsent->getnumpredicates()+rightsent->getnumpredicates()];
 274           for(int il=0;il<leftsent->getnumpredicates();il++)
 275             preds[il]=new CoercePredicate(leftsent->getpredicate(il)->getcoercebool(),leftsent->getpredicate(il)->getpredicate());
 276           for(int ir=0;ir<rightsent->getnumpredicates();ir++)
 277             preds[ir+leftsent->getnumpredicates()]=new CoercePredicate(rightsent->getpredicate(ir)->getcoercebool(),rightsent->getpredicate(ir)->getpredicate());
 278           combine[i*right->length+j]=new CoerceSentence(preds,left->length*right->length);
 279         }
 280       SentenceArray *sa=new SentenceArray(combine, left->length*right->length);
 281       for(int i=0;i<left->length;i++)
 282         delete(left->sentences[i]);
 283       for(int i=0;i<right->length;i++)
 284         delete(right->sentences[i]);
 285       delete(left->sentences);delete(right->sentences);
 286       delete(left);delete(right);
 287       return sa;
 288     }
 289   }
 290   case STATEMENT_AND: {
 291     SentenceArray *left=computesentences(st->getleft(),stat);
 292     SentenceArray *right=computesentences(st->getright(),stat);
 293     if (stat) {
 294       CoerceSentence **combine=new CoerceSentence *[left->length*right->length];
 295       for(int i=0;i<left->length;i++)
 296         for(int j=0;j<right->length;j++) {
 297           CoerceSentence *leftsent=left->sentences[i];
 298           CoerceSentence *rightsent=right->sentences[j];
 299           CoercePredicate **preds=new CoercePredicate *[leftsent->getnumpredicates()+rightsent->getnumpredicates()];
 300           for(int il=0;il<leftsent->getnumpredicates();il++)
 301             preds[il]=new CoercePredicate(leftsent->getpredicate(il)->getcoercebool(),leftsent->getpredicate(il)->getpredicate());
 302           for(int ir=0;ir<rightsent->getnumpredicates();ir++)
 303             preds[ir+leftsent->getnumpredicates()]=new CoercePredicate(rightsent->getpredicate(ir)->getcoercebool(),rightsent->getpredicate(ir)->getpredicate());
 304           combine[i*right->length+j]=new CoerceSentence(preds,left->length*right->length);
 305         }
 306       SentenceArray *sa=new SentenceArray(combine, left->length*right->length);
 307       for(int i=0;i<left->length;i++)
 308         delete(left->sentences[i]);
 309       for(int i=0;i<right->length;i++)
 310         delete(right->sentences[i]);
 311       delete(left->sentences);delete(right->sentences);
 312       delete(left);delete(right);
 313       return sa;
 314     } else {
 315       CoerceSentence **combine=new CoerceSentence *[left->length+right->length];
 316       for(int i=0;i<left->length;i++)
 317         combine[i]=left->sentences[i];
 318       for(int i=0;i<right->length;i++)
 319         combine[i+left->length]=right->sentences[i];
 320       SentenceArray *sa=new SentenceArray(combine, left->length+right->length);
 321       delete(left->sentences);delete(right->sentences);
 322       delete(left);delete(right);
 323       return sa;
 324     }
 325   }
 326   case STATEMENT_NOT:
 327     return computesentences(st->getleft(),!stat);
 328   case STATEMENT_PRED:
 329     CoercePredicate *cp=new CoercePredicate(stat, st->getpredicate());
 330     CoercePredicate **cparray=new CoercePredicate *[1];
 331     cparray[0]=cp;
 332     CoerceSentence *cs=new CoerceSentence(cparray,1);
 333     CoerceSentence **csarray=new CoerceSentence *[1];
 334     csarray[0]=cs;
 335     return new SentenceArray(csarray,1);
 336   }
 337 }
 338
 339
 340
 341
 342 // class SentenceArray
 343
 344 SentenceArray::SentenceArray(CoerceSentence **sentences, int l) {
 345   length=l;
 346   this->sentences=sentences;
 347 }
 348