summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/parser/antlr_input.cpp2
-rw-r--r--src/parser/cvc/cvc_input.h6
-rw-r--r--src/parser/input.h3
-rw-r--r--src/parser/smt1/smt1_input.h6
-rw-r--r--src/parser/smt2/Smt2.g15
-rw-r--r--src/parser/smt2/smt2.cpp13
-rw-r--r--src/parser/smt2/smt2.h12
-rw-r--r--src/parser/smt2/smt2_input.cpp9
-rw-r--r--src/parser/smt2/smt2_input.h11
-rw-r--r--src/parser/smt2/sygus_input.h6
-rw-r--r--src/parser/tptp/tptp_input.h6
11 files changed, 16 insertions, 73 deletions
diff --git a/src/parser/antlr_input.cpp b/src/parser/antlr_input.cpp
index 1e5d62ef8..ddef44c09 100644
--- a/src/parser/antlr_input.cpp
+++ b/src/parser/antlr_input.cpp
@@ -265,7 +265,7 @@ AntlrInput* AntlrInput::newInput(InputLanguage lang, AntlrInputStream& inputStre
default:
if (language::isInputLang_smt2(lang))
{
- input = new Smt2Input(inputStream, lang);
+ input = new Smt2Input(inputStream);
}
else
{
diff --git a/src/parser/cvc/cvc_input.h b/src/parser/cvc/cvc_input.h
index c02c4f452..bd58bff1d 100644
--- a/src/parser/cvc/cvc_input.h
+++ b/src/parser/cvc/cvc_input.h
@@ -50,12 +50,6 @@ class CvcInput : public AntlrInput {
/** Destructor. Frees the lexer and the parser. */
virtual ~CvcInput();
- /** Get the language that this Input is reading. */
- InputLanguage getLanguage() const override
- {
- return language::input::LANG_CVC4;
- }
-
protected:
/** Parse a command from the input. Returns <code>NULL</code> if there is
* no command there to parse.
diff --git a/src/parser/input.h b/src/parser/input.h
index 76e4ac17e..1f020ca56 100644
--- a/src/parser/input.h
+++ b/src/parser/input.h
@@ -131,9 +131,6 @@ class CVC4_PUBLIC Input {
/** Destructor. Frees the input stream and closes the input. */
virtual ~Input();
- /** Get the language that this Input is reading. */
- virtual InputLanguage getLanguage() const = 0;
-
/** Retrieve the name of the input stream */
const std::string getInputStreamName() { return getInputStream()->getName(); }
protected:
diff --git a/src/parser/smt1/smt1_input.h b/src/parser/smt1/smt1_input.h
index cd285255f..9d996aa3b 100644
--- a/src/parser/smt1/smt1_input.h
+++ b/src/parser/smt1/smt1_input.h
@@ -53,12 +53,6 @@ public:
/** Destructor. Frees the lexer and the parser. */
virtual ~Smt1Input();
- /** Get the language that this Input is reading. */
- InputLanguage getLanguage() const override
- {
- return language::input::LANG_SMTLIB_V1;
- }
-
protected:
/**
* Parse a command from the input. Returns <code>NULL</code> if
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index d6b5af324..4b8c52841 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -1128,21 +1128,6 @@ metaInfoInternal[std::unique_ptr<CVC4::Command>* cmd]
{ name = AntlrInput::tokenText($KEYWORD);
if(name == ":cvc4-logic" || name == ":cvc4_logic") {
PARSER_STATE->setLogic(sexpr.getValue());
- } else if(name == ":smt-lib-version") {
- // if we don't recognize the revision name, just keep the current mode
- if( (sexpr.isRational() && sexpr.getRationalValue() == Rational(2)) ||
- sexpr.getValue() == "2" ||
- sexpr.getValue() == "2.0" ) {
- PARSER_STATE->setLanguage(language::input::LANG_SMTLIB_V2_0);
- } else if( (sexpr.isRational() &&
- sexpr.getRationalValue() == Rational(5, 2)) ||
- sexpr.getValue() == "2.5" ) {
- PARSER_STATE->setLanguage(language::input::LANG_SMTLIB_V2_5);
- } else if( (sexpr.isRational() &&
- sexpr.getRationalValue() == Rational(13, 5)) ||
- sexpr.getValue() == "2.6" ) {
- PARSER_STATE->setLanguage(language::input::LANG_SMTLIB_V2_6);
- }
}
PARSER_STATE->setInfo(name.c_str() + 1, sexpr);
cmd->reset(new SetInfoCommand(name.c_str() + 1, sexpr));
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index e0769f88a..4e45df440 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -15,8 +15,8 @@
**/
#include "parser/smt2/smt2.h"
-
#include "expr/type.h"
+#include "options/options.h"
#include "parser/antlr_input.h"
#include "parser/parser.h"
#include "parser/smt1/smt1.h"
@@ -42,10 +42,6 @@ Smt2::Smt2(ExprManager* exprManager, Input* input, bool strictMode, bool parseOn
}
}
-void Smt2::setLanguage(InputLanguage lang) {
- ((Smt2Input*) getInput())->setLanguage(lang);
-}
-
void Smt2::addArithmeticOperators() {
Parser::addOperator(kind::PLUS);
Parser::addOperator(kind::MINUS);
@@ -130,7 +126,7 @@ void Smt2::addStringOperators() {
addOperator(kind::STRING_PREFIX, "str.prefixof" );
addOperator(kind::STRING_SUFFIX, "str.suffixof" );
// at the moment, we only use this syntax for smt2.6.1
- if (getInput()->getLanguage() == language::input::LANG_SMTLIB_V2_6_1)
+ if (getLanguage() == language::input::LANG_SMTLIB_V2_6_1)
{
addOperator(kind::STRING_ITOS, "str.from-int");
addOperator(kind::STRING_STOI, "str.to-int");
@@ -1250,5 +1246,10 @@ const void Smt2::addSygusFunSymbol( Type t, Expr synth_fun ){
preemptCommand(cattr);
}
+InputLanguage Smt2::getLanguage() const {
+ ExprManager* em = getExprManager();
+ return em->getOptions().getInputLanguage();
+}
+
}/* CVC4::parser namespace */
}/* CVC4 namespace */
diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h
index e9e36e78c..c4ebbc745 100644
--- a/src/parser/smt2/smt2.h
+++ b/src/parser/smt2/smt2.h
@@ -153,7 +153,7 @@ public:
const LogicInfo& getLogic() const { return d_logic; }
bool v2_0() const {
- return getInput()->getLanguage() == language::input::LANG_SMTLIB_V2_0;
+ return getLanguage() == language::input::LANG_SMTLIB_V2_0;
}
/**
* Are we using smtlib 2.5 or above? If exact=true, then this method returns
@@ -161,7 +161,7 @@ public:
*/
bool v2_5(bool exact = false) const
{
- return language::isInputLang_smt2_5(getInput()->getLanguage(), exact);
+ return language::isInputLang_smt2_5(getLanguage(), exact);
}
/**
* Are we using smtlib 2.6 or above? If exact=true, then this method returns
@@ -169,14 +169,12 @@ public:
*/
bool v2_6(bool exact = false) const
{
- return language::isInputLang_smt2_6(getInput()->getLanguage(), exact);
+ return language::isInputLang_smt2_6(getLanguage(), exact);
}
bool sygus() const {
- return getInput()->getLanguage() == language::input::LANG_SYGUS;
+ return getLanguage() == language::input::LANG_SYGUS;
}
- void setLanguage(InputLanguage lang);
-
void setInfo(const std::string& flag, const SExpr& sexpr);
void setOption(const std::string& flag, const SExpr& sexpr);
@@ -396,6 +394,8 @@ private:
void addFloatingPointOperators();
void addSepOperators();
+
+ InputLanguage getLanguage() const;
};/* class Smt2 */
}/* CVC4::parser namespace */
diff --git a/src/parser/smt2/smt2_input.cpp b/src/parser/smt2/smt2_input.cpp
index b7ffe6991..0fdf2c784 100644
--- a/src/parser/smt2/smt2_input.cpp
+++ b/src/parser/smt2/smt2_input.cpp
@@ -34,7 +34,7 @@ namespace CVC4 {
namespace parser {
/* Use lookahead=2 */
-Smt2Input::Smt2Input(AntlrInputStream& inputStream, InputLanguage lang) :
+Smt2Input::Smt2Input(AntlrInputStream& inputStream) :
AntlrInput(inputStream, 2) {
pANTLR3_INPUT_STREAM input = inputStream.getAntlr3InputStream();
@@ -56,8 +56,6 @@ Smt2Input::Smt2Input(AntlrInputStream& inputStream, InputLanguage lang) :
}
setAntlr3Parser(d_pSmt2Parser->pParser);
-
- setLanguage(lang);
}
Smt2Input::~Smt2Input() {
@@ -65,11 +63,6 @@ Smt2Input::~Smt2Input() {
d_pSmt2Parser->free(d_pSmt2Parser);
}
-void Smt2Input::setLanguage(InputLanguage lang) {
- CheckArgument(language::isInputLang_smt2(lang), lang);
- d_lang = lang;
-}
-
Command* Smt2Input::parseCommand() {
return d_pSmt2Parser->parseCommand(d_pSmt2Parser);
}
diff --git a/src/parser/smt2/smt2_input.h b/src/parser/smt2/smt2_input.h
index 44187cd2d..1b99828aa 100644
--- a/src/parser/smt2/smt2_input.h
+++ b/src/parser/smt2/smt2_input.h
@@ -44,9 +44,6 @@ class Smt2Input : public AntlrInput {
/** The ANTLR3 SMT2 parser for the input. */
pSmt2Parser d_pSmt2Parser;
- /** Which (variant of the) input language we're using */
- InputLanguage d_lang;
-
/**
* Initialize the class. Called from the constructors once the input
* stream is initialized.
@@ -59,17 +56,11 @@ class Smt2Input : public AntlrInput {
*
* @param inputStream the input stream to use
*/
- Smt2Input(AntlrInputStream& inputStream,
- InputLanguage lang = language::input::LANG_SMTLIB_V2_5);
+ Smt2Input(AntlrInputStream& inputStream);
/** Destructor. Frees the lexer and the parser. */
virtual ~Smt2Input();
- /** Get the language that this Input is reading. */
- InputLanguage getLanguage() const override { return d_lang; }
- /** Set the language that this Input is reading. */
- void setLanguage(InputLanguage);
-
protected:
/**
* Parse a command from the input. Returns <code>NULL</code> if
diff --git a/src/parser/smt2/sygus_input.h b/src/parser/smt2/sygus_input.h
index 58d78fb76..9c103f405 100644
--- a/src/parser/smt2/sygus_input.h
+++ b/src/parser/smt2/sygus_input.h
@@ -61,12 +61,6 @@ class SygusInput : public AntlrInput {
/** Destructor. Frees the lexer and the parser. */
virtual ~SygusInput();
- /** Get the language that this Input is reading. */
- InputLanguage getLanguage() const override
- {
- return language::input::LANG_SYGUS;
- }
-
protected:
/**
* Parse a command from the input. Returns <code>NULL</code> if
diff --git a/src/parser/tptp/tptp_input.h b/src/parser/tptp/tptp_input.h
index 9a820f26d..9976b001c 100644
--- a/src/parser/tptp/tptp_input.h
+++ b/src/parser/tptp/tptp_input.h
@@ -61,12 +61,6 @@ class TptpInput : public AntlrInput {
/** Destructor. Frees the lexer and the parser. */
virtual ~TptpInput();
- /** Get the language that this Input is reading. */
- InputLanguage getLanguage() const override
- {
- return language::input::LANG_TPTP;
- }
-
protected:
/**
* Parse a command from the input. Returns <code>NULL</code> if
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback