#include "expr/proof_checker.h"
+#include "expr/proof_skolem_cache.h"
+#include "smt/smt_statistics_registry.h"
+
+using namespace CVC4::kind;
+
namespace CVC4 {
+Node ProofRuleChecker::check(PfRule id,
+ const std::vector<Node>& children,
+ const std::vector<Node>& args)
+{
+ // convert to witness form
+ std::vector<Node> childrenw = children;
+ std::vector<Node> argsw = args;
+ ProofSkolemCache::convertToWitnessFormVec(childrenw);
+ ProofSkolemCache::convertToWitnessFormVec(argsw);
+ Node res = checkInternal(id, childrenw, argsw);
+ // res is in terms of witness form, convert back to Skolem form
+ return ProofSkolemCache::getSkolemForm(res);
+}
+
+Node ProofRuleChecker::checkChildrenArg(PfRule id,
+ const std::vector<Node>& children,
+ Node arg)
+{
+ return check(id, children, {arg});
+}
+Node ProofRuleChecker::checkChildren(PfRule id,
+ const std::vector<Node>& children)
+{
+ return check(id, children, {});
+}
+Node ProofRuleChecker::checkChild(PfRule id, Node child)
+{
+ return check(id, {child}, {});
+}
+Node ProofRuleChecker::checkArg(PfRule id, Node arg)
+{
+ return check(id, {}, {arg});
+}
+
+Node ProofRuleChecker::mkAnd(const std::vector<Node>& a)
+{
+ if (a.empty())
+ {
+ return NodeManager::currentNM()->mkConst(true);
+ }
+ else if (a.size() == 1)
+ {
+ return a[0];
+ }
+ return NodeManager::currentNM()->mkNode(AND, a);
+}
+
+bool ProofRuleChecker::getUInt32(TNode n, uint32_t& i)
+{
+ // must be a non-negative integer constant that fits an unsigned int
+ if (n.isConst() && n.getType().isInteger()
+ && n.getConst<Rational>().sgn() >= 0
+ && n.getConst<Rational>().getNumerator().fitsUnsignedInt())
+ {
+ i = n.getConst<Rational>().getNumerator().toUnsignedInt();
+ return true;
+ }
+ return false;
+}
+
+bool ProofRuleChecker::getBool(TNode n, bool& b)
+{
+ if (n.isConst() && n.getType().isBoolean())
+ {
+ b = n.getConst<bool>();
+ return true;
+ }
+ return false;
+}
+
+ProofCheckerStatistics::ProofCheckerStatistics()
+ : d_ruleChecks("ProofCheckerStatistics::ruleChecks")
+{
+ smtStatisticsRegistry()->registerStat(&d_ruleChecks);
+}
+
+ProofCheckerStatistics::~ProofCheckerStatistics()
+{
+ smtStatisticsRegistry()->unregisterStat(&d_ruleChecks);
+}
+
Node ProofChecker::check(ProofNode* pn, Node expected)
{
return check(pn->getRule(), pn->getChildren(), pn->getArguments(), expected);
const std::vector<Node>& args,
Node expected)
{
- std::map<PfRule, ProofRuleChecker*>::iterator it = d_checker.find(id);
- if (it == d_checker.end())
+ // optimization: immediately return for ASSUME
+ if (id == PfRule::ASSUME)
{
- // no checker for the rule
- Trace("pfcheck") << "ProofChecker::check: no checker for rule " << id
- << std::endl;
- return Node::null();
+ Assert(children.empty());
+ Assert(args.size() == 1 && args[0].getType().isBoolean());
+ Assert(expected.isNull() || expected == args[0]);
+ return expected;
}
- // check it with the corresponding checker
+ // record stat
+ d_stats.d_ruleChecks << id;
+ Trace("pfcheck") << "ProofChecker::check: " << id << std::endl;
std::vector<Node> cchildren;
for (const std::shared_ptr<ProofNode>& pc : children)
{
Node cres = pc->getResult();
if (cres.isNull())
{
- Trace("pfcheck")
+ Trace("pfcheck") << "ProofChecker::check: failed child" << std::endl;
+ Unreachable()
<< "ProofChecker::check: child proof was invalid (null conclusion)"
<< std::endl;
// should not have been able to create such a proof node
- Assert(false);
return Node::null();
}
cchildren.push_back(cres);
+ if (Trace.isOn("pfcheck"))
+ {
+ std::stringstream ssc;
+ pc->printDebug(ssc);
+ Trace("pfcheck") << " child: " << ssc.str() << " : " << cres
+ << std::endl;
+ }
}
- Node res = it->second->check(id, cchildren, args);
- if (!expected.isNull() && res != expected)
+ Trace("pfcheck") << " args: " << args << std::endl;
+ Trace("pfcheck") << " expected: " << expected << std::endl;
+ std::stringstream out;
+ // we use trusted (null) checkers here, since we want the proof generation to
+ // proceed without failing here.
+ Node res = checkInternal(id, cchildren, args, expected, out, true);
+ if (res.isNull())
{
- Trace("pfcheck")
- << "ProofChecker::check: result does not match expected value."
- << std::endl;
- Trace("pfcheck") << " result: " << res << std::endl;
- Trace("pfcheck") << " expected: " << expected << std::endl;
+ Trace("pfcheck") << "ProofChecker::check: failed" << std::endl;
+ Unreachable() << "ProofChecker::check: failed, " << out.str() << std::endl;
// it did not match the given expectation, fail
return Node::null();
}
+ Trace("pfcheck") << "ProofChecker::check: success!" << std::endl;
+ return res;
+}
+
+Node ProofChecker::checkDebug(PfRule id,
+ const std::vector<Node>& cchildren,
+ const std::vector<Node>& args,
+ Node expected,
+ const char* traceTag)
+{
+ std::stringstream out;
+ // since we are debugging, we want to treat trusted (null) checkers as
+ // a failure.
+ Node res = checkInternal(id, cchildren, args, expected, out, false);
+ Trace(traceTag) << "ProofChecker::checkDebug: " << id;
+ if (res.isNull())
+ {
+ Trace(traceTag) << " failed, " << out.str() << std::endl;
+ }
+ else
+ {
+ Trace(traceTag) << " success" << std::endl;
+ }
+ return res;
+}
+
+Node ProofChecker::checkInternal(PfRule id,
+ const std::vector<Node>& cchildren,
+ const std::vector<Node>& args,
+ Node expected,
+ std::stringstream& out,
+ bool useTrustedChecker)
+{
+ std::map<PfRule, ProofRuleChecker*>::iterator it = d_checker.find(id);
+ if (it == d_checker.end())
+ {
+ // no checker for the rule
+ out << "no checker for rule " << id << std::endl;
+ return Node::null();
+ }
+ else if (it->second == nullptr)
+ {
+ if (useTrustedChecker)
+ {
+ Notice() << "ProofChecker::check: trusting PfRule " << id << std::endl;
+ // trusted checker
+ return expected;
+ }
+ else
+ {
+ out << "trusted checker for rule " << id << std::endl;
+ return Node::null();
+ }
+ }
+ // check it with the corresponding checker
+ Node res = it->second->check(id, cchildren, args);
+ if (!expected.isNull())
+ {
+ Node expectedw = expected;
+ if (res != expectedw)
+ {
+ out << "result does not match expected value." << std::endl
+ << " PfRule: " << id << std::endl;
+ for (const Node& c : cchildren)
+ {
+ out << " child: " << c << std::endl;
+ }
+ for (const Node& a : args)
+ {
+ out << " arg: " << a << std::endl;
+ }
+ out << " result: " << res << std::endl
+ << " expected: " << expected << std::endl;
+ // it did not match the given expectation, fail
+ return Node::null();
+ }
+ }
return res;
}
#include "expr/node.h"
#include "expr/proof_node.h"
+#include "util/statistics_registry.h"
namespace CVC4 {
+class ProofChecker;
+
/** A virtual base class for checking a proof rule */
class ProofRuleChecker
{
* Return the formula that is proven by a proof node with the given id,
* premises and arguments, or null if such a proof node is not well-formed.
*
+ * Note that the input/output of this method expects to be terms in *Skolem
+ * form*. To facilitate checking, this method converts to/from witness
+ * form, calling the subprocedure checkInternal below.
+ *
+ * @param id The id of the proof node to check
+ * @param children The premises of the proof node to check. These are nodes
+ * corresponding to the conclusion (ProofNode::getResult) of the children
+ * of the proof node we are checking in Skolem form.
+ * @param args The arguments of the proof node to check
+ * @return The conclusion of the proof node, in Skolem form, if successful or
+ * null if such a proof node is malformed.
+ */
+ Node check(PfRule id,
+ const std::vector<Node>& children,
+ const std::vector<Node>& args);
+ /** Single arg version */
+ Node checkChildrenArg(PfRule id, const std::vector<Node>& children, Node arg);
+ /** No arg version */
+ Node checkChildren(PfRule id, const std::vector<Node>& children);
+ /** Single child only version */
+ Node checkChild(PfRule id, Node child);
+ /** Single argument only version */
+ Node checkArg(PfRule id, Node arg);
+
+ /** Make AND-kinded node with children a */
+ static Node mkAnd(const std::vector<Node>& a);
+ /** get an index from a node, return false if we fail */
+ static bool getUInt32(TNode n, uint32_t& i);
+ /** get a Boolean from a node, return false if we fail */
+ static bool getBool(TNode n, bool& b);
+
+ /** Register all rules owned by this rule checker into pc. */
+ virtual void registerTo(ProofChecker* pc) {}
+
+ protected:
+ /**
+ * This checks a single step in a proof. It is identical to check above
+ * except that children and args have been converted to "witness form"
+ * (see ProofSkolemCache). Likewise, its output should be in witness form.
+ *
* @param id The id of the proof node to check
* @param children The premises of the proof node to check. These are nodes
* corresponding to the conclusion (ProofNode::getResult) of the children
- * of the proof node we are checking.
+ * of the proof node we are checking, in witness form.
* @param args The arguments of the proof node to check
- * @return The conclusion of the proof node if successful or null if such a
- * proof node is malformed.
+ * @return The conclusion of the proof node, in witness form, if successful or
+ * null if such a proof node is malformed.
*/
- virtual Node check(PfRule id,
- const std::vector<Node>& children,
- const std::vector<Node>& args) = 0;
+ virtual Node checkInternal(PfRule id,
+ const std::vector<Node>& children,
+ const std::vector<Node>& args) = 0;
+};
+
+/** Statistics class */
+class ProofCheckerStatistics
+{
+ public:
+ ProofCheckerStatistics();
+ ~ProofCheckerStatistics();
+ /** Counts the number of checks for each kind of proof rule */
+ HistogramStat<PfRule> d_ruleChecks;
};
/** A class for checking proofs */
const std::vector<std::shared_ptr<ProofNode>>& children,
const std::vector<Node>& args,
Node expected = Node::null());
+ /**
+ * Same as above, without conclusions instead of proof node children. This
+ * is used for debugging. In particular, this function does not throw an
+ * assertion failure when a proof step is malformed and can be used without
+ * constructing proof nodes.
+ *
+ * @param id The id of the proof node to check
+ * @param children The conclusions of the children of the proof node to check
+ * @param args The arguments of the proof node to check
+ * @param expected The (optional) formula that is the expected conclusion of
+ * the proof node.
+ * @param traceTag The trace tag to print debug information to
+ * @return The conclusion of the proof node if successful or null if the
+ * proof is malformed, or if no checker is available for id.
+ */
+ Node checkDebug(PfRule id,
+ const std::vector<Node>& cchildren,
+ const std::vector<Node>& args,
+ Node expected,
+ const char* traceTag);
/** Indicate that psc is the checker for proof rule id */
void registerChecker(PfRule id, ProofRuleChecker* psc);
private:
+ /** statistics class */
+ ProofCheckerStatistics d_stats;
/** Maps proof steps to their checker */
std::map<PfRule, ProofRuleChecker*> d_checker;
+ /**
+ * Check internal. This is used by check and checkDebug above. It writes
+ * checking errors on out. We treat trusted checkers (nullptr in the range
+ * of the map d_checker) as failures if useTrustedChecker = false.
+ */
+ Node checkInternal(PfRule id,
+ const std::vector<Node>& cchildren,
+ const std::vector<Node>& args,
+ Node expected,
+ std::stringstream& out,
+ bool useTrustedChecker);
};
} // namespace CVC4
projects / cvc5.git / commitdiff