diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-09-27 22:04:38 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-09-27 22:04:38 +0000 |
commit | ad0a71e2782bc291ba9f808d24df2e1d8ca1b41e (patch) | |
tree | 744a9ae0f10f6dd8837d7e0dcd8bd2b25d34e481 /src/parser | |
parent | 51daaee8eb1ee55ee3323c5395a95fd121fe87a8 (diff) |
* Rename SMT parts (printer, parser) to SMT1
* Change --lang smt to mean SMT-LIBv2
* --lang smt1 now means SMT-LIBv1
* SMT-LIBv2 parser now gives helpful error if input looks like v1
* SMT-LIBv1 parser now gives helpful error if input looks like v2
* CVC presentation language parser now gives helpful error if input
looks like either SMT-LIB v1 or v2
* Other associated changes
(this commit was certified error- and warning-free by the test-and-commit script.)
Diffstat (limited to 'src/parser')
-rw-r--r-- | src/parser/Makefile.am | 6 | ||||
-rw-r--r-- | src/parser/antlr_input.cpp | 6 | ||||
-rw-r--r-- | src/parser/cvc/Cvc.g | 10 | ||||
-rw-r--r-- | src/parser/parser.cpp | 2 | ||||
-rw-r--r-- | src/parser/parser_builder.cpp | 6 | ||||
-rw-r--r-- | src/parser/smt1/Makefile (renamed from src/parser/smt/Makefile) | 0 | ||||
-rw-r--r-- | src/parser/smt1/Makefile.am (renamed from src/parser/smt/Makefile.am) | 42 | ||||
-rw-r--r-- | src/parser/smt1/Smt1.g (renamed from src/parser/smt/Smt.g) | 26 | ||||
-rw-r--r-- | src/parser/smt1/smt1.cpp (renamed from src/parser/smt/smt.cpp) | 26 | ||||
-rw-r--r-- | src/parser/smt1/smt1.h (renamed from src/parser/smt/smt.h) | 14 | ||||
-rw-r--r-- | src/parser/smt1/smt1_input.cpp (renamed from src/parser/smt/smt_input.cpp) | 36 | ||||
-rw-r--r-- | src/parser/smt1/smt1_input.h (renamed from src/parser/smt/smt_input.h) | 26 | ||||
-rw-r--r-- | src/parser/smt2/Smt2.g | 10 | ||||
-rw-r--r-- | src/parser/smt2/smt2.cpp | 78 | ||||
-rw-r--r-- | src/parser/smt2/smt2.h | 4 | ||||
-rw-r--r-- | src/parser/tptp/tptp.cpp | 1 | ||||
-rw-r--r-- | src/parser/tptp/tptp.h | 1 |
17 files changed, 159 insertions, 135 deletions
diff --git a/src/parser/Makefile.am b/src/parser/Makefile.am index 01b4e359f..6ef353752 100644 --- a/src/parser/Makefile.am +++ b/src/parser/Makefile.am @@ -17,7 +17,7 @@ AM_CPPFLAGS = \ -I@srcdir@/../include -I@srcdir@/.. -I@builddir@/.. $(ANTLR_INCLUDES) AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN) -SUBDIRS = smt smt2 cvc tptp +SUBDIRS = smt1 smt2 cvc tptp lib_LTLIBRARIES = libcvc4parser.la if HAVE_CXXTESTGEN @@ -29,14 +29,14 @@ libcvc4parser_la_LDFLAGS = $(ANTLR_LDFLAGS) \ libcvc4parser_noinst_la_LDFLAGS = $(ANTLR_LDFLAGS) libcvc4parser_la_LIBADD = \ - @builddir@/smt/libparsersmt.la \ + @builddir@/smt1/libparsersmt1.la \ @builddir@/smt2/libparsersmt2.la \ @builddir@/tptp/libparsertptp.la \ @builddir@/cvc/libparsercvc.la \ @builddir@/../lib/libreplacements.la \ -L@builddir@/.. -lcvc4 libcvc4parser_noinst_la_LIBADD = \ - @builddir@/smt/libparsersmt.la \ + @builddir@/smt1/libparsersmt1.la \ @builddir@/smt2/libparsersmt2.la \ @builddir@/tptp/libparsertptp.la \ @builddir@/cvc/libparsercvc.la \ diff --git a/src/parser/antlr_input.cpp b/src/parser/antlr_input.cpp index 5389f270f..ea593e7da 100644 --- a/src/parser/antlr_input.cpp +++ b/src/parser/antlr_input.cpp @@ -32,7 +32,7 @@ #include "expr/command.h" #include "expr/type.h" #include "parser/cvc/cvc_input.h" -#include "parser/smt/smt_input.h" +#include "parser/smt1/smt1_input.h" #include "parser/smt2/smt2_input.h" #include "parser/tptp/tptp_input.h" #include "util/output.h" @@ -194,8 +194,8 @@ AntlrInput* AntlrInput::newInput(InputLanguage lang, AntlrInputStream& inputStre input = new CvcInput(inputStream); break; } - case LANG_SMTLIB: - input = new SmtInput(inputStream); + case LANG_SMTLIB_V1: + input = new Smt1Input(inputStream); break; case LANG_SMTLIB_V2: diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index 82e27401e..4577b504c 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -561,6 +561,16 @@ parseExpr returns [CVC4::Expr expr = CVC4::Expr()] */ parseCommand returns [CVC4::Command* cmd = NULL] : c=command { $cmd = c; } + | LPAREN IDENTIFIER + { std::string s = AntlrInput::tokenText($IDENTIFIER); + if(s == "benchmark") { + PARSER_STATE->parseError("In CVC4 presentation language mode, but SMT-LIBv1 format detected. Use --lang smt1 for SMT-LIBv1 support."); + } else if(s == "set" || s == "get") { + PARSER_STATE->parseError("In CVC4 presentation language mode, but SMT-LIBv2 format detected. Use --lang smt2 for SMT-LIBv2 support."); + } else { + PARSER_STATE->parseError("A CVC4 presentation language command cannot begin with a parenthesis; expected command name."); + } + } | EOF { $cmd = NULL; } ; diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index bf7c372b7..2a64d122d 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -31,8 +31,6 @@ #include "util/output.h" #include "options/options.h" #include "util/Assert.h" -#include "parser/cvc/cvc_input.h" -#include "parser/smt/smt_input.h" using namespace std; using namespace CVC4::kind; diff --git a/src/parser/parser_builder.cpp b/src/parser/parser_builder.cpp index bd71f71e7..73c31f578 100644 --- a/src/parser/parser_builder.cpp +++ b/src/parser/parser_builder.cpp @@ -21,7 +21,7 @@ #include "parser/parser_builder.h" #include "parser/input.h" #include "parser/parser.h" -#include "smt/smt.h" +#include "smt1/smt1.h" #include "smt2/smt2.h" #include "tptp/tptp.h" @@ -86,8 +86,8 @@ Parser* ParserBuilder::build() Parser* parser = NULL; switch(d_lang) { - case language::input::LANG_SMTLIB: - parser = new Smt(d_exprManager, input, d_strictMode, d_parseOnly); + case language::input::LANG_SMTLIB_V1: + parser = new Smt1(d_exprManager, input, d_strictMode, d_parseOnly); break; case language::input::LANG_SMTLIB_V2: parser = new Smt2(d_exprManager, input, d_strictMode, d_parseOnly); diff --git a/src/parser/smt/Makefile b/src/parser/smt1/Makefile index 7e97ed357..7e97ed357 100644 --- a/src/parser/smt/Makefile +++ b/src/parser/smt1/Makefile diff --git a/src/parser/smt/Makefile.am b/src/parser/smt1/Makefile.am index ffc5397c7..34b979ef9 100644 --- a/src/parser/smt/Makefile.am +++ b/src/parser/smt1/Makefile.am @@ -12,35 +12,35 @@ ANTLR_OPTS = # hide this included makefile from automake @mk_include@ @srcdir@/../Makefile.antlr_tracing -noinst_LTLIBRARIES = libparsersmt.la +noinst_LTLIBRARIES = libparsersmt1.la ANTLR_TOKEN_STUFF = \ - generated/Smt.tokens + generated/Smt1.tokens ANTLR_LEXER_STUFF = \ - generated/SmtLexer.h \ - generated/SmtLexer.c \ + generated/Smt1Lexer.h \ + generated/Smt1Lexer.c \ $(ANTLR_TOKEN_STUFF) ANTLR_PARSER_STUFF = \ - generated/SmtParser.h \ - generated/SmtParser.c + generated/Smt1Parser.h \ + generated/Smt1Parser.c ANTLR_STUFF = \ $(ANTLR_LEXER_STUFF) \ $(ANTLR_PARSER_STUFF) -libparsersmt_la_SOURCES = \ - Smt.g \ - smt.h \ - smt.cpp \ - smt_input.h \ - smt_input.cpp \ +libparsersmt1_la_SOURCES = \ + Smt1.g \ + smt1.h \ + smt1.cpp \ + smt1_input.h \ + smt1_input.cpp \ $(ANTLR_STUFF) BUILT_SOURCES = \ - generated/Smt.tokens \ - generated/SmtLexer.h \ - generated/SmtLexer.c \ - generated/SmtParser.h \ - generated/SmtParser.c \ + generated/Smt1.tokens \ + generated/Smt1Lexer.h \ + generated/Smt1Lexer.c \ + generated/Smt1Parser.h \ + generated/Smt1Parser.c \ stamp-generated DISTCLEANFILES = $(ANTLR_STUFF) @@ -53,13 +53,13 @@ stamp-generated: $(AM_V_at)touch stamp-generated # antlr doesn't overwrite output files, it just leaves them. So we have to delete them first. -generated/SmtLexer.h: Smt.g stamp-generated +generated/Smt1Lexer.h: Smt1.g stamp-generated -$(AM_V_at)rm -f $(ANTLR_STUFF) @if test -z "$(ANTLR)"; then echo "ERROR: antlr parser generator cannot be found, cannot generate the parser" >&2; exit 1; fi - $(AM_V_GEN)$(ANTLR) $(ANTLR_OPTS) -fo "generated" "@srcdir@/Smt.g" + $(AM_V_GEN)$(ANTLR) $(ANTLR_OPTS) -fo "generated" "@srcdir@/Smt1.g" -# These don't actually depend on SmtLexer.h, but if we're doing parallel +# These don't actually depend on Smt1Lexer.h, 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) -generated/SmtLexer.c generated/SmtParser.h generated/SmtParser.c $(ANTLR_TOKEN_STUFF): generated/SmtLexer.h +generated/Smt1Lexer.c generated/Smt1Parser.h generated/Smt1Parser.c $(ANTLR_TOKEN_STUFF): generated/Smt1Lexer.h diff --git a/src/parser/smt/Smt.g b/src/parser/smt1/Smt1.g index 0298497e9..b228fb9ec 100644 --- a/src/parser/smt/Smt.g +++ b/src/parser/smt1/Smt1.g @@ -1,5 +1,5 @@ /* ******************* */ -/*! \file Smt.g +/*! \file Smt1.g ** \verbatim ** Original author: cconway ** Major contributors: dejan, mdeters @@ -16,7 +16,7 @@ ** Parser for SMT-LIB input language. **/ -grammar Smt; +grammar Smt1; options { // C output for antlr @@ -27,7 +27,7 @@ options { // Only lookahead of <= k requested (disable for LL* parsing) // Note that CVC4's BoundedTokenBuffer requires a fixed k ! - // If you change this k, change it also in smt_input.cpp ! + // If you change this k, change it also in smt1_input.cpp ! k = 2; }/* options */ @@ -75,7 +75,7 @@ namespace CVC4 { class Expr; namespace parser { - namespace smt { + namespace smt1 { /** * Just exists to provide the uintptr_t constructor that ANTLR * requires. @@ -97,7 +97,7 @@ namespace CVC4 { myType(const Type& t) : CVC4::Type(t) {} myType(const myType& t) : CVC4::Type(t) {} };/* struct myType */ - }/* CVC4::parser::smt namespace */ + }/* CVC4::parser::smt1 namespace */ }/* CVC4::parser namespace */ }/* CVC4 namespace */ @@ -110,7 +110,7 @@ namespace CVC4 { #include "expr/type.h" #include "parser/antlr_input.h" #include "parser/parser.h" -#include "parser/smt/smt.h" +#include "parser/smt1/smt1.h" #include "util/integer.h" #include "util/output.h" #include "util/rational.h" @@ -122,7 +122,7 @@ using namespace CVC4::parser; /* These need to be macros so they can refer to the PARSER macro, which will be defined * by ANTLR *after* this section. (If they were functions, PARSER would be undefined.) */ #undef PARSER_STATE -#define PARSER_STATE ((Smt*)PARSER->super) +#define PARSER_STATE ((Smt1*)PARSER->super) #undef EXPR_MANAGER #define EXPR_MANAGER PARSER_STATE->getExprManager() #undef MK_EXPR @@ -137,7 +137,7 @@ using namespace CVC4::parser; * Parses an expression. * @return the parsed expression */ -parseExpr returns [CVC4::parser::smt::myExpr expr] +parseExpr returns [CVC4::parser::smt1::myExpr expr] : annotatedFormula[expr] | EOF ; @@ -148,6 +148,14 @@ parseExpr returns [CVC4::parser::smt::myExpr expr] */ parseCommand returns [CVC4::Command* cmd = NULL] : b = benchmark { $cmd = b; } + | LPAREN_TOK c=IDENTIFIER + { std::string s = AntlrInput::tokenText($c); + if(s == "set" || s == "get") { + PARSER_STATE->parseError(std::string("In SMT-LIBv1 mode, expected keyword `benchmark', but it looks like you're writing SMT-LIBv2. Use --lang smt for SMT-LIBv2.")); + } else { + PARSER_STATE->parseError(std::string("expected keyword `benchmark', got `" + s + "'")); + } + } ; /** @@ -521,7 +529,7 @@ sortName[std::string& name, CVC4::parser::DeclarationCheck check] : identifier[name,check,SYM_SORT] ; -sortSymbol returns [CVC4::parser::smt::myType t] +sortSymbol returns [CVC4::parser::smt1::myType t] @declarations { std::string name; } diff --git a/src/parser/smt/smt.cpp b/src/parser/smt1/smt1.cpp index e554cee10..c91743226 100644 --- a/src/parser/smt/smt.cpp +++ b/src/parser/smt1/smt1.cpp @@ -1,5 +1,5 @@ /********************* */ -/*! \file smt.cpp +/*! \file smt1.cpp ** \verbatim ** Original author: cconway ** Major contributors: mdeters @@ -11,7 +11,7 @@ ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** - ** Definitions of SMT constants. + ** Definitions of SMT-LIB (v1) constants. **/ #include <ext/hash_map> @@ -22,13 +22,13 @@ namespace std { #include "expr/type.h" #include "expr/command.h" #include "parser/parser.h" -#include "parser/smt/smt.h" +#include "parser/smt1/smt1.h" namespace CVC4 { namespace parser { -std::hash_map<const std::string, Smt::Logic, CVC4::StringHashFunction> Smt::newLogicMap() { - std::hash_map<const std::string, Smt::Logic, CVC4::StringHashFunction> logicMap; +std::hash_map<const std::string, Smt1::Logic, CVC4::StringHashFunction> Smt1::newLogicMap() { + std::hash_map<const std::string, Smt1::Logic, CVC4::StringHashFunction> logicMap; logicMap["AUFLIA"] = AUFLIA; logicMap["AUFLIRA"] = AUFLIRA; logicMap["AUFNIRA"] = AUFNIRA; @@ -66,12 +66,12 @@ std::hash_map<const std::string, Smt::Logic, CVC4::StringHashFunction> Smt::newL return logicMap; } -Smt::Logic Smt::toLogic(const std::string& name) { - static std::hash_map<const std::string, Smt::Logic, CVC4::StringHashFunction> logicMap = newLogicMap(); +Smt1::Logic Smt1::toLogic(const std::string& name) { + static std::hash_map<const std::string, Smt1::Logic, CVC4::StringHashFunction> logicMap = newLogicMap(); return logicMap[name]; } -Smt::Smt(ExprManager* exprManager, Input* input, bool strictMode, bool parseOnly) : +Smt1::Smt1(ExprManager* exprManager, Input* input, bool strictMode, bool parseOnly) : Parser(exprManager,input,strictMode,parseOnly), d_logicSet(false) { @@ -87,7 +87,7 @@ Smt::Smt(ExprManager* exprManager, Input* input, bool strictMode, bool parseOnly } -void Smt::addArithmeticOperators() { +void Smt1::addArithmeticOperators() { addOperator(kind::PLUS); addOperator(kind::MINUS); addOperator(kind::UMINUS); @@ -98,7 +98,7 @@ void Smt::addArithmeticOperators() { addOperator(kind::GEQ); } -void Smt::addTheory(Theory theory) { +void Smt1::addTheory(Theory theory) { switch(theory) { case THEORY_ARRAYS: case THEORY_ARRAYS_EX: { @@ -171,11 +171,11 @@ void Smt::addTheory(Theory theory) { } } -bool Smt::logicIsSet() { +bool Smt1::logicIsSet() { return d_logicSet; } -void Smt::setLogic(const std::string& name) { +void Smt1::setLogic(const std::string& name) { d_logicSet = true; d_logic = toLogic(name); @@ -322,7 +322,7 @@ void Smt::setLogic(const std::string& name) { addTheory(THEORY_QUANTIFIERS); break; } -}/* Smt::setLogic() */ +}/* Smt1::setLogic() */ }/* CVC4::parser namespace */ }/* CVC4 namespace */ diff --git a/src/parser/smt/smt.h b/src/parser/smt1/smt1.h index 1d550cd7e..f6c99da04 100644 --- a/src/parser/smt/smt.h +++ b/src/parser/smt1/smt1.h @@ -1,5 +1,5 @@ /********************* */ -/*! \file smt.h +/*! \file smt1.h ** \verbatim ** Original author: cconway ** Major contributors: mdeters @@ -16,8 +16,8 @@ #include "cvc4parser_private.h" -#ifndef __CVC4__PARSER__SMT_H -#define __CVC4__PARSER__SMT_H +#ifndef __CVC4__PARSER__SMT1_H +#define __CVC4__PARSER__SMT1_H #include <ext/hash_map> namespace std { using namespace __gnu_cxx; } @@ -31,7 +31,7 @@ class SExpr; namespace parser { -class Smt : public Parser { +class Smt1 : public Parser { friend class ParserBuilder; public: @@ -92,7 +92,7 @@ private: Logic d_logic; protected: - Smt(ExprManager* exprManager, Input* input, bool strictMode = false, bool parseOnly = false); + Smt1(ExprManager* exprManager, Input* input, bool strictMode = false, bool parseOnly = false); public: /** @@ -117,9 +117,9 @@ private: void addArithmeticOperators(); static std::hash_map<const std::string, Logic, CVC4::StringHashFunction> newLogicMap(); -};/* class Smt */ +};/* class Smt1 */ }/* CVC4::parser namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__PARSER__SMT_H */ +#endif /* __CVC4__PARSER__SMT1_H */ diff --git a/src/parser/smt/smt_input.cpp b/src/parser/smt1/smt1_input.cpp index 85a117dd0..4987cd793 100644 --- a/src/parser/smt/smt_input.cpp +++ b/src/parser/smt1/smt1_input.cpp @@ -1,5 +1,5 @@ /********************* */ -/*! \file smt_input.cpp +/*! \file smt1_input.cpp ** \verbatim ** Original author: cconway ** Major contributors: mdeters @@ -18,55 +18,55 @@ #include <antlr3.h> -#include "parser/smt/smt_input.h" +#include "parser/smt1/smt1_input.h" #include "expr/expr_manager.h" #include "parser/input.h" #include "parser/parser.h" #include "parser/parser_exception.h" -#include "parser/smt/generated/SmtLexer.h" -#include "parser/smt/generated/SmtParser.h" +#include "parser/smt1/generated/Smt1Lexer.h" +#include "parser/smt1/generated/Smt1Parser.h" namespace CVC4 { namespace parser { /* Use lookahead=2 */ -SmtInput::SmtInput(AntlrInputStream& inputStream) : +Smt1Input::Smt1Input(AntlrInputStream& inputStream) : AntlrInput(inputStream, 2) { pANTLR3_INPUT_STREAM input = inputStream.getAntlr3InputStream(); AlwaysAssert( input != NULL ); - d_pSmtLexer = SmtLexerNew(input); - if( d_pSmtLexer == NULL ) { + d_pSmt1Lexer = Smt1LexerNew(input); + if( d_pSmt1Lexer == NULL ) { throw ParserException("Failed to create SMT lexer."); } - setAntlr3Lexer( d_pSmtLexer->pLexer ); + setAntlr3Lexer( d_pSmt1Lexer->pLexer ); pANTLR3_COMMON_TOKEN_STREAM tokenStream = getTokenStream(); AlwaysAssert( tokenStream != NULL ); - d_pSmtParser = SmtParserNew(tokenStream); - if( d_pSmtParser == NULL ) { + d_pSmt1Parser = Smt1ParserNew(tokenStream); + if( d_pSmt1Parser == NULL ) { throw ParserException("Failed to create SMT parser."); } - setAntlr3Parser(d_pSmtParser->pParser); + setAntlr3Parser(d_pSmt1Parser->pParser); } -SmtInput::~SmtInput() { - d_pSmtLexer->free(d_pSmtLexer); - d_pSmtParser->free(d_pSmtParser); +Smt1Input::~Smt1Input() { + d_pSmt1Lexer->free(d_pSmt1Lexer); + d_pSmt1Parser->free(d_pSmt1Parser); } -Command* SmtInput::parseCommand() +Command* Smt1Input::parseCommand() throw (ParserException, TypeCheckingException, AssertionException) { - return d_pSmtParser->parseCommand(d_pSmtParser); + return d_pSmt1Parser->parseCommand(d_pSmt1Parser); } -Expr SmtInput::parseExpr() +Expr Smt1Input::parseExpr() throw (ParserException, TypeCheckingException, AssertionException) { - return d_pSmtParser->parseExpr(d_pSmtParser); + return d_pSmt1Parser->parseExpr(d_pSmt1Parser); } }/* CVC4::parser namespace */ diff --git a/src/parser/smt/smt_input.h b/src/parser/smt1/smt1_input.h index b976a3b6a..77d6f4b50 100644 --- a/src/parser/smt/smt_input.h +++ b/src/parser/smt1/smt1_input.h @@ -18,14 +18,14 @@ #include "cvc4parser_private.h" -#ifndef __CVC4__PARSER__SMT_INPUT_H -#define __CVC4__PARSER__SMT_INPUT_H +#ifndef __CVC4__PARSER__SMT1_INPUT_H +#define __CVC4__PARSER__SMT1_INPUT_H #include "parser/antlr_input.h" -#include "parser/smt/generated/SmtLexer.h" -#include "parser/smt/generated/SmtParser.h" +#include "parser/smt1/generated/Smt1Lexer.h" +#include "parser/smt1/generated/Smt1Parser.h" -// extern void SmtParserSetAntlrParser(CVC4::parser::AntlrParser* newAntlrParser); +// extern void Smt1ParserSetAntlrParser(CVC4::parser::AntlrParser* newAntlrParser); namespace CVC4 { @@ -35,13 +35,13 @@ class ExprManager; namespace parser { -class SmtInput : public AntlrInput { +class Smt1Input : public AntlrInput { /** The ANTLR3 SMT lexer for the input. */ - pSmtLexer d_pSmtLexer; + pSmt1Lexer d_pSmt1Lexer; /** The ANTLR3 CVC parser for the input. */ - pSmtParser d_pSmtParser; + pSmt1Parser d_pSmt1Parser; public: @@ -50,14 +50,14 @@ public: * * @param inputStream the input stream to use */ - SmtInput(AntlrInputStream& inputStream); + Smt1Input(AntlrInputStream& inputStream); /** Destructor. Frees the lexer and the parser. */ - virtual ~SmtInput(); + virtual ~Smt1Input(); /** Get the language that this Input is reading. */ InputLanguage getLanguage() const throw() { - return language::input::LANG_SMTLIB; + return language::input::LANG_SMTLIB_V1; } protected: @@ -88,9 +88,9 @@ private: */ void init(); -};/* class SmtInput */ +};/* class Smt1Input */ }/* CVC4::parser namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__PARSER__SMT_INPUT_H */ +#endif /* __CVC4__PARSER__SMT1_INPUT_H */ diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 03aa7acc1..fb97d5d1e 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -355,6 +355,16 @@ command returns [CVC4::Command* cmd = NULL] PARSER_STATE->parseError("Extended commands are not permitted while operating in strict compliance mode."); } } + + /* error handling */ + | SIMPLE_SYMBOL + { std::string id = AntlrInput::tokenText($SIMPLE_SYMBOL); + if(id == "benchmark") { + PARSER_STATE->parseError("In SMT-LIBv2 mode, but got something that looks like SMT-LIBv1. Use --lang smt1 for SMT-LIBv1."); + } else { + PARSER_STATE->parseError("expected SMT-LIBv2 command, got `" + id + "'."); + } + } ; extendedCommand[CVC4::Command*& cmd] diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 9bdadc440..ca7697810 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -19,7 +19,7 @@ #include "expr/type.h" #include "expr/command.h" #include "parser/parser.h" -#include "parser/smt/smt.h" +#include "parser/smt1/smt1.h" #include "parser/smt2/smt2.h" namespace CVC4 { @@ -98,107 +98,107 @@ bool Smt2::logicIsSet() { void Smt2::setLogic(const std::string& name) { d_logicSet = true; - d_logic = Smt::toLogic(name); + d_logic = Smt1::toLogic(name); // Core theory belongs to every logic addTheory(THEORY_CORE); switch(d_logic) { - case Smt::QF_SAT: + case Smt1::QF_SAT: /* No extra symbols necessary */ break; - case Smt::QF_AX: + case Smt1::QF_AX: addTheory(THEORY_ARRAYS); break; - case Smt::QF_IDL: - case Smt::QF_LIA: - case Smt::QF_NIA: + case Smt1::QF_IDL: + case Smt1::QF_LIA: + case Smt1::QF_NIA: addTheory(THEORY_INTS); break; - case Smt::QF_RDL: - case Smt::QF_LRA: - case Smt::QF_NRA: + case Smt1::QF_RDL: + case Smt1::QF_LRA: + case Smt1::QF_NRA: addTheory(THEORY_REALS); break; - case Smt::QF_UF: + case Smt1::QF_UF: addOperator(kind::APPLY_UF); break; - case Smt::QF_UFIDL: - case Smt::QF_UFLIA: - case Smt::QF_UFNIA:// nonstandard logic + case Smt1::QF_UFIDL: + case Smt1::QF_UFLIA: + case Smt1::QF_UFNIA:// nonstandard logic addTheory(THEORY_INTS); addOperator(kind::APPLY_UF); break; - case Smt::QF_UFLRA: - case Smt::QF_UFNRA: + case Smt1::QF_UFLRA: + case Smt1::QF_UFNRA: addTheory(THEORY_REALS); addOperator(kind::APPLY_UF); break; - case Smt::QF_UFLIRA:// nonstandard logic - case Smt::QF_UFNIRA:// nonstandard logic + case Smt1::QF_UFLIRA:// nonstandard logic + case Smt1::QF_UFNIRA:// nonstandard logic addOperator(kind::APPLY_UF); addTheory(THEORY_INTS); addTheory(THEORY_REALS); break; - case Smt::QF_BV: + case Smt1::QF_BV: addTheory(THEORY_BITVECTORS); break; - case Smt::QF_ABV: + case Smt1::QF_ABV: addTheory(THEORY_ARRAYS); addTheory(THEORY_BITVECTORS); break; - case Smt::QF_UFBV: + case Smt1::QF_UFBV: addOperator(kind::APPLY_UF); addTheory(THEORY_BITVECTORS); break; - case Smt::QF_AUFBV: + case Smt1::QF_AUFBV: addOperator(kind::APPLY_UF); addTheory(THEORY_ARRAYS); addTheory(THEORY_BITVECTORS); break; - case Smt::QF_AUFBVLIA: + case Smt1::QF_AUFBVLIA: addOperator(kind::APPLY_UF); addTheory(THEORY_ARRAYS); addTheory(THEORY_BITVECTORS); addTheory(THEORY_INTS); break; - case Smt::QF_AUFBVLRA: + case Smt1::QF_AUFBVLRA: addOperator(kind::APPLY_UF); addTheory(THEORY_ARRAYS); addTheory(THEORY_BITVECTORS); addTheory(THEORY_REALS); break; - case Smt::QF_AUFLIA: + case Smt1::QF_AUFLIA: addTheory(THEORY_ARRAYS); addOperator(kind::APPLY_UF); addTheory(THEORY_INTS); break; - case Smt::QF_AUFLIRA: + case Smt1::QF_AUFLIRA: addTheory(THEORY_ARRAYS); addOperator(kind::APPLY_UF); addTheory(THEORY_INTS); addTheory(THEORY_REALS); break; - case Smt::ALL_SUPPORTED: + case Smt1::ALL_SUPPORTED: addTheory(THEORY_QUANTIFIERS); /* fall through */ - case Smt::QF_ALL_SUPPORTED: + case Smt1::QF_ALL_SUPPORTED: addTheory(THEORY_ARRAYS); addOperator(kind::APPLY_UF); addTheory(THEORY_INTS); @@ -206,21 +206,21 @@ void Smt2::setLogic(const std::string& name) { addTheory(THEORY_BITVECTORS); break; - case Smt::AUFLIA: - case Smt::AUFLIRA: - case Smt::AUFNIRA: - case Smt::LRA: - case Smt::UFNIA: - case Smt::UFNIRA: - case Smt::UFLRA: - if(d_logic != Smt::AUFLIA && d_logic != Smt::UFNIA) { + case Smt1::AUFLIA: + case Smt1::AUFLIRA: + case Smt1::AUFNIRA: + case Smt1::LRA: + case Smt1::UFNIA: + case Smt1::UFNIRA: + case Smt1::UFLRA: + if(d_logic != Smt1::AUFLIA && d_logic != Smt1::UFNIA) { addTheory(THEORY_REALS); } - if(d_logic != Smt::LRA) { + if(d_logic != Smt1::LRA) { addOperator(kind::APPLY_UF); - if(d_logic != Smt::UFLRA) { + if(d_logic != Smt1::UFLRA) { addTheory(THEORY_INTS); - if(d_logic != Smt::UFNIA && d_logic != Smt::UFNIRA) { + if(d_logic != Smt1::UFNIA && d_logic != Smt1::UFNIRA) { addTheory(THEORY_ARRAYS); } } diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h index 9bd85d7bc..72310b5a4 100644 --- a/src/parser/smt2/smt2.h +++ b/src/parser/smt2/smt2.h @@ -22,7 +22,7 @@ #define __CVC4__PARSER__SMT2_H #include "parser/parser.h" -#include "parser/smt/smt.h" +#include "parser/smt1/smt1.h" #include <sstream> @@ -48,7 +48,7 @@ public: private: bool d_logicSet; - Smt::Logic d_logic; + Smt1::Logic d_logic; protected: Smt2(ExprManager* exprManager, Input* input, bool strictMode = false, bool parseOnly = false); diff --git a/src/parser/tptp/tptp.cpp b/src/parser/tptp/tptp.cpp index ab7ce5422..134498eea 100644 --- a/src/parser/tptp/tptp.cpp +++ b/src/parser/tptp/tptp.cpp @@ -18,7 +18,6 @@ #include "expr/type.h" #include "parser/parser.h" -#include "parser/smt/smt.h" #include "parser/tptp/tptp.h" #include "parser/antlr_input.h" diff --git a/src/parser/tptp/tptp.h b/src/parser/tptp/tptp.h index ae4ad4e7f..9d75a1d37 100644 --- a/src/parser/tptp/tptp.h +++ b/src/parser/tptp/tptp.h @@ -22,7 +22,6 @@ #define __CVC4__PARSER__TPTP_H #include "parser/parser.h" -#include "parser/smt/smt.h" #include "expr/command.h" #include <ext/hash_set> |