diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-06-10 16:52:46 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-06-10 14:52:46 -0700 |
commit | 356647c4b7eb2420f6c6b350f0622bb4c863b0a5 (patch) | |
tree | 88f88d0c0cc573bcee6fa94732a70abc0d33657d /src/theory/builtin | |
parent | 2da2646dd65e0458311a2dccfb04850c0b7d9e3c (diff) |
(proof-new) Theory proof step buffer utility (#4580)
This is a common class for adding steps for theory-specific proof rules into a ProofStepBuffer.
Diffstat (limited to 'src/theory/builtin')
-rw-r--r-- | src/theory/builtin/proof_checker.cpp | 15 | ||||
-rw-r--r-- | src/theory/builtin/proof_checker.h | 21 |
2 files changed, 30 insertions, 6 deletions
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<Node>& args, 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 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<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; @@ -121,11 +135,6 @@ class BuiltinProofRuleChecker : public ProofRuleChecker 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. */ |