Support sygus version 2 format (#3066)

3 files changed, 27 insertions, 3 deletions

diff --git a/src/options/language.cpp b/src/options/language.cpp
index 4aefd742c..0bd1e144a 100644
--- a/src/options/language.cpp
+++ b/src/options/language.cpp
@@ -79,6 +79,7 @@ InputLanguage toInputLanguage(OutputLanguage language) {
   case output::LANG_CVC4:
   case output::LANG_Z3STR:
   case output::LANG_SYGUS:
+  case output::LANG_SYGUS_V2:
     // these entries directly correspond (by design)
     return InputLanguage(int(language));
 
@@ -103,6 +104,7 @@ OutputLanguage toOutputLanguage(InputLanguage language) {
   case input::LANG_CVC4:
   case input::LANG_Z3STR:
   case input::LANG_SYGUS:
+  case input::LANG_SYGUS_V2:
     // these entries directly correspond (by design)
     return OutputLanguage(int(language));
 
@@ -155,9 +157,17 @@ OutputLanguage toOutputLanguage(std::string language) {
     return output::LANG_Z3STR;
   } else if(language == "sygus" || language == "LANG_SYGUS") {
     return output::LANG_SYGUS;
-  } else if(language == "ast" || language == "LANG_AST") {
+  }
+  else if (language == "sygus2" || language == "LANG_SYGUS_V2")
+  {
+    return output::LANG_SYGUS_V2;
+  }
+  else if (language == "ast" || language == "LANG_AST")
+  {
     return output::LANG_AST;
-  } else if(language == "auto" || language == "LANG_AUTO") {
+  }
+  else if (language == "auto" || language == "LANG_AUTO")
+  {
     return output::LANG_AUTO;
   }
 
@@ -195,7 +205,13 @@ InputLanguage toInputLanguage(std::string language) {
     return input::LANG_Z3STR;
   } else if(language == "sygus" || language == "LANG_SYGUS") {
     return input::LANG_SYGUS;
-  } else if(language == "auto" || language == "LANG_AUTO") {
+  }
+  else if (language == "sygus2" || language == "LANG_SYGUS_V2")
+  {
+    return input::LANG_SYGUS_V2;
+  }
+  else if (language == "auto" || language == "LANG_AUTO")
+  {
     return input::LANG_AUTO;
   }
 
diff --git a/src/options/language.h b/src/options/language.h
index 4d213c305..eec5ad158 100644
--- a/src/options/language.h
+++ b/src/options/language.h
@@ -64,6 +64,8 @@ enum CVC4_PUBLIC Language
   LANG_Z3STR,
   /** The SyGuS input language */
   LANG_SYGUS,
+  /** The SyGuS input language version 2.0 */
+  LANG_SYGUS_V2,
 
   // START OUTPUT-ONLY LANGUAGES AT ENUM VALUE 10
   // THESE ARE IN PRINCIPLE NOT POSSIBLE INPUT LANGUAGES
@@ -103,6 +105,7 @@ inline std::ostream& operator<<(std::ostream& out, Language lang) {
   case LANG_SYGUS:
     out << "LANG_SYGUS";
     break;
+  case LANG_SYGUS_V2: out << "LANG_SYGUS_V2"; break;
   default:
     out << "undefined_input_language";
   }
@@ -147,6 +150,8 @@ enum CVC4_PUBLIC Language
   LANG_Z3STR = input::LANG_Z3STR,
   /** The sygus output language */
   LANG_SYGUS = input::LANG_SYGUS,
+  /** The sygus output language version 2.0 */
+  LANG_SYGUS_V2 = input::LANG_SYGUS_V2,
 
   // START OUTPUT-ONLY LANGUAGES AT ENUM VALUE 10
   // THESE ARE IN PRINCIPLE NOT POSSIBLE INPUT LANGUAGES
@@ -186,6 +191,7 @@ inline std::ostream& operator<<(std::ostream& out, Language lang) {
   case LANG_SYGUS:
     out << "LANG_SYGUS";
     break;
+  case LANG_SYGUS_V2: out << "LANG_SYGUS_V2"; break;
   case LANG_AST:
     out << "LANG_AST";
     break;
diff --git a/src/options/language.i b/src/options/language.i
index 177e590f5..59c204400 100644
--- a/src/options/language.i
+++ b/src/options/language.i
@@ -30,6 +30,7 @@ namespace 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_V2) CVC4::language::input::LANG_SYGUS_V2;
 
 %rename(OUTPUT_LANG_AUTO) CVC4::language::output::LANG_AUTO;
 %rename(OUTPUT_LANG_SMTLIB_V1) CVC4::language::output::LANG_SMTLIB_V1;
@@ -44,5 +45,6 @@ namespace CVC4 {
 %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_V2) CVC4::language::output::LANG_SYGUS_V2;
 
 %include "options/language.h"