source: vis_dev/glu-2.1/src/cuBdd/testcudd.c @ 13

Last change on this file since 13 was 8, checked in by cecile, 13 years ago

src glu
File size: 28.6 KB
Line 
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
68static char rcsid[] DD_UNUSED = "$Id: testcudd.c,v 1.16 2004/08/13 18:04:54 fabio Exp $";
69#endif
70
71static const char *onames[] = { "C", "M" }; /* names of functions to be dumped */
72
73/**AutomaticStart*************************************************************/
74
75/*---------------------------------------------------------------------------*/
76/* Static function prototypes                                                */
77/*---------------------------------------------------------------------------*/
78
79static void usage (char * prog);
80static FILE *open_file (char *filename, const char *mode);
81static int testIterators (DdManager *dd, DdNode *M, DdNode *C, int pr);
82static int testXor (DdManager *dd, DdNode *f, int pr, int nvars);
83static int testHamming (DdManager *dd, DdNode *f, int pr);
84static 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******************************************************************************/
100int
101main(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        FREE(xvars); FREE(yvars);
383
384        Cudd_RecursiveDeref(dd, CP);
385        Cudd_RecursiveDeref(dd, ycube);
386
387        /* Test functions for essential variables. */
388        ess = Cudd_FindEssential(dd,C);
389        if (ess == NULL) exit(2);
390        Cudd_Ref(ess);
391        if (pr>0) {(void) printf(":4: ess"); Cudd_PrintDebug(dd,ess,nx+ny,pr);}
392        Cudd_RecursiveDeref(dd, ess);
393
394        /* Test functions for shortest paths. */
395        shortP = Cudd_ShortestPath(dd, M, NULL, NULL, &length);
396        if (shortP == NULL) exit(2);
397        Cudd_Ref(shortP);
398        if (pr>0) {
399            (void) printf(":5: shortP"); Cudd_PrintDebug(dd,shortP,nx+ny,pr);
400        }
401        /* Test functions for largest cubes. */
402        largest = Cudd_LargestCube(dd, Cudd_Not(C), &length);
403        if (largest == NULL) exit(2);
404        Cudd_Ref(largest);
405        if (pr>0) {
406            (void) printf(":5b: largest");
407            Cudd_PrintDebug(dd,largest,nx+ny,pr);
408        }
409        Cudd_RecursiveDeref(dd, largest);
410
411        /* Test Cudd_addEvalConst and Cudd_addIteConstant. */
412        shortA = Cudd_BddToAdd(dd,shortP);
413        if (shortA == NULL) exit(2);
414        Cudd_Ref(shortA);
415        Cudd_RecursiveDeref(dd, shortP);
416        constN = Cudd_addEvalConst(dd,shortA,M);
417        if (constN == DD_NON_CONSTANT) exit(2);
418        if (Cudd_addIteConstant(dd,shortA,M,constN) != constN) exit(2);
419        if (pr>0) {(void) printf("The value of M along the chosen shortest path is %g\n", cuddV(constN));}
420        Cudd_RecursiveDeref(dd, shortA);
421
422        shortP = Cudd_ShortestPath(dd, C, NULL, NULL, &length);
423        if (shortP == NULL) exit(2);
424        Cudd_Ref(shortP);
425        if (pr>0) {
426            (void) printf(":6: shortP"); Cudd_PrintDebug(dd,shortP,nx+ny,pr);
427        }
428
429        /* Test Cudd_bddIteConstant and Cudd_bddLeq. */
430        if (!Cudd_bddLeq(dd,shortP,C)) exit(2);
431        if (Cudd_bddIteConstant(dd,Cudd_Not(shortP),one,C) != one) exit(2);
432        Cudd_RecursiveDeref(dd, shortP);
433
434        if (profile) {
435            retval = cuddHeapProfile(dd);
436        }
437
438        size = dd->size;
439
440        if (pr>0) {
441            (void) printf("Average distance: %g\n", Cudd_AverageDistance(dd));
442        }
443
444        /* Reorder if so requested. */
445        if (approach != CUDD_REORDER_NONE) {
446#ifndef DD_STATS
447            retval = Cudd_EnableReorderingReporting(dd);
448            if (retval == 0) {
449                (void) fprintf(stderr,"Error reported by Cudd_EnableReorderingReporting\n");
450                exit(3);
451            }
452#endif
453#ifdef DD_DEBUG
454            retval = Cudd_DebugCheck(dd);
455            if (retval != 0) {
456                (void) fprintf(stderr,"Error reported by Cudd_DebugCheck\n");
457                exit(3);
458            }
459            retval = Cudd_CheckKeys(dd);
460            if (retval != 0) {
461                (void) fprintf(stderr,"Error reported by Cudd_CheckKeys\n");
462                exit(3);
463            }
464#endif
465            retval = Cudd_ReduceHeap(dd,(Cudd_ReorderingType)approach,5);
466            if (retval == 0) {
467                (void) fprintf(stderr,"Error reported by Cudd_ReduceHeap\n");
468                exit(3);
469            }
470#ifndef DD_STATS
471            retval = Cudd_DisableReorderingReporting(dd);
472            if (retval == 0) {
473                (void) fprintf(stderr,"Error reported by Cudd_DisableReorderingReporting\n");
474                exit(3);
475            }
476#endif
477#ifdef DD_DEBUG
478            retval = Cudd_DebugCheck(dd);
479            if (retval != 0) {
480                (void) fprintf(stderr,"Error reported by Cudd_DebugCheck\n");
481                exit(3);
482            }
483            retval = Cudd_CheckKeys(dd);
484            if (retval != 0) {
485                (void) fprintf(stderr,"Error reported by Cudd_CheckKeys\n");
486                exit(3);
487            }
488#endif
489            if (approach == CUDD_REORDER_SYMM_SIFT ||
490            approach == CUDD_REORDER_SYMM_SIFT_CONV) {
491                Cudd_SymmProfile(dd,0,dd->size-1);
492            }
493
494            if (pr>0) {
495                (void) printf("Average distance: %g\n", Cudd_AverageDistance(dd));
496            }
497
498            if (keepperm) {
499                /* Print variable permutation. */
500                (void) printf("Variable Permutation:");
501                for (i=0; i<size; i++) {
502                    if (i%20 == 0) (void) printf("\n");
503                    (void) printf("%d ", dd->invperm[i]);
504                }
505                (void) printf("\n");
506                (void) printf("Inverse Permutation:");
507                for (i=0; i<size; i++) {
508                    if (i%20 == 0) (void) printf("\n");
509                    (void) printf("%d ", dd->perm[i]);
510                }
511                (void) printf("\n");
512            }
513
514            if (pr>0) {(void) printf("M"); Cudd_PrintDebug(dd,M,nx+ny,pr);}
515
516            if (profile) {
517                retval = cuddHeapProfile(dd);
518            }
519
520        }
521
522        /* Dump DDs of C and M if so requested. */
523        if (dfile != NULL) {
524            dfunc[0] = C;
525            dfunc[1] = M;
526            if (blifOrDot == 1) {
527                /* Only dump C because blif cannot handle ADDs */
528                retval = Cudd_DumpBlif(dd,1,dfunc,NULL,(char **)onames,
529                                       NULL,dfp);
530            } else {
531                retval = Cudd_DumpDot(dd,2,dfunc,NULL,(char **)onames,dfp);
532            }
533            if (retval != 1) {
534                (void) fprintf(stderr,"abnormal termination\n");
535                exit(2);
536            }
537        }
538
539        Cudd_RecursiveDeref(dd, C);
540        Cudd_RecursiveDeref(dd, M);
541
542        if (clearcache) {
543            if (pr>0) {(void) printf("Clearing the cache... ");}
544            for (i = dd->cacheSlots - 1; i>=0; i--) {
545                dd->cache[i].data = NIL(DdNode);
546            }
547            if (pr>0) {(void) printf("done\n");}
548        }
549        if (pr>0) {
550            (void) printf("Number of variables = %6d\t",dd->size);
551            (void) printf("Number of slots     = %6d\n",dd->slots);
552            (void) printf("Number of keys      = %6d\t",dd->keys);
553            (void) printf("Number of min dead  = %6d\n",dd->minDead);
554        }
555
556    } while (multiple && !feof(fp));
557
558    fclose(fp);
559    if (dfile != NULL) {
560        fclose(dfp);
561    }
562
563    /* Second phase: experiment with Walsh matrices. */
564    if (!testWalsh(dd,N,cmu,approach,pr)) {
565        exit(2);
566    }
567
568    /* Check variable destruction. */
569    assert(cuddDestroySubtables(dd,3));
570    assert(Cudd_DebugCheck(dd) == 0);
571    assert(Cudd_CheckKeys(dd) == 0);
572
573    retval = Cudd_CheckZeroRef(dd);
574    ok = retval != 0;  /* ok == 0 means O.K. */
575    if (retval != 0) {
576        (void) fprintf(stderr,
577            "%d non-zero DD reference counts after dereferencing\n", retval);
578    }
579
580    if (pr >= 0) {
581        (void) Cudd_PrintInfo(dd,stdout);
582    }
583
584    Cudd_Quit(dd);
585
586#ifdef MNEMOSYNE
587    mnem_writestats();
588#endif
589
590    if (pr>0) (void) printf("total time = %s\n",
591                util_print_time(util_cpu_time() - startTime));
592
593    if (pr >= 0) util_print_cpu_stats(stdout);
594    exit(ok);
595    /* NOTREACHED */
596
597} /* end of main */
598
599
600/*---------------------------------------------------------------------------*/
601/* Definition of static functions                                            */
602/*---------------------------------------------------------------------------*/
603
604
605/**Function********************************************************************
606
607  Synopsis    [Prints usage info for testcudd.]
608
609  Description []
610
611  SideEffects [None]
612
613  SeeAlso     []
614
615******************************************************************************/
616static void
617usage(char *prog)
618{
619    (void) fprintf(stderr, "usage: %s [options] [file]\n", prog);
620    (void) fprintf(stderr, "   -C\t\tuse CMU multiplication algorithm\n");
621    (void) fprintf(stderr, "   -D\t\tenable automatic dynamic reordering\n");
622    (void) fprintf(stderr, "   -H\t\tread matrix in Harwell format\n");
623    (void) fprintf(stderr, "   -M\t\tturns off memory allocation recording\n");
624    (void) fprintf(stderr, "   -P\t\tprint BDD heap profile\n");
625    (void) fprintf(stderr, "   -S n\t\tnumber of slots for each subtable\n");
626    (void) fprintf(stderr, "   -X n\t\ttarget maximum memory in bytes\n");
627    (void) fprintf(stderr, "   -a n\t\tchoose reordering approach (0-13)\n");
628    (void) fprintf(stderr, "   \t\t\t0: same as autoMethod\n");
629    (void) fprintf(stderr, "   \t\t\t1: no reordering (default)\n");
630    (void) fprintf(stderr, "   \t\t\t2: random\n");
631    (void) fprintf(stderr, "   \t\t\t3: pivot\n");
632    (void) fprintf(stderr, "   \t\t\t4: sifting\n");
633    (void) fprintf(stderr, "   \t\t\t5: sifting to convergence\n");
634    (void) fprintf(stderr, "   \t\t\t6: symmetric sifting\n");
635    (void) fprintf(stderr, "   \t\t\t7: symmetric sifting to convergence\n");
636    (void) fprintf(stderr, "   \t\t\t8-10: window of size 2-4\n");
637    (void) fprintf(stderr, "   \t\t\t11-13: window of size 2-4 to conv.\n");
638    (void) fprintf(stderr, "   \t\t\t14: group sifting\n");
639    (void) fprintf(stderr, "   \t\t\t15: group sifting to convergence\n");
640    (void) fprintf(stderr, "   \t\t\t16: simulated annealing\n");
641    (void) fprintf(stderr, "   \t\t\t17: genetic algorithm\n");
642    (void) fprintf(stderr, "   -b\t\tuse blif as format for dumps\n");
643    (void) fprintf(stderr, "   -c\t\tclear the cache after each matrix\n");
644    (void) fprintf(stderr, "   -d file\tdump DDs to file\n");
645    (void) fprintf(stderr, "   -g\t\tselect aggregation criterion (0,5,7)\n");
646    (void) fprintf(stderr, "   -h\t\tprints this message\n");
647    (void) fprintf(stderr, "   -k\t\tprint the variable permutation\n");
648    (void) fprintf(stderr, "   -m\t\tread multiple matrices (only with -H)\n");
649    (void) fprintf(stderr, "   -n n\t\tnumber of variables\n");
650    (void) fprintf(stderr, "   -p n\t\tcontrol verbosity\n");
651    (void) fprintf(stderr, "   -v n\t\tinitial variables in the unique table\n");
652    (void) fprintf(stderr, "   -x n\t\tinitial size of the cache\n");
653    exit(2);
654} /* end of usage */
655
656
657/**Function********************************************************************
658
659  Synopsis    [Opens a file.]
660
661  Description [Opens a file, or fails with an error message and exits.
662  Allows '-' as a synonym for standard input.]
663
664  SideEffects [None]
665
666  SeeAlso     []
667
668******************************************************************************/
669static FILE *
670open_file(char *filename, const char *mode)
671{
672    FILE *fp;
673
674    if (strcmp(filename, "-") == 0) {
675        return mode[0] == 'r' ? stdin : stdout;
676    } else if ((fp = fopen(filename, mode)) == NULL) {
677        perror(filename);
678        exit(1);
679    }
680    return fp;
681
682} /* end of open_file */
683
684
685/**Function********************************************************************
686
687  Synopsis    [Tests Walsh matrix multiplication.]
688
689  Description [Tests Walsh matrix multiplication.  Return 1 if successful;
690  0 otherwise.]
691
692  SideEffects [May create new variables in the manager.]
693
694  SeeAlso     []
695
696******************************************************************************/
697static int
698testWalsh(
699  DdManager *dd /* manager */,
700  int N /* number of variables */,
701  int cmu /* use CMU approach to matrix multiplication */,
702  int approach /* reordering approach */,
703  int pr /* verbosity level */)
704{
705    DdNode *walsh1, *walsh2, *wtw;
706    DdNode **x, **v, **z;
707    int i, retval;
708    DdNode *one = DD_ONE(dd);
709    DdNode *zero = DD_ZERO(dd);
710
711    if (N > 3) {
712        x = ALLOC(DdNode *,N);
713        v = ALLOC(DdNode *,N);
714        z = ALLOC(DdNode *,N);
715
716        for (i = N-1; i >= 0; i--) {
717            Cudd_Ref(x[i]=cuddUniqueInter(dd,3*i,one,zero));
718            Cudd_Ref(v[i]=cuddUniqueInter(dd,3*i+1,one,zero));
719            Cudd_Ref(z[i]=cuddUniqueInter(dd,3*i+2,one,zero));
720        }
721        Cudd_Ref(walsh1 = Cudd_addWalsh(dd,v,z,N));
722        if (pr>0) {(void) printf("walsh1"); Cudd_PrintDebug(dd,walsh1,2*N,pr);}
723        Cudd_Ref(walsh2 = Cudd_addWalsh(dd,x,v,N));
724        if (cmu) {
725            Cudd_Ref(wtw = Cudd_addTimesPlus(dd,walsh2,walsh1,v,N));
726        } else {
727            Cudd_Ref(wtw = Cudd_addMatrixMultiply(dd,walsh2,walsh1,v,N));
728        }
729        if (pr>0) {(void) printf("wtw"); Cudd_PrintDebug(dd,wtw,2*N,pr);}
730
731        if (approach != CUDD_REORDER_NONE) {
732#ifdef DD_DEBUG
733            retval = Cudd_DebugCheck(dd);
734            if (retval != 0) {
735                (void) fprintf(stderr,"Error reported by Cudd_DebugCheck\n");
736                return(0);
737            }
738#endif
739            retval = Cudd_ReduceHeap(dd,(Cudd_ReorderingType)approach,5);
740            if (retval == 0) {
741                (void) fprintf(stderr,"Error reported by Cudd_ReduceHeap\n");
742                return(0);
743            }
744#ifdef DD_DEBUG
745            retval = Cudd_DebugCheck(dd);
746            if (retval != 0) {
747                (void) fprintf(stderr,"Error reported by Cudd_DebugCheck\n");
748                return(0);
749            }
750#endif
751            if (approach == CUDD_REORDER_SYMM_SIFT ||
752            approach == CUDD_REORDER_SYMM_SIFT_CONV) {
753                Cudd_SymmProfile(dd,0,dd->size-1);
754            }
755        }
756        /* Clean up. */
757        Cudd_RecursiveDeref(dd, wtw);
758        Cudd_RecursiveDeref(dd, walsh1);
759        Cudd_RecursiveDeref(dd, walsh2);
760        for (i=0; i < N; i++) {
761            Cudd_RecursiveDeref(dd, x[i]);
762            Cudd_RecursiveDeref(dd, v[i]);
763            Cudd_RecursiveDeref(dd, z[i]);
764        }
765        FREE(x);
766        FREE(v);
767        FREE(z);
768    }
769    return(1);
770
771} /* end of testWalsh */
772
773/**Function********************************************************************
774
775  Synopsis    [Tests iterators.]
776
777  Description [Tests iterators on cubes and nodes.]
778
779  SideEffects [None]
780
781  SeeAlso     []
782
783******************************************************************************/
784static int
785testIterators(
786  DdManager *dd,
787  DdNode *M,
788  DdNode *C,
789  int pr)
790{
791    int *cube;
792    CUDD_VALUE_TYPE value;
793    DdGen *gen;
794    int q;
795
796    /* Test iterator for cubes. */
797    if (pr>1) {
798        (void) printf("Testing iterator on cubes:\n");
799        Cudd_ForeachCube(dd,M,gen,cube,value) {
800            for (q = 0; q < dd->size; q++) {
801                switch (cube[q]) {
802                case 0:
803                    (void) printf("0");
804                    break;
805                case 1:
806                    (void) printf("1");
807                    break;
808                case 2:
809                    (void) printf("-");
810                    break;
811                default:
812                    (void) printf("?");
813                }
814            }
815            (void) printf(" %g\n",value);
816        }
817        (void) printf("\n");
818    }
819
820    if (pr>1) {
821        (void) printf("Testing prime expansion of cubes:\n");
822        if (!Cudd_bddPrintCover(dd,C,C)) return(0);
823    }
824
825    if (pr>1) {
826        (void) printf("Testing iterator on primes (CNF):\n");
827        Cudd_ForeachPrime(dd,Cudd_Not(C),Cudd_Not(C),gen,cube) {
828            for (q = 0; q < dd->size; q++) {
829                switch (cube[q]) {
830                case 0:
831                    (void) printf("1");
832                    break;
833                case 1:
834                    (void) printf("0");
835                    break;
836                case 2:
837                    (void) printf("-");
838                    break;
839                default:
840                    (void) printf("?");
841                }
842            }
843            (void) printf(" 1\n");
844        }
845        (void) printf("\n");
846    }
847
848    /* Test iterator on nodes. */
849    if (pr>2) {
850        DdGen *gen;
851        DdNode *node;
852        (void) printf("Testing iterator on nodes:\n");
853        Cudd_ForeachNode(dd,M,gen,node) {
854            if (Cudd_IsConstant(node)) {
855#if SIZEOF_VOID_P == 8
856                (void) printf("ID = 0x%lx\tvalue = %-9g\n",
857                              (unsigned long) node /
858                              (unsigned long) sizeof(DdNode),
859                              Cudd_V(node));
860#else
861                (void) printf("ID = 0x%x\tvalue = %-9g\n",
862                              (unsigned int) node /
863                              (unsigned int) sizeof(DdNode),
864                              Cudd_V(node));
865#endif
866            } else {
867#if SIZEOF_VOID_P == 8
868                (void) printf("ID = 0x%lx\tindex = %d\tr = %d\n",
869                              (unsigned long) node /
870                              (unsigned long) sizeof(DdNode),
871                              node->index, node->ref);
872#else
873                (void) printf("ID = 0x%x\tindex = %d\tr = %d\n",
874                              (unsigned int) node /
875                              (unsigned int) sizeof(DdNode),
876                              node->index, node->ref);
877#endif
878            }
879        }
880        (void) printf("\n");
881    }
882    return(1);
883
884} /* end of testIterators */
885
886
887/**Function********************************************************************
888
889  Synopsis    [Tests the functions related to the exclusive OR.]
890
891  Description [Tests the functions related to the exclusive OR. It
892  builds the boolean difference of the given function in three
893  different ways and checks that the results is the same. Returns 1 if
894  successful; 0 otherwise.]
895
896  SideEffects [None]
897
898  SeeAlso     []
899
900******************************************************************************/
901static int
902testXor(DdManager *dd, DdNode *f, int pr, int nvars)
903{
904    DdNode *f1, *f0, *res1, *res2;
905    int x;
906
907    /* Extract cofactors w.r.t. mid variable. */
908    x = nvars / 2;
909    f1 = Cudd_Cofactor(dd,f,dd->vars[x]);
910    if (f1 == NULL) return(0);
911    Cudd_Ref(f1);
912
913    f0 = Cudd_Cofactor(dd,f,Cudd_Not(dd->vars[x]));
914    if (f0 == NULL) {
915        Cudd_RecursiveDeref(dd,f1);
916        return(0);
917    }
918    Cudd_Ref(f0);
919
920    /* Compute XOR of cofactors with ITE. */
921    res1 = Cudd_bddIte(dd,f1,Cudd_Not(f0),f0);
922    if (res1 == NULL) return(0);
923    Cudd_Ref(res1);
924
925    if (pr>0) {(void) printf("xor1"); Cudd_PrintDebug(dd,res1,nvars,pr);}
926
927    /* Compute XOR of cofactors with XOR. */
928    res2 = Cudd_bddXor(dd,f1,f0);
929    if (res2 == NULL) {
930        Cudd_RecursiveDeref(dd,res1);
931        return(0);
932    }
933    Cudd_Ref(res2);
934
935    if (res1 != res2) {
936        if (pr>0) {(void) printf("xor2"); Cudd_PrintDebug(dd,res2,nvars,pr);}
937        Cudd_RecursiveDeref(dd,res1);
938        Cudd_RecursiveDeref(dd,res2);
939        return(0);
940    }
941    Cudd_RecursiveDeref(dd,res1);
942    Cudd_RecursiveDeref(dd,f1);
943    Cudd_RecursiveDeref(dd,f0);
944
945    /* Compute boolean difference directly. */
946    res1 = Cudd_bddBooleanDiff(dd,f,x);
947    if (res1 == NULL) {
948        Cudd_RecursiveDeref(dd,res2);
949        return(0);
950    }
951    Cudd_Ref(res1);
952
953    if (res1 != res2) {
954        if (pr>0) {(void) printf("xor3"); Cudd_PrintDebug(dd,res1,nvars,pr);}
955        Cudd_RecursiveDeref(dd,res1);
956        Cudd_RecursiveDeref(dd,res2);
957        return(0);
958    }
959    Cudd_RecursiveDeref(dd,res1);
960    Cudd_RecursiveDeref(dd,res2);
961    return(1);
962
963} /* end of testXor */
964
965
966/**Function********************************************************************
967
968  Synopsis    [Tests the Hamming distance functions.]
969
970  Description [Tests the Hammming distance functions. Returns
971  1 if successful; 0 otherwise.]
972
973  SideEffects [None]
974
975  SeeAlso     []
976
977******************************************************************************/
978static int
979testHamming(
980  DdManager *dd,
981  DdNode *f,
982  int pr)
983{
984    DdNode **vars, *minBdd, *zero, *scan;
985    int i;
986    int d;
987    int *minterm;
988    int size = Cudd_ReadSize(dd);
989
990    vars = ALLOC(DdNode *, size);
991    if (vars == NULL) return(0);
992    for (i = 0; i < size; i++) {
993        vars[i] = Cudd_bddIthVar(dd,i);
994    }
995
996    minBdd = Cudd_bddPickOneMinterm(dd,Cudd_Not(f),vars,size);
997    Cudd_Ref(minBdd);
998    if (pr > 0) {
999        (void) printf("Chosen minterm for Hamming distance test: ");
1000        Cudd_PrintDebug(dd,minBdd,size,pr);
1001    }
1002
1003    minterm = ALLOC(int,size);
1004    if (minterm == NULL) {
1005        FREE(vars);
1006        Cudd_RecursiveDeref(dd,minBdd);
1007        return(0);
1008    }
1009    scan = minBdd;
1010    zero = Cudd_Not(DD_ONE(dd));
1011    while (!Cudd_IsConstant(scan)) {
1012        DdNode *R = Cudd_Regular(scan);
1013        DdNode *T = Cudd_T(R);
1014        DdNode *E = Cudd_E(R);
1015        if (R != scan) {
1016            T = Cudd_Not(T);
1017            E = Cudd_Not(E);
1018        }
1019        if (T == zero) {
1020            minterm[R->index] = 0;
1021            scan = E;
1022        } else {
1023            minterm[R->index] = 1;
1024            scan = T;
1025        }
1026    }
1027    Cudd_RecursiveDeref(dd,minBdd);
1028
1029    d = Cudd_MinHammingDist(dd,f,minterm,size);
1030
1031    (void) printf("Minimum Hamming distance = %d\n", d);
1032
1033    FREE(vars);
1034    FREE(minterm);
1035    return(1);
1036
1037} /* end of testHamming */
Note: See TracBrowser for help on using the repository browser.