Improvements and fixes for symmetry detection and breaking (#2459)

This fixes a few open issues with symmetry detection algorithm. It also extends the algorithm to do:
- Alpha equivalence to recognize symmetries between quantified formulas,
- A technique to recognize a subset of variables in two terms are symmetric, e.g. from x in A ^ x in B, we find A and B are interchangeable by treating x as a fixed symbol,
- Symmetry breaking for maximal subterms instead of variables.

3 files changed, 644 insertions, 248 deletions

diff --git a/src/preprocessing/passes/symmetry_breaker.cpp b/src/preprocessing/passes/symmetry_breaker.cpp
index c32057d5f..1e4b9853d 100644
--- a/src/preprocessing/passes/symmetry_breaker.cpp
+++ b/src/preprocessing/passes/symmetry_breaker.cpp
@@ -16,6 +16,7 @@
 #include "preprocessing/passes/symmetry_detect.h"
 
 using namespace std;
+using namespace CVC4::kind;
 
 namespace CVC4 {
 namespace preprocessing {
@@ -31,8 +32,12 @@ Node SymmetryBreaker::generateSymBkConstraints(const vector<vector<Node>>& parts
     if (part.size() >= 2)
     {
       Kind kd = getOrderKind(part[0]);
-
-      if (kd != kind::EQUAL)
+      if (kd == UNDEFINED_KIND)
+      {
+        // no symmetry breaking possible
+        continue;
+      }
+      if (kd != EQUAL)
       {
         for (unsigned int i = 0; i < part.size() - 1; ++i)
         {
@@ -50,12 +55,11 @@ Node SymmetryBreaker::generateSymBkConstraints(const vector<vector<Node>>& parts
         {
           for (unsigned int j = i + 2; j < part.size(); ++j)
           {
-            // Generate consecutive constraints v_i = v_j => v_i = v_{j-1} for all 0
-            // <= i < j-1 < j < part.size()
-            Node constraint = nm->mkNode(
-                kind::IMPLIES,
-                nm->mkNode(kd, part[i], part[j]),
-                nm->mkNode(kd, part[i], part[j - 1]));
+            // Generate consecutive constraints v_i = v_j => v_i = v_{j-1},
+            // for all 0 <= i < j-1 < j < part.size()
+            Node constraint = nm->mkNode(IMPLIES,
+                                         nm->mkNode(kd, part[i], part[j]),
+                                         nm->mkNode(kd, part[i], part[j - 1]));
             constraints.push_back(constraint);
             Trace("sym-bk")
                 << "[sym-bk] Generate a symmetry breaking constraint: "
@@ -74,15 +78,14 @@ Node SymmetryBreaker::generateSymBkConstraints(const vector<vector<Node>>& parts
               if(prev_seg_start_index >= 0)
               {
                 rhs = nm->mkNode(
-                    kind::OR,
+                    OR,
                     rhs,
-                    nm->mkNode(kd, part[i-1], part[prev_seg_start_index]));
+                    nm->mkNode(kd, part[i - 1], part[prev_seg_start_index]));
               }
               // Generate length order constraints
               // v_i = v_j => (v_{i} = v_{i-1} OR v_{i-1} = x_{(i-1)-(j-i)})
               // for all 1 <= i < j < part.size() and (i-1)-(j-i) >= 0
-              Node constraint =
-                  nm->mkNode(kind::IMPLIES, lhs, rhs);
+              Node constraint = nm->mkNode(IMPLIES, lhs, rhs);
               constraints.push_back(constraint);
               Trace("sym-bk")
                   << "[sym-bk] Generate a symmetry breaking constraint: "
@@ -101,23 +104,29 @@ Node SymmetryBreaker::generateSymBkConstraints(const vector<vector<Node>>& parts
   {
     return constraints[0];
   }
-  return nm->mkNode(kind::AND, constraints);
+  return nm->mkNode(AND, constraints);
 }
 
 Kind SymmetryBreaker::getOrderKind(Node node)
 {
-  if (node.getType().isInteger() || node.getType().isReal())
+  TypeNode tn = node.getType();
+  if (tn.isBoolean())
+  {
+    return IMPLIES;
+  }
+  else if (tn.isReal())
   {
-    return kind::LEQ;
+    return LEQ;
   }
-  else if (node.getType().isBitVector())
+  else if (tn.isBitVector())
   {
-    return kind::BITVECTOR_ULE;
+    return BITVECTOR_ULE;
   }
-  else
+  if (tn.isFirstClass())
   {
-    return kind::EQUAL;
+    return EQUAL;
   }
+  return UNDEFINED_KIND;
 }
 
 SymBreakerPass::SymBreakerPass(PreprocessingPassContext* preprocContext)
@@ -128,27 +137,37 @@ PreprocessingPassResult SymBreakerPass::applyInternal(
 {
   Trace("sym-break-pass") << "Apply symmetry breaker pass..." << std::endl;
   // detect symmetries
-  std::vector<std::vector<Node>> part;
+  std::vector<std::vector<Node>> sterms;
   symbreak::SymmetryDetect symd;
-  symd.getPartition(part, assertionsToPreprocess->ref());
-  if (Trace.isOn("sym-break-pass"))
+  symd.computeTerms(sterms, assertionsToPreprocess->ref());
+  if (Trace.isOn("sym-break-pass") || Trace.isOn("sb-constraint"))
   {
-    Trace("sym-break-pass") << "Detected symmetry partition:" << std::endl;
-    for (const std::vector<Node>& p : part)
+    if (sterms.empty())
     {
-      Trace("sym-break-pass") << "  " << p << std::endl;
+      Trace("sym-break-pass") << "Detected no symmetric terms." << std::endl;
+    }
+    else
+    {
+      Trace("sb-constraint") << "; found symmetry" << std::endl;
+      Trace("sym-break-pass") << "Detected symmetric terms:" << std::endl;
+      for (const std::vector<Node>& p : sterms)
+      {
+        Trace("sym-break-pass") << "  " << p << std::endl;
+      }
     }
   }
   // construct the symmetry breaking constraint
   Trace("sym-break-pass") << "Construct symmetry breaking constraint..."
                           << std::endl;
   SymmetryBreaker symb;
-  Node sbConstraint = symb.generateSymBkConstraints(part);
+  Node sbConstraint = symb.generateSymBkConstraints(sterms);
   // add symmetry breaking constraint to the set of assertions
   Trace("sym-break-pass") << "...got: " << sbConstraint << std::endl;
   // if not true
   if (!sbConstraint.isConst())
   {
+    Trace("sb-constraint") << "(symmetry-break " << sbConstraint << ")"
+                           << std::endl;
     // add to assertions
     assertionsToPreprocess->push_back(sbConstraint);
   }
diff --git a/src/preprocessing/passes/symmetry_detect.cpp b/src/preprocessing/passes/symmetry_detect.cpp
index a1273b1d9..24db144e4 100644
--- a/src/preprocessing/passes/symmetry_detect.cpp
+++ b/src/preprocessing/passes/symmetry_detect.cpp
@@ -13,10 +13,13 @@
  **/
 
 #include "preprocessing/passes/symmetry_detect.h"
+#include "expr/node_algorithm.h"
+#include "theory/quantifiers/alpha_equivalence.h"
 #include "theory/quantifiers/term_util.h"
 #include "theory/rewriter.h"
 
 using namespace std;
+using namespace CVC4::kind;
 
 namespace CVC4 {
 namespace preprocessing {
@@ -91,6 +94,25 @@ void Partition::printPartition(const char* c, Partition p)
   }
 }
 
+void Partition::addVariable(Node sv, Node v)
+{
+  d_subvar_to_vars[sv].push_back(v);
+  Assert(d_var_to_subvar.find(v) == d_var_to_subvar.end());
+  d_var_to_subvar[v] = sv;
+}
+
+void Partition::removeVariable(Node sv)
+{
+  std::map<Node, std::vector<Node> >::iterator its = d_subvar_to_vars.find(sv);
+  Assert(its != d_subvar_to_vars.end());
+  for (const Node& v : its->second)
+  {
+    Assert(d_var_to_subvar.find(v) != d_var_to_subvar.end());
+    d_var_to_subvar.erase(v);
+  }
+  d_subvar_to_vars.erase(sv);
+}
+
 void Partition::normalize()
 {
   for (std::pair<const Node, std::vector<Node> > p : d_subvar_to_vars)
@@ -98,12 +120,30 @@ void Partition::normalize()
     std::sort(p.second.begin(), p.second.end());
   }
 }
+void Partition::getVariables(std::vector<Node>& vars)
+{
+  for (const std::pair<const Node, Node>& p : d_var_to_subvar)
+  {
+    vars.push_back(p.first);
+  }
+}
+
+void Partition::getSubstitution(std::vector<Node>& vars,
+                                std::vector<Node>& subs)
+{
+  for (const std::pair<const Node, Node>& p : d_var_to_subvar)
+  {
+    vars.push_back(p.first);
+    subs.push_back(p.second);
+  }
+}
 
 void PartitionMerger::initialize(Kind k,
                                  const std::vector<Partition>& partitions,
                                  const std::vector<unsigned>& indices)
 {
   d_kind = k;
+  Trace("sym-dt-debug") << "Initialize partition merger..." << std::endl;
   Trace("sym-dt-debug") << "Count variable occurrences..." << std::endl;
   for (unsigned index : indices)
   {
@@ -136,7 +176,8 @@ void PartitionMerger::initialize(Kind k,
 
 bool PartitionMerger::merge(std::vector<Partition>& partitions,
                             unsigned base_index,
-                            std::unordered_set<unsigned>& active_indices)
+                            std::unordered_set<unsigned>& active_indices,
+                            std::vector<unsigned>& merged_indices)
 {
   Assert(base_index < partitions.size());
   d_master_base_index = base_index;
@@ -185,7 +226,18 @@ bool PartitionMerger::merge(std::vector<Partition>& partitions,
     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;
+      if (Trace.isOn("sym-dt-debug"))
+      {
+        Trace("sym-dt-debug")
+            << "   ...merged: " << merge_var << " from indices [ ";
+        for (unsigned ni : new_indices)
+        {
+          Trace("sym-dt-debug") << ni << " ";
+        }
+        Trace("sym-dt-debug") << "]" << std::endl;
+      }
+      merged_indices.insert(
+          merged_indices.end(), new_indices.begin(), new_indices.end());
       Assert(!merge_var.isNull());
       merged = true;
       success = true;
@@ -219,7 +271,9 @@ bool PartitionMerger::mergeNewVar(unsigned curr_index,
     return false;
   }
   Trace("sym-dt-debug2") << "merge " << curr_index << " / " << d_indices.size()
-                         << std::endl;
+                         << ", merge var : " << merge_var
+                         << ", upper bound for #occ of merge_var : "
+                         << num_merge_var_max << std::endl;
   // try to include this index
   unsigned index = d_indices[curr_index];
 
@@ -229,6 +283,7 @@ bool PartitionMerger::mergeNewVar(unsigned curr_index,
     Assert(active_indices.find(index) != active_indices.end());
     // check whether it can merge
     Partition& p = partitions[index];
+    Trace("sym-dt-debug2") << "current term is " << p.d_term << std::endl;
     Assert(p.d_subvar_to_vars.size() == 1);
     std::vector<Node>& svs = p.d_subvar_to_vars.begin()->second;
     bool include_success = true;
@@ -286,7 +341,8 @@ bool PartitionMerger::mergeNewVar(unsigned curr_index,
         include_success = false;
       }
     }
-    else if (!include_success && !merge_var.isNull())
+    else if (!merge_var.isNull()
+             && p.d_var_to_subvar.find(merge_var) != p.d_var_to_subvar.end())
     {
       // decrement
       num_merge_var_max--;
@@ -312,7 +368,7 @@ bool PartitionMerger::mergeNewVar(unsigned curr_index,
         // can now include in the base
         d_base_vars.insert(merge_var);
         Trace("sym-dt-debug") << "found symmetry : { ";
-        for (const unsigned& i : new_indices)
+        for (unsigned i : new_indices)
         {
           Assert(d_base_indices.find(i) == d_base_indices.end());
           d_base_indices.insert(i);
@@ -332,10 +388,9 @@ bool PartitionMerger::mergeNewVar(unsigned curr_index,
         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;
+        p.addVariable(sb_v, merge_var);
         return true;
       }
       if (mergeNewVar(curr_index + 1,
@@ -369,70 +424,10 @@ bool PartitionMerger::mergeNewVar(unsigned curr_index,
                      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)
+SymmetryDetect::SymmetryDetect() : d_tsym_id_counter(1)
 {
-  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];
+  d_trueNode = NodeManager::currentNM()->mkConst<bool>(true);
+  d_falseNode = NodeManager::currentNM()->mkConst<bool>(false);
 }
 
 Partition SymmetryDetect::detect(const vector<Node>& assertions)
@@ -471,15 +466,12 @@ Node SymmetryDetect::getSymBreakVariable(TypeNode tn, unsigned index)
     d_sb_vars[tn].clear();
     it = d_sb_vars.find(tn);
   }
+  NodeManager* nm = NodeManager::currentNM();
   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);
+    Node fresh_var = nm->mkBoundVar(ss.str(), tn);
     it->second.push_back(fresh_var);
   }
   return it->second[index];
@@ -499,11 +491,12 @@ Node SymmetryDetect::getSymBreakVariableInc(TypeNode tn,
   return getSymBreakVariable(tn, new_index);
 }
 
-void SymmetryDetect::getPartition(vector<vector<Node> >& parts,
-                                  const vector<Node>& assertions)
+void SymmetryDetect::compute(std::vector<std::vector<Node> >& part,
+                             const std::vector<Node>& assertions)
 {
   Partition p = detect(assertions);
 
+  std::vector<std::vector<Node> > parts;
   for (map<Node, vector<Node> >::const_iterator subvar_to_vars_it =
            p.d_subvar_to_vars.begin();
        subvar_to_vars_it != p.d_subvar_to_vars.end();
@@ -512,6 +505,98 @@ void SymmetryDetect::getPartition(vector<vector<Node> >& parts,
     parts.push_back(subvar_to_vars_it->second);
   }
 }
+void SymmetryDetect::computeTerms(std::vector<std::vector<Node> >& sterms,
+                                  const std::vector<Node>& assertions)
+{
+  Partition p = detect(assertions);
+
+  for (const std::pair<const Node, std::vector<Node> > sp : p.d_subvar_to_vars)
+  {
+    if (sp.second.size() > 1)
+    {
+      // A naive method would do sterms.push_back(sp.second), that is, say that
+      // the variables themselves are symmetric terms. However, the following
+      // code finds some subterms of assertions that are symmetric under this
+      // set in the variable partition. For example, for the input:
+      //   f(x)+f(y) >= 0
+      // naively {x, y} are reported as symmetric terms, but below ensures we
+      // say {f(x), f(y)} are reported as symmetric terms instead.
+      Node sv = sp.first;
+      Trace("sym-dt-tsym-cons")
+          << "Construct term symmetry from " << sp.second << "..." << std::endl;
+      // choose an arbitrary term symmetry
+      std::vector<unsigned>& tsids = d_var_to_tsym_ids[sp.second[0]];
+      if (tsids.empty())
+      {
+        // no (ground) term symmetries, just use naive
+        sterms.push_back(sp.second);
+      }
+      else
+      {
+        unsigned tsymId = tsids[tsids.size() - 1];
+        Trace("sym-dt-tsym-cons") << "...use tsym id " << tsymId << std::endl;
+        // get the substitution
+        std::vector<Node> vars;
+        std::vector<Node> subs;
+        for (const Node& v : sp.second)
+        {
+          vars.push_back(v);
+          subs.push_back(sv);
+        }
+        std::vector<Node>& tsym = d_tsyms[tsymId];
+        // map terms in this symmetry to their final form
+        std::vector<unsigned> tsym_indices;
+        std::vector<Node> tsym_terms;
+        for (unsigned j = 0, size = tsym.size(); j < size; j++)
+        {
+          Node tst = tsym[j];
+          Node tsts = tst.substitute(
+              vars.begin(), vars.end(), subs.begin(), subs.end());
+          tsym_indices.push_back(j);
+          tsym_terms.push_back(tsts);
+        }
+        // take into account alpha-equivalence
+        std::map<Node, std::vector<unsigned> > t_to_st;
+        computeAlphaEqTerms(tsym_indices, tsym_terms, t_to_st);
+        Node tshUse;
+        for (const std::pair<const Node, std::vector<unsigned> >& tsh : t_to_st)
+        {
+          Trace("sym-dt-tsym-cons-debug")
+              << "  " << tsh.first << " -> #" << tsh.second.size() << std::endl;
+          if (tsh.second.size() > 1)
+          {
+            tshUse = tsh.first;
+            break;
+          }
+        }
+        if (!tshUse.isNull())
+        {
+          std::vector<Node> tsymCons;
+          for (unsigned j : t_to_st[tshUse])
+          {
+            tsymCons.push_back(tsym[j]);
+          }
+          Trace("sym-dt-tsym-cons") << "...got " << tsymCons << std::endl;
+          sterms.push_back(tsymCons);
+        }
+      }
+    }
+  }
+}
+
+/**
+ * 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 are 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;
+};
 
 Partition SymmetryDetect::findPartitions(Node node)
 {
@@ -535,14 +620,11 @@ Partition SymmetryDetect::findPartitions(Node node)
   // If node is a variable
   if (node.isVar() && node.getKind() != kind::BOUND_VARIABLE)
   {
-    vector<Node> vars;
     TypeNode type = node.getType();
     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;
+    p.addVariable(fresh_var, node);
     d_term_partition[node] = p;
     return p;
   }
@@ -567,14 +649,18 @@ Partition SymmetryDetect::findPartitions(Node node)
     isAssocComm = theory::quantifiers::TermUtil::isComm(k);
   }
 
-  // Children of node
-  vector<Node> children;
-  // Partitions of children
-  vector<Partition> partitions;
-
   // Get all children of node
   Trace("sym-dt-debug") << "[sym-dt] collectChildren for: " << node
-                        << " with operator " << node.getKind() << endl;
+                        << " with kind " << node.getKind() << endl;
+  // Children of node
+  std::vector<Node> children;
+  bool operatorChild = false;
+  if (node.getKind() == APPLY_UF)
+  {
+    // compute for the operator
+    children.push_back(node.getOperator());
+    operatorChild = true;
+  }
   if (!isAssocComm)
   {
     children.insert(children.end(), node.begin(), node.end());
@@ -585,14 +671,14 @@ Partition SymmetryDetect::findPartitions(Node node)
   }
   Trace("sym-dt-debug") << "[sym-dt] children: " << children << endl;
 
+  // Partitions of children
+  std::vector<Partition> partitions;
   // Create partitions for children
   std::unordered_set<unsigned> active_indices;
-  for (vector<Node>::iterator children_it = children.begin();
-       children_it != children.end();
-       ++children_it)
+  for (const Node& c : children)
   {
     active_indices.insert(partitions.size());
-    partitions.push_back(findPartitions(*children_it));
+    partitions.push_back(findPartitions(c));
   }
   if (Trace.isOn("sym-dt-debug"))
   {
@@ -609,15 +695,21 @@ Partition SymmetryDetect::findPartitions(Node node)
 
   if (isAssocComm)
   {
-    // map substituted terms to indices in partitions
-    std::map<Node, std::vector<unsigned> > sterm_to_indices;
+    // get the list of indices and terms
+    std::vector<unsigned> indices;
+    std::vector<Node> sterms;
     for (unsigned j = 0, size = partitions.size(); j < size; j++)
     {
-      if (!partitions[j].d_sterm.isNull())
+      Node st = partitions[j].d_sterm;
+      if (!st.isNull())
       {
-        sterm_to_indices[partitions[j].d_sterm].push_back(j);
+        indices.push_back(j);
+        sterms.push_back(st);
       }
     }
+    // now, compute terms to indices
+    std::map<Node, std::vector<unsigned> > sterm_to_indices;
+    computeAlphaEqTerms(indices, sterms, sterm_to_indices);
 
     for (const std::pair<Node, std::vector<unsigned> >& sti : sterm_to_indices)
     {
@@ -632,42 +724,26 @@ Partition SymmetryDetect::findPartitions(Node node)
         Trace("sym-dt-debug") << std::endl;
       }
       // merge children, remove active indices
-      processPartitions(k, partitions, sti.second, active_indices);
+      std::vector<Node> fixedSVar;
+      std::vector<Node> fixedVar;
+      processPartitions(
+          k, partitions, sti.second, active_indices, fixedSVar, fixedVar);
     }
   }
   // 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)
-  {
-    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)
+  for (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)
     {
-      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);
+          << "...process " << pas.first << " -> " << pas.second << std::endl;
       // add all vars to partition trie classifier
       for (const Node& c : pas.second)
       {
@@ -676,67 +752,140 @@ Partition SymmetryDetect::findPartitions(Node node)
           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;
-      }
     }
-    // reconstruct the partition
-    for (unsigned j = 0, size = f_vars.size(); j < size; j++)
+    Trace("sym-dt-debug") << "...term : " << pa.d_sterm << std::endl;
+  }
+
+  PartitionTrie pt;
+  std::map<TypeNode, unsigned> type_index;
+  type_index.clear();
+  // the indices we need to reconstruct
+  std::map<unsigned, bool> rcons_indices;
+  // Build the partition trie
+  std::sort(all_vars.begin(), all_vars.end());
+  // for each variable
+  for (const Node& n : all_vars)
+  {
+    Trace("sym-dt-debug") << "[sym-dt] Add a variable {" << n
+                          << "} to the partition trie, #partitions = "
+                          << active_indices.size() << "..." << endl;
+    std::vector<Node> subvars;
+    std::vector<unsigned> useVarInd;
+    Node useVar;
+    for (unsigned i : active_indices)
     {
-      Node v = f_vars[j];
-      Node new_v = f_subs[j];
-      if (new_v != v)
+      Partition& pa = partitions[i];
+      std::map<Node, Node>::iterator var_sub_it = pa.d_var_to_subvar.find(n);
+      if (var_sub_it != pa.d_var_to_subvar.end())
       {
-        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);
+        Node v = var_sub_it->second;
+        subvars.push_back(v);
+        if (useVar.isNull() || v == useVar)
+        {
+          useVar = v;
+          useVarInd.push_back(i);
+        }
+        else
+        {
+          // will need to reconstruct the child
+          rcons_indices[i] = true;
+        }
+      }
+      else
+      {
+        subvars.push_back(Node::null());
       }
     }
-    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)
+    // all variables should occur in at least one child
+    Assert(!useVar.isNull());
+    Trace("sym-dt-debug")
+        << "[sym-dt] Symmetry breaking variables for the variable " << n << ": "
+        << subvars << endl;
+    // add to the trie
+    PartitionTrie* curr = &pt;
+    for (const Node& c : subvars)
+    {
+      curr = &(curr->d_children[c]);
+    }
+    curr->d_variables.push_back(n);
+
+    // allocate the necessary variable
+    bool usingUseVar = false;
+    if (curr->d_variables.size() > 1)
+    {
+      // must use the previous
+      Node an = curr->d_variables[0];
+      useVar = p.d_var_to_subvar[an];
+      Trace("sym-dt-debug") << "...use var from " << an << "." << std::endl;
+    }
+    else if (useVar.isNull()
+             || p.d_subvar_to_vars.find(useVar) != p.d_subvar_to_vars.end())
     {
-      Assert(!pa.d_sterm.isNull());
-      schildren.push_back(pa.d_sterm);
+      Trace("sym-dt-debug") << "...allocate new var." << std::endl;
+      // must allocate new
+      TypeNode ntn = n.getType();
+      do
+      {
+        useVar = getSymBreakVariableInc(ntn, type_index);
+      } while (p.d_subvar_to_vars.find(useVar) != p.d_subvar_to_vars.end());
     }
     else
     {
-      Assert(i < schildren.size());
-      schildren[i] = pa.d_sterm;
+      Trace("sym-dt-debug") << "...reuse var." << std::endl;
+      usingUseVar = true;
+    }
+    if (!usingUseVar)
+    {
+      // can't use the useVar, indicate indices for reconstruction
+      for (unsigned ui : useVarInd)
+      {
+        rcons_indices[ui] = true;
+      }
     }
-    Trace("sym-dt-debug") << "...got : " << pa.d_sterm << std::endl;
-    active_partitions.push_back(pa);
+    Trace("sym-dt-debug") << "[sym-dt] Map : " << n << " -> " << useVar
+                          << std::endl;
+    p.addVariable(useVar, n);
   }
 
-  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)
+  std::vector<Node> pvars;
+  std::vector<Node> psubs;
+  if (!rcons_indices.empty())
+  {
+    p.getSubstitution(pvars, psubs);
+  }
+
+  // Reconstruct the substituted node
+  p.d_term = node;
+  std::vector<Node> schildren;
+  if (!isAssocComm)
   {
-    Node an = pt.addNode(n, active_partitions);
-    // if this is a new node, allocate
-    if (an == n)
+    Assert(active_indices.size() == children.size());
+    // order matters, and there is no chance we merged children
+    schildren.resize(children.size());
+  }
+  for (unsigned i : active_indices)
+  {
+    Partition& pa = partitions[i];
+    Node sterm = pa.d_sterm;
+    Assert(!sterm.isNull());
+    if (rcons_indices.find(i) != rcons_indices.end())
+    {
+      // must reconstruct via a substitution
+      Trace("sym-dt-debug2") << "  reconstruct index " << i << std::endl;
+      sterm = pa.d_term.substitute(
+          pvars.begin(), pvars.end(), psubs.begin(), psubs.end());
+    }
+    if (isAssocComm)
+    {
+      schildren.push_back(sterm);
+    }
+    else
     {
-      Node new_v = getSymBreakVariableInc(n.getType(), type_index);
-      var_to_svar[n] = new_v;
+      Assert(i < schildren.size());
+      schildren[i] = sterm;
     }
   }
 
-  // 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;
@@ -746,7 +895,7 @@ Partition SymmetryDetect::findPartitions(Node node)
   }
   else
   {
-    if (node.getMetaKind() == kind::metakind::PARAMETERIZED)
+    if (node.getMetaKind() == metakind::PARAMETERIZED && !operatorChild)
     {
       schildren.insert(schildren.begin(), node.getOperator());
     }
@@ -757,6 +906,7 @@ Partition SymmetryDetect::findPartitions(Node node)
                         << node.getType() << std::endl;
   Assert(p.d_sterm.getType() == node.getType());
 
+  // normalize: ensures that variable lists are sorted
   p.normalize();
   d_term_partition[node] = p;
   Partition::printPartition("sym-dt-debug", p);
@@ -802,13 +952,54 @@ void SymmetryDetect::collectChildren(Node node, vector<Node>& children)
   } while (!visit.empty());
 }
 
+void SymmetryDetect::computeAlphaEqTerms(
+    const std::vector<unsigned>& indices,
+    const std::vector<Node>& sterms,
+    std::map<Node, std::vector<unsigned> >& sterm_to_indices)
+{
+  Assert(indices.size() == sterms.size());
+  // also store quantified formulas, since these may be alpha-equivalent
+  std::vector<unsigned> quant_sterms;
+  for (unsigned j = 0, size = indices.size(); j < size; j++)
+  {
+    Node st = sterms[j];
+    Assert(!st.isNull());
+    if (st.getKind() == FORALL)
+    {
+      quant_sterms.push_back(j);
+    }
+    else
+    {
+      sterm_to_indices[st].push_back(indices[j]);
+    }
+  }
+  // process the quantified formulas
+  if (quant_sterms.size() == 1)
+  {
+    // only one quantified formula, won't be alpha equivalent
+    unsigned j = quant_sterms[0];
+    sterm_to_indices[sterms[j]].push_back(indices[j]);
+  }
+  else if (!quant_sterms.empty())
+  {
+    theory::quantifiers::AlphaEquivalenceDb aedb(&d_tcanon);
+    for (unsigned j : quant_sterms)
+    {
+      // project via alpha equivalence
+      Node st = sterms[j];
+      Node st_ae = aedb.addTerm(st);
+      sterm_to_indices[st_ae].push_back(indices[j]);
+    }
+  }
+}
+
 /** A basic trie for storing vectors of arguments */
 class NodeTrie
 {
  public:
-  NodeTrie() : d_value(-1) {}
-  /** value of this node, -1 if unset */
-  int d_value;
+  NodeTrie() {}
+  /** value at this node*/
+  std::vector<unsigned> d_value;
   /** children of this node */
   std::map<Node, NodeTrie> d_children;
   /** clear the children */
@@ -823,11 +1014,8 @@ class NodeTrie
   {
     if (index == args.size())
     {
-      if (d_value == -1)
-      {
-        d_value = static_cast<int>(value);
-      }
-      return d_value;
+      d_value.push_back(value);
+      return d_value[0];
     }
     return d_children[args[index]].add(value, args, index + 1);
   }
@@ -837,15 +1025,125 @@ void SymmetryDetect::processPartitions(
     Kind k,
     std::vector<Partition>& partitions,
     const std::vector<unsigned>& indices,
-    std::unordered_set<unsigned>& active_indices)
+    std::unordered_set<unsigned>& active_indices,
+    std::vector<Node>& fixedSVar,
+    std::vector<Node>& fixedVar)
 {
   Assert(!indices.empty());
   unsigned first_index = indices[0];
-
+  if (Trace.isOn("sym-dt-debug"))
+  {
+    Trace("sym-dt-debug") << "[sym-dt] process partitions for ";
+    for (unsigned i : indices)
+    {
+      Trace("sym-dt-debug") << i << " ";
+    }
+    Trace("sym-dt-debug") << std::endl;
+  }
   unsigned num_sb_vars = partitions[first_index].d_subvar_to_vars.size();
-  if (num_sb_vars != 1)
+  if (num_sb_vars == 0)
   {
-    // can only handle symmetries that are classified by { n }
+    // no need to merge
+    Trace("sym-dt-debug") << "...trivial (no sym vars)" << std::endl;
+    return;
+  }
+  if (num_sb_vars > 1)
+  {
+    // see if we can drop, e.g. {x}{A}, {x}{B} ---> {A}, {B}
+
+    std::map<Node, NodeTrie> svarTrie;
+    std::map<Node, std::map<unsigned, std::vector<unsigned> > > svarEqc;
+
+    for (unsigned j = 0, size = indices.size(); j < size; j++)
+    {
+      unsigned index = indices[j];
+      Partition& p = partitions[index];
+      for (const std::pair<const Node, std::vector<Node> > ps :
+           p.d_subvar_to_vars)
+      {
+        Node sv = ps.first;
+        unsigned res = svarTrie[sv].add(index, ps.second);
+        svarEqc[sv][res].push_back(index);
+      }
+    }
+    Trace("sym-dt-debug")
+        << "...multiple symmetry breaking variables, regroup and drop"
+        << std::endl;
+    unsigned minGroups = indices.size();
+    Node svarMin;
+    for (const std::pair<const Node,
+                         std::map<unsigned, std::vector<unsigned> > > sve :
+         svarEqc)
+    {
+      if (Trace.isOn("sym-dt-debug"))
+      {
+        Trace("sym-dt-debug") << "For " << sve.first << " : ";
+        for (const std::pair<const unsigned, std::vector<unsigned> > svee :
+             sve.second)
+        {
+          Trace("sym-dt-debug") << "{ ";
+          for (unsigned i : svee.second)
+          {
+            Trace("sym-dt-debug") << i << " ";
+          }
+          Trace("sym-dt-debug") << "}";
+        }
+      }
+      unsigned ngroups = sve.second.size();
+      Trace("sym-dt-debug") << ", #groups=" << ngroups << std::endl;
+      if (ngroups < minGroups)
+      {
+        minGroups = ngroups;
+        svarMin = sve.first;
+        if (minGroups == 1)
+        {
+          break;
+        }
+      }
+    }
+    if (minGroups == indices.size())
+    {
+      // can only handle symmetries that are classified by { n }
+      Trace("sym-dt-debug") << "...failed to merge (multiple symmetry breaking "
+                               "vars with no groups)"
+                            << std::endl;
+      return;
+    }
+    // recursive call for each group
+    for (const std::pair<unsigned, std::vector<unsigned> >& svee :
+         svarEqc[svarMin])
+    {
+      Assert(!svee.second.empty());
+      unsigned firstIndex = svee.second[0];
+      unsigned nfvars = 0;
+      Trace("sym-dt-debug") << "Recurse, fixing " << svarMin << " -> { ";
+      // add the list of fixed variables
+      for (const Node& v : partitions[firstIndex].d_subvar_to_vars[svarMin])
+      {
+        Trace("sym-dt-debug") << v << " ";
+        fixedSVar.push_back(svarMin);
+        fixedVar.push_back(v);
+        nfvars++;
+      }
+      Trace("sym-dt-debug") << "}" << std::endl;
+
+      // remove it from each of the partitions to process
+      for (unsigned pindex : svee.second)
+      {
+        partitions[pindex].removeVariable(svarMin);
+      }
+
+      // recursive call
+      processPartitions(
+          k, partitions, svee.second, active_indices, fixedSVar, fixedVar);
+
+      // remove the list of fixed variables
+      for (unsigned k = 0; k < nfvars; k++)
+      {
+        fixedVar.pop_back();
+        fixedSVar.pop_back();
+      }
+    }
     return;
   }
   // separate by number of variables
@@ -907,10 +1205,26 @@ void SymmetryDetect::processPartitions(
     }
     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);
   }
+  // now, re-add the fixed variables
+  if (!fixedVar.empty())
+  {
+    for (unsigned j = 0, size = indices.size(); j < size; j++)
+    {
+      unsigned index = indices[j];
+      // if still active
+      if (active_indices.find(index) != active_indices.end())
+      {
+        for (unsigned i = 0, size = fixedSVar.size(); i < size; i++)
+        {
+          // add variable
+          partitions[index].addVariable(fixedSVar[i], fixedVar[i]);
+        }
+      }
+    }
+  }
 }
 
 void SymmetryDetect::mergePartitions(
@@ -925,7 +1239,8 @@ void SymmetryDetect::mergePartitions(
   }
   if (Trace.isOn("sym-dt-debug"))
   {
-    Trace("sym-dt-debug") << "  merge indices ";
+    Trace("sym-dt-debug") << "--- mergePartitions..." << std::endl;
+    Trace("sym-dt-debug") << "  indices ";
     for (unsigned i : indices)
     {
       Trace("sym-dt-debug") << i << " ";
@@ -938,12 +1253,27 @@ void SymmetryDetect::mergePartitions(
   PartitionMerger pm;
   pm.initialize(k, partitions, indices);
 
-  // TODO (#2198): process indices for distinct types separately
   for (unsigned index : indices)
   {
-    if (pm.merge(partitions, index, active_indices))
+    Node mterm = partitions[index].d_term;
+    std::vector<unsigned> merged_indices;
+    if (pm.merge(partitions, index, active_indices, merged_indices))
     {
-      Trace("sym-dt-debug") << "    ......we merged, recurse" << std::endl;
+      // get the symmetric terms, these will be used when doing symmetry
+      // breaking
+      std::vector<Node> symTerms;
+      // include the term from the base index
+      symTerms.push_back(mterm);
+      for (unsigned mi : merged_indices)
+      {
+        Node st = partitions[mi].d_term;
+        symTerms.push_back(st);
+      }
+      Trace("sym-dt-debug") << "    ......merged " << symTerms << std::endl;
+      std::vector<Node> vars;
+      partitions[index].getVariables(vars);
+      storeTermSymmetry(symTerms, vars);
+      Trace("sym-dt-debug") << "    ......recurse" << std::endl;
       std::vector<unsigned> rem_indices;
       for (unsigned ii : indices)
       {
@@ -958,6 +1288,30 @@ void SymmetryDetect::mergePartitions(
   }
 }
 
+void SymmetryDetect::storeTermSymmetry(const std::vector<Node>& symTerms,
+                                       const std::vector<Node>& vars)
+{
+  Trace("sym-dt-tsym") << "*** Term symmetry : " << symTerms << std::endl;
+  Trace("sym-dt-tsym") << "*** Over variables : " << vars << std::endl;
+  // cannot have free variable
+  if (expr::hasFreeVar(symTerms[0]))
+  {
+    Trace("sym-dt-tsym") << "...free variable, do not allocate." << std::endl;
+    return;
+  }
+
+  unsigned tid = d_tsym_id_counter;
+  Trace("sym-dt-tsym") << "...allocate id " << tid << std::endl;
+  d_tsym_id_counter = d_tsym_id_counter + 1;
+  // allocate the term symmetry
+  d_tsyms[tid] = symTerms;
+  d_tsym_to_vars[tid] = vars;
+  for (const Node& v : vars)
+  {
+    d_var_to_tsym_ids[v].push_back(tid);
+  }
+}
+
 }  // namespace symbreak
 }  // namespace passes
 }  // namespace preprocessing
diff --git a/src/preprocessing/passes/symmetry_detect.h b/src/preprocessing/passes/symmetry_detect.h
index 9a5f83868..67e40da00 100644
--- a/src/preprocessing/passes/symmetry_detect.h
+++ b/src/preprocessing/passes/symmetry_detect.h
@@ -21,6 +21,7 @@
 #include <string>
 #include <vector>
 #include "expr/node.h"
+#include "theory/quantifiers/term_canonize.h"
 
 namespace CVC4 {
 namespace preprocessing {
@@ -65,10 +66,18 @@ class Partition
    * { w-> { x, y } }
    */
   std::map<Node, std::vector<Node> > d_subvar_to_vars;
-  /** sorts the ranges of d_subvar_to_vars. */
+  /** Add variable v to d_subvar_to_vars[sv]. */
+  void addVariable(Node sv, Node v);
+  /** Remove variable sv from the domain of d_subvar_to_vars. */
+  void removeVariable(Node sv);
+  /** Sorts the ranges of d_subvar_to_vars. */
   void normalize();
   /** Print a partition */
   static void printPartition(const char* c, Partition p);
+  /** get variables */
+  void getVariables(std::vector<Node>& vars);
+  /** get substitution */
+  void getSubstitution(std::vector<Node>& vars, std::vector<Node>& subs);
 };
 
 /** partition merger
@@ -128,7 +137,8 @@ class PartitionMerger
    */
   bool merge(std::vector<Partition>& partitions,
              unsigned base_index,
-             std::unordered_set<unsigned>& active_indices);
+             std::unordered_set<unsigned>& active_indices,
+             std::vector<unsigned>& merged_indices);
 
  private:
   /** the kind of the node we are consdiering */
@@ -176,49 +186,16 @@ class PartitionMerger
                    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.
- * */
+ * This is the class to detect symmetries between variables or terms relative
+ * to a set of input assertions.
+ */
 class SymmetryDetect
 {
  public:
-  /**
-   * Constructor
-   * */
-  SymmetryDetect()
-  {
-    d_trueNode = NodeManager::currentNM()->mkConst<bool>(true);
-    d_falseNode = NodeManager::currentNM()->mkConst<bool>(false);
-  }
+  /** constructor */
+  SymmetryDetect();
 
   /**
    * Destructor
@@ -226,11 +203,22 @@ class SymmetryDetect
   ~SymmetryDetect() {}
 
   /** Get the final partition after symmetry detection.
-   *  If a vector in parts contains two variables x and y,
+   *
+   *  If a vector in sterms contains two variables x and y,
    *  then assertions and assertions { x -> y, y -> x } are
    *  equisatisfiable.
    * */
-  void getPartition(std::vector<std::vector<Node> >& parts, const std::vector<Node>& assertions);
+  void compute(std::vector<std::vector<Node> >& part,
+               const std::vector<Node>& assertions);
+
+  /** Get the final partition after symmetry detection.
+   *
+   *  If a vector in sterms contains two terms t and s,
+   *  then assertions and assertions { t -> s, s -> t } are
+   *  equisatisfiable.
+   * */
+  void computeTerms(std::vector<std::vector<Node> >& sterms,
+                    const std::vector<Node>& assertions);
 
  private:
   /** (canonical) symmetry breaking variables for each type */
@@ -253,6 +241,9 @@ class SymmetryDetect
   Node d_trueNode;
   Node d_falseNode;
 
+  /** term canonizer (for quantified formulas) */
+  theory::quantifiers::TermCanonize d_tcanon;
+
   /** Cache for partitions */
   std::map<Node, Partition> d_term_partition;
 
@@ -275,6 +266,22 @@ class SymmetryDetect
    * */
   void collectChildren(Node node, std::vector<Node>& children);
 
+  /** Compute alpha equivalent terms
+   *
+   * This is used for determining pairs of terms in sterms that are
+   * alpha-equivalent. In detail, this constructs sterm_to_indices such that if
+   * sterm_to_indices[t] contains an index i, then there exists a k such that
+   * indices[k] = i and sterms[k] is alpha-equivalent to t, and sterm_to_indices
+   * contains indices[k] for each k=1,...,indicies.size()-1. For example,
+   * computeAlphaEqTerms( { 0, 3, 7 }, { Q(a), forall x. P(x), forall y. P(y) }
+   * may construct sterm_to_indices such that
+   *   sterm_to_indices[Q(a)] -> { 0 }
+   *   sterm_to_indices[forall x. P(x)] -> { 3, 7 }
+   */
+  void computeAlphaEqTerms(
+      const std::vector<unsigned>& indices,
+      const std::vector<Node>& sterms,
+      std::map<Node, std::vector<unsigned> >& sterm_to_indices);
   /** process partitions
    *
    * This method is called when we have detected symmetries for the children
@@ -295,7 +302,9 @@ class SymmetryDetect
   void processPartitions(Kind k,
                          std::vector<Partition>& partitions,
                          const std::vector<unsigned>& indices,
-                         std::unordered_set<unsigned>& active_indices);
+                         std::unordered_set<unsigned>& active_indices,
+                         std::vector<Node>& fixedSVar,
+                         std::vector<Node>& fixedVar);
   /** merge partitions
    *
    * This method merges groups of partitions occurring in indices using the
@@ -307,7 +316,21 @@ class SymmetryDetect
                        std::vector<Partition>& partitions,
                        const std::vector<unsigned>& indices,
                        std::unordered_set<unsigned>& active_indices);
+  //-------------------for symmetry breaking terms
+  /** symmetry breaking id counter */
+  unsigned d_tsym_id_counter;
+  /** list of term symmetries */
+  std::map<unsigned, std::vector<Node> > d_tsyms;
+  /** list of term symmetries */
+  std::map<unsigned, std::vector<Node> > d_tsym_to_vars;
+  /** variables to ids */
+  std::map<Node, std::vector<unsigned> > d_var_to_tsym_ids;
+  /** store term symmetry */
+  void storeTermSymmetry(const std::vector<Node>& symTerms,
+                         const std::vector<Node>& vars);
+  //-------------------end for symmetry breaking terms
 };
+
 }  // namespace symbreak
 }  // namespace passes
 }  // namespace preprocessing