cudd
3.0.0
The University of Colorado Decision Diagram Package
|
BDD ITE function and satellites. More...
Functions | |
DdNode * | Cudd_bddIte (DdManager *dd, DdNode *f, DdNode *g, DdNode *h) |
Implements ITE(f,g,h). More... | |
DdNode * | Cudd_bddIteLimit (DdManager *dd, DdNode *f, DdNode *g, DdNode *h, unsigned int limit) |
Implements ITE(f,g,h) unless too many nodes are required. More... | |
DdNode * | Cudd_bddIteConstant (DdManager *dd, DdNode *f, DdNode *g, DdNode *h) |
Implements ITEconstant(f,g,h). More... | |
DdNode * | Cudd_bddIntersect (DdManager *dd, DdNode *f, DdNode *g) |
Returns a function included in the intersection of f and g. More... | |
DdNode * | Cudd_bddAnd (DdManager *dd, DdNode *f, DdNode *g) |
Computes the conjunction of two BDDs f and g. More... | |
DdNode * | Cudd_bddAndLimit (DdManager *dd, DdNode *f, DdNode *g, unsigned int limit) |
Computes the conjunction of two BDDs f and g unless too many nodes are required. More... | |
DdNode * | Cudd_bddOr (DdManager *dd, DdNode *f, DdNode *g) |
Computes the disjunction of two BDDs f and g. More... | |
DdNode * | Cudd_bddOrLimit (DdManager *dd, DdNode *f, DdNode *g, unsigned int limit) |
Computes the disjunction of two BDDs f and g unless too many nodes are required. More... | |
DdNode * | Cudd_bddNand (DdManager *dd, DdNode *f, DdNode *g) |
Computes the NAND of two BDDs f and g. More... | |
DdNode * | Cudd_bddNor (DdManager *dd, DdNode *f, DdNode *g) |
Computes the NOR of two BDDs f and g. More... | |
DdNode * | Cudd_bddXor (DdManager *dd, DdNode *f, DdNode *g) |
Computes the exclusive OR of two BDDs f and g. More... | |
DdNode * | Cudd_bddXnor (DdManager *dd, DdNode *f, DdNode *g) |
Computes the exclusive NOR of two BDDs f and g. More... | |
DdNode * | Cudd_bddXnorLimit (DdManager *dd, DdNode *f, DdNode *g, unsigned int limit) |
Computes the exclusive NOR of two BDDs f and g unless too many nodes are required. More... | |
int | Cudd_bddLeq (DdManager *dd, DdNode *f, DdNode *g) |
Checks whether f is less than or equal to g. More... | |
DdNode * | cuddBddIteRecur (DdManager *dd, DdNode *f, DdNode *g, DdNode *h) |
Implements the recursive step of Cudd_bddIte. More... | |
DdNode * | cuddBddIntersectRecur (DdManager *dd, DdNode *f, DdNode *g) |
Implements the recursive step of Cudd_bddIntersect. More... | |
DdNode * | cuddBddAndRecur (DdManager *manager, DdNode *f, DdNode *g) |
Implements the recursive step of Cudd_bddAnd. More... | |
DdNode * | cuddBddXorRecur (DdManager *manager, DdNode *f, DdNode *g) |
Implements the recursive step of Cudd_bddXor. More... | |
static void | bddVarToConst (DdNode *f, DdNode **gp, DdNode **hp, DdNode *one) |
Replaces variables with constants if possible. More... | |
static int | bddVarToCanonical (DdManager *dd, DdNode **fp, DdNode **gp, DdNode **hp, int *topfp, int *topgp, int *tophp) |
Picks unique member from equiv expressions. More... | |
static int | bddVarToCanonicalSimple (DdManager *dd, DdNode **fp, DdNode **gp, DdNode **hp, int *topfp, int *topgp, int *tophp) |
Picks unique member from equiv expressions. More... | |
BDD ITE function and satellites.
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 |
Picks unique member from equiv expressions.
Reduces 2 variable expressions to canonical form.
|
static |
Picks unique member from equiv expressions.
Makes sure the first two pointers are regular. This mat require the complementation of the result, which is signaled by returning 1 instead of 0. This function is simpler than the general case because it assumes that no two arguments are the same or complementary, and no argument is constant.
Replaces variables with constants if possible.
This function performs part of the transformation to standard form by replacing variables with constants if possible.
Computes the conjunction of two BDDs f and g.
dd | manager |
f | first operand |
g | second operand |
Computes the conjunction of two BDDs f and g unless too many nodes are required.
limit
are required.dd | manager |
f | first operand |
g | second operand |
limit | maximum number of new nodes |
Returns a function included in the intersection of f and g.
The function computed (if not zero) is a witness that the intersection is not empty. Cudd_bddIntersect tries to build as few new nodes as possible. If the only result of interest is whether f and g intersect, Cudd_bddLeq should be used instead.
dd | manager |
f | first operand |
g | second operand |
Implements ITE(f,g,h).
dd | manager |
f | first operand |
g | second operand |
h | third operand |
Implements ITEconstant(f,g,h).
No new nodes are created.
dd | manager |
f | first operand |
g | second operand |
h | thord operand |
Implements ITE(f,g,h) unless too many nodes are required.
limit
are required.dd | manager |
f | first operand |
g | second operand |
h | third operand |
limit | maximum number of new nodes |
Checks whether f is less than or equal to g.
No new nodes are created.
dd | manager |
f | first operand |
g | second operand |
Computes the NAND of two BDDs f and g.
dd | manager |
f | first operand |
g | second operand |
Computes the NOR of two BDDs f and g.
dd | manager |
f | first operand |
g | second operand |
Computes the disjunction of two BDDs f and g.
dd | manager |
f | first operand |
g | second operand |
Computes the disjunction of two BDDs f and g unless too many nodes are required.
limit
are required.dd | manager |
f | first operand |
g | second operand |
limit | maximum number of new nodes |
Computes the exclusive NOR of two BDDs f and g.
dd | manager |
f | first operand |
g | second operand |
Computes the exclusive NOR of two BDDs f and g unless too many nodes are required.
limit
are required.dd | manager |
f | first operand |
g | second operand |
limit | maximum number of new nodes |
Computes the exclusive OR of two BDDs f and g.
dd | manager |
f | first operand |
g | second operand |
Implements the recursive step of Cudd_bddAnd.
Takes the conjunction of two BDDs.
Implements the recursive step of Cudd_bddIte.
Implements the recursive step of Cudd_bddXor.
Takes the exclusive OR of two BDDs.