Index

ADD

Introduction | Nodes | New Constants | Basic ADD Manipulation

aggregation

Variable Reordering for BDDs

Algebraic Decision Diagram

see ADD

arc

complement

New BDD and ADD | Writing Decision Diagrams to | Writing Decision Diagrams to | Complement Arcs | Complement Arcs

regular

Writing Decision Diagrams to | Writing Decision Diagrams to | Complement Arcs

background value

Background

BDD

Introduction | Nodes | One, Logic Zero, and | Basic BDD Manipulation

Binary Decision Diagram

see BDD

box

black

Introduction

clear

Introduction | Compiling and Linking

cache

Cache | Cache | Cache | Initializing and Shutting Down | Complement Arcs | The Cache

collision

Non Modifiable Parameters

collision list

The Unique Table

deletion

Non Modifiable Parameters

local

The Cache | Local Caches

lossless

Local Caches

reward-based resizing

Cache Sizing | Cache Sizing

sizing

Cache Sizing

cacheSize

Initializing and Shutting Down

canonical

The Manager | Local Caches

compiling

Compiling and Linking | Predefined Constants | Compiling and Linking

configuration

The CUDD Package

conversion

of ADDs to BDDs

Converting ADDs to BDDs

of BDDs to ADDs

Converting ADDs to BDDs

of BDDs to ZDDs

Basic ZDD Manipulation | Converting BDDs to ZDDs

of ZDDs to BDDs

Converting BDDs to ZDDs

cube sets

Introduction

cudd.h

Compiling and Linking | Variable Reordering for BDDs | Saturating Increments and Decrements

Cudd_addApply

Basic ADD Manipulation | Basic ADD Manipulation

Cudd_addBddInterval

Converting ADDs to BDDs

Cudd_addBddPattern

Converting ADDs to BDDs

Cudd_addBddThreshold

Converting ADDs to BDDs

Cudd_addConst

New Constants

Cudd_addHarwell

Background

Cudd_AddHook

Hooks

Cudd_addIthBit

Converting ADDs to BDDs

Cudd_addIthVar

New BDD and ADD

Cudd_addNewVar

New BDD and ADD

Cudd_addNewVarAtLevel

New BDD and ADD | Grouping Variables

Cudd_addRead

Background

Cudd_addTimes

Basic ADD Manipulation

Cudd_AutodynDisable

Variable Reordering for BDDs

Cudd_AutodynDisableZdd

Variable Reordering for ZDDs

Cudd_AutodynEnable

Variable Reordering for BDDs | Variable Reordering for BDDs

Cudd_AutodynEnableZdd

Variable Reordering for ZDDs

Cudd_bddAnd

Basic BDD Manipulation | Basic BDD Manipulation | Basic ADD Manipulation

Cudd_bddAndLimit

Timeouts and Limits

Cudd_bddConstrain

Nodes

Cudd_bddIte

Basic BDD Manipulation

Cudd_bddIthVar

New BDD and ADD

Cudd_bddNewVar

New BDD and ADD | New BDD and ADD | New BDD and ADD

Cudd_bddNewVarAtLevel

New BDD and ADD | Grouping Variables

Cudd_BddToAdd

Converting ADDs to BDDs

Cudd_bddXor

Basic ADD Manipulation

CUDD_CACHE_SLOTS

Initializing and Shutting Down

Cudd_CheckKeys

Debugging

Cudd_CheckZeroRef

Debugging

Cudd_CountMinterm

Background

Cudd_DebugCheck

Debugging

Cudd_DelayedDerefBdd

Non Modifiable Parameters

Cudd_Deref

Cudd_RecursiveDeref vs. Cudd_Deref | Saturating Increments and Decrements

Cudd_DumpBlif

Writing Decision Diagrams to

Cudd_DumpDaVinci

Writing Decision Diagrams to

Cudd_DumpDot

Writing Decision Diagrams to

Cudd_ForeachCube

Nodes | Background

Cudd_ForeachNode

Nodes

Cudd_HookType

Hooks

Cudd_Init

Initializing and Shutting Down | Initializing and Shutting Down

Cudd_MakeTreeNode

Grouping Variables | Grouping Variables

Cudd_MakeZddTreeNode

Variable Reordering for ZDDs

Cudd_Not

One, Logic Zero, and

Cudd_PrintInfo

Gathering and Interpreting Statistics

Cudd_PrintMinterm

Background

Cudd_Quit

Initializing and Shutting Down

Cudd_ReadBackground

Background

Cudd_ReadEpsilon

Predefined Constants

Cudd_ReadErrorCode

NULL Return Values

Cudd_ReadInvPerm

Basic BDD Manipulation

Cudd_ReadLogicZero

One, Logic Zero, and

Cudd_ReadLooseUpto

Setting Parameters

Cudd_ReadMaxGrowth

Variable Reordering for BDDs

Cudd_ReadMinusInfinity

Predefined Constants

Cudd_ReadOne

One, Logic Zero, and

Cudd_ReadPlusInfinity

Predefined Constants

Cudd_ReadReorderings

Allowing Asynchronous Reordering

Cudd_ReadSiftMaxVar

Variable Reordering for BDDs

Cudd_ReadTree

Grouping Variables

Cudd_ReadZddOne

One, Logic Zero, and | Basic ZDD Manipulation

Cudd_ReadZero

Predefined Constants

Cudd_RecursiveDeref

Nodes | Reference Counts | Reference Counts | Reference Counts | Cudd_RecursiveDeref vs. Cudd_Deref | When Increasing the Reference | Saturating Increments and Decrements | Local Caches | Debugging

Cudd_RecursiveDerefZdd

Nodes | Reference Counts | Reference Counts | Reference Counts | When Increasing the Reference | Saturating Increments and Decrements

Cudd_ReduceHeap

Variable Reordering for BDDs | Variable Reordering for BDDs | Variable Reordering for BDDs

Cudd_Ref

Nodes | Basic BDD Manipulation | Reference Counts | When Increasing the Reference

Cudd_Regular

Complement Arcs

CUDD_REORDER_ANNEALING

Variable Reordering for BDDs

CUDD_REORDER_EXACT

Variable Reordering for BDDs

CUDD_REORDER_GENETIC

Variable Reordering for BDDs

CUDD_REORDER_GROUP_SIFT

Variable Reordering for BDDs

CUDD_REORDER_GROUP_SIFT_CONV

Variable Reordering for BDDs

CUDD_REORDER_NONE

Variable Reordering for BDDs | Variable Reordering for ZDDs

CUDD_REORDER_RANDOM

Variable Reordering for BDDs | Variable Reordering for ZDDs

CUDD_REORDER_RANDOM_PIVOT

Variable Reordering for BDDs | Variable Reordering for ZDDs

CUDD_REORDER_SAME

Variable Reordering for BDDs | Variable Reordering for ZDDs

CUDD_REORDER_SIFT

Variable Reordering for BDDs | Variable Reordering for ZDDs

CUDD_REORDER_SIFT_CONVERGE

Variable Reordering for BDDs | Variable Reordering for ZDDs

CUDD_REORDER_SYMM_SIFT

Variable Reordering for BDDs | Variable Reordering for ZDDs

CUDD_REORDER_SYMM_SIFT_CONV

Variable Reordering for BDDs | Variable Reordering for ZDDs

CUDD_REORDER_WINDOW2

Variable Reordering for BDDs

CUDD_REORDER_WINDOW2_CONV

Variable Reordering for BDDs

CUDD_REORDER_WINDOW3

Variable Reordering for BDDs

CUDD_REORDER_WINDOW3_CONV

Variable Reordering for BDDs

CUDD_REORDER_WINDOW4

Variable Reordering for BDDs

CUDD_REORDER_WINDOW4_CONV

Variable Reordering for BDDs

Cudd_SetEpsilon

Predefined Constants

Cudd_SetLooseUpTo

Setting Parameters

Cudd_SetMaxCacheHard

Modifiable Parameters

Cudd_SetMaxGrowth

Variable Reordering for BDDs

Cudd_SetSiftMaxVar

Variable Reordering for BDDs

Cudd_SetTimeLimit

Timeouts and Limits

Cudd_SetTree

Grouping Variables

Cudd_ShuffleHeap

Variable Reordering for BDDs

Cudd_StdPostReordHook

Hooks

Cudd_StdPreReordHook

Hooks

Cudd_SymmProfile

Variable Reordering for BDDs

CUDD_UNIQUE_SLOTS

Initializing and Shutting Down

Cudd_zddDumpDot

Writing Decision Diagrams to

Cudd_zddIsop

Basic ZDD Manipulation

Cudd_zddIthVar

New ZDD Variables

Cudd_zddPortFromBdd

Converting BDDs to ZDDs

Cudd_zddPortToBdd

Converting BDDs to ZDDs

Cudd_zddRealignDisable

Keeping Consistent Variable Orders

Cudd_zddRealignEnable

Keeping Consistent Variable Orders

Cudd_zddReduceHeap

Variable Reordering for ZDDs

Cudd_zddShuffleHeap

Variable Reordering for ZDDs

Cudd_zddVarsFromBddVars

Converting BDDs to ZDDs | Converting BDDs to ZDDs

Cudd_zddWeakDiv

Basic ZDD Manipulation

cuddCacheInsert

The Cache

cuddCacheInsert1

The Cache

cuddCacheInsert2

The Cache

cuddCacheLookup

The Cache

cuddCacheLookup1

The Cache

cuddCacheLookup2

The Cache

CUDDDIR

Using the CUDD Package

cuddHeapProfile

Debugging

cuddI

The Unique Table

cuddInt.h

Debugging

cuddIZ

The Unique Table

cuddSatDec

Saturating Increments and Decrements

cuddSatInc

Saturating Increments and Decrements

cuddUniqueConst

Reference Counts | Reference Counts | Reference Counts

cuddUniqueInter

Reference Counts | Reference Counts | Reference Counts | Complement Arcs | Complement Arcs | Allowing Asynchronous Reordering | Allowing Asynchronous Reordering | Allowing Asynchronous Reordering

cuddUniqueInterZdd

Reference Counts | Reference Counts | Reference Counts | Allowing Asynchronous Reordering

DD_CACHE_PROFILE

Extended Statistics and Reporting

DD_DEBUG

Debugging

DD_STATS

Extended Statistics and Reporting

DD_UNIQUE_PROFILE

Extended Statistics and Reporting

DD_VERBOSE

Extended Statistics and Reporting

DdManager

The Manager | Initializing and Shutting Down

DdNode

Nodes | The Cache

debugging

Debugging

DEC Alpha

Predefined Constants | Using the CUDD Package

documentation

Guidelines for Documentation

Description

Guidelines for Documentation

HTML files

Guidelines for Documentation

SeeAlso

Guidelines for Documentation

Synopsis

Guidelines for Documentation

dot

see graph, drawing

Epsilon

Predefined Constants

extdoc

see documentation

floating point

Predefined Constants

double (C type)

Nodes

IEEE Standard 754

Predefined Constants

free list

Reference Counts

FTP

The CUDD Package | CUDD Friends | Using the CUDD Package | Guidelines for Documentation

function

characteristic

Introduction | Converting BDDs to ZDDs

cover

Basic ZDD Manipulation | Converting BDDs to ZDDs | Converting BDDs to ZDDs

irredundant

Basic ZDD Manipulation

minterms

Background | Allowing Asynchronous Reordering

ON-set

Introduction

sum of products

Background

switching

Introduction | Introduction

garbage collection

Nodes | Cache | Setting Parameters | Reference Counts | Reference Counts | The Cache | Local Caches | The Unique Table

hooks

Hooks

gcc

Predefined Constants

generator

Nodes

global variables

The Manager

graph

arc capacity

Background

arc length

Background

drawing

Writing Decision Diagrams to | Writing Decision Diagrams to

growth

Setting Parameters

gzip

The CUDD Package

HAVE_IEEE_754

Predefined Constants

header files

Variable Reordering for BDDs | Saturating Increments and Decrements

hook

Hooks

infinities

Predefined Constants

installation

The CUDD Package

Intel Pentium 4

The CUDD Package

interface

cache

The Cache

SIS

The SIS/VIS Interface | Using the CUDD Package

VIS

The SIS/VIS Interface

libraries

The CUDD Package

cudd

Compiling and Linking

dddmp

Saving and Restoring BDDs

mtr

Compiling and Linking | Grouping Variables

obj

Compiling and Linking

st

Compiling and Linking | The Cache

util

Compiling and Linking

Makefile

Compiling and Linking | Predefined Constants | Compiling and Linking

manager

The Manager | The Manager | Constant Functions

matrix

sparse

Background

maxCache

Cache Sizing

maxMemory

Initializing and Shutting Down

MinusInfinity

Predefined Constants

MTR_DEFAULT

Grouping Variables

MTR_FIXED

Grouping Variables

nanotrav

The CUDD Package | The CUDD Package

node

Nodes

constant

Nodes | Constant Functions | One, Logic Zero, and | Predefined Constants | Background | New Constants | Reference Counts | When Increasing the Reference

value

Nodes

dead

Reference Counts | The Cache | The Unique Table

dereference

Basic ADD Manipulation

reclaimed

The Unique Table

recycling

Nodes

reference

Basic ADD Manipulation

reference count

Nodes | Nodes | Basic BDD Manipulation | Basic BDD Manipulation | Reference Counts | Reference Counts | Reference Counts | When Increasing the Reference | Saturating Increments and Decrements | The Cache | Local Caches | Debugging

saturated

Debugging

terminal

see node, constant

variable index

Nodes

numSlots

Initializing and Shutting Down

numVars

Initializing and Shutting Down

numVarsZ

Initializing and Shutting Down

PlusInfinity

Predefined Constants | Background

projection functions

Creating Variables | New BDD and ADD | New BDD and ADD | New BDD and ADD | New ZDD Variables | Basic BDD Manipulation | Basic ADD Manipulation | Basic ZDD Manipulation | Basic ZDD Manipulation | Debugging

README file

The CUDD Package | The CUDD Package

reordering

Introduction | Introduction | Nodes | The Cache

abort and retry

Allowing Asynchronous Reordering

asynchronous

Variable Reordering for BDDs | Allowing Asynchronous Reordering

converging

Variable Reordering for BDDs | Variable Reordering for BDDs | Variable Reordering for BDDs | Variable Reordering for BDDs

Cudd_ReorderingType

Variable Reordering for BDDs

dynamic

Introduction | Variable Reordering for BDDs | Variable Reordering for ZDDs

exact

Variable Reordering for BDDs

function wrapper

Allowing Asynchronous Reordering | Allowing Asynchronous Reordering

genetic

Variable Reordering for BDDs

group

Variable Reordering for BDDs | Variable Reordering for BDDs

hooks

Hooks

interruptible procedure

Allowing Asynchronous Reordering

of BDDs and ADDs

Variable Reordering for BDDs

of ZDDs

Basic ZDD Manipulation | Variable Reordering for ZDDs

random

Variable Reordering for BDDs

sifting

Variable Reordering for BDDs | Variable Reordering for BDDs

simulated annealing

Variable Reordering for BDDs

symmetric

Variable Reordering for BDDs

threshold

Variable Reordering for BDDs | Allowing Asynchronous Reordering

window

Variable Reordering for BDDs

saturating

decrements

Saturating Increments and Decrements

increments

Saturating Increments and Decrements

SISDIR

Using the CUDD Package

SIZEOF_INT

Saturating Increments and Decrements | Saturating Increments and Decrements

SIZEOF_VOID_P

Saturating Increments and Decrements | Saturating Increments and Decrements

statistical counters

The Manager | Reference Counts | Cache Sizing

statistics

Gathering and Interpreting Statistics

subtable

Initializing and Shutting Down | Reference Counts

symmetry

Variable Reordering for BDDs

table

computed

Cache

growth

Setting Parameters

hash

The Manager | The Unique Table

unique

Nodes | The Manager | The Manager | Initializing and Shutting Down | Initializing and Shutting Down | Setting Parameters | Variable Reordering for BDDs | Reference Counts | Cache Sizing | Cache Sizing | The Unique Table

fast growth

The Unique Table

reward-based resizing

The Unique Table

slow growth

The Unique Table

timeout

Timeouts and Limits

variable

groups

Grouping Variables

order

Nodes | New BDD and ADD

permutation

Nodes | The Unique Table

tree

Grouping Variables | Grouping Variables

ZDD

Introduction | Nodes | New ZDD Variables | Basic ZDD Manipulation | Converting BDDs to ZDDs

zero

arithmetic

One, Logic Zero, and | New BDD and ADD | Converting ADDs to BDDs

logical

One, Logic Zero, and | Converting ADDs to BDDs

Zero-suppressed Binary Decision Diagram

see ZDD