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

int	Cudd_CheckKeys (DdManager *table)
	Checks for several conditions that should not occur. More...

int	cuddHeapProfile (DdManager *dd)
	Prints information about the heap. More...

void	cuddPrintNode (DdNode f, FILE fp)
	Prints out information on a node. More...

void	cuddPrintVarGroups (DdManager dd, MtrNode root, int zdd, int silent)
	Prints the variable groups as a parenthesized list. More...

static void	debugFindParent (DdManager table, DdNode node)
	Searches the subtables above node for its parents. More...

Detailed Description

Functions to check consistency of data structures.

Author: Fabio Somenzi

Copyright

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

◆ Cudd_CheckKeys()

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

◆ 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

◆ cuddHeapProfile()

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

◆ cuddPrintNode()

void cuddPrintNode	(	DdNode *	f,
		FILE *	fp
	)

Prints out information on a node.

Side effects None

◆ cuddPrintVarGroups()

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

◆ debugFindParent()

static void debugFindParent	(	DdManager *	table,
		DdNode *	node
	)

static

Searches the subtables above node for its parents.

Side effects None