Browse Source

started making cudd3 work

Former-commit-id: bc791536bb
tempestpy_adaptions
dehnert 9 years ago
parent
commit
97d9ecccbb
  1. 23
      resources/3rdparty/cudd-3.0.0/Makefile.am
  2. 154
      resources/3rdparty/cudd-3.0.0/Makefile.in
  3. 66
      resources/3rdparty/cudd-3.0.0/aclocal.m4
  4. 12
      resources/3rdparty/cudd-3.0.0/configure
  5. 26
      resources/3rdparty/cudd-3.0.0/cplusplus/cuddObj.cc
  6. 6
      resources/3rdparty/cudd-3.0.0/cplusplus/cuddObj.hh
  7. 6
      resources/3rdparty/cudd-3.0.0/cudd/cudd.h
  8. 49
      resources/3rdparty/cudd-3.0.0/cudd/cuddAPI.c
  9. 3
      src/models/symbolic/Model.cpp
  10. 8
      src/storage/dd/cudd/InternalCuddAdd.cpp
  11. 18
      src/storage/dd/cudd/InternalCuddBdd.cpp

23
resources/3rdparty/cudd-3.0.0/Makefile.am

@ -1,6 +1,7 @@
ACLOCAL_AMFLAGS = -I m4
include_HEADERS = cudd/cudd.h
include_HEADERS += mtr/mtr.h
if DDDMP
include_HEADERS += dddmp/dddmp.h
endif
@ -39,19 +40,19 @@ dist-hook:
all: html/index.html doc/cudd.pdf
if HAVE_DOXYGEN
html/index.html: Doxyfile $(lib_LTLIBRARIES)
@if $(AM_V_P); then dest='2>&1'; else dest='> /dev/null 2>&1'; fi; \
eval "$(DOXYGEN) $< $${dest}"
clean-local:
rm -rf html doxygen_sqlite3.db
else
#if HAVE_DOXYGEN
#
#html/index.html: Doxyfile $(lib_LTLIBRARIES)
# @if $(AM_V_P); then dest='2>&1'; else dest='> /dev/null 2>&1'; fi; \
# eval "$(DOXYGEN) $< $${dest}"
#
#clean-local:
# rm -rf html doxygen_sqlite3.db
#
#else
html/index.html:
endif
#endif
CLEANFILES += $(check_SCRIPTS)

154
resources/3rdparty/cudd-3.0.0/Makefile.in

@ -1,7 +1,7 @@
# Makefile.in generated by automake 1.14.1 from Makefile.am.
# Makefile.in generated by automake 1.15 from Makefile.am.
# @configure_input@
# Copyright (C) 1994-2013 Free Software Foundation, Inc.
# Copyright (C) 1994-2014 Free Software Foundation, Inc.
# This Makefile.in is free software; the Free Software Foundation
# gives unlimited permission to copy and/or distribute it,
@ -16,7 +16,17 @@
VPATH = @srcdir@
am__is_gnu_make = test -n '$(MAKEFILE_LIST)' && test -n '$(MAKELEVEL)'
am__is_gnu_make = { \
if test -z '$(MAKELEVEL)'; then \
false; \
elif test -n '$(MAKE_HOST)'; then \
true; \
elif test -n '$(MAKE_VERSION)' && test -n '$(CURDIR)'; then \
true; \
else \
false; \
fi; \
}
am__make_running_with_option = \
case $${target_option-} in \
?) ;; \
@ -85,35 +95,6 @@ check_PROGRAMS = cudd/testcudd$(EXEEXT) cudd/testextra$(EXEEXT) \
st/testst$(EXEEXT) mtr/testmtr$(EXEEXT) \
dddmp/testdddmp$(EXEEXT) cplusplus/testobj$(EXEEXT) \
cplusplus/testmulti$(EXEEXT) nanotrav/nanotrav$(EXEEXT)
DIST_COMMON = $(top_srcdir)/cudd/Included.am \
$(top_srcdir)/util/Included.am $(top_srcdir)/st/Included.am \
$(top_srcdir)/epd/Included.am $(top_srcdir)/mtr/Included.am \
$(top_srcdir)/dddmp/Included.am \
$(top_srcdir)/cplusplus/Included.am \
$(top_srcdir)/nanotrav/Included.am \
$(top_srcdir)/doc/Included.am $(srcdir)/Makefile.in \
$(srcdir)/Makefile.am $(top_srcdir)/configure \
$(am__configure_deps) $(srcdir)/config.h.in \
$(srcdir)/Doxyfile.in $(top_srcdir)/doc/cudd.tex.in \
$(top_srcdir)/dddmp/exp/test1.sh.in \
$(top_srcdir)/dddmp/exp/test2.sh.in \
$(top_srcdir)/dddmp/exp/test3.sh.in \
$(top_srcdir)/dddmp/exp/test4.sh.in \
$(top_srcdir)/dddmp/exp/test5.sh.in \
$(top_srcdir)/dddmp/exp/test6.sh.in \
$(top_srcdir)/dddmp/exp/test7.sh.in \
$(top_srcdir)/build-aux/depcomp $(dist_check_DATA) \
$(am__include_HEADERS_DIST) README build-aux/ar-lib \
build-aux/compile build-aux/config.guess build-aux/config.sub \
build-aux/depcomp build-aux/install-sh build-aux/missing \
build-aux/ltmain.sh $(top_srcdir)/build-aux/ar-lib \
$(top_srcdir)/build-aux/compile \
$(top_srcdir)/build-aux/config.guess \
$(top_srcdir)/build-aux/config.sub \
$(top_srcdir)/build-aux/install-sh \
$(top_srcdir)/build-aux/ltmain.sh \
$(top_srcdir)/build-aux/missing \
$(top_srcdir)/build-aux/tap-driver.sh
@CROSS_COMPILING_FALSE@am__append_3 = cudd/test_cudd.test \
@CROSS_COMPILING_FALSE@ st/test_st.test mtr/test_mtr.test \
@CROSS_COMPILING_FALSE@ dddmp/test_dddmp.test \
@ -135,6 +116,9 @@ am__aclocal_m4_deps = $(top_srcdir)/m4/libtool.m4 \
$(top_srcdir)/configure.ac
am__configure_deps = $(am__aclocal_m4_deps) $(CONFIGURE_DEPENDENCIES) \
$(ACLOCAL_M4)
DIST_COMMON = $(srcdir)/Makefile.am $(top_srcdir)/configure \
$(am__configure_deps) $(dist_check_DATA) \
$(am__include_HEADERS_DIST) $(am__DIST_COMMON)
am__CONFIG_DISTCLEAN_FILES = config.status config.cache config.log \
configure.lineno config.status.lineno
mkinstalldirs = $(install_sh) -d
@ -455,7 +439,7 @@ am__can_run_installinfo = \
n|no|NO) false;; \
*) (install-info --version) >/dev/null 2>&1;; \
esac
am__include_HEADERS_DIST = cudd/cudd.h dddmp/dddmp.h \
am__include_HEADERS_DIST = cudd/cudd.h mtr/mtr.h dddmp/dddmp.h \
cplusplus/cuddObj.hh
HEADERS = $(include_HEADERS)
am__tagged_files = $(HEADERS) $(SOURCES) $(TAGS_FILES) \
@ -653,6 +637,32 @@ am__set_b = \
*) \
b='$*';; \
esac
am__DIST_COMMON = $(srcdir)/Doxyfile.in $(srcdir)/Makefile.in \
$(srcdir)/config.h.in $(top_srcdir)/build-aux/ar-lib \
$(top_srcdir)/build-aux/compile \
$(top_srcdir)/build-aux/config.guess \
$(top_srcdir)/build-aux/config.sub \
$(top_srcdir)/build-aux/depcomp \
$(top_srcdir)/build-aux/install-sh \
$(top_srcdir)/build-aux/ltmain.sh \
$(top_srcdir)/build-aux/missing \
$(top_srcdir)/build-aux/tap-driver.sh \
$(top_srcdir)/cplusplus/Included.am \
$(top_srcdir)/cudd/Included.am $(top_srcdir)/dddmp/Included.am \
$(top_srcdir)/dddmp/exp/test1.sh.in \
$(top_srcdir)/dddmp/exp/test2.sh.in \
$(top_srcdir)/dddmp/exp/test3.sh.in \
$(top_srcdir)/dddmp/exp/test4.sh.in \
$(top_srcdir)/dddmp/exp/test5.sh.in \
$(top_srcdir)/dddmp/exp/test6.sh.in \
$(top_srcdir)/dddmp/exp/test7.sh.in \
$(top_srcdir)/doc/Included.am $(top_srcdir)/doc/cudd.tex.in \
$(top_srcdir)/epd/Included.am $(top_srcdir)/mtr/Included.am \
$(top_srcdir)/nanotrav/Included.am \
$(top_srcdir)/st/Included.am $(top_srcdir)/util/Included.am \
README build-aux/ar-lib build-aux/compile \
build-aux/config.guess build-aux/config.sub build-aux/depcomp \
build-aux/install-sh build-aux/ltmain.sh build-aux/missing
DISTFILES = $(DIST_COMMON) $(DIST_SOURCES) $(TEXINFOS) $(EXTRA_DIST)
distdir = $(PACKAGE)-$(VERSION)
top_distdir = $(distdir)
@ -794,7 +804,8 @@ top_build_prefix = @top_build_prefix@
top_builddir = @top_builddir@
top_srcdir = @top_srcdir@
ACLOCAL_AMFLAGS = -I m4
include_HEADERS = cudd/cudd.h $(am__append_1) $(am__append_2)
include_HEADERS = cudd/cudd.h mtr/mtr.h $(am__append_1) \
$(am__append_2)
check_SCRIPTS = cudd/test_cudd.test st/test_st.test mtr/test_mtr.test \
dddmp/test_dddmp.test cplusplus/test_obj.test \
nanotrav/test_ntrv.test
@ -830,6 +841,8 @@ EXTRA_DIST = README RELEASE.NOTES LICENSE groups.dox \
dddmp/exp/zero.bdd cplusplus/test_obj.test.in nanotrav/README \
nanotrav/nanotrav.1 nanotrav/test_ntrv.test.in doc/phase.pdf
TESTS = $(am__append_3)
#endif
CLEANFILES = cudd/r7x8.1.tst cudd/extra.tst mtr/test.tst \
dddmp/exp/test1.sh dddmp/exp/test2.sh dddmp/exp/test3.sh \
dddmp/exp/test4.sh dddmp/exp/test5.sh dddmp/exp/test6.sh \
@ -962,7 +975,6 @@ $(srcdir)/Makefile.in: $(srcdir)/Makefile.am $(top_srcdir)/cudd/Included.am $(t
echo ' cd $(top_srcdir) && $(AUTOMAKE) --foreign Makefile'; \
$(am__cd) $(top_srcdir) && \
$(AUTOMAKE) --foreign Makefile
.PRECIOUS: Makefile
Makefile: $(srcdir)/Makefile.in $(top_builddir)/config.status
@case '$?' in \
*config.status*) \
@ -972,7 +984,7 @@ Makefile: $(srcdir)/Makefile.in $(top_builddir)/config.status
echo ' cd $(top_builddir) && $(SHELL) ./config.status $@ $(am__depfiles_maybe)'; \
cd $(top_builddir) && $(SHELL) ./config.status $@ $(am__depfiles_maybe);; \
esac;
$(top_srcdir)/cudd/Included.am $(top_srcdir)/util/Included.am $(top_srcdir)/st/Included.am $(top_srcdir)/epd/Included.am $(top_srcdir)/mtr/Included.am $(top_srcdir)/dddmp/Included.am $(top_srcdir)/cplusplus/Included.am $(top_srcdir)/nanotrav/Included.am $(top_srcdir)/doc/Included.am:
$(top_srcdir)/cudd/Included.am $(top_srcdir)/util/Included.am $(top_srcdir)/st/Included.am $(top_srcdir)/epd/Included.am $(top_srcdir)/mtr/Included.am $(top_srcdir)/dddmp/Included.am $(top_srcdir)/cplusplus/Included.am $(top_srcdir)/nanotrav/Included.am $(top_srcdir)/doc/Included.am $(am__empty):
$(top_builddir)/config.status: $(top_srcdir)/configure $(CONFIG_STATUS_DEPENDENCIES)
$(SHELL) ./config.status --recheck
@ -2669,7 +2681,7 @@ $(TEST_SUITE_LOG): $(TEST_LOGS)
if test -n "$$am__remaking_logs"; then \
echo "fatal: making $(TEST_SUITE_LOG): possible infinite" \
"recursion detected" >&2; \
else \
elif test -n "$$redo_logs"; then \
am__remaking_logs=yes $(MAKE) $(AM_MAKEFLAGS) $$redo_logs; \
fi; \
if $(am__make_dryrun); then :; else \
@ -2854,15 +2866,15 @@ dist-xz: distdir
$(am__post_remove_distdir)
dist-tarZ: distdir
@echo WARNING: "Support for shar distribution archives is" \
"deprecated." >&2
@echo WARNING: "Support for distribution archives compressed with" \
"legacy program 'compress' is deprecated." >&2
@echo WARNING: "It will be removed altogether in Automake 2.0" >&2
tardir=$(distdir) && $(am__tar) | compress -c >$(distdir).tar.Z
$(am__post_remove_distdir)
dist-shar: distdir
@echo WARNING: "Support for distribution archives compressed with" \
"legacy program 'compress' is deprecated." >&2
@echo WARNING: "Support for shar distribution archives is" \
"deprecated." >&2
@echo WARNING: "It will be removed altogether in Automake 2.0" >&2
shar $(distdir) | GZIP=$(GZIP_ENV) gzip -c >$(distdir).shar.gz
$(am__post_remove_distdir)
@ -2898,17 +2910,17 @@ distcheck: dist
esac
chmod -R a-w $(distdir)
chmod u+w $(distdir)
mkdir $(distdir)/_build $(distdir)/_inst
mkdir $(distdir)/_build $(distdir)/_build/sub $(distdir)/_inst
chmod a-w $(distdir)
test -d $(distdir)/_build || exit 0; \
dc_install_base=`$(am__cd) $(distdir)/_inst && pwd | sed -e 's,^[^:\\/]:[\\/],/,'` \
&& dc_destdir="$${TMPDIR-/tmp}/am-dc-$$$$/" \
&& am__cwd=`pwd` \
&& $(am__cd) $(distdir)/_build \
&& ../configure \
&& $(am__cd) $(distdir)/_build/sub \
&& ../../configure \
$(AM_DISTCHECK_CONFIGURE_FLAGS) \
$(DISTCHECK_CONFIGURE_FLAGS) \
--srcdir=.. --prefix="$$dc_install_base" \
--srcdir=../.. --prefix="$$dc_install_base" \
&& $(MAKE) $(AM_MAKEFLAGS) \
&& $(MAKE) $(AM_MAKEFLAGS) dvi \
&& $(MAKE) $(AM_MAKEFLAGS) check \
@ -3021,12 +3033,10 @@ distclean-generic:
maintainer-clean-generic:
@echo "This command is intended for maintainers to use"
@echo "it deletes files that may require special tools to rebuild."
@HAVE_DOXYGEN_FALSE@clean-local:
clean: clean-am
clean-am: clean-checkPROGRAMS clean-generic clean-libLTLIBRARIES \
clean-libtool clean-local clean-noinstLTLIBRARIES \
mostlyclean-am
clean-libtool clean-noinstLTLIBRARIES mostlyclean-am
distclean: distclean-am
-rm -f $(am__CONFIG_DISTCLEAN_FILES)
@ -3101,24 +3111,26 @@ uninstall-am: uninstall-includeHEADERS uninstall-libLTLIBRARIES
.PHONY: CTAGS GTAGS TAGS all all-am am--refresh check check-TESTS \
check-am clean clean-checkPROGRAMS clean-cscope clean-generic \
clean-libLTLIBRARIES clean-libtool clean-local \
clean-noinstLTLIBRARIES cscope cscopelist-am ctags ctags-am \
dist dist-all dist-bzip2 dist-gzip dist-hook dist-lzip \
dist-shar dist-tarZ dist-xz dist-zip distcheck distclean \
distclean-compile distclean-generic distclean-hdr \
distclean-libtool distclean-tags distcleancheck distdir \
distuninstallcheck dvi dvi-am html html-am info info-am \
install install-am install-data install-data-am install-dvi \
install-dvi-am install-exec install-exec-am install-html \
install-html-am install-includeHEADERS install-info \
install-info-am install-libLTLIBRARIES install-man install-pdf \
install-pdf-am install-ps install-ps-am install-strip \
installcheck installcheck-am installdirs maintainer-clean \
clean-libLTLIBRARIES clean-libtool clean-noinstLTLIBRARIES \
cscope cscopelist-am ctags ctags-am dist dist-all dist-bzip2 \
dist-gzip dist-hook dist-lzip dist-shar dist-tarZ dist-xz \
dist-zip distcheck distclean distclean-compile \
distclean-generic distclean-hdr distclean-libtool \
distclean-tags distcleancheck distdir distuninstallcheck dvi \
dvi-am html html-am info info-am install install-am \
install-data install-data-am install-dvi install-dvi-am \
install-exec install-exec-am install-html install-html-am \
install-includeHEADERS install-info install-info-am \
install-libLTLIBRARIES install-man install-pdf install-pdf-am \
install-ps install-ps-am install-strip installcheck \
installcheck-am installdirs maintainer-clean \
maintainer-clean-generic mostlyclean mostlyclean-compile \
mostlyclean-generic mostlyclean-libtool pdf pdf-am ps ps-am \
recheck tags tags-am uninstall uninstall-am \
uninstall-includeHEADERS uninstall-libLTLIBRARIES
.PRECIOUS: Makefile
cudd/test_cudd.test: cudd/test_cudd.test.in Makefile
$(do_subst) $< > $@
@ -3160,14 +3172,18 @@ dist-hook:
all: html/index.html doc/cudd.pdf
@HAVE_DOXYGEN_TRUE@html/index.html: Doxyfile $(lib_LTLIBRARIES)
@HAVE_DOXYGEN_TRUE@ @if $(AM_V_P); then dest='2>&1'; else dest='> /dev/null 2>&1'; fi; \
@HAVE_DOXYGEN_TRUE@ eval "$(DOXYGEN) $< $${dest}"
@HAVE_DOXYGEN_TRUE@clean-local:
@HAVE_DOXYGEN_TRUE@ rm -rf html doxygen_sqlite3.db
@HAVE_DOXYGEN_FALSE@html/index.html:
#if HAVE_DOXYGEN
#
#html/index.html: Doxyfile $(lib_LTLIBRARIES)
# @if $(AM_V_P); then dest='2>&1'; else dest='> /dev/null 2>&1'; fi; \
# eval "$(DOXYGEN) $< $${dest}"
#
#clean-local:
# rm -rf html doxygen_sqlite3.db
#
#else
html/index.html:
# Tell versions [3.59,3.63) of GNU make to not export all variables.
# Otherwise a system limit (for SysV at least) may be exceeded.

66
resources/3rdparty/cudd-3.0.0/aclocal.m4

@ -1,6 +1,6 @@
# generated automatically by aclocal 1.14.1 -*- Autoconf -*-
# generated automatically by aclocal 1.15 -*- Autoconf -*-
# Copyright (C) 1996-2013 Free Software Foundation, Inc.
# Copyright (C) 1996-2014 Free Software Foundation, Inc.
# This file is free software; the Free Software Foundation
# gives unlimited permission to copy and/or distribute it,
@ -20,7 +20,7 @@ You have another version of autoconf. It may work, but is not guaranteed to.
If you have problems, you may need to regenerate the build system entirely.
To do so, use the procedure documented by the package, typically 'autoreconf'.])])
# Copyright (C) 2002-2013 Free Software Foundation, Inc.
# Copyright (C) 2002-2014 Free Software Foundation, Inc.
#
# This file is free software; the Free Software Foundation
# gives unlimited permission to copy and/or distribute it,
@ -32,10 +32,10 @@ To do so, use the procedure documented by the package, typically 'autoreconf'.])
# generated from the m4 files accompanying Automake X.Y.
# (This private macro should not be called outside this file.)
AC_DEFUN([AM_AUTOMAKE_VERSION],
[am__api_version='1.14'
[am__api_version='1.15'
dnl Some users find AM_AUTOMAKE_VERSION and mistake it for a way to
dnl require some minimum version. Point them to the right macro.
m4_if([$1], [1.14.1], [],
m4_if([$1], [1.15], [],
[AC_FATAL([Do not call $0, use AM_INIT_AUTOMAKE([$1]).])])dnl
])
@ -51,12 +51,12 @@ m4_define([_AM_AUTOCONF_VERSION], [])
# Call AM_AUTOMAKE_VERSION and AM_AUTOMAKE_VERSION so they can be traced.
# This function is AC_REQUIREd by AM_INIT_AUTOMAKE.
AC_DEFUN([AM_SET_CURRENT_AUTOMAKE_VERSION],
[AM_AUTOMAKE_VERSION([1.14.1])dnl
[AM_AUTOMAKE_VERSION([1.15])dnl
m4_ifndef([AC_AUTOCONF_VERSION],
[m4_copy([m4_PACKAGE_VERSION], [AC_AUTOCONF_VERSION])])dnl
_AM_AUTOCONF_VERSION(m4_defn([AC_AUTOCONF_VERSION]))])
# Copyright (C) 2011-2013 Free Software Foundation, Inc.
# Copyright (C) 2011-2014 Free Software Foundation, Inc.
#
# This file is free software; the Free Software Foundation
# gives unlimited permission to copy and/or distribute it,
@ -118,7 +118,7 @@ AC_SUBST([AR])dnl
# AM_AUX_DIR_EXPAND -*- Autoconf -*-
# Copyright (C) 2001-2013 Free Software Foundation, Inc.
# Copyright (C) 2001-2014 Free Software Foundation, Inc.
#
# This file is free software; the Free Software Foundation
# gives unlimited permission to copy and/or distribute it,
@ -163,15 +163,14 @@ AC_SUBST([AR])dnl
# configured tree to be moved without reconfiguration.
AC_DEFUN([AM_AUX_DIR_EXPAND],
[dnl Rely on autoconf to set up CDPATH properly.
AC_PREREQ([2.50])dnl
# expand $ac_aux_dir to an absolute path
am_aux_dir=`cd $ac_aux_dir && pwd`
[AC_REQUIRE([AC_CONFIG_AUX_DIR_DEFAULT])dnl
# Expand $ac_aux_dir to an absolute path.
am_aux_dir=`cd "$ac_aux_dir" && pwd`
])
# AM_COND_IF -*- Autoconf -*-
# Copyright (C) 2008-2013 Free Software Foundation, Inc.
# Copyright (C) 2008-2014 Free Software Foundation, Inc.
#
# This file is free software; the Free Software Foundation
# gives unlimited permission to copy and/or distribute it,
@ -208,7 +207,7 @@ fi[]dnl
# AM_CONDITIONAL -*- Autoconf -*-
# Copyright (C) 1997-2013 Free Software Foundation, Inc.
# Copyright (C) 1997-2014 Free Software Foundation, Inc.
#
# This file is free software; the Free Software Foundation
# gives unlimited permission to copy and/or distribute it,
@ -239,7 +238,7 @@ AC_CONFIG_COMMANDS_PRE(
Usually this means the macro was only invoked conditionally.]])
fi])])
# Copyright (C) 1999-2013 Free Software Foundation, Inc.
# Copyright (C) 1999-2014 Free Software Foundation, Inc.
#
# This file is free software; the Free Software Foundation
# gives unlimited permission to copy and/or distribute it,
@ -430,7 +429,7 @@ _AM_SUBST_NOTMAKE([am__nodep])dnl
# Generate code to set up dependency tracking. -*- Autoconf -*-
# Copyright (C) 1999-2013 Free Software Foundation, Inc.
# Copyright (C) 1999-2014 Free Software Foundation, Inc.
#
# This file is free software; the Free Software Foundation
# gives unlimited permission to copy and/or distribute it,
@ -506,7 +505,7 @@ AC_DEFUN([AM_OUTPUT_DEPENDENCY_COMMANDS],
# Do all the work for Automake. -*- Autoconf -*-
# Copyright (C) 1996-2013 Free Software Foundation, Inc.
# Copyright (C) 1996-2014 Free Software Foundation, Inc.
#
# This file is free software; the Free Software Foundation
# gives unlimited permission to copy and/or distribute it,
@ -596,8 +595,8 @@ AC_REQUIRE([AC_PROG_MKDIR_P])dnl
# <http://lists.gnu.org/archive/html/automake/2012-07/msg00001.html>
# <http://lists.gnu.org/archive/html/automake/2012-07/msg00014.html>
AC_SUBST([mkdir_p], ['$(MKDIR_P)'])
# We need awk for the "check" target. The system "awk" is bad on
# some platforms.
# We need awk for the "check" target (and possibly the TAP driver). The
# system "awk" is bad on some platforms.
AC_REQUIRE([AC_PROG_AWK])dnl
AC_REQUIRE([AC_PROG_MAKE_SET])dnl
AC_REQUIRE([AM_SET_LEADING_DOT])dnl
@ -671,6 +670,9 @@ END
AC_MSG_ERROR([Your 'rm' program is bad, sorry.])
fi
fi
dnl The trailing newline in this macro's definition is deliberate, for
dnl backward compatibility and to allow trailing 'dnl'-style comments
dnl after the AM_INIT_AUTOMAKE invocation. See automake bug#16841.
])
dnl Hook into '_AC_COMPILER_EXEEXT' early to learn its expansion. Do not
@ -700,7 +702,7 @@ for _am_header in $config_headers :; do
done
echo "timestamp for $_am_arg" >`AS_DIRNAME(["$_am_arg"])`/stamp-h[]$_am_stamp_count])
# Copyright (C) 2001-2013 Free Software Foundation, Inc.
# Copyright (C) 2001-2014 Free Software Foundation, Inc.
#
# This file is free software; the Free Software Foundation
# gives unlimited permission to copy and/or distribute it,
@ -711,7 +713,7 @@ echo "timestamp for $_am_arg" >`AS_DIRNAME(["$_am_arg"])`/stamp-h[]$_am_stamp_co
# Define $install_sh.
AC_DEFUN([AM_PROG_INSTALL_SH],
[AC_REQUIRE([AM_AUX_DIR_EXPAND])dnl
if test x"${install_sh}" != xset; then
if test x"${install_sh+set}" != xset; then
case $am_aux_dir in
*\ * | *\ *)
install_sh="\${SHELL} '$am_aux_dir/install-sh'" ;;
@ -721,7 +723,7 @@ if test x"${install_sh}" != xset; then
fi
AC_SUBST([install_sh])])
# Copyright (C) 2003-2013 Free Software Foundation, Inc.
# Copyright (C) 2003-2014 Free Software Foundation, Inc.
#
# This file is free software; the Free Software Foundation
# gives unlimited permission to copy and/or distribute it,
@ -742,7 +744,7 @@ AC_SUBST([am__leading_dot])])
# Check to see how 'make' treats includes. -*- Autoconf -*-
# Copyright (C) 2001-2013 Free Software Foundation, Inc.
# Copyright (C) 2001-2014 Free Software Foundation, Inc.
#
# This file is free software; the Free Software Foundation
# gives unlimited permission to copy and/or distribute it,
@ -792,7 +794,7 @@ rm -f confinc confmf
# Fake the existence of programs that GNU maintainers use. -*- Autoconf -*-
# Copyright (C) 1997-2013 Free Software Foundation, Inc.
# Copyright (C) 1997-2014 Free Software Foundation, Inc.
#
# This file is free software; the Free Software Foundation
# gives unlimited permission to copy and/or distribute it,
@ -831,7 +833,7 @@ fi
# Helper functions for option handling. -*- Autoconf -*-
# Copyright (C) 2001-2013 Free Software Foundation, Inc.
# Copyright (C) 2001-2014 Free Software Foundation, Inc.
#
# This file is free software; the Free Software Foundation
# gives unlimited permission to copy and/or distribute it,
@ -860,7 +862,7 @@ AC_DEFUN([_AM_SET_OPTIONS],
AC_DEFUN([_AM_IF_OPTION],
[m4_ifset(_AM_MANGLE_OPTION([$1]), [$2], [$3])])
# Copyright (C) 1999-2013 Free Software Foundation, Inc.
# Copyright (C) 1999-2014 Free Software Foundation, Inc.
#
# This file is free software; the Free Software Foundation
# gives unlimited permission to copy and/or distribute it,
@ -907,7 +909,7 @@ AC_LANG_POP([C])])
# For backward compatibility.
AC_DEFUN_ONCE([AM_PROG_CC_C_O], [AC_REQUIRE([AC_PROG_CC])])
# Copyright (C) 2001-2013 Free Software Foundation, Inc.
# Copyright (C) 2001-2014 Free Software Foundation, Inc.
#
# This file is free software; the Free Software Foundation
# gives unlimited permission to copy and/or distribute it,
@ -926,7 +928,7 @@ AC_DEFUN([AM_RUN_LOG],
# Check to make sure that the build environment is sane. -*- Autoconf -*-
# Copyright (C) 1996-2013 Free Software Foundation, Inc.
# Copyright (C) 1996-2014 Free Software Foundation, Inc.
#
# This file is free software; the Free Software Foundation
# gives unlimited permission to copy and/or distribute it,
@ -1007,7 +1009,7 @@ AC_CONFIG_COMMANDS_PRE(
rm -f conftest.file
])
# Copyright (C) 2009-2013 Free Software Foundation, Inc.
# Copyright (C) 2009-2014 Free Software Foundation, Inc.
#
# This file is free software; the Free Software Foundation
# gives unlimited permission to copy and/or distribute it,
@ -1067,7 +1069,7 @@ AC_SUBST([AM_BACKSLASH])dnl
_AM_SUBST_NOTMAKE([AM_BACKSLASH])dnl
])
# Copyright (C) 2001-2013 Free Software Foundation, Inc.
# Copyright (C) 2001-2014 Free Software Foundation, Inc.
#
# This file is free software; the Free Software Foundation
# gives unlimited permission to copy and/or distribute it,
@ -1095,7 +1097,7 @@ fi
INSTALL_STRIP_PROGRAM="\$(install_sh) -c -s"
AC_SUBST([INSTALL_STRIP_PROGRAM])])
# Copyright (C) 2006-2013 Free Software Foundation, Inc.
# Copyright (C) 2006-2014 Free Software Foundation, Inc.
#
# This file is free software; the Free Software Foundation
# gives unlimited permission to copy and/or distribute it,
@ -1114,7 +1116,7 @@ AC_DEFUN([AM_SUBST_NOTMAKE], [_AM_SUBST_NOTMAKE($@)])
# Check how to create a tarball. -*- Autoconf -*-
# Copyright (C) 2004-2013 Free Software Foundation, Inc.
# Copyright (C) 2004-2014 Free Software Foundation, Inc.
#
# This file is free software; the Free Software Foundation
# gives unlimited permission to copy and/or distribute it,

12
resources/3rdparty/cudd-3.0.0/configure

@ -2753,7 +2753,7 @@ IFS=$ac_save_IFS
case $host_os in *\ *) host_os=`echo "$host_os" | sed 's/ /-/g'`;; esac
am__api_version='1.14'
am__api_version='1.15'
# Find a good install program. We prefer a C program (faster),
# so one script is as good as another. But avoid the broken or
@ -2925,8 +2925,8 @@ test "$program_suffix" != NONE &&
ac_script='s/[\\$]/&&/g;s/;s,x,x,$//'
program_transform_name=`$as_echo "$program_transform_name" | sed "$ac_script"`
# expand $ac_aux_dir to an absolute path
am_aux_dir=`cd $ac_aux_dir && pwd`
# Expand $ac_aux_dir to an absolute path.
am_aux_dir=`cd "$ac_aux_dir" && pwd`
if test x"${MISSING+set}" != xset; then
case $am_aux_dir in
@ -2945,7 +2945,7 @@ else
$as_echo "$as_me: WARNING: 'missing' script is too old or missing" >&2;}
fi
if test x"${install_sh}" != xset; then
if test x"${install_sh+set}" != xset; then
case $am_aux_dir in
*\ * | *\ *)
install_sh="\${SHELL} '$am_aux_dir/install-sh'" ;;
@ -3273,8 +3273,8 @@ MAKEINFO=${MAKEINFO-"${am_missing_run}makeinfo"}
# <http://lists.gnu.org/archive/html/automake/2012-07/msg00014.html>
mkdir_p='$(MKDIR_P)'
# We need awk for the "check" target. The system "awk" is bad on
# some platforms.
# We need awk for the "check" target (and possibly the TAP driver). The
# system "awk" is bad on some platforms.
# Always define AMTAR for backward compatibility. Yes, it's still used
# in the wild :-( We should find a proper way to deprecate it ...
AMTAR='$${TAR-tar}'

26
resources/3rdparty/cudd-3.0.0/cplusplus/cuddObj.cc

@ -63,6 +63,8 @@ using std::string;
using std::vector;
using std::sort;
namespace cudd {
// ---------------------------------------------------------------------------
// Variable declarations
// ---------------------------------------------------------------------------
@ -5625,6 +5627,28 @@ ABDD::CountLeaves() const
} // ABDD::CountLeaves
DdGen *
ABDD::FirstCube(
int ** cube,
CUDD_VALUE_TYPE * value) const
{
DdManager *mgr = p->manager;
DdGen *result = Cudd_FirstCube(mgr, node, cube, value);
checkReturnValue((DdNode *)result);
return result;
} // ABDD::FirstCube
int
ABDD::NextCube(
DdGen * gen,
int ** cube,
CUDD_VALUE_TYPE * value)
{
return Cudd_NextCube(gen, cube, value);
} // ABDD::NextCube
void
BDD::PickOneCube(
@ -6166,3 +6190,5 @@ Cudd::OrderString(void) const
return oss.str();
} // Cudd::OrderString
} // end namespace storm

6
resources/3rdparty/cudd-3.0.0/cplusplus/cuddObj.hh

@ -54,8 +54,11 @@
#include <cstdio>
#include <string>
#include <vector>
#include "mtr.h"
#include "cudd.h"
namespace cudd {
/*---------------------------------------------------------------------------*/
/* Type definitions */
/*---------------------------------------------------------------------------*/
@ -147,6 +150,8 @@ public:
void ClassifySupport(const ABDD& g, BDD* common, BDD* onlyF, BDD* onlyG)
const;
int CountLeaves() const;
DdGen * FirstCube(int ** cube, CUDD_VALUE_TYPE * value) const;
static int NextCube(DdGen * gen, int ** cube, CUDD_VALUE_TYPE * value);
double Density(int nvars) const;
}; // ABDD
@ -746,5 +751,6 @@ public:
}; // Cudd
} // end of namespace cudd
#endif

6
resources/3rdparty/cudd-3.0.0/cudd/cudd.h

@ -518,7 +518,9 @@ extern int Cudd_IsConstant(DdNode *node);
extern int Cudd_IsNonConstant(DdNode *f);
extern DdNode * Cudd_T(DdNode *node);
extern DdNode * Cudd_E(DdNode *node);
extern CUDD_VALUE_TYPE Cudd_V(DdNode *node);
extern DdNode const * Cudd_T_const(DdNode const * node);
extern DdNode const * Cudd_E_const(DdNode const * node);
extern CUDD_VALUE_TYPE Cudd_V(DdNode const * node);
extern unsigned long Cudd_ReadStartTime(DdManager *unique);
extern unsigned long Cudd_ReadElapsedTime(DdManager *unique);
extern void Cudd_SetStartTime(DdManager *unique, unsigned long st);
@ -595,7 +597,7 @@ extern double Cudd_ReadMaxGrowthAlternate(DdManager * dd);
extern void Cudd_SetMaxGrowthAlternate(DdManager * dd, double mg);
extern int Cudd_ReadReorderingCycle(DdManager * dd);
extern void Cudd_SetReorderingCycle(DdManager * dd, int cycle);
extern unsigned int Cudd_NodeReadIndex(DdNode *node);
extern unsigned int Cudd_NodeReadIndex(DdNode const * node);
extern int Cudd_ReadPerm(DdManager *dd, int i);
extern int Cudd_ReadPermZdd(DdManager *dd, int i);
extern int Cudd_ReadInvPerm(DdManager *dd, int i);

49
resources/3rdparty/cudd-3.0.0/cudd/cuddAPI.c

@ -588,8 +588,8 @@ Cudd_IsNonConstant(
@see Cudd_E Cudd_V
*/
DdNode *
Cudd_T(DdNode *node)
DdNode const *
Cudd_T_const(DdNode const *node)
{
return Cudd_Regular(node)->type.kids.T;
@ -607,13 +607,49 @@ Cudd_T(DdNode *node)
@see Cudd_T Cudd_V
*/
DdNode *
Cudd_E(DdNode *node)
DdNode const *
Cudd_E_const(DdNode const * node)
{
return Cudd_Regular(node)->type.kids.E;
} /* end of Cudd_E */
/**
@brief Returns the then child of an internal node.
@details If <code>node</code> is a constant node, the result is
unpredictable.
@sideeffect none
@see Cudd_E Cudd_V
*/
DdNode *
Cudd_T(DdNode * node)
{
return Cudd_Regular(node)->type.kids.T;
} /* end of Cudd_T */
/**
@brief Returns the else child of an internal node.
@details If <code>node</code> is a constant node, the result is
unpredictable.
@sideeffect none
@see Cudd_T Cudd_V
*/
DdNode *
Cudd_E(DdNode * node)
{
return Cudd_Regular(node)->type.kids.E;
} /* end of Cudd_E */
/**
@brief Returns the value of a constant node.
@ -627,7 +663,7 @@ Cudd_E(DdNode *node)
*/
CUDD_VALUE_TYPE
Cudd_V(DdNode *node)
Cudd_V(DdNode const *node)
{
return Cudd_Regular(node)->type.value;
@ -2504,13 +2540,12 @@ Cudd_FreeZddTree(
*/
unsigned int
Cudd_NodeReadIndex(
DdNode * node)
DdNode const * node)
{
return((unsigned int) Cudd_Regular(node)->index);
} /* end of Cudd_NodeReadIndex */
/**
@brief Returns the current position of the i-th variable in the
order.

3
src/models/symbolic/Model.cpp

@ -91,7 +91,8 @@ namespace storm {
template<storm::dd::DdType Type, typename ValueType>
std::size_t Model<Type, ValueType>::getSizeInBytes() const {
return sizeof(*this) + sizeof(DdNode) * (reachableStates.getNodeCount() + initialStates.getNodeCount() + transitionMatrix.getNodeCount());
// FIXME: This assumes a fixed value of 16 bytes per node, which isn't necessarily true.
return sizeof(*this) + 16 * (reachableStates.getNodeCount() + initialStates.getNodeCount() + transitionMatrix.getNodeCount());
}
template<storm::dd::DdType Type, typename ValueType>

8
src/storage/dd/cudd/InternalCuddAdd.cpp

@ -366,7 +366,7 @@ namespace storm {
}
return std::make_shared<Odd>(nullptr, elseOffset, nullptr, thenOffset);
} else if (ddVariableIndices[currentLevel] < static_cast<uint_fast64_t>(dd->index)) {
} else if (ddVariableIndices[currentLevel] < Cudd_NodeReadIndex(dd)) {
// If we skipped the level in the DD, we compute the ODD just for the else-successor and use the same
// node for the then-successor as well.
std::shared_ptr<Odd> elseNode = createOddRec(dd, manager, currentLevel + 1, maxLevel, ddVariableIndices, uniqueTableForLevels);
@ -406,15 +406,15 @@ namespace storm {
if (currentLevel == maxLevel) {
ValueType& targetValue = targetVector[offsets != nullptr ? (*offsets)[currentOffset] : currentOffset];
targetValue = function(targetValue, Cudd_V(dd));
} else if (ddVariableIndices[currentLevel] < dd->index) {
} else if (ddVariableIndices[currentLevel] < Cudd_NodeReadIndex(dd)) {
// If we skipped a level, we need to enumerate the explicit entries for the case in which the bit is set
// and for the one in which it is not set.
composeWithExplicitVectorRec(dd, offsets, currentLevel + 1, maxLevel, currentOffset, odd.getElseSuccessor(), ddVariableIndices, targetVector, function);
composeWithExplicitVectorRec(dd, offsets, currentLevel + 1, maxLevel, currentOffset + odd.getElseOffset(), odd.getThenSuccessor(), ddVariableIndices, targetVector, function);
} else {
// Otherwise, we simply recursively call the function for both (different) cases.
composeWithExplicitVectorRec(Cudd_E(dd), offsets, currentLevel + 1, maxLevel, currentOffset, odd.getElseSuccessor(), ddVariableIndices, targetVector, function);
composeWithExplicitVectorRec(Cudd_T(dd), offsets, currentLevel + 1, maxLevel, currentOffset + odd.getElseOffset(), odd.getThenSuccessor(), ddVariableIndices, targetVector, function);
composeWithExplicitVectorRec(Cudd_E_const(dd), offsets, currentLevel + 1, maxLevel, currentOffset, odd.getElseSuccessor(), ddVariableIndices, targetVector, function);
composeWithExplicitVectorRec(Cudd_T_const(dd), offsets, currentLevel + 1, maxLevel, currentOffset + odd.getElseOffset(), odd.getThenSuccessor(), ddVariableIndices, targetVector, function);
}
}

18
src/storage/dd/cudd/InternalCuddBdd.cpp

@ -287,13 +287,13 @@ namespace storm {
// If we are at the maximal level, the value to be set is stored as a constant in the DD.
if (currentRowLevel == maxLevel) {
result.set(currentRowOffset, true);
} else if (ddRowVariableIndices[currentRowLevel] < dd->index) {
} else if (ddRowVariableIndices[currentRowLevel] < Cudd_NodeReadIndex(dd)) {
toVectorRec(dd, manager, result, rowOdd.getElseSuccessor(), complement, currentRowLevel + 1, maxLevel, currentRowOffset, ddRowVariableIndices);
toVectorRec(dd, manager, result, rowOdd.getThenSuccessor(), complement, currentRowLevel + 1, maxLevel, currentRowOffset + rowOdd.getElseOffset(), ddRowVariableIndices);
} else {
// Otherwise, we compute the ODDs for both the then- and else successors.
DdNode* elseDdNode = Cudd_E(dd);
DdNode* thenDdNode = Cudd_T(dd);
DdNode const* elseDdNode = Cudd_E_const(dd);
DdNode const* thenDdNode = Cudd_T_const(dd);
// Determine whether we have to evaluate the successors as if they were complemented.
bool elseComplemented = Cudd_IsComplement(elseDdNode) ^ complement;
@ -347,7 +347,7 @@ namespace storm {
}
return std::make_shared<Odd>(nullptr, elseOffset, nullptr, thenOffset);
} else if (ddVariableIndices[currentLevel] < static_cast<uint_fast64_t>(dd->index)) {
} else if (ddVariableIndices[currentLevel] < Cudd_NodeReadIndex(dd)) {
// If we skipped the level in the DD, we compute the ODD just for the else-successor and use the same
// node for the then-successor as well.
std::shared_ptr<Odd> elseNode = createOddRec(dd, manager, currentLevel + 1, complement, maxLevel, ddVariableIndices, uniqueTableForLevels);
@ -356,8 +356,8 @@ namespace storm {
return std::make_shared<Odd>(elseNode, totalOffset, thenNode, totalOffset);
} else {
// Otherwise, we compute the ODDs for both the then- and else successors.
DdNode* thenDdNode = Cudd_T(dd);
DdNode* elseDdNode = Cudd_E(dd);
DdNode const* thenDdNode = Cudd_T_const(dd);
DdNode const* elseDdNode = Cudd_E_const(dd);
// Determine whether we have to evaluate the successors as if they were complemented.
bool elseComplemented = Cudd_IsComplement(elseDdNode) ^ complement;
@ -388,15 +388,15 @@ namespace storm {
if (currentLevel == maxLevel) {
result[currentIndex++] = values[currentOffset];
} else if (ddVariableIndices[currentLevel] < dd->index) {
} else if (ddVariableIndices[currentLevel] < Cudd_NodeReadIndex(dd)) {
// If we skipped a level, we need to enumerate the explicit entries for the case in which the bit is set
// and for the one in which it is not set.
filterExplicitVectorRec(dd, manager, currentLevel + 1, complement, maxLevel, ddVariableIndices, currentOffset, odd.getElseSuccessor(), result, currentIndex, values);
filterExplicitVectorRec(dd, manager, currentLevel + 1, complement, maxLevel, ddVariableIndices, currentOffset + odd.getElseOffset(), odd.getThenSuccessor(), result, currentIndex, values);
} else {
// Otherwise, we compute the ODDs for both the then- and else successors.
DdNode* thenDdNode = Cudd_T(dd);
DdNode* elseDdNode = Cudd_E(dd);
DdNode const* thenDdNode = Cudd_T_const(dd);
DdNode const* elseDdNode = Cudd_E_const(dd);
// Determine whether we have to evaluate the successors as if they were complemented.
bool elseComplemented = Cudd_IsComplement(elseDdNode) ^ complement;
Loading…
Cancel
Save