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

Line Exec Source
1
/*********************                                                        */
2
/*! \file eager_proof_generator.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Alex Ozdemir
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 eager proof generator class
13
 **/
14
15
#include "cvc4_private.h"
16
17
#ifndef CVC4__THEORY__EAGER_PROOF_GENERATOR_H
18
#define CVC4__THEORY__EAGER_PROOF_GENERATOR_H
19
20
#include "context/cdhashmap.h"
21
#include "expr/node.h"
22
#include "expr/proof_generator.h"
23
#include "expr/proof_rule.h"
24
#include "theory/trust_node.h"
25
26
namespace CVC4 {
27
28
class ProofNode;
29
class ProofNodeManager;
30
31
namespace theory {
32
33
/**
34
 * An eager proof generator, with explicit proof caching.
35
 *
36
 * The intended use of this class is to store proofs for lemmas and conflicts
37
 * at the time they are sent out on the ProofOutputChannel. This means that the
38
 * getProofForConflict and getProofForLemma methods are lookups in a
39
 * (user-context depedent) map, the field d_proofs below.
40
 *
41
 * In detail, the method setProofForConflict(conf, pf) should be called prior to
42
 * calling ProofOutputChannel(TrustNode(conf,X)), where X is this generator.
43
 * Similarly for setProofForLemma.
44
 *
45
 * The intended usage of this class in combination with OutputChannel is
46
 * the following:
47
 * //-----------------------------------------------------------
48
 *   class MyEagerProofGenerator : public EagerProofGenerator
49
 *   {
50
 *     public:
51
 *      TrustNode getProvenConflictByMethodX(...)
52
 *      {
53
 *        // construct a conflict
54
 *        Node conf = [construct conflict];
55
 *        // construct a proof for conf
56
 *        std::shared_ptr<ProofNode> pf = [construct the proof for conf];
57
 *        // wrap the conflict in a trust node
58
 *        return mkTrustNode(conf,pf);
59
 *      }
60
 *   };
61
 *   // [1] Make objects given user context u and output channel out.
62
 *
63
 *   MyEagerProofGenerator epg(u);
64
 *   OutputChannel out;
65
 *
66
 *   // [2] Assume epg realizes there is a conflict. We have it store the proof
67
 *   // internally and return the conflict node paired with epg.
68
 *
69
 *   TrustNode pconf = epg.getProvenConflictByMethodX(...);
70
 *
71
 *   // [3] Send the conflict on the output channel.
72
 *
73
 *   out.trustedConflict(pconf);
74
 *
75
 *   // [4] The trust node has information about what is proven and who can
76
 *   // prove it, where this association is valid in the remainder of the user
77
 *   // context.
78
 *
79
 *   Node conf = pconf.getProven();
80
 *   ProofGenerator * pg = pconf.getGenerator();
81
 *   std::shared_ptr<ProofNode> pf = pg->getProofForConflict(conf);
82
 * //-----------------------------------------------------------
83
 * In other words, the proof generator epg is responsible for creating and
84
 * storing the proof internally, and the proof output channel is responsible for
85
 * maintaining the map that epg is who to ask for the proof of the conflict.
86
 */
87
class EagerProofGenerator : public ProofGenerator
88
{
89
  typedef context::CDHashMap<Node, std::shared_ptr<ProofNode>, NodeHashFunction>
90
      NodeProofNodeMap;
91
92
 public:
93
  EagerProofGenerator(ProofNodeManager* pnm,
94
                      context::Context* c = nullptr,
95
                      std::string name = "EagerProofGenerator");
96
92587
  ~EagerProofGenerator() {}
97
  /** Get the proof for formula f. */
98
  std::shared_ptr<ProofNode> getProofFor(Node f) override;
99
  /** Can we give the proof for formula f? */
100
  bool hasProofFor(Node f) override;
101
  /**
102
   * Set proof for fact f, called when pf is a proof of f.
103
   *
104
   * @param f The fact proven by pf,
105
   * @param pf The proof to store in this class.
106
   */
107
  void setProofFor(Node f, std::shared_ptr<ProofNode> pf);
108
  /**
109
   * Make trust node: wrap n in a trust node with this generator, and have it
110
   * store the proof pf to lemma or conflict n.
111
   *
112
   * @param n The proven node,
113
   * @param pf The proof of n,
114
   * @param isConflict Whether the returned trust node is a conflict (otherwise
115
   * it is a lemma),
116
   * @return The trust node corresponding to the fact that this generator has
117
   * a proof of n.
118
   */
119
  TrustNode mkTrustNode(Node n,
120
                        std::shared_ptr<ProofNode> pf,
121
                        bool isConflict = false);
122
  /**
123
   * Make trust node from a single step proof. This is a convenience function
124
   * that avoids the need to explictly construct ProofNode by the caller.
125
   *
126
   * @param conc The conclusion of the rule,
127
   * @param id The rule of the proof concluding conc
128
   * @param exp The explanation (premises) to the proof concluding conc,
129
   * @param args The arguments to the proof concluding conc,
130
   * @param isConflict Whether the returned trust node is a conflict (otherwise
131
   * it is a lemma),
132
   * @return The trust node corresponding to the fact that this generator has
133
   * a proof of (children => exp), or of exp if children is empty.
134
   */
135
  TrustNode mkTrustNode(Node conc,
136
                        PfRule id,
137
                        const std::vector<Node>& exp,
138
                        const std::vector<Node>& args,
139
                        bool isConflict = false);
140
  /**
141
   * Make trust node: wrap `exp => n` in a trust node with this generator, and
142
   * have it store the proof `pf` too.
143
   *
144
   * @param n The implication
145
   * @param exp A conjunction of literals that imply it
146
   * @param pf The proof of exp => n,
147
   * @return The trust node corresponding to the fact that this generator has
148
   * a proof of exp => n.
149
   */
150
  TrustNode mkTrustedPropagation(Node n,
151
                                 Node exp,
152
                                 std::shared_ptr<ProofNode> pf);
153
  /**
154
   * Make trust node: `a = b` as a Rewrite trust node
155
   *
156
   * @param a the original
157
   * @param b what is rewrites to
158
   * @param pf The proof of a = b,
159
   * @return The trust node corresponding to the fact that this generator has
160
   * a proof of a = b
161
   */
162
  TrustNode mkTrustedRewrite(
163
      Node a, Node b, std::shared_ptr<ProofNode> pf);
164
  //--------------------------------------- common proofs
165
  /**
166
   * This returns the trust node corresponding to the splitting lemma
167
   * (or f (not f)) and this generator. The method registers its proof in the
168
   * map maintained by this class.
169
   */
170
  TrustNode mkTrustNodeSplit(Node f);
171
  //--------------------------------------- end common proofs
172
  /** identify */
173
  std::string identify() const override;
174
175
 protected:
176
  /** Set that pf is the proof for conflict conf */
177
  void setProofForConflict(Node conf, std::shared_ptr<ProofNode> pf);
178
  /** Set that pf is the proof for lemma lem */
179
  void setProofForLemma(Node lem, std::shared_ptr<ProofNode> pf);
180
  /** Set that pf is the proof for explained propagation */
181
  void setProofForPropExp(TNode lit, Node exp, std::shared_ptr<ProofNode> pf);
182
  /** The proof node manager */
183
  ProofNodeManager* d_pnm;
184
  /** Name identifier */
185
  std::string d_name;
186
  /** A dummy context used by this class if none is provided */
187
  context::Context d_context;
188
  /**
189
   * A user-context-dependent map from lemmas and conflicts to proofs provided
190
   * by calls to setProofForConflict and setProofForLemma above.
191
   */
192
  NodeProofNodeMap d_proofs;
193
};
194
195
}  // namespace theory
196
}  // namespace CVC4
197
198
#endif /* CVC4__THEORY__PROOF_GENERATOR_H */