1 /******************************************************************************
2 * Top contributors (to current version):
3 * Andrew Reynolds, Aina Niemetz
5 * This file is part of the cvc5 project.
7 * Copyright (c) 2009-2021 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 * ****************************************************************************
13 * Implementation of proof checker.
16 #include "proof/proof_checker.h"
18 #include "expr/skolem_manager.h"
19 #include "options/proof_options.h"
20 #include "proof/proof_node.h"
21 #include "smt/smt_statistics_registry.h"
22 #include "util/rational.h"
24 using namespace cvc5::kind
;
28 Node
ProofRuleChecker::check(PfRule id
,
29 const std::vector
<Node
>& children
,
30 const std::vector
<Node
>& args
)
32 // call instance-specific checkInternal method
33 return checkInternal(id
, children
, args
);
36 bool ProofRuleChecker::getUInt32(TNode n
, uint32_t& i
)
38 // must be a non-negative integer constant that fits an unsigned int
39 if (n
.isConst() && n
.getType().isInteger()
40 && n
.getConst
<Rational
>().sgn() >= 0
41 && n
.getConst
<Rational
>().getNumerator().fitsUnsignedInt())
43 i
= n
.getConst
<Rational
>().getNumerator().toUnsignedInt();
49 bool ProofRuleChecker::getBool(TNode n
, bool& b
)
51 if (n
.isConst() && n
.getType().isBoolean())
53 b
= n
.getConst
<bool>();
59 bool ProofRuleChecker::getKind(TNode n
, Kind
& k
)
66 k
= static_cast<Kind
>(i
);
70 Node
ProofRuleChecker::mkKindNode(Kind k
)
72 if (k
== UNDEFINED_KIND
)
74 // UNDEFINED_KIND is negative, hence return null to avoid cast
77 return NodeManager::currentNM()->mkConst(Rational(static_cast<uint32_t>(k
)));
80 ProofCheckerStatistics::ProofCheckerStatistics()
81 : d_ruleChecks(smtStatisticsRegistry().registerHistogram
<PfRule
>(
82 "ProofCheckerStatistics::ruleChecks")),
83 d_totalRuleChecks(smtStatisticsRegistry().registerInt(
84 "ProofCheckerStatistics::totalRuleChecks"))
88 ProofChecker::ProofChecker(uint32_t pclevel
, rewriter::RewriteDb
* rdb
)
89 : d_pclevel(pclevel
), d_rdb(rdb
)
93 Node
ProofChecker::check(ProofNode
* pn
, Node expected
)
95 return check(pn
->getRule(), pn
->getChildren(), pn
->getArguments(), expected
);
98 Node
ProofChecker::check(
100 const std::vector
<std::shared_ptr
<ProofNode
>>& children
,
101 const std::vector
<Node
>& args
,
104 // optimization: immediately return for ASSUME
105 if (id
== PfRule::ASSUME
)
107 Assert(children
.empty());
108 Assert(args
.size() == 1 && args
[0].getType().isBoolean());
109 Assert(expected
.isNull() || expected
== args
[0]);
113 d_stats
.d_ruleChecks
<< id
;
114 ++d_stats
.d_totalRuleChecks
;
115 Trace("pfcheck") << "ProofChecker::check: " << id
<< std::endl
;
116 std::vector
<Node
> cchildren
;
117 for (const std::shared_ptr
<ProofNode
>& pc
: children
)
119 Assert(pc
!= nullptr);
120 Node cres
= pc
->getResult();
123 Trace("pfcheck") << "ProofChecker::check: failed child" << std::endl
;
125 << "ProofChecker::check: child proof was invalid (null conclusion)"
127 // should not have been able to create such a proof node
130 cchildren
.push_back(cres
);
131 if (Trace
.isOn("pfcheck"))
133 std::stringstream ssc
;
135 Trace("pfcheck") << " child: " << ssc
.str() << " : " << cres
139 Trace("pfcheck") << " args: " << args
<< std::endl
;
140 Trace("pfcheck") << " expected: " << expected
<< std::endl
;
141 std::stringstream out
;
142 // we use trusted (null) checkers here, since we want the proof generation to
143 // proceed without failing here. We always enable output since a failure
144 // implies that we will exit with the error message below.
145 Node res
= checkInternal(id
, cchildren
, args
, expected
, out
, true, true);
148 Trace("pfcheck") << "ProofChecker::check: failed" << std::endl
;
149 Unreachable() << "ProofChecker::check: failed, " << out
.str() << std::endl
;
150 // it did not match the given expectation, fail
153 Trace("pfcheck") << "ProofChecker::check: success!" << std::endl
;
157 Node
ProofChecker::checkDebug(PfRule id
,
158 const std::vector
<Node
>& cchildren
,
159 const std::vector
<Node
>& args
,
161 const char* traceTag
)
163 std::stringstream out
;
164 bool traceEnabled
= Trace
.isOn(traceTag
);
165 // Since we are debugging, we want to treat trusted (null) checkers as
166 // a failure. We only enable output if the trace is enabled for efficiency.
168 checkInternal(id
, cchildren
, args
, expected
, out
, false, traceEnabled
);
171 Trace(traceTag
) << "ProofChecker::checkDebug: " << id
;
174 Trace(traceTag
) << " failed, " << out
.str() << std::endl
;
178 Trace(traceTag
) << " success" << std::endl
;
180 Trace(traceTag
) << "cchildren: " << cchildren
<< std::endl
;
181 Trace(traceTag
) << " args: " << args
<< std::endl
;
186 Node
ProofChecker::checkInternal(PfRule id
,
187 const std::vector
<Node
>& cchildren
,
188 const std::vector
<Node
>& args
,
190 std::stringstream
& out
,
191 bool useTrustedChecker
,
194 std::map
<PfRule
, ProofRuleChecker
*>::iterator it
= d_checker
.find(id
);
195 if (it
== d_checker
.end())
197 // no checker for the rule
200 out
<< "no checker for rule " << id
<< std::endl
;
204 else if (it
->second
== nullptr)
206 if (useTrustedChecker
)
208 Notice() << "ProofChecker::check: trusting PfRule " << id
<< std::endl
;
216 out
<< "trusted checker for rule " << id
<< std::endl
;
221 // check it with the corresponding checker
222 Node res
= it
->second
->check(id
, cchildren
, args
);
223 if (!expected
.isNull())
225 Node expectedw
= expected
;
226 if (res
!= expectedw
)
230 out
<< "result does not match expected value." << std::endl
231 << " PfRule: " << id
<< std::endl
;
232 for (const Node
& c
: cchildren
)
234 out
<< " child: " << c
<< std::endl
;
236 for (const Node
& a
: args
)
238 out
<< " arg: " << a
<< std::endl
;
240 out
<< " result: " << res
<< std::endl
241 << " expected: " << expected
<< std::endl
;
243 // it did not match the given expectation, fail
247 // fails if pedantic level is not met
248 if (options::proofEagerChecking())
250 std::stringstream serr
;
251 if (isPedanticFailure(id
, serr
, enableOutput
))
255 out
<< serr
.str() << std::endl
;
256 if (Trace
.isOn("proof-pedantic"))
258 Trace("proof-pedantic")
259 << "Failed pedantic check for " << id
<< std::endl
;
260 Trace("proof-pedantic") << "Expected: " << expected
<< std::endl
;
261 out
<< "Expected: " << expected
<< std::endl
;
270 void ProofChecker::registerChecker(PfRule id
, ProofRuleChecker
* psc
)
272 std::map
<PfRule
, ProofRuleChecker
*>::iterator it
= d_checker
.find(id
);
273 if (it
!= d_checker
.end())
275 // checker is already provided
276 Notice() << "ProofChecker::registerChecker: checker already exists for "
283 void ProofChecker::registerTrustedChecker(PfRule id
,
284 ProofRuleChecker
* psc
,
287 AlwaysAssert(plevel
<= 10) << "ProofChecker::registerTrustedChecker: "
288 "pedantic level must be 0-10, got "
289 << plevel
<< " for " << id
;
290 registerChecker(id
, psc
);
291 // overwrites if already there
292 if (d_plevel
.find(id
) != d_plevel
.end())
294 Notice() << "ProofChecker::registerTrustedRule: already provided pedantic "
298 d_plevel
[id
] = plevel
;
301 ProofRuleChecker
* ProofChecker::getCheckerFor(PfRule id
)
303 std::map
<PfRule
, ProofRuleChecker
*>::const_iterator it
= d_checker
.find(id
);
304 if (it
== d_checker
.end())
311 rewriter::RewriteDb
* ProofChecker::getRewriteDatabase() { return d_rdb
; }
313 uint32_t ProofChecker::getPedanticLevel(PfRule id
) const
315 std::map
<PfRule
, uint32_t>::const_iterator itp
= d_plevel
.find(id
);
316 if (itp
!= d_plevel
.end())
323 bool ProofChecker::isPedanticFailure(PfRule id
,
325 bool enableOutput
) const
331 std::map
<PfRule
, uint32_t>::const_iterator itp
= d_plevel
.find(id
);
332 if (itp
!= d_plevel
.end())
334 if (itp
->second
<= d_pclevel
)
338 out
<< "pedantic level for " << id
<< " not met (rule level is "
339 << itp
->second
<< " which is at or below the pedantic level "
341 bool pedanticTraceEnabled
= Trace
.isOn("proof-pedantic");
342 if (!pedanticTraceEnabled
)
344 out
<< ", use -t proof-pedantic for details";