(proof-new) Add builtin proof checker (#4537)

This adds the proof checker for TheoryBuiltin, which handles the core proof rules (SCOPE and ASSUME) and all proof rules corresponding to generic operations on Node objects. This includes proof rules for rewriting and substitution, which are added in this PR.

1 files changed, 96 insertions, 0 deletions

diff --git a/src/expr/proof_rule.h b/src/expr/proof_rule.h
index 0d03bb347..e0a626b69 100644
--- a/src/expr/proof_rule.h
+++ b/src/expr/proof_rule.h
@@ -72,6 +72,102 @@ enum class PfRule : uint32_t
   // proof with no free assumptions always concludes a valid formula.
   SCOPE,
 
+  //======================== Builtin theory (common node operations)
+  // ======== Substitution
+  // Children: (P1:F1, ..., Pn:Fn)
+  // Arguments: (t, (ids)?)
+  // ---------------------------------------------------------------
+  // Conclusion: (= t t*sigma{ids}(Fn)*...*sigma{ids}(F1))
+  // where sigma{ids}(Fi) are substitutions, which notice are applied in
+  // reverse order.
+  // Notice that ids is a MethodId identifier, which determines how to convert
+  // the formulas F1, ..., Fn into substitutions.
+  SUBS,
+  // ======== Rewrite
+  // Children: none
+  // Arguments: (t, (idr)?)
+  // ----------------------------------------
+  // Conclusion: (= t Rewriter{idr}(t))
+  // where idr is a MethodId identifier, which determines the kind of rewriter
+  // to apply, e.g. Rewriter::rewrite.
+  REWRITE,
+  // ======== Substitution + Rewriting equality introduction
+  //
+  // In this rule, we provide a term t and conclude that it is equal to its
+  // rewritten form under a (proven) substitution.
+  //
+  // Children: (P1:F1, ..., Pn:Fn)
+  // Arguments: (t, (ids (idr)?)?)
+  // ---------------------------------------------------------------
+  // Conclusion: (= t t')
+  // where
+  //   t' is 
+  //   toWitness(Rewriter{idr}(toSkolem(t)*sigma{ids}(Fn)*...*sigma{ids}(F1)))
+  //   toSkolem(...) converts terms from witness form to Skolem form,
+  //   toWitness(...) converts terms from Skolem form to witness form.
+  //
+  // Notice that:
+  //   toSkolem(t')=Rewriter{idr}(toSkolem(t)*sigma{ids}(Fn)*...*sigma{ids}(F1))
+  // In other words, from the point of view of Skolem forms, this rule
+  // transforms t to t' by standard substitution + rewriting.
+  //
+  // The argument ids and idr is optional and specify the identifier of the
+  // substitution and rewriter respectively to be used. For details, see
+  // theory/builtin/proof_checker.h.
+  MACRO_SR_EQ_INTRO,
+  // ======== Substitution + Rewriting predicate introduction
+  //
+  // In this rule, we provide a formula F and conclude it, under the condition
+  // that it rewrites to true under a proven substitution.
+  //
+  // Children: (P1:F1, ..., Pn:Fn)
+  // Arguments: (F, (ids (idr)?)?)
+  // ---------------------------------------------------------------
+  // Conclusion: F
+  // where
+  //   Rewriter{idr}(F*sigma{ids}(Fn)*...*sigma{ids}(F1)) == true
+  // where ids and idr are method identifiers.
+  //
+  // Notice that we apply rewriting on the witness form of F, meaning that this
+  // rule may conclude an F whose Skolem form is justified by the definition of
+  // its (fresh) Skolem variables. Furthermore, notice that the rewriting and
+  // substitution is applied only within the side condition, meaning the
+  // rewritten form of the witness form of F does not escape this rule.
+  MACRO_SR_PRED_INTRO,
+  // ======== Substitution + Rewriting predicate elimination
+  //
+  // In this rule, if we have proven a formula F, then we may conclude its
+  // rewritten form under a proven substitution.
+  //
+  // Children: (P1:F, P2:F1, ..., P_{n+1}:Fn)
+  // Arguments: ((ids (idr)?)?)
+  // ----------------------------------------
+  // Conclusion: F'
+  // where
+  //   F' is
+  //   toWitness(Rewriter{idr}(toSkolem(F)*sigma{ids}(Fn)*...*sigma{ids}(F1)).
+  // where ids and idr are method identifiers.
+  //
+  // We rewrite only on the Skolem form of F, similar to MACRO_SR_EQ_INTRO.
+  MACRO_SR_PRED_ELIM,
+  // ======== Substitution + Rewriting predicate transform
+  //
+  // In this rule, if we have proven a formula F, then we may provide a formula
+  // G and conclude it if F and G are equivalent after rewriting under a proven
+  // substitution.
+  //
+  // Children: (P1:F, P2:F1, ..., P_{n+1}:Fn)
+  // Arguments: (G, (ids (idr)?)?)
+  // ----------------------------------------
+  // Conclusion: G
+  // where
+  //   Rewriter{idr}(F*sigma{ids}(Fn)*...*sigma{ids}(F1)) ==
+  //   Rewriter{idr}(G*sigma{ids}(Fn)*...*sigma{ids}(F1))
+  //
+  // Notice that we apply rewriting on the witness form of F and G, similar to
+  // MACRO_SR_PRED_INTRO.
+  MACRO_SR_PRED_TRANSFORM,
+  
   //================================================= Unknown rule
   UNKNOWN,
 };