src/bdd/cudd/cuddAddNeg.c File Reference

#include "util_hack.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.1.1.1 2003/02/24 22:23:50 wjiang 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 89 of file cuddAddNeg.c.

{
    DdNode *res;

    do {
        res = cuddAddNegateRecur(dd,f);
    } while (dd->reordered == 1);
    return(res);

} /* 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 117 of file cuddAddNeg.c.

{
    DdNode *res;
    double trunc = pow(10.0,(double)N);

    do {
        res = cuddAddRoundOffRecur(dd,f,trunc);
    } while (dd->reordered == 1);
    return(res);

} /* 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 149 of file cuddAddNeg.c.

{
    DdNode *res,
            *fv, *fvn,
            *T, *E;

    statLine(dd);
    /* Check terminal cases. */
    if (cuddIsConstant(f)) {
        res = cuddUniqueConst(dd,-cuddV(f));
        return(res);
    }

    /* Check cache */
    res = cuddCacheLookup1(dd,Cudd_addNegate,f);
    if (res != NULL) return(res);

    /* Recursive Step */
    fv = cuddT(f);
    fvn = cuddE(f);
    T = cuddAddNegateRecur(dd,fv);
    if (T == NULL) return(NULL);
    cuddRef(T);

    E = cuddAddNegateRecur(dd,fvn);
    if (E == NULL) {
        Cudd_RecursiveDeref(dd,T);
        return(NULL);
    }
    cuddRef(E);
    res = (T == E) ? T : cuddUniqueInter(dd,(int)f->index,T,E);
    if (res == NULL) {
        Cudd_RecursiveDeref(dd, T);
        Cudd_RecursiveDeref(dd, E);
        return(NULL);
    }
    cuddDeref(T);
    cuddDeref(E);

    /* Store result. */
    cuddCacheInsert1(dd,Cudd_addNegate,f,res);

    return(res);

} /* 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 209 of file cuddAddNeg.c.

{

    DdNode *res, *fv, *fvn, *T, *E;
    double n;
    DdNode *(*cacheOp)(DdManager *, DdNode *);
  
    statLine(dd);
    if (cuddIsConstant(f)) {
        n = ceil(cuddV(f)*trunc)/trunc;
        res = cuddUniqueConst(dd,n);
        return(res);
    }
    cacheOp = (DdNode *(*)(DdManager *, DdNode *)) Cudd_addRoundOff;
    res = cuddCacheLookup1(dd,cacheOp,f);
    if (res != NULL) {
        return(res);
    }
    /* Recursive Step */
    fv = cuddT(f);
    fvn = cuddE(f);
    T = cuddAddRoundOffRecur(dd,fv,trunc);
    if (T == NULL) {
       return(NULL);
    }
    cuddRef(T);
    E = cuddAddRoundOffRecur(dd,fvn,trunc);
    if (E == NULL) {
        Cudd_RecursiveDeref(dd,T);
        return(NULL);
    }
    cuddRef(E);
    res = (T == E) ? T : cuddUniqueInter(dd,(int)f->index,T,E);
    if (res == NULL) {
        Cudd_RecursiveDeref(dd,T);
        Cudd_RecursiveDeref(dd,E);
        return(NULL);
    }
    cuddDeref(T);
    cuddDeref(E);

    /* Store result. */
    cuddCacheInsert1(dd,cacheOp,f,res);
    return(res);
  
} /* end of cuddAddRoundOffRecur */

---

Variable Documentation

char rcsid [] DD_UNUSED = "$Id: cuddAddNeg.c,v 1.1.1.1 2003/02/24 22:23:50 wjiang Exp $" [static]

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

FileName [cuddAddNeg.c]

PackageName [cudd]

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

Description [External procedures included in this module:

• Cudd_addNegate()
• Cudd_addRoundOff()

Internal procedures included in this module:

• cuddAddNegateRecur()
• cuddAddRoundOffRecur()

]

Author [Fabio Somenzi, Balakrishna Kumthekar]

Copyright [This file was created at the University of Colorado at Boulder. The University of Colorado at Boulder makes no warranty about the suitability of this software for any purpose. It is presented on an AS IS basis.]

Definition at line 53 of file cuddAddNeg.c.