diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-10-26 12:33:01 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-10-26 12:33:01 -0500 |
| commit | 04640a15faeee34b064dc4f1d2045300c2a6f329 (patch) | |
| tree | 86d566b52d4fd9410a0b9ab17b73bd0111b0a8e8 /src/expr/proof_rule.cpp | |
| parent | d7ef769395f75b7acae3dd36df587a4438db5673 (diff) | |
(proof-new) Add datatypes proof checker (#5340)
This adds the proof rules and proof checker for datatypes.
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 9448e1939..4ba483101 100644 --- a/src/expr/proof_rule.cpp +++ b/src/expr/proof_rule.cpp @@ -114,6 +114,13 @@ const char* toString(PfRule id) 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"; + //================================================= Datatype rules + case PfRule::DT_UNIF: return "DT_UNIF"; + case PfRule::DT_INST: return "DT_INST"; + case PfRule::DT_COLLAPSE: return "DT_COLLAPSE"; + case PfRule::DT_SPLIT: return "DT_SPLIT"; + case PfRule::DT_CLASH: return "DT_CLASH"; + case PfRule::DT_TRUST: return "DT_TRUST"; //================================================= Quantifiers rules case PfRule::WITNESS_INTRO: return "WITNESS_INTRO"; case PfRule::EXISTS_INTRO: return "EXISTS_INTRO"; |