This is a common class for adding steps for theory-specific proof rules into a ProofStepBuffer.
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
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
return true;
}
+void BuiltinProofRuleChecker::addMethodIds(std::vector<Node>& 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
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 */
+ /** 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<Node>& 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<Node>& args, MethodId ids, MethodId idr);
/** Register all rules owned by this rule checker into pc. */
void registerTo(ProofChecker* pc) override;
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.
*/
--- /dev/null
+/********************* */
+/*! \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<Node>& exp,
+ MethodId ids,
+ MethodId idr)
+{
+ // symmetric equalities
+ if (CDProof::isSame(src, tgt))
+ {
+ return true;
+ }
+ std::vector<Node> children;
+ children.push_back(src);
+ std::vector<Node> 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<Node>& exp,
+ MethodId ids,
+ MethodId idr)
+{
+ std::vector<Node> 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<Node>& exp,
+ MethodId ids,
+ MethodId idr)
+{
+ std::vector<Node> children;
+ children.push_back(src);
+ children.insert(children.end(), exp.begin(), exp.end());
+ std::vector<Node> 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
--- /dev/null
+/********************* */
+/*! \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 <vector>
+
+#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<Node>& 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<Node>& 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<Node>& 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 */
projects / cvc5.git / commitdiff