1
2
3 package net.sf.bddbddb;
4
5 import java.util.Collection;
6 import java.util.Comparator;
7 import java.util.HashMap;
8 import java.util.Iterator;
9 import java.util.LinkedList;
10 import java.util.List;
11 import java.util.Map;
12 import java.io.FileWriter;
13 import java.io.IOException;
14 import java.io.Writer;
15 import jwutil.collections.LinearMap;
16 import jwutil.io.SystemProperties;
17 import jwutil.util.Assert;
18 import net.sf.javabdd.BDD;
19 import net.sf.javabdd.BDDDomain;
20 import net.sf.javabdd.BDDFactory;
21 import net.sf.javabdd.BDDPairing;
22 import net.sf.javabdd.BDDVarSet;
23
24 /***
25 * An implementation of InferenceRule that uses BDDs.
26 *
27 * @author jwhaley
28 * @version $Id: BDDInferenceRule.java 650 2006-11-29 08:08:45Z joewhaley $
29 */
30 public class BDDInferenceRule extends InferenceRule {
31 /***
32 * @see net.sf.bddbddb.InferenceRule#solver
33 */
34 protected BDDSolver solver;
35
36 /***
37 * Values for subgoals, used for incrementalization.
38 */
39 protected BDD[] oldRelationValues;
40
41 /***
42 * Map from variables to their BDD domains.
43 */
44 protected Map variableToBDDDomain;
45
46 /***
47 * Set of renames that must occur after each of the subgoals.
48 */
49 BDDPairing[] renames;
50
51 /***
52 * Rename operation that must occur to match with the head relation.
53 */
54 BDDPairing bottomRename;
55
56 /***
57 * BDD variables that can be quantified away after each step.
58 */
59 BDDVarSet[] canQuantifyAfter;
60
61 /***
62 * Collection of variables that are still active after each step.
63 */
64 Collection[] variableSet;
65
66 /***
67 * Number of times update() has been called on this rule.
68 */
69 public int updateCount;
70
71 /***
72 * Total time (in ms) spent updating this rule.
73 */
74 long totalTime;
75 int longestIteration = 0;
76 long longestTime = 0;
77
78
79 /***
80 * Whether we should attempt to find the best order for this rule.
81 */
82 boolean find_best_order = !SystemProperties.getProperty("findbestorder", "no").equals("no");
83
84 long FBO_CUTOFF = Long.parseLong(SystemProperties.getProperty("fbocutoff", "90"));
85
86 long DUMP_CUTOFF = Long.parseLong(SystemProperties.getProperty("dumpcutoff", "5000"));
87
88 /***
89 * Construct a new BDDInferenceRule.
90 * Only to be called internally.
91 *
92 * @param solver
93 * @param top
94 * @param bottom
95 */
96 BDDInferenceRule(BDDSolver solver, List
97 super(solver, top, bottom);
98 this.solver = solver;
99 updateCount = 0;
100
101 }
102
103
104
105
106
107
108 public void copyOptions(InferenceRule r) {
109 super.copyOptions(r);
110 if (r instanceof BDDInferenceRule) {
111 BDDInferenceRule that = (BDDInferenceRule) r;
112 this.find_best_order = that.find_best_order;
113 }
114 }
115
116
117
118
119
120
121 void initialize() {
122 if (isInitialized) return;
123 super.initialize();
124 if (TRACE) solver.out.println("Initializing BDDInferenceRule " + this);
125 updateCount = 0;
126 this.oldRelationValues = null;
127 this.variableToBDDDomain = new HashMap();
128 for (int i = 0; i < top.size(); ++i) {
129 RuleTerm rt = (RuleTerm) top.get(i);
130 BDDRelation r = (BDDRelation) rt.relation;
131 for (int j = 0; j < rt.variables.size(); ++j) {
132 Variable v = (Variable) rt.variables.get(j);
133
134 BDDDomain d = (BDDDomain) r.domains.get(j);
135 Assert._assert(d != null);
136
137 BDDDomain d2 = (BDDDomain) variableToBDDDomain.get(v);
138 if (d2 == null) {
139 if (!variableToBDDDomain.containsValue(d)) {
140 d2 = d;
141 } else {
142
143 Attribute a = (Attribute) r.attributes.get(j);
144 Domain fd = a.attributeDomain;
145 Collection existingBDDDomains = solver.getBDDDomains(fd);
146 for (Iterator k = existingBDDDomains.iterator(); k.hasNext();) {
147 BDDDomain d3 = (BDDDomain) k.next();
148 if (!variableToBDDDomain.containsValue(d3)) {
149 d2 = d3;
150 break;
151 }
152 }
153 if (d2 == null) {
154 d2 = solver.allocateBDDDomain(fd);
155 }
156 }
157 if (TRACE) solver.out.println("Variable " + v + " allocated to BDD domain " + d2);
158 variableToBDDDomain.put(v, d2);
159 } else {
160
161
162 }
163 }
164 }
165 if (this.renames == null) {
166 renames = new BDDPairing[top.size()];
167 }
168 for (int i = 0; i < top.size(); ++i) {
169 RuleTerm rt = (RuleTerm) top.get(i);
170
171
172 renames[i] = calculateRenames(rt, true);
173 }
174
175
176 bottomRename = calculateRenames(bottom, false);
177 initializeQuantifySet();
178 if (variableSet == null) {
179 variableSet = new Collection[top.size()];
180 }
181 Collection currentVariableSet = new LinkedList();
182 for (int i = 0; i < top.size(); ++i) {
183 RuleTerm rt = (RuleTerm) top.get(i);
184 currentVariableSet.addAll(rt.variables);
185 if (TRACE) solver.out.println("Calculating quantifiable variables for "+rt);
186 outer : for (Iterator k = rt.variables.iterator(); k.hasNext();) {
187 Variable v = (Variable) k.next();
188 if (bottom.variables.contains(v)) continue;
189 for (int j = i + 1; j < top.size(); ++j) {
190 RuleTerm rt2 = (RuleTerm) top.get(j);
191 if (rt2.variables.contains(v)) continue outer;
192 }
193 if (TRACE) solver.out.println("Can quantify "+v);
194 currentVariableSet.remove(v);
195 }
196 variableSet[i] = currentVariableSet;
197 if (TRACE) solver.out.println("Variable set["+i+"]="+variableSet[i]);
198 currentVariableSet = new LinkedList(currentVariableSet);
199 }
200 isInitialized = true;
201 }
202
203 /***
204 * Initialize the oldRelationValues to be the zero BDD.
205 */
206 private void initializeOldRelationValues() {
207 this.oldRelationValues = new BDD[top.size()];
208 for (int i = 0; i < oldRelationValues.length; ++i) {
209 oldRelationValues[i] = solver.bdd.zero();
210 }
211 }
212
213 void initializeQuantifySet() {
214 if (canQuantifyAfter == null) {
215 canQuantifyAfter = new BDDVarSet[top.size()];
216 }
217 for (int i = 0; i < top.size(); ++i) {
218 RuleTerm rt = (RuleTerm) top.get(i);
219 if (canQuantifyAfter[i] != null) canQuantifyAfter[i].free();
220 canQuantifyAfter[i] = solver.bdd.emptySet();
221 outer : for (Iterator k = rt.variables.iterator(); k.hasNext();) {
222 Variable v = (Variable) k.next();
223 if (bottom.variables.contains(v)) continue;
224 for (int j = i + 1; j < top.size(); ++j) {
225 RuleTerm rt2 = (RuleTerm) top.get(j);
226 if (rt2.variables.contains(v)) continue outer;
227 }
228 BDDDomain d2 = (BDDDomain) variableToBDDDomain.get(v);
229 canQuantifyAfter[i].unionWith(d2.set());
230 }
231 }
232 }
233
234 /***
235 * Calculate the rename operations that are needed for the given term.
236 * The direction flag determines the desired direction of the renames.
237 * If direction is true, we rename from the BDDDomain specified by the
238 * relation to the BDDDomain used by the rule for that variable.
239 * If direction is false, we rename from the BDDDomain used by the rule
240 * to the BDDDomain used by the relation.
241 *
242 * @param rt term to calculate renames for
243 * @param direction direction of desired renames
244 * @return BDDPairing that contains the renames
245 */
246 private BDDPairing calculateRenames(RuleTerm rt, boolean direction) {
247 BDDRelation r = (BDDRelation) rt.relation;
248 if (TRACE) solver.out.println("Calculating renames for " + r);
249 Map pairing = null;
250 for (int j = 0; j < rt.variables.size(); ++j) {
251 Variable v = (Variable) rt.variables.get(j);
252 if (unnecessaryVariables.contains(v)) continue;
253 BDDDomain d = (BDDDomain) r.domains.get(j);
254 BDDDomain d2 = (BDDDomain) variableToBDDDomain.get(v);
255 Assert._assert(d2 != null);
256 if (d != d2) {
257 if (!direction) {
258 BDDDomain d3 = d2;
259 d2 = d;
260 d = d3;
261 }
262 if (TRACE) solver.out.println(rt + " variable " + v + ": replacing " + d + " -> " + d2);
263 if (pairing == null) pairing = new LinearMap(solver.bdd.numberOfDomains());
264 Object foo = pairing.put(d, d2);
265 Assert._assert(foo == null);
266 }
267 }
268 return pairing != null ? solver.getPairing(pairing) : null;
269 }
270
271 void doPreUpdate(BDD oldValue) {
272 if (preCode != null) {
273 for (Iterator i = preCode.iterator(); i.hasNext(); ) {
274 CodeFragment f = (CodeFragment) i.next();
275 f.invoke(this, oldValue);
276 }
277 }
278 }
279
280 void doPostUpdate(BDD oldValue) {
281 if (postCode != null) {
282 for (Iterator i = postCode.iterator(); i.hasNext(); ) {
283 CodeFragment f = (CodeFragment) i.next();
284 f.invoke(this, oldValue);
285 }
286 }
287 }
288
289
290
291
292
293
294 public boolean update() {
295 doPreUpdate(((BDDRelation) bottom.relation).relation);
296 ++updateCount;
297 if (incrementalize) {
298 if (oldRelationValues != null) return updateIncremental();
299 }
300
301 if (solver.NOISY) solver.out.println("Applying inference rule:\n " + this + " (" + updateCount + ")");
302 long time = 0L;
303 long ttime = 0L;
304 if (solver.REPORT_STATS || TRACE) time = System.currentTimeMillis();
305 BDD[] relationValues = new BDD[top.size()];
306
307
308 if (!quantifyAndRestrict(relationValues)) {
309 if (solver.REPORT_STATS) totalTime += System.currentTimeMillis() - time;
310 if (TRACE) solver.out.println("Time spent: " + (System.currentTimeMillis() - time));
311 doPostUpdate(null);
312 return false;
313 }
314
315
316 if (!handleUniversalQuantification(relationValues)) {
317 if (solver.REPORT_STATS) totalTime += System.currentTimeMillis() - time;
318 if (TRACE) solver.out.println("Time spent: " + (System.currentTimeMillis() - time));
319 doPostUpdate(null);
320 return false;
321 }
322
323
324
325
326 if (incrementalize && cache_before_rename) {
327 if (TRACE) {
328 solver.out.print("Caching values of input relations");
329 ttime = System.currentTimeMillis();
330 }
331 if (oldRelationValues == null) initializeOldRelationValues();
332 for (int i = 0; i < relationValues.length; ++i) {
333 oldRelationValues[i].orWith(relationValues[i].id());
334 }
335 if (TRACE) solver.out.println(" (" + (System.currentTimeMillis() - ttime) + " ms)");
336 }
337
338
339 for (int i = 0; i < top.size(); ++i) {
340 RuleTerm rt = (RuleTerm) top.get(i);
341 BDDRelation r = (BDDRelation) rt.relation;
342 if (TRACE) solver.out.println("Relation " + r + " " + relationValues[i].nodeCount() + " nodes, domains " + domainsOf(relationValues[i]));
343 if (TRACE_FULL) solver.out.println(" current value: " + relationValues[i].toStringWithDomains());
344 BDDPairing pairing = renames[i];
345 if (pairing != null) {
346 if (TRACE) {
347 solver.out.print("Relation " + r + " domains " + domainsOf(relationValues[i]) + " -> ");
348 ttime = System.currentTimeMillis();
349 }
350 relationValues[i].replaceWith(pairing);
351 if (TRACE) {
352 solver.out.print(domainsOf(relationValues[i]));
353 solver.out.println(" (" + (System.currentTimeMillis() - ttime) + " ms)");
354 }
355 }
356 }
357 BDDRelation r = (BDDRelation) bottom.relation;
358 if (TRACE_FULL) solver.out.println("Current value of relation " + bottom + ": " + r.relation.toStringWithDomains());
359
360
361 if (incrementalize && !cache_before_rename) {
362 if (TRACE) {
363 solver.out.print("Caching values of input relations");
364 ttime = System.currentTimeMillis();
365 }
366 if (oldRelationValues == null) initializeOldRelationValues();
367 for (int i = 0; i < relationValues.length; ++i) {
368 oldRelationValues[i].orWith(relationValues[i].id());
369 }
370 if (TRACE) solver.out.println(" (" + (System.currentTimeMillis() - ttime) + " ms)");
371 }
372
373 BDD result = evalRelations(solver.bdd, relationValues, canQuantifyAfter, time);
374 long thisTime = System.currentTimeMillis() - time;
375 if (result == null) {
376 doPostUpdate(null);
377 return false;
378 }
379 if (TRACE_FULL) solver.out.println(" = " + result.toStringWithDomains());
380
381 else if (TRACE) solver.out.println(" = " + result.nodeCount());
382 if (single) {
383
384 result = limitToSingle(result);
385 if (TRACE) solver.out.println("Limited to single satisfying tuple: " + result.nodeCount());
386 }
387 if (bottomRename != null) {
388 if (TRACE) {
389 solver.out.print("Result domains " + domainsOf(result) + " -> ");
390 ttime = System.currentTimeMillis();
391 }
392 result.replaceWith(bottomRename);
393 if (TRACE) {
394 solver.out.print(domainsOf(result));
395 solver.out.println(" (" + (System.currentTimeMillis() - ttime) + " ms)");
396 }
397 }
398 for (int i = 0; i < bottom.variables.size(); ++i) {
399 Variable v = (Variable) bottom.variables.get(i);
400 if (v instanceof Constant) {
401 Constant c = (Constant) v;
402 BDDDomain d = (BDDDomain) r.domains.get(i);
403 if (TRACE) {
404 solver.out.print("Restricting result domain " + d + " to constant " + c);
405 ttime = System.currentTimeMillis();
406 }
407 result.andWith(d.ithVar(c.value));
408 if (TRACE) {
409 solver.out.println(" (" + (System.currentTimeMillis() - ttime) + " ms)");
410 }
411 }
412 }
413 BDD oldRelation = r.relation.id();
414 if (TRACE_FULL) solver.out.println("Adding to " + bottom + ": " + result.toStringWithDomains());
415 if (TRACE) {
416 solver.out.print("Result: " + r.relation.nodeCount() + " nodes -> ");
417 ttime = System.currentTimeMillis();
418 }
419 r.relation.orWith(result);
420 if (TRACE) {
421 solver.out.print(r.relation.nodeCount() + " nodes, ");
422 solver.out.print(r.dsize() + " elements.");
423 solver.out.println(" (" + (System.currentTimeMillis() - ttime) + " ms)");
424 }
425 if (TRACE_FULL) solver.out.println("Relation " + r + " is now: " + r.relation.toStringWithDomains());
426 boolean changed = !oldRelation.equals(r.relation);
427 if (TRACE) solver.out.println("Relation " + r + " changed: " + changed);
428 if (solver.REPORT_STATS) totalTime += System.currentTimeMillis() - time;
429 if (TRACE) solver.out.println("Time spent: " + (System.currentTimeMillis() - time));
430 r.updateNegated();
431 r.doUpdate(oldRelation);
432 if (r.negated != null) {
433 BDD old_neg = oldRelation.not();
434 ((BDDRelation)r.negated).doUpdate(old_neg);
435 old_neg.free();
436 }
437 doPostUpdate(oldRelation);
438 oldRelation.free();
439 return changed;
440 }
441
442 public BDD evalRelations(BDDFactory bdd, BDD[] relationValues, BDDVarSet[] canQuantifyAfter, long time) {
443
444 long ttime = 0;
445 BDD result = bdd.universe();
446 for (int j = 0; j < relationValues.length; ++j) {
447 RuleTerm rt = (RuleTerm) top.get(j);
448 BDDVarSet canNowQuantify = canQuantifyAfter[j];
449 if (TRACE) solver.out.print(" x " + rt.relation);
450 BDD b = relationValues[j];
451 if (TRACE) {
452 solver.out.print(" (relprod " + b.nodeCount());
453 solver.out.print(" ("+domainsOf(b)+")/");
454 solver.out.print("("+domainsOf(canNowQuantify)+")");
455 }
456 if (TRACE || find_best_order || DUMP_CUTOFF > 0) ttime = System.currentTimeMillis();
457 BDD topBdd = result.relprod(b, canNowQuantify);
458 if (TRACE || find_best_order || DUMP_CUTOFF > 0) ttime = System.currentTimeMillis() - ttime;
459 if (DUMP_CUTOFF > 0 && ttime >= DUMP_CUTOFF &&
460 SystemProperties.getPropertyFromFile("dumpslow") != null) {
461 long ftime = System.currentTimeMillis();
462
463 try {
464 String baseName = solver.getBaseName()+"rule"+id+"_subgoal"+j+"_update"+updateCount;
465 Writer w = new FileWriter(baseName+".info");
466 w.write("Rule: "+this+"\n");
467 w.write("Time: "+ttime+" ms\n");
468 w.close();
469 BDDRelation.save(solver, baseName+"_op1.bdd", result);
470 BDDRelation.save(solver, baseName+"_op2.bdd", b);
471 BDDRelation.save(solver, baseName+"_op3.bdd", canNowQuantify.toBDD());
472 } catch (IOException x) {
473 System.err.println("Error dumping BDD: "+x);
474 }
475 ftime = System.currentTimeMillis() - ftime;
476 this.totalTime -= ftime;
477 }
478 if (find_best_order && !result.isOne() && ttime >= FBO_CUTOFF) {
479 long ftime = System.currentTimeMillis();
480 FindBestDomainOrder.findBestDomainOrder(solver,this, j,solver.bdd, result, b, canNowQuantify,
481 (RuleTerm) top.get(j-1), rt,
482 variableSet[j], rt.variables);
483
484 ftime = System.currentTimeMillis() - ftime;
485 this.totalTime -= ftime;
486 }
487 b.free();
488 if (TRACE) {
489 solver.out.print("=" + topBdd.nodeCount());
490 solver.out.print(" (" + domainsOf(topBdd) + ")");
491 solver.out.print(") (" + ttime + " ms)");
492 }
493 result.free();
494 result = topBdd;
495 if (result.isZero()) {
496 if (TRACE) solver.out.println(" Became empty, stopping.");
497 for (++j; j < relationValues.length; ++j) {
498 relationValues[j].free();
499 }
500 if (solver.REPORT_STATS) totalTime += System.currentTimeMillis() - time;
501 if (TRACE) solver.out.println("Time spent: " + (System.currentTimeMillis() - time));
502 return null;
503 }
504
505 }
506 return result;
507 }
508
509 private boolean handleUniversalQuantification(BDD[] relationValues) {
510 if (TRACE) solver.out.println("Handling universal quantification...");
511 long ttime = 0L;
512 for (int i = 0; i < top.size(); ++i) {
513 RuleTerm rt = (RuleTerm) top.get(i);
514 BDDRelation r = (BDDRelation) rt.relation;
515
516 for (int j = 0; j < rt.variables.size(); ++j) {
517 Variable v = (Variable) rt.variables.get(j);
518 BDDDomain d = (BDDDomain) r.domains.get(j);
519 if (v instanceof Universe) {
520 if (TRACE) {
521 solver.out.print("Universe: for all " + d);
522 ttime = System.currentTimeMillis();
523 }
524 BDDVarSet dset = d.set();
525 BDD q = relationValues[i].forAll(dset);
526 dset.free();
527 if (TRACE) solver.out.println(" (" + (System.currentTimeMillis() - ttime) + " ms)");
528 relationValues[i].free();
529 relationValues[i] = q;
530 continue;
531 }
532 }
533 if (relationValues[i].isZero()) {
534 if (TRACE) solver.out.println("Relation " + r + " is now empty! Stopping early.");
535 for (int j = 0; j <= i; ++j) {
536 relationValues[j].free();
537 }
538 return false;
539 }
540 }
541 return true;
542 }
543
544 private boolean quantifyAndRestrict(BDD[] relationValues) {
545 long ttime = 0L;
546 if (TRACE) solver.out.println("Quantifying out unnecessary domains and restricting constants...");
547 if (TRACE) solver.out.println("Variables: necessary=" + necessaryVariables + " unnecessary=" + unnecessaryVariables);
548 for (int i = 0; i < top.size(); ++i) {
549 RuleTerm rt = (RuleTerm) top.get(i);
550 BDDRelation r = (BDDRelation) rt.relation;
551 relationValues[i] = r.relation.id();
552 for (int j = 0; j < rt.variables.size(); ++j) {
553 Variable v = (Variable) rt.variables.get(j);
554 BDDDomain d = (BDDDomain) r.domains.get(j);
555 if (v instanceof Constant) {
556 if (TRACE) {
557 solver.out.print("Constant: restricting " + r + " " + d + " = " + v);
558 ttime = System.currentTimeMillis();
559 }
560 relationValues[i].restrictWith(d.ithVar(((Constant) v).value));
561 if (TRACE) {
562 solver.out.print(" (" + (System.currentTimeMillis() - ttime) + " ms)");
563 solver.out.println(" (" + relationValues[i].nodeCount() + " nodes)");
564 }
565 continue;
566 }
567 if (v instanceof Universe) {
568
569 continue;
570 }
571 if (unnecessaryVariables.contains(v)) {
572 if (TRACE) {
573 solver.out.print(v + " is unnecessary, quantifying out " + d);
574 ttime = System.currentTimeMillis();
575 }
576 BDDVarSet dset = d.set();
577 BDD q = relationValues[i].exist(dset);
578 dset.free();
579 if (TRACE) {
580 solver.out.print(" (" + (System.currentTimeMillis() - ttime) + " ms)");
581 solver.out.println(" (" + q.nodeCount() + " nodes)");
582 }
583 relationValues[i].free();
584 relationValues[i] = q;
585 }
586 }
587 if (relationValues[i].isZero()) {
588 if (TRACE) solver.out.println("Relation " + r + " is now empty! Stopping early.");
589 for (int j = 0; j <= i; ++j)
590 relationValues[j].free();
591 return false;
592 }
593 }
594 return true;
595 }
596
597 /***
598 * Incremental version of update().
599 *
600 * @return if the head relation changed
601 */
602 private boolean updateIncremental() {
603 if (solver.NOISY) solver.out.println("Applying inference rule:\n " + this + " (inc) (" + updateCount + ")");
604 long time = 0L;
605 long ttime = 0L;
606 if (solver.REPORT_STATS || TRACE) time = System.currentTimeMillis();
607 BDD[] allRelationValues = new BDD[top.size()];
608 BDD[] newRelationValues = new BDD[top.size()];
609
610
611 if (!quantifyAndRestrict(allRelationValues)) {
612 if (solver.REPORT_STATS) totalTime += System.currentTimeMillis() - time;
613 if (TRACE) solver.out.println("Time spent: " + (System.currentTimeMillis() - time));
614 doPostUpdate(null);
615 return false;
616 }
617
618
619 if (!handleUniversalQuantification(allRelationValues)) {
620 if (solver.REPORT_STATS) totalTime += System.currentTimeMillis() - time;
621 if (TRACE) solver.out.println("Time spent: " + (System.currentTimeMillis() - time));
622 doPostUpdate(null);
623 return false;
624 }
625
626
627 boolean[] needWholeRelation = null;
628 if (cache_before_rename) {
629 needWholeRelation = new boolean[allRelationValues.length];
630 for (int i = 0; i < allRelationValues.length; ++i) {
631 if (!allRelationValues[i].equals(oldRelationValues[i])) {
632 if (TRACE) {
633 Relation r = ((RuleTerm) top.get(i)).relation;
634 solver.out.print("Diff relation #" + i + " ("+r+") : (" + allRelationValues[i].nodeCount() + "x" + oldRelationValues[i].nodeCount()
635 + "=");
636
637 ttime = System.currentTimeMillis();
638 }
639 newRelationValues[i] = allRelationValues[i].apply(oldRelationValues[i], BDDFactory.diff);
640 if (TRACE) {
641 solver.out.print(newRelationValues[i].nodeCount() + ")");
642 solver.out.println(" (" + (System.currentTimeMillis() - ttime) + " ms)");
643 }
644 if (TRACE_FULL) {
645 solver.out.println("New for relation #" + i + ": " + newRelationValues[i].toStringWithDomains());
646 }
647 Assert._assert(!newRelationValues[i].isZero());
648 for (int j = 0; j < needWholeRelation.length; ++j) {
649 if (i == j) continue;
650 needWholeRelation[j] = true;
651 }
652 }
653 oldRelationValues[i].free();
654 }
655 }
656 BDD[] rallRelationValues;
657 if (cache_before_rename) rallRelationValues = new BDD[top.size()];
658 else rallRelationValues = allRelationValues;
659
660
661 for (int i = 0; i < top.size(); ++i) {
662 RuleTerm rt = (RuleTerm) top.get(i);
663 BDDRelation r = (BDDRelation) rt.relation;
664 if (TRACE) solver.out.println("Relation " + r + " " + allRelationValues[i].nodeCount() + " nodes, domains "
665 + domainsOf(allRelationValues[i]));
666 if (TRACE_FULL) solver.out.println(" current value: " + allRelationValues[i].toStringWithDomains());
667 BDDPairing pairing = renames[i];
668 if (cache_before_rename) {
669 if (pairing != null) {
670 if (newRelationValues[i] != null) {
671 if (TRACE) {
672 solver.out.print("Diff for Relation " + r + " domains " + domainsOf(newRelationValues[i]) + " -> ");
673 ttime = System.currentTimeMillis();
674 }
675 newRelationValues[i].replaceWith(pairing);
676 if (TRACE) {
677 solver.out.print(domainsOf(newRelationValues[i]));
678 solver.out.println(" (" + (System.currentTimeMillis() - ttime) + " ms)");
679 }
680 }
681 if (needWholeRelation[i]) {
682 if (TRACE) {
683 solver.out.print("Whole Relation " + r + " domains " + domainsOf(allRelationValues[i]) + " -> ");
684 ttime = System.currentTimeMillis();
685 }
686 rallRelationValues[i] = allRelationValues[i].replace(pairing);
687 if (TRACE) {
688 solver.out.print(domainsOf(rallRelationValues[i]));
689 solver.out.println(" (" + (System.currentTimeMillis() - ttime) + " ms)");
690 }
691 }
692 }
693 if (rallRelationValues[i] == null) {
694 rallRelationValues[i] = allRelationValues[i].id();
695 }
696 } else {
697 if (pairing != null) {
698 if (TRACE) {
699 solver.out.print("Relation " + r + " domains " + domainsOf(allRelationValues[i]) + " -> ");
700 ttime = System.currentTimeMillis();
701 }
702 allRelationValues[i].replaceWith(pairing);
703 if (TRACE) {
704 solver.out.print(domainsOf(allRelationValues[i]));
705 solver.out.println(" (" + (System.currentTimeMillis() - ttime) + " ms)");
706 }
707 }
708 if (!allRelationValues[i].equals(oldRelationValues[i])) {
709 if (TRACE) {
710 solver.out.print("Diff relation #" + i + ": (" + allRelationValues[i].nodeCount() + "x" + oldRelationValues[i].nodeCount()
711 + "=");
712 ttime = System.currentTimeMillis();
713 }
714 newRelationValues[i] = allRelationValues[i].apply(oldRelationValues[i], BDDFactory.diff);
715 if (TRACE) {
716 solver.out.print(newRelationValues[i].nodeCount() + ")");
717 solver.out.println(" (" + (System.currentTimeMillis() - ttime) + " ms)");
718 }
719 if (TRACE_FULL) solver.out.println("New for relation " + r + ": " + newRelationValues[i].toStringWithDomains());
720 }
721 oldRelationValues[i].free();
722 }
723 }
724 BDDRelation r = (BDDRelation) bottom.relation;
725 if (TRACE_FULL) solver.out.println("Current value of relation " + bottom + ": " + r.relation.toStringWithDomains());
726 BDD[] newRelationValuesCopy = new BDD[newRelationValues.length];
727
728 BDD[] results = evalRelationsIncremental(solver.bdd, newRelationValues, rallRelationValues, canQuantifyAfter);
729 long thisTime = System.currentTimeMillis() - time;
730 if (cache_before_rename) {
731 for (int i = 0; i < rallRelationValues.length; ++i) {
732 rallRelationValues[i].free();
733 }
734 }
735 if (TRACE) solver.out.print("Result: ");
736 BDD result = solver.bdd.zero();
737 for (int i = 0; i < results.length; ++i) {
738 if (results[i] != null) {
739 if (TRACE) {
740 ttime = System.currentTimeMillis();
741 }
742 result.orWith(results[i]);
743 if (TRACE) {
744 solver.out.print(" -> " + result.nodeCount());
745 solver.out.print(" (" + (System.currentTimeMillis() - ttime) + " ms)");
746 }
747 }
748 }
749 if (TRACE) solver.out.println(" -> " + result.nodeCount());
750 if (single) {
751 result = limitToSingle(result);
752 if (TRACE) solver.out.println("Limited to single satisfying tuple: " + result.nodeCount());
753 }
754 if (bottomRename != null) {
755 if (TRACE) {
756 solver.out.print("Result domains: " + domainsOf(result) + " -> ");
757 ttime = System.currentTimeMillis();
758 }
759 result.replaceWith(bottomRename);
760 if (TRACE) {
761 solver.out.print(domainsOf(result));
762 solver.out.println(" (" + (System.currentTimeMillis() - ttime) + " ms)");
763 }
764 }
765 for (int i = 0; i < bottom.variables.size(); ++i) {
766 Variable v = (Variable) bottom.variables.get(i);
767 if (v instanceof Constant) {
768 Constant c = (Constant) v;
769 BDDDomain d = (BDDDomain) r.domains.get(i);
770 if (TRACE) {
771 solver.out.print("Restricting result domain " + d + " to constant " + c);
772 ttime = System.currentTimeMillis();
773 }
774 result.andWith(d.ithVar(c.value));
775 if (TRACE) {
776 solver.out.println(" (" + (System.currentTimeMillis() - ttime) + " ms)");
777 }
778 }
779 }
780 BDD oldRelation = r.relation.id();
781 if (TRACE_FULL) solver.out.println("Adding to " + bottom + ": " + result.toStringWithDomains());
782 if (TRACE) {
783 solver.out.print("Result: " + r.relation.nodeCount() + " nodes -> ");
784 ttime = System.currentTimeMillis();
785 }
786 r.relation.orWith(result);
787 if (TRACE) {
788 solver.out.print(r.relation.nodeCount() + " nodes, " + r.dsize() + " elements.");
789 solver.out.println(" (" + (System.currentTimeMillis() - ttime) + " ms)");
790 }
791 if (TRACE_FULL) solver.out.println("Relation " + r + " is now: " + r.relation.toStringWithDomains());
792 boolean changed = !oldRelation.equals(r.relation);
793 if (TRACE) solver.out.println("Relation " + r + " changed: " + changed);
794 if (solver.REPORT_STATS) totalTime += System.currentTimeMillis() - time;
795 if (TRACE) solver.out.println("Time spent: " + (System.currentTimeMillis() - time));
796 r.updateNegated();
797 r.doUpdate(oldRelation);
798 if (r.negated != null) {
799 BDD old_neg = oldRelation.not();
800 ((BDDRelation)r.negated).doUpdate(old_neg);
801 old_neg.free();
802 }
803 doPostUpdate(oldRelation);
804 oldRelation.free();
805 oldRelationValues = allRelationValues;
806 return changed;
807 }
808
809 BDD limitToSingle(BDD result) {
810
811 BDDVarSet set = solver.bdd.emptySet();
812 for (Iterator k = bottom.variables.iterator(); k.hasNext(); ) {
813 Variable v = (Variable) k.next();
814 if (unnecessaryVariables.contains(v)) continue;
815 BDDDomain d2 = (BDDDomain) variableToBDDDomain.get(v);
816 set.unionWith(d2.set());
817 }
818 BDD singleResult = result.satOne(set, false);
819 result.free();
820 if (solver.NOISY) {
821 solver.out.println(" Limiting result to a single tuple: "+singleResult.toStringWithDomains());
822 }
823 set.free();
824 return singleResult;
825 }
826
827 public BDD[] evalRelationsIncremental(BDDFactory bdd, BDD[] newRelationValues, BDD[] rallRelationValues, BDDVarSet[] canQuantifyAfter){
828 long ttime = 0;
829 BDD[] results = new BDD[newRelationValues.length];
830 outer : for (int i = 0; i < newRelationValues.length; ++i) {
831 if (newRelationValues[i] == null) {
832 if (TRACE) solver.out.println("Nothing new for " + (RuleTerm) top.get(i) + ", skipping.");
833 continue;
834 }
835 Assert._assert(!newRelationValues[i].isZero());
836 RuleTerm rt_new = (RuleTerm) top.get(i);
837 results[i] = bdd.universe();
838 for (int j = 0; j < rallRelationValues.length; ++j) {
839 RuleTerm rt = (RuleTerm) top.get(j);
840 BDDVarSet canNowQuantify = canQuantifyAfter[j];
841 if (TRACE) solver.out.print(" x " + rt.relation);
842 BDD b;
843 if (i != j) {
844 b = rallRelationValues[j].id();
845 } else {
846 b = newRelationValues[i];
847 if (TRACE) solver.out.print("'");
848 }
849
850 if (TRACE) {
851 solver.out.print(" (relprod " + b.nodeCount());
852 }
853 if (TRACE || find_best_order || DUMP_CUTOFF > 0) ttime = System.currentTimeMillis();
854 BDD topBdd = results[i].relprod(b, canNowQuantify);
855 if (TRACE || find_best_order || DUMP_CUTOFF > 0) ttime = System.currentTimeMillis() - ttime;
856 if (TRACE) {
857 solver.out.print("=" + topBdd.nodeCount() + ")");
858 solver.out.print(" (" + ttime + " ms)");
859 }
860 if (DUMP_CUTOFF > 0 && ttime >= DUMP_CUTOFF &&
861 SystemProperties.getPropertyFromFile("dumpslow") != null) {
862 long ftime = System.currentTimeMillis();
863
864 try {
865 String baseName = solver.getBaseName()+"rule"+id+"_subgoal"+i+","+j+"_update"+updateCount;
866 Writer w = new FileWriter(baseName+".info");
867 w.write("Rule: "+this+"\n");
868 w.write("Time: "+ttime+" ms\n");
869 w.close();
870 BDDRelation.save(solver, baseName+"_op1.bdd", results[i]);
871 BDDRelation.save(solver, baseName+"_op2.bdd", b);
872 BDDRelation.save(solver, baseName+"_op3.bdd", canNowQuantify.toBDD());
873 } catch (IOException x) {
874 System.err.println("Error dumping BDD: "+x);
875 }
876 ftime = System.currentTimeMillis() - ftime;
877 this.totalTime -= ftime;
878 }
879 if (find_best_order && !results[i].isOne() && ttime >= FBO_CUTOFF) {
880 long ftime = System.currentTimeMillis();
881 FindBestDomainOrder.findBestDomainOrder(solver,this, top.size() + i*j,solver.bdd, results[i], b, canNowQuantify,
882 (RuleTerm) top.get(j-1), rt,
883 variableSet[j], rt.variables);
884
885 ftime = System.currentTimeMillis() - ftime;
886 this.totalTime -= ftime;
887 }
888 b.free();
889 results[i].free();
890 results[i] = topBdd;
891 if (results[i].isZero()) {
892 if (TRACE) solver.out.println(" Became empty, skipping.");
893 if (j < i) newRelationValues[i].free();
894 continue outer;
895 }
896 }
897 if (TRACE_FULL) solver.out.println(" = " + results[i].toStringWithDomains());
898 else if (TRACE) solver.out.println(" = " + results[i].nodeCount());
899 }
900 return results;
901 }
902
903
904
905
906
907 public void reportStats() {
908 solver.out.println("Rule " + this);
909 solver.out.println(" Updates: " + updateCount);
910 solver.out.println(" Time: " + totalTime + " ms");
911 solver.out.println(" Longest Iteration: " + longestIteration + " (" + longestTime + " ms)");
912 }
913
914 /***
915 * Helper function to return a string of the domains of a given BDD.
916 *
917 * @param b input BDD
918 * @return string representation of the domains
919 */
920 private String domainsOf(BDD b) {
921 BDDVarSet s = b.support();
922 String result = domainsOf(s);
923 s.free();
924 return result;
925 }
926
927 private String domainsOf(BDDVarSet s) {
928 BDDDomain[] a = s.getDomains();
929 if (a.length == 0) return "(none)";
930 StringBuffer sb = new StringBuffer();
931 for (int i = 0; i < a.length; ++i) {
932 sb.append(a[i]);
933 if (i < a.length - 1) sb.append(',');
934 }
935 return sb.toString();
936 }
937
938
939
940
941
942
943 public void free() {
944 super.free();
945 if (oldRelationValues != null) {
946 for (int i = 0; i < oldRelationValues.length; ++i) {
947 if (oldRelationValues[i] != null) {
948 oldRelationValues[i].free();
949 oldRelationValues[i] = null;
950 }
951 }
952 }
953 if (canQuantifyAfter != null) {
954 for (int i = 0; i < canQuantifyAfter.length; ++i) {
955 if (canQuantifyAfter[i] != null) {
956 canQuantifyAfter[i].free();
957 canQuantifyAfter[i] = null;
958 }
959 }
960 }
961 if (renames != null) {
962 for (int i = 0; i < renames.length; ++i) {
963 if (renames[i] != null) {
964
965
966 renames[i] = null;
967 }
968 }
969 }
970 if (bottomRename != null) {
971
972
973 bottomRename = null;
974 }
975 }
976
977 /***
978 * Helper function to convert the given term to a string representation.
979 *
980 * @param t term
981 * @return string representation
982 */
983 private String termToString(RuleTerm t) {
984 StringBuffer sb = new StringBuffer();
985 sb.append(t.relation);
986 sb.append("(");
987 for (Iterator i = t.variables.iterator(); i.hasNext();) {
988 Variable v = (Variable) i.next();
989 sb.append(v);
990 if (variableToBDDDomain != null) {
991 BDDDomain d = (BDDDomain) variableToBDDDomain.get(v);
992 if (d != null) {
993 sb.append(':');
994 sb.append(d.getName());
995 }
996 }
997 if (i.hasNext()) sb.append(",");
998 }
999 sb.append(")");
1000 return sb.toString();
1001 }
1002
1003
1004
1005
1006
1007
1008 public String toString() {
1009 StringBuffer sb = new StringBuffer();
1010 sb.append(termToString(bottom));
1011 sb.append(" :- ");
1012 for (Iterator i = top.iterator(); i.hasNext();) {
1013 RuleTerm t = (RuleTerm) i.next();
1014 sb.append(termToString(t));
1015 if (i.hasNext()) sb.append(", ");
1016 }
1017 sb.append(".");
1018 return sb.toString();
1019 }
1020
1021
1022
1023 public class VarOrderComparator implements Comparator {
1024
1025 String varorder;
1026
1027 public VarOrderComparator(String vo) {
1028 this.varorder = vo;
1029 }
1030
1031
1032
1033
1034 public int compare(Object arg0, Object arg1) {
1035 if (arg0 == arg1) return 0;
1036 Variable v0 = (Variable) arg0;
1037 Variable v1 = (Variable) arg1;
1038 BDDDomain d0 = (BDDDomain) variableToBDDDomain.get(v0);
1039 BDDDomain d1 = (BDDDomain) variableToBDDDomain.get(v1);
1040 if (d0 == null) {
1041 if (d1 == null) return 0;
1042 return 1;
1043 } else if (d1 == null) {
1044 return -1;
1045 }
1046 int index0 = varorder.indexOf(d0.getName());
1047 int index1 = varorder.indexOf(d1.getName());
1048 if (index0 < index1) return -1;
1049 else if (index0 > index1) return 1;
1050 return 0;
1051 }
1052
1053 }
1054
1055 public static final long LONG_TIME = 10000000;
1056 public static int MAX_FBO_TRIALS = Integer.parseInt(SystemProperties.getProperty("fbotrials", "50"));
1057
1058 int lastTrialNum = -1;
1059 }