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

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

4 files changed, 205 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.
    */
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<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
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 <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 */