diff options
Diffstat (limited to 'src/parser')
-rw-r--r-- | src/parser/antlr_input.cpp | 35 | ||||
-rw-r--r-- | src/parser/antlr_input.h | 2 | ||||
-rw-r--r-- | src/parser/cvc/Cvc.g | 6 | ||||
-rw-r--r-- | src/parser/input.cpp | 6 | ||||
-rw-r--r-- | src/parser/input.h | 6 | ||||
-rw-r--r-- | src/parser/parser.cpp | 3 | ||||
-rw-r--r-- | src/parser/parser_builder.cpp | 11 | ||||
-rw-r--r-- | src/parser/parser_builder.h | 4 | ||||
-rw-r--r-- | src/parser/smt2/smt2.cpp | 13 | ||||
-rw-r--r-- | src/parser/smt2/smt2.h | 4 |
10 files changed, 40 insertions, 50 deletions
diff --git a/src/parser/antlr_input.cpp b/src/parser/antlr_input.cpp index 73d1b89b5..6d5cbb5cc 100644 --- a/src/parser/antlr_input.cpp +++ b/src/parser/antlr_input.cpp @@ -185,35 +185,32 @@ AntlrInputStream::newStringInputStream(const std::string& input, return new AntlrInputStream(name, inputStream, false, input_duplicate, NULL); } -AntlrInput* AntlrInput::newInput(InputLanguage lang, AntlrInputStream& inputStream) { - using namespace language::input; - +AntlrInput* AntlrInput::newInput(Language lang, AntlrInputStream& inputStream) +{ AntlrInput* input; switch(lang) { - case LANG_CVC: + case Language::LANG_CVC: { input = new CvcInput(inputStream); break; } - case LANG_SYGUS_V2: input = new SygusInput(inputStream); break; + case Language::LANG_SYGUS_V2: input = new SygusInput(inputStream); break; - case LANG_TPTP: - input = new TptpInput(inputStream); - break; + case Language::LANG_TPTP: input = new TptpInput(inputStream); break; - default: - if (language::isInputLang_smt2(lang)) - { - input = new Smt2Input(inputStream); - } - else - { - std::stringstream ss; - ss << "unable to detect input file format, try --lang "; - throw InputStreamException(ss.str()); - } + default: + if (language::isLangSmt2(lang)) + { + input = new Smt2Input(inputStream); + } + else + { + std::stringstream ss; + ss << "unable to detect input file format, try --lang "; + throw InputStreamException(ss.str()); + } } return input; diff --git a/src/parser/antlr_input.h b/src/parser/antlr_input.h index c74962188..52650f561 100644 --- a/src/parser/antlr_input.h +++ b/src/parser/antlr_input.h @@ -155,7 +155,7 @@ public: * @param inputStream the input stream * * */ - static AntlrInput* newInput(InputLanguage lang, AntlrInputStream& inputStream); + static AntlrInput* newInput(Language lang, AntlrInputStream& inputStream); /** Retrieve the text associated with a token. */ static std::string tokenText(pANTLR3_COMMON_TOKEN token); diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index f0cb0fc78..a01753b56 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -491,7 +491,7 @@ api::Term createPrecedenceTree(Parser* parser, api::Solver* s, api::Term e = createPrecedenceTree( parser, s, expressions, operators, 0, expressions.size() - 1); if(Debug.isOn("prec") && operators.size() > 1) { - language::SetLanguage::Scope ls(Debug("prec"), language::output::LANG_AST); + language::SetLanguage::Scope ls(Debug("prec"), Language::LANG_AST); Debug("prec") << "=> " << e << std::endl; } return e; @@ -1103,7 +1103,7 @@ declareVariables[std::unique_ptr<cvc5::Command>* cmd, cvc5::api::Sort& t, << "with type " << oldType << std::endl; if(oldType != t) { std::stringstream ss; - ss << language::SetLanguage(language::output::LANG_CVC) + ss << language::SetLanguage(Language::LANG_CVC) << "incompatible type for `" << *i << "':" << std::endl << " old type: " << oldType << std::endl << " new type: " << t << std::endl; @@ -1514,7 +1514,7 @@ letDecl } : identifier[name,CHECK_NONE,SYM_VARIABLE] EQUAL_TOK formula[e] { - Debug("parser") << language::SetLanguage(language::output::LANG_CVC) + Debug("parser") << language::SetLanguage(Language::LANG_CVC) << e.getSort() << std::endl; PARSER_STATE->defineVar(name, e); Debug("parser") << "LET[" << PARSER_STATE->scopeLevel() << "]: " diff --git a/src/parser/input.cpp b/src/parser/input.cpp index 4c88978de..9d4c65eae 100644 --- a/src/parser/input.cpp +++ b/src/parser/input.cpp @@ -51,7 +51,7 @@ InputStream *Input::getInputStream() { return d_inputStream; } -Input* Input::newFileInput(InputLanguage lang, +Input* Input::newFileInput(Language lang, const std::string& filename, bool useMmap) { @@ -60,7 +60,7 @@ Input* Input::newFileInput(InputLanguage lang, return AntlrInput::newInput(lang, *inputStream); } -Input* Input::newStreamInput(InputLanguage lang, +Input* Input::newStreamInput(Language lang, std::istream& input, const std::string& name) { @@ -69,7 +69,7 @@ Input* Input::newStreamInput(InputLanguage lang, return AntlrInput::newInput(lang, *inputStream); } -Input* Input::newStringInput(InputLanguage lang, +Input* Input::newStringInput(Language lang, const std::string& str, const std::string& name) { diff --git a/src/parser/input.h b/src/parser/input.h index 1821bc034..94bbe1d8a 100644 --- a/src/parser/input.h +++ b/src/parser/input.h @@ -100,7 +100,7 @@ class CVC5_EXPORT Input * @param filename the input filename * @param useMmap true if the parser should use memory-mapped I/O (default: false) */ - static Input* newFileInput(InputLanguage lang, + static Input* newFileInput(Language lang, const std::string& filename, bool useMmap = false); @@ -113,7 +113,7 @@ class CVC5_EXPORT Input * (false, the default, means that the entire Input might be read * before being lexed and parsed) */ - static Input* newStreamInput(InputLanguage lang, + static Input* newStreamInput(Language lang, std::istream& input, const std::string& name); @@ -123,7 +123,7 @@ class CVC5_EXPORT Input * @param input the input string * @param name the name of the stream, for use in error messages */ - static Input* newStringInput(InputLanguage lang, + static Input* newStringInput(Language lang, const std::string& input, const std::string& name); diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index eab982013..bd0f56b2d 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -899,8 +899,7 @@ std::wstring Parser::processAdHocStringEsc(const std::string& s) api::Term Parser::mkStringConstant(const std::string& s) { - if (language::isInputLang_smt2_6( - d_solver->getOptions().base.inputLanguage)) + if (language::isLangSmt2(d_solver->getOptions().base.inputLanguage)) { return d_solver->mkString(s, true); } diff --git a/src/parser/parser_builder.cpp b/src/parser/parser_builder.cpp index 816803ccc..1ac03fb83 100644 --- a/src/parser/parser_builder.cpp +++ b/src/parser/parser_builder.cpp @@ -50,7 +50,7 @@ ParserBuilder::ParserBuilder(api::Solver* solver, void ParserBuilder::init(api::Solver* solver, SymbolManager* sm) { - d_lang = language::input::LANG_AUTO; + d_lang = Language::LANG_AUTO; d_solver = solver; d_symman = sm; d_checksEnabled = true; @@ -66,14 +66,14 @@ Parser* ParserBuilder::build() Parser* parser = NULL; switch (d_lang) { - case language::input::LANG_SYGUS_V2: + case Language::LANG_SYGUS_V2: parser = new Smt2(d_solver, d_symman, d_strictMode, d_parseOnly); break; - case language::input::LANG_TPTP: + case Language::LANG_TPTP: parser = new Tptp(d_solver, d_symman, d_strictMode, d_parseOnly); break; default: - if (language::isInputLang_smt2(d_lang)) + if (language::isLangSmt2(d_lang)) { parser = new Smt2(d_solver, d_symman, d_strictMode, d_parseOnly); } @@ -108,7 +108,8 @@ ParserBuilder& ParserBuilder::withChecks(bool flag) { return *this; } -ParserBuilder& ParserBuilder::withInputLanguage(InputLanguage lang) { +ParserBuilder& ParserBuilder::withInputLanguage(Language lang) +{ d_lang = lang; return *this; } diff --git a/src/parser/parser_builder.h b/src/parser/parser_builder.h index aed3b06f1..61819a8f9 100644 --- a/src/parser/parser_builder.h +++ b/src/parser/parser_builder.h @@ -45,7 +45,7 @@ class Parser; class CVC5_EXPORT ParserBuilder { /** The input language */ - InputLanguage d_lang; + Language d_lang; /** The API Solver object. */ api::Solver* d_solver; @@ -93,7 +93,7 @@ class CVC5_EXPORT ParserBuilder * * (Default: LANG_AUTO) */ - ParserBuilder& withInputLanguage(InputLanguage lang); + ParserBuilder& withInputLanguage(Language lang); /** * Are we only parsing, or doing something with the resulting diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 2a39a6208..fe777fe27 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -711,16 +711,9 @@ api::Grammar* Smt2::mkGrammar(const std::vector<api::Term>& boundVars, return d_allocGrammars.back().get(); } -bool Smt2::sygus() const -{ - InputLanguage ilang = getLanguage(); - return ilang == language::input::LANG_SYGUS_V2; -} +bool Smt2::sygus() const { return language::isLangSygus(getLanguage()); } -bool Smt2::sygus_v2() const -{ - return getLanguage() == language::input::LANG_SYGUS_V2; -} +bool Smt2::sygus_v2() const { return getLanguage() == Language::LANG_SYGUS_V2; } void Smt2::checkThatLogicIsSet() { @@ -848,7 +841,7 @@ api::Term Smt2::mkAbstractValue(const std::string& name) return d_solver->mkAbstractValue(name.substr(1)); } -InputLanguage Smt2::getLanguage() const +Language Smt2::getLanguage() const { return d_solver->getOptions().base.inputLanguage; } diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h index c70a60e99..50b4a4efc 100644 --- a/src/parser/smt2/smt2.h +++ b/src/parser/smt2/smt2.h @@ -230,7 +230,7 @@ class Smt2 : public Parser */ bool v2_6(bool exact = false) const { - return language::isInputLang_smt2_6(getLanguage(), exact); + return language::isLangSmt2(getLanguage()); } /** Are we using a sygus language? */ bool sygus() const; @@ -415,7 +415,7 @@ class Smt2 : public Parser void addSepOperators(); - InputLanguage getLanguage() const; + Language getLanguage() const; /** * Utility function to create a conjunction of expressions. |