(proof-new) Proof recording for assertions pipeline (#4766)

Adds explicit steps to preprocess proof generator if one is provided.

1 files changed, 40 insertions, 10 deletions

diff --git a/src/preprocessing/assertion_pipeline.h b/src/preprocessing/assertion_pipeline.h
index 5d8f64594..4fa8b5bb4 100644
--- a/src/preprocessing/assertion_pipeline.h
+++ b/src/preprocessing/assertion_pipeline.h
@@ -21,7 +21,11 @@
 #include <vector>
 
 #include "expr/node.h"
+#include "expr/proof_generator.h"
+#include "expr/proof_node_manager.h"
+#include "smt/preprocess_proof_generator.h"
 #include "smt/term_formula_removal.h"
+#include "theory/trust_node.h"
 
 namespace CVC4 {
 namespace preprocessing {
@@ -54,8 +58,17 @@ class AssertionPipeline
    * @param n The assertion/assumption
    * @param isAssumption If true, records that \p n is an assumption. Note that
    * all assumptions have to be added contiguously.
+   * @param isInput If true, n is an input formula (an assumption in the main
+   * body of the overall proof).
+   * @param pg The proof generator who can provide a proof of n. The proof
+   * generator is not required and is ignored if isInput is true.
    */
-  void push_back(Node n, bool isAssumption = false);
+  void push_back(Node n,
+                 bool isAssumption = false,
+                 bool isInput = false,
+                 ProofGenerator* pg = nullptr);
+  /** Same as above, with TrustNode */
+  void pushBackTrusted(theory::TrustNode trn);
 
   std::vector<Node>& ref() { return d_nodes; }
   const std::vector<Node>& ref() const { return d_nodes; }
@@ -66,21 +79,31 @@ class AssertionPipeline
   /*
    * Replaces assertion i with node n and records the dependency between the
    * original assertion and its replacement.
+   *
+   * @param i The position of the assertion to replace.
+   * @param n The replacement assertion.
+   * @param pg The proof generator who can provide a proof of d_nodes[i] == n,
+   * where d_nodes[i] is the assertion at position i prior to this call.
    */
-  void replace(size_t i, Node n);
+  void replace(size_t i, Node n, ProofGenerator* pg = nullptr);
+  /** Same as above, with TrustNode */
+  void replaceTrusted(size_t i, theory::TrustNode trn);
 
   /*
    * Replaces assertion i with node n and records that this replacement depends
    * on assertion i and the nodes listed in addnDeps. The dependency
    * information is used for unsat cores and proofs.
+   *
+   * @param i The position of the assertion to replace.
+   * @param n The replacement assertion.
+   * @param addnDeps The dependencies.
+   * @param pg The proof generator who can provide a proof of d_nodes[i] == n,
+   * where d_nodes[i] is the assertion at position i prior to this call.
    */
-  void replace(size_t i, Node n, const std::vector<Node>& addnDeps);
-
-  /*
-   * Replaces an assertion with a vector of assertions and records the
-   * dependencies.
-   */
-  void replace(size_t i, const std::vector<Node>& ns);
+  void replace(size_t i,
+               Node n,
+               const std::vector<Node>& addnDeps,
+               ProofGenerator* pg = nullptr);
 
   IteSkolemMap& getIteSkolemMap() { return d_iteSkolemMap; }
   const IteSkolemMap& getIteSkolemMap() const { return d_iteSkolemMap; }
@@ -125,7 +148,12 @@ class AssertionPipeline
   {
     return d_storeSubstsInAsserts && i == d_substsIndex;
   }
-
+  //------------------------------------ for proofs
+  /** Set proof generator */
+  void setProofGenerator(smt::PreprocessProofGenerator* pppg);
+  /** Is proof enabled? */
+  bool isProofEnabled() const;
+  //------------------------------------ end for proofs
  private:
   /** The list of current assertions */
   std::vector<Node> d_nodes;
@@ -157,6 +185,8 @@ class AssertionPipeline
   size_t d_assumptionsStart;
   /** The number of assumptions */
   size_t d_numAssumptions;
+  /** The proof generator, if one is provided */
+  smt::PreprocessProofGenerator* d_pppg;
 }; /* class AssertionPipeline */
 
 }  // namespace preprocessing