?  search:
summary | log | graphiclog1 | graphiclog2 | commit | commitdiff | tree | refs | edit | fork
blame | history | raw | HEAD
emergency commit
[cl-cudd.git] / distr / cudd / testcudd.c
blob0b5adf97fa7fee3bcbbf45960cee125a93a23bfa
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-2004, 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.20 2009/03/08 02:49:02 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
86 /**AutomaticEnd***************************************************************/
87
88
89 /**Function********************************************************************
90
91 Synopsis [Main function for testcudd.]
92
93 Description []
94
95 SideEffects [None]
96
97 SeeAlso []
98
99 ******************************************************************************/
100 int
101 main(int argc, char **argv)
102 {
103 FILE *fp; /* pointer to input file */
104 char *file = (char *) ""; /* input file name */
105 FILE *dfp = NULL; /* pointer to dump file */
106 char *dfile; /* file for DD dump */
107 DdNode *dfunc[2]; /* addresses of the functions to be dumped */
108 DdManager *dd; /* pointer to DD manager */
109 DdNode *one; /* fast access to constant function */
110 DdNode *M;
111 DdNode **x; /* pointers to variables */
112 DdNode **y; /* pointers to variables */
113 DdNode **xn; /* complements of row variables */
114 DdNode **yn_; /* complements of column variables */
115 DdNode **xvars;
116 DdNode **yvars;
117 DdNode *C; /* result of converting from ADD to BDD */
118 DdNode *ess; /* cube of essential variables */
119 DdNode *shortP; /* BDD cube of shortest path */
120 DdNode *largest; /* BDD of largest cube */
121 DdNode *shortA; /* ADD cube of shortest path */
122 DdNode *constN; /* value returned by evaluation of ADD */
123 DdNode *ycube; /* cube of the negated y vars for c-proj */
124 DdNode *CP; /* C-Projection of C */
125 DdNode *CPr; /* C-Selection of C */
126 int length; /* length of the shortest path */
127 int nx; /* number of variables */
128 int ny;
129 int maxnx;
130 int maxny;
131 int m;
132 int n;
133 int N;
134 int cmu; /* use CMU multiplication */
135 int pr; /* verbose printout level */
136 int harwell;
137 int multiple; /* read multiple matrices */
138 int ok;
139 int c; /* variable to read in options */
140 int approach; /* reordering approach */
141 int autodyn; /* automatic reordering */
142 int groupcheck; /* option for group sifting */
143 int profile; /* print heap profile if != 0 */
144 int keepperm; /* keep track of permutation */
145 int clearcache; /* clear the cache after each matrix */
146 int blifOrDot; /* dump format: 0 -> dot, 1 -> blif, ... */
147 int retval; /* return value */
148 int i; /* loop index */
149 long startTime; /* initial time */
150 long lapTime;
151 int size;
152 unsigned int cacheSize, maxMemory;
153 unsigned int nvars,nslots;
154
155 startTime = util_cpu_time();
156
157 approach = CUDD_REORDER_NONE;
158 autodyn = 0;
159 pr = 0;
160 harwell = 0;
161 multiple = 0;
162 profile = 0;
163 keepperm = 0;
164 cmu = 0;
165 N = 4;
166 nvars = 4;
167 cacheSize = 127;
168 maxMemory = 0;
169 nslots = CUDD_UNIQUE_SLOTS;
170 clearcache = 0;
171 groupcheck = CUDD_GROUP_CHECK7;
172 dfile = NULL;
173 blifOrDot = 0; /* dot format */
174
175 /* Parse command line. */
176 while ((c = util_getopt(argc, argv, (char *) "CDHMPS:a:bcd:g:hkmn:p:v:x:X:"))
177 != EOF) {
178 switch(c) {
179 case 'C':
180 cmu = 1;
181 break;
182 case 'D':
183 autodyn = 1;
184 break;
185 case 'H':
186 harwell = 1;
187 break;
188 case 'M':
189 #ifdef MNEMOSYNE
190 (void) mnem_setrecording(0);
191 #endif
192 break;
193 case 'P':
194 profile = 1;
195 break;
196 case 'S':
197 nslots = atoi(util_optarg);
198 break;
199 case 'X':
200 maxMemory = atoi(util_optarg);
201 break;
202 case 'a':
203 approach = atoi(util_optarg);
204 break;
205 case 'b':
206 blifOrDot = 1; /* blif format */
207 break;
208 case 'c':
209 clearcache = 1;
210 break;
211 case 'd':
212 dfile = util_optarg;
213 break;
214 case 'g':
215 groupcheck = atoi(util_optarg);
216 break;
217 case 'k':
218 keepperm = 1;
219 break;
220 case 'm':
221 multiple = 1;
222 break;
223 case 'n':
224 N = atoi(util_optarg);
225 break;
226 case 'p':
227 pr = atoi(util_optarg);
228 break;
229 case 'v':
230 nvars = atoi(util_optarg);
231 break;
232 case 'x':
233 cacheSize = atoi(util_optarg);
234 break;
235 case 'h':
236 default:
237 usage(argv[0]);
238 break;
239 }
240 }
241
242 if (argc - util_optind == 0) {
243 file = (char *) "-";
244 } else if (argc - util_optind == 1) {
245 file = argv[util_optind];
246 } else {
247 usage(argv[0]);
248 }
249 if ((approach<0) || (approach>17)) {
250 (void) fprintf(stderr,"Invalid approach: %d \n",approach);
251 usage(argv[0]);
252 }
253
254 if (pr >= 0) {
255 (void) printf("# %s\n", TESTCUDD_VERSION);
256 /* Echo command line and arguments. */
257 (void) printf("#");
258 for (i = 0; i < argc; i++) {
259 (void) printf(" %s", argv[i]);
260 }
261 (void) printf("\n");
262 (void) fflush(stdout);
263 }
264
265 /* Initialize manager and provide easy reference to terminals. */
266 dd = Cudd_Init(nvars,0,nslots,cacheSize,maxMemory);
267 one = DD_ONE(dd);
268 dd->groupcheck = (Cudd_AggregationType) groupcheck;
269 if (autodyn) Cudd_AutodynEnable(dd,CUDD_REORDER_SAME);
270
271 /* Open input file. */
272 fp = open_file(file, "r");
273
274 /* Open dump file if requested */
275 if (dfile != NULL) {
276 dfp = open_file(dfile, "w");
277 }
278
279 x = y = xn = yn_ = NULL;
280 do {
281 /* We want to start anew for every matrix. */
282 maxnx = maxny = 0;
283 nx = maxnx; ny = maxny;
284 if (pr>0) lapTime = util_cpu_time();
285 if (harwell) {
286 if (pr >= 0) (void) printf(":name: ");
287 ok = Cudd_addHarwell(fp, dd, &M, &x, &y, &xn, &yn_, &nx, &ny,
288 &m, &n, 0, 2, 1, 2, pr);
289 } else {
290 ok = Cudd_addRead(fp, dd, &M, &x, &y, &xn, &yn_, &nx, &ny,
291 &m, &n, 0, 2, 1, 2);
292 if (pr >= 0)
293 (void) printf(":name: %s: %d rows %d columns\n", file, m, n);
294 }
295 if (!ok) {
296 (void) fprintf(stderr, "Error reading matrix\n");
297 exit(1);
298 }
299
300 if (nx > maxnx) maxnx = nx;
301 if (ny > maxny) maxny = ny;
302
303 /* Build cube of negated y's. */
304 ycube = DD_ONE(dd);
305 Cudd_Ref(ycube);
306 for (i = maxny - 1; i >= 0; i--) {
307 DdNode *tmpp;
308 tmpp = Cudd_bddAnd(dd,Cudd_Not(dd->vars[y[i]->index]),ycube);
309 if (tmpp == NULL) exit(2);
310 Cudd_Ref(tmpp);
311 Cudd_RecursiveDeref(dd,ycube);
312 ycube = tmpp;
313 }
314 /* Initialize vectors of BDD variables used by priority func. */
315 xvars = ALLOC(DdNode *, nx);
316 if (xvars == NULL) exit(2);
317 for (i = 0; i < nx; i++) {
318 xvars[i] = dd->vars[x[i]->index];
319 }
320 yvars = ALLOC(DdNode *, ny);
321 if (yvars == NULL) exit(2);
322 for (i = 0; i < ny; i++) {
323 yvars[i] = dd->vars[y[i]->index];
324 }
325
326 /* Clean up */
327 for (i=0; i < maxnx; i++) {
328 Cudd_RecursiveDeref(dd, x[i]);
329 Cudd_RecursiveDeref(dd, xn[i]);
330 }
331 FREE(x);
332 FREE(xn);
333 for (i=0; i < maxny; i++) {
334 Cudd_RecursiveDeref(dd, y[i]);
335 Cudd_RecursiveDeref(dd, yn_[i]);
336 }
337 FREE(y);
338 FREE(yn_);
339
340 if (pr>0) {(void) printf(":1: M"); Cudd_PrintDebug(dd,M,nx+ny,pr);}
341
342 if (pr>0) (void) printf(":2: time to read the matrix = %s\n",
343 util_print_time(util_cpu_time() - lapTime));
344
345 C = Cudd_addBddPattern(dd, M);
346 if (C == 0) exit(2);
347 Cudd_Ref(C);
348 if (pr>0) {(void) printf(":3: C"); Cudd_PrintDebug(dd,C,nx+ny,pr);}
349
350 /* Test iterators. */
351 retval = testIterators(dd,M,C,pr);
352 if (retval == 0) exit(2);
353
354 cuddCacheProfile(dd,stdout);
355
356 /* Test XOR */
357 retval = testXor(dd,C,pr,nx+ny);
358 if (retval == 0) exit(2);
359
360 /* Test Hamming distance functions. */
361 retval = testHamming(dd,C,pr);
362 if (retval == 0) exit(2);
363
364 /* Test selection functions. */
365 CP = Cudd_CProjection(dd,C,ycube);
366 if (CP == NULL) exit(2);
367 Cudd_Ref(CP);
368 if (pr>0) {(void) printf("ycube"); Cudd_PrintDebug(dd,ycube,nx+ny,pr);}
369 if (pr>0) {(void) printf("CP"); Cudd_PrintDebug(dd,CP,nx+ny,pr);}
370
371 if (nx == ny) {
372 CPr = Cudd_PrioritySelect(dd,C,xvars,yvars,(DdNode **)NULL,
373 (DdNode *)NULL,ny,Cudd_Xgty);
374 if (CPr == NULL) exit(2);
375 Cudd_Ref(CPr);
376 if (pr>0) {(void) printf(":4: CPr"); Cudd_PrintDebug(dd,CPr,nx+ny,pr);}
377 if (CP != CPr) {
378 (void) printf("CP != CPr!\n");
379 }
380 Cudd_RecursiveDeref(dd, CPr);
381 }
382
383 /* Test inequality generator. */
384 {
385 int Nmin = ddMin(nx,ny);
386 int q;
387 DdGen *gen;
388 int *cube;
389 DdNode *f = Cudd_Inequality(dd,Nmin,2,xvars,yvars);
390 if (f == NULL) exit(2);
391 Cudd_Ref(f);
392 if (pr>0) {
393 (void) printf(":4: ineq");
394 Cudd_PrintDebug(dd,f,nx+ny,pr);
395 if (pr>1) {
396 Cudd_ForeachPrime(dd,Cudd_Not(f),Cudd_Not(f),gen,cube) {
397 for (q = 0; q < dd->size; q++) {
398 switch (cube[q]) {
399 case 0:
400 (void) printf("1");
401 break;
402 case 1:
403 (void) printf("0");
404 break;
405 case 2:
406 (void) printf("-");
407 break;
408 default:
409 (void) printf("?");
410 }
411 }
412 (void) printf(" 1\n");
413 }
414 (void) printf("\n");
415 }
416 }
417 Cudd_IterDerefBdd(dd, f);
418 }
419 FREE(xvars); FREE(yvars);
420
421 Cudd_RecursiveDeref(dd, CP);
422 Cudd_RecursiveDeref(dd, ycube);
423
424 /* Test functions for essential variables. */
425 ess = Cudd_FindEssential(dd,C);
426 if (ess == NULL) exit(2);
427 Cudd_Ref(ess);
428 if (pr>0) {(void) printf(":4: ess"); Cudd_PrintDebug(dd,ess,nx+ny,pr);}
429 Cudd_RecursiveDeref(dd, ess);
430
431 /* Test functions for shortest paths. */
432 shortP = Cudd_ShortestPath(dd, M, NULL, NULL, &length);
433 if (shortP == NULL) exit(2);
434 Cudd_Ref(shortP);
435 if (pr>0) {
436 (void) printf(":5: shortP"); Cudd_PrintDebug(dd,shortP,nx+ny,pr);
437 }
438 /* Test functions for largest cubes. */
439 largest = Cudd_LargestCube(dd, Cudd_Not(C), &length);
440 if (largest == NULL) exit(2);
441 Cudd_Ref(largest);
442 if (pr>0) {
443 (void) printf(":5b: largest");
444 Cudd_PrintDebug(dd,largest,nx+ny,pr);
445 }
446 Cudd_RecursiveDeref(dd, largest);
447
448 /* Test Cudd_addEvalConst and Cudd_addIteConstant. */
449 shortA = Cudd_BddToAdd(dd,shortP);
450 if (shortA == NULL) exit(2);
451 Cudd_Ref(shortA);
452 Cudd_RecursiveDeref(dd, shortP);
453 constN = Cudd_addEvalConst(dd,shortA,M);
454 if (constN == DD_NON_CONSTANT) exit(2);
455 if (Cudd_addIteConstant(dd,shortA,M,constN) != constN) exit(2);
456 if (pr>0) {(void) printf("The value of M along the chosen shortest path is %g\n", cuddV(constN));}
457 Cudd_RecursiveDeref(dd, shortA);
458
459 shortP = Cudd_ShortestPath(dd, C, NULL, NULL, &length);
460 if (shortP == NULL) exit(2);
461 Cudd_Ref(shortP);
462 if (pr>0) {
463 (void) printf(":6: shortP"); Cudd_PrintDebug(dd,shortP,nx+ny,pr);
464 }
465
466 /* Test Cudd_bddIteConstant and Cudd_bddLeq. */
467 if (!Cudd_bddLeq(dd,shortP,C)) exit(2);
468 if (Cudd_bddIteConstant(dd,Cudd_Not(shortP),one,C) != one) exit(2);
469 Cudd_RecursiveDeref(dd, shortP);
470
471 if (profile) {
472 retval = cuddHeapProfile(dd);
473 }
474
475 size = dd->size;
476
477 if (pr>0) {
478 (void) printf("Average distance: %g\n", Cudd_AverageDistance(dd));
479 }
480
481 /* Reorder if so requested. */
482 if (approach != CUDD_REORDER_NONE) {
483 #ifndef DD_STATS
484 retval = Cudd_EnableReorderingReporting(dd);
485 if (retval == 0) {
486 (void) fprintf(stderr,"Error reported by Cudd_EnableReorderingReporting\n");
487 exit(3);
488 }
489 #endif
490 #ifdef DD_DEBUG
491 retval = Cudd_DebugCheck(dd);
492 if (retval != 0) {
493 (void) fprintf(stderr,"Error reported by Cudd_DebugCheck\n");
494 exit(3);
495 }
496 retval = Cudd_CheckKeys(dd);
497 if (retval != 0) {
498 (void) fprintf(stderr,"Error reported by Cudd_CheckKeys\n");
499 exit(3);
500 }
501 #endif
502 retval = Cudd_ReduceHeap(dd,(Cudd_ReorderingType)approach,5);
503 if (retval == 0) {
504 (void) fprintf(stderr,"Error reported by Cudd_ReduceHeap\n");
505 exit(3);
506 }
507 #ifndef DD_STATS
508 retval = Cudd_DisableReorderingReporting(dd);
509 if (retval == 0) {
510 (void) fprintf(stderr,"Error reported by Cudd_DisableReorderingReporting\n");
511 exit(3);
512 }
513 #endif
514 #ifdef DD_DEBUG
515 retval = Cudd_DebugCheck(dd);
516 if (retval != 0) {
517 (void) fprintf(stderr,"Error reported by Cudd_DebugCheck\n");
518 exit(3);
519 }
520 retval = Cudd_CheckKeys(dd);
521 if (retval != 0) {
522 (void) fprintf(stderr,"Error reported by Cudd_CheckKeys\n");
523 exit(3);
524 }
525 #endif
526 if (approach == CUDD_REORDER_SYMM_SIFT ||
527 approach == CUDD_REORDER_SYMM_SIFT_CONV) {
528 Cudd_SymmProfile(dd,0,dd->size-1);
529 }
530
531 if (pr>0) {
532 (void) printf("Average distance: %g\n", Cudd_AverageDistance(dd));
533 }
534
535 if (keepperm) {
536 /* Print variable permutation. */
537 (void) printf("Variable Permutation:");
538 for (i=0; i<size; i++) {
539 if (i%20 == 0) (void) printf("\n");
540 (void) printf("%d ", dd->invperm[i]);
541 }
542 (void) printf("\n");
543 (void) printf("Inverse Permutation:");
544 for (i=0; i<size; i++) {
545 if (i%20 == 0) (void) printf("\n");
546 (void) printf("%d ", dd->perm[i]);
547 }
548 (void) printf("\n");
549 }
550
551 if (pr>0) {(void) printf("M"); Cudd_PrintDebug(dd,M,nx+ny,pr);}
552
553 if (profile) {
554 retval = cuddHeapProfile(dd);
555 }
556
557 }
558
559 /* Dump DDs of C and M if so requested. */
560 if (dfile != NULL) {
561 dfunc[0] = C;
562 dfunc[1] = M;
563 if (blifOrDot == 1) {
564 /* Only dump C because blif cannot handle ADDs */
565 retval = Cudd_DumpBlif(dd,1,dfunc,NULL,(char **)onames,
566 NULL,dfp,0);
567 } else {
568 retval = Cudd_DumpDot(dd,2,dfunc,NULL,(char **)onames,dfp);
569 }
570 if (retval != 1) {
571 (void) fprintf(stderr,"abnormal termination\n");
572 exit(2);
573 }
574 }
575
576 Cudd_RecursiveDeref(dd, C);
577 Cudd_RecursiveDeref(dd, M);
578
579 if (clearcache) {
580 if (pr>0) {(void) printf("Clearing the cache... ");}
581 for (i = dd->cacheSlots - 1; i>=0; i--) {
582 dd->cache[i].data = NIL(DdNode);
583 }
584 if (pr>0) {(void) printf("done\n");}
585 }
586 if (pr>0) {
587 (void) printf("Number of variables = %6d\t",dd->size);
588 (void) printf("Number of slots = %6u\n",dd->slots);
589 (void) printf("Number of keys = %6u\t",dd->keys);
590 (void) printf("Number of min dead = %6u\n",dd->minDead);
591 }
592
593 } while (multiple && !feof(fp));
594
595 fclose(fp);
596 if (dfile != NULL) {
597 fclose(dfp);
598 }
599
600 /* Second phase: experiment with Walsh matrices. */
601 if (!testWalsh(dd,N,cmu,approach,pr)) {
602 exit(2);
603 }
604
605 /* Check variable destruction. */
606 assert(cuddDestroySubtables(dd,3));
607 assert(Cudd_DebugCheck(dd) == 0);
608 assert(Cudd_CheckKeys(dd) == 0);
609
610 retval = Cudd_CheckZeroRef(dd);
611 ok = retval != 0; /* ok == 0 means O.K. */
612 if (retval != 0) {
613 (void) fprintf(stderr,
614 "%d non-zero DD reference counts after dereferencing\n", retval);
615 }
616
617 if (pr >= 0) {
618 (void) Cudd_PrintInfo(dd,stdout);
619 }
620
621 Cudd_Quit(dd);
622
623 #ifdef MNEMOSYNE
624 mnem_writestats();
625 #endif
626
627 if (pr>0) (void) printf("total time = %s\n",
628 util_print_time(util_cpu_time() - startTime));
629
630 if (pr >= 0) util_print_cpu_stats(stdout);
631 exit(ok);
632 /* NOTREACHED */
633
634 } /* end of main */
635
636
637 /*---------------------------------------------------------------------------*/
638 /* Definition of static functions */
639 /*---------------------------------------------------------------------------*/
640
641
642 /**Function********************************************************************
643
644 Synopsis [Prints usage info for testcudd.]
645
646 Description []
647
648 SideEffects [None]
649
650 SeeAlso []
651
652 ******************************************************************************/
653 static void
654 usage(char *prog)
655 {
656 (void) fprintf(stderr, "usage: %s [options] [file]\n", prog);
657 (void) fprintf(stderr, " -C\t\tuse CMU multiplication algorithm\n");
658 (void) fprintf(stderr, " -D\t\tenable automatic dynamic reordering\n");
659 (void) fprintf(stderr, " -H\t\tread matrix in Harwell format\n");
660 (void) fprintf(stderr, " -M\t\tturns off memory allocation recording\n");
661 (void) fprintf(stderr, " -P\t\tprint BDD heap profile\n");
662 (void) fprintf(stderr, " -S n\t\tnumber of slots for each subtable\n");
663 (void) fprintf(stderr, " -X n\t\ttarget maximum memory in bytes\n");
664 (void) fprintf(stderr, " -a n\t\tchoose reordering approach (0-13)\n");
665 (void) fprintf(stderr, " \t\t\t0: same as autoMethod\n");
666 (void) fprintf(stderr, " \t\t\t1: no reordering (default)\n");
667 (void) fprintf(stderr, " \t\t\t2: random\n");
668 (void) fprintf(stderr, " \t\t\t3: pivot\n");
669 (void) fprintf(stderr, " \t\t\t4: sifting\n");
670 (void) fprintf(stderr, " \t\t\t5: sifting to convergence\n");
671 (void) fprintf(stderr, " \t\t\t6: symmetric sifting\n");
672 (void) fprintf(stderr, " \t\t\t7: symmetric sifting to convergence\n");
673 (void) fprintf(stderr, " \t\t\t8-10: window of size 2-4\n");
674 (void) fprintf(stderr, " \t\t\t11-13: window of size 2-4 to conv.\n");
675 (void) fprintf(stderr, " \t\t\t14: group sifting\n");
676 (void) fprintf(stderr, " \t\t\t15: group sifting to convergence\n");
677 (void) fprintf(stderr, " \t\t\t16: simulated annealing\n");
678 (void) fprintf(stderr, " \t\t\t17: genetic algorithm\n");
679 (void) fprintf(stderr, " -b\t\tuse blif as format for dumps\n");
680 (void) fprintf(stderr, " -c\t\tclear the cache after each matrix\n");
681 (void) fprintf(stderr, " -d file\tdump DDs to file\n");
682 (void) fprintf(stderr, " -g\t\tselect aggregation criterion (0,5,7)\n");
683 (void) fprintf(stderr, " -h\t\tprints this message\n");
684 (void) fprintf(stderr, " -k\t\tprint the variable permutation\n");
685 (void) fprintf(stderr, " -m\t\tread multiple matrices (only with -H)\n");
686 (void) fprintf(stderr, " -n n\t\tnumber of variables\n");
687 (void) fprintf(stderr, " -p n\t\tcontrol verbosity\n");
688 (void) fprintf(stderr, " -v n\t\tinitial variables in the unique table\n");
689 (void) fprintf(stderr, " -x n\t\tinitial size of the cache\n");
690 exit(2);
691 } /* end of usage */
692
693
694 /**Function********************************************************************
695
696 Synopsis [Opens a file.]
697
698 Description [Opens a file, or fails with an error message and exits.
699 Allows '-' as a synonym for standard input.]
700
701 SideEffects [None]
702
703 SeeAlso []
704
705 ******************************************************************************/
706 static FILE *
707 open_file(char *filename, const char *mode)
708 {
709 FILE *fp;
710
711 if (strcmp(filename, "-") == 0) {
712 return mode[0] == 'r' ? stdin : stdout;
713 } else if ((fp = fopen(filename, mode)) == NULL) {
714 perror(filename);
715 exit(1);
716 }
717 return fp;
718
719 } /* end of open_file */
720
721
722 /**Function********************************************************************
723
724 Synopsis [Tests Walsh matrix multiplication.]
725
726 Description [Tests Walsh matrix multiplication. Return 1 if successful;
727 0 otherwise.]
728
729 SideEffects [May create new variables in the manager.]
730
731 SeeAlso []
732
733 ******************************************************************************/
734 static int
735 testWalsh(
736 DdManager *dd /* manager */,
737 int N /* number of variables */,
738 int cmu /* use CMU approach to matrix multiplication */,
739 int approach /* reordering approach */,
740 int pr /* verbosity level */)
741 {
742 DdNode *walsh1, *walsh2, *wtw;
743 DdNode **x, **v, **z;
744 int i, retval;
745 DdNode *one = DD_ONE(dd);
746 DdNode *zero = DD_ZERO(dd);
747
748 if (N > 3) {
749 x = ALLOC(DdNode *,N);
750 v = ALLOC(DdNode *,N);
751 z = ALLOC(DdNode *,N);
752
753 for (i = N-1; i >= 0; i--) {
754 Cudd_Ref(x[i]=cuddUniqueInter(dd,3*i,one,zero));
755 Cudd_Ref(v[i]=cuddUniqueInter(dd,3*i+1,one,zero));
756 Cudd_Ref(z[i]=cuddUniqueInter(dd,3*i+2,one,zero));
757 }
758 Cudd_Ref(walsh1 = Cudd_addWalsh(dd,v,z,N));
759 if (pr>0) {(void) printf("walsh1"); Cudd_PrintDebug(dd,walsh1,2*N,pr);}
760 Cudd_Ref(walsh2 = Cudd_addWalsh(dd,x,v,N));
761 if (cmu) {
762 Cudd_Ref(wtw = Cudd_addTimesPlus(dd,walsh2,walsh1,v,N));
763 } else {
764 Cudd_Ref(wtw = Cudd_addMatrixMultiply(dd,walsh2,walsh1,v,N));
765 }
766 if (pr>0) {(void) printf("wtw"); Cudd_PrintDebug(dd,wtw,2*N,pr);}
767
768 if (approach != CUDD_REORDER_NONE) {
769 #ifdef DD_DEBUG
770 retval = Cudd_DebugCheck(dd);
771 if (retval != 0) {
772 (void) fprintf(stderr,"Error reported by Cudd_DebugCheck\n");
773 return(0);
774 }
775 #endif
776 retval = Cudd_ReduceHeap(dd,(Cudd_ReorderingType)approach,5);
777 if (retval == 0) {
778 (void) fprintf(stderr,"Error reported by Cudd_ReduceHeap\n");
779 return(0);
780 }
781 #ifdef DD_DEBUG
782 retval = Cudd_DebugCheck(dd);
783 if (retval != 0) {
784 (void) fprintf(stderr,"Error reported by Cudd_DebugCheck\n");
785 return(0);
786 }
787 #endif
788 if (approach == CUDD_REORDER_SYMM_SIFT ||
789 approach == CUDD_REORDER_SYMM_SIFT_CONV) {
790 Cudd_SymmProfile(dd,0,dd->size-1);
791 }
792 }
793 /* Clean up. */
794 Cudd_RecursiveDeref(dd, wtw);
795 Cudd_RecursiveDeref(dd, walsh1);
796 Cudd_RecursiveDeref(dd, walsh2);
797 for (i=0; i < N; i++) {
798 Cudd_RecursiveDeref(dd, x[i]);
799 Cudd_RecursiveDeref(dd, v[i]);
800 Cudd_RecursiveDeref(dd, z[i]);
801 }
802 FREE(x);
803 FREE(v);
804 FREE(z);
805 }
806 return(1);
807
808 } /* end of testWalsh */
809
810 /**Function********************************************************************
811
812 Synopsis [Tests iterators.]
813
814 Description [Tests iterators on cubes and nodes.]
815
816 SideEffects [None]
817
818 SeeAlso []
819
820 ******************************************************************************/
821 static int
822 testIterators(
823 DdManager *dd,
824 DdNode *M,
825 DdNode *C,
826 int pr)
827 {
828 int *cube;
829 CUDD_VALUE_TYPE value;
830 DdGen *gen;
831 int q;
832
833 /* Test iterator for cubes. */
834 if (pr>1) {
835 (void) printf("Testing iterator on cubes:\n");
836 Cudd_ForeachCube(dd,M,gen,cube,value) {
837 for (q = 0; q < dd->size; q++) {
838 switch (cube[q]) {
839 case 0:
840 (void) printf("0");
841 break;
842 case 1:
843 (void) printf("1");
844 break;
845 case 2:
846 (void) printf("-");
847 break;
848 default:
849 (void) printf("?");
850 }
851 }
852 (void) printf(" %g\n",value);
853 }
854 (void) printf("\n");
855 }
856
857 if (pr>1) {
858 (void) printf("Testing prime expansion of cubes:\n");
859 if (!Cudd_bddPrintCover(dd,C,C)) return(0);
860 }
861
862 if (pr>1) {
863 (void) printf("Testing iterator on primes (CNF):\n");
864 Cudd_ForeachPrime(dd,Cudd_Not(C),Cudd_Not(C),gen,cube) {
865 for (q = 0; q < dd->size; q++) {
866 switch (cube[q]) {
867 case 0:
868 (void) printf("1");
869 break;
870 case 1:
871 (void) printf("0");
872 break;
873 case 2:
874 (void) printf("-");
875 break;
876 default:
877 (void) printf("?");
878 }
879 }
880 (void) printf(" 1\n");
881 }
882 (void) printf("\n");
883 }
884
885 /* Test iterator on nodes. */
886 if (pr>2) {
887 DdNode *node;
888 (void) printf("Testing iterator on nodes:\n");
889 Cudd_ForeachNode(dd,M,gen,node) {
890 if (Cudd_IsConstant(node)) {
891 #if SIZEOF_VOID_P == 8
892 (void) printf("ID = 0x%lx\tvalue = %-9g\n",
893 (ptruint) node /
894 (ptruint) sizeof(DdNode),
895 Cudd_V(node));
896 #else
897 (void) printf("ID = 0x%x\tvalue = %-9g\n",
898 (ptruint) node /
899 (ptruint) sizeof(DdNode),
900 Cudd_V(node));
901 #endif
902 } else {
903 #if SIZEOF_VOID_P == 8
904 (void) printf("ID = 0x%lx\tindex = %u\tr = %u\n",
905 (ptruint) node /
906 (ptruint) sizeof(DdNode),
907 node->index, node->ref);
908 #else
909 (void) printf("ID = 0x%x\tindex = %u\tr = %u\n",
910 (ptruint) node /
911 (ptruint) sizeof(DdNode),
912 node->index, node->ref);
913 #endif
914 }
915 }
916 (void) printf("\n");
917 }
918 return(1);
919
920 } /* end of testIterators */
921
922
923 /**Function********************************************************************
924
925 Synopsis [Tests the functions related to the exclusive OR.]
926
927 Description [Tests the functions related to the exclusive OR. It
928 builds the boolean difference of the given function in three
929 different ways and checks that the results is the same. Returns 1 if
930 successful; 0 otherwise.]
931
932 SideEffects [None]
933
934 SeeAlso []
935
936 ******************************************************************************/
937 static int
938 testXor(DdManager *dd, DdNode *f, int pr, int nvars)
939 {
940 DdNode *f1, *f0, *res1, *res2;
941 int x;
942
943 /* Extract cofactors w.r.t. mid variable. */
944 x = nvars / 2;
945 f1 = Cudd_Cofactor(dd,f,dd->vars[x]);
946 if (f1 == NULL) return(0);
947 Cudd_Ref(f1);
948
949 f0 = Cudd_Cofactor(dd,f,Cudd_Not(dd->vars[x]));
950 if (f0 == NULL) {
951 Cudd_RecursiveDeref(dd,f1);
952 return(0);
953 }
954 Cudd_Ref(f0);
955
956 /* Compute XOR of cofactors with ITE. */
957 res1 = Cudd_bddIte(dd,f1,Cudd_Not(f0),f0);
958 if (res1 == NULL) return(0);
959 Cudd_Ref(res1);
960
961 if (pr>0) {(void) printf("xor1"); Cudd_PrintDebug(dd,res1,nvars,pr);}
962
963 /* Compute XOR of cofactors with XOR. */
964 res2 = Cudd_bddXor(dd,f1,f0);
965 if (res2 == NULL) {
966 Cudd_RecursiveDeref(dd,res1);
967 return(0);
968 }
969 Cudd_Ref(res2);
970
971 if (res1 != res2) {
972 if (pr>0) {(void) printf("xor2"); Cudd_PrintDebug(dd,res2,nvars,pr);}
973 Cudd_RecursiveDeref(dd,res1);
974 Cudd_RecursiveDeref(dd,res2);
975 return(0);
976 }
977 Cudd_RecursiveDeref(dd,res1);
978 Cudd_RecursiveDeref(dd,f1);
979 Cudd_RecursiveDeref(dd,f0);
980
981 /* Compute boolean difference directly. */
982 res1 = Cudd_bddBooleanDiff(dd,f,x);
983 if (res1 == NULL) {
984 Cudd_RecursiveDeref(dd,res2);
985 return(0);
986 }
987 Cudd_Ref(res1);
988
989 if (res1 != res2) {
990 if (pr>0) {(void) printf("xor3"); Cudd_PrintDebug(dd,res1,nvars,pr);}
991 Cudd_RecursiveDeref(dd,res1);
992 Cudd_RecursiveDeref(dd,res2);
993 return(0);
994 }
995 Cudd_RecursiveDeref(dd,res1);
996 Cudd_RecursiveDeref(dd,res2);
997 return(1);
998
999 } /* end of testXor */
1000
1001
1002 /**Function********************************************************************
1003
1004 Synopsis [Tests the Hamming distance functions.]
1005
1006 Description [Tests the Hammming distance functions. Returns
1007 1 if successful; 0 otherwise.]
1008
1009 SideEffects [None]
1010
1011 SeeAlso []
1012
1013 ******************************************************************************/
1014 static int
1015 testHamming(
1016 DdManager *dd,
1017 DdNode *f,
1018 int pr)
1019 {
1020 DdNode **vars, *minBdd, *zero, *scan;
1021 int i;
1022 int d;
1023 int *minterm;
1024 int size = Cudd_ReadSize(dd);
1025
1026 vars = ALLOC(DdNode *, size);
1027 if (vars == NULL) return(0);
1028 for (i = 0; i < size; i++) {
1029 vars[i] = Cudd_bddIthVar(dd,i);
1030 }
1031
1032 minBdd = Cudd_bddPickOneMinterm(dd,Cudd_Not(f),vars,size);
1033 Cudd_Ref(minBdd);
1034 if (pr > 0) {
1035 (void) printf("Chosen minterm for Hamming distance test: ");
1036 Cudd_PrintDebug(dd,minBdd,size,pr);
1037 }
1038
1039 minterm = ALLOC(int,size);
1040 if (minterm == NULL) {
1041 FREE(vars);
1042 Cudd_RecursiveDeref(dd,minBdd);
1043 return(0);
1044 }
1045 scan = minBdd;
1046 zero = Cudd_Not(DD_ONE(dd));
1047 while (!Cudd_IsConstant(scan)) {
1048 DdNode *R = Cudd_Regular(scan);
1049 DdNode *T = Cudd_T(R);
1050 DdNode *E = Cudd_E(R);
1051 if (R != scan) {
1052 T = Cudd_Not(T);
1053 E = Cudd_Not(E);
1054 }
1055 if (T == zero) {
1056 minterm[R->index] = 0;
1057 scan = E;
1058 } else {
1059 minterm[R->index] = 1;
1060 scan = T;
1061 }
1062 }
1063 Cudd_RecursiveDeref(dd,minBdd);
1064
1065 d = Cudd_MinHammingDist(dd,f,minterm,size);
1066
1067 (void) printf("Minimum Hamming distance = %d\n", d);
1068
1069 FREE(vars);
1070 FREE(minterm);
1071 return(1);
1072
1073 } /* end of testHamming */
Common Lisp wrappers for CUDD library (Colorado University Decision Diagrams) using swig/cffi