1 files changed, 262 insertions, 0 deletions
diff --git a/src/bdd/cudd/cuddAddNeg.c b/src/bdd/cudd/cuddAddNeg.c
new file mode 100644
index 00000000..2420df64
--- /dev/null
+++ b/src/bdd/cudd/cuddAddNeg.c
@@ -0,0 +1,262 @@
+/**CFile***********************************************************************
+
+  FileName    [cuddAddNeg.c]
+
+  PackageName [cudd]
+
+  Synopsis    [function to compute the negation of an ADD.]
+
+  Description [External procedures included in this module:
+        <ul>
+        <li> Cudd_addNegate()
+        <li> Cudd_addRoundOff()
+        </ul>
+    Internal procedures included in this module:
+        <ul>
+        <li> cuddAddNegateRecur()
+        <li> cuddAddRoundOffRecur()
+        </ul> ]
+
+  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.]
+
+******************************************************************************/
+
+#include    "util.h"
+#include "cuddInt.h"
+
+
+/*---------------------------------------------------------------------------*/
+/* Constant declarations                                                     */
+/*---------------------------------------------------------------------------*/
+
+
+/*---------------------------------------------------------------------------*/
+/* Stucture declarations                                                     */
+/*---------------------------------------------------------------------------*/
+
+
+/*---------------------------------------------------------------------------*/
+/* Type declarations                                                         */
+/*---------------------------------------------------------------------------*/
+
+
+/*---------------------------------------------------------------------------*/
+/* Variable declarations                                                     */
+/*---------------------------------------------------------------------------*/
+
+#ifndef lint
+static char rcsid[] DD_UNUSED = "$Id: cuddAddNeg.c,v 1.1.1.1 2003/02/24 22:23:50 wjiang Exp $";
+#endif
+
+
+/*---------------------------------------------------------------------------*/
+/* Macro declarations                                                        */
+/*---------------------------------------------------------------------------*/
+
+
+/**AutomaticStart*************************************************************/
+
+/*---------------------------------------------------------------------------*/
+/* Static function prototypes                                                */
+/*---------------------------------------------------------------------------*/
+
+
+/**AutomaticEnd***************************************************************/
+
+
+/*---------------------------------------------------------------------------*/
+/* Definition of exported functions                                          */
+/*---------------------------------------------------------------------------*/
+
+/**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]
+
+******************************************************************************/
+DdNode *
+Cudd_addNegate(
+  DdManager * dd,
+  DdNode * f)
+{
+    DdNode *res;
+
+    do {
+    res = cuddAddNegateRecur(dd,f);
+    } while (dd->reordered == 1);
+    return(res);
+
+} /* end of Cudd_addNegate */
+
+
+/**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     []
+
+******************************************************************************/
+DdNode *
+Cudd_addRoundOff(
+  DdManager * dd,
+  DdNode * f,
+  int  N)
+{
+    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 */
+
+
+/*---------------------------------------------------------------------------*/
+/* Definition of internal functions                                          */
+/*---------------------------------------------------------------------------*/
+
+
+/**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]
+
+******************************************************************************/
+DdNode *
+cuddAddNegateRecur(
+  DdManager * dd,
+  DdNode * f)
+{
+    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 */
+
+
+/**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]
+
+******************************************************************************/
+DdNode *
+cuddAddRoundOffRecur(
+  DdManager * dd,
+  DdNode * f,
+  double  trunc)
+{
+
+    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 */
+
+/*---------------------------------------------------------------------------*/
+/* Definition of static functions                                            */
+/*---------------------------------------------------------------------------*/
+