View Javadoc

1   // BDDRelation.java, created Mar 16, 2004 12:40:26 PM 2004 by jwhaley
2   // Copyright (C) 2004 John Whaley <jwhaley@alum.mit.edu>
3   // Licensed under the terms of the GNU LGPL; see COPYING for details.
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/*<BDDDomain>*/ domains;
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       * (non-Javadoc)
84       * Called before variable order is set.
85       * 
86       * @see net.sf.bddbddb.Relation#initialize()
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                     // use the given domain.
110                     if (!option.startsWith(fd.name)) throw new IllegalArgumentException("Attribute " + a + " has domain " + fd + ", but tried to assign "
111                         + option);
112                     //int index =
113                     // Integer.parseInt(option.substring(fd.name.length()));
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                     // find an applicable domain.
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) //(solver.TRACE)
196                 solver.out.println("Initializing value of special relation "+this+" "+d1+","+d2);
197             //Assert._assert(relation.isZero());
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; /* trivially true? */
303         BDDVarSet s = r.support();
304         calculateDomainSet();
305         BDDVarSet t = domainSet.union(s);
306         s.free();
307         //solver.out.println("Relation domains: " + domains + " BDD domains:" + activeDomains(r));
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     /* (non-Javadoc)
317      * @see net.sf.bddbddb.Relation#load()
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                 // Parse BDD information.
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     /* (non-Javadoc)
450      * @see net.sf.bddbddb.Relation#loadTuples()
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     /* (non-Javadoc)
554      * @see net.sf.bddbddb.Relation#loadTuples(java.lang.String)
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             // Load the header line.
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     /* (non-Javadoc)
622      * @see net.sf.bddbddb.Relation#save()
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     /* (non-Javadoc)
689      * @see net.sf.bddbddb.Relation#saveTuples()
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                         // Check if this is the universal set.
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     /* (non-Javadoc)
790      * @see net.sf.bddbddb.Relation#dsize()
791      */
792     public double dsize() {
793         calculateDomainSet();
794         return relation.satCount(domainSet);
795     }
796 
797     /* (non-Javadoc)
798      * @see net.sf.bddbddb.Relation#iterator()
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     /* (non-Javadoc)
839      * @see net.sf.bddbddb.Relation#iterator(int)
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     /* (non-Javadoc)
862      * @see net.sf.bddbddb.Relation#iterator(int, java.math.BigInteger)
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     /* (non-Javadoc)
874      * @see net.sf.bddbddb.Relation#iterator(java.math.BigInteger[])
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     /* (non-Javadoc)
889      * @see net.sf.bddbddb.Relation#contains(int, java.math.BigInteger)
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     /* (non-Javadoc)
966      * @see net.sf.bddbddb.Relation#add(java.math.BigInteger[])
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     /* (non-Javadoc)
1043      * @see net.sf.bddbddb.Relation#copy()
1044      */
1045     public Relation copy() {
1046         List a = new LinkedList(attributes);
1047         Relation that = solver.createRelation(name + '\'', a);
1048         return that;
1049     }
1050 
1051     /* (non-Javadoc)
1052      * @see net.sf.bddbddb.Relation#free()
1053      */
1054     public void free() {
1055         if (relation != null) {
1056             relation.free();
1057             relation = null;
1058         }
1059         /*
1060         if (domainSet != null) {
1061             domainSet.free();
1062             domainSet = null;
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     /* (non-Javadoc)
1106      * @see net.sf.bddbddb.Relation#verboseToString()
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 }