diff options
Diffstat (limited to 'src/theory/strings/theory_strings.cpp')
| -rw-r--r-- | src/theory/strings/theory_strings.cpp | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 7b00ed2e2..1bc104096 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -129,6 +129,7 @@ TheoryStrings::TheoryStrings(context::Context* c, getExtTheory()->addFunctionKind(kind::STRING_CODE); getExtTheory()->addFunctionKind(kind::STRING_TOLOWER); getExtTheory()->addFunctionKind(kind::STRING_TOUPPER); + getExtTheory()->addFunctionKind(kind::STRING_REV); // The kinds we are treating as function application in congruence d_equalityEngine.addFunctionKind(kind::STRING_LENGTH); @@ -147,6 +148,7 @@ TheoryStrings::TheoryStrings(context::Context* c, d_equalityEngine.addFunctionKind(kind::STRING_STRREPLALL); d_equalityEngine.addFunctionKind(kind::STRING_TOLOWER); d_equalityEngine.addFunctionKind(kind::STRING_TOUPPER); + d_equalityEngine.addFunctionKind(kind::STRING_REV); d_zero = NodeManager::currentNM()->mkConst( Rational( 0 ) ); d_one = NodeManager::currentNM()->mkConst( Rational( 1 ) ); @@ -437,7 +439,7 @@ bool TheoryStrings::doReduction(int effort, Node n, bool& isCd) Assert(k == STRING_SUBSTR || k == STRING_STRCTN || k == STRING_STRIDOF || k == STRING_ITOS || k == STRING_STOI || k == STRING_STRREPL || k == STRING_STRREPLALL || k == STRING_LEQ || k == STRING_TOLOWER - || k == STRING_TOUPPER); + || k == STRING_TOUPPER || k == STRING_REV); std::vector<Node> new_nodes; Node res = d_preproc.simplify(n, new_nodes); Assert(res != n); @@ -765,7 +767,8 @@ void TheoryStrings::preRegisterTerm(TNode n) { if (k == kind::STRING_STRIDOF || k == kind::STRING_ITOS || k == kind::STRING_STOI || k == kind::STRING_STRREPL || k == kind::STRING_STRREPLALL || k == kind::STRING_STRCTN - || k == STRING_LEQ || k == STRING_TOLOWER || k == STRING_TOUPPER) + || k == STRING_LEQ || k == STRING_TOLOWER || k == STRING_TOUPPER + || k == STRING_REV) { std::stringstream ss; ss << "Term of kind " << k |