1 /**
2 @file
3
4 @ingroup cudd
5
6 @brief Sanity check tests for some CUDD functions.
7
8 @details testcudd reads a matrix with real coefficients and
9 transforms it into an %ADD. It then performs various operations on
10 the %ADD and on the %BDD corresponding to the ADD pattern. Finally,
11 testcudd tests functions relate to Walsh matrices and matrix
12 multiplication.
13
14 @author Fabio Somenzi
15
16 @copyright@parblock
17 Copyright (c) 1995-2015, Regents of the University of Colorado
18
19 All rights reserved.
20
21 Redistribution and use in source and binary forms, with or without
22 modification, are permitted provided that the following conditions
23 are met:
24
25 Redistributions of source code must retain the above copyright
26 notice, this list of conditions and the following disclaimer.
27
28 Redistributions in binary form must reproduce the above copyright
29 notice, this list of conditions and the following disclaimer in the
30 documentation and/or other materials provided with the distribution.
31
32 Neither the name of the University of Colorado nor the names of its
33 contributors may be used to endorse or promote products derived from
34 this software without specific prior written permission.
35
36 THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
37 "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
38 LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
39 FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
40 COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
41 INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
42 BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
43 LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
44 CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
45 LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
46 ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
47 POSSIBILITY OF SUCH DAMAGE.
48 @endparblock
49
50 */
51
52 #include "util.h"
53 #include "cuddInt.h"
54
55
56 /*---------------------------------------------------------------------------*/
57 /* Constant declarations */
58 /*---------------------------------------------------------------------------*/
59
60 #define TESTCUDD_VERSION "TestCudd Version #1.0, Release date 3/17/01"
61
62 /*---------------------------------------------------------------------------*/
63 /* Variable declarations */
64 /*---------------------------------------------------------------------------*/
65
66 static const char *onames[] = { "C", "M" }; /* names of functions to be dumped */
67
68 /** \cond */
69
70 /*---------------------------------------------------------------------------*/
71 /* Static function prototypes */
72 /*---------------------------------------------------------------------------*/
73
74 static void usage (char * prog);
75 static FILE *open_file (char *filename, const char *mode);
76 static int testIterators (DdManager *dd, DdNode *M, DdNode *C, int pr);
77 static int testXor (DdManager *dd, DdNode *f, int pr, int nvars);
78 static int testHamming (DdManager *dd, DdNode *f, int pr);
79 static int testWalsh (DdManager *dd, int N, int cmu, int approach, int pr);
80 static int testSupport(DdManager *dd, DdNode *f, DdNode *g, int pr);
81
82 /** \endcond */
83
84
85
86 /**
87 @brief Main function for testcudd.
88
89 @sideeffect None
90
91 */
92 int
main(int argc,char * const * argv)93 main(int argc, char * const *argv)
94 {
95 FILE *fp; /* pointer to input file */
96 char *file = (char *) ""; /* input file name */
97 FILE *dfp = NULL; /* pointer to dump file */
98 FILE *savefp = NULL;/* pointer to save current manager's stdout setting */
99 char *dfile; /* file for DD dump */
100 DdNode *dfunc[2]; /* addresses of the functions to be dumped */
101 DdManager *dd; /* pointer to DD manager */
102 DdNode *one; /* fast access to constant function */
103 DdNode *M;
104 DdNode **x; /* pointers to variables */
105 DdNode **y; /* pointers to variables */
106 DdNode **xn; /* complements of row variables */
107 DdNode **yn_; /* complements of column variables */
108 DdNode **xvars;
109 DdNode **yvars;
110 DdNode *C; /* result of converting from ADD to BDD */
111 DdNode *ess; /* cube of essential variables */
112 DdNode *shortP; /* BDD cube of shortest path */
113 DdNode *largest; /* BDD of largest cube */
114 DdNode *shortA; /* ADD cube of shortest path */
115 DdNode *constN; /* value returned by evaluation of ADD */
116 DdNode *ycube; /* cube of the negated y vars for c-proj */
117 DdNode *CP; /* C-Projection of C */
118 DdNode *CPr; /* C-Selection of C */
119 int length; /* length of the shortest path */
120 int nx; /* number of variables */
121 int ny;
122 int maxnx;
123 int maxny;
124 int m;
125 int n;
126 int N;
127 int cmu; /* use CMU multiplication */
128 int pr; /* verbose printout level */
129 int harwell;
130 int multiple; /* read multiple matrices */
131 int ok;
132 int approach; /* reordering approach */
133 int autodyn; /* automatic reordering */
134 int groupcheck; /* option for group sifting */
135 int profile; /* print heap and cache profile if != 0 */
136 int keepperm; /* keep track of permutation */
137 int clearcache; /* clear the cache after each matrix */
138 int blifOrDot; /* dump format: 0 -> dot, 1 -> blif, ... */
139 int retval; /* return value */
140 int i; /* loop index */
141 unsigned long startTime; /* initial time */
142 unsigned long lapTime = 0;
143 int size;
144 unsigned int cacheSize, maxMemory;
145 unsigned int nvars,nslots;
146 int optidx;
147
148 startTime = util_cpu_time();
149
150 approach = CUDD_REORDER_NONE;
151 autodyn = 0;
152 pr = 0;
153 harwell = 0;
154 multiple = 0;
155 profile = 0;
156 keepperm = 0;
157 cmu = 0;
158 N = 4;
159 nvars = 4;
160 cacheSize = 2048;
161 maxMemory = 0;
162 nslots = CUDD_UNIQUE_SLOTS;
163 clearcache = 0;
164 groupcheck = CUDD_GROUP_CHECK7;
165 dfile = NULL;
166 blifOrDot = 0; /* dot format */
167
168 /* Parse command line. */
169 for (optidx = 1; optidx < argc; optidx++) {
170 if (argv[optidx][0] == '-') {
171 switch(argv[optidx][1]) {
172 case 'C':
173 cmu = 1;
174 break;
175 case 'D':
176 autodyn = 1;
177 break;
178 case 'H':
179 harwell = 1;
180 break;
181 case 'M':
182 /* NOOP: retained for backward compatibility. */
183 break;
184 case 'P':
185 profile = 1;
186 break;
187 case 'S':
188 if (++optidx == argc) usage(argv[0]);
189 nslots = atoi(argv[optidx]);
190 break;
191 case 'X':
192 if (++optidx == argc) usage(argv[0]);
193 maxMemory = atoi(argv[optidx]);
194 break;
195 case 'a':
196 if (++optidx == argc) usage(argv[0]);
197 approach = atoi(argv[optidx]);
198 break;
199 case 'b':
200 blifOrDot = 1; /* blif format */
201 break;
202 case 'c':
203 clearcache = 1;
204 break;
205 case 'd':
206 if (++optidx == argc) usage(argv[0]);
207 dfile = argv[optidx];
208 break;
209 case 'g':
210 if (++optidx == argc) usage(argv[0]);
211 groupcheck = atoi(argv[optidx]);
212 break;
213 case 'k':
214 keepperm = 1;
215 break;
216 case 'm':
217 multiple = 1;
218 break;
219 case 'n':
220 if (++optidx == argc) usage(argv[0]);
221 N = atoi(argv[optidx]);
222 break;
223 case 'p':
224 if (++optidx == argc) usage(argv[0]);
225 pr = atoi(argv[optidx]);
226 break;
227 case 'v':
228 if (++optidx == argc) usage(argv[0]);
229 nvars = atoi(argv[optidx]);
230 break;
231 case 'x':
232 if (++optidx == argc) usage(argv[0]);
233 cacheSize = atoi(argv[optidx]);
234 break;
235 case 'h':
236 default:
237 usage(argv[0]);
238 break;
239 }
240 } else if (argc - optidx == 1) {
241 file = argv[optidx];
242 } else {
243 usage(argv[0]);
244 }
245 }
246
247 if ((approach<0) || (approach>17)) {
248 (void) fprintf(stderr,"Invalid approach: %d \n",approach);
249 usage(argv[0]);
250 }
251
252 if (pr > 0) {
253 (void) printf("# %s\n", TESTCUDD_VERSION);
254 /* Echo command line and arguments. */
255 (void) printf("#");
256 for (i = 0; i < argc; i++) {
257 (void) printf(" %s", argv[i]);
258 }
259 (void) printf("\n");
260 (void) fflush(stdout);
261 }
262
263 /* Initialize manager and provide easy reference to terminals. */
264 dd = Cudd_Init(nvars,0,nslots,cacheSize,maxMemory);
265 one = DD_ONE(dd);
266 dd->groupcheck = (Cudd_AggregationType) groupcheck;
267 if (autodyn) Cudd_AutodynEnable(dd,CUDD_REORDER_SAME);
268
269 /* Open input file. */
270 fp = open_file(file, "r");
271
272 /* Open dump file if requested */
273 if (dfile != NULL) {
274 dfp = open_file(dfile, "w");
275 }
276
277 x = y = xn = yn_ = NULL;
278 do {
279 /* We want to start anew for every matrix. */
280 maxnx = maxny = 0;
281 nx = maxnx; ny = maxny;
282 if (pr>0) lapTime = util_cpu_time();
283 if (harwell) {
284 if (pr > 0) (void) printf(":name: ");
285 ok = Cudd_addHarwell(fp, dd, &M, &x, &y, &xn, &yn_, &nx, &ny,
286 &m, &n, 0, 2, 1, 2, pr);
287 } else {
288 ok = Cudd_addRead(fp, dd, &M, &x, &y, &xn, &yn_, &nx, &ny,
289 &m, &n, 0, 2, 1, 2);
290 if (pr > 0)
291 (void) printf(":name: %s: %d rows %d columns\n", file, m, n);
292 }
293 if (!ok) {
294 (void) fprintf(stderr, "Error reading matrix\n");
295 return(1);
296 }
297
298 if (nx > maxnx) maxnx = nx;
299 if (ny > maxny) maxny = ny;
300
301 /* Build cube of negated y's. */
302 ycube = DD_ONE(dd);
303 Cudd_Ref(ycube);
304 for (i = maxny - 1; i >= 0; i--) {
305 DdNode *tmpp;
306 tmpp = Cudd_bddAnd(dd,Cudd_Not(dd->vars[y[i]->index]),ycube);
307 if (tmpp == NULL) return(2);
308 Cudd_Ref(tmpp);
309 Cudd_RecursiveDeref(dd,ycube);
310 ycube = tmpp;
311 }
312 /* Initialize vectors of BDD variables used by priority func. */
313 xvars = ALLOC(DdNode *, nx);
314 if (xvars == NULL) return(2);
315 for (i = 0; i < nx; i++) {
316 xvars[i] = dd->vars[x[i]->index];
317 }
318 yvars = ALLOC(DdNode *, ny);
319 if (yvars == NULL) return(2);
320 for (i = 0; i < ny; i++) {
321 yvars[i] = dd->vars[y[i]->index];
322 }
323
324 /* Clean up */
325 for (i=0; i < maxnx; i++) {
326 Cudd_RecursiveDeref(dd, x[i]);
327 Cudd_RecursiveDeref(dd, xn[i]);
328 }
329 FREE(x);
330 FREE(xn);
331 for (i=0; i < maxny; i++) {
332 Cudd_RecursiveDeref(dd, y[i]);
333 Cudd_RecursiveDeref(dd, yn_[i]);
334 }
335 FREE(y);
336 FREE(yn_);
337
338 if (pr>0) {(void) printf(":1: M"); Cudd_PrintDebug(dd,M,nx+ny,pr);}
339
340 if (pr>0) (void) printf(":2: time to read the matrix = %s\n",
341 util_print_time(util_cpu_time() - lapTime));
342
343 C = Cudd_addBddPattern(dd, M);
344 if (C == 0) return(2);
345 Cudd_Ref(C);
346 if (pr>0) {(void) printf(":3: C"); Cudd_PrintDebug(dd,C,nx+ny,pr);}
347
348 /* Test iterators. */
349 retval = testIterators(dd,M,C,pr);
350 if (retval == 0) return(2);
351
352 if (profile != 0 && pr > 0)
353 cuddCacheProfile(dd,stdout);
354
355 /* Test XOR */
356 retval = testXor(dd,C,pr,nx+ny);
357 if (retval == 0) return(2);
358
359 /* Test Hamming distance functions. */
360 retval = testHamming(dd,C,pr);
361 if (retval == 0) return(2);
362
363 /* Test selection functions. */
364 CP = Cudd_CProjection(dd,C,ycube);
365 if (CP == NULL) return(2);
366 Cudd_Ref(CP);
367 if (pr>0) {(void) printf("ycube"); Cudd_PrintDebug(dd,ycube,nx+ny,pr);}
368 if (pr>0) {(void) printf("CP"); Cudd_PrintDebug(dd,CP,nx+ny,pr);}
369
370 if (nx == ny) {
371 CPr = Cudd_PrioritySelect(dd,C,xvars,yvars,(DdNode **)NULL,
372 (DdNode *)NULL,ny,Cudd_Xgty);
373 if (CPr == NULL) return(2);
374 Cudd_Ref(CPr);
375 if (pr>0) {(void) printf(":4: CPr"); Cudd_PrintDebug(dd,CPr,nx+ny,pr);}
376 if (CP != CPr) {
377 (void) printf("CP != CPr!\n");
378 }
379 Cudd_RecursiveDeref(dd, CPr);
380 }
381
382 /* Test inequality generator. */
383 {
384 int Nmin = ddMin(nx,ny);
385 int q;
386 DdGen *gen;
387 int *cube;
388 DdNode *f = Cudd_Inequality(dd,Nmin,2,xvars,yvars);
389 if (f == NULL) return(2);
390 Cudd_Ref(f);
391 if (pr>0) {
392 (void) printf(":4: ineq");
393 Cudd_PrintDebug(dd,f,nx+ny,pr);
394 if (pr>1) {
395 Cudd_ForeachPrime(dd,Cudd_Not(f),Cudd_Not(f),gen,cube) {
396 for (q = 0; q < dd->size; q++) {
397 switch (cube[q]) {
398 case 0:
399 (void) printf("1");
400 break;
401 case 1:
402 (void) printf("0");
403 break;
404 case 2:
405 (void) printf("-");
406 break;
407 default:
408 (void) printf("?");
409 }
410 }
411 (void) printf(" 1\n");
412 }
413 (void) printf("\n");
414 }
415 }
416 Cudd_IterDerefBdd(dd, f);
417 }
418 FREE(xvars); FREE(yvars);
419
420 Cudd_RecursiveDeref(dd, CP);
421
422 /* Test functions for essential variables. */
423 ess = Cudd_FindEssential(dd,C);
424 if (ess == NULL) return(2);
425 Cudd_Ref(ess);
426 if (pr>0) {(void) printf(":4: ess"); Cudd_PrintDebug(dd,ess,nx+ny,pr);}
427 Cudd_RecursiveDeref(dd, ess);
428
429 /* Test functions for shortest paths. */
430 shortP = Cudd_ShortestPath(dd, M, NULL, NULL, &length);
431 if (shortP == NULL) return(2);
432 Cudd_Ref(shortP);
433 if (pr>0) {
434 (void) printf(":5: shortP"); Cudd_PrintDebug(dd,shortP,nx+ny,pr);
435 }
436 /* Test functions for largest cubes. */
437 largest = Cudd_LargestCube(dd, Cudd_Not(C), &length);
438 if (largest == NULL) return(2);
439 Cudd_Ref(largest);
440 if (pr>0) {
441 (void) printf(":5b: largest");
442 Cudd_PrintDebug(dd,largest,nx+ny,pr);
443 }
444 Cudd_RecursiveDeref(dd, largest);
445
446 /* Test Cudd_addEvalConst and Cudd_addIteConstant. */
447 shortA = Cudd_BddToAdd(dd,shortP);
448 if (shortA == NULL) return(2);
449 Cudd_Ref(shortA);
450 Cudd_RecursiveDeref(dd, shortP);
451 constN = Cudd_addEvalConst(dd,shortA,M);
452 if (constN == DD_NON_CONSTANT) return(2);
453 if (Cudd_addIteConstant(dd,shortA,M,constN) != constN) return(2);
454 if (pr>0) {(void) printf("The value of M along the chosen shortest path is %g\n", cuddV(constN));}
455 Cudd_RecursiveDeref(dd, shortA);
456
457 shortP = Cudd_ShortestPath(dd, C, NULL, NULL, &length);
458 if (shortP == NULL) return(2);
459 Cudd_Ref(shortP);
460 if (pr>0) {
461 (void) printf(":6: shortP"); Cudd_PrintDebug(dd,shortP,nx+ny,pr);
462 }
463
464 /* Test Cudd_bddIteConstant and Cudd_bddLeq. */
465 if (!Cudd_bddLeq(dd,shortP,C)) return(2);
466 if (Cudd_bddIteConstant(dd,Cudd_Not(shortP),one,C) != one) return(2);
467 Cudd_RecursiveDeref(dd, shortP);
468
469 /* Experiment with support functions. */
470 if (!testSupport(dd,M,ycube,pr)) {
471 return(2);
472 }
473 Cudd_RecursiveDeref(dd, ycube);
474
475 if (profile) {
476 retval = cuddHeapProfile(dd);
477 if (retval == 0) {
478 (void) fprintf(stderr,"Error reported by cuddHeapProfile\n");
479 return(2);
480 }
481 }
482
483 size = dd->size;
484
485 if (pr>0) {
486 (void) printf("Average distance: %g\n", Cudd_AverageDistance(dd));
487 }
488
489 /* Reorder if so requested. */
490 if (approach != CUDD_REORDER_NONE) {
491 #ifndef DD_STATS
492 retval = Cudd_EnableReorderingReporting(dd);
493 if (retval == 0) {
494 (void) fprintf(stderr,"Error reported by Cudd_EnableReorderingReporting\n");
495 return(3);
496 }
497 #endif
498 #ifdef DD_DEBUG
499 retval = Cudd_DebugCheck(dd);
500 if (retval != 0) {
501 (void) fprintf(stderr,"Error reported by Cudd_DebugCheck\n");
502 return(3);
503 }
504 retval = Cudd_CheckKeys(dd);
505 if (retval != 0) {
506 (void) fprintf(stderr,"Error reported by Cudd_CheckKeys\n");
507 return(3);
508 }
509 #endif
510 retval = Cudd_ReduceHeap(dd,(Cudd_ReorderingType)approach,5);
511 if (retval == 0) {
512 (void) fprintf(stderr,"Error reported by Cudd_ReduceHeap\n");
513 return(3);
514 }
515 #ifndef DD_STATS
516 retval = Cudd_DisableReorderingReporting(dd);
517 if (retval == 0) {
518 (void) fprintf(stderr,"Error reported by Cudd_DisableReorderingReporting\n");
519 return(3);
520 }
521 #endif
522 #ifdef DD_DEBUG
523 retval = Cudd_DebugCheck(dd);
524 if (retval != 0) {
525 (void) fprintf(stderr,"Error reported by Cudd_DebugCheck\n");
526 return(3);
527 }
528 retval = Cudd_CheckKeys(dd);
529 if (retval != 0) {
530 (void) fprintf(stderr,"Error reported by Cudd_CheckKeys\n");
531 return(3);
532 }
533 #endif
534 if (approach == CUDD_REORDER_SYMM_SIFT ||
535 approach == CUDD_REORDER_SYMM_SIFT_CONV) {
536 Cudd_SymmProfile(dd,0,dd->size-1);
537 }
538
539 if (pr>0) {
540 (void) printf("Average distance: %g\n", Cudd_AverageDistance(dd));
541 }
542
543 if (keepperm) {
544 /* Print variable permutation. */
545 (void) printf("Variable Permutation:");
546 for (i=0; i<size; i++) {
547 if (i%20 == 0) (void) printf("\n");
548 (void) printf("%d ", dd->invperm[i]);
549 }
550 (void) printf("\n");
551 (void) printf("Inverse Permutation:");
552 for (i=0; i<size; i++) {
553 if (i%20 == 0) (void) printf("\n");
554 (void) printf("%d ", dd->perm[i]);
555 }
556 (void) printf("\n");
557 }
558
559 if (pr>0) {(void) printf("M"); Cudd_PrintDebug(dd,M,nx+ny,pr);}
560
561 if (profile) {
562 retval = cuddHeapProfile(dd);
563 if (retval == 0) {
564 (void) fprintf(stderr,"Error reported by cuddHeapProfile\n");
565 return(2);
566 }
567 }
568
569 }
570
571 /* Dump DDs of C and M if so requested. */
572 if (dfile != NULL) {
573 dfunc[0] = C;
574 dfunc[1] = M;
575 if (blifOrDot == 1) {
576 /* Only dump C because blif cannot handle ADDs */
577 retval = Cudd_DumpBlif(dd,1,dfunc,NULL,
578 (char const * const *)onames,NULL,dfp,0);
579 } else {
580 retval = Cudd_DumpDot(dd,2,dfunc,NULL,
581 (char const * const *)onames,dfp);
582 }
583 if (retval != 1) {
584 (void) fprintf(stderr,"abnormal termination\n");
585 return(2);
586 }
587 }
588
589 Cudd_RecursiveDeref(dd, C);
590 Cudd_RecursiveDeref(dd, M);
591
592 if (clearcache) {
593 if (pr>0) {(void) printf("Clearing the cache... ");}
594 for (i = dd->cacheSlots - 1; i>=0; i--) {
595 dd->cache[i].data = NULL;
596 }
597 if (pr>0) {(void) printf("done\n");}
598 }
599 if (pr>0) {
600 (void) printf("Number of variables = %6d\t",dd->size);
601 (void) printf("Number of slots = %6u\n",dd->slots);
602 (void) printf("Number of keys = %6u\t",dd->keys);
603 (void) printf("Number of min dead = %6u\n",dd->minDead);
604 }
605
606 } while (multiple && !feof(fp));
607
608 fclose(fp);
609 if (dfile != NULL) {
610 fclose(dfp);
611 }
612
613 /* Second phase: experiment with Walsh matrices. */
614 if (!testWalsh(dd,N,cmu,approach,pr)) {
615 return(2);
616 }
617
618 /* Check variable destruction. */
619 assert(cuddDestroySubtables(dd,3));
620 if (pr == 0) {
621 savefp = Cudd_ReadStdout(dd);
622 Cudd_SetStdout(dd,fopen("/dev/null","a"));
623 }
624 assert(Cudd_DebugCheck(dd) == 0);
625 assert(Cudd_CheckKeys(dd) == 0);
626 if (pr == 0) {
627 fclose(Cudd_ReadStdout(dd));
628 Cudd_SetStdout(dd,savefp);
629 }
630
631 retval = Cudd_CheckZeroRef(dd);
632 ok = retval != 0; /* ok == 0 means O.K. */
633 if (retval != 0) {
634 (void) fprintf(stderr,
635 "%d non-zero DD reference counts after dereferencing\n", retval);
636 }
637
638 if (pr > 0) {
639 (void) Cudd_PrintInfo(dd,stdout);
640 }
641
642 Cudd_Quit(dd);
643
644 if (pr>0) (void) printf("total time = %s\n",
645 util_print_time(util_cpu_time() - startTime));
646
647 if (pr > 0) util_print_cpu_stats(stdout);
648 return ok;
649
650 } /* end of main */
651
652
653 /*---------------------------------------------------------------------------*/
654 /* Definition of static functions */
655 /*---------------------------------------------------------------------------*/
656
657
658 /**
659 @brief Prints usage info for testcudd.
660
661 @sideeffect None
662
663 */
664 static void
usage(char * prog)665 usage(char *prog)
666 {
667 (void) fprintf(stderr, "usage: %s [options] [file]\n", prog);
668 (void) fprintf(stderr, " -C\t\tuse CMU multiplication algorithm\n");
669 (void) fprintf(stderr, " -D\t\tenable automatic dynamic reordering\n");
670 (void) fprintf(stderr, " -H\t\tread matrix in Harwell format\n");
671 (void) fprintf(stderr, " -P\t\tprint BDD heap and cache profile\n");
672 (void) fprintf(stderr, " -S n\t\tnumber of slots for each subtable\n");
673 (void) fprintf(stderr, " -X n\t\ttarget maximum memory in bytes\n");
674 (void) fprintf(stderr, " -a n\t\tchoose reordering approach (0-13)\n");
675 (void) fprintf(stderr, " \t\t\t0: same as autoMethod\n");
676 (void) fprintf(stderr, " \t\t\t1: no reordering (default)\n");
677 (void) fprintf(stderr, " \t\t\t2: random\n");
678 (void) fprintf(stderr, " \t\t\t3: pivot\n");
679 (void) fprintf(stderr, " \t\t\t4: sifting\n");
680 (void) fprintf(stderr, " \t\t\t5: sifting to convergence\n");
681 (void) fprintf(stderr, " \t\t\t6: symmetric sifting\n");
682 (void) fprintf(stderr, " \t\t\t7: symmetric sifting to convergence\n");
683 (void) fprintf(stderr, " \t\t\t8-10: window of size 2-4\n");
684 (void) fprintf(stderr, " \t\t\t11-13: window of size 2-4 to conv.\n");
685 (void) fprintf(stderr, " \t\t\t14: group sifting\n");
686 (void) fprintf(stderr, " \t\t\t15: group sifting to convergence\n");
687 (void) fprintf(stderr, " \t\t\t16: simulated annealing\n");
688 (void) fprintf(stderr, " \t\t\t17: genetic algorithm\n");
689 (void) fprintf(stderr, " -b\t\tuse blif as format for dumps\n");
690 (void) fprintf(stderr, " -c\t\tclear the cache after each matrix\n");
691 (void) fprintf(stderr, " -d file\tdump DDs to file\n");
692 (void) fprintf(stderr, " -g\t\tselect aggregation criterion (0,5,7)\n");
693 (void) fprintf(stderr, " -h\t\tprints this message\n");
694 (void) fprintf(stderr, " -k\t\tprint the variable permutation\n");
695 (void) fprintf(stderr, " -m\t\tread multiple matrices (only with -H)\n");
696 (void) fprintf(stderr, " -n n\t\tnumber of variables\n");
697 (void) fprintf(stderr, " -p n\t\tcontrol verbosity\n");
698 (void) fprintf(stderr, " -v n\t\tinitial variables in the unique table\n");
699 (void) fprintf(stderr, " -x n\t\tinitial size of the cache\n");
700 exit(2);
701 } /* end of usage */
702
703
704 /**
705 @brief Opens a file.
706
707 @details Opens a file, or fails with an error message and exits.
708 Allows '-' as a synonym for standard input.
709
710 @sideeffect None
711
712 */
713 static FILE *
open_file(char * filename,const char * mode)714 open_file(char *filename, const char *mode)
715 {
716 FILE *fp;
717
718 if (strcmp(filename, "-") == 0) {
719 return mode[0] == 'r' ? stdin : stdout;
720 } else if ((fp = fopen(filename, mode)) == NULL) {
721 perror(filename);
722 exit(1);
723 }
724 return fp;
725
726 } /* end of open_file */
727
728
729 /**
730 @brief Tests Walsh matrix multiplication.
731
732 @return 1 if successful; 0 otherwise.
733
734 @sideeffect May create new variables in the manager.
735
736 */
737 static int
testWalsh(DdManager * dd,int N,int cmu,int approach,int pr)738 testWalsh(
739 DdManager *dd /* manager */,
740 int N /* number of variables */,
741 int cmu /* use CMU approach to matrix multiplication */,
742 int approach /* reordering approach */,
743 int pr /* verbosity level */)
744 {
745 DdNode *walsh1, *walsh2, *wtw;
746 DdNode **x, **v, **z;
747 int i, retval;
748 DdNode *one = DD_ONE(dd);
749 DdNode *zero = DD_ZERO(dd);
750
751 if (N > 3) {
752 x = ALLOC(DdNode *,N);
753 v = ALLOC(DdNode *,N);
754 z = ALLOC(DdNode *,N);
755
756 for (i = N-1; i >= 0; i--) {
757 Cudd_Ref(x[i]=cuddUniqueInter(dd,3*i,one,zero));
758 Cudd_Ref(v[i]=cuddUniqueInter(dd,3*i+1,one,zero));
759 Cudd_Ref(z[i]=cuddUniqueInter(dd,3*i+2,one,zero));
760 }
761 Cudd_Ref(walsh1 = Cudd_addWalsh(dd,v,z,N));
762 if (pr>0) {(void) printf("walsh1"); Cudd_PrintDebug(dd,walsh1,2*N,pr);}
763 Cudd_Ref(walsh2 = Cudd_addWalsh(dd,x,v,N));
764 if (cmu) {
765 Cudd_Ref(wtw = Cudd_addTimesPlus(dd,walsh2,walsh1,v,N));
766 } else {
767 Cudd_Ref(wtw = Cudd_addMatrixMultiply(dd,walsh2,walsh1,v,N));
768 }
769 if (pr>0) {(void) printf("wtw"); Cudd_PrintDebug(dd,wtw,2*N,pr);}
770
771 if (approach != CUDD_REORDER_NONE) {
772 #ifdef DD_DEBUG
773 retval = Cudd_DebugCheck(dd);
774 if (retval != 0) {
775 (void) fprintf(stderr,"Error reported by Cudd_DebugCheck\n");
776 return(0);
777 }
778 #endif
779 retval = Cudd_ReduceHeap(dd,(Cudd_ReorderingType)approach,5);
780 if (retval == 0) {
781 (void) fprintf(stderr,"Error reported by Cudd_ReduceHeap\n");
782 return(0);
783 }
784 #ifdef DD_DEBUG
785 retval = Cudd_DebugCheck(dd);
786 if (retval != 0) {
787 (void) fprintf(stderr,"Error reported by Cudd_DebugCheck\n");
788 return(0);
789 }
790 #endif
791 if (approach == CUDD_REORDER_SYMM_SIFT ||
792 approach == CUDD_REORDER_SYMM_SIFT_CONV) {
793 Cudd_SymmProfile(dd,0,dd->size-1);
794 }
795 }
796 /* Clean up. */
797 Cudd_RecursiveDeref(dd, wtw);
798 Cudd_RecursiveDeref(dd, walsh1);
799 Cudd_RecursiveDeref(dd, walsh2);
800 for (i=0; i < N; i++) {
801 Cudd_RecursiveDeref(dd, x[i]);
802 Cudd_RecursiveDeref(dd, v[i]);
803 Cudd_RecursiveDeref(dd, z[i]);
804 }
805 FREE(x);
806 FREE(v);
807 FREE(z);
808 }
809 return(1);
810
811 } /* end of testWalsh */
812
813 /**
814 @brief Tests iterators on cubes and nodes.
815
816 @sideeffect None
817
818 */
819 static int
testIterators(DdManager * dd,DdNode * M,DdNode * C,int pr)820 testIterators(
821 DdManager *dd,
822 DdNode *M,
823 DdNode *C,
824 int pr)
825 {
826 int *cube;
827 CUDD_VALUE_TYPE value;
828 DdGen *gen;
829 int q;
830
831 /* Test iterator for cubes. */
832 if (pr>1) {
833 (void) printf("Testing iterator on cubes:\n");
834 Cudd_ForeachCube(dd,M,gen,cube,value) {
835 for (q = 0; q < dd->size; q++) {
836 switch (cube[q]) {
837 case 0:
838 (void) printf("0");
839 break;
840 case 1:
841 (void) printf("1");
842 break;
843 case 2:
844 (void) printf("-");
845 break;
846 default:
847 (void) printf("?");
848 }
849 }
850 (void) printf(" %g\n",value);
851 }
852 (void) printf("\n");
853 }
854
855 if (pr>1) {
856 (void) printf("Testing prime expansion of cubes:\n");
857 if (!Cudd_bddPrintCover(dd,C,C)) return(0);
858 }
859
860 if (pr>1) {
861 (void) printf("Testing iterator on primes (CNF):\n");
862 Cudd_ForeachPrime(dd,Cudd_Not(C),Cudd_Not(C),gen,cube) {
863 for (q = 0; q < dd->size; q++) {
864 switch (cube[q]) {
865 case 0:
866 (void) printf("1");
867 break;
868 case 1:
869 (void) printf("0");
870 break;
871 case 2:
872 (void) printf("-");
873 break;
874 default:
875 (void) printf("?");
876 }
877 }
878 (void) printf(" 1\n");
879 }
880 (void) printf("\n");
881 }
882
883 /* Test iterator on nodes. */
884 if (pr>2) {
885 DdNode *node;
886 (void) printf("Testing iterator on nodes:\n");
887 Cudd_ForeachNode(dd,M,gen,node) {
888 if (Cudd_IsConstant(node)) {
889 (void) printf("ID = 0x%"PRIxPTR"\tvalue = %-9g\n",
890 (ptruint) node / (ptruint) sizeof(DdNode),
891 Cudd_V(node));
892 } else {
893 (void) printf("ID = 0x%"PRIxPTR"\tindex = %u\tr = %u\n",
894 (ptruint) node / (ptruint) sizeof(DdNode),
895 node->index, node->ref);
896 }
897 }
898 (void) printf("\n");
899 }
900 return(1);
901
902 } /* end of testIterators */
903
904
905 /**
906 @brief Tests the functions related to the exclusive OR.
907
908 @details Builds the boolean difference of the given function in
909 three different ways and checks that the results is the same.
910
911 @return 1 if successful; 0 otherwise.
912
913 @sideeffect None
914
915 */
916 static int
testXor(DdManager * dd,DdNode * f,int pr,int nvars)917 testXor(DdManager *dd, DdNode *f, int pr, int nvars)
918 {
919 DdNode *f1, *f0, *res1, *res2;
920 int x;
921
922 /* Extract cofactors w.r.t. mid variable. */
923 x = nvars / 2;
924 f1 = Cudd_Cofactor(dd,f,dd->vars[x]);
925 if (f1 == NULL) return(0);
926 Cudd_Ref(f1);
927
928 f0 = Cudd_Cofactor(dd,f,Cudd_Not(dd->vars[x]));
929 if (f0 == NULL) {
930 Cudd_RecursiveDeref(dd,f1);
931 return(0);
932 }
933 Cudd_Ref(f0);
934
935 /* Compute XOR of cofactors with ITE. */
936 res1 = Cudd_bddIte(dd,f1,Cudd_Not(f0),f0);
937 if (res1 == NULL) return(0);
938 Cudd_Ref(res1);
939
940 if (pr>0) {(void) printf("xor1"); Cudd_PrintDebug(dd,res1,nvars,pr);}
941
942 /* Compute XOR of cofactors with XOR. */
943 res2 = Cudd_bddXor(dd,f1,f0);
944 if (res2 == NULL) {
945 Cudd_RecursiveDeref(dd,res1);
946 return(0);
947 }
948 Cudd_Ref(res2);
949
950 if (res1 != res2) {
951 if (pr>0) {(void) printf("xor2"); Cudd_PrintDebug(dd,res2,nvars,pr);}
952 Cudd_RecursiveDeref(dd,res1);
953 Cudd_RecursiveDeref(dd,res2);
954 return(0);
955 }
956 Cudd_RecursiveDeref(dd,res1);
957 Cudd_RecursiveDeref(dd,f1);
958 Cudd_RecursiveDeref(dd,f0);
959
960 /* Compute boolean difference directly. */
961 res1 = Cudd_bddBooleanDiff(dd,f,x);
962 if (res1 == NULL) {
963 Cudd_RecursiveDeref(dd,res2);
964 return(0);
965 }
966 Cudd_Ref(res1);
967
968 if (res1 != res2) {
969 if (pr>0) {(void) printf("xor3"); Cudd_PrintDebug(dd,res1,nvars,pr);}
970 Cudd_RecursiveDeref(dd,res1);
971 Cudd_RecursiveDeref(dd,res2);
972 return(0);
973 }
974 Cudd_RecursiveDeref(dd,res1);
975 Cudd_RecursiveDeref(dd,res2);
976 return(1);
977
978 } /* end of testXor */
979
980
981 /**
982 @brief Tests the Hamming distance functions.
983
984 @return 1 if successful; 0 otherwise.
985
986 @sideeffect None
987
988 */
989 static int
testHamming(DdManager * dd,DdNode * f,int pr)990 testHamming(
991 DdManager *dd,
992 DdNode *f,
993 int pr)
994 {
995 DdNode **vars, *minBdd, *zero, *scan;
996 int i;
997 int d;
998 int *minterm;
999 int size = Cudd_ReadSize(dd);
1000
1001 vars = ALLOC(DdNode *, size);
1002 if (vars == NULL) return(0);
1003 for (i = 0; i < size; i++) {
1004 vars[i] = Cudd_bddIthVar(dd,i);
1005 }
1006
1007 minBdd = Cudd_bddPickOneMinterm(dd,Cudd_Not(f),vars,size);
1008 Cudd_Ref(minBdd);
1009 if (pr > 0) {
1010 (void) printf("Chosen minterm for Hamming distance test: ");
1011 Cudd_PrintDebug(dd,minBdd,size,pr);
1012 }
1013
1014 minterm = ALLOC(int,size);
1015 if (minterm == NULL) {
1016 FREE(vars);
1017 Cudd_RecursiveDeref(dd,minBdd);
1018 return(0);
1019 }
1020 scan = minBdd;
1021 zero = Cudd_Not(DD_ONE(dd));
1022 while (!Cudd_IsConstant(scan)) {
1023 DdNode *R = Cudd_Regular(scan);
1024 DdNode *T = Cudd_T(R);
1025 DdNode *E = Cudd_E(R);
1026 if (R != scan) {
1027 T = Cudd_Not(T);
1028 E = Cudd_Not(E);
1029 }
1030 if (T == zero) {
1031 minterm[R->index] = 0;
1032 scan = E;
1033 } else {
1034 minterm[R->index] = 1;
1035 scan = T;
1036 }
1037 }
1038 Cudd_RecursiveDeref(dd,minBdd);
1039
1040 d = Cudd_MinHammingDist(dd,f,minterm,size);
1041
1042 if (pr > 0)
1043 (void) printf("Minimum Hamming distance = %d\n", d);
1044
1045 FREE(vars);
1046 FREE(minterm);
1047 return(1);
1048
1049 } /* end of testHamming */
1050
1051
1052 /**
1053 @brief Tests the support functions.
1054
1055 @return 1 if successful; 0 otherwise.
1056
1057 @sideeffect None
1058
1059 */
1060 static int
testSupport(DdManager * dd,DdNode * f,DdNode * g,int pr)1061 testSupport(
1062 DdManager *dd,
1063 DdNode *f,
1064 DdNode *g,
1065 int pr)
1066 {
1067 DdNode *sb, *common, *onlyF, *onlyG;
1068 DdNode *F[2];
1069 int *support;
1070 int ret, ssize;
1071 int size = Cudd_ReadSize(dd);
1072
1073 sb = Cudd_Support(dd, f);
1074 if (sb == NULL) return(0);
1075 Cudd_Ref(sb);
1076 if (pr > 0) {
1077 (void) printf("Support of f: ");
1078 Cudd_PrintDebug(dd,sb,size,pr);
1079 }
1080 Cudd_RecursiveDeref(dd, sb);
1081
1082 ssize = Cudd_SupportIndices(dd, f, &support);
1083 if (ssize == CUDD_OUT_OF_MEM) return(0);
1084 if (pr > 0) {
1085 (void) printf("Size of the support of f: %d\n", ssize);
1086 }
1087 FREE(support);
1088
1089 ssize = Cudd_SupportSize(dd, f);
1090 if (pr > 0) {
1091 (void) printf("Size of the support of f: %d\n", ssize);
1092 }
1093
1094 F[0] = f;
1095 F[1] = g;
1096 sb = Cudd_VectorSupport(dd, F, 2);
1097 if (sb == NULL) return(0);
1098 Cudd_Ref(sb);
1099 if (pr > 0) {
1100 (void) printf("Support of f and g: ");
1101 Cudd_PrintDebug(dd,sb,size,pr);
1102 }
1103 Cudd_RecursiveDeref(dd, sb);
1104
1105 ssize = Cudd_VectorSupportIndices(dd, F, 2, &support);
1106 if (ssize == CUDD_OUT_OF_MEM) return(0);
1107 if (pr > 0) {
1108 (void) printf("Size of the support of f and g: %d\n", ssize);
1109 }
1110 FREE(support);
1111
1112 ssize = Cudd_VectorSupportSize(dd, F, 2);
1113 if (pr > 0) {
1114 (void) printf("Size of the support of f and g: %d\n", ssize);
1115 }
1116
1117 ret = Cudd_ClassifySupport(dd, f, g, &common, &onlyF, &onlyG);
1118 if (ret == 0) return(0);
1119 Cudd_Ref(common); Cudd_Ref(onlyF); Cudd_Ref(onlyG);
1120 if (pr > 0) {
1121 (void) printf("Support common to f and g: ");
1122 Cudd_PrintDebug(dd,common,size,pr);
1123 (void) printf("Support private to f: ");
1124 Cudd_PrintDebug(dd,onlyF,size,pr);
1125 (void) printf("Support private to g: ");
1126 Cudd_PrintDebug(dd,onlyG,size,pr);
1127 }
1128 Cudd_RecursiveDeref(dd, common);
1129 Cudd_RecursiveDeref(dd, onlyF);
1130 Cudd_RecursiveDeref(dd, onlyG);
1131
1132 return(1);
1133
1134 } /* end of testSupport */
1135