| [13] | 1 | /**CFile*********************************************************************** | 
|---|
 | 2 |  | 
|---|
 | 3 |   FileName    [cuddAddInv.c] | 
|---|
 | 4 |  | 
|---|
 | 5 |   PackageName [cudd] | 
|---|
 | 6 |  | 
|---|
 | 7 |   Synopsis    [Function to compute the scalar inverse of an ADD.] | 
|---|
 | 8 |  | 
|---|
 | 9 |   Description [External procedures included in this module: | 
|---|
 | 10 |                 <ul> | 
|---|
 | 11 |                 <li> Cudd_addScalarInverse() | 
|---|
 | 12 |                 </ul> | 
|---|
 | 13 |             Internal procedures included in this module: | 
|---|
 | 14 |                 <ul> | 
|---|
 | 15 |                 <li> cuddAddScalarInverseRecur() | 
|---|
 | 16 |                 </ul>] | 
|---|
 | 17 |  | 
|---|
 | 18 |   Author      [Fabio Somenzi] | 
|---|
 | 19 |  | 
|---|
 | 20 |   Copyright   [Copyright (c) 1995-2004, Regents of the University of Colorado | 
|---|
 | 21 |  | 
|---|
 | 22 |   All rights reserved. | 
|---|
 | 23 |  | 
|---|
 | 24 |   Redistribution and use in source and binary forms, with or without | 
|---|
 | 25 |   modification, are permitted provided that the following conditions | 
|---|
 | 26 |   are met: | 
|---|
 | 27 |  | 
|---|
 | 28 |   Redistributions of source code must retain the above copyright | 
|---|
 | 29 |   notice, this list of conditions and the following disclaimer. | 
|---|
 | 30 |  | 
|---|
 | 31 |   Redistributions in binary form must reproduce the above copyright | 
|---|
 | 32 |   notice, this list of conditions and the following disclaimer in the | 
|---|
 | 33 |   documentation and/or other materials provided with the distribution. | 
|---|
 | 34 |  | 
|---|
 | 35 |   Neither the name of the University of Colorado nor the names of its | 
|---|
 | 36 |   contributors may be used to endorse or promote products derived from | 
|---|
 | 37 |   this software without specific prior written permission. | 
|---|
 | 38 |  | 
|---|
 | 39 |   THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS | 
|---|
 | 40 |   "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT | 
|---|
 | 41 |   LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS | 
|---|
 | 42 |   FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE | 
|---|
 | 43 |   COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, | 
|---|
 | 44 |   INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, | 
|---|
 | 45 |   BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; | 
|---|
 | 46 |   LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER | 
|---|
 | 47 |   CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT | 
|---|
 | 48 |   LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN | 
|---|
 | 49 |   ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE | 
|---|
 | 50 |   POSSIBILITY OF SUCH DAMAGE.] | 
|---|
 | 51 |  | 
|---|
 | 52 | ******************************************************************************/ | 
|---|
 | 53 |  | 
|---|
 | 54 | #include "util.h" | 
|---|
 | 55 | #include "cuddInt.h" | 
|---|
 | 56 |  | 
|---|
 | 57 |  | 
|---|
 | 58 | /*---------------------------------------------------------------------------*/ | 
|---|
 | 59 | /* Constant declarations                                                     */ | 
|---|
 | 60 | /*---------------------------------------------------------------------------*/ | 
|---|
 | 61 |  | 
|---|
 | 62 |  | 
|---|
 | 63 | /*---------------------------------------------------------------------------*/ | 
|---|
 | 64 | /* Stucture declarations                                                     */ | 
|---|
 | 65 | /*---------------------------------------------------------------------------*/ | 
|---|
 | 66 |  | 
|---|
 | 67 |  | 
|---|
 | 68 | /*---------------------------------------------------------------------------*/ | 
|---|
 | 69 | /* Type declarations                                                         */ | 
|---|
 | 70 | /*---------------------------------------------------------------------------*/ | 
|---|
 | 71 |  | 
|---|
 | 72 |  | 
|---|
 | 73 | /*---------------------------------------------------------------------------*/ | 
|---|
 | 74 | /* Variable declarations                                                     */ | 
|---|
 | 75 | /*---------------------------------------------------------------------------*/ | 
|---|
 | 76 |  | 
|---|
 | 77 | #ifndef lint | 
|---|
 | 78 | static char rcsid[] DD_UNUSED = "$Id: cuddAddInv.c,v 1.9 2004/08/13 18:04:45 fabio Exp $"; | 
|---|
 | 79 | #endif | 
|---|
 | 80 |  | 
|---|
 | 81 |  | 
|---|
 | 82 | /*---------------------------------------------------------------------------*/ | 
|---|
 | 83 | /* Macro declarations                                                        */ | 
|---|
 | 84 | /*---------------------------------------------------------------------------*/ | 
|---|
 | 85 |  | 
|---|
 | 86 |  | 
|---|
 | 87 | /**AutomaticStart*************************************************************/ | 
|---|
 | 88 |  | 
|---|
 | 89 | /*---------------------------------------------------------------------------*/ | 
|---|
 | 90 | /* Static function prototypes                                                */ | 
|---|
 | 91 | /*---------------------------------------------------------------------------*/ | 
|---|
 | 92 |  | 
|---|
 | 93 |  | 
|---|
 | 94 | /**AutomaticEnd***************************************************************/ | 
|---|
 | 95 |  | 
|---|
 | 96 |  | 
|---|
 | 97 | /*---------------------------------------------------------------------------*/ | 
|---|
 | 98 | /* Definition of exported functions                                          */ | 
|---|
 | 99 | /*---------------------------------------------------------------------------*/ | 
|---|
 | 100 |  | 
|---|
 | 101 |  | 
|---|
 | 102 | /**Function******************************************************************** | 
|---|
 | 103 |  | 
|---|
 | 104 |   Synopsis    [Computes the scalar inverse of an ADD.] | 
|---|
 | 105 |    | 
|---|
 | 106 |   Description [Computes an n ADD where the discriminants are the | 
|---|
 | 107 |   multiplicative inverses of the corresponding discriminants of the | 
|---|
 | 108 |   argument ADD.  Returns a pointer to the resulting ADD in case of | 
|---|
 | 109 |   success. Returns NULL if any discriminants smaller than epsilon is | 
|---|
 | 110 |   encountered.] | 
|---|
 | 111 |  | 
|---|
 | 112 |   SideEffects [None] | 
|---|
 | 113 |  | 
|---|
 | 114 | ******************************************************************************/ | 
|---|
 | 115 | DdNode * | 
|---|
 | 116 | Cudd_addScalarInverse( | 
|---|
 | 117 |   DdManager * dd, | 
|---|
 | 118 |   DdNode * f, | 
|---|
 | 119 |   DdNode * epsilon) | 
|---|
 | 120 | { | 
|---|
 | 121 |     DdNode *res; | 
|---|
 | 122 |  | 
|---|
 | 123 |     if (!cuddIsConstant(epsilon)) { | 
|---|
 | 124 |         (void) fprintf(dd->err,"Invalid epsilon\n"); | 
|---|
 | 125 |         return(NULL); | 
|---|
 | 126 |     } | 
|---|
 | 127 |     do { | 
|---|
 | 128 |         dd->reordered = 0; | 
|---|
 | 129 |         res  = cuddAddScalarInverseRecur(dd,f,epsilon); | 
|---|
 | 130 |     } while (dd->reordered == 1); | 
|---|
 | 131 |     return(res); | 
|---|
 | 132 |  | 
|---|
 | 133 | } /* end of Cudd_addScalarInverse */ | 
|---|
 | 134 |  | 
|---|
 | 135 | /*---------------------------------------------------------------------------*/ | 
|---|
 | 136 | /* Definition of internal functions                                          */ | 
|---|
 | 137 | /*---------------------------------------------------------------------------*/ | 
|---|
 | 138 |  | 
|---|
 | 139 |  | 
|---|
 | 140 | /**Function******************************************************************** | 
|---|
 | 141 |  | 
|---|
 | 142 |   Synopsis    [Performs the recursive step of addScalarInverse.] | 
|---|
 | 143 |  | 
|---|
 | 144 |   Description [Returns a pointer to the resulting ADD in case of | 
|---|
 | 145 |   success. Returns NULL if any discriminants smaller than epsilon is | 
|---|
 | 146 |   encountered.] | 
|---|
 | 147 |  | 
|---|
 | 148 |   SideEffects [None] | 
|---|
 | 149 |  | 
|---|
 | 150 | ******************************************************************************/ | 
|---|
 | 151 | DdNode * | 
|---|
 | 152 | cuddAddScalarInverseRecur( | 
|---|
 | 153 |   DdManager * dd, | 
|---|
 | 154 |   DdNode * f, | 
|---|
 | 155 |   DdNode * epsilon) | 
|---|
 | 156 | { | 
|---|
 | 157 |     DdNode *t, *e, *res; | 
|---|
 | 158 |     CUDD_VALUE_TYPE value; | 
|---|
 | 159 |  | 
|---|
 | 160 |     statLine(dd); | 
|---|
 | 161 |     if (cuddIsConstant(f)) { | 
|---|
 | 162 |         if (ddAbs(cuddV(f)) < cuddV(epsilon)) return(NULL); | 
|---|
 | 163 |         value = 1.0 / cuddV(f); | 
|---|
 | 164 |         res = cuddUniqueConst(dd,value); | 
|---|
 | 165 |         return(res); | 
|---|
 | 166 |     } | 
|---|
 | 167 |  | 
|---|
 | 168 |     res = cuddCacheLookup2(dd,Cudd_addScalarInverse,f,epsilon); | 
|---|
 | 169 |     if (res != NULL) return(res); | 
|---|
 | 170 |  | 
|---|
 | 171 |     t = cuddAddScalarInverseRecur(dd,cuddT(f),epsilon); | 
|---|
 | 172 |     if (t == NULL) return(NULL); | 
|---|
 | 173 |     cuddRef(t); | 
|---|
 | 174 |  | 
|---|
 | 175 |     e = cuddAddScalarInverseRecur(dd,cuddE(f),epsilon); | 
|---|
 | 176 |     if (e == NULL) { | 
|---|
 | 177 |         Cudd_RecursiveDeref(dd, t); | 
|---|
 | 178 |         return(NULL); | 
|---|
 | 179 |     } | 
|---|
 | 180 |     cuddRef(e); | 
|---|
 | 181 |  | 
|---|
 | 182 |     res = (t == e) ? t : cuddUniqueInter(dd,(int)f->index,t,e); | 
|---|
 | 183 |     if (res == NULL) { | 
|---|
 | 184 |         Cudd_RecursiveDeref(dd, t); | 
|---|
 | 185 |         Cudd_RecursiveDeref(dd, e); | 
|---|
 | 186 |         return(NULL); | 
|---|
 | 187 |     } | 
|---|
 | 188 |     cuddDeref(t); | 
|---|
 | 189 |     cuddDeref(e); | 
|---|
 | 190 |  | 
|---|
 | 191 |     cuddCacheInsert2(dd,Cudd_addScalarInverse,f,epsilon,res); | 
|---|
 | 192 |  | 
|---|
 | 193 |     return(res); | 
|---|
 | 194 |  | 
|---|
 | 195 | } /* end of cuddAddScalarInverseRecur */ | 
|---|
 | 196 |  | 
|---|
 | 197 |  | 
|---|
 | 198 | /*---------------------------------------------------------------------------*/ | 
|---|
 | 199 | /* Definition of static functions                                            */ | 
|---|
 | 200 | /*---------------------------------------------------------------------------*/ | 
|---|
 | 201 |  | 
|---|