Initial support for string standard in smt lib 2.6 (#1848)

4 files changed, 97 insertions, 5 deletions

diff --git a/src/options/language.cpp b/src/options/language.cpp
index 86beffd6d..f76893866 100644
--- a/src/options/language.cpp
+++ b/src/options/language.cpp
@@ -19,12 +19,62 @@
 namespace CVC4 {
 namespace language {
 
+/** define the end points of smt2 languages */
+namespace input {
+Language LANG_SMTLIB_V2_END = LANG_SMTLIB_V2_6_1;
+}
+namespace output {
+Language LANG_SMTLIB_V2_END = LANG_SMTLIB_V2_6_1;
+}
+
+bool isInputLang_smt2(InputLanguage lang)
+{
+  return (lang >= input::LANG_SMTLIB_V2_0 && lang <= input::LANG_SMTLIB_V2_END)
+         || lang == input::LANG_Z3STR;
+}
+
+bool isOutputLang_smt2(OutputLanguage lang)
+{
+  return (lang >= output::LANG_SMTLIB_V2_0
+          && lang <= output::LANG_SMTLIB_V2_END)
+         || lang == output::LANG_Z3STR;
+}
+
+bool isInputLang_smt2_5(InputLanguage lang, bool exact)
+{
+  return exact ? lang == input::LANG_SMTLIB_V2_5
+               : (lang >= input::LANG_SMTLIB_V2_5
+                  && lang <= input::LANG_SMTLIB_V2_END);
+}
+
+bool isOutputLang_smt2_5(OutputLanguage lang, bool exact)
+{
+  return exact ? lang == output::LANG_SMTLIB_V2_5
+               : (lang >= output::LANG_SMTLIB_V2_5
+                  && lang <= output::LANG_SMTLIB_V2_END);
+}
+
+bool isInputLang_smt2_6(InputLanguage lang, bool exact)
+{
+  return exact ? lang == input::LANG_SMTLIB_V2_6
+               : (lang >= input::LANG_SMTLIB_V2_6
+                  && lang <= input::LANG_SMTLIB_V2_END);
+}
+
+bool isOutputLang_smt2_6(OutputLanguage lang, bool exact)
+{
+  return exact ? lang == output::LANG_SMTLIB_V2_6
+               : (lang >= output::LANG_SMTLIB_V2_6
+                  && lang <= output::LANG_SMTLIB_V2_END);
+}
+
 InputLanguage toInputLanguage(OutputLanguage language) {
   switch(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_SMTLIB_V2_6_1:
   case output::LANG_TPTP:
   case output::LANG_CVC4:
   case output::LANG_Z3STR:
@@ -47,6 +97,7 @@ OutputLanguage toOutputLanguage(InputLanguage language) {
   case input::LANG_SMTLIB_V2_0:
   case input::LANG_SMTLIB_V2_5:
   case input::LANG_SMTLIB_V2_6:
+  case input::LANG_SMTLIB_V2_6_1:
   case input::LANG_TPTP:
   case input::LANG_CVC4:
   case input::LANG_Z3STR:
@@ -90,6 +141,11 @@ OutputLanguage toOutputLanguage(std::string language) {
   } else if(language == "smtlib2.6" || language == "smt2.6" ||
             language == "LANG_SMTLIB_V2_6") {
     return output::LANG_SMTLIB_V2_6;
+  }
+  else if (language == "smtlib2.6.1" || language == "smt2.6.1"
+           || language == "LANG_SMTLIB_V2_6_1")
+  {
+    return output::LANG_SMTLIB_V2_6_1;
   } else if(language == "tptp" || language == "LANG_TPTP") {
     return output::LANG_TPTP;
   } else if(language == "z3str" || language == "z3-str" ||
@@ -125,6 +181,11 @@ InputLanguage toInputLanguage(std::string language) {
             language == "smtlib2.6" || language == "smt2.6" ||
             language == "LANG_SMTLIB_V2_6" || language == "LANG_SMTLIB_V2") {
     return input::LANG_SMTLIB_V2_6;
+  }
+  else if (language == "smtlib2.6.1" || language == "smt2.6.1"
+           || language == "LANG_SMTLIB_V2_6_1")
+  {
+    return input::LANG_SMTLIB_V2_6_1;
   } 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 f238e765d..2b2e7d5da 100644
--- a/src/options/language.h
+++ b/src/options/language.h
@@ -30,7 +30,8 @@ namespace language {
 
 namespace input {
 
-enum CVC4_PUBLIC Language {
+enum CVC4_PUBLIC Language
+{
   // SPECIAL "NON-LANGUAGE" LANGUAGES HAVE ENUM VALUE < 0
 
   /** Auto-detect the language */
@@ -53,6 +54,8 @@ enum CVC4_PUBLIC Language {
   LANG_SMTLIB_V2_6,
   /** Backward-compatibility for enumeration naming */
   LANG_SMTLIB_V2 = LANG_SMTLIB_V2_6,
+  /** The SMTLIB v2.6 input language, with support for the strings standard */
+  LANG_SMTLIB_V2_6_1,
   /** The TPTP input language */
   LANG_TPTP,
   /** The CVC4 input language */
@@ -67,7 +70,7 @@ enum CVC4_PUBLIC Language {
 
   /** LANG_MAX is > any valid InputLanguage id */
   LANG_MAX
-};/* enum Language */
+}; /* enum Language */
 
 inline std::ostream& operator<<(std::ostream& out, Language lang) CVC4_PUBLIC;
 inline std::ostream& operator<<(std::ostream& out, Language lang) {
@@ -87,6 +90,7 @@ inline std::ostream& operator<<(std::ostream& out, Language lang) {
   case LANG_SMTLIB_V2_6:
     out << "LANG_SMTLIB_V2_6";
     break;
+  case LANG_SMTLIB_V2_6_1: out << "LANG_SMTLIB_V2_6_1"; break;
   case LANG_TPTP:
     out << "LANG_TPTP";
     break;
@@ -109,7 +113,8 @@ inline std::ostream& operator<<(std::ostream& out, Language lang) {
 
 namespace output {
 
-enum CVC4_PUBLIC Language {
+enum CVC4_PUBLIC Language
+{
   // SPECIAL "NON-LANGUAGE" LANGUAGES HAVE ENUM VALUE < 0
 
   /** Match the output language to the input language */
@@ -132,6 +137,8 @@ enum CVC4_PUBLIC Language {
   LANG_SMTLIB_V2_6 = input::LANG_SMTLIB_V2_6,
   /** Backward-compatibility for enumeration naming */
   LANG_SMTLIB_V2 = input::LANG_SMTLIB_V2,
+  /** The SMTLIB v2.6 output language */
+  LANG_SMTLIB_V2_6_1 = input::LANG_SMTLIB_V2_6_1,
   /** The TPTP output language */
   LANG_TPTP = input::LANG_TPTP,
   /** The CVC4 output language */
@@ -151,7 +158,7 @@ enum CVC4_PUBLIC Language {
 
   /** LANG_MAX is > any valid OutputLanguage id */
   LANG_MAX
-};/* enum Language */
+}; /* enum Language */
 
 inline std::ostream& operator<<(std::ostream& out, Language lang) CVC4_PUBLIC;
 inline std::ostream& operator<<(std::ostream& out, Language lang) {
@@ -165,6 +172,8 @@ 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_SMTLIB_V2_6_1: out << "LANG_SMTLIB_V2_6_1"; break;
   case LANG_TPTP:
     out << "LANG_TPTP";
     break;
@@ -198,6 +207,23 @@ typedef language::output::Language OutputLanguage;
 
 namespace language {
 
+/** Is the language a variant of the smtlib version 2 language? */
+bool isInputLang_smt2(InputLanguage lang) CVC4_PUBLIC;
+bool isOutputLang_smt2(OutputLanguage lang) CVC4_PUBLIC;
+
+/**
+  * Is the language smtlib 2.5 or above? If exact=true, then this method returns
+  * false if the input language is not exactly SMT-LIB 2.6.
+  */
+bool isInputLang_smt2_5(InputLanguage lang, bool exact = false) CVC4_PUBLIC;
+bool isOutputLang_smt2_5(OutputLanguage lang, bool exact = false) CVC4_PUBLIC;
+/**
+  * Is the language smtlib 2.6 or above? If exact=true, then this method returns
+  * false if the input language is not exactly SMT-LIB 2.6.
+  */
+bool isInputLang_smt2_6(InputLanguage lang, bool exact = false) CVC4_PUBLIC;
+bool isOutputLang_smt2_6(OutputLanguage lang, bool exact = false) CVC4_PUBLIC;
+
 InputLanguage toInputLanguage(OutputLanguage language) CVC4_PUBLIC;
 OutputLanguage toOutputLanguage(InputLanguage language) CVC4_PUBLIC;
 InputLanguage toInputLanguage(std::string language) CVC4_PUBLIC;
diff --git a/src/options/language.i b/src/options/language.i
index 427e6c608..177e590f5 100644
--- a/src/options/language.i
+++ b/src/options/language.i
@@ -24,6 +24,7 @@ namespace CVC4 {
 %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_SMTLIB_V2_6_1) CVC4::language::input::LANG_SMTLIB_V2_6_1;
 %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;
@@ -36,6 +37,7 @@ namespace CVC4 {
 %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_SMTLIB_V2_6_1) CVC4::language::output::LANG_SMTLIB_V2_6_1;
 %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 917dae687..4fdd477b9 100644
--- a/src/options/options_template.cpp
+++ b/src/options/options_template.cpp
@@ -423,7 +423,8 @@ static const std::string optionsFootnote = "\n\
     sense of the option.\n\
 ";
 
-static const std::string languageDescription = "\
+static const std::string languageDescription =
+    "\
 Languages currently supported as arguments to the -L / --lang option:\n\
   auto                           attempt to automatically determine language\n\
   cvc4 | presentation | pl       CVC4 presentation language\n\
@@ -432,6 +433,7 @@ Languages currently supported as arguments to the -L / --lang option:\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\
+  smt2.6.1 | smtlib2.6.1         SMT-LIB format 2.6 with support for the strings standard\n\
   tptp                           TPTP format (cnf and fof)\n\
   sygus                          SyGuS format\n\
 \n\
@@ -444,6 +446,7 @@ Languages currently supported as arguments to the --output-lang option:\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\
+  smt2.6.1 | smtlib2.6.1         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\