diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2018-03-26 08:52:40 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-03-26 08:52:40 -0700 |
commit | 11c698936c10321db68131eb95e8648a20051e3a (patch) | |
tree | f81a21dda693780d3211881448323ecc57f1bf3e /test/unit | |
parent | f7e0adeae28bae50632edef3ed2325df67a7ee7a (diff) |
Rewrites for substr of strings of length one (#1712)
This commit adds a rewrite for substrings of strings of length one to
the empty string if it can be shown that it is not possible that the
start position and the length are both greater than zero:
```
(str.substr "A" x y) --> "" if x = 0 |= 0 >= y
```
The commit introduces a set of functions to check such entailments
with assumptions.
Diffstat (limited to 'test/unit')
-rw-r--r-- | test/unit/Makefile.am | 9 | ||||
-rw-r--r-- | test/unit/theory/theory_strings_rewriter_white.h | 136 |
2 files changed, 141 insertions, 4 deletions
diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am index 3d5f2702d..b445583ac 100644 --- a/test/unit/Makefile.am +++ b/test/unit/Makefile.am @@ -7,14 +7,15 @@ UNIT_TESTS = \ if WHITE_AND_BLACK_TESTS UNIT_TESTS += \ theory/logic_info_white \ - theory/theory_engine_white \ - theory/theory_black \ - theory/theory_white \ theory/theory_arith_white \ - theory/theory_bv_white \ + theory/theory_black \ theory/theory_bv_bvgauss_white \ + theory/theory_bv_white \ + theory/theory_engine_white \ theory/theory_quantifiers_bv_instantiator_white \ theory/theory_quantifiers_bv_inverter_white \ + theory/theory_strings_rewriter_white \ + theory/theory_white \ theory/type_enumerator_white \ expr/node_white \ expr/node_black \ diff --git a/test/unit/theory/theory_strings_rewriter_white.h b/test/unit/theory/theory_strings_rewriter_white.h new file mode 100644 index 000000000..a1e878f6e --- /dev/null +++ b/test/unit/theory/theory_strings_rewriter_white.h @@ -0,0 +1,136 @@ +/********************* */ +/*! \file theory_strings_rewriter_white.h + ** \verbatim + ** Top contributors (to current version): + ** Andres Noetzli + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Unit tests for the strings rewriter + ** + ** Unit tests for the strings rewriter. + **/ + +#include "expr/node.h" +#include "expr/node_manager.h" +#include "smt/smt_engine.h" +#include "smt/smt_engine_scope.h" +#include "theory/rewriter.h" +#include "theory/strings/theory_strings_rewriter.h" + +#include <cxxtest/TestSuite.h> +#include <vector> + +using namespace CVC4; +using namespace CVC4::smt; +using namespace CVC4::theory; +using namespace CVC4::theory::strings; + +class TheoryStringsRewriterWhite : public CxxTest::TestSuite +{ + ExprManager *d_em; + NodeManager *d_nm; + SmtEngine *d_smt; + SmtScope *d_scope; + + public: + TheoryStringsRewriterWhite() {} + + void setUp() + { + Options opts; + opts.setOutputLanguage(language::output::LANG_SMTLIB_V2); + d_em = new ExprManager(opts); + d_nm = NodeManager::fromExprManager(d_em); + d_smt = new SmtEngine(d_em); + d_scope = new SmtScope(d_smt); + } + + void tearDown() + { + delete d_scope; + delete d_smt; + delete d_em; + } + + void testCheckEntailArithWithAssumption() + { + TypeNode intType = d_nm->integerType(); + TypeNode strType = d_nm->stringType(); + + Node x = d_nm->mkVar("x", intType); + Node y = d_nm->mkVar("y", strType); + Node z = d_nm->mkVar("z", intType); + + Node zero = d_nm->mkConst(Rational(0)); + + Node slen_y = d_nm->mkNode(kind::STRING_LENGTH, y); + Node x_plus_slen_y = d_nm->mkNode(kind::PLUS, x, slen_y); + Node x_plus_slen_y_eq_zero = + Rewriter::rewrite(d_nm->mkNode(kind::EQUAL, x_plus_slen_y, zero)); + + // x + (str.len y) = 0 /\ 0 >= x --> true + TS_ASSERT(TheoryStringsRewriter::checkEntailArithWithAssumption( + x_plus_slen_y_eq_zero, zero, x, false)); + + // x + (str.len y) = 0 /\ 0 > x --> false + TS_ASSERT(!TheoryStringsRewriter::checkEntailArithWithAssumption( + x_plus_slen_y_eq_zero, zero, x, true)); + + Node x_plus_slen_y_plus_z_eq_zero = Rewriter::rewrite(d_nm->mkNode( + kind::EQUAL, d_nm->mkNode(kind::PLUS, x_plus_slen_y, z), zero)); + + // x + (str.len y) + z = 0 /\ 0 > x --> false + TS_ASSERT(!TheoryStringsRewriter::checkEntailArithWithAssumption( + x_plus_slen_y_plus_z_eq_zero, zero, x, true)); + + Node x_plus_slen_y_plus_slen_y_eq_zero = Rewriter::rewrite(d_nm->mkNode( + kind::EQUAL, d_nm->mkNode(kind::PLUS, x_plus_slen_y, slen_y), zero)); + + // x + (str.len y) + (str.len y) = 0 /\ 0 >= x --> true + TS_ASSERT(TheoryStringsRewriter::checkEntailArithWithAssumption( + x_plus_slen_y_plus_slen_y_eq_zero, zero, x, false)); + } + + void testRewriteSubstr() + { + 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 s = d_nm->mkVar("s", strType); + Node x = d_nm->mkVar("x", intType); + Node y = d_nm->mkVar("y", intType); + + // (str.substr "A" x x) --> "" + Node n = d_nm->mkNode(kind::STRING_SUBSTR, a, x, x); + Node res = TheoryStringsRewriter::rewriteSubstr(n); + TS_ASSERT_EQUALS(res, empty); + + // (str.substr "A" (+ x 1) x) -> "" + n = d_nm->mkNode(kind::STRING_SUBSTR, + a, + d_nm->mkNode(kind::PLUS, x, d_nm->mkConst(Rational(1))), + x); + res = TheoryStringsRewriter::rewriteSubstr(n); + TS_ASSERT_EQUALS(res, empty); + + // (str.substr "A" (+ x (str.len s2)) x) -> "" + n = d_nm->mkNode( + kind::STRING_SUBSTR, + a, + d_nm->mkNode(kind::PLUS, x, d_nm->mkNode(kind::STRING_LENGTH, s)), + x); + res = TheoryStringsRewriter::rewriteSubstr(n); + TS_ASSERT_EQUALS(res, empty); + + // (str.substr "A" x y) -> (str.substr "A" x y) + n = d_nm->mkNode(kind::STRING_SUBSTR, a, x, y); + res = TheoryStringsRewriter::rewriteSubstr(n); + TS_ASSERT_EQUALS(res, n); + } +}; |