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