Parsing support for SMT LIB 2.6. Minor fixes for printing datatypes. Fix for mkGroundTerm for parametric datatypes. Minor change to run_regression to allow regressions to override input language. Minor refactoring to Cvc.g.

4 files changed, 20 insertions, 1 deletions

diff --git a/src/options/language.cpp b/src/options/language.cpp
index 665089e45..7ae9d075a 100644
--- a/src/options/language.cpp
+++ b/src/options/language.cpp
@@ -24,6 +24,7 @@ InputLanguage toInputLanguage(OutputLanguage language) {
   case output::LANG_SMTLIB_V1:
   case output::LANG_SMTLIB_V2_0:
   case output::LANG_SMTLIB_V2_5:
+  case output::LANG_SMTLIB_V2_6:
   case output::LANG_TPTP:
   case output::LANG_CVC4:
   case output::LANG_Z3STR:
@@ -45,6 +46,7 @@ OutputLanguage toOutputLanguage(InputLanguage language) {
   case input::LANG_SMTLIB_V1:
   case input::LANG_SMTLIB_V2_0:
   case input::LANG_SMTLIB_V2_5:
+  case input::LANG_SMTLIB_V2_6:
   case input::LANG_TPTP:
   case input::LANG_CVC4:
   case input::LANG_Z3STR:
@@ -85,6 +87,9 @@ OutputLanguage toOutputLanguage(std::string language) {
   } else if(language == "smtlib2.5" || language == "smt2.5" ||
             language == "LANG_SMTLIB_V2_5") {
     return output::LANG_SMTLIB_V2_5;
+  } else if(language == "smtlib2.6" || language == "smt2.6" ||
+            language == "LANG_SMTLIB_V2_6") {
+    return output::LANG_SMTLIB_V2_6;
   } else if(language == "tptp" || language == "LANG_TPTP") {
     return output::LANG_TPTP;
   } else if(language == "z3str" || language == "z3-str" ||
@@ -117,6 +122,9 @@ InputLanguage toInputLanguage(std::string language) {
   } else if(language == "smtlib2.5" || language == "smt2.5" ||
             language == "LANG_SMTLIB_V2_5") {
     return input::LANG_SMTLIB_V2_5;
+  } else if(language == "smtlib2.6" || language == "smt2.6" ||
+            language == "LANG_SMTLIB_V2_6") {
+    return input::LANG_SMTLIB_V2_6;
   } else if(language == "tptp" || language == "LANG_TPTP") {
     return input::LANG_TPTP;
   } else if(language == "z3str" || language == "z3-str" ||
diff --git a/src/options/language.h b/src/options/language.h
index 00328e4ab..6732aa6bd 100644
--- a/src/options/language.h
+++ b/src/options/language.h
@@ -49,8 +49,10 @@ enum CVC4_PUBLIC Language {
   LANG_SMTLIB_V2_0,
   /** The SMTLIB v2.5 input language */
   LANG_SMTLIB_V2_5,
+  /** The SMTLIB v2.6 input language */
+  LANG_SMTLIB_V2_6,
   /** Backward-compatibility for enumeration naming */
-  LANG_SMTLIB_V2 = LANG_SMTLIB_V2_5,
+  LANG_SMTLIB_V2 = LANG_SMTLIB_V2_6,
   /** The TPTP input language */
   LANG_TPTP,
   /** The CVC4 input language */
@@ -82,6 +84,9 @@ inline std::ostream& operator<<(std::ostream& out, Language lang) {
   case LANG_SMTLIB_V2_5:
     out << "LANG_SMTLIB_V2_5";
     break;
+  case LANG_SMTLIB_V2_6:
+    out << "LANG_SMTLIB_V2_6";
+    break;
   case LANG_TPTP:
     out << "LANG_TPTP";
     break;
@@ -123,6 +128,8 @@ enum CVC4_PUBLIC Language {
   LANG_SMTLIB_V2_0 = input::LANG_SMTLIB_V2_0,
   /** The SMTLIB v2.5 output language */
   LANG_SMTLIB_V2_5 = input::LANG_SMTLIB_V2_5,
+  /** The SMTLIB v2.6 output language */
+  LANG_SMTLIB_V2_6 = input::LANG_SMTLIB_V2_6,
   /** Backward-compatibility for enumeration naming */
   LANG_SMTLIB_V2 = input::LANG_SMTLIB_V2,
   /** The TPTP output language */
diff --git a/src/options/language.i b/src/options/language.i
index d14368ca0..427e6c608 100644
--- a/src/options/language.i
+++ b/src/options/language.i
@@ -23,6 +23,7 @@ namespace CVC4 {
 %rename(INPUT_LANG_SMTLIB_V2) CVC4::language::input::LANG_SMTLIB_V2;
 %rename(INPUT_LANG_SMTLIB_V2_0) CVC4::language::input::LANG_SMTLIB_V2_0;
 %rename(INPUT_LANG_SMTLIB_V2_5) CVC4::language::input::LANG_SMTLIB_V2_5;
+%rename(INPUT_LANG_SMTLIB_V2_6) CVC4::language::input::LANG_SMTLIB_V2_6;
 %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;
@@ -34,6 +35,7 @@ namespace CVC4 {
 %rename(OUTPUT_LANG_SMTLIB_V2) CVC4::language::output::LANG_SMTLIB_V2;
 %rename(OUTPUT_LANG_SMTLIB_V2_0) CVC4::language::output::LANG_SMTLIB_V2_0;
 %rename(OUTPUT_LANG_SMTLIB_V2_5) CVC4::language::output::LANG_SMTLIB_V2_5;
+%rename(OUTPUT_LANG_SMTLIB_V2_6) CVC4::language::output::LANG_SMTLIB_V2_6;
 %rename(OUTPUT_LANG_TPTP) CVC4::language::output::LANG_TPTP;
 %rename(OUTPUT_LANG_CVC4) CVC4::language::output::LANG_CVC4;
 %rename(OUTPUT_LANG_AST) CVC4::language::output::LANG_AST;
diff --git a/src/options/options_template.cpp b/src/options/options_template.cpp
index 694d46d31..584be1329 100644
--- a/src/options/options_template.cpp
+++ b/src/options/options_template.cpp
@@ -434,6 +434,7 @@ Languages currently supported as arguments to the -L / --lang option:\n\
   smt | smtlib | smt2 |\n\
   smt2.0 | smtlib2 | smtlib2.0   SMT-LIB format 2.0\n\
   smt2.5 | smtlib2.5             SMT-LIB format 2.5\n\
+  smt2.6 | smtlib2.6             SMT-LIB format 2.6\n\
   tptp                           TPTP format (cnf and fof)\n\
   sygus                          SyGuS format\n\
 \n\
@@ -445,6 +446,7 @@ Languages currently supported as arguments to the --output-lang option:\n\
   smt | smtlib | smt2 |\n\
   smt2.0 | smtlib2.0 | smtlib2   SMT-LIB format 2.0\n\
   smt2.5 | smtlib2.5             SMT-LIB format 2.5\n\
+  smt2.6 | smtlib2.6             SMT-LIB format 2.6\n\
   tptp                           TPTP format\n\
   z3str                          SMT-LIB 2.0 with Z3-str string constraints\n\
   ast                            internal format (simple syntax trees)\n\