summaryrefslogtreecommitdiff
path: root/test
diff options
context:
space:
mode:
Diffstat (limited to 'test')
-rw-r--r--test/regress/CMakeLists.txt1
-rw-r--r--test/regress/Makefile.tests1
-rw-r--r--test/regress/regress2/strings/non_termination_regular_expression6.smt261
-rw-r--r--test/unit/theory/theory_strings_rewriter_white.h40
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()
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback