From 384ab75e8637e872b568b6f493612d308f3f15ee Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 8 Dec 2020 01:50:10 -0600
Subject: 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.
---
 src/theory/strings/base_solver.cpp | 63 +++++++++++++++++++++++++-------------
 1 file changed, 42 insertions(+), 21 deletions(-)

(limited to 'src/theory/strings/base_solver.cpp')

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);
+    }
   }
 }
 
-- 
cgit v1.2.3