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 "misc/util/util_hack.h"
55 #include "cuddInt.h"
56
57 ABC_NAMESPACE_IMPL_START
58
59
60
61
62 /*---------------------------------------------------------------------------*/
63 /* Constant declarations */
64 /*---------------------------------------------------------------------------*/
65
66
67 /*---------------------------------------------------------------------------*/
68 /* Stucture declarations */
69 /*---------------------------------------------------------------------------*/
70
71
72 /*---------------------------------------------------------------------------*/
73 /* Type declarations */
74 /*---------------------------------------------------------------------------*/
75
76
77 /*---------------------------------------------------------------------------*/
78 /* Variable declarations */
79 /*---------------------------------------------------------------------------*/
80
81 #ifndef lint
82 static char rcsid[] DD_UNUSED = "$Id: cuddAddInv.c,v 1.9 2004/08/13 18:04:45 fabio Exp $";
83 #endif
84
85
86 /*---------------------------------------------------------------------------*/
87 /* Macro declarations */
88 /*---------------------------------------------------------------------------*/
89
90
91 /**AutomaticStart*************************************************************/
92
93 /*---------------------------------------------------------------------------*/
94 /* Static function prototypes */
95 /*---------------------------------------------------------------------------*/
96
97
98 /**AutomaticEnd***************************************************************/
99
100
101 /*---------------------------------------------------------------------------*/
102 /* Definition of exported functions */
103 /*---------------------------------------------------------------------------*/
104
105
106 /**Function********************************************************************
107
108 Synopsis [Computes the scalar inverse of an ADD.]
109
110 Description [Computes an n ADD where the discriminants are the
111 multiplicative inverses of the corresponding discriminants of the
112 argument ADD. Returns a pointer to the resulting ADD in case of
113 success. Returns NULL if any discriminants smaller than epsilon is
114 encountered.]
115
116 SideEffects [None]
117
118 ******************************************************************************/
119 DdNode *
Cudd_addScalarInverse(DdManager * dd,DdNode * f,DdNode * epsilon)120 Cudd_addScalarInverse(
121 DdManager * dd,
122 DdNode * f,
123 DdNode * epsilon)
124 {
125 DdNode *res;
126
127 if (!cuddIsConstant(epsilon)) {
128 (void) fprintf(dd->err,"Invalid epsilon\n");
129 return(NULL);
130 }
131 do {
132 dd->reordered = 0;
133 res = cuddAddScalarInverseRecur(dd,f,epsilon);
134 } while (dd->reordered == 1);
135 return(res);
136
137 } /* end of Cudd_addScalarInverse */
138
139 /*---------------------------------------------------------------------------*/
140 /* Definition of internal functions */
141 /*---------------------------------------------------------------------------*/
142
143
144 /**Function********************************************************************
145
146 Synopsis [Performs the recursive step of addScalarInverse.]
147
148 Description [Returns a pointer to the resulting ADD in case of
149 success. Returns NULL if any discriminants smaller than epsilon is
150 encountered.]
151
152 SideEffects [None]
153
154 ******************************************************************************/
155 DdNode *
cuddAddScalarInverseRecur(DdManager * dd,DdNode * f,DdNode * epsilon)156 cuddAddScalarInverseRecur(
157 DdManager * dd,
158 DdNode * f,
159 DdNode * epsilon)
160 {
161 DdNode *t, *e, *res;
162 CUDD_VALUE_TYPE value;
163
164 statLine(dd);
165 if (cuddIsConstant(f)) {
166 if (ddAbs(cuddV(f)) < cuddV(epsilon)) return(NULL);
167 value = 1.0 / cuddV(f);
168 res = cuddUniqueConst(dd,value);
169 return(res);
170 }
171
172 res = cuddCacheLookup2(dd,Cudd_addScalarInverse,f,epsilon);
173 if (res != NULL) return(res);
174
175 t = cuddAddScalarInverseRecur(dd,cuddT(f),epsilon);
176 if (t == NULL) return(NULL);
177 cuddRef(t);
178
179 e = cuddAddScalarInverseRecur(dd,cuddE(f),epsilon);
180 if (e == NULL) {
181 Cudd_RecursiveDeref(dd, t);
182 return(NULL);
183 }
184 cuddRef(e);
185
186 res = (t == e) ? t : cuddUniqueInter(dd,(int)f->index,t,e);
187 if (res == NULL) {
188 Cudd_RecursiveDeref(dd, t);
189 Cudd_RecursiveDeref(dd, e);
190 return(NULL);
191 }
192 cuddDeref(t);
193 cuddDeref(e);
194
195 cuddCacheInsert2(dd,Cudd_addScalarInverse,f,epsilon,res);
196
197 return(res);
198
199 } /* end of cuddAddScalarInverseRecur */
200
201
202 /*---------------------------------------------------------------------------*/
203 /* Definition of static functions */
204 /*---------------------------------------------------------------------------*/
205
206
207 ABC_NAMESPACE_IMPL_END
208
209
210