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/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/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..2a723fc630 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 *) @@ -991,9 +975,8 @@ 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) (DE.{ term_descr; term_ty; term_tags = root_tags; _ } as term) = let mk = aux_mk_expr in @@ -1439,9 +1422,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 @@ -1474,20 +1456,22 @@ 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 *) (* 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 @@ -1525,8 +1509,8 @@ let rec mk_expr let triggers = List.map ( fun t -> - make_trigger ~loc ~name_base ~decl_kind ~in_theory - name hyp (t, true) + make_trigger ~loc ~name ~decl_kind ~in_theory + hyp (t, true) ) trgs in @@ -1536,7 +1520,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 @@ -1622,8 +1606,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 : 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 = @@ -1631,11 +1615,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 @@ -1651,9 +1631,7 @@ and make_trigger ?(loc = Loc.dummy) ~name_base ~decl_kind -> es | e -> [e] in - let mk_expr = - mk_expr ~loc ~name_base ~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*) @@ -1743,15 +1721,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. *) @@ -1768,8 +1743,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 @@ -1797,15 +1773,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 @@ -1832,7 +1808,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 @@ -1846,11 +1824,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 @@ -1950,9 +1928,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 _ -> @@ -1965,18 +1942,18 @@ 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 = get_basename path in + let name = Id.of_term_cst ~defined:true tcst 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 @@ -1994,12 +1971,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)); @@ -2007,20 +1984,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)); @@ -2028,12 +2005,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/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..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 @@ -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/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 347ef6cc48..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 @@ -1875,8 +1883,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 +1895,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/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 6f9f7af11d..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 @@ -168,7 +168,7 @@ 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) -> + | E.Iff (f1, f2) -> let p = E.mk_term (Symbols.name name) [] Ty.Tbool in let np = E.neg p in let defn = @@ -224,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 @@ -242,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 5e037b74ad..e753cb8066 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 @@ -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 c0b448983c..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; @@ -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..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 @@ -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/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.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/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/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..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 @@ -46,19 +46,19 @@ 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 | 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 43f4264d57..4400e4c861 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; @@ -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) @@ -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 @@ -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 @@ -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)" @@ -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 @@ -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 @@ -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 @@ -1144,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 ?? *) @@ -1814,7 +1818,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 @@ -2360,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; } @@ -2607,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 @@ -2835,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; @@ -2847,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 +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 () 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 b8666d20a0..b14e5999d3 100644 --- a/src/lib/structures/id.ml +++ b/src/lib/structures/id.ml @@ -16,45 +16,139 @@ (* *) (**************************************************************************) -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 +let mangle ns s = + match ns with + | Internal -> ".!" ^ s + | Fresh -> ".k" ^ s + | Fresh_ac -> ".K" ^ s + | Skolem -> ".?__" ^ s + | Abstract -> "@a" ^ s -module Namespace = struct - module type S = sig - val fresh : ?base:string -> unit -> string - end +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 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 + 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 Internal = Make () +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" + | _ -> () + in + let hs = Hstring.make (mangle ns s) in + Hstring { hs; ns } - module Skolem = Make () +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 } - module Abstract = Make () +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 - let reinit () = - Internal.reset_fresh_cpt (); - Skolem.reset_fresh_cpt (); - Abstract.reset_fresh_cpt () -end + | 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; _ } -> + 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. *) + 2 * (Hstring.hash hs) + 1 + +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 Set = Set.Make (struct + type nonrec t = t + let compare = compare + end) + +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..c00a08ca23 100644 --- a/src/lib/structures/id.mli +++ b/src/lib/structures/id.mli @@ -16,29 +16,112 @@ (* *) (**************************************************************************) -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 } + +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 compare_typed : typed -> typed -> int 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 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 47df05ccbe..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 = @@ -127,7 +130,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 +160,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 +191,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..f9347e3da7 100644 --- a/src/lib/structures/modelMap.mli +++ b/src/lib/structures/modelMap.mli @@ -28,20 +28,25 @@ type graph = 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]. *) +(* 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 empty : suspicious:bool -> Id.typed list -> 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 -> 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 -(** [find sy mdl] returns the graph associated with the symbol [sy] in the model - [mdl], raises [Not_found] if it doesn't exist. *) +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/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..bbedf54870 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.fresh ~base ~ns:Skolem () + +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/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 : 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/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 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)) )