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 |
---|
78 | static 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 | ******************************************************************************/ |
---|
115 | DdNode * |
---|
116 | Cudd_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 | ******************************************************************************/ |
---|
151 | DdNode * |
---|
152 | cuddAddScalarInverseRecur( |
---|
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 | |
---|