distr/obj/test.out

   1 Entering testBdd
   2 f: 3 nodes 1 leaves 1 minterms
   3 11  1
   4
   5 g: 3 nodes 1 leaves 3 minterms
   6 0-  1
   7 11  1
   8
   9 f and g are not complementary
  10 f is less than or equal to g
  11 g: 2 nodes 1 leaves 2 minterms
  12 1-  1
  13
  14 h: 2 nodes 1 leaves 2 minterms
  15 -1  1
  16
  17 x + h has 3 nodes
  18 h: 3 nodes 1 leaves 3 minterms
  19 01  1
  20 1-  1
  21
  22 Entering testAdd
  23 r: 6 nodes 3 leaves 3 minterms
  24 01  1
  25 10  1
  26 11  2
  27
  28 s: 4 nodes 2 leaves 1 minterms
  29 11  3
  30
  31 s: 1 nodes 1 leaves 4 minterms
  32 --  inf
  33
  34 p is less than or equal to r
  35 r: 4 nodes 2 leaves 3 minterms
  36 01  1
  37 1-  1
  38
  39 Entering testAdd2
  40 f: 7 nodes 4 leaves 4 minterms
  41 00  0.1
  42 01  0.2
  43 10  0.3
  44 11  0.4
  45
  46 l: 7 nodes 4 leaves 4 minterms
  47 00 -2.30259
  48 01 -1.60944
  49 10 -1.20397
  50 11 -0.916291
  51
  52 r: 7 nodes 4 leaves 4 minterms
  53 00 -0.230259
  54 01 -0.321888
  55 10 -0.361192
  56 11 -0.366516
  57
  58 e: 1 nodes 1 leaves 4 minterms
  59 --  1.84644
  60
  61 Entering testZdd
  62 s: 3 nodes 3 minterms
  63 1- 1
  64 01 1
  65
  66 v is less than s
  67 s: 1 nodes 1 minterms
  68 01 1
  69
  70 Entering testBdd2
  71 f: 7 nodes 1 leaves 7 minterms
  72 01-1  1
  73 101-  1
  74 1101  1
  75 111-  1
  76
  77 Irredundant cover of f:
  78 1-1- 1
  79 -1-1 1
  80
  81 Number of minterms (arbitrary precision): 7
  82 Number of minterms (extended precision):  7.000000e+00
  83 Two-literal clauses of f:
  84  x2 |  x3
  85  x1 |  x2
  86  x0 |  x3
  87  x0 |  x1
  88
  89 vect[0]
  90 1--- 1
  91
  92 vect[1]
  93 0--- 1
  94 -1-- 1
  95
  96 vect[2]
  97 10-- 1
  98 --1- 1
  99
 100 vect[3]
 101 0--- 1
 102 -10- 1
 103 ---1 1
 104
 105 digraph "DD" {
 106 size = "7.5,10"
 107 center = true;
 108 edge [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 "0x3e";
 118 "0x7b";
 119 "0x7e";
 120 "0x3a";
 121 }
 122 { rank = same; " x1 ";
 123 "0x7a";
 124 "0x7d";
 125 "0x3b";
 126 }
 127 { rank = same; " x2 ";
 128 "0x6b";
 129 "0x7c";
 130 }
 131 { rank = same; " x3 ";
 132 "0x6c";
 133 }
 134 { rank = same; "CONST NODES";
 135 { node [shape = box]; "0x34";
 136 }
 137 }
 138 "  v0  " -> "0x3a" [style = solid];
 139 "  v1  " -> "0x3e" [style = solid];
 140 "  v2  " -> "0x7b" [style = solid];
 141 "  v3  " -> "0x7e" [style = solid];
 142 "0x3e" -> "0x3b";
 143 "0x3e" -> "0x34" [style = dashed];
 144 "0x7b" -> "0x7a";
 145 "0x7b" -> "0x6b" [style = dashed];
 146 "0x7e" -> "0x7d";
 147 "0x7e" -> "0x34" [style = dashed];
 148 "0x3a" -> "0x34";
 149 "0x3a" -> "0x34" [style = dotted];
 150 "0x7a" -> "0x6b";
 151 "0x7a" -> "0x34" [style = dashed];
 152 "0x7d" -> "0x7c";
 153 "0x7d" -> "0x6c" [style = dashed];
 154 "0x3b" -> "0x34";
 155 "0x3b" -> "0x34" [style = dotted];
 156 "0x6b" -> "0x34";
 157 "0x6b" -> "0x34" [style = dotted];
 158 "0x7c" -> "0x6c";
 159 "0x7c" -> "0x34" [style = dashed];
 160 "0x6c" -> "0x34";
 161 "0x6c" -> "0x34" [style = dotted];
 162 "0x34" [label = "1"];
 163 }
 164 Entering testBdd3
 165 f: 10 nodes 1 leaves 50 minterms
 166 0-0-0-  1
 167 0-0-10  1
 168 0-100-  1
 169 0-1010  1
 170 0-11--  1
 171 10-00-  1
 172 10-010  1
 173 10-1--  1
 174 11000-  1
 175 110010  1
 176 1101--  1
 177 1110-1  1
 178 111101  1
 179
 180 f1: 5 nodes 1 leaves 36 minterms
 181 0---0-  1
 182 0---10  1
 183 10--0-  1
 184 10--10  1
 185
 186 f1 is less than or equal to f
 187 g: 6 nodes 1 leaves 62 minterms
 188 0-----  1
 189 10----  1
 190 110---  1
 191 1110--  1
 192 11110-  1
 193
 194 h: 8 nodes 1 leaves 51 minterms
 195 0-0-0-  1
 196 0-0-10  1
 197 0-100-  1
 198 0-1010  1
 199 0-11--  1
 200 10-00-  1
 201 10-010  1
 202 10-1--  1
 203 11000-  1
 204 110010  1
 205 1101--  1
 206 111--1  1
 207
 208 g * h == f
 209 Entering testZdd2
 210 p[0]: 3 nodes 1 leaves 64 minterms
 211 ----0-0  1
 212 ----1-1  1
 213
 214 p[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
 220 p[2]: 7 nodes 1 leaves 64 minterms
 221 0-0-0-0  1
 222 0-0-10-  1
 223 0-10---  1
 224 1-0-0-1  1
 225 1-0-11-  1
 226 1-11---  1
 227
 228 p[3]: 8 nodes 1 leaves 64 minterms
 229 0-0-0-1  1
 230 0-0-11-  1
 231 0-11---  1
 232 11-----  1
 233
 234 digraph "DD" {
 235 size = "7.5,10"
 236 center = true;
 237 edge [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 "0xb5";
 247 "0xb4";
 248 }
 249 { rank = same; " b2 ";
 250 "0x3b";
 251 }
 252 { rank = same; " a1 ";
 253 "0xb2";
 254 "0xb3";
 255 }
 256 { rank = same; " b1 ";
 257 "0x6c";
 258 }
 259 { rank = same; " a0 ";
 260 "0xb1";
 261 "0xb0";
 262 }
 263 { rank = same; " b0 ";
 264 "0x8b";
 265 }
 266 { rank = same; " c0 ";
 267 "0xaf";
 268 }
 269 { rank = same; "CONST NODES";
 270 { node [shape = box]; "0x34";
 271 }
 272 }
 273 "  s0  " -> "0xb0" [style = solid];
 274 "  s1  " -> "0xb2" [style = solid];
 275 "  s2  " -> "0xb4" [style = solid];
 276 "  c3  " -> "0xb5" [style = solid];
 277 "0xb5" -> "0x3b";
 278 "0xb5" -> "0xb3" [style = dashed];
 279 "0xb4" -> "0xb3";
 280 "0xb4" -> "0xb3" [style = dotted];
 281 "0x3b" -> "0x34";
 282 "0x3b" -> "0x34" [style = dotted];
 283 "0xb2" -> "0xb1";
 284 "0xb2" -> "0xb1" [style = dotted];
 285 "0xb3" -> "0x6c";
 286 "0xb3" -> "0xb1" [style = dashed];
 287 "0x6c" -> "0x34";
 288 "0x6c" -> "0x34" [style = dotted];
 289 "0xb1" -> "0x8b";
 290 "0xb1" -> "0xaf" [style = dashed];
 291 "0xb0" -> "0xaf";
 292 "0xb0" -> "0xaf" [style = dotted];
 293 "0x8b" -> "0x34";
 294 "0x8b" -> "0x34" [style = dotted];
 295 "0xaf" -> "0x34";
 296 "0xaf" -> "0x34" [style = dotted];
 297 "0x34" [label = "1"];
 298 }
 299 z[0]: 4 nodes 2 minterms
 300 00000000100010 1
 301 00000000010001 1
 302
 303 z[1]: 10 nodes 4 minterms
 304 00001000101000 1
 305 00001000010010 1
 306 00000100100100 1
 307 00000100010001 1
 308
 309 z[2]: 16 nodes 6 minterms
 310 10001010000000 1
 311 10000100101000 1
 312 10000100010010 1
 313 01001001000000 1
 314 01000100100100 1
 315 01000100010001 1
 316
 317 z[3]: 10 nodes 4 minterms
 318 10100000000000 1
 319 01001010000000 1
 320 01000100101000 1
 321 01000100010010 1
 322
 323 z[0]
 324 ----1-1 1
 325 ----0-0 1
 326 z[1]
 327 --1-11- 1
 328 --1-0-1 1
 329 --0-10- 1
 330 --0-0-0 1
 331 z[2]
 332 1-11--- 1
 333 1-0-11- 1
 334 1-0-0-1 1
 335 0-10--- 1
 336 0-0-10- 1
 337 0-0-0-0 1
 338 z[3]
 339 11----- 1
 340 0-11--- 1
 341 0-0-11- 1
 342 0-0-0-1 1
 343 digraph "ZDD" {
 344 size = "7.5,10"
 345 center = true;
 346 edge [dir = none];
 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";
 351 }
 352 { rank = same; node [shape = box]; edge [style = invis];
 353 "  s0  " -> "  s1  " -> "  s2  " -> "  c3  "; }
 354 { rank = same; " a2+ ";
 355 "0x6e";
 356 "0x77";
 357 }
 358 { rank = same; " a2- ";
 359 "0x6a";
 360 "0x75";
 361 }
 362 { rank = same; " b2+ ";
 363 "0x71";
 364 }
 365 { rank = same; " a1+ ";
 366 "0x57";
 367 "0x65";
 368 "0x5e";
 369 }
 370 { rank = same; " a1- ";
 371 "0x55";
 372 "0x63";
 373 }
 374 { rank = same; " b1+ ";
 375 "0x5f";
 376 }
 377 { rank = same; " b1- ";
 378 "0x5a";
 379 }
 380 { rank = same; " a0+ ";
 381 "0x50";
 382 "0x42";
 383 "0x49";
 384 }
 385 { rank = same; " a0- ";
 386 "0x4e";
 387 "0x40";
 388 }
 389 { rank = same; " b0+ ";
 390 "0x4a";
 391 }
 392 { rank = same; " b0- ";
 393 "0x45";
 394 }
 395 { rank = same; " c0+ ";
 396 "0x39";
 397 }
 398 { rank = same; " c0- ";
 399 "0x38";
 400 }
 401 { rank = same; "CONST NODES";
 402 { node [shape = box]; "0x35";
 403 "0x34";
 404 }
 405 }
 406 "  s0  " -> "0x42" [style = solid];
 407 "  s1  " -> "0x57" [style = solid];
 408 "  s2  " -> "0x6e" [style = solid];
 409 "  c3  " -> "0x77" [style = solid];
 410 "0x6e" -> "0x65";
 411 "0x6e" -> "0x6a" [style = dashed];
 412 "0x77" -> "0x71";
 413 "0x77" -> "0x75" [style = dashed];
 414 "0x6a" -> "0x5e";
 415 "0x6a" -> "0x35" [style = dashed];
 416 "0x75" -> "0x65";
 417 "0x75" -> "0x35" [style = dashed];
 418 "0x71" -> "0x34";
 419 "0x71" -> "0x35" [style = dashed];
 420 "0x57" -> "0x50";
 421 "0x57" -> "0x55" [style = dashed];
 422 "0x65" -> "0x5f";
 423 "0x65" -> "0x63" [style = dashed];
 424 "0x5e" -> "0x5a";
 425 "0x5e" -> "0x55" [style = dashed];
 426 "0x55" -> "0x49";
 427 "0x55" -> "0x35" [style = dashed];
 428 "0x63" -> "0x50";
 429 "0x63" -> "0x35" [style = dashed];
 430 "0x5f" -> "0x34";
 431 "0x5f" -> "0x35" [style = dashed];
 432 "0x5a" -> "0x34";
 433 "0x5a" -> "0x35" [style = dashed];
 434 "0x50" -> "0x4a";
 435 "0x50" -> "0x4e" [style = dashed];
 436 "0x42" -> "0x39";
 437 "0x42" -> "0x40" [style = dashed];
 438 "0x49" -> "0x45";
 439 "0x49" -> "0x40" [style = dashed];
 440 "0x4e" -> "0x39";
 441 "0x4e" -> "0x35" [style = dashed];
 442 "0x40" -> "0x38";
 443 "0x40" -> "0x35" [style = dashed];
 444 "0x4a" -> "0x34";
 445 "0x4a" -> "0x35" [style = dashed];
 446 "0x45" -> "0x34";
 447 "0x45" -> "0x35" [style = dashed];
 448 "0x39" -> "0x34";
 449 "0x39" -> "0x35" [style = dashed];
 450 "0x38" -> "0x34";
 451 "0x38" -> "0x35" [style = dashed];
 452 "0x35" [label = "0"];
 453 "0x34" [label = "1"];
 454 }
 455 Entering testBdd4
 456 f: 5 nodes 1 leaves 3 minterms
 457 000-----------  1
 458 11------------  1
 459
 460 g: 5 nodes 1 leaves 3 minterms
 461 000  1
 462 11-  1
 463
 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%)
 503 Unique lookups: 475
 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