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