1 /**
2 @file
3
4 @ingroup cplusplus
5
6 @brief Test program for the C++ object-oriented encapsulation of CUDD.
7
8 @author Fabio Somenzi
9
10 @copyright@parblock
11 Copyright (c) 1995-2015, Regents of the University of Colorado
12
13 All rights reserved.
14
15 Redistribution and use in source and binary forms, with or without
16 modification, are permitted provided that the following conditions
17 are met:
18
19 Redistributions of source code must retain the above copyright
20 notice, this list of conditions and the following disclaimer.
21
22 Redistributions in binary form must reproduce the above copyright
23 notice, this list of conditions and the following disclaimer in the
24 documentation and/or other materials provided with the distribution.
25
26 Neither the name of the University of Colorado nor the names of its
27 contributors may be used to endorse or promote products derived from
28 this software without specific prior written permission.
29
30 THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
31 "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
32 LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
33 FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
34 COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
35 INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
36 BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
37 LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
38 CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
39 LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
40 ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
41 POSSIBILITY OF SUCH DAMAGE.
42 @endparblock
43
44 */
45
46 #include "cuddObj.hh"
47 #include <math.h>
48 #include <iostream>
49 #include <sstream>
50 #include <cassert>
51 #include <stdexcept>
52
53 using namespace std;
54
55 /*---------------------------------------------------------------------------*/
56 /* Variable declarations */
57 /*---------------------------------------------------------------------------*/
58
59 /*---------------------------------------------------------------------------*/
60 /* Static function prototypes */
61 /*---------------------------------------------------------------------------*/
62
63 static void testBdd(Cudd& mgr, int verbosity);
64 static void testAdd(Cudd& mgr, int verbosity);
65 static void testAdd2(Cudd& mgr, int verbosity);
66 static void testZdd(Cudd& mgr, int verbosity);
67 static void testBdd2(Cudd& mgr, int verbosity);
68 static void testBdd3(Cudd& mgr, int verbosity);
69 static void testZdd2(Cudd& mgr, int verbosity);
70 static void testBdd4(Cudd& mgr, int verbosity);
71 static void testBdd5(Cudd& mgr, int verbosity);
72 static void testInterpolation(Cudd& mgr, int verbosity);
73 static void testErrorHandling(Cudd& mgr, int verbosity);
74
75 /*---------------------------------------------------------------------------*/
76 /* Definition of exported functions */
77 /*---------------------------------------------------------------------------*/
78
79 /**
80 @brief Main program for testobj.
81 */
82 int
main(int argc,char ** argv)83 main(int argc, char **argv)
84 {
85 int verbosity = 0;
86
87 if (argc == 2) {
88 int cnt;
89 int retval = sscanf(argv[1], "%d %n", &verbosity, &cnt);
90 if (retval != 1 || argv[1][cnt])
91 return 1;
92 } else if (argc != 1) {
93 return 1;
94 }
95
96 Cudd mgr(0,2);
97 if (verbosity > 2) mgr.makeVerbose(); // trace constructors and destructors
98 testBdd(mgr,verbosity);
99 testAdd(mgr,verbosity);
100 testAdd2(mgr,verbosity);
101 testZdd(mgr,verbosity);
102 testBdd2(mgr,verbosity);
103 testBdd3(mgr,verbosity);
104 testZdd2(mgr,verbosity);
105 testBdd4(mgr,verbosity);
106 testBdd5(mgr,verbosity);
107 testInterpolation(mgr,verbosity);
108 testErrorHandling(mgr,verbosity);
109 if (verbosity) mgr.info();
110 return 0;
111
112 } // main
113
114
115 /**
116 @brief Test basic operators on BDDs.
117
118 @details The function returns void
119 because it relies on the error handling done by the interface. The
120 default error handler causes program termination.
121
122 @sideeffect Creates BDD variables in the manager.
123
124 @see testBdd2 testBdd3 testBdd4 testBdd5
125
126 */
127 static void
testBdd(Cudd & mgr,int verbosity)128 testBdd(
129 Cudd& mgr,
130 int verbosity)
131 {
132 if (verbosity) cout << "Entering testBdd\n";
133 // Create two new variables in the manager. If testBdd is called before
134 // any variable is created in mgr, then x gets index 0 and y gets index 1.
135 BDD x = mgr.bddVar();
136 BDD y = mgr.bddVar();
137
138 BDD f = x * y;
139 if (verbosity) cout << "f"; f.print(2,verbosity);
140
141 BDD g = y + !x;
142 if (verbosity) cout << "g"; g.print(2,verbosity);
143
144 if (verbosity)
145 cout << "f and g are" << (f == !g ? "" : " not") << " complementary\n";
146 if (verbosity)
147 cout << "f is" << (f <= g ? "" : " not") << " less than or equal to g\n";
148
149 g = f | ~g;
150 if (verbosity) cout << "g"; g.print(2,verbosity);
151
152 BDD h = f = y;
153 if (verbosity) cout << "h"; h.print(2,verbosity);
154
155 if (verbosity) cout << "x + h has " << (x+h).nodeCount() << " nodes\n";
156
157 h += x;
158 if (verbosity) cout << "h"; h.print(2,verbosity);
159
160 } // testBdd
161
162
163 /**
164 @brief Test basic operators on ADDs.
165
166 @details The function returns void because it relies on the error
167 handling done by the interface. The default error handler causes
168 program termination.
169
170 @sideeffect May create ADD variables in the manager.
171
172 @see testAdd2
173
174 */
175 static void
testAdd(Cudd & mgr,int verbosity)176 testAdd(
177 Cudd& mgr,
178 int verbosity)
179 {
180 if (verbosity) cout << "Entering testAdd\n";
181 // Create two ADD variables. If we called method addVar without an
182 // argument, we would get two new indices. If testAdd is indeed called
183 // after testBdd, then those indices would be 2 and 3. By specifying the
184 // arguments, on the other hand, we avoid creating new unnecessary BDD
185 // variables.
186 ADD p = mgr.addVar(0);
187 ADD q = mgr.addVar(1);
188
189 // Test arithmetic operators.
190 ADD r = p + q;
191 if (verbosity) cout << "r"; r.print(2,verbosity);
192
193 // CUDD_VALUE_TYPE is double.
194 ADD s = mgr.constant(3.0);
195 s *= p * q;
196 if (verbosity) cout << "s"; s.print(2,verbosity);
197
198 s += mgr.plusInfinity();
199 if (verbosity) cout << "s"; s.print(2,verbosity);
200
201 // Test relational operators.
202 if (verbosity)
203 cout << "p is" << (p <= r ? "" : " not") << " less than or equal to r\n";
204
205 // Test logical operators.
206 r = p | q;
207 if (verbosity) cout << "r"; r.print(2,verbosity);
208
209 } // testAdd
210
211
212 /**
213 @brief Test some more operators on ADDs.
214
215 @details The function returns void because it relies on the error
216 handling done by the interface. The default error handler causes
217 program termination.
218
219 @sideeffect May create ADD variables in the manager.
220
221 @see testAdd
222
223 */
224 static void
testAdd2(Cudd & mgr,int verbosity)225 testAdd2(
226 Cudd& mgr,
227 int verbosity)
228 {
229 if (verbosity) cout << "Entering testAdd2\n";
230 // Create two ADD variables. If we called method addVar without an
231 // argument, we would get two new indices.
232 vector<ADD> x(2);
233 for (size_t i = 0; i < 2; ++i) {
234 x[i] = mgr.addVar((int) i);
235 }
236
237 // Build a probability density function: [0.1, 0.2, 0.3, 0.4].
238 ADD f0 = x[1].Ite(mgr.constant(0.2), mgr.constant(0.1));
239 ADD f1 = x[1].Ite(mgr.constant(0.4), mgr.constant(0.3));
240 ADD f = x[0].Ite(f1, f0);
241 if (verbosity) cout << "f"; f.print(2,verbosity);
242
243 // Compute the entropy.
244 ADD l = f.Log();
245 if (verbosity) cout << "l"; l.print(2,verbosity);
246 ADD r = f * l;
247 if (verbosity) cout << "r"; r.print(2,verbosity);
248
249 ADD e = r.MatrixMultiply(mgr.constant(-1.0/log(2.0)),x);
250 if (verbosity) cout << "e"; e.print(2,verbosity);
251
252 } // testAdd2
253
254
255 /**
256 @brief Test basic operators on ZDDs.
257
258 @details The function returns void because it relies on the error
259 handling done by the interface. The default error handler causes
260 program termination.
261
262 @sideeffect May create ZDD variables in the manager.
263
264 @see testZdd2
265
266 */
267 static void
testZdd(Cudd & mgr,int verbosity)268 testZdd(
269 Cudd& mgr,
270 int verbosity)
271 {
272 if (verbosity) cout << "Entering testZdd\n";
273 ZDD v = mgr.zddVar(0);
274 ZDD w = mgr.zddVar(1);
275
276 ZDD s = v + w;
277 if (verbosity) cout << "s"; s.print(2,verbosity);
278
279 if (verbosity) cout << "v is" << (v < s ? "" : " not") << " less than s\n";
280
281 s -= v;
282 if (verbosity) cout << "s"; s.print(2,verbosity);
283
284 } // testZdd
285
286
287 /**
288 @brief Test vector operators on BDDs.
289
290 @details The function returns void because it relies on the error
291 handling done by the interface. The default error handler causes
292 program termination.
293
294 @sideeffect May create BDD variables in the manager.
295
296 @see testBdd testBdd3 testBdd4 testBdd5
297
298 */
299 static void
testBdd2(Cudd & mgr,int verbosity)300 testBdd2(
301 Cudd& mgr,
302 int verbosity)
303 {
304 if (verbosity) cout << "Entering testBdd2\n";
305 vector<BDD> x(4);
306 for (size_t i = 0; i < 4; ++i) {
307 x[i] = mgr.bddVar((int) i);
308 }
309
310 // Create the BDD for the Achilles' Heel function.
311 BDD p1 = x[0] * x[2];
312 BDD p2 = x[1] * x[3];
313 BDD f = p1 + p2;
314 const char* inames[] = {"x0", "x1", "x2", "x3"};
315 if (verbosity) {
316 cout << "f"; f.print(4,verbosity);
317 cout << "Irredundant cover of f:" << endl; f.PrintCover();
318 cout << "Number of minterms (arbitrary precision): "; f.ApaPrintMinterm(4);
319 cout << "Number of minterms (extended precision): "; f.EpdPrintMinterm(4);
320 cout << "Two-literal clauses of f:" << endl;
321 f.PrintTwoLiteralClauses((char **)inames); cout << endl;
322 }
323
324 vector<BDD> vect = f.CharToVect();
325 if (verbosity) {
326 for (size_t i = 0; i < vect.size(); i++) {
327 cout << "vect[" << i << "]" << endl; vect[i].PrintCover();
328 }
329 }
330
331 // v0,...,v3 suffice if testBdd2 is called before testBdd3.
332 if (verbosity) {
333 const char* onames[] = {"v0", "v1", "v2", "v3", "v4", "v5"};
334 mgr.DumpDot(vect, (char **)inames,(char **)onames);
335 }
336
337 } // testBdd2
338
339
340 /**
341 @brief Test additional operators on BDDs.
342
343 @details The function returns void because it relies on the error
344 handling done by the interface. The default error handler causes
345 program termination.
346
347 @sideeffect May create BDD variables in the manager.
348
349 @see testBdd testBdd2 testBdd4 testBdd5
350
351 */
352 static void
testBdd3(Cudd & mgr,int verbosity)353 testBdd3(
354 Cudd& mgr,
355 int verbosity)
356 {
357 if (verbosity) cout << "Entering testBdd3\n";
358 vector<BDD> x(6);
359 for (size_t i = 0; i < 6; ++i) {
360 x[i] = mgr.bddVar((int) i);
361 }
362
363 BDD G = x[4] + !x[5];
364 BDD H = x[4] * x[5];
365 BDD E = x[3].Ite(G,!x[5]);
366 BDD F = x[3] + !H;
367 BDD D = x[2].Ite(F,!H);
368 BDD C = x[2].Ite(E,!F);
369 BDD B = x[1].Ite(C,!F);
370 BDD A = x[0].Ite(B,!D);
371 BDD f = !A;
372 if (verbosity) cout << "f"; f.print(6,verbosity);
373
374 BDD f1 = f.RemapUnderApprox(6);
375 if (verbosity) cout << "f1"; f1.print(6,verbosity);
376 if (verbosity)
377 cout << "f1 is" << (f1 <= f ? "" : " not") << " less than or equal to f\n";
378
379 BDD g;
380 BDD h;
381 f.GenConjDecomp(&g,&h);
382 if (verbosity) {
383 cout << "g"; g.print(6,verbosity);
384 cout << "h"; h.print(6,verbosity);
385 cout << "g * h " << (g * h == f ? "==" : "!=") << " f\n";
386 }
387
388 } // testBdd3
389
390
391 /**
392 @brief Test cover manipulation with BDDs and ZDDs.
393
394 @details The function returns void because it relies on the error
395 handling done by the interface. The default error handler causes
396 program termination. This function builds the BDDs for a
397 transformed adder: one in which the inputs are transformations of
398 the original inputs. It then creates ZDDs for the covers from the
399 BDDs.
400
401 @sideeffect May create BDD and ZDD variables in the manager.
402
403 @see testZdd
404
405 */
406 static void
testZdd2(Cudd & mgr,int verbosity)407 testZdd2(
408 Cudd& mgr,
409 int verbosity)
410 {
411 if (verbosity) cout << "Entering testZdd2\n";
412 size_t N = 3; // number of bits
413 // Create variables.
414 vector<BDD> a(N);
415 vector<BDD> b(N);
416 vector<BDD> c(N+1);
417 for (size_t i = 0; i < N; ++i) {
418 a[N-1-i] = mgr.bddVar(2*(int)i);
419 b[N-1-i] = mgr.bddVar(2*(int)i+1);
420 }
421 c[0] = mgr.bddVar(2*(int)N);
422 // Build functions.
423 vector<BDD> s(N);
424 for (size_t i = 0; i < N; ++i) {
425 s[i] = a[i].Xnor(c[i]);
426 c[i+1] = a[i].Ite(b[i],c[i]);
427 }
428
429 // Create array of outputs and print it.
430 vector<BDD> p(N+1);
431 for (size_t i = 0; i < N; ++i) {
432 p[i] = s[i];
433 }
434 p[N] = c[N];
435 if (verbosity) {
436 for (size_t i = 0; i < p.size(); ++i) {
437 cout << "p[" << i << "]"; p[i].print(2*(int)N+1,verbosity);
438 }
439 }
440 const char* onames[] = {"s0", "s1", "s2", "c3"};
441 if (verbosity) {
442 const char* inames[] = {"a2", "b2", "a1", "b1", "a0", "b0", "c0"};
443 mgr.DumpDot(p, (char **)inames,(char **)onames);
444 }
445
446 // Create ZDD variables and build ZDD covers from BDDs.
447 mgr.zddVarsFromBddVars(2);
448 vector<ZDD> z(N+1);
449 for (size_t i = 0; i < N+1; ++i) {
450 ZDD temp;
451 BDD dummy = p[i].zddIsop(p[i],&temp);
452 z[i] = temp;
453 }
454
455 // Print out covers.
456 if (verbosity) {
457 DdGen *gen;
458 int *path;
459 for (size_t i = 0; i < z.size(); i++) {
460 cout << "z[" << i << "]"; z[i].print(4*(int)N+2,verbosity);
461 }
462 // Print cover in two different ways: with PrintCover and with
463 // enumeration over the paths. The only difference should be
464 // a reversal in the order of the cubes.
465 for (size_t i = 0; i < z.size(); i++) {
466 cout << "z[" << i << "]\n"; z[i].PrintCover();
467 cout << "z[" << i << "]\n";
468 DdNode *f = Cudd_Not(z[i].getNode());
469 Cudd_zddForeachPath(z[i].manager(), f, gen, path) {
470 for (size_t q = 0; q < 4*N+2; q += 2) {
471 int v = path[q] * 4 + path[q+1];
472 switch (v) {
473 case 0:
474 case 2:
475 case 8:
476 case 10:
477 cout << "-";
478 break;
479 case 1:
480 case 9:
481 cout << "0";
482 break;
483 case 6:
484 cout << "1";
485 break;
486 default:
487 cout << "?";
488 }
489 }
490 cout << " 1\n";
491 }
492 }
493 const char* znames[] = {"a2+", "a2-", "b2+", "b2-", "a1+", "a1-", "b1+",
494 "b1-", "a0+", "a0-", "b0+", "b0-", "c0+", "c0-"};
495 mgr.DumpDot(z, (char **)znames,(char **)onames);
496 }
497
498 } // testZdd2
499
500
501 /**
502 @brief Test transfer between BDD managers.
503
504 @details The function returns void because it relies on the error
505 handling done by the interface. The default error handler causes
506 program termination.
507
508 @sideeffect May create BDD variables in the manager.
509
510 @see testBdd testBdd2 testBdd3 testBdd5
511
512 */
513 static void
testBdd4(Cudd & mgr,int verbosity)514 testBdd4(
515 Cudd& mgr,
516 int verbosity)
517 {
518 if (verbosity) cout << "Entering testBdd4\n";
519 BDD x = mgr.bddVar(0);
520 BDD y = mgr.bddVar(1);
521 BDD z = mgr.bddVar(2);
522
523 BDD f = (~x & ~y & ~z) | (x & y);
524 if (verbosity) cout << "f"; f.print(3,verbosity);
525
526 Cudd otherMgr(0,0);
527 BDD g = f.Transfer(otherMgr);
528 if (verbosity) cout << "g"; g.print(3,verbosity);
529
530 BDD h = g.Transfer(mgr);
531 if (verbosity)
532 cout << "f and h are" << (f == h ? "" : " not") << " identical\n";
533
534 } // testBdd4
535
536
537 /**
538 @brief Test maximal expansion of cubes.
539
540 @details The function returns void because it relies on the error
541 handling done by the interface. The default error handler causes
542 program termination.
543
544 @sideeffect May create BDD variables in the manager.
545
546 @see testBdd testBdd2 testBdd3 testBdd4
547
548 */
549 static void
testBdd5(Cudd & mgr,int verbosity)550 testBdd5(
551 Cudd& mgr,
552 int verbosity)
553 {
554 if (verbosity) cout << "Entering testBdd5\n";
555 vector<BDD> x;
556 x.reserve(4);
557 for (int i = 0; i < 4; i++) {
558 x.push_back(mgr.bddVar(i));
559 }
560 const char* inames[] = {"a", "b", "c", "d"};
561 BDD f = (x[1] & x[3]) | (x[0] & ~x[2] & x[3]) | (~x[0] & x[1] & ~x[2]);
562 BDD lb = x[1] & ~x[2] & x[3];
563 BDD ub = x[3];
564 BDD primes = lb.MaximallyExpand(ub,f);
565 assert(primes == (x[1] & x[3]));
566 BDD lprime = primes.LargestPrimeUnate(lb);
567 assert(lprime == primes);
568 if (verbosity) {
569 const char * onames[] = {"lb", "ub", "f", "primes", "lprime"};
570 vector<BDD> z;
571 z.reserve(5);
572 z.push_back(lb);
573 z.push_back(ub);
574 z.push_back(f);
575 z.push_back(primes);
576 z.push_back(lprime);
577 mgr.DumpDot(z, (char **)inames, (char **)onames);
578 cout << "primes(1)"; primes.print(4,verbosity);
579 }
580
581 lb = ~x[0] & x[2] & x[3];
582 primes = lb.MaximallyExpand(ub,f);
583 assert(primes == mgr.bddZero());
584 if (verbosity) {
585 cout << "primes(2)"; primes.print(4,verbosity);
586 }
587
588 lb = x[0] & ~x[2] & x[3];
589 primes = lb.MaximallyExpand(ub,f);
590 assert(primes == lb);
591 lprime = primes.LargestPrimeUnate(lb);
592 assert(lprime == primes);
593 if (verbosity) {
594 cout << "primes(3)"; primes.print(4,verbosity);
595 }
596
597 lb = ~x[0] & x[1] & ~x[2] & x[3];
598 ub = mgr.bddOne();
599 primes = lb.MaximallyExpand(ub,f);
600 assert(primes == ((x[1] & x[3]) | (~x[0] & x[1] & ~x[2])));
601 lprime = primes.LargestPrimeUnate(lb);
602 assert(lprime == (x[1] & x[3]));
603 if (verbosity) {
604 cout << "primes(4)"; primes.print(4,1); primes.PrintCover();
605 }
606
607 ub = ~x[0] & x[3];
608 primes = lb.MaximallyExpand(ub,f);
609 assert(primes == (~x[0] & x[1] & x[3]));
610 lprime = primes.LargestPrimeUnate(lb);
611 assert(lprime == primes);
612 if (verbosity) {
613 cout << "primes(5)"; primes.print(4,verbosity);
614 }
615
616 } // testBdd5
617
618
619 /**
620 @brief Test BDD interpolation.
621 */
622 static void
testInterpolation(Cudd & mgr,int verbosity)623 testInterpolation(
624 Cudd& mgr,
625 int verbosity)
626 {
627 BDD a = mgr.bddVar(0);
628 BDD b = mgr.bddVar(1);
629 BDD c = mgr.bddVar(2);
630 BDD d = mgr.bddVar(3);
631
632 BDD l1 = (a | d) & b & c;
633 BDD u1 = (~a & ~b & ~c) | ((a | b) & c);
634 BDD ip1 = l1.Interpolate(u1);
635 if (verbosity) {
636 cout << "l1"; l1.print(4,verbosity);
637 cout << "u1"; u1.print(4,verbosity);
638 cout << "interpolant1"; ip1.print(4,verbosity);
639 }
640
641 BDD l2 = (~a | ~b) & (a | c) & (b | c) & (a | ~b | ~d);
642 BDD u2 = (~b & ~d) | (~b & c & d) | (b & c & ~d);
643 BDD ip2 = l2.Interpolate(u2);
644 if (verbosity) {
645 cout << "l2"; l2.print(4,verbosity);
646 cout << "u2"; u2.print(4,verbosity);
647 cout << "interpolant2"; ip2.print(4,verbosity);
648 }
649
650 BDD l3 = ~a & ~b & d;
651 BDD u3 = ~b & d;
652 BDD ip3 = l3.Interpolate(u3);
653 if (verbosity) {
654 cout << "l3"; l3.print(4,verbosity);
655 cout << "u3"; u3.print(4,verbosity);
656 cout << "interpolant3"; ip3.print(4,verbosity);
657 }
658
659 } // testInterpolation
660
661
662 /**
663 @brief Basic test of error handling.
664
665 @details This function also illustrates the use of the overloading of the
666 stream insertion operator (operator<<) for BDDs.
667 */
668 static void
testErrorHandling(Cudd & mgr,int verbosity)669 testErrorHandling(
670 Cudd& mgr,
671 int verbosity)
672 {
673 // Setup.
674
675 if (verbosity) cout << "Entering testErrorHandling\n";
676
677 FILE *savefp = 0;
678 if (verbosity == 0) {
679 // Suppress error messages coming from CUDD.
680 savefp = mgr.ReadStderr();
681 #ifndef _WIN32
682 FILE * devnull = fopen("/dev/null", "w");
683 #else
684 FILE * devnull = fopen("NUL", "w");
685 #endif
686 if (devnull)
687 mgr.SetStderr(devnull);
688 }
689
690 size_t const N = 60;
691 vector<BDD> vars;
692 vars.reserve(N);
693 for (size_t i = 0; i < N; ++i) {
694 vars.push_back(mgr.bddVar((int) i));
695 }
696
697 // It is necessary to give names to all the BDD variables in the manager
698 // for the names to be used by operator<<.
699 for (int i = 0; i < mgr.ReadSize(); ++i) {
700 ostringstream os;
701 os << "var[" << i << "]";
702 mgr.pushVariableName(os.str());
703 }
704
705 // Tests.
706
707 // Trying to print the expression of an empty BDD.
708 try {
709 BDD empty;
710 if (verbosity > 0)
711 cout << "Oops! ";
712 cout << empty << endl;
713 } catch (logic_error const & e) {
714 if (verbosity > 0)
715 cerr << "Caught: " << e.what() << endl;
716 }
717
718 // Trying to extract a minterm from the zero BDD.
719 try {
720 BDD zero = mgr.bddZero();
721 BDD minterm = zero.PickOneMinterm(vars);
722 } catch (logic_error const & e) {
723 if (verbosity > 0)
724 cerr << "Caught: " << e.what() << endl;
725 mgr.ClearErrorCode();
726 }
727
728 // Passing a non-cube second argument to Cofactor.
729 try {
730 BDD f = vars.at(1) | (vars.at(2) & vars.at(3));
731 if (verbosity > 0)
732 cout << "f = " << f << endl;
733 BDD notAcube = vars.at(0) | vars.at(1);
734 if (verbosity > 0)
735 cout << notAcube << " is not a cube" << endl;
736 BDD fc = f.Cofactor(notAcube);
737 if (verbosity > 0) {
738 cout << "The cofactor is: "; fc.summary(3);
739 }
740 } catch (logic_error const & e) {
741 if (verbosity > 0)
742 cerr << "Caught: " << e.what() << endl;
743 mgr.ClearErrorCode();
744 }
745
746 #if 0
747 // This attempt to allocate over 100 GB may succeed on machines with
748 // enough memory; hence we exclude it from "make check."
749 // Failing malloc.
750 // Don't let the memory manager kill the program if malloc fails.
751 DD_OOMFP saveHandler = mgr.InstallOutOfMemoryHandler(Cudd_OutOfMemSilent);
752 try {
753 mgr.Reserve(2000000000);
754 } catch (logic_error const & e) {
755 if (verbosity > 0)
756 cerr << "Caught: " << e.what() << endl;
757 mgr.ClearErrorCode();
758 }
759 (void) mgr.InstallOutOfMemoryHandler(saveHandler);
760 #endif
761
762 // Forgetting to check for empty result when setting a limit on
763 // the number of new nodes.
764 try {
765 BDD f = mgr.bddOne();
766 BDD g = f;
767 for (size_t i = 0; i < N/2; i += 4) {
768 f &= vars.at(i) | vars.at(i+N/2);
769 g &= vars.at(i+1) | vars.at(i+N/2+1);
770 }
771 if (verbosity > 0) {
772 cout << "f "; f.summary(N);
773 cout << "g "; g.summary(N);
774 }
775 BDD h = f.And(g, /* max new nodes */ 1);
776 if (verbosity > 0) {
777 cout << "h "; h.summary(N);
778 }
779 } catch (logic_error const & e) {
780 if (verbosity > 0)
781 cerr << "Caught: " << e.what() << endl;
782 mgr.ClearErrorCode();
783 }
784
785 // Using more memory than the set limit.
786 size_t saveLimit = mgr.SetMaxMemory((size_t) 1);
787 try {
788 // The limit is ridiculously low (1 byte), but CUDD is resourceful.
789 // Therefore we can still create a few BDDs.
790 BDD f = mgr.Interval(vars, 122346345U, 348353453U);
791 if (verbosity > 0) {
792 cout << "f "; f.summary(N);
793 }
794 BDD g = mgr.Interval(vars, 34234U, 3143534534U);
795 if (verbosity > 0) {
796 cout << "g "; g.summary(N);
797 }
798 BDD h = f ^ g;
799 if (verbosity > 0) {
800 cout << "h "; h.summary(N);
801 }
802 // But if we really insist...
803 BDD extra = mgr.bddVar(60000);
804 // Here we would have to fix the variable names.
805 } catch (logic_error const & e) {
806 if (verbosity > 0)
807 cerr << "Caught: " << e.what() << endl;
808 mgr.ClearErrorCode();
809 }
810 (void) mgr.SetMaxMemory(saveLimit);
811
812 // Timing out.
813 unsigned long saveTl = mgr.SetTimeLimit(1UL); // 1 ms
814 try {
815 BDD f = mgr.bddOne();
816 for (size_t i = 0; i < N/2; ++i) {
817 f &= vars.at(i) | vars.at(i+N/2);
818 }
819 } catch (logic_error const & e) {
820 if (verbosity > 0)
821 cerr << "Caught: " << e.what() << endl;
822 mgr.ClearErrorCode();
823 }
824 (void) mgr.SetTimeLimit(saveTl);
825
826 // Let's clean up after ourselves.
827 mgr.clearVariableNames();
828 if (verbosity == 0) {
829 mgr.SetStderr(savefp);
830 }
831
832 } // testErrorHandling
833