source: icGREP/icgrep-devel/cudd-2.5.1/nanotrav/ntrZddTest.c

Last change on this file was 4597, checked in by nmedfort, 4 years ago

Upload of the CUDD library.

File size: 13.6 KB
Line 
1/**CFile***********************************************************************
2 
3  FileName    [ntrZddTest.c]
4
5  PackageName [ntr]
6
7  Synopsis    [ZDD test functions.]
8
9  Description []
10
11  SeeAlso     []
12
13  Author      [Fabio Somenzi]
14   
15  Copyright   [Copyright (c) 1995-2012, Regents of the University of Colorado
16
17  All rights reserved.
18
19  Redistribution and use in source and binary forms, with or without
20  modification, are permitted provided that the following conditions
21  are met:
22
23  Redistributions of source code must retain the above copyright
24  notice, this list of conditions and the following disclaimer.
25
26  Redistributions in binary form must reproduce the above copyright
27  notice, this list of conditions and the following disclaimer in the
28  documentation and/or other materials provided with the distribution.
29
30  Neither the name of the University of Colorado nor the names of its
31  contributors may be used to endorse or promote products derived from
32  this software without specific prior written permission.
33
34  THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
35  "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
36  LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
37  FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
38  COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
39  INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
40  BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
41  LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
42  CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
43  LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
44  ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
45  POSSIBILITY OF SUCH DAMAGE.]
46
47******************************************************************************/
48
49#include "ntr.h"
50#include "cuddInt.h"
51
52/*---------------------------------------------------------------------------*/
53/* Constant declarations                                                     */
54/*---------------------------------------------------------------------------*/
55
56/*---------------------------------------------------------------------------*/
57/* Stucture declarations                                                     */
58/*---------------------------------------------------------------------------*/
59
60/*---------------------------------------------------------------------------*/
61/* Type declarations                                                         */
62/*---------------------------------------------------------------------------*/
63
64/*---------------------------------------------------------------------------*/
65/* Variable declarations                                                     */
66/*---------------------------------------------------------------------------*/
67
68#ifndef lint
69static char rcsid[] UTIL_UNUSED = "$Id: ntrZddTest.c,v 1.15 2012/02/05 01:53:01 fabio Exp fabio $";
70#endif
71
72/*---------------------------------------------------------------------------*/
73/* Macro declarations                                                        */
74/*---------------------------------------------------------------------------*/
75
76/**AutomaticStart*************************************************************/
77
78/*---------------------------------------------------------------------------*/
79/* Static function prototypes                                                */
80/*---------------------------------------------------------------------------*/
81
82static int reorderZdd (BnetNetwork *net, DdManager *dd, NtrOptions *option);
83
84/**AutomaticEnd***************************************************************/
85
86/*---------------------------------------------------------------------------*/
87/* Definition of exported functions                                          */
88/*---------------------------------------------------------------------------*/
89
90
91/**Function********************************************************************
92
93  Synopsis    [Tests ZDDs.]
94
95  Description [Tests ZDDs. Returns 1 if successful; 0 otherwise.]
96
97  SideEffects [Creates ZDD variables in the manager.]
98
99  SeeAlso     []
100
101******************************************************************************/
102int
103Ntr_testZDD(
104  DdManager * dd,
105  BnetNetwork * net,
106  NtrOptions * option)
107{
108    DdNode **zdd;               /* array of converted outputs */
109    int nz;                     /* actual number of ZDDs */
110    int result;
111    int i, j;
112    BnetNode *node;             /* auxiliary pointer to network node */
113    int pr = option->verb;
114    int level;                  /* aux. var. used to print variable orders */
115    char **names;               /* array used to print variable orders */
116    int nvars;
117
118    /* Build an array of ZDDs for the output functions or for the
119    ** specified node. */
120    Cudd_AutodynDisable(dd);
121    Cudd_AutodynDisableZdd(dd);
122    zdd = ALLOC(DdNode *,net->noutputs);
123    result = Cudd_zddVarsFromBddVars(dd,1);
124    if (result == 0) return(0);
125    if (option->node == NULL) {
126        for (nz = 0; nz < net->noutputs; nz++) {
127            if (!st_lookup(net->hash,net->outputs[nz],&node)) {
128                return(0);
129            }
130            zdd[nz] = Cudd_zddPortFromBdd(dd, node->dd);
131            if (zdd[nz]) {
132                Cudd_Ref(zdd[nz]);
133                (void) printf("%s", node->name);
134                result = Cudd_zddPrintDebug(dd,zdd[nz],Cudd_ReadZddSize(dd),pr);
135                if (result == 0) return(0);
136            } else {
137                (void) printf("Conversion to ZDD failed.\n");
138            }
139        }
140    } else {
141        if (!st_lookup(net->hash,option->node,&node)) {
142            return(0);
143        }
144        zdd[0] = Cudd_zddPortFromBdd(dd, node->dd);
145        if (zdd[0]) {
146            Cudd_Ref(zdd[0]);
147            (void) printf("%s", node->name);
148            result = Cudd_zddPrintDebug(dd,zdd[0],Cudd_ReadZddSize(dd),pr);
149            if (result == 0) return(0);
150        } else {
151            (void) printf("Conversion to ZDD failed.\n");
152        }
153        nz = 1;
154    }
155
156#ifdef DD_DEBUG
157    result = Cudd_CheckKeys(dd);
158    if (result != 0) {
159        (void) fprintf(stderr,"Error reported by Cudd_CheckKeys\n");
160        return(0);
161    }
162#endif
163
164    if (option->autoDyn & 1) {
165        Cudd_AutodynEnable(dd,CUDD_REORDER_SAME);
166    }
167    if (option->autoDyn & 2) {
168        Cudd_AutodynEnableZdd(dd,CUDD_REORDER_SAME);
169    }
170
171    /* Convert the ZDDs back to BDDs and check identity. */
172    for (i = 0; i < nz; i++) {
173        DdNode *checkBdd;
174        checkBdd = Cudd_zddPortToBdd(dd,zdd[i]);
175        if (checkBdd) {
176            Cudd_Ref(checkBdd);
177            if (option->node == NULL) {
178                if (!st_lookup(net->hash,net->outputs[i],&node)) {
179                    return(0);
180                }
181            } else {
182                if (!st_lookup(net->hash,option->node,&node)) {
183                    return(0);
184                }
185            }
186            if (checkBdd != node->dd) {
187                (void) fprintf(stdout,"Equivalence failed at node %s",
188                               node->name);
189                result = Cudd_PrintDebug(dd,checkBdd,Cudd_ReadZddSize(dd),pr);
190                if (result == 0) return(0);
191            }
192            Cudd_RecursiveDeref(dd,checkBdd);
193        } else {
194            (void) printf("Conversion to BDD failed.\n");
195        }
196    }
197
198#ifdef DD_DEBUG
199    result = Cudd_CheckKeys(dd);
200    if (result != 0) {
201        (void) fprintf(stderr,"Error reported by Cudd_CheckKeys\n");
202        return(0);
203    }
204#endif
205
206    /* Play with the ZDDs a little. */
207    if (nz > 2) {
208        DdNode *f;
209        DdNode *g1, *g2, *g;
210        f = Cudd_zddIte(dd,zdd[0],zdd[1],zdd[2]);
211        if (f == NULL) return(0);
212        cuddRef(f);
213        g1 = Cudd_zddIntersect(dd,zdd[0],zdd[1]);
214        if (g1 == NULL) {
215            Cudd_RecursiveDerefZdd(dd,f);
216            return(0);
217        }
218        cuddRef(g1);
219        g2 = Cudd_zddDiff(dd,zdd[2],zdd[0]);
220        if (g2 == NULL) {
221            Cudd_RecursiveDerefZdd(dd,f);
222            Cudd_RecursiveDerefZdd(dd,g1);
223            return(0);
224        }
225        cuddRef(g2);
226        g = Cudd_zddUnion(dd,g1,g2);
227        if (g == NULL) {
228            Cudd_RecursiveDerefZdd(dd,f);
229            Cudd_RecursiveDerefZdd(dd,g1);
230            Cudd_RecursiveDerefZdd(dd,g2);
231            return(0);
232        }
233        cuddRef(g);
234        Cudd_RecursiveDerefZdd(dd,g1);
235        Cudd_RecursiveDerefZdd(dd,g2);
236        if (g != f) {
237            (void) fprintf(stderr,"f != g!\n");
238        }
239        Cudd_RecursiveDerefZdd(dd,g);
240        Cudd_RecursiveDerefZdd(dd,f);
241    }
242
243#ifdef DD_DEBUG
244    result = Cudd_CheckKeys(dd);
245    if (result != 0) {
246        (void) fprintf(stderr,"Error reported by Cudd_CheckKeys\n");
247        return(0);
248    }
249#endif
250
251    /* Perform ZDD reordering. */
252    result = reorderZdd(net,dd,option);
253    if (result == 0) return(0);
254
255    /* Print final ZDD order. */
256    nvars = Cudd_ReadZddSize(dd);
257    names = ALLOC(char *, nvars);
258    if (names == NULL) return(0);
259    for (i = 0; i < nvars; i++) {
260        names[i] = NULL;
261    }
262    if (option->reordering != CUDD_REORDER_NONE) {
263        for (i = 0; i < net->npis; i++) {
264            if (!st_lookup(net->hash,net->inputs[i],&node)) {
265                FREE(names);
266                return(0);
267            }
268            level = Cudd_ReadPermZdd(dd,node->var);
269            names[level] = node->name;
270        }
271        for (i = 0; i < net->nlatches; i++) {
272            if (!st_lookup(net->hash,net->latches[i][1],&node)) {
273                FREE(names);
274                return(0);
275            }
276            level = Cudd_ReadPermZdd(dd,node->var);
277            names[level] = node->name;
278        }
279        (void) printf("New order\n");
280        for (i = 0, j = 0; i < nvars; i++) {
281            if (names[i] == NULL) continue;
282            if((j%8 == 0)&&j) (void) printf("\n");
283            (void) printf("%s ",names[i]);
284            j++;
285        }
286        (void) printf("\n");
287    }
288    FREE(names);
289
290    /* Dispose of ZDDs. */
291    for (i = 0; i < nz; i++) {
292        Cudd_RecursiveDerefZdd(dd,zdd[i]);
293    }
294    FREE(zdd);
295    return(1);
296
297} /* end of Ntr_testZDD */
298
299
300/**Function********************************************************************
301
302  Synopsis    [Builds ZDD covers.]
303
304  Description []
305
306  SideEffects [Creates ZDD variables in the manager.]
307
308  SeeAlso     []
309
310******************************************************************************/
311int
312Ntr_testISOP(
313  DdManager * dd,
314  BnetNetwork * net,
315  NtrOptions * option)
316{
317    DdNode **zdd;               /* array of converted outputs */
318    DdNode *bdd;                /* return value of Cudd_zddIsop */
319    int nz;                     /* actual number of ZDDs */
320    int result;
321    int i;
322    BnetNode *node;             /* auxiliary pointer to network node */
323    int pr = option->verb;
324
325    /* Build an array of ZDDs for the output functions or the specified
326    ** node. */
327    Cudd_zddRealignEnable(dd);
328    Cudd_AutodynDisableZdd(dd);
329    zdd = ALLOC(DdNode *,net->noutputs);
330    result = Cudd_zddVarsFromBddVars(dd,2);
331    if (result == 0) return(0);
332    if (option->node == NULL) {
333        nz = net->noutputs;
334        for (i = 0; i < nz; i++) {
335            if (!st_lookup(net->hash,net->outputs[i],&node)) {
336                return(0);
337            }
338            bdd = Cudd_zddIsop(dd, node->dd, node->dd, &zdd[i]);
339            if (bdd != node->dd) return(0);
340            Cudd_Ref(bdd);
341            Cudd_RecursiveDeref(dd,bdd);
342            if (zdd[i]) {
343                Cudd_Ref(zdd[i]);
344                (void) printf("%s", node->name);
345                result = Cudd_zddPrintDebug(dd,zdd[i],Cudd_ReadZddSize(dd),pr);
346                if (result == 0) return(0);
347                if (option->printcover) {
348                    int *path;
349                    DdGen *gen;
350                    char *str = ALLOC(char,Cudd_ReadSize(dd)+1);
351                    if (str == NULL) return(0);
352                    (void) printf("Testing iterator on ZDD paths:\n");
353                    Cudd_zddForeachPath(dd,zdd[i],gen,path) {
354                        str = Cudd_zddCoverPathToString(dd,path,str);
355                        (void) printf("%s 1\n", str);
356                    }
357                    (void) printf("\n");
358                    FREE(str);
359                    result = Cudd_zddPrintCover(dd,zdd[i]);
360
361                    if (result == 0) return(0);
362                }
363            } else {
364                (void) printf("Conversion to ISOP failed.\n");
365                return(0);
366            }
367        }
368    } else {
369        nz = 1;
370        if (!st_lookup(net->hash,option->node,&node)) {
371            return(0);
372        }
373        bdd = Cudd_zddIsop(dd, node->dd, node->dd, &zdd[0]);
374        if (bdd != node->dd) return(0);
375        Cudd_Ref(bdd);
376        Cudd_RecursiveDeref(dd,bdd);
377        if (zdd[0]) {
378            Cudd_Ref(zdd[0]);
379            (void) printf("%s", node->name);
380            result = Cudd_zddPrintDebug(dd,zdd[0],Cudd_ReadZddSize(dd),pr);
381            if (result == 0) return(0);
382            if (option->printcover) {
383                int *path;
384                DdGen *gen;
385                char *str = ALLOC(char,Cudd_ReadSize(dd)+1);
386                if (str == NULL) return(0);
387                (void) printf("Testing iterator on ZDD paths:\n");
388                Cudd_zddForeachPath(dd,zdd[0],gen,path) {
389                    str = Cudd_zddCoverPathToString(dd,path,str);
390                    (void) printf("%s 1\n", str);
391                }
392                (void) printf("\n");
393                FREE(str);
394
395                result = Cudd_zddPrintCover(dd,zdd[0]);
396                if (result == 0) return(0);
397            }
398        } else {
399            (void) printf("Conversion to ISOP failed.\n");
400            return(0);
401        }
402    }
403    if (option->autoDyn) {
404        Cudd_AutodynEnableZdd(dd,CUDD_REORDER_SAME);
405    }
406
407    /* Perform ZDD reordering. */
408    result = reorderZdd(net,dd,option);
409    if (result == 0) return(0);
410
411    /* Dispose of ZDDs. */
412    for (i = 0; i < nz; i++) {
413        Cudd_RecursiveDerefZdd(dd,zdd[i]);
414    }
415    FREE(zdd);
416
417    return(1);
418
419} /* end of Ntr_testISOP */
420
421
422/*---------------------------------------------------------------------------*/
423/* Definition of internal functions                                          */
424/*---------------------------------------------------------------------------*/
425
426/*---------------------------------------------------------------------------*/
427/* Definition of static functions                                            */
428/*---------------------------------------------------------------------------*/
429
430
431/**Function********************************************************************
432
433  Synopsis    [Applies reordering to the ZDDs.]
434
435  Description [Explicitly applies reordering to the ZDDs. Returns 1 if
436  successful; 0 otherwise.]
437
438  SideEffects [None]
439
440  SeeAlso     []
441
442*****************************************************************************/
443static int
444reorderZdd(
445  BnetNetwork * net,
446  DdManager * dd /* DD Manager */,
447  NtrOptions * option)
448{
449    int result;                 /* return value from functions */
450
451    /* Perform the final reordering. */
452    if (option->reordering != CUDD_REORDER_NONE) {
453        (void) printf("Number of inputs = %d\n",net->ninputs);
454
455        dd->siftMaxVar = 1000000; 
456        result = Cudd_zddReduceHeap(dd,option->reordering,1);
457        if (result == 0) return(0);
458
459        /* Print symmetry stats if pertinent */
460        if (option->reordering == CUDD_REORDER_SYMM_SIFT ||
461            option->reordering == CUDD_REORDER_SYMM_SIFT_CONV)
462            Cudd_zddSymmProfile(dd, 0, dd->sizeZ - 1);
463    }
464
465    return(1);
466
467} /* end of reorderZdd */
468
Note: See TracBrowser for help on using the repository browser.