1
2
3
4 package net.sf.bddbddb;
5
6 import java.util.Collection;
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.util.StringTokenizer;
13 import java.io.BufferedReader;
14 import java.io.BufferedWriter;
15 import java.io.FileReader;
16 import java.io.FileWriter;
17 import java.io.IOException;
18 import java.math.BigInteger;
19 import java.security.AccessControlException;
20 import jwutil.collections.GenericMultiMap;
21 import jwutil.collections.ListFactory;
22 import jwutil.collections.MultiMap;
23 import jwutil.collections.Pair;
24 import jwutil.io.SystemProperties;
25 import jwutil.util.Assert;
26 import net.sf.bddbddb.ir.BDDInterpreter;
27 import net.sf.javabdd.BDDDomain;
28 import net.sf.javabdd.BDDFactory;
29 import net.sf.javabdd.BDDPairing;
30
31 /***
32 * An implementation of Solver that uses BDDs.
33 *
34 * @author jwhaley
35 * @version $Id: BDDSolver.java 652 2007-03-06 07:31:06Z joewhaley $
36 */
37 public class BDDSolver extends Solver {
38
39 /***
40 * Filename for BDD domain info file.
41 * The BDD domain info file contains the list of domains that are allocated
42 */
43 public static String bddDomainInfoFileName = SystemProperties.getProperty("bddinfo", "bddinfo");
44
45 /***
46 * Link to the BDD factory we use.
47 */
48 BDDFactory bdd;
49
50 /***
51 * Map from a field domain to the set of BDD domains we have allocated for that field domain.
52 */
53 MultiMap fielddomainsToBDDdomains;
54
55 Map bddPairings;
56
57 public BDDPairing getPairing(Map map) {
58 if (bddPairings == null) bddPairings = new HashMap();
59 BDDPairing p = (BDDPairing) bddPairings.get(map);
60 if (p == null) {
61 p = bdd.makePair();
62 for (Iterator i = map.entrySet().iterator(); i.hasNext(); ) {
63 Map.Entry e = (Map.Entry) i.next();
64 p.set((BDDDomain) e.getKey(), (BDDDomain) e.getValue());
65 }
66 bddPairings.put(map, p);
67 }
68 return p;
69 }
70
71 public void ensureCapacity(Domain d, long v) {
72 ensureCapacity(d, BigInteger.valueOf(v));
73 }
74
75 public void ensureCapacity(Domain d, BigInteger range) {
76 if (d.getSize().compareTo(range) <= 0) {
77 d.setSize(range);
78 boolean any = false;
79 for (Iterator i = this.getBDDDomains(d).iterator(); i.hasNext(); ) {
80 if (ensureCapacity((BDDDomain) i.next(), range)) any = true;
81 }
82 if (any) {
83 out.println("Growing domain "+d+" to "+d.getSize());
84 for (Iterator i = this.getBDDDomains(d).iterator(); i.hasNext(); ) {
85 redoPairings((BDDDomain) i.next(), range);
86 }
87 for (Iterator i = this.getRelations().iterator(); i.hasNext(); ) {
88 BDDRelation r = (BDDRelation) i.next();
89 r.calculateDomainSet();
90
91 }
92 for (Iterator i = this.getRules().iterator(); i.hasNext(); ) {
93 BDDInferenceRule r = (BDDInferenceRule) i.next();
94 r.initializeQuantifySet();
95 }
96 }
97 }
98 }
99
100 private boolean ensureCapacity(BDDDomain d, BigInteger range) {
101 if (true) {
102 int oldSize = d.varNum();
103 int newSize = range.bitLength();
104 if (newSize > oldSize) {
105 throw new IllegalArgumentException("value "+range+" is out of range for domain "+d);
106 }
107 return false;
108 }
109 int oldSize = d.varNum();
110 int newSize = d.ensureCapacity(range);
111 if (oldSize != newSize) {
112 if (TRACE) out.println("Growing BDD domain "+d+" to "+newSize+" bits.");
113 return true;
114 }
115 return false;
116 }
117
118 private void redoPairings(BDDDomain d, BigInteger range) {
119 for (Iterator i = bddPairings.entrySet().iterator(); i.hasNext(); ) {
120 Map.Entry e = (Map.Entry) i.next();
121 Map map = (Map) e.getKey();
122 BDDPairing p = (BDDPairing) e.getValue();
123 boolean change = false;
124 for (Iterator j = map.entrySet().iterator(); j.hasNext(); ) {
125 Map.Entry e2 = (Map.Entry) j.next();
126 if (d == e2.getKey()) {
127 ensureCapacity((BDDDomain) e2.getValue(), range);
128 change = true;
129 }
130 if (d == e2.getValue()) {
131 ensureCapacity((BDDDomain) e2.getKey(), range);
132 change = true;
133 }
134 }
135 if (true) {
136
137 p.reset();
138 for (Iterator j = map.entrySet().iterator(); j.hasNext(); ) {
139 Map.Entry e2 = (Map.Entry) j.next();
140 p.set((BDDDomain) e2.getKey(), (BDDDomain) e2.getValue());
141 }
142 }
143 }
144 }
145
146 FindBestDomainOrder fbo;
147
148 /***
149 * Initial size of BDD node table.
150 * You can set this with "-Dbddnodes=xxx"
151 */
152 int BDDNODES = Integer.parseInt(SystemProperties.getProperty("bddnodes", "500000"));
153
154 /***
155 * Initial size of BDD operation cache.
156 * You can set this with "-Dbddcache=xxx"
157 */
158 int BDDCACHE = Integer.parseInt(SystemProperties.getProperty("bddcache", "0"));
159
160 /***
161 * BDD minimum free parameter. This tells the BDD library when to grow the
162 * node table. You can set this with "-Dbddminfree=xxx"
163 */
164 double BDDMINFREE = Double.parseDouble(SystemProperties.getProperty("bddminfree", ".20"));
165
166 /***
167 * BDD variable ordering.
168 */
169 public String VARORDER = SystemProperties.getProperty("bddvarorder", null);
170
171 public String TRIALFILE = SystemProperties.getProperty("trialfile", null);
172
173 public String BDDREORDER = SystemProperties.getProperty("bddreorder", null);
174
175 /***
176 * Constructs a new BDD solver. Also initializes the BDD library.
177 */
178 public BDDSolver() {
179 super();
180 if (BDDCACHE == 0) BDDCACHE = BDDNODES / 4;
181 out.println("Initializing BDD library (" + BDDNODES + " nodes, cache size " + BDDCACHE + ", min free " + BDDMINFREE + "%)");
182 bdd = BDDFactory.init(1000, BDDCACHE);
183 out.println("Using BDD library "+bdd.getVersion());
184 fielddomainsToBDDdomains = new GenericMultiMap(ListFactory.linkedListFactory);
185 bdd.setMinFreeNodes(BDDMINFREE);
186 try {
187 fbo = new FindBestDomainOrder(this);
188 } catch (NoClassDefFoundError x) {
189 out.println("No machine learning library found, learning disabled.");
190 }
191 }
192
193
194
195
196
197
198 public void initialize() {
199 if (!isInitialized)
200 loadBDDDomainInfo();
201 super.initialize();
202 if (!isInitialized) {
203 setVariableOrdering();
204 }
205 initialize2();
206 isInitialized = true;
207
208 if (TRIALFILE == null && inputFilename != null) {
209 String sep = SystemProperties.getProperty("file.separator");
210 int index1 = inputFilename.lastIndexOf(sep) + 1;
211 if (index1 == 0) index1 = inputFilename.lastIndexOf('/') + 1;
212 int index2 = inputFilename.lastIndexOf('.');
213 if (index1 < index2)
214 TRIALFILE = "trials_"+inputFilename.substring(index1, index2)+".xml";
215 }
216 if (TRIALFILE != null && fbo != null) fbo.loadTrials(TRIALFILE);
217 }
218
219 public String getBaseName() {
220 if (inputFilename == null) return null;
221 String sep = SystemProperties.getProperty("file.separator");
222 int index1 = inputFilename.lastIndexOf(sep) + 1;
223 if (index1 == 0) index1 = inputFilename.lastIndexOf('/') + 1;
224 int index2 = inputFilename.lastIndexOf('.');
225 if (index1 < index2)
226 return inputFilename.substring(index1, index2);
227 else
228 return null;
229 }
230
231 /***
232 * Load the BDD domain info, if it exists.
233 * The domain info is the list of domains that are allocated.
234 */
235 void loadBDDDomainInfo() {
236 BufferedReader in = null;
237 try {
238 in = new BufferedReader(new FileReader(basedir + bddDomainInfoFileName));
239 for (;;) {
240 String s = in.readLine();
241 if (s == null) break;
242 if (s.length() == 0) continue;
243 if (s.startsWith("#")) continue;
244 StringTokenizer st = new StringTokenizer(s);
245 String domain = st.nextToken();
246 Domain fd = (Domain) nameToDomain.get(domain);
247 allocateBDDDomain(fd);
248 }
249 } catch (IOException x) {
250 } catch (AccessControlException x) {
251 } finally {
252 if (in != null) try {
253 in.close();
254 } catch (IOException _) {
255 }
256 }
257 }
258
259 /***
260 * Initialize the values of equivalence relations.
261 */
262 public void initialize2() {
263 for (Iterator i = nameToRelation.values().iterator(); i.hasNext();) {
264 BDDRelation r = (BDDRelation) i.next();
265 r.initialize2();
266 }
267 }
268
269 /***
270 * Set the BDD variable ordering based on VARORDER.
271 */
272 public void setVariableOrdering() {
273 if (VARORDER != null) {
274 VARORDER = fixVarOrder(VARORDER, true);
275 out.print("Setting variable ordering to " + VARORDER + ", ");
276 if (bdd instanceof net.sf.javabdd.JFactory && BDDREORDER != null) {
277 System.out.println("Target var order:");
278 int[] varOrder = bdd.makeVarOrdering(true, VARORDER);
279 for (int i = 0; i < varOrder.length; ++i) System.out.print(varOrder[i]+",");
280 System.out.println();
281
282 net.sf.javabdd.JFactory jbdd = (net.sf.javabdd.JFactory) bdd;
283 jbdd.reverseAllDomains();
284 jbdd.setVarOrder(VARORDER);
285 } else {
286 int[] varOrder = bdd.makeVarOrdering(true, VARORDER);
287 bdd.setVarOrder(varOrder);
288 if (BDDREORDER != null) {
289 bdd.varBlockAll();
290 }
291 }
292 out.println("done.");
293 int[] varOrder = bdd.getVarOrder();
294 for (int i = 0; i < varOrder.length; ++i) System.out.print(varOrder[i]+",");
295 System.out.println();
296
297 try {
298 bdd.setNodeTableSize(BDDNODES);
299 } catch (OutOfMemoryError x) {
300 out.println("Not enough memory, cannot grow node table size.");
301 bdd.setCacheSize(bdd.getNodeTableSize());
302 bdd.setCacheRatio(4);
303 }
304
305 bdd.setIncreaseFactor(2);
306 }
307 if (BDDREORDER != null) {
308 try {
309 BDDFactory.ReorderMethod m;
310 java.lang.reflect.Field f = BDDFactory.class.getDeclaredField("REORDER_"+BDDREORDER);
311 m = (BDDFactory.ReorderMethod) f.get(null);
312 out.print("Setting dynamic reordering heuristic to " + BDDREORDER + ", ");
313 bdd.autoReorder(m);
314
315 bdd.reorderVerbose(2);
316 out.println("done.");
317 } catch (NoSuchFieldException x) {
318 err.println("Error: no such reordering method \""+BDDREORDER+"\"");
319 } catch (IllegalArgumentException e) {
320 err.println("Error: "+e+" on reordering method \""+BDDREORDER+"\"");
321 } catch (IllegalAccessException e) {
322 err.println("Error: "+e+" on reordering method \""+BDDREORDER+"\"");
323 }
324 }
325 }
326
327 /***
328 * Verify that the variable order is sane: Missing BDD domains are added and extra
329 * BDD domains are removed.
330 */
331 String fixVarOrder(String varOrder, boolean trace) {
332
333 StringTokenizer st = new StringTokenizer(varOrder, "x_");
334 List domains = new LinkedList();
335 while (st.hasMoreTokens()) {
336 domains.add(st.nextToken());
337 }
338 for (int i = 0; i < bdd.numberOfDomains(); ++i) {
339 String dName = bdd.getDomain(i).getName();
340 if (domains.contains(dName)) {
341 domains.remove(dName);
342 continue;
343 }
344 if (trace) out.println("Adding missing domain \"" + dName + "\" to bddvarorder.");
345 String baseName = dName;
346 for (;;) {
347 char c = baseName.charAt(baseName.length() - 1);
348 if (c < '0' || c > '9') break;
349 baseName = baseName.substring(0, baseName.length() - 1);
350 }
351 int j = varOrder.lastIndexOf(baseName);
352 if (j <= 0) {
353 varOrder = dName + "_" + varOrder;
354 } else {
355 char c = varOrder.charAt(j - 1);
356 varOrder = varOrder.substring(0, j) + dName + c + varOrder.substring(j);
357 }
358 }
359 for (Iterator i = domains.iterator(); i.hasNext();) {
360 String dName = (String) i.next();
361 if (trace) out.println("Eliminating unused domain \"" + dName + "\" from bddvarorder.");
362 int index = varOrder.indexOf(dName);
363 if (index == 0) {
364 if (varOrder.length() <= dName.length() + 1) {
365 varOrder = "";
366 } else {
367 varOrder = varOrder.substring(dName.length() + 1);
368 }
369 } else {
370 char before = varOrder.charAt(index - 1);
371 int k = index + dName.length();
372 if (before == '_' && k < varOrder.length() && varOrder.charAt(k) == 'x') {
373
374 varOrder = varOrder.substring(0, index) + varOrder.substring(k + 1);
375 } else {
376 varOrder = varOrder.substring(0, index - 1) + varOrder.substring(k);
377 }
378 }
379 }
380 return varOrder;
381 }
382
383
384
385
386 public void solve() {
387 if (USE_IR) {
388 BDDInterpreter interpreter = new BDDInterpreter(ir);
389 interpreter.interpret();
390 } else {
391 IterationList list = ifg.getIterationList();
392 if (NOISY) System.out.println(list.dump());
393 BDDInterpreter interpreter = new BDDInterpreter(null);
394 long time = System.currentTimeMillis();
395 interpreter.interpret(list);
396 }
397 }
398
399
400
401
402
403
404 public void finish() {
405 try {
406 saveBDDDomainInfo();
407 } catch (IOException x) {
408 }
409
410
411
412
413 }
414
415
416
417
418 public void cleanup() {
419 BDDFactory.CacheStats s = bdd.getCacheStats();
420 if (s.uniqueAccess > 0) {
421 out.println(s);
422 }
423 bdd.done();
424 }
425
426 /***
427 * Save the BDD domain info.
428 *
429 * @throws IOException
430 */
431 void saveBDDDomainInfo() throws IOException {
432 BufferedWriter dos = null;
433 try {
434 dos = new BufferedWriter(new FileWriter(basedir + "r" + bddDomainInfoFileName));
435 for (int i = 0; i < bdd.numberOfDomains(); ++i) {
436 BDDDomain d = bdd.getDomain(i);
437 for (Iterator j = fielddomainsToBDDdomains.keySet().iterator(); j.hasNext();) {
438 Domain fd = (Domain) j.next();
439 if (fielddomainsToBDDdomains.getValues(fd).contains(d)) {
440 dos.write(fd.toString() + "\n");
441 break;
442 }
443 }
444 }
445 } finally {
446 if (dos != null) dos.close();
447 }
448 }
449
450 /***
451 * Make a BDD domain with the given name and number of bits.
452 *
453 * @param name name of BDD domain
454 * @param bits number of bits desired
455 * @return new BDD domain
456 */
457 BDDDomain makeDomain(String name, int bits) {
458 Assert._assert(bits < 64);
459 BDDDomain d = bdd.extDomain(new long[]{1L << bits})[0];
460 d.setName(name);
461 return d;
462 }
463
464 /***
465 * Allocate a new BDD domain that matches the given domain.
466 *
467 * @param dom domain to match
468 * @return new BDD domain
469 */
470 public BDDDomain allocateBDDDomain(Domain dom) {
471 int version = getBDDDomains(dom).size();
472 int bits = dom.size.subtract(BigInteger.ONE).bitLength();
473 BDDDomain d = makeDomain(dom.name + version, bits);
474 if (TRACE) out.println("Allocated BDD domain " + d + ", size " + dom.size + ", " + bits + " bits.");
475 fielddomainsToBDDdomains.add(dom, d);
476 return d;
477 }
478
479 /***
480 * Get the set of BDD domains allocated for a given domain.
481 *
482 * @param dom domain
483 * @return set of BDD domains
484 */
485 public Collection getBDDDomains(Domain dom) {
486 return fielddomainsToBDDdomains.getValues(dom);
487 }
488
489 /***
490 * Get the k-th BDD domain allocated for a given domain.
491 *
492 * @param dom domain
493 * @param k index
494 * @return k-th BDD domain allocated for the given domain
495 */
496 public BDDDomain getBDDDomain(Domain dom, int k) {
497 List list = (List) fielddomainsToBDDdomains.getValues(dom);
498 return (BDDDomain) list.get(k);
499 }
500
501 /***
502 * Get the BDD domain with the given name.
503 *
504 * @param s name of BDD domain
505 * @return BDD domain with the given name
506 */
507 public BDDDomain getBDDDomain(String s) {
508 for (int i = 0; i < bdd.numberOfDomains(); ++i) {
509 BDDDomain d = bdd.getDomain(i);
510 if (s.equals(d.getName())) return d;
511 }
512 return null;
513 }
514
515 /***
516 * Return the map of field domains to sets of allocated BDD domains.
517 *
518 * @return map between field domains and sets of allocated BDD domains
519 */
520 public MultiMap getBDDDomains() {
521 return fielddomainsToBDDdomains;
522 }
523
524
525
526
527
528
529
530 public InferenceRule createInferenceRule(List top, RuleTerm bottom) {
531 return new BDDInferenceRule(this, top, bottom);
532 }
533
534
535
536
537
538
539
540 public Relation createRelation(String name, List attributes) {
541 while (nameToRelation.containsKey(name)) {
542 name = mungeName(name);
543 }
544 return new BDDRelation(this, name, attributes);
545 }
546
547 /***
548 * Munge the given name to be unique.
549 *
550 * @param name name of relation
551 * @return new unique name
552 */
553 String mungeName(String name) {
554 return name + '#' + relations.size();
555 }
556
557
558
559
560 Relation createEquivalenceRelation(Domain fd1, Domain fd2) {
561 String name = fd1 + "_eq_" + fd2;
562 Attribute a1 = new Attribute(fd1 + "_1", fd1, "");
563 Attribute a2 = new Attribute(fd2 + "_2", fd2, "");
564 BDDRelation r = new BDDRelation(this, name, new Pair(a1, a2));
565 r.special_type = BDDRelation.EQ;
566 return r;
567 }
568
569
570
571
572 Relation createLessThanRelation(Domain fd1, Domain fd2) {
573 String name = fd1 + "_lt_" + fd2;
574 Attribute a1 = new Attribute(fd1 + "_1", fd1, "");
575 Attribute a2 = new Attribute(fd2 + "_2", fd2, "");
576 BDDRelation r = new BDDRelation(this, name, new Pair(a1, a2));
577 r.special_type = BDDRelation.LT;
578 return r;
579 }
580
581
582
583
584 Relation createGreaterThanRelation(Domain fd1, Domain fd2) {
585 String name = fd1 + "_gt_" + fd2;
586 Attribute a1 = new Attribute(fd1 + "_1", fd1, "");
587 Attribute a2 = new Attribute(fd2 + "_2", fd2, "");
588 BDDRelation r = new BDDRelation(this, name, new Pair(a1, a2));
589 r.special_type = BDDRelation.GT;
590 return r;
591 }
592
593
594
595
596 Relation createMapRelation(Domain fd1, Domain fd2) {
597 String name = "map_" + fd1 + "_" + fd2;
598 Attribute a1 = new Attribute(fd1.name, fd1, "");
599 Attribute a2 = new Attribute(fd2.name, fd2, "");
600 BDDRelation r = new BDDRelation(this, name, new Pair(a1, a2));
601 r.special_type = BDDRelation.MAP;
602 return r;
603 }
604
605
606
607
608
609
610 void saveResults() throws IOException {
611 super.saveResults();
612 }
613
614
615
616
617
618
619 public void reportStats() {
620 boolean find_best_order = !SystemProperties.getProperty("findbestorder", "no").equals("no");
621 boolean print_best_order = !SystemProperties.getProperty("printbestorder", "no").equals("no");
622 if(find_best_order || print_best_order){
623 fbo.printBestBDDOrders();
624 return;
625 }
626 int final_node_size = bdd.getNodeNum();
627 int final_table_size = bdd.getNodeTableSize();
628 out.println("MAX_NODES=" + final_table_size);
629 out.println("FINAL_NODES=" + final_node_size);
630 super.reportStats();
631 }
632
633 /***
634 * Get the BDD factory used by this solver.
635 *
636 * @return BDD factory
637 */
638 public BDDFactory getBDDFactory() {
639 return this.bdd;
640 }
641
642 }