GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/uf/proof_equality_engine.h Lines: 1 1 100.0 %
Date: 2021-03-22 Branches: 0 0 0.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file proof_equality_engine.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Haniel Barbosa
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 The proof-producing equality engine
13
 **/
14
15
#include "cvc4_private.h"
16
17
#ifndef CVC4__THEORY__UF__PROOF_EQUALITY_ENGINE_H
18
#define CVC4__THEORY__UF__PROOF_EQUALITY_ENGINE_H
19
20
#include <vector>
21
22
#include "context/cdhashmap.h"
23
#include "context/cdhashset.h"
24
#include "expr/buffered_proof_generator.h"
25
#include "expr/lazy_proof.h"
26
#include "expr/node.h"
27
#include "theory/eager_proof_generator.h"
28
29
namespace CVC4 {
30
31
class ProofNode;
32
class ProofNodeManager;
33
34
namespace theory {
35
namespace eq {
36
37
class EqualityEngine;
38
39
/**
40
 * A layer on top of an EqualityEngine. The goal of this class is manage the
41
 * use of an EqualityEngine object in such a way that the proper proofs are
42
 * internally constructed, and can be retrieved from this class when
43
 * necessary.
44
 *
45
 * Notice that this class is intended to be a *partial layer* on top of
46
 * equality engine. A user of this class should still issue low-level calls
47
 * (getRepresentative, areEqual, areDisequal, etc.) on the underlying equality
48
 * engine directly. The methods that should *not* be called directly on the
49
 * underlying equality engine are:
50
 * - assertEquality/assertPredicate [*]
51
 * - explain
52
 * Instead, the user should use variants of the above methods provided by
53
 * the public interface of this class.
54
 *
55
 * [*] the exception is that assertions from the fact queue (who are their own
56
 * explanation) should be sent directly to the underlying equality engine. This
57
 * is for the sake of efficiency.
58
 *
59
 * This class tracks the reason for why all facts are added to an EqualityEngine
60
 * in a SAT-context dependent manner in a context-dependent (CDProof) object.
61
 * It furthermore maintains an internal FactProofGenerator class for managing
62
 * proofs of facts whose steps are explicitly provided (those that are given
63
 * concrete PfRule, children, and args). Call these "simple facts".
64
 *
65
 * Overall, this class is an eager proof generator (theory/proof_generator.h),
66
 * in that it stores (copies) of proofs for lemmas at the moment they are sent
67
 * out.
68
 *
69
 * A theory that is proof producing and uses the equality engine may use this
70
 * class to manage proofs that are justified by its underlying equality engine.
71
 * In particular, the following interfaces are available for constructing
72
 * a TrustNode:
73
 * - assertConflict, when the user of the equality engine has discovered that
74
 * false can be derived from the current state,
75
 * - assertLemma, for lemmas/conflicts that can be (partially) explained in the
76
 * current state,
77
 * - explain, for explaining why a literal is true in the current state.
78
 * Details on these methods can be found below.
79
 */
80
class ProofEqEngine : public EagerProofGenerator
81
{
82
  typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
83
  typedef context::CDHashMap<Node, std::shared_ptr<ProofNode>, NodeHashFunction>
84
      NodeProofMap;
85
86
 public:
87
  ProofEqEngine(context::Context* c,
88
                context::UserContext* u,
89
                EqualityEngine& ee,
90
                ProofNodeManager* pnm);
91
14330
  ~ProofEqEngine() {}
92
  //-------------------------- assert fact
93
  /**
94
   * Assert the literal lit by proof step id, given explanation exp and
95
   * arguments args. This fact is
96
   *
97
   * @param lit The literal to assert to the equality engine
98
   * @param id The proof rule of the proof step concluding lit
99
   * @param exp The premises of the proof step concluding lit. These are also
100
   * the premises that are used when calling explain(lit).
101
   * @param args The arguments to the proof step concluding lit.
102
   * @return true if this fact was processed by this method. If lit already
103
   * holds in the equality engine, this method returns false.
104
   */
105
  bool assertFact(Node lit,
106
                  PfRule id,
107
                  const std::vector<Node>& exp,
108
                  const std::vector<Node>& args);
109
  /** Same as above but where exp is (conjunctive) node */
110
  bool assertFact(Node lit, PfRule id, Node exp, const std::vector<Node>& args);
111
  /**
112
   * Multi-step version of assert fact via a proof step buffer. This method
113
   * is similar to above, but the justification for lit may have multiple steps.
114
   * In particular, we assume that psb has a list of proof steps where the
115
   * proof step concluding lit has free assumptions exp.
116
   *
117
   * For example, a legal call to this method is such that:
118
   *   lit: A
119
   *   exp: B
120
   *   psb.d_steps: { A by (step id1 {B,C} {}), C by (step id2 {} {}) )
121
   * In other words, A holds by a proof step with rule id1 and premises
122
   * B and C, and C holds by proof step with rule id2 and no premises.
123
   *
124
   * @param lit The literal to assert to the equality engine.
125
   * @param exp The premises of the proof steps concluding lit. These are also
126
   * the premises that are used when calling explain(lit).
127
   * @param psb The proof step buffer containing the proof steps.
128
   * @return true if this fact was processed by this method. If lit already
129
   * holds in the equality engine, this method returns false.
130
   */
131
  bool assertFact(Node lit, Node exp, ProofStepBuffer& psb);
132
  /**
133
   * Assert fact via generator pg. This method asserts lit with explanation exp
134
   * to the equality engine of this class. It must be the case that pg can
135
   * provide a proof for lit in terms of exp. More precisely, pg should be
136
   * prepared in the remainder of the SAT context to respond to a call to
137
   * ProofGenerator::getProofFor(lit), and return a proof whose free
138
   * assumptions are a subset of the conjuncts of exp.
139
   *
140
   * @param lit The literal to assert to the equality engine.
141
   * @param exp The premises of the proof concluding lit. These are also
142
   * the premises that are used when calling explain(lit).
143
   * @param pg The proof generator that can provide a proof concluding lit
144
   * from free asumptions in exp.
145
   * @return true if this fact was processed by this method. If lit already
146
   * holds in the equality engine, this method returns false.
147
   */
148
  bool assertFact(Node lit, Node exp, ProofGenerator* pg);
149
  //-------------------------- assert conflicts
150
  /**
151
   * This method is called when the equality engine of this class is
152
   * inconsistent (false has been proven) by a contradictory literal lit. This
153
   * returns the trust node corresponding to the current conflict.
154
   *
155
   * @param lit The conflicting literal, which must rewrite to false.
156
   * @return The trust node capturing the fact that this class can provide a
157
   * proof for this conflict.
158
   */
159
  TrustNode assertConflict(Node lit);
160
  /**
161
   * Get proven conflict from contradictory facts. This method is called when
162
   * the proof rule with premises exp and arguments args implies a contradiction
163
   * by proof rule id.
164
   *
165
   * This method returns the TrustNode containing the corresponding conflict
166
   * resulting from adding this step, and ensures that a proof has been stored
167
   * internally so that this class may respond to a call to
168
   * ProofGenerator::getProof(...).
169
   */
170
  TrustNode assertConflict(PfRule id,
171
                           const std::vector<Node>& exp,
172
                           const std::vector<Node>& args);
173
  /** Generator version, where pg has a proof of false from assumptions exp */
174
  TrustNode assertConflict(const std::vector<Node>& exp, ProofGenerator* pg);
175
  //-------------------------- assert lemma
176
  /**
177
   * Called when we have concluded conc, typically via theory specific
178
   * reasoning. The purpose of this method is to construct a TrustNode of
179
   * kind TrustNodeKind::LEMMA or TrustNodeKind::CONFLICT corresponding to the
180
   * lemma or conflict to be sent on the output channel of the Theory.
181
   *
182
   * The user provides the explanation of conc in two parts:
183
   * (1) (exp \ noExplain), which are literals that hold in the equality engine
184
   * of this class,
185
   * (2) noExplain, which do not necessarily hold in the equality engine of this
186
   * class.
187
   * Notice that noExplain is a subset of exp.
188
   *
189
   * The proof for conc follows from exp by proof rule with the given
190
   * id and arguments.
191
   *
192
   * This call corresponds to a conflict if conc is false and noExplain is
193
   * empty.
194
   *
195
   * This returns the TrustNode corresponding to the formula corresonding to
196
   * the call to this method [*], for which a proof can be provided by this
197
   * generator in the remainder of the user context.
198
   *
199
   * [*]
200
   * a. If this call does not correspond to a conflict, then this formula is:
201
   *   ( ^_{e in exp \ noExplain} <explain>(e) ^ noExplain ) => conc
202
   * where <explain>(e) is a conjunction of literals L1 ^ ... ^ Ln such that
203
   * L1 ^ ... ^ Ln entail e, and each Li was passed as an explanation to a
204
   * call to assertFact in the current SAT context. This explanation method
205
   * always succeeds, provided that e is a literal that currently holds in
206
   * the equality engine of this class. Notice that if the antecedant is empty,
207
   * the formula above is assumed to be conc itself. The above formula is
208
   * intended to be valid in Theory that owns this class.
209
   * b. If this call is a conflict, then this formula is:
210
   *   ^_{e in exp} <explain>(e)
211
   * The formula can be queried via TrustNode::getProven in the standard way.
212
   */
213
  TrustNode assertLemma(Node conc,
214
                        PfRule id,
215
                        const std::vector<Node>& exp,
216
                        const std::vector<Node>& noExplain,
217
                        const std::vector<Node>& args);
218
  /** Generator version, where pg has a proof of conc */
219
  TrustNode assertLemma(Node conc,
220
                        const std::vector<Node>& exp,
221
                        const std::vector<Node>& noExplain,
222
                        ProofGenerator* pg);
223
  //-------------------------- explain
224
  /**
225
   * Explain literal conc. This calls the appropriate methods in the underlying
226
   * equality engine of this class to construct the explanation of why conc
227
   * currently holds.
228
   *
229
   * It returns a trust node of kind TrustNodeKind::PROP_EXP whose node
230
   * is the explanation of conc (a conjunction of literals that implies it).
231
   * The proof that can be proven by this generator is then (=> exp conc), see
232
   * TrustNode::getPropExpProven(conc,exp);
233
   *
234
   * @param conc The conclusion to explain
235
   * @return The trust node indicating the explanation of conc and the generator
236
   * (this class) that can prove the implication.
237
   */
238
  TrustNode explain(Node conc);
239
240
 private:
241
  /** Assert internal */
242
  bool assertFactInternal(TNode pred, bool polarity, TNode reason);
243
  /** holds */
244
  bool holds(TNode pred, bool polarity);
245
  /**
246
   * Ensure proof for fact. This is called by the above method after we have
247
   * determined the final set of assumptions used for showing conc. This
248
   * method is used for lemmas, conflicts, and explanations for propagations.
249
   * The argument tnk is the kind of trust node to return.
250
   */
251
  TrustNode ensureProofForFact(Node conc,
252
                               const std::vector<TNode>& assumps,
253
                               TrustNodeKind tnk,
254
                               ProofGenerator* curr);
255
  /**
256
   * This ensures the proof of the literals that are in exp but not in
257
   * noExplain have been added to curr. This additionally adds the
258
   * explanation of exp to assumps. It updates tnk to LEMMA if there
259
   * are any literals in exp that are not in noExplain.
260
   */
261
  void explainVecWithProof(TrustNodeKind& tnk,
262
                           std::vector<TNode>& assumps,
263
                           const std::vector<Node>& exp,
264
                           const std::vector<Node>& noExplain,
265
                           LazyCDProof* curr);
266
  /** Explain
267
   *
268
   * This adds to assumps the set of facts that were asserted to this
269
   * class in the current SAT context that are required for showing lit.
270
   *
271
   * This additionally registers the equality proof steps required to
272
   * regress the explanation of lit in curr.
273
   */
274
  void explainWithProof(Node lit,
275
                        std::vector<TNode>& assumps,
276
                        LazyCDProof* curr);
277
  /** Reference to the equality engine */
278
  eq::EqualityEngine& d_ee;
279
  /** The default proof generator (for simple facts) */
280
  BufferedProofGenerator d_factPg;
281
  /** common nodes */
282
  Node d_true;
283
  Node d_false;
284
  /** the proof node manager */
285
  ProofNodeManager* d_pnm;
286
  /** The SAT-context-dependent proof object */
287
  LazyCDProof d_proof;
288
  /**
289
   * The keep set of this class. This set is maintained to ensure that
290
   * facts and their explanations are reference counted. Since facts and their
291
   * explanations are SAT-context-dependent, this set is also
292
   * SAT-context-dependent.
293
   */
294
  NodeSet d_keep;
295
};
296
297
}  // namespace eq
298
}  // namespace theory
299
}  // namespace CVC4
300
301
#endif /* CVC4__THEORY__STRINGS__PROOF_MANAGER_H */