From: Andres Noetzli Date: Wed, 28 Nov 2018 20:33:55 +0000 (-0800) Subject: Improve skolem caching by normalizing skolem args (#2723) X-Git-Tag: cvc5-1.0.0~4346 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=eef3d0d658aed64e8014c28eae5841eed298139a;p=cvc5.git Improve skolem caching by normalizing skolem args (#2723) In certain cases, we can share skolems between similar reductions, e.g. `(str.replace x y z)` and `(str.replace (str.substr x 0 n) y z)` because the first occurrence of `y` in `x` has to be the first occurrence of `y` in `(str.substr x 0 n)` (assuming that `y` appears in both, otherwise the value of the skolems does not matter). This commit adds a helper function in the skolem cache that does some of those simplifications. --- diff --git a/src/theory/strings/skolem_cache.cpp b/src/theory/strings/skolem_cache.cpp index 7725b1b0d..b6604d6e0 100644 --- a/src/theory/strings/skolem_cache.cpp +++ b/src/theory/strings/skolem_cache.cpp @@ -15,6 +15,8 @@ #include "theory/strings/skolem_cache.h" #include "theory/rewriter.h" +#include "theory/strings/theory_strings_rewriter.h" +#include "util/rational.h" namespace CVC4 { namespace theory { @@ -22,7 +24,9 @@ namespace strings { SkolemCache::SkolemCache() { - d_strType = NodeManager::currentNM()->stringType(); + NodeManager* nm = NodeManager::currentNM(); + d_strType = nm->stringType(); + d_zero = nm->mkConst(Rational(0)); } Node SkolemCache::mkSkolemCached(Node a, Node b, SkolemId id, const char* c) @@ -40,6 +44,12 @@ Node SkolemCache::mkTypedSkolemCached( { a = a.isNull() ? a : Rewriter::rewrite(a); b = b.isNull() ? b : Rewriter::rewrite(b); + + if (tn == d_strType) + { + std::tie(id, a, b) = normalizeStringSkolem(id, a, b); + } + std::map::iterator it = d_skolemCache[a][b].find(id); if (it == d_skolemCache[a][b].end()) { @@ -74,6 +84,43 @@ bool SkolemCache::isSkolem(Node n) const return d_allSkolems.find(n) != d_allSkolems.end(); } +std::tuple +SkolemCache::normalizeStringSkolem(SkolemId id, Node a, Node b) +{ + Trace("skolem-cache") << "normalizeStringSkolem start: (" << id << ", " << a + << ", " << b << ")" << std::endl; + + // SK_PURIFY(str.substr x 0 (str.indexof x y 0)) ---> SK_FIRST_CTN_PRE(x, y) + if (id == SK_PURIFY && a.getKind() == kind::STRING_SUBSTR) + { + Node s = a[0]; + Node n = a[1]; + Node m = a[2]; + if (m.getKind() == kind::STRING_STRIDOF && m[0] == s) + { + if (n == d_zero && m[2] == d_zero) + { + id = SK_FIRST_CTN_PRE; + a = m[0]; + b = m[1]; + } + } + } + + if (id == SK_FIRST_CTN_PRE) + { + // SK_FIRST_CTN_PRE((str.substr x 0 n), y) ---> SK_FIRST_CTN_PRE(x, y) + while (a.getKind() == kind::STRING_SUBSTR && a[1] == d_zero) + { + a = a[0]; + } + } + + Trace("skolem-cache") << "normalizeStringSkolem end: (" << id << ", " << a + << ", " << b << ")" << std::endl; + return std::make_tuple(id, a, b); +} + } // namespace strings } // namespace theory } // namespace CVC4 diff --git a/src/theory/strings/skolem_cache.h b/src/theory/strings/skolem_cache.h index d0eabd4c2..a6e91a246 100644 --- a/src/theory/strings/skolem_cache.h +++ b/src/theory/strings/skolem_cache.h @@ -18,7 +18,9 @@ #define __CVC4__THEORY__STRINGS__SKOLEM_CACHE_H #include +#include #include + #include "expr/node.h" namespace CVC4 { @@ -134,8 +136,28 @@ class SkolemCache bool isSkolem(Node n) const; private: + /** + * Simplifies the arguments for a string skolem used for indexing into the + * cache. In certain cases, we can share skolems with similar arguments e.g. + * SK_FIRST_CTN(a, c) can be used instead of SK_FIRST_CTN((str.substr a 0 n), + * c) because the first occurrence of "c" in "(str.substr a 0 n)" is also the + * first occurrence of "c" in "a" (assuming that "c" appears in both and + * otherwise the value of SK_FIRST_CTN does not matter). + * + * @param id The type of skolem + * @param a The first argument used for indexing + * @param b The second argument used for indexing + * @return A tuple with the new skolem id, the new first, and the new second + * argument + */ + std::tuple normalizeStringSkolem(SkolemId id, + Node a, + Node b); + /** string type */ TypeNode d_strType; + /** Constant node zero */ + Node d_zero; /** map from node pairs and identifiers to skolems */ std::map > > d_skolemCache; /** the set of all skolems we have generated */ diff --git a/test/unit/theory/CMakeLists.txt b/test/unit/theory/CMakeLists.txt index a5a67cfa2..3d29c4de1 100644 --- a/test/unit/theory/CMakeLists.txt +++ b/test/unit/theory/CMakeLists.txt @@ -1,11 +1,12 @@ +cvc4_add_unit_test_black(theory_black theory) cvc4_add_unit_test_white(evaluator_white theory) cvc4_add_unit_test_white(logic_info_white theory) cvc4_add_unit_test_white(theory_arith_white theory) -cvc4_add_unit_test_black(theory_black theory) cvc4_add_unit_test_white(theory_bv_white theory) cvc4_add_unit_test_white(theory_engine_white theory) cvc4_add_unit_test_white(theory_quantifiers_bv_instantiator_white theory) cvc4_add_unit_test_white(theory_quantifiers_bv_inverter_white theory) cvc4_add_unit_test_white(theory_strings_rewriter_white theory) +cvc4_add_unit_test_white(theory_strings_skolem_cache_black theory) cvc4_add_unit_test_white(theory_white theory) cvc4_add_unit_test_white(type_enumerator_white theory) diff --git a/test/unit/theory/theory_strings_skolem_cache_black.h b/test/unit/theory/theory_strings_skolem_cache_black.h new file mode 100644 index 000000000..aaf50f219 --- /dev/null +++ b/test/unit/theory/theory_strings_skolem_cache_black.h @@ -0,0 +1,92 @@ +/********************* */ +/*! \file theory_strings_skolem_cache_black.h + ** \verbatim + ** Top contributors (to current version): + ** Andres Noetzli + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2018 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 Black box testing of the skolem cache of the theory of strings. + **/ + +#include + +#include + +#include "expr/node.h" +#include "expr/node_manager.h" +#include "theory/strings/skolem_cache.h" +#include "util/rational.h" +#include "util/regexp.h" + +using namespace CVC4; +using namespace CVC4::theory::strings; + +class TheoryStringsSkolemCacheBlack : public CxxTest::TestSuite +{ + public: + void setUp() override + { + d_nm.reset(new NodeManager(nullptr)); + d_scope.reset(new NodeManagerScope(d_nm.get())); + } + + void tearDown() override {} + + void testMkSkolemCached() + { + Node zero = d_nm->mkConst(Rational(0)); + Node n = d_nm->mkSkolem("n", d_nm->integerType()); + Node a = d_nm->mkSkolem("a", d_nm->stringType()); + Node b = d_nm->mkSkolem("b", d_nm->stringType()); + Node c = d_nm->mkSkolem("c", d_nm->stringType()); + Node d = d_nm->mkSkolem("d", d_nm->stringType()); + Node sa = d_nm->mkNode(kind::STRING_SUBSTR, + a, + zero, + d_nm->mkNode(kind::STRING_STRIDOF, a, b, zero)); + Node sc = d_nm->mkNode(kind::STRING_SUBSTR, c, zero, n); + + SkolemCache sk; + + // Check that skolems are shared between: + // + // SK_FIRST_CTN(a, b) + // + // SK_FIRST_CTN(a, b) + { + Node s1 = sk.mkSkolemCached(a, b, SkolemCache::SK_FIRST_CTN_PRE, "foo"); + Node s2 = sk.mkSkolemCached(a, b, SkolemCache::SK_FIRST_CTN_PRE, "foo"); + TS_ASSERT_EQUALS(s1, s2); + } + + // Check that skolems are shared between: + // + // SK_FIRST_CTN(c, b) + // + // SK_FIRST_CTN((str.substr c), b) + { + Node s1 = sk.mkSkolemCached(c, b, SkolemCache::SK_FIRST_CTN_PRE, "foo"); + Node s2 = sk.mkSkolemCached(sc, b, SkolemCache::SK_FIRST_CTN_PRE, "foo"); + TS_ASSERT_EQUALS(s1, s2); + } + + // Check that skolems are shared between: + // + // SK_PURIFY((str.substr a 0 (str.indexof a b 0))) + // + // SK_FIRST_CTN(a, b) + { + Node s1 = sk.mkSkolemCached(sa, b, SkolemCache::SK_PURIFY, "foo"); + Node s2 = sk.mkSkolemCached(a, b, SkolemCache::SK_FIRST_CTN_PRE, "foo"); + TS_ASSERT_EQUALS(s1, s2); + } + } + + private: + std::unique_ptr d_nm; + std::unique_ptr d_scope; +};