From 1c07b027efc6608892d3081b0e14b9f69cb69238 Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Mon, 19 Sep 2022 21:33:25 -0400
Subject: [PATCH] refactor(const): remove `opaque_to_cc`

---
 src/core-logic/const.ml     | 1 -
 src/core-logic/const.mli    | 1 -
 src/core-logic/types_.ml    | 5 -----
 src/core/default_cc_view.ml | 4 ----
 4 files changed, 11 deletions(-)

diff --git a/src/core-logic/const.ml b/src/core-logic/const.ml
index 0ca300b4..c7004f70 100644
--- a/src/core-logic/const.ml
+++ b/src/core-logic/const.ml
@@ -6,7 +6,6 @@ module type DYN_OPS = sig
   val pp : view Fmt.printer
   val equal : view -> view -> bool
   val hash : view -> int
-  val opaque_to_cc : view -> bool
 end
 
 type ops = (module DYN_OPS)
diff --git a/src/core-logic/const.mli b/src/core-logic/const.mli
index 69fc210d..8fe1838d 100644
--- a/src/core-logic/const.mli
+++ b/src/core-logic/const.mli
@@ -10,7 +10,6 @@ module type DYN_OPS = sig
   val pp : view Fmt.printer
   val equal : view -> view -> bool
   val hash : view -> int
-  val opaque_to_cc : view -> bool
 end
 
 type ops = (module DYN_OPS)
diff --git a/src/core-logic/types_.ml b/src/core-logic/types_.ml
index 79804928..70b445c2 100644
--- a/src/core-logic/types_.ml
+++ b/src/core-logic/types_.ml
@@ -11,11 +11,6 @@ module type DYN_CONST_OPS = sig
 
   val hash : const_view -> int
   (** Hash constant *)
-
-  val opaque_to_cc : const_view -> bool
-  (** If true, congruence closure will not apply for applications of this
-      constant. In other words, [c t1…tn] will appear to the congruence
-      closure as a single opaque term with no subterms. *)
 end
 
 type const_ops = (module DYN_CONST_OPS)
diff --git a/src/core/default_cc_view.ml b/src/core/default_cc_view.ml
index 0e10b00e..e9b4928e 100644
--- a/src/core/default_cc_view.ml
+++ b/src/core/default_cc_view.ml
@@ -9,10 +9,6 @@ let view_as_cc (t : Term.t) : _ CC_view.t =
   | Term.E_const { Const.c_view = T_builtins.C_ite; _ }, [ _ty; a; b; c ] ->
     View.If (a, b, c)
   | Term.E_const { Const.c_view = T_builtins.C_not; _ }, [ a ] -> View.Not a
-  | Term.E_const { Const.c_ops = (module OP); c_view; _ }, _
-    when OP.opaque_to_cc c_view ->
-    (* this constant hides its arguments *)
-    View.Opaque t
   | _ ->
     (match Term.view t with
     | Term.E_app (f, a) -> View.App_ho (f, a)