View Javadoc

1   // JDDFactory.java, created Aug 1, 2003 7:06:47 PM by joewhaley
2   // Copyright (C) 2003 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.lang.reflect.Method;
7   
8   /***
9    * JDDFactory
10   * 
11   * @author John Whaley
12   * @version $Id: JDDFactory.java 465 2006-07-26 16:42:44Z joewhaley $
13   */
14  public class JDDFactory extends BDDFactoryIntImpl {
15  
16      public static final String REVISION = "$Revision: 465 $";
17      
18      public String getVersion() {
19          return "JDDFactory "+REVISION.substring(11, REVISION.length()-2);
20      }
21      
22      static final int INVALID_BDD = -1;
23      
24      // Redirection functions.
25      
26      protected void addref_impl(int v) { bdd.ref(v); }
27      protected void delref_impl(int v) { bdd.deref(v); }
28      protected int zero_impl() { return bdd.getZero(); }
29      protected int one_impl() { return bdd.getOne(); }
30      protected int invalid_bdd_impl() { return INVALID_BDD; }
31      protected int var_impl(int index) {
32          int v = level_impl(index);
33          return level2var != null ? level2var[v] : v;
34      }
35      protected int level_impl(int index) {
36          // NOTE: jdd seems to returns the total number of variables when
37          //       calling getVar() on a terminal.
38          int v = bdd.getVar(index);
39          if (index == bdd.getOne() || index == bdd.getZero())
40              throw new BDDException();
41          if (v == -1)
42              throw new BDDException();
43          return v;
44      }
45      protected int low_impl(int v) {
46          if (v == bdd.getOne() || v == bdd.getZero())
47              throw new BDDException();
48          return bdd.getLow(v);
49      }
50      protected int high_impl(int v) {
51          if (v == bdd.getOne() || v == bdd.getZero())
52              throw new BDDException();
53          return bdd.getHigh(v);
54      }
55      protected int ithVar_impl(int var) {
56          if (var >= bdd.numberOfVariables())
57              throw new BDDException();
58          return vars[var];
59      }
60      protected int nithVar_impl(int var) {
61          if (var >= bdd.numberOfVariables())
62              throw new BDDException();
63          return bdd.not(vars[var]);
64      }
65      protected int makenode_impl(int lev, int lo, int hi) { return bdd.mk(lev, lo, hi); }
66      protected int ite_impl(int v1, int v2, int v3) { return bdd.ite(v1, v2, v3); }
67      protected int apply_impl(int x, int y, BDDOp opr) {
68          int r;
69          switch (opr.id) {
70              case 0: r = bdd.and(x, y); break;
71              case 1: r = bdd.xor(x, y); break;
72              case 2: r = bdd.or(x, y); break;
73              case 3: r = bdd.nand(x, y); break;
74              case 4: r = bdd.nor(x, y); break;
75              case 5: r = bdd.imp(x, y); break;
76              case 6: r = bdd.biimp(x, y); break;
77              case 7: r = bdd.and(x, bdd.not(y)); break; // diff
78              default:
79                  throw new UnsupportedOperationException(); // TODO.
80          }
81          return r;
82      }
83      protected int not_impl(int v1) { return bdd.not(v1); }
84      protected int applyAll_impl(int v1, int v2, BDDOp opr, int v3) {
85          // todo: combine.
86          int r = apply_impl(v1, v2, opr);
87          bdd.ref(r);
88          int r2 = bdd.forall(r, v3);
89          bdd.deref(r);
90          return r2;
91      }
92      protected int applyEx_impl(int v1, int v2, BDDOp opr, int v3) {
93          if (opr == and)
94              return bdd.relProd(v1, v2, v3);
95          // todo: combine.
96          int r = apply_impl(v1, v2, opr);
97          bdd.ref(r);
98          int r2 = bdd.exists(r, v3);
99          bdd.deref(r);
100         return r2;
101     }
102     protected int applyUni_impl(int v1, int v2, BDDOp opr, int v3) {
103         throw new UnsupportedOperationException(); // todo.
104     }
105     protected int compose_impl(int v1, int v2, int var) {
106         throw new UnsupportedOperationException(); // todo.
107     }
108     protected int constrain_impl(int v1, int v2) {
109         throw new UnsupportedOperationException(); // todo.
110     }
111     protected int restrict_impl(int v1, int v2) { return bdd.restrict(v1, v2); }
112     protected int simplify_impl(int v1, int v2) { return bdd.simplify(v1, v2); }
113     protected int support_impl(int v) { return bdd.support(v); }
114     protected int exist_impl(int v1, int v2) { return bdd.exists(v1, v2); }
115     protected int forAll_impl(int v1, int v2) { return bdd.forall(v1, v2); }
116     protected int unique_impl(int v1, int v2) {
117         throw new UnsupportedOperationException(); // todo.
118     }
119     protected int fullSatOne_impl(int v) {
120         if (v == bdd.getZero())
121             return v;
122         int[] res = bdd.oneSat(v, null);
123         int result = bdd.getOne();
124         for (int i = res.length - 1; i >= 0; --i) {
125             int u;
126             if (res[i] == 1) 
127                 u = bdd.mk(i, 0, result);
128             else
129                 u = bdd.mk(i, result, 0);
130             bdd.ref(u); bdd.deref(result);
131             result = u;
132         }
133         bdd.deref(result);
134         return result;
135     }
136     
137     protected int replace_impl(int v, BDDPairing p) { return bdd.replace(v, ((bddPairing) p).pairing); }
138     protected int veccompose_impl(int v, BDDPairing p) {
139         throw new UnsupportedOperationException(); // todo.
140     }
141     
142     protected int nodeCount_impl(int v) { return bdd.nodeCount(v); }
143     protected double pathCount_impl(int v) {
144         throw new UnsupportedOperationException(); // todo.
145     }
146     protected double satCount_impl(int v) { return bdd.satCount(v); }
147     protected int satOne_impl(int v) { return bdd.oneSat(v); }
148     protected int satOne_impl2(int v1, int v2, boolean pol) {
149         if (v1 == bdd.getZero())
150             return v1;
151         int[] res = bdd.oneSat(v1, null);
152         int result = bdd.getOne();
153         for (int i = res.length - 1; i >= 0; --i) {
154             while (bdd.getVar(v2) < i)
155                 v2 = bdd.getHigh(v2);
156             boolean p;
157             if (res[i] == 1) p = true;
158             else if (res[i] == 0) p = false;
159             else {
160                 if (bdd.getVar(v2) != i)
161                     continue;
162                 p = pol;
163             }
164             int u = bdd.mk(i, p?0:result, p?result:0);
165             bdd.ref(u); bdd.deref(result);
166             result = u;
167         }
168         bdd.deref(result);
169         return result;
170     }
171     protected int nodeCount_impl2(int[] v) {
172         throw new UnsupportedOperationException(); // todo.
173     }
174     protected int[] varProfile_impl(int v) {
175         throw new UnsupportedOperationException(); // todo.
176     }
177     protected void printTable_impl(int v) {
178         throw new UnsupportedOperationException(); // todo.
179     }
180     
181     // More redirection functions.
182     
183     protected void initialize(int initnodesize, int cs) {
184         bdd = new jdd.bdd.BDD(initnodesize, cs);
185         vars = new int[256];
186     }
187     public void addVarBlock(int first, int last, boolean fixed) {
188         throw new UnsupportedOperationException();
189     }
190     public void varBlockAll() {
191         throw new UnsupportedOperationException();
192     }
193     public void clearVarBlocks() {
194         throw new UnsupportedOperationException();
195     }
196     public void printOrder() {
197         throw new UnsupportedOperationException();
198     }
199     public int getNodeTableSize() {
200         // todo.
201         return bdd.countRootNodes();
202     }
203     public int setNodeTableSize(int x) {
204         // TODO.
205         return getNodeTableSize();
206     }
207     public int setCacheSize(int x) {
208         // TODO.
209         return 0;
210     }
211     public boolean isInitialized() { return true; }
212     public void done() { super.done(); bdd.cleanup(); bdd = null; }
213     public void setError(int code) {
214         // todo: implement this
215     }
216     public void clearError() {
217         // todo: implement this
218     }
219     public int setMaxNodeNum(int size) {
220         // todo: implement this
221         return 0;
222     }
223     public double setMinFreeNodes(double x) {
224         int old = jdd.util.Configuration.minFreeNodesProcent;
225         jdd.util.Configuration.minFreeNodesProcent = (int)(x * 100);
226         return (double) old / 100.;
227     }
228     public int setMaxIncrease(int x) {
229         int old = jdd.util.Configuration.maxNodeIncrease;
230         jdd.util.Configuration.maxNodeIncrease = x;
231         return old;
232     }
233     public double setIncreaseFactor(double x) {
234         // todo: implement this
235         return 0;
236     }
237     public int getNodeNum() {
238         // todo.
239         return bdd.countRootNodes();
240     }
241     public int getCacheSize() {
242         // TODO Implement this.
243         return 0;
244     }
245     public int reorderGain() {
246         throw new UnsupportedOperationException();
247     }
248     public void printStat() {
249         bdd.showStats();
250     }
251     public double setCacheRatio(double x) {
252         // TODO Implement this.
253         return 0;
254     }
255     public int varNum() {
256         return bdd.numberOfVariables();
257     }
258     public int setVarNum(int num) {
259         if (num > Integer.MAX_VALUE / 2)
260             throw new BDDException();
261         int old = bdd.numberOfVariables();
262         int oldSize = vars.length;
263         int newSize = oldSize;
264         while (num > newSize) {
265             newSize *= 2;
266         }
267         if (oldSize != newSize) {
268             int[] oldVars = vars;
269             vars = new int[newSize];
270             System.arraycopy(oldVars, 0, vars, 0, old);
271             
272             if (level2var != null) {
273                 int[] oldlevel2var = level2var;
274                 level2var = new int[newSize];
275                 System.arraycopy(oldlevel2var, 0, level2var, 0, old);
276                 
277                 int[] oldvar2level = var2level;
278                 var2level = new int[newSize];
279                 System.arraycopy(oldvar2level, 0, var2level, 0, old);
280             }
281         }
282         while (bdd.numberOfVariables() < num) {
283             int k = bdd.numberOfVariables();
284             vars[k] = bdd.createVar();
285             bdd.ref(vars[k]);
286             if (level2var != null) {
287                 level2var[k] = k;
288                 var2level[k] = k;
289             }
290         }
291         return old;
292     }
293     public void printAll() {
294         throw new UnsupportedOperationException();
295     }
296     public void setVarOrder(int[] neworder) {
297         // todo: setting var order corrupts all existing BDDs!
298         if (var2level != null)
299             throw new UnsupportedOperationException();
300         
301         if (bdd.numberOfVariables() != neworder.length)
302             throw new BDDException();
303         
304         int[] newvars = new int[vars.length];
305         var2level = new int[vars.length];
306         level2var = new int[vars.length];
307         for (int i = 0; i < bdd.numberOfVariables(); ++i) {
308             int k = neworder[i];
309             //System.out.println("Var "+k+" (node "+vars[k]+") in original order -> var "+i+" (node "+vars[i]+") in new order");
310             newvars[k] = vars[i];
311             var2level[k] = i;
312             level2var[i] = k;
313         }
314         vars = newvars;
315         
316         //System.out.println("Number of domains: "+numberOfDomains());
317         for (int i = 0; i < numberOfDomains(); ++i) {
318             BDDDomain d = getDomain(i);
319             d.var = makeSet(d.ivar);
320             //System.out.println("Set for domain "+d+": "+d.var.toStringWithDomains());
321         }
322     }
323     public int level2Var(int level) { return level2var != null ? level2var[level] : level; }
324     public int var2Level(int var) { return var2level != null ? var2level[var] : var; }
325     public ReorderMethod getReorderMethod() {
326         throw new UnsupportedOperationException();
327     }
328     public int getReorderTimes() {
329         throw new UnsupportedOperationException();
330     }
331     public void disableReorder() {
332         throw new UnsupportedOperationException();
333     }
334     public void enableReorder() {
335         throw new UnsupportedOperationException();
336     }
337     public int reorderVerbose(int v) {
338         throw new UnsupportedOperationException();
339     }
340     public void reorder(ReorderMethod m) {
341         throw new UnsupportedOperationException();
342     }
343     public void autoReorder(ReorderMethod method) {
344         throw new UnsupportedOperationException();
345     }
346     public void autoReorder(ReorderMethod method, int max) {
347         throw new UnsupportedOperationException();
348     }
349     public void swapVar(int v1, int v2) {
350         throw new UnsupportedOperationException();
351     }
352     
353     private jdd.bdd.BDD bdd;
354     private int[] vars; // indexed by EXTERNAL
355     private int[] level2var; // internal -> external
356     private int[] var2level; // external -> internal
357     
358     static {
359         jdd.util.Options.verbose = true;
360     }
361     
362     private JDDFactory(int nodenum, int cachesize) {
363         initialize(nodenum, cachesize);
364     }
365     
366     /* (non-Javadoc)
367      * @see net.sf.javabdd.BDDFactory#init(int, int)
368      */
369     public static BDDFactory init(int nodenum, int cachesize) {
370         BDDFactory f = new JDDFactory(nodenum, cachesize);
371         return f;
372     }
373 
374     private class bddPairing extends BDDPairing {
375         
376         private int[] from;
377         private int[] to;
378         private jdd.bdd.Permutation pairing;
379         
380         private bddPairing() {
381             reset();
382         }
383         
384         /* (non-Javadoc)
385          * @see net.sf.javabdd.BDDPairing#set(int, int)
386          */
387         public void set(int oldvar, int newvar) {
388             for (int i = 0; i < from.length; ++i) {
389                 if (from[i] == vars[oldvar]) {
390                     to[i] = vars[newvar];
391                     pairing = bdd.createPermutation(from, to);
392                     return;
393                 }
394             }
395             int[] oldfrom = from;
396             from = new int[from.length + 1];
397             System.arraycopy(oldfrom, 0, from, 0, oldfrom.length);
398             from[oldfrom.length] = vars[oldvar];
399             int[] oldto = to;
400             to = new int[to.length + 1];
401             System.arraycopy(oldto, 0, to, 0, oldto.length);
402             to[oldto.length] = vars[newvar];
403             pairing = bdd.createPermutation(from, to);
404         }
405         
406         /* (non-Javadoc)
407          * @see net.sf.javabdd.BDDPairing#set(int, net.sf.javabdd.BDD)
408          */
409         public void set(int oldvar, BDD newvar) {
410             throw new UnsupportedOperationException();
411         }
412         
413         public void set(int[] oldvar, int[] newvar) {
414             int[] oldfrom = from;
415             from = new int[from.length + oldvar.length];
416             System.arraycopy(oldfrom, 0, from, 0, oldfrom.length);
417             for (int i = 0; i < oldvar.length; ++i) {
418                 from[i + oldfrom.length] = vars[oldvar[i]];
419             }
420             int[] oldto = to;
421             to = new int[to.length + newvar.length];
422             System.arraycopy(oldto, 0, to, 0, oldto.length);
423             for (int i = 0; i < newvar.length; ++i) {
424                 to[i + oldto.length] = vars[newvar[i]];
425             }
426             //debug();
427             pairing = bdd.createPermutation(from, to);
428         }
429         
430         void debug() {
431             for (int i = 0; i < from.length; ++i) {
432                 System.out.println(bdd.getVar(from[i])+" -> "+bdd.getVar(to[i]));
433             }
434         }
435         
436         /* (non-Javadoc)
437          * @see net.sf.javabdd.BDDPairing#reset()
438          */
439         public void reset() {
440             from = to = new int[] { };
441             pairing = null;
442         }
443         
444     }
445     
446     public BDDPairing makePair() {
447         return new bddPairing();
448     }
449 
450     public void registerGCCallback(Object o, Method m) {
451         throw new UnsupportedOperationException();
452     }
453     public void unregisterGCCallback(Object o, Method m) {
454         throw new UnsupportedOperationException();
455     }
456     public void registerReorderCallback(Object o, Method m) {
457         throw new UnsupportedOperationException();
458     }
459     public void unregisterReorderCallback(Object o, Method m) {
460         throw new UnsupportedOperationException();
461     }
462     public void registerResizeCallback(Object o, Method m) {
463         throw new UnsupportedOperationException();
464     }
465     public void unregisterResizeCallback(Object o, Method m) {
466         throw new UnsupportedOperationException();
467     }
468 }