Merge branch 'master' into fixCMSBuildPRfixCMSBuildPR

1 files changed, 44 insertions, 9 deletions

diff --git a/src/expr/proof_rule.h b/src/expr/proof_rule.h
index 59c406d28..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
@@ -520,6 +541,20 @@ enum class PfRule : uint32_t
   // ----------------------------------------
   // Conclusion: (not F)
   FALSE_ELIM,
+  // ======== HO trust
+  // Children: none
+  // Arguments: (t)
+  // ---------------------
+  // Conclusion: (= t TheoryUfRewriter::getHoApplyForApplyUf(t))
+  // For example, this rule concludes (f x y) = (HO_APPLY (HO_APPLY f x) y)
+  HO_APP_ENCODE,
+  // ======== Congruence
+  // Children: (P1:(= f g), P2:(= t1 s1), ..., Pn+1:(= tn sn))
+  // Arguments: ()
+  // ---------------------------------------------
+  // Conclusion: (= (f t1 ... tn) (g s1 ... sn))
+  // Notice that this rule is only used when the application kinds are APPLY_UF.
+  HO_CONG,
 
   //================================================= Quantifiers rules
   // ======== Witness intro