[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>

1 files changed, 82 insertions, 0 deletions

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