1
2
3
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.Comparator;
10 import java.util.HashMap;
11 import java.util.Iterator;
12 import java.util.LinkedHashMap;
13 import java.util.LinkedList;
14 import java.util.List;
15 import java.util.Map;
16 import java.io.File;
17 import java.io.FileReader;
18 import java.io.IOException;
19 import java.io.LineNumberReader;
20 import java.io.PrintStream;
21 import java.math.BigInteger;
22 import java.net.URL;
23 import java.text.DecimalFormat;
24 import jwutil.classloader.HijackingClassLoader;
25 import jwutil.collections.GenericMultiMap;
26 import jwutil.collections.IndexMap;
27 import jwutil.collections.MultiMap;
28 import jwutil.collections.Pair;
29 import jwutil.io.SystemProperties;
30 import jwutil.reflect.Reflect;
31 import jwutil.util.Assert;
32 import net.sf.bddbddb.InferenceRule.DependenceNavigator;
33 import net.sf.bddbddb.ir.IR;
34
35 /***
36 * Solver
37 *
38 * @author jwhaley
39 * @version $Id: Solver.java 628 2005-09-27 23:10:31Z joewhaley $
40 */
41 public abstract class Solver {
42 static {
43 SystemProperties.read("solver.properties");
44 }
45
46 /*** Print rules as they are triggered. */
47 boolean NOISY = !SystemProperties.getProperty("noisy", "yes").equals("no");
48 /*** Split all rules. */
49 boolean SPLIT_ALL_RULES = !SystemProperties.getProperty("split_all_rules", "no").equals("no");
50 /*** Split no rules, even if they have a "split" keyword. */
51 boolean SPLIT_NO_RULES = !SystemProperties.getProperty("split_no_rules", "no").equals("no");
52 /*** Report the stats for each rule at the end. */
53 boolean REPORT_STATS = true;
54 /*** Trace the solver. */
55 boolean TRACE = SystemProperties.getProperty("tracesolve") != null;
56 /*** Do a full trace, even dumping the contents of relations. */
57 boolean TRACE_FULL = SystemProperties.getProperty("fulltracesolve") != null;
58 /*** Use the IR rather than the rules. */
59 boolean USE_IR = !SystemProperties.getProperty("useir", "no").equals("no");
60 /*** Print the IR before interpreting it. */
61 boolean PRINT_IR = SystemProperties.getProperty("printir") != null;
62
63 /*** Trace output stream. */
64 public PrintStream out = System.out;
65 public PrintStream err = System.err;
66
67 /*** Input Datalog filename. */
68 String inputFilename;
69 /*** Base directory where to load/save files. */
70 String basedir = SystemProperties.getProperty("basedir");
71 /*** Include directories. */
72 String includedirs = SystemProperties.getProperty("includedirs");
73 /*** List of paths to search when loading files. */
74 List
75 /*** Map between id numbers and relations. */
76 IndexMap
77 /*** Map between names and domains. */
78 Map
79 /*** Map between names and relations. */
80 Map
81 /*** Map between domains and equivalence relations. */
82 MultiMap
83 /*** Map between domains and less than relations. */
84 MultiMap
85 /*** Map between domains and greater than relations. */
86 MultiMap
87 /*** Map between domains and equivalence relations. */
88 Map
89 /*** List of inference rules. */
90 List
91 /*** Iteration order. */
92 IterationFlowGraph ifg;
93
94 /*** Flag that is set on initialization. */
95 boolean isInitialized;
96
97 Collection
98 Collection
99 Collection
100 Collection
101 Collection
102 Collection
103 Collection
104
105 /***
106 * Create a new inference rule.
107 *
108 * @param top list of subgoals of rule
109 * @param bottom head of rule
110 * @return new inference rule
111 */
112 abstract InferenceRule createInferenceRule(List
113
114 /***
115 * Create a new equivalence relation.
116 *
117 * @param fd1 first domain of relation
118 * @param fd2 second domain of relation
119 * @return new equivalence relation
120 */
121 abstract Relation createEquivalenceRelation(Domain fd1, Domain fd2);
122
123 /***
124 * Create a new less-than relation.
125 *
126 * @param fd1 first domain of relation
127 * @param fd2 second domain of relation
128 * @return new equivalence relation
129 */
130 abstract Relation createLessThanRelation(Domain fd1, Domain fd2);
131
132 /***
133 * Create a new greater-than relation.
134 *
135 * @param fd1 first domain of relation
136 * @param fd2 second domain of relation
137 * @return new equivalence relation
138 */
139 abstract Relation createGreaterThanRelation(Domain fd1, Domain fd2);
140
141 /***
142 * Create a new map relation.
143 *
144 * @param fd1 first domain of relation
145 * @param fd2 second domain of relation
146 * @return new map relation
147 */
148 abstract Relation createMapRelation(Domain fd1, Domain fd2);
149
150 /***
151 * Create a new relation.
152 *
153 * @param name name of relation
154 * @param attributes attributes of relation
155 * @return new relation
156 */
157 public abstract Relation createRelation(String name, List
158
159 /***
160 * Register the given relation with this solver.
161 *
162 * @param r relation to register
163 */
164 void registerRelation(Relation r) {
165 int i = relations.get(r);
166 Assert._assert(i == relations.size() - 1);
167 Assert._assert(i == r.id);
168 Object old = nameToRelation.put(r.name, r);
169 Assert._assert(old == null);
170 }
171
172 /***
173 * Create a numbering rule from the given rule template.
174 *
175 * @param ir incoming rule
176 * @return new numbering rule
177 */
178 NumberingRule createNumberingRule(InferenceRule ir) {
179 return new NumberingRule(this, ir);
180 }
181
182 /***
183 * Construct a solver object.
184 */
185 protected Solver() {
186 clear();
187 }
188
189 /***
190 * Clear this solver of all relations, domains, and rules.
191 */
192 public void clear() {
193 relations = new IndexMap("relations");
194 nameToDomain = new HashMap();
195 nameToRelation = new HashMap();
196 equivalenceRelations = new GenericMultiMap();
197 greaterThanRelations = new GenericMultiMap();
198 lessThanRelations = new GenericMultiMap();
199 mapRelations = new HashMap();
200 rules = new LinkedList();
201 relationsToLoad = new LinkedList();
202 relationsToLoadTuples = new LinkedList();
203 relationsToDump = new LinkedList();
204 relationsToDumpTuples = new LinkedList();
205 relationsToPrintTuples = new LinkedList();
206 relationsToPrintSize = new LinkedList();
207 dotGraphsToDump = new LinkedList();
208 }
209
210 /***
211 * Initialize all of the relations and rules.
212 */
213 public void initialize() {
214 for (Iterator i = nameToRelation.values().iterator(); i.hasNext();) {
215 Relation r = (Relation) i.next();
216 r.initialize();
217 }
218 for (Iterator i = rules.iterator(); i.hasNext();) {
219 InferenceRule r = (InferenceRule) i.next();
220 r.initialize();
221 }
222 }
223
224 Stratify stratify;
225 IR ir;
226
227 /***
228 * Stratify the rules.
229 */
230 public void stratify(boolean noisy) {
231 stratify = new Stratify(this);
232 stratify.NOISY = noisy;
233 stratify.stratify();
234
235 if (USE_IR) {
236 ir = IR.create(stratify);
237 ifg = ir.graph;
238 ir.optimize();
239 if (PRINT_IR) ir.printIR();
240 } else {
241 ifg = new IterationFlowGraph(rules, stratify);
242
243 }
244 }
245
246 /***
247 * Solve the rules.
248 */
249 public abstract void solve();
250
251 /***
252 * Called after solving.
253 */
254 public abstract void finish();
255
256 /***
257 * Clean up the solver, freeing the memory associated with it.
258 */
259 public abstract void cleanup();
260
261 /***
262 * Get the named domain.
263 *
264 * @param name domain name
265 * @return domain that has the name
266 */
267 public Domain getDomain(String name) {
268 return (Domain) nameToDomain.get(name);
269 }
270
271 /***
272 * Get the named relation.
273 *
274 * @param name relation name
275 * @return relation that has the name
276 */
277 public Relation getRelation(String name) {
278 return (Relation) nameToRelation.get(name);
279 }
280
281 /***
282 * Get the relation with the given index.
283 *
284 * @param index index desired
285 * @return relation
286 */
287 public Relation getRelation(int index) {
288 return (Relation) relations.get(index);
289 }
290
291 public IndexMap getRelations(){ return relations; }
292
293 static void addAllValues(Collection c, MultiMap m) {
294 for (Iterator i = m.keySet().iterator(); i.hasNext(); ) {
295 c.addAll(m.getValues(i.next()));
296 }
297 }
298
299 /***
300 * Get all the equivalence relations.
301 *
302 * @return collection of equivalence relations
303 */
304 public Collection getComparisonRelations() {
305 Collection set = new LinkedList();
306 addAllValues(set, equivalenceRelations);
307 addAllValues(set, lessThanRelations);
308 addAllValues(set, greaterThanRelations);
309 set.addAll(mapRelations.values());
310 return set;
311 }
312
313 /***
314 * Get the base directory used for output.
315 *
316 * @return base directory used for output
317 */
318 public String getBaseDir() {
319 return basedir;
320 }
321
322 /***
323 * Initialize the basedir variable, given the specified input Datalog filename.
324 *
325 * @param inputFilename input Datalog filename
326 */
327 void initializeBasedir(String inputFilename) {
328 String sep = SystemProperties.getProperty("file.separator");
329 if (basedir == null) {
330 int i = inputFilename.lastIndexOf(sep);
331 if (i >= 0) {
332 basedir = inputFilename.substring(0, i + 1);
333 } else {
334 i = inputFilename.lastIndexOf("/");
335 if (!sep.equals("/") && i >= 0) {
336 basedir = inputFilename.substring(0, i + 1);
337 } else {
338 basedir = "";
339 }
340 }
341 }
342 if (basedir.length() > 0 && !basedir.endsWith(sep) && !basedir.endsWith("/")) {
343 basedir += sep;
344 }
345 if (includedirs == null) includedirs = basedir;
346 }
347
348 public void load(String filename) throws IOException, InstantiationException, IllegalAccessException, ClassNotFoundException {
349 inputFilename = filename;
350 if (NOISY) out.println("Opening Datalog program \"" + inputFilename + "\"");
351 MyReader in = new MyReader(new LineNumberReader(new FileReader(inputFilename)));
352 initializeBasedir(inputFilename);
353 load(in);
354 }
355
356 public void load(MyReader in) throws IOException, InstantiationException, IllegalAccessException, ClassNotFoundException {
357 DatalogParser parser = new DatalogParser(this);
358 parser.readDatalogProgram(in);
359 if (NOISY) out.println(nameToDomain.size() + " field domains.");
360 if (NOISY) out.println(nameToRelation.size() + " relations.");
361 if (NOISY) out.println(rules.size() + " rules.");
362 in.close();
363 if (NOISY) out.print("Splitting rules: ");
364 splitRules();
365 if (NOISY) out.println("done.");
366
367
368
369
370 if (NOISY) out.print("Initializing solver: ");
371 initialize();
372 if (NOISY) out.println("done.");
373 if (NOISY) out.print("Loading initial relations: ");
374 long time = System.currentTimeMillis();
375 loadInitialRelations();
376 time = System.currentTimeMillis() - time;
377 if (NOISY) out.println("done. (" + time + " ms)");
378 out.println("Stratifying: ");
379 time = System.currentTimeMillis();
380 stratify(NOISY);
381 time = System.currentTimeMillis() - time;
382 out.println("done. (" + time + " ms)");
383 out.println("Solving: ");
384 }
385 public long startTime;
386 public void run() {
387 startTime = System.currentTimeMillis();
388 solve();
389 long solveTime = System.currentTimeMillis() - startTime;
390 out.println("done. (" + solveTime + " ms)");
391
392 finish();
393 if (REPORT_STATS) {
394 out.println("SOLVE_TIME=" + solveTime);
395 reportStats();
396 }
397 }
398
399 public void save() throws IOException {
400 if (NOISY) out.print("Saving results: ");
401 long time = System.currentTimeMillis();
402 saveResults();
403 doCallbacks(onSave);
404 time = System.currentTimeMillis() - time;
405 if (NOISY) out.println("done. (" + time + " ms)");
406 }
407
408 Collection onSave = new LinkedList();
409
410 public void addSaveHook(Runnable r) {
411 onSave.add(r);
412 }
413
414 public void doCallbacks(Collection c) {
415 for (Iterator i = c.iterator(); i.hasNext(); ) {
416 Runnable r = (Runnable) i.next();
417 r.run();
418 }
419 }
420
421 /***
422 * The entry point to the application.
423 *
424 * @param args command line arguments
425 * @throws IOException
426 * @throws InstantiationException
427 * @throws IllegalAccessException
428 * @throws ClassNotFoundException
429 */
430 public static Solver main2(String[] args) throws IOException, InstantiationException, IllegalAccessException, ClassNotFoundException {
431 String inputFilename = SystemProperties.getProperty("datalog");
432 if (args.length > 0) inputFilename = args[0];
433 if (inputFilename == null) {
434 printUsage();
435 return null;
436 }
437 String solverName = SystemProperties.getProperty("solver", "net.sf.bddbddb.BDDSolver");
438 Solver dis;
439 dis = (Solver) Class.forName(solverName).newInstance();
440 dis.load(inputFilename);
441 dis.run();
442 dis.save();
443 return dis;
444 }
445
446 /***
447 * Print usage information.
448 */
449 public static void printUsage() {
450 System.out.println("Usage: java {properties} " + Solver.class.getName() + " <datalog file>");
451 System.out.println("System properties:");
452 System.out.println(" -Dnoisy Print rules as they are applied.");
453 System.out.println(" -Dtracesolve Turn on trace information.");
454 System.out.println(" -Dfulltracesolve Also print contents of relations.");
455 System.out.println(" -Dsolver Solver class name.");
456 System.out.println(" -Ddatalog Datalog file name, if not specified on command line.");
457 System.out.println(" -Dbddinfo BDD info file name.");
458 System.out.println(" -Dbddvarorder BDD variable order.");
459 System.out.println(" -Dbddnodes BDD initial node table size.");
460 System.out.println(" -Dbddcache BDD operation cache size.");
461 System.out.println(" -Dbddminfree BDD minimum free parameter.");
462 System.out.println(" -Dincremental Incrementalize all rules by default.");
463 System.out.println(" -Dfindbestorder Find best BDD domain order.");
464 System.out.println(" -Ddumpnumberinggraph Dump the context numbering in dot graph format.");
465 System.out.println(" -Ddumprulegraph Dump the graph of rules in dot format.");
466 System.out.println(" -Duseir Compile rules using intermediate representation.");
467 System.out.println(" -Dprintir Print intermediate representation before interpreting.");
468 }
469
470 /***
471 * A LineNumberReader that can nest through multiple included files.
472 *
473 * @author John Whaley
474 * @version $Id: Solver.java 628 2005-09-27 23:10:31Z joewhaley $
475 */
476 public static class MyReader {
477 /***
478 * Stack of readers, to handle including files.
479 */
480 List readerStack = new LinkedList();
481 /***
482 * Current line number reader.
483 */
484 LineNumberReader current;
485
486 /***
487 * Construct a new reader from the given line number reader.
488 *
489 * @param r reader
490 */
491 public MyReader(LineNumberReader r) {
492 current = r;
493 }
494
495 /***
496 * Register a new reader, pushing the current one on the stack.
497 *
498 * @param r reader to register
499 */
500 public void registerReader(LineNumberReader r) {
501 if (current != null) readerStack.add(current);
502 current = r;
503 }
504
505 /***
506 * Read a line. If the current reader is empty, we pop one off the stack.
507 * If it is empty and the stack is empty, returns null.
508 *
509 * @return the line that was read
510 * @throws IOException
511 */
512 public String readLine() throws IOException {
513 String s;
514 for (;;) {
515 s = current.readLine();
516 if (s != null) return s;
517 if (readerStack.isEmpty()) return null;
518 current = (LineNumberReader) readerStack.remove(readerStack.size() - 1);
519 }
520 }
521
522 /***
523 * Return the line number in the current reader.
524 *
525 * @return line number
526 */
527 public int getLineNumber() {
528 return current.getLineNumber();
529 }
530
531 /***
532 * Close all of the readers we have open.
533 *
534 * @throws IOException
535 */
536 public void close() throws IOException {
537 for (;;) {
538 current.close();
539 if (readerStack.isEmpty()) return;
540 current = (LineNumberReader) readerStack.remove(readerStack.size() - 1);
541 }
542 }
543 }
544
545 /***
546 * Delete the given relation.
547 *
548 * @param r relation to delete
549 */
550 void deleteRelation(Relation r) {
551 relationsToDump.remove(r);
552 relationsToDumpTuples.remove(r);
553 relationsToLoad.remove(r);
554 relationsToLoadTuples.remove(r);
555 relationsToPrintSize.remove(r);
556 relationsToPrintTuples.remove(r);
557 nameToRelation.remove(r.name);
558 }
559
560 boolean includeRelationInComeFromQuery(Relation r, boolean includeDerivations) {
561 String comeFromIncludes = SystemProperties.getProperty("comeFromRelations");
562 if (comeFromIncludes == null) return true;
563 String[] names = comeFromIncludes.split(":");
564 boolean include = false;
565 for (int i=0; !include && i<names.length; i++) {
566 if (includeDerivations) {
567 if (r.name.startsWith(names[i])) include = true;
568 }
569 else {
570 if (r.name.equals(names[i])) include = true;
571 }
572 }
573 return include;
574 }
575
576 /***
577 * Compute a come-from query. A come-from query includes both :- and ?.
578 *
579 * @param rt initial rule term
580 * @return list of inference rules implementing the come-from query
581 */
582 List
583 List newRules = new LinkedList();
584
585 boolean oldTRACE = TRACE;
586 TRACE = TRACE || (SystemProperties.getProperty("traceComeFromQuery") != null);
587
588 Relation r = rt.relation;
589
590
591
592 Relation r2 = createRelation("q_"+r.name, r.attributes);
593
594 RuleTerm my_rt = new RuleTerm(r2, rt.variables);
595 InferenceRule my_ir = createInferenceRule(Collections.singletonList(rt), my_rt);
596
597 if (TRACE) out.println("Adding rule: "+my_ir);
598 newRules.add(my_ir);
599
600 DependenceNavigator nav = new DependenceNavigator(rules);
601 Map
602 LinkedList worklist = new LinkedList();
603 toQueryRelation.put(r, r2);
604 worklist.add(r);
605 while (!worklist.isEmpty()) {
606
607 r = (Relation) worklist.removeFirst();
608
609 r2 = (Relation) toQueryRelation.get(r);
610 if (TRACE) out.println("Finding contributions in relation "+r+": "+r2);
611
612
613 Collection rules = nav.prev(r);
614 for (Iterator i = rules.iterator(); i.hasNext(); ) {
615 InferenceRule ir = (InferenceRule) i.next();
616 if (TRACE) out.println("This rule can contribute: "+ir);
617 Assert._assert(ir.bottom.relation == r);
618
619
620 List
621 Map varMap = new LinkedHashMap();
622 RuleTerm rt2 = new RuleTerm(r2, ir.bottom.variables);
623 terms.add(rt2);
624 addToVarMap(varMap, rt2);
625 for (Iterator j = ir.top.iterator(); j.hasNext(); ) {
626 RuleTerm rt3 = (RuleTerm) j.next();
627 terms.add(rt3);
628 addToVarMap(varMap, rt3);
629 Relation r3 = rt3.relation;
630 Relation r4 = (Relation) toQueryRelation.get(r3);
631 if (r4 == null) {
632 boolean relevantRelation = includeRelationInComeFromQuery(r3,true);
633
634 if (!relevantRelation) {
635 if (TRACE) out.println("Skipping contribution relation "+r3);
636 }
637 else {
638
639 worklist.add(r3);
640 String newName = "q_"+r3.name;
641 r4 = createRelation(newName, r3.attributes);
642 toQueryRelation.put(r3, r4);
643 if (TRACE) out.println("Adding contribution relation "+r3+": "+r4);
644 }
645 }
646 }
647 List vars = new ArrayList(varMap.keySet());
648 List attributes = new ArrayList(vars.size());
649 for (Iterator k = varMap.entrySet().iterator(); k.hasNext(); ) {
650 Map.Entry e = (Map.Entry) k.next();
651 Variable v = (Variable) e.getKey();
652 String name = (String) e.getValue();
653 attributes.add(new Attribute(name, v.getDomain(), ""));
654 }
655 Relation bottomr = createRelation("q"+ir.id+"_"+r.name, attributes);
656 RuleTerm bottom = new RuleTerm(bottomr, vars);
657 InferenceRule newrule = createInferenceRule(terms, bottom);
658 newrule.single = single;
659 if (TRACE) out.println("Adding rule: "+newrule);
660 newRules.add(newrule);
661
662
663
664
665 if(includeRelationInComeFromQuery(r,false)) {
666 List vars_noC = new ArrayList(varMap.keySet());
667 List attributes_noC = new ArrayList(vars.size());
668 for (Iterator k = varMap.entrySet().iterator(); k.hasNext(); ) {
669 Map.Entry e = (Map.Entry) k.next();
670 Variable v = (Variable) e.getKey();
671 String name = (String) e.getValue();
672 if (!name.startsWith("c")) {
673 attributes_noC.add(new Attribute(name, v.getDomain(), ""));
674 }
675 else {
676 vars_noC.remove(v);
677 if (TRACE) out.println("Excluding from non-context version: "+name);
678 }
679 }
680 Relation bottomr_noC = createRelation("q"+ir.id+"_noC_"+r.name, attributes_noC);
681 RuleTerm bottom_noC = new RuleTerm(bottomr_noC, vars_noC);
682 InferenceRule newrule_noC = createInferenceRule(Collections.singletonList(bottom), bottom_noC);
683 newrule_noC.single = single;
684 if (TRACE) out.println("Adding rule: "+newrule_noC);
685 newRules.add(newrule_noC);
686 relationsToPrintTuples.add(bottomr_noC);
687 relationsToDump.add(bottomr_noC);
688 }
689
690
691
692 List terms2 = Collections.singletonList(bottom);
693 for (Iterator j = ir.top.iterator(); j.hasNext(); ) {
694 RuleTerm rt3 = (RuleTerm) j.next();
695 Relation r3 = rt3.relation;
696 Relation r4 = (Relation) toQueryRelation.get(r3);
697 if (r4 != null) {
698 Assert._assert(r4 != null, "no mapping for "+r3);
699 RuleTerm rt4 = new RuleTerm(r4, rt3.variables);
700 InferenceRule newrule2 = createInferenceRule(terms2, rt4);
701
702 if (TRACE) out.println("Adding rule: "+newrule2);
703 newRules.add(newrule2);
704 }
705 }
706 }
707 }
708
709 for (Iterator i = toQueryRelation.values().iterator(); i.hasNext(); ) {
710 Relation r4 = (Relation) i.next();
711 relationsToPrintTuples.add(r4);
712 }
713
714 TRACE = oldTRACE;
715
716 return newRules;
717 }
718
719 /***
720 * Utility function to add the variables in the given rule term to the given
721 * variable map from Variables to Strings. This is used in constructing
722 * come-from queries.
723 *
724 * @param varMap variable map
725 * @param rt rule term whose variables we want to add
726 */
727 private void addToVarMap(Map
728 for (Iterator i = rt.variables.iterator(); i.hasNext(); ) {
729 Variable v = (Variable) i.next();
730 if (v.name.equals("_")) continue;
731 String name;
732 if (v instanceof Constant) {
733 name = rt.relation.getAttribute(rt.variables.indexOf(v)).attributeName;
734 } else {
735 name = v.toString();
736 }
737 varMap.put(v, name);
738 }
739 }
740
741 /***
742 * Get the equivalence relation for the given domains.
743 *
744 * @param fd1 first domain
745 * @param fd2 second domain
746 * @return equivalence relation on those domains
747 */
748 Relation getEquivalenceRelation(Domain fd1, Domain fd2) {
749 if (fd1.name.compareTo(fd2.name) > 0) return getEquivalenceRelation(fd2, fd1);
750 Object key = new Pair(fd1, fd2);
751 Collection c = equivalenceRelations.getValues(key);
752 Relation r;
753 if (c.isEmpty()) {
754 equivalenceRelations.put(key, r = createEquivalenceRelation(fd1, fd2));
755 } else {
756 r = (Relation) c.iterator().next();
757 }
758 return r;
759 }
760
761 /***
762 * Get the negated equivalence relation for the given domains.
763 *
764 * @param fd1 first domain
765 * @param fd2 second domain
766 * @return negated equivalence relation on those domains
767 */
768 Relation getNotEquivalenceRelation(Domain fd1, Domain fd2) {
769 Relation r = getEquivalenceRelation(fd1, fd2);
770 return r.makeNegated(this);
771 }
772
773 /***
774 * Get the greater-than-or-equal-to relation for the given domains.
775 *
776 * @param fd1 first domain
777 * @param fd2 second domain
778 * @return greater-than-or-equal-to relation on those domains
779 */
780 Relation getGreaterThanOrEqualRelation(Domain fd1, Domain fd2) {
781 Relation r = getLessThanRelation(fd1, fd2);
782 return r.makeNegated(this);
783 }
784
785 /***
786 * Get the greater-than relation for the given domains.
787 *
788 * @param fd1 first domain
789 * @param fd2 second domain
790 * @return greater-than relation on those domains
791 */
792 Relation getGreaterThanRelation(Domain fd1, Domain fd2) {
793 Object key = new Pair(fd1, fd2);
794 Collection c = greaterThanRelations.getValues(key);
795 Relation r;
796 if (c.isEmpty()) {
797 greaterThanRelations.put(key, r = createGreaterThanRelation(fd1, fd2));
798 } else {
799 r = (Relation) c.iterator().next();
800 }
801 return r;
802 }
803
804 /***
805 * Get the greater-than relation for the given domains.
806 *
807 * @param fd1 first domain
808 * @param fd2 second domain
809 * @return less-than relation on those domains
810 */
811 Relation getLessThanRelation(Domain fd1, Domain fd2) {
812 Object key = new Pair(fd1, fd2);
813 Collection c = lessThanRelations.getValues(key);
814 Relation r;
815 if (c.isEmpty()) {
816 lessThanRelations.put(key, r = createLessThanRelation(fd1, fd2));
817 } else {
818 r = (Relation) c.iterator().next();
819 }
820 return r;
821 }
822
823 /***
824 * Get the less-than-or-equal-to relation for the given domains.
825 *
826 * @param fd1 first domain
827 * @param fd2 second domain
828 * @return less-than-or-equal-to relation on those domains
829 */
830 Relation getLessThanOrEqualRelation(Domain fd1, Domain fd2) {
831 Relation r = getGreaterThanRelation(fd1, fd2);
832 return r.makeNegated(this);
833 }
834
835 /***
836 * Get the map relation for the given domains.
837 *
838 * @param fd1 first domain
839 * @param fd2 second domain
840 * @return map relation on those domains
841 */
842 Relation getMapRelation(Domain fd1, Domain fd2) {
843 Object key = new Pair(fd1, fd2);
844 Relation r = (Relation) mapRelations.get(key);
845 if (r == null) {
846 mapRelations.put(key, r = createMapRelation(fd1, fd2));
847 }
848 return r;
849 }
850
851 /***
852 * Load in the initial relations.
853 *
854 * @throws IOException
855 */
856 void loadInitialRelations() throws IOException {
857 if (USE_IR) return;
858 for (Iterator i = relationsToLoad.iterator(); i.hasNext();) {
859 Relation r = (Relation) i.next();
860 try {
861 r.load();
862 } catch (IOException x) {
863 out.println("WARNING: Cannot load bdd " + r + ": " + x.toString());
864 }
865 }
866 for (Iterator i = relationsToLoadTuples.iterator(); i.hasNext();) {
867 Relation r = (Relation) i.next();
868 try {
869 r.loadTuples();
870 } catch (IOException x) {
871 out.println("WARNING: Cannot load tuples " + r + ": " + x.toString());
872 }
873 }
874 }
875
876 /***
877 * Split inference rules.
878 */
879 void splitRules() {
880 List newRules = new LinkedList();
881 for (Iterator i = rules.iterator(); i.hasNext();) {
882 InferenceRule r = (InferenceRule) i.next();
883 if (!SPLIT_NO_RULES && (SPLIT_ALL_RULES || r.split)) newRules.addAll(r.split(rules.indexOf(r)));
884 }
885 rules.addAll(newRules);
886 }
887
888 class RuleSorter implements Comparator {
889 long getRuleTime(Object rule) {
890 if (rule instanceof BDDInferenceRule) {
891 return ((BDDInferenceRule)rule).totalTime;
892 }
893 else if (rule instanceof NumberingRule) {
894 return ((NumberingRule)rule).totalTime;
895 }
896 else {
897 return 0;
898 }
899 }
900
901 public int compare(Object o1, Object o2) {
902 return (int)(getRuleTime(o1) - getRuleTime(o2));
903 }
904 }
905
906 /***
907 * Report rule statistics.
908 */
909 void reportStats() {
910 if(USE_IR) return;
911 List sortedRules = new LinkedList(rules);
912 Collections.sort(sortedRules,new RuleSorter());
913
914 for (Iterator i = sortedRules.iterator(); i.hasNext();) {
915 InferenceRule r = (InferenceRule) i.next();
916 r.reportStats();
917
918
919
920
921
922
923
924
925
926 }
927 }
928
929 /***
930 * Save the results and print sizes.
931 *
932 * @throws IOException
933 */
934 void saveResults() throws IOException {
935 if (USE_IR) return;
936 for (Iterator i = relationsToPrintSize.iterator(); i.hasNext();) {
937 Relation r = (Relation) i.next();
938 double size = r.dsize();
939 DecimalFormat myFormatter = new DecimalFormat("0.");
940 String output = myFormatter.format(size);
941 out.println("SIZE OF " + r + ": " + output);
942 }
943 for (Iterator i = relationsToPrintTuples.iterator(); i.hasNext();) {
944 Relation r = (Relation) i.next();
945 double size = r.dsize();
946 DecimalFormat myFormatter = new DecimalFormat("0.");
947 String output = myFormatter.format(size);
948 out.println("Tuples in "+r+": ("+output+")");
949 final int MAX = 100;
950 int num = MAX;
951 TupleIterator j = r.iterator();
952 while (j.hasNext()) {
953 if (--num < 0) break;
954 BigInteger[] a = j.nextTuple();
955 out.print("\t(");
956 for (int k = 0; k < a.length; ++k) {
957 if (k > 0) out.print(',');
958 Attribute at = r.getAttribute(k);
959 out.print(at);
960 out.print('=');
961 out.print(at.attributeDomain.toString(a[k]));
962 if (at.attributeDomain.map != null &&
963 a[k].signum() >= 0 && a[k].intValue() < at.attributeDomain.map.size()) {
964 out.print('(');
965 out.print(a[k]);
966 out.print(')');
967 }
968 }
969 out.println(")");
970 }
971 if (j.hasNext()) {
972 out.println("\tand more ("+r.size()+" in total).");
973 }
974 }
975 for (Iterator i = relationsToDump.iterator(); i.hasNext();) {
976 Relation r = (Relation) i.next();
977 if (NOISY) out.println("Dumping BDD for " + r);
978 r.save();
979 }
980 for (Iterator i = relationsToDumpTuples.iterator(); i.hasNext();) {
981 Relation r = (Relation) i.next();
982 if (NOISY) out.println("Dumping tuples for " + r);
983 r.saveTuples();
984 }
985 for (Iterator i = dotGraphsToDump.iterator(); i.hasNext();) {
986 Dot dot = (Dot) i.next();
987 if (NOISY) out.println("Dumping dot graph");
988 dot.outputGraph();
989 }
990 }
991
992 /***
993 * Return the number of relations.
994 *
995 * @return the number of relations
996 */
997 public int getNumberOfRelations() {
998 return relations.size();
999 }
1000
1001 /***
1002 * Return the list of rules.
1003 *
1004 * @return the list of rules
1005 */
1006 public List getRules() {
1007 return rules;
1008 }
1009
1010 /***
1011 * Returns the ith rule.
1012 *
1013 * @param i index
1014 * @return inference rule
1015 */
1016 public InferenceRule getRule(int i) {
1017 InferenceRule ir = (InferenceRule) rules.get(i);
1018 if (ir.id == i) return ir;
1019 out.println("Id "+i+" doesn't match id "+ir.id+": "+ir);
1020 for (Iterator j = rules.iterator(); j.hasNext(); ) {
1021 ir = (InferenceRule) j.next();
1022 if (ir.id == i) return ir;
1023 }
1024 return null;
1025 }
1026
1027 /***
1028 * Returns the inference rule with the given name.
1029 *
1030 * @param s rule name
1031 * @return inference rul
1032 */
1033 public InferenceRule getRule(String s) {
1034 if (!s.startsWith("rule")) return null;
1035 int index = Integer.parseInt(s.substring(4));
1036 return getRule(index);
1037 }
1038
1039 public InferenceRule getRuleThatContains(Variable v) {
1040 for (Iterator i = rules.iterator(); i.hasNext(); ) {
1041 InferenceRule ir = (InferenceRule) i.next();
1042 if (ir.necessaryVariables == null) continue;
1043 if (ir.necessaryVariables.contains(v) ||
1044 ir.unnecessaryVariables.contains(v)) return ir;
1045 }
1046 return null;
1047 }
1048
1049 /***
1050 * Return the iteration flow graph. This contains the iteration order.
1051 *
1052 * @return iteration flow graph
1053 */
1054 public IterationFlowGraph getIterationFlowGraph() {
1055 return ifg;
1056 }
1057
1058 /***
1059 * Return the collection of relations to load.
1060 *
1061 * @return the collection of relations to load.
1062 */
1063 public Collection getRelationsToLoad() {
1064 return relationsToLoad;
1065 }
1066
1067 /***
1068 * Return the collection of relations to save.
1069 *
1070 * @return the collection of relations to save.
1071 */
1072 public Collection getRelationsToSave() {
1073 return relationsToDump;
1074 }
1075
1076 public static Solver execSolver(String[] args) throws IOException, InstantiationException, IllegalAccessException, ClassNotFoundException {
1077
1078 try {
1079 Class.forName("net.sf.javabdd.BDD");
1080 } catch (ClassNotFoundException x) {
1081 ClassLoader cl = addBDDLibraryToClasspath(args);
1082
1083 Reflect.invoke(cl, Solver.class.getName(), "main2", new Class[] {String[].class}, new Object[] {args});
1084 return null;
1085 }
1086
1087 return main2(args);
1088 }
1089
1090 /***
1091 * Replacement main() function that checks if we have the BDD library in the
1092 * classpath.
1093 *
1094 * @param args
1095 * @throws IOException
1096 */
1097 public static void main(String[] args) throws IOException, InstantiationException, IllegalAccessException, ClassNotFoundException {
1098
1099 try {
1100 Class.forName("net.sf.javabdd.BDD");
1101 } catch (ClassNotFoundException x) {
1102 ClassLoader cl = addBDDLibraryToClasspath(args);
1103
1104 Reflect.invoke(cl, Solver.class.getName(), "main2", new Class[] {String[].class}, new Object[] {args});
1105 return;
1106 }
1107
1108 Solver s = main2(args);
1109 if (s != null) s.cleanup();
1110 }
1111
1112 public static ClassLoader addBDDLibraryToClasspath(String[] args) throws IOException {
1113 System.out.print("BDD library is not in classpath! ");
1114 URL url;
1115 url = HijackingClassLoader.getFileURL("javabdd.jar");
1116 if (url == null) {
1117 String sep = SystemProperties.getProperty("file.separator");
1118 url = HijackingClassLoader.getFileURL(".."+sep+"JavaBDD");
1119 }
1120 if (url == null) {
1121 System.err.println("Cannot find JavaBDD library!");
1122 System.exit(-1);
1123 return null;
1124 }
1125 System.out.println("Adding "+url+" to classpath.");
1126 URL url2 = new File(".").toURL();
1127 return new HijackingClassLoader(new URL[] {url, url2});
1128 }
1129
1130 }