From 219bc599111619c40779992f2199ff284293ec13 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 14 Mar 2019 17:51:39 -0500 Subject: [PATCH] Fix function term set for theory strings compute care graph. (#2862) --- src/theory/strings/theory_strings.cpp | 11 +++++++++-- 1 file 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 ); -- 2.30.2