/lcov/
.cvc4_config
config.reconfig
+*.swp
+/debug/
The core authors and designers of CVC4 are:
+ Kshitij Bansal <kshitij@cs.nyu.edu>, New York University
Clark Barrett <barrett@cs.nyu.edu>, New York University
François Bobot <bobot@lri.fr>, Paris-Sud University
Christopher Conway <cconway@cs.nyu.edu>, New York University
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
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 <tsuna@lrde.epita.fr>
+
+ 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 <http://www.gnu.org/licenses/>.
+
+ 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.
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@
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
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)"
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
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)
--- /dev/null
+# boost.m4: Locate Boost headers and libraries for autoconf-based projects.
+# Copyright (C) 2007, 2008, 2009, 2010 Benoit Sigoure <tsuna@lrde.epita.fr>
+#
+# 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 <http://www.gnu.org/licenses/>.
+
+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 <boost/version.hpp>
+#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 <prefix>/include/boost-<version>. 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/version.hpp>
+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_<HEADER-NAME> 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<void ()> 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.h>],
+ [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:
#AC_TYPE_UINT64_T
#AC_TYPE_SIZE_T
+AC_CHECK_DECLS([optreset], [], [], [#include <getopt.h>])
+
+# 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],
# 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])
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])
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)'
Compat lib : $CVC4_BUILD_LIBCOMPAT
Bindings : ${CVC4_LANGUAGE_BINDINGS:-none}
+Multithreaded: $support_multithreaded
+TLS support : $CVC4_TLS_explanation
+
MP library : $mplibrary
CPPFLAGS : $CPPFLAGS
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
d_commandStatus = CommandSuccess::instance();
}
+Command* EmptyCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
+ return new EmptyCommand(d_name);
+}
+
/* class AssertCommand */
AssertCommand::AssertCommand(const BoolExpr& e) throw() :
}
}
+Command* AssertCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
+ return new AssertCommand(d_expr.exportTo(exprManager, variableMap));
+}
+
/* class PushCommand */
void PushCommand::invoke(SmtEngine* smtEngine) throw() {
}
}
+Command* PushCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
+ return new PushCommand;
+}
+
/* class PopCommand */
void PopCommand::invoke(SmtEngine* smtEngine) throw() {
d_expr() {
}
+Command* PopCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
+ return new PopCommand();
+}
+
+/* class CheckSatCommand */
+
CheckSatCommand::CheckSatCommand(const BoolExpr& expr) throw() :
d_expr(expr) {
}
}
}
+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() :
}
}
+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() {
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) {
d_commandStatus = CommandSuccess::instance();
}
+Command* CommentCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
+ return new CommentCommand(d_comment);
+}
+
/* class CommandSequence */
CommandSequence::CommandSequence() 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();
}
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() :
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,
d_commandStatus = CommandSuccess::instance();
}
+Command* DefineTypeCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
+ vector<Type> 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,
d_commandStatus = CommandSuccess::instance();
}
+Command* DefineFunctionCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
+ Expr func = d_func.exportTo(exprManager, variableMap);
+ vector<Expr> 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,
d_commandStatus = CommandSuccess::instance();
}
+Command* DefineNamedFunctionCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
+ Expr func = d_func.exportTo(exprManager, variableMap);
+ vector<Expr> 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() :
}
}
+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() :
}
}
+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() {
}
}
+Command* GetAssignmentCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
+ GetAssignmentCommand* c = new GetAssignmentCommand;
+ c->d_result = d_result;
+ return c;
+}
+
/* class GetProofCommand */
GetProofCommand::GetProofCommand() throw() {
}
}
+Command* GetProofCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
+ GetProofCommand* c = new GetProofCommand;
+ c->d_result = d_result;
+ return c;
+}
+
/* class GetAssertionsCommand */
GetAssertionsCommand::GetAssertionsCommand() 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() :
}
}
+Command* SetBenchmarkStatusCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
+ SetBenchmarkStatusCommand* c = new SetBenchmarkStatusCommand(d_status);
+ return c;
+}
+
/* class SetBenchmarkLogicCommand */
SetBenchmarkLogicCommand::SetBenchmarkLogicCommand(std::string logic) 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() :
}
}
+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() :
}
}
+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() :
}
}
+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() :
}
}
+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() :
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() {
#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"
};/* 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
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 */
/**
~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 {
~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 {
~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 {
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 {
const std::vector<Type>& 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 {
const std::vector<Expr>& getFormals() const throw();
Expr getFormula() const throw();
void invoke(SmtEngine* smtEngine) throw();
+ Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
};/* class DefineFunctionCommand */
/**
DefineNamedFunctionCommand(const std::string& id, Expr func,
const std::vector<Expr>& formals, Expr formula) throw();
void invoke(SmtEngine* smtEngine) throw();
+ Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
};/* class DefineNamedFunctionCommand */
class CVC4_PUBLIC CheckSatCommand : public Command {
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 {
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
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 {
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 {
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 {
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 {
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 {
~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 {
~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 {
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 {
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 {
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 {
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 {
DatatypeDeclarationCommand(const std::vector<DatatypeType>& datatypes) throw();
const std::vector<DatatypeType>& getDatatypes() const throw();
void invoke(SmtEngine* smtEngine) throw();
+ Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
};/* class DatatypeDeclarationCommand */
class CVC4_PUBLIC QuitCommand : public Command {
QuitCommand() throw();
~QuitCommand() throw() {}
void invoke(SmtEngine* smtEngine) throw();
+ Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
};/* class QuitCommand */
class CVC4_PUBLIC CommentCommand : public Command {
~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 {
iterator begin() throw();
iterator end() throw();
+ Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
};/* class CommandSequence */
class CVC4_PUBLIC DeclarationSequence : public CommandSequence {
#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"
// 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) \
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<TypeConstant>());
+ } else if(n.getKind() == kind::BITVECTOR_TYPE) {
+ return to->mkBitVectorType(n.getConst<BitVectorSize>());
+ }
+ 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 */
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;
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);
#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 <vector>
#include <iterator>
#include <utility>
// 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;
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<Node> 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<Node>::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!");
${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 */
template <bool ref_count>
class NodeTemplate;
+class NodeManager;
+
class Expr;
class ExprManager;
class SmtEngine;
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 */
class CVC4_PUBLIC ExprSetDepth;
class CVC4_PUBLIC ExprPrintTypes;
class CVC4_PUBLIC ExprSetLanguage;
+
+ NodeTemplate<true> exportInternal(NodeTemplate<false> n, ExprManager* from, ExprManager* to, ExprManagerMapCollection& vmap);
}/* CVC4::expr namespace */
/**
*/
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.:
friend class ExprManager;
friend class NodeManager;
friend class TypeCheckingException;
+ friend class expr::pickle::Pickler;
+ friend class prop::SatSolver;
+ friend NodeTemplate<true> expr::exportInternal(NodeTemplate<false> n, ExprManager* from, ExprManager* to, ExprManagerMapCollection& vmap);
+
friend std::ostream& CVC4::operator<<(std::ostream& out, const Expr& e);
template <bool ref_count> friend class NodeTemplate;
${getConst_instantiations}
-#line 832 "${template}"
+#line 861 "${template}"
namespace expr {
getConst_implementations=
mkConst_instantiations=
mkConst_implementations=
+exportConstant_cases=
seen_theory=false
seen_theory_builtin=false
return d_node->getConst< $2 >();
}
"
+ exportConstant_cases="${exportConstant_cases}
+ case $1: return to->mkConst(n.getConst< $2 >());"
}
function check_theory_seen {
getConst_implementations \
mkConst_instantiations \
mkConst_implementations \
+ exportConstant_cases \
typechecker_includes \
typerules \
; do
class TypeNode;
class NodeManager;
+namespace expr {
+ namespace pickle {
+ class PicklerPrivate;
+ }/* CVC4::expr::pickle namespace */
+}/* CVC4::expr namespace */
+
template <bool ref_count>
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;
friend class NodeTemplate<true>;
friend class NodeTemplate<false>;
+ friend class TypeNode;
friend class NodeManager;
template <unsigned nchild_thresh>
// 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")) {
}
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,
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();
// 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";
}
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,
}
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,
d_optionsAllocated(new Options()),
d_options(d_optionsAllocated),
d_statisticsRegistry(new StatisticsRegistry()),
+ next_id(0),
d_attrManager(ctxt),
d_exprManager(exprManager),
d_nodeUnderDeletion(NULL),
d_optionsAllocated(NULL),
d_options(&options),
d_statisticsRegistry(new StatisticsRegistry()),
+ next_id(0),
d_attrManager(ctxt),
d_exprManager(exprManager),
d_nodeUnderDeletion(NULL),
NodeValuePool d_nodeValuePool;
+ size_t next_id;
+
expr::attr::AttributeManager d_attrManager;
/** The associated ExprManager */
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
+ * <code>AttrKind::value_type</code> if not.
+ */
+ template <class AttrKind>
+ 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 <code>true</code> iff <code>attr</code> is set for <code>n</code>.
+ */
+ template <class AttrKind>
+ 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.
+ * <code>value</code> will be set to the value of the attribute, if it is
+ * set for <code>nv</code>; otherwise, it will be set to the default value of
+ * the attribute.
+ * @returns <code>true</code> iff <code>attr</code> is set for <code>n</code>.
+ */
+ template <class AttrKind>
+ 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 <code>attr</code> for <code>n</code>
+ */
+ template <class AttrKind>
+ inline void setAttribute(TypeNode n,
+ const AttrKind& attr,
+ const typename AttrKind::value_type& value);
+
/** Get the (singleton) type for Booleans. */
inline TypeNode booleanType();
d_attrManager.setAttribute(n.d_nv, AttrKind(), value);
}
+template <class AttrKind>
+inline typename AttrKind::value_type
+NodeManager::getAttribute(TypeNode n, const AttrKind&) const {
+ return d_attrManager.getAttribute(n.d_nv, AttrKind());
+}
+
+template <class AttrKind>
+inline bool
+NodeManager::hasAttribute(TypeNode n, const AttrKind&) const {
+ return d_attrManager.hasAttribute(n.d_nv, AttrKind());
+}
+
+template <class AttrKind>
+inline bool
+NodeManager::getAttribute(TypeNode n, const AttrKind&,
+ typename AttrKind::value_type& ret) const {
+ return d_attrManager.getAttribute(n.d_nv, AttrKind(), ret);
+}
+
+template <class AttrKind>
+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() {
inline TypeNode NodeManager::mkSort(const std::string& name) {
TypeNode type = mkSort();
- type.setAttribute(expr::VarNameAttr(), name);
+ setAttribute(type, expr::VarNameAttr(), name);
return type;
}
nb << sortTag;
nb.append(children);
TypeNode type = nb.constructTypeNode();
- type.setAttribute(expr::VarNameAttr(), name);
+ setAttribute(type, expr::VarNameAttr(), name);
return type;
}
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;
}
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;
}
nv->d_nchildren = 0;
nv->d_kind = kind::metakind::ConstantMap<T>::kind;
- nv->d_id = expr::NodeValue::next_id++;// FIXME multithreading
+ nv->d_id = next_id++;// FIXME multithreading
nv->d_rc = 0;
//OwningTheory::mkConst(val);
namespace CVC4 {
namespace expr {
-size_t NodeValue::next_id = 1;
-
NodeValue NodeValue::s_null(0);
string NodeValue::toString() const {
void inc();
void dec();
- static size_t next_id;
-
/**
* Uninitializing constructor for NodeBuilder's use.
*/
--- /dev/null
+/********************* */
+/*! \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 <iostream>
+#include <sstream>
+#include <string>
+
+#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 */
--- /dev/null
+/********************* */
+/*! \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 <sstream>
+#include <deque>
+#include <stack>
+#include <exception>
+
+#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<Block> 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 */
--- /dev/null
+/********************* */
+/*! \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 <iostream>
+#include <sstream>
+#include <string>
+
+#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<Node> 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<uint64_t>(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<bool>());
+ break;
+ case kind::CONST_INTEGER:
+ case kind::CONST_RATIONAL: {
+ std::string asString;
+ if(k == kind::CONST_INTEGER) {
+ const Integer& i = n.getConst<Integer>();
+ asString = i.toString(16);
+ } else {
+ Assert(k == kind::CONST_RATIONAL);
+ const Rational& q = n.getConst<Rational>();
+ asString = q.toString(16);
+ }
+ toCaseString(k, asString);
+ break;
+ }
+ case kind::BITVECTOR_EXTRACT_OP: {
+ BitVectorExtract bve = n.getConst<BitVectorExtract>();
+ 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<BitVector>();
+ 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<NodeValue*>(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<bool>(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<Integer>(i);
+ } else {
+ Rational q(s, 16);
+ return d_nm->mkConst<Rational>(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<BitVectorExtract>(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 */
--- /dev/null
+/********************* */
+/*! \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 <exception>
+#include <stack>
+
+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 */
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;
class ExprManager;
class Expr;
class TypeNode;
+class ExprManagerMapCollection;
class SmtEngine;
*/
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.
*/
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:
*/
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
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
*
--- /dev/null
+/********************* */
+/*! \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<Expr, Expr, ExprHashFunction> d_variables;
+
+ /**
+ * A map Type -> Type, intended to be used for a mapping of types
+ * between two ExprManagers.
+ */
+ std::hash_map<Type, Type, TypeHashFunction> 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<uint64_t, uint64_t> VarMap;
+
+struct CVC4_PUBLIC ExprManagerMapCollection {
+ VariableTypeMap d_typeMap;
+ VarMap d_to;
+ VarMap d_from;
+};
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__VARIABLE_MAP_H */
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 \
else
cvc4_LINK = $(CXXLINK)
endif
+
--- /dev/null
+/********************* */
+/*! \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 <cstdlib>
+#include <cstring>
+#include <fstream>
+#include <iostream>
+#include <new>
+
+#include <stdio.h>
+#include <unistd.h>
+
+#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 ? "<stdin>" : 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<CommandSequence*>(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<SetBenchmarkLogicCommand*>(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;
+}
--- /dev/null
+#include <cstdio>
+#include <cstdlib>
+#include <iostream>
+#include <sys/time.h> // for gettimeofday()
+
+#include <queue>
+
+#include <boost/thread.hpp>
+#include <boost/thread/condition.hpp>
+#include <boost/exception_ptr.hpp>
+#include <boost/lexical_cast.hpp>
+
+#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<typename T>
+void sharingManager(int numThreads,
+ SharedChannel<T>* channelsOut[],
+ SharedChannel<T>* 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 <typename T>
+class EmptySharedChannel: public SharedChannel<T> {
+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<channelFormat>* d_sharedChannel;
+ expr::pickle::MapPickler d_pickler;
+
+public:
+ int cnt;
+ PortfolioLemmaOutputChannel(string tag,
+ SharedChannel<channelFormat> *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<channelFormat>* d_sharedChannel;
+ expr::pickle::MapPickler d_pickler;
+
+public:
+ PortfolioLemmaInputChannel(string tag,
+ SharedChannel<channelFormat>* 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 ? "<stdin>" : 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<Options> 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<stringstream*> ss_out(numThreads);
+ if(options.verbosity == 0 or options.separateOutput) {
+ for(int i = 0;i <numThreads; ++i) {
+ ss_out[i] = new stringstream;
+ threadOptions[i].out = ss_out[i];
+ }
+ }
+
+ /****************************** Driver Statistics *************************/
+
+ // Statistics init
+ pStatistics = &theStatisticsRegistry;
+
+ StatisticsRegistry driverStatisticsRegistry("driver");
+ theStatisticsRegistry.registerStat_((&driverStatisticsRegistry));
+
+ // Timer statistic
+ RegisterStatistic* statTotatTime =
+ new RegisterStatistic(&driverStatisticsRegistry, &s_totalTime);
+ RegisterStatistic* statBeforePortfolioTime =
+ new RegisterStatistic(&driverStatisticsRegistry, &s_beforePortfolioTime);
+
+ // Filename statistics
+ ReferenceStat< const char* > 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<uint64_t> 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<string>(threadOptions[i].thread_id);
+ smts[i]->getStatisticsRegistry()->setName(tag);
+ theStatisticsRegistry.registerStat_( (Stat*)smts[i]->getStatisticsRegistry() );
+ }
+
+ /************************* Lemma sharing init ************************/
+
+ /* Sharing channels */
+ SharedChannel<channelFormat> *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<numThreads; ++i){
+ if(Debug.isOn("channel-empty")) {
+ channelsOut[i] = new EmptySharedChannel<channelFormat>(sharingChannelSize);
+ channelsIn[i] = new EmptySharedChannel<channelFormat>(sharingChannelSize);
+ continue;
+ }
+ channelsOut[i] = new SynchronizedSharedChannel<channelFormat>(sharingChannelSize);
+ channelsIn[i] = new SynchronizedSharedChannel<channelFormat>(sharingChannelSize);
+ }
+
+ /* Lemma output channel */
+ for(int i = 0; i<numThreads; ++i) {
+ string tag = "thread #" + boost::lexical_cast<string>(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<Result()> 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<void()>
+ smFn = boost::bind(sharingManager<channelFormat>, numThreads, channelsOut, channelsIn, smts);
+
+ s_beforePortfolioTime.stop();
+ pair<int, Result> 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<PortfolioLemmaOutputChannel*>(options.lemmaOutputChannel)).cnt;
+ int th1_lemcnt = (*static_cast<PortfolioLemmaOutputChannel*>(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<CommandSequence*>(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<SetBenchmarkLogicCommand*>(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<typename T>
+void sharingManager(int numThreads,
+ SharedChannel<T> *channelsOut[], // out and in with respect
+ SharedChannel<T> *channelsIn[],
+ SmtEngine *smts[]) // to smt engines
+{
+ Trace("sharing") << "sharing: thread started " << std::endl;
+ vector <int> cnt(numThreads); // Debug("sharing")
+
+ vector< queue<T> > queues;
+ for(int i = 0; i < numThreads; ++i){
+ queues.push_back(queue<T>());
+ }
+
+ 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;
+}
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();
#include <cstring>
#include <fstream>
#include <iostream>
-#include <new>
#include <stdio.h>
#include <unistd.h>
-#include "cvc4autoconfig.h"
#include "main/main.h"
#include "main/interactive_shell.h"
#include "parser/parser.h"
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
* 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
#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&) {
#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(...) {
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 ? "<stdin>" : 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<CommandSequence*>(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<SetBenchmarkLogicCommand*>(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;
-}
#include "util/options.h"
#include "util/exception.h"
#include "util/stats.h"
+#include "util/tls.h"
#include "cvc4autoconfig.h"
#ifndef __CVC4__MAIN__MAIN_H
*/
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);
}/* 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 */
--- /dev/null
+/********************* */
+/*! \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 <boost/function.hpp>
+#include <boost/thread.hpp>
+#include <boost/bind.hpp>
+#include <boost/thread/condition.hpp>
+#include <boost/exception_ptr.hpp>
+
+#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<typename S>
+void runThread(int thread_id, function<S()> 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<typename T, typename S>
+std::pair<int, S> runPortfolio(int numThreads,
+ function<T()> driverFn,
+ function<S()> 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<S>, 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<int, S>(global_winner,threads_returnValue[global_winner]);
+}
+
+// instantiation
+template
+std::pair<int, Result>
+runPortfolio<void, Result>(int, boost::function<void()>, boost::function<Result()>*, bool);
+
+}/* CVC4 namespace */
--- /dev/null
+/********************* */
+/*! \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 <boost/function.hpp>
+#include <utility>
+
+#include "smt/smt_engine.h"
+#include "expr/command.h"
+#include "util/options.h"
+
+namespace CVC4 {
+
+template<typename T, typename S>
+std::pair<int, S> runPortfolio(int numThreads,
+ boost::function<T()> driverFn,
+ boost::function<S()> 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 */
/** 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();
}
/** 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();
}
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 {
} 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 */
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 {
}
#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 */
}
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 {
}
#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 */
"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 */
#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;
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);
return *this;
}
-} /* namespace parser */
-
-} /* namespace CVC4 */
+}/* CVC4::parser namespace */
+}/* CVC4 namespace */
std::string d_stringInput;
/** The stream input, if any. */
- std::istream *d_streamInput;
+ std::istream* d_streamInput;
/** The expression manager */
ExprManager* d_exprManager;
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) {
}
n.toString().c_str(),
n.getType().toString().c_str());
- bool negated = false;
+ bool negated CVC4_UNUSED = false;
SatLiteral lit;
if(n.getKind() == kind::NOT) {
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;
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;
* 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
private:
/**
- * Same as above, except that removable is rememebered.
+ * Same as above, except that removable is remembered.
*/
void convertAndAssert(TNode node, bool negated);
#include "prop/sat.h"
#include "context/context.h"
#include "theory/theory_engine.h"
+#include "theory/rewriter.h"
#include "expr/expr_stream.h"
namespace CVC4 {
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() {
/** 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<Node, NodeHashFunction> 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. */
void notifyRestart();
+ void notifyNewLemma(SatClause& lemma);
+
SatLiteral getNextReplayDecision();
void logDecision(SatLiteral lit);
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);
}
*/
StatisticsRegistry* getStatisticsRegistry() const;
+ Result getStatusOfLastCommand() const {
+ return d_status;
+ }
+
};/* class SmtEngine */
}/* CVC4 namespace */
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;
}
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;
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();
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();
}
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();
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();
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 ) {
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 ) {
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();
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();
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 ) {
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 ) {
return RewriteResponse(REWRITE_DONE, result);
}
-AllRewriteRules* TheoryBVRewriter::s_allRules = NULL;
+CVC4_THREADLOCAL(AllRewriteRules*) TheoryBVRewriter::s_allRules = NULL;
void TheoryBVRewriter::init() {
s_allRules = new AllRewriteRules;
class TheoryBVRewriter {
- static AllRewriteRules* s_allRules;
+ static CVC4_THREADLOCAL(AllRewriteRules*) s_allRules;
public:
class BitVectorConstantTypeRule {
public:
inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
- throw (TypeCheckingExceptionPrivate) {
+ throw (TypeCheckingExceptionPrivate, AssertionException) {
return nodeManager->mkBitVectorType(n.getConst<BitVector>().getSize());
}
};
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);
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();
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 ) {
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()) {
class BitVectorExtractTypeRule {
public:
inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
- throw (TypeCheckingExceptionPrivate) {
+ throw (TypeCheckingExceptionPrivate, AssertionException) {
BitVectorExtract extractInfo = n.getOperator().getConst<BitVectorExtract>();
// NOTE: We're throwing a type-checking exception here even
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();
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
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
<< 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<Node> additionalLemmas;
additionalLemmas.push_back(node);
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();
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() ) {
stats.cpp \
dynamic_array.h \
language.h \
+ lemma_output_channel.h \
+ channel.h \
+ channel.cpp \
language.cpp \
ntuple.h \
recursion_breaker.h \
--- /dev/null
+#include "channel.h"
+
--- /dev/null
+
+#ifndef __CVC4__CHANNEL_H
+#define __CVC4__CHANNEL_H
+
+#include <boost/circular_buffer.hpp>
+#include <boost/thread/mutex.hpp>
+#include <boost/thread/condition.hpp>
+#include <boost/thread/thread.hpp>
+#include <boost/call_traits.hpp>
+#include <boost/progress.hpp>
+#include <boost/bind.hpp>
+
+
+namespace CVC4 {
+
+template <typename T>
+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 <typename T>
+class SynchronizedSharedChannel: public SharedChannel<T> {
+public:
+ typedef boost::circular_buffer<T> container_type;
+ typedef typename container_type::size_type size_type;
+ typedef typename container_type::value_type value_type;
+ typedef typename boost::call_traits<value_type>::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<value_type>::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<value_type>::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 */
+
+
namespace __gnu_cxx {}
#include <ext/hash_map>
+
+namespace __gnu_cxx {
+
+#if __WORDSIZE == 32
+// on 32-bit, we need a specialization of hash for 64-bit values
+template <>
+struct hash<uint64_t> {
+ size_t operator()(uint64_t v) const {
+ return v;
+ }
+};/* struct hash<uint64_t> */
+#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 {
--- /dev/null
+#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 */
--- /dev/null
+/********************* */
+/*! \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 */
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),
memoryMap(false),
strictParsing(false),
lazyDefinitionExpansion(false),
+ printWinner(false),
simplificationMode(SIMPLIFICATION_MODE_BATCH),
doStaticLearning(true),
interactive(false),
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)
{
}
--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\
--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 = "\
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,
ARITHMETIC_DIO_SOLVER,
ENABLE_SYMMETRY_BREAKER,
DISABLE_SYMMETRY_BREAKER,
+ PARALLEL_THREADS,
+ PARALLEL_SEPARATE_OUTPUT,
+ PORTFOLIO_FILTER_LENGTH,
TIME_LIMIT,
TIME_LIMIT_PER,
RESOURCE_LIMIT,
{ "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 },
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) {
memoryMap = true;
break;
+ case PRINT_WINNER:
+ printWinner = true;
+ break;
+
case STRICT_PARSING:
strictParsing = true;
break;
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")) {
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] + "'");
}
}
#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 <vector>
+
namespace CVC4 {
class ExprStream;
/** 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 */
**/
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;
*/
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<std::string> 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();
/**
using namespace CVC4;
std::string Stat::s_delim(",");
+std::string StatisticsRegistry::s_regDelim("::");
StatisticsRegistry* StatisticsRegistry::current() {
return NodeManager::currentNM()->getStatisticsRegistry();
#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;
#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();
}/* 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);
+}
/*! \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)
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
/**
* 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);
}
/** 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:
}
}
- /** Get the value of the statistic as a string. */
- std::string getValue() const {
- std::stringstream ss;
- ss << getData();
- return ss.str();
- }
-
};/* class ReadOnlyDataStat<T> */
* 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<double>(name, 0.0), d_count(0) {
+ BackedStat<double>(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);
}
}
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 */
* 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 */
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
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
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
+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.
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
+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.
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
+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.
+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
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
+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.
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
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