This adds the proof checker for TheoryBuiltin, which handles the core proof rules (SCOPE and ASSUME) and all proof rules corresponding to generic operations on Node objects. This includes proof rules for rewriting and substitution, which are added in this PR.
theory/builtin/theory_builtin_rewriter.cpp
theory/builtin/theory_builtin_rewriter.h
theory/builtin/theory_builtin_type_rules.h
+ theory/builtin/proof_checker.cpp
+ theory/builtin/proof_checker.h
theory/builtin/type_enumerator.cpp
theory/builtin/type_enumerator.h
theory/bv/abstraction.cpp
//================================================= Core rules
case PfRule::ASSUME: return "ASSUME";
case PfRule::SCOPE: return "SCOPE";
+ case PfRule::SUBS: return "SUBS";
+ case PfRule::REWRITE: return "REWRITE";
+ case PfRule::MACRO_SR_EQ_INTRO: return "MACRO_SR_EQ_INTRO";
+ 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";
//================================================= Unknown rule
case PfRule::UNKNOWN: return "UNKNOWN";
// proof with no free assumptions always concludes a valid formula.
SCOPE,
+ //======================== 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, (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
+ // 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'
+ // 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: 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,
+
//================================================= 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 equality proof checker
+ **/
+
+#include "theory/builtin/proof_checker.h"
+
+#include "expr/proof_skolem_cache.h"
+#include "theory/rewriter.h"
+#include "theory/theory.h"
+
+using namespace CVC4::kind;
+
+namespace CVC4 {
+namespace theory {
+
+const char* toString(MethodId id)
+{
+ switch (id)
+ {
+ case MethodId::RW_REWRITE: return "RW_REWRITE";
+ case MethodId::RW_IDENTITY: return "RW_IDENTITY";
+ case MethodId::SB_DEFAULT: return "SB_DEFAULT";
+ case MethodId::SB_LITERAL: return "SB_LITERAL";
+ case MethodId::SB_FORMULA: return "SB_FORMULA";
+ default: return "MethodId::Unknown";
+ };
+}
+
+std::ostream& operator<<(std::ostream& out, MethodId id)
+{
+ out << toString(id);
+ return out;
+}
+
+Node mkMethodId(MethodId id)
+{
+ return NodeManager::currentNM()->mkConst(Rational(static_cast<uint32_t>(id)));
+}
+
+namespace builtin {
+
+void BuiltinProofRuleChecker::registerTo(ProofChecker* pc)
+{
+ pc->registerChecker(PfRule::ASSUME, this);
+ pc->registerChecker(PfRule::SCOPE, this);
+ pc->registerChecker(PfRule::SUBS, this);
+ pc->registerChecker(PfRule::REWRITE, this);
+ pc->registerChecker(PfRule::MACRO_SR_EQ_INTRO, this);
+ pc->registerChecker(PfRule::MACRO_SR_PRED_INTRO, this);
+ pc->registerChecker(PfRule::MACRO_SR_PRED_ELIM, this);
+ pc->registerChecker(PfRule::MACRO_SR_PRED_TRANSFORM, this);
+}
+
+Node BuiltinProofRuleChecker::applyRewrite(Node n, MethodId idr)
+{
+ Node nk = ProofSkolemCache::getSkolemForm(n);
+ Node nkr = applyRewriteExternal(nk, idr);
+ return ProofSkolemCache::getWitnessForm(nkr);
+}
+
+Node BuiltinProofRuleChecker::applySubstitution(Node n, Node exp, MethodId ids)
+{
+ if (exp.isNull() || exp.getKind() != EQUAL)
+ {
+ return Node::null();
+ }
+ Node nk = ProofSkolemCache::getSkolemForm(n);
+ Node nks = applySubstitutionExternal(nk, exp, ids);
+ return ProofSkolemCache::getWitnessForm(nks);
+}
+
+Node BuiltinProofRuleChecker::applySubstitution(Node n,
+ const std::vector<Node>& exp,
+ MethodId ids)
+{
+ Node nk = ProofSkolemCache::getSkolemForm(n);
+ Node nks = applySubstitutionExternal(nk, exp, ids);
+ return ProofSkolemCache::getWitnessForm(nks);
+}
+
+Node BuiltinProofRuleChecker::applySubstitutionRewrite(
+ Node n, const std::vector<Node>& exp, MethodId ids, MethodId idr)
+{
+ Node nk = ProofSkolemCache::getSkolemForm(n);
+ Node nks = applySubstitutionExternal(nk, exp, ids);
+ Node nksr = applyRewriteExternal(nks, idr);
+ return ProofSkolemCache::getWitnessForm(nksr);
+}
+
+Node BuiltinProofRuleChecker::applyRewriteExternal(Node n, MethodId idr)
+{
+ Trace("builtin-pfcheck-debug")
+ << "applyRewriteExternal (" << idr << "): " << n << std::endl;
+ if (idr == MethodId::RW_REWRITE)
+ {
+ return Rewriter::rewrite(n);
+ }
+ else if (idr == MethodId::RW_IDENTITY)
+ {
+ // does nothing
+ return n;
+ }
+ // unknown rewriter
+ Assert(false)
+ << "BuiltinProofRuleChecker::applyRewriteExternal: no rewriter for "
+ << idr << std::endl;
+ return n;
+}
+
+Node BuiltinProofRuleChecker::applySubstitutionExternal(Node n,
+ Node exp,
+ MethodId ids)
+{
+ Assert(!exp.isNull());
+ Node expk = ProofSkolemCache::getSkolemForm(exp);
+ TNode var, subs;
+ if (ids == MethodId::SB_DEFAULT)
+ {
+ if (expk.getKind() != EQUAL)
+ {
+ return Node::null();
+ }
+ var = expk[0];
+ subs = expk[1];
+ }
+ else if (ids == MethodId::SB_LITERAL)
+ {
+ bool polarity = expk.getKind() != NOT;
+ var = polarity ? expk : expk[0];
+ subs = NodeManager::currentNM()->mkConst(polarity);
+ }
+ else if (ids == MethodId::SB_FORMULA)
+ {
+ var = expk;
+ subs = NodeManager::currentNM()->mkConst(true);
+ }
+ else
+ {
+ Assert(false) << "BuiltinProofRuleChecker::applySubstitutionExternal: no "
+ "substitution for "
+ << ids << std::endl;
+ }
+ return n.substitute(var, subs);
+}
+
+Node BuiltinProofRuleChecker::applySubstitutionExternal(
+ Node n, const std::vector<Node>& exp, MethodId ids)
+{
+ Node curr = n;
+ // apply substitution one at a time, in reverse order
+ for (size_t i = 0, nexp = exp.size(); i < nexp; i++)
+ {
+ if (exp[nexp - 1 - i].isNull())
+ {
+ return Node::null();
+ }
+ curr = applySubstitutionExternal(curr, exp[nexp - 1 - i], ids);
+ if (curr.isNull())
+ {
+ break;
+ }
+ }
+ return curr;
+}
+
+bool BuiltinProofRuleChecker::getMethodId(TNode n, MethodId& i)
+{
+ uint32_t index;
+ if (!getUInt32(n, index))
+ {
+ return false;
+ }
+ i = static_cast<MethodId>(index);
+ return true;
+}
+
+Node BuiltinProofRuleChecker::checkInternal(PfRule id,
+ const std::vector<Node>& children,
+ const std::vector<Node>& args)
+{
+ // compute what was proven
+ if (id == PfRule::ASSUME)
+ {
+ Assert(children.empty());
+ Assert(args.size() == 1);
+ Assert(args[0].getType().isBoolean());
+ return args[0];
+ }
+ else if (id == PfRule::SCOPE)
+ {
+ Assert(children.size() == 1);
+ if (args.empty())
+ {
+ // no antecedant
+ return children[0];
+ }
+ Node ant = mkAnd(args);
+ // if the conclusion is false, its the negated antencedant only
+ if (children[0].isConst() && !children[0].getConst<bool>())
+ {
+ return ant.notNode();
+ }
+ return NodeManager::currentNM()->mkNode(IMPLIES, ant, children[0]);
+ }
+ else if (id == PfRule::SUBS)
+ {
+ Assert(children.size() > 0);
+ Assert(1 <= args.size() && args.size() <= 2);
+ MethodId ids = MethodId::SB_DEFAULT;
+ if (args.size() == 2 && !getMethodId(args[1], ids))
+ {
+ return Node::null();
+ }
+ std::vector<Node> exp;
+ for (size_t i = 0, nchild = children.size(); i < nchild; i++)
+ {
+ exp.push_back(children[i]);
+ }
+ Node res = applySubstitution(args[0], exp);
+ return args[0].eqNode(res);
+ }
+ else if (id == PfRule::REWRITE)
+ {
+ Assert(children.empty());
+ Assert(1 <= args.size() && args.size() <= 2);
+ MethodId ids = MethodId::RW_REWRITE;
+ if (args.size() == 2 && !getMethodId(args[1], ids))
+ {
+ return Node::null();
+ }
+ Node res = applyRewrite(args[0]);
+ return args[0].eqNode(res);
+ }
+ else if (id == PfRule::MACRO_SR_EQ_INTRO)
+ {
+ Assert(1 <= args.size() && args.size() <= 3);
+ MethodId ids, idr;
+ if (!getMethodIds(args, ids, idr, 1))
+ {
+ return Node::null();
+ }
+ Node res = applySubstitutionRewrite(args[0], children, idr);
+ return args[0].eqNode(res);
+ }
+ else if (id == PfRule::MACRO_SR_PRED_INTRO)
+ {
+ Trace("builtin-pfcheck") << "Check " << id << " " << children.size() << " "
+ << args.size() << std::endl;
+ Assert(1 <= args.size() && args.size() <= 3);
+ MethodId ids, idr;
+ if (!getMethodIds(args, ids, idr, 1))
+ {
+ return Node::null();
+ }
+ Node res = applySubstitutionRewrite(args[0], children, ids, idr);
+ if (res.isNull())
+ {
+ return Node::null();
+ }
+ // **** NOTE: can rewrite the witness form here. This enables certain lemmas
+ // to be provable, e.g. (= k t) where k is a purification Skolem for t.
+ res = Rewriter::rewrite(res);
+ if (!res.isConst() || !res.getConst<bool>())
+ {
+ Trace("builtin-pfcheck")
+ << "Failed to rewrite to true, res=" << res << std::endl;
+ return Node::null();
+ }
+ return args[0];
+ }
+ else if (id == PfRule::MACRO_SR_PRED_ELIM)
+ {
+ Trace("builtin-pfcheck") << "Check " << id << " " << children.size() << " "
+ << args.size() << std::endl;
+ Assert(children.size() >= 1);
+ Assert(args.size() <= 2);
+ std::vector<Node> exp;
+ exp.insert(exp.end(), children.begin() + 1, children.end());
+ MethodId ids, idr;
+ if (!getMethodIds(args, ids, idr, 0))
+ {
+ return Node::null();
+ }
+ Node res1 = applySubstitutionRewrite(children[0], exp, ids, idr);
+ Trace("builtin-pfcheck") << "Returned " << res1 << std::endl;
+ return res1;
+ }
+ else if (id == PfRule::MACRO_SR_PRED_TRANSFORM)
+ {
+ Trace("builtin-pfcheck") << "Check " << id << " " << children.size() << " "
+ << args.size() << std::endl;
+ Assert(children.size() >= 1);
+ Assert(1 <= args.size() && args.size() <= 3);
+ Assert(args[0].getType().isBoolean());
+ MethodId ids, idr;
+ if (!getMethodIds(args, ids, idr, 1))
+ {
+ return Node::null();
+ }
+ std::vector<Node> exp;
+ exp.insert(exp.end(), children.begin() + 1, children.end());
+ Node res1 = applySubstitutionRewrite(children[0], exp, ids, idr);
+ Node res2 = applySubstitutionRewrite(args[0], exp, ids, idr);
+ // can rewrite the witness forms
+ res1 = Rewriter::rewrite(res1);
+ res2 = Rewriter::rewrite(res2);
+ if (res1.isNull() || res1 != res2)
+ {
+ Trace("builtin-pfcheck") << "Failed to match results" << std::endl;
+ Trace("builtin-pfcheck-debug") << res1 << " vs " << res2 << std::endl;
+ return Node::null();
+ }
+ return args[0];
+ }
+ // no rule
+ return Node::null();
+}
+
+bool BuiltinProofRuleChecker::getMethodIds(const std::vector<Node>& args,
+ MethodId& ids,
+ MethodId& idr,
+ size_t index)
+{
+ ids = MethodId::SB_DEFAULT;
+ idr = MethodId::RW_REWRITE;
+ if (args.size() > index)
+ {
+ if (!getMethodId(args[index], ids))
+ {
+ Trace("builtin-pfcheck")
+ << "Failed to get id from " << args[index] << std::endl;
+ return false;
+ }
+ }
+ if (args.size() > index + 1)
+ {
+ if (!getMethodId(args[index + 1], idr))
+ {
+ Trace("builtin-pfcheck")
+ << "Failed to get id from " << args[index + 1] << std::endl;
+ return false;
+ }
+ }
+ return true;
+}
+
+} // namespace builtin
+} // namespace theory
+} // namespace CVC4
--- /dev/null
+/********************* */
+/*! \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 Equality proof checker utility
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__THEORY__BUILTIN__PROOF_CHECKER_H
+#define CVC4__THEORY__BUILTIN__PROOF_CHECKER_H
+
+#include "expr/node.h"
+#include "expr/proof_checker.h"
+#include "expr/proof_node.h"
+
+namespace CVC4 {
+namespace theory {
+
+/**
+ * Identifiers for rewriters and substitutions, which we abstractly
+ * classify as "methods". Methods have a unique identifier in the internal
+ * proof calculus implemented by the checker below.
+ *
+ * A "rewriter" is abstractly a method from Node to Node, where the output
+ * is semantically equivalent to the input. The identifiers below list
+ * various methods that have this contract. This identifier is used
+ * in a number of the builtin rules.
+ *
+ * A substitution is a method for turning a formula into a substitution.
+ */
+enum class MethodId : uint32_t
+{
+ //---------------------------- Rewriters
+ // Rewriter::rewrite(n)
+ RW_REWRITE,
+ // identity
+ RW_IDENTITY,
+ //---------------------------- Substitutions
+ // (= x y) is interpreted as x -> y, using Node::substitute
+ SB_DEFAULT,
+ // P, (not P) are interpreted as P -> true, P -> false using Node::substitute
+ SB_LITERAL,
+ // P is interpreted as P -> true using Node::substitute
+ SB_FORMULA,
+};
+/** Converts a rewriter id to a string. */
+const char* toString(MethodId id);
+/** Write a rewriter id to out */
+std::ostream& operator<<(std::ostream& out, MethodId id);
+/** Make a method id node */
+Node mkMethodId(MethodId id);
+
+namespace builtin {
+
+/** A checker for builtin proofs */
+class BuiltinProofRuleChecker : public ProofRuleChecker
+{
+ public:
+ BuiltinProofRuleChecker() {}
+ ~BuiltinProofRuleChecker() {}
+ /**
+ * Apply rewrite on n (in witness form). This encapsulates the exact behavior
+ * of a REWRITE step in a proof. Rewriting is performed on the Skolem form of
+ * n.
+ *
+ * @param n The node (in witness form) to rewrite,
+ * @param idr The method identifier of the rewriter, by default RW_REWRITE
+ * specifying a call to Rewriter::rewrite.
+ * @return The rewritten form of n.
+ */
+ static Node applyRewrite(Node n, MethodId idr = MethodId::RW_REWRITE);
+ /**
+ * Apply substitution on n (in witness form). This encapsulates the exact
+ * behavior of a SUBS step in a proof. Substitution is on the Skolem form of
+ * n.
+ *
+ * @param n The node (in witness form) to substitute,
+ * @param exp The (set of) equalities (in witness form) corresponding to the
+ * substitution
+ * @param ids The method identifier of the substitution, by default SB_DEFAULT
+ * specifying that lhs/rhs of equalities are interpreted as a substitution.
+ * @return The substituted form of n.
+ */
+ static Node applySubstitution(Node n,
+ Node exp,
+ MethodId ids = MethodId::SB_DEFAULT);
+ static Node applySubstitution(Node n,
+ const std::vector<Node>& exp,
+ MethodId ids = MethodId::SB_DEFAULT);
+ /** Apply substitution + rewriting
+ *
+ * Combines the above two steps.
+ *
+ * @param n The node (in witness form) to substitute and rewrite,
+ * @param exp The (set of) equalities (in witness form) corresponding to the
+ * substitution
+ * @param ids The method identifier of the substitution.
+ * @param idr The method identifier of the rewriter.
+ * @return The substituted, rewritten form of n.
+ */
+ static Node applySubstitutionRewrite(Node n,
+ const std::vector<Node>& exp,
+ MethodId ids = MethodId::SB_DEFAULT,
+ MethodId idr = MethodId::RW_REWRITE);
+ /** get a rewriter Id from a node, return false if we fail */
+ static bool getMethodId(TNode n, MethodId& i);
+
+ /** 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<Node>& children,
+ const std::vector<Node>& args) override;
+ /** get method identifiers */
+ bool getMethodIds(const std::vector<Node>& args,
+ MethodId& ids,
+ MethodId& idr,
+ size_t index);
+ /**
+ * Apply rewrite (on Skolem form). id is the identifier of the rewriter.
+ */
+ static Node applyRewriteExternal(Node n, MethodId idr = MethodId::RW_REWRITE);
+ /**
+ * Apply substitution for n (on Skolem form), where exp is an equality
+ * (or set of equalities) in Witness form. Returns the result of
+ * n * sigma{ids}(exp), where sigma{ids} is a substitution based on method
+ * identifier ids.
+ */
+ static Node applySubstitutionExternal(Node n, Node exp, MethodId ids);
+ /** Same as above, for a list of substitutions in exp */
+ static Node applySubstitutionExternal(Node n,
+ const std::vector<Node>& exp,
+ MethodId ids);
+};
+
+} // namespace builtin
+} // namespace theory
+} // namespace CVC4
+
+#endif /* CVC4__THEORY__BUILTIN__PROOF_CHECKER_H */
projects / cvc5.git / commitdiff