diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-06-03 14:01:13 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-06-03 14:01:13 -0500 |
| commit | f70e265cd4e7df46a1b3b7e3cc67fbf9b9b1b528 (patch) | |
| tree | 289b34fd775c89b2d44b464b18d40f43d16e0630 /src/expr/proof_rule.cpp | |
| parent | 145b9367255d2925b6b4e43818e223b9186bcfad (diff) | |
(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.
Diffstat (limited to 'src/expr/proof_rule.cpp')
| -rw-r--r-- | src/expr/proof_rule.cpp | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/src/expr/proof_rule.cpp b/src/expr/proof_rule.cpp index e555f5691..09ffc82bf 100644 --- a/src/expr/proof_rule.cpp +++ b/src/expr/proof_rule.cpp @@ -25,6 +25,12 @@ const char* toString(PfRule id) //================================================= Core rules case PfRule::ASSUME: return "ASSUME"; case PfRule::SCOPE: return "SCOPE"; + case PfRule::SUBS: return "SUBS"; + case PfRule::REWRITE: return "REWRITE"; + 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"; //================================================= Unknown rule case PfRule::UNKNOWN: return "UNKNOWN"; |