summaryrefslogtreecommitdiff
path: root/test
diff options
context:
space:
mode:
authorAndres Noetzli <andres.noetzli@gmail.com>2019-02-05 10:09:15 -0800
committerAndrew Reynolds <andrew.j.reynolds@gmail.com>2019-02-05 12:09:15 -0600
commit104b28b4c16b90a819c8f79d60f94a42fb0c0261 (patch)
tree3e2f508eadc02ccb7d2e6d20a25cbda15f413224 /test
parentb396d78982e109dc642611d32578bbca82b210cd (diff)
Make stripConstantEndpoints() less aggressive (#2830)
Diffstat (limited to 'test')
-rw-r--r--test/unit/theory/theory_strings_rewriter_white.h32
1 files changed, 31 insertions, 1 deletions
diff --git a/test/unit/theory/theory_strings_rewriter_white.h b/test/unit/theory/theory_strings_rewriter_white.h
index 191d0ba58..c5d20daef 100644
--- a/test/unit/theory/theory_strings_rewriter_white.h
+++ b/test/unit/theory/theory_strings_rewriter_white.h
@@ -1220,15 +1220,33 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite
d_nm->mkNode(kind::STRING_CONCAT, x, b));
sameNormalForm(eq, f);
}
+
+ {
+ // (= (str.++ "A" (int.to.str n)) "A") -/-> false
+ Node eq = d_nm->mkNode(
+ kind::EQUAL,
+ d_nm->mkNode(
+ kind::STRING_CONCAT, a, d_nm->mkNode(kind::STRING_ITOS, n)),
+ a);
+ differentNormalForms(eq, f);
+ }
}
void testStripConstantEndpoints()
{
+ TypeNode intType = d_nm->integerType();
+ TypeNode strType = d_nm->stringType();
+
Node empty = d_nm->mkConst(::CVC4::String(""));
Node a = d_nm->mkConst(::CVC4::String("A"));
+ Node ab = d_nm->mkConst(::CVC4::String("AB"));
+ Node cd = d_nm->mkConst(::CVC4::String("CD"));
+ Node x = d_nm->mkVar("x", strType);
+ Node y = d_nm->mkVar("y", strType);
+ Node n = d_nm->mkVar("n", intType);
{
- // stripConstantEndpoints({ "" }, { "a" }, {}, {}, 0) ---> false
+ // stripConstantEndpoints({ "" }, { "A" }, {}, {}, 0) ---> false
std::vector<Node> n1 = {empty};
std::vector<Node> n2 = {a};
std::vector<Node> nb;
@@ -1237,6 +1255,18 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite
TheoryStringsRewriter::stripConstantEndpoints(n1, n2, nb, ne, 0);
TS_ASSERT(!res);
}
+
+ {
+ // stripConstantEndpoints({ "A" }, { "A". (int.to.str n) }, {}, {}, 0)
+ // ---> false
+ std::vector<Node> n1 = {a};
+ std::vector<Node> n2 = {a, d_nm->mkNode(kind::STRING_ITOS, n)};
+ std::vector<Node> nb;
+ std::vector<Node> ne;
+ bool res =
+ TheoryStringsRewriter::stripConstantEndpoints(n1, n2, nb, ne, 0);
+ TS_ASSERT(!res);
+ }
}
private:
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback