cudd/cuddApprox.c File Reference

Procedures to approximate a given BDD. More...

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

Data Structures

struct  NodeData
 Data structure to store the information on each node. More...
struct  ApproxInfo
 Main bookkeeping data structure for approximation algorithms. More...
struct  GlobalQueueItem
 Item of the queue used in the levelized traversal of the BDD. More...
struct  LocalQueueItem
 Type of the item of the local queue. More...

Defines

#define DBL_MAX_EXP   1024
#define NOTHING   0
#define REPLACE_T   1
#define REPLACE_E   2
#define REPLACE_N   3
#define REPLACE_TT   4
#define REPLACE_TE   5
#define DONT_CARE   0
#define CARE   1
#define TOTAL_CARE   2
#define CARE_ERROR   3

Functions

DdNodeCudd_UnderApprox (DdManager *dd, DdNode *f, int numVars, int threshold, int safe, double quality)
 Extracts a dense subset from a BDD with Shiple's underapproximation method.
DdNodeCudd_OverApprox (DdManager *dd, DdNode *f, int numVars, int threshold, int safe, double quality)
 Extracts a dense superset from a BDD with Shiple's underapproximation method.
DdNodeCudd_RemapUnderApprox (DdManager *dd, DdNode *f, int numVars, int threshold, double quality)
 Extracts a dense subset from a BDD with the remapping underapproximation method.
DdNodeCudd_RemapOverApprox (DdManager *dd, DdNode *f, int numVars, int threshold, double quality)
 Extracts a dense superset from a BDD with the remapping underapproximation method.
DdNodeCudd_BiasedUnderApprox (DdManager *dd, DdNode *f, DdNode *b, int numVars, int threshold, double quality1, double quality0)
 Extracts a dense subset from a BDD with the biased underapproximation method.
DdNodeCudd_BiasedOverApprox (DdManager *dd, DdNode *f, DdNode *b, int numVars, int threshold, double quality1, double quality0)
 Extracts a dense superset from a BDD with the biased underapproximation method.
DdNodecuddUnderApprox (DdManager *dd, DdNode *f, int numVars, int threshold, int safe, double quality)
 Applies Tom Shiple's underappoximation algorithm.
DdNodecuddRemapUnderApprox (DdManager *dd, DdNode *f, int numVars, int threshold, double quality)
 Applies the remapping underappoximation algorithm.
DdNodecuddBiasedUnderApprox (DdManager *dd, DdNode *f, DdNode *b, int numVars, int threshold, double quality1, double quality0)
 Applies the biased remapping underappoximation algorithm.
static void updateParity (DdNode *node, ApproxInfo *info, int newparity)
 Recursively update the parity of the paths reaching a node.
static NodeDatagatherInfoAux (DdNode *node, ApproxInfo *info, int parity)
 Recursively counts minterms and computes reference counts of each node in the BDD.
static ApproxInfogatherInfo (DdManager *dd, DdNode *node, int numVars, int parity)
 Gathers information about each node.
static int computeSavings (DdManager *dd, DdNode *f, DdNode *skip, ApproxInfo *info, DdLevelQueue *queue)
 Counts the nodes that would be eliminated if a given node were replaced by zero.
static int updateRefs (DdManager *dd, DdNode *f, DdNode *skip, ApproxInfo *info, DdLevelQueue *queue)
 Update function reference counts to account for replacement.
static int UAmarkNodes (DdManager *dd, DdNode *f, ApproxInfo *info, int threshold, int safe, double quality)
 Marks nodes for replacement by zero.
static DdNodeUAbuildSubset (DdManager *dd, DdNode *node, ApproxInfo *info)
 Builds the subset BDD.
static int RAmarkNodes (DdManager *dd, DdNode *f, ApproxInfo *info, int threshold, double quality)
 Marks nodes for remapping.
static int BAmarkNodes (DdManager *dd, DdNode *f, ApproxInfo *info, int threshold, double quality1, double quality0)
 Marks nodes for remapping.
static DdNodeRAbuildSubset (DdManager *dd, DdNode *node, ApproxInfo *info)
 Builds the subset BDD for cuddRemapUnderApprox.
static int BAapplyBias (DdManager *dd, DdNode *f, DdNode *b, ApproxInfo *info, DdHashTable *cache)
 Finds don't care nodes by traversing f and b in parallel.

Detailed Description

Procedures to approximate a given BDD.

See also:
cuddSubsetHB.c cuddSubsetSP.c cuddGenCof.c
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

static int BAapplyBias ( DdManager dd,
DdNode f,
DdNode b,
ApproxInfo info,
DdHashTable cache 
) [static]

Finds don't care nodes by traversing f and b in parallel.

Returns:
the care status of the visited f node if successful; CARE_ERROR otherwise.
Side effects
None
See also:
cuddBiasedUnderApprox
static int BAmarkNodes ( DdManager dd,
DdNode f,
ApproxInfo info,
int  threshold,
double  quality1,
double  quality0 
) [static]

Marks nodes for remapping.

Returns:
1 if successful; 0 otherwise.
Side effects
None
See also:
cuddBiasedUnderApprox
Parameters:
dd manager
f function to be analyzed
info info on BDD
threshold when to stop approximating
quality1 minimum improvement for accepted changes when b=1
quality0 minimum improvement for accepted changes when b=0
static int computeSavings ( DdManager dd,
DdNode f,
DdNode skip,
ApproxInfo info,
DdLevelQueue queue 
) [static]

Counts the nodes that would be eliminated if a given node were replaced by zero.

This procedure uses a queue passed by the caller for efficiency: since the queue is left empty at the endof the search, it can be reused as is by the next search.

Returns:
the count (always striclty positive) if successful; 0 otherwise.
Side effects
None
See also:
UAmarkNodes RAmarkNodes BAmarkNodes
DdNode* Cudd_BiasedOverApprox ( DdManager dd,
DdNode f,
DdNode b,
int  numVars,
int  threshold,
double  quality1,
double  quality0 
)

Extracts a dense superset from a BDD with the biased underapproximation method.

The procedure is identical to the underapproximation procedure except for the fact that it works on the complement of the given function. Extracting the subset of the complement function is equivalent to extracting the superset of the function. The parameter numVars is the maximum number of variables to be used in minterm calculation. The optimal number should be as close as possible to the size of the support of f. However, it is safe to pass the value returned by Cudd_ReadSize for numVars when the number of variables is under 1023. If numVars is larger than 1023, it will overflow. If a 0 parameter is passed then the procedure will compute a value which will avoid overflow but will cause underflow with 2046 variables or more.

Returns:
a pointer to the BDD of the superset if successful. NULL if intermediate result causes the procedure to run out of memory.
Side effects
None
See also:
Cudd_SupersetHeavyBranch Cudd_SupersetShortPaths Cudd_RemapOverApprox Cudd_BiasedUnderApprox Cudd_ReadSize
Parameters:
dd manager
f function to be superset
b bias function
numVars number of variables in the support of f
threshold when to stop approximation
quality1 minimum improvement for accepted changes when b=1
quality0 minimum improvement for accepted changes when b=0
DdNode* Cudd_BiasedUnderApprox ( DdManager dd,
DdNode f,
DdNode b,
int  numVars,
int  threshold,
double  quality1,
double  quality0 
)

Extracts a dense subset from a BDD with the biased underapproximation method.

This procedure uses a biased remapping technique and density as the cost function. The bias is a function. This procedure tries to approximate where the bias is 0 and preserve the given function where the bias is 1. The parameter numVars is the maximum number of variables to be used in minterm calculation. The optimal number should be as close as possible to the size of the support of f. However, it is safe to pass the value returned by Cudd_ReadSize for numVars when the number of variables is under 1023. If numVars is larger than 1023, it will cause overflow. If a 0 parameter is passed then the procedure will compute a value which will avoid overflow but will cause underflow with 2046 variables or more.

Returns:
a pointer to the BDD of the subset if successful. NULL if the procedure runs out of memory.
Side effects
None
See also:
Cudd_SubsetShortPaths Cudd_SubsetHeavyBranch Cudd_UnderApprox Cudd_RemapUnderApprox Cudd_ReadSize
Parameters:
dd manager
f function to be subset
b bias function
numVars number of variables in the support of f
threshold when to stop approximation
quality1 minimum improvement for accepted changes when b=1
quality0 minimum improvement for accepted changes when b=0
DdNode* Cudd_OverApprox ( DdManager dd,
DdNode f,
int  numVars,
int  threshold,
int  safe,
double  quality 
)

Extracts a dense superset from a BDD with Shiple's underapproximation method.

The procedure is identical to the underapproximation procedure except for the fact that it works on the complement of the given function. Extracting the subset of the complement function is equivalent to extracting the superset of the function. The parameter numVars is the maximum number of variables to be used in minterm calculation. The optimal number should be as close as possible to the size of the support of f. However, it is safe to pass the value returned by Cudd_ReadSize for numVars when the number of variables is under 1023. If numVars is larger than 1023, it will overflow. If a 0 parameter is passed then the procedure will compute a value which will avoid overflow but will cause underflow with 2046 variables or more.

Returns:
a pointer to the BDD of the superset if successful. NULL if intermediate result causes the procedure to run out of memory.
Side effects
None
See also:
Cudd_SupersetHeavyBranch Cudd_SupersetShortPaths Cudd_ReadSize
Parameters:
dd manager
f function to be superset
numVars number of variables in the support of f
threshold when to stop approximation
safe enforce safe approximation
quality minimum improvement for accepted changes
DdNode* Cudd_RemapOverApprox ( DdManager dd,
DdNode f,
int  numVars,
int  threshold,
double  quality 
)

Extracts a dense superset from a BDD with the remapping underapproximation method.

The procedure is identical to the underapproximation procedure except for the fact that it works on the complement of the given function. Extracting the subset of the complement function is equivalent to extracting the superset of the function. The parameter numVars is the maximum number of variables to be used in minterm calculation. The optimal number should be as close as possible to the size of the support of f. However, it is safe to pass the value returned by Cudd_ReadSize for numVars when the number of variables is under 1023. If numVars is larger than 1023, it will overflow. If a 0 parameter is passed then the procedure will compute a value which will avoid overflow but will cause underflow with 2046 variables or more.

Returns:
a pointer to the BDD of the superset if successful. NULL if intermediate result causes the procedure to run out of memory.
Side effects
None
See also:
Cudd_SupersetHeavyBranch Cudd_SupersetShortPaths Cudd_ReadSize
Parameters:
dd manager
f function to be superset
numVars number of variables in the support of f
threshold when to stop approximation
quality minimum improvement for accepted changes
DdNode* Cudd_RemapUnderApprox ( DdManager dd,
DdNode f,
int  numVars,
int  threshold,
double  quality 
)

Extracts a dense subset from a BDD with the remapping underapproximation method.

This procedure uses a remapping technique and density as the cost function. The parameter numVars is the maximum number of variables to be used in minterm calculation. The optimal number should be as close as possible to the size of the support of f. However, it is safe to pass the value returned by Cudd_ReadSize for numVars when the number of variables is under 1023. If numVars is larger than 1023, it will cause overflow. If a 0 parameter is passed then the procedure will compute a value which will avoid overflow but will cause underflow with 2046 variables or more.

Returns:
a pointer to the BDD of the subset if successful. NULL if the procedure runs out of memory.
Side effects
None
See also:
Cudd_SubsetShortPaths Cudd_SubsetHeavyBranch Cudd_UnderApprox Cudd_ReadSize
Parameters:
dd manager
f function to be subset
numVars number of variables in the support of f
threshold when to stop approximation
quality minimum improvement for accepted changes
DdNode* Cudd_UnderApprox ( DdManager dd,
DdNode f,
int  numVars,
int  threshold,
int  safe,
double  quality 
)

Extracts a dense subset from a BDD with Shiple's underapproximation method.

This procedure uses a variant of Tom Shiple's underapproximation method. The main difference from the original method is that density is used as cost function. The parameter numVars is the maximum number of variables to be used in minterm calculation. The optimal number should be as close as possible to the size of the support of f. However, it is safe to pass the value returned by Cudd_ReadSize for numVars when the number of variables is under 1023. If numVars is larger than 1023, it will cause overflow. If a 0 parameter is passed then the procedure will compute a value which will avoid overflow but will cause underflow with 2046 variables or more.

Returns:
a pointer to the BDD of the subset if successful; NULL if the procedure runs out of memory.
Side effects
None
See also:
Cudd_SubsetShortPaths Cudd_SubsetHeavyBranch Cudd_ReadSize
Parameters:
dd manager
f function to be subset
numVars number of variables in the support of f
threshold when to stop approximation
safe enforce safe approximation
quality minimum improvement for accepted changes
DdNode* cuddBiasedUnderApprox ( DdManager dd,
DdNode f,
DdNode b,
int  numVars,
int  threshold,
double  quality1,
double  quality0 
)

Applies the biased remapping underappoximation algorithm.

Proceeds in three phases:

  • collect information on each node in the BDD; this is done via DFS.
  • traverse the BDD in top-down fashion and compute for each node whether remapping increases density.
  • traverse the BDD via DFS and actually perform the elimination.
Returns:
the approximated BDD if successful; NULL otherwise.
Side effects
None
See also:
Cudd_BiasedUnderApprox
Parameters:
dd DD manager
f current DD
b bias function
numVars maximum number of variables
threshold threshold under which approximation stops
quality1 minimum improvement for accepted changes when b=1
quality0 minimum improvement for accepted changes when b=0
DdNode* cuddRemapUnderApprox ( DdManager dd,
DdNode f,
int  numVars,
int  threshold,
double  quality 
)

Applies the remapping underappoximation algorithm.

Proceeds in three phases:

  • collect information on each node in the BDD; this is done via DFS.
  • traverse the BDD in top-down fashion and compute for each node whether remapping increases density.
  • traverse the BDD via DFS and actually perform the elimination.
Returns:
the approximated BDD if successful; NULL otherwise.
Side effects
None
See also:
Cudd_RemapUnderApprox
Parameters:
dd DD manager
f current DD
numVars maximum number of variables
threshold threshold under which approximation stops
quality minimum improvement for accepted changes
DdNode* cuddUnderApprox ( DdManager dd,
DdNode f,
int  numVars,
int  threshold,
int  safe,
double  quality 
)

Applies Tom Shiple's underappoximation algorithm.

Proceeds in three phases:

  • collect information on each node in the BDD; this is done via DFS.
  • traverse the BDD in top-down fashion and compute for each node whether its elimination increases density.
  • traverse the BDD via DFS and actually perform the elimination.
Returns:
the approximated BDD if successful; NULL otherwise.
Side effects
None
See also:
Cudd_UnderApprox
Parameters:
dd DD manager
f current DD
numVars maximum number of variables
threshold threshold under which approximation stops
safe enforce safe approximation
quality minimum improvement for accepted changes
static ApproxInfo* gatherInfo ( DdManager dd,
DdNode node,
int  numVars,
int  parity 
) [static]

Gathers information about each node.

Counts minterms and computes reference counts of each node in the BDD. The minterm count is separately computed for the node and its complement. This is to avoid cancellation errors.

Returns:
a pointer to the data structure holding the information gathered if successful; NULL otherwise.
Side effects
None
See also:
cuddUnderApprox gatherInfoAux
static NodeData* gatherInfoAux ( DdNode node,
ApproxInfo info,
int  parity 
) [static]

Recursively counts minterms and computes reference counts of each node in the BDD.

Similar to the cuddCountMintermAux which recursively counts the number of minterms for the dag rooted at each node in terms of the total number of variables (max). It assumes that the node pointer passed to it is regular and it maintains the invariant.

Side effects
None
See also:
gatherInfo
Parameters:
node function to analyze
info info on BDD
parity gather parity information
static DdNode* RAbuildSubset ( DdManager dd,
DdNode node,
ApproxInfo info 
) [static]

Builds the subset BDD for cuddRemapUnderApprox.

Based on the info table, performs remapping or replacement at selected nodes.

Returns:
a pointer to the result if successful; NULL otherwise.
Side effects
None
See also:
cuddRemapUnderApprox
Parameters:
dd DD manager
node current node
info node info
static int RAmarkNodes ( DdManager dd,
DdNode f,
ApproxInfo info,
int  threshold,
double  quality 
) [static]

Marks nodes for remapping.

Returns:
1 if successful; 0 otherwise.
Side effects
None
See also:
cuddRemapUnderApprox
Parameters:
dd manager
f function to be analyzed
info info on BDD
threshold when to stop approximating
quality minimum improvement for accepted changes
static DdNode* UAbuildSubset ( DdManager dd,
DdNode node,
ApproxInfo info 
) [static]

Builds the subset BDD.

Based on the info table, replaces selected nodes by zero.

Returns:
a pointer to the result if successful; NULL otherwise.
Side effects
None
See also:
cuddUnderApprox
Parameters:
dd DD manager
node current node
info node info
static int UAmarkNodes ( DdManager dd,
DdNode f,
ApproxInfo info,
int  threshold,
int  safe,
double  quality 
) [static]

Marks nodes for replacement by zero.

Returns:
1 if successful; 0 otherwise.
Side effects
None
See also:
cuddUnderApprox
Parameters:
dd manager
f function to be analyzed
info info on BDD
threshold when to stop approximating
safe enforce safe approximation
quality minimum improvement for accepted changes
static void updateParity ( DdNode node,
ApproxInfo info,
int  newparity 
) [static]

Recursively update the parity of the paths reaching a node.

Assumes that node is regular and propagates the invariant.

Side effects
None
See also:
gatherInfoAux
Parameters:
node function to analyze
info info on BDD
newparity new parity for node
static int updateRefs ( DdManager dd,
DdNode f,
DdNode skip,
ApproxInfo info,
DdLevelQueue queue 
) [static]

Update function reference counts to account for replacement.

Returns:
the number of nodes saved if successful; 0 otherwise.
Side effects
None
See also:
UAmarkNodes RAmarkNodes BAmarkNodes
 All Data Structures Files Functions Variables Typedefs Enumerations Defines

Generated on 31 Dec 2015 for cudd by  doxygen 1.6.1