cudd/cplusplus/test.out

Entering testBdd
f: 3 nodes 1 leaves 1 minterms
11  1

g: 3 nodes 1 leaves 3 minterms
0-  1
11  1

f and g are not complementary
f is less than or equal to g
g: 2 nodes 1 leaves 2 minterms
1-  1

h: 2 nodes 1 leaves 2 minterms
-1  1

x + h has 3 nodes
h: 3 nodes 1 leaves 3 minterms
01  1
1-  1

Entering testAdd
r: 6 nodes 3 leaves 3 minterms
01  1
10  1
11  2

s: 4 nodes 2 leaves 1 minterms
11  3

s: 1 nodes 1 leaves 4 minterms
--  inf

p is less than or equal to r
r: 4 nodes 2 leaves 3 minterms
01  1
1-  1

Entering testAdd2
f: 7 nodes 4 leaves 4 minterms
00  0.1
01  0.2
10  0.3
11  0.4

l: 7 nodes 4 leaves 4 minterms
00 -2.30259
01 -1.60944
10 -1.20397
11 -0.916291

r: 7 nodes 4 leaves 4 minterms
00 -0.230259
01 -0.321888
10 -0.361192
11 -0.366516

e: 1 nodes 1 leaves 4 minterms
--  1.84644

Entering testZdd
s: 3 nodes 3 minterms
1- 1
01 1

v is less than s
s: 1 nodes 1 minterms
01 1

Entering testBdd2
f: 7 nodes 1 leaves 7 minterms
01-1  1
101-  1
1101  1
111-  1

Irredundant cover of f:
1-1- 1
-1-1 1

Number of minterms (arbitrary precision): 7
Number of minterms (extended precision):  7.000000e+00
Two-literal clauses of f:
 x2 |  x3
 x1 |  x2
 x0 |  x3
 x0 |  x1

vect[0]
1--- 1

vect[1]
0--- 1
-1-- 1

vect[2]
10-- 1
--1- 1

vect[3]
0--- 1
-10- 1
---1 1

digraph "DD" {
size = "7.5,10"
center = true;
edge [dir = none];
{ node [shape = plaintext];
  edge [style = invis];
  "CONST NODES" [style = invis];
" x0 " -> " x1 " -> " x2 " -> " x3 " -> "CONST NODES"; 
}
{ rank = same; node [shape = box]; edge [style = invis];
"  v0  " -> "  v1  " -> "  v2  " -> "  v3  "; }
{ rank = same; " x0 ";
"0x1d";
"0x5d";
"0x5a";
"0x19";
}
{ rank = same; " x1 ";
"0x59";
"0x5c";
"0x1a";
}
{ rank = same; " x2 ";
"0x4a";
"0x5b";
}
{ rank = same; " x3 ";
"0x4b";
}
{ rank = same; "CONST NODES";
{ node [shape = box]; "0x13";
}
}
"  v0  " -> "0x19" [style = solid];
"  v1  " -> "0x1d" [style = solid];
"  v2  " -> "0x5a" [style = solid];
"  v3  " -> "0x5d" [style = solid];
"0x1d" -> "0x1a";
"0x1d" -> "0x13" [style = dashed];
"0x5d" -> "0x5c";
"0x5d" -> "0x13" [style = dashed];
"0x5a" -> "0x59";
"0x5a" -> "0x4a" [style = dashed];
"0x19" -> "0x13";
"0x19" -> "0x13" [style = dotted];
"0x59" -> "0x4a";
"0x59" -> "0x13" [style = dashed];
"0x5c" -> "0x5b";
"0x5c" -> "0x4b" [style = dashed];
"0x1a" -> "0x13";
"0x1a" -> "0x13" [style = dotted];
"0x4a" -> "0x13";
"0x4a" -> "0x13" [style = dotted];
"0x5b" -> "0x4b";
"0x5b" -> "0x13" [style = dashed];
"0x4b" -> "0x13";
"0x4b" -> "0x13" [style = dotted];
"0x13" [label = "1"];
}
Entering testBdd3
f: 10 nodes 1 leaves 50 minterms
0-0-0-  1
0-0-10  1
0-100-  1
0-1010  1
0-11--  1
10-00-  1
10-010  1
10-1--  1
11000-  1
110010  1
1101--  1
1110-1  1
111101  1

f1: 5 nodes 1 leaves 36 minterms
0---0-  1
0---10  1
10--0-  1
10--10  1

f1 is less than or equal to f
g: 6 nodes 1 leaves 62 minterms
0-----  1
10----  1
110---  1
1110--  1
11110-  1

h: 8 nodes 1 leaves 51 minterms
0-0-0-  1
0-0-10  1
0-100-  1
0-1010  1
0-11--  1
10-00-  1
10-010  1
10-1--  1
11000-  1
110010  1
1101--  1
111--1  1

g * h == f
Entering testZdd2
p[0]: 3 nodes 1 leaves 64 minterms
----0-0  1
----1-1  1

p[1]: 5 nodes 1 leaves 64 minterms
--0-0-0  1
--0-10-  1
--1-0-1  1
--1-11-  1

p[2]: 7 nodes 1 leaves 64 minterms
0-0-0-0  1
0-0-10-  1
0-10---  1
1-0-0-1  1
1-0-11-  1
1-11---  1

p[3]: 8 nodes 1 leaves 64 minterms
0-0-0-1  1
0-0-11-  1
0-11---  1
11-----  1

digraph "DD" {
size = "7.5,10"
center = true;
edge [dir = none];
{ node [shape = plaintext];
  edge [style = invis];
  "CONST NODES" [style = invis];
" a2 " -> " b2 " -> " a1 " -> " b1 " -> " a0 " -> " b0 " -> " c0 " -> "CONST NODES"; 
}
{ rank = same; node [shape = box]; edge [style = invis];
"  s0  " -> "  s1  " -> "  s2  " -> "  c3  "; }
{ rank = same; " a2 ";
"0x494";
"0x493";
}
{ rank = same; " b2 ";
"0x41a";
}
{ rank = same; " a1 ";
"0x491";
"0x492";
}
{ rank = same; " b1 ";
"0x44b";
}
{ rank = same; " a0 ";
"0x490";
"0x48f";
}
{ rank = same; " b0 ";
"0x46a";
}
{ rank = same; " c0 ";
"0x48e";
}
{ rank = same; "CONST NODES";
{ node [shape = box]; "0x413";
}
}
"  s0  " -> "0x48f" [style = solid];
"  s1  " -> "0x491" [style = solid];
"  s2  " -> "0x493" [style = solid];
"  c3  " -> "0x494" [style = solid];
"0x494" -> "0x41a";
"0x494" -> "0x492" [style = dashed];
"0x493" -> "0x492";
"0x493" -> "0x492" [style = dotted];
"0x41a" -> "0x413";
"0x41a" -> "0x413" [style = dotted];
"0x491" -> "0x490";
"0x491" -> "0x490" [style = dotted];
"0x492" -> "0x44b";
"0x492" -> "0x490" [style = dashed];
"0x44b" -> "0x413";
"0x44b" -> "0x413" [style = dotted];
"0x490" -> "0x46a";
"0x490" -> "0x48e" [style = dashed];
"0x48f" -> "0x48e";
"0x48f" -> "0x48e" [style = dotted];
"0x46a" -> "0x413";
"0x46a" -> "0x413" [style = dotted];
"0x48e" -> "0x413";
"0x48e" -> "0x413" [style = dotted];
"0x413" [label = "1"];
}
z[0]: 4 nodes 2 minterms
00000000100010 1
00000000010001 1

z[1]: 10 nodes 4 minterms
00001000101000 1
00001000010010 1
00000100100100 1
00000100010001 1

z[2]: 16 nodes 6 minterms
10001010000000 1
10000100101000 1
10000100010010 1
01001001000000 1
01000100100100 1
01000100010001 1

z[3]: 10 nodes 4 minterms
10100000000000 1
01001010000000 1
01000100101000 1
01000100010010 1

z[0]
----1-1 1
----0-0 1
z[0]
----0-0 1
----1-1 1
z[1]
--1-11- 1
--1-0-1 1
--0-10- 1
--0-0-0 1
z[1]
--0-0-0 1
--0-10- 1
--1-0-1 1
--1-11- 1
z[2]
1-11--- 1
1-0-11- 1
1-0-0-1 1
0-10--- 1
0-0-10- 1
0-0-0-0 1
z[2]
0-0-0-0 1
0-0-10- 1
0-10--- 1
1-0-0-1 1
1-0-11- 1
1-11--- 1
z[3]
11----- 1
0-11--- 1
0-0-11- 1
0-0-0-1 1
z[3]
0-0-0-1 1
0-0-11- 1
0-11--- 1
11----- 1
digraph "ZDD" {
size = "7.5,10"
center = true;
edge [dir = none];
{ node [shape = plaintext];
  edge [style = invis];
  "CONST NODES" [style = invis];
" a2+ " -> " a2- " -> " b2+ " -> " a1+ " -> " a1- " -> " b1+ " -> " b1- " -> " a0+ " -> " a0- " -> " b0+ " -> " b0- " -> " c0+ " -> " c0- " -> "CONST NODES"; 
}
{ rank = same; node [shape = box]; edge [style = invis];
"  s0  " -> "  s1  " -> "  s2  " -> "  c3  "; }
{ rank = same; " a2+ ";
"0x56";
"0x4d";
}
{ rank = same; " a2- ";
"0x54";
"0x49";
}
{ rank = same; " b2+ ";
"0x50";
}
{ rank = same; " a1+ ";
"0x44";
"0x36";
"0x3d";
}
{ rank = same; " a1- ";
"0x34";
"0x42";
}
{ rank = same; " b1+ ";
"0x3e";
}
{ rank = same; " b1- ";
"0x39";
}
{ rank = same; " a0+ ";
"0x2f";
"0x21";
"0x28";
}
{ rank = same; " a0- ";
"0x2d";
"0x1f";
}
{ rank = same; " b0+ ";
"0x29";
}
{ rank = same; " b0- ";
"0x24";
}
{ rank = same; " c0+ ";
"0x18";
}
{ rank = same; " c0- ";
"0x17";
}
{ rank = same; "CONST NODES";
{ node [shape = box]; "0x14";
"0x13";
}
}
"  s0  " -> "0x21" [style = solid];
"  s1  " -> "0x36" [style = solid];
"  s2  " -> "0x4d" [style = solid];
"  c3  " -> "0x56" [style = solid];
"0x56" -> "0x50";
"0x56" -> "0x54" [style = dashed];
"0x4d" -> "0x44";
"0x4d" -> "0x49" [style = dashed];
"0x54" -> "0x44";
"0x54" -> "0x14" [style = dashed];
"0x49" -> "0x3d";
"0x49" -> "0x14" [style = dashed];
"0x50" -> "0x13";
"0x50" -> "0x14" [style = dashed];
"0x44" -> "0x3e";
"0x44" -> "0x42" [style = dashed];
"0x36" -> "0x2f";
"0x36" -> "0x34" [style = dashed];
"0x3d" -> "0x39";
"0x3d" -> "0x34" [style = dashed];
"0x34" -> "0x28";
"0x34" -> "0x14" [style = dashed];
"0x42" -> "0x2f";
"0x42" -> "0x14" [style = dashed];
"0x3e" -> "0x13";
"0x3e" -> "0x14" [style = dashed];
"0x39" -> "0x13";
"0x39" -> "0x14" [style = dashed];
"0x2f" -> "0x29";
"0x2f" -> "0x2d" [style = dashed];
"0x21" -> "0x18";
"0x21" -> "0x1f" [style = dashed];
"0x28" -> "0x24";
"0x28" -> "0x1f" [style = dashed];
"0x2d" -> "0x18";
"0x2d" -> "0x14" [style = dashed];
"0x1f" -> "0x17";
"0x1f" -> "0x14" [style = dashed];
"0x29" -> "0x13";
"0x29" -> "0x14" [style = dashed];
"0x24" -> "0x13";
"0x24" -> "0x14" [style = dashed];
"0x18" -> "0x13";
"0x18" -> "0x14" [style = dashed];
"0x17" -> "0x13";
"0x17" -> "0x14" [style = dashed];
"0x14" [label = "0"];
"0x13" [label = "1"];
}
Entering testBdd4
f: 5 nodes 1 leaves 3 minterms
000-----------  1
11------------  1

g: 5 nodes 1 leaves 3 minterms
000  1
11-  1

f and h are identical
Entering testBdd5
digraph "DD" {
size = "7.5,10"
center = true;
edge [dir = none];
{ node [shape = plaintext];
  edge [style = invis];
  "CONST NODES" [style = invis];
" a " -> " b " -> " c " -> " d " -> "CONST NODES"; 
}
{ rank = same; node [shape = box]; edge [style = invis];
"  lb  " -> "  ub  " -> "  f  " -> "  primes  " -> "  lprime  "; }
{ rank = same; " a ";
"0x487";
}
{ rank = same; " b ";
"0x484";
"0x486";
"0x483";
"0x488";
}
{ rank = same; " c ";
"0x481";
"0x43b";
}
{ rank = same; " d ";
"0x44b";
}
{ rank = same; "CONST NODES";
{ node [shape = box]; "0x413";
}
}
"  lb  " -> "0x488" [style = dotted];
"  ub  " -> "0x44b" [style = solid];
"  f  " -> "0x487" [style = solid];
"  primes  " -> "0x483" [style = solid];
"  lprime  " -> "0x483" [style = solid];
"0x487" -> "0x484";
"0x487" -> "0x486" [style = dashed];
"0x484" -> "0x44b";
"0x484" -> "0x481" [style = dotted];
"0x486" -> "0x43b";
"0x486" -> "0x413" [style = dotted];
"0x483" -> "0x44b";
"0x483" -> "0x413" [style = dotted];
"0x488" -> "0x481";
"0x488" -> "0x413" [style = dashed];
"0x481" -> "0x413";
"0x481" -> "0x44b" [style = dotted];
"0x43b" -> "0x44b";
"0x43b" -> "0x413" [style = dashed];
"0x44b" -> "0x413";
"0x44b" -> "0x413" [style = dotted];
"0x413" [label = "1"];
}
primes(1): 3 nodes 1 leaves 4 minterms
-1-1----------  1

primes(2): is the zero DD
primes(3): 4 nodes 1 leaves 2 minterms
1-01----------  1

primes(4): 6 nodes 1 leaves 5 minterms
-1-1---------- 1
010----------- 1

primes(5): 4 nodes 1 leaves 2 minterms
01-1----------  1

l1: 7 nodes 1 leaves 3 minterms
0111----------  1
111-----------  1

u1: 4 nodes 1 leaves 8 minterms
000-----------  1
011-----------  1
1-1-----------  1

interpolant1: 4 nodes 1 leaves 6 minterms
011-----------  1
1-1-----------  1

l2: 7 nodes 1 leaves 5 minterms
001-----------  1
0110----------  1
101-----------  1

u2: 5 nodes 1 leaves 8 minterms
-000----------  1
-01-----------  1
-110----------  1

interpolant2: 5 nodes 1 leaves 6 minterms
-01-----------  1
-110----------  1

l3: 4 nodes 1 leaves 2 minterms
00-1----------  1

u3: 3 nodes 1 leaves 4 minterms
-0-1----------  1

interpolant3: 3 nodes 1 leaves 4 minterms
-0-1----------  1

Entering testErrorHandling
Oops! Caught: empty DD.
Caught: Invalid argument.
f = var[1] | (var[2] & var[3])
var[0] | var[1] is not a cube
Cudd_Cofactor: Invalid restriction 2
Caught: Invalid argument.
f : 511 nodes 1 leaves 115422332637413376 minterms
g : 511 nodes 1 leaves 115422332637413376 minterms
h Caught: empty DD.
f : 88 nodes 1 leaves 226007109 minterms
g : 91 nodes 1 leaves 3143500301 minterms
h : 142 nodes 1 leaves 2917493192 minterms
Caught: Maximum memory exceeded.
Caught: Timeout expired.  Lag = 29 ms.
**** CUDD modifiable parameters ****
Hard limit for cache size: 2796202
Cache hit threshold for resizing: 30%
Garbage collection enabled: yes
Limit for fast unique table growth: 1677721
Maximum number of variables sifted per reordering: 1000
Maximum number of variable swaps per reordering: 2000000
Maximum growth while sifting a variable: 1.2
Dynamic reordering of BDDs enabled: no
Default BDD reordering method: 4
Dynamic reordering of ZDDs enabled: no
Default ZDD reordering method: 4
Realignment of ZDDs to BDDs enabled: no
Realignment of BDDs to ZDDs enabled: no
Dead nodes counted in triggering reordering: no
Group checking criterion: 7
Recombination threshold: 0
Symmetry violation threshold: 0
Arc violation threshold: 0
GA population size: 0
Number of crossovers for GA: 0
Next reordering threshold: 4004
**** CUDD non-modifiable parameters ****
Memory in use: 146651968
Peak number of nodes: 2044
Peak number of live nodes: 2030
Number of BDD variables: 60
Number of ZDD variables: 14
Number of cache entries: 524288
Number of cache look-ups: 5326
Number of cache hits: 1226
Number of cache insertions: 4217
Number of cache collisions: 16
Number of cache deletions: 2300
Cache used slots = 0.39% (expected 0.39%)
Soft limit for cache size: 76800
Number of buckets in unique table: 19200
Used buckets in unique table: 9.11% (expected 8.95%)
Number of BDD and ADD nodes: 3789
Number of ZDD nodes: 14
Number of dead BDD and ADD nodes: 3725
Number of dead ZDD nodes: 0
Total number of nodes allocated: 6011
Total number of nodes reclaimed: 154
Garbage collections so far: 3
Time for garbage collection: 0.00 sec
Reorderings so far: 0
Time for reordering: 0.00 sec