From b5222fd98d2ae5ee39f1edebe62014a1501f306c Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Tue, 10 Oct 2023 11:41:34 +0200 Subject: [PATCH] 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 | 2 +- src/lib/reasoners/ccx.ml | 8 ++++---- src/lib/reasoners/ccx.mli | 2 +- src/lib/reasoners/intervalCalculus.ml | 2 +- src/lib/reasoners/theory.ml | 7 +++---- src/lib/reasoners/uf.ml | 6 ++---- src/lib/reasoners/uf.mli | 2 +- src/lib/reasoners/x.ml | 4 ++++ src/lib/structures/xliteral.ml | 24 ++++++++++++------------ src/lib/structures/xliteral.mli | 4 ++-- 10 files changed, 31 insertions(+), 30 deletions(-) create mode 100644 src/lib/reasoners/x.ml diff --git a/src/lib/dune b/src/lib/dune index 23c57e936d..259ad44cb7 100644 --- a/src/lib/dune +++ b/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 diff --git a/src/lib/reasoners/ccx.ml b/src/lib/reasoners/ccx.ml index a7d6a71232..2f1e748789 100644 --- a/src/lib/reasoners/ccx.ml +++ b/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 []; } diff --git a/src/lib/reasoners/ccx.mli b/src/lib/reasoners/ccx.mli index e97a9e55c8..37e4b9ced5 100644 --- a/src/lib/reasoners/ccx.mli +++ b/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 diff --git a/src/lib/reasoners/intervalCalculus.ml b/src/lib/reasoners/intervalCalculus.ml index 2ad4c06bab..0920677d04 100644 --- a/src/lib/reasoners/intervalCalculus.ml +++ b/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 diff --git a/src/lib/reasoners/theory.ml b/src/lib/reasoners/theory.ml index c8d65dbb00..7f95a43f31 100644 --- a/src/lib/reasoners/theory.ml +++ b/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 diff --git a/src/lib/reasoners/uf.ml b/src/lib/reasoners/uf.ml index f1d7ddb768..5663665d7a 100644 --- a/src/lib/reasoners/uf.ml +++ b/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 diff --git a/src/lib/reasoners/uf.mli b/src/lib/reasoners/uf.mli index e6e6d7f738..fbe39d00ce 100644 --- a/src/lib/reasoners/uf.mli +++ b/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 diff --git a/src/lib/reasoners/x.ml b/src/lib/reasoners/x.ml new file mode 100644 index 0000000000..d036163f39 --- /dev/null +++ b/src/lib/reasoners/x.ml @@ -0,0 +1,4 @@ +include Shostak.Combine + +let top = top () +let bot = bot () diff --git a/src/lib/structures/xliteral.ml b/src/lib/structures/xliteral.ml index 4f2871a1e4..cbfd459610 100644 --- a/src/lib/structures/xliteral.ml +++ b/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 diff --git a/src/lib/structures/xliteral.mli b/src/lib/structures/xliteral.mli index ccb1734636..84d5f46ecd 100644 --- a/src/lib/structures/xliteral.mli +++ b/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