Remove sygus1 parser (#4651)

We no longer support sygus v1 inputs. This PR removes support for sygus v1 (as well as a deprecated "z3str" variant of smt lib 2 which is subsumed by the new strings standard).

As mentioned in the release notes, CVC4 1.8 supports a conversion from sygus v1 to v2 script.

This removal is required for further updates to the new API. Further infrastructure (e.g. the sygus print callback) will be removed in a separate PR.

FYI @abdoo8080 .

4 files changed, 4 insertions, 47 deletions

diff --git a/src/options/language.cpp b/src/options/language.cpp
index c03ae1cbb..b00d5c102 100644
--- a/src/options/language.cpp
+++ b/src/options/language.cpp
@@ -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")
   {
diff --git a/src/options/language.h b/src/options/language.h
index 7dc1cf987..0a0f63ca6 100644
--- a/src/options/language.h
+++ b/src/options/language.h
@@ -56,10 +56,6 @@ enum CVC4_PUBLIC Language
   LANG_TPTP,
   /** The CVC4 input language */
   LANG_CVC4,
-  /** The Z3-str input language */
-  LANG_Z3STR,
-  /** The SyGuS input language version 1.0 */
-  LANG_SYGUS_V1,
   /** The SyGuS input language version 2.0 */
   LANG_SYGUS_V2,
 
@@ -91,10 +87,6 @@ inline std::ostream& operator<<(std::ostream& out, Language lang) {
   case LANG_CVC4:
     out << "LANG_CVC4";
     break;
-  case LANG_Z3STR:
-    out << "LANG_Z3STR";
-    break;
-  case LANG_SYGUS_V1: out << "LANG_SYGUS_V1"; break;
   case LANG_SYGUS_V2: out << "LANG_SYGUS_V2"; break;
   default:
     out << "undefined_input_language";
@@ -132,10 +124,6 @@ enum CVC4_PUBLIC Language
   LANG_TPTP = input::LANG_TPTP,
   /** The CVC4 output language */
   LANG_CVC4 = input::LANG_CVC4,
-  /** The Z3-str output language */
-  LANG_Z3STR = input::LANG_Z3STR,
-  /** The sygus output language version 1.0 */
-  LANG_SYGUS_V1 = input::LANG_SYGUS_V1,
   /** The sygus output language version 2.0 */
   LANG_SYGUS_V2 = input::LANG_SYGUS_V2,
 
@@ -167,10 +155,6 @@ inline std::ostream& operator<<(std::ostream& out, Language lang) {
   case LANG_CVC4:
     out << "LANG_CVC4";
     break;
-  case LANG_Z3STR:
-    out << "LANG_Z3STR";
-    break;
-  case LANG_SYGUS_V1: out << "LANG_SYGUS_V1"; break;
   case LANG_SYGUS_V2: out << "LANG_SYGUS_V2"; break;
   case LANG_AST:
     out << "LANG_AST";
diff --git a/src/options/language.i b/src/options/language.i
index 639cb0bda..7f81ea7c6 100644
--- a/src/options/language.i
+++ b/src/options/language.i
@@ -26,8 +26,6 @@ namespace CVC4 {
 %rename(INPUT_LANG_TPTP) CVC4::language::input::LANG_TPTP;
 %rename(INPUT_LANG_CVC4) CVC4::language::input::LANG_CVC4;
 %rename(INPUT_LANG_MAX) CVC4::language::input::LANG_MAX;
-%rename(INPUT_LANG_Z3STR) CVC4::language::input::LANG_Z3STR;
-%rename(INPUT_LANG_SYGUS_V1) CVC4::language::input::LANG_SYGUS_V1;
 %rename(INPUT_LANG_SYGUS_V2) CVC4::language::input::LANG_SYGUS_V2;
 
 %rename(OUTPUT_LANG_AUTO) CVC4::language::output::LANG_AUTO;
@@ -39,8 +37,6 @@ namespace CVC4 {
 %rename(OUTPUT_LANG_CVC4) CVC4::language::output::LANG_CVC4;
 %rename(OUTPUT_LANG_AST) CVC4::language::output::LANG_AST;
 %rename(OUTPUT_LANG_MAX) CVC4::language::output::LANG_MAX;
-%rename(OUTPUT_LANG_Z3STR) CVC4::language::output::LANG_Z3STR;
-%rename(OUTPUT_LANG_SYGUS_V1) CVC4::language::output::LANG_SYGUS_V1;
 %rename(OUTPUT_LANG_SYGUS_V2) CVC4::language::output::LANG_SYGUS_V2;
 
 %include "options/language.h"
diff --git a/src/options/options_template.cpp b/src/options/options_template.cpp
index a49ede98e..234ddd5b4 100644
--- a/src/options/options_template.cpp
+++ b/src/options/options_template.cpp
@@ -418,7 +418,6 @@ Languages currently supported as arguments to the -L / --lang option:\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\
-  sygus1                         SyGuS version 1.0 \n\
   sygus | sygus2                 SyGuS version 2.0\n\
 \n\
 Languages currently supported as arguments to the --output-lang option:\n\
@@ -430,7 +429,6 @@ Languages currently supported as arguments to the --output-lang option:\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\
-  z3str                          SMT-LIB 2.0 with Z3-str string constraints\n\
   ast                            internal format (simple syntax trees)\n\
 ";