distr/cudd/cuddSolve.c

   1 /**CFile***********************************************************************
   2
   3   FileName    [cuddSolve.c]
   4
   5   PackageName [cudd]
   6
   7   Synopsis    [Boolean equation solver and related functions.]
   8
   9   Description [External functions included in this modoule:
  10                 <ul>
  11                 <li> Cudd_SolveEqn()
  12                 <li> Cudd_VerifySol()
  13                 </ul>
  14         Internal functions included in this module:
  15                 <ul>
  16                 <li> cuddSolveEqnRecur()
  17                 <li> cuddVerifySol()
  18                 </ul> ]
  19
  20   SeeAlso     []
  21
  22   Author      [Balakrishna Kumthekar]
  23
  24   Copyright   [Copyright (c) 1995-2004, Regents of the University of Colorado
  25
  26   All rights reserved.
  27
  28   Redistribution and use in source and binary forms, with or without
  29   modification, are permitted provided that the following conditions
  30   are met:
  31
  32   Redistributions of source code must retain the above copyright
  33   notice, this list of conditions and the following disclaimer.
  34
  35   Redistributions in binary form must reproduce the above copyright
  36   notice, this list of conditions and the following disclaimer in the
  37   documentation and/or other materials provided with the distribution.
  38
  39   Neither the name of the University of Colorado nor the names of its
  40   contributors may be used to endorse or promote products derived from
  41   this software without specific prior written permission.
  42
  43   THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
  44   "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
  45   LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
  46   FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
  47   COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
  48   INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
  49   BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
  50   LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
  51   CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
  52   LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
  53   ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
  54   POSSIBILITY OF SUCH DAMAGE.]
  55
  56 ******************************************************************************/
  57
  58 #include "util.h"
  59 #include "cuddInt.h"
  60
  61 /*---------------------------------------------------------------------------*/
  62 /* Constant declarations                                                     */
  63 /*---------------------------------------------------------------------------*/
  64
  65
  66 /*---------------------------------------------------------------------------*/
  67 /* Type declarations                                                         */
  68 /*---------------------------------------------------------------------------*/
  69
  70
  71 /*---------------------------------------------------------------------------*/
  72 /* Structure declarations                                                    */
  73 /*---------------------------------------------------------------------------*/
  74
  75
  76 /*---------------------------------------------------------------------------*/
  77 /* Variable declarations                                                     */
  78 /*---------------------------------------------------------------------------*/
  79
  80 #ifndef lint
  81 static char rcsid[] DD_UNUSED = "$Id: cuddSolve.c,v 1.12 2004/08/13 18:04:51 fabio Exp $";
  82 #endif
  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
 104 /**Function********************************************************************
 105
 106   Synopsis    [Implements the solution of F(x,y) = 0.]
 107
 108   Description [Implements the solution for F(x,y) = 0. The return
 109   value is the consistency condition. The y variables are the unknowns
 110   and the remaining variables are the parameters.  Returns the
 111   consistency condition if successful; NULL otherwise. Cudd_SolveEqn
 112   allocates an array and fills it with the indices of the
 113   unknowns. This array is used by Cudd_VerifySol.]
 114
 115   SideEffects [The solution is returned in G; the indices of the y
 116   variables are returned in yIndex.]
 117
 118   SeeAlso     [Cudd_VerifySol]
 119
 120 ******************************************************************************/
 121 DdNode *
 122 Cudd_SolveEqn(
 123   DdManager *  bdd,
 124   DdNode * F /* the left-hand side of the equation */,
 125   DdNode * Y /* the cube of the y variables */,
 126   DdNode ** G /* the array of solutions (return parameter) */,
 127   int ** yIndex /* index of y variables */,
 128   int  n /* numbers of unknowns */)
 129 {
 130     DdNode *res;
 131     int *temp;
 132
 133     *yIndex = temp = ALLOC(int, n);
 134     if (temp == NULL) {
 135         bdd->errorCode = CUDD_MEMORY_OUT;
 136         (void) fprintf(bdd->out,
 137                        "Cudd_SolveEqn: Out of memory for yIndex\n");
 138         return(NULL);
 139     }
 140
 141     do {
 142         bdd->reordered = 0;
 143         res = cuddSolveEqnRecur(bdd, F, Y, G, n, temp, 0);
 144     } while (bdd->reordered == 1);
 145
 146     return(res);
 147
 148 } /* end of Cudd_SolveEqn */
 149
 150
 151 /**Function********************************************************************
 152
 153   Synopsis    [Checks the solution of F(x,y) = 0.]
 154
 155   Description [Checks the solution of F(x,y) = 0. This procedure
 156   substitutes the solution components for the unknowns of F and returns
 157   the resulting BDD for F.]
 158
 159   SideEffects [Frees the memory pointed by yIndex.]
 160
 161   SeeAlso     [Cudd_SolveEqn]
 162
 163 ******************************************************************************/
 164 DdNode *
 165 Cudd_VerifySol(
 166   DdManager *  bdd,
 167   DdNode * F /* the left-hand side of the equation */,
 168   DdNode ** G /* the array of solutions */,
 169   int * yIndex /* index of y variables */,
 170   int  n /* numbers of unknowns */)
 171 {
 172     DdNode *res;
 173
 174     do {
 175         bdd->reordered = 0;
 176         res = cuddVerifySol(bdd, F, G, yIndex, n);
 177     } while (bdd->reordered == 1);
 178
 179     FREE(yIndex);
 180
 181     return(res);
 182
 183 } /* end of Cudd_VerifySol */
 184
 185
 186 /*---------------------------------------------------------------------------*/
 187 /* Definition of internal functions                                          */
 188 /*---------------------------------------------------------------------------*/
 189
 190
 191 /**Function********************************************************************
 192
 193   Synopsis    [Implements the recursive step of Cudd_SolveEqn.]
 194
 195   Description [Implements the recursive step of Cudd_SolveEqn.
 196   Returns NULL if the intermediate solution blows up
 197   or reordering occurs. The parametric solutions are
 198   stored in the array G.]
 199
 200   SideEffects [none]
 201
 202   SeeAlso     [Cudd_SolveEqn, Cudd_VerifySol]
 203
 204 ******************************************************************************/
 205 DdNode *
 206 cuddSolveEqnRecur(
 207   DdManager * bdd,
 208   DdNode * F /* the left-hand side of the equation */,
 209   DdNode * Y /* the cube of remaining y variables */,
 210   DdNode ** G /* the array of solutions */,
 211   int  n /* number of unknowns */,
 212   int * yIndex /* array holding the y variable indices */,
 213   int  i /* level of recursion */)
 214 {
 215     DdNode *Fn, *Fm1, *Fv, *Fvbar, *T, *w, *nextY, *one;
 216     DdNodePtr *variables;
 217
 218     int j;
 219
 220     statLine(bdd);
 221     variables = bdd->vars;
 222     one = DD_ONE(bdd);
 223
 224     /* Base condition. */
 225     if (Y == one) {
 226         return F;
 227     }
 228
 229     /* Cofactor of Y. */
 230     yIndex[i] = Y->index;
 231     nextY = Cudd_T(Y);
 232
 233     /* Universal abstraction of F with respect to the top variable index. */
 234     Fm1 = cuddBddExistAbstractRecur(bdd, Cudd_Not(F), variables[yIndex[i]]);
 235     if (Fm1) {
 236         Fm1 = Cudd_Not(Fm1);
 237         cuddRef(Fm1);
 238     } else {
 239         return(NULL);
 240     }
 241
 242     Fn = cuddSolveEqnRecur(bdd, Fm1, nextY, G, n, yIndex, i+1);
 243     if (Fn) {
 244         cuddRef(Fn);
 245     } else {
 246         Cudd_RecursiveDeref(bdd, Fm1);
 247         return(NULL);
 248     }
 249
 250     Fv = cuddCofactorRecur(bdd, F, variables[yIndex[i]]);
 251     if (Fv) {
 252         cuddRef(Fv);
 253     } else {
 254         Cudd_RecursiveDeref(bdd, Fm1);
 255         Cudd_RecursiveDeref(bdd, Fn);
 256         return(NULL);
 257     }
 258
 259     Fvbar = cuddCofactorRecur(bdd, F, Cudd_Not(variables[yIndex[i]]));
 260     if (Fvbar) {
 261         cuddRef(Fvbar);
 262     } else {
 263         Cudd_RecursiveDeref(bdd, Fm1);
 264         Cudd_RecursiveDeref(bdd, Fn);
 265         Cudd_RecursiveDeref(bdd, Fv);
 266         return(NULL);
 267     }
 268
 269     /* Build i-th component of the solution. */
 270     w = cuddBddIteRecur(bdd, variables[yIndex[i]], Cudd_Not(Fv), Fvbar);
 271     if (w) {
 272         cuddRef(w);
 273     } else {
 274         Cudd_RecursiveDeref(bdd, Fm1);
 275         Cudd_RecursiveDeref(bdd, Fn);
 276         Cudd_RecursiveDeref(bdd, Fv);
 277         Cudd_RecursiveDeref(bdd, Fvbar);
 278         return(NULL);
 279     }
 280
 281     T = cuddBddRestrictRecur(bdd, w, Cudd_Not(Fm1));
 282     if(T) {
 283         cuddRef(T);
 284     } else {
 285         Cudd_RecursiveDeref(bdd, Fm1);
 286         Cudd_RecursiveDeref(bdd, Fn);
 287         Cudd_RecursiveDeref(bdd, Fv);
 288         Cudd_RecursiveDeref(bdd, Fvbar);
 289         Cudd_RecursiveDeref(bdd, w);
 290         return(NULL);
 291     }
 292
 293     Cudd_RecursiveDeref(bdd,Fm1);
 294     Cudd_RecursiveDeref(bdd,w);
 295     Cudd_RecursiveDeref(bdd,Fv);
 296     Cudd_RecursiveDeref(bdd,Fvbar);
 297
 298     /* Substitute components of solution already found into solution. */
 299     for (j = n-1; j > i; j--) {
 300         w = cuddBddComposeRecur(bdd,T, G[j], variables[yIndex[j]]);
 301         if(w) {
 302             cuddRef(w);
 303         } else {
 304             Cudd_RecursiveDeref(bdd, Fn);
 305             Cudd_RecursiveDeref(bdd, T);
 306             return(NULL);
 307         }
 308         Cudd_RecursiveDeref(bdd,T);
 309         T = w;
 310     }
 311     G[i] = T;
 312
 313     Cudd_Deref(Fn);
 314
 315     return(Fn);
 316
 317 } /* end of cuddSolveEqnRecur */
 318
 319
 320 /**Function********************************************************************
 321
 322   Synopsis    [Implements the recursive step of Cudd_VerifySol. ]
 323
 324   Description []
 325
 326   SideEffects [none]
 327
 328   SeeAlso     [Cudd_VerifySol]
 329
 330 ******************************************************************************/
 331 DdNode *
 332 cuddVerifySol(
 333   DdManager * bdd,
 334   DdNode * F /* the left-hand side of the equation */,
 335   DdNode ** G /* the array of solutions */,
 336   int * yIndex /* array holding the y variable indices */,
 337   int  n /* number of unknowns */)
 338 {
 339     DdNode *w, *R;
 340
 341     int j;
 342
 343     R = F;
 344     cuddRef(R);
 345     for(j = n - 1; j >= 0; j--) {
 346          w = Cudd_bddCompose(bdd, R, G[j], yIndex[j]);
 347         if (w) {
 348             cuddRef(w);
 349         } else {
 350             return(NULL);
 351         }
 352         Cudd_RecursiveDeref(bdd,R);
 353         R = w;
 354     }
 355
 356     cuddDeref(R);
 357
 358     return(R);
 359
 360 } /* end of cuddVerifySol */
 361
 362
 363 /*---------------------------------------------------------------------------*/
 364 /* Definition of static functions                                            */
 365 /*---------------------------------------------------------------------------*/
 366