source: vis_dev/glu-2.3/src/cuBdd/cuddSolve.c @ 104

Last change on this file since 104 was 13, checked in by cecile, 13 years ago

library glu 2.3
File size: 10.6 KB
Line 
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
81static 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******************************************************************************/
121DdNode *
122Cudd_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******************************************************************************/
164DdNode *
165Cudd_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******************************************************************************/
205DdNode *
206cuddSolveEqnRecur(
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******************************************************************************/
331DdNode *
332cuddVerifySol(
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
Note: See TracBrowser for help on using the repository browser.