8f786052bde750ed9f832f242c5721cf96f9f454
1 /********************* */
2 /*! \file proof_checker.cpp
4 ** Top contributors (to current version):
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2020 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.\endverbatim
12 ** \brief Implementation of proof checker
15 #include "expr/proof_checker.h"
17 #include "expr/skolem_manager.h"
18 #include "smt/smt_statistics_registry.h"
20 using namespace CVC4::kind
;
24 Node
ProofRuleChecker::check(PfRule id
,
25 const std::vector
<Node
>& children
,
26 const std::vector
<Node
>& args
)
28 // call instance-specific checkInternal method
29 return checkInternal(id
, children
, args
);
32 Node
ProofRuleChecker::checkChildrenArg(PfRule id
,
33 const std::vector
<Node
>& children
,
36 return check(id
, children
, {arg
});
38 Node
ProofRuleChecker::checkChildren(PfRule id
,
39 const std::vector
<Node
>& children
)
41 return check(id
, children
, {});
43 Node
ProofRuleChecker::checkChild(PfRule id
, Node child
)
45 return check(id
, {child
}, {});
47 Node
ProofRuleChecker::checkArg(PfRule id
, Node arg
)
49 return check(id
, {}, {arg
});
52 Node
ProofRuleChecker::mkAnd(const std::vector
<Node
>& a
)
56 return NodeManager::currentNM()->mkConst(true);
58 else if (a
.size() == 1)
62 return NodeManager::currentNM()->mkNode(AND
, a
);
65 bool ProofRuleChecker::getUInt32(TNode n
, uint32_t& i
)
67 // must be a non-negative integer constant that fits an unsigned int
68 if (n
.isConst() && n
.getType().isInteger()
69 && n
.getConst
<Rational
>().sgn() >= 0
70 && n
.getConst
<Rational
>().getNumerator().fitsUnsignedInt())
72 i
= n
.getConst
<Rational
>().getNumerator().toUnsignedInt();
78 bool ProofRuleChecker::getBool(TNode n
, bool& b
)
80 if (n
.isConst() && n
.getType().isBoolean())
82 b
= n
.getConst
<bool>();
88 ProofCheckerStatistics::ProofCheckerStatistics()
89 : d_ruleChecks("ProofCheckerStatistics::ruleChecks"),
90 d_totalRuleChecks("ProofCheckerStatistics::totalRuleChecks", 0)
92 smtStatisticsRegistry()->registerStat(&d_ruleChecks
);
93 smtStatisticsRegistry()->registerStat(&d_totalRuleChecks
);
96 ProofCheckerStatistics::~ProofCheckerStatistics()
98 smtStatisticsRegistry()->unregisterStat(&d_ruleChecks
);
99 smtStatisticsRegistry()->unregisterStat(&d_totalRuleChecks
);
102 Node
ProofChecker::check(ProofNode
* pn
, Node expected
)
104 return check(pn
->getRule(), pn
->getChildren(), pn
->getArguments(), expected
);
107 Node
ProofChecker::check(
109 const std::vector
<std::shared_ptr
<ProofNode
>>& children
,
110 const std::vector
<Node
>& args
,
113 // optimization: immediately return for ASSUME
114 if (id
== PfRule::ASSUME
)
116 Assert(children
.empty());
117 Assert(args
.size() == 1 && args
[0].getType().isBoolean());
118 Assert(expected
.isNull() || expected
== args
[0]);
122 d_stats
.d_ruleChecks
<< id
;
123 ++d_stats
.d_totalRuleChecks
;
124 Trace("pfcheck") << "ProofChecker::check: " << id
<< std::endl
;
125 std::vector
<Node
> cchildren
;
126 for (const std::shared_ptr
<ProofNode
>& pc
: children
)
128 Assert(pc
!= nullptr);
129 Node cres
= pc
->getResult();
132 Trace("pfcheck") << "ProofChecker::check: failed child" << std::endl
;
134 << "ProofChecker::check: child proof was invalid (null conclusion)"
136 // should not have been able to create such a proof node
139 cchildren
.push_back(cres
);
140 if (Trace
.isOn("pfcheck"))
142 std::stringstream ssc
;
144 Trace("pfcheck") << " child: " << ssc
.str() << " : " << cres
148 Trace("pfcheck") << " args: " << args
<< std::endl
;
149 Trace("pfcheck") << " expected: " << expected
<< std::endl
;
150 std::stringstream out
;
151 // we use trusted (null) checkers here, since we want the proof generation to
152 // proceed without failing here.
153 Node res
= checkInternal(id
, cchildren
, args
, expected
, out
, true);
156 Trace("pfcheck") << "ProofChecker::check: failed" << std::endl
;
157 Unreachable() << "ProofChecker::check: failed, " << out
.str() << std::endl
;
158 // it did not match the given expectation, fail
161 Trace("pfcheck") << "ProofChecker::check: success!" << std::endl
;
165 Node
ProofChecker::checkDebug(PfRule id
,
166 const std::vector
<Node
>& cchildren
,
167 const std::vector
<Node
>& args
,
169 const char* traceTag
)
171 std::stringstream out
;
172 // since we are debugging, we want to treat trusted (null) checkers as
174 Node res
= checkInternal(id
, cchildren
, args
, expected
, out
, false);
175 Trace(traceTag
) << "ProofChecker::checkDebug: " << id
;
178 Trace(traceTag
) << " failed, " << out
.str() << std::endl
;
182 Trace(traceTag
) << " success" << std::endl
;
184 Trace(traceTag
) << "cchildren: " << cchildren
<< std::endl
;
185 Trace(traceTag
) << " args: " << args
<< std::endl
;
189 Node
ProofChecker::checkInternal(PfRule id
,
190 const std::vector
<Node
>& cchildren
,
191 const std::vector
<Node
>& args
,
193 std::stringstream
& out
,
194 bool useTrustedChecker
)
196 std::map
<PfRule
, ProofRuleChecker
*>::iterator it
= d_checker
.find(id
);
197 if (it
== d_checker
.end())
199 // no checker for the rule
200 out
<< "no checker for rule " << id
<< std::endl
;
203 else if (it
->second
== nullptr)
205 if (useTrustedChecker
)
207 Notice() << "ProofChecker::check: trusting PfRule " << id
<< std::endl
;
213 out
<< "trusted checker for rule " << id
<< std::endl
;
217 // check it with the corresponding checker
218 Node res
= it
->second
->check(id
, cchildren
, args
);
219 if (!expected
.isNull())
221 Node expectedw
= expected
;
222 if (res
!= expectedw
)
224 out
<< "result does not match expected value." << std::endl
225 << " PfRule: " << id
<< std::endl
;
226 for (const Node
& c
: cchildren
)
228 out
<< " child: " << c
<< std::endl
;
230 for (const Node
& a
: args
)
232 out
<< " arg: " << a
<< std::endl
;
234 out
<< " result: " << res
<< std::endl
235 << " expected: " << expected
<< std::endl
;
236 // it did not match the given expectation, fail
243 void ProofChecker::registerChecker(PfRule id
, ProofRuleChecker
* psc
)
245 std::map
<PfRule
, ProofRuleChecker
*>::iterator it
= d_checker
.find(id
);
246 if (it
!= d_checker
.end())
248 // checker is already provided
249 Notice() << "ProofChecker::registerChecker: checker already exists for "
256 ProofRuleChecker
* ProofChecker::getCheckerFor(PfRule id
)
258 std::map
<PfRule
, ProofRuleChecker
*>::const_iterator it
= d_checker
.find(id
);
259 if (it
== d_checker
.end())