diff options
Diffstat (limited to 'src/expr/proof_rule.h')
-rw-r--r-- | src/expr/proof_rule.h | 39 |
1 files changed, 30 insertions, 9 deletions
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 |