GCC Code Coverage Report
 Directory: . Exec Total Coverage File: src/theory/uf/symmetry_breaker.h Lines: 7 7 100.0 % Date: 2021-03-23 Branches: 4 18 22.2 %

 Line Exec Source 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-2021 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  **

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                     **
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  48 #include  49 #include  50 #include  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 #include "util/stats_timer.h" 59 60 namespace CVC4 { 61 namespace theory { 62 namespace uf { 63 64 8994 class SymmetryBreaker : public context::ContextNotifyObj { 65 66 15720  class Template { 67  Node d_template; 68  NodeBuilder<> d_assertions; 69  std::unordered_map, TNodeHashFunction> d_sets; 70  std::unordered_map d_reps; 71 72  TNode find(TNode n); 73  bool matchRecursive(TNode t, TNode n); 74 75  public: 76  Template(); 77  bool match(TNode n); 78 28516  std::unordered_map, TNodeHashFunction>& partitions() { return d_sets; } 79  Node assertions() { 80  switch(d_assertions.getNumChildren()) { 81  case 0: return Node::null(); 82  case 1: return d_assertions[0]; 83  default: return Node(d_assertions); 84  } 85  } 86  void reset(); 87  };/* class SymmetryBreaker::Template */ 88 89 public: 90 91  typedef std::set Permutation; 92  typedef std::set Permutations; 93  typedef TNode Term; 94  typedef std::list Terms; 95  typedef std::set TermEq; 96  typedef std::unordered_map TermEqs; 97 98 private: 99 100  /** 101  * This class wasn't initially built to be incremental. It should 102  * be attached to a UserContext so that it clears everything when 103  * a pop occurs. This "assertionsToRerun" is a set of assertions to 104  * feed back through assertFormula() when we started getting things 105  * again. It's not just a matter of effectiveness, but also soundness; 106  * if some assertions (still in scope) are not seen by a symmetry-breaking 107  * round, then some symmetries that don't actually exist might be broken, 108  * leading to unsound results! 109  */ 110  context::CDList d_assertionsToRerun; 111  bool d_rerunningAssertions; 112 113  std::vector d_phi; 114  std::set d_phiSet; 115  Permutations d_permutations; 116  Terms d_terms; 117  Template d_template; 118  std::unordered_map d_normalizationCache; 119  TermEqs d_termEqs; 120  TermEqs d_termEqsOnly; 121 122  void clear(); 123  void rerunAssertionsIfNecessary(); 124 125  void guessPermutations(); 126  bool invariantByPermutations(const Permutation& p); 127  void selectTerms(const Permutation& p); 128  Terms::iterator selectMostPromisingTerm(Terms& terms); 129  void insertUsedIn(Term term, const Permutation& p, std::set& cts); 130  Node normInternal(TNode phi, size_t level); 131  Node norm(TNode n); 132 133  std::string d_name; 134 135  // === STATISTICS === 136  /** number of new clauses that come from the SymmetryBreaker */ 137  struct Statistics { 138  /** number of new clauses that come from the SymmetryBreaker */ 139  IntStat d_clauses; 140  IntStat d_units; 141  /** number of potential permutation sets we found */ 142  IntStat d_permutationSetsConsidered; 143  /** number of invariant permutation sets we found */ 144  IntStat d_permutationSetsInvariant; 145  /** time spent in invariantByPermutations() */ 146  TimerStat d_invariantByPermutationsTimer; 147  /** time spent in selectTerms() */ 148  TimerStat d_selectTermsTimer; 149  /** time spent in initial round of normalization */ 150  TimerStat d_initNormalizationTimer; 151 152  Statistics(std::string name); 153  ~Statistics(); 154  }; 155 156  Statistics d_stats; 157 158  protected: 159 12210  void contextNotifyPop() override 160  { 161 12210  Debug("ufsymm") << "UFSYMM: clearing state due to pop" << std::endl; 162 12210  clear(); 163 12210  } 164 165  public: 166  SymmetryBreaker(context::Context* context, std::string name = ""); 167 168  void assertFormula(TNode phi); 169  void apply(std::vector& newClauses); 170 171 };/* class SymmetryBreaker */ 172 173 }/* CVC4::theory::uf namespace */ 174 }/* CVC4::theory namespace */ 175 176 std::ostream& operator<<(std::ostream& out, const ::CVC4::theory::uf::SymmetryBreaker::Permutation& p); 177 178 }/* CVC4 namespace */ 179 180 #endif /* CVC4__THEORY__UF__SYMMETRY_BREAKER_H */

 Generated by: GCOVR (Version 3.2)