1
2
3
4 package net.sf.javabdd;
5
6 import java.util.Arrays;
7 import java.io.File;
8 import java.io.FileInputStream;
9 import java.io.FileOutputStream;
10 import java.io.IOException;
11
12 /***
13 * <p>An implementation of BDDFactory that relies on the BuDDy library through a
14 * native interface. You can use this by calling the "BuDDyFactory.init()"
15 * method with the desired arguments. This will return you an instance of the
16 * BDDFactory class that you can use. Call "done()" on that instance when you
17 * are finished.</p>
18 *
19 * <p>This class (and the BuDDy library) do NOT support multithreading.
20 * Furthermore, there can be only one instance active at a time. You can only
21 * call "init()" again after you have called "done()" on the original instance.
22 * It is not recommended to call "init()" again after calling "done()" unless
23 * you are _completely_ sure that all BDD objects that reference the old
24 * factory have been freed.</p>
25 *
26 * <p>If you really need multiple BDD factories, consider using the JFactory
27 * class for the additional BDD factories --- JFactory can have multiple
28 * factory instances active at a time.</p>
29 *
30 * @see net.sf.javabdd.BDDFactory
31 *
32 * @author John Whaley
33 * @version $Id: BuDDyFactory.java 476 2007-03-06 06:08:40Z joewhaley $
34 */
35 public class BuDDyFactory extends BDDFactoryIntImpl {
36
37 public static BDDFactory init(int nodenum, int cachesize) {
38 BuDDyFactory f = new BuDDyFactory();
39 f.initialize(nodenum, cachesize);
40 return f;
41 }
42
43 /***
44 * Single factory instance. Only one factory object is enabled at a time.
45 */
46 private static BuDDyFactory INSTANCE;
47
48 static {
49 String libname = getProperty("buddylib", "buddy");
50 try {
51 System.loadLibrary(libname);
52 } catch (java.lang.UnsatisfiedLinkError x) {
53
54 libname = System.mapLibraryName(libname);
55 String currentdir = getProperty("user.dir", ".");
56 String sep = getProperty("file.separator", "/");
57 String filename = currentdir+sep+libname;
58 try {
59 System.load(filename);
60 } catch (java.lang.UnsatisfiedLinkError y) {
61 File f = new File(filename);
62 if (!f.exists()) throw y;
63
64 try {
65 File f2 = File.createTempFile("buddy", ".dll");
66 copyFile(f, f2);
67 f2.deleteOnExit();
68 System.out.println("buddy.dll is in use, linking temporary copy "+f2);
69 System.load(f2.getAbsolutePath());
70 } catch (IOException z) {
71 throw y;
72 }
73 }
74 }
75 registerNatives();
76 }
77
78 private static void copyFile(File in, File out) throws IOException {
79 FileInputStream fis = new FileInputStream(in);
80 FileOutputStream fos = new FileOutputStream(out);
81 byte[] buf = new byte[1024];
82 int i = 0;
83 while ((i = fis.read(buf)) != -1) {
84 fos.write(buf, 0, i);
85 }
86 fis.close();
87 fos.close();
88 }
89
90 private static native void registerNatives();
91
92 private BuDDyFactory() {}
93
94 /*** An invalid id, for use in invalidating BDDs. */
95 static final int INVALID_BDD = -1;
96
97
98
99 protected void addref_impl(int v) { addRef(v); }
100 private static native void addRef(int b);
101 protected void delref_impl(int v) { delRef(v); }
102 private static native void delRef(int b);
103 protected int zero_impl() { return 0; }
104 protected int one_impl() { return 1; }
105 protected int invalid_bdd_impl() { return INVALID_BDD; }
106 protected int var_impl(int v) { return var0(v); }
107 private static native int var0(int b);
108 protected int level_impl(int v) { return var2Level0(var0(v)); }
109 protected int low_impl(int v) { return low0(v); }
110 private static native int low0(int b);
111 protected int high_impl(int v) { return high0(v); }
112 private static native int high0(int b);
113 protected int ithVar_impl(int var) { return ithVar0(var); }
114 private static native int ithVar0(int var);
115 protected int nithVar_impl(int var) { return nithVar0(var); }
116 private static native int nithVar0(int var);
117
118 protected int makenode_impl(int lev, int lo, int hi) { return ite0(ithVar_impl(level2Var0(lev)), hi, lo); }
119 protected int ite_impl(int v1, int v2, int v3) { return ite0(v1, v2, v3); }
120 private static native int ite0(int b, int c, int d);
121 protected int apply_impl(int v1, int v2, BDDOp opr) { return apply0(v1, v2, opr.id); }
122 private static native int apply0(int b, int c, int opr);
123 protected int not_impl(int v1) { return not0(v1); }
124 private static native int not0(int b);
125 protected int applyAll_impl(int v1, int v2, BDDOp opr, int v3) { return applyAll0(v1, v2, opr.id, v3); }
126 private static native int applyAll0(int b, int c, int opr, int d);
127 protected int applyEx_impl(int v1, int v2, BDDOp opr, int v3) { return applyEx0(v1, v2, opr.id, v3); }
128 private static native int applyEx0(int b, int c, int opr, int d);
129 protected int applyUni_impl(int v1, int v2, BDDOp opr, int v3) { return applyUni0(v1, v2, opr.id, v3); }
130 private static native int applyUni0(int b, int c, int opr, int d);
131 protected int compose_impl(int v1, int v2, int var) { return compose0(v1, v2, var); }
132 private static native int compose0(int b, int c, int var);
133 protected int constrain_impl(int v1, int v2) { return constrain0(v1, v2); }
134 private static native int constrain0(int b, int c);
135 protected int restrict_impl(int v1, int v2) { return restrict0(v1, v2); }
136 private static native int restrict0(int b, int var);
137 protected int simplify_impl(int v1, int v2) { return simplify0(v1, v2); }
138 private static native int simplify0(int b, int d);
139 protected int support_impl(int v) { return support0(v); }
140 private static native int support0(int b);
141 protected int exist_impl(int v1, int v2) { return exist0(v1, v2); }
142 private static native int exist0(int b, int var);
143 protected int forAll_impl(int v1, int v2) { return forAll0(v1, v2); }
144 private static native int forAll0(int b, int var);
145 protected int unique_impl(int v1, int v2) { return unique0(v1, v2); }
146 private static native int unique0(int b, int var);
147 protected int fullSatOne_impl(int v) { return fullSatOne0(v); }
148 private static native int fullSatOne0(int b);
149
150 protected int replace_impl(int v, BDDPairing p) { return replace0(v, unwrap(p)); }
151 private static native int replace0(int b, long p);
152 protected int veccompose_impl(int v, BDDPairing p) { return veccompose0(v, unwrap(p)); }
153 private static native int veccompose0(int b, long p);
154
155 protected int nodeCount_impl(int v) { return nodeCount0(v); }
156 private static native int nodeCount0(int b);
157 protected double pathCount_impl(int v) { return pathCount0(v); }
158 private static native double pathCount0(int b);
159 protected double satCount_impl(int v) { return satCount0(v); }
160 private static native double satCount0(int b);
161 protected int satOne_impl(int v) { return satOne0(v); }
162 private static native int satOne0(int b);
163 protected int satOne_impl2(int v1, int v2, boolean pol) { return satOne1(v1, v2, pol?1:0); }
164 private static native int satOne1(int b, int c, int d);
165 protected int nodeCount_impl2(int[] v) { return nodeCount1(v); }
166 private static native int nodeCount1(int[] a);
167 protected int[] varProfile_impl(int v) { return varProfile0(v); }
168 private static native int[] varProfile0(int b);
169 protected void printTable_impl(int v) { printTable0(v); }
170 private static native void printTable0(int b);
171
172
173
174 public void addVarBlock(int first, int last, boolean fixed) { addVarBlock1(first, last, fixed); }
175 private static native void addVarBlock1(int first, int last, boolean fixed);
176 public void varBlockAll() { varBlockAll0(); }
177 private static native void varBlockAll0();
178 public void clearVarBlocks() { clearVarBlocks0(); }
179 private static native void clearVarBlocks0();
180 public void printOrder() { printOrder0(); }
181 private static native void printOrder0();
182 public int getNodeTableSize() { return getAllocNum0(); }
183 private static native int getAllocNum0();
184 public int getNodeNum() { return getNodeNum0(); }
185 private static native int getNodeNum0();
186 public int getCacheSize() { return getCacheSize0(); }
187 private static native int getCacheSize0();
188 public int reorderGain() { return reorderGain0(); }
189 private static native int reorderGain0();
190 public void printStat() { printStat0(); }
191 private static native void printStat0();
192 public void printAll() { printAll0(); }
193 private static native void printAll0();
194 public void setVarOrder(int[] neworder) { setVarOrder0(neworder); }
195 private static native void setVarOrder0(int[] neworder);
196 public int level2Var(int level) { return level2Var0(level); }
197 private static native int level2Var0(int level);
198 public int var2Level(int var) { return var2Level0(var); }
199 private static native int var2Level0(int var);
200 public int getReorderTimes() { return getReorderTimes0(); }
201 private static native int getReorderTimes0();
202 public void disableReorder() { disableReorder0(); }
203 private static native void disableReorder0();
204 public void enableReorder() { enableReorder0(); }
205 private static native void enableReorder0();
206 public int reorderVerbose(int v) { return reorderVerbose0(v); }
207 private static native int reorderVerbose0(int v);
208 public void reorder(ReorderMethod m) { reorder0(m.id); }
209 private static native void reorder0(int method);
210 public void autoReorder(ReorderMethod method) { autoReorder0(method.id); }
211 private static native void autoReorder0(int method);
212 public void autoReorder(ReorderMethod method, int max) { autoReorder1(method.id, max); }
213 private static native void autoReorder1(int method, int max);
214 public void swapVar(int v1, int v2) { swapVar0(v1, v2); }
215 private static native void swapVar0(int v1, int v2);
216
217
218
219
220 protected void initialize(int nodenum, int cachesize) {
221 if (INSTANCE != null)
222 throw new InternalError("Error: BDDFactory already initialized.");
223 INSTANCE = this;
224 initialize0(nodenum, cachesize);
225 }
226 private static native void initialize0(int nodenum, int cachesize);
227
228
229
230
231 public boolean isInitialized() {
232 return isInitialized0();
233 }
234 private static native boolean isInitialized0();
235
236
237
238
239 public void done() {
240 super.done();
241 INSTANCE = null;
242 done0();
243 }
244 private static native void done0();
245
246
247
248
249 public void setError(int code) {
250 setError0(code);
251 }
252 private static native void setError0(int code);
253
254
255
256
257 public void clearError() {
258 clearError0();
259 }
260 private static native void clearError0();
261
262
263
264
265 public int setMaxNodeNum(int size) {
266 return setMaxNodeNum0(size);
267 }
268 private static native int setMaxNodeNum0(int size);
269
270
271
272
273 public double setMinFreeNodes(double x) {
274 return setMinFreeNodes0((int)(x * 100.)) / 100.;
275 }
276 private static native int setMinFreeNodes0(int x);
277
278
279
280
281 public int setMaxIncrease(int x) {
282 return setMaxIncrease0(x);
283 }
284 private static native int setMaxIncrease0(int x);
285
286
287
288
289 public double setIncreaseFactor(double x) {
290 return setIncreaseFactor0(x);
291 }
292 private static native double setIncreaseFactor0(double x);
293
294
295
296
297 public double setCacheRatio(double x) {
298 return setCacheRatio0((int)x);
299 }
300 private static native int setCacheRatio0(int x);
301
302
303
304
305 public int setNodeTableSize(int x) {
306 return setNodeTableSize0(x);
307 }
308 private static native int setNodeTableSize0(int x);
309
310
311
312
313 public int setCacheSize(int x) {
314 return setCacheSize0(x);
315 }
316 private static native int setCacheSize0(int x);
317
318
319
320
321 public int varNum() {
322 return varNum0();
323 }
324 private static native int varNum0();
325
326
327
328
329 public int setVarNum(int num) {
330 return setVarNum0(num);
331 }
332 private static native int setVarNum0(int num);
333
334
335
336
337 public BDDPairing makePair() {
338 long ptr = makePair0();
339 if (USE_FINALIZER) {
340 return new BuDDyPairingWithFinalizer(ptr);
341 } else {
342 return new BuDDyPairing(ptr);
343 }
344 }
345 private static native long makePair0();
346
347
348
349
350 public BDD load(String filename) {
351 int id = load0(filename);
352 return makeBDD(id);
353 }
354 private static native int load0(String filename);
355
356
357
358
359 public void save(String filename, BDD b) {
360 save0(filename, unwrap(b));
361 }
362 private static native void save0(String filename, int b);
363
364
365
366
367 public BDDFactory.ReorderMethod getReorderMethod() {
368 int method = getReorderMethod0();
369 switch (method) {
370 case 0: return REORDER_NONE;
371 case 1: return REORDER_WIN2;
372 case 2: return REORDER_WIN2ITE;
373 case 3: return REORDER_WIN3;
374 case 4: return REORDER_WIN3ITE;
375 case 5: return REORDER_SIFT;
376 case 6: return REORDER_SIFTITE;
377 case 7: return REORDER_RANDOM;
378 default: throw new BDDException();
379 }
380 }
381 private static native int getReorderMethod0();
382
383 static long unwrap(BDDPairing p) {
384 return ((BuDDyPairing)p)._ptr;
385 }
386
387
388
389
390 private static class BuDDyPairing extends BDDPairing {
391
392 private long _ptr;
393
394 private BuDDyPairing(long ptr) {
395 this._ptr = ptr;
396 }
397
398
399
400
401 public void set(int oldvar, int newvar) {
402 set0(_ptr, oldvar, newvar);
403 }
404 private static native void set0(long p, int oldvar, int newvar);
405
406
407
408
409 public void set(int[] oldvar, int[] newvar) {
410 set1(_ptr, oldvar, newvar);
411 }
412 private static native void set1(long p, int[] oldvar, int[] newvar);
413
414
415
416
417 public void set(int oldvar, BDD newvar) {
418 set2(_ptr, oldvar, unwrap(newvar));
419 }
420 private static native void set2(long p, int oldvar, int newbdd);
421
422
423
424
425 public void set(int[] oldvar, BDD[] newvar) {
426 set3(_ptr, oldvar, unwrap(Arrays.asList(newvar)));
427 }
428 private static native void set3(long p, int[] oldvar, int[] newbdds);
429
430
431
432
433 public void reset() {
434 reset0(_ptr);
435 }
436 private static native void reset0(long ptr);
437
438 /***
439 * Free the memory allocated for this pair.
440 */
441 public void free() {
442 if (_ptr != 0) free0(_ptr);
443 _ptr = 0;
444 }
445 private static native void free0(long p);
446
447 }
448
449 private static class BuDDyPairingWithFinalizer extends BuDDyPairing {
450
451 private BuDDyPairingWithFinalizer(long ptr) {
452 super(ptr);
453 }
454
455
456
457
458 protected void finalize() throws Throwable {
459 super.finalize();
460 free();
461 }
462
463 }
464
465 public static final String REVISION = "$Revision: 476 $";
466
467
468
469
470 public String getVersion() {
471 return getVersion0()+" rev"+REVISION.substring(11, REVISION.length()-2);
472 }
473 private static native String getVersion0();
474
475
476 private static void gc_callback(int i) {
477 INSTANCE.gbc_handler(i!=0, INSTANCE.gcstats);
478 }
479
480
481 private static void reorder_callback(int i) {
482 INSTANCE.reorder_handler(i!=0, INSTANCE.reorderstats);
483 }
484
485
486 private static void resize_callback(int i, int j) {
487 INSTANCE.resize_handler(i, j);
488 }
489 }