From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 22 Oct 2020 17:24:53 +0000 (-0500)
Subject: Remove unused equality engine types (#5319)
X-Git-Tag: cvc5-1.0.0~2669
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d758a32f5bb1361d766a71c3d2cdaeacb8f39a76;p=cvc5.git

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 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;