From e54d9691616b9a0326e2fdb3156bb4eeb8abfcd7 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sun, 30 Sep 2007 08:01:00 -0700 Subject: Version abc70930 --- src/bdd/cudd/cuddDecomp.c | 2150 --------------------------------------------- 1 file changed, 2150 deletions(-) delete mode 100644 src/bdd/cudd/cuddDecomp.c (limited to 'src/bdd/cudd/cuddDecomp.c') diff --git a/src/bdd/cudd/cuddDecomp.c b/src/bdd/cudd/cuddDecomp.c deleted file mode 100644 index 4fde7392..00000000 --- a/src/bdd/cudd/cuddDecomp.c +++ /dev/null @@ -1,2150 +0,0 @@ -/**CFile*********************************************************************** - - FileName [cuddDecomp.c] - - PackageName [cudd] - - Synopsis [Functions for BDD decomposition.] - - Description [External procedures included in this file: - - Static procedures included in this module: - ] - - Author [Kavita Ravi, Fabio Somenzi] - - 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 */ -/*---------------------------------------------------------------------------*/ -#define DEPTH 5 -#define THRESHOLD 10 -#define NONE 0 -#define PAIR_ST 1 -#define PAIR_CR 2 -#define G_ST 3 -#define G_CR 4 -#define H_ST 5 -#define H_CR 6 -#define BOTH_G 7 -#define BOTH_H 8 - -/*---------------------------------------------------------------------------*/ -/* Stucture declarations */ -/*---------------------------------------------------------------------------*/ - -/*---------------------------------------------------------------------------*/ -/* Type declarations */ -/*---------------------------------------------------------------------------*/ -typedef struct Conjuncts { - DdNode *g; - DdNode *h; -} Conjuncts; - -typedef struct NodeStat { - int distance; - int localRef; -} NodeStat; - - -/*---------------------------------------------------------------------------*/ -/* Variable declarations */ -/*---------------------------------------------------------------------------*/ - -#ifndef lint -static char rcsid[] DD_UNUSED = "$Id: cuddDecomp.c,v 1.1.1.1 2003/02/24 22:23:51 wjiang Exp $"; -#endif - -static DdNode *one, *zero; -long lastTimeG; - -/*---------------------------------------------------------------------------*/ -/* Macro declarations */ -/*---------------------------------------------------------------------------*/ - - -#define FactorsNotStored(factors) ((int)((long)(factors) & 01)) - -#define FactorsComplement(factors) ((Conjuncts *)((long)(factors) | 01)) - -#define FactorsUncomplement(factors) ((Conjuncts *)((long)(factors) ^ 01)) - -/**AutomaticStart*************************************************************/ - -/*---------------------------------------------------------------------------*/ -/* Static function prototypes */ -/*---------------------------------------------------------------------------*/ - -static NodeStat * CreateBotDist ARGS((DdNode * node, st_table * distanceTable)); -static double CountMinterms ARGS((DdNode * node, double max, st_table * mintermTable, FILE *fp)); -static void ConjunctsFree ARGS((DdManager * dd, Conjuncts * factors)); -static int PairInTables ARGS((DdNode * g, DdNode * h, st_table * ghTable)); -static Conjuncts * CheckTablesCacheAndReturn ARGS((DdNode * node, DdNode * g, DdNode * h, st_table * ghTable, st_table * cacheTable)); -static Conjuncts * PickOnePair ARGS((DdNode * node, DdNode * g1, DdNode * h1, DdNode * g2, DdNode * h2, st_table * ghTable, st_table * cacheTable)); -static Conjuncts * CheckInTables ARGS((DdNode * node, DdNode * g1, DdNode * h1, DdNode * g2, DdNode * h2, st_table * ghTable, st_table * cacheTable, int * outOfMem)); -static Conjuncts * ZeroCase ARGS((DdManager * dd, DdNode * node, Conjuncts * factorsNv, st_table * ghTable, st_table * cacheTable, int switched)); -static Conjuncts * BuildConjuncts ARGS((DdManager * dd, DdNode * node, st_table * distanceTable, st_table * cacheTable, int approxDistance, int maxLocalRef, st_table * ghTable, st_table * mintermTable)); -static int cuddConjunctsAux ARGS((DdManager * dd, DdNode * f, DdNode ** c1, DdNode ** c2)); - -/**AutomaticEnd***************************************************************/ - - -/*---------------------------------------------------------------------------*/ -/* Definition of exported functions */ -/*---------------------------------------------------------------------------*/ - - -/**Function******************************************************************** - - Synopsis [Performs two-way conjunctive decomposition of a BDD.] - - Description [Performs two-way conjunctive decomposition of a - BDD. This procedure owes its name to the use of supersetting to - obtain an initial factor of the given function. Returns the number - of conjuncts produced, that is, 2 if successful; 1 if no meaningful - decomposition was found; 0 otherwise. The conjuncts produced by this - procedure tend to be imbalanced.] - - SideEffects [The factors are returned in an array as side effects. - The array is allocated by this function. It is the caller's responsibility - to free it. On successful completion, the conjuncts are already - referenced. If the function returns 0, the array for the conjuncts is - not allocated. If the function returns 1, the only factor equals the - function to be decomposed.] - - SeeAlso [Cudd_bddApproxDisjDecomp Cudd_bddIterConjDecomp - Cudd_bddGenConjDecomp Cudd_bddVarConjDecomp Cudd_RemapOverApprox - Cudd_bddSqueeze Cudd_bddLICompaction] - -******************************************************************************/ -int -Cudd_bddApproxConjDecomp( - DdManager * dd /* manager */, - DdNode * f /* function to be decomposed */, - DdNode *** conjuncts /* address of the first factor */) -{ - DdNode *superset1, *superset2, *glocal, *hlocal; - int nvars = Cudd_SupportSize(dd,f); - - /* Find a tentative first factor by overapproximation and minimization. */ - superset1 = Cudd_RemapOverApprox(dd,f,nvars,0,1.0); - if (superset1 == NULL) return(0); - cuddRef(superset1); - superset2 = Cudd_bddSqueeze(dd,f,superset1); - if (superset2 == NULL) { - Cudd_RecursiveDeref(dd,superset1); - return(0); - } - cuddRef(superset2); - Cudd_RecursiveDeref(dd,superset1); - - /* Compute the second factor by minimization. */ - hlocal = Cudd_bddLICompaction(dd,f,superset2); - if (hlocal == NULL) { - Cudd_RecursiveDeref(dd,superset2); - return(0); - } - cuddRef(hlocal); - - /* Refine the first factor by minimization. If h turns out to be f, this - ** step guarantees that g will be 1. */ - glocal = Cudd_bddLICompaction(dd,superset2,hlocal); - if (glocal == NULL) { - Cudd_RecursiveDeref(dd,superset2); - Cudd_RecursiveDeref(dd,hlocal); - return(0); - } - cuddRef(glocal); - Cudd_RecursiveDeref(dd,superset2); - - if (glocal != DD_ONE(dd)) { - if (hlocal != DD_ONE(dd)) { - *conjuncts = ALLOC(DdNode *,2); - if (*conjuncts == NULL) { - Cudd_RecursiveDeref(dd,glocal); - Cudd_RecursiveDeref(dd,hlocal); - dd->errorCode = CUDD_MEMORY_OUT; - return(0); - } - (*conjuncts)[0] = glocal; - (*conjuncts)[1] = hlocal; - return(2); - } else { - Cudd_RecursiveDeref(dd,hlocal); - *conjuncts = ALLOC(DdNode *,1); - if (*conjuncts == NULL) { - Cudd_RecursiveDeref(dd,glocal); - dd->errorCode = CUDD_MEMORY_OUT; - return(0); - } - (*conjuncts)[0] = glocal; - return(1); - } - } else { - Cudd_RecursiveDeref(dd,glocal); - *conjuncts = ALLOC(DdNode *,1); - if (*conjuncts == NULL) { - Cudd_RecursiveDeref(dd,hlocal); - dd->errorCode = CUDD_MEMORY_OUT; - return(0); - } - (*conjuncts)[0] = hlocal; - return(1); - } - -} /* end of Cudd_bddApproxConjDecomp */ - - -/**Function******************************************************************** - - Synopsis [Performs two-way disjunctive decomposition of a BDD.] - - Description [Performs two-way disjunctive decomposition of a BDD. - Returns the number of disjuncts produced, that is, 2 if successful; - 1 if no meaningful decomposition was found; 0 otherwise. The - disjuncts produced by this procedure tend to be imbalanced.] - - SideEffects [The two disjuncts are returned in an array as side effects. - The array is allocated by this function. It is the caller's responsibility - to free it. On successful completion, the disjuncts are already - referenced. If the function returns 0, the array for the disjuncts is - not allocated. If the function returns 1, the only factor equals the - function to be decomposed.] - - SeeAlso [Cudd_bddApproxConjDecomp Cudd_bddIterDisjDecomp - Cudd_bddGenDisjDecomp Cudd_bddVarDisjDecomp] - -******************************************************************************/ -int -Cudd_bddApproxDisjDecomp( - DdManager * dd /* manager */, - DdNode * f /* function to be decomposed */, - DdNode *** disjuncts /* address of the array of the disjuncts */) -{ - int result, i; - - result = Cudd_bddApproxConjDecomp(dd,Cudd_Not(f),disjuncts); - for (i = 0; i < result; i++) { - (*disjuncts)[i] = Cudd_Not((*disjuncts)[i]); - } - return(result); - -} /* end of Cudd_bddApproxDisjDecomp */ - - -/**Function******************************************************************** - - Synopsis [Performs two-way conjunctive decomposition of a BDD.] - - Description [Performs two-way conjunctive decomposition of a - BDD. This procedure owes its name to the iterated use of - supersetting to obtain a factor of the given function. Returns the - number of conjuncts produced, that is, 2 if successful; 1 if no - meaningful decomposition was found; 0 otherwise. The conjuncts - produced by this procedure tend to be imbalanced.] - - SideEffects [The factors are returned in an array as side effects. - The array is allocated by this function. It is the caller's responsibility - to free it. On successful completion, the conjuncts are already - referenced. If the function returns 0, the array for the conjuncts is - not allocated. If the function returns 1, the only factor equals the - function to be decomposed.] - - SeeAlso [Cudd_bddIterDisjDecomp Cudd_bddApproxConjDecomp - Cudd_bddGenConjDecomp Cudd_bddVarConjDecomp Cudd_RemapOverApprox - Cudd_bddSqueeze Cudd_bddLICompaction] - -******************************************************************************/ -int -Cudd_bddIterConjDecomp( - DdManager * dd /* manager */, - DdNode * f /* function to be decomposed */, - DdNode *** conjuncts /* address of the array of conjuncts */) -{ - DdNode *superset1, *superset2, *old[2], *res[2]; - int sizeOld, sizeNew; - int nvars = Cudd_SupportSize(dd,f); - - old[0] = DD_ONE(dd); - cuddRef(old[0]); - old[1] = f; - cuddRef(old[1]); - sizeOld = Cudd_SharingSize(old,2); - - do { - /* Find a tentative first factor by overapproximation and - ** minimization. */ - superset1 = Cudd_RemapOverApprox(dd,old[1],nvars,0,1.0); - if (superset1 == NULL) { - Cudd_RecursiveDeref(dd,old[0]); - Cudd_RecursiveDeref(dd,old[1]); - return(0); - } - cuddRef(superset1); - superset2 = Cudd_bddSqueeze(dd,old[1],superset1); - if (superset2 == NULL) { - Cudd_RecursiveDeref(dd,old[0]); - Cudd_RecursiveDeref(dd,old[1]); - Cudd_RecursiveDeref(dd,superset1); - return(0); - } - cuddRef(superset2); - Cudd_RecursiveDeref(dd,superset1); - res[0] = Cudd_bddAnd(dd,old[0],superset2); - if (res[0] == NULL) { - Cudd_RecursiveDeref(dd,superset2); - Cudd_RecursiveDeref(dd,old[0]); - Cudd_RecursiveDeref(dd,old[1]); - return(0); - } - cuddRef(res[0]); - Cudd_RecursiveDeref(dd,superset2); - if (res[0] == old[0]) { - Cudd_RecursiveDeref(dd,res[0]); - break; /* avoid infinite loop */ - } - - /* Compute the second factor by minimization. */ - res[1] = Cudd_bddLICompaction(dd,old[1],res[0]); - if (res[1] == NULL) { - Cudd_RecursiveDeref(dd,old[0]); - Cudd_RecursiveDeref(dd,old[1]); - return(0); - } - cuddRef(res[1]); - - sizeNew = Cudd_SharingSize(res,2); - if (sizeNew <= sizeOld) { - Cudd_RecursiveDeref(dd,old[0]); - old[0] = res[0]; - Cudd_RecursiveDeref(dd,old[1]); - old[1] = res[1]; - sizeOld = sizeNew; - } else { - Cudd_RecursiveDeref(dd,res[0]); - Cudd_RecursiveDeref(dd,res[1]); - break; - } - - } while (1); - - /* Refine the first factor by minimization. If h turns out to - ** be f, this step guarantees that g will be 1. */ - superset1 = Cudd_bddLICompaction(dd,old[0],old[1]); - if (superset1 == NULL) { - Cudd_RecursiveDeref(dd,old[0]); - Cudd_RecursiveDeref(dd,old[1]); - return(0); - } - cuddRef(superset1); - Cudd_RecursiveDeref(dd,old[0]); - old[0] = superset1; - - if (old[0] != DD_ONE(dd)) { - if (old[1] != DD_ONE(dd)) { - *conjuncts = ALLOC(DdNode *,2); - if (*conjuncts == NULL) { - Cudd_RecursiveDeref(dd,old[0]); - Cudd_RecursiveDeref(dd,old[1]); - dd->errorCode = CUDD_MEMORY_OUT; - return(0); - } - (*conjuncts)[0] = old[0]; - (*conjuncts)[1] = old[1]; - return(2); - } else { - Cudd_RecursiveDeref(dd,old[1]); - *conjuncts = ALLOC(DdNode *,1); - if (*conjuncts == NULL) { - Cudd_RecursiveDeref(dd,old[0]); - dd->errorCode = CUDD_MEMORY_OUT; - return(0); - } - (*conjuncts)[0] = old[0]; - return(1); - } - } else { - Cudd_RecursiveDeref(dd,old[0]); - *conjuncts = ALLOC(DdNode *,1); - if (*conjuncts == NULL) { - Cudd_RecursiveDeref(dd,old[1]); - dd->errorCode = CUDD_MEMORY_OUT; - return(0); - } - (*conjuncts)[0] = old[1]; - return(1); - } - -} /* end of Cudd_bddIterConjDecomp */ - - -/**Function******************************************************************** - - Synopsis [Performs two-way disjunctive decomposition of a BDD.] - - Description [Performs two-way disjunctive decomposition of a BDD. - Returns the number of disjuncts produced, that is, 2 if successful; - 1 if no meaningful decomposition was found; 0 otherwise. The - disjuncts produced by this procedure tend to be imbalanced.] - - SideEffects [The two disjuncts are returned in an array as side effects. - The array is allocated by this function. It is the caller's responsibility - to free it. On successful completion, the disjuncts are already - referenced. If the function returns 0, the array for the disjuncts is - not allocated. If the function returns 1, the only factor equals the - function to be decomposed.] - - SeeAlso [Cudd_bddIterConjDecomp Cudd_bddApproxDisjDecomp - Cudd_bddGenDisjDecomp Cudd_bddVarDisjDecomp] - -******************************************************************************/ -int -Cudd_bddIterDisjDecomp( - DdManager * dd /* manager */, - DdNode * f /* function to be decomposed */, - DdNode *** disjuncts /* address of the array of the disjuncts */) -{ - int result, i; - - result = Cudd_bddIterConjDecomp(dd,Cudd_Not(f),disjuncts); - for (i = 0; i < result; i++) { - (*disjuncts)[i] = Cudd_Not((*disjuncts)[i]); - } - return(result); - -} /* end of Cudd_bddIterDisjDecomp */ - - -/**Function******************************************************************** - - Synopsis [Performs two-way conjunctive decomposition of a BDD.] - - Description [Performs two-way conjunctive decomposition of a - BDD. This procedure owes its name to the fact tht it generalizes the - decomposition based on the cofactors with respect to one - variable. Returns the number of conjuncts produced, that is, 2 if - successful; 1 if no meaningful decomposition was found; 0 - otherwise. The conjuncts produced by this procedure tend to be - balanced.] - - SideEffects [The two factors are returned in an array as side effects. - The array is allocated by this function. It is the caller's responsibility - to free it. On successful completion, the conjuncts are already - referenced. If the function returns 0, the array for the conjuncts is - not allocated. If the function returns 1, the only factor equals the - function to be decomposed.] - - SeeAlso [Cudd_bddGenDisjDecomp Cudd_bddApproxConjDecomp - Cudd_bddIterConjDecomp Cudd_bddVarConjDecomp] - -******************************************************************************/ -int -Cudd_bddGenConjDecomp( - DdManager * dd /* manager */, - DdNode * f /* function to be decomposed */, - DdNode *** conjuncts /* address of the array of conjuncts */) -{ - int result; - DdNode *glocal, *hlocal; - - one = DD_ONE(dd); - zero = Cudd_Not(one); - - do { - dd->reordered = 0; - result = cuddConjunctsAux(dd, f, &glocal, &hlocal); - } while (dd->reordered == 1); - - if (result == 0) { - return(0); - } - - if (glocal != one) { - if (hlocal != one) { - *conjuncts = ALLOC(DdNode *,2); - if (*conjuncts == NULL) { - Cudd_RecursiveDeref(dd,glocal); - Cudd_RecursiveDeref(dd,hlocal); - dd->errorCode = CUDD_MEMORY_OUT; - return(0); - } - (*conjuncts)[0] = glocal; - (*conjuncts)[1] = hlocal; - return(2); - } else { - Cudd_RecursiveDeref(dd,hlocal); - *conjuncts = ALLOC(DdNode *,1); - if (*conjuncts == NULL) { - Cudd_RecursiveDeref(dd,glocal); - dd->errorCode = CUDD_MEMORY_OUT; - return(0); - } - (*conjuncts)[0] = glocal; - return(1); - } - } else { - Cudd_RecursiveDeref(dd,glocal); - *conjuncts = ALLOC(DdNode *,1); - if (*conjuncts == NULL) { - Cudd_RecursiveDeref(dd,hlocal); - dd->errorCode = CUDD_MEMORY_OUT; - return(0); - } - (*conjuncts)[0] = hlocal; - return(1); - } - -} /* end of Cudd_bddGenConjDecomp */ - - -/**Function******************************************************************** - - Synopsis [Performs two-way disjunctive decomposition of a BDD.] - - Description [Performs two-way disjunctive decomposition of a BDD. - Returns the number of disjuncts produced, that is, 2 if successful; - 1 if no meaningful decomposition was found; 0 otherwise. The - disjuncts produced by this procedure tend to be balanced.] - - SideEffects [The two disjuncts are returned in an array as side effects. - The array is allocated by this function. It is the caller's responsibility - to free it. On successful completion, the disjuncts are already - referenced. If the function returns 0, the array for the disjuncts is - not allocated. If the function returns 1, the only factor equals the - function to be decomposed.] - - SeeAlso [Cudd_bddGenConjDecomp Cudd_bddApproxDisjDecomp - Cudd_bddIterDisjDecomp Cudd_bddVarDisjDecomp] - -******************************************************************************/ -int -Cudd_bddGenDisjDecomp( - DdManager * dd /* manager */, - DdNode * f /* function to be decomposed */, - DdNode *** disjuncts /* address of the array of the disjuncts */) -{ - int result, i; - - result = Cudd_bddGenConjDecomp(dd,Cudd_Not(f),disjuncts); - for (i = 0; i < result; i++) { - (*disjuncts)[i] = Cudd_Not((*disjuncts)[i]); - } - return(result); - -} /* end of Cudd_bddGenDisjDecomp */ - - -/**Function******************************************************************** - - Synopsis [Performs two-way conjunctive decomposition of a BDD.] - - Description [Conjunctively decomposes one BDD according to a - variable. If f is the function of the BDD and - x is the variable, the decomposition is - (f+x)(f+x'). The variable is chosen so as to balance - the sizes of the two conjuncts and to keep them small. Returns the - number of conjuncts produced, that is, 2 if successful; 1 if no - meaningful decomposition was found; 0 otherwise.] - - SideEffects [The two factors are returned in an array as side effects. - The array is allocated by this function. It is the caller's responsibility - to free it. On successful completion, the conjuncts are already - referenced. If the function returns 0, the array for the conjuncts is - not allocated. If the function returns 1, the only factor equals the - function to be decomposed.] - - SeeAlso [Cudd_bddVarDisjDecomp Cudd_bddGenConjDecomp - Cudd_bddApproxConjDecomp Cudd_bddIterConjDecomp] - -*****************************************************************************/ -int -Cudd_bddVarConjDecomp( - DdManager * dd /* manager */, - DdNode * f /* function to be decomposed */, - DdNode *** conjuncts /* address of the array of conjuncts */) -{ - int best; - int min; - DdNode *support, *scan, *var, *glocal, *hlocal; - - /* Find best cofactoring variable. */ - support = Cudd_Support(dd,f); - if (support == NULL) return(0); - if (Cudd_IsConstant(support)) { - *conjuncts = ALLOC(DdNode *,1); - if (*conjuncts == NULL) { - dd->errorCode = CUDD_MEMORY_OUT; - return(0); - } - (*conjuncts)[0] = f; - cuddRef((*conjuncts)[0]); - return(1); - } - cuddRef(support); - min = 1000000000; - best = -1; - scan = support; - while (!Cudd_IsConstant(scan)) { - int i = scan->index; - int est1 = Cudd_EstimateCofactor(dd,f,i,1); - int est0 = Cudd_EstimateCofactor(dd,f,i,0); - /* Minimize the size of the larger of the two cofactors. */ - int est = (est1 > est0) ? est1 : est0; - if (est < min) { - min = est; - best = i; - } - scan = cuddT(scan); - } -#ifdef DD_DEBUG - assert(best >= 0 && best < dd->size); -#endif - Cudd_RecursiveDeref(dd,support); - - var = Cudd_bddIthVar(dd,best); - glocal = Cudd_bddOr(dd,f,var); - if (glocal == NULL) { - return(0); - } - cuddRef(glocal); - hlocal = Cudd_bddOr(dd,f,Cudd_Not(var)); - if (hlocal == NULL) { - Cudd_RecursiveDeref(dd,glocal); - return(0); - } - cuddRef(hlocal); - - if (glocal != DD_ONE(dd)) { - if (hlocal != DD_ONE(dd)) { - *conjuncts = ALLOC(DdNode *,2); - if (*conjuncts == NULL) { - Cudd_RecursiveDeref(dd,glocal); - Cudd_RecursiveDeref(dd,hlocal); - dd->errorCode = CUDD_MEMORY_OUT; - return(0); - } - (*conjuncts)[0] = glocal; - (*conjuncts)[1] = hlocal; - return(2); - } else { - Cudd_RecursiveDeref(dd,hlocal); - *conjuncts = ALLOC(DdNode *,1); - if (*conjuncts == NULL) { - Cudd_RecursiveDeref(dd,glocal); - dd->errorCode = CUDD_MEMORY_OUT; - return(0); - } - (*conjuncts)[0] = glocal; - return(1); - } - } else { - Cudd_RecursiveDeref(dd,glocal); - *conjuncts = ALLOC(DdNode *,1); - if (*conjuncts == NULL) { - Cudd_RecursiveDeref(dd,hlocal); - dd->errorCode = CUDD_MEMORY_OUT; - return(0); - } - (*conjuncts)[0] = hlocal; - return(1); - } - -} /* end of Cudd_bddVarConjDecomp */ - - -/**Function******************************************************************** - - Synopsis [Performs two-way disjunctive decomposition of a BDD.] - - Description [Performs two-way disjunctive decomposition of a BDD - according to a variable. If f is the function of the - BDD and x is the variable, the decomposition is - f*x + f*x'. The variable is chosen so as to balance - the sizes of the two disjuncts and to keep them small. Returns the - number of disjuncts produced, that is, 2 if successful; 1 if no - meaningful decomposition was found; 0 otherwise.] - - SideEffects [The two disjuncts are returned in an array as side effects. - The array is allocated by this function. It is the caller's responsibility - to free it. On successful completion, the disjuncts are already - referenced. If the function returns 0, the array for the disjuncts is - not allocated. If the function returns 1, the only factor equals the - function to be decomposed.] - - SeeAlso [Cudd_bddVarConjDecomp Cudd_bddApproxDisjDecomp - Cudd_bddIterDisjDecomp Cudd_bddGenDisjDecomp] - -******************************************************************************/ -int -Cudd_bddVarDisjDecomp( - DdManager * dd /* manager */, - DdNode * f /* function to be decomposed */, - DdNode *** disjuncts /* address of the array of the disjuncts */) -{ - int result, i; - - result = Cudd_bddVarConjDecomp(dd,Cudd_Not(f),disjuncts); - for (i = 0; i < result; i++) { - (*disjuncts)[i] = Cudd_Not((*disjuncts)[i]); - } - return(result); - -} /* end of Cudd_bddVarDisjDecomp */ - - -/*---------------------------------------------------------------------------*/ -/* Definition of internal functions */ -/*---------------------------------------------------------------------------*/ - -/*---------------------------------------------------------------------------*/ -/* Definition of static functions */ -/*---------------------------------------------------------------------------*/ - - -/**Function******************************************************************** - - Synopsis [Get longest distance of node from constant.] - - Description [Get longest distance of node from constant. Returns the - distance of the root from the constant if successful; CUDD_OUT_OF_MEM - otherwise.] - - SideEffects [None] - - SeeAlso [] - -******************************************************************************/ -static NodeStat * -CreateBotDist( - DdNode * node, - st_table * distanceTable) -{ - DdNode *N, *Nv, *Nnv; - int distance, distanceNv, distanceNnv; - NodeStat *nodeStat, *nodeStatNv, *nodeStatNnv; - -#if 0 - if (Cudd_IsConstant(node)) { - return(0); - } -#endif - - /* Return the entry in the table if found. */ - N = Cudd_Regular(node); - if (st_lookup(distanceTable, (char *)N, (char **)&nodeStat)) { - nodeStat->localRef++; - return(nodeStat); - } - - Nv = cuddT(N); - Nnv = cuddE(N); - Nv = Cudd_NotCond(Nv, Cudd_IsComplement(node)); - Nnv = Cudd_NotCond(Nnv, Cudd_IsComplement(node)); - - /* Recur on the children. */ - nodeStatNv = CreateBotDist(Nv, distanceTable); - if (nodeStatNv == NULL) return(NULL); - distanceNv = nodeStatNv->distance; - - nodeStatNnv = CreateBotDist(Nnv, distanceTable); - if (nodeStatNnv == NULL) return(NULL); - distanceNnv = nodeStatNnv->distance; - /* Store max distance from constant; note sometimes this distance - ** may be to 0. - */ - distance = (distanceNv > distanceNnv) ? (distanceNv+1) : (distanceNnv + 1); - - nodeStat = ALLOC(NodeStat, 1); - if (nodeStat == NULL) { - return(0); - } - nodeStat->distance = distance; - nodeStat->localRef = 1; - - if (st_insert(distanceTable, (char *)N, (char *)nodeStat) == - ST_OUT_OF_MEM) { - return(0); - - } - return(nodeStat); - -} /* end of CreateBotDist */ - - -/**Function******************************************************************** - - Synopsis [Count the number of minterms of each node ina a BDD and - store it in a hash table.] - - Description [] - - SideEffects [None] - - SeeAlso [] - -******************************************************************************/ -static double -CountMinterms( - DdNode * node, - double max, - st_table * mintermTable, - FILE *fp) -{ - DdNode *N, *Nv, *Nnv; - double min, minNv, minNnv; - double *dummy; - - N = Cudd_Regular(node); - - if (cuddIsConstant(N)) { - if (node == zero) { - return(0); - } else { - return(max); - } - } - - /* Return the entry in the table if found. */ - if (st_lookup(mintermTable, (char *)node, (char **)&dummy)) { - min = *dummy; - return(min); - } - - Nv = cuddT(N); - Nnv = cuddE(N); - Nv = Cudd_NotCond(Nv, Cudd_IsComplement(node)); - Nnv = Cudd_NotCond(Nnv, Cudd_IsComplement(node)); - - /* Recur on the children. */ - minNv = CountMinterms(Nv, max, mintermTable, fp); - if (minNv == -1.0) return(-1.0); - minNnv = CountMinterms(Nnv, max, mintermTable, fp); - if (minNnv == -1.0) return(-1.0); - min = minNv / 2.0 + minNnv / 2.0; - /* store - */ - - dummy = ALLOC(double, 1); - if (dummy == NULL) return(-1.0); - *dummy = min; - if (st_insert(mintermTable, (char *)node, (char *)dummy) == ST_OUT_OF_MEM) { - (void) fprintf(fp, "st table insert failed\n"); - } - return(min); - -} /* end of CountMinterms */ - - -/**Function******************************************************************** - - Synopsis [Free factors structure] - - Description [] - - SideEffects [None] - - SeeAlso [] - -******************************************************************************/ -static void -ConjunctsFree( - DdManager * dd, - Conjuncts * factors) -{ - Cudd_RecursiveDeref(dd, factors->g); - Cudd_RecursiveDeref(dd, factors->h); - FREE(factors); - return; - -} /* end of ConjunctsFree */ - - -/**Function******************************************************************** - - Synopsis [Check whether the given pair is in the tables.] - - Description [.Check whether the given pair is in the tables. gTable - and hTable are combined. - absence in both is indicated by 0, - presence in gTable is indicated by 1, - presence in hTable by 2 and - presence in both by 3. - The values returned by this function are PAIR_ST, - PAIR_CR, G_ST, G_CR, H_ST, H_CR, BOTH_G, BOTH_H, NONE. - PAIR_ST implies g in gTable and h in hTable - PAIR_CR implies g in hTable and h in gTable - G_ST implies g in gTable and h not in any table - G_CR implies g in hTable and h not in any table - H_ST implies h in hTable and g not in any table - H_CR implies h in gTable and g not in any table - BOTH_G implies both in gTable - BOTH_H implies both in hTable - NONE implies none in table; ] - - SideEffects [] - - SeeAlso [CheckTablesCacheAndReturn CheckInTables] - -******************************************************************************/ -static int -PairInTables( - DdNode * g, - DdNode * h, - st_table * ghTable) -{ - int valueG, valueH, gPresent, hPresent; - - valueG = valueH = gPresent = hPresent = 0; - - gPresent = st_lookup_int(ghTable, (char *)Cudd_Regular(g), &valueG); - hPresent = st_lookup_int(ghTable, (char *)Cudd_Regular(h), &valueH); - - if (!gPresent && !hPresent) return(NONE); - - if (!hPresent) { - if (valueG & 1) return(G_ST); - if (valueG & 2) return(G_CR); - } - if (!gPresent) { - if (valueH & 1) return(H_CR); - if (valueH & 2) return(H_ST); - } - /* both in tables */ - if ((valueG & 1) && (valueH & 2)) return(PAIR_ST); - if ((valueG & 2) && (valueH & 1)) return(PAIR_CR); - - if (valueG & 1) { - return(BOTH_G); - } else { - return(BOTH_H); - } - -} /* end of PairInTables */ - - -/**Function******************************************************************** - - Synopsis [Check the tables for the existence of pair and return one - combination, cache the result.] - - Description [Check the tables for the existence of pair and return - one combination, cache the result. The assumption is that one of the - conjuncts is already in the tables.] - - SideEffects [g and h referenced for the cache] - - SeeAlso [ZeroCase] - -******************************************************************************/ -static Conjuncts * -CheckTablesCacheAndReturn( - DdNode * node, - DdNode * g, - DdNode * h, - st_table * ghTable, - st_table * cacheTable) -{ - int pairValue; - int value; - Conjuncts *factors; - - value = 0; - /* check tables */ - pairValue = PairInTables(g, h, ghTable); - assert(pairValue != NONE); - /* if both dont exist in table, we know one exists(either g or h). - * Therefore store the other and proceed - */ - factors = ALLOC(Conjuncts, 1); - if (factors == NULL) return(NULL); - if ((pairValue == BOTH_H) || (pairValue == H_ST)) { - if (g != one) { - value = 0; - if (st_lookup_int(ghTable, (char *)Cudd_Regular(g), &value)) { - value |= 1; - } else { - value = 1; - } - if (st_insert(ghTable, (char *)Cudd_Regular(g), - (char *)(long)value) == ST_OUT_OF_MEM) { - return(NULL); - } - } - factors->g = g; - factors->h = h; - } else if ((pairValue == BOTH_G) || (pairValue == G_ST)) { - if (h != one) { - value = 0; - if (st_lookup_int(ghTable, (char *)Cudd_Regular(h), &value)) { - value |= 2; - } else { - value = 2; - } - if (st_insert(ghTable, (char *)Cudd_Regular(h), - (char *)(long)value) == ST_OUT_OF_MEM) { - return(NULL); - } - } - factors->g = g; - factors->h = h; - } else if (pairValue == H_CR) { - if (g != one) { - value = 2; - if (st_insert(ghTable, (char *)Cudd_Regular(g), - (char *)(long)value) == ST_OUT_OF_MEM) { - return(NULL); - } - } - factors->g = h; - factors->h = g; - } else if (pairValue == G_CR) { - if (h != one) { - value = 1; - if (st_insert(ghTable, (char *)Cudd_Regular(h), - (char *)(long)value) == ST_OUT_OF_MEM) { - return(NULL); - } - } - factors->g = h; - factors->h = g; - } else if (pairValue == PAIR_CR) { - /* pair exists in table */ - factors->g = h; - factors->h = g; - } else if (pairValue == PAIR_ST) { - factors->g = g; - factors->h = h; - } - - /* cache the result for this node */ - if (st_insert(cacheTable, (char *)node, (char *)factors) == ST_OUT_OF_MEM) { - FREE(factors); - return(NULL); - } - - return(factors); - -} /* end of CheckTablesCacheAndReturn */ - -/**Function******************************************************************** - - Synopsis [Check the tables for the existence of pair and return one - combination, store in cache.] - - Description [Check the tables for the existence of pair and return - one combination, store in cache. The pair that has more pointers to - it is picked. An approximation of the number of local pointers is - made by taking the reference count of the pairs sent. ] - - SideEffects [] - - SeeAlso [ZeroCase BuildConjuncts] - -******************************************************************************/ -static Conjuncts * -PickOnePair( - DdNode * node, - DdNode * g1, - DdNode * h1, - DdNode * g2, - DdNode * h2, - st_table * ghTable, - st_table * cacheTable) -{ - int value; - Conjuncts *factors; - int oneRef, twoRef; - - factors = ALLOC(Conjuncts, 1); - if (factors == NULL) return(NULL); - - /* count the number of pointers to pair 2 */ - if (h2 == one) { - twoRef = (Cudd_Regular(g2))->ref; - } else if (g2 == one) { - twoRef = (Cudd_Regular(h2))->ref; - } else { - twoRef = ((Cudd_Regular(g2))->ref + (Cudd_Regular(h2))->ref)/2; - } - - /* count the number of pointers to pair 1 */ - if (h1 == one) { - oneRef = (Cudd_Regular(g1))->ref; - } else if (g1 == one) { - oneRef = (Cudd_Regular(h1))->ref; - } else { - oneRef = ((Cudd_Regular(g1))->ref + (Cudd_Regular(h1))->ref)/2; - } - - /* pick the pair with higher reference count */ - if (oneRef >= twoRef) { - factors->g = g1; - factors->h = h1; - } else { - factors->g = g2; - factors->h = h2; - } - - /* - * Store computed factors in respective tables to encourage - * recombination. - */ - if (factors->g != one) { - /* insert g in htable */ - value = 0; - if (st_lookup_int(ghTable, (char *)Cudd_Regular(factors->g), &value)) { - if (value == 2) { - value |= 1; - if (st_insert(ghTable, (char *)Cudd_Regular(factors->g), - (char *)(long)value) == ST_OUT_OF_MEM) { - FREE(factors); - return(NULL); - } - } - } else { - value = 1; - if (st_insert(ghTable, (char *)Cudd_Regular(factors->g), - (char *)(long)value) == ST_OUT_OF_MEM) { - FREE(factors); - return(NULL); - } - } - } - - if (factors->h != one) { - /* insert h in htable */ - value = 0; - if (st_lookup_int(ghTable, (char *)Cudd_Regular(factors->h), &value)) { - if (value == 1) { - value |= 2; - if (st_insert(ghTable, (char *)Cudd_Regular(factors->h), - (char *)(long)value) == ST_OUT_OF_MEM) { - FREE(factors); - return(NULL); - } - } - } else { - value = 2; - if (st_insert(ghTable, (char *)Cudd_Regular(factors->h), - (char *)(long)value) == ST_OUT_OF_MEM) { - FREE(factors); - return(NULL); - } - } - } - - /* Store factors in cache table for later use. */ - if (st_insert(cacheTable, (char *)node, (char *)factors) == - ST_OUT_OF_MEM) { - FREE(factors); - return(NULL); - } - - return(factors); - -} /* end of PickOnePair */ - - -/**Function******************************************************************** - - Synopsis [Check if the two pairs exist in the table, If any of the - conjuncts do exist, store in the cache and return the corresponding pair.] - - Description [Check if the two pairs exist in the table. If any of - the conjuncts do exist, store in the cache and return the - corresponding pair.] - - SideEffects [] - - SeeAlso [ZeroCase BuildConjuncts] - -******************************************************************************/ -static Conjuncts * -CheckInTables( - DdNode * node, - DdNode * g1, - DdNode * h1, - DdNode * g2, - DdNode * h2, - st_table * ghTable, - st_table * cacheTable, - int * outOfMem) -{ - int pairValue1, pairValue2; - Conjuncts *factors; - int value; - - *outOfMem = 0; - - /* check existence of pair in table */ - pairValue1 = PairInTables(g1, h1, ghTable); - pairValue2 = PairInTables(g2, h2, ghTable); - - /* if none of the 4 exist in the gh tables, return NULL */ - if ((pairValue1 == NONE) && (pairValue2 == NONE)) { - return NULL; - } - - factors = ALLOC(Conjuncts, 1); - if (factors == NULL) { - *outOfMem = 1; - return NULL; - } - - /* pairs that already exist in the table get preference. */ - if (pairValue1 == PAIR_ST) { - factors->g = g1; - factors->h = h1; - } else if (pairValue2 == PAIR_ST) { - factors->g = g2; - factors->h = h2; - } else if (pairValue1 == PAIR_CR) { - factors->g = h1; - factors->h = g1; - } else if (pairValue2 == PAIR_CR) { - factors->g = h2; - factors->h = g2; - } else if (pairValue1 == G_ST) { - /* g exists in the table, h is not found in either table */ - factors->g = g1; - factors->h = h1; - if (h1 != one) { - value = 2; - if (st_insert(ghTable, (char *)Cudd_Regular(h1), - (char *)(long)value) == ST_OUT_OF_MEM) { - *outOfMem = 1; - FREE(factors); - return(NULL); - } - } - } else if (pairValue1 == BOTH_G) { - /* g and h are found in the g table */ - factors->g = g1; - factors->h = h1; - if (h1 != one) { - value = 3; - if (st_insert(ghTable, (char *)Cudd_Regular(h1), - (char *)(long)value) == ST_OUT_OF_MEM) { - *outOfMem = 1; - FREE(factors); - return(NULL); - } - } - } else if (pairValue1 == H_ST) { - /* h exists in the table, g is not found in either table */ - factors->g = g1; - factors->h = h1; - if (g1 != one) { - value = 1; - if (st_insert(ghTable, (char *)Cudd_Regular(g1), - (char *)(long)value) == ST_OUT_OF_MEM) { - *outOfMem = 1; - FREE(factors); - return(NULL); - } - } - } else if (pairValue1 == BOTH_H) { - /* g and h are found in the h table */ - factors->g = g1; - factors->h = h1; - if (g1 != one) { - value = 3; - if (st_insert(ghTable, (char *)Cudd_Regular(g1), - (char *)(long)value) == ST_OUT_OF_MEM) { - *outOfMem = 1; - FREE(factors); - return(NULL); - } - } - } else if (pairValue2 == G_ST) { - /* g exists in the table, h is not found in either table */ - factors->g = g2; - factors->h = h2; - if (h2 != one) { - value = 2; - if (st_insert(ghTable, (char *)Cudd_Regular(h2), - (char *)(long)value) == ST_OUT_OF_MEM) { - *outOfMem = 1; - FREE(factors); - return(NULL); - } - } - } else if (pairValue2 == BOTH_G) { - /* g and h are found in the g table */ - factors->g = g2; - factors->h = h2; - if (h2 != one) { - value = 3; - if (st_insert(ghTable, (char *)Cudd_Regular(h2), - (char *)(long)value) == ST_OUT_OF_MEM) { - *outOfMem = 1; - FREE(factors); - return(NULL); - } - } - } else if (pairValue2 == H_ST) { - /* h exists in the table, g is not found in either table */ - factors->g = g2; - factors->h = h2; - if (g2 != one) { - value = 1; - if (st_insert(ghTable, (char *)Cudd_Regular(g2), - (char *)(long)value) == ST_OUT_OF_MEM) { - *outOfMem = 1; - FREE(factors); - return(NULL); - } - } - } else if (pairValue2 == BOTH_H) { - /* g and h are found in the h table */ - factors->g = g2; - factors->h = h2; - if (g2 != one) { - value = 3; - if (st_insert(ghTable, (char *)Cudd_Regular(g2), - (char *)(long)value) == ST_OUT_OF_MEM) { - *outOfMem = 1; - FREE(factors); - return(NULL); - } - } - } else if (pairValue1 == G_CR) { - /* g found in h table and h in none */ - factors->g = h1; - factors->h = g1; - if (h1 != one) { - value = 1; - if (st_insert(ghTable, (char *)Cudd_Regular(h1), - (char *)(long)value) == ST_OUT_OF_MEM) { - *outOfMem = 1; - FREE(factors); - return(NULL); - } - } - } else if (pairValue1 == H_CR) { - /* h found in g table and g in none */ - factors->g = h1; - factors->h = g1; - if (g1 != one) { - value = 2; - if (st_insert(ghTable, (char *)Cudd_Regular(g1), - (char *)(long)value) == ST_OUT_OF_MEM) { - *outOfMem = 1; - FREE(factors); - return(NULL); - } - } - } else if (pairValue2 == G_CR) { - /* g found in h table and h in none */ - factors->g = h2; - factors->h = g2; - if (h2 != one) { - value = 1; - if (st_insert(ghTable, (char *)Cudd_Regular(h2), - (char *)(long)value) == ST_OUT_OF_MEM) { - *outOfMem = 1; - FREE(factors); - return(NULL); - } - } - } else if (pairValue2 == H_CR) { - /* h found in g table and g in none */ - factors->g = h2; - factors->h = g2; - if (g2 != one) { - value = 2; - if (st_insert(ghTable, (char *)Cudd_Regular(g2), - (char *)(long)value) == ST_OUT_OF_MEM) { - *outOfMem = 1; - FREE(factors); - return(NULL); - } - } - } - - /* Store factors in cache table for later use. */ - if (st_insert(cacheTable, (char *)node, (char *)factors) == - ST_OUT_OF_MEM) { - *outOfMem = 1; - FREE(factors); - return(NULL); - } - return factors; -} /* end of CheckInTables */ - - - -/**Function******************************************************************** - - Synopsis [If one child is zero, do explicitly what Restrict does or better] - - Description [If one child is zero, do explicitly what Restrict does or better. - First separate a variable and its child in the base case. In case of a cube - times a function, separate the cube and function. As a last resort, look in - tables.] - - SideEffects [Frees the BDDs in factorsNv. factorsNv itself is not freed - because it is freed above.] - - SeeAlso [BuildConjuncts] - -******************************************************************************/ -static Conjuncts * -ZeroCase( - DdManager * dd, - DdNode * node, - Conjuncts * factorsNv, - st_table * ghTable, - st_table * cacheTable, - int switched) -{ - int topid; - DdNode *g, *h, *g1, *g2, *h1, *h2, *x, *N, *G, *H, *Gv, *Gnv; - DdNode *Hv, *Hnv; - int value; - int outOfMem; - Conjuncts *factors; - - /* get var at this node */ - N = Cudd_Regular(node); - topid = N->index; - x = dd->vars[topid]; - x = (switched) ? Cudd_Not(x): x; - cuddRef(x); - - /* Seprate variable and child */ - if (factorsNv->g == one) { - Cudd_RecursiveDeref(dd, factorsNv->g); - factors = ALLOC(Conjuncts, 1); - if (factors == NULL) { - dd->errorCode = CUDD_MEMORY_OUT; - Cudd_RecursiveDeref(dd, factorsNv->h); - Cudd_RecursiveDeref(dd, x); - return(NULL); - } - factors->g = x; - factors->h = factorsNv->h; - /* cache the result*/ - if (st_insert(cacheTable, (char *)node, (char *)factors) == ST_OUT_OF_MEM) { - dd->errorCode = CUDD_MEMORY_OUT; - Cudd_RecursiveDeref(dd, factorsNv->h); - Cudd_RecursiveDeref(dd, x); - FREE(factors); - return NULL; - } - - /* store x in g table, the other node is already in the table */ - if (st_lookup_int(ghTable, (char *)Cudd_Regular(x), &value)) { - value |= 1; - } else { - value = 1; - } - if (st_insert(ghTable, (char *)Cudd_Regular(x), (char *)(long)value) == ST_OUT_OF_MEM) { - dd->errorCode = CUDD_MEMORY_OUT; - return NULL; - } - return(factors); - } - - /* Seprate variable and child */ - if (factorsNv->h == one) { - Cudd_RecursiveDeref(dd, factorsNv->h); - factors = ALLOC(Conjuncts, 1); - if (factors == NULL) { - dd->errorCode = CUDD_MEMORY_OUT; - Cudd_RecursiveDeref(dd, factorsNv->g); - Cudd_RecursiveDeref(dd, x); - return(NULL); - } - factors->g = factorsNv->g; - factors->h = x; - /* cache the result. */ - if (st_insert(cacheTable, (char *)node, (char *)factors) == ST_OUT_OF_MEM) { - dd->errorCode = CUDD_MEMORY_OUT; - Cudd_RecursiveDeref(dd, factorsNv->g); - Cudd_RecursiveDeref(dd, x); - FREE(factors); - return(NULL); - } - /* store x in h table, the other node is already in the table */ - if (st_lookup_int(ghTable, (char *)Cudd_Regular(x), &value)) { - value |= 2; - } else { - value = 2; - } - if (st_insert(ghTable, (char *)Cudd_Regular(x), (char *)(long)value) == ST_OUT_OF_MEM) { - dd->errorCode = CUDD_MEMORY_OUT; - return NULL; - } - return(factors); - } - - G = Cudd_Regular(factorsNv->g); - Gv = cuddT(G); - Gnv = cuddE(G); - Gv = Cudd_NotCond(Gv, Cudd_IsComplement(node)); - Gnv = Cudd_NotCond(Gnv, Cudd_IsComplement(node)); - /* if the child below is a variable */ - if ((Gv == zero) || (Gnv == zero)) { - h = factorsNv->h; - g = cuddBddAndRecur(dd, x, factorsNv->g); - if (g != NULL) cuddRef(g); - Cudd_RecursiveDeref(dd, factorsNv->g); - Cudd_RecursiveDeref(dd, x); - if (g == NULL) { - Cudd_RecursiveDeref(dd, factorsNv->h); - return NULL; - } - /* CheckTablesCacheAndReturn responsible for allocating - * factors structure., g,h referenced for cache store the - */ - factors = CheckTablesCacheAndReturn(node, - g, - h, - ghTable, - cacheTable); - if (factors == NULL) { - dd->errorCode = CUDD_MEMORY_OUT; - Cudd_RecursiveDeref(dd, g); - Cudd_RecursiveDeref(dd, h); - } - return(factors); - } - - H = Cudd_Regular(factorsNv->h); - Hv = cuddT(H); - Hnv = cuddE(H); - Hv = Cudd_NotCond(Hv, Cudd_IsComplement(node)); - Hnv = Cudd_NotCond(Hnv, Cudd_IsComplement(node)); - /* if the child below is a variable */ - if ((Hv == zero) || (Hnv == zero)) { - g = factorsNv->g; - h = cuddBddAndRecur(dd, x, factorsNv->h); - if (h!= NULL) cuddRef(h); - Cudd_RecursiveDeref(dd, factorsNv->h); - Cudd_RecursiveDeref(dd, x); - if (h == NULL) { - Cudd_RecursiveDeref(dd, factorsNv->g); - return NULL; - } - /* CheckTablesCacheAndReturn responsible for allocating - * factors structure.g,h referenced for table store - */ - factors = CheckTablesCacheAndReturn(node, - g, - h, - ghTable, - cacheTable); - if (factors == NULL) { - dd->errorCode = CUDD_MEMORY_OUT; - Cudd_RecursiveDeref(dd, g); - Cudd_RecursiveDeref(dd, h); - } - return(factors); - } - - /* build g1 = x*g; h1 = h */ - /* build g2 = g; h2 = x*h */ - Cudd_RecursiveDeref(dd, x); - h1 = factorsNv->h; - g1 = cuddBddAndRecur(dd, x, factorsNv->g); - if (g1 != NULL) cuddRef(g1); - if (g1 == NULL) { - Cudd_RecursiveDeref(dd, factorsNv->g); - Cudd_RecursiveDeref(dd, factorsNv->h); - return NULL; - } - - g2 = factorsNv->g; - h2 = cuddBddAndRecur(dd, x, factorsNv->h); - if (h2 != NULL) cuddRef(h2); - if (h2 == NULL) { - Cudd_RecursiveDeref(dd, factorsNv->h); - Cudd_RecursiveDeref(dd, factorsNv->g); - return NULL; - } - - /* check whether any pair is in tables */ - factors = CheckInTables(node, g1, h1, g2, h2, ghTable, cacheTable, &outOfMem); - if (outOfMem) { - dd->errorCode = CUDD_MEMORY_OUT; - Cudd_RecursiveDeref(dd, g1); - Cudd_RecursiveDeref(dd, h1); - Cudd_RecursiveDeref(dd, g2); - Cudd_RecursiveDeref(dd, h2); - return NULL; - } - if (factors != NULL) { - if ((factors->g == g1) || (factors->g == h1)) { - Cudd_RecursiveDeref(dd, g2); - Cudd_RecursiveDeref(dd, h2); - } else { - Cudd_RecursiveDeref(dd, g1); - Cudd_RecursiveDeref(dd, h1); - } - return factors; - } - - /* check for each pair in tables and choose one */ - factors = PickOnePair(node,g1, h1, g2, h2, ghTable, cacheTable); - if (factors == NULL) { - dd->errorCode = CUDD_MEMORY_OUT; - Cudd_RecursiveDeref(dd, g1); - Cudd_RecursiveDeref(dd, h1); - Cudd_RecursiveDeref(dd, g2); - Cudd_RecursiveDeref(dd, h2); - } else { - /* now free what was created and not used */ - if ((factors->g == g1) || (factors->g == h1)) { - Cudd_RecursiveDeref(dd, g2); - Cudd_RecursiveDeref(dd, h2); - } else { - Cudd_RecursiveDeref(dd, g1); - Cudd_RecursiveDeref(dd, h1); - } - } - - return(factors); -} /* end of ZeroCase */ - - -/**Function******************************************************************** - - Synopsis [Builds the conjuncts recursively, bottom up.] - - Description [Builds the conjuncts recursively, bottom up. Constants - are returned as (f, f). The cache is checked for previously computed - result. The decomposition points are determined by the local - reference count of this node and the longest distance from the - constant. At the decomposition point, the factors returned are (f, - 1). Recur on the two children. The order is determined by the - heavier branch. Combine the factors of the two children and pick the - one that already occurs in the gh table. Occurence in g is indicated - by value 1, occurence in h by 2, occurence in both 3.] - - SideEffects [] - - SeeAlso [cuddConjunctsAux] - -******************************************************************************/ -static Conjuncts * -BuildConjuncts( - DdManager * dd, - DdNode * node, - st_table * distanceTable, - st_table * cacheTable, - int approxDistance, - int maxLocalRef, - st_table * ghTable, - st_table * mintermTable) -{ - int topid, distance; - Conjuncts *factorsNv, *factorsNnv, *factors; - Conjuncts *dummy; - DdNode *N, *Nv, *Nnv, *temp, *g1, *g2, *h1, *h2, *topv; - double minNv = 0.0, minNnv = 0.0; - double *doubleDummy; - int switched =0; - int outOfMem; - int freeNv = 0, freeNnv = 0, freeTemp; - NodeStat *nodeStat; - int value; - - /* if f is constant, return (f,f) */ - if (Cudd_IsConstant(node)) { - factors = ALLOC(Conjuncts, 1); - if (factors == NULL) { - dd->errorCode = CUDD_MEMORY_OUT; - return(NULL); - } - factors->g = node; - factors->h = node; - return(FactorsComplement(factors)); - } - - /* If result (a pair of conjuncts) in cache, return the factors. */ - if (st_lookup(cacheTable, (char *)node, (char **)&dummy)) { - factors = dummy; - return(factors); - } - - /* check distance and local reference count of this node */ - N = Cudd_Regular(node); - if (!st_lookup(distanceTable, (char *)N, (char **)&nodeStat)) { - (void) fprintf(dd->err, "Not in table, Something wrong\n"); - dd->errorCode = CUDD_INTERNAL_ERROR; - return(NULL); - } - distance = nodeStat->distance; - - /* at or below decomposition point, return (f, 1) */ - if (((nodeStat->localRef > maxLocalRef*2/3) && - (distance < approxDistance*2/3)) || - (distance <= approxDistance/4)) { - factors = ALLOC(Conjuncts, 1); - if (factors == NULL) { - dd->errorCode = CUDD_MEMORY_OUT; - return(NULL); - } - /* alternate assigning (f,1) */ - value = 0; - if (st_lookup_int(ghTable, (char *)Cudd_Regular(node), &value)) { - if (value == 3) { - if (!lastTimeG) { - factors->g = node; - factors->h = one; - lastTimeG = 1; - } else { - factors->g = one; - factors->h = node; - lastTimeG = 0; - } - } else if (value == 1) { - factors->g = node; - factors->h = one; - } else { - factors->g = one; - factors->h = node; - } - } else if (!lastTimeG) { - factors->g = node; - factors->h = one; - lastTimeG = 1; - value = 1; - if (st_insert(ghTable, (char *)Cudd_Regular(node), (char *)(long)value) == ST_OUT_OF_MEM) { - dd->errorCode = CUDD_MEMORY_OUT; - FREE(factors); - return NULL; - } - } else { - factors->g = one; - factors->h = node; - lastTimeG = 0; - value = 2; - if (st_insert(ghTable, (char *)Cudd_Regular(node), (char *)(long)value) == ST_OUT_OF_MEM) { - dd->errorCode = CUDD_MEMORY_OUT; - FREE(factors); - return NULL; - } - } - return(FactorsComplement(factors)); - } - - /* get the children and recur */ - Nv = cuddT(N); - Nnv = cuddE(N); - Nv = Cudd_NotCond(Nv, Cudd_IsComplement(node)); - Nnv = Cudd_NotCond(Nnv, Cudd_IsComplement(node)); - - /* Choose which subproblem to solve first based on the number of - * minterms. We go first where there are more minterms. - */ - if (!Cudd_IsConstant(Nv)) { - if (!st_lookup(mintermTable, (char *)Nv, (char **)&doubleDummy)) { - (void) fprintf(dd->err, "Not in table: Something wrong\n"); - dd->errorCode = CUDD_INTERNAL_ERROR; - return(NULL); - } - minNv = *doubleDummy; - } - - if (!Cudd_IsConstant(Nnv)) { - if (!st_lookup(mintermTable, (char *)Nnv, (char **)&doubleDummy)) { - (void) fprintf(dd->err, "Not in table: Something wrong\n"); - dd->errorCode = CUDD_INTERNAL_ERROR; - return(NULL); - } - minNnv = *doubleDummy; - } - - if (minNv < minNnv) { - temp = Nv; - Nv = Nnv; - Nnv = temp; - switched = 1; - } - - /* build gt, ht recursively */ - if (Nv != zero) { - factorsNv = BuildConjuncts(dd, Nv, distanceTable, - cacheTable, approxDistance, maxLocalRef, - ghTable, mintermTable); - if (factorsNv == NULL) return(NULL); - freeNv = FactorsNotStored(factorsNv); - factorsNv = (freeNv) ? FactorsUncomplement(factorsNv) : factorsNv; - cuddRef(factorsNv->g); - cuddRef(factorsNv->h); - - /* Deal with the zero case */ - if (Nnv == zero) { - /* is responsible for freeing factorsNv */ - factors = ZeroCase(dd, node, factorsNv, ghTable, - cacheTable, switched); - if (freeNv) FREE(factorsNv); - return(factors); - } - } - - /* build ge, he recursively */ - if (Nnv != zero) { - factorsNnv = BuildConjuncts(dd, Nnv, distanceTable, - cacheTable, approxDistance, maxLocalRef, - ghTable, mintermTable); - if (factorsNnv == NULL) { - Cudd_RecursiveDeref(dd, factorsNv->g); - Cudd_RecursiveDeref(dd, factorsNv->h); - if (freeNv) FREE(factorsNv); - return(NULL); - } - freeNnv = FactorsNotStored(factorsNnv); - factorsNnv = (freeNnv) ? FactorsUncomplement(factorsNnv) : factorsNnv; - cuddRef(factorsNnv->g); - cuddRef(factorsNnv->h); - - /* Deal with the zero case */ - if (Nv == zero) { - /* is responsible for freeing factorsNv */ - factors = ZeroCase(dd, node, factorsNnv, ghTable, - cacheTable, switched); - if (freeNnv) FREE(factorsNnv); - return(factors); - } - } - - /* construct the 2 pairs */ - /* g1 = x*gt + x'*ge; h1 = x*ht + x'*he; */ - /* g2 = x*gt + x'*he; h2 = x*ht + x'*ge */ - if (switched) { - factors = factorsNnv; - factorsNnv = factorsNv; - factorsNv = factors; - freeTemp = freeNv; - freeNv = freeNnv; - freeNnv = freeTemp; - } - - /* Build the factors for this node. */ - topid = N->index; - topv = dd->vars[topid]; - - g1 = cuddBddIteRecur(dd, topv, factorsNv->g, factorsNnv->g); - if (g1 == NULL) { - Cudd_RecursiveDeref(dd, factorsNv->g); - Cudd_RecursiveDeref(dd, factorsNv->h); - Cudd_RecursiveDeref(dd, factorsNnv->g); - Cudd_RecursiveDeref(dd, factorsNnv->h); - if (freeNv) FREE(factorsNv); - if (freeNnv) FREE(factorsNnv); - return(NULL); - } - - cuddRef(g1); - - h1 = cuddBddIteRecur(dd, topv, factorsNv->h, factorsNnv->h); - if (h1 == NULL) { - Cudd_RecursiveDeref(dd, factorsNv->g); - Cudd_RecursiveDeref(dd, factorsNv->h); - Cudd_RecursiveDeref(dd, factorsNnv->g); - Cudd_RecursiveDeref(dd, factorsNnv->h); - Cudd_RecursiveDeref(dd, g1); - if (freeNv) FREE(factorsNv); - if (freeNnv) FREE(factorsNnv); - return(NULL); - } - - cuddRef(h1); - - g2 = cuddBddIteRecur(dd, topv, factorsNv->g, factorsNnv->h); - if (g2 == NULL) { - Cudd_RecursiveDeref(dd, factorsNv->h); - Cudd_RecursiveDeref(dd, factorsNv->g); - Cudd_RecursiveDeref(dd, factorsNnv->g); - Cudd_RecursiveDeref(dd, factorsNnv->h); - Cudd_RecursiveDeref(dd, g1); - Cudd_RecursiveDeref(dd, h1); - if (freeNv) FREE(factorsNv); - if (freeNnv) FREE(factorsNnv); - return(NULL); - } - cuddRef(g2); - Cudd_RecursiveDeref(dd, factorsNv->g); - Cudd_RecursiveDeref(dd, factorsNnv->h); - - h2 = cuddBddIteRecur(dd, topv, factorsNv->h, factorsNnv->g); - if (h2 == NULL) { - Cudd_RecursiveDeref(dd, factorsNv->g); - Cudd_RecursiveDeref(dd, factorsNv->h); - Cudd_RecursiveDeref(dd, factorsNnv->g); - Cudd_RecursiveDeref(dd, factorsNnv->h); - Cudd_RecursiveDeref(dd, g1); - Cudd_RecursiveDeref(dd, h1); - Cudd_RecursiveDeref(dd, g2); - if (freeNv) FREE(factorsNv); - if (freeNnv) FREE(factorsNnv); - return(NULL); - } - cuddRef(h2); - Cudd_RecursiveDeref(dd, factorsNv->h); - Cudd_RecursiveDeref(dd, factorsNnv->g); - if (freeNv) FREE(factorsNv); - if (freeNnv) FREE(factorsNnv); - - /* check for each pair in tables and choose one */ - factors = CheckInTables(node, g1, h1, g2, h2, ghTable, cacheTable, &outOfMem); - if (outOfMem) { - dd->errorCode = CUDD_MEMORY_OUT; - Cudd_RecursiveDeref(dd, g1); - Cudd_RecursiveDeref(dd, h1); - Cudd_RecursiveDeref(dd, g2); - Cudd_RecursiveDeref(dd, h2); - return(NULL); - } - if (factors != NULL) { - if ((factors->g == g1) || (factors->g == h1)) { - Cudd_RecursiveDeref(dd, g2); - Cudd_RecursiveDeref(dd, h2); - } else { - Cudd_RecursiveDeref(dd, g1); - Cudd_RecursiveDeref(dd, h1); - } - return(factors); - } - - /* if not in tables, pick one pair */ - factors = PickOnePair(node,g1, h1, g2, h2, ghTable, cacheTable); - if (factors == NULL) { - dd->errorCode = CUDD_MEMORY_OUT; - Cudd_RecursiveDeref(dd, g1); - Cudd_RecursiveDeref(dd, h1); - Cudd_RecursiveDeref(dd, g2); - Cudd_RecursiveDeref(dd, h2); - } else { - /* now free what was created and not used */ - if ((factors->g == g1) || (factors->g == h1)) { - Cudd_RecursiveDeref(dd, g2); - Cudd_RecursiveDeref(dd, h2); - } else { - Cudd_RecursiveDeref(dd, g1); - Cudd_RecursiveDeref(dd, h1); - } - } - - return(factors); - -} /* end of BuildConjuncts */ - - -/**Function******************************************************************** - - Synopsis [Procedure to compute two conjunctive factors of f and place in *c1 and *c2.] - - Description [Procedure to compute two conjunctive factors of f and - place in *c1 and *c2. Sets up the required data - table of distances - from the constant and local reference count. Also minterm table. ] - - SideEffects [] - - SeeAlso [] - -******************************************************************************/ -static int -cuddConjunctsAux( - DdManager * dd, - DdNode * f, - DdNode ** c1, - DdNode ** c2) -{ - st_table *distanceTable = NULL; - st_table *cacheTable = NULL; - st_table *mintermTable = NULL; - st_table *ghTable = NULL; - st_generator *stGen; - char *key, *value; - Conjuncts *factors; - int distance, approxDistance; - double max, minterms; - int freeFactors; - NodeStat *nodeStat; - int maxLocalRef; - - /* initialize */ - *c1 = NULL; - *c2 = NULL; - - /* initialize distances table */ - distanceTable = st_init_table(st_ptrcmp,st_ptrhash); - if (distanceTable == NULL) goto outOfMem; - - /* make the entry for the constant */ - nodeStat = ALLOC(NodeStat, 1); - if (nodeStat == NULL) goto outOfMem; - nodeStat->distance = 0; - nodeStat->localRef = 1; - if (st_insert(distanceTable, (char *)one, (char *)nodeStat) == ST_OUT_OF_MEM) { - goto outOfMem; - } - - /* Count node distances from constant. */ - nodeStat = CreateBotDist(f, distanceTable); - if (nodeStat == NULL) goto outOfMem; - - /* set the distance for the decomposition points */ - approxDistance = (DEPTH < nodeStat->distance) ? nodeStat->distance : DEPTH; - distance = nodeStat->distance; - - if (distance < approxDistance) { - /* Too small to bother. */ - *c1 = f; - *c2 = DD_ONE(dd); - cuddRef(*c1); cuddRef(*c2); - stGen = st_init_gen(distanceTable); - if (stGen == NULL) goto outOfMem; - while(st_gen(stGen, (char **)&key, (char **)&value)) { - FREE(value); - } - st_free_gen(stGen); stGen = NULL; - st_free_table(distanceTable); - return(1); - } - - /* record the maximum local reference count */ - maxLocalRef = 0; - stGen = st_init_gen(distanceTable); - if (stGen == NULL) goto outOfMem; - while(st_gen(stGen, (char **)&key, (char **)&value)) { - nodeStat = (NodeStat *)value; - maxLocalRef = (nodeStat->localRef > maxLocalRef) ? - nodeStat->localRef : maxLocalRef; - } - st_free_gen(stGen); stGen = NULL; - - - /* Count minterms for each node. */ - max = pow(2.0, (double)Cudd_SupportSize(dd,f)); /* potential overflow */ - mintermTable = st_init_table(st_ptrcmp,st_ptrhash); - if (mintermTable == NULL) goto outOfMem; - minterms = CountMinterms(f, max, mintermTable, dd->err); - if (minterms == -1.0) goto outOfMem; - - lastTimeG = Cudd_Random() & 1; - cacheTable = st_init_table(st_ptrcmp, st_ptrhash); - if (cacheTable == NULL) goto outOfMem; - ghTable = st_init_table(st_ptrcmp, st_ptrhash); - if (ghTable == NULL) goto outOfMem; - - /* Build conjuncts. */ - factors = BuildConjuncts(dd, f, distanceTable, cacheTable, - approxDistance, maxLocalRef, ghTable, mintermTable); - if (factors == NULL) goto outOfMem; - - /* free up tables */ - stGen = st_init_gen(distanceTable); - if (stGen == NULL) goto outOfMem; - while(st_gen(stGen, (char **)&key, (char **)&value)) { - FREE(value); - } - st_free_gen(stGen); stGen = NULL; - st_free_table(distanceTable); distanceTable = NULL; - st_free_table(ghTable); ghTable = NULL; - - stGen = st_init_gen(mintermTable); - if (stGen == NULL) goto outOfMem; - while(st_gen(stGen, (char **)&key, (char **)&value)) { - FREE(value); - } - st_free_gen(stGen); stGen = NULL; - st_free_table(mintermTable); mintermTable = NULL; - - freeFactors = FactorsNotStored(factors); - factors = (freeFactors) ? FactorsUncomplement(factors) : factors; - if (factors != NULL) { - *c1 = factors->g; - *c2 = factors->h; - cuddRef(*c1); - cuddRef(*c2); - if (freeFactors) FREE(factors); - -#if 0 - if ((*c1 == f) && (!Cudd_IsConstant(f))) { - assert(*c2 == one); - } - if ((*c2 == f) && (!Cudd_IsConstant(f))) { - assert(*c1 == one); - } - - if ((*c1 != one) && (!Cudd_IsConstant(f))) { - assert(!Cudd_bddLeq(dd, *c2, *c1)); - } - if ((*c2 != one) && (!Cudd_IsConstant(f))) { - assert(!Cudd_bddLeq(dd, *c1, *c2)); - } -#endif - } - - stGen = st_init_gen(cacheTable); - if (stGen == NULL) goto outOfMem; - while(st_gen(stGen, (char **)&key, (char **)&value)) { - ConjunctsFree(dd, (Conjuncts *)value); - } - st_free_gen(stGen); stGen = NULL; - - st_free_table(cacheTable); cacheTable = NULL; - - return(1); - -outOfMem: - if (distanceTable != NULL) { - stGen = st_init_gen(distanceTable); - if (stGen == NULL) goto outOfMem; - while(st_gen(stGen, (char **)&key, (char **)&value)) { - FREE(value); - } - st_free_gen(stGen); stGen = NULL; - st_free_table(distanceTable); distanceTable = NULL; - } - if (mintermTable != NULL) { - stGen = st_init_gen(mintermTable); - if (stGen == NULL) goto outOfMem; - while(st_gen(stGen, (char **)&key, (char **)&value)) { - FREE(value); - } - st_free_gen(stGen); stGen = NULL; - st_free_table(mintermTable); mintermTable = NULL; - } - if (ghTable != NULL) st_free_table(ghTable); - if (cacheTable != NULL) { - stGen = st_init_gen(cacheTable); - if (stGen == NULL) goto outOfMem; - while(st_gen(stGen, (char **)&key, (char **)&value)) { - ConjunctsFree(dd, (Conjuncts *)value); - } - st_free_gen(stGen); stGen = NULL; - st_free_table(cacheTable); cacheTable = NULL; - } - dd->errorCode = CUDD_MEMORY_OUT; - return(0); - -} /* end of cuddConjunctsAux */ -- cgit v1.2.3