cudd/cuddCheck.c File Reference

Functions to check consistency of data structures. More...

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

Functions

int Cudd_DebugCheck (DdManager *table)
 Checks for inconsistencies in the DD heap.
int Cudd_CheckKeys (DdManager *table)
 Checks for several conditions that should not occur.
int cuddHeapProfile (DdManager *dd)
 Prints information about the heap.
void cuddPrintNode (DdNode *f, FILE *fp)
 Prints out information on a node.
void cuddPrintVarGroups (DdManager *dd, MtrNode *root, int zdd, int silent)
 Prints the variable groups as a parenthesized list.
static void debugFindParent (DdManager *table, DdNode *node)
 Searches the subtables above node for its parents.

Detailed Description

Functions to check consistency of data structures.

Author:
Fabio Somenzi

Copyright (c) 1995-2015, Regents of the University of Colorado

All rights reserved.

Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met:

Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer.

Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution.

Neither the name of the University of Colorado nor the names of its contributors may be used to endorse or promote products derived from this software without specific prior written permission.

THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.


Function Documentation

int Cudd_CheckKeys ( DdManager table  ) 

Checks for several conditions that should not occur.

Checks for the following conditions:

  • Wrong sizes of subtables.
  • Wrong number of keys found in unique subtable.
  • Wrong number of dead found in unique subtable.
  • Wrong number of keys found in the constant table
  • Wrong number of dead found in the constant table
  • Wrong number of total slots found
  • Wrong number of maximum keys found
  • Wrong number of total dead found

Reports the average length of non-empty lists.

Returns:
the number of subtables for which the number of keys is wrong.
Side effects
None
See also:
Cudd_DebugCheck
int Cudd_DebugCheck ( DdManager table  ) 

Checks for inconsistencies in the DD heap.

The following inconsistencies are checked:

  • node has illegal index
  • live node has dead children
  • node has illegal Then or Else pointers
  • BDD/ADD node has identical children
  • ZDD node has zero then child
  • wrong number of total nodes
  • wrong number of dead nodes
  • ref count error at node
Returns:
0 if no inconsistencies are found; DD_OUT_OF_MEM if there is not enough memory; 1 otherwise.
Side effects
None
See also:
Cudd_CheckKeys
int cuddHeapProfile ( DdManager dd  ) 

Prints information about the heap.

Prints to the manager's stdout the number of live nodes for each level of the DD heap that contains at least one live node. It also prints a summary containing:

  • total number of tables;
  • number of tables with live nodes;
  • table with the largest number of live nodes;
  • number of nodes in that table.

If more than one table contains the maximum number of live nodes, only the one of lowest index is reported.

Returns:
1 in case of success and 0 otherwise.
Side effects
None
void cuddPrintNode ( DdNode f,
FILE *  fp 
)

Prints out information on a node.

Side effects
None
void cuddPrintVarGroups ( DdManager dd,
MtrNode root,
int  zdd,
int  silent 
)

Prints the variable groups as a parenthesized list.

For each group the level range that it represents is printed. After each group, the group's flags are printed, preceded by a `|'. For each flag (except MTR_TERMINAL) a character is printed.

  • F: MTR_FIXED
  • N: MTR_NEWNODE
  • S: MTR_SOFT

The second argument, silent, if different from 0, causes Cudd_PrintVarGroups to only check the syntax of the group tree.

Side effects
None
Parameters:
dd manager
root root of the group tree
zdd 0: BDD; 1: ZDD
silent flag to check tree syntax only
static void debugFindParent ( DdManager table,
DdNode node 
) [static]

Searches the subtables above node for its parents.

Side effects
None
 All Data Structures Files Functions Variables Typedefs Enumerations Defines

Generated on 31 Dec 2015 for cudd by  doxygen 1.6.1