diff options
95 files changed, 2386 insertions, 1290 deletions
@@ -4,16 +4,17 @@ All rights reserved. This is a prerelease version; distribution is restricted. -THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT OWNERS AND CONTRIBUTORS ''AS IS'' AND ANY -EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED -WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE -DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNERS OR CONTRIBUTORS BE LIABLE FOR ANY -DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES -(INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; -LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON -ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT -(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS -SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. +THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT OWNERS AND CONTRIBUTORS +''AS IS'' AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT +LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR +A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT +OWNERS OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, +SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT +LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, +DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY +THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT +(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE +OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. -- Morgan Deters <mdeters@cs.nyu.edu> Thu, 04 Mar 2010 20:46:40 -0500 @@ -81,3 +82,36 @@ See config/doxygen.am. Its copyright: Copyright (C) 2004 Oren Ben-Kiki This file is distributed under the same terms as the Automake macro files. +CVC4 incorporates code from ANTLR3, excluded from the above copyright. +See http://www.antlr.org/, and the files +src/parser/bounded_token_buffer.h and +src/parser/bounded_token_buffer.cpp. Their copyright: + + [The "BSD licence"] + Copyright (c) 2005-2009 Jim Idle, Temporal Wave LLC + http://www.temporal-wave.com + http://www.linkedin.com/in/jimidle + + All rights reserved. + + Redistribution and use in source and binary forms, with or without + modification, are permitted provided that the following conditions + are met: + 1. Redistributions of source code must retain the above copyright + notice, this list of conditions and the following disclaimer. + 2. Redistributions in binary form must reproduce the above copyright + notice, this list of conditions and the following disclaimer in the + documentation and/or other materials provided with the distribution. + 3. The name of the author may not be used to endorse or promote products + derived from this software without specific prior written permission. + + THIS SOFTWARE IS PROVIDED BY THE AUTHOR ``AS IS'' AND ANY EXPRESS OR + IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES + OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. + IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY DIRECT, INDIRECT, + INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT + NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, + DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY + THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT + (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF + THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. diff --git a/autogen.sh b/autogen.sh index 5bce9bab3..3f143a12c 100755 --- a/autogen.sh +++ b/autogen.sh @@ -79,15 +79,18 @@ # set to minimum acceptable version of autoconf if [ "x$AUTOCONF_VERSION" = "x" ] ; then - AUTOCONF_VERSION=2.52 +# AUTOCONF_VERSION=2.52 + AUTOCONF_VERSION=2.61 fi # set to minimum acceptable version of automake if [ "x$AUTOMAKE_VERSION" = "x" ] ; then - AUTOMAKE_VERSION=1.6.0 +# AUTOMAKE_VERSION=1.6.0 + AUTOMAKE_VERSION=1.11 fi # set to minimum acceptable version of libtool if [ "x$LIBTOOL_VERSION" = "x" ] ; then - LIBTOOL_VERSION=1.4.2 +# LIBTOOL_VERSION=1.4.2 + LIBTOOL_VERSION=2.2 fi diff --git a/config/antlr.m4 b/config/antlr.m4 index 842b9b51d..64b554378 100644 --- a/config/antlr.m4 +++ b/config/antlr.m4 @@ -1,11 +1,11 @@ ## -# Check for ANTLR's runantlr script. Will set ANTLR to the location of the -# runantlr script +# Check for ANTLR's antlr3 script. +# Will set ANTLR to the location of the script. ## AC_DEFUN([AC_PROG_ANTLR], [ AC_ARG_VAR([ANTLR],[location of the antlr3 script]) - # Check the existance of the runantlr script + # Check the existence of the runantlr script if test -z "$ANTLR"; then AC_CHECK_PROGS(ANTLR, [antlr3]) else @@ -25,13 +25,13 @@ AC_DEFUN([AC_PROG_ANTLR], [ ]) ## -# Check the existance of the ANTLR C++ runtime library and headers -# Will set ANTLR_CPPFLAGS and ANTLR_LIBS to the location of the ANTLR headers +# Check the existence of the ANTLR3 C runtime library and headers +# Will set ANTLR_INCLUDES and ANTLR_LIBS to the location of the ANTLR headers # and library respectively ## AC_DEFUN([AC_LIB_ANTLR],[ - # Get the location of the ANTLR c++ includes and libraries + # Get the location of the ANTLR3 C includes and libraries AC_ARG_WITH( [antlr-dir], AS_HELP_STRING( @@ -39,10 +39,10 @@ AC_DEFUN([AC_LIB_ANTLR],[ [path to ANTLR C headers and libraries] ), ANTLR_PREFIXES="$withval", - ANTLR_PREFIXES="/usr/local /usr /opt/local /opt" + ANTLR_PREFIXES="$ANTLR_HOME /usr/local /usr /opt/local /opt" ) - AC_MSG_CHECKING(for ANTLR C runtime library) + AC_MSG_CHECKING(for ANTLR3 C runtime library) # Use C and remember the variables we are changing AC_LANG_PUSH(C) @@ -72,7 +72,7 @@ AC_DEFUN([AC_LIB_ANTLR],[ ], [ AC_MSG_RESULT(no) - AC_MSG_ERROR([ANTLR C runtime not found, see <http://www.antlr.org/>]) + AC_MSG_ERROR([ANTLR3 C runtime not found, see <http://www.antlr.org/>]) ] ) done diff --git a/configure.ac b/configure.ac index ecaa1bf30..a80d1fee9 100644 --- a/configure.ac +++ b/configure.ac @@ -1,21 +1,26 @@ # -*- Autoconf -*- # Process this file with autoconf to produce a configure script. +m4_define(_CVC4_MAJOR, 0 ) dnl version (major) +m4_define(_CVC4_MINOR, 0 ) dnl version (minor) +m4_define(_CVC4_RELEASE, 0 ) dnl version (alpha) +m4_define(_CVC4_RELEASE_STRING, [prerelease]) dnl version string + dnl Preprocess CL args. Defined in config/cvc4.m4 CVC4_AC_INIT AC_PREREQ(2.61) -AC_INIT -AC_CONFIG_SRCDIR([src/include/cvc4_config.h]) +AC_INIT([cvc4], _CVC4_RELEASE_STRING) +AC_CONFIG_SRCDIR([src/include/cvc4_public.h]) AC_CONFIG_AUX_DIR([config]) AC_CONFIG_MACRO_DIR([config]) m4_ifdef([AM_SILENT_RULES],[AM_SILENT_RULES([yes])]) -CVC4_MAJOR=0 -CVC4_MINOR=0 -CVC4_RELEASE=0 -CVC4_RELEASE_STRING=prerelease +CVC4_MAJOR=_CVC4_MAJOR +CVC4_MINOR=_CVC4_MINOR +CVC4_RELEASE=_CVC4_RELEASE +CVC4_RELEASE_STRING=_CVC4_RELEASE_STRING # Libtool version numbers for libraries # Version numbers are in the form current:revision:age @@ -138,7 +143,7 @@ AC_MSG_RESULT($build_type) AC_MSG_CHECKING([what dir to configure]) if test "$CVC4_CONFIGURE_IN_BUILDS" = yes; then AC_MSG_RESULT([this one (in builds/)]) -elif test -e src/include/cvc4_config.h; then +elif test -e src/include/cvc4_public.h; then AC_MSG_RESULT([builds/$target/$build_type]) echo if test -z "$ac_srcdir"; then @@ -166,6 +171,7 @@ case "$with_build" in production) # highly optimized, no assertions, no tracing CVC4CPPFLAGS= CVC4CXXFLAGS= + CVC4CFLAGS= CVC4LDFLAGS= if test -z "${OPTLEVEL+set}" ; then OPTLEVEL=3 ; fi if test -z "${enable_optimized+set}" ; then enable_optimized=yes ; fi @@ -177,6 +183,7 @@ case "$with_build" in debug) # unoptimized, debug symbols, assertions, tracing CVC4CPPFLAGS=-DCVC4_DEBUG CVC4CXXFLAGS='-fno-inline' + CVC4CFLAGS='-fno-inline' CVC4LDFLAGS= if test -z "${enable_optimized+set}" ; then enable_optimized=no ; fi if test -z "${enable_debug_symbols+set}"; then enable_debug_symbols=yes ; fi @@ -187,6 +194,7 @@ case "$with_build" in default) # moderately optimized, assertions, tracing CVC4CPPFLAGS= CVC4CXXFLAGS= + CVC4CFLAGS= CVC4LDFLAGS= if test -z "${OPTLEVEL+set}" ; then OPTLEVEL=2 ; fi if test -z "${enable_optimized+set}" ; then enable_optimized=yes ; fi @@ -198,6 +206,7 @@ case "$with_build" in competition) # maximally optimized, no assertions, no tracing, muzzled CVC4CPPFLAGS= CVC4CXXFLAGS='-funroll-all-loops -fexpensive-optimizations -fno-enforce-eh-specs' + CVC4CFLAGS='-funroll-all-loops -fexpensive-optimizations -fno-enforce-eh-specs' CVC4LDFLAGS= if test -z "${OPTLEVEL+set}" ; then OPTLEVEL=9 ; fi if test -z "${enable_optimized+set}" ; then enable_optimized=yes ; fi @@ -239,8 +248,10 @@ AC_MSG_RESULT([$enable_optimized]) if test "$enable_optimized" = yes; then CVC4CXXFLAGS="$CVC4CXXFLAGS -O$OPTLEVEL" + CVC4CFLAGS="$CVC4CFLAGS -O$OPTLEVEL" else CVC4CXXFLAGS="$CVC4CXXFLAGS -O0" + CVC4CFLAGS="$CVC4CFLAGS -O0" fi AC_MSG_CHECKING([whether to include debugging symbols in libcvc4]) @@ -257,6 +268,7 @@ AC_MSG_RESULT([$enable_debug_symbols]) if test "$enable_debug_symbols" = yes; then CVC4CXXFLAGS="$CVC4CXXFLAGS -ggdb3" + CVC4CFLAGS="$CVC4CFLAGS -ggdb3" fi AC_MSG_CHECKING([whether to include assertions in build]) @@ -325,6 +337,7 @@ dnl so that we can automatically disable shared and enable static? CVC4CPPFLAGS="$CVC4CPPFLAGS -DCVC4_COVERAGE" CVC4CXXFLAGS="$CVC4CXXFLAGS --coverage" + CVC4CFLAGS="$CVC4CFLAGS --coverage" CVC4LDFLAGS="$CVC4LDFLAGS --coverage" fi @@ -343,11 +356,12 @@ AC_MSG_RESULT([$enable_profiling]) if test "$enable_profiling" = yes; then CVC4CPPFLAGS="$CVC4CPPFLAGS -DCVC4_PROFILING" CVC4CXXFLAGS="$CVC4CXXFLAGS -pg" + CVC4CFLAGS="$CVC4CFLAGS -pg" CVC4LDFLAGS="$CVC4LDFLAGS -pg" fi -AM_INIT_AUTOMAKE(cvc4, $CVC4_RELEASE_STRING) -AC_CONFIG_HEADERS([config.h]) +AM_INIT_AUTOMAKE([1.11 no-define]) +AC_CONFIG_HEADERS([cvc4autoconfig.h]) # Initialize libtool's configuration options. _LT_SET_OPTION([LT_INIT],[win32-dll]) @@ -402,7 +416,7 @@ fi AM_CONDITIONAL([HAVE_CXXTESTGEN], [test -n "$CXXTESTGEN"]) -AC_ARG_VAR(TEST_CPPFLAGS, [CXXFLAGS to use when testing (default=$CPPFLAGS)]) +AC_ARG_VAR(TEST_CPPFLAGS, [CPPFLAGS to use when testing (default=$CPPFLAGS)]) AC_ARG_VAR(TEST_CXXFLAGS, [CXXFLAGS to use when testing (default=$CXXFLAGS)]) AC_ARG_VAR(TEST_LDFLAGS, [LDFLAGS to use when testing (default=$LDFLAGS)]) @@ -463,6 +477,7 @@ AC_DEFINE_UNQUOTED(CVC4_RELEASE_STRING, ["${CVC4_RELEASE_STRING}"], [Full releas CPPFLAGS="${CPPFLAGS:+$CPPFLAGS }$CVC4CPPFLAGS" CXXFLAGS="${CXXFLAGS:+$CXXFLAGS }$CVC4CXXFLAGS -Wno-deprecated" +CFLAGS="${CFLAGS:+$CFLAGS }$CVC4CFLAGS -Wno-deprecated" LDFLAGS="${LDFLAGS:+$LDFLAGS }$CVC4LDFLAGS" # mk_include @@ -540,6 +555,7 @@ static binary: $enable_static_binary CPPFLAGS : $CPPFLAGS CXXFLAGS : $CXXFLAGS +CFLAGS : $CFLAGS LDFLAGS : $LDFLAGS libcvc4 version : $CVC4_LIBRARY_VERSION diff --git a/contrib/update-copyright.pl b/contrib/update-copyright.pl index 79e5986de..8c73d514c 100755 --- a/contrib/update-copyright.pl +++ b/contrib/update-copyright.pl @@ -28,6 +28,7 @@ # the license.) my $excluded_directories = '^(minisat|CVS|generated)$'; +my $excluded_paths = '^(src/parser/bounded_token_buffer\.(h|cpp))$'; # Years of copyright for the template. E.g., the string # "1985, 1987, 1992, 1997, 2008" or "2006-2009" or whatever. @@ -101,6 +102,7 @@ sub recurse { my $is_directory = S_ISDIR($mode); if($is_directory) { next if $file =~ /$excluded_directories/; + next if $srcdir.'/'.$file =~ /$excluded_paths/; recurse($srcdir.'/'.$file); } else { next if !($file =~ /\.(c|cc|cpp|C|h|hh|hpp|H|y|yy|ypp|Y|l|ll|lpp|L|g)$/); diff --git a/src/Makefile.am b/src/Makefile.am index e021cca8d..17c867163 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -46,7 +46,8 @@ libcvc4_noinst_la_LIBADD = \ empty.cpp:; touch empty.cpp publicheaders = \ - include/cvc4_config.h + include/cvc4_public.h \ + include/cvc4parser_public.h install-data-local: $(publicheaders) $(mkinstalldirs) $(DESTDIR)$(includedir)/cvc4 diff --git a/src/context/cdmap.h b/src/context/cdmap.h index 4adf90e4f..e9ae8337e 100644 --- a/src/context/cdmap.h +++ b/src/context/cdmap.h @@ -271,7 +271,9 @@ public: // ContextObj destructor, which calls CDOmap::destroy(), which // restore()'s, which puts the CDOmap on the trash, which causes // a double-delete. - (*i).second->~CDOmap(); + (*i).second->~Element(); + // Writing ...->~CDOmap() in the above is legal (?) but breaks + // g++ 4.1, though later versions have no problem. typename table_type::iterator j = d_map.find(k); // This if() succeeds for objects inserted when in the diff --git a/src/expr/Makefile.am b/src/expr/Makefile.am index 7b34fe431..76f6ef1a4 100644 --- a/src/expr/Makefile.am +++ b/src/expr/Makefile.am @@ -9,19 +9,19 @@ libexpr_la_SOURCES = \ node.h \ node.cpp \ node_builder.h \ - expr.h \ + @srcdir@/expr.h \ type.h \ node_value.h \ node_manager.h \ - expr_manager.h \ + @srcdir@/expr_manager.h \ attribute.h \ attribute.cpp \ @srcdir@/kind.h \ @srcdir@/metakind.h \ node_manager.cpp \ - expr_manager.cpp \ + @srcdir@/expr_manager.cpp \ node_value.cpp \ - expr.cpp \ + @srcdir@/expr.cpp \ type.cpp \ command.h \ command.cpp @@ -29,25 +29,91 @@ libexpr_la_SOURCES = \ EXTRA_DIST = \ @srcdir@/kind.h \ @srcdir@/metakind.h \ + @srcdir@/expr_manager.h \ + @srcdir@/expr.h \ + @srcdir@/expr_manager.cpp \ + @srcdir@/expr.cpp \ kind_template.h \ - metakind_template.h + metakind_template.h \ + expr_manager_template.h \ + expr_manager_template.cpp \ + expr_template.h \ + expr_template.cpp -@srcdir@/kind.h: mkkind kind_template.h builtin_kinds @top_srcdir@/src/theory/Makefile.in @top_srcdir@/src/theory/*/kinds +@srcdir@/kind.h: kind_template.h mkkind builtin_kinds @top_srcdir@/src/theory/Makefile.in @top_srcdir@/src/theory/*/kinds $(AM_V_at)chmod +x @srcdir@/mkkind + $(AM_V_at)mv -f $@ $@~ 2>/dev/null || true $(AM_V_GEN)(@srcdir@/mkkind \ - @srcdir@/kind_template.h \ + $< \ @srcdir@/builtin_kinds \ `grep '^SUBDIRS = ' @top_srcdir@/src/theory/Makefile.in | cut -d' ' -f3- | tr ' ' "\n" | xargs -i__D__ echo @top_srcdir@/src/theory/__D__/kinds` \ - > @srcdir@/kind.h) || (rm -f @srcdir@/kind.h && exit 1) + > $@) || (rm -f $@ && exit 1) -@srcdir@/metakind.h: mkmetakind metakind_template.h builtin_kinds @top_srcdir@/src/theory/Makefile.in @top_srcdir@/src/theory/*/kinds +@srcdir@/metakind.h: metakind_template.h mkmetakind builtin_kinds @top_srcdir@/src/theory/Makefile.in @top_srcdir@/src/theory/*/kinds $(AM_V_at)chmod +x @srcdir@/mkmetakind + $(AM_V_at)mv -f $@ $@~ 2>/dev/null || true $(AM_V_GEN)(@srcdir@/mkmetakind \ - @srcdir@/metakind_template.h \ + $< \ @srcdir@/builtin_kinds \ `grep '^SUBDIRS = ' @top_srcdir@/src/theory/Makefile.in | cut -d' ' -f3- | tr ' ' "\n" | xargs -i__D__ echo @top_srcdir@/src/theory/__D__/kinds` \ - > @srcdir@/metakind.h) || (rm -f @srcdir@/metakind.h && exit 1) + > $@) || (rm -f $@ && exit 1) -BUILT_SOURCES = @srcdir@/kind.h @srcdir@/metakind.h -dist-hook: @srcdir@/kind.h @srcdir@/metakind.h -MAINTAINERCLEANFILES = @srcdir@/kind.h @srcdir@/metakind.h +@srcdir@/expr.h: expr_template.h mkexpr builtin_kinds @top_srcdir@/src/theory/Makefile.in @top_srcdir@/src/theory/*/kinds + $(AM_V_at)chmod +x @srcdir@/mkexpr + $(AM_V_at)mv -f $@ $@~ 2>/dev/null || true + $(AM_V_GEN)(@srcdir@/mkexpr \ + $< \ + @srcdir@/builtin_kinds \ + `grep '^SUBDIRS = ' @top_srcdir@/src/theory/Makefile.in | cut -d' ' -f3- | tr ' ' "\n" | xargs -i__D__ echo @top_srcdir@/src/theory/__D__/kinds` \ + > $@) || (rm -f $@ && exit 1) + +@srcdir@/expr.cpp: expr_template.cpp mkexpr builtin_kinds @top_srcdir@/src/theory/Makefile.in @top_srcdir@/src/theory/*/kinds + $(AM_V_at)chmod +x @srcdir@/mkexpr + $(AM_V_at)mv -f $@ $@~ 2>/dev/null || true + $(AM_V_GEN)(@srcdir@/mkexpr \ + $< \ + @srcdir@/builtin_kinds \ + `grep '^SUBDIRS = ' @top_srcdir@/src/theory/Makefile.in | cut -d' ' -f3- | tr ' ' "\n" | xargs -i__D__ echo @top_srcdir@/src/theory/__D__/kinds` \ + > $@) || (rm -f $@ && exit 1) + +@srcdir@/expr_manager.h: expr_manager_template.h mkexpr builtin_kinds @top_srcdir@/src/theory/Makefile.in @top_srcdir@/src/theory/*/kinds + $(AM_V_at)chmod +x @srcdir@/mkexpr + $(AM_V_at)mv -f $@ $@~ 2>/dev/null || true + $(AM_V_GEN)(@srcdir@/mkexpr \ + $< \ + @srcdir@/builtin_kinds \ + `grep '^SUBDIRS = ' @top_srcdir@/src/theory/Makefile.in | cut -d' ' -f3- | tr ' ' "\n" | xargs -i__D__ echo @top_srcdir@/src/theory/__D__/kinds` \ + > $@) || (rm -f $@ && exit 1) + +@srcdir@/expr_manager.cpp: expr_manager_template.cpp mkexpr builtin_kinds @top_srcdir@/src/theory/Makefile.in @top_srcdir@/src/theory/*/kinds + $(AM_V_at)chmod +x @srcdir@/mkexpr + $(AM_V_at)mv -f $@ $@~ 2>/dev/null || true + $(AM_V_GEN)(@srcdir@/mkexpr \ + $< \ + @srcdir@/builtin_kinds \ + `grep '^SUBDIRS = ' @top_srcdir@/src/theory/Makefile.in | cut -d' ' -f3- | tr ' ' "\n" | xargs -i__D__ echo @top_srcdir@/src/theory/__D__/kinds` \ + > $@) || (rm -f $@ && exit 1) + +BUILT_SOURCES = \ + @srcdir@/kind.h \ + @srcdir@/metakind.h \ + @srcdir@/expr.h \ + @srcdir@/expr.cpp \ + @srcdir@/expr_manager.h \ + @srcdir@/expr_manager.cpp + +dist-hook: \ + @srcdir@/kind.h \ + @srcdir@/metakind.h \ + @srcdir@/expr.h \ + @srcdir@/expr.cpp \ + @srcdir@/expr_manager.h \ + @srcdir@/expr_manager.cpp + +MAINTAINERCLEANFILES = \ + @srcdir@/kind.h \ + @srcdir@/metakind.h \ + @srcdir@/expr.h \ + @srcdir@/expr.cpp \ + @srcdir@/expr_manager.h \ + @srcdir@/expr_manager.cpp diff --git a/src/expr/attribute.cpp b/src/expr/attribute.cpp index 26cb96646..5e8918133 100644 --- a/src/expr/attribute.cpp +++ b/src/expr/attribute.cpp @@ -25,29 +25,6 @@ namespace CVC4 { namespace expr { namespace attr { -/** - * Search for the NodeValue in all attribute tables and remove it, - * calling the cleanup function if one is defined. - */ -template <class T> -inline void AttributeManager::deleteFromTable(AttrHash<T>& table, - NodeValue* nv) { - for(uint64_t id = 0; id < attr::LastAttributeId<T, false>::s_id; ++id) { - typedef AttributeTraits<T, false> traits_t; - typedef AttrHash<T> hash_t; - pair<uint64_t, NodeValue*> pr = std::make_pair(id, nv); - if(traits_t::cleanup[id] != NULL) { - typename hash_t::iterator i = table.find(pr); - if(i != table.end()) { - traits_t::cleanup[id]((*i).second); - table.erase(pr); - } - } else { - table.erase(pr); - } - } -} - void AttributeManager::deleteAllAttributes(NodeValue* nv) { d_bools.erase(nv); deleteFromTable(d_ints, nv); diff --git a/src/expr/attribute.h b/src/expr/attribute.h index efd33d83b..358755192 100644 --- a/src/expr/attribute.h +++ b/src/expr/attribute.h @@ -27,678 +27,22 @@ #include <string> #include <ext/hash_map> -#include "config.h" #include "context/cdmap.h" #include "expr/node.h" #include "expr/type.h" - #include "util/output.h" +// include supporting templates +#define CVC4_ATTRIBUTE_H__INCLUDING__ATTRIBUTE_INTERNALS_H +#include "expr/attribute_internals.h" +#undef CVC4_ATTRIBUTE_H__INCLUDING__ATTRIBUTE_INTERNALS_H + namespace CVC4 { namespace expr { - -// ATTRIBUTE HASH FUNCTIONS ==================================================== - -namespace attr { - -/** - * A hash function for attribute table keys. Attribute table keys are - * pairs, (unique-attribute-id, Node). - */ -struct AttrHashStrategy { - enum { LARGE_PRIME = 32452843ul }; - std::size_t operator()(const std::pair<uint64_t, NodeValue*>& p) const { - return p.first * LARGE_PRIME + p.second->getId(); - } -}; - -/** - * A hash function for boolean-valued attribute table keys; here we - * don't have to store a pair as the key, because we use a known bit - * in [0..63] for each attribute - */ -struct AttrHashBoolStrategy { - std::size_t operator()(NodeValue* nv) const { - return (size_t)nv->getId(); - } -}; - -}/* CVC4::expr::attr namespace */ - -// ATTRIBUTE TYPE MAPPINGS ===================================================== - -namespace attr { - -/** - * KindValueToTableValueMapping is a compile-time-only mechanism to - * convert "attribute value types" into "table value types" and back - * again. - * - * Each instantiation <T> is expected to have three members: - * - * typename table_value_type - * - * A type representing the underlying table's value_type for - * attribute value type (T). It may be different from T, e.g. T - * could be a pointer-to-Foo, but the underlying table value_type - * might be pointer-to-void. - * - * static [convertible-to-table_value_type] convert([convertible-from-T]) - * - * Converts a T into a table_value_type. Used to convert an - * attribute value on setting it (and assigning it into the - * underlying table). See notes on specializations of - * KindValueToTableValueMapping, below. - * - * static [convertible-to-T] convertBack([convertible-from-table_value_type]) - * - * Converts a table_value_type back into a T. Used to convert an - * underlying table value back into the attribute's expected type - * when retrieving it from the table. See notes on - * specializations of KindValueToTableValueMapping, below. - * - * This general (non-specialized) implementation of the template does - * nothing. - */ -template <class T> -struct KindValueToTableValueMapping { - /** Simple case: T == table_value_type */ - typedef T table_value_type; - /** No conversion necessary */ - inline static T convert(const T& t) { return t; } - /** No conversion necessary */ - inline static T convertBack(const T& t) { return t; } -}; - -/** - * Specialization of KindValueToTableValueMapping<> for pointer-valued - * attributes. - */ -template <class T> -struct KindValueToTableValueMapping<T*> { - /** Table's value type is void* */ - typedef void* table_value_type; - /** A simple reinterpret_cast<>() conversion from T* to void* */ - inline static void* convert(const T* const& t) { - return reinterpret_cast<void*>(const_cast<T*>(t)); - } - /** A simple reinterpret_cast<>() conversion from void* to T* */ - inline static T* convertBack(void* const& t) { - return reinterpret_cast<T*>(t); - } -}; - -/** - * Specialization of KindValueToTableValueMapping<> for const - * pointer-valued attributes. - */ -template <class T> -struct KindValueToTableValueMapping<const T*> { - /** Table's value type is void* */ - typedef void* table_value_type; - /** A simple reinterpret_cast<>() conversion from const T* const to void* */ - inline static void* convert(const T* const& t) { - return reinterpret_cast<void*>(const_cast<T*>(t)); - } - /** A simple reinterpret_cast<>() conversion from const void* const to T* */ - inline static const T* convertBack(const void* const& t) { - return reinterpret_cast<const T*>(t); - } -}; - -}/* CVC4::expr::attr namespace */ - -// ATTRIBUTE HASH TABLES ======================================================= - -namespace attr { - -/** - * An "AttrHash<value_type>"---the hash table underlying - * attributes---is simply a mapping of pair<unique-attribute-id, Node> - * to value_type using our specialized hash function for these pairs. - */ -template <class value_type> -struct AttrHash : - public __gnu_cxx::hash_map<std::pair<uint64_t, NodeValue*>, - value_type, - AttrHashStrategy> { -}; - -/** - * In the case of Boolean-valued attributes we have a special - * "AttrHash<bool>" to pack bits together in words. - */ -template <> -class AttrHash<bool> : - protected __gnu_cxx::hash_map<NodeValue*, - uint64_t, - AttrHashBoolStrategy> { - - /** A "super" type, like in Java, for easy reference below. */ - typedef __gnu_cxx::hash_map<NodeValue*, uint64_t, AttrHashBoolStrategy> super; - - /** - * BitAccessor allows us to return a bit "by reference." Of course, - * we don't require bit-addressibility supported by the system, we - * do it with a complex type. - */ - class BitAccessor { - - uint64_t& d_word; - - unsigned d_bit; - - public: - - BitAccessor(uint64_t& word, unsigned bit) : - d_word(word), - d_bit(bit) { - } - - BitAccessor& operator=(bool b) { - if(b) { - // set the bit - d_word |= (1 << d_bit); - } else { - // clear the bit - d_word &= ~(1 << d_bit); - } - - return *this; - } - - operator bool() const { - return (d_word & (1 << d_bit)) ? true : false; - } - }; - - /** - * A (somewhat degenerate) iterator over boolean-valued attributes. - * This iterator doesn't support anything except comparison and - * dereference. It's intended just for the result of find() on the - * table. - */ - class BitIterator { - - std::pair<NodeValue* const, uint64_t>* d_entry; - - unsigned d_bit; - - public: - - BitIterator() : - d_entry(NULL), - d_bit(0) { - } - - BitIterator(std::pair<NodeValue* const, uint64_t>& entry, unsigned bit) : - d_entry(&entry), - d_bit(bit) { - } - - std::pair<NodeValue* const, BitAccessor> operator*() { - return std::make_pair(d_entry->first, BitAccessor(d_entry->second, d_bit)); - } - - bool operator==(const BitIterator& b) { - return d_entry == b.d_entry && d_bit == b.d_bit; - } - }; - - /** - * A (somewhat degenerate) const_iterator over boolean-valued - * attributes. This const_iterator doesn't support anything except - * comparison and dereference. It's intended just for the result of - * find() on the table. - */ - class ConstBitIterator { - - const std::pair<NodeValue* const, uint64_t>* d_entry; - - unsigned d_bit; - - public: - - ConstBitIterator() : - d_entry(NULL), - d_bit(0) { - } - - ConstBitIterator(const std::pair<NodeValue* const, uint64_t>& entry, unsigned bit) : - d_entry(&entry), - d_bit(bit) { - } - - std::pair<NodeValue* const, bool> operator*() { - return std::make_pair(d_entry->first, (d_entry->second & (1 << d_bit)) ? true : false); - } - - bool operator==(const ConstBitIterator& b) { - return d_entry == b.d_entry && d_bit == b.d_bit; - } - }; - -public: - - typedef std::pair<uint64_t, NodeValue*> key_type; - typedef bool data_type; - typedef std::pair<const key_type, data_type> value_type; - - /** an iterator type; see above for limitations */ - typedef BitIterator iterator; - /** a const_iterator type; see above for limitations */ - typedef ConstBitIterator const_iterator; - - /** - * Find the boolean value in the hash table. Returns something == - * end() if not found. - */ - BitIterator find(const std::pair<uint64_t, NodeValue*>& k) { - super::iterator i = super::find(k.second); - if(i == super::end()) { - return BitIterator(); - } - Debug.printf("boolattr", - "underlying word at 0x%p looks like 0x%016llx, bit is %u\n", - &(*i).second, - (unsigned long long)((*i).second), - unsigned(k.first)); - return BitIterator(*i, k.first); - } - - /** The "off the end" iterator */ - BitIterator end() { - return BitIterator(); - } - - /** - * Find the boolean value in the hash table. Returns something == - * end() if not found. - */ - ConstBitIterator find(const std::pair<uint64_t, NodeValue*>& k) const { - super::const_iterator i = super::find(k.second); - if(i == super::end()) { - return ConstBitIterator(); - } - Debug.printf("boolattr", - "underlying word at 0x%p looks like 0x%016llx, bit is %u\n", - &(*i).second, - (unsigned long long)((*i).second), - unsigned(k.first)); - return ConstBitIterator(*i, k.first); - } - - /** The "off the end" const_iterator */ - ConstBitIterator end() const { - return ConstBitIterator(); - } - - /** - * Access the hash table using the underlying operator[]. Inserts - * the key into the table (associated to default value) if it's not - * already there. - */ - BitAccessor operator[](const std::pair<uint64_t, NodeValue*>& k) { - uint64_t& word = super::operator[](k.second); - return BitAccessor(word, k.first); - } - - /** - * Delete all flags from the given node. - */ - void erase(NodeValue* nv) { - super::erase(nv); - } - -};/* class AttrHash<bool> */ - -/** - * A "CDAttrHash<value_type>"---the hash table underlying - * attributes---is simply a context-dependent mapping of - * pair<unique-attribute-id, Node> to value_type using our specialized - * hash function for these pairs. - */ -template <class value_type> -class CDAttrHash : - public CVC4::context::CDMap<std::pair<uint64_t, NodeValue*>, - value_type, - AttrHashStrategy> { -public: - CDAttrHash(context::Context* ctxt) : - context::CDMap<std::pair<uint64_t, NodeValue*>, - value_type, - AttrHashStrategy>(ctxt) { - } -}; - -/// FIXME ------ need optimized (packed) specialization of CDAttrHash<bool> ------- FIXME -/// FIXME ------ need optimized (packed) specialization of CDAttrHash<bool> ------- FIXME -/// FIXME ------ need optimized (packed) specialization of CDAttrHash<bool> ------- FIXME -/// FIXME ------ need optimized (packed) specialization of CDAttrHash<bool> ------- FIXME -/// FIXME ------ need optimized (packed) specialization of CDAttrHash<bool> ------- FIXME -/// FIXME ------ need optimized (packed) specialization of CDAttrHash<bool> ------- FIXME -/// FIXME ------ need optimized (packed) specialization of CDAttrHash<bool> ------- FIXME -/// FIXME ------ need optimized (packed) specialization of CDAttrHash<bool> ------- FIXME -/// FIXME ------ need optimized (packed) specialization of CDAttrHash<bool> ------- FIXME -/// FIXME ------ need optimized (packed) specialization of CDAttrHash<bool> ------- FIXME - -}/* CVC4::expr::attr namespace */ - -// ATTRIBUTE CLEANUP FUNCTIONS ================================================= - namespace attr { -/** Default cleanup for unmanaged Attribute<> */ -struct NullCleanupStrategy { -};/* struct NullCleanupStrategy */ - -/** Default cleanup for ManagedAttribute<> */ -template <class T> -struct ManagedAttributeCleanupStrategy { -};/* struct ManagedAttributeCleanupStrategy<> */ - -/** Specialization for T* */ -template <class T> -struct ManagedAttributeCleanupStrategy<T*> { - static inline void cleanup(T* p) { delete p; } -};/* struct ManagedAttributeCleanupStrategy<T*> */ - -/** Specialization for const T* */ -template <class T> -struct ManagedAttributeCleanupStrategy<const T*> { - static inline void cleanup(const T* p) { delete p; } -};/* struct ManagedAttributeCleanupStrategy<const T*> */ - -/** - * Helper for Attribute<> class below to determine whether a cleanup - * is defined or not. - */ -template <class T, class C> -struct getCleanupStrategy { - typedef T value_type; - typedef KindValueToTableValueMapping<value_type> mapping; - static void fn(typename mapping::table_value_type t) { - C::cleanup(mapping::convertBack(t)); - } -};/* struct getCleanupStrategy<> */ - -/** - * Specialization for NullCleanupStrategy. - */ -template <class T> -struct getCleanupStrategy<T, NullCleanupStrategy> { - typedef T value_type; - typedef KindValueToTableValueMapping<value_type> mapping; - static void (*const fn)(typename mapping::table_value_type); -};/* struct getCleanupStrategy<T, NullCleanupStrategy> */ - -// out-of-class initialization required (because it's a non-integral type) -template <class T> -void (*const getCleanupStrategy<T, NullCleanupStrategy>::fn)(typename getCleanupStrategy<T, NullCleanupStrategy>::mapping::table_value_type) = NULL; - -/** - * Specialization for ManagedAttributeCleanupStrategy<T>. - */ -template <class T> -struct getCleanupStrategy<T, ManagedAttributeCleanupStrategy<T> > { - typedef T value_type; - typedef KindValueToTableValueMapping<value_type> mapping; - static void (*const fn)(typename mapping::table_value_type); -};/* struct getCleanupStrategy<T, ManagedAttributeCleanupStrategy<T> > */ - -// out-of-class initialization required (because it's a non-integral type) -template <class T> -void (*const getCleanupStrategy<T, ManagedAttributeCleanupStrategy<T> >::fn)(typename getCleanupStrategy<T, ManagedAttributeCleanupStrategy<T> >::mapping::table_value_type) = NULL; - -/** - * Specialization for ManagedAttributeCleanupStrategy<T*>. - */ -template <class T> -struct getCleanupStrategy<T*, ManagedAttributeCleanupStrategy<T*> > { - typedef T* value_type; - typedef ManagedAttributeCleanupStrategy<value_type> C; - typedef KindValueToTableValueMapping<value_type> mapping; - static void fn(typename mapping::table_value_type t) { - C::cleanup(mapping::convertBack(t)); - } -};/* struct getCleanupStrategy<T*, ManagedAttributeCleanupStrategy<T*> > */ - -/** - * Specialization for ManagedAttributeCleanupStrategy<const T*>. - */ -template <class T> -struct getCleanupStrategy<const T*, ManagedAttributeCleanupStrategy<const T*> > { - typedef const T* value_type; - typedef ManagedAttributeCleanupStrategy<value_type> C; - typedef KindValueToTableValueMapping<value_type> mapping; - static void fn(typename mapping::table_value_type t) { - C::cleanup(mapping::convertBack(t)); - } -};/* struct getCleanupStrategy<const T*, ManagedAttributeCleanupStrategy<const T*> > */ - -/** - * Cause compile-time error for improperly-instantiated - * getCleanupStrategy<>. - */ -template <class T, class U> -struct getCleanupStrategy<T, ManagedAttributeCleanupStrategy<U> >; - -}/* CVC4::expr::attr namespace */ - -// ATTRIBUTE IDENTIFIER ASSIGNMENT TEMPLATE ==================================== - -namespace attr { - -/** - * This is the last-attribute-assigner. IDs are not globally - * unique; rather, they are unique for each table_value_type. - */ -template <class T, bool context_dep> -struct LastAttributeId { - static uint64_t s_id; -}; - -/** Initially zero. */ -template <class T, bool context_dep> -uint64_t LastAttributeId<T, context_dep>::s_id = 0; - -}/* CVC4::expr::attr namespace */ - -// ATTRIBUTE TRAITS ============================================================ - -namespace attr { - -/** - * This is the last-attribute-assigner. IDs are not globally - * unique; rather, they are unique for each table_value_type. - */ -template <class T, bool context_dep> -struct AttributeTraits { - typedef void (*cleanup_t)(T); - static std::vector<cleanup_t> cleanup; -}; - -template <class T, bool context_dep> -std::vector<typename AttributeTraits<T, context_dep>::cleanup_t> - AttributeTraits<T, context_dep>::cleanup; - -}/* CVC4::expr::attr namespace */ - -// ATTRIBUTE DEFINITION ======================================================== - -/** - * An "attribute type" structure. - * - * @param T the tag for the attribute kind. - * - * @param value_t the underlying value_type for the attribute kind - * - * @param CleanupStrategy Clean-up routine for associated values when the - * Node goes away. Useful, e.g., for pointer-valued attributes when - * the values are "owned" by the table. - * - * @param context_dep whether this attribute kind is - * context-dependent - */ -template <class T, - class value_t, - class CleanupStrategy = attr::NullCleanupStrategy, - bool context_dep = false> -class Attribute { - /** - * The unique ID associated to this attribute. Assigned statically, - * at load time. - */ - static const uint64_t s_id; - -public: - - /** The value type for this attribute. */ - typedef value_t value_type; - - /** Get the unique ID associated to this attribute. */ - static inline uint64_t getId() { return s_id; } - - /** - * This attribute does not have a default value: calling - * hasAttribute() for a Node that hasn't had this attribute set will - * return false, and getAttribute() for the Node will return a - * default-constructed value_type. - */ - static const bool has_default_value = false; - - /** - * Expose this setting to the users of this Attribute kind. - */ - static const bool context_dependent = context_dep; - - /** - * Register this attribute kind and check that the ID is a valid ID - * for bool-valued attributes. Fail an assert if not. Otherwise - * return the id. - */ - static inline uint64_t registerAttribute() { - typedef typename attr::KindValueToTableValueMapping<value_t>::table_value_type table_value_type; - typedef attr::AttributeTraits<table_value_type, context_dep> traits; - uint64_t id = attr::LastAttributeId<table_value_type, context_dep>::s_id++; - Assert(traits::cleanup.size() == id);// sanity check - traits::cleanup.push_back(attr::getCleanupStrategy<value_t, CleanupStrategy>::fn); - return id; - } -};/* class Attribute<> */ - -/** - * An "attribute type" structure for boolean flags (special). The - * full one is below; the existence of this one disallows for boolean - * flag attributes with a specialized cleanup function. - */ -/* -- doesn't work; other specialization is "more specific" ?? -template <class T, class CleanupStrategy, bool context_dep> -class Attribute<T, bool, CleanupStrategy, context_dep> { - template <bool> struct ERROR_bool_attributes_cannot_have_cleanup_functions; - ERROR_bool_attributes_cannot_have_cleanup_functions<true> blah; -}; -*/ - -/** - * An "attribute type" structure for boolean flags (special). - */ -template <class T, bool context_dep> -class Attribute<T, bool, attr::NullCleanupStrategy, context_dep> { - /** IDs for bool-valued attributes are actually bit assignments. */ - static const uint64_t s_id; - -public: - - /** The value type for this attribute; here, bool. */ - typedef bool value_type; - - /** Get the unique ID associated to this attribute. */ - static inline uint64_t getId() { return s_id; } - - /** - * Such bool-valued attributes ("flags") have a default value: they - * are false for all nodes on entry. Calling hasAttribute() for a - * Node that hasn't had this attribute set will return true, and - * getAttribute() for the Node will return the default_value below. - */ - static const bool has_default_value = true; - - /** - * Default value of the attribute for Nodes without one explicitly - * set. - */ - static const bool default_value = false; - - /** - * Expose this setting to the users of this Attribute kind. - */ - static const bool context_dependent = context_dep; - - /** - * Register this attribute kind and check that the ID is a valid ID - * for bool-valued attributes. Fail an assert if not. Otherwise - * return the id. - */ - static inline uint64_t registerAttribute() { - uint64_t id = attr::LastAttributeId<bool, context_dep>::s_id++; - AlwaysAssert( id <= 63, - "Too many boolean node attributes registered " - "during initialization !" ); - return id; - } -};/* class Attribute<..., bool, ...> */ - -/** - * This is a context-dependent attribute kind (the only difference - * between CDAttribute<> and Attribute<> (with the fourth argument - * "true") is that you cannot supply a cleanup function (a no-op one - * is used). - */ -template <class T, - class value_type> -struct CDAttribute : - public Attribute<T, value_type, attr::NullCleanupStrategy, true> {}; - -/** - * This is a managed attribute kind (the only difference between - * ManagedAttribute<> and Attribute<> is the default cleanup function - * and the fact that ManagedAttributes cannot be context-dependent). - * In the default ManagedAttribute cleanup function, the value is - * destroyed with the delete operator. If the value is allocated with - * the array version of new[], an alternate cleanup function should be - * provided that uses array delete[]. It is an error to create a - * ManagedAttribute<> kind with a non-pointer value_type if you don't - * also supply a custom cleanup function. - */ -template <class T, - class value_type, - class CleanupStrategy = attr::ManagedAttributeCleanupStrategy<value_type> > -struct ManagedAttribute : - public Attribute<T, value_type, CleanupStrategy, false> {}; - -// ATTRIBUTE IDENTIFIER ASSIGNMENT ============================================= - -/** Assign unique IDs to attributes at load time. */ -// Use of the comma-operator here forces instantiation (and -// initialization) of the AttributeTraits<> structure and its -// "cleanup" vector before registerAttribute() is called. This is -// important because otherwise the vector is initialized later, -// clearing the first-pushed cleanup function. -template <class T, class value_t, class CleanupStrategy, bool context_dep> -const uint64_t Attribute<T, value_t, CleanupStrategy, context_dep>::s_id = - ( attr::AttributeTraits<typename attr::KindValueToTableValueMapping<value_t>::table_value_type, context_dep>::cleanup.size(), - Attribute<T, value_t, CleanupStrategy, context_dep>::registerAttribute() ); - -/** Assign unique IDs to attributes at load time. */ -template <class T, bool context_dep> -const uint64_t Attribute<T, bool, attr::NullCleanupStrategy, context_dep>::s_id = - Attribute<T, bool, attr::NullCleanupStrategy, context_dep>::registerAttribute(); - // ATTRIBUTE MANAGER =========================================================== -namespace attr { - /** * A container for the main attribute tables of the system. There's a * one-to-one NodeManager : AttributeManager correspondence. @@ -868,7 +212,7 @@ struct getTable<uint64_t, false> { /** Access the "d_exprs" member of AttributeManager. */ template <> -struct getTable<Node, false> { +struct getTable<TNode, false> { typedef AttrHash<TNode> table_type; static inline table_type& get(AttributeManager& am) { return am.d_exprs; @@ -940,7 +284,7 @@ struct getTable<uint64_t, true> { /** Access the "d_cdexprs" member of AttributeManager. */ template <> -struct getTable<Node, true> { +struct getTable<TNode, true> { typedef CDAttrHash<TNode> table_type; static inline table_type& get(AttributeManager& am) { return am.d_cdexprs; @@ -994,15 +338,17 @@ namespace attr { // implementation for AttributeManager::getAttribute() template <class AttrKind> -typename AttrKind::value_type AttributeManager::getAttribute(NodeValue* nv, - const AttrKind&) const { - +typename AttrKind::value_type +AttributeManager::getAttribute(NodeValue* nv, const AttrKind&) const { typedef typename AttrKind::value_type value_type; typedef KindValueToTableValueMapping<value_type> mapping; - typedef typename getTable<value_type, AttrKind::context_dependent>::table_type table_type; + typedef typename getTable<value_type, AttrKind::context_dependent>:: + table_type table_type; - const table_type& ah = getTable<value_type, AttrKind::context_dependent>::get(*this); - typename table_type::const_iterator i = ah.find(std::make_pair(AttrKind::getId(), nv)); + const table_type& ah = + getTable<value_type, AttrKind::context_dependent>::get(*this); + typename table_type::const_iterator i = + ah.find(std::make_pair(AttrKind::getId(), nv)); if(i == ah.end()) { return typename AttrKind::value_type(); @@ -1038,10 +384,14 @@ struct HasAttribute<true, AttrKind> { typename AttrKind::value_type& ret) { typedef typename AttrKind::value_type value_type; typedef KindValueToTableValueMapping<value_type> mapping; - typedef typename getTable<value_type, AttrKind::context_dependent>::table_type table_type; + typedef typename getTable<value_type, + AttrKind::context_dependent>::table_type + table_type; - const table_type& ah = getTable<value_type, AttrKind::context_dependent>::get(*am); - typename table_type::const_iterator i = ah.find(std::make_pair(AttrKind::getId(), nv)); + const table_type& ah = + getTable<value_type, AttrKind::context_dependent>::get(*am); + typename table_type::const_iterator i = + ah.find(std::make_pair(AttrKind::getId(), nv)); if(i == ah.end()) { ret = AttrKind::default_value; @@ -1063,10 +413,13 @@ struct HasAttribute<false, AttrKind> { NodeValue* nv) { typedef typename AttrKind::value_type value_type; typedef KindValueToTableValueMapping<value_type> mapping; - typedef typename getTable<value_type, AttrKind::context_dependent>::table_type table_type; + typedef typename getTable<value_type, AttrKind::context_dependent>:: + table_type table_type; - const table_type& ah = getTable<value_type, AttrKind::context_dependent>::get(*am); - typename table_type::const_iterator i = ah.find(std::make_pair(AttrKind::getId(), nv)); + const table_type& ah = + getTable<value_type, AttrKind::context_dependent>::get(*am); + typename table_type::const_iterator i = + ah.find(std::make_pair(AttrKind::getId(), nv)); if(i == ah.end()) { return false; @@ -1080,10 +433,13 @@ struct HasAttribute<false, AttrKind> { typename AttrKind::value_type& ret) { typedef typename AttrKind::value_type value_type; typedef KindValueToTableValueMapping<value_type> mapping; - typedef typename getTable<value_type, AttrKind::context_dependent>::table_type table_type; + typedef typename getTable<value_type, AttrKind::context_dependent>:: + table_type table_type; - const table_type& ah = getTable<value_type, AttrKind::context_dependent>::get(*am); - typename table_type::const_iterator i = ah.find(std::make_pair(AttrKind::getId(), nv)); + const table_type& ah = + getTable<value_type, AttrKind::context_dependent>::get(*am); + typename table_type::const_iterator i = + ah.find(std::make_pair(AttrKind::getId(), nv)); if(i == ah.end()) { return false; @@ -1098,29 +454,56 @@ struct HasAttribute<false, AttrKind> { template <class AttrKind> bool AttributeManager::hasAttribute(NodeValue* nv, const AttrKind&) const { - return HasAttribute<AttrKind::has_default_value, AttrKind>::hasAttribute(this, nv); + return HasAttribute<AttrKind::has_default_value, AttrKind>:: + hasAttribute(this, nv); } template <class AttrKind> bool AttributeManager::getAttribute(NodeValue* nv, const AttrKind&, typename AttrKind::value_type& ret) const { - return HasAttribute<AttrKind::has_default_value, AttrKind>::getAttribute(this, nv, ret); + return HasAttribute<AttrKind::has_default_value, AttrKind>:: + getAttribute(this, nv, ret); } template <class AttrKind> -inline void AttributeManager::setAttribute(NodeValue* nv, - const AttrKind&, - const typename AttrKind::value_type& value) { - +inline void +AttributeManager::setAttribute(NodeValue* nv, + const AttrKind&, + const typename AttrKind::value_type& value) { typedef typename AttrKind::value_type value_type; typedef KindValueToTableValueMapping<value_type> mapping; - typedef typename getTable<value_type, AttrKind::context_dependent>::table_type table_type; + typedef typename getTable<value_type, AttrKind::context_dependent>:: + table_type table_type; - table_type& ah = getTable<value_type, AttrKind::context_dependent>::get(*this); + table_type& ah = + getTable<value_type, AttrKind::context_dependent>::get(*this); ah[std::make_pair(AttrKind::getId(), nv)] = mapping::convert(value); } +/** + * Search for the NodeValue in all attribute tables and remove it, + * calling the cleanup function if one is defined. + */ +template <class T> +inline void AttributeManager::deleteFromTable(AttrHash<T>& table, + NodeValue* nv) { + for(uint64_t id = 0; id < attr::LastAttributeId<T, false>::s_id; ++id) { + typedef AttributeTraits<T, false> traits_t; + typedef AttrHash<T> hash_t; + std::pair<uint64_t, NodeValue*> pr = std::make_pair(id, nv); + if(traits_t::cleanup[id] != NULL) { + typename hash_t::iterator i = table.find(pr); + if(i != table.end()) { + traits_t::cleanup[id]((*i).second); + table.erase(pr); + } + } else { + table.erase(pr); + } + } +} + }/* CVC4::expr::attr namespace */ }/* CVC4::expr namespace */ }/* CVC4 namespace */ diff --git a/src/expr/attribute_internals.h b/src/expr/attribute_internals.h new file mode 100644 index 000000000..d50c2284d --- /dev/null +++ b/src/expr/attribute_internals.h @@ -0,0 +1,695 @@ +/********************* */ +/** attribute_internals.h + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010 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. + ** + ** Node attributes' internals. + **/ + +#include "cvc4_private.h" + +#ifndef CVC4_ATTRIBUTE_H__INCLUDING__ATTRIBUTE_INTERNALS_H +# error expr/attribute_internals.h should only be included by expr/attribute.h +#endif /* CVC4_ATTRIBUTE_H__INCLUDING__ATTRIBUTE_INTERNALS_H */ + +#ifndef __CVC4__EXPR__ATTRIBUTE_INTERNALS_H +#define __CVC4__EXPR__ATTRIBUTE_INTERNALS_H + +namespace CVC4 { +namespace expr { + +// ATTRIBUTE HASH FUNCTIONS ==================================================== + +namespace attr { + +/** + * A hash function for attribute table keys. Attribute table keys are + * pairs, (unique-attribute-id, Node). + */ +struct AttrHashStrategy { + enum { LARGE_PRIME = 32452843ul }; + std::size_t operator()(const std::pair<uint64_t, NodeValue*>& p) const { + return p.first * LARGE_PRIME + p.second->getId(); + } +}; + +/** + * A hash function for boolean-valued attribute table keys; here we + * don't have to store a pair as the key, because we use a known bit + * in [0..63] for each attribute + */ +struct AttrHashBoolStrategy { + std::size_t operator()(NodeValue* nv) const { + return (size_t)nv->getId(); + } +}; + +}/* CVC4::expr::attr namespace */ + +// ATTRIBUTE TYPE MAPPINGS ===================================================== + +namespace attr { + +/** + * KindValueToTableValueMapping is a compile-time-only mechanism to + * convert "attribute value types" into "table value types" and back + * again. + * + * Each instantiation <T> is expected to have three members: + * + * typename table_value_type + * + * A type representing the underlying table's value_type for + * attribute value type (T). It may be different from T, e.g. T + * could be a pointer-to-Foo, but the underlying table value_type + * might be pointer-to-void. + * + * static [convertible-to-table_value_type] convert([convertible-from-T]) + * + * Converts a T into a table_value_type. Used to convert an + * attribute value on setting it (and assigning it into the + * underlying table). See notes on specializations of + * KindValueToTableValueMapping, below. + * + * static [convertible-to-T] convertBack([convertible-from-table_value_type]) + * + * Converts a table_value_type back into a T. Used to convert an + * underlying table value back into the attribute's expected type + * when retrieving it from the table. See notes on + * specializations of KindValueToTableValueMapping, below. + * + * This general (non-specialized) implementation of the template does + * nothing. + */ +template <class T> +struct KindValueToTableValueMapping { + /** Simple case: T == table_value_type */ + typedef T table_value_type; + /** No conversion necessary */ + inline static T convert(const T& t) { return t; } + /** No conversion necessary */ + inline static T convertBack(const T& t) { return t; } +}; + +/** + * Specialization of KindValueToTableValueMapping<> for pointer-valued + * attributes. + */ +template <class T> +struct KindValueToTableValueMapping<T*> { + /** Table's value type is void* */ + typedef void* table_value_type; + /** A simple reinterpret_cast<>() conversion from T* to void* */ + inline static void* convert(const T* const& t) { + return reinterpret_cast<void*>(const_cast<T*>(t)); + } + /** A simple reinterpret_cast<>() conversion from void* to T* */ + inline static T* convertBack(void* const& t) { + return reinterpret_cast<T*>(t); + } +}; + +/** + * Specialization of KindValueToTableValueMapping<> for const + * pointer-valued attributes. + */ +template <class T> +struct KindValueToTableValueMapping<const T*> { + /** Table's value type is void* */ + typedef void* table_value_type; + /** A simple reinterpret_cast<>() conversion from const T* const to void* */ + inline static void* convert(const T* const& t) { + return reinterpret_cast<void*>(const_cast<T*>(t)); + } + /** A simple reinterpret_cast<>() conversion from const void* const to T* */ + inline static const T* convertBack(const void* const& t) { + return reinterpret_cast<const T*>(t); + } +}; + +}/* CVC4::expr::attr namespace */ + +// ATTRIBUTE HASH TABLES ======================================================= + +namespace attr { + +/** + * An "AttrHash<value_type>"---the hash table underlying + * attributes---is simply a mapping of pair<unique-attribute-id, Node> + * to value_type using our specialized hash function for these pairs. + */ +template <class value_type> +struct AttrHash : + public __gnu_cxx::hash_map<std::pair<uint64_t, NodeValue*>, + value_type, + AttrHashStrategy> { +}; + +/** + * In the case of Boolean-valued attributes we have a special + * "AttrHash<bool>" to pack bits together in words. + */ +template <> +class AttrHash<bool> : + protected __gnu_cxx::hash_map<NodeValue*, + uint64_t, + AttrHashBoolStrategy> { + + /** A "super" type, like in Java, for easy reference below. */ + typedef __gnu_cxx::hash_map<NodeValue*, uint64_t, AttrHashBoolStrategy> super; + + /** + * BitAccessor allows us to return a bit "by reference." Of course, + * we don't require bit-addressibility supported by the system, we + * do it with a complex type. + */ + class BitAccessor { + + uint64_t& d_word; + + unsigned d_bit; + + public: + + BitAccessor(uint64_t& word, unsigned bit) : + d_word(word), + d_bit(bit) { + } + + BitAccessor& operator=(bool b) { + if(b) { + // set the bit + d_word |= (1 << d_bit); + } else { + // clear the bit + d_word &= ~(1 << d_bit); + } + + return *this; + } + + operator bool() const { + return (d_word & (1 << d_bit)) ? true : false; + } + }; + + /** + * A (somewhat degenerate) iterator over boolean-valued attributes. + * This iterator doesn't support anything except comparison and + * dereference. It's intended just for the result of find() on the + * table. + */ + class BitIterator { + + std::pair<NodeValue* const, uint64_t>* d_entry; + + unsigned d_bit; + + public: + + BitIterator() : + d_entry(NULL), + d_bit(0) { + } + + BitIterator(std::pair<NodeValue* const, uint64_t>& entry, unsigned bit) : + d_entry(&entry), + d_bit(bit) { + } + + std::pair<NodeValue* const, BitAccessor> operator*() { + return std::make_pair(d_entry->first, + BitAccessor(d_entry->second, d_bit)); + } + + bool operator==(const BitIterator& b) { + return d_entry == b.d_entry && d_bit == b.d_bit; + } + }; + + /** + * A (somewhat degenerate) const_iterator over boolean-valued + * attributes. This const_iterator doesn't support anything except + * comparison and dereference. It's intended just for the result of + * find() on the table. + */ + class ConstBitIterator { + + const std::pair<NodeValue* const, uint64_t>* d_entry; + + unsigned d_bit; + + public: + + ConstBitIterator() : + d_entry(NULL), + d_bit(0) { + } + + ConstBitIterator(const std::pair<NodeValue* const, uint64_t>& entry, + unsigned bit) : + d_entry(&entry), + d_bit(bit) { + } + + std::pair<NodeValue* const, bool> operator*() { + return std::make_pair(d_entry->first, + (d_entry->second & (1 << d_bit)) ? true : false); + } + + bool operator==(const ConstBitIterator& b) { + return d_entry == b.d_entry && d_bit == b.d_bit; + } + }; + +public: + + typedef std::pair<uint64_t, NodeValue*> key_type; + typedef bool data_type; + typedef std::pair<const key_type, data_type> value_type; + + /** an iterator type; see above for limitations */ + typedef BitIterator iterator; + /** a const_iterator type; see above for limitations */ + typedef ConstBitIterator const_iterator; + + /** + * Find the boolean value in the hash table. Returns something == + * end() if not found. + */ + BitIterator find(const std::pair<uint64_t, NodeValue*>& k) { + super::iterator i = super::find(k.second); + if(i == super::end()) { + return BitIterator(); + } + Debug.printf("boolattr", + "underlying word at 0x%p looks like 0x%016llx, bit is %u\n", + &(*i).second, + (unsigned long long)((*i).second), + unsigned(k.first)); + return BitIterator(*i, k.first); + } + + /** The "off the end" iterator */ + BitIterator end() { + return BitIterator(); + } + + /** + * Find the boolean value in the hash table. Returns something == + * end() if not found. + */ + ConstBitIterator find(const std::pair<uint64_t, NodeValue*>& k) const { + super::const_iterator i = super::find(k.second); + if(i == super::end()) { + return ConstBitIterator(); + } + Debug.printf("boolattr", + "underlying word at 0x%p looks like 0x%016llx, bit is %u\n", + &(*i).second, + (unsigned long long)((*i).second), + unsigned(k.first)); + return ConstBitIterator(*i, k.first); + } + + /** The "off the end" const_iterator */ + ConstBitIterator end() const { + return ConstBitIterator(); + } + + /** + * Access the hash table using the underlying operator[]. Inserts + * the key into the table (associated to default value) if it's not + * already there. + */ + BitAccessor operator[](const std::pair<uint64_t, NodeValue*>& k) { + uint64_t& word = super::operator[](k.second); + return BitAccessor(word, k.first); + } + + /** + * Delete all flags from the given node. + */ + void erase(NodeValue* nv) { + super::erase(nv); + } + +};/* class AttrHash<bool> */ + +/** + * A "CDAttrHash<value_type>"---the hash table underlying + * attributes---is simply a context-dependent mapping of + * pair<unique-attribute-id, Node> to value_type using our specialized + * hash function for these pairs. + */ +template <class value_type> +class CDAttrHash : + public context::CDMap<std::pair<uint64_t, NodeValue*>, + value_type, + AttrHashStrategy> { +public: + CDAttrHash(context::Context* ctxt) : + context::CDMap<std::pair<uint64_t, NodeValue*>, + value_type, + AttrHashStrategy>(ctxt) { + } +}; + +}/* CVC4::expr::attr namespace */ + +// ATTRIBUTE CLEANUP FUNCTIONS ================================================= + +namespace attr { + +/** Default cleanup for unmanaged Attribute<> */ +struct NullCleanupStrategy { +};/* struct NullCleanupStrategy */ + +/** Default cleanup for ManagedAttribute<> */ +template <class T> +struct ManagedAttributeCleanupStrategy { +};/* struct ManagedAttributeCleanupStrategy<> */ + +/** Specialization for T* */ +template <class T> +struct ManagedAttributeCleanupStrategy<T*> { + static inline void cleanup(T* p) { delete p; } +};/* struct ManagedAttributeCleanupStrategy<T*> */ + +/** Specialization for const T* */ +template <class T> +struct ManagedAttributeCleanupStrategy<const T*> { + static inline void cleanup(const T* p) { delete p; } +};/* struct ManagedAttributeCleanupStrategy<const T*> */ + +/** + * Helper for Attribute<> class below to determine whether a cleanup + * is defined or not. + */ +template <class T, class C> +struct getCleanupStrategy { + typedef T value_type; + typedef KindValueToTableValueMapping<value_type> mapping; + static void fn(typename mapping::table_value_type t) { + C::cleanup(mapping::convertBack(t)); + } +};/* struct getCleanupStrategy<> */ + +/** + * Specialization for NullCleanupStrategy. + */ +template <class T> +struct getCleanupStrategy<T, NullCleanupStrategy> { + typedef T value_type; + typedef KindValueToTableValueMapping<value_type> mapping; + static void (*const fn)(typename mapping::table_value_type); +};/* struct getCleanupStrategy<T, NullCleanupStrategy> */ + +// out-of-class initialization required (because it's a non-integral type) +template <class T> +void (*const getCleanupStrategy<T, NullCleanupStrategy>::fn) + (typename getCleanupStrategy<T, NullCleanupStrategy>:: + mapping::table_value_type) = NULL; + +/** + * Specialization for ManagedAttributeCleanupStrategy<T>. + */ +template <class T> +struct getCleanupStrategy<T, ManagedAttributeCleanupStrategy<T> > { + typedef T value_type; + typedef KindValueToTableValueMapping<value_type> mapping; + static void (*const fn)(typename mapping::table_value_type); +};/* struct getCleanupStrategy<T, ManagedAttributeCleanupStrategy<T> > */ + +// out-of-class initialization required (because it's a non-integral type) +template <class T> +void (*const getCleanupStrategy<T, ManagedAttributeCleanupStrategy<T> >::fn) + (typename getCleanupStrategy<T, ManagedAttributeCleanupStrategy<T> >:: + mapping::table_value_type) = NULL; + +/** + * Specialization for ManagedAttributeCleanupStrategy<T*>. + */ +template <class T> +struct getCleanupStrategy<T*, ManagedAttributeCleanupStrategy<T*> > { + typedef T* value_type; + typedef ManagedAttributeCleanupStrategy<value_type> C; + typedef KindValueToTableValueMapping<value_type> mapping; + static void fn(typename mapping::table_value_type t) { + C::cleanup(mapping::convertBack(t)); + } +};/* struct getCleanupStrategy<T*, ManagedAttributeCleanupStrategy<T*> > */ + +/** + * Specialization for ManagedAttributeCleanupStrategy<const T*>. + */ +template <class T> +struct getCleanupStrategy<const T*, + ManagedAttributeCleanupStrategy<const T*> > { + typedef const T* value_type; + typedef ManagedAttributeCleanupStrategy<value_type> C; + typedef KindValueToTableValueMapping<value_type> mapping; + static void fn(typename mapping::table_value_type t) { + C::cleanup(mapping::convertBack(t)); + } +};/* struct getCleanupStrategy<const T*, + ManagedAttributeCleanupStrategy<const T*> > */ + +/** + * Cause compile-time error for improperly-instantiated + * getCleanupStrategy<>. + */ +template <class T, class U> +struct getCleanupStrategy<T, ManagedAttributeCleanupStrategy<U> >; + +}/* CVC4::expr::attr namespace */ + +// ATTRIBUTE IDENTIFIER ASSIGNMENT TEMPLATE ==================================== + +namespace attr { + +/** + * This is the last-attribute-assigner. IDs are not globally + * unique; rather, they are unique for each table_value_type. + */ +template <class T, bool context_dep> +struct LastAttributeId { + static uint64_t s_id; +}; + +/** Initially zero. */ +template <class T, bool context_dep> +uint64_t LastAttributeId<T, context_dep>::s_id = 0; + +}/* CVC4::expr::attr namespace */ + +// ATTRIBUTE TRAITS ============================================================ + +namespace attr { + +/** + * This is the last-attribute-assigner. IDs are not globally + * unique; rather, they are unique for each table_value_type. + */ +template <class T, bool context_dep> +struct AttributeTraits { + typedef void (*cleanup_t)(T); + static std::vector<cleanup_t> cleanup; +}; + +template <class T, bool context_dep> +std::vector<typename AttributeTraits<T, context_dep>::cleanup_t> + AttributeTraits<T, context_dep>::cleanup; + +}/* CVC4::expr::attr namespace */ + +// ATTRIBUTE DEFINITION ======================================================== + +/** + * An "attribute type" structure. + * + * @param T the tag for the attribute kind. + * + * @param value_t the underlying value_type for the attribute kind + * + * @param CleanupStrategy Clean-up routine for associated values when the + * Node goes away. Useful, e.g., for pointer-valued attributes when + * the values are "owned" by the table. + * + * @param context_dep whether this attribute kind is + * context-dependent + */ +template <class T, + class value_t, + class CleanupStrategy = attr::NullCleanupStrategy, + bool context_dep = false> +class Attribute { + /** + * The unique ID associated to this attribute. Assigned statically, + * at load time. + */ + static const uint64_t s_id; + +public: + + /** The value type for this attribute. */ + typedef value_t value_type; + + /** Get the unique ID associated to this attribute. */ + static inline uint64_t getId() { return s_id; } + + /** + * This attribute does not have a default value: calling + * hasAttribute() for a Node that hasn't had this attribute set will + * return false, and getAttribute() for the Node will return a + * default-constructed value_type. + */ + static const bool has_default_value = false; + + /** + * Expose this setting to the users of this Attribute kind. + */ + static const bool context_dependent = context_dep; + + /** + * Register this attribute kind and check that the ID is a valid ID + * for bool-valued attributes. Fail an assert if not. Otherwise + * return the id. + */ + static inline uint64_t registerAttribute() { + typedef typename attr::KindValueToTableValueMapping<value_t>:: + table_value_type table_value_type; + typedef attr::AttributeTraits<table_value_type, context_dep> traits; + uint64_t id = attr::LastAttributeId<table_value_type, context_dep>::s_id++; + Assert(traits::cleanup.size() == id);// sanity check + traits::cleanup.push_back(attr::getCleanupStrategy<value_t, + CleanupStrategy>::fn); + return id; + } +};/* class Attribute<> */ + +/** + * An "attribute type" structure for boolean flags (special). The + * full one is below; the existence of this one disallows for boolean + * flag attributes with a specialized cleanup function. + */ +/* -- doesn't work; other specialization is "more specific" ?? +template <class T, class CleanupStrategy, bool context_dep> +class Attribute<T, bool, CleanupStrategy, context_dep> { + template <bool> struct ERROR_bool_attributes_cannot_have_cleanup_functions; + ERROR_bool_attributes_cannot_have_cleanup_functions<true> blah; +}; +*/ + +/** + * An "attribute type" structure for boolean flags (special). + */ +template <class T, bool context_dep> +class Attribute<T, bool, attr::NullCleanupStrategy, context_dep> { + /** IDs for bool-valued attributes are actually bit assignments. */ + static const uint64_t s_id; + +public: + + /** The value type for this attribute; here, bool. */ + typedef bool value_type; + + /** Get the unique ID associated to this attribute. */ + static inline uint64_t getId() { return s_id; } + + /** + * Such bool-valued attributes ("flags") have a default value: they + * are false for all nodes on entry. Calling hasAttribute() for a + * Node that hasn't had this attribute set will return true, and + * getAttribute() for the Node will return the default_value below. + */ + static const bool has_default_value = true; + + /** + * Default value of the attribute for Nodes without one explicitly + * set. + */ + static const bool default_value = false; + + /** + * Expose this setting to the users of this Attribute kind. + */ + static const bool context_dependent = context_dep; + + /** + * Register this attribute kind and check that the ID is a valid ID + * for bool-valued attributes. Fail an assert if not. Otherwise + * return the id. + */ + static inline uint64_t registerAttribute() { + uint64_t id = attr::LastAttributeId<bool, context_dep>::s_id++; + AlwaysAssert( id <= 63, + "Too many boolean node attributes registered " + "during initialization !" ); + return id; + } +};/* class Attribute<..., bool, ...> */ + +/** + * This is a context-dependent attribute kind (the only difference + * between CDAttribute<> and Attribute<> (with the fourth argument + * "true") is that you cannot supply a cleanup function (a no-op one + * is used). + */ +template <class T, + class value_type> +struct CDAttribute : + public Attribute<T, value_type, attr::NullCleanupStrategy, true> {}; + +/** + * This is a managed attribute kind (the only difference between + * ManagedAttribute<> and Attribute<> is the default cleanup function + * and the fact that ManagedAttributes cannot be context-dependent). + * In the default ManagedAttribute cleanup function, the value is + * destroyed with the delete operator. If the value is allocated with + * the array version of new[], an alternate cleanup function should be + * provided that uses array delete[]. It is an error to create a + * ManagedAttribute<> kind with a non-pointer value_type if you don't + * also supply a custom cleanup function. + */ +template <class T, + class value_type, + class CleanupStrategy = + attr::ManagedAttributeCleanupStrategy<value_type> > +struct ManagedAttribute : + public Attribute<T, value_type, CleanupStrategy, false> {}; + +// ATTRIBUTE IDENTIFIER ASSIGNMENT ============================================= + +/** Assign unique IDs to attributes at load time. */ +// Use of the comma-operator here forces instantiation (and +// initialization) of the AttributeTraits<> structure and its +// "cleanup" vector before registerAttribute() is called. This is +// important because otherwise the vector is initialized later, +// clearing the first-pushed cleanup function. +template <class T, class value_t, class CleanupStrategy, bool context_dep> +const uint64_t Attribute<T, value_t, CleanupStrategy, context_dep>::s_id = + ( attr::AttributeTraits<typename attr::KindValueToTableValueMapping<value_t>:: + table_value_type, + context_dep>::cleanup.size(), + Attribute<T, value_t, CleanupStrategy, context_dep>::registerAttribute() ); + +/** Assign unique IDs to attributes at load time. */ +template <class T, bool context_dep> +const uint64_t Attribute<T, + bool, + attr::NullCleanupStrategy, context_dep>::s_id = + Attribute<T, bool, attr::NullCleanupStrategy, context_dep>:: + registerAttribute(); + +}/* CVC4::expr namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__EXPR__ATTRIBUTE_INTERNALS_H */ diff --git a/src/expr/builtin_kinds b/src/expr/builtin_kinds index bb224aa91..c4eb3af1c 100644 --- a/src/expr/builtin_kinds +++ b/src/expr/builtin_kinds @@ -17,10 +17,13 @@ # SKOLEM. # # operator K #children ["comment"] +# nonatomic_operator K #children ["comment"] # # Declares a "built-in" operator kind K. Really this is the same # as "variable" except that it has an operator (automatically -# generated by NodeManager). +# generated by NodeManager). These two commands are identical, +# except that kinds declared with nonatomic_operator answer false +# to Node::isAtomic(). # # You can specify an exact # of children required as the second # argument to the operator command. In debug mode, assertions are @@ -109,12 +112,11 @@ theory builtin # Conceptually, (EQUAL a b) is actually an (APPLY EQUAL a b), but it's # not stored that way. If you ask for the operator of (EQUAL a b), # you'll get a special, singleton (BUILTIN EQUAL) Node. -constant BUILTIN ::CVC4::Kind ::CVC4::kind::KindHashFcn \ +constant BUILTIN ::CVC4::Kind ::CVC4::kind::KindHashStrategy \ "expr/kind.h" "The kind of nodes representing built-in operators" operator EQUAL 2 "equality" operator DISTINCT 2: "disequality" -operator ITE 3 "if-then-else" variable SKOLEM "skolem var" variable VARIABLE "variable" operator TUPLE 2: "a tuple" diff --git a/src/expr/command.h b/src/expr/command.h index e5994b3c7..6a4bb67ed 100644 --- a/src/expr/command.h +++ b/src/expr/command.h @@ -16,6 +16,8 @@ ** client code. **/ +#include "cvc4_public.h" + #ifndef __CVC4__COMMAND_H #define __CVC4__COMMAND_H @@ -24,7 +26,6 @@ #include <string> #include <vector> -#include "cvc4_config.h" #include "expr/expr.h" #include "util/result.h" diff --git a/src/expr/expr_manager.cpp b/src/expr/expr_manager_template.cpp index 4eda9805a..2e25b4574 100644 --- a/src/expr/expr_manager.cpp +++ b/src/expr/expr_manager_template.cpp @@ -1,5 +1,5 @@ /********************* */ -/** expr_manager.cpp +/** expr_manager_template.cpp ** Original author: dejan ** Major contributors: cconway, mdeters ** Minor contributors (to current version): none @@ -10,23 +10,25 @@ ** See the file COPYING in the top-level source directory for licensing ** information. ** - ** [[ Add file-specific comments here ]] + ** Public-facing expression manager interface, implementation. **/ -/* - * expr_manager.cpp - * - * Created on: Dec 10, 2009 - * Author: dejan - */ - -#include "context/context.h" +#include "expr/node.h" #include "expr/expr.h" -#include "expr/expr_manager.h" #include "expr/kind.h" -#include "expr/node.h" -#include "expr/node_manager.h" +#include "expr/metakind.h" #include "expr/type.h" +#include "expr/node_manager.h" +#include "expr/expr_manager.h" +#include "context/context.h" + +${includes} + +// This is a hack, but an important one: if there's an error, the +// 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 32 "${template}" using namespace std; using namespace CVC4::context; @@ -122,15 +124,13 @@ FunctionType* ExprManager::mkFunctionType(const std::vector<Type*>& argTypes, return d_nodeManager->mkFunctionType(argTypes, range); } -FunctionType* -ExprManager::mkFunctionType(const std::vector<Type*>& sorts) { +FunctionType* ExprManager::mkFunctionType(const std::vector<Type*>& sorts) { Assert( sorts.size() >= 2 ); NodeManagerScope nms(d_nodeManager); return d_nodeManager->mkFunctionType(sorts); } -FunctionType* -ExprManager::mkPredicateType(const std::vector<Type*>& sorts) { +FunctionType* ExprManager::mkPredicateType(const std::vector<Type*>& sorts) { Assert( sorts.size() >= 1 ); NodeManagerScope nms(d_nodeManager); return d_nodeManager->mkPredicateType(sorts); @@ -151,11 +151,12 @@ Expr ExprManager::mkVar(Type* type) { return Expr(this, new Node(d_nodeManager->mkVar(type))); } -unsigned int ExprManager::minArity(Kind kind) { +unsigned ExprManager::minArity(Kind kind) { + // FIXME: should be implemented this way, but parser depends on *parse*-level. + // See bug 75. + //return metakind::getLowerBoundForKind(kind); switch(kind) { - case FALSE: case SKOLEM: - case TRUE: case VARIABLE: return 0; @@ -181,11 +182,12 @@ unsigned int ExprManager::minArity(Kind kind) { } } -unsigned int ExprManager::maxArity(Kind kind) { +unsigned ExprManager::maxArity(Kind kind) { + // FIXME: should be implemented this way, but parser depends on *parse*-level. + // See bug 75. + //return metakind::getUpperBoundForKind(kind); switch(kind) { - case FALSE: case SKOLEM: - case TRUE: case VARIABLE: return 0; @@ -213,7 +215,6 @@ unsigned int ExprManager::maxArity(Kind kind) { } } - NodeManager* ExprManager::getNodeManager() const { return d_nodeManager; } @@ -222,4 +223,6 @@ Context* ExprManager::getContext() const { return d_ctxt; } +${mkConst_implementations} + }/* CVC4 namespace */ diff --git a/src/expr/expr_manager.h b/src/expr/expr_manager_template.h index f2009ad80..523c12e3b 100644 --- a/src/expr/expr_manager.h +++ b/src/expr/expr_manager_template.h @@ -1,5 +1,5 @@ /********************* */ -/** expr_manager.h +/** expr_manager_template.h ** Original author: dejan ** Major contributors: cconway, mdeters ** Minor contributors (to current version): taking @@ -13,20 +13,27 @@ ** Public-facing expression manager interface. **/ +#include "cvc4_public.h" + #ifndef __CVC4__EXPR_MANAGER_H #define __CVC4__EXPR_MANAGER_H -#include "cvc4_config.h" -#include "expr/kind.h" #include <vector> +#include "expr/kind.h" +#include "expr/type.h" + +${includes} + +// This is a hack, but an important one: if there's an error, the +// 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 33 "${template}" + namespace CVC4 { class Expr; -class Type; -class BooleanType; -class FunctionType; -class KindType; class SmtEngine; class NodeManager; @@ -35,6 +42,33 @@ namespace context { }/* CVC4::context namespace */ class CVC4_PUBLIC ExprManager { +private: + /** The context */ + context::Context* d_ctxt; + + /** The internal node manager */ + NodeManager* d_nodeManager; + + /** + * Returns the internal node manager. This should only be used by + * internal users, i.e. the friend classes. + */ + NodeManager* getNodeManager() const; + + /** + * Returns the internal Context. Used by internal users, i.e. the + * friend classes. + */ + context::Context* getContext() const; + + /** + * SmtEngine will use all the internals, so it will grab the + * NodeManager. + */ + friend class SmtEngine; + + /** ExprManagerScope reaches in to get the NodeManager */ + friend class ExprManagerScope; public: @@ -65,7 +99,7 @@ public: /** * Make a unary expression of a given kind (NOT, BVNOT, ...). - * @param kind the kind of expression + * @param child1 kind the kind of expression * @return the expression */ Expr mkExpr(Kind kind, const Expr& child1); @@ -79,10 +113,39 @@ public: */ Expr mkExpr(Kind kind, const Expr& child1, const Expr& child2); + /** + * Make a 3-ary expression of a given kind (AND, PLUS, ...). + * @param kind the kind of expression + * @param child1 the first child of the new expression + * @param child2 the second child of the new expression + * @param child3 the third child of the new expression + * @return the expression + */ Expr mkExpr(Kind kind, const Expr& child1, const Expr& child2, const Expr& child3); + + /** + * Make a 4-ary expression of a given kind (AND, PLUS, ...). + * @param kind the kind of expression + * @param child1 the first child of the new expression + * @param child2 the second child of the new expression + * @param child3 the third child of the new expression + * @param child4 the fourth child of the new expression + * @return the expression + */ Expr mkExpr(Kind kind, const Expr& child1, const Expr& child2, const Expr& child3, const Expr& child4); + + /** + * Make a 5-ary expression of a given kind (AND, PLUS, ...). + * @param kind the kind of expression + * @param child1 the first child of the new expression + * @param child2 the second child of the new expression + * @param child3 the third child of the new expression + * @param child4 the fourth child of the new expression + * @param child5 the fifth child of the new expression + * @return the expression + */ Expr mkExpr(Kind kind, const Expr& child1, const Expr& child2, const Expr& child3, const Expr& child4, const Expr& child5); @@ -94,30 +157,36 @@ public: */ Expr mkExpr(Kind kind, const std::vector<Expr>& children); + /** Create a constant of type T */ + template <class T> + Expr mkConst(const T&); + /** Make a function type from domain to range. */ - FunctionType* - mkFunctionType(Type* domain, - Type* range); - - /** Make a function type with input types from argTypes. <code>argTypes</code> - * must have at least one element. */ - FunctionType* - mkFunctionType(const std::vector<Type*>& argTypes, - Type* range); - - /** Make a function type with input types from <code>sorts[0..sorts.size()-2]</code> - * and result type <code>sorts[sorts.size()-1]</code>. <code>sorts</code> must have at - * least 2 elements. + FunctionType* mkFunctionType(Type* domain, + Type* range); + + /** + * Make a function type with input types from argTypes. + * <code>argTypes</code> must have at least one element. */ - FunctionType* - mkFunctionType(const std::vector<Type*>& sorts); + FunctionType* mkFunctionType(const std::vector<Type*>& argTypes, + Type* range); - /** Make a predicate type with input types from <code>sorts</code>. The result with - * be a function type with range <code>BOOLEAN</code>. <code>sorts</code> must have at - * least one element. + /** + * Make a function type with input types from + * <code>sorts[0..sorts.size()-2]</code> and result type + * <code>sorts[sorts.size()-1]</code>. <code>sorts</code> must have + * at least 2 elements. */ - FunctionType* - mkPredicateType(const std::vector<Type*>& sorts); + FunctionType* mkFunctionType(const std::vector<Type*>& sorts); + + /** + * Make a predicate type with input types from + * <code>sorts</code>. The result with be a function type with range + * <code>BOOLEAN</code>. <code>sorts</code> must have at least one + * element. + */ + FunctionType* mkPredicateType(const std::vector<Type*>& sorts); /** Make a new sort with the given name. */ Type* mkSort(const std::string& name); @@ -127,41 +196,14 @@ public: Expr mkVar(Type* type); /** Returns the minimum arity of the given kind. */ - static unsigned int minArity(Kind kind); + static unsigned minArity(Kind kind); /** Returns the maximum arity of the given kind. */ - static unsigned int maxArity(Kind kind); - -private: - /** The context */ - context::Context* d_ctxt; - - /** The internal node manager */ - NodeManager* d_nodeManager; - - /** - * Returns the internal node manager. This should only be used by - * internal users, i.e. the friend classes. - */ - NodeManager* getNodeManager() const; - - /** - * Returns the internal Context. Used by internal users, i.e. the - * friend classes. - */ - context::Context* getContext() const; - - /** - * SmtEngine will use all the internals, so it will grab the - * NodeManager. - */ - friend class SmtEngine; - - /** ExprManagerScope reaches in to get the NodeManager */ - friend class ExprManagerScope; + static unsigned maxArity(Kind kind); }; +${mkConst_instantiations} + }/* CVC4 namespace */ #endif /* __CVC4__EXPR_MANAGER_H */ - diff --git a/src/expr/expr.cpp b/src/expr/expr_template.cpp index 2bcd28422..d02272320 100644 --- a/src/expr/expr.cpp +++ b/src/expr/expr_template.cpp @@ -1,5 +1,5 @@ /********************* */ -/** expr.cpp +/** expr_template.cpp ** Original author: dejan ** Major contributors: mdeters ** Minor contributors (to current version): taking @@ -10,7 +10,7 @@ ** See the file COPYING in the top-level source directory for licensing ** information. ** - ** [[ Add file-specific comments here ]] + ** Public-facing expression interface, implementation. **/ #include "expr/expr.h" @@ -19,6 +19,14 @@ #include "util/output.h" +${includes} + +// This is a hack, but an important one: if there's an error, the +// 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 29 "${template}" + using namespace CVC4::kind; namespace CVC4 { @@ -29,25 +37,25 @@ std::ostream& operator<<(std::ostream& out, const Expr& e) { } Expr::Expr() : - d_node(new Node()), d_exprManager(NULL) { + d_node(new Node), + d_exprManager(NULL) { } Expr::Expr(ExprManager* em, Node* node) : - d_node(node), d_exprManager(em) { + d_node(node), + d_exprManager(em) { } Expr::Expr(const Expr& e) : - d_node(new Node(*e.d_node)), d_exprManager(e.d_exprManager) { + d_node(new Node(*e.d_node)), + d_exprManager(e.d_exprManager) { } Expr::Expr(uintptr_t n) : - d_node(new Node()), - d_exprManager(NULL) { - AlwaysAssert(n==0); -} + d_node(new Node), + d_exprManager(NULL) { -ExprManager* Expr::getExprManager() const { - return d_exprManager; + AlwaysAssert(n == 0); } Expr::~Expr() { @@ -55,33 +63,37 @@ Expr::~Expr() { delete d_node; } +ExprManager* Expr::getExprManager() const { + return d_exprManager; +} + Expr& Expr::operator=(const Expr& e) { Assert(d_node != NULL, "Unexpected NULL expression pointer!"); Assert(e.d_node != NULL, "Unexpected NULL expression pointer!"); + ExprManagerScope ems(*this); *d_node = *e.d_node; d_exprManager = e.d_exprManager; + return *this; } /* This should only ever be assigning NULL to a null Expr! */ Expr& Expr::operator=(uintptr_t n) { - AlwaysAssert(n==0); + AlwaysAssert(n == 0); Assert(d_node != NULL, "Unexpected NULL expression pointer!"); - if( EXPECT_FALSE(!isNull()) ) { + + if(EXPECT_FALSE( !isNull() )) { *d_node = Node::null(); } return *this; -/* - Assert(isNull()); - return *this; -*/ } bool Expr::operator==(const Expr& e) const { if(d_exprManager != e.d_exprManager) { return false; } + ExprManagerScope ems(*this); Assert(d_node != NULL, "Unexpected NULL expression pointer!"); Assert(e.d_node != NULL, "Unexpected NULL expression pointer!"); return *d_node == *e.d_node; @@ -94,22 +106,39 @@ bool Expr::operator!=(const Expr& e) const { bool Expr::operator<(const Expr& e) const { Assert(d_node != NULL, "Unexpected NULL expression pointer!"); Assert(e.d_node != NULL, "Unexpected NULL expression pointer!"); - if(d_exprManager != e.d_exprManager) { - return false; + if(isNull() && !e.isNull()) { + return true; } + ExprManagerScope ems(*this); return *d_node < *e.d_node; } Kind Expr::getKind() const { + ExprManagerScope ems(*this); Assert(d_node != NULL, "Unexpected NULL expression pointer!"); return d_node->getKind(); } size_t Expr::getNumChildren() const { + ExprManagerScope ems(*this); Assert(d_node != NULL, "Unexpected NULL expression pointer!"); return d_node->getNumChildren(); } +bool Expr::hasOperator() const { + ExprManagerScope ems(*this); + Assert(d_node != NULL, "Unexpected NULL expression pointer!"); + return d_node->hasOperator(); +} + +Expr Expr::getOperator() const { + ExprManagerScope ems(*this); + Assert(d_node != NULL, "Unexpected NULL expression pointer!"); + CheckArgument(d_node->hasOperator(), + "Expr::getOperator() called on an Expr with no operator"); + return Expr(d_exprManager, new Node(d_node->getOperator())); +} + Type* Expr::getType() const { ExprManagerScope ems(*this); return d_node->getType(); @@ -122,6 +151,7 @@ std::string Expr::toString() const { } bool Expr::isNull() const { + ExprManagerScope ems(*this); Assert(d_node != NULL, "Unexpected NULL expression pointer!"); return d_node->isNull(); } @@ -130,6 +160,18 @@ Expr::operator bool() const { return !isNull(); } +bool Expr::isConst() const { + ExprManagerScope ems(*this); + Assert(d_node != NULL, "Unexpected NULL expression pointer!"); + return d_node->isConst(); +} + +bool Expr::isAtomic() const { + ExprManagerScope ems(*this); + Assert(d_node != NULL, "Unexpected NULL expression pointer!"); + return d_node->isAtomic(); +} + void Expr::toStream(std::ostream& out) const { ExprManagerScope ems(*this); d_node->toStream(out); @@ -207,5 +249,6 @@ void Expr::debugPrint() { #endif /* ! CVC4_MUZZLE */ } +${getConst_implementations} -} // End namespace CVC4 +}/* CVC4 namespace */ diff --git a/src/expr/expr.h b/src/expr/expr_template.h index 48b64fd17..12307e679 100644 --- a/src/expr/expr.h +++ b/src/expr/expr_template.h @@ -1,5 +1,5 @@ /********************* */ -/** expr.h +/** expr_template.h ** Original author: dejan ** Major contributors: none ** Minor contributors (to current version): taking, mdeters @@ -13,22 +13,30 @@ ** Public-facing expression interface. **/ +#include "cvc4_public.h" + // circular dependency: force expr_manager.h first #include "expr/expr_manager.h" #ifndef __CVC4__EXPR_H #define __CVC4__EXPR_H -#include "cvc4_config.h" - #include <string> #include <iostream> #include <stdint.h> +${includes} + +// This is a hack, but an important one: if there's an error, the +// 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 35 "${template}" + namespace CVC4 { // The internal expression representation -template <bool count_ref> +template <bool ref_count> class NodeTemplate; /** @@ -36,6 +44,20 @@ class NodeTemplate; * expressions. */ class CVC4_PUBLIC Expr { +protected: + + /** The internal expression representation */ + NodeTemplate<true>* d_node; + + /** The responsible expression manager */ + ExprManager* d_exprManager; + + /** + * Constructor for internal purposes. + * @param em the expression manager that handles this expression + * @param node the actual expression node pointer + */ + Expr(ExprManager* em, NodeTemplate<true>* node); public: @@ -44,7 +66,7 @@ public: /** * Copy constructor, makes a copy of a given expression - * @param the expression to copy + * @param e the expression to copy */ Expr(const Expr& e); @@ -68,7 +90,7 @@ public: */ Expr& operator=(const Expr& e); - /** + /* * Assignment from an integer. Fails if the integer is not 0. * NOTE: This is here purely to support the auto-initialization * behavior of the ANTLR3 C backend (i.e., a rule attribute @@ -104,11 +126,6 @@ public: bool operator<(const Expr& e) const; /** - * Returns true if the expression is not the null expression. - */ - operator bool() const; - - /** * Returns the kind of the expression (AND, PLUS ...). * @return the kind of the expression */ @@ -120,6 +137,19 @@ public: */ size_t getNumChildren() const; + /** + * Check if this is an expression that has an operator. + * @return true if this expression has an operator + */ + bool hasOperator() const; + + /** + * Get the operator of this expression. + * @throws IllegalArgumentException if it has no operator + * @return the operator of this expression + */ + Expr getOperator() const; + /** Returns the type of the expression, if it has been computed. * Returns NULL if the type of the expression is not known. */ @@ -133,7 +163,7 @@ public: /** * Outputs the string representation of the expression to the stream. - * @param the output stream + * @param out the output stream */ void toStream(std::ostream& out) const; @@ -144,6 +174,28 @@ public: bool isNull() const; /** + * Check if this is a null expression. + * @return true if NOT a null expression + */ + operator bool() const; + + /** + * Check if this is an expression representing a constant. + * @return true if a constant expression + */ + bool isConst() const; + + /** + * Check if this is an expression representing a constant. + * @return true if a constant expression + */ + bool isAtomic() const; + + /** Extract a constant of type T */ + template <class T> + const T& getConst() const; + + /** * Returns the expression reponsible for this expression. */ ExprManager* getExprManager() const; @@ -154,10 +206,10 @@ public: * @param out output stream to print to. * @param indent number of spaces to indent the formula by. */ - void printAst(std::ostream & out, int indent = 0) const; - + void printAst(std::ostream& out, int indent = 0) const; + private: - + /** * Pretty printer for use within gdb * This is not intended to be used outside of gdb. @@ -169,19 +221,6 @@ private: protected: /** - * Constructor for internal purposes. - * @param em the expression manager that handles this expression - * @param node the actual expression node pointer - */ - Expr(ExprManager* em, NodeTemplate<true>* node); - - /** The internal expression representation */ - NodeTemplate<true>* d_node; - - /** The responsible expression manager */ - ExprManager* d_exprManager; - - /** * Returns the actual internal node. * @return the internal node */ @@ -279,6 +318,8 @@ public: Expr iteExpr(const Expr& then_e, const Expr& else_e) const; }; -} +${getConst_instantiations} + +}/* CVC4 namespace */ #endif /* __CVC4__EXPR_H */ diff --git a/src/expr/kind_template.h b/src/expr/kind_template.h index 2b675be0f..96c34a02a 100644 --- a/src/expr/kind_template.h +++ b/src/expr/kind_template.h @@ -13,10 +13,11 @@ ** Template for the Node kind header. **/ +#include "cvc4_public.h" + #ifndef __CVC4__KIND_H #define __CVC4__KIND_H -#include "cvc4_config.h" #include <iostream> #include <sstream> @@ -62,9 +63,9 @@ inline std::string kindToString(::CVC4::Kind k) { return ss.str(); } -struct KindHashFcn { +struct KindHashStrategy { static inline size_t hash(::CVC4::Kind k) { return k; } -}; +};/* struct KindHashStrategy */ }/* CVC4::kind namespace */ }/* CVC4 namespace */ diff --git a/src/expr/metakind_template.h b/src/expr/metakind_template.h index 95e107313..052458cbe 100644 --- a/src/expr/metakind_template.h +++ b/src/expr/metakind_template.h @@ -123,6 +123,16 @@ ${metakind_kinds} return metaKinds[k]; }/* metaKindOf(k) */ +static inline bool kindIsAtomic(Kind k) { + static const bool isAtomic[] = { + false, /* NULL_EXPR */ +${metakind_isatomic} + false /* LAST_KIND */ + };/* isAtomic[] */ + + return isAtomic[k]; +}/* kindIsAtomic(k) */ + }/* CVC4::kind namespace */ namespace expr { diff --git a/src/expr/mkexpr b/src/expr/mkexpr new file mode 100755 index 000000000..de6de014d --- /dev/null +++ b/src/expr/mkexpr @@ -0,0 +1,177 @@ +#!/bin/bash +# +# mkexpr +# Morgan Deters <mdeters@cs.nyu.edu> for CVC4 +# Copyright (c) 2010 The CVC4 Project +# +# The purpose of this script is to create {expr,expr_manager}.{h,cpp} +# from template files and a list of theory kinds. Basically it just +# sets up the public interface for access to constants. +# +# Invocation: +# +# mkexpr template-file theory-kind-files... +# +# Output is to standard out. +# + +copyright=2010 + +filename=`basename "$1" | sed 's,_template,,'` + +cat <<EOF +/********************* */ +/** $filename + ** + ** Copyright $copyright The AcSys Group, New York University, and as below. + ** + ** This file automatically generated by: + ** + ** $0 $@ + ** + ** for the CVC4 project. + **/ + +EOF + +me=$(basename "$0") + +template=$1; shift + +includes= +getConst_instantiations= +getConst_implementations= +mkConst_instantiations= +mkConst_implementations= + +seen_theory=false +seen_theory_builtin=false + +function theory { + # theory T header + + lineno=${BASH_LINENO[0]} + + # this script doesn't care about the theory class information, but + # makes does make sure it's there + seen_theory=true + if [ "$1" = builtin ]; then + if $seen_theory_builtin; then + echo "$kf:$lineno: error: \"builtin\" theory redefined" >&2 + exit 1 + fi + seen_theory_builtin=true + elif [ -z "$1" -o -z "$2" ]; then + echo "$kf:$lineno: error: \"theory\" directive missing class or header argument" >&2 + exit 1 + elif ! expr "$1" : '\(::*\)' >/dev/null; then + echo "$kf:$lineno: warning: theory class \`$1' isn't fully-qualified (e.g., ::CVC4::theory::foo)" >&2 + elif ! expr "$1" : '\(::CVC4::theory::*\)' >/dev/null; then + echo "$kf:$lineno: warning: theory class not under ::CVC4::theory namespace" >&2 + fi +} + +function variable { + # variable K ["comment"] + + lineno=${BASH_LINENO[0]} + + check_theory_seen +} + +function operator { + # operator K #children ["comment"] + + lineno=${BASH_LINENO[0]} + + check_theory_seen +} + +function nonatomic_operator { + # nonatomic_operator K #children ["comment"] + + lineno=${BASH_LINENO[0]} + + check_theory_seen +} + +function parameterized { + # parameterized K #children ["comment"] + + lineno=${BASH_LINENO[0]} + + check_theory_seen +} + +function constant { + # constant K T Hasher header ["comment"] + + lineno=${BASH_LINENO[0]} + + check_theory_seen + + includes="${includes} +#include \"$4\"" + mkConst_instantiations="${mkConst_instantiations} +template <> +Expr ExprManager::mkConst($2 const& val); +" + mkConst_implementations="${mkConst_implementations} +template <> +Expr ExprManager::mkConst($2 const& val) { + return Expr(this, new Node(d_nodeManager->mkConst< $2 >(val))); +} +" + getConst_instantiations="${getConst_instantiations} +template <> +$2 const & Expr::getConst< $2 >() const; +" + getConst_implementations="${getConst_implementations} +template <> +$2 const & Expr::getConst() const { + return d_node->getConst< $2 >(); +} +" +} + +function check_theory_seen { + if ! $seen_theory; then + echo "$kf:$lineno: error: no \"theory\" declaration found (it has to be first)" >&2 + exit 1 + fi +} + +function check_builtin_theory_seen { + if ! $seen_theory_builtin; then + echo "$me: warning: no declaration for the builtin theory found" >&2 + fi +} + +while [ $# -gt 0 ]; do + kf=$1 + seen_theory=false + b=$(basename $(dirname "$kf")) + source "$kf" + check_theory_seen + shift +done +check_builtin_theory_seen + +## output + +text=$(cat "$template") +for var in \ + includes \ + template \ + getConst_instantiations \ + getConst_implementations \ + mkConst_instantiations \ + mkConst_implementations; do + eval text="\${text//\\\$\\{$var\\}/\${$var}}" +done +error=`expr "$text" : '.*\${\([^}]*\)}.*'` +if [ -n "$error" ]; then + echo "$template:0: error: undefined replacement \${$error}" >&2 + exit 1 +fi +echo "$text" diff --git a/src/expr/mkkind b/src/expr/mkkind index 6d75164d1..294dc5d7e 100755 --- a/src/expr/mkkind +++ b/src/expr/mkkind @@ -4,12 +4,12 @@ # Morgan Deters <mdeters@cs.nyu.edu> for CVC4 # Copyright (c) 2010 The CVC4 Project # -# The purpose of this script is to create kind.h from a prologue, -# middle section, epilogue, and a list of theory kinds. +# The purpose of this script is to create kind.h from a template and a +# list of theory kinds. # # Invocation: # -# mkkind prologue-file middle-file epilogue-file theory-kind-files... +# mkkind template-file theory-kind-files... # # Output is to standard out. # @@ -17,7 +17,7 @@ copyright=2010 cat <<EOF -/********************* -*- C++ -*- */ +/********************* */ /** kind.h ** ** Copyright $copyright The AcSys Group, New York University, and as below. @@ -83,6 +83,15 @@ function operator { register_kind "$1" "$2" "$3" } +function nonatomic_operator { + # nonatomic_operator K #children ["comment"] + + lineno=${BASH_LINENO[0]} + + check_theory_seen + register_kind "$1" "$2" "$3" +} + function parameterized { # parameterized K #children ["comment"] diff --git a/src/expr/mkmetakind b/src/expr/mkmetakind index 15551d54d..3884f636a 100755 --- a/src/expr/mkmetakind +++ b/src/expr/mkmetakind @@ -4,15 +4,15 @@ # Morgan Deters <mdeters@cs.nyu.edu> for CVC4 # Copyright (c) 2010 The CVC4 Project # -# The purpose of this script is to create metakind.h from a prologue, -# two middle sections, epilogue, and a list of theory kinds. +# The purpose of this script is to create metakind.h from a template +# and a list of theory kinds. # # This is kept distinct from kind.h because kind.h is a public header # and metakind.h is intended for the expr package only. # # Invocation: # -# mkmetakind prologue-file middle1-file middle2-file epilogue-file theory-kind-files... +# mkmetakind template-file theory-kind-files... # # Output is to standard out. # @@ -20,7 +20,7 @@ copyright=2010 cat <<EOF -/********************* -*- C++ -*- */ +/********************* */ /** metakind.h ** ** Copyright $copyright The AcSys Group, New York University, and as below. @@ -98,6 +98,15 @@ function operator { register_metakind OPERATOR "$1" "$2" } +function nonatomic_operator { + # nonatomic_operator K #children ["comment"] + + lineno=${BASH_LINENO[0]} + + check_theory_seen + register_metakind NONATOMIC_OPERATOR "$1" "$2" +} + function parameterized { # parameterized K #children ["comment"] @@ -115,7 +124,14 @@ function constant { check_theory_seen if ! expr "$2" : '\(::*\)' >/dev/null; then - echo "$kf:$lineno: warning: constant $1 class \`$2' isn't fully-qualified (e.g., ::CVC4::Rational)" >&2 + if ! primitive_type "$2"; then + # if there's an embedded space, we're probably doing something + # tricky to specify the CONST payload, like "int const*"; in any + # case, this warning gives too many false positives, so disable it + if ! expr "$2" : '..* ..*' >/dev/null; then + echo "$kf:$lineno: warning: constant $1 class \`$2' isn't fully-qualified (e.g., ::CVC4::Rational)" >&2 + fi + fi fi if ! expr "$3" : '\(::*\)' >/dev/null; then echo "$kf:$lineno: warning: constant $1 hasher \`$3' isn't fully-qualified (e.g., ::CVC4::RationalHashFcn)" >&2 @@ -133,14 +149,15 @@ function constant { namespace expr { template <> -inline const $2 & NodeValue::getConst< $2 >() const { - Assert(getKind() == ::CVC4::kind::$1); +inline $2 const& NodeValue::getConst< $2 >() const { + AssertArgument(getKind() == ::CVC4::kind::$1, *this, + \"Improper kind for getConst<$2>()\"); // To support non-inlined CONSTANT-kinded NodeValues (those that are // \"constructed\" when initially checking them against the NodeManager // pool), we must check d_nchildren here. return d_nchildren == 0 - ? *reinterpret_cast< const $2 * >(d_children) - : *reinterpret_cast< const $2 * >(d_children[0]); + ? *reinterpret_cast< $2 const* >(d_children) + : *reinterpret_cast< $2 const* >(d_children[0]); } }/* CVC4::expr namespace */ @@ -166,10 +183,12 @@ struct ConstantMapReverse< ::CVC4::kind::$1 > { " metakind_constHashes="${metakind_constHashes} case kind::$1: +#line $lineno \"$kf\" return $3::hash(nv->getConst< $2 >()); " metakind_constPrinters="${metakind_constPrinters} case kind::$1: +#line $lineno \"$kf\" out << nv->getConst< $2 >(); break; " @@ -179,17 +198,27 @@ function register_metakind { mk=$1 k=$2 nc=$3 + + if [ $mk = NONATOMIC_OPERATOR ]; then + metakind_isatomic="${metakind_isatomic} false, /* $k */ +"; + mk=OPERATOR + else + metakind_isatomic="${metakind_isatomic} true, /* $k */ +"; + fi + metakind_kinds="${metakind_kinds} metakind::$mk, /* $k */ "; # figure out the range given by $nc - if expr "$nc" : '^[0-9]\+$' >/dev/null; then + if expr "$nc" : '[0-9]\+$' >/dev/null; then lb=$nc ub=$nc - elif expr "$nc" : '^[0-9]\+:$' >/dev/null; then + elif expr "$nc" : '[0-9]\+:$' >/dev/null; then let `echo "$nc" | awk 'BEGIN{FS=":"}{print"lb="$1}'` ub=MAX_CHILDREN - elif expr "$nc" : '^[0-9]\+:[0-9]\+$' >/dev/null; then + elif expr "$nc" : '[0-9]\+:[0-9]\+$' >/dev/null; then let `echo "$nc" | awk 'BEGIN{FS=":"}{print"lb="$1" ub="$2}'` if [ $ub -lt $lb ]; then echo "$kf:$lineno: error in range \`$nc': LB < UB (in definition of $k)" >&2 @@ -200,12 +229,35 @@ function register_metakind { exit 1 fi + if [ $mk = OPERATOR -o $mk = PARAMETERIZED ]; then + if [ $lb = 0 ]; then + echo "$kf:$lineno: error in range \`$nc' for \`$k': $mk-kinded kinds must always take at least one child" >&2 + exit 1 + fi + fi + metakind_lbchildren="${metakind_lbchildren} $lb, /* $k */" metakind_ubchildren="${metakind_ubchildren} $ub, /* $k */" } +# Returns 0 if arg is a primitive C++ type, or a pointer to same; 1 +# otherwise. Really all this does is check whether we should issue a +# "not fully qualified" warning or not. +function primitive_type { + strip=`expr "$1" : ' *\(.*\)\* *'` + if [ -n "$strip" ]; then + primitive_type "$strip" >&2 + return $? + fi + + case "$1" in + bool|int|size_t|long|void|char|float|double) return 0;; + *) return 1;; + esac +} + function check_theory_seen { if ! $seen_theory; then echo "$kf:$lineno: error: no \"theory\" declaration found (it has to be first)" >&2 @@ -226,6 +278,9 @@ while [ $# -gt 0 ]; do metakind_kinds="${metakind_kinds} /* from $b */ " + metakind_isatomic="${metakind_isatomic} + /* from $b */ +" source "$kf" check_theory_seen shift @@ -235,9 +290,16 @@ check_builtin_theory_seen ## output text=$(cat "$template") -for var in metakind_includes metakind_kinds metakind_constantMaps \ - metakind_compares metakind_constHashes metakind_constPrinters \ - metakind_ubchildren metakind_lbchildren; do +for var in \ + metakind_includes \ + metakind_kinds \ + metakind_isatomic \ + metakind_constantMaps \ + metakind_compares \ + metakind_constHashes \ + metakind_constPrinters \ + metakind_ubchildren \ + metakind_lbchildren; do eval text="\${text//\\\$\\{$var\\}/\${$var}}" done error=`expr "$text" : '.*\${\([^}]*\)}.*'` diff --git a/src/expr/node.h b/src/expr/node.h index 343f03a1f..875760725 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -15,6 +15,7 @@ #include "cvc4_private.h" +// circular dependency #include "expr/node_value.h" #ifndef __CVC4__NODE_H @@ -25,11 +26,10 @@ #include <iostream> #include <stdint.h> -#include "cvc4_config.h" #include "expr/kind.h" +#include "expr/metakind.h" #include "expr/type.h" #include "util/Assert.h" - #include "util/output.h" namespace CVC4 { @@ -216,7 +216,15 @@ public: * Returns true if this node is atomic (has no more Boolean structure) * @return true if atomic */ - bool isAtomic() const; + inline bool isAtomic() const; + + /** + * Returns true if this node represents a constant + * @return true if const + */ + inline bool isConst() const { + return getMetaKind() == kind::metakind::CONSTANT; + } /** * Returns the unique id of this node @@ -578,23 +586,9 @@ setAttribute(const AttrKind&, const typename AttrKind::value_type& value) { template <bool ref_count> NodeTemplate<ref_count> NodeTemplate<ref_count>::s_null(&expr::NodeValue::s_null); -////FIXME: This function is a major hack! Should be changed ASAP -////TODO: Should use positive definition, i.e. what kinds are atomic. template <bool ref_count> bool NodeTemplate<ref_count>::isAtomic() const { - using namespace kind; - switch(getKind()) { - case NOT: - case XOR: - case ITE: - case IFF: - case IMPLIES: - case OR: - case AND: - return false; - default: - return true; - } + return kind::kindIsAtomic(getKind()); } // FIXME: escape from type system convenient but is there a better diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index f2718a06c..d17ec9497 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -293,24 +293,28 @@ public: /** Make a function type from domain to range. */ inline FunctionType* mkFunctionType(Type* domain, Type* range) const; - /** Make a function type with input types from argTypes. <code>argTypes</code> - * must have at least one element. */ + /** + * Make a function type with input types from + * argTypes. <code>argTypes</code> must have at least one element. + */ inline FunctionType* mkFunctionType(const std::vector<Type*>& argTypes, Type* range) const; - /** Make a function type with input types from <code>sorts[0..sorts.size()-2]</code> - * and result type <code>sorts[sorts.size()-1]</code>. <code>sorts</code> must have at - * least 2 elements. + /** + * Make a function type with input types from + * <code>sorts[0..sorts.size()-2]</code> and result type + * <code>sorts[sorts.size()-1]</code>. <code>sorts</code> must have + * at least 2 elements. */ - inline FunctionType* - mkFunctionType(const std::vector<Type*>& sorts); + inline FunctionType* mkFunctionType(const std::vector<Type*>& sorts) const; - /** Make a predicate type with input types from <code>sorts</code>. The result with - * be a function type with range <code>BOOLEAN</code>. <code>sorts</code> must have at - * least one element. + /** + * Make a predicate type with input types from + * <code>sorts</code>. The result with be a function type with range + * <code>BOOLEAN</code>. <code>sorts</code> must have at least one + * element. */ - inline FunctionType* - mkPredicateType(const std::vector<Type*>& sorts); + inline FunctionType* mkPredicateType(const std::vector<Type*>& sorts) const; /** Make a new sort with the given name. */ inline Type* mkSort(const std::string& name) const; @@ -453,7 +457,7 @@ NodeManager::mkFunctionType(const std::vector<Type*>& argTypes, } inline FunctionType* -NodeManager::mkFunctionType(const std::vector<Type*>& sorts) { +NodeManager::mkFunctionType(const std::vector<Type*>& sorts) const { Assert( sorts.size() >= 2 ); std::vector<Type*> argTypes(sorts); Type* rangeType = argTypes.back(); @@ -462,10 +466,11 @@ NodeManager::mkFunctionType(const std::vector<Type*>& sorts) { } inline FunctionType* -NodeManager::mkPredicateType(const std::vector<Type*>& sorts) { +NodeManager::mkPredicateType(const std::vector<Type*>& sorts) const { Assert( sorts.size() >= 1 ); return mkFunctionType(sorts,booleanType()); } + inline Type* NodeManager::mkSort(const std::string& name) const { return new SortType(name); } @@ -577,23 +582,6 @@ template <class T> Node NodeManager::mkConst(const T& val) { // typedef typename kind::metakind::constantMap<T>::OwningTheory theory_t; - // - // TODO: construct a special NodeValue that points to this T but - // is == an inlined version (like exists in the hash_set). - // - // Something similar for (a, b) and (a, b, c) and (a, b, c, d) - // versions. - // - // ALSO TODO: make poolLookup() use hash_set<>::operator[] to auto-insert, - // and then set = value after to avoid double-hashing. fix in all places - // where poolLookup is called. - // - // THEN ALSO TODO: CDMap<> destruction in attribute.cpp to make valgrind - // happy - // - // THEN: reconsider CVC3 tracing mechanism, experiments.. - // - NVStorage<1> nvStorage; expr::NodeValue& nvStack = reinterpret_cast<expr::NodeValue&>(nvStorage); diff --git a/src/expr/node_value.h b/src/expr/node_value.h index 7dd90913f..6408ef01a 100644 --- a/src/expr/node_value.h +++ b/src/expr/node_value.h @@ -25,10 +25,9 @@ #ifndef __CVC4__EXPR__NODE_VALUE_H #define __CVC4__EXPR__NODE_VALUE_H -#include "cvc4_config.h" #include "expr/kind.h" -#include <stdint.h> +#include <stdint.h> #include <string> #include <iterator> diff --git a/src/expr/type.h b/src/expr/type.h index b406bfd76..9e6596e84 100644 --- a/src/expr/type.h +++ b/src/expr/type.h @@ -13,10 +13,11 @@ ** Interface for expression types **/ +#include "cvc4_public.h" + #ifndef __CVC4__TYPE_H #define __CVC4__TYPE_H -#include "cvc4_config.h" #include "util/output.h" #include "util/Assert.h" @@ -262,7 +263,7 @@ struct TypeCleanupStrategy { delete t; } } -}; +};/* struct TypeCleanupStrategy */ }/* CVC4::expr::attr namespace */ }/* CVC4::expr namespace */ diff --git a/src/include/cvc4_private.h b/src/include/cvc4_private.h index df5dd4a0b..298bb14fb 100644 --- a/src/include/cvc4_private.h +++ b/src/include/cvc4_private.h @@ -21,4 +21,7 @@ # warning A private CVC4 header was included when not building the library or private unit test code. #endif /* ! (__BUILDING_CVC4LIB || __BUILDING_CVC4LIB_UNIT_TEST) */ +#include "cvc4_public.h" +#include "cvc4autoconfig.h" + #endif /* __CVC4_PRIVATE_H */ diff --git a/src/include/cvc4_config.h b/src/include/cvc4_public.h index 593e7a5e3..4de3faf4c 100644 --- a/src/include/cvc4_config.h +++ b/src/include/cvc4_public.h @@ -1,5 +1,5 @@ /********************* */ -/** cvc4_config.h +/** cvc4_public.h ** Original author: mdeters ** Major contributors: none ** Minor contributors (to current version): none @@ -11,11 +11,11 @@ ** information. ** ** Macros that should be defined everywhere during the building of - ** the libraries and driver binary. + ** the libraries and driver binary, and also exported to the user. **/ -#ifndef __CVC4_CONFIG_H -#define __CVC4_CONFIG_H +#ifndef __CVC4_PUBLIC_H +#define __CVC4_PUBLIC_H #if defined _WIN32 || defined __CYGWIN__ # ifdef BUILDING_DLL @@ -47,4 +47,4 @@ # define NULL ((void*) 0) #endif -#endif /* __CVC4_CONFIG_H */ +#endif /* __CVC4_PUBLIC_H */ diff --git a/src/include/cvc4parser_private.h b/src/include/cvc4parser_private.h index 72d942ef0..6704daca2 100644 --- a/src/include/cvc4parser_private.h +++ b/src/include/cvc4parser_private.h @@ -21,4 +21,7 @@ # warning A private CVC4 parser header was included when not building the parser library or private unit test code. #endif /* ! (__BUILDING_CVC4PARSERLIB || __BUILDING_CVC4PARSERLIB_UNIT_TEST) */ +#include "cvc4parser_public.h" +#include "cvc4autoconfig.h" + #endif /* __CVC4PARSER_PRIVATE_H */ diff --git a/src/main/getopt.cpp b/src/main/getopt.cpp index ad59e0039..b7474fa7e 100644 --- a/src/main/getopt.cpp +++ b/src/main/getopt.cpp @@ -23,15 +23,16 @@ #include <getopt.h> -#include "config.h" -#include "main.h" #include "util/exception.h" -#include "usage.h" #include "util/configuration.h" #include "util/output.h" #include "util/options.h" #include "parser/parser_options.h" +#include "cvc4autoconfig.h" +#include "main.h" +#include "usage.h" + using namespace std; using namespace CVC4; diff --git a/src/main/main.cpp b/src/main/main.cpp index b65d4f50a..c6899e85a 100644 --- a/src/main/main.cpp +++ b/src/main/main.cpp @@ -19,7 +19,7 @@ #include <cstring> #include <new> -#include "config.h" +#include "cvc4autoconfig.h" #include "main.h" #include "usage.h" #include "parser/input.h" diff --git a/src/main/main.h b/src/main/main.h index 405b22363..117b52c17 100644 --- a/src/main/main.h +++ b/src/main/main.h @@ -16,7 +16,7 @@ #include <exception> #include <string> -#include "config.h" +#include "cvc4autoconfig.h" #include "util/exception.h" #ifndef __CVC4__MAIN__MAIN_H diff --git a/src/main/util.cpp b/src/main/util.cpp index a2b46513d..6a69252ce 100644 --- a/src/main/util.cpp +++ b/src/main/util.cpp @@ -21,8 +21,8 @@ #include <signal.h> #include "util/exception.h" -#include "config.h" +#include "cvc4autoconfig.h" #include "main.h" using CVC4::Exception; diff --git a/src/parser/Makefile.am b/src/parser/Makefile.am index ee0a23c98..5d8b75f38 100644 --- a/src/parser/Makefile.am +++ b/src/parser/Makefile.am @@ -15,7 +15,7 @@ LIBCVC4PARSER_VERSION = @CVC4_PARSER_LIBRARY_VERSION@ AM_CPPFLAGS = \ -D__BUILDING_CVC4PARSERLIB \ -I@srcdir@/../include -I@srcdir@/.. $(ANTLR_INCLUDES) -AM_CXXFLAGS = -Wall -fvisibility=hidden -Wno-deprecated +AM_CXXFLAGS = -Wall -fvisibility=hidden SUBDIRS = smt cvc diff --git a/src/parser/antlr_input.cpp b/src/parser/antlr_input.cpp index 0c0006031..901735b1f 100644 --- a/src/parser/antlr_input.cpp +++ b/src/parser/antlr_input.cpp @@ -13,13 +13,6 @@ ** A super-class for ANTLR-generated input language parsers **/ -/* - * antlr_parser.cpp - * - * Created on: Nov 30, 2009 - * Author: dejan - */ - #include <iostream> #include <limits.h> #include <antlr3.h> diff --git a/src/parser/bounded_token_buffer.cpp b/src/parser/bounded_token_buffer.cpp index f53b6d548..1418e8f3c 100644 --- a/src/parser/bounded_token_buffer.cpp +++ b/src/parser/bounded_token_buffer.cpp @@ -35,8 +35,7 @@ #include <antlr3lexer.h> #include <antlr3tokenstream.h> -#include "bounded_token_buffer.h" -#include "cvc4_config.h" +#include "parser/bounded_token_buffer.h" #include "util/Assert.h" namespace CVC4 { diff --git a/src/parser/bounded_token_factory.cpp b/src/parser/bounded_token_factory.cpp index dae2f46e5..0209eb172 100644 --- a/src/parser/bounded_token_factory.cpp +++ b/src/parser/bounded_token_factory.cpp @@ -1,10 +1,3 @@ -/* - * bounded_token_factory.cpp - * - * Created on: Mar 2, 2010 - * Author: dejan - */ - #include <antlr3input.h> #include <antlr3commontoken.h> #include <antlr3interfaces.h> @@ -130,5 +123,6 @@ setInputStream (pANTLR3_TOKEN_FACTORY factory, pANTLR3_INPUT_STREAM input) factory->unTruc.strFactory = NULL; } } -} -} + +}/* CVC4::parser namespace */ +}/* CVC4 namespace */ diff --git a/src/parser/bounded_token_factory.h b/src/parser/bounded_token_factory.h index 6f8729c19..8f8177544 100644 --- a/src/parser/bounded_token_factory.h +++ b/src/parser/bounded_token_factory.h @@ -1,12 +1,7 @@ -/* - * bounded_token_factory.h - * - * Created on: Mar 2, 2010 - * Author: dejan - */ +#include "cvc4parser_private.h" -#ifndef BOUNDED_TOKEN_FACTORY_H_ -#define BOUNDED_TOKEN_FACTORY_H_ +#ifndef __CVC4__PARSER__BOUNDED_TOKEN_FACTORY_H +#define __CVC4__PARSER__BOUNDED_TOKEN_FACTORY_H namespace CVC4 { namespace parser { @@ -28,11 +23,10 @@ pANTLR3_TOKEN_FACTORY BoundedTokenFactoryNew(pANTLR3_INPUT_STREAM input,ANTLR3_UINT32 size); #ifdef __cplusplus -} +}/* extern "C" */ #endif -} -} - +}/* CVC4::parser namespace */ +}/* CVC4 namespace */ -#endif /* BOUNDED_TOKEN_FACTORY_H_ */ +#endif /* __CVC4__PARSER__BOUNDED_TOKEN_FACTORY_H */ diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index 4cb4d577b..d2ac81167 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -74,6 +74,8 @@ using namespace CVC4::parser; #define EXPR_MANAGER ANTLR_INPUT->getExprManager() #undef MK_EXPR #define MK_EXPR EXPR_MANAGER->mkExpr +#undef MK_CONST +#define MK_CONST EXPR_MANAGER->mkConst } /** @@ -105,7 +107,7 @@ command returns [CVC4::Command* cmd = 0] : ASSERT_TOK formula[f] SEMICOLON { cmd = new AssertCommand(f); } | QUERY_TOK formula[f] SEMICOLON { cmd = new QueryCommand(f); } | CHECKSAT_TOK formula[f] SEMICOLON { cmd = new CheckSatCommand(f); } - | CHECKSAT_TOK SEMICOLON { cmd = new CheckSatCommand(MK_EXPR(CVC4::kind::TRUE)); } + | CHECKSAT_TOK SEMICOLON { cmd = new CheckSatCommand(MK_CONST(true)); } | PUSH_TOK SEMICOLON { cmd = new PushCommand(); } | POP_TOK SEMICOLON { cmd = new PopCommand(); } | declaration[cmd] @@ -369,8 +371,8 @@ term[CVC4::Expr& f] LPAREN formula[f] RPAREN /* constants */ - | TRUE_TOK { f = MK_EXPR(CVC4::kind::TRUE); } - | FALSE_TOK { f = MK_EXPR(CVC4::kind::FALSE); } + | TRUE_TOK { f = MK_CONST(true); } + | FALSE_TOK { f = MK_CONST(false); } | /* variable */ identifier[name,CHECK_DECLARED,SYM_VARIABLE] diff --git a/src/parser/cvc/Makefile.am b/src/parser/cvc/Makefile.am index f02c9345c..ade8d83e7 100644 --- a/src/parser/cvc/Makefile.am +++ b/src/parser/cvc/Makefile.am @@ -2,8 +2,10 @@ AM_CPPFLAGS = \ -D__BUILDING_CVC4PARSERLIB \ -I@srcdir@/../../include -I@srcdir@/../.. $(ANTLR_INCLUDES) AM_CXXFLAGS = -Wall -fvisibility=hidden + # Compile generated C files using C++ compiler CC=$(CXX) +AM_CFLAGS = $(AM_CXXFLAGS) noinst_LTLIBRARIES = libparsercvc.la @@ -30,17 +32,17 @@ BUILT_SOURCES = $(ANTLR_STUFF) dist-hook: $(ANTLR_STUFF) MAINTAINERCLEANFILES = $(ANTLR_STUFF) maintainer-clean-local: - -rmdir @srcdir@/generated - -rm -f @srcdir@/stamp-generated + -$(AM_V_at)rmdir @srcdir@/generated + -$(AM_V_at)rm -f @srcdir@/stamp-generated @srcdir@/stamp-generated: - mkdir -p @srcdir@/generated - touch @srcdir@/stamp-generated + $(AM_V_at)mkdir -p @srcdir@/generated + $(AM_V_at)touch @srcdir@/stamp-generated # antlr doesn't overwrite output files, it just leaves them. So we have to delete them first. @srcdir@/generated/CvcLexer.h: Cvc.g @srcdir@/stamp-generated - -rm -f $(ANTLR_STUFF) - $(ANTLR) -o "@srcdir@/generated" "@srcdir@/Cvc.g" + -$(AM_V_at)rm -f $(ANTLR_STUFF) + $(AM_V_GEN)$(ANTLR) -o "@srcdir@/generated" "@srcdir@/Cvc.g" # These don't actually depend on CvcLexer.h, but if we're doing parallel # make and the lexer needs to be rebuilt, we have to keep the rules diff --git a/src/parser/cvc/cvc_input.cpp b/src/parser/cvc/cvc_input.cpp index 1f1a602c5..241ce62f3 100644 --- a/src/parser/cvc/cvc_input.cpp +++ b/src/parser/cvc/cvc_input.cpp @@ -1,10 +1,3 @@ -/* - * cvc_parser.cpp - * - * Created on: Mar 5, 2010 - * Author: chris - */ - #include <antlr3.h> #include "expr/expr_manager.h" @@ -69,6 +62,5 @@ pANTLR3_LEXER CvcInput::getLexer() { } */ -} // namespace parser - -} // namespace CVC4 +}/* CVC4::parser namespace */ +}/* CVC4 namespace */ diff --git a/src/parser/cvc/cvc_input.h b/src/parser/cvc/cvc_input.h index a6117b4a9..9908a25aa 100644 --- a/src/parser/cvc/cvc_input.h +++ b/src/parser/cvc/cvc_input.h @@ -1,12 +1,7 @@ -/* - * cvc_parser.h - * - * Created on: Mar 5, 2010 - * Author: chris - */ +#include "cvc4parser_public.h" -#ifndef CVC_PARSER_H_ -#define CVC_PARSER_H_ +#ifndef __CVC4__PARSER__CVC_INPUT_H +#define __CVC4__PARSER__CVC_INPUT_H #include "parser/antlr_input.h" #include "parser/cvc/generated/CvcLexer.h" @@ -76,8 +71,7 @@ private: }; // class CvcInput -} // namespace parser +}/* CVC4::parser namespace */ +}/* CVC4 namespace */ -} // namespace CVC4 - -#endif /* CVC_PARSER_H_ */ +#endif /* __CVC4__PARSER__CVC_INPUT_H */ diff --git a/src/parser/input.cpp b/src/parser/input.cpp index 01de4ea4f..0fd9a2628 100644 --- a/src/parser/input.cpp +++ b/src/parser/input.cpp @@ -1,5 +1,5 @@ /********************* */ -/** parser.cpp +/** input.cpp ** Original author: mdeters ** Major contributors: dejan ** Minor contributors (to current version): cconway diff --git a/src/parser/input.h b/src/parser/input.h index 90cdc4e8d..a255ede12 100644 --- a/src/parser/input.h +++ b/src/parser/input.h @@ -1,8 +1,8 @@ /********************* */ -/** parser.h - ** Original author: mdeters - ** Major contributors: dejan - ** Minor contributors (to current version): cconway +/** input.h + ** Original author: cconway + ** Major contributors: none + ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences @@ -13,13 +13,14 @@ ** Parser abstraction. **/ +#include "cvc4parser_public.h" + #ifndef __CVC4__PARSER__PARSER_H #define __CVC4__PARSER__PARSER_H #include <string> #include <iostream> -#include "cvc4_config.h" #include "expr/expr.h" #include "expr/kind.h" #include "parser/parser_exception.h" diff --git a/src/parser/memory_mapped_input_buffer.cpp b/src/parser/memory_mapped_input_buffer.cpp index 6618ecebc..f1a7b5729 100644 --- a/src/parser/memory_mapped_input_buffer.cpp +++ b/src/parser/memory_mapped_input_buffer.cpp @@ -1,10 +1,3 @@ -/* - * memory_mapped_input_buffer.cpp - * - * Created on: Mar 3, 2010 - * Author: chris - */ - #include <fcntl.h> #include <stdio.h> #include <stdint.h> @@ -14,7 +7,7 @@ #include <sys/stat.h> #include <antlr3input.h> -#include "memory_mapped_input_buffer.h" +#include "parser/memory_mapped_input_buffer.h" #include "util/Assert.h" #include "util/exception.h" diff --git a/src/parser/memory_mapped_input_buffer.h b/src/parser/memory_mapped_input_buffer.h index 88ba2183a..4146eec02 100644 --- a/src/parser/memory_mapped_input_buffer.h +++ b/src/parser/memory_mapped_input_buffer.h @@ -1,6 +1,8 @@ /********************* */ -/** memory_mapped_input_buffer.cpp +/** memory_mapped_input_buffer.h ** Original author: cconway + ** Major contributors: none + ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences @@ -11,6 +13,8 @@ ** ANTLR input buffer from a memory-mapped file. **/ +#include "cvc4parser_private.h" + #ifndef __CVC4__PARSER__MEMORY_MAPPED_INPUT_BUFFER_H #define __CVC4__PARSER__MEMORY_MAPPED_INPUT_BUFFER_H @@ -20,15 +24,18 @@ namespace CVC4 { namespace parser { +#ifdef __cplusplus extern "C" { +#endif pANTLR3_INPUT_STREAM MemoryMappedInputBufferNew(const std::string& filename); -} - -} -} +#ifdef __cplusplus +}/* extern "C" */ +#endif +}/* CVC4::parser namespace */ +}/* CVC4 namespace */ #endif /* __CVC4__PARSER__MEMORY_MAPPED_INPUT_BUFFER_H */ diff --git a/src/parser/parser_exception.h b/src/parser/parser_exception.h index ee02289ee..9bbe7d709 100644 --- a/src/parser/parser_exception.h +++ b/src/parser/parser_exception.h @@ -13,15 +13,17 @@ ** Exception class for parse errors. **/ +#include "cvc4parser_public.h" + #ifndef __CVC4__PARSER__PARSER_EXCEPTION_H #define __CVC4__PARSER__PARSER_EXCEPTION_H -#include "util/exception.h" -#include "cvc4_config.h" #include <iostream> #include <string> #include <sstream> +#include "util/exception.h" + namespace CVC4 { namespace parser { diff --git a/src/parser/parser_options.h b/src/parser/parser_options.h index ddba219a4..ae1d99542 100644 --- a/src/parser/parser_options.h +++ b/src/parser/parser_options.h @@ -1,27 +1,22 @@ -/* - * parser_options.h - * - * Created on: Mar 3, 2010 - * Author: chris - */ +#include "cvc4_public.h" -#ifndef CVC4__PARSER__PARSER_OPTIONS_H_ -#define CVC4__PARSER__PARSER_OPTIONS_H_ +#ifndef __CVC4__PARSER__PARSER_OPTIONS_H +#define __CVC4__PARSER__PARSER_OPTIONS_H namespace CVC4 { namespace parser { - /** The input language option */ - enum InputLanguage { - /** The SMTLIB input language */ - LANG_SMTLIB, - /** The CVC4 input language */ - LANG_CVC4, - /** Auto-detect the language */ - LANG_AUTO - }; +/** The input language option */ +enum InputLanguage { + /** The SMTLIB input language */ + LANG_SMTLIB, + /** The CVC4 input language */ + LANG_CVC4, + /** Auto-detect the language */ + LANG_AUTO +};/* enum InputLanguage */ -} -} +}/* CVC4::parser namespace */ +}/* CVC4 namespace */ -#endif /* CVC4__PARSER__PARSER_OPTIONS_H_ */ +#endif /* __CVC4__PARSER__PARSER_OPTIONS_H */ diff --git a/src/parser/smt/Makefile.am b/src/parser/smt/Makefile.am index 3ea6dc940..f081f493f 100644 --- a/src/parser/smt/Makefile.am +++ b/src/parser/smt/Makefile.am @@ -2,7 +2,9 @@ AM_CPPFLAGS = \ -D__BUILDING_CVC4PARSERLIB \ -I@srcdir@/../../include -I@srcdir@/../.. $(ANTLR_INCLUDES) AM_CXXFLAGS = -Wall -fvisibility=hidden + # Compile generated C files using C++ compiler +AM_CFLAGS = $(AM_CXXFLAGS) CC=$(CXX) noinst_LTLIBRARIES = libparsersmt.la @@ -30,17 +32,17 @@ BUILT_SOURCES = $(ANTLR_STUFF) dist-hook: $(ANTLR_STUFF) MAINTAINERCLEANFILES = $(ANTLR_STUFF) maintainer-clean-local: - -rmdir @srcdir@/generated - -rm -f @srcdir@/stamp-generated + -$(AM_V_at)rmdir @srcdir@/generated + -$(AM_V_at)rm -f @srcdir@/stamp-generated @srcdir@/stamp-generated: - mkdir -p @srcdir@/generated - touch @srcdir@/stamp-generated + $(AM_V_at)mkdir -p @srcdir@/generated + $(AM_V_at)touch @srcdir@/stamp-generated # antlr doesn't overwrite output files, it just leaves them. So we have to delete them first. @srcdir@/generated/SmtLexer.h: Smt.g @srcdir@/stamp-generated - -rm -f $(ANTLR_STUFF) - $(ANTLR) -o "@srcdir@/generated" "@srcdir@/Smt.g" + -$(AM_V_at)rm -f $(ANTLR_STUFF) + $(AM_V_GEN)$(ANTLR) -o "@srcdir@/generated" "@srcdir@/Smt.g" # These don't actually depend on SmtLexer.h, but if we're doing parallel # make and the lexer needs to be rebuilt, we have to keep the rules diff --git a/src/parser/smt/Smt.g b/src/parser/smt/Smt.g index 789e01670..48a0eddef 100644 --- a/src/parser/smt/Smt.g +++ b/src/parser/smt/Smt.g @@ -74,6 +74,8 @@ using namespace CVC4::parser; #define EXPR_MANAGER ANTLR_INPUT->getExprManager() #undef MK_EXPR #define MK_EXPR EXPR_MANAGER->mkExpr +#undef MK_CONST +#define MK_CONST EXPR_MANAGER->mkConst } /** @@ -206,8 +208,8 @@ annotatedFormula[CVC4::Expr& expr] { expr = ANTLR_INPUT->getVariable(name); } /* constants */ - | TRUE_TOK { expr = MK_EXPR(CVC4::kind::TRUE); } - | FALSE_TOK { expr = MK_EXPR(CVC4::kind::FALSE); } + | TRUE_TOK { expr = MK_CONST(true); } + | FALSE_TOK { expr = MK_CONST(false); } /* TODO: let, flet, quantifiers, arithmetic constants */ ; diff --git a/src/parser/smt/smt_input.cpp b/src/parser/smt/smt_input.cpp index db4d89860..cd62eec39 100644 --- a/src/parser/smt/smt_input.cpp +++ b/src/parser/smt/smt_input.cpp @@ -1,10 +1,3 @@ -/* - * smt_parser.cpp - * - * Created on: Mar 5, 2010 - * Author: chris - */ - #include <antlr3.h> #include "expr/expr_manager.h" @@ -65,6 +58,5 @@ Expr SmtInput::doParseExpr() throw (ParserException) { return d_pSmtParser->parseExpr(d_pSmtParser); } -} // namespace parser - -} // namespace CVC4 +}/* CVC4::parser namespace */ +}/* CVC4 namespace */ diff --git a/src/parser/smt/smt_input.h b/src/parser/smt/smt_input.h index 4795edc91..3e295d18a 100644 --- a/src/parser/smt/smt_input.h +++ b/src/parser/smt/smt_input.h @@ -1,12 +1,7 @@ -/* - * smt_parser.h - * - * Created on: Mar 5, 2010 - * Author: chris - */ +#include "cvc4parser_public.h" -#ifndef SMT_PARSER_H_ -#define SMT_PARSER_H_ +#ifndef __CVC4__PARSER__SMT_INPUT_H +#define __CVC4__PARSER__SMT_INPUT_H #include "parser/antlr_input.h" #include "parser/smt/generated/SmtLexer.h" @@ -32,7 +27,8 @@ class SmtInput : public AntlrInput { public: - /** Create a file input. + /** + * Create a file input. * * @param exprManager the manager to use when building expressions from the input * @param filename the path of the file to read @@ -41,7 +37,8 @@ public: */ SmtInput(ExprManager* exprManager, const std::string& filename, bool useMmap); - /** Create a string input. + /** + * Create a string input. * * @param exprManager the manager to use when building expressions from the input * @param input the string to read @@ -49,20 +46,22 @@ public: */ SmtInput(ExprManager* exprManager, const std::string& input, const std::string& name); - /* Destructor. Frees the lexer and the parser. */ + /** Destructor. Frees the lexer and the parser. */ ~SmtInput(); protected: - /** Parse a command from the input. Returns <code>NULL</code> if there is - * no command there to parse. + /** + * Parse a command from the input. Returns <code>NULL</code> if + * there is no command there to parse. * * @throws ParserException if an error is encountered during parsing. */ Command* doParseCommand() throw(ParserException); - /** Parse an expression from the input. Returns a null <code>Expr</code> - * if there is no expression there to parse. + /** + * Parse an expression from the input. Returns a null + * <code>Expr</code> if there is no expression there to parse. * * @throws ParserException if an error is encountered during parsing. */ @@ -70,14 +69,15 @@ protected: private: - /** Initialize the class. Called from the constructors once the input stream - * is initialized. */ + /** + * Initialize the class. Called from the constructors once the input + * stream is initialized. + */ void init(); -}; // class SmtInput - -} // namespace parser +};/* class SmtInput */ -} // namespace CVC4 +}/* CVC4::parser namespace */ +}/* CVC4 namespace */ -#endif /* SMT_PARSER_H_ */ +#endif /* __CVC4__PARSER__SMT_INPUT_H */ diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp index 44768009e..611689c2b 100644 --- a/src/prop/cnf_stream.cpp +++ b/src/prop/cnf_stream.cpp @@ -113,15 +113,12 @@ SatLiteral TseitinCnfStream::handleAtom(TNode node) { bool theoryLiteral = node.getKind() != kind::VARIABLE; SatLiteral lit = newLiteral(node, theoryLiteral); - switch(node.getKind()) { - case TRUE: - assertClause(lit); - break; - case FALSE: - assertClause(~lit); - break; - default: - break; + if(node.getKind() == kind::CONST_BOOLEAN) { + if(node.getConst<bool>()) { + assertClause(lit); + } else { + assertClause(~lit); + } } return lit; diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h index 131999e38..bf2018338 100644 --- a/src/prop/minisat/core/Solver.h +++ b/src/prop/minisat/core/Solver.h @@ -17,16 +17,16 @@ DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. **************************************************************************************************/ +#include "cvc4_private.h" + #ifndef __CVC4__PROP__MINISAT__SOLVER_H #define __CVC4__PROP__MINISAT__SOLVER_H -#include "cvc4_private.h" #include "context/context.h" #include <cstdio> #include <cassert> -#include "cvc4_config.h" #include "../mtl/Vec.h" #include "../mtl/Heap.h" #include "../mtl/Alg.h" diff --git a/src/prop/minisat/mtl/Alg.h b/src/prop/minisat/mtl/Alg.h index 0fe6d84c7..e636f2b87 100644 --- a/src/prop/minisat/mtl/Alg.h +++ b/src/prop/minisat/mtl/Alg.h @@ -17,6 +17,8 @@ DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. **************************************************************************************************/ +#include "cvc4_private.h" + #ifndef CVC4_MiniSat_Alg_h #define CVC4_MiniSat_Alg_h diff --git a/src/prop/minisat/mtl/BasicHeap.h b/src/prop/minisat/mtl/BasicHeap.h index 39d825411..cb6a7cbd8 100644 --- a/src/prop/minisat/mtl/BasicHeap.h +++ b/src/prop/minisat/mtl/BasicHeap.h @@ -17,6 +17,8 @@ DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. **************************************************************************************************/ +#include "cvc4_private.h" + #ifndef CVC4_MiniSat_BasicHeap_h #define CVC4_MiniSat_BasicHeap_h diff --git a/src/prop/minisat/mtl/BoxedVec.h b/src/prop/minisat/mtl/BoxedVec.h index 05b801004..7cf5ba14f 100644 --- a/src/prop/minisat/mtl/BoxedVec.h +++ b/src/prop/minisat/mtl/BoxedVec.h @@ -17,6 +17,8 @@ DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. **************************************************************************************************/ +#include "cvc4_private.h" + #ifndef CVC4_MiniSat_BoxedVec_h #define CVC4_MiniSat_BoxedVec_h diff --git a/src/prop/minisat/mtl/Heap.h b/src/prop/minisat/mtl/Heap.h index 0c2019b65..20d379b1d 100644 --- a/src/prop/minisat/mtl/Heap.h +++ b/src/prop/minisat/mtl/Heap.h @@ -17,6 +17,8 @@ DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. **************************************************************************************************/ +#include "cvc4_private.h" + #ifndef CVC4_MiniSat_Heap_h #define CVC4_MiniSat_Heap_h diff --git a/src/prop/minisat/mtl/Map.h b/src/prop/minisat/mtl/Map.h index 9168dde0e..715b84da4 100644 --- a/src/prop/minisat/mtl/Map.h +++ b/src/prop/minisat/mtl/Map.h @@ -17,6 +17,8 @@ DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. **************************************************************************************************/ +#include "cvc4_private.h" + #ifndef CVC4_MiniSat_Map_h #define CVC4_MiniSat_Map_h diff --git a/src/prop/minisat/mtl/Queue.h b/src/prop/minisat/mtl/Queue.h index e02ac7222..291a1f2e3 100644 --- a/src/prop/minisat/mtl/Queue.h +++ b/src/prop/minisat/mtl/Queue.h @@ -17,6 +17,8 @@ DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. **************************************************************************************************/ +#include "cvc4_private.h" + #ifndef CVC4_MiniSat_Queue_h #define CVC4_MiniSat_Queue_h diff --git a/src/prop/minisat/mtl/Sort.h b/src/prop/minisat/mtl/Sort.h index 2b9d5bb15..19e89803b 100644 --- a/src/prop/minisat/mtl/Sort.h +++ b/src/prop/minisat/mtl/Sort.h @@ -17,6 +17,8 @@ DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. **************************************************************************************************/ +#include "cvc4_private.h" + #ifndef CVC4_MiniSat_Sort_h #define CVC4_MiniSat_Sort_h diff --git a/src/prop/minisat/mtl/Vec.h b/src/prop/minisat/mtl/Vec.h index fae1d0c5d..364991aa9 100644 --- a/src/prop/minisat/mtl/Vec.h +++ b/src/prop/minisat/mtl/Vec.h @@ -17,6 +17,8 @@ DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. **************************************************************************************************/ +#include "cvc4_private.h" + #ifndef CVC4_MiniSat_Vec_h #define CVC4_MiniSat_Vec_h diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h index d699153b2..36f6cb0cb 100644 --- a/src/prop/prop_engine.h +++ b/src/prop/prop_engine.h @@ -19,7 +19,6 @@ #ifndef __CVC4__PROP_ENGINE_H #define __CVC4__PROP_ENGINE_H -#include "cvc4_config.h" #include "expr/node.h" #include "util/result.h" #include "util/options.h" diff --git a/src/prop/sat.h b/src/prop/sat.h index 93e95eedf..207ed90fd 100644 --- a/src/prop/sat.h +++ b/src/prop/sat.h @@ -13,11 +13,11 @@ ** SAT Solver. **/ +#include "cvc4_private.h" + #ifndef __CVC4__PROP__SAT_H #define __CVC4__PROP__SAT_H -#include "cvc4_private.h" - #define __CVC4_USE_MINISAT #ifdef __CVC4_USE_MINISAT diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 4836b282e..cca765b84 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -13,12 +13,13 @@ ** SmtEngine: the main public entry point of libcvc4. **/ +#include "cvc4_public.h" + #ifndef __CVC4__SMT_ENGINE_H #define __CVC4__SMT_ENGINE_H #include <vector> -#include "cvc4_config.h" #include "expr/expr.h" #include "expr/expr_manager.h" #include "util/result.h" diff --git a/src/theory/Makefile.am b/src/theory/Makefile.am index 32ea1d2be..2891e64cf 100644 --- a/src/theory/Makefile.am +++ b/src/theory/Makefile.am @@ -23,12 +23,13 @@ EXTRA_DIST = \ @srcdir@/theoryof_table.h \ theoryof_table_template.h -@srcdir@/theoryof_table.h: @srcdir@/mktheoryof theoryof_table_template.h @top_srcdir@/src/theory/Makefile.in @top_srcdir@/src/theory/*/kinds +@srcdir@/theoryof_table.h: theoryof_table_template.h mktheoryof @top_srcdir@/src/theory/Makefile.in @top_srcdir@/src/theory/*/kinds $(AM_V_at)chmod +x @srcdir@/mktheoryof + $(AM_V_at)mv -f $@ $@~ 2>/dev/null || true $(AM_V_GEN)(@srcdir@/mktheoryof \ - @srcdir@/theoryof_table_template.h \ + $< \ `grep '^SUBDIRS = ' @top_srcdir@/src/theory/Makefile.in | cut -d' ' -f3- | tr ' ' "\n" | xargs -i__D__ echo @top_srcdir@/src/theory/__D__/kinds` \ - > @srcdir@/theoryof_table.h) || (rm -f @srcdir@/theoryof_table.h && exit 1) + > $@) || (rm -f $@ && exit 1) BUILT_SOURCES = @srcdir@/theoryof_table.h dist-hook: @srcdir@/theoryof_table.h diff --git a/src/theory/arith/kinds b/src/theory/arith/kinds index 2f2c77d36..3b79192d2 100644 --- a/src/theory/arith/kinds +++ b/src/theory/arith/kinds @@ -10,16 +10,14 @@ operator PLUS 2: "arithmetic addition" operator MULT 2: "arithmetic multiplication" operator UMINUS 1 "arithmetic negation" -constant \ - CONST_RATIONAL \ +constant CONST_RATIONAL \ ::CVC4::Rational \ - ::CVC4::RationalHashFcn \ + ::CVC4::RationalHashStrategy \ "util/rational.h" \ "a multiple-precision rational constant" -constant \ - CONST_INTEGER \ +constant CONST_INTEGER \ ::CVC4::Integer \ - ::CVC4::IntegerHashFcn \ + ::CVC4::IntegerHashStrategy \ "util/integer.h" \ "a multiple-precision integer constant" diff --git a/src/theory/booleans/kinds b/src/theory/booleans/kinds index 12869aad0..5fcf9299a 100644 --- a/src/theory/booleans/kinds +++ b/src/theory/booleans/kinds @@ -6,12 +6,18 @@ theory ::CVC4::theory::booleans::TheoryBool "theory_bool.h" -operator FALSE 0 "falsity" -operator TRUE 0 "truth" +constant CONST_BOOLEAN \ + bool \ + ::CVC4::BoolHashStrategy \ + "util/bool.h" \ + "truth and falsity" -operator NOT 1 "logical not" -operator AND 2: "logical and" -operator IFF 2 "logical equivalence" -operator IMPLIES 2 "logical implication" -operator OR 2: "logical or" -operator XOR 2: "exclusive or" +# these are nonatomic because they have boolean structure. +# i.e. nodes n with this kind return false for n.isAtomic() +nonatomic_operator NOT 1 "logical not" +nonatomic_operator AND 2: "logical and" +nonatomic_operator IFF 2 "logical equivalence" +nonatomic_operator IMPLIES 2 "logical implication" +nonatomic_operator OR 2: "logical or" +nonatomic_operator XOR 2: "exclusive or" +nonatomic_operator ITE 3 "if-then-else" diff --git a/src/theory/mktheoryof b/src/theory/mktheoryof index ef967342b..842e02a07 100755 --- a/src/theory/mktheoryof +++ b/src/theory/mktheoryof @@ -5,11 +5,11 @@ # Copyright (c) 2010 The CVC4 Project # # The purpose of this script is to create theoryof_table.h from a -# prologue, epilogue, and a list of theory kinds. +# template and a list of theory kinds. # # Invocation: # -# mktheoryof prologue-file epilogue-file theory-kind-files... +# mktheoryof template-file theory-kind-files... # # Output is to standard out. # @@ -17,7 +17,7 @@ copyright=2010 cat <<EOF -/********************* -*- C++ -*- */ +/********************* */ /** theoryof_table.h ** ** Copyright $copyright The AcSys Group, New York University, and as below. @@ -84,6 +84,14 @@ function operator { do_theoryof "$1" } +function nonatomic_operator { + # nonatomic_operator K #children ["comment"] + + lineno=${BASH_LINENO[0]} + + do_theoryof "$1" +} + function parameterized { # parameterized K #children ["comment"] diff --git a/src/theory/theory.h b/src/theory/theory.h index 42bdaf2dd..4c3a43061 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -36,7 +36,7 @@ namespace theory { // rewrite cache support struct RewriteCacheTag {}; -typedef expr::Attribute<RewriteCacheTag, Node> RewriteCache; +typedef expr::Attribute<RewriteCacheTag, TNode> RewriteCache; template <class T> class TheoryImpl; diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index f953f97b9..d29195011 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -111,7 +111,7 @@ Node TheoryEngine::rewrite(TNode in) { if(in.getKind() == kind::EQUAL) { Assert(in.getNumChildren() == 2); if(in[0] == in[1]) { - Node out = NodeManager::currentNM()->mkNode(kind::TRUE); + Node out = NodeManager::currentNM()->mkConst(true); //setRewriteCache(in, out); return out; } diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index b8c2d5a75..1d5daf7bd 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -129,6 +129,10 @@ class TheoryEngine { * while leaving the Node's kind alone. */ Node rewriteChildren(TNode in) { + if(in.getMetaKind() == kind::metakind::CONSTANT) { + return in; + } + NodeBuilder<> b(in.getKind()); for(TNode::iterator c = in.begin(); c != in.end(); ++c) { b << rewrite(*c); diff --git a/src/util/Assert.cpp b/src/util/Assert.cpp index f992032ee..06be4ab7c 100644 --- a/src/util/Assert.cpp +++ b/src/util/Assert.cpp @@ -16,10 +16,9 @@ #include <new> #include <cstdarg> #include <cstdio> + #include "util/Assert.h" #include "util/exception.h" -#include "cvc4_config.h" -#include "config.h" using namespace std; diff --git a/src/util/Assert.h b/src/util/Assert.h index ad3f4b1d3..744782ba2 100644 --- a/src/util/Assert.h +++ b/src/util/Assert.h @@ -13,6 +13,8 @@ ** Assertion utility classes, functions, exceptions, and macros. **/ +#include "cvc4_public.h" + #ifndef __CVC4__ASSERT_H #define __CVC4__ASSERT_H @@ -22,8 +24,6 @@ #include <cstdlib> #include <cstdarg> -#include "config.h" -#include "cvc4_config.h" #include "util/exception.h" #include "util/output.h" diff --git a/src/util/Makefile.am b/src/util/Makefile.am index f6f8323be..5e8dfd2a4 100644 --- a/src/util/Makefile.am +++ b/src/util/Makefile.am @@ -20,7 +20,8 @@ libutil_la_SOURCES = \ output.h \ result.h \ unique_id.h \ - configuration.ha \ + configuration.h \ + configuration.cpp \ rational.h \ rational.cpp \ integer.h \ diff --git a/src/util/bool.h b/src/util/bool.h new file mode 100644 index 000000000..edd45b8a0 --- /dev/null +++ b/src/util/bool.h @@ -0,0 +1,37 @@ +/********************* */ +/** bool.h + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010 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. + ** + ** A multiprecision rational constant. + ** This stores the rational as a pair of multiprecision integers, + ** one for the numerator and one for the denominator. + ** The number is always stored so that the gcd of the numerator and denominator + ** is 1. (This is referred to as referred to as canonical form in GMP's + ** literature.) A consquence is that that the numerator and denominator may be + ** different than the values used to construct the Rational. + **/ + +#include "cvc4_public.h" + +#ifndef __CVC4__BOOL_H +#define __CVC4__BOOL_H + +namespace CVC4 { + +struct BoolHashStrategy { + static inline size_t hash(bool b) { + return b; + } +};/* struct BoolHashStrategy */ + +}/* CVC4 namespace */ + +#endif /* __CVC4__BOOL_H */ diff --git a/src/util/configuration.cpp b/src/util/configuration.cpp new file mode 100644 index 000000000..f4ce30968 --- /dev/null +++ b/src/util/configuration.cpp @@ -0,0 +1,102 @@ +/********************* */ +/** configuration.cpp + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010 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. + ** + ** Implementation of Configuration class, which provides compile-time + ** configuration information about the CVC4 library. + **/ + +#include "util/configuration.h" +#include "cvc4autoconfig.h" + +using namespace std; + +namespace CVC4 { + +bool Configuration::isDebugBuild() { +#ifdef CVC4_DEBUG + return true; +#else /* CVC4_DEBUG */ + return false; +#endif /* CVC4_DEBUG */ +} + +bool Configuration::isTracingBuild() { +#ifdef CVC4_TRACING + return true; +#else /* CVC4_TRACING */ + return false; +#endif /* CVC4_TRACING */ +} + +bool Configuration::isMuzzledBuild() { +#ifdef CVC4_MUZZLE + return true; +#else /* CVC4_MUZZLE */ + return false; +#endif /* CVC4_MUZZLE */ +} + +bool Configuration::isAssertionBuild() { +#ifdef CVC4_ASSERTIONS + return true; +#else /* CVC4_ASSERTIONS */ + return false; +#endif /* CVC4_ASSERTIONS */ +} + +bool Configuration::isCoverageBuild() { +#ifdef CVC4_COVERAGE + return true; +#else /* CVC4_COVERAGE */ + return false; +#endif /* CVC4_COVERAGE */ +} + +bool Configuration::isProfilingBuild() { +#ifdef CVC4_PROFILING + return true; +#else /* CVC4_PROFILING */ + return false; +#endif /* CVC4_PROFILING */ +} + +string Configuration::getPackageName() { + return PACKAGE_NAME; +} + +string Configuration::getVersionString() { + return CVC4_RELEASE_STRING; +} + +unsigned Configuration::getVersionMajor() { + return CVC4_MAJOR; +} + +unsigned Configuration::getVersionMinor() { + return CVC4_MINOR; +} + +unsigned Configuration::getVersionRelease() { + return CVC4_RELEASE; +} + +string Configuration::about() { + return string("\ +This is a pre-release of CVC4.\n\ +Copyright (C) 2009, 2010\n\ + The ACSys Group\n\ + Courant Institute of Mathematical Sciences,\n\ + New York University\n\ + New York, NY 10012 USA\n"); +} + +}/* CVC4 namespace */ diff --git a/src/util/configuration.h b/src/util/configuration.h index 20d00a5f8..f939d8981 100644 --- a/src/util/configuration.h +++ b/src/util/configuration.h @@ -10,14 +10,16 @@ ** See the file COPYING in the top-level source directory for licensing ** information. ** - ** SmtEngine: the main public entry point of libcvc4. + ** Interface to a public class that provides compile-time information + ** about the CVC4 library. **/ +#include "cvc4_public.h" + #ifndef __CVC4__CONFIGURATION_H #define __CVC4__CONFIGURATION_H -#include "config.h" -#include "cvc4_config.h" +#include <string> namespace CVC4 { @@ -31,84 +33,29 @@ class CVC4_PUBLIC Configuration { public: - static bool isDebugBuild() { -#ifdef CVC4_DEBUG - return true; -#else /* CVC4_DEBUG */ - return false; -#endif /* CVC4_DEBUG */ - } - - static bool isTracingBuild() { -#ifdef CVC4_TRACING - return true; -#else /* CVC4_TRACING */ - return false; -#endif /* CVC4_TRACING */ - } - - static bool isMuzzledBuild() { -#ifdef CVC4_MUZZLE - return true; -#else /* CVC4_MUZZLE */ - return false; -#endif /* CVC4_MUZZLE */ - } - - static bool isAssertionBuild() { -#ifdef CVC4_ASSERTIONS - return true; -#else /* CVC4_ASSERTIONS */ - return false; -#endif /* CVC4_ASSERTIONS */ - } - - static bool isCoverageBuild() { -#ifdef CVC4_COVERAGE - return true; -#else /* CVC4_COVERAGE */ - return false; -#endif /* CVC4_COVERAGE */ - } - - static bool isProfilingBuild() { -#ifdef CVC4_PROFILING - return true; -#else /* CVC4_PROFILING */ - return false; -#endif /* CVC4_PROFILING */ - } - - static std::string getPackageName() { - return PACKAGE; - } - - static std::string getVersionString() { - return VERSION; - } - - static unsigned getVersionMajor() { - return 0; - } - - static unsigned getVersionMinor() { - return 0; - } - - static unsigned getVersionRelease() { - return 0; - } - - static std::string about() { - return std::string("\ -This is a pre-release of CVC4.\n\ -Copyright (C) 2009, 2010\n\ - The ACSys Group\n\ - Courant Institute of Mathematical Sciences,\n\ - New York University\n\ - New York, NY 10012 USA\n"); - } + static bool isDebugBuild(); + + static bool isTracingBuild(); + + static bool isMuzzledBuild(); + + static bool isAssertionBuild(); + + static bool isCoverageBuild(); + + static bool isProfilingBuild(); + + static std::string getPackageName(); + + static std::string getVersionString(); + + static unsigned getVersionMajor(); + + static unsigned getVersionMinor(); + + static unsigned getVersionRelease(); + static std::string about(); }; }/* CVC4 namespace */ diff --git a/src/util/debug.h b/src/util/debug.h index 13b097955..a99652661 100644 --- a/src/util/debug.h +++ b/src/util/debug.h @@ -20,8 +20,6 @@ #ifndef __CVC4__DEBUG_H #define __CVC4__DEBUG_H -#include "cvc4_config.h" - #include <cassert> #ifdef CVC4_ASSERTIONS diff --git a/src/util/decision_engine.h b/src/util/decision_engine.h index fd757b734..84ace55b2 100644 --- a/src/util/decision_engine.h +++ b/src/util/decision_engine.h @@ -18,7 +18,6 @@ #ifndef __CVC4__DECISION_ENGINE_H #define __CVC4__DECISION_ENGINE_H -#include "cvc4_config.h" #include "expr/node.h" namespace CVC4 { diff --git a/src/util/exception.h b/src/util/exception.h index ff88b5d81..862597bae 100644 --- a/src/util/exception.h +++ b/src/util/exception.h @@ -13,11 +13,12 @@ ** CVC4's exception base class and some associated utilities. **/ +#include "cvc4_public.h" + #ifndef __CVC4__EXCEPTION_H #define __CVC4__EXCEPTION_H #include <string> -#include "cvc4_config.h" namespace CVC4 { diff --git a/src/util/integer.cpp b/src/util/integer.cpp index 8fc788eb8..41291cc42 100644 --- a/src/util/integer.cpp +++ b/src/util/integer.cpp @@ -1,3 +1,24 @@ +/********************* */ +/** integer.cpp + ** Original author: taking + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010 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. + ** + ** A multiprecision rational constant. + ** This stores the rational as a pair of multiprecision integers, + ** one for the numerator and one for the denominator. + ** The number is always stored so that the gcd of the numerator and denominator + ** is 1. (This is referred to as referred to as canonical form in GMP's + ** literature.) A consquence is that that the numerator and denominator may be + ** different than the values used to construct the Rational. + **/ + #include "util/integer.h" using namespace CVC4; diff --git a/src/util/integer.h b/src/util/integer.h index c86e836c7..ffba5543a 100644 --- a/src/util/integer.h +++ b/src/util/integer.h @@ -13,6 +13,8 @@ ** A multiprecision integer constant. **/ +#include "cvc4_public.h" + #ifndef __CVC4__INTEGER_H #define __CVC4__INTEGER_H @@ -148,11 +150,11 @@ public: friend class CVC4::Rational; };/* class Integer */ -struct IntegerHashFcn { +struct IntegerHashStrategy { static inline size_t hash(const CVC4::Integer& i) { return i.hash(); } -}; +};/* struct IntegerHashStrategy */ std::ostream& operator<<(std::ostream& os, const Integer& n); diff --git a/src/util/model.h b/src/util/model.h index d2a51e447..f807ff963 100644 --- a/src/util/model.h +++ b/src/util/model.h @@ -13,6 +13,8 @@ ** A model. **/ +#include "cvc4_public.h" + #ifndef __CVC4__MODEL_H #define __CVC4__MODEL_H diff --git a/src/util/options.h b/src/util/options.h index 8e2d46e99..c8c95dd11 100644 --- a/src/util/options.h +++ b/src/util/options.h @@ -13,12 +13,14 @@ ** Global (command-line or equivalent) tuning parameters. **/ +#include "cvc4_public.h" + #ifndef __CVC4__OPTIONS_H #define __CVC4__OPTIONS_H #include <iostream> #include <string> -#include "cvc4_config.h" + #include "parser/parser_options.h" namespace CVC4 { diff --git a/src/util/output.cpp b/src/util/output.cpp index e7ac3de90..5d09e1d93 100644 --- a/src/util/output.cpp +++ b/src/util/output.cpp @@ -13,8 +13,6 @@ ** Output utility classes and functions. **/ -#include "cvc4_config.h" - #include <iostream> #include "util/output.h" diff --git a/src/util/output.h b/src/util/output.h index 77b755ad5..6315389e8 100644 --- a/src/util/output.h +++ b/src/util/output.h @@ -13,11 +13,11 @@ ** Output utility classes and functions. **/ +#include "cvc4_public.h" + #ifndef __CVC4__OUTPUT_H #define __CVC4__OUTPUT_H -#include "cvc4_config.h" - #include <iostream> #include <string> #include <cstdio> diff --git a/src/util/rational.cpp b/src/util/rational.cpp index 2f33ed859..f3584e8f3 100644 --- a/src/util/rational.cpp +++ b/src/util/rational.cpp @@ -1,3 +1,17 @@ +/********************* */ +/** rational.cpp + ** Original author: taking + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010 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. + ** + ** A multiprecision rational constant. + **/ #include "util/rational.h" diff --git a/src/util/rational.h b/src/util/rational.h index fdd125587..37d0c08cb 100644 --- a/src/util/rational.h +++ b/src/util/rational.h @@ -19,6 +19,8 @@ ** different than the values used to construct the Rational. **/ +#include "cvc4_public.h" + #ifndef __CVC4__RATIONAL_H #define __CVC4__RATIONAL_H @@ -181,11 +183,11 @@ public: };/* class Rational */ -struct RationalHashFcn { +struct RationalHashStrategy { static inline size_t hash(const CVC4::Rational& r) { return r.hash(); } -}; +};/* struct RationalHashStrategy */ std::ostream& operator<<(std::ostream& os, const Rational& n); diff --git a/src/util/result.h b/src/util/result.h index 7557cece8..679e68763 100644 --- a/src/util/result.h +++ b/src/util/result.h @@ -13,6 +13,8 @@ ** Encapsulation of the result of a query. **/ +#include "cvc4_public.h" + #ifndef __CVC4__RESULT_H #define __CVC4__RESULT_H diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am index 3d9e65070..0b40698cd 100644 --- a/test/unit/Makefile.am +++ b/test/unit/Makefile.am @@ -1,5 +1,6 @@ # All unit tests UNIT_TESTS = \ + expr/expr_black \ expr/node_white \ expr/node_black \ expr/kind_black \ diff --git a/test/unit/expr/expr_black.h b/test/unit/expr/expr_black.h new file mode 100644 index 000000000..b08b5c6aa --- /dev/null +++ b/test/unit/expr/expr_black.h @@ -0,0 +1,414 @@ +/********************* */ +/** expr_black.h + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010 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. + ** + ** Black box testing of CVC4::Expr. + **/ + +#include <cxxtest/TestSuite.h> + +#include <sstream> +#include <string> + +#include "expr/expr_manager.h" +#include "expr/expr.h" +#include "util/Assert.h" +#include "util/exception.h" + +using namespace CVC4; +using namespace CVC4::kind; +using namespace std; + +class ExprBlack : public CxxTest::TestSuite { +private: + + ExprManager* d_em; + + Expr* a; + Expr* b; + Expr* c; + Expr* mult; + Expr* plus; + Expr* d; + Expr* null; + + Expr* i1; + Expr* i2; + Expr* r1; + Expr* r2; + +public: + + void setUp() { + try { + d_em = new ExprManager; + + a = new Expr(d_em->mkVar(d_em->booleanType(), "a")); + b = new Expr(d_em->mkVar(d_em->booleanType(), "b")); + c = new Expr(d_em->mkExpr(MULT, *a, *b)); + mult = new Expr(d_em->mkConst(MULT)); + plus = new Expr(d_em->mkConst(PLUS)); + d = new Expr(d_em->mkExpr(APPLY_UF, *plus, *b, *c)); + null = new Expr; + + i1 = new Expr(d_em->mkConst(Integer("0"))); + i2 = new Expr(d_em->mkConst(Integer(23))); + r1 = new Expr(d_em->mkConst(Rational(1, 5))); + r2 = new Expr(d_em->mkConst(Rational("0"))); + } catch(Exception e) { + cerr << "Exception during setUp():" << endl << e; + throw; + } + } + + void tearDown() { + try { + delete r2; + delete r1; + delete i2; + delete i1; + + delete null; + delete d; + delete plus; + delete mult; + delete c; + delete b; + delete a; + + delete d_em; + } catch(Exception e) { + cerr << "Exception during tearDown():" << endl << e; + throw; + } + } + + void testDefaultCtor() { + /* Expr(); */ + Expr e; + TS_ASSERT(e.isNull()); + } + + void testCtors() { + TS_ASSERT(!a->isNull()); + TS_ASSERT(!b->isNull()); + + /* Expr(); */ + Expr e; + TS_ASSERT(e.isNull()); + + /* Expr(const Expr& e) */ + Expr e2(e); + TS_ASSERT(e == e2); + TS_ASSERT(e2 == e); + TS_ASSERT(!(e2 < e)); + TS_ASSERT(!(e < e2)); + TS_ASSERT(e.isNull()); + TS_ASSERT(e2.isNull()); + Expr f = d_em->mkExpr(PLUS, *a, *b); + Expr f2 = f; + TS_ASSERT(!f.isNull()); + TS_ASSERT(!f2.isNull()); + TS_ASSERT(f == f2); + TS_ASSERT(f2 == f); + TS_ASSERT(!(f2 < f)); + TS_ASSERT(!(f < f2)); + TS_ASSERT(f == d_em->mkExpr(PLUS, *a, *b)); + } + + void testAssignment() { + /* Expr& operator=(const Expr& e); */ + Expr e = d_em->mkExpr(PLUS, *a, *b); + Expr f; + TS_ASSERT(f.isNull()); + f = e; + TS_ASSERT(!f.isNull()); + TS_ASSERT(e == f); + TS_ASSERT(f == e); + TS_ASSERT(!(f < e)); + TS_ASSERT(!(e < f)); + TS_ASSERT(f == d_em->mkExpr(PLUS, *a, *b)); + } + + void testEquality() { + /* bool operator==(const Expr& e) const; */ + /* bool operator!=(const Expr& e) const; */ + + TS_ASSERT(*a == *a); + TS_ASSERT(*b == *b); + TS_ASSERT(!(*a != *a)); + TS_ASSERT(!(*b != *b)); + + TS_ASSERT(*a != *b); + TS_ASSERT(*b != *a); + TS_ASSERT(!(*a == *b)); + TS_ASSERT(!(*b == *a)); + } + + void testComparison() { + /* bool operator<(const Expr& e) const; */ + + TS_ASSERT(*null < *a); + TS_ASSERT(*null < *b); + TS_ASSERT(*null < *c); + TS_ASSERT(*null < *d); + TS_ASSERT(*null < *plus); + TS_ASSERT(*null < *mult); + TS_ASSERT(*null < *i1); + TS_ASSERT(*null < *i2); + TS_ASSERT(*null < *r1); + TS_ASSERT(*null < *r2); + + TS_ASSERT(*a < *b); + TS_ASSERT(*a < *c); + TS_ASSERT(*a < *d); + TS_ASSERT(!(*b < *a)); + TS_ASSERT(!(*c < *a)); + TS_ASSERT(!(*d < *a)); + + TS_ASSERT(*b < *c); + TS_ASSERT(*b < *d); + TS_ASSERT(!(*c < *b)); + TS_ASSERT(!(*d < *b)); + + TS_ASSERT(*c < *d); + TS_ASSERT(!(*d < *c)); + + TS_ASSERT(*mult < *c); + TS_ASSERT(*mult < *d); + TS_ASSERT(*plus < *d); + TS_ASSERT(!(*c < *mult)); + TS_ASSERT(!(*d < *mult)); + TS_ASSERT(!(*d < *plus)); + + TS_ASSERT(!(*null < *null)); + TS_ASSERT(!(*a < *a)); + TS_ASSERT(!(*b < *b)); + TS_ASSERT(!(*c < *c)); + TS_ASSERT(!(*plus < *plus)); + TS_ASSERT(!(*mult < *mult)); + TS_ASSERT(!(*d < *d)); + } + + void testGetKind() { + /* Kind getKind() const; */ + + TS_ASSERT(a->getKind() == VARIABLE); + TS_ASSERT(b->getKind() == VARIABLE); + TS_ASSERT(c->getKind() == MULT); + TS_ASSERT(mult->getKind() == BUILTIN); + TS_ASSERT(plus->getKind() == BUILTIN); + TS_ASSERT(d->getKind() == APPLY_UF); + TS_ASSERT(null->getKind() == NULL_EXPR); + + TS_ASSERT(i1->getKind() == CONST_INTEGER); + TS_ASSERT(i2->getKind() == CONST_INTEGER); + TS_ASSERT(r1->getKind() == CONST_RATIONAL); + TS_ASSERT(r2->getKind() == CONST_RATIONAL); + } + + void testGetNumChildren() { + /* size_t getNumChildren() const; */ + + TS_ASSERT(a->getNumChildren() == 0); + TS_ASSERT(b->getNumChildren() == 0); + TS_ASSERT(c->getNumChildren() == 2); + TS_ASSERT(mult->getNumChildren() == 0); + TS_ASSERT(plus->getNumChildren() == 0); + TS_ASSERT(d->getNumChildren() == 2); + TS_ASSERT(null->getNumChildren() == 0); + + TS_ASSERT(i1->getNumChildren() == 0); + TS_ASSERT(i2->getNumChildren() == 0); + TS_ASSERT(r1->getNumChildren() == 0); + TS_ASSERT(r2->getNumChildren() == 0); + } + + void testOperatorFunctions() { + /* bool hasOperator() const; */ + /* Expr getOperator() const; */ + + TS_ASSERT(!a->hasOperator()); + TS_ASSERT(!b->hasOperator()); + TS_ASSERT(c->hasOperator()); + TS_ASSERT(!mult->hasOperator()); + TS_ASSERT(!plus->hasOperator()); + TS_ASSERT(d->hasOperator()); + TS_ASSERT(!null->hasOperator()); + + TS_ASSERT_THROWS(a->getOperator(), IllegalArgumentException); + TS_ASSERT_THROWS(b->getOperator(), IllegalArgumentException); + TS_ASSERT(c->getOperator() == *mult); + TS_ASSERT_THROWS(plus->getOperator(), IllegalArgumentException); + TS_ASSERT_THROWS(mult->getOperator(), IllegalArgumentException); + TS_ASSERT(d->getOperator() == *plus); + TS_ASSERT_THROWS(null->getOperator(), IllegalArgumentException); + } + + void testGetType() { + /* Type* getType() const; */ + + TS_ASSERT(a->getType() == d_em->booleanType()); + TS_ASSERT(b->getType() == d_em->booleanType()); + TS_ASSERT(c->getType() == NULL); + TS_ASSERT(mult->getType() == NULL); + TS_ASSERT(plus->getType() == NULL); + TS_ASSERT(d->getType() == NULL); +#ifdef CVC4_ASSERTIONS + TS_ASSERT_THROWS(null->getType(), AssertionException); +#endif /* CVC4_ASSERTIONS */ + + TS_ASSERT(i1->getType() == NULL); + TS_ASSERT(i2->getType() == NULL); + TS_ASSERT(r1->getType() == NULL); + TS_ASSERT(r2->getType() == NULL); + } + + void testToString() { + /* std::string toString() const; */ + + TS_ASSERT(a->toString() == "a"); + TS_ASSERT(b->toString() == "b"); + TS_ASSERT(c->toString() == "(MULT a b)"); + TS_ASSERT(mult->toString() == "(BUILTIN MULT)"); + TS_ASSERT(plus->toString() == "(BUILTIN PLUS)"); + TS_ASSERT(d->toString() == "(APPLY_UF (BUILTIN PLUS) b (MULT a b))"); + TS_ASSERT(null->toString() == "null"); + + TS_ASSERT(i1->toString() == "(CONST_INTEGER 0)"); + TS_ASSERT(i2->toString() == "(CONST_INTEGER 23)"); + TS_ASSERT(r1->toString() == "(CONST_RATIONAL 1/5)"); + TS_ASSERT(r2->toString() == "(CONST_RATIONAL 0)"); + } + + void testToStream() { + /* void toStream(std::ostream& out) const; */ + + stringstream sa, sb, sc, smult, splus, sd, snull; + stringstream si1, si2, sr1, sr2; + a->toStream(sa); + b->toStream(sb); + c->toStream(sc); + mult->toStream(smult); + plus->toStream(splus); + d->toStream(sd); + null->toStream(snull); + + i1->toStream(si1); + i2->toStream(si2); + r1->toStream(sr1); + r2->toStream(sr2); + + TS_ASSERT(sa.str() == "a"); + TS_ASSERT(sb.str() == "b"); + TS_ASSERT(sc.str() == "(MULT a b)"); + TS_ASSERT(smult.str() == "(BUILTIN MULT)"); + TS_ASSERT(splus.str() == "(BUILTIN PLUS)"); + TS_ASSERT(sd.str() == "(APPLY_UF (BUILTIN PLUS) b (MULT a b))"); + TS_ASSERT(snull.str() == "null"); + + TS_ASSERT(si1.str() == "(CONST_INTEGER 0)"); + TS_ASSERT(si2.str() == "(CONST_INTEGER 23)"); + TS_ASSERT(sr1.str() == "(CONST_RATIONAL 1/5)"); + TS_ASSERT(sr2.str() == "(CONST_RATIONAL 0)"); + } + + void testIsNull() { + /* bool isNull() const; */ + + TS_ASSERT(!a->isNull()); + TS_ASSERT(!b->isNull()); + TS_ASSERT(!c->isNull()); + TS_ASSERT(!mult->isNull()); + TS_ASSERT(!plus->isNull()); + TS_ASSERT(!d->isNull()); + TS_ASSERT(null->isNull()); + } + + void testIsConst() { + /* bool isConst() const; */ + + TS_ASSERT(!a->isConst()); + TS_ASSERT(!b->isConst()); + TS_ASSERT(!c->isConst()); + TS_ASSERT(mult->isConst()); + TS_ASSERT(plus->isConst()); + TS_ASSERT(!d->isConst()); + TS_ASSERT(!null->isConst()); + } + + void testIsAtomic() { + /* bool isAtomic() const; */ + + TS_ASSERT(a->isAtomic()); + TS_ASSERT(b->isAtomic()); + TS_ASSERT(c->isAtomic()); + TS_ASSERT(mult->isAtomic()); + TS_ASSERT(plus->isAtomic()); + TS_ASSERT(d->isAtomic()); + TS_ASSERT(!null->isAtomic()); + + TS_ASSERT(i1->isAtomic()); + TS_ASSERT(i2->isAtomic()); + TS_ASSERT(r1->isAtomic()); + TS_ASSERT(r2->isAtomic()); + + Expr x = d_em->mkExpr(AND, *a, *b); + Expr y = d_em->mkExpr(XOR, *a, *b, *c); + Expr z = d_em->mkExpr(IFF, x, y); + + TS_ASSERT(!x.isAtomic()); + TS_ASSERT(!y.isAtomic()); + TS_ASSERT(!z.isAtomic()); + } + + void testGetConst() { + /* template <class T> + const T& getConst() const; */ + + TS_ASSERT_THROWS(a->getConst<Kind>(), IllegalArgumentException); + TS_ASSERT_THROWS(b->getConst<Kind>(), IllegalArgumentException); + TS_ASSERT_THROWS(c->getConst<Kind>(), IllegalArgumentException); + TS_ASSERT(mult->getConst<Kind>() == MULT); + TS_ASSERT_THROWS(mult->getConst<Integer>(), IllegalArgumentException); + TS_ASSERT(plus->getConst<Kind>() == PLUS); + TS_ASSERT_THROWS(plus->getConst<Rational>(), IllegalArgumentException); + TS_ASSERT_THROWS(d->getConst<Kind>(), IllegalArgumentException); + TS_ASSERT_THROWS(null->getConst<Kind>(), IllegalArgumentException); + + TS_ASSERT(i1->getConst<Integer>() == 0); + TS_ASSERT(i2->getConst<Integer>() == 23); + TS_ASSERT(r1->getConst<Rational>() == Rational(1, 5)); + TS_ASSERT(r2->getConst<Rational>() == Rational("0")); + + TS_ASSERT_THROWS(i1->getConst<Kind>(), IllegalArgumentException); + TS_ASSERT_THROWS(i2->getConst<Kind>(), IllegalArgumentException); + TS_ASSERT_THROWS(r1->getConst<Kind>(), IllegalArgumentException); + TS_ASSERT_THROWS(r2->getConst<Kind>(), IllegalArgumentException); + } + + void testGetExprManager() { + /* ExprManager* getExprManager() const; */ + + TS_ASSERT(a->getExprManager() == d_em); + TS_ASSERT(b->getExprManager() == d_em); + TS_ASSERT(c->getExprManager() == d_em); + TS_ASSERT(mult->getExprManager() == d_em); + TS_ASSERT(plus->getExprManager() == d_em); + TS_ASSERT(d->getExprManager() == d_em); + TS_ASSERT(null->getExprManager() == NULL); + + TS_ASSERT(i1->getExprManager() == d_em); + TS_ASSERT(i2->getExprManager() == d_em); + TS_ASSERT(r1->getExprManager() == d_em); + TS_ASSERT(r2->getExprManager() == d_em); + } +}; diff --git a/test/unit/expr/node_black.h b/test/unit/expr/node_black.h index c92ea31f5..0b46b06ce 100644 --- a/test/unit/expr/node_black.h +++ b/test/unit/expr/node_black.h @@ -174,8 +174,8 @@ public: #endif /* CVC4_ASSERTIONS */ //Basic access check - Node tb = d_nodeManager->mkNode(TRUE); - Node eb = d_nodeManager->mkNode(FALSE); + Node tb = d_nodeManager->mkConst(true); + Node eb = d_nodeManager->mkConst(false); Node cnd = d_nodeManager->mkNode(XOR, tb, eb); Node ite = cnd.iteNode(tb, eb); @@ -232,7 +232,7 @@ public: */ // simple test of descending descendant property - Node child = d_nodeManager->mkNode(TRUE); + Node child = d_nodeManager->mkConst(true); Node parent = d_nodeManager->mkNode(NOT, child); TS_ASSERT(child < parent); @@ -259,8 +259,8 @@ public: void testEqNode() { /* Node eqNode(const Node& right) const; */ - Node left = d_nodeManager->mkNode(TRUE); - Node right = d_nodeManager->mkNode(NOT, d_nodeManager->mkNode(FALSE)); + Node left = d_nodeManager->mkConst(true); + Node right = d_nodeManager->mkNode(NOT, d_nodeManager->mkConst(false)); Node eq = left.eqNode(right); TS_ASSERT(EQUAL == eq.getKind()); @@ -273,7 +273,7 @@ public: void testNotNode() { /* Node notNode() const; */ - Node child = d_nodeManager->mkNode(TRUE); + Node child = d_nodeManager->mkConst(true); Node parent = child.notNode(); TS_ASSERT(NOT == parent.getKind()); @@ -285,8 +285,8 @@ public: void testAndNode() { /*Node andNode(const Node& right) const;*/ - Node left = d_nodeManager->mkNode(TRUE); - Node right = d_nodeManager->mkNode(NOT, (d_nodeManager->mkNode(FALSE))); + Node left = d_nodeManager->mkConst(true); + Node right = d_nodeManager->mkNode(NOT, (d_nodeManager->mkConst(false))); Node eq = left.andNode(right); @@ -301,8 +301,8 @@ public: void testOrNode() { /*Node orNode(const Node& right) const;*/ - Node left = d_nodeManager->mkNode(TRUE); - Node right = d_nodeManager->mkNode(NOT, (d_nodeManager->mkNode(FALSE))); + Node left = d_nodeManager->mkConst(true); + Node right = d_nodeManager->mkNode(NOT, (d_nodeManager->mkConst(false))); Node eq = left.orNode(right); @@ -321,8 +321,8 @@ public: Node b = d_nodeManager->mkVar(); Node cnd = d_nodeManager->mkNode(PLUS, a, b); - Node thenBranch = d_nodeManager->mkNode(TRUE); - Node elseBranch = d_nodeManager->mkNode(NOT, d_nodeManager->mkNode(FALSE)); + Node thenBranch = d_nodeManager->mkConst(true); + Node elseBranch = d_nodeManager->mkNode(NOT, d_nodeManager->mkConst(false)); Node ite = cnd.iteNode(thenBranch, elseBranch); TS_ASSERT(ITE == ite.getKind()); @@ -336,8 +336,8 @@ public: void testIffNode() { /* Node iffNode(const Node& right) const; */ - Node left = d_nodeManager->mkNode(TRUE); - Node right = d_nodeManager->mkNode(NOT, (d_nodeManager->mkNode(FALSE))); + Node left = d_nodeManager->mkConst(true); + Node right = d_nodeManager->mkNode(NOT, (d_nodeManager->mkConst(false))); Node eq = left.iffNode(right); @@ -351,8 +351,8 @@ public: void testImpNode() { /* Node impNode(const Node& right) const; */ - Node left = d_nodeManager->mkNode(TRUE); - Node right = d_nodeManager->mkNode(NOT, (d_nodeManager->mkNode(FALSE))); + Node left = d_nodeManager->mkConst(true); + Node right = d_nodeManager->mkNode(NOT, (d_nodeManager->mkConst(false))); Node eq = left.impNode(right); @@ -365,8 +365,8 @@ public: void testXorNode() { /*Node xorNode(const Node& right) const;*/ - Node left = d_nodeManager->mkNode(TRUE); - Node right = d_nodeManager->mkNode(NOT, (d_nodeManager->mkNode(FALSE))); + Node left = d_nodeManager->mkConst(true); + Node right = d_nodeManager->mkNode(NOT, (d_nodeManager->mkConst(false))); Node eq = left.xorNode(right); @@ -422,7 +422,7 @@ public: void testNaryExpForSize(Kind k, int N) { NodeBuilder<> nbz(k); - Node trueNode = d_nodeManager->mkNode(TRUE); + Node trueNode = d_nodeManager->mkConst(true); for(int i = 0; i < N; ++i) { nbz << trueNode; } @@ -433,7 +433,7 @@ public: void testNumChildren() { /*inline size_t getNumChildren() const;*/ - Node trueNode = d_nodeManager->mkNode(TRUE); + Node trueNode = d_nodeManager->mkConst(true); //test 0 TS_ASSERT(0 == (Node::null()).getNumChildren()); diff --git a/test/unit/expr/node_builder_black.h b/test/unit/expr/node_builder_black.h index cae2e0637..cfef88df7 100644 --- a/test/unit/expr/node_builder_black.h +++ b/test/unit/expr/node_builder_black.h @@ -57,7 +57,7 @@ public: template <unsigned N> void push_back(NodeBuilder<N>& nb, int n){ for(int i = 0; i < n; ++i){ - nb << d_nm->mkNode(TRUE); + nb << d_nm->mkConst(true); } } @@ -293,8 +293,8 @@ public: */ NodeBuilder<> arr(specKind); - Node i_0 = d_nm->mkNode(FALSE); - Node i_2 = d_nm->mkNode(TRUE); + Node i_0 = d_nm->mkConst(false); + Node i_2 = d_nm->mkConst(true); Node i_K = d_nm->mkNode(NOT, i_0); #ifdef CVC4_DEBUG @@ -318,7 +318,7 @@ public: TS_ASSERT_EQUALS(arr[0], i_0); TS_ASSERT_EQUALS(arr[2], i_2); for(int i = 3; i < K; ++i) { - TS_ASSERT_EQUALS(arr[i], d_nm->mkNode(TRUE)); + TS_ASSERT_EQUALS(arr[i], d_nm->mkConst(true)); } arr << i_K; @@ -326,7 +326,7 @@ public: TS_ASSERT_EQUALS(arr[0], i_0); TS_ASSERT_EQUALS(arr[2], i_2); for(int i = 3; i < K; ++i) { - TS_ASSERT_EQUALS(arr[i], d_nm->mkNode(TRUE)); + TS_ASSERT_EQUALS(arr[i], d_nm->mkConst(true)); } TS_ASSERT_EQUALS(arr[K], i_K); @@ -401,7 +401,7 @@ public: TS_ASSERT_EQUALS(modified.getKind(), specKind); NodeBuilder<> nb(specKind); - nb << d_nm->mkNode(TRUE) << d_nm->mkNode(FALSE); + nb << d_nm->mkConst(true) << d_nm->mkConst(false); Node n = nb;// avoid warning on clear() nb.clear(PLUS); @@ -423,10 +423,10 @@ public: #endif /* CVC4_ASSERTIONS */ NodeBuilder<> testMixOrder1; - TS_ASSERT_EQUALS((testMixOrder1 << specKind << d_nm->mkNode(TRUE)).getKind(), + TS_ASSERT_EQUALS((testMixOrder1 << specKind << d_nm->mkConst(true)).getKind(), specKind); NodeBuilder<> testMixOrder2; - TS_ASSERT_EQUALS((testMixOrder2 << d_nm->mkNode(TRUE) << specKind).getKind(), + TS_ASSERT_EQUALS((testMixOrder2 << d_nm->mkConst(true) << specKind).getKind(), specKind); } @@ -539,12 +539,13 @@ public: NodeBuilder<K> a(specKind); NodeBuilder<K> b(specKind); - NodeBuilder<K> c(TRUE); + NodeBuilder<K> c(NOT); string astr, bstr, cstr; stringstream astream, bstream, cstream; push_back(a, K / 2); push_back(b, K / 2); + push_back(c, 1); a.toStream(astream); b.toStream(bstream); @@ -668,7 +669,7 @@ public: // build one-past-the-end for(size_t j = 0; j <= n; ++j) { - b << d_nm->mkNode(TRUE); + b << d_nm->mkConst(true); } } } catch(Exception e) { diff --git a/test/unit/theory/theory_black.h b/test/unit/theory/theory_black.h index 5941b3e5d..7ffc4193a 100644 --- a/test/unit/theory/theory_black.h +++ b/test/unit/theory/theory_black.h @@ -145,8 +145,8 @@ public: d_scope = new NodeManagerScope(d_nm); d_dummy = new DummyTheory(d_ctxt, d_outputChannel); d_outputChannel.clear(); - atom0 = d_nm->mkNode(kind::TRUE); - atom1 = d_nm->mkNode(kind::FALSE); + atom0 = d_nm->mkConst(true); + atom1 = d_nm->mkConst(false); } void tearDown() { |