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

1 files changed, 224 insertions, 73 deletions

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