From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 14 Mar 2019 22:51:39 +0000 (-0500)
Subject: Fix function term set for theory strings compute care graph. (#2862)
X-Git-Tag: cvc5-1.0.0~4241
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=219bc599111619c40779992f2199ff284293ec13;p=cvc5.git

Fix function term set for theory strings compute care graph. (#2862)
---

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 );