cudd  3.0.0
The University of Colorado Decision Diagram Package
Functions
cuddAndAbs.c File Reference

Combined AND and existential abstraction for BDDs. More...

#include "util.h"
#include "cuddInt.h"
Include dependency graph for cuddAndAbs.c:

Functions

DdNodeCudd_bddAndAbstract (DdManager *manager, DdNode *f, DdNode *g, DdNode *cube)
 Takes the AND of two BDDs and simultaneously abstracts the variables in cube. More...
 
DdNodeCudd_bddAndAbstractLimit (DdManager *manager, DdNode *f, DdNode *g, DdNode *cube, unsigned int limit)
 Takes the AND of two BDDs and simultaneously abstracts variables unless too many nodes are needed. More...
 
DdNodecuddBddAndAbstractRecur (DdManager *manager, DdNode *f, DdNode *g, DdNode *cube)
 Takes the AND of two BDDs and simultaneously abstracts the variables in cube. More...
 

Detailed Description

Combined AND and existential abstraction for BDDs.

Author
Fabio Somenzi

Function Documentation

◆ Cudd_bddAndAbstract()

DdNode* Cudd_bddAndAbstract ( DdManager manager,
DdNode f,
DdNode g,
DdNode cube 
)

Takes the AND of two BDDs and simultaneously abstracts the variables in cube.

The variables are existentially abstracted. Cudd_bddAndAbstract implements the semiring matrix multiplication algorithm for the boolean semiring.

Returns
a pointer to the result is successful; NULL otherwise.
Side effects None
See also
Cudd_addMatrixMultiply Cudd_addTriangle Cudd_bddAnd

◆ Cudd_bddAndAbstractLimit()

DdNode* Cudd_bddAndAbstractLimit ( DdManager manager,
DdNode f,
DdNode g,
DdNode cube,
unsigned int  limit 
)

Takes the AND of two BDDs and simultaneously abstracts variables unless too many nodes are needed.

The variables in cube are existentially abstracted.

Returns
a pointer to the result is successful; NULL otherwise. In particular, if the number of new nodes created exceeds limit, this function returns NULL.
Side effects None
See also
Cudd_bddAndAbstract

◆ cuddBddAndAbstractRecur()

DdNode* cuddBddAndAbstractRecur ( DdManager manager,
DdNode f,
DdNode g,
DdNode cube 
)

Takes the AND of two BDDs and simultaneously abstracts the variables in cube.

The variables are existentially abstracted.

Returns
a pointer to the result is successful; NULL otherwise.
Side effects None
See also
Cudd_bddAndAbstract