source: vis_dev/glu-2.3/src/cuBdd/testcudd.c

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

library glu 2.3
File size: 29.2 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.20 2009/03/08 02:49:02 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
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******************************************************************************/
653static void
654usage(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******************************************************************************/
706static FILE *
707open_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******************************************************************************/
734static int
735testWalsh(
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******************************************************************************/
821static int
822testIterators(
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******************************************************************************/
937static int
938testXor(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******************************************************************************/
1014static int
1015testHamming(
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 */
Note: See TracBrowser for help on using the repository browser.