summaryrefslogtreecommitdiff
path: root/src/parser
diff options
context:
space:
mode:
Diffstat (limited to 'src/parser')
-rw-r--r--src/parser/antlr_input.cpp35
-rw-r--r--src/parser/antlr_input.h2
-rw-r--r--src/parser/cvc/Cvc.g6
-rw-r--r--src/parser/input.cpp6
-rw-r--r--src/parser/input.h6
-rw-r--r--src/parser/parser.cpp3
-rw-r--r--src/parser/parser_builder.cpp11
-rw-r--r--src/parser/parser_builder.h4
-rw-r--r--src/parser/smt2/smt2.cpp13
-rw-r--r--src/parser/smt2/smt2.h4
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.
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback