(proof-new) Theory preprocessor proof producing (#4807)

This makes the theory preprocessor proof producing in the new infrastructure, which involves updating its interfaces to TrustNode in a few places.

1 files changed, 18 insertions, 12 deletions

diff --git a/src/expr/proof_rule.h b/src/expr/proof_rule.h
index a83e043bf..59c406d28 100644
--- a/src/expr/proof_rule.h
+++ b/src/expr/proof_rule.h
@@ -174,29 +174,35 @@ enum class PfRule : uint32_t
   THEORY_REWRITE,
 
   //================================================= Processing rules
-  // ======== Preprocess (trusted)
+  // ======== Remove Term Formulas Axiom
+  // Children: none
+  // Arguments: (t)
+  // ---------------------------------------------------------------
+  // Conclusion: RemoveTermFormulas::getAxiomFor(t).
+  REMOVE_TERM_FORMULA_AXIOM,
+
+  //================================================= Trusted rules
+  // The rules in this section have the signature of a "trusted rule":
+  //
   // Children: none
   // Arguments: (F)
   // ---------------------------------------------------------------
   // Conclusion: F
+  //
   // where F is an equality of the form t = t' where t was replaced by t'
   // based on some preprocessing pass, or otherwise F was added as a new
   // assertion by some preprocessing pass.
   PREPROCESS,
-  // ======== Witness axiom (trusted)
-  // Children: none
-  // Arguments: (F)
-  // ---------------------------------------------------------------
-  // Conclusion: F
+  // where F was added as a new assertion by some preprocessing pass.
+  PREPROCESS_LEMMA,
+  // where F is an equality of the form t = Theory::ppRewrite(t) for some
+  // theory. Notice this is a "trusted" rule.
+  THEORY_PREPROCESS,
+  // where F was added as a new assertion by theory preprocessing.
+  THEORY_PREPROCESS_LEMMA,
   // where F is an existential (exists ((x T)) (P x)) used for introducing
   // a witness term (witness ((x T)) (P x)).
   WITNESS_AXIOM,
-  // ======== Remove Term Formulas Axiom
-  // Children: none
-  // Arguments: (t)
-  // ---------------------------------------------------------------
-  // Conclusion: RemoveTermFormulas::getAxiomFor(t).
-  REMOVE_TERM_FORMULA_AXIOM,
 
   //================================================= Boolean rules
   // ======== Split