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.math.BigInteger;
14
15 /***
16 * FindBestOrder
17 *
18 * @author jwhaley
19 * @version $Id: FindBestOrder.java 452 2006-07-16 21:50:02Z joewhaley $
20 */
21 public class FindBestOrder {
22
23 static BDDFactory bdd = null;
24 boolean newbdd = true;
25 BDD b1 = null;
26 BDD b2 = null;
27 BDDVarSet b3 = null;
28
29 String filename0 = "fbo.bi";
30 String filename1 = "fbo.1";
31 String filename2 = "fbo.2";
32 String filename3 = "fbo.3";
33
34 /*** How long to delay for loading, in ms. */
35 long DELAY_TIME = Long.parseLong(System.getProperty("fbo.delaytime", "30000"));
36
37 /*** Factor how long to wait beyond the best time. */
38 float FACTOR = Float.parseFloat(System.getProperty("fbo.waitfactor", "1.1"));
39
40 BDDFactory.BDDOp op;
41 long bestCalcTime;
42 long bestTotalTime;
43 String bestOrder;
44
45 int nodeTableSize;
46 int cacheSize;
47 int maxIncrease;
48
49 File f0, f1, f2, f3;
50
51 public FindBestOrder(int nodeTableSize, int cacheSize, int maxIncrease,
52 long bestTime, long delayTime) {
53 this.bestCalcTime = bestTime;
54 this.bestTotalTime = Long.MAX_VALUE;
55
56 this.nodeTableSize = nodeTableSize;
57 this.cacheSize = cacheSize;
58 this.maxIncrease = maxIncrease;
59 this.DELAY_TIME = delayTime;
60 }
61
62 public void init(BDD b1, BDD b2, BDDVarSet dom, BDDFactory.BDDOp op) throws IOException {
63 this.op = op;
64 f0 = File.createTempFile("fbo", "a");
65 filename0 = f0.getAbsolutePath();
66 f0.deleteOnExit();
67 f1 = File.createTempFile("fbo", "b");
68 filename1 = f1.getAbsolutePath();
69 f1.deleteOnExit();
70 f2 = File.createTempFile("fbo", "c");
71 filename2 = f2.getAbsolutePath();
72 f2.deleteOnExit();
73 f3 = File.createTempFile("fbo", "d");
74 filename3 = f3.getAbsolutePath();
75 f3.deleteOnExit();
76
77 writeBDDConfig(b1.getFactory(), filename0);
78 b1.getFactory().save(filename1, b1);
79 b2.getFactory().save(filename2, b2);
80 dom.getFactory().save(filename3, dom.toBDD());
81
82 }
83
84 public void cleanup() {
85
86 f0.delete();
87 f1.delete();
88 f2.delete();
89 f3.delete();
90 if (b1 != null) b1.free();
91 if (b2 != null) b2.free();
92 if (b3 != null) b3.free();
93 }
94
95 public void writeBDDConfig(BDDFactory bdd, String fileName) throws IOException {
96 BufferedWriter dos = null;
97 try {
98 dos = new BufferedWriter(new FileWriter(fileName));
99 for (int i = 0; i < bdd.numberOfDomains(); ++i) {
100 BDDDomain d = bdd.getDomain(i);
101 dos.write(d.getName()+" "+d.size()+"\n");
102 }
103 } finally {
104 if (dos != null) dos.close();
105 }
106 }
107
108 public long tryOrder(boolean reverse, String varOrder) {
109 System.gc();
110 TryThread t = new TryThread();
111 t.reverse = reverse;
112 t.varOrderToTry = varOrder;
113 t.start();
114 try {
115 long waitTime = (long)(bestTotalTime*FACTOR) + DELAY_TIME;
116 if (waitTime < 0L) waitTime = Long.MAX_VALUE;
117 t.join(waitTime);
118 } catch (InterruptedException x) {
119 }
120 t.stop();
121 Thread.yield();
122 if (t.totalTime == Long.MAX_VALUE) {
123 System.out.println("Thread taking too long, aborted.");
124 System.out.print("Free memory: "+Runtime.getRuntime().freeMemory());
125 b1 = null;
126 b2 = null;
127 b3 = null;
128 bdd = null;
129 newbdd = true;
130 System.gc();
131 System.out.println(" bytes -> "+Runtime.getRuntime().freeMemory()+" bytes");
132 }
133 if (t.time < bestCalcTime) {
134 bestOrder = varOrder;
135 bestCalcTime = t.time;
136 if (t.totalTime < bestTotalTime)
137 bestTotalTime = t.totalTime;
138 }
139 return t.time;
140 }
141
142 public String getBestOrder() {
143 return bestOrder;
144 }
145
146 public long getBestTime() {
147 return bestCalcTime;
148 }
149
150 public class TryThread extends Thread {
151 boolean reverse;
152 String varOrderToTry;
153 long time = Long.MAX_VALUE;
154 long totalTime = Long.MAX_VALUE;
155
156 public void run() {
157 long total = System.currentTimeMillis();
158 if (bdd == null) {
159 bdd = JFactory.init(nodeTableSize, cacheSize);
160 bdd.setMaxIncrease(maxIncrease);
161 readBDDConfig(bdd);
162 }
163 int[] varorder = bdd.makeVarOrdering(reverse, varOrderToTry);
164 bdd.setVarOrder(varorder);
165
166 try {
167 if (newbdd) {
168 b1 = bdd.load(filename1);
169 b2 = bdd.load(filename2);
170 b3 = bdd.load(filename3).toVarSet();
171 newbdd = false;
172 }
173 long t = System.currentTimeMillis();
174 BDD result = b1.applyEx(b2, op, b3);
175 time = System.currentTimeMillis() - t;
176
177 result.free();
178 } catch (IOException x) {
179 }
180 System.out.println("Ordering: "+varOrderToTry+" time: "+time);
181
182 totalTime = System.currentTimeMillis() - total;
183 }
184
185 public void readBDDConfig(BDDFactory bdd) {
186 BufferedReader in = null;
187 try {
188 in = new BufferedReader(new FileReader(filename0));
189 for (;;) {
190 String s = in.readLine();
191 if (s == null || s.equals("")) break;
192 StringTokenizer st = new StringTokenizer(s);
193 String name = st.nextToken();
194 long size = Long.parseLong(st.nextToken())-1;
195 makeDomain(bdd, name, BigInteger.valueOf(size).bitLength());
196 }
197 } catch (IOException x) {
198 } finally {
199 if (in != null) try { in.close(); } catch (IOException _) { }
200 }
201 }
202
203 BDDDomain makeDomain(BDDFactory bdd, String name, int bits) {
204 BDDDomain d = bdd.extDomain(new long[] { 1L << bits })[0];
205 d.setName(name);
206 return d;
207 }
208 }
209 }