src/bdd/cudd/cuddAddInv.c File Reference

#include "util_hack.h"
#include "cuddInt.h"

Include dependency graph for cuddAddInv.c:

Go to the source code of this file.

Functions
DdNode *	Cudd_addScalarInverse (DdManager *dd, DdNode *f, DdNode *epsilon)
DdNode *	cuddAddScalarInverseRecur (DdManager *dd, DdNode *f, DdNode *epsilon)
Variables
static char rcsid[]	DD_UNUSED = "$Id: cuddAddInv.c,v 1.1.1.1 2003/02/24 22:23:50 wjiang Exp $"

---

Function Documentation

DdNode* Cudd_addScalarInverse	(	DdManager *	dd,
		DdNode *	f,
		DdNode *	epsilon
	)

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

Synopsis [Computes the scalar inverse of an ADD.]

Description [Computes an n ADD where the discriminants are the multiplicative inverses of the corresponding discriminants of the argument ADD. Returns a pointer to the resulting ADD in case of success. Returns NULL if any discriminants smaller than epsilon is encountered.]

SideEffects [None]

Definition at line 89 of file cuddAddInv.c.

{
    DdNode *res;

    if (!cuddIsConstant(epsilon)) {
        (void) fprintf(dd->err,"Invalid epsilon\n");
        return(NULL);
    }
    do {
        dd->reordered = 0;
        res  = cuddAddScalarInverseRecur(dd,f,epsilon);
    } while (dd->reordered == 1);
    return(res);

} /* end of Cudd_addScalarInverse */

DdNode* cuddAddScalarInverseRecur	(	DdManager *	dd,
		DdNode *	f,
		DdNode *	epsilon
	)

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

Synopsis [Performs the recursive step of addScalarInverse.]

Description [Returns a pointer to the resulting ADD in case of success. Returns NULL if any discriminants smaller than epsilon is encountered.]

SideEffects [None]

Definition at line 125 of file cuddAddInv.c.

{
    DdNode *t, *e, *res;
    CUDD_VALUE_TYPE value;

    statLine(dd);
    if (cuddIsConstant(f)) {
        if (ddAbs(cuddV(f)) < cuddV(epsilon)) return(NULL);
        value = 1.0 / cuddV(f);
        res = cuddUniqueConst(dd,value);
        return(res);
    }

    res = cuddCacheLookup2(dd,Cudd_addScalarInverse,f,epsilon);
    if (res != NULL) return(res);

    t = cuddAddScalarInverseRecur(dd,cuddT(f),epsilon);
    if (t == NULL) return(NULL);
    cuddRef(t);

    e = cuddAddScalarInverseRecur(dd,cuddE(f),epsilon);
    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);
    }

    cuddCacheInsert2(dd,Cudd_addScalarInverse,f,epsilon,res);

    return(res);

} /* end of cuddAddScalarInverseRecur */

---

Variable Documentation

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

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

FileName [cuddAddInv.c]

PackageName [cudd]

Synopsis [Function to compute the scalar inverse of an ADD.]

Description [External procedures included in this module:

• Cudd_addScalarInverse()

Internal procedures included in this module:

• cuddAddScalarInverseRecur()

]

Author [Fabio Somenzi]

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 51 of file cuddAddInv.c.