Simplify method for inferring proxy lemmas in strings (#5789)

This PR simplifies our heuristic for inferring when an explanation for a strings lemma can be minimized based on proxy variable definitions. In particular, we do not turn solved equalities for proxy variables into substitutions. This aspect of the heuristic is incompatible with the new eager solver work, and moreover is buggy since substitutions should not be applied within string terms. The latter was leading the incorrect models on the 2 issues fixed by this PR.

Current results on the eager solver on SMT-LIB shows this change has very little performance impact.

Fixes #5692, fixes #5610.

3 files changed, 29 insertions, 95 deletions

diff --git a/src/theory/strings/inference_manager.cpp b/src/theory/strings/inference_manager.cpp
index cf90c8fbe..0c55d26e8 100644
--- a/src/theory/strings/inference_manager.cpp
+++ b/src/theory/strings/inference_manager.cpp
@@ -186,17 +186,14 @@ void InferenceManager::sendInference(InferInfo& ii, bool asLemma)
   }
   if (options::stringInferSym())
   {
-    std::vector<Node> vars;
-    std::vector<Node> subs;
     std::vector<Node> unproc;
     for (const Node& ac : ii.d_premises)
     {
-      d_termReg.inferSubstitutionProxyVars(ac, vars, subs, unproc);
+      d_termReg.removeProxyEqs(ac, unproc);
     }
     if (unproc.empty())
     {
-      Node eqs = ii.d_conc.substitute(
-          vars.begin(), vars.end(), subs.begin(), subs.end());
+      Node eqs = ii.d_conc;
       InferInfo iiSubsLem;
       iiSubsLem.d_sim = this;
       // keep the same id for now, since we are transforming the form of the
@@ -209,11 +206,6 @@ void InferenceManager::sendInference(InferInfo& ii, bool asLemma)
             << "Strings::Infer " << iiSubsLem << std::endl;
         Trace("strings-lemma-debug")
             << "Strings::Infer Alternate : " << eqs << std::endl;
-        for (unsigned i = 0, nvars = vars.size(); i < nvars; i++)
-        {
-          Trace("strings-lemma-debug")
-              << "  " << vars[i] << " -> " << subs[i] << std::endl;
-        }
       }
       Trace("strings-infer-debug") << "...as symbolic lemma" << std::endl;
       addPendingLemma(std::unique_ptr<InferInfo>(new InferInfo(iiSubsLem)));
diff --git a/src/theory/strings/term_registry.cpp b/src/theory/strings/term_registry.cpp
index cce2b117f..160bc7d73 100644
--- a/src/theory/strings/term_registry.cpp
+++ b/src/theory/strings/term_registry.cpp
@@ -575,83 +575,39 @@ Node TermRegistry::ensureProxyVariableFor(Node n)
   return proxy;
 }
 
-void TermRegistry::inferSubstitutionProxyVars(Node n,
-                                              std::vector<Node>& vars,
-                                              std::vector<Node>& subs,
-                                              std::vector<Node>& unproc) const
+void TermRegistry::removeProxyEqs(Node n, std::vector<Node>& unproc) const
 {
   if (n.getKind() == AND)
   {
     for (const Node& nc : n)
     {
-      inferSubstitutionProxyVars(nc, vars, subs, unproc);
+      removeProxyEqs(nc, unproc);
     }
     return;
   }
-  if (n.getKind() == EQUAL)
+  Trace("strings-subs-proxy") << "Input : " << n << std::endl;
+  Node ns = Rewriter::rewrite(n);
+  if (ns.getKind() == EQUAL)
   {
-    Node ns = n.substitute(vars.begin(), vars.end(), subs.begin(), subs.end());
-    ns = Rewriter::rewrite(ns);
-    if (ns.getKind() == EQUAL)
+    for (size_t i = 0; i < 2; i++)
     {
-      Node s;
-      Node v;
-      for (unsigned i = 0; i < 2; i++)
+      // determine whether this side has a proxy variable
+      if (ns[i].getAttribute(StringsProxyVarAttribute()))
       {
-        Node ss;
-        // determine whether this side has a proxy variable
-        if (ns[i].getAttribute(StringsProxyVarAttribute()))
+        if (getProxyVariableFor(ns[1 - i]) == ns[i])
         {
-          // it is a proxy variable
-          ss = ns[i];
-        }
-        else if (ns[i].isConst())
-        {
-          ss = getProxyVariableFor(ns[i]);
-        }
-        if (!ss.isNull())
-        {
-          v = ns[1 - i];
-          // if the other side is a constant or variable
-          if (v.getNumChildren() == 0)
-          {
-            if (s.isNull())
-            {
-              s = ss;
-            }
-            else
-            {
-              // both sides of the equality correspond to a proxy variable
-              if (ss == s)
-              {
-                // it is a trivial equality, e.g. between a proxy variable
-                // and its definition
-                return;
-              }
-              else
-              {
-                // equality between proxy variables, non-trivial
-                s = Node::null();
-              }
-            }
-          }
+          Trace("strings-subs-proxy")
+              << "...trivial definition via " << ns[i] << std::endl;
+          // it is a trivial equality, e.g. between a proxy variable
+          // and its definition
+          return;
         }
       }
-      if (!s.isNull())
-      {
-        // the equality can be turned into a substitution
-        subs.push_back(s);
-        vars.push_back(v);
-        return;
-      }
-    }
-    else
-    {
-      n = ns;
     }
   }
   if (!n.isConst() || !n.getConst<bool>())
   {
+    Trace("strings-subs-proxy") << "...unprocessed" << std::endl;
     unproc.push_back(n);
   }
 }
diff --git a/src/theory/strings/term_registry.h b/src/theory/strings/term_registry.h
index a713cc60f..ddff32242 100644
--- a/src/theory/strings/term_registry.h
+++ b/src/theory/strings/term_registry.h
@@ -176,39 +176,25 @@ class TermRegistry
    */
   Node ensureProxyVariableFor(Node n);
 
-  /** infer substitution proxy vars
-   *
-   * This method attempts to (partially) convert the formula n into a
-   * substitution of the form:
-   *   v1 -> s1, ..., vn -> sn
-   * where s1 ... sn are proxy variables and v1 ... vn are either variables
-   * or constants.
-   *
-   * This method ensures that P ^ v1 = s1 ^ ... ^ vn = sn ^ unproc is equivalent
-   * to P ^ n, where P is the conjunction of equalities corresponding to the
-   * definition of all proxy variables introduced by the theory of strings.
+  /**
+   * This method attempts to (partially) remove trivial parts of an explanation
+   * n. It adds conjuncts of n that must be included in the explanation into
+   * unproc and drops the rest.
    *
-   * For example, say that v1 was introduced as a proxy variable for "ABC", and
-   * v2 was introduced as a proxy variable for "AA".
+   * For example, say that v1 was introduced as a proxy variable for "ABC".
    *
-   * Given the input n := v1 = "ABC" ^ v2 = x ^ x = "AA", this method sets:
-   * vars = { x },
-   * subs = { v2 },
-   * unproc = {}.
+   * Given the input n := v1 = "ABC" ^ x = "AA", this method sets:
+   * unproc = { x = "AA" }.
    * In particular, this says that the information content of n is essentially
-   * x = v2. The first and third conjunctions can be dropped from the
-   * explanation since these equalities simply correspond to definitions
-   * of proxy variables.
+   * x = "AA". The first conjunct can be dropped from the explanation since
+   * that equality simply corresponds to definition of a proxy variable.
    *
    * This method is used as a performance heuristic. It can infer when the
-   * explanation of a fact depends only trivially on equalities corresponding
-   * to definitions of proxy variables, which can be omitted since they are
+   * explanation of a fact depends only on equalities corresponding to
+   * definitions of proxy variables, which can be omitted since they are
    * assumed to hold globally.
    */
-  void inferSubstitutionProxyVars(Node n,
-                                  std::vector<Node>& vars,
-                                  std::vector<Node>& subs,
-                                  std::vector<Node>& unproc) const;
+  void removeProxyEqs(Node n, std::vector<Node>& unproc) const;
   //---------------------------- end proxy variables
  private:
   /** Common constants */