From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 19 May 2020 19:51:19 +0000 (-0500)
Subject: Update enum and option names for sygus languages (#4388)
X-Git-Tag: cvc5-1.0.0~3318
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=02b88b7665df5a6b1a2bce231d7567efdcc4b20a;p=cvc5.git

Update enum and option names for sygus languages (#4388)

This ensures sygus is interpreted as sygus version 2; sygus1 must be used to specify sygus version 1.

Required for the 1.8 release.
---

diff --git a/src/options/language.cpp b/src/options/language.cpp
index 52263567b..885549b43 100644
--- a/src/options/language.cpp
+++ b/src/options/language.cpp
@@ -70,12 +70,12 @@ bool isOutputLang_smt2_6(OutputLanguage lang, bool exact)
 
 bool isInputLangSygus(InputLanguage lang)
 {
-  return lang == input::LANG_SYGUS || lang == input::LANG_SYGUS_V2;
+  return lang == input::LANG_SYGUS_V1 || lang == input::LANG_SYGUS_V2;
 }
 
 bool isOutputLangSygus(OutputLanguage lang)
 {
-  return lang == output::LANG_SYGUS || lang == output::LANG_SYGUS_V2;
+  return lang == output::LANG_SYGUS_V1 || lang == output::LANG_SYGUS_V2;
 }
 
 InputLanguage toInputLanguage(OutputLanguage language) {
@@ -86,7 +86,7 @@ InputLanguage toInputLanguage(OutputLanguage language) {
   case output::LANG_TPTP:
   case output::LANG_CVC4:
   case output::LANG_Z3STR:
-  case output::LANG_SYGUS:
+  case output::LANG_SYGUS_V1:
   case output::LANG_SYGUS_V2:
     // these entries directly correspond (by design)
     return InputLanguage(int(language));
@@ -108,7 +108,7 @@ OutputLanguage toOutputLanguage(InputLanguage language) {
   case input::LANG_TPTP:
   case input::LANG_CVC4:
   case input::LANG_Z3STR:
-  case input::LANG_SYGUS:
+  case input::LANG_SYGUS_V1:
   case input::LANG_SYGUS_V2:
     // these entries directly correspond (by design)
     return OutputLanguage(int(language));
@@ -155,10 +155,13 @@ OutputLanguage toOutputLanguage(std::string language) {
   } else if(language == "z3str" || language == "z3-str" ||
             language == "LANG_Z3STR") {
     return output::LANG_Z3STR;
-  } else if(language == "sygus" || language == "LANG_SYGUS") {
-    return output::LANG_SYGUS;
   }
-  else if (language == "sygus2" || language == "LANG_SYGUS_V2")
+  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")
   {
     return output::LANG_SYGUS_V2;
   }
@@ -195,8 +198,10 @@ InputLanguage toInputLanguage(std::string language) {
   } else if(language == "z3str" || language == "z3-str" ||
             language == "LANG_Z3STR") {
     return input::LANG_Z3STR;
-  } else if(language == "sygus" || language == "LANG_SYGUS") {
-    return input::LANG_SYGUS;
+  }
+  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 7866becd3..d0bdc6e77 100644
--- a/src/options/language.h
+++ b/src/options/language.h
@@ -58,8 +58,8 @@ enum CVC4_PUBLIC Language
   LANG_CVC4,
   /** The Z3-str input language */
   LANG_Z3STR,
-  /** The SyGuS input language */
-  LANG_SYGUS,
+  /** The SyGuS input language version 1.0 */
+  LANG_SYGUS_V1,
   /** The SyGuS input language version 2.0 */
   LANG_SYGUS_V2,
 
@@ -94,9 +94,7 @@ inline std::ostream& operator<<(std::ostream& out, Language lang) {
   case LANG_Z3STR:
     out << "LANG_Z3STR";
     break;
-  case LANG_SYGUS:
-    out << "LANG_SYGUS";
-    break;
+  case LANG_SYGUS_V1: out << "LANG_SYGUS_V1"; break;
   case LANG_SYGUS_V2: out << "LANG_SYGUS_V2"; break;
   default:
     out << "undefined_input_language";
@@ -136,8 +134,8 @@ enum CVC4_PUBLIC Language
   LANG_CVC4 = input::LANG_CVC4,
   /** The Z3-str output language */
   LANG_Z3STR = input::LANG_Z3STR,
-  /** The sygus output language */
-  LANG_SYGUS = input::LANG_SYGUS,
+  /** 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,
 
@@ -172,9 +170,7 @@ inline std::ostream& operator<<(std::ostream& out, Language lang) {
   case LANG_Z3STR:
     out << "LANG_Z3STR";
     break;
-  case LANG_SYGUS:
-    out << "LANG_SYGUS";
-    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 acda19aec..639cb0bda 100644
--- a/src/options/language.i
+++ b/src/options/language.i
@@ -27,7 +27,7 @@ namespace CVC4 {
 %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) CVC4::language::input::LANG_SYGUS;
+%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;
@@ -40,7 +40,7 @@ namespace 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) CVC4::language::output::LANG_SYGUS;
+%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 fe742adfc..a6489fcc4 100644
--- a/src/options/options_template.cpp
+++ b/src/options/options_template.cpp
@@ -418,7 +418,8 @@ 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\
-  sygus | sygus2                 SyGuS version 1.0 and 2.0 formats\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\
   auto                           match output language to input language\n\
diff --git a/src/parser/antlr_input.cpp b/src/parser/antlr_input.cpp
index 3157ab6e5..6dc26d439 100644
--- a/src/parser/antlr_input.cpp
+++ b/src/parser/antlr_input.cpp
@@ -247,7 +247,7 @@ AntlrInput* AntlrInput::newInput(InputLanguage lang, AntlrInputStream& inputStre
     break;
   }
 
-  case LANG_SYGUS:
+  case LANG_SYGUS_V1:
   case LANG_SYGUS_V2: input = new SygusInput(inputStream); break;
 
   case LANG_TPTP:
diff --git a/src/parser/parser_builder.cpp b/src/parser/parser_builder.cpp
index 28a965278..651dd560c 100644
--- a/src/parser/parser_builder.cpp
+++ b/src/parser/parser_builder.cpp
@@ -89,7 +89,7 @@ Parser* ParserBuilder::build()
   Parser* parser = NULL;
   switch (d_lang)
   {
-    case language::input::LANG_SYGUS:
+    case language::input::LANG_SYGUS_V1:
     case language::input::LANG_SYGUS_V2:
       parser = new Smt2(d_solver, input, d_strictMode, d_parseOnly);
       break;
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 3c30f5c49..437f5aa2f 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -743,13 +743,13 @@ Command* Smt2::setLogic(std::string name, bool fromCommand)
 bool Smt2::sygus() const
 {
   InputLanguage ilang = getLanguage();
-  return ilang == language::input::LANG_SYGUS
+  return ilang == language::input::LANG_SYGUS_V1
          || ilang == language::input::LANG_SYGUS_V2;
 }
 
 bool Smt2::sygus_v1() const
 {
-  return getLanguage() == language::input::LANG_SYGUS;
+  return getLanguage() == language::input::LANG_SYGUS_V1;
 }
 
 bool Smt2::sygus_v2() const
diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp
index 085a32c43..f8d62a8be 100644
--- a/src/printer/printer.cpp
+++ b/src/printer/printer.cpp
@@ -56,7 +56,7 @@ unique_ptr<Printer> Printer::makePrinter(OutputLanguage lang)
     return unique_ptr<Printer>(
         new printer::smt2::Smt2Printer(printer::smt2::z3str_variant));
 
-  case LANG_SYGUS:
+  case LANG_SYGUS_V1:
     return unique_ptr<Printer>(
         new printer::smt2::Smt2Printer(printer::smt2::sygus_variant));
 
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index fbccd26ed..9edc73acd 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -2276,11 +2276,9 @@ static OutputLanguage variantToLanguage(Variant variant)
     return language::output::LANG_SMTLIB_V2_0;
   case z3str_variant:
     return language::output::LANG_Z3STR;
-  case sygus_variant:
-    return language::output::LANG_SYGUS;
+  case sygus_variant: return language::output::LANG_SYGUS_V1;
   case no_variant:
-  default:
-    return language::output::LANG_SMTLIB_V2_5;
+  default: return language::output::LANG_SMTLIB_V2_6;
   }
 }
 
diff --git a/src/util/result.cpp b/src/util/result.cpp
index 916e16b4f..01d5b052e 100644
--- a/src/util/result.cpp
+++ b/src/util/result.cpp
@@ -374,7 +374,7 @@ void Result::toStreamTptp(std::ostream& out) const {
 
 void Result::toStream(std::ostream& out, OutputLanguage language) const {
   switch (language) {
-    case language::output::LANG_SYGUS:
+    case language::output::LANG_SYGUS_V1:
     case language::output::LANG_SYGUS_V2: toStreamSmt2(out); break;
     case language::output::LANG_TPTP:
       toStreamTptp(out);
diff --git a/src/util/sexpr.cpp b/src/util/sexpr.cpp
index b2dcbbc8e..24ec700bc 100644
--- a/src/util/sexpr.cpp
+++ b/src/util/sexpr.cpp
@@ -272,7 +272,7 @@ void SExpr::toStreamRec(std::ostream& out, const SExpr& sexpr,
 
 bool SExpr::languageQuotesKeywords(OutputLanguage language) {
   switch (language) {
-    case language::output::LANG_SYGUS:
+    case language::output::LANG_SYGUS_V1:
     case language::output::LANG_TPTP:
       return true;
     case language::output::LANG_AST: