From 40186a6c76e278f5d78c1f320dec6f9e761948e1 Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Fri, 8 Feb 2019 19:45:20 -0600
Subject: [PATCH] refactor: renaming `Eq{uiv,}_class

---
 src/smt/Congruence_closure.ml             | 2 +-
 src/smt/Congruence_closure.mli            | 4 ++--
 src/smt/{Equiv_class.ml => Eq_class.ml}   | 0
 src/smt/{Equiv_class.mli => Eq_class.mli} | 0
 src/smt/Sidekick_smt.ml                   | 2 +-
 src/smt/Theory.ml                         | 6 +++---
 src/smt/Theory_combine.ml                 | 4 ++--
 7 files changed, 9 insertions(+), 9 deletions(-)
 rename src/smt/{Equiv_class.ml => Eq_class.ml} (100%)
 rename src/smt/{Equiv_class.mli => Eq_class.mli} (100%)

diff --git a/src/smt/Congruence_closure.ml b/src/smt/Congruence_closure.ml
index a32cb764..37fbbc46 100644
--- a/src/smt/Congruence_closure.ml
+++ b/src/smt/Congruence_closure.ml
@@ -1,7 +1,7 @@
 
 open Solver_types
 
-module N = Equiv_class
+module N = Eq_class
 
 type node = N.t
 type repr = N.t
diff --git a/src/smt/Congruence_closure.mli b/src/smt/Congruence_closure.mli
index 272bb040..73c9892d 100644
--- a/src/smt/Congruence_closure.mli
+++ b/src/smt/Congruence_closure.mli
@@ -5,10 +5,10 @@ open Solver_types
 type t
 (** Global state of the congruence closure *)
 
-type node = Equiv_class.t
+type node = Eq_class.t
 (** Node in the congruence closure *)
 
-type repr = Equiv_class.t
+type repr = Eq_class.t
 (** Node that is currently a representative *)
 
 type conflict = Theory.conflict
diff --git a/src/smt/Equiv_class.ml b/src/smt/Eq_class.ml
similarity index 100%
rename from src/smt/Equiv_class.ml
rename to src/smt/Eq_class.ml
diff --git a/src/smt/Equiv_class.mli b/src/smt/Eq_class.mli
similarity index 100%
rename from src/smt/Equiv_class.mli
rename to src/smt/Eq_class.mli
diff --git a/src/smt/Sidekick_smt.ml b/src/smt/Sidekick_smt.ml
index efcd33ad..efb513cc 100644
--- a/src/smt/Sidekick_smt.ml
+++ b/src/smt/Sidekick_smt.ml
@@ -9,7 +9,7 @@ module Term = Term
 module Value = Value
 module Term_cell = Term_cell
 module Ty = Ty
-module Equiv_class = Equiv_class
+module Eq_class = Eq_class
 module Lit = Lit
 module Explanation = Explanation
 module Congruence_closure = Congruence_closure
diff --git a/src/smt/Theory.ml b/src/smt/Theory.ml
index ad9378ad..f165bc7e 100644
--- a/src/smt/Theory.ml
+++ b/src/smt/Theory.ml
@@ -41,10 +41,10 @@ module type ACTIONS = sig
   (** Add toplevel clause to the SAT solver. This clause will
       not be backtracked. *)
 
-  val find: Term.t -> Equiv_class.t
+  val find: Term.t -> Eq_class.t
   (** Find representative of this term *)
 
-  val all_classes: Equiv_class.t Sequence.t
+  val all_classes: Eq_class.t Sequence.t
   (** All current equivalence classes
       (caution: linear in the number of terms existing in the solver) *)
 end
@@ -60,7 +60,7 @@ module type S = sig
   val create : Term.state -> t
   (** Instantiate the theory's state *)
 
-  val on_merge: t -> actions -> Equiv_class.t -> Equiv_class.t -> Explanation.t -> unit
+  val on_merge: t -> actions -> Eq_class.t -> Eq_class.t -> Explanation.t -> unit
   (** Called when two classes are merged *)
 
   val partial_check : t -> actions -> Lit.t Sequence.t -> unit
diff --git a/src/smt/Theory_combine.ml b/src/smt/Theory_combine.ml
index ce66f756..faff92db 100644
--- a/src/smt/Theory_combine.ml
+++ b/src/smt/Theory_combine.ml
@@ -28,7 +28,7 @@ type t = {
   (** congruence closure *)
   mutable theories : theory_state list;
   (** Set of theories *)
-  new_merges: (Equiv_class.t * Equiv_class.t * explanation) Vec.t;
+  new_merges: (Eq_class.t * Eq_class.t * explanation) Vec.t;
 }
 
 let[@inline] cc (t:t) = Lazy.force t.cc
@@ -86,7 +86,7 @@ let add_formula (self:t) (lit:Lit.t) =
   let t = Lit.view lit in
   let lazy cc = self.cc in
   let n = C_clos.add cc t in
-  Equiv_class.set_field Equiv_class.field_is_literal true n;
+  Eq_class.set_field Eq_class.field_is_literal true n;
   ()
 
 (* propagation from the bool solver *)