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

diff --git a/src/main/interactive_shell.cpp b/src/main/interactive_shell.cpp
index 4761ba07e2eee40dcd3220f1c526c9884d562eb1..e58c5319add7d1711aa832388d90795c9b8e9ed0 100644 (file)
--- a/src/main/interactive_shell.cpp
+++ b/src/main/interactive_shell.cpp
@@ -125,22 +125,25 @@ InteractiveShell::InteractiveShell(ExprManager& exprManager,
       commandsBegin = smt1_commands;
       commandsEnd = smt1_commands + sizeof(smt1_commands) / sizeof(*smt1_commands);
       break;
-    case output::LANG_SMTLIB_V2_0:
-    case output::LANG_SMTLIB_V2_5:
-    case output::LANG_SMTLIB_V2_6:
-      d_historyFilename = string(getenv("HOME")) + "/.cvc4_history_smtlib2";
-      commandsBegin = smt2_commands;
-      commandsEnd = smt2_commands + sizeof(smt2_commands) / sizeof(*smt2_commands);
-      break;
     case output::LANG_TPTP:
       d_historyFilename = string(getenv("HOME")) + "/.cvc4_history_tptp";
       commandsBegin = tptp_commands;
       commandsEnd = tptp_commands + sizeof(tptp_commands) / sizeof(*tptp_commands);
       break;
     default:
-      std::stringstream ss;
-      ss << "internal error: unhandled language " << lang;
-      throw Exception(ss.str());
+      if (language::isOutputLang_smt2(lang))
+      {
+        d_historyFilename = string(getenv("HOME")) + "/.cvc4_history_smtlib2";
+        commandsBegin = smt2_commands;
+        commandsEnd =
+            smt2_commands + sizeof(smt2_commands) / sizeof(*smt2_commands);
+      }
+      else
+      {
+        std::stringstream ss;
+        ss << "internal error: unhandled language " << lang;
+        throw Exception(ss.str());
+      }
     }
     d_usingReadline = true;
     int err = ::read_history(d_historyFilename.c_str());
@@ -333,9 +336,8 @@ restart:
     line += "\n";
     goto restart;
   } catch(ParserException& pe) {
-    if(d_options.getOutputLanguage() == output::LANG_SMTLIB_V2_0 ||
-       d_options.getOutputLanguage() == output::LANG_SMTLIB_V2_5 ||
-       d_options.getOutputLanguage() == output::LANG_SMTLIB_V2_6) {
+    if (language::isOutputLang_smt2(d_options.getOutputLanguage()))
+    {
       d_out << "(error \"" << pe << "\")" << endl;
     } else {
       d_out << pe << endl;

diff --git a/src/main/main.cpp b/src/main/main.cpp
index 758d10af83753182c4789f68bf45dbe99d6bdbf7..29d720b903bdb5af53a7d2f1b145f1f7eb0b0e10 100644 (file)
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -64,9 +64,8 @@ int main(int argc, char* argv[]) {
 #ifdef CVC4_COMPETITION_MODE
     *opts.getOut() << "unknown" << endl;
 #endif
-    if(opts.getOutputLanguage() == output::LANG_SMTLIB_V2_0 ||
-       opts.getOutputLanguage() == output::LANG_SMTLIB_V2_5 ||
-       opts.getOutputLanguage() == output::LANG_SMTLIB_V2_6) {
+    if (language::isOutputLang_smt2(opts.getOutputLanguage()))
+    {
       *opts.getOut() << "(error \"" << e << "\")" << endl;
     } else {
       *opts.getErr() << "CVC4 Error:" << endl << e << endl;

diff --git a/src/options/language.cpp b/src/options/language.cpp
index 86beffd6d35e11ee685068094cfdcad51fb92b41..f76893866475629cfe71aa545113b1bf9f37f255 100644 (file)
--- 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 f238e765d58559356fa8df072b3cad22b9828f3a..2b2e7d5da6aab639f8fd486fbee2c31e398875ec 100644 (file)
--- 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 427e6c6081e6b085b9f82458d830b0cd43a3f90e..177e590f502621bdb85c594889cf0cd8cd0804a4 100644 (file)
--- 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 917dae687f5e441cc09dedb7836aaa1733c18e43..4fdd477b9aef9eb90064689ef116ffef2f222995 100644 (file)
--- 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\

diff --git a/src/parser/antlr_input.cpp b/src/parser/antlr_input.cpp
index a4bab5a8de42af04bdde14add71cbc8c9943b3d1..1e5d62ef8b0d667f05c1905f73772958901dfded 100644 (file)
--- a/src/parser/antlr_input.cpp
+++ b/src/parser/antlr_input.cpp
@@ -254,12 +254,6 @@ AntlrInput* AntlrInput::newInput(InputLanguage lang, AntlrInputStream& inputStre
     input = new Smt1Input(inputStream);
     break;
 
-  case LANG_SMTLIB_V2_0:
-  case LANG_SMTLIB_V2_5:
-  case LANG_SMTLIB_V2_6:
-    input = new Smt2Input(inputStream, lang);
-    break;
-
   case LANG_SYGUS:
     input = new SygusInput(inputStream);
     break;
@@ -269,9 +263,17 @@ AntlrInput* AntlrInput::newInput(InputLanguage lang, AntlrInputStream& inputStre
     break;
 
   default:
-    std::stringstream ss;
-    ss << "internal error: unhandled language " << lang << " in AntlrInput::newInput";
-    throw InputStreamException(ss.str());
+    if (language::isInputLang_smt2(lang))
+    {
+      input = new Smt2Input(inputStream, lang);
+    }
+    else
+    {
+      std::stringstream ss;
+      ss << "internal error: unhandled language " << lang
+         << " in AntlrInput::newInput";
+      throw InputStreamException(ss.str());
+    }
   }
 
   return input;

diff --git a/src/parser/parser_builder.cpp b/src/parser/parser_builder.cpp
index ceda2ba47d8c1f92c30706858a4115df3d48056d..9f161b8301070c941c8b00131d4228506c702e36 100644 (file)
--- a/src/parser/parser_builder.cpp
+++ b/src/parser/parser_builder.cpp
@@ -91,11 +91,6 @@ Parser* ParserBuilder::build()
   case language::input::LANG_SMTLIB_V1:
     parser = new Smt1(d_exprManager, input, d_strictMode, d_parseOnly);
     break;
-  case language::input::LANG_SMTLIB_V2_0:
-  case language::input::LANG_SMTLIB_V2_5:
-  case language::input::LANG_SMTLIB_V2_6:
-    parser = new Smt2(d_exprManager, input, d_strictMode, d_parseOnly);
-    break;
   case language::input::LANG_SYGUS:
     parser = new Smt2(d_exprManager, input, d_strictMode, d_parseOnly);
     break;
@@ -103,7 +98,14 @@ Parser* ParserBuilder::build()
     parser = new Tptp(d_exprManager, input, d_strictMode, d_parseOnly);
     break;
   default:
-    parser = new Parser(d_exprManager, input, d_strictMode, d_parseOnly);
+    if (language::isInputLang_smt2(d_lang))
+    {
+      parser = new Smt2(d_exprManager, input, d_strictMode, d_parseOnly);
+    }
+    else
+    {
+      parser = new Parser(d_exprManager, input, d_strictMode, d_parseOnly);
+    }
     break;
   }
 

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index ae9d304f164b1cf2a735f0d15d3cf14f886d9d5b..74f8e71d3270ffe89e9f8a9928196d3a9ee76106 100644 (file)
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -3103,7 +3103,7 @@ GET_PROOF_TOK : 'get-proof';
 GET_UNSAT_ASSUMPTIONS_TOK : 'get-unsat-assumptions';
 GET_UNSAT_CORE_TOK : 'get-unsat-core';
 EXIT_TOK : 'exit';
-RESET_TOK : { PARSER_STATE->v2_5(false) }? 'reset';
+RESET_TOK : { PARSER_STATE->v2_5() }? 'reset';
 RESET_ASSERTIONS_TOK : 'reset-assertions';
 ITE_TOK : 'ite';
 LET_TOK : { !PARSER_STATE->sygus() }? 'let';
@@ -3362,7 +3362,7 @@ STRING_LITERAL_2_0
  * will be part of the token text.  Use the str[] parser rule instead.
  */
 STRING_LITERAL_2_5
-  : { PARSER_STATE->v2_5(false) || PARSER_STATE->sygus() }?=>
+  : { PARSER_STATE->v2_5() || PARSER_STATE->sygus() }?=>
     '"' (~('"') | '""')* '"'
   ;
 

diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 332c66be1b05f644f271de0dde27c8ab7c5d4707..1d66ab0c1819be919489032a94c993fc3a6e7c22 100644 (file)
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -129,10 +129,22 @@ void Smt2::addStringOperators() {
   addOperator(kind::STRING_STRREPL, "str.replace" );
   addOperator(kind::STRING_PREFIX, "str.prefixof" );
   addOperator(kind::STRING_SUFFIX, "str.suffixof" );
-  addOperator(kind::STRING_ITOS, "int.to.str" );
-  addOperator(kind::STRING_STOI, "str.to.int" );
-  addOperator(kind::STRING_IN_REGEXP, "str.in.re");
-  addOperator(kind::STRING_TO_REGEXP, "str.to.re");
+  // at the moment, we only use this syntax for smt2.6.1
+  if (getInput()->getLanguage() == language::input::LANG_SMTLIB_V2_6_1)
+  {
+    addOperator(kind::STRING_ITOS, "str.from-int");
+    addOperator(kind::STRING_STOI, "str.to-int");
+    addOperator(kind::STRING_IN_REGEXP, "str.in-re");
+    addOperator(kind::STRING_TO_REGEXP, "str.to-re");
+  }
+  else
+  {
+    addOperator(kind::STRING_ITOS, "int.to.str");
+    addOperator(kind::STRING_STOI, "str.to.int");
+    addOperator(kind::STRING_IN_REGEXP, "str.in.re");
+    addOperator(kind::STRING_TO_REGEXP, "str.to.re");
+  }
+
   addOperator(kind::REGEXP_CONCAT, "re.++");
   addOperator(kind::REGEXP_UNION, "re.union");
   addOperator(kind::REGEXP_INTER, "re.inter");

diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h
index 71aa32492f377e430078063ecc774132e8e30fde..e9e36e78c3c3384074baf500157f0ae61b796021 100644 (file)
--- a/src/parser/smt2/smt2.h
+++ b/src/parser/smt2/smt2.h
@@ -155,14 +155,21 @@ public:
   bool v2_0() const {
     return getInput()->getLanguage() == language::input::LANG_SMTLIB_V2_0;
   }
-  // 2.6 is a superset of 2.5, use exact=false to query whether smt lib 2.5 or above
-  bool v2_5( bool exact = true ) const {
-    return exact ? getInput()->getLanguage() == language::input::LANG_SMTLIB_V2_5 : 
-                   ( getInput()->getLanguage() >= language::input::LANG_SMTLIB_V2_5 && 
-                     getInput()->getLanguage() <= language::input::LANG_SMTLIB_V2 );
+  /**
+   * Are we using smtlib 2.5 or above? If exact=true, then this method returns
+   * false if the input language is not exactly SMT-LIB 2.5.
+   */
+  bool v2_5(bool exact = false) const
+  {
+    return language::isInputLang_smt2_5(getInput()->getLanguage(), exact);
   }
-  bool v2_6() const {
-    return getInput()->getLanguage() == language::input::LANG_SMTLIB_V2_6;
+  /**
+   * Are we using 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 v2_6(bool exact = false) const
+  {
+    return language::isInputLang_smt2_6(getInput()->getLanguage(), exact);
   }
   bool sygus() const {
     return getInput()->getLanguage() == language::input::LANG_SYGUS;

diff --git a/src/parser/smt2/smt2_input.cpp b/src/parser/smt2/smt2_input.cpp
index 0958e9d6cf47904ba675c4dc09798b511712262f..b7ffe6991e8d2c3040fb08a3f134ef7dce1f73ff 100644 (file)
--- a/src/parser/smt2/smt2_input.cpp
+++ b/src/parser/smt2/smt2_input.cpp
@@ -66,9 +66,7 @@ Smt2Input::~Smt2Input() {
 }
 
 void Smt2Input::setLanguage(InputLanguage lang) {
-  CheckArgument(lang == language::input::LANG_SMTLIB_V2_0 ||
-                lang == language::input::LANG_SMTLIB_V2_5 ||
-                lang == language::input::LANG_SMTLIB_V2_6, lang);
+  CheckArgument(language::isInputLang_smt2(lang), lang);
   d_lang = lang;
 }
 

diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp
index e8ebadeb87179b2565580c967ecbf0c04e2d89c9..f9486f017d478aee4e2062ee55caeb4a3ac237c7 100644 (file)
--- a/src/printer/printer.cpp
+++ b/src/printer/printer.cpp
@@ -50,6 +50,10 @@ unique_ptr<Printer> Printer::makePrinter(OutputLanguage lang)
     return unique_ptr<Printer>(
         new printer::smt2::Smt2Printer(printer::smt2::smt2_6_variant));
 
+  case LANG_SMTLIB_V2_6_1:
+    return unique_ptr<Printer>(
+        new printer::smt2::Smt2Printer(printer::smt2::smt2_6_1_variant));
+
   case LANG_TPTP:
     return unique_ptr<Printer>(new printer::tptp::TptpPrinter());
 

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 8c9680a7433bee84a8c6c2c8b791848d636dcb9a..5d2b8972d4e2bfe836f12d8b30bad0cac6b5ed47 100644 (file)
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -42,7 +42,13 @@ namespace smt2 {
 
 static OutputLanguage variantToLanguage(Variant v);
 
-static string smtKindString(Kind k);
+static string smtKindString(Kind k, Variant v);
+
+/** returns whether the variant is smt-lib 2.6 or greater */
+bool isVariant_2_6(Variant v)
+{
+  return v == smt2_6_variant || v == smt2_6_1_variant;
+}
 
 static void printBvParameterizedOp(std::ostream& out, TNode n);
 static void printFpParameterizedOp(std::ostream& out, TNode n);
@@ -191,10 +197,10 @@ void Smt2Printer::toStream(std::ostream& out,
       out << (n.getConst<bool>() ? "true" : "false");
       break;
     case kind::BUILTIN:
-      out << smtKindString(n.getConst<Kind>());
+      out << smtKindString(n.getConst<Kind>(), d_variant);
       break;
     case kind::CHAIN_OP:
-      out << smtKindString(n.getConst<Chain>().getOperator());
+      out << smtKindString(n.getConst<Chain>().getOperator(), d_variant);
       break;
     case kind::CONST_RATIONAL: {
       const Rational& r = n.getConst<Rational>();
@@ -323,7 +329,8 @@ void Smt2Printer::toStream(std::ostream& out,
       if (force_nt.isReal())
       {
         out << "(" << smtKindString(force_nt.isInteger() ? kind::TO_INTEGER
-                                                         : kind::TO_REAL)
+                                                         : kind::TO_REAL,
+                                    d_variant)
             << " ";
         toStream(out, n, toDepth, types, TypeNode::null());
         out << ")";
@@ -385,8 +392,8 @@ void Smt2Printer::toStream(std::ostream& out,
     // builtin theory
   case kind::APPLY: break;
   case kind::EQUAL:
-  case kind::DISTINCT: 
-    out << smtKindString(k) << " "; 
+  case kind::DISTINCT:
+    out << smtKindString(k, d_variant) << " ";
     parametricTypeChildren = true;
     break;
   case kind::CHAIN: break;
@@ -407,14 +414,16 @@ void Smt2Printer::toStream(std::ostream& out,
   case kind::IMPLIES:
   case kind::OR:
   case kind::XOR:
-  case kind::ITE: out << smtKindString(k) << " "; break;
+  case kind::ITE:
+    out << smtKindString(k, d_variant) << " ";
+    break;
 
-    // uf theory
+  // uf theory
   case kind::APPLY_UF: typeChildren = true; break;
   // higher-order
   case kind::HO_APPLY: break;
   case kind::LAMBDA:
-    out << smtKindString(k) << " ";
+    out << smtKindString(k, d_variant) << " ";
     break;
 
   // arith theory
@@ -453,7 +462,7 @@ void Smt2Printer::toStream(std::ostream& out,
   case kind::TO_REAL:
   case kind::POW: 
     parametricTypeChildren = true;
-    out << smtKindString(k) << " "; 
+    out << smtKindString(k, d_variant) << " ";
     break;
 
   case kind::DIVISIBLE:
@@ -466,9 +475,11 @@ void Smt2Printer::toStream(std::ostream& out,
   case kind::STORE: typeChildren = true;
   case kind::PARTIAL_SELECT_0:
   case kind::PARTIAL_SELECT_1:
-  case kind::ARRAY_TYPE: out << smtKindString(k) << " "; break;
+  case kind::ARRAY_TYPE:
+    out << smtKindString(k, d_variant) << " ";
+    break;
 
-    // string theory
+  // string theory
   case kind::STRING_CONCAT:
     if(d_variant == z3str_variant) {
       out << "Concat ";
@@ -499,30 +510,30 @@ void Smt2Printer::toStream(std::ostream& out,
       out << ")";
       return;
     }
-    out << "str.in.re ";
+    out << smtKindString(k, d_variant) << " ";
     break;
   }
-  case kind::STRING_LENGTH: out << (d_variant == z3str_variant ? "Length " : "str.len "); break;
-  case kind::STRING_SUBSTR: out << "str.substr "; break;
-  case kind::STRING_CHARAT: out << "str.at "; break;
-  case kind::STRING_STRCTN: out << "str.contains "; break;
-  case kind::STRING_STRIDOF: out << "str.indexof "; break;
-  case kind::STRING_STRREPL: out << "str.replace "; break;
-  case kind::STRING_PREFIX: out << "str.prefixof "; break;
-  case kind::STRING_SUFFIX: out << "str.suffixof "; break;
-  case kind::STRING_ITOS: out << "int.to.str "; break;
-  case kind::STRING_STOI: out << "str.to.int "; break;
-  case kind::STRING_TO_REGEXP: out << "str.to.re "; break;
-  case kind::REGEXP_CONCAT: out << "re.++ "; break;
-  case kind::REGEXP_UNION: out << "re.union "; break;
-  case kind::REGEXP_INTER: out << "re.inter "; break;
-  case kind::REGEXP_STAR: out << "re.* "; break;
-  case kind::REGEXP_PLUS: out << "re.+ "; break;
-  case kind::REGEXP_OPT: out << "re.opt "; break;
-  case kind::REGEXP_RANGE: out << "re.range "; break;
-  case kind::REGEXP_LOOP: out << "re.loop "; break;
-  case kind::REGEXP_EMPTY: out << "re.nostr "; break;
-  case kind::REGEXP_SIGMA: out << "re.allchar "; break;
+  case kind::STRING_LENGTH:
+  case kind::STRING_SUBSTR:
+  case kind::STRING_CHARAT:
+  case kind::STRING_STRCTN:
+  case kind::STRING_STRIDOF:
+  case kind::STRING_STRREPL:
+  case kind::STRING_PREFIX:
+  case kind::STRING_SUFFIX:
+  case kind::STRING_ITOS:
+  case kind::STRING_STOI:
+  case kind::STRING_TO_REGEXP:
+  case kind::REGEXP_CONCAT:
+  case kind::REGEXP_UNION:
+  case kind::REGEXP_INTER:
+  case kind::REGEXP_STAR:
+  case kind::REGEXP_PLUS:
+  case kind::REGEXP_OPT:
+  case kind::REGEXP_RANGE:
+  case kind::REGEXP_LOOP:
+  case kind::REGEXP_EMPTY:
+  case kind::REGEXP_SIGMA: out << smtKindString(k, d_variant) << " "; break;
 
   case kind::CARDINALITY_CONSTRAINT: out << "fmf.card "; break;
   case kind::CARDINALITY_VALUE: out << "fmf.card.val "; break;
@@ -586,12 +597,12 @@ void Smt2Printer::toStream(std::ostream& out,
   case kind::TRANSPOSE:
   case kind::TCLOSURE:
     parametricTypeChildren = true;
-    out << smtKindString(k) << " "; 
+    out << smtKindString(k, d_variant) << " ";
     break;
   case kind::MEMBER: typeChildren = true;
   case kind::SET_TYPE:
   case kind::SINGLETON:
-  case kind::COMPLEMENT:out << smtKindString(k) << " "; break;
+  case kind::COMPLEMENT: out << smtKindString(k, d_variant) << " "; break;
   case kind::UNIVERSE_SET:out << "(as univset " << n.getType() << ")";break;
 
     // fp theory
@@ -621,7 +632,8 @@ void Smt2Printer::toStream(std::ostream& out,
   case kind::FLOATINGPOINT_ISNEG:
   case kind::FLOATINGPOINT_ISPOS:
   case kind::FLOATINGPOINT_TO_REAL:
-    out << smtKindString(k) << ' '; break;
+    out << smtKindString(k, d_variant) << ' ';
+    break;
 
   case kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR:
   case kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT:
@@ -681,7 +693,7 @@ void Smt2Printer::toStream(std::ostream& out,
     case kind::SEP_EMP:
     case kind::SEP_PTO:
     case kind::SEP_STAR:
-    case kind::SEP_WAND: out << smtKindString(k) << " "; break;
+    case kind::SEP_WAND: out << smtKindString(k, d_variant) << " "; break;
 
     case kind::SEP_NIL:
       out << "(as sep.nil " << n.getType() << ")";
@@ -773,7 +785,8 @@ void Smt2Printer::toStream(std::ostream& out,
       }else if( n.getKind()==kind::APPLY_TESTER ){
         unsigned cindex = Datatype::indexOf(n.getOperator().toExpr());
         const Datatype& dt = Datatype::datatypeOf(n.getOperator().toExpr());
-        if( d_variant==smt2_6_variant ){
+        if (isVariant_2_6(d_variant))
+        {
           out << "(_ is ";
           toStream(out, Node::fromExpr(dt[cindex].getConstructor()), toDepth < 0 ? toDepth : toDepth - 1, types, TypeNode::null());
           out << ")";
@@ -856,7 +869,7 @@ void Smt2Printer::toStream(std::ostream& out,
       if(forceBinary && i < n.getNumChildren() - 1) {
         // not going to work properly for parameterized kinds!
         Assert(n.getMetaKind() != kind::metakind::PARAMETERIZED);
-        out << " (" << smtKindString(n.getKind()) << ' ';
+        out << " (" << smtKindString(n.getKind(), d_variant) << ' ';
         parens << ')';
         ++c;
       } else {
@@ -869,7 +882,7 @@ void Smt2Printer::toStream(std::ostream& out,
   }
 }/* Smt2Printer::toStream(TNode) */
 
-static string smtKindString(Kind k)
+static string smtKindString(Kind k, Variant v)
 {
   switch(k) {
     // builtin theory
@@ -1039,7 +1052,7 @@ static string smtKindString(Kind k)
 
   //string theory
   case kind::STRING_CONCAT: return "str.++";
-  case kind::STRING_LENGTH: return "str.len";
+  case kind::STRING_LENGTH: return v == z3str_variant ? "Length" : "str.len";
   case kind::STRING_SUBSTR: return "str.substr" ;
   case kind::STRING_STRCTN: return "str.contains" ;
   case kind::STRING_CHARAT: return "str.at" ;
@@ -1047,10 +1060,14 @@ static string smtKindString(Kind k)
   case kind::STRING_STRREPL: return "str.replace" ;
   case kind::STRING_PREFIX: return "str.prefixof" ;
   case kind::STRING_SUFFIX: return "str.suffixof" ;
-  case kind::STRING_ITOS: return "int.to.str" ;
-  case kind::STRING_STOI: return "str.to.int" ;
-  case kind::STRING_IN_REGEXP: return "str.in.re";
-  case kind::STRING_TO_REGEXP: return "str.to.re";
+  case kind::STRING_ITOS:
+    return v == smt2_6_1_variant ? "str.from-int" : "int.to.str";
+  case kind::STRING_STOI:
+    return v == smt2_6_1_variant ? "str.to-int" : "str.to.int";
+  case kind::STRING_IN_REGEXP:
+    return v == smt2_6_1_variant ? "str.in-re" : "str.in.re";
+  case kind::STRING_TO_REGEXP:
+    return v == smt2_6_1_variant ? "str.to-re" : "str.to.re";
   case kind::REGEXP_CONCAT: return "re.++";
   case kind::REGEXP_UNION: return "re.union";
   case kind::REGEXP_INTER: return "re.inter";
@@ -1310,7 +1327,7 @@ void DeclareTypeCommandToStream(std::ostream& out,
   const std::vector<Node>* type_refs = model.getRepSet()->getTypeRepsOrNull(tn);
   if (options::modelUninterpDtEnum() && tn.isSort() && type_refs != nullptr)
   {
-    if (variant == smt2_6_variant)
+    if (isVariant_2_6(variant))
     {
       out << "(declare-datatypes ((" << command.getSymbol() << " 0)) (";
     }
@@ -1893,7 +1910,7 @@ static void toStream(std::ostream& out,
     out << "co";
   }
   out << "datatypes";
-  if (v == smt2_6_variant)
+  if (isVariant_2_6(v))
   {
     out << " (";
     for (vector<DatatypeType>::const_iterator i = datatypes.begin(),

diff --git a/src/printer/smt2/smt2_printer.h b/src/printer/smt2/smt2_printer.h
index 922b69a9e385ec48b8ef12232c546e0067243bd5..1d281aed488423174c37eda32632d3fe1505f2e9 100644 (file)
--- a/src/printer/smt2/smt2_printer.h
+++ b/src/printer/smt2/smt2_printer.h
@@ -27,14 +27,16 @@ namespace CVC4 {
 namespace printer {
 namespace smt2 {
 
-enum Variant {
+enum Variant
+{
   no_variant,
-  smt2_0_variant, // old-style 2.0 syntax, when it makes a difference
-  smt2_6_variant, // new-style 2.6 syntax, when it makes a difference
-  z3str_variant, // old-style 2.0 and also z3str syntax
-  sygus_variant  // variant for sygus
-};/* enum Variant */
-
+  smt2_0_variant,    // old-style 2.0 syntax, when it makes a difference
+  smt2_6_variant,    // new-style 2.6 syntax, when it makes a difference
+  smt2_6_1_variant,  // new-style 2.6 syntax, when it makes a difference, with
+                     // support for the string standard
+  z3str_variant,     // old-style 2.0 and also z3str syntax
+  sygus_variant      // variant for sygus
+};                   /* enum Variant */
 class Smt2Printer : public CVC4::Printer {
  public:
   Smt2Printer(Variant variant = no_variant) : d_variant(variant) { }

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 97e3f0215dc443154a1275bec97d26eaccc31983..ca01ccd8e8c96915f4ec25ba8bab72a72774bd2f 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1304,8 +1304,8 @@ void SmtEngine::setDefaults() {
   // Language-based defaults
   if (!options::bitvectorDivByZeroConst.wasSetByUser())
   {
-    options::bitvectorDivByZeroConst.set(options::inputLanguage()
-                                         == language::input::LANG_SMTLIB_V2_6);
+    options::bitvectorDivByZeroConst.set(
+        language::isInputLang_smt2_6(options::inputLanguage()));
   }
   if (options::inputLanguage() == language::input::LANG_SYGUS)
   {
@@ -2262,44 +2262,40 @@ void SmtEngine::setInfo(const std::string& key, const CVC4::SExpr& value)
     d_filename = value.getValue();
     return;
   } else if(key == "smt-lib-version") {
+    language::input::Language ilang = language::input::LANG_AUTO;
     if( (value.isInteger() && value.getIntegerValue() == Integer(2)) ||
         (value.isRational() && value.getRationalValue() == Rational(2)) ||
         value.getValue() == "2" ||
         value.getValue() == "2.0" ) {
-      options::inputLanguage.set(language::input::LANG_SMTLIB_V2_0);
-
-      // supported SMT-LIB version
-      if(!options::outputLanguage.wasSetByUser() &&
-         ( options::outputLanguage() == language::output::LANG_SMTLIB_V2_5 || options::outputLanguage() == language::output::LANG_SMTLIB_V2_6 )) {
-        options::outputLanguage.set(language::output::LANG_SMTLIB_V2_0);
-        *options::out() << language::SetLanguage(language::output::LANG_SMTLIB_V2_0);
-      }
-      return;
+      ilang = language::input::LANG_SMTLIB_V2_0;
     } else if( (value.isRational() && value.getRationalValue() == Rational(5, 2)) ||
                value.getValue() == "2.5" ) {
-      options::inputLanguage.set(language::input::LANG_SMTLIB_V2_5);
-
-      // supported SMT-LIB version
-      if(!options::outputLanguage.wasSetByUser() &&
-         options::outputLanguage() == language::output::LANG_SMTLIB_V2_0) {
-        options::outputLanguage.set(language::output::LANG_SMTLIB_V2_5);
-        *options::out() << language::SetLanguage(language::output::LANG_SMTLIB_V2_5);
-      }
-      return;
+      ilang = language::input::LANG_SMTLIB_V2_5;
     } else if( (value.isRational() && value.getRationalValue() == Rational(13, 5)) ||
                value.getValue() == "2.6" ) {
-      options::inputLanguage.set(language::input::LANG_SMTLIB_V2_6);
-
-      // supported SMT-LIB version
-      if(!options::outputLanguage.wasSetByUser() &&
-         options::outputLanguage() == language::output::LANG_SMTLIB_V2_0) {
-        options::outputLanguage.set(language::output::LANG_SMTLIB_V2_6);
-        *options::out() << language::SetLanguage(language::output::LANG_SMTLIB_V2_6);
+      ilang = language::input::LANG_SMTLIB_V2_6;
+    }
+    else if (value.getValue() == "2.6.1")
+    {
+      ilang = language::input::LANG_SMTLIB_V2_6_1;
+    }
+    else
+    {
+      Warning() << "Warning: unsupported smt-lib-version: " << value << endl;
+      throw UnrecognizedOptionException();
+    }
+    options::inputLanguage.set(ilang);
+    // also update the output language
+    if (!options::outputLanguage.wasSetByUser())
+    {
+      language::output::Language olang = language::toOutputLanguage(ilang);
+      if (options::outputLanguage() != olang)
+      {
+        options::outputLanguage.set(olang);
+        *options::out() << language::SetLanguage(olang);
       }
-      return;
     }
-    Warning() << "Warning: unsupported smt-lib-version: " << value << endl;
-    throw UnrecognizedOptionException();
+    return;
   } else if(key == "status") {
     string s;
     if(value.isAtom()) {

diff --git a/src/util/result.cpp b/src/util/result.cpp
index 27d82bb6f46a554c889ad543bcbd1a63441670ae..dfcd74ff7bdbc92e4724643c02b0154ccaa9069d 100644 (file)
--- a/src/util/result.cpp
+++ b/src/util/result.cpp
@@ -349,24 +349,21 @@ void Result::toStreamTptp(std::ostream& out) const {
 
 void Result::toStream(std::ostream& out, OutputLanguage language) const {
   switch (language) {
-    case language::output::LANG_SMTLIB_V2_0:
-    case language::output::LANG_SMTLIB_V2_5:
-    case language::output::LANG_SMTLIB_V2_6:
     case language::output::LANG_SYGUS:
-    case language::output::LANG_Z3STR:
       toStreamSmt2(out);
       break;
     case language::output::LANG_TPTP:
       toStreamTptp(out);
       break;
-    case language::output::LANG_AST:
-    case language::output::LANG_AUTO:
-    case language::output::LANG_CVC3:
-    case language::output::LANG_CVC4:
-    case language::output::LANG_MAX:
-    case language::output::LANG_SMTLIB_V1:
     default:
-      toStreamDefault(out);
+      if (language::isOutputLang_smt2(language))
+      {
+        toStreamSmt2(out);
+      }
+      else
+      {
+        toStreamDefault(out);
+      }
       break;
   };
 }

diff --git a/src/util/sexpr.cpp b/src/util/sexpr.cpp
index 504d58b0e3b6331241f3f5119e024cccd52b01fc..fbc8802d672c0aad3958b3970e875dcc666e13c8 100644 (file)
--- a/src/util/sexpr.cpp
+++ b/src/util/sexpr.cpp
@@ -273,18 +273,13 @@ void SExpr::toStreamRec(std::ostream& out, const SExpr& sexpr,
 bool SExpr::languageQuotesKeywords(OutputLanguage language) {
   switch (language) {
     case language::output::LANG_SMTLIB_V1:
-    case language::output::LANG_SMTLIB_V2_0:
-    case language::output::LANG_SMTLIB_V2_5:
-    case language::output::LANG_SMTLIB_V2_6:
     case language::output::LANG_SYGUS:
     case language::output::LANG_TPTP:
-    case language::output::LANG_Z3STR:
       return true;
     case language::output::LANG_AST:
     case language::output::LANG_CVC3:
     case language::output::LANG_CVC4:
-    default:
-      return false;
+    default: return language::isOutputLang_smt2(language);
   };
 }
 

diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests
index f8a32046f9a58134fc8b3f7f1f9b749406847f8c..3674e42bb6e0bfea3ff7a16023f1f1b46769c67b 100644 (file)
--- a/test/regress/Makefile.tests
+++ b/test/regress/Makefile.tests
@@ -788,6 +788,7 @@ REG0_TESTS = \
        regress0/strings/norn-simp-rew.smt2 \
        regress0/strings/repl-rewrites2.smt2 \
        regress0/strings/rewrites-v2.smt2 \
+       regress0/strings/std2.6.1.smt2 \
        regress0/strings/str003.smt2 \
        regress0/strings/str004.smt2 \
        regress0/strings/str005.smt2 \

diff --git a/test/regress/regress0/strings/bug002.smt2 b/test/regress/regress0/strings/bug002.smt2
index f8a481e14f7f8f40942f45f1627f9f32fcc51bc9..fd60089fd09ad9e2d9387e86eb9bf6af0071f5d6 100644 (file)
--- a/test/regress/regress0/strings/bug002.smt2
+++ b/test/regress/regress0/strings/bug002.smt2
@@ -1,5 +1,5 @@
-(set-logic ASLIA)
 (set-info :smt-lib-version 2.0)
+(set-logic ASLIA)
 (set-option :strings-exp true)
 (set-info :status sat)
 
@@ -7,4 +7,4 @@
 (define-fun strinre ((?s String)) Bool (str.in.re ?s (re.union re.nostr (re.++ (str.to.re "") (str.to.re "") (re.union re.nostr (re.range "*" ",") (str.to.re "\t") (re.range "*" "|") ) (re.+ (re.union re.nostr (re.++ (str.to.re "") (str.to.re "") (re.loop re.allchar 6 ) (re.opt (re.union re.nostr (re.++ (str.to.re "") (str.to.re "") ) ) ) ) ) ) ) )  ) )
 (assert (not (strinre "6O\1\127\n?")))
 
-(check-sat)
\ No newline at end of file
+(check-sat)

diff --git a/test/regress/regress0/strings/issue1189.smt2 b/test/regress/regress0/strings/issue1189.smt2
index fae641ea8ec384f7e951b696d9ce6d85a920237a..0b581994c4b383b4c46e32e1b6d9eb5e6b4dade0 100644 (file)
--- a/test/regress/regress0/strings/issue1189.smt2
+++ b/test/regress/regress0/strings/issue1189.smt2
@@ -1,3 +1,4 @@
+(set-info :smt-lib-version 2.5)
 (set-logic ALL_SUPPORTED)
 (set-info :status unsat)
 (set-option :strings-exp true)

diff --git a/test/regress/regress0/strings/leadingzero001.smt2 b/test/regress/regress0/strings/leadingzero001.smt2
index 2889348c121d5eb67a1b46da9cb5f0d21d1a8ece..09fd80a7b7e6b757f372094b367b271ea47be057 100644 (file)
--- a/test/regress/regress0/strings/leadingzero001.smt2
+++ b/test/regress/regress0/strings/leadingzero001.smt2
@@ -1,3 +1,4 @@
+(set-info :smt-lib-version 2.5)
 (set-logic QF_S)
 (set-option :strings-exp true)
 (set-info :status sat)

diff --git a/test/regress/regress0/strings/norn-31.smt2 b/test/regress/regress0/strings/norn-31.smt2
index 4698f966fceca6a20efcca548189fc5ca6ae293a..1830dd882fa79c016d415b7cf26ae4d1b522c67e 100644 (file)
--- a/test/regress/regress0/strings/norn-31.smt2
+++ b/test/regress/regress0/strings/norn-31.smt2
@@ -1,3 +1,4 @@
+(set-info :smt-lib-version 2.5)
 (set-logic QF_SLIA)
 (set-option :strings-exp true)
 (set-info :status unsat)

diff --git a/test/regress/regress0/strings/norn-simp-rew.smt2 b/test/regress/regress0/strings/norn-simp-rew.smt2
index 45f7ede9477e7bb4ecb94477c2b0464ce56be03d..d729fe5d0106fb15a8511d98a884297ebb87bae6 100644 (file)
--- a/test/regress/regress0/strings/norn-simp-rew.smt2
+++ b/test/regress/regress0/strings/norn-simp-rew.smt2
@@ -1,3 +1,4 @@
+(set-info :smt-lib-version 2.5)
 (set-logic QF_SLIA)
 (set-option :strings-exp true)
 (set-info :status unsat)
@@ -26,4 +27,4 @@
 (assert (str.in.re var_8 (re.* (re.range "a" "u"))))
 (assert (str.in.re var_7 (re.* (re.range "a" "u"))))
 (assert (not (str.in.re (str.++ "b" var_7 ) (re.* (re.range "a" "u")))))
-(check-sat)
\ No newline at end of file
+(check-sat)

diff --git a/test/regress/regress0/strings/rewrites-v2.smt2 b/test/regress/regress0/strings/rewrites-v2.smt2
index 7e285b51a7be1472474914be3d59f2ec82b5f4f5..ce2f140ae236534b929b8f033db8f09c08288324 100644 (file)
--- a/test/regress/regress0/strings/rewrites-v2.smt2
+++ b/test/regress/regress0/strings/rewrites-v2.smt2
@@ -1,5 +1,6 @@
 ; COMMAND-LINE: --strings-exp
 ; EXPECT: unsat
+(set-info :smt-lib-version 2.5)
 (set-logic SLIA)
 (set-info :status unsat)
 (declare-fun x () String)

diff --git a/test/regress/regress0/strings/std2.6.1.smt2 b/test/regress/regress0/strings/std2.6.1.smt2
new file mode 100644 (file)
index 0000000..3302a29
--- /dev/null
+++ b/test/regress/regress0/strings/std2.6.1.smt2
@@ -0,0 +1,9 @@
+; COMMAND-LINE: --strings-exp --lang=smt2.6.1
+; EXPECT: sat
+(set-logic QF_UFSLIA)
+(set-info :status sat)
+(declare-fun x () String)
+(assert (str.in-re x (str.to-re "A")))
+(declare-fun y () Int)
+(assert (= (str.to-int (str.from-int y)) y))
+(check-sat)

diff --git a/test/regress/regress0/strings/type001.smt2 b/test/regress/regress0/strings/type001.smt2
index 77eabccccf14a41f8678cfc8a472fb73837f4912..89191ac3485cf1b2ae21c934d61b4379716cfad5 100644 (file)
--- a/test/regress/regress0/strings/type001.smt2
+++ b/test/regress/regress0/strings/type001.smt2
@@ -1,3 +1,4 @@
+(set-info :smt-lib-version 2.5)
 (set-logic QF_S)
 (set-info :status sat)
 (set-option :strings-exp true)
@@ -18,4 +19,4 @@
 ;should be -1
 (assert (= j (str.to.int "-783914785582390527685649")))
 
-(check-sat)
\ No newline at end of file
+(check-sat)

diff --git a/test/regress/regress1/strings/artemis-0512-nonterm.smt2 b/test/regress/regress1/strings/artemis-0512-nonterm.smt2
index 4b1cad8f620f928840864c66c87a4909b7f12923..a3cca23a2dab36f0d3331b6eafe0d2ff316132a2 100644 (file)
--- a/test/regress/regress1/strings/artemis-0512-nonterm.smt2
+++ b/test/regress/regress1/strings/artemis-0512-nonterm.smt2
@@ -1,3 +1,4 @@
+(set-info :smt-lib-version 2.5)
 (set-logic QF_S)
 (set-option :strings-exp true)
 (set-info :status unsat)

diff --git a/test/regress/regress1/strings/bug615.smt2 b/test/regress/regress1/strings/bug615.smt2
index 86cc592fb2a5f34a3bea043bc195a4ba66505f46..673b0dbd03eaab2964659f909cef675ed16c9bcc 100644 (file)
--- a/test/regress/regress1/strings/bug615.smt2
+++ b/test/regress/regress1/strings/bug615.smt2
@@ -1,3 +1,4 @@
+(set-info :smt-lib-version 2.5)
 (set-logic QF_S)
 (set-option :strings-exp true)
 (set-info :status sat)

diff --git a/test/regress/regress1/strings/bug686dd.smt2 b/test/regress/regress1/strings/bug686dd.smt2
index 7c923654d64800f36a63b00f74ae07d52bb34a73..0cb9fac2655e76db3ccf77f3ab214f64d901af15 100644 (file)
--- a/test/regress/regress1/strings/bug686dd.smt2
+++ b/test/regress/regress1/strings/bug686dd.smt2
@@ -1,7 +1,8 @@
+(set-info :smt-lib-version 2.5)
 (set-logic UFDTSLIA)
 (set-info :status sat)
 
-(declare-datatypes ((T 0)) ( ((TC (TCb String))) ) )
+(declare-datatypes () ((T (TC (TCb String)))))
 
 (declare-fun root5 () String)
 (declare-fun root6 () T)

diff --git a/test/regress/regress1/strings/bug799-min.smt2 b/test/regress/regress1/strings/bug799-min.smt2
index 06acffc973a24f25415cd1a74e7da9944f49adac..0cd15af4ed6ee40a349660a60d26a523f7f4134b 100644 (file)
--- a/test/regress/regress1/strings/bug799-min.smt2
+++ b/test/regress/regress1/strings/bug799-min.smt2
@@ -1,5 +1,6 @@
 ; COMMAND-LINE: --incremental --strings-exp
 ; EXPECT: sat
+(set-info :smt-lib-version 2.5)
 (set-logic ALL)
 (set-info :status sat)
 

diff --git a/test/regress/regress1/strings/fmf001.smt2 b/test/regress/regress1/strings/fmf001.smt2
index 6081c8e06e69ece8abc5651944918610149424ad..71ae63e87b4eb429aa55b7af8b9f9076f51e5b34 100644 (file)
--- a/test/regress/regress1/strings/fmf001.smt2
+++ b/test/regress/regress1/strings/fmf001.smt2
@@ -1,3 +1,4 @@
+(set-info :smt-lib-version 2.5)
 (set-logic QF_S)
 (set-option :strings-exp true)
 (set-option :strings-fmf true)

diff --git a/test/regress/regress1/strings/fmf002.smt2 b/test/regress/regress1/strings/fmf002.smt2
index d52dae2d2b1476985b71fcd5a52c846497f94c42..ab3dc2ae2b8b8a40a77251345297a029970e0b6a 100644 (file)
--- a/test/regress/regress1/strings/fmf002.smt2
+++ b/test/regress/regress1/strings/fmf002.smt2
@@ -1,3 +1,4 @@
+(set-info :smt-lib-version 2.5)
 (set-logic QF_S)
 (set-option :strings-exp true)
 (set-option :strings-fmf true)

diff --git a/test/regress/regress1/strings/issue1105.smt2 b/test/regress/regress1/strings/issue1105.smt2
index 81e7672dabd836dbf9be970f04045faf96842269..bf5cb7669e96871b83c47aacbc3e5074be46cab8 100644 (file)
--- a/test/regress/regress1/strings/issue1105.smt2
+++ b/test/regress/regress1/strings/issue1105.smt2
@@ -1,9 +1,10 @@
+(set-info :smt-lib-version 2.5)
 (set-logic ALL)
 (set-option :strings-exp true)
 (set-info :status sat)
-(declare-datatype Val (
+(declare-datatypes () ((Val
     (Str (str String))
-    (Num (num Int))))
+    (Num (num Int)))))
 
 (declare-const var0 Val)
 (assert (=> (is-Str var0) (distinct (str.to.int (str var0)) (- 1))))

diff --git a/test/regress/regress1/strings/kaluza-fl.smt2 b/test/regress/regress1/strings/kaluza-fl.smt2
index 04775d61c7ea95360f8f82758ea470562756e853..20c2e6aa431f51403ab5dcc8ccfe9a3d20227f7e 100644 (file)
--- a/test/regress/regress1/strings/kaluza-fl.smt2
+++ b/test/regress/regress1/strings/kaluza-fl.smt2
@@ -1,3 +1,4 @@
+(set-info :smt-lib-version 2.5)
 (set-logic QF_S)
 (set-info :status sat)
 

diff --git a/test/regress/regress1/strings/norn-360.smt2 b/test/regress/regress1/strings/norn-360.smt2
index 573dcbe01de528f2e005b38b5851a813564d6408..20ab0b33808544372407a694392950475fd67335 100644 (file)
--- a/test/regress/regress1/strings/norn-360.smt2
+++ b/test/regress/regress1/strings/norn-360.smt2
@@ -1,3 +1,4 @@
+(set-info :smt-lib-version 2.5)
 (set-logic QF_SLIA)
 (set-option :strings-exp true)
 (set-info :status sat)
@@ -22,4 +23,4 @@
 (assert (str.in.re var_4 (re.* (re.range "a" "u"))))
 (assert (str.in.re var_3 (re.* (re.range "a" "u"))))
 (assert (<= 0  (str.len var_4)))
-(check-sat)
\ No newline at end of file
+(check-sat)

diff --git a/test/regress/regress1/strings/norn-ab.smt2 b/test/regress/regress1/strings/norn-ab.smt2
index 48d88984713dd587faf417882893fcf48ed7aafc..47c218179ae9972bfe5c12262bade3b6c40a7c56 100644 (file)
--- a/test/regress/regress1/strings/norn-ab.smt2
+++ b/test/regress/regress1/strings/norn-ab.smt2
@@ -1,3 +1,4 @@
+(set-info :smt-lib-version 2.5)
 (set-logic QF_SLIA)
 (set-info :status unsat)
 (set-option :strings-exp true)
@@ -22,4 +23,4 @@
 (assert (str.in.re var_4 (re.++ (re.* (str.to.re "a")) (re.++ (str.to.re "b") (re.* (str.to.re "b"))))))
 (assert (not (str.in.re (str.++ "a" var_4 "b" ) (re.++ (re.* (str.to.re "a")) (re.++ (str.to.re "b") (re.* (str.to.re "b")))))))
 (assert (and (<= 0  (str.len var_4)) (not (not (exists ((v Int)) (= (* v 2 ) (+ (str.len var_4) 2 )))))))
-(check-sat)
\ No newline at end of file
+(check-sat)

diff --git a/test/regress/regress1/strings/norn-nel-bug-052116.smt2 b/test/regress/regress1/strings/norn-nel-bug-052116.smt2
index f0c2534a1f93cfaac6a6c5c7456afaa0d6d08fb9..9f06152f708c387e3a1298ab872fd8c661888826 100644 (file)
--- a/test/regress/regress1/strings/norn-nel-bug-052116.smt2
+++ b/test/regress/regress1/strings/norn-nel-bug-052116.smt2
@@ -1,3 +1,4 @@
+(set-info :smt-lib-version 2.5)
 (set-logic QF_S)
 (set-info :status sat)
 (set-option :strings-exp true)

diff --git a/test/regress/regress1/strings/norn-simp-rew-sat.smt2 b/test/regress/regress1/strings/norn-simp-rew-sat.smt2
index 01a102bf951c8be438904ee86e0fdf93a900aac1..1336d3bfc2979040c32930beb07faa6b0f3040c3 100644 (file)
--- a/test/regress/regress1/strings/norn-simp-rew-sat.smt2
+++ b/test/regress/regress1/strings/norn-simp-rew-sat.smt2
@@ -1,3 +1,4 @@
+(set-info :smt-lib-version 2.5)
 (set-logic QF_SLIA)
 (set-option :strings-exp true)
 (set-info :status sat)
@@ -22,4 +23,4 @@
 (assert (str.in.re var_3 (re.* (re.range "a" "u"))))
 (assert (str.in.re var_3 (re.* (str.to.re "a"))))
 (assert (<= 0  (str.len var_4)))
-(check-sat)
\ No newline at end of file
+(check-sat)

diff --git a/test/regress/regress1/strings/pierre150331.smt2 b/test/regress/regress1/strings/pierre150331.smt2
index 88d5ec10c63bc1df555a438459a9ef309b294c49..add60d5346a00b4732c61646be6b7f938ff25f63 100644 (file)
--- a/test/regress/regress1/strings/pierre150331.smt2
+++ b/test/regress/regress1/strings/pierre150331.smt2
@@ -1,3 +1,4 @@
+(set-info :smt-lib-version 2.5)\r
 (set-logic SLIA)\r
 (set-info :status sat)\r
 (set-info :smt-lib-version 2.5)\r
@@ -10,4 +11,4 @@
 (declare-fun s1() String)\r
 (declare-fun s2() String)\r
 (assert (and true (stringEval s0) (stringEval s1) (distinct s0 s1) (stringEval s2) (distinct s0 s2) (distinct s1 s2) ) )\r
-(check-sat)
\ No newline at end of file
+(check-sat)\r

diff --git a/test/regress/regress1/strings/regexp001.smt2 b/test/regress/regress1/strings/regexp001.smt2
index 62c142d1da6b2fb80bf6d26cfd007af44814bc3c..142ff679d92a0d233d7234ed9819af16e6d51668 100644 (file)
--- a/test/regress/regress1/strings/regexp001.smt2
+++ b/test/regress/regress1/strings/regexp001.smt2
@@ -1,3 +1,4 @@
+(set-info :smt-lib-version 2.5)
 (set-logic QF_S)
 (set-info :status sat)
 (set-option :strings-exp true)

diff --git a/test/regress/regress1/strings/regexp002.smt2 b/test/regress/regress1/strings/regexp002.smt2
index a8bd2187a5308606bb5f7416f80c4f54efaba969..f109a484e925a68ffac3108913133e9fe844a5ca 100644 (file)
--- a/test/regress/regress1/strings/regexp002.smt2
+++ b/test/regress/regress1/strings/regexp002.smt2
@@ -1,3 +1,4 @@
+(set-info :smt-lib-version 2.5)
 (set-logic QF_S)
 (set-info :status sat)
 (set-option :strings-exp true)

diff --git a/test/regress/regress1/strings/regexp003.smt2 b/test/regress/regress1/strings/regexp003.smt2
index 7696838fe1d28d3cb9932d89bc362e48ccb01440..7c05b422f82086cee41da4c2748ce857658f28e7 100644 (file)
--- a/test/regress/regress1/strings/regexp003.smt2
+++ b/test/regress/regress1/strings/regexp003.smt2
@@ -1,3 +1,4 @@
+(set-info :smt-lib-version 2.5)
 (set-logic QF_S)
 (set-info :status sat)
 (set-option :strings-exp true)

diff --git a/test/regress/regress1/strings/reloop.smt2 b/test/regress/regress1/strings/reloop.smt2
index 9915504ae4889901c6f099deca43c09c2cff68b8..967e564ce99932155dbc5188c86c89662d7fce0e 100644 (file)
--- a/test/regress/regress1/strings/reloop.smt2
+++ b/test/regress/regress1/strings/reloop.smt2
@@ -1,3 +1,4 @@
+(set-info :smt-lib-version 2.5)
 (set-logic QF_S)
 (set-option :strings-exp true)
 (set-info :status sat)

diff --git a/test/regress/regress1/strings/string-unsound-sem.smt2 b/test/regress/regress1/strings/string-unsound-sem.smt2
index 771d8d4b08e76cb49cc68c194f10d634b8dfde49..44591b47ba6a760bfd4ebae1b064aba0bdb16924 100644 (file)
--- a/test/regress/regress1/strings/string-unsound-sem.smt2
+++ b/test/regress/regress1/strings/string-unsound-sem.smt2
@@ -1,3 +1,4 @@
+(set-info :smt-lib-version 2.5)
 (set-logic ALL)
 (set-option :strings-exp true)
 (set-info :status sat)

diff --git a/test/regress/regress1/strings/type002.smt2 b/test/regress/regress1/strings/type002.smt2
index 0df0f20b0cd2fa7bc83d773eb55fcd8f55ea728e..458ac75fe254f9377a3eb45ba4897dd9f0a546ef 100644 (file)
--- a/test/regress/regress1/strings/type002.smt2
+++ b/test/regress/regress1/strings/type002.smt2
@@ -1,3 +1,4 @@
+(set-info :smt-lib-version 2.5)
 (set-logic QF_S)
 (set-info :status sat)
 (set-option :strings-exp true)

diff --git a/test/regress/regress1/strings/type003.smt2 b/test/regress/regress1/strings/type003.smt2
index c2d4792cc6bd0c227840f087f74d3ff3d3da5592..4185041f7d401ec8851787f56226452ceee2841b 100644 (file)
--- a/test/regress/regress1/strings/type003.smt2
+++ b/test/regress/regress1/strings/type003.smt2
@@ -1,3 +1,4 @@
+(set-info :smt-lib-version 2.5)
 (set-logic QF_S)
 (set-info :status sat)
 (set-option :strings-exp true)

diff --git a/test/regress/regress1/strings/username_checker_min.smt2 b/test/regress/regress1/strings/username_checker_min.smt2
index 2f1c35844704f311e35057b36874f634b7711942..f6c152a2a580ff5d41dc548454ee3e5935045d0f 100644 (file)
--- a/test/regress/regress1/strings/username_checker_min.smt2
+++ b/test/regress/regress1/strings/username_checker_min.smt2
@@ -1,3 +1,4 @@
+(set-info :smt-lib-version 2.5)
 (set-logic QF_S)
 (set-option :strings-exp true)
 (set-info :status unsat)