From: Morgan Deters Date: Wed, 9 Dec 2009 23:14:40 +0000 (+0000) Subject: some fixes and organizational adjustments to assert code, parsers/lexers, and build... X-Git-Tag: cvc5-1.0.0~9382 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=2f121daa042c6f25a3f9ed8ece60ac5dccb11976;p=cvc5.git some fixes and organizational adjustments to assert code, parsers/lexers, and build process --- 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 .] ) 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 @@ -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 ]) + CPPFLAGS="$OLD_CPPFLAGS -I$antlr_prefix/include" + LIBS="$OLD_LIBS -L$antlr_prefix/lib -lantlr" + AC_LINK_IFELSE( + [ + #include + 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 ]) + ] + ) ] ) done - + # Return the old compile variables and pop the language. LIBS="$OLD_LIBS" CPPFLAGS="$OLD_CPPFLAGS" diff --git a/configure b/configure index 40fc494a9..61a9f64f9 100755 --- a/configure +++ b/configure @@ -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 + 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 " "$LINENO" 5 + as_fn_error "ANTLR C++ runtime not found, see " "$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/CvcLexer.g b/src/parser/cvc/CvcLexer.g deleted file mode 100644 index 8d706963f..000000000 --- a/src/parser/cvc/CvcLexer.g +++ /dev/null @@ -1,127 +0,0 @@ -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. - */ -class AntlrCvcLexer extends Lexer; - -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; -} - -tokens { - // Types - BOOLEAN = "BOOLEAN"; - // Boolean oparators - AND = "AND"; - IF = "IF"; - THEN = "THEN"; - ELSE = "ELSE"; - ELSEIF = "ELSIF"; - ENDIF = "ENDIF"; - NOT = "NOT"; - OR = "OR"; - TRUE = "TRUE"; - FALSE = "FALSE"; - XOR = "XOR"; - IMPLIES = "=>"; - IFF = "<=>"; - // Commands - ASSERT = "ASSERT"; - QUERY = "QUERY"; - CHECKSAT = "CHECKSAT"; - PRINT = "PRINT"; - EXHO = "ECHO"; - - PUSH = "PUSH"; - POP = "POP"; - POPTO = "POPTO"; -} - -/** - * Matches any letter ('a'-'z' and 'A'-'Z'). - */ -protected -ALPHA options{ paraphrase = "a letter"; } - : 'a'..'z' - | 'A'..'Z' - ; - -/** - * Matches the digits (0-9) - */ -protected -DIGIT options{ paraphrase = "a digit"; } - : '0'..'9' - ; - -/** - * Matches the ':' - */ -COLON options{ paraphrase = "a comma"; } - : ':' - ; - -/** - * Matches the ',' - */ -COMMA options{ paraphrase = "a comma"; } - : ',' - ; - -/** - * Matches an identifier from the input. An identifier is a sequence of letters, - * 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 '('"; } - : '('; - -/** - * Matches the right bracket ('('). - */ -RPAREN options { paraphrase = "a right parenthesis ')'"; } - : ')'; - -/** - * Matches and skips whitespace in the input and ignores it. - */ -WHITESPACE options { paraphrase = "whitespace"; } - : (' ' | '\t' | '\f') { $setType(antlr::Token::SKIP); } - ; - -/** - * Mathces and skips the newline symbols in the input. - */ -NEWLINE options { paraphrase = "a newline"; } - : ('\r' '\n' | '\r' | '\n') { $setType(antlr::Token::SKIP); newline(); } - ; - -/** - * Mathces the comments and ignores them - */ -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/CvcParser.g b/src/parser/cvc/CvcParser.g deleted file mode 100644 index 625f2c381..000000000 --- a/src/parser/cvc/CvcParser.g +++ /dev/null @@ -1,111 +0,0 @@ -header "post_include_hpp" { -#include "parser/antlr_parser.h" -} - -header "post_include_cpp" { -#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. - */ -class AntlrCvcParser extends Parser("AntlrParser"); -options { - genHashLines = true; // Include line number information - importVocab = CvcVocabulary; // Import the common vocabulary - defaultErrorHandler = false; // Skip the defaul error handling, just break with exceptions - k = 2; -} - -/** - * Matches a command of the input. If a declaration, it will return an empty - * command. - */ -command returns [CVC4::Command* cmd = 0] -{ - Expr f; - vector ids; -} - : ASSERT f = formula { cmd = new AssertCommand(f); } - | QUERY f = formula { cmd = new QueryCommand(f); } - | CHECKSAT f = formula { cmd = new CheckSatCommand(f); } - | CHECKSAT { cmd = new CheckSatCommand(); } - | identifierList[ids] COLON type { - newPredicates(ids); - cmd = new EmptyCommand("Declaration"); - } - | EOF - ; - -identifierList[std::vector& id_list] - : id1:IDENTIFIER { id_list.push_back(id1->getText()); } - ( - COMMA - id2:IDENTIFIER { id_list.push_back(id2->getText()); } - )* - ; - -type - : BOOLEAN - ; - -formula returns [CVC4::Expr formula] - : formula = bool_formula - ; - -bool_formula returns [CVC4::Expr formula] -{ - vector formulas; - vector kinds; - Expr f1, f2; - Kind k; -} - : f1 = primary_bool_formula { formulas.push_back(f1); } - ( k = bool_operator { kinds.push_back(k); } f2 = primary_bool_formula { formulas.push_back(f2); } )* - { - // Create the expression based on precedences - formula = createPrecedenceExpr(formulas, kinds); - } - ; - -primary_bool_formula returns [CVC4::Expr formula] - : formula = bool_atom - | NOT formula = primary_bool_formula { formula = newExpression(CVC4::NOT, formula); } - | LPAREN formula = bool_formula RPAREN - ; - -bool_operator returns [CVC4::Kind kind] - : IMPLIES { kind = CVC4::IMPLIES; } - | AND { kind = CVC4::AND; } - | OR { kind = CVC4::OR; } - | XOR { kind = CVC4::XOR; } - | IFF { kind = CVC4::IFF; } - ; - -bool_atom returns [CVC4::Expr atom] -{ - string p; -} - : p = predicate_sym {isDeclared(p, SYM_VARIABLE)}? { atom = getVariable(p); } - exception catch [antlr::SemanticException ex] { - rethrow(ex, "Undeclared variable " + p); - } - | TRUE { atom = getTrueExpr(); } - | FALSE { atom = getFalseExpr(); } - ; - -predicate_sym returns [std::string p] - : id:IDENTIFIER { p = id->getText(); } - ; - \ No newline at end of file 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/cvc_lexer.g b/src/parser/cvc/cvc_lexer.g new file mode 100644 index 000000000..8d706963f --- /dev/null +++ b/src/parser/cvc/cvc_lexer.g @@ -0,0 +1,127 @@ +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. + */ +class AntlrCvcLexer extends Lexer; + +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; +} + +tokens { + // Types + BOOLEAN = "BOOLEAN"; + // Boolean oparators + AND = "AND"; + IF = "IF"; + THEN = "THEN"; + ELSE = "ELSE"; + ELSEIF = "ELSIF"; + ENDIF = "ENDIF"; + NOT = "NOT"; + OR = "OR"; + TRUE = "TRUE"; + FALSE = "FALSE"; + XOR = "XOR"; + IMPLIES = "=>"; + IFF = "<=>"; + // Commands + ASSERT = "ASSERT"; + QUERY = "QUERY"; + CHECKSAT = "CHECKSAT"; + PRINT = "PRINT"; + EXHO = "ECHO"; + + PUSH = "PUSH"; + POP = "POP"; + POPTO = "POPTO"; +} + +/** + * Matches any letter ('a'-'z' and 'A'-'Z'). + */ +protected +ALPHA options{ paraphrase = "a letter"; } + : 'a'..'z' + | 'A'..'Z' + ; + +/** + * Matches the digits (0-9) + */ +protected +DIGIT options{ paraphrase = "a digit"; } + : '0'..'9' + ; + +/** + * Matches the ':' + */ +COLON options{ paraphrase = "a comma"; } + : ':' + ; + +/** + * Matches the ',' + */ +COMMA options{ paraphrase = "a comma"; } + : ',' + ; + +/** + * Matches an identifier from the input. An identifier is a sequence of letters, + * 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 '('"; } + : '('; + +/** + * Matches the right bracket ('('). + */ +RPAREN options { paraphrase = "a right parenthesis ')'"; } + : ')'; + +/** + * Matches and skips whitespace in the input and ignores it. + */ +WHITESPACE options { paraphrase = "whitespace"; } + : (' ' | '\t' | '\f') { $setType(antlr::Token::SKIP); } + ; + +/** + * Mathces and skips the newline symbols in the input. + */ +NEWLINE options { paraphrase = "a newline"; } + : ('\r' '\n' | '\r' | '\n') { $setType(antlr::Token::SKIP); newline(); } + ; + +/** + * Mathces the comments and ignores them + */ +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.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 +#include + +#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/cvc_parser.g b/src/parser/cvc/cvc_parser.g new file mode 100644 index 000000000..625f2c381 --- /dev/null +++ b/src/parser/cvc/cvc_parser.g @@ -0,0 +1,111 @@ +header "post_include_hpp" { +#include "parser/antlr_parser.h" +} + +header "post_include_cpp" { +#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. + */ +class AntlrCvcParser extends Parser("AntlrParser"); +options { + genHashLines = true; // Include line number information + importVocab = CvcVocabulary; // Import the common vocabulary + defaultErrorHandler = false; // Skip the defaul error handling, just break with exceptions + k = 2; +} + +/** + * Matches a command of the input. If a declaration, it will return an empty + * command. + */ +command returns [CVC4::Command* cmd = 0] +{ + Expr f; + vector ids; +} + : ASSERT f = formula { cmd = new AssertCommand(f); } + | QUERY f = formula { cmd = new QueryCommand(f); } + | CHECKSAT f = formula { cmd = new CheckSatCommand(f); } + | CHECKSAT { cmd = new CheckSatCommand(); } + | identifierList[ids] COLON type { + newPredicates(ids); + cmd = new EmptyCommand("Declaration"); + } + | EOF + ; + +identifierList[std::vector& id_list] + : id1:IDENTIFIER { id_list.push_back(id1->getText()); } + ( + COMMA + id2:IDENTIFIER { id_list.push_back(id2->getText()); } + )* + ; + +type + : BOOLEAN + ; + +formula returns [CVC4::Expr formula] + : formula = bool_formula + ; + +bool_formula returns [CVC4::Expr formula] +{ + vector formulas; + vector kinds; + Expr f1, f2; + Kind k; +} + : f1 = primary_bool_formula { formulas.push_back(f1); } + ( k = bool_operator { kinds.push_back(k); } f2 = primary_bool_formula { formulas.push_back(f2); } )* + { + // Create the expression based on precedences + formula = createPrecedenceExpr(formulas, kinds); + } + ; + +primary_bool_formula returns [CVC4::Expr formula] + : formula = bool_atom + | NOT formula = primary_bool_formula { formula = newExpression(CVC4::NOT, formula); } + | LPAREN formula = bool_formula RPAREN + ; + +bool_operator returns [CVC4::Kind kind] + : IMPLIES { kind = CVC4::IMPLIES; } + | AND { kind = CVC4::AND; } + | OR { kind = CVC4::OR; } + | XOR { kind = CVC4::XOR; } + | IFF { kind = CVC4::IFF; } + ; + +bool_atom returns [CVC4::Expr atom] +{ + string p; +} + : p = predicate_sym {isDeclared(p, SYM_VARIABLE)}? { atom = getVariable(p); } + exception catch [antlr::SemanticException ex] { + rethrow(ex, "Undeclared variable " + p); + } + | TRUE { atom = getTrueExpr(); } + | FALSE { atom = getFalseExpr(); } + ; + +predicate_sym returns [std::string p] + : id:IDENTIFIER { p = id->getText(); } + ; + \ No newline at end of file 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 +#include +#include +#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/SmtLexer.g deleted file mode 100644 index 3d9a84f06..000000000 --- a/src/parser/smt/SmtLexer.g +++ /dev/null @@ -1,152 +0,0 @@ -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. - */ -class AntlrSmtLexer extends Lexer; - -options { - exportVocab = SmtVocabulary; // 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; -} - -tokens { - // Base SMT-LIB tokens - DISTINCT = "distinct"; - ITE = "ite"; - TRUE = "true"; - FALSE = "false"; - NOT = "not"; - IMPLIES = "implies"; - IF_THEN_ELSE = "if_then_else"; - AND = "and"; - OR = "or"; - XOR = "xor"; - IFF = "iff"; - EXISTS = "exists"; - FORALL = "forall"; - LET = "let"; - FLET = "flet"; - THEORY = "theory"; - LOGIC = "logic"; - SAT = "sat"; - UNSAT = "unsat"; - UNKNOWN = "unknown"; - BENCHMARK = "benchmark"; - // The SMT attribute tokens - C_LOGIC = ":logic"; - C_ASSUMPTION = ":assumption"; - C_FORMULA = ":formula"; - C_STATUS = ":status"; - C_EXTRASORTS = ":extrasorts"; - C_EXTRAFUNS = ":extrafuns"; - C_EXTRAPREDS = ":extrapreds"; -} - -/** - * Matches any letter ('a'-'z' and 'A'-'Z'). - */ -protected -ALPHA options{ paraphrase = "a letter"; } - : 'a'..'z' - | 'A'..'Z' - ; - -/** - * Matches the digits (0-9) - */ -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. - */ -IDENTIFIER options { paraphrase = "an identifier"; testLiterals = true; } - : ALPHA (ALPHA | DIGIT | '_' | '\'' | '.')* - ; - -/** - * Matches an identifier starting with a colon. An identifier is a sequence of letters, - * digits and "_", "'", "." symbols, starting with a colon. - */ -C_IDENTIFIER options { paraphrase = "an identifier starting with a colon"; testLiterals = true; } - : ':' ALPHA (ALPHA | DIGIT | '_' | '\'' | '.')* - ; - -/** - * Matches the value of user-defined annotations or attributes. The only constraint imposed on a user-defined value is that it start with - * an open brace and end with closed brace. - */ -USER_VALUE - : '{' - ( '\n' { newline(); } - | ~('{' | '}' | '\n') - )* - '}' - ; - -/** - * Matches the question mark symbol ('?'). - */ -QUESTION_MARK options { paraphrase = "a question mark '?'"; } - : '?' - ; - -/** - * Matches the dollar sign ('$'). - */ -DOLLAR_SIGN options { paraphrase = "a dollar sign '$'"; } - : '$' - ; - -/** - * Matches the left bracket ('('). - */ -LPAREN options { paraphrase = "a left parenthesis '('"; } - : '('; - -/** - * Matches the right bracket ('('). - */ -RPAREN options { paraphrase = "a right parenthesis ')'"; } - : ')'; - -/** - * Matches and skips whitespace in the input. - */ -WHITESPACE options { paraphrase = "whitespace"; } - : (' ' | '\t' | '\f') { $setType(antlr::Token::SKIP); } - ; - -/** - * Mathces and skips the newline symbols in the input. - */ -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 a double quoted string literal. No quote-escaping is supported inside. - */ -STRING_LITERAL options { paraphrase = "a string literal"; } - : '\"' (~('\"'))* '\"' - ; - diff --git a/src/parser/smt/SmtParser.g b/src/parser/smt/SmtParser.g deleted file mode 100644 index f68d783bc..000000000 --- a/src/parser/smt/SmtParser.g +++ /dev/null @@ -1,180 +0,0 @@ -header "post_include_hpp" { -#include "parser/antlr_parser.h" -} - -header "post_include_cpp" { -#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. - */ -class AntlrSmtParser extends Parser("AntlrParser"); -options { - genHashLines = true; // Include line number information - importVocab = SmtVocabulary; // Import the common vocabulary - defaultErrorHandler = false; // Skip the defaul error handling, just break with exceptions - k = 2; -} - -/** - * Matches an attribute name from the input (:attribute_name). - */ -attribute - : C_IDENTIFIER - ; - -/** - * Matches the sort symbol, which can be an arbitrary identifier. - */ -sort_symb returns [std::string s] - : id:IDENTIFIER { s = id->getText(); } - ; - -/** - * Matches an annotation, which is an attribute name, with an optional user value. - */ -annotation - : attribute (USER_VALUE)? - ; - -/** - * Matches a predicate symbol from the input. - */ -pred_symb returns [std::string p] - : id:IDENTIFIER { p = id->getText(); } - ; - - -/** - * Matches a propositional atom from the input. - */ -prop_atom returns [CVC4::Expr atom] -{ - std::string p; -} - : p = pred_symb {isDeclared(p, SYM_VARIABLE)}? { atom = getVariable(p); } - exception catch [antlr::SemanticException ex] { - rethrow(ex, "Undeclared variable " + p); - } - | TRUE { atom = getTrueExpr(); } - | FALSE { atom = getFalseExpr(); } - ; - -/** - * Matches an annotated proposition atom which is either a propositional atom, - * or built of other atoms using a predicate symbol. Annotation can be added if - * enclosed in brackets. The prop_atom rule from the original SMT grammar is inlined - * here in order to get rid of the ugly antlr non-determinism warrnings. - */ -an_atom returns [CVC4::Expr atom] - : atom = prop_atom - ; - -/** - * Matches on of the unary Boolean conectives. - */ -connective returns [CVC4::Kind kind] - : NOT { kind = CVC4::NOT; } - | IMPLIES { kind = CVC4::IMPLIES; } - | AND { kind = CVC4::AND; } - | OR { kind = CVC4::OR; } - | XOR { kind = CVC4::XOR; } - | IFF { kind = CVC4::IFF; } - ; - -/** - * Matches an annotated formula. - */ -an_formula returns [CVC4::Expr formula] -{ - Kind kind; - vector children; -} - : formula = an_atom - | LPAREN kind = connective an_formulas[children] RPAREN { formula = newExpression(kind, children); } - ; - -an_formulas[std::vector& formulas] -{ - Expr f; -} - : ( f = an_formula { formulas.push_back(f); } )+ - ; - -/** - * Matches the declaration of a predicate symbol. - */ -pred_symb_decl -{ - string p_name; - vector p_sorts; -} - : LPAREN p_name = pred_symb sort_symbs[p_sorts] RPAREN { newPredicate(p_name, p_sorts); } - ; - -/** - * Matches a sequence of sort symbols and fills them into the given vector. - */ -sort_symbs[std::vector& sorts] -{ - std::string type; -} - : ( type = sort_symb { sorts.push_back(type); })* - ; - -/** - * Matches the status of the benchmark, one of 'sat', 'unsat' or 'unknown'. - */ -status returns [ AntlrParser::BenchmarkStatus status ] - : SAT { status = SMT_SATISFIABLE; } - | UNSAT { status = SMT_UNSATISFIABLE; } - | UNKNOWN { status = SMT_UNKNOWN; } - ; - -/** - * Matches a benchmark attribute, sucha as ':logic', ':formula', etc. - */ -bench_attribute returns [ Command* smt_command = 0] -{ - BenchmarkStatus b_status = SMT_UNKNOWN; - Expr formula; - vector sorts; -} - : C_LOGIC IDENTIFIER - | C_ASSUMPTION formula = an_formula { smt_command = new AssertCommand(formula); } - | C_FORMULA formula = an_formula { smt_command = new CheckSatCommand(formula); } - | C_STATUS b_status = status { setBenchmarkStatus(b_status); } - | C_EXTRASORTS LPAREN sort_symbs[sorts] RPAREN { addExtraSorts(sorts); } - | C_EXTRAPREDS LPAREN (pred_symb_decl)+ RPAREN - | C_NOTES STRING_LITERAL - | annotation - ; - -/** - * Returns a pointer to a command sequence command. - */ -bench_attributes returns [CVC4::CommandSequence* cmd_seq = new CommandSequence()] -{ - Command* cmd; -} - : (cmd = bench_attribute { if (cmd) cmd_seq->addCommand(cmd); } )+ - ; - -/** - * Matches the whole SMT-LIB benchmark. - */ -benchmark returns [Command* cmd] - : LPAREN BENCHMARK IDENTIFIER cmd = bench_attributes RPAREN - ; diff --git a/src/parser/smt/smt_lexer.g b/src/parser/smt/smt_lexer.g new file mode 100644 index 000000000..3d9a84f06 --- /dev/null +++ b/src/parser/smt/smt_lexer.g @@ -0,0 +1,152 @@ +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. + */ +class AntlrSmtLexer extends Lexer; + +options { + exportVocab = SmtVocabulary; // 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; +} + +tokens { + // Base SMT-LIB tokens + DISTINCT = "distinct"; + ITE = "ite"; + TRUE = "true"; + FALSE = "false"; + NOT = "not"; + IMPLIES = "implies"; + IF_THEN_ELSE = "if_then_else"; + AND = "and"; + OR = "or"; + XOR = "xor"; + IFF = "iff"; + EXISTS = "exists"; + FORALL = "forall"; + LET = "let"; + FLET = "flet"; + THEORY = "theory"; + LOGIC = "logic"; + SAT = "sat"; + UNSAT = "unsat"; + UNKNOWN = "unknown"; + BENCHMARK = "benchmark"; + // The SMT attribute tokens + C_LOGIC = ":logic"; + C_ASSUMPTION = ":assumption"; + C_FORMULA = ":formula"; + C_STATUS = ":status"; + C_EXTRASORTS = ":extrasorts"; + C_EXTRAFUNS = ":extrafuns"; + C_EXTRAPREDS = ":extrapreds"; +} + +/** + * Matches any letter ('a'-'z' and 'A'-'Z'). + */ +protected +ALPHA options{ paraphrase = "a letter"; } + : 'a'..'z' + | 'A'..'Z' + ; + +/** + * Matches the digits (0-9) + */ +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. + */ +IDENTIFIER options { paraphrase = "an identifier"; testLiterals = true; } + : ALPHA (ALPHA | DIGIT | '_' | '\'' | '.')* + ; + +/** + * Matches an identifier starting with a colon. An identifier is a sequence of letters, + * digits and "_", "'", "." symbols, starting with a colon. + */ +C_IDENTIFIER options { paraphrase = "an identifier starting with a colon"; testLiterals = true; } + : ':' ALPHA (ALPHA | DIGIT | '_' | '\'' | '.')* + ; + +/** + * Matches the value of user-defined annotations or attributes. The only constraint imposed on a user-defined value is that it start with + * an open brace and end with closed brace. + */ +USER_VALUE + : '{' + ( '\n' { newline(); } + | ~('{' | '}' | '\n') + )* + '}' + ; + +/** + * Matches the question mark symbol ('?'). + */ +QUESTION_MARK options { paraphrase = "a question mark '?'"; } + : '?' + ; + +/** + * Matches the dollar sign ('$'). + */ +DOLLAR_SIGN options { paraphrase = "a dollar sign '$'"; } + : '$' + ; + +/** + * Matches the left bracket ('('). + */ +LPAREN options { paraphrase = "a left parenthesis '('"; } + : '('; + +/** + * Matches the right bracket ('('). + */ +RPAREN options { paraphrase = "a right parenthesis ')'"; } + : ')'; + +/** + * Matches and skips whitespace in the input. + */ +WHITESPACE options { paraphrase = "whitespace"; } + : (' ' | '\t' | '\f') { $setType(antlr::Token::SKIP); } + ; + +/** + * Mathces and skips the newline symbols in the input. + */ +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 a double quoted string literal. No quote-escaping is supported inside. + */ +STRING_LITERAL options { paraphrase = "a string literal"; } + : '\"' (~('\"'))* '\"' + ; + 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 +#include + +#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/smt_parser.g b/src/parser/smt/smt_parser.g new file mode 100644 index 000000000..f68d783bc --- /dev/null +++ b/src/parser/smt/smt_parser.g @@ -0,0 +1,180 @@ +header "post_include_hpp" { +#include "parser/antlr_parser.h" +} + +header "post_include_cpp" { +#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. + */ +class AntlrSmtParser extends Parser("AntlrParser"); +options { + genHashLines = true; // Include line number information + importVocab = SmtVocabulary; // Import the common vocabulary + defaultErrorHandler = false; // Skip the defaul error handling, just break with exceptions + k = 2; +} + +/** + * Matches an attribute name from the input (:attribute_name). + */ +attribute + : C_IDENTIFIER + ; + +/** + * Matches the sort symbol, which can be an arbitrary identifier. + */ +sort_symb returns [std::string s] + : id:IDENTIFIER { s = id->getText(); } + ; + +/** + * Matches an annotation, which is an attribute name, with an optional user value. + */ +annotation + : attribute (USER_VALUE)? + ; + +/** + * Matches a predicate symbol from the input. + */ +pred_symb returns [std::string p] + : id:IDENTIFIER { p = id->getText(); } + ; + + +/** + * Matches a propositional atom from the input. + */ +prop_atom returns [CVC4::Expr atom] +{ + std::string p; +} + : p = pred_symb {isDeclared(p, SYM_VARIABLE)}? { atom = getVariable(p); } + exception catch [antlr::SemanticException ex] { + rethrow(ex, "Undeclared variable " + p); + } + | TRUE { atom = getTrueExpr(); } + | FALSE { atom = getFalseExpr(); } + ; + +/** + * Matches an annotated proposition atom which is either a propositional atom, + * or built of other atoms using a predicate symbol. Annotation can be added if + * enclosed in brackets. The prop_atom rule from the original SMT grammar is inlined + * here in order to get rid of the ugly antlr non-determinism warrnings. + */ +an_atom returns [CVC4::Expr atom] + : atom = prop_atom + ; + +/** + * Matches on of the unary Boolean conectives. + */ +connective returns [CVC4::Kind kind] + : NOT { kind = CVC4::NOT; } + | IMPLIES { kind = CVC4::IMPLIES; } + | AND { kind = CVC4::AND; } + | OR { kind = CVC4::OR; } + | XOR { kind = CVC4::XOR; } + | IFF { kind = CVC4::IFF; } + ; + +/** + * Matches an annotated formula. + */ +an_formula returns [CVC4::Expr formula] +{ + Kind kind; + vector children; +} + : formula = an_atom + | LPAREN kind = connective an_formulas[children] RPAREN { formula = newExpression(kind, children); } + ; + +an_formulas[std::vector& formulas] +{ + Expr f; +} + : ( f = an_formula { formulas.push_back(f); } )+ + ; + +/** + * Matches the declaration of a predicate symbol. + */ +pred_symb_decl +{ + string p_name; + vector p_sorts; +} + : LPAREN p_name = pred_symb sort_symbs[p_sorts] RPAREN { newPredicate(p_name, p_sorts); } + ; + +/** + * Matches a sequence of sort symbols and fills them into the given vector. + */ +sort_symbs[std::vector& sorts] +{ + std::string type; +} + : ( type = sort_symb { sorts.push_back(type); })* + ; + +/** + * Matches the status of the benchmark, one of 'sat', 'unsat' or 'unknown'. + */ +status returns [ AntlrParser::BenchmarkStatus status ] + : SAT { status = SMT_SATISFIABLE; } + | UNSAT { status = SMT_UNSATISFIABLE; } + | UNKNOWN { status = SMT_UNKNOWN; } + ; + +/** + * Matches a benchmark attribute, sucha as ':logic', ':formula', etc. + */ +bench_attribute returns [ Command* smt_command = 0] +{ + BenchmarkStatus b_status = SMT_UNKNOWN; + Expr formula; + vector sorts; +} + : C_LOGIC IDENTIFIER + | C_ASSUMPTION formula = an_formula { smt_command = new AssertCommand(formula); } + | C_FORMULA formula = an_formula { smt_command = new CheckSatCommand(formula); } + | C_STATUS b_status = status { setBenchmarkStatus(b_status); } + | C_EXTRASORTS LPAREN sort_symbs[sorts] RPAREN { addExtraSorts(sorts); } + | C_EXTRAPREDS LPAREN (pred_symb_decl)+ RPAREN + | C_NOTES STRING_LITERAL + | annotation + ; + +/** + * Returns a pointer to a command sequence command. + */ +bench_attributes returns [CVC4::CommandSequence* cmd_seq = new CommandSequence()] +{ + Command* cmd; +} + : (cmd = bench_attribute { if (cmd) cmd_seq->addCommand(cmd); } )+ + ; + +/** + * Matches the whole SMT-LIB benchmark. + */ +benchmark returns [Command* cmd] + : LPAREN BENCHMARK IDENTIFIER cmd = bench_attributes RPAREN + ; 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 +#include +#include +#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 +#include +#include +#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 +#include +#include #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 -