From 6059866b361d0852d0b70d484b0cb397f3cc5bf4 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Tue, 29 May 2018 05:43:20 -0700 Subject: Track input language in a single place (#2003) --- src/parser/antlr_input.cpp | 2 +- src/parser/cvc/cvc_input.h | 6 ------ src/parser/input.h | 3 --- src/parser/smt1/smt1_input.h | 6 ------ src/parser/smt2/Smt2.g | 15 --------------- src/parser/smt2/smt2.cpp | 14 ++++++++------ src/parser/smt2/smt2.h | 14 ++++++-------- src/parser/smt2/smt2_input.cpp | 12 ++---------- src/parser/smt2/smt2_input.h | 11 +---------- src/parser/smt2/sygus_input.h | 6 ------ src/parser/tptp/tptp_input.h | 6 ------ 11 files changed, 18 insertions(+), 77 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 NULL 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 NULL 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* 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..cdb799864 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,11 @@ 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..09f7a5696 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,13 +169,9 @@ 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; - } - - void setLanguage(InputLanguage lang); + bool sygus() const { return getLanguage() == language::input::LANG_SYGUS; } void setInfo(const std::string& flag, const SExpr& sexpr); @@ -396,6 +392,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..e568fb362 100644 --- a/src/parser/smt2/smt2_input.cpp +++ b/src/parser/smt2/smt2_input.cpp @@ -34,9 +34,8 @@ namespace CVC4 { namespace parser { /* Use lookahead=2 */ -Smt2Input::Smt2Input(AntlrInputStream& inputStream, InputLanguage lang) : - AntlrInput(inputStream, 2) { - +Smt2Input::Smt2Input(AntlrInputStream& inputStream) : AntlrInput(inputStream, 2) +{ pANTLR3_INPUT_STREAM input = inputStream.getAntlr3InputStream(); assert( input != NULL ); @@ -56,8 +55,6 @@ Smt2Input::Smt2Input(AntlrInputStream& inputStream, InputLanguage lang) : } setAntlr3Parser(d_pSmt2Parser->pParser); - - setLanguage(lang); } Smt2Input::~Smt2Input() { @@ -65,11 +62,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 NULL 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 NULL 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 NULL if -- cgit v1.2.3