From 799ec513454a61c21820d3beef4ae5de00105a46 Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Fri, 12 Apr 2024 14:30:36 +0200 Subject: [PATCH] Merge `Enum` Theory into `ADT` Theory After refactoring both `Enum` and `ADT` theories, they shared most of their implementation. This PR merges `Enum` theory into `ADT` ones. --- src/lib/dune | 2 +- src/lib/frontend/d_cnf.ml | 114 +++++++++-------------------- src/lib/frontend/typechecker.ml | 33 ++++----- src/lib/reasoners/adt_rel.ml | 10 +-- src/lib/reasoners/relation.ml | 59 +++++---------- src/lib/reasoners/shostak.ml | 96 ++++++------------------ src/lib/reasoners/shostak.mli | 3 - src/lib/reasoners/theory.ml | 18 +---- src/lib/structures/expr.ml | 8 -- src/lib/structures/fpa_rounding.ml | 15 ++-- src/lib/structures/ty.ml | 25 ++----- src/lib/structures/ty.mli | 7 +- 12 files changed, 115 insertions(+), 275 deletions(-) diff --git a/src/lib/dune b/src/lib/dune index e55b2dace..8f4860815 100644 --- a/src/lib/dune +++ b/src/lib/dune @@ -49,7 +49,7 @@ Cnf D_cnf D_loop D_state_option Input Frontend Parsed_interface Typechecker Models ; reasoners - Ac Arith Arrays_rel Bitv Ccx Shostak Relation Enum Enum_rel + Ac Arith Arrays_rel Bitv Ccx Shostak Relation Fun_sat Fun_sat_frontend Inequalities Bitv_rel Th_util Adt Adt_rel Instances IntervalCalculus Intervals Ite_rel Matching Matching_types Polynome Records Records_rel Satml_frontend_hybrid Satml_frontend Satml diff --git a/src/lib/frontend/d_cnf.ml b/src/lib/frontend/d_cnf.ml index cea6c8dc3..ce1a0138e 100644 --- a/src/lib/frontend/d_cnf.ml +++ b/src/lib/frontend/d_cnf.ml @@ -540,7 +540,6 @@ and handle_ty_app ?(update = false) ty_c l = in apply_ty_substs tysubsts ty - | Tsum _ as ty -> ty | Text (_, s) -> Text (tyl, s) | _ -> assert false @@ -573,50 +572,29 @@ let mk_ty_decl (ty_c: DE.ty_cst) = let ty = Ty.trecord ~record_constr tyvl (Uid.of_dolmen ty_c) lbs in Cache.store_ty ty_c ty - | Some ( - (Adt { cases; _ } as adt) - ) -> - (Topological_order.sort [adt]; - let uid = Uid.of_dolmen ty_c in - let tyvl = Cache.store_ty_vars_ret cases.(0).cstr.id_ty in - let rev_cs, is_enum = - Array.fold_left ( - fun (accl, is_enum) DE.{ cstr; dstrs; _ } -> - let is_enum = - if is_enum - then - if Array.length dstrs = 0 - then true - else ( - let ty = Ty.t_adt uid tyvl in - Cache.store_ty ty_c ty; - false - ) - else false - in - let rev_fields = - Array.fold_left ( - fun acc tc_o -> - match tc_o with - | Some (DE.{ id_ty; _ } as field) -> - (Uid.of_dolmen field, dty_to_ty id_ty) :: acc - | None -> assert false - ) [] dstrs - in - (Uid.of_dolmen cstr, List.rev rev_fields) :: accl, is_enum - ) ([], true) cases - in - if is_enum - then - let cstrs = - List.map (fun s -> fst s) (List.rev rev_cs) - in - let ty = Ty.tsum uid cstrs in - Cache.store_ty ty_c ty - else - let body = Some (List.rev rev_cs) in - let ty = Ty.t_adt ~body uid tyvl in - Cache.store_ty ty_c ty) + | Some (Adt { cases; _ } as adt) -> + Topological_order.sort [adt]; + let uid = Uid.of_dolmen ty_c in + 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 = + Array.fold_left ( + fun accl DE.{ cstr; dstrs; _ } -> + let rev_fields = + Array.fold_left ( + fun acc tc_o -> + match tc_o with + | Some (DE.{ id_ty; _ } as field) -> + (Uid.of_dolmen field, dty_to_ty id_ty) :: acc + | None -> assert false + ) [] dstrs + in + (Uid.of_dolmen cstr, List.rev rev_fields) :: accl + ) [] cases + in + let body = Some (List.rev rev_cs) in + let ty = Ty.t_adt ~body uid tyvl in + Cache.store_ty ty_c ty | None | Some Abstract -> let ty_params = [] @@ -675,10 +653,7 @@ let mk_mr_ty_decls (tdl: DE.ty_cst list) = in Cache.store_ty ty_c ty - | Tadt (hs, tyl), - Some ( - Adt { cases; ty = ty_c; _ } - ) -> + | Tadt (hs, tyl), Some (Adt { cases; ty = ty_c; _ }) -> let rev_cs = Array.fold_left ( fun accl DE.{ cstr; dstrs; _ } -> @@ -695,8 +670,7 @@ let mk_mr_ty_decls (tdl: DE.ty_cst list) = ) [] cases in let body = Some (List.rev rev_cs) in - let args = tyl in - let ty = Ty.t_adt ~body hs args in + let ty = Ty.t_adt ~body hs tyl in Cache.store_ty ty_c ty | _ -> assert false @@ -724,32 +698,16 @@ let mk_mr_ty_decls (tdl: DE.ty_cst list) = match tdef with | DE.Adt { cases; record; ty = ty_c; } as adt -> let tyvl = Cache.store_ty_vars_ret cases.(0).cstr.id_ty in - - let cns, is_enum = - Array.fold_right ( - fun DE.{ dstrs; cstr; _ } (nacc, is_enum) -> - Uid.of_dolmen cstr :: nacc, - Array.length dstrs = 0 && is_enum - ) cases ([], true) - in let uid = Uid.of_dolmen ty_c in - if is_enum && not contains_adts - then ( - let ty = Ty.tsum uid cns in - Cache.store_ty ty_c ty; - (* If it's an enum we don't need the second iteration. *) - acc - ) - else ( - let ty = - if (record || Array.length cases = 1) && not contains_adts - then - Ty.trecord ~record_constr:uid tyvl uid [] - else Ty.t_adt uid tyvl - in - Cache.store_ty ty_c ty; - (ty, Some adt) :: acc - ) + let ty = + if (record || Array.length cases = 1) && not contains_adts + then + Ty.trecord ~record_constr:uid tyvl uid [] + else Ty.t_adt uid tyvl + in + Cache.store_ty ty_c ty; + (ty, Some adt) :: acc + | Abstract -> assert false (* unreachable in the second iteration *) ) [] (List.rev rev_tdefs) @@ -1050,9 +1008,7 @@ let rec mk_expr match Cache.find_ty ty_c with | Ty.Tadt _ -> E.mk_builtin ~is_pos:true builtin [aux_mk_expr x] - | Ty.Tsum _ as ty -> - let cstr = E.mk_constr (Uid.of_dolmen cstr) [] ty in - E.mk_eq ~iff:false (aux_mk_expr x) cstr + | Ty.Trecord _ -> (* The typechecker allows only testers whose the two arguments have the same type. Thus, we can always diff --git a/src/lib/frontend/typechecker.ml b/src/lib/frontend/typechecker.ml index 8f4747c46..135c96cee 100644 --- a/src/lib/frontend/typechecker.ml +++ b/src/lib/frontend/typechecker.ml @@ -73,10 +73,6 @@ module Types = struct if List.length lty <> List.length lty' then Errors.typing_error (WrongNumberofArgs (Uid.show s)) loc; lty' - | Ty.Tsum (s, _) -> - if List.length lty <> 0 then - Errors.typing_error (WrongNumberofArgs (Uid.show s)) loc; - [] | _ -> assert false let equal_pp_vars lpp lvars = @@ -145,13 +141,6 @@ module Types = struct | Abstract -> let ty = Ty.text ty_vars (Uid.of_string id) in ty, { env with to_ty = MString.add id ty env.to_ty } - | Enum lc -> - if not (Lists.is_empty ty_vars) then - Errors.typing_error (PolymorphicEnum id) loc; - let ty = - Ty.tsum (Uid.of_string id) (List.map Uid.of_string lc) - in - ty, { env with to_ty = MString.add id ty env.to_ty } | Record (record_constr, lbs) -> let lbs = List.map (fun (x, pp) -> x, ty_of_pp loc env None pp) lbs in @@ -171,6 +160,10 @@ module Types = struct from_labels = List.fold_left (fun fl (l,_) -> MString.add l id fl) env.from_labels lbs } + | Enum l -> + let body = List.map (fun constr -> Uid.of_string constr, []) l in + let ty = Ty.t_adt ~body:(Some body) (Uid.of_string id) [] in + ty, { env with to_ty = MString.add id ty env.to_ty } | Algebraic l -> let l = (* convert ppure_type to Ty.t in l *) List.map (fun (constr, l) -> @@ -276,7 +269,9 @@ module Env = struct let add_fpa_enum map = let ty = Fpa_rounding.fpa_rounding_mode in match ty with - | Ty.Tsum (_, cstrs) -> + | Ty.Tadt (name, params) -> + let Adt cases = Ty.type_body name params in + let cstrs = List.map (fun Ty.{ constr; _ } -> constr) cases in List.fold_left (fun m c -> match Fpa_rounding.translate_smt_rounding_mode @@ -300,8 +295,10 @@ module Env = struct let find_builtin_cstr ty n = match ty with - | Ty.Tsum (_, cstrs) -> - List.find (Uid.equal n) cstrs + | Ty.Tadt (name, params) -> + let Adt cases = Ty.type_body name params in + let cstrs = List.map (fun Ty.{ constr; _ } -> constr) cases in + List.find (fun c -> String.equal n @@ Uid.show c) cstrs | _ -> assert false let add_fpa_builtins env = @@ -327,9 +324,9 @@ module Env = struct let nte = Fpa_rounding.string_of_rounding_mode NearestTiesToEven in let tname = Fpa_rounding.fpa_rounding_mode_ae_type_name in let float32 = float (int "24") (int "149") in - let float32d = float32 (mode (Uid.of_string nte)) in + let float32d = float32 (mode nte) in let float64 = float (int "53") (int "1074") in - let float64d = float64 (mode (Uid.of_string nte)) in + let float64d = float64 (mode nte) in let op n op profile = MString.add n @@ `Term (Symbols.Op op, profile, Other) in @@ -1007,8 +1004,6 @@ let rec type_term ?(call_from_type_form=false) env f = end | Ty.Trecord { Ty.record_constr; lbs; _ } -> [{Ty.constr = record_constr; destrs = lbs}] - | Ty.Tsum (_,l) -> - List.map (fun e -> {Ty.constr = e; destrs = []}) l | _ -> Errors.typing_error (ShouldBeADT ty) loc in let pats = @@ -1419,8 +1414,6 @@ and type_form ?(in_theory=false) env f = | Ty.Trecord { Ty.record_constr; lbs; _ } -> [{Ty.constr = record_constr ; destrs = lbs}] - | Ty.Tsum (_,l) -> - List.map (fun e -> {Ty.constr = e ; destrs = []}) l | _ -> Errors.typing_error (ShouldBeADT ty) f.pp_loc in diff --git a/src/lib/reasoners/adt_rel.ml b/src/lib/reasoners/adt_rel.ml index 725262470..0272999df 100644 --- a/src/lib/reasoners/adt_rel.ml +++ b/src/lib/reasoners/adt_rel.ml @@ -592,12 +592,12 @@ let pick_delayed_destructor env uf = if Domain.cardinal d > 1 then raise_notrace @@ Found (r, destr) else + () + | _ -> () - | _ -> - () - ) env.delayed; - None - with Found (r, d) -> Some (r, d) + ) env.delayed; + None + with Found (r, d) -> Some (r, d) let is_enum ty c = match ty with diff --git a/src/lib/reasoners/relation.ml b/src/lib/reasoners/relation.ml index bfdad703d..12971f1ce 100644 --- a/src/lib/reasoners/relation.ml +++ b/src/lib/reasoners/relation.ml @@ -37,11 +37,9 @@ module Rel3 : Sig_rel.RELATION = Bitv_rel module Rel4 : Sig_rel.RELATION = Arrays_rel -module Rel5 : Sig_rel.RELATION = Enum_rel +module Rel5 : Sig_rel.RELATION = Adt_rel -module Rel6 : Sig_rel.RELATION = Adt_rel - -module Rel7 : Sig_rel.RELATION = Ite_rel +module Rel6 : Sig_rel.RELATION = Ite_rel (* This value is unused. *) let timer = Timers.M_None @@ -53,7 +51,6 @@ type t = { r4: Rel4.t; r5: Rel5.t; r6: Rel6.t; - r7: Rel7.t; } let empty uf = @@ -63,8 +60,7 @@ let empty uf = let r4, doms4 = Rel4.empty (Uf.set_domains uf doms3) in let r5, doms5 = Rel5.empty (Uf.set_domains uf doms4) in let r6, doms6 = Rel6.empty (Uf.set_domains uf doms5) in - let r7, doms7 = Rel7.empty (Uf.set_domains uf doms6) in - {r1; r2; r3; r4; r5; r6; r7}, doms7 + {r1; r2; r3; r4; r5; r6}, doms6 let (|@|) l1 l2 = if l1 == [] then l2 @@ -97,14 +93,10 @@ let assume env uf sa = Timers.with_timer Rel6.timer Timers.F_assume @@ fun () -> Rel6.assume env.r6 (Uf.set_domains uf doms5) sa in - let env7, doms7, ({ assume = a7; remove = rm7}:_ Sig_rel.result) = - Timers.with_timer Rel7.timer Timers.F_assume @@ fun () -> - Rel7.assume env.r7 (Uf.set_domains uf doms6) sa - in - {r1=env1; r2=env2; r3=env3; r4=env4; r5=env5; r6=env6; r7=env7}, - doms7, - ({ assume = a1 |@| a2 |@| a3 |@| a4 |@| a5 |@| a6 |@| a7; - remove = rm1 |@| rm2 |@| rm3 |@| rm4 |@| rm5 |@| rm6 |@| rm7} + {r1=env1; r2=env2; r3=env3; r4=env4; r5=env5; r6=env6}, + doms6, + ({ assume = a1 |@| a2 |@| a3 |@| a4 |@| a5 |@| a6; + remove = rm1 |@| rm2 |@| rm3 |@| rm4 |@| rm5 |@| rm6 } : _ Sig_rel.result) let assume_th_elt env th_elt dep = @@ -115,8 +107,7 @@ let assume_th_elt env th_elt dep = let env4 = Rel4.assume_th_elt env.r4 th_elt dep in let env5 = Rel5.assume_th_elt env.r5 th_elt dep in let env6 = Rel6.assume_th_elt env.r6 th_elt dep in - let env7 = Rel7.assume_th_elt env.r7 th_elt dep in - {r1=env1; r2=env2; r3=env3; r4=env4; r5=env5; r6=env6; r7=env7} + {r1=env1; r2=env2; r3=env3; r4=env4; r5=env5; r6=env6} let try_query (type a) (module R : Sig_rel.RELATION with type t = a) env uf a k = @@ -132,8 +123,7 @@ let query env uf a = try_query (module Rel3) env.r3 uf a @@ fun () -> try_query (module Rel4) env.r4 uf a @@ fun () -> try_query (module Rel5) env.r5 uf a @@ fun () -> - try_query (module Rel6) env.r6 uf a @@ fun () -> - try_query (module Rel7) env.r7 uf a @@ fun () -> None + try_query (module Rel6) env.r6 uf a @@ fun () -> None let case_split env uf ~for_model = Options.exec_thread_yield (); @@ -143,8 +133,7 @@ let case_split env uf ~for_model = let seq4 = Rel4.case_split env.r4 uf ~for_model in let seq5 = Rel5.case_split env.r5 uf ~for_model in let seq6 = Rel6.case_split env.r6 uf ~for_model in - let seq7 = Rel7.case_split env.r7 uf ~for_model in - let splits = [seq1; seq2; seq3; seq4; seq5; seq6; seq7] in + let splits = [seq1; seq2; seq3; seq4; seq5; seq6] in let splits = List.fold_left (|@|) [] splits in List.fast_sort (fun (_ ,_ , sz1) (_ ,_ , sz2) -> @@ -181,8 +170,7 @@ let add env uf r t = let r4, doms4, eqs4 =Rel4.add env.r4 (Uf.set_domains uf doms3) r t in let r5, doms5, eqs5 =Rel5.add env.r5 (Uf.set_domains uf doms4) r t in let r6, doms6, eqs6 =Rel6.add env.r6 (Uf.set_domains uf doms5) r t in - let r7, doms7, eqs7 =Rel7.add env.r7 (Uf.set_domains uf doms6) r t in - {r1;r2;r3;r4;r5;r6;r7;},doms7,eqs1|@|eqs2|@|eqs3|@|eqs4|@|eqs5|@|eqs6|@|eqs7 + {r1;r2;r3;r4;r5;r6}, doms6, eqs1|@|eqs2|@|eqs3|@|eqs4|@|eqs5|@|eqs6 let instantiate ~do_syntactic_matching t_match env uf selector = @@ -199,22 +187,13 @@ let instantiate ~do_syntactic_matching t_match env uf selector = Rel5.instantiate ~do_syntactic_matching t_match env.r5 uf selector in let r6, l6 = Rel6.instantiate ~do_syntactic_matching t_match env.r6 uf selector in - let r7, l7 = - Rel7.instantiate ~do_syntactic_matching t_match env.r7 uf selector in - {r1=r1; r2=r2; r3=r3; r4=r4; r5=r5; r6=r6; r7=r7}, - l7 |@| l6 |@| l5 |@| l4 |@| l3 |@| l2 |@| l1 + {r1=r1; r2=r2; r3=r3; r4=r4; r5=r5; r6=r6}, + l6 |@| l5 |@| l4 |@| l3 |@| l2 |@| l1 let new_terms env = - let t1 = Rel1.new_terms env.r1 in - let t2 = Rel2.new_terms env.r2 in - let t3 = Rel3.new_terms env.r3 in - let t4 = Rel4.new_terms env.r4 in - let t5 = Rel5.new_terms env.r5 in - let t6 = Rel6.new_terms env.r6 in - let t7 = Rel7.new_terms env.r7 in - Expr.Set.union t1 - (Expr.Set.union t2 - (Expr.Set.union t3 - (Expr.Set.union t4 - (Expr.Set.union t5 - (Expr.Set.union t6 t7)) ))) + Rel1.new_terms env.r1 + |> Expr.Set.union @@ Rel2.new_terms env.r2 + |> Expr.Set.union @@ Rel3.new_terms env.r3 + |> Expr.Set.union @@ Rel4.new_terms env.r4 + |> Expr.Set.union @@ Rel5.new_terms env.r5 + |> Expr.Set.union @@ Rel6.new_terms env.r6 diff --git a/src/lib/reasoners/shostak.ml b/src/lib/reasoners/shostak.ml index 898070ff5..0c38e426d 100644 --- a/src/lib/reasoners/shostak.ml +++ b/src/lib/reasoners/shostak.ml @@ -43,11 +43,8 @@ module rec CX : sig val extract3 : r -> BITV.t option val embed3 : BITV.t -> r - val extract4 : r -> ENUM.t option - val embed4 : ENUM.t -> r - - val extract5 : r -> ADT.t option - val embed5 : ADT.t -> r + val extract4 : r -> ADT.t option + val embed4 : ADT.t -> r end = struct @@ -58,7 +55,6 @@ struct | Arith of ARITH.t | Records of RECORDS.t | Bitv of BITV.t - | Enum of ENUM.t | Adt of ADT.t type r = {v : rview ; id : int} @@ -74,7 +70,6 @@ struct | Arith t -> fprintf fmt "%a" ARITH.print t | Records t -> fprintf fmt "%a" RECORDS.print t | Bitv t -> fprintf fmt "%a" BITV.print t - | Enum t -> fprintf fmt "%a" ENUM.print t | Adt t -> fprintf fmt "%a" ADT.print t | Term t -> fprintf fmt "%a" Expr.print t | Ac t -> fprintf fmt "%a" AC.print t @@ -87,8 +82,6 @@ struct fprintf fmt "Records(%s):[%a]" RECORDS.name RECORDS.print t | Bitv t -> fprintf fmt "Bitv(%s):[%a]" BITV.name BITV.print t - | Enum t -> - fprintf fmt "Enum(%s):[%a]" ENUM.name ENUM.print t | Adt t -> fprintf fmt "Adt(%s):[%a]" ADT.name ADT.print t | Term t -> @@ -170,7 +163,6 @@ struct | Arith x -> 1 + 10 * ARITH.hash x | Records x -> 2 + 10 * RECORDS.hash x | Bitv x -> 3 + 10 * BITV.hash x - | Enum x -> 5 + 10 * ENUM.hash x | Adt x -> 6 + 10 * ADT.hash x | Ac ac -> 9 + 10 * AC.hash ac | Term t -> 8 + 10 * Expr.hash t @@ -182,7 +174,6 @@ struct | Arith x, Arith y -> ARITH.equal x y | Records x, Records y -> RECORDS.equal x y | Bitv x, Bitv y -> BITV.equal x y - | Enum x, Enum y -> ENUM.equal x y | Adt x, Adt y -> ADT.equal x y | Term x, Term y -> Expr.equal x y | Ac x, Ac y -> AC.equal x y @@ -209,8 +200,7 @@ struct let embed1 x = hcons {v = Arith x; id = -1000 (* dummy *)} let embed2 x = hcons {v = Records x; id = -1000 (* dummy *)} let embed3 x = hcons {v = Bitv x; id = -1000 (* dummy *)} - let embed4 x = hcons {v = Enum x; id = -1000 (* dummy *)} - let embed5 x = hcons {v = Adt x; id = -1000 (* dummy *)} + let embed4 x = hcons {v = Adt x; id = -1000 (* dummy *)} let ac_embed ({ Sig.l; _ } as t) = match l with @@ -227,8 +217,7 @@ struct let extract1 = function { v=Arith r; _ } -> Some r | _ -> None let extract2 = function { v=Records r; _ } -> Some r | _ -> None let extract3 = function { v=Bitv r; _ } -> Some r | _ -> None - let extract4 = function { v=Enum r; _ } -> Some r | _ -> None - let extract5 = function { v=Adt r; _ } -> Some r | _ -> None + let extract4 = function { v=Adt r; _ } -> Some r | _ -> None let ac_extract = function | { v = Ac t; _ } -> Some t @@ -239,7 +228,6 @@ struct | Arith _ -> ARITH.term_extract r | Records _ -> RECORDS.term_extract r | Bitv _ -> BITV.term_extract r - | Enum _ -> ENUM.term_extract r | Adt _ -> ADT.term_extract r | Ac _ -> None, false (* SYLVAIN : TODO *) | Term t -> Some t, true @@ -250,7 +238,6 @@ struct | Arith _ -> ARITH.to_model_term r | Records _ -> RECORDS.to_model_term r | Bitv _ -> BITV.to_model_term r - | Enum _ -> ENUM.to_model_term r | Adt _ -> ADT.to_model_term r | Term t when Expr.is_model_term t -> Some t | Ac _ | Term _ -> None @@ -266,7 +253,6 @@ struct | { v = Arith t; _ } -> ARITH.type_info t | { v = Records t; _ } -> RECORDS.type_info t | { v = Bitv t; _ } -> BITV.type_info t - | { v = Enum t; _ } -> ENUM.type_info t | { v = Adt t; _ } -> ADT.type_info t | { v = Ac x; _ } -> AC.type_info x | { v = Term t; _ } -> Expr.type_info t @@ -279,8 +265,7 @@ struct | Arith _ -> -3 | Records _ -> -4 | Bitv _ -> -5 - | Enum _ -> -7 - | Adt _ -> -8 + | Adt _ -> -7 let compare_tag a b = theory_num a - theory_num b @@ -291,7 +276,6 @@ struct | Arith _, Arith _ -> ARITH.compare a b | Records _, Records _ -> RECORDS.compare a b | Bitv _, Bitv _ -> BITV.compare a b - | Enum _, Enum _ -> ENUM.compare a b | Adt _, Adt _ -> ADT.compare a b | Term x, Term y -> Expr.compare x y | Ac x, Ac y -> AC.compare x y @@ -308,7 +292,7 @@ struct | Records x -> RECORDS.hash x | Bitv x -> BITV.hash x | Arrays x -> ARRAYS.hash x - | Enum x -> ENUM.hash x + | Adt x -> ADT.hash x ***) @@ -336,7 +320,6 @@ struct | Arith t -> ARITH.leaves t | Records t -> RECORDS.leaves t | Bitv t -> BITV.leaves t - | Enum t -> ENUM.leaves t | Adt t -> ADT.leaves t | Ac t -> r :: (AC.leaves t) | Term _ -> [r] @@ -346,7 +329,6 @@ struct | Arith t -> ARITH.is_constant t | Records t -> RECORDS.is_constant t | Bitv t -> BITV.is_constant t - | Enum t -> ENUM.is_constant t | Adt t -> ADT.is_constant t | Term t -> begin @@ -364,7 +346,6 @@ struct | Arith t -> ARITH.subst p v t | Records t -> RECORDS.subst p v t | Bitv t -> BITV.subst p v t - | Enum t -> ENUM.subst p v t | Adt t -> ADT.subst p v t | Ac t -> if equal p r then v else AC.subst p v t | Term _ -> if equal p r then v else r @@ -376,35 +357,30 @@ struct ARITH.is_mine_symb sb ty, not_restricted && RECORDS.is_mine_symb sb ty, not_restricted && BITV.is_mine_symb sb ty, - not_restricted && ENUM.is_mine_symb sb ty, not_restricted && ADT.is_mine_symb sb ty, AC.is_mine_symb sb ty with - | true , false , false, false, false, false -> + | true, false, false, false, false -> Timers.with_timer Timers.M_Arith Timers.F_make @@ fun () -> ARITH.make t - | false , true , false, false, false, false -> + | false, true, false, false, false -> Timers.with_timer Timers.M_Records Timers.F_make @@ fun () -> RECORDS.make t - | false , false , true , false, false, false -> + | false, false, true, false, false -> Timers.with_timer Timers.M_Bitv Timers.F_make @@ fun () -> BITV.make t - | false , false , false , true , false, false -> - Timers.with_timer Timers.M_Sum Timers.F_make @@ fun () -> - ENUM.make t - - | false , false , false , false, true , false -> + | false, false, false, true, false -> Timers.with_timer Timers.M_Adt Timers.F_make @@ fun () -> ADT.make t - | false , false , false , false, false, true -> + | false, false, false, false, true -> Timers.with_timer Timers.M_AC Timers.F_make @@ fun () -> AC.make t - | false , false , false , false, false, false -> + | false, false, false, false, false -> term_embed t, [] | _ -> assert false @@ -415,23 +391,20 @@ struct ARITH.is_mine_symb sb ty, not_restricted && RECORDS.is_mine_symb sb ty, not_restricted && BITV.is_mine_symb sb ty, - not_restricted && ENUM.is_mine_symb sb ty, not_restricted && ADT.is_mine_symb sb ty, AC.is_mine_symb sb ty with - | true , false , false, false, false, false -> + | true, false, false, false, false -> ARITH.fully_interpreted sb - | false , true , false, false, false, false -> + | false, true, false, false, false -> RECORDS.fully_interpreted sb - | false , false , true , false, false, false -> + | false, false, true, false, false -> BITV.fully_interpreted sb - | false , false , false , true , false, false -> - ENUM.fully_interpreted sb - | false , false , false , false, true, false -> + | false, false, false, true, false -> ADT.fully_interpreted sb - | false , false , false , false, false, true -> + | false, false, false, false, true -> AC.fully_interpreted sb - | false , false , false , false, false, false -> + | false, false, false, false, false -> false | _ -> assert false @@ -440,7 +413,6 @@ struct not (Options.get_restricted ()) && (RECORDS.is_mine_symb sb ty || BITV.is_mine_symb sb ty || - ENUM.is_mine_symb sb ty || ADT.is_mine_symb sb ty) let is_a_leaf r = match r.v with @@ -457,19 +429,16 @@ struct ARITH.is_mine_symb ac.Sig.h ty, RECORDS.is_mine_symb ac.Sig.h ty, BITV.is_mine_symb ac.Sig.h ty, - ENUM.is_mine_symb ac.Sig.h ty, ADT.is_mine_symb ac.Sig.h ty, AC.is_mine_symb ac.Sig.h ty with (*AC.is_mine may say F if Options.get_no_ac is set to F dynamically *) - | true , false, false, false, false, false -> + | true, false, false, false, false -> ARITH.color ac - | false , true , false, false, false, false -> + | false, true, false, false, false -> RECORDS.color ac - | false , false , true , false, false, false -> + | false, false, true, false, false -> BITV.color ac - | false , false , false , true , false, false -> - ENUM.color ac - | false , false , false , false, true, false -> + | false, false, false, true, false -> ADT.color ac | _ -> ac_embed ac @@ -479,7 +448,6 @@ struct | Arith a -> ARITH.abstract_selectors a acc | Records a -> RECORDS.abstract_selectors a acc | Bitv a -> BITV.abstract_selectors a acc - | Enum a -> ENUM.abstract_selectors a acc | Adt a -> ADT.abstract_selectors a acc | Term _ -> a, acc | Ac a -> AC.abstract_selectors a acc @@ -568,10 +536,6 @@ struct Timers.with_timer BITV.timer Timers.F_solve @@ fun () -> BITV.solve ra rb pb - | Ty.Tsum _ -> - Timers.with_timer ENUM.timer Timers.F_solve @@ fun () -> - ENUM.solve ra rb pb - (*| Ty.Tunit -> pb *) | Ty.Tadt _ when not (Options.get_disable_adts()) -> @@ -623,7 +587,6 @@ struct Some (Expr.fresh_name (Expr.type_info t), false) end - | _, Ty.Tsum _ -> ENUM.assign_value r distincts eq | _, Ty.Tadt _ when not (Options.get_disable_adts()) -> ADT.assign_value r distincts eq @@ -700,24 +663,14 @@ and BITV : Sig.SHOSTAK let embed = embed3 end) -and ENUM : Sig.SHOSTAK - with type r = CX.r - and type t = CX.r Enum.abstract = - Enum.Shostak - (struct - include CX - let extract = extract4 - let embed = embed4 - end) - and ADT : Sig.SHOSTAK with type r = CX.r and type t = CX.r Adt.abstract = Adt.Shostak (struct include CX - let extract = extract5 - let embed = embed5 + let extract = extract4 + let embed = embed4 end) (* Its signature is not Sig.SHOSTAK because it does not provide a solver *) @@ -758,7 +711,6 @@ end module Arith = ARITH module Records = RECORDS module Bitv = BITV -module Enum = ENUM module Adt = ADT module Polynome = TARITH module Ac = AC diff --git a/src/lib/reasoners/shostak.mli b/src/lib/reasoners/shostak.mli index 88226887a..0067e7df9 100644 --- a/src/lib/reasoners/shostak.mli +++ b/src/lib/reasoners/shostak.mli @@ -44,9 +44,6 @@ module Records : Sig.SHOSTAK module Bitv : Sig.SHOSTAK with type r = Combine.r and type t = Combine.r Bitv.abstract -module Enum : Sig.SHOSTAK - with type r = Combine.r and type t = Combine.r Enum.abstract - module Adt : Sig.SHOSTAK with type r = Combine.r and type t = Combine.r Adt.abstract diff --git a/src/lib/reasoners/theory.ml b/src/lib/reasoners/theory.ml index 9c0a59ee5..199e8f5df 100644 --- a/src/lib/reasoners/theory.ml +++ b/src/lib/reasoners/theory.ml @@ -159,16 +159,13 @@ module Main_Default : S = struct | Tint | Treal | Tbool | Tunit | Tbitv _ | Tfarray _ -> mp | Tvar _ -> assert false - | Text (_, hs) | Tsum (hs, _) | Trecord { name = hs; _ } when + | Text (_, hs) | Trecord { name = hs; _ } when Uid.Map.mem hs mp -> mp | Text (l, hs) -> let l = List.map (fun _ -> Ty.fresh_tvar()) l in Uid.Map.add hs (Text(l, hs)) mp - | Tsum (hs, _) -> - Uid.Map.add hs ty mp - | Trecord { name; _ } -> (* cannot do better for records ? *) Uid.Map.add name ty mp @@ -187,19 +184,6 @@ module Main_Default : S = struct | Tint | Treal | Tbool | Tunit | Tbitv _ | Tfarray _ -> () | Tvar _ -> assert false | Text _ -> print_dbg ~flushed:false "type %a@ " Ty.print ty - | Tsum (_, l) -> - print_dbg ~flushed:false ~header:false "type %a = " Ty.print ty; - begin match l with - | [] -> assert false - | e::l -> - let print fmt e = - Format.fprintf fmt " | %a" Uid.pp e - in - print_dbg ~flushed:false ~header:false "%a@ %a@ " - Uid.pp e - (pp_list_no_space print) l; - end - | Trecord { Ty.lbs; _ } -> print_dbg ~flushed:false ~header:false "type %a = " Ty.print ty; begin match lbs with diff --git a/src/lib/structures/expr.ml b/src/lib/structures/expr.ml index 5b2c08c93..3e76084d6 100644 --- a/src/lib/structures/expr.ml +++ b/src/lib/structures/expr.ml @@ -2581,7 +2581,6 @@ let mk_match e cases = match ty with | Ty.Tadt _ -> (fun hs -> Sy.destruct hs) | Ty.Trecord _ -> (fun hs -> Sy.Op (Sy.Access hs)) - | Ty.Tsum _ -> (fun _hs -> assert false) (* no destructors for Tsum *) | _ -> assert false in let mker = @@ -2593,13 +2592,6 @@ let mk_match e cases = | Ty.Trecord _ -> (fun _e _name -> assert false) (* no need to test for records *) - | Ty.Tsum _ -> - (fun e n -> (* testers are equalities for Tsum *) - let constr = - mk_term (Sy.constr n) [] (type_info e) - in - mk_eq ~iff:false e constr) - | _ -> assert false in let res = compile_match mk_destr mker e cases e in diff --git a/src/lib/structures/fpa_rounding.ml b/src/lib/structures/fpa_rounding.ml index c94442bc1..d12e38d51 100644 --- a/src/lib/structures/fpa_rounding.ml +++ b/src/lib/structures/fpa_rounding.ml @@ -75,7 +75,7 @@ let string_of_rounding_mode = to_smt_string let hstring_smt_reprs = List.map - (fun c -> Hs.make (to_smt_string c)) + (fun c -> to_smt_string c, []) cstrs let hstring_ae_reprs = @@ -92,18 +92,21 @@ let fpa_rounding_mode_dty, d_cstrs, fpa_rounding_mode = let cstrs = List.map (fun c -> DStd.Path.global @@ to_smt_string c, []) cstrs in - let _, cstrs = DE.Term.define_adt ty_cst [] cstrs in - DE.Ty.apply ty_cst [], cstrs, - Ty.Tsum (Uid.of_dolmen ty_cst, List.map (fun (c, _) -> Uid.of_dolmen c) cstrs) + let _, d_cstrs = DE.Term.define_adt ty_cst [] cstrs in + let body = + List.map (fun (c, _) -> Uid.of_dolmen c, []) d_cstrs + in + let ty = Ty.t_adt ~body:(Some body) (Uid.of_dolmen ty_cst) [] in + DE.Ty.apply ty_cst [], d_cstrs, ty let rounding_mode_of_smt_hs = let table = Hashtbl.create 5 in List.iter2 ( - fun key bnd -> + fun (key, _) bnd -> Hashtbl.add table key bnd ) hstring_smt_reprs cstrs; fun key -> - try Hashtbl.find table key with + try Hashtbl.find table (Hstring.view key) with | Not_found -> Fmt.failwith "Error while searching for SMT2 FPA value %a." diff --git a/src/lib/structures/ty.ml b/src/lib/structures/ty.ml index eb14f8e0c..e749f75a6 100644 --- a/src/lib/structures/ty.ml +++ b/src/lib/structures/ty.ml @@ -34,7 +34,6 @@ type t = | Tbitv of int | Text of t list * Uid.t | Tfarray of t * t - | Tsum of Uid.t * Uid.t list | Tadt of Uid.t * t list | Trecord of trecord @@ -55,7 +54,7 @@ module Smtlib = struct | Tbitv n -> Fmt.pf ppf "(_ BitVec %d)" n | Tfarray (a_t, r_t) -> Fmt.pf ppf "(Array %a %a)" pp a_t pp r_t - | Text ([], name) | Tsum (name, _) + | Text ([], name) | Trecord { args = []; name; _ } | Tadt (name, []) -> Uid.pp ppf name | Text (args, name) | Trecord { args; name; _ } | Tadt (name, args) -> @@ -122,8 +121,6 @@ let print_generic body_of = fprintf fmt "%a %a" print_list l Uid.pp s | Tfarray (t1, t2) -> fprintf fmt "(%a,%a) farray" (print body_of) t1 (print body_of) t2 - | Tsum(s, _) -> - fprintf fmt "%a" Uid.pp s | Trecord { args = lv; name = n; lbs = lbls; _ } -> begin fprintf fmt "%a %a" print_list lv Uid.pp n; @@ -228,7 +225,7 @@ let rec shorten ty = (* should not rebuild the type if no changes are made *) Tadt (n, args') - | Tint | Treal | Tbool | Tunit | Tbitv _ | Tsum (_, _) -> ty + | Tint | Treal | Tbool | Tunit | Tbitv _ -> ty and shorten_body _ _ = () @@ -248,9 +245,6 @@ let rec compare t1 t2 = if c<>0 then c else compare ta2 tb2 | Tfarray _, _ -> -1 | _ , Tfarray _ -> 1 - | Tsum(s1, _), Tsum(s2, _) -> - Uid.compare s1 s2 - | Tsum _, _ -> -1 | _ , Tsum _ -> 1 | Trecord { args = a1; name = s1; lbs = l1; _ }, Trecord { args = a2; name = s2; lbs = l2; _ } -> let c = Uid.compare s1 s2 in @@ -300,7 +294,6 @@ let rec equal t1 t2 = with Invalid_argument _ -> false) | Tfarray (ta1, ta2), Tfarray (tb1, tb2) -> equal ta1 tb1 && equal ta2 tb2 - | Tsum (s1, _), Tsum (s2, _) -> Uid.equal s1 s2 | Trecord { args = a1; name = s1; lbs = l1; _ }, Trecord { args = a2; name = s2; lbs = l2; _ } -> begin @@ -343,7 +336,6 @@ let rec matching s pat t = let s = List.fold_left2 matching s r1.args r2.args in List.fold_left2 (fun s (_, p) (_, ty) -> matching s p ty) s r1.lbs r2.lbs - | Tsum (s1, _), Tsum (s2, _) when Uid.equal s1 s2 -> s | Tint , Tint | Tbool , Tbool | Treal , Treal | Tunit, Tunit -> s | Tbitv n , Tbitv m when n=m -> s | Tadt(n1, args1), Tadt(n2, args2) when Uid.equal n1 n2 -> @@ -381,7 +373,7 @@ let apply_subst = -> Tadt (name, List.map (apply_subst s) params) - | Tint | Treal | Tbool | Tunit | Tbitv _ | Tsum (_, _) -> ty + | Tint | Treal | Tbool | Tunit | Tbitv _ -> ty in fun s ty -> if M.is_empty s then ty else apply_subst s ty @@ -538,8 +530,6 @@ let fresh_empty_text = in text [] (Uid.of_dolmen id) -let tsum s lc = Tsum (s, lc) - let t_adt ?(body=None) s ty_vars = let ty = Tadt (s, ty_vars) in begin match body with @@ -586,9 +576,9 @@ let rec hash t = (abs h) lbs in abs h - | Tsum (s, _) -> abs (Uid.hash s) (*we do not hash constructors*) | Tadt (s, args) -> + (* We do not hash constructors. *) let h = List.fold_left (fun h ty -> 31 * h + hash ty) (Uid.hash s) args in @@ -602,7 +592,7 @@ let occurs { v = n; _ } t = | Text(l,_) -> List.exists occursrec l | Tfarray (t1,t2) -> occursrec t1 || occursrec t2 | Trecord { args ; _ } | Tadt (_, args) -> List.exists occursrec args - | Tsum _ | Tint | Treal | Tbool | Tunit | Tbitv _ -> false + | Tint | Treal | Tbool | Tunit | Tbitv _ -> false in occursrec t (*** destructive unification ***) @@ -623,7 +613,6 @@ let rec unify t1 t2 = | Tfarray (ta1,ta2), Tfarray (tb1,tb2) -> unify ta1 tb1;unify ta2 tb2 | Trecord r1, Trecord r2 when Uid.equal r1.name r2.name -> List.iter2 unify r1.args r2.args - | Tsum(s1, _) , Tsum(s2, _) when Uid.equal s1 s2 -> () | Tint, Tint | Tbool, Tbool | Treal, Treal | Tunit, Tunit -> () | Tbitv n , Tbitv m when m=n -> () @@ -674,7 +663,7 @@ let vty_of t = List.fold_left vty_of_rec acc args | Tvar { value = Some _ ; _ } - | Tint | Treal | Tbool | Tunit | Tbitv _ | Tsum (_, _) -> + | Tint | Treal | Tbool | Tunit | Tbitv _ -> acc in vty_of_rec Svty.empty t @@ -683,7 +672,7 @@ let vty_of t = [@ocaml.ppwarning "TODO: detect when there are no changes "] let rec monomorphize ty = match ty with - | Tint | Treal | Tbool | Tunit | Tbitv _ | Tsum _ -> ty + | Tint | Treal | Tbool | Tunit | Tbitv _ -> ty | Text (tyl,hs) -> Text (List.map monomorphize tyl, hs) | Trecord ({ args = tylv; name = n; lbs = tylb; _ } as r) -> let m_tylv = List.map monomorphize tylv in diff --git a/src/lib/structures/ty.mli b/src/lib/structures/ty.mli index 5003566a6..d98a51d98 100644 --- a/src/lib/structures/ty.mli +++ b/src/lib/structures/ty.mli @@ -48,11 +48,10 @@ type t = (** Abstract types applied to arguments. [Text (args, s)] is the application of the abstract type constructor [s] to arguments [args]. *) + | Tfarray of t * t (** Functional arrays. [TFarray (src,dst)] maps values of type [src] to values of type [dst]. *) - | Tsum of Uid.t * Uid.t list - (** Enumeration, with its name, and the list of its constructors. *) | Tadt of Uid.t * t list (** Application of algebraic data types. [Tadt (a, params)] denotes @@ -169,10 +168,6 @@ val text : t list -> Uid.t -> t (** Apply the abstract type constructor to the list of type arguments given. *) -val tsum : Uid.t -> Uid.t list -> t -(** Create an enumeration type. [tsum name enums] creates an enumeration - named [name], with constructors [enums]. *) - val t_adt : ?body: ((Uid.t * (Uid.t * t) list) list) option -> Uid.t -> t list -> t (** Create an algebraic datatype. The body is a list of