refactor: renaming `Eq{uiv,}_class

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

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

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

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

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 *)