1
2
3
4 package net.sf.javabdd;
5
6 import java.util.StringTokenizer;
7 import java.io.BufferedReader;
8 import java.io.BufferedWriter;
9 import java.io.File;
10 import java.io.FileReader;
11 import java.io.FileWriter;
12 import java.io.IOException;
13 import java.lang.reflect.Constructor;
14 import java.lang.reflect.Method;
15 import java.math.BigInteger;
16
17 /***
18 * TryVarOrder
19 *
20 * @author jwhaley
21 * @version $Id: TryVarOrder.java 452 2006-07-16 21:50:02Z joewhaley $
22 */
23 public class TryVarOrder {
24
25 /*** BDD Factory, reused if possible. */
26 static Object bdd = null;
27
28 static ClassLoader makeClassLoader() {
29
30 return ClassLoader.getSystemClassLoader();
31 }
32
33 /***
34 * Initialize the named BDD factory under a new class loader.
35 *
36 * @param s BDD factory to initialize
37 */
38 void initBDDFactory(String s) {
39 try {
40 ClassLoader cl;
41 if (bddoperation != null) cl = bddoperation.getClass().getClassLoader();
42 else cl = makeClassLoader();
43 Class c = cl.loadClass("net.sf.javabdd.BDDFactory");
44 Method m = c.getMethod("init", new Class[] { String.class, int.class, int.class });
45 bdd = m.invoke(null, new Object[] { s, new Integer(nodeTableSize), new Integer(cacheSize) });
46 m = c.getMethod("setMaxIncrease", new Class[] { int.class });
47 m.invoke(bdd, new Object[] { new Integer(maxIncrease) });
48
49 BufferedReader in = null;
50 try {
51 in = new BufferedReader(new FileReader(filename0));
52 for (;;) {
53 String s2 = in.readLine();
54 if (s2 == null || s2.equals("")) break;
55 StringTokenizer st = new StringTokenizer(s2);
56 String name = st.nextToken();
57 long size = Long.parseLong(st.nextToken())-1;
58 makeDomain(c, name, BigInteger.valueOf(size).bitLength());
59 }
60 } catch (IOException x) {
61 } finally {
62 if (in != null) try { in.close(); } catch (IOException _) { }
63 }
64 } catch (Exception x) {
65 System.err.println("Exception occurred while initializing BDD factory: "+x.getLocalizedMessage());
66 x.printStackTrace();
67 }
68 }
69
70 /***
71 * Destroy the BDD factory.
72 */
73 void destroyBDDFactory() {
74 if (bdd != null) {
75 Class c = bdd.getClass();
76 try {
77 Method m = c.getMethod("done", new Class[] { });
78 m.invoke(bdd, new Object[] { });
79 } catch (Exception x) {
80 System.err.println("Exception occurred while destroying BDD factory: "+x.getLocalizedMessage());
81 x.printStackTrace();
82 }
83 bdd = null;
84 }
85 }
86
87 void setBDDError(int code) {
88 Class c = bdd.getClass();
89 try {
90 Method m = c.getMethod("setError", new Class[] { int.class });
91 m.invoke(bdd, new Object[] { new Integer(code) });
92 } catch (Exception x) {
93 System.err.println("Exception occurred while setting error for BDD factory: "+x.getLocalizedMessage());
94 x.printStackTrace();
95 }
96 }
97
98 /***
99 * Make a domain in the BDD factory.
100 *
101 * @param c BDD factory class
102 * @param name name of domain
103 * @param bits bits in domain
104 * @throws Exception
105 */
106 static void makeDomain(Class c, String name, int bits) throws Exception {
107 Method m = c.getMethod("extDomain", new Class[] { long[].class });
108 Object[] ds = (Object[]) m.invoke(null, new Object[] { new long[] { 1L << bits } });
109 c = c.getClassLoader().loadClass("net.sf.javabdd.BDDDomain");
110 m = c.getMethod("setName", new Class[] { String.class });
111 m.invoke(ds[0], new Object[] { name });
112 }
113
114 Object bddoperation = null;
115
116 void initBDDOperation() throws Exception {
117 ClassLoader cl;
118 if (bdd != null) {
119 cl = bdd.getClass().getClassLoader();
120 } else {
121 cl = makeClassLoader();
122 }
123 Class bddop_class = cl.loadClass("net.sf.javabdd.TryVarOrder$BDDOperation");
124 Constructor c = bddop_class.getConstructor(new Class[0]);
125 bddoperation = c.newInstance(null);
126 Method m = bddop_class.getMethod("setOp", new Class[] { int.class });
127 m.invoke(bddoperation, new Object[] { new Integer(op.id) });
128 m = bddop_class.getMethod("setFilenames", new Class[] { String.class, String.class, String.class });
129 m.invoke(bddoperation, new Object[] { filename1, filename2, filename3 });
130 }
131
132 void setVarOrder(boolean reverse, String varOrderToTry) throws Exception {
133 Class bddop_class = bddoperation.getClass();
134 Method m = bddop_class.getMethod("setVarOrder", new Class[] { boolean.class, String.class });
135 m.invoke(bddoperation, new Object[] { Boolean.valueOf(reverse), varOrderToTry });
136 }
137
138 void load() throws Exception {
139 Class bddop_class = bddoperation.getClass();
140 Method m = bddop_class.getMethod("load", new Class[] { });
141 m.invoke(bddoperation, new Object[] { });
142 }
143
144 long doIt() throws Exception {
145 Class bddop_class = bddoperation.getClass();
146 Method m = bddop_class.getMethod("doIt", new Class[] { });
147 Long result = (Long) m.invoke(bddoperation, new Object[] { });
148 return result.longValue();
149 }
150
151 void free() throws Exception {
152 Class bddop_class = bddoperation.getClass();
153 Method m = bddop_class.getMethod("free", new Class[] { });
154 m.invoke(bddoperation, new Object[] { });
155 }
156
157 public static class BDDOperation {
158
159 public BDDOperation() { }
160
161 public BDDOperation(int op, String f1, String f2, String f3) {
162 setOp(op);
163 setFilenames(f1, f2, f3);
164 }
165
166 public void setOp(int op) {
167 switch (op) {
168 case 0: this.op = BDDFactory.and; break;
169 case 1: this.op = BDDFactory.xor; break;
170 case 2: this.op = BDDFactory.or; break;
171 case 3: this.op = BDDFactory.nand; break;
172 case 4: this.op = BDDFactory.nor; break;
173 case 5: this.op = BDDFactory.imp; break;
174 case 6: this.op = BDDFactory.biimp; break;
175 case 7: this.op = BDDFactory.diff; break;
176 case 8: this.op = BDDFactory.less; break;
177 case 9: this.op = BDDFactory.invimp; break;
178 default: throw new InternalError("Invalid op: "+op);
179 }
180 }
181
182 public void setFilenames(String f1, String f2, String f3) {
183 this.filename1 = f1;
184 this.filename2 = f2;
185 this.filename3 = f3;
186 }
187
188 /*** Operation for applyEx. */
189 BDDFactory.BDDOp op;
190
191 /*** Filenames for inputs. */
192 String filename1;
193 String filename2;
194 String filename3;
195
196 /*** Inputs to applyEx. */
197 BDD b1 = null;
198 BDD b2 = null;
199 BDDVarSet b3 = null;
200
201 public void setVarOrder(boolean reverse, String varOrderToTry) {
202 BDDFactory f = (BDDFactory) bdd;
203 int[] varorder = f.makeVarOrdering(reverse, varOrderToTry);
204 f.setVarOrder(varorder);
205 }
206
207 public void load() throws IOException {
208 BDDFactory f = (BDDFactory) bdd;
209 if (b1 == null) {
210 b1 = f.load(filename1);
211 b2 = f.load(filename2);
212 b3 = f.load(filename3).toVarSet();
213 }
214 }
215
216 public long doIt() {
217 long t = System.currentTimeMillis();
218 BDD result = b1.applyEx(b2, op, b3);
219 long time = System.currentTimeMillis() - t;
220 result.free();
221 return time;
222 }
223
224 public void free() {
225 b1.free(); b1 = null;
226 b2.free(); b2 = null;
227 b3.free(); b3 = null;
228 }
229
230 }
231
232 BDDFactory.BDDOp op;
233
234 /*** Filename for BDD config. */
235 String filename0;
236 /*** Filenames for inputs. */
237 String filename1;
238 String filename2;
239 String filename3;
240
241 /*** How long to delay for loading, in ms. */
242 long DELAY_TIME = Long.parseLong(System.getProperty("fbo.delaytime", "20000"));
243
244 /*** Factor how long to wait beyond the best time. */
245 float FACTOR = Float.parseFloat(System.getProperty("fbo.waitfactor", "1.1"));
246
247 /*** Best calc time so far. */
248 long bestCalcTime;
249 /*** Best varorder so far. */
250 String bestOrder;
251
252 /*** Initial node table size. */
253 int nodeTableSize;
254 /*** Initial cache size. */
255 int cacheSize;
256 /*** Initial max increase. */
257 int maxIncrease;
258
259 /*** File pointers for output and input BDDs. */
260 File f0, f1, f2, f3;
261
262 /*** Construct a new TryVarOrder. */
263 public TryVarOrder(int nodeTableSize, int cacheSize, int maxIncrease,
264 long bestTime, long delayTime) {
265 this.bestCalcTime = bestTime;
266
267 this.nodeTableSize = nodeTableSize;
268 this.cacheSize = cacheSize;
269 this.maxIncrease = maxIncrease;
270 this.DELAY_TIME = delayTime;
271 }
272
273 /***
274 * Initialize for a new trial.
275 * Takes the given input BDDs and saves them out to temporary files.
276 *
277 * @param b1 first input to applyEx
278 * @param b2 second input to applyEx
279 * @param dom third input to applyEx
280 * @param op operation to be passed to applyEx
281 * @throws IOException
282 */
283 public void init(BDD b1, BDD b2, BDD dom, BDDFactory.BDDOp op) throws IOException {
284 this.op = op;
285 f0 = File.createTempFile("fbo", "a");
286 filename0 = f0.getAbsolutePath();
287 f0.deleteOnExit();
288 f1 = File.createTempFile("fbo", "b");
289 filename1 = f1.getAbsolutePath();
290 f1.deleteOnExit();
291 f2 = File.createTempFile("fbo", "c");
292 filename2 = f2.getAbsolutePath();
293 f2.deleteOnExit();
294 f3 = File.createTempFile("fbo", "d");
295 filename3 = f3.getAbsolutePath();
296 f3.deleteOnExit();
297
298 writeBDDConfig(b1.getFactory(), filename0);
299 b1.getFactory().save(filename1, b1);
300 b2.getFactory().save(filename2, b2);
301 dom.getFactory().save(filename3, dom);
302
303 try {
304 initBDDOperation();
305 } catch (Exception x) {
306 System.err.println("Exception occurred while initializing: "+x.getLocalizedMessage());
307 x.printStackTrace();
308 }
309 }
310
311 /***
312 * Clean up the temporary files.
313 */
314 public void cleanup() {
315
316 try {
317 f0.delete();
318 f1.delete();
319 f2.delete();
320 f3.delete();
321 free();
322 } catch (Exception x) {
323 System.err.println("Exception occurred while cleaning up: "+x.getLocalizedMessage());
324 x.printStackTrace();
325 }
326 }
327
328 /***
329 * Write the BDD configuration to a file.
330 *
331 * @param bdd BDD factory
332 * @param fileName filename
333 * @throws IOException
334 */
335 public void writeBDDConfig(BDDFactory bdd, String fileName) throws IOException {
336 BufferedWriter dos = null;
337 try {
338 dos = new BufferedWriter(new FileWriter(fileName));
339 for (int i = 0; i < bdd.numberOfDomains(); ++i) {
340 BDDDomain d = bdd.getDomain(i);
341 dos.write(d.getName()+" "+d.size()+"\n");
342 }
343 } finally {
344 if (dos != null) dos.close();
345 }
346 }
347
348 /***
349 * Try out a variable order.
350 *
351 * @param reverse whether to reverse the bits
352 * @param varOrder variable order to try
353 * @return time spent, or Long.MAX_VALUE if it didn't terminate
354 */
355 public long tryOrder(String factory, boolean reverse, String varOrder) {
356 if (bdd == null) initBDDFactory(factory);
357
358 TryThread t = new TryThread(reverse, varOrder);
359 t.start();
360 try {
361 t.join(DELAY_TIME);
362 if (t.initTime >= 0L) {
363 t.join((long)(bestCalcTime*FACTOR));
364 }
365 } catch (InterruptedException x) {
366 }
367 if (t.isAlive()) {
368 setBDDError(1);
369 try {
370 t.join();
371 } catch (InterruptedException x) {
372 }
373 System.out.print("Free memory: "+Runtime.getRuntime().freeMemory());
374 destroyBDDFactory();
375 System.gc();
376 System.out.println(" bytes -> "+Runtime.getRuntime().freeMemory()+" bytes");
377 }
378 if (t.computeTime < 0) {
379 if (t.initTime < 0) {
380
381 System.out.println("BDD factory took too long to initialize, aborted.");
382 } else {
383 System.out.println("Took too long to compute, aborted.");
384 }
385 } else if (t.computeTime < bestCalcTime) {
386 bestOrder = varOrder;
387 bestCalcTime = t.computeTime;
388 }
389 return t.computeTime;
390 }
391
392 public String getBestOrder() {
393 return bestOrder;
394 }
395
396 public long getBestTime() {
397 return bestCalcTime;
398 }
399
400 public class TryThread extends Thread {
401 boolean reverse;
402 String varOrderToTry;
403 long initTime = -1;
404 long computeTime = -1;
405
406 TryThread(boolean r, String v) {
407 reverse = r;
408 varOrderToTry = v;
409 }
410
411 public void run() {
412
413 try {
414 long time = System.currentTimeMillis();
415 setVarOrder(reverse, varOrderToTry);
416 load();
417 initTime = time - System.currentTimeMillis();
418 computeTime = doIt();
419 free();
420 System.out.println("Ordering: "+varOrderToTry+" init: "+initTime+" compute: "+computeTime);
421 } catch (Exception x) {
422 System.err.println("Exception occurred while trying order: "+x.getLocalizedMessage());
423 x.printStackTrace();
424 }
425 }
426
427 }
428
429 }