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 proof checker.
11 : : */
12 : :
13 : : #include "proof/proof_checker.h"
14 : :
15 : : #include "expr/skolem_manager.h"
16 : : #include "proof/proof_node.h"
17 : : #include "util/rational.h"
18 : : #include "util/statistics_registry.h"
19 : :
20 : : using namespace cvc5::internal::kind;
21 : :
22 : : namespace cvc5::internal {
23 : :
24 : 18896 : ProofCheckerStatistics::ProofCheckerStatistics(StatisticsRegistry& sr)
25 : : : d_ruleChecks(
26 : 18896 : sr.registerHistogram<ProofRule>("ProofCheckerStatistics::ruleChecks")),
27 : : d_totalRuleChecks(
28 : 18896 : sr.registerInt("ProofCheckerStatistics::totalRuleChecks"))
29 : : {
30 : 18896 : }
31 : :
32 : 18896 : ProofChecker::ProofChecker(StatisticsRegistry& sr,
33 : : options::ProofCheckMode pcMode,
34 : : uint32_t pclevel,
35 : 18896 : rewriter::RewriteDb* rdb)
36 : 18896 : : d_stats(sr), d_pcMode(pcMode), d_pclevel(pclevel), d_rdb(rdb)
37 : : {
38 : 18896 : }
39 : :
40 : 18895 : void ProofChecker::reset()
41 : : {
42 : 18895 : d_checker.clear();
43 : 18895 : d_plevel.clear();
44 : 18895 : }
45 : :
46 : 21642312 : Node ProofChecker::check(ProofNode* pn, Node expected)
47 : : {
48 : 21642312 : return check(pn->getRule(), pn->getChildren(), pn->getArguments(), expected);
49 : : }
50 : :
51 : 24497924 : Node ProofChecker::check(
52 : : ProofRule id,
53 : : const std::vector<std::shared_ptr<ProofNode>>& children,
54 : : const std::vector<Node>& args,
55 : : Node expected)
56 : : {
57 : : // optimization: immediately return for ASSUME
58 [ + + ]: 24497924 : if (id == ProofRule::ASSUME)
59 : : {
60 [ - + ][ - + ]: 7909170 : Assert(children.empty());
[ - - ]
61 : 7909170 : Assert(args.size() == 1 && args[0].getType().isBoolean());
62 [ + - ][ + - ]: 7909170 : Assert(expected.isNull() || expected == args[0]);
[ - + ][ - + ]
[ - - ]
63 : 7909170 : return expected;
64 : : }
65 : : // record stat
66 : 16588754 : d_stats.d_ruleChecks << id;
67 : 16588754 : ++d_stats.d_totalRuleChecks;
68 [ + - ]: 16588754 : Trace("pfcheck") << "ProofChecker::check: " << id << std::endl;
69 : 16588754 : std::vector<Node> cchildren;
70 [ + + ]: 72475811 : for (const std::shared_ptr<ProofNode>& pc : children)
71 : : {
72 [ - + ][ - + ]: 55887057 : Assert(pc != nullptr);
[ - - ]
73 : 55887057 : Node cres = pc->getResult();
74 [ - + ]: 55887057 : if (cres.isNull())
75 : : {
76 [ - - ]: 0 : Trace("pfcheck") << "ProofChecker::check: failed child" << std::endl;
77 : 0 : Unreachable()
78 : 0 : << "ProofChecker::check: child proof was invalid (null conclusion)"
79 : 0 : << std::endl;
80 : : // should not have been able to create such a proof node
81 : : return Node::null();
82 : : }
83 : 55887057 : cchildren.push_back(cres);
84 [ - + ]: 55887057 : if (TraceIsOn("pfcheck"))
85 : : {
86 : 0 : std::stringstream ssc;
87 : 0 : pc->printDebug(ssc);
88 : 0 : Trace("pfcheck") << " child: " << ssc.str() << " : " << cres
89 : 0 : << std::endl;
90 : 0 : }
91 [ + - ]: 55887057 : }
92 [ + - ]: 16588754 : Trace("pfcheck") << " args: " << args << std::endl;
93 [ + - ]: 16588754 : Trace("pfcheck") << " expected: " << expected << std::endl;
94 : : // we use trusted (null) checkers here, since we want the proof generation to
95 : : // proceed without failing here. We always enable output since a failure
96 : : // implies that we will exit with the error message below.
97 : 16588754 : Node res = checkInternal(id, cchildren, args, expected, nullptr, true);
98 [ - + ]: 16588754 : if (res.isNull())
99 : : {
100 : 0 : std::stringstream out;
101 : 0 : checkInternal(id, cchildren, args, expected, &out, true);
102 [ - - ]: 0 : Trace("pfcheck") << "ProofChecker::check: failed" << std::endl;
103 : 0 : Unreachable() << "ProofChecker::check: failed, " << out.str() << std::endl;
104 : : // it did not match the given expectation, fail
105 : : return Node::null();
106 : 0 : }
107 [ + - ]: 16588754 : Trace("pfcheck") << "ProofChecker::check: success!" << std::endl;
108 : 16588754 : return res;
109 : 16588754 : }
110 : :
111 : 2505373 : Node ProofChecker::checkDebug(ProofRule id,
112 : : const std::vector<Node>& cchildren,
113 : : const std::vector<Node>& args,
114 : : Node expected,
115 : : const char* traceTag)
116 : : {
117 : 2505373 : bool debugTrace = TraceIsOn(traceTag);
118 [ + - ]: 2505373 : if (!debugTrace)
119 : : {
120 : : // run without output stream
121 : 2505373 : return checkInternal(id, cchildren, args, expected, nullptr, false);
122 : : }
123 : 0 : std::stringstream out;
124 : : // Since we are debugging, we want to treat trusted (null) checkers as
125 : : // a failure. We only enable output if the trace is enabled for efficiency.
126 : 0 : Node res = checkInternal(id, cchildren, args, expected, &out, false);
127 [ - - ]: 0 : Trace(traceTag) << "ProofChecker::checkDebug: " << id;
128 [ - - ]: 0 : if (res.isNull())
129 : : {
130 : 0 : Trace(traceTag) << " failed, " << out.str() << std::endl;
131 : : }
132 : : else
133 : : {
134 [ - - ]: 0 : Trace(traceTag) << " success" << std::endl;
135 : : }
136 [ - - ]: 0 : Trace(traceTag) << "cchildren: " << cchildren << std::endl;
137 [ - - ]: 0 : Trace(traceTag) << " args: " << args << std::endl;
138 : 0 : return res;
139 : 0 : }
140 : :
141 : 4244 : void ProofChecker::setProofCheckMode(options::ProofCheckMode pcMode)
142 : : {
143 : 4244 : d_pcMode = pcMode;
144 : 4244 : }
145 : :
146 : 19094127 : Node ProofChecker::checkInternal(ProofRule id,
147 : : const std::vector<Node>& cchildren,
148 : : const std::vector<Node>& args,
149 : : Node expected,
150 : : std::stringstream* out,
151 : : bool useTrustedChecker)
152 : : {
153 : 19094127 : std::map<ProofRule, ProofRuleChecker*>::iterator it = d_checker.find(id);
154 [ - + ]: 19094127 : if (it == d_checker.end())
155 : : {
156 : : // no checker for the rule
157 [ - - ]: 0 : if (out != nullptr)
158 : : {
159 : 0 : (*out) << "no checker for rule " << id << std::endl;
160 : : }
161 : 0 : return Node::null();
162 : : }
163 [ - + ]: 19094127 : else if (it->second == nullptr)
164 : : {
165 [ - - ]: 0 : if (useTrustedChecker)
166 : : {
167 [ - - ]: 0 : if (out != nullptr)
168 : : {
169 : 0 : (*out) << "ProofChecker::check: trusting ProofRule " << id << std::endl;
170 : : }
171 : : // trusted checker
172 : 0 : return expected;
173 : : }
174 : : else
175 : : {
176 [ - - ]: 0 : if (out != nullptr)
177 : : {
178 : 0 : (*out) << "trusted checker for rule " << id << std::endl;
179 : : }
180 : 0 : return Node::null();
181 : : }
182 : : }
183 : : // if we aren't doing checking, trust the expected if it exists
184 [ + + ][ + + ]: 19094127 : if (d_pcMode == options::ProofCheckMode::NONE && !expected.isNull())
[ + + ]
185 : : {
186 : 7186718 : return expected;
187 : : }
188 : : // check it with the corresponding checker
189 : 11907409 : Node res = it->second->check(id, cchildren, args);
190 [ + + ]: 11907409 : if (!expected.isNull())
191 : : {
192 : 6704230 : Node expectedw = expected;
193 [ - + ]: 6704230 : if (res != expectedw)
194 : : {
195 [ - - ]: 0 : if (out != nullptr)
196 : : {
197 : 0 : (*out) << "result does not match expected value." << std::endl
198 : 0 : << " ProofRule: " << id << std::endl;
199 [ - - ]: 0 : for (const Node& c : cchildren)
200 : : {
201 : 0 : (*out) << " child: " << c << std::endl;
202 : : }
203 [ - - ]: 0 : for (const Node& a : args)
204 : : {
205 : 0 : (*out) << " arg: " << a << std::endl;
206 : : }
207 : 0 : (*out) << " result: " << res << std::endl
208 : 0 : << " expected: " << expected << std::endl;
209 : : }
210 : : // it did not match the given expectation, fail
211 : 0 : return Node::null();
212 : : }
213 [ + - ]: 6704230 : }
214 : : // fails if pedantic level is not met
215 [ + + ]: 11907409 : if (d_pcMode == options::ProofCheckMode::EAGER)
216 : : {
217 [ - + ]: 107464 : if (isPedanticFailure(id, nullptr))
218 : : {
219 [ - - ]: 0 : if (out != nullptr)
220 : : {
221 : : // recompute with output
222 : 0 : std::stringstream serr;
223 : 0 : isPedanticFailure(id, &serr);
224 : 0 : (*out) << serr.str() << std::endl;
225 [ - - ]: 0 : if (TraceIsOn("proof-pedantic"))
226 : : {
227 [ - - ]: 0 : Trace("proof-pedantic")
228 : 0 : << "Failed pedantic check for " << id << std::endl;
229 [ - - ]: 0 : Trace("proof-pedantic") << "Expected: " << expected << std::endl;
230 : 0 : (*out) << "Expected: " << expected << std::endl;
231 : : }
232 : 0 : }
233 : 0 : return Node::null();
234 : : }
235 : : }
236 : 11907409 : return res;
237 : 11907409 : }
238 : :
239 : 2928820 : void ProofChecker::registerChecker(ProofRule id, ProofRuleChecker* psc)
240 : : {
241 : 2928820 : std::map<ProofRule, ProofRuleChecker*>::iterator it = d_checker.find(id);
242 [ - + ]: 2928820 : if (it != d_checker.end())
243 : : {
244 : : // checker is already provided
245 [ - - ]: 0 : Trace("pfcheck")
246 : 0 : << "ProofChecker::registerChecker: checker already exists for " << id
247 : 0 : << std::endl;
248 : 0 : return;
249 : : }
250 : 2928820 : d_checker[id] = psc;
251 : : }
252 : :
253 : 226762 : void ProofChecker::registerTrustedChecker(ProofRule id,
254 : : ProofRuleChecker* psc,
255 : : uint32_t plevel)
256 : : {
257 [ - + ][ - + ]: 226762 : AlwaysAssert(plevel <= 10) << "ProofChecker::registerTrustedChecker: "
[ - - ]
258 : 0 : "pedantic level must be 0-10, got "
259 : 0 : << plevel << " for " << id;
260 : 226762 : registerChecker(id, psc);
261 : : // overwrites if already there
262 [ - + ]: 226762 : if (d_plevel.find(id) != d_plevel.end())
263 : : {
264 [ - - ]: 0 : Trace("proof-pedantic")
265 : : << "ProofChecker::registerTrustedRule: already provided pedantic "
266 : 0 : "level for "
267 : 0 : << id << std::endl;
268 : : }
269 : 226762 : d_plevel[id] = plevel;
270 : 226762 : }
271 : :
272 : 0 : ProofRuleChecker* ProofChecker::getCheckerFor(ProofRule id)
273 : : {
274 : : std::map<ProofRule, ProofRuleChecker*>::const_iterator it =
275 : 0 : d_checker.find(id);
276 [ - - ]: 0 : if (it == d_checker.end())
277 : : {
278 : 0 : return nullptr;
279 : : }
280 : 0 : return it->second;
281 : : }
282 : :
283 : 18896 : rewriter::RewriteDb* ProofChecker::getRewriteDatabase() { return d_rdb; }
284 : :
285 : 2225964 : uint32_t ProofChecker::getPedanticLevel(ProofRule id) const
286 : : {
287 : 2225964 : std::map<ProofRule, uint32_t>::const_iterator itp = d_plevel.find(id);
288 [ + + ]: 2225964 : if (itp != d_plevel.end())
289 : : {
290 : 1910 : return itp->second;
291 : : }
292 : 2224054 : return 0;
293 : : }
294 : :
295 : 2329980 : bool ProofChecker::isPedanticFailure(ProofRule id, std::ostream* out) const
296 : : {
297 [ + - ]: 2329980 : if (d_pclevel == 0)
298 : : {
299 : 2329980 : return false;
300 : : }
301 : 0 : std::map<ProofRule, uint32_t>::const_iterator itp = d_plevel.find(id);
302 [ - - ]: 0 : if (itp != d_plevel.end())
303 : : {
304 [ - - ]: 0 : if (itp->second <= d_pclevel)
305 : : {
306 [ - - ]: 0 : if (out != nullptr)
307 : : {
308 : 0 : (*out) << "pedantic level for " << id << " not met (rule level is "
309 : 0 : << itp->second << " which is at or below the pedantic level "
310 : 0 : << d_pclevel << ")";
311 : 0 : bool pedanticTraceEnabled = TraceIsOn("proof-pedantic");
312 [ - - ]: 0 : if (!pedanticTraceEnabled)
313 : : {
314 : 0 : (*out) << ", use -t proof-pedantic for details";
315 : : }
316 : : }
317 : 0 : return true;
318 : : }
319 : : }
320 : 0 : return false;
321 : : }
322 : :
323 : : } // namespace cvc5::internal
|
