diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-11-21 14:44:44 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-11-21 14:44:44 -0600 |
| commit | 2c05402119dba7e90e24621c5768514ab2f5042c (patch) | |
| tree | cec74ac8b51d20c622205bfa39e6ef6e44d510dc /src/theory/strings/theory_strings.cpp | |
| parent | b3b1fffb390d19312227d7095fb404e9e0447d95 (diff) | |
Support string replace all (#2704)
Diffstat (limited to 'src/theory/strings/theory_strings.cpp')
| -rw-r--r-- | src/theory/strings/theory_strings.cpp | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 883683f52..e8b753768 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -144,6 +144,7 @@ TheoryStrings::TheoryStrings(context::Context* c, getExtTheory()->addFunctionKind(kind::STRING_ITOS); getExtTheory()->addFunctionKind(kind::STRING_STOI); getExtTheory()->addFunctionKind(kind::STRING_STRREPL); + getExtTheory()->addFunctionKind(kind::STRING_STRREPLALL); getExtTheory()->addFunctionKind(kind::STRING_STRCTN); getExtTheory()->addFunctionKind(kind::STRING_IN_REGEXP); getExtTheory()->addFunctionKind(kind::STRING_LEQ); @@ -162,6 +163,7 @@ TheoryStrings::TheoryStrings(context::Context* c, d_equalityEngine.addFunctionKind(kind::STRING_STOI); d_equalityEngine.addFunctionKind(kind::STRING_STRIDOF); d_equalityEngine.addFunctionKind(kind::STRING_STRREPL); + d_equalityEngine.addFunctionKind(kind::STRING_STRREPLALL); } d_zero = NodeManager::currentNM()->mkConst( Rational( 0 ) ); @@ -503,7 +505,7 @@ bool TheoryStrings::doReduction(int effort, Node n, bool& isCd) NodeManager* nm = NodeManager::currentNM(); Assert(k == STRING_SUBSTR || k == STRING_STRCTN || k == STRING_STRIDOF || k == STRING_ITOS || k == STRING_STOI || k == STRING_STRREPL - || k == STRING_LEQ); + || k == STRING_STRREPLALL || k == STRING_LEQ); std::vector<Node> new_nodes; Node res = d_preproc.simplify(n, new_nodes); Assert(res != n); @@ -817,9 +819,8 @@ void TheoryStrings::preRegisterTerm(TNode n) { Kind k = n.getKind(); if( !options::stringExp() ){ if (k == kind::STRING_STRIDOF || k == kind::STRING_ITOS - || k == kind::STRING_STOI - || k == kind::STRING_STRREPL - || k == kind::STRING_STRCTN + || k == kind::STRING_STOI || k == kind::STRING_STRREPL + || k == kind::STRING_STRREPLALL || k == kind::STRING_STRCTN || k == STRING_LEQ) { std::stringstream ss; |