diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-03-14 17:51:39 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-03-14 17:51:39 -0500 |
commit | 219bc599111619c40779992f2199ff284293ec13 (patch) | |
tree | 3aa24bacea6405cffd68ffc5078d279620ae40a7 /src/theory | |
parent | 504da2e215bd002ba763b7f102ddbd05917bc0d8 (diff) |
Fix function term set for theory strings compute care graph. (#2862)
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/strings/theory_strings.cpp | 11 |
1 files changed, 9 insertions, 2 deletions
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index e89a8f917..6300345ae 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -885,8 +885,15 @@ void TheoryStrings::preRegisterTerm(TNode n) { // Function applications/predicates d_equalityEngine.addTerm(n); } - //concat terms do not contribute to theory combination? TODO: verify - if (n.hasOperator() && kindToTheoryId(k) == THEORY_STRINGS + // Set d_functionsTerms stores all function applications that are + // relevant to theory combination. Notice that this is a subset of + // the applications whose kinds are function kinds in the equality + // engine. This means it does not include applications of operators + // like re.++, which is not a function kind in the equality engine. + // Concatenation terms do not need to be considered here because + // their arguments have string type and do not introduce any shared + // terms. + if (n.hasOperator() && d_equalityEngine.isFunctionKind(k) && k != kind::STRING_CONCAT) { d_functionsTerms.push_back( n ); |