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-2012, 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.13 2012/02/05 01:07:19 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 *
Cudd_SolveEqn(DdManager * bdd,DdNode * F,DdNode * Y,DdNode ** G,int ** yIndex,int n)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 *
Cudd_VerifySol(DdManager * bdd,DdNode * F,DdNode ** G,int * yIndex,int n)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 *
cuddSolveEqnRecur(DdManager * bdd,DdNode * F,DdNode * Y,DdNode ** G,int n,int * yIndex,int i)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 *
cuddVerifySol(DdManager * bdd,DdNode * F,DdNode ** G,int * yIndex,int n)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
367