1 /**CFile***********************************************************************
2
3 FileName [cuddAddNeg.c]
4
5 PackageName [cudd]
6
7 Synopsis [Function to compute the negation of an ADD.]
8
9 Description [External procedures included in this module:
10 <ul>
11 <li> Cudd_addNegate()
12 <li> Cudd_addRoundOff()
13 </ul>
14 Internal procedures included in this module:
15 <ul>
16 <li> cuddAddNegateRecur()
17 <li> cuddAddRoundOffRecur()
18 </ul> ]
19
20 Author [Fabio Somenzi, Balakrishna Kumthekar]
21
22 Copyright [Copyright (c) 1995-2004, Regents of the University of Colorado
23
24 All rights reserved.
25
26 Redistribution and use in source and binary forms, with or without
27 modification, are permitted provided that the following conditions
28 are met:
29
30 Redistributions of source code must retain the above copyright
31 notice, this list of conditions and the following disclaimer.
32
33 Redistributions in binary form must reproduce the above copyright
34 notice, this list of conditions and the following disclaimer in the
35 documentation and/or other materials provided with the distribution.
36
37 Neither the name of the University of Colorado nor the names of its
38 contributors may be used to endorse or promote products derived from
39 this software without specific prior written permission.
40
41 THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
42 "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
43 LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
44 FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
45 COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
46 INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
47 BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
48 LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
49 CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
50 LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
51 ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
52 POSSIBILITY OF SUCH DAMAGE.]
53
54 ******************************************************************************/
55
56 #include "misc/util/util_hack.h"
57 #include "cuddInt.h"
58
59 ABC_NAMESPACE_IMPL_START
60
61
62
63
64 /*---------------------------------------------------------------------------*/
65 /* Constant declarations */
66 /*---------------------------------------------------------------------------*/
67
68
69 /*---------------------------------------------------------------------------*/
70 /* Stucture declarations */
71 /*---------------------------------------------------------------------------*/
72
73
74 /*---------------------------------------------------------------------------*/
75 /* Type declarations */
76 /*---------------------------------------------------------------------------*/
77
78
79 /*---------------------------------------------------------------------------*/
80 /* Variable declarations */
81 /*---------------------------------------------------------------------------*/
82
83 #ifndef lint
84 static char rcsid[] DD_UNUSED = "$Id: cuddAddNeg.c,v 1.12 2009/02/20 02:14:58 fabio Exp $";
85 #endif
86
87
88 /*---------------------------------------------------------------------------*/
89 /* Macro declarations */
90 /*---------------------------------------------------------------------------*/
91
92
93 /**AutomaticStart*************************************************************/
94
95 /*---------------------------------------------------------------------------*/
96 /* Static function prototypes */
97 /*---------------------------------------------------------------------------*/
98
99
100 /**AutomaticEnd***************************************************************/
101
102
103 /*---------------------------------------------------------------------------*/
104 /* Definition of exported functions */
105 /*---------------------------------------------------------------------------*/
106
107 /**Function********************************************************************
108
109 Synopsis [Computes the additive inverse of an ADD.]
110
111 Description [Computes the additive inverse of an ADD. Returns a pointer
112 to the result if successful; NULL otherwise.]
113
114 SideEffects [None]
115
116 SeeAlso [Cudd_addCmpl]
117
118 ******************************************************************************/
119 DdNode *
Cudd_addNegate(DdManager * dd,DdNode * f)120 Cudd_addNegate(
121 DdManager * dd,
122 DdNode * f)
123 {
124 DdNode *res;
125
126 do {
127 res = cuddAddNegateRecur(dd,f);
128 } while (dd->reordered == 1);
129 return(res);
130
131 } /* end of Cudd_addNegate */
132
133
134 /**Function********************************************************************
135
136 Synopsis [Rounds off the discriminants of an ADD.]
137
138 Description [Rounds off the discriminants of an ADD. The discriminants are
139 rounded off to N digits after the decimal. Returns a pointer to the result
140 ADD if successful; NULL otherwise.]
141
142 SideEffects [None]
143
144 SeeAlso []
145
146 ******************************************************************************/
147 DdNode *
Cudd_addRoundOff(DdManager * dd,DdNode * f,int N)148 Cudd_addRoundOff(
149 DdManager * dd,
150 DdNode * f,
151 int N)
152 {
153 DdNode *res;
154 double trunc = pow(10.0,(double)N);
155
156 do {
157 res = cuddAddRoundOffRecur(dd,f,trunc);
158 } while (dd->reordered == 1);
159 return(res);
160
161 } /* end of Cudd_addRoundOff */
162
163
164 /*---------------------------------------------------------------------------*/
165 /* Definition of internal functions */
166 /*---------------------------------------------------------------------------*/
167
168
169 /**Function********************************************************************
170
171 Synopsis [Implements the recursive step of Cudd_addNegate.]
172
173 Description [Implements the recursive step of Cudd_addNegate.
174 Returns a pointer to the result.]
175
176 SideEffects [None]
177
178 ******************************************************************************/
179 DdNode *
cuddAddNegateRecur(DdManager * dd,DdNode * f)180 cuddAddNegateRecur(
181 DdManager * dd,
182 DdNode * f)
183 {
184 DdNode *res,
185 *fv, *fvn,
186 *T, *E;
187
188 statLine(dd);
189 /* Check terminal cases. */
190 if (cuddIsConstant(f)) {
191 res = cuddUniqueConst(dd,-cuddV(f));
192 return(res);
193 }
194
195 /* Check cache */
196 res = cuddCacheLookup1(dd,Cudd_addNegate,f);
197 if (res != NULL) return(res);
198
199 /* Recursive Step */
200 fv = cuddT(f);
201 fvn = cuddE(f);
202 T = cuddAddNegateRecur(dd,fv);
203 if (T == NULL) return(NULL);
204 cuddRef(T);
205
206 E = cuddAddNegateRecur(dd,fvn);
207 if (E == NULL) {
208 Cudd_RecursiveDeref(dd,T);
209 return(NULL);
210 }
211 cuddRef(E);
212 res = (T == E) ? T : cuddUniqueInter(dd,(int)f->index,T,E);
213 if (res == NULL) {
214 Cudd_RecursiveDeref(dd, T);
215 Cudd_RecursiveDeref(dd, E);
216 return(NULL);
217 }
218 cuddDeref(T);
219 cuddDeref(E);
220
221 /* Store result. */
222 cuddCacheInsert1(dd,Cudd_addNegate,f,res);
223
224 return(res);
225
226 } /* end of cuddAddNegateRecur */
227
228
229 /**Function********************************************************************
230
231 Synopsis [Implements the recursive step of Cudd_addRoundOff.]
232
233 Description [Implements the recursive step of Cudd_addRoundOff.
234 Returns a pointer to the result.]
235
236 SideEffects [None]
237
238 ******************************************************************************/
239 DdNode *
cuddAddRoundOffRecur(DdManager * dd,DdNode * f,double trunc)240 cuddAddRoundOffRecur(
241 DdManager * dd,
242 DdNode * f,
243 double trunc)
244 {
245
246 DdNode *res, *fv, *fvn, *T, *E;
247 double n;
248 DD_CTFP1 cacheOp;
249
250 statLine(dd);
251 if (cuddIsConstant(f)) {
252 n = ceil(cuddV(f)*trunc)/trunc;
253 res = cuddUniqueConst(dd,n);
254 return(res);
255 }
256 cacheOp = (DD_CTFP1) Cudd_addRoundOff;
257 res = cuddCacheLookup1(dd,cacheOp,f);
258 if (res != NULL) {
259 return(res);
260 }
261 /* Recursive Step */
262 fv = cuddT(f);
263 fvn = cuddE(f);
264 T = cuddAddRoundOffRecur(dd,fv,trunc);
265 if (T == NULL) {
266 return(NULL);
267 }
268 cuddRef(T);
269 E = cuddAddRoundOffRecur(dd,fvn,trunc);
270 if (E == NULL) {
271 Cudd_RecursiveDeref(dd,T);
272 return(NULL);
273 }
274 cuddRef(E);
275 res = (T == E) ? T : cuddUniqueInter(dd,(int)f->index,T,E);
276 if (res == NULL) {
277 Cudd_RecursiveDeref(dd,T);
278 Cudd_RecursiveDeref(dd,E);
279 return(NULL);
280 }
281 cuddDeref(T);
282 cuddDeref(E);
283
284 /* Store result. */
285 cuddCacheInsert1(dd,cacheOp,f,res);
286 return(res);
287
288 } /* end of cuddAddRoundOffRecur */
289
290 /*---------------------------------------------------------------------------*/
291 /* Definition of static functions */
292 /*---------------------------------------------------------------------------*/
293
294
295 ABC_NAMESPACE_IMPL_END
296
297