6 public class Optimizer {
9 public Optimizer(State s) {
13 public void optimize() {
15 /* functional relation strength reduction */
21 collapseconstraints();
23 eliminateUnusedSets();
27 public class ReduceRelationVisitor {
30 RelationDescriptor relation;
33 Constraint constraint;
35 public ReduceRelationVisitor(RelationDescriptor rd, Rule rule, State state) {
41 public void rewrite(Constraint theconstraint) {
43 constraint = theconstraint;
44 constraint.logicstatement = (LogicStatement) rw(constraint.logicstatement);
49 if (o instanceof LiteralExpr) {
51 } else if (o instanceof VarExpr) {
53 } else if (o instanceof OpExpr ) {
54 OpExpr oe = (OpExpr) o;
55 oe.left = (Expr) rw(oe.left);
56 if (oe.right != null) {
57 oe.right = (Expr) rw(oe.right);
60 } else if (o instanceof ImageSetExpr) {
61 // shouldn't get here because we have to special case sizeof
62 // which is the only supported region for a strength reduction
63 throw new IRException("shouldn't be here");
64 } else if (o instanceof SetExpr) {
66 } else if (o instanceof SizeofExpr) {
67 SizeofExpr soe = (SizeofExpr) o;
68 // check to see if the relation is the one we are replacing..
69 // and then replace this relationexpr with another
71 // #TODO#: create a new EXPR which is basically an execution of a rule and a new
72 // binding . for sizeofexpr itsa little different because we are only interested
73 // in reporting 0 or 1
75 SetExpr se = soe.getSetExpr();
76 if (se instanceof ImageSetExpr) {
77 ImageSetExpr ise = (ImageSetExpr) se;
78 if (ise.getRelation() == relation) {
79 System.err.println("\nfound instance of sizeof for candidate");
80 soe.prettyPrint(new PrettyPrinter() { public void output(String s) { System.err.print(s); } });
81 System.err.println("");
83 // rewrite this node with a sizeoffunction IR node
84 return new SizeofFunction(ise.getVar(), relation, rule);
89 } else if (o instanceof RelationExpr) {
90 RelationExpr re = (RelationExpr) o;
91 // check to see if the relation is the one we are replacing..
92 // and then replace this relationexpr with another
94 // #TODO#: we'll replace this relationexpr with a new expr which
95 // takes the rule, relation and bindings... when we generate we'll
96 // just insert the rule inline...
98 if (re.getRelation() == relation) {
99 System.err.println("\nfound instance of relationexpr for candidate");
100 re.prettyPrint(new PrettyPrinter() { public void output(String s) { System.err.print(s); } });
101 System.err.println("");
103 // rewrite this node with a relationfunctionexpr IR node
104 return new RelationFunctionExpr(re.getExpr(), relation, rule);
109 } else if (o instanceof RelationFunctionExpr) {
111 } else if (o instanceof SizeofFunction) {
113 } else if (o instanceof Expr) {
114 // catches castexpr, dotexpr, elementofexpr, tupleofexpr
115 throw new IRException("unsupported");
116 } else if (o instanceof ExprPredicate) {
117 ExprPredicate ep = (ExprPredicate) o;
118 ep.expr = (Expr) rw(ep.expr);
120 } else if (o instanceof InclusionPredicate) {
121 throw new IRException("unsupported");
122 } else if (o instanceof LogicStatement) {
123 LogicStatement ls = (LogicStatement) o;
124 ls.left = (LogicStatement) rw(ls.left);
125 if (ls.right != null) {
126 ls.right = (LogicStatement) rw(ls.right);
130 throw new IRException("unsupported");
135 public void strengthreduction() {
137 // ok... need to find all relations that are quantified over...
138 // because these cannot be made into relational functions
140 HashSet forbiddenrelations = new HashSet();
141 Vector rules = state.vRules;
142 for (int i = 0; i < rules.size(); i++) {
143 Rule rule = (Rule) rules.elementAt(i);
144 forbiddenrelations.addAll(rule.getQuantifierDescriptors());
147 // forbiddenrelations now contains all of the descriptors that
148 // are quantified over... strictly we could allow a relation
149 // to be quantified over by replacing the relation with a set
150 // quantifier and rewriting occurrences of the right hand side
151 // with the function applied to the left hand side (the set
152 // element)... but we won't. it is also not clear what the
153 // set of values should be on the left hand side... it is only
154 // well defined for true function, or rather could only be
155 // done efficiently by true functions because the set of s in
156 // S where s.R is not null is not S in general.
158 // ok enough rambling, uh... find candidate relations... these will be as follows...
159 // 1. they'll not be used as an inverse
160 // 2. they'll be generated by a rule of the form [forall x in S], guard => <x, x.field> in R
162 // ok... lets get a list of quantifiers used as inverses. we
163 // are going to loop through the constraints and then we are
164 // going to write some code that searches through the
165 // expression tree for inverses... when we find one we are
166 // going to add it to a set of inversed relations.... which we
167 // will add to our set of forbidden descriptors... then we'll
168 // search through the rules and look at the target descriptors
169 // and find relations that are not on the forbidden list
171 Vector constraints = state.vConstraints;
172 for (int i = 0; i < constraints.size(); i++) {
173 Constraint constraint = (Constraint) constraints.elementAt(i);
175 // ok... no we need to look for inversed relations...
176 Set inversedrelations = constraint.getLogicStatement().getInversedRelations();
177 forbiddenrelations.addAll(inversedrelations);
180 // now we need to search through the rules and look at the target
181 // descriptors... we are looking for relations that are not on
182 // the forbidden list... these we will add to our candidate list...
183 // we can ignore rules that don't have a single quantifier and
184 // we want rules of the form [fa s in S], guard => <s, s.field> in
186 HashMap candidaterelations = new HashMap();
188 for (int i = 0; i < rules.size(); i++) {
189 Rule rule = (Rule) rules.elementAt(i);
191 if (rule.quantifiers.size() == 1) {
193 Quantifier quantifier = (Quantifier) rule.quantifiers.elementAt(0);
194 if (quantifier instanceof SetQuantifier) {
196 SetQuantifier sq = (SetQuantifier) quantifier;
197 VarDescriptor setvar = sq.getVar();
199 // now we got the set var... because there can't be any funny
200 // business in the guard (we don't allow "in?" for these
201 // optimizations) we can go ahead and look at the inclusion...
202 // hopefully its a relationinclusion and then we'll inspect
205 Inclusion inclusion = rule.getInclusion();
207 if (inclusion instanceof RelationInclusion) {
208 // ok... lets make sure the left hand element is the
209 // setdescriptors' var descriptor
210 RelationInclusion ri = (RelationInclusion) inclusion;
212 // lets make sure this relationdescriptor is not in our forbidden list
214 if (!forbiddenrelations.contains(ri.getRelation())) {
217 // lets make sure its of the form <s, s.field>
218 Expr expr = ri.getLeftExpr();
220 // lets make sure its a
221 if (expr instanceof VarExpr) {
222 VarExpr ve = (VarExpr) expr;
223 // lets make sure that ve points to our setvar
224 if (ve.getVar() == setvar) {
225 // ok, this relation is of the form
226 // [forall s in S], guard => <s, ??> in R
228 Expr rightexpr = ri.getRightExpr();
229 if (rightexpr instanceof DotExpr) {
230 DotExpr de = (DotExpr) rightexpr;
231 Expr innerexpr = de.getExpr();
232 if (expr instanceof VarExpr) {
233 VarExpr rightvar = (VarExpr) expr;
234 if (rightvar.getVar() == setvar) {
235 // ok... we have found a candidate
236 // lets add the relation and the rule that builds it to the candidate list
237 candidaterelations.put(ri.getRelation(), rule);
249 // ok... we now have candidaterelations... however, we aren't done... we need to make sure
250 // that they are built from a single rule, because, otherwise, i'll be confused.
252 for (int i = 0; i < rules.size(); i++) {
253 Rule rule = (Rule) rules.elementAt(i);
254 if (rule.getInclusion() instanceof RelationInclusion) {
255 RelationInclusion ri = (RelationInclusion) rule.getInclusion();
256 RelationDescriptor rd = ri.getRelation();
257 if (candidaterelations.containsKey(rd)) {
258 // we need to make sure the rules match
259 Rule buildrule = (Rule) candidaterelations.get(rd);
260 if (buildrule != rule) {
261 // uh oh... relation is candidate but is build
262 // by multiple rules... we don't support this.
263 // remove it from the list of candidates
264 candidaterelations.remove(rd);
270 // ok... now we have some true candidates...
271 // candidates are relations and there rules that build them... basically whenever we see an
272 // instance of this relation we are going to replace it with this relation
276 // alright, lets find some places to replace these candidates!!!
278 candidates = candidaterelations.keySet().iterator();
279 while (candidates.hasNext()) {
280 RelationDescriptor rd = (RelationDescriptor) candidates.next();
281 Rule rule = (Rule) candidaterelations.get(rd);
283 System.err.println(rd.toString() + " is a candidate for STRENGTH REDUCTION!");
285 // ok ... lets seek out and destroy! we only need to look in constraints because
286 // candidates can't appear as quantifiers
288 ReduceRelationVisitor rrv = new ReduceRelationVisitor(rd, rule, state);
290 ListIterator listofconstraints = state.vConstraints.listIterator();
291 while (listofconstraints.hasNext()) {
292 Constraint constraint = (Constraint) listofconstraints.next();
294 // um... ok.. we have a constraint and we want to see if there are any places
295 // to replace the constraint...!!! ok... so basically what are the options
296 // well we allow anything really but the two things that should be swapped are
297 // relationexpr's with our relation and sizeof's... i think that covers everything
300 // so because our IR blows, we are going to have to traverse the IR and make
301 // changes to the IR... this is fine.. we should write a visitor...
303 rrv.rewrite(constraint);
308 // we need to remove the rules that build these relations
309 candidates = candidaterelations.values().iterator();
310 while (candidates.hasNext()) {
311 state.vRules.remove((Rule) candidates.next());
316 public void mergerules() {
319 1. recognize that if you have an *unique* inclusion "... => x in S" and
320 a set of model rules of the form "[forall y in S]" that do not
321 contain any references to other sets (in? operator) then you can move
322 those quantified rules into the original inclusion
325 // lets find unique inclusions! (inclusions are unique if there set identifier is unique)
327 HashMap includedsets = new HashMap();
328 ListIterator rules = state.vRules.listIterator();
330 while (rules.hasNext()) {
331 Rule rule = (Rule) rules.next();
332 Inclusion inclusion = rule.getInclusion();
334 if (inclusion instanceof SetInclusion) {
335 SetInclusion si = (SetInclusion) inclusion;
336 SetDescriptor sd = si.getSet();
338 if (includedsets.containsKey(sd)) {
339 // already contained... set to empty
340 includedsets.put(sd, null);
342 includedsets.put(sd, rule);
348 HashMap uniques = new HashMap(); // this a vector of pairs (or in java... vector pairs)
349 Iterator allsd = includedsets.keySet().iterator();
350 while (allsd.hasNext()) {
351 SetDescriptor sd = (SetDescriptor) allsd.next();
352 Object o = includedsets.get(sd);
354 if (o != null) { // a unique set!
355 uniques.put(sd, (Rule) o);
359 // ok now we have a vector "unique set" of all of the
360 // set descriptors with unique inclusion rules
361 // NOW lets find all of the rules whose quantifiers
362 // have single set quantifiers for each of these set
364 Iterator uniquesetiterator = uniques.keySet().iterator();
365 while (uniquesetiterator.hasNext()) {
366 SetDescriptor sd = (SetDescriptor) uniquesetiterator.next();
367 Rule uniquerule = (Rule) uniques.get(sd);
369 // ok... search for candidate rules...
370 Vector candidaterules = new Vector();
371 ListIterator morerules = state.vRules.listIterator();
372 while (morerules.hasNext()) {
373 Rule rule = (Rule) morerules.next();
374 ListIterator quantifiers = rule.quantifiers();
376 if (rule == uniquerule) continue;
378 if (quantifiers.hasNext()) {
380 Quantifier quantifier = (Quantifier) quantifiers.next();
381 if (quantifier instanceof SetQuantifier) {
382 SetQuantifier sq = (SetQuantifier) quantifier;
383 if (sq.getSet() == sd) {
384 // match! lets make sure this is the sole quantifier
385 if (!quantifiers.hasNext()) {
386 // no more quantifiers! bingo, match
387 candidaterules.addElement(rule);
394 // at this point we have a vector "candidaterules" which is composed
395 // of rules which have a first quantifier, which is a set quantifier
396 // which has the same setdescriptor as one that is unique and has no
397 // further quantifiers (sole quantifier)
399 // we need to now move these rules into the inclusion of "unique rule"
400 // we'll do by creating a meta-inclusion to replace the current
401 // inclusion ... the meta-inclusion will include the current inclusion
402 // to generate the rule's target set as well as the "candidate rules"
404 if (candidaterules.size() > 0) {
405 MetaInclusion meta = new MetaInclusion();
406 Inclusion oldinclusion = uniquerule.getInclusion();
407 meta.setInclusion(oldinclusion);
408 meta.addRules(candidaterules);
409 uniquerule.setInclusion(meta);
411 // no we must remove these rules from the global list so they are generated twice
412 state.vRules.removeAll(candidaterules);
417 public void collapseconstraints() {
420 we are going to look at constraints of the form "[forall s in S], logicstatement"
421 where logicstatement does not make any reference to any descriptors besides "s"
424 HashMap candidates = new HashMap();
425 Iterator constraints = state.vConstraints.iterator();
426 while (constraints.hasNext()) {
427 Constraint constraint = (Constraint) constraints.next();
429 // ok ... we are looping through the constraints trying to find ones
430 // with empty required descriptors in the logicstatement and single setquantifiers
432 if (constraint.getLogicStatement().getRequiredDescriptors().isEmpty()) {
433 // haha, no requried descriptors... this is what we want!
434 if (constraint.quantifiers.size() == 1) {
436 Quantifier q = (Quantifier) constraint.quantifiers.elementAt(0);
437 if (q instanceof SetQuantifier) {
438 SetQuantifier sq = (SetQuantifier) q;
439 SetDescriptor sd = sq.getSet();
440 candidates.put(constraint, sd);
447 // ok... "candidates" now has a set of constraints that have the following
448 // properties: 1) don't have any model descriptors referenced in there body
449 // 2) have a single set quantifier
451 // now we will loop through our rules and find any rules that produce said
454 // we can reuse the constraint iterator
455 constraints = candidates.keySet().iterator();
456 while (constraints.hasNext()) {
457 Constraint constraint = (Constraint) constraints.next();
458 SetDescriptor sd = (SetDescriptor) candidates.get(constraint);
460 // now we loop through all of the rules and find rules that
461 // and items to the set "sd"
463 Iterator rules = state.vRules.iterator();
464 while (rules.hasNext()) {
465 Rule rule = (Rule) rules.next();
466 mergeConstraintIntoRule(constraint, sd, rule);
470 // no we must remove the candidates from the list of constraints
471 // in state.vConstraints so they don't get built (redundant!)
472 state.vConstraints.removeAll(candidates.keySet());
477 void mergeConstraintIntoRule(Constraint constraint, SetDescriptor sd, Rule rule) {
479 if (rule.getInclusion() instanceof SetInclusion) {
480 SetInclusion si = (SetInclusion) rule.getInclusion();
481 if (si.getSet() == sd) {
482 // we have a match... lets convert this inclusion to a meta-inclusion
483 MetaInclusion meta = new MetaInclusion();
484 meta.setInclusion(si);
485 meta.addConstraint(constraint);
486 rule.setInclusion(meta);
488 } else if (rule.getInclusion() instanceof MetaInclusion) {
490 MetaInclusion meta = (MetaInclusion) rule.getInclusion();
492 if (meta.getInclusion() instanceof SetInclusion) {
493 SetInclusion si = (SetInclusion) meta.getInclusion();
494 if (si.getSet() == sd) {
495 // we have a match, we need to add this constraint to the current
497 meta.addConstraint(constraint);
501 // we need to recurse on the sub rules
502 Iterator subrules = meta.rules.iterator();
503 while (subrules.hasNext()) {
504 mergeConstraintIntoRule(constraint, sd, (Rule)subrules.next());
510 public void eliminateUnusedSets() {
512 // ok. so we know that rules with metainclusions have setquantifiers and that all
513 // sub rules and sub constraints use that set. however they don't need that inclusion
516 // so we are going to loop through the constraints and the relations and we are going to keep
517 // track of all the required model descriptors for the top-level rules/constraints...
519 // we are then going to go through all of the rules and look at the inclusion constraints
520 // if the inclusion constraint is adding to a ste that is not on the required list then
521 // we are going to flag that setinclusion with a "donotstore" flag which will prevent it
522 // from adding to its respective sets
524 // there is one complication... if the inclusion is in a meta inclusion then its possible that
525 // the values being added to the set are not unique. ... there are two possibilities, this matters,
526 // or it doesn't matter. ok... it doesn't matter if the rules below aren't optimized by removing
527 // redundancy checks... ok... actually... i don't think it ever matters. in the worst case you'll
528 // do a lot more work than necessary because the sub rules and sub constraints could represent a lot
529 // of work that you don't need to do because there is say , for example, only three distinct items in
530 // 1,000,000 instances...
532 // ok... with that aside aside, we continue.
534 // loop through constraints and relations and get the set of requireddescriptors
536 HashSet required = new HashSet();
538 Iterator allrules = state.vRules.iterator();
539 while (allrules.hasNext()) {
540 required.addAll( ((Rule) allrules.next()).getRequiredDescriptors());
543 Iterator allconstraints = state.vConstraints.iterator();
544 while (allconstraints.hasNext()) {
545 required.addAll( ((Constraint) allconstraints.next()).getRequiredDescriptors());
548 // ok... now the set "required" has a list of all the descriptors that do not need to be built.
549 // lets now loop through the rules and look at the inclusion constraints . if a rule has an setinculsion
550 // whose set is not on the list than the rule is removed. if a rule has a metainclusion whose set inclusion's
551 // set is not on the list the setinclusion is marked "dostore= false"
554 allrules = state.vRules.iterator();
555 while (allrules.hasNext()) {
556 Rule rule = (Rule) allrules.next();
558 if (rule.getInclusion() instanceof SetInclusion) {
559 SetInclusion si = (SetInclusion) rule.getInclusion();
560 if (!required.contains(si.getSet())) {
561 System.err.println("removing " + rule.getLabel());
562 // we don't need this set so remove the rule
566 } else if (rule.getInclusion() instanceof MetaInclusion) {
567 MetaInclusion meta = (MetaInclusion) rule.getInclusion();
568 // we are guanarneed taht the sub inclsion on a meta inclusion is a setinclusion
569 SetInclusion si = (SetInclusion) meta.getInclusion();
570 if (!required.contains(si.getSet())) {
571 // don't need this set, but need its value
573 System.err.println("removing set construction for " + si.getSet().toString() + " in " + rule.getLabel());