(proof-new) Updates to builtin proof checker (#4962)

This includes support for some trusted rules (whose use is to come). It also modifies THEORY_REWRITE so that it is a "trusted" rule, that is, it is not re-checked. The reason for this is that TheoryRewriter is not deterministic. An example of non-determinism in TheoryRewriter are rules that introduce bound variables (e.g. quantifiers rewriter) since these bound variables are fresh each time it is invoked. Non-deterministic theory rewriters cannot be rechecked, which was leading to failures on proof-new at proof check time. The other way to fix this would be to cache TheoryRewriter responses, but then the checker would only be verifying that the caching was being done properly. This is not worthwhile.

2 files changed, 33 insertions, 10 deletions

diff --git a/src/expr/proof_rule.cpp b/src/expr/proof_rule.cpp
index bd58fc787..1d46b183f 100644
--- a/src/expr/proof_rule.cpp
+++ b/src/expr/proof_rule.cpp
@@ -27,13 +27,15 @@ const char* toString(PfRule id)
     case PfRule::SCOPE: return "SCOPE";
     case PfRule::SUBS: return "SUBS";
     case PfRule::REWRITE: return "REWRITE";
+    case PfRule::EVALUATE: return "EVALUATE";
     case PfRule::MACRO_SR_EQ_INTRO: return "MACRO_SR_EQ_INTRO";
     case PfRule::MACRO_SR_PRED_INTRO: return "MACRO_SR_PRED_INTRO";
     case PfRule::MACRO_SR_PRED_ELIM: return "MACRO_SR_PRED_ELIM";
     case PfRule::MACRO_SR_PRED_TRANSFORM: return "MACRO_SR_PRED_TRANSFORM";
-    case PfRule::THEORY_REWRITE: return "THEORY_REWRITE";
     case PfRule::REMOVE_TERM_FORMULA_AXIOM: return "REMOVE_TERM_FORMULA_AXIOM";
     //================================================= Trusted rules
+    case PfRule::THEORY_LEMMA: return "THEORY_LEMMA";
+    case PfRule::THEORY_REWRITE: return "THEORY_REWRITE";
     case PfRule::PREPROCESS: return "PREPROCESS";
     case PfRule::PREPROCESS_LEMMA: return "PREPROCESS_LEMMA";
     case PfRule::THEORY_PREPROCESS: return "THEORY_PREPROCESS";
diff --git a/src/expr/proof_rule.h b/src/expr/proof_rule.h
index b6b9f1ea8..825503d5d 100644
--- a/src/expr/proof_rule.h
+++ b/src/expr/proof_rule.h
@@ -91,6 +91,14 @@ enum class PfRule : uint32_t
   // where idr is a MethodId identifier, which determines the kind of rewriter
   // to apply, e.g. Rewriter::rewrite.
   REWRITE,
+  // ======== Evaluate
+  // Children: none
+  // Arguments: (t)
+  // ----------------------------------------
+  // Conclusion: (= t Evaluator::evaluate(t))
+  // Note this is equivalent to:
+  //   (REWRITE t MethodId::RW_EVALUATE)
+  EVALUATE,
   // ======== Substitution + Rewriting equality introduction
   //
   // In this rule, we provide a term t and conclude that it is equal to its
@@ -163,15 +171,6 @@ enum class PfRule : uint32_t
   // Notice that we apply rewriting on the witness form of F and G, similar to
   // MACRO_SR_PRED_INTRO.
   MACRO_SR_PRED_TRANSFORM,
-  // ======== Theory Rewrite
-  // Children: none
-  // Arguments: (t, preRewrite?)
-  // ----------------------------------------
-  // Conclusion: (= t t')
-  // where
-  //  t' is the result of applying either a pre-rewrite or a post-rewrite step
-  //  to t (depending on the second argument).
-  THEORY_REWRITE,
 
   //================================================= Processing rules
   // ======== Remove Term Formulas Axiom
@@ -182,6 +181,28 @@ enum class PfRule : uint32_t
   REMOVE_TERM_FORMULA_AXIOM,
 
   //================================================= Trusted rules
+  // ======== Theory lemma
+  // Children: none
+  // Arguments: (F, tid)
+  // ---------------------------------------------------------------
+  // Conclusion: F
+  // where F is a (T-valid) theory lemma generated by theory with TheoryId tid.
+  // This is a "coarse-grained" rule that is used as a placeholder if a theory
+  // did not provide a proof for a lemma or conflict.
+  THEORY_LEMMA,
+  // ======== Theory Rewrite
+  // Children: none
+  // Arguments: (F, tid, preRewrite?)
+  // ----------------------------------------
+  // Conclusion: F
+  // where F is an equality of the form (= t t') where t' is obtained by
+  // applying the theory rewriter with identifier tid in either its prewrite
+  // (when preRewrite is true) or postrewrite method. Notice that the checker
+  // for this rule does not replay the rewrite to ensure correctness, since
+  // theory rewriter methods are not static. For example, the quantifiers
+  // rewriter involves constructing new bound variables that are not guaranteed
+  // to be consistent on each call.
+  THEORY_REWRITE,
   // The rules in this section have the signature of a "trusted rule":
   //
   // Children: none