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 52263567b3d1febb2caaa1ba6c12fc44d645278f..885549b43028a14d64b52220875f46432a061c14 100644 (file)
--- 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 7866becd3707440c2fa493b864e141906684e42f..d0bdc6e77c50da111ffc861bc7301c0836848641 100644 (file)
--- 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 acda19aeca5cd01c5adafcf8c4654e7119a2d688..639cb0bda4b149b2e69db7411c69e3093e8ef8a7 100644 (file)
--- 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 fe742adfc4c590f0aabb8e4ebf0e8806c766efc2..a6489fcc40ee7e84047392ee29e34839dfa47e32 100644 (file)
--- 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 3157ab6e5aa0a241a579063f2cbc2c6a0bdd3ef9..6dc26d43969aae69e64d05c859df7058d03d18c3 100644 (file)
--- 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 28a965278ebd6f5176cf86b68867ee78d4256f4e..651dd560c130411c374ce3aebaebcd0e2ca0337a 100644 (file)
--- 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 3c30f5c49970d4270788325869af8fec06c533c4..437f5aa2f7211174cf301e8bf4fd8d1517abee1c 100644 (file)
--- 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 085a32c434eddbc117e1509676d06dd6eb094174..f8d62a8be6e31a3aebbfbf0705868989be36165f 100644 (file)
--- 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 fbccd26ed35064f43f3b2b69df6dbf9390a24c09..9edc73acd2abf9d0e1bd66dfcc357bc91c51e47d 100644 (file)
--- 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 916e16b4fc95b231e3c273ae51d5621e56c70445..01d5b052eb50f298fe42a65ae0797ae626b341c8 100644 (file)
--- 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 b2dcbbc8e4277fa4623257e9cde899b07391f4c3..24ec700bcaa9be58993fafdbd654181e96aab3b9 100644 (file)
--- 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: