From 801b0332f890e96bd007cc24d0d6f3bd3a6a1359 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Mon, 28 May 2018 22:04:28 -0700 Subject: Track input language in a single place Currently, we store and update the input language in two places: the Input object and the options. The language stored in the Input object was only really used for SMT2 inputs. Storing the input language in two places means that we have to update the language in two places, which duplicates code (e.g. [0] and [1]). This removes the duplicate code and changes the code to track the input language in the options only. This commit is preparation for fixing #1969. [0] https://github.com/CVC4/CVC4/blob/74c1ad7e4a8e93316b7555ac8a1b88ee777335e2/src/smt/smt_engine.cpp#L2359-L2381 [1] https://github.com/CVC4/CVC4/blob/74c1ad7e4a8e93316b7555ac8a1b88ee777335e2/src/parser/smt2/Smt2.g#L1131-L1146 --- 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 | 13 +++++++------ src/parser/smt2/smt2.h | 12 ++++++------ src/parser/smt2/smt2_input.cpp | 9 +-------- src/parser/smt2/smt2_input.h | 11 +---------- src/parser/smt2/sygus_input.h | 6 ------ src/parser/tptp/tptp_input.h | 6 ------ 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 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..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 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