diff options
Diffstat (limited to 'test')
-rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
-rw-r--r-- | test/regress/Makefile.tests | 1 | ||||
-rw-r--r-- | test/regress/regress2/strings/non_termination_regular_expression6.smt2 | 61 | ||||
-rw-r--r-- | test/unit/theory/theory_strings_rewriter_white.h | 40 |
4 files changed, 100 insertions, 3 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index a7b7532f1..bfcd640b9 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1710,6 +1710,7 @@ set(regress_2_tests regress2/strings/cmu-disagree-0707-dd.smt2 regress2/strings/cmu-prereg-fmf.smt2 regress2/strings/cmu-repl-len-nterm.smt2 + regress2/strings/non_termination_regular_expression6.smt2 regress2/strings/norn-dis-0707-3.smt2 regress2/strings/repl-repl.smt2 regress2/sygus/MPwL_d1s3.sy diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests index 523650926..fc080f0e0 100644 --- a/test/regress/Makefile.tests +++ b/test/regress/Makefile.tests @@ -1703,6 +1703,7 @@ REG2_TESTS = \ regress2/strings/cmu-disagree-0707-dd.smt2 \ regress2/strings/cmu-prereg-fmf.smt2 \ regress2/strings/cmu-repl-len-nterm.smt2 \ + regress2/strings/non_termination_regular_expression6.smt2 \ regress2/strings/norn-dis-0707-3.smt2 \ regress2/strings/repl-repl.smt2 \ regress2/sygus/MPwL_d1s3.sy \ diff --git a/test/regress/regress2/strings/non_termination_regular_expression6.smt2 b/test/regress/regress2/strings/non_termination_regular_expression6.smt2 new file mode 100644 index 000000000..340cade1c --- /dev/null +++ b/test/regress/regress2/strings/non_termination_regular_expression6.smt2 @@ -0,0 +1,61 @@ +; COMMAND-LINE: --strings-exp --re-elim +; EXPECT: unsat +(set-logic ALL) +(set-info :status unsat) +(declare-const actionName String) +(declare-const actionNamespace String) +(declare-const resource_account String) +(declare-const resource_partition String) +(declare-const resource_prefix String) +(declare-const resource_region String) +(declare-const resource_resource String) +(declare-const resource_service String) + +; Action: p0.0 +(declare-const p0.0.action Bool) +(assert (= p0.0.action (and (= "sqs" actionNamespace) (= "sendmessage" actionName)))) + +; Resource: p0.0 +(declare-const p0.0.resource Bool) +(assert (= p0.0.resource (and (= resource_prefix "arn") (= resource_partition "aws") (= resource_service "sqs") (= resource_region "us-east-1") (= resource_account "111144448888") (str.in.re resource_resource (re.++ (str.to.re "ab") (re.* re.allchar) (str.to.re "b") (re.* re.allchar) (str.to.re "b") (re.* re.allchar) (str.to.re "b")))))) + +; Statement: p0.0 +(declare-const p0.0.statement.allows Bool) +(assert (= p0.0.statement.allows (and p0.0.action p0.0.resource))) + +; Policy: 0 +(declare-const p0.denies Bool) +(assert (not p0.denies)) +(declare-const p0.allows Bool) +(assert (= p0.allows (and (not p0.denies) p0.0.statement.allows))) +(declare-const p0.neutral Bool) +(assert (= p0.neutral (and (not p0.allows) (not p0.denies)))) + +; Action: p1.0 +(declare-const p1.0.action Bool) +(assert (= p1.0.action (and (= "sqs" actionNamespace) (= "sendmessage" actionName)))) + +; Resource: p1.0 +(declare-const p1.0.resource Bool) +(assert (= p1.0.resource (and (= resource_prefix "arn") (= resource_partition "aws") (= resource_service "sqs") (= resource_region "us-east-1") (= resource_account "111144448888") (str.in.re resource_resource (re.++ (str.to.re "a") (re.* re.allchar) (str.to.re "b") (re.* re.allchar) (str.to.re "b") (re.* re.allchar) (str.to.re "b")))))) + +; Statement: p1.0 +(declare-const p1.0.statement.allows Bool) +(assert (= p1.0.statement.allows (and p1.0.action p1.0.resource))) + +; Policy: 1 +(declare-const p1.denies Bool) +(assert (not p1.denies)) +(declare-const p1.allows Bool) +(assert (= p1.allows (and (not p1.denies) p1.0.statement.allows))) +(declare-const p1.neutral Bool) +(assert (= p1.neutral (and (not p1.allows) (not p1.denies)))) + +; Resource service invariant +(assert (not (str.contains resource_service ":"))) +(assert (= resource_prefix "arn")) + +; Goals +(assert p0.allows) +(assert (or p1.denies p1.neutral)) +(check-sat) diff --git a/test/unit/theory/theory_strings_rewriter_white.h b/test/unit/theory/theory_strings_rewriter_white.h index d038b310e..d967ab793 100644 --- a/test/unit/theory/theory_strings_rewriter_white.h +++ b/test/unit/theory/theory_strings_rewriter_white.h @@ -152,7 +152,9 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite Node empty = d_nm->mkConst(::CVC4::String("")); Node a = d_nm->mkConst(::CVC4::String("A")); + Node b = d_nm->mkConst(::CVC4::String("B")); Node abcd = d_nm->mkConst(::CVC4::String("ABCD")); + Node zero = d_nm->mkConst(Rational(0)); Node two = d_nm->mkConst(Rational(2)); Node three = d_nm->mkConst(Rational(3)); @@ -198,6 +200,26 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite kind::STRING_SUBSTR, abcd, d_nm->mkNode(kind::PLUS, x, two), x); res = TheoryStringsRewriter::rewriteSubstr(n); TS_ASSERT_EQUALS(res, n); + + // (str.substr (str.substr s x x) x x) -> "" + n = d_nm->mkNode( + kind::STRING_SUBSTR, d_nm->mkNode(kind::STRING_SUBSTR, s, x, x), x, x); + sameNormalForm(n, empty); + + // Same normal form for: + // + // (str.substr (str.replace "" s "B") x x) + // + // (str.replace "" s (str.substr "B" x x))) + Node lhs = d_nm->mkNode(kind::STRING_SUBSTR, + d_nm->mkNode(kind::STRING_STRREPL, empty, s, b), + x, + x); + Node rhs = d_nm->mkNode(kind::STRING_STRREPL, + empty, + s, + d_nm->mkNode(kind::STRING_SUBSTR, b, x, x)); + sameNormalForm(lhs, rhs); } void testRewriteConcat() @@ -297,6 +319,7 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite void testRewriteIndexOf() { + TypeNode intType = d_nm->integerType(); TypeNode strType = d_nm->stringType(); Node a = d_nm->mkConst(::CVC4::String("A")); @@ -305,17 +328,20 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite Node b = d_nm->mkConst(::CVC4::String("B")); Node x = d_nm->mkVar("x", strType); Node y = d_nm->mkVar("y", strType); - Node one = d_nm->mkConst(Rational(2)); + Node negOne = d_nm->mkConst(Rational(-1)); + Node one = d_nm->mkConst(Rational(1)); + Node two = d_nm->mkConst(Rational(2)); Node three = d_nm->mkConst(Rational(3)); + Node i = d_nm->mkVar("i", intType); // Same normal form for: // // (str.to.int (str.indexof "A" x 1)) // // (str.to.int (str.indexof "B" x 1)) - Node a_idof_x = d_nm->mkNode(kind::STRING_STRIDOF, a, x, one); + Node a_idof_x = d_nm->mkNode(kind::STRING_STRIDOF, a, x, two); Node itos_a_idof_x = d_nm->mkNode(kind::STRING_ITOS, a_idof_x); - Node b_idof_x = d_nm->mkNode(kind::STRING_STRIDOF, b, x, one); + Node b_idof_x = d_nm->mkNode(kind::STRING_STRIDOF, b, x, two); Node itos_b_idof_x = d_nm->mkNode(kind::STRING_ITOS, b_idof_x); sameNormalForm(itos_a_idof_x, itos_b_idof_x); @@ -333,6 +359,14 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite y, three); sameNormalForm(idof_abcd, idof_aaad); + + // (str.indexof (str.substr x 1 i) "A" i) ---> -1 + Node idof_substr = + d_nm->mkNode(kind::STRING_STRIDOF, + d_nm->mkNode(kind::STRING_SUBSTR, x, one, i), + a, + i); + sameNormalForm(idof_substr, negOne); } void testRewriteReplace() |