diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-09-21 12:09:33 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-09-21 12:09:33 -0500 |
| commit | 44fd0bd8441d9dcce5aa9173757c9d8173924c17 (patch) | |
| tree | db47d0c29fffeca7301d83ab6ef4320ccd37701b /src/expr/proof_rule.cpp | |
| parent | 63e7c6bb6d9c99a5282241be8b32a04ea67dfb8d (diff) | |
(proof-new) Add the arrays proof checker (#5047)
Includes adding the standard method for constructing the extensionality skolem using the skolem manager.
Diffstat (limited to 'src/expr/proof_rule.cpp')
| -rw-r--r-- | src/expr/proof_rule.cpp | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/src/expr/proof_rule.cpp b/src/expr/proof_rule.cpp index 57dd3e0bd..400567b5d 100644 --- a/src/expr/proof_rule.cpp +++ b/src/expr/proof_rule.cpp @@ -102,6 +102,13 @@ const char* toString(PfRule id) case PfRule::FALSE_ELIM: return "FALSE_ELIM"; case PfRule::HO_APP_ENCODE: return "HO_APP_ENCODE"; case PfRule::HO_CONG: return "HO_CONG"; + //================================================= Array rules + case PfRule::ARRAYS_READ_OVER_WRITE: return "ARRAYS_READ_OVER_WRITE"; + case PfRule::ARRAYS_READ_OVER_WRITE_CONTRA: + return "ARRAYS_READ_OVER_WRITE_CONTRA"; + case PfRule::ARRAYS_READ_OVER_WRITE_1: return "ARRAYS_READ_OVER_WRITE_1"; + case PfRule::ARRAYS_EXT: return "ARRAYS_EXT"; + case PfRule::ARRAYS_TRUST: return "ARRAYS_TRUST"; //================================================= Quantifiers rules case PfRule::WITNESS_INTRO: return "WITNESS_INTRO"; case PfRule::EXISTS_INTRO: return "EXISTS_INTRO"; |