1
2
3
4 package net.sf.javabdd;
5
6 import java.util.Arrays;
7 import java.util.Comparator;
8 import java.util.HashSet;
9 import java.util.Iterator;
10 import java.util.Random;
11 import java.util.Set;
12 import java.io.BufferedReader;
13 import java.io.BufferedWriter;
14 import java.io.IOException;
15 import java.io.PrintStream;
16
17 /***
18 * <p>BDD factory where each node only takes 16 bytes.
19 * This is accomplished by tightly packing the bits and limiting the
20 * maximum number of BDD variables to 2^10 = 1024.</p>
21 *
22 * <p>Because of the extra computation required for packing/unpacking,
23 * this BDD factory is a little slower than JFactory, but it also uses
24 * 20% less memory.</p>
25 *
26 * @author jwhaley
27 * @version $Id: MicroFactory.java 465 2006-07-26 16:42:44Z joewhaley $
28 */
29 public class MicroFactory extends BDDFactoryIntImpl {
30
31
32
33
34
35
36
37
38
39
40 public static boolean FLUSH_CACHE_ON_GC = true;
41
42 static final boolean VERIFY_ASSERTIONS = false;
43 static final boolean ORDER_CACHE = false;
44 static final int CACHESTATS = 0;
45 static final boolean SWAPCOUNT = false;
46
47 public static final String REVISION = "$Revision: 465 $";
48
49 public String getVersion() {
50 return "MicroFactory "+REVISION.substring(11, REVISION.length()-2);
51 }
52
53 private MicroFactory() { }
54
55
56
57
58 public static BDDFactory init(int nodenum, int cachesize) {
59 BDDFactory f = new MicroFactory();
60 f.initialize(nodenum, cachesize);
61 if (CACHESTATS > 0) addShutdownHook(f);
62 return f;
63 }
64
65 static void addShutdownHook(final BDDFactory f) {
66 Runtime.getRuntime().addShutdownHook(new Thread() {
67 public void run() {
68 System.out.println(f.getCacheStats().toString());
69 }
70 });
71 }
72
73 /***
74 * Implementation of BDDPairing used by JFactory.
75 */
76 class bddPair extends BDDPairing {
77 int[] result;
78 int last;
79 int id;
80 bddPair next;
81
82
83
84
85 public void set(int oldvar, int newvar) {
86 bdd_setpair(this, oldvar, newvar);
87 }
88
89
90
91 public void set(int oldvar, BDD newvar) {
92 bdd_setbddpair(this, oldvar, unwrap(newvar));
93 }
94
95
96
97 public void reset() {
98 bdd_resetpair(this);
99 }
100
101 public String toString() {
102 StringBuffer sb = new StringBuffer();
103 sb.append('{');
104 boolean any = false;
105 for (int i = 0; i < result.length; ++i) {
106 if (result[i] != bdd_ithvar(bddlevel2var[i])) {
107 if (any) sb.append(", ");
108 any = true;
109 sb.append(bddlevel2var[i]);
110 sb.append('=');
111 BDD b = makeBDD(result[i]);
112 sb.append(b);
113 b.free();
114 }
115 }
116 sb.append('}');
117 return sb.toString();
118 }
119 }
120
121
122
123
124 public BDDPairing makePair() {
125 bddPair p = new bddPair();
126 p.result = new int[bddvarnum];
127 int n;
128 for (n = 0; n < bddvarnum; n++)
129 p.result[n] = bdd_ithvar(bddlevel2var[n]);
130
131 p.id = update_pairsid();
132 p.last = -1;
133
134 bdd_register_pair(p);
135 return p;
136 }
137
138
139
140 protected void addref_impl(int v) { bdd_addref(v); }
141 protected void delref_impl(int v) { bdd_delref(v); }
142 protected int zero_impl() { return BDDZERO; }
143 protected int one_impl() { return BDDONE; }
144 protected int invalid_bdd_impl() { return INVALID_BDD; }
145 protected int var_impl(int v) { return bdd_var(v); }
146 protected int level_impl(int v) { return LEVEL(v); }
147 protected int low_impl(int v) { return bdd_low(v); }
148 protected int high_impl(int v) { return bdd_high(v); }
149 protected int ithVar_impl(int var) { return bdd_ithvar(var); }
150 protected int nithVar_impl(int var) { return bdd_nithvar(var); }
151
152 protected int makenode_impl(int lev, int lo, int hi) { return bdd_makenode(lev, lo, hi); }
153 protected int ite_impl(int v1, int v2, int v3) { return bdd_ite(v1, v2, v3); }
154 protected int apply_impl(int v1, int v2, BDDOp opr) { return bdd_apply(v1, v2, opr.id); }
155 protected int not_impl(int v1) { return bdd_not(v1); }
156 protected int applyAll_impl(int v1, int v2, BDDOp opr, int v3) { return bdd_appall(v1, v2, opr.id, v3); }
157 protected int applyEx_impl(int v1, int v2, BDDOp opr, int v3) { return bdd_appex(v1, v2, opr.id, v3); }
158 protected int applyUni_impl(int v1, int v2, BDDOp opr, int v3) { return bdd_appuni(v1, v2, opr.id, v3); }
159 protected int compose_impl(int v1, int v2, int var) { return bdd_compose(v1, v2, var); }
160 protected int constrain_impl(int v1, int v2) { return bdd_constrain(v1, v2); }
161 protected int restrict_impl(int v1, int v2) { return bdd_restrict(v1, v2); }
162 protected int simplify_impl(int v1, int v2) { return bdd_simplify(v1, v2); }
163 protected int support_impl(int v) { return bdd_support(v); }
164 protected int exist_impl(int v1, int v2) { return bdd_exist(v1, v2); }
165 protected int forAll_impl(int v1, int v2) { return bdd_forall(v1, v2); }
166 protected int unique_impl(int v1, int v2) { return bdd_unique(v1, v2); }
167 protected int fullSatOne_impl(int v) { return bdd_fullsatone(v); }
168
169 protected int replace_impl(int v, BDDPairing p) { return bdd_replace(v, (bddPair)p); }
170 protected int veccompose_impl(int v, BDDPairing p) { return bdd_veccompose(v, (bddPair)p); }
171
172 protected int nodeCount_impl(int v) { return bdd_nodecount(v); }
173 protected double pathCount_impl(int v) { return bdd_pathcount(v); }
174 protected double satCount_impl(int v) { return bdd_satcount(v); }
175 protected int satOne_impl(int v) { return bdd_satone(v); }
176 protected int satOne_impl2(int v1, int v2, boolean pol) { return bdd_satoneset(v1, v2, pol); }
177 protected int nodeCount_impl2(int[] v) { return bdd_anodecount(v); }
178 protected int[] varProfile_impl(int v) { return bdd_varprofile(v); }
179 protected void printTable_impl(int v) { bdd_fprinttable(System.out, v); }
180
181
182
183 protected void initialize(int initnodesize, int cs) { bdd_init(initnodesize, cs); }
184 public void addVarBlock(int first, int last, boolean fixed) { bdd_intaddvarblock(first, last, fixed); }
185 public void varBlockAll() { bdd_varblockall(); }
186 public void clearVarBlocks() { bdd_clrvarblocks(); }
187 public void printOrder() { bdd_fprintorder(System.out); }
188 public int getNodeTableSize() { return bdd_getallocnum(); }
189 public int setNodeTableSize(int size) { return bdd_setallocnum(size); }
190 public int setCacheSize(int v) { return bdd_setcachesize(v); }
191 public boolean isInitialized() { return bddrunning; }
192 public void done() { super.done(); bdd_done(); }
193 public void setError(int code) { bdderrorcond = code; }
194 public void clearError() { bdderrorcond = 0; }
195 public int setMaxNodeNum(int size) { return bdd_setmaxnodenum(size); }
196 public double setMinFreeNodes(double x) { return bdd_setminfreenodes((int)(x * 100.)) / 100.; }
197 public int setMaxIncrease(int x) { return bdd_setmaxincrease(x); }
198 public double setIncreaseFactor(double x) { return bdd_setincreasefactor(x); }
199 public int getNodeNum() { return bdd_getnodenum(); }
200 public int getCacheSize() { return cachesize; }
201 public int reorderGain() { return bdd_reorder_gain(); }
202 public void printStat() { bdd_fprintstat(System.out); }
203 public double setCacheRatio(double x) { return bdd_setcacheratio((int)(x * 100)) / 100.; }
204 public int varNum() { return bdd_varnum(); }
205 public int setVarNum(int num) { return bdd_setvarnum(num); }
206 public void printAll() { bdd_fprintall(System.out); }
207 public BDD load(BufferedReader in, int[] translate) throws IOException { return makeBDD(bdd_load(in, translate)); }
208 public void save(BufferedWriter out, BDD b) throws IOException { bdd_save(out, unwrap(b)); }
209 public void setVarOrder(int[] neworder) { bdd_setvarorder(neworder); }
210 public int level2Var(int level) { return bddlevel2var[level]; }
211 public int var2Level(int var) { return bddvar2level[var]; }
212 public int getReorderTimes() { return bddreordertimes; }
213 public void disableReorder() { bdd_disable_reorder(); }
214 public void enableReorder() { bdd_enable_reorder(); }
215 public int reorderVerbose(int v) { return bdd_reorder_verbose(v); }
216 public void reorder(ReorderMethod m) { bdd_reorder(m.id); }
217 public void autoReorder(ReorderMethod method) { bdd_autoreorder(method.id); }
218 public void autoReorder(ReorderMethod method, int max) { bdd_autoreorder_times(method.id, max); }
219 public void swapVar(int v1, int v2) { bdd_swapvar(v1, v2); }
220
221 public ReorderMethod getReorderMethod() {
222 switch (bddreordermethod) {
223 case BDD_REORDER_NONE :
224 return REORDER_NONE;
225 case BDD_REORDER_WIN2 :
226 return REORDER_WIN2;
227 case BDD_REORDER_WIN2ITE :
228 return REORDER_WIN2ITE;
229 case BDD_REORDER_WIN3 :
230 return REORDER_WIN3;
231 case BDD_REORDER_WIN3ITE :
232 return REORDER_WIN3ITE;
233 case BDD_REORDER_SIFT :
234 return REORDER_SIFT;
235 case BDD_REORDER_SIFTITE :
236 return REORDER_SIFTITE;
237 case BDD_REORDER_RANDOM :
238 return REORDER_RANDOM;
239 default :
240 throw new BDDException();
241 }
242 }
243
244
245
246 public void validateAll() { bdd_validate_all(); }
247 public void validateBDD(BDD b) { bdd_validate(unwrap(b)); }
248
249 public MicroFactory cloneFactory() {
250 MicroFactory INSTANCE = new MicroFactory();
251 if (applycache != null)
252 INSTANCE.applycache = this.applycache.copy();
253 if (itecache != null)
254 INSTANCE.itecache = this.itecache.copy();
255 if (quantcache != null)
256 INSTANCE.quantcache = this.quantcache.copy();
257 if (appexcache != null)
258 INSTANCE.appexcache = this.appexcache.copy();
259 if (appex3cache != null)
260 INSTANCE.appex3cache = this.appex3cache.copy();
261 if (replacecache != null)
262 INSTANCE.replacecache = this.replacecache.copy();
263 if (misccache != null)
264 INSTANCE.misccache = this.misccache.copy();
265 if (countcache != null)
266 INSTANCE.countcache = this.countcache.copy();
267
268 INSTANCE.rng = new Random();
269 INSTANCE.verbose = this.verbose;
270 INSTANCE.cachestats.copyFrom(this.cachestats);
271
272 INSTANCE.bddrunning = this.bddrunning;
273 INSTANCE.bdderrorcond = this.bdderrorcond;
274 INSTANCE.bddnodesize = this.bddnodesize;
275 INSTANCE.bddmaxnodesize = this.bddmaxnodesize;
276 INSTANCE.bddmaxnodeincrease = this.bddmaxnodeincrease;
277 INSTANCE.bddfreepos = this.bddfreepos;
278 INSTANCE.bddfreenum = this.bddfreenum;
279 INSTANCE.bddproduced = this.bddproduced;
280 INSTANCE.bddvarnum = this.bddvarnum;
281
282 INSTANCE.gbcollectnum = this.gbcollectnum;
283 INSTANCE.cachesize = this.cachesize;
284 INSTANCE.gbcclock = this.gbcclock;
285 INSTANCE.usednodes_nextreorder = this.usednodes_nextreorder;
286
287 INSTANCE.bddrefstacktop = this.bddrefstacktop;
288 INSTANCE.bddresized = this.bddresized;
289 INSTANCE.minfreenodes = this.minfreenodes;
290 INSTANCE.bddnodes = new int[this.bddnodes.length];
291 System.arraycopy(this.bddnodes, 0, INSTANCE.bddnodes, 0, this.bddnodes.length);
292 INSTANCE.bddrefstack = new int[this.bddrefstack.length];
293 System.arraycopy(this.bddrefstack, 0, INSTANCE.bddrefstack, 0, this.bddrefstack.length);
294 INSTANCE.bddvar2level = new int[this.bddvar2level.length];
295 System.arraycopy(this.bddvar2level, 0, INSTANCE.bddvar2level, 0, this.bddvar2level.length);
296 INSTANCE.bddlevel2var = new int[this.bddlevel2var.length];
297 System.arraycopy(this.bddlevel2var, 0, INSTANCE.bddlevel2var, 0, this.bddlevel2var.length);
298 INSTANCE.bddvarset = new int[this.bddvarset.length];
299 System.arraycopy(this.bddvarset, 0, INSTANCE.bddvarset, 0, this.bddvarset.length);
300
301 INSTANCE.domain = new BDDDomain[this.domain.length];
302 for (int i = 0; i < INSTANCE.domain.length; ++i) {
303 INSTANCE.domain[i] = INSTANCE.createDomain(i, this.domain[i].realsize);
304 }
305 return INSTANCE;
306 }
307
308 /***
309 * Use this function to translate BDD's from a JavaFactory into its clone.
310 * This will only work immediately after cloneFactory() is called, and
311 * before any other BDD operations are performed.
312 *
313 * @param that BDD in old factory
314 * @return a BDD in the new factory
315 */
316 public BDD copyNode(BDD that) {
317 return makeBDD(unwrap(that));
318 }
319
320
321 /****** IMPLEMENTATION BELOW *****/
322
323 private int[] bddnodes;
324
325 static final int __node_size = 4;
326 static final int offset__lref = 0;
327 static final int offset__href = 1;
328 static final int offset__low = 2;
329 static final int offset__high = 3;
330 static final int offset__hash = 0;
331 static final int offset__next = 1;
332 static final int offset__llev = 2;
333 static final int offset__hlev = 3;
334 static final int offset__mark = 1;
335
336 static final int NODE_MASK = 0x07FFFFFF;
337 static final int LEV_LMASK = 0xF8000000;
338 static final int LEV_HMASK = 0xF8000000;
339
340 static final int REF_LMASK = 0xF8000000;
341 static final int REF_HMASK = 0xF0000000;
342 static final int REF_LINC = 0x08000000;
343 static final int REF_HINC = 0x10000000;
344 static final int MARK_MASK = 0x08000000;
345 static final int HASH_MASK = 0x07FFFFFF;
346 static final int NEXT_MASK = 0x07FFFFFF;
347
348 static final int NODE_BITS = 27;
349 static final int LEV_LPOS = 27;
350 static final int LEV_LBITS = 5;
351 static final int LEV_HPOS = 27;
352 static final int LEV_HBITS = 5;
353 static final int REF_LPOS = 27;
354 static final int REF_LBITS = 5;
355 static final int REF_HPOS = 28;
356 static final int REF_HBITS = 4;
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382 static final int INVALID_BDD = NODE_MASK;
383 static final int MAXVAR = (1 << (LEV_LBITS + LEV_HBITS)) - 1;
384 static final int MAX_PAIRSID = MAXVAR;
385
386 private final boolean HASREF(int node) {
387 int a = bddnodes[node*__node_size + offset__lref] & REF_LMASK;
388 if (a != 0) return true;
389 if (REF_HMASK == 0) return false;
390 int b = bddnodes[node*__node_size + offset__href] & REF_HMASK;
391 return (b != 0);
392 }
393
394 private final void SETMAXREF(int node) {
395 bddnodes[node*__node_size + offset__lref] |= REF_LMASK;
396 if (REF_HMASK != 0)
397 bddnodes[node*__node_size + offset__href] |= REF_HMASK;
398 }
399
400 private final void CLEARREF(int node) {
401 bddnodes[node*__node_size + offset__lref] &= ~REF_LMASK;
402 if (REF_HMASK != 0)
403 bddnodes[node*__node_size + offset__href] &= ~REF_HMASK;
404 }
405
406 private final void INCREF(int node) {
407 int a = bddnodes[node*__node_size + offset__lref] & REF_LMASK;
408 if (a == REF_LMASK) {
409 if (REF_HMASK == 0) return;
410 int b = bddnodes[node*__node_size + offset__href] & REF_HMASK;
411 if (b == REF_HMASK) return;
412 bddnodes[node*__node_size + offset__href] += REF_HINC;
413 }
414 bddnodes[node*__node_size + offset__lref] += REF_LINC;
415 }
416
417 private final void DECREF(int node) {
418 int a = bddnodes[node*__node_size + offset__lref] & REF_LMASK;
419 if (a != REF_LMASK ||
420 (REF_HMASK != 0 &&
421 (bddnodes[node*__node_size + offset__href] & REF_HMASK) != REF_HMASK)) {
422 if (REF_HMASK != 0 && a == 0) bddnodes[node*__node_size + offset__href] -= REF_HINC;
423 bddnodes[node*__node_size + offset__lref] -= REF_LINC;
424 }
425 }
426
427 private final int GETREF(int node) {
428 int a = bddnodes[node*__node_size + offset__lref] & REF_LMASK;
429 if (REF_HMASK == 0) return a >>> REF_LPOS;
430 int b = bddnodes[node*__node_size + offset__href] & REF_HMASK;
431 return a >>> REF_LPOS | b >>> (REF_HPOS-REF_LBITS);
432 }
433
434 private final int LEVEL(int node) {
435 int a = bddnodes[node*__node_size + offset__llev] & LEV_LMASK;
436 if (LEV_HMASK == 0) return a >>> LEV_LPOS;
437 int b = bddnodes[node*__node_size + offset__hlev] & LEV_HMASK;
438 int lev = a >>> LEV_LPOS | b >>> (LEV_HPOS-LEV_LBITS);
439 return lev;
440 }
441
442 private final void SETLEVEL(int node, int val) {
443 if (VERIFY_ASSERTIONS) _assert(val >= 0 && val < (1 << (LEV_LBITS + LEV_HBITS)));
444 int a = bddnodes[node*__node_size + offset__llev] & ~LEV_LMASK;
445 a |= (val << LEV_LPOS);
446 bddnodes[node*__node_size + offset__llev] = a;
447 if (LEV_HMASK == 0) return;
448 int b = bddnodes[node*__node_size + offset__hlev] & ~LEV_HMASK;
449 b |= (val << (LEV_HPOS-LEV_LBITS)) & LEV_HMASK;
450 bddnodes[node*__node_size + offset__hlev] = b;
451 }
452
453 private final void SETMARK(int n) {
454 bddnodes[n*__node_size + offset__mark] |= MARK_MASK;
455 }
456
457 private final void UNMARK(int n) {
458 bddnodes[n*__node_size + offset__mark] &= ~MARK_MASK;
459 }
460
461 private final boolean MARKED(int n) {
462 return (bddnodes[n*__node_size + offset__mark] & MARK_MASK) != 0;
463 }
464
465 private final int LOW(int r) {
466 return bddnodes[r*__node_size + offset__low] & NODE_MASK;
467 }
468
469 private final void SETLOW(int r, int v) {
470 if (VERIFY_ASSERTIONS) _assert(v >= 0 && v <= NODE_MASK);
471 int a = bddnodes[r*__node_size + offset__low] & ~NODE_MASK;
472 a |= v;
473 bddnodes[r*__node_size + offset__low] = a;
474 }
475
476 private final int HIGH(int r) {
477 return bddnodes[r*__node_size + offset__high] & NODE_MASK;
478 }
479
480 private final void SETHIGH(int r, int v) {
481 if (VERIFY_ASSERTIONS) _assert(v >= 0 && v <= NODE_MASK);
482 int a = bddnodes[r*__node_size + offset__high] & ~NODE_MASK;
483 a |= v;
484 bddnodes[r*__node_size + offset__high] = a;
485 }
486
487 private final int HASH(int r) {
488 return bddnodes[r*__node_size + offset__hash] & HASH_MASK;
489 }
490
491 private final void SETHASH(int r, int v) {
492 if (VERIFY_ASSERTIONS) _assert(v >= 0 && v <= HASH_MASK);
493 int a = bddnodes[r*__node_size + offset__hash] & ~HASH_MASK;
494 a |= v;
495 bddnodes[r*__node_size + offset__hash] = a;
496 }
497
498 private final int NEXT(int r) {
499 return bddnodes[r*__node_size + offset__next] & NEXT_MASK;
500 }
501
502 private final void SETNEXT(int r, int v) {
503 if (VERIFY_ASSERTIONS) _assert(v >= 0 && v <= NEXT_MASK);
504 int a = bddnodes[r*__node_size + offset__next] & ~NEXT_MASK;
505 a |= v;
506 bddnodes[r*__node_size + offset__next] = a;
507 }
508
509 private final void INIT_NODE(int r, int lev, int lo, int hi, int next) {
510 bddnodes[r*__node_size + offset__next] = next;
511 bddnodes[r*__node_size + offset__low] = lo | (lev << LEV_LPOS);
512 int k;
513 if (LEV_HMASK == 0) k = hi;
514 else k = hi | ((lev << (LEV_HPOS-LEV_LBITS)) & LEV_HMASK);
515 bddnodes[r*__node_size + offset__high] = k;
516 }
517
518 private final int VARr(int r) {
519 return LEVEL(r);
520 }
521 private final void SETVARr(int n, int val) {
522 SETLEVEL(n, val);
523 }
524 private final int LEVELANDMARK(int r) {
525 return LEVEL(r);
526 }
527 private final void SETLEVELANDMARK(int n, int val) {
528 SETLEVEL(n, val);
529 }
530
531 private static final void _assert(boolean b) {
532 if (!b)
533 throw new InternalError();
534 }
535
536 private class OpCache {
537 int cacheHit;
538 int cacheMiss;
539 int compulsoryMiss;
540 Set cache;
541
542 OpCache() {
543 if (CACHESTATS > 1) cache = new HashSet();
544 }
545
546 public String toString() {
547 return "\tHit: "+cacheHit+"\tMiss: "+cacheMiss
548 +" ("+compulsoryMiss+" compulsory)"
549 +"\t("+((float)cacheHit/((float) cacheHit+cacheMiss))*100+"%)";
550 }
551
552 void checkCompulsory(int a) {
553 if (!cache.contains(new Integer(a)))
554 ++compulsoryMiss;
555 }
556 void checkCompulsory(int a, int b) {
557 if (!cache.contains(new PairOfInts(a, b)))
558 ++compulsoryMiss;
559 }
560 void checkCompulsory(int a, int b, int c) {
561 if (!cache.contains(new TripleOfInts(a, b, c)))
562 ++compulsoryMiss;
563 }
564 void checkCompulsory(int a, int b, int c, int d) {
565 if (!cache.contains(new QuadOfInts(a, b, c, d)))
566 ++compulsoryMiss;
567 }
568 void addCompulsory(int a) {
569 cache.add(new Integer(a));
570 }
571 void addCompulsory(int a, int b) {
572 cache.add(new PairOfInts(a, b));
573 }
574 void addCompulsory(int a, int b, int c) {
575 cache.add(new TripleOfInts(a, b, c));
576 }
577 void addCompulsory(int a, int b, int c, int d) {
578 cache.add(new QuadOfInts(a, b, c, d));
579 }
580 void removeCompulsory(int a) {
581 cache.remove(new Integer(a));
582 }
583 void removeCompulsory(int a, int b) {
584 cache.remove(new PairOfInts(a, b));
585 }
586 void removeCompulsory(int a, int b, int c) {
587 cache.remove(new TripleOfInts(a, b, c));
588 }
589 void removeCompulsory(int a, int b, int c, int d) {
590 cache.remove(new QuadOfInts(a, b, c, d));
591 }
592 void removeAll(int n) {
593 for (Iterator i = cache.iterator(); i.hasNext(); ) {
594 Object o = i.next();
595 if (o instanceof Integer) {
596 Integer a = (Integer) o;
597 if (n == a.intValue()) i.remove();
598 } else if (o instanceof PairOfInts) {
599 PairOfInts a = (PairOfInts) o;
600 if (n == a.a || n == a.b) i.remove();
601 } else if (o instanceof TripleOfInts) {
602 TripleOfInts a = (TripleOfInts) o;
603 if (n == a.a || n == a.b || n == a.c) i.remove();
604 } else if (o instanceof QuadOfInts) {
605 QuadOfInts a = (QuadOfInts) o;
606 if (n == a.a || n == a.b || n == a.c || n == a.d) i.remove();
607 }
608 }
609 }
610 }
611
612 public static class PairOfInts {
613 int a, b;
614 public PairOfInts(int x, int y) { a = x; b = y; }
615 public boolean equals(PairOfInts o) {
616 return a == o.a && b == o.b;
617 }
618 public boolean equals(Object o) {
619 if (o instanceof PairOfInts)
620 return equals((PairOfInts) o);
621 return false;
622 }
623 public int hashCode() { return a ^ b; }
624 }
625
626 public static class TripleOfInts {
627 int a, b, c;
628 public TripleOfInts(int x, int y, int z) { a = x; b = y; c = z; }
629 public boolean equals(TripleOfInts o) {
630 return a == o.a && b == o.b && c == o.c;
631 }
632 public boolean equals(Object o) {
633 if (o instanceof TripleOfInts)
634 return equals((TripleOfInts) o);
635 return false;
636 }
637 public int hashCode() { return a ^ b ^ c; }
638 }
639
640 public static class QuadOfInts {
641 int a, b, c, d;
642 public QuadOfInts(int x, int y, int z, int q) { a = x; b = y; c = z; d = q; }
643 public boolean equals(QuadOfInts o) {
644 return a == o.a && b == o.b && c == o.c && d == o.d;
645 }
646 public boolean equals(Object o) {
647 if (o instanceof QuadOfInts)
648 return equals((QuadOfInts) o);
649 return false;
650 }
651 public int hashCode() { return a ^ b ^ c ^ d; }
652 }
653
654 private class OpCache1 extends OpCache {
655 OpCache1Entry table[];
656
657 OpCache1(int size) { alloc(size); }
658 final void alloc(int size) {
659 table = new OpCache1Entry[size];
660 for (int i = 0; i < table.length; ++i) {
661 table[i] = new OpCache1Entry();
662 }
663 }
664 final OpCache1Entry lookup(int hash) {
665 return (OpCache1Entry) table[Math.abs(hash % table.length)];
666 }
667 final void reset() {
668 for (int i = 0; i < table.length; ++i) {
669 table[i].a = -1;
670 }
671 if (CACHESTATS > 1) cache.clear();
672 }
673 final void clean() {
674 for (int i = 0; i < table.length; ++i) {
675 int a = table[i].a;
676 if (a == -1) continue;
677 if (LOW(a & NODE_MASK) == INVALID_BDD ||
678 LOW(table[i].res) == INVALID_BDD) {
679 if (CACHESTATS > 1) removeCompulsory(table[i].a);
680 table[i].a = -1;
681 }
682 }
683 }
684 final OpCache1 copy() {
685 OpCache1 that = new OpCache1(this.table.length);
686 for (int i = 0; i < this.table.length; ++i) {
687 that.table[i].a = this.table[i].a;
688 that.table[i].res = this.table[i].res;
689 }
690 if (CACHESTATS > 0) {
691 that.cacheHit = this.cacheHit;
692 that.cacheMiss = this.cacheMiss;
693 if (CACHESTATS > 1)
694 that.cache.addAll(this.cache);
695 }
696 return that;
697 }
698 final int get_sid(OpCache1Entry e, int node, int id) {
699 if (VERIFY_ASSERTIONS) {
700 _assert(node == (node & NODE_MASK));
701 _assert(id == (id & ~NODE_MASK));
702 }
703 int k = node | id;
704 if (e.a != k) {
705 if (CACHESTATS > 0) cacheMiss++;
706 if (CACHESTATS > 1) checkCompulsory(k);
707 return -1;
708 }
709 if (CACHESTATS > 0) cacheHit++;
710 return e.res;
711 }
712 final void set_sid(OpCache1Entry e, int node, int id, int r) {
713 if (VERIFY_ASSERTIONS) {
714 _assert(node == (node & NODE_MASK));
715 _assert(id == (id & ~NODE_MASK));
716 }
717 e.a = node | id;
718 e.res = r;
719 if (CACHESTATS > 1) addCompulsory(e.a);
720 }
721
722 }
723
724 private static class OpCache1Entry {
725 int a;
726 int res;
727 }
728
729 private class OpCache2 extends OpCache {
730 OpCache2Entry table[];
731
732 OpCache2(int size) { alloc(size); }
733 final void alloc(int size) {
734 table = new OpCache2Entry[size];
735 for (int i = 0; i < table.length; ++i) {
736 table[i] = new OpCache2Entry();
737 }
738 }
739 final OpCache2Entry lookup(int hash) {
740 return (OpCache2Entry) table[Math.abs(hash % table.length)];
741 }
742 final void reset() {
743 for (int i = 0; i < table.length; ++i) {
744 table[i].a = -1;
745 }
746 if (CACHESTATS > 1) cache.clear();
747 }
748 final void clean() {
749 for (int i = 0; i < table.length; ++i) {
750 int a = table[i].a;
751 if (a == -1) continue;
752 if (LOW(a & NODE_MASK) == INVALID_BDD ||
753 LOW(table[i].b) == INVALID_BDD ||
754 LOW(table[i].res) == INVALID_BDD) {
755 if (CACHESTATS > 1) removeCompulsory(table[i].a, table[i].b);
756 table[i].a = -1;
757 }
758 }
759 }
760 final OpCache2 copy() {
761 OpCache2 that = new OpCache2(this.table.length);
762 for (int i = 0; i < this.table.length; ++i) {
763 that.table[i].a = this.table[i].a;
764 that.table[i].b = this.table[i].b;
765 that.table[i].res = this.table[i].res;
766 }
767 if (CACHESTATS > 0) {
768 that.cacheHit = this.cacheHit;
769 that.cacheMiss = this.cacheMiss;
770 if (CACHESTATS > 1)
771 that.cache.addAll(this.cache);
772 }
773 return that;
774 }
775
776 final int get_id(OpCache2Entry e, int node1, int node2, int id) {
777 if (VERIFY_ASSERTIONS) {
778 _assert(node1 == (node1 & NODE_MASK));
779 _assert(node2 == (node2 & NODE_MASK));
780 _assert(id >= 0 && id < (1 << (LEV_LBITS + LEV_HBITS)));
781 }
782 int k1 = node1 | (id << LEV_LPOS);
783 if (e.a != k1 ||
784 e.b != (node2 | ((id << (LEV_HPOS-LEV_LBITS)) & LEV_HMASK))) {
785 if (CACHESTATS > 0) cacheMiss++;
786 if (CACHESTATS > 1) checkCompulsory(k1, node2 | ((id << (LEV_HPOS-LEV_LBITS)) & LEV_HMASK));
787 return -1;
788 }
789 if (CACHESTATS > 0) cacheHit++;
790 return e.res;
791 }
792
793 final int get_sid(OpCache2Entry e, int node1, int node2, int id) {
794 if (VERIFY_ASSERTIONS) {
795 _assert(node1 == (node1 & NODE_MASK));
796 _assert(node2 == (node2 & NODE_MASK));
797 _assert(id == (id & ~NODE_MASK));
798 }
799 int k = node1 | id;
800 if (e.a != k || e.b != node2) {
801 if (CACHESTATS > 0) cacheMiss++;
802 if (CACHESTATS > 1) checkCompulsory(k, node2);
803 return -1;
804 }
805 if (CACHESTATS > 0) cacheHit++;
806 return e.res;
807 }
808
809 final int get(OpCache2Entry e, int node1, int node2) {
810 if (VERIFY_ASSERTIONS) {
811 _assert(node1 == (node1 & NODE_MASK));
812 _assert(node2 == (node2 & NODE_MASK));
813 }
814 if (e.a != node1 || e.b != node2) {
815 if (CACHESTATS > 0) cacheMiss++;
816 if (CACHESTATS > 1) checkCompulsory(node1, node2);
817 return -1;
818 }
819 if (CACHESTATS > 0) cacheHit++;
820 return e.res;
821 }
822
823 final void set_id(OpCache2Entry e, int node1, int node2, int id, int r) {
824 if (VERIFY_ASSERTIONS) {
825 _assert(node1 == (node1 & NODE_MASK));
826 _assert(node2 == (node2 & NODE_MASK));
827 _assert(id >= 0 && id < (1 << (LEV_LBITS + LEV_HBITS)));
828 }
829 e.a = node1 | (id << LEV_LPOS);
830 e.b = node2 | ((id << (LEV_HPOS-LEV_LBITS)) & LEV_HMASK);
831 e.res = r;
832 if (CACHESTATS > 1) addCompulsory(e.a, e.b);
833 }
834
835 final void set_sid(OpCache2Entry e, int node1, int node2, int id, int r) {
836 if (VERIFY_ASSERTIONS) {
837 _assert(node1 == (node1 & NODE_MASK));
838 _assert(node2 == (node2 & NODE_MASK));
839 _assert(id == (id & ~NODE_MASK));
840 }
841 e.a = node1 | id;
842 e.b = node2;
843 e.res = r;
844 if (CACHESTATS > 1) addCompulsory(e.a, e.b);
845 }
846
847 final void set(OpCache2Entry e, int node1, int node2, int r) {
848 e.a = node1;
849 e.b = node2;
850 e.res = r;
851 if (CACHESTATS > 1) addCompulsory(e.a, e.b);
852 }
853 }
854
855 private static class OpCache2Entry {
856 int a, b;
857 int res;
858 }
859
860 private class OpCache3 extends OpCache {
861 OpCache3Entry table[];
862
863 OpCache3(int size) { alloc(size); }
864 final void alloc(int size) {
865 table = new OpCache3Entry[size];
866 for (int i = 0; i < table.length; ++i) {
867 table[i] = new OpCache3Entry();
868 }
869 }
870 final OpCache3Entry lookup(int hash) {
871 return (OpCache3Entry) table[Math.abs(hash % table.length)];
872 }
873 final void reset() {
874 for (int i = 0; i < table.length; ++i) {
875 table[i].a = -1;
876 }
877 if (CACHESTATS > 1) cache.clear();
878 }
879 final void clean() {
880 for (int i = 0; i < table.length; ++i) {
881 int a = table[i].a;
882 if (a == -1) continue;
883 if (LOW(a & NODE_MASK) == INVALID_BDD ||
884 LOW(table[i].b) == INVALID_BDD ||
885 LOW(table[i].c) == INVALID_BDD ||
886 LOW(table[i].res) == INVALID_BDD) {
887 if (CACHESTATS > 1) removeCompulsory(table[i].a, table[i].b, table[i].c);
888 table[i].a = -1;
889 }
890 }
891 }
892 final OpCache3 copy() {
893 OpCache3 that = new OpCache3(this.table.length);
894 for (int i = 0; i < this.table.length; ++i) {
895 that.table[i].a = this.table[i].a;
896 that.table[i].b = this.table[i].b;
897 that.table[i].c = this.table[i].c;
898 that.table[i].res = this.table[i].res;
899 }
900 if (CACHESTATS > 0) {
901 that.cacheHit = this.cacheHit;
902 that.cacheMiss = this.cacheMiss;
903 if (CACHESTATS > 1)
904 that.cache.addAll(this.cache);
905 }
906 return that;
907 }
908
909 final int get(OpCache3Entry e, int node1, int node2, int node3) {
910 if (e.a != node1 || e.b != node2 || e.c != node3) {
911 if (CACHESTATS > 0) cacheMiss++;
912 if (CACHESTATS > 1) checkCompulsory(node1, node2, node3);
913 return -1;
914 }
915 if (CACHESTATS > 0) cacheHit++;
916 return e.res;
917 }
918
919 final void set(OpCache3Entry e, int node1, int node2, int node3, int r) {
920 e.a = node1;
921 e.b = node2;
922 e.c = node3;
923 e.res = r;
924 if (CACHESTATS > 1) addCompulsory(e.a, e.b, e.c);
925 }
926 }
927
928 private static class OpCache3Entry {
929 int a, b, c;
930 int res;
931 }
932
933 private class OpCache4 extends OpCache {
934 OpCache4Entry table[];
935
936 OpCache4(int size) { alloc(size); }
937 final void alloc(int size) {
938 table = new OpCache4Entry[size];
939 for (int i = 0; i < table.length; ++i) {
940 table[i] = new OpCache4Entry();
941 }
942 }
943 final OpCache4Entry lookup(int hash) {
944 return (OpCache4Entry) table[Math.abs(hash % table.length)];
945 }
946 final void reset() {
947 for (int i = 0; i < table.length; ++i) {
948 table[i].a = -1;
949 }
950 if (CACHESTATS > 1) cache.clear();
951 }
952 final void clean() {
953 for (int i = 0; i < table.length; ++i) {
954 int a = table[i].a;
955 if (a == -1) continue;
956 if (LOW(a & NODE_MASK) == INVALID_BDD ||
957 LOW(table[i].b) == INVALID_BDD ||
958 LOW(table[i].c) == INVALID_BDD ||
959 LOW(table[i].d) == INVALID_BDD ||
960 LOW(table[i].res) == INVALID_BDD) {
961 if (CACHESTATS > 1) removeCompulsory(table[i].a, table[i].b, table[i].c, table[i].d);
962 table[i].a = -1;
963 }
964 }
965 }
966 final OpCache4 copy() {
967 OpCache4 that = new OpCache4(this.table.length);
968 for (int i = 0; i < this.table.length; ++i) {
969 that.table[i].a = this.table[i].a;
970 that.table[i].b = this.table[i].b;
971 that.table[i].c = this.table[i].c;
972 that.table[i].d = this.table[i].d;
973 that.table[i].res = this.table[i].res;
974 }
975 if (CACHESTATS > 0) {
976 that.cacheHit = this.cacheHit;
977 that.cacheMiss = this.cacheMiss;
978 if (CACHESTATS > 1)
979 that.cache.addAll(this.cache);
980 }
981 return that;
982 }
983
984 final int get(OpCache4Entry e, int node1, int node2, int node3, int node4) {
985 if (e.a != node1 || e.b != node2 || e.c != node3 || e.d != node4) {
986 if (CACHESTATS > 0) cacheMiss++;
987 if (CACHESTATS > 1) checkCompulsory(node1, node2, node3, node4);
988 return -1;
989 }
990 if (CACHESTATS > 0) cacheHit++;
991 return e.res;
992 }
993
994 final void set(OpCache4Entry e, int node1, int node2, int node3, int node4, int r) {
995 e.a = node1;
996 e.b = node2;
997 e.c = node3;
998 e.d = node4;
999 e.res = r;
1000 if (CACHESTATS > 1) addCompulsory(e.a, e.b, e.c, e.d);
1001 }
1002 }
1003
1004 private static class OpCache4Entry {
1005 int a, b, c, d;
1006 int res;
1007 }
1008
1009 private class OpCacheD extends OpCache {
1010 OpCacheDEntry table[];
1011
1012 OpCacheD(int size) { alloc(size); }
1013 final void alloc(int size) {
1014 table = new OpCacheDEntry[size];
1015 for (int i = 0; i < table.length; ++i) {
1016 table[i] = new OpCacheDEntry();
1017 }
1018 }
1019 final OpCacheDEntry lookup(int hash) {
1020 return (OpCacheDEntry) table[Math.abs(hash % table.length)];
1021 }
1022 final void reset() {
1023 for (int i = 0; i < table.length; ++i) {
1024 table[i].a = -1;
1025 }
1026 if (CACHESTATS > 1) cache.clear();
1027 }
1028 final void clean() {
1029 for (int i = 0; i < table.length; ++i) {
1030 int a = table[i].a;
1031 if (a == -1) continue;
1032 if (LOW(a & NODE_MASK) == INVALID_BDD) {
1033 if (CACHESTATS > 1) removeCompulsory(table[i].a);
1034 table[i].a = -1;
1035 }
1036 }
1037 }
1038 final OpCacheD copy() {
1039 OpCacheD that = new OpCacheD(this.table.length);
1040 for (int i = 0; i < this.table.length; ++i) {
1041 that.table[i].a = this.table[i].a;
1042 that.table[i].res = this.table[i].res;
1043 }
1044 if (CACHESTATS > 0) {
1045 that.cacheHit = this.cacheHit;
1046 that.cacheMiss = this.cacheMiss;
1047 if (CACHESTATS > 1)
1048 that.cache.addAll(this.cache);
1049 }
1050 return that;
1051 }
1052
1053 final double get_sid(OpCacheDEntry e, int node, int id) {
1054 if (VERIFY_ASSERTIONS) {
1055 _assert(node == (node & NODE_MASK));
1056 _assert(id == (id & ~NODE_MASK));
1057 }
1058 int k = node | id;
1059 if (e.a != k) {
1060 if (CACHESTATS > 0) cacheMiss++;
1061 if (CACHESTATS > 1) checkCompulsory(k);
1062 return -1;
1063 }
1064 if (CACHESTATS > 0) cacheHit++;
1065 return e.res;
1066 }
1067
1068 final void set_sid(OpCacheDEntry e, int node, int id, double r) {
1069 if (VERIFY_ASSERTIONS) {
1070 _assert(node == (node & NODE_MASK));
1071 _assert(id == (id & ~NODE_MASK));
1072 }
1073 e.a = node | id;
1074 e.res = r;
1075 if (CACHESTATS > 1) addCompulsory(e.a);
1076 }
1077 }
1078
1079 private static class OpCacheDEntry {
1080 int a;
1081 double res;
1082 }
1083
1084 private static class JavaBDDException extends BDDException {
1085 /***
1086 * Version ID for serialization.
1087 */
1088 private static final long serialVersionUID = 3257289123604607538L;
1089
1090 public JavaBDDException(int x) {
1091 super(errorstrings[-x]);
1092 }
1093 }
1094
1095 private static class ReorderException extends RuntimeException {
1096 /***
1097 * Version ID for serialization.
1098 */
1099 private static final long serialVersionUID = 3256727264505772345L;
1100 }
1101
1102 static final int bddtrue = 1;
1103 static final int bddfalse = 0;
1104
1105 static final int BDDONE = 1;
1106 static final int BDDZERO = 0;
1107
1108 boolean bddrunning; /package-summary.html">initialized */
1109 int bdderrorcond;
1110 int bddnodesize;
1111 int bddmaxnodesize;
1112 int bddmaxnodeincrease;
1113 int bddfreepos;
1114 int bddfreenum;
1115 int bddproduced;
1116 int bddvarnum;
1117 int[] bddrefstack;
1118 int bddrefstacktop;
1119 int[] bddvar2level;
1120 int[] bddlevel2var;
1121 boolean bddresized;
1122
1123 int minfreenodes = 20;
1124
1125
1126
1127 int[] bddvarset;
1128 int gbcollectnum;
1129 int cachesize;
1130 long gbcclock;
1131 int usednodes_nextreorder;
1132
1133 static final int BDD_MEMORY = (-1);
1134 static final int BDD_VAR = (-2);
1135 static final int BDD_RANGE = (-3);
1136 static final int BDD_DEREF = (-4);
1137 static final int BDD_RUNNING = (-5);
1138 static final int BDD_FILE = (-6);
1139 static final int BDD_FORMAT = (-7);
1140 static final int BDD_ORDER = (-8);
1141 static final int BDD_BREAK = (-9);
1142 static final int BDD_VARNUM = (-10);
1143 static final int BDD_NODES = (-11);
1144
1145 static final int BDD_OP = (-12);
1146 static final int BDD_VARSET = (-13);
1147 static final int BDD_VARBLK = (-14);
1148 static final int BDD_DECVNUM = (-15);
1149 static final int BDD_REPLACE = (-16);
1150 static final int BDD_NODENUM = (-17);
1151 static final int BDD_ILLBDD = (-18);
1152 static final int BDD_SIZE = (-19);
1153
1154 static final int BVEC_SIZE = (-20);
1155 static final int BVEC_SHIFT = (-21);
1156 static final int BVEC_DIVZERO = (-22);
1157
1158 static final int BDD_ERRNUM = 24;
1159
1160
1161 static String errorstrings[] =
1162 {
1163 "",
1164 "Out of memory",
1165 "Unknown variable",
1166 "Value out of range",
1167 "Unknown BDD root dereferenced",
1168 "bdd_init() called twice",
1169 "File operation failed",
1170 "Incorrect file format",
1171 "Variables not in ascending order",
1172 "User called break",
1173 "Mismatch in size of variable sets",
1174 "Cannot allocate fewer nodes than already in use",
1175 "Unknown operator",
1176 "Illegal variable set",
1177 "Bad variable block operation",
1178 "Trying to decrease the number of variables",
1179 "Trying to replace with variables already in the bdd",
1180 "Number of nodes reached user defined maximum",
1181 "Unknown BDD - was not in node table",
1182 "Bad size argument",
1183 "Mismatch in bitvector size",
1184 "Illegal shift-left/right parameter",
1185 "Division by zero" };
1186
1187 static final int DEFAULTMAXNODEINC = 10000000;
1188
1189
1190
1191 static final int PAIR(int a, int b) {
1192
1193 return ((a + b) * (a + b + 1) / 2 + a);
1194 }
1195 static final int TRIPLE(int a, int b, int c) {
1196
1197 return (PAIR(c, PAIR(a, b)));
1198 }
1199
1200 final int NODEHASH(int lvl, int l, int h) {
1201 return Math.abs(TRIPLE(lvl, l, h) % bddnodesize);
1202 }
1203
1204 int bdd_ithvar(int var) {
1205 if (var < 0 || var >= bddvarnum) {
1206 bdd_error(BDD_VAR);
1207 return bddfalse;
1208 }
1209
1210 return bddvarset[var * 2];
1211 }
1212
1213 int bdd_nithvar(int var) {
1214 if (var < 0 || var >= bddvarnum) {
1215 bdd_error(BDD_VAR);
1216 return bddfalse;
1217 }
1218
1219 return bddvarset[var * 2 + 1];
1220 }
1221
1222 int bdd_varnum() {
1223 return bddvarnum;
1224 }
1225
1226 static int bdd_error(int v) {
1227 throw new JavaBDDException(v);
1228 }
1229
1230 static boolean ISZERO(int r) {
1231 return r == bddfalse;
1232 }
1233
1234 static boolean ISONE(int r) {
1235 return r == bddtrue;
1236 }
1237
1238 static boolean ISCONST(int r) {
1239
1240 return r < 2;
1241 }
1242
1243 void CHECK(int r) {
1244 if (!bddrunning)
1245 bdd_error(BDD_RUNNING);
1246 else if (r < 0 || r >= bddnodesize)
1247 bdd_error(BDD_ILLBDD);
1248 else if (r >= 2 && LOW(r) == INVALID_BDD)
1249 bdd_error(BDD_ILLBDD);
1250 }
1251 void CHECKa(int r, int x) {
1252 CHECK(r);
1253 }
1254
1255 int bdd_var(int root) {
1256 CHECK(root);
1257 if (root < 2)
1258 bdd_error(BDD_ILLBDD);
1259
1260 return (bddlevel2var[LEVEL(root)]);
1261 }
1262
1263 int bdd_low(int root) {
1264 CHECK(root);
1265 if (root < 2)
1266 return bdd_error(BDD_ILLBDD);
1267
1268 return (LOW(root));
1269 }
1270
1271 int bdd_high(int root) {
1272 CHECK(root);
1273 if (root < 2)
1274 return bdd_error(BDD_ILLBDD);
1275
1276 return (HIGH(root));
1277 }
1278
1279 void checkresize() {
1280 if (bddresized)
1281 bdd_operator_noderesize();
1282 bddresized = false;
1283 }
1284
1285 static final int NOTHASH(int r) {
1286 return r;
1287 }
1288 static final int ANDHASH(int l, int r) {
1289
1290 return (l ^ r);
1291 }
1292 static final int ORHASH(int l, int r) {
1293
1294 return (l ^ r);
1295 }
1296 static final int APPLYHASH(int l, int r, int op) {
1297 return TRIPLE(l, r, op);
1298 }
1299 static final int ITEHASH(int f, int g, int h) {
1300 return TRIPLE(f, g, h);
1301 }
1302 static final int RESTRHASH(int r, int var) {
1303 return PAIR(r, var);
1304 }
1305 static final int CONSTRAINHASH(int f, int c) {
1306 return PAIR(f, c);
1307 }
1308 static final int QUANTHASH(int r) {
1309 return r;
1310 }
1311 static final int REPLACEHASH(int r) {
1312 return r;
1313 }
1314 static final int VECCOMPOSEHASH(int f) {
1315 return f;
1316 }
1317 static final int COMPOSEHASH(int f, int g) {
1318 return PAIR(f, g);
1319 }
1320 static final int SATCOUHASH(int r) {
1321 return r;
1322 }
1323 static final int PATHCOUHASH(int r) {
1324 return r;
1325 }
1326 static final int APPEXHASH(int l, int r, int op) {
1327
1328 return (l ^ r ^ op);
1329 }
1330 static final int APPEX3HASH(int a, int b, int c, int op) {
1331
1332 return (a ^ b ^ c ^ op);
1333 }
1334
1335 static final double M_LN2 = 0.69314718055994530942;
1336
1337 static double log1p(double a) {
1338 return Math.log(1.0 + a);
1339 }
1340
1341 final boolean INVARSET(int a) {
1342 return (quantvarset[a] == quantvarsetID);
1343 }
1344 final boolean INSVARSET(int a) {
1345 return Math.abs(quantvarset[a]) == quantvarsetID;
1346 }
1347
1348 static final int bddop_and = 0;
1349 static final int bddop_xor = 1;
1350 static final int bddop_or = 2;
1351 static final int bddop_nand = 3;
1352 static final int bddop_nor = 4;
1353 static final int bddop_imp = 5;
1354 static final int bddop_biimp = 6;
1355 static final int bddop_diff = 7;
1356 static final int bddop_less = 8;
1357 static final int bddop_invimp = 9;
1358
1359
1360 static final int bddop_not = 10;
1361 static final int bddop_simplify = 11;
1362
1363 int bdd_not(int r) {
1364 int res;
1365 int numReorder = 1;
1366 CHECKa(r, bddfalse);
1367
1368 if (singlecache == null) singlecache = new OpCache1(cachesize);
1369
1370 again : for (;;) {
1371 try {
1372 INITREF();
1373 if (numReorder == 0) bdd_disable_reorder();
1374 res = not_rec(r);
1375 if (numReorder == 0) bdd_enable_reorder();
1376 } catch (ReorderException x) {
1377 bdd_checkreorder();
1378 numReorder--;
1379 continue again;
1380 }
1381 break;
1382 }
1383
1384 checkresize();
1385 return res;
1386 }
1387
1388 int not_rec(int r) {
1389 OpCache1Entry entry;
1390 int res;
1391
1392 if (ISCONST(r))
1393 return 1 - r;
1394
1395 entry = singlecache.lookup(NOTHASH(r));
1396 if ((res = singlecache.get_sid(entry, r, bddop_not << NODE_BITS)) >= 0) {
1397 return res;
1398 }
1399
1400 PUSHREF(not_rec(LOW(r)));
1401 PUSHREF(not_rec(HIGH(r)));
1402 res = bdd_makenode(LEVEL(r), READREF(2), READREF(1));
1403 POPREF(2);
1404
1405 singlecache.set_sid(entry, r, bddop_not << NODE_BITS, res);
1406
1407 return res;
1408 }
1409
1410 int bdd_ite(int f, int g, int h) {
1411 int res;
1412 int numReorder = 1;
1413
1414 CHECKa(f, bddfalse);
1415 CHECKa(g, bddfalse);
1416 CHECKa(h, bddfalse);
1417
1418 if (itecache == null) itecache = new OpCache3(cachesize);
1419 if (singlecache == null) singlecache = new OpCache1(cachesize);
1420
1421 again : for (;;) {
1422 try {
1423 INITREF();
1424 if (numReorder == 0) bdd_disable_reorder();
1425 res = ite_rec(f, g, h);
1426 if (numReorder == 0) bdd_enable_reorder();
1427 } catch (ReorderException x) {
1428 bdd_checkreorder();
1429 numReorder--;
1430 continue again;
1431 }
1432 break;
1433 }
1434
1435 checkresize();
1436 return res;
1437 }
1438
1439 int ite_rec(int f, int g, int h) {
1440 OpCache3Entry entry;
1441 int res;
1442
1443 if (ISONE(f)) return g;
1444 if (ISZERO(f)) return h;
1445 if (g == h) return g;
1446 if (ISONE(g) && ISZERO(h)) return f;
1447 if (ISZERO(g) && ISONE(h)) return not_rec(f);
1448
1449 entry = itecache.lookup(ITEHASH(f, g, h));
1450 if ((res = itecache.get(entry, f, g, h)) >= 0) {
1451 return res;
1452 }
1453
1454 int LEVEL_f = LEVEL(f);
1455 int LEVEL_g = LEVEL(g);
1456 int LEVEL_h = LEVEL(h);
1457 if (LEVEL_f == LEVEL_g) {
1458 if (LEVEL_f == LEVEL_h) {
1459 PUSHREF(ite_rec(LOW(f), LOW(g), LOW(h)));
1460 PUSHREF(ite_rec(HIGH(f), HIGH(g), HIGH(h)));
1461 res = bdd_makenode(LEVEL_f, READREF(2), READREF(1));
1462 } else if (LEVEL_f < LEVEL_h) {
1463 PUSHREF(ite_rec(LOW(f), LOW(g), h));
1464 PUSHREF(ite_rec(HIGH(f), HIGH(g), h));
1465 res = bdd_makenode(LEVEL_f, READREF(2), READREF(1));
1466 } else
1467 PUSHREF(ite_rec(f, g, LOW(h)));
1468 PUSHREF(ite_rec(f, g, HIGH(h)));
1469 res = bdd_makenode(LEVEL_h, READREF(2), READREF(1));
1470 }
1471 } else if (LEVEL_f < LEVEL_g) {
1472 if (LEVEL_f == LEVEL_h) {
1473 PUSHREF(ite_rec(LOW(f), g, LOW(h)));
1474 PUSHREF(ite_rec(HIGH(f), g, HIGH(h)));
1475 res = bdd_makenode(LEVEL_f, READREF(2), READREF(1));
1476 } else if (LEVEL_f < LEVEL_h) {
1477 PUSHREF(ite_rec(LOW(f), g, h));
1478 PUSHREF(ite_rec(HIGH(f), g, h));
1479 res = bdd_makenode(LEVEL_f, READREF(2), READREF(1));
1480 } else
1481 PUSHREF(ite_rec(f, g, LOW(h)));
1482 PUSHREF(ite_rec(f, g, HIGH(h)));
1483 res = bdd_makenode(LEVEL_h, READREF(2), READREF(1));
1484 }
1485 } else
1486 if (LEVEL_g == LEVEL_h) {
1487 PUSHREF(ite_rec(f, LOW(g), LOW(h)));
1488 PUSHREF(ite_rec(f, HIGH(g), HIGH(h)));
1489 res = bdd_makenode(LEVEL_g, READREF(2), READREF(1));
1490 } else if (LEVEL_g < LEVEL_h) {
1491 PUSHREF(ite_rec(f, LOW(g), h));
1492 PUSHREF(ite_rec(f, HIGH(g), h));
1493 res = bdd_makenode(LEVEL_g, READREF(2), READREF(1));
1494 } else
1495 PUSHREF(ite_rec(f, g, LOW(h)));
1496 PUSHREF(ite_rec(f, g, HIGH(h)));
1497 res = bdd_makenode(LEVEL_h, READREF(2), READREF(1));
1498 }
1499 }
1500
1501 POPREF(2);
1502
1503 itecache.set(entry, f, g, h, res);
1504
1505 return res;
1506 }
1507
1508 int bdd_replace(int r, bddPair pair) {
1509 int res;
1510 int numReorder = 1;
1511
1512 CHECKa(r, bddfalse);
1513
1514 if (replacecache == null) replacecache = new OpCache2(cachesize);
1515
1516 again : for (;;) {
1517 try {
1518 INITREF();
1519 replacepair = pair.result;
1520 replacelast = pair.last;
1521 replaceid = (pair.id << 1) | CACHEID_REPLACE;
1522 if (numReorder == 0) bdd_disable_reorder();
1523 res = replace_rec(r);
1524 if (numReorder == 0) bdd_enable_reorder();
1525 } catch (ReorderException x) {
1526 bdd_checkreorder();
1527 numReorder--;
1528 continue again;
1529 }
1530 break;
1531 }
1532
1533 checkresize();
1534 return res;
1535 }
1536
1537 int replace_rec(int r) {
1538 OpCache2Entry entry;
1539 int res;
1540
1541 if (ISCONST(r) || LEVEL(r) > replacelast) return r;
1542
1543 entry = replacecache.lookup(REPLACEHASH(r));
1544 if ((res = replacecache.get(entry, r, replaceid)) >= 0) {
1545 return res;
1546 }
1547
1548 PUSHREF(replace_rec(LOW(r)));
1549 PUSHREF(replace_rec(HIGH(r)));
1550
1551 res = bdd_correctify(LEVEL(replacepair[LEVEL(r)]), READREF(2), READREF(1));
1552 POPREF(2);
1553
1554 replacecache.set(entry, r, replaceid, res);
1555
1556 return res;
1557 }
1558
1559 int bdd_correctify(int level, int l, int r) {
1560 int res;
1561
1562 if (level < LEVEL(l) && level < LEVEL(r))
1563 return bdd_makenode(level, l, r);
1564
1565 if (level == LEVEL(l) || level == LEVEL(r)) {
1566 bdd_error(BDD_REPLACE);
1567 return 0;
1568 }
1569
1570 if (LEVEL(l) == LEVEL(r)) {
1571 PUSHREF(bdd_correctify(level, LOW(l), LOW(r)));
1572 PUSHREF(bdd_correctify(level, HIGH(l), HIGH(r)));
1573 res = bdd_makenode(LEVEL(l), READREF(2), READREF(1));
1574 } else if (LEVEL(l) < LEVEL(r)) {
1575 PUSHREF(bdd_correctify(level, LOW(l), r));
1576 PUSHREF(bdd_correctify(level, HIGH(l), r));
1577 res = bdd_makenode(LEVEL(l), READREF(2), READREF(1));
1578 } else {
1579 PUSHREF(bdd_correctify(level, l, LOW(r)));
1580 PUSHREF(bdd_correctify(level, l, HIGH(r)));
1581 res = bdd_makenode(LEVEL(r), READREF(2), READREF(1));
1582 }
1583 POPREF(2);
1584
1585 return res;
1586 }
1587
1588 int bdd_apply(int l, int r, int op) {
1589 int res;
1590 int numReorder = 1;
1591
1592 CHECKa(l, bddfalse);
1593 CHECKa(r, bddfalse);
1594
1595 if (op < 0 || op > bddop_invimp) {
1596 bdd_error(BDD_OP);
1597 return bddfalse;
1598 }
1599
1600 switch (op) {
1601 case bddop_and:
1602 if (andcache == null) andcache = new OpCache2(cachesize);
1603 break;
1604 case bddop_or:
1605 if (orcache == null) orcache = new OpCache2(cachesize);
1606 break;
1607 default:
1608 if (applycache == null) applycache = new OpCache2(cachesize);
1609 break;
1610 }
1611
1612 again : for (;;) {
1613 try {
1614 INITREF();
1615 applyop = op;
1616 if (numReorder == 0) bdd_disable_reorder();
1617 switch (op) {
1618 case bddop_and: res = and_rec(l, r); break;
1619 case bddop_or: res = or_rec(l, r); break;
1620 default: res = apply_rec(l, r); break;
1621 }
1622 if (numReorder == 0) bdd_enable_reorder();
1623 } catch (ReorderException x) {
1624 bdd_checkreorder();
1625 numReorder--;
1626 continue again;
1627 }
1628 break;
1629 }
1630
1631 checkresize();
1632 return res;
1633 }
1634
1635 int apply_rec(int l, int r) {
1636 OpCache2Entry entry;
1637 int res;
1638
1639 if (VERIFY_ASSERTIONS) _assert(applyop != bddop_and && applyop != bddop_or);
1640
1641 switch (applyop) {
1642 case bddop_xor :
1643 if (l == r)
1644 return 0;
1645 if (ISZERO(l))
1646 return r;
1647 if (ISZERO(r))
1648 return l;
1649 break;
1650 case bddop_nand :
1651 if (ISZERO(l) || ISZERO(r))
1652 return 1;
1653 break;
1654 case bddop_nor :
1655 if (ISONE(l) || ISONE(r))
1656 return 0;
1657 break;
1658 case bddop_imp :
1659 if (ISZERO(l))
1660 return 1;
1661 if (ISONE(l))
1662 return r;
1663 if (ISONE(r))
1664 return 1;
1665 break;
1666 }
1667
1668 if (ISCONST(l) && ISCONST(r))
1669 res = oprres[applyop][l << 1 | r];
1670 else {
1671 entry = applycache.lookup(APPLYHASH(l, r, applyop));
1672 if ((res = applycache.get_sid(entry, l, r, applyop << NODE_BITS)) >= 0) {
1673 return res;
1674 }
1675
1676 int LEVEL_l = LEVEL(l);
1677 int LEVEL_r = LEVEL(r);
1678 if (LEVEL_l == LEVEL_r) {
1679 PUSHREF(apply_rec(LOW(l), LOW(r)));
1680 PUSHREF(apply_rec(HIGH(l), HIGH(r)));
1681 res = bdd_makenode(LEVEL_l, READREF(2), READREF(1));
1682 } else if (LEVEL_l < LEVEL_r) {
1683 PUSHREF(apply_rec(LOW(l), r));
1684 PUSHREF(apply_rec(HIGH(l), r));
1685 res = bdd_makenode(LEVEL_l, READREF(2), READREF(1));
1686 } else {
1687 PUSHREF(apply_rec(l, LOW(r)));
1688 PUSHREF(apply_rec(l, HIGH(r)));
1689 res = bdd_makenode(LEVEL_r, READREF(2), READREF(1));
1690 }
1691
1692 POPREF(2);
1693
1694 applycache.set_sid(entry, l, r, applyop << NODE_BITS, res);
1695 }
1696
1697 return res;
1698 }
1699
1700 int and_rec(int l, int r) {
1701 OpCache2Entry entry;
1702 int res;
1703
1704 if (l == r) return l;
1705 if (ISZERO(l) || ISZERO(r)) return 0;
1706 if (ISONE(l)) return r;
1707 if (ISONE(r)) return l;
1708
1709 if (ORDER_CACHE && l < r) { int t = l; l = r; r = t; }
1710
1711 entry = andcache.lookup(ANDHASH(l, r));
1712 if ((res = andcache.get(entry, l, r)) >= 0) {
1713 return res;
1714 }
1715
1716 int LEVEL_l = LEVEL(l);
1717 int LEVEL_r = LEVEL(r);
1718 if (LEVEL_l == LEVEL_r) {
1719 PUSHREF(and_rec(LOW(l), LOW(r)));
1720 PUSHREF(and_rec(HIGH(l), HIGH(r)));
1721 res = bdd_makenode(LEVEL_l, READREF(2), READREF(1));
1722 } else if (LEVEL_l < LEVEL_r) {
1723 PUSHREF(and_rec(LOW(l), r));
1724 PUSHREF(and_rec(HIGH(l), r));
1725 res = bdd_makenode(LEVEL_l, READREF(2), READREF(1));
1726 } else {
1727 PUSHREF(and_rec(l, LOW(r)));
1728 PUSHREF(and_rec(l, HIGH(r)));
1729 res = bdd_makenode(LEVEL_r, READREF(2), READREF(1));
1730 }
1731
1732 POPREF(2);
1733
1734 andcache.set(entry, l, r, res);
1735
1736 return res;
1737 }
1738
1739 int or_rec(int l, int r) {
1740 OpCache2Entry entry;
1741 int res;
1742
1743 if (l == r) return l;
1744 if (ISONE(l) || ISONE(r)) return 1;
1745 if (ISZERO(l)) return r;
1746 if (ISZERO(r)) return l;
1747
1748 if (l < r) { int t = l; l = r; r = t; }
1749
1750 entry = orcache.lookup(ORHASH(l, r));
1751 if ((res = orcache.get(entry, l, r)) >= 0) {
1752 return res;
1753 }
1754
1755 int LEVEL_l = LEVEL(l);
1756 int LEVEL_r = LEVEL(r);
1757 if (LEVEL_l == LEVEL_r) {
1758 PUSHREF(or_rec(LOW(l), LOW(r)));
1759 PUSHREF(or_rec(HIGH(l), HIGH(r)));
1760 res = bdd_makenode(LEVEL_l, READREF(2), READREF(1));
1761 } else if (LEVEL_l < LEVEL_r) {
1762 PUSHREF(or_rec(LOW(l), r));
1763 PUSHREF(or_rec(HIGH(l), r));
1764 res = bdd_makenode(LEVEL_l, READREF(2), READREF(1));
1765 } else {
1766 PUSHREF(or_rec(l, LOW(r)));
1767 PUSHREF(or_rec(l, HIGH(r)));
1768 res = bdd_makenode(LEVEL_r, READREF(2), READREF(1));
1769 }
1770
1771 POPREF(2);
1772
1773 orcache.set(entry, l, r, res);
1774
1775 return res;
1776 }
1777
1778 int bdd_relprod(int a, int b, int var) {
1779 return bdd_appex(a, b, bddop_and, var);
1780 }
1781
1782 int bdd_relprod3(int a, int b, int c, int var) {
1783 int res;
1784 int numReorder = 1;
1785
1786 CHECKa(a, bddfalse);
1787 CHECKa(b, bddfalse);
1788 CHECKa(c, bddfalse);
1789 CHECKa(var, bddfalse);
1790
1791 if (ISCONST(var)) {
1792
1793 res = bdd_apply(a, b, bddop_and);
1794 return bdd_apply(res, c, bddop_and);
1795 }
1796
1797 if (andcache == null) andcache = new OpCache2(cachesize);
1798 if (appexcache == null) appexcache = new OpCache3(cachesize);
1799 if (appex3cache == null) appex3cache = new OpCache4(cachesize);
1800 if (orcache == null) orcache = new OpCache2(cachesize);
1801 if (quantcache == null) quantcache = new OpCache2(cachesize);
1802
1803 again : for (;;) {
1804 if (varset2vartable(var) < 0)
1805 return bddfalse;
1806 try {
1807 INITREF();
1808 applyop = bddop_or;
1809 appexop = bddop_and;
1810 appexid = (var << 7) | (appexop << 3) | CACHEID_APPEX;
1811 quantid = appexid;
1812 if (numReorder == 0) bdd_disable_reorder();
1813 res = relprod3_rec(a, b, c);
1814 if (numReorder == 0) bdd_enable_reorder();
1815 } catch (ReorderException x) {
1816 bdd_checkreorder();
1817 numReorder--;
1818 continue again;
1819 }
1820 break;
1821 }
1822
1823 checkresize();
1824 return res;
1825 }
1826
1827 int bdd_appex(int l, int r, int opr, int var) {
1828 int res;
1829 int numReorder = 1;
1830
1831 CHECKa(l, bddfalse);
1832 CHECKa(r, bddfalse);
1833 CHECKa(var, bddfalse);
1834
1835 if (opr < 0 || opr > bddop_invimp) {
1836 bdd_error(BDD_OP);
1837 return bddfalse;
1838 }
1839
1840 if (ISCONST(var))
1841 return bdd_apply(l, r, opr);
1842
1843 switch (opr) {
1844 case bddop_and:
1845 if (andcache == null) andcache = new OpCache2(cachesize);
1846 break;
1847 default:
1848 if (applycache == null) applycache = new OpCache2(cachesize);
1849 break;
1850 }
1851 if (appexcache == null) appexcache = new OpCache3(cachesize);
1852 if (orcache == null) orcache = new OpCache2(cachesize);
1853 if (quantcache == null) quantcache = new OpCache2(cachesize);
1854
1855 again : for (;;) {
1856 if (varset2vartable(var) < 0)
1857 return bddfalse;
1858 try {
1859 INITREF();
1860 applyop = bddop_or;
1861 appexop = opr;
1862 appexid = (var << 7) | (appexop << 3) | CACHEID_APPEX;
1863 quantid = appexid;
1864 if (numReorder == 0) bdd_disable_reorder();
1865 if (opr == bddop_and)
1866 res = relprod_rec(l, r);
1867 else
1868 res = appquant_rec(l, r);
1869 if (numReorder == 0) bdd_enable_reorder();
1870 } catch (ReorderException x) {
1871 bdd_checkreorder();
1872 numReorder--;
1873 continue again;
1874 }
1875 break;
1876 }
1877
1878 checkresize();
1879 return res;
1880 }
1881
1882 int bdd_appall(int l, int r, int opr, int var) {
1883 int res;
1884 int numReorder = 1;
1885
1886 CHECKa(l, bddfalse);
1887 CHECKa(r, bddfalse);
1888 CHECKa(var, bddfalse);
1889
1890 if (opr < 0 || opr > bddop_invimp) {
1891 bdd_error(BDD_OP);
1892 return bddfalse;
1893 }
1894
1895 if (var < 2)
1896 return bdd_apply(l, r, opr);
1897
1898 switch (opr) {
1899 case bddop_or:
1900 if (orcache == null) orcache = new OpCache2(cachesize);
1901 break;
1902 default:
1903 if (applycache == null) applycache = new OpCache2(cachesize);
1904 break;
1905 }
1906 if (appexcache == null) appexcache = new OpCache3(cachesize);
1907 if (andcache == null) andcache = new OpCache2(cachesize);
1908 if (quantcache == null) quantcache = new OpCache2(cachesize);
1909
1910 again : for (;;) {
1911 if (varset2vartable(var) < 0)
1912 return bddfalse;
1913 try {
1914 INITREF();
1915 applyop = bddop_and;
1916 appexop = opr;
1917 appexid = (var << 7) | (appexop << 3) | CACHEID_APPAL;
1918 quantid = appexid;
1919 if (numReorder == 0) bdd_disable_reorder();
1920 res = appquant_rec(l, r);
1921 if (numReorder == 0) bdd_enable_reorder();
1922 } catch (ReorderException x) {
1923 bdd_checkreorder();
1924 numReorder--;
1925 continue again;
1926 }
1927 break;
1928 }
1929
1930 checkresize();
1931 return res;
1932 }
1933
1934 int bdd_appuni(int l, int r, int opr, int var) {
1935 int res;
1936 int numReorder = 1;
1937
1938 CHECKa(l, bddfalse);
1939 CHECKa(r, bddfalse);
1940 CHECKa(var, bddfalse);
1941
1942 if (opr < 0 || opr > bddop_invimp) {
1943 bdd_error(BDD_OP);
1944 return bddfalse;
1945 }
1946
1947 if (var < 2)
1948 return bdd_apply(l, r, opr);
1949
1950 switch (opr) {
1951 case bddop_and:
1952 if (andcache == null) andcache = new OpCache2(cachesize);
1953 break;
1954 case bddop_or:
1955 if (orcache == null) orcache = new OpCache2(cachesize);
1956 break;
1957 default:
1958 if (applycache == null) applycache = new OpCache2(cachesize);
1959 break;
1960 }
1961 if (appexcache == null) appexcache = new OpCache3(cachesize);
1962 if (quantcache == null) quantcache = new OpCache2(cachesize);
1963
1964 again : for (;;) {
1965 try {
1966 INITREF();
1967 applyop = bddop_xor;
1968 appexop = opr;
1969 appexid = (var << 7) | (appexop << 3) | CACHEID_APPUN;
1970 quantid = appexid;
1971 if (numReorder == 0) bdd_disable_reorder();
1972 res = appuni_rec(l, r, var);
1973 if (numReorder == 0) bdd_enable_reorder();
1974 } catch (ReorderException x) {
1975 bdd_checkreorder();
1976 numReorder--;
1977 continue again;
1978 }
1979 break;
1980 }
1981
1982 checkresize();
1983 return res;
1984 }
1985
1986 int varset2vartable(int r) {
1987 int n;
1988
1989 if (r < 2) return bdd_error(BDD_VARSET);
1990
1991 quantvarsetID++;
1992 if (quantvarsetID == Integer.MAX_VALUE) {
1993 for (int i = 0; i < bddvarnum; ++i)
1994 quantvarset[i] = 0;
1995 quantvarsetID = 1;
1996 }
1997
1998 quantlast = -1;
1999 for (n = r; n > 1; n = HIGH(n)) {
2000 quantvarset[LEVEL(n)] = quantvarsetID;
2001 if (VERIFY_ASSERTIONS) _assert(quantlast < LEVEL(n));
2002 quantlast = LEVEL(n);
2003 }
2004
2005 return 0;
2006 }
2007
2008 int varset2svartable(int r) {
2009 int n;
2010
2011 if (r < 2) return bdd_error(BDD_VARSET);
2012
2013 quantvarsetID++;
2014
2015 if (quantvarsetID == Integer.MAX_VALUE / 2) {
2016 for (int i = 0; i < bddvarnum; ++i)
2017 quantvarset[i] = 0;
2018 quantvarsetID = 1;
2019 }
2020
2021 quantlast = 0;
2022 for (n = r; !ISCONST(n); ) {
2023 if (ISZERO(LOW(n))) {
2024 quantvarset[LEVEL(n)] = quantvarsetID;
2025 n = HIGH(n);
2026 } else {
2027 quantvarset[LEVEL(n)] = -quantvarsetID;
2028 n = LOW(n);
2029 }
2030 if (VERIFY_ASSERTIONS) _assert(quantlast < LEVEL(n));
2031 quantlast = LEVEL(n);
2032 }
2033
2034 return 0;
2035 }
2036
2037 int appquant_rec(int l, int r) {
2038 OpCache3Entry entry;
2039 int res;
2040
2041 if (VERIFY_ASSERTIONS) _assert(appexop != bddop_and);
2042
2043 switch (appexop) {
2044 case bddop_or :
2045 if (l == 1 || r == 1) return 1;
2046 if (l == r) return quant_rec(l);
2047 if (l == 0) return quant_rec(r);
2048 if (r == 0) return quant_rec(l);
2049 break;
2050 case bddop_xor :
2051 if (l == r) return 0;
2052 if (l == 0) return quant_rec(r);
2053 if (r == 0) return quant_rec(l);
2054 break;
2055 case bddop_nand :
2056 if (l == 0 || r == 0) return 1;
2057 break;
2058 case bddop_nor :
2059 if (l == 1 || r == 1) return 0;
2060 break;
2061 }
2062
2063 if (ISCONST(l) && ISCONST(r))
2064 return oprres[appexop][(l << 1) | r];
2065
2066 int LEVEL_l = LEVEL(l);
2067 int LEVEL_r = LEVEL(r);
2068 if (LEVEL_l > quantlast && LEVEL_r > quantlast) {
2069 int oldop = applyop;
2070 applyop = appexop;
2071 switch (applyop) {
2072 case bddop_and: res = and_rec(l, r); break;
2073 case bddop_or: res = or_rec(l, r); break;
2074 default: res = apply_rec(l, r); break;
2075 }
2076 applyop = oldop;
2077 return res;
2078 }
2079 entry = appexcache.lookup(APPEXHASH(l, r, appexop));
2080 if ((res = appexcache.get(entry, l, r, appexid)) >= 0) {
2081 return res;
2082 }
2083
2084 int lev;
2085 if (LEVEL_l == LEVEL_r) {
2086 PUSHREF(appquant_rec(LOW(l), LOW(r)));
2087 PUSHREF(appquant_rec(HIGH(l), HIGH(r)));
2088 lev = LEVEL_l;
2089 } else if (LEVEL_l < LEVEL_r) {
2090 PUSHREF(appquant_rec(LOW(l), r));
2091 PUSHREF(appquant_rec(HIGH(l), r));
2092 lev = LEVEL_l;
2093 } else {
2094 PUSHREF(appquant_rec(l, LOW(r)));
2095 PUSHREF(appquant_rec(l, HIGH(r)));
2096 lev = LEVEL_r;
2097 }
2098 if (INVARSET(lev)) {
2099 int r2 = READREF(2), r1 = READREF(1);
2100 switch (applyop) {
2101 case bddop_and: res = and_rec(r2, r1); break;
2102 case bddop_or: res = or_rec(r2, r1); break;
2103 default: res = apply_rec(r2, r1); break;
2104 }
2105 } else {
2106 res = bdd_makenode(lev, READREF(2), READREF(1));
2107 }
2108
2109 POPREF(2);
2110
2111 appexcache.set(entry, l, r, appexid, res);
2112
2113 return res;
2114 }
2115
2116 int relprod_rec(int l, int r) {
2117 OpCache3Entry entry;
2118 int res;
2119
2120 if (l == 0 || r == 0) return 0;
2121 if (l == r) return quant_rec(l);
2122 if (l == 1) return quant_rec(r);
2123 if (r == 1) return quant_rec(l);
2124
2125 if (l < r) { int t = l; l = r; r = t; }
2126
2127 int LEVEL_l = LEVEL(l);
2128 int LEVEL_r = LEVEL(r);
2129 if (LEVEL_l > quantlast && LEVEL_r > quantlast) {
2130 applyop = bddop_and;
2131 res = and_rec(l, r);
2132 applyop = bddop_or;
2133 return res;
2134 }
2135
2136 entry = appexcache.lookup(APPEXHASH(l, r, appexop));
2137 if ((res = appexcache.get(entry, l, r, appexid)) >= 0) {
2138 return res;
2139 }
2140
2141 int lev;
2142 if (LEVEL_l == LEVEL_r) {
2143 PUSHREF(relprod_rec(LOW(l), LOW(r)));
2144 PUSHREF(relprod_rec(HIGH(l), HIGH(r)));
2145 lev = LEVEL_l;
2146 } else if (LEVEL_l < LEVEL_r) {
2147 PUSHREF(relprod_rec(LOW(l), r));
2148 PUSHREF(relprod_rec(HIGH(l), r));
2149 lev = LEVEL_l;
2150 } else {
2151 PUSHREF(relprod_rec(l, LOW(r)));
2152 PUSHREF(relprod_rec(l, HIGH(r)));
2153 lev = LEVEL_r;
2154 }
2155 if (INVARSET(lev))
2156 res = or_rec(READREF(2), READREF(1));
2157 else
2158 res = bdd_makenode(lev, READREF(2), READREF(1));
2159
2160 POPREF(2);
2161
2162 appexcache.set(entry, l, r, appexid, res);
2163
2164 return res;
2165 }
2166
2167 int relprod3_rec(int a, int b, int c) {
2168 OpCache4Entry entry;
2169 int res;
2170
2171 if (a == 0 || b == 0 || c == 0) return 0;
2172 if (a == b || a == 1) return relprod_rec(b, c);
2173 if (b == c || b == 1) return relprod_rec(a, c);
2174 if (c == a || c == 1) return relprod_rec(a, b);
2175
2176 int LEVEL_a = LEVEL(a);
2177 int LEVEL_b = LEVEL(b);
2178 int LEVEL_c = LEVEL(c);
2179 if (LEVEL_a > quantlast && LEVEL_b > quantlast && LEVEL_c > quantlast) {
2180 applyop = bddop_and;
2181 res = and_rec(a, b);
2182 res = and_rec(res, c);
2183 applyop = bddop_or;
2184 return res;
2185 }
2186
2187 entry = appex3cache.lookup(APPEX3HASH(a, b, c, appexop));
2188 if ((res = appex3cache.get(entry, a, b, c, appexid)) >= 0) {
2189 return res;
2190 }
2191
2192 int x1, x2, x3, y1, y2, y3, lev;
2193 x1 = y1 = a;
2194 x2 = y2 = b;
2195 x3 = y3 = c;
2196 if (LEVEL_b < LEVEL_c) {
2197 if (LEVEL_a < LEVEL_b) {
2198
2199 x1 = LOW(a); y1 = HIGH(a); lev = LEVEL_a;
2200 } else {
2201 x2 = LOW(b); y2 = HIGH(b); lev = LEVEL_b;
2202 if (LEVEL_a == LEVEL_b) {
2203
2204 x1 = LOW(a); y1 = HIGH(a);
2205 }
2206 }
2207 } else if (LEVEL_b == LEVEL_c) {
2208 if (LEVEL_a < LEVEL_b) {
2209
2210 x1 = LOW(a); y1 = HIGH(a); lev = LEVEL_a;
2211 } else {
2212 x2 = LOW(b); y2 = HIGH(b); lev = LEVEL_b;
2213 x3 = LOW(c); y3 = HIGH(c);
2214 if (LEVEL_a == LEVEL_b) {
2215
2216 x1 = LOW(a); y1 = HIGH(a);
2217 }
2218 }
2219 } else if (LEVEL_a < LEVEL_c) {
2220
2221 x1 = LOW(a); y1 = HIGH(a); lev = LEVEL_a;
2222 } else {
2223 x3 = LOW(c); y3 = HIGH(c); lev = LEVEL_c;
2224 if (LEVEL_a == LEVEL_c) {
2225 x1 = LOW(a); y1 = HIGH(a);
2226 }
2227 }
2228
2229 PUSHREF(relprod3_rec(x1, x2, x3));
2230 PUSHREF(relprod3_rec(y1, y2, y3));
2231 if (INVARSET(lev)) {
2232 res = or_rec(READREF(2), READREF(1));
2233 } else {
2234 res = bdd_makenode(lev, READREF(2), READREF(1));
2235 }
2236
2237 POPREF(2);
2238
2239 appex3cache.set(entry, a, b, c, appexid, res);
2240
2241 return res;
2242 }
2243
2244 int appuni_rec(int l, int r, int var) {
2245 OpCache3Entry entry;
2246 int res;
2247
2248 int LEVEL_l, LEVEL_r, LEVEL_var;
2249 LEVEL_l = LEVEL(l);
2250 LEVEL_r = LEVEL(r);
2251 LEVEL_var = LEVEL(var);
2252
2253 if (LEVEL_l > LEVEL_var && LEVEL_r > LEVEL_var) {
2254
2255 return BDDZERO;
2256 }
2257
2258 if (ISCONST(l) && ISCONST(r)) {
2259 res = oprres[appexop][(l << 1) | r];
2260 return res;
2261 } else if (ISCONST(var)) {
2262 int oldop = applyop;
2263 applyop = appexop;
2264 switch (applyop) {
2265 case bddop_and: res = and_rec(l, r); break;
2266 case bddop_or: res = or_rec(l, r); break;
2267 default: res = apply_rec(l, r); break;
2268 }
2269 applyop = oldop;
2270 return res;
2271 }
2272 entry = appexcache.lookup(APPEXHASH(l, r, appexop));
2273 if ((res = appexcache.get(entry, l, r, appexid)) >= 0) {
2274 return res;
2275 }
2276
2277 int lev;
2278 if (LEVEL_l == LEVEL_r) {
2279 if (LEVEL_l == LEVEL_var) {
2280 lev = -1;
2281 var = HIGH(var);
2282 } else {
2283 lev = LEVEL_l;
2284 }
2285 PUSHREF(appuni_rec(LOW(l), LOW(r), var));
2286 PUSHREF(appuni_rec(HIGH(l), HIGH(r), var));
2287 lev = LEVEL_l;
2288 } else if (LEVEL_l < LEVEL_r) {
2289 if (LEVEL_l == LEVEL_var) {
2290 lev = -1;
2291 var = HIGH(var);
2292 } else {
2293 lev = LEVEL_l;
2294 }
2295 PUSHREF(appuni_rec(LOW(l), r, var));
2296 PUSHREF(appuni_rec(HIGH(l), r, var));
2297 } else {
2298 if (LEVEL_r == LEVEL_var) {
2299 lev = -1;
2300 var = HIGH(var);
2301 } else {
2302 lev = LEVEL_r;
2303 }
2304 PUSHREF(appuni_rec(l, LOW(r), var));
2305 PUSHREF(appuni_rec(l, HIGH(r), var));
2306 }
2307 if (lev == -1) {
2308 int r2 = READREF(2), r1 = READREF(1);
2309 switch (applyop) {
2310 case bddop_and: res = and_rec(r2, r1); break;
2311 case bddop_or: res = or_rec(r2, r1); break;
2312 default: res = apply_rec(r2, r1); break;
2313 }
2314 } else {
2315 res = bdd_makenode(lev, READREF(2), READREF(1));
2316 }
2317
2318 POPREF(2);
2319
2320 appexcache.set(entry, l, r, appexid, res);
2321
2322 return res;
2323 }
2324
2325 int bdd_constrain(int f, int c) {
2326 int res;
2327 int numReorder = 1;
2328
2329 CHECKa(f, bddfalse);
2330 CHECKa(c, bddfalse);
2331
2332 if (misccache == null) misccache = new OpCache2(cachesize);
2333
2334 again : for (;;) {
2335 try {
2336 INITREF();
2337 miscid = CACHEID_CONSTRAIN << NODE_BITS;
2338 if (numReorder == 0) bdd_disable_reorder();
2339 res = constrain_rec(f, c);
2340 if (numReorder == 0) bdd_enable_reorder();
2341 } catch (ReorderException x) {
2342 bdd_checkreorder();
2343 numReorder--;
2344 continue again;
2345 }
2346 break;
2347 }
2348
2349 checkresize();
2350 return res;
2351 }
2352
2353 int constrain_rec(int f, int c) {
2354 OpCache2Entry entry;
2355 int res;
2356
2357 if (ISONE(c)) return f;
2358 if (ISCONST(f)) return f;
2359 if (c == f) return BDDONE;
2360 if (ISZERO(c)) return BDDZERO;
2361
2362 entry = misccache.lookup(CONSTRAINHASH(f, c));
2363 if ((res = misccache.get_sid(entry, f, c, miscid)) >= 0) {
2364 return res;
2365 }
2366
2367 int LEVEL_f = LEVEL(f);
2368 int LEVEL_c = LEVEL(c);
2369 if (LEVEL_f == LEVEL_c) {
2370 int LOW_c = LOW(c);
2371 int HIGH_c = HIGH(c);
2372 if (ISZERO(LOW_c))
2373 res = constrain_rec(HIGH(f), HIGH_c);
2374 else if (ISZERO(HIGH_c))
2375 res = constrain_rec(LOW(f), LOW_c);
2376 else {
2377 PUSHREF(constrain_rec(LOW(f), LOW_c));
2378 PUSHREF(constrain_rec(HIGH(f), HIGH_c));
2379 res = bdd_makenode(LEVEL_f, READREF(2), READREF(1));
2380 POPREF(2);
2381 }
2382 } else if (LEVEL_f < LEVEL_c) {
2383 PUSHREF(constrain_rec(LOW(f), c));
2384 PUSHREF(constrain_rec(HIGH(f), c));
2385 res = bdd_makenode(LEVEL_f, READREF(2), READREF(1));
2386 POPREF(2);
2387 } else {
2388 int LOW_c = LOW(c);
2389 int HIGH_c = HIGH(c);
2390 if (ISZERO(LOW_c))
2391 res = constrain_rec(f, HIGH_c);
2392 else if (ISZERO(HIGH_c))
2393 res = constrain_rec(f, LOW_c);
2394 else {
2395 PUSHREF(constrain_rec(f, LOW_c));
2396 PUSHREF(constrain_rec(f, HIGH_c));
2397 res = bdd_makenode(LEVEL_c, READREF(2), READREF(1));
2398 POPREF(2);
2399 }
2400 }
2401
2402 misccache.set_sid(entry, f, c, miscid, res);
2403
2404 return res;
2405 }
2406
2407 int bdd_compose(int f, int g, int var) {
2408 int res;
2409 int numReorder = 1;
2410
2411 CHECKa(f, bddfalse);
2412 CHECKa(g, bddfalse);
2413 if (var < 0 || var >= bddvarnum) {
2414 bdd_error(BDD_VAR);
2415 return bddfalse;
2416 }
2417
2418 if (appexcache == null) appexcache = new OpCache3(cachesize);
2419 if (itecache == null) itecache = new OpCache3(cachesize);
2420
2421 again : for (;;) {
2422 try {
2423 INITREF();
2424 composelevel = bddvar2level[var];
2425 appexid = (composelevel << 3) | CACHEID_COMPOSE;
2426 if (numReorder == 0) bdd_disable_reorder();
2427 res = compose_rec(f, g);
2428 if (numReorder == 0) bdd_enable_reorder();
2429 } catch (ReorderException x) {
2430 bdd_checkreorder();
2431 numReorder--;
2432 continue again;
2433 }
2434 break;
2435 }
2436
2437 checkresize();
2438 return res;
2439 }
2440
2441 int compose_rec(int f, int g) {
2442 OpCache3Entry entry;
2443 int res;
2444
2445 int LEVEL_f = LEVEL(f);
2446 if (LEVEL_f > composelevel) return f;
2447
2448 entry = appexcache.lookup(COMPOSEHASH(f, g));
2449 if ((res = appexcache.get(entry, f, g, appexid)) >= 0) {
2450 return res;
2451 }
2452
2453 if (LEVEL_f < composelevel) {
2454 int LEVEL_g = LEVEL(g);
2455 int lev;
2456 if (LEVEL_f == LEVEL_g) {
2457 PUSHREF(compose_rec(LOW(f), LOW(g)));
2458 PUSHREF(compose_rec(HIGH(f), HIGH(g)));
2459 lev = LEVEL_f;
2460 } else if (LEVEL_f < LEVEL_g) {
2461 PUSHREF(compose_rec(LOW(f), g));
2462 PUSHREF(compose_rec(HIGH(f), g));
2463 lev = LEVEL_f;
2464 } else {
2465 PUSHREF(compose_rec(f, LOW(g)));
2466 PUSHREF(compose_rec(f, HIGH(g)));
2467 lev = LEVEL_g;
2468 }
2469 res = bdd_makenode(lev, READREF(2), READREF(1));
2470 POPREF(2);
2471 } else
2472
2473 res = ite_rec(g, HIGH(f), LOW(f));
2474 }
2475
2476 appexcache.set(entry, f, g, appexid, res);
2477
2478 return res;
2479 }
2480
2481 int bdd_veccompose(int f, bddPair pair) {
2482 int res;
2483 int numReorder = 1;
2484
2485 CHECKa(f, bddfalse);
2486
2487 if (singlecache == null) singlecache = new OpCache1(cachesize);
2488 if (replacecache == null) replacecache = new OpCache2(cachesize);
2489 if (itecache == null) itecache = new OpCache3(cachesize);
2490
2491 again : for (;;) {
2492 try {
2493 INITREF();
2494 replacepair = pair.result;
2495 replacelast = pair.last;
2496 replaceid = (pair.id << 1) | CACHEID_VECCOMPOSE;
2497 if (numReorder == 0) bdd_disable_reorder();
2498 res = veccompose_rec(f);
2499 if (numReorder == 0) bdd_enable_reorder();
2500 } catch (ReorderException x) {
2501 bdd_checkreorder();
2502 numReorder--;
2503 continue again;
2504 }
2505 break;
2506 }
2507
2508 checkresize();
2509 return res;
2510 }
2511
2512 int veccompose_rec(int f) {
2513 OpCache2Entry entry;
2514 int res;
2515
2516 int LEVEL_f = LEVEL(f);
2517 if (LEVEL_f > replacelast) return f;
2518
2519 entry = replacecache.lookup(VECCOMPOSEHASH(f));
2520 if ((res = replacecache.get(entry, f, replaceid)) >= 0) {
2521 return res;
2522 }
2523
2524 PUSHREF(veccompose_rec(LOW(f)));
2525 PUSHREF(veccompose_rec(HIGH(f)));
2526 res = ite_rec(replacepair[LEVEL(f)], READREF(1), READREF(2));
2527 POPREF(2);
2528
2529 replacecache.set(entry, f, replaceid, res);
2530
2531 return res;
2532 }
2533
2534 int bdd_exist(int r, int var) {
2535 int res;
2536 int numReorder = 1;
2537
2538 CHECKa(r, bddfalse);
2539 CHECKa(var, bddfalse);
2540
2541 if (ISCONST(var))
2542 return r;
2543
2544 if (quantcache == null) quantcache = new OpCache2(cachesize);
2545 if (orcache == null) orcache = new OpCache2(cachesize);
2546
2547 again : for (;;) {
2548 if (varset2vartable(var) < 0) return bddfalse;
2549 try {
2550 INITREF();
2551 quantid = (var << 3) | CACHEID_EXIST;
2552 applyop = bddop_or;
2553 if (numReorder == 0) bdd_disable_reorder();
2554 res = quant_rec(r);
2555 if (numReorder == 0) bdd_enable_reorder();
2556 } catch (ReorderException x) {
2557 bdd_checkreorder();
2558 numReorder--;
2559 continue again;
2560 }
2561 break;
2562 }
2563
2564 checkresize();
2565 return res;
2566 }
2567
2568 int bdd_forall(int r, int var) {
2569 int res;
2570 int numReorder = 1;
2571
2572 CHECKa(r, bddfalse);
2573 CHECKa(var, bddfalse);
2574
2575 if (var < 2)
2576 return r;
2577
2578 if (quantcache == null) quantcache = new OpCache2(cachesize);
2579 if (andcache == null) andcache = new OpCache2(cachesize);
2580
2581 again : for (;;) {
2582 if (varset2vartable(var) < 0) return bddfalse;
2583 try {
2584 INITREF();
2585 quantid = (var << 3) | CACHEID_FORALL;
2586 applyop = bddop_and;
2587 if (numReorder == 0) bdd_disable_reorder();
2588 res = quant_rec(r);
2589 if (numReorder == 0) bdd_enable_reorder();
2590 } catch (ReorderException x) {
2591 bdd_checkreorder();
2592 numReorder--;
2593 continue again;
2594 }
2595 break;
2596 }
2597
2598 checkresize();
2599 return res;
2600 }
2601
2602 int bdd_unique(int r, int var) {
2603 int res;
2604 int numReorder = 1;
2605
2606 CHECKa(r, bddfalse);
2607 CHECKa(var, bddfalse);
2608
2609 if (var < 2)
2610 return r;
2611
2612 if (quantcache == null) quantcache = new OpCache2(cachesize);
2613 if (applycache == null) applycache = new OpCache2(cachesize);
2614
2615 again : for (;;) {
2616 try {
2617 INITREF();
2618 quantid = (var << 3) | CACHEID_UNIQUE;
2619 applyop = bddop_xor;
2620 if (numReorder == 0) bdd_disable_reorder();
2621 res = unique_rec(r, var);
2622 if (numReorder == 0) bdd_enable_reorder();
2623 } catch (ReorderException x) {
2624 bdd_checkreorder();
2625 numReorder--;
2626 continue again;
2627 }
2628 break;
2629 }
2630
2631 checkresize();
2632 return res;
2633 }
2634
2635 int unique_rec(int r, int q) {
2636 OpCache2Entry entry;
2637 int res;
2638 int LEVEL_r, LEVEL_q;
2639
2640 LEVEL_r = LEVEL(r);
2641 LEVEL_q = LEVEL(q);
2642 if (LEVEL_r > LEVEL_q) {
2643
2644 return BDDZERO;
2645 }
2646
2647 if (r < 2 || q < 2)
2648 return r;
2649
2650 entry = quantcache.lookup(QUANTHASH(r));
2651 if ((res = quantcache.get(entry, r, quantid)) >= 0) {
2652 return res;
2653 }
2654
2655 if (LEVEL_r == LEVEL_q) {
2656 PUSHREF(unique_rec(LOW(r), HIGH(q)));
2657 PUSHREF(unique_rec(HIGH(r), HIGH(q)));
2658 res = apply_rec(READREF(2), READREF(1));
2659 } else {
2660 PUSHREF(unique_rec(LOW(r), q));
2661 PUSHREF(unique_rec(HIGH(r), q));
2662 res = bdd_makenode(LEVEL(r), READREF(2), READREF(1));
2663 }
2664
2665 POPREF(2);
2666
2667 quantcache.set(entry, r, quantid, res);
2668
2669 return res;
2670 }
2671
2672 int quant_rec(int r) {
2673 OpCache2Entry entry;
2674 int res;
2675
2676 if (ISCONST(r) || LEVEL(r) > quantlast) return r;
2677
2678 entry = quantcache.lookup(QUANTHASH(r));
2679 if ((res = quantcache.get(entry, r, quantid)) >= 0) {
2680 return res;
2681 }
2682
2683 PUSHREF(quant_rec(LOW(r)));
2684 PUSHREF(quant_rec(HIGH(r)));
2685
2686 if (INVARSET(LEVEL(r))) {
2687 int r2 = READREF(2), r1 = READREF(1);
2688 switch (applyop) {
2689 case bddop_and: res = and_rec(r2, r1); break;
2690 case bddop_or: res = or_rec(r2, r1); break;
2691 default: res = apply_rec(r2, r1); break;
2692 }
2693 } else {
2694 res = bdd_makenode(LEVEL(r), READREF(2), READREF(1));
2695 }
2696
2697 POPREF(2);
2698
2699 quantcache.set(entry, r, quantid, res);
2700
2701 return res;
2702 }
2703
2704 int bdd_restrict(int r, int var) {
2705 int res;
2706 int numReorder = 1;
2707
2708 CHECKa(r, bddfalse);
2709 CHECKa(var, bddfalse);
2710
2711 if (var < 2)
2712 return r;
2713
2714 if (quantcache == null) quantcache = new OpCache2(cachesize);
2715
2716 again : for (;;) {
2717 if (varset2svartable(var) < 0)
2718 return bddfalse;
2719 try {
2720 INITREF();
2721 quantid = (var << 3) | CACHEID_RESTRICT;
2722 if (numReorder == 0) bdd_disable_reorder();
2723 res = restrict_rec(r);
2724 if (numReorder == 0) bdd_enable_reorder();
2725 } catch (ReorderException x) {
2726 bdd_checkreorder();
2727 numReorder--;
2728 continue again;
2729 }
2730 break;
2731 }
2732
2733 checkresize();
2734 return res;
2735 }
2736
2737 int restrict_rec(int r) {
2738 OpCache2Entry entry;
2739 int res;
2740
2741 if (ISCONST(r) || LEVEL(r) > quantlast) return r;
2742 entry = quantcache.lookup(RESTRHASH(r, quantid));
2743 if ((res = quantcache.get(entry, r, quantid)) >= 0) {
2744 return res;
2745 }
2746
2747 if (INSVARSET(LEVEL(r))) {
2748 if (quantvarset[LEVEL(r)] > 0) {
2749 res = restrict_rec(HIGH(r));
2750 } else {
2751 res = restrict_rec(LOW(r));
2752 }
2753 } else {
2754 PUSHREF(restrict_rec(LOW(r)));
2755 PUSHREF(restrict_rec(HIGH(r)));
2756 res = bdd_makenode(LEVEL(r), READREF(2), READREF(1));
2757 POPREF(2);
2758 }
2759
2760 quantcache.set(entry, r, quantid, res);
2761
2762 return res;
2763 }
2764
2765 int bdd_simplify(int f, int d) {
2766 int res;
2767 int numReorder = 1;
2768
2769 CHECKa(f, bddfalse);
2770 CHECKa(d, bddfalse);
2771
2772 if (applycache == null) applycache = new OpCache2(cachesize);
2773 if (orcache == null) orcache = new OpCache2(cachesize);
2774
2775 again : for (;;) {
2776 try {
2777 INITREF();
2778 applyop = bddop_or;
2779 if (numReorder == 0) bdd_disable_reorder();
2780 res = simplify_rec(f, d);
2781 if (numReorder == 0) bdd_enable_reorder();
2782 } catch (ReorderException x) {
2783 bdd_checkreorder();
2784 numReorder--;
2785 continue again;
2786 }
2787 break;
2788 }
2789
2790 checkresize();
2791 return res;
2792 }
2793
2794 int simplify_rec(int f, int d) {
2795 OpCache2Entry entry;
2796 int res;
2797
2798 if (ISONE(d) || ISCONST(f)) return f;
2799 if (d == f) return BDDONE;
2800 if (ISZERO(d)) return BDDZERO;
2801
2802 entry = applycache.lookup(APPLYHASH(f, d, bddop_simplify));
2803 if ((res = applycache.get_sid(entry, f, d, bddop_simplify << NODE_BITS)) >= 0) {
2804 return res;
2805 }
2806
2807 int LEVEL_f = LEVEL(f);
2808 int LEVEL_d = LEVEL(d);
2809 if (LEVEL_f == LEVEL_d) {
2810 int LOW_d = LOW(d);
2811 int HIGH_d = HIGH(d);
2812 if (ISZERO(LOW_d))
2813 res = simplify_rec(HIGH(f), HIGH_d);
2814 else if (ISZERO(HIGH_d))
2815 res = simplify_rec(LOW(f), LOW_d);
2816 else {
2817 PUSHREF(simplify_rec(LOW(f), LOW_d));
2818 PUSHREF(simplify_rec(HIGH(f), HIGH_d));
2819 res = bdd_makenode(LEVEL_f, READREF(2), READREF(1));
2820 POPREF(2);
2821 }
2822 } else if (LEVEL_f < LEVEL_d) {
2823 PUSHREF(simplify_rec(LOW(f), d));
2824 PUSHREF(simplify_rec(HIGH(f), d));
2825 res = bdd_makenode(LEVEL_f, READREF(2), READREF(1));
2826 POPREF(2);
2827 } else
2828 PUSHREF(or_rec(LOW(d), HIGH(d)));
2829 res = simplify_rec(f, READREF(1));
2830 POPREF(1);
2831 }
2832
2833 applycache.set_sid(entry, f, d, bddop_simplify << NODE_BITS, res);
2834
2835 return res;
2836 }
2837
2838 int bdd_support(int r) {
2839 int n;
2840 int res = 1;
2841
2842 CHECKa(r, bddfalse);
2843
2844 if (ISCONST(r)) return bddtrue;
2845
2846
2847 if (supportSet == null || supportSet.length < bddvarnum) {
2848 supportSet = new int[bddvarnum];
2849 supportID = 0;
2850 }
2851
2852
2853
2854
2855
2856
2857
2858 if (supportID == 0x0FFFFFFF) {
2859
2860 for (int i = 0; i < bddvarnum; ++i)
2861 supportSet[i] = 0;
2862 supportID = 0;
2863 }
2864 ++supportID;
2865 supportMin = LEVEL(r);
2866 supportMax = supportMin;
2867
2868 support_rec(r);
2869 bdd_unmark(r);
2870
2871 bdd_disable_reorder();
2872
2873 for (n = supportMax; n >= supportMin; --n)
2874 if (supportSet[n] == supportID) {
2875 int tmp;
2876 bdd_addref(res);
2877 tmp = bdd_makenode(n, 0, res);
2878 bdd_delref(res);
2879 res = tmp;
2880 }
2881
2882 bdd_enable_reorder();
2883
2884 return res;
2885 }
2886
2887 void support_rec(int r) {
2888 if (ISCONST(r) ||
2889 MARKED(r))
2890 return;
2891
2892 supportSet[LEVEL(r)] = supportID;
2893 if (LEVEL(r) > supportMax) supportMax = LEVEL(r);
2894 SETMARK(r);
2895
2896 support_rec(LOW(r));
2897 support_rec(HIGH(r));
2898 }
2899
2900 int bdd_satone(int r) {
2901 int res;
2902
2903 CHECKa(r, bddfalse);
2904 if (ISCONST(r)) return r;
2905
2906 bdd_disable_reorder();
2907
2908 INITREF();
2909 res = satone_rec(r);
2910
2911 bdd_enable_reorder();
2912
2913 checkresize();
2914 return res;
2915 }
2916
2917 int satone_rec(int r) {
2918 if (ISCONST(r)) return r;
2919
2920 if (ISZERO(LOW(r))) {
2921 int res = satone_rec(HIGH(r));
2922 int m = bdd_makenode(LEVEL(r), BDDZERO, res);
2923 PUSHREF(m);
2924 return m;
2925 } else {
2926 int res = satone_rec(LOW(r));
2927 int m = bdd_makenode(LEVEL(r), res, BDDZERO);
2928 PUSHREF(m);
2929 return m;
2930 }
2931 }
2932
2933 int bdd_satoneset(int r, int var, boolean pol) {
2934 int res;
2935
2936 CHECKa(r, bddfalse);
2937 if (ISZERO(r)) return r;
2938
2939 bdd_disable_reorder();
2940
2941 INITREF();
2942 satPolarity = pol;
2943 res = satoneset_rec(r, var);
2944
2945 bdd_enable_reorder();
2946
2947 checkresize();
2948 return res;
2949 }
2950
2951 int satoneset_rec(int r, int var) {
2952 if (ISCONST(r) && ISCONST(var)) return r;
2953
2954 int LEVEL_r = LEVEL(r);
2955 int LEVEL_var = LEVEL(var);
2956 if (LEVEL_r < LEVEL_var) {
2957 int LOW_r = LOW(r);
2958 if (ISZERO(LOW_r)) {
2959 int res = satoneset_rec(HIGH(r), var);
2960 int m = bdd_makenode(LEVEL_r, BDDZERO, res);
2961 PUSHREF(m);
2962 return m;
2963 } else {
2964 int res = satoneset_rec(LOW_r, var);
2965 int m = bdd_makenode(LEVEL_r, res, BDDZERO);
2966 PUSHREF(m);
2967 return m;
2968 }
2969 } else if (LEVEL_var < LEVEL_r) {
2970 int res = satoneset_rec(r, HIGH(var));
2971 if (satPolarity) {
2972 int m = bdd_makenode(LEVEL_var, BDDZERO, res);
2973 PUSHREF(m);
2974 return m;
2975 } else {
2976 int m = bdd_makenode(LEVEL_var, res, BDDZERO);
2977 PUSHREF(m);
2978 return m;
2979 }
2980 } else
2981 int LOW_r = LOW(r);
2982 int HIGH_var = HIGH(var);
2983 if (ISZERO(LOW_r)) {
2984 int res = satoneset_rec(HIGH(r), HIGH_var);
2985 int m = bdd_makenode(LEVEL_r, BDDZERO, res);
2986 PUSHREF(m);
2987 return m;
2988 } else {
2989 int res = satoneset_rec(LOW_r, HIGH_var);
2990 int m = bdd_makenode(LEVEL_r, res, BDDZERO);
2991 PUSHREF(m);
2992 return m;
2993 }
2994 }
2995
2996 }
2997
2998 int bdd_fullsatone(int r) {
2999 int res;
3000 int v;
3001
3002 CHECKa(r, bddfalse);
3003 if (ISZERO(r)) return 0;
3004
3005 bdd_disable_reorder();
3006
3007 INITREF();
3008 res = fullsatone_rec(r);
3009
3010 for (v = LEVEL(r) - 1; v >= 0; v--) {
3011 res = PUSHREF(bdd_makenode(v, res, 0));
3012 }
3013
3014 bdd_enable_reorder();
3015
3016 checkresize();
3017 return res;
3018 }
3019
3020 int fullsatone_rec(int r) {
3021 if (ISCONST(r)) return r;
3022
3023 int LOW_r = LOW(r);
3024 int LEVEL_r = LEVEL(r);
3025 if (LOW_r != 0) {
3026 int res = fullsatone_rec(LOW_r);
3027 for (int v = LEVEL(LOW_r) - 1; v > LEVEL_r; v--) {
3028 res = PUSHREF(bdd_makenode(v, res, 0));
3029 }
3030 return PUSHREF(bdd_makenode(LEVEL_r, res, 0));
3031 } else {
3032 int HIGH_r = HIGH(r);
3033 int res = fullsatone_rec(HIGH_r);
3034 for (int v = LEVEL(HIGH_r) - 1; v > LEVEL_r; v--) {
3035 res = PUSHREF(bdd_makenode(v, res, 0));
3036 }
3037 return PUSHREF(bdd_makenode(LEVEL_r, 0, res));
3038 }
3039 }
3040
3041 void bdd_gbc_rehash() {
3042 int n;
3043
3044 bddfreepos = 0;
3045 bddfreenum = 0;
3046
3047 for (n = bddnodesize - 1; n >= 2; n--) {
3048 int LOW_n = LOW(n);
3049 if (LOW_n != INVALID_BDD) {
3050 int hash2 = NODEHASH(LEVEL(n), LOW_n, HIGH(n));
3051 SETNEXT(n, HASH(hash2));
3052 SETHASH(hash2, n);
3053 } else {
3054 SETNEXT(n, bddfreepos);
3055 bddfreepos = n;
3056 bddfreenum++;
3057 }
3058 }
3059 }
3060
3061 final long clock() {
3062 return System.currentTimeMillis();
3063 }
3064
3065 final void INITREF() {
3066 bddrefstacktop = 0;
3067 }
3068 final int PUSHREF(int a) {
3069 bddrefstack[bddrefstacktop++] = a;
3070 return a;
3071 }
3072 final int READREF(int a) {
3073 return bddrefstack[bddrefstacktop - a];
3074 }
3075 final void POPREF(int a) {
3076 bddrefstacktop -= a;
3077 }
3078
3079 int bdd_nodecount(int r) {
3080 int[] num = new int[1];
3081
3082 CHECK(r);
3083
3084 bdd_markcount(r, num);
3085 bdd_unmark(r);
3086
3087 return num[0];
3088 }
3089
3090 int bdd_anodecount(int[] r) {
3091 int n;
3092 int[] cou = new int[1];
3093
3094 for (n = 0; n < r.length; n++)
3095 bdd_markcount(r[n], cou);
3096
3097 for (n = 0; n < r.length; n++)
3098 bdd_unmark(r[n]);
3099
3100 return cou[0];
3101 }
3102
3103 int[] bdd_varprofile(int r) {
3104 CHECK(r);
3105
3106 int[] varprofile = new int[bddvarnum];
3107 varprofile_rec(r, varprofile);
3108 bdd_unmark(r);
3109 return varprofile;
3110 }
3111
3112 void varprofile_rec(int r, int[] varprofile) {
3113
3114 if (ISCONST(r) || MARKED(r)) return;
3115
3116 varprofile[bddlevel2var[LEVEL(r)]]++;
3117 SETMARK(r);
3118
3119 varprofile_rec(LOW(r), varprofile);
3120 varprofile_rec(HIGH(r), varprofile);
3121 }
3122
3123 double bdd_pathcount(int r) {
3124 CHECK(r);
3125
3126 miscid = CACHEID_PATHCOU << NODE_BITS;
3127
3128 if (countcache == null) countcache = new OpCacheD(cachesize);
3129
3130 return bdd_pathcount_rec(r);
3131 }
3132
3133 double bdd_pathcount_rec(int r) {
3134 OpCacheDEntry entry;
3135 double size;
3136
3137 if (ISZERO(r)) return 0f;
3138 if (ISONE(r)) return 1f;
3139
3140 entry = countcache.lookup(PATHCOUHASH(r));
3141 if ((size = countcache.get_sid(entry, r, miscid)) >= 0) {
3142 return size;
3143 }
3144
3145 size = bdd_pathcount_rec(LOW(r)) + bdd_pathcount_rec(HIGH(r));
3146
3147 countcache.set_sid(entry, r, miscid, size);
3148
3149 return size;
3150 }
3151
3152 double bdd_satcount(int r) {
3153 double size = 1;
3154
3155 CHECK(r);
3156
3157 if (countcache == null) countcache = new OpCacheD(cachesize);
3158
3159 miscid = CACHEID_SATCOU << NODE_BITS;
3160 size = Math.pow(2.0, (double) LEVEL(r));
3161
3162 return size * satcount_rec(r);
3163 }
3164
3165 double bdd_satcountset(int r, int varset) {
3166 double unused = bddvarnum;
3167 int n;
3168
3169 if (ISCONST(varset) || ISZERO(r))
3170 return 0.0;
3171
3172 for (n = varset; !ISCONST(n); n = HIGH(n))
3173 unused--;
3174
3175 unused = bdd_satcount(r) / Math.pow(2.0, unused);
3176
3177 return unused >= 1.0 ? unused : 1.0;
3178 }
3179
3180 double satcount_rec(int r) {
3181 OpCacheDEntry entry;
3182 double size, s;
3183
3184 if (ISCONST(r)) return r;
3185
3186 entry = countcache.lookup(SATCOUHASH(r));
3187 if ((size = countcache.get_sid(entry, r, miscid)) >= 0) {
3188 return size;
3189 }
3190
3191 size = 0;
3192 s = 1;
3193
3194 int LEVEL_r = LEVEL(r);
3195 int LOW_r = LOW(r);
3196 int HIGH_r = HIGH(r);
3197 s *= Math.pow(2.0, (float) (LEVEL(LOW_r) - LEVEL_r - 1));
3198 size += s * satcount_rec(LOW_r);
3199
3200 s = 1;
3201 s *= Math.pow(2.0, (float) (LEVEL(HIGH_r) - LEVEL_r - 1));
3202 size += s * satcount_rec(HIGH_r);
3203
3204 countcache.set_sid(entry, r, miscid, size);
3205
3206 return size;
3207 }
3208
3209 void bdd_gbc() {
3210 int r;
3211 int n;
3212 long c2, c1 = clock();
3213
3214 gcstats.nodes = bddnodesize;
3215 gcstats.freenodes = bddfreenum;
3216 gcstats.time = 0;
3217 gcstats.sumtime = gbcclock;
3218 gcstats.num = gbcollectnum;
3219 gbc_handler(true, gcstats);
3220
3221
3222 handleDeferredFree();
3223
3224 for (r = 0; r < bddrefstacktop; r++)
3225 bdd_mark(bddrefstack[r]);
3226
3227 for (n = 0; n < bddnodesize; n++) {
3228 if (HASREF(n))
3229 bdd_mark(n);
3230 SETHASH(n, 0);
3231 }
3232
3233 bddfreepos = 0;
3234 bddfreenum = 0;
3235
3236 for (n = bddnodesize - 1; n >= 2; n--) {
3237 int LOW_n = LOW(n);
3238 if (MARKED(n) && LOW_n != INVALID_BDD) {
3239 int hash2;
3240 UNMARK(n);
3241 hash2 = NODEHASH(LEVEL(n), LOW_n, HIGH(n));
3242 SETNEXT(n, HASH(hash2));
3243 SETHASH(hash2, n);
3244 } else {
3245 SETLOW(n, INVALID_BDD);
3246 SETNEXT(n, bddfreepos);
3247 bddfreepos = n;
3248 bddfreenum++;
3249 }
3250 }
3251
3252 if (FLUSH_CACHE_ON_GC) {
3253 bdd_operator_reset();
3254 } else {
3255 bdd_operator_clean();
3256 }
3257
3258 c2 = clock();
3259 gbcclock += c2 - c1;
3260 gbcollectnum++;
3261
3262 gcstats.nodes = bddnodesize;
3263 gcstats.freenodes = bddfreenum;
3264 gcstats.time = c2 - c1;
3265 gcstats.sumtime = gbcclock;
3266 gcstats.num = gbcollectnum;
3267 gbc_handler(false, gcstats);
3268
3269
3270 }
3271
3272 int bdd_addref(int root) {
3273 if (root == INVALID_BDD)
3274 bdd_error(BDD_BREAK);
3275 if (root < 2 || !bddrunning)
3276 return root;
3277 if (root >= bddnodesize)
3278 return bdd_error(BDD_ILLBDD);
3279 if (LOW(root) == INVALID_BDD)
3280 return bdd_error(BDD_ILLBDD);
3281
3282 INCREF(root);
3283 if (false) System.out.println("INCREF("+root+") = "+GETREF(root));
3284 return root;
3285 }
3286
3287 int bdd_delref(int root) {
3288 if (root == INVALID_BDD)
3289 bdd_error(BDD_BREAK);
3290 if (root < 2 || !bddrunning)
3291 return root;
3292 if (root >= bddnodesize)
3293 return bdd_error(BDD_ILLBDD);
3294 if (LOW(root) == INVALID_BDD)
3295 return bdd_error(BDD_ILLBDD);
3296
3297
3298 if (!HASREF(root))
3299 bdd_error(BDD_BREAK);
3300
3301 DECREF(root);
3302 if (false) System.out.println("DECREF("+root+") = "+GETREF(root));
3303 return root;
3304 }
3305
3306 void bdd_mark(int i) {
3307
3308 if (ISCONST(i) || MARKED(i))
3309 return;
3310
3311 SETMARK(i);
3312
3313 bdd_mark(LOW(i));
3314 bdd_mark(HIGH(i));
3315 }
3316
3317 void bdd_markcount(int i, int[] cou) {
3318
3319 if (ISCONST(i) || MARKED(i))
3320 return;
3321
3322 SETMARK(i);
3323 cou[0] += 1;
3324
3325 bdd_markcount(LOW(i), cou);
3326 bdd_markcount(HIGH(i), cou);
3327 }
3328
3329 void bdd_unmark(int i) {
3330
3331 if (ISCONST(i) || !MARKED(i))
3332 return;
3333
3334 UNMARK(i);
3335
3336 bdd_unmark(LOW(i));
3337 bdd_unmark(HIGH(i));
3338 }
3339
3340 int bdd_makenode(int level, int low, int high) {
3341 int hash2;
3342 int res;
3343
3344 if (CACHESTATS > 0) cachestats.uniqueAccess++;
3345
3346
3347 if (low == high) return low;
3348
3349
3350 hash2 = NODEHASH(level, low, high);
3351 res = HASH(hash2);
3352
3353 if (res != 0) {
3354 int m1 = (level << LEV_LPOS) | low;
3355 int m2 = ((level << (LEV_HPOS-LEV_LBITS)) & LEV_HMASK) | high;
3356 do {
3357 if (bddnodes[res*__node_size + offset__low] == m1 &&
3358 bddnodes[res*__node_size + offset__high] == m2) {
3359 if (CACHESTATS > 0) cachestats.uniqueHit++;
3360 return res;
3361 }
3362 res = NEXT(res);
3363 if (CACHESTATS > 0) cachestats.uniqueChain++;
3364 } while (res != 0);
3365 }
3366
3367
3368 if (CACHESTATS > 0) cachestats.uniqueMiss++;
3369
3370
3371 if (bddfreepos == 0) {
3372 if (bdderrorcond != 0) return 0;
3373
3374
3375 bdd_gbc();
3376
3377 if ((bddnodesize-bddfreenum) >= usednodes_nextreorder &&
3378 bdd_reorder_ready()) {
3379 throw new ReorderException();
3380 }
3381
3382 if ((bddfreenum * 100) / bddnodesize <= minfreenodes) {
3383 bdd_noderesize(true);
3384 hash2 = NODEHASH(level, low, high);
3385 }
3386
3387
3388 if (bddfreepos == 0) {
3389 bdderrorcond = Math.abs(BDD_NODENUM);
3390 bdd_error(BDD_NODENUM);
3391 return 0;
3392 }
3393 }
3394
3395
3396 res = bddfreepos;
3397 bddfreepos = NEXT(bddfreepos);
3398 bddfreenum--;
3399 bddproduced++;
3400
3401 INIT_NODE(res, level, low, high, HASH(hash2));
3402 SETHASH(hash2, res);
3403
3404 return res;
3405 }
3406
3407 int bdd_noderesize(boolean doRehash) {
3408 int oldsize = bddnodesize;
3409 int newsize = bddnodesize;
3410
3411 if (bddmaxnodesize > 0) {
3412 if (newsize >= bddmaxnodesize)
3413 return -1;
3414 }
3415
3416 if (increasefactor > 0) {
3417 newsize += (int)(newsize * increasefactor);
3418 } else {
3419 newsize = newsize << 1;
3420 }
3421
3422 if (bddmaxnodeincrease > 0) {
3423 if (newsize > oldsize + bddmaxnodeincrease)
3424 newsize = oldsize + bddmaxnodeincrease;
3425 }
3426
3427 if (bddmaxnodesize > 0) {
3428 if (newsize > bddmaxnodesize)
3429 newsize = bddmaxnodesize;
3430 }
3431
3432 return doResize(doRehash, oldsize, newsize);
3433 }
3434
3435 int bdd_setallocnum(int size) {
3436 int old = bddnodesize;
3437 doResize(true, old, size);
3438 return old;
3439 }
3440
3441 int doResize(boolean doRehash, int oldsize, int newsize) {
3442
3443 newsize = bdd_prime_lte(newsize);
3444
3445 if (oldsize > newsize) return 0;
3446 if (newsize >= NODE_MASK) newsize = NODE_MASK-1;
3447
3448 resize_handler(oldsize, newsize);
3449
3450 int[] newnodes;
3451 int n;
3452 newnodes = new int[newsize*__node_size];
3453 System.arraycopy(bddnodes, 0, newnodes, 0, bddnodes.length);
3454 bddnodes = newnodes;
3455 bddnodesize = newsize;
3456
3457 if (doRehash)
3458 for (n = 0; n < oldsize; n++)
3459 SETHASH(n, 0);
3460
3461 for (n = oldsize; n < bddnodesize; n++) {
3462 SETLOW(n, INVALID_BDD);
3463 SETNEXT(n, n+1);
3464 }
3465 SETNEXT(bddnodesize-1, bddfreepos);
3466 bddfreepos = oldsize;
3467 bddfreenum += bddnodesize - oldsize;
3468
3469 if (doRehash)
3470 bdd_gbc_rehash();
3471
3472 bddresized = true;
3473
3474 return 0;
3475 }
3476
3477 void bdd_init(int initnodesize, int cs) {
3478 int n;
3479
3480 if (bddrunning)
3481 throw new JavaBDDException(BDD_RUNNING);
3482
3483 bddnodesize = bdd_prime_gte(initnodesize);
3484 cachesize = bdd_prime_gte(cs);
3485
3486 bddnodes = new int[bddnodesize*__node_size];
3487
3488 bddresized = false;
3489
3490 for (n = 0; n < bddnodesize; n++) {
3491 SETLOW(n, INVALID_BDD);
3492 SETNEXT(n, n+1);
3493 }
3494 SETNEXT(bddnodesize-1, 0);
3495
3496 SETMAXREF(0);
3497 SETMAXREF(1);
3498 SETLOW(0, 0); SETHIGH(0, 0);
3499 SETLOW(1, 1); SETHIGH(1, 1);
3500
3501 bdd_operator_init(cachesize);
3502
3503 bddfreepos = 2;
3504 bddfreenum = bddnodesize - 2;
3505 bddrunning = true;
3506 bddvarnum = 0;
3507 gbcollectnum = 0;
3508 gbcclock = 0;
3509 usednodes_nextreorder = bddnodesize;
3510 bddmaxnodeincrease = DEFAULTMAXNODEINC;
3511
3512 bdderrorcond = 0;
3513
3514 bdd_pairs_init();
3515 bdd_reorder_init();
3516 }
3517
3518
3519 static final int CACHEID_CONSTRAIN = 0x0;
3520 static final int CACHEID_SATCOU = 0x2;
3521 static final int CACHEID_SATCOULN = 0x3;
3522 static final int CACHEID_PATHCOU = 0x4;
3523
3524
3525 static final int CACHEID_REPLACE = 0x0;
3526 static final int CACHEID_VECCOMPOSE = 0x1;
3527
3528
3529 static final int CACHEID_EXIST = 0x0;
3530 static final int CACHEID_FORALL = 0x1;
3531 static final int CACHEID_UNIQUE = 0x2;
3532 static final int CACHEID_APPEX = 0x3;
3533 static final int CACHEID_APPAL = 0x4;
3534 static final int CACHEID_APPUN = 0x5;
3535 static final int CACHEID_RESTRICT = 0x6;
3536 static final int CACHEID_COMPOSE = 0x7;
3537
3538
3539 static int oprres[][] =
3540 { { 0, 0, 0, 1 },
3541 0, 1, 1, 0 },
3542 0, 1, 1, 1 },
3543 1, 1, 1, 0 },
3544 1, 0, 0, 0 },
3545 1, 1, 0, 1 },
3546 1, 0, 0, 1 },
3547 0, 0, 1, 0 },
3548 0, 1, 0, 0 },
3549 1, 0, 1, 1 },
3550 1, 1, 0, 0 }
3551 };
3552
3553 int applyop;
3554 int appexop;
3555 int appexid;
3556 int quantid;
3557 int[] quantvarset;
3558 int quantvarsetID;
3559 int quantlast;
3560 int replaceid;
3561 int[] replacepair;
3562 int replacelast;
3563 int composelevel;
3564 int miscid;
3565 int supportID;
3566 int supportMin;
3567 int supportMax;
3568 int[] supportSet;
3569 int cacheratio;
3570 boolean satPolarity;
3571
3572 OpCache1 singlecache;
3573 OpCache2 replacecache;
3574 OpCache2 andcache;
3575 OpCache2 orcache;
3576 OpCache2 applycache;
3577 OpCache2 quantcache;
3578 OpCache3 appexcache;
3579 OpCache4 appex3cache;
3580 OpCache3 itecache;
3581 OpCache2 misccache;
3582 OpCacheD countcache;
3583
3584 void bdd_operator_init(int cachesize) {
3585 quantvarsetID = 0;
3586 quantvarset = null;
3587 cacheratio = 0;
3588 supportSet = null;
3589 }
3590
3591 void bdd_operator_done() {
3592 quantvarset = null;
3593 supportSet = null;
3594
3595 singlecache = null;
3596 replacecache = null;
3597 andcache = null;
3598 orcache = null;
3599 applycache = null;
3600 quantcache = null;
3601 appexcache = null;
3602 appex3cache = null;
3603 itecache = null;
3604 countcache = null;
3605 misccache = null;
3606 }
3607
3608 void bdd_operator_reset() {
3609 if (singlecache != null)
3610 singlecache.reset();
3611 if (replacecache != null)
3612 replacecache.reset();
3613 if (andcache != null)
3614 andcache.reset();
3615 if (orcache != null)
3616 orcache.reset();
3617 if (applycache != null)
3618 applycache.reset();
3619 if (quantcache != null)
3620 quantcache.reset();
3621 if (appexcache != null)
3622 appexcache.reset();
3623 if (appex3cache != null)
3624 appex3cache.reset();
3625 if (itecache != null)
3626 itecache.reset();
3627 if (countcache != null)
3628 countcache.reset();
3629 if (misccache != null)
3630 misccache.reset();
3631 }
3632
3633 void bdd_operator_clean() {
3634 if (singlecache != null)
3635 singlecache.clean();
3636 if (replacecache != null)
3637 replacecache.clean();
3638 if (andcache != null)
3639 andcache.clean();
3640 if (orcache != null)
3641 orcache.clean();
3642 if (applycache != null)
3643 applycache.clean();
3644 if (quantcache != null)
3645 quantcache.clean();
3646 if (appexcache != null)
3647 appexcache.clean();
3648 if (appex3cache != null)
3649 appex3cache.reset();
3650 if (itecache != null)
3651 itecache.clean();
3652 if (countcache != null)
3653 countcache.clean();
3654 if (misccache != null)
3655 misccache.clean();
3656 }
3657
3658 void bdd_operator_varresize() {
3659 quantvarset = new int[bddvarnum];
3660 quantvarsetID = 0;
3661 if (countcache != null) countcache.reset();
3662 }
3663
3664 int bdd_setcachesize(int newcachesize) {
3665 int old = cachesize;
3666 cachesize = bdd_prime_lte(cachesize);
3667 singlecache = null;
3668 replacecache = null;
3669 andcache = null;
3670 orcache = null;
3671 applycache = null;
3672 quantcache = null;
3673 appexcache = null;
3674 appex3cache = null;
3675 itecache = null;
3676 countcache = null;
3677 misccache = null;
3678 return old;
3679 }
3680
3681 void bdd_operator_noderesize() {
3682 if (cacheratio > 0) {
3683 cachesize = bddnodesize / cacheratio;
3684 singlecache = null;
3685 replacecache = null;
3686 andcache = null;
3687 orcache = null;
3688 applycache = null;
3689 quantcache = null;
3690 appexcache = null;
3691 appex3cache = null;
3692 itecache = null;
3693 countcache = null;
3694 misccache = null;
3695 }
3696 }
3697
3698 void bdd_setpair(bddPair pair, int oldvar, int newvar) {
3699 if (pair == null) return;
3700
3701 if (oldvar < 0 || oldvar > bddvarnum - 1)
3702 bdd_error(BDD_VAR);
3703 if (newvar < 0 || newvar > bddvarnum - 1)
3704 bdd_error(BDD_VAR);
3705
3706 bdd_delref(pair.result[bddvar2level[oldvar]]);
3707 pair.result[bddvar2level[oldvar]] = bdd_ithvar(newvar);
3708 pair.id = update_pairsid();
3709
3710 if (bddvar2level[oldvar] > pair.last)
3711 pair.last = bddvar2level[oldvar];
3712
3713 }
3714
3715 void bdd_setbddpair(bddPair pair, int oldvar, int newvar) {
3716 int oldlevel;
3717
3718 if (pair == null) return;
3719
3720 CHECK(newvar);
3721 if (oldvar < 0 || oldvar >= bddvarnum)
3722 bdd_error(BDD_VAR);
3723 oldlevel = bddvar2level[oldvar];
3724
3725 bdd_delref(pair.result[oldlevel]);
3726 pair.result[oldlevel] = bdd_addref(newvar);
3727 pair.id = update_pairsid();
3728
3729 if (oldlevel > pair.last)
3730 pair.last = oldlevel;
3731
3732 }
3733
3734 void bdd_resetpair(bddPair p) {
3735 for (int n = 0; n < bddvarnum; n++) {
3736 bdd_delref(p.result[n]);
3737 p.result[n] = bdd_ithvar(n);
3738 }
3739 p.last = 0;
3740 }
3741
3742 bddPair pairs;
3743 int pairsid;
3744
3745 /**************************************************************************
3746 *************************************************************************/
3747
3748 void bdd_pairs_init() {
3749 pairsid = 0;
3750 pairs = null;
3751 }
3752
3753 void bdd_pairs_done() {
3754 bddPair p = pairs;
3755 int n;
3756
3757 while (p != null) {
3758 bddPair next = p.next;
3759 for (n = 0; n < bddvarnum; n++)
3760 bdd_delref(p.result[n]);
3761 p.result = null;
3762 p = next;
3763 }
3764 }
3765
3766 int update_pairsid() {
3767 pairsid++;
3768
3769 if (pairsid == MAX_PAIRSID) {
3770 pairsid = 0;
3771 for (bddPair p = pairs; p != null; p = p.next)
3772 p.id = pairsid++;
3773 if (pairsid >= MAX_PAIRSID)
3774 throw new BDDException("Too many pairs!");
3775 if (replacecache != null) replacecache.reset();
3776 }
3777
3778 return pairsid;
3779 }
3780
3781 void bdd_register_pair(bddPair p) {
3782 p.next = pairs;
3783 pairs = p;
3784 }
3785
3786 void bdd_pairs_vardown(int level) {
3787 bddPair p;
3788
3789 for (p = pairs; p != null; p = p.next) {
3790 int tmp;
3791
3792 tmp = p.result[level];
3793 p.result[level] = p.result[level + 1];
3794 p.result[level + 1] = tmp;
3795
3796 if (p.last == level)
3797 p.last++;
3798 }
3799 }
3800
3801 int bdd_pairs_resize(int oldsize, int newsize) {
3802 bddPair p;
3803 int n;
3804
3805 for (p = pairs; p != null; p = p.next) {
3806 int[] new_result = new int[newsize];
3807 System.arraycopy(p.result, 0, new_result, 0, oldsize);
3808 p.result = new_result;
3809
3810 for (n = oldsize; n < newsize; n++)
3811 p.result[n] = bdd_ithvar(bddlevel2var[n]);
3812 }
3813
3814 return 0;
3815 }
3816
3817 void bdd_disable_reorder() {
3818 reorderdisabled = 1;
3819 }
3820 void bdd_enable_reorder() {
3821 reorderdisabled = 0;
3822 }
3823 void bdd_checkreorder() {
3824 bdd_reorder_auto();
3825
3826
3827 usednodes_nextreorder = 2 * (bddnodesize - bddfreenum);
3828
3829
3830
3831 if (bdd_reorder_gain() < 20)
3832 usednodes_nextreorder
3833 += (usednodes_nextreorder * (20 - bdd_reorder_gain())) / 20;
3834 }
3835
3836 boolean bdd_reorder_ready() {
3837 if ((bddreordermethod == BDD_REORDER_NONE)
3838 || (vartree == null)
3839 || (bddreordertimes == 0)
3840 || (reorderdisabled != 0))
3841 return false;
3842 return true;
3843 }
3844
3845 void bdd_reorder(int method) {
3846 BddTree top;
3847 int savemethod = bddreordermethod;
3848 int savetimes = bddreordertimes;
3849
3850 bddreordermethod = method;
3851 bddreordertimes = 1;
3852
3853 if ((top = bddtree_new(-1)) != null) {
3854 if (reorder_init() >= 0) {
3855
3856 usednum_before = bddnodesize - bddfreenum;
3857
3858 top.first = 0;
3859 top.last = bdd_varnum() - 1;
3860 top.fixed = false;
3861 top.next = null;
3862 top.nextlevel = vartree;
3863
3864 reorder_block(top, method);
3865 vartree = top.nextlevel;
3866
3867 usednum_after = bddnodesize - bddfreenum;
3868
3869 reorder_done();
3870 bddreordermethod = savemethod;
3871 bddreordertimes = savetimes;
3872 }
3873 }
3874 }
3875
3876 BddTree bddtree_new(int id) {
3877 BddTree t = new BddTree();
3878
3879 t.first = t.last = -1;
3880 t.fixed = true;
3881 t.next = t.prev = t.nextlevel = null;
3882 t.seq = null;
3883 t.id = id;
3884 return t;
3885 }
3886
3887 BddTree reorder_block(BddTree t, int method) {
3888 BddTree dis;
3889
3890 if (t == null)
3891 return null;
3892
3893 if (!t.fixed
3894 && t.nextlevel != null) {
3895 switch (method) {
3896 case BDD_REORDER_WIN2 :
3897 t.nextlevel = reorder_win2(t.nextlevel);
3898 break;
3899 case BDD_REORDER_WIN2ITE :
3900 t.nextlevel = reorder_win2ite(t.nextlevel);
3901 break;
3902 case BDD_REORDER_SIFT :
3903 t.nextlevel = reorder_sift(t.nextlevel);
3904 break;
3905 case BDD_REORDER_SIFTITE :
3906 t.nextlevel = reorder_siftite(t.nextlevel);
3907 break;
3908 case BDD_REORDER_WIN3 :
3909 t.nextlevel = reorder_win3(t.nextlevel);
3910 break;
3911 case BDD_REORDER_WIN3ITE :
3912 t.nextlevel = reorder_win3ite(t.nextlevel);
3913 break;
3914 case BDD_REORDER_RANDOM :
3915 t.nextlevel = reorder_random(t.nextlevel);
3916 break;
3917 }
3918 }
3919
3920 for (dis = t.nextlevel; dis != null; dis = dis.next)
3921 reorder_block(dis, method);
3922
3923 if (t.seq != null) {
3924 varseq_qsort(t.seq, 0, t.last-t.first + 1);
3925 }
3926
3927 return t;
3928 }
3929
3930
3931 void varseq_qsort(int[] target, int from, int to) {
3932
3933 int x, i, j;
3934
3935 switch (to - from) {
3936 case 0 :
3937 return;
3938
3939 case 1 :
3940 return;
3941
3942 case 2 :
3943 if (bddvar2level[target[from]] <= bddvar2level[target[from + 1]])
3944 return;
3945 else {
3946 x = target[from];
3947 target[from] = target[from + 1];
3948 target[from + 1] = x;
3949 }
3950 return;
3951 }
3952
3953 int r = target[from];
3954 int s = target[(from + to) / 2];
3955 int t = target[to - 1];
3956
3957 if (bddvar2level[r] <= bddvar2level[s]) {
3958 if (bddvar2level[s] <= bddvar2level[t]) {
3959 } else if (bddvar2level[r] <= bddvar2level[t]) {
3960 target[to - 1] = s;
3961 target[(from + to) / 2] = t;
3962 } else {
3963 target[to - 1] = s;
3964 target[from] = t;
3965 target[(from + to) / 2] = r;
3966 }
3967 } else {
3968 if (bddvar2level[r] <= bddvar2level[t]) {
3969 target[(from + to) / 2] = r;
3970 target[from] = s;
3971 } else if (bddvar2level[s] <= bddvar2level[t]) {
3972 target[to - 1] = r;
3973 target[(from + to) / 2] = t;
3974 target[from] = s;
3975 } else {
3976 target[to - 1] = r;
3977 target[from] = t;
3978 }
3979 }
3980
3981 int mid = target[(from + to) / 2];
3982
3983 for (i = from + 1, j = to - 1; i + 1 != j;) {
3984 if (target[i] == mid) {
3985 target[i] = target[i + 1];
3986 target[i + 1] = mid;
3987 }
3988
3989 x = target[i];
3990
3991 if (x <= mid)
3992 i++;
3993 else {
3994 x = target[--j];
3995 target[j] = target[i];
3996 target[i] = x;
3997 }
3998 }
3999
4000 varseq_qsort(target, from, i);
4001 varseq_qsort(target, i + 1, to);
4002 }
4003
4004 BddTree reorder_win2(BddTree t) {
4005 BddTree dis = t, first = t;
4006
4007 if (t == null)
4008 return t;
4009
4010 if (verbose > 1) {
4011 System.out.println("Win2 start: " + reorder_nodenum() + " nodes");
4012 System.out.flush();
4013 }
4014
4015 while (dis.next != null) {
4016 int best = reorder_nodenum();
4017 blockdown(dis);
4018
4019 if (best < reorder_nodenum()) {
4020 blockdown(dis.prev);
4021 dis = dis.next;
4022 } else if (first == dis)
4023 first = dis.prev;
4024
4025 if (verbose > 1) {
4026 System.out.print(".");
4027 System.out.flush();
4028 }
4029 }
4030
4031 if (verbose > 1) {
4032 System.out.println();
4033 System.out.println("Win2 end: " + reorder_nodenum() + " nodes");
4034 System.out.flush();
4035 }
4036
4037 return first;
4038 }
4039
4040 BddTree reorder_win3(BddTree t) {
4041 BddTree dis = t, first = t;
4042
4043 if (t == null)
4044 return t;
4045
4046 if (verbose > 1) {
4047 System.out.println("Win3 start: " + reorder_nodenum() + " nodes");
4048 System.out.flush();
4049 }
4050
4051 while (dis.next != null) {
4052 BddTree[] f = new BddTree[1];
4053 f[0] = first;
4054 dis = reorder_swapwin3(dis, f);
4055 first = f[0];
4056
4057 if (verbose > 1) {
4058 System.out.print(".");
4059 System.out.flush();
4060 }
4061 }
4062
4063 if (verbose > 1) {
4064 System.out.println();
4065 System.out.println("Win3 end: " + reorder_nodenum() + " nodes");
4066 System.out.flush();
4067 }
4068
4069 return first;
4070 }
4071
4072 BddTree reorder_win3ite(BddTree t) {
4073 BddTree dis = t, first = t;
4074 int lastsize;
4075
4076 if (t == null)
4077 return t;
4078
4079 if (verbose > 1)
4080 System.out.println(
4081 "Win3ite start: " + reorder_nodenum() + " nodes");
4082
4083 do {
4084 lastsize = reorder_nodenum();
4085 dis = first;
4086
4087 while (dis.next != null && dis.next.next != null) {
4088 BddTree[] f = new BddTree[1];
4089 f[0] = first;
4090 dis = reorder_swapwin3(dis, f);
4091 first = f[0];
4092
4093 if (verbose > 1) {
4094 System.out.print(".");
4095 System.out.flush();
4096 }
4097 }
4098
4099 if (verbose > 1)
4100 System.out.println(" " + reorder_nodenum() + " nodes");
4101 }
4102 while (reorder_nodenum() != lastsize);
4103
4104 if (verbose > 1)
4105 System.out.println("Win3ite end: " + reorder_nodenum() + " nodes");
4106
4107 return first;
4108 }
4109
4110 BddTree reorder_swapwin3(BddTree dis, BddTree[] first) {
4111 boolean setfirst = dis.prev == null;
4112 BddTree next = dis;
4113 int best = reorder_nodenum();
4114
4115 if (dis.next.next == null)
4116 blockdown(dis.prev);
4117
4118 if (best < reorder_nodenum()) {
4119 blockdown(dis.prev);
4120 next = dis.next;
4121 } else {
4122 next = dis;
4123 if (setfirst)
4124 first[0] = dis.prev;
4125 }
4126 } else
4127 int pos = 0;
4128 blockdown(dis);
4129 pos++;
4130 if (best > reorder_nodenum()) {
4131 pos = 0;
4132 best = reorder_nodenum();
4133 }
4134
4135 blockdown(dis);
4136 pos++;
4137 if (best > reorder_nodenum()) {
4138 pos = 0;
4139 best = reorder_nodenum();
4140 }
4141
4142 dis = dis.prev.prev;
4143 blockdown(dis);
4144 pos++;
4145 if (best > reorder_nodenum()) {
4146 pos = 0;
4147 best = reorder_nodenum();
4148 }
4149
4150 blockdown(dis);
4151 pos++;
4152 if (best > reorder_nodenum()) {
4153 pos = 0;
4154 best = reorder_nodenum();
4155 }
4156
4157 dis = dis.prev.prev;
4158 blockdown(dis);
4159 pos++;
4160 if (best > reorder_nodenum()) {
4161 pos = 0;
4162 best = reorder_nodenum();
4163 }
4164
4165 if (pos >= 1)
4166 dis = dis.prev;
4167 blockdown(dis);
4168 next = dis;
4169 if (setfirst)
4170 first[0] = dis.prev;
4171 }
4172
4173 if (pos >= 2)
4174 blockdown(dis);
4175 next = dis.prev;
4176 if (setfirst)
4177 first[0] = dis.prev.prev;
4178 }
4179
4180 if (pos >= 3)
4181 dis = dis.prev.prev;
4182 blockdown(dis);
4183 next = dis;
4184 if (setfirst)
4185 first[0] = dis.prev;
4186 }
4187
4188 if (pos >= 4)
4189 blockdown(dis);
4190 next = dis.prev;
4191 if (setfirst)
4192 first[0] = dis.prev.prev;
4193 }
4194
4195 if (pos >= 5)
4196 dis = dis.prev.prev;
4197 blockdown(dis);
4198 next = dis;
4199 if (setfirst)
4200 first[0] = dis.prev;
4201 }
4202 }
4203
4204 return next;
4205 }
4206
4207 BddTree reorder_sift_seq(BddTree t, BddTree seq[], int num) {
4208 BddTree dis;
4209 int n;
4210
4211 if (t == null)
4212 return t;
4213
4214 for (n = 0; n < num; n++) {
4215 long c2, c1 = clock();
4216
4217 if (verbose > 1) {
4218 System.out.print("Sift ");
4219
4220
4221
4222 System.out.print(seq[n].id);
4223 System.out.print(": ");
4224 }
4225
4226 reorder_sift_bestpos(seq[n], num / 2);
4227
4228 if (verbose > 1) {
4229 System.out.println();
4230 System.out.print("> " + reorder_nodenum() + " nodes");
4231 }
4232
4233 c2 = clock();
4234 if (verbose > 1)
4235 System.out.println(
4236 " (" + (float) (c2 - c1) / (float) 1000 + " sec)\n");
4237 }
4238
4239
4240 for (dis = t; dis.prev != null; dis = dis.prev)
4241
4242
4243 return dis;
4244 }
4245
4246 void reorder_sift_bestpos(BddTree blk, int middlePos) {
4247 int best = reorder_nodenum();
4248 int maxAllowed;
4249 int bestpos = 0;
4250 boolean dirIsUp = true;
4251 int n;
4252
4253 if (bddmaxnodesize > 0)
4254 maxAllowed =
4255 MIN(best / 5 + best, bddmaxnodesize - bddmaxnodeincrease - 2);
4256 else
4257 maxAllowed = best / 5 + best;
4258
4259
4260 if (blk.pos > middlePos)
4261 dirIsUp = false;
4262
4263
4264 for (n = 0; n < 2; n++) {
4265 int first = 1;
4266
4267 if (dirIsUp) {
4268 while (blk.prev != null
4269 && (reorder_nodenum() <= maxAllowed || first != 0)) {
4270 first = 0;
4271 blockdown(blk.prev);
4272 bestpos--;
4273
4274 if (verbose > 1) {
4275 System.out.print("-");
4276 System.out.flush();
4277 }
4278
4279 if (reorder_nodenum() < best) {
4280 best = reorder_nodenum();
4281 bestpos = 0;
4282
4283 if (bddmaxnodesize > 0)
4284 maxAllowed =
4285 MIN(
4286 best / 5 + best,
4287 bddmaxnodesize - bddmaxnodeincrease - 2);
4288 else
4289 maxAllowed = best / 5 + best;
4290 }
4291 }
4292 } else {
4293 while (blk.next != null
4294 && (reorder_nodenum() <= maxAllowed || first != 0)) {
4295 first = 0;
4296 blockdown(blk);
4297 bestpos++;
4298
4299 if (verbose > 1) {
4300 System.out.print("+");
4301 System.out.flush();
4302 }
4303
4304 if (reorder_nodenum() < best) {
4305 best = reorder_nodenum();
4306 bestpos = 0;
4307
4308 if (bddmaxnodesize > 0)
4309 maxAllowed =
4310 MIN(
4311 best / 5 + best,
4312 bddmaxnodesize - bddmaxnodeincrease - 2);
4313 else
4314 maxAllowed = best / 5 + best;
4315 }
4316 }
4317 }
4318
4319 if (reorder_nodenum() > maxAllowed && verbose > 1) {
4320 System.out.print("!");
4321 System.out.flush();
4322 }
4323
4324 dirIsUp = !dirIsUp;
4325 }
4326
4327
4328 while (bestpos < 0) {
4329 blockdown(blk);
4330 bestpos++;
4331 }
4332 while (bestpos > 0) {
4333 blockdown(blk.prev);
4334 bestpos--;
4335 }
4336 }
4337
4338 BddTree reorder_random(BddTree t) {
4339 BddTree dis;
4340 BddTree[] seq;
4341 int n, num = 0;
4342
4343 if (t == null)
4344 return t;
4345
4346 for (dis = t; dis != null; dis = dis.next)
4347 num++;
4348 seq = new BddTree[num];
4349 for (dis = t, num = 0; dis != null; dis = dis.next)
4350 seq[num++] = dis;
4351
4352 for (n = 0; n < 4 * num; n++) {
4353 int blk = rng.nextInt(num);
4354 if (seq[blk].next != null)
4355 blockdown(seq[blk]);
4356 }
4357
4358
4359 for (dis = t; dis.prev != null; dis = dis.prev)
4360
4361
4362 if (verbose != 0)
4363 System.out.println("Random order: " + reorder_nodenum() + " nodes");
4364 return dis;
4365 }
4366
4367 static int siftTestCmp(Object aa, Object bb) {
4368 sizePair a = (sizePair) aa;
4369 sizePair b = (sizePair) bb;
4370
4371 if (a.val < b.val)
4372 return -1;
4373 if (a.val > b.val)
4374 return 1;
4375 return 0;
4376 }
4377
4378 static class sizePair {
4379 int val;
4380 BddTree block;
4381 }
4382
4383 BddTree reorder_sift(BddTree t) {
4384 BddTree dis, seq[];
4385 sizePair[] p;
4386 int n, num;
4387
4388 for (dis = t, num = 0; dis != null; dis = dis.next)
4389 dis.pos = num++;
4390
4391 p = new sizePair[num];
4392 seq = new BddTree[num];
4393
4394 for (dis = t, n = 0; dis != null; dis = dis.next, n++) {
4395 int v;
4396
4397
4398 p[n].val = 0;
4399 for (v = dis.first; v <= dis.last; v++)
4400 p[n].val -= levels[v].nodenum;
4401
4402 p[n].block = dis;
4403 }
4404
4405
4406 Arrays.sort(p, 0, num, new Comparator() {
4407
4408 public int compare(Object o1, Object o2) {
4409 return siftTestCmp(o1, o2);
4410 }
4411
4412 });
4413
4414
4415 for (n = 0; n < num; n++)
4416 seq[n] = p[n].block;
4417
4418
4419 t = reorder_sift_seq(t, seq, num);
4420
4421 return t;
4422 }
4423
4424 BddTree reorder_siftite(BddTree t) {
4425 BddTree first = t;
4426 int lastsize;
4427 int c = 1;
4428
4429 if (t == null)
4430 return t;
4431
4432 do {
4433 if (verbose > 1)
4434 System.out.println("Reorder " + (c++) + "\n");
4435
4436 lastsize = reorder_nodenum();
4437 first = reorder_sift(first);
4438 } while (reorder_nodenum() != lastsize);
4439
4440 return first;
4441 }
4442
4443 void blockdown(BddTree left) {
4444 BddTree right = left.next;
4445 int n;
4446 int leftsize = left.last - left.first;
4447 int rightsize = right.last - right.first;
4448 int leftstart = bddvar2level[left.seq[0]];
4449 int[] lseq = left.seq;
4450 int[] rseq = right.seq;
4451
4452
4453 while (bddvar2level[lseq[0]] < bddvar2level[rseq[rightsize]]) {
4454 for (n = 0; n < leftsize; n++) {
4455 if (bddvar2level[lseq[n]] + 1 != bddvar2level[lseq[n + 1]]
4456 && bddvar2level[lseq[n]] < bddvar2level[rseq[rightsize]]) {
4457 reorder_vardown(lseq[n]);
4458 }
4459 }
4460
4461 if (bddvar2level[lseq[leftsize]] < bddvar2level[rseq[rightsize]]) {
4462 reorder_vardown(lseq[leftsize]);
4463 }
4464 }
4465
4466
4467 while (bddvar2level[rseq[0]] > leftstart) {
4468 for (n = rightsize; n > 0; n--) {
4469 if (bddvar2level[rseq[n]] - 1 != bddvar2level[rseq[n - 1]]
4470 && bddvar2level[rseq[n]] > leftstart) {
4471 reorder_varup(rseq[n]);
4472 }
4473 }
4474
4475 if (bddvar2level[rseq[0]] > leftstart)
4476 reorder_varup(rseq[0]);
4477 }
4478
4479
4480 left.next = right.next;
4481 right.prev = left.prev;
4482 left.prev = right;
4483 right.next = left;
4484
4485 if (right.prev != null)
4486 right.prev.next = right;
4487 if (left.next != null)
4488 left.next.prev = left;
4489
4490 n = left.pos;
4491 left.pos = right.pos;
4492 right.pos = n;
4493 }
4494
4495 BddTree reorder_win2ite(BddTree t) {
4496 BddTree dis, first = t;
4497 int lastsize;
4498 int c = 1;
4499
4500 if (t == null)
4501 return t;
4502
4503 if (verbose > 1)
4504 System.out.println(
4505 "Win2ite start: " + reorder_nodenum() + " nodes");
4506
4507 do {
4508 lastsize = reorder_nodenum();
4509
4510 dis = t;
4511 while (dis.next != null) {
4512 int best = reorder_nodenum();
4513
4514 blockdown(dis);
4515
4516 if (best < reorder_nodenum()) {
4517 blockdown(dis.prev);
4518 dis = dis.next;
4519 } else if (first == dis)
4520 first = dis.prev;
4521 if (verbose > 1) {
4522 System.out.print(".");
4523 System.out.flush();
4524 }
4525 }
4526
4527 if (verbose > 1)
4528 System.out.println(" " + reorder_nodenum() + " nodes");
4529 c++;
4530 }
4531 while (reorder_nodenum() != lastsize);
4532
4533 return first;
4534 }
4535
4536 void bdd_reorder_auto() {
4537 if (!bdd_reorder_ready())
4538 return;
4539
4540 bdd_reorder(bddreordermethod);
4541 bddreordertimes--;
4542 }
4543
4544 int bdd_reorder_gain() {
4545 if (usednum_before == 0)
4546 return 0;
4547
4548 return (100 * (usednum_before - usednum_after)) / usednum_before;
4549 }
4550
4551 void bdd_done() {
4552
4553
4554
4555 bdd_pairs_done();
4556
4557 bddnodes = null;
4558 bddrefstack = null;
4559 bddvarset = null;
4560 bddvar2level = null;
4561 bddlevel2var = null;
4562
4563 bdd_operator_done();
4564
4565 bddrunning = false;
4566 bddnodesize = 0;
4567 bddmaxnodesize = 0;
4568 bddvarnum = 0;
4569 bddproduced = 0;
4570
4571
4572
4573
4574 }
4575
4576 int bdd_setmaxnodenum(int size) {
4577 if (size > bddnodesize || size == 0) {
4578 int old = bddmaxnodesize;
4579 bddmaxnodesize = size;
4580 return old;
4581 }
4582
4583 return bdd_error(BDD_NODES);
4584 }
4585
4586 int bdd_setminfreenodes(int mf) {
4587 int old = minfreenodes;
4588
4589 if (mf < 0 || mf > 100)
4590 return bdd_error(BDD_RANGE);
4591
4592 minfreenodes = mf;
4593 return old;
4594 }
4595
4596 int bdd_setmaxincrease(int size) {
4597 int old = bddmaxnodeincrease;
4598
4599 if (size < 0)
4600 return bdd_error(BDD_SIZE);
4601
4602 bddmaxnodeincrease = size;
4603 return old;
4604 }
4605
4606 double increasefactor;
4607
4608 double bdd_setincreasefactor(double x) {
4609 if (x < 0)
4610 return bdd_error(BDD_RANGE);
4611 double old = increasefactor;
4612 increasefactor = x;
4613 return old;
4614 }
4615
4616 int bdd_setcacheratio(int r) {
4617 int old = cacheratio;
4618
4619 if (r <= 0)
4620 return bdd_error(BDD_RANGE);
4621 if (bddnodesize == 0)
4622 return old;
4623
4624 cacheratio = r;
4625 bdd_operator_noderesize();
4626 return old;
4627 }
4628
4629 int bdd_setvarnum(int num) {
4630 int bdv;
4631 int oldbddvarnum = bddvarnum;
4632
4633 bdd_disable_reorder();
4634
4635 if (num < 1 || num > MAXVAR) {
4636 bdd_error(BDD_RANGE);
4637 return bddfalse;
4638 }
4639
4640 if (num < bddvarnum)
4641 return bdd_error(BDD_DECVNUM);
4642 if (num == bddvarnum)
4643 return 0;
4644
4645 if (bddvarset == null) {
4646 bddvarset = new int[num * 2];
4647 bddlevel2var = new int[num + 1];
4648 bddvar2level = new int[num + 1];
4649 } else {
4650 int[] bddvarset2 = new int[num * 2];
4651 System.arraycopy(bddvarset, 0, bddvarset2, 0, bddvarset.length);
4652 bddvarset = bddvarset2;
4653 int[] bddlevel2var2 = new int[num + 1];
4654 System.arraycopy(
4655 bddlevel2var,
4656 0,
4657 bddlevel2var2,
4658 0,
4659 bddlevel2var.length);
4660 bddlevel2var = bddlevel2var2;
4661 int[] bddvar2level2 = new int[num + 1];
4662 System.arraycopy(
4663 bddvar2level,
4664 0,
4665 bddvar2level2,
4666 0,
4667 bddvar2level.length);
4668 bddvar2level = bddvar2level2;
4669 }
4670
4671 bddrefstack = new int[num * 2 + 1];
4672 bddrefstacktop = 0;
4673
4674 for (bdv = bddvarnum; bddvarnum < num; bddvarnum++) {
4675 bddvarset[bddvarnum * 2] = PUSHREF(bdd_makenode(bddvarnum, 0, 1));
4676 bddvarset[bddvarnum * 2 + 1] = bdd_makenode(bddvarnum, 1, 0);
4677 POPREF(1);
4678
4679 if (bdderrorcond != 0) {
4680 bddvarnum = bdv;
4681 return -bdderrorcond;
4682 }
4683
4684 SETMAXREF(bddvarset[bddvarnum * 2]);
4685 SETMAXREF(bddvarset[bddvarnum * 2 + 1]);
4686 bddlevel2var[bddvarnum] = bddvarnum;
4687 bddvar2level[bddvarnum] = bddvarnum;
4688 }
4689
4690 SETLEVEL(0, num);
4691 SETLEVEL(1, num);
4692 bddvar2level[num] = num;
4693 bddlevel2var[num] = num;
4694
4695 bdd_pairs_resize(oldbddvarnum, bddvarnum);
4696 bdd_operator_varresize();
4697
4698 bdd_enable_reorder();
4699
4700 return 0;
4701 }
4702
4703 static class BddTree {
4704 int first, last;
4705 int pos;
4706 int[] seq;
4707 boolean fixed;
4708 int id;
4709 BddTree next, prev;
4710 BddTree nextlevel;
4711 }
4712
4713
4714 int bddreordermethod;
4715 int bddreordertimes;
4716
4717
4718 int reorderdisabled;
4719
4720 BddTree vartree;
4721 int blockid;
4722
4723 int[] extroots;
4724 int extrootsize;
4725
4726 levelData levels[];
4727
4728 static class levelData {
4729 int start;
4730 int size;
4731 int maxsize;
4732 int nodenum;
4733 }
4734
4735 static class imatrix {
4736 byte rows[][];
4737 int size;
4738 }
4739
4740
4741 imatrix iactmtx;
4742
4743 int verbose;
4744
4745
4746
4747
4748
4749 int usednum_before;
4750 int usednum_after;
4751
4752 void bdd_reorder_init() {
4753 reorderdisabled = 0;
4754 vartree = null;
4755
4756 bdd_clrvarblocks();
4757
4758 bdd_reorder_verbose(0);
4759 bdd_autoreorder_times(BDD_REORDER_NONE, 0);
4760
4761 usednum_before = usednum_after = 0;
4762 blockid = 0;
4763 }
4764
4765 int reorder_nodenum() {
4766 return bdd_getnodenum();
4767 }
4768
4769 int bdd_getnodenum() {
4770 return bddnodesize - bddfreenum;
4771 }
4772
4773 int bdd_reorder_verbose(int v) {
4774 int tmp = verbose;
4775 verbose = v;
4776 return tmp;
4777 }
4778
4779 int bdd_autoreorder(int method) {
4780 int tmp = bddreordermethod;
4781 bddreordermethod = method;
4782 bddreordertimes = -1;
4783 return tmp;
4784 }
4785
4786 int bdd_autoreorder_times(int method, int num) {
4787 int tmp = bddreordermethod;
4788 bddreordermethod = method;
4789 bddreordertimes = num;
4790 return tmp;
4791 }
4792
4793 static final int BDD_REORDER_NONE = 0;
4794 static final int BDD_REORDER_WIN2 = 1;
4795 static final int BDD_REORDER_WIN2ITE = 2;
4796 static final int BDD_REORDER_SIFT = 3;
4797 static final int BDD_REORDER_SIFTITE = 4;
4798 static final int BDD_REORDER_WIN3 = 5;
4799 static final int BDD_REORDER_WIN3ITE = 6;
4800 static final int BDD_REORDER_RANDOM = 7;
4801
4802 static final int BDD_REORDER_FREE = 0;
4803 static final int BDD_REORDER_FIXED = 1;
4804
4805 static long c1;
4806
4807 void bdd_reorder_done() {
4808 bddtree_del(vartree);
4809 bdd_operator_reset();
4810 vartree = null;
4811 }
4812
4813 void bddtree_del(BddTree t) {
4814 if (t == null)
4815 return;
4816
4817 bddtree_del(t.nextlevel);
4818 bddtree_del(t.next);
4819 t.seq = null;
4820 }
4821
4822 void bdd_clrvarblocks() {
4823 bddtree_del(vartree);
4824 vartree = null;
4825 blockid = 0;
4826 }
4827
4828 int NODEHASHr(int var, int l, int h) {
4829 return (Math.abs(PAIR(l, (h)) % levels[var].size) + levels[var].start);
4830 }
4831
4832 void bdd_setvarorder(int[] neworder) {
4833 int level;
4834
4835
4836 if (vartree != null) {
4837 bdd_error(BDD_VARBLK);
4838 return;
4839 }
4840
4841 reorder_init();
4842
4843 for (level = 0; level < bddvarnum; level++) {
4844 int lowvar = neworder[level];
4845
4846 while (bddvar2level[lowvar] > level)
4847 reorder_varup(lowvar);
4848 }
4849
4850 reorder_done();
4851 }
4852
4853 int reorder_varup(int var) {
4854 if (var < 0 || var >= bddvarnum)
4855 return bdd_error(BDD_VAR);
4856 if (bddvar2level[var] == 0)
4857 return 0;
4858 return reorder_vardown(bddlevel2var[bddvar2level[var] - 1]);
4859 }
4860
4861 int reorder_vardown(int var) {
4862 int n, level;
4863
4864 if (var < 0 || var >= bddvarnum)
4865 return bdd_error(BDD_VAR);
4866 if ((level = bddvar2level[var]) >= bddvarnum - 1)
4867 return 0;
4868
4869 resizedInMakenode = false;
4870
4871 if (imatrixDepends(iactmtx, var, bddlevel2var[level + 1])) {
4872 int toBeProcessed = reorder_downSimple(var);
4873 levelData l = levels[var];
4874
4875 if (l.nodenum < (l.size) / 3
4876 || l.nodenum >= (l.size * 3) / 2
4877 && l.size < l.maxsize) {
4878 reorder_swapResize(toBeProcessed, var);
4879 reorder_localGbcResize(toBeProcessed, var);
4880 } else {
4881 reorder_swap(toBeProcessed, var);
4882 reorder_localGbc(var);
4883 }
4884 }
4885
4886
4887 n = bddlevel2var[level];
4888 bddlevel2var[level] = bddlevel2var[level + 1];
4889 bddlevel2var[level + 1] = n;
4890
4891 n = bddvar2level[var];
4892 bddvar2level[var] = bddvar2level[bddlevel2var[level]];
4893 bddvar2level[bddlevel2var[level]] = n;
4894
4895
4896 bdd_pairs_vardown(level);
4897
4898 if (resizedInMakenode)
4899 reorder_rehashAll();
4900
4901 return 0;
4902 }
4903
4904 boolean imatrixDepends(imatrix mtx, int a, int b) {
4905 return (mtx.rows[a][b / 8] & (1 << (b % 8))) != 0;
4906 }
4907
4908 void reorder_setLevellookup() {
4909 int n;
4910
4911 for (n = 0; n < bddvarnum; n++) {
4912 levels[n].maxsize = bddnodesize / bddvarnum;
4913 levels[n].start = n * levels[n].maxsize;
4914 levels[n].size =
4915 Math.min(levels[n].maxsize, (levels[n].nodenum * 5) / 4);
4916
4917 if (levels[n].size >= 4)
4918 levels[n].size = bdd_prime_lte(levels[n].size);
4919
4920 }
4921 }
4922
4923 void reorder_rehashAll() {
4924 int n;
4925
4926 reorder_setLevellookup();
4927 bddfreepos = 0;
4928
4929 for (n = bddnodesize - 1; n >= 0; n--)
4930 SETHASH(n, 0);
4931
4932 for (n = bddnodesize - 1; n >= 2; n--) {
4933
4934 if (HASREF(n)) {
4935 int hash2;
4936
4937 hash2 = NODEHASH2(VARr(n), LOW(n), HIGH(n));
4938 SETNEXT(n, hash2);
4939 SETHASH(hash2, n);
4940 } else {
4941 SETNEXT(n, bddfreepos);
4942 bddfreepos = n;
4943 }
4944 }
4945 }
4946
4947 void reorder_localGbc(int var0) {
4948 int var1 = bddlevel2var[bddvar2level[var0] + 1];
4949 int vl1 = levels[var1].start;
4950 int size1 = levels[var1].size;
4951 int n;
4952
4953 for (n = 0; n < size1; n++) {
4954 int hash = n + vl1;
4955 int r = HASH(hash);
4956 SETHASH(hash, 0);
4957
4958 while (r != 0) {
4959 int next = NEXT(r);
4960
4961 if (HASREF(r)) {
4962 SETNEXT(r, HASH(hash));
4963 SETHASH(hash, r);
4964 } else {
4965 DECREF(LOW(r));
4966 DECREF(HIGH(r));
4967
4968 SETLOW(r, INVALID_BDD);
4969 SETNEXT(r, bddfreepos);
4970 bddfreepos = r;
4971 levels[var1].nodenum--;
4972 bddfreenum++;
4973 }
4974
4975 r = next;
4976 }
4977 }
4978 }
4979
4980 int reorder_downSimple(int var0) {
4981 int toBeProcessed = 0;
4982 int var1 = bddlevel2var[bddvar2level[var0] + 1];
4983 int vl0 = levels[var0].start;
4984 int size0 = levels[var0].size;
4985 int n;
4986
4987 levels[var0].nodenum = 0;
4988
4989 for (n = 0; n < size0; n++) {
4990 int r;
4991
4992 r = HASH(n + vl0);
4993 SETHASH(n + vl0, 0);
4994
4995 while (r != 0) {
4996 int next = NEXT(r);
4997
4998 if (VARr(LOW(r)) != var1 && VARr(HIGH(r)) != var1) {
4999
5000 SETNEXT(r, HASH(n + vl0));
5001 SETHASH(n + vl0, r);
5002 levels[var0].nodenum++;
5003 } else {
5004
5005 SETNEXT(r, toBeProcessed);
5006 toBeProcessed = r;
5007 if (SWAPCOUNT)
5008 cachestats.swapCount++;
5009
5010 }
5011
5012 r = next;
5013 }
5014 }
5015
5016 return toBeProcessed;
5017 }
5018
5019 void reorder_swapResize(int toBeProcessed, int var0) {
5020 int var1 = bddlevel2var[bddvar2level[var0] + 1];
5021
5022 while (toBeProcessed != 0) {
5023 int next = NEXT(toBeProcessed);
5024 int f0 = LOW(toBeProcessed);
5025 int f1 = HIGH(toBeProcessed);
5026 int f00, f01, f10, f11;
5027
5028
5029 if (VARr(f0) == var1) {
5030 f00 = LOW(f0);
5031 f01 = HIGH(f0);
5032 } else
5033 f00 = f01 = f0;
5034
5035 if (VARr(f1) == var1) {
5036 f10 = LOW(f1);
5037 f11 = HIGH(f1);
5038 } else
5039 f10 = f11 = f1;
5040
5041
5042 f0 = reorder_makenode(var0, f00, f10);
5043 f1 = reorder_makenode(var0, f01, f11);
5044
5045
5046
5047
5048
5049
5050
5051
5052 DECREF(LOW(toBeProcessed));
5053 DECREF(HIGH(toBeProcessed));
5054
5055
5056 SETVARr(toBeProcessed, var1);
5057 SETLOW(toBeProcessed, f0);
5058 SETHIGH(toBeProcessed, f1);
5059
5060 levels[var1].nodenum++;
5061
5062
5063
5064 toBeProcessed = next;
5065 }
5066 }
5067
5068 static final int MIN(int a, int b) {
5069 return Math.min(a, b);
5070 }
5071
5072 void reorder_localGbcResize(int toBeProcessed, int var0) {
5073 int var1 = bddlevel2var[bddvar2level[var0] + 1];
5074 int vl1 = levels[var1].start;
5075 int size1 = levels[var1].size;
5076 int n;
5077
5078 for (n = 0; n < size1; n++) {
5079 int hash = n + vl1;
5080 int r = HASH(hash);
5081 SETHASH(hash, 0);
5082
5083 while (r != 0) {
5084 int next = NEXT(r);
5085
5086 if (HASREF(r)) {
5087 SETNEXT(r, toBeProcessed);
5088 toBeProcessed = r;
5089 } else {
5090 DECREF(LOW(r));
5091 DECREF(HIGH(r));
5092
5093 SETLOW(r, INVALID_BDD);
5094 SETNEXT(r, bddfreepos);
5095 bddfreepos = r;
5096 levels[var1].nodenum--;
5097 bddfreenum++;
5098 }
5099
5100 r = next;
5101 }
5102 }
5103
5104
5105 if (levels[var1].nodenum < levels[var1].size)
5106 levels[var1].size =
5107 MIN(levels[var1].maxsize, levels[var1].size / 2);
5108 else
5109 levels[var1].size =
5110 MIN(levels[var1].maxsize, levels[var1].size * 2);
5111
5112 if (levels[var1].size >= 4)
5113 levels[var1].size = bdd_prime_lte(levels[var1].size);
5114
5115
5116 while (toBeProcessed != 0) {
5117 int next = NEXT(toBeProcessed);
5118 int hash = NODEHASH2(VARr(toBeProcessed), LOW(toBeProcessed), HIGH(toBeProcessed));
5119
5120 SETNEXT(toBeProcessed, HASH(hash));
5121 SETHASH(hash, toBeProcessed);
5122
5123 toBeProcessed = next;
5124 }
5125 }
5126
5127 void reorder_swap(int toBeProcessed, int var0) {
5128 int var1 = bddlevel2var[bddvar2level[var0] + 1];
5129
5130 while (toBeProcessed != 0) {
5131 int next = NEXT(toBeProcessed);
5132 int f0 = LOW(toBeProcessed);
5133 int f1 = HIGH(toBeProcessed);
5134 int f00, f01, f10, f11, hash;
5135
5136
5137 if (VARr(f0) == var1) {
5138 f00 = LOW(f0);
5139 f01 = HIGH(f0);
5140 } else
5141 f00 = f01 = f0;
5142
5143 if (VARr(f1) == var1) {
5144 f10 = LOW(f1);
5145 f11 = HIGH(f1);
5146 } else
5147 f10 = f11 = f1;
5148
5149
5150 f0 = reorder_makenode(var0, f00, f10);
5151 f1 = reorder_makenode(var0, f01, f11);
5152
5153
5154
5155
5156
5157
5158
5159
5160 DECREF(LOW(toBeProcessed));
5161 DECREF(HIGH(toBeProcessed));
5162
5163
5164 SETVARr(toBeProcessed, var1);
5165 SETLOW(toBeProcessed, f0);
5166 SETHIGH(toBeProcessed, f1);
5167
5168 levels[var1].nodenum++;
5169
5170
5171 hash = NODEHASH2(VARr(toBeProcessed), LOW(toBeProcessed), HIGH(toBeProcessed));
5172 SETNEXT(toBeProcessed, HASH(hash));
5173 SETHASH(hash, toBeProcessed);
5174
5175 toBeProcessed = next;
5176 }
5177 }
5178
5179 int NODEHASH2(int var, int l, int h) {
5180 return (Math.abs(PAIR(l, h) % levels[var].size) + levels[var].start);
5181 }
5182
5183 boolean resizedInMakenode;
5184
5185 int reorder_makenode(int var, int low, int high) {
5186 int hash;
5187 int res;
5188
5189 if (CACHESTATS > 0) cachestats.uniqueAccess++;
5190
5191
5192
5193
5194
5195 if (low == high) {
5196 INCREF(low);
5197 return low;
5198 }
5199
5200
5201 hash = NODEHASH2(var, low, high);
5202 res = HASH(hash);
5203
5204 while (res != 0) {
5205 if (LOW(res) == low && HIGH(res) == high) {
5206 if (CACHESTATS > 0) cachestats.uniqueHit++;
5207 INCREF(res);
5208 return res;
5209 }
5210 res = NEXT(res);
5211
5212 if (CACHESTATS > 0) cachestats.uniqueChain++;
5213 }
5214
5215
5216 if (CACHESTATS > 0) cachestats.uniqueMiss++;
5217
5218
5219 if (bddfreepos == 0) {
5220 if (bdderrorcond != 0)
5221 return 0;
5222
5223
5224
5225
5226
5227 bdd_noderesize(false);
5228 resizedInMakenode = true;
5229
5230
5231 if (bddfreepos == 0) {
5232 bdd_error(BDD_NODENUM);
5233 bdderrorcond = Math.abs(BDD_NODENUM);
5234 return 0;
5235 }
5236 }
5237
5238
5239 res = bddfreepos;
5240 bddfreepos = NEXT(bddfreepos);
5241 levels[var].nodenum++;
5242 bddproduced++;
5243 bddfreenum--;
5244
5245 SETVARr(res, var);
5246 SETLOW(res, low);
5247 SETHIGH(res, high);
5248
5249
5250 SETNEXT(res, HASH(hash));
5251 SETHASH(hash, res);
5252
5253
5254 CLEARREF(res);
5255 INCREF(res);
5256 INCREF(LOW(res));
5257 INCREF(HIGH(res));
5258
5259 return res;
5260 }
5261
5262 int reorder_init() {
5263 int n;
5264
5265 reorder_handler(true, reorderstats);
5266
5267 levels = new levelData[bddvarnum];
5268
5269 for (n = 0; n < bddvarnum; n++) {
5270 levels[n] = new levelData();
5271 levels[n].start = -1;
5272 levels[n].size = 0;
5273 levels[n].nodenum = 0;
5274 }
5275
5276
5277
5278 if (mark_roots() < 0)
5279 return -1;
5280
5281
5282 reorder_setLevellookup();
5283
5284
5285 reorder_gbc();
5286
5287 return 0;
5288 }
5289
5290 int mark_roots() {
5291 boolean[] dep = new boolean[bddvarnum];
5292 int n;
5293
5294 for (n = 2, extrootsize = 0; n < bddnodesize; n++) {
5295
5296 int lev = LEVEL(n);
5297 int var = bddlevel2var[lev];
5298 SETVARr(n, var);
5299
5300 if (HASREF(n)) {
5301 SETMARK(n);
5302 extrootsize++;
5303 }
5304 }
5305
5306 extroots = new int[extrootsize];
5307
5308 iactmtx = imatrixNew(bddvarnum);
5309
5310 for (n = 2, extrootsize = 0; n < bddnodesize; n++) {
5311
5312 if (MARKED(n)) {
5313 UNMARK(n);
5314 extroots[extrootsize++] = n;
5315
5316 for (int i = 0; i < bddvarnum; ++i)
5317 dep[i] = false;
5318 dep[VARr(n)] = true;
5319 levels[VARr(n)].nodenum++;
5320
5321 addref_rec(LOW(n), dep);
5322 addref_rec(HIGH(n), dep);
5323
5324 addDependencies(dep);
5325 }
5326
5327
5328
5329 SETHASH(n, 0);
5330 }
5331
5332 SETHASH(0, 0);
5333 SETHASH(1, 0);
5334
5335 return 0;
5336 }
5337
5338 imatrix imatrixNew(int size) {
5339 imatrix mtx = new imatrix();
5340 int n;
5341
5342 mtx.rows = new byte[size][];
5343
5344 for (n = 0; n < size; n++) {
5345 mtx.rows[n] = new byte[size / 8 + 1];
5346 }
5347
5348 mtx.size = size;
5349
5350 return mtx;
5351 }
5352
5353 void addref_rec(int r, boolean[] dep) {
5354 if (r < 2)
5355 return;
5356
5357 if (!HASREF(r) || MARKED(r)) {
5358 bddfreenum--;
5359
5360
5361 dep[VARr(r) & ~MARK_MASK] = true;
5362
5363
5364 levels[VARr(r) & ~MARK_MASK].nodenum++;
5365
5366 addref_rec(LOW(r), dep);
5367 addref_rec(HIGH(r), dep);
5368 } else {
5369 int n;
5370
5371
5372
5373 for (n = 0; n < bddvarnum; n++)
5374 dep[n]
5375 |= imatrixDepends(iactmtx, VARr(r) & ~MARK_MASK, n);
5376 }
5377
5378 INCREF(r);
5379 }
5380
5381 void addDependencies(boolean[] dep) {
5382 int n, m;
5383
5384 for (n = 0; n < bddvarnum; n++) {
5385 for (m = n; m < bddvarnum; m++) {
5386 if ((dep[n]) && (dep[m])) {
5387 imatrixSet(iactmtx, n, m);
5388 imatrixSet(iactmtx, m, n);
5389 }
5390 }
5391 }
5392 }
5393
5394 void imatrixSet(imatrix mtx, int a, int b) {
5395 mtx.rows[a][b / 8] |= 1 << (b % 8);
5396 }
5397
5398 void reorder_gbc() {
5399 int n;
5400
5401 bddfreepos = 0;
5402 bddfreenum = 0;
5403
5404
5405
5406 for (n = bddnodesize - 1; n >= 2; n--) {
5407
5408 if (HASREF(n)) {
5409 int hash;
5410
5411 hash = NODEHASH2(VARr(n), LOW(n), HIGH(n));
5412 SETNEXT(n, HASH(hash));
5413 SETHASH(hash, n);
5414
5415 } else {
5416 SETLOW(n, INVALID_BDD);
5417 SETNEXT(n, bddfreepos);
5418 bddfreepos = n;
5419 bddfreenum++;
5420 }
5421 }
5422 }
5423
5424 void reorder_done() {
5425 int n;
5426
5427 for (n = 0; n < extrootsize; n++)
5428 SETMARK(extroots[n]);
5429 for (n = 2; n < bddnodesize; n++) {
5430 if (MARKED(n))
5431 UNMARK(n);
5432 else
5433 CLEARREF(n);
5434
5435
5436 SETLEVEL(n, bddvar2level[VARr(n)]);
5437 }
5438
5439 imatrixDelete(iactmtx);
5440 bdd_gbc();
5441
5442 reorder_handler(false, reorderstats);
5443 }
5444
5445 void imatrixDelete(imatrix mtx) {
5446 int n;
5447
5448 for (n = 0; n < mtx.size; n++) {
5449 mtx.rows[n] = null;
5450 }
5451 mtx.rows = null;
5452 }
5453
5454 int bdd_getallocnum() {
5455 return bddnodesize;
5456 }
5457
5458 int bdd_swapvar(int v1, int v2) {
5459 int l1, l2;
5460
5461
5462 if (vartree != null)
5463 return bdd_error(BDD_VARBLK);
5464
5465
5466 if (v1 == v2)
5467 return 0;
5468
5469
5470 if (v1 < 0 || v1 >= bddvarnum || v2 < 0 || v2 >= bddvarnum)
5471 return bdd_error(BDD_VAR);
5472
5473 l1 = bddvar2level[v1];
5474 l2 = bddvar2level[v2];
5475
5476
5477 if (l1 > l2) {
5478 int tmp = v1;
5479 v1 = v2;
5480 v2 = tmp;
5481 l1 = bddvar2level[v1];
5482 l2 = bddvar2level[v2];
5483 }
5484
5485 reorder_init();
5486
5487
5488 while (bddvar2level[v1] < l2)
5489 reorder_vardown(v1);
5490
5491
5492 while (bddvar2level[v2] > l1)
5493 reorder_varup(v2);
5494
5495 reorder_done();
5496
5497 return 0;
5498 }
5499
5500 void bdd_fprintall(PrintStream out) {
5501 int n;
5502
5503 for (n = 0; n < bddnodesize; n++) {
5504 if (LOW(n) != INVALID_BDD) {
5505 out.print(
5506 "["
5507 + right(n, 5)
5508 + " - "
5509 + right(GETREF(n), 2)
5510 + "] ");
5511
5512 out.print(right(bddlevel2var[LEVEL(n)], 3));
5513
5514 out.print(": " + right(LOW(n), 3));
5515 out.println(" " + right(HIGH(n), 3));
5516 }
5517 }
5518 }
5519
5520 void bdd_fprinttable(PrintStream out, int r) {
5521 int n;
5522
5523 out.println("ROOT: " + r);
5524 if (r < 2)
5525 return;
5526
5527 bdd_mark(r);
5528
5529 for (n = 0; n < bddnodesize; n++) {
5530 if (MARKED(n)) {
5531 UNMARK(n);
5532
5533 out.print("[" + right(n, 5) + "] ");
5534
5535 out.print(right(bddlevel2var[LEVEL(n)], 3));
5536
5537 out.print(": " + right(LOW(n), 3));
5538 out.println(" " + right(HIGH(n), 3));
5539 }
5540 }
5541 }
5542
5543 int lh_nodenum;
5544 int lh_freepos;
5545 int[] loadvar2level;
5546 LoadHash[] lh_table;
5547
5548 int bdd_load(BufferedReader ifile, int[] translate) throws IOException {
5549 int n, vnum, tmproot;
5550 int root;
5551
5552 lh_nodenum = Integer.parseInt(readNext(ifile));
5553 vnum = Integer.parseInt(readNext(ifile));
5554
5555
5556 if (lh_nodenum == 0 && vnum == 0) {
5557 root = Integer.parseInt(readNext(ifile));
5558 return root;
5559 }
5560
5561
5562 loadvar2level = new int[vnum];
5563 for (n = 0; n < vnum; n++) {
5564 loadvar2level[n] = Integer.parseInt(readNext(ifile));
5565 }
5566
5567 if (vnum > bddvarnum)
5568 bdd_setvarnum(vnum);
5569
5570 lh_table = new LoadHash[lh_nodenum];
5571
5572 for (n = 0; n < lh_nodenum; n++) {
5573 lh_table[n] = new LoadHash();
5574 lh_table[n].first = -1;
5575 lh_table[n].next = n + 1;
5576 }
5577 lh_table[lh_nodenum - 1].next = -1;
5578 lh_freepos = 0;
5579
5580 tmproot = bdd_loaddata(ifile, translate);
5581
5582 for (n = 0; n < lh_nodenum; n++)
5583 bdd_delref(lh_table[n].data);
5584
5585 lh_table = null;
5586 loadvar2level = null;
5587
5588 root = tmproot;
5589 return root;
5590 }
5591
5592 static class LoadHash {
5593 int key;
5594 int data;
5595 int first;
5596 int next;
5597 }
5598
5599 int bdd_loaddata(BufferedReader ifile, int[] translate) throws IOException {
5600 int key, var, low, high, root = 0, n;
5601
5602 for (n = 0; n < lh_nodenum; n++) {
5603 key = Integer.parseInt(readNext(ifile));
5604 var = Integer.parseInt(readNext(ifile));
5605 if (translate != null)
5606 var = translate[var];
5607 low = Integer.parseInt(readNext(ifile));
5608 high = Integer.parseInt(readNext(ifile));
5609
5610 if (low >= 2)
5611 low = loadhash_get(low);
5612 if (high >= 2)
5613 high = loadhash_get(high);
5614
5615 if (low < 0 || high < 0 || var < 0)
5616 return bdd_error(BDD_FORMAT);
5617
5618 root = bdd_addref(bdd_ite(bdd_ithvar(var), high, low));
5619
5620 loadhash_add(key, root);
5621 }
5622
5623 return root;
5624 }
5625
5626 void loadhash_add(int key, int data) {
5627 int hash = key % lh_nodenum;
5628 int pos = lh_freepos;
5629
5630 lh_freepos = lh_table[pos].next;
5631 lh_table[pos].next = lh_table[hash].first;
5632 lh_table[hash].first = pos;
5633
5634 lh_table[pos].key = key;
5635 lh_table[pos].data = data;
5636 }
5637
5638 int loadhash_get(int key) {
5639 int hash = lh_table[key % lh_nodenum].first;
5640
5641 while (hash != -1 && lh_table[hash].key != key)
5642 hash = lh_table[hash].next;
5643
5644 if (hash == -1)
5645 return -1;
5646 return lh_table[hash].data;
5647 }
5648
5649 void bdd_save(BufferedWriter out, int r) throws IOException {
5650 int[] n = new int[1];
5651
5652 if (r < 2) {
5653 out.write("0 0 " + r + "\n");
5654 return;
5655 }
5656
5657 bdd_markcount(r, n);
5658 bdd_unmark(r);
5659 out.write(n[0] + " " + bddvarnum + "\n");
5660
5661 for (int x = 0; x < bddvarnum; x++)
5662 out.write(bddvar2level[x] + " ");
5663 out.write("\n");
5664
5665 bdd_save_rec(out, r);
5666 bdd_unmark(r);
5667
5668 return;
5669 }
5670
5671 void bdd_save_rec(BufferedWriter out, int root) throws IOException {
5672
5673 if (root < 2)
5674 return;
5675
5676 if (MARKED(root))
5677 return;
5678 SETMARK(root);
5679
5680 bdd_save_rec(out, LOW(root));
5681 bdd_save_rec(out, HIGH(root));
5682
5683 out.write(root + " ");
5684 out.write(bddlevel2var[LEVEL(root)] + " ");
5685 out.write(LOW(root) + " ");
5686 out.write(HIGH(root) + "\n");
5687
5688 return;
5689 }
5690
5691 static String right(int x, int w) {
5692 return right(Integer.toString(x), w);
5693 }
5694 static String right(String s, int w) {
5695 int n = s.length();
5696
5697 StringBuffer b = new StringBuffer(w);
5698 for (int i = n; i < w; ++i) {
5699 b.append(' ');
5700 }
5701 b.append(s);
5702 return b.toString();
5703 }
5704
5705 int bdd_intaddvarblock(int first, int last, boolean fixed) {
5706 BddTree t;
5707
5708 if (first < 0 || first >= bddvarnum || last < 0 || last >= bddvarnum)
5709 return bdd_error(BDD_VAR);
5710
5711 if ((t = bddtree_addrange(vartree, first, last, fixed, blockid))
5712 == null)
5713 return bdd_error(BDD_VARBLK);
5714
5715 vartree = t;
5716 return blockid++;
5717 }
5718
5719 BddTree bddtree_addrange_rec(
5720 BddTree t,
5721 BddTree prev,
5722 int first,
5723 int last,
5724 boolean fixed,
5725 int id) {
5726 if (first < 0 || last < 0 || last < first)
5727 return null;
5728
5729
5730 if (t == null) {
5731 if ((t = bddtree_new(id)) == null)
5732 return null;
5733 t.first = first;
5734 t.fixed = fixed;
5735 t.seq = new int[last - first + 1];
5736 t.last = last;
5737 update_seq(t);
5738 t.prev = prev;
5739 return t;
5740 }
5741
5742
5743 if (first == t.first && last == t.last)
5744 return t;
5745
5746
5747 if (last < t.first) {
5748 BddTree tnew = bddtree_new(id);
5749 if (tnew == null)
5750 return null;
5751 tnew.first = first;
5752 tnew.last = last;
5753 tnew.fixed = fixed;
5754 tnew.seq = new int[last - first + 1];
5755 update_seq(tnew);
5756 tnew.next = t;
5757 tnew.prev = t.prev;
5758 t.prev = tnew;
5759 return tnew;
5760 }
5761
5762
5763 if (first > t.last) {
5764 t.next = bddtree_addrange_rec(t.next, t, first, last, fixed, id);
5765 return t;
5766 }
5767
5768
5769 if (first >= t.first && last <= t.last) {
5770 t.nextlevel =
5771 bddtree_addrange_rec(t.nextlevel, null, first, last, fixed, id);
5772 return t;
5773 }
5774
5775
5776 if (first <= t.first) {
5777 BddTree tnew;
5778 BddTree dis = t;
5779
5780 while (true) {
5781
5782 if (last >= dis.first && last < dis.last)
5783 return null;
5784
5785 if (dis.next == null || last < dis.next.first) {
5786 tnew = bddtree_new(id);
5787 if (tnew == null)
5788 return null;
5789 tnew.first = first;
5790 tnew.last = last;
5791 tnew.fixed = fixed;
5792 tnew.seq = new int[last - first + 1];
5793 update_seq(tnew);
5794 tnew.nextlevel = t;
5795 tnew.next = dis.next;
5796 tnew.prev = t.prev;
5797 if (dis.next != null)
5798 dis.next.prev = tnew;
5799 dis.next = null;
5800 t.prev = null;
5801 return tnew;
5802 }
5803
5804 dis = dis.next;
5805 }
5806
5807 }
5808
5809 return null;
5810 }
5811
5812 void update_seq(BddTree t) {
5813 int n;
5814 int low = t.first;
5815
5816 for (n = t.first; n <= t.last; n++)
5817 if (bddvar2level[n] < bddvar2level[low])
5818 low = n;
5819
5820 for (n = t.first; n <= t.last; n++)
5821 t.seq[bddvar2level[n] - bddvar2level[low]] = n;
5822 }
5823
5824 BddTree bddtree_addrange(
5825 BddTree t,
5826 int first,
5827 int last,
5828 boolean fixed,
5829 int id) {
5830 return bddtree_addrange_rec(t, null, first, last, fixed, id);
5831 }
5832
5833 void bdd_varblockall() {
5834 int n;
5835
5836 for (n = 0; n < bddvarnum; n++)
5837 bdd_intaddvarblock(n, n, true);
5838 }
5839
5840 void print_order_rec(PrintStream o, BddTree t, int level) {
5841 if (t == null)
5842 return;
5843
5844 if (t.nextlevel != null) {
5845 for (int i = 0; i < level; ++i)
5846 o.print(" ");
5847
5848 o.print(right(t.id, 3));
5849 o.println("{\n");
5850
5851 print_order_rec(o, t.nextlevel, level + 1);
5852
5853 for (int i = 0; i < level; ++i)
5854 o.print(" ");
5855
5856 o.print(right(t.id, 3));
5857 o.println("}\n");
5858
5859 print_order_rec(o, t.next, level);
5860 } else {
5861 for (int i = 0; i < level; ++i)
5862 o.print(" ");
5863
5864 o.println(right(t.id, 3));
5865
5866 print_order_rec(o, t.next, level);
5867 }
5868 }
5869
5870 void bdd_fprintorder(PrintStream ofile) {
5871 print_order_rec(ofile, vartree, 0);
5872 }
5873
5874 void bdd_fprintstat(PrintStream out) {
5875 CacheStats s = cachestats;
5876 out.print(s.toString());
5877 }
5878
5879 void bdd_validate_all() {
5880 int n;
5881 for (n = bddnodesize - 1; n >= 2; n--) {
5882 if (HASREF(n)) {
5883 bdd_validate(n);
5884 }
5885 }
5886 }
5887 void bdd_validate(int k) {
5888 bdd_validate(k, -1);
5889 }
5890 void bdd_validate(int k, int lastLevel) {
5891 if (k < 2) return;
5892 int lev = LEVEL(k);
5893
5894 if (lev <= lastLevel)
5895 throw new BDDException(lev+" <= "+lastLevel);
5896
5897 bdd_validate(LOW(k), lev);
5898
5899 bdd_validate(HIGH(k), lev);
5900 }
5901
5902
5903
5904 Random rng = new Random();
5905
5906 final int Random(int i) {
5907 return rng.nextInt(i) + 1;
5908 }
5909
5910 static boolean isEven(int src) {
5911 return (src & 0x1) == 0;
5912 }
5913
5914 static boolean hasFactor(int src, int n) {
5915 return (src != n) && (src % n == 0);
5916 }
5917
5918 static boolean BitIsSet(int src, int b) {
5919 return (src & (1 << b)) != 0;
5920 }
5921
5922 static final int CHECKTIMES = 20;
5923
5924 static final int u64_mulmod(int a, int b, int c) {
5925 return (int) (((long) a * (long) b) % (long) c);
5926 }
5927
5928 /**************************************************************************
5929 Miller Rabin check
5930 *************************************************************************/
5931
5932 static int numberOfBits(int src) {
5933 int b;
5934
5935 if (src == 0)
5936 return 0;
5937
5938 for (b = 31; b > 0; --b)
5939 if (BitIsSet(src, b))
5940 return b + 1;
5941
5942 return 1;
5943 }
5944
5945 static boolean isWitness(int witness, int src) {
5946 int bitNum = numberOfBits(src - 1) - 1;
5947 int d = 1;
5948 int i;
5949
5950 for (i = bitNum; i >= 0; --i) {
5951 int x = d;
5952
5953 d = u64_mulmod(d, d, src);
5954
5955 if (d == 1 && x != 1 && x != src - 1)
5956 return true;
5957
5958 if (BitIsSet(src - 1, i))
5959 d = u64_mulmod(d, witness, src);
5960 }
5961
5962 return d != 1;
5963 }
5964
5965 boolean isMillerRabinPrime(int src) {
5966 int n;
5967
5968 for (n = 0; n < CHECKTIMES; ++n) {
5969 int witness = Random(src - 1);
5970
5971 if (isWitness(witness, src))
5972 return false;
5973 }
5974
5975 return true;
5976 }
5977
5978 /**************************************************************************
5979 Basic prime searching stuff
5980 *************************************************************************/
5981
5982 static boolean hasEasyFactors(int src) {
5983 return hasFactor(src, 3)
5984 || hasFactor(src, 5)
5985 || hasFactor(src, 7)
5986 || hasFactor(src, 11)
5987 || hasFactor(src, 13);
5988 }
5989
5990 boolean isPrime(int src) {
5991 if (hasEasyFactors(src))
5992 return false;
5993
5994 return isMillerRabinPrime(src);
5995 }
5996
5997 /**************************************************************************
5998 External interface
5999 *************************************************************************/
6000
6001 int bdd_prime_gte(int src) {
6002 if (isEven(src))
6003 ++src;
6004
6005 while (!isPrime(src))
6006 src += 2;
6007
6008 return src;
6009 }
6010
6011 int bdd_prime_lte(int src) {
6012 if (isEven(src))
6013 --src;
6014
6015 while (!isPrime(src))
6016 src -= 2;
6017
6018 return src;
6019 }
6020
6021
6022
6023
6024 public CacheStats getCacheStats() {
6025 cachestats.opHit = 0;
6026 cachestats.opMiss = 0;
6027 if (singlecache != null) {
6028 System.out.println("Single cache: "+singlecache);
6029 cachestats.opHit += singlecache.cacheHit;
6030 cachestats.opMiss += singlecache.cacheMiss;
6031 }
6032 if (replacecache != null) {
6033 System.out.println("Replace cache: "+replacecache);
6034 cachestats.opHit += replacecache.cacheHit;
6035 cachestats.opMiss += replacecache.cacheMiss;
6036 }
6037 if (andcache != null) {
6038 System.out.println("And cache: "+andcache);
6039 cachestats.opHit += andcache.cacheHit;
6040 cachestats.opMiss += andcache.cacheMiss;
6041 }
6042 if (orcache != null) {
6043 System.out.println("Or cache: "+orcache);
6044 cachestats.opHit += orcache.cacheHit;
6045 cachestats.opMiss += orcache.cacheMiss;
6046 }
6047 if (applycache != null) {
6048 System.out.println("Apply cache: "+applycache);
6049 cachestats.opHit += applycache.cacheHit;
6050 cachestats.opMiss += applycache.cacheMiss;
6051 }
6052 if (quantcache != null) {
6053 System.out.println("Quant cache: "+quantcache);
6054 cachestats.opHit += quantcache.cacheHit;
6055 cachestats.opMiss += quantcache.cacheMiss;
6056 }
6057 if (appexcache != null) {
6058 System.out.println("Appex cache: "+appexcache);
6059 cachestats.opHit += appexcache.cacheHit;
6060 cachestats.opMiss += appexcache.cacheMiss;
6061 }
6062 if (appex3cache != null) {
6063 System.out.println("Appex3 cache: "+appex3cache);
6064 cachestats.opHit += appex3cache.cacheHit;
6065 cachestats.opMiss += appex3cache.cacheMiss;
6066 }
6067 if (itecache != null) {
6068 System.out.println("ITE cache: "+itecache);
6069 cachestats.opHit += itecache.cacheHit;
6070 cachestats.opMiss += itecache.cacheMiss;
6071 }
6072 if (countcache != null) {
6073 System.out.println("Count cache: "+countcache);
6074 cachestats.opHit += countcache.cacheHit;
6075 cachestats.opMiss += countcache.cacheMiss;
6076 }
6077 if (misccache != null) {
6078 System.out.println("Misc cache: "+misccache);
6079 cachestats.opHit += misccache.cacheHit;
6080 cachestats.opMiss += misccache.cacheMiss;
6081 }
6082 return cachestats;
6083 }
6084 }