Simple changes towards unicode string standard (#3791)

This updates --lang=smt2.6.1 with the minor syntactic differences from the current syntax and the standard here: http://smtlib.cs.uiowa.edu/theories-UnicodeStrings.shtml.

The next steps will be to address the more invasive changes required to support the standard.

diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 11dedb25954d8dc43b363a753168aeba63a29d0c..a7033b2776f5de286938c84e8921b7f5ccb596ad 100644 (file)
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -163,7 +163,6 @@ void Smt2::addStringOperators() {
   addOperator(kind::STRING_CHARAT, "str.at" );
   addOperator(kind::STRING_STRIDOF, "str.indexof" );
   addOperator(kind::STRING_STRREPL, "str.replace" );
-  addOperator(kind::STRING_STRREPLALL, "str.replaceall");
   if (!strictModeEnabled())
   {
     addOperator(kind::STRING_TOLOWER, "str.tolower");
@@ -175,10 +174,12 @@ void Smt2::addStringOperators() {
   // at the moment, we only use this syntax for smt2.6.1
   if (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");
+    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");
+    addOperator(kind::STRING_CODE, "str.to_code");
+    addOperator(kind::STRING_STRREPLALL, "str.replace_all");
   }
   else
   {
@@ -186,6 +187,8 @@ void Smt2::addStringOperators() {
     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::STRING_CODE, "str.code");
+    addOperator(kind::STRING_STRREPLALL, "str.replaceall");
   }
 
   addOperator(kind::REGEXP_CONCAT, "re.++");
@@ -196,7 +199,6 @@ void Smt2::addStringOperators() {
   addOperator(kind::REGEXP_OPT, "re.opt");
   addOperator(kind::REGEXP_RANGE, "re.range");
   addOperator(kind::REGEXP_LOOP, "re.loop");
-  addOperator(kind::STRING_CODE, "str.code");
   addOperator(kind::STRING_LT, "str.<");
   addOperator(kind::STRING_LEQ, "str.<=");
 }
@@ -365,7 +367,14 @@ void Smt2::addTheory(Theory theory) {
     defineType("RegLan", getExprManager()->regExpType());
     defineType("Int", getExprManager()->integerType());
 
-    defineVar("re.nostr", d_solver->mkRegexpEmpty().getExpr());
+    if (getLanguage() == language::input::LANG_SMTLIB_V2_6_1)
+    {
+      defineVar("re.none", d_solver->mkRegexpEmpty().getExpr());
+    }
+    else
+    {
+      defineVar("re.nostr", d_solver->mkRegexpEmpty().getExpr());
+    }
     defineVar("re.allchar", d_solver->mkRegexpSigma().getExpr());
 
     addStringOperators();

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 159f87037aeda3fd242b7144512bb76ce43284c7..d61203ac2d697ca525413ad8b87fd7c90b31e6b1 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -884,6 +884,7 @@ set(regress_0_tests
   regress0/strings/bug002.smt2
   regress0/strings/bug612.smt2
   regress0/strings/bug613.smt2
+  regress0/strings/code-eval.smt2
   regress0/strings/code-perf.smt2
   regress0/strings/code-sat-neg-one.smt2
   regress0/strings/escchar.smt2
@@ -907,6 +908,7 @@ set(regress_0_tests
   regress0/strings/norn-simp-rew.smt2
   regress0/strings/parser-syms.cvc
   regress0/strings/re.all.smt2
+  regress0/strings/re-syntax.smt2
   regress0/strings/regexp-native-simple.cvc
   regress0/strings/regexp_inclusion.smt2
   regress0/strings/regexp_inclusion_reduction.smt2

diff --git a/test/regress/regress0/strings/code-eval.smt2 b/test/regress/regress0/strings/code-eval.smt2
new file mode 100644 (file)
index 0000000..faa5c17
--- /dev/null
+++ b/test/regress/regress0/strings/code-eval.smt2
@@ -0,0 +1,10 @@
+; COMMAND-LINE: --lang=smt2.6.1
+; EXPECT: sat
+(set-logic ALL)
+(set-info :status sat)
+
+(assert (< (str.to_code "A") (str.to_code "Z")))
+(assert (= (- 1) (str.to_code "AAA")))
+(assert (= (- 1) (str.to_code "")))
+
+(check-sat)

diff --git a/test/regress/regress0/strings/code-perf.smt2 b/test/regress/regress0/strings/code-perf.smt2
index 39cab48ce3fb96e1b72b1100a6908dcfe47ab59e..4d7e22bd314700cb60eb6efb73cbda5896ae8ca2 100644 (file)
--- a/test/regress/regress0/strings/code-perf.smt2
+++ b/test/regress/regress0/strings/code-perf.smt2
@@ -1,5 +1,6 @@
 ; COMMAND-LINE: --strings-exp
 ; EXPECT: sat
+(set-info :smt-lib-version 2.5)
 (set-logic QF_SLIA)
 (declare-const x0 String)
 (declare-const x1 String)

diff --git a/test/regress/regress0/strings/code-sat-neg-one.smt2 b/test/regress/regress0/strings/code-sat-neg-one.smt2
index c69276a4f40fef0d9334e2eec72712c555fdc88f..403319d02e9af059f255a1682963d3df0d2ed776 100644 (file)
--- a/test/regress/regress0/strings/code-sat-neg-one.smt2
+++ b/test/regress/regress0/strings/code-sat-neg-one.smt2
@@ -1,3 +1,4 @@
+(set-info :smt-lib-version 2.5)
 (set-logic QF_SLIA)
 (set-info :status sat)
 (declare-fun x () String)

diff --git a/test/regress/regress0/strings/re-syntax.smt2 b/test/regress/regress0/strings/re-syntax.smt2
new file mode 100644 (file)
index 0000000..4c25a65
--- /dev/null
+++ b/test/regress/regress0/strings/re-syntax.smt2
@@ -0,0 +1,9 @@
+; COMMAND-LINE: --lang=smt2.6.1
+; EXPECT: unsat
+(set-logic ALL)
+(set-info :status unsat)
+(declare-fun x () String)
+
+(assert (or (str.in_re x re.none) (not (str.in_re x re.all))))
+
+(check-sat)

diff --git a/test/regress/regress0/strings/replaceall-eval.smt2 b/test/regress/regress0/strings/replaceall-eval.smt2
index 924515901874c5dcc66688e26bac8377b25ce1da..c118a7dc4ab8a3470b01a2589fefdbbc7eb37c96 100644 (file)
--- a/test/regress/regress0/strings/replaceall-eval.smt2
+++ b/test/regress/regress0/strings/replaceall-eval.smt2
@@ -1,10 +1,11 @@
-(set-info :smt-lib-version 2.5)
+; COMMAND-LINE: --lang=smt2.6.1
+; EXPECT: sat
 (set-logic ALL)
 (set-info :status sat)
 (declare-fun x () String)
 (declare-fun y () String)
 
-(assert (= x (str.replaceall "AABAABBC" "B" "def")))
-(assert (= y (str.replaceall "AABAABBC" "AB" "BA")))
+(assert (= x (str.replace_all "AABAABBC" "B" "def")))
+(assert (= y (str.replace_all "AABAABBC" "AB" "BA")))
 
 (check-sat)

diff --git a/test/regress/regress0/strings/std2.6.1.smt2 b/test/regress/regress0/strings/std2.6.1.smt2
index 3302a29e53e52a876d3b7f9e8ddd538c7eeb5ac2..d30cfc83c9720d917d2ee014f6e49ccb93764029 100644 (file)
--- a/test/regress/regress0/strings/std2.6.1.smt2
+++ b/test/regress/regress0/strings/std2.6.1.smt2
@@ -3,7 +3,7 @@
 (set-logic QF_UFSLIA)
 (set-info :status sat)
 (declare-fun x () String)
-(assert (str.in-re x (str.to-re "A")))
+(assert (str.in_re x (str.to_re "A")))
 (declare-fun y () Int)
-(assert (= (str.to-int (str.from-int y)) y))
+(assert (= (str.to_int (str.from_int y)) y))
 (check-sat)