Branch data Line data Source code
1 : : /******************************************************************************
2 : : * This file is part of the cvc5 project.
3 : : *
4 : : * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
5 : : * in the top-level source directory and their institutional affiliations.
6 : : * All rights reserved. See the file COPYING in the top-level source
7 : : * directory for licensing information.
8 : : * ****************************************************************************
9 : : *
10 : : * The eager proof generator class.
11 : : */
12 : :
13 : : #include "cvc5_private.h"
14 : :
15 : : #ifndef CVC5__PROOF__EAGER_PROOF_GENERATOR_H
16 : : #define CVC5__PROOF__EAGER_PROOF_GENERATOR_H
17 : :
18 : : #include "context/cdhashmap.h"
19 : : #include "cvc5/cvc5_proof_rule.h"
20 : : #include "expr/node.h"
21 : : #include "proof/proof_generator.h"
22 : : #include "proof/trust_id.h"
23 : : #include "proof/trust_node.h"
24 : : #include "smt/env_obj.h"
25 : :
26 : : namespace cvc5::internal {
27 : :
28 : : class ProofNode;
29 : : class ProofNodeManager;
30 : :
31 : : /**
32 : : * An eager proof generator, with explicit proof caching.
33 : : *
34 : : * The intended use of this class is to store proofs for lemmas and conflicts
35 : : * at the time they are sent out on the ProofOutputChannel. This means that the
36 : : * getProofForConflict and getProofForLemma methods are lookups in a
37 : : * (user-context depedent) map, the field d_proofs below.
38 : : *
39 : : * In detail, the method setProofForConflict(conf, pf) should be called prior to
40 : : * calling ProofOutputChannel(TrustNode(conf,X)), where X is this generator.
41 : : * Similarly for setProofForLemma.
42 : : *
43 : : * The intended usage of this class in combination with OutputChannel is
44 : : * the following:
45 : : * //-----------------------------------------------------------
46 : : * class MyEagerProofGenerator : public EagerProofGenerator
47 : : * {
48 : : * public:
49 : : * TrustNode getProvenConflictByMethodX(...)
50 : : * {
51 : : * // construct a conflict
52 : : * Node conf = [construct conflict];
53 : : * // construct a proof for conf
54 : : * std::shared_ptr<ProofNode> pf = [construct the proof for conf];
55 : : * // wrap the conflict in a trust node
56 : : * return mkTrustNode(conf,pf);
57 : : * }
58 : : * };
59 : : * // [1] Make objects given user context u and output channel out.
60 : : *
61 : : * MyEagerProofGenerator epg(u);
62 : : * OutputChannel out;
63 : : *
64 : : * // [2] Assume epg realizes there is a conflict. We have it store the proof
65 : : * // internally and return the conflict node paired with epg.
66 : : *
67 : : * TrustNode pconf = epg.getProvenConflictByMethodX(...);
68 : : *
69 : : * // [3] Send the conflict on the output channel.
70 : : *
71 : : * out.trustedConflict(pconf);
72 : : *
73 : : * // [4] The trust node has information about what is proven and who can
74 : : * // prove it, where this association is valid in the remainder of the user
75 : : * // context.
76 : : *
77 : : * Node conf = pconf.getProven();
78 : : * ProofGenerator * pg = pconf.getGenerator();
79 : : * std::shared_ptr<ProofNode> pf = pg->getProofForConflict(conf);
80 : : * //-----------------------------------------------------------
81 : : * In other words, the proof generator epg is responsible for creating and
82 : : * storing the proof internally, and the proof output channel is responsible for
83 : : * maintaining the map that epg is who to ask for the proof of the conflict.
84 : : */
85 : : class EagerProofGenerator : protected EnvObj, public ProofGenerator
86 : : {
87 : : typedef context::CDHashMap<Node, std::shared_ptr<ProofNode>> NodeProofNodeMap;
88 : :
89 : : public:
90 : : EagerProofGenerator(Env& env,
91 : : context::Context* c = nullptr,
92 : : std::string name = "EagerProofGenerator");
93 : 816431 : ~EagerProofGenerator() {}
94 : : /** Get the proof for formula f. */
95 : : std::shared_ptr<ProofNode> getProofFor(Node f) override;
96 : : /** Can we give the proof for formula f? */
97 : : bool hasProofFor(Node f) override;
98 : : /**
99 : : * Set proof for fact f, called when pf is a proof of f.
100 : : *
101 : : * @param f The fact proven by pf,
102 : : * @param pf The proof to store in this class.
103 : : */
104 : : void setProofFor(Node f, std::shared_ptr<ProofNode> pf);
105 : : /**
106 : : * Make trust node: wrap n in a trust node with this generator, and have it
107 : : * store the proof pf to lemma or conflict n.
108 : : *
109 : : * @param n The proven node,
110 : : * @param pf The proof of n,
111 : : * @param isConflict Whether the returned trust node is a conflict (otherwise
112 : : * it is a lemma),
113 : : * @return The trust node corresponding to the fact that this generator has
114 : : * a proof of n.
115 : : */
116 : : TrustNode mkTrustNode(Node n,
117 : : std::shared_ptr<ProofNode> pf,
118 : : bool isConflict = false);
119 : : /**
120 : : * Make trust node from a single step proof. This is a convenience function
121 : : * that avoids the need to explictly construct ProofNode by the caller.
122 : : *
123 : : * @param conc The conclusion of the rule, or its negation if isConflict is
124 : : * true.
125 : : * @param id The rule of the proof concluding conc
126 : : * @param exp The explanation (premises) to the proof concluding conc,
127 : : * @param args The arguments to the proof concluding conc,
128 : : * @param isConflict Whether the returned trust node is a conflict (otherwise
129 : : * it is a lemma),
130 : : * @return The trust node corresponding to the fact that this generator has
131 : : * a proof of (exp => conc), or of conc if exp is empty.
132 : : */
133 : : TrustNode mkTrustNode(Node conc,
134 : : ProofRule id,
135 : : const std::vector<Node>& exp,
136 : : const std::vector<Node>& args,
137 : : bool isConflict = false);
138 : : /**
139 : : * Same as above, but with a trusted id.
140 : : *
141 : : * @param conc The conclusion of the rule, or its negation if isConflict is
142 : : * true.
143 : : * @param id The trust id of the proof concluding conc
144 : : * @param exp The explanation (premises) to the proof concluding conc,
145 : : * @param args The arguments to the proof concluding conc,
146 : : * @param isConflict Whether the returned trust node is a conflict (otherwise
147 : : * it is a lemma),
148 : : * @return The trust node corresponding to the fact that this generator has
149 : : * a proof of (exp => conc), or of conc if exp is empty.
150 : : */
151 : : TrustNode mkTrustNodeTrusted(Node conc,
152 : : TrustId id,
153 : : const std::vector<Node>& exp,
154 : : const std::vector<Node>& args,
155 : : bool isConflict = false);
156 : : /**
157 : : * Make trust node from a single step proof of a rewrite. This is a
158 : : * convenience function that avoids the need to explictly construct ProofNode
159 : : * by the caller.
160 : : *
161 : : * @param a the original
162 : : * @param b what is rewrites to
163 : : * @param id The rewrite rule of the proof concluding conc based on rewriting
164 : : * the term a.
165 : : * @return The trust node corresponding to the fact that this generator has
166 : : * a proof of a=b.
167 : : */
168 : : TrustNode mkTrustNodeRewrite(const Node& a,
169 : : const Node& b,
170 : : ProofRewriteRule id);
171 : : /**
172 : : * Make trust node: wrap `exp => n` in a trust node with this generator, and
173 : : * have it store the proof `pf` too.
174 : : *
175 : : * @param n The implication
176 : : * @param exp A conjunction of literals that imply it
177 : : * @param pf The proof of exp => n,
178 : : * @return The trust node corresponding to the fact that this generator has
179 : : * a proof of exp => n.
180 : : */
181 : : TrustNode mkTrustedPropagation(Node n,
182 : : Node exp,
183 : : std::shared_ptr<ProofNode> pf);
184 : : /**
185 : : * Make trust node: `a = b` as a Rewrite trust node
186 : : *
187 : : * @param a the original
188 : : * @param b what is rewrites to
189 : : * @param pf The proof of a = b,
190 : : * @return The trust node corresponding to the fact that this generator has
191 : : * a proof of a = b
192 : : */
193 : : TrustNode mkTrustedRewrite(Node a, Node b, std::shared_ptr<ProofNode> pf);
194 : : /**
195 : : * Make trust node from a single step proof. This is a convenience function
196 : : * that avoids the need to explictly construct ProofNode by the caller.
197 : : *
198 : : * @param a the original
199 : : * @param b what is rewrites to
200 : : * @param id The rule of the proof concluding a=b
201 : : * @param args The arguments to the proof concluding a=b,
202 : : * @return The trust node corresponding to the fact that this generator has
203 : : * a proof of a=b.
204 : : */
205 : : TrustNode mkTrustedRewrite(Node a,
206 : : Node b,
207 : : ProofRule id,
208 : : const std::vector<Node>& args);
209 : : //--------------------------------------- common proofs
210 : : /**
211 : : * This returns the trust node corresponding to the splitting lemma
212 : : * (or f (not f)) and this generator. The method registers its proof in the
213 : : * map maintained by this class.
214 : : */
215 : : TrustNode mkTrustNodeSplit(Node f);
216 : : //--------------------------------------- end common proofs
217 : : /** identify */
218 : : std::string identify() const override;
219 : :
220 : : protected:
221 : : /** Set that pf is the proof for conflict conf */
222 : : void setProofForConflict(Node conf, std::shared_ptr<ProofNode> pf);
223 : : /** Set that pf is the proof for lemma lem */
224 : : void setProofForLemma(Node lem, std::shared_ptr<ProofNode> pf);
225 : : /** Set that pf is the proof for explained propagation */
226 : : void setProofForPropExp(TNode lit, Node exp, std::shared_ptr<ProofNode> pf);
227 : : /** Name identifier */
228 : : std::string d_name;
229 : : /** A dummy context used by this class if none is provided */
230 : : context::Context d_context;
231 : : /**
232 : : * A user-context-dependent map from lemmas and conflicts to proofs provided
233 : : * by calls to setProofForConflict and setProofForLemma above.
234 : : */
235 : : NodeProofNodeMap d_proofs;
236 : : };
237 : :
238 : : } // namespace cvc5::internal
239 : :
240 : : #endif /* CVC5__PROOF__PROOF_GENERATOR_H */
|
