cudd/cuddInt.h File Reference

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:

Go to the source code of this file.

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

Defines

#define CUDD_VERSION   PACKAGE_VERSION
#define DD_MAXREF   ((DdHalfWord) ~0)
#define DD_DEFAULT_RESIZE   10
#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   (10e301)
#define DD_CRI_HI_MARK   (10e150)
#define DD_CRI_LO_MARK   (-(DD_CRI_HI_MARK))
#define DD_MINUS_INF_VAL   (-(DD_PLUS_INF_VAL))
#define DD_NON_CONSTANT   ((DdNode *) 1)
#define DD_MAX_SUBTABLE_DENSITY   4
#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   30
#define DD_MAX_LOOSE_FRACTION   5
#define DD_MAX_CACHE_FRACTION   3
#define DD_STASH_FRACTION   64
#define DD_MAX_CACHE_TO_SLOTS_RATIO   4
#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
#define DD_DYN_RATIO   2
#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)
 Maximum variable index.
#define CUDD_CONST_INDEX   CUDD_MAXINDEX
 The index of constant nodes.
#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.
#define cuddDeallocNode(unique, node)
 Adds node to the head of the free list.
#define cuddDeallocMove(unique, node)
 Adds node to the head of the free list.
#define cuddRef(n)   cuddSatInc(Cudd_Regular(n)->ref)
 Increases the reference count of a node, if it is not saturated.
#define cuddDeref(n)   cuddSatDec(Cudd_Regular(n)->ref)
 Decreases the reference count of a node, if it is not saturated.
#define Cudd_IsConstantInt(node)   ((Cudd_Regular(node))->index == CUDD_CONST_INDEX)
 Returns 1 if the node is a constant node.
#define cuddIsConstant(node)   ((node)->index == CUDD_CONST_INDEX)
 Returns 1 if the node is a constant node.
#define cuddT(node)   ((node)->type.kids.T)
 Returns the then child of an internal node.
#define cuddE(node)   ((node)->type.kids.E)
 Returns the else child of an internal node.
#define cuddV(node)   ((node)->type.value)
 Returns the value of a constant node.
#define cuddI(dd, index)   (((index)==CUDD_CONST_INDEX)?(int)(index):(dd)->perm[(index)])
 Finds the current position of variable index in the order.
#define cuddIZ(dd, index)   (((index)==CUDD_CONST_INDEX)?(int)(index):(dd)->permZ[(index)])
 Finds the current position of ZDD variable index in the order.
#define ddHash(f, g, s)   ((((unsigned)(f) * DD_P1 + (unsigned)(g)) * DD_P2) >> (s))
 Hash function for the unique table.
#define ddCHash(o, f, g, h, s)
 Hash function for the cache.
#define ddCHash2(o, f, g, s)   (((((unsigned)(f) + (unsigned)(o)) * DD_P1 + (unsigned)(g)) * DD_P2) >> (s))
 Hash function for the cache for functions with two operands.
#define cuddClean(p)   ((DdNode *)((ptruint)(p) & ~ (ptruint) 0xf))
 Clears the 4 least significant bits of a pointer.
#define ddMin(x, y)   (((y) < (x)) ? (y) : (x))
 Computes the minimum of two numbers.
#define ddMax(x, y)   (((y) > (x)) ? (y) : (x))
 Computes the maximum of two numbers.
#define ddAbs(x)   (((x)<0) ? -(x) : (x))
 Computes the absolute value of a number.
#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.
#define cuddSatInc(x)   ((x) += (x) != (DdHalfWord)DD_MAXREF)
 Saturating increment operator.
#define cuddSatDec(x)   ((x) -= (x) != (DdHalfWord)DD_MAXREF)
 Saturating decrement operator.
#define DD_ONE(dd)   ((dd)->one)
 Returns the constant 1 node.
#define DD_ZERO(dd)   ((dd)->zero)
 Returns the arithmetic 0 constant node.
#define DD_PLUS_INFINITY(dd)   ((dd)->plusinfinity)
 Returns the plus infinity constant node.
#define DD_MINUS_INFINITY(dd)   ((dd)->minusinfinity)
 Returns the minus infinity constant node.
#define cuddAdjust(x)   ((x) = ((x) >= DD_CRI_HI_MARK) ? DD_PLUS_INF_VAL : (((x) <= DD_CRI_LO_MARK) ? DD_MINUS_INF_VAL : (x)))
 Enforces DD_MINUS_INF_VAL <= x <= DD_PLUS_INF_VAL.
#define statLine(dd)
 Outputs a line of stats.
#define checkWhetherToGiveUp(dd)
 Checks for termination or timeout.

Typedefs

typedef uint16_t DdHalfWord
 Type that is half the size of a pointer.
typedef intptr_t ptrint
 Signed integer that is the size of a pointer.
typedef uintptr_t ptruint
 Unsigned integer that is the size of a pointer.
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 (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.


Define Documentation

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

#define CUDD_CHECK_MASK   0x7ff

Mask for periodic check of termination and timeout.

See also:
checkWhetherToGiveUp
#define CUDD_CONST_INDEX   CUDD_MAXINDEX

The index of constant nodes.

This is a synonim for CUDD_MAXINDEX.

#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
#define CUDD_MAXINDEX   ((DdHalfWord) ~0)

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.

#define cuddAdjust (  )     ((x) = ((x) >= DD_CRI_HI_MARK) ? DD_PLUS_INF_VAL : (((x) <= DD_CRI_LO_MARK) ? DD_MINUS_INF_VAL : (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
#define cuddClean (  )     ((DdNode *)((ptruint)(p) & ~ (ptruint) 0xf))

Clears the 4 least significant bits of a pointer.

Side effects
none
#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
#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
#define cuddDeref (  )     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
#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
#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
#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
#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
#define cuddRef (  )     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
#define cuddSatDec (  )     ((x) -= (x) != (DdHalfWord)DD_MAXREF)

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
#define cuddSatInc (  )     ((x) += (x) != (DdHalfWord)DD_MAXREF)

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
#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
#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
#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
#define DD_ONE ( dd   )     ((dd)->one)

Returns the constant 1 node.

Side effects
none
See also:
DD_ZERO DD_PLUS_INFINITY DD_MINUS_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
#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
#define ddAbs (  )     (((x)<0) ? -(x) : (x))

Computes the absolute value of a number.

Side effects
none
#define ddCHash ( o,
f,
g,
h,
 ) 
Value:
((((((unsigned)(f) + (unsigned)(o)) * DD_P1 + (unsigned)(g)) * DD_P2 + \
   (unsigned)(h)) * DD_P3) >> (s))

Hash function for the cache.

Side effects
none
See also:
ddHash ddCHash2
#define ddCHash2 ( o,
f,
g,
 )     (((((unsigned)(f) + (unsigned)(o)) * DD_P1 + (unsigned)(g)) * DD_P2) >> (s))

Hash function for the cache for functions with two operands.

Side effects
none
See also:
ddHash ddCHash
#define ddEqualVal ( x,
y,
 )     (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
#define ddHash ( f,
g,
 )     ((((unsigned)(f) * DD_P1 + (unsigned)(g)) * DD_P2) >> (s))

Hash function for the unique table.

Side effects
none
See also:
ddCHash ddCHash2
#define ddMax ( x,
 )     (((y) > (x)) ? (y) : (x))

Computes the maximum of two numbers.

Side effects
none
See also:
ddMin
#define ddMin ( x,
 )     (((y) < (x)) ? (y) : (x))

Computes the minimum of two numbers.

Side effects
none
See also:
ddMax
#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

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.

typedef uintptr_t ptruint

Unsigned integer that is the size of a pointer.

See also:
ptrint
 All Data Structures Files Functions Variables Typedefs Enumerations Defines

Generated on 31 Dec 2015 for cudd by  doxygen 1.6.1