From df98bc96168869e1615bc0756bde3b2c5dba160e Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 15 Jun 2020 19:04:29 -0500 Subject: (proof-new) Add quantifiers proof checker (#4593) Adds core rules for quantifiers, some of which also will be used as a general way for introducing and skolemizing witness terms. This PR also changes the order of other rules in proof_rule.h/cpp which was in an abnormal order from previous merges. --- src/theory/quantifiers/proof_checker.cpp | 109 +++++++++++++++++++++++++++++++ src/theory/quantifiers/proof_checker.h | 49 ++++++++++++++ 2 files changed, 158 insertions(+) create mode 100644 src/theory/quantifiers/proof_checker.cpp create mode 100644 src/theory/quantifiers/proof_checker.h (limited to 'src/theory/quantifiers') diff --git a/src/theory/quantifiers/proof_checker.cpp b/src/theory/quantifiers/proof_checker.cpp new file mode 100644 index 000000000..a86fc90f8 --- /dev/null +++ b/src/theory/quantifiers/proof_checker.cpp @@ -0,0 +1,109 @@ +/********************* */ +/*! \file proof_checker.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Implementation of quantifiers proof checker + **/ + +#include "theory/quantifiers/proof_checker.h" + +#include "expr/skolem_manager.h" +#include "theory/builtin/proof_checker.h" + +using namespace CVC4::kind; + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +void QuantifiersProofRuleChecker::registerTo(ProofChecker* pc) +{ + // add checkers + pc->registerChecker(PfRule::WITNESS_INTRO, this); + pc->registerChecker(PfRule::EXISTS_INTRO, this); + pc->registerChecker(PfRule::SKOLEMIZE, this); + pc->registerChecker(PfRule::INSTANTIATE, this); +} + +Node QuantifiersProofRuleChecker::checkInternal( + PfRule id, const std::vector& children, const std::vector& args) +{ + NodeManager* nm = NodeManager::currentNM(); + // compute what was proven + if (id == PfRule::WITNESS_INTRO || id == PfRule::EXISTS_INTRO) + { + Assert(children.size() == 1); + Assert(args.size() == 1); + SkolemManager* sm = nm->getSkolemManager(); + Node p = children[0]; + Node t = args[0]; + Node exists = sm->mkExistential(t, p); + if (id == PfRule::EXISTS_INTRO) + { + return exists; + } + std::vector skolems; + sm->mkSkolemize(exists, skolems, "k"); + Assert(skolems.size() == 1); + return skolems[0]; + } + else if (id == PfRule::SKOLEMIZE) + { + Assert(children.size() == 1); + Assert(args.empty()); + // can use either negated FORALL or EXISTS + if (children[0].getKind() != EXISTS + && (children[0].getKind() != NOT || children[0][0].getKind() != FORALL)) + { + return Node::null(); + } + SkolemManager* sm = nm->getSkolemManager(); + Node exists; + if (children[0].getKind() == EXISTS) + { + exists = children[0]; + } + else + { + std::vector echildren(children[0][0].begin(), children[0][0].end()); + exists = nm->mkNode(EXISTS, echildren); + } + std::vector skolems; + Node res = sm->mkSkolemize(exists, skolems, "k"); + return res; + } + else if (id == PfRule::INSTANTIATE) + { + Assert(children.size() == 1); + if (children[0].getKind() != FORALL + || args.size() != children[0][0].getNumChildren()) + { + return Node::null(); + } + Node body = children[0][1]; + std::vector vars; + std::vector subs; + for (unsigned i = 0, nargs = args.size(); i < nargs; i++) + { + vars.push_back(children[0][0][i]); + subs.push_back(args[i]); + } + Node inst = + body.substitute(vars.begin(), vars.end(), subs.begin(), subs.end()); + return inst; + } + + // no rule + return Node::null(); +} + +} // namespace quantifiers +} // namespace theory +} // namespace CVC4 diff --git a/src/theory/quantifiers/proof_checker.h b/src/theory/quantifiers/proof_checker.h new file mode 100644 index 000000000..fd55dbf31 --- /dev/null +++ b/src/theory/quantifiers/proof_checker.h @@ -0,0 +1,49 @@ +/********************* */ +/*! \file proof_checker.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Quantifiers proof checker utility + **/ + +#include "cvc4_private.h" + +#ifndef CVC4__THEORY__QUANTIFIERS__PROOF_CHECKER_H +#define CVC4__THEORY__QUANTIFIERS__PROOF_CHECKER_H + +#include "expr/node.h" +#include "expr/proof_checker.h" +#include "expr/proof_node.h" + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +/** A checker for quantifiers proofs */ +class QuantifiersProofRuleChecker : public ProofRuleChecker +{ + public: + QuantifiersProofRuleChecker() {} + ~QuantifiersProofRuleChecker() {} + + /** Register all rules owned by this rule checker into pc. */ + void registerTo(ProofChecker* pc) override; + + protected: + /** Return the conclusion of the given proof step, or null if it is invalid */ + Node checkInternal(PfRule id, + const std::vector& children, + const std::vector& args) override; +}; + +} // namespace quantifiers +} // namespace theory +} // namespace CVC4 + +#endif /* CVC4__THEORY__QUANTIFIERS__PROOF_CHECKER_H */ -- cgit v1.2.3