Remove SMT-LIB 2.5 and 2.0 support. (#6068)

This commit removes parser and printer support for old SMT-LIB standards and also converts all regression tests to 2.6.

4 files changed, 9 insertions, 73 deletions

diff --git a/src/options/language.cpp b/src/options/language.cpp
index ee6da3e48..a7f74067f 100644
--- a/src/options/language.cpp
+++ b/src/options/language.cpp
@@ -26,34 +26,24 @@ namespace language {
 
 /** define the end points of smt2 languages */
 namespace input {
+Language LANG_SMTLIB_V2_START = LANG_SMTLIB_V2_6;
 Language LANG_SMTLIB_V2_END = LANG_SMTLIB_V2_6;
 }
 namespace output {
+Language LANG_SMTLIB_V2_START = LANG_SMTLIB_V2_6;
 Language LANG_SMTLIB_V2_END = LANG_SMTLIB_V2_6;
 }
 
 bool isInputLang_smt2(InputLanguage lang)
 {
-  return lang >= input::LANG_SMTLIB_V2_0 && lang <= input::LANG_SMTLIB_V2_END;
+  return lang >= input::LANG_SMTLIB_V2_START
+         && lang <= input::LANG_SMTLIB_V2_END;
 }
 
 bool isOutputLang_smt2(OutputLanguage lang)
 {
-  return lang >= output::LANG_SMTLIB_V2_0 && lang <= output::LANG_SMTLIB_V2_END;
-}
-
-bool isInputLang_smt2_5(InputLanguage lang, bool exact)
-{
-  return exact ? lang == input::LANG_SMTLIB_V2_5
-               : (lang >= input::LANG_SMTLIB_V2_5
-                  && lang <= input::LANG_SMTLIB_V2_END);
-}
-
-bool isOutputLang_smt2_5(OutputLanguage lang, bool exact)
-{
-  return exact ? lang == output::LANG_SMTLIB_V2_5
-               : (lang >= output::LANG_SMTLIB_V2_5
-                  && lang <= output::LANG_SMTLIB_V2_END);
+  return lang >= output::LANG_SMTLIB_V2_START
+         && lang <= output::LANG_SMTLIB_V2_END;
 }
 
 bool isInputLang_smt2_6(InputLanguage lang, bool exact)
@@ -82,8 +72,6 @@ bool isOutputLangSygus(OutputLanguage lang)
 
 InputLanguage toInputLanguage(OutputLanguage language) {
   switch(language) {
-  case output::LANG_SMTLIB_V2_0:
-  case output::LANG_SMTLIB_V2_5:
   case output::LANG_SMTLIB_V2_6:
   case output::LANG_TPTP:
   case output::LANG_CVC4:
@@ -102,8 +90,6 @@ InputLanguage toInputLanguage(OutputLanguage language) {
 
 OutputLanguage toOutputLanguage(InputLanguage language) {
   switch(language) {
-  case input::LANG_SMTLIB_V2_0:
-  case input::LANG_SMTLIB_V2_5:
   case input::LANG_SMTLIB_V2_6:
   case input::LANG_TPTP:
   case input::LANG_CVC4:
@@ -134,14 +120,6 @@ OutputLanguage toOutputLanguage(std::string language) {
   } else if(language == "cvc3" || language == "LANG_CVC3") {
     return output::LANG_CVC3;
   }
-  else if (language == "smtlib2.0" || language == "smt2.0"
-           || language == "LANG_SMTLIB_V2_0")
-  {
-    return output::LANG_SMTLIB_V2_0;
-  } else if(language == "smtlib2.5" || language == "smt2.5" ||
-            language == "LANG_SMTLIB_V2_5") {
-    return output::LANG_SMTLIB_V2_5;
-  }
   else if (language == "smtlib" || language == "smt" || language == "smtlib2"
            || language == "smt2" || language == "smtlib2.6"
            || language == "smt2.6" || language == "LANG_SMTLIB_V2_6"
@@ -173,12 +151,6 @@ InputLanguage toInputLanguage(std::string language) {
      language == "presentation" || language == "native" ||
      language == "LANG_CVC4") {
     return input::LANG_CVC4;
-  } else if(language == "smtlib2.0" || language == "smt2.0" ||
-            language == "LANG_SMTLIB_V2_0") {
-    return input::LANG_SMTLIB_V2_0;
-  } else if(language == "smtlib2.5" || language == "smt2.5" ||
-            language == "LANG_SMTLIB_V2_5") {
-    return input::LANG_SMTLIB_V2_5;
   } else if(language == "smtlib" || language == "smt" ||
             language == "smtlib2" || language == "smt2" ||
             language == "smtlib2.6" || language == "smt2.6" ||
diff --git a/src/options/language.h b/src/options/language.h
index e1e4dfed3..e986dd318 100644
--- a/src/options/language.h
+++ b/src/options/language.h
@@ -41,12 +41,8 @@ enum CVC4_PUBLIC Language
   // OUTPUT LANGUAGE, IF IT IS "IN PRINCIPLE" A COMMON LANGUAGE,
   // INCLUDE IT HERE
 
-  /** The SMTLIB v2.0 input language */
-  LANG_SMTLIB_V2_0 = 0,
-  /** The SMTLIB v2.5 input language */
-  LANG_SMTLIB_V2_5,
   /** The SMTLIB v2.6 input language, with support for the strings standard */
-  LANG_SMTLIB_V2_6,
+  LANG_SMTLIB_V2_6 = 0,
   /** Backward-compatibility for enumeration naming */
   LANG_SMTLIB_V2 = LANG_SMTLIB_V2_6,
   /** The TPTP input language */
@@ -69,12 +65,6 @@ inline std::ostream& operator<<(std::ostream& out, Language lang) {
   case LANG_AUTO:
     out << "LANG_AUTO";
     break;
-  case LANG_SMTLIB_V2_0:
-    out << "LANG_SMTLIB_V2_0";
-    break;
-  case LANG_SMTLIB_V2_5:
-    out << "LANG_SMTLIB_V2_5";
-    break;
   case LANG_SMTLIB_V2_6:
     out << "LANG_SMTLIB_V2_6";
     break;
@@ -109,10 +99,6 @@ enum CVC4_PUBLIC Language
   // OUTPUT LANGUAGE, IF IT IS "IN PRINCIPLE" A COMMON LANGUAGE,
   // INCLUDE IT HERE
 
-  /** The SMTLIB v2.0 output language */
-  LANG_SMTLIB_V2_0 = input::LANG_SMTLIB_V2_0,
-  /** The SMTLIB v2.5 output language */
-  LANG_SMTLIB_V2_5 = input::LANG_SMTLIB_V2_5,
   /** The SMTLIB v2.6 output language, with support for the strings standard */
   LANG_SMTLIB_V2_6 = input::LANG_SMTLIB_V2_6,
   /** Backward-compatibility for enumeration naming */
@@ -139,12 +125,6 @@ enum CVC4_PUBLIC Language
 inline std::ostream& operator<<(std::ostream& out, Language lang) CVC4_PUBLIC;
 inline std::ostream& operator<<(std::ostream& out, Language lang) {
   switch(lang) {
-  case LANG_SMTLIB_V2_0:
-    out << "LANG_SMTLIB_V2_0";
-    break;
-  case LANG_SMTLIB_V2_5:
-    out << "LANG_SMTLIB_V2_5";
-    break;
   case LANG_SMTLIB_V2_6: out << "LANG_SMTLIB_V2_6"; break;
   case LANG_TPTP:
     out << "LANG_TPTP";
@@ -179,12 +159,6 @@ bool isInputLang_smt2(InputLanguage lang) CVC4_PUBLIC;
 bool isOutputLang_smt2(OutputLanguage lang) CVC4_PUBLIC;
 
 /**
- * Is the language smtlib 2.5 or above? If exact=true, then this method returns
- * false if the input language is not exactly SMT-LIB 2.5.
- */
-bool isInputLang_smt2_5(InputLanguage lang, bool exact = false) CVC4_PUBLIC;
-bool isOutputLang_smt2_5(OutputLanguage lang, bool exact = false) CVC4_PUBLIC;
-/**
   * Is the language smtlib 2.6 or above? If exact=true, then this method returns
   * false if the input language is not exactly SMT-LIB 2.6.
   */
diff --git a/src/options/options_template.cpp b/src/options/options_template.cpp
index af74fd31e..f6a8e9573 100644
--- a/src/options/options_template.cpp
+++ b/src/options/options_template.cpp
@@ -287,8 +287,6 @@ Languages currently supported as arguments to the -L / --lang option:\n\
   auto                           attempt to automatically determine language\n\
   cvc4 | presentation | pl       CVC4 presentation language\n\
   smt | smtlib | smt2 |\n\
-  smt2.0 | smtlib2 | smtlib2.0   SMT-LIB format 2.0\n\
-  smt2.5 | smtlib2.5             SMT-LIB format 2.5\n\
   smt2.6 | smtlib2.6             SMT-LIB format 2.6 with support for the strings standard\n\
   tptp                           TPTP format (cnf, fof and tff)\n\
   sygus | sygus2                 SyGuS version 2.0\n\
@@ -298,8 +296,6 @@ Languages currently supported as arguments to the --output-lang option:\n\
   cvc4 | presentation | pl       CVC4 presentation language\n\
   cvc3                           CVC3 presentation language\n\
   smt | smtlib | smt2 |\n\
-  smt2.0 | smtlib2.0 | smtlib2   SMT-LIB format 2.0\n\
-  smt2.5 | smtlib2.5             SMT-LIB format 2.5\n\
   smt2.6 | smtlib2.6             SMT-LIB format 2.6 with support for the strings standard\n\
   tptp                           TPTP format\n\
   ast                            internal format (simple syntax trees)\n\
diff --git a/src/options/set_language.h b/src/options/set_language.h
index a69278154..1c9a520e6 100644
--- a/src/options/set_language.h
+++ b/src/options/set_language.h
@@ -76,18 +76,12 @@ private:
   OutputLanguage d_language;
 };/* class SetLanguage */
 
-
 /**
  * Sets the output language when pretty-printing a Expr to an ostream.
- * This is used liek this:
- *
- *   // let out be an ostream, e an Expr
- *   out << language::SetLanguage(LANG_SMTLIB_V2_5) << e << endl;
- *
- * This used to be used like this:
+ * This is used like this:
  *
  *   // let out be an ostream, e an Expr
- *   out << Expr::setlanguage(LANG_SMTLIB_V2_5) << e << endl;
+ *   out << Expr::setlanguage(LANG_SMTLIB_V2_6) << e << endl;
  *
  * The setting stays permanently (until set again) with the stream.
  */