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-2019 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); partitions()77 std::unordered_map<TNode, std::set<TNode>, TNodeHashFunction>& partitions() { return d_sets; } assertions()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: contextNotifyPop()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 */ 180