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