1
2
3
4 package net.sf.bddbddb;
5
6 import java.util.ArrayList;
7 import java.util.Arrays;
8 import java.util.Collection;
9 import java.util.Collections;
10 import java.util.HashMap;
11 import java.util.HashSet;
12 import java.util.Iterator;
13 import java.util.LinkedHashSet;
14 import java.util.LinkedList;
15 import java.util.List;
16 import java.util.ListIterator;
17 import java.util.Map;
18 import java.util.Set;
19 import jwutil.collections.BinHeapPriorityQueue;
20 import jwutil.graphs.Navigator;
21 import jwutil.graphs.ReverseNavigator;
22 import jwutil.graphs.SCComponent;
23 import jwutil.graphs.Traversals;
24 import jwutil.util.Assert;
25
26 /***
27 * Implements stratification and decides iteration order.
28 *
29 * @author jwhaley
30 * @version $Id: Stratify.java 642 2006-06-08 02:35:35Z joewhaley $
31 */
32 public class Stratify {
33
34 public Solver solver;
35 public List strata;
36 public Map innerSccs;
37 Map nodes;
38 PDGRelationNode emptyRelationNode;
39 boolean NOISY;
40 boolean TRACE;
41
42 public Stratify(Solver solver) {
43 this.solver = solver;
44 this.NOISY = solver.NOISY;
45 this.TRACE = solver.TRACE;
46 this.nodes = new HashMap();
47 this.emptyRelationNode = getRelationNode(null);
48 }
49
50 static class PDGRelationNode {
51 Relation relation;
52 List
53 List
54
55 PDGRelationNode(Relation r) {
56 this.relation = r;
57 this.in = new LinkedList();
58 this.out = new LinkedList();
59 }
60
61 private static Set getRules(List list) {
62 Set result = new LinkedHashSet(list.size());
63 for (Iterator i = list.iterator(); i.hasNext(); ) {
64 PDGRuleNode e = (PDGRuleNode) i.next();
65 if (e.rule != null)
66 result.add(e.rule);
67 }
68 return result;
69 }
70
71 Set getInRules() {
72 return getRules(in);
73 }
74
75 Set getOutRules() {
76 return getRules(out);
77 }
78
79 void remove() {
80 for (Iterator i = in.iterator(); i.hasNext(); ) {
81 PDGRuleNode e = (PDGRuleNode) i.next();
82 e.to.remove(this);
83 i.remove();
84 }
85 for (Iterator i = out.iterator(); i.hasNext(); ) {
86 PDGRuleNode e = (PDGRuleNode) i.next();
87 e.from.remove(this);
88 i.remove();
89 }
90 }
91
92 public String toString() {
93 return relation == null ? "<null>" : relation.toString();
94 }
95
96 }
97
98 static class PDGRuleNode {
99 InferenceRule rule;
100 List
101 List
102 List
103
104 PDGRuleNode(InferenceRule rule, List from, List to) {
105 this.rule = rule;
106 this.from = from;
107 this.to = to;
108
109 for (Iterator i = from.iterator(); i.hasNext(); ) {
110 PDGRelationNode n = (PDGRelationNode) i.next();
111 n.out.add(this);
112 }
113 for (Iterator i = to.iterator(); i.hasNext(); ) {
114 PDGRelationNode n = (PDGRelationNode) i.next();
115 n.in.add(this);
116 }
117 if (false && rule != null) {
118 negated = new ArrayList(rule.top.size());
119 for (Iterator i = rule.top.iterator(); i.hasNext(); ) {
120 RuleTerm rt = (RuleTerm) i.next();
121 Boolean b;
122 if (rt.relation.name.startsWith("!"))
123 b = Boolean.TRUE;
124 else
125 b = Boolean.FALSE;
126 negated.add(b);
127 }
128 }
129 }
130
131 void remove() {
132 for (Iterator i = from.iterator(); i.hasNext(); ) {
133 PDGRelationNode n = (PDGRelationNode) i.next();
134 n.out.remove(this);
135 i.remove();
136 }
137 for (Iterator i = to.iterator(); i.hasNext(); ) {
138 PDGRelationNode n = (PDGRelationNode) i.next();
139 n.in.remove(this);
140 i.remove();
141 }
142 }
143
144 boolean isNegated(Relation n) {
145 if (rule == null) return false;
146 for (Iterator i = rule.top.iterator(); i.hasNext(); ) {
147 RuleTerm rt = (RuleTerm) i.next();
148 Relation r2 = rt.relation;
149 if (r2.name.startsWith("!")) {
150 if (r2.negated == n)
151 return true;
152 }
153 }
154 return false;
155 }
156
157 public String toString() {
158 return ""+rule;
159 }
160 }
161
162 PDGRelationNode getRelationNode(Relation r) {
163 if (r != null && r.name.startsWith("!")) {
164 Assert._assert(r.negated != null, r.name);
165 r = r.negated;
166 }
167 PDGRelationNode p = (PDGRelationNode) nodes.get(r);
168 if (p == null) {
169 nodes.put(r, p = new PDGRelationNode(r));
170 }
171 return p;
172 }
173
174 PDGRuleNode getRuleNode(InferenceRule rule) {
175 PDGRuleNode p = (PDGRuleNode) nodes.get(rule);
176 if (p == null) {
177 List from;
178 if (rule.top.isEmpty()) {
179 from = new ArrayList(1); from.add(emptyRelationNode);
180 } else {
181 from = new ArrayList(rule.top.size());
182 for (Iterator i = rule.top.iterator(); i.hasNext(); ) {
183 RuleTerm rt = (RuleTerm) i.next();
184 PDGRelationNode n = getRelationNode(rt.relation);
185 from.add(n);
186 }
187 }
188 Assert._assert(!rule.bottom.relation.name.startsWith("!"));
189 PDGRelationNode n = getRelationNode(rule.bottom.relation);
190 List to = new ArrayList(1); to.add(n);
191 if (rule.extraDefines != null) {
192 for (Iterator i = rule.extraDefines.iterator(); i.hasNext(); ) {
193 Relation r = (Relation) i.next();
194 PDGRelationNode node = getRelationNode(r);
195 to.add(node);
196 }
197 }
198 p = new PDGRuleNode(rule, from, to);
199 if (TRACE) {
200 solver.out.println("Added PDG edges from "+from+" to "+to);
201 }
202 nodes.put(rule, p);
203 }
204 return p;
205 }
206
207 static class PDGRelationNavigator implements Navigator {
208
209 static final PDGRelationNavigator INSTANCE = new PDGRelationNavigator();
210
211 private PDGRelationNavigator() {}
212
213 public Collection next(Object node) {
214 PDGRelationNode n = (PDGRelationNode) node;
215 List out = new ArrayList(n.out.size());
216 for (Iterator i = n.out.iterator(); i.hasNext(); ) {
217 PDGRuleNode e = (PDGRuleNode) i.next();
218 out.addAll(e.to);
219 }
220 return out;
221 }
222
223 public Collection prev(Object node) {
224 PDGRelationNode n = (PDGRelationNode) node;
225 List in = new ArrayList(n.in.size());
226 for (Iterator i = n.in.iterator(); i.hasNext(); ) {
227 PDGRuleNode e = (PDGRuleNode) i.next();
228 in.addAll(e.from);
229 }
230 return in;
231 }
232
233 }
234
235 static boolean containsAny(Collection c1, Collection c2) {
236 for (Iterator i = c2.iterator(); i.hasNext(); ) {
237 Object o = i.next();
238 if (c1.contains(o)) return true;
239 }
240 return false;
241 }
242
243 static class PDGEdgeNavigator implements Navigator {
244
245 static final PDGEdgeNavigator INSTANCE = new PDGEdgeNavigator();
246
247 Collection limitRelationNodes;
248 Collection cutRuleNodes;
249
250 private PDGEdgeNavigator() {}
251
252 PDGEdgeNavigator(Collection limit, Collection edges) {
253 limitRelationNodes = limit;
254 cutRuleNodes = edges;
255 }
256
257 public Collection next(Object node) {
258 if (node instanceof PDGRelationNode) {
259 PDGRelationNode n = (PDGRelationNode) node;
260 Assert._assert(limitRelationNodes == null || limitRelationNodes.contains(n));
261 if (limitRelationNodes == null) return n.out;
262 else {
263 List out = new ArrayList(n.out.size());
264 for (Iterator i = n.out.iterator(); i.hasNext(); ) {
265 PDGRuleNode e = (PDGRuleNode) i.next();
266 if (containsAny(e.to, limitRelationNodes))
267 out.add(e);
268 }
269 return out;
270 }
271 } else {
272 PDGRuleNode e = (PDGRuleNode) node;
273 if (cutRuleNodes != null && cutRuleNodes.contains(e))
274 return Collections.EMPTY_SET;
275 if (limitRelationNodes != null) {
276 ArrayList result = new ArrayList(e.to.size());
277 for (Iterator i = e.to.iterator(); i.hasNext(); ) {
278 PDGRelationNode n = (PDGRelationNode) i.next();
279 if (limitRelationNodes.contains(n))
280 result.add(n);
281 }
282 return result;
283 }
284 return e.to;
285 }
286 }
287
288 public Collection prev(Object node) {
289 if (node instanceof PDGRelationNode) {
290 PDGRelationNode n = (PDGRelationNode) node;
291 Assert._assert(limitRelationNodes == null || limitRelationNodes.contains(n));
292 if (limitRelationNodes == null && cutRuleNodes == null) return n.in;
293 else {
294 List in = new ArrayList(n.in.size());
295 for (Iterator i = n.in.iterator(); i.hasNext(); ) {
296 PDGRuleNode e = (PDGRuleNode) i.next();
297 if (cutRuleNodes.contains(e))
298 continue;
299 if (containsAny(e.from, limitRelationNodes))
300 in.add(e);
301 }
302 return in;
303 }
304 } else {
305 PDGRuleNode e = (PDGRuleNode) node;
306 if (limitRelationNodes != null) {
307 ArrayList result = new ArrayList(e.from.size());
308 for (Iterator i = e.from.iterator(); i.hasNext(); ) {
309 PDGRelationNode n = (PDGRelationNode) i.next();
310 if (limitRelationNodes.contains(n))
311 result.add(n);
312 }
313 return result;
314 }
315 return e.from;
316 }
317 }
318
319 }
320
321 public void stratify() {
322 Iterator i;
323 Set inputs = new HashSet();
324 inputs.addAll(solver.relationsToLoad);
325 inputs.addAll(solver.relationsToLoadTuples);
326 for (i = solver.getComparisonRelations().iterator(); i.hasNext(); ) {
327 Relation r = (Relation) i.next();
328 inputs.add(r);
329 if (r.getNegated() != null) inputs.add(r.getNegated());
330 Assert._assert(!r.name.startsWith("!"));
331 }
332 Set outputs = new HashSet();
333 outputs.addAll(solver.relationsToDump);
334 outputs.addAll(solver.relationsToDumpTuples);
335 outputs.addAll(solver.relationsToPrintSize);
336 outputs.addAll(solver.relationsToPrintTuples);
337 i = solver.dotGraphsToDump.iterator();
338 while (i.hasNext()) {
339 outputs.addAll(((Dot) i.next()).getUsedRelations());
340 }
341 stratify(solver.rules, inputs, outputs);
342 }
343
344 /***
345 * Stratify the given list of rules with respect to the given inputs and outputs.
346 *
347 * @param rules rules to stratify
348 * @param inputs input relations
349 * @param outputs output relations
350 */
351 public void stratify(List rules, Set inputs, Set outputs) {
352
353 nodes.clear();
354
355
356 for (Iterator i = inputs.iterator(); i.hasNext(); ) {
357 Relation r = (Relation) i.next();
358 PDGRelationNode n = getRelationNode(r);
359 List from = new ArrayList(1); from.add(emptyRelationNode);
360 List to = new ArrayList(1); to.add(n);
361 PDGRuleNode edge = new PDGRuleNode(null, from, to);
362 if (TRACE) {
363 solver.out.println("Added PDG edges from "+from+" to "+to);
364 }
365 }
366
367 Collection outputNodes = new ArrayList(outputs.size());
368 for (Iterator i = outputs.iterator(); i.hasNext(); ) {
369 Relation r = (Relation) i.next();
370 PDGRelationNode n = getRelationNode(r);
371 outputNodes.add(n);
372 }
373
374
375 for (Iterator i = rules.iterator(); i.hasNext(); ) {
376 InferenceRule r = (InferenceRule) i.next();
377 getRuleNode(r);
378 }
379
380
381
382 List forwardRpo = Traversals.reversePostOrder(PDGRelationNavigator.INSTANCE, emptyRelationNode);
383 Set reachable = new HashSet(forwardRpo);
384
385
386
387
388 List backwardRpo = Traversals.reversePostOrder(new ReverseNavigator(PDGRelationNavigator.INSTANCE), outputNodes);
389 Set unnecessary = new HashSet(solver.nameToRelation.values());
390 for (Iterator i = backwardRpo.iterator(); i.hasNext(); ) {
391 PDGRelationNode o = (PDGRelationNode) i.next();
392 if (!reachable.remove(o)) {
393 solver.out.println("ERROR: The following relation is necessary, but is not present in any strata:");
394 solver.out.println(" " + o);
395 solver.out.println("You may be using this relation without defining it.");
396 throw new IllegalArgumentException();
397 }
398 if (o.relation == null) continue;
399
400 boolean b = unnecessary.remove(o.relation);
401 Assert._assert(b);
402 if (o.relation.negated != null)
403 unnecessary.remove(o.relation.negated);
404 }
405
406
407 if (!unnecessary.isEmpty()) {
408 if (NOISY) {
409 solver.out.println("Note: the following relations are unused:");
410 solver.out.println(" " + unnecessary);
411 }
412 Set unusedRules = new HashSet();
413 for (Iterator i = unnecessary.iterator(); i.hasNext(); ) {
414 Relation r = (Relation) i.next();
415 PDGRelationNode n = getRelationNode(r);
416 unusedRules.addAll(n.getInRules());
417 unusedRules.addAll(n.getOutRules());
418 n.remove();
419 forwardRpo.remove(n);
420 }
421 if (NOISY) solver.out.println("Note: the following rules are unused:");
422 for (Iterator i = unusedRules.iterator(); i.hasNext(); ) {
423 InferenceRule ir = (InferenceRule) i.next();
424 if (NOISY) solver.out.println(" " + ir);
425 getRuleNode(ir).remove();
426 }
427 }
428
429
430 SCComponent root = SCComponent.buildSCC(emptyRelationNode, PDGEdgeNavigator.INSTANCE);
431
432
433 List sortedSccs = Traversals.reversePostOrder(SCComponent.SCC_NAVIGATOR, root);
434
435
436 for (Iterator i = sortedSccs.iterator(); i.hasNext(); ) {
437 SCComponent o = (SCComponent) i.next();
438 if (o.isLoop())
439 checkForNegatedEdges(Arrays.asList(o.nodes()));
440 }
441
442
443 strata = new LinkedList();
444 Set visitedSccs = new HashSet();
445 while (!sortedSccs.isEmpty()) {
446 List stratum = discoverStratum(sortedSccs, visitedSccs);
447 Assert._assert(!stratum.isEmpty());
448 strata.add(stratum);
449 visitedSccs.addAll(stratum);
450 }
451 if (NOISY) solver.out.println("Finished discovery of "+visitedSccs.size()+" SCCs in "+strata.size()+" strata");
452
453
454 innerSccs = new HashMap();
455 for (Iterator i = strata.iterator(); i.hasNext(); ) {
456 Collection stratum = (Collection) i.next();
457 for (Iterator j = stratum.iterator(); j.hasNext(); ) {
458 SCComponent scc = (SCComponent) j.next();
459 if (scc.isLoop()) {
460 computeLoopNesting(scc, new HashSet());
461 }
462 }
463 }
464 }
465
466 void checkForNegatedEdges(Collection c) {
467 for (Iterator i = c.iterator(); i.hasNext(); ) {
468 Object o = i.next();
469 if (o instanceof PDGRuleNode) {
470 PDGRuleNode n = (PDGRuleNode) o;
471 for (Iterator j = n.from.iterator(); j.hasNext(); ) {
472 PDGRelationNode n2 = (PDGRelationNode) j.next();
473 if (c.contains(n2) && n.isNegated(n2.relation)) {
474 solver.out.println("ERROR: Datalog is not stratifiable due to this rule:");
475 solver.out.println(" "+n.rule);
476 throw new IllegalArgumentException();
477 }
478 }
479 }
480 }
481 }
482
483 List discoverStratum(List sortedSccs, Set visitedSccs) {
484 if (NOISY) solver.out.println("Discovering stratum, "+visitedSccs.size()+" SCCs visited so far");
485
486 List stratum = new LinkedList();
487 Set stratumSet = new HashSet();
488 outer:
489 for (ListIterator i = sortedSccs.listIterator(); i.hasNext(); ) {
490 SCComponent scc = (SCComponent) i.next();
491 Assert._assert(!visitedSccs.contains(scc));
492 for (int j = 0; j < scc.prevLength(); ++j) {
493 SCComponent pscc = scc.prev(j);
494 if (!visitedSccs.contains(pscc)) {
495 if (!stratumSet.contains(pscc)) {
496 if (TRACE) solver.out.println("Predecessor "+pscc+" of "+scc+" not done yet.");
497 continue outer;
498 }
499 if (checkForNegatedEdge(pscc, scc)) {
500 if (TRACE) solver.out.println("Negated edge: "+pscc+" to "+scc);
501 continue outer;
502 }
503 } else {
504 if (TRACE) solver.out.println("Predecessor "+pscc+" of "+scc+" already visited.");
505 }
506 }
507 if (TRACE) solver.out.println("Adding to stratum: "+scc);
508 stratum.add(scc);
509 boolean b = stratumSet.add(scc);
510 Assert._assert(b);
511 i.remove();
512 }
513 return stratum;
514 }
515
516 boolean checkForNegatedEdge(SCComponent from, SCComponent to) {
517 if (to.size() == 1) {
518 Object o = to.nodes()[0];
519 if (o instanceof PDGRuleNode) {
520 PDGRuleNode n = (PDGRuleNode) o;
521 for (Iterator j = n.from.iterator(); j.hasNext(); ) {
522 PDGRelationNode n2 = (PDGRelationNode) j.next();
523 if (from.contains(n2) && n.isNegated(n2.relation)) {
524 return true;
525 }
526 }
527 }
528 }
529 return false;
530 }
531
532 void computeLoopNesting(SCComponent scc, Set cutEdges) {
533 if (TRACE) solver.out.println("Computing loop nesting for "+scc);
534
535 scc.fillEntriesAndExits(PDGEdgeNavigator.INSTANCE);
536
537
538 PDGEdgeNavigator nav = new PDGEdgeNavigator(scc.nodeSet(), cutEdges);
539 PDGRuleNode backEdge = chooseABackedge(scc, nav);
540 if (TRACE) solver.out.println("Cutting backedge "+backEdge);
541 boolean b = nav.cutRuleNodes.add(backEdge);
542 Assert._assert(b);
543
544
545
546 Collection entries = Arrays.asList(scc.entries());
547
548 Assert._assert(!entries.isEmpty());
549 Collection
550 List inner = Traversals.reversePostOrder(SCComponent.SCC_NAVIGATOR, sccs);
551 if (TRACE) solver.out.println("Inner sccs for SCC"+scc.getId()+":");
552 innerSccs.put(scc, inner);
553 for (Iterator i = inner.iterator(); i.hasNext(); ) {
554 SCComponent scc2 = (SCComponent) i.next();
555 if (TRACE) solver.out.println(" "+scc2);
556 if (scc2.isLoop()) {
557 computeLoopNesting(scc2, (Set) nav.cutRuleNodes);
558 }
559 }
560 }
561
562 PDGRuleNode chooseABackedge(SCComponent scc, PDGEdgeNavigator nav) {
563 Object[] entries = scc.entries();
564 Object entry = null;
565 for (int i = 0; i < entries.length; ++i) {
566 entry = entries[i];
567 if (!nav.cutRuleNodes.contains(entry)) break;
568 }
569 if (entry == null) {
570 entry = scc.nodes()[0];
571 }
572 if (TRACE) solver.out.println("Starting from entry point "+entry);
573 Assert._assert(!nav.cutRuleNodes.contains(entry));
574
575 Set visited = new HashSet();
576 BinHeapPriorityQueue queue = new BinHeapPriorityQueue();
577 int priority = getPriority(entry);
578 queue.insert(entry, priority);
579 visited.add(entry);
580 Object last = null; int min = Integer.MAX_VALUE;
581 while (!queue.isEmpty()) {
582 Object o = (Object) queue.peekMax();
583 priority = queue.getPriority(o);
584 queue.deleteMax();
585 boolean any = false;
586 for (Iterator i = nav.next(o).iterator(); i.hasNext(); ) {
587 Object q = (Object) i.next();
588 if (!scc.contains(q)) continue;
589 if (visited.add(q)) {
590 queue.insert(q, priority+getPriority(q));
591 any = true;
592 }
593 }
594 if (!any && priority <= min && !nav.cutRuleNodes.contains(last)) {
595 last = o; min = priority;
596 }
597 }
598 if (TRACE) solver.out.println("Last node: "+last);
599 Assert._assert(!nav.cutRuleNodes.contains(last));
600 Object last_next = null;
601 for (Iterator i = nav.next(last).iterator(); i.hasNext(); ) {
602 Object o = i.next();
603 if (!nav.cutRuleNodes.contains(o)) {
604 last_next = o;
605 break;
606 }
607 }
608 if (TRACE) solver.out.println("Successor of last node: "+last_next);
609 Assert._assert(!nav.cutRuleNodes.contains(last_next));
610 if (last instanceof PDGRuleNode) {
611 return (PDGRuleNode) last;
612 } else {
613 return (PDGRuleNode) last_next;
614 }
615 }
616
617 public static int getPriority(Object o) {
618 if (o instanceof PDGRuleNode) {
619 return ((PDGRuleNode) o).rule.priority-2;
620 } else {
621 return ((PDGRelationNode) o).relation.priority-2;
622 }
623 }
624
625 }