More aggressive substitutions for extf evalextfSubst

5 files changed, 142 insertions, 5 deletions

diff --git a/src/parser/parser.h b/src/parser/parser.h
index cd4105cd0..efa845c4c 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -805,10 +805,6 @@ public:
     d_globalDeclarations = flag;
   }
 
-  inline SymbolTable* getSymbolTable() const {
-    return d_symtab;
-  }
-  
   //------------------------ operator overloading
   /** is this function overloaded? */
   bool isOverloadedFunction(api::Term fun)
diff --git a/src/theory/strings/base_solver.cpp b/src/theory/strings/base_solver.cpp
index 1f8d2f49c..62a57d511 100644
--- a/src/theory/strings/base_solver.cpp
+++ b/src/theory/strings/base_solver.cpp
@@ -45,6 +45,7 @@ void BaseSolver::checkInit()
   d_eqcToConst.clear();
   d_eqcToConstBase.clear();
   d_eqcToConstExp.clear();
+  d_eqcToMostContent.clear();
   d_termIndex.clear();
   d_stringsEqc.clear();
 
@@ -186,6 +187,65 @@ void BaseSolver::checkInit()
             {
               congruent[k]++;
             }
+
+            if (k == STRING_CONCAT)
+            {
+              NodeManager* nm = NodeManager::currentNM();
+
+              const auto& it = d_eqcToMostContent.find(eqc);
+              if (it == d_eqcToMostContent.end())
+              {
+                std::vector<Node> vec;
+                size_t score = 0;
+                bool change = false;
+                for (const Node& nc : n)
+                {
+                  Node rep = ee->getRepresentative(nc);
+                  if (rep.isConst())
+                  {
+                    change = change || (rep != nc);
+                    vec.push_back(rep);
+                    score += rep.getConst<String>().size();
+                  }
+                  else
+                  {
+                    vec.push_back(nc);
+                  }
+                }
+
+                if ((change || n != eqc) && score > 0)
+                {
+                  d_eqcToMostContent.insert(std::make_pair(
+                      eqc,
+                      ContentInfo(n, nm->mkNode(STRING_CONCAT, vec), score)));
+                }
+              }
+              else
+              {
+                std::vector<Node> vec;
+                size_t score = 0;
+                for (const Node& nc : n)
+                {
+                  Node rep = ee->getRepresentative(nc);
+                  if (rep.isConst())
+                  {
+                    vec.push_back(rep);
+                    score += rep.getConst<String>().size();
+                  }
+                  else
+                  {
+                    vec.push_back(nc);
+                  }
+                }
+
+                if (score > it->second.d_score)
+                {
+                  d_eqcToMostContent.insert(std::make_pair(
+                      eqc,
+                      ContentInfo(n, nm->mkNode(STRING_CONCAT, vec), score)));
+                }
+              }
+            }
           }
         }
         else
@@ -525,6 +585,49 @@ Node BaseSolver::explainConstantEqc(Node n, Node eqc, std::vector<Node>& exp)
   return Node::null();
 }
 
+Node BaseSolver::getMostContentInEqc(Node eqc)
+{
+  Node c = getConstantEqc(eqc);
+  if (!c.isNull())
+  {
+    return c;
+  }
+
+  const auto& it = d_eqcToMostContent.find(eqc);
+  if (it != d_eqcToMostContent.end())
+  {
+    return it->second.d_content;
+  }
+  return Node::null();
+}
+
+Node BaseSolver::explainMostContentInEqc(Node n,
+                                         Node eqc,
+                                         std::vector<Node>& exp)
+{
+  Node c = explainConstantEqc(n, eqc, exp);
+  if (!c.isNull())
+  {
+    return c;
+  }
+
+  const auto& it = d_eqcToMostContent.find(eqc);
+  if (it != d_eqcToMostContent.end())
+  {
+    Node original = it->second.d_original;
+    Node content = it->second.d_content;
+    for (size_t i = 0, size = original.getNumChildren(); i < size; i++)
+    {
+      d_im.addToExplanation(original[i], content[i], exp);
+    }
+    d_im.addToExplanation(n, eqc, exp);
+    d_im.addToExplanation(eqc, original, exp);
+    return content;
+  }
+
+  return Node::null();
+}
+
 const std::vector<Node>& BaseSolver::getStringEqc() const
 {
   return d_stringsEqc;
diff --git a/src/theory/strings/base_solver.h b/src/theory/strings/base_solver.h
index 3681b49a4..44b6fd0a2 100644
--- a/src/theory/strings/base_solver.h
+++ b/src/theory/strings/base_solver.h
@@ -30,6 +30,29 @@ namespace CVC4 {
 namespace theory {
 namespace strings {
 
+/**
+ * This struct stores the content information for an equivalence class
+ * containing at least one string concatenation.
+ */
+struct ContentInfo
+{
+  Node d_original;
+  /** The content */
+  Node d_content;
+  /**
+   * The score, which is determined by how many known characters the string
+   * literals in the content have
+   */
+  size_t d_score;
+
+  std::vector<Node> d_exp;
+
+  ContentInfo(Node original, Node content, size_t score)
+      : d_original(original), d_content(content), d_score(score)
+  {
+  }
+};
+
 /** The base solver for the theory of strings
  *
  * This implements techniques for inferring when terms are congruent in the
@@ -99,6 +122,9 @@ class BaseSolver
    * equivalence class of eqc.
    */
   Node explainConstantEqc(Node n, Node eqc, std::vector<Node>& exp);
+
+  Node getMostContentInEqc(Node eqc);
+  Node explainMostContentInEqc(Node n, Node eqc, std::vector<Node>& exp);
   /**
    * Get the set of equivalence classes of type string.
    */
@@ -185,6 +211,8 @@ class BaseSolver
   std::map<Node, Node> d_eqcToConst;
   std::map<Node, Node> d_eqcToConstBase;
   std::map<Node, Node> d_eqcToConstExp;
+  /** Maps representatives of equivalence classes */
+  std::map<Node, ContentInfo> d_eqcToMostContent;
   /** The list of equivalence classes of type string */
   std::vector<Node> d_stringsEqc;
   /** A term index for each function kind */
diff --git a/src/theory/strings/extf_solver.cpp b/src/theory/strings/extf_solver.cpp
index 775b4a796..a843f2c22 100644
--- a/src/theory/strings/extf_solver.cpp
+++ b/src/theory/strings/extf_solver.cpp
@@ -624,6 +624,7 @@ void ExtfSolver::checkExtfInference(Node n,
   Node inferEq = nr.eqNode(in.d_const);
   Node inferEqr = Rewriter::rewrite(inferEq);
   Node inferEqrr = inferEqr;
+
   if (inferEqr.getKind() == EQUAL)
   {
     // try to use the extended rewriter for equalities
@@ -650,7 +651,8 @@ Node ExtfSolver::getCurrentSubstitutionFor(int effort,
     return mv;
   }
   Node nr = d_state.getRepresentative(n);
-  Node c = d_bsolver.explainConstantEqc(n, nr, exp);
+  // Node c = d_bsolver.explainConstantEqc(n, nr, exp);
+  Node c = d_bsolver.explainMostContentInEqc(n, nr, exp);
   if (!c.isNull())
   {
     return c;
diff --git a/src/theory/strings/sequences_rewriter.cpp b/src/theory/strings/sequences_rewriter.cpp
index d8b8765eb..46ed5ac80 100644
--- a/src/theory/strings/sequences_rewriter.cpp
+++ b/src/theory/strings/sequences_rewriter.cpp
@@ -2992,6 +2992,14 @@ Node SequencesRewriter::rewritePrefixSuffix(Node n)
   Node retNode = n[0].eqNode(
       NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR, n[1], val, lens));
 
+  NodeManager* nm = NodeManager::currentNM();
+  retNode =
+      nm->mkNode(AND,
+                 retNode,
+                 nm->mkNode(STRING_LENGTH,
+                            nm->mkNode(kind::STRING_SUBSTR, n[1], val, lens))
+                     .eqNode(lens));
+
   return returnRewrite(n, retNode, Rewrite::SUF_PREFIX_ELIM);
 }