Use constants for the top and bottom formulae

The `top` and `bottom` are constant but we use closures to define them
because of limitation of the recursive module. This commit refactors the
way we define them. Now, `top` and `bot` are constants exposed by the
module `Shostak.Combine`.

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 () = {
+  let empty = {
     use = Use.empty ;
-    uf = Uf.empty () ;
+    uf = Uf.empty;
     relation = Rel.empty [];
   }
 
@@ -377,9 +377,9 @@ module Main : S = struct
 
   let contra_congruence env facts r =
     Options.exec_thread_yield ();
-    if X.equal (fst (Uf.find_r env.uf r)) (X.top()) then
+    if X.equal (fst (Uf.find_r env.uf r)) X.top then
       new_facts_by_contra_congruence env facts r E.faux
-    else if X.equal (fst (Uf.find_r env.uf r)) (X.bot()) then
+    else if X.equal (fst (Uf.find_r env.uf r)) X.bot then
       new_facts_by_contra_congruence env facts r E.vrai
 
   let congruence_closure env (facts: r Sig_rel.facts) r1 r2 ex =
@@ -576,7 +576,7 @@ module Main : S = struct
       Debug.assume_literal sa;
       let env = match sa with
         | A.Pred (r1,neg) ->
-          let r2, r3 =  if neg then X.bot(), X.top() else X.top(), X.bot() in
+          let r2, r3 =  if neg then X.bot, X.top else X.top, X.bot in
           if X.hash_cmp r1 r2 = 0 then env
           else
             let env = assume_eq env facts r1 r2 ex in

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

@@ -695,7 +695,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/shostak.ml

@@ -34,6 +34,9 @@
 module rec CX : sig
   include Sig.X
 
+  val top : unit -> r
+  val bot : unit -> r
+
   val extract1 : r -> ARITH.t option
   val embed1 : ARITH.t -> r
 
@@ -825,6 +828,8 @@ module Combine = struct
     in
     make, save_cache_aux, reinit_cache_aux
 
+  let top = top ()
+  let bot = bot ()
 end
 
 module Arith = ARITH

src/lib/reasoners/shostak.mli

@@ -28,7 +28,12 @@
 (*                                                                        *)
 (**************************************************************************)
 
-module Combine : Sig.X
+module Combine : sig
+  include Sig.X
+
+  val top : r
+  val bot : r
+end
 
 module Polynome : Polynome.T
   with type r = Combine.r

src/lib/reasoners/sig.mli

@@ -148,9 +148,6 @@ module type X = sig
 
   val abstract_selectors : r -> (r * r) list -> r * (r * r) list
 
-  val top : unit -> r
-  val bot : unit -> r
-
   val is_solvable_theory_symbol : Symbols.t -> Ty.t -> bool
 
   (* the returned bool is true when the returned term in a constant of the

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

@@ -900,7 +900,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 +912,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/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

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