diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2020-01-17 18:14:04 -0800 |
---|---|---|
committer | Andres Noetzli <andres.noetzli@gmail.com> | 2020-01-17 18:14:04 -0800 |
commit | 6e43379a400ed9e5993c285d180a2f824fc9f130 (patch) | |
tree | ac8b29d1ed79c6bd04b3e3afb816164f86e174c4 /src | |
parent | c3bc4ac99c36029b78d866ffb89bd0d322821f34 (diff) |
Use kinds instead of skolems
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/strings/kinds | 6 | ||||
-rw-r--r-- | src/theory/strings/skolem_cache.cpp | 11 | ||||
-rw-r--r-- | src/theory/strings/theory_strings.cpp | 15 | ||||
-rw-r--r-- | src/theory/strings/theory_strings.h | 2 | ||||
-rw-r--r-- | src/theory/strings/theory_strings_rewriter.cpp | 45 |
5 files changed, 79 insertions, 0 deletions
diff --git a/src/theory/strings/kinds b/src/theory/strings/kinds index aa1e2627a..cd8550905 100644 --- a/src/theory/strings/kinds +++ b/src/theory/strings/kinds @@ -31,6 +31,9 @@ operator STRING_CODE 1 "string to code, returns the code of the first character operator STRING_TOLOWER 1 "string to lowercase conversion" operator STRING_TOUPPER 1 "string to uppercase conversion" operator STRING_REV 1 "string reverse" +operator STRING_SK_PREFIX 2 "string prefix" +operator STRING_SK_SUFFIX 2 "string suffix" +operator STRING_SK_FIRST_CTN_PRE 2 "string suffix" sort STRING_TYPE \ Cardinality::INTEGERS \ @@ -106,6 +109,9 @@ typerule STRING_CODE "SimpleTypeRule<RInteger, AString>" typerule STRING_TOUPPER "SimpleTypeRule<RString, AString>" typerule STRING_TOLOWER "SimpleTypeRule<RString, AString>" typerule STRING_REV "SimpleTypeRule<RString, AString>" +typerule STRING_SK_PREFIX "SimpleTypeRule<RString, AString, AInteger>" +typerule STRING_SK_SUFFIX "SimpleTypeRule<RString, AString, AInteger>" +typerule STRING_SK_FIRST_CTN_PRE "SimpleTypeRule<RString, AString, AString>" typerule STRING_IN_REGEXP "SimpleTypeRule<RBool, AString, ARegExp>" diff --git a/src/theory/strings/skolem_cache.cpp b/src/theory/strings/skolem_cache.cpp index b4e1c74ea..327ae19e1 100644 --- a/src/theory/strings/skolem_cache.cpp +++ b/src/theory/strings/skolem_cache.cpp @@ -52,6 +52,17 @@ Node SkolemCache::mkTypedSkolemCached( std::tie(id, a, b) = normalizeStringSkolem(id, a, b); } + NodeManager* nm = NodeManager::currentNM(); + switch (id) + { + case SK_PREFIX: return nm->mkNode(STRING_SK_PREFIX, a, b); break; + case SK_SUFFIX_REM: return nm->mkNode(STRING_SK_SUFFIX, a, b); break; + case SK_FIRST_CTN_PRE: + return nm->mkNode(STRING_SK_FIRST_CTN_PRE, a, b); + break; + default: break; + } + std::map<SkolemId, Node>::iterator it = d_skolemCache[a][b].find(id); if (it == d_skolemCache[a][b].end()) { diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 1bc104096..2f658550f 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -130,6 +130,9 @@ TheoryStrings::TheoryStrings(context::Context* c, getExtTheory()->addFunctionKind(kind::STRING_TOLOWER); getExtTheory()->addFunctionKind(kind::STRING_TOUPPER); getExtTheory()->addFunctionKind(kind::STRING_REV); + getExtTheory()->addFunctionKind(kind::STRING_SK_PREFIX); + getExtTheory()->addFunctionKind(kind::STRING_SK_SUFFIX); + getExtTheory()->addFunctionKind(kind::STRING_SK_FIRST_CTN_PRE); // The kinds we are treating as function application in congruence d_equalityEngine.addFunctionKind(kind::STRING_LENGTH); @@ -149,6 +152,9 @@ TheoryStrings::TheoryStrings(context::Context* c, d_equalityEngine.addFunctionKind(kind::STRING_TOLOWER); d_equalityEngine.addFunctionKind(kind::STRING_TOUPPER); d_equalityEngine.addFunctionKind(kind::STRING_REV); + d_equalityEngine.addFunctionKind(kind::STRING_SK_PREFIX); + d_equalityEngine.addFunctionKind(kind::STRING_SK_SUFFIX); + d_equalityEngine.addFunctionKind(kind::STRING_SK_FIRST_CTN_PRE); d_zero = NodeManager::currentNM()->mkConst( Rational( 0 ) ); d_one = NodeManager::currentNM()->mkConst( Rational( 1 ) ); @@ -164,6 +170,15 @@ TheoryStrings::~TheoryStrings() { } +void TheoryStrings::finishInit() +{ + TheoryModel* tm = d_valuation.getModel(); + Assert(tm != nullptr); + tm->setSemiEvaluatedKind(STRING_SK_FIRST_CTN_PRE); + tm->setSemiEvaluatedKind(STRING_SK_SUFFIX); + tm->setSemiEvaluatedKind(STRING_SK_PREFIX); +} + bool TheoryStrings::areCareDisequal( TNode x, TNode y ) { Assert(d_equalityEngine.hasTerm(x)); Assert(d_equalityEngine.hasTerm(y)); diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index 8e2af8434..4ce83704e 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -102,6 +102,8 @@ class TheoryStrings : public Theory { const LogicInfo& logicInfo); ~TheoryStrings(); + void finishInit() override; + void setMasterEqualityEngine(eq::EqualityEngine* eq) override; std::string identify() const override { return std::string("TheoryStrings"); } diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp index f17944027..0f6ec03d2 100644 --- a/src/theory/strings/theory_strings_rewriter.cpp +++ b/src/theory/strings/theory_strings_rewriter.cpp @@ -1563,6 +1563,51 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) { { retNode = rewriteConcat(node); } + else if (nk == STRING_SK_PREFIX) + { + if (node[0].isConst() && node[1].isConst()) + { + String s = node[0].getConst<String>(); + size_t n = node[1].getConst<Rational>().getNumerator().toUnsignedInt(); + if (s.size() >= n) + { + retNode = nm->mkConst(s.prefix(n)); + } + } + else if (node[1].getKind() == STRING_LENGTH && node[0] == node[1][0]) + { + retNode = node[0]; + } + } + else if (nk == STRING_SK_SUFFIX) + { + if (node[0].isConst() && node[1].isConst()) + { + String s = node[0].getConst<String>(); + size_t n = node[1].getConst<Rational>().getNumerator().toUnsignedInt(); + if (s.size() >= n) + { + retNode = nm->mkConst(s.suffix(s.size() - n)); + } + } + else if (node[1].getKind() == STRING_LENGTH && node[0] == node[1][0]) + { + retNode = nm->mkConst(String()); + } + } + else if (nk == STRING_SK_FIRST_CTN_PRE) + { + if (node[0].isConst() && node[1].isConst()) + { + String s1 = node[0].getConst<String>(); + String s2 = node[1].getConst<String>(); + size_t pos = s1.find(s2); + if (pos != std::string::npos) + { + retNode = nm->mkConst(s1.prefix(pos)); + } + } + } else if (nk == kind::EQUAL) { retNode = rewriteEquality(node); |