1 files changed, 76 insertions, 0 deletions
diff --git a/src/proof/proof_set.h b/src/proof/proof_set.h
new file mode 100644
index 000000000..4015e0466
--- /dev/null
+++ b/src/proof/proof_set.h
@@ -0,0 +1,76 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Gereon Kremer, Andrew Reynolds
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 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.
+ * ****************************************************************************
+ *
+ * Proof set utility.
+ */
+
+#include "cvc5_private.h"
+
+#ifndef CVC5__PROOF__PROOF_SET_H
+#define CVC5__PROOF__PROOF_SET_H
+
+#include <memory>
+
+#include "context/cdlist.h"
+#include "context/context.h"
+#include "proof/proof_node_manager.h"
+
+namespace cvc5 {
+
+/**
+ * A (context-dependent) set of proofs, which is used for memory
+ * management purposes.
+ */
+template <typename T>
+class CDProofSet
+{
+ public:
+  CDProofSet(ProofNodeManager* pnm,
+             context::Context* c,
+             std::string namePrefix = "Proof")
+      : d_pnm(pnm), d_proofs(c), d_namePrefix(namePrefix)
+  {
+  }
+  /**
+   * Allocate a new proof.
+   *
+   * This returns a fresh proof object that remains alive in the context given
+   * to this class. Internally, this adds a new proof of type T to a
+   * context-dependent list of proofs and passes the following arguments to the
+   * T constructor:
+   *   pnm, args..., name
+   * where pnm is the proof node manager
+   * provided to this proof set upon construction, args... are the arguments to
+   * allocateProof() and name is the namePrefix with an appended index.
+   */
+  template <typename... Args>
+  T* allocateProof(Args&&... args)
+  {
+    d_proofs.push_back(std::make_shared<T>(
+        d_pnm,
+        std::forward<Args>(args)...,
+        d_namePrefix + "_" + std::to_string(d_proofs.size())));
+    return d_proofs.back().get();
+  }
+
+ protected:
+  /** The proof node manager */
+  ProofNodeManager* d_pnm;
+  /** A context-dependent list of lazy proofs. */
+  context::CDList<std::shared_ptr<T>> d_proofs;
+  /** The name prefix of the lazy proofs */
+  std::string d_namePrefix;
+};
+
+}  // namespace cvc5
+
+#endif /* CVC5__PROOF__LAZY_PROOF_SET_H */