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

Line Exec Source
1
/*********************                                                        */
2
/*! \file eq_proof.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Haniel Barbosa, Dejan Jovanovic, Morgan Deters
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 A proof as produced by the equality engine.
13
 **
14
 **/
15
16
#include "cvc4_private.h"
17
#include "expr/node.h"
18
#include "theory/uf/equality_engine_types.h"
19
20
namespace CVC4 {
21
22
class CDProof;
23
24
namespace theory {
25
namespace eq {
26
27
/**
28
 * An equality proof.
29
 *
30
 * This represents the reasoning performed by the Equality Engine to derive
31
 * facts, represented in terms of the rules in MergeReasonType. Each proof step
32
 * is annotated with the rule id, the conclusion node and a vector of proofs of
33
 * the rule's premises.
34
 **/
35
2652818
class EqProof
36
{
37
 public:
38
2508493
  EqProof() : d_id(MERGED_THROUGH_REFLEXIVITY) {}
39
  /** The proof rule for concluding d_node */
40
  MergeReasonType d_id;
41
  /** The conclusion of this EqProof */
42
  Node d_node;
43
  /** The proofs of the premises for deriving d_node with d_id */
44
  std::vector<std::shared_ptr<EqProof>> d_children;
45
  /**
46
   * Debug print this proof on debug trace c with tabulation tb.
47
   */
48
  void debug_print(const char* c, unsigned tb = 0) const;
49
  /**
50
   * Debug print this proof on output stream os with tabulation tb.
51
   */
52
  void debug_print(std::ostream& os, unsigned tb = 0) const;
53
54
  /** Add to proof
55
   *
56
   * Converts EqProof into ProofNode via a series of steps to be stored in
57
   * CDProof* p.
58
   *
59
   * This method can be seen as a best-effort solution until the EqualityEngine
60
   * is updated to produce ProofNodes directly, if ever. Note that since the
61
   * original EqProof steps can be coarse-grained (e.g. without proper order,
62
   * implicit inferences related to disequelaties) and are phrased over curried
63
   * terms, the transformation requires significant, although cheap (mostly
64
   * linear on the DAG-size of EqProof), post-processing.
65
   *
66
   * An important invariant of the resulting ProofNode is that neither its
67
   * assumptions nor its conclusion are predicate equalities, i.e. of the form
68
   * (= t true/false), modulo symmetry. This is so that users of the converted
69
   * ProofNode don't need to do case analysis on whether assumptions/conclusion
70
   * are either t or (= t true/false).
71
   *
72
   * @param p a pointer to a CDProof to store the conversion of this EqProof
73
   * @return the node that is the conclusion of the proof as added to p.
74
   */
75
  Node addToProof(CDProof* p) const;
76
77
 private:
78
  /**
79
   * As above, but with a cache of previously processed nodes and their results
80
   * (for DAG traversal). The caching is in terms of the original conclusions of
81
   * EqProof.
82
   *
83
   * @param p a pointer to a CDProof to store the conversion of this EqProof
84
   * @param visited a cache of the original EqProof conclusions and the
85
   * resulting conclusion after conversion.
86
   * @param assumptions the assumptions of the original EqProof (and their
87
   * variations in terms of symmetry and conversion to/from predicate
88
   * equalities)
89
   * @return the node that is the conclusion of the proof as added to p.
90
   */
91
  Node addToProof(
92
      CDProof* p,
93
      std::unordered_map<Node, Node, NodeHashFunction>& visited,
94
      std::unordered_set<Node, NodeHashFunction>& assumptions) const;
95
96
  /** Removes all reflexivity steps, i.e. (= t t), from premises. */
97
  void cleanReflPremises(std::vector<Node>& premises) const;
98
99
  /** Expand coarse-grained transitivity steps for disequalities
100
   *
101
   * Currently the equality engine can represent disequality reasoning in a
102
   * rather coarse-grained manner with EqProof. This is always the case when the
103
   * transitivity step contains a disequality, (= (= t t') false) or its
104
   * symmetric, as a premise.
105
   *
106
   * There are two cases. In the simplest one the general shape of the EqProof
107
   * is
108
   *  (= t1 t2) (= t3 t2) (= (t1 t3) false)
109
   *  ------------------------------------- EQP::TR
110
   *             false = true
111
   *
112
   * which is expanded into
113
   *                                          (= t3 t2)
114
   *                                          --------- SYMM
115
   *                                (= t1 t2) (= t2 t3)
116
   *                                ------------------- TRANS
117
   *   (= (= t1 t3) false)                (= t1 t3)
118
   *  --------------------- SYMM    ------------------ TRUE_INTRO
119
   *   (= false (= t1 t3))         (= (= t1 t3) true)
120
   *  ----------------------------------------------- TRANS
121
   *             false = true
122
   *
123
   * by explicitly adding the transitivity step for inferring (= t1 t3) and its
124
   * predicate equality. Note that we differentiate (from now on) the EqProof
125
   * rules ids from those of ProofRule by adding the prefix EQP:: to the former.
126
   *
127
   * In the other case, the general shape of the EqProof is
128
   *
129
   *  (= (= t1 t2) false) (= t1 x1) ... (= xn t3) (= t2 y1) ... (= ym t4)
130
   * ------------------------------------------------------------------- EQP::TR
131
   *         (= (= t4 t3) false)
132
   *
133
   * which is converted into
134
   *
135
   *   (= t1 x1) ... (= xn t3)      (= t2 y1) ... (= ym t4)
136
   *  ------------------------ TR  ------------------------ TR
137
   *   (= t1 t3)                    (= t2 t4)
138
   *  ----------- SYMM             ----------- SYMM
139
   *   (= t3 t1)                    (= t4 t2)
140
   *  ---------------------------------------- CONG
141
   *   (= (= t3 t4) (= t1 t2))                         (= (= t1 t2) false)
142
   *  --------------------------------------------------------------------- TR
143
   *           (= (= t3 t4) false)
144
   *          --------------------- MACRO_SR_PRED_TRANSFORM
145
   *           (= (= t4 t3) false)
146
   *
147
   * whereas the last step is only necessary if the conclusion has the arguments
148
   * in reverse order than expected. Note that the original step represents two
149
   * substitutions happening on the disequality, from t1->t3 and t2->t4, which
150
   * are implicitly justified by transitivity steps that need to be made
151
   * explicity. Since there is no sense of ordering among which premisis (other
152
   * than (= (= t1 t2) false)) are used for which substitution, the transitivity
153
   * proofs are built greedly by searching the sets of premises.
154
   *
155
   * If in either of the above cases then the conclusion is directly derived
156
   * in the call, so only in the other cases we try to build a transitivity
157
   * step below
158
   *
159
   * @param conclusion the conclusion of the (possibly) coarse-grained
160
   * transitivity step
161
   * @param premises the premises of the (possibly) coarse-grained
162
   * transitivity step
163
   * @param p a pointer to a CDProof to store the conversion of this EqProof
164
   * @param assumptions the assumptions (and variants) of the original
165
   * EqProof. These are necessary to avoid cyclic proofs, which could be
166
   * generated by creating transitivity steps for assumptions (which depend on
167
   * themselves).
168
   * @return True if the EqProof transitivity step is in either of the above
169
   * cases, symbolizing that the ProofNode justifying the conclusion has already
170
   * been produced.
171
   */
172
  bool expandTransitivityForDisequalities(
173
      Node conclusion,
174
      std::vector<Node>& premises,
175
      CDProof* p,
176
      std::unordered_set<Node, NodeHashFunction>& assumptions) const;
177
178
  /** Expand coarse-grained transitivity steps for theory disequalities
179
   *
180
   * Currently the equality engine can represent disequality reasoning of theory
181
   * symbols in a rather coarse-grained manner with EqProof. This is the case
182
   * when EqProof is
183
   *            (= t1 c1) (= t2 c2)
184
   *  ------------------------------------- EQP::TR
185
   *             (= (t1 t2) false)
186
   *
187
   * which is converted into
188
   *
189
   *   (= t1 c1)        (= t2 c2)
190
   *  -------------------------- CONG  --------------------- MACRO_SR_PRED_INTRO
191
   *   (= (= t1 t2) (= c1 t2))           (= (= c1 c2) false)
192
   *  --------------------------------------------------------- TR
193
   *           (= (= t1 t2) false)
194
   *
195
   * @param conclusion the conclusion of the (possibly) coarse-grained
196
   * transitivity step
197
   * @param premises the premises of the (possibly) coarse-grained
198
   * transitivity step
199
   * @param p a pointer to a CDProof to store the conversion of this EqProof
200
   * @return True if the EqProof transitivity step is the above case,
201
   * indicating that the ProofNode justifying the conclusion has already been
202
   * produced.
203
   */
204
  bool expandTransitivityForTheoryDisequalities(Node conclusion,
205
                                                std::vector<Node>& premises,
206
                                                CDProof* p) const;
207
208
  /** Builds a transitivity chain from equalities to derive a conclusion
209
   *
210
   * Given an equality (= t1 tn), and a list of equalities premises, attempts to
211
   * build a chain (= t1 t2) ... (= tn-1 tn) from premises. This is done in a
212
   * greedy manner by finding one "link" in the chain at a time, updating the
213
   * conclusion to be the next link and the premises by removing the used
214
   * premise, and searching recursively.
215
   *
216
   * Consider for example
217
   * - conclusion: (= t1 t4)
218
   * - premises:   (= t4 t2), (= t2 t3), (= t2 t1), (= t3 t4)
219
   *
220
   * It proceeds by searching for t1 in an equality in the premises, in order,
221
   * which is found in the equality (= t2 t1). Since t2 != t4, it attempts to
222
   * build a chain with
223
   * - conclusion (= t2 t4)
224
   * - premises (= t4 t2), (= t2 t3), (= t3 t4)
225
   *
226
   * In the first equality it finds t2 and also t4, which closes the chain, so
227
   * that premises is updated to (= t2 t4) and the method returns true. Since
228
   * the recursive call was successful, the original conclusion (= t1 t4) is
229
   * justified with (= t1 t2) plus the chain built in the recursive call,
230
   * i.e. (= t1 t2), (= t2 t4).
231
   *
232
   * Note that not all the premises were necessary to build a successful
233
   * chain. Moreover, note that building a successful chain can depend on the
234
   * order in which the equalities are chosen. When a recursive call fails to
235
   * close a chain, the chosen equality is dismissed and another is searched for
236
   * among the remaining ones.
237
   *
238
   * This method assumes that premises does not contain reflexivity premises.
239
   * This is without loss of generality since such premises are spurious for a
240
   * transitivity step.
241
   *
242
   * @param conclusion the conclusion of the transitivity chain of equalities
243
   * @param premises the list of equalities to build a chain with
244
   * @return whether premises successfully build a transitivity chain for the
245
   * conclusion
246
   */
247
  bool buildTransitivityChain(Node conclusion,
248
                              std::vector<Node>& premises) const;
249
250
  /** Reduce the a congruence EqProof into a transitivity matrix
251
   *
252
   * Given a congruence EqProof of (= (f a0 ... an-1) (f b0 ... bn-1)), reduce
253
   * its justification into a matrix
254
   *
255
   *   [0]   -> p_{0,0} ... p_{m_0,0}
256
   *   ...
257
   *   [n-1] -> p_{0,n} ... p_{m_n-1,n-1}
258
   *
259
   * where f has arity n and each p_{0,i} ... p_{m_i, i} is a transitivity chain
260
   * (modulo ordering) justifying (= ai bi).
261
   *
262
   * Congruence steps in EqProof are binary, representing reasoning over curried
263
   * applications. In the simplest case the general shape of a congruence
264
   * EqProof is:
265
   *                                     P0
266
   *              ------- EQP::REFL  ----------
267
   *       P1        []               (= a0 b0)
268
   *  ---------   ----------------------- EQP::CONG
269
   *  (= a1 b1)             []                        P2
270
   *  ------------------------- EQP::CONG        -----------
271
   *             []                               (= a2 b2)
272
   *          ------------------------------------------------ EQP::CONG
273
   *                  (= (f a0 a1 a2) (f b0 b1 b2))
274
   *
275
   * where [] stands for the null node, symbolizing "equality between partial
276
   * applications".
277
   *
278
   * The reduction of such a proof is done by
279
   * - converting the proof of the second CONG premise (via addToProof) and
280
   *   adding the resulting node to row i of the matrix
281
   * - recursively reducing the first proof with i-1
282
   *
283
   * In the above case the transitivity matrix would thus be
284
   *   [0] -> (= a0 b0)
285
   *   [1] -> (= a1 b1)
286
   *   [2] -> (= a2 b2)
287
   *
288
   * The more complex case of congruence proofs has transitivity steps as the
289
   * first child of CONG steps. For example
290
   *                                     P0
291
   *              ------- EQP::REFL  ----------
292
   *     P'          []            (= a0 c)
293
   *  ---------   ----------------------------- EQP::CONG
294
   *  (= b0 c)             []                               P1
295
   * ------------------------- EQP::TRANS             -----------
296
   *            []                                     (= a1 b1)
297
   *         ----------------------------------------------------- EQP::CONG
298
   *                          (= (f a0 a1) (f b0 b1))
299
   *
300
   * where when the first child of CONG is a transitivity step
301
   * - the premises that are CONG steps are recursively reduced with *the same*
302
       argument i
303
   * - the other premises are processed with addToProof and added to the i row
304
   *   in the matrix
305
   *
306
   * In the above example the to which the transitivity matrix is
307
   *   [0] -> (= a0 c), (= b0 c)
308
   *   [1] -> (= a1 b1)
309
   *
310
   * The remaining complication is that when conclusion is an equality of n-ary
311
   * applications of *different* arities, there is, necessarily, a transitivity
312
   * step as a first child a CONG step whose conclusion is an equality of n-ary
313
   * applications of different arities. For example
314
   *             P0                              P1
315
   * -------------------------- EQP::TRANS  -----------
316
   *     (= (f a0 a1) (f b0))                (= a2 b1)
317
   * -------------------------------------------------- EQP::CONG
318
   *              (= (f a0 a1 a2) (f b0 b1))
319
   *
320
   * will be first reduced with i = 2 (maximal arity amorg the original
321
   * conclusion's applications), adding (= a2 b1) to row 2 after processing
322
   * P1. The first child is reduced with i = 1. Since it is a TRANS step whose
323
   * conclusion is an equality of n-ary applications with mismatching arity, P0
324
   * is processed with addToProof and the result is added to row 1. Thus the
325
   * transitivity matrix is
326
   *   [0] ->
327
   *   [1] -> (= (f a0 a1) (f b0))
328
   *   [2] -> (= a2 b1)
329
   *
330
   * The empty row 0 is used by the original caller of reduceNestedCongruence to
331
   * compute that the above congruence proof's conclusion is
332
   *   (= (f (f a0 a1) a2) (f (f b0) b1))
333
   *
334
   * @param i the i-th argument of the congruent applications, initially being
335
   * the maximal arity among conclusion's applications.
336
   * @param conclusion the original congruence conclusion
337
   * @param transitivityMatrix a matrix of equalities with each row justifying
338
   * an equality between the congruent applications
339
   * @param p a pointer to a CDProof to store the conversion of this EqProof
340
   * @param visited a cache of the original EqProof conclusions and the
341
   * resulting conclusion after conversion.
342
   * @param assumptions the assumptions (and variants) of the original EqProof
343
   * @param isNary whether conclusion is an equality of n-ary applications
344
   */
345
  void reduceNestedCongruence(
346
      unsigned i,
347
      Node conclusion,
348
      std::vector<std::vector<Node>>& transitivityMatrix,
349
      CDProof* p,
350
      std::unordered_map<Node, Node, NodeHashFunction>& visited,
351
      std::unordered_set<Node, NodeHashFunction>& assumptions,
352
      bool isNary) const;
353
354
}; /* class EqProof */
355
356
}  // Namespace eq
357
}  // Namespace theory
358
}  // Namespace CVC4