Track input language in a single place (#2003)

diff --git a/src/parser/antlr_input.cpp b/src/parser/antlr_input.cpp
index 1e5d62ef8b0d667f05c1905f73772958901dfded..ddef44c09b8ebecc439d4660a7d434674b494fb3 100644 (file)
--- 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 c02c4f45200292024d84f0370279007189d5493a..bd58bff1d36a9f5f319952fdc6a0339ed46bf03b 100644 (file)
--- 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 76e4ac17edaf6005af5cd428920ef7e6dbcae19c..1f020ca56038fd60d214396c797f1f06ff34396d 100644 (file)
--- 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 cd285255f877ddc3031d91ead871f229c412d32d..9d996aa3b2c2b90eea0681ad6d7c67a4aa6f4479 100644 (file)
--- 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 d6b5af3242bd759cf38c324bb2a953bc38a20473..4b8c5284137b14d895f74a76695147774b33275a 100644 (file)
--- 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 e0769f88a20f7a92823c8953906ee9e5e3ded5ff..cdb79986437d693499a4dab943e027cecfe8c386 100644 (file)
--- 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 e9e36e78c3c3384074baf500157f0ae61b796021..09f7a5696503b2bfd18a0cf10a5595e020468b5e 100644 (file)
--- 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 b7ffe6991e8d2c3040fb08a3f134ef7dce1f73ff..e568fb36238cd612e0bbf0b661817ecf5fec9191 100644 (file)
--- 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 44187cd2da69c92384bb8633ecea4b235d5e7a51..1b99828aa5401c3ef0677528b6eb3e028d9cb738 100644 (file)
--- 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 58d78fb760a1188e4b0a09f266d2c44effc562b4..9c103f40526537dd44ca88fb7575c6fea6716f41 100644 (file)
--- 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 9a820f26dd192ca790ebaceb8d05c7605a318f1b..9976b001c1a4dd25d8f82a803409c1946000a577 100644 (file)
--- 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