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, 0 insertions, 339 deletions
diff --git a/src/bdd/cudd/cuddSolve.c b/src/bdd/cudd/cuddSolve.c
deleted file mode 100644
index d9c4a2e7..00000000
--- a/src/bdd/cudd/cuddSolve.c
+++ /dev/null
@@ -1,339 +0,0 @@
-/**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-08-19 12:51:55 +0000