1 /**CFile***********************************************************************
7 Synopsis [Boolean equation solver and related functions.]
9 Description [External functions included in this modoule:
14 Internal functions included in this module:
16 <li> cuddSolveEqnRecur()
22 Author [Balakrishna Kumthekar]
24 Copyright [Copyright (c) 1995-2004, Regents of the University of Colorado
28 Redistribution and use in source and binary forms, with or without
29 modification, are permitted provided that the following conditions
32 Redistributions of source code must retain the above copyright
33 notice, this list of conditions and the following disclaimer.
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.
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.
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.]
56 ******************************************************************************/
61 /*---------------------------------------------------------------------------*/
62 /* Constant declarations */
63 /*---------------------------------------------------------------------------*/
66 /*---------------------------------------------------------------------------*/
67 /* Type declarations */
68 /*---------------------------------------------------------------------------*/
71 /*---------------------------------------------------------------------------*/
72 /* Structure declarations */
73 /*---------------------------------------------------------------------------*/
76 /*---------------------------------------------------------------------------*/
77 /* Variable declarations */
78 /*---------------------------------------------------------------------------*/
81 static char rcsid
[] DD_UNUSED
= "$Id: cuddSolve.c,v 1.12 2004/08/13 18:04:51 fabio Exp $";
84 /*---------------------------------------------------------------------------*/
85 /* Macro declarations */
86 /*---------------------------------------------------------------------------*/
89 /**AutomaticStart*************************************************************/
91 /*---------------------------------------------------------------------------*/
92 /* Static function prototypes */
93 /*---------------------------------------------------------------------------*/
96 /**AutomaticEnd***************************************************************/
99 /*---------------------------------------------------------------------------*/
100 /* Definition of exported functions */
101 /*---------------------------------------------------------------------------*/
104 /**Function********************************************************************
106 Synopsis [Implements the solution of F(x,y) = 0.]
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.]
115 SideEffects [The solution is returned in G; the indices of the y
116 variables are returned in yIndex.]
118 SeeAlso [Cudd_VerifySol]
120 ******************************************************************************/
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 */)
133 *yIndex
= temp
= ALLOC(int, n
);
135 bdd
->errorCode
= CUDD_MEMORY_OUT
;
136 (void) fprintf(bdd
->out
,
137 "Cudd_SolveEqn: Out of memory for yIndex\n");
143 res
= cuddSolveEqnRecur(bdd
, F
, Y
, G
, n
, temp
, 0);
144 } while (bdd
->reordered
== 1);
148 } /* end of Cudd_SolveEqn */
151 /**Function********************************************************************
153 Synopsis [Checks the solution of F(x,y) = 0.]
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.]
159 SideEffects [Frees the memory pointed by yIndex.]
161 SeeAlso [Cudd_SolveEqn]
163 ******************************************************************************/
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 */)
176 res
= cuddVerifySol(bdd
, F
, G
, yIndex
, n
);
177 } while (bdd
->reordered
== 1);
183 } /* end of Cudd_VerifySol */
186 /*---------------------------------------------------------------------------*/
187 /* Definition of internal functions */
188 /*---------------------------------------------------------------------------*/
191 /**Function********************************************************************
193 Synopsis [Implements the recursive step of Cudd_SolveEqn.]
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.]
202 SeeAlso [Cudd_SolveEqn, Cudd_VerifySol]
204 ******************************************************************************/
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 */)
215 DdNode
*Fn
, *Fm1
, *Fv
, *Fvbar
, *T
, *w
, *nextY
, *one
;
216 DdNodePtr
*variables
;
221 variables
= bdd
->vars
;
224 /* Base condition. */
230 yIndex
[i
] = Y
->index
;
233 /* Universal abstraction of F with respect to the top variable index. */
234 Fm1
= cuddBddExistAbstractRecur(bdd
, Cudd_Not(F
), variables
[yIndex
[i
]]);
242 Fn
= cuddSolveEqnRecur(bdd
, Fm1
, nextY
, G
, n
, yIndex
, i
+1);
246 Cudd_RecursiveDeref(bdd
, Fm1
);
250 Fv
= cuddCofactorRecur(bdd
, F
, variables
[yIndex
[i
]]);
254 Cudd_RecursiveDeref(bdd
, Fm1
);
255 Cudd_RecursiveDeref(bdd
, Fn
);
259 Fvbar
= cuddCofactorRecur(bdd
, F
, Cudd_Not(variables
[yIndex
[i
]]));
263 Cudd_RecursiveDeref(bdd
, Fm1
);
264 Cudd_RecursiveDeref(bdd
, Fn
);
265 Cudd_RecursiveDeref(bdd
, Fv
);
269 /* Build i-th component of the solution. */
270 w
= cuddBddIteRecur(bdd
, variables
[yIndex
[i
]], Cudd_Not(Fv
), Fvbar
);
274 Cudd_RecursiveDeref(bdd
, Fm1
);
275 Cudd_RecursiveDeref(bdd
, Fn
);
276 Cudd_RecursiveDeref(bdd
, Fv
);
277 Cudd_RecursiveDeref(bdd
, Fvbar
);
281 T
= cuddBddRestrictRecur(bdd
, w
, Cudd_Not(Fm1
));
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
);
293 Cudd_RecursiveDeref(bdd
,Fm1
);
294 Cudd_RecursiveDeref(bdd
,w
);
295 Cudd_RecursiveDeref(bdd
,Fv
);
296 Cudd_RecursiveDeref(bdd
,Fvbar
);
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
]]);
304 Cudd_RecursiveDeref(bdd
, Fn
);
305 Cudd_RecursiveDeref(bdd
, T
);
308 Cudd_RecursiveDeref(bdd
,T
);
317 } /* end of cuddSolveEqnRecur */
320 /**Function********************************************************************
322 Synopsis [Implements the recursive step of Cudd_VerifySol. ]
328 SeeAlso [Cudd_VerifySol]
330 ******************************************************************************/
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 */)
345 for(j
= n
- 1; j
>= 0; j
--) {
346 w
= Cudd_bddCompose(bdd
, R
, G
[j
], yIndex
[j
]);
352 Cudd_RecursiveDeref(bdd
,R
);
360 } /* end of cuddVerifySol */
363 /*---------------------------------------------------------------------------*/
364 /* Definition of static functions */
365 /*---------------------------------------------------------------------------*/