summaryrefslogtreecommitdiffstats
path: root/src/bdd/cudd/cuddSolve.c
diff options
context:
space:
mode:
Diffstat (limited to 'src/bdd/cudd/cuddSolve.c')
-rw-r--r--src/bdd/cudd/cuddSolve.c339
1 files changed, 339 insertions, 0 deletions
diff --git a/src/bdd/cudd/cuddSolve.c b/src/bdd/cudd/cuddSolve.c
new file mode 100644
index 00000000..d9c4a2e7
--- /dev/null
+++ b/src/bdd/cudd/cuddSolve.c
@@ -0,0 +1,339 @@
+/**CFile***********************************************************************
+
+ FileName [cuddSolve.c]
+
+ PackageName [cudd]
+
+ Synopsis [Boolean equation solver and related functions.]
+
+ Description [External functions included in this modoule:
+ <ul>
+ <li> Cudd_SolveEqn()
+ <li> Cudd_VerifySol()
+ </ul>
+ Internal functions included in this module:
+ <ul>
+ <li> cuddSolveEqnRecur()
+ <li> cuddVerifySol()
+ </ul> ]
+
+ SeeAlso []
+
+ Author [Balakrishna Kumthekar]
+
+ Copyright [This file was created at the University of Colorado at
+ Boulder. The University of Colorado at Boulder makes no warranty
+ about the suitability of this software for any purpose. It is
+ presented on an AS IS basis.]
+
+******************************************************************************/
+
+#include "util_hack.h"
+#include "cuddInt.h"
+
+/*---------------------------------------------------------------------------*/
+/* Constant declarations */
+/*---------------------------------------------------------------------------*/
+
+
+/*---------------------------------------------------------------------------*/
+/* Type declarations */
+/*---------------------------------------------------------------------------*/
+
+
+/*---------------------------------------------------------------------------*/
+/* Structure declarations */
+/*---------------------------------------------------------------------------*/
+
+
+/*---------------------------------------------------------------------------*/
+/* Variable declarations */
+/*---------------------------------------------------------------------------*/
+
+#ifndef lint
+static char rcsid[] DD_UNUSED = "$Id: cuddSolve.c,v 1.1.1.1 2003/02/24 22:23:53 wjiang Exp $";
+#endif
+
+/*---------------------------------------------------------------------------*/
+/* Macro declarations */
+/*---------------------------------------------------------------------------*/
+
+
+/**AutomaticStart*************************************************************/
+
+/*---------------------------------------------------------------------------*/
+/* Static function prototypes */
+/*---------------------------------------------------------------------------*/
+
+
+/**AutomaticEnd***************************************************************/
+
+
+/*---------------------------------------------------------------------------*/
+/* Definition of exported functions */
+/*---------------------------------------------------------------------------*/
+
+
+/**Function********************************************************************
+
+ Synopsis [Implements the solution of F(x,y) = 0.]
+
+ Description [Implements the solution for F(x,y) = 0. The return
+ value is the consistency condition. The y variables are the unknowns
+ and the remaining variables are the parameters. Returns the
+ consistency condition if successful; NULL otherwise. Cudd_SolveEqn
+ allocates an array and fills it with the indices of the
+ unknowns. This array is used by Cudd_VerifySol.]
+
+ SideEffects [The solution is returned in G; the indices of the y
+ variables are returned in yIndex.]
+
+ SeeAlso [Cudd_VerifySol]
+
+******************************************************************************/
+DdNode *
+Cudd_SolveEqn(
+ DdManager * bdd,
+ DdNode * F /* the left-hand side of the equation */,
+ DdNode * Y /* the cube of the y variables */,
+ DdNode ** G /* the array of solutions (return parameter) */,
+ int ** yIndex /* index of y variables */,
+ int n /* numbers of unknowns */)
+{
+ DdNode *res;
+ int *temp;
+
+ *yIndex = temp = ALLOC(int, n);
+ if (temp == NULL) {
+ bdd->errorCode = CUDD_MEMORY_OUT;
+ (void) fprintf(bdd->out,
+ "Cudd_SolveEqn: Out of memory for yIndex\n");
+ return(NULL);
+ }
+
+ do {
+ bdd->reordered = 0;
+ res = cuddSolveEqnRecur(bdd, F, Y, G, n, temp, 0);
+ } while (bdd->reordered == 1);
+
+ return(res);
+
+} /* end of Cudd_SolveEqn */
+
+
+/**Function********************************************************************
+
+ Synopsis [Checks the solution of F(x,y) = 0.]
+
+ Description [Checks the solution of F(x,y) = 0. This procedure
+ substitutes the solution components for the unknowns of F and returns
+ the resulting BDD for F.]
+
+ SideEffects [Frees the memory pointed by yIndex.]
+
+ SeeAlso [Cudd_SolveEqn]
+
+******************************************************************************/
+DdNode *
+Cudd_VerifySol(
+ DdManager * bdd,
+ DdNode * F /* the left-hand side of the equation */,
+ DdNode ** G /* the array of solutions */,
+ int * yIndex /* index of y variables */,
+ int n /* numbers of unknowns */)
+{
+ DdNode *res;
+
+ do {
+ bdd->reordered = 0;
+ res = cuddVerifySol(bdd, F, G, yIndex, n);
+ } while (bdd->reordered == 1);
+
+ FREE(yIndex);
+
+ return(res);
+
+} /* end of Cudd_VerifySol */
+
+
+/*---------------------------------------------------------------------------*/
+/* Definition of internal functions */
+/*---------------------------------------------------------------------------*/
+
+
+/**Function********************************************************************
+
+ Synopsis [Implements the recursive step of Cudd_SolveEqn.]
+
+ Description [Implements the recursive step of Cudd_SolveEqn.
+ Returns NULL if the intermediate solution blows up
+ or reordering occurs. The parametric solutions are
+ stored in the array G.]
+
+ SideEffects [none]
+
+ SeeAlso [Cudd_SolveEqn, Cudd_VerifySol]
+
+******************************************************************************/
+DdNode *
+cuddSolveEqnRecur(
+ DdManager * bdd,
+ DdNode * F /* the left-hand side of the equation */,
+ DdNode * Y /* the cube of remaining y variables */,
+ DdNode ** G /* the array of solutions */,
+ int n /* number of unknowns */,
+ int * yIndex /* array holding the y variable indices */,
+ int i /* level of recursion */)
+{
+ DdNode *Fn, *Fm1, *Fv, *Fvbar, *T, *w, *nextY, *one;
+ DdNodePtr *variables;
+
+ int j;
+
+ statLine(bdd);
+ variables = bdd->vars;
+ one = DD_ONE(bdd);
+
+ /* Base condition. */
+ if (Y == one) {
+ return F;
+ }
+
+ /* Cofactor of Y. */
+ yIndex[i] = Y->index;
+ nextY = Cudd_T(Y);
+
+ /* Universal abstraction of F with respect to the top variable index. */
+ Fm1 = cuddBddExistAbstractRecur(bdd, Cudd_Not(F), variables[yIndex[i]]);
+ if (Fm1) {
+ Fm1 = Cudd_Not(Fm1);
+ cuddRef(Fm1);
+ } else {
+ return(NULL);
+ }
+
+ Fn = cuddSolveEqnRecur(bdd, Fm1, nextY, G, n, yIndex, i+1);
+ if (Fn) {
+ cuddRef(Fn);
+ } else {
+ Cudd_RecursiveDeref(bdd, Fm1);
+ return(NULL);
+ }
+
+ Fv = cuddCofactorRecur(bdd, F, variables[yIndex[i]]);
+ if (Fv) {
+ cuddRef(Fv);
+ } else {
+ Cudd_RecursiveDeref(bdd, Fm1);
+ Cudd_RecursiveDeref(bdd, Fn);
+ return(NULL);
+ }
+
+ Fvbar = cuddCofactorRecur(bdd, F, Cudd_Not(variables[yIndex[i]]));
+ if (Fvbar) {
+ cuddRef(Fvbar);
+ } else {
+ Cudd_RecursiveDeref(bdd, Fm1);
+ Cudd_RecursiveDeref(bdd, Fn);
+ Cudd_RecursiveDeref(bdd, Fv);
+ return(NULL);
+ }
+
+ /* Build i-th component of the solution. */
+ w = cuddBddIteRecur(bdd, variables[yIndex[i]], Cudd_Not(Fv), Fvbar);
+ if (w) {
+ cuddRef(w);
+ } else {
+ Cudd_RecursiveDeref(bdd, Fm1);
+ Cudd_RecursiveDeref(bdd, Fn);
+ Cudd_RecursiveDeref(bdd, Fv);
+ Cudd_RecursiveDeref(bdd, Fvbar);
+ return(NULL);
+ }
+
+ T = cuddBddRestrictRecur(bdd, w, Cudd_Not(Fm1));
+ if(T) {
+ cuddRef(T);
+ } else {
+ Cudd_RecursiveDeref(bdd, Fm1);
+ Cudd_RecursiveDeref(bdd, Fn);
+ Cudd_RecursiveDeref(bdd, Fv);
+ Cudd_RecursiveDeref(bdd, Fvbar);
+ Cudd_RecursiveDeref(bdd, w);
+ return(NULL);
+ }
+
+ Cudd_RecursiveDeref(bdd,Fm1);
+ Cudd_RecursiveDeref(bdd,w);
+ Cudd_RecursiveDeref(bdd,Fv);
+ Cudd_RecursiveDeref(bdd,Fvbar);
+
+ /* Substitute components of solution already found into solution. */
+ for (j = n-1; j > i; j--) {
+ w = cuddBddComposeRecur(bdd,T, G[j], variables[yIndex[j]]);
+ if(w) {
+ cuddRef(w);
+ } else {
+ Cudd_RecursiveDeref(bdd, Fn);
+ Cudd_RecursiveDeref(bdd, T);
+ return(NULL);
+ }
+ Cudd_RecursiveDeref(bdd,T);
+ T = w;
+ }
+ G[i] = T;
+
+ Cudd_Deref(Fn);
+
+ return(Fn);
+
+} /* end of cuddSolveEqnRecur */
+
+
+/**Function********************************************************************
+
+ Synopsis [Implements the recursive step of Cudd_VerifySol. ]
+
+ Description []
+
+ SideEffects [none]
+
+ SeeAlso [Cudd_VerifySol]
+
+******************************************************************************/
+DdNode *
+cuddVerifySol(
+ DdManager * bdd,
+ DdNode * F /* the left-hand side of the equation */,
+ DdNode ** G /* the array of solutions */,
+ int * yIndex /* array holding the y variable indices */,
+ int n /* number of unknowns */)
+{
+ DdNode *w, *R;
+
+ int j;
+
+ R = F;
+ cuddRef(R);
+ for(j = n - 1; j >= 0; j--) {
+ w = Cudd_bddCompose(bdd, R, G[j], yIndex[j]);
+ if (w) {
+ cuddRef(w);
+ } else {
+ return(NULL);
+ }
+ Cudd_RecursiveDeref(bdd,R);
+ R = w;
+ }
+
+ cuddDeref(R);
+
+ return(R);
+
+} /* end of cuddVerifySol */
+
+
+/*---------------------------------------------------------------------------*/
+/* Definition of static functions */
+/*---------------------------------------------------------------------------*/
+
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-15 14:08:34 +0000