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
 ** <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
#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<TNode, std::set<TNode>, TNodeHashFunction> d_sets;
70
    std::unordered_map<TNode, TNode, TNodeHashFunction> 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<TNode, std::set<TNode>, 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<TNode> Permutation;
92
  typedef std::set<Permutation> Permutations;
93
  typedef TNode Term;
94
  typedef std::list<Term> Terms;
95
  typedef std::set<Term> TermEq;
96
  typedef std::unordered_map<Term, TermEq, TNodeHashFunction> 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<Node> d_assertionsToRerun;
111
  bool d_rerunningAssertions;
112
113
  std::vector<Node> d_phi;
114
  std::set<TNode> d_phiSet;
115
  Permutations d_permutations;
116
  Terms d_terms;
117
  Template d_template;
118
  std::unordered_map<Node, Node, NodeHashFunction> 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<Node>& 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<Node>& 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 */