Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Andrew Reynolds, Alex Ozdemir, Hans-Joerg Schurr
4 : : *
5 : : * This file is part of the cvc5 project.
6 : : *
7 : : * Copyright (c) 2009-2024 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.
11 : : * ****************************************************************************
12 : : *
13 : : * The eager proof generator class.
14 : : */
15 : :
16 : : #include "cvc5_private.h"
17 : :
18 : : #ifndef CVC5__PROOF__EAGER_PROOF_GENERATOR_H
19 : : #define CVC5__PROOF__EAGER_PROOF_GENERATOR_H
20 : :
21 : : #include "context/cdhashmap.h"
22 : : #include "expr/node.h"
23 : : #include "proof/proof_generator.h"
24 : : #include "cvc5/cvc5_proof_rule.h"
25 : : #include "proof/trust_node.h"
26 : : #include "smt/env_obj.h"
27 : :
28 : : namespace cvc5::internal {
29 : :
30 : : class ProofNode;
31 : : class ProofNodeManager;
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 : protected EnvObj, public ProofGenerator
88 : : {
89 : : typedef context::CDHashMap<Node, std::shared_ptr<ProofNode>> NodeProofNodeMap;
90 : :
91 : : public:
92 : : EagerProofGenerator(Env& env,
93 : : context::Context* c = nullptr,
94 : : std::string name = "EagerProofGenerator");
95 : 1152903 : ~EagerProofGenerator() {}
96 : : /** Get the proof for formula f. */
97 : : std::shared_ptr<ProofNode> getProofFor(Node f) override;
98 : : /** Can we give the proof for formula f? */
99 : : bool hasProofFor(Node f) override;
100 : : /**
101 : : * Set proof for fact f, called when pf is a proof of f.
102 : : *
103 : : * @param f The fact proven by pf,
104 : : * @param pf The proof to store in this class.
105 : : */
106 : : void setProofFor(Node f, std::shared_ptr<ProofNode> pf);
107 : : /**
108 : : * Make trust node: wrap n in a trust node with this generator, and have it
109 : : * store the proof pf to lemma or conflict n.
110 : : *
111 : : * @param n The proven node,
112 : : * @param pf The proof of n,
113 : : * @param isConflict Whether the returned trust node is a conflict (otherwise
114 : : * it is a lemma),
115 : : * @return The trust node corresponding to the fact that this generator has
116 : : * a proof of n.
117 : : */
118 : : TrustNode mkTrustNode(Node n,
119 : : std::shared_ptr<ProofNode> pf,
120 : : bool isConflict = false);
121 : : /**
122 : : * Make trust node from a single step proof. This is a convenience function
123 : : * that avoids the need to explictly construct ProofNode by the caller.
124 : : *
125 : : * @param conc The conclusion of the rule, or its negation if isConflict is
126 : : * true.
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 (exp => conc), or of conc if exp is empty.
134 : : */
135 : : TrustNode mkTrustNode(Node conc,
136 : : ProofRule id,
137 : : const std::vector<Node>& exp,
138 : : const std::vector<Node>& args,
139 : : bool isConflict = false);
140 : : /**
141 : : * Make trust node from a single step proof of a rewrite. This is a
142 : : * convenience function that avoids the need to explictly construct ProofNode
143 : : * by the caller.
144 : : *
145 : : * @param a the original
146 : : * @param b what is rewrites to
147 : : * @param id The rewrite rule of the proof concluding conc based on rewriting
148 : : * the term a.
149 : : * @return The trust node corresponding to the fact that this generator has
150 : : * a proof of a=b.
151 : : */
152 : : TrustNode mkTrustNodeRewrite(const Node& a,
153 : : const Node& b,
154 : : ProofRewriteRule id);
155 : : /**
156 : : * Make trust node: wrap `exp => n` in a trust node with this generator, and
157 : : * have it store the proof `pf` too.
158 : : *
159 : : * @param n The implication
160 : : * @param exp A conjunction of literals that imply it
161 : : * @param pf The proof of exp => n,
162 : : * @return The trust node corresponding to the fact that this generator has
163 : : * a proof of exp => n.
164 : : */
165 : : TrustNode mkTrustedPropagation(Node n,
166 : : Node exp,
167 : : std::shared_ptr<ProofNode> pf);
168 : : /**
169 : : * Make trust node: `a = b` as a Rewrite trust node
170 : : *
171 : : * @param a the original
172 : : * @param b what is rewrites to
173 : : * @param pf The proof of a = b,
174 : : * @return The trust node corresponding to the fact that this generator has
175 : : * a proof of a = b
176 : : */
177 : : TrustNode mkTrustedRewrite(Node a, Node b, std::shared_ptr<ProofNode> pf);
178 : : /**
179 : : * Make trust node from a single step proof. This is a convenience function
180 : : * that avoids the need to explictly construct ProofNode by the caller.
181 : : *
182 : : * @param a the original
183 : : * @param b what is rewrites to
184 : : * @param id The rule of the proof concluding a=b
185 : : * @param args The arguments to the proof concluding a=b,
186 : : * @return The trust node corresponding to the fact that this generator has
187 : : * a proof of a=b.
188 : : */
189 : : TrustNode mkTrustedRewrite(Node a,
190 : : Node b,
191 : : ProofRule id,
192 : : const std::vector<Node>& args);
193 : : //--------------------------------------- common proofs
194 : : /**
195 : : * This returns the trust node corresponding to the splitting lemma
196 : : * (or f (not f)) and this generator. The method registers its proof in the
197 : : * map maintained by this class.
198 : : */
199 : : TrustNode mkTrustNodeSplit(Node f);
200 : : //--------------------------------------- end common proofs
201 : : /** identify */
202 : : std::string identify() const override;
203 : :
204 : : protected:
205 : : /** Set that pf is the proof for conflict conf */
206 : : void setProofForConflict(Node conf, std::shared_ptr<ProofNode> pf);
207 : : /** Set that pf is the proof for lemma lem */
208 : : void setProofForLemma(Node lem, std::shared_ptr<ProofNode> pf);
209 : : /** Set that pf is the proof for explained propagation */
210 : : void setProofForPropExp(TNode lit, Node exp, std::shared_ptr<ProofNode> pf);
211 : : /** Name identifier */
212 : : std::string d_name;
213 : : /** A dummy context used by this class if none is provided */
214 : : context::Context d_context;
215 : : /**
216 : : * A user-context-dependent map from lemmas and conflicts to proofs provided
217 : : * by calls to setProofForConflict and setProofForLemma above.
218 : : */
219 : : NodeProofNodeMap d_proofs;
220 : : };
221 : :
222 : : } // namespace cvc5::internal
223 : :
224 : : #endif /* CVC5__PROOF__PROOF_GENERATOR_H */
|
