GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/arith/congruence_manager.h Lines: 3 3 100.0 %
Date: 2021-03-23 Branches: 0 0 0.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file congruence_manager.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Alex Ozdemir, Tim King, Andrew Reynolds
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 [[ Add one-line brief description here ]]
13
 **
14
 ** [[ Add lengthier description here ]]
15
 ** \todo document this file
16
 **/
17
18
#include "cvc4_private.h"
19
20
#pragma once
21
22
#include "context/cdhashmap.h"
23
#include "context/cdlist.h"
24
#include "context/cdmaybe.h"
25
#include "context/cdtrail_queue.h"
26
#include "theory/arith/arithvar.h"
27
#include "theory/arith/arith_utilities.h"
28
#include "theory/arith/callbacks.h"
29
#include "theory/arith/constraint_forward.h"
30
#include "theory/trust_node.h"
31
#include "theory/uf/equality_engine_notify.h"
32
#include "util/dense_map.h"
33
#include "util/statistics_registry.h"
34
35
namespace CVC4 {
36
37
class ProofNodeManager;
38
39
namespace context {
40
class Context;
41
class UserContext;
42
}
43
44
namespace theory {
45
46
class EagerProofGenerator;
47
struct EeSetupInfo;
48
49
namespace eq {
50
class ProofEqEngine;
51
class EqualityEngine;
52
}
53
54
namespace arith {
55
56
class ArithVariables;
57
58
class ArithCongruenceManager {
59
private:
60
  context::CDRaised d_inConflict;
61
  RaiseEqualityEngineConflict d_raiseConflict;
62
63
  /**
64
   * The set of ArithVars equivalent to a pair of terms.
65
   * If this is 0 or cannot be 0, this can be signalled.
66
   * The pair of terms for the congruence is stored in watched equalities.
67
   */
68
  DenseSet d_watchedVariables;
69
  /** d_watchedVariables |-> (= x y) */
70
  ArithVarToNodeMap d_watchedEqualities;
71
72
73
8994
  class ArithCongruenceNotify : public eq::EqualityEngineNotify {
74
  private:
75
    ArithCongruenceManager& d_acm;
76
  public:
77
    ArithCongruenceNotify(ArithCongruenceManager& acm);
78
79
    bool eqNotifyTriggerPredicate(TNode predicate, bool value) override;
80
81
    bool eqNotifyTriggerTermEquality(TheoryId tag,
82
                                     TNode t1,
83
                                     TNode t2,
84
                                     bool value) override;
85
86
    void eqNotifyConstantTermMerge(TNode t1, TNode t2) override;
87
    void eqNotifyNewClass(TNode t) override;
88
    void eqNotifyMerge(TNode t1, TNode t2) override;
89
    void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) override;
90
  };
91
  ArithCongruenceNotify d_notify;
92
93
  context::CDList<Node> d_keepAlive;
94
95
  /** Store the propagations. */
96
  context::CDTrailQueue<Node> d_propagatations;
97
98
  /* This maps the node a theory engine will request on an explain call to
99
   * to its corresponding PropUnit.
100
   * This is node is potentially both the propagation or
101
   * Rewriter::rewrite(propagation).
102
   */
103
  typedef context::CDHashMap<Node, size_t, NodeHashFunction> ExplainMap;
104
  ExplainMap d_explanationMap;
105
106
  ConstraintDatabase& d_constraintDatabase;
107
  SetupLiteralCallBack d_setupLiteral;
108
109
  const ArithVariables& d_avariables;
110
111
  /** The equality engine being used by this class */
112
  eq::EqualityEngine* d_ee;
113
  /** The sat context */
114
  context::Context* d_satContext;
115
  /** The user context */
116
  context::UserContext* d_userContext;
117
118
  /** proof manager */
119
  ProofNodeManager* d_pnm;
120
  /** A proof generator for storing proofs of facts that are asserted to the EQ
121
   * engine. Note that these proofs **are not closed**; they may contain
122
   * literals from the explanation of their fact as unclosed assumptions.
123
   * This makes these proofs SAT-context depdent.
124
   *
125
   * This is why this generator is separate from the TheoryArithPrivate
126
   * generator, which stores closed proofs.
127
   */
128
  std::unique_ptr<EagerProofGenerator> d_pfGenEe;
129
  /** A proof generator for TrustNodes sent to TheoryArithPrivate.
130
   *
131
   * When TheoryArithPrivate requests an explanation from
132
   * ArithCongruenceManager, it can request a TrustNode for that explanation.
133
   * This proof generator is the one used in that TrustNode: it stores the
134
   * (closed) proofs of implications proved by the
135
   * ArithCongruenceManager/EqualityEngine.
136
   *
137
   * It is insufficient to just use the ProofGenerator from the ProofEqEngine,
138
   * since sometimes the ArithCongruenceManager needs to add some
139
   * arith-specific reasoning to extend the proof (e.g. rewriting the result
140
   * into a normal form).
141
   * */
142
  std::unique_ptr<EagerProofGenerator> d_pfGenExplain;
143
144
  /** Pointer to the proof equality engine of TheoryArith */
145
  theory::eq::ProofEqEngine* d_pfee;
146
147
  /** Raise a conflict node `conflict` to the theory of arithmetic.
148
   *
149
   * When proofs are enabled, a (closed) proof of the conflict should be
150
   * provided.
151
   */
152
  void raiseConflict(Node conflict, std::shared_ptr<ProofNode> pf = nullptr);
153
  /**
154
   * Are proofs enabled? This is true if a non-null proof manager was provided
155
   * to the constructor of this class.
156
   */
157
  bool isProofEnabled() const;
158
159
 public:
160
  bool inConflict() const;
161
162
  bool hasMorePropagations() const;
163
164
  const Node getNextPropagation();
165
166
  bool canExplain(TNode n) const;
167
168
private:
169
  Node externalToInternal(TNode n) const;
170
171
  void pushBack(TNode n);
172
173
  void pushBack(TNode n, TNode r);
174
175
  void pushBack(TNode n, TNode r, TNode w);
176
177
  bool propagate(TNode x);
178
  void explain(TNode literal, std::vector<TNode>& assumptions);
179
180
  /** Assert this literal to the eq engine. Common functionality for
181
   *   * assertionToEqualityEngine(..)
182
   *   * equalsConstant(c)
183
   *   * equalsConstant(lb, ub)
184
   * If proof is off, then just asserts.
185
   */
186
  void assertLitToEqualityEngine(Node lit,
187
                                 TNode reason,
188
                                 std::shared_ptr<ProofNode> pf);
189
  /** This sends a shared term to the uninterpreted equality engine. */
190
  void assertionToEqualityEngine(bool eq,
191
                                 ArithVar s,
192
                                 TNode reason,
193
                                 std::shared_ptr<ProofNode> pf);
194
195
  /** Check for proof for this or a symmetric fact
196
   *
197
   * The proof submitted to this method are stored in `d_pfGenEe`, and should
198
   * have closure properties consistent with the documentation for that member.
199
   *
200
   * @returns whether this or a symmetric fact has a proof.
201
   */
202
  bool hasProofFor(TNode f) const;
203
  /**
204
   * Sets the proof for this fact and the symmetric one.
205
   *
206
   * The proof submitted to this method are stored in `d_pfGenEe`, and should
207
   * have closure properties consistent with the documentation for that member.
208
   * */
209
  void setProofFor(TNode f, std::shared_ptr<ProofNode> pf) const;
210
211
  /** Dequeues the delay queue and asserts these equalities.*/
212
  void enableSharedTerms();
213
  void dequeueLiterals();
214
215
  void enqueueIntoNB(const std::set<TNode> all, NodeBuilder<>& nb);
216
217
  /**
218
   * Determine an explaination for `internal`. That is a conjunction of theory
219
   * literals which imply `internal`.
220
   *
221
   * The TrustNode here is a trusted propagation.
222
   */
223
  TrustNode explainInternal(TNode internal);
224
225
 public:
226
  ArithCongruenceManager(context::Context* satContext,
227
                         context::UserContext* u,
228
                         ConstraintDatabase&,
229
                         SetupLiteralCallBack,
230
                         const ArithVariables&,
231
                         RaiseEqualityEngineConflict raiseConflict,
232
                         ProofNodeManager* pnm);
233
  ~ArithCongruenceManager();
234
235
  //--------------------------------- initialization
236
  /**
237
   * Returns true if we need an equality engine, see
238
   * Theory::needsEqualityEngine.
239
   */
240
  bool needsEqualityEngine(EeSetupInfo& esi);
241
  /**
242
   * Finish initialize. This class is instructed by TheoryArithPrivate to use
243
   * the equality engine ee and proof equality engine pfee.
244
   */
245
  void finishInit(eq::EqualityEngine* ee, eq::ProofEqEngine* pfee);
246
  //--------------------------------- end initialization
247
248
  /**
249
   * Return the trust node for the explanation of literal. The returned
250
   * trust node is generated by the proof equality engine of this class.
251
   */
252
  TrustNode explain(TNode literal);
253
254
  void explain(TNode lit, NodeBuilder<>& out);
255
256
  void addWatchedPair(ArithVar s, TNode x, TNode y);
257
258
6044378
  inline bool isWatchedVariable(ArithVar s) const {
259
6044378
    return d_watchedVariables.isMember(s);
260
  }
261
262
  /** Assert an equality. */
263
  void watchedVariableIsZero(ConstraintCP eq);
264
265
  /** Assert a conjunction from lb and ub. */
266
  void watchedVariableIsZero(ConstraintCP lb, ConstraintCP ub);
267
268
  /** Assert that the value cannot be zero. */
269
  void watchedVariableCannotBeZero(ConstraintCP c);
270
271
  /** Assert that the value cannot be zero. */
272
  void watchedVariableCannotBeZero(ConstraintCP c, ConstraintCP d);
273
274
275
  /** Assert that the value is congruent to a constant. */
276
  void equalsConstant(ConstraintCP eq);
277
  void equalsConstant(ConstraintCP lb, ConstraintCP ub);
278
279
 private:
280
  class Statistics {
281
  public:
282
    IntStat d_watchedVariables;
283
    IntStat d_watchedVariableIsZero;
284
    IntStat d_watchedVariableIsNotZero;
285
286
    IntStat d_equalsConstantCalls;
287
288
    IntStat d_propagations;
289
    IntStat d_propagateConstraints;
290
    IntStat d_conflicts;
291
292
    Statistics();
293
    ~Statistics();
294
  } d_statistics;
295
296
};/* class ArithCongruenceManager */
297
298
std::vector<Node> andComponents(TNode an);
299
300
}/* CVC4::theory::arith namespace */
301
}/* CVC4::theory namespace */
302
}/* CVC4 namespace */