(proof-new) Theory proof step buffer utility (#4580)

This is a common class for adding steps for theory-specific proof rules into a ProofStepBuffer.

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.
    */