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.
#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 {
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)
{
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<SkolemId, Node>::iterator it = d_skolemCache[a][b].find(id);
if (it == d_skolemCache[a][b].end())
{
return d_allSkolems.find(n) != d_allSkolems.end();
}
+std::tuple<SkolemCache::SkolemId, Node, Node>
+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
#define __CVC4__THEORY__STRINGS__SKOLEM_CACHE_H
#include <map>
+#include <tuple>
#include <unordered_set>
+
#include "expr/node.h"
namespace CVC4 {
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<SkolemId, Node, Node> 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<Node, std::map<Node, std::map<SkolemId, Node> > > d_skolemCache;
/** the set of all skolems we have generated */
+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)
--- /dev/null
+/********************* */
+/*! \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 <cxxtest/TestSuite.h>
+
+#include <memory>
+
+#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<NodeManager> d_nm;
+ std::unique_ptr<NodeManagerScope> d_scope;
+};
projects / cvc5.git / commitdiff