(proof-new) Proofs for non-clausal simplification (#5409)

Adds proof support in non-clausal simplification, connecting the proofs from circuit propagator.

1 files changed, 41 insertions, 3 deletions

diff --git a/src/preprocessing/passes/non_clausal_simp.h b/src/preprocessing/passes/non_clausal_simp.h
index defb3cc82..d3a9e0b1a 100644
--- a/src/preprocessing/passes/non_clausal_simp.h
+++ b/src/preprocessing/passes/non_clausal_simp.h
@@ -19,9 +19,12 @@
 
 #include <vector>
 
+#include "expr/lazy_proof.h"
 #include "expr/node.h"
 #include "preprocessing/preprocessing_pass.h"
 #include "preprocessing/preprocessing_pass_context.h"
+#include "smt/preprocess_proof_generator.h"
+#include "theory/trust_node.h"
 
 namespace CVC4 {
 namespace preprocessing {
@@ -45,9 +48,44 @@ class NonClausalSimp : public PreprocessingPass
   };
 
   Statistics d_statistics;
-
-  /** Learned literals */
-  std::vector<Node> d_nonClausalLearnedLiterals;
+  /**
+   * Transform learned literal lit. We apply substitutions in subs once and then
+   * apply constant propagations cp to fixed point. Return the rewritten
+   * form of lit.
+   *
+   * If proofs are enabled, then we require that the learned literal preprocess
+   * proof generator (d_llpg) has a proof of lit when this method is called,
+   * and ensure that the return literal also has a proof in d_llpg.
+   */
+  Node processLearnedLit(Node lit,
+                         theory::TrustSubstitutionMap* subs,
+                         theory::TrustSubstitutionMap* cp);
+  /**
+   * Process rewritten learned literal. This is called when we have a
+   * learned literal lit that is rewritten to litr based on the proof generator
+   * contained in trn (if it exists). The trust node trn should be of kind
+   * REWRITE and proving (= lit litr).
+   *
+   * This tracks the proof in the learned literal preprocess proof generator
+   * d_llpg below and returns the rewritten learned literal.
+   */
+  Node processRewrittenLearnedLit(theory::TrustNode trn);
+  /** Is proof enabled? */
+  bool isProofEnabled() const;
+  /** The proof node manager */
+  ProofNodeManager* d_pnm;
+  /** the learned literal preprocess proof generator */
+  std::unique_ptr<smt::PreprocessProofGenerator> d_llpg;
+  /**
+   * An lazy proof for learned literals that are reasserted into the assertions
+   * pipeline by this class.
+   */
+  std::unique_ptr<LazyCDProof> d_llra;
+  /**
+   * A context-dependent list of trust substitution maps, which are required
+   * for storing proofs.
+   */
+  context::CDList<std::shared_ptr<theory::TrustSubstitutionMap> > d_tsubsList;
 };
 
 }  // namespace passes