From 64d530e5b9096e66398f92d93cf7bc4268df0e70 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Wed, 3 Feb 2010 22:20:25 +0000 Subject: [PATCH] Addressed many of the concerns of bug 10 (build system code review). 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.builds.in | 55 ++++++++- config/build-type | 22 ++-- configure | 175 +++++++++++------------------ configure.ac | 114 ++++++++----------- src/Makefile.am | 5 +- src/main/main.cpp | 47 +++++++- src/parser/Makefile.am | 6 +- src/parser/antlr_parser.cpp | 1 + src/parser/antlr_parser.h | 4 +- src/parser/cvc/cvc_lexer.g | 59 ++++++---- src/parser/cvc/cvc_parser.g | 122 +++++++++++--------- src/parser/parser.h | 4 +- src/parser/smt/smt_lexer.g | 86 ++++++++------ src/parser/smt/smt_parser.g | 127 +++++++++++---------- src/prop/minisat/core/Solver.C | 3 +- src/prop/prop_engine.cpp | 13 ++- src/prop/prop_engine.h | 21 ++-- src/smt/smt_engine.cpp | 18 +-- src/smt/smt_engine.h | 10 +- src/util/Assert.h | 10 +- src/util/command.cpp | 141 +++-------------------- src/util/command.h | 198 ++++++++++++++++++++++++++++++--- src/util/output.cpp | 2 + src/util/output.h | 35 +++++- src/util/result.h | 66 ++++++++++- 25 files changed, 783 insertions(+), 561 deletions(-) diff --git a/Makefile.builds.in b/Makefile.builds.in index 789fb0bae..650d7be6d 100644 --- a/Makefile.builds.in +++ b/Makefile.builds.in @@ -1,9 +1,27 @@ # -*- 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@ @@ -11,39 +29,64 @@ prefix = @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) $@) diff --git a/config/build-type b/config/build-type index 997e0f8e3..5c48f8fef 100755 --- a/config/build-type +++ b/config/build-type @@ -6,8 +6,8 @@ # 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): @@ -18,15 +18,15 @@ # 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 @@ -46,7 +46,7 @@ while [ $# -gt 0 ]; do 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 diff --git a/configure b/configure index 8e60591d9..bcad3dc5b 100755 --- a/configure +++ b/configure @@ -712,7 +712,6 @@ LIBOBJS mk_include CVC4_PARSER_LIBRARY_VERSION CVC4_LIBRARY_VERSION -CVC4_LIBRARY_RELEASE_CODE BUILDING_STATIC BUILDING_SHARED ANTLR_LDFLAGS @@ -2617,11 +2616,14 @@ CVC4_RELEASE=prerelease # 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 @@ -2820,51 +2822,51 @@ fi 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 @@ -2881,7 +2883,13 @@ fi { $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 @@ -3571,26 +3579,7 @@ am__tar='${AMTAR} chof - "$$tardir"'; am__untar='${AMTAR} xf -' 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 @@ -3892,7 +3881,6 @@ test -z "$OBJDUMP" && OBJDUMP=objdump - case `pwd` in *\ * | *\ *) { $as_echo "$as_me:${as_lineno-$LINENO}: WARNING: Libtool does not cope well with whitespace in \`pwd\`" >&5 @@ -5458,13 +5446,13 @@ if test "${lt_cv_nm_interface+set}" = set; then : 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" @@ -6667,7 +6655,7 @@ ia64-*-hpux*) ;; *-*-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=$? @@ -8135,11 +8123,11 @@ else -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. @@ -8474,11 +8462,11 @@ else -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. @@ -8579,11 +8567,11 @@ else -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 @@ -8634,11 +8622,11 @@ else -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 @@ -11017,7 +11005,7 @@ else 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 @@ -11113,7 +11101,7 @@ else 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 @@ -14668,11 +14656,11 @@ else -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. @@ -14767,11 +14755,11 @@ else -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 @@ -14819,11 +14807,11 @@ else -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 @@ -16454,20 +16442,28 @@ if test "$enable_static" = yes; then BUILDING_STATIC=1; fi +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" @@ -19135,50 +19131,9 @@ CPPFLAGS : $CPPFLAGS 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 ' 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 diff --git a/configure.ac b/configure.ac index 2937f62d7..45ace0842 100644 --- a/configure.ac +++ b/configure.ac @@ -30,11 +30,14 @@ CVC4_RELEASE=prerelease # 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 @@ -62,51 +65,51 @@ fi 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]) @@ -120,7 +123,13 @@ if test "$custom_build_profile" = yes; then 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/)]) @@ -297,23 +306,8 @@ fi 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. @@ -404,23 +398,31 @@ if test "$enable_static" = yes; then BUILDING_STATIC=1; fi 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 @@ -484,35 +486,9 @@ CPPFLAGS : $CPPFLAGS 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 ' 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 diff --git a/src/Makefile.am b/src/Makefile.am index 97a2ecead..fac263152 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -10,9 +10,6 @@ # 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 = @@ -26,7 +23,7 @@ lib_LTLIBRARIES = libcvc4.la 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 = diff --git a/src/main/main.cpp b/src/main/main.cpp index 4731c536e..387d5ca97 100644 --- a/src/main/main.cpp +++ b/src/main/main.cpp @@ -26,6 +26,7 @@ #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" @@ -35,9 +36,12 @@ using namespace CVC4; 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 { @@ -110,10 +114,7 @@ int main(int argc, char *argv[]) { // 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; } @@ -147,5 +148,39 @@ int main(int argc, char *argv[]) { abort(); } + // TODO: adjust return value based on lastResult return 0; } + +void doCommand(SmtEngine& smt, Command* cmd) { + CommandSequence *seq = dynamic_cast(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(cmd); + if(qc != NULL) { + lastResult = qc->getResult(); + if(options.verbosity >= 0) { + cout << lastResult << endl; + } + } else { + CheckSatCommand *csc = dynamic_cast(cmd); + if(csc != NULL) { + lastResult = csc->getResult(); + if(options.verbosity >= 0) { + cout << lastResult << endl; + } + } + } + } +} diff --git a/src/parser/Makefile.am b/src/parser/Makefile.am index 4fcaed14d..fe906cbe0 100644 --- a/src/parser/Makefile.am +++ b/src/parser/Makefile.am @@ -10,9 +10,6 @@ # 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 = \ @@ -25,7 +22,8 @@ SUBDIRS = smt cvc 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) diff --git a/src/parser/antlr_parser.cpp b/src/parser/antlr_parser.cpp index 3522bfd75..34bf4bc82 100644 --- a/src/parser/antlr_parser.cpp +++ b/src/parser/antlr_parser.cpp @@ -25,6 +25,7 @@ #include "antlr_parser.h" #include "util/output.h" #include "util/Assert.h" +#include "util/command.h" using namespace std; using namespace CVC4; diff --git a/src/parser/antlr_parser.h b/src/parser/antlr_parser.h index ae84318c8..a3015eb22 100644 --- a/src/parser/antlr_parser.h +++ b/src/parser/antlr_parser.h @@ -25,11 +25,13 @@ #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 { /** diff --git a/src/parser/cvc/cvc_lexer.g b/src/parser/cvc/cvc_lexer.g index 52c58a38f..db40be3a8 100644 --- a/src/parser/cvc/cvc_lexer.g +++ b/src/parser/cvc/cvc_lexer.g @@ -1,12 +1,26 @@ +/* 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; @@ -14,15 +28,15 @@ options { 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"; @@ -42,7 +56,7 @@ tokens { CHECKSAT = "CHECKSAT"; PRINT = "PRINT"; ECHO = "ECHO"; - + PUSH = "PUSH"; POP = "POP"; POPTO = "POPTO"; @@ -56,56 +70,56 @@ IFF : "<=>"; /** * 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); } @@ -114,7 +128,7 @@ WHITESPACE options { paraphrase = "whitespace"; } /** * 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(); } ; @@ -124,11 +138,10 @@ NEWLINE options { paraphrase = "a 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 diff --git a/src/parser/cvc/cvc_parser.g b/src/parser/cvc/cvc_parser.g index eb21283a3..ce61deae2 100644 --- a/src/parser/cvc/cvc_parser.g +++ b/src/parser/cvc/cvc_parser.g @@ -1,24 +1,39 @@ +/* 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 +#include 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 { @@ -27,7 +42,7 @@ options { defaultErrorHandler = false; // Skip the defaul error handling, just break with exceptions k = 2; } - + /** * Parses the next command. * @return command or 0 if EOF @@ -44,9 +59,9 @@ parseExpr returns [CVC4::Expr expr] : 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] @@ -58,36 +73,36 @@ 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 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& 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] { @@ -95,11 +110,11 @@ identifier[DeclarationCheck check = CHECK_NONE] returns [std::string id] 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 */ @@ -107,10 +122,10 @@ type : BOOLEAN ; -/** +/** * Matches a CVC4 formula. * @return the expression representing the formula - */ + */ formula returns [CVC4::Expr formula] : formula = boolFormula ; @@ -121,69 +136,69 @@ formula returns [CVC4::Expr formula] * 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 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 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 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 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); } @@ -191,21 +206,21 @@ boolImpliesFormula returns [CVC4::Expr 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 */ @@ -247,7 +262,7 @@ iteElseFormula returns [CVC4::Expr formula] /** * Parses the Boolean atoms (variables and predicates). * @return the expression representing the atom. - */ + */ boolAtom returns [CVC4::Expr atom] { string p; @@ -259,13 +274,12 @@ boolAtom returns [CVC4::Expr atom] | 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] ; - diff --git a/src/parser/parser.h b/src/parser/parser.h index 618b1c8ab..4f0502f24 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -18,10 +18,10 @@ #include #include + #include "cvc4_config.h" #include "parser/parser_exception.h" #include "util/Assert.h" -#include "antlr_parser.h" namespace antlr { class CharScanner; @@ -36,6 +36,8 @@ class ExprManager; namespace parser { +class AntlrParser; + /** * The parser. The parser should be obtained by calling the static methods * getNewParser, and should be deleted when done. diff --git a/src/parser/smt/smt_lexer.g b/src/parser/smt/smt_lexer.g index a82e54e30..e9abab61a 100644 --- a/src/parser/smt/smt_lexer.g +++ b/src/parser/smt/smt_lexer.g @@ -1,13 +1,27 @@ +/* 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; @@ -15,9 +29,9 @@ options { 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"; @@ -55,28 +69,28 @@ tokens { /** * 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. @@ -84,47 +98,47 @@ IDENTIFIER options { paraphrase = "an identifier"; testLiterals = true; } 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); } @@ -133,32 +147,32 @@ WHITESPACE options { paraphrase = "whitespace"; } /** * 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 */ diff --git a/src/parser/smt/smt_parser.g b/src/parser/smt/smt_parser.g index 0db89d4f1..3933a04f0 100644 --- a/src/parser/smt/smt_parser.g +++ b/src/parser/smt/smt_parser.g @@ -1,24 +1,39 @@ +/* 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 +#include 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 { @@ -43,50 +58,50 @@ parseExpr returns [CVC4::Expr expr] */ 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 ; @@ -96,38 +111,38 @@ benchAttribute returns [Command* smt_command = 0] * @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 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 ; /** @@ -135,7 +150,7 @@ annotatedAtom returns [CVC4::Expr atom] * @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; } @@ -147,7 +162,7 @@ boolConnective returns [CVC4::Kind kind] * Mathces a sequence of annotaed formulas and puts them into the formulas * vector. * @param formulas the vector to fill with formulas - */ + */ annotatedFormulas[std::vector& formulas] { Expr f; @@ -157,40 +172,40 @@ annotatedFormulas[std::vector& formulas] /** * 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 */ @@ -199,9 +214,9 @@ predicateDeclaration string p_name; vector 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. */ @@ -209,7 +224,7 @@ sortNames[std::vector& sorts] { std::string sort; } - : ( sort = sortName[CHECK_UNDECLARED] { sorts.push_back(sort); })* + : ( sort = sortName[CHECK_UNDECLARED] { sorts.push_back(sort); })* ; /** @@ -222,9 +237,9 @@ status returns [ SetBenchmarkStatusCommand::BenchmarkStatus status ] ; /** - * 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)? ; - + diff --git a/src/prop/minisat/core/Solver.C b/src/prop/minisat/core/Solver.C index 4ea33e101..e99870654 100644 --- a/src/prop/minisat/core/Solver.C +++ b/src/prop/minisat/core/Solver.C @@ -724,7 +724,8 @@ void Solver::verifyModel() assert(!failed); - reportf("Verified %d original clauses.\n", clauses.size()); + if(verbosity >= 1) + reportf("Verified %d original clauses.\n", clauses.size()); } diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index b4df32f0f..3455b845e 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -22,6 +22,8 @@ #include "prop/minisat/core/SolverTypes.h" #include "util/Assert.h" #include "util/output.h" +#include "util/options.h" +#include "util/result.h" #include #include @@ -31,7 +33,10 @@ using namespace std; 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){ @@ -82,11 +87,11 @@ void PropEngine::restart(){ } } -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){ @@ -94,6 +99,8 @@ void PropEngine::solve() { } Notice() << "result is " << (result ? "sat/invalid" : "unsat/valid") << endl; + + return Result(result ? Result::SAT : Result::UNSAT); } }/* CVC4 namespace */ diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h index 9f5f9dac1..181c0288e 100644 --- a/src/prop/prop_engine.h +++ b/src/prop/prop_engine.h @@ -23,6 +23,7 @@ #include "theory/theory_engine.h" #include "prop/minisat/simp/SimpSolver.h" #include "prop/minisat/core/SolverTypes.h" +#include "util/result.h" #include #include "prop/cnf_stream.h" @@ -31,6 +32,8 @@ namespace CVC4 { namespace prop { class CnfStream; } + + class Options; } namespace CVC4 { @@ -40,20 +43,16 @@ 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 d_atom2lit; std::map d_lit2atom; @@ -101,7 +100,9 @@ public: /** * 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(); /** @@ -115,7 +116,7 @@ public: * and invokes the sat solver for a satisfying assignment. * TODO: what does well-formed mean here? */ - void solve(); + Result solve(); };/* class PropEngine */ diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 7e2b6e24c..e4a54b694 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -17,17 +17,18 @@ #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() { @@ -53,8 +54,7 @@ void SmtEngine::processAssertionList() { 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() { @@ -73,7 +73,9 @@ Result SmtEngine::checkSat(const BoolExpr& e) { 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) { @@ -81,7 +83,9 @@ 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) { @@ -89,7 +93,7 @@ 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) { diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 59eddccf0..48365e129 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -26,7 +26,6 @@ #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" @@ -37,6 +36,7 @@ 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 @@ -56,7 +56,7 @@ public: /** * 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. @@ -116,13 +116,13 @@ private: std::vector 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; diff --git a/src/util/Assert.h b/src/util/Assert.h index d8e881613..fa05ecaa5 100644 --- a/src/util/Assert.h +++ b/src/util/Assert.h @@ -17,6 +17,7 @@ #define __CVC4__ASSERT_H #include +#include #include #include #include "util/exception.h" @@ -35,9 +36,11 @@ protected: 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); @@ -99,11 +102,14 @@ public: va_end(args); } + template 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, diff --git a/src/util/command.cpp b/src/util/command.cpp index 90204a63f..f5a694a73 100644 --- a/src/util/command.cpp +++ b/src/util/command.cpp @@ -10,30 +10,16 @@ ** 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 #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"; @@ -43,99 +29,35 @@ ostream& operator<<(ostream& out, const Command* c) { 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& ids) : - d_declaredSymbols(ids) { -} - void DeclarationCommand::toStream(std::ostream& out) const { out << "Declare("; bool first = true; @@ -149,41 +71,4 @@ void DeclarationCommand::toStream(std::ostream& out) const { 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 */ diff --git a/src/util/command.h b/src/util/command.h index 57edfea01..15104a5ea 100644 --- a/src/util/command.h +++ b/src/util/command.h @@ -10,26 +10,30 @@ ** 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 +#include +#include +#include #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 { @@ -49,7 +53,6 @@ private: std::string d_name; };/* class EmptyCommand */ - class CVC4_PUBLIC AssertCommand : public Command { public: AssertCommand(const BoolExpr& e); @@ -59,7 +62,6 @@ protected: BoolExpr d_expr; };/* class AssertCommand */ - class CVC4_PUBLIC DeclarationCommand : public EmptyCommand { public: DeclarationCommand(const std::vector& ids); @@ -73,22 +75,24 @@ public: 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 */ @@ -105,7 +109,11 @@ public: 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: @@ -114,9 +122,7 @@ public: void toStream(std::ostream& out) const; protected: std::string d_logic; -};/* class QueryCommand */ - - +};/* class SetBenchmarkLogicCommand */ class CVC4_PUBLIC CommandSequence : public Command { public: @@ -125,13 +131,171 @@ public: void invoke(SmtEngine* smt); void addCommand(Command* cmd); void toStream(std::ostream& out) const; + + typedef std::vector::iterator iterator; + typedef std::vector::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 d_command_sequence; + std::vector 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& 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 */ diff --git a/src/util/output.cpp b/src/util/output.cpp index 05c74918c..b42fc77be 100644 --- a/src/util/output.cpp +++ b/src/util/output.cpp @@ -20,6 +20,8 @@ namespace CVC4 { +/* Definitions of the declared globals from output.h... */ + null_streambuf null_sb; std::ostream null_os(&null_sb); diff --git a/src/util/output.h b/src/util/output.h index c1e513703..6a6c76d83 100644 --- a/src/util/output.h +++ b/src/util/output.h @@ -28,14 +28,28 @@ 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 d_tags; std::ostream *d_os; @@ -47,12 +61,9 @@ public: 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()) @@ -64,7 +75,11 @@ public: 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); } @@ -74,8 +89,10 @@ public: 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; @@ -92,8 +109,10 @@ public: 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; @@ -110,8 +129,10 @@ public: 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; @@ -128,8 +149,10 @@ public: 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; @@ -146,8 +169,10 @@ public: 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 d_tags; @@ -161,6 +186,7 @@ public: 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); @@ -191,6 +217,7 @@ public: void setStream(std::ostream& os) { d_os = &os; } };/* class Trace */ +/** The trace output singleton */ extern TraceC Trace CVC4_PUBLIC; }/* CVC4 namespace */ diff --git a/src/util/result.h b/src/util/result.h index 87686d59c..d4980c776 100644 --- a/src/util/result.h +++ b/src/util/result.h @@ -16,6 +16,8 @@ #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), @@ -52,20 +54,78 @@ public: 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) { -- 2.30.2