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 implementation of the module for proofs for preprocessing in an
11 : : * SMT engine.
12 : : */
13 : :
14 : : #include "smt/preprocess_proof_generator.h"
15 : :
16 : : #include <sstream>
17 : :
18 : : #include "options/proof_options.h"
19 : : #include "proof/method_id.h"
20 : : #include "proof/proof.h"
21 : : #include "proof/proof_checker.h"
22 : : #include "proof/proof_node.h"
23 : : #include "proof/proof_node_manager.h"
24 : : #include "smt/env.h"
25 : : #include "theory/quantifiers/extended_rewrite.h"
26 : :
27 : : namespace cvc5::internal {
28 : : namespace smt {
29 : :
30 : 30357 : PreprocessProofGenerator::PreprocessProofGenerator(Env& env,
31 : : context::Context* c,
32 : 30357 : std::string name)
33 : : : EnvObj(env),
34 [ - + ]: 30357 : d_ctx(c ? c : &d_context),
35 : 30357 : d_src(d_ctx),
36 : 30357 : d_inputPf(env, c, "InputProof"),
37 : 30357 : d_trustPf(env, c, "PreprocessTrustProof"),
38 : 60714 : d_name(name)
39 : : {
40 : 30357 : }
41 : :
42 : 104079 : void PreprocessProofGenerator::notifyInput(Node n)
43 : : {
44 : 104079 : notifyNewAssert(n, &d_inputPf);
45 : 104079 : }
46 : :
47 : 420575 : void PreprocessProofGenerator::notifyNewAssert(Node n,
48 : : ProofGenerator* pg,
49 : : TrustId id)
50 : : {
51 [ + + ][ + + ]: 420575 : if (n.isConst() && n.getConst<bool>())
[ + + ]
52 : : {
53 : : // ignore true assertions
54 : 17602 : return;
55 : : }
56 [ + - ]: 805946 : Trace("smt-proof-pp-debug")
57 [ - - ]: 402973 : << "PreprocessProofGenerator::notifyNewAssert: " << identify() << " " << n
58 : 402973 : << " from " << (pg == nullptr ? "null" : pg->identify()) << std::endl;
59 [ + + ]: 402973 : if (d_src.find(n) == d_src.end())
60 : : {
61 : : // if no proof generator provided for (non-true) assertion
62 [ + + ]: 384420 : if (pg == nullptr)
63 : : {
64 [ - + ][ - + ]: 3224 : Assert(id != TrustId::UNKNOWN_PREPROCESS_LEMMA);
[ - - ]
65 : : // if no proof generator provided, use a trust step
66 : 3224 : d_trustPf.addTrustedStep(n, id, {}, {});
67 : 3224 : pg = &d_trustPf;
68 : : }
69 : 384420 : d_src[n] = TrustNode::mkTrustLemma(n, pg);
70 : : }
71 : : else
72 : : {
73 [ + - ]: 18553 : Trace("smt-proof-pp-debug") << "...already proven" << std::endl;
74 : : }
75 : : }
76 : :
77 : 128665 : void PreprocessProofGenerator::notifyNewTrustedAssert(TrustNode tn, TrustId id)
78 : : {
79 : 128665 : notifyNewAssert(tn.getProven(), tn.getGenerator(), id);
80 : 128665 : }
81 : :
82 : 206196 : void PreprocessProofGenerator::notifyPreprocessed(Node n,
83 : : Node np,
84 : : ProofGenerator* pg,
85 : : TrustId id)
86 : : {
87 : : // only do anything if indeed it rewrote
88 [ - + ]: 206196 : if (n == np)
89 : : {
90 : 0 : return;
91 : : }
92 : : // call the trusted version
93 : 206196 : notifyTrustedPreprocessed(TrustNode::mkTrustRewrite(n, np, pg), id);
94 : : }
95 : :
96 : 287525 : void PreprocessProofGenerator::notifyTrustedPreprocessed(TrustNode tnp,
97 : : TrustId id)
98 : : {
99 [ - + ]: 287525 : if (tnp.isNull())
100 : : {
101 : : // no rewrite, nothing to do
102 : 0 : return;
103 : : }
104 [ - + ][ - + ]: 287525 : Assert(tnp.getKind() == TrustNodeKind::REWRITE);
[ - - ]
105 : 287525 : Node np = tnp.getNode();
106 [ + - ]: 575050 : Trace("smt-proof-pp-debug")
107 : 287525 : << "PreprocessProofGenerator::notifyPreprocessed: " << tnp << std::endl;
108 [ + + ]: 287525 : if (d_src.find(np) == d_src.end())
109 : : {
110 [ + + ]: 234164 : if (tnp.getGenerator() == nullptr)
111 : : {
112 : : // if no proof generator provided, use a trust step
113 : 8484 : d_trustPf.addTrustedStep(tnp.getProven(), id, {}, {});
114 : 8484 : tnp = TrustNode::mkReplaceGenTrustNode(tnp, &d_trustPf);
115 : : }
116 : 234164 : d_src[np] = tnp;
117 : : }
118 : : else
119 : : {
120 [ + - ]: 53361 : Trace("smt-proof-pp-debug") << "...already proven" << std::endl;
121 : : }
122 : 287525 : }
123 : :
124 : 190231 : std::shared_ptr<ProofNode> PreprocessProofGenerator::getProofFor(Node f)
125 : : {
126 [ + - ]: 380462 : Trace("smt-pppg") << "PreprocessProofGenerator::getProofFor: (" << d_name
127 : 190231 : << ") input " << f << std::endl;
128 : 190231 : NodeTrustNodeMap::iterator it = d_src.find(f);
129 [ + + ]: 190231 : if (it == d_src.end())
130 : : {
131 [ + - ][ - + ]: 136498 : Trace("smt-pppg") << "...no proof for " << identify() << " " << f
[ - - ]
132 : 68249 : << std::endl;
133 : : // could be an assumption, return nullptr
134 : 68249 : return nullptr;
135 : : }
136 : : // make CDProof to construct the proof below
137 : 243964 : CDProof cdp(d_env);
138 : :
139 : 121982 : Node curr = f;
140 : 121982 : std::vector<Node> transChildren;
141 : 121982 : std::unordered_set<Node> processed;
142 : : bool success;
143 : : // we connect the proof of f to its source via the map d_src until we
144 : : // discover that its source is a preprocessing lemma (a lemma stored in d_src)
145 : : // or otherwise it is assumed to be an input assumption.
146 [ + + ]: 173653 : do
147 : : {
148 : 173653 : success = false;
149 [ + - ]: 173653 : if (it != d_src.end())
150 : : {
151 [ - + ][ - + ]: 173653 : Assert((*it).second.getNode() == curr);
[ - - ]
152 : : // get the proven node
153 : 173653 : Node proven = (*it).second.getProven();
154 [ - + ][ - + ]: 173653 : Assert(!proven.isNull());
[ - - ]
155 [ + - ]: 173653 : Trace("smt-pppg") << "...process proven " << proven << std::endl;
156 [ - + ]: 173653 : if (processed.find(proven) != processed.end())
157 : : {
158 : 0 : Unhandled() << "Cyclic steps in preprocess proof generator";
159 : : continue;
160 : : }
161 : 173653 : processed.insert(proven);
162 : 173653 : bool proofStepProcessed = false;
163 : :
164 : : // if a generator for the step was provided, it is stored in the proof
165 [ + - ]: 347306 : Trace("smt-pppg-debug")
166 : 173653 : << "...get provided proof " << (*it).second << std::endl;
167 : 173653 : std::shared_ptr<ProofNode> pfr = (*it).second.toProofNode();
168 [ + - ]: 173653 : if (pfr != nullptr)
169 : : {
170 [ + - ]: 347306 : Trace("smt-pppg-debug")
171 : 0 : << "...add provided " << *pfr << " from "
172 [ - + ][ - - ]: 173653 : << (*it).second.getGenerator()->identify() << std::endl;
173 [ - + ][ - + ]: 173653 : Assert(pfr->getResult() == proven);
[ - - ]
174 : 173653 : cdp.addProof(pfr);
175 : 173653 : proofStepProcessed = true;
176 : : }
177 : :
178 [ + - ]: 173653 : Trace("smt-pppg-debug") << "...update" << std::endl;
179 : 173653 : TrustNodeKind tnk = (*it).second.getKind();
180 [ + + ]: 173653 : if (tnk == TrustNodeKind::REWRITE)
181 : : {
182 [ + - ]: 103342 : Trace("smt-pppg-debug")
183 [ - + ][ - - ]: 51671 : << "...rewritten from " << proven[0] << std::endl;
184 [ - + ][ - + ]: 51671 : Assert(proven.getKind() == Kind::EQUAL);
[ - - ]
185 : 51671 : transChildren.push_back(proven);
186 : : // continue with source
187 : 51671 : curr = proven[0];
188 : 51671 : success = true;
189 : : // find the next node
190 [ + - ]: 51671 : Trace("smt-pppg") << "...continue " << curr << std::endl;
191 : 51671 : it = d_src.find(curr);
192 : : }
193 : : else
194 : : {
195 [ + - ]: 121982 : Trace("smt-pppg") << "...lemma" << std::endl;
196 [ - + ][ - + ]: 121982 : Assert(tnk == TrustNodeKind::LEMMA);
[ - - ]
197 : : }
198 : :
199 [ - + ][ - + ]: 173653 : Assert(proofStepProcessed) << "Failed to get proof for preprocess step";
[ - - ]
200 : : // if we had a dynamic failure, e.g. the provided proof generator did
201 : : // not generate a proof
202 [ - + ]: 173653 : if (!proofStepProcessed)
203 : : {
204 : : // if in production, we get an unknown trust step
205 : 0 : TrustId id = (tnk == TrustNodeKind::LEMMA)
206 [ - - ]: 0 : ? TrustId::UNKNOWN_PREPROCESS_LEMMA
207 : : : TrustId::UNKNOWN_PREPROCESS;
208 [ - - ]: 0 : Trace("smt-pppg-debug")
209 : 0 : << "...justify missing step with " << id << std::endl;
210 : : // add trusted step, the rule depends on the kind of trust node
211 : 0 : cdp.addTrustedStep(proven, id, {}, {});
212 : : }
213 [ + - ]: 173653 : }
214 : : } while (success);
215 : :
216 : : // prove ( curr == f ), which is not necessary if they are the same
217 : : // modulo symmetry.
218 [ + + ]: 121982 : if (!CDProof::isSame(f, curr))
219 : : {
220 : 40065 : Node fullRewrite = curr.eqNode(f);
221 [ + + ]: 40065 : if (transChildren.size() >= 2)
222 : : {
223 [ + - ]: 6928 : Trace("smt-pppg") << "...apply trans to get " << fullRewrite << std::endl;
224 : 6928 : std::reverse(transChildren.begin(), transChildren.end());
225 : 6928 : cdp.addStep(fullRewrite, ProofRule::TRANS, transChildren, {});
226 : : }
227 [ + - ]: 40065 : Trace("smt-pppg") << "...eq_resolve to prove" << std::endl;
228 : : // prove f
229 [ + + ][ - - ]: 120195 : cdp.addStep(f, ProofRule::EQ_RESOLVE, {curr, fullRewrite}, {});
230 [ + - ]: 40065 : Trace("smt-pppg") << "...finished" << std::endl;
231 : 40065 : }
232 : :
233 : : // overall, proof is:
234 : : // --------- from proof generator ---------- from proof generator
235 : : // F_1 = F_2 ... F_{n-1} = F_n
236 : : // ---? -------------------------------------------------- TRANS
237 : : // F_1 F_1 = F_n
238 : : // ---------------- EQ_RESOLVE
239 : : // F_n
240 : : // Note F_1 may have been given a proof if it was not an input assumption.
241 : :
242 : 121982 : return cdp.getProofFor(f);
243 : 121982 : }
244 : :
245 : 0 : std::string PreprocessProofGenerator::identify() const { return d_name; }
246 : :
247 : 0 : void PreprocessProofGenerator::checkEagerPedantic(TrustId r)
248 : : {
249 [ - - ]: 0 : if (options().proof.proofCheck == options::ProofCheckMode::EAGER)
250 : : {
251 : : // catch a pedantic failure now, which otherwise would not be
252 : : // triggered since we are doing lazy proof generation
253 : 0 : ProofChecker* pc = d_env.getProofNodeManager()->getChecker();
254 [ - - ]: 0 : if (pc->isPedanticFailure(ProofRule::TRUST, nullptr))
255 : : {
256 : 0 : std::stringstream serr;
257 : 0 : pc->isPedanticFailure(ProofRule::TRUST, &serr);
258 : 0 : Unhandled() << "PreprocessProofGenerator::checkEagerPedantic (" << r
259 : 0 : << "): " << serr.str();
260 : 0 : }
261 : : }
262 : 0 : }
263 : :
264 : : } // namespace smt
265 : : } // namespace cvc5::internal
|
