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