From 97d9ecccbba5ae7fa7c9c303ce49d0efac4b5c62 Mon Sep 17 00:00:00 2001 From: dehnert <dehnert@cs.rwth-aachen.de> Date: Wed, 17 Feb 2016 18:40:18 +0100 Subject: [PATCH] started making cudd3 work Former-commit-id: bc791536bb8fa7426889dfdbc9d52fc91a970f31 --- resources/3rdparty/cudd-3.0.0/Makefile.am | 23 +-- resources/3rdparty/cudd-3.0.0/Makefile.in | 154 ++++++++++-------- resources/3rdparty/cudd-3.0.0/aclocal.m4 | 66 ++++---- resources/3rdparty/cudd-3.0.0/configure | 12 +- .../3rdparty/cudd-3.0.0/cplusplus/cuddObj.cc | 26 +++ .../3rdparty/cudd-3.0.0/cplusplus/cuddObj.hh | 6 + resources/3rdparty/cudd-3.0.0/cudd/cudd.h | 6 +- resources/3rdparty/cudd-3.0.0/cudd/cuddAPI.c | 49 +++++- src/models/symbolic/Model.cpp | 3 +- src/storage/dd/cudd/InternalCuddAdd.cpp | 8 +- src/storage/dd/cudd/InternalCuddBdd.cpp | 18 +- 11 files changed, 230 insertions(+), 141 deletions(-) diff --git a/resources/3rdparty/cudd-3.0.0/Makefile.am b/resources/3rdparty/cudd-3.0.0/Makefile.am index 45f216a58..54f0b03d4 100644 --- a/resources/3rdparty/cudd-3.0.0/Makefile.am +++ b/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) diff --git a/resources/3rdparty/cudd-3.0.0/Makefile.in b/resources/3rdparty/cudd-3.0.0/Makefile.in index c42e8b723..75846bc4c 100644 --- a/resources/3rdparty/cudd-3.0.0/Makefile.in +++ b/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. diff --git a/resources/3rdparty/cudd-3.0.0/aclocal.m4 b/resources/3rdparty/cudd-3.0.0/aclocal.m4 index e231ebf46..0de6688a7 100644 --- a/resources/3rdparty/cudd-3.0.0/aclocal.m4 +++ b/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, diff --git a/resources/3rdparty/cudd-3.0.0/configure b/resources/3rdparty/cudd-3.0.0/configure index 668e3daaf..f0e0e742e 100755 --- a/resources/3rdparty/cudd-3.0.0/configure +++ b/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}' diff --git a/resources/3rdparty/cudd-3.0.0/cplusplus/cuddObj.cc b/resources/3rdparty/cudd-3.0.0/cplusplus/cuddObj.cc index 352561237..6aa67b516 100644 --- a/resources/3rdparty/cudd-3.0.0/cplusplus/cuddObj.cc +++ b/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 diff --git a/resources/3rdparty/cudd-3.0.0/cplusplus/cuddObj.hh b/resources/3rdparty/cudd-3.0.0/cplusplus/cuddObj.hh index c9b02e897..e71bc486c 100644 --- a/resources/3rdparty/cudd-3.0.0/cplusplus/cuddObj.hh +++ b/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 diff --git a/resources/3rdparty/cudd-3.0.0/cudd/cudd.h b/resources/3rdparty/cudd-3.0.0/cudd/cudd.h index 7d6f10e50..9c140fd5d 100644 --- a/resources/3rdparty/cudd-3.0.0/cudd/cudd.h +++ b/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); diff --git a/resources/3rdparty/cudd-3.0.0/cudd/cuddAPI.c b/resources/3rdparty/cudd-3.0.0/cudd/cuddAPI.c index fcc5eb03b..78214567e 100644 --- a/resources/3rdparty/cudd-3.0.0/cudd/cuddAPI.c +++ b/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. diff --git a/src/models/symbolic/Model.cpp b/src/models/symbolic/Model.cpp index 9840a3188..b2549e5a2 100644 --- a/src/models/symbolic/Model.cpp +++ b/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> diff --git a/src/storage/dd/cudd/InternalCuddAdd.cpp b/src/storage/dd/cudd/InternalCuddAdd.cpp index 10107ff2c..564a521e9 100644 --- a/src/storage/dd/cudd/InternalCuddAdd.cpp +++ b/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); } } diff --git a/src/storage/dd/cudd/InternalCuddBdd.cpp b/src/storage/dd/cudd/InternalCuddBdd.cpp index ce285fc1d..607b68428 100644 --- a/src/storage/dd/cudd/InternalCuddBdd.cpp +++ b/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;