From 00049ae26b952c5ab8128a59e1f1e5c1bbe622da Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Wed, 29 Jan 2025 15:13:57 +0100 Subject: [PATCH 1/7] Use constant terms as identifiers in names and variables This PR changes the way we construct identifiers for names (in Symbols) and variables (in Var). We plan to completely replace the AE identifiers with identifiers from Dolmen. This PR serves as an intermediate step from string-based identifiers to Dolmen identifiers. - All the identifiers are now managed in the Id module. - Constant terms are used for declared or defined identifiers in the input file. - Internal identifiers are still pre-mangled strings. Replacing them with Dolmen identifiers requires careful investigation, particularly in the AC(X) implementation. - I haven't removed Id.typed yet. After this PR, the user identifiers will be typed, so we do not need to store them separately. If we use the internal type of the identifier, we will need to implement a conversion function from Dolmen type to Alt-Ergo type, which is not trivial. I prefer keeping this type and remove it after transitioning from Alt-Ergo types to Dolmen types. - The new API of Id prevents us from creating duplicate fresh/fresh_ac/abstract identifiers. - I still check that user identifiers do not start with . or @. In Before this PR, we mangled the identifier if it happened. In this PR, we crash. I don't have a strong opinion on this behavior, it was just simpler to implement this way. - I use identifiers for term variables too. I preserved the internal representation because: 1. The notion of local variables is AE-specific, whereas the local name in Dolmen identifiers is a distinct concept. 2. After this PR, variables are typed but what is the type of Underscore? May be forall a. a? This PR have been tested on ae-format (+2-2). --- src/bin/common/solving_loop.ml | 22 +-- src/lib/frontend/models.ml | 9 +- src/lib/frontend/translate.ml | 74 +++------ src/lib/reasoners/ac.ml | 8 +- src/lib/reasoners/arith.ml | 15 +- src/lib/reasoners/ccx.ml | 4 +- src/lib/reasoners/fun_sat.ml | 4 +- src/lib/reasoners/instances.ml | 10 +- src/lib/reasoners/intervalCalculus.ml | 4 +- src/lib/reasoners/satml_frontend.ml | 6 +- src/lib/reasoners/theory.ml | 18 +- src/lib/reasoners/uf.ml | 43 +++-- src/lib/reasoners/use.ml | 5 +- src/lib/structures/commands.ml | 4 +- src/lib/structures/expr.ml | 35 ++-- src/lib/structures/id.ml | 154 ++++++++++++++---- src/lib/structures/id.mli | 122 ++++++++++++-- src/lib/structures/modelMap.ml | 6 +- src/lib/structures/modelMap.mli | 10 +- src/lib/structures/satml_types.ml | 10 +- src/lib/structures/symbols.ml | 86 +++------- src/lib/structures/symbols.mli | 93 +---------- src/lib/structures/var.ml | 83 +++++----- src/lib/structures/var.mli | 36 ++-- src/lib/util/util.ml | 26 +++ src/lib/util/util.mli | 9 + tests/issues/854/function.default.expected | 2 +- tests/issues/854/original.default.expected | 2 +- tests/issues/854/twice_eq.default.expected | 2 +- tests/models/adt/arith.default.expected | 4 +- tests/models/arith/arith11.default.expected | 4 +- .../array/embedded-array.default.expected | 2 +- tests/models/bool/bool1.default.expected | 8 +- tests/models/bool/bool3.default.expected | 4 +- tests/models/records/record3.default.expected | 2 +- tests/models/uf/uf1.default.expected | 2 +- tests/models/uf/uf2.default.expected | 2 +- 37 files changed, 503 insertions(+), 427 deletions(-) diff --git a/src/bin/common/solving_loop.ml b/src/bin/common/solving_loop.ml index a35411d7bd..1dd0fb46ed 100644 --- a/src/bin/common/solving_loop.ml +++ b/src/bin/common/solving_loop.ml @@ -32,6 +32,8 @@ module DO = D_state_option module Sy = Symbols module O = Options +module ConstSet = Map.Make (Dolmen.Std.Expr.Term.Const) + exception Exit_with_code of int type solver_ctx = { @@ -103,14 +105,14 @@ let cmd_on_modes st modes cmd = (** Adds the named terms of the statement [stmt] to the map accumulator [acc] *) let add_if_named - ~(acc : DStd.Expr.term Util.MS.t) + ~(acc : DStd.Expr.term ConstSet.t) (stmt : Typer_Pipe.typechecked D_loop.Typer_Pipe.stmt) = match stmt.contents with - | `Defs [`Term_def ({name = Simple n; _}, id, _, _, t)] -> + | `Defs [`Term_def (_, id, _, _, t)] -> begin match DStd.Expr.Id.get_tag id DStd.Expr.Tags.named with | None -> acc - | Some _ -> Util.MS.add n t acc + | Some _ -> ConstSet.add id t acc end | _ -> (* Named terms are expected to be definitions with simple names. *) @@ -212,7 +214,7 @@ let process_source ?selector_inst ~print_status src = State.create_key ~pipe:"" "sat_state" in - let named_terms: DStd.Expr.term Util.MS.t State.key = + let named_terms: DStd.Expr.term ConstSet.t State.key = State.create_key ~pipe:"" "named_terms" in @@ -357,7 +359,7 @@ let process_source ?selector_inst ~print_status src = State.empty |> State.set solver_ctx_key solver_ctx |> State.set partial_model_key None - |> State.set named_terms Util.MS.empty + |> State.set named_terms ConstSet.empty |> DO.init |> State.init ~debug ~report_style ~reports ~max_warn ~time_limit ~size_limit ~response_file @@ -633,14 +635,14 @@ let process_source ?selector_inst ~print_status src = in (* Fetches the term value in the current model. *) - let evaluate_term get_value name term = + let evaluate_term get_value tcst term = (* There are two ways to evaluate a term: - if its name is registered in the environment, get its value; - if not, check if the formula is in the environment. *) let simple_form = Expr.mk_term - (Sy.name name) + (Sy.name @@ Id.of_term_cst ~defined:true tcst) [] (Translate.dty_to_ty term.DStd.Expr.term_ty) in @@ -652,12 +654,12 @@ let process_source ?selector_inst ~print_status src = let print_terms_assignments = Fmt.list ~sep:Fmt.cut - (fun fmt (name, v) -> Fmt.pf fmt "(%s %s)" name v) + (fun fmt (name, v) -> Fmt.pf fmt "(%a %s)" Util.pp_term_cst name v) in let handle_get_assignment ~get_value st = let assignments = - Util.MS.fold + ConstSet.fold (fun name term acc -> if DStd.Expr.Ty.equal term.DStd.Expr.term_ty DStd.Expr.Ty.bool then (name, evaluate_term get_value name term) :: acc @@ -789,7 +791,7 @@ let process_source ?selector_inst ~print_status src = |> DO.StrictMode.clear |> DO.ProduceAssignment.clear |> DO.init - |> State.set named_terms Util.MS.empty + |> State.set named_terms ConstSet.empty | {contents = `Exit; _} -> raise Exit diff --git a/src/lib/frontend/models.ml b/src/lib/frontend/models.ml index afa71e83d2..fc2be74b56 100644 --- a/src/lib/frontend/models.ml +++ b/src/lib/frontend/models.ml @@ -194,14 +194,15 @@ module Pp_smtlib_term = struct | Sy.In(lb, rb), [t] -> fprintf fmt "(%a in %a, %a)" print t Sy.print_bound lb Sy.print_bound rb - | Sy.Name { hs = n; _ }, l -> begin + | Sy.Name { id; _ }, l -> begin let constraint_name = + let s = Id.show id in try let constraint_name,_,_ = - (MS.find (Hstring.view n) !constraints) in + (MS.find s !constraints) in constraint_name with _ -> - let constraint_name = "c_"^(Hstring.view n) in - constraints := MS.add (Hstring.view n) + let constraint_name = "c_" ^ s in + constraints := MS.add s (constraint_name, to_string_type (E.type_info t), List.map (fun e -> to_string_type (E.type_info e)) l diff --git a/src/lib/frontend/translate.ml b/src/lib/frontend/translate.ml index 0b3f5c8038..71fc7787a8 100644 --- a/src/lib/frontend/translate.ml +++ b/src/lib/frontend/translate.ml @@ -45,23 +45,6 @@ module HT = let hash (Id i)= DE.Id.hash i end) -(** Helper function: returns the basename of a dolmen path, since in AE - the problems are contained in one-file (for now at least), the path is - irrelevant and only the basename matters *) -let get_basename = function - | DStd.Path.Local { name; } - | Absolute { name; path = []; } -> name - | Absolute { name; path; } -> - Fmt.failwith - "Expected an empty path to the basename: \"%s\" but got: [%a]." - name (fun fmt l -> - match l with - | h :: t -> - Format.fprintf fmt "%s" h; - List.iter (Format.fprintf fmt "; %s") t - | _ -> () - ) path - module Cache = struct let ae_sy_ht: Sy.t HT.t = HT.create 100 @@ -124,8 +107,9 @@ module Cache = struct let store_sy_vl_names (tvl: DE.term_var list) = List.iter ( fun ({ DE.path; _ } as tv) -> - let name = get_basename path in - store_sy tv (Sy.name name) + let name = Util.get_basename path in + (* TODO : Check this line! *) + store_sy tv (Sy.name @@ Id.of_string ~ns:Internal name) ) tvl let store_ty_vars ?(is_var = true) ty = @@ -176,7 +160,7 @@ let builtin_term t = Dl.Typer.T.builtin_term t let builtin_ty t = Dl.Typer.T.builtin_ty t let ty (ty_cst : DE.ty_cst) ty = - let name = get_basename ty_cst.path in + let name = Util.get_basename ty_cst.path in DStd.Id.Map.add { name = DStd.Name.simple name; ns = Sort } @@ fun env s -> builtin_ty @@ @@ -188,7 +172,7 @@ let fpa_rounding_mode, rounding_modes, add_rounding_modes = let constrs = Fpa_rounding.d_constrs in let add_constrs map = List.fold_left (fun map (c : DE.term_cst) -> - let name = get_basename c.path in + let name = Util.get_basename c.path in DStd.Id.Map.add { name = DStd.Name.simple name; ns = Term } (fun env _ -> builtin_term @@ @@ -629,12 +613,12 @@ let mk_ty_decl (ty_c: DE.ty_cst) = (** Handles term declaration by storing the eventual present type variables in the cache as well as the symbol associated to the term. *) -let mk_term_decl ({ id_ty; path; tags; _ } as tcst: DE.term_cst) = - let name = get_basename path in +let mk_term_decl ({ id_ty; tags; _ } as tcst: DE.term_cst) = let sy = + let id = Id.of_term_cst tcst in begin match DStd.Tag.get tags DE.Tags.ac with - | Some () -> Sy.name ~kind:Sy.Ac name - | _ -> Sy.name name + | Some () -> Sy.name ~kind:Sy.Ac id + | _ -> Sy.name id end in Cache.store_sy tcst sy; @@ -646,7 +630,7 @@ let mk_term_decl ({ id_ty; path; tags; _ } as tcst: DE.term_cst) = List.map dty_to_ty arg_tys, dty_to_ty ret_ty | _ -> [], dty_to_ty id_ty in - (Hstring.make name, arg_tys, ret_ty) + (tcst, 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 @@ -744,15 +728,15 @@ let handle_patt_var id (DE.{ term_descr; _ } as term) = match term_descr with | Cst ({ builtin = B.Base; id_ty; _ } as ty_c) -> let ty = dty_to_ty id_ty in - let v = Var.of_string @@ Fmt.to_to_string DE.Term.Const.print id in - let sy = Sy.Var v in + let v = Var.of_id @@ Id.of_term_cst ty_c in + let sy = Sy.var v in Cache.store_sy ty_c sy; v, id, ty | Var ({ builtin = B.Base; id_ty; _ } as ty_v) -> let ty = dty_to_ty id_ty in - let v = Var.of_string @@ Fmt.to_to_string DE.Term.Const.print id in - let sy = Sy.Var v in + let v = Var.of_id @@ Id.of_term_cst ty_v in + let sy = Sy.var v in Cache.store_sy ty_v sy; v, id, ty @@ -815,10 +799,10 @@ end = struct | Cst ({ builtin = B.Constructor _; _ } as cst) -> Constr (cst, []) - | Var ({ builtin = B.Base; path; _ } as t_v) -> + | Var ({ builtin = B.Base; _ } as t_v) -> (* Should the type be passed as an argument instead of re-evaluating it here? *) - let v = Var.of_string (get_basename path) in + let v = Var.of_id @@ Id.of_term_cst t_v in let sy = Sy.var v in Cache.store_sy t_v sy; (* Adding the matched variable to the store *) @@ -1439,9 +1423,8 @@ let rec mk_expr | Binder ((Let_par ls | Let_seq ls) as let_binder, body) -> let lsbis = List.map ( - fun ({ DE.path; _ } as tv, t) -> - let name = get_basename path in - let v = Var.of_string name in + fun (tv, t) -> + let v = Var.of_id @@ Id.of_term_cst tv in Cache.store_sy tv (Sy.var v); v, t ) ls @@ -1485,9 +1468,9 @@ let rec mk_expr (* the following is done in two iterations to preserve the order *) (* quantified variables *) let ntvl = List.rev_map ( - fun (DE.{ path; id_ty; _ } as t_v) -> + fun (DE.{ id_ty; _ } as t_v) -> dty_to_ty id_ty, - Var.of_string (get_basename path), + Var.of_id @@ Id.of_term_cst t_v, t_v ) tvl in @@ -1631,11 +1614,7 @@ and make_trigger ?(loc = Loc.dummy) ~name_base ~decl_kind | { DE.term_descr = Binder (Exists (_, qm_vars), e); _ } -> List.iter (fun (v : DE.term_var) -> - let var = - match v.path with - | Local { name } -> Var.local name - | _ -> assert false - in + let var = Var.local @@ Id.of_term_cst v in Cache.store_var v var) qm_vars; e @@ -1950,9 +1929,8 @@ let make dloc_file acc stmt = names in a row. *) List.iter (fun (def : Typer_Pipe.def) -> match def with - | `Term_def (_, ({ path; _ } as tcst), _, _, _) -> - let name_base = get_basename path in - let sy = Sy.name ~defined:true name_base in + | `Term_def (_, tcst, _, _, _) -> + let sy = Sy.name @@ Id.of_term_cst ~defined:true tcst in Cache.store_sy tcst sy | `Type_alias _ -> () | `Instanceof _ -> @@ -1968,15 +1946,15 @@ let make dloc_file acc stmt = | `Term_def ( _, ({ path; tags; _ } as tcst), tyvars, terml, body) -> Cache.store_tyvl tyvars; let st_loc = dl_to_ael dloc_file loc in - let name_base = get_basename path in + let name_base = Util.get_basename path in let binders, defn = let rty = dty_to_ty body.term_ty in let binders, rev_args = List.fold_left ( - fun (binders, acc) (DE.{ path; id_ty; _ } as tv) -> + fun (binders, acc) (DE.{ id_ty; _ } as tv) -> let ty = dty_to_ty id_ty in - let v = Var.of_string (get_basename path) in + let v = Var.of_id @@ Id.of_term_cst tv in let sy = Sy.var v in Cache.store_sy tv sy; let e = E.mk_term sy [] ty in diff --git a/src/lib/reasoners/ac.ml b/src/lib/reasoners/ac.ml index bedf316845..d21e28d35c 100644 --- a/src/lib/reasoners/ac.ml +++ b/src/lib/reasoners/ac.ml @@ -202,17 +202,19 @@ module Make (X : Sig.X) = struct let abstract2 sy t r acc = if List.exists (is_other_ac_symbol sy) (X.leaves r) then match X.ac_extract r, Expr.term_view t with - | Some ac, { f = Name { hs; kind = Ac; _ } ; xs; ty; _ } -> + | Some ac, { f = Name { id; kind = Ac; _ } ; xs; ty; _ } -> (* It should have been abstracted when building [r] *) assert (not (Sy.equal sy ac.h)); - let aro_sy = Sy.name ~ns:Internal ("@" ^ (HS.view hs)) in + let aro_sy = + Sy.name @@ Id.of_string ~ns:Internal ("@" ^ (Id.show id)) + in let aro_t = Expr.mk_term aro_sy xs ty in let eq = Expr.mk_eq ~iff:false aro_t t in X.term_embed aro_t, eq::acc | Some ac, { f = Op Mult; xs; ty; _ } -> (* It should have been abstracted when building [r] *) assert (not (Sy.equal sy ac.h)); - let aro_sy = Sy.name ~ns:Internal "@*" in + let aro_sy = Sy.name @@ Id.of_string ~ns:Internal "@*" in let aro_t = Expr.mk_term aro_sy xs ty in let eq = Expr.mk_eq ~iff:false aro_t t in X.term_embed aro_t, eq::acc diff --git a/src/lib/reasoners/arith.ml b/src/lib/reasoners/arith.ml index afc1b7ae91..a1dc21a2dd 100644 --- a/src/lib/reasoners/arith.ml +++ b/src/lib/reasoners/arith.ml @@ -36,7 +36,7 @@ let src = Logs.Src.create ~doc:"Arith" __MODULE__ module Log = (val Logs.src_log src : Logs.LOG) let is_mult h = Sy.equal (Sy.Op Sy.Mult) h -let mod_symb = Sy.name ~ns:Internal "@mod" +let mod_symb = Sy.name @@ Id.of_string ~ns:Internal "@mod" let calc_power (c : Q.t) (d : Q.t) (ty : Ty.t) = (* d must be integral and if we work on integer exponentation, @@ -246,7 +246,8 @@ module Shostak then (* becomes uninterpreted *) let tau = - E.mk_term (Sy.name ~kind:Sy.Ac ~ns:Internal "@*") [t1; t2] ty + let sy = Sy.name ~kind:Sy.Ac @@ Id.of_string ~ns:Internal "@*" in + E.mk_term sy [t1; t2] ty in let xtau, ctx' = X.make tau in P.add p (P.create [coef, xtau] Q.zero ty), List.rev_append ctx' ctx @@ -260,7 +261,10 @@ module Shostak (P.is_const p2 == None || (ty == Ty.Tint && P.is_const p1 == None)) then (* becomes uninterpreted *) - let tau = E.mk_term (Sy.name ~ns:Internal "@/") [t1; t2] ty in + let tau = + let sy = Sy.name @@ Id.of_string ~ns:Internal "@/" in + E.mk_term sy [t1; t2] ty + in let xtau, ctx' = X.make tau in P.add p (P.create [coef, xtau] Q.zero ty), List.rev_append ctx' ctx else @@ -287,7 +291,10 @@ module Shostak (P.is_const p1 == None || P.is_const p2 == None) then (* becomes uninterpreted *) - let tau = E.mk_term (Sy.name ~ns:Internal "@%") [t1; t2] ty in + let tau = + let sy = Sy.name @@ Id.of_string ~ns:Internal "@%" in + E.mk_term sy [t1; t2] ty + in let xtau, ctx' = X.make tau in P.add p (P.create [coef, xtau] Q.zero ty), List.rev_append ctx' ctx else diff --git a/src/lib/reasoners/ccx.ml b/src/lib/reasoners/ccx.ml index 5d9f56787c..4b4bac58d4 100644 --- a/src/lib/reasoners/ccx.ml +++ b/src/lib/reasoners/ccx.ml @@ -249,7 +249,9 @@ module Main : S = struct end (*BISECT-IGNORE-END*) - let one, _ = X.make (Expr.mk_term (Sy.name ~ns:Internal "@bottom") [] Ty.Tint) + let one, _ = + let sy = Sy.name @@ Id.of_string ~ns:Internal "@bottom" in + X.make (Expr.mk_term sy [] Ty.Tint) let concat_leaves uf l = let concat_rec acc t = diff --git a/src/lib/reasoners/fun_sat.ml b/src/lib/reasoners/fun_sat.ml index 347ef6cc48..5480e2d498 100644 --- a/src/lib/reasoners/fun_sat.ml +++ b/src/lib/reasoners/fun_sat.ml @@ -1875,8 +1875,7 @@ module Make (Th : Theory.S) = struct clear_instances_cache (); Th.reinit_cpt (); Symbols.clear_labels (); - Id.Namespace.reinit (); - Var.reinit_cnt (); + Id.reinit (); Satml_types.Flat_Formula.reinit_cpt (); Ty.reinit_decls (); IntervalCalculus.reinit_cache (); @@ -1888,7 +1887,6 @@ module Make (Th : Theory.S) = struct let () = Steps.save_steps (); - Var.save_cnt (); Expr.save_cache (); Hstring.save_cache (); Shostak.Combine.save_cache (); diff --git a/src/lib/reasoners/instances.ml b/src/lib/reasoners/instances.ml index 6f9f7af11d..280d3c7dab 100644 --- a/src/lib/reasoners/instances.ml +++ b/src/lib/reasoners/instances.ml @@ -168,8 +168,10 @@ module Make(X : Theory.S) : S with type tbox = X.t = struct let env = { env with matching = EM.max_term_depth env.matching (E.depth f) } in match E.form_view f with - | E.Iff(f1, f2) -> - let p = E.mk_term (Symbols.name name) [] Ty.Tbool in + | E.Iff (f1, f2) -> + let p = + E.mk_term (Symbols.name @@ Id.of_string ~ns:Internal name) [] Ty.Tbool + in let np = E.neg p in let defn = if E.equal f1 p then f2 @@ -179,7 +181,9 @@ module Make(X : Theory.S) : S with type tbox = X.t = struct add_ground_pred env ~guard p np defn ex | E.Literal _ -> - let p = E.mk_term (Symbols.name name) [] Ty.Tbool in + let p = + E.mk_term (Symbols.name @@ Id.of_string ~ns:Internal name) [] Ty.Tbool + in let np = E.neg p in let defn = if E.equal p f then E.vrai diff --git a/src/lib/reasoners/intervalCalculus.ml b/src/lib/reasoners/intervalCalculus.ml index 5e037b74ad..81d90fd544 100644 --- a/src/lib/reasoners/intervalCalculus.ml +++ b/src/lib/reasoners/intervalCalculus.ml @@ -2202,7 +2202,7 @@ let integrate_mapsTo_bindings sbs maps_to = ~function_name:"integrate_maps_to_bindings" "bad semantic trigger %a |-> %a@,\ left-hand side is not a constant!" - Var.print x E.print tx; + Var.pp x E.print tx; raise Exit | Some c -> let tc = mk_const_term (E.type_info t) c in @@ -2231,7 +2231,7 @@ let extend_with_domain_substitution = "[Error] %a <= %a <= %a@,\ Which value should we choose?" Q.print q1 - Var.print lb_var + Var.pp lb_var Q.print q2; assert (Q.compare q2 q1 >= 0); assert false diff --git a/src/lib/reasoners/satml_frontend.ml b/src/lib/reasoners/satml_frontend.ml index c0b448983c..94517019f6 100644 --- a/src/lib/reasoners/satml_frontend.ml +++ b/src/lib/reasoners/satml_frontend.ml @@ -1393,9 +1393,9 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct | Ty.Tbool -> begin let bmodel = SAT.boolean_model env.satml in + let tlit = Shostak.Literal.make (LTerm t) in Compat.List.find_map (fun Atom.{lit; neg = {lit=neglit; _}; _} -> - let tlit = Shostak.Literal.make (LTerm t) in if Shostak.Literal.equal tlit lit then Some E.vrai else if Shostak.Literal.equal tlit neglit then @@ -1414,9 +1414,8 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct let reinit_ctx () = Steps.reinit_steps (); Th.reinit_cpt (); - Id.Namespace.reinit (); + Id.reinit (); Symbols.clear_labels (); - Var.reinit_cnt (); Objective.Function.reinit_cnt (); Satml_types.Flat_Formula.reinit_cpt (); Ty.reinit_decls (); @@ -1429,7 +1428,6 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct let () = Steps.save_steps (); - Var.save_cnt (); Expr.save_cache (); Hstring.save_cache (); Shostak.Combine.save_cache (); diff --git a/src/lib/reasoners/theory.ml b/src/lib/reasoners/theory.ml index ad9ad7962a..df1cb2a170 100644 --- a/src/lib/reasoners/theory.ml +++ b/src/lib/reasoners/theory.ml @@ -130,17 +130,17 @@ module Main_Default : S = struct | _ -> Ty.fresh_tvar () let logics_of_assumed st = - (* NB: using an [Hstring.Map] here depends on the fact that name mangling - is done pre-emptively in [Symbols.name] *) + (* NB: using an [Id.Map] here depends on the fact that name mangling + is done pre-emptively in [Id.of_string] or [Id.fresh]. *) SE.fold (fun t mp -> match E.term_view t with - | { E.f = Sy.Name { hs; kind = ((Sy.Ac | Sy.Other) as is_ac); _ }; + | { E.f = Sy.Name { id; kind = ((Sy.Ac | Sy.Other) as is_ac); _ }; xs; ty; _ } -> let xs = List.map E.type_info xs in let xs, ty = try - let xs', ty', is_ac' = Hstring.Map.find hs mp in + let xs', ty', is_ac' = Id.Map.find id mp in assert (is_ac == is_ac'); let ty = generalize_types ty ty' in let xs = @@ -149,10 +149,10 @@ module Main_Default : S = struct xs, ty with Not_found -> xs, ty in - Hstring.Map.add hs (xs, ty, is_ac) mp + Id.Map.add id (xs, ty, is_ac) mp | _ -> mp - ) st Hstring.Map.empty + ) st Id.Map.empty module Ty_map = Map.Make (DE.Ty.Const) @@ -218,12 +218,12 @@ module Main_Default : S = struct let print_logics ?(header=true) logics = print_dbg ~header "@[(* logics: *)@ "; - Hstring.Map.iter + Id.Map.iter (fun hs (xs, ty, is_ac) -> print_dbg ~flushed:false ~header:false - "logic %s%s : %a%a@ " + "logic %s%a : %a%a@ " (if is_ac == Sy.Ac then "ac " else "") - (Hstring.view hs) + Id.pp hs print_arrow_type xs Ty.print ty )logics; diff --git a/src/lib/reasoners/uf.ml b/src/lib/reasoners/uf.ml index 0d94864e6b..afdc738b1b 100644 --- a/src/lib/reasoners/uf.ml +++ b/src/lib/reasoners/uf.ml @@ -1112,14 +1112,9 @@ module MED = Map.Make else Expr.compare a b end) -let is_suspicious_name hs = - match Hstring.view hs with - | "@/" | "@%" | "@*" -> true - | _ -> false - (* The model generation is known to be imcomplete for FPA theory. *) let is_suspicious_symbol = function - | Symbols.Name { hs; _ } when is_suspicious_name hs -> true + | Symbols.Name { id; _ } when Id.is_suspicious id -> true | _ -> false let terms env = @@ -1127,8 +1122,8 @@ let terms env = (fun t r ((terms, suspicious) as acc) -> let Expr.{ f; _ } = Expr.term_view t in match f with - | Name { defined = true; _ } -> - (* We don't store names defined by the user. *) + | Name { id = Term_cst { defined = true; _ }; _ } -> + (* We do not store names defined by the user. *) acc | _ -> let suspicious = is_suspicious_symbol f || suspicious in @@ -1234,7 +1229,11 @@ let compute_concrete_model_of_val cache = acc end - | Sy.Name { hs = id; _ }, _, _ -> + | Sy.Name { id = Term_cst { tcst; defined }; _ }, _, _ + when not defined -> + (* XXX: Currently, all the declared constant term identifiers + are user-provided. This will change after adopting Dolmen + identifiers everywhere. *) let value = match ty with | Ty.Text _ -> @@ -1244,7 +1243,7 @@ let compute_concrete_model_of_val cache = get_abstract_for env t | _ -> ret_rep in - ModelMap.(add (id, arg_tys, ty) arg_vals value mdl), mrepr + ModelMap.(add (tcst, arg_tys, ty) arg_vals value mdl), mrepr | _ -> Printer.print_err @@ -1273,24 +1272,24 @@ let extract_concrete_model cache = Expr.ArraysEx.store arr_val i v ) vals abstract in - let id, is_user = + let id, mdl = let Expr.{ f; _ } = Expr.term_view t in match f with - | Sy.Name { hs; ns = User; _ } -> hs, true - | Sy.Name { hs; _ } -> hs, false + | Sy.Name { id = Term_cst { tcst; defined } as id; _ } + when not defined -> + (* XXX: Currently, all the declared constant term identifiers + are user-provided. This will change after adopting Dolmen + identifiers everywhere. *) + id, ModelMap.add (tcst, [], ty) [] arr_val mdl + | Sy.Name { id; _ } -> + (* Internal identifiers can occur here if we need to generate + a model term for an embedded array but this array is not itself + declared by the user -- see the [embedded-array] test . *) + id, mdl | _ -> (* Excluded in [compute_concrete_model_of_val] *) assert false in - let mdl = - if is_user then - ModelMap.add (id, [], ty) [] arr_val mdl - else - (* Internal identifiers can occur here if we need to generate - a model term for an embedded array but this array isn't itself - declared by the user -- see the [embedded-array] test . *) - mdl - in (* We need to update the model [mdl] in order to substitute all the occurrences of the array identifier [id] by an appropriate model term. This cannot be performed while computing the model with diff --git a/src/lib/reasoners/use.ml b/src/lib/reasoners/use.ml index 1d6670acdd..65a52602f2 100644 --- a/src/lib/reasoners/use.ml +++ b/src/lib/reasoners/use.ml @@ -53,7 +53,10 @@ let union_tpl (x1,y1) (x2,y2) = Options.exec_thread_yield (); SE.union x1 x2, SA.union y1 y2 -let one, _ = X.make (E.mk_term (Symbols.name ~ns:Internal "@bottom") [] Ty.Tint) +let one, _ = + let sy = Symbols.name @@ Id.of_string ~ns:Internal "@bottom" in + X.make (E.mk_term sy [] Ty.Tint) + let leaves r = match X.leaves r with [] -> [one] | l -> l diff --git a/src/lib/structures/commands.ml b/src/lib/structures/commands.ml index 45b8dcaf8b..20e2a9ef6e 100644 --- a/src/lib/structures/commands.ml +++ b/src/lib/structures/commands.ml @@ -46,9 +46,9 @@ type sat_tdecl = { } let print_aux fmt = function - | Decl (id, arg_tys, ret_ty) -> + | Decl (tcst, arg_tys, ret_ty) -> Fmt.pf fmt "declare %a with type (%a) -> %a" - Id.pp id + Util.pp_term_cst tcst Fmt.(list ~sep:comma Ty.print) arg_tys Ty.print ret_ty diff --git a/src/lib/structures/expr.ml b/src/lib/structures/expr.ml index 43f4264d57..1d3d8e3bec 100644 --- a/src/lib/structures/expr.ml +++ b/src/lib/structures/expr.ml @@ -331,7 +331,7 @@ module SmtPrinter = struct Z.pp_print (Q.den q) let pp_binder ppf (var, ty) = - Fmt.pf ppf "(%a %a)" Var.print var Ty.pp_smtlib ty + Fmt.pf ppf "(%a %a)" Var.pp var Ty.pp_smtlib ty let pp_binders = Fmt.(box @@ iter_bindings ~sep:sp Var.Map.iter pp_binder) @@ -444,7 +444,7 @@ module SmtPrinter = struct | Sy.Let, [] -> let x = match bind with B_let x -> x | _ -> assert false in Fmt.pf ppf "@[<2>(let@ ((%a %a))@ %a@])" - Var.print x.let_v + Var.pp x.let_v pp x.let_e pp_boxed x.in_e @@ -479,17 +479,17 @@ module SmtPrinter = struct | Sy.False, [] -> Fmt.pf ppf "false" - | Sy.Name { ns = Abstract; hs = n; _ }, [] -> - Fmt.pf ppf "(as %a %a)" Id.pp n Ty.pp_smtlib ty + | Sy.Name { id = Hstring { ns = Abstract; _ } as id; _ }, [] -> + Fmt.pf ppf "(as %a %a)" Id.pp id Ty.pp_smtlib ty - | Sy.Name { hs = n; _ }, [] -> Id.pp ppf n + | Sy.Name { id; _ }, [] -> Id.pp ppf id - | Sy.Name { hs = n; _ }, _ :: _ -> + | Sy.Name { id; _ }, _ :: _ -> Fmt.pf ppf "@[<2>(%a %a@])" - Id.pp n + Id.pp id Fmt.(list ~sep:sp pp |> box) xs - | Sy.Var v, [] -> Var.print ppf v + | Sy.Var v, [] -> Var.pp ppf v | Sy.Int i, [] -> pp_integer ppf i @@ -502,7 +502,7 @@ module SmtPrinter = struct Fmt.pf ppf "#b%s" (Z.format (Fmt.str "%%0%db" n) s) | Sy.MapsTo v, [t] -> - Fmt.pf ppf "@[<2>(ae.mapsto %a %a@])" Var.print v pp t + Fmt.pf ppf "@[<2>(ae.mapsto %a %a@])" Var.pp v pp t | Sy.In (_lb, _rb), [_t] -> (* WARNING: we don't print the content of this semantic trigger as @@ -533,7 +533,7 @@ end module AEPrinter = struct let pp_binder ppf (var, ty) = - Fmt.pf ppf "%a:%a" Var.print var Ty.pp_smtlib ty + Fmt.pf ppf "%a:%a" Var.pp var Ty.pp_smtlib ty let pp_binders ppf binders = if Var.Map.is_empty binders then @@ -631,7 +631,7 @@ module AEPrinter = struct (fun ppf x -> if Options.get_verbose () then Fmt.pf ppf " [sko = %a]" pp x.let_sko) x - Var.print x.let_v pp x.let_e pp_silent x.in_e + Var.pp x.let_v pp x.let_e pp_silent x.in_e | Sy.(Op Get), [e1; e2] -> Fmt.pf ppf "%a[%a]" pp e1 pp e2 @@ -982,17 +982,20 @@ let vrai = let faux = neg (vrai) let fresh_name ty = - mk_term (Sy.name ~ns:Fresh @@ Id.Namespace.Internal.fresh ()) [] ty + let sy = Sy.name @@ Id.fresh ~ns:Fresh () in + mk_term sy [] ty let mk_abstract ty = - mk_term (Sy.name ~ns:Abstract @@ Id.Namespace.Abstract.fresh ()) [] ty + let sy = Sy.name @@ Id.fresh ~ns:Abstract () in + mk_term sy [] ty let fresh_ac_name ty = - mk_term (Sy.name ~ns:Fresh_ac @@ Id.Namespace.Internal.fresh ()) [] ty + let sy = Sy.name @@ Id.fresh ~ns:Fresh_ac () in + mk_term sy [] ty let is_fresh_ac_name t = match t with - | { f = Name { ns = Fresh_ac; _ }; xs = []; _ } -> true + | { f = Name { id = Hstring { ns = Fresh_ac; _ }; _ }; xs = []; _ } -> true | _ -> false let positive_int i = mk_term (Sy.int i) [] Ty.Tint @@ -1814,7 +1817,7 @@ let skolemize { main = f; binders; sko_v; sko_vty; _ } = let mk_sym cpt s = Fmt.kstr - (fun str -> Sy.name ~ns:Skolem str) + (fun str -> Sy.name @@ Id.of_string ~ns:Skolem str) "%s%s!%d" s tyvars diff --git a/src/lib/structures/id.ml b/src/lib/structures/id.ml index b8666d20a0..e1933ef937 100644 --- a/src/lib/structures/id.ml +++ b/src/lib/structures/id.ml @@ -16,45 +16,135 @@ (* *) (**************************************************************************) -type t = Hstring.t [@@deriving ord] +type name_space = Internal | Fresh | Fresh_ac | Skolem | Abstract -type typed = t * Ty.t list * Ty.t [@@deriving ord] +module Make () = struct + let fresh, reset_fresh_cpt = + let cpt = ref 0 in + let fresh_string ?(base = "") () = + let res = base ^ (string_of_int !cpt) in + incr cpt; + res + in + let reset_fresh_string_cpt () = + cpt := 0 + in + fresh_string, reset_fresh_string_cpt +end -let equal = Hstring.equal +module Internal = Make () +module Skolem = Make () +module Abstract = Make () -let pp ppf id = - Dolmen.Smtlib2.Script.Poly.Print.id ppf - (Dolmen.Std.Name.simple (Hstring.view id)) +type t = + | Term_cst of { tcst : Dolmen.Std.Expr.term_cst; defined : bool } + | Hstring of { hs : Hstring.t; ns : name_space } -let show id = Fmt.str "%a" pp id +type typed = Dolmen.Std.Expr.term_cst * Ty.t list * Ty.t -module Namespace = struct - module type S = sig - val fresh : ?base:string -> unit -> string - end +let compare_typed (t1, _, _) (t2, _, _) = + Dolmen.Std.Expr.Term.Const.compare t1 t2 - module Make () = struct - let fresh, reset_fresh_cpt = - let cpt = ref 0 in - let fresh_string ?(base = "") () = - let res = base ^ (string_of_int !cpt) in - incr cpt; - res - in - let reset_fresh_string_cpt () = - cpt := 0 - in - fresh_string, reset_fresh_string_cpt - end +let mangle ns s = + match ns with + | Internal -> ".!" ^ s + | Fresh -> ".k" ^ s + | Fresh_ac -> ".K" ^ s + | Skolem -> ".?__" ^ s + | Abstract -> "@a" ^ s - module Internal = Make () +let of_term_cst ?(defined = false) tcst = + (* If the name we got from the user starts with either "." + or "@" (which are prefixes reserved for solver use in the SMT-LIB + standard), the name will be printed with an extra ".". So if the user + writes ".x" or "@x", it will be printed as "..x" and ".@x" instead. - module Skolem = Make () + Normally, this should not occur, but we do this to ensure no confusion + even if invalid names ever sneak through. *) + assert ( + let s = Util.show_term_cst tcst in + not (Compat.String.starts_with ~prefix:"." s) && + not (Compat.String.starts_with ~prefix:"@" s)); + Term_cst { tcst; defined } - module Abstract = Make () +let of_string ~ns s = + let () = + match ns with + | Fresh | Fresh_ac | Abstract -> invalid_arg "of_string" + | _ -> () + in + let hs = Hstring.make (mangle ns s) in + Hstring { hs; ns } - let reinit () = - Internal.reset_fresh_cpt (); - Skolem.reset_fresh_cpt (); - Abstract.reset_fresh_cpt () -end +let fresh ?base ~ns () = + let s = + match ns with + | Skolem -> Skolem.fresh ?base () + | Abstract -> Abstract.fresh ?base () + | _ -> Internal.fresh ?base () + in + let hs = Hstring.make (mangle ns s) in + Hstring { hs; ns } + +let compare i1 i2 = + match i1, i2 with + | Term_cst { tcst = t1; defined = d1 }, + Term_cst { tcst = t2; defined = d2 } -> + let c = Bool.compare d1 d2 in + if c <> 0 then c + else Dolmen.Std.Expr.Term.Const.compare t1 t2 + | Term_cst _, _ -> 1 + | _, Term_cst _ -> -1 + + | Hstring { hs = hs1; _ }, Hstring { hs = hs2; _ } -> + (* NB: Internal identifiers are pre-mangled, which means that we do not + need to take the name space into consideration when comparing. *) + Hstring.compare hs1 hs2 + +let equal i1 i2 = + match i1, i2 with + | Term_cst { tcst = t1; defined = d1 }, + Term_cst { tcst = t2; defined = d2 } -> + Bool.equal d1 d2 && Dolmen.Std.Expr.Term.Const.equal t1 t2 + | Hstring { hs = hs1; _ }, Hstring { hs = hs2; _ } -> + (* NB: Internal identifiers are pre-mangled, which means that we do not + need to take the name space into consideration when comparing. *) + Hstring.equal hs1 hs2 + | _ -> false + +let hash i = + match i with + | Term_cst { tcst; _ } -> + Dolmen.Std.Expr.Term.Const.hash tcst + | Hstring { hs; _ } -> + (* NB: Internal identifiers are pre-mangled, which means that we do not + need to take the name space into consideration when hashing. *) + Hstring.hash hs + +let pp ppf i = + match i with + | Term_cst { tcst; _ } -> Util.pp_term_cst ppf tcst + | Hstring { hs; _ } -> + (* Names are pre-mangled *) + Dolmen.Smtlib2.Script.Poly.Print.id ppf + @@ Dolmen.Std.Name.simple @@ Hstring.view hs + +let show = Fmt.to_to_string pp + +let is_suspicious i = + match i with + | Term_cst _ -> false + | Hstring { hs; _ } -> + match Hstring.view hs with + | "@/" | "@%" | "@*" -> true + | _ -> false + +let reinit () = + Internal.reset_fresh_cpt (); + Skolem.reset_fresh_cpt (); + Abstract.reset_fresh_cpt () + +module Map = Map.Make (struct + type nonrec t = t + let compare = compare + end) diff --git a/src/lib/structures/id.mli b/src/lib/structures/id.mli index 5666a0a8a4..437f4928ba 100644 --- a/src/lib/structures/id.mli +++ b/src/lib/structures/id.mli @@ -16,29 +16,115 @@ (* *) (**************************************************************************) -type t = Hstring.t [@@deriving ord] +(** The [name_space] type discriminates the different types of internal + identifiers. The same string in different name spaces is considered as + different identifiers. -type typed = t * Ty.t list * Ty.t -(** Typed identifier of function. In order: - - The identifier. - - Types of its arguments. - - The returned type. *) + Note that the identifier stored in the [Hstring] constructor below are + mangled during its creation: a special prefix is added depending on the + name space. *) +type name_space = + | Internal + (** This symbol is an internal implementation detail of the solver, such as + a proxy formula or the abstracted counterpart of AC symbols. + Internal identifiers are printed with a ".!" prefix. *) + | Fresh + (** This symbol is a "fresh" internal identifer. Fresh internal identifiers + play a similar role as internal identifiers, but they always represent a + constant that was introduced during solving as part of some kind of + purification or abstraction procedure. + + In order to correctly implement AC(X) in the presence of distributive + symbols, symbols generated for AC(X) abstraction use a special + namespace, [Fresh_ac] below. + + To ensure uniqueness, fresh identifiers must always be generated using + [Id.Namespace.Internal.fresh ()]. + + In particular, fresh identifiers are only used to denote constants, not + arbitrary functions. *) + | Fresh_ac + (** This symbol has been introduced as part of the AC(X) abstraction process. + This is notably used by some parts of AC(X) that check if terms contains + fresh symbols (see [contains_a_fresh_alien] in the [Arith] module for an + example). + + These correspond to the K sort in the AC(X) paper. They use a different + name space from other fresh symbols because we need to be able to know + whether a fresh symbol comes from the AC(X) abstraction procedure in order + to prevent loops. + + To ensure uniqueness, AC abstraction identifiers must always be generated + using [fresh ~ns:Fresh_ac ()]. *) + | Skolem + (** This symbol has been introduced as part of skolemization, and represents + the (dependent) variable of an existential quantifier. Skolem identifiers + can have arbitrary arity to depend on previous skolem names in binding + order (so if you have `(exists (x y) e)` then there will be a skolem + variable `sko_x` and a skolem function `(sko_y sko_x)`). *) + | Abstract + (** This symbol has been introduced as part of model generation, and + represents an abstract value. + + To ensure uniqueness, abstract identifiers must always be generated using + [fresh ~ns:Abstract ()]. *) + +type t = private + | Term_cst of { tcst : Dolmen.Std.Expr.term_cst; defined : bool } + (** This identifier was declared or defined by the user, and appears as is + somewhere in a source file. *) + + | Hstring of { hs : Hstring.t; ns : name_space } + +(* TODO: remove this type after replacing Alt-Ergo types by Dolmen types. *) +type typed = Dolmen.Std.Expr.term_cst * Ty.t list * Ty.t val compare_typed : typed -> typed -> int + +val of_term_cst : ?defined:bool -> Dolmen.Std.Expr.term_cst -> t +(** [of_term_cst ?defined t] creates an identifier from a constant term. + The argument [defined] is used to determine if the identifier is + declared or defined by user. *) + +val of_string : ns:name_space -> string -> t +(** [of_string ~ns s] creates an identifier in the name space [ns] from the + string [s]. + + Note that identifiers are pre-mangled: the [hs] field of the resulting + identifier may not be exactly the string that was passed to this function + (however, calling [of_string] with the same string but two different name + spaces is guaranteed to return two identifiers with distinct [hs] fields). + + @raise Invalid_argument if the name space is [Fresh], [Fresh_ac] or + [Abstract]. *) + +val fresh : ?base:string -> ns:name_space -> unit -> t +(** [fresh ?base ~ns ()] generates a fresh identifier within the name space [ns] + derived from the base string [base]. If [base] is not provided, an empty + string is used by default. + + The identifier is pre-mangled similarly to [of_string]. *) + +val compare : t -> t -> int +(** [compare i1 i2] compares the identifiers [i1] and [i2]. *) + val equal : t -> t -> bool -val show : t -> string +(** [equal i1 i2] checks if [i1] and [i2] are equal. *) + +val hash : t -> int +(** [hash i] computes a hash for the identifier [i]. On term constant + identifiers, this hash is perfect. *) + val pp : t Fmt.t +(** [pp ppf i] prints the identifier [i] on the formatter [ppf], quoting the + string, if it needs. *) + +val show : t -> string +(** Same as [pp] but outputs the result as a string. *) -module Namespace : sig - module type S = sig - val fresh : ?base:string -> unit -> string - end +val is_suspicious : t -> bool - module Internal : S - module Skolem : S - module Abstract : S +val reinit : unit -> unit +(** Resets the internal counters of the [fresh] function. *) - val reinit : unit -> unit - (** Resets the [fresh_internal_name], [fresh_skolem] and [fresh_abstract] - counters. *) -end +module Map : Map.S with type key = t diff --git a/src/lib/structures/modelMap.ml b/src/lib/structures/modelMap.ml index 47df05ccbe..015452e37b 100644 --- a/src/lib/structures/modelMap.ml +++ b/src/lib/structures/modelMap.ml @@ -127,7 +127,7 @@ type t = { let add ((id, arg_tys, _) as sy) arg_vals ret_val { values; suspicious } = if List.compare_lengths arg_tys arg_vals <> 0 then Fmt.invalid_arg "The arity of the symbol %a doesn't agree the number of \ - arguments" Id.pp id; + arguments" Util.pp_term_cst id; let constraints = match P.find sy values with | C g -> g @@ -157,7 +157,7 @@ let empty ~suspicious declared_ids = let rec subst_in_term id e c = let Expr.{ f; xs; ty = ty'; _ } = Expr.term_view c in match f, xs with - | Sy.Name { hs = id'; _ }, [] when Id.equal id id' -> + | Sy.Name { id = id'; _ }, [] when Id.equal id id' -> let ty = Expr.type_info e in if not @@ Ty.equal ty ty' then Errors.error (Model_error (Subst_type_clash (id, ty', ty))); @@ -188,7 +188,7 @@ let pp_named_arg_ty ~unused ppf (arg_name, arg_ty) = let pp_define_fun ~is_constant pp ppf ((id, arg_tys, ret_ty), a) = let named_arg_tys = List.mapi (fun i arg_ty -> (i, arg_ty)) arg_tys in Fmt.pf ppf "(@[define-fun %a (%a) %a@ %a)@]" - Id.pp id + Util.pp_term_cst id Fmt.(list ~sep:sp (pp_named_arg_ty ~unused:is_constant)) named_arg_tys Ty.pp_smtlib ret_ty pp a diff --git a/src/lib/structures/modelMap.mli b/src/lib/structures/modelMap.mli index f3bc5406ef..0f0f6fd127 100644 --- a/src/lib/structures/modelMap.mli +++ b/src/lib/structures/modelMap.mli @@ -29,8 +29,8 @@ type t (** Type of model. *) val add : Id.typed -> Expr.t list -> Expr.t -> t -> t -(** [add sy args ret mdl] adds the binding [args -> ret] to the partial graph - associated with the symbol [sy]. *) +(** [add id args ret mdl] adds the binding [args -> ret] to the partial graph + associated with the identifier [id]. *) val empty : suspicious:bool -> Id.typed list -> t (** An empty model. The [suspicious] flag is used to remember that this @@ -38,8 +38,10 @@ val empty : suspicious:bool -> Id.typed list -> t model generation is known to be incomplete. *) val find : Id.typed -> t -> graph -(** [find sy mdl] returns the graph associated with the symbol [sy] in the model - [mdl], raises [Not_found] if it doesn't exist. *) +(** [find id mdl] returns the graph associated with the identifier [id] in the + model [mdl]. + + @raise Not_found if it does not exist. *) val fold: (Id.typed -> graph -> 'a -> 'a) -> t -> 'a -> 'a (** [fold f mdl init] folds over the bindings in the model [mdl] with the diff --git a/src/lib/structures/satml_types.ml b/src/lib/structures/satml_types.ml index be109c2de4..7f3ee6bb10 100644 --- a/src/lib/structures/satml_types.ml +++ b/src/lib/structures/satml_types.ml @@ -953,7 +953,10 @@ module Flat_Formula : FLAT_FORMULA = struct if is_neg then a.Atom.neg,l else a,l let mk_new_proxy n = - let sy = Symbols.name ~ns:Internal @@ "PROXY__" ^ string_of_int n in + let sy = + Symbols.name @@ Id.of_string ~ns:Internal @@ + "PROXY__" ^ string_of_int n + in E.mk_term sy [] Ty.Tbool let get_proxy_of f proxies_mp = @@ -1020,7 +1023,10 @@ module Proxy_formula = struct if is_neg then a.Atom.neg,l else a,l let mk_new_proxy n = - let sy = Symbols.name ~ns:Internal @@ "PROXY__" ^ (string_of_int n) in + let sy = + Symbols.name @@ Id.of_string ~ns:Internal + @@ "PROXY__" ^ (string_of_int n) + in E.mk_term sy [] Ty.Tbool let rec mk_cnf hcons f ((proxies, inv_proxies, new_vars, cnf) as accu) = diff --git a/src/lib/structures/symbols.ml b/src/lib/structures/symbols.ml index 87e47fb45a..ad48a3ba21 100644 --- a/src/lib/structures/symbols.ml +++ b/src/lib/structures/symbols.ml @@ -79,32 +79,6 @@ type form = type name_kind = Ac | Other -type name_space = User | Internal | Fresh | Fresh_ac | Skolem | Abstract - -let compare_name_space ns1 ns2 = - match ns1, ns2 with - | User, User -> 0 - | User, _ -> -1 - | _, User -> 1 - - | Internal, Internal -> 0 - | Internal, _ -> -1 - | _, Internal -> 1 - - | Fresh, Fresh -> 0 - | Fresh, _ -> -1 - | _, Fresh -> 1 - - | Fresh_ac, Fresh_ac -> 0 - | Fresh_ac, _ -> -1 - | _, Fresh_ac -> 1 - - | Skolem, Skolem -> 0 - | Skolem, _ -> -1 - | _, Skolem -> 1 - - | Abstract, Abstract -> 0 - type bound_kind = Unbounded | VarBnd of Var.t | ValBnd of Numbers.Q.t type bound = (* private *) @@ -113,11 +87,7 @@ type bound = (* private *) type t = | True | False - | Name of - { hs : Id.t - ; kind : name_kind - ; defined : bool - ; ns : name_space } + | Name of { id : Id.t ; kind : name_kind } | Int of Z.t | Real of Q.t | Bitv of int * Z.t @@ -129,21 +99,7 @@ type t = | MapsTo of Var.t | Let -let mangle ns s = - match ns with - | User when String.length s > 0 && Char.equal '.' s.[0] -> ".." ^ s - | User when String.length s > 0 && Char.equal '@' s.[0] -> ".@" ^ s - | User -> s - | Internal -> ".!" ^ s - | Fresh -> ".k" ^ s - | Fresh_ac -> ".K" ^ s - | Skolem -> ".?__" ^ s - | Abstract -> "@a" ^ s - -(* NB: names are pre-mangled, which means that we don't need to take the - namespace into consideration when hashing or comparing. *) -let name ?(kind=Other) ?(defined=false) ?(ns = User) s = - Name { hs = Hstring.make (mangle ns s) ; kind ; defined ; ns } +let name ?(kind=Other) id = Name { id ; kind } let var s = Var s let int i = Int (Z.of_string i) @@ -174,8 +130,10 @@ let is_ac x = match x with | _ -> false let is_internal sy = + (* In the current `Id` implementation, all constant terms are user-provided. + This will change once Dolmen identifiers are adopted everywhere. *) match sy with - | Name { ns = User; _ } -> false + | Name { id = Term_cst _; _ } -> false | Name _ -> true | _ -> false @@ -263,12 +221,10 @@ let compare s1 s2 = | Int z1, Int z2 -> Z.compare z1 z2 | Real h1, Real h2 -> Q.compare h1 h2 | Var v1, Var v2 | MapsTo v1, MapsTo v2 -> Var.compare v1 v2 - | Name { ns = ns1; hs = h1; kind = k1; _ }, - Name { ns = ns2; hs = h2; kind = k2; _ } -> - let c = Hstring.compare h1 h2 in - if c <> 0 then c else - let c = compare_kinds k1 k2 in - if c <> 0 then c else compare_name_space ns1 ns2 + | Name { id = i1; kind = k1; _ }, + Name { id = i2; kind = k2; _ } -> + let c = Id.compare i1 i2 in + if c <> 0 then c else compare_kinds k1 k2 | Bitv (n1, s1), Bitv (n2, s2) -> let c = Int.compare n1 n2 in if c <> 0 then c else Z.compare s1 s2 @@ -295,8 +251,8 @@ let hash x = | Bitv (n, s) -> 19 * (Hashtbl.hash n + Hashtbl.hash s) + 3 | In (b1, b2) -> 19 * (Hashtbl.hash b1 + Hashtbl.hash b2) + 4 (* NB: No need to hash the namespace because names are pre-mangled *) - | Name { hs = n; kind = Ac; _ } -> 19 * Hstring.hash n + 5 - | Name { hs = n; kind = Other; _ } -> 19 * Hstring.hash n + 6 + | Name { id; kind = Ac; _ } -> 19 * Id.hash id + 5 + | Name { id; kind = Other; _ } -> 19 * Id.hash id + 6 | Int z -> 19 * Z.hash z + 7 | Real n -> 19 * Hashtbl.hash n + 7 | Var v -> 19 * Var.hash v + 8 @@ -307,7 +263,7 @@ let hash x = let string_of_bound_kind x = match x with | Unbounded -> "?" - | VarBnd v -> Var.to_string v + | VarBnd v -> Var.show v | ValBnd v -> Numbers.Q.to_string v let string_of_bound b = @@ -319,10 +275,6 @@ let string_of_bound b = let print_bound fmt b = Format.fprintf fmt "%s" (string_of_bound b) -let pp_name ppf (_ns, s) = - (* Names are pre-mangled *) - Dolmen.Smtlib2.Script.Poly.Print.id ppf (Dolmen.Std.Name.simple s) - module AEPrinter = struct let pp_operator ppf op = match op with @@ -427,9 +379,9 @@ module AEPrinter = struct (* Core theory *) | True -> Fmt.pf ppf "true" | False -> Fmt.pf ppf "false" - | Name { ns; hs; _ } -> pp_name ppf (ns, Hstring.view hs) - | Var v when show_vars -> Fmt.pf ppf "'%s'" (Var.to_string v) - | Var v -> Fmt.string ppf (Var.to_string v) + | Name { id; _ } -> Id.pp ppf id + | Var v when show_vars -> Fmt.pf ppf "'%s'" (Var.show v) + | Var v -> Fmt.string ppf (Var.show v) (* Reals and Ints theories *) | Int i -> Z.pp_print ppf i @@ -442,7 +394,7 @@ module AEPrinter = struct (* Symbols used in semantic triggers *) | In (lb, rb) -> Fmt.pf ppf "%s, %s" (string_of_bound lb) (string_of_bound rb) - | MapsTo v -> Fmt.pf ppf "%a |->" Var.print v + | MapsTo v -> Fmt.pf ppf "%a |->" Var.pp v end module SmtPrinter = struct @@ -527,9 +479,9 @@ let to_string_clean sy = let to_string sy = Fmt.str "%a" (AEPrinter.pp ~show_vars:true) sy -let fresh_skolem_string base = Id.Namespace.Skolem.fresh ~base () -let fresh_skolem_name base = name ~ns:Skolem (fresh_skolem_string base) -let fresh_skolem_var base = Var.of_string (fresh_skolem_string base) +let fresh_skolem_name base = name @@ Id.of_string ~ns:Skolem base + +let fresh_skolem_var base = Var.of_id @@ Id.fresh ~base ~ns:Skolem () let is_get f = equal f (Op Get) let is_set f = equal f (Op Set) diff --git a/src/lib/structures/symbols.mli b/src/lib/structures/symbols.mli index eb93fb3e79..b7a037b206 100644 --- a/src/lib/structures/symbols.mli +++ b/src/lib/structures/symbols.mli @@ -77,70 +77,6 @@ type form = type name_kind = Ac | Other -(** The [name_space] type discriminates the different types of names. The same - string in different name spaces is considered as different names. - - Note that the names stored in the [Name] constructor below are mangled - during creation of the symbol: a special prefix is added depending on the - name space. *) -type name_space = - | User - (** This symbol was defined by the user, and appears as is somewhere in a - source file. - - As an exception, if the name we got from the user starts with either "." - or "@" (which are prefixes reserved for solver use in the SMT-LIB - standard), the name will be printed with an extra ".". So if the user - writes ".x" or "@x", it will be printed as "..x" and ".@x" instead. - - Normally, this shouldn't occur, but we do this to ensure no confusion - even if invalid names ever sneak through. *) - | Internal - (** This symbol is an internal implementation detail of the solver, such as - a proxy formula or the abstracted counterpart of AC symbols. - - Internal names are printed with a ".!" prefix. *) - | Fresh - (** This symbol is a "fresh" internal name. Fresh internal names play a - similar role as internal names, but they always represent a constant - that was introduced during solving as part of some kind of purification - or abstraction procedure. - - In order to correctly implement AC(X) in the presence of distributive - symbols, symbols generated for AC(X) abstraction use a special - namespace, [Fresh_ac] below. - - To ensure uniqueness, fresh names must always be generated using - [Id.Namespace.Internal.fresh ()]. - - In particular, fresh names are only used to denote constants, not - arbitrary functions. *) - | Fresh_ac - (** This symbol has been introduced as part of the AC(X) abstraction process. - This is notably used by some parts of AC(X) that check if terms contains - fresh symbols (see [contains_a_fresh_alien] in the [Arith] module for an - example). - - These correspond to the K sort in the AC(X) paper. They use a different - name space from other fresh symbols because we need to be able to know - whether a fresh symbol comes from the AC(X) abstraction procedure in order - to prevent loops. - - To ensure uniqueness, AC abstraction names must always be generated using - [Id.Namespace.Internal.fresh ()]. *) - | Skolem - (** This symbol has been introduced as part of skolemization, and represents - the (dependent) variable of an existential quantifier. Skolem names can - have arbitrary arity to depend on previous skolem names in binding order - (so if you have `(exists (x y) e)` then there will be a skolem variable - `sko_x` and a skolem function `(sko_y sko_x)`). *) - | Abstract - (** This symbol has been introduced as part of model generation, and - represents an abstract value. - - To ensure uniqueness, abstract names must always be generated using - [Id.Namespace.Abstract.fresh ()]. *) - type bound_kind = Unbounded | VarBnd of Var.t | ValBnd of Numbers.Q.t type bound = private @@ -149,12 +85,7 @@ type bound = private type t = | True | False - | Name of - { hs : Id.t - (** Note: [hs] is prefixed according to [ns]. *) - ; kind : name_kind - ; defined : bool - ; ns : name_space } + | Name of { id : Id.t ; kind : name_kind } | Int of Z.t | Real of Q.t | Bitv of int * Z.t @@ -166,15 +97,9 @@ type t = | MapsTo of Var.t | Let -(** Create a new symbol with the given name. - - By default, names are created in the [User] name space. - - Note that names are pre-mangled: the [hs] field of the resulting name may - not be exactly the name that was passed to this function (however, calling - `name` with the same string but two different name spaces is guaranteed to - return two [Name]s with distinct [hs] fields). *) -val name : ?kind:name_kind -> ?defined:bool -> ?ns:name_space -> string -> t +val name : ?kind:name_kind -> Id.t -> t +(** Create a new symbol with the given identifier. + By default, the kind is is [Other]. *) val var : Var.t -> t val int : string -> t @@ -205,15 +130,13 @@ val print : t Fmt.t val to_string_clean : t -> string val print_clean : t Fmt.t -val pp_name : (name_space * string) Fmt.t - val pp_ae_operator : operator Fmt.t -(* [pp_ae_operator ppf op] prints the operator symbol [op] on the - formatter [ppf] using the Alt-Ergo native format. *) +(** [pp_ae_operator ppf op] prints the operator symbol [op] on the + formatter [ppf] using the Alt-Ergo native format. *) val pp_smtlib_operator : operator Fmt.t -(* [pp_smtlib_operator ppf op] prints the operator symbol [op] on the - formatter [ppf] using the SMT-LIB format. *) +(** [pp_smtlib_operator ppf op] prints the operator symbol [op] on the + formatter [ppf] using the SMT-LIB format. *) (*val dummy : t*) diff --git a/src/lib/structures/var.ml b/src/lib/structures/var.ml index a451f569b9..903735c5f7 100644 --- a/src/lib/structures/var.ml +++ b/src/lib/structures/var.ml @@ -25,7 +25,6 @@ (* *) (**************************************************************************) -type repr = Underscore | Local of Hstring.t | Named of Hstring.t (** A variable can be: - The special `Underscore` variable that is used to discard values in @@ -37,63 +36,61 @@ type repr = Underscore | Local of Hstring.t | Named of Hstring.t user. Depending on the input format, regular variable may start with '?' (e.g. in SMT-LIB format, this is allowed). *) +type t = + | Underscore + | Local of Id.t + | Named of Id.t + +let[@inline always] local id = + assert ( + let s = Id.show id in + Compat.String.starts_with ~prefix:"?" s); + Local id + +let[@inline always] of_id i = + assert ( + match i with + | Id.Term_cst _ | Hstring { ns = Skolem; _ } -> true + | _ -> false); + Named i + +(* Note: there is a single [Underscore] variable, with id 0. *) +let underscore = Underscore + +let is_local v = match v with Local _ -> true | _ -> false + +let uid v = + match v with + | Underscore -> 0 + | Local i -> 3 * Id.hash i + 1 + | Named i -> 3 * Id.hash i + 2 + +let hash = uid let equal_repr v1 v2 = match v1, v2 with | Underscore, Underscore -> true | Underscore, _ | _, Underscore -> false - | Local hs1, Local hs2 - | Named hs1, Named hs2 -> Hstring.equal hs1 hs2 + | Local i1, Local i2 + | Named i1, Named i2 -> Id.equal i1 i2 | Local _, Named _ | Named _, Local _ -> false -let pp_repr ppf = function - | Underscore -> Fmt.pf ppf "_" - | Local hs | Named hs -> Hstring.print ppf hs - -type t = { repr : repr ; id : int } - -let fresh, save_cnt, reinit_cnt = - let cpt = ref 0 in - let fresh repr = incr cpt; { repr ; id = !cpt } in - let saved_cnt = ref 0 in - let save_cnt () = - saved_cnt := !cpt - in - let reinit_cnt () = - cpt := !saved_cnt - in - fresh, save_cnt, reinit_cnt - -let of_hstring hs = fresh (Named hs) - -let of_string s = of_hstring (Hstring.make s) - -let local s = - assert (String.length s > 0 && Char.equal '?' s.[0]); - fresh (Local (Hstring.make s)) - -let is_local { repr; _ } = match repr with Local _ -> true | _ -> false - let compare a b = - let c = a.id - b.id in + let c = (uid a) - (uid b) in if c <> 0 then c else begin - assert (equal_repr a.repr b.repr); + assert (equal_repr a b); c end let equal a b = compare a b = 0 -let uid { id; _ } = id - -let hash = uid - -(* Note: there is a single [Underscore] variable, with id 1. *) -let underscore = fresh Underscore - -let print ppf { repr; id } = Fmt.pf ppf "%a~%d" pp_repr repr id +let pp ppf = function + | Underscore -> Fmt.pf ppf "_" + | Local i | Named i -> + Fmt.pf ppf "%a~%d" Id.pp i (Id.hash i) -let to_string = Fmt.to_to_string print +let show = Fmt.to_to_string pp module Set = Set.Make(struct type nonrec t = t let compare = compare end) @@ -104,5 +101,5 @@ module Map = struct let sep ppf () = Fmt.pf ppf " -> " in Fmt.box @@ Fmt.braces @@ Fmt.iter_bindings ~sep:Fmt.comma iter - @@ Fmt.pair ~sep print pp_elt + @@ Fmt.pair ~sep pp pp_elt end diff --git a/src/lib/structures/var.mli b/src/lib/structures/var.mli index 128eb2eb1e..2bfd651968 100644 --- a/src/lib/structures/var.mli +++ b/src/lib/structures/var.mli @@ -26,20 +26,20 @@ (**************************************************************************) type t +(** Type of variable. *) -val of_hstring : Hstring.t -> t -(** Create a *fresh* variable with the given name. +val of_id : Id.t -> t +(** Create a variable from an identifier. *) - Calling [of_hstring] twice with the same [Hstring.t] as argument will result - in *distinct* variables. *) - -val of_string : string -> t -(** Convenient alias for [of_hstring (Hstring.make s)]. *) - -val local : string -> t +val local : Id.t -> t (** Create a new "local" variable. Local variables are variables used exclusively in user-defined theories for semantic triggers, and are - implicitly bound at the level of the enclosing quantifier. *) + implicitly bound at the level of the enclosing quantifier. + They must starts with `?`. *) + +val underscore : t +(** Unique special variable. Used to indicate fields that should be ignored in + pattern matching and triggers. *) val is_local : t -> bool (** Indicates whether the given variable is a local variable (see {!local} above @@ -54,21 +54,9 @@ val hash : t -> int val uid : t -> int (** Globally unique identifier for the variable. *) -val underscore : t -(** Unique special variable. Used to indicate fields that should be ignored in - pattern matching and triggers. *) - -val print : Format.formatter -> t -> unit - -val to_string : t -> string - -val save_cnt: unit -> unit -(** Saves the values of the counter *) +val pp : Format.formatter -> t -> unit -val reinit_cnt: unit -> unit -(** Reinitializes the counter to the saved value with [save_cnt], 1 if no value - is saved, since after the initialization of the modules [cnt] is set to 1 - when initializing the [underscore] constant in the Symbols module *) +val show : t -> string module Set : Set.S with type elt = t diff --git a/src/lib/util/util.ml b/src/lib/util/util.ml index 6f43b934b8..2b0f407511 100644 --- a/src/lib/util/util.ml +++ b/src/lib/util/util.ml @@ -202,3 +202,29 @@ let rec print_list_pp ~sep ~pp fmt = function let internal_error msg = Format.kasprintf (fun s -> raise (Internal_error s)) msg + +module DStd = Dolmen.Std + +let pp_term_cst ppf t = + let show = Fmt.to_to_string DStd.Expr.Term.Const.print in + Dolmen.Smtlib2.Script.Poly.Print.id ppf + @@ DStd.Name.simple (show t) + +let show_term_cst = Fmt.to_to_string pp_term_cst + +(** Helper function: returns the basename of a dolmen path, since in AE + the problems are contained in one-file (for now at least), the path is + irrelevant and only the basename matters *) +let get_basename = function + | DStd.Path.Local { name; } + | Absolute { name; path = []; } -> name + | Absolute { name; path; } -> + Fmt.failwith + "Expected an empty path to the basename: \"%s\" but got: [%a]." + name (fun fmt l -> + match l with + | h :: t -> + Format.fprintf fmt "%s" h; + List.iter (Format.fprintf fmt "; %s") t + | _ -> () + ) path diff --git a/src/lib/util/util.mli b/src/lib/util/util.mli index 196e922c78..7c5d48443a 100644 --- a/src/lib/util/util.mli +++ b/src/lib/util/util.mli @@ -134,3 +134,12 @@ val print_list_pp: Format.formatter -> 'a list -> unit val internal_error : ('a, Format.formatter, unit, 'b) format4 -> 'a + +val pp_term_cst : Dolmen.Std.Expr.term_cst Fmt.t +(** [pp_term_cst ppf t] prints the constant term to the formatter [ppf], + surrounding it with quotes, if it needs. *) + +val show_term_cst : Dolmen.Std.Expr.term_cst -> string +(** Same as pp_term_cst but outpus the result as a string. *) + +val get_basename : Dolmen.Std.Path.t -> string diff --git a/tests/issues/854/function.default.expected b/tests/issues/854/function.default.expected index 63577badcf..6e5eeb8fb5 100644 --- a/tests/issues/854/function.default.expected +++ b/tests/issues/854/function.default.expected @@ -1,8 +1,8 @@ unknown ( - (define-fun a () Int 0) (define-fun intrefqtmk ((_arg_0 Int)) intref (as @a4 intref)) + (define-fun a () Int 0) (define-fun f ((_arg_0 Int)) Int 0) (define-fun a1 () Int 0) ) diff --git a/tests/issues/854/original.default.expected b/tests/issues/854/original.default.expected index a0ce9f571c..7d40ab42e2 100644 --- a/tests/issues/854/original.default.expected +++ b/tests/issues/854/original.default.expected @@ -1,7 +1,7 @@ unknown ( - (define-fun a () Int 0) (define-fun intrefqtmk ((_arg_0 Int)) intref (as @a3 intref)) + (define-fun a () Int 0) (define-fun a1 () Int 0) ) diff --git a/tests/issues/854/twice_eq.default.expected b/tests/issues/854/twice_eq.default.expected index 3488c940f2..ee4c1de0d3 100644 --- a/tests/issues/854/twice_eq.default.expected +++ b/tests/issues/854/twice_eq.default.expected @@ -1,8 +1,8 @@ unknown ( - (define-fun a () Int 0) (define-fun intrefqtmk ((_arg_0 Int)) intref (as @a4 intref)) (define-fun another_mk ((_arg_0 Int)) intref (as @a4 intref)) + (define-fun a () Int 0) (define-fun a1 () Int 0) ) diff --git a/tests/models/adt/arith.default.expected b/tests/models/adt/arith.default.expected index 18e539f318..7da79872d1 100644 --- a/tests/models/adt/arith.default.expected +++ b/tests/models/adt/arith.default.expected @@ -1,8 +1,8 @@ unknown ( - (define-fun x () Real 2.0) - (define-fun y () Real 0.0) (define-fun a () Data (cons1 2.0 0.0)) (define-fun b () Data (cons3 0.0)) + (define-fun x () Real 2.0) + (define-fun y () Real 0.0) ) diff --git a/tests/models/arith/arith11.default.expected b/tests/models/arith/arith11.default.expected index 216672887e..35ae71285c 100644 --- a/tests/models/arith/arith11.default.expected +++ b/tests/models/arith/arith11.default.expected @@ -1,10 +1,10 @@ unknown ( - (define-fun x () Real 2.0) - (define-fun y () Real (as @a0 Real)) (define-fun p1 () Bool false) (define-fun p2 () Bool true) + (define-fun x () Real 2.0) + (define-fun y () Real (as @a0 Real)) ) (objectives (x 2.0) diff --git a/tests/models/array/embedded-array.default.expected b/tests/models/array/embedded-array.default.expected index 0cb5c3d3ec..057bc1a6c0 100644 --- a/tests/models/array/embedded-array.default.expected +++ b/tests/models/array/embedded-array.default.expected @@ -1,8 +1,8 @@ unknown ( + (define-fun s () S (as @a2 S)) (define-fun x () Pair (pair (store (as @a3 (Array Int S)) 0 s) (store (as @a3 (Array Int S)) 0 s))) - (define-fun s () S (as @a2 S)) ) diff --git a/tests/models/bool/bool1.default.expected b/tests/models/bool/bool1.default.expected index 1eb3e25e7d..3a2ce307f4 100644 --- a/tests/models/bool/bool1.default.expected +++ b/tests/models/bool/bool1.default.expected @@ -4,8 +4,8 @@ unknown (define-fun p () Bool true) (define-fun q () Bool true) ) -((notp false) - (notnq false)) +((notnq false) + (notp false)) unknown @@ -13,6 +13,6 @@ unknown (define-fun p () Bool true) (define-fun q () Bool true) ) -((notp false) - (notnq false)) +((notnq false) + (notp false)) diff --git a/tests/models/bool/bool3.default.expected b/tests/models/bool/bool3.default.expected index 341a2df7ef..ed7a9b1e24 100644 --- a/tests/models/bool/bool3.default.expected +++ b/tests/models/bool/bool3.default.expected @@ -4,6 +4,6 @@ unknown (define-fun x () Bool true) (define-fun y () Bool true) ) -((foo true) - (bar false)) +((bar false) + (foo true)) diff --git a/tests/models/records/record3.default.expected b/tests/models/records/record3.default.expected index 8b2d9f83ae..b478bf755b 100644 --- a/tests/models/records/record3.default.expected +++ b/tests/models/records/record3.default.expected @@ -1,7 +1,7 @@ unknown ( + (define-fun f ((_arg_0 Int)) Pair (pair 5 0)) (define-fun x () Int 0) (define-fun y () Int 5) - (define-fun f ((_arg_0 Int)) Pair (pair 5 0)) ) diff --git a/tests/models/uf/uf1.default.expected b/tests/models/uf/uf1.default.expected index d3b170c21e..2891baf569 100644 --- a/tests/models/uf/uf1.default.expected +++ b/tests/models/uf/uf1.default.expected @@ -1,7 +1,7 @@ unknown ( + (define-fun f ((_arg_0 Int)) Int 0) (define-fun a () Int 0) (define-fun b () Int 0) - (define-fun f ((_arg_0 Int)) Int 0) ) diff --git a/tests/models/uf/uf2.default.expected b/tests/models/uf/uf2.default.expected index 232c59a455..faa7fb056c 100644 --- a/tests/models/uf/uf2.default.expected +++ b/tests/models/uf/uf2.default.expected @@ -1,7 +1,7 @@ unknown ( + (define-fun f ((arg_0 Int)) Int (ite (= arg_0 0) 1 0)) (define-fun a () Int 0) (define-fun b () Int (- 1)) - (define-fun f ((arg_0 Int)) Int (ite (= arg_0 0) 1 0)) ) From d501b4f426c307e5de23d06f5a90321a20e3202d Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Mon, 3 Feb 2025 11:00:05 +0100 Subject: [PATCH 2/7] Use identifier for lemma names --- src/bin/js/worker_js.ml | 5 +- src/lib/frontend/frontend.ml | 33 ++++++----- src/lib/frontend/frontend.mli | 6 +- src/lib/frontend/translate.ml | 82 ++++++++++++++------------- src/lib/frontend/translate.mli | 2 +- src/lib/reasoners/ccx.ml | 2 +- src/lib/reasoners/ccx.mli | 2 +- src/lib/reasoners/fun_sat.ml | 38 ++++++++----- src/lib/reasoners/fun_sat.mli | 4 +- src/lib/reasoners/instances.ml | 16 ++---- src/lib/reasoners/instances.mli | 2 +- src/lib/reasoners/intervalCalculus.ml | 8 +-- src/lib/reasoners/matching.ml | 4 +- src/lib/reasoners/sat_solver_sig.ml | 4 +- src/lib/reasoners/sat_solver_sig.mli | 4 +- src/lib/reasoners/satml.ml | 2 +- src/lib/reasoners/satml.mli | 2 +- src/lib/reasoners/satml_frontend.ml | 12 ++-- src/lib/reasoners/theory.ml | 2 +- src/lib/reasoners/theory.mli | 2 +- src/lib/reasoners/uf.mli | 2 +- src/lib/structures/commands.ml | 16 +++--- src/lib/structures/commands.mli | 8 +-- src/lib/structures/explanation.ml | 10 ++-- src/lib/structures/explanation.mli | 2 +- src/lib/structures/expr.ml | 41 ++++++++------ src/lib/structures/expr.mli | 16 +++--- src/lib/structures/id.ml | 10 ++-- src/lib/structures/id.mli | 5 +- src/lib/structures/modelMap.ml | 7 ++- src/lib/structures/modelMap.mli | 11 ++-- src/lib/util/printer.ml | 2 +- src/lib/util/printer.mli | 10 ++-- 33 files changed, 200 insertions(+), 172 deletions(-) diff --git a/src/bin/js/worker_js.ml b/src/bin/js/worker_js.ml index b86340b996..e1a1224361 100644 --- a/src/bin/js/worker_js.ml +++ b/src/bin/js/worker_js.ml @@ -107,12 +107,13 @@ let main worker_id filename filecontent = let used = if Options.get_unsat_core () then Worker_interface.Unused else Worker_interface.Unknown in - (name,b.Lexing.pos_lnum,e.Lexing.pos_lnum,!nb,used) :: acc + (Id.show name,b.Lexing.pos_lnum,e.Lexing.pos_lnum, + !nb,used) :: acc | _ -> acc end | Some r -> let b,e = r.loc in - (r.name,b.Lexing.pos_lnum,e.Lexing.pos_lnum, + (Id.show r.name,b.Lexing.pos_lnum,e.Lexing.pos_lnum, !nb,Worker_interface.Used) :: acc ) tbl [] diff --git a/src/lib/frontend/frontend.ml b/src/lib/frontend/frontend.ml index 37690ba0ed..2b8df1573c 100644 --- a/src/lib/frontend/frontend.ml +++ b/src/lib/frontend/frontend.ml @@ -32,12 +32,12 @@ open Options module E = Expr module Ex = Explanation -type used_context = Util.SS.t option +type used_context = Id.Set.t option let unused_context name context = match context with | None -> false - | Some s -> not (Util.SS.mem name s) + | Some s -> not (Id.Set.mem name s) type status = | Unsat of Commands.sat_tdecl * Ex.t @@ -147,11 +147,11 @@ module type S = sig val pop : int process - val assume : (string * E.t * bool) process + val assume : (Id.t * E.t * bool) process - val pred_def : (string * E.t) process + val pred_def : (Id.t * E.t) process - val query : (string * E.t * Ty.goal_sort) process + val query : (Id.t * E.t * Ty.goal_sort) process val th_assume : E.th_elt process @@ -169,9 +169,12 @@ end let init_with_replay_used acc f = assert (Sys.file_exists f); let cin = open_in f in - let acc = ref (match acc with None -> Util.SS.empty | Some ss -> ss) in + let acc = ref (match acc with None -> Id.Set.empty | Some ss -> ss) in try - while true do acc := Util.SS.add (input_line cin) !acc done; + while true do + (* TODO: check this line? *) + acc := Id.Set.add (Id.of_string ~ns:Internal (input_line cin)) !acc + done; assert false with End_of_file -> Some !acc @@ -238,7 +241,7 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct let output_used_context g_name dep = let f = Options.get_used_context_file () in - let cout = open_out (sprintf "%s.%s.used" f g_name) in + let cout = open_out (asprintf "%s.%a.used" f Id.pp g_name) in let cfmt = Format.formatter_of_out_channel cout in Ex.print_unsat_core cfmt dep; close_out cout @@ -258,7 +261,7 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct (fun f -> SAT.assume satenv {E.ff=f; - origin_name = ""; + origin_name = Id.of_string ~ns:Internal ""; gdist = -1; hdist = -1; trigger_depth = max_int; @@ -276,7 +279,7 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct ignore (SAT.unsat satenv {E.ff=E.vrai; - origin_name = ""; + origin_name = Id.of_string ~ns:Internal ""; gdist = -1; hdist = -1; trigger_depth = max_int; @@ -297,7 +300,8 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct if Options.get_unsat_core () then Ex.singleton (Ex.RootDep {name;f;loc}) else Ex.empty - let internal_decl ?(loc = Loc.dummy) (id : Id.typed) (env : env) : unit = + let internal_decl ?(loc = Loc.dummy) (id : ModelMap.typed) + (env : env) : unit = ignore loc; match env.res with | `Sat | `Unknown -> @@ -322,9 +326,12 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct let internal_assume ?(loc = Loc.dummy) - ((name, f, mf) : string * E.t * bool) + ((name, f, mf) : Id.t * E.t * bool) (env : env) = - let is_hyp = try (Char.equal '@' name.[0]) with _ -> false in + let is_hyp = + (* TODO: check this code! *) + Compat.String.starts_with ~prefix:"@" (Id.show name) + in if is_hyp || not (unused_context name env.used_context) then let expl = if is_hyp then diff --git a/src/lib/frontend/frontend.mli b/src/lib/frontend/frontend.mli index 9622bd4181..9213add51e 100644 --- a/src/lib/frontend/frontend.mli +++ b/src/lib/frontend/frontend.mli @@ -71,11 +71,11 @@ module type S = sig val pop : int process - val assume : (string * Expr.t * bool) process + val assume : (Id.t * Expr.t * bool) process - val pred_def : (string * Expr.t) process + val pred_def : (Id.t * Expr.t) process - val query : (string * Expr.t * Ty.goal_sort) process + val query : (Id.t * Expr.t * Ty.goal_sort) process val th_assume : Expr.th_elt process diff --git a/src/lib/frontend/translate.ml b/src/lib/frontend/translate.ml index 71fc7787a8..6e1f506fc7 100644 --- a/src/lib/frontend/translate.ml +++ b/src/lib/frontend/translate.ml @@ -975,7 +975,7 @@ let mk_rounding fpar = Builds an Alt-Ergo hashconsed expression from a dolmen term *) let rec mk_expr - ?(loc = Loc.dummy) ?(name_base = "") ?(toplevel = false) + ?(loc = Loc.dummy) ~name ?(toplevel = false) ~decl_kind dt = let name_tag = ref 0 in let rec aux_mk_expr ?(toplevel = false) @@ -1457,12 +1457,14 @@ let rec mk_expr Cache.store_tyvl tyvl; aux_mk_expr ~toplevel:true body end - else - let name = - if !name_tag = 0 then name_base - else Format.sprintf "#%s#sub-%d" name_base !name_tag - in - incr name_tag; + else ( + (* let name = + let base = + if !name_tag = 0 then name_base + else Format.sprintf "#%s#sub-" name_base + in + Id.fresh ~base ~ns:Fresh () + in *) if tyvl != [] then Cache.store_tyvl tyvl; (* the following is done in two iterations to preserve the order *) @@ -1508,7 +1510,7 @@ let rec mk_expr let triggers = List.map ( fun t -> - make_trigger ~loc ~name_base ~decl_kind ~in_theory + make_trigger ~loc ~name ~decl_kind ~in_theory name hyp (t, true) ) trgs in @@ -1519,7 +1521,7 @@ let rec mk_expr | _ -> assert false (* unreachable *) end in - mk name loc binders triggers qbody ~toplevel ~decl_kind + mk name loc binders triggers qbody ~toplevel ~decl_kind) | _ -> unsupported "Term %a" DE.Term.print term in match DStd.Tag.get root_tags DE.Tags.named with @@ -1605,8 +1607,8 @@ let rec mk_expr in aux_mk_expr ~toplevel dt -and make_trigger ?(loc = Loc.dummy) ~name_base ~decl_kind - ~(in_theory: bool) (name: string) (hyp: E.t list) +and make_trigger ?(loc = Loc.dummy) ~name ~decl_kind + ~(in_theory: bool) (name: Id.t) (hyp: E.t list) (e, from_user: DE.term * bool) = (* Dolmen adds an existential quantifier to bind the '?xxx' variables *) let e = @@ -1631,7 +1633,7 @@ and make_trigger ?(loc = Loc.dummy) ~name_base ~decl_kind | e -> [e] in let mk_expr = - mk_expr ~loc ~name_base ~decl_kind + mk_expr ~loc ~name ~decl_kind in let content = List.map mk_expr e in (* clean trigger: @@ -1722,15 +1724,12 @@ let pp_query ?(hyps =[]) t = let axioms, goal = intro_hypothesis t in List.rev_append (List.rev_map (elim_toplevel_forall false) hyps) axioms, goal -let make_form name_base f loc ~decl_kind = - let ff = - mk_expr ~loc ~name_base ~toplevel:true ~decl_kind f - in +let make_form name f loc ~decl_kind = + let ff = mk_expr ~loc ~name ~toplevel:true ~decl_kind f in assert (Var.Map.is_empty (E.free_vars ff Var.Map.empty)); let ff = E.purify_form ff in if Ty.TvSet.is_empty (E.free_type_vars ff) then ff - else - E.mk_forall name_base loc Var.Map.empty [] ff ~toplevel:true ~decl_kind + else E.mk_forall name loc Var.Map.empty [] ff ~toplevel:true ~decl_kind (* Helper function used to check if the expression defining an objective function is a pure term. *) @@ -1747,8 +1746,9 @@ let make dloc_file acc stmt = (* Optimize terms *) | { contents = `Optimize (t, is_max); loc; _ } -> let st_loc = dl_to_ael dloc_file loc in + let name = Id.of_string ~ns:Internal "" in let e = - mk_expr ~loc:st_loc ~toplevel:true ~decl_kind:Dobjective t + mk_expr ~name ~loc:st_loc ~toplevel:true ~decl_kind:Dobjective t in let fn = Objective.Function.mk ~is_max e in if not @@ is_pure_term e then @@ -1776,15 +1776,15 @@ let make dloc_file acc stmt = (* Goal and check-sat definitions *) | { - id; loc; attrs; + loc; attrs; contents = (`Goal _ | `Check _) as contents; - implicit; + implicit; _ } -> - let name = - match id.name with - | Simple name -> name - | Indexed _ | Qualified _ -> assert false - in + (* let name = + match id.name with + | Simple name -> Id.of_string ~ns:Internal name + | Indexed _ | Qualified _ -> assert false + in *) let goal_sort = match contents with | `Goal _ -> Ty.Thm @@ -1811,7 +1811,9 @@ let make dloc_file acc stmt = aux acc decl ) [] _hyps in - let e = make_form "" t st_loc ~decl_kind:E.Dgoal in + (* TODO: put a correct identifier *) + let name = Id.of_string ~ns:Internal "" in + let e = make_form name t st_loc ~decl_kind:E.Dgoal in let st_decl = C.Query (name, e, goal_sort) in C.{st_decl; st_loc} :: List.rev_append (List.rev rev_hyps_c) acc @@ -1825,11 +1827,11 @@ let make dloc_file acc stmt = implicit=_ } -> let name = match DStd.Tag.get t.term_tags lemma_name_attr with - | Some n -> n + | Some n -> Id.of_string ~ns:Internal n | None -> match DStd.Tag.get t.term_tags DE.Tags.named with - | Some n -> n - | None -> name + | Some n -> Id.of_string ~ns:Internal n + | None -> Id.of_string ~ns:Internal name in let dloc = DStd.Loc.(loc dloc_file stmt.loc) in let aloc = DStd.Loc.lexing_positions dloc in @@ -1943,10 +1945,10 @@ let make dloc_file acc stmt = append @@ List.filter_map (fun (def : Typer_Pipe.def) -> match def with - | `Term_def ( _, ({ path; tags; _ } as tcst), tyvars, terml, body) -> + | `Term_def ( _, ({ tags; _ } as tcst), tyvars, terml, body) -> Cache.store_tyvl tyvars; let st_loc = dl_to_ael dloc_file loc in - let name_base = Util.get_basename path in + let name = Id.of_term_cst tcst in let binders, defn = let rty = dty_to_ty body.term_ty in @@ -1972,12 +1974,12 @@ let make dloc_file acc stmt = | Some () -> let decl_kind = E.Dpredicate defn in let ff = - mk_expr ~loc ~name_base + mk_expr ~loc ~name ~toplevel:false ~decl_kind body in let qb = E.mk_eq ~iff:true defn ff in let ff = - E.mk_forall name_base Loc.dummy binders [] qb ~toplevel:true + E.mk_forall name Loc.dummy binders [] qb ~toplevel:true ~decl_kind in assert (Var.Map.is_empty (E.free_vars ff Var.Map.empty)); @@ -1985,20 +1987,20 @@ let make dloc_file acc stmt = let e = if Ty.TvSet.is_empty (E.free_type_vars ff) then ff else - E.mk_forall name_base loc + E.mk_forall name loc Var.Map.empty [] ff ~toplevel:true ~decl_kind in - Some C.{ st_decl = C.PredDef (e, name_base); st_loc } + Some C.{ st_decl = C.PredDef (e, name); st_loc } | None -> let decl_kind = E.Dfunction defn in let ff = - mk_expr ~loc ~name_base + mk_expr ~loc ~name ~toplevel:false ~decl_kind body in let iff = Ty.equal (Expr.type_info defn) (Ty.Tbool) in let qb = E.mk_eq ~iff defn ff in let ff = - E.mk_forall name_base Loc.dummy binders [] qb ~toplevel:true + E.mk_forall name Loc.dummy binders [] qb ~toplevel:true ~decl_kind in assert (Var.Map.is_empty (E.free_vars ff Var.Map.empty)); @@ -2006,12 +2008,12 @@ let make dloc_file acc stmt = let e = if Ty.TvSet.is_empty (E.free_type_vars ff) then ff else - E.mk_forall name_base loc + E.mk_forall name loc Var.Map.empty [] ff ~toplevel:true ~decl_kind in if Options.get_verbose () then Format.eprintf "defining term of %a@." DE.Term.print body; - Some C.{ st_decl = C.Assume (name_base, e, true); st_loc } + Some C.{ st_decl = C.Assume (name, e, true); st_loc } end | `Type_alias _ -> None | `Instanceof _ -> diff --git a/src/lib/frontend/translate.mli b/src/lib/frontend/translate.mli index abb36451c9..baa51d5752 100644 --- a/src/lib/frontend/translate.mli +++ b/src/lib/frontend/translate.mli @@ -33,7 +33,7 @@ val dty_to_ty : ?update:bool -> ?is_var:bool -> D_loop.DStd.Expr.ty -> Ty.t *) val make_form : - string -> + Id.t -> D_loop.DStd.Expr.term -> Loc.t -> decl_kind:Expr.decl_kind -> diff --git a/src/lib/reasoners/ccx.ml b/src/lib/reasoners/ccx.ml index 4b4bac58d4..c6f8341aec 100644 --- a/src/lib/reasoners/ccx.ml +++ b/src/lib/reasoners/ccx.ml @@ -88,7 +88,7 @@ module type S = sig val extract_concrete_model : prop_model:Expr.Set.t -> - declared_ids:Id.typed list -> + declared_ids:ModelMap.typed list -> t -> Models.t end diff --git a/src/lib/reasoners/ccx.mli b/src/lib/reasoners/ccx.mli index 83c09ed508..3b2091a54d 100644 --- a/src/lib/reasoners/ccx.mli +++ b/src/lib/reasoners/ccx.mli @@ -78,7 +78,7 @@ module type S = sig val extract_concrete_model : prop_model:Expr.Set.t -> - declared_ids:Id.typed list -> + declared_ids:ModelMap.typed list -> t -> Models.t end diff --git a/src/lib/reasoners/fun_sat.ml b/src/lib/reasoners/fun_sat.ml index 5480e2d498..436b6a5dce 100644 --- a/src/lib/reasoners/fun_sat.ml +++ b/src/lib/reasoners/fun_sat.ml @@ -88,7 +88,8 @@ module Make (Th : Theory.S) = struct if Options.get_no_decisions_on_is_empty () then delta, [] else List.partition - (fun (a, _,_,_) -> Options.get_can_decide_on a.E.origin_name) delta + (fun (a, _,_,_) -> + Options.get_can_decide_on (Id.show a.E.origin_name)) delta in let dec = List.rev_map @@ -178,8 +179,8 @@ module Make (Th : Theory.S) = struct last_saved_model : Models.t Lazy.t option ref; unknown_reason : Sat_solver_sig.unknown_reason option; - declare_top : Id.typed list ref; - declare_tail : Id.typed list Stack.t; + declare_top : ModelMap.typed list ref; + declare_tail : ModelMap.typed list Stack.t; (** Stack of the declared symbols by the user. The field [declare_top] is the top of the stack and [declare_tail] is tail. In particular, this stack is never empty. *) @@ -276,7 +277,7 @@ module Make (Th : Theory.S) = struct | None -> "" | Some ff -> begin match E.form_view ff with - | E.Lemma xx -> xx.E.name + | E.Lemma xx -> Id.show xx.E.name | E.Unit _ | E.Clause _ | E.Literal _ | E.Skolem _ | E.Let _ | E.Iff _ | E.Xor _ -> "" end @@ -408,10 +409,10 @@ module Make (Th : Theory.S) = struct if Options.get_debug_fpa() > 1 || Options.get_debug_sat() then print_dbg ~module_name:"Fun_sat" ~function_name:"print_theory_instances" - "@[@ %s >@ \ + "@[@ %a >@ \ hypotheses: %a@ \ conclusion: %a@]" - (E.name_of_lemma_opt gf.E.lem) + Id.pp (E.name_of_lemma_opt gf.E.lem) print_f_conj hyp E.print gf.E.ff @@ -600,7 +601,9 @@ module Make (Th : Theory.S) = struct let cdcl_learn_clause delay env ex acc0 = let f = shift env.gamma ex acc0 in - let ff = mk_gf f "" true true in + let ff = + mk_gf f (Id.of_string ~ns:Internal "") true true + in cdcl_assume delay env [ff, Ex.empty] let profile_conflicting_instances exp = @@ -608,8 +611,8 @@ module Make (Th : Theory.S) = struct SE.iter (fun f -> match E.form_view f with - | E.Lemma { E.name; loc; _ } -> - Profiling.conflicting_instance name loc + | E.Lemma { name; loc; _ } -> + Profiling.conflicting_instance (Id.show name) loc | E.Unit _ | E.Clause _ | E.Literal _ | E.Skolem _ | E.Let _ | E.Iff _ | E.Xor _ -> () )(Ex.formulas_of exp) @@ -622,7 +625,9 @@ module Make (Th : Theory.S) = struct "performing case-split"; let tbox, new_terms = Th.do_case_split env.tbox origin in let inst = - Inst.add_terms env.inst new_terms (mk_gf E.vrai "" false false) in + Inst.add_terms env.inst new_terms + (mk_gf E.vrai (Id.of_string ~ns:Internal "") false false) + in {env with tbox = tbox; inst = inst} with Ex.Inconsistent (expl, classes) -> Debug.inconsistent expl env; @@ -885,7 +890,8 @@ module Make (Th : Theory.S) = struct raise e in let utbox = if env.dlevel = 0 then tbox else utbox in - let inst = Inst.add_terms inst new_terms (mk_gf E.vrai "" mf gf) in + let inst = Inst.add_terms inst new_terms + (mk_gf E.vrai (Id.of_string ~ns:Internal "") mf gf) in Steps.incr (Th_assumed cpt); { env with tbox = tbox; unit_tbox = utbox; inst = inst } @@ -1429,7 +1435,7 @@ module Make (Th : Theory.S) = struct in let new_level = env.dlevel + 1 in if Options.get_profiling() then - Profiling.decision new_level a.E.origin_name; + Profiling.decision new_level (Id.show a.E.origin_name); (*fprintf fmt "@.BEFORE DECIDING %a@." E.print f;*) Options.heavy_assert (fun () -> cdcl_same_decisions env); let env_a = @@ -1633,7 +1639,8 @@ module Make (Th : Theory.S) = struct let new_guard = E.fresh_name Ty.Tbool in save_guard_and_refs acc new_guard; let guards = ME.add new_guard - (mk_gf new_guard "" true true,Ex.empty) + (mk_gf new_guard + (Id.of_string ~ns:Internal "") true true,Ex.empty) acc.guards.guards in Stack.push !(env.declare_top) env.declare_tail; {acc with guards = @@ -1661,7 +1668,8 @@ module Make (Th : Theory.S) = struct assert (not (Stack.is_empty acc.guards.stack_elt)); let new_current_guard,_ = Stack.top acc.guards.stack_elt in let guards = ME.add guard_to_neg - (mk_gf (E.neg guard_to_neg) "" true true,Ex.empty) + (mk_gf (E.neg guard_to_neg) + (Id.of_string ~ns:Internal "") true true, Ex.empty) acc.guards.guards in acc.model_gen_phase := false; @@ -1806,7 +1814,7 @@ module Make (Th : Theory.S) = struct (* initialize some structures in SAT.empty. Otherwise, E.faux is never added as it is replaced with (not E.vrai) *) reset_refs (); - let gf_true = mk_gf E.vrai "" true true in + let gf_true = mk_gf E.vrai (Id.of_string ~ns:Internal "") true true in let inst = Inst.empty in let tbox = Th.empty () in let inst = Inst.add_terms inst (SE.singleton E.vrai) gf_true in diff --git a/src/lib/reasoners/fun_sat.mli b/src/lib/reasoners/fun_sat.mli index 6e018f04e0..8146209ca3 100644 --- a/src/lib/reasoners/fun_sat.mli +++ b/src/lib/reasoners/fun_sat.mli @@ -37,7 +37,7 @@ module Make (_ : Theory.S) : sig val empty : ?selector:(Expr.t -> bool) -> unit -> t - val declare : t -> Id.typed -> t + val declare : t -> ModelMap.typed -> t val push : t -> int -> t @@ -50,7 +50,7 @@ module Make (_ : Theory.S) : sig val assume_th_elt : t -> Expr.th_elt -> Explanation.t -> t - val pred_def : t -> Expr.t -> string -> Explanation.t -> Loc.t -> t + val pred_def : t -> Expr.t -> Id.t -> Explanation.t -> Loc.t -> t val unsat : t -> Expr.gformula -> Explanation.t diff --git a/src/lib/reasoners/instances.ml b/src/lib/reasoners/instances.ml index 280d3c7dab..384f8bea16 100644 --- a/src/lib/reasoners/instances.ml +++ b/src/lib/reasoners/instances.ml @@ -43,7 +43,7 @@ module type S = sig val add_predicate : t -> guard:Expr.t -> - name:string -> + name:Id.t -> Expr.gformula -> Ex.t -> t @@ -123,7 +123,7 @@ module Make(X : Theory.S) : S with type tbox = X.t = struct let new_facts_of_axiom ax insts_ok = if get_debug_matching () >= 1 && insts_ok != ME.empty then let name = match Expr.form_view ax with - | E.Lemma { E.name = s; _ } -> s + | E.Lemma { name; _ } -> Id.show name | E.Unit _ | E.Clause _ | E.Literal _ | E.Skolem _ | E.Let _ | E.Iff _ | E.Xor _ -> "!(no-name)" in @@ -169,9 +169,7 @@ module Make(X : Theory.S) : S with type tbox = X.t = struct matching = EM.max_term_depth env.matching (E.depth f) } in match E.form_view f with | E.Iff (f1, f2) -> - let p = - E.mk_term (Symbols.name @@ Id.of_string ~ns:Internal name) [] Ty.Tbool - in + let p = E.mk_term (Symbols.name name) [] Ty.Tbool in let np = E.neg p in let defn = if E.equal f1 p then f2 @@ -181,9 +179,7 @@ module Make(X : Theory.S) : S with type tbox = X.t = struct add_ground_pred env ~guard p np defn ex | E.Literal _ -> - let p = - E.mk_term (Symbols.name @@ Id.of_string ~ns:Internal name) [] Ty.Tbool - in + let p = E.mk_term (Symbols.name name) [] Ty.Tbool in let np = E.neg p in let defn = if E.equal p f then E.vrai @@ -228,7 +224,7 @@ module Make(X : Theory.S) : S with type tbox = X.t = struct let record_this_instance f accepted lorig = match Expr.form_view lorig with | E.Lemma { E.name; loc; _ } -> - Profiling.new_instance_of name f loc accepted + Profiling.new_instance_of (Id.show name) f loc accepted | E.Unit _ | E.Clause _ | E.Literal _ | E.Skolem _ | E.Let _ | E.Iff _ | E.Xor _ -> assert false @@ -246,7 +242,7 @@ module Make(X : Theory.S) : S with type tbox = X.t = struct let diff = Expr.Set.diff st1 st0 in let info, _ = EM.terms_info env.matching in let _new = Expr.Set.filter (fun t -> not (ME.mem t info)) diff in - Profiling.register_produced_terms name loc st0 st1 diff _new + Profiling.register_produced_terms (Id.show name) loc st0 st1 diff _new let inst_is_seen_during_this_round orig f insts = try diff --git a/src/lib/reasoners/instances.mli b/src/lib/reasoners/instances.mli index 75749ad9a5..a49d3caa13 100644 --- a/src/lib/reasoners/instances.mli +++ b/src/lib/reasoners/instances.mli @@ -36,7 +36,7 @@ module type S = sig val add_predicate : t -> guard:Expr.t -> - name:string -> + name:Id.t -> Expr.gformula -> Explanation.t -> t diff --git a/src/lib/reasoners/intervalCalculus.ml b/src/lib/reasoners/intervalCalculus.ml index 81d90fd544..e753cb8066 100644 --- a/src/lib/reasoners/intervalCalculus.ml +++ b/src/lib/reasoners/intervalCalculus.ml @@ -2330,7 +2330,7 @@ let record_this_instance f accepted lorig = if Options.get_profiling() then match E.form_view lorig with | E.Lemma { E.name; loc; _ } -> - Profiling.new_instance_of name f loc accepted + Profiling.new_instance_of (Id.show name) f loc accepted | E.Unit _ | E.Clause _ | E.Literal _ | E.Skolem _ | E.Let _ | E.Iff _ | E.Xor _ -> assert false @@ -2349,7 +2349,7 @@ let profile_produced_terms menv lorig nf s trs = let diff = SE.diff st1 st0 in let info, _ = EM.terms_info menv in let _new = SE.filter (fun t -> not (ME.mem t info)) diff in - Profiling.register_produced_terms name loc st0 st1 diff _new + Profiling.register_produced_terms (Id.show name) loc st0 st1 diff _new let new_facts_for_axiom ~do_syntactic_matching menv uf selector optimized substs accu = @@ -2467,8 +2467,8 @@ let syntactic_matching menv env uf _selector = Printer.print_dbg ~module_name:"IntervalCalculus" ~function_name:"syntactic_matching" - "syntactic matching of Ax %s: got %d substs" - (E.name_of_lemma f) !cpt + "syntactic matching of Ax %a: got %d substs" + Id.pp (E.name_of_lemma f) !cpt end; res:: accu )env.th_axioms [] diff --git a/src/lib/reasoners/matching.ml b/src/lib/reasoners/matching.ml index 8e9dedd3de..1e2a7bf838 100644 --- a/src/lib/reasoners/matching.ml +++ b/src/lib/reasoners/matching.ml @@ -666,8 +666,8 @@ module Make (X : Arg) : S with type theory = X.t = struct if Options.get_debug_triggers () then Printer.print_dbg ~module_name:"Matching" ~function_name:"add_triggers" - "@[%s triggers of %s are:@ %a@]" - kind name E.print_triggers tgs; + "@[%s triggers of %a are:@ %a@]" + kind Id.pp name E.print_triggers tgs; List.fold_left (fun env tr -> let info = diff --git a/src/lib/reasoners/sat_solver_sig.ml b/src/lib/reasoners/sat_solver_sig.ml index c8450e6d34..2531ccaed7 100644 --- a/src/lib/reasoners/sat_solver_sig.ml +++ b/src/lib/reasoners/sat_solver_sig.ml @@ -75,7 +75,7 @@ module type S = sig The optional argument [selector] is used to filter ground facts discovered by the instantiation engine. *) - val declare : t -> Id.typed -> unit + val declare : t -> ModelMap.typed -> unit (** [declare env id] declares a new identifier [id]. If the environment [env] isn't unsatisfiable and the model generation @@ -109,7 +109,7 @@ module type S = sig (** [assume env f exp] assumes a new formula [f] with the explanation [exp] in the theory environment of [env]. *) - val pred_def : t -> Expr.t -> string -> Explanation.t -> Loc.t -> unit + val pred_def : t -> Expr.t -> Id.t -> Explanation.t -> Loc.t -> unit (** [pred_def env f] assumes a new predicate definition [f] in [env]. *) val optimize : t -> Objective.Function.t -> unit diff --git a/src/lib/reasoners/sat_solver_sig.mli b/src/lib/reasoners/sat_solver_sig.mli index 9380bbbbce..80232ffbbd 100644 --- a/src/lib/reasoners/sat_solver_sig.mli +++ b/src/lib/reasoners/sat_solver_sig.mli @@ -55,7 +55,7 @@ module type S = sig The optional argument [selector] is used to filter ground facts discovered by the instantiation engine. *) - val declare : t -> Id.typed -> unit + val declare : t -> ModelMap.typed -> unit (** [declare env id] declares a new identifier [id]. If the environment [env] isn't unsatisfiable and the model generation @@ -89,7 +89,7 @@ module type S = sig (** [assume env f exp] assumes a new formula [f] with the explanation [exp] in the theory environment of [env]. *) - val pred_def : t -> Expr.t -> string -> Explanation.t -> Loc.t -> unit + val pred_def : t -> Expr.t -> Id.t -> Explanation.t -> Loc.t -> unit (** [pred_def env f] assumes a new predicate definition [f] in [env]. *) val optimize : t -> Objective.Function.t -> unit diff --git a/src/lib/reasoners/satml.ml b/src/lib/reasoners/satml.ml index cd061c17c9..4e39114f4a 100644 --- a/src/lib/reasoners/satml.ml +++ b/src/lib/reasoners/satml.ml @@ -92,7 +92,7 @@ module type SAT_ML = sig val solve : t -> unit val compute_concrete_model : - declared_ids:Id.typed list -> + declared_ids:ModelMap.typed list -> t -> Models.t Lazy.t * Objective.Model.t diff --git a/src/lib/reasoners/satml.mli b/src/lib/reasoners/satml.mli index 166b2ff5a7..f048586c50 100644 --- a/src/lib/reasoners/satml.mli +++ b/src/lib/reasoners/satml.mli @@ -46,7 +46,7 @@ module type SAT_ML = sig val solve : t -> unit val compute_concrete_model : - declared_ids:Id.typed list -> + declared_ids:ModelMap.typed list -> t -> Models.t Lazy.t * Objective.Model.t diff --git a/src/lib/reasoners/satml_frontend.ml b/src/lib/reasoners/satml_frontend.ml index 94517019f6..b5fee38c0f 100644 --- a/src/lib/reasoners/satml_frontend.ml +++ b/src/lib/reasoners/satml_frontend.ml @@ -68,8 +68,8 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct (** The reason why satml raised [I_dont_know] if it does; [None] by default. *) - mutable declare_top : Id.typed list; - declare_tail : Id.typed list Stack.t; + mutable declare_top : ModelMap.typed list; + declare_tail : ModelMap.typed list Stack.t; (** Stack of the declared symbols by the user. The field [declare_top] is the top of the stack and [declare_tail] is tail. In particular, this stack is never empty. *) @@ -122,7 +122,7 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct { E.ff = f; trigger_depth = max_int; nb_reductions = 0; - origin_name = ""; + origin_name = Id.of_string ~ns:Internal ""; age = 0; lem = None; mf = false; @@ -170,7 +170,7 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct | None -> "" | Some ff -> begin match E.form_view ff with - | E.Lemma xx -> xx.E.name + | E.Lemma xx -> Id.show xx.E.name | E.Unit _ | E.Clause _ | E.Literal _ | E.Skolem _ | E.Let _ | E.Iff _ | E.Xor _ -> "" end @@ -339,10 +339,10 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct if Options.get_debug_fpa() > 1 || Options.get_debug_sat() then print_dbg ~module_name:"Satml_frontend" ~function_name:"theory_instance" - "@[%s >@,\ + "@[%a >@,\ hypotheses: %a@,\ conclusion: %a@]" - (E.name_of_lemma_opt gf.E.lem) + Id.pp (E.name_of_lemma_opt gf.E.lem) print_f_conj hyp E.print gf.E.ff; diff --git a/src/lib/reasoners/theory.ml b/src/lib/reasoners/theory.ml index df1cb2a170..fe1e994801 100644 --- a/src/lib/reasoners/theory.ml +++ b/src/lib/reasoners/theory.ml @@ -68,7 +68,7 @@ module type S = sig val compute_concrete_model : acts:Shostak.Literal.t Th_util.acts -> t -> unit val extract_concrete_model : - declared_ids:Id.typed list -> + declared_ids:ModelMap.typed list -> t -> Models.t Lazy.t * Objective.Model.t diff --git a/src/lib/reasoners/theory.mli b/src/lib/reasoners/theory.mli index f8c4e115d3..6379feddbb 100644 --- a/src/lib/reasoners/theory.mli +++ b/src/lib/reasoners/theory.mli @@ -59,7 +59,7 @@ module type S = sig val compute_concrete_model : acts:Shostak.Literal.t Th_util.acts -> t -> unit val extract_concrete_model : - declared_ids:Id.typed list -> + declared_ids:ModelMap.typed list -> t -> Models.t Lazy.t * Objective.Model.t diff --git a/src/lib/reasoners/uf.mli b/src/lib/reasoners/uf.mli index f73f3f7942..4051658aa0 100644 --- a/src/lib/reasoners/uf.mli +++ b/src/lib/reasoners/uf.mli @@ -160,7 +160,7 @@ val assign_next : t -> (r Xliteral.view * bool * Th_util.lit_origin) list * t (** Compute a counterexample using the Uf environment *) val extract_concrete_model : prop_model:Expr.Set.t -> - declared_ids:Id.typed list -> + declared_ids:ModelMap.typed list -> t -> Models.t diff --git a/src/lib/structures/commands.ml b/src/lib/structures/commands.ml index 20e2a9ef6e..214dd89b07 100644 --- a/src/lib/structures/commands.ml +++ b/src/lib/structures/commands.ml @@ -31,11 +31,11 @@ let src = Logs.Src.create ~doc:"Commands" __MODULE__ module Log = (val Logs.src_log src : Logs.LOG) type sat_decl_aux = - | Decl of Id.typed - | Assume of string * Expr.t * bool - | PredDef of Expr.t * string (*name of the predicate*) + | Decl of ModelMap.typed + | Assume of Id.t * Expr.t * bool + | PredDef of Expr.t * Id.t (*name of the predicate*) | Optimize of Objective.Function.t - | Query of string * Expr.t * Ty.goal_sort + | Query of Id.t * Expr.t * Ty.goal_sort | ThAssume of Expr.th_elt | Push of int | Pop of int @@ -53,12 +53,12 @@ let print_aux fmt = function Ty.print ret_ty | Assume (name, e, b) -> - Format.fprintf fmt "assume %s(%b): @[%a@]" name b Expr.print e + Format.fprintf fmt "assume %a(%b): @[%a@]" Id.pp name b Expr.print e | PredDef (e, name) -> - Format.fprintf fmt "pred-def %s: @[%a@]" name Expr.print e + Format.fprintf fmt "pred-def %a: @[%a@]" Id.pp name Expr.print e | Query (name, e, sort) -> - Format.fprintf fmt "query %s(%a): @[%a@]" - name Ty.print_goal_sort sort Expr.print e + Format.fprintf fmt "query %a(%a): @[%a@]" + Id.pp name Ty.print_goal_sort sort Expr.print e | ThAssume t -> Format.fprintf fmt "th assume %a" Expr.print_th_elt t | Push n -> Format.fprintf fmt "Push %d" n diff --git a/src/lib/structures/commands.mli b/src/lib/structures/commands.mli index 06eb89001d..0c0c6d304c 100644 --- a/src/lib/structures/commands.mli +++ b/src/lib/structures/commands.mli @@ -28,11 +28,11 @@ (* Sat entry *) type sat_decl_aux = - | Decl of Id.typed - | Assume of string * Expr.t * bool - | PredDef of Expr.t * string (*name of the predicate*) + | Decl of ModelMap.typed + | Assume of Id.t * Expr.t * bool + | PredDef of Expr.t * Id.t (*name of the predicate*) | Optimize of Objective.Function.t - | Query of string * Expr.t * Ty.goal_sort + | Query of Id.t * Expr.t * Ty.goal_sort | ThAssume of Expr.th_elt | Push of int | Pop of int diff --git a/src/lib/structures/explanation.ml b/src/lib/structures/explanation.ml index 2896e7b752..b9c2b0460d 100644 --- a/src/lib/structures/explanation.ml +++ b/src/lib/structures/explanation.ml @@ -27,7 +27,7 @@ module E = Expr -type rootdep = { name : string; f : Expr.t; loc : Loc.t} +type rootdep = { name : Id.t; f : Expr.t; loc : Loc.t} type exp = | Literal of Satml_types.Atom.atom @@ -112,7 +112,7 @@ let print fmt ex = | Literal a -> fprintf fmt "{Literal:%a}, " Satml_types.Atom.pr_atom a | Fresh i -> fprintf fmt "{Fresh:%i}" i; | Dep f -> fprintf fmt "{Dep:%a}" E.print f - | RootDep r -> fprintf fmt "{RootDep:%s}" r.name + | RootDep r -> fprintf fmt "{RootDep:%a}" Id.pp r.name | Bj f -> fprintf fmt "{BJ:%a}" E.print f ) ex; fprintf fmt "}" @@ -131,8 +131,10 @@ let print_unsat_core ?(tab=false) fmt dep = iter_atoms (function | RootDep r -> - if tab then Format.fprintf fmt " %s@." r.name (* tab is too big *) - else Format.fprintf fmt "%s@." r.name + if tab then + Format.fprintf fmt " %a@." Id.pp r.name (* tab is too big *) + else + Format.fprintf fmt "%a@." Id.pp r.name | Dep _ -> () | Bj _ | Fresh _ | Literal _ -> assert false ) dep diff --git a/src/lib/structures/explanation.mli b/src/lib/structures/explanation.mli index 7d4008eb7c..8ef4d90175 100644 --- a/src/lib/structures/explanation.mli +++ b/src/lib/structures/explanation.mli @@ -27,7 +27,7 @@ type t -type rootdep = { name : string; f : Expr.t; loc : Loc.t} +type rootdep = { name : Id.t; f : Expr.t; loc : Loc.t} type exp = | Literal of Satml_types.Atom.atom | Fresh of int diff --git a/src/lib/structures/expr.ml b/src/lib/structures/expr.ml index 1d3d8e3bec..09c62b9bc3 100644 --- a/src/lib/structures/expr.ml +++ b/src/lib/structures/expr.ml @@ -64,7 +64,7 @@ and bind_kind = | B_let of letin and quantified = { - name : string; + name : Id.t; main : t; toplevel : bool; user_trs : trigger list; @@ -378,15 +378,15 @@ module SmtPrinter = struct | Sy.F_Lemma, [], B_lemma q -> if Options.get_verbose () then - Fmt.pf ppf "@[<2>(! %a :named %s@])" pp_lemma q q.name + Fmt.pf ppf "@[<2>(! %a :named %a@])" pp_lemma q Id.pp q.name else - Fmt.string ppf q.name + Id.pp ppf q.name | Sy.F_Skolem, [], B_skolem q -> if Options.get_verbose () then - Fmt.pf ppf "@[<2>(! %a :named %s@])" pp_skolem q q.name + Fmt.pf ppf "@[<2>(! %a :named %a@])" pp_skolem q Id.pp q.name else - Fmt.string ppf q.name + Id.pp ppf q.name | _ -> assert false @@ -558,13 +558,13 @@ module AEPrinter = struct | Sy.F_Lemma, [], B_lemma { user_trs ; main ; name ; binders; _ } -> if Options.get_verbose () then - Fmt.pf ppf "@[(lemma: %s@ forall %a[%a].@ %a@])" - name + Fmt.pf ppf "@[(lemma: %a@ forall %a[%a].@ %a@])" + Id.pp name pp_binders binders pp_triggers user_trs pp_silent main else - Fmt.pf ppf "(lem %s)" name + Fmt.pf ppf "(lem %a)" Id.pp name | Sy.F_Skolem, [], B_skolem { main; binders; _ } -> Fmt.pf ppf "( %a)" @@ -829,7 +829,7 @@ let name_of_lemma f = let name_of_lemma_opt opt = match opt with - | None -> "(Lemma=None)" + | None -> Id.of_string ~ns:Internal "(Lemma=None)" | Some f -> name_of_lemma f @@ -1147,7 +1147,8 @@ let mk_forall_ter = let q = match form_view lem with Lemma q -> q | _ -> assert false in assert (equal q.main f (* should be true *)); if compare_quant q new_q <> 0 then raise Exit; - Printer.print_wrn "(sub) axiom %s replaced with %s" name q.name; + Printer.print_wrn "(sub) axiom %a replaced with %a" + Id.pp name Id.pp q.name; lem with Not_found | Exit -> let d = new_q.main.depth in (* + 1 ?? *) @@ -2363,10 +2364,10 @@ module Triggers = struct if Options.get_verbose () then Printer.print_dbg ~module_name:"Translate" ~function_name:"clean_trigger" - "AXIOM: %s@ \ + "AXIOM: %a@ \ from multi-trig of sz %d : %a@ \ to multi-trig of sz %d : %a" - name + Id.pp name sz_l print_list trig.content sz_s print_list content; { trig with content; } @@ -2610,7 +2611,15 @@ let mk_exists name loc binders trs f ~toplevel ~decl_kind = a forall quantification without term variables (ie. only with type variables). 2 - we keep the triggers of 'exists' to try to instantiate these type variables *) - let nm = Format.sprintf "#%s#sub-%d" name 0 in + let nm = + let s = Format.asprintf "#%a#sub-%d" Id.pp name 0 in + match name with + | Term_cst { tcst = { id_ty; _ }; defined } -> + DStd.Expr.Term.Const.mk (DStd.Path.local s) id_ty + |> Id.of_term_cst ~defined + | Hstring { ns; _ } -> + Id.of_string ~ns s + in let tmp = neg (mk_forall nm loc binders trs (neg f) ~toplevel:false ~decl_kind) in @@ -2838,7 +2847,7 @@ type gformula = { trigger_depth : int; age: int; lem: expr option; - origin_name : string; + origin_name : Id.t; from_terms : expr list; mf: bool; gf: bool; @@ -2850,14 +2859,14 @@ type gformula = { type th_elt = { th_name : string; - ax_name : string; + ax_name : Id.t; ax_form : t; extends : Util.theories_extensions; axiom_kind : Util.axiom_kind; } let print_th_elt fmt t = - Format.fprintf fmt "%s/%s: @[%a@]" t.th_name t.ax_name print t.ax_form + Format.fprintf fmt "%s/%a: @[%a@]" t.th_name Id.pp t.ax_name print t.ax_form let save_cache () = HC.save_cache () diff --git a/src/lib/structures/expr.mli b/src/lib/structures/expr.mli index bb04604491..3b91f574fd 100644 --- a/src/lib/structures/expr.mli +++ b/src/lib/structures/expr.mli @@ -65,7 +65,7 @@ and bind_kind = | B_let of letin and quantified = private { - name : string; + name : Id.t; (** Name of the lemma. This field is used by printers. *) main : t; @@ -237,8 +237,8 @@ val symbol_info : t -> Symbols.t val add_label : Hstring.t -> t -> unit val label : t -> Hstring.t -val name_of_lemma : t -> string -val name_of_lemma_opt : t option -> string +val name_of_lemma : t -> Id.t +val name_of_lemma_opt : t option -> Id.t val print_tagged_classes : Format.formatter -> Set.t list -> unit @@ -370,14 +370,14 @@ val make_triggers: The matching environment [env] is used to limit the number of multi-triggers generated per axiom. *) -val clean_trigger: in_theory:bool -> string -> trigger -> trigger +val clean_trigger: in_theory:bool -> Id.t -> trigger -> trigger (** clean trigger: remove useless terms in multi-triggers after inlining of lets*) val resolution_triggers: is_back:bool -> quantified -> trigger list val mk_forall : - string -> (* name *) + Id.t -> (* name *) Loc.t -> (* location in the original file *) binders -> (* quantified variables *) trigger list -> (* triggers *) @@ -387,7 +387,7 @@ val mk_forall : t val mk_exists : - string -> (* name *) + Id.t -> (* name *) Loc.t -> (* location in the original file *) binders -> (* quantified variables *) trigger list -> (* triggers *) @@ -415,7 +415,7 @@ type gformula = { trigger_depth : int; age: int; lem: t option; - origin_name : string; + origin_name : Id.t; from_terms : t list; mf: bool; gf: bool; @@ -427,7 +427,7 @@ type gformula = { type th_elt = { th_name : string; - ax_name : string; + ax_name : Id.t; ax_form : t; extends : Util.theories_extensions; axiom_kind : Util.axiom_kind; diff --git a/src/lib/structures/id.ml b/src/lib/structures/id.ml index e1933ef937..c030b3998b 100644 --- a/src/lib/structures/id.ml +++ b/src/lib/structures/id.ml @@ -40,11 +40,6 @@ type t = | Term_cst of { tcst : Dolmen.Std.Expr.term_cst; defined : bool } | Hstring of { hs : Hstring.t; ns : name_space } -type typed = Dolmen.Std.Expr.term_cst * Ty.t list * Ty.t - -let compare_typed (t1, _, _) (t2, _, _) = - Dolmen.Std.Expr.Term.Const.compare t1 t2 - let mangle ns s = match ns with | Internal -> ".!" ^ s @@ -144,6 +139,11 @@ let reinit () = Skolem.reset_fresh_cpt (); Abstract.reset_fresh_cpt () +module Set = Set.Make (struct + type nonrec t = t + let compare = compare + end) + module Map = Map.Make (struct type nonrec t = t let compare = compare diff --git a/src/lib/structures/id.mli b/src/lib/structures/id.mli index 437f4928ba..c00a08ca23 100644 --- a/src/lib/structures/id.mli +++ b/src/lib/structures/id.mli @@ -77,10 +77,6 @@ type t = private | Hstring of { hs : Hstring.t; ns : name_space } -(* TODO: remove this type after replacing Alt-Ergo types by Dolmen types. *) -type typed = Dolmen.Std.Expr.term_cst * Ty.t list * Ty.t -val compare_typed : typed -> typed -> int - val of_term_cst : ?defined:bool -> Dolmen.Std.Expr.term_cst -> t (** [of_term_cst ?defined t] creates an identifier from a constant term. The argument [defined] is used to determine if the identifier is @@ -127,4 +123,5 @@ val is_suspicious : t -> bool val reinit : unit -> unit (** Resets the internal counters of the [fresh] function. *) +module Set : Set.S with type elt = t module Map : Map.S with type key = t diff --git a/src/lib/structures/modelMap.ml b/src/lib/structures/modelMap.ml index 015452e37b..408ffca14b 100644 --- a/src/lib/structures/modelMap.ml +++ b/src/lib/structures/modelMap.ml @@ -19,6 +19,8 @@ module X = Shostak.Combine module Sy = Symbols +type typed = Dolmen.Std.Expr.term_cst * Ty.t list * Ty.t + module M: Map.S with type key = Expr.t list = Map.Make (struct type t = Expr.t list [@@deriving ord] @@ -107,9 +109,10 @@ end module P = Map.Make (struct - type t = Id.typed + type t = typed - let compare = Id.compare_typed + let compare (t1, _, _) (t2, _, _) = + Dolmen.Std.Expr.Term.Const.compare t1 t2 end) type graph = diff --git a/src/lib/structures/modelMap.mli b/src/lib/structures/modelMap.mli index 0f0f6fd127..f9347e3da7 100644 --- a/src/lib/structures/modelMap.mli +++ b/src/lib/structures/modelMap.mli @@ -28,22 +28,25 @@ type graph = type t (** Type of model. *) -val add : Id.typed -> Expr.t list -> Expr.t -> t -> t +(* TODO: remove this type after replacing Alt-Ergo types by Dolmen types. *) +type typed = Dolmen.Std.Expr.term_cst * Ty.t list * Ty.t + +val add : typed -> Expr.t list -> Expr.t -> t -> t (** [add id args ret mdl] adds the binding [args -> ret] to the partial graph associated with the identifier [id]. *) -val empty : suspicious:bool -> Id.typed list -> t +val empty : suspicious:bool -> typed list -> t (** An empty model. The [suspicious] flag is used to remember that this model may be wrong as it involves symbols from theories for which the model generation is known to be incomplete. *) -val find : Id.typed -> t -> graph +val find : typed -> t -> graph (** [find id mdl] returns the graph associated with the identifier [id] in the model [mdl]. @raise Not_found if it does not exist. *) -val fold: (Id.typed -> graph -> 'a -> 'a) -> t -> 'a -> 'a +val fold: (typed -> graph -> 'a -> 'a) -> t -> 'a -> 'a (** [fold f mdl init] folds over the bindings in the model [mdl] with the function [f] and with [init] as a initial value for the accumulator. *) diff --git a/src/lib/util/printer.ml b/src/lib/util/printer.ml index 6386b193df..09b42fea49 100644 --- a/src/lib/util/printer.ml +++ b/src/lib/util/printer.ml @@ -304,7 +304,7 @@ let status_steps s = let status_goal g = match g with None -> "" - | Some g -> Format.sprintf " (goal %s)" g + | Some g -> Format.asprintf " (goal %a)" Id.pp g let print_status_loc fmt loc = match loc with diff --git a/src/lib/util/printer.mli b/src/lib/util/printer.mli index 98d1501e3e..7756db81f2 100644 --- a/src/lib/util/printer.mli +++ b/src/lib/util/printer.mli @@ -107,7 +107,7 @@ val print_status_unsat : Loc.t option -> float option -> int option -> - string option -> unit + Id.t option -> unit (** Print sat status message from the frontend on the standard output. If validity_mode is set, the status print : @@ -120,7 +120,7 @@ val print_status_sat : Loc.t option -> float option -> int option -> - string option -> unit + Id.t option -> unit (** Print unknown status message from the frontend on the standard output. If validity_mode is set, the status print : @@ -133,7 +133,7 @@ val print_status_unknown : Loc.t option -> float option -> int option -> - string option -> unit + Id.t option -> unit (** Print timeout status message from the frontend on the standard output. If validity_mode is set, the status print : @@ -146,7 +146,7 @@ val print_status_timeout : Loc.t option -> float option -> int option -> - string option -> unit + Id.t option -> unit (** Print inconsistent status message from the frontend on the standard output. If validity_mode is set, the status print : @@ -159,7 +159,7 @@ val print_status_inconsistent : Loc.t option -> float option -> int option -> - string option -> unit + Id.t option -> unit (** Print preprocess status message from the frontend on the standard output. If validity_mode is set, the status print : From 0763d0e7c7cf29a38a48357955029bece950449f Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Mon, 3 Feb 2025 13:18:58 +0100 Subject: [PATCH 3/7] Lemma names are defined identifier --- src/lib/frontend/translate.ml | 13 +++++-------- src/lib/reasoners/instances.ml | 17 ++++++++++++++++- src/lib/structures/id.ml | 4 ++++ tests/everything/predicate_name.ae | 3 +++ tests/everything/predicate_name.expected | 2 ++ 5 files changed, 30 insertions(+), 9 deletions(-) create mode 100755 tests/everything/predicate_name.ae create mode 100644 tests/everything/predicate_name.expected diff --git a/src/lib/frontend/translate.ml b/src/lib/frontend/translate.ml index 6e1f506fc7..2a723fc630 100644 --- a/src/lib/frontend/translate.ml +++ b/src/lib/frontend/translate.ml @@ -977,7 +977,6 @@ let mk_rounding fpar = let rec mk_expr ?(loc = Loc.dummy) ~name ?(toplevel = false) ~decl_kind dt = - let name_tag = ref 0 in let rec aux_mk_expr ?(toplevel = false) (DE.{ term_descr; term_ty; term_tags = root_tags; _ } as term) = let mk = aux_mk_expr in @@ -1511,7 +1510,7 @@ let rec mk_expr List.map ( fun t -> make_trigger ~loc ~name ~decl_kind ~in_theory - name hyp (t, true) + hyp (t, true) ) trgs in @@ -1607,8 +1606,8 @@ let rec mk_expr in aux_mk_expr ~toplevel dt -and make_trigger ?(loc = Loc.dummy) ~name ~decl_kind - ~(in_theory: bool) (name: Id.t) (hyp: E.t list) +and make_trigger ?(loc = Loc.dummy) ~(name : Id.t) ~decl_kind + ~(in_theory: bool) (hyp: E.t list) (e, from_user: DE.term * bool) = (* Dolmen adds an existential quantifier to bind the '?xxx' variables *) let e = @@ -1632,9 +1631,7 @@ and make_trigger ?(loc = Loc.dummy) ~name ~decl_kind -> es | e -> [e] in - let mk_expr = - mk_expr ~loc ~name ~decl_kind - in + let mk_expr = mk_expr ~loc ~name ~decl_kind in let content = List.map mk_expr e in (* clean trigger: remove useless terms in multi-triggers after inlining of lets*) @@ -1948,7 +1945,7 @@ let make dloc_file acc stmt = | `Term_def ( _, ({ tags; _ } as tcst), tyvars, terml, body) -> Cache.store_tyvl tyvars; let st_loc = dl_to_ael dloc_file loc in - let name = Id.of_term_cst tcst in + let name = Id.of_term_cst ~defined:true tcst in let binders, defn = let rty = dty_to_ty body.term_ty in diff --git a/src/lib/reasoners/instances.ml b/src/lib/reasoners/instances.ml index 384f8bea16..c7fb7c49b3 100644 --- a/src/lib/reasoners/instances.ml +++ b/src/lib/reasoners/instances.ml @@ -184,7 +184,22 @@ module Make(X : Theory.S) : S with type tbox = X.t = struct let defn = if E.equal p f then E.vrai else if E.equal np f then E.faux - else assert false + else ( + Fmt.pr "p = %a, np = %a, f = %a@." + E.print p E.print np E.print f; + let () = + let E.{ f = nff; _ } = E.term_view (E.neg np) in + let E.{ f = ff; _ } = E.term_view (E.neg f) in + let module Sy = Symbols in + match nff, ff with + | Sy.Name { id = Id.Term_cst { tcst = _; defined = d1 }; _ }, + Sy.Name { id = Id.Term_cst { tcst = _; defined = d2 }; _ } -> + if Stdlib.(d1 != d2) then assert false + else () + | Sy.Name { id = Id.Hstring _; _ }, Sy.Name { id = Id.Hstring _; _ } -> () + | _ -> assert false + in + assert false) in add_ground_pred env ~guard p np defn ex diff --git a/src/lib/structures/id.ml b/src/lib/structures/id.ml index c030b3998b..92fead0229 100644 --- a/src/lib/structures/id.ml +++ b/src/lib/structures/id.ml @@ -63,6 +63,10 @@ let of_term_cst ?(defined = false) tcst = Term_cst { tcst; defined } let of_string ~ns s = + let () = + if String.equal s "P_F" then assert false + else () + in let () = match ns with | Fresh | Fresh_ac | Abstract -> invalid_arg "of_string" diff --git a/tests/everything/predicate_name.ae b/tests/everything/predicate_name.ae new file mode 100755 index 0000000000..8ef35426e9 --- /dev/null +++ b/tests/everything/predicate_name.ae @@ -0,0 +1,3 @@ +predicate P1 () = false +logic P2 : prop +goal g: P1 -> P2 diff --git a/tests/everything/predicate_name.expected b/tests/everything/predicate_name.expected new file mode 100644 index 0000000000..6f99ff0f44 --- /dev/null +++ b/tests/everything/predicate_name.expected @@ -0,0 +1,2 @@ + +unsat From ec6cf3f3f07d83bd267a2d94ef4cac57272ed203 Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Mon, 3 Feb 2025 13:38:29 +0100 Subject: [PATCH 4/7] Remove assertion --- src/lib/reasoners/instances.ml | 17 +---------------- 1 file changed, 1 insertion(+), 16 deletions(-) diff --git a/src/lib/reasoners/instances.ml b/src/lib/reasoners/instances.ml index c7fb7c49b3..384f8bea16 100644 --- a/src/lib/reasoners/instances.ml +++ b/src/lib/reasoners/instances.ml @@ -184,22 +184,7 @@ module Make(X : Theory.S) : S with type tbox = X.t = struct let defn = if E.equal p f then E.vrai else if E.equal np f then E.faux - else ( - Fmt.pr "p = %a, np = %a, f = %a@." - E.print p E.print np E.print f; - let () = - let E.{ f = nff; _ } = E.term_view (E.neg np) in - let E.{ f = ff; _ } = E.term_view (E.neg f) in - let module Sy = Symbols in - match nff, ff with - | Sy.Name { id = Id.Term_cst { tcst = _; defined = d1 }; _ }, - Sy.Name { id = Id.Term_cst { tcst = _; defined = d2 }; _ } -> - if Stdlib.(d1 != d2) then assert false - else () - | Sy.Name { id = Id.Hstring _; _ }, Sy.Name { id = Id.Hstring _; _ } -> () - | _ -> assert false - in - assert false) + else assert false in add_ground_pred env ~guard p np defn ex From e753a09393c678f1dfa6b1a3ace525df634eba89 Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Mon, 3 Feb 2025 13:39:30 +0100 Subject: [PATCH 5/7] Too long lines --- src/lib/structures/expr.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/lib/structures/expr.ml b/src/lib/structures/expr.ml index 09c62b9bc3..4400e4c861 100644 --- a/src/lib/structures/expr.ml +++ b/src/lib/structures/expr.ml @@ -2865,8 +2865,8 @@ type th_elt = axiom_kind : Util.axiom_kind; } -let print_th_elt fmt t = - Format.fprintf fmt "%s/%a: @[%a@]" t.th_name Id.pp t.ax_name print t.ax_form +let print_th_elt ppf t = + Fmt.pf ppf "%s/%a: @[%a@]" t.th_name Id.pp t.ax_name print t.ax_form let save_cache () = HC.save_cache () From 32a687fc0fd2a9d7dce665f38ff60dafd4fa1bbc Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Mon, 3 Feb 2025 15:13:38 +0100 Subject: [PATCH 6/7] Fresh skolem names must be fresh... of course! --- src/lib/structures/symbols.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/lib/structures/symbols.ml b/src/lib/structures/symbols.ml index ad48a3ba21..bbedf54870 100644 --- a/src/lib/structures/symbols.ml +++ b/src/lib/structures/symbols.ml @@ -479,7 +479,7 @@ let to_string_clean sy = let to_string sy = Fmt.str "%a" (AEPrinter.pp ~show_vars:true) sy -let fresh_skolem_name base = name @@ Id.of_string ~ns:Skolem base +let fresh_skolem_name base = name @@ Id.fresh ~base ~ns:Skolem () let fresh_skolem_var base = Var.of_id @@ Id.fresh ~base ~ns:Skolem () From 7c04389f7222b098530e31e737563e07475387df Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Tue, 4 Feb 2025 18:03:19 +0100 Subject: [PATCH 7/7] Try to avoid collision in Id.hash --- src/lib/structures/id.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/lib/structures/id.ml b/src/lib/structures/id.ml index 92fead0229..b14e5999d3 100644 --- a/src/lib/structures/id.ml +++ b/src/lib/structures/id.ml @@ -114,11 +114,11 @@ let equal i1 i2 = let hash i = match i with | Term_cst { tcst; _ } -> - Dolmen.Std.Expr.Term.Const.hash tcst + 2 * (Dolmen.Std.Expr.Term.Const.hash tcst) | Hstring { hs; _ } -> (* NB: Internal identifiers are pre-mangled, which means that we do not need to take the name space into consideration when hashing. *) - Hstring.hash hs + 2 * (Hstring.hash hs) + 1 let pp ppf i = match i with