diff options
31 files changed, 845 insertions, 367 deletions
diff --git a/autogen.sh b/autogen.sh index 5f2611c91..5f0dc09e0 100755 --- a/autogen.sh +++ b/autogen.sh @@ -1,4 +1,36 @@ -#!/bin/sh -ex +#!/bin/sh + +# Expected versions of tools. +# +# If the installed autotools aren't these versions, issue a warning +# about checking results into subversion. +libtoolize_version='libtoolize (GNU libtool) 2.2.6' +autoheader_version='autoheader (GNU Autoconf) 2.64' +aclocal_version='aclocal (GNU automake) 1.11' +autoconf_version='autoconf (GNU Autoconf) 2.64' +automake_version='automake (GNU automake) 1.11' + +# first, check versions of tools + +warning= +for tool in libtoolize autoheader aclocal autoconf automake; do + version=`eval echo '${'$tool'_version}'` + if $tool --version | grep -Fq "$version"; then :; else + echo "WARNING: [$tool] Expected $version." + warning=yes + fi +done + +if test -n "$warning"; then + echo "WARNING:" + echo "WARNING: Due to the above unexpected versions of autotools, please do not commit" + echo "WARNING: the files these tools generate to CVC4 svn." + echo +fi + +# now do a standard autogen + +set -ex cd "$(dirname "$0")" libtoolize --copy diff --git a/config/antlr.m4 b/config/antlr.m4 index fbc4dbe56..ad0ddcd91 100644 --- a/config/antlr.m4 +++ b/config/antlr.m4 @@ -1,33 +1,36 @@ ## # Check for ANTLR's runantlr script. Will set ANTLR to the location of the -# runantlr script +# runantlr script ## AC_DEFUN([AC_PROG_ANTLR], [ - + # Get the location of the runantlr script AC_ARG_WITH( [antlr], AC_HELP_STRING( [--with-antlr=RUNANTLR], - [location of the ANTLR's `runantlr` script] + [location of the ANTLR's `runantlr` script] ), ANTLR="$withval", - ANTLR="runantlr" - ) + ) # Check the existance of the runantlr script - AC_CHECK_PROG(ANTLR, "$ANTLR", "$ANTLR", []) - if test no$ANTLR = "no"; + if test -z "$ANTLR"; then + AC_CHECK_PROGS(ANTLR, [runantlr antlr]) + else + AC_CHECK_PROG(ANTLR, "$ANTLR", "$ANTLR", []) + fi + if test no$ANTLR = "no"; then AC_MSG_WARN( - [Couldn't find the runantlr script, make sure that the parser code has + [Couldn't find the runantlr script, make sure that the parser code has been generated already. To obtain ANTLR see <http://www.antlr.org/>.] ) AC_MSG_RESULT(no) - fi + fi - # Define the ANTL related variables - AC_SUBST(ANTLR) + # Define the ANTL related variables + AC_SUBST(ANTLR) ]) ## @@ -43,7 +46,7 @@ AC_DEFUN([AC_LIB_ANTLR],[ AC_HELP_STRING( [--with-antlr-prefix=PATH], [set the search path for ANTLR headers and libraries to `PATH/include` - and `PATH/lib`. By default we look in /usr, /usr/local, /opt and + and `PATH/lib`. By default we look in /usr, /usr/local, /opt and /opt/local. ] ), @@ -53,16 +56,16 @@ AC_DEFUN([AC_LIB_ANTLR],[ AC_MSG_CHECKING(for antlr C++ runtime library) - # Use C++ and remember the variables we are changing + # Use C++ and remember the variables we are changing AC_LANG_PUSH(C++) OLD_CPPFLAGS="$CPPFLAGS" OLD_LIBS="$LIBS" - + # Try all the includes/libs set in ANTLR_PREFIXES for antlr_prefix in $ANTLR_PREFIXES - do + do CPPFLAGS="$OLD_CPPFLAGS -I$antlr_prefix/include" - LIBS="$OLD_LIBS -L$antlr_prefix/lib -lantlr" + LIBS="$OLD_LIBS -L$antlr_prefix/lib -lantlr-pic" AC_LINK_IFELSE( [ #include <antlr/CommonAST.hpp> @@ -71,20 +74,40 @@ AC_DEFUN([AC_LIB_ANTLR],[ int main() { MyAST ast; } - ], + ], [ AC_MSG_RESULT(found in $antlr_prefix) ANTLR_INCLUDES="-I$antlr_prefix/include" ANTLR_LDFLAGS="-L$antlr_prefix/lib -lantlr-pic" break - ], + ], [ - AC_MSG_RESULT(no) - AC_MSG_ERROR([ANTLR C++ runtime not found, see <http://www.antlr.org/>]) + CPPFLAGS="$OLD_CPPFLAGS -I$antlr_prefix/include" + LIBS="$OLD_LIBS -L$antlr_prefix/lib -lantlr" + AC_LINK_IFELSE( + [ + #include <antlr/CommonAST.hpp> + class MyAST : public ANTLR_USE_NAMESPACE(antlr)CommonAST { + }; + int main() { + MyAST ast; + } + ], + [ + AC_MSG_RESULT(found in $antlr_prefix) + ANTLR_INCLUDES="-I$antlr_prefix/include" + ANTLR_LDFLAGS="-L$antlr_prefix/lib -lantlr" + break + ], + [ + AC_MSG_RESULT(no) + AC_MSG_ERROR([ANTLR C++ runtime not found, see <http://www.antlr.org/>]) + ] + ) ] ) done - + # Return the old compile variables and pop the language. LIBS="$OLD_LIBS" CPPFLAGS="$OLD_CPPFLAGS" @@ -15750,14 +15750,55 @@ ac_compiler_gnu=$ac_cv_c_compiler_gnu # Check whether --with-antlr was given. if test "${with_antlr+set}" = set; then : withval=$with_antlr; ANTLR="$withval" +fi + + + # Check the existance of the runantlr script + if test -z "$ANTLR"; then + for ac_prog in runantlr antlr +do + # Extract the first word of "$ac_prog", so it can be a program name with args. +set dummy $ac_prog; ac_word=$2 +{ $as_echo "$as_me:${as_lineno-$LINENO}: checking for $ac_word" >&5 +$as_echo_n "checking for $ac_word... " >&6; } +if test "${ac_cv_prog_ANTLR+set}" = set; then : + $as_echo_n "(cached) " >&6 else - ANTLR="runantlr" + if test -n "$ANTLR"; then + ac_cv_prog_ANTLR="$ANTLR" # Let the user override the test. +else +as_save_IFS=$IFS; IFS=$PATH_SEPARATOR +for as_dir in $PATH +do + IFS=$as_save_IFS + test -z "$as_dir" && as_dir=. + for ac_exec_ext in '' $ac_executable_extensions; do + if { test -f "$as_dir/$ac_word$ac_exec_ext" && $as_test_x "$as_dir/$ac_word$ac_exec_ext"; }; then + ac_cv_prog_ANTLR="$ac_prog" + $as_echo "$as_me:${as_lineno-$LINENO}: found $as_dir/$ac_word$ac_exec_ext" >&5 + break 2 + fi +done + done +IFS=$as_save_IFS fi +fi +ANTLR=$ac_cv_prog_ANTLR +if test -n "$ANTLR"; then + { $as_echo "$as_me:${as_lineno-$LINENO}: result: $ANTLR" >&5 +$as_echo "$ANTLR" >&6; } +else + { $as_echo "$as_me:${as_lineno-$LINENO}: result: no" >&5 +$as_echo "no" >&6; } +fi - # Check the existance of the runantlr script - # Extract the first word of ""$ANTLR"", so it can be a program name with args. + test -n "$ANTLR" && break +done + + else + # Extract the first word of ""$ANTLR"", so it can be a program name with args. set dummy "$ANTLR"; ac_word=$2 { $as_echo "$as_me:${as_lineno-$LINENO}: checking for $ac_word" >&5 $as_echo_n "checking for $ac_word... " >&6; } @@ -15794,6 +15835,7 @@ $as_echo "no" >&6; } fi + fi if test no$ANTLR = "no"; then { $as_echo "$as_me:${as_lineno-$LINENO}: WARNING: Couldn't find the runantlr script, make sure that the parser code has @@ -16058,7 +16100,7 @@ ac_compiler_gnu=$ac_cv_cxx_compiler_gnu for antlr_prefix in $ANTLR_PREFIXES do CPPFLAGS="$OLD_CPPFLAGS -I$antlr_prefix/include" - LIBS="$OLD_LIBS -L$antlr_prefix/lib -lantlr" + LIBS="$OLD_LIBS -L$antlr_prefix/lib -lantlr-pic" cat confdefs.h - <<_ACEOF >conftest.$ac_ext /* end confdefs.h. */ @@ -16080,9 +16122,37 @@ $as_echo "found in $antlr_prefix" >&6; } else - { $as_echo "$as_me:${as_lineno-$LINENO}: result: no" >&5 + CPPFLAGS="$OLD_CPPFLAGS -I$antlr_prefix/include" + LIBS="$OLD_LIBS -L$antlr_prefix/lib -lantlr" + cat confdefs.h - <<_ACEOF >conftest.$ac_ext +/* end confdefs.h. */ + + #include <antlr/CommonAST.hpp> + class MyAST : public ANTLR_USE_NAMESPACE(antlr)CommonAST { + }; + int main() { + MyAST ast; + } + +_ACEOF +if ac_fn_cxx_try_link "$LINENO"; then : + + { $as_echo "$as_me:${as_lineno-$LINENO}: result: found in $antlr_prefix" >&5 +$as_echo "found in $antlr_prefix" >&6; } + ANTLR_INCLUDES="-I$antlr_prefix/include" + ANTLR_LDFLAGS="-L$antlr_prefix/lib -lantlr" + break + +else + + { $as_echo "$as_me:${as_lineno-$LINENO}: result: no" >&5 $as_echo "no" >&6; } - as_fn_error "ANTLR C++ runtime not found, see <http://www.antlr.org/>" "$LINENO" 5 + as_fn_error "ANTLR C++ runtime not found, see <http://www.antlr.org/>" "$LINENO" 5 + + +fi +rm -f core conftest.err conftest.$ac_objext \ + conftest$ac_exeext conftest.$ac_ext fi diff --git a/src/include/cvc4_config.h b/src/include/cvc4_config.h index 95fac9aaa..a42ae28fb 100644 --- a/src/include/cvc4_config.h +++ b/src/include/cvc4_config.h @@ -34,3 +34,4 @@ #define EXPECT_TRUE(x) __builtin_expect( (x), true) #define EXPECT_FALSE(x) __builtin_expect( (x), false) +#define NORETURN __attribute__ ((noreturn)) diff --git a/src/main/main.cpp b/src/main/main.cpp index d4ee8fd0d..8b59e6013 100644 --- a/src/main/main.cpp +++ b/src/main/main.cpp @@ -20,6 +20,8 @@ #include "main.h" #include "usage.h" #include "parser/parser.h" +#include "parser/smt/smt_parser.h" +#include "parser/cvc/cvc_parser.h" #include "expr/expr_manager.h" #include "smt/smt_engine.h" #include "util/command.h" @@ -82,20 +84,16 @@ int main(int argc, char *argv[]) { Warning.setStream(CVC4::null_os); } + const char* fname = inputFromStdin ? argv[firstArgIndex] : "stdin"; + // Create the parser Parser* parser; switch(options.lang) { case Options::LANG_SMTLIB: - if(inputFromStdin) - parser = new SmtParser(&exprMgr, cin); - else - parser = new SmtParser(&exprMgr, argv[firstArgIndex]); + parser = new SmtParser(&exprMgr, cin, fname); break; case Options::LANG_CVC4: - if(inputFromStdin) - parser = new CvcParser(&exprMgr, cin); - else - parser = new CvcParser(&exprMgr, argv[firstArgIndex]); + parser = new CvcParser(&exprMgr, cin, fname); break; case Options::LANG_AUTO: cerr << "Auto language detection not supported yet." << endl; diff --git a/src/parser/Makefile.am b/src/parser/Makefile.am index 8b728f5f4..e54d4aa2d 100644 --- a/src/parser/Makefile.am +++ b/src/parser/Makefile.am @@ -31,7 +31,7 @@ libcvc4parser_la_LIBADD = \ libcvc4parser_la_SOURCES = \ parser.h \ parser.cpp \ + parser_exception.h \ symbol_table.h \ antlr_parser.h \ antlr_parser.cpp - diff --git a/src/parser/Makefile.in b/src/parser/Makefile.in index 231643474..24cd1ed84 100644 --- a/src/parser/Makefile.in +++ b/src/parser/Makefile.in @@ -309,6 +309,7 @@ libcvc4parser_la_LIBADD = \ libcvc4parser_la_SOURCES = \ parser.h \ parser.cpp \ + parser_exception.h \ symbol_table.h \ antlr_parser.h \ antlr_parser.cpp diff --git a/src/parser/cvc/Makefile.am b/src/parser/cvc/Makefile.am index eb0adc39c..6fb9689de 100644 --- a/src/parser/cvc/Makefile.am +++ b/src/parser/cvc/Makefile.am @@ -1,4 +1,4 @@ -INCLUDES = -I@srcdir@/../../include -I@srcdir@/../.. -I@builddir@/../.. +INCLUDES = -I@srcdir@/../../include -I@srcdir@/../.. AM_CXXFLAGS = -Wall -fvisibility=hidden AM_CPPFLAGS = -D__BUILDING_CVC4PARSERLIB @@ -21,8 +21,10 @@ ANTLR_STUFF = \ $(ANTLR_PARSER_STUFF) libparsercvc_la_SOURCES = \ - CvcLexer.g \ - CvcParser.g \ + cvc_lexer.g \ + cvc_parser.g \ + cvc_parser.h \ + cvc_parser.cpp \ $(ANTLR_STUFF) BUILT_SOURCES = $(ANTLR_STUFF) @@ -36,13 +38,15 @@ maintainer-clean-local: mkdir -p @srcdir@/generated touch @srcdir@/stamp-generated # antlr doesn't overwrite output files, it just leaves them. So we have to delete them first. -$(ANTLR_LEXER_STUFF): CvcLexer.g @srcdir@/stamp-generated +@srcdir@/generated/AntlrCvcLexer.hpp: cvc_lexer.g @srcdir@/stamp-generated -rm -f $(ANTLR_LEXER_STUFF) - $(ANTLR) -o "@srcdir@/generated" "@srcdir@/CvcLexer.g" + $(ANTLR) -o "@srcdir@/generated" "@srcdir@/cvc_lexer.g" +@srcdir@/generated/AntlrCvcLexer.cpp $(ANTLR_TOKEN_STUFF): @srcdir@/generated/AntlrCvcLexer.hpp # doesn't actually depend on the lexer, but if we're doing parallel # make and the lexer needs to be rebuilt, we have to keep the rules # from running in parallel (since the token files will be deleted & # recreated) -$(ANTLR_PARSER_STUFF): CvcParser.g CvcLexer.g $(ANTLR_TOKEN_STUFF) @srcdir@/stamp-generated +@srcdir@/generated/AntlrCvcParser.hpp: cvc_parser.g cvc_lexer.g $(ANTLR_TOKEN_STUFF) @srcdir@/stamp-generated -rm -f $(ANTLR_PARSER_STUFF) - $(ANTLR) -o "@srcdir@/generated" "@srcdir@/CvcParser.g" + $(ANTLR) -o "@srcdir@/generated" "@srcdir@/cvc_parser.g" +@srcdir@/generated/AntlrCvcParser.cpp: @srcdir@/generated/AntlrCvcParser.hpp diff --git a/src/parser/cvc/Makefile.in b/src/parser/cvc/Makefile.in index f7358bfcc..b953d3c54 100644 --- a/src/parser/cvc/Makefile.in +++ b/src/parser/cvc/Makefile.in @@ -56,7 +56,7 @@ am__objects_1 = am__objects_2 = AntlrCvcLexer.lo $(am__objects_1) am__objects_3 = AntlrCvcParser.lo am__objects_4 = $(am__objects_2) $(am__objects_3) -am_libparsercvc_la_OBJECTS = $(am__objects_4) +am_libparsercvc_la_OBJECTS = cvc_parser.lo $(am__objects_4) libparsercvc_la_OBJECTS = $(am_libparsercvc_la_OBJECTS) DEFAULT_INCLUDES = -I.@am__isrc@ -I$(top_builddir) depcomp = $(SHELL) $(top_srcdir)/config/depcomp @@ -219,7 +219,7 @@ target_vendor = @target_vendor@ top_build_prefix = @top_build_prefix@ top_builddir = @top_builddir@ top_srcdir = @top_srcdir@ -INCLUDES = -I@srcdir@/../../include -I@srcdir@/../.. -I@builddir@/../.. +INCLUDES = -I@srcdir@/../../include -I@srcdir@/../.. AM_CXXFLAGS = -Wall -fvisibility=hidden AM_CPPFLAGS = -D__BUILDING_CVC4PARSERLIB noinst_LTLIBRARIES = libparsercvc.la @@ -243,8 +243,10 @@ ANTLR_STUFF = \ $(ANTLR_PARSER_STUFF) libparsercvc_la_SOURCES = \ - CvcLexer.g \ - CvcParser.g \ + cvc_lexer.g \ + cvc_parser.g \ + cvc_parser.h \ + cvc_parser.cpp \ $(ANTLR_STUFF) BUILT_SOURCES = $(ANTLR_STUFF) @@ -304,6 +306,7 @@ distclean-compile: @AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/AntlrCvcLexer.Plo@am__quote@ @AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/AntlrCvcParser.Plo@am__quote@ +@AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/cvc_parser.Plo@am__quote@ .cpp.o: @am__fastdepCXX_TRUE@ $(CXXCOMPILE) -MT $@ -MD -MP -MF $(DEPDIR)/$*.Tpo -c -o $@ $< @@ -561,16 +564,18 @@ maintainer-clean-local: mkdir -p @srcdir@/generated touch @srcdir@/stamp-generated # antlr doesn't overwrite output files, it just leaves them. So we have to delete them first. -$(ANTLR_LEXER_STUFF): CvcLexer.g @srcdir@/stamp-generated +@srcdir@/generated/AntlrCvcLexer.hpp: cvc_lexer.g @srcdir@/stamp-generated -rm -f $(ANTLR_LEXER_STUFF) - $(ANTLR) -o "@srcdir@/generated" "@srcdir@/CvcLexer.g" + $(ANTLR) -o "@srcdir@/generated" "@srcdir@/cvc_lexer.g" +@srcdir@/generated/AntlrCvcLexer.cpp $(ANTLR_TOKEN_STUFF): @srcdir@/generated/AntlrCvcLexer.hpp # doesn't actually depend on the lexer, but if we're doing parallel # make and the lexer needs to be rebuilt, we have to keep the rules # from running in parallel (since the token files will be deleted & # recreated) -$(ANTLR_PARSER_STUFF): CvcParser.g CvcLexer.g $(ANTLR_TOKEN_STUFF) @srcdir@/stamp-generated +@srcdir@/generated/AntlrCvcParser.hpp: cvc_parser.g cvc_lexer.g $(ANTLR_TOKEN_STUFF) @srcdir@/stamp-generated -rm -f $(ANTLR_PARSER_STUFF) - $(ANTLR) -o "@srcdir@/generated" "@srcdir@/CvcParser.g" + $(ANTLR) -o "@srcdir@/generated" "@srcdir@/cvc_parser.g" +@srcdir@/generated/AntlrCvcParser.cpp: @srcdir@/generated/AntlrCvcParser.hpp # Tell versions [3.59,3.63) of GNU make to not export all variables. # Otherwise a system limit (for SysV at least) may be exceeded. diff --git a/src/parser/cvc/CvcLexer.g b/src/parser/cvc/cvc_lexer.g index 8d706963f..8d706963f 100644 --- a/src/parser/cvc/CvcLexer.g +++ b/src/parser/cvc/cvc_lexer.g diff --git a/src/parser/cvc/cvc_parser.cpp b/src/parser/cvc/cvc_parser.cpp new file mode 100644 index 000000000..adeb5761d --- /dev/null +++ b/src/parser/cvc/cvc_parser.cpp @@ -0,0 +1,79 @@ +/********************* -*- C++ -*- */ +/** cvc_parser.cpp + ** 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. + ** + ** CVC presentation language parser implementation. + **/ + +#include <iostream> +#include <fstream> + +#include "parser/parser.h" +#include "util/command.h" +#include "util/Assert.h" +#include "parser/parser_exception.h" +#include "parser/antlr_parser.h" +#include "parser/cvc/cvc_parser.h" +#include "parser/cvc/generated/AntlrCvcParser.hpp" +#include "parser/cvc/generated/AntlrCvcLexer.hpp" + +using namespace std; + +namespace CVC4 { +namespace parser { + +Command* CvcParser::parseNextCommand() throw(ParserException) { + Command* cmd = 0; + if(!done()) { + try { + cmd = d_antlr_parser->command(); + if(cmd == 0) { + setDone(); + cmd = new EmptyCommand("EOF"); + } + } catch(antlr::ANTLRException& e) { + setDone(); + throw ParserException(e.toString()); + } + } + return cmd; +} + +Expr CvcParser::parseNextExpression() throw(ParserException) { + Expr result; + if(!done()) { + try { + result = d_antlr_parser->formula(); + } catch(antlr::ANTLRException& e) { + setDone(); + throw ParserException(e.toString()); + } + } + return result; +} + +CvcParser::~CvcParser() { + delete d_antlr_parser; + delete d_antlr_lexer; +} + +CvcParser::CvcParser(ExprManager*em, istream& input, const char* file_name) : + Parser(em), d_input(input) { + if(!d_input) { + throw ParserException(string("Read error") + + ((file_name != NULL) ? (string(" on ") + file_name) : "")); + } + d_antlr_lexer = new AntlrCvcLexer(d_input); + d_antlr_lexer->setFilename(file_name); + d_antlr_parser = new AntlrCvcParser(*d_antlr_lexer); + d_antlr_parser->setExpressionManager(d_expr_manager); + d_antlr_parser->setFilename(file_name); +} + +}/* CVC4::parser namespace */ +}/* CVC4 namespace */ diff --git a/src/parser/cvc/CvcParser.g b/src/parser/cvc/cvc_parser.g index 625f2c381..625f2c381 100644 --- a/src/parser/cvc/CvcParser.g +++ b/src/parser/cvc/cvc_parser.g diff --git a/src/parser/cvc/cvc_parser.h b/src/parser/cvc/cvc_parser.h new file mode 100644 index 000000000..9cb6b7594 --- /dev/null +++ b/src/parser/cvc/cvc_parser.h @@ -0,0 +1,77 @@ +/********************* -*- C++ -*- */ +/** cvc_parser.h + ** 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. + ** + ** CVC presentation language parser abstraction. + **/ + +#ifndef __CVC4__PARSER__CVC_PARSER_H +#define __CVC4__PARSER__CVC_PARSER_H + +#include <string> +#include <iostream> +#include <fstream> +#include "cvc4_config.h" +#include "parser/parser_exception.h" +#include "parser/parser.h" + +namespace CVC4 { +namespace parser { + +/** + * The CVC parser. + */ +class CVC4_PUBLIC CvcParser : public Parser { + +public: + + /** + * Construct the parser that uses the given expression manager and parses + * from the given input stream. + * @param em the expression manager to use + * @param input the input stream to parse + * @param file_name the name of the file (for diagnostic output) + */ + CvcParser(ExprManager* em, std::istream& input, const char* file_name = ""); + + /** + * Destructor. + */ + ~CvcParser(); + + /** + * Parses the next command. By default, the CVC parser produces one + * CommandSequence command. If parsing is successful, we should be + * done after the first call to this command. + * @return the CommandSequence command that includes the whole + * benchmark + */ + Command* parseNextCommand() throw(ParserException); + + /** + * Parses the next complete expression of the stream. + * @return the expression parsed + */ + Expr parseNextExpression() throw(ParserException); + +protected: + + /** The ANTLR smt lexer */ + AntlrCvcLexer* d_antlr_lexer; + + /** The ANTLR smt parser */ + AntlrCvcParser* d_antlr_parser; + + /** The file stream we might be using */ + std::istream& d_input; +}; + +}/* CVC4::parser namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__PARSER__CVC_PARSER_H */ diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index 4309ec355..8d4af5ba1 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -40,112 +40,5 @@ bool Parser::done() const { return d_done; } -Command* SmtParser::parseNextCommand() throw (ParserException) { - Command* cmd = 0; - if(!done()) { - try { - cmd = d_antlr_parser->benchmark(); - setDone(); - } catch(antlr::ANTLRException& e) { - setDone(); - throw ParserException(e.toString()); - } - } - return cmd; -} - -Expr SmtParser::parseNextExpression() throw (ParserException) { - Expr result; - if (!done()) { - try { - result = d_antlr_parser->an_formula(); - } catch(antlr::ANTLRException& e) { - setDone(); - throw ParserException(e.toString()); - } - } - return result; -} - -SmtParser::~SmtParser() { - delete d_antlr_parser; - delete d_antlr_lexer; -} - -SmtParser::SmtParser(ExprManager* em, istream& input) : - Parser(em) { - d_antlr_lexer = new AntlrSmtLexer(input); - d_antlr_parser = new AntlrSmtParser(*d_antlr_lexer); - d_antlr_parser->setExpressionManager(d_expr_manager); -} - -SmtParser::SmtParser(ExprManager*em, const char* file_name) : - Parser(em), d_input(file_name) { - if(!d_input) { - throw ParserException(string("File not found or inaccessible: ") + file_name); - } - d_antlr_lexer = new AntlrSmtLexer(d_input); - d_antlr_lexer->setFilename(file_name); - d_antlr_parser = new AntlrSmtParser(*d_antlr_lexer); - d_antlr_parser->setExpressionManager(d_expr_manager); - d_antlr_parser->setFilename(file_name); -} - -Command* CvcParser::parseNextCommand() throw (ParserException) { - Command* cmd = 0; - if(!done()) { - try { - cmd = d_antlr_parser->command(); - if (cmd == 0) { - setDone(); - cmd = new EmptyCommand("EOF"); - } - } catch(antlr::ANTLRException& e) { - setDone(); - throw ParserException(e.toString()); - } - } - return cmd; -} - -Expr CvcParser::parseNextExpression() throw (ParserException) { - Expr result; - if (!done()) { - try { - result = d_antlr_parser->formula(); - } catch(antlr::ANTLRException& e) { - setDone(); - throw ParserException(e.toString()); - } - } - return result; -} - -CvcParser::~CvcParser() { - delete d_antlr_parser; - delete d_antlr_lexer; -} - -CvcParser::CvcParser(ExprManager* em, istream& input) : - Parser(em) { - d_antlr_lexer = new AntlrCvcLexer(input); - d_antlr_parser = new AntlrCvcParser(*d_antlr_lexer); - d_antlr_parser->setExpressionManager(d_expr_manager); -} - -CvcParser::CvcParser(ExprManager*em, const char* file_name) : - Parser(em), d_input(file_name) { - if(!d_input) { - throw ParserException(string("File not found or inaccessible: ") + file_name); - } - d_antlr_lexer = new AntlrCvcLexer(d_input); - d_antlr_lexer->setFilename(file_name); - d_antlr_parser = new AntlrCvcParser(*d_antlr_lexer); - d_antlr_parser->setExpressionManager(d_expr_manager); - d_antlr_parser->setFilename(file_name); -} - - }/* CVC4::parser namespace */ }/* CVC4 namespace */ - diff --git a/src/parser/parser.h b/src/parser/parser.h index dbdca4af8..7755d65f0 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -80,109 +80,6 @@ protected: }; // end of class Parser -class CVC4_PUBLIC SmtParser : public Parser { - -public: - - /** - * Construct the parser that uses the given expression manager and parses - * from the given input stream. - * @param em the expression manager to use - * @param input the input stream to parse - */ - SmtParser(ExprManager* em, std::istream& input); - - /** - * Construct the parser that uses the given expression manager and parses - * from the file. - * @param em the expression manager to use - * @param file_name the file to parse - */ - SmtParser(ExprManager* em, const char* file_name); - - /** - * Destructor. - */ - ~SmtParser(); - - /** - * Parses the next command. By default, the SMTLIB parser produces one - * CommandSequence command. If parsing is successful, we should be done - * after the first call to this command. - * @return the CommandSequence command that includes the whole benchmark - */ - Command* parseNextCommand() throw (ParserException); - - /** - * Parses the next complete expression of the stream. - * @return the expression parsed - */ - Expr parseNextExpression() throw (ParserException); - -protected: - - /** The ANTLR smt lexer */ - AntlrSmtLexer* d_antlr_lexer; - - /** The ANTLR smt parser */ - AntlrSmtParser* d_antlr_parser; - - /** The file stream we might be using */ - std::ifstream d_input; -}; - -class CVC4_PUBLIC CvcParser : public Parser { - -public: - - /** - * Construct the parser that uses the given expression manager and parses - * from the given input stream. - * @param em the expression manager to use - * @param input the input stream to parse - */ - CvcParser(ExprManager* em, std::istream& input); - - /** - * Construct the parser that uses the given expression manager and parses - * from the file. - * @param em the expression manager to use - * @param file_name the file to parse - */ - CvcParser(ExprManager* em, const char* file_name); - - /** - * Destructor. - */ - ~CvcParser(); - - /** - * Parses the next command. By default, the SMTLIB parser produces one - * CommandSequence command. If parsing is successful, we should be done - * after the first call to this command. - * @return the CommandSequence command that includes the whole benchmark - */ - Command* parseNextCommand() throw (ParserException); - - /** - * Parses the next complete expression of the stream. - * @return the expression parsed - */ - Expr parseNextExpression() throw (ParserException); - -protected: - - /** The ANTLR smt lexer */ - AntlrCvcLexer* d_antlr_lexer; - - /** The ANTLR smt parser */ - AntlrCvcParser* d_antlr_parser; - - /** The file stream we might be using */ - std::ifstream d_input; -}; - - }/* CVC4::parser namespace */ }/* CVC4 namespace */ diff --git a/src/parser/smt/Makefile.am b/src/parser/smt/Makefile.am index a6d234bd0..c3273f501 100644 --- a/src/parser/smt/Makefile.am +++ b/src/parser/smt/Makefile.am @@ -1,4 +1,4 @@ -INCLUDES = -I@srcdir@/../../include -I@srcdir@/../.. -I@builddir@/../.. +INCLUDES = -I@srcdir@/../../include -I@srcdir@/../.. AM_CXXFLAGS = -Wall -fvisibility=hidden AM_CPPFLAGS = -D__BUILDING_CVC4PARSERLIB @@ -21,8 +21,10 @@ ANTLR_STUFF = \ $(ANTLR_PARSER_STUFF) libparsersmt_la_SOURCES = \ - SmtLexer.g \ - SmtParser.g \ + smt_lexer.g \ + smt_parser.g \ + smt_parser.h \ + smt_parser.cpp \ $(ANTLR_STUFF) BUILT_SOURCES = $(ANTLR_STUFF) @@ -36,13 +38,15 @@ maintainer-clean-local: mkdir -p @srcdir@/generated touch @srcdir@/stamp-generated # antlr doesn't overwrite output files, it just leaves them. So we have to delete them first. -$(ANTLR_LEXER_STUFF): SmtLexer.g @srcdir@/stamp-generated +@srcdir@/generated/AntlrSmtLexer.hpp: smt_lexer.g @srcdir@/stamp-generated -rm -f $(ANTLR_LEXER_STUFF) - $(ANTLR) -o "@srcdir@/generated" "@srcdir@/SmtLexer.g" + $(ANTLR) -o "@srcdir@/generated" "@srcdir@/smt_lexer.g" +@srcdir@/generated/AntlrSmtLexer.cpp $(ANTLR_TOKEN_STUFF): @srcdir@/generated/AntlrSmtLexer.hpp # doesn't actually depend on the lexer, but if we're doing parallel # make and the lexer needs to be rebuilt, we have to keep the rules # from running in parallel (since the token files will be deleted & # recreated) -$(ANTLR_PARSER_STUFF): SmtParser.g SmtLexer.g $(ANTLR_TOKEN_STUFF) @srcdir@/stamp-generated +@srcdir@/generated/AntlrSmtParser.hpp: smt_parser.g smt_lexer.g $(ANTLR_TOKEN_STUFF) @srcdir@/stamp-generated -rm -f $(ANTLR_PARSER_STUFF) - $(ANTLR) -o "@srcdir@/generated" "@srcdir@/SmtParser.g" + $(ANTLR) -o "@srcdir@/generated" "@srcdir@/smt_parser.g" +@srcdir@/generated/AntlrSmtParser.cpp: @srcdir@/generated/AntlrSmtParser.hpp diff --git a/src/parser/smt/Makefile.in b/src/parser/smt/Makefile.in index 20c91c28a..e153135c5 100644 --- a/src/parser/smt/Makefile.in +++ b/src/parser/smt/Makefile.in @@ -56,7 +56,7 @@ am__objects_1 = am__objects_2 = AntlrSmtLexer.lo $(am__objects_1) am__objects_3 = AntlrSmtParser.lo am__objects_4 = $(am__objects_2) $(am__objects_3) -am_libparsersmt_la_OBJECTS = $(am__objects_4) +am_libparsersmt_la_OBJECTS = smt_parser.lo $(am__objects_4) libparsersmt_la_OBJECTS = $(am_libparsersmt_la_OBJECTS) DEFAULT_INCLUDES = -I.@am__isrc@ -I$(top_builddir) depcomp = $(SHELL) $(top_srcdir)/config/depcomp @@ -219,7 +219,7 @@ target_vendor = @target_vendor@ top_build_prefix = @top_build_prefix@ top_builddir = @top_builddir@ top_srcdir = @top_srcdir@ -INCLUDES = -I@srcdir@/../../include -I@srcdir@/../.. -I@builddir@/../.. +INCLUDES = -I@srcdir@/../../include -I@srcdir@/../.. AM_CXXFLAGS = -Wall -fvisibility=hidden AM_CPPFLAGS = -D__BUILDING_CVC4PARSERLIB noinst_LTLIBRARIES = libparsersmt.la @@ -243,8 +243,10 @@ ANTLR_STUFF = \ $(ANTLR_PARSER_STUFF) libparsersmt_la_SOURCES = \ - SmtLexer.g \ - SmtParser.g \ + smt_lexer.g \ + smt_parser.g \ + smt_parser.h \ + smt_parser.cpp \ $(ANTLR_STUFF) BUILT_SOURCES = $(ANTLR_STUFF) @@ -304,6 +306,7 @@ distclean-compile: @AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/AntlrSmtLexer.Plo@am__quote@ @AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/AntlrSmtParser.Plo@am__quote@ +@AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/smt_parser.Plo@am__quote@ .cpp.o: @am__fastdepCXX_TRUE@ $(CXXCOMPILE) -MT $@ -MD -MP -MF $(DEPDIR)/$*.Tpo -c -o $@ $< @@ -561,16 +564,18 @@ maintainer-clean-local: mkdir -p @srcdir@/generated touch @srcdir@/stamp-generated # antlr doesn't overwrite output files, it just leaves them. So we have to delete them first. -$(ANTLR_LEXER_STUFF): SmtLexer.g @srcdir@/stamp-generated +@srcdir@/generated/AntlrSmtLexer.hpp: smt_lexer.g @srcdir@/stamp-generated -rm -f $(ANTLR_LEXER_STUFF) - $(ANTLR) -o "@srcdir@/generated" "@srcdir@/SmtLexer.g" + $(ANTLR) -o "@srcdir@/generated" "@srcdir@/smt_lexer.g" +@srcdir@/generated/AntlrSmtLexer.cpp $(ANTLR_TOKEN_STUFF): @srcdir@/generated/AntlrSmtLexer.hpp # doesn't actually depend on the lexer, but if we're doing parallel # make and the lexer needs to be rebuilt, we have to keep the rules # from running in parallel (since the token files will be deleted & # recreated) -$(ANTLR_PARSER_STUFF): SmtParser.g SmtLexer.g $(ANTLR_TOKEN_STUFF) @srcdir@/stamp-generated +@srcdir@/generated/AntlrSmtParser.hpp: smt_parser.g smt_lexer.g $(ANTLR_TOKEN_STUFF) @srcdir@/stamp-generated -rm -f $(ANTLR_PARSER_STUFF) - $(ANTLR) -o "@srcdir@/generated" "@srcdir@/SmtParser.g" + $(ANTLR) -o "@srcdir@/generated" "@srcdir@/smt_parser.g" +@srcdir@/generated/AntlrSmtParser.cpp: @srcdir@/generated/AntlrSmtParser.hpp # Tell versions [3.59,3.63) of GNU make to not export all variables. # Otherwise a system limit (for SysV at least) may be exceeded. diff --git a/src/parser/smt/SmtLexer.g b/src/parser/smt/smt_lexer.g index 3d9a84f06..3d9a84f06 100644 --- a/src/parser/smt/SmtLexer.g +++ b/src/parser/smt/smt_lexer.g diff --git a/src/parser/smt/smt_parser.cpp b/src/parser/smt/smt_parser.cpp new file mode 100644 index 000000000..65d36690c --- /dev/null +++ b/src/parser/smt/smt_parser.cpp @@ -0,0 +1,76 @@ +/********************* -*- C++ -*- */ +/** smt_parser.cpp + ** 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. + ** + ** SMT-LIB language parser implementation. + **/ + +#include <iostream> +#include <fstream> + +#include "parser/parser.h" +#include "util/command.h" +#include "util/Assert.h" +#include "parser/parser_exception.h" +#include "parser/antlr_parser.h" +#include "parser/smt/smt_parser.h" +#include "parser/smt/generated/AntlrSmtParser.hpp" +#include "parser/smt/generated/AntlrSmtLexer.hpp" + +using namespace std; + +namespace CVC4 { +namespace parser { + +Command* SmtParser::parseNextCommand() throw(ParserException) { + Command* cmd = 0; + if(!done()) { + try { + cmd = d_antlr_parser->benchmark(); + setDone(); + } catch(antlr::ANTLRException& e) { + setDone(); + throw ParserException(e.toString()); + } + } + return cmd; +} + +Expr SmtParser::parseNextExpression() throw(ParserException) { + Expr result; + if(!done()) { + try { + result = d_antlr_parser->an_formula(); + } catch(antlr::ANTLRException& e) { + setDone(); + throw ParserException(e.toString()); + } + } + return result; +} + +SmtParser::~SmtParser() { + delete d_antlr_parser; + delete d_antlr_lexer; +} + +SmtParser::SmtParser(ExprManager* em, istream& input, const char* file_name) : + Parser(em), d_input(input) { + if(!d_input) { + throw ParserException(string("Read error") + + ((file_name != NULL) ? (string(" on ") + file_name) : "")); + } + d_antlr_lexer = new AntlrSmtLexer(input); + d_antlr_lexer->setFilename(file_name); + d_antlr_parser = new AntlrSmtParser(*d_antlr_lexer); + d_antlr_parser->setExpressionManager(d_expr_manager); + d_antlr_parser->setFilename(file_name); +} + +}/* CVC4::parser namespace */ +}/* CVC4 namespace */ diff --git a/src/parser/smt/SmtParser.g b/src/parser/smt/smt_parser.g index f68d783bc..f68d783bc 100644 --- a/src/parser/smt/SmtParser.g +++ b/src/parser/smt/smt_parser.g diff --git a/src/parser/smt/smt_parser.h b/src/parser/smt/smt_parser.h new file mode 100644 index 000000000..a68f0e783 --- /dev/null +++ b/src/parser/smt/smt_parser.h @@ -0,0 +1,77 @@ +/********************* -*- C++ -*- */ +/** smt_parser.h + ** 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. + ** + ** SMT-LIB language parser abstraction. + **/ + +#ifndef __CVC4__PARSER__SMT_PARSER_H +#define __CVC4__PARSER__SMT_PARSER_H + +#include <string> +#include <iostream> +#include <fstream> +#include "cvc4_config.h" +#include "parser/parser_exception.h" +#include "parser/parser.h" + +namespace CVC4 { +namespace parser { + +/** + * The SMT parser. + */ +class CVC4_PUBLIC SmtParser : public Parser { + +public: + + /** + * Construct the parser that uses the given expression manager and parses + * from the given input stream. + * @param em the expression manager to use + * @param input the input stream to parse + * @param file_name the name of the file (for diagnostic output) + */ + SmtParser(ExprManager* em, std::istream& input, const char* file_name = ""); + + /** + * Destructor. + */ + ~SmtParser(); + + /** + * Parses the next command. By default, the SMT-LIB parser produces + * one CommandSequence command. If parsing is successful, we should + * be done after the first call to this command. + * @return the CommandSequence command that includes the whole + * benchmark + */ + Command* parseNextCommand() throw(ParserException); + + /** + * Parses the next complete expression of the stream. + * @return the expression parsed + */ + Expr parseNextExpression() throw(ParserException); + +protected: + + /** The ANTLR smt lexer */ + AntlrSmtLexer* d_antlr_lexer; + + /** The ANTLR smt parser */ + AntlrSmtParser* d_antlr_parser; + + /** The file stream we might be using */ + std::istream& d_input; +}; + +}/* CVC4::parser namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__PARSER__SMT_PARSER_H */ diff --git a/src/prop/Makefile.am b/src/prop/Makefile.am index 4071197ad..715e79d16 100644 --- a/src/prop/Makefile.am +++ b/src/prop/Makefile.am @@ -5,6 +5,8 @@ AM_CPPFLAGS = -D__BUILDING_CVC4LIB noinst_LTLIBRARIES = libprop.la libprop_la_SOURCES = \ - prop_engine.cpp + prop_engine.cpp \ + prop_engine.h \ + sat.h SUBDIRS = minisat diff --git a/src/prop/Makefile.in b/src/prop/Makefile.in index 1bfd4d706..5fb636c23 100644 --- a/src/prop/Makefile.in +++ b/src/prop/Makefile.in @@ -67,6 +67,15 @@ CXXLD = $(CXX) CXXLINK = $(LIBTOOL) --tag=CXX $(AM_LIBTOOLFLAGS) $(LIBTOOLFLAGS) \ --mode=link $(CXXLD) $(AM_CXXFLAGS) $(CXXFLAGS) $(AM_LDFLAGS) \ $(LDFLAGS) -o $@ +COMPILE = $(CC) $(DEFS) $(DEFAULT_INCLUDES) $(INCLUDES) $(AM_CPPFLAGS) \ + $(CPPFLAGS) $(AM_CFLAGS) $(CFLAGS) +LTCOMPILE = $(LIBTOOL) --tag=CC $(AM_LIBTOOLFLAGS) $(LIBTOOLFLAGS) \ + --mode=compile $(CC) $(DEFS) $(DEFAULT_INCLUDES) $(INCLUDES) \ + $(AM_CPPFLAGS) $(CPPFLAGS) $(AM_CFLAGS) $(CFLAGS) +CCLD = $(CC) +LINK = $(LIBTOOL) --tag=CC $(AM_LIBTOOLFLAGS) $(LIBTOOLFLAGS) \ + --mode=link $(CCLD) $(AM_CFLAGS) $(CFLAGS) $(AM_LDFLAGS) \ + $(LDFLAGS) -o $@ SOURCES = $(libprop_la_SOURCES) DIST_SOURCES = $(libprop_la_SOURCES) RECURSIVE_TARGETS = all-recursive check-recursive dvi-recursive \ @@ -249,7 +258,9 @@ AM_CXXFLAGS = -Wall -fvisibility=hidden AM_CPPFLAGS = -D__BUILDING_CVC4LIB noinst_LTLIBRARIES = libprop.la libprop_la_SOURCES = \ - prop_engine.cpp + prop_engine.cpp \ + prop_engine.h \ + sat.h SUBDIRS = minisat all: all-recursive diff --git a/src/prop/minisat/Makefile.am b/src/prop/minisat/Makefile.am index f2716ff56..cef9a4c1e 100644 --- a/src/prop/minisat/Makefile.am +++ b/src/prop/minisat/Makefile.am @@ -5,4 +5,23 @@ AM_CPPFLAGS = -D__BUILDING_CVC4LIB noinst_LTLIBRARIES = libminisat.la libminisat_la_SOURCES = \ core/Solver.C \ - simp/SimpSolver.C + core/Solver.h \ + core/SolverTypes.h \ + simp/SimpSolver.C \ + simp/SimpSolver.h + +EXTRA_DIST = \ + core/Main.C \ + core/Makefile \ + simp/Main.C \ + simp/Makefile \ + README \ + LICENSE \ + mtl/Heap.h \ + mtl/Map.h \ + mtl/Queue.h \ + mtl/Alg.h \ + mtl/Sort.h \ + mtl/BasicHeap.h \ + mtl/BoxedVec.h \ + mtl/template.mk diff --git a/src/prop/minisat/Makefile.in b/src/prop/minisat/Makefile.in index fe890e46a..646389c80 100644 --- a/src/prop/minisat/Makefile.in +++ b/src/prop/minisat/Makefile.in @@ -67,6 +67,15 @@ CXXLD = $(CXX) CXXLINK = $(LIBTOOL) --tag=CXX $(AM_LIBTOOLFLAGS) $(LIBTOOLFLAGS) \ --mode=link $(CXXLD) $(AM_CXXFLAGS) $(CXXFLAGS) $(AM_LDFLAGS) \ $(LDFLAGS) -o $@ +COMPILE = $(CC) $(DEFS) $(DEFAULT_INCLUDES) $(INCLUDES) $(AM_CPPFLAGS) \ + $(CPPFLAGS) $(AM_CFLAGS) $(CFLAGS) +LTCOMPILE = $(LIBTOOL) --tag=CC $(AM_LIBTOOLFLAGS) $(LIBTOOLFLAGS) \ + --mode=compile $(CC) $(DEFS) $(DEFAULT_INCLUDES) $(INCLUDES) \ + $(AM_CPPFLAGS) $(CPPFLAGS) $(AM_CFLAGS) $(CFLAGS) +CCLD = $(CC) +LINK = $(LIBTOOL) --tag=CC $(AM_LIBTOOLFLAGS) $(LIBTOOLFLAGS) \ + --mode=link $(CCLD) $(AM_CFLAGS) $(CFLAGS) $(AM_LDFLAGS) \ + $(LDFLAGS) -o $@ SOURCES = $(libminisat_la_SOURCES) DIST_SOURCES = $(libminisat_la_SOURCES) ETAGS = etags @@ -212,7 +221,26 @@ AM_CPPFLAGS = -D__BUILDING_CVC4LIB noinst_LTLIBRARIES = libminisat.la libminisat_la_SOURCES = \ core/Solver.C \ - simp/SimpSolver.C + core/Solver.h \ + core/SolverTypes.h \ + simp/SimpSolver.C \ + simp/SimpSolver.h + +EXTRA_DIST = \ + core/Main.C \ + core/Makefile \ + simp/Main.C \ + simp/Makefile \ + README \ + LICENSE \ + mtl/Heap.h \ + mtl/Map.h \ + mtl/Queue.h \ + mtl/Alg.h \ + mtl/Sort.h \ + mtl/BasicHeap.h \ + mtl/BoxedVec.h \ + mtl/template.mk all: all-am diff --git a/src/util/Assert.cpp b/src/util/Assert.cpp new file mode 100644 index 000000000..799af12ab --- /dev/null +++ b/src/util/Assert.cpp @@ -0,0 +1,101 @@ +/********************* -*- C++ -*- */ +/** Assert.cpp + ** 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. + ** + ** Assertion utility classes, functions, and exceptions. Implementation. + **/ + +#include <new> +#include <cstdarg> +#include <cstdio> +#include "util/Assert.h" +#include "util/exception.h" +#include "cvc4_config.h" +#include "config.h" + +using namespace std; + +namespace CVC4 { + +void AssertionException::construct(const char* header, const char* extra, + const char* function, const char* file, + unsigned line, const char* fmt, + va_list args) { + // try building the exception msg with a smallish buffer first, + // then with a larger one if sprintf tells us to. + int n = 256; + char* buf; + + for(;;) { + buf = new char[n]; + + int size; + if(extra == NULL) { + size = snprintf(buf, n, "%s\n%s\n%s:%d\n", + header, function, file, line); + } else { + size = snprintf(buf, n, "%s\n%s\n%s:%d:\n\n %s\n", + header, function, file, line, extra); + } + + if(size < n) { + va_list args_copy; + va_copy(args_copy, args); + size += vsnprintf(buf + size, n - size, fmt, args); + va_end(args_copy); + + if(size < n) { + break; + } + } + + if(size >= n) { + // try again with a buffer that's large enough + n = size + 1; + delete [] buf; + } + } + + setMessage(string(buf)); + delete [] buf; +} + +void AssertionException::construct(const char* header, const char* extra, + const char* function, const char* file, + unsigned line) { + // try building the exception msg with a smallish buffer first, + // then with a larger one if sprintf tells us to. + int n = 256; + char* buf; + + for(;;) { + buf = new char[n]; + + int size; + if(extra == NULL) { + size = snprintf(buf, n, "%s.\n%s\n%s:%d\n", + header, function, file, line); + } else { + size = snprintf(buf, n, "%s.\n%s\n%s:%d:\n\n %s\n", + header, function, file, line, extra); + } + + if(size < n) { + break; + } else { + // try again with a buffer that's large enough + n = size + 1; + delete [] buf; + } + } + + setMessage(string(buf)); + delete [] buf; +} + +}/* CVC4 namespace */ diff --git a/src/util/Assert.h b/src/util/Assert.h index 8fd970c6c..3da76c5db 100644 --- a/src/util/Assert.h +++ b/src/util/Assert.h @@ -1,5 +1,5 @@ /********************* -*- C++ -*- */ -/** assert.h +/** Assert.h ** This file is part of the CVC4 prototype. ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences @@ -7,13 +7,15 @@ ** See the file COPYING in the top-level source directory for licensing ** information. ** - ** Assertion utility classes, functions, and exceptions. + ** Assertion utility classes, functions, exceptions, and macros. **/ #ifndef __CVC4__ASSERT_H #define __CVC4__ASSERT_H #include <string> +#include <cstdio> +#include <cstdarg> #include "util/exception.h" #include "cvc4_config.h" #include "config.h" @@ -21,91 +23,136 @@ namespace CVC4 { class CVC4_PUBLIC AssertionException : public Exception { -public: +protected: + void construct(const char* header, const char* extra, + const char* function, const char* file, + unsigned line, const char* fmt, ...) { + va_list args; + va_start(args, fmt); + 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); + AssertionException() : Exception() {} - AssertionException(std::string msg) : Exception(msg) {} - AssertionException(const char* msg) : Exception(msg) {} + +public: + AssertionException(const char* extra, const char* function, + const char* file, unsigned line, + const char* fmt, ...) : + Exception() { + va_list args; + va_start(args, fmt); + construct("Assertion failure", extra, function, file, line, fmt, args); + va_end(args); + } + + AssertionException(const char* extra, const char* function, + const char* file, unsigned line) : + Exception() { + construct("Assertion failure", extra, function, file, line); + } };/* class AssertionException */ class CVC4_PUBLIC UnreachableCodeException : public AssertionException { -public: +protected: UnreachableCodeException() : AssertionException() {} - UnreachableCodeException(std::string msg) : AssertionException(msg) {} - UnreachableCodeException(const char* msg) : AssertionException(msg) {} + +public: + UnreachableCodeException(const char* function, const char* file, + unsigned line, const char* fmt, ...) : + AssertionException() { + va_list args; + va_start(args, fmt); + construct("Unreachable code reached", + NULL, function, file, line, fmt, args); + va_end(args); + } + + UnreachableCodeException(const char* function, const char* file, + unsigned line) : + AssertionException() { + construct("Unreachable code reached", NULL, function, file, line); + } };/* class UnreachableCodeException */ class CVC4_PUBLIC UnhandledCaseException : public UnreachableCodeException { -public: +protected: UnhandledCaseException() : UnreachableCodeException() {} - UnhandledCaseException(std::string msg) : UnreachableCodeException(msg) {} - UnhandledCaseException(const char* msg) : UnreachableCodeException(msg) {} + +public: + UnhandledCaseException(const char* function, const char* file, + unsigned line, const char* fmt, ...) : + UnreachableCodeException() { + va_list args; + va_start(args, fmt); + construct("Unhandled case encountered", + NULL, function, file, line, fmt, args); + va_end(args); + } + + UnhandledCaseException(const char* function, const char* file, + unsigned line, int theCase) : + UnreachableCodeException() { + construct("Unhandled case encountered", + NULL, function, file, line, "The case was: %d", theCase); + } + + UnhandledCaseException(const char* function, const char* file, + unsigned line) : + UnreachableCodeException() { + construct("Unhandled case encountered", NULL, function, file, line); + } };/* class UnhandledCaseException */ +class CVC4_PUBLIC IllegalArgumentException : public AssertionException { +protected: + IllegalArgumentException() : AssertionException() {} + +public: + IllegalArgumentException(const char* argDesc, const char* function, + const char* file, unsigned line, + const char* fmt, ...) : + AssertionException() { + va_list args; + va_start(args, fmt); + construct("Illegal argument detected", + argDesc, function, file, line, fmt, args); + va_end(args); + } + + IllegalArgumentException(const char* argDesc, const char* function, + const char* file, unsigned line) : + AssertionException() { + construct("Illegal argument detected", + argDesc, function, file, line); + } +};/* class IllegalArgumentException */ + +#define AlwaysAssert(cond, msg...) \ + do { \ + if(EXPECT_FALSE( ! (cond) )) { \ + throw AssertionException(#cond, __FUNCTION__, __FILE__, __LINE__, ## msg); \ + } \ + } while(0) +#define Unreachable(msg...) \ + throw UnreachableCodeException(__FUNCTION__, __FILE__, __LINE__, ## msg) +#define Unhandled(msg...) \ + throw UnhandledCaseException(__FUNCTION__, __FILE__, __LINE__, ## msg) +#define IllegalArgument(arg, msg...) \ + throw IllegalArgumentException(#arg, __FUNCTION__, __FILE__, __LINE__, ## msg) + #ifdef CVC4_ASSERTIONS -# define Assert(cond, msg...) __CVC4_ASSERTGLUE("Assertion failure at " __FILE__ ":", __LINE__, ": " #cond, __builtin_expect((cond), 1), ## msg) +# define Assert(cond, msg...) AlwaysAssert(cond, ## msg) #else /* ! CVC4_ASSERTIONS */ # define Assert(cond, msg...) /*EXPECT_TRUE( cond )*/ #endif /* CVC4_ASSERTIONS */ -#define AlwaysAssert(cond, msg...) __CVC4_ASSERTGLUE("Assertion failure at " __FILE__ ":", __LINE__, ": " #cond, __builtin_expect((cond), 1), ## msg) -#define Unreachable(msg...) __CVC4_UNREACHABLEGLUE("Hit a section of unreachable code at " __FILE__ ":", __LINE__, ## msg) -#define Unhandled(msg...) __CVC4_UNHANDLEDGLUE("Hit an unhandled case at " __FILE__ ":", __LINE__, ## msg) - -#define __CVC4_ASSERTGLUE(str1, line, str2, cond, msg...) AssertImpl(str1 #line str2, cond, ## msg) -#define __CVC4_UNREACHABLEGLUE(str, line, msg...) UnreachableImpl(str #line, ## msg) -#define __CVC4_UNHANDLEDGLUE(str, line, msg...) UnhandledImpl(str #line, ## msg) - -inline void AssertImpl(const char* info, bool cond, std::string msg) { - if(EXPECT_FALSE( ! cond )) - throw AssertionException(std::string(info) + "\n" + msg); -} - -inline void AssertImpl(const char* info, bool cond, const char* msg) { - if(EXPECT_FALSE( ! cond )) - throw AssertionException(std::string(info) + "\n" + msg); -} - -inline void AssertImpl(const char* info, bool cond) { - if(EXPECT_FALSE( ! cond )) - throw AssertionException(info); -} - -#ifdef __GNUC__ -inline void UnreachableImpl(const char* info, std::string msg) __attribute__ ((noreturn)); -inline void UnreachableImpl(const char* info, const char* msg) __attribute__ ((noreturn)); -inline void UnreachableImpl(const char* info) __attribute__ ((noreturn)); -#endif /* __GNUC__ */ - -inline void UnreachableImpl(const char* info, std::string msg) { - throw UnreachableCodeException(std::string(info) + "\n" + msg); -} - -inline void UnreachableImpl(const char* info, const char* msg) { - throw UnreachableCodeException(std::string(info) + "\n" + msg); -} - -inline void UnreachableImpl(const char* info) { - throw UnreachableCodeException(info); -} - -#ifdef __GNUC__ -inline void UnhandledImpl(const char* info, std::string msg) __attribute__ ((noreturn)); -inline void UnhandledImpl(const char* info, const char* msg) __attribute__ ((noreturn)); -inline void UnhandledImpl(const char* info) __attribute__ ((noreturn)); -#endif /* __GNUC__ */ - -inline void UnhandledImpl(const char* info, std::string msg) { - throw UnhandledCaseException(std::string(info) + "\n" + msg); -} - -inline void UnhandledImpl(const char* info, const char* msg) { - throw UnhandledCaseException(std::string(info) + "\n" + msg); -} - -inline void UnhandledImpl(const char* info) { - throw UnhandledCaseException(info); -} - }/* CVC4 namespace */ #endif /* __CVC4__ASSERT_H */ diff --git a/src/util/Makefile.am b/src/util/Makefile.am index 8baf872d2..b6c116a6d 100644 --- a/src/util/Makefile.am +++ b/src/util/Makefile.am @@ -5,6 +5,20 @@ AM_CPPFLAGS = -D__BUILDING_CVC4LIB noinst_LTLIBRARIES = libutil.la libutil_la_SOURCES = \ + Assert.h \ + Assert.cpp \ + Makefile.am \ + Makefile.in \ command.cpp \ + command.h \ + debug.h \ decision_engine.cpp \ - output.cpp + decision_engine.h \ + exception.h \ + literal.h \ + model.h \ + options.h \ + output.cpp \ + output.h \ + result.h \ + unique_id.h diff --git a/src/util/Makefile.in b/src/util/Makefile.in index ac8d4b522..9f17df4c7 100644 --- a/src/util/Makefile.in +++ b/src/util/Makefile.in @@ -52,7 +52,8 @@ CONFIG_CLEAN_FILES = CONFIG_CLEAN_VPATH_FILES = LTLIBRARIES = $(noinst_LTLIBRARIES) libutil_la_LIBADD = -am_libutil_la_OBJECTS = command.lo decision_engine.lo output.lo +am_libutil_la_OBJECTS = Assert.lo command.lo decision_engine.lo \ + output.lo libutil_la_OBJECTS = $(am_libutil_la_OBJECTS) DEFAULT_INCLUDES = -I.@am__isrc@ -I$(top_builddir) depcomp = $(SHELL) $(top_srcdir)/config/depcomp @@ -67,6 +68,15 @@ CXXLD = $(CXX) CXXLINK = $(LIBTOOL) --tag=CXX $(AM_LIBTOOLFLAGS) $(LIBTOOLFLAGS) \ --mode=link $(CXXLD) $(AM_CXXFLAGS) $(CXXFLAGS) $(AM_LDFLAGS) \ $(LDFLAGS) -o $@ +COMPILE = $(CC) $(DEFS) $(DEFAULT_INCLUDES) $(INCLUDES) $(AM_CPPFLAGS) \ + $(CPPFLAGS) $(AM_CFLAGS) $(CFLAGS) +LTCOMPILE = $(LIBTOOL) --tag=CC $(AM_LIBTOOLFLAGS) $(LIBTOOLFLAGS) \ + --mode=compile $(CC) $(DEFS) $(DEFAULT_INCLUDES) $(INCLUDES) \ + $(AM_CPPFLAGS) $(CPPFLAGS) $(AM_CFLAGS) $(CFLAGS) +CCLD = $(CC) +LINK = $(LIBTOOL) --tag=CC $(AM_LIBTOOLFLAGS) $(LIBTOOLFLAGS) \ + --mode=link $(CCLD) $(AM_CFLAGS) $(CFLAGS) $(AM_LDFLAGS) \ + $(LDFLAGS) -o $@ SOURCES = $(libutil_la_SOURCES) DIST_SOURCES = $(libutil_la_SOURCES) ETAGS = etags @@ -211,9 +221,23 @@ AM_CXXFLAGS = -Wall -fvisibility=hidden AM_CPPFLAGS = -D__BUILDING_CVC4LIB noinst_LTLIBRARIES = libutil.la libutil_la_SOURCES = \ + Assert.h \ + Assert.cpp \ + Makefile.am \ + Makefile.in \ command.cpp \ + command.h \ + debug.h \ decision_engine.cpp \ - output.cpp + decision_engine.h \ + exception.h \ + literal.h \ + model.h \ + options.h \ + output.cpp \ + output.h \ + result.h \ + unique_id.h all: all-am @@ -267,6 +291,7 @@ mostlyclean-compile: distclean-compile: -rm -f *.tab.c +@AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/Assert.Plo@am__quote@ @AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/command.Plo@am__quote@ @AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/decision_engine.Plo@am__quote@ @AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/output.Plo@am__quote@ diff --git a/src/util/exception.h b/src/util/exception.h index 164cda8b5..d239f48de 100644 --- a/src/util/exception.h +++ b/src/util/exception.h @@ -31,7 +31,7 @@ public: Exception(const char* msg) : d_msg(msg) {} // Destructor virtual ~Exception() {} - // NON-VIRTUAL METHODs for setting and printing the error message + // NON-VIRTUAL METHOD for setting and printing the error message void setMessage(const std::string& msg) { d_msg = msg; } // Printing: feel free to redefine toString(). When inherited, // it's recommended that this method print the type of exception @@ -41,20 +41,10 @@ public: friend std::ostream& operator<<(std::ostream& os, const Exception& e); };/* class Exception */ - -class CVC4_PUBLIC IllegalArgumentException : public Exception { -public: - IllegalArgumentException() : Exception("Illegal argument to method or function") {} - IllegalArgumentException(const std::string& msg) : Exception(msg) {} - IllegalArgumentException(const char* msg) : Exception(msg) {} -};/* class IllegalArgumentException */ - - inline std::ostream& operator<<(std::ostream& os, const Exception& e) { return os << e.toString(); } - }/* CVC4 namespace */ #endif /* __CVC4__EXCEPTION_H */ diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am index acac06965..d6908cef9 100644 --- a/test/unit/Makefile.am +++ b/test/unit/Makefile.am @@ -34,4 +34,3 @@ else TESTS = no_cxxtest endif - |