From 3d2b33d66998261f9369cccc098140f64bc8b417 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Mon, 20 Feb 2012 17:59:33 +0000 Subject: [PATCH] portfolio merge --- .gitignore | 2 + AUTHORS | 3 + COPYING | 26 + Makefile.builds.in | 147 ++- README | 1 + config/boost.m4 | 1044 +++++++++++++++++ configure.ac | 71 +- src/expr/Makefile.am | 6 + src/expr/command.cpp | 152 +++ src/expr/command.h | 54 + src/expr/expr_manager_template.cpp | 49 +- src/expr/expr_manager_template.h | 12 + src/expr/expr_template.cpp | 82 +- src/expr/expr_template.h | 31 +- src/expr/mkexpr | 4 + src/expr/node.h | 10 + src/expr/node_builder.h | 12 +- src/expr/node_manager.cpp | 2 + src/expr/node_manager.h | 112 +- src/expr/node_value.cpp | 2 - src/expr/node_value.h | 2 - src/expr/pickle_data.cpp | 60 + src/expr/pickle_data.h | 122 ++ src/expr/pickler.cpp | 477 ++++++++ src/expr/pickler.h | 139 +++ src/expr/type.cpp | 4 + src/expr/type.h | 11 + src/expr/type_node.h | 10 + src/expr/variable_type_map.h | 64 + src/main/Makefile.am | 31 +- src/main/driver.cpp | 355 ++++++ src/main/driver_portfolio.cpp | 808 +++++++++++++ src/main/interactive_shell.cpp | 2 +- src/main/main.cpp | 318 +---- src/main/main.h | 9 +- src/main/portfolio.cpp | 93 ++ src/main/portfolio.h | 42 + src/main/util.cpp | 40 +- src/parser/parser_builder.cpp | 34 +- src/parser/parser_builder.h | 2 +- src/prop/cnf_stream.cpp | 7 +- src/prop/cnf_stream.h | 13 +- src/prop/sat.cpp | 50 + src/prop/sat.h | 14 + src/smt/smt_engine.h | 4 + src/theory/arith/arith_priority_queue.cpp | 3 + src/theory/arith/simplex.cpp | 4 +- src/theory/arith/theory_arith.cpp | 2 +- src/theory/arith/theory_arith_type_rules.h | 6 +- src/theory/arrays/theory_arrays_type_rules.h | 4 +- src/theory/booleans/theory_bool_type_rules.h | 4 +- .../builtin/theory_builtin_type_rules.h | 4 +- src/theory/bv/theory_bv_rewriter.cpp | 2 +- src/theory/bv/theory_bv_rewriter.h | 2 +- src/theory/bv/theory_bv_type_rules.h | 18 +- src/theory/theory_engine.h | 10 +- src/theory/uf/theory_uf_type_rules.h | 2 +- src/util/Makefile.am | 3 + src/util/channel.cpp | 2 + src/util/channel.h | 96 ++ src/util/hash.h | 16 + src/util/lemma_input_channel.h | 19 + src/util/lemma_output_channel.h | 46 + src/util/options.cpp | 96 +- src/util/options.h | 41 + src/util/stats.cpp | 48 +- src/util/stats.h | 230 ++-- test/regress/regress0/Makefile.am | 5 +- test/regress/regress0/arith/Makefile.am | 5 +- test/regress/regress0/bv/Makefile.am | 5 +- test/regress/regress0/bv/core/Makefile.am | 5 +- test/regress/regress0/lemmas/Makefile.am | 5 +- test/regress/regress0/precedence/Makefile.am | 5 +- test/regress/regress0/push-pop/Makefile.am | 5 +- test/regress/regress0/uf/Makefile.am | 5 +- test/regress/regress0/uflra/Makefile.am | 5 +- test/regress/regress1/Makefile.am | 5 +- test/regress/regress1/arith/Makefile.am | 5 +- test/regress/regress2/Makefile.am | 5 +- test/regress/regress3/Makefile.am | 5 +- 80 files changed, 4651 insertions(+), 605 deletions(-) create mode 100644 config/boost.m4 create mode 100644 src/expr/pickle_data.cpp create mode 100644 src/expr/pickle_data.h create mode 100644 src/expr/pickler.cpp create mode 100644 src/expr/pickler.h create mode 100644 src/expr/variable_type_map.h create mode 100644 src/main/driver.cpp create mode 100644 src/main/driver_portfolio.cpp create mode 100644 src/main/portfolio.cpp create mode 100644 src/main/portfolio.h create mode 100644 src/util/channel.cpp create mode 100644 src/util/channel.h create mode 100644 src/util/lemma_input_channel.h create mode 100644 src/util/lemma_output_channel.h diff --git a/.gitignore b/.gitignore index 2bb76f9dc..e2c448004 100644 --- a/.gitignore +++ b/.gitignore @@ -25,3 +25,5 @@ generated/ /lcov/ .cvc4_config config.reconfig +*.swp +/debug/ diff --git a/AUTHORS b/AUTHORS index f5897d574..db0cf4a9c 100644 --- a/AUTHORS +++ b/AUTHORS @@ -1,5 +1,6 @@ The core authors and designers of CVC4 are: + Kshitij Bansal , New York University Clark Barrett , New York University François Bobot , Paris-Sud University Christopher Conway , New York University @@ -27,5 +28,7 @@ CVC4 contains the pkg.m4 autoconf module by Scott James Remnant. CVC4 contains the ax_tls.m4 autoconf module by Alan Woodland and Diego Elio Petteno. +CVC4 contains the boost.m4 autoconf module by Benoit Sigoure. + CVC4 maintainer versions contain the script autogen.sh, by the U.S. Army Research Laboratory diff --git a/COPYING b/COPYING index bcb21aa3d..9d9e116fd 100644 --- a/COPYING +++ b/COPYING @@ -145,6 +145,32 @@ See config/ax_tls.m4. Its copyright: modified version of the Autoconf Macro, you may extend this special exception to the GPL to apply to your modified version as well. +CVC4 incorporates the m4 macro file "boost.m4", excluded from the above +copyright and downloaded from http://github.com/tsuna/boost.m4 . +See config/boost.m4. Its copyright: + + Copyright (C) 2007 Benoit Sigoure + + This program is free software: you can redistribute it and/or modify + it under the terms of the GNU General Public License as published by + the Free Software Foundation, either version 3 of the License, or + (at your option) any later version. + + This program is distributed in the hope that it will be useful, + but WITHOUT ANY WARRANTY; without even the implied warranty of + MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + GNU General Public License for more details. + + You should have received a copy of the GNU General Public License + along with this program. If not, see . + + Additional permission under section 7 of the GNU General Public + License, version 3 ("GPLv3"): + + If you convey this file as part of a work that contains a + configuration script generated by Autoconf, you may do so under + terms of your choice. + CVC4 incorporates code from ANTLR3, excluded from the above copyright. See http://www.antlr.org/, and the files src/parser/bounded_token_buffer.h, src/parser/bounded_token_buffer.cpp, and src/parser/antlr_input_imports.cpp. diff --git a/Makefile.builds.in b/Makefile.builds.in index 21d172623..054b4eb7b 100644 --- a/Makefile.builds.in +++ b/Makefile.builds.in @@ -30,6 +30,9 @@ bindir = @bindir@ libdir = @libdir@ abs_builddir = @abs_builddir@ distdir = @PACKAGE@-@VERSION@ +AM_DEFAULT_VERBOSITY = @AM_DEFAULT_VERBOSITY@ +SHELL = @SHELL@ +LIBTOOL = $(CURRENT_BUILD)/libtool # Are we building the libcvc4compat library ? CVC4_BUILD_LIBCOMPAT = @CVC4_BUILD_LIBCOMPAT@ @@ -40,21 +43,56 @@ BUILDING_STATIC = @BUILDING_STATIC@ BUILDING_SHARED = @BUILDING_SHARED@ STATIC_BINARY = @STATIC_BINARY@ +# @ +AM_V_at = $(am__v_at_$(V)) +am__v_at_ = $(am__v_at_$(AM_DEFAULT_VERBOSITY)) +am__v_at_0 = @ +am__v_at_1 = +# mkinstalldirs (never prefix with @; not a top-level instruction) +AM_V_mkdir_noat = $(am__v_mkdir_noat_$(V)) +am__v_mkdir_noat_ = $(am__v_mkdir_noat_$(AM_DEFAULT_VERBOSITY)) +am__v_mkdir_noat_0 = $(SHELL) -c 'echo " MKDIR $$@"; $(mkinstalldirs) "$$@"' bash +am__v_mkdir_noat_1 = $(mkinstalldirs) +# mkinstalldirs (can prefix with @) +AM_V_mkdir = $(am__v_mkdir_$(V)) +am__v_mkdir_ = $(am__v_mkdir_$(AM_DEFAULT_VERBOSITY)) +am__v_mkdir_0 = @$(am__v_mkdir_noat_0) +am__v_mkdir_1 = $(am__v_mkdir_noat_1) +# libtool --mode=install install +AM_V_ltinstall = $(am__v_ltinstall_$(V)) +am__v_ltinstall_ = $(am__v_ltinstall_$(AM_DEFAULT_VERBOSITY)) +am__v_ltinstall_0 = @$(SHELL) -c 'echo " LTINS $$1"; $(LIBTOOL) --silent --mode=install install "$$@"' bash +am__v_ltinstall_1 = $(LIBTOOL) --mode=install install +# install_sh (never prefix with @) +AM_V_install_sh_noat = $(am__v_install_sh_noat_$(V)) +am__v_install_sh_noat_ = $(am__v_install_sh_noat_$(AM_DEFAULT_VERBOSITY)) +am__v_install_sh_noat_0 = $(SHELL) -c 'echo " INSTL $$1"; $(install_sh) "$$@"' bash +am__v_install_sh_noat_1 = $(install_sh) +# relinking +AM_V_relink = $(am__v_relink_$(V)) +am__v_relink_ = $(am__v_relink_$(AM_DEFAULT_VERBOSITY)) +am__v_relink_0 = echo " RELNK" +am__v_relink_1 = : + +# all the binaries that might need to be installed +# (it's not a fatal error for one/some don't exist in a given build +# configuration) +CVC4_BINARIES = cvc4 pcvc4 + .PHONY: _default_build_ all _default_build_: all all: # build the current build profile - +(cd $(CURRENT_BUILD) && $(MAKE) $@) + $(AM_V_at)(cd $(CURRENT_BUILD) && $(MAKE) $@) # set up builds/$(CURRENT_BUILD)/...prefix.../bin # and builds/$(CURRENT_BUILD)/...prefix.../lib - $(mkinstalldirs) "$(CURRENT_BUILD)$(bindir)" "$(CURRENT_BUILD)$(libdir)" + $(AM_V_mkdir) "$(CURRENT_BUILD)$(bindir)" + $(AM_V_mkdir) "$(CURRENT_BUILD)$(libdir)" # install libcvc4 - $(CURRENT_BUILD)/libtool --mode=install install -v \ - $(CURRENT_BUILD)/src/libcvc4.la \ + $(AM_V_ltinstall) $(CURRENT_BUILD)/src/libcvc4.la \ "$(abs_builddir)$(libdir)" # install libcvc4parser - $(CURRENT_BUILD)/libtool --mode=install install -v \ - $(CURRENT_BUILD)/src/parser/libcvc4parser.la \ + $(AM_V_ltinstall) $(CURRENT_BUILD)/src/parser/libcvc4parser.la \ "$(abs_builddir)$(libdir)" ifeq ($(CVC4_BUILD_LIBCOMPAT),yes) # install libcvc4compat @@ -65,35 +103,47 @@ endif ifeq ($(BUILDING_SHARED)$(STATIC_BINARY),10) # if we're building shared libs and the binary is not static, relink # the handling with empty $relink_command is a hack for Mac OS - thelibdir="$(abs_builddir)$(libdir)"; \ - progdir="$(abs_builddir)$(bindir)"; file=cvc4; \ - eval `grep '^relink_command=' $(CURRENT_BUILD)/src/main/cvc4 | sed 's:-Wl,-rpath:-Wl,-rpath -Wl,\\\\$$thelibdir -Wl,-rpath:'`; \ - if test -z "$$relink_command"; then \ - $(mkinstalldirs) "$(CURRENT_BUILD)$(bindir)/.libs"; \ - $(install_sh) \ - $(CURRENT_BUILD)/src/main/.libs/cvc4 \ - "$(abs_builddir)$(bindir)/.libs"; \ - $(install_sh) \ - $(CURRENT_BUILD)/src/main/cvc4 \ - "$(abs_builddir)$(bindir)"; \ + $(AM_V_at)thelibdir="$(abs_builddir)$(libdir)"; \ + progdir="$(abs_builddir)$(bindir)"; for file in $(CVC4_BINARIES); do \ + if test -r $(CURRENT_BUILD)/src/main/$$file; then \ + eval `grep '^relink_command=' $(CURRENT_BUILD)/src/main/$$file | sed 's:-Wl,-rpath:-Wl,-rpath -Wl,\\\\$$thelibdir -Wl,-rpath:'`; \ + if test -z "$$relink_command"; then \ + $(AM_V_mkdir_noat) "$(CURRENT_BUILD)$(bindir)/.libs"; \ + $(AM_V_install_sh_noat) \ + $(CURRENT_BUILD)/src/main/.libs/$$file \ + "$(abs_builddir)$(bindir)/.libs"; \ + $(AM_V_install_sh_noat) \ + $(CURRENT_BUILD)/src/main/$$file \ + "$(abs_builddir)$(bindir)"; \ + else \ + $(AM_V_relink) "$$file"; eval "(cd $(CURRENT_BUILD)/src/main && $$relink_command)"; \ + fi; \ else \ - eval "(cd $(CURRENT_BUILD)/src/main && $$relink_command)"; \ - fi + rm -f "$(abs_builddir)$(bindir)/$$file"; \ + fi; \ + done else # if we're building static libs only, just install the driver binary directly - $(install_sh) \ - $(CURRENT_BUILD)/src/main/cvc4 \ - "$(abs_builddir)$(bindir)" + $(AM_V_at)for file in $(CVC4_BINARIES); do \ + if test -r $(CURRENT_BUILD)/src/main/$$file; then \ + $(AM_V_install_sh_noat) \ + $(CURRENT_BUILD)/src/main/$$file \ + "$(abs_builddir)$(bindir)"; \ + else \ + rm -f "$(abs_builddir)$(bindir)/$$file"; \ + fi; \ + done endif # set up builds/$(CURRENT_BUILD)/bin and builds/$(CURRENT_BUILD)/lib - test -e $(CURRENT_BUILD)/lib || ln -sfv "$(abs_builddir)$(libdir)" $(CURRENT_BUILD)/lib - test -e $(CURRENT_BUILD)/bin || ln -sfv "$(abs_builddir)$(bindir)" $(CURRENT_BUILD)/bin + $(AM_V_at)test -e $(CURRENT_BUILD)/lib || ln -sfv "$(abs_builddir)$(libdir)" $(CURRENT_BUILD)/lib + $(AM_V_at)test -e $(CURRENT_BUILD)/bin || ln -sfv "$(abs_builddir)$(bindir)" $(CURRENT_BUILD)/bin # set up builds/...prefix.../bin and builds/...prefix.../lib - $(mkinstalldirs) ".$(bindir)" ".$(libdir)" + $(AM_V_mkdir) ".$(bindir)" + $(AM_V_mkdir) ".$(libdir)" # install libcvc4 - $(CURRENT_BUILD)/libtool --mode=install install -v $(CURRENT_BUILD)/src/libcvc4.la "`pwd`$(libdir)" + $(AM_V_ltinstall) $(CURRENT_BUILD)/src/libcvc4.la "`pwd`$(libdir)" # install libcvc4parser - $(CURRENT_BUILD)/libtool --mode=install install -v $(CURRENT_BUILD)/src/parser/libcvc4parser.la "`pwd`$(libdir)" + $(AM_V_ltinstall) $(CURRENT_BUILD)/src/parser/libcvc4parser.la "`pwd`$(libdir)" ifeq ($(CVC4_BUILD_LIBCOMPAT),yes) # install libcvc4compat $(CURRENT_BUILD)/libtool --mode=install install -v $(CURRENT_BUILD)/src/compat/libcvc4compat.la "`pwd`$(libdir)" @@ -101,26 +151,39 @@ endif ifeq ($(BUILDING_SHARED)$(STATIC_BINARY),10) # if we're building shared libs and the binary is not static, relink # the handling with empty $relink_command is a hack for Mac OS - thelibdir="`pwd`$(libdir)"; progdir="`pwd`$(bindir)"; file=cvc4; \ - eval `grep '^relink_command=' $(CURRENT_BUILD)/src/main/cvc4 | sed 's:-Wl,-rpath:-Wl,-rpath -Wl,\\\\$$thelibdir -Wl,-rpath:'`; \ - if test -z "$$relink_command"; then \ - $(mkinstalldirs) ".$(bindir)/.libs"; \ - $(install_sh) \ - $(CURRENT_BUILD)/src/main/.libs/cvc4 \ - "`pwd`$(bindir)/.libs"; \ - $(install_sh) \ - $(CURRENT_BUILD)/src/main/cvc4 \ - "`pwd`$(bindir)"; \ + $(AM_V_at)thelibdir="`pwd`$(libdir)"; progdir="`pwd`$(bindir)"; for file in $(CVC4_BINARIES); do \ + if test -r $(CURRENT_BUILD)/src/main/$$file; then \ + eval `grep '^relink_command=' $(CURRENT_BUILD)/src/main/$$file | sed 's:-Wl,-rpath:-Wl,-rpath -Wl,\\\\$$thelibdir -Wl,-rpath:'`; \ + if test -z "$$relink_command"; then \ + $(AM_V_mkdir_noat) ".$(bindir)/.libs"; \ + $(AM_V_install_sh_noat) \ + $(CURRENT_BUILD)/src/main/.libs/$$file \ + "`pwd`$(bindir)/.libs"; \ + $(AM_V_install_sh_noat) \ + $(CURRENT_BUILD)/src/main/$$file \ + "`pwd`$(bindir)"; \ + else \ + $(AM_V_relink) "$$file"; eval "(cd $(CURRENT_BUILD)/src/main && $$relink_command)"; \ + fi; \ else \ - eval "(cd $(CURRENT_BUILD)/src/main && $$relink_command)"; \ - fi + rm -f "`pwd`$(bindir)/$$file"; \ + fi; \ + done else # if we're building static libs only, just install the driver binary directly - $(install_sh) $(CURRENT_BUILD)/src/main/cvc4 "`pwd`$(bindir)" + $(AM_V_at)for file in $(CVC4_BINARIES); do \ + if test -r $(CURRENT_BUILD)/src/main/$$file; then \ + $(AM_V_install_sh_noat) \ + $(CURRENT_BUILD)/src/main/$$file \ + "`pwd`$(bindir)"; \ + else \ + rm -f "`pwd`$(bindir)/$$file"; \ + fi; \ + done endif # set up builds/bin and builds/lib - test -e lib || ln -sfv ".$(libdir)" lib - test -e bin || ln -sfv ".$(bindir)" bin + $(AM_V_at)test -e lib || ln -sfv ".$(libdir)" lib + $(AM_V_at)test -e bin || ln -sfv ".$(bindir)" bin rm -f examples; ln -sf "$(CURRENT_BUILD)/examples" examples # The descent into "src" with target "check" is to build check diff --git a/README b/README index 23fdf9a51..981eeaa60 100644 --- a/README +++ b/README @@ -37,6 +37,7 @@ GNU C and C++ (gcc and g++), reasonably recent versions GNU Make GNU Bash GMP v4.2 (GNU Multi-Precision arithmetic library) +The Boost C++ threading library (libboost_thread) libantlr3c v3.2 (ANTLR parser generator) Optional: CLN v1.3 (Class Library for Numbers) Optional: CUDD v2.4.2 (Colorado University Decision Diagram package) diff --git a/config/boost.m4 b/config/boost.m4 new file mode 100644 index 000000000..b9c60d9c3 --- /dev/null +++ b/config/boost.m4 @@ -0,0 +1,1044 @@ +# boost.m4: Locate Boost headers and libraries for autoconf-based projects. +# Copyright (C) 2007, 2008, 2009, 2010 Benoit Sigoure +# +# This program is free software: you can redistribute it and/or modify +# it under the terms of the GNU General Public License as published by +# the Free Software Foundation, either version 3 of the License, or +# (at your option) any later version. +# +# Additional permission under section 7 of the GNU General Public +# License, version 3 ("GPLv3"): +# +# If you convey this file as part of a work that contains a +# configuration script generated by Autoconf, you may do so under +# terms of your choice. +# +# This program is distributed in the hope that it will be useful, +# but WITHOUT ANY WARRANTY; without even the implied warranty of +# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +# GNU General Public License for more details. +# +# You should have received a copy of the GNU General Public License +# along with this program. If not, see . + +m4_define([_BOOST_SERIAL], [m4_translit([ +# serial 13 +], [# +], [])]) + +# Original sources can be found at http://github.com/tsuna/boost.m4 +# You can fetch the latest version of the script by doing: +# wget http://github.com/tsuna/boost.m4/raw/master/build-aux/boost.m4 + +# ------ # +# README # +# ------ # + +# This file provides several macros to use the various Boost libraries. +# The first macro is BOOST_REQUIRE. It will simply check if it's possible to +# find the Boost headers of a given (optional) minimum version and it will +# define BOOST_CPPFLAGS accordingly. It will add an option --with-boost to +# your configure so that users can specify non standard locations. +# If the user's environment contains BOOST_ROOT and --with-boost was not +# specified, --with-boost=$BOOST_ROOT is implicitly used. +# For more README and documentation, go to http://github.com/tsuna/boost.m4 +# Note: THESE MACROS ASSUME THAT YOU USE LIBTOOL. If you don't, don't worry, +# simply read the README, it will show you what to do step by step. + +m4_pattern_forbid([^_?BOOST_]) + + +# _BOOST_SED_CPP(SED-PROGRAM, PROGRAM, +# [ACTION-IF-FOUND], [ACTION-IF-NOT-FOUND]) +# -------------------------------------------------------- +# Same as AC_EGREP_CPP, but leave the result in conftest.i. +# PATTERN is *not* overquoted, as in AC_EGREP_CPP. It could be useful +# to turn this into a macro which extracts the value of any macro. +m4_define([_BOOST_SED_CPP], +[AC_LANG_PREPROC_REQUIRE()dnl +AC_REQUIRE([AC_PROG_SED])dnl +AC_LANG_CONFTEST([AC_LANG_SOURCE([[$2]])]) +AS_IF([dnl eval is necessary to expand ac_cpp. +dnl Ultrix and Pyramid sh refuse to redirect output of eval, so use subshell. +dnl Beware of Windows end-of-lines, for instance if we are running +dnl some Windows programs under Wine. In that case, boost/version.hpp +dnl is certainly using "\r\n", but the regular Unix shell will only +dnl strip `\n' with backquotes, not the `\r'. This results in +dnl boost_cv_lib_version='1_37\r' for instance, which breaks +dnl everything else. +dnl Cannot use 'dnl' after [$4] because a trailing dnl may break AC_CACHE_CHECK +(eval "$ac_cpp conftest.$ac_ext") 2>&AS_MESSAGE_LOG_FD | + tr -d '\r' | + $SED -n -e "$1" >conftest.i 2>&1], + [$3], + [$4]) +rm -rf conftest* +])# AC_EGREP_CPP + + + +# BOOST_REQUIRE([VERSION], [ACTION-IF-NOT-FOUND]) +# ----------------------------------------------- +# Look for Boost. If version is given, it must either be a literal of the form +# "X.Y.Z" where X, Y and Z are integers (the ".Z" part being optional) or a +# variable "$var". +# Defines the value BOOST_CPPFLAGS. This macro only checks for headers with +# the required version, it does not check for any of the Boost libraries. +# On # success, defines HAVE_BOOST. On failure, calls the optional +# ACTION-IF-NOT-FOUND action if one was supplied. +# Otherwise aborts with an error message. +AC_DEFUN([BOOST_REQUIRE], +[AC_REQUIRE([AC_PROG_CXX])dnl +AC_REQUIRE([AC_PROG_GREP])dnl +echo "$as_me: this is boost.m4[]_BOOST_SERIAL" >&AS_MESSAGE_LOG_FD +boost_save_IFS=$IFS +boost_version_req=$1 +IFS=. +set x $boost_version_req 0 0 0 +IFS=$boost_save_IFS +shift +boost_version_req=`expr "$[1]" '*' 100000 + "$[2]" '*' 100 + "$[3]"` +boost_version_req_string=$[1].$[2].$[3] +AC_ARG_WITH([boost], + [AS_HELP_STRING([--with-boost=DIR], + [prefix of Boost $1 @<:@guess@:>@])])dnl +AC_ARG_VAR([BOOST_ROOT],[Location of Boost installation])dnl +# If BOOST_ROOT is set and the user has not provided a value to +# --with-boost, then treat BOOST_ROOT as if it the user supplied it. +if test x"$BOOST_ROOT" != x; then + if test x"$with_boost" = x; then + AC_MSG_NOTICE([Detected BOOST_ROOT; continuing with --with-boost=$BOOST_ROOT]) + with_boost=$BOOST_ROOT + else + AC_MSG_NOTICE([Detected BOOST_ROOT=$BOOST_ROOT, but overridden by --with-boost=$with_boost]) + fi +fi +AC_SUBST([DISTCHECK_CONFIGURE_FLAGS], + ["$DISTCHECK_CONFIGURE_FLAGS '--with-boost=$with_boost'"]) +boost_save_CPPFLAGS=$CPPFLAGS + AC_CACHE_CHECK([for Boost headers version >= $boost_version_req_string], + [boost_cv_inc_path], + [boost_cv_inc_path=no +AC_LANG_PUSH([C++])dnl +m4_pattern_allow([^BOOST_VERSION$])dnl + AC_LANG_CONFTEST([AC_LANG_PROGRAM([[#include +#if !defined BOOST_VERSION +# error BOOST_VERSION is not defined +#elif BOOST_VERSION < $boost_version_req +# error Boost headers version < $boost_version_req +#endif +]])]) + # If the user provided a value to --with-boost, use it and only it. + case $with_boost in #( + ''|yes) set x '' /opt/local/include /usr/local/include /opt/include \ + /usr/include C:/Boost/include;; #( + *) set x "$with_boost/include" "$with_boost";; + esac + shift + for boost_dir + do + # Without --layout=system, Boost (or at least some versions) installs + # itself in /include/boost-. This inner loop helps to + # find headers in such directories. + # + # Any ${boost_dir}/boost-x_xx directories are searched in reverse version + # order followed by ${boost_dir}. The final '.' is a sentinel for + # searching $boost_dir" itself. Entries are whitespace separated. + # + # I didn't indent this loop on purpose (to avoid over-indented code) + boost_layout_system_search_list=`cd "$boost_dir" 2>/dev/null \ + && ls -1 | "${GREP}" '^boost-' | sort -rn -t- -k2 \ + && echo .` + for boost_inc in $boost_layout_system_search_list + do + if test x"$boost_inc" != x.; then + boost_inc="$boost_dir/$boost_inc" + else + boost_inc="$boost_dir" # Uses sentinel in boost_layout_system_search_list + fi + if test x"$boost_inc" != x; then + # We are going to check whether the version of Boost installed + # in $boost_inc is usable by running a compilation that + # #includes it. But if we pass a -I/some/path in which Boost + # is not installed, the compiler will just skip this -I and + # use other locations (either from CPPFLAGS, or from its list + # of system include directories). As a result we would use + # header installed on the machine instead of the /some/path + # specified by the user. So in that precise case (trying + # $boost_inc), make sure the version.hpp exists. + # + # Use test -e as there can be symlinks. + test -e "$boost_inc/boost/version.hpp" || continue + CPPFLAGS="$CPPFLAGS -I$boost_inc" + fi + AC_COMPILE_IFELSE([], [boost_cv_inc_path=yes], [boost_cv_version=no]) + if test x"$boost_cv_inc_path" = xyes; then + if test x"$boost_inc" != x; then + boost_cv_inc_path=$boost_inc + fi + break 2 + fi + done + done +AC_LANG_POP([C++])dnl + ]) + case $boost_cv_inc_path in #( + no) + boost_errmsg="cannot find Boost headers version >= $boost_version_req_string" + m4_if([$2], [], [AC_MSG_ERROR([$boost_errmsg])], + [AC_MSG_NOTICE([$boost_errmsg])]) + $2 + ;;#( + yes) + BOOST_CPPFLAGS= + ;;#( + *) + AC_SUBST([BOOST_CPPFLAGS], ["-I$boost_cv_inc_path"]) + ;; + esac + if test x"$boost_cv_inc_path" != xno; then + AC_DEFINE([HAVE_BOOST], [1], + [Defined if the requested minimum BOOST version is satisfied]) + AC_CACHE_CHECK([for Boost's header version], + [boost_cv_lib_version], + [m4_pattern_allow([^BOOST_LIB_VERSION$])dnl + _BOOST_SED_CPP([/^boost-lib-version = /{s///;s/\"//g;p;g;}], + [#include +boost-lib-version = BOOST_LIB_VERSION], + [boost_cv_lib_version=`cat conftest.i`])]) + # e.g. "134" for 1_34_1 or "135" for 1_35 + boost_major_version=`echo "$boost_cv_lib_version" | sed 's/_//;s/_.*//'` + case $boost_major_version in #( + '' | *[[!0-9]]*) + AC_MSG_ERROR([invalid value: boost_major_version=$boost_major_version]) + ;; + esac +fi +CPPFLAGS=$boost_save_CPPFLAGS +])# BOOST_REQUIRE + +# BOOST_STATIC() +# -------------- +# Add the "--enable-static-boost" configure argument. If this argument is given +# on the command line, static versions of the libraries will be looked up. +AC_DEFUN([BOOST_STATIC], + [AC_ARG_ENABLE([static-boost], + [AC_HELP_STRING([--enable-static-boost], + [Prefer the static boost libraries over the shared ones [no]])], + [enable_static_boost=yes], + [enable_static_boost=no])])# BOOST_STATIC + +# BOOST_FIND_HEADER([HEADER-NAME], [ACTION-IF-NOT-FOUND], [ACTION-IF-FOUND]) +# -------------------------------------------------------------------------- +# Wrapper around AC_CHECK_HEADER for Boost headers. Useful to check for +# some parts of the Boost library which are only made of headers and don't +# require linking (such as Boost.Foreach). +# +# Default ACTION-IF-NOT-FOUND: Fail with a fatal error unless Boost couldn't be +# found in the first place, in which case by default a notice is issued to the +# user. Presumably if we haven't died already it's because it's OK to not have +# Boost, which is why only a notice is issued instead of a hard error. +# +# Default ACTION-IF-FOUND: define the preprocessor symbol HAVE_ in +# case of success # (where HEADER-NAME is written LIKE_THIS, e.g., +# HAVE_BOOST_FOREACH_HPP). +AC_DEFUN([BOOST_FIND_HEADER], +[AC_REQUIRE([BOOST_REQUIRE])dnl +if test x"$boost_cv_inc_path" = xno; then + m4_default([$2], [AC_MSG_NOTICE([Boost not available, not searching for $1])]) +else +AC_LANG_PUSH([C++])dnl +boost_save_CPPFLAGS=$CPPFLAGS +CPPFLAGS="$CPPFLAGS $BOOST_CPPFLAGS" +AC_CHECK_HEADER([$1], + [m4_default([$3], [AC_DEFINE(AS_TR_CPP([HAVE_$1]), [1], + [Define to 1 if you have <$1>])])], + [m4_default([$2], [AC_MSG_ERROR([cannot find $1])])]) +CPPFLAGS=$boost_save_CPPFLAGS +AC_LANG_POP([C++])dnl +fi +])# BOOST_FIND_HEADER + + +# BOOST_FIND_LIB([LIB-NAME], [PREFERRED-RT-OPT], [HEADER-NAME], [CXX-TEST], +# [CXX-PROLOGUE]) +# ------------------------------------------------------------------------- +# Look for the Boost library LIB-NAME (e.g., LIB-NAME = `thread', for +# libboost_thread). Check that HEADER-NAME works and check that +# libboost_LIB-NAME can link with the code CXX-TEST. The optional argument +# CXX-PROLOGUE can be used to include some C++ code before the `main' +# function. +# +# Invokes BOOST_FIND_HEADER([HEADER-NAME]) (see above). +# +# Boost libraries typically come compiled with several flavors (with different +# runtime options) so PREFERRED-RT-OPT is the preferred suffix. A suffix is one +# or more of the following letters: sgdpn (in that order). s = static +# runtime, d = debug build, g = debug/diagnostic runtime, p = STLPort build, +# n = (unsure) STLPort build without iostreams from STLPort (it looks like `n' +# must always be used along with `p'). Additionally, PREFERRED-RT-OPT can +# start with `mt-' to indicate that there is a preference for multi-thread +# builds. Some sample values for PREFERRED-RT-OPT: (nothing), mt, d, mt-d, gdp +# ... If you want to make sure you have a specific version of Boost +# (eg, >= 1.33) you *must* invoke BOOST_REQUIRE before this macro. +AC_DEFUN([BOOST_FIND_LIB], +[AC_REQUIRE([BOOST_REQUIRE])dnl +AC_REQUIRE([_BOOST_FIND_COMPILER_TAG])dnl +AC_REQUIRE([BOOST_STATIC])dnl +AC_REQUIRE([_BOOST_GUESS_WHETHER_TO_USE_MT])dnl +if test x"$boost_cv_inc_path" = xno; then + AC_MSG_NOTICE([Boost not available, not searching for the Boost $1 library]) +else +dnl The else branch is huge and wasn't intended on purpose. +AC_LANG_PUSH([C++])dnl +AS_VAR_PUSHDEF([Boost_lib], [boost_cv_lib_$1])dnl +AS_VAR_PUSHDEF([Boost_lib_LDFLAGS], [boost_cv_lib_$1_LDFLAGS])dnl +AS_VAR_PUSHDEF([Boost_lib_LDPATH], [boost_cv_lib_$1_LDPATH])dnl +AS_VAR_PUSHDEF([Boost_lib_LIBS], [boost_cv_lib_$1_LIBS])dnl +BOOST_FIND_HEADER([$3]) +boost_save_CPPFLAGS=$CPPFLAGS +CPPFLAGS="$CPPFLAGS $BOOST_CPPFLAGS" +# Now let's try to find the library. The algorithm is as follows: first look +# for a given library name according to the user's PREFERRED-RT-OPT. For each +# library name, we prefer to use the ones that carry the tag (toolset name). +# Each library is searched through the various standard paths were Boost is +# usually installed. If we can't find the standard variants, we try to +# enforce -mt (for instance on MacOSX, libboost_threads.dylib doesn't exist +# but there's -obviously- libboost_threads-mt.dylib). +AC_CACHE_CHECK([for the Boost $1 library], [Boost_lib], + [Boost_lib=no + case "$2" in #( + mt | mt-) boost_mt=-mt; boost_rtopt=;; #( + mt* | mt-*) boost_mt=-mt; boost_rtopt=`expr "X$2" : 'Xmt-*\(.*\)'`;; #( + *) boost_mt=; boost_rtopt=$2;; + esac + if test $enable_static_boost = yes; then + boost_rtopt="s$boost_rtopt" + fi + # Find the proper debug variant depending on what we've been asked to find. + case $boost_rtopt in #( + *d*) boost_rt_d=$boost_rtopt;; #( + *[[sgpn]]*) # Insert the `d' at the right place (in between `sg' and `pn') + boost_rt_d=`echo "$boost_rtopt" | sed 's/\(s*g*\)\(p*n*\)/\1\2/'`;; #( + *) boost_rt_d='-d';; + esac + # If the PREFERRED-RT-OPT are not empty, prepend a `-'. + test -n "$boost_rtopt" && boost_rtopt="-$boost_rtopt" + $boost_guess_use_mt && boost_mt=-mt + # Look for the abs path the static archive. + # $libext is computed by Libtool but let's make sure it's non empty. + test -z "$libext" && + AC_MSG_ERROR([the libext variable is empty, did you invoke Libtool?]) + boost_save_ac_objext=$ac_objext + # Generate the test file. + AC_LANG_CONFTEST([AC_LANG_PROGRAM([#include <$3> +$5], [$4])]) +dnl Optimization hacks: compiling C++ is slow, especially with Boost. What +dnl we're trying to do here is guess the right combination of link flags +dnl (LIBS / LDFLAGS) to use a given library. This can take several +dnl iterations before it succeeds and is thus *very* slow. So what we do +dnl instead is that we compile the code first (and thus get an object file, +dnl typically conftest.o). Then we try various combinations of link flags +dnl until we succeed to link conftest.o in an executable. The problem is +dnl that the various TRY_LINK / COMPILE_IFELSE macros of Autoconf always +dnl remove all the temporary files including conftest.o. So the trick here +dnl is to temporarily change the value of ac_objext so that conftest.o is +dnl preserved accross tests. This is obviously fragile and I will burn in +dnl hell for not respecting Autoconf's documented interfaces, but in the +dnl mean time, it optimizes the macro by a factor of 5 to 30. +dnl Another small optimization: the first argument of AC_COMPILE_IFELSE left +dnl empty because the test file is generated only once above (before we +dnl start the for loops). + AC_COMPILE_IFELSE([], + [ac_objext=do_not_rm_me_plz], + [AC_MSG_ERROR([cannot compile a test that uses Boost $1])]) + ac_objext=$boost_save_ac_objext + boost_failed_libs= +# Don't bother to ident the 6 nested for loops, only the 2 innermost ones +# matter. +for boost_tag_ in -$boost_cv_lib_tag ''; do +for boost_ver_ in -$boost_cv_lib_version ''; do +for boost_mt_ in $boost_mt -mt ''; do +for boost_rtopt_ in $boost_rtopt '' -d; do + for boost_lib in \ + boost_$1$boost_tag_$boost_mt_$boost_rtopt_$boost_ver_ \ + boost_$1$boost_tag_$boost_rtopt_$boost_ver_ \ + boost_$1$boost_tag_$boost_mt_$boost_ver_ \ + boost_$1$boost_tag_$boost_ver_ + do + # Avoid testing twice the same lib + case $boost_failed_libs in #( + *@$boost_lib@*) continue;; + esac + # If with_boost is empty, we'll search in /lib first, which is not quite + # right so instead we'll try to a location based on where the headers are. + boost_tmp_lib=$with_boost + test x"$with_boost" = x && boost_tmp_lib=${boost_cv_inc_path%/include} + for boost_ldpath in "$boost_tmp_lib/lib" '' \ + /opt/local/lib /usr/local/lib /opt/lib /usr/lib \ + "$with_boost" C:/Boost/lib /lib /usr/lib64 /lib64 + do + test -e "$boost_ldpath" || continue + boost_save_LDFLAGS=$LDFLAGS + # Are we looking for a static library? + case $boost_ldpath:$boost_rtopt_ in #( + *?*:*s*) # Yes (Non empty boost_ldpath + s in rt opt) + Boost_lib_LIBS="$boost_ldpath/lib$boost_lib.$libext" + test -e "$Boost_lib_LIBS" || continue;; #( + *) # No: use -lboost_foo to find the shared library. + Boost_lib_LIBS="-l$boost_lib";; + esac + boost_save_LIBS=$LIBS + LIBS="$Boost_lib_LIBS $LIBS" + test x"$boost_ldpath" != x && LDFLAGS="$LDFLAGS -L$boost_ldpath" +dnl First argument of AC_LINK_IFELSE left empty because the test file is +dnl generated only once above (before we start the for loops). + _BOOST_AC_LINK_IFELSE([], + [Boost_lib=yes], [Boost_lib=no]) + ac_objext=$boost_save_ac_objext + LDFLAGS=$boost_save_LDFLAGS + LIBS=$boost_save_LIBS + if test x"$Boost_lib" = xyes; then + Boost_lib_LDFLAGS="-L$boost_ldpath -R$boost_ldpath" + Boost_lib_LDPATH="$boost_ldpath" + break 6 + else + boost_failed_libs="$boost_failed_libs@$boost_lib@" + fi + done + done +done +done +done +done +rm -f conftest.$ac_objext +]) +case $Boost_lib in #( + no) _AC_MSG_LOG_CONFTEST + AC_MSG_ERROR([cannot not find the flags to link with Boost $1]) + ;; +esac +AC_SUBST(AS_TR_CPP([BOOST_$1_LDFLAGS]), [$Boost_lib_LDFLAGS]) +AC_SUBST(AS_TR_CPP([BOOST_$1_LDPATH]), [$Boost_lib_LDPATH]) +AC_SUBST([BOOST_LDPATH], [$Boost_lib_LDPATH]) +AC_SUBST(AS_TR_CPP([BOOST_$1_LIBS]), [$Boost_lib_LIBS]) +CPPFLAGS=$boost_save_CPPFLAGS +AS_VAR_POPDEF([Boost_lib])dnl +AS_VAR_POPDEF([Boost_lib_LDFLAGS])dnl +AS_VAR_POPDEF([Boost_lib_LDPATH])dnl +AS_VAR_POPDEF([Boost_lib_LIBS])dnl +AC_LANG_POP([C++])dnl +fi +])# BOOST_FIND_LIB + + +# --------------------------------------- # +# Checks for the various Boost libraries. # +# --------------------------------------- # + +# List of boost libraries: http://www.boost.org/libs/libraries.htm +# The page http://beta.boost.org/doc/libs is useful: it gives the first release +# version of each library (among other things). + +# BOOST_ARRAY() +# ------------- +# Look for Boost.Array +AC_DEFUN([BOOST_ARRAY], +[BOOST_FIND_HEADER([boost/array.hpp])]) + + +# BOOST_ASIO() +# ------------ +# Look for Boost.Asio (new in Boost 1.35). +AC_DEFUN([BOOST_ASIO], +[AC_REQUIRE([BOOST_SYSTEM])dnl +BOOST_FIND_HEADER([boost/asio.hpp])]) + + +# BOOST_BIND() +# ------------ +# Look for Boost.Bind +AC_DEFUN([BOOST_BIND], +[BOOST_FIND_HEADER([boost/bind.hpp])]) + + +# BOOST_CONVERSION() +# ------------------ +# Look for Boost.Conversion (cast / lexical_cast) +AC_DEFUN([BOOST_CONVERSION], +[BOOST_FIND_HEADER([boost/cast.hpp]) +BOOST_FIND_HEADER([boost/lexical_cast.hpp]) +])# BOOST_CONVERSION + + +# BOOST_DATE_TIME([PREFERRED-RT-OPT]) +# ----------------------------------- +# Look for Boost.Date_Time. For the documentation of PREFERRED-RT-OPT, see the +# documentation of BOOST_FIND_LIB above. +AC_DEFUN([BOOST_DATE_TIME], +[BOOST_FIND_LIB([date_time], [$1], + [boost/date_time/posix_time/posix_time.hpp], + [boost::posix_time::ptime t;]) +])# BOOST_DATE_TIME + + +# BOOST_FILESYSTEM([PREFERRED-RT-OPT]) +# ------------------------------------ +# Look for Boost.Filesystem. For the documentation of PREFERRED-RT-OPT, see +# the documentation of BOOST_FIND_LIB above. +# Do not check for boost/filesystem.hpp because this file was introduced in +# 1.34. +AC_DEFUN([BOOST_FILESYSTEM], +[# Do we have to check for Boost.System? This link-time dependency was +# added as of 1.35.0. If we have a version <1.35, we must not attempt to +# find Boost.System as it didn't exist by then. +if test $boost_major_version -ge 135; then +BOOST_SYSTEM([$1]) +fi # end of the Boost.System check. +boost_filesystem_save_LIBS=$LIBS +boost_filesystem_save_LDFLAGS=$LDFLAGS +m4_pattern_allow([^BOOST_SYSTEM_(LIBS|LDFLAGS)$])dnl +LIBS="$LIBS $BOOST_SYSTEM_LIBS" +LDFLAGS="$LDFLAGS $BOOST_SYSTEM_LDFLAGS" +BOOST_FIND_LIB([filesystem], [$1], + [boost/filesystem/path.hpp], [boost::filesystem::path p;]) +LIBS=$boost_filesystem_save_LIBS +LDFLAGS=$boost_filesystem_save_LDFLAGS +])# BOOST_FILESYSTEM + + +# BOOST_FOREACH() +# --------------- +# Look for Boost.Foreach +AC_DEFUN([BOOST_FOREACH], +[BOOST_FIND_HEADER([boost/foreach.hpp])]) + + +# BOOST_FORMAT() +# -------------- +# Look for Boost.Format +# Note: we can't check for boost/format/format_fwd.hpp because the header isn't +# standalone. It can't be compiled because it triggers the following error: +# boost/format/detail/config_macros.hpp:88: error: 'locale' in namespace 'std' +# does not name a type +AC_DEFUN([BOOST_FORMAT], +[BOOST_FIND_HEADER([boost/format.hpp])]) + + +# BOOST_FUNCTION() +# ---------------- +# Look for Boost.Function +AC_DEFUN([BOOST_FUNCTION], +[BOOST_FIND_HEADER([boost/function.hpp])]) + + +# BOOST_GRAPH([PREFERRED-RT-OPT]) +# ------------------------------- +# Look for Boost.Graphs. For the documentation of PREFERRED-RT-OPT, see the +# documentation of BOOST_FIND_LIB above. +AC_DEFUN([BOOST_GRAPH], +[BOOST_FIND_LIB([graph], [$1], + [boost/graph/adjacency_list.hpp], [boost::adjacency_list<> g;]) +])# BOOST_GRAPH + + +# BOOST_IOSTREAMS([PREFERRED-RT-OPT]) +# ------------------------------- +# Look for Boost.IOStreams. For the documentation of PREFERRED-RT-OPT, see the +# documentation of BOOST_FIND_LIB above. +AC_DEFUN([BOOST_IOSTREAMS], +[BOOST_FIND_LIB([iostreams], [$1], + [boost/iostreams/device/file_descriptor.hpp], + [boost::iostreams::file_descriptor fd; fd.close();]) +])# BOOST_IOSTREAMS + + +# BOOST_HASH() +# ------------ +# Look for Boost.Functional/Hash +AC_DEFUN([BOOST_HASH], +[BOOST_FIND_HEADER([boost/functional/hash.hpp])]) + + +# BOOST_LAMBDA() +# -------------- +# Look for Boost.Lambda +AC_DEFUN([BOOST_LAMBDA], +[BOOST_FIND_HEADER([boost/lambda/lambda.hpp])]) + + +# BOOST_MATH() +# ------------ +# Look for Boost.Math +# TODO: This library isn't header-only but it comes in multiple different +# flavors that don't play well with BOOST_FIND_LIB (e.g, libboost_math_c99, +# libboost_math_c99f, libboost_math_c99l, libboost_math_tr1, +# libboost_math_tr1f, libboost_math_tr1l). This macro must be fixed to do the +# right thing anyway. +AC_DEFUN([BOOST_MATH], +[BOOST_FIND_HEADER([boost/math/special_functions.hpp])]) + + +# BOOST_MULTIARRAY() +# ------------------ +# Look for Boost.MultiArray +AC_DEFUN([BOOST_MULTIARRAY], +[BOOST_FIND_HEADER([boost/multi_array.hpp])]) + + +# BOOST_NUMERIC_CONVERSION() +# -------------------------- +# Look for Boost.NumericConversion (policy-based numeric conversion) +AC_DEFUN([BOOST_NUMERIC_CONVERSION], +[BOOST_FIND_HEADER([boost/numeric/conversion/converter.hpp]) +])# BOOST_NUMERIC_CONVERSION + + +# BOOST_OPTIONAL() +# ---------------- +# Look for Boost.Optional +AC_DEFUN([BOOST_OPTIONAL], +[BOOST_FIND_HEADER([boost/optional.hpp])]) + + +# BOOST_PREPROCESSOR() +# -------------------- +# Look for Boost.Preprocessor +AC_DEFUN([BOOST_PREPROCESSOR], +[BOOST_FIND_HEADER([boost/preprocessor/repeat.hpp])]) + + +# BOOST_PROGRAM_OPTIONS([PREFERRED-RT-OPT]) +# ----------------------------------------- +# Look for Boost.Program_options. For the documentation of PREFERRED-RT-OPT, see +# the documentation of BOOST_FIND_LIB above. +AC_DEFUN([BOOST_PROGRAM_OPTIONS], +[BOOST_FIND_LIB([program_options], [$1], + [boost/program_options.hpp], + [boost::program_options::options_description d("test");]) +])# BOOST_PROGRAM_OPTIONS + + +# BOOST_REF() +# ----------- +# Look for Boost.Ref +AC_DEFUN([BOOST_REF], +[BOOST_FIND_HEADER([boost/ref.hpp])]) + + +# BOOST_REGEX([PREFERRED-RT-OPT]) +# ------------------------------- +# Look for Boost.Regex. For the documentation of PREFERRED-RT-OPT, see the +# documentation of BOOST_FIND_LIB above. +AC_DEFUN([BOOST_REGEX], +[BOOST_FIND_LIB([regex], [$1], + [boost/regex.hpp], + [boost::regex exp("*"); boost::regex_match("foo", exp);]) +])# BOOST_REGEX + + +# BOOST_SERIALIZATION([PREFERRED-RT-OPT]) +# --------------------------------------- +# Look for Boost.Serialization. For the documentation of PREFERRED-RT-OPT, see +# the documentation of BOOST_FIND_LIB above. +AC_DEFUN([BOOST_SERIALIZATION], +[BOOST_FIND_LIB([serialization], [$1], + [boost/archive/text_oarchive.hpp], + [std::ostream* o = 0; // Cheap way to get an ostream... + boost::archive::text_oarchive t(*o);]) +])# BOOST_SIGNALS + + +# BOOST_SIGNALS([PREFERRED-RT-OPT]) +# --------------------------------- +# Look for Boost.Signals. For the documentation of PREFERRED-RT-OPT, see the +# documentation of BOOST_FIND_LIB above. +AC_DEFUN([BOOST_SIGNALS], +[BOOST_FIND_LIB([signals], [$1], + [boost/signal.hpp], + [boost::signal s;]) +])# BOOST_SIGNALS + + +# BOOST_SMART_PTR() +# ----------------- +# Look for Boost.SmartPtr +AC_DEFUN([BOOST_SMART_PTR], +[BOOST_FIND_HEADER([boost/scoped_ptr.hpp]) +BOOST_FIND_HEADER([boost/shared_ptr.hpp]) +]) + + +# BOOST_STATICASSERT() +# -------------------- +# Look for Boost.StaticAssert +AC_DEFUN([BOOST_STATICASSERT], +[BOOST_FIND_HEADER([boost/static_assert.hpp])]) + + +# BOOST_STRING_ALGO() +# ------------------- +# Look for Boost.StringAlgo +AC_DEFUN([BOOST_STRING_ALGO], +[BOOST_FIND_HEADER([boost/algorithm/string.hpp]) +]) + + +# BOOST_SYSTEM([PREFERRED-RT-OPT]) +# -------------------------------- +# Look for Boost.System. For the documentation of PREFERRED-RT-OPT, see the +# documentation of BOOST_FIND_LIB above. This library was introduced in Boost +# 1.35.0. +AC_DEFUN([BOOST_SYSTEM], +[BOOST_FIND_LIB([system], [$1], + [boost/system/error_code.hpp], + [boost::system::error_code e; e.clear();]) +])# BOOST_SYSTEM + + +# BOOST_TEST([PREFERRED-RT-OPT]) +# ------------------------------ +# Look for Boost.Test. For the documentation of PREFERRED-RT-OPT, see the +# documentation of BOOST_FIND_LIB above. +AC_DEFUN([BOOST_TEST], +[m4_pattern_allow([^BOOST_CHECK$])dnl +BOOST_FIND_LIB([unit_test_framework], [$1], + [boost/test/unit_test.hpp], [BOOST_CHECK(2 == 2);], + [using boost::unit_test::test_suite; + test_suite* init_unit_test_suite(int argc, char ** argv) + { return NULL; }]) +])# BOOST_TEST + + +# BOOST_THREADS([PREFERRED-RT-OPT]) +# --------------------------------- +# Look for Boost.Thread. For the documentation of PREFERRED-RT-OPT, see the +# documentation of BOOST_FIND_LIB above. +# FIXME: Provide an alias "BOOST_THREAD". +AC_DEFUN([BOOST_THREADS], +[dnl Having the pthread flag is required at least on GCC3 where +dnl boost/thread.hpp would complain if we try to compile without +dnl -pthread on GNU/Linux. +AC_REQUIRE([_BOOST_PTHREAD_FLAG])dnl +boost_threads_save_LIBS=$LIBS +boost_threads_save_CPPFLAGS=$CPPFLAGS +LIBS="$LIBS $boost_cv_pthread_flag" +# Yes, we *need* to put the -pthread thing in CPPFLAGS because with GCC3, +# boost/thread.hpp will trigger a #error if -pthread isn't used: +# boost/config/requires_threads.hpp:47:5: #error "Compiler threading support +# is not turned on. Please set the correct command line options for +# threading: -pthread (Linux), -pthreads (Solaris) or -mthreads (Mingw32)" +CPPFLAGS="$CPPFLAGS $boost_cv_pthread_flag" +BOOST_FIND_LIB([thread], [$1], + [boost/thread.hpp], [boost::thread t; boost::mutex m;]) +BOOST_THREAD_LIBS="$BOOST_THREAD_LIBS $boost_cv_pthread_flag" +BOOST_CPPFLAGS="$BOOST_CPPFLAGS $boost_cv_pthread_flag" +LIBS=$boost_threads_save_LIBS +CPPFLAGS=$boost_threads_save_CPPFLAGS +])# BOOST_THREADS + + +# BOOST_TOKENIZER() +# ----------------- +# Look for Boost.Tokenizer +AC_DEFUN([BOOST_TOKENIZER], +[BOOST_FIND_HEADER([boost/tokenizer.hpp])]) + + +# BOOST_TRIBOOL() +# --------------- +# Look for Boost.Tribool +AC_DEFUN([BOOST_TRIBOOL], +[BOOST_FIND_HEADER([boost/logic/tribool_fwd.hpp]) +BOOST_FIND_HEADER([boost/logic/tribool.hpp]) +]) + + +# BOOST_TUPLE() +# ------------- +# Look for Boost.Tuple +AC_DEFUN([BOOST_TUPLE], +[BOOST_FIND_HEADER([boost/tuple/tuple.hpp])]) + + +# BOOST_TYPETRAITS() +# -------------------- +# Look for Boost.TypeTraits +AC_DEFUN([BOOST_TYPETRAITS], +[BOOST_FIND_HEADER([boost/type_traits.hpp])]) + + +# BOOST_UTILITY() +# --------------- +# Look for Boost.Utility (noncopyable, result_of, base-from-member idiom, +# etc.) +AC_DEFUN([BOOST_UTILITY], +[BOOST_FIND_HEADER([boost/utility.hpp])]) + + +# BOOST_VARIANT() +# --------------- +# Look for Boost.Variant. +AC_DEFUN([BOOST_VARIANT], +[BOOST_FIND_HEADER([boost/variant/variant_fwd.hpp]) +BOOST_FIND_HEADER([boost/variant.hpp])]) + + +# BOOST_WAVE([PREFERRED-RT-OPT]) +# ------------------------------ +# NOTE: If you intend to use Wave/Spirit with thread support, make sure you +# call BOOST_THREADS first. +# Look for Boost.Wave. For the documentation of PREFERRED-RT-OPT, see the +# documentation of BOOST_FIND_LIB above. +AC_DEFUN([BOOST_WAVE], +[AC_REQUIRE([BOOST_FILESYSTEM])dnl +AC_REQUIRE([BOOST_DATE_TIME])dnl +boost_wave_save_LIBS=$LIBS +boost_wave_save_LDFLAGS=$LDFLAGS +m4_pattern_allow([^BOOST_((FILE)?SYSTEM|DATE_TIME|THREAD)_(LIBS|LDFLAGS)$])dnl +LIBS="$LIBS $BOOST_SYSTEM_LIBS $BOOST_FILESYSTEM_LIBS $BOOST_DATE_TIME_LIBS\ +$BOOST_THREAD_LIBS" +LDFLAGS="$LDFLAGS $BOOST_SYSTEM_LDFLAGS $BOOST_FILESYSTEM_LDFLAGS\ +$BOOST_DATE_TIME_LDFLAGS $BOOST_THREAD_LDFLAGS" +BOOST_FIND_LIB([wave], [$1], + [boost/wave.hpp], + [boost::wave::token_id id; get_token_name(id);]) +LIBS=$boost_wave_save_LIBS +LDFLAGS=$boost_wave_save_LDFLAGS +])# BOOST_WAVE + + +# BOOST_XPRESSIVE() +# ----------------- +# Look for Boost.Xpressive (new since 1.36.0). +AC_DEFUN([BOOST_XPRESSIVE], +[BOOST_FIND_HEADER([boost/xpressive/xpressive.hpp])]) + + +# ----------------- # +# Internal helpers. # +# ----------------- # + + +# _BOOST_PTHREAD_FLAG() +# --------------------- +# Internal helper for BOOST_THREADS. Based on ACX_PTHREAD: +# http://autoconf-archive.cryp.to/acx_pthread.html +AC_DEFUN([_BOOST_PTHREAD_FLAG], +[AC_REQUIRE([AC_PROG_CXX])dnl +AC_REQUIRE([AC_CANONICAL_HOST])dnl +AC_LANG_PUSH([C++])dnl +AC_CACHE_CHECK([for the flags needed to use pthreads], [boost_cv_pthread_flag], +[ boost_cv_pthread_flag= + # The ordering *is* (sometimes) important. Some notes on the + # individual items follow: + # (none): in case threads are in libc; should be tried before -Kthread and + # other compiler flags to prevent continual compiler warnings + # -lpthreads: AIX (must check this before -lpthread) + # -Kthread: Sequent (threads in libc, but -Kthread needed for pthread.h) + # -kthread: FreeBSD kernel threads (preferred to -pthread since SMP-able) + # -llthread: LinuxThreads port on FreeBSD (also preferred to -pthread) + # -pthread: GNU Linux/GCC (kernel threads), BSD/GCC (userland threads) + # -pthreads: Solaris/GCC + # -mthreads: MinGW32/GCC, Lynx/GCC + # -mt: Sun Workshop C (may only link SunOS threads [-lthread], but it + # doesn't hurt to check since this sometimes defines pthreads too; + # also defines -D_REENTRANT) + # ... -mt is also the pthreads flag for HP/aCC + # -lpthread: GNU Linux, etc. + # --thread-safe: KAI C++ + case $host_os in #( + *solaris*) + # On Solaris (at least, for some versions), libc contains stubbed + # (non-functional) versions of the pthreads routines, so link-based + # tests will erroneously succeed. (We need to link with -pthreads/-mt/ + # -lpthread.) (The stubs are missing pthread_cleanup_push, or rather + # a function called by this macro, so we could check for that, but + # who knows whether they'll stub that too in a future libc.) So, + # we'll just look for -pthreads and -lpthread first: + boost_pthread_flags="-pthreads -lpthread -mt -pthread";; #( + *) + boost_pthread_flags="-lpthreads -Kthread -kthread -llthread -pthread \ + -pthreads -mthreads -lpthread --thread-safe -mt";; + esac + # Generate the test file. + AC_LANG_CONFTEST([AC_LANG_PROGRAM([#include ], + [pthread_t th; pthread_join(th, 0); + pthread_attr_init(0); pthread_cleanup_push(0, 0); + pthread_create(0,0,0,0); pthread_cleanup_pop(0);])]) + for boost_pthread_flag in '' $boost_pthread_flags; do + boost_pthread_ok=false +dnl Re-use the test file already generated. + boost_pthreads__save_LIBS=$LIBS + LIBS="$LIBS $boost_pthread_flag" + AC_LINK_IFELSE([], + [if grep ".*$boost_pthread_flag" conftest.err; then + echo "This flag seems to have triggered warnings" >&AS_MESSAGE_LOG_FD + else + boost_pthread_ok=:; boost_cv_pthread_flag=$boost_pthread_flag + fi]) + LIBS=$boost_pthreads__save_LIBS + $boost_pthread_ok && break + done +]) +AC_LANG_POP([C++])dnl +])# _BOOST_PTHREAD_FLAG + + +# _BOOST_gcc_test(MAJOR, MINOR) +# ----------------------------- +# Internal helper for _BOOST_FIND_COMPILER_TAG. +m4_define([_BOOST_gcc_test], +["defined __GNUC__ && __GNUC__ == $1 && __GNUC_MINOR__ == $2 && !defined __ICC @ gcc$1$2"])dnl + + +# _BOOST_FIND_COMPILER_TAG() +# -------------------------- +# Internal. When Boost is installed without --layout=system, each library +# filename will hold a suffix that encodes the compiler used during the +# build. The Boost build system seems to call this a `tag'. +AC_DEFUN([_BOOST_FIND_COMPILER_TAG], +[AC_REQUIRE([AC_PROG_CXX])dnl +AC_REQUIRE([AC_CANONICAL_HOST])dnl +AC_CACHE_CHECK([for the toolset name used by Boost for $CXX], [boost_cv_lib_tag], +[boost_cv_lib_tag=unknown +if test x$boost_cv_inc_path != xno; then + AC_LANG_PUSH([C++])dnl + # The following tests are mostly inspired by boost/config/auto_link.hpp + # The list is sorted to most recent/common to oldest compiler (in order + # to increase the likelihood of finding the right compiler with the + # least number of compilation attempt). + # Beware that some tests are sensible to the order (for instance, we must + # look for MinGW before looking for GCC3). + # I used one compilation test per compiler with a #error to recognize + # each compiler so that it works even when cross-compiling (let me know + # if you know a better approach). + # Known missing tags (known from Boost's tools/build/v2/tools/common.jam): + # como, edg, kcc, bck, mp, sw, tru, xlc + # I'm not sure about my test for `il' (be careful: Intel's ICC pre-defines + # the same defines as GCC's). + for i in \ + _BOOST_gcc_test(4, 5) \ + _BOOST_gcc_test(4, 4) \ + _BOOST_gcc_test(4, 3) \ + _BOOST_gcc_test(4, 2) \ + _BOOST_gcc_test(4, 1) \ + _BOOST_gcc_test(4, 0) \ + "defined __GNUC__ && __GNUC__ == 3 && !defined __ICC \ + && (defined WIN32 || defined WINNT || defined _WIN32 || defined __WIN32 \ + || defined __WIN32__ || defined __WINNT || defined __WINNT__) @ mgw" \ + _BOOST_gcc_test(3, 4) \ + _BOOST_gcc_test(3, 3) \ + "defined _MSC_VER && _MSC_VER >= 1500 @ vc90" \ + "defined _MSC_VER && _MSC_VER == 1400 @ vc80" \ + _BOOST_gcc_test(3, 2) \ + "defined _MSC_VER && _MSC_VER == 1310 @ vc71" \ + _BOOST_gcc_test(3, 1) \ + _BOOST_gcc_test(3, 0) \ + "defined __BORLANDC__ @ bcb" \ + "defined __ICC && (defined __unix || defined __unix__) @ il" \ + "defined __ICL @ iw" \ + "defined _MSC_VER && _MSC_VER == 1300 @ vc7" \ + _BOOST_gcc_test(2, 95) \ + "defined __MWERKS__ && __MWERKS__ <= 0x32FF @ cw9" \ + "defined _MSC_VER && _MSC_VER < 1300 && !defined UNDER_CE @ vc6" \ + "defined _MSC_VER && _MSC_VER < 1300 && defined UNDER_CE @ evc4" \ + "defined __MWERKS__ && __MWERKS__ <= 0x31FF @ cw8" + do + boost_tag_test=`expr "X$i" : 'X\([[^@]]*\) @ '` + boost_tag=`expr "X$i" : 'X[[^@]]* @ \(.*\)'` + AC_COMPILE_IFELSE([AC_LANG_PROGRAM([[ +#if $boost_tag_test +/* OK */ +#else +# error $boost_tag_test +#endif +]])], [boost_cv_lib_tag=$boost_tag; break], []) + done +AC_LANG_POP([C++])dnl + case $boost_cv_lib_tag in #( + # Some newer (>= 1.35?) versions of Boost seem to only use "gcc" as opposed + # to "gcc41" for instance. + *-gcc | *'-gcc ') :;; #( Don't re-add -gcc: it's already in there. + gcc*) + boost_tag_x= + case $host_os in #( + darwin*) + if test $boost_major_version -ge 136; then + # The `x' added in r46793 of Boost. + boost_tag_x=x + fi;; + esac + # We can specify multiple tags in this variable because it's used by + # BOOST_FIND_LIB that does a `for tag in -$boost_cv_lib_tag' ... + boost_cv_lib_tag="$boost_tag_x$boost_cv_lib_tag -${boost_tag_x}gcc" + ;; #( + unknown) + AC_MSG_WARN([[could not figure out which toolset name to use for $CXX]]) + boost_cv_lib_tag= + ;; + esac +fi])dnl end of AC_CACHE_CHECK +])# _BOOST_FIND_COMPILER_TAG + + +# _BOOST_GUESS_WHETHER_TO_USE_MT() +# -------------------------------- +# Compile a small test to try to guess whether we should favor MT (Multi +# Thread) flavors of Boost. Sets boost_guess_use_mt accordingly. +AC_DEFUN([_BOOST_GUESS_WHETHER_TO_USE_MT], +[# Check whether we do better use `mt' even though we weren't ask to. +AC_COMPILE_IFELSE([AC_LANG_PROGRAM([[ +#if defined _REENTRANT || defined _MT || defined __MT__ +/* use -mt */ +#else +# error MT not needed +#endif +]])], [boost_guess_use_mt=:], [boost_guess_use_mt=false]) +]) + +# _BOOST_AC_LINK_IFELSE(PROGRAM, [ACTION-IF-TRUE], [ACTION-IF-FALSE]) +# ------------------------------------------------------------------- +# Fork of _AC_LINK_IFELSE that preserves conftest.o across calls. Fragile, +# will break when Autoconf changes its internals. Requires that you manually +# rm -f conftest.$ac_objext in between to really different tests, otherwise +# you will try to link a conftest.o left behind by a previous test. +# Used to aggressively optimize BOOST_FIND_LIB (see the big comment in this +# macro). +# +# Don't use "break" in the actions, as it would short-circuit some code +# this macro runs after the actions. +m4_define([_BOOST_AC_LINK_IFELSE], +[m4_ifvaln([$1], [AC_LANG_CONFTEST([$1])])dnl +rm -f conftest$ac_exeext +boost_save_ac_ext=$ac_ext +boost_use_source=: +# If we already have a .o, re-use it. We change $ac_ext so that $ac_link +# tries to link the existing object file instead of compiling from source. +test -f conftest.$ac_objext && ac_ext=$ac_objext && boost_use_source=false && + _AS_ECHO_LOG([re-using the existing conftest.$ac_objext]) +AS_IF([_AC_DO_STDERR($ac_link) && { + test -z "$ac_[]_AC_LANG_ABBREV[]_werror_flag" || + test ! -s conftest.err + } && test -s conftest$ac_exeext && { + test "$cross_compiling" = yes || + $as_executable_p conftest$ac_exeext +dnl FIXME: use AS_TEST_X instead when 2.61 is widespread enough. + }], + [$2], + [if $boost_use_source; then + _AC_MSG_LOG_CONFTEST + fi + $3]) +ac_objext=$boost_save_ac_objext +ac_ext=$boost_save_ac_ext +dnl Delete also the IPA/IPO (Inter Procedural Analysis/Optimization) +dnl information created by the PGI compiler (conftest_ipa8_conftest.oo), +dnl as it would interfere with the next link command. +rm -f core conftest.err conftest_ipa8_conftest.oo \ + conftest$ac_exeext m4_ifval([$1], [conftest.$ac_ext])[]dnl +])# _BOOST_AC_LINK_IFELSE + +# Local Variables: +# mode: autoconf +# End: diff --git a/configure.ac b/configure.ac index a36a38636..3ea9d3457 100644 --- a/configure.ac +++ b/configure.ac @@ -842,6 +842,23 @@ AC_CHECK_HEADERS([getopt.h unistd.h]) #AC_TYPE_UINT64_T #AC_TYPE_SIZE_T +AC_CHECK_DECLS([optreset], [], [], [#include ]) + +# look for boost library, but don't make it a fatal error if not found +cvc4_has_threads=maybe +BOOST_REQUIRE([], [cvc4_has_threads=no]) +if test $cvc4_has_threads = no; then + AC_MSG_WARN([disabling multithreaded support]) +else + BOOST_THREADS + if test -n "$BOOST_THREAD_LIBS"; then + cvc4_has_threads=yes + else + AC_MSG_WARN([disabling multithreaded support]) + cvc4_has_threads=no + fi +fi + # Whether to build compatibility library CVC4_BUILD_LIBCOMPAT=yes AC_ARG_WITH([compat], @@ -859,18 +876,28 @@ AM_CONDITIONAL([CVC4_BUILD_LIBCOMPAT], [test "$CVC4_BUILD_LIBCOMPAT" = yes]) # Check for availability of TLS support (e.g. __thread storage class) AC_MSG_CHECKING([whether to use compiler-supported TLS if available]) AC_ARG_ENABLE([tls], AS_HELP_STRING([--disable-tls], [don't use compiler-native TLS])) -if test -z "${enable_tls+set}" || test "$enable_tls" = "yes"; then - AC_MSG_RESULT([yes]) - AX_TLS([CVC4_TLS=$ac_cv_tls], [CVC4_TLS=]) -else - AC_MSG_RESULT([no]) - CVC4_TLS= -fi -if test -n "$CVC4_TLS"; then +if test $cvc4_has_threads = no; then + # We disable TLS entirely by simply telling the build system that + # the empty string is the __thread keyword. + AC_MSG_RESULT([multithreading disabled]) CVC4_TLS_SUPPORTED=1 + CVC4_TLS= + CVC4_TLS_explanation='disabled (no multithreading support)' else - CVC4_TLS='pthread_getspecific()' - CVC4_TLS_SUPPORTED=0 + if test -z "${enable_tls+set}" || test "$enable_tls" = "yes"; then + AC_MSG_RESULT([yes]) + AX_TLS([CVC4_TLS=$ac_cv_tls], [CVC4_TLS=]) + else + AC_MSG_RESULT([no]) + CVC4_TLS= + fi + if test -n "$CVC4_TLS"; then + CVC4_TLS_SUPPORTED=1 + CVC4_TLS_explanation="$CVC4_TLS" + else + CVC4_TLS_explanation='pthread_getspecific()' + CVC4_TLS_SUPPORTED=0 + fi fi AC_SUBST([CVC4_TLS]) AC_SUBST([CVC4_TLS_SUPPORTED]) @@ -1001,6 +1028,16 @@ AC_CONFIG_FILES([ m4_esyscmd([find contrib src test examples -name Makefile.am | grep -v '^contrib/theoryskel/' | sort | sed 's,\.am$,,']) ) +if test $cvc4_has_threads = yes; then + support_multithreaded='with boost threading library' + AM_CONDITIONAL([CVC4_HAS_THREADS], [true]) + AC_SUBST([CVC4_HAS_THREADS], 1) +else + support_multithreaded='no' + AM_CONDITIONAL([CVC4_HAS_THREADS], [false]) + AC_SUBST([CVC4_HAS_THREADS], 0) +fi + CVC4_CONFIG_FILE_ONLY_IF_CHANGED([src/util/rational.h]) CVC4_CONFIG_FILE_ONLY_IF_CHANGED([src/util/integer.h]) CVC4_CONFIG_FILE_ONLY_IF_CHANGED([src/util/tls.h]) @@ -1047,6 +1084,17 @@ normally suggest. For full details of CLN and its license, please visit To build CVC4 with GMP instead (which is covered under the more permissive LGPL), configure --without-cln. +WARNING * WARNING * WARNING * WARNING * WARNING * WARNING * WARNING * WARNING +WARNING * WARNING * WARNING * WARNING * WARNING * WARNING * WARNING * WARNING + +Note that CLN is UNSAFE FOR USE in parallel contexts! +This build of CVC4 cannot be used safely as a portfolio solver. +since the result of building with CLN will include numerous race +conditions on the refcounts internal to CLN. + +WARNING * WARNING * WARNING * WARNING * WARNING * WARNING * WARNING * WARNING +WARNING * WARNING * WARNING * WARNING * WARNING * WARNING * WARNING * WARNING + " else mplibrary='gmp (LGPL)' @@ -1091,6 +1139,9 @@ Static binary: $enable_static_binary Compat lib : $CVC4_BUILD_LIBCOMPAT Bindings : ${CVC4_LANGUAGE_BINDINGS:-none} +Multithreaded: $support_multithreaded +TLS support : $CVC4_TLS_explanation + MP library : $mplibrary CPPFLAGS : $CPPFLAGS diff --git a/src/expr/Makefile.am b/src/expr/Makefile.am index 6a070a88a..6baa4613f 100644 --- a/src/expr/Makefile.am +++ b/src/expr/Makefile.am @@ -28,6 +28,12 @@ libexpr_la_SOURCES = \ declaration_scope.cpp \ expr_manager_scope.h \ node_self_iterator.h \ + variable_type_map.h \ + pickle_data.h \ + pickle_data.cpp \ + pickler.h \ + pickler.cpp \ + node_self_iterator.h \ expr_stream.h \ kind_map.h diff --git a/src/expr/command.cpp b/src/expr/command.cpp index 7d060186a..ba29b6c34 100644 --- a/src/expr/command.cpp +++ b/src/expr/command.cpp @@ -126,6 +126,10 @@ void EmptyCommand::invoke(SmtEngine* smtEngine) throw() { d_commandStatus = CommandSuccess::instance(); } +Command* EmptyCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + return new EmptyCommand(d_name); +} + /* class AssertCommand */ AssertCommand::AssertCommand(const BoolExpr& e) throw() : @@ -145,6 +149,10 @@ void AssertCommand::invoke(SmtEngine* smtEngine) throw() { } } +Command* AssertCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + return new AssertCommand(d_expr.exportTo(exprManager, variableMap)); +} + /* class PushCommand */ void PushCommand::invoke(SmtEngine* smtEngine) throw() { @@ -156,6 +164,10 @@ void PushCommand::invoke(SmtEngine* smtEngine) throw() { } } +Command* PushCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + return new PushCommand; +} + /* class PopCommand */ void PopCommand::invoke(SmtEngine* smtEngine) throw() { @@ -173,6 +185,12 @@ CheckSatCommand::CheckSatCommand() throw() : d_expr() { } +Command* PopCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + return new PopCommand(); +} + +/* class CheckSatCommand */ + CheckSatCommand::CheckSatCommand(const BoolExpr& expr) throw() : d_expr(expr) { } @@ -202,6 +220,12 @@ void CheckSatCommand::printResult(std::ostream& out) const throw() { } } +Command* CheckSatCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + CheckSatCommand* c = new CheckSatCommand(d_expr.exportTo(exprManager, variableMap)); + c->d_result = d_result; + return c; +} + /* class QueryCommand */ QueryCommand::QueryCommand(const BoolExpr& e) throw() : @@ -233,6 +257,12 @@ void QueryCommand::printResult(std::ostream& out) const throw() { } } +Command* QueryCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + QueryCommand* c = new QueryCommand(d_expr.exportTo(exprManager, variableMap)); + c->d_result = d_result; + return c; +} + /* class QuitCommand */ QuitCommand::QuitCommand() throw() { @@ -243,6 +273,10 @@ void QuitCommand::invoke(SmtEngine* smtEngine) throw() { d_commandStatus = CommandSuccess::instance(); } +Command* QuitCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + return new QuitCommand(); +} + /* class CommentCommand */ CommentCommand::CommentCommand(std::string comment) throw() : d_comment(comment) { @@ -257,6 +291,10 @@ void CommentCommand::invoke(SmtEngine* smtEngine) throw() { d_commandStatus = CommandSuccess::instance(); } +Command* CommentCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + return new CommentCommand(d_comment); +} + /* class CommandSequence */ CommandSequence::CommandSequence() throw() : @@ -299,6 +337,15 @@ CommandSequence::const_iterator CommandSequence::begin() const throw() { return d_commandSequence.begin(); } +Command* CommandSequence::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + CommandSequence* seq = new CommandSequence(); + for(iterator i = begin(); i != end(); ++i) { + seq->addCommand((*i)->exportTo(exprManager, variableMap)); + } + seq->d_index = d_index; + return seq; +} + CommandSequence::const_iterator CommandSequence::end() const throw() { return d_commandSequence.end(); } @@ -338,6 +385,12 @@ void DeclareFunctionCommand::invoke(SmtEngine* smtEngine) throw() { Dump("declarations") << *this << endl; } +Command* DeclareFunctionCommand::exportTo(ExprManager* exprManager, + ExprManagerMapCollection& variableMap) { + return new DeclareFunctionCommand(d_symbol, + d_type.exportTo(exprManager, variableMap)); +} + /* class DeclareTypeCommand */ DeclareTypeCommand::DeclareTypeCommand(const std::string& id, size_t arity, Type t) throw() : @@ -358,6 +411,12 @@ void DeclareTypeCommand::invoke(SmtEngine* smtEngine) throw() { Dump("declarations") << *this << endl; } +Command* DeclareTypeCommand::exportTo(ExprManager* exprManager, + ExprManagerMapCollection& variableMap) { + return new DeclareTypeCommand(d_symbol, d_arity, + d_type.exportTo(exprManager, variableMap)); +} + /* class DefineTypeCommand */ DefineTypeCommand::DefineTypeCommand(const std::string& id, @@ -388,6 +447,14 @@ void DefineTypeCommand::invoke(SmtEngine* smtEngine) throw() { d_commandStatus = CommandSuccess::instance(); } +Command* DefineTypeCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + vector params; + transform(d_params.begin(), d_params.end(), back_inserter(params), + ExportTransformer(exprManager, variableMap)); + Type type = d_type.exportTo(exprManager, variableMap); + return new DefineTypeCommand(d_symbol, params, type); +} + /* class DefineFunctionCommand */ DefineFunctionCommand::DefineFunctionCommand(const std::string& id, @@ -429,6 +496,15 @@ void DefineFunctionCommand::invoke(SmtEngine* smtEngine) throw() { d_commandStatus = CommandSuccess::instance(); } +Command* DefineFunctionCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + Expr func = d_func.exportTo(exprManager, variableMap); + vector formals; + transform(d_formals.begin(), d_formals.end(), back_inserter(formals), + ExportTransformer(exprManager, variableMap)); + Expr formula = d_formula.exportTo(exprManager, variableMap); + return new DefineFunctionCommand(d_symbol, func, formals, formula); +} + /* class DefineNamedFunctionCommand */ DefineNamedFunctionCommand::DefineNamedFunctionCommand(const std::string& id, @@ -446,6 +522,15 @@ void DefineNamedFunctionCommand::invoke(SmtEngine* smtEngine) throw() { d_commandStatus = CommandSuccess::instance(); } +Command* DefineNamedFunctionCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + Expr func = d_func.exportTo(exprManager, variableMap); + vector formals; + transform(d_formals.begin(), d_formals.end(), back_inserter(formals), + ExportTransformer(exprManager, variableMap)); + Expr formula = d_formula.exportTo(exprManager, variableMap); + return new DefineNamedFunctionCommand(d_symbol, func, formals, formula); +} + /* class Simplify */ SimplifyCommand::SimplifyCommand(Expr term) throw() : @@ -473,6 +558,12 @@ void SimplifyCommand::printResult(std::ostream& out) const throw() { } } +Command* SimplifyCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + SimplifyCommand* c = new SimplifyCommand(d_term.exportTo(exprManager, variableMap)); + c->d_result = d_result.exportTo(exprManager, variableMap); + return c; +} + /* class GetValueCommand */ GetValueCommand::GetValueCommand(Expr term) throw() : @@ -505,6 +596,12 @@ void GetValueCommand::printResult(std::ostream& out) const throw() { } } +Command* GetValueCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + GetValueCommand* c = new GetValueCommand(d_term.exportTo(exprManager, variableMap)); + c->d_result = d_result.exportTo(exprManager, variableMap); + return c; +} + /* class GetAssignmentCommand */ GetAssignmentCommand::GetAssignmentCommand() throw() { @@ -531,6 +628,12 @@ void GetAssignmentCommand::printResult(std::ostream& out) const throw() { } } +Command* GetAssignmentCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + GetAssignmentCommand* c = new GetAssignmentCommand; + c->d_result = d_result; + return c; +} + /* class GetProofCommand */ GetProofCommand::GetProofCommand() throw() { @@ -557,6 +660,12 @@ void GetProofCommand::printResult(std::ostream& out) const throw() { } } +Command* GetProofCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + GetProofCommand* c = new GetProofCommand; + c->d_result = d_result; + return c; +} + /* class GetAssertionsCommand */ GetAssertionsCommand::GetAssertionsCommand() throw() { @@ -586,6 +695,12 @@ void GetAssertionsCommand::printResult(std::ostream& out) const throw() { } } +Command* GetAssertionsCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + GetAssertionsCommand* c = new GetAssertionsCommand; + c->d_result = d_result; + return c; +} + /* class SetBenchmarkStatusCommand */ SetBenchmarkStatusCommand::SetBenchmarkStatusCommand(BenchmarkStatus status) throw() : @@ -608,6 +723,11 @@ void SetBenchmarkStatusCommand::invoke(SmtEngine* smtEngine) throw() { } } +Command* SetBenchmarkStatusCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + SetBenchmarkStatusCommand* c = new SetBenchmarkStatusCommand(d_status); + return c; +} + /* class SetBenchmarkLogicCommand */ SetBenchmarkLogicCommand::SetBenchmarkLogicCommand(std::string logic) throw() : @@ -627,6 +747,11 @@ void SetBenchmarkLogicCommand::invoke(SmtEngine* smtEngine) throw() { } } +Command* SetBenchmarkLogicCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + SetBenchmarkLogicCommand* c = new SetBenchmarkLogicCommand(d_logic); + return c; +} + /* class SetInfoCommand */ SetInfoCommand::SetInfoCommand(std::string flag, const SExpr& sexpr) throw() : @@ -653,6 +778,11 @@ void SetInfoCommand::invoke(SmtEngine* smtEngine) throw() { } } +Command* SetInfoCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + SetInfoCommand* c = new SetInfoCommand(d_flag, d_sexpr); + return c; +} + /* class GetInfoCommand */ GetInfoCommand::GetInfoCommand(std::string flag) throw() : @@ -688,6 +818,12 @@ void GetInfoCommand::printResult(std::ostream& out) const throw() { } } +Command* GetInfoCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + GetInfoCommand* c = new GetInfoCommand(d_flag); + c->d_result = d_result; + return c; +} + /* class SetOptionCommand */ SetOptionCommand::SetOptionCommand(std::string flag, const SExpr& sexpr) throw() : @@ -714,6 +850,11 @@ void SetOptionCommand::invoke(SmtEngine* smtEngine) throw() { } } +Command* SetOptionCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + SetOptionCommand* c = new SetOptionCommand(d_flag, d_sexpr); + return c; +} + /* class GetOptionCommand */ GetOptionCommand::GetOptionCommand(std::string flag) throw() : @@ -747,6 +888,12 @@ void GetOptionCommand::printResult(std::ostream& out) const throw() { } } +Command* GetOptionCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + GetOptionCommand* c = new GetOptionCommand(d_flag); + c->d_result = d_result; + return c; +} + /* class DatatypeDeclarationCommand */ DatatypeDeclarationCommand::DatatypeDeclarationCommand(const DatatypeType& datatype) throw() : @@ -768,6 +915,11 @@ void DatatypeDeclarationCommand::invoke(SmtEngine* smtEngine) throw() { d_commandStatus = CommandSuccess::instance(); } +Command* DatatypeDeclarationCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + std::cout << "We currently do not support exportTo with Datatypes" << std::endl; + exit(1); + return NULL; +} /* output stream insertion operator for benchmark statuses */ std::ostream& operator<<(std::ostream& out, BenchmarkStatus status) throw() { diff --git a/src/expr/command.h b/src/expr/command.h index cf8c1b615..2d87fefc2 100644 --- a/src/expr/command.h +++ b/src/expr/command.h @@ -32,6 +32,7 @@ #include "expr/expr.h" #include "expr/type.h" +#include "expr/variable_type_map.h" #include "util/result.h" #include "util/sexpr.h" #include "util/datatype.h" @@ -177,6 +178,10 @@ public: };/* class CommandFailure */ class CVC4_PUBLIC Command { + // intentionally not permitted + Command(const Command&) CVC4_UNDEFINED; + Command& operator=(const Command&) CVC4_UNDEFINED; + protected: /** * This field contains a command status if the command has been @@ -210,6 +215,29 @@ public: virtual void printResult(std::ostream& out) const throw(); + /** + * Maps this Command into one for a different ExprManager, using + * variableMap for the translation and extending it with any new + * mappings. + */ + virtual Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) = 0; + +protected: + class ExportTransformer { + ExprManager* d_exprManager; + ExprManagerMapCollection& d_variableMap; + public: + ExportTransformer(ExprManager* exprManager, ExprManagerMapCollection& variableMap) : + d_exprManager(exprManager), + d_variableMap(variableMap) { + } + Expr operator()(Expr e) { + return e.exportTo(d_exprManager, d_variableMap); + } + Type operator()(Type t) { + return t.exportTo(d_exprManager, d_variableMap); + } + };/* class Command::ExportTransformer */ };/* class Command */ /** @@ -224,6 +252,7 @@ public: ~EmptyCommand() throw() {} std::string getName() const throw(); void invoke(SmtEngine* smtEngine) throw(); + Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); };/* class EmptyCommand */ class CVC4_PUBLIC AssertCommand : public Command { @@ -234,18 +263,21 @@ public: ~AssertCommand() throw() {} BoolExpr getExpr() const throw(); void invoke(SmtEngine* smtEngine) throw(); + Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); };/* class AssertCommand */ class CVC4_PUBLIC PushCommand : public Command { public: ~PushCommand() throw() {} void invoke(SmtEngine* smtEngine) throw(); + Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); };/* class PushCommand */ class CVC4_PUBLIC PopCommand : public Command { public: ~PopCommand() throw() {} void invoke(SmtEngine* smtEngine) throw(); + Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); };/* class PopCommand */ class CVC4_PUBLIC DeclarationDefinitionCommand : public Command { @@ -265,6 +297,7 @@ public: ~DeclareFunctionCommand() throw() {} Type getType() const throw(); void invoke(SmtEngine* smtEngine) throw(); + Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); };/* class DeclareFunctionCommand */ class CVC4_PUBLIC DeclareTypeCommand : public DeclarationDefinitionCommand { @@ -277,6 +310,7 @@ public: size_t getArity() const throw(); Type getType() const throw(); void invoke(SmtEngine* smtEngine) throw(); + Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); };/* class DeclareTypeCommand */ class CVC4_PUBLIC DefineTypeCommand : public DeclarationDefinitionCommand { @@ -290,6 +324,7 @@ public: const std::vector& getParameters() const throw(); Type getType() const throw(); void invoke(SmtEngine* smtEngine) throw(); + Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); };/* class DefineTypeCommand */ class CVC4_PUBLIC DefineFunctionCommand : public DeclarationDefinitionCommand { @@ -306,6 +341,7 @@ public: const std::vector& getFormals() const throw(); Expr getFormula() const throw(); void invoke(SmtEngine* smtEngine) throw(); + Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); };/* class DefineFunctionCommand */ /** @@ -318,6 +354,7 @@ public: DefineNamedFunctionCommand(const std::string& id, Expr func, const std::vector& formals, Expr formula) throw(); void invoke(SmtEngine* smtEngine) throw(); + Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); };/* class DefineNamedFunctionCommand */ class CVC4_PUBLIC CheckSatCommand : public Command { @@ -332,6 +369,7 @@ public: void invoke(SmtEngine* smtEngine) throw(); Result getResult() const throw(); void printResult(std::ostream& out) const throw(); + Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); };/* class CheckSatCommand */ class CVC4_PUBLIC QueryCommand : public Command { @@ -345,6 +383,7 @@ public: void invoke(SmtEngine* smtEngine) throw(); Result getResult() const throw(); void printResult(std::ostream& out) const throw(); + Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); };/* class QueryCommand */ // this is TRANSFORM in the CVC presentation language @@ -359,6 +398,7 @@ public: void invoke(SmtEngine* smtEngine) throw(); Expr getResult() const throw(); void printResult(std::ostream& out) const throw(); + Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); };/* class SimplifyCommand */ class CVC4_PUBLIC GetValueCommand : public Command { @@ -372,6 +412,7 @@ public: void invoke(SmtEngine* smtEngine) throw(); Expr getResult() const throw(); void printResult(std::ostream& out) const throw(); + Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); };/* class GetValueCommand */ class CVC4_PUBLIC GetAssignmentCommand : public Command { @@ -383,6 +424,7 @@ public: void invoke(SmtEngine* smtEngine) throw(); SExpr getResult() const throw(); void printResult(std::ostream& out) const throw(); + Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); };/* class GetAssignmentCommand */ class CVC4_PUBLIC GetProofCommand : public Command { @@ -394,6 +436,7 @@ public: void invoke(SmtEngine* smtEngine) throw(); Proof* getResult() const throw(); void printResult(std::ostream& out) const throw(); + Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); };/* class GetProofCommand */ class CVC4_PUBLIC GetAssertionsCommand : public Command { @@ -405,6 +448,7 @@ public: void invoke(SmtEngine* smtEngine) throw(); std::string getResult() const throw(); void printResult(std::ostream& out) const throw(); + Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); };/* class GetAssertionsCommand */ class CVC4_PUBLIC SetBenchmarkStatusCommand : public Command { @@ -415,6 +459,7 @@ public: ~SetBenchmarkStatusCommand() throw() {} BenchmarkStatus getStatus() const throw(); void invoke(SmtEngine* smtEngine) throw(); + Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); };/* class SetBenchmarkStatusCommand */ class CVC4_PUBLIC SetBenchmarkLogicCommand : public Command { @@ -425,6 +470,7 @@ public: ~SetBenchmarkLogicCommand() throw() {} std::string getLogic() const throw(); void invoke(SmtEngine* smtEngine) throw(); + Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); };/* class SetBenchmarkLogicCommand */ class CVC4_PUBLIC SetInfoCommand : public Command { @@ -437,6 +483,7 @@ public: std::string getFlag() const throw(); SExpr getSExpr() const throw(); void invoke(SmtEngine* smtEngine) throw(); + Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); };/* class SetInfoCommand */ class CVC4_PUBLIC GetInfoCommand : public Command { @@ -450,6 +497,7 @@ public: void invoke(SmtEngine* smtEngine) throw(); std::string getResult() const throw(); void printResult(std::ostream& out) const throw(); + Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); };/* class GetInfoCommand */ class CVC4_PUBLIC SetOptionCommand : public Command { @@ -462,6 +510,7 @@ public: std::string getFlag() const throw(); SExpr getSExpr() const throw(); void invoke(SmtEngine* smtEngine) throw(); + Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); };/* class SetOptionCommand */ class CVC4_PUBLIC GetOptionCommand : public Command { @@ -475,6 +524,7 @@ public: void invoke(SmtEngine* smtEngine) throw(); std::string getResult() const throw(); void printResult(std::ostream& out) const throw(); + Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); };/* class GetOptionCommand */ class CVC4_PUBLIC DatatypeDeclarationCommand : public Command { @@ -486,6 +536,7 @@ public: DatatypeDeclarationCommand(const std::vector& datatypes) throw(); const std::vector& getDatatypes() const throw(); void invoke(SmtEngine* smtEngine) throw(); + Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); };/* class DatatypeDeclarationCommand */ class CVC4_PUBLIC QuitCommand : public Command { @@ -493,6 +544,7 @@ public: QuitCommand() throw(); ~QuitCommand() throw() {} void invoke(SmtEngine* smtEngine) throw(); + Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); };/* class QuitCommand */ class CVC4_PUBLIC CommentCommand : public Command { @@ -502,6 +554,7 @@ public: ~CommentCommand() throw() {} std::string getComment() const throw(); void invoke(SmtEngine* smtEngine) throw(); + Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); };/* class CommentCommand */ class CVC4_PUBLIC CommandSequence : public Command { @@ -528,6 +581,7 @@ public: iterator begin() throw(); iterator end() throw(); + Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); };/* class CommandSequence */ class CVC4_PUBLIC DeclarationSequence : public CommandSequence { diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp index 576d0324d..83a80ed13 100644 --- a/src/expr/expr_manager_template.cpp +++ b/src/expr/expr_manager_template.cpp @@ -18,6 +18,7 @@ #include "expr/node_manager.h" #include "expr/expr_manager.h" +#include "expr/variable_type_map.h" #include "context/context.h" #include "util/options.h" #include "util/stats.h" @@ -30,7 +31,7 @@ ${includes} // compiler directs the user to the template file instead of the // generated one. We don't want the user to modify the generated one, // since it'll get overwritten on a later build. -#line 34 "${template}" +#line 35 "${template}" #ifdef CVC4_STATISTICS_ON #define INC_STAT(kind) \ @@ -829,6 +830,52 @@ Context* ExprManager::getContext() const { return d_ctxt; } +namespace expr { + +Node exportInternal(TNode n, ExprManager* from, ExprManager* to, ExprManagerMapCollection& vmap); + +TypeNode exportTypeInternal(TypeNode n, NodeManager* from, NodeManager* to, ExprManagerMapCollection& vmap) { + Debug("export") << "type: " << n << std::endl; + Assert(n.getKind() == kind::SORT_TYPE || + n.getMetaKind() != kind::metakind::PARAMETERIZED, + "PARAMETERIZED-kinded types (other than SORT_KIND) not supported"); + if(n.getKind() == kind::TYPE_CONSTANT) { + return to->mkTypeConst(n.getConst()); + } else if(n.getKind() == kind::BITVECTOR_TYPE) { + return to->mkBitVectorType(n.getConst()); + } + Type from_t = from->toType(n); + Type& to_t = vmap.d_typeMap[from_t]; + if(! to_t.isNull()) { + Debug("export") << "+ mapped `" << from_t << "' to `" << to_t << "'" << std::endl; + return *Type::getTypeNode(to_t); + } + NodeBuilder<> children(to, n.getKind()); + if(n.getKind() == kind::SORT_TYPE) { + Debug("export") << "type: operator: " << n.getOperator() << std::endl; + // make a new sort tag in target node manager + Node sortTag = NodeBuilder<0>(to, kind::SORT_TAG); + children << sortTag; + } + for(TypeNode::iterator i = n.begin(), i_end = n.end(); i != i_end; ++i) { + Debug("export") << "type: child: " << *i << std::endl; + children << exportTypeInternal(*i, from, to, vmap); + } + TypeNode out = children.constructTypeNode();// FIXME thread safety + to_t = to->toType(out); + return out; +}/* exportTypeInternal() */ + +}/* CVC4::expr namespace */ + +Type ExprManager::exportType(const Type& t, ExprManager* em, ExprManagerMapCollection& vmap) { + Assert(t.d_nodeManager != em->d_nodeManager, + "Can't export a Type to the same ExprManager"); + NodeManagerScope ems(t.d_nodeManager); + return Type(em->d_nodeManager, + new TypeNode(expr::exportTypeInternal(*t.d_typeNode, t.d_nodeManager, em->d_nodeManager, vmap))); +} + ${mkConst_implementations} }/* CVC4 namespace */ diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h index 81d30fd1e..eecb40f3e 100644 --- a/src/expr/expr_manager_template.h +++ b/src/expr/expr_manager_template.h @@ -42,6 +42,13 @@ class SmtEngine; class NodeManager; struct Options; class IntStat; +class ExprManagerMapCollection; + +namespace expr { + namespace pickle { + class Pickler; + }/* CVC4::expr::pickle namespace */ +}/* CVC4::expr namespace */ namespace context { class Context; @@ -404,6 +411,11 @@ public: Expr mkVar(const std::string& name, Type type); Expr mkVar(Type type); + /** Export an expr to a different ExprManager */ + //static Expr exportExpr(const Expr& e, ExprManager* em); + /** Export a type to a different ExprManager */ + static Type exportType(const Type& t, ExprManager* em, ExprManagerMapCollection& vmap); + /** Returns the minimum arity of the given kind. */ static unsigned minArity(Kind kind); diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp index 3c376f632..c510ce381 100644 --- a/src/expr/expr_template.cpp +++ b/src/expr/expr_template.cpp @@ -19,8 +19,10 @@ #include "expr/expr.h" #include "expr/node.h" #include "expr/expr_manager_scope.h" +#include "expr/variable_type_map.h" #include "util/Assert.h" +#include #include #include @@ -30,7 +32,7 @@ ${includes} // compiler directs the user to the template file instead of the // generated one. We don't want the user to modify the generated one, // since it'll get overwritten on a later build. -#line 34 "${template}" +#line 36 "${template}" using namespace CVC4::kind; using namespace std; @@ -105,6 +107,72 @@ ExprManager* Expr::getExprManager() const { return d_exprManager; } +namespace expr { + +static Node exportConstant(TNode n, NodeManager* to); + +Node exportInternal(TNode n, ExprManager* from, ExprManager* to, ExprManagerMapCollection& vmap) { + if(n.getMetaKind() == kind::metakind::CONSTANT) { + return exportConstant(n, NodeManager::fromExprManager(to)); + } else if(n.getMetaKind() == kind::metakind::VARIABLE) { + Expr from_e(from, new Node(n)); + Expr& to_e = vmap.d_typeMap[from_e]; + if(! to_e.isNull()) { +Debug("export") << "+ mapped `" << from_e << "' to `" << to_e << "'" << std::endl; + return to_e.getNode(); + } else { + // construct new variable in other manager: + // to_e is a ref, so this inserts from_e -> to_e + std::string name; + Type type = from->exportType(from_e.getType(), to, vmap); + if(Node::fromExpr(from_e).getAttribute(VarNameAttr(), name)) { + to_e = to->mkVar(name, type);// FIXME thread safety +Debug("export") << "+ exported var `" << from_e << "'[" << from_e.getId() << "] with name `" << name << "' and type `" << from_e.getType() << "' to `" << to_e << "'[" << to_e.getId() << "] with type `" << type << "'" << std::endl; + } else { + to_e = to->mkVar(type);// FIXME thread safety +Debug("export") << "+ exported unnamed var `" << from_e << "' with type `" << from_e.getType() << "' to `" << to_e << "' with type `" << type << "'" << std::endl; + } + uint64_t to_int = (uint64_t)(to_e.getNode().d_nv); + uint64_t from_int = (uint64_t)(from_e.getNode().d_nv); + vmap.d_from[to_int] = from_int; + vmap.d_to[from_int] = to_int; + vmap.d_typeMap[to_e] = from_e;// insert other direction too + return Node::fromExpr(to_e); + } + } else { + std::vector children; +Debug("export") << "n: " << n << std::endl; + if(n.getMetaKind() == kind::metakind::PARAMETERIZED) { +Debug("export") << "+ parameterized, op is " << n.getOperator() << std::endl; + children.reserve(n.getNumChildren() + 1); + children.push_back(exportInternal(n.getOperator(), from, to, vmap)); + } else { + children.reserve(n.getNumChildren()); + } + for(TNode::iterator i = n.begin(), i_end = n.end(); i != i_end; ++i) { +Debug("export") << "+ child: " << *i << std::endl; + children.push_back(exportInternal(*i, from, to, vmap)); + } + if(Debug.isOn("export")) { + ExprManagerScope ems(*to); + Debug("export") << "children for export from " << n << std::endl; + for(std::vector::iterator i = children.begin(), i_end = children.end(); i != i_end; ++i) { + Debug("export") << " child: " << *i << std::endl; + } + } + return NodeManager::fromExprManager(to)->mkNode(n.getKind(), children);// FIXME thread safety + } +}/* exportInternal() */ + +}/* CVC4::expr namespace */ + +Expr Expr::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + Assert(d_exprManager != exprManager, + "No sense in cloning an Expr in the same ExprManager"); + ExprManagerScope ems(*this); + return Expr(exprManager, new Node(expr::exportInternal(*d_node, d_exprManager, exprManager, variableMap))); +} + Expr& Expr::operator=(const Expr& e) { Assert(d_node != NULL, "Unexpected NULL expression pointer!"); Assert(e.d_node != NULL, "Unexpected NULL expression pointer!"); @@ -449,4 +517,16 @@ void Expr::debugPrint() { ${getConst_implementations} +namespace expr { + +static Node exportConstant(TNode n, NodeManager* to) { + Assert(n.getMetaKind() == kind::metakind::CONSTANT); + switch(n.getKind()) { +${exportConstant_cases} + + default: Unhandled(n.getKind()); + } +}/* exportConstant() */ + +}/* CVC4::expr namespace */ }/* CVC4 namespace */ diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h index b54ec20d4..56396da01 100644 --- a/src/expr/expr_template.h +++ b/src/expr/expr_template.h @@ -49,6 +49,8 @@ namespace CVC4 { template class NodeTemplate; +class NodeManager; + class Expr; class ExprManager; class SmtEngine; @@ -56,6 +58,20 @@ class Type; class TypeCheckingException; class TypeCheckingExceptionPrivate; +namespace expr { + namespace pickle { + class Pickler; + }/* CVC4::expr::pickle namespace */ +}/* CVC4::expr namespace */ + +namespace prop { + class SatSolver; +}/* CVC4::prop namespace */ + +class ExprManagerMapCollection; + +struct ExprHashFunction; + namespace smt { class SmtEnginePrivate; }/* CVC4::smt namespace */ @@ -64,6 +80,8 @@ namespace expr { class CVC4_PUBLIC ExprSetDepth; class CVC4_PUBLIC ExprPrintTypes; class CVC4_PUBLIC ExprSetLanguage; + + NodeTemplate exportInternal(NodeTemplate n, ExprManager* from, ExprManager* to, ExprManagerMapCollection& vmap); }/* CVC4::expr namespace */ /** @@ -436,6 +454,13 @@ public: */ ExprManager* getExprManager() const; + /** + * Maps this Expr into one for a different ExprManager, using + * variableMap for the translation and extending it with any new + * mappings. + */ + Expr exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); + /** * IOStream manipulator to set the maximum depth of Exprs when * pretty-printing. -1 means print to any depth. E.g.: @@ -510,6 +535,10 @@ protected: friend class ExprManager; friend class NodeManager; friend class TypeCheckingException; + friend class expr::pickle::Pickler; + friend class prop::SatSolver; + friend NodeTemplate expr::exportInternal(NodeTemplate n, ExprManager* from, ExprManager* to, ExprManagerMapCollection& vmap); + friend std::ostream& CVC4::operator<<(std::ostream& out, const Expr& e); template friend class NodeTemplate; @@ -828,7 +857,7 @@ public: ${getConst_instantiations} -#line 832 "${template}" +#line 861 "${template}" namespace expr { diff --git a/src/expr/mkexpr b/src/expr/mkexpr index 69f7019ab..0cae68ed0 100755 --- a/src/expr/mkexpr +++ b/src/expr/mkexpr @@ -60,6 +60,7 @@ getConst_instantiations= getConst_implementations= mkConst_instantiations= mkConst_implementations= +exportConstant_cases= seen_theory=false seen_theory_builtin=false @@ -193,6 +194,8 @@ template <> $2 const & Expr::getConst() const { return d_node->getConst< $2 >(); } " + exportConstant_cases="${exportConstant_cases} + case $1: return to->mkConst(n.getConst< $2 >());" } function check_theory_seen { @@ -244,6 +247,7 @@ for var in \ getConst_implementations \ mkConst_instantiations \ mkConst_implementations \ + exportConstant_cases \ typechecker_includes \ typerules \ ; do diff --git a/src/expr/node.h b/src/expr/node.h index 57b02b05b..37499c3bf 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -49,6 +49,12 @@ namespace CVC4 { class TypeNode; class NodeManager; +namespace expr { + namespace pickle { + class PicklerPrivate; + }/* CVC4::expr::pickle namespace */ +}/* CVC4::expr namespace */ + template class NodeTemplate; @@ -177,6 +183,9 @@ class NodeTemplate { */ friend class expr::NodeValue; + friend class expr::pickle::PicklerPrivate; + friend Node expr::exportInternal(TNode n, ExprManager* from, ExprManager* to, ExprManagerMapCollection& vmap); + /** A convenient null-valued encapsulated pointer */ static NodeTemplate s_null; @@ -200,6 +209,7 @@ class NodeTemplate { friend class NodeTemplate; friend class NodeTemplate; + friend class TypeNode; friend class NodeManager; template diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h index ded7ad8fe..c5d41816e 100644 --- a/src/expr/node_builder.h +++ b/src/expr/node_builder.h @@ -928,7 +928,7 @@ expr::NodeValue* NodeBuilder::constructNV() { // reference counts in this case. nv->d_nchildren = 0; nv->d_kind = d_nv->d_kind; - nv->d_id = expr::NodeValue::next_id++;// FIXME multithreading + nv->d_id = d_nm->next_id++;// FIXME multithreading nv->d_rc = 0; setUsed(); if(Debug.isOn("gc")) { @@ -1015,7 +1015,7 @@ expr::NodeValue* NodeBuilder::constructNV() { } nv->d_nchildren = d_inlineNv.d_nchildren; nv->d_kind = d_inlineNv.d_kind; - nv->d_id = expr::NodeValue::next_id++;// FIXME multithreading + nv->d_id = d_nm->next_id++;// FIXME multithreading nv->d_rc = 0; std::copy(d_inlineNv.d_children, @@ -1069,7 +1069,7 @@ expr::NodeValue* NodeBuilder::constructNV() { crop(); expr::NodeValue* nv = d_nv; - nv->d_id = expr::NodeValue::next_id++;// FIXME multithreading + nv->d_id = d_nm->next_id++;// FIXME multithreading d_nv = &d_inlineNv; d_nvMaxChildren = nchild_thresh; setUsed(); @@ -1118,7 +1118,7 @@ expr::NodeValue* NodeBuilder::constructNV() const { // reference counts in this case. nv->d_nchildren = 0; nv->d_kind = d_nv->d_kind; - nv->d_id = expr::NodeValue::next_id++;// FIXME multithreading + nv->d_id = d_nm->next_id++;// FIXME multithreading nv->d_rc = 0; Debug("gc") << "creating node value " << nv << " [" << nv->d_id << "]: " << *nv << "\n"; @@ -1194,7 +1194,7 @@ expr::NodeValue* NodeBuilder::constructNV() const { } nv->d_nchildren = d_inlineNv.d_nchildren; nv->d_kind = d_inlineNv.d_kind; - nv->d_id = expr::NodeValue::next_id++;// FIXME multithreading + nv->d_id = d_nm->next_id++;// FIXME multithreading nv->d_rc = 0; std::copy(d_inlineNv.d_children, @@ -1248,7 +1248,7 @@ expr::NodeValue* NodeBuilder::constructNV() const { } nv->d_nchildren = d_nv->d_nchildren; nv->d_kind = d_nv->d_kind; - nv->d_id = expr::NodeValue::next_id++;// FIXME multithreading + nv->d_id = d_nm->next_id++;// FIXME multithreading nv->d_rc = 0; std::copy(d_nv->d_children, diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index 2bf0a864a..1d4b7d3d1 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -84,6 +84,7 @@ NodeManager::NodeManager(context::Context* ctxt, d_optionsAllocated(new Options()), d_options(d_optionsAllocated), d_statisticsRegistry(new StatisticsRegistry()), + next_id(0), d_attrManager(ctxt), d_exprManager(exprManager), d_nodeUnderDeletion(NULL), @@ -98,6 +99,7 @@ NodeManager::NodeManager(context::Context* ctxt, d_optionsAllocated(NULL), d_options(&options), d_statisticsRegistry(new StatisticsRegistry()), + next_id(0), d_attrManager(ctxt), d_exprManager(exprManager), d_nodeUnderDeletion(NULL), diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 3646e91c5..e446b7d71 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -88,6 +88,8 @@ class NodeManager { NodeValuePool d_nodeValuePool; + size_t next_id; + expr::attr::AttributeManager d_attrManager; /** The associated ExprManager */ @@ -503,6 +505,60 @@ public: const AttrKind& attr, const typename AttrKind::value_type& value); + /** + * Retrieve an attribute for a TypeNode. + * + * @param n the type node + * @param attr an instance of the attribute kind to retrieve. + * @returns the attribute, if set, or a default-constructed + * AttrKind::value_type if not. + */ + template + inline typename AttrKind::value_type + getAttribute(TypeNode n, const AttrKind& attr) const; + + /** + * Check whether an attribute is set for a TypeNode. + * + * @param n the type node + * @param attr an instance of the attribute kind to check + * @returns true iff attr is set for n. + */ + template + inline bool hasAttribute(TypeNode n, + const AttrKind& attr) const; + + /** + * Check whether an attribute is set for a TypeNode and, if so, retieve + * it. + * + * @param n the type node + * @param attr an instance of the attribute kind to check + * @param value a reference to an object of the attribute's value type. + * value will be set to the value of the attribute, if it is + * set for nv; otherwise, it will be set to the default value of + * the attribute. + * @returns true iff attr is set for n. + */ + template + inline bool getAttribute(TypeNode n, + const AttrKind& attr, + typename AttrKind::value_type& value) const; + + /** + * Set an attribute for a type node. If the node doesn't have the + * attribute, this function assigns one. If the type node has one, + * this overwrites it. + * + * @param n the type node + * @param attr an instance of the attribute kind to set + * @param value the value of attr for n + */ + template + inline void setAttribute(TypeNode n, + const AttrKind& attr, + const typename AttrKind::value_type& value); + /** Get the (singleton) type for Booleans. */ inline TypeNode booleanType(); @@ -762,6 +818,32 @@ NodeManager::setAttribute(TNode n, const AttrKind&, d_attrManager.setAttribute(n.d_nv, AttrKind(), value); } +template +inline typename AttrKind::value_type +NodeManager::getAttribute(TypeNode n, const AttrKind&) const { + return d_attrManager.getAttribute(n.d_nv, AttrKind()); +} + +template +inline bool +NodeManager::hasAttribute(TypeNode n, const AttrKind&) const { + return d_attrManager.hasAttribute(n.d_nv, AttrKind()); +} + +template +inline bool +NodeManager::getAttribute(TypeNode n, const AttrKind&, + typename AttrKind::value_type& ret) const { + return d_attrManager.getAttribute(n.d_nv, AttrKind(), ret); +} + +template +inline void +NodeManager::setAttribute(TypeNode n, const AttrKind&, + const typename AttrKind::value_type& value) { + d_attrManager.setAttribute(n.d_nv, AttrKind(), value); +} + /** Get the (singleton) type for booleans. */ inline TypeNode NodeManager::booleanType() { @@ -965,7 +1047,7 @@ inline TypeNode NodeManager::mkSort() { inline TypeNode NodeManager::mkSort(const std::string& name) { TypeNode type = mkSort(); - type.setAttribute(expr::VarNameAttr(), name); + setAttribute(type, expr::VarNameAttr(), name); return type; } @@ -986,7 +1068,7 @@ inline TypeNode NodeManager::mkSort(TypeNode constructor, nb << sortTag; nb.append(children); TypeNode type = nb.constructTypeNode(); - type.setAttribute(expr::VarNameAttr(), name); + setAttribute(type, expr::VarNameAttr(), name); return type; } @@ -997,8 +1079,8 @@ inline TypeNode NodeManager::mkSortConstructor(const std::string& name, Node sortTag = NodeBuilder<0>(this, kind::SORT_TAG); nb << sortTag; TypeNode type = nb.constructTypeNode(); - type.setAttribute(expr::VarNameAttr(), name); - type.setAttribute(expr::SortArityAttr(), arity); + setAttribute(type, expr::VarNameAttr(), name); + setAttribute(type, expr::SortArityAttr(), arity); return type; } @@ -1211,37 +1293,37 @@ inline TypeNode NodeManager::mkTypeNode(Kind kind, inline Node NodeManager::mkVar(const std::string& name, const TypeNode& type) { Node n = mkVar(type); - n.setAttribute(TypeAttr(), type); - n.setAttribute(expr::VarNameAttr(), name); + setAttribute(n, TypeAttr(), type); + setAttribute(n, expr::VarNameAttr(), name); return n; } inline Node* NodeManager::mkVarPtr(const std::string& name, const TypeNode& type) { Node* n = mkVarPtr(type); - n->setAttribute(TypeAttr(), type); - n->setAttribute(expr::VarNameAttr(), name); + setAttribute(*n, TypeAttr(), type); + setAttribute(*n, expr::VarNameAttr(), name); return n; } inline Node NodeManager::mkVar(const TypeNode& type) { Node n = NodeBuilder<0>(this, kind::VARIABLE); - n.setAttribute(TypeAttr(), type); - n.setAttribute(TypeCheckedAttr(), true); + setAttribute(n, TypeAttr(), type); + setAttribute(n, TypeCheckedAttr(), true); return n; } inline Node* NodeManager::mkVarPtr(const TypeNode& type) { Node* n = NodeBuilder<0>(this, kind::VARIABLE).constructNodePtr(); - n->setAttribute(TypeAttr(), type); - n->setAttribute(TypeCheckedAttr(), true); + setAttribute(*n, TypeAttr(), type); + setAttribute(*n, TypeCheckedAttr(), true); return n; } inline Node NodeManager::mkSkolem(const TypeNode& type) { Node n = NodeBuilder<0>(this, kind::SKOLEM); - n.setAttribute(TypeAttr(), type); - n.setAttribute(TypeCheckedAttr(), true); + setAttribute(n, TypeAttr(), type); + setAttribute(n, TypeCheckedAttr(), true); return n; } @@ -1282,7 +1364,7 @@ NodeClass NodeManager::mkConstInternal(const T& val) { nv->d_nchildren = 0; nv->d_kind = kind::metakind::ConstantMap::kind; - nv->d_id = expr::NodeValue::next_id++;// FIXME multithreading + nv->d_id = next_id++;// FIXME multithreading nv->d_rc = 0; //OwningTheory::mkConst(val); diff --git a/src/expr/node_value.cpp b/src/expr/node_value.cpp index 89ac7ffca..970d2e0fc 100644 --- a/src/expr/node_value.cpp +++ b/src/expr/node_value.cpp @@ -33,8 +33,6 @@ using namespace std; namespace CVC4 { namespace expr { -size_t NodeValue::next_id = 1; - NodeValue NodeValue::s_null(0); string NodeValue::toString() const { diff --git a/src/expr/node_value.h b/src/expr/node_value.h index 95af57719..e5ecfbc48 100644 --- a/src/expr/node_value.h +++ b/src/expr/node_value.h @@ -126,8 +126,6 @@ class NodeValue { void inc(); void dec(); - static size_t next_id; - /** * Uninitializing constructor for NodeBuilder's use. */ diff --git a/src/expr/pickle_data.cpp b/src/expr/pickle_data.cpp new file mode 100644 index 000000000..1de8f2cf7 --- /dev/null +++ b/src/expr/pickle_data.cpp @@ -0,0 +1,60 @@ +/********************* */ +/*! \file pickle_data.cpp + ** \verbatim + ** Original author: kshitij + ** Major contributors: taking, mdeters + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief This is a "pickle" for expressions, CVC4-internal view + ** + ** This is the CVC4-internal view (private data structure) for a + ** "pickle" for expressions. The public-facing view is a "Pickle", + ** which just points to a PickleData. A pickle is a binary + ** serialization of an expression that can be converted back into an + ** expression in the same or another ExprManager. + **/ + +#include +#include +#include + +#include "expr/pickle_data.h" +#include "expr/expr.h" +#include "expr/node.h" +#include "expr/node_manager.h" +#include "expr/node_value.h" +#include "expr/expr_manager_scope.h" +#include "expr/variable_type_map.h" +#include "util/Assert.h" +#include "expr/kind.h" +#include "expr/metakind.h" + +namespace CVC4 { +namespace expr { +namespace pickle { + +void PickleData::writeToStringStream(std::ostringstream& oss) const { + BlockDeque::const_iterator i = d_blocks.begin(), end = d_blocks.end(); + for(; i != end; ++i) { + Block b = *i; + Assert(sizeof(b) * 8 == NBITS_BLOCK); + oss << b.d_body.d_data << " "; + } +} + +std::string PickleData::toString() const { + std::ostringstream oss; + oss.flags(std::ios::oct | std::ios::showbase); + writeToStringStream(oss); + return oss.str(); +} + +}/* CVC4::expr::pickle namespace */ +}/* CVC4::expr namespace */ +}/* CVC4 namespace */ diff --git a/src/expr/pickle_data.h b/src/expr/pickle_data.h new file mode 100644 index 000000000..dab6e56c3 --- /dev/null +++ b/src/expr/pickle_data.h @@ -0,0 +1,122 @@ +/********************* */ +/*! \file pickle_data.h + ** \verbatim + ** Original author: kshitij + ** Major contributors: taking, mdeters + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief This is a "pickle" for expressions, CVC4-internal view + ** + ** This is the CVC4-internal view (private data structure) for a + ** "pickle" for expressions. The public-facing view is a "Pickle", + ** which just points to a PickleData. A pickle is a binary + ** serialization of an expression that can be converted back into an + ** expression in the same or another ExprManager. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__PICKLE_DATA_H +#define __CVC4__PICKLE_DATA_H + +#include +#include +#include +#include + +#include "expr/expr.h" +#include "expr/node.h" +#include "expr/node_manager.h" +#include "expr/expr_manager.h" +#include "expr/variable_type_map.h" +#include "expr/kind.h" +#include "expr/metakind.h" + +namespace CVC4 { + +class NodeManager; + +namespace expr { +namespace pickle { + +const unsigned NBITS_BLOCK = 32; +const unsigned NBITS_KIND = __CVC4__EXPR__NODE_VALUE__NBITS__KIND; +const unsigned NBITS_NCHILDREN = __CVC4__EXPR__NODE_VALUE__NBITS__NCHILDREN; +const unsigned NBITS_CONSTBLOCKS = 32; + +struct BlockHeader { + unsigned d_kind : NBITS_KIND; +};/* struct BlockHeader */ + +struct BlockHeaderOperator { + unsigned d_kind : NBITS_KIND; + unsigned d_nchildren : NBITS_NCHILDREN; + unsigned : NBITS_BLOCK - (NBITS_KIND + NBITS_NCHILDREN); +};/* struct BlockHeaderOperator */ + +struct BlockHeaderConstant { + unsigned d_kind : NBITS_KIND; + unsigned d_constblocks : NBITS_BLOCK - NBITS_KIND; +};/* struct BlockHeaderConstant */ + +struct BlockHeaderVariable { + unsigned d_kind : NBITS_KIND; + unsigned : NBITS_BLOCK - NBITS_KIND; +};/* struct BlockHeaderVariable */ + +struct BlockBody { + unsigned d_data : NBITS_BLOCK; +};/* struct BlockBody */ + +union Block { + BlockHeader d_header; + BlockHeaderConstant d_headerConstant; + BlockHeaderOperator d_headerOperator; + BlockHeaderVariable d_headerVariable; + + BlockBody d_body; +};/* union Block */ + +class PickleData { + typedef std::deque BlockDeque; + BlockDeque d_blocks; + +public: + PickleData& operator<<(Block b) { + enqueue(b); + return (*this); + } + + std::string toString() const; + + void enqueue(Block b) { + d_blocks.push_back(b); + } + + Block dequeue() { + Block b = d_blocks.front(); + d_blocks.pop_front(); + return b; + } + + bool empty() const { return d_blocks.empty(); } + uint32_t size() const { return d_blocks.size(); } + + void swap(PickleData& other){ + d_blocks.swap(other.d_blocks); + } + + void writeToStringStream(std::ostringstream& oss) const; +};/* class PickleData */ + +}/* CVC4::expr::pickle namespace */ +}/* CVC4::expr namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__PICKLE_DATA_H */ diff --git a/src/expr/pickler.cpp b/src/expr/pickler.cpp new file mode 100644 index 000000000..f09c552d1 --- /dev/null +++ b/src/expr/pickler.cpp @@ -0,0 +1,477 @@ +/********************* */ +/*! \file pickler.cpp + ** \verbatim + ** Original author: kshitij + ** Major contributors: taking, mdeters + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief This is a "pickler" for expressions + ** + ** This is a "pickler" for expressions. It produces a binary + ** serialization of an expression that can be converted back + ** into an expression in the same or another ExprManager. + **/ + +#include +#include +#include + +#include "expr/pickler.h" +#include "expr/pickle_data.h" +#include "expr/expr.h" +#include "expr/node.h" +#include "expr/node_manager.h" +#include "expr/node_value.h" +#include "expr/expr_manager_scope.h" +#include "expr/variable_type_map.h" +#include "util/Assert.h" +#include "expr/kind.h" +#include "expr/metakind.h" +#include "util/output.h" + +namespace CVC4 { +namespace expr { +namespace pickle { + +class PicklerPrivate { +public: + typedef std::stack NodeStack; + NodeStack d_stack; + + PickleData d_current; + + Pickler& d_pickler; + + NodeManager* const d_nm; + + PicklerPrivate(Pickler& pickler, ExprManager* em) : + d_pickler(pickler), + d_nm(NodeManager::fromExprManager(em)) { + } + + bool atDefaultState(){ + return d_stack.empty() && d_current.empty(); + } + + /* Helper functions for toPickle */ + void toCaseNode(TNode n) throw(AssertionException, PicklingException); + void toCaseVariable(TNode n) throw(AssertionException, PicklingException); + void toCaseConstant(TNode n); + void toCaseOperator(TNode n) throw(AssertionException, PicklingException); + void toCaseString(Kind k, const std::string& s); + + /* Helper functions for toPickle */ + Node fromCaseOperator(Kind k, uint32_t nchildren); + Node fromCaseConstant(Kind k, uint32_t nblocks); + std::string fromCaseString(uint32_t nblocks); + Node fromCaseVariable(Kind k); + +};/* class PicklerPrivate */ + +static Block mkBlockBody4Chars(char a, char b, char c, char d) { + Block newBody; + newBody.d_body.d_data = (a << 24) | (b << 16) | (c << 8) | d; + return newBody; +} + +static char getCharBlockBody(BlockBody body, int i) { + Assert(0 <= i && i <= 3); + + switch(i) { + case 0: return (body.d_data & 0xff000000) >> 24; + case 1: return (body.d_data & 0x00ff0000) >> 16; + case 2: return (body.d_data & 0x0000ff00) >> 8; + case 3: return (body.d_data & 0x000000ff); + default: + Unreachable(); + } + return '\0'; +} + +static Block mkBlockBody(unsigned data) { + Block newBody; + newBody.d_body.d_data = data; + return newBody; +} + +static Block mkOperatorHeader(Kind k, unsigned numChildren) { + Block newHeader; + newHeader.d_headerOperator.d_kind = k; + newHeader.d_headerOperator.d_nchildren = numChildren; + return newHeader; +} + +static Block mkVariableHeader(Kind k) { + Block newHeader; + newHeader.d_header.d_kind = k; + return newHeader; +} + +static Block mkConstantHeader(Kind k, unsigned numBlocks) { + Block newHeader; + newHeader.d_headerConstant.d_kind = k; + newHeader.d_headerConstant.d_constblocks = numBlocks; + return newHeader; +} + +Pickler::Pickler(ExprManager* em) : + d_private(new PicklerPrivate(*this, em)) { +} + +Pickler::~Pickler() { + delete d_private; +} + +void Pickler::toPickle(Expr e, Pickle& p) + throw(AssertionException, PicklingException) { + Assert(NodeManager::fromExprManager(e.getExprManager()) == d_private->d_nm); + Assert(d_private->atDefaultState()); + + try{ + d_private->d_current.swap(*p.d_data); + d_private->toCaseNode(e.getTNode()); + d_private->d_current.swap(*p.d_data); + }catch(PicklingException& pe){ + d_private->d_current = PickleData(); + Assert(d_private->atDefaultState()); + throw pe; + } + + Assert(d_private->atDefaultState()); +} + +void PicklerPrivate::toCaseNode(TNode n) + throw(AssertionException, PicklingException) { + Debug("pickler") << "toCaseNode: " << n << std::endl; + Kind k = n.getKind(); + kind::MetaKind m = metaKindOf(k); + switch(m) { + case kind::metakind::CONSTANT: + toCaseConstant(n); + break; + case kind::metakind::VARIABLE: + toCaseVariable(n); + break; + case kind::metakind::OPERATOR: + case kind::metakind::PARAMETERIZED: + toCaseOperator(n); + break; + default: + Unhandled(m); + } +} + +void PicklerPrivate::toCaseOperator(TNode n) + throw(AssertionException, PicklingException) { + Kind k = n.getKind(); + kind::MetaKind m = metaKindOf(k); + Assert(m == kind::metakind::PARAMETERIZED || m == kind::metakind::OPERATOR); + if(m == kind::metakind::PARAMETERIZED) { + toCaseNode(n.getOperator()); + } + for(TNode::iterator i = n.begin(), i_end = n.end(); i != i_end; ++i) { + toCaseNode(*i); + } + d_current << mkOperatorHeader(k, n.getNumChildren()); +} + +void PicklerPrivate::toCaseVariable(TNode n) + throw(AssertionException, PicklingException) { + Kind k = n.getKind(); + Assert(metaKindOf(k) == kind::metakind::VARIABLE); + + const NodeValue* nv = n.d_nv; + uint64_t asInt = reinterpret_cast(nv); + uint64_t mapped = d_pickler.variableToMap(asInt); + + uint32_t firstHalf = mapped >> 32; + uint32_t secondHalf = mapped & 0xffffffff; + + d_current << mkVariableHeader(k); + d_current << mkBlockBody(firstHalf); + d_current << mkBlockBody(secondHalf); +} + + +void PicklerPrivate::toCaseConstant(TNode n) { + Kind k = n.getKind(); + Assert(metaKindOf(k) == kind::metakind::CONSTANT); + switch(k) { + case kind::CONST_BOOLEAN: + d_current << mkConstantHeader(k, 1); + d_current << mkBlockBody(n.getConst()); + break; + case kind::CONST_INTEGER: + case kind::CONST_RATIONAL: { + std::string asString; + if(k == kind::CONST_INTEGER) { + const Integer& i = n.getConst(); + asString = i.toString(16); + } else { + Assert(k == kind::CONST_RATIONAL); + const Rational& q = n.getConst(); + asString = q.toString(16); + } + toCaseString(k, asString); + break; + } + case kind::BITVECTOR_EXTRACT_OP: { + BitVectorExtract bve = n.getConst(); + d_current << mkConstantHeader(k, 2); + d_current << mkBlockBody(bve.high); + d_current << mkBlockBody(bve.low); + break; + } + case kind::CONST_BITVECTOR: { + // irritating: we incorporate the size of the string in with the + // size of this constant, so it appears as one big constant and + // doesn't confuse anybody + BitVector bv = n.getConst(); + std::string asString = bv.getValue().toString(16); + d_current << mkConstantHeader(k, 2 + asString.size()); + d_current << mkBlockBody(bv.getSize()); + toCaseString(k, asString); + break; + } + default: + Unhandled(k); + } +} + +void PicklerPrivate::toCaseString(Kind k, const std::string& s) { + d_current << mkConstantHeader(k, s.size()); + + unsigned size = s.size(); + unsigned i; + for(i = 0; i + 4 <= size; i += 4) { + d_current << mkBlockBody4Chars(s[i + 0], s[i + 1],s[i + 2], s[i + 3]); + } + switch(size % 4) { + case 0: break; + case 1: d_current << mkBlockBody4Chars(s[i + 0], '\0','\0', '\0'); break; + case 2: d_current << mkBlockBody4Chars(s[i + 0], s[i + 1], '\0', '\0'); break; + case 3: d_current << mkBlockBody4Chars(s[i + 0], s[i + 1],s[i + 2], '\0'); break; + default: + Unreachable(); + } + +} + +void Pickler::debugPickleTest(Expr e) { + + //ExprManager *em = e.getExprManager(); + //Expr e1 = mkVar("x", makeType()); + //return ; + + Pickler pickler(e.getExprManager()); + + Pickle p; + pickler.toPickle(e, p); + + uint32_t size = p.d_data->size(); + std::string str = p.d_data->toString(); + + Expr from = pickler.fromPickle(p); + ExprManagerScope ems(e); + + Debug("pickle") << "before: " << e << std::endl; + Debug("pickle") << "after: " << from.getNode() << std::endl; + Debug("pickle") << "pickle: (oct) "<< size << " " << str.length() << " " << str << std::endl; + + Assert(p.d_data->empty()); + Assert(e == from); +} + +Expr Pickler::fromPickle(Pickle& p) { + Assert(d_private->atDefaultState()); + + d_private->d_current.swap(*p.d_data); + + while(!d_private->d_current.empty()) { + Block front = d_private->d_current.dequeue(); + + Kind k = (Kind)front.d_header.d_kind; + kind::MetaKind m = metaKindOf(k); + + Node result = Node::null(); + switch(m) { + case kind::metakind::VARIABLE: + result = d_private->fromCaseVariable(k); + break; + case kind::metakind::CONSTANT: + result = d_private->fromCaseConstant(k, front.d_headerConstant.d_constblocks); + break; + case kind::metakind::OPERATOR: + case kind::metakind::PARAMETERIZED: + result = d_private->fromCaseOperator(k, front.d_headerOperator.d_nchildren); + break; + default: + Unhandled(m); + } + Assert(result != Node::null()); + d_private->d_stack.push(result); + } + + Assert(d_private->d_current.empty()); + Assert(d_private->d_stack.size() == 1); + Node res = d_private->d_stack.top(); + d_private->d_stack.pop(); + + Assert(d_private->atDefaultState()); + + return d_private->d_nm->toExpr(res); +} + +Node PicklerPrivate::fromCaseVariable(Kind k) { + Assert(metaKindOf(k) == kind::metakind::VARIABLE); + + Block firstHalf = d_current.dequeue(); + Block secondHalf = d_current.dequeue(); + + uint64_t asInt = firstHalf.d_body.d_data; + asInt = asInt << 32; + asInt = asInt | (secondHalf.d_body.d_data); + + uint64_t mapped = d_pickler.variableFromMap(asInt); + + NodeValue* nv = reinterpret_cast(mapped); + Node fromNodeValue(nv); + + Assert(fromNodeValue.getKind() == k); + + return fromNodeValue; +} + +Node PicklerPrivate::fromCaseConstant(Kind k, uint32_t constblocks) { + switch(k) { + case kind::CONST_BOOLEAN: { + Assert(constblocks == 1); + Block val = d_current.dequeue(); + + bool b= val.d_body.d_data; + return d_nm->mkConst(b); + } + case kind::CONST_INTEGER: + case kind::CONST_RATIONAL: { + std::string s = fromCaseString(constblocks); + if(k == kind::CONST_INTEGER) { + Integer i(s, 16); + return d_nm->mkConst(i); + } else { + Rational q(s, 16); + return d_nm->mkConst(q); + } + } + case kind::BITVECTOR_EXTRACT_OP: { + Block high = d_current.dequeue(); + Block low = d_current.dequeue(); + BitVectorExtract bve(high.d_body.d_data, low.d_body.d_data); + return d_nm->mkConst(bve); + } + case kind::CONST_BITVECTOR: { + unsigned size = d_current.dequeue().d_body.d_data; + Block header CVC4_UNUSED = d_current.dequeue(); + Assert(header.d_headerConstant.d_kind == kind::CONST_BITVECTOR); + Assert(header.d_headerConstant.d_constblocks == constblocks - 2); + Integer value(fromCaseString(constblocks - 2)); + BitVector bv(size, value); + return d_nm->mkConst(bv); + } + default: + Unhandled(k); + } +} + +std::string PicklerPrivate::fromCaseString(uint32_t size) { + std::stringstream ss; + unsigned i; + for(i = 0; i + 4 <= size; i += 4) { + Block front = d_current.dequeue(); + BlockBody body = front.d_body; + + ss << getCharBlockBody(body,0) + << getCharBlockBody(body,1) + << getCharBlockBody(body,2) + << getCharBlockBody(body,3); + } + Assert(i == size - (size%4) ); + if(size % 4 != 0) { + Block front = d_current.dequeue(); + BlockBody body = front.d_body; + switch(size % 4) { + case 1: + ss << getCharBlockBody(body,0); + break; + case 2: + ss << getCharBlockBody(body,0) + << getCharBlockBody(body,1); + break; + case 3: + ss << getCharBlockBody(body,0) + << getCharBlockBody(body,1) + << getCharBlockBody(body,2); + break; + default: + Unreachable(); + } + } + return ss.str(); +} + +Node PicklerPrivate::fromCaseOperator(Kind k, uint32_t nchildren) { + kind::MetaKind m = metaKindOf(k); + bool parameterized = (m == kind::metakind::PARAMETERIZED); + uint32_t npops = nchildren + (parameterized? 1 : 0); + + NodeStack aux; + while(npops > 0) { + Assert(!d_stack.empty()); + Node top = d_stack.top(); + aux.push(top); + d_stack.pop(); + --npops; + } + + NodeBuilder<> nb(d_nm, k); + while(!aux.empty()) { + Node top = aux.top(); + nb << top; + aux.pop(); + } + + return nb; +} + +Pickle::Pickle() { + d_data = new PickleData(); +} + +// Just copying the pointer isn't right, we have to copy the +// underlying data. Otherwise user-level Pickles will delete the data +// twice! (once in each thread) +Pickle::Pickle(const Pickle& p) { + d_data = new PickleData(*p.d_data); +} + +Pickle& Pickle::operator = (const Pickle& other) { + if (this != &other) { + delete d_data; + d_data = new PickleData(*other.d_data); + } + return *this; +} + + +Pickle::~Pickle() { + delete d_data; +} + +}/* CVC4::expr::pickle namespace */ +}/* CVC4::expr namespace */ +}/* CVC4 namespace */ diff --git a/src/expr/pickler.h b/src/expr/pickler.h new file mode 100644 index 000000000..264ae0e4b --- /dev/null +++ b/src/expr/pickler.h @@ -0,0 +1,139 @@ +/********************* */ +/*! \file pickle.h + ** \verbatim + ** Original author: kshitij + ** Major contributors: taking, mdeters + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief This is a "pickler" for expressions + ** + ** This is a "pickler" for expressions. It produces a binary + ** serialization of an expression that can be converted back + ** into an expression in the same or another ExprManager. + **/ + +#include "cvc4_public.h" + +#ifndef __CVC4__PICKLER_H +#define __CVC4__PICKLER_H + +#include "expr/variable_type_map.h" +#include "expr/expr.h" +#include "util/exception.h" + +#include +#include + +namespace CVC4 { + +class ExprManager; + +namespace expr { +namespace pickle { + +class Pickler; +class PicklerPrivate; + +class PickleData;// CVC4-internal representation + +class CVC4_PUBLIC Pickle { + PickleData* d_data; + friend class Pickler; + friend class PicklerPrivate; +public: + Pickle(); + Pickle(const Pickle& p); + ~Pickle(); + Pickle& operator = (const Pickle& other); +};/* class Pickle */ + +class CVC4_PUBLIC PicklingException : public Exception { +public: + PicklingException() : + Exception("Pickling failed") { + } +};/* class PicklingException */ + +class CVC4_PUBLIC Pickler { + PicklerPrivate* d_private; + + friend class PicklerPrivate; + +protected: + virtual uint64_t variableToMap(uint64_t x) const + throw(AssertionException, PicklingException) { + return x; + } + virtual uint64_t variableFromMap(uint64_t x) const { + return x; + } + +public: + Pickler(ExprManager* em); + ~Pickler(); + + /** + * Constructs a new Pickle of the node n. + * n must be a node allocated in the node manager specified at initialization + * time. The new pickle has variables mapped using the VariableIDMap provided + * at initialization. + * TODO: Fix comment + * + * @return the pickle, which should be dispose()'d when you're done with it + */ + void toPickle(Expr e, Pickle& p) throw(AssertionException, PicklingException); + + /** + * Constructs a node from a Pickle. + * This destroys the contents of the Pickle. + * The node is created in the NodeManager getNM(); + * TODO: Fix comment + */ + Expr fromPickle(Pickle& p); + + static void debugPickleTest(Expr e); + +};/* class Pickler */ + +class MapPickler : public Pickler { +private: + const VarMap& d_toMap; + const VarMap& d_fromMap; + +public: + MapPickler(ExprManager* em, const VarMap& to, const VarMap& from): + Pickler(em), + d_toMap(to), + d_fromMap(from) { + } + +protected: + + virtual uint64_t variableToMap(uint64_t x) const + throw(AssertionException, PicklingException){ + VarMap::const_iterator i = d_toMap.find(x); + if(i != d_toMap.end()){ + return i->second; + }else{ + throw PicklingException(); + } + } + + virtual uint64_t variableFromMap(uint64_t x) const { + VarMap::const_iterator i = d_fromMap.find(x); + Assert(i != d_fromMap.end()); + return i->second; + } +};/* class MapPickler */ + +}/* CVC4::expr::pickle namespace */ +}/* CVC4::expr namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__PICKLER_H */ diff --git a/src/expr/type.cpp b/src/expr/type.cpp index 7e06a05ae..a901af73a 100644 --- a/src/expr/type.cpp +++ b/src/expr/type.cpp @@ -162,6 +162,10 @@ ExprManager* Type::getExprManager() const { return d_nodeManager->toExprManager(); } +Type Type::exportTo(ExprManager* exprManager, ExprManagerMapCollection& vmap) { + return ExprManager::exportType(*this, exprManager, vmap); +} + void Type::toStream(std::ostream& out) const { NodeManagerScope nms(d_nodeManager); out << *d_typeNode; diff --git a/src/expr/type.h b/src/expr/type.h index 0b50fbd3c..34cc925f6 100644 --- a/src/expr/type.h +++ b/src/expr/type.h @@ -35,6 +35,7 @@ class NodeManager; class ExprManager; class Expr; class TypeNode; +class ExprManagerMapCollection; class SmtEngine; @@ -75,6 +76,10 @@ struct CVC4_PUBLIC TypeHashFunction { */ std::ostream& operator<<(std::ostream& out, const Type& t) CVC4_PUBLIC; +namespace expr { + TypeNode exportTypeInternal(TypeNode n, NodeManager* from, NodeManager* nm, ExprManagerMapCollection& vmap); +}/* CVC4::expr namespace */ + /** * Class encapsulating CVC4 expression types. */ @@ -86,6 +91,7 @@ class CVC4_PUBLIC Type { friend class TypeNode; friend struct TypeHashStrategy; friend std::ostream& CVC4::operator<<(std::ostream& out, const Type& t); + friend TypeNode expr::exportTypeInternal(TypeNode n, NodeManager* from, NodeManager* nm, ExprManagerMapCollection& vmap); protected: @@ -165,6 +171,11 @@ public: */ ExprManager* getExprManager() const; + /** + * Exports this type into a different ExprManager. + */ + Type exportTo(ExprManager* exprManager, ExprManagerMapCollection& vmap); + /** * Assignment operator. * @param t the type to assign to this type diff --git a/src/expr/type_node.h b/src/expr/type_node.h index 553f83276..c7da5ceb7 100644 --- a/src/expr/type_node.h +++ b/src/expr/type_node.h @@ -228,6 +228,16 @@ public: return TypeNode(d_nv->getChild(i)); } + /** + * PARAMETERIZED-metakinded types (the SORT_TYPE is one of these) + * have an operator. "Little-p parameterized" types (like Array), + * are OPERATORs, not PARAMETERIZEDs. + */ + inline Node getOperator() const { + Assert(getMetaKind() == kind::metakind::PARAMETERIZED); + return Node(d_nv->getChild(-1)); + } + /** * Returns the unique id of this node * diff --git a/src/expr/variable_type_map.h b/src/expr/variable_type_map.h new file mode 100644 index 000000000..a34bec846 --- /dev/null +++ b/src/expr/variable_type_map.h @@ -0,0 +1,64 @@ +/********************* */ +/*! \file variable_type_map.h + ** \verbatim + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + +#include "cvc4_public.h" + +#ifndef __CVC4__VARIABLE_TYPE_MAP_H +#define __CVC4__VARIABLE_TYPE_MAP_H + +#include "expr/expr.h" +#include "util/hash.h" + +namespace CVC4 { + +class Expr; +struct ExprHashFunction; +class Type; +struct TypeHashFunction; + +class CVC4_PUBLIC VariableTypeMap { + /** + * A map Expr -> Expr, intended to be used for a mapping of variables + * between two ExprManagers. + */ + std::hash_map d_variables; + + /** + * A map Type -> Type, intended to be used for a mapping of types + * between two ExprManagers. + */ + std::hash_map d_types; + +public: + Expr& operator[](Expr e) { return d_variables[e]; } + Type& operator[](Type t) { return d_types[t]; } + +};/* class VariableTypeMap */ + +typedef __gnu_cxx::hash_map VarMap; + +struct CVC4_PUBLIC ExprManagerMapCollection { + VariableTypeMap d_typeMap; + VarMap d_to; + VarMap d_from; +}; + +}/* CVC4 namespace */ + +#endif /* __CVC4__VARIABLE_MAP_H */ diff --git a/src/main/Makefile.am b/src/main/Makefile.am index 78d468000..ae7764e32 100644 --- a/src/main/Makefile.am +++ b/src/main/Makefile.am @@ -4,16 +4,42 @@ AM_CPPFLAGS = \ AM_CXXFLAGS = -Wall -Wno-unknown-pragmas bin_PROGRAMS = cvc4 + noinst_LIBRARIES = libmain.a libmain_a_SOURCES = \ interactive_shell.h \ interactive_shell.cpp \ main.h \ - main.cpp \ util.cpp -cvc4_SOURCES = +if CVC4_HAS_THREADS +bin_PROGRAMS += pcvc4 +pcvc4_SOURCES = \ + main.cpp \ + portfolio.cpp \ + portfolio.h \ + driver_portfolio.cpp +pcvc4_LDADD = \ + libmain.a \ + @builddir@/../parser/libcvc4parser.la \ + @builddir@/../libcvc4.la \ + @builddir@/../lib/libreplacements.la \ + $(READLINE_LIBS) +pcvc4_CPPFLAGS = $(AM_CPPFLAGS) $(BOOST_CPPFLAGS) +pcvc4_LDADD += $(BOOST_THREAD_LIBS) -lpthread +pcvc4_LDADD += $(BOOST_THREAD_LDFLAGS) + +if STATIC_BINARY +pcvc4_LINK = $(CXXLINK) -all-static +else +pcvc4_LINK = $(CXXLINK) +endif +endif + +cvc4_SOURCES = \ + main.cpp \ + driver.cpp cvc4_LDADD = \ libmain.a \ @builddir@/../parser/libcvc4parser.la \ @@ -44,3 +70,4 @@ cvc4_LINK = $(CXXLINK) -all-static else cvc4_LINK = $(CXXLINK) endif + diff --git a/src/main/driver.cpp b/src/main/driver.cpp new file mode 100644 index 000000000..e9bfde024 --- /dev/null +++ b/src/main/driver.cpp @@ -0,0 +1,355 @@ +/********************* */ +/*! \file driver.cpp + ** \verbatim + ** Original author: mdeters + ** Major contributors: cconway + ** Minor contributors (to current version): barrett, dejan, taking + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011, 2012 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Driver for (sequential) CVC4 executable + ** + ** Driver for (sequential) CVC4 executable. + **/ + +#include +#include +#include +#include +#include + +#include +#include + +#include "cvc4autoconfig.h" +#include "main/main.h" +#include "main/interactive_shell.h" +#include "parser/parser.h" +#include "parser/parser_builder.h" +#include "parser/parser_exception.h" +#include "expr/expr_manager.h" +#include "smt/smt_engine.h" +#include "expr/command.h" +#include "util/Assert.h" +#include "util/configuration.h" +#include "util/options.h" +#include "util/output.h" +#include "util/result.h" +#include "util/stats.h" + +using namespace std; +using namespace CVC4; +using namespace CVC4::parser; +using namespace CVC4::main; + +static bool doCommand(SmtEngine&, Command*, Options&); + +namespace CVC4 { + namespace main { + /** Global options variable */ + CVC4_THREADLOCAL(Options*) pOptions; + + /** Full argv[0] */ + const char *progPath; + + /** Just the basename component of argv[0] */ + const char *progName; + + /** A pointer to the StatisticsRegistry (the signal handlers need it) */ + CVC4::StatisticsRegistry* pStatistics; + } +} + + +void printUsage(Options& options, bool full) { + stringstream ss; + ss << "usage: " << options.binary_name << " [options] [input-file]" << endl + << endl + << "Without an input file, or with `-', CVC4 reads from standard input." << endl + << endl + << "CVC4 options:" << endl; + if(full) { + Options::printUsage( ss.str(), *options.out ); + } else { + Options::printShortUsage( ss.str(), *options.out ); + } +} + +int runCvc4(int argc, char* argv[], Options& options) { + + // For the signal handlers' benefit + pOptions = &options; + + // Initialize the signal handlers + cvc4_init(); + + progPath = argv[0]; + + // Parse the options + int firstArgIndex = options.parseOptions(argc, argv); + + progName = options.binary_name.c_str(); + + if( options.help ) { + printUsage(options, true); + exit(1); + } else if( options.languageHelp ) { + Options::printLanguageHelp(*options.out); + exit(1); + } else if( options.version ) { + *options.out << Configuration::about().c_str() << flush; + exit(0); + } + + segvNoSpin = options.segvNoSpin; + + // If in competition mode, set output stream option to flush immediately +#ifdef CVC4_COMPETITION_MODE + *options.out << unitbuf; +#endif + + // We only accept one input file + if(argc > firstArgIndex + 1) { + throw Exception("Too many input files specified."); + } + + // If no file supplied we will read from standard input + const bool inputFromStdin = + firstArgIndex >= argc || !strcmp("-", argv[firstArgIndex]); + + // if we're reading from stdin on a TTY, default to interactive mode + if(!options.interactiveSetByUser) { + options.interactive = inputFromStdin && isatty(fileno(stdin)); + } + + // Determine which messages to show based on smtcomp_mode and verbosity + if(Configuration::isMuzzledBuild()) { + Debug.setStream(CVC4::null_os); + Trace.setStream(CVC4::null_os); + Notice.setStream(CVC4::null_os); + Chat.setStream(CVC4::null_os); + Message.setStream(CVC4::null_os); + Warning.setStream(CVC4::null_os); + Dump.setStream(CVC4::null_os); + } else { + if(options.verbosity < 2) { + Chat.setStream(CVC4::null_os); + } + if(options.verbosity < 1) { + Notice.setStream(CVC4::null_os); + } + if(options.verbosity < 0) { + Message.setStream(CVC4::null_os); + Warning.setStream(CVC4::null_os); + } + } + + // Create the expression manager + ExprManager exprMgr(options); + + // Create the SmtEngine + SmtEngine smt(&exprMgr); + + // signal handlers need access + pStatistics = smt.getStatisticsRegistry(); + + // Auto-detect input language by filename extension + const char* filename = inputFromStdin ? "" : argv[firstArgIndex]; + + ReferenceStat< const char* > s_statFilename("filename", filename); + RegisterStatistic statFilenameReg(exprMgr, &s_statFilename); + + if(options.inputLanguage == language::input::LANG_AUTO) { + if( inputFromStdin ) { + // We can't do any fancy detection on stdin + options.inputLanguage = language::input::LANG_CVC4; + } else { + unsigned len = strlen(filename); + if(len >= 5 && !strcmp(".smt2", filename + len - 5)) { + options.inputLanguage = language::input::LANG_SMTLIB_V2; + } else if(len >= 4 && !strcmp(".smt", filename + len - 4)) { + options.inputLanguage = language::input::LANG_SMTLIB; + } else if(( len >= 4 && !strcmp(".cvc", filename + len - 4) ) + || ( len >= 5 && !strcmp(".cvc4", filename + len - 5) )) { + options.inputLanguage = language::input::LANG_CVC4; + } + } + } + + if(options.outputLanguage == language::output::LANG_AUTO) { + options.outputLanguage = language::toOutputLanguage(options.inputLanguage); + } + + // Determine which messages to show based on smtcomp_mode and verbosity + if(Configuration::isMuzzledBuild()) { + Debug.setStream(CVC4::null_os); + Trace.setStream(CVC4::null_os); + Notice.setStream(CVC4::null_os); + Chat.setStream(CVC4::null_os); + Message.setStream(CVC4::null_os); + Warning.setStream(CVC4::null_os); + Dump.setStream(CVC4::null_os); + } else { + if(options.verbosity < 2) { + Chat.setStream(CVC4::null_os); + } + if(options.verbosity < 1) { + Notice.setStream(CVC4::null_os); + } + if(options.verbosity < 0) { + Message.setStream(CVC4::null_os); + Warning.setStream(CVC4::null_os); + } + + Debug.getStream() << Expr::setlanguage(options.outputLanguage); + Trace.getStream() << Expr::setlanguage(options.outputLanguage); + Notice.getStream() << Expr::setlanguage(options.outputLanguage); + Chat.getStream() << Expr::setlanguage(options.outputLanguage); + Message.getStream() << Expr::setlanguage(options.outputLanguage); + Warning.getStream() << Expr::setlanguage(options.outputLanguage); + Dump.getStream() << Expr::setlanguage(options.outputLanguage) + << Expr::setdepth(-1) + << Expr::printtypes(false); + } + + Parser* replayParser = NULL; + if( options.replayFilename != "" ) { + ParserBuilder replayParserBuilder(&exprMgr, options.replayFilename, options); + + if( options.replayFilename == "-") { + if( inputFromStdin ) { + throw OptionException("Replay file and input file can't both be stdin."); + } + replayParserBuilder.withStreamInput(cin); + } + replayParser = replayParserBuilder.build(); + options.replayStream = new Parser::ExprStream(replayParser); + } + if( options.replayLog != NULL ) { + *options.replayLog << Expr::setlanguage(options.outputLanguage) << Expr::setdepth(-1); + } + + // Parse and execute commands until we are done + Command* cmd; + bool status = true; + if( options.interactive ) { + InteractiveShell shell(exprMgr, options); + Message() << Configuration::getPackageName() + << " " << Configuration::getVersionString(); + if(Configuration::isSubversionBuild()) { + Message() << " [" << Configuration::getSubversionId() << "]"; + } + Message() << (Configuration::isDebugBuild() ? " DEBUG" : "") + << " assertions:" + << (Configuration::isAssertionBuild() ? "on" : "off") + << endl; + if(replayParser != NULL) { + // have the replay parser use the declarations input interactively + replayParser->useDeclarationsFrom(shell.getParser()); + } + while((cmd = shell.readCommand())) { + status = doCommand(smt,cmd, options) && status; + delete cmd; + } + } else { + ParserBuilder parserBuilder(&exprMgr, filename, options); + + if( inputFromStdin ) { + parserBuilder.withStreamInput(cin); + } + + Parser *parser = parserBuilder.build(); + if(replayParser != NULL) { + // have the replay parser use the file's declarations + replayParser->useDeclarationsFrom(parser); + } + while((cmd = parser->nextCommand())) { + status = doCommand(smt, cmd, options) && status; + delete cmd; + } + // Remove the parser + delete parser; + } + + if( options.replayStream != NULL ) { + // this deletes the expression parser too + delete options.replayStream; + options.replayStream = NULL; + } + + int returnValue; + string result = "unknown"; + if(status) { + result = smt.getInfo(":status").getValue(); + + if(result == "sat") { + returnValue = 10; + } else if(result == "unsat") { + returnValue = 20; + } else { + returnValue = 0; + } + } else { + // there was some kind of error + returnValue = 1; + } + +#ifdef CVC4_COMPETITION_MODE + // exit, don't return + // (don't want destructors to run) + exit(returnValue); +#endif + + ReferenceStat< Result > s_statSatResult("sat/unsat", result); + RegisterStatistic statSatResultReg(exprMgr, &s_statSatResult); + + if(options.statistics) { + pStatistics->flushInformation(*options.err); + } + + return returnValue; +} + +/** Executes a command. Deletes the command after execution. */ +static bool doCommand(SmtEngine& smt, Command* cmd, Options& options) { + if( options.parseOnly ) { + return true; + } + + // assume no error + bool status = true; + + CommandSequence *seq = dynamic_cast(cmd); + if(seq != NULL) { + for(CommandSequence::iterator subcmd = seq->begin(); + subcmd != seq->end(); + ++subcmd) { + status = doCommand(smt, *subcmd, options) && status; + } + } else { + // by default, symmetry breaker is on only for QF_UF + if(! options.ufSymmetryBreakerSetByUser) { + SetBenchmarkLogicCommand *logic = dynamic_cast(cmd); + if(logic != NULL) { + options.ufSymmetryBreaker = (logic->getLogic() == "QF_UF"); + } + } + + if(options.verbosity > 0) { + *options.out << "Invoking: " << *cmd << endl; + } + + if(options.verbosity >= 0) { + cmd->invoke(&smt, *options.out); + } else { + cmd->invoke(&smt); + } + status = status && cmd->ok(); + } + + return status; +} diff --git a/src/main/driver_portfolio.cpp b/src/main/driver_portfolio.cpp new file mode 100644 index 000000000..5c8f908f8 --- /dev/null +++ b/src/main/driver_portfolio.cpp @@ -0,0 +1,808 @@ +#include +#include +#include +#include // for gettimeofday() + +#include + +#include +#include +#include +#include + +#include "cvc4autoconfig.h" +#include "main/main.h" +#include "main/interactive_shell.h" +#include "parser/parser.h" +#include "parser/parser_builder.h" +#include "parser/parser_exception.h" +#include "expr/expr_manager.h" +#include "expr/variable_type_map.h" +#include "smt/smt_engine.h" +#include "expr/command.h" +#include "util/Assert.h" +#include "util/configuration.h" +#include "util/options.h" +#include "util/output.h" +#include "util/result.h" +#include "util/stats.h" + +#include "expr/pickler.h" +#include "util/channel.h" + +#include "main/portfolio.h" + +using namespace std; +using namespace CVC4; +using namespace CVC4::parser; +using namespace CVC4::main; + +/* Global variables */ + +namespace CVC4 { + namespace main { + + StatisticsRegistry theStatisticsRegistry; + + /** A pointer to the StatisticsRegistry (the signal handlers need it) */ + CVC4::StatisticsRegistry* pStatistics; + + }/* CVC4::main namespace */ +}/* CVC4 namespace */ + +/* Function declarations */ + +static bool doCommand(SmtEngine&, Command*, Options&); + +Result doSmt(SmtEngine &smt, Command *cmd, Options &options); + +template +void sharingManager(int numThreads, + SharedChannel* channelsOut[], + SharedChannel* channelsIn[], + SmtEngine* smts[]); + + +/* To monitor for activity on shared channels */ +bool global_activity; +bool global_activity_true() { return global_activity; } +bool global_activity_false() { return not global_activity; } +boost::condition global_activity_cond; + +typedef expr::pickle::Pickle channelFormat; /* Remove once we are using Pickle */ + +template +class EmptySharedChannel: public SharedChannel { +public: + EmptySharedChannel(int) {} + bool push(const T&) { return true; } + T pop() { return T(); } + bool empty() { return true; } + bool full() { return false; } +}; + +class PortfolioLemmaOutputChannel : public LemmaOutputChannel { +private: + string d_tag; + SharedChannel* d_sharedChannel; + expr::pickle::MapPickler d_pickler; + +public: + int cnt; + PortfolioLemmaOutputChannel(string tag, + SharedChannel *c, + ExprManager* em, + VarMap& to, + VarMap& from) : + d_tag(tag), + d_sharedChannel(c), + d_pickler(em, to, from) + ,cnt(0) + {} + + void notifyNewLemma(Expr lemma) { + if(Debug.isOn("disable-lemma-sharing")) return; + const Options *options = Options::current(); + if(options->sharingFilterByLength >= 0) { // 0 would mean no-sharing effectively + if( int(lemma.getNumChildren()) > options->sharingFilterByLength) + return; + } + ++cnt; + Trace("sharing") << d_tag << ": " << lemma << std::endl; + expr::pickle::Pickle pkl; + try{ + d_pickler.toPickle(lemma, pkl); + d_sharedChannel->push(pkl); + if(Trace.isOn("showSharing") and options->thread_id == 0) { + *(Options::current()->out) << "thread #0: notifyNewLemma: " << lemma << endl; + } + }catch(expr::pickle::PicklingException& p){ + Trace("sharing::blocked") << lemma << std::endl; + } + } + +}; + +/* class PortfolioLemmaInputChannel */ +class PortfolioLemmaInputChannel : public LemmaInputChannel { +private: + string d_tag; + SharedChannel* d_sharedChannel; + expr::pickle::MapPickler d_pickler; + +public: + PortfolioLemmaInputChannel(string tag, + SharedChannel* c, + ExprManager* em, + VarMap& to, + VarMap& from) : + d_tag(tag), + d_sharedChannel(c), + d_pickler(em, to, from){ + } + + bool hasNewLemma(){ + Debug("lemmaInputChannel") << d_tag << ": " << "hasNewLemma" << endl; + return !d_sharedChannel->empty(); + } + + Expr getNewLemma() { + Debug("lemmaInputChannel") << d_tag << ": " << "getNewLemma" << endl; + expr::pickle::Pickle pkl = d_sharedChannel->pop(); + + Expr e = d_pickler.fromPickle(pkl); + if(Trace.isOn("showSharing") and Options::current()->thread_id == 0) { + *(Options::current()->out) << "thread #0: getNewLemma: " << e << endl; + } + return e; + } + +};/* class PortfolioLemmaInputChannel */ + + + +int runCvc4(int argc, char *argv[], Options& options) { + +#ifdef CVC4_CLN_IMP + Warning() << "WARNING:" << endl + << "WARNING: This build of portfolio-CVC4 uses the CLN library" << endl + << "WARNING: which is not thread-safe! Expect crashes and" << endl + << "WARNING: incorrect answers." << endl + << "WARNING:" << endl; +#endif /* CVC4_CLN_IMP */ + + /************************************************************************** + * runCvc4 outline: + * -> Start a couple of timers + * -> Processing of options, including thread specific ones + * -> Statistics related stuff + * -> Create ExprManager, parse commands, duplicate exprMgrs using export + * -> Create smtEngines + * -> Lemma sharing init + * -> Run portfolio, exit/print stats etc. + * (This list might become outdated, a timestamp might be good: 7 Dec '11.) + **************************************************************************/ + + // Timer statistic + TimerStat s_totalTime("totalTime"); + TimerStat s_beforePortfolioTime("beforePortfolioTime"); + s_totalTime.start(); + s_beforePortfolioTime.start(); + + // For the signal handlers' benefit + pOptions = &options; + + // Initialize the signal handlers + cvc4_init(); + + progPath = argv[0]; + + + /****************************** Options Processing ************************/ + + // Parse the options + int firstArgIndex = options.parseOptions(argc, argv); + + progName = options.binary_name.c_str(); + + if( options.help ) { + printUsage(options, true); + exit(1); + } else if( options.languageHelp ) { + Options::printLanguageHelp(*options.out); + exit(1); + } else if( options.version ) { + *options.out << Configuration::about().c_str() << flush; + exit(0); + } + + int numThreads = options.threads; + + if(options.threadArgv.size() > size_t(numThreads)) { + stringstream ss; + ss << "--thread" << (options.threadArgv.size() - 1) + << " configuration string seen but this portfolio will only contain " + << numThreads << " thread(s)!"; + throw OptionException(ss.str()); + } + + segvNoSpin = options.segvNoSpin; + + // If in competition mode, set output stream option to flush immediately +#ifdef CVC4_COMPETITION_MODE + *options.out << unitbuf; +#endif + + // We only accept one input file + if(argc > firstArgIndex + 1) { + throw Exception("Too many input files specified."); + } + + // If no file supplied we will read from standard input + const bool inputFromStdin = + firstArgIndex >= argc || !strcmp("-", argv[firstArgIndex]); + + // if we're reading from stdin on a TTY, default to interactive mode + if(!options.interactiveSetByUser) { + options.interactive = inputFromStdin && isatty(fileno(stdin)); + } + + // Auto-detect input language by filename extension + const char* filename = inputFromStdin ? "" : argv[firstArgIndex]; + + if(options.inputLanguage == language::input::LANG_AUTO) { + if( inputFromStdin ) { + // We can't do any fancy detection on stdin + options.inputLanguage = language::input::LANG_CVC4; + } else { + unsigned len = strlen(filename); + if(len >= 5 && !strcmp(".smt2", filename + len - 5)) { + options.inputLanguage = language::input::LANG_SMTLIB_V2; + } else if(len >= 4 && !strcmp(".smt", filename + len - 4)) { + options.inputLanguage = language::input::LANG_SMTLIB; + } else if(( len >= 4 && !strcmp(".cvc", filename + len - 4) ) + || ( len >= 5 && !strcmp(".cvc4", filename + len - 5) )) { + options.inputLanguage = language::input::LANG_CVC4; + } + } + } + + // Determine which messages to show based on smtcomp_mode and verbosity + if(Configuration::isMuzzledBuild()) { + Debug.setStream(CVC4::null_os); + Trace.setStream(CVC4::null_os); + Notice.setStream(CVC4::null_os); + Chat.setStream(CVC4::null_os); + Message.setStream(CVC4::null_os); + Warning.setStream(CVC4::null_os); + } else { + if(options.verbosity < 2) { + Chat.setStream(CVC4::null_os); + } + if(options.verbosity < 1) { + Notice.setStream(CVC4::null_os); + } + if(options.verbosity < 0) { + Message.setStream(CVC4::null_os); + Warning.setStream(CVC4::null_os); + } + + OutputLanguage language = language::toOutputLanguage(options.inputLanguage); + Debug.getStream() << Expr::setlanguage(language); + Trace.getStream() << Expr::setlanguage(language); + Notice.getStream() << Expr::setlanguage(language); + Chat.getStream() << Expr::setlanguage(language); + Message.getStream() << Expr::setlanguage(language); + Warning.getStream() << Expr::setlanguage(language); + } + + vector threadOptions; + for(int i = 0; i < numThreads; ++i) { + threadOptions.push_back(options); + Options& opts = threadOptions.back(); + + // Set thread identifier + opts.thread_id = i; + + // If the random-seed is negative, pick a random seed randomly + if(options.satRandomSeed < 0) + opts.satRandomSeed = (double)rand(); + + if(i < (int)options.threadArgv.size() && !options.threadArgv[i].empty()) { + // separate out the thread's individual configuration string + stringstream optidss; + optidss << "--thread" << i; + string optid = optidss.str(); + int targc = 1; + char* tbuf = strdup(options.threadArgv[i].c_str()); + char* p = tbuf; + // string length is certainly an upper bound on size needed + char** targv = new char*[options.threadArgv[i].size()]; + char** vp = targv; + *vp++ = strdup(optid.c_str()); + p = strtok(p, " "); + while(p != NULL) { + *vp++ = p; + ++targc; + p = strtok(NULL, " "); + } + *vp++ = NULL; + if(targc > 1) { // this is necessary in case you do e.g. --thread0=" " + try { + opts.parseOptions(targc, targv); + } catch(OptionException& e) { + stringstream ss; + ss << optid << ": " << e.getMessage(); + throw OptionException(ss.str()); + } + if(optind != targc) { + stringstream ss; + ss << "unused argument `" << targv[optind] + << "' in thread configuration " << optid << " !"; + throw OptionException(ss.str()); + } + if(opts.threads != numThreads || opts.threadArgv != options.threadArgv) { + stringstream ss; + ss << "not allowed to set thread options in " << optid << " !"; + throw OptionException(ss.str()); + } + } + free(targv[0]); + delete targv; + free(tbuf); + } + } + + // Some more options related stuff + + /* Use satRandomSeed for generating random numbers, in particular satRandomSeed-s */ + srand((unsigned int)(-options.satRandomSeed)); + + assert(numThreads >= 1); //do we need this? + + /* Output to string stream */ + vector ss_out(numThreads); + if(options.verbosity == 0 or options.separateOutput) { + for(int i = 0;i s_statFilename("filename", filename); + RegisterStatistic* statFilenameReg = + new RegisterStatistic(&driverStatisticsRegistry, &s_statFilename); + + + /****************** ExprManager + CommandParsing + Export *****************/ + + // Create the expression manager + ExprManager* exprMgrs[numThreads]; + exprMgrs[0] = new ExprManager(threadOptions[0]); + ExprManager* exprMgr = exprMgrs[0]; // to avoid having to change code which uses that + + // Parse commands until we are done + Command* cmd; + // bool status = true; // Doesn't seem to be use right now: commenting it out + CommandSequence* seq = new CommandSequence(); + if( options.interactive ) { + InteractiveShell shell(*exprMgr, options); + Message() << Configuration::getPackageName() + << " " << Configuration::getVersionString(); + if(Configuration::isSubversionBuild()) { + Message() << " [subversion " << Configuration::getSubversionBranchName() + << " r" << Configuration::getSubversionRevision() + << (Configuration::hasSubversionModifications() ? + " (with modifications)" : "") + << "]"; + } + Message() << (Configuration::isDebugBuild() ? " DEBUG" : "") + << " assertions:" + << (Configuration::isAssertionBuild() ? "on" : "off") + << endl; + while((cmd = shell.readCommand())) { + seq->addCommand(cmd); + } + } else { + ParserBuilder parserBuilder = + ParserBuilder(exprMgr, filename). + withOptions(options); + + if( inputFromStdin ) { + parserBuilder.withStreamInput(cin); + } + + Parser *parser = parserBuilder.build(); + while((cmd = parser->nextCommand())) { + seq->addCommand(cmd); + // doCommand(smt, cmd, options); + // delete cmd; + } + // Remove the parser + delete parser; + } + + exprMgr = NULL; // don't want to use that variable + // after this point + + /* Duplication, Individualisation */ + ExprManagerMapCollection* vmaps[numThreads]; // vmaps[0] is generally empty + Command *seqs[numThreads]; + seqs[0] = seq; seq = NULL; + for(int i = 1; i < numThreads; ++i) { + vmaps[i] = new ExprManagerMapCollection(); + exprMgrs[i] = new ExprManager(threadOptions[i]); + seqs[i] = seqs[0]->exportTo(exprMgrs[i], *(vmaps[i]) ); + } + /** + * vmaps[i].d_from [x] = y means + * that in thread #0's expr manager id is y + * and in thread #i's expr manager id is x + * opposite for d_to + * + * d_from[x] : in a sense gives the id if converting *from* it to + * first thread + */ + + /** + * Create identity variable map for the first thread, with only + * those variables which have a corresponding variable in another + * thread. (TODO:Also assert, all threads have the same set of + * variables mapped.) + */ + if(numThreads >= 2) { + // Get keys from the first thread + //Set s = vmaps[1]->d_to.keys(); + vmaps[0] = new ExprManagerMapCollection(); // identity be default? + for(typeof(vmaps[1]->d_to.begin()) i=vmaps[1]->d_to.begin(); i!=vmaps[1]->d_to.end(); ++i) { + (vmaps[0]->d_from)[i->first] = i->first; + } + vmaps[0]->d_to = vmaps[0]->d_from; + } + + // Create the SmtEngine(s) + SmtEngine *smts[numThreads]; + for(int i = 0; i < numThreads; ++i) { + smts[i] = new SmtEngine(exprMgrs[i]); + + // Register the statistics registry of the thread + string tag = "thread #" + boost::lexical_cast(threadOptions[i].thread_id); + smts[i]->getStatisticsRegistry()->setName(tag); + theStatisticsRegistry.registerStat_( (Stat*)smts[i]->getStatisticsRegistry() ); + } + + /************************* Lemma sharing init ************************/ + + /* Sharing channels */ + SharedChannel *channelsOut[numThreads], *channelsIn[numThreads]; + + if(numThreads == 1) { + // Disable sharing + threadOptions[0].sharingFilterByLength = 0; + } else { + // Setup sharing channels + const unsigned int sharingChannelSize = 1000000; + + for(int i = 0; i(sharingChannelSize); + channelsIn[i] = new EmptySharedChannel(sharingChannelSize); + continue; + } + channelsOut[i] = new SynchronizedSharedChannel(sharingChannelSize); + channelsIn[i] = new SynchronizedSharedChannel(sharingChannelSize); + } + + /* Lemma output channel */ + for(int i = 0; i(threadOptions[i].thread_id); + threadOptions[i].lemmaOutputChannel = + new PortfolioLemmaOutputChannel(tag, channelsOut[i], exprMgrs[i], + vmaps[i]->d_from, vmaps[i]->d_to); + threadOptions[i].lemmaInputChannel = + new PortfolioLemmaInputChannel(tag, channelsIn[i], exprMgrs[i], + vmaps[i]->d_from, vmaps[i]->d_to); + } + } + + /************************** End of initialization ***********************/ + + /* Portfolio */ + boost::function fns[numThreads]; + + for(int i = 0; i < numThreads; ++i) { + fns[i] = boost::bind(doSmt, boost::ref(*smts[i]), seqs[i], boost::ref(threadOptions[i])); + } + + boost::function + smFn = boost::bind(sharingManager, numThreads, channelsOut, channelsIn, smts); + + s_beforePortfolioTime.stop(); + pair portfolioReturn = runPortfolio(numThreads, smFn, fns, true); + int winner = portfolioReturn.first; + Result result = portfolioReturn.second; + + cout << result << endl; + + /************************* Post printing answer ***********************/ + + if(options.printWinner){ + cout << "The winner is #" << winner << endl; + } + + Result satRes = result.asSatisfiabilityResult(); + int returnValue; + if(satRes.isSat() == Result::SAT) { + returnValue = 10; + } else if(satRes.isSat() == Result::UNSAT) { + returnValue = 20; + } else { + returnValue = 0; + } + +#ifdef CVC4_COMPETITION_MODE + // exit, don't return + // (don't want destructors to run) + exit(returnValue); +#endif + + // ReferenceStat< Result > s_statSatResult("sat/unsat", result); + // RegisterStatistic statSatResultReg(*exprMgr, &s_statSatResult); + + // Stop timers, enough work done + s_totalTime.stop(); + + if(options.statistics) { + pStatistics->flushInformation(*options.err); + } + + if(options.separateOutput) { + for(int i = 0; i < numThreads; ++i) { + *options.out << "--- Output from thread #" << i << " ---" << endl; + *options.out << ss_out[i]->str(); + } + } + + /*if(options.statistics) { + double totalTime = double(s_totalTime.getData().tv_sec) + + double(s_totalTime.getData().tv_nsec)/1000000000.0; + cout.precision(6); + *options.err << "real time: " << totalTime << "s\n"; + int th0_lemcnt = (*static_cast(options.lemmaOutputChannel)).cnt; + int th1_lemcnt = (*static_cast(threadOptions[1].lemmaOutputChannel)).cnt; + *options.err << "lemmas shared by thread #0: " << th0_lemcnt << endl; + *options.err << "lemmas shared by thread #1: " << th1_lemcnt << endl; + *options.err << "sharing rate: " << double(th0_lemcnt+th1_lemcnt)/(totalTime) + << " lem/sec" << endl; + *options.err << "winner: #" << (winner == 0 ? 0 : 1) << endl; + }*/ + + // destruction is causing segfaults, let us just exit + exit(returnValue); + + //delete vmaps; + + delete statTotatTime; + delete statBeforePortfolioTime; + delete statFilenameReg; + + // delete seq; + // delete exprMgr; + + // delete seq2; + // delete exprMgr2; + + return returnValue; +} + +/**** Code shared with driver.cpp ****/ + +namespace CVC4 { + namespace main {/* Global options variable */ + CVC4_THREADLOCAL(Options*) pOptions; + + /** Full argv[0] */ + const char *progPath; + + /** Just the basename component of argv[0] */ + const char *progName; + } +} + +void printUsage(Options& options, bool full) { + stringstream ss; + ss << "usage: " << options.binary_name << " [options] [input-file]" << endl + << endl + << "Without an input file, or with `-', CVC4 reads from standard input." << endl + << endl + << "CVC4 options:" << endl; + if(full) { + Options::printUsage( ss.str(), *options.out ); + } else { + Options::printShortUsage( ss.str(), *options.out ); + } +} + +/** Executes a command. Deletes the command after execution. */ +static bool doCommand(SmtEngine& smt, Command* cmd, Options& options) { + if( options.parseOnly ) { + return true; + } + + // assume no error + bool status = true; + + CommandSequence *seq = dynamic_cast(cmd); + if(seq != NULL) { + for(CommandSequence::iterator subcmd = seq->begin(); + subcmd != seq->end(); + ++subcmd) { + status = doCommand(smt, *subcmd, options) && status; + } + } else { + // by default, symmetry breaker is on only for QF_UF + if(! options.ufSymmetryBreakerSetByUser) { + SetBenchmarkLogicCommand *logic = dynamic_cast(cmd); + if(logic != NULL) { + options.ufSymmetryBreaker = (logic->getLogic() == "QF_UF"); + } + } + + if(options.verbosity > 0) { + *options.out << "Invoking: " << *cmd << endl; + } + + if(options.verbosity >= 0) { + cmd->invoke(&smt, *options.out); + } else { + cmd->invoke(&smt); + } + status = status && cmd->ok(); + } + + return status; +} + +/**** End of code shared with driver.cpp ****/ + +/** Create the SMT engine and execute the commands */ +Result doSmt(SmtEngine &smt, Command *cmd, Options &options) { + + try { + // For the signal handlers' benefit + pOptions = &options; + + // Execute the commands + bool status = doCommand(smt, cmd, options); + + // if(options.statistics) { + // smt.getStatisticsRegistry()->flushInformation(*options.err); + // *options.err << "Statistics printing of my thread complete " << endl; + // } + + return status ? smt.getStatusOfLastCommand() : Result::SAT_UNKNOWN; + } catch(OptionException& e) { + *pOptions->out << "unknown" << endl; + cerr << "CVC4 Error:" << endl << e << endl; + printUsage(*pOptions); + return Result::SAT_UNKNOWN; + } catch(Exception& e) { +#ifdef CVC4_COMPETITION_MODE + *pOptions->out << "unknown" << endl; +#endif + *pOptions->err << "CVC4 Error:" << endl << e << endl; + if(pOptions->statistics) { + pStatistics->flushInformation(*pOptions->err); + } + return Result::SAT_UNKNOWN; + } catch(bad_alloc) { +#ifdef CVC4_COMPETITION_MODE + *pOptions->out << "unknown" << endl; +#endif + *pOptions->err << "CVC4 ran out of memory." << endl; + if(pOptions->statistics) { + pStatistics->flushInformation(*pOptions->err); + } + return Result::SAT_UNKNOWN; + } catch(...) { +#ifdef CVC4_COMPETITION_MODE + *pOptions->out << "unknown" << endl; +#endif + *pOptions->err << "CVC4 threw an exception of unknown type." << endl; + return Result::SAT_UNKNOWN; + } +} + +template +void sharingManager(int numThreads, + SharedChannel *channelsOut[], // out and in with respect + SharedChannel *channelsIn[], + SmtEngine *smts[]) // to smt engines +{ + Trace("sharing") << "sharing: thread started " << std::endl; + vector cnt(numThreads); // Debug("sharing") + + vector< queue > queues; + for(int i = 0; i < numThreads; ++i){ + queues.push_back(queue()); + } + + const unsigned int sharingBroadcastInterval = 1; + + boost::mutex mutex_activity; + + /* Disable interruption, so that we can check manually */ + boost::this_thread::disable_interruption di; + + while(not boost::this_thread::interruption_requested()) { + + boost::this_thread::sleep(boost::posix_time::milliseconds(sharingBroadcastInterval)); + + for(int t = 0; t < numThreads; ++t) { + + if(channelsOut[t]->empty()) continue; /* No activity on this channel */ + + /* Alert if channel full, so that we increase sharingChannelSize + or decrease sharingBroadcastInterval */ + Assert(not channelsOut[t]->full()); + + T data = channelsOut[t]->pop(); + + if(Trace.isOn("sharing")) { + ++cnt[t]; + Trace("sharing") << "sharing: Got data. Thread #" << t + << ". Chunk " << cnt[t] << std :: endl; + } + + for(int u = 0; u < numThreads; ++u) { + if(u != t){ + Trace("sharing") << "sharing: adding to queue " << u << std::endl; + queues[u].push(data); + } + }/* end of inner for: broadcast activity */ + + } /* end of outer for: look for activity */ + + for(int t = 0; t < numThreads; ++t){ + /* Alert if channel full, so that we increase sharingChannelSize + or decrease sharingBroadcastInterval */ + Assert(not channelsIn[t]->full()); + + while(!queues[t].empty() && !channelsIn[t]->full()){ + Trace("sharing") << "sharing: pushing on channel " << t << std::endl; + T data = queues[t].front(); + channelsIn[t]->push(data); + queues[t].pop(); + } + } + } /* end of infinite while */ + + Trace("interrupt") << "sharing thread interuppted, interrupting all smtEngines" << std::endl; + + for(int t = 0; t < numThreads; ++t) { + Trace("interrupt") << "Interuppting thread #" << t << std::endl; + try{ + smts[t]->interrupt(); + }catch(ModalException &e){ + // It's fine, the thread is probably not there. + Trace("interrupt") << "Could not interrupt thread #" << t << std::endl; + } + } + + Trace("sharing") << "sharing: Interuppted, exiting." << std::endl; +} diff --git a/src/main/interactive_shell.cpp b/src/main/interactive_shell.cpp index dca554330..a63d6c67b 100644 --- a/src/main/interactive_shell.cpp +++ b/src/main/interactive_shell.cpp @@ -85,7 +85,7 @@ InteractiveShell::InteractiveShell(ExprManager& exprManager, d_out(*options.out), d_language(options.inputLanguage), d_quit(false) { - ParserBuilder parserBuilder(&exprManager,INPUT_FILENAME,options); + ParserBuilder parserBuilder(&exprManager, INPUT_FILENAME, options); /* Create parser with bogus input. */ d_parser = parserBuilder.withStringInput("").build(); diff --git a/src/main/main.cpp b/src/main/main.cpp index ecef7e79f..5d051cdad 100644 --- a/src/main/main.cpp +++ b/src/main/main.cpp @@ -20,12 +20,10 @@ #include #include #include -#include #include #include -#include "cvc4autoconfig.h" #include "main/main.h" #include "main/interactive_shell.h" #include "parser/parser.h" @@ -43,42 +41,8 @@ using namespace std; using namespace CVC4; -using namespace CVC4::parser; using namespace CVC4::main; -static int runCvc4(int argc, char* argv[]); -static bool doCommand(SmtEngine&, Command*); -static void printUsage(bool full = false); - -namespace CVC4 { - namespace main { - /** Global options variable */ - Options options; - - /** Full argv[0] */ - const char *progPath; - - /** Just the basename component of argv[0] */ - const char *progName; - - /** A pointer to the StatisticsRegistry (the signal handlers need it) */ - CVC4::StatisticsRegistry* pStatistics; - } -} - -static void printUsage(bool full) { - stringstream ss; - ss << "usage: " << options.binary_name << " [options] [input-file]" << endl - << endl - << "Without an input file, or with `-', CVC4 reads from standard input." << endl - << endl; - if(full) { - Options::printUsage( ss.str(), *options.out ); - } else { - Options::printShortUsage( ss.str(), *options.out ); - } -} - /** * CVC4's main() routine is just an exception-safe wrapper around CVC4. * Please don't construct anything here. Even if the constructor is @@ -87,14 +51,15 @@ static void printUsage(bool full) { * Put everything in runCvc4(). */ int main(int argc, char* argv[]) { + Options options; try { - return runCvc4(argc, argv); + return runCvc4(argc, argv, options); } catch(OptionException& e) { #ifdef CVC4_COMPETITION_MODE *options.out << "unknown" << endl; #endif cerr << "CVC4 Error:" << endl << e << endl; - printUsage(); + printUsage(options); exit(1); } catch(Exception& e) { #ifdef CVC4_COMPETITION_MODE @@ -102,7 +67,7 @@ int main(int argc, char* argv[]) { #endif *options.err << "CVC4 Error:" << endl << e << endl; if(options.statistics && pStatistics != NULL) { - pStatistics->flushStatistics(*options.err); + pStatistics->flushInformation(*options.err); } exit(1); } catch(bad_alloc&) { @@ -111,7 +76,7 @@ int main(int argc, char* argv[]) { #endif *options.err << "CVC4 ran out of memory." << endl; if(options.statistics && pStatistics != NULL) { - pStatistics->flushStatistics(*options.err); + pStatistics->flushInformation(*options.err); } exit(1); } catch(...) { @@ -122,276 +87,3 @@ int main(int argc, char* argv[]) { exit(1); } } - - -static int runCvc4(int argc, char* argv[]) { - - // Initialize the signal handlers - cvc4_init(); - - progPath = argv[0]; - - // Parse the options - int firstArgIndex = options.parseOptions(argc, argv); - - progName = options.binary_name.c_str(); - - if( options.help ) { - printUsage(true); - exit(1); - } else if( options.languageHelp ) { - Options::printLanguageHelp(*options.out); - exit(1); - } else if( options.version ) { - *options.out << Configuration::about().c_str() << flush; - exit(0); - } - - segvNoSpin = options.segvNoSpin; - - // If in competition mode, set output stream option to flush immediately -#ifdef CVC4_COMPETITION_MODE - *options.out << unitbuf; -#endif - - // We only accept one input file - if(argc > firstArgIndex + 1) { - throw Exception("Too many input files specified."); - } - - // If no file supplied we will read from standard input - const bool inputFromStdin = - firstArgIndex >= argc || !strcmp("-", argv[firstArgIndex]); - - // if we're reading from stdin on a TTY, default to interactive mode - if(!options.interactiveSetByUser) { - options.interactive = inputFromStdin && isatty(fileno(stdin)); - } - - // Determine which messages to show based on smtcomp_mode and verbosity - if(Configuration::isMuzzledBuild()) { - Debug.setStream(CVC4::null_os); - Trace.setStream(CVC4::null_os); - Notice.setStream(CVC4::null_os); - Chat.setStream(CVC4::null_os); - Message.setStream(CVC4::null_os); - Warning.setStream(CVC4::null_os); - Dump.setStream(CVC4::null_os); - } else { - if(options.verbosity < 2) { - Chat.setStream(CVC4::null_os); - } - if(options.verbosity < 1) { - Notice.setStream(CVC4::null_os); - } - if(options.verbosity < 0) { - Message.setStream(CVC4::null_os); - Warning.setStream(CVC4::null_os); - } - } - - // Create the expression manager - ExprManager exprMgr(options); - - // Create the SmtEngine - SmtEngine smt(&exprMgr); - - // signal handlers need access - pStatistics = smt.getStatisticsRegistry(); - - // Auto-detect input language by filename extension - const char* filename = inputFromStdin ? "" : argv[firstArgIndex]; - - ReferenceStat< const char* > s_statFilename("filename", filename); - RegisterStatistic statFilenameReg(exprMgr, &s_statFilename); - - if(options.inputLanguage == language::input::LANG_AUTO) { - if( inputFromStdin ) { - // We can't do any fancy detection on stdin - options.inputLanguage = language::input::LANG_CVC4; - } else { - unsigned len = strlen(filename); - if(len >= 5 && !strcmp(".smt2", filename + len - 5)) { - options.inputLanguage = language::input::LANG_SMTLIB_V2; - } else if(len >= 4 && !strcmp(".smt", filename + len - 4)) { - options.inputLanguage = language::input::LANG_SMTLIB; - } else if(( len >= 4 && !strcmp(".cvc", filename + len - 4) ) - || ( len >= 5 && !strcmp(".cvc4", filename + len - 5) )) { - options.inputLanguage = language::input::LANG_CVC4; - } - } - } - - if(options.outputLanguage == language::output::LANG_AUTO) { - options.outputLanguage = language::toOutputLanguage(options.inputLanguage); - } - - // Determine which messages to show based on smtcomp_mode and verbosity - if(Configuration::isMuzzledBuild()) { - Debug.setStream(CVC4::null_os); - Trace.setStream(CVC4::null_os); - Notice.setStream(CVC4::null_os); - Chat.setStream(CVC4::null_os); - Message.setStream(CVC4::null_os); - Warning.setStream(CVC4::null_os); - Dump.setStream(CVC4::null_os); - } else { - if(options.verbosity < 2) { - Chat.setStream(CVC4::null_os); - } - if(options.verbosity < 1) { - Notice.setStream(CVC4::null_os); - } - if(options.verbosity < 0) { - Message.setStream(CVC4::null_os); - Warning.setStream(CVC4::null_os); - } - - Debug.getStream() << Expr::setlanguage(options.outputLanguage); - Trace.getStream() << Expr::setlanguage(options.outputLanguage); - Notice.getStream() << Expr::setlanguage(options.outputLanguage); - Chat.getStream() << Expr::setlanguage(options.outputLanguage); - Message.getStream() << Expr::setlanguage(options.outputLanguage); - Warning.getStream() << Expr::setlanguage(options.outputLanguage); - Dump.getStream() << Expr::setlanguage(options.outputLanguage) - << Expr::setdepth(-1) - << Expr::printtypes(false); - } - - Parser* replayParser = NULL; - if( options.replayFilename != "" ) { - ParserBuilder replayParserBuilder(&exprMgr, options.replayFilename, options); - - if( options.replayFilename == "-") { - if( inputFromStdin ) { - throw OptionException("Replay file and input file can't both be stdin."); - } - replayParserBuilder.withStreamInput(cin); - } - replayParser = replayParserBuilder.build(); - options.replayStream = new Parser::ExprStream(replayParser); - } - if( options.replayLog != NULL ) { - *options.replayLog << Expr::setlanguage(options.outputLanguage) << Expr::setdepth(-1); - } - - // Parse and execute commands until we are done - Command* cmd; - bool status = true; - if( options.interactive ) { - InteractiveShell shell(exprMgr, options); - Message() << Configuration::getPackageName() - << " " << Configuration::getVersionString(); - if(Configuration::isSubversionBuild()) { - Message() << " [" << Configuration::getSubversionId() << "]"; - } - Message() << (Configuration::isDebugBuild() ? " DEBUG" : "") - << " assertions:" - << (Configuration::isAssertionBuild() ? "on" : "off") - << endl; - if(replayParser != NULL) { - // have the replay parser use the declarations input interactively - replayParser->useDeclarationsFrom(shell.getParser()); - } - while((cmd = shell.readCommand())) { - status = doCommand(smt, cmd) && status; - delete cmd; - } - } else { - ParserBuilder parserBuilder(&exprMgr, filename, options); - - if( inputFromStdin ) { - parserBuilder.withStreamInput(cin); - } - - Parser *parser = parserBuilder.build(); - if(replayParser != NULL) { - // have the replay parser use the file's declarations - replayParser->useDeclarationsFrom(parser); - } - while((cmd = parser->nextCommand())) { - status = doCommand(smt, cmd) && status; - delete cmd; - } - // Remove the parser - delete parser; - } - - if( options.replayStream != NULL ) { - // this deletes the expression parser too - delete options.replayStream; - options.replayStream = NULL; - } - - int returnValue; - string result = "unknown"; - if(status) { - result = smt.getInfo(":status").getValue(); - - if(result == "sat") { - returnValue = 10; - } else if(result == "unsat") { - returnValue = 20; - } else { - returnValue = 0; - } - } else { - // there was some kind of error - returnValue = 1; - } - -#ifdef CVC4_COMPETITION_MODE - // exit, don't return - // (don't want destructors to run) - exit(returnValue); -#endif - - ReferenceStat< Result > s_statSatResult("sat/unsat", result); - RegisterStatistic statSatResultReg(exprMgr, &s_statSatResult); - - if(options.statistics) { - smt.getStatisticsRegistry()->flushStatistics(*options.err); - } - - return returnValue; -} - -/** Executes a command. Deletes the command after execution. */ -static bool doCommand(SmtEngine& smt, Command* cmd) { - if( options.parseOnly ) { - return true; - } - - // assume no error - bool status = true; - - CommandSequence *seq = dynamic_cast(cmd); - if(seq != NULL) { - for(CommandSequence::iterator subcmd = seq->begin(); - subcmd != seq->end(); - ++subcmd) { - status = doCommand(smt, *subcmd) && status; - } - } else { - // by default, symmetry breaker is on only for QF_UF - if(! options.ufSymmetryBreakerSetByUser) { - SetBenchmarkLogicCommand *logic = dynamic_cast(cmd); - if(logic != NULL) { - options.ufSymmetryBreaker = (logic->getLogic() == "QF_UF"); - } - } - - if(options.verbosity > 0) { - *options.out << "Invoking: " << *cmd << endl; - } - - if(options.verbosity >= 0) { - cmd->invoke(&smt, *options.out); - } else { - cmd->invoke(&smt); - } - status = status && cmd->ok(); - } - - return status; -} diff --git a/src/main/main.h b/src/main/main.h index 1771198f4..4df5ccc49 100644 --- a/src/main/main.h +++ b/src/main/main.h @@ -22,6 +22,7 @@ #include "util/options.h" #include "util/exception.h" #include "util/stats.h" +#include "util/tls.h" #include "cvc4autoconfig.h" #ifndef __CVC4__MAIN__MAIN_H @@ -46,8 +47,8 @@ extern CVC4::StatisticsRegistry* pStatistics; */ extern bool segvNoSpin; -/** The options currently in play */ -extern Options options; +/** A pointer to the options in play */ +extern CVC4_THREADLOCAL(Options*) pOptions; /** Initialize the driver. Sets signal handlers for SIGINT and SIGSEGV. */ void cvc4_init() throw(Exception); @@ -55,4 +56,8 @@ void cvc4_init() throw(Exception); }/* CVC4::main namespace */ }/* CVC4 namespace */ +/** Actual Cvc4 driver functions **/ +int runCvc4(int argc, char* argv[], CVC4::Options&); +void printUsage(CVC4::Options&, bool full = false); + #endif /* __CVC4__MAIN__MAIN_H */ diff --git a/src/main/portfolio.cpp b/src/main/portfolio.cpp new file mode 100644 index 000000000..fc22374cf --- /dev/null +++ b/src/main/portfolio.cpp @@ -0,0 +1,93 @@ +/********************* */ +/*! \file portfolio.cpp + ** \verbatim + ** Original author: kshitij + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009-2012 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + +#include +#include +#include +#include +#include + +#include "smt/smt_engine.h" +#include "util/result.h" +#include "util/options.h" + +using namespace boost; + +namespace CVC4 { + +mutex mutex_done; +mutex mutex_main_wait; +condition condition_var_main_wait; + +bool global_flag_done = false; +int global_winner = -1; + +template +void runThread(int thread_id, function threadFn, S& returnValue) { + returnValue = threadFn(); + + if( mutex_done.try_lock() ) { + if(global_flag_done == false) { + global_flag_done = true; + global_winner = thread_id; + } + mutex_done.unlock(); + condition_var_main_wait.notify_all(); // we want main thread to quit + } +} + +template +std::pair runPortfolio(int numThreads, + function driverFn, + function threadFns[], + bool optionWaitToJoin) { + thread thread_driver; + thread threads[numThreads]; + S threads_returnValue[numThreads]; + + for(int t = 0; t < numThreads; ++t) { + threads[t] = thread(bind(runThread, t, threadFns[t], ref(threads_returnValue[t]) )); + } + + if(not driverFn.empty()) + thread_driver = boost::thread(driverFn); + + while(global_flag_done == false) + condition_var_main_wait.wait(mutex_main_wait); + + if(not driverFn.empty()) { + thread_driver.interrupt(); + thread_driver.join(); + } + + for(int t = 0; t < numThreads; ++t) { + if(optionWaitToJoin) { + threads[t].join(); + } + } + + return std::pair(global_winner,threads_returnValue[global_winner]); +} + +// instantiation +template +std::pair +runPortfolio(int, boost::function, boost::function*, bool); + +}/* CVC4 namespace */ diff --git a/src/main/portfolio.h b/src/main/portfolio.h new file mode 100644 index 000000000..9bc911be3 --- /dev/null +++ b/src/main/portfolio.h @@ -0,0 +1,42 @@ +/********************* */ +/*! \file portfolio.h + ** \verbatim + ** Original author: kshitij + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009-2012 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + +#ifndef __CVC4__PORTFOLIO_H +#define __CVC4__PORTFOLIO_H + +#include +#include + +#include "smt/smt_engine.h" +#include "expr/command.h" +#include "util/options.h" + +namespace CVC4 { + +template +std::pair runPortfolio(int numThreads, + boost::function driverFn, + boost::function threadFns[], + bool optionWaitToJoin); +// as we have defined things, S=void would give compile errors +// do we want to fix this? yes, no, maybe? + +}/* CVC4 namespace */ + +#endif /* __CVC4__PORTFOLIO_H */ diff --git a/src/main/util.cpp b/src/main/util.cpp index 89aa5c6aa..35cff4abd 100644 --- a/src/main/util.cpp +++ b/src/main/util.cpp @@ -51,8 +51,8 @@ bool segvNoSpin = false; /** Handler for SIGXCPU, i.e., timeout. */ void timeout_handler(int sig, siginfo_t* info, void*) { fprintf(stderr, "CVC4 interrupted by timeout.\n"); - if(options.statistics && pStatistics != NULL) { - pStatistics->flushStatistics(cerr); + if(pOptions->statistics && pStatistics != NULL) { + pStatistics->flushInformation(cerr); } abort(); } @@ -60,8 +60,8 @@ void timeout_handler(int sig, siginfo_t* info, void*) { /** Handler for SIGINT, i.e., when the user hits control C. */ void sigint_handler(int sig, siginfo_t* info, void*) { fprintf(stderr, "CVC4 interrupted by user.\n"); - if(options.statistics && pStatistics != NULL) { - pStatistics->flushStatistics(cerr); + if(pOptions->statistics && pStatistics != NULL) { + pStatistics->flushInformation(cerr); } abort(); } @@ -85,8 +85,8 @@ void segv_handler(int sig, siginfo_t* info, void* c) { if(segvNoSpin) { fprintf(stderr, "No-spin requested, aborting...\n"); - if(options.statistics && pStatistics != NULL) { - pStatistics->flushStatistics(cerr); + if(pOptions->statistics && pStatistics != NULL) { + pStatistics->flushInformation(cerr); } abort(); } else { @@ -105,8 +105,8 @@ void segv_handler(int sig, siginfo_t* info, void* c) { } else if(addr < 10*1024) { cerr << "Looks like a NULL pointer was dereferenced." << endl; } - if(options.statistics && pStatistics != NULL) { - pStatistics->flushStatistics(cerr); + if(pOptions->statistics && pStatistics != NULL) { + pStatistics->flushInformation(cerr); } abort(); #endif /* CVC4_DEBUG */ @@ -118,8 +118,8 @@ void ill_handler(int sig, siginfo_t* info, void*) { fprintf(stderr, "CVC4 executed an illegal instruction in DEBUG mode.\n"); if(segvNoSpin) { fprintf(stderr, "No-spin requested, aborting...\n"); - if(options.statistics && pStatistics != NULL) { - pStatistics->flushStatistics(cerr); + if(pOptions->statistics && pStatistics != NULL) { + pStatistics->flushInformation(cerr); } abort(); } else { @@ -131,8 +131,8 @@ void ill_handler(int sig, siginfo_t* info, void*) { } #else /* CVC4_DEBUG */ fprintf(stderr, "CVC4 executed an illegal instruction.\n"); - if(options.statistics && pStatistics != NULL) { - pStatistics->flushStatistics(cerr); + if(pOptions->statistics && pStatistics != NULL) { + pStatistics->flushInformation(cerr); } abort(); #endif /* CVC4_DEBUG */ @@ -155,8 +155,8 @@ void cvc4unexpected() { } if(segvNoSpin) { fprintf(stderr, "No-spin requested.\n"); - if(options.statistics && pStatistics != NULL) { - pStatistics->flushStatistics(cerr); + if(pOptions->statistics && pStatistics != NULL) { + pStatistics->flushInformation(cerr); } set_terminate(default_terminator); } else { @@ -168,8 +168,8 @@ void cvc4unexpected() { } #else /* CVC4_DEBUG */ fprintf(stderr, "CVC4 threw an \"unexpected\" exception.\n"); - if(options.statistics && pStatistics != NULL) { - pStatistics->flushStatistics(cerr); + if(pOptions->statistics && pStatistics != NULL) { + pStatistics->flushInformation(cerr); } set_terminate(default_terminator); #endif /* CVC4_DEBUG */ @@ -181,16 +181,16 @@ void cvc4terminate() { "CVC4 was terminated by the C++ runtime.\n" "Perhaps an exception was thrown during stack unwinding. " "(Don't do that.)\n"); - if(options.statistics && pStatistics != NULL) { - pStatistics->flushStatistics(cerr); + if(pOptions->statistics && pStatistics != NULL) { + pStatistics->flushInformation(cerr); } default_terminator(); #else /* CVC4_DEBUG */ fprintf(stderr, "CVC4 was terminated by the C++ runtime.\n" "Perhaps an exception was thrown during stack unwinding.\n"); - if(options.statistics && pStatistics != NULL) { - pStatistics->flushStatistics(cerr); + if(pOptions->statistics && pStatistics != NULL) { + pStatistics->flushInformation(cerr); } default_terminator(); #endif /* CVC4_DEBUG */ diff --git a/src/parser/parser_builder.cpp b/src/parser/parser_builder.cpp index 5c755b5f6..c17956e62 100644 --- a/src/parser/parser_builder.cpp +++ b/src/parser/parser_builder.cpp @@ -28,26 +28,25 @@ #include "util/options.h" namespace CVC4 { - namespace parser { -ParserBuilder::ParserBuilder(ExprManager* exprManager, - const std::string& filename) : +ParserBuilder::ParserBuilder(ExprManager* exprManager, + const std::string& filename) : d_filename(filename), d_exprManager(exprManager) { - init(exprManager,filename); + init(exprManager, filename); } -ParserBuilder::ParserBuilder(ExprManager* exprManager, - const std::string& filename, +ParserBuilder::ParserBuilder(ExprManager* exprManager, + const std::string& filename, const Options& options) : d_filename(filename), d_exprManager(exprManager) { - init(exprManager,filename); + init(exprManager, filename); withOptions(options); } -void ParserBuilder::init(ExprManager* exprManager, +void ParserBuilder::init(ExprManager* exprManager, const std::string& filename) { d_inputType = FILE_INPUT; d_lang = language::input::LANG_AUTO; @@ -60,26 +59,26 @@ void ParserBuilder::init(ExprManager* exprManager, d_parseOnly = false; } -Parser *ParserBuilder::build() - throw (InputStreamException,AssertionException) { - Input *input = NULL; +Parser* ParserBuilder::build() + throw (InputStreamException, AssertionException) { + Input* input = NULL; switch( d_inputType ) { case FILE_INPUT: - input = Input::newFileInput(d_lang,d_filename,d_mmap); + input = Input::newFileInput(d_lang, d_filename, d_mmap); break; case STREAM_INPUT: AlwaysAssert( d_streamInput != NULL, "Uninitialized stream input in ParserBuilder::build()" ); - input = Input::newStreamInput(d_lang,*d_streamInput,d_filename); + input = Input::newStreamInput(d_lang, *d_streamInput, d_filename); break; case STRING_INPUT: - input = Input::newStringInput(d_lang,d_stringInput,d_filename); + input = Input::newStringInput(d_lang, d_stringInput, d_filename); break; default: Unreachable(); } - Parser *parser = NULL; + Parser* parser = NULL; switch(d_lang) { case language::input::LANG_SMTLIB: parser = new Smt(d_exprManager, input, d_strictMode, d_parseOnly); @@ -162,6 +161,5 @@ ParserBuilder& ParserBuilder::withStringInput(const std::string& input) { return *this; } -} /* namespace parser */ - -} /* namespace CVC4 */ +}/* CVC4::parser namespace */ +}/* CVC4 namespace */ diff --git a/src/parser/parser_builder.h b/src/parser/parser_builder.h index 0463a079f..ce01d3c53 100644 --- a/src/parser/parser_builder.h +++ b/src/parser/parser_builder.h @@ -61,7 +61,7 @@ class CVC4_PUBLIC ParserBuilder { std::string d_stringInput; /** The stream input, if any. */ - std::istream *d_streamInput; + std::istream* d_streamInput; /** The expression manager */ ExprManager* d_exprManager; diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp index 09e072370..7f1456639 100644 --- a/src/prop/cnf_stream.cpp +++ b/src/prop/cnf_stream.cpp @@ -43,8 +43,9 @@ using namespace CVC4::kind; namespace CVC4 { namespace prop { -CnfStream::CnfStream(SatInputInterface *satSolver, theory::Registrar registrar) : +CnfStream::CnfStream(SatInputInterface *satSolver, theory::Registrar registrar, bool fullLitToNodeMap) : d_satSolver(satSolver), + d_fullLitToNodeMap(fullLitToNodeMap), d_registrar(registrar) { } @@ -129,7 +130,7 @@ void TseitinCnfStream::ensureLiteral(TNode n) { n.toString().c_str(), n.getType().toString().c_str()); - bool negated = false; + bool negated CVC4_UNUSED = false; SatLiteral lit; if(n.getKind() == kind::NOT) { @@ -178,7 +179,7 @@ SatLiteral CnfStream::newLiteral(TNode node, bool theoryLiteral) { d_translationCache[node.notNode()].level = level; // If it's a theory literal, need to store it for back queries - if ( theoryLiteral || + if ( theoryLiteral || d_fullLitToNodeMap || ( CVC4_USE_REPLAY && Options::current()->replayLog != NULL ) || Dump.isOn("clauses") ) { d_nodeCache[lit] = node; diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h index 5eaeeef94..c9fd4a08b 100644 --- a/src/prop/cnf_stream.h +++ b/src/prop/cnf_stream.h @@ -69,6 +69,13 @@ protected: TranslationCache d_translationCache; NodeCache d_nodeCache; + /** + * True if the lit-to-Node map should be kept for all lits, not just + * theory lits. This is true if e.g. replay logging is on, which + * dumps the Nodes corresponding to decision literals. + */ + const bool d_fullLitToNodeMap; + /** The "registrar" for pre-registration of terms */ theory::Registrar d_registrar; @@ -179,8 +186,10 @@ public: * set of clauses and sends them to the given sat solver. * @param satSolver the sat solver to use * @param registrar the entity that takes care of preregistration of Nodes + * @param fullLitToNodeMap maintain a full SAT-literal-to-Node mapping, + * even for non-theory literals. */ - CnfStream(SatInputInterface* satSolver, theory::Registrar registrar); + CnfStream(SatInputInterface* satSolver, theory::Registrar registrar, bool fullLitToNodeMap = false); /** * Destructs a CnfStream. This implementation does nothing, but we @@ -283,7 +292,7 @@ public: private: /** - * Same as above, except that removable is rememebered. + * Same as above, except that removable is remembered. */ void convertAndAssert(TNode node, bool negated); diff --git a/src/prop/sat.cpp b/src/prop/sat.cpp index 36f411df4..7df7535dd 100644 --- a/src/prop/sat.cpp +++ b/src/prop/sat.cpp @@ -22,6 +22,7 @@ #include "prop/sat.h" #include "context/context.h" #include "theory/theory_engine.h" +#include "theory/rewriter.h" #include "expr/expr_stream.h" namespace CVC4 { @@ -89,6 +90,55 @@ TNode SatSolver::getNode(SatLiteral lit) { void SatSolver::notifyRestart() { d_propEngine->checkTime(); d_theoryEngine->notifyRestart(); + + static uint32_t lemmaCount = 0; + + if(Options::current()->lemmaInputChannel != NULL) { + while(Options::current()->lemmaInputChannel->hasNewLemma()) { + Debug("shared") << "shared" << std::endl; + Expr lemma = Options::current()->lemmaInputChannel->getNewLemma(); + Node asNode = lemma.getNode(); + asNode = theory::Rewriter::rewrite(asNode); + + if(d_shared.find(asNode) == d_shared.end()) { + d_shared.insert(asNode); + if(asNode.getKind() == kind::OR) { + ++lemmaCount; + if(lemmaCount % 1 == 0) { + Debug("shared") << "=) " << asNode << std::endl; + } + d_propEngine->assertLemma(d_theoryEngine->preprocess(asNode), false, true); + } else { + Debug("shared") << "=(" << asNode << std::endl; + } + } else { + Debug("shared") <<"drop shared " << asNode << std::endl; + } + } + } +} + +void SatSolver::notifyNewLemma(SatClause& lemma) { + Assert(lemma.size() > 0); + if(Options::current()->lemmaOutputChannel != NULL) { + if(lemma.size() == 1) { + // cannot share units yet + //Options::current()->lemmaOutputChannel->notifyNewLemma(d_cnfStream->getNode(lemma[0]).toExpr()); + } else { + NodeBuilder<> b(kind::OR); + for(unsigned i = 0, i_end = lemma.size(); i < i_end; ++i) { + b << d_cnfStream->getNode(lemma[i]); + } + Node n = b; + + if(d_shared.find(n) == d_shared.end()) { + d_shared.insert(n); + Options::current()->lemmaOutputChannel->notifyNewLemma(n.toExpr()); + } else { + Debug("shared") <<"drop new " << n << std::endl; + } + } + } } SatLiteral SatSolver::getNextReplayDecision() { diff --git a/src/prop/sat.h b/src/prop/sat.h index be3ed244b..e86443827 100644 --- a/src/prop/sat.h +++ b/src/prop/sat.h @@ -137,6 +137,12 @@ class SatSolver : public SatInputInterface { /** Context we will be using to synchronzie the sat solver */ context::Context* d_context; + /** + * Set of all lemmas that have been "shared" in the portfolio---i.e., + * all imported and exported lemmas. + */ + std::hash_set d_shared; + /* Pointer to the concrete SAT solver. Including this via the preprocessor saves us a level of indirection vs, e.g., defining a sub-class for each solver. */ @@ -263,6 +269,8 @@ public: void notifyRestart(); + void notifyNewLemma(SatClause& lemma); + SatLiteral getNextReplayDecision(); void logDecision(SatLiteral lit); @@ -294,6 +302,12 @@ inline SatSolver::SatSolver(PropEngine* propEngine, d_minisat->random_var_freq = Options::current()->satRandomFreq; d_minisat->random_seed = Options::current()->satRandomSeed; + // Give access to all possible options in the sat solver + d_minisat->var_decay = Options::current()->satVarDecay; + d_minisat->clause_decay = Options::current()->satClauseDecay; + d_minisat->restart_first = Options::current()->satRestartFirst; + d_minisat->restart_inc = Options::current()->satRestartInc; + d_statistics.init(d_minisat); } diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index a8f2d5700..52a98f414 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -455,6 +455,10 @@ public: */ StatisticsRegistry* getStatisticsRegistry() const; + Result getStatusOfLastCommand() const { + return d_status; + } + };/* class SmtEngine */ }/* CVC4 namespace */ diff --git a/src/theory/arith/arith_priority_queue.cpp b/src/theory/arith/arith_priority_queue.cpp index 3b1f5f395..e74a250a3 100644 --- a/src/theory/arith/arith_priority_queue.cpp +++ b/src/theory/arith/arith_priority_queue.cpp @@ -191,12 +191,15 @@ void ArithPriorityQueue::transitionToDifferenceMode() { switch(d_pivotRule){ case MINIMUM: + Debug("arith::pivotRule") << "Making the minimum heap." << endl; make_heap(d_diffQueue.begin(), d_diffQueue.end(), VarDRatPair::minimumRule); break; case BREAK_TIES: + Debug("arith::pivotRule") << "Making the break ties heap." << endl; make_heap(d_diffQueue.begin(), d_diffQueue.end(), VarDRatPair::breakTiesRules); break; case MAXIMUM: + Debug("arith::pivotRule") << "Making the maximum heap." << endl; make_heap(d_diffQueue.begin(), d_diffQueue.end(), VarDRatPair::maximumRule); break; } diff --git a/src/theory/arith/simplex.cpp b/src/theory/arith/simplex.cpp index 27fb0bb02..26cdb2cdb 100644 --- a/src/theory/arith/simplex.cpp +++ b/src/theory/arith/simplex.cpp @@ -619,9 +619,9 @@ Node SimplexDecisionProcedure::updateInconsistentVars(){ if(d_queue.empty()){ return Node::null(); } - static unsigned int instance = 0; - ++instance; + static CVC4_THREADLOCAL(unsigned int) instance = 0; + ++instance; Debug("arith::updateInconsistentVars") << "begin updateInconsistentVars() " << instance << endl; diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 64e713b0a..268829105 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -1223,7 +1223,7 @@ void TheoryArith::presolve(){ if(Debug.isOn("paranoid:check_tableau")){ d_simplex.debugCheckTableau(); } - static int callCount = 0; + static CVC4_THREADLOCAL(unsigned) callCount = 0; Debug("arith::presolve") << "TheoryArith::presolve #" << (callCount++) << endl; d_learner.clear(); diff --git a/src/theory/arith/theory_arith_type_rules.h b/src/theory/arith/theory_arith_type_rules.h index 9c69ec684..511982d48 100644 --- a/src/theory/arith/theory_arith_type_rules.h +++ b/src/theory/arith/theory_arith_type_rules.h @@ -29,7 +29,7 @@ namespace arith { class ArithConstantTypeRule { public: inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) - throw (TypeCheckingExceptionPrivate) { + throw (TypeCheckingExceptionPrivate, AssertionException) { if (n.getKind() == kind::CONST_RATIONAL) return nodeManager->realType(); return nodeManager->integerType(); } @@ -38,7 +38,7 @@ public: class ArithOperatorTypeRule { public: inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) - throw (TypeCheckingExceptionPrivate) { + throw (TypeCheckingExceptionPrivate, AssertionException) { TypeNode integerType = nodeManager->integerType(); TypeNode realType = nodeManager->realType(); TNode::iterator child_it = n.begin(); @@ -65,7 +65,7 @@ public: class ArithPredicateTypeRule { public: inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) - throw (TypeCheckingExceptionPrivate) { + throw (TypeCheckingExceptionPrivate, AssertionException) { if( check ) { TypeNode integerType = nodeManager->integerType(); TypeNode realType = nodeManager->realType(); diff --git a/src/theory/arrays/theory_arrays_type_rules.h b/src/theory/arrays/theory_arrays_type_rules.h index bd3c8ad67..fd9e7cb2f 100644 --- a/src/theory/arrays/theory_arrays_type_rules.h +++ b/src/theory/arrays/theory_arrays_type_rules.h @@ -27,7 +27,7 @@ namespace arrays { struct ArraySelectTypeRule { inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) - throw (TypeCheckingExceptionPrivate) { + throw (TypeCheckingExceptionPrivate, AssertionException) { Assert(n.getKind() == kind::SELECT); TypeNode arrayType = n[0].getType(check); if( check ) { @@ -45,7 +45,7 @@ struct ArraySelectTypeRule { struct ArrayStoreTypeRule { inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) - throw (TypeCheckingExceptionPrivate) { + throw (TypeCheckingExceptionPrivate, AssertionException) { Assert(n.getKind() == kind::STORE); TypeNode arrayType = n[0].getType(check); if( check ) { diff --git a/src/theory/booleans/theory_bool_type_rules.h b/src/theory/booleans/theory_bool_type_rules.h index e6c3e0f54..3b30b9f59 100644 --- a/src/theory/booleans/theory_bool_type_rules.h +++ b/src/theory/booleans/theory_bool_type_rules.h @@ -28,7 +28,7 @@ namespace boolean { class BooleanTypeRule { public: inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) - throw (TypeCheckingExceptionPrivate) { + throw (TypeCheckingExceptionPrivate, AssertionException) { TypeNode booleanType = nodeManager->booleanType(); if( check ) { TNode::iterator child_it = n.begin(); @@ -49,7 +49,7 @@ public: class IteTypeRule { public: inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) - throw (TypeCheckingExceptionPrivate) { + throw (TypeCheckingExceptionPrivate, AssertionException) { TypeNode iteType = n[1].getType(check); if( check ) { TypeNode booleanType = nodeManager->booleanType(); diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h index 86603f004..cd3e1437f 100644 --- a/src/theory/builtin/theory_builtin_type_rules.h +++ b/src/theory/builtin/theory_builtin_type_rules.h @@ -34,7 +34,7 @@ namespace builtin { class ApplyTypeRule { public: inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) - throw (TypeCheckingExceptionPrivate) { + throw (TypeCheckingExceptionPrivate, AssertionException) { TNode f = n.getOperator(); TypeNode fType = f.getType(check); if( !fType.isFunction() && n.getNumChildren() > 0 ) { @@ -72,7 +72,7 @@ class ApplyTypeRule { class EqualityTypeRule { public: - inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) throw (TypeCheckingExceptionPrivate) { + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) throw (TypeCheckingExceptionPrivate, AssertionException) { TypeNode booleanType = nodeManager->booleanType(); if( check ) { diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp index a232ad33b..566bf3a68 100644 --- a/src/theory/bv/theory_bv_rewriter.cpp +++ b/src/theory/bv/theory_bv_rewriter.cpp @@ -84,7 +84,7 @@ RewriteResponse TheoryBVRewriter::postRewrite(TNode node) { return RewriteResponse(REWRITE_DONE, result); } -AllRewriteRules* TheoryBVRewriter::s_allRules = NULL; +CVC4_THREADLOCAL(AllRewriteRules*) TheoryBVRewriter::s_allRules = NULL; void TheoryBVRewriter::init() { s_allRules = new AllRewriteRules; diff --git a/src/theory/bv/theory_bv_rewriter.h b/src/theory/bv/theory_bv_rewriter.h index 11a55ca61..f0eb621ca 100644 --- a/src/theory/bv/theory_bv_rewriter.h +++ b/src/theory/bv/theory_bv_rewriter.h @@ -32,7 +32,7 @@ struct AllRewriteRules; class TheoryBVRewriter { - static AllRewriteRules* s_allRules; + static CVC4_THREADLOCAL(AllRewriteRules*) s_allRules; public: diff --git a/src/theory/bv/theory_bv_type_rules.h b/src/theory/bv/theory_bv_type_rules.h index 926ceb767..192295bc0 100644 --- a/src/theory/bv/theory_bv_type_rules.h +++ b/src/theory/bv/theory_bv_type_rules.h @@ -30,7 +30,7 @@ namespace bv { class BitVectorConstantTypeRule { public: inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) - throw (TypeCheckingExceptionPrivate) { + throw (TypeCheckingExceptionPrivate, AssertionException) { return nodeManager->mkBitVectorType(n.getConst().getSize()); } }; @@ -38,7 +38,7 @@ public: class BitVectorCompRule { public: inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) - throw (TypeCheckingExceptionPrivate) { + throw (TypeCheckingExceptionPrivate, AssertionException) { if( check ) { TypeNode lhs = n[0].getType(check); TypeNode rhs = n[1].getType(check); @@ -53,7 +53,7 @@ public: class BitVectorArithRule { public: inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) - throw (TypeCheckingExceptionPrivate) { + throw (TypeCheckingExceptionPrivate, AssertionException) { unsigned maxWidth = 0; TNode::iterator it = n.begin(); TNode::iterator it_end = n.end(); @@ -72,7 +72,7 @@ public: class BitVectorFixedWidthTypeRule { public: inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) - throw (TypeCheckingExceptionPrivate) { + throw (TypeCheckingExceptionPrivate, AssertionException) { TNode::iterator it = n.begin(); TypeNode t = (*it).getType(check); if( check ) { @@ -93,7 +93,7 @@ public: class BitVectorPredicateTypeRule { public: inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) - throw (TypeCheckingExceptionPrivate) { + throw (TypeCheckingExceptionPrivate, AssertionException) { if( check ) { TypeNode lhsType = n[0].getType(check); if (!lhsType.isBitVector()) { @@ -111,7 +111,7 @@ public: class BitVectorExtractTypeRule { public: inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) - throw (TypeCheckingExceptionPrivate) { + throw (TypeCheckingExceptionPrivate, AssertionException) { BitVectorExtract extractInfo = n.getOperator().getConst(); // NOTE: We're throwing a type-checking exception here even @@ -137,7 +137,7 @@ public: class BitVectorConcatRule { public: inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) - throw (TypeCheckingExceptionPrivate) { + throw (TypeCheckingExceptionPrivate, AssertionException) { unsigned size = 0; TNode::iterator it = n.begin(); TNode::iterator it_end = n.end(); @@ -158,7 +158,7 @@ public: class BitVectorRepeatTypeRule { public: inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) - throw (TypeCheckingExceptionPrivate) { + throw (TypeCheckingExceptionPrivate, AssertionException) { TypeNode t = n[0].getType(check); // NOTE: We're throwing a type-checking exception here even // when check is false, bc if the argument isn't a bit-vector @@ -174,7 +174,7 @@ public: class BitVectorExtendTypeRule { public: inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) - throw (TypeCheckingExceptionPrivate) { + throw (TypeCheckingExceptionPrivate, AssertionException) { TypeNode t = n[0].getType(check); // NOTE: We're throwing a type-checking exception here even // when check is false, bc if the argument isn't a bit-vector diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 147fb868e..6385d1467 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -364,6 +364,12 @@ class TheoryEngine { << std::endl << QueryCommand(node.toExpr()) << std::endl; } + + // Share with other portfolio threads + if(Options::current()->lemmaOutputChannel != NULL) { + Options::current()->lemmaOutputChannel->notifyNewLemma(node.toExpr()); + } + // Remove the ITEs and assert to prop engine std::vector additionalLemmas; additionalLemmas.push_back(node); @@ -514,13 +520,13 @@ public: void staticLearning(TNode in, NodeBuilder<>& learned); /** - * Calls presolve() on all active theories and returns true + * Calls presolve() on all theories and returns true * if one of the theories discovers a conflict. */ bool presolve(); /** - * Calls postsolve() on all active theories. + * Calls postsolve() on all theories. */ void postsolve(); diff --git a/src/theory/uf/theory_uf_type_rules.h b/src/theory/uf/theory_uf_type_rules.h index 927a31e01..9b622bc15 100644 --- a/src/theory/uf/theory_uf_type_rules.h +++ b/src/theory/uf/theory_uf_type_rules.h @@ -28,7 +28,7 @@ namespace uf { class UfTypeRule { public: inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) - throw (TypeCheckingExceptionPrivate) { + throw (TypeCheckingExceptionPrivate, AssertionException) { TNode f = n.getOperator(); TypeNode fType = f.getType(check); if( !fType.isFunction() ) { diff --git a/src/util/Makefile.am b/src/util/Makefile.am index c5a20cd5d..3cb6ea16f 100644 --- a/src/util/Makefile.am +++ b/src/util/Makefile.am @@ -50,6 +50,9 @@ libutil_la_SOURCES = \ stats.cpp \ dynamic_array.h \ language.h \ + lemma_output_channel.h \ + channel.h \ + channel.cpp \ language.cpp \ ntuple.h \ recursion_breaker.h \ diff --git a/src/util/channel.cpp b/src/util/channel.cpp new file mode 100644 index 000000000..998550f8e --- /dev/null +++ b/src/util/channel.cpp @@ -0,0 +1,2 @@ +#include "channel.h" + diff --git a/src/util/channel.h b/src/util/channel.h new file mode 100644 index 000000000..1701feba9 --- /dev/null +++ b/src/util/channel.h @@ -0,0 +1,96 @@ + +#ifndef __CVC4__CHANNEL_H +#define __CVC4__CHANNEL_H + +#include +#include +#include +#include +#include +#include +#include + + +namespace CVC4 { + +template +class SharedChannel { +private: + int d_maxsize; // just call it size? +public: + SharedChannel() {} + SharedChannel(int maxsize) : d_maxsize(maxsize) {} + + /* Tries to add element and returns true if successful */ + virtual bool push(const T&) = 0; + + /* Removes an element from the channel */ + virtual T pop() = 0; + + /* */ + virtual bool empty() = 0; + + /* */ + virtual bool full() = 0; +}; + +/* +This code is from + +http://live.boost.org/doc/libs/1_46_1/libs/circular_buffer/doc/circular_buffer.html#boundedbuffer +*/ +template +class SynchronizedSharedChannel: public SharedChannel { +public: + typedef boost::circular_buffer container_type; + typedef typename container_type::size_type size_type; + typedef typename container_type::value_type value_type; + typedef typename boost::call_traits::param_type param_type; + + explicit SynchronizedSharedChannel(size_type capacity) : m_unread(0), m_container(capacity) {} + + bool push(param_type item){ + // param_type represents the "best" way to pass a parameter of type value_type to a method + + boost::mutex::scoped_lock lock(m_mutex); + m_not_full.wait(lock, boost::bind(&SynchronizedSharedChannel::is_not_full, this)); + m_container.push_front(item); + ++m_unread; + lock.unlock(); + m_not_empty.notify_one(); + return true; + }//function definitions need to be moved to cpp + + value_type pop(){ + value_type ret; + boost::mutex::scoped_lock lock(m_mutex); + m_not_empty.wait(lock, boost::bind(&SynchronizedSharedChannel::is_not_empty, this)); + ret = m_container[--m_unread]; + lock.unlock(); + m_not_full.notify_one(); + return ret; + } + + + bool empty() { return not is_not_empty(); } + bool full() { return not is_not_full(); } + +private: + SynchronizedSharedChannel(const SynchronizedSharedChannel&); // Disabled copy constructor + SynchronizedSharedChannel& operator = (const SynchronizedSharedChannel&); // Disabled assign operator + + bool is_not_empty() const { return m_unread > 0; } + bool is_not_full() const { return m_unread < m_container.capacity(); } + + size_type m_unread; + container_type m_container; + boost::mutex m_mutex; + boost::condition m_not_empty; + boost::condition m_not_full; +}; + +} + +#endif /* __CVC4__CHANNEL_H */ + + diff --git a/src/util/hash.h b/src/util/hash.h index 6183c5208..5f0189d44 100644 --- a/src/util/hash.h +++ b/src/util/hash.h @@ -26,6 +26,22 @@ namespace __gnu_cxx {} #include + +namespace __gnu_cxx { + +#if __WORDSIZE == 32 +// on 32-bit, we need a specialization of hash for 64-bit values +template <> +struct hash { + size_t operator()(uint64_t v) const { + return v; + } +};/* struct hash */ +#endif /* 32-bit */ + +}/* __gnu_cxx namespace */ + +// hackish: treat hash stuff as if it were in std namespace namespace std { using namespace __gnu_cxx; } namespace CVC4 { diff --git a/src/util/lemma_input_channel.h b/src/util/lemma_input_channel.h new file mode 100644 index 000000000..1627711ee --- /dev/null +++ b/src/util/lemma_input_channel.h @@ -0,0 +1,19 @@ +#include "cvc4_public.h" + +#ifndef __CVC4__LEMMA_INPUT_CHANNEL_H +#define __CVC4__LEMMA_INPUT_CHANNEL_H + +#include "expr/expr.h" + +namespace CVC4 { + +class CVC4_PUBLIC LemmaInputChannel { +public: + virtual bool hasNewLemma() = 0; + virtual Expr getNewLemma() = 0; + +};/* class LemmaOutputChannel */ + +}/* CVC4 namespace */ + +#endif /* __CVC4__LEMMA_INPUT_CHANNEL_H */ diff --git a/src/util/lemma_output_channel.h b/src/util/lemma_output_channel.h new file mode 100644 index 000000000..720dd6512 --- /dev/null +++ b/src/util/lemma_output_channel.h @@ -0,0 +1,46 @@ +/********************* */ +/*! \file lemma_output_channel.h + ** \verbatim + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Mechanism for communication about new lemmas + ** + ** This file defines an interface for use by the theory and propositional + ** engines to communicate new lemmas to the "outside world," for example + ** for lemma sharing between threads. + **/ + +#include "cvc4_public.h" + +#ifndef __CVC4__LEMMA_OUTPUT_CHANNEL_H +#define __CVC4__LEMMA_OUTPUT_CHANNEL_H + +#include "expr/expr.h" + +namespace CVC4 { + +/** + * This interface describes a mechanism for the propositional and theory + * engines to communicate with the "outside world" about new lemmas being + * discovered. + */ +class CVC4_PUBLIC LemmaOutputChannel { +public: + /** + * Notifies this output channel that there's a new lemma. + * The lemma may or may not be in CNF. + */ + virtual void notifyNewLemma(Expr lemma) = 0; +};/* class LemmaOutputChannel */ + +}/* CVC4 namespace */ + +#endif /* __CVC4__LEMMA_OUTPUT_CHANNEL_H */ diff --git a/src/util/options.cpp b/src/util/options.cpp index d33064c73..e33fbc263 100644 --- a/src/util/options.cpp +++ b/src/util/options.cpp @@ -64,6 +64,9 @@ Options::Options() : verbosity(0), inputLanguage(language::input::LANG_AUTO), outputLanguage(language::output::LANG_AUTO), + help(false), + version(false), + languageHelp(false), parseOnly(false), preprocessOnly(false), semanticChecks(DO_SEMANTIC_CHECKS_BY_DEFAULT), @@ -71,6 +74,7 @@ Options::Options() : memoryMap(false), strictParsing(false), lazyDefinitionExpansion(false), + printWinner(false), simplificationMode(SIMPLIFICATION_MODE_BATCH), doStaticLearning(true), interactive(false), @@ -93,12 +97,23 @@ Options::Options() : arithPropagation(true), satRandomFreq(0.0), satRandomSeed(91648253),// Minisat's default value + satVarDecay(0.95), + satClauseDecay(0.999), + satRestartFirst(25), + satRestartInc(3.0), pivotRule(MINIMUM), arithPivotThreshold(16), arithPropagateMaxLength(16), ufSymmetryBreaker(false), ufSymmetryBreakerSetByUser(false), - dioSolver(true) + dioSolver(true), + lemmaOutputChannel(NULL), + lemmaInputChannel(NULL), + threads(2),// default should be 1 probably, but say 2 for now + threadArgv(), + thread_id(-1), + separateOutput(false), + sharingFilterByLength(-1) { } @@ -141,6 +156,7 @@ Additional CVC4 options:\n\ --no-type-checking never type check expressions\n\ --no-checking disable ALL semantic checks, including type checks\n\ --no-theory-registration disable theory reg (not safe for some theories)\n\ + --print-winner enable printing the winning thread (pcvc4 only)\n\ --trace | -t trace something (e.g. -t pushpop), can repeat\n\ --debug | -d debug something (e.g. -d arith), can repeat\n\ --show-debug-tags show all avalable tags for debugging\n\ @@ -157,13 +173,19 @@ Additional CVC4 options:\n\ --prop-row-length=N sets the maximum row length to be used in propagation\n\ --random-freq=P sets the frequency of random decisions in the sat solver(P=0.0 by default)\n\ --random-seed=S sets the random seed for the sat solver\n\ + --restart-int-base=I sets the base restart interval for the sat solver (I=25 by default)\n\ + --restart-int-inc=F sets the restart interval increase factor for the sat solver (F=3.0 by default)\n\ --disable-variable-removal enable permanent removal of variables in arithmetic (UNSAFE! experts only)\n\ --disable-arithmetic-propagation turns on arithmetic propagation\n\ --enable-symmetry-breaker turns on UF symmetry breaker (Deharbe et al., CADE 2011) [on by default only for QF_UF]\n\ --disable-symmetry-breaker turns off UF symmetry breaker\n\ --disable-dio-solver turns off Linear Diophantine Equation solver (Griggio, JSAT 2012)\n\ + --threads=N sets the number of solver threads\n\ + --threadN=string configures thread N (0..#threads-1)\n\ + --filter-lemma-length=N don't share lemmas strictly longer than N\n\ "; + #warning "Change CL options as --disable-variable-removal cannot do anything currently." static const string languageDescription = "\ @@ -322,8 +344,11 @@ enum OptionValue { REPLAY, REPLAY_LOG, PIVOT_RULE, + PRINT_WINNER, RANDOM_FREQUENCY, RANDOM_SEED, + SAT_RESTART_FIRST, + SAT_RESTART_INC, ARITHMETIC_VARIABLE_REMOVAL, ARITHMETIC_PROPAGATION, ARITHMETIC_PIVOT_THRESHOLD, @@ -331,6 +356,9 @@ enum OptionValue { ARITHMETIC_DIO_SOLVER, ENABLE_SYMMETRY_BREAKER, DISABLE_SYMMETRY_BREAKER, + PARALLEL_THREADS, + PARALLEL_SEPARATE_OUTPUT, + PORTFOLIO_FILTER_LENGTH, TIME_LIMIT, TIME_LIMIT_PER, RESOURCE_LIMIT, @@ -409,11 +437,17 @@ static struct option cmdlineOptions[] = { { "prop-row-length" , required_argument, NULL, ARITHMETIC_PROP_MAX_LENGTH }, { "random-freq" , required_argument, NULL, RANDOM_FREQUENCY }, { "random-seed" , required_argument, NULL, RANDOM_SEED }, + { "restart-int-base", required_argument, NULL, SAT_RESTART_FIRST }, + { "restart-int-inc", required_argument, NULL, SAT_RESTART_INC }, + { "print-winner", no_argument , NULL, PRINT_WINNER }, { "disable-variable-removal", no_argument, NULL, ARITHMETIC_VARIABLE_REMOVAL }, { "disable-arithmetic-propagation", no_argument, NULL, ARITHMETIC_PROPAGATION }, { "disable-dio-solver", no_argument, NULL, ARITHMETIC_DIO_SOLVER }, { "enable-symmetry-breaker", no_argument, NULL, ENABLE_SYMMETRY_BREAKER }, { "disable-symmetry-breaker", no_argument, NULL, DISABLE_SYMMETRY_BREAKER }, + { "threads", required_argument, NULL, PARALLEL_THREADS }, + { "separate-output", no_argument, NULL, PARALLEL_SEPARATE_OUTPUT }, + { "filter-lemma-length", required_argument, NULL, PORTFOLIO_FILTER_LENGTH }, { "tlimit" , required_argument, NULL, TIME_LIMIT }, { "tlimit-per" , required_argument, NULL, TIME_LIMIT_PER }, { "rlimit" , required_argument, NULL, RESOURCE_LIMIT }, @@ -428,6 +462,13 @@ throw(OptionException) { const char *progName = argv[0]; int c; + // Reset getopt(), in the case of multiple calls. + // This can be = 1 in newer GNU getopt, but older (< 2007) require = 0. + optind = 0; +#if HAVE_DECL_OPTRESET + optreset = 1; // on BSD getopt() (e.g. Mac OS), might also need this +#endif /* HAVE_DECL_OPTRESET */ + // find the base name of the program const char *x = strrchr(progName, '/'); if(x != NULL) { @@ -595,6 +636,10 @@ throw(OptionException) { memoryMap = true; break; + case PRINT_WINNER: + printWinner = true; + break; + case STRICT_PARSING: strictParsing = true; break; @@ -807,6 +852,26 @@ throw(OptionException) { optarg + "' is not between 0.0 and 1.0."); } break; + + case SAT_RESTART_FIRST: + { + int i = atoi(optarg); + if(i < 1) { + throw OptionException("--restart-int-base requires a number bigger than 1"); + } + satRestartFirst = i; + break; + } + + case SAT_RESTART_INC: + { + int i = atoi(optarg); + if(i < 1) { + throw OptionException("--restart-int-inc requires a number bigger than 1.0"); + } + satRestartInc = i; + } + break; case PIVOT_RULE: if(!strcmp(optarg, "min")) { @@ -905,11 +970,40 @@ throw(OptionException) { printf("tls : %s\n", Configuration::isBuiltWithTlsSupport() ? "yes" : "no"); exit(0); + case PARALLEL_THREADS: + threads = atoi(optarg); + break; + + case PARALLEL_SEPARATE_OUTPUT: + separateOutput = true; + break; + + case PORTFOLIO_FILTER_LENGTH: + sharingFilterByLength = atoi(optarg); + break; + case ':': throw OptionException(string("option `") + argv[optind - 1] + "' missing its required argument"); case '?': default: + if(optopt == 0 && + !strncmp(argv[optind - 1], "--thread", 8) && + strlen(argv[optind - 1]) > 8 && + isdigit(argv[optind - 1][8])) { + int tnum = atoi(argv[optind - 1] + 8); + threadArgv.resize(tnum + 1); + if(threadArgv[tnum] != "") { + threadArgv[tnum] += " "; + } + const char* p = strchr(argv[optind - 1] + 9, '='); + if(p == NULL) { // e.g., we have --thread0 "foo" + threadArgv[tnum] += argv[optind++]; + } else { // e.g., we have --thread0="foo" + threadArgv[tnum] += p + 1; + } + break; + } throw OptionException(string("can't understand option `") + argv[optind - 1] + "'"); } } diff --git a/src/util/options.h b/src/util/options.h index d04947b02..6b8054a13 100644 --- a/src/util/options.h +++ b/src/util/options.h @@ -27,8 +27,12 @@ #include "util/exception.h" #include "util/language.h" +#include "util/lemma_output_channel.h" +#include "util/lemma_input_channel.h" #include "util/tls.h" +#include + namespace CVC4 { class ExprStream; @@ -104,6 +108,9 @@ struct CVC4_PUBLIC Options { /** Should we expand function definitions lazily? */ bool lazyDefinitionExpansion; + /** Parallel Only: Whether the winner is printed at the end or not. */ + bool printWinner; + /** Enumeration of simplification modes (when to simplify). */ typedef enum { /** Simplify the assertions as they come in */ @@ -187,6 +194,18 @@ struct CVC4_PUBLIC Options { **/ double satRandomSeed; + /** Variable activity decay factor for Minisat */ + double satVarDecay; + + /** Clause activity decay factor for Minisat */ + double satClauseDecay; + + /** Base restart interval for Minisat */ + int satRestartFirst; + + /** Restart interval increase factor for Minisat */ + double satRestartInc; + /** The pivot rule for arithmetic */ typedef enum { MINIMUM, BREAK_TIES, MAXIMUM } ArithPivotRule; ArithPivotRule pivotRule; @@ -220,6 +239,28 @@ struct CVC4_PUBLIC Options { */ bool dioSolver; + /** The output channel to receive notfication events for new lemmas */ + LemmaOutputChannel* lemmaOutputChannel; + LemmaInputChannel* lemmaInputChannel; + + /** Total number of threads */ + int threads; + + /** Thread configuration (a string to be passed to parseOptions) */ + std::vector threadArgv; + + /** Thread ID, for internal use in case of multi-threaded run */ + int thread_id; + + /** + * In multi-threaded setting print output of each thread at the + * end of run, separated by a divider ("----"). + **/ + bool separateOutput; + + /** Filter depending on length of lemma */ + int sharingFilterByLength; + Options(); /** diff --git a/src/util/stats.cpp b/src/util/stats.cpp index 474d8fa7a..709f80b04 100644 --- a/src/util/stats.cpp +++ b/src/util/stats.cpp @@ -31,6 +31,7 @@ using namespace CVC4; std::string Stat::s_delim(","); +std::string StatisticsRegistry::s_regDelim("::"); StatisticsRegistry* StatisticsRegistry::current() { return NodeManager::currentNM()->getStatisticsRegistry(); @@ -45,6 +46,14 @@ void StatisticsRegistry::registerStat(Stat* s) throw(AssertionException) { #endif /* CVC4_STATISTICS_ON */ }/* StatisticsRegistry::registerStat() */ +void StatisticsRegistry::registerStat_(Stat* s) throw(AssertionException) +{ +#ifdef CVC4_STATISTICS_ON + AlwaysAssert(d_registeredStats.find(s) == d_registeredStats.end()); + d_registeredStats.insert(s); +#endif /* CVC4_STATISTICS_ON */ +}/* StatisticsRegistry::registerStat_() */ + void StatisticsRegistry::unregisterStat(Stat* s) throw(AssertionException) { #ifdef CVC4_STATISTICS_ON StatSet& registeredStats = NodeManager::currentNM()->getStatisticsRegistry()->d_registeredStats; @@ -54,17 +63,33 @@ void StatisticsRegistry::unregisterStat(Stat* s) throw(AssertionException) { #endif /* CVC4_STATISTICS_ON */ }/* StatisticsRegistry::unregisterStat() */ -void StatisticsRegistry::flushStatistics(std::ostream& out) { +void StatisticsRegistry::unregisterStat_(Stat* s) throw(AssertionException) { +#ifdef CVC4_STATISTICS_ON + AlwaysAssert(d_registeredStats.find(s) != d_registeredStats.end()); + d_registeredStats.erase(s); +#endif /* CVC4_STATISTICS_ON */ +}/* StatisticsRegistry::unregisterStat_() */ + +void StatisticsRegistry::flushInformation(std::ostream& out) const { #ifdef CVC4_STATISTICS_ON for(StatSet::iterator i = d_registeredStats.begin(); i != d_registeredStats.end(); ++i) { Stat* s = *i; + if(d_name != "") { + out << d_name << s_regDelim; + } s->flushStat(out); out << std::endl; } #endif /* CVC4_STATISTICS_ON */ -}/* StatisticsRegistry::flushStatistics() */ +}/* StatisticsRegistry::flushInformation() */ + +void StatisticsRegistry::flushStat(std::ostream &out) const {; +#ifdef CVC4_STATISTICS_ON + flushInformation(out); +#endif /* CVC4_STATISTICS_ON */ +} StatisticsRegistry::const_iterator StatisticsRegistry::begin() { return NodeManager::currentNM()->getStatisticsRegistry()->d_registeredStats.begin(); @@ -93,16 +118,9 @@ void TimerStat::stop() { }/* TimerStat::stop() */ RegisterStatistic::RegisterStatistic(ExprManager& em, Stat* stat) : - d_em(&em), d_stat(stat) { - ExprManagerScope ems(*d_em); - StatisticsRegistry::registerStat(d_stat); -}/* RegisterStatistic::RegisterStatistic(ExprManager&, Stat*) */ - -RegisterStatistic::~RegisterStatistic() { - if(d_em != NULL) { - ExprManagerScope ems(*d_em); - StatisticsRegistry::unregisterStat(d_stat); - } else { - StatisticsRegistry::unregisterStat(d_stat); - } -}/* RegisterStatistic::~RegisterStatistic() */ + d_reg(NULL), + d_stat(stat) { + ExprManagerScope ems(em); + d_reg = StatisticsRegistry::current(); + d_reg->registerStat_(d_stat); +} diff --git a/src/util/stats.h b/src/util/stats.h index 719bbaab6..63e732305 100644 --- a/src/util/stats.h +++ b/src/util/stats.h @@ -2,7 +2,7 @@ /*! \file stats.h ** \verbatim ** Original author: taking - ** Major contributors: mdeters + ** Major contributors: mdeters, kshitij ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) @@ -46,85 +46,33 @@ class ExprManager; class CVC4_PUBLIC Stat; -/** - * The main statistics registry. This registry maintains the list of - * currently active statistics and is able to "flush" them all. - */ -class CVC4_PUBLIC StatisticsRegistry { -private: - /** A helper class for comparing two statistics */ - struct StatCmp { - inline bool operator()(const Stat* s1, const Stat* s2) const; - };/* class StatisticsRegistry::StatCmp */ - - /** A type for a set of statistics */ - typedef std::set< Stat*, StatCmp > StatSet; - - /** The set of currently active statistics */ - StatSet d_registeredStats; - - /** Private copy constructor undefined (no copy permitted). */ - StatisticsRegistry(const StatisticsRegistry&) CVC4_UNDEFINED; - -public: - - /** Construct a statistics registry */ - StatisticsRegistry() { } - - /** An iterator type over a set of statistics */ - typedef StatSet::const_iterator const_iterator; - - /** Get a pointer to the current statistics registry */ - static StatisticsRegistry* current(); - - /** Flush all statistics to the given output stream. */ - void flushStatistics(std::ostream& out); - - /** Register a new statistic, making it active. */ - static void registerStat(Stat* s) throw(AssertionException); - - /** Unregister an active statistic, making it inactive. */ - static void unregisterStat(Stat* s) throw(AssertionException); - - /** - * Get an iterator to the beginning of the range of the set of active - * (registered) statistics. - */ - static const_iterator begin(); - - /** - * Get an iterator to the end of the range of the set of active - * (registered) statistics. - */ - static const_iterator end(); - -};/* class StatisticsRegistry */ - - /** * The base class for all statistics. * - * This base class keeps the name of the statistic and declares two (pure) - * virtual functionss flushInformation() and getValue(). Derived classes - * must implement these functions and pass their name to the base class - * constructor. + * This base class keeps the name of the statistic and declares the (pure) + * virtual function flushInformation(). Derived classes must implement + * this function and pass their name to the base class constructor. * * This class also (statically) maintains the delimiter used to separate * the name and the value when statistics are output. */ class CVC4_PUBLIC Stat { private: - /** The name of this statistic */ - std::string d_name; - /** * The delimiter between name and value to use when outputting a * statistic. */ static std::string s_delim; +protected: + /** The name of this statistic */ + std::string d_name; + public: + /** Nullary constructor, does nothing */ + Stat() { } + /** * Construct a statistic with the given name. Debug builds of CVC4 * will throw an assertion exception if the given name contains the @@ -149,8 +97,10 @@ public: /** * Flush the name,value pair of this statistic to an output stream. * Uses the statistic delimiter string between name and value. + * + * May be redefined by a child class */ - void flushStat(std::ostream& out) const { + virtual void flushStat(std::ostream& out) const { if(__CVC4_USE_STATISTICS) { out << d_name << s_delim; flushInformation(out); @@ -163,21 +113,18 @@ public: } /** Get the value of this statistic as a string. */ - virtual std::string getValue() const = 0; + std::string getValue() const { + std::stringstream ss; + flushInformation(ss); + return ss.str(); + } };/* class Stat */ -inline bool StatisticsRegistry::StatCmp::operator()(const Stat* s1, - const Stat* s2) const { - return s1->getName() < s2->getName(); -} - /** * A class to represent a "read-only" data statistic of type T. Adds to * the Stat base class the pure virtual function getData(), which returns - * type T, along with an implementation of getValue(), which converts the - * type T to a string using an existing stream insertion operator defined - * on T, and flushInformation(), which outputs the statistic value to an + * type T, and flushInformation(), which outputs the statistic value to an * output stream (using the same existing stream insertion operator). * * Template class T must have stream insertion operation defined: @@ -204,13 +151,6 @@ public: } } - /** Get the value of the statistic as a string. */ - std::string getValue() const { - std::stringstream ss; - ss << getData(); - return ss.str(); - } - };/* class ReadOnlyDataStat */ @@ -480,20 +420,20 @@ private: * have seen so far. */ uint32_t d_count; + double d_sum; public: /** Construct an average statistic with the given name. */ AverageStat(const std::string& name) : - BackedStat(name, 0.0), d_count(0) { + BackedStat(name, 0.0), d_count(0), d_sum(0.0) { } /** Add an entry to the running-average calculation. */ void addEntry(double e) { if(__CVC4_USE_STATISTICS) { - double oldSum = d_count * getData(); ++d_count; - double newSum = oldSum + e; - setData(newSum / d_count); + d_sum += e; + setData(d_sum / d_count); } } @@ -535,13 +475,102 @@ public: return (*this); } - std::string getValue() const { - std::stringstream ss; - flushInformation(ss); - return ss.str(); +};/* class ListStat */ + +/****************************************************************************/ +/* Statistics Registry */ +/****************************************************************************/ + +/** + * The main statistics registry. This registry maintains the list of + * currently active statistics and is able to "flush" them all. + */ +class CVC4_PUBLIC StatisticsRegistry : public Stat { +private: + /** A helper class for comparing two statistics */ + struct StatCmp { + inline bool operator()(const Stat* s1, const Stat* s2) const; + };/* class StatisticsRegistry::StatCmp */ + + /** A type for a set of statistics */ + typedef std::set< Stat*, StatCmp > StatSet; + + /** The set of currently active statistics */ + StatSet d_registeredStats; + + /** Private copy constructor undefined (no copy permitted). */ + StatisticsRegistry(const StatisticsRegistry&) CVC4_UNDEFINED; + + static std::string s_regDelim; +public: + + /** Construct an nameless statistics registry */ + StatisticsRegistry() {} + + /** Construct a statistics registry */ + StatisticsRegistry(const std::string& name) throw(CVC4::AssertionException) : + Stat(name) { + if(__CVC4_USE_STATISTICS) { + AlwaysAssert(d_name.find(s_regDelim) == std::string::npos); + } } -};/* class ListStat */ + /** + * Set the name of this statistic registry, used as prefix during + * output. + * + * TODO: Get rid of this function once we have ability to set the + * name of StatisticsRegistry at creation time. + */ + void setName(const std::string& name) { + d_name = name; + } + + /** An iterator type over a set of statistics */ + typedef StatSet::const_iterator const_iterator; + + /** Get a pointer to the current statistics registry */ + static StatisticsRegistry* current(); + + /** Flush all statistics to the given output stream. */ + void flushInformation(std::ostream& out) const; + + /** Obsolete flushStatistics -- use flushInformation */ + //void flushStatistics(std::ostream& out) const; + + /** Overridden to avoid the name being printed */ + void flushStat(std::ostream &out) const; + + /** Register a new statistic, making it active. */ + static void registerStat(Stat* s) throw(AssertionException); + + /** Register a new statistic */ + void registerStat_(Stat* s) throw(AssertionException); + + /** Unregister an active statistic, making it inactive. */ + static void unregisterStat(Stat* s) throw(AssertionException); + + /** Unregister a new statistic */ + void unregisterStat_(Stat* s) throw(AssertionException); + + /** + * Get an iterator to the beginning of the range of the set of active + * (registered) statistics. + */ + static const_iterator begin(); + + /** + * Get an iterator to the end of the range of the set of active + * (registered) statistics. + */ + static const_iterator end(); + +};/* class StatisticsRegistry */ + +inline bool StatisticsRegistry::StatCmp::operator()(const Stat* s1, + const Stat* s2) const { + return s1->getName() < s2->getName(); +} /****************************************************************************/ /* Some utility functions for timespec */ @@ -753,19 +782,30 @@ public: * registration and unregistration. */ class CVC4_PUBLIC RegisterStatistic { - ExprManager* d_em; + StatisticsRegistry* d_reg; Stat* d_stat; public: - RegisterStatistic(Stat* stat) : d_stat(stat) { - Assert(StatisticsRegistry::current() != NULL, - "You need to specify an expression manager " - "on which to set the statistic"); + RegisterStatistic(Stat* stat) : + d_reg(StatisticsRegistry::current()), + d_stat(stat) { + Assert(d_reg != NULL, "There is no current statistics registry!"); StatisticsRegistry::registerStat(d_stat); } + RegisterStatistic(StatisticsRegistry* reg, Stat* stat) : + d_reg(reg), + d_stat(stat) { + Assert(d_reg != NULL, + "You need to specify a statistics registry" + "on which to set the statistic"); + d_reg->registerStat_(d_stat); + } + RegisterStatistic(ExprManager& em, Stat* stat); - ~RegisterStatistic(); + ~RegisterStatistic() { + d_reg->unregisterStat_(d_stat); + } };/* class RegisterStatistic */ diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am index 27ebac603..0bc78e6c4 100644 --- a/test/regress/regress0/Makefile.am +++ b/test/regress/regress0/Makefile.am @@ -1,9 +1,10 @@ SUBDIRS = . arith precedence uf uflra bv arrays datatypes lemmas push-pop preprocess +BINARY = cvc4 if PROOF_REGRESSIONS -TESTS_ENVIRONMENT = LFSC="$(LFSC) $(LFSCARGS)" @srcdir@/../run_regression --proof @top_builddir@/src/main/cvc4 +TESTS_ENVIRONMENT = LFSC="$(LFSC) $(LFSCARGS)" @srcdir@/../run_regression --proof @top_builddir@/src/main/$(BINARY) else -TESTS_ENVIRONMENT = @srcdir@/../run_regression @top_builddir@/src/main/cvc4 +TESTS_ENVIRONMENT = @srcdir@/../run_regression @top_builddir@/src/main/$(BINARY) endif MAKEFLAGS = -k diff --git a/test/regress/regress0/arith/Makefile.am b/test/regress/regress0/arith/Makefile.am index fdd0ad4ed..d6b2b143a 100644 --- a/test/regress/regress0/arith/Makefile.am +++ b/test/regress/regress0/arith/Makefile.am @@ -1,9 +1,10 @@ SUBDIRS = . integers +BINARY = cvc4 if PROOF_REGRESSIONS -TESTS_ENVIRONMENT = LFSC="$(LFSC) $(LFSCARGS)" @srcdir@/../../run_regression --proof @top_builddir@/src/main/cvc4 +TESTS_ENVIRONMENT = LFSC="$(LFSC) $(LFSCARGS)" @srcdir@/../../run_regression --proof @top_builddir@/src/main/$(BINARY) else -TESTS_ENVIRONMENT = @srcdir@/../../run_regression @top_builddir@/src/main/cvc4 +TESTS_ENVIRONMENT = @srcdir@/../../run_regression @top_builddir@/src/main/$(BINARY) endif MAKEFLAGS = -k diff --git a/test/regress/regress0/bv/Makefile.am b/test/regress/regress0/bv/Makefile.am index 8d65ee3a9..1cdfec8fc 100644 --- a/test/regress/regress0/bv/Makefile.am +++ b/test/regress/regress0/bv/Makefile.am @@ -1,9 +1,10 @@ SUBDIRS = . core +BINARY = cvc4 if PROOF_REGRESSIONS -TESTS_ENVIRONMENT = LFSC="$(LFSC) $(LFSCARGS)" @srcdir@/../../run_regression --proof @top_builddir@/src/main/cvc4 +TESTS_ENVIRONMENT = LFSC="$(LFSC) $(LFSCARGS)" @srcdir@/../../run_regression --proof @top_builddir@/src/main/$(BINARY) else -TESTS_ENVIRONMENT = @srcdir@/../../run_regression @top_builddir@/src/main/cvc4 +TESTS_ENVIRONMENT = @srcdir@/../../run_regression @top_builddir@/src/main/$(BINARY) endif MAKEFLAGS = -k diff --git a/test/regress/regress0/bv/core/Makefile.am b/test/regress/regress0/bv/core/Makefile.am index fa0144da0..6a36f5188 100644 --- a/test/regress/regress0/bv/core/Makefile.am +++ b/test/regress/regress0/bv/core/Makefile.am @@ -1,7 +1,8 @@ +BINARY = cvc4 if PROOF_REGRESSIONS -TESTS_ENVIRONMENT = LFSC="$(LFSC) $(LFSCARGS)" @srcdir@/../../../run_regression --proof @top_builddir@/src/main/cvc4 +TESTS_ENVIRONMENT = LFSC="$(LFSC) $(LFSCARGS)" @srcdir@/../../../run_regression --proof @top_builddir@/src/main/$(BINARY) else -TESTS_ENVIRONMENT = @srcdir@/../../../run_regression @top_builddir@/src/main/cvc4 +TESTS_ENVIRONMENT = @srcdir@/../../../run_regression @top_builddir@/src/main/$(BINARY) endif # These are run for all build profiles. diff --git a/test/regress/regress0/lemmas/Makefile.am b/test/regress/regress0/lemmas/Makefile.am index 70375e1d7..94104ed49 100644 --- a/test/regress/regress0/lemmas/Makefile.am +++ b/test/regress/regress0/lemmas/Makefile.am @@ -1,9 +1,10 @@ SUBDIRS = . +BINARY = cvc4 if PROOF_REGRESSIONS -TESTS_ENVIRONMENT = LFSC="$(LFSC) $(LFSCARGS)" @srcdir@/../../run_regression --proof @top_builddir@/src/main/cvc4 +TESTS_ENVIRONMENT = LFSC="$(LFSC) $(LFSCARGS)" @srcdir@/../../run_regression --proof @top_builddir@/src/main/$(BINARY) else -TESTS_ENVIRONMENT = @srcdir@/../../run_regression @top_builddir@/src/main/cvc4 +TESTS_ENVIRONMENT = @srcdir@/../../run_regression @top_builddir@/src/main/$(BINARY) endif MAKEFLAGS = -k diff --git a/test/regress/regress0/precedence/Makefile.am b/test/regress/regress0/precedence/Makefile.am index 6d60bcb4f..719b196ca 100644 --- a/test/regress/regress0/precedence/Makefile.am +++ b/test/regress/regress0/precedence/Makefile.am @@ -1,7 +1,8 @@ +BINARY = cvc4 if PROOF_REGRESSIONS -TESTS_ENVIRONMENT = LFSC="$(LFSC) $(LFSCARGS)" @srcdir@/../../run_regression --proof @top_builddir@/src/main/cvc4 +TESTS_ENVIRONMENT = LFSC="$(LFSC) $(LFSCARGS)" @srcdir@/../../run_regression --proof @top_builddir@/src/main/$(BINARY) else -TESTS_ENVIRONMENT = @srcdir@/../../run_regression @top_builddir@/src/main/cvc4 +TESTS_ENVIRONMENT = @srcdir@/../../run_regression @top_builddir@/src/main/$(BINARY) endif # These are run for all build profiles. diff --git a/test/regress/regress0/push-pop/Makefile.am b/test/regress/regress0/push-pop/Makefile.am index 827dc04aa..aedf03470 100644 --- a/test/regress/regress0/push-pop/Makefile.am +++ b/test/regress/regress0/push-pop/Makefile.am @@ -1,9 +1,10 @@ SUBDIRS = . +BINARY = cvc4 if PROOF_REGRESSIONS -TESTS_ENVIRONMENT = LFSC="$(LFSC) $(LFSCARGS)" @srcdir@/../../run_regression --proof @top_builddir@/src/main/cvc4 +TESTS_ENVIRONMENT = LFSC="$(LFSC) $(LFSCARGS)" @srcdir@/../../run_regression --proof @top_builddir@/src/main/$(BINARY) else -TESTS_ENVIRONMENT = @srcdir@/../../run_regression @top_builddir@/src/main/cvc4 +TESTS_ENVIRONMENT = @srcdir@/../../run_regression @top_builddir@/src/main/$(BINARY) endif MAKEFLAGS = -k diff --git a/test/regress/regress0/uf/Makefile.am b/test/regress/regress0/uf/Makefile.am index 3a9749598..e7dae1080 100644 --- a/test/regress/regress0/uf/Makefile.am +++ b/test/regress/regress0/uf/Makefile.am @@ -1,7 +1,8 @@ +BINARY = cvc4 if PROOF_REGRESSIONS -TESTS_ENVIRONMENT = LFSC="$(LFSC) $(LFSCARGS)" @srcdir@/../../run_regression --proof @top_builddir@/src/main/cvc4 +TESTS_ENVIRONMENT = LFSC="$(LFSC) $(LFSCARGS)" @srcdir@/../../run_regression --proof @top_builddir@/src/main/$(BINARY) else -TESTS_ENVIRONMENT = @srcdir@/../../run_regression @top_builddir@/src/main/cvc4 +TESTS_ENVIRONMENT = @srcdir@/../../run_regression @top_builddir@/src/main/$(BINARY) endif # These are run for all build profiles. diff --git a/test/regress/regress0/uflra/Makefile.am b/test/regress/regress0/uflra/Makefile.am index bee9e8d76..f32e980ad 100644 --- a/test/regress/regress0/uflra/Makefile.am +++ b/test/regress/regress0/uflra/Makefile.am @@ -1,7 +1,8 @@ +BINARY = cvc4 if PROOF_REGRESSIONS -TESTS_ENVIRONMENT = LFSC="$(LFSC) $(LFSCARGS)" @srcdir@/../../run_regression --proof @top_builddir@/src/main/cvc4 +TESTS_ENVIRONMENT = LFSC="$(LFSC) $(LFSCARGS)" @srcdir@/../../run_regression --proof @top_builddir@/src/main/$(BINARY) else -TESTS_ENVIRONMENT = @srcdir@/../../run_regression @top_builddir@/src/main/cvc4 +TESTS_ENVIRONMENT = @srcdir@/../../run_regression @top_builddir@/src/main/$(BINARY) endif MAKEFLAGS = -k diff --git a/test/regress/regress1/Makefile.am b/test/regress/regress1/Makefile.am index c7087219a..2135cf55b 100644 --- a/test/regress/regress1/Makefile.am +++ b/test/regress/regress1/Makefile.am @@ -1,9 +1,10 @@ SUBDIRS = . arith +BINARY = cvc4 if PROOF_REGRESSIONS -TESTS_ENVIRONMENT = LFSC="$(LFSC) $(LFSCARGS)" @srcdir@/../run_regression --proof @top_builddir@/src/main/cvc4 +TESTS_ENVIRONMENT = LFSC="$(LFSC) $(LFSCARGS)" @srcdir@/../run_regression --proof @top_builddir@/src/main/$(BINARY) else -TESTS_ENVIRONMENT = @srcdir@/../run_regression @top_builddir@/src/main/cvc4 +TESTS_ENVIRONMENT = @srcdir@/../run_regression @top_builddir@/src/main/$(BINARY) endif MAKEFLAGS = -k diff --git a/test/regress/regress1/arith/Makefile.am b/test/regress/regress1/arith/Makefile.am index 046efe65f..3eb33d311 100644 --- a/test/regress/regress1/arith/Makefile.am +++ b/test/regress/regress1/arith/Makefile.am @@ -1,7 +1,8 @@ +BINARY = cvc4 if PROOF_REGRESSIONS -TESTS_ENVIRONMENT = LFSC="$(LFSC) $(LFSCARGS)" @srcdir@/../../run_regression --proof @top_builddir@/src/main/cvc4 +TESTS_ENVIRONMENT = LFSC="$(LFSC) $(LFSCARGS)" @srcdir@/../../run_regression --proof @top_builddir@/src/main/$(BINARY) else -TESTS_ENVIRONMENT = @srcdir@/../../run_regression @top_builddir@/src/main/cvc4 +TESTS_ENVIRONMENT = @srcdir@/../../run_regression @top_builddir@/src/main/$(BINARY) endif # These are run for all build profiles. diff --git a/test/regress/regress2/Makefile.am b/test/regress/regress2/Makefile.am index 8a17bf6b2..d084ad47a 100644 --- a/test/regress/regress2/Makefile.am +++ b/test/regress/regress2/Makefile.am @@ -1,9 +1,10 @@ SUBDIRS = . +BINARY = cvc4 if PROOF_REGRESSIONS -TESTS_ENVIRONMENT = LFSC="$(LFSC) $(LFSCARGS)" @srcdir@/../run_regression --proof @top_builddir@/src/main/cvc4 +TESTS_ENVIRONMENT = LFSC="$(LFSC) $(LFSCARGS)" @srcdir@/../run_regression --proof @top_builddir@/src/main/$(BINARY) else -TESTS_ENVIRONMENT = @srcdir@/../run_regression @top_builddir@/src/main/cvc4 +TESTS_ENVIRONMENT = @srcdir@/../run_regression @top_builddir@/src/main/$(BINARY) endif MAKEFLAGS = -k diff --git a/test/regress/regress3/Makefile.am b/test/regress/regress3/Makefile.am index 08a675273..201e332d1 100644 --- a/test/regress/regress3/Makefile.am +++ b/test/regress/regress3/Makefile.am @@ -1,9 +1,10 @@ SUBDIRS = . +BINARY = cvc4 if PROOF_REGRESSIONS -TESTS_ENVIRONMENT = LFSC="$(LFSC) $(LFSCARGS)" @srcdir@/../run_regression --proof @top_builddir@/src/main/cvc4 +TESTS_ENVIRONMENT = LFSC="$(LFSC) $(LFSCARGS)" @srcdir@/../run_regression --proof @top_builddir@/src/main/$(BINARY) else -TESTS_ENVIRONMENT = @srcdir@/../run_regression @top_builddir@/src/main/cvc4 +TESTS_ENVIRONMENT = @srcdir@/../run_regression @top_builddir@/src/main/$(BINARY) endif MAKEFLAGS = -k -- 2.30.2