abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
Data Structures | Macros | Typedefs | Functions | Variables
cuddApprox.c File Reference
#include "misc/util/util_hack.h"
#include "cuddInt.h"

Go to the source code of this file.

Data Structures

struct  NodeData
 
struct  ApproxInfo
 
struct  GlobalQueueItem
 
struct  LocalQueueItem
 

Macros

#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
 

Typedefs

typedef struct NodeData NodeData
 
typedef struct ApproxInfo ApproxInfo
 
typedef struct GlobalQueueItem GlobalQueueItem
 
typedef struct LocalQueueItem LocalQueueItem
 

Functions

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)
 
DdNode * Cudd_UnderApprox (DdManager *dd, DdNode *f, int numVars, int threshold, int safe, double quality)
 
DdNode * Cudd_OverApprox (DdManager *dd, DdNode *f, int numVars, int threshold, int safe, double quality)
 
DdNode * Cudd_RemapUnderApprox (DdManager *dd, DdNode *f, int numVars, int threshold, double quality)
 
DdNode * Cudd_RemapOverApprox (DdManager *dd, DdNode *f, int numVars, int threshold, double quality)
 
DdNode * Cudd_BiasedUnderApprox (DdManager *dd, DdNode *f, DdNode *b, int numVars, int threshold, double quality1, double quality0)
 
DdNode * Cudd_BiasedOverApprox (DdManager *dd, DdNode *f, DdNode *b, int numVars, int threshold, double quality1, double quality0)
 
DdNode * cuddUnderApprox (DdManager *dd, DdNode *f, int numVars, int threshold, int safe, double quality)
 
DdNode * cuddRemapUnderApprox (DdManager *dd, DdNode *f, int numVars, int threshold, double quality)
 
DdNode * cuddBiasedUnderApprox (DdManager *dd, DdNode *f, DdNode *b, int numVars, int threshold, double quality1, double quality0)
 

Variables

static char rcsid[] DD_UNUSED = "$Id: cuddApprox.c,v 1.27 2009/02/19 16:16:51 fabio Exp $"
 

Macro Definition Documentation

#define CARE   1

Definition at line 100 of file cuddApprox.c.

#define CARE_ERROR   3

Definition at line 102 of file cuddApprox.c.

#define DBL_MAX_EXP   1024

CFile***********************************************************************

FileName [cuddApprox.c]

PackageName [cudd]

Synopsis [Procedures to approximate a given BDD.]

Description [External procedures provided by this module:

Internal procedures included in this module:

Static procedures included in this module:

]

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.]

Definition at line 79 of file cuddApprox.c.

#define DONT_CARE   0

Definition at line 99 of file cuddApprox.c.

#define NOTHING   0

Definition at line 92 of file cuddApprox.c.

#define REPLACE_E   2

Definition at line 94 of file cuddApprox.c.

#define REPLACE_N   3

Definition at line 95 of file cuddApprox.c.

#define REPLACE_T   1

Definition at line 93 of file cuddApprox.c.

#define REPLACE_TE   5

Definition at line 97 of file cuddApprox.c.

#define REPLACE_TT   4

Definition at line 96 of file cuddApprox.c.

#define TOTAL_CARE   2

Definition at line 101 of file cuddApprox.c.

Typedef Documentation

typedef struct ApproxInfo ApproxInfo
typedef struct GlobalQueueItem GlobalQueueItem
typedef struct LocalQueueItem LocalQueueItem
typedef struct NodeData NodeData

Function Documentation

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

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]

Definition at line 2138 of file cuddApprox.c.

2144 {
2145  DdNode *one, *zero, *res;
2146  DdNode *Ft, *Fe, *B, *Bt, *Be;
2147  unsigned int topf, topb;
2148  NodeData *infoF;
2149  int careT, careE;
2150 
2151  one = DD_ONE(dd);
2152  zero = Cudd_Not(one);
2153 
2154  if (! st__lookup(info->table, (const char *)f, (char **)&infoF))
2155  return(CARE_ERROR);
2156  if (f == one) return(TOTAL_CARE);
2157  if (b == zero) return(infoF->care);
2158  if (infoF->care == TOTAL_CARE) return(TOTAL_CARE);
2159 
2160  if ((f->ref != 1 || Cudd_Regular(b)->ref != 1) &&
2161  (res = cuddHashTableLookup2(cache,f,b)) != NULL) {
2162  if (res->ref == 0) {
2163  cache->manager->dead++;
2164  cache->manager->constants.dead++;
2165  }
2166  return(infoF->care);
2167  }
2168 
2169  topf = dd->perm[f->index];
2170  B = Cudd_Regular(b);
2171  topb = cuddI(dd,B->index);
2172  if (topf <= topb) {
2173  Ft = cuddT(f); Fe = cuddE(f);
2174  } else {
2175  Ft = Fe = f;
2176  }
2177  if (topb <= topf) {
2178  /* We know that b is not constant because f is not. */
2179  Bt = cuddT(B); Be = cuddE(B);
2180  if (Cudd_IsComplement(b)) {
2181  Bt = Cudd_Not(Bt);
2182  Be = Cudd_Not(Be);
2183  }
2184  } else {
2185  Bt = Be = b;
2186  }
2187 
2188  careT = BAapplyBias(dd, Ft, Bt, info, cache);
2189  if (careT == CARE_ERROR)
2190  return(CARE_ERROR);
2191  careE = BAapplyBias(dd, Cudd_Regular(Fe), Be, info, cache);
2192  if (careE == CARE_ERROR)
2193  return(CARE_ERROR);
2194  if (careT == TOTAL_CARE && careE == TOTAL_CARE) {
2195  infoF->care = TOTAL_CARE;
2196  } else {
2197  infoF->care = CARE;
2198  }
2199 
2200  if (f->ref != 1 || Cudd_Regular(b)->ref != 1) {
2201  ptrint fanout = (ptrint) f->ref * Cudd_Regular(b)->ref;
2202  cuddSatDec(fanout);
2203  if (!cuddHashTableInsert2(cache,f,b,one,fanout)) {
2204  return(CARE_ERROR);
2205  }
2206  }
2207  return(infoF->care);
2208 
2209 } /* end of BAapplyBias */
DdNode::ref
DdHalfWord ref
Definition: cudd.h:280
DdNode
Definition: cudd.h:278
Cudd_Not
#define Cudd_Not(node)
Definition: cudd.h:367
BAapplyBias
static int BAapplyBias(DdManager *dd, DdNode *f, DdNode *b, ApproxInfo *info, DdHashTable *cache)
Definition: cuddApprox.c:2138
CARE_ERROR
#define CARE_ERROR
Definition: cuddApprox.c:102
DdHashTable::manager
DdManager * manager
Definition: cuddInt.h:313
Cudd_Regular
#define Cudd_Regular(node)
Definition: cudd.h:397
DdManager::dead
unsigned int dead
Definition: cuddInt.h:371
NodeData::care
char care
Definition: cuddApprox.c:124
Cudd_IsComplement
#define Cudd_IsComplement(node)
Definition: cudd.h:425
DdSubtable::dead
unsigned int dead
Definition: cuddInt.h:332
one
static DdNode * one
Definition: cuddDecomp.c:112
ptrint
ABC_PTRINT_T ptrint
Definition: cuddInt.h:260
TOTAL_CARE
#define TOTAL_CARE
Definition: cuddApprox.c:101
ApproxInfo::table
st__table * table
Definition: cuddApprox.c:135
cuddT
#define cuddT(node)
Definition: cuddInt.h:636
cuddHashTableInsert2
int cuddHashTableInsert2(DdHashTable *hash, DdNode *f, DdNode *g, DdNode *value, ptrint count)
Definition: cuddLCache.c:874
cuddI
#define cuddI(dd, index)
Definition: cuddInt.h:686
st__lookup
int st__lookup(st__table *table, const char *key, char **value)
Definition: st.c:114
CARE
#define CARE
Definition: cuddApprox.c:100
DdNode::index
DdHalfWord index
Definition: cudd.h:279
cuddHashTableLookup2
DdNode * cuddHashTableLookup2(DdHashTable *hash, DdNode *f, DdNode *g)
Definition: cuddLCache.c:928
cuddE
#define cuddE(node)
Definition: cuddInt.h:652
cuddSatDec
#define cuddSatDec(x)
Definition: cuddInt.h:896
DdManager::constants
DdSubtable constants
Definition: cuddInt.h:367
DD_ONE
#define DD_ONE(dd)
Definition: cuddInt.h:911
DdManager::perm
int * perm
Definition: cuddInt.h:386
zero
static DdNode * zero
Definition: cuddApa.c:100
static int BAmarkNodes ( DdManager *  dd,
DdNode *  f,
ApproxInfo *  info,
int  threshold,
double  quality1,
double  quality0 
)
static

Function********************************************************************

Synopsis [Marks nodes for remapping.]

Description [Marks nodes for remapping. Returns 1 if successful; 0 otherwise.]

SideEffects [None]

SeeAlso [cuddRemapUnderApprox]

Definition at line 1673 of file cuddApprox.c.

1680 {
1681  DdLevelQueue *queue;
1682  DdLevelQueue *localQueue;
1683  NodeData *infoN, *infoT, *infoE;
1684  GlobalQueueItem *item;
1685  DdNode *node, *T, *E;
1686  DdNode *shared; /* grandchild shared by the two children of node */
1687  double numOnset;
1688  double impact, impactP, impactN;
1689  double minterms;
1690  double quality;
1691  int savings;
1692  int replace;
1693 
1694 #if 0
1695  (void) fprintf(dd->out,"initial size = %d initial minterms = %g\n",
1696  info->size, info->minterms);
1697 #endif
1698  queue = cuddLevelQueueInit(dd->size,sizeof(GlobalQueueItem),info->size);
1699  if (queue == NULL) {
1700  return(0);
1701  }
1702  localQueue = cuddLevelQueueInit(dd->size,sizeof(LocalQueueItem),
1703  dd->initSlots);
1704  if (localQueue == NULL) {
1705  cuddLevelQueueQuit(queue);
1706  return(0);
1707  }
1708  /* Enqueue regular pointer to root and initialize impact. */
1709  node = Cudd_Regular(f);
1710  item = (GlobalQueueItem *)
1711  cuddLevelQueueEnqueue(queue,node,cuddI(dd,node->index));
1712  if (item == NULL) {
1713  cuddLevelQueueQuit(queue);
1714  cuddLevelQueueQuit(localQueue);
1715  return(0);
1716  }
1717  if (Cudd_IsComplement(f)) {
1718  item->impactP = 0.0;
1719  item->impactN = 1.0;
1720  } else {
1721  item->impactP = 1.0;
1722  item->impactN = 0.0;
1723  }
1724  /* The nodes retrieved here are guaranteed to be non-terminal.
1725  ** The initial node is not terminal because constant nodes are
1726  ** dealt with in the calling procedure. Subsequent nodes are inserted
1727  ** only if they are not terminal. */
1728  while (queue->first != NULL) {
1729  /* If the size of the subset is below the threshold, quit. */
1730  if (info->size <= threshold)
1731  break;
1732  item = (GlobalQueueItem *) queue->first;
1733  node = item->node;
1734 #ifdef DD_DEBUG
1735  assert(item->impactP >= 0 && item->impactP <= 1.0);
1736  assert(item->impactN >= 0 && item->impactN <= 1.0);
1737  assert(!Cudd_IsComplement(node));
1738  assert(!Cudd_IsConstant(node));
1739 #endif
1740  if (! st__lookup(info->table, (const char *)node, (char **)&infoN)) {
1741  cuddLevelQueueQuit(queue);
1742  cuddLevelQueueQuit(localQueue);
1743  return(0);
1744  }
1745  quality = infoN->care ? quality1 : quality0;
1746 #ifdef DD_DEBUG
1747  assert(infoN->parity >= 1 && infoN->parity <= 3);
1748 #endif
1749  if (infoN->parity == 3) {
1750  /* This node can be reached through paths of different parity.
1751  ** It is not safe to replace it, because remapping will give
1752  ** an incorrect result, while replacement by 0 may cause node
1753  ** splitting. */
1754  cuddLevelQueueDequeue(queue,cuddI(dd,node->index));
1755  continue;
1756  }
1757  T = cuddT(node);
1758  E = cuddE(node);
1759  shared = NULL;
1760  impactP = item->impactP;
1761  impactN = item->impactN;
1762  if (Cudd_bddLeq(dd,T,E)) {
1763  /* Here we know that E is regular. */
1764 #ifdef DD_DEBUG
1765  assert(!Cudd_IsComplement(E));
1766 #endif
1767  (void) st__lookup(info->table, (const char *)T, (char **)&infoT);
1768  (void) st__lookup(info->table, (const char *)E, (char **)&infoE);
1769  if (infoN->parity == 1) {
1770  impact = impactP;
1771  minterms = infoE->mintermsP/2.0 - infoT->mintermsP/2.0;
1772  if (infoE->functionRef == 1 && !Cudd_IsConstant(E)) {
1773  savings = 1 + computeSavings(dd,E,NULL,info,localQueue);
1774  if (savings == 1) {
1775  cuddLevelQueueQuit(queue);
1776  cuddLevelQueueQuit(localQueue);
1777  return(0);
1778  }
1779  } else {
1780  savings = 1;
1781  }
1782  replace = REPLACE_E;
1783  } else {
1784 #ifdef DD_DEBUG
1785  assert(infoN->parity == 2);
1786 #endif
1787  impact = impactN;
1788  minterms = infoT->mintermsN/2.0 - infoE->mintermsN/2.0;
1789  if (infoT->functionRef == 1 && !Cudd_IsConstant(T)) {
1790  savings = 1 + computeSavings(dd,T,NULL,info,localQueue);
1791  if (savings == 1) {
1792  cuddLevelQueueQuit(queue);
1793  cuddLevelQueueQuit(localQueue);
1794  return(0);
1795  }
1796  } else {
1797  savings = 1;
1798  }
1799  replace = REPLACE_T;
1800  }
1801  numOnset = impact * minterms;
1802  } else if (Cudd_bddLeq(dd,E,T)) {
1803  /* Here E may be complemented. */
1804  DdNode *Ereg = Cudd_Regular(E);
1805  (void) st__lookup(info->table, (const char *)T, (char **)&infoT);
1806  (void) st__lookup(info->table, (const char *)Ereg, (char **)&infoE);
1807  if (infoN->parity == 1) {
1808  impact = impactP;
1809  minterms = infoT->mintermsP/2.0 -
1810  ((E == Ereg) ? infoE->mintermsP : infoE->mintermsN)/2.0;
1811  if (infoT->functionRef == 1 && !Cudd_IsConstant(T)) {
1812  savings = 1 + computeSavings(dd,T,NULL,info,localQueue);
1813  if (savings == 1) {
1814  cuddLevelQueueQuit(queue);
1815  cuddLevelQueueQuit(localQueue);
1816  return(0);
1817  }
1818  } else {
1819  savings = 1;
1820  }
1821  replace = REPLACE_T;
1822  } else {
1823 #ifdef DD_DEBUG
1824  assert(infoN->parity == 2);
1825 #endif
1826  impact = impactN;
1827  minterms = ((E == Ereg) ? infoE->mintermsN :
1828  infoE->mintermsP)/2.0 - infoT->mintermsN/2.0;
1829  if (infoE->functionRef == 1 && !Cudd_IsConstant(E)) {
1830  savings = 1 + computeSavings(dd,E,NULL,info,localQueue);
1831  if (savings == 1) {
1832  cuddLevelQueueQuit(queue);
1833  cuddLevelQueueQuit(localQueue);
1834  return(0);
1835  }
1836  } else {
1837  savings = 1;
1838  }
1839  replace = REPLACE_E;
1840  }
1841  numOnset = impact * minterms;
1842  } else {
1843  DdNode *Ereg = Cudd_Regular(E);
1844  DdNode *TT = cuddT(T);
1845  DdNode *ET = Cudd_NotCond(cuddT(Ereg), Cudd_IsComplement(E));
1846  if (T->index == Ereg->index && TT == ET) {
1847  shared = TT;
1848  replace = REPLACE_TT;
1849  } else {
1850  DdNode *TE = cuddE(T);
1851  DdNode *EE = Cudd_NotCond(cuddE(Ereg), Cudd_IsComplement(E));
1852  if (T->index == Ereg->index && TE == EE) {
1853  shared = TE;
1854  replace = REPLACE_TE;
1855  } else {
1856  replace = REPLACE_N;
1857  }
1858  }
1859  numOnset = infoN->mintermsP * impactP + infoN->mintermsN * impactN;
1860  savings = computeSavings(dd,node,shared,info,localQueue);
1861  if (shared != NULL) {
1862  NodeData *infoS;
1863  (void) st__lookup(info->table, (const char *)Cudd_Regular(shared), (char **)&infoS);
1864  if (Cudd_IsComplement(shared)) {
1865  numOnset -= (infoS->mintermsN * impactP +
1866  infoS->mintermsP * impactN)/2.0;
1867  } else {
1868  numOnset -= (infoS->mintermsP * impactP +
1869  infoS->mintermsN * impactN)/2.0;
1870  }
1871  savings--;
1872  }
1873  }
1874 
1875  cuddLevelQueueDequeue(queue,cuddI(dd,node->index));
1876 #if 0
1877  if (replace == REPLACE_T || replace == REPLACE_E)
1878  (void) printf("node %p: impact = %g numOnset = %g savings %d\n",
1879  node, impact, numOnset, savings);
1880  else
1881  (void) printf("node %p: impact = %g/%g numOnset = %g savings %d\n",
1882  node, impactP, impactN, numOnset, savings);
1883 #endif
1884  if ((1 - numOnset / info->minterms) >
1885  quality * (1 - (double) savings / info->size)) {
1886  infoN->replace = (char) replace;
1887  info->size -= savings;
1888  info->minterms -=numOnset;
1889 #if 0
1890  (void) printf("remap(%d): new size = %d new minterms = %g\n",
1891  replace, info->size, info->minterms);
1892 #endif
1893  if (replace == REPLACE_N) {
1894  savings -= updateRefs(dd,node,NULL,info,localQueue);
1895  } else if (replace == REPLACE_T) {
1896  savings -= updateRefs(dd,node,E,info,localQueue);
1897  } else if (replace == REPLACE_E) {
1898  savings -= updateRefs(dd,node,T,info,localQueue);
1899  } else {
1900 #ifdef DD_DEBUG
1901  assert(replace == REPLACE_TT || replace == REPLACE_TE);
1902 #endif
1903  savings -= updateRefs(dd,node,shared,info,localQueue) - 1;
1904  }
1905  assert(savings == 0);
1906  } else {
1907  replace = NOTHING;
1908  }
1909  if (replace == REPLACE_N) continue;
1910  if ((replace == REPLACE_E || replace == NOTHING) &&
1911  !cuddIsConstant(cuddT(node))) {
1912  item = (GlobalQueueItem *) cuddLevelQueueEnqueue(queue,cuddT(node),
1913  cuddI(dd,cuddT(node)->index));
1914  if (replace == REPLACE_E) {
1915  item->impactP += impactP;
1916  item->impactN += impactN;
1917  } else {
1918  item->impactP += impactP/2.0;
1919  item->impactN += impactN/2.0;
1920  }
1921  }
1922  if ((replace == REPLACE_T || replace == NOTHING) &&
1923  !Cudd_IsConstant(cuddE(node))) {
1924  item = (GlobalQueueItem *) cuddLevelQueueEnqueue(queue,Cudd_Regular(cuddE(node)),
1925  cuddI(dd,Cudd_Regular(cuddE(node))->index));
1926  if (Cudd_IsComplement(cuddE(node))) {
1927  if (replace == REPLACE_T) {
1928  item->impactP += impactN;
1929  item->impactN += impactP;
1930  } else {
1931  item->impactP += impactN/2.0;
1932  item->impactN += impactP/2.0;
1933  }
1934  } else {
1935  if (replace == REPLACE_T) {
1936  item->impactP += impactP;
1937  item->impactN += impactN;
1938  } else {
1939  item->impactP += impactP/2.0;
1940  item->impactN += impactN/2.0;
1941  }
1942  }
1943  }
1944  if ((replace == REPLACE_TT || replace == REPLACE_TE) &&
1945  !Cudd_IsConstant(shared)) {
1946  item = (GlobalQueueItem *) cuddLevelQueueEnqueue(queue,Cudd_Regular(shared),
1947  cuddI(dd,Cudd_Regular(shared)->index));
1948  if (Cudd_IsComplement(shared)) {
1949  if (replace == REPLACE_T) {
1950  item->impactP += impactN;
1951  item->impactN += impactP;
1952  } else {
1953  item->impactP += impactN/2.0;
1954  item->impactN += impactP/2.0;
1955  }
1956  } else {
1957  if (replace == REPLACE_T) {
1958  item->impactP += impactP;
1959  item->impactN += impactN;
1960  } else {
1961  item->impactP += impactP/2.0;
1962  item->impactN += impactN/2.0;
1963  }
1964  }
1965  }
1966  }
1967 
1968  cuddLevelQueueQuit(queue);
1969  cuddLevelQueueQuit(localQueue);
1970  return(1);
1971 
1972 } /* end of BAmarkNodes */
cuddLevelQueueDequeue
void cuddLevelQueueDequeue(DdLevelQueue *queue, int level)
Definition: cuddLevelQ.c:354
updateRefs
static int updateRefs(DdManager *dd, DdNode *f, DdNode *skip, ApproxInfo *info, DdLevelQueue *queue)
Definition: cuddApprox.c:1073
DdNode
Definition: cudd.h:278
computeSavings
static int computeSavings(DdManager *dd, DdNode *f, DdNode *skip, ApproxInfo *info, DdLevelQueue *queue)
Definition: cuddApprox.c:1001
DdManager::size
int size
Definition: cuddInt.h:361
Cudd_IsConstant
#define Cudd_IsConstant(node)
Definition: cudd.h:352
Cudd_Regular
#define Cudd_Regular(node)
Definition: cudd.h:397
ApproxInfo::minterms
double minterms
Definition: cuddApprox.c:139
cuddLevelQueueQuit
void cuddLevelQueueQuit(DdLevelQueue *queue)
Definition: cuddLevelQ.c:244
REPLACE_TE
#define REPLACE_TE
Definition: cuddApprox.c:97
REPLACE_E
#define REPLACE_E
Definition: cuddApprox.c:94
GlobalQueueItem::node
DdNode * node
Definition: cuddApprox.c:150
NodeData::mintermsP
double mintermsP
Definition: cuddApprox.c:121
DdManager::initSlots
unsigned int initSlots
Definition: cuddInt.h:379
cuddLevelQueueEnqueue
void * cuddLevelQueueEnqueue(DdLevelQueue *queue, void *key, int level)
Definition: cuddLevelQ.c:282
cuddLevelQueueInit
DdLevelQueue * cuddLevelQueueInit(int levels, int itemSize, int numBuckets)
Definition: cuddLevelQ.c:169
NodeData::care
char care
Definition: cuddApprox.c:124
Cudd_IsComplement
#define Cudd_IsComplement(node)
Definition: cudd.h:425
DdManager::out
FILE * out
Definition: cuddInt.h:441
NodeData::mintermsN
double mintermsN
Definition: cuddApprox.c:122
REPLACE_N
#define REPLACE_N
Definition: cuddApprox.c:95
cuddIsConstant
#define cuddIsConstant(node)
Definition: cuddInt.h:620
REPLACE_TT
#define REPLACE_TT
Definition: cuddApprox.c:96
ApproxInfo::table
st__table * table
Definition: cuddApprox.c:135
cuddT
#define cuddT(node)
Definition: cuddInt.h:636
DdLevelQueue::first
void * first
Definition: cuddInt.h:509
cuddI
#define cuddI(dd, index)
Definition: cuddInt.h:686
DD_DEBUG
#define DD_DEBUG
Definition: cuddPriority.c:88
Cudd_bddLeq
int Cudd_bddLeq(DdManager *dd, DdNode *f, DdNode *g)
Definition: cuddBddIte.c:536
st__lookup
int st__lookup(st__table *table, const char *key, char **value)
Definition: st.c:114
REPLACE_T
#define REPLACE_T
Definition: cuddApprox.c:93
NodeData::parity
short int parity
Definition: cuddApprox.c:126
DdNode::index
DdHalfWord index
Definition: cudd.h:279
cuddE
#define cuddE(node)
Definition: cuddInt.h:652
Cudd_NotCond
#define Cudd_NotCond(node, c)
Definition: cudd.h:383
assert
#define assert(ex)
Definition: util_old.h:213
minterms
pset minterms()
NodeData::replace
char replace
Definition: cuddApprox.c:125
NOTHING
#define NOTHING
Definition: cuddApprox.c:92
static int computeSavings ( DdManager *  dd,
DdNode *  f,
DdNode *  skip,
ApproxInfo *  info,
DdLevelQueue *  queue 
)
static

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]

Definition at line 1001 of file cuddApprox.c.

1007 {
1008  NodeData *infoN;
1009  LocalQueueItem *item;
1010  DdNode *node;
1011  int savings = 0;
1012 
1013  node = Cudd_Regular(f);
1014  skip = Cudd_Regular(skip);
1015  /* Insert the given node in the level queue. Its local reference
1016  ** count is set equal to the function reference count so that the
1017  ** search will continue from it when it is retrieved. */
1018  item = (LocalQueueItem *)
1019  cuddLevelQueueEnqueue(queue,node,cuddI(dd,node->index));
1020  if (item == NULL)
1021  return(0);
1022  (void) st__lookup(info->table, (const char *)node, (char **)&infoN);
1023  item->localRef = infoN->functionRef;
1024 
1025  /* Process the queue. */
1026  while (queue->first != NULL) {
1027  item = (LocalQueueItem *) queue->first;
1028  node = item->node;
1029  cuddLevelQueueDequeue(queue,cuddI(dd,node->index));
1030  if (node == skip) continue;
1031  (void) st__lookup(info->table, (const char *)node, (char **)&infoN);
1032  if (item->localRef != infoN->functionRef) {
1033  /* This node is shared. */
1034  continue;
1035  }
1036  savings++;
1037  if (!cuddIsConstant(cuddT(node))) {
1038  item = (LocalQueueItem *) cuddLevelQueueEnqueue(queue,cuddT(node),
1039  cuddI(dd,cuddT(node)->index));
1040  if (item == NULL) return(0);
1041  item->localRef++;
1042  }
1043  if (!Cudd_IsConstant(cuddE(node))) {
1044  item = (LocalQueueItem *) cuddLevelQueueEnqueue(queue,Cudd_Regular(cuddE(node)),
1045  cuddI(dd,Cudd_Regular(cuddE(node))->index));
1046  if (item == NULL) return(0);
1047  item->localRef++;
1048  }
1049  }
1050 
1051 #ifdef DD_DEBUG
1052  /* At the end of a local search the queue should be empty. */
1053  assert(queue->size == 0);
1054 #endif
1055  return(savings);
1056 
1057 } /* end of computeSavings */
cuddLevelQueueDequeue
void cuddLevelQueueDequeue(DdLevelQueue *queue, int level)
Definition: cuddLevelQ.c:354
DdNode
Definition: cudd.h:278
Cudd_IsConstant
#define Cudd_IsConstant(node)
Definition: cudd.h:352
Cudd_Regular
#define Cudd_Regular(node)
Definition: cudd.h:397
cuddLevelQueueEnqueue
void * cuddLevelQueueEnqueue(DdLevelQueue *queue, void *key, int level)
Definition: cuddLevelQ.c:282
cuddIsConstant
#define cuddIsConstant(node)
Definition: cuddInt.h:620
ApproxInfo::table
st__table * table
Definition: cuddApprox.c:135
cuddT
#define cuddT(node)
Definition: cuddInt.h:636
DdLevelQueue::first
void * first
Definition: cuddInt.h:509
cuddI
#define cuddI(dd, index)
Definition: cuddInt.h:686
st__lookup
int st__lookup(st__table *table, const char *key, char **value)
Definition: st.c:114
DdNode::index
DdHalfWord index
Definition: cudd.h:279
cuddE
#define cuddE(node)
Definition: cuddInt.h:652
assert
#define assert(ex)
Definition: util_old.h:213
LocalQueueItem::node
DdNode * node
Definition: cuddApprox.c:158
DdNode* Cudd_BiasedOverApprox ( DdManager *  dd,
DdNode *  f,
DdNode *  b,
int  numVars,
int  threshold,
double  quality1,
double  quality0 
)

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]

Definition at line 463 of file cuddApprox.c.

471 {
472  DdNode *subset, *g;
473 
474  g = Cudd_Not(f);
475  do {
476  dd->reordered = 0;
477  subset = cuddBiasedUnderApprox(dd, g, b, numVars, threshold, quality1,
478  quality0);
479  } while (dd->reordered == 1);
480 
481  return(Cudd_NotCond(subset, (subset != NULL)));
482 
483 } /* end of Cudd_BiasedOverApprox */
DdNode
Definition: cudd.h:278
Cudd_Not
#define Cudd_Not(node)
Definition: cudd.h:367
cuddBiasedUnderApprox
DdNode * cuddBiasedUnderApprox(DdManager *dd, DdNode *f, DdNode *b, int numVars, int threshold, double quality1, double quality0)
Definition: cuddApprox.c:691
DdManager::reordered
int reordered
Definition: cuddInt.h:409
Cudd_NotCond
#define Cudd_NotCond(node, c)
Definition: cudd.h:383
DdNode* Cudd_BiasedUnderApprox ( DdManager *  dd,
DdNode *  f,
DdNode *  b,
int  numVars,
int  threshold,
double  quality1,
double  quality0 
)

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]

Definition at line 413 of file cuddApprox.c.

421 {
422  DdNode *subset;
423 
424  do {
425  dd->reordered = 0;
426  subset = cuddBiasedUnderApprox(dd, f, b, numVars, threshold, quality1,
427  quality0);
428  } while (dd->reordered == 1);
429 
430  return(subset);
431 
432 } /* end of Cudd_BiasedUnderApprox */
DdNode
Definition: cudd.h:278
cuddBiasedUnderApprox
DdNode * cuddBiasedUnderApprox(DdManager *dd, DdNode *f, DdNode *b, int numVars, int threshold, double quality1, double quality0)
Definition: cuddApprox.c:691
DdManager::reordered
int reordered
Definition: cuddInt.h:409
DdNode* Cudd_OverApprox ( DdManager *  dd,
DdNode *  f,
int  numVars,
int  threshold,
int  safe,
double  quality 
)

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]

Definition at line 275 of file cuddApprox.c.

282 {
283  DdNode *subset, *g;
284 
285  g = Cudd_Not(f);
286  do {
287  dd->reordered = 0;
288  subset = cuddUnderApprox(dd, g, numVars, threshold, safe, quality);
289  } while (dd->reordered == 1);
290 
291  return(Cudd_NotCond(subset, (subset != NULL)));
292 
293 } /* end of Cudd_OverApprox */
DdNode
Definition: cudd.h:278
Cudd_Not
#define Cudd_Not(node)
Definition: cudd.h:367
cuddUnderApprox
DdNode * cuddUnderApprox(DdManager *dd, DdNode *f, int numVars, int threshold, int safe, double quality)
Definition: cuddApprox.c:511
DdManager::reordered
int reordered
Definition: cuddInt.h:409
Cudd_NotCond
#define Cudd_NotCond(node, c)
Definition: cudd.h:383
DdNode* Cudd_RemapOverApprox ( DdManager *  dd,
DdNode *  f,
int  numVars,
int  threshold,
double  quality 
)

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]

Definition at line 366 of file cuddApprox.c.

372 {
373  DdNode *subset, *g;
374 
375  g = Cudd_Not(f);
376  do {
377  dd->reordered = 0;
378  subset = cuddRemapUnderApprox(dd, g, numVars, threshold, quality);
379  } while (dd->reordered == 1);
380 
381  return(Cudd_NotCond(subset, (subset != NULL)));
382 
383 } /* end of Cudd_RemapOverApprox */
DdNode
Definition: cudd.h:278
Cudd_Not
#define Cudd_Not(node)
Definition: cudd.h:367
DdManager::reordered
int reordered
Definition: cuddInt.h:409
cuddRemapUnderApprox
DdNode * cuddRemapUnderApprox(DdManager *dd, DdNode *f, int numVars, int threshold, double quality)
Definition: cuddApprox.c:601
Cudd_NotCond
#define Cudd_NotCond(node, c)
Definition: cudd.h:383
DdNode* Cudd_RemapUnderApprox ( DdManager *  dd,
DdNode *  f,
int  numVars,
int  threshold,
double  quality 
)

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]

Definition at line 320 of file cuddApprox.c.

326 {
327  DdNode *subset;
328 
329  do {
330  dd->reordered = 0;
331  subset = cuddRemapUnderApprox(dd, f, numVars, threshold, quality);
332  } while (dd->reordered == 1);
333 
334  return(subset);
335 
336 } /* end of Cudd_RemapUnderApprox */
DdNode
Definition: cudd.h:278
DdManager::reordered
int reordered
Definition: cuddInt.h:409
cuddRemapUnderApprox
DdNode * cuddRemapUnderApprox(DdManager *dd, DdNode *f, int numVars, int threshold, double quality)
Definition: cuddApprox.c:601
DdNode* Cudd_UnderApprox ( DdManager *  dd,
DdNode *  f,
int  numVars,
int  threshold,
int  safe,
double  quality 
)

AutomaticEnd 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]

Definition at line 228 of file cuddApprox.c.

235 {
236  DdNode *subset;
237 
238  do {
239  dd->reordered = 0;
240  subset = cuddUnderApprox(dd, f, numVars, threshold, safe, quality);
241  } while (dd->reordered == 1);
242 
243  return(subset);
244 
245 } /* end of Cudd_UnderApprox */
DdNode
Definition: cudd.h:278
cuddUnderApprox
DdNode * cuddUnderApprox(DdManager *dd, DdNode *f, int numVars, int threshold, int safe, double quality)
Definition: cuddApprox.c:511
DdManager::reordered
int reordered
Definition: cuddInt.h:409
DdNode* cuddBiasedUnderApprox ( DdManager *  dd,
DdNode *  f,
DdNode *  b,
int  numVars,
int  threshold,
double  quality1,
double  quality0 
)

Function********************************************************************

Synopsis [Applies the biased remapping underappoximation algorithm.]

Description [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.]

SideEffects [None]

SeeAlso [Cudd_BiasedUnderApprox]

Definition at line 691 of file cuddApprox.c.

699 {
700  ApproxInfo *info;
701  DdNode *subset;
702  int result;
703  DdHashTable *cache;
704 
705  if (f == NULL) {
706  fprintf(dd->err, "Cannot subset, nil object\n");
707  dd->errorCode = CUDD_INVALID_ARG;
708  return(NULL);
709  }
710 
711  if (Cudd_IsConstant(f)) {
712  return(f);
713  }
714 
715  /* Create table where node data are accessible via a hash table. */
716  info = gatherInfo(dd, f, numVars, TRUE);
717  if (info == NULL) {
718  (void) fprintf(dd->err, "Out-of-memory; Cannot subset\n");
719  dd->errorCode = CUDD_MEMORY_OUT;
720  return(NULL);
721  }
722 
723  cache = cuddHashTableInit(dd,2,2);
724  result = BAapplyBias(dd, Cudd_Regular(f), b, info, cache);
725  if (result == CARE_ERROR) {
726  (void) fprintf(dd->err, "Out-of-memory; Cannot subset\n");
727  cuddHashTableQuit(cache);
728  ABC_FREE(info->page);
729  st__free_table(info->table);
730  ABC_FREE(info);
731  dd->errorCode = CUDD_MEMORY_OUT;
732  return(NULL);
733  }
734  cuddHashTableQuit(cache);
735 
736  /* Mark nodes that should be replaced by zero. */
737  result = BAmarkNodes(dd, f, info, threshold, quality1, quality0);
738  if (result == 0) {
739  (void) fprintf(dd->err, "Out-of-memory; Cannot subset\n");
740  ABC_FREE(info->page);
741  st__free_table(info->table);
742  ABC_FREE(info);
743  dd->errorCode = CUDD_MEMORY_OUT;
744  return(NULL);
745  }
746 
747  /* Build the result. */
748  subset = RAbuildSubset(dd, f, info);
749 #if 1
750  if (subset && info->size < Cudd_DagSize(subset))
751  (void) fprintf(dd->err, "Wrong prediction: %d versus actual %d\n",
752  info->size, Cudd_DagSize(subset));
753 #endif
754  ABC_FREE(info->page);
755  st__free_table(info->table);
756  ABC_FREE(info);
757 
758 #ifdef DD_DEBUG
759  if (subset != NULL) {
760  cuddRef(subset);
761 #if 0
762  (void) Cudd_DebugCheck(dd);
763  (void) Cudd_CheckKeys(dd);
764 #endif
765  if (!Cudd_bddLeq(dd, subset, f)) {
766  (void) fprintf(dd->err, "Wrong subset\n");
767  }
768  cuddDeref(subset);
769  dd->errorCode = CUDD_INTERNAL_ERROR;
770  }
771 #endif
772  return(subset);
773 
774 } /* end of cuddBiasedUnderApprox */
st__free_table
void st__free_table(st__table *table)
Definition: st.c:81
cuddRef
#define cuddRef(n)
Definition: cuddInt.h:584
cuddDeref
#define cuddDeref(n)
Definition: cuddInt.h:604
DdNode
Definition: cudd.h:278
BAapplyBias
static int BAapplyBias(DdManager *dd, DdNode *f, DdNode *b, ApproxInfo *info, DdHashTable *cache)
Definition: cuddApprox.c:2138
CARE_ERROR
#define CARE_ERROR
Definition: cuddApprox.c:102
Cudd_IsConstant
#define Cudd_IsConstant(node)
Definition: cudd.h:352
Cudd_Regular
#define Cudd_Regular(node)
Definition: cudd.h:397
DdManager::err
FILE * err
Definition: cuddInt.h:442
gatherInfo
static ApproxInfo * gatherInfo(DdManager *dd, DdNode *node, int numVars, int parity)
Definition: cuddApprox.c:907
BAmarkNodes
static int BAmarkNodes(DdManager *dd, DdNode *f, ApproxInfo *info, int threshold, double quality1, double quality0)
Definition: cuddApprox.c:1673
Cudd_DebugCheck
int Cudd_DebugCheck(DdManager *table)
Definition: cuddCheck.c:142
ApproxInfo::table
st__table * table
Definition: cuddApprox.c:135
cuddHashTableQuit
void cuddHashTableQuit(DdHashTable *hash)
Definition: cuddLCache.c:595
TRUE
#define TRUE
Definition: cudd.h:88
Cudd_bddLeq
int Cudd_bddLeq(DdManager *dd, DdNode *f, DdNode *g)
Definition: cuddBddIte.c:536
ABC_FREE
#define ABC_FREE(obj)
Definition: abc_global.h:232
Cudd_CheckKeys
int Cudd_CheckKeys(DdManager *table)
Definition: cuddCheck.c:458
RAbuildSubset
static DdNode * RAbuildSubset(DdManager *dd, DdNode *node, ApproxInfo *info)
Definition: cuddApprox.c:1990
cuddHashTableInit
DdHashTable * cuddHashTableInit(DdManager *manager, unsigned int keySize, unsigned int initSize)
Definition: cuddLCache.c:538
ApproxInfo::page
NodeData * page
Definition: cuddApprox.c:134
result
static int result
Definition: cuddGenetic.c:125
DdManager::errorCode
Cudd_ErrorType errorCode
Definition: cuddInt.h:447
Cudd_DagSize
int Cudd_DagSize(DdNode *node)
Definition: cuddUtil.c:442
DdNode* cuddRemapUnderApprox ( DdManager *  dd,
DdNode *  f,
int  numVars,
int  threshold,
double  quality 
)

Function********************************************************************

Synopsis [Applies the remapping underappoximation algorithm.]

Description [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.]

SideEffects [None]

SeeAlso [Cudd_RemapUnderApprox]

Definition at line 601 of file cuddApprox.c.

607 {
608  ApproxInfo *info;
609  DdNode *subset;
610  int result;
611 
612  if (f == NULL) {
613  fprintf(dd->err, "Cannot subset, nil object\n");
614  dd->errorCode = CUDD_INVALID_ARG;
615  return(NULL);
616  }
617 
618  if (Cudd_IsConstant(f)) {
619  return(f);
620  }
621 
622  /* Create table where node data are accessible via a hash table. */
623  info = gatherInfo(dd, f, numVars, TRUE);
624  if (info == NULL) {
625  (void) fprintf(dd->err, "Out-of-memory; Cannot subset\n");
626  dd->errorCode = CUDD_MEMORY_OUT;
627  return(NULL);
628  }
629 
630  /* Mark nodes that should be replaced by zero. */
631  result = RAmarkNodes(dd, f, info, threshold, quality);
632  if (result == 0) {
633  (void) fprintf(dd->err, "Out-of-memory; Cannot subset\n");
634  ABC_FREE(info->page);
635  st__free_table(info->table);
636  ABC_FREE(info);
637  dd->errorCode = CUDD_MEMORY_OUT;
638  return(NULL);
639  }
640 
641  /* Build the result. */
642  subset = RAbuildSubset(dd, f, info);
643 #if 1
644  if (subset && info->size < Cudd_DagSize(subset))
645  (void) fprintf(dd->err, "Wrong prediction: %d versus actual %d\n",
646  info->size, Cudd_DagSize(subset));
647 #endif
648  ABC_FREE(info->page);
649  st__free_table(info->table);
650  ABC_FREE(info);
651 
652 #ifdef DD_DEBUG
653  if (subset != NULL) {
654  cuddRef(subset);
655 #if 0
656  (void) Cudd_DebugCheck(dd);
657  (void) Cudd_CheckKeys(dd);
658 #endif
659  if (!Cudd_bddLeq(dd, subset, f)) {
660  (void) fprintf(dd->err, "Wrong subset\n");
661  }
662  cuddDeref(subset);
663  dd->errorCode = CUDD_INTERNAL_ERROR;
664  }
665 #endif
666  return(subset);
667 
668 } /* end of cuddRemapUnderApprox */
st__free_table
void st__free_table(st__table *table)
Definition: st.c:81
cuddRef
#define cuddRef(n)
Definition: cuddInt.h:584
cuddDeref
#define cuddDeref(n)
Definition: cuddInt.h:604
DdNode
Definition: cudd.h:278
Cudd_IsConstant
#define Cudd_IsConstant(node)
Definition: cudd.h:352
DdManager::err
FILE * err
Definition: cuddInt.h:442
gatherInfo
static ApproxInfo * gatherInfo(DdManager *dd, DdNode *node, int numVars, int parity)
Definition: cuddApprox.c:907
Cudd_DebugCheck
int Cudd_DebugCheck(DdManager *table)
Definition: cuddCheck.c:142
ApproxInfo::table
st__table * table
Definition: cuddApprox.c:135
TRUE
#define TRUE
Definition: cudd.h:88
RAmarkNodes
static int RAmarkNodes(DdManager *dd, DdNode *f, ApproxInfo *info, int threshold, double quality)
Definition: cuddApprox.c:1371
Cudd_bddLeq
int Cudd_bddLeq(DdManager *dd, DdNode *f, DdNode *g)
Definition: cuddBddIte.c:536
ABC_FREE
#define ABC_FREE(obj)
Definition: abc_global.h:232
Cudd_CheckKeys
int Cudd_CheckKeys(DdManager *table)
Definition: cuddCheck.c:458
RAbuildSubset
static DdNode * RAbuildSubset(DdManager *dd, DdNode *node, ApproxInfo *info)
Definition: cuddApprox.c:1990
ApproxInfo::page
NodeData * page
Definition: cuddApprox.c:134
result
static int result
Definition: cuddGenetic.c:125
DdManager::errorCode
Cudd_ErrorType errorCode
Definition: cuddInt.h:447
Cudd_DagSize
int Cudd_DagSize(DdNode *node)
Definition: cuddUtil.c:442
DdNode* cuddUnderApprox ( DdManager *  dd,
DdNode *  f,
int  numVars,
int  threshold,
int  safe,
double  quality 
)

Function********************************************************************

Synopsis [Applies Tom Shiple's underappoximation algorithm.]

Description [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.]

SideEffects [None]

SeeAlso [Cudd_UnderApprox]

Definition at line 511 of file cuddApprox.c.

518 {
519  ApproxInfo *info;
520  DdNode *subset;
521  int result;
522 
523  if (f == NULL) {
524  fprintf(dd->err, "Cannot subset, nil object\n");
525  return(NULL);
526  }
527 
528  if (Cudd_IsConstant(f)) {
529  return(f);
530  }
531 
532  /* Create table where node data are accessible via a hash table. */
533  info = gatherInfo(dd, f, numVars, safe);
534  if (info == NULL) {
535  (void) fprintf(dd->err, "Out-of-memory; Cannot subset\n");
536  dd->errorCode = CUDD_MEMORY_OUT;
537  return(NULL);
538  }
539 
540  /* Mark nodes that should be replaced by zero. */
541  result = UAmarkNodes(dd, f, info, threshold, safe, quality);
542  if (result == 0) {
543  (void) fprintf(dd->err, "Out-of-memory; Cannot subset\n");
544  ABC_FREE(info->page);
545  st__free_table(info->table);
546  ABC_FREE(info);
547  dd->errorCode = CUDD_MEMORY_OUT;
548  return(NULL);
549  }
550 
551  /* Build the result. */
552  subset = UAbuildSubset(dd, f, info);
553 #if 1
554  if (subset && info->size < Cudd_DagSize(subset))
555  (void) fprintf(dd->err, "Wrong prediction: %d versus actual %d\n",
556  info->size, Cudd_DagSize(subset));
557 #endif
558  ABC_FREE(info->page);
559  st__free_table(info->table);
560  ABC_FREE(info);
561 
562 #ifdef DD_DEBUG
563  if (subset != NULL) {
564  cuddRef(subset);
565 #if 0
566  (void) Cudd_DebugCheck(dd);
567  (void) Cudd_CheckKeys(dd);
568 #endif
569  if (!Cudd_bddLeq(dd, subset, f)) {
570  (void) fprintf(dd->err, "Wrong subset\n");
571  dd->errorCode = CUDD_INTERNAL_ERROR;
572  }
573  cuddDeref(subset);
574  }
575 #endif
576  return(subset);
577 
578 } /* end of cuddUnderApprox */
st__free_table
void st__free_table(st__table *table)
Definition: st.c:81
cuddRef
#define cuddRef(n)
Definition: cuddInt.h:584
UAmarkNodes
static int UAmarkNodes(DdManager *dd, DdNode *f, ApproxInfo *info, int threshold, int safe, double quality)
Definition: cuddApprox.c:1152
cuddDeref
#define cuddDeref(n)
Definition: cuddInt.h:604
DdNode
Definition: cudd.h:278
Cudd_IsConstant
#define Cudd_IsConstant(node)
Definition: cudd.h:352
DdManager::err
FILE * err
Definition: cuddInt.h:442
UAbuildSubset
static DdNode * UAbuildSubset(DdManager *dd, DdNode *node, ApproxInfo *info)
Definition: cuddApprox.c:1276
gatherInfo
static ApproxInfo * gatherInfo(DdManager *dd, DdNode *node, int numVars, int parity)
Definition: cuddApprox.c:907
Cudd_DebugCheck
int Cudd_DebugCheck(DdManager *table)
Definition: cuddCheck.c:142
ApproxInfo::table
st__table * table
Definition: cuddApprox.c:135
Cudd_bddLeq
int Cudd_bddLeq(DdManager *dd, DdNode *f, DdNode *g)
Definition: cuddBddIte.c:536
ABC_FREE
#define ABC_FREE(obj)
Definition: abc_global.h:232
Cudd_CheckKeys
int Cudd_CheckKeys(DdManager *table)
Definition: cuddCheck.c:458
ApproxInfo::page
NodeData * page
Definition: cuddApprox.c:134
result
static int result
Definition: cuddGenetic.c:125
DdManager::errorCode
Cudd_ErrorType errorCode
Definition: cuddInt.h:447
Cudd_DagSize
int Cudd_DagSize(DdNode *node)
Definition: cuddUtil.c:442
static ApproxInfo * gatherInfo ( DdManager *  dd,
DdNode *  node,
int  numVars,
int  parity 
)
static

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]

Definition at line 907 of file cuddApprox.c.

912 {
913  ApproxInfo *info;
914  NodeData *infoTop;
915 
916  /* If user did not give numVars value, set it to the maximum
917  ** exponent that the pow function can take. The -1 is due to the
918  ** discrepancy in the value that pow takes and the value that
919  ** log gives.
920  */
921  if (numVars == 0) {
922  numVars = DBL_MAX_EXP - 1;
923  }
924 
925  info = ABC_ALLOC(ApproxInfo,1);
926  if (info == NULL) {
927  dd->errorCode = CUDD_MEMORY_OUT;
928  return(NULL);
929  }
930  info->max = pow(2.0,(double) numVars);
931  info->one = DD_ONE(dd);
932  info->zero = Cudd_Not(info->one);
933  info->size = Cudd_DagSize(node);
934  /* All the information gathered will be stored in a contiguous
935  ** piece of memory, which is allocated here. This can be done
936  ** efficiently because we have counted the number of nodes of the
937  ** BDD. info->index points to the next available entry in the array
938  ** that stores the per-node information. */
939  info->page = ABC_ALLOC(NodeData,info->size);
940  if (info->page == NULL) {
941  dd->errorCode = CUDD_MEMORY_OUT;
942  ABC_FREE(info);
943  return(NULL);
944  }
945  memset(info->page, 0, info->size * sizeof(NodeData)); /* clear all page */
946  info->table = st__init_table( st__ptrcmp, st__ptrhash);
947  if (info->table == NULL) {
948  ABC_FREE(info->page);
949  ABC_FREE(info);
950  return(NULL);
951  }
952  /* We visit the DAG in post-order DFS. Hence, the constant node is
953  ** in first position, and the root of the DAG is in last position. */
954 
955  /* Info for the constant node: Initialize only fields different from 0. */
956  if ( st__insert(info->table, (char *)info->one, (char *)info->page) == st__OUT_OF_MEM) {
957  ABC_FREE(info->page);
958  ABC_FREE(info);
959  st__free_table(info->table);
960  return(NULL);
961  }
962  info->page[0].mintermsP = info->max;
963  info->index = 1;
964 
965  infoTop = gatherInfoAux(node,info,parity);
966  if (infoTop == NULL) {
967  ABC_FREE(info->page);
968  st__free_table(info->table);
969  ABC_FREE(info);
970  return(NULL);
971  }
972  if (Cudd_IsComplement(node)) {
973  info->minterms = infoTop->mintermsN;
974  } else {
975  info->minterms = infoTop->mintermsP;
976  }
977 
978  infoTop->functionRef = 1;
979  return(info);
980 
981 } /* end of gatherInfo */
memset
char * memset()
st__free_table
void st__free_table(st__table *table)
Definition: st.c:81
Cudd_Not
#define Cudd_Not(node)
Definition: cudd.h:367
gatherInfoAux
static NodeData * gatherInfoAux(DdNode *node, ApproxInfo *info, int parity)
Definition: cuddApprox.c:837
st__insert
int st__insert(st__table *table, const char *key, char *value)
Definition: st.c:171
st__ptrcmp
int st__ptrcmp(const char *, const char *)
Definition: st.c:480
ApproxInfo::max
double max
Definition: cuddApprox.c:137
ApproxInfo::minterms
double minterms
Definition: cuddApprox.c:139
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
DBL_MAX_EXP
#define DBL_MAX_EXP
Definition: cuddApprox.c:79
NodeData::functionRef
int functionRef
Definition: cuddApprox.c:123
NodeData::mintermsP
double mintermsP
Definition: cuddApprox.c:121
ApproxInfo::zero
DdNode * zero
Definition: cuddApprox.c:133
st__init_table
st__table * st__init_table(st__compare_func_type compare, st__hash_func_type hash)
Definition: st.c:72
Cudd_IsComplement
#define Cudd_IsComplement(node)
Definition: cudd.h:425
NodeData::mintermsN
double mintermsN
Definition: cuddApprox.c:122
ApproxInfo::one
DdNode * one
Definition: cuddApprox.c:132
ApproxInfo::table
st__table * table
Definition: cuddApprox.c:135
st__OUT_OF_MEM
#define st__OUT_OF_MEM
Definition: st.h:113
ABC_FREE
#define ABC_FREE(obj)
Definition: abc_global.h:232
ApproxInfo::page
NodeData * page
Definition: cuddApprox.c:134
DD_ONE
#define DD_ONE(dd)
Definition: cuddInt.h:911
DdManager::errorCode
Cudd_ErrorType errorCode
Definition: cuddInt.h:447
st__ptrhash
int st__ptrhash(const char *, int)
Definition: st.c:468
Cudd_DagSize
int Cudd_DagSize(DdNode *node)
Definition: cuddUtil.c:442
static NodeData * gatherInfoAux ( DdNode *  node,
ApproxInfo *  info,
int  parity 
)
static

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]

Definition at line 837 of file cuddApprox.c.

841 {
842  DdNode *N, *Nt, *Ne;
843  NodeData *infoN, *infoT, *infoE;
844 
845  N = Cudd_Regular(node);
846 
847  /* Check whether entry for this node exists. */
848  if ( st__lookup(info->table, (const char *)N, (char **)&infoN)) {
849  if (parity) {
850  /* Update parity and propagate. */
851  updateParity(N, info, 1 + (int) Cudd_IsComplement(node));
852  }
853  return(infoN);
854  }
855 
856  /* Compute the cofactors. */
857  Nt = Cudd_NotCond(cuddT(N), N != node);
858  Ne = Cudd_NotCond(cuddE(N), N != node);
859 
860  infoT = gatherInfoAux(Nt, info, parity);
861  if (infoT == NULL) return(NULL);
862  infoE = gatherInfoAux(Ne, info, parity);
863  if (infoE == NULL) return(NULL);
864 
865  infoT->functionRef++;
866  infoE->functionRef++;
867 
868  /* Point to the correct location in the page. */
869  infoN = &(info->page[info->index++]);
870  infoN->parity |= (short) (1 + Cudd_IsComplement(node));
871 
872  infoN->mintermsP = infoT->mintermsP/2;
873  infoN->mintermsN = infoT->mintermsN/2;
874  if (Cudd_IsComplement(Ne) ^ Cudd_IsComplement(node)) {
875  infoN->mintermsP += infoE->mintermsN/2;
876  infoN->mintermsN += infoE->mintermsP/2;
877  } else {
878  infoN->mintermsP += infoE->mintermsP/2;
879  infoN->mintermsN += infoE->mintermsN/2;
880  }
881 
882  /* Insert entry for the node in the table. */
883  if ( st__insert(info->table,(char *)N, (char *)infoN) == st__OUT_OF_MEM) {
884  return(NULL);
885  }
886  return(infoN);
887 
888 } /* end of gatherInfoAux */
DdNode
Definition: cudd.h:278
gatherInfoAux
static NodeData * gatherInfoAux(DdNode *node, ApproxInfo *info, int parity)
Definition: cuddApprox.c:837
st__insert
int st__insert(st__table *table, const char *key, char *value)
Definition: st.c:171
Cudd_Regular
#define Cudd_Regular(node)
Definition: cudd.h:397
NodeData::functionRef
int functionRef
Definition: cuddApprox.c:123
NodeData::mintermsP
double mintermsP
Definition: cuddApprox.c:121
Cudd_IsComplement
#define Cudd_IsComplement(node)
Definition: cudd.h:425
NodeData::mintermsN
double mintermsN
Definition: cuddApprox.c:122
ApproxInfo::table
st__table * table
Definition: cuddApprox.c:135
cuddT
#define cuddT(node)
Definition: cuddInt.h:636
st__OUT_OF_MEM
#define st__OUT_OF_MEM
Definition: st.h:113
st__lookup
int st__lookup(st__table *table, const char *key, char **value)
Definition: st.c:114
NodeData::parity
short int parity
Definition: cuddApprox.c:126
cuddE
#define cuddE(node)
Definition: cuddInt.h:652
Cudd_NotCond
#define Cudd_NotCond(node, c)
Definition: cudd.h:383
updateParity
static void updateParity(DdNode *node, ApproxInfo *info, int newparity)
Definition: cuddApprox.c:795
ApproxInfo::page
NodeData * page
Definition: cuddApprox.c:134
static DdNode * RAbuildSubset ( DdManager *  dd,
DdNode *  node,
ApproxInfo *  info 
)
static

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]

Definition at line 1990 of file cuddApprox.c.

1994 {
1995  DdNode *Nt, *Ne, *N, *t, *e, *r;
1996  NodeData *infoN;
1997 
1998  if (Cudd_IsConstant(node))
1999  return(node);
2000 
2001  N = Cudd_Regular(node);
2002 
2003  Nt = Cudd_NotCond(cuddT(N), Cudd_IsComplement(node));
2004  Ne = Cudd_NotCond(cuddE(N), Cudd_IsComplement(node));
2005 
2006  if ( st__lookup(info->table, (const char *)N, (char **)&infoN)) {
2007  if (N == node ) {
2008  if (infoN->resultP != NULL) {
2009  return(infoN->resultP);
2010  }
2011  } else {
2012  if (infoN->resultN != NULL) {
2013  return(infoN->resultN);
2014  }
2015  }
2016  if (infoN->replace == REPLACE_T) {
2017  r = RAbuildSubset(dd, Ne, info);
2018  return(r);
2019  } else if (infoN->replace == REPLACE_E) {
2020  r = RAbuildSubset(dd, Nt, info);
2021  return(r);
2022  } else if (infoN->replace == REPLACE_N) {
2023  return(info->zero);
2024  } else if (infoN->replace == REPLACE_TT) {
2025  DdNode *Ntt = Cudd_NotCond(cuddT(cuddT(N)),
2026  Cudd_IsComplement(node));
2027  int index = cuddT(N)->index;
2028  e = info->zero;
2029  t = RAbuildSubset(dd, Ntt, info);
2030  if (t == NULL) {
2031  return(NULL);
2032  }
2033  cuddRef(t);
2034  if (Cudd_IsComplement(t)) {
2035  t = Cudd_Not(t);
2036  e = Cudd_Not(e);
2037  r = (t == e) ? t : cuddUniqueInter(dd, index, t, e);
2038  if (r == NULL) {
2039  Cudd_RecursiveDeref(dd, t);
2040  return(NULL);
2041  }
2042  r = Cudd_Not(r);
2043  } else {
2044  r = (t == e) ? t : cuddUniqueInter(dd, index, t, e);
2045  if (r == NULL) {
2046  Cudd_RecursiveDeref(dd, t);
2047  return(NULL);
2048  }
2049  }
2050  cuddDeref(t);
2051  return(r);
2052  } else if (infoN->replace == REPLACE_TE) {
2053  DdNode *Nte = Cudd_NotCond(cuddE(cuddT(N)),
2054  Cudd_IsComplement(node));
2055  int index = cuddT(N)->index;
2056  t = info->one;
2057  e = RAbuildSubset(dd, Nte, info);
2058  if (e == NULL) {
2059  return(NULL);
2060  }
2061  cuddRef(e);
2062  e = Cudd_Not(e);
2063  r = (t == e) ? t : cuddUniqueInter(dd, index, t, e);
2064  if (r == NULL) {
2065  Cudd_RecursiveDeref(dd, e);
2066  return(NULL);
2067  }
2068  r =Cudd_Not(r);
2069  cuddDeref(e);
2070  return(r);
2071  }
2072  } else {
2073  (void) fprintf(dd->err,
2074  "Something is wrong, ought to be in info table\n");
2075  dd->errorCode = CUDD_INTERNAL_ERROR;
2076  return(NULL);
2077  }
2078 
2079  t = RAbuildSubset(dd, Nt, info);
2080  if (t == NULL) {
2081  return(NULL);
2082  }
2083  cuddRef(t);
2084 
2085  e = RAbuildSubset(dd, Ne, info);
2086  if (e == NULL) {
2087  Cudd_RecursiveDeref(dd,t);
2088  return(NULL);
2089  }
2090  cuddRef(e);
2091 
2092  if (Cudd_IsComplement(t)) {
2093  t = Cudd_Not(t);
2094  e = Cudd_Not(e);
2095  r = (t == e) ? t : cuddUniqueInter(dd, N->index, t, e);
2096  if (r == NULL) {
2097  Cudd_RecursiveDeref(dd, e);
2098  Cudd_RecursiveDeref(dd, t);
2099  return(NULL);
2100  }
2101  r = Cudd_Not(r);
2102  } else {
2103  r = (t == e) ? t : cuddUniqueInter(dd, N->index, t, e);
2104  if (r == NULL) {
2105  Cudd_RecursiveDeref(dd, e);
2106  Cudd_RecursiveDeref(dd, t);
2107  return(NULL);
2108  }
2109  }
2110  cuddDeref(t);
2111  cuddDeref(e);
2112 
2113  if (N == node) {
2114  infoN->resultP = r;
2115  } else {
2116  infoN->resultN = r;
2117  }
2118 
2119  return(r);
2120 
2121 } /* end of RAbuildSubset */
cuddRef
#define cuddRef(n)
Definition: cuddInt.h:584
cuddDeref
#define cuddDeref(n)
Definition: cuddInt.h:604
Cudd_RecursiveDeref
void Cudd_RecursiveDeref(DdManager *table, DdNode *n)
Definition: cuddRef.c:154
DdNode
Definition: cudd.h:278
Cudd_Not
#define Cudd_Not(node)
Definition: cudd.h:367
Cudd_IsConstant
#define Cudd_IsConstant(node)
Definition: cudd.h:352
Cudd_Regular
#define Cudd_Regular(node)
Definition: cudd.h:397
DdManager::err
FILE * err
Definition: cuddInt.h:442
REPLACE_TE
#define REPLACE_TE
Definition: cuddApprox.c:97
REPLACE_E
#define REPLACE_E
Definition: cuddApprox.c:94
NodeData::resultP
DdNode * resultP
Definition: cuddApprox.c:127
NodeData::resultN
DdNode * resultN
Definition: cuddApprox.c:128
ApproxInfo::zero
DdNode * zero
Definition: cuddApprox.c:133
Cudd_IsComplement
#define Cudd_IsComplement(node)
Definition: cudd.h:425
REPLACE_N
#define REPLACE_N
Definition: cuddApprox.c:95
REPLACE_TT
#define REPLACE_TT
Definition: cuddApprox.c:96
ApproxInfo::one
DdNode * one
Definition: cuddApprox.c:132
ApproxInfo::table
st__table * table
Definition: cuddApprox.c:135
cuddT
#define cuddT(node)
Definition: cuddInt.h:636
st__lookup
int st__lookup(st__table *table, const char *key, char **value)
Definition: st.c:114
REPLACE_T
#define REPLACE_T
Definition: cuddApprox.c:93
DdNode::index
DdHalfWord index
Definition: cudd.h:279
RAbuildSubset
static DdNode * RAbuildSubset(DdManager *dd, DdNode *node, ApproxInfo *info)
Definition: cuddApprox.c:1990
cuddE
#define cuddE(node)
Definition: cuddInt.h:652
Cudd_NotCond
#define Cudd_NotCond(node, c)
Definition: cudd.h:383
DdManager::errorCode
Cudd_ErrorType errorCode
Definition: cuddInt.h:447
cuddUniqueInter
DdNode * cuddUniqueInter(DdManager *unique, int index, DdNode *T, DdNode *E)
Definition: cuddTable.c:1128
NodeData::replace
char replace
Definition: cuddApprox.c:125
static int RAmarkNodes ( DdManager *  dd,
DdNode *  f,
ApproxInfo *  info,
int  threshold,
double  quality 
)
static

Function********************************************************************

Synopsis [Marks nodes for remapping.]

Description [Marks nodes for remapping. Returns 1 if successful; 0 otherwise.]

SideEffects [None]

SeeAlso [cuddRemapUnderApprox]

Definition at line 1371 of file cuddApprox.c.

1377 {
1378  DdLevelQueue *queue;
1379  DdLevelQueue *localQueue;
1380  NodeData *infoN, *infoT, *infoE;
1381  GlobalQueueItem *item;
1382  DdNode *node, *T, *E;
1383  DdNode *shared; /* grandchild shared by the two children of node */
1384  double numOnset;
1385  double impact, impactP, impactN;
1386  double minterms;
1387  int savings;
1388  int replace;
1389 
1390 #if 0
1391  (void) fprintf(dd->out,"initial size = %d initial minterms = %g\n",
1392  info->size, info->minterms);
1393 #endif
1394  queue = cuddLevelQueueInit(dd->size,sizeof(GlobalQueueItem),info->size);
1395  if (queue == NULL) {
1396  return(0);
1397  }
1398  localQueue = cuddLevelQueueInit(dd->size,sizeof(LocalQueueItem),
1399  dd->initSlots);
1400  if (localQueue == NULL) {
1401  cuddLevelQueueQuit(queue);
1402  return(0);
1403  }
1404  /* Enqueue regular pointer to root and initialize impact. */
1405  node = Cudd_Regular(f);
1406  item = (GlobalQueueItem *)
1407  cuddLevelQueueEnqueue(queue,node,cuddI(dd,node->index));
1408  if (item == NULL) {
1409  cuddLevelQueueQuit(queue);
1410  cuddLevelQueueQuit(localQueue);
1411  return(0);
1412  }
1413  if (Cudd_IsComplement(f)) {
1414  item->impactP = 0.0;
1415  item->impactN = 1.0;
1416  } else {
1417  item->impactP = 1.0;
1418  item->impactN = 0.0;
1419  }
1420  /* The nodes retrieved here are guaranteed to be non-terminal.
1421  ** The initial node is not terminal because constant nodes are
1422  ** dealt with in the calling procedure. Subsequent nodes are inserted
1423  ** only if they are not terminal. */
1424  while (queue->first != NULL) {
1425  /* If the size of the subset is below the threshold, quit. */
1426  if (info->size <= threshold)
1427  break;
1428  item = (GlobalQueueItem *) queue->first;
1429  node = item->node;
1430 #ifdef DD_DEBUG
1431  assert(item->impactP >= 0 && item->impactP <= 1.0);
1432  assert(item->impactN >= 0 && item->impactN <= 1.0);
1433  assert(!Cudd_IsComplement(node));
1434  assert(!Cudd_IsConstant(node));
1435 #endif
1436  if (! st__lookup(info->table, (const char *)node, (char **)&infoN)) {
1437  cuddLevelQueueQuit(queue);
1438  cuddLevelQueueQuit(localQueue);
1439  return(0);
1440  }
1441 #ifdef DD_DEBUG
1442  assert(infoN->parity >= 1 && infoN->parity <= 3);
1443 #endif
1444  if (infoN->parity == 3) {
1445  /* This node can be reached through paths of different parity.
1446  ** It is not safe to replace it, because remapping will give
1447  ** an incorrect result, while replacement by 0 may cause node
1448  ** splitting. */
1449  cuddLevelQueueDequeue(queue,cuddI(dd,node->index));
1450  continue;
1451  }
1452  T = cuddT(node);
1453  E = cuddE(node);
1454  shared = NULL;
1455  impactP = item->impactP;
1456  impactN = item->impactN;
1457  if (Cudd_bddLeq(dd,T,E)) {
1458  /* Here we know that E is regular. */
1459 #ifdef DD_DEBUG
1460  assert(!Cudd_IsComplement(E));
1461 #endif
1462  (void) st__lookup(info->table, (const char *)T, (char **)&infoT);
1463  (void) st__lookup(info->table, (const char *)E, (char **)&infoE);
1464  if (infoN->parity == 1) {
1465  impact = impactP;
1466  minterms = infoE->mintermsP/2.0 - infoT->mintermsP/2.0;
1467  if (infoE->functionRef == 1 && !Cudd_IsConstant(E)) {
1468  savings = 1 + computeSavings(dd,E,NULL,info,localQueue);
1469  if (savings == 1) {
1470  cuddLevelQueueQuit(queue);
1471  cuddLevelQueueQuit(localQueue);
1472  return(0);
1473  }
1474  } else {
1475  savings = 1;
1476  }
1477  replace = REPLACE_E;
1478  } else {
1479 #ifdef DD_DEBUG
1480  assert(infoN->parity == 2);
1481 #endif
1482  impact = impactN;
1483  minterms = infoT->mintermsN/2.0 - infoE->mintermsN/2.0;
1484  if (infoT->functionRef == 1 && !Cudd_IsConstant(T)) {
1485  savings = 1 + computeSavings(dd,T,NULL,info,localQueue);
1486  if (savings == 1) {
1487  cuddLevelQueueQuit(queue);
1488  cuddLevelQueueQuit(localQueue);
1489  return(0);
1490  }
1491  } else {
1492  savings = 1;
1493  }
1494  replace = REPLACE_T;
1495  }
1496  numOnset = impact * minterms;
1497  } else if (Cudd_bddLeq(dd,E,T)) {
1498  /* Here E may be complemented. */
1499  DdNode *Ereg = Cudd_Regular(E);
1500  (void) st__lookup(info->table, (const char *)T, (char **)&infoT);
1501  (void) st__lookup(info->table, (const char *)Ereg, (char **)&infoE);
1502  if (infoN->parity == 1) {
1503  impact = impactP;
1504  minterms = infoT->mintermsP/2.0 -
1505  ((E == Ereg) ? infoE->mintermsP : infoE->mintermsN)/2.0;
1506  if (infoT->functionRef == 1 && !Cudd_IsConstant(T)) {
1507  savings = 1 + computeSavings(dd,T,NULL,info,localQueue);
1508  if (savings == 1) {
1509  cuddLevelQueueQuit(queue);
1510  cuddLevelQueueQuit(localQueue);
1511  return(0);
1512  }
1513  } else {
1514  savings = 1;
1515  }
1516  replace = REPLACE_T;
1517  } else {
1518 #ifdef DD_DEBUG
1519  assert(infoN->parity == 2);
1520 #endif
1521  impact = impactN;
1522  minterms = ((E == Ereg) ? infoE->mintermsN :
1523  infoE->mintermsP)/2.0 - infoT->mintermsN/2.0;
1524  if (infoE->functionRef == 1 && !Cudd_IsConstant(E)) {
1525  savings = 1 + computeSavings(dd,E,NULL,info,localQueue);
1526  if (savings == 1) {
1527  cuddLevelQueueQuit(queue);
1528  cuddLevelQueueQuit(localQueue);
1529  return(0);
1530  }
1531  } else {
1532  savings = 1;
1533  }
1534  replace = REPLACE_E;
1535  }
1536  numOnset = impact * minterms;
1537  } else {
1538  DdNode *Ereg = Cudd_Regular(E);
1539  DdNode *TT = cuddT(T);
1540  DdNode *ET = Cudd_NotCond(cuddT(Ereg), Cudd_IsComplement(E));
1541  if (T->index == Ereg->index && TT == ET) {
1542  shared = TT;
1543  replace = REPLACE_TT;
1544  } else {
1545  DdNode *TE = cuddE(T);
1546  DdNode *EE = Cudd_NotCond(cuddE(Ereg), Cudd_IsComplement(E));
1547  if (T->index == Ereg->index && TE == EE) {
1548  shared = TE;
1549  replace = REPLACE_TE;
1550  } else {
1551  replace = REPLACE_N;
1552  }
1553  }
1554  numOnset = infoN->mintermsP * impactP + infoN->mintermsN * impactN;
1555  savings = computeSavings(dd,node,shared,info,localQueue);
1556  if (shared != NULL) {
1557  NodeData *infoS;
1558  (void) st__lookup(info->table, (const char *)Cudd_Regular(shared), (char **)&infoS);
1559  if (Cudd_IsComplement(shared)) {
1560  numOnset -= (infoS->mintermsN * impactP +
1561  infoS->mintermsP * impactN)/2.0;
1562  } else {
1563  numOnset -= (infoS->mintermsP * impactP +
1564  infoS->mintermsN * impactN)/2.0;
1565  }
1566  savings--;
1567  }
1568  }
1569 
1570  cuddLevelQueueDequeue(queue,cuddI(dd,node->index));
1571 #if 0
1572  if (replace == REPLACE_T || replace == REPLACE_E)
1573  (void) printf("node %p: impact = %g numOnset = %g savings %d\n",
1574  node, impact, numOnset, savings);
1575  else
1576  (void) printf("node %p: impact = %g/%g numOnset = %g savings %d\n",
1577  node, impactP, impactN, numOnset, savings);
1578 #endif
1579  if ((1 - numOnset / info->minterms) >
1580  quality * (1 - (double) savings / info->size)) {
1581  infoN->replace = (char) replace;
1582  info->size -= savings;
1583  info->minterms -=numOnset;
1584 #if 0
1585  (void) printf("remap(%d): new size = %d new minterms = %g\n",
1586  replace, info->size, info->minterms);
1587 #endif
1588  if (replace == REPLACE_N) {
1589  savings -= updateRefs(dd,node,NULL,info,localQueue);
1590  } else if (replace == REPLACE_T) {
1591  savings -= updateRefs(dd,node,E,info,localQueue);
1592  } else if (replace == REPLACE_E) {
1593  savings -= updateRefs(dd,node,T,info,localQueue);
1594  } else {
1595 #ifdef DD_DEBUG
1596  assert(replace == REPLACE_TT || replace == REPLACE_TE);
1597 #endif
1598  savings -= updateRefs(dd,node,shared,info,localQueue) - 1;
1599  }
1600  assert(savings == 0);
1601  } else {
1602  replace = NOTHING;
1603  }
1604  if (replace == REPLACE_N) continue;
1605  if ((replace == REPLACE_E || replace == NOTHING) &&
1606  !cuddIsConstant(cuddT(node))) {
1607  item = (GlobalQueueItem *) cuddLevelQueueEnqueue(queue,cuddT(node),
1608  cuddI(dd,cuddT(node)->index));
1609  if (replace == REPLACE_E) {
1610  item->impactP += impactP;
1611  item->impactN += impactN;
1612  } else {
1613  item->impactP += impactP/2.0;
1614  item->impactN += impactN/2.0;
1615  }
1616  }
1617  if ((replace == REPLACE_T || replace == NOTHING) &&
1618  !Cudd_IsConstant(cuddE(node))) {
1619  item = (GlobalQueueItem *) cuddLevelQueueEnqueue(queue,Cudd_Regular(cuddE(node)),
1620  cuddI(dd,Cudd_Regular(cuddE(node))->index));
1621  if (Cudd_IsComplement(cuddE(node))) {
1622  if (replace == REPLACE_T) {
1623  item->impactP += impactN;
1624  item->impactN += impactP;
1625  } else {
1626  item->impactP += impactN/2.0;
1627  item->impactN += impactP/2.0;
1628  }
1629  } else {
1630  if (replace == REPLACE_T) {
1631  item->impactP += impactP;
1632  item->impactN += impactN;
1633  } else {
1634  item->impactP += impactP/2.0;
1635  item->impactN += impactN/2.0;
1636  }
1637  }
1638  }
1639  if ((replace == REPLACE_TT || replace == REPLACE_TE) &&
1640  !Cudd_IsConstant(shared)) {
1641  item = (GlobalQueueItem *) cuddLevelQueueEnqueue(queue,Cudd_Regular(shared),
1642  cuddI(dd,Cudd_Regular(shared)->index));
1643  if (Cudd_IsComplement(shared)) {
1644  item->impactP += impactN;
1645  item->impactN += impactP;
1646  } else {
1647  item->impactP += impactP;
1648  item->impactN += impactN;
1649  }
1650  }
1651  }
1652 
1653  cuddLevelQueueQuit(queue);
1654  cuddLevelQueueQuit(localQueue);
1655  return(1);
1656 
1657 } /* end of RAmarkNodes */
cuddLevelQueueDequeue
void cuddLevelQueueDequeue(DdLevelQueue *queue, int level)
Definition: cuddLevelQ.c:354
updateRefs
static int updateRefs(DdManager *dd, DdNode *f, DdNode *skip, ApproxInfo *info, DdLevelQueue *queue)
Definition: cuddApprox.c:1073
DdNode
Definition: cudd.h:278
computeSavings
static int computeSavings(DdManager *dd, DdNode *f, DdNode *skip, ApproxInfo *info, DdLevelQueue *queue)
Definition: cuddApprox.c:1001
DdManager::size
int size
Definition: cuddInt.h:361
Cudd_IsConstant
#define Cudd_IsConstant(node)
Definition: cudd.h:352
Cudd_Regular
#define Cudd_Regular(node)
Definition: cudd.h:397
ApproxInfo::minterms
double minterms
Definition: cuddApprox.c:139
cuddLevelQueueQuit
void cuddLevelQueueQuit(DdLevelQueue *queue)
Definition: cuddLevelQ.c:244
REPLACE_TE
#define REPLACE_TE
Definition: cuddApprox.c:97
REPLACE_E
#define REPLACE_E
Definition: cuddApprox.c:94
GlobalQueueItem::node
DdNode * node
Definition: cuddApprox.c:150
NodeData::mintermsP
double mintermsP
Definition: cuddApprox.c:121
DdManager::initSlots
unsigned int initSlots
Definition: cuddInt.h:379
cuddLevelQueueEnqueue
void * cuddLevelQueueEnqueue(DdLevelQueue *queue, void *key, int level)
Definition: cuddLevelQ.c:282
cuddLevelQueueInit
DdLevelQueue * cuddLevelQueueInit(int levels, int itemSize, int numBuckets)
Definition: cuddLevelQ.c:169
Cudd_IsComplement
#define Cudd_IsComplement(node)
Definition: cudd.h:425
DdManager::out
FILE * out
Definition: cuddInt.h:441
NodeData::mintermsN
double mintermsN
Definition: cuddApprox.c:122
REPLACE_N
#define REPLACE_N
Definition: cuddApprox.c:95
cuddIsConstant
#define cuddIsConstant(node)
Definition: cuddInt.h:620
REPLACE_TT
#define REPLACE_TT
Definition: cuddApprox.c:96
ApproxInfo::table
st__table * table
Definition: cuddApprox.c:135
cuddT
#define cuddT(node)
Definition: cuddInt.h:636
DdLevelQueue::first
void * first
Definition: cuddInt.h:509
cuddI
#define cuddI(dd, index)
Definition: cuddInt.h:686
DD_DEBUG
#define DD_DEBUG
Definition: cuddPriority.c:88
Cudd_bddLeq
int Cudd_bddLeq(DdManager *dd, DdNode *f, DdNode *g)
Definition: cuddBddIte.c:536
st__lookup
int st__lookup(st__table *table, const char *key, char **value)
Definition: st.c:114
REPLACE_T
#define REPLACE_T
Definition: cuddApprox.c:93
NodeData::parity
short int parity
Definition: cuddApprox.c:126
DdNode::index
DdHalfWord index
Definition: cudd.h:279
cuddE
#define cuddE(node)
Definition: cuddInt.h:652
Cudd_NotCond
#define Cudd_NotCond(node, c)
Definition: cudd.h:383
assert
#define assert(ex)
Definition: util_old.h:213
minterms
pset minterms()
NodeData::replace
char replace
Definition: cuddApprox.c:125
NOTHING
#define NOTHING
Definition: cuddApprox.c:92
static DdNode * UAbuildSubset ( DdManager *  dd,
DdNode *  node,
ApproxInfo *  info 
)
static

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]

Definition at line 1276 of file cuddApprox.c.

1280 {
1281 
1282  DdNode *Nt, *Ne, *N, *t, *e, *r;
1283  NodeData *infoN;
1284 
1285  if (Cudd_IsConstant(node))
1286  return(node);
1287 
1288  N = Cudd_Regular(node);
1289 
1290  if ( st__lookup(info->table, (const char *)N, (char **)&infoN)) {
1291  if (infoN->replace == TRUE) {
1292  return(info->zero);
1293  }
1294  if (N == node ) {
1295  if (infoN->resultP != NULL) {
1296  return(infoN->resultP);
1297  }
1298  } else {
1299  if (infoN->resultN != NULL) {
1300  return(infoN->resultN);
1301  }
1302  }
1303  } else {
1304  (void) fprintf(dd->err,
1305  "Something is wrong, ought to be in info table\n");
1306  dd->errorCode = CUDD_INTERNAL_ERROR;
1307  return(NULL);
1308  }
1309 
1310  Nt = Cudd_NotCond(cuddT(N), Cudd_IsComplement(node));
1311  Ne = Cudd_NotCond(cuddE(N), Cudd_IsComplement(node));
1312 
1313  t = UAbuildSubset(dd, Nt, info);
1314  if (t == NULL) {
1315  return(NULL);
1316  }
1317  cuddRef(t);
1318 
1319  e = UAbuildSubset(dd, Ne, info);
1320  if (e == NULL) {
1321  Cudd_RecursiveDeref(dd,t);
1322  return(NULL);
1323  }
1324  cuddRef(e);
1325 
1326  if (Cudd_IsComplement(t)) {
1327  t = Cudd_Not(t);
1328  e = Cudd_Not(e);
1329  r = (t == e) ? t : cuddUniqueInter(dd, N->index, t, e);
1330  if (r == NULL) {
1331  Cudd_RecursiveDeref(dd, e);
1332  Cudd_RecursiveDeref(dd, t);
1333  return(NULL);
1334  }
1335  r = Cudd_Not(r);
1336  } else {
1337  r = (t == e) ? t : cuddUniqueInter(dd, N->index, t, e);
1338  if (r == NULL) {
1339  Cudd_RecursiveDeref(dd, e);
1340  Cudd_RecursiveDeref(dd, t);
1341  return(NULL);
1342  }
1343  }
1344  cuddDeref(t);
1345  cuddDeref(e);
1346 
1347  if (N == node) {
1348  infoN->resultP = r;
1349  } else {
1350  infoN->resultN = r;
1351  }
1352 
1353  return(r);
1354 
1355 } /* end of UAbuildSubset */
cuddRef
#define cuddRef(n)
Definition: cuddInt.h:584
cuddDeref
#define cuddDeref(n)
Definition: cuddInt.h:604
Cudd_RecursiveDeref
void Cudd_RecursiveDeref(DdManager *table, DdNode *n)
Definition: cuddRef.c:154
DdNode
Definition: cudd.h:278
Cudd_Not
#define Cudd_Not(node)
Definition: cudd.h:367
Cudd_IsConstant
#define Cudd_IsConstant(node)
Definition: cudd.h:352
Cudd_Regular
#define Cudd_Regular(node)
Definition: cudd.h:397
DdManager::err
FILE * err
Definition: cuddInt.h:442
UAbuildSubset
static DdNode * UAbuildSubset(DdManager *dd, DdNode *node, ApproxInfo *info)
Definition: cuddApprox.c:1276
NodeData::resultP
DdNode * resultP
Definition: cuddApprox.c:127
NodeData::resultN
DdNode * resultN
Definition: cuddApprox.c:128
ApproxInfo::zero
DdNode * zero
Definition: cuddApprox.c:133
Cudd_IsComplement
#define Cudd_IsComplement(node)
Definition: cudd.h:425
ApproxInfo::table
st__table * table
Definition: cuddApprox.c:135
cuddT
#define cuddT(node)
Definition: cuddInt.h:636
TRUE
#define TRUE
Definition: cudd.h:88
st__lookup
int st__lookup(st__table *table, const char *key, char **value)
Definition: st.c:114
DdNode::index
DdHalfWord index
Definition: cudd.h:279
cuddE
#define cuddE(node)
Definition: cuddInt.h:652
Cudd_NotCond
#define Cudd_NotCond(node, c)
Definition: cudd.h:383
DdManager::errorCode
Cudd_ErrorType errorCode
Definition: cuddInt.h:447
cuddUniqueInter
DdNode * cuddUniqueInter(DdManager *unique, int index, DdNode *T, DdNode *E)
Definition: cuddTable.c:1128
NodeData::replace
char replace
Definition: cuddApprox.c:125
static int UAmarkNodes ( DdManager *  dd,
DdNode *  f,
ApproxInfo *  info,
int  threshold,
int  safe,
double  quality 
)
static

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]

Definition at line 1152 of file cuddApprox.c.

1159 {
1160  DdLevelQueue *queue;
1161  DdLevelQueue *localQueue;
1162  NodeData *infoN;
1163  GlobalQueueItem *item;
1164  DdNode *node;
1165  double numOnset;
1166  double impactP, impactN;
1167  int savings;
1168 
1169 #if 0
1170  (void) printf("initial size = %d initial minterms = %g\n",
1171  info->size, info->minterms);
1172 #endif
1173  queue = cuddLevelQueueInit(dd->size,sizeof(GlobalQueueItem),info->size);
1174  if (queue == NULL) {
1175  return(0);
1176  }
1177  localQueue = cuddLevelQueueInit(dd->size,sizeof(LocalQueueItem),
1178  dd->initSlots);
1179  if (localQueue == NULL) {
1180  cuddLevelQueueQuit(queue);
1181  return(0);
1182  }
1183  node = Cudd_Regular(f);
1184  item = (GlobalQueueItem *) cuddLevelQueueEnqueue(queue,node,cuddI(dd,node->index));
1185  if (item == NULL) {
1186  cuddLevelQueueQuit(queue);
1187  cuddLevelQueueQuit(localQueue);
1188  return(0);
1189  }
1190  if (Cudd_IsComplement(f)) {
1191  item->impactP = 0.0;
1192  item->impactN = 1.0;
1193  } else {
1194  item->impactP = 1.0;
1195  item->impactN = 0.0;
1196  }
1197  while (queue->first != NULL) {
1198  /* If the size of the subset is below the threshold, quit. */
1199  if (info->size <= threshold)
1200  break;
1201  item = (GlobalQueueItem *) queue->first;
1202  node = item->node;
1203  node = Cudd_Regular(node);
1204  (void) st__lookup(info->table, (const char *)node, (char **)&infoN);
1205  if (safe && infoN->parity == 3) {
1206  cuddLevelQueueDequeue(queue,cuddI(dd,node->index));
1207  continue;
1208  }
1209  impactP = item->impactP;
1210  impactN = item->impactN;
1211  numOnset = infoN->mintermsP * impactP + infoN->mintermsN * impactN;
1212  savings = computeSavings(dd,node,NULL,info,localQueue);
1213  if (savings == 0) {
1214  cuddLevelQueueQuit(queue);
1215  cuddLevelQueueQuit(localQueue);
1216  return(0);
1217  }
1218  cuddLevelQueueDequeue(queue,cuddI(dd,node->index));
1219 #if 0
1220  (void) printf("node %p: impact = %g/%g numOnset = %g savings %d\n",
1221  node, impactP, impactN, numOnset, savings);
1222 #endif
1223  if ((1 - numOnset / info->minterms) >
1224  quality * (1 - (double) savings / info->size)) {
1225  infoN->replace = TRUE;
1226  info->size -= savings;
1227  info->minterms -=numOnset;
1228 #if 0
1229  (void) printf("replace: new size = %d new minterms = %g\n",
1230  info->size, info->minterms);
1231 #endif
1232  savings -= updateRefs(dd,node,NULL,info,localQueue);
1233  assert(savings == 0);
1234  continue;
1235  }
1236  if (!cuddIsConstant(cuddT(node))) {
1237  item = (GlobalQueueItem *) cuddLevelQueueEnqueue(queue,cuddT(node),
1238  cuddI(dd,cuddT(node)->index));
1239  item->impactP += impactP/2.0;
1240  item->impactN += impactN/2.0;
1241  }
1242  if (!Cudd_IsConstant(cuddE(node))) {
1243  item = (GlobalQueueItem *) cuddLevelQueueEnqueue(queue,Cudd_Regular(cuddE(node)),
1244  cuddI(dd,Cudd_Regular(cuddE(node))->index));
1245  if (Cudd_IsComplement(cuddE(node))) {
1246  item->impactP += impactN/2.0;
1247  item->impactN += impactP/2.0;
1248  } else {
1249  item->impactP += impactP/2.0;
1250  item->impactN += impactN/2.0;
1251  }
1252  }
1253  }
1254 
1255  cuddLevelQueueQuit(queue);
1256  cuddLevelQueueQuit(localQueue);
1257  return(1);
1258 
1259 } /* end of UAmarkNodes */
cuddLevelQueueDequeue
void cuddLevelQueueDequeue(DdLevelQueue *queue, int level)
Definition: cuddLevelQ.c:354
updateRefs
static int updateRefs(DdManager *dd, DdNode *f, DdNode *skip, ApproxInfo *info, DdLevelQueue *queue)
Definition: cuddApprox.c:1073
DdNode
Definition: cudd.h:278
computeSavings
static int computeSavings(DdManager *dd, DdNode *f, DdNode *skip, ApproxInfo *info, DdLevelQueue *queue)
Definition: cuddApprox.c:1001
DdManager::size
int size
Definition: cuddInt.h:361
Cudd_IsConstant
#define Cudd_IsConstant(node)
Definition: cudd.h:352
Cudd_Regular
#define Cudd_Regular(node)
Definition: cudd.h:397
ApproxInfo::minterms
double minterms
Definition: cuddApprox.c:139
cuddLevelQueueQuit
void cuddLevelQueueQuit(DdLevelQueue *queue)
Definition: cuddLevelQ.c:244
GlobalQueueItem::node
DdNode * node
Definition: cuddApprox.c:150
DdManager::initSlots
unsigned int initSlots
Definition: cuddInt.h:379
cuddLevelQueueEnqueue
void * cuddLevelQueueEnqueue(DdLevelQueue *queue, void *key, int level)
Definition: cuddLevelQ.c:282
cuddLevelQueueInit
DdLevelQueue * cuddLevelQueueInit(int levels, int itemSize, int numBuckets)
Definition: cuddLevelQ.c:169
Cudd_IsComplement
#define Cudd_IsComplement(node)
Definition: cudd.h:425
cuddIsConstant
#define cuddIsConstant(node)
Definition: cuddInt.h:620
ApproxInfo::table
st__table * table
Definition: cuddApprox.c:135
cuddT
#define cuddT(node)
Definition: cuddInt.h:636
DdLevelQueue::first
void * first
Definition: cuddInt.h:509
TRUE
#define TRUE
Definition: cudd.h:88
cuddI
#define cuddI(dd, index)
Definition: cuddInt.h:686
st__lookup
int st__lookup(st__table *table, const char *key, char **value)
Definition: st.c:114
DdNode::index
DdHalfWord index
Definition: cudd.h:279
cuddE
#define cuddE(node)
Definition: cuddInt.h:652
assert
#define assert(ex)
Definition: util_old.h:213
static void updateParity ( DdNode *  node,
ApproxInfo *  info,
int  newparity 
)
static

AutomaticStart

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]

Definition at line 795 of file cuddApprox.c.

799 {
800  NodeData *infoN;
801  DdNode *E;
802 
803  if (! st__lookup(info->table, (const char *)node, (char **)&infoN)) return;
804  if ((infoN->parity & newparity) != 0) return;
805  infoN->parity |= (short) newparity;
806  if (Cudd_IsConstant(node)) return;
807  updateParity(cuddT(node),info,newparity);
808  E = cuddE(node);
809  if (Cudd_IsComplement(E)) {
810  updateParity(Cudd_Not(E),info,3-newparity);
811  } else {
812  updateParity(E,info,newparity);
813  }
814  return;
815 
816 } /* end of updateParity */
DdNode
Definition: cudd.h:278
Cudd_Not
#define Cudd_Not(node)
Definition: cudd.h:367
Cudd_IsConstant
#define Cudd_IsConstant(node)
Definition: cudd.h:352
Cudd_IsComplement
#define Cudd_IsComplement(node)
Definition: cudd.h:425
ApproxInfo::table
st__table * table
Definition: cuddApprox.c:135
cuddT
#define cuddT(node)
Definition: cuddInt.h:636
st__lookup
int st__lookup(st__table *table, const char *key, char **value)
Definition: st.c:114
NodeData::parity
short int parity
Definition: cuddApprox.c:126
cuddE
#define cuddE(node)
Definition: cuddInt.h:652
updateParity
static void updateParity(DdNode *node, ApproxInfo *info, int newparity)
Definition: cuddApprox.c:795
static int updateRefs ( DdManager *  dd,
DdNode *  f,
DdNode *  skip,
ApproxInfo *  info,
DdLevelQueue *  queue 
)
static

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]

Definition at line 1073 of file cuddApprox.c.

1079 {
1080  NodeData *infoN;
1081  LocalQueueItem *item;
1082  DdNode *node;
1083  int savings = 0;
1084 
1085  node = Cudd_Regular(f);
1086  /* Insert the given node in the level queue. Its function reference
1087  ** count is set equal to 0 so that the search will continue from it
1088  ** when it is retrieved. */
1089  item = (LocalQueueItem *) cuddLevelQueueEnqueue(queue,node,cuddI(dd,node->index));
1090  if (item == NULL)
1091  return(0);
1092  (void) st__lookup(info->table, (const char *)node, (char **)&infoN);
1093  infoN->functionRef = 0;
1094 
1095  if (skip != NULL) {
1096  /* Increase the function reference count of the node to be skipped
1097  ** by 1 to account for the node pointing to it that will be created. */
1098  skip = Cudd_Regular(skip);
1099  (void) st__lookup(info->table, (const char *)skip, (char **)&infoN);
1100  infoN->functionRef++;
1101  }
1102 
1103  /* Process the queue. */
1104  while (queue->first != NULL) {
1105  item = (LocalQueueItem *) queue->first;
1106  node = item->node;
1107  cuddLevelQueueDequeue(queue,cuddI(dd,node->index));
1108  (void) st__lookup(info->table, (const char *)node, (char **)&infoN);
1109  if (infoN->functionRef != 0) {
1110  /* This node is shared or must be skipped. */
1111  continue;
1112  }
1113  savings++;
1114  if (!cuddIsConstant(cuddT(node))) {
1115  item = (LocalQueueItem *) cuddLevelQueueEnqueue(queue,cuddT(node),
1116  cuddI(dd,cuddT(node)->index));
1117  if (item == NULL) return(0);
1118  (void) st__lookup(info->table, (const char *)cuddT(node), (char **)&infoN);
1119  infoN->functionRef--;
1120  }
1121  if (!Cudd_IsConstant(cuddE(node))) {
1122  item = (LocalQueueItem *) cuddLevelQueueEnqueue(queue,Cudd_Regular(cuddE(node)),
1123  cuddI(dd,Cudd_Regular(cuddE(node))->index));
1124  if (item == NULL) return(0);
1125  (void) st__lookup(info->table, (const char *)Cudd_Regular(cuddE(node)), (char **)&infoN);
1126  infoN->functionRef--;
1127  }
1128  }
1129 
1130 #ifdef DD_DEBUG
1131  /* At the end of a local search the queue should be empty. */
1132  assert(queue->size == 0);
1133 #endif
1134  return(savings);
1135 
1136 } /* end of updateRefs */
cuddLevelQueueDequeue
void cuddLevelQueueDequeue(DdLevelQueue *queue, int level)
Definition: cuddLevelQ.c:354
DdNode
Definition: cudd.h:278
Cudd_IsConstant
#define Cudd_IsConstant(node)
Definition: cudd.h:352
Cudd_Regular
#define Cudd_Regular(node)
Definition: cudd.h:397
cuddLevelQueueEnqueue
void * cuddLevelQueueEnqueue(DdLevelQueue *queue, void *key, int level)
Definition: cuddLevelQ.c:282
cuddIsConstant
#define cuddIsConstant(node)
Definition: cuddInt.h:620
ApproxInfo::table
st__table * table
Definition: cuddApprox.c:135
cuddT
#define cuddT(node)
Definition: cuddInt.h:636
DdLevelQueue::first
void * first
Definition: cuddInt.h:509
cuddI
#define cuddI(dd, index)
Definition: cuddInt.h:686
st__lookup
int st__lookup(st__table *table, const char *key, char **value)
Definition: st.c:114
DdNode::index
DdHalfWord index
Definition: cudd.h:279
cuddE
#define cuddE(node)
Definition: cuddInt.h:652
assert
#define assert(ex)
Definition: util_old.h:213
LocalQueueItem::node
DdNode * node
Definition: cuddApprox.c:158

Variable Documentation

char rcsid [] DD_UNUSED = "$Id: cuddApprox.c,v 1.27 2009/02/19 16:16:51 fabio Exp $"
static

Definition at line 171 of file cuddApprox.c.