distr/cudd/cuddCof.c

   1 /**CFile***********************************************************************
   2
   3   FileName    [cuddCof.c]
   4
   5   PackageName [cudd]
   6
   7   Synopsis    [Cofactoring functions.]
   8
   9   Description [External procedures included in this module:
  10                 <ul>
  11                 <li> Cudd_Cofactor()
  12                 </ul>
  13                Internal procedures included in this module:
  14                 <ul>
  15                 <li> cuddGetBranches()
  16                 <li> cuddCheckCube()
  17                 <li> cuddCofactorRecur()
  18                 </ul>
  19               ]
  20
  21   SeeAlso     []
  22
  23   Author      [Fabio Somenzi]
  24
  25   Copyright   [Copyright (c) 1995-2004, Regents of the University of Colorado
  26
  27   All rights reserved.
  28
  29   Redistribution and use in source and binary forms, with or without
  30   modification, are permitted provided that the following conditions
  31   are met:
  32
  33   Redistributions of source code must retain the above copyright
  34   notice, this list of conditions and the following disclaimer.
  35
  36   Redistributions in binary form must reproduce the above copyright
  37   notice, this list of conditions and the following disclaimer in the
  38   documentation and/or other materials provided with the distribution.
  39
  40   Neither the name of the University of Colorado nor the names of its
  41   contributors may be used to endorse or promote products derived from
  42   this software without specific prior written permission.
  43
  44   THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
  45   "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
  46   LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
  47   FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
  48   COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
  49   INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
  50   BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
  51   LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
  52   CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
  53   LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
  54   ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
  55   POSSIBILITY OF SUCH DAMAGE.]
  56
  57 ******************************************************************************/
  58
  59 #include "util.h"
  60 #include "cuddInt.h"
  61
  62 /*---------------------------------------------------------------------------*/
  63 /* Constant declarations                                                     */
  64 /*---------------------------------------------------------------------------*/
  65
  66
  67 /*---------------------------------------------------------------------------*/
  68 /* Stucture declarations                                                     */
  69 /*---------------------------------------------------------------------------*/
  70
  71
  72 /*---------------------------------------------------------------------------*/
  73 /* Type declarations                                                         */
  74 /*---------------------------------------------------------------------------*/
  75
  76
  77 /*---------------------------------------------------------------------------*/
  78 /* Variable declarations                                                     */
  79 /*---------------------------------------------------------------------------*/
  80
  81 #ifndef lint
  82 static char rcsid[] DD_UNUSED = "$Id: cuddCof.c,v 1.9 2004/08/13 18:04:47 fabio Exp $";
  83 #endif
  84
  85 /*---------------------------------------------------------------------------*/
  86 /* Macro declarations                                                        */
  87 /*---------------------------------------------------------------------------*/
  88
  89
  90 /**AutomaticStart*************************************************************/
  91
  92 /*---------------------------------------------------------------------------*/
  93 /* Static function prototypes                                                */
  94 /*---------------------------------------------------------------------------*/
  95
  96
  97 /**AutomaticEnd***************************************************************/
  98
  99
 100 /*---------------------------------------------------------------------------*/
 101 /* Definition of exported functions                                          */
 102 /*---------------------------------------------------------------------------*/
 103
 104
 105 /**Function********************************************************************
 106
 107   Synopsis    [Computes the cofactor of f with respect to g.]
 108
 109   Description [Computes the cofactor of f with respect to g; g must be
 110   the BDD or the ADD of a cube. Returns a pointer to the cofactor if
 111   successful; NULL otherwise.]
 112
 113   SideEffects [None]
 114
 115   SeeAlso     [Cudd_bddConstrain Cudd_bddRestrict]
 116
 117 ******************************************************************************/
 118 DdNode *
 119 Cudd_Cofactor(
 120   DdManager * dd,
 121   DdNode * f,
 122   DdNode * g)
 123 {
 124     DdNode *res,*zero;
 125
 126     zero = Cudd_Not(DD_ONE(dd));
 127     if (g == zero || g == DD_ZERO(dd)) {
 128         (void) fprintf(dd->err,"Cudd_Cofactor: Invalid restriction 1\n");
 129         dd->errorCode = CUDD_INVALID_ARG;
 130         return(NULL);
 131     }
 132     do {
 133         dd->reordered = 0;
 134         res = cuddCofactorRecur(dd,f,g);
 135     } while (dd->reordered == 1);
 136     return(res);
 137
 138 } /* end of Cudd_Cofactor */
 139
 140
 141 /*---------------------------------------------------------------------------*/
 142 /* Definition of internal functions                                          */
 143 /*---------------------------------------------------------------------------*/
 144
 145
 146 /**Function********************************************************************
 147
 148   Synopsis    [Computes the children of g.]
 149
 150   Description []
 151
 152   SideEffects [None]
 153
 154   SeeAlso     []
 155
 156 ******************************************************************************/
 157 void
 158 cuddGetBranches(
 159   DdNode * g,
 160   DdNode ** g1,
 161   DdNode ** g0)
 162 {
 163     DdNode      *G = Cudd_Regular(g);
 164
 165     *g1 = cuddT(G);
 166     *g0 = cuddE(G);
 167     if (Cudd_IsComplement(g)) {
 168         *g1 = Cudd_Not(*g1);
 169         *g0 = Cudd_Not(*g0);
 170     }
 171
 172 } /* end of cuddGetBranches */
 173
 174
 175 /**Function********************************************************************
 176
 177   Synopsis    [Checks whether g is the BDD of a cube.]
 178
 179   Description [Checks whether g is the BDD of a cube. Returns 1 in case
 180   of success; 0 otherwise. The constant 1 is a valid cube, but all other
 181   constant functions cause cuddCheckCube to return 0.]
 182
 183   SideEffects [None]
 184
 185   SeeAlso     []
 186
 187 ******************************************************************************/
 188 int
 189 cuddCheckCube(
 190   DdManager * dd,
 191   DdNode * g)
 192 {
 193     DdNode *g1,*g0,*one,*zero;
 194
 195     one = DD_ONE(dd);
 196     if (g == one) return(1);
 197     if (Cudd_IsConstant(g)) return(0);
 198
 199     zero = Cudd_Not(one);
 200     cuddGetBranches(g,&g1,&g0);
 201
 202     if (g0 == zero) {
 203         return(cuddCheckCube(dd, g1));
 204     }
 205     if (g1 == zero) {
 206         return(cuddCheckCube(dd, g0));
 207     }
 208     return(0);
 209
 210 } /* end of cuddCheckCube */
 211
 212
 213 /**Function********************************************************************
 214
 215   Synopsis    [Performs the recursive step of Cudd_Cofactor.]
 216
 217   Description [Performs the recursive step of Cudd_Cofactor. Returns a
 218   pointer to the cofactor if successful; NULL otherwise.]
 219
 220   SideEffects [None]
 221
 222   SeeAlso     [Cudd_Cofactor]
 223
 224 ******************************************************************************/
 225 DdNode *
 226 cuddCofactorRecur(
 227   DdManager * dd,
 228   DdNode * f,
 229   DdNode * g)
 230 {
 231     DdNode *one,*zero,*F,*G,*g1,*g0,*f1,*f0,*t,*e,*r;
 232     unsigned int topf,topg;
 233     int comple;
 234
 235     statLine(dd);
 236     F = Cudd_Regular(f);
 237     if (cuddIsConstant(F)) return(f);
 238
 239     one = DD_ONE(dd);
 240
 241     /* The invariant g != 0 is true on entry to this procedure and is
 242     ** recursively maintained by it. Therefore it suffices to test g
 243     ** against one to make sure it is not constant.
 244     */
 245     if (g == one) return(f);
 246     /* From now on, f and g are known not to be constants. */
 247
 248     comple = f != F;
 249     r = cuddCacheLookup2(dd,Cudd_Cofactor,F,g);
 250     if (r != NULL) {
 251         return(Cudd_NotCond(r,comple));
 252     }
 253
 254     topf = dd->perm[F->index];
 255     G = Cudd_Regular(g);
 256     topg = dd->perm[G->index];
 257
 258     /* We take the cofactors of F because we are going to rely on
 259     ** the fact that the cofactors of the complement are the complements
 260     ** of the cofactors to better utilize the cache. Variable comple
 261     ** remembers whether we have to complement the result or not.
 262     */
 263     if (topf <= topg) {
 264         f1 = cuddT(F); f0 = cuddE(F);
 265     } else {
 266         f1 = f0 = F;
 267     }
 268     if (topg <= topf) {
 269         g1 = cuddT(G); g0 = cuddE(G);
 270         if (g != G) { g1 = Cudd_Not(g1); g0 = Cudd_Not(g0); }
 271     } else {
 272         g1 = g0 = g;
 273     }
 274
 275     zero = Cudd_Not(one);
 276     if (topf >= topg) {
 277         if (g0 == zero || g0 == DD_ZERO(dd)) {
 278             r = cuddCofactorRecur(dd, f1, g1);
 279         } else if (g1 == zero || g1 == DD_ZERO(dd)) {
 280             r = cuddCofactorRecur(dd, f0, g0);
 281         } else {
 282             (void) fprintf(dd->out,
 283                            "Cudd_Cofactor: Invalid restriction 2\n");
 284             dd->errorCode = CUDD_INVALID_ARG;
 285             return(NULL);
 286         }
 287         if (r == NULL) return(NULL);
 288     } else /* if (topf < topg) */ {
 289         t = cuddCofactorRecur(dd, f1, g);
 290         if (t == NULL) return(NULL);
 291         cuddRef(t);
 292         e = cuddCofactorRecur(dd, f0, g);
 293         if (e == NULL) {
 294             Cudd_RecursiveDeref(dd, t);
 295             return(NULL);
 296         }
 297         cuddRef(e);
 298
 299         if (t == e) {
 300             r = t;
 301         } else if (Cudd_IsComplement(t)) {
 302             r = cuddUniqueInter(dd,(int)F->index,Cudd_Not(t),Cudd_Not(e));
 303             if (r != NULL)
 304                 r = Cudd_Not(r);
 305         } else {
 306             r = cuddUniqueInter(dd,(int)F->index,t,e);
 307         }
 308         if (r == NULL) {
 309             Cudd_RecursiveDeref(dd ,e);
 310             Cudd_RecursiveDeref(dd ,t);
 311             return(NULL);
 312         }
 313         cuddDeref(t);
 314         cuddDeref(e);
 315     }
 316
 317     cuddCacheInsert2(dd,Cudd_Cofactor,F,g,r);
 318
 319     return(Cudd_NotCond(r,comple));
 320
 321 } /* end of cuddCofactorRecur */
 322
 323
 324 /*---------------------------------------------------------------------------*/
 325 /* Definition of static functions                                            */
 326 /*---------------------------------------------------------------------------*/
 327