1
2
3
4 package joeq.Main;
5
6 import java.util.StringTokenizer;
7 import java.io.BufferedReader;
8 import java.io.FileReader;
9 import java.io.IOException;
10 import java.math.BigInteger;
11 import jwutil.util.Assert;
12 import net.sf.javabdd.BDD;
13 import net.sf.javabdd.BDDDomain;
14 import net.sf.javabdd.BDDFactory;
15 import net.sf.javabdd.JFactory;
16
17 /***
18 * FindBestPermutation
19 *
20 * @author jwhaley
21 * @version $Id: FindBestPermutation.java 2465 2006-06-07 23:03:17Z joewhaley $
22 */
23 public class FindBestPermutation extends Thread {
24
25 static long bestTime = Integer.MAX_VALUE;
26 static int bestNodeCount = Integer.MAX_VALUE;
27 static String bestOrdering;
28
29 boolean reverse;
30 String orderingToTry;
31 String filename;
32 int myNodeCount;
33
34 /***
35 * @param reverse
36 * @param orderingToTry
37 * @param filename
38 */
39 public FindBestPermutation(boolean reverse, String orderingToTry,
40 String filename) {
41 super();
42 this.reverse = reverse;
43 this.orderingToTry = orderingToTry;
44 this.filename = filename;
45 }
46
47 public void run() {
48 BDDFactory bdd = JFactory.init(1000000, 50000);
49
50 bdd.setIncreaseFactor(2);
51 readBDDConfig(bdd);
52 int[] varorder = bdd.makeVarOrdering(reverse, orderingToTry);
53 bdd.setVarOrder(varorder);
54
55 try {
56 BDD foo = bdd.load(filename);
57 myNodeCount = foo.nodeCount();
58 } catch (IOException x) {
59 }
60 System.out.println("Ordering: "+orderingToTry+" node count: "+myNodeCount+" vs. best "+bestNodeCount);
61 bdd.done();
62 }
63
64 static int N_ITER = 100;
65
66 public static void main(String[] args) {
67 String ordering = System.getProperty("bddordering");
68 boolean reverse = System.getProperty("bddnoreverse") == null;
69 String filename = args[0];
70
71
72 boolean flip = false;
73 boolean updated = true;
74 for (int i = 0; i < N_ITER; ++i) {
75 FindBestPermutation t = new FindBestPermutation(reverse, ordering, filename);
76 long time = System.currentTimeMillis();
77 t.start();
78 try {
79 t.join(bestTime + 1000);
80 } catch (InterruptedException e) {
81 }
82 if (t.myNodeCount == 0) {
83 try {
84 System.out.println("Thread timed out!");
85 t.stop();
86 System.gc();
87 System.out.println("Thread killed.");
88 Thread.sleep(100);
89 } catch (InterruptedException e2) { }
90 } else if (t.myNodeCount < bestNodeCount) {
91 bestNodeCount = t.myNodeCount;
92 bestOrdering = ordering;
93 bestTime = System.currentTimeMillis() - time;
94 System.out.println("New best: ordering = "+bestOrdering+" node count: "+bestNodeCount+" time: "+bestTime+" ms");
95 if (index1 != 0 || index2 != 0) updated = true;
96 }
97 if (flip) {
98 ordering = tweakInterleaving(bestOrdering);
99 System.out.println("Tweaked interleaving = "+ordering);
100 } else {
101 if (index1 == 0 && index2 == 0) {
102 if (!updated) {
103 break;
104 }
105 updated = false;
106 }
107 ordering = tweakOrdering(bestOrdering);
108 System.out.println("Tweaked ordering = "+ordering);
109 }
110 flip = !flip;
111 }
112 System.out.println("Best: ordering = "+bestOrdering+" node count: "+bestNodeCount+" time: "+bestTime+" ms");
113 }
114
115 public static void readBDDConfig(BDDFactory bdd) {
116 String fileName = System.getProperty("bddcfg", "bdd.cfg");
117 BufferedReader in = null;
118 try {
119 in = new BufferedReader(new FileReader(fileName));
120 for (;;) {
121 String s = in.readLine();
122 if (s == null || s.equals("")) break;
123 StringTokenizer st = new StringTokenizer(s);
124 String name = st.nextToken();
125 long size = Long.parseLong(st.nextToken())-1;
126 makeDomain(bdd, name, BigInteger.valueOf(size).bitLength());
127 }
128 in.close();
129 } catch (IOException x) {
130 } finally {
131 if (in != null) try { in.close(); } catch (IOException _) { }
132 }
133 }
134
135 static BDDDomain makeDomain(BDDFactory bdd, String name, int bits) {
136 Assert._assert(bits < 64);
137 BDDDomain d = bdd.extDomain(new long[] { 1L << bits })[0];
138 d.setName(name);
139
140 return d;
141 }
142
143 static int countDomains(String order) {
144 StringTokenizer st = new StringTokenizer(order, "x_");
145 int n = 1;
146 while (st.hasMoreTokens()) {
147 st.nextToken();
148 ++n;
149 }
150 return n;
151 }
152
153
154
155 static int index1, index2;
156
157 static String tweakOrdering(String ordering) {
158 StringTokenizer st = new StringTokenizer(ordering, "_");
159 int num = 0;
160 for (int i = 0; st.hasMoreTokens(); ++i) {
161 st.nextToken();
162 ++num;
163 }
164 st = new StringTokenizer(ordering, "_");
165 String[] a = new String[num];
166 for (int i = 0; i < a.length; ++i) {
167 a[i] = st.nextToken();
168 }
169 ++index2;
170 if (index2 == index1) ++index2;
171 if (index2 >= a.length) {
172 ++index1;
173 index2 = index1 + 1;
174 if (index1 >= a.length-1) {
175 index1 = 0;
176 }
177 if (index2 >= a.length) {
178 index2 = 0;
179 }
180 }
181 System.out.println("Swapping "+index1+" and "+index2);
182 String temp = a[index1];
183 a[index1] = a[index2];
184 a[index2] = temp;
185 StringBuffer sb = new StringBuffer();
186 for (int i = 0; i < a.length; ++i) {
187 sb.append(a[i]);
188 if (i < a.length - 1)
189 sb.append("_");
190 }
191 return sb.toString();
192 }
193
194 static int indexp;
195
196 static String tweakInterleaving(String ordering) {
197 StringBuffer sb = new StringBuffer();
198 StringTokenizer st = new StringTokenizer(ordering, "_x", true);
199 sb.append(st.nextToken());
200 for (int i = 0; i < indexp; ++i) {
201 sb.append(st.nextToken());
202 sb.append(st.nextToken());
203 }
204 if (!st.hasMoreTokens()) {
205 indexp = 0;
206 return sb.toString();
207 }
208 indexp++;
209 String s = st.nextToken();
210 if (s.equals("x")) sb.append("_");
211 else sb.append("x");
212 while (st.hasMoreTokens()) {
213 sb.append(st.nextToken());
214 }
215 return sb.toString();
216 }
217 }