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
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.
# 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
##
-# 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
])
##
-# 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(
[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)
],
[
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
# -*- 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
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
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
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
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
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
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])
if test "$enable_debug_symbols" = yes; then
CVC4CXXFLAGS="$CVC4CXXFLAGS -ggdb3"
+ CVC4CFLAGS="$CVC4CFLAGS -ggdb3"
fi
AC_MSG_CHECKING([whether to include assertions in build])
CVC4CPPFLAGS="$CVC4CPPFLAGS -DCVC4_COVERAGE"
CVC4CXXFLAGS="$CVC4CXXFLAGS --coverage"
+ CVC4CFLAGS="$CVC4CFLAGS --coverage"
CVC4LDFLAGS="$CVC4LDFLAGS --coverage"
fi
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])
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)])
CPPFLAGS="${CPPFLAGS:+$CPPFLAGS }$CVC4CPPFLAGS"
CXXFLAGS="${CXXFLAGS:+$CXXFLAGS }$CVC4CXXFLAGS -Wno-deprecated"
+CFLAGS="${CFLAGS:+$CFLAGS }$CVC4CFLAGS -Wno-deprecated"
LDFLAGS="${LDFLAGS:+$LDFLAGS }$CVC4LDFLAGS"
# mk_include
CPPFLAGS : $CPPFLAGS
CXXFLAGS : $CXXFLAGS
+CFLAGS : $CFLAGS
LDFLAGS : $LDFLAGS
libcvc4 version : $CVC4_LIBRARY_VERSION
# 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.
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)$/);
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
// 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
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
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
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);
#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.
/** 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;
/** 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;
// 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();
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;
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;
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;
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 */
--- /dev/null
+/********************* */
+/** 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 */
# 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
# 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"
** client code.
**/
+#include "cvc4_public.h"
+
#ifndef __CVC4__COMMAND_H
#define __CVC4__COMMAND_H
#include <string>
#include <vector>
-#include "cvc4_config.h"
#include "expr/expr.h"
#include "util/result.h"
+++ /dev/null
-/********************* */
-/** expr.cpp
- ** Original author: dejan
- ** Major contributors: mdeters
- ** Minor contributors (to current version): taking
- ** 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.
- **
- ** [[ Add file-specific comments here ]]
- **/
-
-#include "expr/expr.h"
-#include "expr/node.h"
-#include "util/Assert.h"
-
-#include "util/output.h"
-
-using namespace CVC4::kind;
-
-namespace CVC4 {
-
-std::ostream& operator<<(std::ostream& out, const Expr& e) {
- e.toStream(out);
- return out;
-}
-
-Expr::Expr() :
- d_node(new Node()), d_exprManager(NULL) {
-}
-
-Expr::Expr(ExprManager* em, Node* node) :
- d_node(node), d_exprManager(em) {
-}
-
-Expr::Expr(const Expr& e) :
- 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);
-}
-
-ExprManager* Expr::getExprManager() const {
- return d_exprManager;
-}
-
-Expr::~Expr() {
- ExprManagerScope ems(*this);
- delete d_node;
-}
-
-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);
- Assert(d_node != NULL, "Unexpected NULL expression pointer!");
- 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;
- }
- Assert(d_node != NULL, "Unexpected NULL expression pointer!");
- Assert(e.d_node != NULL, "Unexpected NULL expression pointer!");
- return *d_node == *e.d_node;
-}
-
-bool Expr::operator!=(const Expr& e) const {
- return !(*this == e);
-}
-
-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;
- }
- return *d_node < *e.d_node;
-}
-
-Kind Expr::getKind() const {
- Assert(d_node != NULL, "Unexpected NULL expression pointer!");
- return d_node->getKind();
-}
-
-size_t Expr::getNumChildren() const {
- Assert(d_node != NULL, "Unexpected NULL expression pointer!");
- return d_node->getNumChildren();
-}
-
-Type* Expr::getType() const {
- ExprManagerScope ems(*this);
- return d_node->getType();
-}
-
-std::string Expr::toString() const {
- ExprManagerScope ems(*this);
- Assert(d_node != NULL, "Unexpected NULL expression pointer!");
- return d_node->toString();
-}
-
-bool Expr::isNull() const {
- Assert(d_node != NULL, "Unexpected NULL expression pointer!");
- return d_node->isNull();
-}
-
-Expr::operator bool() const {
- return !isNull();
-}
-
-void Expr::toStream(std::ostream& out) const {
- ExprManagerScope ems(*this);
- d_node->toStream(out);
-}
-
-Node Expr::getNode() const {
- return *d_node;
-}
-
-BoolExpr::BoolExpr() {
-}
-
-BoolExpr::BoolExpr(const Expr& e) :
- Expr(e) {
-}
-
-BoolExpr BoolExpr::notExpr() const {
- Assert(d_exprManager != NULL, "Don't have an expression manager for this expression!");
- return d_exprManager->mkExpr(NOT, *this);
-}
-
-BoolExpr BoolExpr::andExpr(const BoolExpr& e) const {
- Assert(d_exprManager != NULL, "Don't have an expression manager for this expression!");
- Assert(d_exprManager == e.d_exprManager, "Different expression managers!");
- return d_exprManager->mkExpr(AND, *this, e);
-}
-
-BoolExpr BoolExpr::orExpr(const BoolExpr& e) const {
- Assert(d_exprManager != NULL, "Don't have an expression manager for this expression!");
- Assert(d_exprManager == e.d_exprManager, "Different expression managers!");
- return d_exprManager->mkExpr(OR, *this, e);
-}
-
-BoolExpr BoolExpr::xorExpr(const BoolExpr& e) const {
- Assert(d_exprManager != NULL, "Don't have an expression manager for this expression!");
- Assert(d_exprManager == e.d_exprManager, "Different expression managers!");
- return d_exprManager->mkExpr(XOR, *this, e);
-}
-
-BoolExpr BoolExpr::iffExpr(const BoolExpr& e) const {
- Assert(d_exprManager != NULL, "Don't have an expression manager for this expression!");
- Assert(d_exprManager == e.d_exprManager, "Different expression managers!");
- return d_exprManager->mkExpr(IFF, *this, e);
-}
-
-BoolExpr BoolExpr::impExpr(const BoolExpr& e) const {
- Assert(d_exprManager != NULL, "Don't have an expression manager for this expression!");
- Assert(d_exprManager == e.d_exprManager, "Different expression managers!");
- return d_exprManager->mkExpr(IMPLIES, *this, e);
-}
-
-BoolExpr BoolExpr::iteExpr(const BoolExpr& then_e, const BoolExpr& else_e) const {
- Assert(d_exprManager != NULL, "Don't have an expression manager for this expression!");
- Assert(d_exprManager == then_e.d_exprManager, "Different expression managers!");
- Assert(d_exprManager == else_e.d_exprManager, "Different expression managers!");
- return d_exprManager->mkExpr(ITE, *this, then_e, else_e);
-}
-
-Expr BoolExpr::iteExpr(const Expr& then_e, const Expr& else_e) const {
- Assert(d_exprManager != NULL, "Don't have an expression manager for this expression!");
- Assert(d_exprManager == then_e.getExprManager(), "Different expression managers!");
- Assert(d_exprManager == else_e.getExprManager(), "Different expression managers!");
- return d_exprManager->mkExpr(ITE, *this, then_e, else_e);
-}
-
-void Expr::printAst(std::ostream & o, int indent) const {
- ExprManagerScope ems(*this);
- getNode().printAst(o, indent);
-}
-
-void Expr::debugPrint() {
-#ifndef CVC4_MUZZLE
- printAst(Warning());
- Warning().flush();
-#endif /* ! CVC4_MUZZLE */
-}
-
-
-} // End namespace CVC4
+++ /dev/null
-/********************* */
-/** expr.h
- ** Original author: dejan
- ** Major contributors: none
- ** Minor contributors (to current version): taking, mdeters
- ** 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.
- **
- ** Public-facing expression interface.
- **/
-
-// 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>
-
-namespace CVC4 {
-
-// The internal expression representation
-template <bool count_ref>
-class NodeTemplate;
-
-/**
- * Class encapsulating CVC4 expressions and methods for constructing new
- * expressions.
- */
-class CVC4_PUBLIC Expr {
-
-public:
-
- /** Default constructor, makes a null expression. */
- Expr();
-
- /**
- * Copy constructor, makes a copy of a given expression
- * @param the expression to copy
- */
- Expr(const Expr& e);
-
- /**
- * Initialize 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. Should be removed if future
- * versions of ANTLR fix the problem.
- */
- Expr(uintptr_t n);
-
- /** Destructor */
- ~Expr();
-
- /**
- * Assignment operator, makes a copy of the given expression. If the
- * expression managers of the two expressions differ, the expression of
- * the given expression will be used.
- * @param e the expression to assign
- * @return the reference to this expression after assignment
- */
- 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
- * <code>Expr e</code> gets initialized with <code>e = NULL;</code>.
- * Should be removed if future versions of ANTLR fix the problem.
- */
- Expr& operator=(uintptr_t n);
-
- /**
- * Syntactic comparison operator. Returns true if expressions belong to the
- * same expression manager and are syntactically identical.
- * @param e the expression to compare to
- * @return true if expressions are syntactically the same, false otherwise
- */
- bool operator==(const Expr& e) const;
-
- /**
- * Syntactic dis-equality operator.
- * @param e the expression to compare to
- * @return true if expressions differ syntactically, false otherwise
- */
- bool operator!=(const Expr& e) const;
-
- /**
- * Order comparison operator. The only invariant on the order of expressions
- * is that the expressions that were created sooner will be smaller in the
- * ordering than all the expressions created later. Null expression is the
- * smallest element of the ordering. The behavior of the operator is
- * undefined if the expressions come from two different expression managers.
- * @param e the expression to compare to
- * @return true if this expression is smaller than the given one
- */
- 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
- */
- Kind getKind() const;
-
- /**
- * Returns the number of children of this expression.
- * @return the number of children
- */
- size_t getNumChildren() const;
-
- /** Returns the type of the expression, if it has been computed.
- * Returns NULL if the type of the expression is not known.
- */
- Type* getType() const;
-
- /**
- * Returns the string representation of the expression.
- * @return a string representation of the expression
- */
- std::string toString() const;
-
- /**
- * Outputs the string representation of the expression to the stream.
- * @param the output stream
- */
- void toStream(std::ostream& out) const;
-
- /**
- * Check if this is a null expression.
- * @return true if a null expression
- */
- bool isNull() const;
-
- /**
- * Returns the expression reponsible for this expression.
- */
- ExprManager* getExprManager() const;
-
- /**
- * Very basic pretty printer for Expr.
- * This is equivalent to calling e.getNode().printAst(...)
- * @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;
-
-private:
-
- /**
- * Pretty printer for use within gdb
- * This is not intended to be used outside of gdb.
- * This writes to the ostream Warning() and immediately flushes
- * the ostream.
- */
- void debugPrint();
-
-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
- */
- NodeTemplate<true> getNode() const;
-
- // Friend to access the actual internal node information and private methods
- friend class SmtEngine;
- friend class ExprManager;
-};
-
-/**
- * Output operator for expressions
- * @param out the stream to output to
- * @param e the expression to output
- * @return the stream
- */
-std::ostream& operator<<(std::ostream& out, const Expr& e) CVC4_PUBLIC;
-
-/**
- * Extending the expression with the capability to construct Boolean
- * expressions.
- */
-class CVC4_PUBLIC BoolExpr : public Expr {
-
-public:
-
- /** Default constructor, makes a null expression */
- BoolExpr();
-
- /**
- * Convert an expression to a Boolean expression
- */
- BoolExpr(const Expr& e);
-
- /**
- * Negate this expression.
- * @return the logical negation of this expression.
- */
- BoolExpr notExpr() const;
-
- /**
- * Conjunct the given expression to this expression.
- * @param e the expression to conjunct
- * @return the conjunction of this expression and e
- */
- BoolExpr andExpr(const BoolExpr& e) const;
-
- /**
- * Disjunct the given expression to this expression.
- * @param e the expression to disjunct
- * @return the disjunction of this expression and e
- */
- BoolExpr orExpr(const BoolExpr& e) const;
-
- /**
- * Make an exclusive or expression out of this expression and the given
- * expression.
- * @param e the right side of the xor
- * @return the xor of this expression and e
- */
- BoolExpr xorExpr(const BoolExpr& e) const;
-
- /**
- * Make an equivalence expression out of this expression and the given
- * expression.
- * @param e the right side of the equivalence
- * @return the equivalence expression
- */
- BoolExpr iffExpr(const BoolExpr& e) const;
-
- /**
- * Make an implication expression out of this expression and the given
- * expression.
- * @param e the right side of the equivalence
- * @return the equivalence expression
- */
- BoolExpr impExpr(const BoolExpr& e) const;
-
- /**
- * Make a Boolean if-then-else expression using this expression as the
- * condition, and given the then and else parts
- * @param then_e the then branch expression
- * @param else_e the else branch expression
- * @return the if-then-else expression
- */
- BoolExpr iteExpr(const BoolExpr& then_e, const BoolExpr& else_e) const;
-
- /**
- * Make a term if-then-else expression using this expression as the
- * condition, and given the then and else parts
- * @param then_e the then branch expression
- * @param else_e the else branch expression
- * @return the if-then-else expression
- */
- Expr iteExpr(const Expr& then_e, const Expr& else_e) const;
-};
-
-}
-
-#endif /* __CVC4__EXPR_H */
+++ /dev/null
-/********************* */
-/** expr_manager.cpp
- ** Original author: dejan
- ** Major contributors: cconway, mdeters
- ** 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.
- **
- ** [[ Add file-specific comments here ]]
- **/
-
-/*
- * expr_manager.cpp
- *
- * Created on: Dec 10, 2009
- * Author: dejan
- */
-
-#include "context/context.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/type.h"
-
-using namespace std;
-using namespace CVC4::context;
-using namespace CVC4::kind;
-
-namespace CVC4 {
-
-ExprManager::ExprManager() :
- d_ctxt(new Context),
- d_nodeManager(new NodeManager(d_ctxt)) {
-}
-
-ExprManager::~ExprManager() {
- delete d_nodeManager;
- delete d_ctxt;
-}
-
-BooleanType* ExprManager::booleanType() const {
- NodeManagerScope nms(d_nodeManager);
- return d_nodeManager->booleanType();
-}
-
-KindType* ExprManager::kindType() const {
- NodeManagerScope nms(d_nodeManager);
- return d_nodeManager->kindType();
-}
-
-Expr ExprManager::mkExpr(Kind kind) {
- NodeManagerScope nms(d_nodeManager);
- return Expr(this, new Node(d_nodeManager->mkNode(kind)));
-}
-
-Expr ExprManager::mkExpr(Kind kind, const Expr& child1) {
- NodeManagerScope nms(d_nodeManager);
- return Expr(this, new Node(d_nodeManager->mkNode(kind, child1.getNode())));
-}
-
-Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2) {
- NodeManagerScope nms(d_nodeManager);
- return Expr(this, new Node(d_nodeManager->mkNode(kind, child1.getNode(),
- child2.getNode())));
-}
-
-Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2,
- const Expr& child3) {
- NodeManagerScope nms(d_nodeManager);
- return Expr(this, new Node(d_nodeManager->mkNode(kind, child1.getNode(),
- child2.getNode(), child3.getNode())));
-}
-
-Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2,
- const Expr& child3, const Expr& child4) {
- NodeManagerScope nms(d_nodeManager);
- return Expr(this, new Node(d_nodeManager->mkNode(kind, child1.getNode(),
- child2.getNode(), child3.getNode(),
- child4.getNode())));
-}
-
-Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2,
- const Expr& child3, const Expr& child4,
- const Expr& child5) {
- NodeManagerScope nms(d_nodeManager);
- return Expr(this, new Node(d_nodeManager->mkNode(kind, child1.getNode(),
- child2.getNode(), child3.getNode(),
- child5.getNode())));
-}
-
-Expr ExprManager::mkExpr(Kind kind, const vector<Expr>& children) {
- NodeManagerScope nms(d_nodeManager);
-
- vector<Node> nodes;
- vector<Expr>::const_iterator it = children.begin();
- vector<Expr>::const_iterator it_end = children.end();
- while(it != it_end) {
- nodes.push_back(it->getNode());
- ++it;
- }
- return Expr(this, new Node(d_nodeManager->mkNode(kind, nodes)));
-}
-
-/** Make a function type from domain to range. */
-FunctionType* ExprManager::mkFunctionType(Type* domain,
- Type* range) {
- NodeManagerScope nms(d_nodeManager);
- return d_nodeManager->mkFunctionType(domain, range);
-}
-
-/** Make a function type with input types from argTypes. */
-FunctionType* ExprManager::mkFunctionType(const std::vector<Type*>& argTypes,
- Type* range) {
- Assert( argTypes.size() >= 1 );
- NodeManagerScope nms(d_nodeManager);
- return d_nodeManager->mkFunctionType(argTypes, range);
-}
-
-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) {
- Assert( sorts.size() >= 1 );
- NodeManagerScope nms(d_nodeManager);
- return d_nodeManager->mkPredicateType(sorts);
-}
-
-Type* ExprManager::mkSort(const std::string& name) {
- NodeManagerScope nms(d_nodeManager);
- return d_nodeManager->mkSort(name);
-}
-
-Expr ExprManager::mkVar(Type* type, const std::string& name) {
- NodeManagerScope nms(d_nodeManager);
- return Expr(this, new Node(d_nodeManager->mkVar(type, name)));
-}
-
-Expr ExprManager::mkVar(Type* type) {
- NodeManagerScope nms(d_nodeManager);
- return Expr(this, new Node(d_nodeManager->mkVar(type)));
-}
-
-unsigned int ExprManager::minArity(Kind kind) {
- switch(kind) {
- case FALSE:
- case SKOLEM:
- case TRUE:
- case VARIABLE:
- return 0;
-
- case AND:
- case NOT:
- case OR:
- return 1;
-
- case APPLY_UF:
- case DISTINCT:
- case EQUAL:
- case IFF:
- case IMPLIES:
- case PLUS:
- case XOR:
- return 2;
-
- case ITE:
- return 3;
-
- default:
- Unhandled(kind);
- }
-}
-
-unsigned int ExprManager::maxArity(Kind kind) {
- switch(kind) {
- case FALSE:
- case SKOLEM:
- case TRUE:
- case VARIABLE:
- return 0;
-
- case NOT:
- return 1;
-
- case EQUAL:
- case IFF:
- case IMPLIES:
- case XOR:
- return 2;
-
- case ITE:
- return 3;
-
- case AND:
- case APPLY_UF:
- case DISTINCT:
- case PLUS:
- case OR:
- return UINT_MAX;
-
- default:
- Unhandled(kind);
- }
-}
-
-
-NodeManager* ExprManager::getNodeManager() const {
- return d_nodeManager;
-}
-
-Context* ExprManager::getContext() const {
- return d_ctxt;
-}
-
-}/* CVC4 namespace */
+++ /dev/null
-/********************* */
-/** expr_manager.h
- ** Original author: dejan
- ** Major contributors: cconway, mdeters
- ** Minor contributors (to current version): taking
- ** 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.
- **
- ** Public-facing expression manager interface.
- **/
-
-#ifndef __CVC4__EXPR_MANAGER_H
-#define __CVC4__EXPR_MANAGER_H
-
-#include "cvc4_config.h"
-#include "expr/kind.h"
-#include <vector>
-
-namespace CVC4 {
-
-class Expr;
-class Type;
-class BooleanType;
-class FunctionType;
-class KindType;
-class SmtEngine;
-class NodeManager;
-
-namespace context {
- class Context;
-}/* CVC4::context namespace */
-
-class CVC4_PUBLIC ExprManager {
-
-public:
-
- /**
- * Creates an expression manager.
- */
- ExprManager();
-
- /**
- * Destroys the expression manager. No will be deallocated at this point, so
- * any expression references that used to be managed by this expression
- * manager and are left-over are bad.
- */
- ~ExprManager();
-
- /** Get the type for booleans */
- BooleanType* booleanType() const;
-
- /** Get the type for sorts. */
- KindType* kindType() const;
-
- /**
- * Make a unary expression of a given kind (TRUE, FALSE,...).
- * @param kind the kind of expression
- * @return the expression
- */
- Expr mkExpr(Kind kind);
-
- /**
- * Make a unary expression of a given kind (NOT, BVNOT, ...).
- * @param kind the kind of expression
- * @return the expression
- */
- Expr mkExpr(Kind kind, const Expr& child1);
-
- /**
- * Make a binary 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
- * @return the expression
- */
- Expr mkExpr(Kind kind, const Expr& child1, const Expr& child2);
-
- Expr mkExpr(Kind kind, const Expr& child1, const Expr& child2,
- const Expr& child3);
- Expr mkExpr(Kind kind, const Expr& child1, const Expr& child2,
- const Expr& child3, const Expr& child4);
- Expr mkExpr(Kind kind, const Expr& child1, const Expr& child2,
- const Expr& child3, const Expr& child4, const Expr& child5);
-
- /**
- * Make an n-ary expression of given kind given a vector of it's children
- * @param kind the kind of expression to build
- * @param children the subexpressions
- * @return the n-ary expression
- */
- Expr mkExpr(Kind kind, const std::vector<Expr>& children);
-
- /** 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(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);
-
- // variables are special, because duplicates are permitted
- Expr mkVar(Type* type, const std::string& name);
- Expr mkVar(Type* type);
-
- /** Returns the minimum arity of the given kind. */
- static unsigned int 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;
-};
-
-}/* CVC4 namespace */
-
-#endif /* __CVC4__EXPR_MANAGER_H */
-
--- /dev/null
+/********************* */
+/** expr_manager_template.cpp
+ ** Original author: dejan
+ ** Major contributors: cconway, mdeters
+ ** 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.
+ **
+ ** Public-facing expression manager interface, implementation.
+ **/
+
+#include "expr/node.h"
+#include "expr/expr.h"
+#include "expr/kind.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;
+using namespace CVC4::kind;
+
+namespace CVC4 {
+
+ExprManager::ExprManager() :
+ d_ctxt(new Context),
+ d_nodeManager(new NodeManager(d_ctxt)) {
+}
+
+ExprManager::~ExprManager() {
+ delete d_nodeManager;
+ delete d_ctxt;
+}
+
+BooleanType* ExprManager::booleanType() const {
+ NodeManagerScope nms(d_nodeManager);
+ return d_nodeManager->booleanType();
+}
+
+KindType* ExprManager::kindType() const {
+ NodeManagerScope nms(d_nodeManager);
+ return d_nodeManager->kindType();
+}
+
+Expr ExprManager::mkExpr(Kind kind) {
+ NodeManagerScope nms(d_nodeManager);
+ return Expr(this, new Node(d_nodeManager->mkNode(kind)));
+}
+
+Expr ExprManager::mkExpr(Kind kind, const Expr& child1) {
+ NodeManagerScope nms(d_nodeManager);
+ return Expr(this, new Node(d_nodeManager->mkNode(kind, child1.getNode())));
+}
+
+Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2) {
+ NodeManagerScope nms(d_nodeManager);
+ return Expr(this, new Node(d_nodeManager->mkNode(kind, child1.getNode(),
+ child2.getNode())));
+}
+
+Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2,
+ const Expr& child3) {
+ NodeManagerScope nms(d_nodeManager);
+ return Expr(this, new Node(d_nodeManager->mkNode(kind, child1.getNode(),
+ child2.getNode(), child3.getNode())));
+}
+
+Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2,
+ const Expr& child3, const Expr& child4) {
+ NodeManagerScope nms(d_nodeManager);
+ return Expr(this, new Node(d_nodeManager->mkNode(kind, child1.getNode(),
+ child2.getNode(), child3.getNode(),
+ child4.getNode())));
+}
+
+Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2,
+ const Expr& child3, const Expr& child4,
+ const Expr& child5) {
+ NodeManagerScope nms(d_nodeManager);
+ return Expr(this, new Node(d_nodeManager->mkNode(kind, child1.getNode(),
+ child2.getNode(), child3.getNode(),
+ child5.getNode())));
+}
+
+Expr ExprManager::mkExpr(Kind kind, const vector<Expr>& children) {
+ NodeManagerScope nms(d_nodeManager);
+
+ vector<Node> nodes;
+ vector<Expr>::const_iterator it = children.begin();
+ vector<Expr>::const_iterator it_end = children.end();
+ while(it != it_end) {
+ nodes.push_back(it->getNode());
+ ++it;
+ }
+ return Expr(this, new Node(d_nodeManager->mkNode(kind, nodes)));
+}
+
+/** Make a function type from domain to range. */
+FunctionType* ExprManager::mkFunctionType(Type* domain,
+ Type* range) {
+ NodeManagerScope nms(d_nodeManager);
+ return d_nodeManager->mkFunctionType(domain, range);
+}
+
+/** Make a function type with input types from argTypes. */
+FunctionType* ExprManager::mkFunctionType(const std::vector<Type*>& argTypes,
+ Type* range) {
+ Assert( argTypes.size() >= 1 );
+ NodeManagerScope nms(d_nodeManager);
+ return d_nodeManager->mkFunctionType(argTypes, range);
+}
+
+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) {
+ Assert( sorts.size() >= 1 );
+ NodeManagerScope nms(d_nodeManager);
+ return d_nodeManager->mkPredicateType(sorts);
+}
+
+Type* ExprManager::mkSort(const std::string& name) {
+ NodeManagerScope nms(d_nodeManager);
+ return d_nodeManager->mkSort(name);
+}
+
+Expr ExprManager::mkVar(Type* type, const std::string& name) {
+ NodeManagerScope nms(d_nodeManager);
+ return Expr(this, new Node(d_nodeManager->mkVar(type, name)));
+}
+
+Expr ExprManager::mkVar(Type* type) {
+ NodeManagerScope nms(d_nodeManager);
+ return Expr(this, new Node(d_nodeManager->mkVar(type)));
+}
+
+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 SKOLEM:
+ case VARIABLE:
+ return 0;
+
+ case AND:
+ case NOT:
+ case OR:
+ return 1;
+
+ case APPLY_UF:
+ case DISTINCT:
+ case EQUAL:
+ case IFF:
+ case IMPLIES:
+ case PLUS:
+ case XOR:
+ return 2;
+
+ case ITE:
+ return 3;
+
+ default:
+ Unhandled(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 SKOLEM:
+ case VARIABLE:
+ return 0;
+
+ case NOT:
+ return 1;
+
+ case EQUAL:
+ case IFF:
+ case IMPLIES:
+ case XOR:
+ return 2;
+
+ case ITE:
+ return 3;
+
+ case AND:
+ case APPLY_UF:
+ case DISTINCT:
+ case PLUS:
+ case OR:
+ return UINT_MAX;
+
+ default:
+ Unhandled(kind);
+ }
+}
+
+NodeManager* ExprManager::getNodeManager() const {
+ return d_nodeManager;
+}
+
+Context* ExprManager::getContext() const {
+ return d_ctxt;
+}
+
+${mkConst_implementations}
+
+}/* CVC4 namespace */
--- /dev/null
+/********************* */
+/** expr_manager_template.h
+ ** Original author: dejan
+ ** Major contributors: cconway, mdeters
+ ** Minor contributors (to current version): taking
+ ** 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.
+ **
+ ** Public-facing expression manager interface.
+ **/
+
+#include "cvc4_public.h"
+
+#ifndef __CVC4__EXPR_MANAGER_H
+#define __CVC4__EXPR_MANAGER_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 SmtEngine;
+class NodeManager;
+
+namespace context {
+ class 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:
+
+ /**
+ * Creates an expression manager.
+ */
+ ExprManager();
+
+ /**
+ * Destroys the expression manager. No will be deallocated at this point, so
+ * any expression references that used to be managed by this expression
+ * manager and are left-over are bad.
+ */
+ ~ExprManager();
+
+ /** Get the type for booleans */
+ BooleanType* booleanType() const;
+
+ /** Get the type for sorts. */
+ KindType* kindType() const;
+
+ /**
+ * Make a unary expression of a given kind (TRUE, FALSE,...).
+ * @param kind the kind of expression
+ * @return the expression
+ */
+ Expr mkExpr(Kind kind);
+
+ /**
+ * Make a unary expression of a given kind (NOT, BVNOT, ...).
+ * @param child1 kind the kind of expression
+ * @return the expression
+ */
+ Expr mkExpr(Kind kind, const Expr& child1);
+
+ /**
+ * Make a binary 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
+ * @return the expression
+ */
+ 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);
+
+ /**
+ * Make an n-ary expression of given kind given a vector of it's children
+ * @param kind the kind of expression to build
+ * @param children the subexpressions
+ * @return the n-ary expression
+ */
+ 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(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);
+
+ // variables are special, because duplicates are permitted
+ Expr mkVar(Type* type, const std::string& name);
+ Expr mkVar(Type* type);
+
+ /** Returns the minimum arity of the given kind. */
+ static unsigned minArity(Kind kind);
+
+ /** Returns the maximum arity of the given kind. */
+ static unsigned maxArity(Kind kind);
+};
+
+${mkConst_instantiations}
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__EXPR_MANAGER_H */
--- /dev/null
+/********************* */
+/** expr_template.cpp
+ ** Original author: dejan
+ ** Major contributors: mdeters
+ ** Minor contributors (to current version): taking
+ ** 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.
+ **
+ ** Public-facing expression interface, implementation.
+ **/
+
+#include "expr/expr.h"
+#include "expr/node.h"
+#include "util/Assert.h"
+
+#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 {
+
+std::ostream& operator<<(std::ostream& out, const Expr& e) {
+ e.toStream(out);
+ return out;
+}
+
+Expr::Expr() :
+ d_node(new Node),
+ d_exprManager(NULL) {
+}
+
+Expr::Expr(ExprManager* em, Node* node) :
+ d_node(node),
+ d_exprManager(em) {
+}
+
+Expr::Expr(const Expr& e) :
+ 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);
+}
+
+Expr::~Expr() {
+ ExprManagerScope ems(*this);
+ 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);
+ Assert(d_node != NULL, "Unexpected NULL expression pointer!");
+
+ if(EXPECT_FALSE( !isNull() )) {
+ *d_node = Node::null();
+ }
+ 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;
+}
+
+bool Expr::operator!=(const Expr& e) const {
+ return !(*this == e);
+}
+
+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(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();
+}
+
+std::string Expr::toString() const {
+ ExprManagerScope ems(*this);
+ Assert(d_node != NULL, "Unexpected NULL expression pointer!");
+ return d_node->toString();
+}
+
+bool Expr::isNull() const {
+ ExprManagerScope ems(*this);
+ Assert(d_node != NULL, "Unexpected NULL expression pointer!");
+ return d_node->isNull();
+}
+
+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);
+}
+
+Node Expr::getNode() const {
+ return *d_node;
+}
+
+BoolExpr::BoolExpr() {
+}
+
+BoolExpr::BoolExpr(const Expr& e) :
+ Expr(e) {
+}
+
+BoolExpr BoolExpr::notExpr() const {
+ Assert(d_exprManager != NULL, "Don't have an expression manager for this expression!");
+ return d_exprManager->mkExpr(NOT, *this);
+}
+
+BoolExpr BoolExpr::andExpr(const BoolExpr& e) const {
+ Assert(d_exprManager != NULL, "Don't have an expression manager for this expression!");
+ Assert(d_exprManager == e.d_exprManager, "Different expression managers!");
+ return d_exprManager->mkExpr(AND, *this, e);
+}
+
+BoolExpr BoolExpr::orExpr(const BoolExpr& e) const {
+ Assert(d_exprManager != NULL, "Don't have an expression manager for this expression!");
+ Assert(d_exprManager == e.d_exprManager, "Different expression managers!");
+ return d_exprManager->mkExpr(OR, *this, e);
+}
+
+BoolExpr BoolExpr::xorExpr(const BoolExpr& e) const {
+ Assert(d_exprManager != NULL, "Don't have an expression manager for this expression!");
+ Assert(d_exprManager == e.d_exprManager, "Different expression managers!");
+ return d_exprManager->mkExpr(XOR, *this, e);
+}
+
+BoolExpr BoolExpr::iffExpr(const BoolExpr& e) const {
+ Assert(d_exprManager != NULL, "Don't have an expression manager for this expression!");
+ Assert(d_exprManager == e.d_exprManager, "Different expression managers!");
+ return d_exprManager->mkExpr(IFF, *this, e);
+}
+
+BoolExpr BoolExpr::impExpr(const BoolExpr& e) const {
+ Assert(d_exprManager != NULL, "Don't have an expression manager for this expression!");
+ Assert(d_exprManager == e.d_exprManager, "Different expression managers!");
+ return d_exprManager->mkExpr(IMPLIES, *this, e);
+}
+
+BoolExpr BoolExpr::iteExpr(const BoolExpr& then_e, const BoolExpr& else_e) const {
+ Assert(d_exprManager != NULL, "Don't have an expression manager for this expression!");
+ Assert(d_exprManager == then_e.d_exprManager, "Different expression managers!");
+ Assert(d_exprManager == else_e.d_exprManager, "Different expression managers!");
+ return d_exprManager->mkExpr(ITE, *this, then_e, else_e);
+}
+
+Expr BoolExpr::iteExpr(const Expr& then_e, const Expr& else_e) const {
+ Assert(d_exprManager != NULL, "Don't have an expression manager for this expression!");
+ Assert(d_exprManager == then_e.getExprManager(), "Different expression managers!");
+ Assert(d_exprManager == else_e.getExprManager(), "Different expression managers!");
+ return d_exprManager->mkExpr(ITE, *this, then_e, else_e);
+}
+
+void Expr::printAst(std::ostream & o, int indent) const {
+ ExprManagerScope ems(*this);
+ getNode().printAst(o, indent);
+}
+
+void Expr::debugPrint() {
+#ifndef CVC4_MUZZLE
+ printAst(Warning());
+ Warning().flush();
+#endif /* ! CVC4_MUZZLE */
+}
+
+${getConst_implementations}
+
+}/* CVC4 namespace */
--- /dev/null
+/********************* */
+/** expr_template.h
+ ** Original author: dejan
+ ** Major contributors: none
+ ** Minor contributors (to current version): taking, mdeters
+ ** 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.
+ **
+ ** 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 <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 ref_count>
+class NodeTemplate;
+
+/**
+ * Class encapsulating CVC4 expressions and methods for constructing new
+ * 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:
+
+ /** Default constructor, makes a null expression. */
+ Expr();
+
+ /**
+ * Copy constructor, makes a copy of a given expression
+ * @param e the expression to copy
+ */
+ Expr(const Expr& e);
+
+ /**
+ * Initialize 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. Should be removed if future
+ * versions of ANTLR fix the problem.
+ */
+ Expr(uintptr_t n);
+
+ /** Destructor */
+ ~Expr();
+
+ /**
+ * Assignment operator, makes a copy of the given expression. If the
+ * expression managers of the two expressions differ, the expression of
+ * the given expression will be used.
+ * @param e the expression to assign
+ * @return the reference to this expression after assignment
+ */
+ 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
+ * <code>Expr e</code> gets initialized with <code>e = NULL;</code>.
+ * Should be removed if future versions of ANTLR fix the problem.
+ */
+ Expr& operator=(uintptr_t n);
+
+ /**
+ * Syntactic comparison operator. Returns true if expressions belong to the
+ * same expression manager and are syntactically identical.
+ * @param e the expression to compare to
+ * @return true if expressions are syntactically the same, false otherwise
+ */
+ bool operator==(const Expr& e) const;
+
+ /**
+ * Syntactic dis-equality operator.
+ * @param e the expression to compare to
+ * @return true if expressions differ syntactically, false otherwise
+ */
+ bool operator!=(const Expr& e) const;
+
+ /**
+ * Order comparison operator. The only invariant on the order of expressions
+ * is that the expressions that were created sooner will be smaller in the
+ * ordering than all the expressions created later. Null expression is the
+ * smallest element of the ordering. The behavior of the operator is
+ * undefined if the expressions come from two different expression managers.
+ * @param e the expression to compare to
+ * @return true if this expression is smaller than the given one
+ */
+ bool operator<(const Expr& e) const;
+
+ /**
+ * Returns the kind of the expression (AND, PLUS ...).
+ * @return the kind of the expression
+ */
+ Kind getKind() const;
+
+ /**
+ * Returns the number of children of this expression.
+ * @return the number of children
+ */
+ 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.
+ */
+ Type* getType() const;
+
+ /**
+ * Returns the string representation of the expression.
+ * @return a string representation of the expression
+ */
+ std::string toString() const;
+
+ /**
+ * Outputs the string representation of the expression to the stream.
+ * @param out the output stream
+ */
+ void toStream(std::ostream& out) const;
+
+ /**
+ * Check if this is a null expression.
+ * @return true if a null expression
+ */
+ 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;
+
+ /**
+ * Very basic pretty printer for Expr.
+ * This is equivalent to calling e.getNode().printAst(...)
+ * @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;
+
+private:
+
+ /**
+ * Pretty printer for use within gdb
+ * This is not intended to be used outside of gdb.
+ * This writes to the ostream Warning() and immediately flushes
+ * the ostream.
+ */
+ void debugPrint();
+
+protected:
+
+ /**
+ * Returns the actual internal node.
+ * @return the internal node
+ */
+ NodeTemplate<true> getNode() const;
+
+ // Friend to access the actual internal node information and private methods
+ friend class SmtEngine;
+ friend class ExprManager;
+};
+
+/**
+ * Output operator for expressions
+ * @param out the stream to output to
+ * @param e the expression to output
+ * @return the stream
+ */
+std::ostream& operator<<(std::ostream& out, const Expr& e) CVC4_PUBLIC;
+
+/**
+ * Extending the expression with the capability to construct Boolean
+ * expressions.
+ */
+class CVC4_PUBLIC BoolExpr : public Expr {
+
+public:
+
+ /** Default constructor, makes a null expression */
+ BoolExpr();
+
+ /**
+ * Convert an expression to a Boolean expression
+ */
+ BoolExpr(const Expr& e);
+
+ /**
+ * Negate this expression.
+ * @return the logical negation of this expression.
+ */
+ BoolExpr notExpr() const;
+
+ /**
+ * Conjunct the given expression to this expression.
+ * @param e the expression to conjunct
+ * @return the conjunction of this expression and e
+ */
+ BoolExpr andExpr(const BoolExpr& e) const;
+
+ /**
+ * Disjunct the given expression to this expression.
+ * @param e the expression to disjunct
+ * @return the disjunction of this expression and e
+ */
+ BoolExpr orExpr(const BoolExpr& e) const;
+
+ /**
+ * Make an exclusive or expression out of this expression and the given
+ * expression.
+ * @param e the right side of the xor
+ * @return the xor of this expression and e
+ */
+ BoolExpr xorExpr(const BoolExpr& e) const;
+
+ /**
+ * Make an equivalence expression out of this expression and the given
+ * expression.
+ * @param e the right side of the equivalence
+ * @return the equivalence expression
+ */
+ BoolExpr iffExpr(const BoolExpr& e) const;
+
+ /**
+ * Make an implication expression out of this expression and the given
+ * expression.
+ * @param e the right side of the equivalence
+ * @return the equivalence expression
+ */
+ BoolExpr impExpr(const BoolExpr& e) const;
+
+ /**
+ * Make a Boolean if-then-else expression using this expression as the
+ * condition, and given the then and else parts
+ * @param then_e the then branch expression
+ * @param else_e the else branch expression
+ * @return the if-then-else expression
+ */
+ BoolExpr iteExpr(const BoolExpr& then_e, const BoolExpr& else_e) const;
+
+ /**
+ * Make a term if-then-else expression using this expression as the
+ * condition, and given the then and else parts
+ * @param then_e the then branch expression
+ * @param else_e the else branch expression
+ * @return the if-then-else expression
+ */
+ Expr iteExpr(const Expr& then_e, const Expr& else_e) const;
+};
+
+${getConst_instantiations}
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__EXPR_H */
** 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>
return ss.str();
}
-struct KindHashFcn {
+struct KindHashStrategy {
static inline size_t hash(::CVC4::Kind k) { return k; }
-};
+};/* struct KindHashStrategy */
}/* CVC4::kind namespace */
}/* CVC4 namespace */
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 {
--- /dev/null
+#!/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"
# 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.
#
copyright=2010
cat <<EOF
-/********************* -*- C++ -*- */
+/********************* */
/** kind.h
**
** Copyright $copyright The AcSys Group, New York University, and as below.
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"]
# 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.
#
copyright=2010
cat <<EOF
-/********************* -*- C++ -*- */
+/********************* */
/** metakind.h
**
** Copyright $copyright The AcSys Group, New York University, and as below.
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"]
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
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 */
"
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;
"
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
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
b=$(basename $(dirname "$kf"))
metakind_kinds="${metakind_kinds}
/* from $b */
+"
+ metakind_isatomic="${metakind_isatomic}
+ /* from $b */
"
source "$kf"
check_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" : '.*\${\([^}]*\)}.*'`
#include "cvc4_private.h"
+// circular dependency
#include "expr/node_value.h"
#ifndef __CVC4__NODE_H
#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 {
* 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
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
/** 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;
}
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();
}
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);
}
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);
#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>
** 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"
delete t;
}
}
-};
+};/* struct TypeCleanupStrategy */
}/* CVC4::expr::attr namespace */
}/* CVC4::expr namespace */
+++ /dev/null
-/********************* */
-/** cvc4_config.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.
- **
- ** Macros that should be defined everywhere during the building of
- ** the libraries and driver binary.
- **/
-
-#ifndef __CVC4_CONFIG_H
-#define __CVC4_CONFIG_H
-
-#if defined _WIN32 || defined __CYGWIN__
-# ifdef BUILDING_DLL
-# ifdef __GNUC__
-# define CVC4_PUBLIC __attribute__((dllexport))
-# else /* ! __GNUC__ */
-# define CVC4_PUBLIC __declspec(dllexport)
-# endif /* __GNUC__ */
-# else /* BUILDING_DLL */
-# ifdef __GNUC__
-# define CVC4_PUBLIC __attribute__((dllimport))
-# else /* ! __GNUC__ */
-# define CVC4_PUBLIC __declspec(dllimport)
-# endif /* __GNUC__ */
-# endif /* BUILDING_DLL */
-#else /* !( defined _WIN32 || defined __CYGWIN__ ) */
-# if __GNUC__ >= 4
-# define CVC4_PUBLIC __attribute__ ((visibility("default")))
-# else /* !( __GNUC__ >= 4 ) */
-# define CVC4_PUBLIC
-# endif /* __GNUC__ >= 4 */
-#endif /* defined _WIN32 || defined __CYGWIN__ */
-
-#define EXPECT_TRUE(x) __builtin_expect( (x), true)
-#define EXPECT_FALSE(x) __builtin_expect( (x), false)
-#define NORETURN __attribute__ ((noreturn))
-
-#ifndef NULL
-# define NULL ((void*) 0)
-#endif
-
-#endif /* __CVC4_CONFIG_H */
# 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 */
--- /dev/null
+/********************* */
+/** cvc4_public.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.
+ **
+ ** Macros that should be defined everywhere during the building of
+ ** the libraries and driver binary, and also exported to the user.
+ **/
+
+#ifndef __CVC4_PUBLIC_H
+#define __CVC4_PUBLIC_H
+
+#if defined _WIN32 || defined __CYGWIN__
+# ifdef BUILDING_DLL
+# ifdef __GNUC__
+# define CVC4_PUBLIC __attribute__((dllexport))
+# else /* ! __GNUC__ */
+# define CVC4_PUBLIC __declspec(dllexport)
+# endif /* __GNUC__ */
+# else /* BUILDING_DLL */
+# ifdef __GNUC__
+# define CVC4_PUBLIC __attribute__((dllimport))
+# else /* ! __GNUC__ */
+# define CVC4_PUBLIC __declspec(dllimport)
+# endif /* __GNUC__ */
+# endif /* BUILDING_DLL */
+#else /* !( defined _WIN32 || defined __CYGWIN__ ) */
+# if __GNUC__ >= 4
+# define CVC4_PUBLIC __attribute__ ((visibility("default")))
+# else /* !( __GNUC__ >= 4 ) */
+# define CVC4_PUBLIC
+# endif /* __GNUC__ >= 4 */
+#endif /* defined _WIN32 || defined __CYGWIN__ */
+
+#define EXPECT_TRUE(x) __builtin_expect( (x), true)
+#define EXPECT_FALSE(x) __builtin_expect( (x), false)
+#define NORETURN __attribute__ ((noreturn))
+
+#ifndef NULL
+# define NULL ((void*) 0)
+#endif
+
+#endif /* __CVC4_PUBLIC_H */
# 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 */
#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;
#include <cstring>
#include <new>
-#include "config.h"
+#include "cvc4autoconfig.h"
#include "main.h"
#include "usage.h"
#include "parser/input.h"
#include <exception>
#include <string>
-#include "config.h"
+#include "cvc4autoconfig.h"
#include "util/exception.h"
#ifndef __CVC4__MAIN__MAIN_H
#include <signal.h>
#include "util/exception.h"
-#include "config.h"
+#include "cvc4autoconfig.h"
#include "main.h"
using CVC4::Exception;
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
** 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>
#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 {
-/*
- * bounded_token_factory.cpp
- *
- * Created on: Mar 2, 2010
- * Author: dejan
- */
-
#include <antlr3input.h>
#include <antlr3commontoken.h>
#include <antlr3interfaces.h>
factory->unTruc.strFactory = NULL;
}
}
-}
-}
+
+}/* CVC4::parser namespace */
+}/* CVC4 namespace */
-/*
- * 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 {
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 */
#define EXPR_MANAGER ANTLR_INPUT->getExprManager()
#undef MK_EXPR
#define MK_EXPR EXPR_MANAGER->mkExpr
+#undef MK_CONST
+#define MK_CONST EXPR_MANAGER->mkConst
}
/**
: 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]
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]
-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
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
-/*
- * cvc_parser.cpp
- *
- * Created on: Mar 5, 2010
- * Author: chris
- */
-
#include <antlr3.h>
#include "expr/expr_manager.h"
}
*/
-} // namespace parser
-
-} // namespace CVC4
+}/* CVC4::parser namespace */
+}/* CVC4 namespace */
-/*
- * 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"
}; // class CvcInput
-} // namespace parser
+}/* CVC4::parser namespace */
+}/* CVC4 namespace */
-} // namespace CVC4
-
-#endif /* CVC_PARSER_H_ */
+#endif /* __CVC4__PARSER__CVC_INPUT_H */
/********************* */
-/** parser.cpp
+/** input.cpp
** Original author: mdeters
** Major contributors: dejan
** Minor contributors (to current version): cconway
/********************* */
-/** 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
** 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"
-/*
- * memory_mapped_input_buffer.cpp
- *
- * Created on: Mar 3, 2010
- * Author: chris
- */
-
#include <fcntl.h>
#include <stdio.h>
#include <stdint.h>
#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"
/********************* */
-/** 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
** 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
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 */
** 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 {
-/*
- * 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 */
-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
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
#define EXPR_MANAGER ANTLR_INPUT->getExprManager()
#undef MK_EXPR
#define MK_EXPR EXPR_MANAGER->mkExpr
+#undef MK_CONST
+#define MK_CONST EXPR_MANAGER->mkConst
}
/**
{ 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 */
;
-/*
- * smt_parser.cpp
- *
- * Created on: Mar 5, 2010
- * Author: chris
- */
-
#include <antlr3.h>
#include "expr/expr_manager.h"
return d_pSmtParser->parseExpr(d_pSmtParser);
}
-} // namespace parser
-
-} // namespace CVC4
+}/* CVC4::parser namespace */
+}/* CVC4 namespace */
-/*
- * 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"
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
*/
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
*/
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.
*/
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 */
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;
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"
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
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
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
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
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
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
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
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
#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"
** 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
** 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"
@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
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"
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"
# 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.
#
copyright=2010
cat <<EOF
-/********************* -*- C++ -*- */
+/********************* */
/** theoryof_table.h
**
** Copyright $copyright The AcSys Group, New York University, and as below.
do_theoryof "$1"
}
+function nonatomic_operator {
+ # nonatomic_operator K #children ["comment"]
+
+ lineno=${BASH_LINENO[0]}
+
+ do_theoryof "$1"
+}
+
function parameterized {
# parameterized K #children ["comment"]
// rewrite cache support
struct RewriteCacheTag {};
-typedef expr::Attribute<RewriteCacheTag, Node> RewriteCache;
+typedef expr::Attribute<RewriteCacheTag, TNode> RewriteCache;
template <class T>
class TheoryImpl;
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;
}
* 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);
#include <new>
#include <cstdarg>
#include <cstdio>
+
#include "util/Assert.h"
#include "util/exception.h"
-#include "cvc4_config.h"
-#include "config.h"
using namespace std;
** Assertion utility classes, functions, exceptions, and macros.
**/
+#include "cvc4_public.h"
+
#ifndef __CVC4__ASSERT_H
#define __CVC4__ASSERT_H
#include <cstdlib>
#include <cstdarg>
-#include "config.h"
-#include "cvc4_config.h"
#include "util/exception.h"
#include "util/output.h"
output.h \
result.h \
unique_id.h \
- configuration.ha \
+ configuration.h \
+ configuration.cpp \
rational.h \
rational.cpp \
integer.h \
--- /dev/null
+/********************* */
+/** 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 */
--- /dev/null
+/********************* */
+/** 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 */
** 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 {
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 */
#ifndef __CVC4__DEBUG_H
#define __CVC4__DEBUG_H
-#include "cvc4_config.h"
-
#include <cassert>
#ifdef CVC4_ASSERTIONS
#ifndef __CVC4__DECISION_ENGINE_H
#define __CVC4__DECISION_ENGINE_H
-#include "cvc4_config.h"
#include "expr/node.h"
namespace CVC4 {
** 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 {
+/********************* */
+/** 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;
** A multiprecision integer constant.
**/
+#include "cvc4_public.h"
+
#ifndef __CVC4__INTEGER_H
#define __CVC4__INTEGER_H
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);
** A model.
**/
+#include "cvc4_public.h"
+
#ifndef __CVC4__MODEL_H
#define __CVC4__MODEL_H
** 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 {
** Output utility classes and functions.
**/
-#include "cvc4_config.h"
-
#include <iostream>
#include "util/output.h"
** 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>
+/********************* */
+/** 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"
** different than the values used to construct the Rational.
**/
+#include "cvc4_public.h"
+
#ifndef __CVC4__RATIONAL_H
#define __CVC4__RATIONAL_H
};/* 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);
** Encapsulation of the result of a query.
**/
+#include "cvc4_public.h"
+
#ifndef __CVC4__RESULT_H
#define __CVC4__RESULT_H
# All unit tests
UNIT_TESTS = \
+ expr/expr_black \
expr/node_white \
expr/node_black \
expr/kind_black \
--- /dev/null
+/********************* */
+/** 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);
+ }
+};
#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);
*/
// 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);
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());
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());
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);
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);
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());
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);
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);
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);
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;
}
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());
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);
}
}
*/
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
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;
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);
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);
#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);
}
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);
// 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) {
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() {
projects / cvc5.git / commitdiff