/**CFile***********************************************************************
FileName [cuddApprox.c]
PackageName [cudd]
Synopsis [Procedures to approximate a given BDD.]
Description [External procedures provided by this module:
<ul>
<li> Cudd_UnderApprox()
<li> Cudd_OverApprox()
<li> Cudd_RemapUnderApprox()
<li> Cudd_RemapOverApprox()
<li> Cudd_BiasedUnderApprox()
<li> Cudd_BiasedOverApprox()
</ul>
Internal procedures included in this module:
<ul>
<li> cuddUnderApprox()
<li> cuddRemapUnderApprox()
<li> cuddBiasedUnderApprox()
</ul>
Static procedures included in this module:
<ul>
<li> gatherInfoAux()
<li> gatherInfo()
<li> computeSavings()
<li> UAmarkNodes()
<li> UAbuildSubset()
<li> updateRefs()
<li> RAmarkNodes()
<li> BAmarkNodes()
<li> RAbuildSubset()
</ul>
]
SeeAlso [cuddSubsetHB.c cuddSubsetSP.c cuddGenCof.c]
Author [Fabio Somenzi]
Copyright [Copyright (c) 1995-2004, 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.]
******************************************************************************/
#ifdef __STDC__
#include <float.h>
#else
#define DBL_MAX_EXP 1024
#endif
#include "misc/util/util_hack.h"
#include "cuddInt.h"
ABC_NAMESPACE_IMPL_START
/*---------------------------------------------------------------------------*/
/* 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 */
/*---------------------------------------------------------------------------*/
/* Data structure to store the information on each node. 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
** reference count of the node from an internal node; and the flag
** that says whether the node should be replaced and how. */
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;
typedef struct ApproxInfo {
DdNode *one; /* one constant */
DdNode *zero; /* BDD zero constant */
NodeData *page; /* per-node information */
st__table *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;
/* Item of the queue used in the levelized traversal of the BDD. */
#ifdef __osf__
#pragma pointer_size save
#pragma pointer_size short
#endif
typedef struct GlobalQueueItem {
struct GlobalQueueItem *next;
struct GlobalQueueItem *cnext;
DdNode *node;
double impactP;
double impactN;
} GlobalQueueItem;
typedef struct LocalQueueItem {
struct LocalQueueItem *next;
struct LocalQueueItem *cnext;
DdNode *node;
int localRef;
} LocalQueueItem;
#ifdef __osf__
#pragma pointer_size restore
#endif
/*---------------------------------------------------------------------------*/
/* Variable declarations */
/*---------------------------------------------------------------------------*/
#ifndef lint
static char rcsid[] DD_UNUSED = "$Id: cuddApprox.c,v 1.27 2009/02/19 16:16:51 fabio Exp $";
#endif
/*---------------------------------------------------------------------------*/
/* Macro declarations */
/*---------------------------------------------------------------------------*/
/**AutomaticStart*************************************************************/
/*---------------------------------------------------------------------------*/
/* 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);
/**AutomaticEnd***************************************************************/
/*---------------------------------------------------------------------------*/
/* Definition of exported functions */
/*---------------------------------------------------------------------------*/
/**Function********************************************************************
Synopsis [Extracts a dense subset from a BDD with Shiple's
underapproximation method.]
Description [Extracts a dense subset from a BDD. 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. Returns a pointer to the BDD of the subset if
successful. NULL if the procedure runs out of memory. 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.]
SideEffects [None]
SeeAlso [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);
return(subset);
} /* end of Cudd_UnderApprox */
/**Function********************************************************************
Synopsis [Extracts a dense superset from a BDD with Shiple's
underapproximation method.]
Description [Extracts a dense superset from a BDD. 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.
Returns a pointer to the BDD of the superset if successful. NULL if
intermediate result causes the procedure to run out of memory. 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.]
SideEffects [None]
SeeAlso [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);
return(Cudd_NotCond(subset, (subset != NULL)));
} /* end of Cudd_OverApprox */
/**Function********************************************************************
Synopsis [Extracts a dense subset from a BDD with the remapping
underapproximation method.]
Description [Extracts a dense subset from a BDD. This procedure uses
a remapping technique and density as the cost function.
Returns a pointer to the BDD of the subset if
successful. NULL if the procedure runs out of memory. 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.]
SideEffects [None]
SeeAlso [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);
return(subset);
} /* end of Cudd_RemapUnderApprox */
/**Function********************************************************************
Synopsis [Extracts a dense superset from a BDD with the remapping
underapproximation method.]
Description [Extracts a dense superset from a BDD. 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.
Returns a pointer to the BDD of the superset if successful. NULL if
intermediate result causes the procedure to run out of memory. 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.]
SideEffects [None]
SeeAlso [Cudd_SupersetHeavyBranch Cudd_SupersetShortPaths Cudd_ReadSize]
******************************************************************************/
DdNode *
Cudd_RemapOverApprox(
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 */,
double quality /* minimum improvement for accepted changes */)
{
DdNode *subset, *g;
g = Cudd_Not(f);
do {
dd->reordered = 0;
subset = cuddRemapUnderApprox(dd, g, numVars, threshold, quality);
} while (dd->reordered == 1);
return(Cudd_NotCond(subset, (subset != NULL)));
} /* end of Cudd_RemapOverApprox */
/**Function********************************************************************
Synopsis [Extracts a dense subset from a BDD with the biased
underapproximation method.]
Description [Extracts a dense subset from a BDD. 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.
Returns a pointer to the BDD of the subset if
successful. NULL if the procedure runs out of memory. 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.]
SideEffects [None]
SeeAlso [Cudd_SubsetShortPaths Cudd_SubsetHeavyBranch Cudd_UnderApprox
Cudd_RemapUnderApprox Cudd_ReadSize]
******************************************************************************/
DdNode *
Cudd_BiasedUnderApprox(
DdManager *dd /* manager */,
DdNode *f /* function to be subset */,
DdNode *b /* bias function */,
int numVars /* number of variables in the support of f */,
int threshold /* when to stop approximation */,
double quality1 /* minimum improvement for accepted changes when b=1 */,
double quality0 /* minimum improvement for accepted changes when b=0 */)
{
DdNode *subset;
do {
dd->reordered = 0;
subset = cuddBiasedUnderApprox(dd, f, b, numVars, threshold, quality1,
quality0);
} while (dd->reordered == 1);
return(subset);
} /* end of Cudd_BiasedUnderApprox */
/**Function********************************************************************
Synopsis [Extracts a dense superset from a BDD with the biased
underapproximation method.]
Description [Extracts a dense superset from a BDD. 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.
Returns a pointer to the BDD of the superset if successful. NULL if
intermediate result causes the procedure to run out of memory. 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.]
SideEffects [None]
SeeAlso [Cudd_SupersetHeavyBranch Cudd_SupersetShortPaths
Cudd_RemapOverApprox Cudd_BiasedUnderApprox Cudd_ReadSize]
******************************************************************************/
DdNode *
Cudd_BiasedOverApprox(
DdManager *dd /* manager */,
DdNode *f /* function to be superset */,
DdNode *b /* bias function */,
int numVars /* number of variables in the support of f */,
int threshold /* when to stop approximation */,
double quality1 /* minimum improvement for accepted changes when b=1*/,
double quality0 /* minimum improvement for accepted changes when b=0 */)
{
DdNode *subset, *g;
g = Cudd_Not(f);
do {
dd->reordered = 0;
subset = cuddBiasedUnderApprox(dd, g, b, numVars, threshold, quality1,
quality0);
} while (dd->reordered == 1);
return(Cudd_NotCond(subset, (subset != NULL)));
} /* end of Cudd_BiasedOverApprox */
/*---------------------------------------------------------------------------*/
/* Definition of internal functions */
/*---------------------------------------------------------------------------*/
/**Function********************************************************************
Synopsis [Applies Tom Shiple's underappoximation algorithm.]
Description [Applies Tom Shiple's underappoximation algorithm. Proceeds
in three phases:
<ul>
<li> collect information on each node in the BDD; this is done via DFS.
<li> traverse the BDD in top-down fashion and compute for each node
whether its elimination increases density.
<li> traverse the BDD via DFS and actually perform the elimination.
</ul>
Returns the approximated BDD if successful; NULL otherwise.]
SideEffects [None]
SeeAlso [Cudd_UnderApprox]
******************************************************************************/
DdNode *
cuddUnderApprox(
DdManager * dd /* DD manager */,
DdNode * f /* current DD */,
int numVars /* maximum number of variables */,
int threshold /* threshold under which approximation stops */,
int safe /* enforce safe approximation */,
double quality /* minimum improvement for accepted changes */)
{
ApproxInfo *info;
DdNode *subset;
int result;
if (f == NULL) {
fprintf(dd->err, "Cannot subset, nil object\n");
return(NULL);
}
if (Cudd_IsConstant(f)) {
return(f);
}
/* Create table where node data are accessible via a hash table. */
info = gatherInfo(dd, f, numVars, safe);
if (info == NULL) {
(void) fprintf(dd->err, "Out-of-memory; Cannot subset\n");
dd->errorCode = CUDD_MEMORY_OUT;
return(NULL);
}
/* Mark nodes that should be replaced by zero. */
result = UAmarkNodes(dd, f, info, threshold, safe, quality);
if (result == 0) {
(void) fprintf(dd->err, "Out-of-memory; Cannot subset\n");
ABC_FREE(info->page);
st__free_table(info->table);
ABC_FREE(info);
dd->errorCode = CUDD_MEMORY_OUT;
return(NULL);
}
/* Build the result. */
subset = UAbuildSubset(dd, f, info);
#if 1
if (subset && info->size < Cudd_DagSize(subset))
(void) fprintf(dd->err, "Wrong prediction: %d versus actual %d\n",
info->size, Cudd_DagSize(subset));
#endif
ABC_FREE(info->page);
st__free_table(info->table);
ABC_FREE(info);
#ifdef DD_DEBUG
if (subset != NULL) {
cuddRef(subset);
#if 0
(void) Cudd_DebugCheck(dd);
(void) Cudd_CheckKeys(dd);
#endif
if (!Cudd_bddLeq(dd, subset, f)) {
(void) fprintf(dd->err, "Wrong subset\n");
dd->errorCode = CUDD_INTERNAL_ERROR;
}
cuddDeref(subset);
}
#endif
return(subset);
} /* end of cuddUnderApprox */
/**Function********************************************************************
Synopsis [Applies the remapping underappoximation algorithm.]
Description [Applies the remapping underappoximation algorithm.
Proceeds in three phases:
<ul>
<li> collect information on each node in the BDD; this is done via DFS.
<li> traverse the BDD in top-down fashion and compute for each node
whether remapping increases density.
<li> traverse the BDD via DFS and actually perform the elimination.
</ul>
Returns the approximated BDD if successful; NULL otherwise.]
SideEffects [None]
SeeAlso [Cudd_RemapUnderApprox]
******************************************************************************/
DdNode *
cuddRemapUnderApprox(
DdManager * dd /* DD manager */,
DdNode * f /* current DD */,
int numVars /* maximum number of variables */,
int threshold /* threshold under which approximation stops */,
double quality /* minimum improvement for accepted changes */)
{
ApproxInfo *info;
DdNode *subset;
int result;
if (f == NULL) {
fprintf(dd->err, "Cannot subset, nil object\n");
dd->errorCode = CUDD_INVALID_ARG;
return(NULL);
}
if (Cudd_IsConstant(f)) {
return(f);
}
/* Create table where node data are accessible via a hash table. */
info = gatherInfo(dd, f, numVars, TRUE);
if (info == NULL) {
(void) fprintf(dd->err, "Out-of-memory; Cannot subset\n");
dd->errorCode = CUDD_MEMORY_OUT;
return(NULL);
}
/* Mark nodes that should be replaced by zero. */
result = RAmarkNodes(dd, f, info, threshold, quality);
if (result == 0) {
(void) fprintf(dd->err, "Out-of-memory; Cannot subset\n");
ABC_FREE(info->page);
st__free_table(info->table);
ABC_FREE(info);
dd->errorCode = CUDD_MEMORY_OUT;
return(NULL);
}
/* Build the result. */
subset = RAbuildSubset(dd, f, info);
#if 1
if (subset && info->size < Cudd_DagSize(subset))
(void) fprintf(dd->err, "Wrong prediction: %d versus actual %d\n",
info->size, Cudd_DagSize(subset));
#endif
ABC_FREE(info->page);
st__free_table(info->table);
ABC_FREE(info);
#ifdef DD_DEBUG
if (subset != NULL) {
cuddRef(subset);
#if 0
(void) Cudd_DebugCheck(dd);
(void) Cudd_CheckKeys(dd);
#endif
if (!Cudd_bddLeq(dd, subset, f)) {
(void) fprintf(dd->err, "Wrong subset\n");
}
cuddDeref(subset);
dd->errorCode = CUDD_INTERNAL_ERROR;
}
#endif
return(subset);
} /* end of cuddRemapUnderApprox */
/**Function********************************************************************
Synopsis [Applies the biased remapping underappoximation algorithm.]
Description [Applies the biased remapping underappoximation algorithm.
Proceeds in three phases:
<ul>
<li> collect information on each node in the BDD; this is done via DFS.
<li> traverse the BDD in top-down fashion and compute for each node
whether remapping increases density.
<li> traverse the BDD via DFS and actually perform the elimination.
</ul>
Returns the approximated BDD if successful; NULL otherwise.]
SideEffects [None]
SeeAlso [Cudd_BiasedUnderApprox]
******************************************************************************/
DdNode *
cuddBiasedUnderApprox(
DdManager *dd /* DD manager */,
DdNode *f /* current DD */,
DdNode *b /* bias function */,
int numVars /* maximum number of variables */,
int threshold /* threshold under which approximation stops */,
double quality1 /* minimum improvement for accepted changes when b=1 */,
double quality0 /* minimum improvement for accepted changes when b=0 */)
{
ApproxInfo *info;
DdNode *subset;
int result;
DdHashTable *cache;
if (f == NULL) {
fprintf(dd->err, "Cannot subset, nil object\n");
dd->errorCode = CUDD_INVALID_ARG;
return(NULL);
}
if (Cudd_IsConstant(f)) {
return(f);
}
/* Create table where node data are accessible via a hash table. */
info = gatherInfo(dd, f, numVars, TRUE);
if (info == NULL) {
(void) fprintf(dd->err, "Out-of-memory; Cannot subset\n");
dd->errorCode = CUDD_MEMORY_OUT;
return(NULL);
}
cache = cuddHashTableInit(dd,2,2);
result = BAapplyBias(dd, Cudd_Regular(f), b, info, cache);
if (result == CARE_ERROR) {
(void) fprintf(dd->err, "Out-of-memory; Cannot subset\n");
cuddHashTableQuit(cache);
ABC_FREE(info->page);
st__free_table(info->table);
ABC_FREE(info);
dd->errorCode = CUDD_MEMORY_OUT;
return(NULL);
}
cuddHashTableQuit(cache);
/* Mark nodes that should be replaced by zero. */
result = BAmarkNodes(dd, f, info, threshold, quality1, quality0);
if (result == 0) {
(void) fprintf(dd->err, "Out-of-memory; Cannot subset\n");
ABC_FREE(info->page);
st__free_table(info->table);
ABC_FREE(info);
dd->errorCode = CUDD_MEMORY_OUT;
return(NULL);
}
/* Build the result. */
subset = RAbuildSubset(dd, f, info);
#if 1
if (subset && info->size < Cudd_DagSize(subset))
(void) fprintf(dd->err, "Wrong prediction: %d versus actual %d\n",
info->size, Cudd_DagSize(subset));
#endif
ABC_FREE(info->page);
st__free_table(info->table);
ABC_FREE(info);
#ifdef DD_DEBUG
if (subset != NULL) {
cuddRef(subset);
#if 0
(void) Cudd_DebugCheck(dd);
(void) Cudd_CheckKeys(dd);
#endif
if (!Cudd_bddLeq(dd, subset, f)) {
(void) fprintf(dd->err, "Wrong subset\n");
}
cuddDeref(subset);
dd->errorCode = CUDD_INTERNAL_ERROR;
}
#endif
return(subset);
} /* end of cuddBiasedUnderApprox */
/*---------------------------------------------------------------------------*/
/* Definition of static functions */
/*---------------------------------------------------------------------------*/
/**Function********************************************************************
Synopsis [Recursively update the parity of the paths reaching a node.]
Description [Recursively update the parity of the paths reaching a node.
Assumes that node is regular and propagates the invariant.]
SideEffects [None]
SeeAlso [gatherInfoAux]
******************************************************************************/
static void
updateParity(
DdNode * node /* function to analyze */,
ApproxInfo * info /* info on BDD */,
int newparity /* new parity for node */)
{
NodeData *infoN;
DdNode *E;
if (! st__lookup(info->table, (const char *)node, (char **)&infoN)) return;
if ((infoN->parity & newparity) != 0) return;
infoN->parity |= (short) newparity;
if (Cudd_IsConstant(node)) return;
updateParity(cuddT(node),info,newparity);
E = cuddE(node);
if (Cudd_IsComplement(E)) {
updateParity(Cudd_Not(E),info,3-newparity);
} else {
updateParity(E,info,newparity);
}
return;
} /* end of updateParity */
/**Function********************************************************************
Synopsis [Recursively counts minterms and computes reference counts
of each node in the BDD.]
Description [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.]
SideEffects [None]
SeeAlso [gatherInfo]
******************************************************************************/
static NodeData *
gatherInfoAux(
DdNode * node /* function to analyze */,
ApproxInfo * info /* info on BDD */,
int parity /* gather parity information */)
{
DdNode *N, *Nt, *Ne;
NodeData *infoN, *infoT, *infoE;
N = Cudd_Regular(node);
/* Check whether entry for this node exists. */
if ( st__lookup(info->table, (const char *)N, (char **)&infoN)) {
if (parity) {
/* Update parity and propagate. */
updateParity(N, info, 1 + (int) Cudd_IsComplement(node));
}
return(infoN);
}
/* Compute the cofactors. */
Nt = Cudd_NotCond(cuddT(N), N != node);
Ne = Cudd_NotCond(cuddE(N), N != node);
infoT = gatherInfoAux(Nt, info, parity);
if (infoT == NULL) return(NULL);
infoE = gatherInfoAux(Ne, info, parity);
if (infoE == NULL) return(NULL);
infoT->functionRef++;
infoE->functionRef++;
/* Point to the correct location in the page. */
infoN = &(info->page[info->index++]);
infoN->parity |= (short) (1 + Cudd_IsComplement(node));
infoN->mintermsP = infoT->mintermsP/2;
infoN->mintermsN = infoT->mintermsN/2;
if (Cudd_IsComplement(Ne) ^ Cudd_IsComplement(node)) {
infoN->mintermsP += infoE->mintermsN/2;
infoN->mintermsN += infoE->mintermsP/2;
} else {
infoN->mintermsP += infoE->mintermsP/2;
infoN->mintermsN += infoE->mintermsN/2;
}
/* Insert entry for the node in the table. */
if ( st__insert(info->table,(char *)N, (char *)infoN) == st__OUT_OF_MEM) {
return(NULL);
}
return(infoN);
} /* end of gatherInfoAux */
/**Function********************************************************************
Synopsis [Gathers information about each node.]
Description [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.]
SideEffects [None]
SeeAlso [cuddUnderApprox gatherInfoAux]
******************************************************************************/
static ApproxInfo *
gatherInfo(
DdManager * dd /* manager */,
DdNode * node /* function to be analyzed */,
int numVars /* number of variables node depends on */,
int parity /* gather parity information */)
{
ApproxInfo *info;
NodeData *infoTop;
/* If user did not give numVars value, set it to the maximum
** exponent that the pow function can take. The -1 is due to the
** discrepancy in the value that pow takes and the value that
** log gives.
*/
if (numVars == 0) {
numVars = DBL_MAX_EXP - 1;
}
info = ABC_ALLOC(ApproxInfo,1);
if (info == NULL) {
dd->errorCode = CUDD_MEMORY_OUT;
return(NULL);
}
info->max = pow(2.0,(double) numVars);
info->one = DD_ONE(dd);
info->zero = Cudd_Not(info->one);
info->size = Cudd_DagSize(node);
/* All the information gathered will be stored in a contiguous
** piece of memory, which is allocated here. This can be done
** efficiently because we have counted the number of nodes of the
** BDD. info->index points to the next available entry in the array
** that stores the per-node information. */
info->page = ABC_ALLOC(NodeData,info->size);
if (info->page == NULL) {
dd->errorCode = CUDD_MEMORY_OUT;
ABC_FREE(info);
return(NULL);
}
memset(info->page, 0, info->size * sizeof(NodeData)); /* clear all page */
info->table = st__init_table( st__ptrcmp, st__ptrhash);
if (info->table == NULL) {
ABC_FREE(info->page);
ABC_FREE(info);
return(NULL);
}
/* We visit the DAG in post-order DFS. Hence, the constant node is
** in first position, and the root of the DAG is in last position. */
/* Info for the constant node: Initialize only fields different from 0. */
if ( st__insert(info->table, (char *)info->one, (char *)info->page) == st__OUT_OF_MEM) {
ABC_FREE(info->page);
ABC_FREE(info);
st__free_table(info->table);
return(NULL);
}
info->page[0].mintermsP = info->max;
info->index = 1;
infoTop = gatherInfoAux(node,info,parity);
if (infoTop == NULL) {
ABC_FREE(info->page);
st__free_table(info->table);
ABC_FREE(info);
return(NULL);
}
if (Cudd_IsComplement(node)) {
info->minterms = infoTop->mintermsN;
} else {
info->minterms = infoTop->mintermsP;
}
infoTop->functionRef = 1;
return(info);
} /* end of gatherInfo */
/**Function********************************************************************
Synopsis [Counts the nodes that would be eliminated if a given node
were replaced by zero.]
Description [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.]
SideEffects [None]
SeeAlso [cuddUnderApprox]
******************************************************************************/
static int
computeSavings(
DdManager * dd,
DdNode * f,
DdNode * skip,
ApproxInfo * info,
DdLevelQueue * queue)
{
NodeData *infoN;
LocalQueueItem *item;
DdNode *node;
int savings = 0;
node = Cudd_Regular(f);
skip = Cudd_Regular(skip);
/* Insert the given node in the level queue. Its local reference
** count is set equal to the function reference count so that the
** search will continue from it when it is retrieved. */
item = (LocalQueueItem *)
cuddLevelQueueEnqueue(queue,node,cuddI(dd,node->index));
if (item == NULL)
return(0);
(void) st__lookup(info->table, (const char *)node, (char **)&infoN);
item->localRef = infoN->functionRef;
/* Process the queue. */
while (queue->first != NULL) {
item = (LocalQueueItem *) queue->first;
node = item->node;
cuddLevelQueueDequeue(queue,cuddI(dd,node->index));
if (node == skip) continue;
(void) st__lookup(info->table, (const char *)node, (char **)&infoN);
if (item->localRef != infoN->functionRef) {
/* This node is shared. */
continue;
}
savings++;
if (!cuddIsConstant(cuddT(node))) {
item = (LocalQueueItem *) cuddLevelQueueEnqueue(queue,cuddT(node),
cuddI(dd,cuddT(node)->index));
if (item == NULL) return(0);
item->localRef++;
}
if (!Cudd_IsConstant(cuddE(node))) {
item = (LocalQueueItem *) cuddLevelQueueEnqueue(queue,Cudd_Regular(cuddE(node)),
cuddI(dd,Cudd_Regular(cuddE(node))->index));
if (item == NULL) return(0);
item->localRef++;
}
}
#ifdef DD_DEBUG
/* At the end of a local search the queue should be empty. */
assert(queue->size == 0);
#endif
return(savings);
} /* end of computeSavings */
/**Function********************************************************************
Synopsis [Update function reference counts.]
Description [Update function reference counts to account for replacement.
Returns the number of nodes saved if successful; 0 otherwise.]
SideEffects [None]
SeeAlso [UAmarkNodes RAmarkNodes]
******************************************************************************/
static int
updateRefs(
DdManager * dd,
DdNode * f,
DdNode * skip,
ApproxInfo * info,
DdLevelQueue * queue)
{
NodeData *infoN;
LocalQueueItem *item;
DdNode *node;
int savings = 0;
node = Cudd_Regular(f);
/* Insert the given node in the level queue. Its function reference
** count is set equal to 0 so that the search will continue from it
** when it is retrieved. */
item = (LocalQueueItem *) cuddLevelQueueEnqueue(queue,node,cuddI(dd,node->index));
if (item == NULL)
return(0);
(void) st__lookup(info->table, (const char *)node, (char **)&infoN);
infoN->functionRef = 0;
if (skip != NULL) {
/* Increase the function reference count of the node to be skipped
** by 1 to account for the node pointing to it that will be created. */
skip = Cudd_Regular(skip);
(void) st__lookup(info->table, (const char *)skip, (char **)&infoN);
infoN->functionRef++;
}
/* Process the queue. */
while (queue->first != NULL) {
item = (LocalQueueItem *) queue->first;
node = item->node;
cuddLevelQueueDequeue(queue,cuddI(dd,node->index));
(void) st__lookup(info->table, (const char *)node, (char **)&infoN);
if (infoN->functionRef != 0) {
/* This node is shared or must be skipped. */
continue;
}
savings++;
if (!cuddIsConstant(cuddT(node))) {
item = (LocalQueueItem *) cuddLevelQueueEnqueue(queue,cuddT(node),
cuddI(dd,cuddT(node)->index));
if (item == NULL) return(0);
(void) st__lookup(info->table, (const char *)cuddT(node), (char **)&infoN);
infoN->functionRef--;
}
if (!Cudd_IsConstant(cuddE(node))) {
item = (LocalQueueItem *) cuddLevelQueueEnqueue(queue,Cudd_Regular(cuddE(node)),
cuddI(dd,Cudd_Regular(cuddE(node))->index));
if (item == NULL) return(0);
(void) st__lookup(info->table, (const char *)Cudd_Regular(cuddE(node)), (char **)&infoN);
infoN->functionRef--;
}
}
#ifdef DD_DEBUG
/* At the end of a local search the queue should be empty. */
assert(queue->size == 0);
#endif
return(savings);
} /* end of updateRefs */
/**Function********************************************************************
Synopsis [Marks nodes for replacement by zero.]
Description [Marks nodes for replacement by zero. Returns 1 if successful;
0 otherwise.]
SideEffects [None]
SeeAlso [cuddUnderApprox]
******************************************************************************/
static int
UAmarkNodes(
DdManager * dd /* manager */,
DdNode * f /* function to be analyzed */,
ApproxInfo * info /* info on BDD */,
int threshold /* when to stop approximating */,
int safe /* enforce safe approximation */,
double quality /* minimum improvement for accepted changes */)
{
DdLevelQueue *queue;
DdLevelQueue *localQueue;
NodeData *infoN;
GlobalQueueItem *item;
DdNode *node;
double numOnset;
double impactP, impactN;
int savings;
#if 0
(void) printf("initial size = %d initial minterms = %g\n",
info->size, info->minterms);
#endif
queue = cuddLevelQueueInit(dd->size,sizeof(GlobalQueueItem),info->size);
if (queue == NULL) {
return(0);
}
localQueue = cuddLevelQueueInit(dd->size,sizeof(LocalQueueItem),
dd->initSlots);
if (localQueue == NULL) {
cuddLevelQueueQuit(queue);
return(0);
}
node = Cudd_Regular(f);
item = (GlobalQueueItem *) cuddLevelQueueEnqueue(queue,node,cuddI(dd,node->index));
if (item == NULL) {
cuddLevelQueueQuit(queue);
cuddLevelQueueQuit(localQueue);
return(0);
}
if (Cudd_IsComplement(f)) {
item->impactP = 0.0;
item->impactN = 1.0;
} else {
item->impactP = 1.0;
item->impactN = 0.0;
}
while (queue->first != NULL) {
/* If the size of the subset is below the threshold, quit. */
if (info->size <= threshold)
break;
item = (GlobalQueueItem *) queue->first;
node = item->node;
node = Cudd_Regular(node);
(void) st__lookup(info->table, (const char *)node, (char **)&infoN);
if (safe && infoN->parity == 3) {
cuddLevelQueueDequeue(queue,cuddI(dd,node->index));
continue;
}
impactP = item->impactP;
impactN = item->impactN;
numOnset = infoN->mintermsP * impactP + infoN->mintermsN * impactN;
savings = computeSavings(dd,node,NULL,info,localQueue);
if (savings == 0) {
cuddLevelQueueQuit(queue);
cuddLevelQueueQuit(localQueue);
return(0);
}
cuddLevelQueueDequeue(queue,cuddI(dd,node->index));
#if 0
(void) printf("node %p: impact = %g/%g numOnset = %g savings %d\n",
node, impactP, impactN, numOnset, savings);
#endif
if ((1 - numOnset / info->minterms) >
quality * (1 - (double) savings / info->size)) {
infoN->replace = TRUE;
info->size -= savings;
info->minterms -=numOnset;
#if 0
(void) printf("replace: new size = %d new minterms = %g\n",
info->size, info->minterms);
#endif
savings -= updateRefs(dd,node,NULL,info,localQueue);
assert(savings == 0);
continue;
}
if (!cuddIsConstant(cuddT(node))) {
item = (GlobalQueueItem *) cuddLevelQueueEnqueue(queue,cuddT(node),
cuddI(dd,cuddT(node)->index));
item->impactP += impactP/2.0;
item->impactN += impactN/2.0;
}
if (!Cudd_IsConstant(cuddE(node))) {
item = (GlobalQueueItem *) cuddLevelQueueEnqueue(queue,Cudd_Regular(cuddE(node)),
cuddI(dd,Cudd_Regular(cuddE(node))->index));
if (Cudd_IsComplement(cuddE(node))) {
item->impactP += impactN/2.0;
item->impactN += impactP/2.0;
} else {
item->impactP += impactP/2.0;
item->impactN += impactN/2.0;
}
}
}
cuddLevelQueueQuit(queue);
cuddLevelQueueQuit(localQueue);
return(1);
} /* end of UAmarkNodes */
/**Function********************************************************************
Synopsis [Builds the subset BDD.]
Description [Builds the subset BDD. Based on the info table,
replaces selected nodes by zero. Returns a pointer to the result if
successful; NULL otherwise.]
SideEffects [None]
SeeAlso [cuddUnderApprox]
******************************************************************************/
static DdNode *
UAbuildSubset(
DdManager * dd /* DD manager */,
DdNode * node /* current node */,
ApproxInfo * info /* node info */)
{
DdNode *Nt, *Ne, *N, *t, *e, *r;
NodeData *infoN;
if (Cudd_IsConstant(node))
return(node);
N = Cudd_Regular(node);
if ( st__lookup(info->table, (const char *)N, (char **)&infoN)) {
if (infoN->replace == TRUE) {
return(info->zero);
}
if (N == node ) {
if (infoN->resultP != NULL) {
return(infoN->resultP);
}
} else {
if (infoN->resultN != NULL) {
return(infoN->resultN);
}
}
} else {
(void) fprintf(dd->err,
"Something is wrong, ought to be in info table\n");
dd->errorCode = CUDD_INTERNAL_ERROR;
return(NULL);
}
Nt = Cudd_NotCond(cuddT(N), Cudd_IsComplement(node));
Ne = Cudd_NotCond(cuddE(N), Cudd_IsComplement(node));
t = UAbuildSubset(dd, Nt, info);
if (t == NULL) {
return(NULL);
}
cuddRef(t);
e = UAbuildSubset(dd, Ne, info);
if (e == NULL) {
Cudd_RecursiveDeref(dd,t);
return(NULL);
}
cuddRef(e);
if (Cudd_IsComplement(t)) {
t = Cudd_Not(t);
e = Cudd_Not(e);
r = (t == e) ? t : cuddUniqueInter(dd, N->index, t, e);
if (r == NULL) {
Cudd_RecursiveDeref(dd, e);
Cudd_RecursiveDeref(dd, t);
return(NULL);
}
r = Cudd_Not(r);
} else {
r = (t == e) ? t : cuddUniqueInter(dd, N->index, t, e);
if (r == NULL) {
Cudd_RecursiveDeref(dd, e);
Cudd_RecursiveDeref(dd, t);
return(NULL);
}
}
cuddDeref(t);
cuddDeref(e);
if (N == node) {
infoN->resultP = r;
} else {
infoN->resultN = r;
}
return(r);
} /* end of UAbuildSubset */
/**Function********************************************************************
Synopsis [Marks nodes for remapping.]
Description [Marks nodes for remapping. Returns 1 if successful; 0
otherwise.]
SideEffects [None]
SeeAlso [cuddRemapUnderApprox]
******************************************************************************/
static int
RAmarkNodes(
DdManager * dd /* manager */,
DdNode * f /* function to be analyzed */,
ApproxInfo * info /* info on BDD */,
int threshold /* when to stop approximating */,
double quality /* minimum improvement for accepted changes */)
{
DdLevelQueue *queue;
DdLevelQueue *localQueue;
NodeData *infoN, *infoT, *infoE;
GlobalQueueItem *item;
DdNode *node, *T, *E;
DdNode *shared; /* grandchild shared by the two children of node */
double numOnset;
double impact, impactP, impactN;
double minterms;
int savings;
int replace;
#if 0
(void) fprintf(dd->out,"initial size = %d initial minterms = %g\n",
info->size, info->minterms);
#endif
queue = cuddLevelQueueInit(dd->size,sizeof(GlobalQueueItem),info->size);
if (queue == NULL) {
return(0);
}
localQueue = cuddLevelQueueInit(dd->size,sizeof(LocalQueueItem),
dd->initSlots);
if (localQueue == NULL) {
cuddLevelQueueQuit(queue);
return(0);
}
/* Enqueue regular pointer to root and initialize impact. */
node = Cudd_Regular(f);
item = (GlobalQueueItem *)
cuddLevelQueueEnqueue(queue,node,cuddI(dd,node->index));
if (item == NULL) {
cuddLevelQueueQuit(queue);
cuddLevelQueueQuit(localQueue);
return(0);
}
if (Cudd_IsComplement(f)) {
item->impactP = 0.0;
item->impactN = 1.0;
} else {
item->impactP = 1.0;
item->impactN = 0.0;
}
/* The nodes retrieved here are guaranteed to be non-terminal.
** The initial node is not terminal because constant nodes are
** dealt with in the calling procedure. Subsequent nodes are inserted
** only if they are not terminal. */
while (queue->first != NULL) {
/* If the size of the subset is below the threshold, quit. */
if (info->size <= threshold)
break;
item = (GlobalQueueItem *) queue->first;
node = item->node;
#ifdef DD_DEBUG
assert(item->impactP >= 0 && item->impactP <= 1.0);
assert(item->impactN >= 0 && item->impactN <= 1.0);
assert(!Cudd_IsComplement(node));
assert(!Cudd_IsConstant(node));
#endif
if (! st__lookup(info->table, (const char *)node, (char **)&infoN)) {
cuddLevelQueueQuit(queue);
cuddLevelQueueQuit(localQueue);
return(0);
}
#ifdef DD_DEBUG
assert(infoN->parity >= 1 && infoN->parity <= 3);
#endif
if (infoN->parity == 3) {
/* This node can be reached through paths of different parity.
** It is not safe to replace it, because remapping will give
** an incorrect result, while replacement by 0 may cause node
** splitting. */
cuddLevelQueueDequeue(queue,cuddI(dd,node->index));
continue;
}
T = cuddT(node);
E = cuddE(node);
shared = NULL;
impactP = item->impactP;
impactN = item->impactN;
if (Cudd_bddLeq(dd,T,E)) {
/* Here we know that E is regular. */
#ifdef DD_DEBUG
assert(!Cudd_IsComplement(E));
#endif
(void) st__lookup(info->table, (const char *)T, (char **)&infoT);
(void) st__lookup(info->table, (const char *)E, (char **)&infoE);
if (infoN->parity == 1) {
impact = impactP;
minterms = infoE->mintermsP/2.0 - infoT->mintermsP/2.0;
if (infoE->functionRef == 1 && !Cudd_IsConstant(E)) {
savings = 1 + computeSavings(dd,E,NULL,info,localQueue);
if (savings == 1) {
cuddLevelQueueQuit(queue);
cuddLevelQueueQuit(localQueue);
return(0);
}
} else {
savings = 1;
}
replace = REPLACE_E;
} else {
#ifdef DD_DEBUG
assert(infoN->parity == 2);
#endif
impact = impactN;
minterms = infoT->mintermsN/2.0 - infoE->mintermsN/2.0;
if (infoT->functionRef == 1 && !Cudd_IsConstant(T)) {
savings = 1 + computeSavings(dd,T,NULL,info,localQueue);
if (savings == 1) {
cuddLevelQueueQuit(queue);
cuddLevelQueueQuit(localQueue);
return(0);
}
} else {
savings = 1;
}
replace = REPLACE_T;
}
numOnset = impact * minterms;
} else if (Cudd_bddLeq(dd,E,T)) {
/* Here E may be complemented. */
DdNode *Ereg = Cudd_Regular(E);
(void) st__lookup(info->table, (const char *)T, (char **)&infoT);
(void) st__lookup(info->table, (const char *)Ereg, (char **)&infoE);
if (infoN->parity == 1) {
impact = impactP;
minterms = infoT->mintermsP/2.0 -
((E == Ereg) ? infoE->mintermsP : infoE->mintermsN)/2.0;
if (infoT->functionRef == 1 && !Cudd_IsConstant(T)) {
savings = 1 + computeSavings(dd,T,NULL,info,localQueue);
if (savings == 1) {
cuddLevelQueueQuit(queue);
cuddLevelQueueQuit(localQueue);
return(0);
}
} else {
savings = 1;
}
replace = REPLACE_T;
} else {
#ifdef DD_DEBUG
assert(infoN->parity == 2);
#endif
impact = impactN;
minterms = ((E == Ereg) ? infoE->mintermsN :
infoE->mintermsP)/2.0 - infoT->mintermsN/2.0;
if (infoE->functionRef == 1 && !Cudd_IsConstant(E)) {
savings = 1 + computeSavings(dd,E,NULL,info,localQueue);
if (savings == 1) {
cuddLevelQueueQuit(queue);
cuddLevelQueueQuit(localQueue);
return(0);
}
} else {
savings = 1;
}
replace = REPLACE_E;
}
numOnset = impact * minterms;
} else {
DdNode *Ereg = Cudd_Regular(E);
DdNode *TT = cuddT(T);
DdNode *ET = Cudd_NotCond(cuddT(Ereg), Cudd_IsComplement(E));
if (T->index == Ereg->index && TT == ET) {
shared = TT;
replace = REPLACE_TT;
} else {
DdNode *TE = cuddE(T);
DdNode *EE = Cudd_NotCond(cuddE(Ereg), Cudd_IsComplement(E));
if (T->index == Ereg->index && TE == EE) {
shared = TE;
replace = REPLACE_TE;
} else {
replace = REPLACE_N;
}
}
numOnset = infoN->mintermsP * impactP + infoN->mintermsN * impactN;
savings = computeSavings(dd,node,shared,info,localQueue);
if (shared != NULL) {
NodeData *infoS;
(void) st__lookup(info->table, (const char *)Cudd_Regular(shared), (char **)&infoS);
if (Cudd_IsComplement(shared)) {
numOnset -= (infoS->mintermsN * impactP +
infoS->mintermsP * impactN)/2.0;
} else {
numOnset -= (infoS->mintermsP * impactP +
infoS->mintermsN * impactN)/2.0;
}
savings--;
}
}
cuddLevelQueueDequeue(queue,cuddI(dd,node->index));
#if 0
if (replace == REPLACE_T || replace == REPLACE_E)
(void) printf("node %p: impact = %g numOnset = %g savings %d\n",
node, impact, numOnset, savings);
else
(void) printf("node %p: impact = %g/%g numOnset = %g savings %d\n",
node, impactP, impactN, numOnset, savings);
#endif
if ((1 - numOnset / info->minterms) >
quality * (1 - (double) savings / info->size)) {
infoN->replace = (char) replace;
info->size -= savings;
info->minterms -=numOnset;
#if 0
(void) printf("remap(%d): new size = %d new minterms = %g\n",
replace, info->size, info->minterms);
#endif
if (replace == REPLACE_N) {
savings -= updateRefs(dd,node,NULL,info,localQueue);
} else if (replace == REPLACE_T) {
savings -= updateRefs(dd,node,E,info,localQueue);
} else if (replace == REPLACE_E) {
savings -= updateRefs(dd,node,T,info,localQueue);
} else {
#ifdef DD_DEBUG
assert(replace == REPLACE_TT || replace == REPLACE_TE);
#endif
savings -= updateRefs(dd,node,shared,info,localQueue) - 1;
}
assert(savings == 0);
} else {
replace = NOTHING;
}
if (replace == REPLACE_N) continue;
if ((replace == REPLACE_E || replace == NOTHING) &&
!cuddIsConstant(cuddT(node))) {
item = (GlobalQueueItem *) cuddLevelQueueEnqueue(queue,cuddT(node),
cuddI(dd,cuddT(node)->index));
if (replace == REPLACE_E) {
item->impactP += impactP;
item->impactN += impactN;
} else {
item->impactP += impactP/2.0;
item->impactN += impactN/2.0;
}
}
if ((replace == REPLACE_T || replace == NOTHING) &&
!Cudd_IsConstant(cuddE(node))) {
item = (GlobalQueueItem *) cuddLevelQueueEnqueue(queue,Cudd_Regular(cuddE(node)),
cuddI(dd,Cudd_Regular(cuddE(node))->index));
if (Cudd_IsComplement(cuddE(node))) {
if (replace == REPLACE_T) {
item->impactP += impactN;
item->impactN += impactP;
} else {
item->impactP += impactN/2.0;
item->impactN += impactP/2.0;
}
} else {
if (replace == REPLACE_T) {
item->impactP += impactP;
item->impactN += impactN;
} else {
item->impactP += impactP/2.0;
item->impactN += impactN/2.0;
}
}
}
if ((replace == REPLACE_TT || replace == REPLACE_TE) &&
!Cudd_IsConstant(shared)) {
item = (GlobalQueueItem *) cuddLevelQueueEnqueue(queue,Cudd_Regular(shared),
cuddI(dd,Cudd_Regular(shared)->index));
if (Cudd_IsComplement(shared)) {
item->impactP += impactN;
item->impactN += impactP;
} else {
item->impactP += impactP;
item->impactN += impactN;
}
}
}
cuddLevelQueueQuit(queue);
cuddLevelQueueQuit(localQueue);
return(1);
} /* end of RAmarkNodes */
/**Function********************************************************************
Synopsis [Marks nodes for remapping.]
Description [Marks nodes for remapping. Returns 1 if successful; 0
otherwise.]
SideEffects [None]
SeeAlso [cuddRemapUnderApprox]
******************************************************************************/
static int
BAmarkNodes(
DdManager *dd /* manager */,
DdNode *f /* function to be analyzed */,
ApproxInfo *info /* info on BDD */,
int threshold /* when to stop approximating */,
double quality1 /* minimum improvement for accepted changes when b=1 */,
double quality0 /* minimum improvement for accepted changes when b=0 */)
{
DdLevelQueue *queue;
DdLevelQueue *localQueue;
NodeData *infoN, *infoT, *infoE;
GlobalQueueItem *item;
DdNode *node, *T, *E;
DdNode *shared; /* grandchild shared by the two children of node */
double numOnset;
double impact, impactP, impactN;
double minterms;
double quality;
int savings;
int replace;
#if 0
(void) fprintf(dd->out,"initial size = %d initial minterms = %g\n",
info->size, info->minterms);
#endif
queue = cuddLevelQueueInit(dd->size,sizeof(GlobalQueueItem),info->size);
if (queue == NULL) {
return(0);
}
localQueue = cuddLevelQueueInit(dd->size,sizeof(LocalQueueItem),
dd->initSlots);
if (localQueue == NULL) {
cuddLevelQueueQuit(queue);
return(0);
}
/* Enqueue regular pointer to root and initialize impact. */
node = Cudd_Regular(f);
item = (GlobalQueueItem *)
cuddLevelQueueEnqueue(queue,node,cuddI(dd,node->index));
if (item == NULL) {
cuddLevelQueueQuit(queue);
cuddLevelQueueQuit(localQueue);
return(0);
}
if (Cudd_IsComplement(f)) {
item->impactP = 0.0;
item->impactN = 1.0;
} else {
item->impactP = 1.0;
item->impactN = 0.0;
}
/* The nodes retrieved here are guaranteed to be non-terminal.
** The initial node is not terminal because constant nodes are
** dealt with in the calling procedure. Subsequent nodes are inserted
** only if they are not terminal. */
while (queue->first != NULL) {
/* If the size of the subset is below the threshold, quit. */
if (info->size <= threshold)
break;
item = (GlobalQueueItem *) queue->first;
node = item->node;
#ifdef DD_DEBUG
assert(item->impactP >= 0 && item->impactP <= 1.0);
assert(item->impactN >= 0 && item->impactN <= 1.0);
assert(!Cudd_IsComplement(node));
assert(!Cudd_IsConstant(node));
#endif
if (! st__lookup(info->table, (const char *)node, (char **)&infoN)) {
cuddLevelQueueQuit(queue);
cuddLevelQueueQuit(localQueue);
return(0);
}
quality = infoN->care ? quality1 : quality0;
#ifdef DD_DEBUG
assert(infoN->parity >= 1 && infoN->parity <= 3);
#endif
if (infoN->parity == 3) {
/* This node can be reached through paths of different parity.
** It is not safe to replace it, because remapping will give
** an incorrect result, while replacement by 0 may cause node
** splitting. */
cuddLevelQueueDequeue(queue,cuddI(dd,node->index));
continue;
}
T = cuddT(node);
E = cuddE(node);
shared = NULL;
impactP = item->impactP;
impactN = item->impactN;
if (Cudd_bddLeq(dd,T,E)) {
/* Here we know that E is regular. */
#ifdef DD_DEBUG
assert(!Cudd_IsComplement(E));
#endif
(void) st__lookup(info->table, (const char *)T, (char **)&infoT);
(void) st__lookup(info->table, (const char *)E, (char **)&infoE);
if (infoN->parity == 1) {
impact = impactP;
minterms = infoE->mintermsP/2.0 - infoT->mintermsP/2.0;
if (infoE->functionRef == 1 && !Cudd_IsConstant(E)) {
savings = 1 + computeSavings(dd,E,NULL,info,localQueue);
if (savings == 1) {
cuddLevelQueueQuit(queue);
cuddLevelQueueQuit(localQueue);
return(0);
}
} else {
savings = 1;
}
replace = REPLACE_E;
} else {
#ifdef DD_DEBUG
assert(infoN->parity == 2);
#endif
impact = impactN;
minterms = infoT->mintermsN/2.0 - infoE->mintermsN/2.0;
if (infoT->functionRef == 1 && !Cudd_IsConstant(T)) {
savings = 1 + computeSavings(dd,T,NULL,info,localQueue);
if (savings == 1) {
cuddLevelQueueQuit(queue);
cuddLevelQueueQuit(localQueue);
return(0);
}
} else {
savings = 1;
}
replace = REPLACE_T;
}
numOnset = impact * minterms;
} else if (Cudd_bddLeq(dd,E,T)) {
/* Here E may be complemented. */
DdNode *Ereg = Cudd_Regular(E);
(void) st__lookup(info->table, (const char *)T, (char **)&infoT);
(void) st__lookup(info->table, (const char *)Ereg, (char **)&infoE);
if (infoN->parity == 1) {
impact = impactP;
minterms = infoT->mintermsP/2.0 -
((E == Ereg) ? infoE->mintermsP : infoE->mintermsN)/2.0;
if (infoT->functionRef == 1 && !Cudd_IsConstant(T)) {
savings = 1 + computeSavings(dd,T,NULL,info,localQueue);
if (savings == 1) {
cuddLevelQueueQuit(queue);
cuddLevelQueueQuit(localQueue);
return(0);
}
} else {
savings = 1;
}
replace = REPLACE_T;
} else {
#ifdef DD_DEBUG
assert(infoN->parity == 2);
#endif
impact = impactN;
minterms = ((E == Ereg) ? infoE->mintermsN :
infoE->mintermsP)/2.0 - infoT->mintermsN/2.0;
if (infoE->functionRef == 1 && !Cudd_IsConstant(E)) {
savings = 1 + computeSavings(dd,E,NULL,info,localQueue);
if (savings == 1) {
cuddLevelQueueQuit(queue);
cuddLevelQueueQuit(localQueue);
return(0);
}
} else {
savings = 1;
}
replace = REPLACE_E;
}
numOnset = impact * minterms;
} else {
DdNode *Ereg = Cudd_Regular(E);
DdNode *TT = cuddT(T);
DdNode *ET = Cudd_NotCond(cuddT(Ereg), Cudd_IsComplement(E));
if (T->index == Ereg->index && TT == ET) {
shared = TT;
replace = REPLACE_TT;
} else {
DdNode *TE = cuddE(T);
DdNode *EE = Cudd_NotCond(cuddE(Ereg), Cudd_IsComplement(E));
if (T->index == Ereg->index && TE == EE) {
shared = TE;
replace = REPLACE_TE;
} else {
replace = REPLACE_N;
}
}
numOnset = infoN->mintermsP * impactP + infoN->mintermsN * impactN;
savings = computeSavings(dd,node,shared,info,localQueue);
if (shared != NULL) {
NodeData *infoS;
(void) st__lookup(info->table, (const char *)Cudd_Regular(shared), (char **)&infoS);
if (Cudd_IsComplement(shared)) {
numOnset -= (infoS->mintermsN * impactP +
infoS->mintermsP * impactN)/2.0;
} else {
numOnset -= (infoS->mintermsP * impactP +
infoS->mintermsN * impactN)/2.0;
}
savings--;
}
}
cuddLevelQueueDequeue(queue,cuddI(dd,node->index));
#if 0
if (replace == REPLACE_T || replace == REPLACE_E)
(void) printf("node %p: impact = %g numOnset = %g savings %d\n",
node, impact, numOnset, savings);
else
(void) printf("node %p: impact = %g/%g numOnset = %g savings %d\n",
node, impactP, impactN, numOnset, savings);
#endif
if ((1 - numOnset / info->minterms) >
quality * (1 - (double) savings / info->size)) {
infoN->replace = (char) replace;
info->size -= savings;
info->minterms -=numOnset;
#if 0
(void) printf("remap(%d): new size = %d new minterms = %g\n",
replace, info->size, info->minterms);
#endif
if (replace == REPLACE_N) {
savings -= updateRefs(dd,node,NULL,info,localQueue);
} else if (replace == REPLACE_T) {
savings -= updateRefs(dd,node,E,info,localQueue);
} else if (replace == REPLACE_E) {
savings -= updateRefs(dd,node,T,info,localQueue);
} else {
#ifdef DD_DEBUG
assert(replace == REPLACE_TT || replace == REPLACE_TE);
#endif
savings -= updateRefs(dd,node,shared,info,localQueue) - 1;
}
assert(savings == 0);
} else {
replace = NOTHING;
}
if (replace == REPLACE_N) continue;
if ((replace == REPLACE_E || replace == NOTHING) &&
!cuddIsConstant(cuddT(node))) {
item = (GlobalQueueItem *) cuddLevelQueueEnqueue(queue,cuddT(node),
cuddI(dd,cuddT(node)->index));
if (replace == REPLACE_E) {
item->impactP += impactP;
item->impactN += impactN;
} else {
item->impactP += impactP/2.0;
item->impactN += impactN/2.0;
}
}
if ((replace == REPLACE_T || replace == NOTHING) &&
!Cudd_IsConstant(cuddE(node))) {
item = (GlobalQueueItem *) cuddLevelQueueEnqueue(queue,Cudd_Regular(cuddE(node)),
cuddI(dd,Cudd_Regular(cuddE(node))->index));
if (Cudd_IsComplement(cuddE(node))) {
if (replace == REPLACE_T) {
item->impactP += impactN;
item->impactN += impactP;
} else {
item->impactP += impactN/2.0;
item->impactN += impactP/2.0;
}
} else {
if (replace == REPLACE_T) {
item->impactP += impactP;
item->impactN += impactN;
} else {
item->impactP += impactP/2.0;
item->impactN += impactN/2.0;
}
}
}
if ((replace == REPLACE_TT || replace == REPLACE_TE) &&
!Cudd_IsConstant(shared)) {
item = (GlobalQueueItem *) cuddLevelQueueEnqueue(queue,Cudd_Regular(shared),
cuddI(dd,Cudd_Regular(shared)->index));
if (Cudd_IsComplement(shared)) {
if (replace == REPLACE_T) {
item->impactP += impactN;
item->impactN += impactP;
} else {
item->impactP += impactN/2.0;
item->impactN += impactP/2.0;
}
} else {
if (replace == REPLACE_T) {
item->impactP += impactP;
item->impactN += impactN;
} else {
item->impactP += impactP/2.0;
item->impactN += impactN/2.0;
}
}
}
}
cuddLevelQueueQuit(queue);
cuddLevelQueueQuit(localQueue);
return(1);
} /* end of BAmarkNodes */
/**Function********************************************************************
Synopsis [Builds the subset BDD for cuddRemapUnderApprox.]
Description [Builds the subset BDDfor cuddRemapUnderApprox. Based
on the info table, performs remapping or replacement at selected
nodes. Returns a pointer to the result if successful; NULL
otherwise.]
SideEffects [None]
SeeAlso [cuddRemapUnderApprox]
******************************************************************************/
static DdNode *
RAbuildSubset(
DdManager * dd /* DD manager */,
DdNode * node /* current node */,
ApproxInfo * info /* node info */)
{
DdNode *Nt, *Ne, *N, *t, *e, *r;
NodeData *infoN;
if (Cudd_IsConstant(node))
return(node);
N = Cudd_Regular(node);
Nt = Cudd_NotCond(cuddT(N), Cudd_IsComplement(node));
Ne = Cudd_NotCond(cuddE(N), Cudd_IsComplement(node));
if ( st__lookup(info->table, (const char *)N, (char **)&infoN)) {
if (N == node ) {
if (infoN->resultP != NULL) {
return(infoN->resultP);
}
} else {
if (infoN->resultN != NULL) {
return(infoN->resultN);
}
}
if (infoN->replace == REPLACE_T) {
r = RAbuildSubset(dd, Ne, info);
return(r);
} else if (infoN->replace == REPLACE_E) {
r = RAbuildSubset(dd, Nt, info);
return(r);
} else if (infoN->replace == REPLACE_N) {
return(info->zero);
} else if (infoN->replace == REPLACE_TT) {
DdNode *Ntt = Cudd_NotCond(cuddT(cuddT(N)),
Cudd_IsComplement(node));
int index = cuddT(N)->index;
e = info->zero;
t = RAbuildSubset(dd, Ntt, info);
if (t == NULL) {
return(NULL);
}
cuddRef(t);
if (Cudd_IsComplement(t)) {
t = Cudd_Not(t);
e = Cudd_Not(e);
r = (t == e) ? t : cuddUniqueInter(dd, index, t, e);
if (r == NULL) {
Cudd_RecursiveDeref(dd, t);
return(NULL);
}
r = Cudd_Not(r);
} else {
r = (t == e) ? t : cuddUniqueInter(dd, index, t, e);
if (r == NULL) {
Cudd_RecursiveDeref(dd, t);
return(NULL);
}
}
cuddDeref(t);
return(r);
} else if (infoN->replace == REPLACE_TE) {
DdNode *Nte = Cudd_NotCond(cuddE(cuddT(N)),
Cudd_IsComplement(node));
int index = cuddT(N)->index;
t = info->one;
e = RAbuildSubset(dd, Nte, info);
if (e == NULL) {
return(NULL);
}
cuddRef(e);
e = Cudd_Not(e);
r = (t == e) ? t : cuddUniqueInter(dd, index, t, e);
if (r == NULL) {
Cudd_RecursiveDeref(dd, e);
return(NULL);
}
r =Cudd_Not(r);
cuddDeref(e);
return(r);
}
} else {
(void) fprintf(dd->err,
"Something is wrong, ought to be in info table\n");
dd->errorCode = CUDD_INTERNAL_ERROR;
return(NULL);
}
t = RAbuildSubset(dd, Nt, info);
if (t == NULL) {
return(NULL);
}
cuddRef(t);
e = RAbuildSubset(dd, Ne, info);
if (e == NULL) {
Cudd_RecursiveDeref(dd,t);
return(NULL);
}
cuddRef(e);
if (Cudd_IsComplement(t)) {
t = Cudd_Not(t);
e = Cudd_Not(e);
r = (t == e) ? t : cuddUniqueInter(dd, N->index, t, e);
if (r == NULL) {
Cudd_RecursiveDeref(dd, e);
Cudd_RecursiveDeref(dd, t);
return(NULL);
}
r = Cudd_Not(r);
} else {
r = (t == e) ? t : cuddUniqueInter(dd, N->index, t, e);
if (r == NULL) {
Cudd_RecursiveDeref(dd, e);
Cudd_RecursiveDeref(dd, t);
return(NULL);
}
}
cuddDeref(t);
cuddDeref(e);
if (N == node) {
infoN->resultP = r;
} else {
infoN->resultN = r;
}
return(r);
} /* end of RAbuildSubset */
/**Function********************************************************************
Synopsis [Finds don't care nodes.]
Description [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.]
SideEffects [None]
SeeAlso [cuddBiasedUnderApprox]
******************************************************************************/
static int
BAapplyBias(
DdManager *dd,
DdNode *f,
DdNode *b,
ApproxInfo *info,
DdHashTable *cache)
{
DdNode *one, *zero, *res;
DdNode *Ft, *Fe, *B, *Bt, *Be;
unsigned int topf, topb;
NodeData *infoF;
int careT, careE;
one = DD_ONE(dd);
zero = Cudd_Not(one);
if (! st__lookup(info->table, (const char *)f, (char **)&infoF))
return(CARE_ERROR);
if (f == one) return(TOTAL_CARE);
if (b == zero) return(infoF->care);
if (infoF->care == TOTAL_CARE) return(TOTAL_CARE);
if ((f->ref != 1 || Cudd_Regular(b)->ref != 1) &&
(res = cuddHashTableLookup2(cache,f,b)) != NULL) {
if (res->ref == 0) {
cache->manager->dead++;
cache->manager->constants.dead++;
}
return(infoF->care);
}
topf = dd->perm[f->index];
B = Cudd_Regular(b);
topb = cuddI(dd,B->index);
if (topf <= topb) {
Ft = cuddT(f); Fe = cuddE(f);
} else {
Ft = Fe = f;
}
if (topb <= topf) {
/* We know that b is not constant because f is not. */
Bt = cuddT(B); Be = cuddE(B);
if (Cudd_IsComplement(b)) {
Bt = Cudd_Not(Bt);
Be = Cudd_Not(Be);
}
} else {
Bt = Be = b;
}
careT = BAapplyBias(dd, Ft, Bt, info, cache);
if (careT == CARE_ERROR)
return(CARE_ERROR);
careE = BAapplyBias(dd, Cudd_Regular(Fe), Be, info, cache);
if (careE == CARE_ERROR)
return(CARE_ERROR);
if (careT == TOTAL_CARE && careE == TOTAL_CARE) {
infoF->care = TOTAL_CARE;
} else {
infoF->care = CARE;
}
if (f->ref != 1 || Cudd_Regular(b)->ref != 1) {
ptrint fanout = (ptrint) f->ref * Cudd_Regular(b)->ref;
cuddSatDec(fanout);
if (!cuddHashTableInsert2(cache,f,b,one,fanout)) {
return(CARE_ERROR);
}
}
return(infoF->care);
} /* end of BAapplyBias */
ABC_NAMESPACE_IMPL_END