(proof-new) Split proof ensure closed checks to own file (#5522)

Split proof ensure closed checks to own file

1 files changed, 0 insertions, 43 deletions

diff --git a/src/expr/proof_generator.h b/src/expr/proof_generator.h
index 6e6316356..869f226b8 100644
--- a/src/expr/proof_generator.h
+++ b/src/expr/proof_generator.h
@@ -107,49 +107,6 @@ class ProofGenerator
   virtual std::string identify() const = 0;
 };
 
-/**
- * Debug check closed on Trace c. Context ctx is string for debugging.
- * This method throws an assertion failure if pg cannot provide a closed
- * proof for fact proven. This is checked only if --proof-new-eager-checking
- * is enabled or the Trace c is enabled.
- *
- * @param reqGen Whether we consider a null generator to be a failure.
- */
-void pfgEnsureClosed(Node proven,
-                     ProofGenerator* pg,
-                     const char* c,
-                     const char* ctx,
-                     bool reqGen = true);
-
-/**
- * Debug check closed with Trace c. Context ctx is string for debugging and
- * assumps is the set of allowed open assertions. This method throws an
- * assertion failure if pg cannot provide a proof for fact proven whose
- * free assumptions are contained in assumps.
- *
- * @param reqGen Whether we consider a null generator to be a failure.
- */
-void pfgEnsureClosedWrt(Node proven,
-                        ProofGenerator* pg,
-                        const std::vector<Node>& assumps,
-                        const char* c,
-                        const char* ctx,
-                        bool reqGen = true);
-
-/**
- * Debug check closed with Trace c, proof node versions. This gives an
- * assertion failure if pn is not closed. Detailed information is printed
- * on trace c. Context ctx is a string used for debugging.
- */
-void pfnEnsureClosed(ProofNode* pn, const char* c, const char* ctx);
-/**
- * Same as above, but throws an assertion failure only if the free assumptions
- * of pn are not contained in assumps.
- */
-void pfnEnsureClosedWrt(ProofNode* pn,
-                        const std::vector<Node>& assumps,
-                        const char* c,
-                        const char* ctx);
 }  // namespace CVC4
 
 #endif /* CVC4__EXPR__PROOF_GENERATOR_H */