src/theory/uf/symmetry_breaker.h

   1 /*********************                                                        */
   2 /*! \file symmetry_breaker.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Morgan Deters, Liana Hadarean, Tim King
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
   8  ** in the top-level source directory) and their institutional affiliations.
   9  ** All rights reserved.  See the file COPYING in the top-level source
  10  ** directory for licensing information.\endverbatim
  11  **
  12  ** \brief Implementation of algorithm suggested by Deharbe, Fontaine,
  13  ** Merz, and Paleo, "Exploiting symmetry in SMT problems," CADE 2011
  14  **
  15  ** Implementation of algorithm suggested by Deharbe, Fontaine, Merz,
  16  ** and Paleo, "Exploiting symmetry in SMT problems," CADE 2011.
  17  **
  18  ** From the paper:
  19  **
  20  ** <pre>
  21  **   \f$ P := guess\_permutations(\phi) \f$
  22  **   foreach \f$ {c_0, ..., c_n} \in P \f$ do
  23  **     if \f$ invariant\_by\_permutations(\phi, {c_0, ..., c_n}) \f$ then
  24  **       T := \f$ select\_terms(\phi, {c_0, ..., c_n}) \f$
  25  **       cts := \f$ \emptyset \f$
  26  **       while T != \f$ \empty \wedge |cts| <= n \f$ do
  27  **         \f$ t := select\_most\_promising\_term(T, \phi) \f$
  28  **         \f$ T := T \setminus {t} \f$
  29  **         cts := cts \f$ \cup used\_in(t, {c_0, ..., c_n}) \f$
  30  **         let \f$ c \in {c_0, ..., c_n} \setminus cts \f$
  31  **         cts := cts \f$ \cup {c} \f$
  32  **         if cts != \f$ {c_0, ..., c_n} \f$ then
  33  **           \f$ \phi := \phi \wedge ( \vee_{c_i \in cts} t = c_i ) \f$
  34  **         end
  35  **       end
  36  **     end
  37  **   end
  38  **   return \f$ \phi \f$
  39  ** </pre>
  40  **/
  41
  42 #include "cvc4_private.h"
  43
  44 #ifndef CVC4__THEORY__UF__SYMMETRY_BREAKER_H
  45 #define CVC4__THEORY__UF__SYMMETRY_BREAKER_H
  46
  47 #include <iostream>
  48 #include <list>
  49 #include <unordered_map>
  50 #include <vector>
  51
  52 #include "context/cdlist.h"
  53 #include "context/context.h"
  54 #include "expr/node.h"
  55 #include "expr/node_builder.h"
  56 #include "smt/smt_statistics_registry.h"
  57 #include "util/statistics_registry.h"
  58
  59 namespace CVC4 {
  60 namespace theory {
  61 namespace uf {
  62
  63 class SymmetryBreaker : public context::ContextNotifyObj {
  64
  65   class Template {
  66     Node d_template;
  67     NodeBuilder<> d_assertions;
  68     std::unordered_map<TNode, std::set<TNode>, TNodeHashFunction> d_sets;
  69     std::unordered_map<TNode, TNode, TNodeHashFunction> d_reps;
  70
  71     TNode find(TNode n);
  72     bool matchRecursive(TNode t, TNode n);
  73
  74   public:
  75     Template();
  76     bool match(TNode n);
  77     std::unordered_map<TNode, std::set<TNode>, TNodeHashFunction>& partitions() { return d_sets; }
  78     Node assertions() {
  79       switch(d_assertions.getNumChildren()) {
  80       case 0: return Node::null();
  81       case 1: return d_assertions[0];
  82       default: return Node(d_assertions);
  83       }
  84     }
  85     void reset();
  86   };/* class SymmetryBreaker::Template */
  87
  88 public:
  89
  90   typedef std::set<TNode> Permutation;
  91   typedef std::set<Permutation> Permutations;
  92   typedef TNode Term;
  93   typedef std::list<Term> Terms;
  94   typedef std::set<Term> TermEq;
  95   typedef std::unordered_map<Term, TermEq, TNodeHashFunction> TermEqs;
  96
  97 private:
  98
  99   /**
 100    * This class wasn't initially built to be incremental.  It should
 101    * be attached to a UserContext so that it clears everything when
 102    * a pop occurs.  This "assertionsToRerun" is a set of assertions to
 103    * feed back through assertFormula() when we started getting things
 104    * again.  It's not just a matter of effectiveness, but also soundness;
 105    * if some assertions (still in scope) are not seen by a symmetry-breaking
 106    * round, then some symmetries that don't actually exist might be broken,
 107    * leading to unsound results!
 108    */
 109   context::CDList<Node> d_assertionsToRerun;
 110   bool d_rerunningAssertions;
 111
 112   std::vector<Node> d_phi;
 113   std::set<TNode> d_phiSet;
 114   Permutations d_permutations;
 115   Terms d_terms;
 116   Template d_template;
 117   std::unordered_map<Node, Node, NodeHashFunction> d_normalizationCache;
 118   TermEqs d_termEqs;
 119   TermEqs d_termEqsOnly;
 120
 121   void clear();
 122   void rerunAssertionsIfNecessary();
 123
 124   void guessPermutations();
 125   bool invariantByPermutations(const Permutation& p);
 126   void selectTerms(const Permutation& p);
 127   Terms::iterator selectMostPromisingTerm(Terms& terms);
 128   void insertUsedIn(Term term, const Permutation& p, std::set<Node>& cts);
 129   Node normInternal(TNode phi, size_t level);
 130   Node norm(TNode n);
 131
 132   std::string d_name;
 133
 134   // === STATISTICS ===
 135   /** number of new clauses that come from the SymmetryBreaker */
 136   struct Statistics {
 137     /** number of new clauses that come from the SymmetryBreaker */
 138     IntStat d_clauses;
 139     IntStat d_units;
 140     /** number of potential permutation sets we found */
 141     IntStat d_permutationSetsConsidered;
 142     /** number of invariant permutation sets we found */
 143     IntStat d_permutationSetsInvariant;
 144     /** time spent in invariantByPermutations() */
 145     TimerStat d_invariantByPermutationsTimer;
 146     /** time spent in selectTerms() */
 147     TimerStat d_selectTermsTimer;
 148     /** time spent in initial round of normalization */
 149     TimerStat d_initNormalizationTimer;
 150
 151     Statistics(std::string name);
 152     ~Statistics();
 153   };
 154
 155   Statistics d_stats;
 156
 157  protected:
 158   void contextNotifyPop() override
 159   {
 160     Debug("ufsymm") << "UFSYMM: clearing state due to pop" << std::endl;
 161     clear();
 162   }
 163
 164  public:
 165   SymmetryBreaker(context::Context* context, std::string name = "");
 166
 167   void assertFormula(TNode phi);
 168   void apply(std::vector<Node>& newClauses);
 169
 170 };/* class SymmetryBreaker */
 171
 172 }/* CVC4::theory::uf namespace */
 173 }/* CVC4::theory namespace */
 174
 175 std::ostream& operator<<(std::ostream& out, const ::CVC4::theory::uf::SymmetryBreaker::Permutation& p);
 176
 177 }/* CVC4 namespace */
 178
 179 #endif /* CVC4__THEORY__UF__SYMMETRY_BREAKER_H */