GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/shared_terms_database.h Lines: 24 24 100.0 %
Date: 2021-03-23 Branches: 10 32 31.3 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file shared_terms_database.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Dejan Jovanovic, Andrew Reynolds, Mathias Preiner
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
 ** [[ Add lengthier description here ]]
13
 ** \todo document this file
14
 **/
15
16
#include "cvc4_private.h"
17
18
#pragma once
19
20
#include <unordered_map>
21
22
#include "context/cdhashset.h"
23
#include "expr/node.h"
24
#include "expr/proof_node_manager.h"
25
#include "theory/ee_setup_info.h"
26
#include "theory/theory_id.h"
27
#include "theory/trust_node.h"
28
#include "theory/uf/equality_engine.h"
29
#include "theory/uf/proof_equality_engine.h"
30
#include "util/statistics_registry.h"
31
32
namespace CVC4 {
33
34
class TheoryEngine;
35
36
class SharedTermsDatabase : public context::ContextNotifyObj {
37
 public:
38
  /** A container for a list of shared terms */
39
  typedef std::vector<TNode> shared_terms_list;
40
41
  /** The iterator to go through the shared terms list */
42
  typedef shared_terms_list::const_iterator shared_terms_iterator;
43
44
 private:
45
  /** Some statistics */
46
  IntStat d_statSharedTerms;
47
48
  // Needs to be a map from Nodes as after a backtrack they might not exist
49
  typedef std::unordered_map<Node, shared_terms_list, TNodeHashFunction> SharedTermsMap;
50
51
  /** A map from atoms to a list of shared terms */
52
  SharedTermsMap d_atomsToTerms;
53
54
  /** Each time we add a shared term, we add it's parent to this list */
55
  std::vector<TNode> d_addedSharedTerms;
56
57
  /** Context-dependent size of the d_addedSharedTerms list */
58
  context::CDO<unsigned> d_addedSharedTermsSize;
59
60
  /** A map from atoms and subterms to the theories that use it */
61
  typedef context::CDHashMap<std::pair<Node, TNode>,
62
                             theory::TheoryIdSet,
63
                             TNodePairHashFunction>
64
      SharedTermsTheoriesMap;
65
  SharedTermsTheoriesMap d_termsToTheories;
66
67
  /** Map from term to theories that have already been notified about the shared term */
68
  typedef context::CDHashMap<TNode, theory::TheoryIdSet, TNodeHashFunction>
69
      AlreadyNotifiedMap;
70
  AlreadyNotifiedMap d_alreadyNotifiedMap;
71
72
  /** The registered equalities for propagation */
73
  typedef context::CDHashSet<Node, NodeHashFunction> RegisteredEqualitiesSet;
74
  RegisteredEqualitiesSet d_registeredEqualities;
75
76
 private:
77
  /** This method removes all the un-necessary stuff from the maps */
78
  void backtrack();
79
80
  // EENotifyClass: template helper class for d_equalityEngine - handles call-backs
81
8994
  class EENotifyClass : public theory::eq::EqualityEngineNotify {
82
    SharedTermsDatabase& d_sharedTerms;
83
  public:
84
8997
    EENotifyClass(SharedTermsDatabase& shared): d_sharedTerms(shared) {}
85
4807925
    bool eqNotifyTriggerPredicate(TNode predicate, bool value) override
86
    {
87
4807925
      Assert(predicate.getKind() == kind::EQUAL);
88
4807925
      d_sharedTerms.propagateEquality(predicate, value);
89
4807925
      return true;
90
    }
91
92
3602925
    bool eqNotifyTriggerTermEquality(theory::TheoryId tag,
93
                                     TNode t1,
94
                                     TNode t2,
95
                                     bool value) override
96
    {
97
3602925
      return d_sharedTerms.propagateSharedEquality(tag, t1, t2, value);
98
    }
99
100
12390
    void eqNotifyConstantTermMerge(TNode t1, TNode t2) override
101
    {
102
12390
      d_sharedTerms.conflict(t1, t2, true);
103
12390
    }
104
105
409341
    void eqNotifyNewClass(TNode t) override {}
106
6461575
    void eqNotifyMerge(TNode t1, TNode t2) override {}
107
1420750
    void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) override {}
108
  };
109
110
  /** The notify class for d_equalityEngine */
111
  EENotifyClass d_EENotify;
112
113
  /**
114
   * Method called by equalityEngine when a becomes (dis-)equal to b and a and b are shared with
115
   * the theory. Returns false if there is a direct conflict (via rewrite for example).
116
   */
117
  bool propagateSharedEquality(theory::TheoryId theory, TNode a, TNode b, bool value);
118
119
  /**
120
   * Called from the equality engine when a trigger equality is deduced.
121
   */
122
  bool propagateEquality(TNode equality, bool polarity);
123
124
  /** Theory engine */
125
  TheoryEngine* d_theoryEngine;
126
127
  /** Are we in conflict */
128
  context::CDO<bool> d_inConflict;
129
130
  /** Conflicting terms, if any */
131
  Node d_conflictLHS, d_conflictRHS;
132
133
  /** Polarity of the conflict */
134
  bool d_conflictPolarity;
135
136
  /** Called by the equality engine notify to mark the conflict */
137
12390
  void conflict(TNode lhs, TNode rhs, bool polarity) {
138
12390
    if (!d_inConflict) {
139
      // Only remember it if we're not already in conflict
140
12390
      d_inConflict = true;
141
12390
      d_conflictLHS = lhs;
142
12390
      d_conflictRHS = rhs;
143
12390
      d_conflictPolarity = polarity;
144
    }
145
12390
  }
146
147
  /**
148
   * Should be called before any public non-const method in order to
149
   * enqueue the conflict to the theory engine.
150
   */
151
  void checkForConflict();
152
153
 public:
154
  /**
155
   * @param theoryEngine The parent theory engine
156
   * @param context The SAT context
157
   * @param userContext The user context
158
   * @param pnm The proof node manager to use, which is non-null if proofs
159
   * are enabled.
160
   */
161
  SharedTermsDatabase(TheoryEngine* theoryEngine,
162
                      context::Context* context,
163
                      context::UserContext* userContext,
164
                      ProofNodeManager* pnm);
165
  ~SharedTermsDatabase();
166
167
  //-------------------------------------------- initialization
168
  /** Called to set the equality engine. */
169
  void setEqualityEngine(theory::eq::EqualityEngine* ee);
170
  /**
171
   * Returns true if we need an equality engine, this has the same contract
172
   * as Theory::needsEqualityEngine.
173
   */
174
  bool needsEqualityEngine(theory::EeSetupInfo& esi);
175
  //-------------------------------------------- end initialization
176
177
  /**
178
   * Asserts the equality to the shared terms database,
179
   */
180
  void assertEquality(TNode equality, bool polarity, TNode reason);
181
182
  /**
183
   * Return whether the equality is alreday known to the engine
184
   */
185
  bool isKnown(TNode literal) const;
186
187
  /**
188
   * Returns an explanation of the propagation that came from the database.
189
   */
190
  theory::TrustNode explain(TNode literal) const;
191
192
  /**
193
   * Add an equality to propagate.
194
   */
195
  void addEqualityToPropagate(TNode equality);
196
197
  /**
198
   * Add a shared term to the database. The shared term is a subterm of the atom and
199
   * should be associated with the given theory.
200
   */
201
  void addSharedTerm(TNode atom, TNode term, theory::TheoryIdSet theories);
202
203
  /**
204
   * Mark that the given theories have been notified of the given shared term.
205
   */
206
  void markNotified(TNode term, theory::TheoryIdSet theories);
207
208
  /**
209
   * Returns true if the atom contains any shared terms, false otherwise.
210
   */
211
  bool hasSharedTerms(TNode atom) const;
212
213
  /**
214
   * Iterator pointing to the first shared term belonging to the given atom.
215
   */
216
  shared_terms_iterator begin(TNode atom) const;
217
218
  /**
219
   * Iterator pointing to the end of the list of shared terms belonging to the given atom.
220
   */
221
  shared_terms_iterator end(TNode atom) const;
222
223
  /**
224
   * Get the theories that share the term in a given atom (and have not yet been notified).
225
   */
226
  theory::TheoryIdSet getTheoriesToNotify(TNode atom, TNode term) const;
227
228
  /**
229
   * Get the theories that share the term and have been notified already.
230
   */
231
  theory::TheoryIdSet getNotifiedTheories(TNode term) const;
232
233
  /**
234
   * Returns true if the term is currently registered as shared with some theory.
235
   */
236
3105711
  bool isShared(TNode term) const {
237
3105711
    return d_alreadyNotifiedMap.find(term) != d_alreadyNotifiedMap.end();
238
  }
239
240
  /**
241
   * Returns true if the literal is an (dis-)equality with both sides registered as shared with
242
   * some theory.
243
   */
244
  bool isSharedEquality(TNode literal) const {
245
    TNode atom = literal.getKind() == kind::NOT ? literal[0] : literal;
246
    return atom.getKind() == kind::EQUAL && isShared(atom[0]) && isShared(atom[1]);
247
  }
248
249
  /**
250
   * Returns true if the shared terms a and b are known to be equal.
251
   */
252
  bool areEqual(TNode a, TNode b) const;
253
254
  /**
255
   * Retursn true if the shared terms a and b are known to be dis-equal.
256
   */
257
  bool areDisequal(TNode a, TNode b) const;
258
259
  /**
260
   * get equality engine
261
   */
262
  theory::eq::EqualityEngine* getEqualityEngine();
263
264
 protected:
265
  /**
266
   * This method gets called on backtracks from the context manager.
267
   */
268
2507010
  void contextNotifyPop() override { backtrack(); }
269
  /** The SAT search context. */
270
  context::Context* d_satContext;
271
  /** The user level assertion context. */
272
  context::UserContext* d_userContext;
273
  /** Equality engine */
274
  theory::eq::EqualityEngine* d_equalityEngine;
275
  /** Proof equality engine */
276
  std::unique_ptr<theory::eq::ProofEqEngine> d_pfee;
277
  /** The proof node manager */
278
  ProofNodeManager* d_pnm;
279
};
280
281
}