Internal data structures of the CUDD package. More...

#include <math.h>
#include "config.h"
#include "st.h"
#include "mtr.h"
#include "epd.h"
#include "cudd.h"

Include dependency graph for cuddInt.h:

Data Structures
struct	DdChildren
	The two children of a non-terminal node. More...

struct	DdNode
	Decision diagram node. More...

struct	DdGen
	CUDD generator. More...

struct	DdHook
	CUDD hook. More...

struct	DdLocalCacheItem
	Generic local cache item. More...

struct	DdLocalCache
	Local cache. More...

struct	DdHashItem
	Local hash table item. More...

struct	DdHashTable
	Local hash table. More...

struct	DdCache
	Computed table. More...

struct	DdSubtable
	Subtable for one index. More...

struct	DdManager
	Specialized DD symbol table. More...

struct	Move
	Reordering move record. More...

struct	IndexKey
	Used to sort variables for reordering. More...

struct	DdQueueItem
	Generic level queue item. More...

struct	DdLevelQueue
	Level queue. More...

Macros
#define	CUDD_VERSION PACKAGE_VERSION

#define	DD_MAXREF ((DdHalfWord) ~0)

#define	DD_DEFAULT_RESIZE 10 /* how many extra variables */

#define	DD_MEM_CHUNK 1022

#define	DD_ONE_VAL (1.0)

#define	DD_ZERO_VAL (0.0)

#define	DD_EPSILON (1.0e-12)

#define	DD_PLUS_INF_VAL (HUGE_VAL)

#define	DD_MINUS_INF_VAL (-(DD_PLUS_INF_VAL))

#define	DD_NON_CONSTANT ((DdNode ) 1) / for Cudd_bddIteConstant */

#define	DD_MAX_SUBTABLE_DENSITY 4 /* tells when to resize a subtable */

#define	DD_GC_FRAC_LO DD_MAX_SUBTABLE_DENSITY * 0.25

#define	DD_GC_FRAC_HI DD_MAX_SUBTABLE_DENSITY * 1.0

#define	DD_GC_FRAC_MIN 0.2

#define	DD_MIN_HIT

#define	DD_MAX_LOOSE_FRACTION

#define	DD_MAX_CACHE_FRACTION

#define	DD_STASH_FRACTION

#define	DD_MAX_CACHE_TO_SLOTS_RATIO 4 /* used to limit the cache size */

#define	DD_SIFT_MAX_VAR 1000

#define	DD_SIFT_MAX_SWAPS 2000000

#define	DD_DEFAULT_RECOMB 0

#define	DD_MAX_REORDER_GROWTH 1.2

#define	DD_FIRST_REORDER 4004 /* 4 for the constants */

#define	DD_DYN_RATIO 2 /* when to dynamically reorder */

#define	DD_P1 12582917

#define	DD_P2 4256249

#define	DD_P3 741457

#define	DD_P4 1618033999

#define	DD_ADD_ITE_TAG 0x02

#define	DD_BDD_AND_ABSTRACT_TAG 0x06

#define	DD_BDD_XOR_EXIST_ABSTRACT_TAG 0x0a

#define	DD_BDD_ITE_TAG 0x0e

#define	DD_ADD_BDD_DO_INTERVAL_TAG 0x22

#define	DD_BDD_CLIPPING_AND_ABSTRACT_UP_TAG 0x26

#define	DD_BDD_CLIPPING_AND_ABSTRACT_DOWN_TAG 0x2a

#define	DD_BDD_COMPOSE_RECUR_TAG 0x2e

#define	DD_ADD_COMPOSE_RECUR_TAG 0x42

#define	DD_ADD_NON_SIM_COMPOSE_TAG 0x46

#define	DD_EQUIV_DC_TAG 0x4a

#define	DD_ZDD_ITE_TAG 0x4e

#define	DD_ADD_ITE_CONSTANT_TAG 0x62

#define	DD_ADD_EVAL_CONST_TAG 0x66

#define	DD_BDD_ITE_CONSTANT_TAG 0x6a

#define	DD_ADD_OUT_SUM_TAG 0x6e

#define	DD_BDD_LEQ_UNLESS_TAG 0x82

#define	DD_ADD_TRIANGLE_TAG 0x86

#define	DD_BDD_MAX_EXP_TAG 0x8a

#define	DD_VARS_SYMM_BEFORE_TAG 0x8e

#define	DD_VARS_SYMM_BETWEEN_TAG 0xa2

#define	CUDD_GEN_CUBES 0

#define	CUDD_GEN_PRIMES 1

#define	CUDD_GEN_NODES 2

#define	CUDD_GEN_ZDD_PATHS 3

#define	CUDD_GEN_EMPTY 0

#define	CUDD_GEN_NONEMPTY 1

#define	CUDD_MAXINDEX (((DdHalfWord) ~0) >> 1)
	Maximum variable index. More...

#define	CUDD_CONST_INDEX CUDD_MAXINDEX
	The index of constant nodes. More...

#define	STAB_SIZE 64
	Size of the random number generator shuffle table.

#define	CUDD_CHECK_MASK 0x7ff
	Mask for periodic check of termination and timeout. More...

#define	cuddDeallocNode(unique, node)
	Adds node to the head of the free list. More...

#define	cuddDeallocMove(unique, node)
	Adds node to the head of the free list. More...

#define	cuddRef(n) cuddSatInc(Cudd_Regular(n)->ref)
	Increases the reference count of a node, if it is not saturated. More...

#define	cuddDeref(n) cuddSatDec(Cudd_Regular(n)->ref)
	Decreases the reference count of a node, if it is not saturated. More...

#define	Cudd_IsConstantInt(node) ((Cudd_Regular(node))->index == CUDD_CONST_INDEX)
	Returns 1 if the node is a constant node. More...

#define	cuddIsConstant(node) ((node)->index == CUDD_CONST_INDEX)
	Returns 1 if the node is a constant node. More...

#define	cuddT(node) ((node)->type.kids.T)
	Returns the then child of an internal node. More...

#define	cuddE(node) ((node)->type.kids.E)
	Returns the else child of an internal node. More...

#define	cuddV(node) ((node)->type.value)
	Returns the value of a constant node. More...

#define	cuddI(dd, index) (((index)==CUDD_CONST_INDEX)?(int)(index):(dd)->perm[(index)])
	Finds the current position of variable index in the order. More...

#define	cuddIZ(dd, index) (((index)==CUDD_CONST_INDEX)?(int)(index):(dd)->permZ[(index)])
	Finds the current position of ZDD variable index in the order. More...

#define	ddHash(f, g, s)
	Hash function for the unique table. More...

#define	ddCHash(o, f, g, h, s)
	Hash function for the cache. More...

#define	ddCHash2(o, f, g, s)
	Hash function for the cache for functions with two operands. More...

#define	cuddClean(p) ((DdNode *)((ptruint)(p) & ~ (ptruint) 0xf))
	Clears the 4 least significant bits of a pointer. More...

#define	ddMin(x, y) (((y) < (x)) ? (y) : (x))
	Computes the minimum of two numbers. More...

#define	ddMax(x, y) (((y) > (x)) ? (y) : (x))
	Computes the maximum of two numbers. More...

#define	ddAbs(x) (((x)<0) ? -(x) : (x))
	Computes the absolute value of a number. More...

#define	ddEqualVal(x, y, e) (ddAbs((x)-(y))<(e))
	Returns 1 if the absolute value of the difference of the two arguments x and y is less than e. More...

#define	cuddSatInc(x) ((x)++)
	Saturating increment operator. More...

#define	cuddSatDec(x) ((x)--)
	Saturating decrement operator. More...

#define	DD_ONE(dd) ((dd)->one)
	Returns the constant 1 node. More...

#define	DD_ZERO(dd) ((dd)->zero)
	Returns the arithmetic 0 constant node. More...

#define	DD_PLUS_INFINITY(dd) ((dd)->plusinfinity)
	Returns the plus infinity constant node. More...

#define	DD_MINUS_INFINITY(dd) ((dd)->minusinfinity)
	Returns the minus infinity constant node. More...

#define	cuddAdjust(x)
	Enforces DD_MINUS_INF_VAL <= x <= DD_PLUS_INF_VAL. More...

#define	statLine(dd)
	Outputs a line of stats. More...

#define	checkWhetherToGiveUp(dd)
	Checks for termination or timeout. More...

Typedefs
typedef uint32_t	DdHalfWord
	Type that is half the size of a pointer.

typedef intptr_t	ptrint
	Signed integer that is the size of a pointer. More...

typedef uintptr_t	ptruint
	Unsigned integer that is the size of a pointer. More...

typedef struct DdChildren	DdChildren

typedef struct DdHook	DdHook

typedef struct DdSubtable	DdSubtable

typedef struct DdCache	DdCache

typedef struct DdLocalCacheItem	DdLocalCacheItem

typedef struct DdLocalCache	DdLocalCache

typedef struct DdHashItem	DdHashItem

typedef struct DdHashTable	DdHashTable

typedef struct Move	Move

typedef struct IndexKey	IndexKey

typedef struct DdQueueItem	DdQueueItem

typedef struct DdLevelQueue	DdLevelQueue

Detailed Description

Internal data structures of the CUDD package.

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.

Macro Definition Documentation

◆ checkWhetherToGiveUp

#define checkWhetherToGiveUp ( dd )

Value:

do {                                                                \
        if (((int64_t) CUDD_CHECK_MASK & (int64_t) (dd)->cacheMisses) == 0) { \
            if ((dd)->terminationCallback != NULL &&                    \
                (dd)->terminationCallback((dd)->tcbArg)) {              \
                (dd)->errorCode = CUDD_TERMINATION;                     \
                return(NULL);                                           \
            }                                                           \
            if (util_cpu_time() - (dd)->startTime > (dd)->timeLimit) {  \
                (dd)->errorCode = CUDD_TIMEOUT_EXPIRED;                 \
                return(NULL);                                           \
            }                                                           \
        }                                                               \
    } while (0)

Checks for termination or timeout.

◆ CUDD_CHECK_MASK

#define CUDD_CHECK_MASK 0x7ff

Mask for periodic check of termination and timeout.

See also: checkWhetherToGiveUp

◆ CUDD_CONST_INDEX

#define CUDD_CONST_INDEX CUDD_MAXINDEX

The index of constant nodes.

This is a synonim for CUDD_MAXINDEX.

◆ Cudd_IsConstantInt

#define Cudd_IsConstantInt ( node ) ((Cudd_Regular(node))->index == CUDD_CONST_INDEX)

Returns 1 if the node is a constant node.

Returns 1 if the node is a constant node (rather than an internal node). All constant nodes have the same index (CUDD_CONST_INDEX). The pointer passed to Cudd_IsConstantInt may be either regular or complemented.

Side effects none

See also: cuddIsConstant Cudd_IsConstant

◆ CUDD_MAXINDEX

#define CUDD_MAXINDEX (((DdHalfWord) ~0) >> 1)

Maximum variable index.

CUDD_MAXINDEX is defined in such a way that on 32-bit and 64-bit machines one can cast an index to (int) without generating a negative number.

◆ cuddAdjust

#define cuddAdjust ( x )

Enforces DD_MINUS_INF_VAL <= x <= DD_PLUS_INF_VAL.

Furthermore, if x <= DD_MINUS_INF_VAL/2, x is set to DD_MINUS_INF_VAL. Similarly, if DD_PLUS_INF_VAL/2 <= x, x is set to DD_PLUS_INF_VAL. Normally this macro is a NOOP. However, if HAVE_IEEE_754 is not defined, it makes sure that a value does not get larger than infinity in absolute value, and once it gets to infinity, stays there. If the value overflows before this macro is applied, no recovery is possible.

Side effects none

◆ cuddClean

#define cuddClean ( p ) ((DdNode *)((ptruint)(p) & ~ (ptruint) 0xf))

Clears the 4 least significant bits of a pointer.

Side effects none

◆ cuddDeallocMove

#define cuddDeallocMove	(	unique,
		node
	)

Value:

((DdNode *)(node))->ref = 0; \
    ((DdNode *)(node))->next = (unique)->nextFree; \
    (unique)->nextFree = (DdNode *)(node);

Adds node to the head of the free list.

Does not deallocate memory chunks that become free. This function is also used by the dynamic reordering functions.

Side effects None

See also: cuddDeallocNode cuddDynamicAllocNode

◆ cuddDeallocNode

#define cuddDeallocNode	(	unique,
		node
	)

Value:

(node)->next = (unique)->nextFree; \

(unique)->nextFree = node;

Adds node to the head of the free list.

Does not deallocate memory chunks that become free. This function is also used by the dynamic reordering functions.

Side effects None

See also: cuddAllocNode cuddDynamicAllocNode cuddDeallocMove

◆ cuddDeref

#define cuddDeref ( n ) cuddSatDec(Cudd_Regular(n)->ref)

Decreases the reference count of a node, if it is not saturated.

It is primarily used in recursive procedures to decrease the ref count of a result node before returning it. This accomplishes the goal of removing the protection applied by a previous cuddRef. This being a macro, it is faster than Cudd_Deref, but it cannot be used in constructs like cuddDeref(a = b()).

Side effects none

See also: Cudd_Deref

◆ cuddE

#define cuddE ( node ) ((node)->type.kids.E)

Returns the else child of an internal node.

If node is a constant node, the result is unpredictable. The pointer passed to cuddE must be regular.

Side effects none

See also: Cudd_E

◆ cuddI

#define cuddI	(	dd,
		index
	)	(((index)==CUDD_CONST_INDEX)?(int)(index):(dd)->perm[(index)])

Finds the current position of variable index in the order.

This macro duplicates the functionality of Cudd_ReadPerm, but it does not check for out-of-bounds indices and it is more efficient.

Side effects none

See also: Cudd_ReadPerm

◆ cuddIsConstant

#define cuddIsConstant ( node ) ((node)->index == CUDD_CONST_INDEX)

Returns 1 if the node is a constant node.

Returns 1 if the node is a constant node (rather than an internal node). All constant nodes have the same index (CUDD_CONST_INDEX). The pointer passed to cuddIsConstant must be regular.

Side effects none

See also: Cudd_IsConstant Cudd_IsConstantInt

◆ cuddIZ

#define cuddIZ	(	dd,
		index
	)	(((index)==CUDD_CONST_INDEX)?(int)(index):(dd)->permZ[(index)])

Finds the current position of ZDD variable index in the order.

This macro duplicates the functionality of Cudd_ReadPermZdd, but it does not check for out-of-bounds indices and it is more efficient.

Side effects none

See also: Cudd_ReadPermZdd

◆ cuddRef

#define cuddRef ( n ) cuddSatInc(Cudd_Regular(n)->ref)

Increases the reference count of a node, if it is not saturated.

This being a macro, it is faster than Cudd_Ref, but it cannot be used in constructs like cuddRef(a = b()).

Side effects none

See also: Cudd_Ref

◆ cuddSatDec

#define cuddSatDec ( x ) ((x)--)

Saturating decrement operator.

Saturation is only necessary on 32-bit machines, where the reference count is only 16-bit wide.

Side effects none

See also: cuddSatInc

◆ cuddSatInc

#define cuddSatInc ( x ) ((x)++)

Saturating increment operator.

Saturation is only necessary on 32-bit machines, where the reference count is only 16-bit wide.

Side effects none

See also: cuddSatDec

◆ cuddT

#define cuddT ( node ) ((node)->type.kids.T)

Returns the then child of an internal node.

If node is a constant node, the result is unpredictable. The pointer passed to cuddT must be regular.

Side effects none

See also: Cudd_T

◆ cuddV

#define cuddV ( node ) ((node)->type.value)

Returns the value of a constant node.

If node is an internal node, the result is unpredictable. The pointer passed to cuddV must be regular.

Side effects none

See also: Cudd_V

◆ DD_MAX_CACHE_FRACTION

#define DD_MAX_CACHE_FRACTION

Value:

3 /* 1 / (max fraction of memory used for

computed table if resizing enabled) */

◆ DD_MAX_LOOSE_FRACTION

#define DD_MAX_LOOSE_FRACTION

Value:

5 /* 1 / (max fraction of memory used for

unique table in fast growth mode) */

◆ DD_MIN_HIT

#define DD_MIN_HIT

Value:

30 /* resize cache when hit ratio

above this percentage (default) */

◆ DD_MINUS_INFINITY

#define DD_MINUS_INFINITY ( dd ) ((dd)->minusinfinity)

Returns the minus infinity constant node.

Side effects none

See also: DD_ONE DD_ZERO DD_PLUS_INFINITY

◆ DD_ONE

#define DD_ONE ( dd ) ((dd)->one)

Returns the constant 1 node.

Side effects none

See also: DD_ZERO DD_PLUS_INFINITY DD_MINUS_INFINITY

◆ DD_PLUS_INFINITY

#define DD_PLUS_INFINITY ( dd ) ((dd)->plusinfinity)

Returns the plus infinity constant node.

Side effects none

See also: DD_ONE DD_ZERO DD_MINUS_INFINITY

◆ DD_STASH_FRACTION

#define DD_STASH_FRACTION

Value:

64 /* 1 / (fraction of memory set

aside for emergencies) */

◆ DD_ZERO

#define DD_ZERO ( dd ) ((dd)->zero)

Returns the arithmetic 0 constant node.

This is different from the logical zero. The latter is obtained by Cudd_Not(DD_ONE(dd)).

Side effects none

See also: DD_ONE Cudd_Not DD_PLUS_INFINITY DD_MINUS_INFINITY

◆ ddAbs

#define ddAbs ( x ) (((x)<0) ? -(x) : (x))

Computes the absolute value of a number.

Side effects none

◆ ddCHash

#define ddCHash	(	o,
		f,
		g,
		h,
		s
	)

Value:

((((((unsigned)(ptruint)(f) + (unsigned)(ptruint)(o)) * DD_P1 + \
    (unsigned)(ptruint)(g)) * DD_P2 + \
   (unsigned)(ptruint)(h)) * DD_P3) >> (s))

Hash function for the cache.

Side effects none

See also: ddHash ddCHash2

◆ ddCHash2

#define ddCHash2	(	o,
		f,
		g,
		s
	)

Value:

(((((unsigned)(ptruint)(f) + (unsigned)(ptruint)(o)) * DD_P1 + \

(unsigned)(ptruint)(g)) * DD_P2) >> (s))

ptruint

uintptr_t ptruint

Unsigned integer that is the size of a pointer.

Definition: cuddInt.h:231

Hash function for the cache for functions with two operands.

Side effects none

See also: ddHash ddCHash

◆ ddEqualVal

#define ddEqualVal	(	x,
		y,
		e
	)	(ddAbs((x)-(y))<(e))

Returns 1 if the absolute value of the difference of the two arguments x and y is less than e.

Side effects none

◆ ddHash

#define ddHash	(	f,
		g,
		s
	)

Value:

((((unsigned)(ptruint)(f) * DD_P1 + \

(unsigned)(ptruint)(g)) * DD_P2) >> (s))

ptruint

uintptr_t ptruint

Unsigned integer that is the size of a pointer.

Definition: cuddInt.h:231

Hash function for the unique table.

Side effects none

See also: ddCHash ddCHash2

◆ ddMax

#define ddMax	(	x,
		y
	)	(((y) > (x)) ? (y) : (x))

Computes the maximum of two numbers.

Side effects none

See also: ddMin

◆ ddMin

#define ddMin	(	x,
		y
	)	(((y) < (x)) ? (y) : (x))

Computes the minimum of two numbers.

Side effects none

See also: ddMax

◆ statLine

#define statLine ( dd )

Outputs a line of stats.

Outputs a line of stats if DD_COUNT and DD_STATS are defined. Increments the number of recursive calls if DD_COUNT is defined.

Side effects None

Typedef Documentation

◆ ptrint

typedef intptr_t ptrint

Signed integer that is the size of a pointer.

The only platforms on which CUDD has been tested define intptr_t and uintptr_t in inttypes.h and satisfy the condition

sizeof(intptr_t) == sizeof(uintptr_t) == sizeof(void *)

Neither of these is guaranteed by the C standard.

◆ ptruint

typedef uintptr_t ptruint

Unsigned integer that is the size of a pointer.

See also: ptrint

Data Structures

Macros

Typedefs

Detailed Description

Macro Definition Documentation

◆ checkWhetherToGiveUp

◆ CUDD_CHECK_MASK

◆ CUDD_CONST_INDEX

◆ Cudd_IsConstantInt

◆ CUDD_MAXINDEX

◆ cuddAdjust

◆ cuddClean

◆ cuddDeallocMove

◆ cuddDeallocNode

◆ cuddDeref

◆ cuddE

◆ cuddI

◆ cuddIsConstant

◆ cuddIZ

◆ cuddRef

◆ cuddSatDec

◆ cuddSatInc

◆ cuddT

◆ cuddV

◆ DD_MAX_CACHE_FRACTION

◆ DD_MAX_LOOSE_FRACTION

◆ DD_MIN_HIT

◆ DD_MINUS_INFINITY

◆ DD_ONE

◆ DD_PLUS_INFINITY

◆ DD_STASH_FRACTION

◆ DD_ZERO

◆ ddAbs

◆ ddCHash

◆ ddCHash2

◆ ddEqualVal

◆ ddHash

◆ ddMax

◆ ddMin

◆ statLine

Typedef Documentation

◆ ptrint

◆ ptruint