(proof-new) Add lazy proof set utility (#5221)

This is a common pattern that is required in several places in preprocessing.

diff --git a/src/expr/CMakeLists.txt b/src/expr/CMakeLists.txt
index 8742612ad6e1cd3a3526c6bb55cee50949502ed3..ccc5752892b129710f80e9c7d8627ac96a4aa4b4 100644 (file)
--- a/src/expr/CMakeLists.txt
+++ b/src/expr/CMakeLists.txt
@@ -31,6 +31,8 @@ libcvc4_add_sources(
   lazy_proof.h
   lazy_proof_chain.cpp
   lazy_proof_chain.h
+  lazy_proof_set.cpp
+  lazy_proof_set.h
   match_trie.cpp
   match_trie.h
   node.cpp

diff --git a/src/expr/lazy_proof_set.cpp b/src/expr/lazy_proof_set.cpp
new file mode 100644 (file)
index 0000000..be6abbb
--- /dev/null
+++ b/src/expr/lazy_proof_set.cpp
@@ -0,0 +1,39 @@
+/*********************                                                        */
+/*! \file lazy_proof_set.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** 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 Lazy proof set utility
+ **/
+
+#include "expr/lazy_proof_set.h"
+
+namespace CVC4 {
+
+LazyCDProofSet::LazyCDProofSet(ProofNodeManager* pnm,
+                               context::Context* c,
+                               std::string namePrefix)
+    : d_pnm(pnm),
+      d_contextUse(c ? c : &d_context),
+      d_pfs(d_contextUse),
+      d_namePrefix(namePrefix)
+{
+}
+
+LazyCDProof* LazyCDProofSet::allocateProof(bool isCd)
+{
+  std::stringstream ss;
+  ss << d_namePrefix << "_" << d_pfs.size();
+  std::shared_ptr<LazyCDProof> pf = std::make_shared<LazyCDProof>(
+      d_pnm, nullptr, isCd ? d_contextUse : nullptr, ss.str());
+  d_pfs.push_back(pf);
+  return pf.get();
+}
+
+}  // namespace CVC4

diff --git a/src/expr/lazy_proof_set.h b/src/expr/lazy_proof_set.h
new file mode 100644 (file)
index 0000000..3501aab
--- /dev/null
+++ b/src/expr/lazy_proof_set.h
@@ -0,0 +1,67 @@
+/*********************                                                        */
+/*! \file lazy_proof_set.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** 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 Lazy proof set utility
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__EXPR__LAZY_PROOF_SET_H
+#define CVC4__EXPR__LAZY_PROOF_SET_H
+
+#include <memory>
+
+#include "context/cdlist.h"
+#include "context/context.h"
+#include "expr/lazy_proof.h"
+
+namespace CVC4 {
+
+/**
+ * A (context-dependent) set of lazy proofs, which is used for memory
+ * management purposes.
+ */
+class LazyCDProofSet
+{
+ public:
+  LazyCDProofSet(ProofNodeManager* pnm,
+                 context::Context* c = nullptr,
+                 std::string namePrefix = "LazyCDProof");
+  ~LazyCDProofSet() {}
+  /**
+   * Allocate a lazy proof. This returns a fresh lazy proof object that
+   * remains alive in the context given to this class.  Internally, this adds a
+   * LazyCDProof to the list d_pfs below.
+   *
+   * @param isCd Whether the proof is context-dependent (using the same context
+   * that is provided to this class).
+   */
+  LazyCDProof* allocateProof(bool isCd = false);
+
+ protected:
+  /** The proof node manager */
+  ProofNodeManager* d_pnm;
+  /** A dummy context used by this class if none is provided */
+  context::Context d_context;
+  /**
+   * The context we are using (either the one provided in the constructor or
+   * d_context).
+   */
+  context::Context* d_contextUse;
+  /** A context-dependent list of lazy proofs. */
+  context::CDList<std::shared_ptr<LazyCDProof> > d_pfs;
+  /** The name prefix of the lazy proofs */
+  std::string d_namePrefix;
+};
+
+}  // namespace CVC4
+
+#endif /* CVC4__EXPR__LAZY_PROOF_SET_H */