distr/cudd/cuddAddNeg.c

   1 /**CFile***********************************************************************
   2
   3   FileName    [cuddAddNeg.c]
   4
   5   PackageName [cudd]
   6
   7   Synopsis    [Function to compute the negation of an ADD.]
   8
   9   Description [External procedures included in this module:
  10                 <ul>
  11                 <li> Cudd_addNegate()
  12                 <li> Cudd_addRoundOff()
  13                 </ul>
  14         Internal procedures included in this module:
  15                 <ul>
  16                 <li> cuddAddNegateRecur()
  17                 <li> cuddAddRoundOffRecur()
  18                 </ul> ]
  19
  20   Author      [Fabio Somenzi, Balakrishna Kumthekar]
  21
  22   Copyright   [Copyright (c) 1995-2004, Regents of the University of Colorado
  23
  24   All rights reserved.
  25
  26   Redistribution and use in source and binary forms, with or without
  27   modification, are permitted provided that the following conditions
  28   are met:
  29
  30   Redistributions of source code must retain the above copyright
  31   notice, this list of conditions and the following disclaimer.
  32
  33   Redistributions in binary form must reproduce the above copyright
  34   notice, this list of conditions and the following disclaimer in the
  35   documentation and/or other materials provided with the distribution.
  36
  37   Neither the name of the University of Colorado nor the names of its
  38   contributors may be used to endorse or promote products derived from
  39   this software without specific prior written permission.
  40
  41   THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
  42   "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
  43   LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
  44   FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
  45   COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
  46   INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
  47   BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
  48   LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
  49   CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
  50   LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
  51   ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
  52   POSSIBILITY OF SUCH DAMAGE.]
  53
  54 ******************************************************************************/
  55
  56 #include "util.h"
  57 #include "cuddInt.h"
  58
  59
  60 /*---------------------------------------------------------------------------*/
  61 /* Constant declarations                                                     */
  62 /*---------------------------------------------------------------------------*/
  63
  64
  65 /*---------------------------------------------------------------------------*/
  66 /* Stucture declarations                                                     */
  67 /*---------------------------------------------------------------------------*/
  68
  69
  70 /*---------------------------------------------------------------------------*/
  71 /* Type declarations                                                         */
  72 /*---------------------------------------------------------------------------*/
  73
  74
  75 /*---------------------------------------------------------------------------*/
  76 /* Variable declarations                                                     */
  77 /*---------------------------------------------------------------------------*/
  78
  79 #ifndef lint
  80 static char rcsid[] DD_UNUSED = "$Id: cuddAddNeg.c,v 1.12 2009/02/20 02:14:58 fabio Exp $";
  81 #endif
  82
  83
  84 /*---------------------------------------------------------------------------*/
  85 /* Macro declarations                                                        */
  86 /*---------------------------------------------------------------------------*/
  87
  88
  89 /**AutomaticStart*************************************************************/
  90
  91 /*---------------------------------------------------------------------------*/
  92 /* Static function prototypes                                                */
  93 /*---------------------------------------------------------------------------*/
  94
  95
  96 /**AutomaticEnd***************************************************************/
  97
  98
  99 /*---------------------------------------------------------------------------*/
 100 /* Definition of exported functions                                          */
 101 /*---------------------------------------------------------------------------*/
 102
 103 /**Function********************************************************************
 104
 105   Synopsis    [Computes the additive inverse of an ADD.]
 106
 107   Description [Computes the additive inverse of an ADD. Returns a pointer
 108   to the result if successful; NULL otherwise.]
 109
 110   SideEffects [None]
 111
 112   SeeAlso     [Cudd_addCmpl]
 113
 114 ******************************************************************************/
 115 DdNode *
 116 Cudd_addNegate(
 117   DdManager * dd,
 118   DdNode * f)
 119 {
 120     DdNode *res;
 121
 122     do {
 123         res = cuddAddNegateRecur(dd,f);
 124     } while (dd->reordered == 1);
 125     return(res);
 126
 127 } /* end of Cudd_addNegate */
 128
 129
 130 /**Function********************************************************************
 131
 132   Synopsis    [Rounds off the discriminants of an ADD.]
 133
 134   Description [Rounds off the discriminants of an ADD. The discriminants are
 135   rounded off to N digits after the decimal. Returns a pointer to the result
 136   ADD if successful; NULL otherwise.]
 137
 138   SideEffects [None]
 139
 140   SeeAlso     []
 141
 142 ******************************************************************************/
 143 DdNode *
 144 Cudd_addRoundOff(
 145   DdManager * dd,
 146   DdNode * f,
 147   int  N)
 148 {
 149     DdNode *res;
 150     double trunc = pow(10.0,(double)N);
 151
 152     do {
 153         res = cuddAddRoundOffRecur(dd,f,trunc);
 154     } while (dd->reordered == 1);
 155     return(res);
 156
 157 } /* end of Cudd_addRoundOff */
 158
 159
 160 /*---------------------------------------------------------------------------*/
 161 /* Definition of internal functions                                          */
 162 /*---------------------------------------------------------------------------*/
 163
 164
 165 /**Function********************************************************************
 166
 167   Synopsis    [Implements the recursive step of Cudd_addNegate.]
 168
 169   Description [Implements the recursive step of Cudd_addNegate.
 170   Returns a pointer to the result.]
 171
 172   SideEffects [None]
 173
 174 ******************************************************************************/
 175 DdNode *
 176 cuddAddNegateRecur(
 177   DdManager * dd,
 178   DdNode * f)
 179 {
 180     DdNode *res,
 181             *fv, *fvn,
 182             *T, *E;
 183
 184     statLine(dd);
 185     /* Check terminal cases. */
 186     if (cuddIsConstant(f)) {
 187         res = cuddUniqueConst(dd,-cuddV(f));
 188         return(res);
 189     }
 190
 191     /* Check cache */
 192     res = cuddCacheLookup1(dd,Cudd_addNegate,f);
 193     if (res != NULL) return(res);
 194
 195     /* Recursive Step */
 196     fv = cuddT(f);
 197     fvn = cuddE(f);
 198     T = cuddAddNegateRecur(dd,fv);
 199     if (T == NULL) return(NULL);
 200     cuddRef(T);
 201
 202     E = cuddAddNegateRecur(dd,fvn);
 203     if (E == NULL) {
 204         Cudd_RecursiveDeref(dd,T);
 205         return(NULL);
 206     }
 207     cuddRef(E);
 208     res = (T == E) ? T : cuddUniqueInter(dd,(int)f->index,T,E);
 209     if (res == NULL) {
 210         Cudd_RecursiveDeref(dd, T);
 211         Cudd_RecursiveDeref(dd, E);
 212         return(NULL);
 213     }
 214     cuddDeref(T);
 215     cuddDeref(E);
 216
 217     /* Store result. */
 218     cuddCacheInsert1(dd,Cudd_addNegate,f,res);
 219
 220     return(res);
 221
 222 } /* end of cuddAddNegateRecur */
 223
 224
 225 /**Function********************************************************************
 226
 227   Synopsis    [Implements the recursive step of Cudd_addRoundOff.]
 228
 229   Description [Implements the recursive step of Cudd_addRoundOff.
 230   Returns a pointer to the result.]
 231
 232   SideEffects [None]
 233
 234 ******************************************************************************/
 235 DdNode *
 236 cuddAddRoundOffRecur(
 237   DdManager * dd,
 238   DdNode * f,
 239   double  trunc)
 240 {
 241
 242     DdNode *res, *fv, *fvn, *T, *E;
 243     double n;
 244     DD_CTFP1 cacheOp;
 245
 246     statLine(dd);
 247     if (cuddIsConstant(f)) {
 248         n = ceil(cuddV(f)*trunc)/trunc;
 249         res = cuddUniqueConst(dd,n);
 250         return(res);
 251     }
 252     cacheOp = (DD_CTFP1) Cudd_addRoundOff;
 253     res = cuddCacheLookup1(dd,cacheOp,f);
 254     if (res != NULL) {
 255         return(res);
 256     }
 257     /* Recursive Step */
 258     fv = cuddT(f);
 259     fvn = cuddE(f);
 260     T = cuddAddRoundOffRecur(dd,fv,trunc);
 261     if (T == NULL) {
 262        return(NULL);
 263     }
 264     cuddRef(T);
 265     E = cuddAddRoundOffRecur(dd,fvn,trunc);
 266     if (E == NULL) {
 267         Cudd_RecursiveDeref(dd,T);
 268         return(NULL);
 269     }
 270     cuddRef(E);
 271     res = (T == E) ? T : cuddUniqueInter(dd,(int)f->index,T,E);
 272     if (res == NULL) {
 273         Cudd_RecursiveDeref(dd,T);
 274         Cudd_RecursiveDeref(dd,E);
 275         return(NULL);
 276     }
 277     cuddDeref(T);
 278     cuddDeref(E);
 279
 280     /* Store result. */
 281     cuddCacheInsert1(dd,cacheOp,f,res);
 282     return(res);
 283
 284 } /* end of cuddAddRoundOffRecur */
 285
 286 /*---------------------------------------------------------------------------*/
 287 /* Definition of static functions                                            */
 288 /*---------------------------------------------------------------------------*/