src/cuBdd/cuddAddNeg.c File Reference

#include "util.h"
#include "cuddInt.h"
Include dependency graph for cuddAddNeg.c:

Go to the source code of this file.

Functions

DdNode * Cudd_addNegate (DdManager *dd, DdNode *f)
DdNode * Cudd_addRoundOff (DdManager *dd, DdNode *f, int N)
DdNode * cuddAddNegateRecur (DdManager *dd, DdNode *f)
DdNode * cuddAddRoundOffRecur (DdManager *dd, DdNode *f, double trunc)

Variables

static char rcsid[] DD_UNUSED = "$Id: cuddAddNeg.c,v 1.12 2009/02/20 02:14:58 fabio Exp $"

Function Documentation

DdNode* Cudd_addNegate ( DdManager *  dd,
DdNode *  f 
)

AutomaticStart AutomaticEnd Function********************************************************************

Synopsis [Computes the additive inverse of an ADD.]

Description [Computes the additive inverse of an ADD. Returns a pointer to the result if successful; NULL otherwise.]

SideEffects [None]

SeeAlso [Cudd_addCmpl]

Definition at line 116 of file cuddAddNeg.c.

00119 {
00120     DdNode *res;
00121 
00122     do {
00123         res = cuddAddNegateRecur(dd,f);
00124     } while (dd->reordered == 1);
00125     return(res);
00126 
00127 } /* end of Cudd_addNegate */

DdNode* Cudd_addRoundOff ( DdManager *  dd,
DdNode *  f,
int  N 
)

Function********************************************************************

Synopsis [Rounds off the discriminants of an ADD.]

Description [Rounds off the discriminants of an ADD. The discriminants are rounded off to N digits after the decimal. Returns a pointer to the result ADD if successful; NULL otherwise.]

SideEffects [None]

SeeAlso []

Definition at line 144 of file cuddAddNeg.c.

00148 {
00149     DdNode *res;
00150     double trunc = pow(10.0,(double)N);
00151 
00152     do {
00153         res = cuddAddRoundOffRecur(dd,f,trunc);
00154     } while (dd->reordered == 1);
00155     return(res);
00156 
00157 } /* end of Cudd_addRoundOff */

DdNode* cuddAddNegateRecur ( DdManager *  dd,
DdNode *  f 
)

Function********************************************************************

Synopsis [Implements the recursive step of Cudd_addNegate.]

Description [Implements the recursive step of Cudd_addNegate. Returns a pointer to the result.]

SideEffects [None]

Definition at line 176 of file cuddAddNeg.c.

00179 {
00180     DdNode *res,
00181             *fv, *fvn,
00182             *T, *E;
00183 
00184     statLine(dd);
00185     /* Check terminal cases. */
00186     if (cuddIsConstant(f)) {
00187         res = cuddUniqueConst(dd,-cuddV(f));
00188         return(res);
00189     }
00190 
00191     /* Check cache */
00192     res = cuddCacheLookup1(dd,Cudd_addNegate,f);
00193     if (res != NULL) return(res);
00194 
00195     /* Recursive Step */
00196     fv = cuddT(f);
00197     fvn = cuddE(f);
00198     T = cuddAddNegateRecur(dd,fv);
00199     if (T == NULL) return(NULL);
00200     cuddRef(T);
00201 
00202     E = cuddAddNegateRecur(dd,fvn);
00203     if (E == NULL) {
00204         Cudd_RecursiveDeref(dd,T);
00205         return(NULL);
00206     }
00207     cuddRef(E);
00208     res = (T == E) ? T : cuddUniqueInter(dd,(int)f->index,T,E);
00209     if (res == NULL) {
00210         Cudd_RecursiveDeref(dd, T);
00211         Cudd_RecursiveDeref(dd, E);
00212         return(NULL);
00213     }
00214     cuddDeref(T);
00215     cuddDeref(E);
00216 
00217     /* Store result. */
00218     cuddCacheInsert1(dd,Cudd_addNegate,f,res);
00219 
00220     return(res);
00221 
00222 } /* end of cuddAddNegateRecur */

DdNode* cuddAddRoundOffRecur ( DdManager *  dd,
DdNode *  f,
double  trunc 
)

Function********************************************************************

Synopsis [Implements the recursive step of Cudd_addRoundOff.]

Description [Implements the recursive step of Cudd_addRoundOff. Returns a pointer to the result.]

SideEffects [None]

Definition at line 236 of file cuddAddNeg.c.

00240 {
00241 
00242     DdNode *res, *fv, *fvn, *T, *E;
00243     double n;
00244     DD_CTFP1 cacheOp;
00245 
00246     statLine(dd);
00247     if (cuddIsConstant(f)) {
00248         n = ceil(cuddV(f)*trunc)/trunc;
00249         res = cuddUniqueConst(dd,n);
00250         return(res);
00251     }
00252     cacheOp = (DD_CTFP1) Cudd_addRoundOff;
00253     res = cuddCacheLookup1(dd,cacheOp,f);
00254     if (res != NULL) {
00255         return(res);
00256     }
00257     /* Recursive Step */
00258     fv = cuddT(f);
00259     fvn = cuddE(f);
00260     T = cuddAddRoundOffRecur(dd,fv,trunc);
00261     if (T == NULL) {
00262        return(NULL);
00263     }
00264     cuddRef(T);
00265     E = cuddAddRoundOffRecur(dd,fvn,trunc);
00266     if (E == NULL) {
00267         Cudd_RecursiveDeref(dd,T);
00268         return(NULL);
00269     }
00270     cuddRef(E);
00271     res = (T == E) ? T : cuddUniqueInter(dd,(int)f->index,T,E);
00272     if (res == NULL) {
00273         Cudd_RecursiveDeref(dd,T);
00274         Cudd_RecursiveDeref(dd,E);
00275         return(NULL);
00276     }
00277     cuddDeref(T);
00278     cuddDeref(E);
00279 
00280     /* Store result. */
00281     cuddCacheInsert1(dd,cacheOp,f,res);
00282     return(res);
00283 
00284 } /* end of cuddAddRoundOffRecur */

Variable Documentation

char rcsid [] DD_UNUSED = "$Id: cuddAddNeg.c,v 1.12 2009/02/20 02:14:58 fabio Exp $" [static]

CFile***********************************************************************

FileName [cuddAddNeg.c]

PackageName [cudd]

Synopsis [Function to compute the negation of an ADD.]

Description [External procedures included in this module:

Internal procedures included in this module:

]

Author [Fabio Somenzi, Balakrishna Kumthekar]

Copyright [Copyright (c) 1995-2004, Regents of the University of Colorado

All rights reserved.

Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met:

Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer.

Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution.

Neither the name of the University of Colorado nor the names of its contributors may be used to endorse or promote products derived from this software without specific prior written permission.

THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.]

Definition at line 80 of file cuddAddNeg.c.

Generated on Tue Jan 12 13:57:17 2010 for glu-2.2 by  doxygen 1.6.1