Add identifiers for extended function reductions (#6314)

This adds identifiers for extended function reductions, which are reasons for why an extended term no longer needs to be processed. The motivation is help understand check-model failures.

This PR adds identifiers to the ExtTheory utility. It also cleans up some unused parts of this utility. Some blocks of code changed indentation in this class.

9 files changed, 208 insertions, 201 deletions

diff --git a/src/theory/arith/nl/ext_theory_callback.cpp b/src/theory/arith/nl/ext_theory_callback.cpp
index 72848ac89..8fa1a56c9 100644
--- a/src/theory/arith/nl/ext_theory_callback.cpp
+++ b/src/theory/arith/nl/ext_theory_callback.cpp
@@ -69,17 +69,21 @@ bool NlExtTheoryCallback::getCurrentSubstitution(
   return retVal;
 }
 
-bool NlExtTheoryCallback::isExtfReduced(int effort,
-                                        Node n,
-                                        Node on,
-                                        std::vector<Node>& exp)
+bool NlExtTheoryCallback::isExtfReduced(
+    int effort, Node n, Node on, std::vector<Node>& exp, ExtReducedId& id)
 {
   if (n != d_zero)
   {
     Kind k = n.getKind();
-    return k != NONLINEAR_MULT && !isTranscendentalKind(k) && k != IAND;
+    if (k != NONLINEAR_MULT && !isTranscendentalKind(k) && k != IAND)
+    {
+      id = ExtReducedId::ARITH_SR_LINEAR;
+      return true;
+    }
+    return false;
   }
   Assert(n == d_zero);
+  id = ExtReducedId::ARITH_SR_ZERO;
   if (on.getKind() == NONLINEAR_MULT)
   {
     Trace("nl-ext-zero-exp")
diff --git a/src/theory/arith/nl/ext_theory_callback.h b/src/theory/arith/nl/ext_theory_callback.h
index 0e0e1411b..78ea3b2b6 100644
--- a/src/theory/arith/nl/ext_theory_callback.h
+++ b/src/theory/arith/nl/ext_theory_callback.h
@@ -72,7 +72,8 @@ class NlExtTheoryCallback : public ExtTheoryCallback
   bool isExtfReduced(int effort,
                      Node n,
                      Node on,
-                     std::vector<Node>& exp) override;
+                     std::vector<Node>& exp,
+                     ExtReducedId& id) override;
 
  private:
   /** The underlying equality engine. */
diff --git a/src/theory/arith/nl/nonlinear_extension.cpp b/src/theory/arith/nl/nonlinear_extension.cpp
index 16142886f..20d64b0d5 100644
--- a/src/theory/arith/nl/nonlinear_extension.cpp
+++ b/src/theory/arith/nl/nonlinear_extension.cpp
@@ -248,7 +248,6 @@ void NonlinearExtension::check(Theory::Effort e)
   Trace("nl-ext") << "NonlinearExtension::check, effort = " << e << std::endl;
   if (e == Theory::EFFORT_FULL)
   {
-    d_extTheory.clearCache();
     d_needsLastCall = true;
     if (options::nlExtRewrites())
     {
diff --git a/src/theory/ext_theory.cpp b/src/theory/ext_theory.cpp
index 80fafe92c..5cd38e4e0 100644
--- a/src/theory/ext_theory.cpp
+++ b/src/theory/ext_theory.cpp
@@ -30,6 +30,34 @@ using namespace std;
 namespace cvc5 {
 namespace theory {
 
+const char* toString(ExtReducedId id)
+{
+  switch (id)
+  {
+    case ExtReducedId::SR_CONST: return "SR_CONST";
+    case ExtReducedId::REDUCTION: return "REDUCTION";
+    case ExtReducedId::ARITH_SR_ZERO: return "ARITH_SR_ZERO";
+    case ExtReducedId::ARITH_SR_LINEAR: return "ARITH_SR_LINEAR";
+    case ExtReducedId::STRINGS_SR_CONST: return "STRINGS_SR_CONST";
+    case ExtReducedId::STRINGS_NEG_CTN_DEQ: return "STRINGS_NEG_CTN_DEQ";
+    case ExtReducedId::STRINGS_POS_CTN: return "STRINGS_POS_CTN";
+    case ExtReducedId::STRINGS_CTN_DECOMPOSE: return "STRINGS_CTN_DECOMPOSE";
+    case ExtReducedId::STRINGS_REGEXP_INTER: return "STRINGS_REGEXP_INTER";
+    case ExtReducedId::STRINGS_REGEXP_INTER_SUBSUME:
+      return "STRINGS_REGEXP_INTER_SUBSUME";
+    case ExtReducedId::STRINGS_REGEXP_INCLUDE: return "STRINGS_REGEXP_INCLUDE";
+    case ExtReducedId::STRINGS_REGEXP_INCLUDE_NEG:
+      return "STRINGS_REGEXP_INCLUDE_NEG";
+    default: return "?ExtReducedId?";
+  }
+}
+
+std::ostream& operator<<(std::ostream& out, ExtReducedId id)
+{
+  out << toString(id);
+  return out;
+}
+
 bool ExtTheoryCallback::getCurrentSubstitution(
     int effort,
     const std::vector<Node>& vars,
@@ -38,11 +66,10 @@ bool ExtTheoryCallback::getCurrentSubstitution(
 {
   return false;
 }
-bool ExtTheoryCallback::isExtfReduced(int effort,
-                                      Node n,
-                                      Node on,
-                                      std::vector<Node>& exp)
+bool ExtTheoryCallback::isExtfReduced(
+    int effort, Node n, Node on, std::vector<Node>& exp, ExtReducedId& id)
 {
+  id = ExtReducedId::SR_CONST;
   return n.isConst();
 }
 bool ExtTheoryCallback::getReduction(int effort,
@@ -56,16 +83,15 @@ bool ExtTheoryCallback::getReduction(int effort,
 ExtTheory::ExtTheory(ExtTheoryCallback& p,
                      context::Context* c,
                      context::UserContext* u,
-                     OutputChannel& out,
-                     bool cacheEnabled)
+                     OutputChannel& out)
     : d_parent(p),
       d_out(out),
       d_ext_func_terms(c),
+      d_extfExtReducedIdMap(c),
       d_ci_inactive(u),
       d_has_extf(c),
       d_lemmas(u),
-      d_pp_lemmas(u),
-      d_cacheEnabled(cacheEnabled)
+      d_pp_lemmas(u)
 {
   d_true = NodeManager::currentNM()->mkConst(true);
 }
@@ -103,23 +129,13 @@ std::vector<Node> ExtTheory::collectVars(Node n)
 
 Node ExtTheory::getSubstitutedTerm(int effort,
                                    Node term,
-                                   std::vector<Node>& exp,
-                                   bool useCache)
+                                   std::vector<Node>& exp)
 {
-  if (useCache)
-  {
-    Assert(d_gst_cache[effort].find(term) != d_gst_cache[effort].end());
-    exp.insert(exp.end(),
-               d_gst_cache[effort][term].d_exp.begin(),
-               d_gst_cache[effort][term].d_exp.end());
-    return d_gst_cache[effort][term].d_sterm;
-  }
-
   std::vector<Node> terms;
   terms.push_back(term);
   std::vector<Node> sterms;
   std::vector<std::vector<Node> > exps;
-  getSubstitutedTerms(effort, terms, sterms, exps, useCache);
+  getSubstitutedTerms(effort, terms, sterms, exps);
   Assert(sterms.size() == 1);
   Assert(exps.size() == 1);
   exp.insert(exp.end(), exps[0].begin(), exps[0].end());
@@ -130,92 +146,67 @@ Node ExtTheory::getSubstitutedTerm(int effort,
 void ExtTheory::getSubstitutedTerms(int effort,
                                     const std::vector<Node>& terms,
                                     std::vector<Node>& sterms,
-                                    std::vector<std::vector<Node> >& exp,
-                                    bool useCache)
+                                    std::vector<std::vector<Node> >& exp)
 {
-  if (useCache)
+  Trace("extt-debug") << "getSubstitutedTerms for " << terms.size() << " / "
+                      << d_ext_func_terms.size() << " extended functions."
+                      << std::endl;
+  if (!terms.empty())
   {
+    // all variables we need to find a substitution for
+    std::vector<Node> vars;
+    std::vector<Node> sub;
+    std::map<Node, std::vector<Node> > expc;
     for (const Node& n : terms)
     {
-      Assert(d_gst_cache[effort].find(n) != d_gst_cache[effort].end());
-      sterms.push_back(d_gst_cache[effort][n].d_sterm);
-      exp.push_back(std::vector<Node>());
-      exp[0].insert(exp[0].end(),
-                    d_gst_cache[effort][n].d_exp.begin(),
-                    d_gst_cache[effort][n].d_exp.end());
-    }
-  }
-  else
-  {
-    Trace("extt-debug") << "getSubstitutedTerms for " << terms.size() << " / "
-                        << d_ext_func_terms.size() << " extended functions."
-                        << std::endl;
-    if (!terms.empty())
-    {
-      // all variables we need to find a substitution for
-      std::vector<Node> vars;
-      std::vector<Node> sub;
-      std::map<Node, std::vector<Node> > expc;
-      for (const Node& n : terms)
+      // do substitution, rewrite
+      std::map<Node, ExtfInfo>::iterator iti = d_extf_info.find(n);
+      Assert(iti != d_extf_info.end());
+      for (const Node& v : iti->second.d_vars)
       {
-        // do substitution, rewrite
-        std::map<Node, ExtfInfo>::iterator iti = d_extf_info.find(n);
-        Assert(iti != d_extf_info.end());
-        for (const Node& v : iti->second.d_vars)
+        if (std::find(vars.begin(), vars.end(), v) == vars.end())
         {
-          if (std::find(vars.begin(), vars.end(), v) == vars.end())
-          {
-            vars.push_back(v);
-          }
+          vars.push_back(v);
         }
       }
-      bool useSubs = d_parent.getCurrentSubstitution(effort, vars, sub, expc);
-      // get the current substitution for all variables
-      Assert(!useSubs || vars.size() == sub.size());
-      for (const Node& n : terms)
+    }
+    bool useSubs = d_parent.getCurrentSubstitution(effort, vars, sub, expc);
+    // get the current substitution for all variables
+    Assert(!useSubs || vars.size() == sub.size());
+    for (const Node& n : terms)
+    {
+      Node ns = n;
+      std::vector<Node> expn;
+      if (useSubs)
       {
-        Node ns = n;
-        std::vector<Node> expn;
-        if (useSubs)
+        // do substitution
+        ns = n.substitute(vars.begin(), vars.end(), sub.begin(), sub.end());
+        if (ns != n)
         {
-          // do substitution
-          ns = n.substitute(vars.begin(), vars.end(), sub.begin(), sub.end());
-          if (ns != n)
+          // build explanation: explanation vars = sub for each vars in FV(n)
+          std::map<Node, ExtfInfo>::iterator iti = d_extf_info.find(n);
+          Assert(iti != d_extf_info.end());
+          for (const Node& v : iti->second.d_vars)
           {
-            // build explanation: explanation vars = sub for each vars in FV(n)
-            std::map<Node, ExtfInfo>::iterator iti = d_extf_info.find(n);
-            Assert(iti != d_extf_info.end());
-            for (const Node& v : iti->second.d_vars)
+            std::map<Node, std::vector<Node> >::iterator itx = expc.find(v);
+            if (itx != expc.end())
             {
-              std::map<Node, std::vector<Node> >::iterator itx = expc.find(v);
-              if (itx != expc.end())
+              for (const Node& e : itx->second)
               {
-                for (const Node& e : itx->second)
+                if (std::find(expn.begin(), expn.end(), e) == expn.end())
                 {
-                  if (std::find(expn.begin(), expn.end(), e) == expn.end())
-                  {
-                    expn.push_back(e);
-                  }
+                  expn.push_back(e);
                 }
               }
             }
           }
-          Trace("extt-debug")
-              << "  have " << n << " == " << ns << ", exp size=" << expn.size()
-              << "." << std::endl;
-        }
-        // add to vector
-        sterms.push_back(ns);
-        exp.push_back(expn);
-        // add to cache
-        if (d_cacheEnabled)
-        {
-          d_gst_cache[effort][n].d_sterm = ns;
-          d_gst_cache[effort][n].d_exp.clear();
-          d_gst_cache[effort][n].d_exp.insert(
-              d_gst_cache[effort][n].d_exp.end(), expn.begin(), expn.end());
         }
+        Trace("extt-debug") << "  have " << n << " == " << ns
+                            << ", exp size=" << expn.size() << "." << std::endl;
       }
+      // add to vector
+      sterms.push_back(ns);
+      exp.push_back(expn);
     }
   }
 }
@@ -252,7 +243,7 @@ bool ExtTheory::doInferencesInternal(int effort,
               addedLemma = true;
             }
           }
-          markReduced(n, satDep);
+          markReduced(n, ExtReducedId::REDUCTION, satDep);
         }
       }
     }
@@ -271,10 +262,11 @@ bool ExtTheory::doInferencesInternal(int effort,
           Node sr = Rewriter::rewrite(sterms[i]);
           // ask the theory if this term is reduced, e.g. is it constant or it
           // is a non-extf term.
-          if (d_parent.isExtfReduced(effort, sr, terms[i], exp[i]))
+          ExtReducedId id;
+          if (d_parent.isExtfReduced(effort, sr, terms[i], exp[i], id))
           {
             processed = true;
-            markReduced(terms[i]);
+            markReduced(terms[i], id);
             // We have exp[i] => terms[i] = sr, convert this to a clause.
             // This ensures the proof infrastructure can process this as a
             // normal theory lemma.
@@ -441,15 +433,16 @@ void ExtTheory::registerTerm(Node n)
 }
 
 // mark reduced
-void ExtTheory::markReduced(Node n, bool satDep)
+void ExtTheory::markReduced(Node n, ExtReducedId rid, bool satDep)
 {
   Trace("extt-debug") << "Mark reduced " << n << std::endl;
   registerTerm(n);
   Assert(d_ext_func_terms.find(n) != d_ext_func_terms.end());
   d_ext_func_terms[n] = false;
+  d_extfExtReducedIdMap[n] = rid;
   if (!satDep)
   {
-    d_ci_inactive.insert(n);
+    d_ci_inactive[n] = rid;
   }
 
   // update has_extf
@@ -468,34 +461,21 @@ void ExtTheory::markReduced(Node n, bool satDep)
   }
 }
 
-// mark congruent
-void ExtTheory::markCongruent(Node a, Node b)
+bool ExtTheory::isContextIndependentInactive(Node n) const
 {
-  Trace("extt-debug") << "Mark congruent : " << a << " " << b << std::endl;
-  registerTerm(a);
-  registerTerm(b);
-  NodeBoolMap::const_iterator it = d_ext_func_terms.find(b);
-  if (it != d_ext_func_terms.end())
-  {
-    if (d_ext_func_terms.find(a) != d_ext_func_terms.end())
-    {
-      d_ext_func_terms[a] = d_ext_func_terms[a] && (*it).second;
-    }
-    else
-    {
-      Assert(false);
-    }
-    d_ext_func_terms[b] = false;
-  }
-  else
-  {
-    Assert(false);
-  }
+  ExtReducedId rid = ExtReducedId::UNKNOWN;
+  return isContextIndependentInactive(n, rid);
 }
 
-bool ExtTheory::isContextIndependentInactive(Node n) const
+bool ExtTheory::isContextIndependentInactive(Node n, ExtReducedId& rid) const
 {
-  return d_ci_inactive.find(n) != d_ci_inactive.end();
+  NodeExtReducedIdMap::iterator it = d_ci_inactive.find(n);
+  if (it != d_ci_inactive.end())
+  {
+    rid = it->second;
+    return true;
+  }
+  return false;
 }
 
 void ExtTheory::getTerms(std::vector<Node>& terms)
@@ -510,13 +490,25 @@ void ExtTheory::getTerms(std::vector<Node>& terms)
 
 bool ExtTheory::hasActiveTerm() const { return !d_has_extf.get().isNull(); }
 
-// is active
 bool ExtTheory::isActive(Node n) const
 {
+  ExtReducedId rid = ExtReducedId::UNKNOWN;
+  return isActive(n, rid);
+}
+
+bool ExtTheory::isActive(Node n, ExtReducedId& rid) const
+{
   NodeBoolMap::const_iterator it = d_ext_func_terms.find(n);
   if (it != d_ext_func_terms.end())
   {
-    return (*it).second && !isContextIndependentInactive(n);
+    if ((*it).second)
+    {
+      return !isContextIndependentInactive(n, rid);
+    }
+    NodeExtReducedIdMap::const_iterator itr = d_extfExtReducedIdMap.find(n);
+    Assert(itr != d_extfExtReducedIdMap.end());
+    rid = itr->second;
+    return false;
   }
   return false;
 }
@@ -555,7 +547,5 @@ std::vector<Node> ExtTheory::getActive(Kind k) const
   return active;
 }
 
-void ExtTheory::clearCache() { d_gst_cache.clear(); }
-
 }  // namespace theory
 }  // namespace cvc5
diff --git a/src/theory/ext_theory.h b/src/theory/ext_theory.h
index b44f2b852..0beca705d 100644
--- a/src/theory/ext_theory.h
+++ b/src/theory/ext_theory.h
@@ -46,6 +46,52 @@ namespace theory {
 
 class OutputChannel;
 
+/** Reasons for why a term was marked reduced */
+enum class ExtReducedId
+{
+  UNKNOWN,
+  // the extended function substitutes+rewrites to a constant
+  SR_CONST,
+  // the extended function was reduced by the callback
+  REDUCTION,
+  // the extended function substitutes+rewrites to zero
+  ARITH_SR_ZERO,
+  // the extended function substitutes+rewrites to a linear (non-zero) term
+  ARITH_SR_LINEAR,
+  // an extended string function substitutes+rewrites to a constant
+  STRINGS_SR_CONST,
+  // a negative str.contains was reduced to a disequality
+  STRINGS_NEG_CTN_DEQ,
+  // a positive str.contains was reduced to an equality
+  STRINGS_POS_CTN,
+  // a str.contains was subsumed by another based on a decomposition
+  STRINGS_CTN_DECOMPOSE,
+  // reduced via an intersection inference
+  STRINGS_REGEXP_INTER,
+  // subsumed due to intersection reasoning
+  STRINGS_REGEXP_INTER_SUBSUME,
+  // subsumed due to RE inclusion reasoning for positive memberships
+  STRINGS_REGEXP_INCLUDE,
+  // subsumed due to RE inclusion reasoning for negative memberships
+  STRINGS_REGEXP_INCLUDE_NEG,
+};
+/**
+ * Converts an ext reduced identifier to a string.
+ *
+ * @param id The ext reduced identifier
+ * @return The name of the ext reduced identifier
+ */
+const char* toString(ExtReducedId id);
+
+/**
+ * Writes an ext reduced identifier to a stream.
+ *
+ * @param out The stream to write to
+ * @param id The ext reduced identifier to write to the stream
+ * @return The stream
+ */
+std::ostream& operator<<(std::ostream& out, ExtReducedId id);
+
 /**
  * A callback class for ExtTheory below. This class is responsible for
  * determining how to apply context-dependent simplification.
@@ -78,12 +124,12 @@ class ExtTheoryCallback
    * @param n The term to reduce
    * @param on The original form of n, before substitution
    * @param exp The explanation of on = n
+   * @param id If this method returns true, then id is updated to the reason
+   * why n was reduced.
    * @return true if n is reduced.
    */
-  virtual bool isExtfReduced(int effort,
-                             Node n,
-                             Node on,
-                             std::vector<Node>& exp);
+  virtual bool isExtfReduced(
+      int effort, Node n, Node on, std::vector<Node>& exp, ExtReducedId& id);
 
   /**
    * Get reduction for node n.
@@ -117,8 +163,10 @@ class ExtTheoryCallback
  */
 class ExtTheory
 {
-  typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap;
-  typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
+  using NodeBoolMap = context::CDHashMap<Node, bool, NodeHashFunction>;
+  using NodeExtReducedIdMap =
+      context::CDHashMap<Node, ExtReducedId, NodeHashFunction>;
+  using NodeSet = context::CDHashSet<Node, NodeHashFunction>;
 
  public:
   /** constructor
@@ -128,8 +176,7 @@ class ExtTheory
   ExtTheory(ExtTheoryCallback& p,
             context::Context* c,
             context::UserContext* u,
-            OutputChannel& out,
-            bool cacheEnabled = false);
+            OutputChannel& out);
   virtual ~ExtTheory() {}
   /** Tells this class to treat terms with Kind k as extended functions */
   void addFunctionKind(Kind k) { d_extf_kind[k] = true; }
@@ -150,12 +197,7 @@ class ExtTheory
    * If satDep = false, then n remains inactive in the duration of this
    * user-context level
    */
-  void markReduced(Node n, bool satDep = true);
-  /**
-   * Mark that a and b are congruent terms. This sets b inactive, and sets a to
-   * inactive if b was inactive.
-   */
-  void markCongruent(Node a, Node b);
+  void markReduced(Node n, ExtReducedId rid, bool satDep = true);
   /** getSubstitutedTerms
    *
    *  input : effort, terms
@@ -163,27 +205,17 @@ class ExtTheory
    *
    * For each i, sterms[i] = term[i] * sigma for some "derivable substitution"
    * sigma. We obtain derivable substitutions and their explanations via calls
-   * to the underlying theory's Theory::getCurrentSubstitution method. This
-   * also
-   *
-   * If useCache is true, we cache the result in d_gst_cache. This is a context
-   * independent cache that can be cleared using clearCache() below.
+   * to the underlying theory's Theory::getCurrentSubstitution method.
    */
   void getSubstitutedTerms(int effort,
                            const std::vector<Node>& terms,
                            std::vector<Node>& sterms,
-                           std::vector<std::vector<Node> >& exp,
-                           bool useCache = false);
+                           std::vector<std::vector<Node> >& exp);
   /**
    * Same as above, but for a single term. We return the substituted form of
    * term and add its explanation to exp.
    */
-  Node getSubstitutedTerm(int effort,
-                          Node term,
-                          std::vector<Node>& exp,
-                          bool useCache = false);
-  /** clear the cache for getSubstitutedTerm */
-  void clearCache();
+  Node getSubstitutedTerm(int effort, Node term, std::vector<Node>& exp);
   /** doInferences
    *
    * This function performs "context-dependent simplification". The method takes
@@ -232,6 +264,11 @@ class ExtTheory
   bool hasActiveTerm() const;
   /** is n an active extended function term? */
   bool isActive(Node n) const;
+  /**
+   * Same as above, but rid is updated to the reason if this method returns
+   * false.
+   */
+  bool isActive(Node n, ExtReducedId& rid) const;
   /** get the set of active terms from d_ext_func_terms */
   std::vector<Node> getActive() const;
   /** get the set of active terms from d_ext_func_terms of kind k */
@@ -242,6 +279,11 @@ class ExtTheory
   static std::vector<Node> collectVars(Node n);
   /** is n context dependent inactive? */
   bool isContextIndependentInactive(Node n) const;
+  /**
+   * Same as above, but rid is updated to the reason if this method returns
+   * true.
+   */
+  bool isContextIndependentInactive(Node n, ExtReducedId& rid) const;
   /** do inferences internal */
   bool doInferencesInternal(int effort,
                             const std::vector<Node>& terms,
@@ -258,12 +300,14 @@ class ExtTheory
   Node d_true;
   /** extended function terms, map to whether they are active */
   NodeBoolMap d_ext_func_terms;
+  /** mapping to why extended function terms are inactive */
+  NodeExtReducedIdMap d_extfExtReducedIdMap;
   /**
    * The set of terms from d_ext_func_terms that are SAT-context-independent
    * inactive. For instance, a term t is SAT-context-independent inactive if
    * a reduction lemma of the form t = t' was added in this user-context level.
    */
-  NodeSet d_ci_inactive;
+  NodeExtReducedIdMap d_ci_inactive;
   /**
    * Watched term for checking if any non-reduced extended functions exist.
    * This is an arbitrary active member of d_ext_func_terms.
@@ -283,22 +327,6 @@ class ExtTheory
   // cache of all lemmas sent
   NodeSet d_lemmas;
   NodeSet d_pp_lemmas;
-  /** whether we enable caching for getSubstitutedTerm */
-  bool d_cacheEnabled;
-  /** Substituted term info */
-  class SubsTermInfo
-  {
-   public:
-    /** the substituted term */
-    Node d_sterm;
-    /** an explanation */
-    std::vector<Node> d_exp;
-  };
-  /**
-   * This maps an (effort, term) to the information above. It is used as a
-   * cache for getSubstitutedTerm when d_cacheEnabled is true.
-   */
-  std::map<int, std::map<Node, SubsTermInfo> > d_gst_cache;
 };
 
 }  // namespace theory
diff --git a/src/theory/strings/extf_solver.cpp b/src/theory/strings/extf_solver.cpp
index fd50e78ee..6051bc4ca 100644
--- a/src/theory/strings/extf_solver.cpp
+++ b/src/theory/strings/extf_solver.cpp
@@ -132,7 +132,7 @@ bool ExtfSolver::doReduction(int effort, Node n)
           }
           // this depends on the current assertions, so this
           // inference is context-dependent
-          d_extt.markReduced(n, true);
+          d_extt.markReduced(n, ExtReducedId::STRINGS_NEG_CTN_DEQ, true);
           return true;
         }
         else
@@ -183,7 +183,7 @@ bool ExtfSolver::doReduction(int effort, Node n)
     Trace("strings-red-lemma") << "Reduction (positive contains) lemma : " << n
                                << " => " << eq << std::endl;
     // context-dependent because it depends on the polarity of n itself
-    d_extt.markReduced(n, true);
+    d_extt.markReduced(n, ExtReducedId::STRINGS_POS_CTN, true);
   }
   else if (k != kind::STRING_TO_CODE)
   {
@@ -297,7 +297,7 @@ void ExtfSolver::checkExtfEval(int effort)
       {
         if (effort < 3)
         {
-          d_extt.markReduced(n);
+          d_extt.markReduced(n, ExtReducedId::STRINGS_SR_CONST);
           Trace("strings-extf-debug")
               << "  resolvable by evaluation..." << std::endl;
           std::vector<Node> exps;
@@ -549,7 +549,7 @@ void ExtfSolver::checkExtfInference(Node n,
             else if (d_extt.hasFunctionKind(conc.getKind()))
             {
               // can mark as reduced, since model for n implies model for conc
-              d_extt.markReduced(conc);
+              d_extt.markReduced(conc, ExtReducedId::STRINGS_CTN_DECOMPOSE);
             }
           }
         }
@@ -730,9 +730,10 @@ std::string ExtfSolver::debugPrintModel()
   for (const Node& n : extf)
   {
     ss << "- " << n;
-    if (!d_extt.isActive(n))
+    ExtReducedId id;
+    if (!d_extt.isActive(n, id))
     {
-      ss << " :extt-inactive";
+      ss << " :extt-inactive " << id;
     }
     if (!d_extfInfoTmp[n].d_modelActive)
     {
diff --git a/src/theory/strings/inference_manager.cpp b/src/theory/strings/inference_manager.cpp
index 8a0429fae..6f218e5be 100644
--- a/src/theory/strings/inference_manager.cpp
+++ b/src/theory/strings/inference_manager.cpp
@@ -268,18 +268,9 @@ bool InferenceManager::hasProcessed() const
   return d_state.isInConflict() || hasPending();
 }
 
-void InferenceManager::markCongruent(Node a, Node b)
+void InferenceManager::markReduced(Node n, ExtReducedId id, bool contextDepend)
 {
-  Assert(a.getKind() == b.getKind());
-  if (d_extt.hasFunctionKind(a.getKind()))
-  {
-    d_extt.markCongruent(a, b);
-  }
-}
-
-void InferenceManager::markReduced(Node n, bool contextDepend)
-{
-  d_extt.markReduced(n, contextDepend);
+  d_extt.markReduced(n, id, contextDepend);
 }
 
 void InferenceManager::processConflict(const InferInfo& ii)
diff --git a/src/theory/strings/inference_manager.h b/src/theory/strings/inference_manager.h
index cfb8614ca..abc5c5709 100644
--- a/src/theory/strings/inference_manager.h
+++ b/src/theory/strings/inference_manager.h
@@ -220,18 +220,11 @@ class InferenceManager : public InferenceManagerBuffered
 
   // ------------------------------------------------- extended theory
   /**
-   * Mark that terms a and b are congruent in the current context.
-   * This makes a call to markCongruent in the extended theory object of
-   * the parent theory if the kind of a (and b) is owned by the extended
-   * theory.
-   */
-  void markCongruent(Node a, Node b);
-  /**
    * Mark that extended function is reduced. If contextDepend is true,
    * then this mark is SAT-context dependent, otherwise it is user-context
    * dependent (see ExtTheory::markReduced).
    */
-  void markReduced(Node n, bool contextDepend = true);
+  void markReduced(Node n, ExtReducedId id, bool contextDepend = true);
   // ------------------------------------------------- end extended theory
 
   /**
diff --git a/src/theory/strings/regexp_solver.cpp b/src/theory/strings/regexp_solver.cpp
index 85d66cd54..151761329 100644
--- a/src/theory/strings/regexp_solver.cpp
+++ b/src/theory/strings/regexp_solver.cpp
@@ -361,14 +361,14 @@ bool RegExpSolver::checkEqcInclusion(std::vector<Node>& mems)
           {
             // ~str.in.re(x, R1) includes ~str.in.re(x, R2) --->
             //   mark ~str.in.re(x, R2) as reduced
-            d_im.markReduced(m2Lit);
+            d_im.markReduced(m2Lit, ExtReducedId::STRINGS_REGEXP_INCLUDE_NEG);
             remove.insert(m2);
           }
           else
           {
             // str.in.re(x, R1) includes str.in.re(x, R2) --->
             //   mark str.in.re(x, R1) as reduced
-            d_im.markReduced(m1Lit);
+            d_im.markReduced(m1Lit, ExtReducedId::STRINGS_REGEXP_INCLUDE);
             remove.insert(m1);
 
             // We don't need to process m1 anymore
@@ -489,12 +489,12 @@ bool RegExpSolver::checkEqcIntersect(const std::vector<Node>& mems)
     {
       // if R1 = intersect( R1, R2 ), then x in R1 ^ x in R2 is equivalent
       // to x in R1, hence x in R2 can be marked redundant.
-      d_im.markReduced(m);
+      d_im.markReduced(m, ExtReducedId::STRINGS_REGEXP_INTER_SUBSUME);
     }
     else if (mresr == m)
     {
       // same as above, opposite direction
-      d_im.markReduced(mi);
+      d_im.markReduced(mi, ExtReducedId::STRINGS_REGEXP_INTER_SUBSUME);
     }
     else
     {
@@ -510,8 +510,8 @@ bool RegExpSolver::checkEqcIntersect(const std::vector<Node>& mems)
       d_im.sendInference(
           vec_nodes, mres, InferenceId::STRINGS_RE_INTER_INFER, false, true);
       // both are reduced
-      d_im.markReduced(m);
-      d_im.markReduced(mi);
+      d_im.markReduced(m, ExtReducedId::STRINGS_REGEXP_INTER);
+      d_im.markReduced(mi, ExtReducedId::STRINGS_REGEXP_INTER);
       // do not send more than one lemma for this class
       return true;
     }