From 7b4049aedf7c16a5f9480100d5e887d6f7d0a8ed Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Sun, 14 Apr 2024 13:05:16 +0200 Subject: [PATCH 01/14] Merge `Records` into `ADT` --- src/lib/dune | 2 +- src/lib/frontend/models.ml | 22 +---- src/lib/frontend/translate.ml | 162 +++------------------------------ src/lib/reasoners/adt.ml | 7 +- src/lib/reasoners/adt_rel.ml | 6 +- src/lib/reasoners/matching.ml | 22 ++--- src/lib/reasoners/relation.ml | 49 ++++------ src/lib/reasoners/shostak.ml | 105 ++++++--------------- src/lib/reasoners/shostak.mli | 3 - src/lib/reasoners/theory.ml | 24 +---- src/lib/structures/expr.ml | 58 +----------- src/lib/structures/expr.mli | 5 - src/lib/structures/symbols.ml | 13 +-- src/lib/structures/symbols.mli | 3 +- src/lib/structures/ty.ml | 112 +++-------------------- src/lib/structures/ty.mli | 31 +------ 16 files changed, 101 insertions(+), 523 deletions(-) diff --git a/src/lib/dune b/src/lib/dune index b16028751..1b0d245b8 100644 --- a/src/lib/dune +++ b/src/lib/dune @@ -51,7 +51,7 @@ Ac Arith Arrays_rel Bitv Ccx Shostak Relation Fun_sat Fun_sat_frontend Inequalities Bitv_rel Th_util Adt Adt_rel Instances IntervalCalculus Intervals_intf Intervals_core Intervals - Ite_rel Matching Matching_types Polynome Records Records_rel + Ite_rel Matching Matching_types Polynome Satml_frontend_hybrid Satml_frontend Satml Sat_solver Sat_solver_sig Sig Sig_rel Theory Uf Use Domains Domains_intf Rel_utils Bitlist ; structures diff --git a/src/lib/frontend/models.ml b/src/lib/frontend/models.ml index afa71e83d..25972083b 100644 --- a/src/lib/frontend/models.ml +++ b/src/lib/frontend/models.ml @@ -42,7 +42,7 @@ module Pp_smtlib_term = struct asprintf "%a" Ty.pp_smtlib t let rec print fmt t = - let {Expr.f;xs;ty; _} = Expr.term_view t in + let {Expr.f;xs; _} = Expr.term_view t in match f, xs with | Sy.Lit lit, xs -> @@ -151,26 +151,6 @@ module Pp_smtlib_term = struct | Sy.Op Sy.Extract (i, j), [e] -> fprintf fmt "%a^{%d,%d}" print e i j - | Sy.Op (Sy.Access field), [e] -> - if Options.get_output_smtlib () then - fprintf fmt "(%a %a)" DE.Term.Const.print field print e - else - fprintf fmt "%a.%a" print e DE.Term.Const.print field - - | Sy.Op (Sy.Record), _ -> - begin match ty with - | Ty.Trecord { Ty.lbs = lbs; _ } -> - assert (List.length xs = List.length lbs); - fprintf fmt "{"; - ignore (List.fold_left2 (fun first (field,_) e -> - fprintf fmt "%s%a = %a" (if first then "" else "; ") - DE.Term.Const.print field print e; - false - ) true lbs xs); - fprintf fmt "}"; - | _ -> assert false - end - (* TODO: introduce PrefixOp in the future to simplify this ? *) | Sy.Op op, [e1; e2] when op == Sy.Pow || op == Sy.Integer_round || op == Sy.Max_real || op == Sy.Max_int || diff --git a/src/lib/frontend/translate.ml b/src/lib/frontend/translate.ml index 0b3f5c803..5d7bd7a91 100644 --- a/src/lib/frontend/translate.ml +++ b/src/lib/frontend/translate.ml @@ -519,85 +519,17 @@ let rec dty_to_ty ?(update = false) ?(is_var = false) dty = | _ -> unsupported "Type %a" DE.Ty.print dty and handle_ty_app ?(update = false) ty_c l = - (* Applies the substitutions in [tysubsts] to each encountered type - variable. *) - let rec apply_ty_substs tysubsts ty = - match ty with - | Ty.Tvar v -> - Ty.TvMap.find v tysubsts - - | Text (tyl, hs) -> - Ty.Text (List.map (apply_ty_substs tysubsts) tyl, hs) - - | Tfarray (ti, tv) -> - Tfarray ( - apply_ty_substs tysubsts ti, - apply_ty_substs tysubsts tv - ) - - | Tadt (hs, tyl) -> - Tadt (hs, List.map (apply_ty_substs tysubsts) tyl) - - | Trecord ({ args; lbs; _ } as rcrd) -> - Trecord { - rcrd with - args = List.map (apply_ty_substs tysubsts) args; - lbs = List.map ( - fun (hs, t) -> - hs, apply_ty_substs tysubsts t - ) lbs; - } - - | _ -> ty - in let tyl = List.map (dty_to_ty ~update) l in (* Recover the initial versions of the types and apply them on the provided type arguments stored in [tyl]. *) match Cache.find_ty ty_c with - | Tadt (hs, _) -> Tadt (hs, tyl) - - | Trecord { args; _ } as ty -> - let tysubsts = - List.fold_left2 ( - fun acc tv ty -> - match tv with - | Ty.Tvar v -> Ty.TvMap.add v ty acc - | _ -> assert false - ) Ty.TvMap.empty args tyl - in - apply_ty_substs tysubsts ty - + | Tadt (hs, _, record) -> Tadt (hs, tyl, record) | Text (_, s) -> Text (tyl, s) | _ -> assert false (** Handles a simple type declaration. *) let mk_ty_decl (ty_c: DE.ty_cst) = match DT.definition ty_c with - | Some ( - (Adt - { cases = [| { cstr = { id_ty; _ } as cstr; dstrs; _ } |]; _ } as adt) - ) -> - (* Records and adts that only have one case are treated in the same way, - and considered as records. *) - Nest.attach_orders [adt]; - let tyvl = Cache.store_ty_vars_ret id_ty in - let lbs = - Array.fold_right ( - fun c acc -> - match c with - | Some (DE.{ id_ty; _ } as id) -> - let pty = dty_to_ty id_ty in - (id, pty) :: acc - | _ -> - Fmt.failwith - "Unexpected null label for some field of the record type %a" - DE.Ty.Const.print ty_c - - ) dstrs [] - in - let ty = Ty.trecord ~record_constr:cstr tyvl ty_c lbs in - Cache.store_ty ty_c ty - | Some (Adt { cases; _ } as adt) -> Nest.attach_orders [adt]; let tyvl = Cache.store_ty_vars_ret cases.(0).cstr.id_ty in @@ -654,29 +586,7 @@ let mk_term_decl ({ id_ty; path; tags; _ } as tcst: DE.term_cst) = let mk_mr_ty_decls (tdl: DE.ty_cst list) = let handle_ty_decl (ty: Ty.t) (tdef: DE.Ty.def option) = match ty, tdef with - | Trecord { args; name; record_constr; _ }, - Some ( - Adt { cases = [| { dstrs; _ } |]; ty = ty_c; _ } - ) -> - let lbs = - Array.fold_right ( - fun c acc -> - match c with - | Some (DE.{ id_ty; _ } as id) -> - let pty = dty_to_ty id_ty in - (id, pty) :: acc - | _ -> - Fmt.failwith - "Unexpected null label for some field of the record type %a" - DE.Ty.Const.print ty_c - ) dstrs [] - in - let ty = - Ty.trecord ~record_constr args name lbs - 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 cs = Array.fold_right ( fun DE.{ cstr; dstrs; _ } accl -> @@ -697,37 +607,15 @@ let mk_mr_ty_decls (tdl: DE.ty_cst list) = | _ -> assert false in - (* If there are adts in the list of type declarations then records are - converted to adts, because that's how it's done in the legacy typechecker. - But it might be more efficient not to do that. *) - let rev_tdefs, contains_adts = - List.fold_left ( - fun (acc, ca) ty_c -> - match DT.definition ty_c with - | Some (Adt { record; cases; _ } as df) - when not record && Array.length cases > 1 -> - df :: acc, true - | Some (Adt _ as df) -> - df :: acc, ca - | Some Abstract | None -> - assert false - ) ([], false) tdl - in + let rev_tdefs = List.rev_map (fun td -> Option.get @@ DT.definition td) tdl in Nest.attach_orders rev_tdefs; let rev_l = List.fold_left ( fun acc tdef -> match tdef with - | DE.Adt { cases; record; ty = ty_c; } as adt -> + | DE.Adt { cases; ty = ty_c; _ } as adt -> let tyvl = Cache.store_ty_vars_ret cases.(0).cstr.id_ty in - let record_constr = cases.(0).cstr in - let ty = - if (record || Array.length cases = 1) && not contains_adts - then - Ty.trecord ~record_constr tyvl ty_c [] - else - Ty.t_adt ty_c tyvl - in + let ty = Ty.t_adt ty_c tyvl in Cache.store_ty ty_c ty; (ty, Some adt) :: acc @@ -854,15 +742,11 @@ end = struct let mk_destr = match ty with | Ty.Tadt _ -> (fun hs -> Sy.destruct hs) - | Ty.Trecord _ -> (fun hs -> Sy.Op (Sy.Access hs)) | _ -> assert false in let mk_tester = match ty with | Ty.Tadt _ -> E.mk_tester - | Ty.Trecord _ -> - (* no need to test for records *) - (fun _e _name -> assert false) | _ -> assert false in let res = compile mk_destr mk_tester e cases e in @@ -1015,14 +899,8 @@ let rec mk_expr E.mk_term sy [] ty | B.Constructor _ -> - begin match dty_to_ty term_ty with - | Trecord _ as ty -> - E.mk_record [] ty - | Tadt _ as ty -> - E.mk_constr tcst [] ty - | ty -> - Fmt.failwith "unexpected type %a@." Ty.print ty - end + let ty = dty_to_ty term_ty in + E.mk_constr tcst [] ty | _ -> unsupported "Constant term %a" DE.Term.print term end @@ -1063,10 +941,7 @@ let rec mk_expr let e = aux_mk_expr x in let sy = match Cache.find_ty adt with - | Trecord _ -> - Sy.Op (Sy.Access destr) - | Tadt _ -> - Sy.destruct destr + | Tadt _ -> Sy.destruct destr | _ -> assert false in E.mk_term sy [e] ty @@ -1097,11 +972,6 @@ let rec mk_expr | Ty.Tadt _ -> E.mk_tester cstr (aux_mk_expr x) - | Ty.Trecord _ -> - (* The typechecker allows only testers whose the - two arguments have the same type. Thus, we can always - replace the tester of a record by the true literal. *) - E.vrai | _ -> assert false end @@ -1368,19 +1238,9 @@ let rec mk_expr | B.Constructor _, _ -> let ty = dty_to_ty term_ty in - begin match ty with - | Ty.Tadt _ -> - let l = List.map (fun t -> aux_mk_expr t) args in - E.mk_constr tcst l ty - | Ty.Trecord _ -> - let l = List.map (fun t -> aux_mk_expr t) args in - E.mk_record l ty - | _ -> - Fmt.failwith - "Constructor error: %a does not belong to a record nor an\ - algebraic data type" - DE.Term.print app_term - end + let sy = Sy.constr tcst in + let l = List.map (fun t -> aux_mk_expr t) args in + E.mk_term sy l ty | B.Coercion, [ x ] -> begin match DT.view (DE.Term.ty x), DT.view term_ty with diff --git a/src/lib/reasoners/adt.ml b/src/lib/reasoners/adt.ml index fca71829f..92ebde84b 100644 --- a/src/lib/reasoners/adt.ml +++ b/src/lib/reasoners/adt.ml @@ -62,7 +62,7 @@ let constr_of_destr ty dest = ~module_name:"Adt" ~function_name:"constr_of_destr" "ty = %a" Ty.print ty; match ty with - | Ty.Tadt (s, params) -> + | Ty.Tadt (s, params, _) -> begin let cases = Ty.type_body s params in try @@ -182,7 +182,7 @@ module Shostak (X : ALIEN) = struct in let xs = List.rev sx in match f, xs, ty with - | Sy.Op Sy.Constr hs, _, Ty.Tadt (name, params) -> + | Sy.Op Sy.Constr hs, _, Ty.Tadt (name, params, _) -> let cases = Ty.type_body name params in let case_hs = try Ty.assoc_destrs hs cases with Not_found -> assert false @@ -203,9 +203,6 @@ module Shostak (X : ALIEN) = struct else sel_x, ctx (* canonization OK *) *) - | Sy.Op Sy.Constr _, _, Ty.Trecord _ -> - Fmt.failwith "unexpected record constructor %a@." E.print t - | _ -> assert false let hash x = diff --git a/src/lib/reasoners/adt_rel.ml b/src/lib/reasoners/adt_rel.ml index 87e10b0bc..bafcb9a09 100644 --- a/src/lib/reasoners/adt_rel.ml +++ b/src/lib/reasoners/adt_rel.ml @@ -93,7 +93,7 @@ module Domain = struct let unknown ty = match ty with - | Ty.Tadt (name, params) -> + | 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 constrs = @@ -462,7 +462,7 @@ let build_constr_eq r c = match Th.embed r with | Alien r -> begin match X.type_info r with - | Ty.Tadt (name, params) as ty -> + | Ty.Tadt (name, params, _) as ty -> let cases = Ty.type_body name params in let ds = try Ty.assoc_destrs c cases with Not_found -> assert false @@ -548,7 +548,7 @@ let two = Numbers.Q.from_int 2 (* TODO: we should compute this reverse map in `Ty` and store it there. *) let constr_of_destr ty d = match ty with - | Ty.Tadt (name, params) -> + | Ty.Tadt (name, params, _) -> begin let cases = Ty.type_body name params in try diff --git a/src/lib/reasoners/matching.ml b/src/lib/reasoners/matching.ml index 8e9dedd3d..d51957e52 100644 --- a/src/lib/reasoners/matching.ml +++ b/src/lib/reasoners/matching.ml @@ -314,11 +314,11 @@ module Make (X : Arg) : S with type theory = X.t = struct | _ , [] -> l1 | _ -> List.fold_left (fun acc e -> e :: acc) l2 (List.rev l1) - let xs_modulo_records t { Ty.lbs; _ } = - List.rev + (* let xs_modulo_records t { Ty.lbs; _ } = + List.rev (List.rev_map (fun (hs, ty) -> - E.mk_term (Symbols.Op (Symbols.Access hs)) [t] ty) lbs) + E.mk_term (Symbols.Op (Symbols.Access hs)) [t] ty) lbs) *) module SLE = (* sets of lists of terms *) Set.Make(struct @@ -411,15 +411,15 @@ module Make (X : Arg) : S with type theory = X.t = struct let cl = E.Set.fold (fun t l -> - let { E.f = f; xs = xs; ty = ty; _ } = E.term_view t in + let { E.f = f; xs = xs; _ } = E.term_view t in if Symbols.compare f_pat f = 0 then xs::l - else - begin - match f_pat, ty with - | Symbols.Op (Symbols.Record), Ty.Trecord record -> - (xs_modulo_records t record) :: l - | _ -> l - end + else l + (* begin + match f_pat, ty with + | Symbols.Op (Symbols.Record), Ty.Trecord record -> + (xs_modulo_records t record) :: l + | _ -> l + end *) ) cl [] in let cl = filter_classes mconf cl tbox in diff --git a/src/lib/reasoners/relation.ml b/src/lib/reasoners/relation.ml index d36a88526..78eb6699a 100644 --- a/src/lib/reasoners/relation.ml +++ b/src/lib/reasoners/relation.ml @@ -31,15 +31,13 @@ module X = Shostak.Combine module Rel1 : Sig_rel.RELATION = IntervalCalculus -module Rel2 : Sig_rel.RELATION = Records_rel +module Rel2 : Sig_rel.RELATION = Bitv_rel -module Rel3 : Sig_rel.RELATION = Bitv_rel +module Rel3 : Sig_rel.RELATION = Arrays_rel -module Rel4 : Sig_rel.RELATION = Arrays_rel +module Rel4 : Sig_rel.RELATION = Adt_rel -module Rel5 : Sig_rel.RELATION = Adt_rel - -module Rel6 : Sig_rel.RELATION = Ite_rel +module Rel5 : Sig_rel.RELATION = Ite_rel (* This value is unused. *) let timer = Timers.M_None @@ -50,7 +48,6 @@ type t = { r3: Rel3.t; r4: Rel4.t; r5: Rel5.t; - r6: Rel6.t; } let empty uf = @@ -59,8 +56,7 @@ let empty uf = let r3, doms3 = Rel3.empty (Uf.set_domains uf doms2) in 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 - {r1; r2; r3; r4; r5; r6}, doms6 + {r1; r2; r3; r4; r5}, doms5 let (|@|) l1 l2 = if l1 == [] then l2 @@ -89,14 +85,10 @@ let assume env uf sa = Timers.with_timer Rel5.timer Timers.F_assume @@ fun () -> Rel5.assume env.r5 (Uf.set_domains uf doms4) sa in - let env6, doms6, ({ assume = a6; remove = rm6}:_ Sig_rel.result) = - Timers.with_timer Rel6.timer Timers.F_assume @@ fun () -> - Rel6.assume env.r6 (Uf.set_domains uf doms5) sa - in - {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 } + {r1=env1; r2=env2; r3=env3; r4=env4; r5=env5}, + doms5, + ({ assume = a1 |@| a2 |@| a3 |@| a4 |@| a5; + remove = rm1 |@| rm2 |@| rm3 |@| rm4 |@| rm5 } : _ Sig_rel.result) let assume_th_elt env th_elt dep = @@ -106,8 +98,7 @@ let assume_th_elt env th_elt dep = let env3 = Rel3.assume_th_elt env.r3 th_elt dep in 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 - {r1=env1; r2=env2; r3=env3; r4=env4; r5=env5; r6=env6} + {r1=env1; r2=env2; r3=env3; r4=env4; r5=env5} let try_query (type a) (module R : Sig_rel.RELATION with type t = a) env uf a k = @@ -122,8 +113,7 @@ let query env uf a = try_query (module Rel2) env.r2 uf a @@ fun () -> 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 () -> None + try_query (module Rel5) env.r5 uf a @@ fun () -> None let case_split env uf ~for_model = Options.exec_thread_yield (); @@ -132,8 +122,7 @@ let case_split env uf ~for_model = let seq3 = Rel3.case_split env.r3 uf ~for_model in 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 splits = [seq1; seq2; seq3; seq4; seq5; seq6] in + let splits = [seq1; seq2; seq3; seq4; seq5] in let splits = List.fold_left (|@|) [] splits in List.fast_sort (fun (_ ,_ , sz1) (_ ,_ , sz2) -> @@ -158,8 +147,7 @@ let optimizing_objective env uf o = Rel1.optimizing_objective env.r1 uf; Rel2.optimizing_objective env.r2 uf; Rel3.optimizing_objective env.r3 uf; - Rel4.optimizing_objective env.r4 uf; - Rel5.optimizing_objective env.r5 uf + Rel4.optimizing_objective env.r4 uf ] let add env uf r t = @@ -169,9 +157,7 @@ let add env uf r t = let r3, doms3, eqs3 =Rel3.add env.r3 (Uf.set_domains uf doms2) r t in 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 - {r1;r2;r3;r4;r5;r6}, doms6, eqs1|@|eqs2|@|eqs3|@|eqs4|@|eqs5|@|eqs6 - + {r1;r2;r3;r4;r5}, doms5, eqs1|@|eqs2|@|eqs3|@|eqs4|@|eqs5 let instantiate ~do_syntactic_matching t_match env uf selector = Options.exec_thread_yield (); @@ -185,10 +171,8 @@ let instantiate ~do_syntactic_matching t_match env uf selector = Rel4.instantiate ~do_syntactic_matching t_match env.r4 uf selector in let r5, l5 = 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 - {r1=r1; r2=r2; r3=r3; r4=r4; r5=r5; r6=r6}, - l6 |@| l5 |@| l4 |@| l3 |@| l2 |@| l1 + {r1=r1; r2=r2; r3=r3; r4=r4; r5=r5}, + l5 |@| l4 |@| l3 |@| l2 |@| l1 let new_terms env = Rel1.new_terms env.r1 @@ -196,4 +180,3 @@ let new_terms env = |> 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 919783407..6ef1950c6 100644 --- a/src/lib/reasoners/shostak.ml +++ b/src/lib/reasoners/shostak.ml @@ -37,14 +37,11 @@ module rec CX : sig val extract1 : r -> ARITH.t option val embed1 : ARITH.t -> r - val extract2 : r -> RECORDS.t option - val embed2 : RECORDS.t -> r + val extract2 : r -> BITV.t option + val embed2 : BITV.t -> r - val extract3 : r -> BITV.t option - val embed3 : BITV.t -> r - - val extract4 : r -> ADT.t option - val embed4 : ADT.t -> r + val extract3 : r -> ADT.t option + val embed3 : ADT.t -> r end = struct @@ -53,7 +50,6 @@ struct | Term of Expr.t | Ac of AC.t | Arith of ARITH.t - | Records of RECORDS.t | Bitv of BITV.t | Adt of ADT.t @@ -68,7 +64,6 @@ struct if Options.get_term_like_pp () then begin match r.v with | Arith t -> fprintf fmt "%a" ARITH.print t - | Records t -> fprintf fmt "%a" RECORDS.print t | Bitv t -> fprintf fmt "%a" BITV.print t | Adt t -> fprintf fmt "%a" ADT.print t | Term t -> fprintf fmt "%a" Expr.print t @@ -78,8 +73,6 @@ struct match r.v with | Arith t -> fprintf fmt "Arith(%s):[%a]" ARITH.name ARITH.print t - | Records t -> - fprintf fmt "Records(%s):[%a]" RECORDS.name RECORDS.print t | Bitv t -> fprintf fmt "Bitv(%s):[%a]" BITV.name BITV.print t | Adt t -> @@ -161,7 +154,6 @@ struct let hash r = let res = match r.v with | Arith x -> 1 + 10 * ARITH.hash x - | Records x -> 2 + 10 * RECORDS.hash x | Bitv x -> 3 + 10 * BITV.hash x | Adt x -> 6 + 10 * ADT.hash x | Ac ac -> 9 + 10 * AC.hash ac @@ -172,7 +164,6 @@ struct let eq r1 r2 = match r1.v, r2.v with | Arith x, Arith y -> ARITH.equal x y - | Records x, Records y -> RECORDS.equal x y | Bitv x, Bitv y -> BITV.equal x y | Adt x, Adt y -> ADT.equal x y | Term x, Term y -> Expr.equal x y @@ -198,9 +189,8 @@ struct (* end: Hconsing modules and functions *) 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 = Adt x; id = -1000 (* dummy *)} + let embed2 x = hcons {v = Bitv x; id = -1000 (* dummy *)} + let embed3 x = hcons {v = Adt x; id = -1000 (* dummy *)} let ac_embed ({ Sig.l; _ } as t) = match l with @@ -215,9 +205,8 @@ struct let term_embed t = hcons {v = Term t; id = -1000 (* dummy *)} 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=Adt r; _ } -> Some r | _ -> None + let extract2 = function { v=Bitv r; _ } -> Some r | _ -> None + let extract3 = function { v=Adt r; _ } -> Some r | _ -> None let ac_extract = function | { v = Ac t; _ } -> Some t @@ -226,7 +215,6 @@ struct let term_extract r = match r.v with | Arith _ -> ARITH.term_extract r - | Records _ -> RECORDS.term_extract r | Bitv _ -> BITV.term_extract r | Adt _ -> ADT.term_extract r | Ac _ -> None, false (* SYLVAIN : TODO *) @@ -236,7 +224,6 @@ struct let res = match r.v with | Arith _ -> ARITH.to_model_term r - | Records _ -> RECORDS.to_model_term r | Bitv _ -> BITV.to_model_term r | Adt _ -> ADT.to_model_term r | Term t when Expr.is_model_term t -> Some t @@ -251,7 +238,6 @@ struct let type_info = function | { v = Arith t; _ } -> ARITH.type_info t - | { v = Records t; _ } -> RECORDS.type_info t | { v = Bitv t; _ } -> BITV.type_info t | { v = Adt t; _ } -> ADT.type_info t | { v = Ac x; _ } -> AC.type_info x @@ -263,9 +249,8 @@ struct | Ac _ -> -1 | Term _ -> -2 | Arith _ -> -3 - | Records _ -> -4 - | Bitv _ -> -5 - | Adt _ -> -7 + | Bitv _ -> -4 + | Adt _ -> -5 let compare_tag a b = theory_num a - theory_num b @@ -274,7 +259,6 @@ struct else match a.v, b.v with | Arith _, Arith _ -> ARITH.compare a b - | Records _, Records _ -> RECORDS.compare a b | Bitv _, Bitv _ -> BITV.compare a b | Adt _, Adt _ -> ADT.compare a b | Term x, Term y -> Expr.compare x y @@ -289,7 +273,6 @@ struct | Term t -> Expr.hash t | Ac x -> AC.hash x | Arith x -> ARITH.hash x - | Records x -> RECORDS.hash x | Bitv x -> BITV.hash x | Arrays x -> ARRAYS.hash x | Adt x -> ADT.hash x @@ -318,7 +301,6 @@ struct let leaves r = match r.v with | Arith t -> ARITH.leaves t - | Records t -> RECORDS.leaves t | Bitv t -> BITV.leaves t | Adt t -> ADT.leaves t | Ac t -> r :: (AC.leaves t) @@ -327,7 +309,6 @@ struct let is_constant r = match r.v with | Arith t -> ARITH.is_constant t - | Records t -> RECORDS.is_constant t | Bitv t -> BITV.is_constant t | Adt t -> ADT.is_constant t | Term t -> @@ -344,7 +325,6 @@ struct if equal p v then r else match r.v with | Arith t -> ARITH.subst p v t - | Records t -> RECORDS.subst p v t | Bitv t -> BITV.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 @@ -355,32 +335,27 @@ struct let not_restricted = not @@ Options.get_restricted () in match ARITH.is_mine_symb sb, - not_restricted && RECORDS.is_mine_symb sb, not_restricted && BITV.is_mine_symb sb, not_restricted && ADT.is_mine_symb sb, AC.is_mine_symb sb with - | true, false, false, false, false -> + | true, false, false, false -> Timers.with_timer Timers.M_Arith Timers.F_make @@ fun () -> ARITH.make t - | false, true, false, false, false -> - Timers.with_timer Timers.M_Records Timers.F_make @@ fun () -> - RECORDS.make t - - | false, false, true, 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, false, true, false -> Timers.with_timer Timers.M_Adt Timers.F_make @@ fun () -> ADT.make t - | false, false, false, false, true -> + | 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 -> term_embed t, [] | _ -> assert false @@ -389,30 +364,26 @@ struct let not_restricted = not @@ Options.get_restricted () in match ARITH.is_mine_symb sb, - not_restricted && RECORDS.is_mine_symb sb, not_restricted && BITV.is_mine_symb sb, not_restricted && ADT.is_mine_symb sb, AC.is_mine_symb sb with - | true, false, false, false, false -> + | true, false, false, false -> ARITH.fully_interpreted sb - | false, true, false, false, false -> - RECORDS.fully_interpreted sb - | false, false, true, false, false -> + | false, true, false, false -> BITV.fully_interpreted sb - | false, false, false, true, false -> + | false, false, true, false -> ADT.fully_interpreted sb - | false, false, false, false, true -> + | false, false, false, true -> AC.fully_interpreted sb - | false, false, false, false, false -> + | false, false, false, false -> false | _ -> assert false let is_solvable_theory_symbol sb = ARITH.is_mine_symb sb || not (Options.get_restricted ()) && - (RECORDS.is_mine_symb sb || - BITV.is_mine_symb sb || + (BITV.is_mine_symb sb|| ADT.is_mine_symb sb) let is_a_leaf r = match r.v with @@ -426,18 +397,15 @@ struct | _ -> match ARITH.is_mine_symb ac.Sig.h, - RECORDS.is_mine_symb ac.Sig.h, BITV.is_mine_symb ac.Sig.h, ADT.is_mine_symb ac.Sig.h, AC.is_mine_symb ac.Sig.h with (*AC.is_mine may say F if Options.get_no_ac is set to F dynamically *) - | true, false, false, false, false -> + | true, false, false, false -> ARITH.color ac - | false, true, false, false, false -> - RECORDS.color ac - | false, false, true, false, false -> + | false, true, false, false -> BITV.color ac - | false, false, false, true, false -> + | false, false, true, false -> ADT.color ac | _ -> ac_embed ac @@ -445,7 +413,6 @@ struct Debug.debug_abstract_selectors a; match a.v with | Arith a -> ARITH.abstract_selectors a acc - | Records a -> RECORDS.abstract_selectors a acc | Bitv a -> BITV.abstract_selectors a acc | Adt a -> ADT.abstract_selectors a acc | Term _ -> a, acc @@ -527,10 +494,6 @@ struct Timers.with_timer ARITH.timer Timers.F_solve @@ fun () -> ARITH.solve ra rb pb - | Ty.Trecord _ -> - Timers.with_timer RECORDS.timer Timers.F_solve @@ fun () -> - RECORDS.solve ra rb pb - | Ty.Tbitv _ -> Timers.with_timer BITV.timer Timers.F_solve @@ fun () -> BITV.solve ra rb pb @@ -577,7 +540,6 @@ struct let opt = match r.v, type_info r with | _, Ty.Tint | _, Ty.Treal -> ARITH.assign_value r distincts eq - | _, Ty.Trecord _ -> RECORDS.assign_value r distincts eq | _, Ty.Tbitv _ -> BITV.assign_value r distincts eq | Term t, Ty.Tfarray _ -> begin @@ -642,24 +604,14 @@ and ARITH : Sig.SHOSTAK let embed = CX.embed1 end) -and RECORDS : Sig.SHOSTAK - with type r = CX.r - and type t = CX.r Records.abstract = - Records.Shostak - (struct - include CX - let extract = extract2 - let embed = embed2 - end) - and BITV : Sig.SHOSTAK with type r = CX.r and type t = CX.r Bitv.abstract = Bitv.Shostak (struct include CX - let extract = extract3 - let embed = embed3 + let extract = extract2 + let embed = embed2 end) and ADT : Sig.SHOSTAK @@ -668,8 +620,8 @@ and ADT : Sig.SHOSTAK Adt.Shostak (struct include CX - let extract = extract4 - let embed = embed4 + let extract = extract3 + let embed = embed3 end) (* Its signature is not Sig.SHOSTAK because it does not provide a solver *) @@ -711,7 +663,6 @@ module Combine = struct end module Arith = ARITH -module Records = RECORDS module Bitv = BITV module Adt = ADT module Polynome = TARITH diff --git a/src/lib/reasoners/shostak.mli b/src/lib/reasoners/shostak.mli index 0fdc94591..d8fd29fc7 100644 --- a/src/lib/reasoners/shostak.mli +++ b/src/lib/reasoners/shostak.mli @@ -40,9 +40,6 @@ module Polynome : Polynome.T module Arith : Sig.SHOSTAK with type r = Combine.r and type t = Polynome.t -module Records : Sig.SHOSTAK - with type r = Combine.r and type t = Combine.r Records.abstract - module Bitv : Sig.SHOSTAK with type r = Combine.r and type t = Combine.r Bitv.abstract diff --git a/src/lib/reasoners/theory.ml b/src/lib/reasoners/theory.ml index ad9ad7962..4a3544961 100644 --- a/src/lib/reasoners/theory.ml +++ b/src/lib/reasoners/theory.ml @@ -164,18 +164,12 @@ module Main_Default : S = struct | Tint | Treal | Tbool | Tbitv _ | Tfarray _ -> mp | Tvar _ -> assert false - | Text (_, hs) | Trecord { name = hs; _ } when - Ty_map.mem hs mp -> mp - + | Text (_, hs) when Ty_map.mem hs mp -> mp | Text (l, hs) -> let l = List.map (fun _ -> Ty.fresh_tvar()) l in Ty_map.add hs (Text(l, hs)) mp - | Trecord { name; _ } -> - (* cannot do better for records ? *) - Ty_map.add name ty mp - - | Tadt (hs, _) -> + | Tadt (hs, _, _) -> (* cannot do better for ADT ? *) Ty_map.add hs ty mp )sty Ty_map.empty @@ -189,20 +183,6 @@ module Main_Default : S = struct | Tint | Treal | Tbool | Tbitv _ | Tfarray _ -> () | Tvar _ -> assert false | Text _ -> print_dbg ~flushed:false "type %a@ " Ty.print ty - | Trecord { Ty.lbs; _ } -> - print_dbg ~flushed:false ~header:false "type %a = " Ty.print ty; - begin match lbs with - | [] -> assert false - | (lbl, ty)::l -> - let print fmt (lbl,ty) = - Format.fprintf fmt " ; %a :%a" - DE.Term.Const.print lbl Ty.print ty in - print_dbg ~flushed:false ~header:false - "{ %a : %a%a" - DE.Term.Const.print lbl Ty.print ty - (pp_list_no_space print) l; - print_dbg ~flushed:false ~header:false " }@ " - end | Tadt _ -> print_dbg ~flushed:false ~header:false "%a@ " Ty.print_full ty )types; diff --git a/src/lib/structures/expr.ml b/src/lib/structures/expr.ml index 3c5313c7d..c46535cf7 100644 --- a/src/lib/structures/expr.ml +++ b/src/lib/structures/expr.ml @@ -441,20 +441,6 @@ module SmtPrinter = struct pp x.let_e pp_boxed x.in_e - | Sy.(Op Record), _ -> - begin - match ty with - | Ty.Trecord { Ty.lbs = lbs; record_constr; _ } -> - assert (List.compare_lengths xs lbs = 0); - Fmt.pf ppf "@[<2>(%a %a@])" - DE.Term.Const.print record_constr - Fmt.(list ~sep:sp pp |> box) xs - - | _ -> - (* Excluded by the typechecker. *) - assert false - end - | Sy.Op op, [] -> Symbols.pp_smtlib_operator ppf op | Sy.Op Minus, [e1; { f = Sy.Real q; _ }] when is_zero e1.f -> @@ -616,7 +602,7 @@ module AEPrinter = struct assert false and pp_silent ppf t = - let { f ; xs ; ty; bind; _ } = t in + let { f ; xs ; bind; _ } = t in match f, xs with | Sy.Form form, xs -> pp_formula ppf form xs bind @@ -643,25 +629,6 @@ module AEPrinter = struct | Sy.(Op Extract (i, j)), [e] -> Fmt.pf ppf "%a^{%d, %d}" pp e i j - | Sy.(Op (Access field)), [e] -> - Fmt.pf ppf "%a.%a" pp e DE.Term.Const.print field - - | Sy.(Op Record), _ -> - begin match ty with - | Ty.Trecord { Ty.lbs = lbs; _ } -> - assert (List.compare_lengths xs lbs = 0); - Fmt.pf ppf "{"; - ignore (List.fold_left2 (fun first (field,_) e -> - Fmt.pf ppf "%s%a = %a" (if first then "" else "; ") - DE.Term.Const.print field pp e; - false - ) true lbs xs); - Fmt.pf ppf "}"; - | _ -> - (* Excluded by the typechecker. *) - assert false - end - | Sy.(Op ((Pow | Integer_round | Max_real | Min_real | Max_int | Min_int) as op)), [e1; e2] -> Fmt.pf ppf "%a(%a, %a)" Symbols.pp_ae_operator op pp e1 pp e2 @@ -1108,7 +1075,7 @@ let mk_ite cond th el = let rec is_model_term e = match e.f, e.xs with - | (Op Constr _ | Op Record | Op Set), xs -> List.for_all is_model_term xs + | (Op Constr _ | Op Set), xs -> List.for_all is_model_term xs | Op Div, [{ f = Real _; _ }; { f = Real _; _ }] -> true | Op Minus, [{ f = Real q; _ }; { f = Real _; _ }] -> Q.equal q Q.zero | Op Minus, [{ f = Int i; _ }; { f = Int _; _ }] -> Z.equal i Z.zero @@ -1317,8 +1284,6 @@ let mk_tester c t = | _ -> Fmt.invalid_arg "expected a constructor, got %a" DE.Id.print c -let mk_record xs ty = mk_term (Sy.Op Record) xs ty - let void = mk_constr Dolmen.Std.Expr.Term.Cstr.void [] Ty.tunit (** Substitutions *) @@ -1954,11 +1919,9 @@ module Triggers = struct | { f = Op (Get | Set) ; xs = [t1 ; t2]; _ } -> max (score_term t1) (score_term t2) - | { f = Op (Access _ | Destruct _ | Extract _) ; xs = [t]; _ } -> + | { f = Op (Destruct _ | Extract _) ; xs = [t]; _ } -> 1 + score_term t - | { f = Op Record; xs; _ } -> - 1 + (List.fold_left - (fun acc t -> max (score_term t) acc) 0 xs) + | { f = Op Set; xs = [t1; t2; t3]; _ } -> max (score_term t1) (max (score_term t2) (score_term t3)) @@ -2041,14 +2004,6 @@ module Triggers = struct | { f = Op Concat; _ }, _ -> -1 | _, { f = Op Concat; _ } -> 1 - | { f = Op (Access a1) ; xs=[t1]; _ }, - { f = Op (Access a2) ; xs=[t2]; _ } -> - let c = DE.Term.Const.compare a1 a2 in - if c<>0 then c else cmp_trig_term t1 t2 - - | { f = Op (Access _); _ }, _ -> -1 - | _, { f = Op (Access _); _ } -> 1 - | { f = Op (Destruct a1) ; xs = [t1]; _ }, { f = Op (Destruct a2) ; xs = [t2]; _ } -> let c = DE.Term.Const.compare a1 a2 in @@ -2057,11 +2012,6 @@ module Triggers = struct | { f = Op (Destruct _); _ }, _ -> -1 | _, { f =Op (Destruct _); _ } -> 1 - | { f = Op Record ; xs= lbs1; _ }, { f = Op Record ; xs = lbs2; _ } -> - Util.cmp_lists lbs1 lbs2 cmp_trig_term - | { f = Op Record; _ }, _ -> -1 - | _, { f = Op Record; _ } -> 1 - | { f = (Op _) as s1; xs=tl1; _ }, { f = (Op _) as s2; xs=tl2; _ } -> (* ops that are not infix or prefix *) let l1 = List.map score_term tl1 in diff --git a/src/lib/structures/expr.mli b/src/lib/structures/expr.mli index bb0460449..f070a42d3 100644 --- a/src/lib/structures/expr.mli +++ b/src/lib/structures/expr.mli @@ -294,11 +294,6 @@ val mk_constr : Dolmen.Std.Expr.term_cst -> t list -> Ty.t -> t [Nest.attach_orders]. *) val mk_tester : Dolmen.Std.Expr.term_cst -> t -> t -(** [mk_tester c e] produces the tester expression ((_ is c) e). - - @raise Invalid_argument if [c] is not a Dolmen constructor. *) - -val mk_record : t list -> Ty.t -> t (** Substitutions *) diff --git a/src/lib/structures/symbols.ml b/src/lib/structures/symbols.ml index 87e47fb45..a848d7092 100644 --- a/src/lib/structures/symbols.ml +++ b/src/lib/structures/symbols.ml @@ -37,8 +37,7 @@ type operator = (* Arithmetic *) | Plus | Minus | Mult | Div | Modulo | Pow (* ADTs *) - | Access of DE.term_cst | Record - | Constr of DE.term_cst (* enums, adts *) + | Constr of DE.term_cst | Destruct of DE.term_cst (* Arrays *) | Get | Set @@ -188,7 +187,7 @@ let compare_kinds k1 k2 = let compare_operators op1 op2 = Util.compare_algebraic op1 op2 (function - | Access h1, Access h2 | Constr h1, Constr h2 + | Constr h1, Constr h2 | Destruct h1, Destruct h2 -> DE.Term.Const.compare h1 h2 | Extract (i1, j1), Extract (i2, j2) -> @@ -200,7 +199,7 @@ let compare_operators op1 op2 = | Int2BV n1, Int2BV n2 -> Int.compare n1 n2 | _ , (Plus | Minus | Mult | Div | Modulo | Real_is_int | Concat | Extract _ | Sign_extend _ | Repeat _ | Get | Set | Float - | Access _ | Record | Sqrt_real | Abs_int | Abs_real + | Sqrt_real | Abs_int | Abs_real | Real_of_int | Int_floor | Int_ceil | Sqrt_real_default | Sqrt_real_excess | Min_real | Min_int | Max_real | Max_int | Integer_log2 | Pow | Integer_round @@ -380,8 +379,6 @@ module AEPrinter = struct | Set -> Fmt.pf ppf "set" (* DT theory *) - | Record -> Fmt.pf ppf "@Record" - | Access tcst -> Fmt.pf ppf "@Access_%a" DE.Term.Const.print tcst | Constr tcst | Destruct tcst -> DE.Term.Const.print ppf tcst @@ -489,9 +486,7 @@ module SmtPrinter = struct | Set -> Fmt.pf ppf "store" (* DT theory *) - | Record -> () - | Access tcst | Constr tcst | Destruct tcst -> - DE.Term.Const.print ppf tcst + | Constr tcst | Destruct tcst -> DE.Term.Const.print ppf tcst (* Float theory *) | Float -> Fmt.pf ppf "ae.round" diff --git a/src/lib/structures/symbols.mli b/src/lib/structures/symbols.mli index eb93fb3e7..ac99780d8 100644 --- a/src/lib/structures/symbols.mli +++ b/src/lib/structures/symbols.mli @@ -35,8 +35,7 @@ type operator = (* Arithmetic *) | Plus | Minus | Mult | Div | Modulo | Pow (* ADTs *) - | Access of Dolmen.Std.Expr.term_cst | Record - | Constr of Dolmen.Std.Expr.term_cst (* enums, adts *) + | Constr of Dolmen.Std.Expr.term_cst | Destruct of Dolmen.Std.Expr.term_cst (* Arrays *) | Get | Set diff --git a/src/lib/structures/ty.ml b/src/lib/structures/ty.ml index 1d1fd4730..18a54350a 100644 --- a/src/lib/structures/ty.ml +++ b/src/lib/structures/ty.ml @@ -40,16 +40,7 @@ type t = | Tbitv of int | Text of t list * DE.ty_cst | Tfarray of t * t - | Tadt of DE.ty_cst * t list - | Trecord of trecord - -and trecord = { - mutable args : t list; - name : DE.ty_cst; - mutable lbs : (DE.term_cst * t) list; - record_constr : DE.term_cst; - (* for ADTs that become records. default is "{" *) -} + | Tadt of DE.ty_cst * t list * bool module Smtlib = struct let rec pp ppf = function @@ -59,11 +50,9 @@ 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) - | Trecord { args = []; name; _ } | Tadt (name, []) -> + | Text ([], name) | Tadt (name, [], _) -> DE.Ty.Const.print ppf name - | Text (args, name) - | Trecord { args; name; _ } | Tadt (name, args) -> + | Text (args, name) | Tadt (name, args, _) -> Fmt.(pf ppf "(@[%a %a@])" DE.Ty.Const.print name (list ~sep:sp pp) args) | Tvar tv -> DE.Ty.Var.print ppf tv end @@ -111,22 +100,7 @@ let print_generic body_of = fprintf fmt "%a %a" print_list l DE.Ty.Const.print s | Tfarray (t1, t2) -> fprintf fmt "(%a,%a) farray" (print body_of) t1 (print body_of) t2 - | Trecord { args = lv; name = n; lbs = lbls; _ } -> - begin - fprintf fmt "%a %a" print_list lv DE.Ty.Const.print n; - if body_of != None then begin - fprintf fmt " = {"; - let first = ref true in - List.iter - (fun (s, t) -> - fprintf fmt "%s%a : %a" (if !first then "" else "; ") - DE.Term.Const.print s (print body_of) t; - first := false - ) lbls; - fprintf fmt "}" - end - end - | Tadt (n, lv) -> + | Tadt (n, lv, _) -> fprintf fmt "%a %a" print_list lv DE.Ty.Const.print n; begin match body_of with | None -> () @@ -193,17 +167,7 @@ let rec compare t1 t2 = if c<>0 then c else compare ta2 tb2 | Tfarray _, _ -> -1 | _ , Tfarray _ -> 1 - | Trecord { args = a1; name = s1; lbs = l1; _ }, - Trecord { args = a2; name = s2; lbs = l2; _ } -> - let c = DE.Ty.Const.compare s1 s2 in - if c <> 0 then c else - let c = compare_list a1 a2 in - if c <> 0 then c else - let l1, l2 = List.map snd l1, List.map snd l2 in - compare_list l1 l2 - | Trecord _, _ -> -1 | _ , Trecord _ -> 1 - - | Tadt (s1, pars1), Tadt (s2, pars2) -> + | Tadt (s1, pars1, _), Tadt (s2, pars2, _) -> let c = DE.Ty.Const.compare s1 s2 in if c <> 0 then c else compare_list pars1 pars2 @@ -239,20 +203,10 @@ let rec equal t1 t2 = with Invalid_argument _ -> false) | Tfarray (ta1, ta2), Tfarray (tb1, tb2) -> equal ta1 tb1 && equal ta2 tb2 - | Trecord { args = a1; name = s1; lbs = l1; _ }, - Trecord { args = a2; name = s2; lbs = l2; _ } -> - begin - try - DE.Ty.Const.equal s1 s2 && List.for_all2 equal a1 a2 && - List.for_all2 - (fun (l1, ty1) (l2, ty2) -> - DE.Term.Const.equal l1 l2 && equal ty1 ty2) l1 l2 - with Invalid_argument _ -> false - end | Tint, Tint | Treal, Treal | Tbool, Tbool -> true | Tbitv n1, Tbitv n2 -> n1 =n2 - | Tadt (s1, pars1), Tadt (s2, pars2) -> + | Tadt (s1, pars1, _), Tadt (s2, pars2, _) -> begin try DE.Ty.Const.equal s1 s2 && List.for_all2 equal pars1 pars2 with Invalid_argument _ -> false @@ -278,13 +232,9 @@ let rec matching s pat t = List.fold_left2 matching s l1 l2 | Tfarray (ta1,ta2), Tfarray (tb1,tb2) -> matching (matching s ta1 tb1) ta2 tb2 - | Trecord r1, Trecord r2 when DE.Ty.Const.equal r1.name r2.name -> - 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 | Tint , Tint | Tbool , Tbool | Treal , Treal -> s | Tbitv n , Tbitv m when n=m -> s - | Tadt(n1, args1), Tadt(n2, args2) when DE.Ty.Const.equal n1 n2 -> + | Tadt(n1, args1, _), Tadt(n2, args2, _) when DE.Ty.Const.equal n1 n2 -> List.fold_left2 matching s args1 args2 | _ , _ -> raise (TypeClash(pat,t)) @@ -304,20 +254,10 @@ let apply_subst = let t2' = apply_subst s t2 in if t1 == t1' && t2 == t2' then ty else Tfarray (t1', t2') - | Trecord r -> - let lbs, same1 = My_list.apply_right (apply_subst s) r.lbs in - let args, same2 = My_list.apply (apply_subst s) r.args in - if same1 && same2 then ty - else - Trecord - {r with args = args; - name = r.name; - lbs = lbs} - - | Tadt(name, params) + | Tadt(name, params, record) [@ocaml.ppwarning "TODO: detect when there are no changes "] -> - Tadt (name, List.map (apply_subst s) params) + Tadt (name, List.map (apply_subst s) params, record) | Tint | Treal | Tbool | Tbitv _ -> ty in @@ -339,18 +279,9 @@ let rec fresh ty subst = let ty1, subst = fresh ty1 subst in let ty2, subst = fresh ty2 subst in Tfarray (ty1, ty2), subst - | Trecord ({ args; name = n; lbs; _ } as r) -> + | Tadt(s,args, record) -> let args, subst = fresh_list args subst in - let lbs, subst = - List.fold_right - (fun (x,ty) (lbs, subst) -> - let ty, subst = fresh ty subst in - (x, ty)::lbs, subst) lbs ([], subst) - in - Trecord {r with args = args; name = n; lbs = lbs}, subst - | Tadt(s, args) -> - let args, subst = fresh_list args subst in - Tadt (s, args), subst + Tadt (s,args, record), subst | t -> t, subst and fresh_list lty subst = @@ -466,8 +397,8 @@ let fresh_empty_text = in text [] id -let t_adt ?(body=None) s ty_vars = - let ty = Tadt (s, ty_vars) in +let t_adt ?(record=false) ?(body=None) s ty_vars = + let ty = Tadt (s, ty_vars, record) in begin match body with | None -> () | Some [] -> assert false @@ -497,23 +428,13 @@ let tunit = let ty = t_adt ~body DE.Ty.Const.unit [] in ty -let trecord ~record_constr lv name lbs = - Trecord { record_constr; args = lv; name; lbs = lbs} - let rec hash t = match t with | Tvar tv -> DE.Ty.Var.hash tv | Text(l,s) -> abs (List.fold_left (fun acc x-> acc*19 + hash x) (DE.Ty.Const.hash s) l) | Tfarray (t1,t2) -> 19 * (hash t1) + 23 * (hash t2) - | Trecord { args; name = s; _ } -> - (* We do not hash constructors. *) - let h = - List.fold_left (fun h ty -> 27 * h + hash ty) (DE.Ty.Const.hash s) args - in - abs h - - | Tadt (ty, args) -> + | Tadt (ty, args, _) -> (* We do not hash constructors. *) let h = List.fold_left (fun h ty -> 31 * h + hash ty) (DE.Ty.Const.hash ty) args @@ -541,10 +462,7 @@ let vty_of t = | Tvar tv -> TvSet.add tv acc | Text (l,_) -> List.fold_left vty_of_rec acc l | Tfarray (t1,t2) -> vty_of_rec (vty_of_rec acc t1) t2 - | Trecord { args; lbs; _ } -> - let acc = List.fold_left vty_of_rec acc args in - List.fold_left (fun acc (_, ty) -> vty_of_rec acc ty) acc lbs - | Tadt(_, args) -> + | Tadt(_, args, _) -> List.fold_left vty_of_rec acc args | Tint | Treal | Tbool | Tbitv _ -> diff --git a/src/lib/structures/ty.mli b/src/lib/structures/ty.mli index 168c95b69..75c855d8b 100644 --- a/src/lib/structures/ty.mli +++ b/src/lib/structures/ty.mli @@ -57,7 +57,7 @@ type t = (** Functional arrays. [TFarray (src,dst)] maps values of type [src] to values of type [dst]. *) - | Tadt of Dolmen.Std.Expr.ty_cst * t list + | Tadt of Dolmen.Std.Expr.ty_cst * t list * bool (** Application of algebraic data types. [Tadt (a, params)] denotes the application of the polymorphic datatype [a] to the types parameters [params]. @@ -66,23 +66,6 @@ type t = value [Tadt (Hstring.make "list", [Tint]] where the identifier {e list} denotes a polymorphic ADT defined by the user with [t_adt]. *) - | Trecord of trecord - (** Record type. *) - -and trecord = { - mutable args : t list; - (** Arguments passed to the record constructor *) - name : Dolmen.Std.Expr.ty_cst; - (** Name of the record type *) - mutable lbs : (Dolmen.Std.Expr.term_cst * t) list; - (** List of fields of the record. Each field has a name, - and an associated type. *) - record_constr : Dolmen.Std.Expr.term_cst; - (** record constructor. Useful is case it's a specialization of an - algeberaic datatype. Default value is "\{__[name]" *) -} -(** Record types. *) - type adt_constr = { constr : Dolmen.Std.Expr.term_cst ; (** constructor of an ADT type *) @@ -155,6 +138,7 @@ val text : t list -> Dolmen.Std.Expr.ty_cst -> t given. *) val t_adt : + ?record:bool -> ?body:((Dolmen.Std.Expr.term_cst * (Dolmen.Std.Expr.term_cst * t) list) list) option -> Dolmen.Std.Expr.ty_cst -> @@ -167,17 +151,6 @@ val t_adt : argument is the name of the type. The third one provides its list of arguments. *) -val trecord : - record_constr:Dolmen.Std.Expr.term_cst -> - t list -> Dolmen.Std.Expr.ty_cst -> (Dolmen.Std.Expr.term_cst * t) list -> t -(** Create a record type. [trecord args name lbs] creates a record - type with name [name], arguments [args] and fields [lbs]. - - If [sort_fields] is true, the record fields are sorted according to - [Hstring.compare]. This is to preserve compatibility with the old - typechecker behavior and should not be used in new code. *) - - (** {2 Substitutions} *) type subst = t TvMap.t From 8cac7a8a983263740de50c79fd95c1b9a69a2802 Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Tue, 22 Oct 2024 17:19:11 +0200 Subject: [PATCH 02/14] Remove useless flag in adt type --- src/lib/frontend/translate.ml | 4 ++-- src/lib/reasoners/adt.ml | 4 ++-- src/lib/reasoners/adt_rel.ml | 6 +++--- src/lib/reasoners/theory.ml | 2 +- src/lib/structures/ty.ml | 30 +++++++++++++++--------------- src/lib/structures/ty.mli | 7 ++----- 6 files changed, 25 insertions(+), 28 deletions(-) diff --git a/src/lib/frontend/translate.ml b/src/lib/frontend/translate.ml index 5d7bd7a91..c2b4df693 100644 --- a/src/lib/frontend/translate.ml +++ b/src/lib/frontend/translate.ml @@ -523,7 +523,7 @@ and handle_ty_app ?(update = false) ty_c l = (* Recover the initial versions of the types and apply them on the provided type arguments stored in [tyl]. *) match Cache.find_ty ty_c with - | Tadt (hs, _, record) -> Tadt (hs, tyl, record) + | Tadt (hs, _) -> Tadt (hs, tyl ) | Text (_, s) -> Text (tyl, s) | _ -> assert false @@ -586,7 +586,7 @@ let mk_term_decl ({ id_ty; path; tags; _ } as tcst: DE.term_cst) = let mk_mr_ty_decls (tdl: DE.ty_cst list) = let handle_ty_decl (ty: Ty.t) (tdef: DE.Ty.def option) = match ty, tdef with - | Tadt (hs, tyl, _), Some (Adt { cases; ty = ty_c; _ }) -> + | Tadt (hs, tyl), Some (Adt { cases; ty = ty_c; _ }) -> let cs = Array.fold_right ( fun DE.{ cstr; dstrs; _ } accl -> diff --git a/src/lib/reasoners/adt.ml b/src/lib/reasoners/adt.ml index 92ebde84b..d9df614c4 100644 --- a/src/lib/reasoners/adt.ml +++ b/src/lib/reasoners/adt.ml @@ -62,7 +62,7 @@ let constr_of_destr ty dest = ~module_name:"Adt" ~function_name:"constr_of_destr" "ty = %a" Ty.print ty; match ty with - | Ty.Tadt (s, params, _) -> + | Ty.Tadt (s, params) -> begin let cases = Ty.type_body s params in try @@ -182,7 +182,7 @@ module Shostak (X : ALIEN) = struct in let xs = List.rev sx in match f, xs, ty with - | Sy.Op Sy.Constr hs, _, Ty.Tadt (name, params, _) -> + | Sy.Op Sy.Constr hs, _, Ty.Tadt (name, params) -> let cases = Ty.type_body name params in let case_hs = try Ty.assoc_destrs hs cases with Not_found -> assert false diff --git a/src/lib/reasoners/adt_rel.ml b/src/lib/reasoners/adt_rel.ml index bafcb9a09..87e10b0bc 100644 --- a/src/lib/reasoners/adt_rel.ml +++ b/src/lib/reasoners/adt_rel.ml @@ -93,7 +93,7 @@ module Domain = struct let unknown ty = match ty with - | Ty.Tadt (name, params, _) -> + | 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 constrs = @@ -462,7 +462,7 @@ let build_constr_eq r c = match Th.embed r with | Alien r -> begin match X.type_info r with - | Ty.Tadt (name, params, _) as ty -> + | Ty.Tadt (name, params) as ty -> let cases = Ty.type_body name params in let ds = try Ty.assoc_destrs c cases with Not_found -> assert false @@ -548,7 +548,7 @@ let two = Numbers.Q.from_int 2 (* TODO: we should compute this reverse map in `Ty` and store it there. *) let constr_of_destr ty d = match ty with - | Ty.Tadt (name, params, _) -> + | Ty.Tadt (name, params) -> begin let cases = Ty.type_body name params in try diff --git a/src/lib/reasoners/theory.ml b/src/lib/reasoners/theory.ml index 4a3544961..9a6905d3f 100644 --- a/src/lib/reasoners/theory.ml +++ b/src/lib/reasoners/theory.ml @@ -169,7 +169,7 @@ module Main_Default : S = struct let l = List.map (fun _ -> Ty.fresh_tvar()) l in Ty_map.add hs (Text(l, hs)) mp - | Tadt (hs, _, _) -> + | Tadt (hs, _) -> (* cannot do better for ADT ? *) Ty_map.add hs ty mp )sty Ty_map.empty diff --git a/src/lib/structures/ty.ml b/src/lib/structures/ty.ml index 18a54350a..7111f2244 100644 --- a/src/lib/structures/ty.ml +++ b/src/lib/structures/ty.ml @@ -40,7 +40,7 @@ type t = | Tbitv of int | Text of t list * DE.ty_cst | Tfarray of t * t - | Tadt of DE.ty_cst * t list * bool + | Tadt of DE.ty_cst * t list module Smtlib = struct let rec pp ppf = function @@ -50,9 +50,9 @@ 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) | Tadt (name, [], _) -> + | Text ([], name) | Tadt (name, []) -> DE.Ty.Const.print ppf name - | Text (args, name) | Tadt (name, args, _) -> + | Text (args, name) | Tadt (name, args) -> Fmt.(pf ppf "(@[%a %a@])" DE.Ty.Const.print name (list ~sep:sp pp) args) | Tvar tv -> DE.Ty.Var.print ppf tv end @@ -100,7 +100,7 @@ let print_generic body_of = fprintf fmt "%a %a" print_list l DE.Ty.Const.print s | Tfarray (t1, t2) -> fprintf fmt "(%a,%a) farray" (print body_of) t1 (print body_of) t2 - | Tadt (n, lv, _) -> + | Tadt (n, lv) -> fprintf fmt "%a %a" print_list lv DE.Ty.Const.print n; begin match body_of with | None -> () @@ -167,7 +167,7 @@ let rec compare t1 t2 = if c<>0 then c else compare ta2 tb2 | Tfarray _, _ -> -1 | _ , Tfarray _ -> 1 - | Tadt (s1, pars1, _), Tadt (s2, pars2, _) -> + | Tadt (s1, pars1), Tadt (s2, pars2) -> let c = DE.Ty.Const.compare s1 s2 in if c <> 0 then c else compare_list pars1 pars2 @@ -206,7 +206,7 @@ let rec equal t1 t2 = | Tint, Tint | Treal, Treal | Tbool, Tbool -> true | Tbitv n1, Tbitv n2 -> n1 =n2 - | Tadt (s1, pars1, _), Tadt (s2, pars2, _) -> + | Tadt (s1, pars1), Tadt (s2, pars2) -> begin try DE.Ty.Const.equal s1 s2 && List.for_all2 equal pars1 pars2 with Invalid_argument _ -> false @@ -234,7 +234,7 @@ let rec matching s pat t = matching (matching s ta1 tb1) ta2 tb2 | Tint , Tint | Tbool , Tbool | Treal , Treal -> s | Tbitv n , Tbitv m when n=m -> s - | Tadt(n1, args1, _), Tadt(n2, args2, _) when DE.Ty.Const.equal n1 n2 -> + | Tadt(n1, args1), Tadt(n2, args2) when DE.Ty.Const.equal n1 n2 -> List.fold_left2 matching s args1 args2 | _ , _ -> raise (TypeClash(pat,t)) @@ -254,10 +254,10 @@ let apply_subst = let t2' = apply_subst s t2 in if t1 == t1' && t2 == t2' then ty else Tfarray (t1', t2') - | Tadt(name, params, record) + | Tadt(name, params) [@ocaml.ppwarning "TODO: detect when there are no changes "] -> - Tadt (name, List.map (apply_subst s) params, record) + Tadt (name, List.map (apply_subst s) params) | Tint | Treal | Tbool | Tbitv _ -> ty in @@ -279,9 +279,9 @@ let rec fresh ty subst = let ty1, subst = fresh ty1 subst in let ty2, subst = fresh ty2 subst in Tfarray (ty1, ty2), subst - | Tadt(s,args, record) -> + | Tadt(s,args) -> let args, subst = fresh_list args subst in - Tadt (s,args, record), subst + Tadt (s,args), subst | t -> t, subst and fresh_list lty subst = @@ -397,8 +397,8 @@ let fresh_empty_text = in text [] id -let t_adt ?(record=false) ?(body=None) s ty_vars = - let ty = Tadt (s, ty_vars, record) in +let t_adt ?(body=None) s ty_vars = + let ty = Tadt (s, ty_vars) in begin match body with | None -> () | Some [] -> assert false @@ -434,7 +434,7 @@ let rec hash t = | Text(l,s) -> abs (List.fold_left (fun acc x-> acc*19 + hash x) (DE.Ty.Const.hash s) l) | Tfarray (t1,t2) -> 19 * (hash t1) + 23 * (hash t2) - | Tadt (ty, args, _) -> + | Tadt (ty, args) -> (* We do not hash constructors. *) let h = List.fold_left (fun h ty -> 31 * h + hash ty) (DE.Ty.Const.hash ty) args @@ -462,7 +462,7 @@ let vty_of t = | Tvar tv -> TvSet.add tv acc | Text (l,_) -> List.fold_left vty_of_rec acc l | Tfarray (t1,t2) -> vty_of_rec (vty_of_rec acc t1) t2 - | Tadt(_, args, _) -> + | Tadt(_, args) -> List.fold_left vty_of_rec acc args | Tint | Treal | Tbool | Tbitv _ -> diff --git a/src/lib/structures/ty.mli b/src/lib/structures/ty.mli index 75c855d8b..fef2ee068 100644 --- a/src/lib/structures/ty.mli +++ b/src/lib/structures/ty.mli @@ -57,7 +57,7 @@ type t = (** Functional arrays. [TFarray (src,dst)] maps values of type [src] to values of type [dst]. *) - | Tadt of Dolmen.Std.Expr.ty_cst * t list * bool + | Tadt of Dolmen.Std.Expr.ty_cst * t list (** Application of algebraic data types. [Tadt (a, params)] denotes the application of the polymorphic datatype [a] to the types parameters [params]. @@ -75,10 +75,8 @@ type adt_constr = their respective types *) } -(** Bodies of types definitions. Currently, bodies are inlined in the - type [t] for records and enumerations. But, this is not possible - for recursive ADTs *) type type_body = adt_constr list +(** Bodies of types definitions. *) module Set : Set.S with type elt = t (** Sets of types *) @@ -138,7 +136,6 @@ val text : t list -> Dolmen.Std.Expr.ty_cst -> t given. *) val t_adt : - ?record:bool -> ?body:((Dolmen.Std.Expr.term_cst * (Dolmen.Std.Expr.term_cst * t) list) list) option -> Dolmen.Std.Expr.ty_cst -> From 6ff0e4176e5ea87418f6d9bc673ed7a70174cbae Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Tue, 22 Oct 2024 17:26:10 +0200 Subject: [PATCH 03/14] Remove more dead code --- src/lib/reasoners/records.ml | 420 ------------------------------ src/lib/reasoners/records.mli | 37 --- src/lib/reasoners/records_rel.ml | 49 ---- src/lib/reasoners/records_rel.mli | 29 --- src/lib/structures/expr.mli | 1 - src/lib/structures/profiling.ml | 16 +- src/lib/structures/ty.ml | 8 - src/lib/util/timers.ml | 6 - src/lib/util/timers.mli | 2 - src/lib/util/util.ml | 6 - src/lib/util/util.mli | 2 - 11 files changed, 1 insertion(+), 575 deletions(-) delete mode 100644 src/lib/reasoners/records.ml delete mode 100644 src/lib/reasoners/records.mli delete mode 100644 src/lib/reasoners/records_rel.ml delete mode 100644 src/lib/reasoners/records_rel.mli diff --git a/src/lib/reasoners/records.ml b/src/lib/reasoners/records.ml deleted file mode 100644 index bc6c2a452..000000000 --- a/src/lib/reasoners/records.ml +++ /dev/null @@ -1,420 +0,0 @@ -(**************************************************************************) -(* *) -(* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) --- OCamlPro SAS *) -(* *) -(* This file is distributed under the terms of OCamlPro *) -(* Non-Commercial Purpose License, version 1. *) -(* *) -(* As an exception, Alt-Ergo Club members at the Gold level can *) -(* use this file under the terms of the Apache Software License *) -(* version 2.0. *) -(* *) -(* --------------------------------------------------------------- *) -(* *) -(* The Alt-Ergo theorem prover *) -(* *) -(* Sylvain Conchon, Evelyne Contejean, Francois Bobot *) -(* Mohamed Iguernelala, Stephane Lescuyer, Alain Mebsout *) -(* *) -(* CNRS - INRIA - Universite Paris Sud *) -(* *) -(* --------------------------------------------------------------- *) -(* *) -(* More details can be found in the directory licenses/ *) -(* *) -(**************************************************************************) - -module E = Expr -module Sy = Symbols -module DE = Dolmen.Std.Expr - -type 'a abstract = - | Record of (DE.term_cst * 'a abstract) list * Ty.t - | Access of DE.term_cst * 'a abstract * Ty.t - | Other of 'a * Ty.t - -module type ALIEN = sig - include Sig.X - val embed : r abstract -> r - val extract : r -> (r abstract) option -end - -module Shostak (X : ALIEN) = struct - - module XS = Set.Make(struct type t = X.r let compare = X.hash_cmp end) - - let name = "records" - - let timer = Timers.M_Records - - type t = X.r abstract - type r = X.r - - (*BISECT-IGNORE-BEGIN*) - module Debug = struct - - let rec print fmt = function - | Record (lbs, _) -> - Format.fprintf fmt "{"; - let _ = List.fold_left - (fun first (lb, e) -> - Format.fprintf fmt "%s%a = %a" - (if first then "" else "; ") DE.Term.Const.print lb print e; - false - ) true lbs in - Format.fprintf fmt "}" - | Access(a, e, _) -> - Format.fprintf fmt "%a.%a" print e DE.Term.Const.print a - | Other(t, _) -> X.print fmt t - - end - (*BISECT-IGNORE-END*) - - let print = Debug.print - - let rec raw_compare r1 r2 = - match r1, r2 with - | Other (u1, ty1), Other (u2, ty2) -> - let c = Ty.compare ty1 ty2 in - if c <> 0 then c else X.str_cmp u1 u2 - | Other _, _ -> -1 - | _, Other _ -> 1 - | Access (tcst1, u1, ty1), Access (tcst2, u2, ty2) -> - let c = Ty.compare ty1 ty2 in - if c <> 0 then c - else - let c = DE.Term.Const.compare tcst1 tcst2 in - if c <> 0 then c - else raw_compare u1 u2 - | Access _, _ -> -1 - | _, Access _ -> 1 - | Record (lbs1, ty1), Record (lbs2, ty2) -> - let c = Ty.compare ty1 ty2 in - if c <> 0 then c else raw_compare_list lbs1 lbs2 - - and raw_compare_list l1 l2 = - match l1, l2 with - | [], [] -> 0 - | [], _ -> 1 - | _, [] -> -1 - | (_, x1)::l1, (_, x2)::l2 -> - let c = raw_compare x1 x2 in - if c<>0 then c else raw_compare_list l1 l2 - - let rec normalize v = - match v with - | Record (lbs, ty) -> - begin - let lbs_n = List.map (fun (lb, x) -> lb, normalize x) lbs in - match lbs_n with - | (lb1, Access(lb2, x, _)) :: l when DE.Term.Const.equal lb1 lb2 -> - if List.for_all - (function - | (lb1, Access(lb2, y, _)) -> - DE.Term.Const.equal lb1 lb2 && raw_compare x y = 0 - | _ -> false) l - then x - else Record (lbs_n, ty) - | _ -> Record (lbs_n, ty) - end - | Access (a, x, ty) -> - begin - match normalize x with - | Record (lbs, _) -> My_list.assoc DE.Term.Const.equal a lbs - | x_n -> Access (a, x_n, ty) - end - | Other _ -> v - - let embed r = - match X.extract r with - | Some p -> p - | None -> Other(r, X.type_info r) - - let compare_mine t u = raw_compare (normalize t) (normalize u) - - let compare x y = compare_mine (embed x) (embed y) - - let rec equal r1 r2 = - match r1, r2 with - | Other (u1, ty1), Other (u2, ty2) -> - Ty.equal ty1 ty2 && X.equal u1 u2 - - | Access (s1, u1, ty1), Access (s2, u2, ty2) -> - DE.Term.Const.equal s1 s2 && Ty.equal ty1 ty2 && equal u1 u2 - - | Record (lbs1, ty1), Record (lbs2, ty2) -> - Ty.equal ty1 ty2 && equal_list lbs1 lbs2 - - | Other _, _ | _, Other _ | Access _, _ | _, Access _ -> false - - and equal_list l1 l2 = - try List.for_all2 (fun (_,r1) (_,r2) -> equal r1 r2) l1 l2 - with Invalid_argument _ -> false - - let is_mine t = - match normalize t with - | Other(r, _) -> r - | x -> X.embed x - - let type_info = function - | Record (_, ty) | Access (_, _, ty) | Other (_, ty) -> ty - - let make t = - let rec make_rec t ctx = - let { E.f; xs; ty; _ } = E.term_view t in - match f, ty with - | Symbols.Op (Symbols.Record), Ty.Trecord { Ty.lbs; _ } -> - assert (List.length xs = List.length lbs); - let l, ctx = - List.fold_right2 - (fun x (lb, _) (l, ctx) -> - let r, ctx = make_rec x ctx in - let tyr = type_info r in - let dlb = E.mk_term (Symbols.Op (Symbols.Access lb)) [t] tyr in - let c = E.mk_eq ~iff:false dlb x in - (lb, r)::l, c::ctx - ) - xs lbs ([], ctx) - in - Record (l, ty), ctx - | Symbols.Op (Symbols.Access a), _ -> - begin - match xs with - | [x] -> - let r, ctx = make_rec x ctx in - Access (a, r, ty), ctx - | _ -> assert false - end - - | _, _ -> - let r, ctx' = X.make t in - Other (r, ty), ctx'@ctx - in - let r, ctx = make_rec t [] in - let is_m = is_mine r in - is_m, ctx - - let color _ = assert false - - let embed r = - match X.extract r with - | Some p -> p - | None -> Other(r, X.type_info r) - - let xs_of_list = List.fold_left (fun s x -> XS.add x s) XS.empty - - let leaves t = - let rec leaves t = - match normalize t with - | Record (lbs, _) -> - List.fold_left (fun s (_, x) -> XS.union (leaves x) s) XS.empty lbs - | Access (_, x, _) -> leaves x - | Other (x, _) -> xs_of_list (X.leaves x) - in - XS.elements (leaves t) - - let is_constant = - let rec is_constant t = - match normalize t with - | Record (lbs, _) -> - List.for_all (fun (_, x) -> is_constant x) lbs - | Access (_, x, _) -> is_constant x - | Other (x, _) -> X.is_constant x - in is_constant - - let rec hash = function - | Record (lbs, ty) -> - List.fold_left - (fun h (lb, x) -> 17 * hash x + 13 * DE.Term.Const.hash lb + h) - (Ty.hash ty) lbs - | Access (a, x, ty) -> - 19 * hash x + 17 * DE.Term.Const.hash a + Ty.hash ty - | Other (x, ty) -> - Ty.hash ty + 23 * X.hash x - - let rec subst_rec p v r = - match r with - | Other (t, _) -> - embed (if X.equal p t then v else X.subst p v t) - | Access (a, t, ty) -> - Access (a, subst_rec p v t, ty) - | Record (lbs, ty) -> - let lbs = List.map (fun (lb, t) -> lb, subst_rec p v t) lbs in - Record (lbs, ty) - - let subst p v r = is_mine (subst_rec p v r) - - let is_mine_symb sy = - match sy with - | Symbols.Op (Symbols.Record | Symbols.Access _) -> true - | _ -> false - - let abstract_access field e ty acc = - let xe = is_mine e in - let abs_right_xe, acc = - try My_list.assoc X.equal xe acc, acc - with Not_found -> - let left_abs_xe2, acc = X.abstract_selectors xe acc in - match X.type_info left_abs_xe2 with - | (Ty.Trecord { Ty.lbs; _ }) as tyr -> - let flds = - List.map - (fun (lb,ty) -> lb, embed (X.term_embed (E.fresh_name ty))) lbs - in - let record = is_mine (Record (flds, tyr)) in - record, (left_abs_xe2, record) :: acc - | ty -> - Fmt.failwith - "Not a record type: `%a" Ty.print_full ty - in - let abs_access = normalize (Access (field, embed abs_right_xe, ty)) in - is_mine abs_access, acc - - let abstract_selectors v acc = - match v with - (* Handled by combine. Should not happen! *) - | Other _ -> assert false - - (* This is not a selector *) - | Record (fields,ty) -> - let flds, acc = - List.fold_left - (fun (flds,acc) (lbl,e) -> - let e, acc = X.abstract_selectors (is_mine e) acc in - (lbl, embed e)::flds, acc - )([], acc) fields - [@ocaml.ppwarning "TODO: should not rebuild if not changed !"] - in - is_mine (Record (List.rev flds, ty)), acc - - (* Selector ! Interesting case !*) - | Access (field, e, ty) -> abstract_access field e ty acc - - - (* Shostak'pair solver adapted to records *) - - (* unused -- - let mk_fresh_record x info = - let ty = type_info x in - let lbs = match ty with Ty.Trecord r -> r.Ty.lbs | _ -> assert false in - let lbs = - List.map - (fun (lb, ty) -> - match info with - | Some (a, v) when Uid.equal lb a -> lb, v - | _ -> let n = embed (X.term_embed (E.fresh_name ty)) in lb, n) - lbs - in - Record (lbs, ty), lbs - *) - - (* unused -- - let rec occurs x = function - | Record (lbs, _) -> - List.exists (fun (_, v) -> occurs x v) lbs - | Access (_, v, _) -> occurs x v - | Other _ as v -> compare_mine x v = 0 (* XXX *) - *) - - (* unused -- - let rec subst_access x s e = - match e with - | Record (lbs, ty) -> - Record (List.map (fun (n,e') -> n, subst_access x s e') lbs, ty) - | Access (lb, e', _) when compare_mine x e' = 0 -> - My_list.assoc Uid.equal lb s - | Access (lb', e', ty) -> Access (lb', subst_access x s e', ty) - | Other _ -> e - *) - - let fully_interpreted = is_mine_symb - - let rec term_extract r = - match X.extract r with - | Some v -> begin match v with - | Record (lbs, ty) -> - begin - try - let lbs = - List.map - (fun (_, r) -> - match term_extract (is_mine r) with - | None, _ -> raise Not_found - | Some t, _ -> t) - lbs - in - Some (E.mk_term (Symbols.Op Symbols.Record) lbs ty), false - with Not_found -> None, false - end - | Access (a, r, ty) -> - begin - match X.term_extract (is_mine r) with - | None, _ -> None, false - | Some t, _ -> - Some (E.mk_term (Symbols.Op (Symbols.Access a)) [t] ty), false - end - | Other (r, _) -> X.term_extract r - end - | None -> X.term_extract r - - - let orient_solved p v pb = - if List.exists (X.equal p) (X.leaves v) then raise Util.Unsolvable; - Sig.{ pb with sbt = (p,v) :: pb.sbt } - - let solve r1 r2 (pb : _ Sig.solve_pb) = - match embed r1, embed r2 with - | Record (l1, _), Record (l2, _) -> - let eqs = - List.fold_left2 - (fun eqs (a, b) (x, y) -> - assert (DE.Term.Const.compare a x = 0); - (is_mine y, is_mine b) :: eqs - ) pb.eqs l1 l2 - in - {pb with eqs=eqs} - - | Other _, Other _ -> - if X.str_cmp r1 r2 > 0 then { pb with sbt = (r1,r2)::pb.sbt } - else { pb with sbt = (r2,r1)::pb.sbt } - - | Other _, Record _ -> orient_solved r1 r2 pb - | Record _, Other _ -> orient_solved r2 r1 pb - | Access _ , _ -> assert false - | _ , Access _ -> assert false - - let assign_value t _ eq = - match embed t with - | Access _ -> None - - | Record (_, ty) -> - if List.exists (fun (t,_) -> Expr.is_model_term t) eq - then None - else Some (Expr.fresh_name ty, false) - - | Other (_,ty) -> - match ty with - | Ty.Trecord { Ty.lbs; _ } -> - let rev_lbs = List.rev_map (fun (_, ty) -> Expr.fresh_name ty) lbs in - let s = E.mk_term (Symbols.Op Symbols.Record) (List.rev rev_lbs) ty in - Some (s, false) (* false <-> not a case-split *) - | _ -> assert false - - let to_model_term = - let rec to_model_term r = - match r with - | Record (fields, ty) -> - (* We can ignore the names of fields as they are inlined in the - type [ty] of the record. *) - let l = - My_list.try_map (fun (_name, rf) -> to_model_term rf) fields - in - Option.bind l @@ fun l -> - Some (E.mk_term Sy.(Op Record) l ty) - - | Other (a, _) -> - X.to_model_term a - | Access _ -> None - in fun r -> to_model_term (embed r) -end diff --git a/src/lib/reasoners/records.mli b/src/lib/reasoners/records.mli deleted file mode 100644 index 4283685e5..000000000 --- a/src/lib/reasoners/records.mli +++ /dev/null @@ -1,37 +0,0 @@ -(**************************************************************************) -(* *) -(* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) --- OCamlPro SAS *) -(* *) -(* This file is distributed under the terms of OCamlPro *) -(* Non-Commercial Purpose License, version 1. *) -(* *) -(* As an exception, Alt-Ergo Club members at the Gold level can *) -(* use this file under the terms of the Apache Software License *) -(* version 2.0. *) -(* *) -(* --------------------------------------------------------------- *) -(* *) -(* The Alt-Ergo theorem prover *) -(* *) -(* Sylvain Conchon, Evelyne Contejean, Francois Bobot *) -(* Mohamed Iguernelala, Stephane Lescuyer, Alain Mebsout *) -(* *) -(* CNRS - INRIA - Universite Paris Sud *) -(* *) -(* --------------------------------------------------------------- *) -(* *) -(* More details can be found in the directory licenses/ *) -(* *) -(**************************************************************************) - -type 'a abstract - -module type ALIEN = sig - include Sig.X - val embed : r abstract -> r - val extract : r -> (r abstract) option -end - -module Shostak - (X : ALIEN) : Sig.SHOSTAK with type r = X.r and type t = X.r abstract diff --git a/src/lib/reasoners/records_rel.ml b/src/lib/reasoners/records_rel.ml deleted file mode 100644 index 84f2a54ea..000000000 --- a/src/lib/reasoners/records_rel.ml +++ /dev/null @@ -1,49 +0,0 @@ -(**************************************************************************) -(* *) -(* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) --- OCamlPro SAS *) -(* *) -(* This file is distributed under the terms of OCamlPro *) -(* Non-Commercial Purpose License, version 1. *) -(* *) -(* As an exception, Alt-Ergo Club members at the Gold level can *) -(* use this file under the terms of the Apache Software License *) -(* version 2.0. *) -(* *) -(* --------------------------------------------------------------- *) -(* *) -(* The Alt-Ergo theorem prover *) -(* *) -(* Sylvain Conchon, Evelyne Contejean, Francois Bobot *) -(* Mohamed Iguernelala, Stephane Lescuyer, Alain Mebsout *) -(* *) -(* CNRS - INRIA - Universite Paris Sud *) -(* *) -(* --------------------------------------------------------------- *) -(* *) -(* More details can be found in the directory licenses/ *) -(* *) -(**************************************************************************) - -type t = unit - -let src = Logs.Src.create ~doc:"Records" __MODULE__ -module Log = (val Logs.src_log src : Logs.LOG) - -let timer = Timers.M_Records - -let empty uf = (), Uf.domains uf -let assume _ uf _ = - (), Uf.domains uf, { Sig_rel.assume = []; remove = [] } -let query _ _ _ = None -let case_split _env _uf ~for_model:_ = [] -let optimizing_objective _env _uf _o = None -let add env uf _ _ = env, Uf.domains uf, [] -let new_terms _ = Expr.Set.empty -let instantiate ~do_syntactic_matching:_ _ env _ _ = env, [] - -let assume_th_elt t th_elt _ = - match th_elt.Expr.extends with - | Util.Records -> - failwith "This Theory does not support theories extension" - | _ -> t diff --git a/src/lib/reasoners/records_rel.mli b/src/lib/reasoners/records_rel.mli deleted file mode 100644 index cac59a5a1..000000000 --- a/src/lib/reasoners/records_rel.mli +++ /dev/null @@ -1,29 +0,0 @@ -(**************************************************************************) -(* *) -(* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) --- OCamlPro SAS *) -(* *) -(* This file is distributed under the terms of OCamlPro *) -(* Non-Commercial Purpose License, version 1. *) -(* *) -(* As an exception, Alt-Ergo Club members at the Gold level can *) -(* use this file under the terms of the Apache Software License *) -(* version 2.0. *) -(* *) -(* --------------------------------------------------------------- *) -(* *) -(* The Alt-Ergo theorem prover *) -(* *) -(* Sylvain Conchon, Evelyne Contejean, Francois Bobot *) -(* Mohamed Iguernelala, Stephane Lescuyer, Alain Mebsout *) -(* *) -(* CNRS - INRIA - Universite Paris Sud *) -(* *) -(* --------------------------------------------------------------- *) -(* *) -(* More details can be found in the directory licenses/ *) -(* *) -(**************************************************************************) - -include Sig_rel.RELATION -val src : Logs.src diff --git a/src/lib/structures/expr.mli b/src/lib/structures/expr.mli index f070a42d3..db38e65e9 100644 --- a/src/lib/structures/expr.mli +++ b/src/lib/structures/expr.mli @@ -435,7 +435,6 @@ val is_pure : t -> bool val is_model_term : t -> bool (** [is_model_term e] checks if the expression [e] is a model terms. A model term can be: - - A record definition involving only model terms. - A constructor application involving only model terms, - A literal of a basic type (integer, real, boolean, unit or bitvector), - A name. *) diff --git a/src/lib/structures/profiling.ml b/src/lib/structures/profiling.ml index 308ea1230..1d129aa6d 100644 --- a/src/lib/structures/profiling.ml +++ b/src/lib/structures/profiling.ml @@ -454,18 +454,6 @@ let columns : (string * string * int * bool option * 'a) list = Format.sprintf "%s~%s" (float_resize curr (sz - 5)) (string_resize (percent gtime curr) 4)); - "Sum", "Time spent in Sum module(s)", 16, Some false, - (fun _ gtime sz -> - let curr = Timers.get_sum (get_timers ()) Timers.M_Sum in - Format.sprintf "%s~%s" - (float_resize curr (sz - 5)) (string_resize (percent gtime curr) 4)); - - "Records", "Time spent in Records module(s)", 16, Some false, - (fun _ gtime sz -> - let curr = Timers.get_sum (get_timers ()) Timers.M_Records in - Format.sprintf "%s~%s" - (float_resize curr (sz - 5)) (string_resize (percent gtime curr) 4)); - "AC", "Time spent in AC module(s)", 16, Some false, (fun _ gtime sz -> let curr = Timers.get_sum (get_timers ()) Timers.M_AC in @@ -480,10 +468,8 @@ let columns : (string * string * int * bool option * 'a) list = let tcc = Timers.get_sum timers Timers.M_CC in let tarith = Timers.get_sum timers Timers.M_Arith in let tarrays = Timers.get_sum timers Timers.M_Arrays in - let tsum = Timers.get_sum timers Timers.M_Sum in - let trecs = Timers.get_sum timers Timers.M_Records in let tac = Timers.get_sum timers Timers.M_AC in - let total = tsat+.tmatch+.tcc+.tarith+.tarrays+.tsum+.trecs+.tac in + let total = tsat+.tmatch+.tcc+.tarith+.tarrays+.tac in float_resize total sz); ] diff --git a/src/lib/structures/ty.ml b/src/lib/structures/ty.ml index 7111f2244..9f9b5aab7 100644 --- a/src/lib/structures/ty.ml +++ b/src/lib/structures/ty.ml @@ -402,14 +402,6 @@ let t_adt ?(body=None) s ty_vars = begin match body with | None -> () | Some [] -> assert false - | Some ([_] as cases) -> - if Options.get_debug_adt () then - Printer.print_dbg ~module_name:"Ty" - "should be registered as a record"; - let cases = - List.map (fun (constr, destrs) -> {constr; destrs}) cases - in - Decls.add s ty_vars cases | Some cases -> let cases = List.map (fun (constr, destrs) -> {constr; destrs}) cases diff --git a/src/lib/util/timers.ml b/src/lib/util/timers.ml index c6ca31a9d..732459612 100644 --- a/src/lib/util/timers.ml +++ b/src/lib/util/timers.ml @@ -39,8 +39,6 @@ type ty_module = | M_UF | M_Arith | M_Arrays - | M_Sum - | M_Records | M_Adt | M_Bitv | M_AC @@ -61,8 +59,6 @@ let all_modules = M_UF; M_Arith; M_Arrays; - M_Sum; - M_Records; M_Adt; M_Bitv; M_AC; @@ -136,8 +132,6 @@ let string_of_ty_module k = match k with | M_UF -> "UF" | M_Arith -> "Arith" | M_Arrays -> "Arrays" - | M_Sum -> "Sum" - | M_Records -> "Records" | M_Adt -> "Adt" | M_Bitv -> "Bitv" | M_AC -> "AC" diff --git a/src/lib/util/timers.mli b/src/lib/util/timers.mli index d7143847f..a1ca9ed67 100644 --- a/src/lib/util/timers.mli +++ b/src/lib/util/timers.mli @@ -35,8 +35,6 @@ type ty_module = | M_UF | M_Arith | M_Arrays - | M_Sum - | M_Records | M_Adt | M_Bitv | M_AC diff --git a/src/lib/util/util.ml b/src/lib/util/util.ml index 876eea711..838f12e84 100644 --- a/src/lib/util/util.ml +++ b/src/lib/util/util.ml @@ -77,10 +77,8 @@ let pp_sat_solver ppf = function | CDCL_Tableaux -> Format.fprintf ppf "CDCL-Tableaux" type theories_extensions = - | Sum | Adt | Arrays - | Records | Bitv | LIA | LRA @@ -116,10 +114,8 @@ let equal_mode x y = match x, y with let th_ext_of_string ext = match ext with - | "Sum" -> Some Sum | "Adt" -> Some Adt | "Arrays" -> Some Arrays - | "Records" -> Some Records | "Bitv" -> Some Bitv | "LIA" -> Some LIA | "LRA" -> Some LRA @@ -131,10 +127,8 @@ let th_ext_of_string ext = let string_of_th_ext ext = match ext with - | Sum -> "Sum" | Adt -> "Adt" | Arrays -> "Arrays" - | Records -> "Records" | Bitv -> "Bitv" | LIA -> "LIA" | LRA -> "LRA" diff --git a/src/lib/util/util.mli b/src/lib/util/util.mli index 2ce5175ed..f003f78ef 100644 --- a/src/lib/util/util.mli +++ b/src/lib/util/util.mli @@ -59,10 +59,8 @@ type sat_solver = val pp_sat_solver : Format.formatter -> sat_solver -> unit type theories_extensions = - | Sum | Adt | Arrays - | Records | Bitv | LIA | LRA From d8508cba8b3c591a41b24e00d69ee5b80ad1a95b Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Wed, 23 Oct 2024 11:49:14 +0200 Subject: [PATCH 04/14] Promote tests --- tests/issues/1008/record.expected | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/issues/1008/record.expected b/tests/issues/1008/record.expected index a6e005255..6f99ff0f4 100644 --- a/tests/issues/1008/record.expected +++ b/tests/issues/1008/record.expected @@ -1,2 +1,2 @@ -unknown +unsat From aabc2bc0086d9e23f146c3f8282b834982356e5d Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Wed, 23 Oct 2024 14:08:36 +0200 Subject: [PATCH 05/14] Do not display 0 candidates messages As we load by default prelude with plenty of axioms, we got a lot of messages about these axioms in the debugging printers of `Matching`. This commit changes this behavior. We only print messages if there is at least one candidate. --- src/lib/reasoners/adt.ml | 2 +- src/lib/reasoners/matching.ml | 30 ++++++++++++++++-------------- test.smt2 | 10 ++++++++++ 3 files changed, 27 insertions(+), 15 deletions(-) create mode 100644 test.smt2 diff --git a/src/lib/reasoners/adt.ml b/src/lib/reasoners/adt.ml index d9df614c4..cb7e16854 100644 --- a/src/lib/reasoners/adt.ml +++ b/src/lib/reasoners/adt.ml @@ -38,7 +38,7 @@ type 'a abstract = c_ty : Ty.t; c_args : (DE.term_cst * 'a) list } - (* [Cons { c_name; c_ty; c_args }] reprensents the application of the + (* [Cons { c_name; c_ty; c_args }] represents the application of the constructor [c_name] of the ADT [ty] with the arguments [c_args]. *) | Select of { d_name : DE.term_cst ; d_ty : Ty.t ; d_arg : 'a } diff --git a/src/lib/reasoners/matching.ml b/src/lib/reasoners/matching.ml index d51957e52..fd4918dad 100644 --- a/src/lib/reasoners/matching.ml +++ b/src/lib/reasoners/matching.ml @@ -165,20 +165,22 @@ module Make (X : Arg) : S with type theory = X.t = struct let candidate_substitutions pat_info res = let open Matching_types in - if Options.get_debug_matching () >= 1 then - print_dbg - ~module_name:"Matching" ~function_name:"candidate_substitutions" - "@[%3d candidate substitutions for Axiom %a with trigger %a@ " - (List.length res) - E.print pat_info.trigger_orig - E.print_list pat_info.trigger.E.content; - if Options.get_debug_matching() >= 2 then - List.iter - (fun gsbt -> - print_dbg ~header:false - ">>> sbs = %a and sbty = %a@ " - (SubstE.pp E.print) gsbt.sbs Ty.print_subst gsbt.sty - )res + if not @@ Compat.List.is_empty res then begin + if Options.get_debug_matching () >= 1 then + print_dbg + ~module_name:"Matching" ~function_name:"candidate_substitutions" + "@[%3d candidate substitutions for Axiom %a with trigger %a@ " + (List.length res) + E.print pat_info.trigger_orig + E.print_list pat_info.trigger.E.content; + if Options.get_debug_matching() >= 2 then + List.iter + (fun gsbt -> + print_dbg ~header:false + ">>> sbs = %a and sbty = %a@ " + (SubstE.pp E.print) gsbt.sbs Ty.print_subst gsbt.sty + )res + end end (*BISECT-IGNORE-END*) diff --git a/test.smt2 b/test.smt2 new file mode 100644 index 000000000..6a8c7f2b7 --- /dev/null +++ b/test.smt2 @@ -0,0 +1,10 @@ +(set-option :produce-models true) +(set-logic ALL) +(declare-datatype t ((B (i Int)))) + +(declare-const e t) + +(assert ((_ is B) e)) +(assert (forall ((n Int)) (distinct e (B n)))) +(check-sat) +(get-model) From 62021dc5d9b1c2f4abcefcddb2f746f6c993c368 Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Mon, 28 Oct 2024 13:30:33 +0100 Subject: [PATCH 06/14] Add a variant of the issue 1008 test Currently, the test `record.smt2` of the issue 1008 only succeeds with the Tableaux SAT solver --- tests/issues/1008/record.default.expected | 2 ++ tests/issues/1008/{record.expected => record.tableaux.expected} | 0 tests/issues/1008/{record.smt2 => record.tableaux.smt2} | 0 tools/gentest.ml | 2 ++ 4 files changed, 4 insertions(+) create mode 100644 tests/issues/1008/record.default.expected rename tests/issues/1008/{record.expected => record.tableaux.expected} (100%) rename tests/issues/1008/{record.smt2 => record.tableaux.smt2} (100%) diff --git a/tests/issues/1008/record.default.expected b/tests/issues/1008/record.default.expected new file mode 100644 index 000000000..a6e005255 --- /dev/null +++ b/tests/issues/1008/record.default.expected @@ -0,0 +1,2 @@ + +unknown diff --git a/tests/issues/1008/record.expected b/tests/issues/1008/record.tableaux.expected similarity index 100% rename from tests/issues/1008/record.expected rename to tests/issues/1008/record.tableaux.expected diff --git a/tests/issues/1008/record.smt2 b/tests/issues/1008/record.tableaux.smt2 similarity index 100% rename from tests/issues/1008/record.smt2 rename to tests/issues/1008/record.tableaux.smt2 diff --git a/tools/gentest.ml b/tools/gentest.ml index b6e20987a..bf1fde645 100644 --- a/tools/gentest.ml +++ b/tools/gentest.ml @@ -264,6 +264,8 @@ end = struct {acc with accepted_exit_codes = [142]} | "default" -> {acc with filters = Some ["default"]} + | "tableaux" -> + {acc with filters = Some ["tableaux"]} | _ -> acc ) Test.base_params From 6529b174494a21458aac3ddf4fb8b162e8d91718 Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Wed, 30 Oct 2024 14:55:20 +0100 Subject: [PATCH 07/14] Better printer + remove dead code The function `xs_modulo_records` is not useful anymore. Indeed, all the ADT variables are sent to the ADT relation thanks to the `init` function of `Uf`. As record type has only one constructor by definition, this will always replace a record variable by a record definition in the union find and we can match patterns of the form `{ lbl1 = ..; ...; lblk = ..}`. --- src/lib/reasoners/adt.ml | 20 ++++++------- src/lib/reasoners/adt_rel.ml | 5 +++- src/lib/reasoners/matching.ml | 54 ++++++++++++----------------------- 3 files changed, 31 insertions(+), 48 deletions(-) diff --git a/src/lib/reasoners/adt.ml b/src/lib/reasoners/adt.ml index cb7e16854..85613fcc5 100644 --- a/src/lib/reasoners/adt.ml +++ b/src/lib/reasoners/adt.ml @@ -105,21 +105,20 @@ module Shostak (X : ALIEN) = struct | Some c -> c | None -> Alien r - let pp_field ppf (lbl, v) = - Fmt.pf ppf "%a : %a" DE.Term.Const.print lbl X.print v - let print ppf = function | Alien x -> X.print ppf x | Constr { c_name; c_args; _ } -> - Fmt.pf ppf "%a@[(%a@])" - DE.Term.Const.print c_name - Fmt.(list ~sep:semi pp_field) c_args + if Compat.List.is_empty c_args then + Fmt.pf ppf "%a" DE.Term.Const.print c_name + else + Fmt.pf ppf "(%a %a)" + DE.Term.Const.print c_name + Fmt.(box @@ list ~sep:sp @@ pair nop X.print) c_args | Select d -> - Fmt.pf ppf "%a#!!%a" X.print d.d_arg DE.Term.Const.print d.d_name - + Fmt.pf ppf "(%a %a)" X.print d.d_arg DE.Term.Const.print d.d_name let is_mine u = match u with @@ -168,10 +167,7 @@ module Shostak (X : ALIEN) = struct let make t = assert (not @@ Options.get_disable_adts ()); - if Options.get_debug_adt () then - Printer.print_dbg - ~module_name:"Adt" ~function_name:"make" - "make %a" E.print t; + Log.debug (fun k -> k "make %a" E.print t); let { E.f; xs; ty; _ } = E.term_view t in let sx, ctx = List.fold_left diff --git a/src/lib/reasoners/adt_rel.ml b/src/lib/reasoners/adt_rel.ml index 87e10b0bc..55012e260 100644 --- a/src/lib/reasoners/adt_rel.ml +++ b/src/lib/reasoners/adt_rel.ml @@ -200,6 +200,7 @@ module Domains = struct let init r t = match Th.embed r with | Alien _ when not (MX.mem r t.domains) -> + Log.debug (fun k -> k"init term %a" X.print r); (* We have to add a default domain if the key `r` is not in map in order to be sure that the case split mechanism will attempt to choose a value for it. *) @@ -242,7 +243,9 @@ module Domains = struct let t = remove r t in tighten nr nd t - | exception Not_found -> init nr t + | exception Not_found -> + Log.debug (fun k -> k"add term %a" X.print nr); + init nr t (* [propagate f a t] iterates on all the changed domains of [t] since the last call of [propagate]. The list of changed domains is flushed after diff --git a/src/lib/reasoners/matching.ml b/src/lib/reasoners/matching.ml index fd4918dad..2ac57dc93 100644 --- a/src/lib/reasoners/matching.ml +++ b/src/lib/reasoners/matching.ml @@ -26,6 +26,7 @@ (**************************************************************************) module E = Expr +module Sy = Symbols module ME = E.Map module SubstE = Var.Map @@ -156,31 +157,26 @@ module Make (X : Arg) : S with type theory = X.t = struct Ty.print_subst sty let match_class_of t cl = - if Options.get_debug_matching() >= 3 then - print_dbg - ~module_name:"Matching" ~function_name:"match_class_of" - "class_of (%a) = { %a }" - E.print t - (fun fmt -> E.Set.iter (Format.fprintf fmt "%a , " E.print)) cl + Log.debug (fun k -> k "class of '%a' is:@ %a" + E.print t + Fmt.(box @@ braces @@ iter ~sep:comma E.Set.iter E.print) cl) let candidate_substitutions pat_info res = let open Matching_types in - if not @@ Compat.List.is_empty res then begin - if Options.get_debug_matching () >= 1 then - print_dbg - ~module_name:"Matching" ~function_name:"candidate_substitutions" - "@[%3d candidate substitutions for Axiom %a with trigger %a@ " - (List.length res) - E.print pat_info.trigger_orig - E.print_list pat_info.trigger.E.content; - if Options.get_debug_matching() >= 2 then - List.iter - (fun gsbt -> - print_dbg ~header:false - ">>> sbs = %a and sbty = %a@ " - (SubstE.pp E.print) gsbt.sbs Ty.print_subst gsbt.sty - )res - end + if Options.get_debug_matching () >= 1 then + print_dbg + ~module_name:"Matching" ~function_name:"candidate_substitutions" + "@[%3d candidate substitutions for Axiom %a with trigger %a@ " + (List.length res) + E.print pat_info.trigger_orig + E.print_list pat_info.trigger.E.content; + if Options.get_debug_matching() >= 2 then + List.iter + (fun gsbt -> + print_dbg ~header:false + ">>> sbs = %a and sbty = %a@ " + (SubstE.pp E.print) gsbt.sbs Ty.print_subst gsbt.sty + )res end (*BISECT-IGNORE-END*) @@ -316,12 +312,6 @@ module Make (X : Arg) : S with type theory = X.t = struct | _ , [] -> l1 | _ -> List.fold_left (fun acc e -> e :: acc) l2 (List.rev l1) - (* let xs_modulo_records t { Ty.lbs; _ } = - List.rev - (List.rev_map - (fun (hs, ty) -> - E.mk_term (Symbols.Op (Symbols.Access hs)) [t] ty) lbs) *) - module SLE = (* sets of lists of terms *) Set.Make(struct type t = E.t list @@ -414,14 +404,8 @@ module Make (X : Arg) : S with type theory = X.t = struct E.Set.fold (fun t l -> let { E.f = f; xs = xs; _ } = E.term_view t in - if Symbols.compare f_pat f = 0 then xs::l + if Symbols.compare f_pat f = 0 then xs :: l else l - (* begin - match f_pat, ty with - | Symbols.Op (Symbols.Record), Ty.Trecord record -> - (xs_modulo_records t record) :: l - | _ -> l - end *) ) cl [] in let cl = filter_classes mconf cl tbox in From caaf87b14be1fd41ccdcbe464897805c5c0d2ca7 Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Wed, 30 Oct 2024 15:44:18 +0100 Subject: [PATCH 08/14] Add new tests --- tests/adts/trigger_definition.expected | 2 ++ tests/adts/trigger_definition.smt2 | 7 +++++++ tests/adts/trigger_destructor.expected | 2 ++ tests/adts/trigger_destructor.smt2 | 7 +++++++ 4 files changed, 18 insertions(+) create mode 100644 tests/adts/trigger_definition.expected create mode 100644 tests/adts/trigger_definition.smt2 create mode 100644 tests/adts/trigger_destructor.expected create mode 100644 tests/adts/trigger_destructor.smt2 diff --git a/tests/adts/trigger_definition.expected b/tests/adts/trigger_definition.expected new file mode 100644 index 000000000..6f99ff0f4 --- /dev/null +++ b/tests/adts/trigger_definition.expected @@ -0,0 +1,2 @@ + +unsat diff --git a/tests/adts/trigger_definition.smt2 b/tests/adts/trigger_definition.smt2 new file mode 100644 index 000000000..7da615094 --- /dev/null +++ b/tests/adts/trigger_definition.smt2 @@ -0,0 +1,7 @@ +(set-logic ALL) +(declare-datatype t ((c (b Bool)))) +(declare-fun f (t) Bool) +(declare-const x t) +(assert (forall ((y Bool)) (f (c y)))) +(assert (not (f x))) +(check-sat) diff --git a/tests/adts/trigger_destructor.expected b/tests/adts/trigger_destructor.expected new file mode 100644 index 000000000..6f99ff0f4 --- /dev/null +++ b/tests/adts/trigger_destructor.expected @@ -0,0 +1,2 @@ + +unsat diff --git a/tests/adts/trigger_destructor.smt2 b/tests/adts/trigger_destructor.smt2 new file mode 100644 index 000000000..6a2832e2d --- /dev/null +++ b/tests/adts/trigger_destructor.smt2 @@ -0,0 +1,7 @@ +(set-logic ALL) +(declare-datatype unit ((void))) +(declare-datatype t ((box (unbox unit)))) +(declare-fun f (t t) Bool) +(assert (forall ((u t) (v t)) (f u (box (unbox v))))) +(assert (not (f (box void) (box void)))) +(check-sat) From 7f2006fa6c95f7b6d07e5c191e97aacb097a801b Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Wed, 30 Oct 2024 15:44:37 +0100 Subject: [PATCH 09/14] Use context of `X.make` --- src/lib/reasoners/adt.ml | 22 ++++++++++++++++------ src/lib/reasoners/adt_rel.ml | 4 ++-- src/lib/reasoners/shostak.ml | 3 +++ 3 files changed, 21 insertions(+), 8 deletions(-) diff --git a/src/lib/reasoners/adt.ml b/src/lib/reasoners/adt.ml index 85613fcc5..37fa20fa3 100644 --- a/src/lib/reasoners/adt.ml +++ b/src/lib/reasoners/adt.ml @@ -169,16 +169,16 @@ module Shostak (X : ALIEN) = struct assert (not @@ Options.get_disable_adts ()); Log.debug (fun k -> k "make %a" E.print t); let { E.f; xs; ty; _ } = E.term_view t in - let sx, ctx = + let ssx, ctx = List.fold_left (fun (args, ctx) s -> let rs, ctx' = X.make s in rs :: args, List.rev_append ctx' ctx )([], []) xs in - let xs = List.rev sx in - match f, xs, ty with - | Sy.Op Sy.Constr hs, _, Ty.Tadt (name, params) -> + let xxs = List.rev ssx in + match f, ty with + | Sy.Op Sy.Constr hs, Ty.Tadt (name, params) -> let cases = Ty.type_body name params in let case_hs = try Ty.assoc_destrs hs cases with Not_found -> assert false @@ -188,12 +188,22 @@ module Shostak (X : ALIEN) = struct List.rev @@ List.fold_left2 (fun c_args v (lbl, _) -> (lbl, v) :: c_args) - [] xs case_hs + [] xxs case_hs with Invalid_argument _ -> assert false in + let ctx = + match cases with + | [{ destrs; _ }] -> + List.fold_left2 + (fun ctx x (d, d_ty) -> + let access = E.mk_term (Sy.destruct d) [t] d_ty in + E.mk_eq ~iff:false x access :: ctx + ) ctx xs destrs + | _ -> ctx + in is_mine @@ Constr {c_name = hs; c_ty = ty; c_args}, ctx - | Sy.Op Sy.Destruct _, [_], _ -> X.term_embed t, ctx + | Sy.Op Sy.Destruct _, _ -> X.term_embed t, ctx (* No risk ! if equal sel (embed sel_x) then X.term_embed t, ctx else sel_x, ctx (* canonization OK *) diff --git a/src/lib/reasoners/adt_rel.ml b/src/lib/reasoners/adt_rel.ml index 55012e260..d80023978 100644 --- a/src/lib/reasoners/adt_rel.ml +++ b/src/lib/reasoners/adt_rel.ml @@ -472,12 +472,12 @@ let build_constr_eq r c = in let xs = List.map (fun (_, ty) -> E.fresh_name ty) ds in let cons = E.mk_constr c xs ty in - let r', ctx = X.make cons in + let r', _ctx = X.make cons in (* In the current implementation of `X.make`, we produce a nonempty context only for interpreted semantic values of the `Arith` and `Records` theories. The semantic values `cons` never involves such values. *) - assert (Compat.List.is_empty ctx); + (* assert (Compat.List.is_empty ctx); *) let eq = Shostak.L.(view @@ mk_eq r r') in Some (eq, E.mk_constr c xs ty) diff --git a/src/lib/reasoners/shostak.ml b/src/lib/reasoners/shostak.ml index 6ef1950c6..fd2cafe69 100644 --- a/src/lib/reasoners/shostak.ml +++ b/src/lib/reasoners/shostak.ml @@ -27,6 +27,9 @@ (*** Combination module of Shostak theories ***) +module E = Expr +module Sy = Symbols + [@@@ocaml.warning "-60"] module rec CX : sig include Sig.X From a89abf7b908796e9278647557993e16d26078753 Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Mon, 4 Nov 2024 11:23:11 +0100 Subject: [PATCH 10/14] Revert "Use context of `X.make`" This reverts commit 31c4c66e1992464aa17d8a67d4b10667f48b2dac. --- src/lib/reasoners/adt.ml | 22 ++++++---------------- src/lib/reasoners/adt_rel.ml | 4 ++-- src/lib/reasoners/shostak.ml | 3 --- 3 files changed, 8 insertions(+), 21 deletions(-) diff --git a/src/lib/reasoners/adt.ml b/src/lib/reasoners/adt.ml index 37fa20fa3..85613fcc5 100644 --- a/src/lib/reasoners/adt.ml +++ b/src/lib/reasoners/adt.ml @@ -169,16 +169,16 @@ module Shostak (X : ALIEN) = struct assert (not @@ Options.get_disable_adts ()); Log.debug (fun k -> k "make %a" E.print t); let { E.f; xs; ty; _ } = E.term_view t in - let ssx, ctx = + let sx, ctx = List.fold_left (fun (args, ctx) s -> let rs, ctx' = X.make s in rs :: args, List.rev_append ctx' ctx )([], []) xs in - let xxs = List.rev ssx in - match f, ty with - | Sy.Op Sy.Constr hs, Ty.Tadt (name, params) -> + let xs = List.rev sx in + match f, xs, ty with + | Sy.Op Sy.Constr hs, _, Ty.Tadt (name, params) -> let cases = Ty.type_body name params in let case_hs = try Ty.assoc_destrs hs cases with Not_found -> assert false @@ -188,22 +188,12 @@ module Shostak (X : ALIEN) = struct List.rev @@ List.fold_left2 (fun c_args v (lbl, _) -> (lbl, v) :: c_args) - [] xxs case_hs + [] xs case_hs with Invalid_argument _ -> assert false in - let ctx = - match cases with - | [{ destrs; _ }] -> - List.fold_left2 - (fun ctx x (d, d_ty) -> - let access = E.mk_term (Sy.destruct d) [t] d_ty in - E.mk_eq ~iff:false x access :: ctx - ) ctx xs destrs - | _ -> ctx - in is_mine @@ Constr {c_name = hs; c_ty = ty; c_args}, ctx - | Sy.Op Sy.Destruct _, _ -> X.term_embed t, ctx + | Sy.Op Sy.Destruct _, [_], _ -> X.term_embed t, ctx (* No risk ! if equal sel (embed sel_x) then X.term_embed t, ctx else sel_x, ctx (* canonization OK *) diff --git a/src/lib/reasoners/adt_rel.ml b/src/lib/reasoners/adt_rel.ml index d80023978..55012e260 100644 --- a/src/lib/reasoners/adt_rel.ml +++ b/src/lib/reasoners/adt_rel.ml @@ -472,12 +472,12 @@ let build_constr_eq r c = in let xs = List.map (fun (_, ty) -> E.fresh_name ty) ds in let cons = E.mk_constr c xs ty in - let r', _ctx = X.make cons in + let r', ctx = X.make cons in (* In the current implementation of `X.make`, we produce a nonempty context only for interpreted semantic values of the `Arith` and `Records` theories. The semantic values `cons` never involves such values. *) - (* assert (Compat.List.is_empty ctx); *) + assert (Compat.List.is_empty ctx); let eq = Shostak.L.(view @@ mk_eq r r') in Some (eq, E.mk_constr c xs ty) diff --git a/src/lib/reasoners/shostak.ml b/src/lib/reasoners/shostak.ml index fd2cafe69..6ef1950c6 100644 --- a/src/lib/reasoners/shostak.ml +++ b/src/lib/reasoners/shostak.ml @@ -27,9 +27,6 @@ (*** Combination module of Shostak theories ***) -module E = Expr -module Sy = Symbols - [@@@ocaml.warning "-60"] module rec CX : sig include Sig.X From f2cbfc2659d73c48b1800531ecedb1c490353f86 Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Mon, 4 Nov 2024 11:32:01 +0100 Subject: [PATCH 11/14] Remove test.smt2 --- test.smt2 | 10 ---------- 1 file changed, 10 deletions(-) delete mode 100644 test.smt2 diff --git a/test.smt2 b/test.smt2 deleted file mode 100644 index 6a8c7f2b7..000000000 --- a/test.smt2 +++ /dev/null @@ -1,10 +0,0 @@ -(set-option :produce-models true) -(set-logic ALL) -(declare-datatype t ((B (i Int)))) - -(declare-const e t) - -(assert ((_ is B) e)) -(assert (forall ((n Int)) (distinct e (B n)))) -(check-sat) -(get-model) From 6d20e79c02433b78d712e8e12891d72e3517041a Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Tue, 12 Nov 2024 14:06:37 +0100 Subject: [PATCH 12/14] clean up --- docs/sphinx_docs/Alt_ergo_native/05_theories.md | 4 +--- rsc/extra/subgraphs.dot | 1 - src/lib/frontend/translate.ml | 4 +--- src/lib/reasoners/adt_rel.ml | 14 ++------------ src/lib/reasoners/sig.mli | 6 +++--- 5 files changed, 7 insertions(+), 22 deletions(-) diff --git a/docs/sphinx_docs/Alt_ergo_native/05_theories.md b/docs/sphinx_docs/Alt_ergo_native/05_theories.md index ee814cee5..75f0f7a83 100644 --- a/docs/sphinx_docs/Alt_ergo_native/05_theories.md +++ b/docs/sphinx_docs/Alt_ergo_native/05_theories.md @@ -17,8 +17,7 @@ Alt-Ergo currently provides built-in support for the following theories. * Linear arithmetic over integers and rationals * (Fragment of) non-linear arithmetic * Floating-point arithmetic (as an extension) -* Enumerated datatypes -* Record datatypes +* Algebraic datatypes * Polymorphic functional arrays * Fixed-size bitvectors @@ -28,7 +27,6 @@ All theories are always considered *modulo equality*. * `SUM`: Enumerated datatypes * `Adt`: Algebraic datatypes * `Arrays`: Polymorphic functional arrays -* `Records`: Record datatypes * `Bitv`: Fixed-size bitvectors * `LIA`: Linear arithmetic over integers * `LRA`: Linear arithmetic over rationals diff --git a/rsc/extra/subgraphs.dot b/rsc/extra/subgraphs.dot index 749b42d54..d99059ae6 100644 --- a/rsc/extra/subgraphs.dot +++ b/rsc/extra/subgraphs.dot @@ -141,7 +141,6 @@ subgraph cluster_lib { "Enum"; "Ite"; "Polynome"; - "Records"; "Sig"; } diff --git a/src/lib/frontend/translate.ml b/src/lib/frontend/translate.ml index c2b4df693..2536ad9d5 100644 --- a/src/lib/frontend/translate.ml +++ b/src/lib/frontend/translate.ml @@ -580,9 +580,7 @@ let mk_term_decl ({ id_ty; path; tags; _ } as tcst: DE.term_cst) = in (Hstring.make name, arg_tys, ret_ty) -(** Handles the definitions of a list of mutually recursive types. - - If one of the types is an ADT, the ADTs that have only one case are - considered as ADTs as well and not as records. *) +(** Handles the definitions of a list of mutually recursive types. *) let mk_mr_ty_decls (tdl: DE.ty_cst list) = let handle_ty_decl (ty: Ty.t) (tdef: DE.Ty.def option) = match ty, tdef with diff --git a/src/lib/reasoners/adt_rel.ml b/src/lib/reasoners/adt_rel.ml index 55012e260..6886c5b3c 100644 --- a/src/lib/reasoners/adt_rel.ml +++ b/src/lib/reasoners/adt_rel.ml @@ -472,12 +472,7 @@ let build_constr_eq r c = in let xs = List.map (fun (_, ty) -> E.fresh_name ty) ds in let cons = E.mk_constr c xs ty in - let r', ctx = X.make cons in - (* In the current implementation of `X.make`, we produce - a nonempty context only for interpreted semantic values - of the `Arith` and `Records` theories. The semantic - values `cons` never involves such values. *) - assert (Compat.List.is_empty ctx); + let r', _ctx = X.make cons in let eq = Shostak.L.(view @@ mk_eq r r') in Some (eq, E.mk_constr c xs ty) @@ -635,12 +630,7 @@ let split_domain ~for_model env uf = let* cd, r, c = pick_domain ~for_model uf in if for_model || can_split env (Numbers.Q.from_int cd) then let _, cons = Option.get @@ build_constr_eq r c in - let nr, ctx = X.make cons in - (* In the current implementation of `X.make`, we produce - a nonempty context only for interpreted semantic values - of the `Arith` and `Records` theories. The semantic - values `cons` never involves such values. *) - assert (Compat.List.is_empty ctx); + let nr, _ctx = X.make cons in Some (LR.mkv_eq r nr) else None diff --git a/src/lib/reasoners/sig.mli b/src/lib/reasoners/sig.mli index 3050e1f23..111e354d5 100644 --- a/src/lib/reasoners/sig.mli +++ b/src/lib/reasoners/sig.mli @@ -71,7 +71,7 @@ module type SHOSTAK = sig Semantic value for which [is_constant] returns [true] contains no free names and thus have the same concrete value in all contexts. - Note that for some theories (e.g. records, arrays) the constant may not be + Note that for some theories (e.g. adt, arrays) the constant may not be pure: it may involve nested (constant) terms of other theories. *) val is_constant : t -> bool @@ -126,7 +126,7 @@ module type SHOSTAK = sig forced. Use [false] only when the returned term contains aliens that should be - assigned (e.g. records). + assigned (e.g. adt). **When returning [false], you must ensure that the equality between the first argument and the return value always hold (i.e. is a *unit* fact). @@ -198,7 +198,7 @@ module type X = sig (* the returned bool is true when the returned term in a constant of the theory. Otherwise, the term contains aliens that should be assigned - (eg. records). In this case, it's a unit fact, not a decision + (eg. adt). In this case, it is a unit fact, not a decision *) val assign_value : r -> r list -> (Expr.t * r) list -> (Expr.t * bool) option From 1bf9e0f4418cd2c1831fc134e3639b5900926d55 Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Tue, 12 Nov 2024 14:07:58 +0100 Subject: [PATCH 13/14] Reapply "Use context of `X.make`" This reverts commit 874ea984f937df2f475697bab27015fda30de13b. --- src/lib/reasoners/adt.ml | 22 ++++++++++++++++------ src/lib/reasoners/shostak.ml | 3 +++ 2 files changed, 19 insertions(+), 6 deletions(-) diff --git a/src/lib/reasoners/adt.ml b/src/lib/reasoners/adt.ml index 85613fcc5..37fa20fa3 100644 --- a/src/lib/reasoners/adt.ml +++ b/src/lib/reasoners/adt.ml @@ -169,16 +169,16 @@ module Shostak (X : ALIEN) = struct assert (not @@ Options.get_disable_adts ()); Log.debug (fun k -> k "make %a" E.print t); let { E.f; xs; ty; _ } = E.term_view t in - let sx, ctx = + let ssx, ctx = List.fold_left (fun (args, ctx) s -> let rs, ctx' = X.make s in rs :: args, List.rev_append ctx' ctx )([], []) xs in - let xs = List.rev sx in - match f, xs, ty with - | Sy.Op Sy.Constr hs, _, Ty.Tadt (name, params) -> + let xxs = List.rev ssx in + match f, ty with + | Sy.Op Sy.Constr hs, Ty.Tadt (name, params) -> let cases = Ty.type_body name params in let case_hs = try Ty.assoc_destrs hs cases with Not_found -> assert false @@ -188,12 +188,22 @@ module Shostak (X : ALIEN) = struct List.rev @@ List.fold_left2 (fun c_args v (lbl, _) -> (lbl, v) :: c_args) - [] xs case_hs + [] xxs case_hs with Invalid_argument _ -> assert false in + let ctx = + match cases with + | [{ destrs; _ }] -> + List.fold_left2 + (fun ctx x (d, d_ty) -> + let access = E.mk_term (Sy.destruct d) [t] d_ty in + E.mk_eq ~iff:false x access :: ctx + ) ctx xs destrs + | _ -> ctx + in is_mine @@ Constr {c_name = hs; c_ty = ty; c_args}, ctx - | Sy.Op Sy.Destruct _, [_], _ -> X.term_embed t, ctx + | Sy.Op Sy.Destruct _, _ -> X.term_embed t, ctx (* No risk ! if equal sel (embed sel_x) then X.term_embed t, ctx else sel_x, ctx (* canonization OK *) diff --git a/src/lib/reasoners/shostak.ml b/src/lib/reasoners/shostak.ml index 6ef1950c6..fd2cafe69 100644 --- a/src/lib/reasoners/shostak.ml +++ b/src/lib/reasoners/shostak.ml @@ -27,6 +27,9 @@ (*** Combination module of Shostak theories ***) +module E = Expr +module Sy = Symbols + [@@@ocaml.warning "-60"] module rec CX : sig include Sig.X From 20d966c1481e3744b37de01a539c4a17913c7982 Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Tue, 12 Nov 2024 14:10:37 +0100 Subject: [PATCH 14/14] restore printer --- src/lib/reasoners/matching.ml | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/src/lib/reasoners/matching.ml b/src/lib/reasoners/matching.ml index 2ac57dc93..55e2bf782 100644 --- a/src/lib/reasoners/matching.ml +++ b/src/lib/reasoners/matching.ml @@ -157,9 +157,11 @@ module Make (X : Arg) : S with type theory = X.t = struct Ty.print_subst sty let match_class_of t cl = - Log.debug (fun k -> k "class of '%a' is:@ %a" - E.print t - Fmt.(box @@ braces @@ iter ~sep:comma E.Set.iter E.print) cl) + if Options.get_debug_matching() >= 3 then + Log.debug (fun k -> k "class of '%a' is:@ %a" + E.print t + Fmt.(box @@ braces + @@ iter ~sep:comma E.Set.iter E.print) cl) let candidate_substitutions pat_info res = let open Matching_types in