Remove unused equality engine types (#5319)

This is leftover from the old proof infrastructure.

diff --git a/src/theory/uf/equality_engine_types.h b/src/theory/uf/equality_engine_types.h
index a376458a7e49546b5acea10bf707b9644e9d0520..2fdbbffa843763b4e975228e63025e6c21a06e7e 100644 (file)
--- 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;