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

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