View Javadoc

1   // TryVarOrder.java, created Apr 2, 2004 10:43:21 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.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          //return HijackingClassLoader.makeClassLoader();
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         //this.nodeTableSize = b1.getFactory().getAllocNum();
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         //System.out.print("Writing BDDs to files...");
298         writeBDDConfig(b1.getFactory(), filename0);
299         b1.getFactory().save(filename1, b1);
300         b2.getFactory().save(filename2, b2);
301         dom.getFactory().save(filename3, dom);
302         //System.out.println("done.");
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         //System.out.println("Cleaning up temporary files.");
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         //System.gc();
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                 // Couldn't even initialize in time!
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             //System.out.println("\nTrying ordering "+varOrderToTry);
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 }