diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-10-22 12:24:53 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-10-22 12:24:53 -0500 |
| commit | d758a32f5bb1361d766a71c3d2cdaeacb8f39a76 (patch) | |
| tree | 6b4e3d94766f4e8cb8a120ca5867fcb54ff6b329 | |
| parent | e09c7d12441e55fe942ae573b49b880431cf1af1 (diff) | |
Remove unused equality engine types (#5319)
This is leftover from the old proof infrastructure.
| -rw-r--r-- | src/theory/uf/equality_engine_types.h | 11 |
1 files changed, 0 insertions, 11 deletions
diff --git a/src/theory/uf/equality_engine_types.h b/src/theory/uf/equality_engine_types.h index a376458a7..2fdbbffa8 100644 --- a/src/theory/uf/equality_engine_types.h +++ b/src/theory/uf/equality_engine_types.h @@ -75,14 +75,6 @@ enum MergeReasonType MERGED_THROUGH_CONSTANTS, /** Terms were merged due to transitivity */ MERGED_THROUGH_TRANS, - // TEMPORARY RULES WHILE WE DON'T MIGRATE TO PROOF_NEW - - /** Terms were merged due to arrays read-over-write */ - MERGED_THROUGH_ROW, - /** Terms were merged due to arrays read-over-write (1) */ - MERGED_THROUGH_ROW1, - /** Terms were merged due to extensionality */ - MERGED_THROUGH_EXT, }; inline std::ostream& operator << (std::ostream& out, MergeReasonType reason) { @@ -100,9 +92,6 @@ inline std::ostream& operator << (std::ostream& out, MergeReasonType reason) { case MERGED_THROUGH_TRANS: out << "transitivity"; break; - case MERGED_THROUGH_ROW: out << "read-over-write"; break; - case MERGED_THROUGH_ROW1: out << "read-over-write (1)"; break; - case MERGED_THROUGH_EXT: out << "extensionality"; break; default: out << "[theory]"; break; |