glu-2.2: src/cuBdd/cuddAddNeg.c Source File

00001 
00056 #include "util.h"
00057 #include "cuddInt.h"
00058 
00059 
00060 /*---------------------------------------------------------------------------*/
00061 /* Constant declarations                                                     */
00062 /*---------------------------------------------------------------------------*/
00063 
00064 
00065 /*---------------------------------------------------------------------------*/
00066 /* Stucture declarations                                                     */
00067 /*---------------------------------------------------------------------------*/
00068 
00069 
00070 /*---------------------------------------------------------------------------*/
00071 /* Type declarations                                                         */
00072 /*---------------------------------------------------------------------------*/
00073 
00074 
00075 /*---------------------------------------------------------------------------*/
00076 /* Variable declarations                                                     */
00077 /*---------------------------------------------------------------------------*/
00078 
00079 #ifndef lint
00080 static char rcsid[] DD_UNUSED = "$Id: cuddAddNeg.c,v 1.12 2009/02/20 02:14:58 fabio Exp $";
00081 #endif
00082 
00083 
00084 /*---------------------------------------------------------------------------*/
00085 /* Macro declarations                                                        */
00086 /*---------------------------------------------------------------------------*/
00087 
00088 
00091 /*---------------------------------------------------------------------------*/
00092 /* Static function prototypes                                                */
00093 /*---------------------------------------------------------------------------*/
00094 
00095 
00099 /*---------------------------------------------------------------------------*/
00100 /* Definition of exported functions                                          */
00101 /*---------------------------------------------------------------------------*/
00102 
00115 DdNode *
00116 Cudd_addNegate(
00117   DdManager * dd,
00118   DdNode * f)
00119 {
00120     DdNode *res;
00121 
00122     do {
00123         res = cuddAddNegateRecur(dd,f);
00124     } while (dd->reordered == 1);
00125     return(res);
00126 
00127 } /* end of Cudd_addNegate */
00128 
00129 
00143 DdNode *
00144 Cudd_addRoundOff(
00145   DdManager * dd,
00146   DdNode * f,
00147   int  N)
00148 {
00149     DdNode *res;
00150     double trunc = pow(10.0,(double)N);
00151 
00152     do {
00153         res = cuddAddRoundOffRecur(dd,f,trunc);
00154     } while (dd->reordered == 1);
00155     return(res);
00156 
00157 } /* end of Cudd_addRoundOff */
00158 
00159 
00160 /*---------------------------------------------------------------------------*/
00161 /* Definition of internal functions                                          */
00162 /*---------------------------------------------------------------------------*/
00163 
00164 
00175 DdNode *
00176 cuddAddNegateRecur(
00177   DdManager * dd,
00178   DdNode * f)
00179 {
00180     DdNode *res,
00181             *fv, *fvn,
00182             *T, *E;
00183 
00184     statLine(dd);
00185     /* Check terminal cases. */
00186     if (cuddIsConstant(f)) {
00187         res = cuddUniqueConst(dd,-cuddV(f));
00188         return(res);
00189     }
00190 
00191     /* Check cache */
00192     res = cuddCacheLookup1(dd,Cudd_addNegate,f);
00193     if (res != NULL) return(res);
00194 
00195     /* Recursive Step */
00196     fv = cuddT(f);
00197     fvn = cuddE(f);
00198     T = cuddAddNegateRecur(dd,fv);
00199     if (T == NULL) return(NULL);
00200     cuddRef(T);
00201 
00202     E = cuddAddNegateRecur(dd,fvn);
00203     if (E == NULL) {
00204         Cudd_RecursiveDeref(dd,T);
00205         return(NULL);
00206     }
00207     cuddRef(E);
00208     res = (T == E) ? T : cuddUniqueInter(dd,(int)f->index,T,E);
00209     if (res == NULL) {
00210         Cudd_RecursiveDeref(dd, T);
00211         Cudd_RecursiveDeref(dd, E);
00212         return(NULL);
00213     }
00214     cuddDeref(T);
00215     cuddDeref(E);
00216 
00217     /* Store result. */
00218     cuddCacheInsert1(dd,Cudd_addNegate,f,res);
00219 
00220     return(res);
00221 
00222 } /* end of cuddAddNegateRecur */
00223 
00224 
00235 DdNode *
00236 cuddAddRoundOffRecur(
00237   DdManager * dd,
00238   DdNode * f,
00239   double  trunc)
00240 {
00241 
00242     DdNode *res, *fv, *fvn, *T, *E;
00243     double n;
00244     DD_CTFP1 cacheOp;
00245 
00246     statLine(dd);
00247     if (cuddIsConstant(f)) {
00248         n = ceil(cuddV(f)*trunc)/trunc;
00249         res = cuddUniqueConst(dd,n);
00250         return(res);
00251     }
00252     cacheOp = (DD_CTFP1) Cudd_addRoundOff;
00253     res = cuddCacheLookup1(dd,cacheOp,f);
00254     if (res != NULL) {
00255         return(res);
00256     }
00257     /* Recursive Step */
00258     fv = cuddT(f);
00259     fvn = cuddE(f);
00260     T = cuddAddRoundOffRecur(dd,fv,trunc);
00261     if (T == NULL) {
00262        return(NULL);
00263     }
00264     cuddRef(T);
00265     E = cuddAddRoundOffRecur(dd,fvn,trunc);
00266     if (E == NULL) {
00267         Cudd_RecursiveDeref(dd,T);
00268         return(NULL);
00269     }
00270     cuddRef(E);
00271     res = (T == E) ? T : cuddUniqueInter(dd,(int)f->index,T,E);
00272     if (res == NULL) {
00273         Cudd_RecursiveDeref(dd,T);
00274         Cudd_RecursiveDeref(dd,E);
00275         return(NULL);
00276     }
00277     cuddDeref(T);
00278     cuddDeref(E);
00279 
00280     /* Store result. */
00281     cuddCacheInsert1(dd,cacheOp,f,res);
00282     return(res);
00283 
00284 } /* end of cuddAddRoundOffRecur */
00285 
00286 /*---------------------------------------------------------------------------*/
00287 /* Definition of static functions                                            */
00288 /*---------------------------------------------------------------------------*/