VIS
|
#include "synthInt.h"
Go to the source code of this file.
Functions | |
static int | CountMultiLevelFactor (bdd_manager *dd, MlTree *top, MlTree *tree, int ref) |
static int | GetLiteralCount (bdd_manager *dd, bdd_node *node, int nLiterals) |
int | SynthCountMlLiteral (bdd_manager *dd, MlTree *tree, int ref) |
int | SynthGetSupportMask (bdd_manager *dd, bdd_node *node, unsigned int *mask) |
int | SynthGetSupportCount (bdd_manager *dd, bdd_node *node) |
void | SynthZddSupportStep (bdd_node *f, int *support) |
void | SynthZddClearFlag (bdd_node *f) |
int | SynthGetLiteralCount (bdd_manager *dd, bdd_node *node) |
Variables | |
static char rcsid[] | UNUSED = "$Id: synthCount.c,v 1.14 1998/08/31 19:22:12 mooni Exp $" |
static int CountMultiLevelFactor | ( | bdd_manager * | dd, |
MlTree * | top, | ||
MlTree * | tree, | ||
int | ref | ||
) | [static] |
AutomaticStart
Function********************************************************************
Synopsis [Counts the number of literals of a MlTree.]
Description [Counts the number of literals of a MlTree.]
SideEffects []
SeeAlso [SynthCountMlLiteral]
Definition at line 284 of file synthCount.c.
{ bdd_node *one = bdd_read_one(dd); bdd_node *zero = bdd_read_zero(dd); bdd_node *f; int i, *support; int count = 0; int sizeZ = bdd_num_zdd_vars(dd); if (ref && tree != top && tree->shared) return(1); f = tree->node; if (f == one || f == zero) return(0); if (tree->leaf) { support = ALLOC(int, sizeZ); if (!support) return(0); (void)memset((void *)support, 0, sizeof(int) * sizeZ); SynthZddSupportStep(bdd_regular(tree->node), support); SynthZddClearFlag(bdd_regular(tree->node)); for (i = 0; i < sizeZ; i++) { if (support[i]) count++; } FREE(support); return(count); } count += CountMultiLevelFactor(dd, top, tree->q, ref); count += CountMultiLevelFactor(dd, top, tree->d, ref); count += CountMultiLevelFactor(dd, top, tree->r, ref); return(count); }
static int GetLiteralCount | ( | bdd_manager * | dd, |
bdd_node * | node, | ||
int | nLiterals | ||
) | [static] |
Function********************************************************************
Synopsis [Recursive procedure of SynthGetLiteralCount.]
Description [Recursive procedure of SynthGetLiteralCount. Counts the number of literals in a ZDD cover. The argument nLiterals is the number of literals currently counted.]
SideEffects []
SeeAlso []
Definition at line 340 of file synthCount.c.
{ bdd_node *one = bdd_read_one(dd); bdd_node *zero = bdd_read_zero(dd); int count = 0; if (node == zero) return(0); if (node == one) return(nLiterals); count = GetLiteralCount(dd, bdd_bdd_T(node), nLiterals + 1); count += GetLiteralCount(dd, bdd_bdd_E(node), nLiterals); return(count); }
int SynthCountMlLiteral | ( | bdd_manager * | dd, |
MlTree * | tree, | ||
int | ref | ||
) |
AutomaticEnd Function********************************************************************
Synopsis [Counts the number of literals of a MlTree.]
Description [Counts the number of literals of a MlTree. The argument ref controls whether to count shared literals or non-shared. If ref is 1, it counts shared literals.]
SideEffects []
SeeAlso []
Definition at line 75 of file synthCount.c.
{ bdd_node *one = bdd_read_one(dd); bdd_node *zero = bdd_read_zero(dd); int count = 0; if (tree->top || tree->shared) { if (ref && tree->ref) { if (tree->node != zero && tree->node != one) count = 1; return(count); } count += CountMultiLevelFactor(dd, tree, tree, ref); } if (tree->leaf) return(count); if (tree->q_ref == 0) count += SynthCountMlLiteral(dd, tree->q, ref); if (tree->d_ref == 0) count += SynthCountMlLiteral(dd, tree->d, ref); if (tree->r_ref == 0) count += SynthCountMlLiteral(dd, tree->r, ref); return(count); }
int SynthGetLiteralCount | ( | bdd_manager * | dd, |
bdd_node * | node | ||
) |
Function********************************************************************
Synopsis [Counts the number of literals in a ZDD cover.]
Description [Counts the number of literals in a ZDD cover.]
SideEffects []
SeeAlso []
Definition at line 261 of file synthCount.c.
{ return(GetLiteralCount(dd, node, 0)); }
int SynthGetSupportCount | ( | bdd_manager * | dd, |
bdd_node * | node | ||
) |
Function********************************************************************
Synopsis [Returns the number of support variables of a node.]
Description [Returns the number of support variables of a node.]
SideEffects []
SeeAlso []
Definition at line 165 of file synthCount.c.
{ int i, count; int *support; int zddSize = bdd_num_zdd_vars(dd); count = 0; support = ALLOC(int, zddSize); (void)memset((void *)support, 0, sizeof(int) * zddSize); SynthZddSupportStep(bdd_regular(node), support); SynthZddClearFlag(bdd_regular(node)); for (i = 0; i < zddSize; i++) { if (support[i]) count++; } FREE(support); return(count); }
int SynthGetSupportMask | ( | bdd_manager * | dd, |
bdd_node * | node, | ||
unsigned int * | mask | ||
) |
Function********************************************************************
Synopsis [Makes a bit string for representing the support of a node.]
Description [Makes a bit string for representing the support of a node. It returns the number of support variables of the ZDD node. The argument mask is given by caller, which is array of unsigned integer.]
SideEffects []
SeeAlso []
Definition at line 120 of file synthCount.c.
{ int i, pos, count; int word, size; int bit, bit_mask; int *support; int zddSize = bdd_num_zdd_vars(dd); count = 0; word = sizeof(int) * 8; size = zddSize / word + 1; support = ALLOC(int, zddSize); (void)memset((void *)support, 0, sizeof(int) * zddSize); (void)memset((void *)mask, 0, size * sizeof(int)); SynthZddSupportStep(bdd_regular(node), support); SynthZddClearFlag(bdd_regular(node)); for (i = 0; i < zddSize; i++) { if (support[i]) { pos = i / word; bit = i % word; bit_mask = 01 << bit; mask[pos] |= bit_mask; count++; } } FREE(support); return(count); }
void SynthZddClearFlag | ( | bdd_node * | f | ) |
Function********************************************************************
Synopsis [Performs a DFS from f, clearing the LSB of the next pointers.]
Description [Performs a DFS from f, clearing the LSB of the next pointers.]
SideEffects []
SeeAlso [SynthZddSupportStep]
Definition at line 229 of file synthCount.c.
{ bdd_node *temp; temp = bdd_read_next(f); if (!bdd_is_complement(temp)) { return; } /* Clear visited flag. */ bdd_set_next(f, bdd_regular(temp)); if (bdd_is_constant(f)) { return; } SynthZddClearFlag(bdd_bdd_T(f)); SynthZddClearFlag(bdd_regular(bdd_bdd_E(f))); return; }
void SynthZddSupportStep | ( | bdd_node * | f, |
int * | support | ||
) |
Function********************************************************************
Synopsis [Finds the support of f.]
Description [Finds the support of f. Performs a DFS from f. Whenever a node is visited, the variable of the node is accumulated in support, and the the node is marked not to be visited again. Uses the LSB of the next pointer as visited flag.]
SideEffects [Once this function is called, SynthZddClearFlag() should be called right after.]
SeeAlso [SynthZddClearFlag]
Definition at line 202 of file synthCount.c.
{ if (bdd_is_constant(f) || bdd_is_complement(bdd_read_next(f))) { return; } support[bdd_node_read_index(f)] = 1; SynthZddSupportStep(bdd_bdd_T(f),support); SynthZddSupportStep(bdd_regular(bdd_bdd_E(f)),support); /* Mark as visited. */ bdd_set_next(f, bdd_not_bdd_node(bdd_read_next(f))); return; }
char rcsid [] UNUSED = "$Id: synthCount.c,v 1.14 1998/08/31 19:22:12 mooni Exp $" [static] |
CFile***********************************************************************
FileName [synthCount.c]
PackageName [synth]
Synopsis [Literal counting functions.]
Author [In-Ho Moon, Balakrishna Kumthekar]
Copyright [This file was created at the University of Colorado at Boulder. The University of Colorado at Boulder makes no warranty about the suitability of this software for any purpose. It is presented on an AS IS basis.]
Definition at line 19 of file synthCount.c.