1Entering testBdd
2f: 3 nodes 1 leaves 1 minterms
311  1
4
5g: 3 nodes 1 leaves 3 minterms
60-  1
711  1
8
9f and g are not complementary
10f is less than or equal to g
11g: 2 nodes 1 leaves 2 minterms
121-  1
13
14h: 2 nodes 1 leaves 2 minterms
15-1  1
16
17x + h has 3 nodes
18h: 3 nodes 1 leaves 3 minterms
1901  1
201-  1
21
22Entering testAdd
23r: 6 nodes 3 leaves 3 minterms
2401  1
2510  1
2611  2
27
28s: 4 nodes 2 leaves 1 minterms
2911  3
30
31s: 1 nodes 1 leaves 4 minterms
32--  inf
33
34p is less than or equal to r
35r: 4 nodes 2 leaves 3 minterms
3601  1
371-  1
38
39Entering testAdd2
40f: 7 nodes 4 leaves 4 minterms
4100  0.1
4201  0.2
4310  0.3
4411  0.4
45
46l: 7 nodes 4 leaves 4 minterms
4700 -2.30259
4801 -1.60944
4910 -1.20397
5011 -0.916291
51
52r: 7 nodes 4 leaves 4 minterms
5300 -0.230259
5401 -0.321888
5510 -0.361192
5611 -0.366516
57
58e: 1 nodes 1 leaves 4 minterms
59--  1.84644
60
61Entering testZdd
62s: 3 nodes 3 minterms
631- 1
6401 1
65
66v is less than s
67s: 1 nodes 1 minterms
6801 1
69
70Entering testBdd2
71f: 7 nodes 1 leaves 7 minterms
7201-1  1
73101-  1
741101  1
75111-  1
76
77Irredundant cover of f:
781-1- 1
79-1-1 1
80
81Number of minterms (arbitrary precision): 7
82Number of minterms (extended precision):  7.000000e+00
83Two-literal clauses of f:
84 x2 |  x3
85 x1 |  x2
86 x0 |  x3
87 x0 |  x1
88
89vect[0]
901--- 1
91
92vect[1]
930--- 1
94-1-- 1
95
96vect[2]
9710-- 1
98--1- 1
99
100vect[3]
1010--- 1
102-10- 1
103---1 1
104
105digraph "DD" {
106size = "7.5,10"
107center = true;
108edge [dir = none];
109{ node [shape = plaintext];
110  edge [style = invis];
111  "CONST NODES" [style = invis];
112" x0 " -> " x1 " -> " x2 " -> " x3 " -> "CONST NODES";
113}
114{ rank = same; node [shape = box]; edge [style = invis];
115"  v0  " -> "  v1  " -> "  v2  " -> "  v3  "; }
116{ rank = same; " x0 ";
117"0x1d";
118"0x5d";
119"0x5a";
120"0x19";
121}
122{ rank = same; " x1 ";
123"0x59";
124"0x5c";
125"0x1a";
126}
127{ rank = same; " x2 ";
128"0x4a";
129"0x5b";
130}
131{ rank = same; " x3 ";
132"0x4b";
133}
134{ rank = same; "CONST NODES";
135{ node [shape = box]; "0x13";
136}
137}
138"  v0  " -> "0x19" [style = solid];
139"  v1  " -> "0x1d" [style = solid];
140"  v2  " -> "0x5a" [style = solid];
141"  v3  " -> "0x5d" [style = solid];
142"0x1d" -> "0x1a";
143"0x1d" -> "0x13" [style = dashed];
144"0x5d" -> "0x5c";
145"0x5d" -> "0x13" [style = dashed];
146"0x5a" -> "0x59";
147"0x5a" -> "0x4a" [style = dashed];
148"0x19" -> "0x13";
149"0x19" -> "0x13" [style = dotted];
150"0x59" -> "0x4a";
151"0x59" -> "0x13" [style = dashed];
152"0x5c" -> "0x5b";
153"0x5c" -> "0x4b" [style = dashed];
154"0x1a" -> "0x13";
155"0x1a" -> "0x13" [style = dotted];
156"0x4a" -> "0x13";
157"0x4a" -> "0x13" [style = dotted];
158"0x5b" -> "0x4b";
159"0x5b" -> "0x13" [style = dashed];
160"0x4b" -> "0x13";
161"0x4b" -> "0x13" [style = dotted];
162"0x13" [label = "1"];
163}
164Entering testBdd3
165f: 10 nodes 1 leaves 50 minterms
1660-0-0-  1
1670-0-10  1
1680-100-  1
1690-1010  1
1700-11--  1
17110-00-  1
17210-010  1
17310-1--  1
17411000-  1
175110010  1
1761101--  1
1771110-1  1
178111101  1
179
180f1: 5 nodes 1 leaves 36 minterms
1810---0-  1
1820---10  1
18310--0-  1
18410--10  1
185
186f1 is less than or equal to f
187g: 6 nodes 1 leaves 62 minterms
1880-----  1
18910----  1
190110---  1
1911110--  1
19211110-  1
193
194h: 8 nodes 1 leaves 51 minterms
1950-0-0-  1
1960-0-10  1
1970-100-  1
1980-1010  1
1990-11--  1
20010-00-  1
20110-010  1
20210-1--  1
20311000-  1
204110010  1
2051101--  1
206111--1  1
207
208g * h == f
209Entering testZdd2
210p[0]: 3 nodes 1 leaves 64 minterms
211----0-0  1
212----1-1  1
213
214p[1]: 5 nodes 1 leaves 64 minterms
215--0-0-0  1
216--0-10-  1
217--1-0-1  1
218--1-11-  1
219
220p[2]: 7 nodes 1 leaves 64 minterms
2210-0-0-0  1
2220-0-10-  1
2230-10---  1
2241-0-0-1  1
2251-0-11-  1
2261-11---  1
227
228p[3]: 8 nodes 1 leaves 64 minterms
2290-0-0-1  1
2300-0-11-  1
2310-11---  1
23211-----  1
233
234digraph "DD" {
235size = "7.5,10"
236center = true;
237edge [dir = none];
238{ node [shape = plaintext];
239  edge [style = invis];
240  "CONST NODES" [style = invis];
241" a2 " -> " b2 " -> " a1 " -> " b1 " -> " a0 " -> " b0 " -> " c0 " -> "CONST NODES";
242}
243{ rank = same; node [shape = box]; edge [style = invis];
244"  s0  " -> "  s1  " -> "  s2  " -> "  c3  "; }
245{ rank = same; " a2 ";
246"0x494";
247"0x493";
248}
249{ rank = same; " b2 ";
250"0x41a";
251}
252{ rank = same; " a1 ";
253"0x491";
254"0x492";
255}
256{ rank = same; " b1 ";
257"0x44b";
258}
259{ rank = same; " a0 ";
260"0x490";
261"0x48f";
262}
263{ rank = same; " b0 ";
264"0x46a";
265}
266{ rank = same; " c0 ";
267"0x48e";
268}
269{ rank = same; "CONST NODES";
270{ node [shape = box]; "0x413";
271}
272}
273"  s0  " -> "0x48f" [style = solid];
274"  s1  " -> "0x491" [style = solid];
275"  s2  " -> "0x493" [style = solid];
276"  c3  " -> "0x494" [style = solid];
277"0x494" -> "0x41a";
278"0x494" -> "0x492" [style = dashed];
279"0x493" -> "0x492";
280"0x493" -> "0x492" [style = dotted];
281"0x41a" -> "0x413";
282"0x41a" -> "0x413" [style = dotted];
283"0x491" -> "0x490";
284"0x491" -> "0x490" [style = dotted];
285"0x492" -> "0x44b";
286"0x492" -> "0x490" [style = dashed];
287"0x44b" -> "0x413";
288"0x44b" -> "0x413" [style = dotted];
289"0x490" -> "0x46a";
290"0x490" -> "0x48e" [style = dashed];
291"0x48f" -> "0x48e";
292"0x48f" -> "0x48e" [style = dotted];
293"0x46a" -> "0x413";
294"0x46a" -> "0x413" [style = dotted];
295"0x48e" -> "0x413";
296"0x48e" -> "0x413" [style = dotted];
297"0x413" [label = "1"];
298}
299z[0]: 4 nodes 2 minterms
30000000000100010 1
30100000000010001 1
302
303z[1]: 10 nodes 4 minterms
30400001000101000 1
30500001000010010 1
30600000100100100 1
30700000100010001 1
308
309z[2]: 16 nodes 6 minterms
31010001010000000 1
31110000100101000 1
31210000100010010 1
31301001001000000 1
31401000100100100 1
31501000100010001 1
316
317z[3]: 10 nodes 4 minterms
31810100000000000 1
31901001010000000 1
32001000100101000 1
32101000100010010 1
322
323z[0]
324----1-1 1
325----0-0 1
326z[0]
327----0-0 1
328----1-1 1
329z[1]
330--1-11- 1
331--1-0-1 1
332--0-10- 1
333--0-0-0 1
334z[1]
335--0-0-0 1
336--0-10- 1
337--1-0-1 1
338--1-11- 1
339z[2]
3401-11--- 1
3411-0-11- 1
3421-0-0-1 1
3430-10--- 1
3440-0-10- 1
3450-0-0-0 1
346z[2]
3470-0-0-0 1
3480-0-10- 1
3490-10--- 1
3501-0-0-1 1
3511-0-11- 1
3521-11--- 1
353z[3]
35411----- 1
3550-11--- 1
3560-0-11- 1
3570-0-0-1 1
358z[3]
3590-0-0-1 1
3600-0-11- 1
3610-11--- 1
36211----- 1
363digraph "ZDD" {
364size = "7.5,10"
365center = true;
366edge [dir = none];
367{ node [shape = plaintext];
368  edge [style = invis];
369  "CONST NODES" [style = invis];
370" a2+ " -> " a2- " -> " b2+ " -> " a1+ " -> " a1- " -> " b1+ " -> " b1- " -> " a0+ " -> " a0- " -> " b0+ " -> " b0- " -> " c0+ " -> " c0- " -> "CONST NODES";
371}
372{ rank = same; node [shape = box]; edge [style = invis];
373"  s0  " -> "  s1  " -> "  s2  " -> "  c3  "; }
374{ rank = same; " a2+ ";
375"0x56";
376"0x4d";
377}
378{ rank = same; " a2- ";
379"0x54";
380"0x49";
381}
382{ rank = same; " b2+ ";
383"0x50";
384}
385{ rank = same; " a1+ ";
386"0x44";
387"0x36";
388"0x3d";
389}
390{ rank = same; " a1- ";
391"0x34";
392"0x42";
393}
394{ rank = same; " b1+ ";
395"0x3e";
396}
397{ rank = same; " b1- ";
398"0x39";
399}
400{ rank = same; " a0+ ";
401"0x2f";
402"0x21";
403"0x28";
404}
405{ rank = same; " a0- ";
406"0x2d";
407"0x1f";
408}
409{ rank = same; " b0+ ";
410"0x29";
411}
412{ rank = same; " b0- ";
413"0x24";
414}
415{ rank = same; " c0+ ";
416"0x18";
417}
418{ rank = same; " c0- ";
419"0x17";
420}
421{ rank = same; "CONST NODES";
422{ node [shape = box]; "0x14";
423"0x13";
424}
425}
426"  s0  " -> "0x21" [style = solid];
427"  s1  " -> "0x36" [style = solid];
428"  s2  " -> "0x4d" [style = solid];
429"  c3  " -> "0x56" [style = solid];
430"0x56" -> "0x50";
431"0x56" -> "0x54" [style = dashed];
432"0x4d" -> "0x44";
433"0x4d" -> "0x49" [style = dashed];
434"0x54" -> "0x44";
435"0x54" -> "0x14" [style = dashed];
436"0x49" -> "0x3d";
437"0x49" -> "0x14" [style = dashed];
438"0x50" -> "0x13";
439"0x50" -> "0x14" [style = dashed];
440"0x44" -> "0x3e";
441"0x44" -> "0x42" [style = dashed];
442"0x36" -> "0x2f";
443"0x36" -> "0x34" [style = dashed];
444"0x3d" -> "0x39";
445"0x3d" -> "0x34" [style = dashed];
446"0x34" -> "0x28";
447"0x34" -> "0x14" [style = dashed];
448"0x42" -> "0x2f";
449"0x42" -> "0x14" [style = dashed];
450"0x3e" -> "0x13";
451"0x3e" -> "0x14" [style = dashed];
452"0x39" -> "0x13";
453"0x39" -> "0x14" [style = dashed];
454"0x2f" -> "0x29";
455"0x2f" -> "0x2d" [style = dashed];
456"0x21" -> "0x18";
457"0x21" -> "0x1f" [style = dashed];
458"0x28" -> "0x24";
459"0x28" -> "0x1f" [style = dashed];
460"0x2d" -> "0x18";
461"0x2d" -> "0x14" [style = dashed];
462"0x1f" -> "0x17";
463"0x1f" -> "0x14" [style = dashed];
464"0x29" -> "0x13";
465"0x29" -> "0x14" [style = dashed];
466"0x24" -> "0x13";
467"0x24" -> "0x14" [style = dashed];
468"0x18" -> "0x13";
469"0x18" -> "0x14" [style = dashed];
470"0x17" -> "0x13";
471"0x17" -> "0x14" [style = dashed];
472"0x14" [label = "0"];
473"0x13" [label = "1"];
474}
475Entering testBdd4
476f: 5 nodes 1 leaves 3 minterms
477000-----------  1
47811------------  1
479
480g: 5 nodes 1 leaves 3 minterms
481000  1
48211-  1
483
484f and h are identical
485Entering testBdd5
486digraph "DD" {
487size = "7.5,10"
488center = true;
489edge [dir = none];
490{ node [shape = plaintext];
491  edge [style = invis];
492  "CONST NODES" [style = invis];
493" a " -> " b " -> " c " -> " d " -> "CONST NODES";
494}
495{ rank = same; node [shape = box]; edge [style = invis];
496"  lb  " -> "  ub  " -> "  f  " -> "  primes  " -> "  lprime  "; }
497{ rank = same; " a ";
498"0x487";
499}
500{ rank = same; " b ";
501"0x484";
502"0x486";
503"0x483";
504"0x488";
505}
506{ rank = same; " c ";
507"0x481";
508"0x43b";
509}
510{ rank = same; " d ";
511"0x44b";
512}
513{ rank = same; "CONST NODES";
514{ node [shape = box]; "0x413";
515}
516}
517"  lb  " -> "0x488" [style = dotted];
518"  ub  " -> "0x44b" [style = solid];
519"  f  " -> "0x487" [style = solid];
520"  primes  " -> "0x483" [style = solid];
521"  lprime  " -> "0x483" [style = solid];
522"0x487" -> "0x484";
523"0x487" -> "0x486" [style = dashed];
524"0x484" -> "0x44b";
525"0x484" -> "0x481" [style = dotted];
526"0x486" -> "0x43b";
527"0x486" -> "0x413" [style = dotted];
528"0x483" -> "0x44b";
529"0x483" -> "0x413" [style = dotted];
530"0x488" -> "0x481";
531"0x488" -> "0x413" [style = dashed];
532"0x481" -> "0x413";
533"0x481" -> "0x44b" [style = dotted];
534"0x43b" -> "0x44b";
535"0x43b" -> "0x413" [style = dashed];
536"0x44b" -> "0x413";
537"0x44b" -> "0x413" [style = dotted];
538"0x413" [label = "1"];
539}
540primes(1): 3 nodes 1 leaves 4 minterms
541-1-1----------  1
542
543primes(2): is the zero DD
544primes(3): 4 nodes 1 leaves 2 minterms
5451-01----------  1
546
547primes(4): 6 nodes 1 leaves 5 minterms
548-1-1---------- 1
549010----------- 1
550
551primes(5): 4 nodes 1 leaves 2 minterms
55201-1----------  1
553
554l1: 7 nodes 1 leaves 3 minterms
5550111----------  1
556111-----------  1
557
558u1: 4 nodes 1 leaves 8 minterms
559000-----------  1
560011-----------  1
5611-1-----------  1
562
563interpolant1: 4 nodes 1 leaves 6 minterms
564011-----------  1
5651-1-----------  1
566
567l2: 7 nodes 1 leaves 5 minterms
568001-----------  1
5690110----------  1
570101-----------  1
571
572u2: 5 nodes 1 leaves 8 minterms
573-000----------  1
574-01-----------  1
575-110----------  1
576
577interpolant2: 5 nodes 1 leaves 6 minterms
578-01-----------  1
579-110----------  1
580
581l3: 4 nodes 1 leaves 2 minterms
58200-1----------  1
583
584u3: 3 nodes 1 leaves 4 minterms
585-0-1----------  1
586
587interpolant3: 3 nodes 1 leaves 4 minterms
588-0-1----------  1
589
590Entering testErrorHandling
591Oops! Caught: empty DD.
592Caught: Invalid argument.
593f = var[1] | (var[2] & var[3])
594var[0] | var[1] is not a cube
595Cudd_Cofactor: Invalid restriction 2
596Caught: Invalid argument.
597f : 511 nodes 1 leaves 115422332637413376 minterms
598g : 511 nodes 1 leaves 115422332637413376 minterms
599h Caught: empty DD.
600f : 88 nodes 1 leaves 226007109 minterms
601g : 91 nodes 1 leaves 3143500301 minterms
602h : 142 nodes 1 leaves 2917493192 minterms
603Caught: Maximum memory exceeded.
604Caught: Timeout expired.  Lag = 29 ms.
605**** CUDD modifiable parameters ****
606Hard limit for cache size: 2796202
607Cache hit threshold for resizing: 30%
608Garbage collection enabled: yes
609Limit for fast unique table growth: 1677721
610Maximum number of variables sifted per reordering: 1000
611Maximum number of variable swaps per reordering: 2000000
612Maximum growth while sifting a variable: 1.2
613Dynamic reordering of BDDs enabled: no
614Default BDD reordering method: 4
615Dynamic reordering of ZDDs enabled: no
616Default ZDD reordering method: 4
617Realignment of ZDDs to BDDs enabled: no
618Realignment of BDDs to ZDDs enabled: no
619Dead nodes counted in triggering reordering: no
620Group checking criterion: 7
621Recombination threshold: 0
622Symmetry violation threshold: 0
623Arc violation threshold: 0
624GA population size: 0
625Number of crossovers for GA: 0
626Next reordering threshold: 4004
627**** CUDD non-modifiable parameters ****
628Memory in use: 146651968
629Peak number of nodes: 2044
630Peak number of live nodes: 2030
631Number of BDD variables: 60
632Number of ZDD variables: 14
633Number of cache entries: 524288
634Number of cache look-ups: 5326
635Number of cache hits: 1226
636Number of cache insertions: 4217
637Number of cache collisions: 16
638Number of cache deletions: 2300
639Cache used slots = 0.39% (expected 0.39%)
640Soft limit for cache size: 76800
641Number of buckets in unique table: 19200
642Used buckets in unique table: 9.11% (expected 8.95%)
643Number of BDD and ADD nodes: 3789
644Number of ZDD nodes: 14
645Number of dead BDD and ADD nodes: 3725
646Number of dead ZDD nodes: 0
647Total number of nodes allocated: 6011
648Total number of nodes reclaimed: 154
649Garbage collections so far: 3
650Time for garbage collection: 0.00 sec
651Reorderings so far: 0
652Time for reordering: 0.00 sec
653