diff options
Diffstat (limited to 'src/expr/proof_rule.h')
-rw-r--r-- | src/expr/proof_rule.h | 53 |
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 |