From 63937f1bed61edaebc19d88dc931463af5bd180a Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Tue, 9 Jul 2024 15:59:55 +0200 Subject: [PATCH] review changes --- src/lib/frontend/d_cnf.ml | 4 +- src/lib/reasoners/adt_rel.ml | 79 ++++++++++++------------------ src/lib/structures/fpa_rounding.ml | 5 +- src/lib/structures/ty.ml | 9 ++-- src/lib/structures/uid.ml | 30 +++--------- src/lib/structures/uid.mli | 22 ++------- src/lib/util/nest.ml | 32 ++---------- src/lib/util/nest.mli | 5 +- 8 files changed, 54 insertions(+), 132 deletions(-) diff --git a/src/lib/frontend/d_cnf.ml b/src/lib/frontend/d_cnf.ml index c099923ea..05ed3c858 100644 --- a/src/lib/frontend/d_cnf.ml +++ b/src/lib/frontend/d_cnf.ml @@ -612,7 +612,7 @@ let mk_ty_decl (ty_c: DE.ty_cst) = | Some (Adt { cases; _ } as adt) -> let uid = Uid.of_ty_cst ty_c in - List.iter (fun (i, h) -> Uid.set_hash i h) @@ Nest.generate [adt]; + Nest.attach_orders [adt]; let tyvl = Cache.store_ty_vars_ret cases.(0).cstr.id_ty in Cache.store_ty ty_c (Ty.t_adt uid tyvl); let rev_cs = @@ -729,7 +729,7 @@ let mk_mr_ty_decls (tdl: DE.ty_cst list) = assert false ) ([], false) tdl in - List.iter (fun (i, h) -> Uid.set_hash i h) @@ Nest.generate rev_tdefs; + Nest.attach_orders rev_tdefs; let rev_l = List.fold_left ( fun acc tdef -> diff --git a/src/lib/reasoners/adt_rel.ml b/src/lib/reasoners/adt_rel.ml index cae6b1a80..213c1523d 100644 --- a/src/lib/reasoners/adt_rel.ml +++ b/src/lib/reasoners/adt_rel.ml @@ -39,31 +39,19 @@ module SLR = Set.Make(LR) module DE = Dolmen.Std.Expr module DT = Dolmen.Std.Expr.Ty module B = Dolmen.Std.Builtin -module TSet = Set.Make (Int) -let timer = Timers.M_Adt +module TSet = + Set.Make + (struct + type t = Uid.t -(* HACK: this wrapper around [Uid.get_hash] is a temporary hack - used by the legacy frontend only. For the legacy frontend, we generate a - trivial perfect hash for the type [ty], that is a hash whose the associated - order does not ensure the termination of the model generation. *) -let get_hash ty = - match ty with - | Ty.Tadt (name, params) -> - let cases = Ty.type_body name params in - begin match name with - | Ty_cst _ -> - Uid.get_hash name + (* We use a dedicated total order on the constructors to ensure + the termination of model generation. *) + let compare id1 id2 = + Uid.perfect_hash id1 - Uid.perfect_hash id2 + end) - | Hstring _ -> - let cstrs = List.map (fun Ty.{ constr; _ } -> constr) cases in - let of_int = List.nth cstrs in - let to_int id = Option.get @@ Lists.find_index (Uid.equal id) cstrs in - Uid.{ to_int; of_int } - - | _ -> assert false - end - | _ -> assert false +let timer = Timers.M_Adt module Domain = struct (* Set of possible constructors. The explanation justifies that any value @@ -71,7 +59,6 @@ module Domain = struct domain. *) type t = { constrs : TSet.t; - hash : Uid.hash; ex : Ex.t; } @@ -79,25 +66,25 @@ module Domain = struct let[@inline always] cardinal { constrs; _ } = TSet.cardinal constrs - let[@inline always] choose { constrs; hash; _ } = + let[@inline always] choose { constrs; _ } = (* We choose the minimal element to ensure the termination of model generation. *) - TSet.min_elt constrs |> hash.of_int + TSet.min_elt constrs - let[@inline always] as_singleton { constrs; hash; ex; _ } = + let[@inline always] as_singleton { constrs; ex } = if TSet.cardinal constrs = 1 then - Some (TSet.choose constrs |> hash.of_int, ex) + Some (TSet.choose constrs, ex) else None - let domain ~constrs hash ex = + let domain ~constrs ex = if TSet.is_empty constrs then raise @@ Inconsistent ex else - { constrs; hash; ex } + { constrs; ex } - let[@inline always] singleton ~ex hash c = - { constrs = TSet.singleton (hash.Uid.to_int c); hash; ex } + let[@inline always] singleton ~ex c = + { constrs = TSet.singleton c; ex } let[@inline always] subset d1 d2 = TSet.subset d1.constrs d2.constrs @@ -106,15 +93,14 @@ module Domain = struct | Ty.Tadt (name, params) -> (* Return the list of all the constructors of the type of [r]. *) let cases = Ty.type_body name params in - let hash = get_hash ty in let constrs = List.fold_left (fun acc Ty.{ constr; _ } -> - TSet.add (hash.to_int constr) acc + TSet.add constr acc ) TSet.empty cases in assert (not @@ TSet.is_empty constrs); - { constrs; hash; ex = Ex.empty } + { constrs; ex = Ex.empty } | _ -> (* Only ADT values can have a domain. This case shouldn't happen since we check the type of semantic values in both [add] and [assume]. *) @@ -122,27 +108,23 @@ module Domain = struct let equal d1 d2 = TSet.equal d1.constrs d2.constrs - let pp_cstr of_int ppf i = - Uid.pp ppf @@ of_int i - let pp ppf d = Fmt.(braces @@ - iter ~sep:comma TSet.iter (pp_cstr d.hash.Uid.of_int)) ppf d.constrs; + iter ~sep:comma TSet.iter Uid.pp) ppf d.constrs; if Options.(get_verbose () || get_unsat_core ()) then Fmt.pf ppf " %a" (Fmt.box Ex.print) d.ex let intersect ~ex d1 d2 = let constrs = TSet.inter d1.constrs d2.constrs in let ex = ex |> Ex.union d1.ex |> Ex.union d2.ex in - domain ~constrs d1.hash ex + domain ~constrs ex - let remove ~ex c { constrs; hash; ex = ex' } = - let constrs = TSet.remove (hash.to_int c) constrs in - let ex = Ex.union ex' ex in - domain ~constrs hash ex + let remove ~ex c d = + let constrs = TSet.remove c d.constrs in + let ex = Ex.union ex d.ex in + domain ~constrs ex - let for_all f { constrs; hash; _ } = - TSet.for_all (fun c -> f @@ hash.of_int c) constrs + let for_all f { constrs; _ } = TSet.for_all f constrs end let is_adt_ty = function @@ -207,11 +189,10 @@ module Domains = struct let get r t = match Th.embed r with - | Constr { c_name; c_ty; _ } -> + | Constr { c_name; _ } -> (* For sake of efficiency, we don't look in the map if the semantic value is a constructor. *) - let hash = get_hash c_ty in - Domain.singleton ~ex:Explanation.empty hash c_name + Domain.singleton ~ex:Explanation.empty c_name | _ -> try MX.find r t.domains with Not_found -> @@ -436,7 +417,7 @@ let assume_distinct = cannot be an application of the constructor [c]. *) let assume_is_constr ~ex r c domains = let d1 = Domains.get r domains in - let d2 = Domain.singleton ~ex:Explanation.empty d1.hash c in + let d2 = Domain.singleton ~ex:Explanation.empty c in let nd = Domain.intersect ~ex d1 d2 in Domains.tighten r nd domains diff --git a/src/lib/structures/fpa_rounding.ml b/src/lib/structures/fpa_rounding.ml index b2341f3dc..754839ae8 100644 --- a/src/lib/structures/fpa_rounding.ml +++ b/src/lib/structures/fpa_rounding.ml @@ -95,10 +95,7 @@ let fpa_rounding_mode_dty, d_cstrs, fpa_rounding_mode = let _, d_cstrs = DE.Term.define_adt ty_cst [] cstrs in let () = match DStd.Expr.Ty.definition ty_cst with - | Some def -> - let name, hash = Nest.generate [def] |> List.hd in - Uid.set_hash name hash - + | Some def -> Nest.attach_orders [def] | None -> assert false in let body = diff --git a/src/lib/structures/ty.ml b/src/lib/structures/ty.ml index 018cff950..39424257f 100644 --- a/src/lib/structures/ty.ml +++ b/src/lib/structures/ty.ml @@ -536,17 +536,14 @@ let t_adt ?(body=None) s ty_vars = module DE = Dolmen.Std.Expr let tunit = - let name = + let () = match Dolmen.Std.Expr.Ty.definition DE.Ty.Const.unit with - | Some def -> - let name, hash = Nest.generate [def] |> List.hd in - Uid.set_hash name hash; - name + | Some def -> Nest.attach_orders [def] | None -> assert false in let void = Uid.of_term_cst DE.Term.Cstr.void in let body = Some [void, []] in - let ty = t_adt ~body name [] in + let ty = t_adt ~body (Uid.of_ty_cst DE.Ty.Const.unit) [] in ty let trecord ?(sort_fields = false) ~record_constr lv name lbs = diff --git a/src/lib/structures/uid.ml b/src/lib/structures/uid.ml index 99a503c61..0d594d039 100644 --- a/src/lib/structures/uid.ml +++ b/src/lib/structures/uid.ml @@ -34,18 +34,6 @@ type t = | Term_cst : DE.term_cst -> t | Ty_cst : DE.ty_cst -> t -type hash = { - to_int : t -> int; - (** Return a perfect hash for the constructor. This hash is between [0] - and [n] where [n] is the number of constructors of the ADT. *) - - of_int : int -> t; - (** Return the associated constructor to the integer. - - @raises Invalid_argument if the integer does not correspond to - a constructor of this ADT. *) -} - let[@inline always] of_dolmen id = Dolmen id let[@inline always] of_term_cst id = Term_cst id let[@inline always] of_ty_cst id = Ty_cst id @@ -87,19 +75,15 @@ let compare u1 u2 = | Ty_cst id1, Ty_cst id2 -> DE.Id.compare id1 id2 | _ -> String.compare (show u1) (show u2) -let hash_tag : hash DStd.Tag.t = DStd.Tag.create () - -let set_hash id hash = - match id with - | Ty_cst ty_c -> - DE.Ty.Const.set_tag ty_c hash_tag hash - | _ -> Fmt.invalid_arg "set_hash %a" pp id +let order_tag : int DStd.Tag.t = DStd.Tag.create () -let get_hash id = +let perfect_hash id = match id with - | Ty_cst ty_c -> - Option.get @@ DE.Ty.Const.get_tag ty_c hash_tag - | _ -> Fmt.invalid_arg "get_hash %a" pp id + | Term_cst id -> + Option.get @@ DE.Term.Const.get_tag id order_tag + | Hstring hs -> + Hstring.hash hs + | _ -> assert false module Set = Set.Make (struct diff --git a/src/lib/structures/uid.mli b/src/lib/structures/uid.mli index f308db982..45553fcf1 100644 --- a/src/lib/structures/uid.mli +++ b/src/lib/structures/uid.mli @@ -33,19 +33,6 @@ type t = private | Term_cst : DE.term_cst -> t | Ty_cst : DE.ty_cst -> t -type hash = { - to_int : t -> int; - (** Return a hash for the constructor. This hash is between [0] and [n] - exclusive where [n] is the number of constructors of the ADT. *) - - of_int : int -> t; - (** Return the associated constructor to the integer. - - @raises Invalid_argument if the integer does not correspond to - a constructor of this ADT. *) -} -(** Minimal perfect hash function for the constructors of an ADT. *) - val of_dolmen : 'a DE.Id.t -> t val of_term_cst : DE.term_cst -> t val of_ty_cst : DE.ty_cst -> t @@ -54,15 +41,16 @@ val of_hstring : Hstring.t -> t val to_term_cst : t -> DE.term_cst +val order_tag : int Dolmen.Std.Tag.t +(** Tag used to attach the order of constructor. Used to + retrieve efficiency the order of the constructor in [to_int]. *) + +val perfect_hash : t -> int val hash : t -> int val pp : t Fmt.t val show : t -> string val equal : t -> t -> bool val compare : t -> t -> int -val hash_tag : hash DE.Tags.t -val set_hash : t -> hash -> unit -val get_hash : t -> hash - module Set : Set.S with type elt = t module Map : Map.S with type key = t diff --git a/src/lib/util/nest.ml b/src/lib/util/nest.ml index ccab7bf0a..fa80dfbc2 100644 --- a/src/lib/util/nest.ml +++ b/src/lib/util/nest.ml @@ -137,10 +137,6 @@ let build_graph (defs : DE.ty_def list) : Hp.t = ) defs; hp -(* Tag used to attach the order of constructor. Used to - retrieve efficiency the order of the constructor in [to_int]. *) -let order_tag : int DStd.Tag.t = DStd.Tag.create () - module H = struct include Hashtbl.Make (DE.Ty.Const) @@ -150,27 +146,6 @@ module H = struct add t ty (len + 1, cstr :: cstrs); len | exception Not_found -> add t ty (1, [cstr]); 0 - - let to_hash t = - fold - (fun ty (_, cstrs) acc -> - let cstrs = Array.of_list cstrs in - let of_int = - let len = Array.length cstrs - in fun i -> - if i < 0 || i > len then - invalid_arg "hash" - else Array.unsafe_get cstrs (len-1-i) |> Uid.of_term_cst - in - let to_int cstr = - let d_cstr = Uid.to_term_cst cstr in - match DE.Term.Const.get_tag d_cstr order_tag with - | Some i -> i - | None -> - Fmt.failwith "the constructor %a has no order" DE.Id.print d_cstr - in - (Uid.of_ty_cst ty, Uid.{ to_int; of_int }) :: acc - ) t [] end let ty_cst_of_cstr DE.{ builtin; _ } = @@ -178,7 +153,7 @@ let ty_cst_of_cstr DE.{ builtin; _ } = | B.Constructor { adt; _ } -> adt | _ -> Fmt.failwith "expect an ADT constructor" -let generate defs = +let attach_orders defs = let hp = build_graph defs in let r : (int * DE.term_cst list) H.t = H.create 17 in while not @@ Hp.is_empty hp do @@ -187,7 +162,7 @@ let generate defs = let { id; outgoing; in_degree; _ } = Hp.pop_min hp in let ty = ty_cst_of_cstr id in let o = H.add_cstr r ty id in - DE.Term.Const.set_tag id order_tag o; + DE.Term.Const.set_tag id Uid.order_tag o; assert (in_degree = 0); List.iter (fun node -> @@ -197,5 +172,4 @@ let generate defs = Hp.insert hp node ) !outgoing; outgoing := []; - done; - H.to_hash r + done diff --git a/src/lib/util/nest.mli b/src/lib/util/nest.mli index 84ba660b0..a466903f3 100644 --- a/src/lib/util/nest.mli +++ b/src/lib/util/nest.mli @@ -28,8 +28,9 @@ module DE = Dolmen.Std.Expr number of constructors. The total order on ADT constructors is given by the hash function. *) -val generate : DE.ty_def list -> (Uid.t * Uid.hash) list -(** [generate defs] generate minimal perfect hashes for each ADT of [defs]. +val attach_orders : DE.ty_def list -> unit +(** [attach_orders defs] generate and attach orders on the constructors for + each ADT of [defs]. {b Note:} assume that [defs] is a list of definitions of a complete nest (in any order). By nest, we mean the set of all the constructors in a