2 f: 3 nodes 1 leaves 1 minterms
5 g: 3 nodes 1 leaves 3 minterms
9 f and g are not complementary
10 f is less than or equal to g
11 g: 2 nodes 1 leaves 2 minterms
14 h: 2 nodes 1 leaves 2 minterms
18 h: 3 nodes 1 leaves 3 minterms
23 r: 6 nodes 3 leaves 3 minterms
28 s: 4 nodes 2 leaves 1 minterms
31 s: 1 nodes 1 leaves 4 minterms
34 p is less than or equal to r
35 r: 4 nodes 2 leaves 3 minterms
40 f: 7 nodes 4 leaves 4 minterms
46 l: 7 nodes 4 leaves 4 minterms
52 r: 7 nodes 4 leaves 4 minterms
58 e: 1 nodes 1 leaves 4 minterms
71 f: 7 nodes 1 leaves 7 minterms
77 Irredundant cover of f:
81 Number of minterms (arbitrary precision): 7
82 Number of minterms (extended precision): 7.000000e+00
83 Two-literal clauses of f:
109 { node [shape = plaintext];
110 edge [style = invis];
111 "CONST NODES" [style = invis];
112 " x0 " -> " x1 " -> " x2 " -> " x3 " -> "CONST NODES";
114 { rank = same; node [shape = box]; edge [style = invis];
115 " v0 " -> " v1 " -> " v2 " -> " v3 "; }
116 { rank = same; " x0 ";
122 { rank = same; " x1 ";
127 { rank = same; " x2 ";
131 { rank = same; " x3 ";
134 { rank = same; "CONST NODES";
135 { node [shape = box]; "0x34";
138 " v0 " -> "0x3a" [style = solid];
139 " v1 " -> "0x3e" [style = solid];
140 " v2 " -> "0x7b" [style = solid];
141 " v3 " -> "0x7e" [style = solid];
143 "0x3e" -> "0x34" [style = dashed];
145 "0x7b" -> "0x6b" [style = dashed];
147 "0x7e" -> "0x34" [style = dashed];
149 "0x3a" -> "0x34" [style = dotted];
151 "0x7a" -> "0x34" [style = dashed];
153 "0x7d" -> "0x6c" [style = dashed];
155 "0x3b" -> "0x34" [style = dotted];
157 "0x6b" -> "0x34" [style = dotted];
159 "0x7c" -> "0x34" [style = dashed];
161 "0x6c" -> "0x34" [style = dotted];
162 "0x34" [label = "1"];
165 f: 10 nodes 1 leaves 50 minterms
180 f1: 5 nodes 1 leaves 36 minterms
186 f1 is less than or equal to f
187 g: 6 nodes 1 leaves 62 minterms
194 h: 8 nodes 1 leaves 51 minterms
210 p[0]: 3 nodes 1 leaves 64 minterms
214 p[1]: 5 nodes 1 leaves 64 minterms
220 p[2]: 7 nodes 1 leaves 64 minterms
228 p[3]: 8 nodes 1 leaves 64 minterms
238 { node [shape = plaintext];
239 edge [style = invis];
240 "CONST NODES" [style = invis];
241 " a2 " -> " b2 " -> " a1 " -> " b1 " -> " a0 " -> " b0 " -> " c0 " -> "CONST NODES";
243 { rank = same; node [shape = box]; edge [style = invis];
244 " s0 " -> " s1 " -> " s2 " -> " c3 "; }
245 { rank = same; " a2 ";
249 { rank = same; " b2 ";
252 { rank = same; " a1 ";
256 { rank = same; " b1 ";
259 { rank = same; " a0 ";
263 { rank = same; " b0 ";
266 { rank = same; " c0 ";
269 { rank = same; "CONST NODES";
270 { node [shape = box]; "0x34";
273 " s0 " -> "0xb0" [style = solid];
274 " s1 " -> "0xb2" [style = solid];
275 " s2 " -> "0xb4" [style = solid];
276 " c3 " -> "0xb5" [style = solid];
278 "0xb5" -> "0xb3" [style = dashed];
280 "0xb4" -> "0xb3" [style = dotted];
282 "0x3b" -> "0x34" [style = dotted];
284 "0xb2" -> "0xb1" [style = dotted];
286 "0xb3" -> "0xb1" [style = dashed];
288 "0x6c" -> "0x34" [style = dotted];
290 "0xb1" -> "0xaf" [style = dashed];
292 "0xb0" -> "0xaf" [style = dotted];
294 "0x8b" -> "0x34" [style = dotted];
296 "0xaf" -> "0x34" [style = dotted];
297 "0x34" [label = "1"];
299 z[0]: 4 nodes 2 minterms
303 z[1]: 10 nodes 4 minterms
309 z[2]: 16 nodes 6 minterms
317 z[3]: 10 nodes 4 minterms
347 { node [shape = plaintext];
348 edge [style = invis];
349 "CONST NODES" [style = invis];
350 " a2+ " -> " a2- " -> " b2+ " -> " a1+ " -> " a1- " -> " b1+ " -> " b1- " -> " a0+ " -> " a0- " -> " b0+ " -> " b0- " -> " c0+ " -> " c0- " -> "CONST NODES";
352 { rank = same; node [shape = box]; edge [style = invis];
353 " s0 " -> " s1 " -> " s2 " -> " c3 "; }
354 { rank = same; " a2+ ";
358 { rank = same; " a2- ";
362 { rank = same; " b2+ ";
365 { rank = same; " a1+ ";
370 { rank = same; " a1- ";
374 { rank = same; " b1+ ";
377 { rank = same; " b1- ";
380 { rank = same; " a0+ ";
385 { rank = same; " a0- ";
389 { rank = same; " b0+ ";
392 { rank = same; " b0- ";
395 { rank = same; " c0+ ";
398 { rank = same; " c0- ";
401 { rank = same; "CONST NODES";
402 { node [shape = box]; "0x35";
406 " s0 " -> "0x42" [style = solid];
407 " s1 " -> "0x57" [style = solid];
408 " s2 " -> "0x6e" [style = solid];
409 " c3 " -> "0x77" [style = solid];
411 "0x6e" -> "0x6a" [style = dashed];
413 "0x77" -> "0x75" [style = dashed];
415 "0x6a" -> "0x35" [style = dashed];
417 "0x75" -> "0x35" [style = dashed];
419 "0x71" -> "0x35" [style = dashed];
421 "0x57" -> "0x55" [style = dashed];
423 "0x65" -> "0x63" [style = dashed];
425 "0x5e" -> "0x55" [style = dashed];
427 "0x55" -> "0x35" [style = dashed];
429 "0x63" -> "0x35" [style = dashed];
431 "0x5f" -> "0x35" [style = dashed];
433 "0x5a" -> "0x35" [style = dashed];
435 "0x50" -> "0x4e" [style = dashed];
437 "0x42" -> "0x40" [style = dashed];
439 "0x49" -> "0x40" [style = dashed];
441 "0x4e" -> "0x35" [style = dashed];
443 "0x40" -> "0x35" [style = dashed];
445 "0x4a" -> "0x35" [style = dashed];
447 "0x45" -> "0x35" [style = dashed];
449 "0x39" -> "0x35" [style = dashed];
451 "0x38" -> "0x35" [style = dashed];
452 "0x35" [label = "0"];
453 "0x34" [label = "1"];
456 f: 5 nodes 1 leaves 3 minterms
460 g: 5 nodes 1 leaves 3 minterms
464 f and h are identical
465 **** CUDD modifiable parameters ****
466 Hard limit for cache size: 7645866
467 Cache hit threshold for resizing: 30%
468 Garbage collection enabled: yes
469 Limit for fast unique table growth: 4587520
470 Maximum number of variables sifted per reordering: 1000
471 Maximum number of variable swaps per reordering: 2000000
472 Maximum growth while sifting a variable: 1.2
473 Dynamic reordering of BDDs enabled: no
474 Default BDD reordering method: 4
475 Dynamic reordering of ZDDs enabled: no
476 Default ZDD reordering method: 4
477 Realignment of ZDDs to BDDs enabled: no
478 Realignment of BDDs to ZDDs enabled: no
479 Dead nodes counted in triggering reordering: no
480 Group checking criterion: 7
481 Recombination threshold: 0
482 Symmetry violation threshold: 0
483 Arc violation threshold: 0
484 GA population size: 0
485 Number of crossovers for GA: 0
486 Next reordering threshold: 4004
487 **** CUDD non-modifiable parameters ****
488 Memory in use: 8436016
489 Peak number of nodes: 1022
490 Peak number of live nodes: 35
491 Number of BDD variables: 14
492 Number of ZDD variables: 14
493 Number of cache entries: 262144
494 Number of cache look-ups: 396
495 Number of cache hits: 91
496 Number of cache insertions: 303
497 Number of cache collisions: 0
498 Number of cache deletions: 162
499 Cache used slots = 0.11% (expected 0.05%)
500 Soft limit for cache size: 29696
501 Number of buckets in unique table: 7424
502 Used buckets in unique table: 1.58% (expected 1.69%)
504 Unique links: 6 (0.0126316 per lookup)
505 Number of BDD and ADD nodes: 78
506 Number of ZDD nodes: 49
507 Number of dead BDD and ADD nodes: 60
508 Number of dead ZDD nodes: 35
509 Total number of nodes allocated: 247
510 Total number of nodes reclaimed: 85
511 Number of recursive calls: 1265
512 Garbage collections so far: 1
513 Time for garbage collection: 0.00 sec
514 Reorderings so far: 0
515 Time for reordering: 0.00 sec
516 Node swaps in reordering: 0