1 // converts constraints into disjunctive normal form
4 #include "normalizer.h"
6 #include "processobject.h"
13 // class CoercePredicate
15 CoercePredicate::CoercePredicate(char *ts, char *lt, char *rs) {
25 CoercePredicate::CoercePredicate(char *ts, char *lt, char *rt,char *rs) {
35 CoercePredicate::CoercePredicate(bool b, Predicate *p) {
40 if((p->gettype()==PREDICATE_EQ1||
41 p->gettype()==PREDICATE_GTE1)&&coercebool==false) {
42 printf("Possible forcing size predicate to be false. Error!\n");
48 Predicate * CoercePredicate::getpredicate() {
52 bool CoercePredicate::isrule() {
56 bool CoercePredicate::istuple() {
60 bool CoercePredicate::getcoercebool() {
64 char * CoercePredicate::gettriggerset() {
68 char * CoercePredicate::getrelset() {
72 char * CoercePredicate::getltype() {
76 char * CoercePredicate::getrtype() {
83 // class CoerceSentence
85 CoerceSentence::CoerceSentence(CoercePredicate **pred, int numpred) {
91 int CoerceSentence::getnumpredicates() {
96 CoercePredicate * CoerceSentence::getpredicate(int i) {
102 // returns true iff the sentence is satisfied
103 bool CoerceSentence::issatisfied(processobject *po, Hashtable *env)
105 for (int i=0; i<getnumpredicates(); i++)
107 CoercePredicate *cp = getpredicate(i);
108 Predicate *p = cp->getpredicate();
109 if (!po->processpredicate(cp->getpredicate(),env))
116 // returns how much we pay if we satisfy this sentence
117 int CoerceSentence::cost(processobject *po, Hashtable *env) {
119 for(int i=0;i<numpreds;i++) {
120 CoercePredicate *cp=predicates[i];
122 if (cp->getpredicate()!=NULL)
123 pvalue=po->processpredicate(cp->getpredicate(),env);
124 if (pvalue!=cp->getcoercebool())
125 cost+=costfunction(cp);
131 CoerceSentence::~CoerceSentence() {
132 for(int i=0;i<numpreds;i++)
133 delete(predicates[i]);
142 NormalForm::NormalForm(Constraint *c) {
143 SentenceArray *sa=computesentences(c->getstatement(),true);
144 this->length=sa->length;
145 this->sentences=sa->sentences;
150 void NormalForm::fprint(FILE *f) {
155 NormalForm::NormalForm(Rule *r) {
157 char *label, *triggerset;
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();
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());
175 cp=new CoercePredicate(triggerset,gettype(label,triggerset,sb->getleft()),gettype(label,triggerset,sb->getright()),sb->getsetlabel()->getname());
177 CoercePredicate **cpa=new CoercePredicate*[1];
179 CoerceSentence *cs=new CoerceSentence(cpa,1);
180 sentences=new CoerceSentence*[1];
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:
193 case AELEMENTEXPR_NULL:
195 case AELEMENTEXPR_FIELD:
196 case AELEMENTEXPR_FIELDARRAY:
198 case AELEMENTEXPR_LIT:
199 switch(ae->getliteral()->gettype()) {
205 printf("error in normalizer.gettype()\n");
208 case AELEMENTEXPR_LABEL:
209 if (equivalentstrings(ae->getlabel()->label(),label))
212 case AELEMENTEXPR_CAST:
213 return gettype(label,set,ae->getleft());
218 int NormalForm::getnumsentences() {
223 CoerceSentence * NormalForm::getsentence(int i) {
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]))
236 int cost=sentences[i]->cost(po,env);
237 if ((totalcost==-1)||(totalcost>cost)) {
243 return sentences[bestmatch];
246 int costfunction(CoercePredicate *p) {
251 // computes the normal form of the given statement
252 SentenceArray * computesentences(Statement *st,bool stat) {
253 switch(st->gettype()) {
255 SentenceArray *left=computesentences(st->getleft(),stat);
256 SentenceArray *right=computesentences(st->getright(),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);
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);
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);
290 case STATEMENT_AND: {
291 SentenceArray *left=computesentences(st->getleft(),stat);
292 SentenceArray *right=computesentences(st->getright(),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);
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);
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);
327 return computesentences(st->getleft(),!stat);
329 CoercePredicate *cp=new CoercePredicate(stat, st->getpredicate());
330 CoercePredicate **cparray=new CoercePredicate *[1];
332 CoerceSentence *cs=new CoerceSentence(cparray,1);
333 CoerceSentence **csarray=new CoerceSentence *[1];
335 return new SentenceArray(csarray,1);
342 // class SentenceArray
344 SentenceArray::SentenceArray(CoerceSentence **sentences, int l) {
346 this->sentences=sentences;