[proof-new] A simple proof generator for buffered proof steps (#5069)

This commit also modifies proof equality engine to use this new proof generator rather than the FactProofGenerator, on which this new one is based.

Co-authored-by: Andrew Reynolds <andrew.j.reynolds@gmail.com>

5 files changed, 151 insertions, 85 deletions

diff --git a/src/expr/CMakeLists.txt b/src/expr/CMakeLists.txt
index aed7a866c..3e3b569af 100644
--- a/src/expr/CMakeLists.txt
+++ b/src/expr/CMakeLists.txt
@@ -7,6 +7,8 @@ libcvc4_add_sources(
   attribute.cpp
   attribute_internals.h
   attribute_unique_id.h
+  buffered_proof_generator.cpp
+  buffered_proof_generator.h
   emptyset.cpp
   emptyset.h
   expr_iomanip.cpp
diff --git a/src/expr/buffered_proof_generator.cpp b/src/expr/buffered_proof_generator.cpp
new file mode 100644
index 000000000..aa0fe19bd
--- /dev/null
+++ b/src/expr/buffered_proof_generator.cpp
@@ -0,0 +1,82 @@
+/*********************                                                        */
+/*! \file buffered_proof_generator.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds, Haniel Barbosa
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 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 a proof generator for buffered proof steps
+ **/
+
+#include "expr/buffered_proof_generator.h"
+
+#include "expr/proof.h"
+
+namespace CVC4 {
+
+BufferedProofGenerator::BufferedProofGenerator(context::Context* c,
+                                               ProofNodeManager* pnm)
+    : ProofGenerator(), d_facts(c), d_pnm(pnm)
+{
+}
+
+bool BufferedProofGenerator::addStep(Node fact,
+                                     ProofStep ps,
+                                     CDPOverwrite opolicy)
+{
+  // check duplicates if we are not always overwriting
+  if (opolicy != CDPOverwrite::ALWAYS)
+  {
+    if (d_facts.find(fact) != d_facts.end())
+    {
+      // duplicate
+      return false;
+    }
+    Node symFact = CDProof::getSymmFact(fact);
+    if (!symFact.isNull())
+    {
+      if (d_facts.find(symFact) != d_facts.end())
+      {
+        // duplicate due to symmetry
+        return false;
+      }
+    }
+  }
+  // note that this replaces the value fact is mapped to if there is already one
+  d_facts.insert(fact, std::make_shared<ProofStep>(ps));
+  return true;
+}
+
+std::shared_ptr<ProofNode> BufferedProofGenerator::getProofFor(Node fact)
+{
+  Trace("pfee-fact-gen") << "BufferedProofGenerator::getProofFor: " << fact
+                         << std::endl;
+  NodeProofStepMap::iterator it = d_facts.find(fact);
+  if (it == d_facts.end())
+  {
+    Node symFact = CDProof::getSymmFact(fact);
+    if (symFact.isNull())
+    {
+      Trace("pfee-fact-gen") << "...cannot find step" << std::endl;
+      Assert(false);
+      return nullptr;
+    }
+    it = d_facts.find(symFact);
+    if (it == d_facts.end())
+    {
+      Assert(false);
+      Trace("pfee-fact-gen") << "...cannot find step (no sym)" << std::endl;
+      return nullptr;
+    }
+  }
+  Trace("pfee-fact-gen") << "...return via step " << *(*it).second << std::endl;
+  CDProof cdp(d_pnm);
+  cdp.addStep(fact, *(*it).second);
+  return cdp.getProofFor(fact);
+}
+
+}  // namespace CVC4
diff --git a/src/expr/buffered_proof_generator.h b/src/expr/buffered_proof_generator.h
new file mode 100644
index 000000000..987bd2465
--- /dev/null
+++ b/src/expr/buffered_proof_generator.h
@@ -0,0 +1,65 @@
+/*********************                                                        */
+/*! \file buffered_proof_generator.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds, Haniel Barbosa
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 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 A proof generator for buffered proof steps
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__EXPR__BUFFERED_PROOF_GENERATOR_H
+#define CVC4__EXPR__BUFFERED_PROOF_GENERATOR_H
+
+#include <map>
+#include <vector>
+
+#include "context/cdhashmap.h"
+#include "context/cdhashset.h"
+#include "expr/proof_generator.h"
+#include "expr/proof_node_manager.h"
+#include "expr/proof_step_buffer.h"
+
+namespace CVC4 {
+
+/**
+ * The proof generator for buffered steps. This class is a context-dependent
+ * mapping from formulas to proof steps. It does not generate ProofNodes until it
+ * is asked to provide a proof for a given fact.
+ */
+class BufferedProofGenerator : public ProofGenerator
+{
+  typedef context::CDHashMap<Node, std::shared_ptr<ProofStep>, NodeHashFunction>
+      NodeProofStepMap;
+
+ public:
+  BufferedProofGenerator(context::Context* c, ProofNodeManager* pnm);
+  ~BufferedProofGenerator() {}
+  /** add step
+   * Unless the overwrite policy is ALWAYS it does not replace previously
+   * registered steps (modulo (dis)equality symmetry).
+   */
+  bool addStep(Node fact,
+               ProofStep ps,
+               CDPOverwrite opolicy = CDPOverwrite::NEVER);
+  /** Get proof for. It is robust to (dis)equality symmetry. */
+  std::shared_ptr<ProofNode> getProofFor(Node f) override;
+  /** identify */
+  std::string identify() const override { return "BufferedProofGenerator"; }
+
+ private:
+  /** maps expected to ProofStep */
+  NodeProofStepMap d_facts;
+  /** the proof node manager */
+  ProofNodeManager* d_pnm;
+};
+
+}  // namespace CVC4
+
+#endif /* CVC4__EXPR__BUFFERED_PROOF_GENERATOR_H */
diff --git a/src/theory/uf/proof_equality_engine.cpp b/src/theory/uf/proof_equality_engine.cpp
index c8f5ebb4d..5811257ed 100644
--- a/src/theory/uf/proof_equality_engine.cpp
+++ b/src/theory/uf/proof_equality_engine.cpp
@@ -573,62 +573,6 @@ void ProofEqEngine::explainWithProof(Node lit,
   Trace("pfee-proof") << "pfee::explainWithProof: finished" << std::endl;
 }
 
-
-ProofEqEngine::FactProofGenerator::FactProofGenerator(context::Context* c,
-                                                      ProofNodeManager* pnm)
-    : ProofGenerator(), d_facts(c), d_pnm(pnm)
-{
-}
-
-bool ProofEqEngine::FactProofGenerator::addStep(Node fact, ProofStep ps)
-{
-  if (d_facts.find(fact) != d_facts.end())
-  {
-    // duplicate
-    return false;
-  }
-  Node symFact = CDProof::getSymmFact(fact);
-  if (!symFact.isNull())
-  {
-    if (d_facts.find(symFact) != d_facts.end())
-    {
-      // duplicate due to symmetry
-      return false;
-    }
-  }
-  d_facts.insert(fact, std::make_shared<ProofStep>(ps));
-  return true;
-}
-
-std::shared_ptr<ProofNode> ProofEqEngine::FactProofGenerator::getProofFor(
-    Node fact)
-{
-  Trace("pfee-fact-gen") << "FactProofGenerator::getProofFor: " << fact
-                         << std::endl;
-  NodeProofStepMap::iterator it = d_facts.find(fact);
-  if (it == d_facts.end())
-  {
-    Node symFact = CDProof::getSymmFact(fact);
-    if (symFact.isNull())
-    {
-      Trace("pfee-fact-gen") << "...cannot find step" << std::endl;
-      Assert(false);
-      return nullptr;
-    }
-    it = d_facts.find(symFact);
-    if (it == d_facts.end())
-    {
-      Assert(false);
-      Trace("pfee-fact-gen") << "...cannot find step (no sym)" << std::endl;
-      return nullptr;
-    }
-  }
-  Trace("pfee-fact-gen") << "...return via step " << *(*it).second << std::endl;
-  CDProof cdp(d_pnm);
-  cdp.addStep(fact, *(*it).second);
-  return cdp.getProofFor(fact);
-}
-
 }  // namespace eq
 }  // namespace theory
 }  // namespace CVC4
diff --git a/src/theory/uf/proof_equality_engine.h b/src/theory/uf/proof_equality_engine.h
index 49fde759e..67740d51f 100644
--- a/src/theory/uf/proof_equality_engine.h
+++ b/src/theory/uf/proof_equality_engine.h
@@ -22,11 +22,11 @@
 
 #include "context/cdhashmap.h"
 #include "context/cdhashset.h"
+#include "expr/buffered_proof_generator.h"
 #include "expr/lazy_proof.h"
 #include "expr/node.h"
 #include "expr/proof_node.h"
 #include "expr/proof_node_manager.h"
-#include "expr/proof_step_buffer.h"
 #include "theory/eager_proof_generator.h"
 #include "theory/uf/equality_engine.h"
 
@@ -243,33 +243,6 @@ class ProofEqEngine : public EagerProofGenerator
   TrustNode explain(Node conc);
 
  private:
-  /**
-   * The default proof generator (for simple facts). This class is a context
-   * dependent mapping from formulas to proof steps. It does not generate
-   * ProofNode until it is asked to provide a proof for a given fact.
-   */
-  class FactProofGenerator : public ProofGenerator
-  {
-    typedef context::
-        CDHashMap<Node, std::shared_ptr<ProofStep>, NodeHashFunction>
-            NodeProofStepMap;
-
-   public:
-    FactProofGenerator(context::Context* c, ProofNodeManager* pnm);
-    ~FactProofGenerator() {}
-    /** add step */
-    bool addStep(Node fact, ProofStep ps);
-    /** Get proof for */
-    std::shared_ptr<ProofNode> getProofFor(Node f) override;
-    /** identify */
-    std::string identify() const override { return "FactProofGenerator"; }
-
-   private:
-    /** maps expected to ProofStep */
-    NodeProofStepMap d_facts;
-    /** the proof node manager */
-    ProofNodeManager* d_pnm;
-  };
   /** Assert internal */
   bool assertFactInternal(TNode pred, bool polarity, TNode reason);
   /** holds */
@@ -302,7 +275,7 @@ class ProofEqEngine : public EagerProofGenerator
   /** Reference to the equality engine */
   eq::EqualityEngine& d_ee;
   /** The default proof generator (for simple facts) */
-  FactProofGenerator d_factPg;
+  BufferedProofGenerator d_factPg;
   /** common nodes */
   Node d_true;
   Node d_false;