From 18eb247c3f14761dc0e1981d4faf11833f069b9d Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 21 Feb 2020 13:36:01 -0600 Subject: [PATCH] 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. --- src/parser/smt2/smt2.cpp | 23 +++++++++++++------ test/regress/CMakeLists.txt | 2 ++ test/regress/regress0/strings/code-eval.smt2 | 10 ++++++++ test/regress/regress0/strings/code-perf.smt2 | 1 + .../regress0/strings/code-sat-neg-one.smt2 | 1 + test/regress/regress0/strings/re-syntax.smt2 | 9 ++++++++ .../regress0/strings/replaceall-eval.smt2 | 7 +++--- test/regress/regress0/strings/std2.6.1.smt2 | 4 ++-- 8 files changed, 45 insertions(+), 12 deletions(-) create mode 100644 test/regress/regress0/strings/code-eval.smt2 create mode 100644 test/regress/regress0/strings/re-syntax.smt2 diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 11dedb259..a7033b277 100644 --- 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 159f87037..d61203ac2 100644 --- 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 index 000000000..faa5c174c --- /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 39cab48ce..4d7e22bd3 100644 --- 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 c69276a4f..403319d02 100644 --- 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 index 000000000..4c25a65a4 --- /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 924515901..c118a7dc4 100644 --- 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 3302a29e5..d30cfc83c 100644 --- 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) -- 2.30.2