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

4 files changed, 33 insertions, 16 deletions

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index ae9d304f1..74f8e71d3 100644
--- 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 332c66be1..1d66ab0c1 100644
--- 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 71aa32492..e9e36e78c 100644
--- 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 0958e9d6c..b7ffe6991 100644
--- 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;
 }