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