// 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
// 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,
--- /dev/null
+/********************* */
+/*! \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<Node>& children, const std::vector<Node>& 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<Node> 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<Node> echildren(children[0][0].begin(), children[0][0].end());
+ exists = nm->mkNode(EXISTS, echildren);
+ }
+ std::vector<Node> 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<Node> vars;
+ std::vector<Node> 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
projects / cvc5.git / commitdiff