Some parts split into other bugs: 19, 20, 21.
Addressed concerns of bug 11 (util package code review).
Slight parser source file modifications: file comments, #included
headers in generated parsers/lexers
Added CVC4::Result propagation back through
MiniSat->PropEngine->SmtEngine->main(). Silenced MiniSat when
verbosity is not requested.
# -*- makefile -*-
+#
+# This Makefile produces the Makefile in the top-level builds/
+# directory for standard-path builds (e.g., those configured from the
+# source tree). It has some autoconf cruft in it, documented below.
+#
+# Its main purposes are to:
+# 1. build the current build profile
+# 2. install into "builds/$(CURRENT_BUILD)/$(prefix)"
+# 3. set up "builds/$(CURRENT_BUILD)/{bin,lib}" symlinks
+# 4. install into "builds/$(prefix)"
+# 5. set up "builds/bin" and "builds/lib"
+#
+# Steps 2 and 4 require libtool-relinking for dynamically-linked
+# executables and libraries, since build/bin is not the final
+# installation path.
+# Include the "current" build profile.
include current
+# Set up $(MAKE)
@SET_MAKE@
+# Set up some basic autoconf make vars
install_sh = @install_sh@
mkinstalldirs = $(install_sh) -d
exec_prefix = @exec_prefix@
bindir = @bindir@
libdir = @libdir@
abs_builddir = @abs_builddir@
+
+# Are we building static/dynamic libraries? One or the other can be
+# on, or both.
BUILDING_STATIC = @BUILDING_STATIC@
BUILDING_SHARED = @BUILDING_SHARED@
.PHONY: _default_build_ all
_default_build_: all
all:
+# build the current build profile
(cd $(CURRENT_BUILD) && $(MAKE) $@)
+# set up builds/$(CURRENT_BUILD)/...prefix.../bin
+# and builds/$(CURRENT_BUILD)/...prefix.../lib
$(mkinstalldirs) "$(CURRENT_BUILD)$(bindir)" "$(CURRENT_BUILD)$(libdir)"
- $(CURRENT_BUILD)/libtool --mode=install install -v $(CURRENT_BUILD)/src/libcvc4.la "$(abs_builddir)$(libdir)"
- $(CURRENT_BUILD)/libtool --mode=install install -v $(CURRENT_BUILD)/src/parser/libcvc4parser.la "$(abs_builddir)$(libdir)"
+# install libcvc4
+ $(CURRENT_BUILD)/libtool --mode=install install -v \
+ $(CURRENT_BUILD)/src/libcvc4.la \
+ "$(abs_builddir)$(libdir)"
+# install libcvc4parser
+ $(CURRENT_BUILD)/libtool --mode=install install -v \
+ $(CURRENT_BUILD)/src/parser/libcvc4parser.la \
+ "$(abs_builddir)$(libdir)"
ifeq ($(BUILDING_SHARED),1)
- thelibdir="$(abs_builddir)$(libdir)"; progdir="$(abs_builddir)$(bindir)"; file=cvc4; \
+# if we're building shared libs, relink
+ thelibdir="$(abs_builddir)$(libdir)"; \
+ progdir="$(abs_builddir)$(bindir)"; file=cvc4; \
eval `grep '^relink_command=' $(CURRENT_BUILD)/src/main/cvc4 | sed 's:-Wl,-rpath:-Wl,-rpath -Wl,\\\\$$thelibdir -Wl,-rpath:'`; \
eval "(cd $(CURRENT_BUILD)/src/main && $$relink_command)"
endif
ifeq ($(BUILDING_STATIC),1)
- install -v $(CURRENT_BUILD)/src/main/cvc4 "$(abs_builddir)$(bindir)"
+# if we're building static libs, just install them directly
+ $(install_sh) \
+ $(CURRENT_BUILD)/src/main/cvc4 \
+ "$(abs_builddir)$(bindir)"
endif
+# set up builds/$(CURRENT_BUILD)/bin and builds/$(CURRENT_BUILD)/lib
test -e $(CURRENT_BUILD)/lib || ln -sfv "$(abs_builddir)$(libdir)" $(CURRENT_BUILD)/lib
test -e $(CURRENT_BUILD)/bin || ln -sfv "$(abs_builddir)$(bindir)" $(CURRENT_BUILD)/bin
- mkdir -pv ".$(bindir)" ".$(libdir)"
+# set up builds/...prefix.../bin and builds/...prefix.../lib
+ $(mkinstalldirs) ".$(bindir)" ".$(libdir)"
+# install libcvc4
$(CURRENT_BUILD)/libtool --mode=install install -v $(CURRENT_BUILD)/src/libcvc4.la "`pwd`$(libdir)"
+# install libcvc4parser
$(CURRENT_BUILD)/libtool --mode=install install -v $(CURRENT_BUILD)/src/parser/libcvc4parser.la "`pwd`$(libdir)"
ifeq ($(BUILDING_SHARED),1)
+# if we're building shared libs, relink
thelibdir="`pwd`$(libdir)"; progdir="`pwd`$(bindir)"; file=cvc4; \
eval `grep '^relink_command=' $(CURRENT_BUILD)/src/main/cvc4 | sed 's:-Wl,-rpath:-Wl,-rpath -Wl,\\\\$$thelibdir -Wl,-rpath:'`; \
eval "(cd $(CURRENT_BUILD)/src/main && $$relink_command)"
endif
ifeq ($(BUILDING_STATIC),1)
- install -v $(CURRENT_BUILD)/src/main/cvc4 "`pwd`$(bindir)"
+# if we're building static libs, just install them directly
+ $(install_sh) $(CURRENT_BUILD)/src/main/cvc4 "`pwd`$(bindir)"
endif
+# set up builds/bin and builds/lib
test -e lib || ln -sfv ".$(libdir)" lib
test -e bin || ln -sfv ".$(bindir)" bin
+# any other target than the default doesn't do the extra stuff above
%:
(cd $(CURRENT_BUILD) && $(MAKE) $@)
# usage: build-type profile [ overrides... ]
#
# Returns a build string for the given profile and overrides.
-# For example, "build-type debug noass" returns the canonical build
-# string for a debug build with assertions turned off.
+# For example, "build-type debug noassertions" returns the canonical
+# build string for a debug build with assertions turned off.
#
# The default build directory for CVC4 is then (assuming a standard
# debug build):
# top-level Makefile when you build another profile than the
# "current" build (to see if there already was a build of that type).
#
-# The codes for overrides are as follows:
+# The overrides are as follows:
#
-# opt - optimizing
-# dsy - debug symbols
-# ass - assertions
-# trc - tracing
-# mzl - muzzle
-# cvg - coverage
-# prf - profiling
+# optimized
+# debugsymbols
+# assertions
+# tracing
+# muzzle
+# coverage
+# profiling
#
if [ $# -eq 0 ]; then
done
build_type_suffix=
-for arg in opt dsy ass trc mzl cvg prf; do
+for arg in optimized debugsymbols assertions tracing muzzle coverage profiling; do
if eval [ -n '"${'$arg'+set}"' ]; then
if eval [ '"${'$arg'}"' -eq 0 ]; then
build_type_suffix=$build_type_suffix-no$arg
mk_include
CVC4_PARSER_LIBRARY_VERSION
CVC4_LIBRARY_VERSION
-CVC4_LIBRARY_RELEASE_CODE
BUILDING_STATIC
BUILDING_SHARED
ANTLR_LDFLAGS
# For guidance on when to change the version number, refer to the
# developer's guide.
-CVC4_LIBRARY_RELEASE_CODE=0:0:0
CVC4_LIBRARY_VERSION=0:0:0
CVC4_PARSER_LIBRARY_VERSION=0:0:0
-# really irritating: AC_CANONICAL_* bash $@
+# Using the AC_CANONICAL_* macros destroy the command line you get
+# from $@, which we want later for determining the build profile. So
+# we save it. (We can't do our build profile stuff here, or it's not
+# included in the output... autoconf overrides us on the orderings of
+# some things.)
config_cmdline="$@"
# turn off static lib building by default
btargs=
if test -n "${enable_optimized+set}"; then
if test "$enable_optimized" = yes; then
- btargs="$btargs opt"
+ btargs="$btargs optimized"
else
- btargs="$btargs noopt"
+ btargs="$btargs nooptimized"
fi
fi
if test -n "${enable_debug_symbols+set}"; then
if test "$enable_debug_symbols" = yes; then
- btargs="$btargs dsy"
+ btargs="$btargs debugsymbols"
else
- btargs="$btargs nodsy"
+ btargs="$btargs nodebugsymbols"
fi
fi
if test -n "${enable_assertions+set}"; then
if test "$enable_assertions" = yes; then
- btargs="$btargs ass"
+ btargs="$btargs assertions"
else
- btargs="$btargs noass"
+ btargs="$btargs noassertions"
fi
fi
if test -n "${enable_tracing+set}"; then
if test "$enable_tracing" = yes; then
- btargs="$btargs trc"
+ btargs="$btargs tracing"
else
- btargs="$btargs notrc"
+ btargs="$btargs notracing"
fi
fi
if test -n "${enable_muzzle+set}"; then
if test "$enable_muzzle" = yes; then
- btargs="$btargs mzl"
+ btargs="$btargs muzzle"
else
- btargs="$btargs nomzl"
+ btargs="$btargs nomuzzle"
fi
fi
if test -n "${enable_coverage+set}"; then
if test "$enable_coverage" = yes; then
- btargs="$btargs cvg"
+ btargs="$btargs coverage"
else
- btargs="$btargs nocvg"
+ btargs="$btargs nocoverage"
fi
fi
if test -n "${enable_profiling+set}"; then
if test "$enable_profiling" = yes; then
- btargs="$btargs prf"
+ btargs="$btargs profiling"
else
- btargs="$btargs noprf"
+ btargs="$btargs noprofiling"
fi
fi
{ $as_echo "$as_me:${as_lineno-$LINENO}: result: $with_build" >&5
{ $as_echo "$as_me:${as_lineno-$LINENO}: result: $build_type" >&5
$as_echo "$build_type" >&6; }
-# require building in target and build-specific build directory
+# Require building in target and build-specific build directory:
+#
+# If the configure script is invoked from the top-level source
+# directory, it creates a suitable build directory (based on the build
+# architecture and build profile from $build_type), changes into it,
+# and reinvokes itself. CVC4_CONFIGURE_IN_BUILDS is an envariable
+# that breaks any possibility of infinite recursion in this process.
{ $as_echo "$as_me:${as_lineno-$LINENO}: checking what dir to configure" >&5
$as_echo_n "checking what dir to configure... " >&6; }
if test "$CVC4_CONFIGURE_IN_BUILDS" = yes; then
ac_config_headers="$ac_config_headers config.h"
-# keep track of whether the user set these (check here, because
-# autoconf might set a default later)
-{ $as_echo "$as_me:${as_lineno-$LINENO}: checking for user CPPFLAGS" >&5
-$as_echo_n "checking for user CPPFLAGS... " >&6; }
-if test -z "${CPPFLAGS+set}"; then user_cppflags=no; else user_cppflags=yes; fi
-{ $as_echo "$as_me:${as_lineno-$LINENO}: result: ${CPPFLAGS-none}" >&5
-$as_echo "${CPPFLAGS-none}" >&6; }
-{ $as_echo "$as_me:${as_lineno-$LINENO}: checking for user CXXFLAGS" >&5
-$as_echo_n "checking for user CXXFLAGS... " >&6; }
-if test -z "${CXXFLAGS+set}"; then user_cxxflags=no; else user_cxxflags=yes; fi
-{ $as_echo "$as_me:${as_lineno-$LINENO}: result: ${CXXFLAGS-none}" >&5
-$as_echo "${CXXFLAGS-none}" >&6; }
-{ $as_echo "$as_me:${as_lineno-$LINENO}: checking for user LDFLAGS" >&5
-$as_echo_n "checking for user LDFLAGS... " >&6; }
-if test -z "${LDFLAGS+set}" ; then user_ldflags=no ; else user_ldflags=yes ; fi
-{ $as_echo "$as_me:${as_lineno-$LINENO}: result: ${LDFLAGS-none}" >&5
-$as_echo "${LDFLAGS-none}" >&6; }
-
-# Initialize libtools configuration options.
-
+# Initialize libtool's configuration options.
enable_win32_dll=yes
case $host in
-
case `pwd` in
*\ * | *\ *)
{ $as_echo "$as_me:${as_lineno-$LINENO}: WARNING: Libtool does not cope well with whitespace in \`pwd\`" >&5
else
lt_cv_nm_interface="BSD nm"
echo "int some_variable = 0;" > conftest.$ac_ext
- (eval echo "\"\$as_me:5461: $ac_compile\"" >&5)
+ (eval echo "\"\$as_me:5449: $ac_compile\"" >&5)
(eval "$ac_compile" 2>conftest.err)
cat conftest.err >&5
- (eval echo "\"\$as_me:5464: $NM \\\"conftest.$ac_objext\\\"\"" >&5)
+ (eval echo "\"\$as_me:5452: $NM \\\"conftest.$ac_objext\\\"\"" >&5)
(eval "$NM \"conftest.$ac_objext\"" 2>conftest.err > conftest.out)
cat conftest.err >&5
- (eval echo "\"\$as_me:5467: output\"" >&5)
+ (eval echo "\"\$as_me:5455: output\"" >&5)
cat conftest.out >&5
if $GREP 'External.*some_variable' conftest.out > /dev/null; then
lt_cv_nm_interface="MS dumpbin"
;;
*-*-irix6*)
# Find out which ABI we are using.
- echo '#line 6670 "configure"' > conftest.$ac_ext
+ echo '#line 6658 "configure"' > conftest.$ac_ext
if { { eval echo "\"\$as_me\":${as_lineno-$LINENO}: \"$ac_compile\""; } >&5
(eval $ac_compile) 2>&5
ac_status=$?
-e 's:.*FLAGS}\{0,1\} :&$lt_compiler_flag :; t' \
-e 's: [^ ]*conftest\.: $lt_compiler_flag&:; t' \
-e 's:$: $lt_compiler_flag:'`
- (eval echo "\"\$as_me:8138: $lt_compile\"" >&5)
+ (eval echo "\"\$as_me:8126: $lt_compile\"" >&5)
(eval "$lt_compile" 2>conftest.err)
ac_status=$?
cat conftest.err >&5
- echo "$as_me:8142: \$? = $ac_status" >&5
+ echo "$as_me:8130: \$? = $ac_status" >&5
if (exit $ac_status) && test -s "$ac_outfile"; then
# The compiler can only warn and ignore the option if not recognized
# So say no if there are warnings other than the usual output.
-e 's:.*FLAGS}\{0,1\} :&$lt_compiler_flag :; t' \
-e 's: [^ ]*conftest\.: $lt_compiler_flag&:; t' \
-e 's:$: $lt_compiler_flag:'`
- (eval echo "\"\$as_me:8477: $lt_compile\"" >&5)
+ (eval echo "\"\$as_me:8465: $lt_compile\"" >&5)
(eval "$lt_compile" 2>conftest.err)
ac_status=$?
cat conftest.err >&5
- echo "$as_me:8481: \$? = $ac_status" >&5
+ echo "$as_me:8469: \$? = $ac_status" >&5
if (exit $ac_status) && test -s "$ac_outfile"; then
# The compiler can only warn and ignore the option if not recognized
# So say no if there are warnings other than the usual output.
-e 's:.*FLAGS}\{0,1\} :&$lt_compiler_flag :; t' \
-e 's: [^ ]*conftest\.: $lt_compiler_flag&:; t' \
-e 's:$: $lt_compiler_flag:'`
- (eval echo "\"\$as_me:8582: $lt_compile\"" >&5)
+ (eval echo "\"\$as_me:8570: $lt_compile\"" >&5)
(eval "$lt_compile" 2>out/conftest.err)
ac_status=$?
cat out/conftest.err >&5
- echo "$as_me:8586: \$? = $ac_status" >&5
+ echo "$as_me:8574: \$? = $ac_status" >&5
if (exit $ac_status) && test -s out/conftest2.$ac_objext
then
# The compiler can only warn and ignore the option if not recognized
-e 's:.*FLAGS}\{0,1\} :&$lt_compiler_flag :; t' \
-e 's: [^ ]*conftest\.: $lt_compiler_flag&:; t' \
-e 's:$: $lt_compiler_flag:'`
- (eval echo "\"\$as_me:8637: $lt_compile\"" >&5)
+ (eval echo "\"\$as_me:8625: $lt_compile\"" >&5)
(eval "$lt_compile" 2>out/conftest.err)
ac_status=$?
cat out/conftest.err >&5
- echo "$as_me:8641: \$? = $ac_status" >&5
+ echo "$as_me:8629: \$? = $ac_status" >&5
if (exit $ac_status) && test -s out/conftest2.$ac_objext
then
# The compiler can only warn and ignore the option if not recognized
lt_dlunknown=0; lt_dlno_uscore=1; lt_dlneed_uscore=2
lt_status=$lt_dlunknown
cat > conftest.$ac_ext <<_LT_EOF
-#line 11020 "configure"
+#line 11008 "configure"
#include "confdefs.h"
#if HAVE_DLFCN_H
lt_dlunknown=0; lt_dlno_uscore=1; lt_dlneed_uscore=2
lt_status=$lt_dlunknown
cat > conftest.$ac_ext <<_LT_EOF
-#line 11116 "configure"
+#line 11104 "configure"
#include "confdefs.h"
#if HAVE_DLFCN_H
-e 's:.*FLAGS}\{0,1\} :&$lt_compiler_flag :; t' \
-e 's: [^ ]*conftest\.: $lt_compiler_flag&:; t' \
-e 's:$: $lt_compiler_flag:'`
- (eval echo "\"\$as_me:14671: $lt_compile\"" >&5)
+ (eval echo "\"\$as_me:14659: $lt_compile\"" >&5)
(eval "$lt_compile" 2>conftest.err)
ac_status=$?
cat conftest.err >&5
- echo "$as_me:14675: \$? = $ac_status" >&5
+ echo "$as_me:14663: \$? = $ac_status" >&5
if (exit $ac_status) && test -s "$ac_outfile"; then
# The compiler can only warn and ignore the option if not recognized
# So say no if there are warnings other than the usual output.
-e 's:.*FLAGS}\{0,1\} :&$lt_compiler_flag :; t' \
-e 's: [^ ]*conftest\.: $lt_compiler_flag&:; t' \
-e 's:$: $lt_compiler_flag:'`
- (eval echo "\"\$as_me:14770: $lt_compile\"" >&5)
+ (eval echo "\"\$as_me:14758: $lt_compile\"" >&5)
(eval "$lt_compile" 2>out/conftest.err)
ac_status=$?
cat out/conftest.err >&5
- echo "$as_me:14774: \$? = $ac_status" >&5
+ echo "$as_me:14762: \$? = $ac_status" >&5
if (exit $ac_status) && test -s out/conftest2.$ac_objext
then
# The compiler can only warn and ignore the option if not recognized
-e 's:.*FLAGS}\{0,1\} :&$lt_compiler_flag :; t' \
-e 's: [^ ]*conftest\.: $lt_compiler_flag&:; t' \
-e 's:$: $lt_compiler_flag:'`
- (eval echo "\"\$as_me:14822: $lt_compile\"" >&5)
+ (eval echo "\"\$as_me:14810: $lt_compile\"" >&5)
(eval "$lt_compile" 2>out/conftest.err)
ac_status=$?
cat out/conftest.err >&5
- echo "$as_me:14826: \$? = $ac_status" >&5
+ echo "$as_me:14814: \$? = $ac_status" >&5
if (exit $ac_status) && test -s out/conftest2.$ac_objext
then
# The compiler can only warn and ignore the option if not recognized
+CPPFLAGS="${CPPFLAGS:+$CPPFLAGS }$CVC4CPPFLAGS"
+CXXFLAGS="${CXXFLAGS:+$CXXFLAGS }$CVC4CXXFLAGS"
+LDFLAGS="${LDFLAGS:+$LDFLAGS }$CVC4LDFLAGS"
-if test "$user_cppflags" = no; then
- CPPFLAGS="$CVC4CPPFLAGS"
-fi
-if test "$user_cxxflags" = no; then
- CXXFLAGS="$CVC4CXXFLAGS"
-fi
-if test "$user_ldflags" = no; then
- LDFLAGS="$CVC4LDFLAGS"
-fi
-
+# mk_include
+#
+# When automake scans Makefiles, it complains about non-standard make
+# features (including GNU extensions), and breaks GNU Make's
+# "if/endif" construct, replacing the "if" with AM_CONDITIONAL if
+# constructs. automake even follows "include" and messes with
+# included Makefiles.
+#
+# CVC4 assumes GNU Make and we want to use GNU Make if/endifs, so we
+# have to hide some included Makefiles with GNU extensions. We do
+# this by defining mk_include as an autoconf substitution and then
+# using "@mk_include@ other_makefile" in Makefile.am to include
+# makefiles with GNU extensions; this hides them from automake.
mk_include=include
+othermakefiles="`find src -name Makefile.am | sed 's,\.am$,,'` `find test -name Makefile.am | sed 's,\.am$,,'`"
+
ac_config_files="$ac_config_files Makefile.builds Makefile contrib/Makefile doc/Makefile src/Makefile src/expr/Makefile src/smt/Makefile src/main/Makefile src/prop/minisat/Makefile src/prop/Makefile src/util/Makefile src/context/Makefile src/parser/Makefile src/parser/cvc/Makefile src/parser/smt/Makefile src/theory/Makefile src/theory/uf/Makefile test/Makefile test/regress/Makefile test/system/Makefile test/unit/Makefile"
CXXFLAGS : $CXXFLAGS
LDFLAGS : $LDFLAGS
-Library releases : $CVC4_LIBRARY_RELEASE_CODE
libcvc4 version : $CVC4_LIBRARY_VERSION
libcvc4parser version: $CVC4_PARSER_LIBRARY_VERSION
Now just type make, followed by make check or make install, as you like.
-You can use 'make <build_profile>' to reconfig/build a different profile.
-Build profiles: production optimized default competition
-
EOF
-
-if test "$user_cppflags" = yes; then
- { $as_echo "$as_me:${as_lineno-$LINENO}: WARNING: " >&5
-$as_echo "$as_me: WARNING: " >&2;}
- { $as_echo "$as_me:${as_lineno-$LINENO}: WARNING: I won't override your CPPFLAGS setting. But some of your build options to configure may not be honored." >&5
-$as_echo "$as_me: WARNING: I won't override your CPPFLAGS setting. But some of your build options to configure may not be honored." >&2;}
- { $as_echo "$as_me:${as_lineno-$LINENO}: WARNING: To support your options to configure, I would like to set CPPFLAGS to:" >&5
-$as_echo "$as_me: WARNING: To support your options to configure, I would like to set CPPFLAGS to:" >&2;}
- { $as_echo "$as_me:${as_lineno-$LINENO}: WARNING: $CVC4CPPFLAGS" >&5
-$as_echo "$as_me: WARNING: $CVC4CPPFLAGS" >&2;}
- { $as_echo "$as_me:${as_lineno-$LINENO}: WARNING: " >&5
-$as_echo "$as_me: WARNING: " >&2;}
-fi
-if test "$user_cxxflags" = yes; then
- { $as_echo "$as_me:${as_lineno-$LINENO}: WARNING: " >&5
-$as_echo "$as_me: WARNING: " >&2;}
- { $as_echo "$as_me:${as_lineno-$LINENO}: WARNING: I won't override your CXXFLAGS setting. But some of your build options to configure may not be honored." >&5
-$as_echo "$as_me: WARNING: I won't override your CXXFLAGS setting. But some of your build options to configure may not be honored." >&2;}
- { $as_echo "$as_me:${as_lineno-$LINENO}: WARNING: To support your options to configure, I would like to set CXXFLAGS to:" >&5
-$as_echo "$as_me: WARNING: To support your options to configure, I would like to set CXXFLAGS to:" >&2;}
- { $as_echo "$as_me:${as_lineno-$LINENO}: WARNING: $CVC4CXXFLAGS" >&5
-$as_echo "$as_me: WARNING: $CVC4CXXFLAGS" >&2;}
- { $as_echo "$as_me:${as_lineno-$LINENO}: WARNING: " >&5
-$as_echo "$as_me: WARNING: " >&2;}
-fi
-if test "$user_ldflags" = yes; then
- { $as_echo "$as_me:${as_lineno-$LINENO}: WARNING: " >&5
-$as_echo "$as_me: WARNING: " >&2;}
- { $as_echo "$as_me:${as_lineno-$LINENO}: WARNING: I won't override your LDFLAGS setting. But some of your build options to configure may not be honored." >&5
-$as_echo "$as_me: WARNING: I won't override your LDFLAGS setting. But some of your build options to configure may not be honored." >&2;}
- { $as_echo "$as_me:${as_lineno-$LINENO}: WARNING: To support your options to configure, I would like to set LDFLAGS to:" >&5
-$as_echo "$as_me: WARNING: To support your options to configure, I would like to set LDFLAGS to:" >&2;}
- { $as_echo "$as_me:${as_lineno-$LINENO}: WARNING: $CVC4LDFLAGS" >&5
-$as_echo "$as_me: WARNING: $CVC4LDFLAGS" >&2;}
- { $as_echo "$as_me:${as_lineno-$LINENO}: WARNING: " >&5
-$as_echo "$as_me: WARNING: " >&2;}
-fi
# For guidance on when to change the version number, refer to the
# developer's guide.
-CVC4_LIBRARY_RELEASE_CODE=0:0:0
CVC4_LIBRARY_VERSION=0:0:0
CVC4_PARSER_LIBRARY_VERSION=0:0:0
-# really irritating: AC_CANONICAL_* bash $@
+# Using the AC_CANONICAL_* macros destroy the command line you get
+# from $@, which we want later for determining the build profile. So
+# we save it. (We can't do our build profile stuff here, or it's not
+# included in the output... autoconf overrides us on the orderings of
+# some things.)
config_cmdline="$@"
# turn off static lib building by default
btargs=
if test -n "${enable_optimized+set}"; then
if test "$enable_optimized" = yes; then
- btargs="$btargs opt"
+ btargs="$btargs optimized"
else
- btargs="$btargs noopt"
+ btargs="$btargs nooptimized"
fi
fi
if test -n "${enable_debug_symbols+set}"; then
if test "$enable_debug_symbols" = yes; then
- btargs="$btargs dsy"
+ btargs="$btargs debugsymbols"
else
- btargs="$btargs nodsy"
+ btargs="$btargs nodebugsymbols"
fi
fi
if test -n "${enable_assertions+set}"; then
if test "$enable_assertions" = yes; then
- btargs="$btargs ass"
+ btargs="$btargs assertions"
else
- btargs="$btargs noass"
+ btargs="$btargs noassertions"
fi
fi
if test -n "${enable_tracing+set}"; then
if test "$enable_tracing" = yes; then
- btargs="$btargs trc"
+ btargs="$btargs tracing"
else
- btargs="$btargs notrc"
+ btargs="$btargs notracing"
fi
fi
if test -n "${enable_muzzle+set}"; then
if test "$enable_muzzle" = yes; then
- btargs="$btargs mzl"
+ btargs="$btargs muzzle"
else
- btargs="$btargs nomzl"
+ btargs="$btargs nomuzzle"
fi
fi
if test -n "${enable_coverage+set}"; then
if test "$enable_coverage" = yes; then
- btargs="$btargs cvg"
+ btargs="$btargs coverage"
else
- btargs="$btargs nocvg"
+ btargs="$btargs nocoverage"
fi
fi
if test -n "${enable_profiling+set}"; then
if test "$enable_profiling" = yes; then
- btargs="$btargs prf"
+ btargs="$btargs profiling"
else
- btargs="$btargs noprf"
+ btargs="$btargs noprofiling"
fi
fi
AC_MSG_RESULT([$with_build])
fi
AC_MSG_RESULT($build_type)
-# require building in target and build-specific build directory
+# Require building in target and build-specific build directory:
+#
+# If the configure script is invoked from the top-level source
+# directory, it creates a suitable build directory (based on the build
+# architecture and build profile from $build_type), changes into it,
+# and reinvokes itself. CVC4_CONFIGURE_IN_BUILDS is an envariable
+# that breaks any possibility of infinite recursion in this process.
AC_MSG_CHECKING([what dir to configure])
if test "$CVC4_CONFIGURE_IN_BUILDS" = yes; then
AC_MSG_RESULT([this one (in builds/)])
AM_INIT_AUTOMAKE(cvc4, $CVC4_RELEASE)
AC_CONFIG_HEADERS([config.h])
-# keep track of whether the user set these (check here, because
-# autoconf might set a default later)
-AC_MSG_CHECKING([for user CPPFLAGS])
-if test -z "${CPPFLAGS+set}"; then user_cppflags=no; else user_cppflags=yes; fi
-AC_MSG_RESULT([${CPPFLAGS-none}])
-AC_MSG_CHECKING([for user CXXFLAGS])
-if test -z "${CXXFLAGS+set}"; then user_cxxflags=no; else user_cxxflags=yes; fi
-AC_MSG_RESULT([${CXXFLAGS-none}])
-AC_MSG_CHECKING([for user LDFLAGS])
-if test -z "${LDFLAGS+set}" ; then user_ldflags=no ; else user_ldflags=yes ; fi
-AC_MSG_RESULT([${LDFLAGS-none}])
-
-# Initialize libtools configuration options.
-
+# Initialize libtool's configuration options.
_LT_SET_OPTION([LT_INIT],[win32-dll])
-
-dnl defined in config/libtools.m4
LT_INIT
# Checks for programs.
AC_SUBST(BUILDING_SHARED)
AC_SUBST(BUILDING_STATIC)
-AC_SUBST(CVC4_LIBRARY_RELEASE_CODE)
AC_SUBST(CVC4_LIBRARY_VERSION)
AC_SUBST(CVC4_PARSER_LIBRARY_VERSION)
-if test "$user_cppflags" = no; then
- CPPFLAGS="$CVC4CPPFLAGS"
-fi
-if test "$user_cxxflags" = no; then
- CXXFLAGS="$CVC4CXXFLAGS"
-fi
-if test "$user_ldflags" = no; then
- LDFLAGS="$CVC4LDFLAGS"
-fi
+CPPFLAGS="${CPPFLAGS:+$CPPFLAGS }$CVC4CPPFLAGS"
+CXXFLAGS="${CXXFLAGS:+$CXXFLAGS }$CVC4CXXFLAGS"
+LDFLAGS="${LDFLAGS:+$LDFLAGS }$CVC4LDFLAGS"
+# mk_include
+#
+# When automake scans Makefiles, it complains about non-standard make
+# features (including GNU extensions), and breaks GNU Make's
+# "if/endif" construct, replacing the "if" with AM_CONDITIONAL if
+# constructs. automake even follows "include" and messes with
+# included Makefiles.
+#
+# CVC4 assumes GNU Make and we want to use GNU Make if/endifs, so we
+# have to hide some included Makefiles with GNU extensions. We do
+# this by defining mk_include as an autoconf substitution and then
+# using "@mk_include@ other_makefile" in Makefile.am to include
+# makefiles with GNU extensions; this hides them from automake.
mk_include=include
AC_SUBST(mk_include)
+othermakefiles="`find src -name Makefile.am | sed 's,\.am$,,'` `find test -name Makefile.am | sed 's,\.am$,,'`"
+
AC_CONFIG_FILES([
Makefile.builds
Makefile
CXXFLAGS : $CXXFLAGS
LDFLAGS : $LDFLAGS
-Library releases : $CVC4_LIBRARY_RELEASE_CODE
libcvc4 version : $CVC4_LIBRARY_VERSION
libcvc4parser version: $CVC4_PARSER_LIBRARY_VERSION
Now just type make, followed by make check or make install, as you like.
-You can use 'make <build_profile>' to reconfig/build a different profile.
-Build profiles: production optimized default competition
-
EOF
-
-if test "$user_cppflags" = yes; then
- AC_MSG_WARN([])
- AC_MSG_WARN([I won't override your CPPFLAGS setting. But some of your build options to configure may not be honored.])
- AC_MSG_WARN([To support your options to configure, I would like to set CPPFLAGS to:])
- AC_MSG_WARN([ $CVC4CPPFLAGS])
- AC_MSG_WARN([])
-fi
-if test "$user_cxxflags" = yes; then
- AC_MSG_WARN([])
- AC_MSG_WARN([I won't override your CXXFLAGS setting. But some of your build options to configure may not be honored.])
- AC_MSG_WARN([To support your options to configure, I would like to set CXXFLAGS to:])
- AC_MSG_WARN([ $CVC4CXXFLAGS])
- AC_MSG_WARN([])
-fi
-if test "$user_ldflags" = yes; then
- AC_MSG_WARN([])
- AC_MSG_WARN([I won't override your LDFLAGS setting. But some of your build options to configure may not be honored.])
- AC_MSG_WARN([To support your options to configure, I would like to set LDFLAGS to:])
- AC_MSG_WARN([ $CVC4LDFLAGS])
- AC_MSG_WARN([])
-fi
# set to zero if interfaces have been removed
# or changed
#
-# LIBCVC4_RELEASE (-release) should match the CVC4 release version
-#
-LIBCVC4_RELEASE = @CVC4_LIBRARY_RELEASE_CODE@
LIBCVC4_VERSION = @CVC4_LIBRARY_VERSION@
AM_CPPFLAGS =
noinst_LTLIBRARIES = libcvc4_noinst.la
-libcvc4_la_LDFLAGS = -version-info $(LIBCVC4_VERSION) -release $(LIBCVC4_RELEASE)
+libcvc4_la_LDFLAGS = -version-info $(LIBCVC4_VERSION)
libcvc4_la_LINK = $(CXXLINK)
libcvc4_la_SOURCES =
#include "expr/expr_manager.h"
#include "smt/smt_engine.h"
#include "util/command.h"
+#include "util/result.h"
#include "util/Assert.h"
#include "util/output.h"
#include "util/options.h"
using namespace CVC4::parser;
using namespace CVC4::main;
-int main(int argc, char *argv[]) {
+static Result lastResult;
+static struct Options options;
+
+void doCommand(SmtEngine&, Command*);
- struct Options options;
+int main(int argc, char *argv[]) {
try {
// Parse and execute commands until we are done
Command* cmd;
while((cmd = parser->parseNextCommand())) {
- if(options.verbosity > 0) {
- cout << "Invoking: " << *cmd << endl;
- }
- cmd->invoke(&smt);
+ doCommand(smt, cmd);
delete cmd;
}
abort();
}
+ // TODO: adjust return value based on lastResult
return 0;
}
+
+void doCommand(SmtEngine& smt, Command* cmd) {
+ CommandSequence *seq = dynamic_cast<CommandSequence*>(cmd);
+ if(seq != NULL) {
+ for(CommandSequence::iterator subcmd = seq->begin();
+ subcmd != seq->end();
+ ++subcmd) {
+ doCommand(smt, *subcmd);
+ }
+ } else {
+ if(options.verbosity > 0) {
+ cout << "Invoking: " << *cmd << endl;
+ }
+
+ cmd->invoke(&smt);
+
+ QueryCommand *qc = dynamic_cast<QueryCommand*>(cmd);
+ if(qc != NULL) {
+ lastResult = qc->getResult();
+ if(options.verbosity >= 0) {
+ cout << lastResult << endl;
+ }
+ } else {
+ CheckSatCommand *csc = dynamic_cast<CheckSatCommand*>(cmd);
+ if(csc != NULL) {
+ lastResult = csc->getResult();
+ if(options.verbosity >= 0) {
+ cout << lastResult << endl;
+ }
+ }
+ }
+ }
+}
# set to zero if interfaces have been removed
# or changed
#
-# LIBCVC4PARSER_RELEASE (-release) should match the CVC4 release version
-#
-LIBCVC4PARSER_RELEASE = @CVC4_LIBRARY_RELEASE_CODE@
LIBCVC4PARSER_VERSION = @CVC4_PARSER_LIBRARY_VERSION@
AM_CPPFLAGS = \
nobase_lib_LTLIBRARIES = libcvc4parser.la
noinst_LTLIBRARIES = libcvc4parser_noinst.la
-libcvc4parser_la_LDFLAGS = $(ANTLR_LDFLAGS)
+libcvc4parser_la_LDFLAGS = $(ANTLR_LDFLAGS) \
+ -version-info $(LIBCVC4PARSER_VERSION)
libcvc4parser_la_LIBADD = libcvc4parser_noinst.la
libcvc4parser_la_LINK = $(CXXLINK)
#include "antlr_parser.h"
#include "util/output.h"
#include "util/Assert.h"
+#include "util/command.h"
using namespace std;
using namespace CVC4;
#include "expr/expr.h"
#include "expr/expr_manager.h"
-#include "util/command.h"
#include "util/Assert.h"
#include "parser/symbol_table.h"
namespace CVC4 {
+
+class Command;
+
namespace parser {
/**
+/* cvc_lexer.g
+ * Original author: dejan
+ * Major contributors:
+ * Minor contributors (to current version): none
+ * This file is part of the CVC4 prototype.
+ * Copyright (c) 2009 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.
+ *
+ * Lexer for CVC presentation language.
+ */
+
options {
language = "Cpp"; // C++ output for antlr
namespaceStd = "std"; // Cosmetic option to get rid of long defines in generated code
namespaceAntlr = "antlr"; // Cosmetic option to get rid of long defines in generated code
namespace = "CVC4::parser"; // Wrap everything in the smtparser namespace
}
-
+
/**
- * AntlrCvcLexer class is a stream tokenizer (lexer) for the CVC language.
+ * AntlrCvcLexer class is a stream tokenizer (lexer) for the CVC language.
*/
class AntlrCvcLexer extends Lexer;
exportVocab = CvcVocabulary; // Name of the shared token vocabulary
testLiterals = false; // Do not check for literals by default
defaultErrorHandler = false; // Skip the defaul error handling, just break with exceptions
- k = 2;
+ k = 2;
}
-
+
/*
* The tokens that might match with the identifiers go here. Otherwise define
* them below.
*/
tokens {
- // Types
+ // Types
BOOLEAN = "BOOLEAN";
// Boolean oparators
AND = "AND";
CHECKSAT = "CHECKSAT";
PRINT = "PRINT";
ECHO = "ECHO";
-
+
PUSH = "PUSH";
POP = "POP";
POPTO = "POPTO";
/**
* Matches any letter ('a'-'z' and 'A'-'Z').
*/
-protected
-ALPHA options { paraphrase = "a letter"; }
- : 'a'..'z'
+protected
+ALPHA options { paraphrase = "a letter"; }
+ : 'a'..'z'
| 'A'..'Z'
;
-
+
/**
* Matches the digits (0-9)
*/
-protected
-DIGIT options { paraphrase = "a digit"; }
+protected
+DIGIT options { paraphrase = "a digit"; }
: '0'..'9'
;
/**
* Matches the ':'
*/
-COLON options { paraphrase = "a colon"; }
+COLON options { paraphrase = "a colon"; }
: ':'
;
/**
* Matches the 'l'
*/
-SEMICOLON options { paraphrase = "a semicolon"; }
+SEMICOLON options { paraphrase = "a semicolon"; }
: ';'
;
/**
* Matches an identifier from the input. An identifier is a sequence of letters,
- * digits and "_", "'", "." symbols, starting with a letter.
+ * digits and "_", "'", "." symbols, starting with a letter.
*/
IDENTIFIER options { paraphrase = "an identifier"; testLiterals = true; }
: ALPHA (ALPHA | DIGIT | '_' | '\'' | '.')*
;
-
+
/**
* Matches the left bracket ('(').
*/
-LPAREN options { paraphrase = "a left parenthesis '('"; }
+LPAREN options { paraphrase = "a left parenthesis '('"; }
: '(';
-
+
/**
* Matches the right bracket ('(').
*/
-RPAREN options { paraphrase = "a right parenthesis ')'"; }
+RPAREN options { paraphrase = "a right parenthesis ')'"; }
: ')';
/**
- * Matches and skips whitespace in the input and ignores it.
+ * Matches and skips whitespace in the input and ignores it.
*/
WHITESPACE options { paraphrase = "whitespace"; }
: (' ' | '\t' | '\f') { $setType(antlr::Token::SKIP); }
/**
* Matches and skips the newline symbols in the input.
*/
-NEWLINE options { paraphrase = "a newline"; }
+NEWLINE options { paraphrase = "a newline"; }
: ('\r' '\n' | '\r' | '\n') { $setType(antlr::Token::SKIP); newline(); }
;
COMMENT options { paraphrase = "comment"; }
: '%' (~('\n' | '\r'))* { $setType(antlr::Token::SKIP); }
;
-
+
/**
* Matches a numeral from the input (non-empty sequence of digits).
*/
NUMERAL options { paraphrase = "a numeral"; }
: (DIGIT)+
;
-
\ No newline at end of file
+/* cvc_parser.g
+ * Original author: dejan
+ * Major contributors:
+ * Minor contributors (to current version): none
+ * This file is part of the CVC4 prototype.
+ * Copyright (c) 2009 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.
+ *
+ * Parser for CVC presentation language.
+ */
+
header "post_include_hpp" {
#include "parser/antlr_parser.h"
+#include "util/command.h"
}
header "post_include_cpp" {
-#include <vector>
+#include <vector>
using namespace std;
using namespace CVC4;
using namespace CVC4::parser;
}
-
+
options {
language = "Cpp"; // C++ output for antlr
namespaceStd = "std"; // Cosmetic option to get rid of long defines in generated code
namespaceAntlr = "antlr"; // Cosmetic option to get rid of long defines in generated code
namespace = "CVC4::parser"; // Wrap everything in the smtparser namespace
}
-
+
/**
- * AntlrCvcParser class is the parser for the files in CVC format.
+ * AntlrCvcParser class is the parser for the files in CVC format.
*/
class AntlrCvcParser extends Parser("AntlrParser");
options {
defaultErrorHandler = false; // Skip the defaul error handling, just break with exceptions
k = 2;
}
-
+
/**
* Parses the next command.
* @return command or 0 if EOF
: expr = formula
| EOF
;
-
+
/**
- * Matches a command of the input. If a declaration, it will return an empty
+ * Matches a command of the input. If a declaration, it will return an empty
* command.
*/
command returns [CVC4::Command* cmd = 0]
| QUERY f = formula SEMICOLON { cmd = new QueryCommand(f); }
| CHECKSAT f = formula SEMICOLON { cmd = new CheckSatCommand(f); }
| CHECKSAT SEMICOLON { cmd = new CheckSatCommand(); }
- | identifierList[ids, CHECK_UNDECLARED] COLON type {
+ | identifierList[ids, CHECK_UNDECLARED] COLON type {
// FIXME: switch on type (may not be predicates)
vector<string> sorts;
- newPredicates(ids,sorts);
- cmd = new DeclarationCommand(ids);
+ newPredicates(ids,sorts);
+ cmd = new DeclarationCommand(ids);
}
SEMICOLON
- | EOF
+ | EOF
;
/**
- * Mathches a list of identifiers separated by a comma and puts them in the
+ * Mathches a list of identifiers separated by a comma and puts them in the
* given list.
* @param idList the list to fill with identifiers.
- * @param check what kinds of check to perform on the symbols
+ * @param check what kinds of check to perform on the symbols
*/
identifierList[std::vector<std::string>& idList, DeclarationCheck check = CHECK_NONE]
{
string id;
}
- : id = identifier[check] { idList.push_back(id); }
+ : id = identifier[check] { idList.push_back(id); }
(COMMA id = identifier[check] { idList.push_back(id); })*
;
-
+
/**
* Matches an identifier and returns a string.
*/
identifier[DeclarationCheck check = CHECK_NONE] returns [std::string id]
- : x:IDENTIFIER
+ : x:IDENTIFIER
{ id = x->getText(); }
{ checkDeclaration(id, check) }?
exception catch [antlr::SemanticException& ex] {
case CHECK_DECLARED: rethrow(ex, "Symbol " + id + " not declared");
case CHECK_UNDECLARED: rethrow(ex, "Symbol " + id + " already declared");
default: throw ex;
- }
- }
+ }
+ }
;
-
-/**
+
+/**
* Matches a type.
* TODO: parse more types
*/
: BOOLEAN
;
-/**
+/**
* Matches a CVC4 formula.
* @return the expression representing the formula
- */
+ */
formula returns [CVC4::Expr formula]
: formula = boolFormula
;
* createPrecedenceExpr method to build the expression using the precedence
* and associativity of the operators.
* @return the expression representing the formula
- */
+ */
boolFormula returns [CVC4::Expr formula]
- : formula = boolAndFormula
+ : formula = boolAndFormula
;
/**
- * Matches a Boolean AND formula of a given kind by doing a recursive descent.
+ * Matches a Boolean AND formula of a given kind by doing a recursive descent.
*/
boolAndFormula returns [CVC4::Expr andFormula]
{
Expr e;
vector<Expr> exprs;
}
- : e = boolXorFormula { exprs.push_back(e); }
+ : e = boolXorFormula { exprs.push_back(e); }
( AND e = boolXorFormula { exprs.push_back(e); } )*
- {
- andFormula = (exprs.size() > 1 ? mkExpr(CVC4::AND, exprs) : exprs[0]);
- }
+ {
+ andFormula = (exprs.size() > 1 ? mkExpr(CVC4::AND, exprs) : exprs[0]);
+ }
;
/**
- * Matches a Boolean XOR formula of a given kind by doing a recursive descent.
+ * Matches a Boolean XOR formula of a given kind by doing a recursive descent.
*/
boolXorFormula returns [CVC4::Expr xorFormula]
{
Expr e;
vector<Expr> exprs;
}
- : e = boolOrFormula { exprs.push_back(e); }
+ : e = boolOrFormula { exprs.push_back(e); }
( XOR e = boolOrFormula { exprs.push_back(e); } )*
- {
- xorFormula = (exprs.size() > 1 ? mkExpr(CVC4::XOR, exprs) : exprs[0]);
- }
+ {
+ xorFormula = (exprs.size() > 1 ? mkExpr(CVC4::XOR, exprs) : exprs[0]);
+ }
;
/**
- * Matches a Boolean OR formula of a given kind by doing a recursive descent.
+ * Matches a Boolean OR formula of a given kind by doing a recursive descent.
*/
boolOrFormula returns [CVC4::Expr orFormula]
{
Expr e;
vector<Expr> exprs;
}
- : e = boolImpliesFormula { exprs.push_back(e); }
+ : e = boolImpliesFormula { exprs.push_back(e); }
( OR e = boolImpliesFormula { exprs.push_back(e); } )*
- {
- orFormula = (exprs.size() > 1 ? mkExpr(CVC4::OR, exprs) : exprs[0]);
- }
+ {
+ orFormula = (exprs.size() > 1 ? mkExpr(CVC4::OR, exprs) : exprs[0]);
+ }
;
/**
- * Matches a Boolean IMPLIES formula of a given kind by doing a recursive descent.
+ * Matches a Boolean IMPLIES formula of a given kind by doing a recursive descent.
*/
boolImpliesFormula returns [CVC4::Expr impliesFormula]
{
vector<Expr> exprs;
Expr e;
}
- : e = boolIffFormula { exprs.push_back(e); }
- ( IMPLIES e = boolIffFormula { exprs.push_back(e); }
+ : e = boolIffFormula { exprs.push_back(e); }
+ ( IMPLIES e = boolIffFormula { exprs.push_back(e); }
)*
{
- impliesFormula = exprs.back();
+ impliesFormula = exprs.back();
for (int i = exprs.size() - 2; i >= 0; -- i) {
impliesFormula = mkExpr(CVC4::IMPLIES, exprs[i], impliesFormula);
}
;
/**
- * Matches a Boolean IFF formula of a given kind by doing a recursive descent.
+ * Matches a Boolean IFF formula of a given kind by doing a recursive descent.
*/
boolIffFormula returns [CVC4::Expr iffFormula]
{
Expr e;
}
- : iffFormula = primaryBoolFormula
- ( IFF e = primaryBoolFormula
- { iffFormula = mkExpr(CVC4::IFF, iffFormula, e); }
+ : iffFormula = primaryBoolFormula
+ ( IFF e = primaryBoolFormula
+ { iffFormula = mkExpr(CVC4::IFF, iffFormula, e); }
)*
;
-
+
/**
- * Parses a primary Boolean formula. A primary Boolean formula is either a
- * Boolean atom (variables and predicates) a negation of a primary Boolean
+ * Parses a primary Boolean formula. A primary Boolean formula is either a
+ * Boolean atom (variables and predicates) a negation of a primary Boolean
* formula or a formula enclosed in parenthesis.
* @return the expression representing the formula
*/
/**
* Parses the Boolean atoms (variables and predicates).
* @return the expression representing the atom.
- */
+ */
boolAtom returns [CVC4::Expr atom]
{
string p;
| TRUE { atom = getTrueExpr(); }
| FALSE { atom = getFalseExpr(); }
;
-
+
/**
* Parses a predicate symbol (an identifier).
- * @param what kind of check to perform on the id
+ * @param what kind of check to perform on the id
* @return the predicate symol
*/
predicateSymbol[DeclarationCheck check = CHECK_NONE] returns [std::string pSymbol]
: pSymbol = identifier[check]
;
-
#include <string>
#include <iostream>
+
#include "cvc4_config.h"
#include "parser/parser_exception.h"
#include "util/Assert.h"
-#include "antlr_parser.h"
namespace antlr {
class CharScanner;
namespace parser {
+class AntlrParser;
+
/**
* The parser. The parser should be obtained by calling the static methods
* getNewParser, and should be deleted when done.
+/* smt_lexer.g
+ * Original author: dejan
+ * Major contributors:
+ * Minor contributors (to current version): none
+ * This file is part of the CVC4 prototype.
+ * Copyright (c) 2009 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.
+ *
+ * Lexer for SMT-LIB input language.
+ */
+
options {
language = "Cpp"; // C++ output for antlr
namespaceStd = "std"; // Cosmetic option to get rid of long defines in generated code
namespaceAntlr = "antlr"; // Cosmetic option to get rid of long defines in generated code
namespace = "CVC4::parser"; // Wrap everything in the smtparser namespace
}
-
+
/**
- * AntlrSmtLexer class is a stream tokenizer (lexer) for the SMT-LIB benchmark
- * language.
+ * AntlrSmtLexer class is a stream tokenizer (lexer) for the SMT-LIB benchmark
+ * language.
*/
class AntlrSmtLexer extends Lexer;
exportVocab = SmtVocabulary; // Name of the shared token vocabulary
testLiterals = false; // Do not check for literals by default
defaultErrorHandler = false; // Skip the default error handling, just break with exceptions
- k = 2;
+ k = 2;
}
-
+
tokens {
// Base SMT-LIB tokens
DISTINCT = "distinct";
/**
* Matches any letter ('a'-'z' and 'A'-'Z').
*/
-protected
-ALPHA options { paraphrase = "a letter"; }
- : 'a'..'z'
+protected
+ALPHA options { paraphrase = "a letter"; }
+ : 'a'..'z'
| 'A'..'Z'
;
-
+
/**
* Matches the digits (0-9)
*/
-protected
-DIGIT options { paraphrase = "a digit"; }
+protected
+DIGIT options { paraphrase = "a digit"; }
: '0'..'9'
;
/**
* Matches an identifier from the input. An identifier is a sequence of letters,
- * digits and "_", "'", "." symbols, starting with a letter.
+ * digits and "_", "'", "." symbols, starting with a letter.
*/
IDENTIFIER options { paraphrase = "an identifier"; testLiterals = true; }
: ALPHA (ALPHA | DIGIT | '_' | '\'' | '.')*
;
-
+
/**
* Matches an identifier starting with a colon. An identifier is a sequence of letters,
* digits and "_", "'", "." symbols, starting with a colon.
C_IDENTIFIER options { paraphrase = "an identifier starting with a colon"; testLiterals = true; }
: ':' ALPHA (ALPHA | DIGIT | '_' | '\'' | '.')*
;
-
+
/**
* Matches the value of user-defined annotations or attributes. The only constraint imposed on a user-defined value is that it start with
* an open brace and end with closed brace.
*/
USER_VALUE
- : '{'
+ : '{'
( '\n' { newline(); }
- | ~('{' | '}' | '\n')
- )*
+ | ~('{' | '}' | '\n')
+ )*
'}'
;
-
+
/**
- * Matches the question mark symbol ('?').
+ * Matches the question mark symbol ('?').
*/
-QUESTION_MARK options { paraphrase = "a question mark '?'"; }
+QUESTION_MARK options { paraphrase = "a question mark '?'"; }
: '?'
;
-
+
/**
* Matches the dollar sign ('$').
*/
-DOLLAR_SIGN options { paraphrase = "a dollar sign '$'"; }
+DOLLAR_SIGN options { paraphrase = "a dollar sign '$'"; }
: '$'
;
-
+
/**
* Matches the left bracket ('(').
*/
-LPAREN options { paraphrase = "a left parenthesis '('"; }
+LPAREN options { paraphrase = "a left parenthesis '('"; }
: '(';
-
+
/**
* Matches the right bracket ('(').
*/
-RPAREN options { paraphrase = "a right parenthesis ')'"; }
+RPAREN options { paraphrase = "a right parenthesis ')'"; }
: ')';
/**
- * Matches and skips whitespace in the input.
+ * Matches and skips whitespace in the input.
*/
WHITESPACE options { paraphrase = "whitespace"; }
: (' ' | '\t' | '\f') { $setType(antlr::Token::SKIP); }
/**
* Matches and skips the newline symbols in the input.
*/
-NEWLINE options { paraphrase = "a newline"; }
+NEWLINE options { paraphrase = "a newline"; }
: ('\r' '\n' | '\r' | '\n') { $setType(antlr::Token::SKIP); newline(); }
;
-
+
/**
* Matches a numeral from the input (non-empty sequence of digits).
*/
NUMERAL options { paraphrase = "a numeral"; }
: (DIGIT)+
;
-
+
/**
* Matches an allowed escaped character.
- */
+ */
protected ESCAPE
: '\\' ('"' | '\\' | 'n' | 't' | 'r')
- ;
-
+ ;
+
/**
* Matches a double quoted string literal. Escaping is supported, and escape
- * character '\' has to be escaped.
+ * character '\' has to be escaped.
*/
-STRING_LITERAL options { paraphrase = "a string literal"; }
+STRING_LITERAL options { paraphrase = "a string literal"; }
: '"' (ESCAPE | ~('"'|'\\'))* '"'
;
-
+
/**
* Matches the comments and ignores them
*/
+/* smt_parser.g
+ * Original author: dejan
+ * Major contributors:
+ * Minor contributors (to current version): none
+ * This file is part of the CVC4 prototype.
+ * Copyright (c) 2009 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.
+ *
+ * Parser for SMT-LIB input language.
+ */
+
header "post_include_hpp" {
#include "parser/antlr_parser.h"
+#include "util/command.h"
}
header "post_include_cpp" {
-#include <vector>
+#include <vector>
using namespace std;
using namespace CVC4;
using namespace CVC4::parser;
}
-
+
options {
language = "Cpp"; // C++ output for antlr
namespaceStd = "std"; // Cosmetic option to get rid of long defines in generated code
namespaceAntlr = "antlr"; // Cosmetic option to get rid of long defines in generated code
namespace = "CVC4::parser"; // Wrap everything in the smtparser namespace
}
-
+
/**
- * AntlrSmtParser class is the parser for the SMT-LIB files.
+ * AntlrSmtParser class is the parser for the SMT-LIB files.
*/
class AntlrSmtParser extends Parser("AntlrParser");
options {
*/
parseCommand returns [CVC4::Command* cmd]
: cmd = benchmark
- ;
-
+ ;
+
/**
* Matches the whole SMT-LIB benchmark.
* @return the sequence command containing the whole problem
- */
+ */
benchmark returns [Command* cmd]
: LPAREN BENCHMARK IDENTIFIER cmd = benchAttributes RPAREN
- | EOF { cmd = 0; }
+ | EOF { cmd = 0; }
;
/**
- * Matches a sequence of benchmark attributes and returns a pointer to a
+ * Matches a sequence of benchmark attributes and returns a pointer to a
* command sequence.
- * @return the command sequence
+ * @return the command sequence
*/
benchAttributes returns [CVC4::CommandSequence* cmd_seq = new CommandSequence()]
{
Command* cmd;
}
- : (cmd = benchAttribute { if (cmd) cmd_seq->addCommand(cmd); } )+
+ : (cmd = benchAttribute { if (cmd) cmd_seq->addCommand(cmd); } )+
;
-
+
/**
- * Matches a benchmark attribute, sucha as ':logic', ':formula', and returns
+ * Matches a benchmark attribute, sucha as ':logic', ':formula', and returns
* a corresponding command
* @retrurn a command corresponding to the attribute
*/
benchAttribute returns [Command* smt_command = 0]
{
- Expr formula;
- string logic;
+ Expr formula;
+ string logic;
SetBenchmarkStatusCommand::BenchmarkStatus b_status = SetBenchmarkStatusCommand::SMT_UNKNOWN;
}
- : LOGIC_ATTR logic = identifier
- { smt_command = new SetBenchmarkLogicCommand(logic); }
- | ASSUMPTION_ATTR formula = annotatedFormula
- { smt_command = new AssertCommand(formula); }
- | FORMULA_ATTR formula = annotatedFormula
+ : LOGIC_ATTR logic = identifier
+ { smt_command = new SetBenchmarkLogicCommand(logic); }
+ | ASSUMPTION_ATTR formula = annotatedFormula
+ { smt_command = new AssertCommand(formula); }
+ | FORMULA_ATTR formula = annotatedFormula
{ smt_command = new CheckSatCommand(formula); }
- | STATUS_ATTR b_status = status
- { smt_command = new SetBenchmarkStatusCommand(b_status); }
- | EXTRAPREDS_ATTR LPAREN (predicateDeclaration)+ RPAREN
- | NOTES_ATTR STRING_LITERAL
+ | STATUS_ATTR b_status = status
+ { smt_command = new SetBenchmarkStatusCommand(b_status); }
+ | EXTRAPREDS_ATTR LPAREN (predicateDeclaration)+ RPAREN
+ | NOTES_ATTR STRING_LITERAL
| annotation
;
* @return the id string
*/
identifier[DeclarationCheck check = CHECK_NONE] returns [std::string id]
- : x:IDENTIFIER
+ : x:IDENTIFIER
{ id = x->getText(); }
- { checkDeclaration(id, check) }?
+ { checkDeclaration(id, check) }?
exception catch [antlr::SemanticException& ex] {
switch (check) {
case CHECK_DECLARED: rethrow(ex, "Symbol " + id + " not declared");
case CHECK_UNDECLARED: rethrow(ex, "Symbol " + id + " already declared");
default: throw ex;
- }
- }
+ }
+ }
;
-/**
+/**
* Matches an annotated formula.
- * @return the expression representing the formula
+ * @return the expression representing the formula
*/
-annotatedFormula returns [CVC4::Expr formula]
-{
- Kind kind;
+annotatedFormula returns [CVC4::Expr formula]
+{
+ Kind kind;
vector<Expr> children;
}
- : formula = annotatedAtom
- | LPAREN kind = boolConnective annotatedFormulas[children] RPAREN { formula = mkExpr(kind, children); }
+ : formula = annotatedAtom
+ | LPAREN kind = boolConnective annotatedFormulas[children] RPAREN { formula = mkExpr(kind, children); }
;
/**
- * Matches an annotated proposition atom, which is either a propositional atom
- * or built of other atoms using a predicate symbol.
+ * Matches an annotated proposition atom, which is either a propositional atom
+ * or built of other atoms using a predicate symbol.
* @return expression representing the atom
*/
-annotatedAtom returns [CVC4::Expr atom]
- : atom = propositionalAtom
+annotatedAtom returns [CVC4::Expr atom]
+ : atom = propositionalAtom
;
/**
* @return the kind of the Bollean connective
*/
boolConnective returns [CVC4::Kind kind]
- : NOT { kind = CVC4::NOT; }
+ : NOT { kind = CVC4::NOT; }
| IMPLIES { kind = CVC4::IMPLIES; }
| AND { kind = CVC4::AND; }
| OR { kind = CVC4::OR; }
* Mathces a sequence of annotaed formulas and puts them into the formulas
* vector.
* @param formulas the vector to fill with formulas
- */
+ */
annotatedFormulas[std::vector<Expr>& formulas]
{
Expr f;
/**
* Matches a propositional atom and returns the expression of the atom.
- * @return atom the expression of the atom
+ * @return atom the expression of the atom
*/
propositionalAtom returns [CVC4::Expr atom]
{
std::string p;
-}
+}
: p = predicateName[CHECK_DECLARED] { atom = getVariable(p); }
| TRUE { atom = getTrueExpr(); }
| FALSE { atom = getFalseExpr(); }
;
/**
- * Matches a predicate symbol.
+ * Matches a predicate symbol.
* @param check what kind of check to do with the symbol
*/
predicateName[DeclarationCheck check = CHECK_NONE] returns [std::string p]
: p = identifier[check]
;
-
+
/**
* Matches an attribute name from the input (:attribute_name).
- */
-attribute
+ */
+attribute
: C_IDENTIFIER
;
-
+
/**
* Matches the sort symbol, which can be an arbitrary identifier.
* @param check the check to perform on the name
*/
-sortName[DeclarationCheck check = CHECK_NONE] returns [std::string s]
+sortName[DeclarationCheck check = CHECK_NONE] returns [std::string s]
: s = identifier[check]
;
-
+
/**
* Matches the declaration of a predicate and declares it
*/
string p_name;
vector<string> p_sorts;
}
- : LPAREN p_name = predicateName[CHECK_UNDECLARED] sortNames[p_sorts] RPAREN { newPredicate(p_name, p_sorts); }
+ : LPAREN p_name = predicateName[CHECK_UNDECLARED] sortNames[p_sorts] RPAREN { newPredicate(p_name, p_sorts); }
;
-
+
/**
* Matches a sequence of sort symbols and fills them into the given vector.
*/
{
std::string sort;
}
- : ( sort = sortName[CHECK_UNDECLARED] { sorts.push_back(sort); })*
+ : ( sort = sortName[CHECK_UNDECLARED] { sorts.push_back(sort); })*
;
/**
;
/**
- * Matches an annotation, which is an attribute name, with an optional user
+ * Matches an annotation, which is an attribute name, with an optional user
*/
-annotation
+annotation
: attribute (USER_VALUE)?
;
-
+
assert(!failed);
- reportf("Verified %d original clauses.\n", clauses.size());
+ if(verbosity >= 1)
+ reportf("Verified %d original clauses.\n", clauses.size());
}
#include "prop/minisat/core/SolverTypes.h"
#include "util/Assert.h"
#include "util/output.h"
+#include "util/options.h"
+#include "util/result.h"
#include <utility>
#include <map>
namespace CVC4 {
-PropEngine::PropEngine(DecisionEngine& de, TheoryEngine& te) :
+PropEngine::PropEngine(const Options* opts,
+ DecisionEngine& de,
+ TheoryEngine& te) :
+ d_opts(opts),
d_de(de),
d_te(te),
d_restartMayBeNeeded(false){
}
}
-void PropEngine::solve() {
+Result PropEngine::solve() {
if(d_restartMayBeNeeded)
restart();
- d_sat->verbosity = 1;
+ d_sat->verbosity = (d_opts->verbosity > 0) ? 1 : -1;
bool result = d_sat->solve();
if(!result){
}
Notice() << "result is " << (result ? "sat/invalid" : "unsat/valid") << endl;
+
+ return Result(result ? Result::SAT : Result::UNSAT);
}
}/* CVC4 namespace */
#include "theory/theory_engine.h"
#include "prop/minisat/simp/SimpSolver.h"
#include "prop/minisat/core/SolverTypes.h"
+#include "util/result.h"
#include <map>
#include "prop/cnf_stream.h"
namespace prop {
class CnfStream;
}
+
+ class Options;
}
namespace CVC4 {
// propositional solver, DPLL or otherwise.
class PropEngine {
+ const Options *d_opts;
DecisionEngine &d_de;
TheoryEngine &d_te;
friend class CVC4::prop::CnfStream;
- /* Morgan: I added these back.
- * Why did you push these into solve()?
- * I am guessing this is for either a technical reason I'm not seeing,
- * or that you wanted to have a clean restart everytime solve() was called
- * and to start from scratch everytime. (Avoid push/pop problems?)
- * Is this right?
+ /**
+ * The SAT solver.
*/
- CVC4::prop::minisat::Solver * d_sat;
-
+ CVC4::prop::minisat::Solver* d_sat;
std::map<Node, CVC4::prop::minisat::Lit> d_atom2lit;
std::map<CVC4::prop::minisat::Lit, Node> d_lit2atom;
/**
* Create a PropEngine with a particular decision and theory engine.
*/
- CVC4_PUBLIC PropEngine(CVC4::DecisionEngine&, CVC4::TheoryEngine&);
+ CVC4_PUBLIC PropEngine(const CVC4::Options* opts,
+ CVC4::DecisionEngine&,
+ CVC4::TheoryEngine&);
CVC4_PUBLIC ~PropEngine();
/**
* and invokes the sat solver for a satisfying assignment.
* TODO: what does well-formed mean here?
*/
- void solve();
+ Result solve();
};/* class PropEngine */
#include "util/command.h"
#include "util/output.h"
#include "expr/node_builder.h"
+#include "util/options.h"
namespace CVC4 {
-SmtEngine::SmtEngine(ExprManager* em, Options* opts) throw() :
+SmtEngine::SmtEngine(ExprManager* em, const Options* opts) throw() :
d_assertions(),
d_publicEm(em),
d_nm(em->getNodeManager()),
d_opts(opts),
d_de(),
d_te(),
- d_prop(d_de, d_te){
+ d_prop(opts, d_de, d_te) {
}
SmtEngine::~SmtEngine() {
Result SmtEngine::check() {
Debug("smt") << "SMT check()" << std::endl;
processAssertionList();
- d_prop.solve();
- return Result(Result::VALIDITY_UNKNOWN);
+ return d_prop.solve();
}
Result SmtEngine::quickCheck() {
NodeManagerScope nms(d_nm);
Node node_e = preprocess(e.getNode());
addFormula(node_e);
- return check();
+ Result r = check().asSatisfiabilityResult();
+ Debug("smt") << "SMT checkSat(" << e << ") ==> " << r << std::endl;
+ return r;
}
Result SmtEngine::query(const BoolExpr& e) {
NodeManagerScope nms(d_nm);
Node node_e = preprocess(d_nm->mkNode(NOT, e.getNode()));
addFormula(node_e);
- return check();
+ Result r = check().asValidityResult();
+ Debug("smt") << "SMT query(" << e << ") ==> " << r << std::endl;
+ return r;
}
Result SmtEngine::assertFormula(const BoolExpr& e) {
NodeManagerScope nms(d_nm);
Node node_e = preprocess(e.getNode());
addFormula(node_e);
- return quickCheck();
+ return quickCheck().asValidityResult();
}
Expr SmtEngine::simplify(const Expr& e) {
#include "expr/expr_manager.h"
#include "util/result.h"
#include "util/model.h"
-#include "util/options.h"
#include "prop/prop_engine.h"
#include "util/decision_engine.h"
namespace CVC4 {
class Command;
+class Options;
// TODO: SAT layer (esp. CNF- versus non-clausal solvers under the
// hood): use a type parameter and have check() delegate, or subclass
/**
* Construct an SmtEngine with the given expression manager and user options.
*/
- SmtEngine(ExprManager* em, Options* opts) throw();
+ SmtEngine(ExprManager* em, const Options* opts) throw();
/**
* Destruct the SMT engine.
std::vector<Node> d_assertions;
/** Our expression manager */
- ExprManager *d_publicEm;
+ ExprManager* d_publicEm;
/** Out internal expression/node manager */
- NodeManager *d_nm;
+ NodeManager* d_nm;
/** User-level options */
- Options *d_opts;
+ const Options* d_opts;
/** The decision engine */
DecisionEngine d_de;
#define __CVC4__ASSERT_H
#include <string>
+#include <sstream>
#include <cstdio>
#include <cstdarg>
#include "util/exception.h"
construct(header, extra, function, file, line, fmt, args);
va_end(args);
}
+
void construct(const char* header, const char* extra,
const char* function, const char* file,
unsigned line, const char* fmt, va_list args);
+
void construct(const char* header, const char* extra,
const char* function, const char* file,
unsigned line);
va_end(args);
}
+ template <class T>
UnhandledCaseException(const char* function, const char* file,
- unsigned line, int theCase) :
+ unsigned line, T theCase) :
UnreachableCodeException() {
+ std::stringstream sb;
+ sb << theCase;
construct("Unhandled case encountered",
- NULL, function, file, line, "The case was: %d", theCase);
+ NULL, function, file, line, "The case was: %s", sb.str().c_str());
}
UnhandledCaseException(const char* function, const char* file,
** See the file COPYING in the top-level source directory for licensing
** information.
**
- ** [[ Add file-specific comments here ]]
+ ** Implementation of command objects.
**/
-/*
- * command.cpp
- *
- * Created on: Nov 25, 2009
- * Author: dejan
- */
-
-#include <sstream>
#include "util/command.h"
-#include "util/Assert.h"
#include "smt/smt_engine.h"
using namespace std;
namespace CVC4 {
-ostream& operator<<(ostream& out, const Command& c) {
- c.toStream(out);
- return out;
-}
-
ostream& operator<<(ostream& out, const Command* c) {
if (c == NULL) {
out << "null";
return out;
}
-std::string Command::toString() const {
- stringstream ss;
- toStream(ss);
- return ss.str();
-}
-
-EmptyCommand::EmptyCommand(string name) :
- d_name(name) {
-}
-
-void EmptyCommand::invoke(SmtEngine* smt_engine) {
-}
-
-AssertCommand::AssertCommand(const BoolExpr& e) :
- d_expr(e) {
-}
-
-void AssertCommand::invoke(SmtEngine* smt_engine) {
- smt_engine->assertFormula(d_expr);
-}
-
-CheckSatCommand::CheckSatCommand() {
-}
-
-CheckSatCommand::CheckSatCommand(const BoolExpr& e) :
- d_expr(e) {
-}
-
-void CheckSatCommand::invoke(SmtEngine* smt_engine) {
- smt_engine->checkSat(d_expr);
-}
-
-QueryCommand::QueryCommand(const BoolExpr& e) :
- d_expr(e) {
-}
-
-void QueryCommand::invoke(CVC4::SmtEngine* smt_engine) {
- smt_engine->query(d_expr);
-}
-
-CommandSequence::CommandSequence() :
- d_last_index(0) {
-}
-
CommandSequence::~CommandSequence() {
- for(unsigned i = d_last_index; i < d_command_sequence.size(); ++i)
- delete d_command_sequence[i];
-}
-
-void CommandSequence::invoke(SmtEngine* smt_engine) {
- for(; d_last_index < d_command_sequence.size(); ++d_last_index) {
- d_command_sequence[d_last_index]->invoke(smt_engine);
- delete d_command_sequence[d_last_index];
+ for(unsigned i = d_index; i < d_commandSequence.size(); ++i) {
+ delete d_commandSequence[i];
}
}
-void CommandSequence::addCommand(Command* cmd) {
- d_command_sequence.push_back(cmd);
-}
-
-void EmptyCommand::toStream(ostream& out) const {
- out << "EmptyCommand(" << d_name << ")";
-}
-
-void AssertCommand::toStream(ostream& out) const {
- out << "Assert(" << d_expr << ")";
+void CommandSequence::invoke(SmtEngine* smtEngine) {
+ for(; d_index < d_commandSequence.size(); ++d_index) {
+ d_commandSequence[d_index]->invoke(smtEngine);
+ delete d_commandSequence[d_index];
+ }
}
void CheckSatCommand::toStream(ostream& out) const {
- if(d_expr.isNull())
+ if(d_expr.isNull()) {
out << "CheckSat()";
- else
+ } else {
out << "CheckSat(" << d_expr << ")";
-}
-
-void QueryCommand::toStream(ostream& out) const {
- out << "Query(";
- d_expr.printAst(out, 0);
- out << ")";
+ }
}
void CommandSequence::toStream(ostream& out) const {
out << "CommandSequence[" << endl;
- for(unsigned i = d_last_index; i < d_command_sequence.size(); ++i) {
- out << *d_command_sequence[i] << endl;
+ for(unsigned i = d_index; i < d_commandSequence.size(); ++i) {
+ out << *d_commandSequence[i] << endl;
}
out << "]";
}
-DeclarationCommand::DeclarationCommand(const std::vector<std::string>& ids) :
- d_declaredSymbols(ids) {
-}
-
void DeclarationCommand::toStream(std::ostream& out) const {
out << "Declare(";
bool first = true;
out << ")";
}
-SetBenchmarkStatusCommand::SetBenchmarkStatusCommand(BenchmarkStatus status) :
- d_status(status) {
-}
-
-void SetBenchmarkStatusCommand::invoke(SmtEngine* smt) {
- // TODO: something to be done with the status
-}
-
-void SetBenchmarkStatusCommand::toStream(std::ostream& out) const {
- out << "SetBenchmarkStatus(";
- switch(d_status) {
- case SMT_SATISFIABLE:
- out << "sat";
- break;
- case SMT_UNSATISFIABLE:
- out << "unsat";
- break;
- case SMT_UNKNOWN:
- out << "unknown";
- break;
- default:
- Unhandled("Unknown benchmark status");
- }
- out << ")";
-}
-
-SetBenchmarkLogicCommand::SetBenchmarkLogicCommand(string logic) : d_logic(logic)
- {}
-
-void SetBenchmarkLogicCommand::invoke(SmtEngine* smt) {
- // TODO: something to be done with the logic
-}
-
-void SetBenchmarkLogicCommand::toStream(std::ostream& out) const {
- out << "SetBenchmarkLogic(" << d_logic << ")";
-}
-
}/* CVC4 namespace */
** See the file COPYING in the top-level source directory for licensing
** information.
**
- ** Implementation of the command pattern on SmtEngines. Generated by
- ** the parser.
+ ** Implementation of the command pattern on SmtEngines. Command
+ ** objects are generated by the parser (typically) to implement the
+ ** commands in parsed input (see Parser::parseNextCommand()), or by
+ ** client code.
**/
#ifndef __CVC4__COMMAND_H
#define __CVC4__COMMAND_H
#include <iostream>
+#include <sstream>
+#include <string>
+#include <vector>
#include "cvc4_config.h"
#include "expr/expr.h"
+#include "util/result.h"
namespace CVC4 {
- class SmtEngine;
- class Command;
-}/* CVC4 namespace */
-namespace CVC4 {
+class SmtEngine;
+class Command;
-std::ostream& operator<<(std::ostream&, const Command&) CVC4_PUBLIC;
+inline std::ostream& operator<<(std::ostream&, const Command&) CVC4_PUBLIC;
std::ostream& operator<<(std::ostream&, const Command*) CVC4_PUBLIC;
class CVC4_PUBLIC Command {
std::string d_name;
};/* class EmptyCommand */
-
class CVC4_PUBLIC AssertCommand : public Command {
public:
AssertCommand(const BoolExpr& e);
BoolExpr d_expr;
};/* class AssertCommand */
-
class CVC4_PUBLIC DeclarationCommand : public EmptyCommand {
public:
DeclarationCommand(const std::vector<std::string>& ids);
CheckSatCommand();
CheckSatCommand(const BoolExpr& e);
void invoke(SmtEngine* smt);
+ Result getResult();
void toStream(std::ostream& out) const;
protected:
BoolExpr d_expr;
+ Result d_result;
};/* class CheckSatCommand */
-
class CVC4_PUBLIC QueryCommand : public Command {
public:
QueryCommand(const BoolExpr& e);
void invoke(SmtEngine* smt);
+ Result getResult();
void toStream(std::ostream& out) const;
protected:
BoolExpr d_expr;
+ Result d_result;
};/* class QueryCommand */
-
class CVC4_PUBLIC SetBenchmarkStatusCommand : public Command {
public:
/** The status an SMT benchmark can have */
void toStream(std::ostream& out) const;
protected:
BenchmarkStatus d_status;
-};/* class QueryCommand */
+};/* class SetBenchmarkStatusCommand */
+
+inline std::ostream& operator<<(std::ostream& out,
+ SetBenchmarkStatusCommand::BenchmarkStatus bs)
+ CVC4_PUBLIC;
class CVC4_PUBLIC SetBenchmarkLogicCommand : public Command {
public:
void toStream(std::ostream& out) const;
protected:
std::string d_logic;
-};/* class QueryCommand */
-
-
+};/* class SetBenchmarkLogicCommand */
class CVC4_PUBLIC CommandSequence : public Command {
public:
void invoke(SmtEngine* smt);
void addCommand(Command* cmd);
void toStream(std::ostream& out) const;
+
+ typedef std::vector<Command*>::iterator iterator;
+ typedef std::vector<Command*>::const_iterator const_iterator;
+
+ const_iterator begin() const { return d_commandSequence.begin(); }
+ const_iterator end() const { return d_commandSequence.end(); }
+
+ iterator begin() { return d_commandSequence.begin(); }
+ iterator end() { return d_commandSequence.end(); }
+
private:
/** All the commands to be executed (in sequence) */
- std::vector<Command*> d_command_sequence;
+ std::vector<Command*> d_commandSequence;
/** Next command to be executed */
- unsigned int d_last_index;
+ unsigned int d_index;
};/* class CommandSequence */
}/* CVC4 namespace */
+/* =========== inline function definitions =========== */
+
+#include "smt/smt_engine.h"
+
+namespace CVC4 {
+
+inline std::ostream& operator<<(std::ostream& out, const Command& c) {
+ c.toStream(out);
+ return out;
+}
+
+/* class Command */
+
+inline std::string Command::toString() const {
+ std::stringstream ss;
+ toStream(ss);
+ return ss.str();
+}
+
+/* class EmptyCommand */
+
+inline EmptyCommand::EmptyCommand(std::string name) :
+ d_name(name) {
+}
+
+inline void EmptyCommand::invoke(SmtEngine* smt_engine) {
+}
+
+inline void EmptyCommand::toStream(std::ostream& out) const {
+ out << "EmptyCommand(" << d_name << ")";
+}
+
+/* class AssertCommand */
+
+inline AssertCommand::AssertCommand(const BoolExpr& e) :
+ d_expr(e) {
+}
+
+inline void AssertCommand::invoke(SmtEngine* smt_engine) {
+ smt_engine->assertFormula(d_expr);
+}
+
+inline void AssertCommand::toStream(std::ostream& out) const {
+ out << "Assert(" << d_expr << ")";
+}
+
+/* class CheckSatCommand */
+
+inline CheckSatCommand::CheckSatCommand() {
+}
+
+inline CheckSatCommand::CheckSatCommand(const BoolExpr& e) :
+ d_expr(e) {
+}
+
+inline void CheckSatCommand::invoke(SmtEngine* smt_engine) {
+ d_result = smt_engine->checkSat(d_expr);
+}
+
+inline Result CheckSatCommand::getResult() {
+ return d_result;
+}
+
+/* class QueryCommand */
+
+inline QueryCommand::QueryCommand(const BoolExpr& e) :
+ d_expr(e) {
+}
+
+inline void QueryCommand::invoke(CVC4::SmtEngine* smt_engine) {
+ d_result = smt_engine->query(d_expr);
+}
+
+inline Result QueryCommand::getResult() {
+ return d_result;
+}
+
+inline void QueryCommand::toStream(std::ostream& out) const {
+ out << "Query(";
+ d_expr.printAst(out, 0);
+ out << ")";
+}
+
+/* class CommandSequence */
+
+inline CommandSequence::CommandSequence() :
+ d_index(0) {
+}
+
+inline void CommandSequence::addCommand(Command* cmd) {
+ d_commandSequence.push_back(cmd);
+}
+
+/* class DeclarationCommand */
+
+inline DeclarationCommand::DeclarationCommand(const std::vector<std::string>& ids) :
+ d_declaredSymbols(ids) {
+}
+
+/* class SetBenchmarkStatusCommand */
+
+inline SetBenchmarkStatusCommand::SetBenchmarkStatusCommand(BenchmarkStatus s) :
+ d_status(s) {
+}
+
+inline void SetBenchmarkStatusCommand::invoke(SmtEngine* smt) {
+ // FIXME: TODO: something to be done with the status
+}
+
+inline void SetBenchmarkStatusCommand::toStream(std::ostream& out) const {
+ out << "SetBenchmarkStatus(" << d_status << ")";
+}
+
+/* class SetBenchmarkLogicCommand */
+
+inline SetBenchmarkLogicCommand::SetBenchmarkLogicCommand(std::string l) :
+ d_logic(l) {
+}
+
+inline void SetBenchmarkLogicCommand::invoke(SmtEngine* smt) {
+ // FIXME: TODO: something to be done with the logic
+}
+
+inline void SetBenchmarkLogicCommand::toStream(std::ostream& out) const {
+ out << "SetBenchmarkLogic(" << d_logic << ")";
+}
+
+/* output stream insertion operator for benchmark statuses */
+inline std::ostream& operator<<(std::ostream& out,
+ SetBenchmarkStatusCommand::BenchmarkStatus bs) {
+ switch(bs) {
+
+ case SetBenchmarkStatusCommand::SMT_SATISFIABLE:
+ return out << "sat";
+
+ case SetBenchmarkStatusCommand::SMT_UNSATISFIABLE:
+ return out << "unsat";
+
+ case SetBenchmarkStatusCommand::SMT_UNKNOWN:
+ return out << "unknown";
+
+ default:
+ return out << "SetBenchmarkStatusCommand::[UNKNOWNSTATUS!]";
+ }
+}
+
+}/* CVC4 namespace */
+
#endif /* __CVC4__COMMAND_H */
namespace CVC4 {
+/* Definitions of the declared globals from output.h... */
+
null_streambuf null_sb;
std::ostream null_os(&null_sb);
namespace CVC4 {
+/**
+ * A utility class to provide (essentially) a "/dev/null" streambuf.
+ * If debugging support is compiled in, but debugging for
+ * e.g. "parser" is off, then Debug("parser") returns a stream
+ * attached to a null_streambuf instance so that output is directed to
+ * the bit bucket.
+ */
class null_streambuf : public std::streambuf {
public:
+ /* Overriding overflow() just ensures that EOF isn't returned on the
+ * stream. Perhaps this is not so critical, but recommended; this
+ * way the output stream looks like it's functioning, in a non-error
+ * state. */
int overflow(int c) { return c; }
};/* class null_streambuf */
+/** A null stream-buffer singleton */
extern null_streambuf null_sb;
+/** A null output stream singleton */
extern std::ostream null_os CVC4_PUBLIC;
+/** The debug output class */
class CVC4_PUBLIC DebugC {
std::set<std::string> d_tags;
std::ostream *d_os;
void operator()(const char* tag, std::string);
void operator()(std::string tag, const char*);
void operator()(std::string tag, std::string);
- //void operator()(const char*);// Yeting option
- //void operator()(std::string);// Yeting option
static void printf(const char* tag, const char* fmt, ...) __attribute__ ((format(printf, 2, 3)));
static void printf(std::string tag, const char* fmt, ...) __attribute__ ((format(printf, 2, 3)));
- // Yeting option not possible here
std::ostream& operator()(const char* tag) {
if(d_tags.find(std::string(tag)) != d_tags.end())
return *d_os;
else return null_os;
}
- std::ostream& operator()();// Yeting option
+ /**
+ * The "Yeting option" - this allows use of Debug() without a tag
+ * for temporary (file-only) debugging.
+ */
+ std::ostream& operator()();
void on (const char* tag) { d_tags.insert(std::string(tag)); }
void on (std::string tag) { d_tags.insert(tag); }
void setStream(std::ostream& os) { d_os = &os; }
};/* class Debug */
+/** The debug output singleton */
extern DebugC Debug CVC4_PUBLIC;
+/** The warning output class */
class CVC4_PUBLIC WarningC {
std::ostream *d_os;
void setStream(std::ostream& os) { d_os = &os; }
};/* class Warning */
+/** The warning output singleton */
extern WarningC Warning CVC4_PUBLIC;
+/** The message output class */
class CVC4_PUBLIC MessageC {
std::ostream *d_os;
void setStream(std::ostream& os) { d_os = &os; }
};/* class Message */
+/** The message output singleton */
extern MessageC Message CVC4_PUBLIC;
+/** The notice output class */
class CVC4_PUBLIC NoticeC {
std::ostream *d_os;
void setStream(std::ostream& os) { d_os = &os; }
};/* class Notice */
+/** The notice output singleton */
extern NoticeC Notice CVC4_PUBLIC;
+/** The chat output class */
class CVC4_PUBLIC ChatC {
std::ostream *d_os;
void setStream(std::ostream& os) { d_os = &os; }
};/* class Chat */
+/** The chat output singleton */
extern ChatC Chat CVC4_PUBLIC;
+/** The trace output class */
class CVC4_PUBLIC TraceC {
std::ostream *d_os;
std::set<std::string> d_tags;
void operator()(std::string tag, std::string);
void printf(const char* tag, const char* fmt, ...) __attribute__ ((format(printf, 3, 4))) {
+ // chop off output after 1024 bytes
char buf[1024];
va_list vl;
va_start(vl, fmt);
void setStream(std::ostream& os) { d_os = &os; }
};/* class Trace */
+/** The trace output singleton */
extern TraceC Trace CVC4_PUBLIC;
}/* CVC4 namespace */
#ifndef __CVC4__RESULT_H
#define __CVC4__RESULT_H
+#include "util/Assert.h"
+
namespace CVC4 {
// TODO: perhaps best to templatize Result on its Kind (SAT/Validity),
private:
enum SAT d_sat;
enum Validity d_validity;
- enum { TYPE_SAT, TYPE_VALIDITY } d_which;
+ enum { TYPE_SAT, TYPE_VALIDITY, TYPE_NONE } d_which;
friend std::ostream& CVC4::operator<<(std::ostream& out, Result r);
public:
- Result(enum SAT s) : d_sat(s), d_validity(VALIDITY_UNKNOWN), d_which(TYPE_SAT) {}
- Result(enum Validity v) : d_sat(SAT_UNKNOWN), d_validity(v), d_which(TYPE_VALIDITY) {}
+ Result() :
+ d_sat(SAT_UNKNOWN),
+ d_validity(VALIDITY_UNKNOWN),
+ d_which(TYPE_NONE) {
+ }
+ Result(enum SAT s) :
+ d_sat(s),
+ d_validity(VALIDITY_UNKNOWN),
+ d_which(TYPE_SAT) {
+ }
+ Result(enum Validity v) :
+ d_sat(SAT_UNKNOWN),
+ d_validity(v),
+ d_which(TYPE_VALIDITY) {
+ }
enum SAT isSAT();
enum Validity isValid();
enum UnknownExplanation whyUnknown();
+ inline Result asSatisfiabilityResult() const;
+ inline Result asValidityResult() const;
+
};/* class Result */
+inline Result Result::asSatisfiabilityResult() const {
+ if(d_which == TYPE_SAT) {
+ return *this;
+ }
+
+ switch(d_validity) {
+
+ case INVALID:
+ return Result(SAT);
+
+ case VALID:
+ return Result(UNSAT);
+
+ case VALIDITY_UNKNOWN:
+ return Result(SAT_UNKNOWN);
+
+ default:
+ Unhandled(d_validity);
+ }
+}
+
+inline Result Result::asValidityResult() const {
+ if(d_which == TYPE_VALIDITY) {
+ return *this;
+ }
+
+ switch(d_sat) {
+
+ case SAT:
+ return Result(INVALID);
+
+ case UNSAT:
+ return Result(VALID);
+
+ case SAT_UNKNOWN:
+ return Result(VALIDITY_UNKNOWN);
+
+ default:
+ Unhandled(d_sat);
+ }
+}
+
inline std::ostream& operator<<(std::ostream& out, Result r) {
if(r.d_which == Result::TYPE_SAT) {
switch(r.d_sat) {
projects / cvc5.git / commitdiff