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

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

library glu 2.3
File size: 6.7 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [cuddAddInv.c]
4
5  PackageName [cudd]
6
7  Synopsis    [Function to compute the scalar inverse of an ADD.]
8
9  Description [External procedures included in this module:
10                <ul>
11                <li> Cudd_addScalarInverse()
12                </ul>
13            Internal procedures included in this module:
14                <ul>
15                <li> cuddAddScalarInverseRecur()
16                </ul>]
17
18  Author      [Fabio Somenzi]
19
20  Copyright   [Copyright (c) 1995-2004, Regents of the University of Colorado
21
22  All rights reserved.
23
24  Redistribution and use in source and binary forms, with or without
25  modification, are permitted provided that the following conditions
26  are met:
27
28  Redistributions of source code must retain the above copyright
29  notice, this list of conditions and the following disclaimer.
30
31  Redistributions in binary form must reproduce the above copyright
32  notice, this list of conditions and the following disclaimer in the
33  documentation and/or other materials provided with the distribution.
34
35  Neither the name of the University of Colorado nor the names of its
36  contributors may be used to endorse or promote products derived from
37  this software without specific prior written permission.
38
39  THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
40  "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
41  LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
42  FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
43  COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
44  INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
45  BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
46  LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
47  CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
48  LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
49  ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
50  POSSIBILITY OF SUCH DAMAGE.]
51
52******************************************************************************/
53
54#include "util.h"
55#include "cuddInt.h"
56
57
58/*---------------------------------------------------------------------------*/
59/* Constant declarations                                                     */
60/*---------------------------------------------------------------------------*/
61
62
63/*---------------------------------------------------------------------------*/
64/* Stucture declarations                                                     */
65/*---------------------------------------------------------------------------*/
66
67
68/*---------------------------------------------------------------------------*/
69/* Type declarations                                                         */
70/*---------------------------------------------------------------------------*/
71
72
73/*---------------------------------------------------------------------------*/
74/* Variable declarations                                                     */
75/*---------------------------------------------------------------------------*/
76
77#ifndef lint
78static char rcsid[] DD_UNUSED = "$Id: cuddAddInv.c,v 1.9 2004/08/13 18:04:45 fabio Exp $";
79#endif
80
81
82/*---------------------------------------------------------------------------*/
83/* Macro declarations                                                        */
84/*---------------------------------------------------------------------------*/
85
86
87/**AutomaticStart*************************************************************/
88
89/*---------------------------------------------------------------------------*/
90/* Static function prototypes                                                */
91/*---------------------------------------------------------------------------*/
92
93
94/**AutomaticEnd***************************************************************/
95
96
97/*---------------------------------------------------------------------------*/
98/* Definition of exported functions                                          */
99/*---------------------------------------------------------------------------*/
100
101
102/**Function********************************************************************
103
104  Synopsis    [Computes the scalar inverse of an ADD.]
105 
106  Description [Computes an n ADD where the discriminants are the
107  multiplicative inverses of the corresponding discriminants of the
108  argument ADD.  Returns a pointer to the resulting ADD in case of
109  success. Returns NULL if any discriminants smaller than epsilon is
110  encountered.]
111
112  SideEffects [None]
113
114******************************************************************************/
115DdNode *
116Cudd_addScalarInverse(
117  DdManager * dd,
118  DdNode * f,
119  DdNode * epsilon)
120{
121    DdNode *res;
122
123    if (!cuddIsConstant(epsilon)) {
124        (void) fprintf(dd->err,"Invalid epsilon\n");
125        return(NULL);
126    }
127    do {
128        dd->reordered = 0;
129        res  = cuddAddScalarInverseRecur(dd,f,epsilon);
130    } while (dd->reordered == 1);
131    return(res);
132
133} /* end of Cudd_addScalarInverse */
134
135/*---------------------------------------------------------------------------*/
136/* Definition of internal functions                                          */
137/*---------------------------------------------------------------------------*/
138
139
140/**Function********************************************************************
141
142  Synopsis    [Performs the recursive step of addScalarInverse.]
143
144  Description [Returns a pointer to the resulting ADD in case of
145  success. Returns NULL if any discriminants smaller than epsilon is
146  encountered.]
147
148  SideEffects [None]
149
150******************************************************************************/
151DdNode *
152cuddAddScalarInverseRecur(
153  DdManager * dd,
154  DdNode * f,
155  DdNode * epsilon)
156{
157    DdNode *t, *e, *res;
158    CUDD_VALUE_TYPE value;
159
160    statLine(dd);
161    if (cuddIsConstant(f)) {
162        if (ddAbs(cuddV(f)) < cuddV(epsilon)) return(NULL);
163        value = 1.0 / cuddV(f);
164        res = cuddUniqueConst(dd,value);
165        return(res);
166    }
167
168    res = cuddCacheLookup2(dd,Cudd_addScalarInverse,f,epsilon);
169    if (res != NULL) return(res);
170
171    t = cuddAddScalarInverseRecur(dd,cuddT(f),epsilon);
172    if (t == NULL) return(NULL);
173    cuddRef(t);
174
175    e = cuddAddScalarInverseRecur(dd,cuddE(f),epsilon);
176    if (e == NULL) {
177        Cudd_RecursiveDeref(dd, t);
178        return(NULL);
179    }
180    cuddRef(e);
181
182    res = (t == e) ? t : cuddUniqueInter(dd,(int)f->index,t,e);
183    if (res == NULL) {
184        Cudd_RecursiveDeref(dd, t);
185        Cudd_RecursiveDeref(dd, e);
186        return(NULL);
187    }
188    cuddDeref(t);
189    cuddDeref(e);
190
191    cuddCacheInsert2(dd,Cudd_addScalarInverse,f,epsilon,res);
192
193    return(res);
194
195} /* end of cuddAddScalarInverseRecur */
196
197
198/*---------------------------------------------------------------------------*/
199/* Definition of static functions                                            */
200/*---------------------------------------------------------------------------*/
201
Note: See TracBrowser for help on using the repository browser.