[refactor] Always represent classes as sets (#721)

Most representations of UF classes uses Expr.Set.t, but `class_of`
specifically converts the class to a list. There doesn't seem to be any
real reason for that, and it simply causes a bit of memory overhead by
creating the list instead of iterating over the expression set directly.

This patch is a first step towards abstracting the representation of UF
classes by using a common type for all their representations. It is not
entirely trivial to abstract the representation, because of cyclic
dependencies with `Explanation.Inconsistent`.

src/lib/reasoners/arrays_rel.ml

@@ -229,8 +229,8 @@ let update_env are_eq are_dist dep env acc gi si p p_ded n n_ded =
   ---------------------------------------------------------------------*)
 let get_of_set are_eq are_dist gtype (env,acc) class_of =
   let {g=get; gt=gtab; gi=gi; gty=gty} = gtype in
-  L.fold_left
-    (fun (env,acc) set ->
+  E.Set.fold
+    (fun set (env,acc) ->
        if Tmap.splited get set env.seen then (env,acc)
        else
          let env = {env with seen = Tmap.update get set env.seen} in
@@ -253,16 +253,16 @@ let get_of_set are_eq are_dist gtype (env,acc) class_of =
            update_env
              are_eq are_dist dep env acc gi si p p_ded n n_ded
          | _ -> (env,acc)
-    ) (env,acc) (class_of gtab)
+    ) (class_of gtab) (env,acc)
 
 (*----------------------------------------------------------------------
   set(-,-,-) modulo egalite
   ---------------------------------------------------------------------*)
 let get_from_set _are_eq _are_dist stype (env,acc) class_of =
   let sets =
-    L.fold_left
-      (fun acc t -> S.union acc (TBS.find t env.tbset))
-      (S.singleton stype) (class_of stype.st)
+    E.Set.fold
+      (fun t acc -> S.union acc (TBS.find t env.tbset))
+      (class_of stype.st) (S.singleton stype)
   in
 
   S.fold (fun { s = set; si = si; sv = sv; _ } (env,acc) ->
@@ -285,9 +285,9 @@ let get_and_set are_eq are_dist gtype (env,acc) class_of =
   let {g=get; gt=gtab; gi=gi; gty=gty} = gtype in
 
   let suff_sets =
-    L.fold_left
-      (fun acc t -> S.union acc (TBS.find t env.tbset))
-      S.empty (class_of gtab)
+    E.Set.fold
+      (fun t acc -> S.union acc (TBS.find t env.tbset))
+      (class_of gtab) S.empty
   in
   S.fold
     (fun  {s=set; st=stab; si=si; sv=sv; _ } (env,acc) ->

src/lib/reasoners/ccx.ml

@@ -71,7 +71,7 @@ module type S = sig
     (r Xliteral.view * bool * Th_util.lit_origin) list * t
   val query :  t -> E.t -> Th_util.answer
   val new_terms : t -> Expr.Set.t
-  val class_of : t -> Expr.t -> Expr.t list
+  val class_of : t -> Expr.t -> Expr.Set.t
   val are_equal : t -> Expr.t -> Expr.t -> init_terms:bool -> Th_util.answer
   val are_distinct : t -> Expr.t -> Expr.t -> Th_util.answer
   val cl_extract : t -> Expr.Set.t list
@@ -341,7 +341,7 @@ module Main : S = struct
       match E.term_view t1 with
       | { E.f = f1; xs = [x]; _ } ->
         let ty_x = Expr.type_info x in
-        List.iter
+        E.Set.iter
           (fun t2 ->
              match E.term_view t2 with
              | { E.f = f2 ; xs = [y]; _ } when Sy.equal f1 f2 ->

src/lib/reasoners/ccx.mli

@@ -63,7 +63,7 @@ module type S = sig
     (r Xliteral.view * bool * Th_util.lit_origin) list * t
   val query :  t -> Expr.t -> Th_util.answer
   val new_terms : t -> Expr.Set.t
-  val class_of : t -> Expr.t -> Expr.t list
+  val class_of : t -> Expr.t -> Expr.Set.t
   val are_equal : t -> Expr.t -> Expr.t -> init_terms:bool -> Th_util.answer
   val are_distinct : t -> Expr.t -> Expr.t -> Th_util.answer
   val cl_extract : t -> Expr.Set.t list

src/lib/reasoners/matching.ml

@@ -62,7 +62,7 @@ module type Arg = sig
   type t
   val term_repr : t -> E.t -> init_term:bool -> E.t
   val are_equal : t -> E.t -> E.t -> init_terms:bool -> Th_util.answer
-  val class_of : t -> E.t -> E.t list
+  val class_of : t -> E.t -> E.Set.t
 end
 
 module Make (X : Arg) : S with type theory = X.t = struct
@@ -161,7 +161,7 @@ module Make (X : Arg) : S with type theory = X.t = struct
           ~module_name:"Matching" ~function_name:"match_class_of"
           "class_of (%a) = { %a }"
           E.print t
-          (fun fmt -> List.iter (Format.fprintf fmt "%a , " E.print)) cl
+          (fun fmt -> E.Set.iter (Format.fprintf fmt "%a , " E.print)) cl
 
     let candidate_substitutions pat_info res =
       let open Matching_types in
@@ -404,13 +404,13 @@ module Make (X : Arg) : S with type theory = X.t = struct
            are_equal_light tbox pat t != None then
           [gsb]
         else
-          let cl = if mconf.Util.no_ematching then [t]
+          let cl = if mconf.Util.no_ematching then E.Set.singleton t
             else X.class_of tbox t
           in
           Debug.match_class_of t cl;
           let cl =
-            List.fold_left
-              (fun l t ->
+            E.Set.fold
+              (fun t l ->
                  let { E.f = f; xs = xs; ty = ty; _ } = E.term_view t in
                  if Symbols.compare f_pat f = 0 then xs::l
                  else
@@ -420,7 +420,7 @@ module Make (X : Arg) : S with type theory = X.t = struct
                        (xs_modulo_records t record) :: l
                      | _ -> l
                    end
-              )[] cl
+              ) cl []
           in
           let cl = filter_classes mconf cl tbox in
           let cl =

src/lib/reasoners/matching.mli

@@ -60,7 +60,7 @@ module type Arg = sig
   type t
   val term_repr : t -> Expr.t -> init_term:bool -> Expr.t
   val are_equal : t -> Expr.t -> Expr.t -> init_terms:bool -> Th_util.answer
-  val class_of : t -> Expr.t -> Expr.t list
+  val class_of : t -> Expr.t -> Expr.Set.t
 end
 
 

src/lib/reasoners/uf.ml

@@ -900,8 +900,6 @@ let term_repr uf t =
   try SE.min_elt st
   with Not_found -> t
 
-let class_of env t = SE.elements (class_of env t)
-
 let empty () =
   let env = {
     make  = ME.empty;

src/lib/reasoners/uf.mli

@@ -55,7 +55,7 @@ val are_equal : t -> Expr.t -> Expr.t -> added_terms:bool -> Th_util.answer
 val are_distinct : t -> Expr.t -> Expr.t -> Th_util.answer
 val already_distinct : t -> r list -> bool
 
-val class_of : t -> Expr.t -> Expr.t list
+val class_of : t -> Expr.t -> Expr.Set.t
 val rclass_of : t -> r -> Expr.Set.t
 
 val cl_extract : t -> Expr.Set.t list