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 : : * Implementation of lazy proof utility.
11 : : */
12 : :
13 : : #include "proof/lazy_proof.h"
14 : :
15 : : #include "proof/proof_ensure_closed.h"
16 : : #include "proof/proof_node.h"
17 : : #include "proof/proof_node_manager.h"
18 : :
19 : : using namespace cvc5::internal::kind;
20 : :
21 : : namespace cvc5::internal {
22 : :
23 : 1513696 : LazyCDProof::LazyCDProof(Env& env,
24 : : ProofGenerator* dpg,
25 : : context::Context* c,
26 : : const std::string& name,
27 : : bool autoSym,
28 : 1513696 : bool doCache)
29 : : : CDProof(env, c, name, autoSym),
30 : 1513696 : d_gens(c ? c : &d_context),
31 : 1513696 : d_defaultGen(dpg),
32 : 1513696 : d_doCache(doCache),
33 [ + + ][ + + ]: 3027392 : d_allVisited(c ? c : &d_context)
34 : : {
35 : 1513696 : }
36 : :
37 : 1855432 : LazyCDProof::~LazyCDProof() {}
38 : :
39 : 7734054 : std::shared_ptr<ProofNode> LazyCDProof::getProofFor(Node fact)
40 : : {
41 [ + - ]: 7734054 : Trace("lazy-cdproof") << "LazyCDProof::mkLazyProof " << fact << std::endl;
42 : : // make the proof, which should always be non-null, since we construct an
43 : : // assumption in the worst case.
44 : 7734054 : std::shared_ptr<ProofNode> opf = CDProof::getProofFor(fact);
45 [ - + ][ - + ]: 7734054 : Assert(opf != nullptr);
[ - - ]
46 [ + + ]: 7734054 : if (!hasGenerators())
47 : : {
48 [ + - ]: 2854184 : Trace("lazy-cdproof") << "...no generators, finished" << std::endl;
49 : : // optimization: no generators, we are done
50 : 2854184 : return opf;
51 : : }
52 : : // otherwise, we traverse the proof opf and fill in the ASSUME leafs that
53 : : // have generators
54 : 4879870 : std::unordered_set<ProofNode*> visited;
55 : 4879870 : std::vector<ProofNode*> visit;
56 : : ProofNode* cur;
57 : 4879870 : visit.push_back(opf.get());
58 : : bool alreadyVisited;
59 : : do
60 : : {
61 : 19572106 : cur = visit.back();
62 : 19572106 : visit.pop_back();
63 [ + - ]: 19572106 : if (d_doCache)
64 : : {
65 : 19572106 : alreadyVisited = d_allVisited.find(cur) != d_allVisited.end();
66 : : }
67 : : else
68 : : {
69 : 0 : alreadyVisited = visited.find(cur) != visited.end();
70 : : }
71 : :
72 [ + + ]: 19572106 : if (!alreadyVisited)
73 : : {
74 [ + - ]: 14292050 : if (d_doCache)
75 : : {
76 : 14292050 : d_allVisited.insert(cur);
77 : : }
78 : : else
79 : : {
80 : 0 : visited.insert(cur);
81 : : }
82 : 14292050 : Node cfact = cur->getResult();
83 [ + + ]: 14292050 : if (getProof(cfact).get() != cur)
84 : : {
85 : : // We don't own this proof, skip it. This is to ensure that this method
86 : : // is idempotent, since it may be the case that a previous call to
87 : : // getProofFor connected a proof from a proof generator as a child of
88 : : // a ProofNode in the range of the map in CDProof. Thus, this ensures
89 : : // we don't touch such proofs.
90 [ + - ]: 181595 : Trace("lazy-cdproof") << "...skip unowned proof" << std::endl;
91 : : }
92 [ + + ]: 14110455 : else if (cur->getRule() == ProofRule::ASSUME)
93 : : {
94 : 6234846 : bool isSym = false;
95 : 6234846 : ProofGenerator* pg = getGeneratorFor(cfact, isSym);
96 [ + + ]: 6234846 : if (pg != nullptr)
97 : : {
98 [ + - ]: 9211626 : Trace("lazy-cdproof")
99 [ - + ][ - - ]: 4605813 : << "LazyCDProof: Call generator " << pg->identify()
100 : 4605813 : << " for assumption " << cfact << std::endl;
101 [ + + ][ + + ]: 4605813 : Node cfactGen = isSym ? CDProof::getSymmFact(cfact) : cfact;
[ - - ]
102 [ - + ][ - + ]: 4605813 : Assert(!cfactGen.isNull());
[ - - ]
103 : : // Do not use the addProofTo interface, instead use the update node
104 : : // interface, since this ensures that we don't take ownership for
105 : : // the current proof. Instead, it is only linked, and ignored on
106 : : // future calls to getProofFor due to the check above.
107 : 4605813 : std::shared_ptr<ProofNode> pgc = pg->getProofFor(cfactGen);
108 : : // If the proof was null, then the update is not performed. This is
109 : : // not considered an error, since this behavior is equivalent to
110 : : // if pg had provided the proof (ASSUME cfactGen). Ensuring the
111 : : // proper behavior wrt closed proofs should be done outside this
112 : : // method.
113 [ + - ]: 4605813 : if (pgc != nullptr)
114 : : {
115 [ + - ]: 9211626 : Trace("lazy-cdproof-gen")
116 : 4605813 : << "LazyCDProof: stored proof: " << *pgc.get() << std::endl;
117 : :
118 [ + + ]: 4605813 : if (isSym)
119 : : {
120 [ + + ]: 85086 : if (pgc->getRule() == ProofRule::SYMM)
121 : : {
122 : 9 : getManager()->updateNode(cur, pgc->getChildren()[0].get());
123 : : }
124 : : else
125 : : {
126 : 170154 : getManager()->updateNode(cur, ProofRule::SYMM, {pgc}, {});
127 : : }
128 : : }
129 : : else
130 : : {
131 : 4520727 : getManager()->updateNode(cur, pgc.get());
132 : : }
133 [ + - ]: 9211626 : Trace("lazy-cdproof") << "LazyCDProof: Successfully added fact for "
134 : 4605813 : << cfactGen << std::endl;
135 : : }
136 : 4605813 : }
137 : : else
138 : : {
139 [ + - ][ - + ]: 3258066 : Trace("lazy-cdproof") << "LazyCDProof: " << identify()
[ - - ]
140 : 1629033 : << " : No generator for " << cfact << std::endl;
141 : : }
142 : : // Notice that we do not traverse the proofs that have been generated
143 : : // lazily by the proof generators here. In other words, we assume that
144 : : // the proofs from provided proof generators are final and need
145 : : // no further modification by this class.
146 : : }
147 : : else
148 : : {
149 : 7875609 : const std::vector<std::shared_ptr<ProofNode>>& cc = cur->getChildren();
150 [ + + ]: 22567845 : for (const std::shared_ptr<ProofNode>& cp : cc)
151 : : {
152 : 14692236 : visit.push_back(cp.get());
153 : : }
154 : : }
155 : 14292050 : }
156 [ + + ]: 19572106 : } while (!visit.empty());
157 : : // we have now updated the ASSUME leafs of opf, return it
158 [ + - ]: 4879870 : Trace("lazy-cdproof") << "...finished" << std::endl;
159 [ - + ][ - + ]: 4879870 : Assert(opf->getResult() == fact);
[ - - ]
160 : 4879870 : return opf;
161 : 4879870 : }
162 : :
163 : 4540353 : void LazyCDProof::addLazyStep(Node expected,
164 : : ProofGenerator* pg,
165 : : TrustId idNull,
166 : : bool isClosed,
167 : : const char* ctx,
168 : : bool forceOverwrite)
169 : : {
170 [ + + ]: 4540353 : if (pg == nullptr)
171 : : {
172 : : // null generator, should have given a proof rule
173 [ - + ]: 108752 : if (idNull == TrustId::NONE)
174 : : {
175 : 0 : Unreachable() << "LazyCDProof::addLazyStep: " << identify()
176 : 0 : << ": failed to provide proof generator for " << expected;
177 : : return;
178 : : }
179 [ + - ]: 217504 : Trace("lazy-cdproof") << "LazyCDProof::addLazyStep: " << expected
180 : 108752 : << " set (trusted) step " << idNull << "\n";
181 : 108752 : Node tid = mkTrustId(nodeManager(), idNull);
182 [ + + ][ - - ]: 326256 : addStep(expected, ProofRule::TRUST, {}, {tid, expected});
183 : 108752 : return;
184 : 108752 : }
185 [ + - ]: 8863202 : Trace("lazy-cdproof") << "LazyCDProof::addLazyStep: " << expected
186 [ - + ][ - - ]: 4431601 : << " set to generator " << pg->identify() << "\n";
187 [ + - ]: 4431601 : if (!forceOverwrite)
188 : : {
189 : 4431601 : NodeProofGeneratorMap::const_iterator it = d_gens.find(expected);
190 [ + + ]: 4431601 : if (it != d_gens.end())
191 : : {
192 : : // don't overwrite something that is already there
193 : 1117702 : return;
194 : : }
195 : : }
196 : : // just store now
197 : 3313899 : d_gens.insert(expected, pg);
198 : : // debug checking
199 [ + + ]: 3313899 : if (isClosed)
200 : : {
201 [ + - ]: 745744 : Trace("lazy-cdproof-debug") << "Checking closed..." << std::endl;
202 : 745744 : pfgEnsureClosed(options(), expected, pg, "lazy-cdproof-debug", ctx);
203 : : }
204 : : }
205 : :
206 : 6234846 : ProofGenerator* LazyCDProof::getGeneratorFor(Node fact, bool& isSym)
207 : : {
208 : 6234846 : isSym = false;
209 : 6234846 : NodeProofGeneratorMap::const_iterator it = d_gens.find(fact);
210 [ + + ]: 6234846 : if (it != d_gens.end())
211 : : {
212 : 667432 : return (*it).second;
213 : : }
214 [ + + ]: 5567414 : if (d_autoSymm)
215 : : {
216 : 4641330 : Node factSym = CDProof::getSymmFact(fact);
217 : : // could be symmetry
218 [ + + ]: 4641330 : if (factSym.isNull())
219 : : {
220 : : // can't be symmetry, return the default generator
221 : 929838 : return d_defaultGen;
222 : : }
223 : 3711492 : it = d_gens.find(factSym);
224 [ + + ]: 3711492 : if (it != d_gens.end())
225 : : {
226 : 85086 : isSym = true;
227 : 85086 : return (*it).second;
228 : : }
229 [ + + ]: 4641330 : }
230 : : // return the default generator
231 : 4552490 : return d_defaultGen;
232 : : }
233 : :
234 : 7734054 : bool LazyCDProof::hasGenerators() const
235 : : {
236 [ + + ][ + + ]: 7734054 : return !d_gens.empty() || d_defaultGen != nullptr;
237 : : }
238 : :
239 : 250930 : bool LazyCDProof::hasGenerator(Node fact) const
240 : : {
241 [ - + ]: 250930 : if (d_defaultGen != nullptr)
242 : : {
243 : 0 : return true;
244 : : }
245 : 250930 : NodeProofGeneratorMap::const_iterator it = d_gens.find(fact);
246 [ + + ]: 250930 : if (it != d_gens.end())
247 : : {
248 : 94 : return true;
249 : : }
250 : : // maybe there is a symmetric fact?
251 : 250836 : Node factSym = CDProof::getSymmFact(fact);
252 [ + + ]: 250836 : if (!factSym.isNull())
253 : : {
254 : 49630 : it = d_gens.find(factSym);
255 : : }
256 : 250836 : return it != d_gens.end();
257 : 250836 : }
258 : :
259 : : } // namespace cvc5::internal
|
