Browse Source

Merge branch 'future' into monolithic-dft

Former-commit-id: 1336ad7295
main
sjunges 9 years ago
parent
commit
1d0debc79c
  1. 20
      CMakeLists.txt
  2. 19
      resources/3rdparty/CMakeLists.txt
  3. 42
      resources/3rdparty/cudd-2.5.0/CMakeLists.txt
  4. 323
      resources/3rdparty/cudd-2.5.0/Makefile
  5. 177
      resources/3rdparty/cudd-2.5.0/README
  6. 131
      resources/3rdparty/cudd-2.5.0/RELEASE.NOTES
  7. 18
      resources/3rdparty/cudd-2.5.0/setup.sh
  8. 2
      resources/3rdparty/cudd-2.5.0/shutdown.sh
  9. 124
      resources/3rdparty/cudd-2.5.0/src/cudd/Makefile
  10. 1090
      resources/3rdparty/cudd-2.5.0/src/cudd/cudd.h
  11. 4893
      resources/3rdparty/cudd-2.5.0/src/cudd/cuddAPI.c
  12. 960
      resources/3rdparty/cudd-2.5.0/src/cudd/cuddGenetic.c
  13. 1190
      resources/3rdparty/cudd-2.5.0/src/cudd/cuddInt.h
  14. 1331
      resources/3rdparty/cudd-2.5.0/src/cudd/cuddSubsetHB.c
  15. 6776
      resources/3rdparty/cudd-2.5.0/src/cudd/doc/cudd.doc
  16. 5036
      resources/3rdparty/cudd-2.5.0/src/cudd/doc/cudd.ps
  17. 3114
      resources/3rdparty/cudd-2.5.0/src/cudd/doc/cuddAllAbs.html
  18. 13
      resources/3rdparty/cudd-2.5.0/src/cudd/doc/cuddAllByFile.html
  19. 13
      resources/3rdparty/cudd-2.5.0/src/cudd/doc/cuddAllByFunc.html
  20. 15754
      resources/3rdparty/cudd-2.5.0/src/cudd/doc/cuddAllDet.html
  21. 4876
      resources/3rdparty/cudd-2.5.0/src/cudd/doc/cuddAllFile.html
  22. 33
      resources/3rdparty/cudd-2.5.0/src/cudd/doc/cuddDesc.html
  23. 14
      resources/3rdparty/cudd-2.5.0/src/cudd/doc/cuddExt.html
  24. 1415
      resources/3rdparty/cudd-2.5.0/src/cudd/doc/cuddExtAbs.html
  25. 4450
      resources/3rdparty/cudd-2.5.0/src/cudd/doc/cuddExtDet.html
  26. 30
      resources/3rdparty/cudd-2.5.0/src/cudd/doc/cuddIntro.css
  27. 219
      resources/3rdparty/cudd-2.5.0/src/cudd/doc/cuddIntro.html
  28. 18
      resources/3rdparty/cudd-2.5.0/src/cudd/doc/cuddTitle.html
  29. 109
      resources/3rdparty/cudd-2.5.0/src/cudd/doc/footnode.html
  30. BIN
      resources/3rdparty/cudd-2.5.0/src/cudd/doc/icons/blueball.png
  31. BIN
      resources/3rdparty/cudd-2.5.0/src/cudd/doc/icons/ch_beg_r.png
  32. BIN
      resources/3rdparty/cudd-2.5.0/src/cudd/doc/icons/ch_begin.png
  33. BIN
      resources/3rdparty/cudd-2.5.0/src/cudd/doc/icons/ch_del_r.png
  34. BIN
      resources/3rdparty/cudd-2.5.0/src/cudd/doc/icons/ch_delet.png
  35. BIN
      resources/3rdparty/cudd-2.5.0/src/cudd/doc/icons/ch_end.png
  36. BIN
      resources/3rdparty/cudd-2.5.0/src/cudd/doc/icons/ch_end_r.png
  37. BIN
      resources/3rdparty/cudd-2.5.0/src/cudd/doc/icons/contents.png
  38. BIN
      resources/3rdparty/cudd-2.5.0/src/cudd/doc/icons/crossref.png
  39. BIN
      resources/3rdparty/cudd-2.5.0/src/cudd/doc/icons/footnote.png
  40. BIN
      resources/3rdparty/cudd-2.5.0/src/cudd/doc/icons/greenball.png
  41. BIN
      resources/3rdparty/cudd-2.5.0/src/cudd/doc/icons/image.png
  42. BIN
      resources/3rdparty/cudd-2.5.0/src/cudd/doc/icons/index.png
  43. BIN
      resources/3rdparty/cudd-2.5.0/src/cudd/doc/icons/next.png
  44. BIN
      resources/3rdparty/cudd-2.5.0/src/cudd/doc/icons/next_g.png
  45. BIN
      resources/3rdparty/cudd-2.5.0/src/cudd/doc/icons/nx_grp.png
  46. BIN
      resources/3rdparty/cudd-2.5.0/src/cudd/doc/icons/nx_grp_g.png
  47. BIN
      resources/3rdparty/cudd-2.5.0/src/cudd/doc/icons/orangeball.png
  48. BIN
      resources/3rdparty/cudd-2.5.0/src/cudd/doc/icons/pinkball.png
  49. BIN
      resources/3rdparty/cudd-2.5.0/src/cudd/doc/icons/prev.png
  50. BIN
      resources/3rdparty/cudd-2.5.0/src/cudd/doc/icons/prev_g.png
  51. BIN
      resources/3rdparty/cudd-2.5.0/src/cudd/doc/icons/purpleball.png
  52. BIN
      resources/3rdparty/cudd-2.5.0/src/cudd/doc/icons/pv_grp.png
  53. BIN
      resources/3rdparty/cudd-2.5.0/src/cudd/doc/icons/pv_grp_g.png
  54. BIN
      resources/3rdparty/cudd-2.5.0/src/cudd/doc/icons/redball.png
  55. BIN
      resources/3rdparty/cudd-2.5.0/src/cudd/doc/icons/up.png
  56. BIN
      resources/3rdparty/cudd-2.5.0/src/cudd/doc/icons/up_g.png
  57. BIN
      resources/3rdparty/cudd-2.5.0/src/cudd/doc/icons/whiteball.png
  58. BIN
      resources/3rdparty/cudd-2.5.0/src/cudd/doc/icons/yellowball.png
  59. BIN
      resources/3rdparty/cudd-2.5.0/src/cudd/doc/img1.png
  60. BIN
      resources/3rdparty/cudd-2.5.0/src/cudd/doc/img10.png
  61. BIN
      resources/3rdparty/cudd-2.5.0/src/cudd/doc/img11.png
  62. BIN
      resources/3rdparty/cudd-2.5.0/src/cudd/doc/img12.png
  63. BIN
      resources/3rdparty/cudd-2.5.0/src/cudd/doc/img13.png
  64. BIN
      resources/3rdparty/cudd-2.5.0/src/cudd/doc/img14.png
  65. BIN
      resources/3rdparty/cudd-2.5.0/src/cudd/doc/img15.png
  66. BIN
      resources/3rdparty/cudd-2.5.0/src/cudd/doc/img16.png
  67. BIN
      resources/3rdparty/cudd-2.5.0/src/cudd/doc/img17.png
  68. BIN
      resources/3rdparty/cudd-2.5.0/src/cudd/doc/img18.png
  69. BIN
      resources/3rdparty/cudd-2.5.0/src/cudd/doc/img19.png
  70. BIN
      resources/3rdparty/cudd-2.5.0/src/cudd/doc/img2.png
  71. BIN
      resources/3rdparty/cudd-2.5.0/src/cudd/doc/img20.png
  72. BIN
      resources/3rdparty/cudd-2.5.0/src/cudd/doc/img21.png
  73. BIN
      resources/3rdparty/cudd-2.5.0/src/cudd/doc/img22.png
  74. BIN
      resources/3rdparty/cudd-2.5.0/src/cudd/doc/img3.png
  75. BIN
      resources/3rdparty/cudd-2.5.0/src/cudd/doc/img4.png
  76. BIN
      resources/3rdparty/cudd-2.5.0/src/cudd/doc/img5.png
  77. BIN
      resources/3rdparty/cudd-2.5.0/src/cudd/doc/img6.png
  78. BIN
      resources/3rdparty/cudd-2.5.0/src/cudd/doc/img7.png
  79. BIN
      resources/3rdparty/cudd-2.5.0/src/cudd/doc/img8.png
  80. BIN
      resources/3rdparty/cudd-2.5.0/src/cudd/doc/img9.png
  81. 219
      resources/3rdparty/cudd-2.5.0/src/cudd/doc/index.html
  82. 174
      resources/3rdparty/cudd-2.5.0/src/cudd/doc/node1.html
  83. 175
      resources/3rdparty/cudd-2.5.0/src/cudd/doc/node2.html
  84. 1637
      resources/3rdparty/cudd-2.5.0/src/cudd/doc/node3.html
  85. 1165
      resources/3rdparty/cudd-2.5.0/src/cudd/doc/node4.html
  86. 130
      resources/3rdparty/cudd-2.5.0/src/cudd/doc/node5.html
  87. 132
      resources/3rdparty/cudd-2.5.0/src/cudd/doc/node6.html
  88. 195
      resources/3rdparty/cudd-2.5.0/src/cudd/doc/node7.html
  89. 848
      resources/3rdparty/cudd-2.5.0/src/cudd/doc/node8.html
  90. 396
      resources/3rdparty/cudd-2.5.0/src/cudd/r7x8.1.out
  91. 243
      resources/3rdparty/cudd-2.5.0/src/dddmp/Makefile
  92. 455
      resources/3rdparty/cudd-2.5.0/src/dddmp/dddmpDdNodeBdd.c
  93. 944
      resources/3rdparty/cudd-2.5.0/src/dddmp/dddmpDdNodeCnf.c
  94. 269
      resources/3rdparty/cudd-2.5.0/src/dddmp/exp/runAllTest.out
  95. 11
      resources/3rdparty/cudd-2.5.0/src/dddmp/exp/runAllTest.script
  96. 44
      resources/3rdparty/cudd-2.5.0/src/dddmp/exp/test1.out
  97. 23
      resources/3rdparty/cudd-2.5.0/src/dddmp/exp/test2.out
  98. 18
      resources/3rdparty/cudd-2.5.0/src/dddmp/exp/test3.out
  99. 69
      resources/3rdparty/cudd-2.5.0/src/dddmp/exp/test3.script
  100. 24
      resources/3rdparty/cudd-2.5.0/src/dddmp/exp/test4.out

20
CMakeLists.txt

@ -12,6 +12,7 @@ include_directories("${PROJECT_SOURCE_DIR}/src")
set(CMAKE_MODULE_PATH ${CMAKE_MODULE_PATH} "${PROJECT_SOURCE_DIR}/resources/cmake/")
include(ExternalProject)
#############################################################
##
## CMake options of StoRM
@ -181,6 +182,7 @@ message(STATUS "StoRM - Using Compiler Configuration: ${STORM_COMPILED_BY}")
#############################################################
add_subdirectory(resources/3rdparty)
# Add the version of GMM in the repository to the include pathes
set(GMMXX_INCLUDE_DIR "${PROJECT_SOURCE_DIR}/resources/3rdparty/gmm-5.0/include")
include_directories(${GMMXX_INCLUDE_DIR})
@ -433,19 +435,10 @@ endif()
## CUDD
##
#############################################################
add_subdirectory("${PROJECT_SOURCE_DIR}/resources/3rdparty/cudd-2.5.0")
include_directories("${PROJECT_SOURCE_DIR}/resources/3rdparty/cudd-2.5.0/src/cudd")
include_directories("${PROJECT_SOURCE_DIR}/resources/3rdparty/cudd-2.5.0/src/epd")
include_directories("${PROJECT_SOURCE_DIR}/resources/3rdparty/cudd-2.5.0/src/mtr")
include_directories("${PROJECT_SOURCE_DIR}/resources/3rdparty/cudd-2.5.0/src/nanotrav")
include_directories("${PROJECT_SOURCE_DIR}/resources/3rdparty/cudd-2.5.0/src/obj")
include_directories("${PROJECT_SOURCE_DIR}/resources/3rdparty/cudd-2.5.0/src/st")
include_directories("${PROJECT_SOURCE_DIR}/resources/3rdparty/cudd-2.5.0/src/util")
list(APPEND STORM_LINK_LIBRARIES cudd)
message("${CUDD3_INCLUDE_DIR}")
include_directories(${CUDD3_INCLUDE_DIR})
list(APPEND STORM_LINK_LIBRARIES ${CUDD3_SHARED_LIBRARIES})
#############################################################
##
@ -543,7 +536,7 @@ endif()
## Sylvan
##
#############################################################
include(ExternalProject)
set(STORM_SYLVAN_ROOT "${PROJECT_SOURCE_DIR}/resources/3rdparty/sylvan")
ExternalProject_Add(
sylvan
@ -728,7 +721,6 @@ set(STORM_GENERATED_SOURCES "${PROJECT_BINARY_DIR}/src/utility/storm-version.cpp
# Add the binary dir include directory for storm-config.h
include_directories("${PROJECT_BINARY_DIR}/include")
add_subdirectory(resources/3rdparty)
add_subdirectory(src)
add_subdirectory(test)

19
resources/3rdparty/CMakeLists.txt

@ -1,6 +1,7 @@
add_custom_target(resources)
add_custom_target(test-resources)
if(STORM_SUPPORT_XML_INPUT_FORMATS)
ExternalProject_Add(
xercesc
@ -32,6 +33,24 @@ ExternalProject_Add(
add_dependencies(resources glpk)
ExternalProject_Add(
cudd3
DOWNLOAD_COMMAND ""
SOURCE_DIR ${CMAKE_CURRENT_SOURCE_DIR}/cudd-3.0.0
PREFIX ${CMAKE_CURRENT_BINARY_DIR}/cudd-3.0.0
CONFIGURE_COMMAND ${CMAKE_CURRENT_SOURCE_DIR}/cudd-3.0.0/configure --enable-shared --enable-obj --prefix=${CMAKE_CURRENT_BINARY_DIR}/cudd-3.0.0 --libdir=${CMAKE_CURRENT_BINARY_DIR}/cudd-3.0.0/lib CC=${CMAKE_C_COMPILER} CXX=${CMAKE_CXX_COMPILER}
BUILD_COMMAND make "CFLAGS=-O2 -w"
INSTALL_COMMAND make install
BUILD_IN_SOURCE 0
)
add_dependencies(resources cudd3)
ExternalProject_Get_Property(cudd3 binary_dir)
set(CUDD3_INCLUDE_DIR ${CMAKE_CURRENT_BINARY_DIR}/cudd-3.0.0/include PARENT_SCOPE)
set(CUDD3_SHARED_LIBRARIES ${CMAKE_CURRENT_BINARY_DIR}/cudd-3.0.0/lib/libcudd${DYNAMIC_EXT} PARENT_SCOPE)
set(CUDD3_STATIC_LIBRARIES ${CMAKE_CURRENT_BINARY_DIR}/cudd-3.0.0/liblibcudd${STATIC_EXT} PARENT_SCOPE)
ExternalProject_Add(
googletest
#For downloads (may be useful later!)

42
resources/3rdparty/cudd-2.5.0/CMakeLists.txt

@ -1,42 +0,0 @@
cmake_minimum_required (VERSION 2.8.6)
# Set project name
project (cudd C CXX)
# Main Sources
file(GLOB_RECURSE CUDD_HEADERS ${PROJECT_SOURCE_DIR}/src/*.h)
file(GLOB_RECURSE CUDD_HEADERS_CXX ${PROJECT_SOURCE_DIR}/src/*.hh)
file(GLOB_RECURSE CUDD_SOURCES ${PROJECT_SOURCE_DIR}/src/*.c)
file(GLOB_RECURSE CUDD_SOURCES_CXX ${PROJECT_SOURCE_DIR}/src/*.cc)
# Add base folder for better inclusion paths
include_directories("${PROJECT_SOURCE_DIR}/src")
include_directories("${PROJECT_SOURCE_DIR}/src/cudd")
include_directories("${PROJECT_SOURCE_DIR}/src/dddmp")
include_directories("${PROJECT_SOURCE_DIR}/src/epd")
include_directories("${PROJECT_SOURCE_DIR}/src/mtr")
include_directories("${PROJECT_SOURCE_DIR}/src/nanotrav")
include_directories("${PROJECT_SOURCE_DIR}/src/st")
include_directories("${PROJECT_SOURCE_DIR}/src/util")
if(CMAKE_COMPILER_IS_GNUCC)
set(CMAKE_C_FLAGS "${CMAKE_C_FLAGS} -Wno-unused-variable -Wno-unused-but-set-variable -Wno-unused-function")
elseif(MSVC)
# required for GMM to compile, ugly error directive in their code
add_definitions(/D_SCL_SECURE_NO_DEPRECATE /D_CRT_SECURE_NO_WARNINGS)
else(CLANG)
set(CMAKE_C_FLAGS "${CMAKE_C_FLAGS} -Wno-newline-eof -Wno-unneeded-internal-declaration -Wno-unused-variable -Wno-unused-const-variable -Wno-parentheses-equality")
endif()
# Since we do not target Alphas, this symbol is always set
add_definitions(-DHAVE_IEEE_754)
if(CMAKE_SIZEOF_VOID_P EQUAL 8)
message(STATUS "CUDD: Targeting 64bit architecture")
add_definitions(-DSIZEOF_VOID_P=8)
add_definitions(-DSIZEOF_LONG=8)
endif()
# Add the library
add_library(cudd STATIC ${CUDD_SOURCES} ${CUDD_HEADERS} ${CUDD_HEADERS_CXX} ${CUDD_SOURCES_CXX})

323
resources/3rdparty/cudd-2.5.0/Makefile

@ -1,323 +0,0 @@
# $Id$
#
# Makefile for the CUDD distribution kit
#---------------------------------------------------------------------------
# Beginning of the configuration section. These symbol definitions can
# be overridden from the command line.
# C++ compiler
#CXX = g++
#CXX = icpc
#CXX = ecpc
#CXX = CC
#CXX = /usr/local/opt/SUNWspro/bin/CC
#CXX = cxx
CXX = clang++
# Specific options for compilation of C++ files.
CXXFLAGS = -std=c++11 -stdlib=libc++
# Stricter standard conformance for g++.
#CXXFLAGS = -std=c++98
# For Sun CC version 5, this invokes compatibility mode.
#CXXFLAGS = -compat
# On some versions of UP-UX, it is necessary to pass the option +a1
# to CC for the C++ test program to compile successfully.
#CXXFLAGS = +a1
# C compiler used for all targets except optimize_dec, which always uses cc.
#CC = cc
#CC = /usr/local/opt/SUNWspro/bin/cc
#CC = gcc
#CC = icc
#CC = ecc
#CC = /usr/ucb/cc
#CC = c89
#CC = $(CXX)
CC = clang
# On some machines ranlib is either non-existent or redundant.
# Use the following definition if your machine has ranlib and you think
# it is needed.
RANLIB = ranlib
# Use the following definition if your machine either does not have
# ranlib (e.g., SUN running solaris) or can do without it (e.g., DEC Alpha).
#RANLIB = :
# Use ICFLAGS to specify machine-independent compilation flags.
# These three are typical settings for cc.
#ICFLAGS = -g
#ICFLAGS = -O
#ICFLAGS =
# These two are typical settings for optimized code with gcc.
#ICFLAGS = -g -O3 -Wall
ICFLAGS = -O4
# Use XCFLAGS to specify machine-dependent compilation flags.
# For some platforms no special flags are needed.
#XCFLAGS = -DHAVE_IEEE_754 -DBSD
#
#==========================
# Linux
#
# Gcc 4.2.4 or higher on i686.
XCFLAGS = -arch x86_64 -DHAVE_IEEE_754 -DBSD -DSIZEOF_VOID_P=8 -DSIZEOF_LONG=8
# Gcc 3.2.2 or higher on i686.
#XCFLAGS = -mtune=pentium4 -malign-double -DHAVE_IEEE_754 -DBSD
# Gcc 2.8.1 on i686.
#XCFLAGS = -mcpu=pentiumpro -malign-double -DHAVE_IEEE_754 -DBSD
# Gcc 4.2.4 or higher on x86_64 (64-bit compilation)
#XCFLAGS = -mtune=native -DHAVE_IEEE_754 -DBSD -DSIZEOF_VOID_P=8 -DSIZEOF_LONG=8
# Gcc 4.2.4 or higher on x86_64 (32-bit compilation)
#XCFLAGS = -m32 -mtune=native -malign-double -DHAVE_IEEE_754 -DBSD
# Icc on i686 (older versions may not support -xHost).
#XCFLAGS = -ansi -xHost -align -ip -DHAVE_IEEE_754 -DBSD
# Icc on x86_64 (64-bit compilation).
#XCFLAGS = -ansi -xHost -align -ip -DHAVE_IEEE_754 -DBSD -DSIZEOF_VOID_P=8 -DSIZEOF_LONG=8
# Gcc on ia64.
#XCFLAGS = -DHAVE_IEEE_754 -DBSD -DSIZEOF_VOID_P=8 -DSIZEOF_LONG=8
# Icc/ecc on ia64.
#XCFLAGS = -ansi -DBSD -DHAVE_IEEE_754 -DSIZEOF_VOID_P=8 -DSIZEOF_LONG=8
#
#==========================
# Solaris
#
# For Solaris, BSD should not be replaced by UNIX100.
#XCFLAGS = -DHAVE_IEEE_754 -DUNIX100 -DEPD_BIG_ENDIAN
# Gcc 2.8.1 or higher on Ultrasparc.
#XCFLAGS = -mcpu=ultrasparc -DHAVE_IEEE_754 -DUNIX100 -DEPD_BIG_ENDIAN
# For Solaris 2.5 and higher, optimized code with /usr/bin/cc or CC.
#XCFLAGS = -DHAVE_IEEE_754 -DUNIX100 -xO5 -native -dalign -DEPD_BIG_ENDIAN
# On IA platforms, -dalign is not supported and causes warnings.
#XCFLAGS = -DHAVE_IEEE_754 -DUNIX100 -xO5 -native
# Recent Sun compilers won't let you use -native on old Ultras.
#XCFLAGS = -DHAVE_IEEE_754 -DUNIX100 -xO5 -dalign -xlibmil -DEPD_BIG_ENDIAN
# For Solaris 2.4, optimized code with /usr/bin/cc.
#XCFLAGS = -DHAVE_IEEE_754 -DUNIX100 -xO4 -dalign -DEPD_BIG_ENDIAN
# For Solaris 2.5 and higher, optimized code with /usr/ucb/cc.
#XCFLAGS = -DHAVE_IEEE_754 -DBSD -xO5 -native -dalign -DEPD_BIG_ENDIAN
#XCFLAGS = -DHAVE_IEEE_754 -DBSD -xO5 -dalign -xlibmil -DEPD_BIG_ENDIAN
# For Solaris 2.4, optimized code with /usr/ucb/cc.
#XCFLAGS = -DHAVE_IEEE_754 -DBSD -xO4 -dalign -DEPD_BIG_ENDIAN
#
#==========================
# DEC Alphas running Digital Unix
#
# For DEC Alphas either -ieee_with_inexact or -ieee_with_no_inexact is
# needed. If you use only BDDs, -ieee_with_no_inexact is enough.
# In the following, we consider three different compilers:
# - the old native compiler (the one of MIPS ancestry that produces u-code);
# - the new native compiler;
# - gcc
# On the Alphas, gcc (as of release 2.7.2) does not support 32-bit pointers
# and IEEE 754 floating point arithmetic. Therefore, for this architecture
# only, the native compilers provide a substatial advantage.
# With the native compilers, specify -xtaso for 32-bit pointers.
# Do not use -xtaso_short because explicit reference to stdout and stderr
# does not work with this option. (Among other things.)
# Notice that -taso must be included in LDFLAGS for -xtaso to work.
# Given the number of possible choices, only some typical configurations
# are proposed here.
#
# Old native compiler for the Alphas; 64-bit pointers.
#XCFLAGS = -DBSD -DHAVE_IEEE_754 -ieee_with_no_inexact -tune host -DSIZEOF_VOID_P=8 -DSIZEOF_LONG=8
# Old native compiler for the Alphas; 32-bit pointers.
#XCFLAGS = -DBSD -DHAVE_IEEE_754 -ieee_with_no_inexact -tune host -xtaso -DSIZEOF_LONG=8
# New native compiler for the Alphas; 64-bit pointers.
#XCFLAGS = -g3 -O4 -std -DBSD -DHAVE_IEEE_754 -ieee_with_no_inexact -tune host -DSIZEOF_VOID_P=8 -DSIZEOF_LONG=8
# New native compiler for the Alphas; 32-bit pointers.
#XCFLAGS = -g3 -O4 -std -DBSD -DHAVE_IEEE_754 -ieee_with_no_inexact -tune host -xtaso -DSIZEOF_LONG=8
# gcc for the Alphas: compile without HAVE_IEEE_754.
#XCFLAGS = -DBSD -DSIZEOF_VOID_P=8 -DSIZEOF_LONG=8
#
#==========================
#
# IBM RS6000
#
# For the IBM RS6000 -qstrict is necessary when specifying -O3 with cc.
#XCFLAGS = -DBSD -DHAVE_IEEE_754 -DEPD_BIG_ENDIAN -O3 -qstrict
#
#==========================
#
# HP-UX
#
# I haven't figured out how to enable IEEE 754 on the HPs I've tried...
# For HP-UX using gcc.
#XCFLAGS = -DUNIX100 -DEPD_BIG_ENDIAN
# For HP-UX using c89.
#XCFLAGS = +O3 -DUNIX100 -DEPD_BIG_ENDIAN
#
#==========================
#
# Windows 95/98/NT/XP/Vista/7 with Cygwin tools
#
# The value of RLIMIT_DATA_DEFAULT should reflect the amount of
# available memory (expressed in bytes).
# Recent versions of cygwin have getrlimit, but the datasize limit
# cannot be set.
#XCFLAGS = -mtune=native -malign-double -DHAVE_IEEE_754 -DHAVE_GETRLIMIT=0 -DRLIMIT_DATA_DEFAULT=268435456
# Define the level of self-checking and verbosity of the CUDD package.
#DDDEBUG = -DDD_DEBUG -DDD_VERBOSE -DDD_STATS -DDD_CACHE_PROFILE -DDD_UNIQUE_PROFILE -DDD_COUNT
DDDEBUG =
# Define the level of self-checking and verbosity of the MTR package.
#MTRDEBUG = -DMTR_DEBUG
MTRDEBUG =
# Loader options.
LDFLAGS =
# This may produce faster code on the DECstations.
#LDFLAGS = -jmpopt -Olimit 1000
# This may be necessary under some old versions of Linux.
#LDFLAGS = -static
# This normally makes the program faster on the DEC Alphas.
#LDFLAGS = -non_shared -om
# This is for 32-bit pointers on the DEC Alphas.
#LDFLAGS = -non_shared -om -taso
#LDFLAGS = -non_shared -taso
# Define PURE as purify to link with purify.
# Define PURE as quantify to link with quantify.
# Remember to compile with -g if you want line-by-line info with quantify.
PURE =
#PURE = purify
#PURE = quantify
# Define EXE as .exe for MS-DOS and derivatives. Not required by recent
# versions of cygwin.
EXE =
#EXE = .exe
# End of the configuration section.
#---------------------------------------------------------------------------
MFLAG = -DMNEMOSYNE
MNEMLIB = ../mnemosyne/libmnem.a
DDWDIR = .
IDIR = $(DDWDIR)/include
INCLUDE = -I$(IDIR)
BDIRS = cudd dddmp mtr st util epd obj
DIRS = $(BDIRS)
#------------------------------------------------------------------------
.PHONY : build
.PHONY : nanotrav
.PHONY : check_leaks
.PHONY : optimize_dec
.PHONY : testcudd
.PHONY : libobj
.PHONY : testobj
.PHONY : testdddmp
.PHONY : testmtr
.PHONY : lint
.PHONY : all
.PHONY : clean
.PHONY : distclean
build:
sh ./setup.sh
@for dir in $(DIRS); do \
(cd $$dir; \
echo Making $$dir ...; \
make CC=$(CC) RANLIB=$(RANLIB) MFLAG= MNEMLIB= ICFLAGS="$(ICFLAGS)" XCFLAGS="$(XCFLAGS)" DDDEBUG="$(DDDEBUG)" MTRDEBUG="$(MTRDEBUG)" LDFLAGS="$(LDFLAGS)" PURE="$(PURE)" EXE="$(EXE)" )\
done
nanotrav: build
check_leaks:
sh ./setup.sh
@for dir in mnemosyne $(DIRS); do \
(cd $$dir; \
echo Making $$dir ...; \
make CC=$(CC) RANLIB=$(RANLIB) MFLAG=$(MFLAG) MNEMLIB=$(MNEMLIB) ICFLAGS="$(ICFLAGS)" XCFLAGS="$(XCFLAGS)" DDDEBUG="$(DDDEBUG)" MTRDEBUG="$(MTRDEBUG)" LDFLAGS="$(LDFLAGS)" EXE="$(EXE)" )\
done
optimize_dec:
sh ./setup.sh
@for dir in $(DIRS); do \
(cd $$dir; \
echo Making $$dir ...; \
make CC=$(CC) RANLIB=$(RANLIB) XCFLAGS="$(XCFLAGS)" LDFLAGS="$(LDFLAGS)" optimize_dec )\
done
lint:
sh ./setup.sh
@for dir in $(DIRS) obj; do \
(cd $$dir; \
echo Making lint in $$dir ...; \
make CC=$(CC) lint )\
done
tags:
sh ./setup.sh
@for dir in $(DIRS) obj; do \
(cd $$dir; \
echo Making tags in $$dir ...; \
make CC=$(CC) tags )\
done
all:
sh ./setup.sh
@for dir in $(DIRS); do \
(cd $$dir; \
echo Making all in $$dir ...; \
make CC=$(CC) RANLIB=$(RANLIB) MFLAG= MNEMLIB= ICFLAGS="$(ICFLAGS)" XCFLAGS="$(XCFLAGS)" DDDEBUG="$(DDDEBUG)" MTRDEBUG="$(MTRDEBUG)" LDFLAGS="$(LDFLAGS)" PURE="$(PURE)" EXE="$(EXE)" all )\
done
testcudd:
sh ./setup.sh
@for dir in util st mtr epd; do \
(cd $$dir; \
echo Making $$dir ...; \
make CC=$(CC) RANLIB=$(RANLIB) MFLAG= MNEMLIB= ICFLAGS="$(ICFLAGS)" XCFLAGS="$(XCFLAGS)" DDDEBUG="$(DDDEBUG)" MTRDEBUG="$(MTRDEBUG)" LDFLAGS="$(LDFLAGS)" PURE="$(PURE)" EXE="$(EXE)" )\
done
@(cd cudd; \
echo Making testcudd ...; \
make CC=$(CC) RANLIB=$(RANLIB) MFLAG= MNEMLIB= ICFLAGS="$(ICFLAGS)" XCFLAGS="$(XCFLAGS)" DDDEBUG="$(DDDEBUG)" MTRDEBUG="$(MTRDEBUG)" LDFLAGS="$(LDFLAGS)" PURE="$(PURE)" EXE="$(EXE)" testcudd$(EXE) )
objlib:
sh ./setup.sh
@for dir in $(BDIRS); do \
(cd $$dir; \
echo Making $$dir ...; \
make CC=$(CC) RANLIB=$(RANLIB) MFLAG= MNEMLIB= ICFLAGS="$(ICFLAGS)" XCFLAGS="$(XCFLAGS)" DDDEBUG="$(DDDEBUG)" MTRDEBUG="$(MTRDEBUG)" LDFLAGS="$(LDFLAGS)" PURE="$(PURE)" EXE="$(EXE)" )\
done
@(cd obj; \
echo Making obj ...; \
make CXX=$(CXX) CXXFLAGS=$(CXXFLAGS) RANLIB=$(RANLIB) MFLAG= MNEMLIB= ICFLAGS="$(ICFLAGS)" XCFLAGS="$(XCFLAGS)" DDDEBUG="$(DDDEBUG)" MTRDEBUG="$(MTRDEBUG)" LDFLAGS="$(LDFLAGS)" PURE="$(PURE)" EXE="$(EXE)" )
testobj: objlib
@(cd obj; \
echo Making testobj ...; \
make CXX=$(CXX) CXXFLAGS=$(CXXFLAGS) RANLIB=$(RANLIB) MFLAG= MNEMLIB= ICFLAGS="$(ICFLAGS)" XCFLAGS="$(XCFLAGS)" DDDEBUG="$(DDDEBUG)" MTRDEBUG="$(MTRDEBUG)" LDFLAGS="$(LDFLAGS)" PURE="$(PURE)" EXE="$(EXE)" testobj$(EXE) )
testdddmp: build
@(cd dddmp; \
echo Making testdddmp ...; \
make CC=$(CC) RANLIB=$(RANLIB) MFLAG= MNEMLIB= ICFLAGS="$(ICFLAGS)" XCFLAGS="$(XCFLAGS)" DDDEBUG="$(DDDEBUG)" MTRDEBUG="$(MTRDEBUG)" LDFLAGS="$(LDFLAGS)" PURE="$(PURE)" EXE="$(EXE)" testdddmp$(EXE) )
testmtr: build
@(cd mtr; \
echo Making testmtr ...; \
make CC=$(CC) RANLIB=$(RANLIB) MFLAG= MNEMLIB= ICFLAGS="$(ICFLAGS)" XCFLAGS="$(XCFLAGS)" DDDEBUG="$(DDDEBUG)" MTRDEBUG="$(MTRDEBUG)" LDFLAGS="$(LDFLAGS)" PURE="$(PURE)" EXE="$(EXE)" testmtr$(EXE) )
clean:
@for dir in mnemosyne $(DIRS) obj; do \
(cd $$dir; \
echo Cleaning $$dir ...; \
make -s clean ) \
done
distclean:
@for dir in mnemosyne $(DIRS) obj; do \
(cd $$dir; \
echo Cleaning $$dir ...; \
make -s EXE="$(EXE)" distclean ) \
done
sh ./shutdown.sh

177
resources/3rdparty/cudd-2.5.0/README

@ -1,177 +0,0 @@
$Id$
This directory contains a set of packages that allow you to build a toy
application based on the CUDD package.
The CUDD package is a package written in C for the manipulation of
decision diagrams. It supports binary decision diagrams (BDDs),
algebraic decision diagrams (ADDs), and Zero-Suppressed BDDs (ZDDs).
The toy application provided in this kit is called nanotrav and is a
simple-minded FSM traversal program. (See the README file and the man
page nanotrav.1 in the nanotrav directory for the details.) It is
included so that you can run a sanity check on your installation.
INSTALLATION
Before you build the libraries and programs, you need to check the
Makefile in the top directory. Go through the definitions contained in the
configuration section, and select the desired compiler and compilation
flags. Instructions are provided in the comments of the Makefile.
You can always specify the options on the command line. For instance,
on some machines you can build a "fast" version of the program by typing:
make DDDEBUG= MTRDEBUG= ICFLAGS=-O2
The Makefile supports several targets:
make:
Creates a "plain" version of the program.
make testdddmp:
Builds a test program (testdddmp) for BDD loading from and
storing to disk. See file README.test in the dddmp directory for
how to run the program.
make testobj:
Builds a test program for the C++ interface. Requires a C++
compiler. To run the program, run obj/testobj.
make testcudd:
Builds a test program for CUDD. To run the program, go to the
cudd directory and type "./testcudd -p 2 r7x8.1.mat". The result
can be compared to r7x7.1.out.
make testmtr:
Builds a test program for the mtr package. To run the program,
go to the mtr directory and type "./testmtr -p 1 test.groups".
make clean:
Cleans directories, but leaves libraries and programs.
make distclean:
Cleans thoroughly, returning the directories to their pristine
state.
The following targets are more or less obsolete and may disappear or
change in the future.
make check_leaks:
Creates a version of the program with the mnemosyne library
linked to it. It also builds the mnemalyse program, which
helps in finding memory leaks. This target does not work on the
IBM RS6000. The makefile also supports purify. To use purify,
set the PURE variable in the Makefile, and use the standard
target.
make optimize_dec:
Builds a version of the program using the u-code compiler
available on DEC machines (DECstations and Alphas). The newer
native compiler on the Alphas does not use u-code, though.
Therefore the standard target should be used with it.
make lint:
Runs lint on all subdirectories except mnemosyne. Creates lint
libraries for all object libraries.
make tags:
Builds ctags-style tag files for all subdirectories except
mnemosyne.
make all:
Makes all of the above, except check_leaks, which is
incompatible with a plain "make."
All targets, except clean and distclean, will create the include
directory if it does not already exist.
The Makefile does not compile the SIS interface (cuddBddPort.c and
cuddPwPt.c found in subdirectory sis). To compile the interface, you
also need array.h and var_set.h, which are not part of this
distribution, but come with SIS. Detailed instructions on how to
integrate the CUDD package in SIS can be found in the documentation
(cudd/doc).
PLATFORMS
This kit has been successfully built on the following configurations:
PC (ia32 and ia64) running Ubuntu with gcc
PC (ia32 and ia64) running Ubuntu with g++
PC (ia32 and ia64) running Linux RedHat with gcc
PC (ia32 and ia64) running Linux RedHat with g++
PC (ia64) running Cygwin on Windows 7 and Vista with gcc
PC (ia64) running Cygwin on Windows 7 and Vista with g++
Platforms to which I have no longer access and therefore are no longer
supported.
PC (ia32) running Linux RedHat with icc
PC (ia32) running Linux RedHat with icpc
PC (ia64) running Linux RedHat with ecc
PC (ia64) running Linux RedHat with ecpc
SUN running Solaris 2.8 with cc
SUN running Solaris 2.8 with CC
SUN running Solaris 2.8 with gcc
SUN running Solaris 2.8 with g++
DECstation running Ultrix with cc
DECstation running Ultrix with gcc
IBM RS6000 running AIX 3.2.4 with cc (**)
IBM RS6000 running AIX 3.2.4 with gcc
IBM RS6000 running AIX 3.2.4 with g++
SUN running SunOS with gcc
DEC Alpha running Digital Unix with cc
DEC Alpha running Digital Unix with cxx
DEC Alpha running Digital Unix with gcc
HP 9000/770 running HP-UX with c89
HP 9000/770 running HP-UX with CC
HP 9000/770 running HP-UX with gcc
HP 9000/770 running HP-UX with g++ (*)
SUN running Solaris 2.8 with /usr/ucb/cc
PC running Solaris 2.8 with /usr/bin/cc
PC running Solaris 2.8 with /usr/ucb/cc
PC running Solaris 2.8 with CC
PC running Solaris 2.8 with gcc
PC running Solaris 2.8 with g++
NOTES
(*) C programs were compiled with g++, but linked with gcc.
(**) Some old versions of the AIX cc compiler have buggy optimizers:
Try compiling with -O2 instead of -O3 if the program crashes.
Running lint and compiling with gcc -Wall still produces warnings.
Running `purify' under Solaris 2.8 generates no messages.
SANITY CHECK
The directory `nanotrav' contains a very simple application based on the
CUDD package. The `nanotrav' directory contains a man page that
describes the options nanotrav supports. The files *.blif are sample
input files for nanotrav.
If you have built the mnemosyne library (make check_leaks), you can do
cd mnemosyne
make runmtest
This does not work on machines running SunOS, but the version of
nanotrav that uses mnemosyne may work.
DOCUMENTATION
Directory cudd-2.5.0/cudd/doc contains HTML documentation for the CUDD
package. The recommended starting point is cuddIntro.html. Documentation
in both postscript(tm) format and plain text format is also provided.
Documentation for the auxiliary libraries (except for the util library)
is in the doc subdirectories.
FEEDBACK:
Send feedback to:
Fabio Somenzi
University of Colorado at Boulder
ECE Dept.
Boulder, CO 80309-0425
Fabio@Colorado.EDU
http://vlsi.colorado.edu/~fabio

131
resources/3rdparty/cudd-2.5.0/RELEASE.NOTES

@ -1,131 +0,0 @@
Release 2.5.0 of Cudd introduces the ability to set timeouts. The
function that is interrupted returns NULL (which the application must
be prepared to handle,) but the BDDs are uncorrupted and the invoking
program can continue to use the manager.
In addition, reordering is now aware of timeouts, so that it gives up
when a timeout is approaching to give the invoking program a chance to
obtain some results.
The response time to the timeout is not immediate, though most of the time
it is well below one second. Checking for timeouts has a small overhead.
In experiments, less than 1% has been observed on average.
Creation of BDD managers with many variables (e.g., tens or hundreds
of thousands) is now much more efficient. Computing small supports of
BDDs when there are many variables is also much more efficient, but
this has been at the cost of separating the function for BDDs and ADDs
(Cudd_Support) from that for ZDDs (Cudd_zddSupport).
The C++ interface has undergone a major upgrade.
The handling of variable gruops in reordering has been much improved.
(Thanks to Arie Gurfinkel for a very detailed bug report!) A handful
of other bugs have been fixed as well.
New Functions:
unsigned long Cudd_ReadStartTime(DdManager *unique);
unsigned long Cudd_ReadElapsedTime(DdManager *unique);
void Cudd_SetStartTime(DdManager *unique, unsigned long st);
void Cudd_ResetStartTime(DdManager *unique);
unsigned long Cudd_ReadTimeLimit(DdManager *unique);
void Cudd_SetTimeLimit(DdManager *unique, unsigned long tl);
void Cudd_UpdateTimeLimit(DdManager * unique);
void Cudd_IncreaseTimeLimit(DdManager * unique, unsigned long increase);
void Cudd_UnsetTimeLimit(DdManager *unique);
int Cudd_TimeLimited(DdManager *unique);
unsigned int Cudd_ReadMaxReorderings (DdManager *dd);
void Cudd_SetMaxReorderings (DdManager *dd, unsigned int mr);
unsigned int Cudd_ReadOrderRandomization(DdManager * dd);
void Cudd_SetOrderRandomization(DdManager * dd, unsigned int factor);
int Cudd_PrintGroupedOrder(DdManager * dd, const char *str, void *data);
int Cudd_EnableOrderingMonitoring(DdManager *dd);
int Cudd_DisableOrderingMonitoring(DdManager *dd);
int Cudd_OrderingMonitoring(DdManager *dd);
DdNode * Cudd_bddExistAbstractLimit(DdManager * manager, DdNode * f, DdNode * cube, unsigned int limit);
DdNode * Cudd_bddIteLimit (DdManager *dd, DdNode *f, DdNode *g, DdNode *h, unsigned int limit);
DdNode * Cudd_bddOrLimit (DdManager *dd, DdNode *f, DdNode *g, unsigned int limit);
DdNode * Cudd_bddXnorLimit (DdManager *dd, DdNode *f, DdNode *g, unsigned int limit);
int Cudd_CheckCube (DdManager *dd, DdNode *g);
DdNode * Cudd_bddMaximallyExpand(DdManager *dd, DdNode *lb, DdNode *ub, DdNode *f);
DdNode * Cudd_bddLargestPrimeUnate(DdManager *dd , DdNode *f, DdNode *phaseBdd);
int Cudd_Reserve(DdManager *manager, int amount);
int Cudd_SupportIndices(DdManager * dd, DdNode * f, int **indices);
int Cudd_VectorSupportIndices(DdManager * dd, DdNode ** F, int n, int **indices);
DdNode * Cudd_zddSupport(DdManager * dd, DdNode * f);
Changed prototypes:
unsigned int Cudd_ReadReorderings (DdManager *dd);
----------------------------------------------------------------------
Release 2.4.2 of Cudd features several bug fixes. The most important
are those that prevented Cudd from making full use of up to 4 GB of
memory when using 32-bit pointers. A handful of bugs were discovered by
Coverity. (Thanks to Christian Stangier!)
This release can be compiled with either 64-bit pointers or 32-bit
pointers on x86_64 platforms if sizeof(long) = sizeof(void *) = 8 and
sizeof(int) = 4. This is known as the LP64 model. For 32-bit pointers,
one usually needs supplementary libraries. On Ubuntu and Debian Linux,
one needs g++-multilib, which can be installed with
"apt-get install g++-multilib."
Added functions
DdNode *Cudd_Inequality (DdManager * dd, int N, int c, DdNode ** x,
DdNode ** y);
DdNode * Cudd_Disequality (DdManager * dd, int N, int c, DdNode ** x,
DdNode ** y);
DdNode * Cudd_bddInterval (DdManager * dd, int N, DdNode ** x,
unsigned int lowerB, unsigned int upperB);
Changed prototypes:
int Cudd_DumpBlif (DdManager *dd, int n, DdNode **f, char
**inames, char **onames, char *mname, FILE *fp, int mv);
int Cudd_DumpBlifBody (DdManager *dd, int n, DdNode **f, char
**inames, char **onames, FILE *fp, int mv);
The additional parameter allows the caller to choose between plain blif
and blif-MV.
----------------------------------------------------------------------
Release 2.4.1 of Cudd features one major change with respect to previous
releases. The licensing terms are now explicitly stated.

18
resources/3rdparty/cudd-2.5.0/setup.sh

@ -1,18 +0,0 @@
#! /bin/sh
CREATE="ln -s"
if test -d include
then
:
else
mkdir include
cd include
$CREATE ../cudd/cudd.h .
$CREATE ../cudd/cuddInt.h .
$CREATE ../epd/epd.h .
$CREATE ../dddmp/dddmp.h .
$CREATE ../mtr/mtr.h .
$CREATE ../obj/cuddObj.hh .
$CREATE ../st/st.h .
$CREATE ../util/util.h .
$CREATE ../mnemosyne/mnemosyne.h .
fi

2
resources/3rdparty/cudd-2.5.0/shutdown.sh

@ -1,2 +0,0 @@
#! /bin/sh
rm -rf include *.bak *~

124
resources/3rdparty/cudd-2.5.0/src/cudd/Makefile

@ -1,124 +0,0 @@
# $Id$
#
# Cudd - DD package
#---------------------------
.SUFFIXES: .o .c .u
CC = gcc
RANLIB = ranlib
PURE =
# Define EXE as .exe for MS-DOS and derivatives.
EXE =
#EXE = .exe
MFLAG =
ICFLAGS = -g
XCFLAGS = -DDD_STATS
CFLAGS = $(ICFLAGS) $(MFLAG) $(XCFLAGS)
#DDDEBUG = -DDD_DEBUG -DDD_CACHE_PROFILE -DDD_VERBOSE -DDD_UNIQUE_PROFILE
DDDEBUG =
LINTFLAGS = -u -n -DDD_STATS -DDD_CACHE_PROFILE -DDD_VERBOSE -DDD_DEBUG -DDD_UNIQUE_PROFILE
# this is to create the lint library
LINTSWITCH = -o
WHERE = ..
INCLUDE = $(WHERE)/include
LIBS = ./libcudd.a $(WHERE)/mtr/libmtr.a \
$(WHERE)/st/libst.a $(WHERE)/util/libutil.a $(WHERE)/epd/libepd.a
MNEMLIB =
BLIBS = -kL. -klcudd -kL$(WHERE)/mtr -klmtr \
-kL$(WHERE)/st -klst -kL$(WHERE)/util -klutil -kL$(WHERE)/epd -klepd
LINTLIBS = ./llib-lcudd.ln $(WHERE)/mtr/llib-lmtr.ln \
$(WHERE)/st/llib-lst.ln $(WHERE)/util/llib-lutil.ln \
$(WHERE)/epd/llib-lepd.ln
LDFLAGS =
# files for the package
P = cudd
PSRC = cuddAPI.c cuddAddAbs.c cuddAddApply.c cuddAddFind.c cuddAddIte.c \
cuddAddInv.c cuddAddNeg.c cuddAddWalsh.c cuddAndAbs.c \
cuddAnneal.c cuddApa.c cuddApprox.c cuddBddAbs.c cuddBddCorr.c \
cuddBddIte.c cuddBridge.c cuddCache.c cuddCheck.c cuddClip.c \
cuddCof.c cuddCompose.c cuddDecomp.c cuddEssent.c \
cuddExact.c cuddExport.c cuddGenCof.c cuddGenetic.c \
cuddGroup.c cuddHarwell.c cuddInit.c cuddInteract.c \
cuddLCache.c cuddLevelQ.c \
cuddLinear.c cuddLiteral.c cuddMatMult.c cuddPriority.c \
cuddRead.c cuddRef.c cuddReorder.c cuddSat.c cuddSign.c \
cuddSolve.c cuddSplit.c cuddSubsetHB.c cuddSubsetSP.c cuddSymmetry.c \
cuddTable.c cuddUtil.c cuddWindow.c cuddZddCount.c cuddZddFuncs.c \
cuddZddGroup.c cuddZddIsop.c cuddZddLin.c cuddZddMisc.c \
cuddZddPort.c cuddZddReord.c cuddZddSetop.c cuddZddSymm.c \
cuddZddUtil.c
PHDR = cudd.h cuddInt.h
POBJ = $(PSRC:.c=.o)
PUBJ = $(PSRC:.c=.u)
TARGET = test$(P)$(EXE)
TARGETu = test$(P)-u
# files for the test program
SRC = test$(P).c
OBJ = $(SRC:.c=.o)
UBJ = $(SRC:.c=.u)
#------------------------------------------------------
lib$(P).a: $(POBJ)
ar rv $@ $?
$(RANLIB) $@
.c.o: $(PSRC) $(PHDR)
$(CC) -c $< -I$(INCLUDE) $(CFLAGS) $(DDDEBUG)
optimize_dec: lib$(P).b
lib$(P).b: $(PUBJ)
ar rv $@ $?
$(RANLIB) $@
.c.u: $(PSRC) $(PHDR)
cc -j $< -I$(INCLUDE) $(XCFLAGS)
# if the header files change, recompile
$(POBJ): $(PHDR)
$(PUBJ): $(PHDR)
$(OBJ): $(PHDR)
$(UBJ): $(PHDR)
$(TARGET): $(SRC) $(OBJ) $(HDR) $(LIBS) $(MNEMLIB)
$(PURE) $(CC) $(CFLAGS) $(LDFLAGS) -o $@ $(OBJ) $(LIBS) $(MNEMLIB) -lm
# optimize (DECstations and Alphas only: uses u-code)
$(TARGETu): $(SRC) $(UBJ) $(HDR) $(LIBS:.a=.b)
$(CC) -O3 -Olimit 1000 $(XCFLAGS) $(LDFLAGS) -o $@ $(UBJ) $(BLIBS) -lm
lint: llib-l$(P).ln
llib-l$(P).ln: $(PSRC) $(PHDR)
lint $(LINTFLAGS) $(LINTSWITCH)$(P) -I$(INCLUDE) $(PSRC)
lintpgm: lint
lint $(LINTFLAGS) -I$(INCLUDE) $(SRC) $(LINTLIBS)
tags: $(PSRC) $(PHDR)
ctags $(PSRC) $(PHDR)
all: lib$(P).a lib$(P).b llib-l$(P).ln tags
programs: $(TARGET) $(TARGETu) lintpgm
clean:
rm -f *.o *.u mon.out gmon.out *.pixie *.Addrs *.Counts mnem.* \
.pure core *.warnings
distclean: clean
rm -f $(TARGET) $(TARGETu) lib*.a lib$(P).b llib-l$(P).ln \
*.bak *~ tags .gdb_history *.qv *.qx

1090
resources/3rdparty/cudd-2.5.0/src/cudd/cudd.h
File diff suppressed because it is too large
View File

4893
resources/3rdparty/cudd-2.5.0/src/cudd/cuddAPI.c
File diff suppressed because it is too large
View File

960
resources/3rdparty/cudd-2.5.0/src/cudd/cuddGenetic.c

@ -1,960 +0,0 @@
/**CFile***********************************************************************
FileName [cuddGenetic.c]
PackageName [cudd]
Synopsis [Genetic algorithm for variable reordering.]
Description [Internal procedures included in this file:
<ul>
<li> cuddGa()
</ul>
Static procedures included in this module:
<ul>
<li> make_random()
<li> sift_up()
<li> build_dd()
<li> largest()
<li> rand_int()
<li> array_hash()
<li> array_compare()
<li> find_best()
<li> find_average_fitness()
<li> PMX()
<li> roulette()
</ul>
The genetic algorithm implemented here is as follows. We start with
the current DD order. We sift this order and use this as the
reference DD. We only keep 1 DD around for the entire process and
simply rearrange the order of this DD, storing the various orders
and their corresponding DD sizes. We generate more random orders to
build an initial population. This initial population is 3 times the
number of variables, with a maximum of 120. Each random order is
built (from the reference DD) and its size stored. Each random
order is also sifted to keep the DD sizes fairly small. Then a
crossover is performed between two orders (picked randomly) and the
two resulting DDs are built and sifted. For each new order, if its
size is smaller than any DD in the population, it is inserted into
the population and the DD with the largest number of nodes is thrown
out. The crossover process happens up to 50 times, and at this point
the DD in the population with the smallest size is chosen as the
result. This DD must then be built from the reference DD.]
SeeAlso []
Author [Curt Musfeldt, Alan Shuler, Fabio Somenzi]
Copyright [Copyright (c) 1995-2012, 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.]
******************************************************************************/
#include "util.h"
#include "cuddInt.h"
/*---------------------------------------------------------------------------*/
/* Constant declarations */
/*---------------------------------------------------------------------------*/
/*---------------------------------------------------------------------------*/
/* Stucture declarations */
/*---------------------------------------------------------------------------*/
/*---------------------------------------------------------------------------*/
/* Type declarations */
/*---------------------------------------------------------------------------*/
/*---------------------------------------------------------------------------*/
/* Variable declarations */
/*---------------------------------------------------------------------------*/
#ifndef lint
static char rcsid[] DD_UNUSED = "$Id: cuddGenetic.c,v 1.30 2012/02/05 01:07:18 fabio Exp $";
#endif
static int popsize; /* the size of the population */
static int numvars; /* the number of input variables in the ckt. */
/* storedd stores the population orders and sizes. This table has two
** extra rows and one extras column. The two extra rows are used for the
** offspring produced by a crossover. Each row stores one order and its
** size. The order is stored by storing the indices of variables in the
** order in which they appear in the order. The table is in reality a
** one-dimensional array which is accessed via a macro to give the illusion
** it is a two-dimensional structure.
*/
static int *storedd;
static st_table *computed; /* hash table to identify existing orders */
static int *repeat; /* how many times an order is present */
static int large; /* stores the index of the population with
** the largest number of nodes in the DD */
static int result;
static int cross; /* the number of crossovers to perform */
/*---------------------------------------------------------------------------*/
/* Macro declarations */
/*---------------------------------------------------------------------------*/
/* macro used to access the population table as if it were a
** two-dimensional structure.
*/
#define STOREDD(i,j) storedd[(i)*(numvars+1)+(j)]
#ifdef __cplusplus
extern "C" {
#endif
/**AutomaticStart*************************************************************/
/*---------------------------------------------------------------------------*/
/* Static function prototypes */
/*---------------------------------------------------------------------------*/
static int make_random (DdManager *table, int lower);
static int sift_up (DdManager *table, int x, int x_low);
static int build_dd (DdManager *table, int num, int lower, int upper);
static int largest (void);
static int rand_int (int a);
static int array_hash (char *array, int modulus);
static int array_compare (const char *array1, const char *array2);
static int find_best (void);
#ifdef DD_STATS
static double find_average_fitness (void);
#endif
static int PMX (int maxvar);
static int roulette (int *p1, int *p2);
/**AutomaticEnd***************************************************************/
#ifdef __cplusplus
}
#endif
/*---------------------------------------------------------------------------*/
/* Definition of exported functions */
/*---------------------------------------------------------------------------*/
/*---------------------------------------------------------------------------*/
/* Definition of internal functions */
/*---------------------------------------------------------------------------*/
/**Function********************************************************************
Synopsis [Genetic algorithm for DD reordering.]
Description [Genetic algorithm for DD reordering.
The two children of a crossover will be stored in
storedd[popsize] and storedd[popsize+1] --- the last two slots in the
storedd array. (This will make comparisons and replacement easy.)
Returns 1 in case of success; 0 otherwise.]
SideEffects [None]
SeeAlso []
******************************************************************************/
int
cuddGa(
DdManager * table /* manager */,
int lower /* lowest level to be reordered */,
int upper /* highest level to be reorderded */)
{
int i,n,m; /* dummy/loop vars */
int index;
#ifdef DD_STATS
double average_fitness;
#endif
int small; /* index of smallest DD in population */
/* Do an initial sifting to produce at least one reasonable individual. */
if (!cuddSifting(table,lower,upper)) return(0);
/* Get the initial values. */
numvars = upper - lower + 1; /* number of variables to be reordered */
if (table->populationSize == 0) {
popsize = 3 * numvars; /* population size is 3 times # of vars */
if (popsize > 120) {
popsize = 120; /* Maximum population size is 120 */
}
} else {
popsize = table->populationSize; /* user specified value */
}
if (popsize < 4) popsize = 4; /* enforce minimum population size */
/* Allocate population table. */
storedd = ALLOC(int,(popsize+2)*(numvars+1));
if (storedd == NULL) {
table->errorCode = CUDD_MEMORY_OUT;
return(0);
}
/* Initialize the computed table. This table is made up of two data
** structures: A hash table with the key given by the order, which says
** if a given order is present in the population; and the repeat
** vector, which says how many copies of a given order are stored in
** the population table. If there are multiple copies of an order, only
** one has a repeat count greater than 1. This copy is the one pointed
** by the computed table.
*/
repeat = ALLOC(int,popsize);
if (repeat == NULL) {
table->errorCode = CUDD_MEMORY_OUT;
FREE(storedd);
return(0);
}
for (i = 0; i < popsize; i++) {
repeat[i] = 0;
}
computed = st_init_table(array_compare,array_hash);
if (computed == NULL) {
table->errorCode = CUDD_MEMORY_OUT;
FREE(storedd);
FREE(repeat);
return(0);
}
/* Copy the current DD and its size to the population table. */
for (i = 0; i < numvars; i++) {
STOREDD(0,i) = table->invperm[i+lower]; /* order of initial DD */
}
STOREDD(0,numvars) = table->keys - table->isolated; /* size of initial DD */
/* Store the initial order in the computed table. */
if (st_insert(computed,(char *)storedd,(char *) 0) == ST_OUT_OF_MEM) {
FREE(storedd);
FREE(repeat);
st_free_table(computed);
return(0);
}
repeat[0]++;
/* Insert the reverse order as second element of the population. */
for (i = 0; i < numvars; i++) {
STOREDD(1,numvars-1-i) = table->invperm[i+lower]; /* reverse order */
}
/* Now create the random orders. make_random fills the population
** table with random permutations. The successive loop builds and sifts
** the DDs for the reverse order and each random permutation, and stores
** the results in the computed table.
*/
if (!make_random(table,lower)) {
table->errorCode = CUDD_MEMORY_OUT;
FREE(storedd);
FREE(repeat);
st_free_table(computed);
return(0);
}
for (i = 1; i < popsize; i++) {
result = build_dd(table,i,lower,upper); /* build and sift order */
if (!result) {
FREE(storedd);
FREE(repeat);
st_free_table(computed);
return(0);
}
if (st_lookup_int(computed,(char *)&STOREDD(i,0),&index)) {
repeat[index]++;
} else {
if (st_insert(computed,(char *)&STOREDD(i,0),(char *)(long)i) ==
ST_OUT_OF_MEM) {
FREE(storedd);
FREE(repeat);
st_free_table(computed);
return(0);
}
repeat[i]++;
}
}
#if 0
#ifdef DD_STATS
/* Print the initial population. */
(void) fprintf(table->out,"Initial population after sifting\n");
for (m = 0; m < popsize; m++) {
for (i = 0; i < numvars; i++) {
(void) fprintf(table->out," %2d",STOREDD(m,i));
}
(void) fprintf(table->out," : %3d (%d)\n",
STOREDD(m,numvars),repeat[m]);
}
#endif
#endif
small = find_best();
#ifdef DD_STATS
average_fitness = find_average_fitness();
(void) fprintf(table->out,"\nInitial population: best fitness = %d, average fitness %8.3f",STOREDD(small,numvars),average_fitness);
#endif
/* Decide how many crossovers should be tried. */
if (table->numberXovers == 0) {
cross = 3*numvars;
if (cross > 60) { /* do a maximum of 50 crossovers */
cross = 60;
}
} else {
cross = table->numberXovers; /* use user specified value */
}
if (cross >= popsize) {
cross = popsize;
}
/* Perform the crossovers to get the best order. */
for (m = 0; m < cross; m++) {
if (!PMX(table->size)) { /* perform one crossover */
table->errorCode = CUDD_MEMORY_OUT;
FREE(storedd);
FREE(repeat);
st_free_table(computed);
return(0);
}
/* The offsprings are left in the last two entries of the
** population table. These are now considered in turn.
*/
for (i = popsize; i <= popsize+1; i++) {
result = build_dd(table,i,lower,upper); /* build and sift child */
if (!result) {
FREE(storedd);
FREE(repeat);
st_free_table(computed);
return(0);
}
large = largest(); /* find the largest DD in population */
/* If the new child is smaller than the largest DD in the current
** population, enter it into the population in place of the
** largest DD.
*/
if (STOREDD(i,numvars) < STOREDD(large,numvars)) {
/* Look up the largest DD in the computed table.
** Decrease its repetition count. If the repetition count
** goes to 0, remove the largest DD from the computed table.
*/
result = st_lookup_int(computed,(char *)&STOREDD(large,0),
&index);
if (!result) {
FREE(storedd);
FREE(repeat);
st_free_table(computed);
return(0);
}
repeat[index]--;
if (repeat[index] == 0) {
int *pointer = &STOREDD(index,0);
result = st_delete(computed, &pointer, NULL);
if (!result) {
FREE(storedd);
FREE(repeat);
st_free_table(computed);
return(0);
}
}
/* Copy the new individual to the entry of the
** population table just made available and update the
** computed table.
*/
for (n = 0; n <= numvars; n++) {
STOREDD(large,n) = STOREDD(i,n);
}
if (st_lookup_int(computed,(char *)&STOREDD(large,0),
&index)) {
repeat[index]++;
} else {
if (st_insert(computed,(char *)&STOREDD(large,0),
(char *)(long)large) == ST_OUT_OF_MEM) {
FREE(storedd);
FREE(repeat);
st_free_table(computed);
return(0);
}
repeat[large]++;
}
}
}
}
/* Find the smallest DD in the population and build it;
** that will be the result.
*/
small = find_best();
/* Print stats on the final population. */
#ifdef DD_STATS
average_fitness = find_average_fitness();
(void) fprintf(table->out,"\nFinal population: best fitness = %d, average fitness %8.3f",STOREDD(small,numvars),average_fitness);
#endif
/* Clean up, build the result DD, and return. */
st_free_table(computed);
computed = NULL;
result = build_dd(table,small,lower,upper);
FREE(storedd);
FREE(repeat);
return(result);
} /* end of cuddGa */
/*---------------------------------------------------------------------------*/
/* Definition of static functions */
/*---------------------------------------------------------------------------*/
/**Function********************************************************************
Synopsis [Generates the random sequences for the initial population.]
Description [Generates the random sequences for the initial population.
The sequences are permutations of the indices between lower and
upper in the current order.]
SideEffects [None]
SeeAlso []
******************************************************************************/
static int
make_random(
DdManager * table,
int lower)
{
int i,j; /* loop variables */
int *used; /* is a number already in a permutation */
int next; /* next random number without repetitions */
used = ALLOC(int,numvars);
if (used == NULL) {
table->errorCode = CUDD_MEMORY_OUT;
return(0);
}
#if 0
#ifdef DD_STATS
(void) fprintf(table->out,"Initial population before sifting\n");
for (i = 0; i < 2; i++) {
for (j = 0; j < numvars; j++) {
(void) fprintf(table->out," %2d",STOREDD(i,j));
}
(void) fprintf(table->out,"\n");
}
#endif
#endif
for (i = 2; i < popsize; i++) {
for (j = 0; j < numvars; j++) {
used[j] = 0;
}
/* Generate a permutation of {0...numvars-1} and use it to
** permute the variables in the layesr from lower to upper.
*/
for (j = 0; j < numvars; j++) {
do {
next = rand_int(numvars-1);
} while (used[next] != 0);
used[next] = 1;
STOREDD(i,j) = table->invperm[next+lower];
}
#if 0
#ifdef DD_STATS
/* Print the order just generated. */
for (j = 0; j < numvars; j++) {
(void) fprintf(table->out," %2d",STOREDD(i,j));
}
(void) fprintf(table->out,"\n");
#endif
#endif
}
FREE(used);
return(1);
} /* end of make_random */
/**Function********************************************************************
Synopsis [Moves one variable up.]
Description [Takes a variable from position x and sifts it up to
position x_low; x_low should be less than x. Returns 1 if successful;
0 otherwise]
SideEffects [None]
SeeAlso []
******************************************************************************/
static int
sift_up(
DdManager * table,
int x,
int x_low)
{
int y;
int size;
y = cuddNextLow(table,x);
while (y >= x_low) {
size = cuddSwapInPlace(table,y,x);
if (size == 0) {
return(0);
}
x = y;
y = cuddNextLow(table,x);
}
return(1);
} /* end of sift_up */
/**Function********************************************************************
Synopsis [Builds a DD from a given order.]
Description [Builds a DD from a given order. This procedure also
sifts the final order and inserts into the array the size in nodes
of the result. Returns 1 if successful; 0 otherwise.]
SideEffects [None]
SeeAlso []
******************************************************************************/
static int
build_dd(
DdManager * table,
int num /* the index of the individual to be built */,
int lower,
int upper)
{
int i,j; /* loop vars */
int position;
int index;
int limit; /* how large the DD for this order can grow */
int size;
/* Check the computed table. If the order already exists, it
** suffices to copy the size from the existing entry.
*/
if (computed && st_lookup_int(computed,(char *)&STOREDD(num,0),&index)) {
STOREDD(num,numvars) = STOREDD(index,numvars);
#ifdef DD_STATS
(void) fprintf(table->out,"\nCache hit for index %d", index);
#endif
return(1);
}
/* Stop if the DD grows 20 times larges than the reference size. */
limit = 20 * STOREDD(0,numvars);
/* Sift up the variables so as to build the desired permutation.
** First the variable that has to be on top is sifted to the top.
** Then the variable that has to occupy the secon position is sifted
** up to the second position, and so on.
*/
for (j = 0; j < numvars; j++) {
i = STOREDD(num,j);
position = table->perm[i];
result = sift_up(table,position,j+lower);
if (!result) return(0);
size = table->keys - table->isolated;
if (size > limit) break;
}
/* Sift the DD just built. */
#ifdef DD_STATS
(void) fprintf(table->out,"\n");
#endif
result = cuddSifting(table,lower,upper);
if (!result) return(0);
/* Copy order and size to table. */
for (j = 0; j < numvars; j++) {
STOREDD(num,j) = table->invperm[lower+j];
}
STOREDD(num,numvars) = table->keys - table->isolated; /* size of new DD */
return(1);
} /* end of build_dd */
/**Function********************************************************************
Synopsis [Finds the largest DD in the population.]
Description [Finds the largest DD in the population. If an order is
repeated, it avoids choosing the copy that is in the computed table
(it has repeat[i] > 1).]
SideEffects [None]
SeeAlso []
******************************************************************************/
static int
largest(void)
{
int i; /* loop var */
int big; /* temporary holder to return result */
big = 0;
while (repeat[big] > 1) big++;
for (i = big + 1; i < popsize; i++) {
if (STOREDD(i,numvars) >= STOREDD(big,numvars) && repeat[i] <= 1) {
big = i;
}
}
return(big);
} /* end of largest */
/**Function********************************************************************
Synopsis [Generates a random number between 0 and the integer a.]
Description []
SideEffects [None]
SeeAlso []
******************************************************************************/
static int
rand_int(
int a)
{
return(Cudd_Random() % (a+1));
} /* end of rand_int */
/**Function********************************************************************
Synopsis [Hash function for the computed table.]
Description [Hash function for the computed table. Returns the bucket
number.]
SideEffects [None]
SeeAlso []
******************************************************************************/
static int
array_hash(
char * array,
int modulus)
{
int val = 0;
int i;
int *intarray;
intarray = (int *) array;
for (i = 0; i < numvars; i++) {
val = val * 997 + intarray[i];
}
return ((val < 0) ? -val : val) % modulus;
} /* end of array_hash */
/**Function********************************************************************
Synopsis [Comparison function for the computed table.]
Description [Comparison function for the computed table. Returns 0 if
the two arrays are equal; 1 otherwise.]
SideEffects [None]
SeeAlso []
******************************************************************************/
static int
array_compare(
const char * array1,
const char * array2)
{
int i;
int *intarray1, *intarray2;
intarray1 = (int *) array1;
intarray2 = (int *) array2;
for (i = 0; i < numvars; i++) {
if (intarray1[i] != intarray2[i]) return(1);
}
return(0);
} /* end of array_compare */
/**Function********************************************************************
Synopsis [Returns the index of the fittest individual.]
Description []
SideEffects [None]
SeeAlso []
******************************************************************************/
static int
find_best(void)
{
int i,small;
small = 0;
for (i = 1; i < popsize; i++) {
if (STOREDD(i,numvars) < STOREDD(small,numvars)) {
small = i;
}
}
return(small);
} /* end of find_best */
/**Function********************************************************************
Synopsis [Returns the average fitness of the population.]
Description []
SideEffects [None]
SeeAlso []
******************************************************************************/
#ifdef DD_STATS
static double
find_average_fitness(void)
{
int i;
int total_fitness = 0;
double average_fitness;
for (i = 0; i < popsize; i++) {
total_fitness += STOREDD(i,numvars);
}
average_fitness = (double) total_fitness / (double) popsize;
return(average_fitness);
} /* end of find_average_fitness */
#endif
/**Function********************************************************************
Synopsis [Performs the crossover between two parents.]
Description [Performs the crossover between two randomly chosen
parents, and creates two children, x1 and x2. Uses the Partially
Matched Crossover operator.]
SideEffects [None]
SeeAlso []
******************************************************************************/
static int
PMX(
int maxvar)
{
int cut1,cut2; /* the two cut positions (random) */
int mom,dad; /* the two randomly chosen parents */
int *inv1; /* inverse permutations for repair algo */
int *inv2;
int i; /* loop vars */
int u,v; /* aux vars */
inv1 = ALLOC(int,maxvar);
if (inv1 == NULL) {
return(0);
}
inv2 = ALLOC(int,maxvar);
if (inv2 == NULL) {
FREE(inv1);
return(0);
}
/* Choose two orders from the population using roulette wheel. */
if (!roulette(&mom,&dad)) {
FREE(inv1);
FREE(inv2);
return(0);
}
/* Choose two random cut positions. A cut in position i means that
** the cut immediately precedes position i. If cut1 < cut2, we
** exchange the middle of the two orderings; otherwise, we
** exchange the beginnings and the ends.
*/
cut1 = rand_int(numvars-1);
do {
cut2 = rand_int(numvars-1);
} while (cut1 == cut2);
#if 0
/* Print out the parents. */
(void) fprintf(table->out,
"Crossover of %d (mom) and %d (dad) between %d and %d\n",
mom,dad,cut1,cut2);
for (i = 0; i < numvars; i++) {
if (i == cut1 || i == cut2) (void) fprintf(table->out,"|");
(void) fprintf(table->out,"%2d ",STOREDD(mom,i));
}
(void) fprintf(table->out,"\n");
for (i = 0; i < numvars; i++) {
if (i == cut1 || i == cut2) (void) fprintf(table->out,"|");
(void) fprintf(table->out,"%2d ",STOREDD(dad,i));
}
(void) fprintf(table->out,"\n");
#endif
/* Initialize the inverse permutations: -1 means yet undetermined. */
for (i = 0; i < maxvar; i++) {
inv1[i] = -1;
inv2[i] = -1;
}
/* Copy the portions whithin the cuts. */
for (i = cut1; i != cut2; i = (i == numvars-1) ? 0 : i+1) {
STOREDD(popsize,i) = STOREDD(dad,i);
inv1[STOREDD(popsize,i)] = i;
STOREDD(popsize+1,i) = STOREDD(mom,i);
inv2[STOREDD(popsize+1,i)] = i;
}
/* Now apply the repair algorithm outside the cuts. */
for (i = cut2; i != cut1; i = (i == numvars-1 ) ? 0 : i+1) {
v = i;
do {
u = STOREDD(mom,v);
v = inv1[u];
} while (v != -1);
STOREDD(popsize,i) = u;
inv1[u] = i;
v = i;
do {
u = STOREDD(dad,v);
v = inv2[u];
} while (v != -1);
STOREDD(popsize+1,i) = u;
inv2[u] = i;
}
#if 0
/* Print the results of crossover. */
for (i = 0; i < numvars; i++) {
if (i == cut1 || i == cut2) (void) fprintf(table->out,"|");
(void) fprintf(table->out,"%2d ",STOREDD(popsize,i));
}
(void) fprintf(table->out,"\n");
for (i = 0; i < numvars; i++) {
if (i == cut1 || i == cut2) (void) fprintf(table->out,"|");
(void) fprintf(table->out,"%2d ",STOREDD(popsize+1,i));
}
(void) fprintf(table->out,"\n");
#endif
FREE(inv1);
FREE(inv2);
return(1);
} /* end of PMX */
/**Function********************************************************************
Synopsis [Selects two parents with the roulette wheel method.]
Description [Selects two distinct parents with the roulette wheel method.]
SideEffects [The indices of the selected parents are returned as side
effects.]
SeeAlso []
******************************************************************************/
static int
roulette(
int * p1,
int * p2)
{
double *wheel;
double spin;
int i;
wheel = ALLOC(double,popsize);
if (wheel == NULL) {
return(0);
}
/* The fitness of an individual is the reciprocal of its size. */
wheel[0] = 1.0 / (double) STOREDD(0,numvars);
for (i = 1; i < popsize; i++) {
wheel[i] = wheel[i-1] + 1.0 / (double) STOREDD(i,numvars);
}
/* Get a random number between 0 and wheel[popsize-1] (that is,
** the sum of all fitness values. 2147483561 is the largest number
** returned by Cudd_Random.
*/
spin = wheel[numvars-1] * (double) Cudd_Random() / 2147483561.0;
/* Find the lucky element by scanning the wheel. */
for (i = 0; i < popsize; i++) {
if (spin <= wheel[i]) break;
}
*p1 = i;
/* Repeat the process for the second parent, making sure it is
** distinct from the first.
*/
do {
spin = wheel[popsize-1] * (double) Cudd_Random() / 2147483561.0;
for (i = 0; i < popsize; i++) {
if (spin <= wheel[i]) break;
}
} while (i == *p1);
*p2 = i;
FREE(wheel);
return(1);
} /* end of roulette */

1190
resources/3rdparty/cudd-2.5.0/src/cudd/cuddInt.h
File diff suppressed because it is too large
View File

1331
resources/3rdparty/cudd-2.5.0/src/cudd/cuddSubsetHB.c
File diff suppressed because it is too large
View File

6776
resources/3rdparty/cudd-2.5.0/src/cudd/doc/cudd.doc
File diff suppressed because it is too large
View File

5036
resources/3rdparty/cudd-2.5.0/src/cudd/doc/cudd.ps
File diff suppressed because it is too large
View File

3114
resources/3rdparty/cudd-2.5.0/src/cudd/doc/cuddAllAbs.html
File diff suppressed because it is too large
View File

13
resources/3rdparty/cudd-2.5.0/src/cudd/doc/cuddAllByFile.html

@ -1,13 +0,0 @@
<HTML>
<HEAD><TITLE>The cudd package for maintainers</TITLE></HEAD>
<FRAMESET ROWS="5%,90%,5%">
<FRAME SRC="cuddTitle.html">
<FRAMESET COLS="40%,60%">
<FRAME SRC="cuddAllFile.html" NAME="ABSTRACT">
<FRAME SRC="cuddAllDet.html" NAME="MAIN">
</FRAMESET>
<FRAME SRC="credit.html">
</FRAMESET>
</HTML>

13
resources/3rdparty/cudd-2.5.0/src/cudd/doc/cuddAllByFunc.html

@ -1,13 +0,0 @@
<HTML>
<HEAD><TITLE>The cudd package for maintainers</TITLE></HEAD>
<FRAMESET ROWS="5%,90%,5%">
<FRAME SRC="cuddTitle.html">
<FRAMESET COLS="40%,60%">
<FRAME SRC="cuddAllAbs.html" NAME="ABSTRACT">
<FRAME SRC="cuddAllDet.html" NAME="MAIN">
</FRAMESET>
<FRAME SRC="credit.html">
</FRAMESET>
</HTML>

15754
resources/3rdparty/cudd-2.5.0/src/cudd/doc/cuddAllDet.html
File diff suppressed because it is too large
View File

4876
resources/3rdparty/cudd-2.5.0/src/cudd/doc/cuddAllFile.html
File diff suppressed because it is too large
View File

33
resources/3rdparty/cudd-2.5.0/src/cudd/doc/cuddDesc.html

@ -1,33 +0,0 @@
<HTML>
<HEAD><TITLE>The cudd package: Overview</TITLE></HEAD>
<BODY>
<H1>The cudd package</H1>
<H2>The University of Colorado decision diagram package.</H2>
<H3>By Fabio Somenzi</H3>
<UL>
<LI> <A HREF="cuddExt.html" TARGET="_top">
Information for programmers</A>
<LI> <A HREF="cuddAllByFunc.html" TARGET="_top">
Information for developers sorted by function</A>
<LI> <A HREF="cuddAllByFile.html" TARGET="_top">
Information for developers sorted by file</A>
</UL>
<HR>
External functions and data strucures of the CUDD package.
<ul>
<li> To turn on the gathering of statistics, define DD_STATS.
<li> To link with mis, define DD_MIS.
</ul>
Modified by Abelardo Pardo to interface it to VIS.
<HR>
Last updated on 20120204 17h33
</BODY>
</HTML>
writing ./cuddExt.html

14
resources/3rdparty/cudd-2.5.0/src/cudd/doc/cuddExt.html

@ -1,14 +0,0 @@
<HTML>
<HEAD><TITLE>The cudd Package for Programmers</TITLE></HEAD>
<FRAMESET ROWS="5%,90%,5%">
<FRAME SRC="cuddTitle.html">
<FRAMESET COLS="40%,60%">
<FRAME SRC="cuddExtAbs.html" NAME="ABSTRACT">
<FRAME SRC="cuddExtDet.html" NAME="MAIN">
</FRAMESET>
<FRAME SRC="credit.html">
</FRAMESET>
</HTML>
writing ./cuddAllByFunc.html

1415
resources/3rdparty/cudd-2.5.0/src/cudd/doc/cuddExtAbs.html
File diff suppressed because it is too large
View File

4450
resources/3rdparty/cudd-2.5.0/src/cudd/doc/cuddExtDet.html
File diff suppressed because it is too large
View File

30
resources/3rdparty/cudd-2.5.0/src/cudd/doc/cuddIntro.css

@ -1,30 +0,0 @@
/* Century Schoolbook font is very similar to Computer Modern Math: cmmi */
.MATH { font-family: "Century Schoolbook", serif; }
.MATH I { font-family: "Century Schoolbook", serif; font-style: italic }
.BOLDMATH { font-family: "Century Schoolbook", serif; font-weight: bold }
/* implement both fixed-size and relative sizes */
SMALL.XTINY { font-size : xx-small }
SMALL.TINY { font-size : x-small }
SMALL.SCRIPTSIZE { font-size : smaller }
SMALL.FOOTNOTESIZE { font-size : small }
SMALL.SMALL { }
BIG.LARGE { }
BIG.XLARGE { font-size : large }
BIG.XXLARGE { font-size : x-large }
BIG.HUGE { font-size : larger }
BIG.XHUGE { font-size : xx-large }
/* heading styles */
H1 { }
H2 { }
H3 { }
H4 { }
H5 { }
/* mathematics styles */
DIV.displaymath { } /* math displays */
TD.eqno { } /* equation-number cells */
/* document-specific styles come next */

219
resources/3rdparty/cudd-2.5.0/src/cudd/doc/cuddIntro.html

@ -1,219 +0,0 @@
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 3.2 Final//EN">
<!--Converted with LaTeX2HTML 2008 (1.71)
original version by: Nikos Drakos, CBLU, University of Leeds
* revised and updated by: Marcus Hennecke, Ross Moore, Herb Swan
* with significant contributions from:
Jens Lippmann, Marek Rouchal, Martin Wilck and others -->
<HTML>
<HEAD>
<TITLE>CUDD: CU Decision Diagram Package
Release 2.5.0</TITLE>
<META NAME="description" CONTENT="CUDD: CU Decision Diagram Package
Release 2.5.0">
<META NAME="keywords" CONTENT="cuddIntro">
<META NAME="resource-type" CONTENT="document">
<META NAME="distribution" CONTENT="global">
<META NAME="Generator" CONTENT="LaTeX2HTML v2008">
<META HTTP-EQUIV="Content-Style-Type" CONTENT="text/css">
<LINK REL="STYLESHEET" HREF="cuddIntro.css">
<LINK REL="next" HREF="node1.html">
</HEAD>
<BODY >
<!--Navigation Panel-->
<A NAME="tex2html14"
HREF="node1.html">
<IMG WIDTH="37" HEIGHT="24" ALIGN="BOTTOM" BORDER="0" ALT="next"
SRC="icons/next.png"></A>
<IMG WIDTH="26" HEIGHT="24" ALIGN="BOTTOM" BORDER="0" ALT="up"
SRC="icons/up_g.png">
<IMG WIDTH="63" HEIGHT="24" ALIGN="BOTTOM" BORDER="0" ALT="previous"
SRC="icons/prev_g.png">
<A NAME="tex2html12"
HREF="node8.html">
<IMG WIDTH="43" HEIGHT="24" ALIGN="BOTTOM" BORDER="0" ALT="index"
SRC="icons/index.png"></A>
<BR>
<B> Next:</B> <A NAME="tex2html15"
HREF="node1.html">Introduction</A>
&nbsp; <B> <A NAME="tex2html13"
HREF="node8.html">Index</A></B>
<BR>
<BR>
<!--End of Navigation Panel-->
<H1 ALIGN="CENTER">CUDD: CU Decision Diagram Package
<BR>
Release 2.5.0</H1>
<DIV>
<P ALIGN="CENTER"><STRONG>Fabio Somenzi</STRONG></P>
<P ALIGN="CENTER"><I>Department of Electrical, Computer, and Energy Engineering</I></P>
<P ALIGN="LEFT"><SMALL>University of Colorado at Boulder</SMALL></P>
</DIV>
<P>
<BR><HR>
<!--Table of Child-Links-->
<A NAME="CHILD_LINKS"></A>
<UL>
<LI><A NAME="tex2html16"
HREF="node1.html">Introduction</A>
<LI><A NAME="tex2html17"
HREF="node2.html">How to Get CUDD</A>
<UL>
<LI><A NAME="tex2html18"
HREF="node2.html#SECTION00021000000000000000">The CUDD Package</A>
<LI><A NAME="tex2html19"
HREF="node2.html#SECTION00022000000000000000">CUDD Friends</A>
</UL>
<BR>
<LI><A NAME="tex2html20"
HREF="node3.html">User's Manual</A>
<UL>
<LI><A NAME="tex2html21"
HREF="node3.html#SECTION00031000000000000000">Compiling and Linking</A>
<LI><A NAME="tex2html22"
HREF="node3.html#SECTION00032000000000000000">Basic Data Structures</A>
<UL>
<LI><A NAME="tex2html23"
HREF="node3.html#SECTION00032100000000000000">Nodes</A>
<LI><A NAME="tex2html24"
HREF="node3.html#SECTION00032200000000000000">The Manager</A>
<LI><A NAME="tex2html25"
HREF="node3.html#SECTION00032300000000000000">Cache</A>
</UL>
<LI><A NAME="tex2html26"
HREF="node3.html#SECTION00033000000000000000">Initializing and Shutting Down a DdManager</A>
<LI><A NAME="tex2html27"
HREF="node3.html#SECTION00034000000000000000">Setting Parameters</A>
<LI><A NAME="tex2html28"
HREF="node3.html#SECTION00035000000000000000">Constant Functions</A>
<UL>
<LI><A NAME="tex2html29"
HREF="node3.html#SECTION00035100000000000000">One, Logic Zero, and Arithmetic Zero</A>
<LI><A NAME="tex2html30"
HREF="node3.html#SECTION00035200000000000000">Predefined Constants</A>
<LI><A NAME="tex2html31"
HREF="node3.html#SECTION00035300000000000000">Background</A>
<LI><A NAME="tex2html32"
HREF="node3.html#SECTION00035400000000000000">New Constants</A>
</UL>
<LI><A NAME="tex2html33"
HREF="node3.html#SECTION00036000000000000000">Creating Variables</A>
<UL>
<LI><A NAME="tex2html34"
HREF="node3.html#SECTION00036100000000000000">New BDD and ADD Variables</A>
<LI><A NAME="tex2html35"
HREF="node3.html#SECTION00036200000000000000">New ZDD Variables</A>
</UL>
<LI><A NAME="tex2html36"
HREF="node3.html#SECTION00037000000000000000">Basic BDD Manipulation</A>
<LI><A NAME="tex2html37"
HREF="node3.html#SECTION00038000000000000000">Basic ADD Manipulation</A>
<LI><A NAME="tex2html38"
HREF="node3.html#SECTION00039000000000000000">Basic ZDD Manipulation</A>
<LI><A NAME="tex2html39"
HREF="node3.html#SECTION000310000000000000000">Converting ADDs to BDDs and Vice Versa</A>
<LI><A NAME="tex2html40"
HREF="node3.html#SECTION000311000000000000000">Converting BDDs to ZDDs and Vice Versa</A>
<LI><A NAME="tex2html41"
HREF="node3.html#SECTION000312000000000000000">Variable Reordering for BDDs and ADDs</A>
<LI><A NAME="tex2html42"
HREF="node3.html#SECTION000313000000000000000">Grouping Variables</A>
<LI><A NAME="tex2html43"
HREF="node3.html#SECTION000314000000000000000">Variable Reordering for ZDDs</A>
<LI><A NAME="tex2html44"
HREF="node3.html#SECTION000315000000000000000">Keeping Consistent Variable Orders for BDDs and ZDDs</A>
<LI><A NAME="tex2html45"
HREF="node3.html#SECTION000316000000000000000">Hooks</A>
<LI><A NAME="tex2html46"
HREF="node3.html#SECTION000317000000000000000">Timeouts and Limits</A>
<LI><A NAME="tex2html47"
HREF="node3.html#SECTION000318000000000000000">The SIS/VIS Interface</A>
<UL>
<LI><A NAME="tex2html48"
HREF="node3.html#SECTION000318100000000000000">Using the CUDD Package in SIS</A>
</UL>
<LI><A NAME="tex2html49"
HREF="node3.html#SECTION000319000000000000000">Writing Decision Diagrams to a File</A>
<LI><A NAME="tex2html50"
HREF="node3.html#SECTION000320000000000000000">Saving and Restoring BDDs</A>
</UL>
<BR>
<LI><A NAME="tex2html51"
HREF="node4.html">Programmer's Manual</A>
<UL>
<LI><A NAME="tex2html52"
HREF="node4.html#SECTION00041000000000000000">Compiling and Linking</A>
<LI><A NAME="tex2html53"
HREF="node4.html#SECTION00042000000000000000">Reference Counts</A>
<UL>
<LI><A NAME="tex2html54"
HREF="node4.html#SECTION00042100000000000000">NULL Return Values</A>
<LI><A NAME="tex2html55"
HREF="node4.html#SECTION00042200000000000000"><I>Cudd_RecursiveDeref</I> vs. <I>Cudd_Deref</I></A>
<LI><A NAME="tex2html56"
HREF="node4.html#SECTION00042300000000000000">When Increasing the Reference Count is Unnecessary</A>
<LI><A NAME="tex2html57"
HREF="node4.html#SECTION00042400000000000000">Saturating Increments and Decrements</A>
</UL>
<LI><A NAME="tex2html58"
HREF="node4.html#SECTION00043000000000000000">Complement Arcs</A>
<LI><A NAME="tex2html59"
HREF="node4.html#SECTION00044000000000000000">The Cache</A>
<UL>
<LI><A NAME="tex2html60"
HREF="node4.html#SECTION00044100000000000000">Cache Sizing</A>
<LI><A NAME="tex2html61"
HREF="node4.html#SECTION00044200000000000000">Local Caches</A>
</UL>
<LI><A NAME="tex2html62"
HREF="node4.html#SECTION00045000000000000000">The Unique Table</A>
<LI><A NAME="tex2html63"
HREF="node4.html#SECTION00046000000000000000">Allowing Asynchronous Reordering</A>
<LI><A NAME="tex2html64"
HREF="node4.html#SECTION00047000000000000000">Debugging</A>
<LI><A NAME="tex2html65"
HREF="node4.html#SECTION00048000000000000000">Gathering and Interpreting Statistics</A>
<UL>
<LI><A NAME="tex2html66"
HREF="node4.html#SECTION00048100000000000000">Non Modifiable Parameters</A>
<LI><A NAME="tex2html67"
HREF="node4.html#SECTION00048200000000000000">Modifiable Parameters</A>
<LI><A NAME="tex2html68"
HREF="node4.html#SECTION00048300000000000000">Extended Statistics and Reporting</A>
</UL>
<LI><A NAME="tex2html69"
HREF="node4.html#SECTION00049000000000000000">Guidelines for Documentation</A>
</UL>
<BR>
<LI><A NAME="tex2html70"
HREF="node5.html">The C++ Interface</A>
<UL>
<LI><A NAME="tex2html71"
HREF="node5.html#SECTION00051000000000000000">Compiling and Linking</A>
<LI><A NAME="tex2html72"
HREF="node5.html#SECTION00052000000000000000">Basic Manipulation</A>
</UL>
<BR>
<LI><A NAME="tex2html73"
HREF="node6.html">Acknowledgments</A>
<LI><A NAME="tex2html74"
HREF="node7.html">Bibliography</A>
<LI><A NAME="tex2html75"
HREF="node8.html">Index</A>
</UL>
<!--End of Table of Child-Links-->
<BR><HR>
<ADDRESS>
Fabio Somenzi
2012-02-04
</ADDRESS>
</BODY>
</HTML>

18
resources/3rdparty/cudd-2.5.0/src/cudd/doc/cuddTitle.html

@ -1,18 +0,0 @@
<HTML>
<HEAD><TITLE>The cudd package: Title</TITLE></HEAD>
<BODY>
<TABLE BORDER WIDTH="100%">
<TR>
<TD ALIGN=center> <A HREF="cuddExt.html" TARGET="_top">
Programmer view</A> </TD>
<TD ALIGN=center> <A HREF="cuddAllByFunc.html" TARGET="_top">
Maintainer by function</A> </TD>
<TD ALIGN=center> <A HREF="cuddAllByFile.html" TARGET="_top">
Maintainer by file</A> </TD>
</TR>
</TABLE>
</BODY>
</HTML>
writing ./cuddDesc.html

109
resources/3rdparty/cudd-2.5.0/src/cudd/doc/footnode.html

@ -1,109 +0,0 @@
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 3.2 Final//EN">
<!--Converted with LaTeX2HTML 2008 (1.71)
original version by: Nikos Drakos, CBLU, University of Leeds
* revised and updated by: Marcus Hennecke, Ross Moore, Herb Swan
* with significant contributions from:
Jens Lippmann, Marek Rouchal, Martin Wilck and others -->
<HTML>
<HEAD>
<TITLE>Footnotes</TITLE>
<META NAME="description" CONTENT="Footnotes">
<META NAME="keywords" CONTENT="cuddIntro">
<META NAME="resource-type" CONTENT="document">
<META NAME="distribution" CONTENT="global">
<META NAME="Generator" CONTENT="LaTeX2HTML v2008">
<META HTTP-EQUIV="Content-Style-Type" CONTENT="text/css">
<LINK REL="STYLESHEET" HREF="cuddIntro.css">
<LINK REL="previous" HREF="node7.html">
<LINK REL="up" HREF="cuddIntro.html">
</HEAD>
<BODY >
<DL>
<DT><A NAME="foot139">... application.</A><A
HREF="node3.html#tex2html3"><SUP>1</SUP></A></DT>
<DD>The
global statistical counters are used locally; hence they are
compatible with the use of multiple managers.
<PRE>.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
</PRE>
</DD>
<DT><A NAME="foot1083">...
node.</A><A
HREF="node3.html#tex2html4"><SUP>2</SUP></A></DT>
<DD>When the variables in a group are reordered, the
association between the <I>low</I> field and the index of the first
variable in the group is lost. The package updates the tree to keep
track of the changes. However, the application cannot rely on
<I>low</I> to determine the position of variables.
<PRE>.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
</PRE>
</DD>
</DL>
</BODY>
</HTML>

BIN
resources/3rdparty/cudd-2.5.0/src/cudd/doc/icons/blueball.png

Before

Width: 14  |  Height: 14  |  Size: 333 B

BIN
resources/3rdparty/cudd-2.5.0/src/cudd/doc/icons/ch_beg_r.png

Before

Width: 104  |  Height: 24  |  Size: 165 B

BIN
resources/3rdparty/cudd-2.5.0/src/cudd/doc/icons/ch_begin.png

Before

Width: 104  |  Height: 24  |  Size: 174 B

BIN
resources/3rdparty/cudd-2.5.0/src/cudd/doc/icons/ch_del_r.png

Before

Width: 109  |  Height: 24  |  Size: 288 B

BIN
resources/3rdparty/cudd-2.5.0/src/cudd/doc/icons/ch_delet.png

Before

Width: 109  |  Height: 24  |  Size: 288 B

BIN
resources/3rdparty/cudd-2.5.0/src/cudd/doc/icons/ch_end.png

Before

Width: 104  |  Height: 24  |  Size: 171 B

BIN
resources/3rdparty/cudd-2.5.0/src/cudd/doc/icons/ch_end_r.png

Before

Width: 104  |  Height: 24  |  Size: 155 B

BIN
resources/3rdparty/cudd-2.5.0/src/cudd/doc/icons/contents.png

Before

Width: 65  |  Height: 24  |  Size: 278 B

BIN
resources/3rdparty/cudd-2.5.0/src/cudd/doc/icons/crossref.png

Before

Width: 13  |  Height: 13  |  Size: 147 B

BIN
resources/3rdparty/cudd-2.5.0/src/cudd/doc/icons/footnote.png

Before

Width: 15  |  Height: 15  |  Size: 190 B

BIN
resources/3rdparty/cudd-2.5.0/src/cudd/doc/icons/greenball.png

Before

Width: 14  |  Height: 14  |  Size: 333 B

BIN
resources/3rdparty/cudd-2.5.0/src/cudd/doc/icons/image.png

Before

Width: 48  |  Height: 24  |  Size: 244 B

BIN
resources/3rdparty/cudd-2.5.0/src/cudd/doc/icons/index.png

Before

Width: 43  |  Height: 24  |  Size: 246 B

BIN
resources/3rdparty/cudd-2.5.0/src/cudd/doc/icons/next.png

Before

Width: 37  |  Height: 24  |  Size: 245 B

BIN
resources/3rdparty/cudd-2.5.0/src/cudd/doc/icons/next_g.png

Before

Width: 37  |  Height: 24  |  Size: 272 B

BIN
resources/3rdparty/cudd-2.5.0/src/cudd/doc/icons/nx_grp.png

Before

Width: 81  |  Height: 24  |  Size: 314 B

BIN
resources/3rdparty/cudd-2.5.0/src/cudd/doc/icons/nx_grp_g.png

Before

Width: 81  |  Height: 24  |  Size: 386 B

BIN
resources/3rdparty/cudd-2.5.0/src/cudd/doc/icons/orangeball.png

Before

Width: 14  |  Height: 14  |  Size: 333 B

BIN
resources/3rdparty/cudd-2.5.0/src/cudd/doc/icons/pinkball.png

Before

Width: 14  |  Height: 14  |  Size: 332 B

BIN
resources/3rdparty/cudd-2.5.0/src/cudd/doc/icons/prev.png

Before

Width: 63  |  Height: 24  |  Size: 279 B

BIN
resources/3rdparty/cudd-2.5.0/src/cudd/doc/icons/prev_g.png

Before

Width: 63  |  Height: 24  |  Size: 327 B

BIN
resources/3rdparty/cudd-2.5.0/src/cudd/doc/icons/purpleball.png

Before

Width: 14  |  Height: 14  |  Size: 332 B

BIN
resources/3rdparty/cudd-2.5.0/src/cudd/doc/icons/pv_grp.png

Before

Width: 107  |  Height: 24  |  Size: 352 B

BIN
resources/3rdparty/cudd-2.5.0/src/cudd/doc/icons/pv_grp_g.png

Before

Width: 107  |  Height: 24  |  Size: 430 B

BIN
resources/3rdparty/cudd-2.5.0/src/cudd/doc/icons/redball.png

Before

Width: 14  |  Height: 14  |  Size: 332 B

BIN
resources/3rdparty/cudd-2.5.0/src/cudd/doc/icons/up.png

Before

Width: 26  |  Height: 24  |  Size: 211 B

BIN
resources/3rdparty/cudd-2.5.0/src/cudd/doc/icons/up_g.png

Before

Width: 26  |  Height: 24  |  Size: 231 B

BIN
resources/3rdparty/cudd-2.5.0/src/cudd/doc/icons/whiteball.png

Before

Width: 14  |  Height: 14  |  Size: 229 B

BIN
resources/3rdparty/cudd-2.5.0/src/cudd/doc/icons/yellowball.png

Before

Width: 14  |  Height: 14  |  Size: 333 B

BIN
resources/3rdparty/cudd-2.5.0/src/cudd/doc/img1.png

Before

Width: 18  |  Height: 32  |  Size: 201 B

BIN
resources/3rdparty/cudd-2.5.0/src/cudd/doc/img10.png

Before

Width: 14  |  Height: 15  |  Size: 211 B

BIN
resources/3rdparty/cudd-2.5.0/src/cudd/doc/img11.png

Before

Width: 95  |  Height: 35  |  Size: 476 B

BIN
resources/3rdparty/cudd-2.5.0/src/cudd/doc/img12.png

Before

Width: 108  |  Height: 35  |  Size: 555 B

BIN
resources/3rdparty/cudd-2.5.0/src/cudd/doc/img13.png

Before

Width: 117  |  Height: 33  |  Size: 560 B

BIN
resources/3rdparty/cudd-2.5.0/src/cudd/doc/img14.png

Before

Width: 172  |  Height: 35  |  Size: 675 B

BIN
resources/3rdparty/cudd-2.5.0/src/cudd/doc/img15.png

Before

Width: 16  |  Height: 15  |  Size: 200 B

BIN
resources/3rdparty/cudd-2.5.0/src/cudd/doc/img16.png

Before

Width: 18  |  Height: 15  |  Size: 223 B

BIN
resources/3rdparty/cudd-2.5.0/src/cudd/doc/img17.png

Before

Width: 19  |  Height: 15  |  Size: 246 B

BIN
resources/3rdparty/cudd-2.5.0/src/cudd/doc/img18.png

Before

Width: 49  |  Height: 32  |  Size: 298 B

BIN
resources/3rdparty/cudd-2.5.0/src/cudd/doc/img19.png

Before

Width: 94  |  Height: 33  |  Size: 409 B

BIN
resources/3rdparty/cudd-2.5.0/src/cudd/doc/img2.png

Before

Width: 18  |  Height: 32  |  Size: 197 B

BIN
resources/3rdparty/cudd-2.5.0/src/cudd/doc/img20.png

Before

Width: 22  |  Height: 32  |  Size: 238 B

BIN
resources/3rdparty/cudd-2.5.0/src/cudd/doc/img21.png

Before

Width: 124  |  Height: 35  |  Size: 614 B

BIN
resources/3rdparty/cudd-2.5.0/src/cudd/doc/img22.png

Before

Width: 429  |  Height: 701  |  Size: 12 KiB

BIN
resources/3rdparty/cudd-2.5.0/src/cudd/doc/img3.png

Before

Width: 56  |  Height: 35  |  Size: 401 B

BIN
resources/3rdparty/cudd-2.5.0/src/cudd/doc/img4.png

Before

Width: 15  |  Height: 15  |  Size: 204 B

BIN
resources/3rdparty/cudd-2.5.0/src/cudd/doc/img5.png

Before

Width: 47  |  Height: 18  |  Size: 315 B

BIN
resources/3rdparty/cudd-2.5.0/src/cudd/doc/img6.png

Before

Width: 10  |  Height: 15  |  Size: 185 B

BIN
resources/3rdparty/cudd-2.5.0/src/cudd/doc/img7.png

Before

Width: 45  |  Height: 32  |  Size: 262 B

BIN
resources/3rdparty/cudd-2.5.0/src/cudd/doc/img8.png

Before

Width: 15  |  Height: 33  |  Size: 220 B

BIN
resources/3rdparty/cudd-2.5.0/src/cudd/doc/img9.png

Before

Width: 13  |  Height: 32  |  Size: 215 B

219
resources/3rdparty/cudd-2.5.0/src/cudd/doc/index.html

@ -1,219 +0,0 @@
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 3.2 Final//EN">
<!--Converted with LaTeX2HTML 2008 (1.71)
original version by: Nikos Drakos, CBLU, University of Leeds
* revised and updated by: Marcus Hennecke, Ross Moore, Herb Swan
* with significant contributions from:
Jens Lippmann, Marek Rouchal, Martin Wilck and others -->
<HTML>
<HEAD>
<TITLE>CUDD: CU Decision Diagram Package
Release 2.5.0</TITLE>
<META NAME="description" CONTENT="CUDD: CU Decision Diagram Package
Release 2.5.0">
<META NAME="keywords" CONTENT="cuddIntro">
<META NAME="resource-type" CONTENT="document">
<META NAME="distribution" CONTENT="global">
<META NAME="Generator" CONTENT="LaTeX2HTML v2008">
<META HTTP-EQUIV="Content-Style-Type" CONTENT="text/css">
<LINK REL="STYLESHEET" HREF="cuddIntro.css">
<LINK REL="next" HREF="node1.html">
</HEAD>
<BODY >
<!--Navigation Panel-->
<A NAME="tex2html14"
HREF="node1.html">
<IMG WIDTH="37" HEIGHT="24" ALIGN="BOTTOM" BORDER="0" ALT="next"
SRC="icons/next.png"></A>
<IMG WIDTH="26" HEIGHT="24" ALIGN="BOTTOM" BORDER="0" ALT="up"
SRC="icons/up_g.png">
<IMG WIDTH="63" HEIGHT="24" ALIGN="BOTTOM" BORDER="0" ALT="previous"
SRC="icons/prev_g.png">
<A NAME="tex2html12"
HREF="node8.html">
<IMG WIDTH="43" HEIGHT="24" ALIGN="BOTTOM" BORDER="0" ALT="index"
SRC="icons/index.png"></A>
<BR>
<B> Next:</B> <A NAME="tex2html15"
HREF="node1.html">Introduction</A>
&nbsp; <B> <A NAME="tex2html13"
HREF="node8.html">Index</A></B>
<BR>
<BR>
<!--End of Navigation Panel-->
<H1 ALIGN="CENTER">CUDD: CU Decision Diagram Package
<BR>
Release 2.5.0</H1>
<DIV>
<P ALIGN="CENTER"><STRONG>Fabio Somenzi</STRONG></P>
<P ALIGN="CENTER"><I>Department of Electrical, Computer, and Energy Engineering</I></P>
<P ALIGN="LEFT"><SMALL>University of Colorado at Boulder</SMALL></P>
</DIV>
<P>
<BR><HR>
<!--Table of Child-Links-->
<A NAME="CHILD_LINKS"></A>
<UL>
<LI><A NAME="tex2html16"
HREF="node1.html">Introduction</A>
<LI><A NAME="tex2html17"
HREF="node2.html">How to Get CUDD</A>
<UL>
<LI><A NAME="tex2html18"
HREF="node2.html#SECTION00021000000000000000">The CUDD Package</A>
<LI><A NAME="tex2html19"
HREF="node2.html#SECTION00022000000000000000">CUDD Friends</A>
</UL>
<BR>
<LI><A NAME="tex2html20"
HREF="node3.html">User's Manual</A>
<UL>
<LI><A NAME="tex2html21"
HREF="node3.html#SECTION00031000000000000000">Compiling and Linking</A>
<LI><A NAME="tex2html22"
HREF="node3.html#SECTION00032000000000000000">Basic Data Structures</A>
<UL>
<LI><A NAME="tex2html23"
HREF="node3.html#SECTION00032100000000000000">Nodes</A>
<LI><A NAME="tex2html24"
HREF="node3.html#SECTION00032200000000000000">The Manager</A>
<LI><A NAME="tex2html25"
HREF="node3.html#SECTION00032300000000000000">Cache</A>
</UL>
<LI><A NAME="tex2html26"
HREF="node3.html#SECTION00033000000000000000">Initializing and Shutting Down a DdManager</A>
<LI><A NAME="tex2html27"
HREF="node3.html#SECTION00034000000000000000">Setting Parameters</A>
<LI><A NAME="tex2html28"
HREF="node3.html#SECTION00035000000000000000">Constant Functions</A>
<UL>
<LI><A NAME="tex2html29"
HREF="node3.html#SECTION00035100000000000000">One, Logic Zero, and Arithmetic Zero</A>
<LI><A NAME="tex2html30"
HREF="node3.html#SECTION00035200000000000000">Predefined Constants</A>
<LI><A NAME="tex2html31"
HREF="node3.html#SECTION00035300000000000000">Background</A>
<LI><A NAME="tex2html32"
HREF="node3.html#SECTION00035400000000000000">New Constants</A>
</UL>
<LI><A NAME="tex2html33"
HREF="node3.html#SECTION00036000000000000000">Creating Variables</A>
<UL>
<LI><A NAME="tex2html34"
HREF="node3.html#SECTION00036100000000000000">New BDD and ADD Variables</A>
<LI><A NAME="tex2html35"
HREF="node3.html#SECTION00036200000000000000">New ZDD Variables</A>
</UL>
<LI><A NAME="tex2html36"
HREF="node3.html#SECTION00037000000000000000">Basic BDD Manipulation</A>
<LI><A NAME="tex2html37"
HREF="node3.html#SECTION00038000000000000000">Basic ADD Manipulation</A>
<LI><A NAME="tex2html38"
HREF="node3.html#SECTION00039000000000000000">Basic ZDD Manipulation</A>
<LI><A NAME="tex2html39"
HREF="node3.html#SECTION000310000000000000000">Converting ADDs to BDDs and Vice Versa</A>
<LI><A NAME="tex2html40"
HREF="node3.html#SECTION000311000000000000000">Converting BDDs to ZDDs and Vice Versa</A>
<LI><A NAME="tex2html41"
HREF="node3.html#SECTION000312000000000000000">Variable Reordering for BDDs and ADDs</A>
<LI><A NAME="tex2html42"
HREF="node3.html#SECTION000313000000000000000">Grouping Variables</A>
<LI><A NAME="tex2html43"
HREF="node3.html#SECTION000314000000000000000">Variable Reordering for ZDDs</A>
<LI><A NAME="tex2html44"
HREF="node3.html#SECTION000315000000000000000">Keeping Consistent Variable Orders for BDDs and ZDDs</A>
<LI><A NAME="tex2html45"
HREF="node3.html#SECTION000316000000000000000">Hooks</A>
<LI><A NAME="tex2html46"
HREF="node3.html#SECTION000317000000000000000">Timeouts and Limits</A>
<LI><A NAME="tex2html47"
HREF="node3.html#SECTION000318000000000000000">The SIS/VIS Interface</A>
<UL>
<LI><A NAME="tex2html48"
HREF="node3.html#SECTION000318100000000000000">Using the CUDD Package in SIS</A>
</UL>
<LI><A NAME="tex2html49"
HREF="node3.html#SECTION000319000000000000000">Writing Decision Diagrams to a File</A>
<LI><A NAME="tex2html50"
HREF="node3.html#SECTION000320000000000000000">Saving and Restoring BDDs</A>
</UL>
<BR>
<LI><A NAME="tex2html51"
HREF="node4.html">Programmer's Manual</A>
<UL>
<LI><A NAME="tex2html52"
HREF="node4.html#SECTION00041000000000000000">Compiling and Linking</A>
<LI><A NAME="tex2html53"
HREF="node4.html#SECTION00042000000000000000">Reference Counts</A>
<UL>
<LI><A NAME="tex2html54"
HREF="node4.html#SECTION00042100000000000000">NULL Return Values</A>
<LI><A NAME="tex2html55"
HREF="node4.html#SECTION00042200000000000000"><I>Cudd_RecursiveDeref</I> vs. <I>Cudd_Deref</I></A>
<LI><A NAME="tex2html56"
HREF="node4.html#SECTION00042300000000000000">When Increasing the Reference Count is Unnecessary</A>
<LI><A NAME="tex2html57"
HREF="node4.html#SECTION00042400000000000000">Saturating Increments and Decrements</A>
</UL>
<LI><A NAME="tex2html58"
HREF="node4.html#SECTION00043000000000000000">Complement Arcs</A>
<LI><A NAME="tex2html59"
HREF="node4.html#SECTION00044000000000000000">The Cache</A>
<UL>
<LI><A NAME="tex2html60"
HREF="node4.html#SECTION00044100000000000000">Cache Sizing</A>
<LI><A NAME="tex2html61"
HREF="node4.html#SECTION00044200000000000000">Local Caches</A>
</UL>
<LI><A NAME="tex2html62"
HREF="node4.html#SECTION00045000000000000000">The Unique Table</A>
<LI><A NAME="tex2html63"
HREF="node4.html#SECTION00046000000000000000">Allowing Asynchronous Reordering</A>
<LI><A NAME="tex2html64"
HREF="node4.html#SECTION00047000000000000000">Debugging</A>
<LI><A NAME="tex2html65"
HREF="node4.html#SECTION00048000000000000000">Gathering and Interpreting Statistics</A>
<UL>
<LI><A NAME="tex2html66"
HREF="node4.html#SECTION00048100000000000000">Non Modifiable Parameters</A>
<LI><A NAME="tex2html67"
HREF="node4.html#SECTION00048200000000000000">Modifiable Parameters</A>
<LI><A NAME="tex2html68"
HREF="node4.html#SECTION00048300000000000000">Extended Statistics and Reporting</A>
</UL>
<LI><A NAME="tex2html69"
HREF="node4.html#SECTION00049000000000000000">Guidelines for Documentation</A>
</UL>
<BR>
<LI><A NAME="tex2html70"
HREF="node5.html">The C++ Interface</A>
<UL>
<LI><A NAME="tex2html71"
HREF="node5.html#SECTION00051000000000000000">Compiling and Linking</A>
<LI><A NAME="tex2html72"
HREF="node5.html#SECTION00052000000000000000">Basic Manipulation</A>
</UL>
<BR>
<LI><A NAME="tex2html73"
HREF="node6.html">Acknowledgments</A>
<LI><A NAME="tex2html74"
HREF="node7.html">Bibliography</A>
<LI><A NAME="tex2html75"
HREF="node8.html">Index</A>
</UL>
<!--End of Table of Child-Links-->
<BR><HR>
<ADDRESS>
Fabio Somenzi
2012-02-04
</ADDRESS>
</BODY>
</HTML>

174
resources/3rdparty/cudd-2.5.0/src/cudd/doc/node1.html

@ -1,174 +0,0 @@
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 3.2 Final//EN">
<!--Converted with LaTeX2HTML 2008 (1.71)
original version by: Nikos Drakos, CBLU, University of Leeds
* revised and updated by: Marcus Hennecke, Ross Moore, Herb Swan
* with significant contributions from:
Jens Lippmann, Marek Rouchal, Martin Wilck and others -->
<HTML>
<HEAD>
<TITLE>Introduction</TITLE>
<META NAME="description" CONTENT="Introduction">
<META NAME="keywords" CONTENT="cuddIntro">
<META NAME="resource-type" CONTENT="document">
<META NAME="distribution" CONTENT="global">
<META NAME="Generator" CONTENT="LaTeX2HTML v2008">
<META HTTP-EQUIV="Content-Style-Type" CONTENT="text/css">
<LINK REL="STYLESHEET" HREF="cuddIntro.css">
<LINK REL="next" HREF="node2.html">
<LINK REL="previous" HREF="cuddIntro.html">
<LINK REL="up" HREF="cuddIntro.html">
<LINK REL="next" HREF="node2.html">
</HEAD>
<BODY >
<!--Navigation Panel-->
<A NAME="tex2html86"
HREF="node2.html">
<IMG WIDTH="37" HEIGHT="24" ALIGN="BOTTOM" BORDER="0" ALT="next"
SRC="icons/next.png"></A>
<A NAME="tex2html82"
HREF="cuddIntro.html">
<IMG WIDTH="26" HEIGHT="24" ALIGN="BOTTOM" BORDER="0" ALT="up"
SRC="icons/up.png"></A>
<A NAME="tex2html76"
HREF="cuddIntro.html">
<IMG WIDTH="63" HEIGHT="24" ALIGN="BOTTOM" BORDER="0" ALT="previous"
SRC="icons/prev.png"></A>
<A NAME="tex2html84"
HREF="node8.html">
<IMG WIDTH="43" HEIGHT="24" ALIGN="BOTTOM" BORDER="0" ALT="index"
SRC="icons/index.png"></A>
<BR>
<B> Next:</B> <A NAME="tex2html87"
HREF="node2.html">How to Get CUDD</A>
<B> Up:</B> <A NAME="tex2html83"
HREF="cuddIntro.html">CUDD: CU Decision Diagram</A>
<B> Previous:</B> <A NAME="tex2html77"
HREF="cuddIntro.html">CUDD: CU Decision Diagram</A>
&nbsp; <B> <A NAME="tex2html85"
HREF="node8.html">Index</A></B>
<BR>
<BR>
<!--End of Navigation Panel-->
<H1><A NAME="SECTION00010000000000000000"></A>
<A NAME="sec:intro"></A>
<BR>
Introduction
</H1>
<P>
The CUDD package provides functions to manipulate Binary Decision
Diagrams<A NAME="14"></A> (BDDs) [<A
HREF="node7.html#BDD">5</A>,<A
HREF="node7.html#BBR">3</A>],
Algebraic Decision Diagrams<A NAME="16"></A> (ADDs)
[<A
HREF="node7.html#Bahar93">1</A>], and Zero-suppressed Binary Decision
Diagrams<A NAME="18"></A> (ZDDs)
[<A
HREF="node7.html#Minato93">12</A>]. BDDs are used to represent
switching<A NAME="20"></A> functions; ADDs are used to
represent function from <IMG
WIDTH="56" HEIGHT="35" ALIGN="MIDDLE" BORDER="0"
SRC="img3.png"
ALT="$\{0,1\}^n$"> to an arbitrary set. ZDDs
represent switching<A NAME="21"></A> functions like BDDs;
however, they are much more efficient than BDDs when the functions to
be represented are characteristic<A NAME="22"></A>
functions of cube<A NAME="23"></A> sets, or in general, when the
ON-set<A NAME="24"></A> of the function to be represented is
very sparse. They are inferior to BDDs in other cases.
<P>
The package provides a large set of operations on BDDs, ADDs, and
ZDDs, functions to convert BDDs into ADDs or ZDDs and vice versa, and
a large assortment of variable reordering<A NAME="25"></A> methods.
<P>
The CUDD package can be used in three ways:
<UL>
<LI>As a black box<A NAME="27"></A>. In this case, the application
program that needs to manipulate decision diagrams only uses the
exported functions of the package. The rich set of functions
included in the CUDD package allows many applications to be written
in this way. Section&nbsp;<A HREF="node3.html#sec:user">3</A> describes how to use the
exported functions of the package. An application written in terms
of the exported functions of the package needs not concern itself
with the details of variable reordering<A NAME="29"></A>, which may
take place behind the scenes.
Click <A NAME="tex2html1"
HREF="cuddExtAbs.html">here</A>
for a list of the
exported functions.
</LI>
<LI>As a clear box<A NAME="32"></A>. When writing a sophisticated
application based on decision diagrams, efficiency often dictates
that some functions be implemented as direct recursive manipulation
of the diagrams, instead of being written in terms of existing
primitive functions. Section&nbsp;<A HREF="node4.html#sec:prog">4</A> explains how to add new
functions to the CUDD package. It also details how to write a
recursive function that can be interrupted by
dynamic<A NAME="34"></A> variable reordering.
Click <A NAME="tex2html2"
HREF="cuddAllAbs.html">here</A>
for a list of the
exported and internal functions.
</LI>
<LI>Through an interface. Object-oriented languages like C++ and
Perl5 can free the programmer from the burden of memory management.
A C++ interface is included in the distribution of CUDD. It
automatically frees decision diagrams that are no longer used by the
application and overloads operators. Almost all the functionality
provided by the CUDD exported functions is available through the C++
interface, which is especially recommended for fast prototyping.
Section&nbsp;<A HREF="node5.html#sec:cpp">5</A> explains how to use the interface. A Perl5
interface also exists and is ditributed separately. (See
Section&nbsp;<A HREF="node2.html#sec:getFriends">2.2</A>.) Some applications define their own
interfaces. See for example Section&nbsp;<A HREF="node3.html#sec:sis-vis">3.18</A>.
</LI>
</UL>
In the following, the reader is supposed to be familiar with the basic
ideas about decision diagrams, as found, for instance, in [<A
HREF="node7.html#BBR">3</A>].
<P>
<HR>
<!--Navigation Panel-->
<A NAME="tex2html86"
HREF="node2.html">
<IMG WIDTH="37" HEIGHT="24" ALIGN="BOTTOM" BORDER="0" ALT="next"
SRC="icons/next.png"></A>
<A NAME="tex2html82"
HREF="cuddIntro.html">
<IMG WIDTH="26" HEIGHT="24" ALIGN="BOTTOM" BORDER="0" ALT="up"
SRC="icons/up.png"></A>
<A NAME="tex2html76"
HREF="cuddIntro.html">
<IMG WIDTH="63" HEIGHT="24" ALIGN="BOTTOM" BORDER="0" ALT="previous"
SRC="icons/prev.png"></A>
<A NAME="tex2html84"
HREF="node8.html">
<IMG WIDTH="43" HEIGHT="24" ALIGN="BOTTOM" BORDER="0" ALT="index"
SRC="icons/index.png"></A>
<BR>
<B> Next:</B> <A NAME="tex2html87"
HREF="node2.html">How to Get CUDD</A>
<B> Up:</B> <A NAME="tex2html83"
HREF="cuddIntro.html">CUDD: CU Decision Diagram</A>
<B> Previous:</B> <A NAME="tex2html77"
HREF="cuddIntro.html">CUDD: CU Decision Diagram</A>
&nbsp; <B> <A NAME="tex2html85"
HREF="node8.html">Index</A></B>
<!--End of Navigation Panel-->
<ADDRESS>
Fabio Somenzi
2012-02-04
</ADDRESS>
</BODY>
</HTML>

175
resources/3rdparty/cudd-2.5.0/src/cudd/doc/node2.html

@ -1,175 +0,0 @@
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 3.2 Final//EN">
<!--Converted with LaTeX2HTML 2008 (1.71)
original version by: Nikos Drakos, CBLU, University of Leeds
* revised and updated by: Marcus Hennecke, Ross Moore, Herb Swan
* with significant contributions from:
Jens Lippmann, Marek Rouchal, Martin Wilck and others -->
<HTML>
<HEAD>
<TITLE>How to Get CUDD</TITLE>
<META NAME="description" CONTENT="How to Get CUDD">
<META NAME="keywords" CONTENT="cuddIntro">
<META NAME="resource-type" CONTENT="document">
<META NAME="distribution" CONTENT="global">
<META NAME="Generator" CONTENT="LaTeX2HTML v2008">
<META HTTP-EQUIV="Content-Style-Type" CONTENT="text/css">
<LINK REL="STYLESHEET" HREF="cuddIntro.css">
<LINK REL="next" HREF="node3.html">
<LINK REL="previous" HREF="node1.html">
<LINK REL="up" HREF="cuddIntro.html">
<LINK REL="next" HREF="node3.html">
</HEAD>
<BODY >
<!--Navigation Panel-->
<A NAME="tex2html98"
HREF="node3.html">
<IMG WIDTH="37" HEIGHT="24" ALIGN="BOTTOM" BORDER="0" ALT="next"
SRC="icons/next.png"></A>
<A NAME="tex2html94"
HREF="cuddIntro.html">
<IMG WIDTH="26" HEIGHT="24" ALIGN="BOTTOM" BORDER="0" ALT="up"
SRC="icons/up.png"></A>
<A NAME="tex2html88"
HREF="node1.html">
<IMG WIDTH="63" HEIGHT="24" ALIGN="BOTTOM" BORDER="0" ALT="previous"
SRC="icons/prev.png"></A>
<A NAME="tex2html96"
HREF="node8.html">
<IMG WIDTH="43" HEIGHT="24" ALIGN="BOTTOM" BORDER="0" ALT="index"
SRC="icons/index.png"></A>
<BR>
<B> Next:</B> <A NAME="tex2html99"
HREF="node3.html">User's Manual</A>
<B> Up:</B> <A NAME="tex2html95"
HREF="cuddIntro.html">CUDD: CU Decision Diagram</A>
<B> Previous:</B> <A NAME="tex2html89"
HREF="node1.html">Introduction</A>
&nbsp; <B> <A NAME="tex2html97"
HREF="node8.html">Index</A></B>
<BR>
<BR>
<!--End of Navigation Panel-->
<!--Table of Child-Links-->
<A NAME="CHILD_LINKS"><STRONG>Subsections</STRONG></A>
<UL>
<LI><A NAME="tex2html100"
HREF="node2.html#SECTION00021000000000000000">The CUDD Package</A>
<LI><A NAME="tex2html101"
HREF="node2.html#SECTION00022000000000000000">CUDD Friends</A>
</UL>
<!--End of Table of Child-Links-->
<HR>
<H1><A NAME="SECTION00020000000000000000"></A>
<A NAME="sec:getting"></A>
<BR>
How to Get CUDD
</H1>
<P>
<H2><A NAME="SECTION00021000000000000000"></A>
<A NAME="sec:getCUDD"></A>
<BR>
The CUDD Package
</H2>
<P>
The CUDD package is available via anonymous FTP<A NAME="46"></A> from
vlsi.Colorado.EDU. A compressed tar file named
<TT>cudd-2.5.0.tar.gz</TT> can be found in directory <TT>pub</TT>.
Once you have this file,
<BLOCKQUOTE>
<TT>gzip<A NAME="50"></A> -dc cudd-2.5.0.tar.gz | tar xvf -
</TT></BLOCKQUOTE>
will create directory <TT>cudd-2.5.0</TT> and its subdirectories.
These directories contain the decision diagram package, a few support
libraries<A NAME="53"></A>, and a toy application based on the
decision diagram package. There is a README<A NAME="54"></A> file
with instructions on configuration<A NAME="55"></A> and
installation<A NAME="56"></A> in <TT>cudd-2.5.0</TT>. You can use
a compiler for either ANSI C or C++.
<P>
Once you have made the libraries and program, you can type:
<BLOCKQUOTE>
<TT>cd nanotrav<A NAME="59"></A>
<BR>
nanotrav -p 1 -autodyn -reordering sifting -trav mult32a.blif
</TT></BLOCKQUOTE>
This will run a simple-minded FSM traversal program. (On a 2.4 GHz
Pentium 4<A NAME="61"></A> (TM), it takes about 0.5 s.) The
output produced by the program can be checked against
<TT>cudd-2.5.0/nanotrav/mult32a.out</TT>. More information on the
<TT>nanotrav<A NAME="63"></A></TT> program can be found in
<TT>cudd-2.5.0/nanotrav/README<A NAME="64"></A></TT>.
<P>
If you want to be notified of new releases of the CUDD package, send a
message to <TT>Fabio@Colorado.EDU</TT>.
<P>
<H2><A NAME="SECTION00022000000000000000"></A>
<A NAME="sec:getFriends"></A>
<BR>
CUDD Friends
</H2>
<P>
Two CUDD extensions are available via anonymous FTP<A NAME="68"></A> from
vlsi.Colorado.EDU.
<UL>
<LI><I>PerlDD</I> is an object-oriented Perl5 interface to CUDD. It
is organized as a standard Perl extension module. The Perl interface
is at a somewhat higher level than the C++ interface, but it is not
as complete.
</LI>
<LI><I>DDcal</I> is a graphic BDD calculator based on CUDD, Perl-Tk,
and dot. (See Section&nbsp;<A HREF="node3.html#sec:dump">3.19</A> for information on <I>dot</I>.)
<P>
</LI>
</UL><HR>
<!--Navigation Panel-->
<A NAME="tex2html98"
HREF="node3.html">
<IMG WIDTH="37" HEIGHT="24" ALIGN="BOTTOM" BORDER="0" ALT="next"
SRC="icons/next.png"></A>
<A NAME="tex2html94"
HREF="cuddIntro.html">
<IMG WIDTH="26" HEIGHT="24" ALIGN="BOTTOM" BORDER="0" ALT="up"
SRC="icons/up.png"></A>
<A NAME="tex2html88"
HREF="node1.html">
<IMG WIDTH="63" HEIGHT="24" ALIGN="BOTTOM" BORDER="0" ALT="previous"
SRC="icons/prev.png"></A>
<A NAME="tex2html96"
HREF="node8.html">
<IMG WIDTH="43" HEIGHT="24" ALIGN="BOTTOM" BORDER="0" ALT="index"
SRC="icons/index.png"></A>
<BR>
<B> Next:</B> <A NAME="tex2html99"
HREF="node3.html">User's Manual</A>
<B> Up:</B> <A NAME="tex2html95"
HREF="cuddIntro.html">CUDD: CU Decision Diagram</A>
<B> Previous:</B> <A NAME="tex2html89"
HREF="node1.html">Introduction</A>
&nbsp; <B> <A NAME="tex2html97"
HREF="node8.html">Index</A></B>
<!--End of Navigation Panel-->
<ADDRESS>
Fabio Somenzi
2012-02-04
</ADDRESS>
</BODY>
</HTML>

1637
resources/3rdparty/cudd-2.5.0/src/cudd/doc/node3.html
File diff suppressed because it is too large
View File

1165
resources/3rdparty/cudd-2.5.0/src/cudd/doc/node4.html
File diff suppressed because it is too large
View File

130
resources/3rdparty/cudd-2.5.0/src/cudd/doc/node5.html

@ -1,130 +0,0 @@
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 3.2 Final//EN">
<!--Converted with LaTeX2HTML 2008 (1.71)
original version by: Nikos Drakos, CBLU, University of Leeds
* revised and updated by: Marcus Hennecke, Ross Moore, Herb Swan
* with significant contributions from:
Jens Lippmann, Marek Rouchal, Martin Wilck and others -->
<HTML>
<HEAD>
<TITLE>The C++ Interface</TITLE>
<META NAME="description" CONTENT="The C++ Interface">
<META NAME="keywords" CONTENT="cuddIntro">
<META NAME="resource-type" CONTENT="document">
<META NAME="distribution" CONTENT="global">
<META NAME="Generator" CONTENT="LaTeX2HTML v2008">
<META HTTP-EQUIV="Content-Style-Type" CONTENT="text/css">
<LINK REL="STYLESHEET" HREF="cuddIntro.css">
<LINK REL="next" HREF="node6.html">
<LINK REL="previous" HREF="node4.html">
<LINK REL="up" HREF="cuddIntro.html">
<LINK REL="next" HREF="node6.html">
</HEAD>
<BODY >
<!--Navigation Panel-->
<A NAME="tex2html184"
HREF="node6.html">
<IMG WIDTH="37" HEIGHT="24" ALIGN="BOTTOM" BORDER="0" ALT="next"
SRC="icons/next.png"></A>
<A NAME="tex2html180"
HREF="cuddIntro.html">
<IMG WIDTH="26" HEIGHT="24" ALIGN="BOTTOM" BORDER="0" ALT="up"
SRC="icons/up.png"></A>
<A NAME="tex2html174"
HREF="node4.html">
<IMG WIDTH="63" HEIGHT="24" ALIGN="BOTTOM" BORDER="0" ALT="previous"
SRC="icons/prev.png"></A>
<A NAME="tex2html182"
HREF="node8.html">
<IMG WIDTH="43" HEIGHT="24" ALIGN="BOTTOM" BORDER="0" ALT="index"
SRC="icons/index.png"></A>
<BR>
<B> Next:</B> <A NAME="tex2html185"
HREF="node6.html">Acknowledgments</A>
<B> Up:</B> <A NAME="tex2html181"
HREF="cuddIntro.html">CUDD: CU Decision Diagram</A>
<B> Previous:</B> <A NAME="tex2html175"
HREF="node4.html">Programmer's Manual</A>
&nbsp; <B> <A NAME="tex2html183"
HREF="node8.html">Index</A></B>
<BR>
<BR>
<!--End of Navigation Panel-->
<!--Table of Child-Links-->
<A NAME="CHILD_LINKS"><STRONG>Subsections</STRONG></A>
<UL>
<LI><A NAME="tex2html186"
HREF="node5.html#SECTION00051000000000000000">Compiling and Linking</A>
<LI><A NAME="tex2html187"
HREF="node5.html#SECTION00052000000000000000">Basic Manipulation</A>
</UL>
<!--End of Table of Child-Links-->
<HR>
<H1><A NAME="SECTION00050000000000000000"></A>
<A NAME="sec:cpp"></A>
<BR>
The C++ Interface
</H1>
<P>
<H2><A NAME="SECTION00051000000000000000"></A>
<A NAME="sec:compileCpp"></A>
<BR>
Compiling and Linking
</H2>
<P>
To build an application that uses the CUDD C++ interface, you should
add
<PRE>
#include "cuddObj.hh"
</PRE>
to your source files. In addition to the normal CUDD libraries (see
Section&nbsp;<A HREF="node3.html#sec:compileExt">3.1</A>) you should link
<code>libobj.a</code><A NAME="1051"></A> to your executable. Refer to the
<TT>Makefile<A NAME="1052"></A></TT> in the top level directory of the
distribution for further details.
<P>
<H2><A NAME="SECTION00052000000000000000"></A>
<A NAME="sec:basicCpp"></A>
<BR>
Basic Manipulation
</H2>
<P>
The following fragment of code illustrates some simple operations on
BDDs using the C++ interface.
<PRE>
Cudd mgr(0,0);
BDD x = mgr.bddVar();
BDD y = mgr.bddVar();
BDD f = x * y;
BDD g = y + !x;
cout &lt;&lt; "f is" &lt;&lt; (f &lt;= g ? "" : " not")
&lt;&lt; " less than or equal to g\n";
</PRE>
This code creates a manager called <code>mgr</code> and two variables in it.
It then defines two functions <code>f</code> and <code>g</code> in terms of the
variables. Finally, it prints a message based on the comparison of the
two functions. No explicit referencing or dereferencing is required.
The operators are overloaded in the intuitive way. BDDs are freed when
execution leaves the scope in which they are defined or when the
variables referring to them are overwritten.
<P>
<BR><HR>
<ADDRESS>
Fabio Somenzi
2012-02-04
</ADDRESS>
</BODY>
</HTML>

132
resources/3rdparty/cudd-2.5.0/src/cudd/doc/node6.html

@ -1,132 +0,0 @@
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 3.2 Final//EN">
<!--Converted with LaTeX2HTML 2008 (1.71)
original version by: Nikos Drakos, CBLU, University of Leeds
* revised and updated by: Marcus Hennecke, Ross Moore, Herb Swan
* with significant contributions from:
Jens Lippmann, Marek Rouchal, Martin Wilck and others -->
<HTML>
<HEAD>
<TITLE>Acknowledgments</TITLE>
<META NAME="description" CONTENT="Acknowledgments">
<META NAME="keywords" CONTENT="cuddIntro">
<META NAME="resource-type" CONTENT="document">
<META NAME="distribution" CONTENT="global">
<META NAME="Generator" CONTENT="LaTeX2HTML v2008">
<META HTTP-EQUIV="Content-Style-Type" CONTENT="text/css">
<LINK REL="STYLESHEET" HREF="cuddIntro.css">
<LINK REL="next" HREF="node7.html">
<LINK REL="previous" HREF="node5.html">
<LINK REL="up" HREF="cuddIntro.html">
<LINK REL="next" HREF="node7.html">
</HEAD>
<BODY >
<!--Navigation Panel-->
<A NAME="tex2html198"
HREF="node7.html">
<IMG WIDTH="37" HEIGHT="24" ALIGN="BOTTOM" BORDER="0" ALT="next"
SRC="icons/next.png"></A>
<A NAME="tex2html194"
HREF="cuddIntro.html">
<IMG WIDTH="26" HEIGHT="24" ALIGN="BOTTOM" BORDER="0" ALT="up"
SRC="icons/up.png"></A>
<A NAME="tex2html188"
HREF="node5.html">
<IMG WIDTH="63" HEIGHT="24" ALIGN="BOTTOM" BORDER="0" ALT="previous"
SRC="icons/prev.png"></A>
<A NAME="tex2html196"
HREF="node8.html">
<IMG WIDTH="43" HEIGHT="24" ALIGN="BOTTOM" BORDER="0" ALT="index"
SRC="icons/index.png"></A>
<BR>
<B> Next:</B> <A NAME="tex2html199"
HREF="node7.html">Bibliography</A>
<B> Up:</B> <A NAME="tex2html195"
HREF="cuddIntro.html">CUDD: CU Decision Diagram</A>
<B> Previous:</B> <A NAME="tex2html189"
HREF="node5.html">The C++ Interface</A>
&nbsp; <B> <A NAME="tex2html197"
HREF="node8.html">Index</A></B>
<BR>
<BR>
<!--End of Navigation Panel-->
<H1><A NAME="SECTION00060000000000000000"></A>
<A NAME="sec:ack"></A>
<BR>
Acknowledgments
</H1>
<P>
The contributors: Iris Bahar, Hyunwoo Cho, Erica Frohm, Charlie Gaona,
Cheng Hua, Jae-Young Jang, Seh-Woong Jeong, Balakrishna Kumthekar,
Enrico Macii, Bobbie Manne, In-Ho Moon, Curt Musfeldt, Shipra Panda,
Abelardo Pardo, Bernard Plessier, Kavita Ravi, Hyongkyoon Shin, Alan
Shuler, Arun Sivakumaran, Jorgen Sivesind.
<P>
The early adopters: Gianpiero Cabodi, Jordi Cortadella, Mario Escobar,
Gayani Gamage, Gary Hachtel, Mariano Hermida, Woohyuk Lee, Enric
Pastor, Massimo Poncino, Ellen Sentovich, the students of ECEN5139.
<P>
I am also particularly indebted to the following people for in-depth
discussions on BDDs: Armin Biere, Olivier Coudert, Arie Gurfinkel,
Geert Janssen, Don Knuth, David Long, Jean Christophe Madre, Ken
McMillan, Shin-Ichi Minato, Jaehong Park, Rajeev Ranjan, Rick Rudell,
Ellen Sentovich, Tom Shiple, Christian Stangier, and Bwolen Yang.
<P>
Special thanks to Norris Ip for guiding my faltering steps
in the design of the C++ interface.
Gianpiero Cabodi and Stefano Quer have graciously agreed to let me
distribute their dddmp library with CUDD.
<P>
Masahiro Fujita, Gary Hachtel, and Carl Pixley have provided
encouragement and advice.
<P>
The National Science Foundation and the Semiconductor Research
Corporation have supported in part the development of this package.
<P>
<HR>
<!--Navigation Panel-->
<A NAME="tex2html198"
HREF="node7.html">
<IMG WIDTH="37" HEIGHT="24" ALIGN="BOTTOM" BORDER="0" ALT="next"
SRC="icons/next.png"></A>
<A NAME="tex2html194"
HREF="cuddIntro.html">
<IMG WIDTH="26" HEIGHT="24" ALIGN="BOTTOM" BORDER="0" ALT="up"
SRC="icons/up.png"></A>
<A NAME="tex2html188"
HREF="node5.html">
<IMG WIDTH="63" HEIGHT="24" ALIGN="BOTTOM" BORDER="0" ALT="previous"
SRC="icons/prev.png"></A>
<A NAME="tex2html196"
HREF="node8.html">
<IMG WIDTH="43" HEIGHT="24" ALIGN="BOTTOM" BORDER="0" ALT="index"
SRC="icons/index.png"></A>
<BR>
<B> Next:</B> <A NAME="tex2html199"
HREF="node7.html">Bibliography</A>
<B> Up:</B> <A NAME="tex2html195"
HREF="cuddIntro.html">CUDD: CU Decision Diagram</A>
<B> Previous:</B> <A NAME="tex2html189"
HREF="node5.html">The C++ Interface</A>
&nbsp; <B> <A NAME="tex2html197"
HREF="node8.html">Index</A></B>
<!--End of Navigation Panel-->
<ADDRESS>
Fabio Somenzi
2012-02-04
</ADDRESS>
</BODY>
</HTML>

195
resources/3rdparty/cudd-2.5.0/src/cudd/doc/node7.html

@ -1,195 +0,0 @@
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 3.2 Final//EN">
<!--Converted with LaTeX2HTML 2008 (1.71)
original version by: Nikos Drakos, CBLU, University of Leeds
* revised and updated by: Marcus Hennecke, Ross Moore, Herb Swan
* with significant contributions from:
Jens Lippmann, Marek Rouchal, Martin Wilck and others -->
<HTML>
<HEAD>
<TITLE>Bibliography</TITLE>
<META NAME="description" CONTENT="Bibliography">
<META NAME="keywords" CONTENT="cuddIntro">
<META NAME="resource-type" CONTENT="document">
<META NAME="distribution" CONTENT="global">
<META NAME="Generator" CONTENT="LaTeX2HTML v2008">
<META HTTP-EQUIV="Content-Style-Type" CONTENT="text/css">
<LINK REL="STYLESHEET" HREF="cuddIntro.css">
<LINK REL="next" HREF="node8.html">
<LINK REL="previous" HREF="node6.html">
<LINK REL="up" HREF="cuddIntro.html">
<LINK REL="next" HREF="node8.html">
</HEAD>
<BODY >
<!--Navigation Panel-->
<A NAME="tex2html210"
HREF="node8.html">
<IMG WIDTH="37" HEIGHT="24" ALIGN="BOTTOM" BORDER="0" ALT="next"
SRC="icons/next.png"></A>
<A NAME="tex2html206"
HREF="cuddIntro.html">
<IMG WIDTH="26" HEIGHT="24" ALIGN="BOTTOM" BORDER="0" ALT="up"
SRC="icons/up.png"></A>
<A NAME="tex2html200"
HREF="node6.html">
<IMG WIDTH="63" HEIGHT="24" ALIGN="BOTTOM" BORDER="0" ALT="previous"
SRC="icons/prev.png"></A>
<A NAME="tex2html208"
HREF="node8.html">
<IMG WIDTH="43" HEIGHT="24" ALIGN="BOTTOM" BORDER="0" ALT="index"
SRC="icons/index.png"></A>
<BR>
<B> Next:</B> <A NAME="tex2html211"
HREF="node8.html">Index</A>
<B> Up:</B> <A NAME="tex2html207"
HREF="cuddIntro.html">CUDD: CU Decision Diagram</A>
<B> Previous:</B> <A NAME="tex2html201"
HREF="node6.html">Acknowledgments</A>
&nbsp; <B> <A NAME="tex2html209"
HREF="node8.html">Index</A></B>
<BR><BR>
<!--End of Navigation Panel-->
<H2><A NAME="SECTION00070000000000000000">
Bibliography</A>
</H2><DL COMPACT><DD><P></P><DT><A NAME="Bahar93">1</A>
<DD>
R.&nbsp;I. Bahar, E.&nbsp;A. Frohm, C.&nbsp;M. Gaona, G.&nbsp;D. Hachtel, E.&nbsp;Macii, A.&nbsp;Pardo, and
F.&nbsp;Somenzi.
<BR>Algebraic decision diagrams and their applications.
<BR>In <EM>Proceedings of the International Conference on Computer-Aided
Design</EM>, pages 188-191, Santa Clara, CA, November 1993.
<P></P><DT><A NAME="Bollig95">2</A>
<DD>
B.&nbsp;Bollig, M.&nbsp;L&#246;bbing, and I.&nbsp;Wegener.
<BR>Simulated annealing to improve variable orderings for OBDDs.
<BR>Presented at the International Workshop on Logic Synthesis,
Granlibakken, CA, May 1995.
<P></P><DT><A NAME="BBR">3</A>
<DD>
K.&nbsp;S. Brace, R.&nbsp;L. Rudell, and R.&nbsp;E. Bryant.
<BR>Efficient implementation of a BDD package.
<BR>In <EM>Proceedings of the 27th Design Automation Conference</EM>, pages
40-45, Orlando, FL, June 1990.
<P></P><DT><A NAME="VIS">4</A>
<DD>
R.&nbsp;K. Brayton et&nbsp;al.
<BR>VIS: A system for verification and synthesis.
<BR>Technical Report UCB/ERL M95/104, Electronics Research Lab, Univ. of
California, December 1995.
<P></P><DT><A NAME="BDD">5</A>
<DD>
R.&nbsp;E. Bryant.
<BR>Graph-based algorithms for Boolean function manipulation.
<BR><EM>IEEE Transactions on Computers</EM>, C-35(8):677-691, August 1986.
<P></P><DT><A NAME="Drechs95">6</A>
<DD>
R.&nbsp;Drechsler, B.&nbsp;Becker, and N.&nbsp;G&#246;ckel.
<BR>A genetic algorithm for variable ordering of OBDDs.
<BR>Presented at the International Workshop on Logic Synthesis,
Granlibakken, CA, May 1995.
<P></P><DT><A NAME="Friedman90">7</A>
<DD>
S.&nbsp;J. Friedman and K.&nbsp;J. Supowit.
<BR>Finding the optimal variable ordering for binary decision diagrams.
<BR><EM>IEEE Transactions on Computers</EM>, 39(5):710-713, May 1990.
<P></P><DT><A NAME="Fujita91b">8</A>
<DD>
M.&nbsp;Fujita, Y.&nbsp;Matsunaga, and T.&nbsp;Kakuda.
<BR>On variable ordering of binary decision diagrams for the application
of multi-level logic synthesis.
<BR>In <EM>Proceedings of the European Conference on Design Automation</EM>,
pages 50-54, Amsterdam, February 1991.
<P></P><DT><A NAME="Held62">9</A>
<DD>
M.&nbsp;Held and R.&nbsp;M. Karp.
<BR>A dynamic programming approach to sequencing problems.
<BR><EM>J. SIAM</EM>, 10(1):196-210, 1962.
<P></P><DT><A NAME="Ishiur91">10</A>
<DD>
N.&nbsp;Ishiura, H.&nbsp;Sawada, and S.&nbsp;Yajima.
<BR>Minimization of binary decision diagrams based on exchanges of
variables.
<BR>In <EM>Proceedings of the International Conference on Computer-Aided
Design</EM>, pages 472-475, Santa Clara, CA, November 1991.
<P></P><DT><A NAME="Jeong93">11</A>
<DD>
S.-W. Jeong, T.-S. Kim, and F.&nbsp;Somenzi.
<BR>An efficient method for optimal BDD ordering computation.
<BR>In <EM>International Conference on VLSI and CAD (ICVC'93)</EM>, Taejon,
Korea, November 1993.
<P></P><DT><A NAME="Minato93">12</A>
<DD>
S.-I. Minato.
<BR>Zero-suppressed BDDs for set manipulation in combinatorial
problems.
<BR>In <EM>Proceedings of the Design Automation Conference</EM>, pages
272-277, Dallas, TX, June 1993.
<P></P><DT><A NAME="Panda95b">13</A>
<DD>
S.&nbsp;Panda and F.&nbsp;Somenzi.
<BR>Who are the variables in your neighborhood.
<BR>In <EM>Proceedings of the International Conference on Computer-Aided
Design</EM>, pages 74-77, San Jose, CA, November 1995.
<P></P><DT><A NAME="Panda94">14</A>
<DD>
S.&nbsp;Panda, F.&nbsp;Somenzi, and B.&nbsp;F. Plessier.
<BR>Symmetry detection and dynamic variable ordering of decision
diagrams.
<BR>In <EM>Proceedings of the International Conference on Computer-Aided
Design</EM>, pages 628-631, San Jose, CA, November 1994.
<P></P><DT><A NAME="Plessi93">15</A>
<DD>
B.&nbsp;F. Plessier.
<BR><EM>A General Framework for Verification of Sequential Circuits</EM>.
<BR>PhD thesis, University of Colorado at Boulder, Dept. of Electrical
and Computer Engineering, 1993.
<P></P><DT><A NAME="Rudell93">16</A>
<DD>
R.&nbsp;Rudell.
<BR>Dynamic variable ordering for ordered binary decision diagrams.
<BR>In <EM>Proceedings of the International Conference on Computer-Aided
Design</EM>, pages 42-47, Santa Clara, CA, November 1993.
<P></P><DT><A NAME="Sentov92">17</A>
<DD>
E.&nbsp;M. Sentovich, K.&nbsp;J. Singh, C.&nbsp;Moon, H.&nbsp;Savoj, R.&nbsp;K. Brayton, and
A.&nbsp;Sangiovanni-Vincentelli.
<BR>Sequential circuit design using synthesis and optimization.
<BR>In <EM>Proceedings of the International Conference on Computer
Design</EM>, pages 328-333, Cambridge, MA, October 1992.
</DL>
<A NAME="1101"></A>
<A NAME="1102"></A>
<A NAME="1103"></A>
<A NAME="1104"></A>
<A NAME="1105"></A>
<A NAME="1106"></A>
<P>
<BR><HR>
<ADDRESS>
Fabio Somenzi
2012-02-04
</ADDRESS>
</BODY>
</HTML>

848
resources/3rdparty/cudd-2.5.0/src/cudd/doc/node8.html

@ -1,848 +0,0 @@
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 3.2 Final//EN">
<!--Converted with LaTeX2HTML 2008 (1.71)
original version by: Nikos Drakos, CBLU, University of Leeds
* revised and updated by: Marcus Hennecke, Ross Moore, Herb Swan
* with significant contributions from:
Jens Lippmann, Marek Rouchal, Martin Wilck and others -->
<HTML>
<HEAD>
<TITLE>Index</TITLE>
<META NAME="description" CONTENT="Index">
<META NAME="keywords" CONTENT="cuddIntro">
<META NAME="resource-type" CONTENT="document">
<META NAME="distribution" CONTENT="global">
<META NAME="Generator" CONTENT="LaTeX2HTML v2008">
<META HTTP-EQUIV="Content-Style-Type" CONTENT="text/css">
<LINK REL="STYLESHEET" HREF="cuddIntro.css">
<LINK REL="previous" HREF="node7.html">
<LINK REL="up" HREF="cuddIntro.html">
</HEAD>
<BODY >
<!--Navigation Panel-->
<IMG WIDTH="37" HEIGHT="24" ALIGN="BOTTOM" BORDER="0" ALT="next"
SRC="icons/next_g.png">
<A NAME="tex2html216"
HREF="cuddIntro.html">
<IMG WIDTH="26" HEIGHT="24" ALIGN="BOTTOM" BORDER="0" ALT="up"
SRC="icons/up.png"></A>
<A NAME="tex2html212"
HREF="node7.html">
<IMG WIDTH="63" HEIGHT="24" ALIGN="BOTTOM" BORDER="0" ALT="previous"
SRC="icons/prev.png"></A>
<BR>
<B> Up:</B> <A NAME="tex2html217"
HREF="cuddIntro.html">CUDD: CU Decision Diagram</A>
<B> Previous:</B> <A NAME="tex2html213"
HREF="node7.html">Bibliography</A>
<BR>
<BR>
<!--End of Navigation Panel-->
<BR>
<H2><A NAME="SECTION00080000000000000000">
Index</A>
</H2><DL COMPACT>
<DT><STRONG>ADD</STRONG>
<DD><A HREF="node1.html#16">Introduction</A>
| <A HREF="node3.html#116">Nodes</A>
| <A HREF="node3.html#261">New Constants</A>
| <A HREF="node3.html#335">Basic ADD Manipulation</A>
<DT><STRONG>aggregation</STRONG>
<DD><A HREF="node3.html#473">Variable Reordering for BDDs</A>
<DT><STRONG>Algebraic Decision Diagram</STRONG>
<DD><i>see </i> ADD
<DT><STRONG>arc</STRONG>
<DD><DL COMPACT>
<DT><STRONG>complement</STRONG>
<DD><A HREF="node3.html#270">New BDD and ADD</A>
| <A HREF="node3.html#680">Writing Decision Diagrams to</A>
| <A HREF="node3.html#680">Writing Decision Diagrams to</A>
| <A HREF="node4.html#805">Complement Arcs</A>
| <A HREF="node4.html#809">Complement Arcs</A>
<DT><STRONG>regular</STRONG>
<DD><A HREF="node3.html#681">Writing Decision Diagrams to</A>
| <A HREF="node3.html#681">Writing Decision Diagrams to</A>
| <A HREF="node4.html#808">Complement Arcs</A>
</DL>
<DT><STRONG>background value</STRONG>
<DD><A HREF="node3.html#234">Background</A>
<DT><STRONG>BDD</STRONG>
<DD><A HREF="node1.html#14">Introduction</A>
| <A HREF="node3.html#115">Nodes</A>
| <A HREF="node3.html#200">One, Logic Zero, and</A>
| <A HREF="node3.html#302">Basic BDD Manipulation</A>
<DT><STRONG>Binary Decision Diagram</STRONG>
<DD><i>see </i> BDD
<DT><STRONG>box</STRONG>
<DD><DL COMPACT>
<DT><STRONG>black</STRONG>
<DD><A HREF="node1.html#27">Introduction</A>
<DT><STRONG>clear</STRONG>
<DD><A HREF="node1.html#32">Introduction</A>
| <A HREF="node4.html#704">Compiling and Linking</A>
</DL>
<DT><STRONG>cache</STRONG>
<DD><A HREF="node3.html#141">Cache</A>
| <A HREF="node3.html#144">Cache</A>
| <A HREF="node3.html#146">Cache</A>
| <A HREF="node3.html#163">Initializing and Shutting Down</A>
| <A HREF="node4.html#807">Complement Arcs</A>
| <A HREF="node4.html#817">The Cache</A>
<DL COMPACT>
<DT><STRONG>collision</STRONG>
<DD><A HREF="node4.html#962">Non Modifiable Parameters</A>
<DT><STRONG>collision list</STRONG>
<DD><A HREF="node4.html#877">The Unique Table</A>
<DT><STRONG>deletion</STRONG>
<DD><A HREF="node4.html#963">Non Modifiable Parameters</A>
<DT><STRONG>local</STRONG>
<DD><A HREF="node4.html#827">The Cache</A>
| <A HREF="node4.html#857">Local Caches</A>
<DT><STRONG>lossless</STRONG>
<DD><A HREF="node4.html#859">Local Caches</A>
<DT><STRONG>reward-based resizing</STRONG>
<DD><A HREF="node4.html#851">Cache Sizing</A>
| <A HREF="node4.html#854">Cache Sizing</A>
<DT><STRONG>sizing</STRONG>
<DD><A HREF="node4.html#846">Cache Sizing</A>
</DL>
<DT><STRONG>cacheSize</STRONG>
<DD><A HREF="node3.html#162">Initializing and Shutting Down</A>
<DT><STRONG>canonical</STRONG>
<DD><A HREF="node3.html#132">The Manager</A>
| <A HREF="node4.html#860">Local Caches</A>
<DT><STRONG>compiling</STRONG>
<DD><A HREF="node3.html#79">Compiling and Linking</A>
| <A HREF="node3.html#218">Predefined Constants</A>
| <A HREF="node4.html#702">Compiling and Linking</A>
<DT><STRONG>configuration</STRONG>
<DD><A HREF="node2.html#55">The CUDD Package</A>
<DT><STRONG>conversion</STRONG>
<DD><DL COMPACT>
<DT><STRONG>of ADDs to BDDs</STRONG>
<DD><A HREF="node3.html#377">Converting ADDs to BDDs</A>
<DT><STRONG>of BDDs to ADDs</STRONG>
<DD><A HREF="node3.html#378">Converting ADDs to BDDs</A>
<DT><STRONG>of BDDs to ZDDs</STRONG>
<DD><A HREF="node3.html#357">Basic ZDD Manipulation</A>
| <A HREF="node3.html#394">Converting BDDs to ZDDs</A>
<DT><STRONG>of ZDDs to BDDs</STRONG>
<DD><A HREF="node3.html#393">Converting BDDs to ZDDs</A>
</DL>
<DT><STRONG>cube sets</STRONG>
<DD><A HREF="node1.html#23">Introduction</A>
<DT><STRONG>cudd.h</STRONG>
<DD><A HREF="node3.html#82">Compiling and Linking</A>
| <A HREF="node3.html#437">Variable Reordering for BDDs</A>
| <A HREF="node4.html#797">Saturating Increments and Decrements</A>
<DT><STRONG><I>Cudd_addApply</I></STRONG>
<DD><A HREF="node3.html#1190">Basic ADD Manipulation</A>
| <A HREF="node3.html#1192">Basic ADD Manipulation</A>
<DT><STRONG><I>Cudd_addBddInterval</I></STRONG>
<DD><A HREF="node3.html#1208">Converting ADDs to BDDs</A>
<DT><STRONG><I>Cudd_addBddPattern</I></STRONG>
<DD><A HREF="node3.html#1206">Converting ADDs to BDDs</A>
<DT><STRONG><I>Cudd_addBddThreshold</I></STRONG>
<DD><A HREF="node3.html#1210">Converting ADDs to BDDs</A>
<DT><STRONG><I>Cudd_addConst</I></STRONG>
<DD><A HREF="node3.html#1160">New Constants</A>
<DT><STRONG><I>Cudd_addHarwell</I></STRONG>
<DD><A HREF="node3.html#1152">Background</A>
<DT><STRONG><I>Cudd_AddHook</I></STRONG>
<DD><A HREF="node3.html#1276">Hooks</A>
<DT><STRONG><I>Cudd_addIthBit</I></STRONG>
<DD><A HREF="node3.html#1214">Converting ADDs to BDDs</A>
<DT><STRONG><I>Cudd_addIthVar</I></STRONG>
<DD><A HREF="node3.html#1172">New BDD and ADD</A>
<DT><STRONG><I>Cudd_addNewVar</I></STRONG>
<DD><A HREF="node3.html#1174">New BDD and ADD</A>
<DT><STRONG><I>Cudd_addNewVarAtLevel</I></STRONG>
<DD><A HREF="node3.html#1176">New BDD and ADD</A>
| <A HREF="node3.html#1258">Grouping Variables</A>
<DT><STRONG><I>Cudd_addRead</I></STRONG>
<DD><A HREF="node3.html#1150">Background</A>
<DT><STRONG><I>Cudd_addTimes</I></STRONG>
<DD><A HREF="node3.html#1194">Basic ADD Manipulation</A>
<DT><STRONG><I>Cudd_AutodynDisable</I></STRONG>
<DD><A HREF="node3.html#1228">Variable Reordering for BDDs</A>
<DT><STRONG><I>Cudd_AutodynDisableZdd</I></STRONG>
<DD><A HREF="node3.html#1266">Variable Reordering for ZDDs</A>
<DT><STRONG><I>Cudd_AutodynEnable</I></STRONG>
<DD><A HREF="node3.html#1226">Variable Reordering for BDDs</A>
| <A HREF="node3.html#1232">Variable Reordering for BDDs</A>
<DT><STRONG><I>Cudd_AutodynEnableZdd</I></STRONG>
<DD><A HREF="node3.html#1264">Variable Reordering for ZDDs</A>
<DT><STRONG><I>Cudd_bddAnd</I></STRONG>
<DD><A HREF="node3.html#1182">Basic BDD Manipulation</A>
| <A HREF="node3.html#1186">Basic BDD Manipulation</A>
| <A HREF="node3.html#1196">Basic ADD Manipulation</A>
<DT><STRONG><I>Cudd_bddAndLimit</I></STRONG>
<DD><A HREF="node3.html#1284">Timeouts and Limits</A>
<DT><STRONG><I>Cudd_bddConstrain</I></STRONG>
<DD><A HREF="node3.html#1112">Nodes</A>
<DT><STRONG><I>Cudd_bddIte</I></STRONG>
<DD><A HREF="node3.html#1180">Basic BDD Manipulation</A>
<DT><STRONG><I>Cudd_bddIthVar</I></STRONG>
<DD><A HREF="node3.html#1162">New BDD and ADD</A>
<DT><STRONG><I>Cudd_bddNewVar</I></STRONG>
<DD><A HREF="node3.html#1164">New BDD and ADD</A>
| <A HREF="node3.html#1168">New BDD and ADD</A>
| <A HREF="node3.html#1170">New BDD and ADD</A>
<DT><STRONG><I>Cudd_bddNewVarAtLevel</I></STRONG>
<DD><A HREF="node3.html#1166">New BDD and ADD</A>
| <A HREF="node3.html#1256">Grouping Variables</A>
<DT><STRONG><I>Cudd_BddToAdd</I></STRONG>
<DD><A HREF="node3.html#1212">Converting ADDs to BDDs</A>
<DT><STRONG><I>Cudd_bddXor</I></STRONG>
<DD><A HREF="node3.html#1198">Basic ADD Manipulation</A>
<DT><STRONG>CUDD_CACHE_SLOTS</STRONG>
<DD><A HREF="node3.html#164">Initializing and Shutting Down</A>
<DT><STRONG><I>Cudd_CheckKeys</I></STRONG>
<DD><A HREF="node4.html#1384">Debugging</A>
<DT><STRONG><I>Cudd_CheckZeroRef</I></STRONG>
<DD><A HREF="node4.html#1390">Debugging</A>
<DT><STRONG><I>Cudd_CountMinterm</I></STRONG>
<DD><A HREF="node3.html#1158">Background</A>
<DT><STRONG><I>Cudd_DebugCheck</I></STRONG>
<DD><A HREF="node4.html#1382">Debugging</A>
<DT><STRONG><I>Cudd_DelayedDerefBdd</I></STRONG>
<DD><A HREF="node4.html#1394">Non Modifiable Parameters</A>
<DT><STRONG><I>Cudd_Deref</I></STRONG>
<DD><A HREF="node4.html#1330"><I>Cudd_RecursiveDeref</I> vs. <I>Cudd_Deref</I></A>
| <A HREF="node4.html#1342">Saturating Increments and Decrements</A>
<DT><STRONG><I>Cudd_DumpBlif</I></STRONG>
<DD><A HREF="node3.html#1286">Writing Decision Diagrams to</A>
<DT><STRONG><I>Cudd_DumpDaVinci</I></STRONG>
<DD><A HREF="node3.html#1292">Writing Decision Diagrams to</A>
<DT><STRONG><I>Cudd_DumpDot</I></STRONG>
<DD><A HREF="node3.html#1288">Writing Decision Diagrams to</A>
<DT><STRONG><I>Cudd_ForeachCube</I></STRONG>
<DD><A HREF="node3.html#1108">Nodes</A>
| <A HREF="node3.html#1156">Background</A>
<DT><STRONG><I>Cudd_ForeachNode</I></STRONG>
<DD><A HREF="node3.html#1110">Nodes</A>
<DT><STRONG><I>Cudd_HookType</I></STRONG>
<DD><A HREF="node3.html#1274">Hooks</A>
<DT><STRONG><I>Cudd_Init</I></STRONG>
<DD><A HREF="node3.html#1120">Initializing and Shutting Down</A>
| <A HREF="node3.html#1122">Initializing and Shutting Down</A>
<DT><STRONG><I>Cudd_MakeTreeNode</I></STRONG>
<DD><A HREF="node3.html#1248">Grouping Variables</A>
| <A HREF="node3.html#1254">Grouping Variables</A>
<DT><STRONG><I>Cudd_MakeZddTreeNode</I></STRONG>
<DD><A HREF="node3.html#1268">Variable Reordering for ZDDs</A>
<DT><STRONG><I>Cudd_Not</I></STRONG>
<DD><A HREF="node3.html#1134">One, Logic Zero, and</A>
<DT><STRONG><I>Cudd_PrintInfo</I></STRONG>
<DD><A HREF="node4.html#1392">Gathering and Interpreting Statistics</A>
<DT><STRONG><I>Cudd_PrintMinterm</I></STRONG>
<DD><A HREF="node3.html#1154">Background</A>
<DT><STRONG><I>Cudd_Quit</I></STRONG>
<DD><A HREF="node3.html#1124">Initializing and Shutting Down</A>
<DT><STRONG><I>Cudd_ReadBackground</I></STRONG>
<DD><A HREF="node3.html#1148">Background</A>
<DT><STRONG><I>Cudd_ReadEpsilon</I></STRONG>
<DD><A HREF="node3.html#1144">Predefined Constants</A>
<DT><STRONG><I>Cudd_ReadErrorCode</I></STRONG>
<DD><A HREF="node4.html#1326">NULL Return Values</A>
<DT><STRONG><I>Cudd_ReadInvPerm</I></STRONG>
<DD><A HREF="node3.html#1188">Basic BDD Manipulation</A>
<DT><STRONG><I>Cudd_ReadLogicZero</I></STRONG>
<DD><A HREF="node3.html#1136">One, Logic Zero, and</A>
<DT><STRONG><I>Cudd_ReadLooseUpto</I></STRONG>
<DD><A HREF="node3.html#1126">Setting Parameters</A>
<DT><STRONG><I>Cudd_ReadMaxGrowth</I></STRONG>
<DD><A HREF="node3.html#1240">Variable Reordering for BDDs</A>
<DT><STRONG><I>Cudd_ReadMinusInfinity</I></STRONG>
<DD><A HREF="node3.html#1142">Predefined Constants</A>
<DT><STRONG><I>Cudd_ReadOne</I></STRONG>
<DD><A HREF="node3.html#1130">One, Logic Zero, and</A>
<DT><STRONG><I>Cudd_ReadPlusInfinity</I></STRONG>
<DD><A HREF="node3.html#1140">Predefined Constants</A>
<DT><STRONG><I>Cudd_ReadReorderings</I></STRONG>
<DD><A HREF="node4.html#1378">Allowing Asynchronous Reordering</A>
<DT><STRONG><I>Cudd_ReadSiftMaxVar</I></STRONG>
<DD><A HREF="node3.html#1236">Variable Reordering for BDDs</A>
<DT><STRONG><I>Cudd_ReadTree</I></STRONG>
<DD><A HREF="node3.html#1252">Grouping Variables</A>
<DT><STRONG><I>Cudd_ReadZddOne</I></STRONG>
<DD><A HREF="node3.html#1132">One, Logic Zero, and</A>
| <A HREF="node3.html#1200">Basic ZDD Manipulation</A>
<DT><STRONG><I>Cudd_ReadZero</I></STRONG>
<DD><A HREF="node3.html#1138">Predefined Constants</A>
<DT><STRONG><I>Cudd_RecursiveDeref</I></STRONG>
<DD><A HREF="node3.html#1116">Nodes</A>
| <A HREF="node4.html#1308">Reference Counts</A>
| <A HREF="node4.html#1312">Reference Counts</A>
| <A HREF="node4.html#1322">Reference Counts</A>
| <A HREF="node4.html#1328"><I>Cudd_RecursiveDeref</I> vs. <I>Cudd_Deref</I></A>
| <A HREF="node4.html#1334">When Increasing the Reference</A>
| <A HREF="node4.html#1338">Saturating Increments and Decrements</A>
| <A HREF="node4.html#1366">Local Caches</A>
| <A HREF="node4.html#1388">Debugging</A>
<DT><STRONG><I>Cudd_RecursiveDerefZdd</I></STRONG>
<DD><A HREF="node3.html#1118">Nodes</A>
| <A HREF="node4.html#1310">Reference Counts</A>
| <A HREF="node4.html#1314">Reference Counts</A>
| <A HREF="node4.html#1324">Reference Counts</A>
| <A HREF="node4.html#1336">When Increasing the Reference</A>
| <A HREF="node4.html#1340">Saturating Increments and Decrements</A>
<DT><STRONG><I>Cudd_ReduceHeap</I></STRONG>
<DD><A HREF="node3.html#1224">Variable Reordering for BDDs</A>
| <A HREF="node3.html#1230">Variable Reordering for BDDs</A>
| <A HREF="node3.html#1234">Variable Reordering for BDDs</A>
<DT><STRONG><I>Cudd_Ref</I></STRONG>
<DD><A HREF="node3.html#1114">Nodes</A>
| <A HREF="node3.html#1184">Basic BDD Manipulation</A>
| <A HREF="node4.html#1306">Reference Counts</A>
| <A HREF="node4.html#1332">When Increasing the Reference</A>
<DT><STRONG><I>Cudd_Regular</I></STRONG>
<DD><A HREF="node4.html#1348">Complement Arcs</A>
<DT><STRONG>CUDD_REORDER_ANNEALING</STRONG>
<DD><A HREF="node3.html#485">Variable Reordering for BDDs</A>
<DT><STRONG>CUDD_REORDER_EXACT</STRONG>
<DD><A HREF="node3.html#491">Variable Reordering for BDDs</A>
<DT><STRONG>CUDD_REORDER_GENETIC</STRONG>
<DD><A HREF="node3.html#488">Variable Reordering for BDDs</A>
<DT><STRONG>CUDD_REORDER_GROUP_SIFT</STRONG>
<DD><A HREF="node3.html#470">Variable Reordering for BDDs</A>
<DT><STRONG>CUDD_REORDER_GROUP_SIFT_CONV</STRONG>
<DD><A HREF="node3.html#474">Variable Reordering for BDDs</A>
<DT><STRONG>CUDD_REORDER_NONE</STRONG>
<DD><A HREF="node3.html#440">Variable Reordering for BDDs</A>
| <A HREF="node3.html#544">Variable Reordering for ZDDs</A>
<DT><STRONG>CUDD_REORDER_RANDOM</STRONG>
<DD><A HREF="node3.html#446">Variable Reordering for BDDs</A>
| <A HREF="node3.html#546">Variable Reordering for ZDDs</A>
<DT><STRONG>CUDD_REORDER_RANDOM_PIVOT</STRONG>
<DD><A HREF="node3.html#448">Variable Reordering for BDDs</A>
| <A HREF="node3.html#547">Variable Reordering for ZDDs</A>
<DT><STRONG>CUDD_REORDER_SAME</STRONG>
<DD><A HREF="node3.html#441">Variable Reordering for BDDs</A>
| <A HREF="node3.html#545">Variable Reordering for ZDDs</A>
<DT><STRONG>CUDD_REORDER_SIFT</STRONG>
<DD><A HREF="node3.html#449">Variable Reordering for BDDs</A>
| <A HREF="node3.html#548">Variable Reordering for ZDDs</A>
<DT><STRONG>CUDD_REORDER_SIFT_CONVERGE</STRONG>
<DD><A HREF="node3.html#460">Variable Reordering for BDDs</A>
| <A HREF="node3.html#549">Variable Reordering for ZDDs</A>
<DT><STRONG>CUDD_REORDER_SYMM_SIFT</STRONG>
<DD><A HREF="node3.html#462">Variable Reordering for BDDs</A>
| <A HREF="node3.html#550">Variable Reordering for ZDDs</A>
<DT><STRONG>CUDD_REORDER_SYMM_SIFT_CONV</STRONG>
<DD><A HREF="node3.html#468">Variable Reordering for BDDs</A>
| <A HREF="node3.html#551">Variable Reordering for ZDDs</A>
<DT><STRONG>CUDD_REORDER_WINDOW2</STRONG>
<DD><A HREF="node3.html#475">Variable Reordering for BDDs</A>
<DT><STRONG>CUDD_REORDER_WINDOW2_CONV</STRONG>
<DD><A HREF="node3.html#481">Variable Reordering for BDDs</A>
<DT><STRONG>CUDD_REORDER_WINDOW3</STRONG>
<DD><A HREF="node3.html#479">Variable Reordering for BDDs</A>
<DT><STRONG>CUDD_REORDER_WINDOW3_CONV</STRONG>
<DD><A HREF="node3.html#483">Variable Reordering for BDDs</A>
<DT><STRONG>CUDD_REORDER_WINDOW4</STRONG>
<DD><A HREF="node3.html#480">Variable Reordering for BDDs</A>
<DT><STRONG>CUDD_REORDER_WINDOW4_CONV</STRONG>
<DD><A HREF="node3.html#484">Variable Reordering for BDDs</A>
<DT><STRONG><I>Cudd_SetEpsilon</I></STRONG>
<DD><A HREF="node3.html#1146">Predefined Constants</A>
<DT><STRONG><I>Cudd_SetLooseUpTo</I></STRONG>
<DD><A HREF="node3.html#1128">Setting Parameters</A>
<DT><STRONG><I>Cudd_SetMaxCacheHard</I></STRONG>
<DD><A HREF="node4.html#1396">Modifiable Parameters</A>
<DT><STRONG><I>Cudd_SetMaxGrowth</I></STRONG>
<DD><A HREF="node3.html#1242">Variable Reordering for BDDs</A>
<DT><STRONG><I>Cudd_SetSiftMaxVar</I></STRONG>
<DD><A HREF="node3.html#1238">Variable Reordering for BDDs</A>
<DT><STRONG><I>Cudd_SetTimeLimit</I></STRONG>
<DD><A HREF="node3.html#1282">Timeouts and Limits</A>
<DT><STRONG><I>Cudd_SetTree</I></STRONG>
<DD><A HREF="node3.html#1250">Grouping Variables</A>
<DT><STRONG><I>Cudd_ShuffleHeap</I></STRONG>
<DD><A HREF="node3.html#1246">Variable Reordering for BDDs</A>
<DT><STRONG><I>Cudd_StdPostReordHook</I></STRONG>
<DD><A HREF="node3.html#1280">Hooks</A>
<DT><STRONG><I>Cudd_StdPreReordHook</I></STRONG>
<DD><A HREF="node3.html#1278">Hooks</A>
<DT><STRONG><I>Cudd_SymmProfile</I></STRONG>
<DD><A HREF="node3.html#1244">Variable Reordering for BDDs</A>
<DT><STRONG>CUDD_UNIQUE_SLOTS</STRONG>
<DD><A HREF="node3.html#161">Initializing and Shutting Down</A>
<DT><STRONG><I>Cudd_zddDumpDot</I></STRONG>
<DD><A HREF="node3.html#1290">Writing Decision Diagrams to</A>
<DT><STRONG><I>Cudd_zddIsop</I></STRONG>
<DD><A HREF="node3.html#1202">Basic ZDD Manipulation</A>
<DT><STRONG><I>Cudd_zddIthVar</I></STRONG>
<DD><A HREF="node3.html#1178">New ZDD Variables</A>
<DT><STRONG><I>Cudd_zddPortFromBdd</I></STRONG>
<DD><A HREF="node3.html#1218">Converting BDDs to ZDDs</A>
<DT><STRONG><I>Cudd_zddPortToBdd</I></STRONG>
<DD><A HREF="node3.html#1220">Converting BDDs to ZDDs</A>
<DT><STRONG><I>Cudd_zddRealignDisable</I></STRONG>
<DD><A HREF="node3.html#1272">Keeping Consistent Variable Orders</A>
<DT><STRONG><I>Cudd_zddRealignEnable</I></STRONG>
<DD><A HREF="node3.html#1270">Keeping Consistent Variable Orders</A>
<DT><STRONG><I>Cudd_zddReduceHeap</I></STRONG>
<DD><A HREF="node3.html#1260">Variable Reordering for ZDDs</A>
<DT><STRONG><I>Cudd_zddShuffleHeap</I></STRONG>
<DD><A HREF="node3.html#1262">Variable Reordering for ZDDs</A>
<DT><STRONG><I>Cudd_zddVarsFromBddVars</I></STRONG>
<DD><A HREF="node3.html#1216">Converting BDDs to ZDDs</A>
| <A HREF="node3.html#1222">Converting BDDs to ZDDs</A>
<DT><STRONG><I>Cudd_zddWeakDiv</I></STRONG>
<DD><A HREF="node3.html#1204">Basic ZDD Manipulation</A>
<DT><STRONG><I>cuddCacheInsert</I></STRONG>
<DD><A HREF="node4.html#1354">The Cache</A>
<DT><STRONG><I>cuddCacheInsert1</I></STRONG>
<DD><A HREF="node4.html#1362">The Cache</A>
<DT><STRONG><I>cuddCacheInsert2</I></STRONG>
<DD><A HREF="node4.html#1358">The Cache</A>
<DT><STRONG><I>cuddCacheLookup</I></STRONG>
<DD><A HREF="node4.html#1356">The Cache</A>
<DT><STRONG><I>cuddCacheLookup1</I></STRONG>
<DD><A HREF="node4.html#1364">The Cache</A>
<DT><STRONG><I>cuddCacheLookup2</I></STRONG>
<DD><A HREF="node4.html#1360">The Cache</A>
<DT><STRONG>CUDDDIR</STRONG>
<DD><A HREF="node3.html#595">Using the CUDD Package</A>
<DT><STRONG><I>cuddHeapProfile</I></STRONG>
<DD><A HREF="node4.html#1386">Debugging</A>
<DT><STRONG><I>cuddI</I></STRONG>
<DD><A HREF="node4.html#1368">The Unique Table</A>
<DT><STRONG>cuddInt.h</STRONG>
<DD><A HREF="node4.html#927">Debugging</A>
<DT><STRONG><I>cuddIZ</I></STRONG>
<DD><A HREF="node4.html#1370">The Unique Table</A>
<DT><STRONG><I>cuddSatDec</I></STRONG>
<DD><A HREF="node4.html#1346">Saturating Increments and Decrements</A>
<DT><STRONG><I>cuddSatInc</I></STRONG>
<DD><A HREF="node4.html#1344">Saturating Increments and Decrements</A>
<DT><STRONG><I>cuddUniqueConst</I></STRONG>
<DD><A HREF="node4.html#1298">Reference Counts</A>
| <A HREF="node4.html#1304">Reference Counts</A>
| <A HREF="node4.html#1320">Reference Counts</A>
<DT><STRONG><I>cuddUniqueInter</I></STRONG>
<DD><A HREF="node4.html#1294">Reference Counts</A>
| <A HREF="node4.html#1300">Reference Counts</A>
| <A HREF="node4.html#1316">Reference Counts</A>
| <A HREF="node4.html#1350">Complement Arcs</A>
| <A HREF="node4.html#1352">Complement Arcs</A>
| <A HREF="node4.html#1372">Allowing Asynchronous Reordering</A>
| <A HREF="node4.html#1376">Allowing Asynchronous Reordering</A>
| <A HREF="node4.html#1380">Allowing Asynchronous Reordering</A>
<DT><STRONG><I>cuddUniqueInterZdd</I></STRONG>
<DD><A HREF="node4.html#1296">Reference Counts</A>
| <A HREF="node4.html#1302">Reference Counts</A>
| <A HREF="node4.html#1318">Reference Counts</A>
| <A HREF="node4.html#1374">Allowing Asynchronous Reordering</A>
<DT><STRONG>DD_CACHE_PROFILE</STRONG>
<DD><A HREF="node4.html#1019">Extended Statistics and Reporting</A>
<DT><STRONG>DD_DEBUG</STRONG>
<DD><A HREF="node4.html#918">Debugging</A>
<DT><STRONG>DD_STATS</STRONG>
<DD><A HREF="node4.html#1018">Extended Statistics and Reporting</A>
<DT><STRONG>DD_UNIQUE_PROFILE</STRONG>
<DD><A HREF="node4.html#1020">Extended Statistics and Reporting</A>
<DT><STRONG>DD_VERBOSE</STRONG>
<DD><A HREF="node4.html#1021">Extended Statistics and Reporting</A>
<DT><STRONG>DdManager</STRONG>
<DD><A HREF="node3.html#134">The Manager</A>
| <A HREF="node3.html#149">Initializing and Shutting Down</A>
<DT><STRONG>DdNode</STRONG>
<DD><A HREF="node3.html#92">Nodes</A>
| <A HREF="node4.html#825">The Cache</A>
<DT><STRONG>debugging</STRONG>
<DD><A HREF="node4.html#916">Debugging</A>
<DT><STRONG>DEC Alpha</STRONG>
<DD><A HREF="node3.html#217">Predefined Constants</A>
| <A HREF="node3.html#662">Using the CUDD Package</A>
<DT><STRONG>documentation</STRONG>
<DD><A HREF="node4.html#1025">Guidelines for Documentation</A>
<DL COMPACT>
<DT><STRONG><I>Description</I></STRONG>
<DD><A HREF="node4.html#1097">Guidelines for Documentation</A>
<DT><STRONG>HTML files</STRONG>
<DD><A HREF="node4.html#1041">Guidelines for Documentation</A>
<DT><STRONG><I>SeeAlso</I></STRONG>
<DD><A HREF="node4.html#1096">Guidelines for Documentation</A>
<DT><STRONG><I>Synopsis</I></STRONG>
<DD><A HREF="node4.html#1098">Guidelines for Documentation</A>
</DL>
<DT><STRONG>dot</STRONG>
<DD><i>see </i> graph, drawing
<DT><STRONG>Epsilon</STRONG>
<DD><A HREF="node3.html#226">Predefined Constants</A>
<DT><STRONG>extdoc</STRONG>
<DD><i>see </i> documentation
<DT><STRONG>floating point</STRONG>
<DD><A HREF="node3.html#215">Predefined Constants</A>
<DL COMPACT>
<DT><STRONG>double (C type)</STRONG>
<DD><A HREF="node3.html#126">Nodes</A>
<DT><STRONG>IEEE Standard 754</STRONG>
<DD><A HREF="node3.html#214">Predefined Constants</A>
</DL>
<DT><STRONG>free list</STRONG>
<DD><A HREF="node4.html#743">Reference Counts</A>
<DT><STRONG>FTP</STRONG>
<DD><A HREF="node2.html#46">The CUDD Package</A>
| <A HREF="node2.html#68">CUDD Friends</A>
| <A HREF="node3.html#657">Using the CUDD Package</A>
| <A HREF="node4.html#1026">Guidelines for Documentation</A>
<DT><STRONG>function</STRONG>
<DD><DL COMPACT>
<DT><STRONG>characteristic</STRONG>
<DD><A HREF="node1.html#22">Introduction</A>
| <A HREF="node3.html#413">Converting BDDs to ZDDs</A>
<DT><STRONG>cover</STRONG>
<DD><A HREF="node3.html#367">Basic ZDD Manipulation</A>
| <A HREF="node3.html#406">Converting BDDs to ZDDs</A>
| <A HREF="node3.html#412">Converting BDDs to ZDDs</A>
<DD><DL COMPACT>
<DT><STRONG>irredundant</STRONG>
<DD><A HREF="node3.html#370">Basic ZDD Manipulation</A>
</DL>
<DT><STRONG>minterms</STRONG>
<DD><A HREF="node3.html#253">Background</A>
| <A HREF="node4.html#894">Allowing Asynchronous Reordering</A>
<DT><STRONG>ON-set</STRONG>
<DD><A HREF="node1.html#24">Introduction</A>
<DT><STRONG>sum of products</STRONG>
<DD><A HREF="node3.html#248">Background</A>
<DT><STRONG>switching</STRONG>
<DD><A HREF="node1.html#20">Introduction</A>
| <A HREF="node1.html#21">Introduction</A>
</DL>
<DT><STRONG>garbage collection</STRONG>
<DD><A HREF="node3.html#113">Nodes</A>
| <A HREF="node3.html#145">Cache</A>
| <A HREF="node3.html#180">Setting Parameters</A>
| <A HREF="node4.html#711">Reference Counts</A>
| <A HREF="node4.html#742">Reference Counts</A>
| <A HREF="node4.html#822">The Cache</A>
| <A HREF="node4.html#861">Local Caches</A>
| <A HREF="node4.html#879">The Unique Table</A>
<DL COMPACT>
<DT><STRONG>hooks</STRONG>
<DD><A HREF="node3.html#568">Hooks</A>
</DL>
<DT><STRONG>gcc</STRONG>
<DD><A HREF="node3.html#219">Predefined Constants</A>
<DT><STRONG>generator</STRONG>
<DD><A HREF="node3.html#104">Nodes</A>
<DT><STRONG>global variables</STRONG>
<DD><A HREF="node3.html#138">The Manager</A>
<DT><STRONG>graph</STRONG>
<DD><DL COMPACT>
<DT><STRONG>arc capacity</STRONG>
<DD><A HREF="node3.html#239">Background</A>
<DT><STRONG>arc length</STRONG>
<DD><A HREF="node3.html#237">Background</A>
<DT><STRONG>drawing</STRONG>
<DD><A HREF="node3.html#673">Writing Decision Diagrams to</A>
| <A HREF="node3.html#689">Writing Decision Diagrams to</A>
</DL>
<DT><STRONG>growth</STRONG>
<DD><A HREF="node3.html#181">Setting Parameters</A>
<DT><STRONG>gzip</STRONG>
<DD><A HREF="node2.html#50">The CUDD Package</A>
<DT><STRONG>HAVE_IEEE_754</STRONG>
<DD><A HREF="node3.html#220">Predefined Constants</A>
<DT><STRONG>header files</STRONG>
<DD><A HREF="node3.html#438">Variable Reordering for BDDs</A>
| <A HREF="node4.html#795">Saturating Increments and Decrements</A>
<DT><STRONG>hook</STRONG>
<DD><A HREF="node3.html#562">Hooks</A>
<DT><STRONG>infinities</STRONG>
<DD><A HREF="node3.html#216">Predefined Constants</A>
<DT><STRONG>installation</STRONG>
<DD><A HREF="node2.html#56">The CUDD Package</A>
<DT><STRONG>Intel Pentium 4</STRONG>
<DD><A HREF="node2.html#61">The CUDD Package</A>
<DT><STRONG>interface</STRONG>
<DD><DL COMPACT>
<DT><STRONG>cache</STRONG>
<DD><A HREF="node4.html#832">The Cache</A>
<DT><STRONG>SIS</STRONG>
<DD><A HREF="node3.html#584">The SIS/VIS Interface</A>
| <A HREF="node3.html#592">Using the CUDD Package</A>
<DT><STRONG>VIS</STRONG>
<DD><A HREF="node3.html#585">The SIS/VIS Interface</A>
</DL>
<DT><STRONG>libraries</STRONG>
<DD><A HREF="node2.html#53">The CUDD Package</A>
<DL COMPACT>
<DT><STRONG>cudd</STRONG>
<DD><A HREF="node3.html#83">Compiling and Linking</A>
<DT><STRONG>dddmp</STRONG>
<DD><A HREF="node3.html#698">Saving and Restoring BDDs</A>
<DT><STRONG>mtr</STRONG>
<DD><A HREF="node3.html#84">Compiling and Linking</A>
| <A HREF="node3.html#505">Grouping Variables</A>
<DT><STRONG>obj</STRONG>
<DD><A HREF="node5.html#1051">Compiling and Linking</A>
<DT><STRONG>st</STRONG>
<DD><A HREF="node3.html#85">Compiling and Linking</A>
| <A HREF="node4.html#829">The Cache</A>
<DT><STRONG>util</STRONG>
<DD><A HREF="node3.html#86">Compiling and Linking</A>
</DL>
<DT><STRONG>Makefile</STRONG>
<DD><A HREF="node3.html#87">Compiling and Linking</A>
| <A HREF="node3.html#221">Predefined Constants</A>
| <A HREF="node5.html#1052">Compiling and Linking</A>
<DT><STRONG>manager</STRONG>
<DD><A HREF="node3.html#128">The Manager</A>
| <A HREF="node3.html#135">The Manager</A>
| <A HREF="node3.html#190">Constant Functions</A>
<DT><STRONG>matrix</STRONG>
<DD><DL COMPACT>
<DT><STRONG>sparse</STRONG>
<DD><A HREF="node3.html#240">Background</A>
</DL>
<DT><STRONG>maxCache</STRONG>
<DD><A HREF="node4.html#849">Cache Sizing</A>
<DT><STRONG>maxMemory</STRONG>
<DD><A HREF="node3.html#165">Initializing and Shutting Down</A>
<DT><STRONG>MinusInfinity</STRONG>
<DD><A HREF="node3.html#213">Predefined Constants</A>
<DT><STRONG>MTR_DEFAULT</STRONG>
<DD><A HREF="node3.html#520">Grouping Variables</A>
<DT><STRONG>MTR_FIXED</STRONG>
<DD><A HREF="node3.html#515">Grouping Variables</A>
<DT><STRONG>nanotrav</STRONG>
<DD><A HREF="node2.html#59">The CUDD Package</A>
| <A HREF="node2.html#63">The CUDD Package</A>
<DT><STRONG>node</STRONG>
<DD><A HREF="node3.html#93">Nodes</A>
<DL COMPACT>
<DT><STRONG>constant</STRONG>
<DD><A HREF="node3.html#100">Nodes</A>
| <A HREF="node3.html#188">Constant Functions</A>
| <A HREF="node3.html#195">One, Logic Zero, and</A>
| <A HREF="node3.html#210">Predefined Constants</A>
| <A HREF="node3.html#236">Background</A>
| <A HREF="node3.html#258">New Constants</A>
| <A HREF="node4.html#716">Reference Counts</A>
| <A HREF="node4.html#772">When Increasing the Reference</A>
<DD><DL COMPACT>
<DT><STRONG>value</STRONG>
<DD><A HREF="node3.html#125">Nodes</A>
</DL>
<DT><STRONG>dead</STRONG>
<DD><A HREF="node4.html#733">Reference Counts</A>
| <A HREF="node4.html#823">The Cache</A>
| <A HREF="node4.html#878">The Unique Table</A>
<DT><STRONG>dereference</STRONG>
<DD><A HREF="node3.html#344">Basic ADD Manipulation</A>
<DT><STRONG>reclaimed</STRONG>
<DD><A HREF="node4.html#882">The Unique Table</A>
<DT><STRONG>recycling</STRONG>
<DD><A HREF="node3.html#124">Nodes</A>
<DT><STRONG>reference</STRONG>
<DD><A HREF="node3.html#343">Basic ADD Manipulation</A>
<DT><STRONG>reference count</STRONG>
<DD><A HREF="node3.html#95">Nodes</A>
| <A HREF="node3.html#114">Nodes</A>
| <A HREF="node3.html#315">Basic BDD Manipulation</A>
| <A HREF="node3.html#327">Basic BDD Manipulation</A>
| <A HREF="node4.html#709">Reference Counts</A>
| <A HREF="node4.html#731">Reference Counts</A>
| <A HREF="node4.html#744">Reference Counts</A>
| <A HREF="node4.html#770">When Increasing the Reference</A>
| <A HREF="node4.html#784">Saturating Increments and Decrements</A>
| <A HREF="node4.html#821">The Cache</A>
| <A HREF="node4.html#862">Local Caches</A>
| <A HREF="node4.html#937">Debugging</A>
<DD><DL COMPACT>
<DT><STRONG>saturated</STRONG>
<DD><A HREF="node4.html#939">Debugging</A>
</DL>
<DT><STRONG>terminal</STRONG>
<DD><i>see </i> node, constant
<DT><STRONG>variable index</STRONG>
<DD><A HREF="node3.html#94">Nodes</A>
</DL>
<DT><STRONG>numSlots</STRONG>
<DD><A HREF="node3.html#158">Initializing and Shutting Down</A>
<DT><STRONG>numVars</STRONG>
<DD><A HREF="node3.html#154">Initializing and Shutting Down</A>
<DT><STRONG>numVarsZ</STRONG>
<DD><A HREF="node3.html#155">Initializing and Shutting Down</A>
<DT><STRONG>PlusInfinity</STRONG>
<DD><A HREF="node3.html#212">Predefined Constants</A>
| <A HREF="node3.html#238">Background</A>
<DT><STRONG>projection functions</STRONG>
<DD><A HREF="node3.html#265">Creating Variables</A>
| <A HREF="node3.html#268">New BDD and ADD</A>
| <A HREF="node3.html#276">New BDD and ADD</A>
| <A HREF="node3.html#279">New BDD and ADD</A>
| <A HREF="node3.html#297">New ZDD Variables</A>
| <A HREF="node3.html#314">Basic BDD Manipulation</A>
| <A HREF="node3.html#342">Basic ADD Manipulation</A>
| <A HREF="node3.html#359">Basic ZDD Manipulation</A>
| <A HREF="node3.html#363">Basic ZDD Manipulation</A>
| <A HREF="node4.html#938">Debugging</A>
<DT><STRONG>README file</STRONG>
<DD><A HREF="node2.html#64">The CUDD Package</A>
| <A HREF="node2.html#54">The CUDD Package</A>
<DT><STRONG>reordering</STRONG>
<DD><A HREF="node1.html#25">Introduction</A>
| <A HREF="node1.html#29">Introduction</A>
| <A HREF="node3.html#102">Nodes</A>
| <A HREF="node4.html#824">The Cache</A>
<DL COMPACT>
<DT><STRONG>abort and retry</STRONG>
<DD><A HREF="node4.html#896">Allowing Asynchronous Reordering</A>
<DT><STRONG>asynchronous</STRONG>
<DD><A HREF="node3.html#425">Variable Reordering for BDDs</A>
| <A HREF="node4.html#891">Allowing Asynchronous Reordering</A>
<DT><STRONG>converging</STRONG>
<DD><A HREF="node3.html#432">Variable Reordering for BDDs</A>
| <A HREF="node3.html#461">Variable Reordering for BDDs</A>
| <A HREF="node3.html#469">Variable Reordering for BDDs</A>
| <A HREF="node3.html#482">Variable Reordering for BDDs</A>
<DT><STRONG>Cudd_ReorderingType</STRONG>
<DD><A HREF="node3.html#436">Variable Reordering for BDDs</A>
<DT><STRONG>dynamic</STRONG>
<DD><A HREF="node1.html#34">Introduction</A>
| <A HREF="node3.html#417">Variable Reordering for BDDs</A>
| <A HREF="node3.html#538">Variable Reordering for ZDDs</A>
<DT><STRONG>exact</STRONG>
<DD><A HREF="node3.html#492">Variable Reordering for BDDs</A>
<DT><STRONG>function wrapper</STRONG>
<DD><A HREF="node4.html#898">Allowing Asynchronous Reordering</A>
| <A HREF="node4.html#913">Allowing Asynchronous Reordering</A>
<DT><STRONG>genetic</STRONG>
<DD><A HREF="node3.html#489">Variable Reordering for BDDs</A>
<DT><STRONG>group</STRONG>
<DD><A HREF="node3.html#434">Variable Reordering for BDDs</A>
| <A HREF="node3.html#471">Variable Reordering for BDDs</A>
<DT><STRONG>hooks</STRONG>
<DD><A HREF="node3.html#569">Hooks</A>
<DT><STRONG>interruptible procedure</STRONG>
<DD><A HREF="node4.html#897">Allowing Asynchronous Reordering</A>
<DT><STRONG>of BDDs and ADDs</STRONG>
<DD><A HREF="node3.html#415">Variable Reordering for BDDs</A>
<DT><STRONG>of ZDDs</STRONG>
<DD><A HREF="node3.html#374">Basic ZDD Manipulation</A>
| <A HREF="node3.html#530">Variable Reordering for ZDDs</A>
<DT><STRONG>random</STRONG>
<DD><A HREF="node3.html#447">Variable Reordering for BDDs</A>
<DT><STRONG>sifting</STRONG>
<DD><A HREF="node3.html#435">Variable Reordering for BDDs</A>
| <A HREF="node3.html#450">Variable Reordering for BDDs</A>
<DT><STRONG>simulated annealing</STRONG>
<DD><A HREF="node3.html#486">Variable Reordering for BDDs</A>
<DT><STRONG>symmetric</STRONG>
<DD><A HREF="node3.html#463">Variable Reordering for BDDs</A>
<DT><STRONG>threshold</STRONG>
<DD><A HREF="node3.html#424">Variable Reordering for BDDs</A>
| <A HREF="node4.html#893">Allowing Asynchronous Reordering</A>
<DT><STRONG>window</STRONG>
<DD><A HREF="node3.html#476">Variable Reordering for BDDs</A>
</DL>
<DT><STRONG>saturating</STRONG>
<DD><DL COMPACT>
<DT><STRONG>decrements</STRONG>
<DD><A HREF="node4.html#782">Saturating Increments and Decrements</A>
<DT><STRONG>increments</STRONG>
<DD><A HREF="node4.html#781">Saturating Increments and Decrements</A>
</DL>
<DT><STRONG>SISDIR</STRONG>
<DD><A HREF="node3.html#594">Using the CUDD Package</A>
<DT><STRONG>SIZEOF_INT</STRONG>
<DD><A HREF="node4.html#794">Saturating Increments and Decrements</A>
| <A HREF="node4.html#803">Saturating Increments and Decrements</A>
<DT><STRONG>SIZEOF_VOID_P</STRONG>
<DD><A HREF="node4.html#793">Saturating Increments and Decrements</A>
| <A HREF="node4.html#802">Saturating Increments and Decrements</A>
<DT><STRONG>statistical counters</STRONG>
<DD><A HREF="node3.html#137">The Manager</A>
| <A HREF="node4.html#734">Reference Counts</A>
| <A HREF="node4.html#853">Cache Sizing</A>
<DT><STRONG>statistics</STRONG>
<DD><A HREF="node4.html#941">Gathering and Interpreting Statistics</A>
<DT><STRONG>subtable</STRONG>
<DD><A HREF="node3.html#159">Initializing and Shutting Down</A>
| <A HREF="node4.html#735">Reference Counts</A>
<DT><STRONG>symmetry</STRONG>
<DD><A HREF="node3.html#465">Variable Reordering for BDDs</A>
<DT><STRONG>table</STRONG>
<DD><DL COMPACT>
<DT><STRONG>computed</STRONG>
<DD><A HREF="node3.html#143">Cache</A>
<DT><STRONG>growth</STRONG>
<DD><A HREF="node3.html#179">Setting Parameters</A>
<DT><STRONG>hash</STRONG>
<DD><A HREF="node3.html#130">The Manager</A>
| <A HREF="node4.html#874">The Unique Table</A>
<DT><STRONG>unique</STRONG>
<DD><A HREF="node3.html#96">Nodes</A>
| <A HREF="node3.html#131">The Manager</A>
| <A HREF="node3.html#133">The Manager</A>
| <A HREF="node3.html#160">Initializing and Shutting Down</A>
| <A HREF="node3.html#167">Initializing and Shutting Down</A>
| <A HREF="node3.html#178">Setting Parameters</A>
| <A HREF="node3.html#420">Variable Reordering for BDDs</A>
| <A HREF="node4.html#736">Reference Counts</A>
| <A HREF="node4.html#850">Cache Sizing</A>
| <A HREF="node4.html#855">Cache Sizing</A>
| <A HREF="node4.html#867">The Unique Table</A>
<DD><DL COMPACT>
<DT><STRONG>fast growth</STRONG>
<DD><A HREF="node4.html#885">The Unique Table</A>
<DT><STRONG>reward-based resizing</STRONG>
<DD><A HREF="node4.html#883">The Unique Table</A>
<DT><STRONG>slow growth</STRONG>
<DD><A HREF="node4.html#886">The Unique Table</A>
</DL>
</DL>
<DT><STRONG>timeout</STRONG>
<DD><A HREF="node3.html#577">Timeouts and Limits</A>
<DT><STRONG>variable</STRONG>
<DD><DL COMPACT>
<DT><STRONG>groups</STRONG>
<DD><A HREF="node3.html#499">Grouping Variables</A>
<DT><STRONG>order</STRONG>
<DD><A HREF="node3.html#99">Nodes</A>
| <A HREF="node3.html#284">New BDD and ADD</A>
<DT><STRONG>permutation</STRONG>
<DD><A HREF="node3.html#101">Nodes</A>
| <A HREF="node4.html#869">The Unique Table</A>
<DT><STRONG>tree</STRONG>
<DD><A HREF="node3.html#501">Grouping Variables</A>
| <A HREF="node3.html#524">Grouping Variables</A>
</DL>
<DT><STRONG>ZDD</STRONG>
<DD><A HREF="node1.html#18">Introduction</A>
| <A HREF="node3.html#117">Nodes</A>
| <A HREF="node3.html#295">New ZDD Variables</A>
| <A HREF="node3.html#355">Basic ZDD Manipulation</A>
| <A HREF="node3.html#396">Converting BDDs to ZDDs</A>
<DT><STRONG>zero</STRONG>
<DD><DL COMPACT>
<DT><STRONG>arithmetic</STRONG>
<DD><A HREF="node3.html#193">One, Logic Zero, and</A>
| <A HREF="node3.html#272">New BDD and ADD</A>
| <A HREF="node3.html#389">Converting ADDs to BDDs</A>
<DT><STRONG>logical</STRONG>
<DD><A HREF="node3.html#192">One, Logic Zero, and</A>
| <A HREF="node3.html#388">Converting ADDs to BDDs</A>
</DL>
<DT><STRONG>Zero-suppressed Binary Decision Diagram</STRONG>
<DD><i>see </i> ZDD
</DL>
<BR><HR>
<ADDRESS>
Fabio Somenzi
2012-02-04
</ADDRESS>
</BODY>
</HTML>

396
resources/3rdparty/cudd-2.5.0/src/cudd/r7x8.1.out

@ -1,396 +0,0 @@
# TestCudd Version #1.0, Release date 3/17/01
# ./testcudd -p2 r7x8.1.mat
:name: r7x8.1.mat: 7 rows 9 columns
:1: M: 63 nodes 5 leaves 52 minterms
000000-- 1
000001-0 1
000001-1 4
000010-0 4
000010-1 3
000011-0 2
000011-1 4
000100-- 3
000101-0 3
000110-0 1
000110-1 2
000111-0 4
001000-- 1
001001-0 4
001010-0 2
001010-1 1
001011-1 4
001100-0 2
001100-1 3
001101-0 3
001110-0 4
001110-1 1
0100-0-0 3
011000-0 3
011010-0 1
100000-0 2
100000-1 3
100001-0 2
100001-1 4
100010-- 3
100011-- 4
100100-- 1
100101-0 2
100110-0 1
100110-1 3
100111-0 3
101000-1 1
101001-0 1
101001-1 4
101100-0 2
101100-1 4
101101-0 4
110000-0 2
110010-0 4
111000-0 2
:2: time to read the matrix = 0.00 sec
:3: C: 22 nodes 1 leaves 52 minterms
0000---- 1
0001-0-- 1
0001-1-0 1
001000-- 1
001001-0 1
001010-- 1
001011-1 1
001100-- 1
001101-0 1
001110-- 1
01-0-0-0 1
1000---- 1
1001-0-- 1
1001-1-0 1
101000-1 1
101001-- 1
101100-- 1
101101-0 1
1100-0-0 1
111000-0 1
Testing iterator on cubes:
000000-- 1
000001-0 1
000001-1 4
000010-0 4
000010-1 3
000011-0 2
000011-1 4
000100-- 3
000101-0 3
000110-0 1
000110-1 2
000111-0 4
001000-- 1
001001-0 4
001010-0 2
001010-1 1
001011-1 4
001100-0 2
001100-1 3
001101-0 3
001110-0 4
001110-1 1
0100-0-0 3
011000-0 3
011010-0 1
100000-0 2
100000-1 3
100001-0 2
100001-1 4
100010-- 3
100011-- 4
100100-- 1
100101-0 2
100110-0 1
100110-1 3
100111-0 3
101000-1 1
101001-0 1
101001-1 4
101100-0 2
101100-1 4
101101-0 4
110000-0 2
110010-0 4
111000-0 2
Testing prime expansion of cubes:
-000---- 1
-00--0-- 1
0--0-0-0 1
--00-0-0 1
-0-100-- 1
10-001-- 1
-00----0 1
00---0-- 1
-1-000-0 1
-0--01-0 1
-0--00-1 1
00-01--1 1
Testing iterator on primes (CNF):
-0-0---- 1
-0---0-- 1
0-0-0--- 1
-0-----0 1
---0-0-0 1
0101-1-1 1
--0-00-1 1
1-0-10-0 1
Cache used slots = 58.06% (expected 58.94%)
xor1: 14 nodes 1 leaves 28 minterms
000--1-1 1
001-11-1 1
01---0-0 1
100--1-1 1
101-00-0 1
101-01-1 1
110--0-0 1
111-00-0 1
Chosen minterm for Hamming distance test: : 9 nodes 1 leaves 1 minterms
11110010 1
Minimum Hamming distance = 1
ycube: 5 nodes 1 leaves 8 minterms
-0-0-0-0 1
CP: 11 nodes 1 leaves 7 minterms
00-0-0-0 1
1000-0-0 1
101000-1 1
:4: ineq: 10 nodes 1 leaves 42 minterms
001000-- 1
00101--- 1
1000---- 1
100100-- 1
10011--- 1
101----- 1
111000-- 1
11101--- 1
10------ 1
-01----- 1
1-1----- 1
-0-0---- 1
1--0---- 1
-0--10-- 1
--1010-- 1
1---10-- 1
:4: ess: 1 nodes 1 leaves 128 minterms
-------- 1
:5: shortP: 7 nodes 1 leaves 2 minterms
000000-- 1
:5b: largest: 4 nodes 1 leaves 16 minterms
01-1---- 1
The value of M along the chosen shortest path is 1
:6: shortP: 5 nodes 1 leaves 8 minterms
0000---- 1
Support of f: : 8 nodes 1 leaves 2 minterms
111111-1 1
Size of the support of f: 7
Size of the support of f: 7
Support of f and g: : 8 nodes 1 leaves 2 minterms
111111-1 1
Size of the support of f and g: 7
Size of the support of f and g: 7
Support common to f and g: : 5 nodes 1 leaves 16 minterms
-1-1-1-1 1
Support private to f: : 4 nodes 1 leaves 32 minterms
1-1-1--- 1
Support private to g: : 1 nodes 1 leaves 256 minterms
-------- 1
Average distance: 4138.57
Number of variables = 8 Number of slots = 2304
Number of keys = 999 Number of min dead = 9216
walsh1: 16 nodes 2 leaves 256 minterms
-0--0--0--0- 1
-0--0--0--10 1
-0--0--0--11 -1
-0--0--10-0- 1
-0--0--10-10 1
-0--0--10-11 -1
-0--0--11-0- -1
-0--0--11-10 -1
-0--0--11-11 1
-0--10-0--0- 1
-0--10-0--10 1
-0--10-0--11 -1
-0--10-10-0- 1
-0--10-10-10 1
-0--10-10-11 -1
-0--10-11-0- -1
-0--10-11-10 -1
-0--10-11-11 1
-0--11-0--0- -1
-0--11-0--10 -1
-0--11-0--11 1
-0--11-10-0- -1
-0--11-10-10 -1
-0--11-10-11 1
-0--11-11-0- 1
-0--11-11-10 1
-0--11-11-11 -1
-10-0--0--0- 1
-10-0--0--10 1
-10-0--0--11 -1
-10-0--10-0- 1
-10-0--10-10 1
-10-0--10-11 -1
-10-0--11-0- -1
-10-0--11-10 -1
-10-0--11-11 1
-10-10-0--0- 1
-10-10-0--10 1
-10-10-0--11 -1
-10-10-10-0- 1
-10-10-10-10 1
-10-10-10-11 -1
-10-10-11-0- -1
-10-10-11-10 -1
-10-10-11-11 1
-10-11-0--0- -1
-10-11-0--10 -1
-10-11-0--11 1
-10-11-10-0- -1
-10-11-10-10 -1
-10-11-10-11 1
-10-11-11-0- 1
-10-11-11-10 1
-10-11-11-11 -1
-11-0--0--0- -1
-11-0--0--10 -1
-11-0--0--11 1
-11-0--10-0- -1
-11-0--10-10 -1
-11-0--10-11 1
-11-0--11-0- 1
-11-0--11-10 1
-11-0--11-11 -1
-11-10-0--0- -1
-11-10-0--10 -1
-11-10-0--11 1
-11-10-10-0- -1
-11-10-10-10 -1
-11-10-10-11 1
-11-10-11-0- 1
-11-10-11-10 1
-11-10-11-11 -1
-11-11-0--0- 1
-11-11-0--10 1
-11-11-0--11 -1
-11-11-10-0- 1
-11-11-10-10 1
-11-11-10-11 -1
-11-11-11-0- -1
-11-11-11-10 -1
-11-11-11-11 1
wtw: 14 nodes 2 leaves 16 minterms
0-00-00-00-0 16
0-00-00-01-1 16
0-00-01-10-0 16
0-00-01-11-1 16
0-01-10-00-0 16
0-01-10-01-1 16
0-01-11-10-0 16
0-01-11-11-1 16
1-10-00-00-0 16
1-10-00-01-1 16
1-10-01-10-0 16
1-10-01-11-1 16
1-11-10-00-0 16
1-11-10-01-1 16
1-11-11-10-0 16
1-11-11-11-1 16
Average length of non-empty lists = 1
**** CUDD modifiable parameters ****
Hard limit for cache size: 7645866
Cache hit threshold for resizing: 30%
Garbage collection enabled: yes
Limit for fast unique table growth: 4587520
Maximum number of variables sifted per reordering: 1000
Maximum number of variable swaps per reordering: 2000000
Maximum growth while sifting a variable: 1.2
Dynamic reordering of BDDs enabled: no
Default BDD reordering method: 4
Dynamic reordering of ZDDs enabled: no
Default ZDD reordering method: 4
Realignment of ZDDs to BDDs enabled: no
Realignment of BDDs to ZDDs enabled: no
Dead nodes counted in triggering reordering: no
Group checking criterion: 7
Recombination threshold: 0
Symmetry violation threshold: 0
Arc violation threshold: 0
GA population size: 0
Number of crossovers for GA: 0
Next reordering threshold: 4004
**** CUDD non-modifiable parameters ****
Memory in use: 4274508
Peak number of nodes: 2044
Peak number of live nodes: 119
Number of BDD variables: 9
Number of ZDD variables: 0
Number of cache entries: 2048
Number of cache look-ups: 2864
Number of cache hits: 729
Number of cache insertions: 2301
Number of cache collisions: 947
Number of cache deletions: 1351
Cache used slots = 66.11% (expected 67.49%)
Soft limit for cache size: 13312
Number of buckets in unique table: 2560
Used buckets in unique table: 0.51% (expected 0.51%)
Number of BDD and ADD nodes: 13
Number of ZDD nodes: 0
Number of dead BDD and ADD nodes: 0
Number of dead ZDD nodes: 0
Total number of nodes allocated: 1095
Total number of nodes reclaimed: 967
Garbage collections so far: 1
Time for garbage collection: 0.00 sec
Reorderings so far: 0
Time for reordering: 0.00 sec
total time = 0.00 sec
Runtime Statistics
------------------
Machine name: jobim.colorado.edu
User time 0.0 seconds
System time 0.0 seconds
Average resident text size = 0K
Average resident data+stack size = 0K
Maximum resident size = 0K
Virtual text size = 131653K
Virtual data size = 152K
data size initialized = 18K
data size uninitialized = 1K
data size sbrk = 133K
Virtual memory limit = 358400K (4194304K)
Major page faults = 0
Minor page faults = 1330
Swaps = 0
Input blocks = 0
Output blocks = 16
Context switch (voluntary) = 0
Context switch (involuntary) = 1

243
resources/3rdparty/cudd-2.5.0/src/dddmp/Makefile

@ -1,243 +0,0 @@
#----------------------------------------------------------------------------#
# Makefile for the dddmp distribution kit #
# dddmp: Decision Diagram DuMP #
# (storage and retrieval of BDDs, ADDs and CNF formulas) #
# Revision: Version 2.0.2, February 01, 2004 #
#----------------------------------------------------------------------------#
# Commands Available:
# make
# it makes the library libdddmp.a
# make testdddmp
# it makes the testdddmp program, which allows to test the dddmp
# package
# make clean
# it cleans dddmp
# make distclean
# it cleans dddmp (as clean) with libraries and executable
# files
#----------------------------------------------------------------------------#
# Configuration Section #
# uncomment the desired options/sections #
#----------------------------------------------------------------------------#
#--------------------#
# Define Directories #
#--------------------#
# Cudd directory
WHERE = ..
#WHERE = ../cudd-2.4.0
# Include directory (Cudd include files)
INCLUDE = $(WHERE)/include
#------------------------#
# Define C Compiler Used #
#------------------------#
CC = gcc
#CC = g++
#CC = cc
#CC = icc
#CC = ecc
#CC = /usr/ucb/cc
#CC = c89
.SUFFIXES: .o .c .u
#---------------#
# Define ranlib #
#---------------#
# For machines with ranlib and you think it is needed
RANLIB = ranlib
# For machines which either do not have ranlib or can do without it
#RANLIB = :
#----------------------------------#
# Define Machine Independent Flags #
#----------------------------------#
# Settings for cc
#ICFLAGS =
#ICFLAGS = -g
#ICFLAGS = -O
# Settings for optimized code with gcc
#ICFLAGS = -g -Wall
#ICFLAGS = -g -O3 -Wall
ICFLAGS = -g -O6 -Wall
#--------------------------------#
# Define Machine Dependent Flags #
#--------------------------------#
# When no special flags are needed
#XCFLAGS = -DHAVE_IEEE_754 -DBSD
# Linux with Gcc 2.8.1 or higher on i686.
#XCFLAGS = -mcpu=pentiumpro -malign-double -DHAVE_IEEE_754 -DBSD
# Gcc 3.3.2 or higher on i686.
XCFLAGS = -mcpu=pentium4 -malign-double -DHAVE_IEEE_754 -DBSD
# For Solaris, BSD should not be replaced by UNIX100.
#XCFLAGS = -DHAVE_IEEE_754 -DUNIX100 -DEPD_BIG_ENDIAN
# New native compiler for the Alphas; 64-bit pointers.
#XCFLAGS = -g3 -O4 -std -DBSD -DHAVE_IEEE_754 -ieee_with_no_inexact -tune host -DSIZEOF_VOID_P=8 -DSIZEOF_LONG=8
# New native compiler for the Alphas; 32-bit pointers.
#XCFLAGS = -g3 -O4 -std -DBSD -DHAVE_IEEE_754 -ieee_with_no_inexact -tune host -xtaso -DSIZEOF_LONG=8
# Windows95/98/NT/XP with Cygwin tools
#XCFLAGS = -mcpu=pentiumpro -malign-double -DHAVE_IEEE_754 -DHAVE_GETRLIMIT=0 -DRLIMIT_DATA_DEFAULT=67108864
#---------------------------------------------#
# Define Level of Self-Checking and Verbosity #
#---------------------------------------------#
# ... for the CUDD package
#DDDEBUG = -DDD_DEBUG -DDD_VERBOSE -DDD_STATS -DDD_CACHE_PROFILE -DDD_UNIQUE_PROFILE -DDD_COUNT
DDDEBUG =
# ... for the MTR package
#MTRDEBUG = -DMTR_DEBUG
MTRDEBUG =
# ... for the DDDMP package
#DDDMPDEBUG = -DDDDMP_DEBUG
DDDMPDEBUG =
#-----------------------#
# Define Loader Options #
#-----------------------#
LDFLAGS =
# This may produce faster code on the DECstations.
#LDFLAGS = -jmpopt -Olimit 1000
# This may be necessary under some old versions of Linux.
#LDFLAGS = -static
# This normally makes the program faster on the DEC Alphas.
#LDFLAGS = -non_shared -om
# This is for 32-bit pointers on the DEC Alphas.
#LDFLAGS = -non_shared -om -taso
#LDFLAGS = -non_shared -taso
#-------------#
# Define PURE #
#-------------#
PURE =
# ... as purify to link with purify.
#PURE = purify
# ... as quantify to link with quantify.
#PURE = quantify
#------------#
# Define EXE #
#------------#
EXE =
# ... as .exe for MS-DOS and derivatives.
#EXE = .exe
#----------------------------------------------------------------------------#
# Files for the Package #
#----------------------------------------------------------------------------#
P = dddmp
PSRC = dddmpStoreBdd.c dddmpStoreAdd.c dddmpStoreCnf.c \
dddmpLoad.c dddmpLoadCnf.c \
dddmpNodeBdd.c dddmpNodeAdd.c dddmpNodeCnf.c \
dddmpStoreMisc.c dddmpUtil.c dddmpBinary.c dddmpConvert.c \
dddmpDbg.c
PHDR = dddmp.h dddmpInt.h $(INCLUDE)/cudd.h $(INCLUDE)/cuddInt.h
POBJ = $(PSRC:.c=.o)
PUBJ = $(PSRC:.c=.u)
TARGET = test$(P)$(EXE)
TARGETu = test$(P)-u
# files for the test program
SRC = test$(P).c
OBJ = $(SRC:.c=.o)
UBJ = $(SRC:.c=.u)
#----------------------------------------------------------------------------#
# Rules to compile and build libraries and executables #
#----------------------------------------------------------------------------#
#MFLAG =
MFLAG = -DMNEMOSYNE
MNEMLIB = ../mnemosyne/libmnem.a
# This is to create the lint library
LINTFLAGS = -u -n
LINTSWITCH = -o
LIBS = ./libdddmp.a $(WHERE)/cudd/libcudd.a $(WHERE)/mtr/libmtr.a \
$(WHERE)/st/libst.a $(WHERE)/util/libutil.a $(WHERE)/epd/libepd.a
MNEMLIB =
BLIBS = -kL. -kldddmp -kL$(WHERE)/cudd -klcudd -kL$(WHERE)/mtr -klmtr \
-kL$(WHERE)/st -klst -kL$(WHERE)/util -klutil
LINTLIBS = ./llib-ldddmp.ln $(WHERE)/cudd/llib-lcudd.ln \
$(WHERE)/mtr/llib-lmtr.ln $(WHERE)/st/llib-lst.ln \
$(WHERE)/util/llib-lutil.ln
lib$(P).a: $(POBJ)
ar rv $@ $?
$(RANLIB) $@
.c.o: $(PHDR)
$(CC) -c $< -I$(INCLUDE) $(ICFLAGS) $(XCFLAGS) $(DDDEBUG) $(MTRDEBUG) $(DDDMPDEBUG) $(LDFLAGS)
optimize_dec: lib$(P).b
lib$(P).b: $(PUBJ)
ar rv $@ $?
$(RANLIB) $@
.c.u: $(PHDR)
cc -c $< -I$(INCLUDE) $(CFLAGS)
# if the header files change, recompile
$(POBJ): $(PHDR)
$(PUBJ): $(PHDR)
$(OBJ): $(PHDR)
$(UBJ): $(PHDR)
$(TARGET): $(SRC) $(OBJ) $(PHDR) $(LIBS) $(MNEMLIB)
$(PURE) $(CC) $(ICFLAGS) $(XCFLAGS) $(DDDEBUG) $(MTRDEBUG) $(DDDMPDEBUG) $(LDFLAGS) -o $@ $(OBJ) $(LIBS) $(MNEMLIB) -lm
# optimize (DECstations and Alphas only: uses u-code)
$(TARGETu): $(SRC) $(UBJ) $(PHDR) $(LIBS:.a=.b)
cc -O3 -Olimit 1000 $(XCFLAGS) $(LDFLAGS) -o $@ $(UBJ) $(BLIBS) -lm
lint: llib-l$(P).ln
llib-l$(P).ln: $(PSRC) $(PHDR)
lint $(LINTFLAGS) $(LINTSWITCH)$(P) -I$(INCLUDE) $(PSRC)
lintpgm: lint
lint $(LINTFLAGS) -I$(INCLUDE) $(SRC) $(LINTLIBS)
tags: $(PSRC) $(PHDR)
ctags $(PSRC) $(PHDR)
all: lib$(P).a lib$(P).b llib-l$(P).ln tags
programs: $(TARGET) $(TARGETu) lintpgm
#----------------------------------------------------------------------------#
# Clean the Package #
#----------------------------------------------------------------------------#
clean:
rm -f *.o *.u mon.out gmon.out *.pixie *.Addrs *.Counts mnem.* \
.pure core *.warnings
distclean: clean
rm -f $(TARGET) $(TARGETu) lib*.a lib$(P).b llib-l$(P).ln \
*.bak *~ tags .gdb_history *.qv *.qx

455
resources/3rdparty/cudd-2.5.0/src/dddmp/dddmpDdNodeBdd.c

@ -1,455 +0,0 @@
/**CFile**********************************************************************
FileName [dddmpDdNodeBdd.c]
PackageName [dddmp]
Synopsis [Functions to handle BDD node infos and numbering]
Description [Functions to handle BDD node infos and numbering.
]
Author [Gianpiero Cabodi and Stefano Quer]
Copyright [
Copyright (c) 2004 by Politecnico di Torino.
All Rights Reserved. This software is for educational purposes only.
Permission is given to academic institutions to use, copy, and modify
this software and its documentation provided that this introductory
message is not removed, that this software and its documentation is
used for the institutions' internal research and educational purposes,
and that no monies are exchanged. No guarantee is expressed or implied
by the distribution of this code.
Send bug-reports and/or questions to:
{gianpiero.cabodi,stefano.quer}@polito.it.
]
******************************************************************************/
#include "dddmpInt.h"
/*---------------------------------------------------------------------------*/
/* Stucture declarations */
/*---------------------------------------------------------------------------*/
/*---------------------------------------------------------------------------*/
/* Type declarations */
/*---------------------------------------------------------------------------*/
/*---------------------------------------------------------------------------*/
/* Variable declarations */
/*---------------------------------------------------------------------------*/
/*---------------------------------------------------------------------------*/
/* Macro declarations */
/*---------------------------------------------------------------------------*/
/**AutomaticStart*************************************************************/
/*---------------------------------------------------------------------------*/
/* Static function prototypes */
/*---------------------------------------------------------------------------*/
static int NumberNodeRecur(DdNode *f, int id);
static void RemoveFromUniqueRecur(DdManager *ddMgr, DdNode *f);
static void RestoreInUniqueRecur(DdManager *ddMgr, DdNode *f);
/**AutomaticEnd***************************************************************/
/*---------------------------------------------------------------------------*/
/* Definition of exported functions */
/*---------------------------------------------------------------------------*/
/*---------------------------------------------------------------------------*/
/* Definition of internal functions */
/*---------------------------------------------------------------------------*/
/**Function********************************************************************
Synopsis [Removes nodes from unique table and number them]
Description [Node numbering is required to convert pointers to integers.
Since nodes are removed from unique table, no new nodes should
be generated before re-inserting nodes in the unique table
(DddmpUnnumberDdNodes()).
]
SideEffects [Nodes are temporarily removed from unique table]
SeeAlso [RemoveFromUniqueRecur(), NumberNodeRecur(),
DddmpUnnumberDdNodes()]
******************************************************************************/
int
DddmpNumberDdNodes (
DdManager *ddMgr /* IN: DD Manager */,
DdNode **f /* IN: array of BDDs */,
int n /* IN: number of BDD roots in the array of BDDs */
)
{
int id=0, i;
for (i=0; i<n; i++) {
RemoveFromUniqueRecur (ddMgr, f[i]);
}
for (i=0; i<n; i++) {
id = NumberNodeRecur (f[i], id);
}
return (id);
}
/**Function********************************************************************
Synopsis [Restores nodes in unique table, loosing numbering]
Description [Node indexes are no more needed. Nodes are re-linked in the
unique table.
]
SideEffects [None]
SeeAlso [DddmpNumberDdNode()]
******************************************************************************/
void
DddmpUnnumberDdNodes(
DdManager *ddMgr /* IN: DD Manager */,
DdNode **f /* IN: array of BDDs */,
int n /* IN: number of BDD roots in the array of BDDs */
)
{
int i;
for (i=0; i<n; i++) {
RestoreInUniqueRecur (ddMgr, f[i]);
}
return;
}
/**Function********************************************************************
Synopsis [Write index to node]
Description [The index of the node is written in the "next" field of
a DdNode struct. LSB is not used (set to 0). It is used as
"visited" flag in DD traversals.
]
SideEffects [None]
SeeAlso [DddmpReadNodeIndex(), DddmpSetVisited (), DddmpVisited ()]
******************************************************************************/
void
DddmpWriteNodeIndex (
DdNode *f /* IN: BDD node */,
int id /* IN: index to be written */
)
{
#if 0
if (1 || !Cudd_IsConstant (f)) {
#else
if (!Cudd_IsConstant (f)) {
#endif
f->next = (struct DdNode *)((ptruint)((id)<<1));
}
return;
}
/**Function********************************************************************
Synopsis [Reads the index of a node]
Description [Reads the index of a node. LSB is skipped (used as visited
flag).
]
SideEffects [None]
SeeAlso [DddmpWriteNodeIndex(), DddmpSetVisited (), DddmpVisited ()]
******************************************************************************/
int
DddmpReadNodeIndex (
DdNode *f /* IN: BDD node */
)
{
#if 0
if (1 || !Cudd_IsConstant (f)) {
#else
if (!Cudd_IsConstant (f)) {
#endif
return ((int)(((ptruint)(f->next))>>1));
} else {
return (1);
}
}
/**Function********************************************************************
Synopsis [Returns true if node is visited]
Description [Returns true if node is visited]
SideEffects [None]
SeeAlso [DddmpSetVisited (), DddmpClearVisited ()]
******************************************************************************/
int
DddmpVisited (
DdNode *f /* IN: BDD node to be tested */
)
{
f = Cudd_Regular(f);
return ((int)((ptruint)(f->next)) & (01));
}
/**Function********************************************************************
Synopsis [Marks a node as visited]
Description [Marks a node as visited]
SideEffects [None]
SeeAlso [DddmpVisited (), DddmpClearVisited ()]
******************************************************************************/
void
DddmpSetVisited (
DdNode *f /* IN: BDD node to be marked (as visited) */
)
{
f = Cudd_Regular(f);
f->next = (DdNode *)(ptruint)((int)((ptruint)(f->next))|01);
return;
}
/**Function********************************************************************
Synopsis [Marks a node as not visited]
Description [Marks a node as not visited]
SideEffects [None]
SeeAlso [DddmpVisited (), DddmpSetVisited ()]
******************************************************************************/
void
DddmpClearVisited (
DdNode *f /* IN: BDD node to be marked (as not visited) */
)
{
f = Cudd_Regular (f);
f->next = (DdNode *)(ptruint)((int)((ptruint)(f->next)) & (~01));
return;
}
/*---------------------------------------------------------------------------*/
/* Definition of static functions */
/*---------------------------------------------------------------------------*/
/**Function********************************************************************
Synopsis [Number nodes recursively in post-order]
Description [Number nodes recursively in post-order.
The "visited" flag is used with inverse polarity, because all nodes
were set "visited" when removing them from unique.
]
SideEffects ["visited" flags are reset.]
SeeAlso []
******************************************************************************/
static int
NumberNodeRecur(
DdNode *f /* IN: root of the BDD to be numbered */,
int id /* IN/OUT: index to be assigned to the node */
)
{
f = Cudd_Regular(f);
if (!DddmpVisited (f)) {
return (id);
}
if (!cuddIsConstant (f)) {
id = NumberNodeRecur (cuddT (f), id);
id = NumberNodeRecur (cuddE (f), id);
}
DddmpWriteNodeIndex (f, ++id);
DddmpClearVisited (f);
return (id);
}
/**Function********************************************************************
Synopsis [Removes a node from unique table]
Description [Removes a node from the unique table by locating the proper
subtable and unlinking the node from it. It recurs on the
children of the node.
]
SideEffects [Nodes are left with the "visited" flag true.]
SeeAlso [RestoreInUniqueRecur()]
******************************************************************************/
static void
RemoveFromUniqueRecur (
DdManager *ddMgr /* IN: DD Manager */,
DdNode *f /* IN: root of the BDD to be extracted */
)
{
DdNode *node, *last, *next;
DdNode *sentinel = &(ddMgr->sentinel);
DdNodePtr *nodelist;
DdSubtable *subtable;
int pos, level;
f = Cudd_Regular (f);
if (DddmpVisited (f)) {
return;
}
if (!cuddIsConstant (f)) {
RemoveFromUniqueRecur (ddMgr, cuddT (f));
RemoveFromUniqueRecur (ddMgr, cuddE (f));
level = ddMgr->perm[f->index];
subtable = &(ddMgr->subtables[level]);
nodelist = subtable->nodelist;
pos = ddHash (cuddT (f), cuddE (f), subtable->shift);
node = nodelist[pos];
last = NULL;
while (node != sentinel) {
next = node->next;
if (node == f) {
if (last != NULL)
last->next = next;
else
nodelist[pos] = next;
break;
} else {
last = node;
node = next;
}
}
f->next = NULL;
}
DddmpSetVisited (f);
return;
}
/**Function********************************************************************
Synopsis [Restores a node in unique table]
Description [Restores a node in unique table (recursively)]
SideEffects [Nodes are not restored in the same order as before removal]
SeeAlso [RemoveFromUnique()]
******************************************************************************/
static void
RestoreInUniqueRecur (
DdManager *ddMgr /* IN: DD Manager */,
DdNode *f /* IN: root of the BDD to be restored */
)
{
DdNodePtr *nodelist;
DdNode *T, *E, *looking;
DdNodePtr *previousP;
DdSubtable *subtable;
int pos, level;
#ifdef DDDMP_DEBUG
DdNode *node;
DdNode *sentinel = &(ddMgr->sentinel);
#endif
f = Cudd_Regular(f);
if (!Cudd_IsComplement (f->next)) {
return;
}
if (cuddIsConstant (f)) {
DddmpClearVisited (f);
/*f->next = NULL;*/
return;
}
RestoreInUniqueRecur (ddMgr, cuddT (f));
RestoreInUniqueRecur (ddMgr, cuddE (f));
level = ddMgr->perm[f->index];
subtable = &(ddMgr->subtables[level]);
nodelist = subtable->nodelist;
pos = ddHash (cuddT (f), cuddE (f), subtable->shift);
#ifdef DDDMP_DEBUG
/* verify uniqueness to avoid duplicate nodes in unique table */
for (node=nodelist[pos]; node != sentinel; node=node->next)
assert(node!=f);
#endif
T = cuddT (f);
E = cuddE (f);
previousP = &(nodelist[pos]);
looking = *previousP;
while (T < cuddT (looking)) {
previousP = &(looking->next);
looking = *previousP;
}
while (T == cuddT (looking) && E < cuddE (looking)) {
previousP = &(looking->next);
looking = *previousP;
}
f->next = *previousP;
*previousP = f;
return;
}

944
resources/3rdparty/cudd-2.5.0/src/dddmp/dddmpDdNodeCnf.c

@ -1,944 +0,0 @@
/**CFile**********************************************************************
FileName [dddmpDdNodeCnf.c]
PackageName [dddmp]
Synopsis [Functions to handle BDD node infos and numbering
while storing a CNF formula from a BDD or an array of BDDs]
Description [Functions to handle BDD node infos and numbering
while storing a CNF formula from a BDD or an array of BDDs.
]
Author [Gianpiero Cabodi and Stefano Quer]
Copyright [
Copyright (c) 2004 by Politecnico di Torino.
All Rights Reserved. This software is for educational purposes only.
Permission is given to academic institutions to use, copy, and modify
this software and its documentation provided that this introductory
message is not removed, that this software and its documentation is
used for the institutions' internal research and educational purposes,
and that no monies are exchanged. No guarantee is expressed or implied
by the distribution of this code.
Send bug-reports and/or questions to:
{gianpiero.cabodi,stefano.quer}@polito.it.
]
******************************************************************************/
#include "dddmpInt.h"
/*---------------------------------------------------------------------------*/
/* Stucture declarations */
/*---------------------------------------------------------------------------*/
/*---------------------------------------------------------------------------*/
/* Type declarations */
/*---------------------------------------------------------------------------*/
/*---------------------------------------------------------------------------*/
/* Variable declarations */
/*---------------------------------------------------------------------------*/
#define DDDMP_DEBUG_CNF 0
/*---------------------------------------------------------------------------*/
/* Macro declarations */
/*---------------------------------------------------------------------------*/
/**AutomaticStart*************************************************************/
/*---------------------------------------------------------------------------*/
/* Static function prototypes */
/*---------------------------------------------------------------------------*/
int DddmpWriteNodeIndexCnf(DdNode *f, int *cnfIds, int id);
int DddmpReadNodeIndexCnf(DdNode *f);
static int DddmpClearVisitedCnfRecur(DdNode *f);
int DddmpVisitedCnf(DdNode *f);
void DddmpSetVisitedCnf(DdNode *f);
static void DddmpClearVisitedCnf(DdNode *f);
static int NumberNodeRecurCnf(DdNode *f, int *cnfIds, int id);
static void DddmpDdNodesCheckIncomingAndScanPath(DdNode *f, int pathLengthCurrent, int edgeInTh, int pathLengthTh);
static int DddmpDdNodesNumberEdgesRecur(DdNode *f, int *cnfIds, int id);
static int DddmpDdNodesResetCountRecur(DdNode *f);
static int DddmpDdNodesCountEdgesRecur(DdNode *f);
static void RemoveFromUniqueRecurCnf(DdManager *ddMgr, DdNode *f);
static void RestoreInUniqueRecurCnf(DdManager *ddMgr, DdNode *f);
static int DddmpPrintBddAndNextRecur(DdManager *ddMgr, DdNode *f);
/**AutomaticEnd***************************************************************/
/*---------------------------------------------------------------------------*/
/* Definition of exported functions */
/*---------------------------------------------------------------------------*/
/*---------------------------------------------------------------------------*/
/* Definition of internal functions */
/*---------------------------------------------------------------------------*/
/**Function********************************************************************
Synopsis [Removes nodes from unique table and numbers them]
Description [Node numbering is required to convert pointers to integers.
Since nodes are removed from unique table, no new nodes should
be generated before re-inserting nodes in the unique table
(DddmpUnnumberDdNodesCnf()).
]
SideEffects [Nodes are temporarily removed from unique table]
SeeAlso [RemoveFromUniqueRecurCnf(), NumberNodeRecurCnf(),
DddmpUnnumberDdNodesCnf()]
******************************************************************************/
int
DddmpNumberDdNodesCnf (
DdManager *ddMgr /* IN: DD Manager */,
DdNode **f /* IN: array of BDDs */,
int rootN /* IN: number of BDD roots in the array of BDDs */,
int *cnfIds /* OUT: CNF identifiers for variables */,
int id /* OUT: number of Temporary Variables Introduced */
)
{
int i;
for (i=0; i<rootN; i++) {
RemoveFromUniqueRecurCnf (ddMgr, f[i]);
}
for (i=0; i<rootN; i++) {
id = NumberNodeRecurCnf (f[i], cnfIds, id);
}
return (id);
}
/**Function********************************************************************
Synopsis [Removes nodes from unique table and numbers each node according
to the number of its incoming BDD edges.
]
Description [Removes nodes from unique table and numbers each node according
to the number of its incoming BDD edges.
]
SideEffects [Nodes are temporarily removed from unique table]
SeeAlso [RemoveFromUniqueRecurCnf()]
******************************************************************************/
int
DddmpDdNodesCountEdgesAndNumber (
DdManager *ddMgr /* IN: DD Manager */,
DdNode **f /* IN: Array of BDDs */,
int rootN /* IN: Number of BDD roots in the array of BDDs */,
int edgeInTh /* IN: Max # In-Edges, after a Insert Cut Point */,
int pathLengthTh /* IN: Max Path Length (after, Insert a Cut Point) */,
int *cnfIds /* OUT: CNF identifiers for variables */,
int id /* OUT: Number of Temporary Variables Introduced */
)
{
int retValue, i;
/*-------------------------- Remove From Unique ---------------------------*/
for (i=0; i<rootN; i++) {
RemoveFromUniqueRecurCnf (ddMgr, f[i]);
}
/*-------------------- Reset Counter and Reset Visited --------------------*/
for (i=0; i<rootN; i++) {
retValue = DddmpDdNodesResetCountRecur (f[i]);
}
/* Here we must have:
* cnfIndex = 0
* visitedFlag = 0
* FOR ALL nodes
*/
#if DDDMP_DEBUG_CNF
fprintf (stdout, "###---> BDDs After Count Reset:\n");
DddmpPrintBddAndNext (ddMgr, f, rootN);
#endif
/*----------------------- Count Incoming Edges ----------------------------*/
for (i=0; i<rootN; i++) {
retValue = DddmpDdNodesCountEdgesRecur (f[i]);
}
/* Here we must have:
* cnfIndex = incoming edge count
* visitedFlag = 0 (AGAIN ... remains untouched)
* FOR ALL nodes
*/
#if DDDMP_DEBUG_CNF
fprintf (stdout, "###---> BDDs After Count Recur:\n");
DddmpPrintBddAndNext (ddMgr, f, rootN);
#endif
/*------------------------- Count Path Length ----------------------------*/
for (i=0; i<rootN; i++) {
DddmpDdNodesCheckIncomingAndScanPath (f[i], 0, edgeInTh,
pathLengthTh);
}
/* Here we must have:
* cnfIndex = 1 if we want to insert there a cut point
* 0 if we do NOT want to insert there a cut point
* visitedFlag = 1
* FOR ALL nodes
*/
#if DDDMP_DEBUG_CNF
fprintf (stdout, "###---> BDDs After Check Incoming And Scan Path:\n");
DddmpPrintBddAndNext (ddMgr, f, rootN);
#endif
/*-------------------- Number Nodes and Set Visited -----------------------*/
for (i=0; i<rootN; i++) {
id = DddmpDdNodesNumberEdgesRecur (f[i], cnfIds, id);
}
/* Here we must have:
* cnfIndex = CNF auxiliary variable enumeration
* visitedFlag = 0
* FOR ALL nodes
*/
#if DDDMP_DEBUG_CNF
fprintf (stdout, "###---> BDDs After Count Edges Recur:\n");
DddmpPrintBddAndNext (ddMgr, f, rootN);
#endif
/*---------------------------- Clear Visited ------------------------------*/
#if DDDMP_DEBUG_CNF
for (i=0; i<rootN; i++) {
retValue = DddmpClearVisitedCnfRecur (f[i]);
}
#if DDDMP_DEBUG_CNF
fprintf (stdout, "###---> BDDs After All Numbering Process:\n");
DddmpPrintBddAndNext (ddMgr, f, rootN);
#endif
#endif
return (id);
}
/**Function********************************************************************
Synopsis [Restores nodes in unique table, loosing numbering]
Description [Node indexes are no more needed. Nodes are re-linked in the
unique table.
]
SideEffects [None]
SeeAlso [DddmpNumberDdNode()]
******************************************************************************/
void
DddmpUnnumberDdNodesCnf(
DdManager *ddMgr /* IN: DD Manager */,
DdNode **f /* IN: array of BDDs */,
int rootN /* IN: number of BDD roots in the array of BDDs */
)
{
int i;
for (i=0; i<rootN; i++) {
RestoreInUniqueRecurCnf (ddMgr, f[i]);
}
return;
}
/**Function********************************************************************
Synopsis [Prints debug information]
Description [Prints debug information for an array of BDDs on the screen]
SideEffects [None]
SeeAlso []
******************************************************************************/
int
DddmpPrintBddAndNext (
DdManager *ddMgr /* IN: DD Manager */,
DdNode **f /* IN: Array of BDDs to be displayed */,
int rootN /* IN: Number of BDD roots in the array of BDDs */
)
{
int i;
for (i=0; i<rootN; i++) {
fprintf (stdout, "---> Bdd %d:\n", i);
fflush (stdout);
DddmpPrintBddAndNextRecur (ddMgr, f[i]);
}
return (DDDMP_SUCCESS);
}
/**Function********************************************************************
Synopsis [Write index to node]
Description [The index of the node is written in the "next" field of
a DdNode struct. LSB is not used (set to 0). It is used as
"visited" flag in DD traversals.
]
SideEffects [None]
SeeAlso [DddmpReadNodeIndexCnf(), DddmpSetVisitedCnf (),
DddmpVisitedCnf ()
]
******************************************************************************/
int
DddmpWriteNodeIndexCnfBis (
DdNode *f /* IN: BDD node */,
int id /* IN: index to be written */
)
{
if (!Cudd_IsConstant (f)) {
f->next = (struct DdNode *)((ptruint)((id)<<1));
}
return (DDDMP_SUCCESS);
}
/*---------------------------------------------------------------------------*/
/* Definition of static functions */
/*---------------------------------------------------------------------------*/
/**Function********************************************************************
Synopsis [Write index to node]
Description [The index of the node is written in the "next" field of
a DdNode struct. LSB is not used (set to 0). It is used as
"visited" flag in DD traversals. The index corresponds to
the BDD node variable if both the node's children are a
constant node, otherwise a new CNF variable is used.
]
SideEffects [None]
SeeAlso [DddmpReadNodeIndexCnf(), DddmpSetVisitedCnf (),
DddmpVisitedCnf ()]
*****************************************************************************/
int
DddmpWriteNodeIndexCnf (
DdNode *f /* IN: BDD node */,
int *cnfIds /* IN: possible source for the index to be written */,
int id /* IN: possible source for the index to be written */
)
{
if (!Cudd_IsConstant (f)) {
if (Cudd_IsConstant (cuddT (f)) && Cudd_IsConstant (cuddE (f))) {
/* If Variable SET ID as Variable ID */
f->next = (struct DdNode *)((ptruint)((cnfIds[f->index])<<1));
} else {
f->next = (struct DdNode *)((ptruint)((id)<<1));
id++;
}
}
return(id);
}
/**Function********************************************************************
Synopsis [Reads the index of a node]
Description [Reads the index of a node. LSB is skipped (used as visited
flag).
]
SideEffects [None]
SeeAlso [DddmpWriteNodeIndexCnf(), DddmpSetVisitedCnf (),
DddmpVisitedCnf ()]
******************************************************************************/
int
DddmpReadNodeIndexCnf (
DdNode *f /* IN: BDD node */
)
{
if (!Cudd_IsConstant (f)) {
return ((int)(((ptruint)(f->next))>>1));
} else {
return (1);
}
}
/**Function********************************************************************
Synopsis [Mark ALL nodes as not visited]
Description [Mark ALL nodes as not visited (it recurs on the node children)]
SideEffects [None]
SeeAlso [DddmpVisitedCnf (), DddmpSetVisitedCnf ()]
******************************************************************************/
static int
DddmpClearVisitedCnfRecur (
DdNode *f /* IN: root of the BDD to be marked */
)
{
int retValue;
f = Cudd_Regular(f);
if (cuddIsConstant (f)) {
return (DDDMP_SUCCESS);
}
if (!DddmpVisitedCnf (f)) {
return (DDDMP_SUCCESS);
}
retValue = DddmpClearVisitedCnfRecur (cuddT (f));
retValue = DddmpClearVisitedCnfRecur (cuddE (f));
DddmpClearVisitedCnf (f);
return (DDDMP_SUCCESS);
}
/**Function********************************************************************
Synopsis [Returns true if node is visited]
Description [Returns true if node is visited]
SideEffects [None]
SeeAlso [DddmpSetVisitedCnf (), DddmpClearVisitedCnf ()]
******************************************************************************/
int
DddmpVisitedCnf (
DdNode *f /* IN: BDD node to be tested */
)
{
f = Cudd_Regular(f);
return ((int)((ptruint)(f->next)) & (01));
}
/**Function********************************************************************
Synopsis [Marks a node as visited]
Description [Marks a node as visited]
SideEffects [None]
SeeAlso [DddmpVisitedCnf (), DddmpClearVisitedCnf ()]
******************************************************************************/
void
DddmpSetVisitedCnf (
DdNode *f /* IN: BDD node to be marked (as visited) */
)
{
f = Cudd_Regular(f);
f->next = (DdNode *)(ptruint)((int)((ptruint)(f->next))|01);
return;
}
/**Function********************************************************************
Synopsis [Marks a node as not visited]
Description [Marks a node as not visited]
SideEffects [None]
SeeAlso [DddmpVisitedCnf (), DddmpSetVisitedCnf ()]
******************************************************************************/
static void
DddmpClearVisitedCnf (
DdNode *f /* IN: BDD node to be marked (as not visited) */
)
{
f = Cudd_Regular (f);
f->next = (DdNode *)(ptruint)((int)((ptruint)(f->next)) & (~01));
return;
}
/**Function********************************************************************
Synopsis [Number nodes recursively in post-order]
Description [Number nodes recursively in post-order.
The "visited" flag is used with inverse polarity, because all nodes
were set "visited" when removing them from unique.
]
SideEffects ["visited" flags are reset.]
SeeAlso []
******************************************************************************/
static int
NumberNodeRecurCnf(
DdNode *f /* IN: root of the BDD to be numbered */,
int *cnfIds /* IN: possible source for numbering */,
int id /* IN/OUT: possible source for numbering */
)
{
f = Cudd_Regular(f);
if (!DddmpVisitedCnf (f)) {
return (id);
}
if (!cuddIsConstant (f)) {
id = NumberNodeRecurCnf (cuddT (f), cnfIds, id);
id = NumberNodeRecurCnf (cuddE (f), cnfIds, id);
}
id = DddmpWriteNodeIndexCnf (f, cnfIds, id);
DddmpClearVisitedCnf (f);
return (id);
}
/**Function********************************************************************
Synopsis [Number nodes recursively in post-order]
Description [Number nodes recursively in post-order.
The "visited" flag is used with the right polarity.
The node is assigned to a new CNF variable only if it is a "shared"
node (i.e. the number of its incoming edges is greater than 1).
]
SideEffects ["visited" flags are set.]
SeeAlso []
******************************************************************************/
static void
DddmpDdNodesCheckIncomingAndScanPath (
DdNode *f /* IN: BDD node to be numbered */,
int pathLengthCurrent /* IN: Current Path Length */,
int edgeInTh /* IN: Max # In-Edges, after a Insert Cut Point */,
int pathLengthTh /* IN: Max Path Length (after, Insert a Cut Point) */
)
{
int retValue;
f = Cudd_Regular(f);
if (DddmpVisitedCnf (f)) {
return;
}
if (cuddIsConstant (f)) {
return;
}
pathLengthCurrent++;
retValue = DddmpReadNodeIndexCnf (f);
if ( ((edgeInTh >= 0) && (retValue > edgeInTh)) ||
((pathLengthTh >= 0) && (pathLengthCurrent > pathLengthTh))
) {
DddmpWriteNodeIndexCnfBis (f, 1);
pathLengthCurrent = 0;
} else {
DddmpWriteNodeIndexCnfBis (f, 0);
}
DddmpDdNodesCheckIncomingAndScanPath (cuddT (f), pathLengthCurrent,
edgeInTh, pathLengthTh);
DddmpDdNodesCheckIncomingAndScanPath (cuddE (f), pathLengthCurrent,
edgeInTh, pathLengthTh);
DddmpSetVisitedCnf (f);
return;
}
/**Function********************************************************************
Synopsis [Number nodes recursively in post-order]
Description [Number nodes recursively in post-order.
The "visited" flag is used with the inverse polarity.
Numbering follows the subsequent strategy:
* if the index = 0 it remains so
* if the index >= 1 it gets enumerated.
This implies that the node is assigned to a new CNF variable only if
it is not a terminal node otherwise it is assigned the index of
the BDD variable.
]
SideEffects ["visited" flags are reset.]
SeeAlso []
******************************************************************************/
static int
DddmpDdNodesNumberEdgesRecur (
DdNode *f /* IN: BDD node to be numbered */,
int *cnfIds /* IN: possible source for numbering */,
int id /* IN/OUT: possible source for numbering */
)
{
int retValue;
f = Cudd_Regular(f);
if (!DddmpVisitedCnf (f)) {
return (id);
}
if (cuddIsConstant (f)) {
return (id);
}
id = DddmpDdNodesNumberEdgesRecur (cuddT (f), cnfIds, id);
id = DddmpDdNodesNumberEdgesRecur (cuddE (f), cnfIds, id);
retValue = DddmpReadNodeIndexCnf (f);
if (retValue >= 1) {
id = DddmpWriteNodeIndexCnf (f, cnfIds, id);
} else {
DddmpWriteNodeIndexCnfBis (f, 0);
}
DddmpClearVisitedCnf (f);
return (id);
}
/**Function********************************************************************
Synopsis [Resets counter and visited flag for ALL nodes of a BDD]
Description [Resets counter and visited flag for ALL nodes of a BDD (it
recurs on the node children). The index field of the node is
used as counter.
]
SideEffects []
SeeAlso []
******************************************************************************/
static int
DddmpDdNodesResetCountRecur (
DdNode *f /* IN: root of the BDD whose counters are reset */
)
{
int retValue;
f = Cudd_Regular (f);
if (!DddmpVisitedCnf (f)) {
return (DDDMP_SUCCESS);
}
if (!cuddIsConstant (f)) {
retValue = DddmpDdNodesResetCountRecur (cuddT (f));
retValue = DddmpDdNodesResetCountRecur (cuddE (f));
}
DddmpWriteNodeIndexCnfBis (f, 0);
DddmpClearVisitedCnf (f);
return (DDDMP_SUCCESS);
}
/**Function********************************************************************
Synopsis [Counts the number of incoming edges for each node of a BDD]
Description [Counts (recursively) the number of incoming edges for each
node of a BDD. This number is stored in the index field.
]
SideEffects ["visited" flags remain untouched.]
SeeAlso []
******************************************************************************/
static int
DddmpDdNodesCountEdgesRecur (
DdNode *f /* IN: root of the BDD */
)
{
int indexValue, retValue;
f = Cudd_Regular (f);
if (cuddIsConstant (f)) {
return (DDDMP_SUCCESS);
}
if (Cudd_IsConstant (cuddT (f)) && Cudd_IsConstant (cuddE (f))) {
return (DDDMP_SUCCESS);
}
indexValue = DddmpReadNodeIndexCnf (f);
/* IF (first time) THEN recur */
if (indexValue == 0) {
retValue = DddmpDdNodesCountEdgesRecur (cuddT (f));
retValue = DddmpDdNodesCountEdgesRecur (cuddE (f));
}
/* Increment Incoming-Edge Count Flag */
indexValue++;
DddmpWriteNodeIndexCnfBis (f, indexValue);
return (DDDMP_SUCCESS);
}
/**Function********************************************************************
Synopsis [Removes a node from unique table]
Description [Removes a node from the unique table by locating the proper
subtable and unlinking the node from it. It recurs on son nodes.
]
SideEffects [Nodes are left with the "visited" flag true.]
SeeAlso [RestoreInUniqueRecurCnf()]
******************************************************************************/
static void
RemoveFromUniqueRecurCnf (
DdManager *ddMgr /* IN: DD Manager */,
DdNode *f /* IN: root of the BDD to be extracted */
)
{
DdNode *node, *last, *next;
DdNode *sentinel = &(ddMgr->sentinel);
DdNodePtr *nodelist;
DdSubtable *subtable;
int pos, level;
f = Cudd_Regular (f);
if (DddmpVisitedCnf (f)) {
return;
}
if (!cuddIsConstant (f)) {
RemoveFromUniqueRecurCnf (ddMgr, cuddT (f));
RemoveFromUniqueRecurCnf (ddMgr, cuddE (f));
level = ddMgr->perm[f->index];
subtable = &(ddMgr->subtables[level]);
nodelist = subtable->nodelist;
pos = ddHash (cuddT (f), cuddE (f), subtable->shift);
node = nodelist[pos];
last = NULL;
while (node != sentinel) {
next = node->next;
if (node == f) {
if (last != NULL)
last->next = next;
else
nodelist[pos] = next;
break;
} else {
last = node;
node = next;
}
}
f->next = NULL;
}
DddmpSetVisitedCnf (f);
return;
}
/**Function********************************************************************
Synopsis [Restores a node in unique table]
Description [Restores a node in unique table (recursive)]
SideEffects [Nodes are not restored in the same order as before removal]
SeeAlso [RemoveFromUnique()]
******************************************************************************/
static void
RestoreInUniqueRecurCnf (
DdManager *ddMgr /* IN: DD Manager */,
DdNode *f /* IN: root of the BDD to be restored */
)
{
DdNodePtr *nodelist;
DdNode *T, *E, *looking;
DdNodePtr *previousP;
DdSubtable *subtable;
int pos, level;
#ifdef DDDMP_DEBUG
DdNode *node;
DdNode *sentinel = &(ddMgr->sentinel);
#endif
f = Cudd_Regular(f);
if (!Cudd_IsComplement (f->next)) {
return;
}
if (cuddIsConstant (f)) {
DddmpClearVisitedCnf (f);
/*f->next = NULL;*/
return;
}
RestoreInUniqueRecurCnf (ddMgr, cuddT (f));
RestoreInUniqueRecurCnf (ddMgr, cuddE (f));
level = ddMgr->perm[f->index];
subtable = &(ddMgr->subtables[level]);
nodelist = subtable->nodelist;
pos = ddHash (cuddT (f), cuddE (f), subtable->shift);
#ifdef DDDMP_DEBUG
/* verify uniqueness to avoid duplicate nodes in unique table */
for (node=nodelist[pos]; node != sentinel; node=node->next)
assert(node!=f);
#endif
T = cuddT (f);
E = cuddE (f);
previousP = &(nodelist[pos]);
looking = *previousP;
while (T < cuddT (looking)) {
previousP = &(looking->next);
looking = *previousP;
}
while (T == cuddT (looking) && E < cuddE (looking)) {
previousP = &(looking->next);
looking = *previousP;
}
f->next = *previousP;
*previousP = f;
return;
}
/**Function********************************************************************
Synopsis [Prints debug info]
Description [Prints debug info for a BDD on the screen. It recurs on
node's children.
]
SideEffects []
SeeAlso []
******************************************************************************/
static int
DddmpPrintBddAndNextRecur (
DdManager *ddMgr /* IN: DD Manager */,
DdNode *f /* IN: root of the BDD to be displayed */
)
{
int retValue;
DdNode *fPtr, *tPtr, *ePtr;
fPtr = Cudd_Regular (f);
if (Cudd_IsComplement (f)) {
fprintf (stdout, "sign=- ptr=%ld ", ((long int) fPtr));
} else {
fprintf (stdout, "sign=+ ptr=%ld ", ((long int) fPtr));
}
if (cuddIsConstant (fPtr)) {
fprintf (stdout, "one\n");
fflush (stdout);
return (DDDMP_SUCCESS);
}
fprintf (stdout,
"thenPtr=%ld elsePtr=%ld BddId=%d CnfId=%d Visited=%d\n",
((long int) cuddT (fPtr)), ((long int) cuddE (fPtr)),
fPtr->index, DddmpReadNodeIndexCnf (fPtr),
DddmpVisitedCnf (fPtr));
tPtr = cuddT (fPtr);
ePtr = cuddE (fPtr);
if (Cudd_IsComplement (f)) {
tPtr = Cudd_Not (tPtr);
ePtr = Cudd_Not (ePtr);
}
retValue = DddmpPrintBddAndNextRecur (ddMgr, tPtr);
retValue = DddmpPrintBddAndNextRecur (ddMgr, ePtr);
return (DDDMP_SUCCESS);
}

269
resources/3rdparty/cudd-2.5.0/src/dddmp/exp/runAllTest.out

@ -1,269 +0,0 @@
---------------------------------------------------------------------------
--------------------- TESTING Load and Write Header -----------------------
---------------------------------------------------------------------------
#./../testdddmp Version 2.0.2 (use command help)
TestDddmp> Number of Variables: TestDddmp> File : TestDddmp> DD TYPE: DDDMP_BDD
Number of variables: 50
Number of support variables: 15
suppVarNames: V2 V3 V8 V9 V10 V12 V22 V23 V24 V37 V38 V39 V48 V49 V50
orderedVarNames: V1 V2 V3 V4 V5 V6 V7 V8 V9 V10 V11 V12 V13 V14 V15 V16 V17 V18 V19 V20 V21 V22 V23 V24 V25 V26 V27 V28 V29 V30 V31 V32 V33 V34 V35 V36 V37 V38 V39 V40 V41 V42 V43 V44 V45 V46 V47 V48 V49 V50
varIds: 1 2 7 8 9 11 21 22 23 36 37 38 47 48 49
varIds for ALL Manager Variables: -1 1 2 -1 -1 -1 -1 7 8 9 -1 11 -1 -1 -1 -1 -1 -1 -1 -1 -1 21 22 23 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 36 37 38 -1 -1 -1 -1 -1 -1 -1 -1 47 48 49
varComposeIds: 1 2 7 8 9 11 21 22 23 36 37 38 47 48 49
varComposeIds for ALL Manager Variables: -1 1 2 -1 -1 -1 -1 7 8 9 -1 11 -1 -1 -1 -1 -1 -1 -1 -1 -1 21 22 23 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 36 37 38 -1 -1 -1 -1 -1 -1 -1 -1 47 48 49
varAuxIds: 3 5 15 17 19 23 43 45 47 73 75 77 95 97 99
varAuxIds for ALL Manager Variables: -1 3 5 -1 -1 -1 -1 15 17 19 -1 23 -1 -1 -1 -1 -1 -1 -1 -1 -1 43 45 47 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 73 75 77 -1 -1 -1 -1 -1 -1 -1 -1 95 97 99
Number of roots: 1
TestDddmp> File : TestDddmp> DD TYPE: DDDMP_ADD
Number of variables: 3
Number of support variables: 2
suppVarNames: DUMMY1 DUMMY2
orderedVarNames: DUMMY0 DUMMY1 DUMMY2
varIds: 1 2
varIds for ALL Manager Variables: -1 1 2
varComposeIds: 1 2
varComposeIds for ALL Manager Variables: -1 1 2
varAuxIds: 1 2
varAuxIds for ALL Manager Variables: -1 1 2
Number of roots: 1
TestDddmp> File : TestDddmp> DD TYPE: DDDMP_CNF
Number of variables: 50
Number of support variables: 15
suppVarNames: V2 V3 V8 V9 V10 V12 V22 V23 V24 V37 V38 V39 V48 V49 V50
orderedVarNames: V1 V2 V3 V4 V5 V6 V7 V8 V9 V10 V11 V12 V13 V14 V15 V16 V17 V18 V19 V20 V21 V22 V23 V24 V25 V26 V27 V28 V29 V30 V31 V32 V33 V34 V35 V36 V37 V38 V39 V40 V41 V42 V43 V44 V45 V46 V47 V48 V49 V50
varIds: 1 2 7 8 9 11 21 22 23 36 37 38 47 48 49
varIds for ALL Manager Variables: -1 1 2 -1 -1 -1 -1 7 8 9 -1 11 -1 -1 -1 -1 -1 -1 -1 -1 -1 21 22 23 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 36 37 38 -1 -1 -1 -1 -1 -1 -1 -1 47 48 49
varComposeIds: 1 2 7 8 9 11 21 22 23 36 37 38 47 48 49
varComposeIds for ALL Manager Variables: -1 1 2 -1 -1 -1 -1 7 8 9 -1 11 -1 -1 -1 -1 -1 -1 -1 -1 -1 21 22 23 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 36 37 38 -1 -1 -1 -1 -1 -1 -1 -1 47 48 49
varAuxIds: 1 2 7 8 9 11 21 22 23 36 37 38 47 48 49
varAuxIds for ALL Manager Variables: -1 1 2 -1 -1 -1 -1 7 8 9 -1 11 -1 -1 -1 -1 -1 -1 -1 -1 -1 21 22 23 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 36 37 38 -1 -1 -1 -1 -1 -1 -1 -1 47 48 49
Number of roots: 1
TestDddmp> Quitting CUDD Manager.
TestDddmp> End of test.
-------------------------------- ... END ----------------------------------
rm: No match.
---------------------------------------------------------------------------
-------------------- TESTING Load BDD from DDDMP-1.0 ----------------------
---------------------------------------------------------------------------
#./../testdddmp Version 2.0.2 (use command help)
TestDddmp> Number of Variables: TestDddmp> File : TestDddmp> DD TYPE: DDDMP_BDD
Number of variables: 10
Number of support variables: 7
suppVarNames: G0 G1 G2 G3 G5 G6 G7
orderedVarNames: G0 G1 G2 G3 G5 G6 G7 DUMMY7 DUMMY8 DUMMY9
varIds: 0 1 2 3 4 5 6
varIds for ALL Manager Variables: 0 1 2 3 4 5 6 -1 -1 -1
varComposeIds: 0 1 2 3 4 6 8
varComposeIds for ALL Manager Variables: 0 1 2 3 4 6 8 -1 -1 -1
varAuxIds: 0 1 2 3 4 5 6
varAuxIds for ALL Manager Variables: 0 1 2 3 4 5 6 -1 -1 -1
Number of roots: 3
TestDddmp> File : Which Array of BDDs [0..19]: TestDddmp> File : Which Array of BDDs [0..19]: Storing Array of BDDs in file s27deltaDddmp1.bdd.tmp ...
done.
TestDddmp> Quitting CUDD Manager.
TestDddmp> End of test.
----------------------------- ... RESULTS ... -----------------------------
-------------------------------- ... END ----------------------------------
rm: No match.
---------------------------------------------------------------------------
----------------------- TESTING basic Load/Store ... ----------------------
---------------------------------------------------------------------------
#./../testdddmp Version 2.0.2 (use command help)
TestDddmp> Number of Variables: TestDddmp> File : TestDddmp> File : Which BDDs [0..19]: Loading 0.bdd ...
TestDddmp> File : Which BDDs [0..19]: Loading 1.bdd ...
TestDddmp> Operation [or,and,xor,!,buf(=)] : Source1 [0..19]: Source2 [0..19]: Destination [0..19]: TestDddmp> File : Which BDDs [0..19]: Storing 0or1.bdd.tmp ...
TestDddmp> File : Which BDDs [0..19]: Loading 2.bdd ...
TestDddmp> File : Which BDDs [0..19]: Loading 3.bdd ...
TestDddmp> Operation [or,and,xor,!,buf(=)] : Source1 [0..19]: Source2 [0..19]: Destination [0..19]: TestDddmp> File : Which BDDs [0..19]: Storing 2and3.bdd.tmp ...
TestDddmp> File : TestDddmp> File : Which BDDs [0..19]: Loading 4.bdd ...
TestDddmp> File : Which BDDs [0..19]: Loading 5.bdd ...
TestDddmp> Operation [or,and,xor,!,buf(=)] : Source1 [0..19]: Source2 [0..19]: Destination [0..19]: TestDddmp> File : Which BDDs [0..19]: Storing 4xor5.bdd.tmp ...
TestDddmp> Quitting CUDD Manager.
TestDddmp> End of test.
----------------------------- ... RESULTS ... -----------------------------
-------------------------------- ... END ----------------------------------
rm: No match.
---------------------------------------------------------------------------
---------- TESTING Load/Store with sifting, varnames & varauxids ----------
---------------------------------------------------------------------------
#./../testdddmp Version 2.0.2 (use command help)
TestDddmp> Number of Variables: TestDddmp> File : TestDddmp> File : Which BDDs [0..19]: Loading 4.bdd ...
TestDddmp> File : TestDddmp> File : Which BDDs [0..19]: Storing 4a.bdd.tmp ...
TestDddmp> Reordering Approach (1..17): TestDddmp> File : Which BDDs [0..19]: Storing 4b.bdd.tmp ...
TestDddmp> Quitting CUDD Manager.
TestDddmp> End of test.
------------------------- ... END PHASE 1 ... -----------------------------
#./../testdddmp Version 2.0.2 (use command help)
TestDddmp> Number of Variables: TestDddmp> File : TestDddmp> Variable matchmode:
Match IDs (1)
Match permIDs (2)
Match names (must have been loaded) (3)
Match auxids (must have been loaded) (4)
Match composeids (must have been loaded) (5)
Your choice: TestDddmp> File : Which BDDs [0..19]: Loading 4b.bdd.tmp ...
TestDddmp> File : TestDddmp> File : Which BDDs [0..19]: Storing 4c.bdd.tmp ...
TestDddmp> Quitting CUDD Manager.
TestDddmp> End of test.
----------------------------- ... RESULTS ... -----------------------------
-------------------------------- ... END ----------------------------------
rm: No match.
---------------------------------------------------------------------------
--------------------- TESTING Load ADD and Store ADD ----------------------
---------------------------------------------------------------------------
#./../testdddmp Version 2.0.2 (use command help)
TestDddmp> Number of Variables: TestDddmp> File : TestDddmp> File : Which BDDs [0..19]: Loading 0.add ...
Load:
-01 2
-1- 1
TestDddmp> File : Which BDDs [0..19]: Storing 0.add.tmp ...
TestDddmp> Quitting CUDD Manager.
TestDddmp> Number of Variables: TestDddmp> File : TestDddmp> File : Which BDDs [0..19]: Loading 1.add ...
Load:
-0001--------------------------------------------- 1
-0010--------------------------------------------- 2
-0100--------------------------------------------- 1
-0101--------------------------------------------- 2
-0111--------------------------------------------- 1
-1000--------------------------------------------- 2
-1010--------------------------------------------- 1
-1011--------------------------------------------- 2
-1101--------------------------------------------- 1
-1110--------------------------------------------- 2
TestDddmp> File : Which BDDs [0..19]: Storing 1.add.tmp ...
TestDddmp> Quitting CUDD Manager.
TestDddmp> End of test.
----------------------------- ... RESULTS ... -----------------------------
-------------------------------- ... END ----------------------------------
rm: No match.
---------------------------------------------------------------------------
--------------------- TESTING Load BDD and Store CNF ----------------------
---------------------------------------------------------------------------
#./../testdddmp Version 2.0.2 (use command help)
TestDddmp> Number of Variables: TestDddmp> File : TestDddmp> File : Which BDDs [0..19]: Loading 4.bdd ...
TestDddmp> File : Which BDDs [0..19]: Format (Node=N, Maxterm=M, Best=B) : Initial ID : Storing 4.cnf.tmp ...
Number of Clauses Stored = 108
Number of New Variable Created Storing = 31
TestDddmp> Quitting CUDD Manager.
TestDddmp> End of test.
--------------------- TESTING Load CNF and Store BDD ----------------------
#./../testdddmp Version 2.0.2 (use command help)
TestDddmp> Number of Variables: TestDddmp> File : TestDddmp> File : Which BDDs [0..19]: Loading 4.cnf.tmp ...
TestDddmp> DD TYPE: DDDMP_CNF
Number of variables: 150
Number of support variables: 15
suppVarNames: V3 V8 V23 V24 V37 V39 DUMMY21 DUMMY22 DUMMY23 DUMMY36 DUMMY37 DUMMY38 DUMMY47 DUMMY48 DUMMY49
orderedVarNames: V2 V3 V8 V9 V10 V12 V22 V23 V24 V37 V38 V39 V48 V49 V50 DUMMY15 DUMMY16 DUMMY17 DUMMY18 DUMMY19 DUMMY20 DUMMY21 DUMMY22 DUMMY23 DUMMY24 DUMMY25 DUMMY26 DUMMY27 DUMMY28 DUMMY29 DUMMY30 DUMMY31 DUMMY32 DUMMY33 DUMMY34 DUMMY35 DUMMY36 DUMMY37 DUMMY38 DUMMY39 DUMMY40 DUMMY41 DUMMY42 DUMMY43 DUMMY44 DUMMY45 DUMMY46 DUMMY47 DUMMY48 DUMMY49 DUMMY50 DUMMY51 DUMMY52 DUMMY53 DUMMY54 DUMMY55 DUMMY56 DUMMY57 DUMMY58 DUMMY59 DUMMY60 DUMMY61 DUMMY62 DUMMY63 DUMMY64 DUMMY65 DUMMY66 DUMMY67 DUMMY68 DUMMY69 DUMMY70 DUMMY71 DUMMY72 DUMMY73 DUMMY74 DUMMY75 DUMMY76 DUMMY77 DUMMY78 DUMMY79 DUMMY80 DUMMY81 DUMMY82 DUMMY83 DUMMY84 DUMMY85 DUMMY86 DUMMY87 DUMMY88 DUMMY89 DUMMY90 DUMMY91 DUMMY92 DUMMY93 DUMMY94 DUMMY95 DUMMY96 DUMMY97 DUMMY98 DUMMY99 DUMMY100 DUMMY101 DUMMY102 DUMMY103 DUMMY104 DUMMY105 DUMMY106 DUMMY107 DUMMY108 DUMMY109 DUMMY110 DUMMY111 DUMMY112 DUMMY113 DUMMY114 DUMMY115 DUMMY116 DUMMY117 DUMMY118 DUMMY119 DUMMY120 DUMMY121 DUMMY122 DUMMY123 DUMMY124 DUMMY125 DUMMY126 DUMMY127 DUMMY128 DUMMY129 DUMMY130 DUMMY131 DUMMY132 DUMMY133 DUMMY134 DUMMY135 DUMMY136 DUMMY137 DUMMY138 DUMMY139 DUMMY140 DUMMY141 DUMMY142 DUMMY143 DUMMY144 DUMMY145 DUMMY146 DUMMY147 DUMMY148 DUMMY149
varIds: 1 2 7 8 9 11 21 22 23 36 37 38 47 48 49
varIds for ALL Manager Variables: -1 1 2 -1 -1 -1 -1 7 8 9 -1 11 -1 -1 -1 -1 -1 -1 -1 -1 -1 21 22 23 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 36 37 38 -1 -1 -1 -1 -1 -1 -1 -1 47 48 49 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1
varComposeIds: 1 2 7 8 9 11 21 22 23 36 37 38 47 48 49
varComposeIds for ALL Manager Variables: -1 1 2 -1 -1 -1 -1 7 8 9 -1 11 -1 -1 -1 -1 -1 -1 -1 -1 -1 21 22 23 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 36 37 38 -1 -1 -1 -1 -1 -1 -1 -1 47 48 49 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1
varAuxIds: 1 2 7 8 9 11 21 22 23 36 37 38 47 48 49
varAuxIds for ALL Manager Variables: -1 1 2 -1 -1 -1 -1 7 8 9 -1 11 -1 -1 -1 -1 -1 -1 -1 -1 -1 21 22 23 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 36 37 38 -1 -1 -1 -1 -1 -1 -1 -1 47 48 49 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1
Number of roots: 1
TestDddmp> File : Which BDDs [0..19]: Storing 4.bdd.tmp ...
TestDddmp> Quitting CUDD Manager.
TestDddmp> End of test.
----------------------------- ... RESULTS ... -----------------------------
-------------------------------- ... END ----------------------------------
rm: No match.
---------------------------------------------------------------------------
--------------------- TESTING Load BDD and Store CNF ----------------------
---------------------------------------------------------------------------
#./../testdddmp Version 2.0.2 (use command help)
TestDddmp> Number of Variables: TestDddmp> File : TestDddmp> File : Which BDDs [0..19]: Loading 4.bdd ...
TestDddmp> File : Which BDDs [0..19]: Format (Node=N, Maxterm=M, Best=B) : Initial ID : Storing 4.node1.tmp ...
Number of Clauses Stored = 108
Number of New Variable Created Storing = 31
TestDddmp> File : Which BDDs [0..19]: Format (Node=N, Maxterm=M, Best=B) : Initial ID : Storing 4.max1.tmp ...
Number of Clauses Stored = 103
Number of New Variable Created Storing = 0
TestDddmp> File : Which BDDs [0..19]: Format (Node=N, Maxterm=M, Best=B) : Max Number of Edges (Insert cut-point from there on) : Max BDD-Path Length (Insert cut-point from there on) : Initial ID : Storing 4.node2.tmp ...
Number of Clauses Stored = 114
Number of New Variable Created Storing = 31
TestDddmp> File : Which BDDs [0..19]: Format (Node=N, Maxterm=M, Best=B) : Max Number of Edges (Insert cut-point from there on) : Max BDD-Path Length (Insert cut-point from there on) : Initial ID : Storing 4.node3.tmp ...
Number of Clauses Stored = 108
Number of New Variable Created Storing = 31
TestDddmp> File : Which BDDs [0..19]: Format (Node=N, Maxterm=M, Best=B) : Max Number of Edges (Insert cut-point from there on) : Max BDD-Path Length (Insert cut-point from there on) : Initial ID : Storing 4.max2.tmp ...
Number of Clauses Stored = 103
Number of New Variable Created Storing = 0
TestDddmp> File : Which BDDs [0..19]: Format (Node=N, Maxterm=M, Best=B) : Max Number of Edges (Insert cut-point from there on) : Max BDD-Path Length (Insert cut-point from there on) : Initial ID : Storing 4.best1.tmp ...
Number of Clauses Stored = 53
Number of New Variable Created Storing = 7
TestDddmp> File : Which BDDs [0..19]: Format (Node=N, Maxterm=M, Best=B) : Max Number of Edges (Insert cut-point from there on) : Max BDD-Path Length (Insert cut-point from there on) : Initial ID : Storing 4.best2.tmp ...
Number of Clauses Stored = 69
Number of New Variable Created Storing = 12
TestDddmp> Quitting CUDD Manager.
TestDddmp> End of test.
---------------------------------------------------------------------------
--------------------- TESTING Load CNF and Store BDD ----------------------
---------------------------------------------------------------------------
#./../testdddmp Version 2.0.2 (use command help)
TestDddmp> Number of Variables: TestDddmp> File : TestDddmp> File : Which BDDs [0..19]: Loading 4.node2.tmp ...
TestDddmp> DD TYPE: DDDMP_CNF
Number of variables: 150
Number of support variables: 15
suppVarNames: V3 V8 V23 V24 V37 V39 DUMMY21 DUMMY22 DUMMY23 DUMMY36 DUMMY37 DUMMY38 DUMMY47 DUMMY48 DUMMY49
orderedVarNames: V2 V3 V8 V9 V10 V12 V22 V23 V24 V37 V38 V39 V48 V49 V50 DUMMY15 DUMMY16 DUMMY17 DUMMY18 DUMMY19 DUMMY20 DUMMY21 DUMMY22 DUMMY23 DUMMY24 DUMMY25 DUMMY26 DUMMY27 DUMMY28 DUMMY29 DUMMY30 DUMMY31 DUMMY32 DUMMY33 DUMMY34 DUMMY35 DUMMY36 DUMMY37 DUMMY38 DUMMY39 DUMMY40 DUMMY41 DUMMY42 DUMMY43 DUMMY44 DUMMY45 DUMMY46 DUMMY47 DUMMY48 DUMMY49 DUMMY50 DUMMY51 DUMMY52 DUMMY53 DUMMY54 DUMMY55 DUMMY56 DUMMY57 DUMMY58 DUMMY59 DUMMY60 DUMMY61 DUMMY62 DUMMY63 DUMMY64 DUMMY65 DUMMY66 DUMMY67 DUMMY68 DUMMY69 DUMMY70 DUMMY71 DUMMY72 DUMMY73 DUMMY74 DUMMY75 DUMMY76 DUMMY77 DUMMY78 DUMMY79 DUMMY80 DUMMY81 DUMMY82 DUMMY83 DUMMY84 DUMMY85 DUMMY86 DUMMY87 DUMMY88 DUMMY89 DUMMY90 DUMMY91 DUMMY92 DUMMY93 DUMMY94 DUMMY95 DUMMY96 DUMMY97 DUMMY98 DUMMY99 DUMMY100 DUMMY101 DUMMY102 DUMMY103 DUMMY104 DUMMY105 DUMMY106 DUMMY107 DUMMY108 DUMMY109 DUMMY110 DUMMY111 DUMMY112 DUMMY113 DUMMY114 DUMMY115 DUMMY116 DUMMY117 DUMMY118 DUMMY119 DUMMY120 DUMMY121 DUMMY122 DUMMY123 DUMMY124 DUMMY125 DUMMY126 DUMMY127 DUMMY128 DUMMY129 DUMMY130 DUMMY131 DUMMY132 DUMMY133 DUMMY134 DUMMY135 DUMMY136 DUMMY137 DUMMY138 DUMMY139 DUMMY140 DUMMY141 DUMMY142 DUMMY143 DUMMY144 DUMMY145 DUMMY146 DUMMY147 DUMMY148 DUMMY149
varIds: 1 2 7 8 9 11 21 22 23 36 37 38 47 48 49
varIds for ALL Manager Variables: -1 1 2 -1 -1 -1 -1 7 8 9 -1 11 -1 -1 -1 -1 -1 -1 -1 -1 -1 21 22 23 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 36 37 38 -1 -1 -1 -1 -1 -1 -1 -1 47 48 49 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1
varComposeIds: 1 2 7 8 9 11 21 22 23 36 37 38 47 48 49
varComposeIds for ALL Manager Variables: -1 1 2 -1 -1 -1 -1 7 8 9 -1 11 -1 -1 -1 -1 -1 -1 -1 -1 -1 21 22 23 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 36 37 38 -1 -1 -1 -1 -1 -1 -1 -1 47 48 49 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1
varAuxIds: 1 2 7 8 9 11 21 22 23 36 37 38 47 48 49
varAuxIds for ALL Manager Variables: -1 1 2 -1 -1 -1 -1 7 8 9 -1 11 -1 -1 -1 -1 -1 -1 -1 -1 -1 21 22 23 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 36 37 38 -1 -1 -1 -1 -1 -1 -1 -1 47 48 49 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1
Number of roots: 1
TestDddmp> File : Which BDDs [0..19]: Storing 4.node2.bdd.tmp ...
TestDddmp> Quitting CUDD Manager.
TestDddmp> End of test.
#./../testdddmp Version 2.0.2 (use command help)
TestDddmp> Number of Variables: TestDddmp> File : TestDddmp> File : Which BDDs [0..19]: Loading 4.node3.tmp ...
TestDddmp> DD TYPE: DDDMP_CNF
Number of variables: 150
Number of support variables: 15
suppVarNames: V3 V8 V23 V24 V37 V39 DUMMY21 DUMMY22 DUMMY23 DUMMY36 DUMMY37 DUMMY38 DUMMY47 DUMMY48 DUMMY49
orderedVarNames: V2 V3 V8 V9 V10 V12 V22 V23 V24 V37 V38 V39 V48 V49 V50 DUMMY15 DUMMY16 DUMMY17 DUMMY18 DUMMY19 DUMMY20 DUMMY21 DUMMY22 DUMMY23 DUMMY24 DUMMY25 DUMMY26 DUMMY27 DUMMY28 DUMMY29 DUMMY30 DUMMY31 DUMMY32 DUMMY33 DUMMY34 DUMMY35 DUMMY36 DUMMY37 DUMMY38 DUMMY39 DUMMY40 DUMMY41 DUMMY42 DUMMY43 DUMMY44 DUMMY45 DUMMY46 DUMMY47 DUMMY48 DUMMY49 DUMMY50 DUMMY51 DUMMY52 DUMMY53 DUMMY54 DUMMY55 DUMMY56 DUMMY57 DUMMY58 DUMMY59 DUMMY60 DUMMY61 DUMMY62 DUMMY63 DUMMY64 DUMMY65 DUMMY66 DUMMY67 DUMMY68 DUMMY69 DUMMY70 DUMMY71 DUMMY72 DUMMY73 DUMMY74 DUMMY75 DUMMY76 DUMMY77 DUMMY78 DUMMY79 DUMMY80 DUMMY81 DUMMY82 DUMMY83 DUMMY84 DUMMY85 DUMMY86 DUMMY87 DUMMY88 DUMMY89 DUMMY90 DUMMY91 DUMMY92 DUMMY93 DUMMY94 DUMMY95 DUMMY96 DUMMY97 DUMMY98 DUMMY99 DUMMY100 DUMMY101 DUMMY102 DUMMY103 DUMMY104 DUMMY105 DUMMY106 DUMMY107 DUMMY108 DUMMY109 DUMMY110 DUMMY111 DUMMY112 DUMMY113 DUMMY114 DUMMY115 DUMMY116 DUMMY117 DUMMY118 DUMMY119 DUMMY120 DUMMY121 DUMMY122 DUMMY123 DUMMY124 DUMMY125 DUMMY126 DUMMY127 DUMMY128 DUMMY129 DUMMY130 DUMMY131 DUMMY132 DUMMY133 DUMMY134 DUMMY135 DUMMY136 DUMMY137 DUMMY138 DUMMY139 DUMMY140 DUMMY141 DUMMY142 DUMMY143 DUMMY144 DUMMY145 DUMMY146 DUMMY147 DUMMY148 DUMMY149
varIds: 1 2 7 8 9 11 21 22 23 36 37 38 47 48 49
varIds for ALL Manager Variables: -1 1 2 -1 -1 -1 -1 7 8 9 -1 11 -1 -1 -1 -1 -1 -1 -1 -1 -1 21 22 23 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 36 37 38 -1 -1 -1 -1 -1 -1 -1 -1 47 48 49 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1
varComposeIds: 1 2 7 8 9 11 21 22 23 36 37 38 47 48 49
varComposeIds for ALL Manager Variables: -1 1 2 -1 -1 -1 -1 7 8 9 -1 11 -1 -1 -1 -1 -1 -1 -1 -1 -1 21 22 23 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 36 37 38 -1 -1 -1 -1 -1 -1 -1 -1 47 48 49 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1
varAuxIds: 1 2 7 8 9 11 21 22 23 36 37 38 47 48 49
varAuxIds for ALL Manager Variables: -1 1 2 -1 -1 -1 -1 7 8 9 -1 11 -1 -1 -1 -1 -1 -1 -1 -1 -1 21 22 23 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 36 37 38 -1 -1 -1 -1 -1 -1 -1 -1 47 48 49 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1
Number of roots: 1
TestDddmp> File : Which BDDs [0..19]: Storing 4.node3.bdd.tmp ...
TestDddmp> Quitting CUDD Manager.
TestDddmp> End of test.
#./../testdddmp Version 2.0.2 (use command help)
TestDddmp> Number of Variables: TestDddmp> File : TestDddmp> File : Which BDDs [0..19]: Loading 4.best1.tmp ...
TestDddmp> DD TYPE: DDDMP_CNF
Number of variables: 150
Number of support variables: 15
suppVarNames: V3 V8 V23 V24 V37 V39 DUMMY21 DUMMY22 DUMMY23 DUMMY36 DUMMY37 DUMMY38 DUMMY47 DUMMY48 DUMMY49
orderedVarNames: V2 V3 V8 V9 V10 V12 V22 V23 V24 V37 V38 V39 V48 V49 V50 DUMMY15 DUMMY16 DUMMY17 DUMMY18 DUMMY19 DUMMY20 DUMMY21 DUMMY22 DUMMY23 DUMMY24 DUMMY25 DUMMY26 DUMMY27 DUMMY28 DUMMY29 DUMMY30 DUMMY31 DUMMY32 DUMMY33 DUMMY34 DUMMY35 DUMMY36 DUMMY37 DUMMY38 DUMMY39 DUMMY40 DUMMY41 DUMMY42 DUMMY43 DUMMY44 DUMMY45 DUMMY46 DUMMY47 DUMMY48 DUMMY49 DUMMY50 DUMMY51 DUMMY52 DUMMY53 DUMMY54 DUMMY55 DUMMY56 DUMMY57 DUMMY58 DUMMY59 DUMMY60 DUMMY61 DUMMY62 DUMMY63 DUMMY64 DUMMY65 DUMMY66 DUMMY67 DUMMY68 DUMMY69 DUMMY70 DUMMY71 DUMMY72 DUMMY73 DUMMY74 DUMMY75 DUMMY76 DUMMY77 DUMMY78 DUMMY79 DUMMY80 DUMMY81 DUMMY82 DUMMY83 DUMMY84 DUMMY85 DUMMY86 DUMMY87 DUMMY88 DUMMY89 DUMMY90 DUMMY91 DUMMY92 DUMMY93 DUMMY94 DUMMY95 DUMMY96 DUMMY97 DUMMY98 DUMMY99 DUMMY100 DUMMY101 DUMMY102 DUMMY103 DUMMY104 DUMMY105 DUMMY106 DUMMY107 DUMMY108 DUMMY109 DUMMY110 DUMMY111 DUMMY112 DUMMY113 DUMMY114 DUMMY115 DUMMY116 DUMMY117 DUMMY118 DUMMY119 DUMMY120 DUMMY121 DUMMY122 DUMMY123 DUMMY124 DUMMY125 DUMMY126 DUMMY127 DUMMY128 DUMMY129 DUMMY130 DUMMY131 DUMMY132 DUMMY133 DUMMY134 DUMMY135 DUMMY136 DUMMY137 DUMMY138 DUMMY139 DUMMY140 DUMMY141 DUMMY142 DUMMY143 DUMMY144 DUMMY145 DUMMY146 DUMMY147 DUMMY148 DUMMY149
varIds: 1 2 7 8 9 11 21 22 23 36 37 38 47 48 49
varIds for ALL Manager Variables: -1 1 2 -1 -1 -1 -1 7 8 9 -1 11 -1 -1 -1 -1 -1 -1 -1 -1 -1 21 22 23 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 36 37 38 -1 -1 -1 -1 -1 -1 -1 -1 47 48 49 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1
varComposeIds: 1 2 7 8 9 11 21 22 23 36 37 38 47 48 49
varComposeIds for ALL Manager Variables: -1 1 2 -1 -1 -1 -1 7 8 9 -1 11 -1 -1 -1 -1 -1 -1 -1 -1 -1 21 22 23 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 36 37 38 -1 -1 -1 -1 -1 -1 -1 -1 47 48 49 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1
varAuxIds: 1 2 7 8 9 11 21 22 23 36 37 38 47 48 49
varAuxIds for ALL Manager Variables: -1 1 2 -1 -1 -1 -1 7 8 9 -1 11 -1 -1 -1 -1 -1 -1 -1 -1 -1 21 22 23 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 36 37 38 -1 -1 -1 -1 -1 -1 -1 -1 47 48 49 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1
Number of roots: 1
TestDddmp> File : Which BDDs [0..19]: Storing 4.best1.bdd.tmp ...
TestDddmp> Quitting CUDD Manager.
TestDddmp> End of test.
#./../testdddmp Version 2.0.2 (use command help)
TestDddmp> Number of Variables: TestDddmp> File : TestDddmp> File : Which BDDs [0..19]: Loading 4.best2.tmp ...
TestDddmp> DD TYPE: DDDMP_CNF
Number of variables: 150
Number of support variables: 15
suppVarNames: V3 V8 V23 V24 V37 V39 DUMMY21 DUMMY22 DUMMY23 DUMMY36 DUMMY37 DUMMY38 DUMMY47 DUMMY48 DUMMY49
orderedVarNames: V2 V3 V8 V9 V10 V12 V22 V23 V24 V37 V38 V39 V48 V49 V50 DUMMY15 DUMMY16 DUMMY17 DUMMY18 DUMMY19 DUMMY20 DUMMY21 DUMMY22 DUMMY23 DUMMY24 DUMMY25 DUMMY26 DUMMY27 DUMMY28 DUMMY29 DUMMY30 DUMMY31 DUMMY32 DUMMY33 DUMMY34 DUMMY35 DUMMY36 DUMMY37 DUMMY38 DUMMY39 DUMMY40 DUMMY41 DUMMY42 DUMMY43 DUMMY44 DUMMY45 DUMMY46 DUMMY47 DUMMY48 DUMMY49 DUMMY50 DUMMY51 DUMMY52 DUMMY53 DUMMY54 DUMMY55 DUMMY56 DUMMY57 DUMMY58 DUMMY59 DUMMY60 DUMMY61 DUMMY62 DUMMY63 DUMMY64 DUMMY65 DUMMY66 DUMMY67 DUMMY68 DUMMY69 DUMMY70 DUMMY71 DUMMY72 DUMMY73 DUMMY74 DUMMY75 DUMMY76 DUMMY77 DUMMY78 DUMMY79 DUMMY80 DUMMY81 DUMMY82 DUMMY83 DUMMY84 DUMMY85 DUMMY86 DUMMY87 DUMMY88 DUMMY89 DUMMY90 DUMMY91 DUMMY92 DUMMY93 DUMMY94 DUMMY95 DUMMY96 DUMMY97 DUMMY98 DUMMY99 DUMMY100 DUMMY101 DUMMY102 DUMMY103 DUMMY104 DUMMY105 DUMMY106 DUMMY107 DUMMY108 DUMMY109 DUMMY110 DUMMY111 DUMMY112 DUMMY113 DUMMY114 DUMMY115 DUMMY116 DUMMY117 DUMMY118 DUMMY119 DUMMY120 DUMMY121 DUMMY122 DUMMY123 DUMMY124 DUMMY125 DUMMY126 DUMMY127 DUMMY128 DUMMY129 DUMMY130 DUMMY131 DUMMY132 DUMMY133 DUMMY134 DUMMY135 DUMMY136 DUMMY137 DUMMY138 DUMMY139 DUMMY140 DUMMY141 DUMMY142 DUMMY143 DUMMY144 DUMMY145 DUMMY146 DUMMY147 DUMMY148 DUMMY149
varIds: 1 2 7 8 9 11 21 22 23 36 37 38 47 48 49
varIds for ALL Manager Variables: -1 1 2 -1 -1 -1 -1 7 8 9 -1 11 -1 -1 -1 -1 -1 -1 -1 -1 -1 21 22 23 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 36 37 38 -1 -1 -1 -1 -1 -1 -1 -1 47 48 49 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1
varComposeIds: 1 2 7 8 9 11 21 22 23 36 37 38 47 48 49
varComposeIds for ALL Manager Variables: -1 1 2 -1 -1 -1 -1 7 8 9 -1 11 -1 -1 -1 -1 -1 -1 -1 -1 -1 21 22 23 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 36 37 38 -1 -1 -1 -1 -1 -1 -1 -1 47 48 49 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1
varAuxIds: 1 2 7 8 9 11 21 22 23 36 37 38 47 48 49
varAuxIds for ALL Manager Variables: -1 1 2 -1 -1 -1 -1 7 8 9 -1 11 -1 -1 -1 -1 -1 -1 -1 -1 -1 21 22 23 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 36 37 38 -1 -1 -1 -1 -1 -1 -1 -1 47 48 49 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1
Number of roots: 1
TestDddmp> File : Which BDDs [0..19]: Storing 4.best2.bdd.tmp ...
TestDddmp> Quitting CUDD Manager.
TestDddmp> End of test.
----------------------------- ... RESULTS ... -----------------------------
-------------------------------- ... END ----------------------------------

11
resources/3rdparty/cudd-2.5.0/src/dddmp/exp/runAllTest.script

@ -1,11 +0,0 @@
# !/bin/sh
#
# Run All Test Files
#
./test1.script
./test2.script
./test3.script
./test4.script
./test5.script
./test6.script
./test7.script

44
resources/3rdparty/cudd-2.5.0/src/dddmp/exp/test1.out

@ -1,44 +0,0 @@
rm: No match.
---------------------------------------------------------------------------
--------------------- TESTING Load and Write Header -----------------------
---------------------------------------------------------------------------
#./../testdddmp Version 2.0.2 (use command help)
TestDddmp> Number of Variables: TestDddmp> File : TestDddmp> DD TYPE: DDDMP_BDD
Number of variables: 50
Number of support variables: 15
suppVarNames: V2 V3 V8 V9 V10 V12 V22 V23 V24 V37 V38 V39 V48 V49 V50
orderedVarNames: V1 V2 V3 V4 V5 V6 V7 V8 V9 V10 V11 V12 V13 V14 V15 V16 V17 V18 V19 V20 V21 V22 V23 V24 V25 V26 V27 V28 V29 V30 V31 V32 V33 V34 V35 V36 V37 V38 V39 V40 V41 V42 V43 V44 V45 V46 V47 V48 V49 V50
varIds: 1 2 7 8 9 11 21 22 23 36 37 38 47 48 49
varIds for ALL Manager Variables: -1 1 2 -1 -1 -1 -1 7 8 9 -1 11 -1 -1 -1 -1 -1 -1 -1 -1 -1 21 22 23 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 36 37 38 -1 -1 -1 -1 -1 -1 -1 -1 47 48 49
varComposeIds: 1 2 7 8 9 11 21 22 23 36 37 38 47 48 49
varComposeIds for ALL Manager Variables: -1 1 2 -1 -1 -1 -1 7 8 9 -1 11 -1 -1 -1 -1 -1 -1 -1 -1 -1 21 22 23 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 36 37 38 -1 -1 -1 -1 -1 -1 -1 -1 47 48 49
varAuxIds: 3 5 15 17 19 23 43 45 47 73 75 77 95 97 99
varAuxIds for ALL Manager Variables: -1 3 5 -1 -1 -1 -1 15 17 19 -1 23 -1 -1 -1 -1 -1 -1 -1 -1 -1 43 45 47 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 73 75 77 -1 -1 -1 -1 -1 -1 -1 -1 95 97 99
Number of roots: 1
TestDddmp> File : TestDddmp> DD TYPE: DDDMP_ADD
Number of variables: 3
Number of support variables: 2
suppVarNames: DUMMY1 DUMMY2
orderedVarNames: DUMMY0 DUMMY1 DUMMY2
varIds: 1 2
varIds for ALL Manager Variables: -1 1 2
varComposeIds: 1 2
varComposeIds for ALL Manager Variables: -1 1 2
varAuxIds: 1 2
varAuxIds for ALL Manager Variables: -1 1 2
Number of roots: 1
TestDddmp> File : TestDddmp> DD TYPE: DDDMP_CNF
Number of variables: 50
Number of support variables: 15
suppVarNames: V2 V3 V8 V9 V10 V12 V22 V23 V24 V37 V38 V39 V48 V49 V50
orderedVarNames: V1 V2 V3 V4 V5 V6 V7 V8 V9 V10 V11 V12 V13 V14 V15 V16 V17 V18 V19 V20 V21 V22 V23 V24 V25 V26 V27 V28 V29 V30 V31 V32 V33 V34 V35 V36 V37 V38 V39 V40 V41 V42 V43 V44 V45 V46 V47 V48 V49 V50
varIds: 1 2 7 8 9 11 21 22 23 36 37 38 47 48 49
varIds for ALL Manager Variables: -1 1 2 -1 -1 -1 -1 7 8 9 -1 11 -1 -1 -1 -1 -1 -1 -1 -1 -1 21 22 23 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 36 37 38 -1 -1 -1 -1 -1 -1 -1 -1 47 48 49
varComposeIds: 1 2 7 8 9 11 21 22 23 36 37 38 47 48 49
varComposeIds for ALL Manager Variables: -1 1 2 -1 -1 -1 -1 7 8 9 -1 11 -1 -1 -1 -1 -1 -1 -1 -1 -1 21 22 23 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 36 37 38 -1 -1 -1 -1 -1 -1 -1 -1 47 48 49
varAuxIds: 1 2 7 8 9 11 21 22 23 36 37 38 47 48 49
varAuxIds for ALL Manager Variables: -1 1 2 -1 -1 -1 -1 7 8 9 -1 11 -1 -1 -1 -1 -1 -1 -1 -1 -1 21 22 23 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 36 37 38 -1 -1 -1 -1 -1 -1 -1 -1 47 48 49
Number of roots: 1
TestDddmp> Quitting CUDD Manager.
TestDddmp> End of test.
-------------------------------- ... END ----------------------------------

23
resources/3rdparty/cudd-2.5.0/src/dddmp/exp/test2.out

@ -1,23 +0,0 @@
rm: No match.
---------------------------------------------------------------------------
-------------------- TESTING Load BDD from DDDMP-1.0 ----------------------
---------------------------------------------------------------------------
#./../testdddmp Version 2.0.2 (use command help)
TestDddmp> Number of Variables: TestDddmp> File : TestDddmp> DD TYPE: DDDMP_BDD
Number of variables: 10
Number of support variables: 7
suppVarNames: G0 G1 G2 G3 G5 G6 G7
orderedVarNames: G0 G1 G2 G3 G5 G6 G7 DUMMY7 DUMMY8 DUMMY9
varIds: 0 1 2 3 4 5 6
varIds for ALL Manager Variables: 0 1 2 3 4 5 6 -1 -1 -1
varComposeIds: 0 1 2 3 4 6 8
varComposeIds for ALL Manager Variables: 0 1 2 3 4 6 8 -1 -1 -1
varAuxIds: 0 1 2 3 4 5 6
varAuxIds for ALL Manager Variables: 0 1 2 3 4 5 6 -1 -1 -1
Number of roots: 3
TestDddmp> File : Which Array of BDDs [0..19]: TestDddmp> File : Which Array of BDDs [0..19]: Storing Array of BDDs in file s27deltaDddmp1.bdd.tmp ...
done.
TestDddmp> Quitting CUDD Manager.
TestDddmp> End of test.
----------------------------- ... RESULTS ... -----------------------------
-------------------------------- ... END ----------------------------------

18
resources/3rdparty/cudd-2.5.0/src/dddmp/exp/test3.out

@ -1,18 +0,0 @@
rm: No match.
---------------------------------------------------------------------------
----------------------- TESTING basic Load/Store ... ----------------------
---------------------------------------------------------------------------
#./../testdddmp Version 2.0.2 (use command help)
TestDddmp> Number of Variables: TestDddmp> File : TestDddmp> File : Which BDDs [0..19]: Loading 0.bdd ...
TestDddmp> File : Which BDDs [0..19]: Loading 1.bdd ...
TestDddmp> Operation [or,and,xor,!,buf(=)] : Source1 [0..19]: Source2 [0..19]: Destination [0..19]: TestDddmp> File : Which BDDs [0..19]: Storing 0or1.bdd.tmp ...
TestDddmp> File : Which BDDs [0..19]: Loading 2.bdd ...
TestDddmp> File : Which BDDs [0..19]: Loading 3.bdd ...
TestDddmp> Operation [or,and,xor,!,buf(=)] : Source1 [0..19]: Source2 [0..19]: Destination [0..19]: TestDddmp> File : Which BDDs [0..19]: Storing 2and3.bdd.tmp ...
TestDddmp> File : TestDddmp> File : Which BDDs [0..19]: Loading 4.bdd ...
TestDddmp> File : Which BDDs [0..19]: Loading 5.bdd ...
TestDddmp> Operation [or,and,xor,!,buf(=)] : Source1 [0..19]: Source2 [0..19]: Destination [0..19]: TestDddmp> File : Which BDDs [0..19]: Storing 4xor5.bdd.tmp ...
TestDddmp> Quitting CUDD Manager.
TestDddmp> End of test.
----------------------------- ... RESULTS ... -----------------------------
-------------------------------- ... END ----------------------------------

69
resources/3rdparty/cudd-2.5.0/src/dddmp/exp/test3.script

@ -1,69 +0,0 @@
# !/bin/sh
#
# BDD check:
# Load BDDs
# Make some operations
# Store BDDs
#
rm -f *.*.tmp
echo "---------------------------------------------------------------------------"
echo "----------------------- TESTING basic Load/Store ... ----------------------"
echo "---------------------------------------------------------------------------"
./../testdddmp << END
mi
50
hlb
0or1.bdd
bl
0.bdd
0
bl
1.bdd
1
op
or
0
1
2
bs
0or1.bdd.tmp
2
bl
2.bdd
2
bl
3.bdd
3
op
and
2
3
4
bs
2and3.bdd.tmp
4
hlb
4xor5.bdd
bl
4.bdd
4
bl
5.bdd
5
op
xor
4
5
6
bs
4xor5.bdd.tmp
6
mq
quit
END
echo "----------------------------- ... RESULTS ... -----------------------------"
diff --brief 0or1.bdd 0or1.bdd.tmp
diff --brief 2and3.bdd 2and3.bdd.tmp
diff --brief 4xor5.bdd 4xor5.bdd.tmp
echo "-------------------------------- ... END ----------------------------------"
rm -f *.*.tmp

24
resources/3rdparty/cudd-2.5.0/src/dddmp/exp/test4.out

@ -1,24 +0,0 @@
rm: No match.
---------------------------------------------------------------------------
---------- TESTING Load/Store with sifting, varnames & varauxids ----------
---------------------------------------------------------------------------
#./../testdddmp Version 2.0.2 (use command help)
TestDddmp> Number of Variables: TestDddmp> File : TestDddmp> File : Which BDDs [0..19]: Loading 4.bdd ...
TestDddmp> File : TestDddmp> File : Which BDDs [0..19]: Storing 4a.bdd.tmp ...
TestDddmp> Reordering Approach (1..17): TestDddmp> File : Which BDDs [0..19]: Storing 4b.bdd.tmp ...
TestDddmp> Quitting CUDD Manager.
TestDddmp> End of test.
------------------------- ... END PHASE 1 ... -----------------------------
#./../testdddmp Version 2.0.2 (use command help)
TestDddmp> Number of Variables: TestDddmp> File : TestDddmp> Variable matchmode:
Match IDs (1)
Match permIDs (2)
Match names (must have been loaded) (3)
Match auxids (must have been loaded) (4)
Match composeids (must have been loaded) (5)
Your choice: TestDddmp> File : Which BDDs [0..19]: Loading 4b.bdd.tmp ...
TestDddmp> File : TestDddmp> File : Which BDDs [0..19]: Storing 4c.bdd.tmp ...
TestDddmp> Quitting CUDD Manager.
TestDddmp> End of test.
----------------------------- ... RESULTS ... -----------------------------
-------------------------------- ... END ----------------------------------

Some files were not shown because too many files changed in this diff

|||||||
100:0
Loading…
Cancel
Save