Functions for BDD decomposition. More...
#include "util.h"
#include "cuddInt.h"
Data Structures | |
struct | Conjuncts |
Type of a pair of conjoined BDDs. More... | |
struct | NodeStat |
Stats for one node. More... | |
Defines | |
#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 |
#define | FactorsNotStored(factors) ((int)((ptrint)(factors) & 01)) |
#define | FactorsComplement(factors) ((Conjuncts *)((ptrint)(factors) | 01)) |
#define | FactorsUncomplement(factors) ((Conjuncts *)((ptrint)(factors) ^ 01)) |
Functions | |
int | Cudd_bddApproxConjDecomp (DdManager *dd, DdNode *f, DdNode ***conjuncts) |
Performs two-way conjunctive decomposition of a BDD. | |
int | Cudd_bddApproxDisjDecomp (DdManager *dd, DdNode *f, DdNode ***disjuncts) |
Performs two-way disjunctive decomposition of a BDD. | |
int | Cudd_bddIterConjDecomp (DdManager *dd, DdNode *f, DdNode ***conjuncts) |
Performs two-way conjunctive decomposition of a BDD. | |
int | Cudd_bddIterDisjDecomp (DdManager *dd, DdNode *f, DdNode ***disjuncts) |
Performs two-way disjunctive decomposition of a BDD. | |
int | Cudd_bddGenConjDecomp (DdManager *dd, DdNode *f, DdNode ***conjuncts) |
Performs two-way conjunctive decomposition of a BDD. | |
int | Cudd_bddGenDisjDecomp (DdManager *dd, DdNode *f, DdNode ***disjuncts) |
Performs two-way disjunctive decomposition of a BDD. | |
int | Cudd_bddVarConjDecomp (DdManager *dd, DdNode *f, DdNode ***conjuncts) |
Performs two-way conjunctive decomposition of a BDD. | |
int | Cudd_bddVarDisjDecomp (DdManager *dd, DdNode *f, DdNode ***disjuncts) |
Performs two-way disjunctive decomposition of a BDD. | |
static NodeStat * | CreateBotDist (DdNode *node, st_table *distanceTable) |
Get longest distance of node from constant. | |
static double | CountMinterms (DdManager *dd, DdNode *node, double max, st_table *mintermTable, FILE *fp) |
Count the number of minterms of each node ina a BDD and store it in a hash table. | |
static void | ConjunctsFree (DdManager *dd, Conjuncts *factors) |
Free factors structure. | |
static int | PairInTables (DdNode *g, DdNode *h, st_table *ghTable) |
Check whether the given pair is in the tables. | |
static Conjuncts * | CheckTablesCacheAndReturn (DdManager *manager, DdNode *node, DdNode *g, DdNode *h, st_table *ghTable, st_table *cacheTable) |
Check the tables for the existence of pair and return one combination, cache the result. | |
static Conjuncts * | PickOnePair (DdManager *manager, DdNode *node, DdNode *g1, DdNode *h1, DdNode *g2, DdNode *h2, st_table *ghTable, st_table *cacheTable) |
Check the tables for the existence of pair and return one combination, store in cache. | |
static Conjuncts * | CheckInTables (DdManager *manager, DdNode *node, DdNode *g1, DdNode *h1, DdNode *g2, DdNode *h2, st_table *ghTable, st_table *cacheTable, int *outOfMem) |
Check if the two pairs exist in the table. | |
static Conjuncts * | ZeroCase (DdManager *dd, DdNode *node, Conjuncts *factorsNv, st_table *ghTable, st_table *cacheTable, int switched) |
If one child is zero, do explicitly what Restrict does or better. | |
static Conjuncts * | BuildConjuncts (DdManager *dd, DdNode *node, st_table *distanceTable, st_table *cacheTable, int approxDistance, int maxLocalRef, st_table *ghTable, st_table *mintermTable, int32_t *lastTimeG) |
Builds the conjuncts recursively, bottom up. | |
static int | cuddConjunctsAux (DdManager *dd, DdNode *f, DdNode **c1, DdNode **c2) |
Computes two conjunctive factors of f and places them in *c1 and *c2. |
Functions for BDD decomposition.
Copyright (c) 1995-2015, 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.
static Conjuncts* BuildConjuncts | ( | DdManager * | dd, | |
DdNode * | node, | |||
st_table * | distanceTable, | |||
st_table * | cacheTable, | |||
int | approxDistance, | |||
int | maxLocalRef, | |||
st_table * | ghTable, | |||
st_table * | mintermTable, | |||
int32_t * | lastTimeG | |||
) | [static] |
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 by 3.
static Conjuncts* CheckInTables | ( | DdManager * | manager, | |
DdNode * | node, | |||
DdNode * | g1, | |||
DdNode * | h1, | |||
DdNode * | g2, | |||
DdNode * | h2, | |||
st_table * | ghTable, | |||
st_table * | cacheTable, | |||
int * | outOfMem | |||
) | [static] |
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.
static Conjuncts* CheckTablesCacheAndReturn | ( | DdManager * | manager, | |
DdNode * | node, | |||
DdNode * | g, | |||
DdNode * | h, | |||
st_table * | ghTable, | |||
st_table * | cacheTable | |||
) | [static] |
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.
Free factors structure.
static double CountMinterms | ( | DdManager * | dd, | |
DdNode * | node, | |||
double | max, | |||
st_table * | mintermTable, | |||
FILE * | fp | |||
) | [static] |
Count the number of minterms of each node ina a BDD and store it in a hash table.
Get longest distance of node from constant.
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. The conjuncts produced by this procedure tend to be imbalanced.
dd | manager | |
f | function to be decomposed | |
conjuncts | address of the first factor |
Performs two-way disjunctive decomposition of a BDD.
The disjuncts produced by this procedure tend to be imbalanced.
dd | manager | |
f | function to be decomposed | |
disjuncts | address of the array of the disjuncts |
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. The conjuncts produced by this procedure tend to be balanced.
dd | manager | |
f | function to be decomposed | |
conjuncts | address of the array of conjuncts |
Performs two-way disjunctive decomposition of a BDD.
The disjuncts produced by this procedure tend to be balanced.
dd | manager | |
f | function to be decomposed | |
disjuncts | address of the array of the disjuncts |
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. The conjuncts produced by this procedure tend to be imbalanced.
dd | manager | |
f | function to be decomposed | |
conjuncts | address of the array of conjuncts |
Performs two-way disjunctive decomposition of a BDD.
The disjuncts produced by this procedure tend to be imbalanced.
dd | manager | |
f | function to be decomposed | |
disjuncts | address of the array of the disjuncts |
Performs two-way conjunctive decomposition of a BDD.
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.
dd | manager | |
f | function to be decomposed | |
conjuncts | address of the array of conjuncts |
Performs two-way disjunctive decomposition of a BDD.
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.
dd | manager | |
f | function to be decomposed | |
disjuncts | address of the array of the disjuncts |
Computes two conjunctive factors of f and places them in *c1 and *c2.
Sets up the required data - table of distances from the constant and local reference count. Also minterm table.
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;
static Conjuncts* PickOnePair | ( | DdManager * | manager, | |
DdNode * | node, | |||
DdNode * | g1, | |||
DdNode * | h1, | |||
DdNode * | g2, | |||
DdNode * | h2, | |||
st_table * | ghTable, | |||
st_table * | cacheTable | |||
) | [static] |
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.
static Conjuncts* ZeroCase | ( | DdManager * | dd, | |
DdNode * | node, | |||
Conjuncts * | factorsNv, | |||
st_table * | ghTable, | |||
st_table * | cacheTable, | |||
int | switched | |||
) | [static] |
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.