abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
cuddAddInv.c File Reference
#include "misc/util/util_hack.h"
#include "cuddInt.h"

Go to the source code of this file.

Functions

DdNodeCudd_addScalarInverse (DdManager *dd, DdNode *f, DdNode *epsilon)
 
DdNodecuddAddScalarInverseRecur (DdManager *dd, DdNode *f, DdNode *epsilon)
 

Variables

static
ABC_NAMESPACE_IMPL_START char
rcsid[] 
DD_UNUSED = "$Id: cuddAddInv.c,v 1.9 2004/08/13 18:04:45 fabio 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 120 of file cuddAddInv.c.

124 {
125  DdNode *res;
126 
127  if (!cuddIsConstant(epsilon)) {
128  (void) fprintf(dd->err,"Invalid epsilon\n");
129  return(NULL);
130  }
131  do {
132  dd->reordered = 0;
133  res = cuddAddScalarInverseRecur(dd,f,epsilon);
134  } while (dd->reordered == 1);
135  return(res);
136 
137 } /* end of Cudd_addScalarInverse */
Definition: cudd.h:278
FILE * err
Definition: cuddInt.h:442
int reordered
Definition: cuddInt.h:409
#define cuddIsConstant(node)
Definition: cuddInt.h:620
DdNode * cuddAddScalarInverseRecur(DdManager *dd, DdNode *f, DdNode *epsilon)
Definition: cuddAddInv.c:156
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 156 of file cuddAddInv.c.

160 {
161  DdNode *t, *e, *res;
163 
164  statLine(dd);
165  if (cuddIsConstant(f)) {
166  if (ddAbs(cuddV(f)) < cuddV(epsilon)) return(NULL);
167  value = 1.0 / cuddV(f);
168  res = cuddUniqueConst(dd,value);
169  return(res);
170  }
171 
172  res = cuddCacheLookup2(dd,Cudd_addScalarInverse,f,epsilon);
173  if (res != NULL) return(res);
174 
175  t = cuddAddScalarInverseRecur(dd,cuddT(f),epsilon);
176  if (t == NULL) return(NULL);
177  cuddRef(t);
178 
179  e = cuddAddScalarInverseRecur(dd,cuddE(f),epsilon);
180  if (e == NULL) {
181  Cudd_RecursiveDeref(dd, t);
182  return(NULL);
183  }
184  cuddRef(e);
185 
186  res = (t == e) ? t : cuddUniqueInter(dd,(int)f->index,t,e);
187  if (res == NULL) {
188  Cudd_RecursiveDeref(dd, t);
189  Cudd_RecursiveDeref(dd, e);
190  return(NULL);
191  }
192  cuddDeref(t);
193  cuddDeref(e);
194 
195  cuddCacheInsert2(dd,Cudd_addScalarInverse,f,epsilon,res);
196 
197  return(res);
198 
199 } /* end of cuddAddScalarInverseRecur */
#define cuddRef(n)
Definition: cuddInt.h:584
#define cuddDeref(n)
Definition: cuddInt.h:604
void Cudd_RecursiveDeref(DdManager *table, DdNode *n)
Definition: cuddRef.c:154
Definition: cudd.h:278
void cuddCacheInsert2(DdManager *table, DD_CTFP op, DdNode *f, DdNode *g, DdNode *data)
Definition: cuddCache.c:277
DdNode * cuddUniqueConst(DdManager *unique, CUDD_VALUE_TYPE value)
Definition: cuddTable.c:1450
#define statLine(dd)
Definition: cuddInt.h:1037
#define cuddV(node)
Definition: cuddInt.h:668
DdNode * cuddCacheLookup2(DdManager *table, DD_CTFP op, DdNode *f, DdNode *g)
Definition: cuddCache.c:502
#define ddAbs(x)
Definition: cuddInt.h:846
#define cuddIsConstant(node)
Definition: cuddInt.h:620
#define cuddT(node)
Definition: cuddInt.h:636
#define CUDD_VALUE_TYPE
Definition: cudd.h:94
DdNode * cuddAddScalarInverseRecur(DdManager *dd, DdNode *f, DdNode *epsilon)
Definition: cuddAddInv.c:156
DdHalfWord index
Definition: cudd.h:279
#define cuddE(node)
Definition: cuddInt.h:652
int value
DdNode * Cudd_addScalarInverse(DdManager *dd, DdNode *f, DdNode *epsilon)
Definition: cuddAddInv.c:120
DdNode * cuddUniqueInter(DdManager *unique, int index, DdNode *T, DdNode *E)
Definition: cuddTable.c:1128

Variable Documentation

ABC_NAMESPACE_IMPL_START char rcsid [] DD_UNUSED = "$Id: cuddAddInv.c,v 1.9 2004/08/13 18:04:45 fabio 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:

Internal procedures included in this module:

]

Author [Fabio Somenzi]

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