Symmetry detection module (#1749)

13 files changed, 817 insertions, 5 deletions

diff --git a/src/Makefile.am b/src/Makefile.am
index f89a8426e..04d6e24b7 100644
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -68,6 +68,8 @@ libcvc4_la_SOURCES = \
 	preprocessing/passes/int_to_bv.h \
 	preprocessing/passes/pseudo_boolean_processor.cpp \
 	preprocessing/passes/pseudo_boolean_processor.h \
+	preprocessing/passes/symmetry_detect.cpp \
+	preprocessing/passes/symmetry_detect.h \
 	preprocessing/preprocessing_pass.cpp \
 	preprocessing/preprocessing_pass.h \
 	preprocessing/preprocessing_pass_context.cpp \
diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml
index a9093b894..e7a385a42 100644
--- a/src/options/smt_options.toml
+++ b/src/options/smt_options.toml
@@ -342,6 +342,14 @@ header = "options/smt_options.h"
   type       = "bool"
   default    = "false"
   help       = "calculate sort inference of input problem, convert the input based on monotonic sorts"
+   
+[[option]]
+  name       = "symmetryDetect"
+  category   = "regular"
+  long       = "symmetry-detect"
+  type       = "bool"
+  default    = "false"
+  help       = "compute symmetries in the input as a preprocessing pass"    
 
 [[option]]
   name       = "incrementalSolving"
diff --git a/src/preprocessing/passes/symmetry_detect.cpp b/src/preprocessing/passes/symmetry_detect.cpp
new file mode 100644
index 000000000..d39b8d14e
--- /dev/null
+++ b/src/preprocessing/passes/symmetry_detect.cpp
@@ -0,0 +1,459 @@
+/*********************                                                        */
+/*! \file symmetry_detect.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **  Paul Meng, Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Symmetry detection module
+ **/
+
+#include "preprocessing/passes/symmetry_detect.h"
+#include "theory/quantifiers/term_util.h"
+#include "theory/rewriter.h"
+
+using namespace std;
+
+namespace CVC4 {
+namespace preprocessing {
+namespace passes {
+
+SymmetryDetect::Partition SymmetryDetect::detect(const vector<Node>& assertions)
+{
+  Partition p =
+      findPartitions(NodeManager::currentNM()->mkNode(kind::AND, assertions));
+  Trace("sym-dt") << endl
+                  << "------------------------------ The Final Partition "
+                     "------------------------------"
+                  << endl;
+  if(Trace.isOn("sym-dt"))
+  {
+    printPartition(p);
+  }
+  return p;
+}
+
+void SymmetryDetect::getPartition(vector<vector<Node> >& parts,
+                                  const vector<Node>& assertions)
+{
+  Partition p = detect(assertions);
+
+  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();
+       ++subvar_to_vars_it)
+  {
+    parts.push_back(subvar_to_vars_it->second);
+  }
+}
+
+SymmetryDetect::Partition SymmetryDetect::findPartitions(Node node)
+{
+  Trace("sym-dt")
+      << "------------------------------------------------------------"
+      << endl;
+  Trace("sym-dt") << "[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;
+    return partition->second;
+  }
+
+  // The new partition for node
+  Partition p;
+  // If node is a variable
+  if (node.isVar() && node.getKind() != kind::BOUND_VARIABLE)
+  {
+    vector<Node> vars;
+    TypeNode type = node.getType();
+    Node fresh_var = NodeManager::currentNM()->mkSkolem("sym_bk", type);
+
+    vars.push_back(node);
+    p.d_term = node;
+    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())
+  {
+    p.d_term = node;
+    d_term_partition[node] = p;
+    return p;
+  }
+
+  // Children of node
+  vector<Node> children;
+  // Partitions of children
+  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;
+
+  // Create partitions for children
+  for (vector<Node>::iterator children_it = children.begin();
+       children_it != children.end();
+       ++children_it)
+  {
+    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
+  {
+    // 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);
+  }
+
+  // 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())
+  {
+    // 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)
+    {
+      // Skip expr_it1->first, if it has been merged
+      if (merged.find(expr_it1->first) != merged.end())
+      {
+        continue;
+      }
+
+      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)
+      {
+        if (merged.find(expr_it2->first) != merged.end())
+        {
+          continue;
+        }
+        if ((expr_it1->second).getType() != (expr_it2->second).getType())
+        {
+          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;
+        }
+      }
+      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);
+    }
+  }
+}
+
+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)
+  {
+    if ((*part_it).d_var_to_subvar.size() == 1)
+    {
+      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;
+    }
+    else if ((*part_it).d_var_to_subvar.size() >= 2)
+    {
+      for (const pair<Node, Node>& var_to_subvar : (*part_it).d_var_to_subvar)
+      {
+        vars.insert(var_to_subvar.first);
+      }
+      // Only add partitions that have more than 1 variable
+      new_partitions.push_back(*part_it);
+    }
+  }
+
+  // Save all partitions that have more than 1 variable
+  partitions = new_partitions;
+
+  // Do matches on singleton terms
+  if (!subvar_to_var.empty())
+  {
+    matches(partitions, subvar_to_var, subvar_to_expr);
+  }
+}
+
+void SymmetryDetect::collectChildren(Node node, vector<Node>& children)
+{
+  Kind k = node.getKind();
+
+  if(!theory::quantifiers::TermUtil::isAssoc(k))
+  {
+    children.insert(children.end(), node.begin(), node.end());
+    return;
+  }
+
+  Node cur;
+  vector<Node> visit;
+  visit.push_back(node);
+  unordered_set<Node, NodeHashFunction> visited;
+
+  do
+  {
+    cur = visit.back();
+    visit.pop_back();
+    if (visited.find(cur) == visited.end())
+    {
+      visited.insert(cur);
+      if (cur.getKind() == k)
+      {
+        for (const Node& cn : cur)
+        {
+          visit.push_back(cn);
+        }
+      }
+      else
+      {
+        children.push_back(cur);
+      }
+    }
+  } while (!visit.empty());
+}
+
+void SymmetryDetect::PartitionTrie::getNewPartition(Partition& part,
+                                                    PartitionTrie& pt)
+{
+  if (!pt.d_variables.empty())
+  {
+    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)
+    {
+      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);
+    }
+  }
+}
+
+void SymmetryDetect::getVariables(vector<Partition>& partitions,
+                                  unordered_set<Node, NodeHashFunction>& vars)
+{
+  for (vector<Partition>::iterator part_it = partitions.begin();
+       part_it != partitions.end();
+       ++part_it)
+  {
+    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());
+    }
+  }
+}
+
+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)
+  {
+    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())
+    {
+      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)
+      {
+        if (var_sub_it->second == sub_vars_it->first)
+        {
+          subvars.push_back(var_sub_it->second);
+        }
+        else
+        {
+          subvars.push_back(Node::null());
+        }
+      }
+    }
+    else
+    {
+      subvars.resize(subvars.size()+(*part_it).d_subvar_to_vars.size());
+    }
+  }
+
+  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)
+{
+  if (subvars.empty())
+  {
+    d_variables.push_back(target_var);
+  }
+  else
+  {
+    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())
+    {
+      (children_it->second).addNode(target_var, new_subs);
+    }
+    else
+    {
+      PartitionTrie pt;
+
+      pt.addNode(target_var, new_subs);
+      d_children[subvars[0]] = pt;
+    }
+  }
+}
+
+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 << " -> {";
+
+    for (vector<Node>::iterator part_it = (sub_vars_it->second).begin();
+         part_it != (sub_vars_it->second).end();
+         ++part_it)
+    {
+      Trace("sym-dt") << " " << *part_it;
+    }
+    Trace("sym-dt") << " }" << endl;
+  }
+}
+}  // namespace passes
+}  // namespace preprocessing
+}  // namespace CVC4
diff --git a/src/preprocessing/passes/symmetry_detect.h b/src/preprocessing/passes/symmetry_detect.h
new file mode 100644
index 000000000..3741eff3e
--- /dev/null
+++ b/src/preprocessing/passes/symmetry_detect.h
@@ -0,0 +1,165 @@
+/*********************                                                        */
+/*! \file symmetry_detect.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **  Paul Meng, Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Symmetry detection for theories
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__PREPROCESSING__PASSES__SYMMETRY_DETECT_H
+#define __CVC4__PREPROCESSING__PASSES__SYMMETRY_DETECT_H
+
+#include <map>
+#include <string>
+#include <vector>
+#include "expr/node.h"
+
+namespace CVC4 {
+namespace preprocessing {
+namespace passes {
+
+/**
+ * This is the class to detect symmetries from input based on terms equality.
+ * */
+class SymmetryDetect
+{
+ public:
+  /**
+   * Constructor
+   * */
+  SymmetryDetect()
+  {
+    d_trueNode = NodeManager::currentNM()->mkConst<bool>(true);
+    d_falseNode = NodeManager::currentNM()->mkConst<bool>(false);
+  }
+
+  /**
+   * Destructor
+   * */
+  ~SymmetryDetect() {}
+
+  /** Get the final partition after symmetry detection.
+   *  If a vector in parts 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);
+
+ private:
+  /**
+   * 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.
+   */
+  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;
+  };
+
+  /**
+   * 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]. */
+    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);
+  };
+
+
+  /** True and false constant nodes */
+  Node d_trueNode;
+  Node d_falseNode;
+
+  /** Cache for partitions */
+  std::map<Node, Partition> d_term_partition;
+
+  /** detect
+   *
+   * Called on the input assertions, where assertions are interpreted as a
+   * conjunction. This computes a partition P of the variables in assertions
+   * such that for each set S in P, then all automorphisms for S applied to
+   * assertions result in an equisatisfiable formula.
+   */
+  Partition detect(const std::vector<Node>& assertions);
+
+  /** Find symmetries in node */
+  SymmetryDetect::Partition findPartitions(Node node);
+
+  /** Collect children of a node
+   *  If the kind of node is associative, we will chain its children together.
+   *  We might need optimizations here, such as rewriting the input to negation
+   *  normal form.
+   * */
+  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);
+};
+}  // namespace passes
+}  // namespace preprocessing
+}  // namespace CVC4
+
+#endif
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 65d3697b7..a65d55859 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -71,6 +71,7 @@
 #include "preprocessing/passes/bv_gauss.h"
 #include "preprocessing/passes/int_to_bv.h"
 #include "preprocessing/passes/pseudo_boolean_processor.h"
+#include "preprocessing/passes/symmetry_detect.h"
 #include "preprocessing/preprocessing_pass.h"
 #include "preprocessing/preprocessing_pass_context.h"
 #include "preprocessing/preprocessing_pass_registry.h"
@@ -4283,6 +4284,13 @@ void SmtEnginePrivate::processAssertions() {
   Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-simplify" << endl;
   dumpAssertions("post-simplify", d_assertions);
 
+  if (options::symmetryDetect())
+  {
+    SymmetryDetect symd;
+    vector<vector<Node>> part;
+    symd.getPartition(part, d_assertions.ref());
+  }
+
   dumpAssertions("pre-static-learning", d_assertions);
   if(options::doStaticLearning()) {
     Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-static-learning" << endl;
diff --git a/src/theory/quantifiers/term_util.cpp b/src/theory/quantifiers/term_util.cpp
index b3915bd5d..76d95bf5e 100644
--- a/src/theory/quantifiers/term_util.cpp
+++ b/src/theory/quantifiers/term_util.cpp
@@ -811,14 +811,18 @@ Node TermUtil::mkNegate(Kind notk, Node n)
 }
 
 bool TermUtil::isAssoc( Kind k ) {
-  return k==PLUS || k==MULT || k==AND || k==OR || 
-         k==BITVECTOR_PLUS || k==BITVECTOR_MULT || k==BITVECTOR_AND || k==BITVECTOR_OR || k==BITVECTOR_XOR || k==BITVECTOR_XNOR || k==BITVECTOR_CONCAT ||
-         k==STRING_CONCAT;
+  return k == PLUS || k == MULT || k == AND || k == OR || k == BITVECTOR_PLUS
+         || k == BITVECTOR_MULT || k == BITVECTOR_AND || k == BITVECTOR_OR
+         || k == BITVECTOR_XOR || k == BITVECTOR_XNOR || k == BITVECTOR_CONCAT
+         || k == STRING_CONCAT || k == UNION || k == INTERSECTION || k == JOIN
+         || k == PRODUCT;
 }
 
 bool TermUtil::isComm( Kind k ) {
-  return k==EQUAL || k==PLUS || k==MULT || k==AND || k==OR || k==XOR || 
-         k==BITVECTOR_PLUS || k==BITVECTOR_MULT || k==BITVECTOR_AND || k==BITVECTOR_OR || k==BITVECTOR_XOR || k==BITVECTOR_XNOR;
+  return k == EQUAL || k == PLUS || k == MULT || k == AND || k == OR || k == XOR
+         || k == BITVECTOR_PLUS || k == BITVECTOR_MULT || k == BITVECTOR_AND
+         || k == BITVECTOR_OR || k == BITVECTOR_XOR || k == BITVECTOR_XNOR
+         || k == UNION || k == INTERSECTION;
 }
 
 bool TermUtil::isNonAdditive( Kind k ) {
diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests
index 56965f272..a29236914 100644
--- a/test/regress/Makefile.tests
+++ b/test/regress/Makefile.tests
@@ -1490,6 +1490,12 @@ REG1_TESTS = \
 	regress1/sygus/twolets2-orig.sy \
 	regress1/sygus/unbdd_inv_gen_ex7.sy \
 	regress1/sygus/unbdd_inv_gen_winf1.sy \
+	regress1/sym/sym1.smt2 \
+	regress1/sym/sym2.smt2 \
+	regress1/sym/sym3.smt2 \
+	regress1/sym/sym4.smt2 \
+	regress1/sym/sym5.smt2 \
+	regress1/sym/sym6.smt2 \
 	regress1/test12.cvc \
 	regress1/trim.cvc \
 	regress1/uf2.smt2 \
diff --git a/test/regress/regress1/sym/sym1.smt2 b/test/regress/regress1/sym/sym1.smt2
new file mode 100644
index 000000000..ac1c0215f
--- /dev/null
+++ b/test/regress/regress1/sym/sym1.smt2
@@ -0,0 +1,21 @@
+; COMMAND-LINE: --symmetry-detect
+(set-logic ALL)
+(set-info :status sat)
+(declare-fun x () Int)
+(declare-fun y () Int)
+(declare-fun z () Int)
+
+
+(declare-fun p (Int) Bool)
+(declare-fun A () (Set Int))
+(declare-fun F () (Set Int))
+
+
+
+(assert (= F (insert x y (singleton z))))
+(assert (subset F A))
+(assert (= x y))
+
+
+(check-sat)
+
diff --git a/test/regress/regress1/sym/sym2.smt2 b/test/regress/regress1/sym/sym2.smt2
new file mode 100644
index 000000000..cff424ba9
--- /dev/null
+++ b/test/regress/regress1/sym/sym2.smt2
@@ -0,0 +1,27 @@
+; COMMAND-LINE: --symmetry-detect
+(set-logic ALL)
+(set-info :status sat)
+(declare-fun x () Int)
+(declare-fun y () Int)
+(declare-fun z () Int)
+(declare-fun w () Int)
+(declare-fun u () Int)
+(declare-fun v () Int)
+
+
+(assert (> (- (+ (* 3 x) (* 3 y) (* 3 z)) u v) 0))
+(assert (> (+ u v) 0))
+(assert (> (+ x y) 0))
+(assert (> x 0))
+(assert (> z 0))
+(assert (> u 0))
+(assert (> v 0))
+(assert (< u 10))
+(assert (< v 10))
+
+
+
+
+
+(check-sat)
+
diff --git a/test/regress/regress1/sym/sym3.smt2 b/test/regress/regress1/sym/sym3.smt2
new file mode 100644
index 000000000..52f9855c9
--- /dev/null
+++ b/test/regress/regress1/sym/sym3.smt2
@@ -0,0 +1,21 @@
+; COMMAND-LINE: --symmetry-detect
+(set-logic ALL)
+(set-info :status sat)
+(declare-fun x () Int)
+(declare-fun y () Int)
+(declare-fun z () Int)
+(declare-fun w () Int)
+(declare-fun u () Int)
+(declare-fun v () Int)
+
+(declare-fun p (Int Int) Int)
+(declare-fun A () (Set Int))
+
+
+(assert (or (> (+ x y z) 3) (< (p x (+ (* 3 y) (* 3 z))) 5)))
+(assert (subset A (insert y (singleton z))))
+
+
+
+(check-sat)
+
diff --git a/test/regress/regress1/sym/sym4.smt2 b/test/regress/regress1/sym/sym4.smt2
new file mode 100644
index 000000000..5582ef7d0
--- /dev/null
+++ b/test/regress/regress1/sym/sym4.smt2
@@ -0,0 +1,48 @@
+; COMMAND-LINE: --symmetry-detect
+(set-info :smt-lib-version 2.6)
+(set-logic QF_LIA)
+(set-info :category "crafted")
+(set-info :status sat)
+(declare-fun x_0 () Int)
+(declare-fun x_1 () Int)
+(declare-fun x_2 () Int)
+(declare-fun x_3 () Int)
+(declare-fun x_4 () Int)
+(declare-fun x_5 () Int)
+(declare-fun x_6 () Int)
+(declare-fun x_7 () Int)
+(declare-fun x_8 () Int)
+(declare-fun x_9 () Int)
+(declare-fun x_10 () Int)
+(declare-fun x_11 () Int)
+(declare-fun x_12 () Int)
+(declare-fun x_13 () Int)
+(declare-fun x_14 () Int)
+(declare-fun x_15 () Int)
+(declare-fun x_16 () Int)
+(assert (>= x_0 0))
+(assert (>= x_1 0))
+(assert (>= x_2 0))
+(assert (>= x_3 0))
+(assert (>= x_4 0))
+(assert (>= x_5 0))
+(assert (>= x_6 0))
+(assert (>= x_7 0))
+(assert (>= x_8 0))
+(assert (>= x_9 0))
+(assert (>= x_10 0))
+(assert (>= x_11 0))
+(assert (>= x_12 0))
+(assert (>= x_13 0))
+(assert (>= x_14 0))
+(assert (>= x_15 0))
+(assert (>= x_16 0))
+(assert (<= (+ (* 37 x_0) (* 37 x_1) (* 37 x_2) (* 37 x_3) (* 37 x_4) (* 37 x_5) (* 37 x_6) (* 37 x_7) (* 37 x_8) (* 37 x_9) (* 37 x_10) (* (- 404) x_11) (* 37 x_12) (* 37 x_13) (* 37 x_14) (* 37 x_15) (* 37 x_16)) 0))
+(assert (<= (+ (* 41 x_0) (* 41 x_1) (* 41 x_2) (* 41 x_3) (* 41 x_4) (* 41 x_5) (* 41 x_6) (* 41 x_7) (* 41 x_8) (* 41 x_9) (* 41 x_10) (* 41 x_11) (* (- 400) x_12) (* 41 x_13) (* 41 x_14) (* 41 x_15) (* 41 x_16)) 0))
+(assert (<= (+ (* 43 x_0) (* 43 x_1) (* 43 x_2) (* 43 x_3) (* 43 x_4) (* 43 x_5) (* 43 x_6) (* 43 x_7) (* 43 x_8) (* 43 x_9) (* 43 x_10) (* 43 x_11) (* 43 x_12) (* (- 398) x_13) (* 43 x_14) (* 43 x_15) (* 43 x_16)) 0))
+(assert (<= (+ (* 47 x_0) (* 47 x_1) (* 47 x_2) (* 47 x_3) (* 47 x_4) (* 47 x_5) (* 47 x_6) (* 47 x_7) (* 47 x_8) (* 47 x_9) (* 47 x_10) (* 47 x_11) (* 47 x_12) (* 47 x_13) (* (- 394) x_14) (* 47 x_15) (* 47 x_16)) 0))
+(assert (<= (+ (* 53 x_0) (* 53 x_1) (* 53 x_2) (* 53 x_3) (* 53 x_4) (* 53 x_5) (* 53 x_6) (* 53 x_7) (* 53 x_8) (* 53 x_9) (* 53 x_10) (* 53 x_11) (* 53 x_12) (* 53 x_13) (* 53 x_14) (* (- 388) x_15) (* 53 x_16)) 0))
+(assert (<= (+ (* 59 x_0) (* 59 x_1) (* 59 x_2) (* 59 x_3) (* 59 x_4) (* 59 x_5) (* 59 x_6) (* 59 x_7) (* 59 x_8) (* 59 x_9) (* 59 x_10) (* 59 x_11) (* 59 x_12) (* 59 x_13) (* 59 x_14) (* 59 x_15) (* (- 382) x_16)) 0))
+(assert (>= (+ x_0 x_1 x_2 x_3 x_4 x_5 x_6 x_7 x_8 x_9 x_10 x_11 x_12 x_13 x_14 x_15 x_16) 1))
+(check-sat)
+(exit)
\ No newline at end of file
diff --git a/test/regress/regress1/sym/sym5.smt2 b/test/regress/regress1/sym/sym5.smt2
new file mode 100644
index 000000000..f5ef1d003
--- /dev/null
+++ b/test/regress/regress1/sym/sym5.smt2
@@ -0,0 +1,19 @@
+; COMMAND-LINE: --symmetry-detect
+(set-logic ALL)
+(set-info :status unsat)
+(declare-fun A () (Set Int))
+(declare-fun B () (Set Int))
+(declare-fun C () (Set Int))
+
+(declare-fun f () Int)
+(declare-fun g () Int)
+(declare-fun h () Int)
+(declare-fun i () Int)
+(declare-fun j () Int)
+
+(assert (subset A (insert g h i (singleton f))))
+(assert (= C (setminus A B) ))
+(assert (subset B A))
+(assert (= C (intersection A B)))
+(assert (member j C))
+(check-sat)
\ No newline at end of file
diff --git a/test/regress/regress1/sym/sym6.smt2 b/test/regress/regress1/sym/sym6.smt2
new file mode 100644
index 000000000..3da6b4cb4
--- /dev/null
+++ b/test/regress/regress1/sym/sym6.smt2
@@ -0,0 +1,24 @@
+; COMMAND-LINE: --symmetry-detect
+(set-logic ALL)
+(set-info :status sat)
+(declare-fun x () Int)
+(declare-fun y () Int)
+(declare-fun z () Int)
+(declare-fun w () Int)
+(declare-fun u () Int)
+(declare-fun v () Int)
+
+
+(assert (= (+ w y u) (+ v z)))
+
+(assert (> (+ x (* 2 y)) (+ u v)))
+
+(assert (= (- x) (- (- y))))
+
+
+
+(assert (or (< (+ x y z) 10) (> (+ v u) 10)))
+
+
+(check-sat)
+