View Javadoc

1   // InferenceRule.java, created Mar 16, 2004 12:41:14 PM 2004 by jwhaley
2   // Copyright (C) 2004 John Whaley <jwhaley@alum.mit.edu>
3   // Licensed under the terms of the GNU LGPL; see COPYING for details.
4   package net.sf.bddbddb;
5   
6   import java.util.ArrayList;
7   import java.util.Collection;
8   import java.util.Collections;
9   import java.util.HashMap;
10  import java.util.HashSet;
11  import java.util.Iterator;
12  import java.util.LinkedList;
13  import java.util.List;
14  import java.util.Map;
15  import java.util.Set;
16  import jwutil.collections.GenericMultiMap;
17  import jwutil.collections.LinearMap;
18  import jwutil.collections.MultiMap;
19  import jwutil.graphs.Navigator;
20  import jwutil.io.SystemProperties;
21  import jwutil.util.Assert;
22  import net.sf.bddbddb.ir.highlevel.Copy;
23  import net.sf.bddbddb.ir.highlevel.Difference;
24  import net.sf.bddbddb.ir.highlevel.GenConstant;
25  import net.sf.bddbddb.ir.highlevel.Invert;
26  import net.sf.bddbddb.ir.highlevel.Join;
27  import net.sf.bddbddb.ir.highlevel.JoinConstant;
28  import net.sf.bddbddb.ir.highlevel.Project;
29  import net.sf.bddbddb.ir.highlevel.Rename;
30  import net.sf.bddbddb.ir.highlevel.Union;
31  import net.sf.bddbddb.ir.highlevel.Universe;
32  import org.jdom.Element;
33  
34  /***
35   * An InferenceRule represents a single Datalog rule.
36   * 
37   * @author jwhaley
38   * @version $Id: InferenceRule.java 585 2005-06-10 18:04:11Z joewhaley $
39   */
40  public abstract class InferenceRule implements IterationElement {
41      
42      /***
43       * Static rule id factory.
44       */
45      private static int ruleCount;
46      
47      /***
48       * Link to solver.
49       */
50      protected final Solver solver;
51      
52      /***
53       * Unique id number for this rule.
54       */
55      public final int id;
56      
57      /***
58       * List of subgoals for the rule (i.e. the terms on the right hand side).
59       * May be empty.
60       */
61      protected List/*<RuleTerm>*/ top;
62      
63      /***
64       * Head of the rule (i.e. the term on the left hand side).
65       */
66      protected RuleTerm bottom;
67      
68      /***
69       * Set of variables that are necessary.  Initialized after calling initialize().
70       */
71      protected Set/*<Variable>*/ necessaryVariables;
72      
73      /***
74       * Set of variables that are unnecessary.  Initialized after calling initialize().
75       */
76      protected Set/*<Variable>*/ unnecessaryVariables;
77      
78      /***
79       * List of IR instructions that implement this rule.  Used for compilation.
80       */
81      List ir_full, ir_incremental;
82      
83      /***
84       * Set of old values for each of the subgoals.  Used for incrementalization;
85       */
86      Relation[] oldRelationValues;
87      
88      /***
89       * Flag specifying whether or not to split this rule.
90       */
91      boolean split;
92  
93      /***
94       * Flag specifying whether to limit the generated tuples to a single one.
95       */
96      boolean single;
97      
98      /***
99       * The priority of this rule, used in determining iteration order.
100      */
101     int priority = 1;
102     
103     /***
104      * Trace flags to control output of trace information about this rule.
105      */
106     boolean TRACE, TRACE_FULL;
107     
108     /***
109      * Flag specifying whether or not to incrementalize computation of this rule.
110      */
111     boolean incrementalize = !SystemProperties.getProperty("incremental", "yes").equals("no");
112     
113     /***
114      * Flag specifying whether to cache values before or after renaming.
115      * If we cache before rename, we can sometimes avoid renaming the whole relation.
116      * However, in some cases we might need to rename both the diff and the whole relation.
117      */
118     boolean cache_before_rename = true;
119     
120     /***
121      * Flag that shows whether or not this inference rule has been initialized yet.
122      */
123     boolean isInitialized;
124     
125     /***
126      * Code fragments to be executed before invoking this rule.
127      */
128     List preCode;
129 
130     /***
131      * Code fragments to be executed after invoking this rule.
132      */
133     List postCode;
134 
135     /***
136      * Relations (besides the head relation) that are modified as a side effect of this rule.
137      * Used with code fragments.
138      */
139     List extraDefines;
140     
141     /***
142      * Construct a new inference rule.
143      * 
144      * @param solver  solver
145      * @param top  subgoal terms
146      * @param bottom  head term
147      */
148     protected InferenceRule(Solver solver, List/*<RuleTerm>*/ top, RuleTerm bottom) {
149         this(solver, top, bottom, ruleCount++);
150     }
151     protected InferenceRule(Solver solver, List/*<RuleTerm>*/ top, RuleTerm bottom, int id) {
152         this.solver = solver;
153         this.top = top;
154         this.bottom = bottom;
155         this.TRACE = solver.TRACE;
156         this.TRACE_FULL = solver.TRACE_FULL;
157         this.id = id;
158         this.preCode = new LinkedList();
159         this.postCode = new LinkedList();
160         this.extraDefines = new LinkedList();
161     }
162 
163     /***
164      * Initialize this inference rule, if it hasn't been already.
165      */
166     void initialize() {
167         if (isInitialized) return;
168         calculateNecessaryVariables();
169         isInitialized = true;
170     }
171 
172     /***
173      * Returns the list of subgoals.  Subgoals are the terms to the right
174      * of the ":-".
175      * 
176      * @return  list of subgoals
177      */
178     public List/*<RuleTerm>*/ getSubgoals() {
179         return top;
180     }
181     
182     /***
183      * Returns the head term.  That is the term on the left of the ":-".
184      * 
185      * @return  the head term
186      */
187     public RuleTerm getHead() {
188         return bottom;
189     }
190     
191     /***
192      * Calculate the set of necessary variables in the given list of terms
193      * assuming that the given collection of variables has already been listed once.
194      * 
195      * @param s  initial collection of variables that have been listed
196      * @param terms  terms to check
197      * @return  set of necessary variables
198      */
199     static Set calculateNecessaryVariables(Collection s, List terms) {
200         Set necessaryVariables = new HashSet();
201         Set unnecessaryVariables = new HashSet(s);
202         for (int i = 0; i < terms.size(); ++i) {
203             RuleTerm rt = (RuleTerm) terms.get(i);
204             for (int j = 0; j < rt.variables.size(); ++j) {
205                 Variable v = (Variable) rt.variables.get(j);
206                 if (necessaryVariables.contains(v)) continue;
207                 if (unnecessaryVariables.contains(v)) {
208                     necessaryVariables.add(v);
209                     unnecessaryVariables.remove(v);
210                 } else {
211                     unnecessaryVariables.add(v);
212                 }
213             }
214         }
215         return necessaryVariables;
216     }
217 
218     /***
219      * Calculate and return the set of necessary variables for this rule.
220      * Sets the necessaryVariables and unnecessaryVariables fields.
221      * 
222      * @return  set of necessary variables.
223      */
224     protected Set calculateNecessaryVariables() {
225         necessaryVariables = new HashSet();
226         unnecessaryVariables = new HashSet();
227         for (int i = 0; i < top.size(); ++i) {
228             RuleTerm rt = (RuleTerm) top.get(i);
229             for (int j = 0; j < rt.variables.size(); ++j) {
230                 Variable v = (Variable) rt.variables.get(j);
231                 if (necessaryVariables.contains(v)) continue;
232                 if (unnecessaryVariables.contains(v)) {
233                     necessaryVariables.add(v);
234                     unnecessaryVariables.remove(v);
235                 } else {
236                     unnecessaryVariables.add(v);
237                 }
238             }
239         }
240         for (int j = 0; j < bottom.variables.size(); ++j) {
241             Variable v = (Variable) bottom.variables.get(j);
242             if (necessaryVariables.contains(v)) continue;
243             if (unnecessaryVariables.contains(v)) {
244                 necessaryVariables.add(v);
245                 unnecessaryVariables.remove(v);
246             } else {
247                 unnecessaryVariables.add(v);
248             }
249         }
250         return necessaryVariables;
251     }
252 
253     /***
254      * Checks to see if there are any variables that only appear once.
255      */
256     public Variable checkUnnecessaryVariables() {
257         calculateNecessaryVariables();
258         for (Iterator i = unnecessaryVariables.iterator(); i.hasNext(); ) {
259             Variable v = (Variable) i.next();
260             if (v instanceof Constant) continue;
261             if (!"_".equals(v.name) && !"*".equals(v.name)) {
262                 return v;
263             }
264         }
265         return null;
266     }
267     
268     /***
269      * Update the head relation of this rule based on the subgoal relations.
270      * Returns true if the head relation changed.
271      * 
272      * @return  true if the head relation changed
273      */
274     public abstract boolean update();
275 
276     /***
277      * Report statistics about this rule.
278      */
279     public abstract void reportStats();
280 
281     /***
282      * Free the memory associated with this rule.  After calling this, the rule can
283      * no longer be used.
284      */
285     public void free() {
286         if (oldRelationValues != null) {
287             for (int i = 0; i < oldRelationValues.length; ++i) {
288                 oldRelationValues[i].free();
289             }
290         }
291     }
292 
293     /***
294      * Given a collection of rules, returns a multimap that maps relations to
295      * the rules that use that relation.
296      * 
297      * @param rules  collection of rules
298      * @return  multimap from relations to rules that use them
299      */
300     public static MultiMap getRelationToUsingRule(Collection rules) {
301         MultiMap mm = new GenericMultiMap();
302         for (Iterator i = rules.iterator(); i.hasNext();) {
303             Object o = i.next();
304             if (o instanceof InferenceRule) {
305                 InferenceRule ir = (InferenceRule) o;
306                 for (Iterator j = ir.top.iterator(); j.hasNext();) {
307                     RuleTerm rt = (RuleTerm) j.next();
308                     mm.add(rt.relation, ir);
309                 }
310             }
311         }
312         return mm;
313     }
314 
315     /***
316      * Given a collection of rules, returns a multimap that maps relations to
317      * the rules that define that relation.
318      * 
319      * @param rules  collection of rules
320      * @return  multimap from relations to rules that define them
321      */
322     public static MultiMap getRelationToDefiningRule(Collection rules) {
323         MultiMap mm = new GenericMultiMap();
324         for (Iterator i = rules.iterator(); i.hasNext();) {
325             Object o = i.next();
326             if (o instanceof InferenceRule) {
327                 InferenceRule ir = (InferenceRule) o;
328                 mm.add(ir.bottom.relation, ir);
329                 for (Iterator j = ir.extraDefines.iterator(); j.hasNext(); ) {
330                     Relation r = (Relation) j.next();
331                     mm.add(r, ir);
332                 }
333             }
334         }
335         return mm;
336     }
337 
338     /***
339      * Splits a rule into a collection of rules, such that each of the new rules
340      * has only two subgoals.  The current rule is simply mutated and not returned
341      * in the collection.
342      * 
343      * @param myIndex  index number used to name the new rules
344      * @return  collection of new inference rules
345      */
346     public Collection/*<InferenceRule>*/ split(int myIndex) {
347         List newRules = new LinkedList();
348         int count = 0;
349         while (top.size() > 2) {
350             RuleTerm rt1 = (RuleTerm) top.remove(0);
351             RuleTerm rt2 = (RuleTerm) top.remove(0);
352             if (TRACE) solver.out.println("Combining " + rt1 + " and " + rt2 + " into a new rule.");
353             // Calculate our new necessary variables.
354             LinkedList ll = new LinkedList();
355             ll.addAll(rt1.variables);
356             ll.addAll(rt2.variables);
357             LinkedList terms = new LinkedList(top);
358             terms.add(bottom);
359             Set myNewNecessaryVariables = calculateNecessaryVariables(ll, terms);
360             List newTop = new LinkedList();
361             newTop.add(rt1);
362             newTop.add(rt2);
363             // Make a new relation for the bottom.
364             Map neededVariables = new LinearMap();
365             Map variableOptions = new HashMap();
366             Iterator i = rt1.variables.iterator();
367             Iterator j = rt1.relation.attributes.iterator();
368             while (i.hasNext()) {
369                 Variable v = (Variable) i.next();
370                 Attribute a = (Attribute) j.next();
371                 Domain d = a.attributeDomain;
372                 String o = a.attributeOptions;
373                 if (!myNewNecessaryVariables.contains(v)) continue;
374                 Domain d2 = (Domain) neededVariables.get(v);
375                 if (d2 != null && d != d2) {
376                     throw new IllegalArgumentException(v + ": " + d + " != " + d2);
377                 }
378                 neededVariables.put(v, d);
379                 String o2 = (String) variableOptions.get(v);
380                 if (o == null || o.equals("")) o = o2;
381                 if (o2 == null || o2.equals("")) o2 = o;
382                 if (o != null && o2 != null && !o.equals(o2)) {
383                     throw new IllegalArgumentException(v + ": " + o + " != " + o2);
384                 }
385                 variableOptions.put(v, o);
386             }
387             i = rt2.variables.iterator();
388             j = rt2.relation.attributes.iterator();
389             while (i.hasNext()) {
390                 Variable v = (Variable) i.next();
391                 Attribute a = (Attribute) j.next();
392                 Domain d = a.attributeDomain;
393                 String o = a.attributeOptions;
394                 if (!myNewNecessaryVariables.contains(v)) continue;
395                 Domain d2 = (Domain) neededVariables.get(v);
396                 if (d2 != null && d != d2) {
397                     throw new IllegalArgumentException(v + ": " + d + " != " + d2);
398                 }
399                 neededVariables.put(v, d);
400                 String o2 = (String) variableOptions.get(v);
401                 if (o == null || o.equals("")) o = o2;
402                 if (o2 == null || o2.equals("")) o2 = o;
403                 if (o != null && o2 != null && !o.equals(o2)) {
404                     throw new IllegalArgumentException(v + ": " + o + " != " + o2);
405                 }
406                 variableOptions.put(v, o);
407             }
408             // Make a new relation for the bottom.
409             List attributes = new LinkedList();
410             List newVariables = new LinkedList();
411             for (i = neededVariables.entrySet().iterator(); i.hasNext();) {
412                 Map.Entry e = (Map.Entry) i.next();
413                 Variable v = (Variable) e.getKey();
414                 Domain d = (Domain) e.getValue();
415                 String o = (String) variableOptions.get(v);
416                 Attribute a = new Attribute("_" + v, d, o);
417                 attributes.add(a);
418                 newVariables.add(v);
419             }
420             String relationName = bottom.relation.name + "_" + myIndex + "_" + count;
421             if (TRACE) solver.out.println("New attributes: " + attributes);
422             Relation newRelation = solver.createRelation(relationName, attributes);
423             //newRelation.priority = bottom.relation.priority;
424             if (TRACE) solver.out.println("New relation: " + newRelation);
425             RuleTerm newBottom = new RuleTerm(newRelation, newVariables);
426             InferenceRule newRule = solver.createInferenceRule(newTop, newBottom);
427             if (TRACE) solver.out.println("New rule: " + newRule);
428             newRule.calculateNecessaryVariables();
429             if (TRACE) solver.out.println("Necessary variables: " + newRule.necessaryVariables);
430             //s.rules.add(newRule);
431             newRules.add(newRule);
432             newRule.copyOptions(this);
433             boolean changed = newRule.preCode.addAll(this.preCode);
434             this.preCode.clear();
435             if (changed) {
436                 // todo: split extraDefines into pre- and post-
437                 newRule.extraDefines.addAll(this.extraDefines);
438             }
439             // Now include the bottom of the new rule on the top of our rule.
440             top.add(0, newBottom);
441             // Reinitialize this rule because the terms have changed.
442             this.calculateNecessaryVariables();
443             if (TRACE) solver.out.println("Current rule is now: " + this);
444             if (TRACE) solver.out.println("My new necessary variables: " + necessaryVariables);
445             Assert._assert(necessaryVariables.equals(myNewNecessaryVariables));
446             ++count;
447         }
448         return newRules;
449     }
450 
451     /***
452      * Utility function to retain in a multimap only the elements in a given collection.
453      * 
454      * @param mm  multimap
455      * @param c  collection
456      */
457     static void retainAll(MultiMap mm, Collection c) {
458         for (Iterator i = mm.keySet().iterator(); i.hasNext();) {
459             Object o = i.next();
460             if (!c.contains(o)) {
461                 i.remove();
462                 continue;
463             }
464             Collection vals = mm.getValues(o);
465             for (Iterator j = vals.iterator(); j.hasNext();) {
466                 Object o2 = j.next();
467                 if (!c.contains(o2)) {
468                     j.remove();
469                 }
470             }
471             if (vals.isEmpty()) i.remove();
472         }
473     }
474 
475     /***
476      * Utility function to remove from a multimap all of the elements in a given collection.
477      * 
478      * @param mm  multimap
479      * @param c  collection
480      */
481     static void removeAll(MultiMap mm, Collection c) {
482         for (Iterator i = mm.keySet().iterator(); i.hasNext();) {
483             Object o = i.next();
484             if (c.contains(o)) {
485                 i.remove();
486                 continue;
487             }
488             Collection vals = mm.getValues(o);
489             for (Iterator j = vals.iterator(); j.hasNext();) {
490                 Object o2 = j.next();
491                 if (c.contains(o2)) {
492                     j.remove();
493                 }
494             }
495             if (vals.isEmpty()) i.remove();
496         }
497     }
498 
499     /***
500      * Copy the options from another rule into this one.
501      * 
502      * @param that
503      */
504     public void copyOptions(InferenceRule that) {
505         this.TRACE = that.TRACE;
506         this.TRACE_FULL = that.TRACE_FULL;
507         this.incrementalize = that.incrementalize;
508         this.cache_before_rename = that.cache_before_rename;
509         //this.priority = that.priority;
510     }
511     
512     /***
513      * A navigator that can navigate over rule dependencies.
514      * next() on a rule returns its head relation, and
515      * next() on a relation returns the rules that use that relation.
516      * Likewise, prev() on a rule returns its subgoal relations,
517      * and prev() on a relation returns the rules that define that relation.
518      * 
519      * This class also allows you to remove edges/nodes from it.
520      */
521     public static class DependenceNavigator implements Navigator {
522         MultiMap relationToUsingRule;
523         MultiMap relationToDefiningRule;
524 
525         /***
526          * Construct a new DependenceNavigator using the given collection of rules.
527          * 
528          * @param rules  rules
529          */
530         public DependenceNavigator(Collection/*<InferenceRule>*/ rules) {
531             this(getRelationToUsingRule(rules), getRelationToDefiningRule(rules));
532         }
533 
534         /***
535          * Retain only the relations/rules in the given collection.
536          * 
537          * @param c  collection to retain
538          */
539         public void retainAll(Collection c) {
540             InferenceRule.retainAll(relationToUsingRule, c);
541             InferenceRule.retainAll(relationToDefiningRule, c);
542         }
543 
544         /***
545          * Remove all of the relations/rules in the given collection.
546          * 
547          * @param c  collection to remove
548          */
549         public void removeAll(Collection c) {
550             InferenceRule.removeAll(relationToUsingRule, c);
551             InferenceRule.removeAll(relationToDefiningRule, c);
552         }
553 
554         /***
555          * Remove a specific edge from this navigator.
556          * 
557          * @param from  source of edge
558          * @param to  target of edge
559          */
560         public void removeEdge(Object from, Object to) {
561             if (from instanceof InferenceRule) {
562                 InferenceRule ir = (InferenceRule) from;
563                 Relation r = (Relation) to;
564                 relationToDefiningRule.remove(r, ir);
565             } else {
566                 Relation r = (Relation) from;
567                 InferenceRule ir = (InferenceRule) to;
568                 relationToUsingRule.remove(r, ir);
569             }
570         }
571 
572         /***
573          * Construct a new DependenceNavigator that is a copy of another
574          * DependenceNavigator.
575          * 
576          * @param that  the one to copy from
577          */
578         public DependenceNavigator(DependenceNavigator that) {
579             this(((GenericMultiMap) that.relationToUsingRule).copy(), ((GenericMultiMap) that.relationToDefiningRule).copy());
580         }
581 
582         /***
583          * Not to be called externally.
584          * 
585          * @param relationToUsingRule
586          * @param relationToDefiningRule
587          */
588         private DependenceNavigator(MultiMap relationToUsingRule, MultiMap relationToDefiningRule) {
589             super();
590             this.relationToUsingRule = relationToUsingRule;
591             this.relationToDefiningRule = relationToDefiningRule;
592         }
593 
594         /*
595          * (non-Javadoc)
596          * 
597          * @see joeq.Util.Graphs.Navigator#next(java.lang.Object)
598          */
599         public Collection next(Object node) {
600             if (node instanceof InferenceRule) {
601                 InferenceRule ir = (InferenceRule) node;
602                 Collection extras = ir.extraDefines;
603                 if (extras == null || extras.isEmpty()) {
604                     if (relationToDefiningRule.contains(ir.bottom.relation, ir)) return Collections.singleton(ir.bottom.relation);
605                     else return Collections.EMPTY_SET;
606                 } else {
607                     LinkedList result = new LinkedList();
608                     for (Iterator i = extras.iterator(); i.hasNext(); ) {
609                         Relation r = (Relation) i.next();
610                         if (relationToDefiningRule.contains(r, ir)) result.add(r);
611                     }
612                     if (relationToDefiningRule.contains(ir.bottom.relation, ir)) result.add(ir.bottom.relation);
613                     return result;
614                 }
615             } else {
616                 Relation r = (Relation) node;
617                 Collection c = relationToUsingRule.getValues(r);
618                 return c;
619             }
620         }
621 
622         /*
623          * (non-Javadoc)
624          * 
625          * @see joeq.Util.Graphs.Navigator#prev(java.lang.Object)
626          */
627         public Collection prev(Object node) {
628             if (node instanceof InferenceRule) {
629                 InferenceRule ir = (InferenceRule) node;
630                 List list = new LinkedList();
631                 for (Iterator i = ir.top.iterator(); i.hasNext();) {
632                     RuleTerm rt = (RuleTerm) i.next();
633                     if (relationToUsingRule.contains(rt.relation, ir)) list.add(rt.relation);
634                 }
635                 return list;
636             } else {
637                 Relation r = (Relation) node;
638                 Collection c = relationToDefiningRule.getValues(r);
639                 return c;
640             }
641         }
642     }
643 
644     /***
645      * Helper function for IR generation.
646      * Generate code to project away unnecessary variables and restrict constants.
647      * 
648      * @param ir  list of IR instructions
649      * @param rt  subgoal term
650      * @return  resulting relation after projecting and restricting
651      */
652     Relation generate1(List ir, RuleTerm rt) {
653         Relation top_r = rt.relation;
654         Collection varsToProject = new LinkedList(rt.variables);
655         
656         varsToProject.removeAll(necessaryVariables);
657         if (!varsToProject.isEmpty()) {
658             if (solver.TRACE) solver.out.println("Projecting away variables: " + varsToProject);
659             List newAttributes = new LinkedList();
660             for (int j = 0; j < rt.numberOfVariables(); ++j) {
661                 Variable v = rt.getVariable(j);
662                 if (!varsToProject.contains(v)) {
663                     newAttributes.add(top_r.getAttribute(j));
664                 } else if (v instanceof Constant) {
665                     Relation new_r = top_r.copy();
666                     new_r.initialize();
667                     Attribute a = top_r.getAttribute(j);
668                     long value = ((Constant) v).value;
669                     JoinConstant jc = new JoinConstant(new_r, top_r, a, value);
670                     if (solver.TRACE) solver.out.println("Generated: " + jc);
671                     ir.add(jc);
672                     top_r = new_r;
673                 }
674             }
675             Relation new_r = solver.createRelation(top_r + "_p", newAttributes);
676             new_r.initialize();
677             Project p = new Project(new_r, top_r);
678             if (solver.TRACE) solver.out.println("Generated: " + p);
679             ir.add(p);
680             top_r = new_r;
681         }
682         return top_r;
683     }
684 
685     /***
686      * Generate and return the IR that implements this rule.
687      * 
688      * @return  list of IR instructions
689      */
690     public List/*<Operation>*/ generateIR() {
691         if (ir_full != null) return ir_full;
692         List ir = new LinkedList();
693         Relation result = null;
694         Map varToAttrib = new HashMap();
695         int x = 0;
696         for (Iterator i = top.iterator(); i.hasNext(); ++x) {
697             RuleTerm rt = (RuleTerm) i.next();
698             // Step 1: Project away unnecessary variables and restrict
699             // constants.
700             Relation r = generate1(ir, rt);
701             // If we are incrementalizing, cache copies of the input relations.
702             // This happens after we have quantified away and restricted constants,
703             // but before we do renaming.
704             if (incrementalize && cache_before_rename) {
705                 if (oldRelationValues == null) oldRelationValues = new Relation[top.size()];
706                 oldRelationValues[x] = r.copy();
707                 oldRelationValues[x].initialize();
708                 Copy c = new Copy(oldRelationValues[x], r);
709                 if (solver.TRACE) solver.out.println("Generated: " + c);
710                 ir.add(c);
711             }
712             // Calculate renames.
713             List newAttributes = new LinkedList();
714             Map renames = new LinearMap();
715             for (int j = 0; j < rt.numberOfVariables(); ++j) {
716                 Variable v = rt.getVariable(j);
717                 if (unnecessaryVariables.contains(v)) continue;
718                 Attribute a = rt.relation.getAttribute(j);
719                 Attribute a2 = (Attribute) varToAttrib.get(v);
720                 if (a2 == null) {
721                     if (result != null && result.attributes.contains(a)) {
722                         // Attribute is already present in result, use a
723                         // different attribute.
724                         a2 = new Attribute(a.attributeName + '\'', a.attributeDomain, "");
725                         renames.put(a, a2);
726                         a = a2;
727                     }
728                     varToAttrib.put(v, a2 = a);
729                 } else if (!a2.equals(a)) {
730                     renames.put(a, a2);
731                 }
732                 newAttributes.add(a2);
733             }
734             if (!renames.isEmpty()) {
735                 Relation new_r = solver.createRelation(r + "_r", newAttributes);
736                 new_r.initialize();
737                 Rename rename = new Rename(new_r, r, renames);
738                 if (solver.TRACE) solver.out.println("Generated: " + rename);
739                 ir.add(rename);
740                 r = new_r;
741             }
742             // If we are incrementalizing, cache copies of the input relations.
743             // If the option is set, we do this after the rename.
744             if (incrementalize && !cache_before_rename) {
745                 if (oldRelationValues == null) oldRelationValues = new Relation[top.size()];
746                 oldRelationValues[x] = r.copy();
747                 oldRelationValues[x].initialize();
748                 Copy c = new Copy(oldRelationValues[x], r);
749                 if (solver.TRACE) solver.out.println("Generated: " + c);
750                 ir.add(c);
751             }
752             if (result != null) {
753                 // Do a "join".
754                 newAttributes = new LinkedList(result.attributes);
755                 newAttributes.removeAll(r.attributes);
756                 newAttributes.addAll(r.attributes);
757                 Relation new_r = solver.createRelation(r + "_j", newAttributes);
758                 new_r.initialize();
759                 Join join = new Join(new_r, r, result);
760                 if (solver.TRACE) solver.out.println("Generated: " + join);
761                 ir.add(join);
762                 result = new_r;
763             } else {
764                 // This is the first loop iteration, so there is no prior result
765                 // to join with.
766                 result = r;
767             }
768             if (solver.TRACE && result != null) solver.out.println("Result attributes after join: " + result.attributes);
769             // Project away unnecessary attributes.
770             List toProject = new LinkedList();
771             outer : for (int k = 0; k < rt.numberOfVariables(); ++k) {
772                 Variable v = rt.getVariable(k);
773                 if (unnecessaryVariables.contains(v)) continue;
774                 Attribute a = (Attribute) varToAttrib.get(v);
775                 Assert._assert(a != null);
776                 if (solver.TRACE) solver.out.print("Variable " + v + " Attribute " + a + ": ");
777                 Assert._assert(result.attributes.contains(a));
778                 if (bottom.variables.contains(v)) {
779                     if (solver.TRACE) solver.out.println("variable needed for bottom");
780                     continue;
781                 }
782                 Iterator j = top.iterator();
783                 while (j.next() != rt);
784                 while (j.hasNext()) {
785                     RuleTerm rt2 = (RuleTerm) j.next();
786                     if (rt2.variables.contains(v)) {
787                         if (solver.TRACE) solver.out.println("variable needed for future term");
788                         continue outer;
789                     }
790                 }
791                 if (solver.TRACE) solver.out.println("Not needed anymore, projecting away");
792                 toProject.add(a);
793             }
794             if (!toProject.isEmpty()) {
795                 newAttributes = new LinkedList(result.attributes);
796                 newAttributes.removeAll(toProject);
797                 Relation result2 = solver.createRelation(result + "_p2", newAttributes);
798                 result2.initialize();
799                 Project p = new Project(result2, result);
800                 if (solver.TRACE) solver.out.println("Generated: " + p);
801                 ir.add(p);
802                 result = result2;
803             }
804         }
805         // Rename result to match head relation.
806         Map renames = new LinearMap();
807         List newAttributes = new LinkedList();
808         for (int j = 0; j < bottom.numberOfVariables(); ++j) {
809             Variable v = bottom.getVariable(j);
810             if (unnecessaryVariables.contains(v)) continue;
811             Attribute a = bottom.relation.getAttribute(j);
812             Attribute a2 = (Attribute) varToAttrib.get(v);
813             //solver.out.println("Variable "+v+" has attribute "+a2);
814             Assert._assert(a2 != null);
815             if (!a2.equals(a)) {
816                 renames.put(a2, a);
817             }
818             newAttributes.add(a);
819         }
820         if (!renames.isEmpty()) {
821             Relation result2 = solver.createRelation(result + "_r2", newAttributes);
822             result2.initialize();
823             Rename rename = new Rename(result2, result, renames);
824             if (solver.TRACE) solver.out.println("Generated: " + rename);
825             ir.add(rename);
826             result = result2;
827         }
828         // Restrict constants.
829         for (int j = 0; j < bottom.numberOfVariables(); ++j) {
830             Variable v = bottom.getVariable(j);
831             if (v instanceof Constant) {
832                 Attribute a = bottom.relation.getAttribute(j);
833                 long value = ((Constant) v).getValue();
834                 if (result == null) {
835                     // Empty right-hand-side.
836                     result = bottom.relation.copy();
837                     result.initialize();
838                     GenConstant c = new GenConstant(result, a, value);
839                     if (solver.TRACE) solver.out.println("Generated: " + c);
840                     ir.add(c);
841                 } else {
842                     List a2 = new LinkedList(result.attributes);
843                     a2.add(a);
844                     Relation result2 = solver.createRelation(result.name+"_jc", a2);
845                     result2.initialize();
846                     JoinConstant jc = new JoinConstant(result2, result, a, value);
847                     if (solver.TRACE) solver.out.println("Generated: " + jc);
848                     ir.add(jc);
849                     result = result2;
850                 }
851             }
852         }
853         if (result != null) {
854             // Finally, union in the result.
855             Union u = new Union(bottom.relation, bottom.relation, result);
856             if (solver.TRACE) solver.out.println("Generated: " + u);
857             ir.add(u);
858         } else {
859             // No constants: Universal set.
860             Universe u = new Universe(bottom.relation);
861             if (solver.TRACE) solver.out.println("Generated: " + u);
862             ir.add(u);
863         }
864         if (bottom.relation.negated != null) {
865             // Update negated.
866             Invert i = new Invert(bottom.relation.negated, bottom.relation);
867             if (solver.TRACE) solver.out.println("Generated: " + i);
868             ir.add(i);
869         }
870         ir_full = ir;
871         return ir;
872     }
873 
874     /***
875      * Generate and return the IR that implements the incrementalized version of this rule.
876      * 
877      * @return  list of IR instructions
878      */
879     public List/*<Operation>*/ generateIR_incremental() {
880         if (ir_incremental != null) return ir_incremental;
881         LinkedList ir = new LinkedList();
882         Map varToAttrib = new HashMap();
883         Relation[] allRelationValues = new Relation[top.size()];
884         Relation[] newRelationValues = new Relation[top.size()];
885         List[] toProject = new LinkedList[top.size()];
886         List oldAttributes = null;
887         int x = 0;
888         for (Iterator i = top.iterator(); i.hasNext(); ++x) {
889             RuleTerm rt = (RuleTerm) i.next();
890             // Step 1: Project away unnecessary variables and restrict
891             // constants.
892             Relation r = generate1(ir, rt);
893             allRelationValues[x] = r;
894             if (cache_before_rename) {
895                 if (oldRelationValues == null) oldRelationValues = new Relation[top.size()];
896                 if (oldRelationValues[x] == null) {
897                     oldRelationValues[x] = r.copy();
898                     oldRelationValues[x].initialize();
899                 }
900                 // TODO: calculate if we need the whole relation.
901                 newRelationValues[x] = oldRelationValues[x].copy();
902                 newRelationValues[x].initialize();
903                 Difference diff = new Difference(newRelationValues[x], allRelationValues[x], oldRelationValues[x]);
904                 if (solver.TRACE) solver.out.println("Generated: " + diff);
905                 ir.add(diff);
906                 Copy copy = new Copy(oldRelationValues[x], allRelationValues[x]);
907                 if (solver.TRACE) solver.out.println("Generated: " + copy);
908                 ir.add(copy);
909             }
910             // Calculate renames.
911             List newAttributes = new LinkedList();
912             Map renames = new LinearMap();
913             for (int j = 0; j < rt.numberOfVariables(); ++j) {
914                 Variable v = rt.getVariable(j);
915                 if (unnecessaryVariables.contains(v)) continue;
916                 Attribute a = rt.relation.getAttribute(j);
917                 Attribute a2 = (Attribute) varToAttrib.get(v);
918                 if (a2 == null) {
919                     if (oldAttributes != null && oldAttributes.contains(a)) {
920                         // Attribute is already present in result, use a
921                         // different attribute.
922                         a2 = new Attribute(a.attributeName + '\'', a.attributeDomain, "");
923                         renames.put(a, a2);
924                         a = a2;
925                     }
926                     varToAttrib.put(v, a2 = a);
927                 } else if (!a2.equals(a)) {
928                     renames.put(a, a2);
929                 }
930                 newAttributes.add(a2);
931             }
932             if (!renames.isEmpty()) {
933                 if (cache_before_rename) {
934                     Relation new_r = solver.createRelation(newRelationValues[x] + "_r", newAttributes);
935                     new_r.initialize();
936                     Rename rename = new Rename(new_r, newRelationValues[x], renames);
937                     if (solver.TRACE) solver.out.println("Generated: " + rename);
938                     ir.add(rename);
939                     newRelationValues[x] = new_r;
940                 }
941                 // TODO: only rename whole relation if it is actually needed.
942                 Relation new_r = solver.createRelation(r + "_r", newAttributes);
943                 new_r.initialize();
944                 Rename rename = new Rename(new_r, r, renames);
945                 if (solver.TRACE) solver.out.println("Generated: " + rename);
946                 ir.add(rename);
947                 r = new_r;
948             }
949             allRelationValues[x] = r;
950             if (!cache_before_rename) {
951                 if (oldRelationValues == null) oldRelationValues = new Relation[top.size()];
952                 if (oldRelationValues[x] == null) {
953                     oldRelationValues[x] = r.copy();
954                     oldRelationValues[x].initialize();
955                 }
956                 newRelationValues[x] = oldRelationValues[x].copy();
957                 newRelationValues[x].initialize();
958                 Difference diff = new Difference(newRelationValues[x], allRelationValues[x], oldRelationValues[x]);
959                 if (solver.TRACE) solver.out.println("Generated: " + diff);
960                 ir.add(diff);
961                 Copy copy = new Copy(oldRelationValues[x], allRelationValues[x]);
962                 if (solver.TRACE) solver.out.println("Generated: " + copy);
963                 ir.add(copy);
964             }
965             oldAttributes = new LinkedList();
966             if (x > 0) oldAttributes.addAll(allRelationValues[x - 1].attributes);
967             oldAttributes.removeAll(r.attributes);
968             oldAttributes.addAll(r.attributes);
969             // Project away unnecessary attributes.
970             toProject[x] = new LinkedList();
971             outer : for (int k = 0; k < rt.numberOfVariables(); ++k) {
972                 Variable v = rt.getVariable(k);
973                 if (unnecessaryVariables.contains(v)) continue;
974                 Attribute a = (Attribute) varToAttrib.get(v);
975                 Assert._assert(a != null);
976                 if (solver.TRACE) solver.out.print("Variable " + v + " Attribute " + a + ": ");
977                 Assert._assert(oldAttributes.contains(a));
978                 if (bottom.variables.contains(v)) {
979                     if (solver.TRACE) solver.out.println("variable needed for bottom");
980                     continue;
981                 }
982                 Iterator j = top.iterator();
983                 while (j.next() != rt);
984                 while (j.hasNext()) {
985                     RuleTerm rt2 = (RuleTerm) j.next();
986                     if (rt2.variables.contains(v)) {
987                         if (solver.TRACE) solver.out.println("variable needed for future term");
988                         continue outer;
989                     }
990                 }
991                 if (solver.TRACE) solver.out.println("Not needed anymore, projecting away");
992                 toProject[x].add(a);
993             }
994         }
995         for (x = 0; x < newRelationValues.length; ++x) {
996             Relation result = newRelationValues[x];
997             for (int y = 0; y < allRelationValues.length; ++y) {
998                 if (x != y) {
999                     Relation r = allRelationValues[y];
1000                     List newAttributes = new LinkedList(result.attributes);
1001                     newAttributes.removeAll(r.attributes);
1002                     newAttributes.addAll(r.attributes);
1003                     Relation new_r = solver.createRelation(result + "_j", newAttributes);
1004                     new_r.initialize();
1005                     Join join = new Join(new_r, r, result);
1006                     if (solver.TRACE) solver.out.println("Generated: " + join);
1007                     ir.add(join);
1008                     result = new_r;
1009                 }
1010                 if (!toProject[y].isEmpty()) {
1011                     List newAttributes = new LinkedList(result.attributes);
1012                     newAttributes.removeAll(toProject[y]);
1013                     Relation result2 = solver.createRelation(result + "_p2", newAttributes);
1014                     result2.initialize();
1015                     Project p = new Project(result2, result);
1016                     if (solver.TRACE) solver.out.println("Generated: " + p);
1017                     ir.add(p);
1018                     result = result2;
1019                 }
1020             }
1021             // Rename result to match head relation.
1022             Map renames = new LinearMap();
1023             List renamedAttributes = new LinkedList();
1024             for (int j = 0; j < bottom.numberOfVariables(); ++j) {
1025                 Variable v = bottom.getVariable(j);
1026                 if (unnecessaryVariables.contains(v)) continue;
1027                 Attribute a = bottom.relation.getAttribute(j);
1028                 Attribute a2 = (Attribute) varToAttrib.get(v);
1029                 //solver.out.println("Variable "+v+" has attribute "+a2);
1030                 Assert._assert(a2 != null);
1031                 if (!a2.equals(a)) {
1032                     renames.put(a2, a);
1033                 }
1034                 renamedAttributes.add(a);
1035             }
1036             if (!renames.isEmpty()) {
1037                 Relation result2 = solver.createRelation(result + "_r2", renamedAttributes);
1038                 result2.initialize();
1039                 Rename rename = new Rename(result2, result, renames);
1040                 if (solver.TRACE) solver.out.println("Generated: " + rename);
1041                 ir.add(rename);
1042                 result = result2;
1043             }
1044             // Restrict constants.
1045             for (int j = 0; j < bottom.numberOfVariables(); ++j) {
1046                 Variable v = bottom.getVariable(j);
1047                 if (v instanceof Constant) {
1048                     Attribute a = bottom.relation.getAttribute(j);
1049                     long value = ((Constant) v).getValue();
1050                     List a2 = new LinkedList(result.attributes);
1051                     a2.add(a);
1052                     Relation result2 = solver.createRelation(result.name+"_jc", a2);
1053                     result2.initialize();
1054                     JoinConstant jc = new JoinConstant(result2, result, a, value);
1055                     if (solver.TRACE) solver.out.println("Generated: " + jc);
1056                     ir.add(jc);
1057                     result = result2;
1058                 }
1059             }
1060             // Finally, union in the result.
1061             Union u = new Union(bottom.relation, bottom.relation, result);
1062             if (solver.TRACE) solver.out.println("Generated: " + u);
1063             ir.add(u);
1064         }
1065         if (bottom.relation.negated != null) {
1066             // Update negated.
1067             Invert i = new Invert(bottom.relation.negated, bottom.relation);
1068             if (solver.TRACE) solver.out.println("Generated: " + i);
1069             ir.add(i);
1070         }
1071         ir_incremental = ir;
1072         return ir;
1073     }
1074 
1075     /*
1076      * (non-Javadoc)
1077      * 
1078      * @see java.lang.Object#toString()
1079      */
1080     public String toString() {
1081         StringBuffer sb = new StringBuffer();
1082         sb.append(bottom);
1083         sb.append(" :- ");
1084         for (Iterator i = top.iterator(); i.hasNext();) {
1085             sb.append(i.next());
1086             if (i.hasNext()) sb.append(", ");
1087         }
1088         sb.append(".");
1089         return sb.toString();
1090     }
1091     
1092     /***
1093      * The hashCode for rules is deterministic.  (We use the unique id number.)
1094      * @see java.lang.Object#hashCode()
1095      */
1096     public int hashCode() {
1097         return id;
1098     }
1099 
1100     /***
1101      * Returns the variable with the given name, or null if there is none.
1102      * 
1103      * @param name  variable name
1104      * @return  variable
1105      */
1106     public Variable getVariable(String name) {
1107         for (Iterator i = necessaryVariables.iterator(); i.hasNext(); ) {
1108             Variable v = (Variable) i.next();
1109             if (name.equals(v.getName())) return v;
1110         }
1111         for (Iterator i = unnecessaryVariables.iterator(); i.hasNext(); ) {
1112             Variable v = (Variable) i.next();
1113             if (name.equals(v.getName())) return v;
1114         }
1115         return null;
1116     }
1117     
1118     public int numberOfVariables() {
1119         return necessaryVariables.size() + unnecessaryVariables.size();
1120     }
1121     
1122     public Set getNecessaryVariables() {
1123         return necessaryVariables;
1124     }
1125     
1126     public Set getUnnecessaryVariables() {
1127         return unnecessaryVariables;
1128     }
1129     
1130     public Set getVariables() {
1131         HashSet s = new HashSet();
1132         s.addAll(necessaryVariables);
1133         s.addAll(unnecessaryVariables);
1134         return s;
1135     }
1136     
1137     /***
1138      * @return  map from names to variables
1139      */
1140     public Map getVarNameMap() {
1141         HashMap nameToVar = new HashMap();
1142         for (Iterator i = necessaryVariables.iterator(); i.hasNext(); ) {
1143             Variable v = (Variable) i.next();
1144             nameToVar.put(v.getName(), v);
1145         }
1146         for (Iterator i = unnecessaryVariables.iterator(); i.hasNext(); ) {
1147             Variable v = (Variable) i.next();
1148             nameToVar.put(v.getName(), v);
1149         }
1150         return nameToVar;
1151     }
1152     
1153     /***
1154      * Returns the attribute associated with the given variable.
1155      * 
1156      * @param v  variable
1157      * @return  attribute
1158      */
1159     public Attribute getAttribute(Variable v) {
1160         Attribute a = bottom.getAttribute(v);
1161         if (a != null) return a;
1162         for (Iterator i = top.iterator(); i.hasNext(); ) {
1163             RuleTerm rt = (RuleTerm) i.next();
1164             a = rt.getAttribute(v);
1165             if (a != null) return a;
1166         }
1167         return null;
1168     }
1169     
1170     public static InferenceRule fromXMLElement(Element e, Solver s) {
1171         Map nameToVar = new HashMap();
1172         RuleTerm b = RuleTerm.fromXMLElement((Element) e.getContent(0), s, nameToVar);
1173         List t = new ArrayList(e.getContentSize()-1);
1174         for (Iterator i = e.getContent().subList(1, e.getContentSize()).iterator(); i.hasNext(); ) {
1175             Element e2 = (Element) i.next();
1176             t.add(RuleTerm.fromXMLElement(e2, s, nameToVar));
1177         }
1178         InferenceRule ir = s.createInferenceRule(t, b);
1179         Assert._assert(Integer.parseInt(e.getAttributeValue("id")) == ir.id);
1180         return ir;
1181     }
1182     
1183     public Element toXMLElement() {
1184         Element e = new Element("rule");
1185         e.setAttribute("id", Integer.toString(id));
1186         e.addContent(bottom.toXMLElement());
1187         for (Iterator i = top.iterator(); i.hasNext(); ) {
1188             RuleTerm rt = (RuleTerm) i.next();
1189             e.addContent(rt.toXMLElement());
1190         }
1191         return e;
1192     }
1193     
1194 }