summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/theory/strings/kinds4
-rw-r--r--src/theory/strings/theory_strings.cpp15
-rw-r--r--src/theory/strings/theory_strings.h2
-rw-r--r--src/theory/strings/theory_strings_preprocess.cpp9
-rw-r--r--src/theory/strings/theory_strings_rewriter.cpp61
-rw-r--r--src/theory/strings/theory_strings_type_rules.h60
6 files changed, 148 insertions, 3 deletions
diff --git a/src/theory/strings/kinds b/src/theory/strings/kinds
index df6085422..9629f0a8a 100644
--- a/src/theory/strings/kinds
+++ b/src/theory/strings/kinds
@@ -28,6 +28,8 @@ operator STRING_SUFFIX 2 "string suffixof"
operator STRING_ITOS 1 "integer to string"
operator STRING_STOI 1 "string to integer (total function)"
operator STRING_CODE 1 "string to code, returns the code of the first character of the string if it has length one, -1 otherwise"
+operator STRING_FST_OCC_PRE 2 "string prefixof"
+operator STRING_FST_OCC_POST 2 "string suffixof"
sort STRING_TYPE \
Cardinality::INTEGERS \
@@ -100,6 +102,8 @@ typerule STRING_SUFFIX ::CVC4::theory::strings::StringSuffixOfTypeRule
typerule STRING_ITOS ::CVC4::theory::strings::StringIntToStrTypeRule
typerule STRING_STOI ::CVC4::theory::strings::StringStrToIntTypeRule
typerule STRING_CODE ::CVC4::theory::strings::StringStrToIntTypeRule
+typerule STRING_FST_OCC_PRE ::CVC4::theory::strings::StringFstOccPreTypeRule
+typerule STRING_FST_OCC_POST ::CVC4::theory::strings::StringFstOccPostTypeRule
typerule STRING_IN_REGEXP ::CVC4::theory::strings::StringInRegExpTypeRule
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 5179ddab3..88fc3e36d 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -154,6 +154,8 @@ TheoryStrings::TheoryStrings(context::Context* c,
d_equalityEngine.addFunctionKind(kind::STRING_CONCAT);
d_equalityEngine.addFunctionKind(kind::STRING_IN_REGEXP);
d_equalityEngine.addFunctionKind(kind::STRING_CODE);
+ d_equalityEngine.addFunctionKind(kind::STRING_FST_OCC_PRE);
+ d_equalityEngine.addFunctionKind(kind::STRING_FST_OCC_POST);
if( options::stringLazyPreproc() ){
d_equalityEngine.addFunctionKind(kind::STRING_STRCTN);
d_equalityEngine.addFunctionKind(kind::STRING_LEQ);
@@ -262,6 +264,14 @@ void TheoryStrings::setMasterEqualityEngine(eq::EqualityEngine* eq) {
d_equalityEngine.setMasterEqualityEngine(eq);
}
+void TheoryStrings::finishInit()
+{
+ TheoryModel* tm = d_valuation.getModel();
+ Assert(tm != nullptr);
+ tm->setSemiEvaluatedKind(kind::STRING_FST_OCC_PRE);
+ tm->setSemiEvaluatedKind(kind::STRING_FST_OCC_POST);
+}
+
void TheoryStrings::addSharedTerm(TNode t) {
Debug("strings") << "TheoryStrings::addSharedTerm(): "
<< t << " " << t.getType().isBoolean() << endl;
@@ -480,6 +490,7 @@ bool TheoryStrings::doReduction(int effort, Node n, bool& isCd)
<< "Process reduction for " << n << ", pol = " << pol << std::endl;
if (k == STRING_STRCTN && pol == 1)
{
+ NodeManager* nm = NodeManager::currentNM();
Node x = n[0];
Node s = n[1];
// positive contains reduces to a equality
@@ -487,7 +498,9 @@ bool TheoryStrings::doReduction(int effort, Node n, bool& isCd)
d_sk_cache.mkSkolemCached(x, s, SkolemCache::SK_FIRST_CTN_PRE, "sc1");
Node sk2 =
d_sk_cache.mkSkolemCached(x, s, SkolemCache::SK_FIRST_CTN_POST, "sc2");
- Node eq = Rewriter::rewrite(x.eqNode(mkConcat(sk1, s, sk2)));
+ Node sk1EqPre = sk1.eqNode(nm->mkNode(kind::STRING_FST_OCC_PRE, x, s));
+ Node sk2EqPost = sk2.eqNode(nm->mkNode(kind::STRING_FST_OCC_POST, x, s));
+ Node eq = Rewriter::rewrite(nm->mkNode(AND, x.eqNode(mkConcat(sk1, s, sk2)), sk1EqPre, sk2EqPost));
std::vector<Node> exp_vec;
exp_vec.push_back(n);
sendInference(d_empty_vec, exp_vec, eq, "POS-CTN", true);
diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h
index aa86f1bc1..8aa9bea6b 100644
--- a/src/theory/strings/theory_strings.h
+++ b/src/theory/strings/theory_strings.h
@@ -147,6 +147,8 @@ class TheoryStrings : public Theory {
void setMasterEqualityEngine(eq::EqualityEngine* eq) override;
+ void finishInit() override;
+
std::string identify() const override { return std::string("TheoryStrings"); }
public:
diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp
index d095d6801..8ee9e3afa 100644
--- a/src/theory/strings/theory_strings_preprocess.cpp
+++ b/src/theory/strings/theory_strings_preprocess.cpp
@@ -170,8 +170,10 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
// ~contains( str.++( io2, substr( y, 0, len( y ) - 1) ), y ) ^
// skk = n + len( io2 )
// for fresh io2, io4.
+ Node io2EqPre = io2.eqNode(nm->mkNode(kind::STRING_FST_OCC_PRE, Rewriter::rewrite(st), Rewriter::rewrite(y)));
+ Node io4EqPost = io4.eqNode(nm->mkNode(kind::STRING_FST_OCC_POST, Rewriter::rewrite(st), Rewriter::rewrite(y)));
Node rr = nm->mkNode(ITE, cond1, cc1, nm->mkNode(ITE, cond2, cc2, cc3));
- new_nodes.push_back( rr );
+ new_nodes.push_back(nm->mkNode(AND, rr, io2EqPre, io4EqPost));
// Thus, indexof( x, y, n ) = skk.
retNode = skk;
@@ -390,6 +392,9 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
y)
.negate();
+ Node rp1EqPre = rp1.eqNode(nm->mkNode(kind::STRING_FST_OCC_PRE, Rewriter::rewrite(x), Rewriter::rewrite(y)));
+ Node rp2EqPost = rp2.eqNode(nm->mkNode(kind::STRING_FST_OCC_POST, Rewriter::rewrite(x), Rewriter::rewrite(y)));
+
// assert:
// IF y=""
// THEN: rpw = str.++( z, x )
@@ -406,7 +411,7 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
cond2,
nm->mkNode(kind::AND, c21, c22, c23),
rpw.eqNode(x)));
- new_nodes.push_back( rr );
+ new_nodes.push_back( nm->mkNode(AND, rr, rp1EqPre, rp2EqPost) );
// Thus, replace( x, y, z ) = rpw.
retNode = rpw;
diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index 57a99532e..0841eb810 100644
--- a/src/theory/strings/theory_strings_rewriter.cpp
+++ b/src/theory/strings/theory_strings_rewriter.cpp
@@ -1497,6 +1497,59 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) {
}
}
}
+ else if (nk == kind::STRING_FST_OCC_PRE)
+ {
+ Node empty = nm->mkConst(String(""));
+ if (node[0] == node[1])
+ {
+ retNode = empty;
+ }
+ else if (node[1].isConst())
+ {
+ if (node[1] == empty)
+ {
+ retNode = empty;
+ }
+ else if (node[0].isConst())
+ {
+ String x = node[0].getConst<String>();
+ String y = node[1].getConst<String>();
+
+ size_t i = x.find(y);
+ if (i != std::string::npos)
+ {
+ retNode = nm->mkConst(x.substr(0, i));
+ }
+ }
+ }
+ }
+ else if (nk == kind::STRING_FST_OCC_POST)
+ {
+ Node empty = nm->mkConst(String(""));
+ if (node[0] == node[1])
+ {
+ retNode = empty;
+ }
+ else if (node[1].isConst())
+ {
+ if (node[1] == empty)
+ {
+ retNode = node[0];
+ }
+ else if (node[0].isConst())
+ {
+ String x = node[0].getConst<String>();
+ String y = node[1].getConst<String>();
+
+ size_t i = x.find(y);
+ if (i != std::string::npos)
+ {
+ retNode =
+ nm->mkConst(x.substr(i + y.size(), x.size() - i - y.size()));
+ }
+ }
+ }
+ }
else if (nk == kind::STRING_IN_REGEXP)
{
retNode = rewriteMembership(node);
@@ -2224,6 +2277,14 @@ Node TheoryStringsRewriter::rewriteContains( Node node ) {
}
}
}
+ else if (node[0].getKind() == kind::STRING_FST_OCC_PRE)
+ {
+ if (node[0][1] == node[1])
+ {
+ Node ret = nm->mkConst(false);
+ return returnRewrite(node, ret, "ctn-fst-occ-pre-false");
+ }
+ }
if (node[1].getKind() == kind::STRING_STRREPL)
{
diff --git a/src/theory/strings/theory_strings_type_rules.h b/src/theory/strings/theory_strings_type_rules.h
index 9357a8f98..3e99add13 100644
--- a/src/theory/strings/theory_strings_type_rules.h
+++ b/src/theory/strings/theory_strings_type_rules.h
@@ -240,6 +240,66 @@ public:
}
};
+class StringFstOccPreTypeRule
+{
+ public:
+ inline static TypeNode computeType(NodeManager* nodeManager,
+ TNode n,
+ bool check)
+ {
+ if (check)
+ {
+ TypeNode t = n[0].getType(check);
+ if (!t.isString())
+ {
+ throw TypeCheckingExceptionPrivate(
+ n,
+ "expecting a string term as the first argument to first occurence "
+ "pre");
+ }
+ t = n[1].getType(check);
+ if (!t.isString())
+ {
+ throw TypeCheckingExceptionPrivate(
+ n,
+ "expecting a string term as the second argument to first occurence "
+ "pre");
+ }
+ }
+ return nodeManager->stringType();
+ }
+};
+
+class StringFstOccPostTypeRule
+{
+ public:
+ inline static TypeNode computeType(NodeManager* nodeManager,
+ TNode n,
+ bool check)
+ {
+ if (check)
+ {
+ TypeNode t = n[0].getType(check);
+ if (!t.isString())
+ {
+ throw TypeCheckingExceptionPrivate(
+ n,
+ "expecting a string term as the first argument to first occurence "
+ "post");
+ }
+ t = n[1].getType(check);
+ if (!t.isString())
+ {
+ throw TypeCheckingExceptionPrivate(
+ n,
+ "expecting a string term as the second argument to first occurence "
+ "post");
+ }
+ }
+ return nodeManager->stringType();
+ }
+};
+
class RegExpConcatTypeRule {
public:
inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback