| /**CFile*********************************************************************** |
| |
| FileName [cuddDecomp.c] |
| |
| PackageName [cudd] |
| |
| Synopsis [Functions for BDD decomposition.] |
| |
| Description [External procedures included in this file: |
| <ul> |
| <li> Cudd_bddApproxConjDecomp() |
| <li> Cudd_bddApproxDisjDecomp() |
| <li> Cudd_bddIterConjDecomp() |
| <li> Cudd_bddIterDisjDecomp() |
| <li> Cudd_bddGenConjDecomp() |
| <li> Cudd_bddGenDisjDecomp() |
| <li> Cudd_bddVarConjDecomp() |
| <li> Cudd_bddVarDisjDecomp() |
| </ul> |
| Static procedures included in this module: |
| <ul> |
| <li> cuddConjunctsAux() |
| <li> CreateBotDist() |
| <li> BuildConjuncts() |
| <li> ConjunctsFree() |
| </ul>] |
| |
| Author [Kavita Ravi, Fabio Somenzi] |
| |
| Copyright [Copyright (c) 1995-2004, Regents of the University of Colorado |
| |
| All rights reserved. |
| |
| Redistribution and use in source and binary forms, with or without |
| modification, are permitted provided that the following conditions |
| are met: |
| |
| Redistributions of source code must retain the above copyright |
| notice, this list of conditions and the following disclaimer. |
| |
| Redistributions in binary form must reproduce the above copyright |
| notice, this list of conditions and the following disclaimer in the |
| documentation and/or other materials provided with the distribution. |
| |
| Neither the name of the University of Colorado nor the names of its |
| contributors may be used to endorse or promote products derived from |
| this software without specific prior written permission. |
| |
| THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS |
| "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT |
| LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS |
| FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE |
| COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, |
| INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, |
| BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; |
| LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER |
| CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT |
| LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN |
| ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE |
| POSSIBILITY OF SUCH DAMAGE.] |
| |
| ******************************************************************************/ |
| |
| #include "misc/util/util_hack.h" |
| #include "cuddInt.h" |
| |
| ABC_NAMESPACE_IMPL_START |
| |
| |
| |
| /*---------------------------------------------------------------------------*/ |
| /* 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.44 2004/08/13 18:04:47 fabio 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 (DdNode * node, st__table * distanceTable); |
| static double CountMinterms (DdNode * node, double max, st__table * mintermTable, FILE *fp); |
| static void ConjunctsFree (DdManager * dd, Conjuncts * factors); |
| static int PairInTables (DdNode * g, DdNode * h, st__table * ghTable); |
| static Conjuncts * CheckTablesCacheAndReturn (DdNode * node, DdNode * g, DdNode * h, st__table * ghTable, st__table * cacheTable); |
| static Conjuncts * PickOnePair (DdNode * node, DdNode * g1, DdNode * h1, DdNode * g2, DdNode * h2, st__table * ghTable, st__table * cacheTable); |
| static Conjuncts * CheckInTables (DdNode * node, DdNode * g1, DdNode * h1, DdNode * g2, DdNode * h2, st__table * ghTable, st__table * cacheTable, int * outOfMem); |
| static Conjuncts * ZeroCase (DdManager * dd, DdNode * node, Conjuncts * factorsNv, st__table * ghTable, st__table * cacheTable, int switched); |
| static Conjuncts * BuildConjuncts (DdManager * dd, DdNode * node, st__table * distanceTable, st__table * cacheTable, int approxDistance, int maxLocalRef, st__table * ghTable, st__table * mintermTable); |
| static int cuddConjunctsAux (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 = ABC_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 = ABC_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 = ABC_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 = ABC_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 = ABC_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 = ABC_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 = ABC_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 = ABC_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 = ABC_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 <code>f</code> is the function of the BDD and |
| <code>x</code> is the variable, the decomposition is |
| <code>(f+x)(f+x')</code>. 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 = ABC_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 = ABC_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 = ABC_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 = ABC_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 <code>f</code> is the function of the |
| BDD and <code>x</code> is the variable, the decomposition is |
| <code>f*x + f*x'</code>. 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, (const 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 = ABC_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, (const 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 = ABC_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); |
| ABC_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 = ABC_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) { |
| ABC_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 = ABC_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) { |
| ABC_FREE(factors); |
| return(NULL); |
| } |
| } |
| } else { |
| value = 1; |
| if ( st__insert(ghTable, (char *)Cudd_Regular(factors->g), |
| (char *)(long)value) == st__OUT_OF_MEM) { |
| ABC_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) { |
| ABC_FREE(factors); |
| return(NULL); |
| } |
| } |
| } else { |
| value = 2; |
| if ( st__insert(ghTable, (char *)Cudd_Regular(factors->h), |
| (char *)(long)value) == st__OUT_OF_MEM) { |
| ABC_FREE(factors); |
| return(NULL); |
| } |
| } |
| } |
| |
| /* Store factors in cache table for later use. */ |
| if ( st__insert(cacheTable, (char *)node, (char *)factors) == |
| st__OUT_OF_MEM) { |
| ABC_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 = ABC_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; |
| ABC_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; |
| ABC_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; |
| ABC_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; |
| ABC_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; |
| ABC_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; |
| ABC_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; |
| ABC_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; |
| ABC_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; |
| ABC_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; |
| ABC_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; |
| ABC_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; |
| ABC_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; |
| ABC_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 = ABC_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); |
| ABC_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 = ABC_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); |
| ABC_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 = NULL, *factorsNnv = NULL, *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 = ABC_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, (const 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, (const 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 = ABC_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; |
| ABC_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; |
| ABC_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, (const 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, (const 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) ABC_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) ABC_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) ABC_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) ABC_FREE(factorsNv); |
| if (freeNnv) ABC_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) ABC_FREE(factorsNv); |
| if (freeNnv) ABC_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) ABC_FREE(factorsNv); |
| if (freeNnv) ABC_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) ABC_FREE(factorsNv); |
| if (freeNnv) ABC_FREE(factorsNnv); |
| return(NULL); |
| } |
| cuddRef(h2); |
| Cudd_RecursiveDeref(dd, factorsNv->h); |
| Cudd_RecursiveDeref(dd, factorsNnv->g); |
| if (freeNv) ABC_FREE(factorsNv); |
| if (freeNnv) ABC_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 = ABC_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, (const char **)&key, (char **)&value)) { |
| ABC_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, (const 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, (const char **)&key, (char **)&value)) { |
| ABC_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, (const char **)&key, (char **)&value)) { |
| ABC_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) ABC_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, (const 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, (const char **)&key, (char **)&value)) { |
| ABC_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, (const char **)&key, (char **)&value)) { |
| ABC_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, (const 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 */ |
| |
| |
| ABC_NAMESPACE_IMPL_END |
| |
