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