6 public class Optimizer {
10 public Optimizer(State s) {
14 public void optimize() {
16 /* functional relation strength reduction */
22 collapseconstraints();
24 eliminateUnusedSets();
28 public class ReduceRelationVisitor {
31 RelationDescriptor relation;
34 Constraint constraint;
36 public ReduceRelationVisitor(RelationDescriptor rd, Rule rule, State state) {
42 public void rewrite(Constraint theconstraint) {
44 constraint = theconstraint;
45 constraint.logicstatement = (LogicStatement) rw(constraint.logicstatement);
50 if (o instanceof LiteralExpr) {
52 } else if (o instanceof VarExpr) {
54 } else if (o instanceof OpExpr ) {
55 OpExpr oe = (OpExpr) o;
56 oe.left = (Expr) rw(oe.left);
57 if (oe.right != null) {
58 oe.right = (Expr) rw(oe.right);
61 } else if (o instanceof ImageSetExpr) {
62 // shouldn't get here because we have to special case sizeof
63 // which is the only supported region for a strength reduction
64 throw new IRException("shouldn't be here");
65 } else if (o instanceof SetExpr) {
67 } else if (o instanceof SizeofExpr) {
68 SizeofExpr soe = (SizeofExpr) o;
69 // check to see if the relation is the one we are replacing..
70 // and then replace this relationexpr with another
72 // #TODO#: create a new EXPR which is basically an execution of a rule and a new
73 // binding . for sizeofexpr itsa little different because we are only interested
74 // in reporting 0 or 1
76 SetExpr se = soe.getSetExpr();
77 if (se instanceof ImageSetExpr) {
78 ImageSetExpr ise = (ImageSetExpr) se;
79 if (ise.getRelation() == relation) {
80 System.err.println("\nfound instance of sizeof for candidate");
81 soe.prettyPrint(new PrettyPrinter() { public void output(String s) { System.err.print(s); } });
82 System.err.println("");
84 // rewrite this node with a sizeoffunction IR node
85 return new SizeofFunction(ise.getVar(), relation, rule);
90 } else if (o instanceof RelationExpr) {
91 RelationExpr re = (RelationExpr) o;
92 // check to see if the relation is the one we are replacing..
93 // and then replace this relationexpr with another
95 // #TODO#: we'll replace this relationexpr with a new expr which
96 // takes the rule, relation and bindings... when we generate we'll
97 // just insert the rule inline...
99 if (re.getRelation() == relation) {
100 System.err.println("\nfound instance of relationexpr for candidate");
101 re.prettyPrint(new PrettyPrinter() { public void output(String s) { System.err.print(s); } });
102 System.err.println("");
104 // rewrite this node with a relationfunctionexpr IR node
105 return new RelationFunctionExpr(re.getExpr(), relation, rule);
110 } else if (o instanceof RelationFunctionExpr) {
112 } else if (o instanceof SizeofFunction) {
114 } else if (o instanceof Expr) {
115 // catches castexpr, dotexpr, elementofexpr, tupleofexpr
116 throw new IRException("unsupported");
117 } else if (o instanceof ExprPredicate) {
118 ExprPredicate ep = (ExprPredicate) o;
119 ep.expr = (Expr) rw(ep.expr);
121 } else if (o instanceof InclusionPredicate) {
122 throw new IRException("unsupported");
123 } else if (o instanceof LogicStatement) {
124 LogicStatement ls = (LogicStatement) o;
125 ls.left = (LogicStatement) rw(ls.left);
126 if (ls.right != null) {
127 ls.right = (LogicStatement) rw(ls.right);
131 throw new IRException("unsupported");
136 public void strengthreduction() {
138 // ok... need to find all relations that are quantified over...
139 // because these cannot be made into relational functions
141 HashSet forbiddenrelations = new HashSet();
142 Vector rules = state.vRules;
143 for (int i = 0; i < rules.size(); i++) {
144 Rule rule = (Rule) rules.elementAt(i);
145 forbiddenrelations.addAll(rule.getQuantifierDescriptors());
148 // forbiddenrelations now contains all of the descriptors that
149 // are quantified over... strictly we could allow a relation
150 // to be quantified over by replacing the relation with a set
151 // quantifier and rewriting occurrences of the right hand side
152 // with the function applied to the left hand side (the set
153 // element)... but we won't. it is also not clear what the
154 // set of values should be on the left hand side... it is only
155 // well defined for true function, or rather could only be
156 // done efficiently by true functions because the set of s in
157 // S where s.R is not null is not S in general.
159 // ok enough rambling, uh... find candidate relations... these will be as follows...
160 // 1. they'll not be used as an inverse
161 // 2. they'll be generated by a rule of the form [forall x in S], guard => <x, x.field> in R
163 // ok... lets get a list of quantifiers used as inverses. we
164 // are going to loop through the constraints and then we are
165 // going to write some code that searches through the
166 // expression tree for inverses... when we find one we are
167 // going to add it to a set of inversed relations.... which we
168 // will add to our set of forbidden descriptors... then we'll
169 // search through the rules and look at the target descriptors
170 // and find relations that are not on the forbidden list
172 Vector constraints = state.vConstraints;
173 for (int i = 0; i < constraints.size(); i++) {
174 Constraint constraint = (Constraint) constraints.elementAt(i);
176 // ok... no we need to look for inversed relations...
177 Set inversedrelations = constraint.getLogicStatement().getInversedRelations();
178 forbiddenrelations.addAll(inversedrelations);
181 // now we need to search through the rules and look at the target
182 // descriptors... we are looking for relations that are not on
183 // the forbidden list... these we will add to our candidate list...
184 // we can ignore rules that don't have a single quantifier and
185 // we want rules of the form [fa s in S], guard => <s, s.field> in
187 HashMap candidaterelations = new HashMap();
189 for (int i = 0; i < rules.size(); i++) {
190 Rule rule = (Rule) rules.elementAt(i);
192 if (rule.quantifiers.size() == 1) {
194 Quantifier quantifier = (Quantifier) rule.quantifiers.elementAt(0);
195 if (quantifier instanceof SetQuantifier) {
197 SetQuantifier sq = (SetQuantifier) quantifier;
198 VarDescriptor setvar = sq.getVar();
200 // now we got the set var... because there can't be any funny
201 // business in the guard (we don't allow "in?" for these
202 // optimizations) we can go ahead and look at the inclusion...
203 // hopefully its a relationinclusion and then we'll inspect
206 Inclusion inclusion = rule.getInclusion();
208 if (inclusion instanceof RelationInclusion) {
209 // ok... lets make sure the left hand element is the
210 // setdescriptors' var descriptor
211 RelationInclusion ri = (RelationInclusion) inclusion;
213 // lets make sure this relationdescriptor is not in our forbidden list
215 if (!forbiddenrelations.contains(ri.getRelation())) {
218 // lets make sure its of the form <s, s.field>
219 Expr expr = ri.getLeftExpr();
221 // lets make sure its a
222 if (expr instanceof VarExpr) {
223 VarExpr ve = (VarExpr) expr;
224 // lets make sure that ve points to our setvar
225 if (ve.getVar() == setvar) {
226 // ok, this relation is of the form
227 // [forall s in S], guard => <s, ??> in R
229 Expr rightexpr = ri.getRightExpr();
230 if (rightexpr instanceof DotExpr) {
231 DotExpr de = (DotExpr) rightexpr;
232 Expr innerexpr = de.getExpr();
233 if (expr instanceof VarExpr) {
234 VarExpr rightvar = (VarExpr) expr;
235 if (rightvar.getVar() == setvar) {
236 // ok... we have found a candidate
237 // lets add the relation and the rule that builds it to the candidate list
238 candidaterelations.put(ri.getRelation(), rule);
250 // ok... we now have candidaterelations... however, we aren't done... we need to make sure
251 // that they are built from a single rule, because, otherwise, i'll be confused.
253 for (int i = 0; i < rules.size(); i++) {
254 Rule rule = (Rule) rules.elementAt(i);
255 if (rule.getInclusion() instanceof RelationInclusion) {
256 RelationInclusion ri = (RelationInclusion) rule.getInclusion();
257 RelationDescriptor rd = ri.getRelation();
258 if (candidaterelations.containsKey(rd)) {
259 // we need to make sure the rules match
260 Rule buildrule = (Rule) candidaterelations.get(rd);
261 if (buildrule != rule) {
262 // uh oh... relation is candidate but is build
263 // by multiple rules... we don't support this.
264 // remove it from the list of candidates
265 candidaterelations.remove(rd);
271 // ok... now we have some true candidates...
272 // candidates are relations and there rules that build them... basically whenever we see an
273 // instance of this relation we are going to replace it with this relation
277 // alright, lets find some places to replace these candidates!!!
279 candidates = candidaterelations.keySet().iterator();
280 while (candidates.hasNext()) {
281 RelationDescriptor rd = (RelationDescriptor) candidates.next();
282 Rule rule = (Rule) candidaterelations.get(rd);
284 System.err.println(rd.toString() + " is a candidate for STRENGTH REDUCTION!");
286 // ok ... lets seek out and destroy! we only need to look in constraints because
287 // candidates can't appear as quantifiers
289 ReduceRelationVisitor rrv = new ReduceRelationVisitor(rd, rule, state);
291 ListIterator listofconstraints = state.vConstraints.listIterator();
292 while (listofconstraints.hasNext()) {
293 Constraint constraint = (Constraint) listofconstraints.next();
295 // um... ok.. we have a constraint and we want to see if there are any places
296 // to replace the constraint...!!! ok... so basically what are the options
297 // well we allow anything really but the two things that should be swapped are
298 // relationexpr's with our relation and sizeof's... i think that covers everything
301 // so because our IR blows, we are going to have to traverse the IR and make
302 // changes to the IR... this is fine.. we should write a visitor...
304 rrv.rewrite(constraint);
309 // we need to remove the rules that build these relations
310 candidates = candidaterelations.values().iterator();
311 while (candidates.hasNext()) {
312 state.vRules.remove((Rule) candidates.next());
317 public void mergerules() {
320 1. recognize that if you have an *unique* inclusion "... => x in S" and
321 a set of model rules of the form "[forall y in S]" that do not
322 contain any references to other sets (in? operator) then you can move
323 those quantified rules into the original inclusion
326 // lets find unique inclusions! (inclusions are unique if there set identifier is unique)
328 HashMap includedsets = new HashMap();
329 ListIterator rules = state.vRules.listIterator();
331 while (rules.hasNext()) {
332 Rule rule = (Rule) rules.next();
333 Inclusion inclusion = rule.getInclusion();
335 if (inclusion instanceof SetInclusion) {
336 SetInclusion si = (SetInclusion) inclusion;
337 SetDescriptor sd = si.getSet();
339 if (includedsets.containsKey(sd)) {
340 // already contained... set to empty
341 includedsets.put(sd, null);
343 includedsets.put(sd, rule);
349 HashMap uniques = new HashMap(); // this a vector of pairs (or in java... vector pairs)
350 Iterator allsd = includedsets.keySet().iterator();
351 while (allsd.hasNext()) {
352 SetDescriptor sd = (SetDescriptor) allsd.next();
353 Object o = includedsets.get(sd);
355 if (o != null) { // a unique set!
356 uniques.put(sd, (Rule) o);
360 // ok now we have a vector "unique set" of all of the
361 // set descriptors with unique inclusion rules
362 // NOW lets find all of the rules whose quantifiers
363 // have single set quantifiers for each of these set
365 Iterator uniquesetiterator = uniques.keySet().iterator();
366 while (uniquesetiterator.hasNext()) {
367 SetDescriptor sd = (SetDescriptor) uniquesetiterator.next();
368 Rule uniquerule = (Rule) uniques.get(sd);
370 // ok... search for candidate rules...
371 Vector candidaterules = new Vector();
372 ListIterator morerules = state.vRules.listIterator();
373 while (morerules.hasNext()) {
374 Rule rule = (Rule) morerules.next();
375 ListIterator quantifiers = rule.quantifiers();
377 if (rule == uniquerule) continue;
379 if (quantifiers.hasNext()) {
381 Quantifier quantifier = (Quantifier) quantifiers.next();
382 if (quantifier instanceof SetQuantifier) {
383 SetQuantifier sq = (SetQuantifier) quantifier;
384 if (sq.getSet() == sd) {
385 // match! lets make sure this is the sole quantifier
386 if (!quantifiers.hasNext()) {
387 // no more quantifiers! bingo, match
388 candidaterules.addElement(rule);
395 // at this point we have a vector "candidaterules" which is composed
396 // of rules which have a first quantifier, which is a set quantifier
397 // which has the same setdescriptor as one that is unique and has no
398 // further quantifiers (sole quantifier)
400 // we need to now move these rules into the inclusion of "unique rule"
401 // we'll do by creating a meta-inclusion to replace the current
402 // inclusion ... the meta-inclusion will include the current inclusion
403 // to generate the rule's target set as well as the "candidate rules"
405 if (candidaterules.size() > 0) {
406 MetaInclusion meta = new MetaInclusion();
407 Inclusion oldinclusion = uniquerule.getInclusion();
408 meta.setInclusion(oldinclusion);
409 meta.addRules(candidaterules);
410 uniquerule.setInclusion(meta);
412 // no we must remove these rules from the global list so they are generated twice
413 state.vRules.removeAll(candidaterules);
418 public void collapseconstraints() {
421 we are going to look at constraints of the form "[forall s in S], logicstatement"
422 where logicstatement does not make any reference to any descriptors besides "s"
425 HashMap candidates = new HashMap();
426 Iterator constraints = state.vConstraints.iterator();
427 while (constraints.hasNext()) {
428 Constraint constraint = (Constraint) constraints.next();
430 // ok ... we are looping through the constraints trying to find ones
431 // with empty required descriptors in the logicstatement and single setquantifiers
433 if (constraint.getLogicStatement().getRequiredDescriptors().isEmpty()) {
434 // haha, no requried descriptors... this is what we want!
435 if (constraint.quantifiers.size() == 1) {
437 Quantifier q = (Quantifier) constraint.quantifiers.elementAt(0);
438 if (q instanceof SetQuantifier) {
439 SetQuantifier sq = (SetQuantifier) q;
440 SetDescriptor sd = sq.getSet();
441 candidates.put(constraint, sd);
448 // ok... "candidates" now has a set of constraints that have the following
449 // properties: 1) don't have any model descriptors referenced in there body
450 // 2) have a single set quantifier
452 // now we will loop through our rules and find any rules that produce said
455 // we can reuse the constraint iterator
456 constraints = candidates.keySet().iterator();
457 while (constraints.hasNext()) {
458 Constraint constraint = (Constraint) constraints.next();
459 SetDescriptor sd = (SetDescriptor) candidates.get(constraint);
461 // now we loop through all of the rules and find rules that
462 // and items to the set "sd"
464 Iterator rules = state.vRules.iterator();
465 while (rules.hasNext()) {
466 Rule rule = (Rule) rules.next();
467 mergeConstraintIntoRule(constraint, sd, rule);
471 // no we must remove the candidates from the list of constraints
472 // in state.vConstraints so they don't get built (redundant!)
473 state.vConstraints.removeAll(candidates.keySet());
478 void mergeConstraintIntoRule(Constraint constraint, SetDescriptor sd, Rule rule) {
480 if (rule.getInclusion() instanceof SetInclusion) {
481 SetInclusion si = (SetInclusion) rule.getInclusion();
482 if (si.getSet() == sd) {
483 // we have a match... lets convert this inclusion to a meta-inclusion
484 MetaInclusion meta = new MetaInclusion();
485 meta.setInclusion(si);
486 meta.addConstraint(constraint);
487 rule.setInclusion(meta);
489 } else if (rule.getInclusion() instanceof MetaInclusion) {
491 MetaInclusion meta = (MetaInclusion) rule.getInclusion();
493 if (meta.getInclusion() instanceof SetInclusion) {
494 SetInclusion si = (SetInclusion) meta.getInclusion();
495 if (si.getSet() == sd) {
496 // we have a match, we need to add this constraint to the current
498 meta.addConstraint(constraint);
502 // we need to recurse on the sub rules
503 Iterator subrules = meta.rules.iterator();
504 while (subrules.hasNext()) {
505 mergeConstraintIntoRule(constraint, sd, (Rule)subrules.next());
511 public void eliminateUnusedSets() {
513 // ok. so we know that rules with metainclusions have setquantifiers and that all
514 // sub rules and sub constraints use that set. however they don't need that inclusion
517 // so we are going to loop through the constraints and the relations and we are going to keep
518 // track of all the required model descriptors for the top-level rules/constraints...
520 // we are then going to go through all of the rules and look at the inclusion constraints
521 // if the inclusion constraint is adding to a ste that is not on the required list then
522 // we are going to flag that setinclusion with a "donotstore" flag which will prevent it
523 // from adding to its respective sets
525 // there is one complication... if the inclusion is in a meta inclusion then its possible that
526 // the values being added to the set are not unique. ... there are two possibilities, this matters,
527 // or it doesn't matter. ok... it doesn't matter if the rules below aren't optimized by removing
528 // redundancy checks... ok... actually... i don't think it ever matters. in the worst case you'll
529 // do a lot more work than necessary because the sub rules and sub constraints could represent a lot
530 // of work that you don't need to do because there is say , for example, only three distinct items in
531 // 1,000,000 instances...
533 // ok... with that aside aside, we continue.
535 // loop through constraints and relations and get the set of requireddescriptors
537 HashSet required = new HashSet();
539 Iterator allrules = state.vRules.iterator();
540 while (allrules.hasNext()) {
541 required.addAll( ((Rule) allrules.next()).getRequiredDescriptors());
544 Iterator allconstraints = state.vConstraints.iterator();
545 while (allconstraints.hasNext()) {
546 required.addAll( ((Constraint) allconstraints.next()).getRequiredDescriptors());
549 // ok... now the set "required" has a list of all the descriptors that do not need to be built.
550 // lets now loop through the rules and look at the inclusion constraints . if a rule has an setinculsion
551 // whose set is not on the list than the rule is removed. if a rule has a metainclusion whose set inclusion's
552 // set is not on the list the setinclusion is marked "dostore= false"
555 allrules = state.vRules.iterator();
556 while (allrules.hasNext()) {
557 Rule rule = (Rule) allrules.next();
559 if (rule.getInclusion() instanceof SetInclusion) {
560 SetInclusion si = (SetInclusion) rule.getInclusion();
561 if (!required.contains(si.getSet())) {
562 System.err.println("removing " + rule.getLabel());
563 // we don't need this set so remove the rule
567 } else if (rule.getInclusion() instanceof MetaInclusion) {
568 MetaInclusion meta = (MetaInclusion) rule.getInclusion();
569 // we are guanarneed taht the sub inclsion on a meta inclusion is a setinclusion
570 SetInclusion si = (SetInclusion) meta.getInclusion();
571 if (!required.contains(si.getSet())) {
572 // don't need this set, but need its value
574 System.err.println("removing set construction for " + si.getSet().toString() + " in " + rule.getLabel());