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

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

library glu 2.3
File size: 8.4 KB
Line 
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.