Generalize symmetry detection for 1 symmetry variable mapped to n input variables (#1888)

3 files changed, 1002 insertions, 346 deletions

diff --git a/src/preprocessing/passes/symmetry_breaker.cpp b/src/preprocessing/passes/symmetry_breaker.cpp
index e1b6b4274..c32057d5f 100644
--- a/src/preprocessing/passes/symmetry_breaker.cpp
+++ b/src/preprocessing/passes/symmetry_breaker.cpp
@@ -129,7 +129,7 @@ PreprocessingPassResult SymBreakerPass::applyInternal(
   Trace("sym-break-pass") << "Apply symmetry breaker pass..." << std::endl;
   // detect symmetries
   std::vector<std::vector<Node>> part;
-  SymmetryDetect symd;
+  symbreak::SymmetryDetect symd;
   symd.getPartition(part, assertionsToPreprocess->ref());
   if (Trace.isOn("sym-break-pass"))
   {
diff --git a/src/preprocessing/passes/symmetry_detect.cpp b/src/preprocessing/passes/symmetry_detect.cpp
index 683bec6ac..a1273b1d9 100644
--- a/src/preprocessing/passes/symmetry_detect.cpp
+++ b/src/preprocessing/passes/symmetry_detect.cpp
@@ -21,22 +21,484 @@ using namespace std;
 namespace CVC4 {
 namespace preprocessing {
 namespace passes {
+namespace symbreak {
 
-SymmetryDetect::Partition SymmetryDetect::detect(const vector<Node>& assertions)
+/** returns n choose k, that is, n!/(k! * (n-k)!) */
+unsigned nChoosek(unsigned n, unsigned k)
 {
-  Partition p =
-      findPartitions(NodeManager::currentNM()->mkNode(kind::AND, assertions));
+  if (k > n) return 0;
+  if (k * 2 > n) k = n - k;
+  if (k == 0) return 1;
+
+  int result = n;
+  for (int i = 2; i <= static_cast<int>(k); ++i)
+  {
+    result *= (n - i + 1);
+    result /= i;
+  }
+  return result;
+}
+
+/** mk associative node
+ *
+ * This returns (a normal form for) the term <k>( children ), where
+ * k is an associative operator. We return a right-associative
+ * chain, since some operators (e.g. set union) require this.
+ */
+Node mkAssociativeNode(Kind k, std::vector<Node>& children)
+{
+  Assert(!children.empty());
+  NodeManager* nm = NodeManager::currentNM();
+  // sort and make right-associative chain
+  bool isComm = theory::quantifiers::TermUtil::isComm(k);
+  if (isComm)
+  {
+    std::sort(children.begin(), children.end());
+  }
+  Node sn;
+  for (const Node& sc : children)
+  {
+    Assert(!sc.isNull());
+    if (sn.isNull())
+    {
+      sn = sc;
+    }
+    else
+    {
+      Assert(!isComm || sc.getType().isComparableTo(sn.getType()));
+      sn = nm->mkNode(k, sc, sn);
+    }
+  }
+  return sn;
+}
+
+void Partition::printPartition(const char* c, Partition p)
+{
+  for (map<Node, vector<Node> >::iterator sub_vars_it =
+           p.d_subvar_to_vars.begin();
+       sub_vars_it != p.d_subvar_to_vars.end();
+       ++sub_vars_it)
+  {
+    Trace(c) << "[sym-dt] Partition: " << sub_vars_it->first << " -> {";
+
+    for (vector<Node>::iterator part_it = (sub_vars_it->second).begin();
+         part_it != (sub_vars_it->second).end();
+         ++part_it)
+    {
+      Trace(c) << " " << *part_it;
+    }
+    Trace(c) << " }" << endl;
+  }
+}
+
+void Partition::normalize()
+{
+  for (std::pair<const Node, std::vector<Node> > p : d_subvar_to_vars)
+  {
+    std::sort(p.second.begin(), p.second.end());
+  }
+}
+
+void PartitionMerger::initialize(Kind k,
+                                 const std::vector<Partition>& partitions,
+                                 const std::vector<unsigned>& indices)
+{
+  d_kind = k;
+  Trace("sym-dt-debug") << "Count variable occurrences..." << std::endl;
+  for (unsigned index : indices)
+  {
+    d_indices.push_back(index);
+    const Partition& p = partitions[index];
+    const std::vector<Node>& svs = p.d_subvar_to_vars.begin()->second;
+    for (const Node& v : svs)
+    {
+      if (d_occurs_count.find(v) == d_occurs_count.end())
+      {
+        d_occurs_count[v] = 1;
+      }
+      else
+      {
+        d_occurs_count[v]++;
+      }
+      d_occurs_by[index][v] = d_occurs_count[v] - 1;
+    }
+  }
+  if (Trace.isOn("sym-dt-debug"))
+  {
+    Trace("sym-dt-debug") << "    variable occurrences: " << std::endl;
+    for (const std::pair<const Node, unsigned>& o : d_occurs_count)
+    {
+      Trace("sym-dt-debug")
+          << "     " << o.first << " -> " << o.second << std::endl;
+    }
+  }
+}
+
+bool PartitionMerger::merge(std::vector<Partition>& partitions,
+                            unsigned base_index,
+                            std::unordered_set<unsigned>& active_indices)
+{
+  Assert(base_index < partitions.size());
+  d_master_base_index = base_index;
+  Partition& p = partitions[base_index];
+  Trace("sym-dt-debug") << "   try basis index " << base_index
+                        << " (#vars = " << p.d_subvar_to_vars.size() << ")"
+                        << std::endl;
+  Assert(p.d_subvar_to_vars.size() == 1);
+  std::vector<Node>& svs = p.d_subvar_to_vars.begin()->second;
+  Trace("sym-dt-debug") << "   try basis: " << svs << std::endl;
+  // try to merge variables one-by-one
+  d_base_indices.clear();
+  d_base_indices.insert(base_index);
+  d_base_vars.clear();
+  d_base_vars.insert(svs.begin(), svs.end());
+  d_num_new_indices_needed = d_base_vars.size();
+  bool merged = false;
+  bool success = false;
+  unsigned base_choose = d_base_vars.size() - 1;
+  unsigned base_occurs_req = d_base_vars.size();
+  do
+  {
+    Trace("sym-dt-debug") << "   base variables must occur " << base_occurs_req
+                          << " times." << std::endl;
+    // check if all the base_vars occur at least the required number of times
+    bool var_ok = true;
+    for (const Node& v : d_base_vars)
+    {
+      if (d_occurs_count[v] < base_occurs_req)
+      {
+        Trace("sym-dt-debug") << "...failed variable " << v << std::endl;
+        var_ok = false;
+        break;
+      }
+    }
+    if (!var_ok)
+    {
+      // cannot merge due to a base variable
+      break;
+    }
+    // try to find a new variable to merge
+    Trace("sym-dt-debug") << "   must find " << d_num_new_indices_needed
+                          << " new indices to merge." << std::endl;
+    std::vector<unsigned> new_indices;
+    Node merge_var;
+    d_merge_var_tried.clear();
+    if (mergeNewVar(0, new_indices, merge_var, 0, partitions, active_indices))
+    {
+      Trace("sym-dt-debug") << "   ...merged: " << merge_var << std::endl;
+      Assert(!merge_var.isNull());
+      merged = true;
+      success = true;
+      // update the number of new indicies needed
+      if (base_choose > 0)
+      {
+        d_num_new_indices_needed +=
+            nChoosek(d_base_vars.size(), base_choose - 1);
+        // TODO (#2198): update base_occurs_req
+      }
+    }
+    else
+    {
+      Trace("sym-dt-debug") << "   ...failed to merge" << std::endl;
+      success = false;
+    }
+  } while (success);
+  return merged;
+}
+
+bool PartitionMerger::mergeNewVar(unsigned curr_index,
+                                  std::vector<unsigned>& new_indices,
+                                  Node& merge_var,
+                                  unsigned num_merge_var_max,
+                                  std::vector<Partition>& partitions,
+                                  std::unordered_set<unsigned>& active_indices)
+{
+  Assert(new_indices.size() < d_num_new_indices_needed);
+  if (curr_index == d_indices.size())
+  {
+    return false;
+  }
+  Trace("sym-dt-debug2") << "merge " << curr_index << " / " << d_indices.size()
+                         << std::endl;
+  // try to include this index
+  unsigned index = d_indices[curr_index];
+
+  // if not already included
+  if (d_base_indices.find(index) == d_base_indices.end())
+  {
+    Assert(active_indices.find(index) != active_indices.end());
+    // check whether it can merge
+    Partition& p = partitions[index];
+    Assert(p.d_subvar_to_vars.size() == 1);
+    std::vector<Node>& svs = p.d_subvar_to_vars.begin()->second;
+    bool include_success = true;
+    Node curr_merge_var;
+    for (const Node& v : svs)
+    {
+      if (d_base_vars.find(v) == d_base_vars.end() && v != merge_var)
+      {
+        if (merge_var.isNull() && curr_merge_var.isNull())
+        {
+          curr_merge_var = v;
+        }
+        else
+        {
+          // cannot include
+          Trace("sym-dt-debug2") << "...cannot include (new-var)\n";
+          include_success = false;
+          curr_merge_var = Node::null();
+          break;
+        }
+      }
+    }
+    if (!curr_merge_var.isNull())
+    {
+      // compute the maximum number of indices we can include for v
+      Assert(d_occurs_by[index].find(curr_merge_var)
+             != d_occurs_by[index].end());
+      Assert(d_occurs_count.find(curr_merge_var) != d_occurs_count.end());
+      unsigned num_v_max =
+          d_occurs_count[curr_merge_var] - d_occurs_by[index][curr_merge_var];
+      if (num_v_max >= d_num_new_indices_needed)
+      {
+        // have we already tried this merge_var?
+        if (d_merge_var_tried.find(curr_merge_var) != d_merge_var_tried.end())
+        {
+          include_success = false;
+          Trace("sym-dt-debug2")
+              << "...cannot include (already tried new merge var "
+              << curr_merge_var << ")\n";
+        }
+        else
+        {
+          Trace("sym-dt-debug2")
+              << "set merge var : " << curr_merge_var << std::endl;
+          d_merge_var_tried.insert(curr_merge_var);
+          num_merge_var_max = num_v_max;
+          merge_var = curr_merge_var;
+        }
+      }
+      else
+      {
+        Trace("sym-dt-debug2")
+            << "...cannot include (not enough room for new merge var "
+            << num_v_max << "<" << d_num_new_indices_needed << ")\n";
+        include_success = false;
+      }
+    }
+    else if (!include_success && !merge_var.isNull())
+    {
+      // decrement
+      num_merge_var_max--;
+      if (num_merge_var_max < d_num_new_indices_needed - new_indices.size())
+      {
+        Trace("sym-dt-debug2") << "...fail (out of merge var)\n";
+        return false;
+      }
+    }
+
+    if (include_success)
+    {
+      // try with the index included
+      new_indices.push_back(index);
+
+      // do we have enough now?
+      if (new_indices.size() == d_num_new_indices_needed)
+      {
+        std::vector<Node> children;
+        children.push_back(p.d_term);
+        std::vector<Node> schildren;
+        schildren.push_back(p.d_sterm);
+        // can now include in the base
+        d_base_vars.insert(merge_var);
+        Trace("sym-dt-debug") << "found symmetry : { ";
+        for (const unsigned& i : new_indices)
+        {
+          Assert(d_base_indices.find(i) == d_base_indices.end());
+          d_base_indices.insert(i);
+          Trace("sym-dt-debug") << i << " ";
+          const Partition& p = partitions[i];
+          children.push_back(p.d_term);
+          schildren.push_back(p.d_sterm);
+          Assert(active_indices.find(i) != active_indices.end());
+          active_indices.erase(i);
+        }
+        Trace("sym-dt-debug") << "}" << std::endl;
+        Trace("sym-dt-debug") << "Reconstruct master partition "
+                              << d_master_base_index << std::endl;
+        Partition& p = partitions[d_master_base_index];
+        // reconstruct the master partition
+        p.d_term = mkAssociativeNode(d_kind, children);
+        p.d_sterm = mkAssociativeNode(d_kind, schildren);
+        Assert(p.d_subvar_to_vars.size() == 1);
+        Node sb_v = p.d_subvar_to_vars.begin()->first;
+        p.d_subvar_to_vars[sb_v].push_back(merge_var);
+        Trace("sym-dt-debug") << "- set var to svar: " << merge_var << " -> "
+                              << sb_v << std::endl;
+        p.d_var_to_subvar[merge_var] = sb_v;
+        return true;
+      }
+      if (mergeNewVar(curr_index + 1,
+                      new_indices,
+                      merge_var,
+                      num_merge_var_max,
+                      partitions,
+                      active_indices))
+      {
+        return true;
+      }
+      new_indices.pop_back();
+      // if we included with the merge var, no use trying not including
+      if (curr_merge_var.isNull() && !merge_var.isNull())
+      {
+        Trace("sym-dt-debug2") << "...fail (failed merge var)\n";
+        return false;
+      }
+    }
+  }
+  // TODO (#2198):
+  // if we haven't yet chosen a merge variable, we may not have enough elements
+  // left in d_indices.
+
+  // try with it not included
+  return mergeNewVar(curr_index + 1,
+                     new_indices,
+                     merge_var,
+                     num_merge_var_max,
+                     partitions,
+                     active_indices);
+}
+
+void PartitionTrie::getNewPartition(Partition& part,
+                                    PartitionTrie& pt,
+                                    std::map<Node, Node>& var_to_svar)
+{
+  if (!pt.d_variables.empty())
+  {
+    Assert(var_to_svar.find(pt.d_variables[0]) != var_to_svar.end());
+    Node svar = var_to_svar[pt.d_variables[0]];
+    Trace("sym-dt-debug")
+        << "[sym-dt] A partition from leaves of the partition trie:{";
+    for (const Node& v : pt.d_variables)
+    {
+      Trace("sym-dt-debug") << " " << v;
+      part.d_var_to_subvar[v] = svar;
+      part.d_subvar_to_vars[svar].push_back(v);
+    }
+    Trace("sym-dt-debug") << " }" << endl;
+  }
+  else
+  {
+    for (map<Node, PartitionTrie>::iterator part_it = pt.d_children.begin();
+         part_it != pt.d_children.end();
+         ++part_it)
+    {
+      getNewPartition(part, part_it->second, var_to_svar);
+    }
+  }
+}
+
+Node PartitionTrie::addNode(Node target_var, vector<Partition>& partitions)
+{
+  Trace("sym-dt-debug") << "[sym-dt] Add a variable {" << target_var
+                        << "} to the partition trie, #partitions = "
+                        << partitions.size() << "..." << endl;
+  Assert(!partitions.empty());
+  vector<Node> subvars;
+
+  for (vector<Partition>::iterator part_it = partitions.begin();
+       part_it != partitions.end();
+       ++part_it)
+  {
+    map<Node, Node>::iterator var_sub_it =
+        (*part_it).d_var_to_subvar.find(target_var);
+
+    if (var_sub_it != (*part_it).d_var_to_subvar.end())
+    {
+      subvars.push_back(var_sub_it->second);
+    }
+    else
+    {
+      subvars.push_back(Node::null());
+    }
+  }
+
+  Trace("sym-dt-debug")
+      << "[sym-dt] Symmetry breaking variables for the variable " << target_var
+      << ": " << subvars << endl;
+  PartitionTrie* curr = this;
+  for (const Node& c : subvars)
+  {
+    curr = &(curr->d_children[c]);
+  }
+  curr->d_variables.push_back(target_var);
+  return curr->d_variables[0];
+}
+
+Partition SymmetryDetect::detect(const vector<Node>& assertions)
+{
+  Node an;
+  if (assertions.empty())
+  {
+    an = d_trueNode;
+  }
+  else if (assertions.size() == 1)
+  {
+    an = assertions[0];
+  }
+  else
+  {
+    an = NodeManager::currentNM()->mkNode(kind::AND, assertions);
+  }
+  Partition p = findPartitions(an);
   Trace("sym-dt") << endl
                   << "------------------------------ The Final Partition "
                      "------------------------------"
                   << endl;
   if(Trace.isOn("sym-dt"))
   {
-    printPartition(p);
+    Partition::printPartition("sym-dt", p);
   }
   return p;
 }
 
+Node SymmetryDetect::getSymBreakVariable(TypeNode tn, unsigned index)
+{
+  std::map<TypeNode, std::vector<Node> >::iterator it = d_sb_vars.find(tn);
+  if (it == d_sb_vars.end())
+  {
+    // initialize the variables for type tn
+    d_sb_vars[tn].clear();
+    it = d_sb_vars.find(tn);
+  }
+  while (it->second.size() <= index)
+  {
+    std::stringstream ss;
+    ss << "_sym_bk_" << tn << "_" << (it->second.size() + 1);
+    Node fresh_var =
+        NodeManager::currentNM()->mkSkolem(ss.str(),
+                                           tn,
+                                           "symmetry breaking variable",
+                                           NodeManager::SKOLEM_EXACT_NAME);
+    it->second.push_back(fresh_var);
+  }
+  return it->second[index];
+}
+
+Node SymmetryDetect::getSymBreakVariableInc(TypeNode tn,
+                                            std::map<TypeNode, unsigned>& index)
+{
+  // ensure we use a new index for this variable
+  unsigned new_index = 0;
+  std::map<TypeNode, unsigned>::iterator itt = index.find(tn);
+  if (itt != index.end())
+  {
+    new_index = itt->second;
+  }
+  index[tn] = new_index + 1;
+  return getSymBreakVariable(tn, new_index);
+}
+
 void SymmetryDetect::getPartition(vector<vector<Node> >& parts,
                                   const vector<Node>& assertions)
 {
@@ -51,20 +513,20 @@ void SymmetryDetect::getPartition(vector<vector<Node> >& parts,
   }
 }
 
-SymmetryDetect::Partition SymmetryDetect::findPartitions(Node node)
+Partition SymmetryDetect::findPartitions(Node node)
 {
-  Trace("sym-dt")
-      << "------------------------------------------------------------"
-      << endl;
-  Trace("sym-dt") << "[sym-dt] findPartitions gets a term: " << node << endl;
+  Trace("sym-dt-debug")
+      << "------------------------------------------------------------" << endl;
+  Trace("sym-dt-debug") << "[sym-dt] findPartitions gets a term: " << node
+                        << endl;
   map<Node, Partition>::iterator partition = d_term_partition.find(node);
 
   // Return its partition from cache if we have processed the node before
   if (partition != d_term_partition.end())
   {
-    Trace("sym-dt") << "[sym-dt] We have seen the node " << node
-                    << " before, thus we return its partition from cache."
-                    << endl;
+    Trace("sym-dt-debug") << "[sym-dt] We have seen the node " << node
+                          << " before, thus we return its partition from cache."
+                          << endl;
     return partition->second;
   }
 
@@ -75,22 +537,35 @@ SymmetryDetect::Partition SymmetryDetect::findPartitions(Node node)
   {
     vector<Node> vars;
     TypeNode type = node.getType();
-    Node fresh_var = NodeManager::currentNM()->mkSkolem("sym_bk", type);
-
+    Node fresh_var = getSymBreakVariable(type, 0);
     vars.push_back(node);
     p.d_term = node;
+    p.d_sterm = fresh_var;
     p.d_subvar_to_vars[fresh_var] = vars;
     p.d_var_to_subvar[node] = fresh_var;
     d_term_partition[node] = p;
     return p;
   }
   // If node is a constant
-  else if (node.isConst())
+  else if (node.getNumChildren() == 0)
   {
     p.d_term = node;
+    p.d_sterm = node;
     d_term_partition[node] = p;
     return p;
   }
+  NodeManager* nm = NodeManager::currentNM();
+
+  Kind k = node.getKind();
+  bool isAssocComm = false;
+  // EQUAL is a special case here: we consider EQUAL to be associative,
+  // and handle the type polymorphism specially.
+  bool isAssoc = k == kind::EQUAL || theory::quantifiers::TermUtil::isAssoc(k);
+  // for now, only consider commutative operators that are also associative
+  if (isAssoc)
+  {
+    isAssocComm = theory::quantifiers::TermUtil::isComm(k);
+  }
 
   // Children of node
   vector<Node> children;
@@ -98,193 +573,206 @@ SymmetryDetect::Partition SymmetryDetect::findPartitions(Node node)
   vector<Partition> partitions;
 
   // Get all children of node
-  Trace("sym-dt") << "[sym-dt] collectChildren for: " << node
-                  << " with operator " << node.getKind() << endl;
-  collectChildren(node, children);
-  Trace("sym-dt") << "[sym-dt] children: " << children
-                  << endl;
+  Trace("sym-dt-debug") << "[sym-dt] collectChildren for: " << node
+                        << " with operator " << node.getKind() << endl;
+  if (!isAssocComm)
+  {
+    children.insert(children.end(), node.begin(), node.end());
+  }
+  else
+  {
+    collectChildren(node, children);
+  }
+  Trace("sym-dt-debug") << "[sym-dt] children: " << children << endl;
 
   // Create partitions for children
+  std::unordered_set<unsigned> active_indices;
   for (vector<Node>::iterator children_it = children.begin();
        children_it != children.end();
        ++children_it)
   {
+    active_indices.insert(partitions.size());
     partitions.push_back(findPartitions(*children_it));
   }
-
-  Trace("sym-dt") << "----------------------------- Start processing "
-                     "partitions -------------------------------"
-                  << endl;
-
-  PartitionTrie pt;
-  unordered_set<Node, NodeHashFunction> vars;
-
-  if (theory::quantifiers::TermUtil::isComm(node.getKind()))
-  {
-    // Start processing the singleton partitions and collect variables
-    processSingletonPartitions(partitions, vars);
-  }
-  else
+  if (Trace.isOn("sym-dt-debug"))
   {
-    // Get all the variables from the partitions
-    getVariables(partitions, vars);
-  }
-
-  // Build the partition trie
-  for (unordered_set<Node, NodeHashFunction>::iterator vars_it = vars.begin();
-       vars_it != vars.end();
-       ++vars_it)
-  {
-    pt.addNode(*vars_it, partitions);
+    Trace("sym-dt-debug") << "----------------------------- Start processing "
+                             "partitions for "
+                          << node << " -------------------------------" << endl;
+    for (unsigned j = 0, size = partitions.size(); j < size; j++)
+    {
+      Trace("sym-dt-debug") << "[" << j << "]: " << partitions[j].d_term
+                            << " --> " << partitions[j].d_sterm << std::endl;
+    }
+    Trace("sym-dt-debug") << "-----------------------------" << std::endl;
   }
 
-  // Get the new partition
-  pt.getNewPartition(p, pt);
-
-  // Reconstruct the node
-  Trace("sym-dt") << "[sym-dt] Reconstructing node: " << node << endl;
-  p.d_term = node;
-  d_term_partition[node] = p;
-  printPartition(p);
-  return p;
-}
-
-void SymmetryDetect::matches(vector<Partition>& partitions,
-                             map<Node, Node>& subvar_to_var,
-                             map<Node, Node>& subvar_to_expr)
-{
-  Trace("sym-dt")
-      << "[sym-dt] Start testing if singleton partitions can be merged!"
-      << endl;
-
-  if (!subvar_to_expr.empty())
+  if (isAssocComm)
   {
-    // Replacement variables
-    vector<Node> repls;
-    // Variables that have been merged
-    unordered_set<Node, NodeHashFunction> merged;
-    // Put the variable in repls
-    repls.push_back((subvar_to_expr.begin())->first);
-
-    for (map<Node, Node>::iterator expr_it1 = subvar_to_expr.begin();
-         expr_it1 != subvar_to_expr.end();
-         ++expr_it1)
+    // map substituted terms to indices in partitions
+    std::map<Node, std::vector<unsigned> > sterm_to_indices;
+    for (unsigned j = 0, size = partitions.size(); j < size; j++)
     {
-      // Skip expr_it1->first, if it has been merged
-      if (merged.find(expr_it1->first) != merged.end())
+      if (!partitions[j].d_sterm.isNull())
       {
-        continue;
+        sterm_to_indices[partitions[j].d_sterm].push_back(j);
       }
+    }
 
-      Partition p;
-      vector<Node> subs;
-      vector<Node> part;
-      Node fst_var = subvar_to_var.find(expr_it1->first)->second;
-
-      part.push_back(fst_var);
-      subs.push_back(fst_var);
-      merged.insert(expr_it1->first);
-      p.d_var_to_subvar[fst_var] = expr_it1->first;
-      Node sub_expr1 =
-          (expr_it1->second)
-              .substitute(subs.begin(), subs.end(), repls.begin(), repls.end());
-
-      for (map<Node, Node>::iterator expr_it2 = subvar_to_expr.begin();
-           expr_it2 != subvar_to_expr.end();
-           ++expr_it2)
+    for (const std::pair<Node, std::vector<unsigned> >& sti : sterm_to_indices)
+    {
+      Node cterm = sti.first;
+      if (Trace.isOn("sym-dt-debug"))
       {
-        if (merged.find(expr_it2->first) != merged.end())
-        {
-          continue;
-        }
-        if ((expr_it1->second).getType() != (expr_it2->second).getType())
+        Trace("sym-dt-debug") << "  indices[" << cterm << "] = ";
+        for (unsigned i : sti.second)
         {
-          continue;
-        }
-        vector<Node> subs2;
-        Node snd_var = subvar_to_var.find(expr_it2->first)->second;
-
-        subs2.push_back(snd_var);
-        Node sub_expr2 =
-            (expr_it2->second)
-                .substitute(
-                    subs2.begin(), subs2.end(), repls.begin(), repls.end());
-        Trace("sym-dt") << "[sym-dt] Testing if " << sub_expr1
-                        << " is equivalent to " << sub_expr2 << endl;
-
-        if (sub_expr1 == sub_expr2)
-        {
-          Trace("sym-dt") << "[sym-dt] Merge variable " << fst_var
-                          << " with variable " << snd_var << endl;
-          merged.insert(expr_it2->first);
-          part.push_back(snd_var);
-          p.d_var_to_subvar[snd_var] = expr_it1->first;
+          Trace("sym-dt-debug") << i << " ";
         }
+        Trace("sym-dt-debug") << std::endl;
       }
-      p.d_subvar_to_vars[expr_it1->first] = part;
-      Trace("sym-dt") << "[sym-dt] Add a new partition after merging: " << endl;
-      printPartition(p);
-      partitions.push_back(p);
+      // merge children, remove active indices
+      processPartitions(k, partitions, sti.second, active_indices);
     }
   }
-}
-
-void SymmetryDetect::processSingletonPartitions(
-    vector<Partition>& partitions, unordered_set<Node, NodeHashFunction>& vars)
-{
-  Trace("sym-dt") << "[sym-dt] Start post-processing partitions with size = "
-                  << partitions.size() << endl;
-
-  // Mapping between the substitution variable to the actual variable
-  map<Node, Node> subvar_to_var;
-  // Mapping between the substitution variable to the actual expression
-  map<Node, Node> subvar_to_expr;
-  // Partitions that have 2 or more variables
-  vector<Partition> new_partitions;
-
-  // Collect singleton partitions: subvar_to_expr, subvar_to_var, and variables
-  for (vector<Partition>::const_iterator part_it = partitions.begin();
-       part_it != partitions.end();
-       ++part_it)
+  // initially set substituted term to node
+  p.d_sterm = node;
+  // for all active indices
+  vector<Node> all_vars;
+  std::map<TypeNode, unsigned> type_index;
+  std::vector<Node> schildren;
+  if (!isAssocComm)
   {
-    if ((*part_it).d_var_to_subvar.size() == 1)
+    Assert(active_indices.size() == children.size());
+    // order matters, and there is no chance we merged children
+    schildren.resize(children.size());
+  }
+  std::vector<Partition> active_partitions;
+  for (const unsigned& i : active_indices)
+  {
+    Trace("sym-dt-debug") << "Reconstruct partition for active index : " << i
+                          << std::endl;
+    Partition& pa = partitions[i];
+    // ensure the variables of pa are fresh
+    std::vector<Node> f_vars;
+    std::vector<Node> f_subs;
+    // add to overall list of variables
+    for (const pair<const Node, vector<Node> >& pas : pa.d_subvar_to_vars)
     {
-      vars.insert(((*part_it).d_var_to_subvar.begin())->first);
-      subvar_to_expr[((*part_it).d_var_to_subvar.begin())->second] =
-          (*part_it).d_term;
-      subvar_to_var[((*part_it).d_var_to_subvar.begin())->second] =
-          ((*part_it).d_var_to_subvar.begin())->first;
+      Node v = pas.first;
+      Trace("sym-dt-debug")
+          << "...process " << v << " -> " << pas.second << std::endl;
+      Assert(!v.isNull());
+      TypeNode tnv = v.getType();
+      // ensure we use a new index for this variable
+      Node new_v = getSymBreakVariableInc(tnv, type_index);
+      f_vars.push_back(v);
+      f_subs.push_back(new_v);
+      // add all vars to partition trie classifier
+      for (const Node& c : pas.second)
+      {
+        if (std::find(all_vars.begin(), all_vars.end(), c) == all_vars.end())
+        {
+          all_vars.push_back(c);
+        }
+      }
+      for (const Node& x : pas.second)
+      {
+        Assert(x.getType() == new_v.getType());
+        pa.d_var_to_subvar[x] = new_v;
+        Trace("sym-dt-debug")
+            << "...set var to svar: " << x << " -> " << new_v << std::endl;
+      }
     }
-    else if ((*part_it).d_var_to_subvar.size() >= 2)
+    // reconstruct the partition
+    for (unsigned j = 0, size = f_vars.size(); j < size; j++)
     {
-      for (const pair<Node, Node>& var_to_subvar : (*part_it).d_var_to_subvar)
+      Node v = f_vars[j];
+      Node new_v = f_subs[j];
+      if (new_v != v)
       {
-        vars.insert(var_to_subvar.first);
+        pa.d_subvar_to_vars[new_v].insert(pa.d_subvar_to_vars[new_v].end(),
+                                          pa.d_subvar_to_vars[v].begin(),
+                                          pa.d_subvar_to_vars[v].end());
+        pa.d_subvar_to_vars.erase(v);
       }
-      // Only add partitions that have more than 1 variable
-      new_partitions.push_back(*part_it);
     }
+    Assert(f_vars.size() == f_subs.size());
+    Assert(!pa.d_sterm.isNull());
+    pa.d_sterm = pa.d_sterm.substitute(
+        f_vars.begin(), f_vars.end(), f_subs.begin(), f_subs.end());
+    if (isAssocComm)
+    {
+      Assert(!pa.d_sterm.isNull());
+      schildren.push_back(pa.d_sterm);
+    }
+    else
+    {
+      Assert(i < schildren.size());
+      schildren[i] = pa.d_sterm;
+    }
+    Trace("sym-dt-debug") << "...got : " << pa.d_sterm << std::endl;
+    active_partitions.push_back(pa);
   }
 
-  // Save all partitions that have more than 1 variable
-  partitions = new_partitions;
+  PartitionTrie pt;
+  std::map<Node, Node> var_to_svar;
+  type_index.clear();
+  // Build the partition trie
+  std::sort(all_vars.begin(), all_vars.end());
+  for (const Node& n : all_vars)
+  {
+    Node an = pt.addNode(n, active_partitions);
+    // if this is a new node, allocate
+    if (an == n)
+    {
+      Node new_v = getSymBreakVariableInc(n.getType(), type_index);
+      var_to_svar[n] = new_v;
+    }
+  }
 
-  // Do matches on singleton terms
-  if (!subvar_to_var.empty())
+  // Get the new partition
+  pt.getNewPartition(p, pt, var_to_svar);
+
+  // Reconstruct the node
+  p.d_term = node;
+  Assert(!p.d_sterm.isNull());
+  Trace("sym-dt-debug") << "[sym-dt] Reconstructing node: " << node
+                        << ", #children = " << schildren.size() << "/"
+                        << children.size() << endl;
+  if (isAssocComm)
+  {
+    p.d_sterm = mkAssociativeNode(k, schildren);
+  }
+  else
   {
-    matches(partitions, subvar_to_var, subvar_to_expr);
+    if (node.getMetaKind() == kind::metakind::PARAMETERIZED)
+    {
+      schildren.insert(schildren.begin(), node.getOperator());
+    }
+    p.d_sterm = nm->mkNode(k, schildren);
   }
+  Trace("sym-dt-debug") << "...return sterm: " << p.d_sterm << std::endl;
+  Trace("sym-dt-debug") << ".....types: " << p.d_sterm.getType() << " "
+                        << node.getType() << std::endl;
+  Assert(p.d_sterm.getType() == node.getType());
+
+  p.normalize();
+  d_term_partition[node] = p;
+  Partition::printPartition("sym-dt-debug", p);
+  return p;
 }
 
 void SymmetryDetect::collectChildren(Node node, vector<Node>& children)
 {
   Kind k = node.getKind();
+  Assert((k == kind::EQUAL || theory::quantifiers::TermUtil::isAssoc(k))
+         && theory::quantifiers::TermUtil::isComm(k));
 
-  if(!theory::quantifiers::TermUtil::isAssoc(k))
-  {
-    children.insert(children.end(), node.begin(), node.end());
-    return;
-  }
+  // must track the type of the children we are collecting
+  // this is to avoid having vectors of children with different type, like
+  // (= (= x 0) (= y "abc"))
+  TypeNode ctn = node[0].getType();
 
   Node cur;
   vector<Node> visit;
@@ -298,7 +786,8 @@ void SymmetryDetect::collectChildren(Node node, vector<Node>& children)
     if (visited.find(cur) == visited.end())
     {
       visited.insert(cur);
-      if (cur.getKind() == k)
+      if (cur.getNumChildren() > 0 && cur.getKind() == k
+          && cur[0].getType() == ctn)
       {
         for (const Node& cn : cur)
         {
@@ -313,147 +802,163 @@ void SymmetryDetect::collectChildren(Node node, vector<Node>& children)
   } while (!visit.empty());
 }
 
-void SymmetryDetect::PartitionTrie::getNewPartition(Partition& part,
-                                                    PartitionTrie& pt)
+/** A basic trie for storing vectors of arguments */
+class NodeTrie
 {
-  if (!pt.d_variables.empty())
+ public:
+  NodeTrie() : d_value(-1) {}
+  /** value of this node, -1 if unset */
+  int d_value;
+  /** children of this node */
+  std::map<Node, NodeTrie> d_children;
+  /** clear the children */
+  void clear() { d_children.clear(); }
+  /**
+   * Return true iff we've added the suffix of the vector of arguments starting
+   * at index before.
+   */
+  unsigned add(unsigned value,
+               const std::vector<Node>& args,
+               unsigned index = 0)
   {
-    vector<Node> vars;
-    Node fresh_var = NodeManager::currentNM()->mkSkolem(
-        "sym_bk", pt.d_variables[0].getType());
-    Trace("sym-dt")
-        << "[sym-dt] A partition from leaves of the partition trie:{";
-
-    for (vector<Node>::iterator var_it = pt.d_variables.begin();
-         var_it != pt.d_variables.end();
-         ++var_it)
+    if (index == args.size())
     {
-      Trace("sym-dt") << " " << *var_it;
-      vars.push_back(*var_it);
-      part.d_var_to_subvar[*var_it] = fresh_var;
-    }
-    Trace("sym-dt") << " }" << endl;
-    part.d_subvar_to_vars[fresh_var] = vars;
-  }
-  else
-  {
-    for (map<Node, PartitionTrie>::iterator part_it = pt.d_children.begin();
-         part_it != pt.d_children.end();
-         ++part_it)
-    {
-      getNewPartition(part, part_it->second);
+      if (d_value == -1)
+      {
+        d_value = static_cast<int>(value);
+      }
+      return d_value;
     }
+    return d_children[args[index]].add(value, args, index + 1);
   }
-}
+};
 
-void SymmetryDetect::getVariables(vector<Partition>& partitions,
-                                  unordered_set<Node, NodeHashFunction>& vars)
+void SymmetryDetect::processPartitions(
+    Kind k,
+    std::vector<Partition>& partitions,
+    const std::vector<unsigned>& indices,
+    std::unordered_set<unsigned>& active_indices)
 {
-  for (vector<Partition>::iterator part_it = partitions.begin();
-       part_it != partitions.end();
-       ++part_it)
+  Assert(!indices.empty());
+  unsigned first_index = indices[0];
+
+  unsigned num_sb_vars = partitions[first_index].d_subvar_to_vars.size();
+  if (num_sb_vars != 1)
   {
-    for (map<Node, vector<Node> >::iterator sub_var_it =
-             (*part_it).d_subvar_to_vars.begin();
-         sub_var_it != (*part_it).d_subvar_to_vars.end();
-         ++sub_var_it)
-    {
-      vars.insert((sub_var_it->second).begin(), (sub_var_it->second).end());
-    }
+    // can only handle symmetries that are classified by { n }
+    return;
   }
-}
-
-void SymmetryDetect::PartitionTrie::addNode(Node target_var,
-                                            vector<Partition>& partitions)
-{
-  Trace("sym-dt") << "[sym-dt] Add a variable {" << target_var
-                  << "} to the partition trie..." << endl;
-  vector<Node> subvars;
-
-  for (vector<Partition>::iterator part_it = partitions.begin();
-       part_it != partitions.end();
-       ++part_it)
+  // separate by number of variables
+  // for each n, nv_indices[n] contains the indices of partitions of the form
+  // { w1 -> { x1, ..., xn } }
+  std::map<unsigned, std::vector<unsigned> > nv_indices;
+  for (unsigned j = 0, size = indices.size(); j < size; j++)
   {
-    map<Node, Node>::iterator var_sub_it =
-        (*part_it).d_var_to_subvar.find(target_var);
-
-    if (var_sub_it != (*part_it).d_var_to_subvar.end())
+    unsigned index = indices[j];
+    Assert(partitions[index].d_subvar_to_vars.size() == 1);
+    unsigned num_vars = partitions[index].d_var_to_subvar.size();
+    nv_indices[num_vars].push_back(index);
+  }
+  for (const std::pair<const unsigned, std::vector<unsigned> >& nvi :
+       nv_indices)
+  {
+    if (nvi.second.size() <= 1)
     {
-      for (map<Node, vector<Node> >::iterator sub_vars_it =
-               (*part_it).d_subvar_to_vars.begin();
-           sub_vars_it != (*part_it).d_subvar_to_vars.end();
-           ++sub_vars_it)
+      // no symmetries
+      continue;
+    }
+    unsigned num_vars = nvi.first;
+    if (Trace.isOn("sym-dt-debug"))
+    {
+      Trace("sym-dt-debug") << "    nv_indices[" << num_vars << "] = ";
+      for (unsigned i : nvi.second)
       {
-        if (var_sub_it->second == sub_vars_it->first)
-        {
-          subvars.push_back(var_sub_it->second);
-        }
-        else
-        {
-          subvars.push_back(Node::null());
-        }
+        Trace("sym-dt-debug") << i << " ";
       }
+      Trace("sym-dt-debug") << std::endl;
     }
-    else
+    Trace("sym-dt-debug") << "Check for duplicates..." << std::endl;
+    // drop duplicates
+    // this ensures we don't double count equivalent children that were not
+    // syntactically identical e.g. (or (= x y) (= y x))
+    NodeTrie ntrie;
+    // non-duplicate indices
+    std::unordered_set<unsigned> nvis;
+    for (unsigned index : nvi.second)
     {
-      subvars.resize(subvars.size()+(*part_it).d_subvar_to_vars.size());
+      Partition& p = partitions[index];
+      std::vector<Node>& svs = p.d_subvar_to_vars.begin()->second;
+      unsigned aindex = ntrie.add(index, svs);
+      if (aindex == index)
+      {
+        nvis.insert(index);
+      }
+      else if (theory::quantifiers::TermUtil::isNonAdditive(k))
+      {
+        Trace("sym-dt-debug")
+            << "Drop duplicate child : " << index << std::endl;
+        Assert(active_indices.find(index) != active_indices.end());
+        active_indices.erase(index);
+      }
+      else
+      {
+        nvis.erase(aindex);
+      }
     }
+    std::vector<unsigned> check_indices;
+    check_indices.insert(check_indices.end(), nvis.begin(), nvis.end());
+    Trace("sym-dt-debug") << "Merge..." << std::endl;
+    // now, try to merge these partitions
+    mergePartitions(k, partitions, check_indices, active_indices);
   }
-
-  Trace("sym-dt") << "[sym-dt] Substitution variables for the variable "
-                  << target_var << ": " << subvars << endl;
-  addNode(target_var, subvars);
 }
 
-void SymmetryDetect::PartitionTrie::addNode(Node target_var,
-                                            vector<Node>& subvars)
+void SymmetryDetect::mergePartitions(
+    Kind k,
+    std::vector<Partition>& partitions,
+    const std::vector<unsigned>& indices,
+    std::unordered_set<unsigned>& active_indices)
 {
-  if (subvars.empty())
+  if (indices.size() <= 1)
   {
-    d_variables.push_back(target_var);
+    return;
   }
-  else
+  if (Trace.isOn("sym-dt-debug"))
   {
-    vector<Node> new_subs;
-    map<Node, PartitionTrie>::iterator children_it =
-        d_children.find(subvars[0]);
-
-    if (subvars.begin() + 1 < subvars.end())
-    {
-      new_subs.insert(new_subs.begin(), subvars.begin() + 1, subvars.end());
-    }
-    if (children_it != d_children.end())
+    Trace("sym-dt-debug") << "  merge indices ";
+    for (unsigned i : indices)
     {
-      (children_it->second).addNode(target_var, new_subs);
-    }
-    else
-    {
-      PartitionTrie pt;
-
-      pt.addNode(target_var, new_subs);
-      d_children[subvars[0]] = pt;
+      Trace("sym-dt-debug") << i << " ";
     }
+    Trace("sym-dt-debug") << std::endl;
   }
-}
+  Assert(!indices.empty());
 
-void SymmetryDetect::printPartition(Partition p)
-{
-  for (map<Node, vector<Node> >::iterator sub_vars_it =
-           p.d_subvar_to_vars.begin();
-       sub_vars_it != p.d_subvar_to_vars.end();
-       ++sub_vars_it)
-  {
-    Trace("sym-dt") << "[sym-dt] Partition: " << sub_vars_it->first << " -> {";
+  // initialize partition merger class
+  PartitionMerger pm;
+  pm.initialize(k, partitions, indices);
 
-    for (vector<Node>::iterator part_it = (sub_vars_it->second).begin();
-         part_it != (sub_vars_it->second).end();
-         ++part_it)
+  // TODO (#2198): process indices for distinct types separately
+  for (unsigned index : indices)
+  {
+    if (pm.merge(partitions, index, active_indices))
     {
-      Trace("sym-dt") << " " << *part_it;
+      Trace("sym-dt-debug") << "    ......we merged, recurse" << std::endl;
+      std::vector<unsigned> rem_indices;
+      for (unsigned ii : indices)
+      {
+        if (ii != index && active_indices.find(ii) != active_indices.end())
+        {
+          rem_indices.push_back(ii);
+        }
+      }
+      mergePartitions(k, partitions, rem_indices, active_indices);
+      return;
     }
-    Trace("sym-dt") << " }" << endl;
   }
 }
+
+}  // namespace symbreak
 }  // namespace passes
 }  // namespace preprocessing
 }  // namespace CVC4
diff --git a/src/preprocessing/passes/symmetry_detect.h b/src/preprocessing/passes/symmetry_detect.h
index 758169611..9a5f83868 100644
--- a/src/preprocessing/passes/symmetry_detect.h
+++ b/src/preprocessing/passes/symmetry_detect.h
@@ -25,6 +25,185 @@
 namespace CVC4 {
 namespace preprocessing {
 namespace passes {
+namespace symbreak {
+
+/**
+ * This class stores a "partition", which is a way of representing a
+ * class of symmetries.
+ *
+ * For example, when finding symmetries for a term like x+y = 0, we
+ * construct a partition { w -> { x, y } } that indicates that automorphisms
+ * over { x, y } do not affect the satisfiability of this term. In this
+ * example, we have the following assignments to the members of this class:
+ *   d_term : x+y=0
+ *   d_sterm : w+w=0
+ *   d_var_to_subvar : { x -> w, y -> w }
+ *   d_subvar_to_vars : { w -> { x, y } }
+ * We often identify a partition with its d_subvar_to_vars field.
+ *
+ * We call w a "symmetry breaking variable".
+ */
+class Partition
+{
+ public:
+  /** The term for which the partition was computed for. */
+  Node d_term;
+  /** Substituted term corresponding to the partition
+   *
+   * This is equal to d_term * d_var_to_subvar, where * is application of
+   * substitution.
+   */
+  Node d_sterm;
+  /**
+   * Mapping between the variable and the symmetry breaking variable e.g.
+   * { x -> w, y -> w }.
+   */
+  std::map<Node, Node> d_var_to_subvar;
+
+  /**
+   * Mapping between the symmetry breaking variables and variables, e.g.
+   * { w-> { x, y } }
+   */
+  std::map<Node, std::vector<Node> > d_subvar_to_vars;
+  /** sorts the ranges of d_subvar_to_vars. */
+  void normalize();
+  /** Print a partition */
+  static void printPartition(const char* c, Partition p);
+};
+
+/** partition merger
+ *
+ * This class is used to identify sets of children of commutative operators k
+ * that are identical up to a set of automorphisms.
+ *
+ * This class is used when we have detected symmetries for the children
+ * of a term t of the form <k>( t_1, ..., t_n ), where k is a commutative
+ * operator. For each i=1,...n, partitions[i] represents symmetries (in the
+ * form of a partition) computed for the child t_i.
+ *
+ * The vector d_indices of this class stores a list ( i_1...i_m ) such that
+ * ( t_i_j * partition[i_j].d_var_to_subvar ) is syntactically equivalent
+ * for each j=1...m, where * is application of substitution.
+ *
+ * In detail, we say that
+ *   partition[j1] = { w -> X_1 },
+ *   ...,
+ *   partition[jp] = { w -> X_p }
+ * are mergeable if s=|X_1|=...=|X_p|, and all subsets of
+ * X* = ( union_{k=1...p} X_k ) of size s are equal to exactly one of
+ * X_1 ... X_p.
+ */
+class PartitionMerger
+{
+ public:
+  PartitionMerger()
+      : d_kind(kind::UNDEFINED_KIND),
+        d_master_base_index(0),
+        d_num_new_indices_needed(0)
+  {
+  }
+  /** initialize this class
+   *
+   * We will be trying to merge the given partitions that occur at the given
+   * indices. k is the kind of the operator that partitions are children of.
+   */
+  void initialize(Kind k,
+                  const std::vector<Partition>& partitions,
+                  const std::vector<unsigned>& indices);
+  /** merge
+   *
+   * This method tries to "merge" partitions occurring at the indices d_indices
+   * of the vector partitions.
+   *
+   * Assuming the setting described above, if there exists a mergeable set of
+   * partitions with indices (j_m1...j_mp), we remove {j_m1...j_mp} \ { j_m1 }
+   * from active_indices, and update partition[j1] := { w -> X* }.
+   *
+   * The base_index is an index from d_indices that serves as a basis for
+   * detecting this symmetry. In particular, we start by assuming that
+   * p=1, and j_m1 is base_index. We proceed by trying to find sets of indices
+   * that add exactly one variable to X* at a time. We return
+   * true if p>1, that is, at least one partition was merged with the
+   * base_index.
+   */
+  bool merge(std::vector<Partition>& partitions,
+             unsigned base_index,
+             std::unordered_set<unsigned>& active_indices);
+
+ private:
+  /** the kind of the node we are consdiering */
+  Kind d_kind;
+  /** indices we are considering */
+  std::vector<unsigned> d_indices;
+  /** count the number of times each variable occurs */
+  std::map<Node, unsigned> d_occurs_count;
+  /** the number of times each variable occurs up to the given index */
+  std::map<unsigned, std::map<Node, unsigned> > d_occurs_by;
+  /** current master base index */
+  unsigned d_master_base_index;
+  /** the indices that occur in the current symmetry (the list (j1...jp)) */
+  std::unordered_set<unsigned> d_base_indices;
+  /** the free variables that occur in the current symmetry (the set X*)*/
+  std::unordered_set<Node, NodeHashFunction> d_base_vars;
+  /** the number of indices we need to add to extended X* by one variable */
+  unsigned d_num_new_indices_needed;
+  /** the variables we have currently tried to add to X* */
+  std::unordered_set<Node, NodeHashFunction> d_merge_var_tried;
+  /** merge new variable
+   *
+   * This is a recursive helper for the merge function. This function attempts
+   * to construct a set of indices {j1...jp} of partitions and a variable
+   * "merge_var" such that partitions[ji] is of the form { w -> X_ji }, where
+   * merge_var in X_ji and ( X_ji \ { merge_var } ) is a subset of the base
+   * variables X*. We require that p = d_num_new_indices_needed, where
+   * d_num_new_indices_needed is
+   *   |d_base_vars| choose (|X_ji|-1)
+   * that is, n!/((n-k)!*k!) where n=|d_base_vars| and k=|X_ji|-1.
+   *
+   * curr_index : the index of d_indices we are currently considering whether
+   * to add to new_indices,
+   * new_indices : the currently considered indices {j1...jp},
+   * merge_var : the variable we are currently trying to add to X*,
+   * new_merge_var_max : the maximum number of times that merge_var might
+   * appear in remainding indices, i.e. d_indices[curr_index]...d_indices.end(),
+   * which is used as an optimization for recognizing quickly when this method
+   * will fail.
+   */
+  bool mergeNewVar(unsigned curr_index,
+                   std::vector<unsigned>& new_indices,
+                   Node& merge_var,
+                   unsigned num_merge_var_max,
+                   std::vector<Partition>& partitions,
+                   std::unordered_set<unsigned>& active_indices);
+};
+/**
+ * We build the partition trie indexed by
+ * parts[0].var_to_subvar[v]....parts[n].var_to_subvar[v]. The leaves of a
+ * partition trie is the new regions of a partition
+ */
+class PartitionTrie
+{
+ public:
+  /** Variables at the leave */
+  std::vector<Node> d_variables;
+
+  /** The mapping from a node to its children */
+  std::map<Node, PartitionTrie> d_children;
+
+  /** Add variable v to the trie, indexed by
+   * parts[0].var_to_subvar[v]....parts[n].var_to_subvar[v]. */
+  Node addNode(Node v, std::vector<Partition>& parts);
+
+  /** Get all the new regions of a partition and store in part
+   *
+   * This constructs a new partition, part, where each set in this partition
+   * corresponds to one leaf in the PartitionTrie pt.
+   * var_to_svar: map from variables to symmetry variables to use in part.
+   */
+  void getNewPartition(Partition& part,
+                       PartitionTrie& pt,
+                       std::map<Node, Node>& var_to_svar);
+};
 
 /**
  * This is the class to detect symmetries from input based on terms equality.
@@ -54,49 +233,21 @@ class SymmetryDetect
   void getPartition(std::vector<std::vector<Node> >& parts, const std::vector<Node>& assertions);
 
  private:
+  /** (canonical) symmetry breaking variables for each type */
+  std::map<TypeNode, std::vector<Node> > d_sb_vars;
   /**
-   * This is the class to store the partition,
-   * where d_term store the term corresponding to the partition,
-   * d_var_to_subvar is the mapping from the variable to the substitution
-   * variable, and d_subvar_to_vars is the mapping from the substitution
-   * variable to a list of variables forming a region of a partition.
+   * Get the index^th symmetry breaking variable for type tn in the above
+   * vector. These are fresh variables of type tn which are used for
+   * constructing a canonical form for terms considered by this class, and
+   * are used in the domains of partitions (Partition::d_subvar_to_vars).
+   * This variable is created by this method if it does not already exist.
    */
-  class Partition
-  {
-   public:
-    /** Term corresponding to the partition, e.g., x + y = 0 */
-    Node d_term;
-    /** Mapping between the variable and the substitution variable x -> w, y -> w,
-     * z -> w */
-    std::map<Node, Node> d_var_to_subvar;
-
-    /** Mapping between the substitution variable and variables w-> { x, y, z } */
-    std::map<Node, std::vector<Node> > d_subvar_to_vars;
-  };
-
+  Node getSymBreakVariable(TypeNode tn, unsigned index);
   /**
-   * We build the partition trie indexed by
-   * parts[0].var_to_subvar[v]....parts[n].var_to_subvar[v]. The leaves of a
-   * partition trie is the new regions of a partition
+   * Get the index[tn]^th symmetry breaking variable for type tn using the
+   * above function and increment index[tn].
    */
-  class PartitionTrie
-  {
-   public:
-    /** Variables at the leave */
-    std::vector<Node> d_variables;
-
-    /** The mapping from a node to its children */
-    std::map<Node, PartitionTrie> d_children;
-
-    /** Add variable v to the trie, indexed by
-     * parts[0].var_to_subvar[v]....parts[n].var_to_subvar[v]. */
-    void addNode(Node v, std::vector<Partition>& parts);
-    void addNode(Node v, std::vector<Node>& subs);
-
-    /** Get all the new regions of a partition and store in part */
-    void getNewPartition(Partition& part, PartitionTrie& pt);
-  };
-
+  Node getSymBreakVariableInc(TypeNode tn, std::map<TypeNode, unsigned>& index);
 
   /** True and false constant nodes */
   Node d_trueNode;
@@ -115,7 +266,7 @@ class SymmetryDetect
   Partition detect(const std::vector<Node>& assertions);
 
   /** Find symmetries in node */
-  SymmetryDetect::Partition findPartitions(Node node);
+  Partition findPartitions(Node node);
 
   /** Collect children of a node
    *  If the kind of node is associative, we will chain its children together.
@@ -124,40 +275,40 @@ class SymmetryDetect
    * */
   void collectChildren(Node node, std::vector<Node>& children);
 
-  /** Print a partition */
-  void printPartition(Partition p);
-
-  /** Retrieve all variables from partitions and put in vars */
-  void getVariables(std::vector<Partition>& partitions,
-                    std::unordered_set<Node, NodeHashFunction>& vars);
-
-  /** Process singleton partitions and add all variables to vars
-   *  It collects all partitions with more than 1 variable and save it in
-   *  partitions first. And then it collects the substitution variable to
-   *  variable and to term mappings respectively from partitions with 1
-   *  variable and invokes matches function on the mappings to check
-   *  if any subset of the variables can be merged. If yes, they will be merged
-   *  and put in partitions. The remaining ones after the merge check will be
-   *  put in the partitions as well.
-   * */
-  void processSingletonPartitions(std::vector<Partition>& partitions,
-                                  std::unordered_set<Node, NodeHashFunction>& vars);
-
-  /** Do matches on singleton partitions
-   *  This function checks if any subset of the expressions corresponding to
-   *  substitution variables are equivalent under variables substitution.
-   *  If the expressions are equivalent, we will merge the variables corresponding
-   *  to the same substitution variables and put them in partitions.
-   *  For example, suppose we have subvar_to_var: {w1 -> u, w2 -> x, w3 -> y,
-   *  w4 -> z} and subvar_to_expr: {w1 -> u>2, w2 -> x>0, w3 -> y>0, w4 -> z>1}.
-   *  Since [x/w]>0 is equivalent [y/w]>0 but not equivalent to [z/w]>1 and [u/w]>2,
-   *  and [u/w]>2 is not equivalent to [z/w]>1, we would merge x and y and put
-   *  w5->{x, y} and also w1->{u}, w4->{z} in partitions.
-   * */
-  void matches(std::vector<Partition>& partitions,
-               std::map<Node, Node>& subvar_to_var,
-               std::map<Node, Node>& subvar_to_expr);
+  /** process partitions
+   *
+   * This method is called when we have detected symmetries for the children
+   * of a term t of the form <k>( t_1, ..., t_n ), where k is a commutative
+   * operator.  The vector indices stores a list ( i_1...i_m ) such that
+   * ( t_i_j * partition[i_j].d_var_to_subvar ) is syntactically equivalent
+   * for each j=1...m, where * is application of substitution. In particular,
+   * ( t_i_j * partition[i_j].d_var_to_subvar ) is equal to
+   * partitions[i_j].d_sterm for each j=1...m.
+   *
+   * This function calls mergePartitions on subsets of these indices for which
+   * it is possible to "merge" (see PartitionMerger). In particular, we consider
+   * subsets of indices whose corresponding partitions are of the form
+   *   { w -> { x1...xn } }
+   * for each n. This means that partitions like { w -> { x1 } } and
+   * { w -> { x1 x2 } } are considered separately when merging.
+   */
+  void processPartitions(Kind k,
+                         std::vector<Partition>& partitions,
+                         const std::vector<unsigned>& indices,
+                         std::unordered_set<unsigned>& active_indices);
+  /** merge partitions
+   *
+   * This method merges groups of partitions occurring in indices using the
+   * PartitionMerger class. Each merge updates one partition in partitions (the
+   * master index of the merge) and removes a set of indices from active_indices
+   * (the slave indices).
+   */
+  void mergePartitions(Kind k,
+                       std::vector<Partition>& partitions,
+                       const std::vector<unsigned>& indices,
+                       std::unordered_set<unsigned>& active_indices);
 };
+}  // namespace symbreak
 }  // namespace passes
 }  // namespace preprocessing
 }  // namespace CVC4