1
2
3
4 package net.sf.bddbddb;
5
6 import java.util.Iterator;
7 import java.util.List;
8 import java.io.BufferedReader;
9 import java.io.BufferedWriter;
10 import java.io.FileReader;
11 import java.io.FileWriter;
12 import java.io.IOException;
13 import jwutil.collections.IndexMap;
14 import jwutil.collections.Pair;
15 import net.sf.javabdd.BDD;
16 import net.sf.javabdd.BDDDomain;
17
18 /***
19 * Utility to build equivalence relations between multiple domains.
20 *
21 * @author jwhaley
22 * @version $Id: BuildEquivalenceRelation.java 549 2005-05-17 10:17:33Z joewhaley $
23 */
24 public class BuildEquivalenceRelation {
25
26 public static void main(String[] args) throws Exception {
27 int n = args.length / 2;
28
29 BDDDomain[] domains = new BDDDomain[n];
30 long[] sizes = new long[n];
31 BDDDomain targetDomain;
32
33 BDDSolver s = new BDDSolver();
34 DatalogParser parser = new DatalogParser(s);
35 parser.readDatalogProgram(s.basedir+"fielddomains.pa");
36 System.out.println("Domains: "+s.nameToDomain);
37 s.loadBDDDomainInfo();
38 s.setVariableOrdering();
39
40 targetDomain = s.getBDDDomain(args[0]);
41 if (targetDomain == null) throw new Exception("Invalid domain: "+args[0]);
42 for (int i = 0; i < domains.length; ++i) {
43 String name = args[i*2 + 1];
44 domains[i] = s.getBDDDomain(name);
45 if (domains[i] == null)
46 throw new Exception("Invalid domain: "+args[0]);
47 String size = args[i*2 + 2];
48 try {
49 sizes[i] = Long.parseLong(size);
50 } catch (NumberFormatException x) {
51 BufferedReader in = new BufferedReader(new FileReader(s.basedir+size));
52 IndexMap m = IndexMap.loadStringMap("map", in);
53 in.close();
54 sizes[i] = m.size();
55 }
56 }
57
58 long index = 0;
59 for (int i = 0; i < domains.length; ++i) {
60 int bits = Math.min(domains[i].varNum(), targetDomain.varNum());
61 BDD b = domains[i].buildAdd(targetDomain, bits, index);
62 b.andWith(domains[i].varRange(0, sizes[i]));
63 System.out.println(domains[i]+" [0.."+sizes[i]+"] corresponds to "+targetDomain+"["+index+".."+(index+sizes[i])+"]");
64 System.out.println("Result: "+b.nodeCount()+" nodes");
65 bdd_save("map_"+domains[i]+"_"+targetDomain+".bdd", b, new Pair(domains[i], targetDomain));
66 index += sizes[i] + 1;
67 }
68 }
69
70 public static void bdd_save(String filename, BDD b, List ds) throws IOException {
71 BufferedWriter out = null;
72 try {
73 out = new BufferedWriter(new FileWriter(filename));
74 out.write('#');
75 for (Iterator i = ds.iterator(); i.hasNext(); ) {
76 BDDDomain d = (BDDDomain) i.next();
77 out.write(' ');
78 out.write(d.getName());
79 out.write(':');
80 out.write(Integer.toString(d.varNum()));
81 }
82 out.write('\n');
83 for (Iterator i = ds.iterator(); i.hasNext(); ) {
84 BDDDomain d = (BDDDomain) i.next();
85 out.write('#');
86 int[] vars = d.vars();
87 for (int j = 0; j < vars.length; ++j) {
88 out.write(' ');
89 out.write(Integer.toString(vars[j]));
90 }
91 out.write('\n');
92 }
93 b.getFactory().save(out, b);
94 } finally {
95 if (out != null) try { out.close(); } catch (IOException _) { }
96 }
97 }
98
99 }