From: Andrew Reynolds Date: Tue, 16 Jun 2020 00:04:29 +0000 (-0500) Subject: (proof-new) Add quantifiers proof checker (#4593) X-Git-Tag: cvc5-1.0.0~3213 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=df98bc96168869e1615bc0756bde3b2c5dba160e;p=cvc5.git (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. --- diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index a5160d2fe..c50578c46 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -534,6 +534,8 @@ libcvc4_add_sources( theory/quantifiers/instantiate.h theory/quantifiers/lazy_trie.cpp theory/quantifiers/lazy_trie.h + theory/quantifiers/proof_checker.cpp + theory/quantifiers/proof_checker.h theory/quantifiers/quant_conflict_find.cpp theory/quantifiers/quant_conflict_find.h theory/quantifiers/quant_epr.cpp diff --git a/src/expr/proof_rule.cpp b/src/expr/proof_rule.cpp index 595e1d5f7..339b4f582 100644 --- a/src/expr/proof_rule.cpp +++ b/src/expr/proof_rule.cpp @@ -31,15 +31,6 @@ const char* toString(PfRule id) case PfRule::MACRO_SR_PRED_INTRO: return "MACRO_SR_PRED_INTRO"; case PfRule::MACRO_SR_PRED_ELIM: return "MACRO_SR_PRED_ELIM"; case PfRule::MACRO_SR_PRED_TRANSFORM: return "MACRO_SR_PRED_TRANSFORM"; - //================================================= Equality rules - case PfRule::REFL: return "REFL"; - case PfRule::SYMM: return "SYMM"; - case PfRule::TRANS: return "TRANS"; - case PfRule::CONG: return "CONG"; - case PfRule::TRUE_INTRO: return "TRUE_INTRO"; - case PfRule::TRUE_ELIM: return "TRUE_ELIM"; - case PfRule::FALSE_INTRO: return "FALSE_INTRO"; - case PfRule::FALSE_ELIM: return "FALSE_ELIM"; //================================================= Boolean rules case PfRule::SPLIT: return "SPLIT"; case PfRule::AND_ELIM: return "AND_ELIM"; @@ -85,6 +76,20 @@ const char* toString(PfRule id) case PfRule::CNF_ITE_NEG1: return "CNF_ITE_NEG1"; case PfRule::CNF_ITE_NEG2: return "CNF_ITE_NEG2"; case PfRule::CNF_ITE_NEG3: return "CNF_ITE_NEG3"; + //================================================= Equality rules + case PfRule::REFL: return "REFL"; + case PfRule::SYMM: return "SYMM"; + case PfRule::TRANS: return "TRANS"; + case PfRule::CONG: return "CONG"; + case PfRule::TRUE_INTRO: return "TRUE_INTRO"; + case PfRule::TRUE_ELIM: return "TRUE_ELIM"; + case PfRule::FALSE_INTRO: return "FALSE_INTRO"; + case PfRule::FALSE_ELIM: return "FALSE_ELIM"; + //================================================= Quantifiers rules + case PfRule::WITNESS_INTRO: return "WITNESS_INTRO"; + case PfRule::EXISTS_INTRO: return "EXISTS_INTRO"; + case PfRule::SKOLEMIZE: return "SKOLEMIZE"; + case PfRule::INSTANTIATE: return "INSTANTIATE"; //================================================= Unknown rule case PfRule::UNKNOWN: return "UNKNOWN"; default: return "?"; diff --git a/src/expr/proof_rule.h b/src/expr/proof_rule.h index 6acccfffd..daded84d4 100644 --- a/src/expr/proof_rule.h +++ b/src/expr/proof_rule.h @@ -71,55 +71,102 @@ enum class PfRule : uint32_t // has the conclusion (=> F F) and has no free assumptions. More generally, a // proof with no free assumptions always concludes a valid formula. SCOPE, - //================================================= Equality rules - // ======== Reflexive + + //======================== Builtin theory (common node operations) + // ======== Substitution + // Children: (P1:F1, ..., Pn:Fn) + // Arguments: (t, (ids)?) + // --------------------------------------------------------------- + // Conclusion: (= t t*sigma{ids}(Fn)*...*sigma{ids}(F1)) + // where sigma{ids}(Fi) are substitutions, which notice are applied in + // reverse order. + // Notice that ids is a MethodId identifier, which determines how to convert + // the formulas F1, ..., Fn into substitutions. + SUBS, + // ======== Rewrite // Children: none - // Arguments: (t) - // --------------------- - // Conclusion: (= t t) - REFL, - // ======== Symmetric - // Children: (P:(= t1 t2)) or (P:(not (= t1 t2))) - // Arguments: none - // ----------------------- - // Conclusion: (= t2 t1) or (not (= t2 t1)) - SYMM, - // ======== Transitivity - // Children: (P1:(= t1 t2), ..., Pn:(= t{n-1} tn)) - // Arguments: none - // ----------------------- - // Conclusion: (= t1 tn) - TRANS, - // ======== Congruence (subsumed by Substitute?) - // Children: (P1:(= t1 s1), ..., Pn:(= tn sn)) - // Arguments: (f) - // --------------------------------------------- - // Conclusion: (= (f t1 ... tn) (f s1 ... sn)) - CONG, - // ======== True intro - // Children: (P:F) - // Arguments: none - // ---------------------------------------- - // Conclusion: (= F true) - TRUE_INTRO, - // ======== True elim - // Children: (P:(= F true) - // Arguments: none + // Arguments: (t, (idr)?) // ---------------------------------------- + // Conclusion: (= t Rewriter{idr}(t)) + // where idr is a MethodId identifier, which determines the kind of rewriter + // to apply, e.g. Rewriter::rewrite. + REWRITE, + // ======== Substitution + Rewriting equality introduction + // + // In this rule, we provide a term t and conclude that it is equal to its + // rewritten form under a (proven) substitution. + // + // Children: (P1:F1, ..., Pn:Fn) + // Arguments: (t, (ids (idr)?)?) + // --------------------------------------------------------------- + // Conclusion: (= t t') + // where + // t' is + // toWitness(Rewriter{idr}(toSkolem(t)*sigma{ids}(Fn)*...*sigma{ids}(F1))) + // toSkolem(...) converts terms from witness form to Skolem form, + // toWitness(...) converts terms from Skolem form to witness form. + // + // Notice that: + // toSkolem(t')=Rewriter{idr}(toSkolem(t)*sigma{ids}(Fn)*...*sigma{ids}(F1)) + // In other words, from the point of view of Skolem forms, this rule + // transforms t to t' by standard substitution + rewriting. + // + // The argument ids and idr is optional and specify the identifier of the + // substitution and rewriter respectively to be used. For details, see + // theory/builtin/proof_checker.h. + MACRO_SR_EQ_INTRO, + // ======== Substitution + Rewriting predicate introduction + // + // In this rule, we provide a formula F and conclude it, under the condition + // that it rewrites to true under a proven substitution. + // + // Children: (P1:F1, ..., Pn:Fn) + // Arguments: (F, (ids (idr)?)?) + // --------------------------------------------------------------- // Conclusion: F - TRUE_ELIM, - // ======== False intro - // Children: (P:(not F)) - // Arguments: none + // where + // Rewriter{idr}(F*sigma{ids}(Fn)*...*sigma{ids}(F1)) == true + // where ids and idr are method identifiers. + // + // Notice that we apply rewriting on the witness form of F, meaning that this + // rule may conclude an F whose Skolem form is justified by the definition of + // its (fresh) Skolem variables. Furthermore, notice that the rewriting and + // substitution is applied only within the side condition, meaning the + // rewritten form of the witness form of F does not escape this rule. + MACRO_SR_PRED_INTRO, + // ======== Substitution + Rewriting predicate elimination + // + // In this rule, if we have proven a formula F, then we may conclude its + // rewritten form under a proven substitution. + // + // Children: (P1:F, P2:F1, ..., P_{n+1}:Fn) + // Arguments: ((ids (idr)?)?) // ---------------------------------------- - // Conclusion: (= F false) - FALSE_INTRO, - // ======== False elim - // Children: (P:(= F false) - // Arguments: none + // Conclusion: F' + // where + // F' is + // toWitness(Rewriter{idr}(toSkolem(F)*sigma{ids}(Fn)*...*sigma{ids}(F1)). + // where ids and idr are method identifiers. + // + // We rewrite only on the Skolem form of F, similar to MACRO_SR_EQ_INTRO. + MACRO_SR_PRED_ELIM, + // ======== Substitution + Rewriting predicate transform + // + // In this rule, if we have proven a formula F, then we may provide a formula + // G and conclude it if F and G are equivalent after rewriting under a proven + // substitution. + // + // Children: (P1:F, P2:F1, ..., P_{n+1}:Fn) + // Arguments: (G, (ids (idr)?)?) // ---------------------------------------- - // Conclusion: (not F) - FALSE_ELIM, + // Conclusion: G + // where + // Rewriter{idr}(F*sigma{ids}(Fn)*...*sigma{ids}(F1)) == + // Rewriter{idr}(G*sigma{ids}(Fn)*...*sigma{ids}(F1)) + // + // Notice that we apply rewriting on the witness form of F and G, similar to + // MACRO_SR_PRED_INTRO. + MACRO_SR_PRED_TRANSFORM, //================================================= Boolean rules // ======== Split @@ -378,101 +425,87 @@ enum class PfRule : uint32_t // Conclusion: (or (ite C F1 F2) (not F1) (not F2)) CNF_ITE_NEG3, - //======================== Builtin theory (common node operations) - // ======== Substitution - // Children: (P1:F1, ..., Pn:Fn) - // Arguments: (t, (ids)?) - // --------------------------------------------------------------- - // Conclusion: (= t t*sigma{ids}(Fn)*...*sigma{ids}(F1)) - // where sigma{ids}(Fi) are substitutions, which notice are applied in - // reverse order. - // Notice that ids is a MethodId identifier, which determines how to convert - // the formulas F1, ..., Fn into substitutions. - SUBS, - // ======== Rewrite + //================================================= Equality rules + // ======== Reflexive // Children: none - // Arguments: (t, (idr)?) + // Arguments: (t) + // --------------------- + // Conclusion: (= t t) + REFL, + // ======== Symmetric + // Children: (P:(= t1 t2)) or (P:(not (= t1 t2))) + // Arguments: none + // ----------------------- + // Conclusion: (= t2 t1) or (not (= t2 t1)) + SYMM, + // ======== Transitivity + // Children: (P1:(= t1 t2), ..., Pn:(= t{n-1} tn)) + // Arguments: none + // ----------------------- + // Conclusion: (= t1 tn) + TRANS, + // ======== Congruence (subsumed by Substitute?) + // Children: (P1:(= t1 s1), ..., Pn:(= tn sn)) + // Arguments: (f) + // --------------------------------------------- + // Conclusion: (= (f t1 ... tn) (f s1 ... sn)) + CONG, + // ======== True intro + // Children: (P:F) + // Arguments: none + // ---------------------------------------- + // Conclusion: (= F true) + TRUE_INTRO, + // ======== True elim + // Children: (P:(= F true) + // Arguments: none // ---------------------------------------- - // Conclusion: (= t Rewriter{idr}(t)) - // where idr is a MethodId identifier, which determines the kind of rewriter - // to apply, e.g. Rewriter::rewrite. - REWRITE, - // ======== Substitution + Rewriting equality introduction - // - // In this rule, we provide a term t and conclude that it is equal to its - // rewritten form under a (proven) substitution. - // - // Children: (P1:F1, ..., Pn:Fn) - // Arguments: (t, (ids (idr)?)?) - // --------------------------------------------------------------- - // Conclusion: (= t t') - // where - // t' is - // toWitness(Rewriter{idr}(toSkolem(t)*sigma{ids}(Fn)*...*sigma{ids}(F1))) - // toSkolem(...) converts terms from witness form to Skolem form, - // toWitness(...) converts terms from Skolem form to witness form. - // - // Notice that: - // toSkolem(t')=Rewriter{idr}(toSkolem(t)*sigma{ids}(Fn)*...*sigma{ids}(F1)) - // In other words, from the point of view of Skolem forms, this rule - // transforms t to t' by standard substitution + rewriting. - // - // The argument ids and idr is optional and specify the identifier of the - // substitution and rewriter respectively to be used. For details, see - // theory/builtin/proof_checker.h. - MACRO_SR_EQ_INTRO, - // ======== Substitution + Rewriting predicate introduction - // - // In this rule, we provide a formula F and conclude it, under the condition - // that it rewrites to true under a proven substitution. - // - // Children: (P1:F1, ..., Pn:Fn) - // Arguments: (F, (ids (idr)?)?) - // --------------------------------------------------------------- // Conclusion: F - // where - // Rewriter{idr}(F*sigma{ids}(Fn)*...*sigma{ids}(F1)) == true - // where ids and idr are method identifiers. - // - // Notice that we apply rewriting on the witness form of F, meaning that this - // rule may conclude an F whose Skolem form is justified by the definition of - // its (fresh) Skolem variables. Furthermore, notice that the rewriting and - // substitution is applied only within the side condition, meaning the - // rewritten form of the witness form of F does not escape this rule. - MACRO_SR_PRED_INTRO, - // ======== Substitution + Rewriting predicate elimination - // - // In this rule, if we have proven a formula F, then we may conclude its - // rewritten form under a proven substitution. - // - // Children: (P1:F, P2:F1, ..., P_{n+1}:Fn) - // Arguments: ((ids (idr)?)?) + TRUE_ELIM, + // ======== False intro + // Children: (P:(not F)) + // Arguments: none // ---------------------------------------- - // Conclusion: F' - // where - // F' is - // toWitness(Rewriter{idr}(toSkolem(F)*sigma{ids}(Fn)*...*sigma{ids}(F1)). - // where ids and idr are method identifiers. - // - // We rewrite only on the Skolem form of F, similar to MACRO_SR_EQ_INTRO. - MACRO_SR_PRED_ELIM, - // ======== Substitution + Rewriting predicate transform - // - // In this rule, if we have proven a formula F, then we may provide a formula - // G and conclude it if F and G are equivalent after rewriting under a proven - // substitution. - // - // Children: (P1:F, P2:F1, ..., P_{n+1}:Fn) - // Arguments: (G, (ids (idr)?)?) + // Conclusion: (= F false) + FALSE_INTRO, + // ======== False elim + // Children: (P:(= F false) + // Arguments: none // ---------------------------------------- - // Conclusion: G - // where - // Rewriter{idr}(F*sigma{ids}(Fn)*...*sigma{ids}(F1)) == - // Rewriter{idr}(G*sigma{ids}(Fn)*...*sigma{ids}(F1)) - // - // Notice that we apply rewriting on the witness form of F and G, similar to - // MACRO_SR_PRED_INTRO. - MACRO_SR_PRED_TRANSFORM, + // Conclusion: (not F) + FALSE_ELIM, + + //================================================= Quantifiers rules + // ======== Witness intro + // Children: (P:F[t]) + // Arguments: (t) + // ---------------------------------------- + // Conclusion: (= t (witness ((x T)) F[x])) + // where x is a BOUND_VARIABLE unique to the pair F,t. + WITNESS_INTRO, + // ======== Exists intro + // Children: (P:F[t]) + // Arguments: (t) + // ---------------------------------------- + // Conclusion: (exists ((x T)) F[x]) + // where x is a BOUND_VARIABLE unique to the pair F,t. + EXISTS_INTRO, + // ======== Skolemize + // Children: (P:(exists ((x1 T1) ... (xn Tn)) F)) + // Arguments: none + // ---------------------------------------- + // Conclusion: F*sigma + // sigma maps x1 ... xn to their representative skolems obtained by + // SkolemManager::mkSkolemize, returned in the skolems argument of that + // method. + SKOLEMIZE, + // ======== Instantiate + // Children: (P:(forall ((x1 T1) ... (xn Tn)) F)) + // Arguments: (t1 ... tn) + // ---------------------------------------- + // Conclusion: F*sigma + // sigma maps x1 ... xn to t1 ... tn. + INSTANTIATE, //================================================= Unknown rule UNKNOWN, 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 */