Merge branch 'master' into lfscTestslfscTests

1 files changed, 6 insertions, 27 deletions

diff --git a/src/options/language.cpp b/src/options/language.cpp
index 885549b43..b00d5c102 100644
--- a/src/options/language.cpp
+++ b/src/options/language.cpp
@@ -2,9 +2,9 @@
 /*! \file language.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Morgan Deters, Andrew Reynolds, Andres Noetzli
+ **   Andrew Reynolds, Morgan Deters, Andres Noetzli
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
@@ -29,15 +29,12 @@ 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)
-         || lang == input::LANG_Z3STR;
+  return lang >= input::LANG_SMTLIB_V2_0 && lang <= input::LANG_SMTLIB_V2_END;
 }
 
 bool isOutputLang_smt2(OutputLanguage lang)
 {
-  return (lang >= output::LANG_SMTLIB_V2_0
-          && lang <= output::LANG_SMTLIB_V2_END)
-         || lang == output::LANG_Z3STR;
+  return lang >= output::LANG_SMTLIB_V2_0 && lang <= output::LANG_SMTLIB_V2_END;
 }
 
 bool isInputLang_smt2_5(InputLanguage lang, bool exact)
@@ -70,12 +67,12 @@ bool isOutputLang_smt2_6(OutputLanguage lang, bool exact)
 
 bool isInputLangSygus(InputLanguage lang)
 {
-  return lang == input::LANG_SYGUS_V1 || lang == input::LANG_SYGUS_V2;
+  return lang == input::LANG_SYGUS_V2;
 }
 
 bool isOutputLangSygus(OutputLanguage lang)
 {
-  return lang == output::LANG_SYGUS_V1 || lang == output::LANG_SYGUS_V2;
+  return lang == output::LANG_SYGUS_V2;
 }
 
 InputLanguage toInputLanguage(OutputLanguage language) {
@@ -85,8 +82,6 @@ InputLanguage toInputLanguage(OutputLanguage language) {
   case output::LANG_SMTLIB_V2_6:
   case output::LANG_TPTP:
   case output::LANG_CVC4:
-  case output::LANG_Z3STR:
-  case output::LANG_SYGUS_V1:
   case output::LANG_SYGUS_V2:
     // these entries directly correspond (by design)
     return InputLanguage(int(language));
@@ -107,8 +102,6 @@ OutputLanguage toOutputLanguage(InputLanguage language) {
   case input::LANG_SMTLIB_V2_6:
   case input::LANG_TPTP:
   case input::LANG_CVC4:
-  case input::LANG_Z3STR:
-  case input::LANG_SYGUS_V1:
   case input::LANG_SYGUS_V2:
     // these entries directly correspond (by design)
     return OutputLanguage(int(language));
@@ -152,13 +145,6 @@ OutputLanguage toOutputLanguage(std::string language) {
     return output::LANG_SMTLIB_V2_6;
   } else if(language == "tptp" || language == "LANG_TPTP") {
     return output::LANG_TPTP;
-  } else if(language == "z3str" || language == "z3-str" ||
-            language == "LANG_Z3STR") {
-    return output::LANG_Z3STR;
-  }
-  else if (language == "sygus1" || language == "LANG_SYGUS_V1")
-  {
-    return output::LANG_SYGUS_V1;
   }
   else if (language == "sygus" || language == "LANG_SYGUS"
            || language == "sygus2" || language == "LANG_SYGUS_V2")
@@ -195,13 +181,6 @@ InputLanguage toInputLanguage(std::string language) {
     return input::LANG_SMTLIB_V2_6;
   } else if(language == "tptp" || language == "LANG_TPTP") {
     return input::LANG_TPTP;
-  } else if(language == "z3str" || language == "z3-str" ||
-            language == "LANG_Z3STR") {
-    return input::LANG_Z3STR;
-  }
-  else if (language == "sygus1" || language == "LANG_SYGUS_V1")
-  {
-    return input::LANG_SYGUS_V1;
   }
   else if (language == "sygus2" || language == "LANG_SYGUS_V2")
   {