The environments of CC(X) and UF(X) are constant

This PR makes clear that the environments of both CC(X) and UF(X) are
constant. The previous signature of the constructors for these environments
was `unit -> t` and not `t` only because they use the `top` and
`bot` semantic values. As the module Combine in `Shostak` cannot contain
constants because of limitations with recursive module in OCaml, we have
put these constants in a trivial closure.

I create a new module X which is an alias of `Shostak.Combine` and
contains the constants `top` and `bot`.

Note: I don't remove all the aliases `module X = Shostak.Combine` in many
modules of AE. We can do it gradually and modifying all the files will
be painful while rebasing our current PRs.

Note: I cannot turn the environment of Theory into a constant because
this environment uses mutable states to enqueue facts. I plan to
fix that in another PR (probably by writing a module for functional
queues but I have to check how the current environment behaves while
backtracking).

src/lib/dune

@@ -40,7 +40,7 @@
     Fun_sat Inequalities Bitv_rel Th_util Adt Adt_rel
     Instances IntervalCalculus Intervals Ite_rel Ite Matching Matching_types
     Polynome Records Records_rel Satml_frontend_hybrid Satml_frontend Satml
-    Sat_solver Sat_solver_sig Sig Sig_rel Theory Uf Use
+    Sat_solver Sat_solver_sig Sig Sig_rel Theory Uf Use X
     ; structures
     Commands Errors Explanation Fpa_rounding
     Parsed Profiling Satml_types Symbols

src/lib/reasoners/ccx.ml

@@ -41,7 +41,7 @@ module type S = sig
   type t
   type r = Shostak.Combine.r
 
-  val empty : unit -> t
+  val empty : t
 
   val empty_facts : unit -> r Sig_rel.facts
 
@@ -107,9 +107,9 @@ module Main : S = struct
 
   type r = Shostak.Combine.r
 
-  let empty () = {
-    use = Use.empty ;
-    uf = Uf.empty () ;
+  let empty = {
+    use = Use.empty;
+    uf = Uf.empty;
     relation = Rel.empty [];
   }
 

src/lib/reasoners/ccx.mli

@@ -33,7 +33,7 @@ module type S = sig
   type t
   type r = Shostak.Combine.r
 
-  val empty : unit -> t
+  val empty : t
 
   val empty_facts : unit -> r Sig_rel.facts
 

src/lib/reasoners/intervalCalculus.ml

@@ -665,7 +665,7 @@ let empty classes = {
   improved_x = SX.empty ;
   classes = classes;
   size_splits = Q.one;
-  new_uf = Uf.empty ();
+  new_uf = Uf.empty;
 
   rat_sim =
     Sim.Solve.solve

src/lib/reasoners/theory.ml

@@ -712,7 +712,7 @@ module Main_Default : S = struct
     else {env with gamma=gm; gamma_finite=add_term_in_gm env.gamma_finite t}
 
   let empty () =
-    let env = CC_X.empty () in
+    let env = CC_X.empty in
     let env, _ = CC_X.add_term env (CC_X.empty_facts()) E.vrai Ex.empty in
     let env, _ = CC_X.add_term env (CC_X.empty_facts()) E.faux Ex.empty in
     let t =
@@ -798,9 +798,8 @@ module Main_Empty : S = struct
   let cl_extract _ = []
   let extract_ground_terms _ = Expr.Set.empty
 
-  let empty_ccx = CC_X.empty ()
-  let get_real_env _ = empty_ccx
-  let get_case_split_env _ = empty_ccx
+  let get_real_env _ = CC_X.empty
+  let get_case_split_env _ = CC_X.empty
   let do_case_split env _ = env, E.Set.empty
   let add_term env _ ~add_in_cs:_ = env
   let compute_concrete_model _env = None

src/lib/reasoners/uf.ml

@@ -28,8 +28,6 @@
 (*                                                                        *)
 (**************************************************************************)
 
-module X = Shostak.Combine
-
 module Ac = Shostak.Ac
 module Ex = Explanation
 
@@ -900,7 +898,7 @@ let term_repr uf t =
   try SE.min_elt st
   with Not_found -> t
 
-let empty () =
+let empty =
   let env = {
     make  = ME.empty;
     repr = MapX.empty;
@@ -912,7 +910,7 @@ let empty () =
   in
   let env, _ = add env E.vrai in
   let env, _ = add env E.faux in
-  distinct env [X.top (); X.bot ()] Ex.empty
+  distinct env [X.top; X.bot] Ex.empty
 
 let make uf t = ME.find t uf.make
 

src/lib/reasoners/uf.mli

@@ -36,7 +36,7 @@ type r = Shostak.Combine.r
 
 module LX : Xliteral.S with type elt = r
 
-val empty : unit -> t
+val empty : t
 val add : t -> Expr.t -> t * Expr.t list
 
 val mem : t -> Expr.t -> bool

src/lib/reasoners/x.ml

@@ -0,0 +1,4 @@
+include Shostak.Combine
+
+let top = top ()
+let bot = bot ()

src/lib/structures/xliteral.ml

@@ -49,8 +49,8 @@ module type OrderedType = sig
   val compare : t -> t -> int
   val hash :  t -> int
   val print : Format.formatter -> t -> unit
-  val top : unit -> t
-  val bot : unit -> t
+  val top : t
+  val bot : t
   val type_info : t -> Ty.t
 end
 
@@ -231,16 +231,16 @@ module Make (X : OrderedType) : S with type elt = X.t = struct
   module HC = Hconsing.Make(V)
 
   let normalize_eq_bool t1 t2 is_neg =
-    if X.compare t1 (X.bot()) = 0 then Pred(t2, not is_neg)
-    else if X.compare t2 (X.bot()) = 0 then Pred(t1, not is_neg)
-    else if X.compare t1 (X.top()) = 0 then Pred(t2, is_neg)
-    else if X.compare t2 (X.top()) = 0 then Pred(t1, is_neg)
+    if X.compare t1 (X.bot) = 0 then Pred(t2, not is_neg)
+    else if X.compare t2 (X.bot) = 0 then Pred(t1, not is_neg)
+    else if X.compare t1 (X.top) = 0 then Pred(t2, is_neg)
+    else if X.compare t2 (X.top) = 0 then Pred(t1, is_neg)
     else if is_neg then Distinct (false, [t1;t2]) (* XXX assert ? *)
     else Eq(t1,t2) (* should be translated into iff *)
 
   let normalize_eq t1 t2 is_neg =
     let c = X.compare t1 t2 in
-    if c = 0 then Pred(X.top(), is_neg)
+    if c = 0 then Pred(X.top, is_neg)
     else
       let t1, t2 = if c < 0 then t1, t2 else t2, t1 in
       if X.type_info t1 == Ty.Tbool then normalize_eq_bool t1 t2 is_neg
@@ -273,15 +273,15 @@ module Make (X : OrderedType) : S with type elt = X.t = struct
 
   (*
     let mk_eq_bool t1 t2 is_neg =
-    if X.compare t1 (X.bot()) = 0 then make_aux (PR t2) (not is_neg)
-    else if X.compare t2 (X.bot()) = 0 then make_aux (PR t1) (not is_neg)
-    else if X.compare t1 (X.top()) = 0 then make_aux (PR t2) is_neg
-    else if X.compare t2 (X.top()) = 0 then make_aux (PR t1) is_neg
+    if X.compare t1 (X.bot) = 0 then make_aux (PR t2) (not is_neg)
+    else if X.compare t2 (X.bot) = 0 then make_aux (PR t1) (not is_neg)
+    else if X.compare t1 (X.top) = 0 then make_aux (PR t2) is_neg
+    else if X.compare t2 (X.top) = 0 then make_aux (PR t1) is_neg
     else make_aux (EQ(t1,t2)) is_neg
 
     let mk_equa t1 t2 is_neg =
     let c = X.compare t1 t2 in
-    if c = 0 then make_aux (PR (X.top())) is_neg
+    if c = 0 then make_aux (PR (X.top)) is_neg
     else
     let t1, t2 = if c < 0 then t1, t2 else t2, t1 in
     if X.type_info t1 = Ty.Tbool then mk_eq_bool t1 t2 is_neg

src/lib/structures/xliteral.mli

@@ -52,8 +52,8 @@ module type OrderedType = sig
   val compare : t -> t -> int
   val hash :  t -> int
   val print : Format.formatter -> t -> unit
-  val top : unit -> t
-  val bot : unit -> t
+  val top : t
+  val bot : t
   val type_info : t -> Ty.t
 end