From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Tue, 29 May 2018 12:43:20 +0000 (-0700)
Subject: Track input language in a single place (#2003)
X-Git-Tag: cvc5-1.0.0~5001
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=6059866b361d0852d0b70d484b0cb397f3cc5bf4;p=cvc5.git

Track input language in a single place (#2003)
---

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..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 <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