From 11c698936c10321db68131eb95e8648a20051e3a Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Mon, 26 Mar 2018 08:52:40 -0700 Subject: 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. --- test/unit/Makefile.am | 9 +- test/unit/theory/theory_strings_rewriter_white.h | 136 +++++++++++++++++++++++ 2 files changed, 141 insertions(+), 4 deletions(-) create mode 100644 test/unit/theory/theory_strings_rewriter_white.h (limited to 'test/unit') 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 +#include + +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); + } +}; -- cgit v1.2.3