summaryrefslogtreecommitdiffstats
path: root/src/bdd/cudd/cuddAddFind.c
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2007-10-01 08:01:00 -0700
committerAlan Mishchenko <alanmi@berkeley.edu>2007-10-01 08:01:00 -0700
commit4812c90424dfc40d26725244723887a2d16ddfd9 (patch)
treeb32ace96e7e2d84d586e09ba605463b6f49c3271 /src/bdd/cudd/cuddAddFind.c
parente54d9691616b9a0326e2fdb3156bb4eeb8abfcd7 (diff)
downloadabc-4812c90424dfc40d26725244723887a2d16ddfd9.tar.gz
abc-4812c90424dfc40d26725244723887a2d16ddfd9.tar.bz2
abc-4812c90424dfc40d26725244723887a2d16ddfd9.zip
Version abc71001
Diffstat (limited to 'src/bdd/cudd/cuddAddFind.c')
-rw-r--r--src/bdd/cudd/cuddAddFind.c283
1 files changed, 283 insertions, 0 deletions
diff --git a/src/bdd/cudd/cuddAddFind.c b/src/bdd/cudd/cuddAddFind.c
new file mode 100644
index 00000000..0469b014
--- /dev/null
+++ b/src/bdd/cudd/cuddAddFind.c
@@ -0,0 +1,283 @@
+/**CFile***********************************************************************
+
+ FileName [cuddAddFind.c]
+
+ PackageName [cudd]
+
+ Synopsis [Functions to find maximum and minimum in an ADD and to
+ extract the i-th bit.]
+
+ Description [External procedures included in this module:
+ <ul>
+ <li> Cudd_addFindMax()
+ <li> Cudd_addFindMin()
+ <li> Cudd_addIthBit()
+ </ul>
+ Static functions included in this module:
+ <ul>
+ <li> addDoIthBit()
+ </ul>]
+
+ 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.]
+
+******************************************************************************/
+
+#include "util_hack.h"
+#include "cuddInt.h"
+
+/*---------------------------------------------------------------------------*/
+/* Constant declarations */
+/*---------------------------------------------------------------------------*/
+
+
+/*---------------------------------------------------------------------------*/
+/* Stucture declarations */
+/*---------------------------------------------------------------------------*/
+
+
+/*---------------------------------------------------------------------------*/
+/* Type declarations */
+/*---------------------------------------------------------------------------*/
+
+
+/*---------------------------------------------------------------------------*/
+/* Variable declarations */
+/*---------------------------------------------------------------------------*/
+
+#ifndef lint
+static char rcsid[] DD_UNUSED = "$Id: cuddAddFind.c,v 1.1.1.1 2003/02/24 22:23:50 wjiang Exp $";
+#endif
+
+
+/*---------------------------------------------------------------------------*/
+/* Macro declarations */
+/*---------------------------------------------------------------------------*/
+
+
+/**AutomaticStart*************************************************************/
+
+/*---------------------------------------------------------------------------*/
+/* Static function prototypes */
+/*---------------------------------------------------------------------------*/
+
+static DdNode * addDoIthBit ARGS((DdManager *dd, DdNode *f, DdNode *index));
+
+/**AutomaticEnd***************************************************************/
+
+
+/*---------------------------------------------------------------------------*/
+/* Definition of exported functions */
+/*---------------------------------------------------------------------------*/
+
+/**Function********************************************************************
+
+ Synopsis [Finds the maximum discriminant of f.]
+
+ Description [Returns a pointer to a constant ADD.]
+
+ SideEffects [None]
+
+******************************************************************************/
+DdNode *
+Cudd_addFindMax(
+ DdManager * dd,
+ DdNode * f)
+{
+ DdNode *t, *e, *res;
+
+ statLine(dd);
+ if (cuddIsConstant(f)) {
+ return(f);
+ }
+
+ res = cuddCacheLookup1(dd,Cudd_addFindMax,f);
+ if (res != NULL) {
+ return(res);
+ }
+
+ t = Cudd_addFindMax(dd,cuddT(f));
+ if (t == DD_PLUS_INFINITY(dd)) return(t);
+
+ e = Cudd_addFindMax(dd,cuddE(f));
+
+ res = (cuddV(t) >= cuddV(e)) ? t : e;
+
+ cuddCacheInsert1(dd,Cudd_addFindMax,f,res);
+
+ return(res);
+
+} /* end of Cudd_addFindMax */
+
+
+/**Function********************************************************************
+
+ Synopsis [Finds the minimum discriminant of f.]
+
+ Description [Returns a pointer to a constant ADD.]
+
+ SideEffects [None]
+
+******************************************************************************/
+DdNode *
+Cudd_addFindMin(
+ DdManager * dd,
+ DdNode * f)
+{
+ DdNode *t, *e, *res;
+
+ statLine(dd);
+ if (cuddIsConstant(f)) {
+ return(f);
+ }
+
+ res = cuddCacheLookup1(dd,Cudd_addFindMin,f);
+ if (res != NULL) {
+ return(res);
+ }
+
+ t = Cudd_addFindMin(dd,cuddT(f));
+ if (t == DD_MINUS_INFINITY(dd)) return(t);
+
+ e = Cudd_addFindMin(dd,cuddE(f));
+
+ res = (cuddV(t) <= cuddV(e)) ? t : e;
+
+ cuddCacheInsert1(dd,Cudd_addFindMin,f,res);
+
+ return(res);
+
+} /* end of Cudd_addFindMin */
+
+
+/**Function********************************************************************
+
+ Synopsis [Extracts the i-th bit from an ADD.]
+
+ Description [Produces an ADD from another ADD by replacing all
+ discriminants whose i-th bit is equal to 1 with 1, and all other
+ discriminants with 0. The i-th bit refers to the integer
+ representation of the leaf value. If the value is has a fractional
+ part, it is ignored. Repeated calls to this procedure allow one to
+ transform an integer-valued ADD into an array of ADDs, one for each
+ bit of the leaf values. Returns a pointer to the resulting ADD if
+ successful; NULL otherwise.]
+
+ SideEffects [None]
+
+ SeeAlso [Cudd_addBddIthBit]
+
+******************************************************************************/
+DdNode *
+Cudd_addIthBit(
+ DdManager * dd,
+ DdNode * f,
+ int bit)
+{
+ DdNode *res;
+ DdNode *index;
+
+ /* Use a constant node to remember the bit, so that we can use the
+ ** global cache.
+ */
+ index = cuddUniqueConst(dd,(CUDD_VALUE_TYPE) bit);
+ if (index == NULL) return(NULL);
+ cuddRef(index);
+
+ do {
+ dd->reordered = 0;
+ res = addDoIthBit(dd, f, index);
+ } while (dd->reordered == 1);
+
+ if (res == NULL) {
+ Cudd_RecursiveDeref(dd, index);
+ return(NULL);
+ }
+ cuddRef(res);
+ Cudd_RecursiveDeref(dd, index);
+ cuddDeref(res);
+ return(res);
+
+} /* end of Cudd_addIthBit */
+
+
+/*---------------------------------------------------------------------------*/
+/* Definition of internal functions */
+/*---------------------------------------------------------------------------*/
+
+
+/*---------------------------------------------------------------------------*/
+/* Definition of static functions */
+/*---------------------------------------------------------------------------*/
+
+
+/**Function********************************************************************
+
+ Synopsis [Performs the recursive step for Cudd_addIthBit.]
+
+ Description [Performs the recursive step for Cudd_addIthBit.
+ Returns a pointer to the BDD if successful; NULL otherwise.]
+
+ SideEffects [None]
+
+ SeeAlso []
+
+******************************************************************************/
+static DdNode *
+addDoIthBit(
+ DdManager * dd,
+ DdNode * f,
+ DdNode * index)
+{
+ DdNode *res, *T, *E;
+ DdNode *fv, *fvn;
+ int mask, value;
+ int v;
+
+ statLine(dd);
+ /* Check terminal case. */
+ if (cuddIsConstant(f)) {
+ mask = 1 << ((int) cuddV(index));
+ value = (int) cuddV(f);
+ return((value & mask) == 0 ? DD_ZERO(dd) : DD_ONE(dd));
+ }
+
+ /* Check cache. */
+ res = cuddCacheLookup2(dd,addDoIthBit,f,index);
+ if (res != NULL) return(res);
+
+ /* Recursive step. */
+ v = f->index;
+ fv = cuddT(f); fvn = cuddE(f);
+
+ T = addDoIthBit(dd,fv,index);
+ if (T == NULL) return(NULL);
+ cuddRef(T);
+
+ E = addDoIthBit(dd,fvn,index);
+ if (E == NULL) {
+ Cudd_RecursiveDeref(dd, T);
+ return(NULL);
+ }
+ cuddRef(E);
+
+ res = (T == E) ? T : cuddUniqueInter(dd,v,T,E);
+ if (res == NULL) {
+ Cudd_RecursiveDeref(dd, T);
+ Cudd_RecursiveDeref(dd, E);
+ return(NULL);
+ }
+ cuddDeref(T);
+ cuddDeref(E);
+
+ /* Store result. */
+ cuddCacheInsert2(dd,addDoIthBit,f,index,res);
+
+ return(res);
+
+} /* end of addDoIthBit */
+