You can not select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
2177 lines
64 KiB
2177 lines
64 KiB
/**
|
|
@file
|
|
|
|
@ingroup cudd
|
|
|
|
@brief Procedures to approximate a given %BDD.
|
|
|
|
@see cuddSubsetHB.c cuddSubsetSP.c cuddGenCof.c
|
|
|
|
@author Fabio Somenzi
|
|
|
|
@copyright@parblock
|
|
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.
|
|
@endparblock
|
|
|
|
*/
|
|
|
|
#ifdef __STDC__
|
|
#include <float.h>
|
|
#else
|
|
#define DBL_MAX_EXP 1024
|
|
#endif
|
|
#include "util.h"
|
|
#include "cuddInt.h"
|
|
|
|
/*---------------------------------------------------------------------------*/
|
|
/* Constant declarations */
|
|
/*---------------------------------------------------------------------------*/
|
|
|
|
#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
|
|
|
|
/*---------------------------------------------------------------------------*/
|
|
/* Stucture declarations */
|
|
/*---------------------------------------------------------------------------*/
|
|
|
|
/*---------------------------------------------------------------------------*/
|
|
/* Type declarations */
|
|
/*---------------------------------------------------------------------------*/
|
|
|
|
/**
|
|
** @brief Data structure to store the information on each node.
|
|
**
|
|
** @details It keeps the number of minterms of the function rooted at
|
|
** this node in terms of the number of variables specified by the
|
|
** user; the number of minterms of the complement; the impact of the
|
|
** number of minterms of this function on the number of minterms of
|
|
** the root function; the reference count of the node from within the
|
|
** root function; the flag that says whether the node intersects the
|
|
** care set; the flag that says whether the node should be replaced
|
|
** and how; the results of subsetting in both phases.
|
|
*/
|
|
typedef struct NodeData {
|
|
double mintermsP; /**< minterms for the regular node */
|
|
double mintermsN; /**< minterms for the complemented node */
|
|
int functionRef; /**< references from within this function */
|
|
char care; /**< node intersects care set */
|
|
char replace; /**< replacement decision */
|
|
short int parity; /**< 1: even; 2: odd; 3: both */
|
|
DdNode *resultP; /**< result for even parity */
|
|
DdNode *resultN; /**< result for odd parity */
|
|
} NodeData;
|
|
|
|
/**
|
|
** @brief Main bookkeeping data structure for approximation algorithms.
|
|
*/
|
|
typedef struct ApproxInfo {
|
|
DdNode *one; /**< one constant */
|
|
DdNode *zero; /**< %BDD zero constant */
|
|
NodeData *page; /**< per-node information */
|
|
DdHashTable *table; /**< hash table to access the per-node info */
|
|
int index; /**< index of the current node */
|
|
double max; /**< max number of minterms */
|
|
int size; /**< how many nodes are left */
|
|
double minterms; /**< how many minterms are left */
|
|
} ApproxInfo;
|
|
|
|
/**
|
|
** @brief Item of the queue used in the levelized traversal of the %BDD.
|
|
*/
|
|
typedef struct GlobalQueueItem {
|
|
struct GlobalQueueItem *next;
|
|
struct GlobalQueueItem *cnext;
|
|
DdNode *node;
|
|
double impactP;
|
|
double impactN;
|
|
} GlobalQueueItem;
|
|
|
|
/**
|
|
** @brief Type of the item of the local queue.
|
|
*/
|
|
typedef struct LocalQueueItem {
|
|
struct LocalQueueItem *next;
|
|
struct LocalQueueItem *cnext;
|
|
DdNode *node;
|
|
int localRef;
|
|
} LocalQueueItem;
|
|
|
|
|
|
/*---------------------------------------------------------------------------*/
|
|
/* Variable declarations */
|
|
/*---------------------------------------------------------------------------*/
|
|
|
|
|
|
/*---------------------------------------------------------------------------*/
|
|
/* Macro declarations */
|
|
/*---------------------------------------------------------------------------*/
|
|
|
|
/** \cond */
|
|
|
|
/*---------------------------------------------------------------------------*/
|
|
/* Static function prototypes */
|
|
/*---------------------------------------------------------------------------*/
|
|
|
|
static void updateParity (DdNode *node, ApproxInfo *info, int newparity);
|
|
static NodeData * gatherInfoAux (DdNode *node, ApproxInfo *info, int parity);
|
|
static ApproxInfo * gatherInfo (DdManager *dd, DdNode *node, int numVars, int parity);
|
|
static int computeSavings (DdManager *dd, DdNode *f, DdNode *skip, ApproxInfo *info, DdLevelQueue *queue);
|
|
static int updateRefs (DdManager *dd, DdNode *f, DdNode *skip, ApproxInfo *info, DdLevelQueue *queue);
|
|
static int UAmarkNodes (DdManager *dd, DdNode *f, ApproxInfo *info, int threshold, int safe, double quality);
|
|
static DdNode * UAbuildSubset (DdManager *dd, DdNode *node, ApproxInfo *info);
|
|
static int RAmarkNodes (DdManager *dd, DdNode *f, ApproxInfo *info, int threshold, double quality);
|
|
static int BAmarkNodes (DdManager *dd, DdNode *f, ApproxInfo *info, int threshold, double quality1, double quality0);
|
|
static DdNode * RAbuildSubset (DdManager *dd, DdNode *node, ApproxInfo *info);
|
|
static int BAapplyBias (DdManager *dd, DdNode *f, DdNode *b, ApproxInfo *info, DdHashTable *cache);
|
|
|
|
/** \endcond */
|
|
|
|
|
|
/*---------------------------------------------------------------------------*/
|
|
/* Definition of exported functions */
|
|
/*---------------------------------------------------------------------------*/
|
|
|
|
/**
|
|
@brief Extracts a dense subset from a %BDD with Shiple's
|
|
underapproximation method.
|
|
|
|
@details 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.
|
|
|
|
@return a pointer to the %BDD of the subset if successful; NULL if
|
|
the procedure runs out of memory.
|
|
|
|
@sideeffect None
|
|
|
|
@see Cudd_SubsetShortPaths Cudd_SubsetHeavyBranch Cudd_ReadSize
|
|
|
|
*/
|
|
DdNode *
|
|
Cudd_UnderApprox(
|
|
DdManager * dd /**< manager */,
|
|
DdNode * f /**< function to be subset */,
|
|
int numVars /**< number of variables in the support of f */,
|
|
int threshold /**< when to stop approximation */,
|
|
int safe /**< enforce safe approximation */,
|
|
double quality /**< minimum improvement for accepted changes */)
|
|
{
|
|
DdNode *subset;
|
|
|
|
do {
|
|
dd->reordered = 0;
|
|
subset = cuddUnderApprox(dd, f, numVars, threshold, safe, quality);
|
|
} while (dd->reordered == 1);
|
|
if (dd->errorCode == CUDD_TIMEOUT_EXPIRED && dd->timeoutHandler) {
|
|
dd->timeoutHandler(dd, dd->tohArg);
|
|
}
|
|
|
|
return(subset);
|
|
|
|
} /* end of Cudd_UnderApprox */
|
|
|
|
|
|
/**
|
|
@brief Extracts a dense superset from a %BDD with Shiple's
|
|
underapproximation method.
|
|
|
|
@details 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.
|
|
|
|
@return a pointer to the %BDD of the superset if successful. NULL if
|
|
intermediate result causes the procedure to run out of memory.
|
|
|
|
@sideeffect None
|
|
|
|
@see Cudd_SupersetHeavyBranch Cudd_SupersetShortPaths Cudd_ReadSize
|
|
|
|
*/
|
|
DdNode *
|
|
Cudd_OverApprox(
|
|
DdManager * dd /**< manager */,
|
|
DdNode * f /**< function to be superset */,
|
|
int numVars /**< number of variables in the support of f */,
|
|
int threshold /**< when to stop approximation */,
|
|
int safe /**< enforce safe approximation */,
|
|
double quality /**< minimum improvement for accepted changes */)
|
|
{
|
|
DdNode *subset, *g;
|
|
|
|
g = Cudd_Not(f);
|
|
do {
|
|
dd->reordered = 0;
|
|
subset = cuddUnderApprox(dd, g, numVars, threshold, safe, quality);
|
|
} while (dd->reordered == 1);
|
|
if (dd->errorCode == CUDD_TIMEOUT_EXPIRED && dd->timeoutHandler) {
|
|
dd->timeoutHandler(dd, dd->tohArg);
|
|
}
|
|
|
|
return(Cudd_NotCond(subset, (subset != NULL)));
|
|
|
|
} /* end of Cudd_OverApprox */
|
|
|
|
|
|
/**
|
|
@brief Extracts a dense subset from a %BDD with the remapping
|
|
underapproximation method.
|
|
|
|
@details 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.
|
|
|
|
@return a pointer to the %BDD of the subset if successful. NULL if
|
|
the procedure runs out of memory.
|
|
|
|
@sideeffect None
|
|
|
|
@see Cudd_SubsetShortPaths Cudd_SubsetHeavyBranch Cudd_UnderApprox Cudd_ReadSize
|
|
|
|
*/
|
|
DdNode *
|
|
Cudd_RemapUnderApprox(
|
|
DdManager * dd /**< manager */,
|
|
DdNode * f /**< function to be subset */,
|
|
int numVars /**< number of variables in the support of f */,
|
|
int threshold /**< when to stop approximation */,
|
|
double quality /**< minimum improvement for accepted changes */)
|
|
{
|
|
DdNode *subset;
|
|
|
|
do {
|
|
dd->reordered = 0;
|
|
subset = cuddRemapUnderApprox(dd, f, numVars, threshold, quality);
|
|
} while (dd->reordered == 1);
|
|
if (dd->errorCode == CUDD_TIMEOUT_EXPIRED && dd->timeoutHandler) {
|
|
|
|
