New normal forms heuristicnormalFormsHeuristic

3 files changed, 74 insertions, 2 deletions

diff --git a/src/theory/strings/normal_form.cpp b/src/theory/strings/normal_form.cpp
index c70845d64..249f53bf7 100644
--- a/src/theory/strings/normal_form.cpp
+++ b/src/theory/strings/normal_form.cpp
@@ -40,6 +40,8 @@ void NormalForm::init(Node base)
   {
     d_nf.push_back(base);
   }
+
+  d_complexityComputed = false;
 }
 
 void NormalForm::reverse()
@@ -75,6 +77,7 @@ void NormalForm::splitConstant(unsigned index, Node c1, Node c2)
       }
     }
   }
+  d_complexityComputed = false;
 }
 
 void NormalForm::addToExplanation(Node exp,
@@ -158,6 +161,60 @@ void NormalForm::getExplanationForPrefixEq(NormalForm& nfi,
   }
 }
 
+uint64_t NormalForm::getComplexity()
+{
+  if (d_complexityComputed)
+  {
+    return d_complexity;
+  }
+
+  std::unordered_map<TNode, uint64_t, TNodeHashFunction> visited;
+  std::unordered_map<TNode, uint64_t, TNodeHashFunction>::iterator it;
+  std::vector<Node> visit = d_nf;
+  do
+  {
+    Node cur = visit.back();
+    visit.pop_back();
+    it = visited.find(cur);
+    if (it == visited.end())
+    {
+      visited[cur] = 0;
+
+      visit.push_back(cur);
+      for (unsigned i = 0; i < cur.getNumChildren(); i++)
+      {
+        visit.push_back(cur[i]);
+      }
+    }
+    else if (!it->second)
+    {
+      for (const Node& c : cur)
+      {
+        visited[cur] += visited[c];
+      }
+
+      Kind k = cur.getKind();
+      if (k == kind::STRING_STRCTN || k == kind::STRING_STRREPL
+          || k == kind::STRING_STRIDOF || k == kind::STRING_ITOS
+          || k == kind::STRING_STOI || k == kind::STRING_IN_REGEXP
+          || k == kind::STRING_SUBSTR || k == kind::STRING_CHARAT
+          || k == kind::STRING_PREFIX || k == kind::STRING_SUFFIX)
+      {
+        visited[cur]++;
+      }
+    }
+  } while (!visit.empty());
+
+  d_complexity = 0;
+  for (const Node& n : d_nf)
+  {
+    d_complexity += visited[n];
+  }
+
+  d_complexityComputed = true;
+  return d_complexity;
+}
+
 }  // namespace strings
 }  // namespace theory
 }  // namespace CVC4
diff --git a/src/theory/strings/normal_form.h b/src/theory/strings/normal_form.h
index 73036e68f..ac776d0b2 100644
--- a/src/theory/strings/normal_form.h
+++ b/src/theory/strings/normal_form.h
@@ -41,7 +41,7 @@ namespace strings {
 class NormalForm
 {
  public:
-  NormalForm() : d_isRev(false) {}
+  NormalForm() : d_isRev(false), d_complexity(0), d_complexityComputed(false) {}
   /**
    * The "base" of the normal form. This is some term in the equivalence
    * class of t that the normal form is based on. This is an arbitrary term
@@ -150,6 +150,12 @@ class NormalForm
                                         int index_i,
                                         int index_j,
                                         std::vector<Node>& curr_exp);
+
+  uint64_t getComplexity();
+
+ private:
+  uint64_t d_complexity;
+  bool d_complexityComputed;
 };
 
 }  // namespace strings
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index c2b87fbef..7e3d4d663 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -2653,6 +2653,7 @@ void TheoryStrings::normalizeEquivalenceClass( Node eqc ) {
 
     //construct the normal form
     Assert( !normal_forms.empty() );
+
     unsigned nf_index = 0;
     std::map<Node, unsigned>::iterator it = term_to_nf_index.find(eqc);
     // we prefer taking the normal form whose base is the equivalence
@@ -2662,7 +2663,15 @@ void TheoryStrings::normalizeEquivalenceClass( Node eqc ) {
     {
       nf_index = it->second;
     }
-    d_normal_form[eqc] = normal_forms[nf_index];
+
+    NormalForm& min = normal_forms[nf_index];
+    for (NormalForm& nf : normal_forms) {
+      if (nf.getComplexity() < min.getComplexity()) {
+        min = nf;
+      }
+    }
+    d_normal_form[eqc] = min;
+
     Trace("strings-process-debug")
         << "Return process equivalence class " << eqc
         << " : returned, size = " << d_normal_form[eqc].d_nf.size()