1
2
3
4 package net.sf.bddbddb;
5
6 import java.util.ArrayList;
7 import java.util.Collections;
8 import java.util.HashMap;
9 import java.util.Iterator;
10 import java.util.LinkedList;
11 import java.util.List;
12 import java.util.Map;
13 import java.util.StringTokenizer;
14 import java.io.BufferedReader;
15 import java.io.FileReader;
16 import java.io.IOException;
17 import java.math.BigInteger;
18 import jwutil.collections.EntryValueComparator;
19 import jwutil.io.SystemProperties;
20 import net.sf.bddbddb.order.Order;
21 import net.sf.bddbddb.order.OrderConstraint;
22 import net.sf.bddbddb.order.OrderConstraintSet;
23 import net.sf.bddbddb.order.OrderIterator;
24 import net.sf.javabdd.BDD;
25 import net.sf.javabdd.BDDDomain;
26 import net.sf.javabdd.BDDFactory;
27 import net.sf.javabdd.BDDVarSet;
28 import net.sf.javabdd.FindBestOrder;
29
30 public class TryDomainOrders {
31
32 BDDSolver solver;
33 List domList;
34 String varorder;
35 OrderConstraintSet loaded_varorder;
36
37 public TryDomainOrders() {
38 solver = new BDDSolver();
39 domList = new ArrayList();
40 varorder = solver.VARORDER;
41 loaded_varorder = new OrderConstraintSet();
42 }
43
44 BDDRelation parseRelation(String name, BufferedReader in) throws IOException {
45 String s = in.readLine();
46 if (!s.startsWith("# ")) {
47
48 throw new IOException("no header line");
49 }
50 StringTokenizer st = new StringTokenizer(s.substring(2));
51 List attribs = new LinkedList();
52 List bdddoms = new LinkedList();
53 while (st.hasMoreTokens()) {
54 String msg = null;
55 String dname = st.nextToken(": ");
56 int dbits = Integer.parseInt(st.nextToken());
57 String fdname = dname;
58 while (fdname.length() > 0 &&
59 Character.isDigit(fdname.charAt(fdname.length()-1))) {
60 fdname = fdname.substring(0, fdname.length()-1);
61 }
62 Domain fd = solver.getDomain(fdname);
63 if (fd == null) {
64 fd = new Domain(fdname, BigInteger.ONE.shiftLeft(dbits).subtract(BigInteger.ONE));
65 solver.nameToDomain.put(fdname, fd);
66 } else {
67 if (dbits != fd.getSize().bitLength())
68 throw new IOException("different number of bits for "+fd+" ("+dbits+" vs "+
69 fd.getSize().bitLength()+")");
70 }
71 BDDDomain d = solver.getBDDDomain(dname);
72 while (d == null) {
73 BDDDomain dom = solver.allocateBDDDomain(fd);
74 if (dom.getName().equals(dname)) {
75 d = dom;
76 domList.add(dom);
77 break;
78 }
79 }
80 bdddoms.add(d);
81 Attribute a = new Attribute(dname, fd, dname);
82 attribs.add(a);
83 }
84 Relation r = solver.createRelation(name, attribs);
85 solver.out.println("Relation "+r+": "+attribs);
86
87
88 int[][] domvars = new int[bdddoms.size()][];
89 int k = 0;
90 for (Iterator i = bdddoms.iterator(); i.hasNext(); ++k) {
91 BDDDomain d = (BDDDomain) i.next();
92 s = in.readLine();
93 if (!s.startsWith("# "))
94 throw new IOException("missing variable line for domain "+d);
95 s = s.substring(2);
96 domvars[k] = new int[d.varNum()];
97 st = new StringTokenizer(s);
98 for (int j = 0; j < domvars[k].length; ++j) {
99 if (!st.hasMoreTokens())
100 throw new IOException("not enough variables for domain "+d);
101 domvars[k][j] = Integer.parseInt(st.nextToken());
102 }
103 if (st.hasMoreTokens())
104 throw new IOException("too many variables for domain "+d);
105 }
106
107 s = in.readLine();
108 st = new StringTokenizer(s);
109 int nNodes = Integer.parseInt(st.nextToken());
110 int nVars = Integer.parseInt(st.nextToken());
111
112 s = in.readLine();
113 st = new StringTokenizer(s);
114 int[] varorder = new int[nVars];
115 for (k = 0; k < varorder.length; ++k) {
116 if (!st.hasMoreTokens())
117 throw new IOException("varorder line too short");
118 varorder[k] = Integer.parseInt(st.nextToken());
119 }
120 if (st.hasMoreTokens())
121 throw new IOException("varorder line too long");
122
123 for (int a = 0; a < domvars.length; ++a) {
124 BDDDomain adom = (BDDDomain)bdddoms.get(a);
125 int[] a_vars = domvars[a];
126 int a1 = varorder[a_vars[0]];
127 int a2 = varorder[a_vars[a_vars.length-1]];
128 int a_start = Math.min(a1, a2);
129 int a_end = Math.max(a1, a2);
130 for (int b = a+1; b < domvars.length; ++b) {
131 BDDDomain bdom = (BDDDomain)bdddoms.get(b);
132 int[] b_vars = domvars[b];
133 int b1 = varorder[b_vars[0]];
134 int b2 = varorder[b_vars[b_vars.length-1]];
135 int b_start = Math.min(b1, b2);
136 int b_end = Math.max(b1, b2);
137 OrderConstraint c;
138 if (a_start > b_end) {
139 c = OrderConstraint.makePrecedenceConstraint(bdom, adom);
140 } else if (b_start > a_end) {
141 c = OrderConstraint.makePrecedenceConstraint(adom, bdom);
142 } else {
143 c = OrderConstraint.makeInterleaveConstraint(adom, bdom);
144 }
145 solver.out.println("Order constraint: "+c);
146 boolean ok = loaded_varorder.constrain(c);
147 if (!ok)
148 solver.out.println("Note: order conflicts! cannot add constraint "+c);
149 }
150 }
151 return (BDDRelation) r;
152 }
153
154 BDDRelation parseRelation(String filename) throws IOException {
155
156 int x = Math.max(filename.lastIndexOf('/'),
157 filename.lastIndexOf(SystemProperties.getProperty("file.separator")));
158 int y = filename.lastIndexOf('.');
159 if (x >= y)
160 throw new IOException("bad filename: "+filename);
161 String relationName = filename.substring(x+1, y);
162 String suffixName = filename.substring(y+1);
163 BufferedReader in = null;
164 try {
165 in = new BufferedReader(new FileReader(filename));
166
167 return parseRelation(relationName, in);
168 } finally {
169 if (in != null) try { in.close(); } catch (IOException _) { }
170 }
171 }
172
173 void setVarOrder(OrderConstraintSet ocs) {
174 if (varorder == null) {
175 Order o = ocs.generateRandomOrder(domList);
176 solver.VARORDER = o.toVarOrderString(null);
177 } else {
178 solver.VARORDER = varorder;
179 }
180 solver.setVariableOrdering();
181 }
182
183 void doApplyEx(BDDFactory.BDDOp op, BDD b1, BDD b2, BDDVarSet b3) {
184 long time = System.currentTimeMillis();
185 FindBestOrder fbo = new FindBestOrder(solver.BDDNODES, solver.BDDCACHE, 0, Long.MAX_VALUE, 5000);
186 try {
187 fbo.init(b1, b2, b3, op);
188 } catch (IOException x) {
189 solver.err.println("IO Exception occurred: " + x);
190 fbo.cleanup();
191 return;
192 }
193 solver.out.println("Time to initialize FindBestOrder: "+(System.currentTimeMillis()-time));
194
195 Map orderTimes = new HashMap();
196 if (true) {
197 Order o = loaded_varorder.generateRandomOrder(domList);
198 String vOrder = o.toVarOrderString(null);
199 solver.out.println("Trying initial order "+vOrder);
200 vOrder = solver.fixVarOrder(vOrder, false);
201 solver.out.println("Complete order "+vOrder);
202 time = fbo.tryOrder(true, vOrder);
203 time = Math.min(time, BDDInferenceRule.LONG_TIME);
204 solver.out.println("Order "+o+" time: "+time+" ms");
205 orderTimes.put(o, new Long(time));
206 }
207
208 OrderIterator i = new OrderIterator(domList);
209 while (i.hasNext()) {
210 Order o = i.nextOrder();
211 String vOrder = o.toVarOrderString(null);
212 solver.out.println("Trying order "+vOrder);
213 vOrder = solver.fixVarOrder(vOrder, false);
214 solver.out.println("Complete order "+vOrder);
215 time = fbo.tryOrder(true, vOrder);
216 time = Math.min(time, BDDInferenceRule.LONG_TIME);
217 solver.out.println("Order "+o+" time: "+time+" ms");
218 orderTimes.put(o, new Long(time));
219 }
220 fbo.cleanup();
221
222 List sortedEntries = new ArrayList(orderTimes.entrySet());
223 Collections.sort(sortedEntries, EntryValueComparator.INSTANCE);
224 for (Iterator it = sortedEntries.iterator(); it.hasNext(); ) {
225 Map.Entry e = (Map.Entry) it.next();
226 Order o = (Order) e.getKey();
227 Long t = (Long) e.getValue();
228 if (t.longValue() >= BDDInferenceRule.LONG_TIME) break;
229 solver.out.println("Order: "+o+" "+t+" ms");
230 }
231 }
232
233 void handleCommand(String[] args) throws IOException {
234 if (args.length > 1) {
235 if (args[0].equals("relprod")) {
236 if (args.length == 4 || args.length == 2) {
237 String rn1, rn2, rn3;
238 if (args.length == 4) {
239 rn1 = args[1]; rn2 = args[2]; rn3 = args[3];
240 } else {
241 rn1 = args[1]+"_op1.bdd";
242 rn2 = args[1]+"_op2.bdd";
243 rn3 = args[1]+"_op3.bdd";
244 }
245 BDDRelation r1 = parseRelation(rn1);
246 BDDRelation r2 = parseRelation(rn2);
247 BDDRelation r3 = parseRelation(rn3);
248 setVarOrder(loaded_varorder);
249 solver.initialize();
250 r1.load(rn1);
251 r2.load(rn2);
252 r3.load(rn3);
253 doApplyEx(BDDFactory.and, r1.getBDD(), r2.getBDD(), r3.getBDD().toVarSet());
254 return;
255 }
256 } else if (args[0].equals("and")) {
257
258 } else if (args[0].equals("or")) {
259
260 }
261 }
262 solver.out.println("Usage: java "+TryDomainOrders.class.getName()+" relprod bdd1 bdd2 bdd3");
263 solver.out.println(" java "+TryDomainOrders.class.getName()+" and bdd1 bdd2");
264 solver.out.println(" java "+TryDomainOrders.class.getName()+" or bdd1 bdd2");
265 }
266
267 /***
268 * @param args
269 */
270 public static void main(String[] args) throws IOException {
271 TryDomainOrders dis = new TryDomainOrders();
272 dis.handleCommand(args);
273 }
274 }