From: Andrew Reynolds Date: Wed, 10 Jun 2020 21:52:46 +0000 (-0500) Subject: (proof-new) Theory proof step buffer utility (#4580) X-Git-Tag: cvc5-1.0.0~3230 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=356647c4b7eb2420f6c6b350f0622bb4c863b0a5;p=cvc5.git (proof-new) Theory proof step buffer utility (#4580) This is a common class for adding steps for theory-specific proof rules into a ProofStepBuffer. --- diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 1820fbb5d..0ed3934a7 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -643,7 +643,6 @@ libcvc4_add_sources( theory/rewriter.h theory/rewriter_attributes.h theory/sep/theory_sep.cpp - theory/theory_rewriter.h theory/sep/theory_sep.h theory/sep/theory_sep_rewriter.cpp theory/sep/theory_sep_rewriter.h @@ -744,6 +743,9 @@ libcvc4_add_sources( theory/theory_model.h theory/theory_model_builder.cpp theory/theory_model_builder.h + theory/theory_proof_step_buffer.cpp + theory/theory_proof_step_buffer.h + theory/theory_rewriter.h theory/theory_registrar.h theory/theory_test_utils.h theory/trust_node.cpp diff --git a/src/theory/builtin/proof_checker.cpp b/src/theory/builtin/proof_checker.cpp index 1884d3890..dbbaf63b1 100644 --- a/src/theory/builtin/proof_checker.cpp +++ b/src/theory/builtin/proof_checker.cpp @@ -354,6 +354,21 @@ bool BuiltinProofRuleChecker::getMethodIds(const std::vector& args, return true; } +void BuiltinProofRuleChecker::addMethodIds(std::vector& args, + MethodId ids, + MethodId idr) +{ + bool ndefRewriter = (idr != MethodId::RW_REWRITE); + if (ids != MethodId::SB_DEFAULT || ndefRewriter) + { + args.push_back(mkMethodId(ids)); + } + if (ndefRewriter) + { + args.push_back(mkMethodId(idr)); + } +} + } // namespace builtin } // namespace theory } // namespace CVC4 diff --git a/src/theory/builtin/proof_checker.h b/src/theory/builtin/proof_checker.h index f4424b107..ba5c6574f 100644 --- a/src/theory/builtin/proof_checker.h +++ b/src/theory/builtin/proof_checker.h @@ -110,8 +110,22 @@ class BuiltinProofRuleChecker : public ProofRuleChecker const std::vector& exp, MethodId ids = MethodId::SB_DEFAULT, MethodId idr = MethodId::RW_REWRITE); - /** get a rewriter Id from a node, return false if we fail */ + /** get a method identifier from a node, return false if we fail */ static bool getMethodId(TNode n, MethodId& i); + /** + * Get method identifiers from args starting at the given index. Store their + * values into ids, idr. This method returns false if args does not contain + * valid method identifiers at position index in args. + */ + bool getMethodIds(const std::vector& args, + MethodId& ids, + MethodId& idr, + size_t index); + /** + * Add method identifiers ids and idr as nodes to args. This does not add ids + * or idr if their values are the default ones. + */ + static void addMethodIds(std::vector& args, MethodId ids, MethodId idr); /** Register all rules owned by this rule checker into pc. */ void registerTo(ProofChecker* pc) override; @@ -121,11 +135,6 @@ class BuiltinProofRuleChecker : public ProofRuleChecker Node checkInternal(PfRule id, const std::vector& children, const std::vector& args) override; - /** get method identifiers */ - bool getMethodIds(const std::vector& args, - MethodId& ids, - MethodId& idr, - size_t index); /** * Apply rewrite (on Skolem form). id is the identifier of the rewriter. */ diff --git a/src/theory/theory_proof_step_buffer.cpp b/src/theory/theory_proof_step_buffer.cpp new file mode 100644 index 000000000..3ea2f3627 --- /dev/null +++ b/src/theory/theory_proof_step_buffer.cpp @@ -0,0 +1,94 @@ +/********************* */ +/*! \file theory_proof_step_buffer.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 theory proof step buffer utility + **/ + +#include "theory/theory_proof_step_buffer.h" + +#include "expr/proof.h" + +using namespace CVC4::kind; + +namespace CVC4 { +namespace theory { + +TheoryProofStepBuffer::TheoryProofStepBuffer(ProofChecker* pc) + : ProofStepBuffer(pc) +{ +} + +bool TheoryProofStepBuffer::applyPredTransform(Node src, + Node tgt, + const std::vector& exp, + MethodId ids, + MethodId idr) +{ + // symmetric equalities + if (CDProof::isSame(src, tgt)) + { + return true; + } + std::vector children; + children.push_back(src); + std::vector args; + // try to prove that tgt rewrites to src + children.insert(children.end(), exp.begin(), exp.end()); + args.push_back(tgt); + builtin::BuiltinProofRuleChecker::addMethodIds(args, ids, idr); + Node res = tryStep(PfRule::MACRO_SR_PRED_TRANSFORM, children, args); + if (res.isNull()) + { + // failed to apply + return false; + } + // should definitely have concluded tgt + Assert(res == tgt); + return true; +} + +bool TheoryProofStepBuffer::applyPredIntro(Node tgt, + const std::vector& exp, + MethodId ids, + MethodId idr) +{ + std::vector args; + args.push_back(tgt); + builtin::BuiltinProofRuleChecker::addMethodIds(args, ids, idr); + Node res = tryStep(PfRule::MACRO_SR_PRED_INTRO, exp, args); + if (res.isNull()) + { + return false; + } + Assert(res == tgt); + return true; +} + +Node TheoryProofStepBuffer::applyPredElim(Node src, + const std::vector& exp, + MethodId ids, + MethodId idr) +{ + std::vector children; + children.push_back(src); + children.insert(children.end(), exp.begin(), exp.end()); + std::vector args; + builtin::BuiltinProofRuleChecker::addMethodIds(args, ids, idr); + Node srcRew = tryStep(PfRule::MACRO_SR_PRED_ELIM, children, args); + if (CDProof::isSame(src, srcRew)) + { + popStep(); + } + return srcRew; +} + +} // namespace theory +} // namespace CVC4 diff --git a/src/theory/theory_proof_step_buffer.h b/src/theory/theory_proof_step_buffer.h new file mode 100644 index 000000000..b0ef4e8c1 --- /dev/null +++ b/src/theory/theory_proof_step_buffer.h @@ -0,0 +1,81 @@ +/********************* */ +/*! \file theory_proof_step_buffer.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 Theory proof step buffer utility. + **/ + +#include "cvc4_private.h" + +#ifndef CVC4__THEORY__THEORY_PROOF_STEP_BUFFER_H +#define CVC4__THEORY__THEORY_PROOF_STEP_BUFFER_H + +#include + +#include "expr/node.h" +#include "expr/proof_step_buffer.h" +#include "theory/builtin/proof_checker.h" + +namespace CVC4 { +namespace theory { +/** + * Class used to speculatively try and buffer a set of proof steps before + * sending them to a proof object, extended with theory-specfic proof rule + * utilities. + */ +class TheoryProofStepBuffer : public ProofStepBuffer +{ + public: + TheoryProofStepBuffer(ProofChecker* pc = nullptr); + ~TheoryProofStepBuffer() {} + //---------------------------- utilities builtin proof rules + /** + * Apply predicate transform. If this method returns true, it adds (at most + * one) proof step to the buffer that conclude tgt from premises src, exp. In + * particular, it may attempt to apply MACRO_SR_PRED_TRANSFORM. This method + * should be applied when src and tgt are equivalent formulas assuming exp. + */ + bool applyPredTransform(Node src, + Node tgt, + const std::vector& exp, + MethodId ids = MethodId::SB_DEFAULT, + MethodId idr = MethodId::RW_REWRITE); + /** + * Apply predicate introduction. If this method returns true, it adds proof + * step(s) to the buffer that conclude tgt from premises exp. In particular, + * it may attempt to apply the rule MACRO_SR_PRED_INTRO. This method should be + * applied when tgt is equivalent to true assuming exp. + */ + bool applyPredIntro(Node tgt, + const std::vector& exp, + MethodId ids = MethodId::SB_DEFAULT, + MethodId idr = MethodId::RW_REWRITE); + /** + * Apply predicate elimination. This method returns the result of applying + * the rule MACRO_SR_PRED_ELIM on src, exp. The returned formula is equivalent + * to src assuming exp. If the return value is equivalent to src, then no + * proof step is added to this buffer, since this step is a no-op in this + * case. + * + * Notice that in contrast to the other rules above, predicate elimination + * never fails and proves a formula that is not explicitly given as an + * argument tgt. Thus, the return value of this method is Node not bool. + */ + Node applyPredElim(Node src, + const std::vector& exp, + MethodId ids = MethodId::SB_DEFAULT, + MethodId idr = MethodId::RW_REWRITE); + //---------------------------- end utilities builtin proof rules +}; + +} // namespace theory +} // namespace CVC4 + +#endif /* CVC4__THEORY__THEORY_PROOF_STEP_BUFFER_H */