cudd/cuddGenCof.c File Reference

Generalized cofactors for BDDs and ADDs. More...

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

Data Structures

struct  MarkCacheKey

Defines

#define DD_LIC_DC   0
#define DD_LIC_1   1
#define DD_LIC_0   2
#define DD_LIC_NL   3

Functions

DdNodeCudd_bddConstrain (DdManager *dd, DdNode *f, DdNode *c)
 Computes f constrain c.
DdNodeCudd_bddRestrict (DdManager *dd, DdNode *f, DdNode *c)
 BDD restrict according to Coudert and Madre's algorithm (ICCAD90).
DdNodeCudd_bddNPAnd (DdManager *dd, DdNode *f, DdNode *g)
 Computes f non-polluting-and g.
DdNodeCudd_addConstrain (DdManager *dd, DdNode *f, DdNode *c)
 Computes f constrain c for ADDs.
DdNode ** Cudd_bddConstrainDecomp (DdManager *dd, DdNode *f)
 BDD conjunctive decomposition as in McMillan's CAV96 paper.
DdNodeCudd_addRestrict (DdManager *dd, DdNode *f, DdNode *c)
 ADD restrict according to Coudert and Madre's algorithm (ICCAD90).
DdNode ** Cudd_bddCharToVect (DdManager *dd, DdNode *f)
 Computes a vector of BDDs whose image equals a non-zero function.
DdNodeCudd_bddLICompaction (DdManager *dd, DdNode *f, DdNode *c)
 Performs safe minimization of a BDD.
DdNodeCudd_bddSqueeze (DdManager *dd, DdNode *l, DdNode *u)
 Finds a small BDD in a function interval.
DdNodeCudd_bddInterpolate (DdManager *dd, DdNode *l, DdNode *u)
 Finds an interpolant of two functions.
DdNodeCudd_bddMinimize (DdManager *dd, DdNode *f, DdNode *c)
 Finds a small BDD that agrees with `f` over `c`.
DdNodeCudd_SubsetCompress (DdManager *dd, DdNode *f, int nvars, int threshold)
 Find a dense subset of BDD `f`.
DdNodeCudd_SupersetCompress (DdManager *dd, DdNode *f, int nvars, int threshold)
 Find a dense superset of BDD `f`.
DdNodecuddBddConstrainRecur (DdManager *dd, DdNode *f, DdNode *c)
 Performs the recursive step of Cudd_bddConstrain.
DdNodecuddBddRestrictRecur (DdManager *dd, DdNode *f, DdNode *c)
 Performs the recursive step of Cudd_bddRestrict.
DdNodecuddBddNPAndRecur (DdManager *manager, DdNode *f, DdNode *g)
 Implements the recursive step of Cudd_bddAnd.
DdNodecuddAddConstrainRecur (DdManager *dd, DdNode *f, DdNode *c)
 Performs the recursive step of Cudd_addConstrain.
DdNodecuddAddRestrictRecur (DdManager *dd, DdNode *f, DdNode *c)
 Performs the recursive step of Cudd_addRestrict.
DdNodecuddBddLICompaction (DdManager *dd, DdNode *f, DdNode *c)
 Performs safe minimization of a BDD.
static int cuddBddConstrainDecomp (DdManager *dd, DdNode *f, DdNode **decomp)
 Performs the recursive step of Cudd_bddConstrainDecomp.
static DdNodecuddBddCharToVect (DdManager *dd, DdNode *f, DdNode *x)
 Performs the recursive step of Cudd_bddCharToVect.
static int cuddBddLICMarkEdges (DdManager *dd, DdNode *f, DdNode *c, st_table *table, st_table *cache)
 Performs the edge marking step of Cudd_bddLICompaction.
static DdNodecuddBddLICBuildResult (DdManager *dd, DdNode *f, st_table *cache, st_table *table)
 Builds the result of Cudd_bddLICompaction.
static int MarkCacheHash (void const *ptr, int modulus)
 Hash function for the computed table of cuddBddLICMarkEdges.
static int MarkCacheCompare (const void *ptr1, const void *ptr2)
 Comparison function for the computed table of cuddBddLICMarkEdges.
static enum st_retval MarkCacheCleanUp (void *key, void *value, void *arg)
 Frees memory associated with computed table of cuddBddLICMarkEdges.
static DdNodecuddBddSqueeze (DdManager *dd, DdNode *l, DdNode *u)
 Performs the recursive step of Cudd_bddSqueeze.
static DdNodecuddBddInterpolate (DdManager *dd, DdNode *l, DdNode *u)
 Performs the recursive step of Cudd_bddInterpolate.

Detailed Description

Generalized cofactors for BDDs and ADDs.

Author:
Fabio Somenzi

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.


Function Documentation

DdNode* Cudd_addConstrain ( DdManager dd,
DdNode f,
DdNode c 
)

Computes f constrain c for ADDs.

Computes f constrain c (f @ c), for f an ADD and c a 0-1 ADD. List of special cases:

  • F @ 0 = 0
  • F @ 1 = F
  • 0 @ c = 0
  • 1 @ c = 1
  • F @ F = 1
Returns:
a pointer to the result if successful; NULL otherwise.
Side effects
None
See also:
Cudd_bddConstrain
DdNode* Cudd_addRestrict ( DdManager dd,
DdNode f,
DdNode c 
)

ADD restrict according to Coudert and Madre's algorithm (ICCAD90).

If application of restrict results in an ADD larger than the input ADD, the input ADD is returned.

Returns:
the restricted ADD if successful; otherwise NULL.
Side effects
None
See also:
Cudd_addConstrain Cudd_bddRestrict
DdNode** Cudd_bddCharToVect ( DdManager dd,
DdNode f 
)

Computes a vector of BDDs whose image equals a non-zero function.

The result depends on the variable order. The i-th component of the vector depends only on the first i variables in the order. Each BDD in the vector is not larger than the BDD of the given characteristic function. This function is based on the description of char-to-vect in "Verification of Sequential Machines Using Boolean Functional Vectors" by O. Coudert, C. Berthet and J. C. Madre.

Returns:
a pointer to an array containing the result if successful; NULL otherwise. The size of the array equals the number of variables in the manager. The components of the solution have their reference counts already incremented (unlike the results of most other functions in the package).
Side effects
None
See also:
Cudd_bddConstrain
DdNode* Cudd_bddConstrain ( DdManager dd,
DdNode f,
DdNode c 
)

Computes f constrain c.

Computes f constrain c (f @ c). Uses a canonical form: (f' @ c) = (f @ c)'. (Note: this is not true for c.) List of special cases:

  • f @ 0 = 0
  • f @ 1 = f
  • 0 @ c = 0
  • 1 @ c = 1
  • f @ f = 1
  • f @ f'= 0

Note that if F=(f1,...,fn) and reordering takes place while computing F @ c, then the image restriction property (Img(F,c) = Img(F @ c)) is lost.

Returns:
a pointer to the result if successful; NULL otherwise.
Side effects
None
See also:
Cudd_bddRestrict Cudd_addConstrain
DdNode** Cudd_bddConstrainDecomp ( DdManager dd,
DdNode f 
)

BDD conjunctive decomposition as in McMillan's CAV96 paper.

The decomposition is canonical only for a given variable order. If canonicity is required, variable ordering must be disabled after the decomposition has been computed. The components of the solution have their reference counts already incremented (unlike the results of most other functions in the package).

Returns:
an array with one entry for each BDD variable in the manager if successful; otherwise NULL.
Side effects
None
See also:
Cudd_bddConstrain Cudd_bddExistAbstract
DdNode* Cudd_bddInterpolate ( DdManager dd,
DdNode l,
DdNode u 
)

Finds an interpolant of two functions.

Given BDDs `l` and `u`, representing the lower bound and upper bound of a function interval, Cudd_bddInterpolate produces the BDD of a function within the interval that only depends on the variables common to `l` and `u`.

The approach is based on quantification as in Cudd_bddRestrict(). The function assumes that `l` implies `u`, but does not check whether that's true.

Returns:
a pointer to the result if successful; NULL otherwise.
Side effects
None
See also:
Cudd_bddRestrict Cudd_bddSqueeze
Parameters:
dd manager
l lower bound
u upper bound
DdNode* Cudd_bddLICompaction ( DdManager dd,
DdNode f,
DdNode c 
)

Performs safe minimization of a BDD.

Given the BDD `f` of a function to be minimized and a BDD `c` representing the care set, Cudd_bddLICompaction produces the BDD of a function that agrees with `f` wherever `c` is 1. Safe minimization means that the size of the result is guaranteed not to exceed the size of `f`. This function is based on the DAC97 paper by Hong et al..

Returns:
a pointer to the result if successful; NULL otherwise.
Side effects
None
See also:
Cudd_bddRestrict
Parameters:
dd manager
f function to be minimized
c constraint (care set)
DdNode* Cudd_bddMinimize ( DdManager dd,
DdNode f,
DdNode c 
)

Finds a small BDD that agrees with `f` over `c`.

Returns:
a pointer to the result if successful; NULL otherwise.
Side effects
None
See also:
Cudd_bddRestrict Cudd_bddLICompaction Cudd_bddSqueeze
DdNode* Cudd_bddNPAnd ( DdManager dd,
DdNode f,
DdNode g 
)

Computes f non-polluting-and g.

The non-polluting AND of f and g is a hybrid of AND and Restrict. From Restrict, this operation takes the idea of existentially quantifying the top variable of the second operand if it does not appear in the first. Therefore, the variables that appear in the result also appear in f. For the rest, the function behaves like AND. Since the two operands play different roles, non-polluting AND is not commutative.

Returns:
a pointer to the result if successful; NULL otherwise.
Side effects
None
See also:
Cudd_bddConstrain Cudd_bddRestrict
DdNode* Cudd_bddRestrict ( DdManager dd,
DdNode f,
DdNode c 
)

BDD restrict according to Coudert and Madre's algorithm (ICCAD90).

If application of restrict results in a BDD larger than the input BDD, the input BDD is returned.

Returns:
the restricted BDD if successful; otherwise NULL.
Side effects
None
See also:
Cudd_bddConstrain Cudd_addRestrict
DdNode* Cudd_bddSqueeze ( DdManager dd,
DdNode l,
DdNode u 
)

Finds a small BDD in a function interval.

Given BDDs `l` and `u`, representing the lower bound and upper bound of a function interval, Cudd_bddSqueeze produces the BDD of a function within the interval with a small BDD.

Returns:
a pointer to the result if successful; NULL otherwise.
Side effects
None
See also:
Cudd_bddRestrict Cudd_bddLICompaction
Parameters:
dd manager
l lower bound
u upper bound
DdNode* Cudd_SubsetCompress ( DdManager dd,
DdNode f,
int  nvars,
int  threshold 
)

Find a dense subset of BDD `f`.

Density is the ratio of number of minterms to number of nodes. Uses several techniques in series. It is more expensive than other subsetting procedures, but often produces better results. See Cudd_SubsetShortPaths for a description of the threshold and nvars parameters.

Returns:
a pointer to the result if successful; NULL otherwise.
Side effects
None
See also:
Cudd_RemapUnderApprox Cudd_SubsetShortPaths Cudd_SubsetHeavyBranch Cudd_bddSqueeze
Parameters:
dd manager
f BDD whose subset is sought
nvars number of variables in the support of f
threshold maximum number of nodes in the subset
DdNode* Cudd_SupersetCompress ( DdManager dd,
DdNode f,
int  nvars,
int  threshold 
)

Find a dense superset of BDD `f`.

Density is the ratio of number of minterms to number of nodes. Uses several techniques in series. It is more expensive than other supersetting procedures, but often produces better results. See Cudd_SupersetShortPaths for a description of the threshold and nvars parameters.

Returns:
a pointer to the result if successful; NULL otherwise.
Side effects
None
See also:
Cudd_SubsetCompress Cudd_SupersetRemap Cudd_SupersetShortPaths Cudd_SupersetHeavyBranch Cudd_bddSqueeze
Parameters:
dd manager
f BDD whose superset is sought
nvars number of variables in the support of f
threshold maximum number of nodes in the superset
DdNode* cuddAddConstrainRecur ( DdManager dd,
DdNode f,
DdNode c 
)

Performs the recursive step of Cudd_addConstrain.

Returns:
a pointer to the result if successful; NULL otherwise.
Side effects
None
See also:
Cudd_addConstrain
DdNode* cuddAddRestrictRecur ( DdManager dd,
DdNode f,
DdNode c 
)

Performs the recursive step of Cudd_addRestrict.

Returns:
the restricted ADD if successful; otherwise NULL.
Side effects
None
See also:
Cudd_addRestrict
static DdNode* cuddBddCharToVect ( DdManager dd,
DdNode f,
DdNode x 
) [static]

Performs the recursive step of Cudd_bddCharToVect.

This function maintains the invariant that f is non-zero.

Returns:
the i-th component of the vector if successful; otherwise NULL.
Side effects
None
See also:
Cudd_bddCharToVect
static int cuddBddConstrainDecomp ( DdManager dd,
DdNode f,
DdNode **  decomp 
) [static]

Performs the recursive step of Cudd_bddConstrainDecomp.

Returns:
f super (i) if successful; otherwise NULL.
Side effects
None
See also:
Cudd_bddConstrainDecomp
DdNode* cuddBddConstrainRecur ( DdManager dd,
DdNode f,
DdNode c 
)

Performs the recursive step of Cudd_bddConstrain.

Returns:
a pointer to the result if successful; NULL otherwise.
Side effects
None
See also:
Cudd_bddConstrain
static DdNode* cuddBddInterpolate ( DdManager dd,
DdNode l,
DdNode u 
) [static]

Performs the recursive step of Cudd_bddInterpolate.

This procedure exploits the fact that if we complement and swap the bounds of the interval we obtain a valid solution by taking the complement of the solution to the original problem. Therefore, we can enforce the condition that the upper bound is always regular.

Returns:
a pointer to the result if successful; NULL otherwise.
Side effects
None
See also:
Cudd_bddInterpolate
static DdNode* cuddBddLICBuildResult ( DdManager dd,
DdNode f,
st_table cache,
st_table table 
) [static]

Builds the result of Cudd_bddLICompaction.

Returns:
a pointer to the minimized BDD if successful; otherwise NULL.
Side effects
None
See also:
Cudd_bddLICompaction cuddBddLICMarkEdges
static int cuddBddLICMarkEdges ( DdManager dd,
DdNode f,
DdNode c,
st_table table,
st_table cache 
) [static]

Performs the edge marking step of Cudd_bddLICompaction.

Returns:
the LUB of the markings of the two outgoing edges of f if successful; otherwise CUDD_OUT_OF_MEM.
Side effects
None
See also:
Cudd_bddLICompaction cuddBddLICBuildResult
DdNode* cuddBddLICompaction ( DdManager dd,
DdNode f,
DdNode c 
)

Performs safe minimization of a BDD.

Given the BDD `f` of a function to be minimized and a BDD `c` representing the care set, Cudd_bddLICompaction produces the BDD of a function that agrees with `f` wherever `c` is 1. Safe minimization means that the size of the result is guaranteed not to exceed the size of `f`. This function is based on the DAC97 paper by Hong et al..

Returns:
a pointer to the result if successful; NULL otherwise.
Side effects
None
See also:
Cudd_bddLICompaction
Parameters:
dd manager
f function to be minimized
c constraint (care set)
DdNode* cuddBddNPAndRecur ( DdManager manager,
DdNode f,
DdNode g 
)

Implements the recursive step of Cudd_bddAnd.

Returns:
a pointer to the result is successful; NULL otherwise.
Side effects
None
See also:
Cudd_bddNPAnd
DdNode* cuddBddRestrictRecur ( DdManager dd,
DdNode f,
DdNode c 
)

Performs the recursive step of Cudd_bddRestrict.

Returns:
the restricted BDD if successful; otherwise NULL.
Side effects
None
See also:
Cudd_bddRestrict
static DdNode* cuddBddSqueeze ( DdManager dd,
DdNode l,
DdNode u 
) [static]

Performs the recursive step of Cudd_bddSqueeze.

This procedure exploits the fact that if we complement and swap the bounds of the interval we obtain a valid solution by taking the complement of the solution to the original problem. Therefore, we can enforce the condition that the upper bound is always regular.

Returns:
a pointer to the result if successful; NULL otherwise.
Side effects
None
See also:
Cudd_bddSqueeze
static enum st_retval MarkCacheCleanUp ( void *  key,
void *  value,
void *  arg 
) [static]

Frees memory associated with computed table of cuddBddLICMarkEdges.

Returns:
ST_CONTINUE.
Side effects
None
See also:
Cudd_bddLICompaction
static int MarkCacheCompare ( const void *  ptr1,
const void *  ptr2 
) [static]

Comparison function for the computed table of cuddBddLICMarkEdges.

Returns:
0 if the two nodes of the key are equal; 1 otherwise.
Side effects
None
See also:
Cudd_bddLICompaction
static int MarkCacheHash ( void const *  ptr,
int  modulus 
) [static]

Hash function for the computed table of cuddBddLICMarkEdges.

Returns:
the bucket number.
Side effects
None
See also:
Cudd_bddLICompaction
 All Data Structures Files Functions Variables Typedefs Enumerations Defines

Generated on 31 Dec 2015 for cudd by  doxygen 1.6.1