Care graphs based on polymorphic operators in strings (#4150)

Towards theory of sequences.

To compute a care graphs, we need to group function applications by the string type they are associated with. This PR introduces a utility to function to get the "owning string type" for a function application, and updates the care graph computation so that it partitions function applications according to this type.

3 files changed, 53 insertions, 5 deletions

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 83f0159b5..789099ee4 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -873,7 +873,9 @@ void TheoryStrings::addCarePairs(TNodeTrie* t1,
 void TheoryStrings::computeCareGraph(){
   //computing the care graph here is probably still necessary, due to operators that take non-string arguments  TODO: verify
   Trace("strings-cg") << "TheoryStrings::computeCareGraph(): Build term indices..." << std::endl;
-  std::map<Node, TNodeTrie> index;
+  // Term index for each (type, operator) pair. We require the operator here
+  // since operators are polymorphic, taking strings/sequences.
+  std::map<std::pair<TypeNode, Node>, TNodeTrie> index;
   std::map< Node, unsigned > arity;
   unsigned functionTerms = d_functionsTerms.size();
   for (unsigned i = 0; i < functionTerms; ++ i) {
@@ -889,16 +891,19 @@ void TheoryStrings::computeCareGraph(){
       }
     }
     if( has_trigger_arg ){
-      index[op].addTerm( f1, reps );
+      TypeNode ft = utils::getOwnerStringType(f1);
+      std::pair<TypeNode, Node> ikey = std::pair<TypeNode, Node>(ft, op);
+      index[ikey].addTerm(f1, reps);
       arity[op] = reps.size();
     }
   }
   //for each index
-  for (std::pair<const Node, TNodeTrie>& tt : index)
+  for (std::pair<const std::pair<TypeNode, Node>, TNodeTrie>& ti : index)
   {
     Trace("strings-cg") << "TheoryStrings::computeCareGraph(): Process index "
-                        << tt.first << "..." << std::endl;
-    addCarePairs(&tt.second, nullptr, arity[tt.first], 0);
+                        << ti.first << "..." << std::endl;
+    Node op = ti.first.second;
+    addCarePairs(&ti.second, nullptr, arity[op], 0);
   }
 }
 
diff --git a/src/theory/strings/theory_strings_utils.cpp b/src/theory/strings/theory_strings_utils.cpp
index 5d27b8e2b..74cd6c4a3 100644
--- a/src/theory/strings/theory_strings_utils.cpp
+++ b/src/theory/strings/theory_strings_utils.cpp
@@ -264,6 +264,36 @@ void printConcatTrace(std::vector<Node>& n, const char* c)
   Trace(c) << ss.str();
 }
 
+bool isStringKind(Kind k)
+{
+  return k == STRING_STOI || k == STRING_ITOS || k == STRING_TOLOWER
+         || k == STRING_TOUPPER || k == STRING_LEQ || k == STRING_LT
+         || k == STRING_FROM_CODE || k == STRING_TO_CODE;
+}
+
+TypeNode getOwnerStringType(Node n)
+{
+  TypeNode tn;
+  Kind k = n.getKind();
+  if (k == STRING_STRIDOF || k == STRING_LENGTH || k == STRING_STRCTN
+      || k == STRING_PREFIX || k == STRING_SUFFIX)
+  {
+    // owning string type is the type of first argument
+    tn = n[0].getType();
+  }
+  else if (isStringKind(k))
+  {
+    tn = NodeManager::currentNM()->stringType();
+  }
+  else
+  {
+    tn = n.getType();
+  }
+  AlwaysAssert(tn.isStringLike())
+      << "Unexpected term in getOwnerStringType : " << n << ", type " << tn;
+  return tn;
+}
+
 }  // namespace utils
 }  // namespace strings
 }  // namespace theory
diff --git a/src/theory/strings/theory_strings_utils.h b/src/theory/strings/theory_strings_utils.h
index 5f18d3936..578c224df 100644
--- a/src/theory/strings/theory_strings_utils.h
+++ b/src/theory/strings/theory_strings_utils.h
@@ -140,6 +140,19 @@ void printConcat(std::ostream& out, std::vector<Node>& n);
 /** Print the vector n as a concatentation term on trace given by c */
 void printConcatTrace(std::vector<Node>& n, const char* c);
 
+/** Is k a string-specific kind? */
+bool isStringKind(Kind k);
+
+/** Get owner string type
+ *
+ * This returns a string-like type for a term n that belongs to the theory of
+ * strings. This type conceptually represents the subtheory of strings
+ * (Sequence(T) or String) that owns n. This is typically the type of n,
+ * but for instance, operators like str.indexof( s, t, n ), this is the type
+ * of s.
+ */
+TypeNode getOwnerStringType(Node n);
+
 }  // namespace utils
 }  // namespace strings
 }  // namespace theory