Make term indices in the strings base solver aware of types (#5589)

This is required for handling inputs that combine strings and sequences.

Fixes #5542.

4 files changed, 56 insertions, 23 deletions

diff --git a/src/theory/strings/base_solver.cpp b/src/theory/strings/base_solver.cpp
index 451c01f8c..93803ea02 100644
--- a/src/theory/strings/base_solver.cpp
+++ b/src/theory/strings/base_solver.cpp
@@ -44,8 +44,10 @@ void BaseSolver::checkInit()
   d_termIndex.clear();
   d_stringsEqc.clear();
 
-  std::map<Kind, uint32_t> ncongruent;
-  std::map<Kind, uint32_t> congruent;
+  Trace("strings-base") << "BaseSolver::checkInit" << std::endl;
+  // count of congruent, non-congruent per operator (independent of type),
+  // for debugging.
+  std::map<Kind, std::pair<uint32_t, uint32_t>> congruentCount;
   eq::EqualityEngine* ee = d_state.getEqualityEngine();
   eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(ee);
   while (!eqcs_i.isFinished())
@@ -55,6 +57,8 @@ void BaseSolver::checkInit()
     if (!tn.isRegExp())
     {
       Node emps;
+      // get the term index for type tn
+      std::map<Kind, TermIndex>& tti = d_termIndex[tn];
       if (tn.isStringLike())
       {
         d_stringsEqc.push_back(eqc);
@@ -66,6 +70,7 @@ void BaseSolver::checkInit()
       {
         Node n = *eqc_i;
         Kind k = n.getKind();
+        Trace("strings-base") << "initialize term: " << n << std::endl;
         // process constant-like terms
         if (utils::isConstantLike(n))
         {
@@ -136,14 +141,17 @@ void BaseSolver::checkInit()
             if (d_congruent.find(n) == d_congruent.end())
             {
               std::vector<Node> c;
-              Node nc = d_termIndex[k].add(n, 0, d_state, emps, c);
+              Node nc = tti[k].add(n, 0, d_state, emps, c);
               if (nc != n)
               {
+                Trace("strings-base-debug")
+                    << "...found congruent term " << nc << std::endl;
                 // check if we have inferred a new equality by removal of empty
                 // components
                 if (k == STRING_CONCAT && !d_state.areEqual(nc, n))
                 {
                   std::vector<Node> exp;
+                  // the number of empty components of n, nc
                   size_t count[2] = {0, 0};
                   while (count[0] < nc.getNumChildren()
                          || count[1] < n.getNumChildren())
@@ -163,6 +171,9 @@ void BaseSolver::checkInit()
                         count[t]++;
                       }
                     }
+                    Trace("strings-base-debug")
+                        << "  counts = " << count[0] << ", " << count[1]
+                        << std::endl;
                     // explain equal components
                     if (count[0] < nc.getNumChildren())
                     {
@@ -190,15 +201,15 @@ void BaseSolver::checkInit()
                   // assuming that the reduction of f(a) depends on itself.
                 }
                 // this node is congruent to another one, we can ignore it
-                Trace("strings-process-debug")
+                Trace("strings-base-debug")
                     << "  congruent term : " << n << " (via " << nc << ")"
                     << std::endl;
                 d_congruent.insert(n);
-                congruent[k]++;
+                congruentCount[k].first++;
               }
               else if (k == STRING_CONCAT && c.size() == 1)
               {
-                Trace("strings-process-debug")
+                Trace("strings-base-debug")
                     << "  congruent term by singular : " << n << " " << c[0]
                     << std::endl;
                 // singular case
@@ -229,16 +240,16 @@ void BaseSolver::checkInit()
                   d_im.sendInference(exp, n.eqNode(ns), Inference::I_NORM_S);
                 }
                 d_congruent.insert(n);
-                congruent[k]++;
+                congruentCount[k].first++;
               }
               else
               {
-                ncongruent[k]++;
+                congruentCount[k].second++;
               }
             }
             else
             {
-              congruent[k]++;
+              congruentCount[k].first++;
             }
           }
         }
@@ -254,14 +265,14 @@ void BaseSolver::checkInit()
             }
             else if (var > n)
             {
-              Trace("strings-process-debug")
+              Trace("strings-base-debug")
                   << "  congruent variable : " << var << std::endl;
               d_congruent.insert(var);
               var = n;
             }
             else
             {
-              Trace("strings-process-debug")
+              Trace("strings-base-debug")
                   << "  congruent variable : " << n << std::endl;
               d_congruent.insert(n);
             }
@@ -272,17 +283,17 @@ void BaseSolver::checkInit()
     }
     ++eqcs_i;
   }
-  if (Trace.isOn("strings-process"))
+  if (Trace.isOn("strings-base"))
   {
-    for (std::map<Kind, TermIndex>::iterator it = d_termIndex.begin();
-         it != d_termIndex.end();
-         ++it)
+    for (const std::pair<const Kind, std::pair<uint32_t, uint32_t>>& cc :
+         congruentCount)
     {
-      Trace("strings-process")
-          << "  Terms[" << it->first << "] = " << ncongruent[it->first] << "/"
-          << (congruent[it->first] + ncongruent[it->first]) << std::endl;
+      Trace("strings-base")
+          << "  Terms[" << cc.first << "] = " << cc.second.second << "/"
+          << (cc.second.first + cc.second.second) << std::endl;
     }
   }
+  Trace("strings-base") << "BaseSolver::checkInit finished" << std::endl;
 }
 
 void BaseSolver::checkConstantEquivalenceClasses()
@@ -293,17 +304,27 @@ void BaseSolver::checkConstantEquivalenceClasses()
   do
   {
     vecc.clear();
-    Trace("strings-process-debug")
+    Trace("strings-base-debug")
         << "Check constant equivalence classes..." << std::endl;
     prevSize = d_eqcInfo.size();
-    checkConstantEquivalenceClasses(&d_termIndex[STRING_CONCAT], vecc, true);
+    for (std::pair<const TypeNode, std::map<Kind, TermIndex>>& tindex :
+         d_termIndex)
+    {
+      checkConstantEquivalenceClasses(
+          &tindex.second[STRING_CONCAT], vecc, true);
+    }
   } while (!d_im.hasProcessed() && d_eqcInfo.size() > prevSize);
 
   if (!d_im.hasProcessed())
   {
     // now, go back and set "most content" terms
     vecc.clear();
-    checkConstantEquivalenceClasses(&d_termIndex[STRING_CONCAT], vecc, false);
+    for (std::pair<const TypeNode, std::map<Kind, TermIndex>>& tindex :
+         d_termIndex)
+    {
+      checkConstantEquivalenceClasses(
+          &tindex.second[STRING_CONCAT], vecc, false);
+    }
   }
 }
 
diff --git a/src/theory/strings/base_solver.h b/src/theory/strings/base_solver.h
index 87f136dd0..929034e42 100644
--- a/src/theory/strings/base_solver.h
+++ b/src/theory/strings/base_solver.h
@@ -235,8 +235,8 @@ class BaseSolver
   std::map<Node, BaseEqcInfo> d_eqcInfo;
   /** The list of equivalence classes of type string */
   std::vector<Node> d_stringsEqc;
-  /** A term index for each function kind */
-  std::map<Kind, TermIndex> d_termIndex;
+  /** A term index for each type, function kind pair */
+  std::map<TypeNode, std::map<Kind, TermIndex> > d_termIndex;
   /** the cardinality of the alphabet */
   uint32_t d_cardSize;
 }; /* class BaseSolver */
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 062478075..7b3f94c1a 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1029,6 +1029,7 @@ set(regress_0_tests
   regress0/strings/issue5090.smt2
   regress0/strings/issue5384-double-conflict.smt2
   regress0/strings/issue5428-re-diff-assoc.smt2
+  regress0/strings/issue5542-strings-seq-mix.smt2
   regress0/strings/itos-entail.smt2
   regress0/strings/large-model.smt2
   regress0/strings/leadingzero001.smt2
diff --git a/test/regress/regress0/strings/issue5542-strings-seq-mix.smt2 b/test/regress/regress0/strings/issue5542-strings-seq-mix.smt2
new file mode 100644
index 000000000..56d1ddfb4
--- /dev/null
+++ b/test/regress/regress0/strings/issue5542-strings-seq-mix.smt2
@@ -0,0 +1,11 @@
+; COMMAND-LINE: --strings-exp
+; EXPECT: sat
+(set-logic ALL)
+(set-info :status sat)
+(declare-fun a () String)
+(declare-fun b () String)
+(declare-fun c () (Seq Int))
+(assert (distinct b (str.++ a a)))
+(assert (distinct (seq.unit 0) (seq.extract c 1 1)))
+(assert (= (seq.len c) 1))
+(check-sat)