source: vis_dev/glu-2.3/src/cuBdd/cuddAddNeg.c@ 33

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

library glu 2.3
File size: 8.4 KB
RevLine 
[13]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 "util.h"
57#include "cuddInt.h"
58
59
60/*---------------------------------------------------------------------------*/
61/* Constant declarations */
62/*---------------------------------------------------------------------------*/
63
64
65/*---------------------------------------------------------------------------*/
66/* Stucture declarations */
67/*---------------------------------------------------------------------------*/
68
69
70/*---------------------------------------------------------------------------*/
71/* Type declarations */
72/*---------------------------------------------------------------------------*/
73
74
75/*---------------------------------------------------------------------------*/
76/* Variable declarations */
77/*---------------------------------------------------------------------------*/
78
79#ifndef lint
80static char rcsid[] DD_UNUSED = "$Id: cuddAddNeg.c,v 1.12 2009/02/20 02:14:58 fabio Exp $";
81#endif
82
83
84/*---------------------------------------------------------------------------*/
85/* Macro declarations */
86/*---------------------------------------------------------------------------*/
87
88
89/**AutomaticStart*************************************************************/
90
91/*---------------------------------------------------------------------------*/
92/* Static function prototypes */
93/*---------------------------------------------------------------------------*/
94
95
96/**AutomaticEnd***************************************************************/
97
98
99/*---------------------------------------------------------------------------*/
100/* Definition of exported functions */
101/*---------------------------------------------------------------------------*/
102
103/**Function********************************************************************
104
105 Synopsis [Computes the additive inverse of an ADD.]
106
107 Description [Computes the additive inverse of an ADD. Returns a pointer
108 to the result if successful; NULL otherwise.]
109
110 SideEffects [None]
111
112 SeeAlso [Cudd_addCmpl]
113
114******************************************************************************/
115DdNode *
116Cudd_addNegate(
117 DdManager * dd,
118 DdNode * f)
119{
120 DdNode *res;
121
122 do {
123 res = cuddAddNegateRecur(dd,f);
124 } while (dd->reordered == 1);
125 return(res);
126
127} /* end of Cudd_addNegate */
128
129
130/**Function********************************************************************
131
132 Synopsis [Rounds off the discriminants of an ADD.]
133
134 Description [Rounds off the discriminants of an ADD. The discriminants are
135 rounded off to N digits after the decimal. Returns a pointer to the result
136 ADD if successful; NULL otherwise.]
137
138 SideEffects [None]
139
140 SeeAlso []
141
142******************************************************************************/
143DdNode *
144Cudd_addRoundOff(
145 DdManager * dd,
146 DdNode * f,
147 int N)
148{
149 DdNode *res;
150 double trunc = pow(10.0,(double)N);
151
152 do {
153 res = cuddAddRoundOffRecur(dd,f,trunc);
154 } while (dd->reordered == 1);
155 return(res);
156
157} /* end of Cudd_addRoundOff */
158
159
160/*---------------------------------------------------------------------------*/
161/* Definition of internal functions */
162/*---------------------------------------------------------------------------*/
163
164
165/**Function********************************************************************
166
167 Synopsis [Implements the recursive step of Cudd_addNegate.]
168
169 Description [Implements the recursive step of Cudd_addNegate.
170 Returns a pointer to the result.]
171
172 SideEffects [None]
173
174******************************************************************************/
175DdNode *
176cuddAddNegateRecur(
177 DdManager * dd,
178 DdNode * f)
179{
180 DdNode *res,
181 *fv, *fvn,
182 *T, *E;
183
184 statLine(dd);
185 /* Check terminal cases. */
186 if (cuddIsConstant(f)) {
187 res = cuddUniqueConst(dd,-cuddV(f));
188 return(res);
189 }
190
191 /* Check cache */
192 res = cuddCacheLookup1(dd,Cudd_addNegate,f);
193 if (res != NULL) return(res);
194
195 /* Recursive Step */
196 fv = cuddT(f);
197 fvn = cuddE(f);
198 T = cuddAddNegateRecur(dd,fv);
199 if (T == NULL) return(NULL);
200 cuddRef(T);
201
202 E = cuddAddNegateRecur(dd,fvn);
203 if (E == NULL) {
204 Cudd_RecursiveDeref(dd,T);
205 return(NULL);
206 }
207 cuddRef(E);
208 res = (T == E) ? T : cuddUniqueInter(dd,(int)f->index,T,E);
209 if (res == NULL) {
210 Cudd_RecursiveDeref(dd, T);
211 Cudd_RecursiveDeref(dd, E);
212 return(NULL);
213 }
214 cuddDeref(T);
215 cuddDeref(E);
216
217 /* Store result. */
218 cuddCacheInsert1(dd,Cudd_addNegate,f,res);
219
220 return(res);
221
222} /* end of cuddAddNegateRecur */
223
224
225/**Function********************************************************************
226
227 Synopsis [Implements the recursive step of Cudd_addRoundOff.]
228
229 Description [Implements the recursive step of Cudd_addRoundOff.
230 Returns a pointer to the result.]
231
232 SideEffects [None]
233
234******************************************************************************/
235DdNode *
236cuddAddRoundOffRecur(
237 DdManager * dd,
238 DdNode * f,
239 double trunc)
240{
241
242 DdNode *res, *fv, *fvn, *T, *E;
243 double n;
244 DD_CTFP1 cacheOp;
245
246 statLine(dd);
247 if (cuddIsConstant(f)) {
248 n = ceil(cuddV(f)*trunc)/trunc;
249 res = cuddUniqueConst(dd,n);
250 return(res);
251 }
252 cacheOp = (DD_CTFP1) Cudd_addRoundOff;
253 res = cuddCacheLookup1(dd,cacheOp,f);
254 if (res != NULL) {
255 return(res);
256 }
257 /* Recursive Step */
258 fv = cuddT(f);
259 fvn = cuddE(f);
260 T = cuddAddRoundOffRecur(dd,fv,trunc);
261 if (T == NULL) {
262 return(NULL);
263 }
264 cuddRef(T);
265 E = cuddAddRoundOffRecur(dd,fvn,trunc);
266 if (E == NULL) {
267 Cudd_RecursiveDeref(dd,T);
268 return(NULL);
269 }
270 cuddRef(E);
271 res = (T == E) ? T : cuddUniqueInter(dd,(int)f->index,T,E);
272 if (res == NULL) {
273 Cudd_RecursiveDeref(dd,T);
274 Cudd_RecursiveDeref(dd,E);
275 return(NULL);
276 }
277 cuddDeref(T);
278 cuddDeref(E);
279
280 /* Store result. */
281 cuddCacheInsert1(dd,cacheOp,f,res);
282 return(res);
283
284} /* end of cuddAddRoundOffRecur */
285
286/*---------------------------------------------------------------------------*/
287/* Definition of static functions */
288/*---------------------------------------------------------------------------*/
Note: See TracBrowser for help on using the repository browser.