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.HashSet;
10 import java.util.Iterator;
11 import java.util.LinkedList;
12 import java.util.List;
13 import java.util.StringTokenizer;
14 import java.io.BufferedReader;
15 import java.io.BufferedWriter;
16 import java.io.FileReader;
17 import java.io.FileWriter;
18 import java.io.IOException;
19 import java.math.BigInteger;
20 import jwutil.io.SystemProperties;
21 import jwutil.util.Assert;
22 import net.sf.javabdd.BDD;
23 import net.sf.javabdd.BDDDomain;
24 import net.sf.javabdd.BDDFactory;
25 import net.sf.javabdd.BDDVarSet;
26 import net.sf.javabdd.BDD.BDDIterator;
27
28 /***
29 * An implementation of Relation that uses BDDs.
30 *
31 * @author jwhaley
32 * @version $Id: BDDRelation.java 650 2006-11-29 08:08:45Z joewhaley $
33 */
34 public class BDDRelation extends Relation {
35
36 public static String BDD_INPUT_SUFFIX = SystemProperties.getProperty("bddinputsuffix", ".bdd");
37 public static String BDD_OUTPUT_SUFFIX = SystemProperties.getProperty("bddoutputsuffix", ".bdd");
38 public static String TUPLES_INPUT_SUFFIX = SystemProperties.getProperty("tuplesinputsuffix", ".tuples");
39 public static String TUPLES_OUTPUT_SUFFIX = SystemProperties.getProperty("tuplesoutputsuffix", ".tuples");
40
41 /***
42 * Link to solver.
43 */
44 protected BDDSolver solver;
45
46 /***
47 * Value of relation.
48 */
49 protected BDD relation;
50
51 /***
52 * List of BDDDomains that are used in this relation.
53 * The indices coincide with those of the attributes.
54 */
55 protected List
56
57 /***
58 * Cache of the BDD set.
59 */
60 private BDDVarSet domainSet;
61
62 static final byte EQ = 1;
63 static final byte LT = 2;
64 static final byte GT = 3;
65 static final byte MAP = 4;
66 protected byte special_type;
67
68 /***
69 * Construct a new BDDRelation.
70 * This is only to be called internally.
71 *
72 * @param solver solver
73 * @param name name of relation
74 * @param attributes list of attributes for relation
75 */
76 BDDRelation(BDDSolver solver, String name, List attributes) {
77 super(solver, name, attributes);
78 this.solver = solver;
79 if (solver.TRACE) solver.out.println("Created BDDRelation " + this);
80 }
81
82
83
84
85
86
87
88 public void initialize() {
89 if (!isInitialized) {
90 if (negated != null && name.startsWith("!")) {
91 if (solver.TRACE) solver.out.println("Skipping initialization of negated BDDRelation " + name);
92 if (solver.TRACE) solver.out.println(" because normal " + negated.name + " is/will be initialized.");
93 return;
94 }
95 this.relation = solver.bdd.zero();
96 this.domains = new LinkedList();
97 if (solver.TRACE) solver.out.println("Initializing BDDRelation " + name + " with attributes " + attributes);
98 this.domainSet = solver.bdd.emptySet();
99 for (Iterator i = attributes.iterator(); i.hasNext();) {
100 Attribute a = (Attribute) i.next();
101 Domain fd = a.attributeDomain;
102 if (fd == null) {
103 throw new IllegalArgumentException("BDD relation "+name+" attribute "+a+" has no domain!");
104 }
105 Collection doms = solver.getBDDDomains(fd);
106 BDDDomain d = null;
107 String option = a.attributeOptions;
108 if (option != null && option.length() > 0) {
109
110 if (!option.startsWith(fd.name)) throw new IllegalArgumentException("Attribute " + a + " has domain " + fd + ", but tried to assign "
111 + option);
112
113
114 for (Iterator j = doms.iterator(); j.hasNext();) {
115 BDDDomain dom = (BDDDomain) j.next();
116 if (dom.getName().equals(option)) {
117 if (domains.contains(dom)) {
118 solver.out.println("Cannot assign " + dom + " to attribute " + a + ": " + dom + " is already assigned");
119 option = "";
120 break;
121 } else {
122 d = dom;
123 break;
124 }
125 }
126 }
127 if (option.length() > 0) {
128 while (d == null) {
129 BDDDomain dom = solver.allocateBDDDomain(fd);
130 if (dom.getName().equals(option)) {
131 d = dom;
132 break;
133 }
134 }
135 }
136 }
137 if (d == null) {
138
139 for (Iterator j = doms.iterator(); j.hasNext();) {
140 BDDDomain dom = (BDDDomain) j.next();
141 if (!domains.contains(dom)) {
142 d = dom;
143 break;
144 }
145 }
146 if (d == null) {
147 d = solver.allocateBDDDomain(fd);
148 }
149 }
150 if (solver.TRACE) solver.out.println("Attribute " + a + " (" + a.attributeDomain + ") assigned to BDDDomain " + d);
151 domains.add(d);
152 domainSet.unionWith(d.set());
153 }
154 isInitialized = true;
155 }
156 if (negated != null && !negated.isInitialized) {
157 BDDRelation bddn = (BDDRelation) negated;
158 bddn.relation = solver.bdd.universe();
159 bddn.domains = this.domains;
160 bddn.domainSet = this.domainSet.id();
161 bddn.isInitialized = true;
162 }
163 }
164
165 /***
166 * (Re-)calculate the domain set.
167 *
168 * @return the domain set
169 */
170 BDDVarSet calculateDomainSet() {
171 if (domainSet != null) {
172 domainSet.free();
173 }
174 this.domainSet = solver.bdd.emptySet();
175 for (Iterator i = domains.iterator(); i.hasNext();) {
176 BDDDomain d = (BDDDomain) i.next();
177 domainSet.unionWith(d.set());
178 }
179 return domainSet;
180 }
181
182 public BDDVarSet getDomainSet() {
183 return domainSet;
184 }
185
186 /***
187 * Do more initialization. This initializes the values of equivalence relations.
188 * Called after variable order is set, so the computation is faster.
189 */
190 public void initialize2() {
191 Assert._assert(isInitialized);
192 if (special_type != 0) {
193 BDDDomain d1 = (BDDDomain) domains.get(0);
194 BDDDomain d2 = (BDDDomain) domains.get(1);
195 if (true)
196 solver.out.println("Initializing value of special relation "+this+" "+d1+","+d2);
197
198 relation.free();
199 BDD b;
200 switch (special_type) {
201 case EQ:
202 b = d1.buildEquals(d2);
203 break;
204 case LT:
205 b = buildLessThan(d1, d2);
206 break;
207 case GT:
208 b = buildLessThan(d2, d1);
209 break;
210 case MAP:
211 Domain a1 = ((Attribute)attributes.get(0)).attributeDomain;
212 Domain a2 = ((Attribute)attributes.get(1)).attributeDomain;
213 b = buildMap(a1, d1, a2, d2);
214 break;
215 default:
216 throw new InternalError();
217 }
218
219 relation = b;
220 updateNegated();
221 }
222 }
223
224 /***
225 * Build a BDD representing d1 < d2.
226 *
227 * @param d1 first domain
228 * @param d2 second domain
229 * @return BDD that is true iff d1 < d2.
230 */
231 private BDD buildLessThan(BDDDomain d1, BDDDomain d2) {
232 BDD leftwardBitsEqual = solver.bdd.universe();
233 BDD result = solver.bdd.zero();
234 for (int i=d1.varNum()-1; i>=0; i--) {
235 BDD v1 = d1.getFactory().ithVar(d1.vars()[i]);
236 BDD v2 = d2.getFactory().ithVar(d2.vars()[i]);
237 result.orWith(v2.and(v1.not()).and(leftwardBitsEqual));
238 leftwardBitsEqual.andWith(v1.biimp(v2));
239 }
240 return result;
241 }
242
243 /***
244 * Helper function for building a map.
245 */
246 private BDD buildMap(Domain a1, BDDDomain d1, Domain a2, BDDDomain d2) {
247 if (solver.NOISY) solver.out.print("Building "+this+": ");
248 BigInteger index, size;
249 index = (a2.map != null) ? BigInteger.valueOf(a2.map.size()) : a2.size;
250 size = (a1.map != null) ? BigInteger.valueOf(a1.map.size()) : a1.size;
251 BigInteger total = index.add(size);
252 if (total.compareTo(d2.size()) > 0) {
253 throw new IllegalArgumentException("Domain "+a2+" (current size="+index+", max size="+d2.size()+") is not large enough to contain mapping from "+a1+" (size "+size+")");
254 }
255 int bits = Math.min(d1.varNum(), d2.varNum());
256 BDD b = d1.buildAdd(d2, bits, index.longValue());
257 b.andWith(d1.varRange(BigInteger.ZERO, size.subtract(BigInteger.ONE)));
258 if (a2.map != null) {
259 if (a1.map != null) {
260 a2.map.addAll(a1.map);
261 } else {
262 int v = size.intValue();
263 for (int i = 0; i < v; ++i) {
264 a2.map.get(a1+"_"+i);
265 }
266 }
267 Assert._assert(a2.map.size() == total.intValue(), a1.map.size()+" != "+total);
268 } else {
269 a2.size = a2.size.add(size);
270 }
271 if (solver.NOISY) solver.out.println(a1+" ("+d1+") 0.."+(size.subtract(BigInteger.ONE))+" maps to "+a2+" ("+d2+") "+index+".."+(total.subtract(BigInteger.ONE)));
272 return b;
273 }
274
275 /***
276 * Updated the negated form of this relation.
277 */
278 void updateNegated() {
279 if (negated != null) {
280 BDDRelation bddn = (BDDRelation) negated;
281 bddn.relation.free();
282 bddn.relation = relation.not();
283 }
284 }
285
286 /***
287 * Verify that the domains for this BDD are correct.
288 *
289 * @return whether the domains are correct
290 */
291 public boolean verify() {
292 return verify(relation);
293 }
294
295 /***
296 * Verify that the domains for the given BDD match this relation.
297 *
298 * @param r the given BDD
299 * @return whether the domains match
300 */
301 public boolean verify(BDD r) {
302 if (r == null) return true;
303 BDDVarSet s = r.support();
304 calculateDomainSet();
305 BDDVarSet t = domainSet.union(s);
306 s.free();
307
308
309 boolean result = t.equals(domainSet);
310 if (!result) {
311 solver.out.println("Warning, domains for " + this + " don't match BDD: " + activeDomains(r) + " vs " + domains);
312 }
313 return result;
314 }
315
316
317
318
319 public void load() throws IOException {
320 if (solver.NOISY) solver.out.print("Loading BDD from file: " + name + ".bdd ");
321 load(solver.basedir + name + ".bdd");
322 if (solver.NOISY) solver.out.println(relation.nodeCount() + " nodes, " + dsize() + " elements.");
323 if (solver.TRACE) solver.out.println("Domains of loaded relation:" + activeDomains(relation));
324 }
325
326 public static boolean SMART_LOAD = true;
327
328 /***
329 * Load this relation from the given file.
330 *
331 * @param filename the file to load
332 * @throws IOException
333 */
334 public void load(String filename) throws IOException {
335 Assert._assert(isInitialized);
336 BDD r2;
337 BufferedReader in = null;
338 try {
339 in = new BufferedReader(new FileReader(filename));
340 String s = in.readLine();
341 if (s != null && s.startsWith("# ")) {
342
343 List fileDomains = checkInfoLine(filename, s, false, true);
344 in.mark(4096);
345 int[] translate = null;
346 BDD mask = null;
347 for (Iterator i = fileDomains.iterator(); i.hasNext(); ) {
348 BDDDomain d = (BDDDomain) i.next();
349 String s2 = in.readLine();
350 if (!s2.startsWith("# ")) {
351 solver.err.println("BDD file \""+filename+"\" has no variable assignment line for "+d);
352 in.reset();
353 break;
354 }
355 StringTokenizer st = new StringTokenizer(s2.substring(2));
356 if (!st.hasMoreTokens()) {
357 String msg = "BDD file \""+filename+"\" has an invalid BDD information line";
358 throw new IOException(msg);
359 }
360 int[] vars = d.vars();
361 int j;
362 for (j = 0; j < vars.length; ++j) {
363 if (!st.hasMoreTokens()) {
364 if (!SMART_LOAD) {
365 String msg = "in file \""+filename+"\", not enough bits for domain "+d;
366 throw new IOException(msg);
367 }
368 if (mask == null) mask = solver.bdd.nithVar(vars[j]);
369 else mask.andWith(solver.bdd.nithVar(vars[j]));
370 continue;
371 }
372 int k = Integer.parseInt(st.nextToken());
373 if (vars[j] != k) {
374 if (!SMART_LOAD) {
375 String msg = "in file \""+filename+"\", bit "+j+" for domain "+d+" ("+k+") does not match expected ("+vars[j]+")";
376 throw new IOException(msg);
377 }
378 if (k >= solver.bdd.varNum())
379 solver.bdd.setVarNum(k+1);
380 if (translate == null || translate.length < solver.bdd.varNum()) {
381 int[] t = new int[solver.bdd.varNum()];
382 for (int x = 0; x < t.length; ++x) t[x] = x;
383 if (translate != null) System.arraycopy(translate, 0, t, 0, translate.length);
384 translate = t;
385 }
386 if (solver.TRACE) solver.out.println("Rename "+k+" to "+vars[j]);
387 translate[k] = vars[j];
388 }
389 }
390 if (st.hasMoreTokens()) {
391 if (!SMART_LOAD) {
392 String msg = "in file \""+filename+"\", too many bits for domain "+d;
393 throw new IOException(msg);
394 }
395 int num = 0;
396 for (StringTokenizer st2 = new StringTokenizer(s2.substring(2)); st2.hasMoreTokens(); st2.nextToken(), ++num) ;
397 int extra = num - vars.length;
398 Domain dd = getAttribute(d).getDomain();
399 final boolean ALL_AT_ONCE = false;
400 if (ALL_AT_ONCE)
401 solver.ensureCapacity(dd, BigInteger.ONE.shiftLeft(num));
402 while (--extra >= 0) {
403 if (!ALL_AT_ONCE)
404 solver.ensureCapacity(dd, BigInteger.ONE.shiftLeft(d.varNum()+1));
405 int k = Integer.parseInt(st.nextToken());
406 if (k >= solver.bdd.varNum())
407 solver.bdd.setVarNum(k+1);
408 if (translate == null || translate.length < solver.bdd.varNum()) {
409 int[] t = new int[solver.bdd.varNum()];
410 for (int x = 0; x < t.length; ++x) t[x] = x;
411 if (translate != null) System.arraycopy(translate, 0, t, 0, translate.length);
412 translate = t;
413 }
414 if (solver.TRACE) solver.out.println("Rename "+k+" to "+d.vars()[j]);
415 translate[k] = d.vars()[j];
416 ++j;
417 }
418 Assert._assert(!st.hasMoreTokens());
419 }
420 }
421 r2 = solver.bdd.load(in, translate);
422 if (mask != null) {
423 r2.andWith(mask);
424 }
425 } else {
426 solver.err.println("BDD file \""+filename+"\" has no header line.");
427 r2 = solver.bdd.load(filename);
428 }
429 } finally {
430 if (in != null) try { in.close(); } catch (IOException _) { }
431 }
432 if (r2 != null) {
433 if (r2.isZero()) {
434 solver.out.println("Warning: " + filename + " is zero.");
435 } else if (r2.isOne()) {
436 solver.out.println("Warning: " + filename + " is one.");
437 } else {
438 if (!verify(r2)) {
439 throw new IOException("Expected domains for loaded BDD " + filename + " to be " + domains + ", but found " + activeDomains(r2)
440 + " instead");
441 }
442 }
443 relation.free();
444 relation = r2;
445 }
446 updateNegated();
447 }
448
449
450
451
452 public void loadTuples() throws IOException {
453 loadTuples(solver.basedir + name + ".tuples");
454 if (solver.NOISY) solver.out.println("Loaded tuples from file: " + name + ".tuples");
455 if (solver.NOISY) solver.out.println("Domains of loaded relation:" + activeDomains(relation));
456 }
457
458 /***
459 * Makes a domain info line for this relation.
460 *
461 * @return domain info line
462 */
463 String makeInfoLine() {
464 return makeInfoLine(domains);
465 }
466
467 static String makeInfoLine(Collection domains) {
468 StringBuffer sb = new StringBuffer();
469 sb.append("#");
470 for (Iterator i = domains.iterator(); i.hasNext();) {
471 BDDDomain d = (BDDDomain) i.next();
472 sb.append(' ');
473 sb.append(d.toString());
474 sb.append(':');
475 sb.append(d.varNum());
476 }
477 return sb.toString();
478 }
479
480 /***
481 * Makes a BDD variable info line for this relation and domain.
482 *
483 * @param d domain
484 * @return BDD variable info line
485 */
486 static String makeBDDVarInfoLine(BDDDomain d) {
487 StringBuffer sb = new StringBuffer();
488 sb.append("#");
489 int[] vars = d.vars();
490 for (int i = 0; i < vars.length; ++i) {
491 sb.append(' ');
492 sb.append(vars[i]);
493 }
494 return sb.toString();
495 }
496
497 /***
498 * Checks that the given domain info line matches this relation.
499 *
500 * @param filename filename to use in error message
501 * @param s domain info line
502 * @param order true if we want to check the order, false otherwise
503 * @param ex true if we want to throw an exception, false if we just want to print to stderr
504 * @throws IOException
505 */
506 List checkInfoLine(String filename, String s, boolean order, boolean ex) throws IOException {
507 StringTokenizer st = new StringTokenizer(s.substring(2));
508 List domainList = new ArrayList(domains.size());
509 Iterator i = domains.iterator();
510 while (st.hasMoreTokens()) {
511 String msg = null;
512 String dname = st.nextToken(": ");
513 int dbits = Integer.parseInt(st.nextToken());
514 if (domainList.size() >= domains.size()) {
515 msg = "extra domain "+dname;
516 } else {
517 BDDDomain d = solver.getBDDDomain(dname);
518 if (d == null) {
519 msg = "unknown domain "+dname;
520 } else if (order) {
521 BDDDomain d2 = (BDDDomain) domains.get(domainList.size());
522 if (d != d2) {
523 msg = "domain "+dname+" does not match expected domain "+d2;
524 }
525 } else if (!domains.contains(d)) {
526 msg = "domain "+dname+" is not in domain set "+domains;
527 }
528 if (msg == null && !SMART_LOAD && d.varNum() != dbits) {
529 msg = "number of bits for domain "+dname+" ("+dbits +") does not match expected ("+d.varNum()+")";
530 }
531 if (d != null) domainList.add(d);
532 }
533 if (msg != null) {
534 if (ex) throw new IOException("in file \""+filename+"\", "+msg);
535 else solver.err.println("WARNING: in file \""+filename+"\", "+msg);
536 }
537 }
538 if (domainList.size() != domains.size()) {
539 Collection c = new ArrayList(domains);
540 c.removeAll(domainList);
541 StringBuffer sb = new StringBuffer();
542 sb.append("file \""+filename+"\" is missing domains:");
543 for (Iterator j = c.iterator(); j.hasNext(); ) {
544 sb.append(" "+j.next());
545 }
546 String msg = sb.toString();
547 if (ex) throw new IOException(msg);
548 else solver.err.println("WARNING: "+msg);
549 }
550 return domainList;
551 }
552
553
554
555
556 public void loadTuples(String filename) throws IOException {
557 Assert._assert(isInitialized);
558 BufferedReader in = null;
559 try {
560 in = new BufferedReader(new FileReader(filename));
561
562 String s = in.readLine();
563 if (s == null) return;
564 if (!s.startsWith("# ")) {
565 solver.err.println("Tuple file \""+filename+"\" is missing header line, using default.");
566 BDD b = parseTuple(s);
567 relation.orWith(b);
568 } else {
569 checkInfoLine(filename, s, true, true);
570 }
571 for (;;) {
572 s = in.readLine();
573 if (s == null) break;
574 if (s.length() == 0) continue;
575 if (s.startsWith("#")) continue;
576 BDD b = parseTuple(s);
577 relation.orWith(b);
578 }
579 } finally {
580 if (in != null) in.close();
581 }
582 updateNegated();
583 }
584
585 /***
586 * Parse the given tuple string and return a BDD corresponding to it.
587 *
588 * @param s tuple string
589 * @return BDD form of tuple
590 */
591 BDD parseTuple(String s) {
592 StringTokenizer st = new StringTokenizer(s);
593 BDD b = solver.bdd.universe();
594 for (int i = 0; i < domains.size(); ++i) {
595 BDDDomain d = (BDDDomain) domains.get(i);
596 String v = st.nextToken();
597 if (v.equals("*")) {
598 b.andWith(d.domain());
599 } else {
600 int x = v.indexOf('-');
601 if (x < 0) {
602 BigInteger l = new BigInteger(v);
603 Domain dd = getAttribute(i).getDomain();
604 solver.ensureCapacity(dd, l);
605 b.andWith(d.ithVar(l));
606 if (solver.TRACE_FULL) solver.out.print(attributes.get(i) + ": " + l + ", ");
607 } else {
608 BigInteger l = new BigInteger(v.substring(0, x));
609 BigInteger m = new BigInteger(v.substring(x + 1));
610 Domain dd = getAttribute(i).getDomain();
611 solver.ensureCapacity(dd, m);
612 b.andWith(d.varRange(l, m));
613 if (solver.TRACE_FULL) solver.out.print(attributes.get(i) + ": " + l + "-" + m + ", ");
614 }
615 }
616 }
617 if (solver.TRACE_FULL) solver.out.println();
618 return b;
619 }
620
621
622
623
624 public void save() throws IOException {
625 save(solver.basedir + name + ".bdd");
626 }
627
628 /***
629 * Save a BDD with a valid header.
630 *
631 * @param solver solver object
632 * @param filename filename to save into
633 * @param relation BDD to save
634 * @throws IOException
635 */
636 public static void save(BDDSolver solver, String filename, BDD relation) throws IOException {
637 BDDVarSet s = relation.support();
638 BDDDomain[] doms = s.getDomains();
639 s.free();
640 List domains = Arrays.asList(doms);
641 BDDVarSet dom = solver.bdd.emptySet();
642 for (int i = 0; i < doms.length; ++i) {
643 dom.unionWith(doms[i].set());
644 }
645 solver.out.println("Saving " + filename + ": " + relation.nodeCount() + " nodes, " +
646 relation.satCount(dom) + " elements ("+domains+")");
647 BufferedWriter out = null;
648 try {
649 out = new BufferedWriter(new FileWriter(filename));
650 out.write(makeInfoLine(domains));
651 out.write('\n');
652 for (Iterator i = domains.iterator(); i.hasNext(); ) {
653 BDDDomain d = (BDDDomain) i.next();
654 out.write(makeBDDVarInfoLine(d));
655 out.write('\n');
656 }
657 solver.bdd.save(out, relation);
658 } finally {
659 if (out != null) try { out.close(); } catch (IOException x) { }
660 }
661 }
662
663 /***
664 * Save the value of this relation to the given file.
665 *
666 * @param filename name of file to save
667 * @throws IOException
668 */
669 public void save(String filename) throws IOException {
670 Assert._assert(isInitialized);
671 solver.out.println("Relation " + this + ": " + relation.nodeCount() + " nodes, " + dsize() + " elements ("+activeDomains(relation)+")");
672 BufferedWriter out = null;
673 try {
674 out = new BufferedWriter(new FileWriter(filename));
675 out.write(makeInfoLine());
676 out.write('\n');
677 for (Iterator i = domains.iterator(); i.hasNext(); ) {
678 BDDDomain d = (BDDDomain) i.next();
679 out.write(makeBDDVarInfoLine(d));
680 out.write('\n');
681 }
682 solver.bdd.save(out, relation);
683 } finally {
684 if (out != null) try { out.close(); } catch (IOException x) { }
685 }
686 }
687
688
689
690
691 public void saveTuples() throws IOException {
692 saveTuples(solver.basedir + name + ".tuples");
693 }
694
695 /***
696 * Save the value of this relation in tuple form to the given file.
697 *
698 * @param filename name of file to save
699 * @throws IOException
700 */
701 public void saveTuples(String filename) throws IOException {
702 solver.out.println("Relation " + this + ": " + relation.nodeCount() + " nodes, " + dsize() + " elements ("+activeDomains(relation)+")");
703 saveTuples(solver.basedir + name + ".tuples", relation);
704 }
705
706 /***
707 * Save the given relation in tuple form to the given file.
708 *
709 * @param fileName name of file to save
710 * @param relation value to save
711 * @throws IOException
712 */
713 public void saveTuples(String fileName, BDD relation) throws IOException {
714 Assert._assert(isInitialized);
715 BufferedWriter dos = null;
716 try {
717 dos = new BufferedWriter(new FileWriter(fileName));
718 if (relation.isZero()) {
719 return;
720 }
721 BDD allDomains = solver.bdd.universe();
722 dos.write("#");
723 solver.out.print(fileName + " domains {");
724 int[] domIndices = new int[domains.size()];
725 int k = -1;
726 for (Iterator i = domains.iterator(); i.hasNext();) {
727 BDDDomain d = (BDDDomain) i.next();
728 solver.out.print(" " + d.toString());
729 dos.write(" " + d.toString() + ":" + d.varNum());
730 domIndices[++k] = d.getIndex();
731 }
732 dos.write("\n");
733 solver.out.println(" } = " + relation.nodeCount() + " nodes, " + dsize() + " elements");
734 if (relation.isOne()) {
735 for (k = 0; k < domIndices.length; ++k) {
736 dos.write("* ");
737 }
738 dos.write("\n");
739 return;
740 }
741
742 calculateDomainSet();
743 int lines = 0;
744 BDDIterator i = relation.iterator(domainSet);
745 while (i.hasNext()) {
746 BigInteger[] v = i.nextTuple();
747 for (k = 0; k < domIndices.length; ++k) {
748 BigInteger val = v[domIndices[k]];
749 if (val.equals(BigInteger.ZERO)) {
750
751 BDDDomain d = solver.bdd.getDomain(domIndices[k]);
752 if (i.isDontCare(d)) {
753 i.skipDontCare(d);
754 dos.write("* ");
755 continue;
756 }
757 }
758 dos.write(val + " ");
759 }
760 dos.write("\n");
761 ++lines;
762 }
763 solver.out.println("Done writing " + lines + " lines.");
764 } finally {
765 if (dos != null) dos.close();
766 }
767 }
768
769 /***
770 * Return a string representation of the active domains of the given relation.
771 *
772 * @param r relation to check
773 * @return string representation of the active domains
774 */
775 public static String activeDomains(BDD r) {
776 BDDFactory bdd = r.getFactory();
777 BDDVarSet s = r.support();
778 BDDDomain[] a = s.getDomains();
779 s.free();
780 if (a.length == 0) return "(none)";
781 StringBuffer sb = new StringBuffer();
782 for (int i = 0; i < a.length; ++i) {
783 sb.append(a[i]);
784 if (i < a.length - 1) sb.append(',');
785 }
786 return sb.toString();
787 }
788
789
790
791
792 public double dsize() {
793 calculateDomainSet();
794 return relation.satCount(domainSet);
795 }
796
797
798
799
800 public TupleIterator iterator() {
801 calculateDomainSet();
802 final BDDIterator i = relation.iterator(domainSet);
803 return new MyTupleIterator(i, domains);
804 }
805
806 /***
807 * Implementation of TupleIterator for BDDs.
808 */
809 static class MyTupleIterator extends TupleIterator {
810 protected BDDIterator i;
811 protected List domains;
812
813 protected MyTupleIterator(BDDIterator i, List domains) {
814 this.i = i;
815 this.domains = domains;
816 }
817
818 public BigInteger[] nextTuple() {
819 BigInteger[] q = i.nextTuple();
820 BigInteger[] r = new BigInteger[domains.size()];
821 int j = 0;
822 for (Iterator k = domains.iterator(); k.hasNext(); ++j) {
823 BDDDomain d = (BDDDomain) k.next();
824 r[j] = q[d.getIndex()];
825 }
826 return r;
827 }
828
829 public boolean hasNext() {
830 return i.hasNext();
831 }
832
833 public void remove() {
834 i.remove();
835 }
836 }
837
838
839
840
841 public TupleIterator iterator(int k) {
842 final BDDDomain d = (BDDDomain) domains.get(k);
843 BDDVarSet s = d.set();
844 final BDDIterator i = relation.iterator(s);
845 return new TupleIterator() {
846 public BigInteger[] nextTuple() {
847 BigInteger v = i.nextValue(d);
848 return new BigInteger[]{v};
849 }
850
851 public boolean hasNext() {
852 return i.hasNext();
853 }
854
855 public void remove() {
856 i.remove();
857 }
858 };
859 }
860
861
862
863
864 public TupleIterator iterator(int k, BigInteger j) {
865 final BDDDomain d = (BDDDomain) domains.get(k);
866 BDD val = d.ithVar(j);
867 val.andWith(relation.id());
868 calculateDomainSet();
869 final BDDIterator i = val.iterator(domainSet);
870 return new MyTupleIterator(i, domains);
871 }
872
873
874
875
876 public TupleIterator iterator(BigInteger[] j) {
877 BDD val = relation.id();
878 for (int i = 0; i < j.length; ++i) {
879 if (j[i].signum() < 0) continue;
880 final BDDDomain d = (BDDDomain) domains.get(i);
881 val.andWith(d.ithVar(j[i]));
882 }
883 calculateDomainSet();
884 final BDDIterator i = val.iterator(domainSet);
885 return new MyTupleIterator(i, domains);
886 }
887
888
889
890
891 public boolean contains(int k, BigInteger j) {
892 final BDDDomain d = (BDDDomain) domains.get(k);
893 BDD b = relation.id();
894 b.restrictWith(d.ithVar(j));
895 boolean result = !b.isZero();
896 b.free();
897 return result;
898 }
899
900 boolean add(BDD val) {
901 BDD old = relation.id();
902 relation.orWith(val);
903 boolean result = !old.equals(relation);
904 old.free();
905 return result;
906 }
907
908 /***
909 * Add a single to this relation.
910 *
911 * @param a first attribute
912 * @return whether this relation changed
913 */
914 public boolean add(int a) {
915 BDDDomain d0 = (BDDDomain) domains.get(0);
916 Domain dd0 = getAttribute(0).getDomain();
917 solver.ensureCapacity(dd0, a);
918 BDD val = d0.ithVar(a);
919 return add(val);
920 }
921
922 /***
923 * Add a double to this relation.
924 *
925 * @param a first attribute
926 * @param b second attribute
927 * @return whether this relation changed
928 */
929 public boolean add(int a, int b) {
930 BDDDomain d0 = (BDDDomain) domains.get(0);
931 Domain dd0 = getAttribute(0).getDomain();
932 solver.ensureCapacity(dd0, a);
933 BDD val = d0.ithVar(a);
934 BDDDomain d1 = (BDDDomain) domains.get(1);
935 Domain dd1 = getAttribute(1).getDomain();
936 solver.ensureCapacity(dd1, b);
937 val.andWith(d1.ithVar(b));
938 return add(val);
939 }
940
941 /***
942 * Add a triple to this relation.
943 *
944 * @param a first attribute
945 * @param b second attribute
946 * @param c third attribute
947 * @return whether this relation changed
948 */
949 public boolean add(int a, int b, int c) {
950 BDDDomain d0 = (BDDDomain) domains.get(0);
951 Domain dd0 = getAttribute(0).getDomain();
952 solver.ensureCapacity(dd0, a);
953 BDD val = d0.ithVar(a);
954 BDDDomain d1 = (BDDDomain) domains.get(1);
955 Domain dd1 = getAttribute(1).getDomain();
956 solver.ensureCapacity(dd1, b);
957 val.andWith(d1.ithVar(b));
958 BDDDomain d2 = (BDDDomain) domains.get(2);
959 Domain dd2 = getAttribute(2).getDomain();
960 solver.ensureCapacity(dd2, c);
961 val.andWith(d2.ithVar(c));
962 return add(val);
963 }
964
965
966
967
968 public boolean add(BigInteger[] tuple) {
969 BDD val = solver.bdd.universe();
970 for (int i = 0; i < tuple.length; ++i) {
971 final BDDDomain d = (BDDDomain) domains.get(i);
972 Domain dd = getAttribute(i).getDomain();
973 solver.ensureCapacity(dd, tuple[i]);
974 val.andWith(d.ithVar(tuple[i]));
975 }
976 return add(val);
977 }
978
979 /***
980 * Return the value of this relation in BDD form.
981 *
982 * @return BDD form of this relation
983 */
984 public BDD getBDD() {
985 return relation;
986 }
987
988 /***
989 * Set the value of this relation from the given BDD.
990 *
991 * @param b BDD value to set from
992 */
993 public void setBDD(BDD b) {
994 if (relation != null) relation.free();
995 relation = b;
996 }
997
998 /***
999 * Get the BDDDomain with the given index.
1000 *
1001 * @param i index
1002 * @return BDDDomain at that index
1003 */
1004 public BDDDomain getBDDDomain(int i) {
1005 return (BDDDomain) domains.get(i);
1006 }
1007
1008 /***
1009 * Get the BDDDomain that matches the given attribute, or
1010 * null if the attribute hasn't been assigned one yet.
1011 *
1012 * @param a attribute
1013 * @return BDDDomain that matches that attribute
1014 */
1015 public BDDDomain getBDDDomain(Attribute a) {
1016 int i = attributes.indexOf(a);
1017 if (i == -1 || domains == null) return null;
1018 return (BDDDomain) domains.get(i);
1019 }
1020
1021 /***
1022 * Get the attribute that is assigned to the given BDDDomain.
1023 *
1024 * @param d BDD domain
1025 * @return attribute
1026 */
1027 public Attribute getAttribute(BDDDomain d) {
1028 int i = domains.indexOf(d);
1029 if (i == -1) return null;
1030 return (Attribute) attributes.get(i);
1031 }
1032
1033 /***
1034 * Returns the list of BDD domains this relation is using.
1035 *
1036 * @return the list of BDDDomains this relation is using
1037 */
1038 public List getBDDDomains() {
1039 return domains;
1040 }
1041
1042
1043
1044
1045 public Relation copy() {
1046 List a = new LinkedList(attributes);
1047 Relation that = solver.createRelation(name + '\'', a);
1048 return that;
1049 }
1050
1051
1052
1053
1054 public void free() {
1055 if (relation != null) {
1056 relation.free();
1057 relation = null;
1058 }
1059
1060
1061
1062
1063
1064 }
1065
1066 /***
1067 * Do any onUpdate actions.
1068 * Called just after an update occurs.
1069 *
1070 * @param oldValue old value of relation
1071 */
1072 void doUpdate(BDD oldValue) {
1073 if (onUpdate != null) {
1074 for (Iterator i = onUpdate.iterator(); i.hasNext(); ) {
1075 CodeFragment f = (CodeFragment) i.next();
1076 f.invoke(this, oldValue);
1077 }
1078 }
1079 }
1080
1081 /***
1082 * Get the solver object.
1083 *
1084 * @return solver object
1085 */
1086 public BDDSolver getSolver() {
1087 return solver;
1088 }
1089
1090 /***
1091 * Set the BDD domain assignment of this relation to the given one.
1092 *
1093 * @param newdom new BDD domain assignment
1094 */
1095 public void setDomainAssignment(List newdom) {
1096 Assert._assert(newdom.size() == attributes.size());
1097 Assert._assert(new HashSet(newdom).size() == newdom.size(), newdom.toString());
1098 for (int i = 0; i < newdom.size(); ++i) {
1099 Domain d = ((Attribute) attributes.get(i)).getDomain();
1100 Assert._assert(solver.getBDDDomains(d).contains(newdom.get(i)));
1101 }
1102 this.domains = newdom;
1103 }
1104
1105
1106
1107
1108 public String verboseToString(){
1109 StringBuffer sb = new StringBuffer();
1110 sb.append(super.toString());
1111 sb.append('[');
1112 boolean any = false;
1113 for (Iterator it = getAttributes().iterator(); it.hasNext(); ){
1114 any = true;
1115 Attribute a = (Attribute) it.next();
1116 sb.append(a + ":");
1117 if (domains != null)
1118 sb.append(getBDDDomain(a));
1119 else
1120 sb.append(a.attributeDomain.toString());
1121 sb.append(',');
1122 }
1123 if (any)
1124 sb.deleteCharAt(sb.length() - 1);
1125 sb.append(']');
1126
1127 return sb.toString();
1128 }
1129 }