diff --git a/alt-ergo-lib.opam b/alt-ergo-lib.opam index b4e86e7ca..89b163266 100644 --- a/alt-ergo-lib.opam +++ b/alt-ergo-lib.opam @@ -26,6 +26,7 @@ depends: [ "fmt" {>= "0.9.0"} "stdlib-shims" "ppx_blob" {>= "0.7.2"} + "ppx_deriving" "camlzip" {>= "1.07"} "odoc" {with-doc} "ppx_deriving" diff --git a/dune-project b/dune-project index cab2fcd37..2b6de3b71 100644 --- a/dune-project +++ b/dune-project @@ -86,6 +86,7 @@ See more details on http://alt-ergo.ocamlpro.com/" (fmt (>= 0.9.0)) stdlib-shims (ppx_blob (>= 0.7.2)) + ppx_deriving (camlzip (>= 1.07)) (odoc :with-doc) ppx_deriving diff --git a/src/bin/common/solving_loop.ml b/src/bin/common/solving_loop.ml index 746e17dcc..33e996d1c 100644 --- a/src/bin/common/solving_loop.ml +++ b/src/bin/common/solving_loop.ml @@ -181,7 +181,8 @@ let main () = begin let mdl = Model ((module SAT), partial_model) in if Options.(get_interpretation () && get_dump_models ()) then begin - FE.print_model (Options.Output.get_fmt_models ()) partial_model + Fmt.pf (Options.Output.get_fmt_models ()) "%a@." + FE.print_model partial_model end; Sat mdl end @@ -193,7 +194,8 @@ let main () = Printer.print_fmt (Options.Output.get_fmt_diagnostic ()) "@[Returned unknown reason = %a@]" Sat_solver_sig.pp_ae_unknown_reason_opt ur; - FE.print_model (Options.Output.get_fmt_models ()) partial_model + Fmt.pf (Options.Output.get_fmt_models ()) "%a@." + FE.print_model partial_model end; Unknown (Some mdl) end @@ -927,7 +929,8 @@ let main () = let () = match State.get partial_model_key st with | Some (Model ((module SAT), env)) -> let module FE = Frontend.Make (SAT) in - FE.print_model (Options.Output.get_fmt_regular ()) env + Fmt.pf (Options.Output.get_fmt_regular ()) "%a@." + FE.print_model env | None -> (* TODO: add the location of the statement. *) recoverable_error "No model produced." diff --git a/src/lib/dune b/src/lib/dune index 7bada9b61..1d59f6223 100644 --- a/src/lib/dune +++ b/src/lib/dune @@ -55,7 +55,7 @@ ; structures Commands Errors Explanation Fpa_rounding Parsed Profiling Satml_types Symbols - Expr Var Ty Typed Xliteral ModelMap Objective + Expr Var Ty Typed Xliteral ModelMap Id Objective ; util Emap Gc_debug Hconsing Hstring Heap Lists Loc MyUnix Numbers diff --git a/src/lib/frontend/d_cnf.ml b/src/lib/frontend/d_cnf.ml index 1ba519ec4..c7545a8ee 100644 --- a/src/lib/frontend/d_cnf.ml +++ b/src/lib/frontend/d_cnf.ml @@ -39,7 +39,6 @@ module SM = Sy.Map module DE = DStd.Expr module DT = DE.Ty -module Id = DStd.Id module B = DStd.Builtin let unsupported msg = @@ -194,7 +193,7 @@ let builtin_term t = Dl.Typer.T.builtin_term t let builtin_ty t = Dl.Typer.T.builtin_ty t let ty name ty = - Id.Map.add { name = DStd.Name.simple name; ns = Sort } @@ + DStd.Id.Map.add { name = DStd.Name.simple name; ns = Sort } @@ fun env s -> builtin_ty @@ Dolmen_type.Base.app0 (module Dl.Typer.T) env s ty @@ -214,10 +213,11 @@ let builtin_enum = function let add_cstrs map = List.fold_left (fun map ((c : DE.term_cst), _) -> let name = get_basename c.path in - Id.Map.add { name = DStd.Name.simple name; ns = Term } (fun env _ -> - builtin_term @@ - Dolmen_type.Base.term_app_cst - (module Dl.Typer.T) env c) map) + DStd.Id.Map.add { name = DStd.Name.simple name; ns = Term } + (fun env _ -> + builtin_term @@ + Dolmen_type.Base.term_app_cst + (module Dl.Typer.T) env c) map) map cstrs in Cache.store_ty (DE.Ty.Const.hash ty_cst) ty_; @@ -238,19 +238,19 @@ module Const = struct let bv2nat = with_cache (fun n -> let name = "bv2nat" in - Id.mk ~name ~builtin:(BV2Nat n) + DE.Id.mk ~name ~builtin:(BV2Nat n) (DStd.Path.global name) Ty.(arrow [bitv n] int)) let int2bv = with_cache (fun n -> let name = "int2bv" in - Id.mk ~name ~builtin:(Int2BV n) + DE.Id.mk ~name ~builtin:(Int2BV n) (DStd.Path.global name) Ty.(arrow [int] (bitv n))) let smt_round = with_cache (fun (n, m) -> let name = "ae.round" in - Id.mk + DE.Id.mk ~name ~builtin:(AERound (n, m)) (DStd.Path.global name) @@ -299,7 +299,7 @@ let bv_builtins env s = equivalent *) let inject_ae_to_smt2 id = match id with - | Id.{name = Simple n; _} -> + | DStd.Id.{name = Simple n; _} -> begin if String.equal n Fpa_rounding.fpa_rounding_mode_ae_type_name then (* Injecting the type name as the SMT2 Type name. *) @@ -322,7 +322,7 @@ let inject_ae_to_smt2 id = let ae_fpa_builtins = let (->.) args ret = (args, ret) in let dterm name f = - Id.Map.add { name = DStd.Name.simple name; ns = Term } @@ + DStd.Id.Map.add { name = DStd.Name.simple name; ns = Term } @@ fun env s -> builtin_term @@ Dolmen_type.Base.term_app1 (module Dl.Typer.T) env s f @@ -330,7 +330,7 @@ let ae_fpa_builtins = let op ?(tyvars = []) name builtin (args, ret) = let ty = DT.pi tyvars @@ DT.arrow args ret in let cst = DE.Id.mk ~name ~builtin (DStd.Path.global name) ty in - Id.Map.add { name = DStd.Name.simple name; ns = Term } @@ + DStd.Id.Map.add { name = DStd.Name.simple name; ns = Term } @@ fun env _ -> builtin_term @@ Dolmen_type.Base.term_app_cst @@ -358,13 +358,13 @@ let ae_fpa_builtins = let float64 = float (DE.Term.int "53") (DE.Term.int "1074") in let float64d x = float64 (mode "NearestTiesToEven") x in let partial1 name f = - Id.Map.add { name = DStd.Name.simple name; ns = Term } @@ + DStd.Id.Map.add { name = DStd.Name.simple name; ns = Term } @@ fun env s -> builtin_term @@ Dolmen_type.Base.term_app1 (module Dl.Typer.T) env s f in let partial2 name f = - Id.Map.add { name = DStd.Name.simple name; ns = Term } @@ + DStd.Id.Map.add { name = DStd.Name.simple name; ns = Term } @@ fun env s -> builtin_term @@ Dolmen_type.Base.term_app2 (module Dl.Typer.T) env s f @@ -380,7 +380,7 @@ let ae_fpa_builtins = in let fpa_builtins = let open DT in - Id.Map.empty + DStd.Id.Map.empty |> add_rounding_modes @@ -454,7 +454,7 @@ let ae_fpa_builtins = fun env s -> let search_id id = try - Id.Map.find_exn id fpa_builtins env s + DStd.Id.Map.find_exn id fpa_builtins env s with Not_found -> `Not_found in match s with @@ -469,7 +469,7 @@ let smt_fpa_builtins = Dolmen_type.Base.term_app2 (module Dl.Typer.T) env s f in let other_builtins = - Id.Map.empty + DStd.Id.Map.empty |> add_rounding_modes in fun env s -> @@ -487,7 +487,7 @@ let smt_fpa_builtins = | exception Failure _ -> `Not_found end | Dl.Typer.T.Id id -> begin - match Id.Map.find_exn id other_builtins env s with + match DStd.Id.Map.find_exn id other_builtins env s with | e -> e | exception Not_found -> `Not_found end @@ -1876,7 +1876,7 @@ let make dloc_file acc stmt = let ns = DStd.Namespace.Decl in let name = Ty.fresh_hypothesis_name goal_sort in let decl: _ Typer_Pipe.stmt = { - id = Id.mk ns name; + id = DStd.Id.mk ns name; contents = `Hyp t; loc; attrs; implicit } in @@ -1893,7 +1893,7 @@ let make dloc_file acc stmt = assert false (* Axiom definitions *) - | { id = Id.{name = Simple name; _}; contents = `Hyp t; loc; attrs; + | { id = DStd.Id.{name = Simple name; _}; contents = `Hyp t; loc; attrs; implicit=_ } -> let dloc = DStd.Loc.(loc dloc_file stmt.loc) in let aloc = DStd.Loc.lexing_positions dloc in diff --git a/src/lib/frontend/frontend.ml b/src/lib/frontend/frontend.ml index c18df4c21..10808c3cf 100644 --- a/src/lib/frontend/frontend.ml +++ b/src/lib/frontend/frontend.ml @@ -520,5 +520,5 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct Sat_solver_sig.pp_ae_unknown_reason_opt ur; | Some model -> - Models.output_concrete_model ppf model + Models.pp ppf model end diff --git a/src/lib/frontend/models.ml b/src/lib/frontend/models.ml index 7a962267a..457475278 100644 --- a/src/lib/frontend/models.ml +++ b/src/lib/frontend/models.ml @@ -28,53 +28,39 @@ (* *) (**************************************************************************) -open Format -open Options - -module X = Shostak.Combine - -module Ac = Shostak.Ac -module Ex = Explanation - module Sy = Symbols +module X = Shostak.Combine module E = Expr -module ME = Expr.Map -module SE = Expr.Set module MS = Map.Make(String) -module MX = Shostak.MXH let constraints = ref MS.empty type t = { propositional : Expr.Set.t; - constants : ModelMap.t; - functions : ModelMap.t; - arrays : ModelMap.t; - terms_values : (Shostak.Combine.r * string) Expr.Map.t + model : ModelMap.t; + term_values : Expr.t Expr.Map.t } let empty = { propositional = Expr.Set.empty; - constants = ModelMap.empty; - functions = ModelMap.empty; - arrays = ModelMap.empty; - terms_values = Expr.Map.empty; + model = ModelMap.empty ~suspicious:false; + term_values = Expr.Map.empty; } module Pp_smtlib_term = struct - + open Format let to_string_type t = asprintf "%a" Ty.pp_smtlib t let rec print fmt t = - let {E.f;xs;ty; _} = E.term_view t in + let {Expr.f;xs;ty; _} = Expr.term_view t in match f, xs with | Sy.Lit lit, xs -> begin match lit, xs with | Sy.L_eq, a::l -> - if get_output_smtlib () then + if Options.get_output_smtlib () then fprintf fmt "(= %a%a)" print a (fun fmt -> List.iter (fprintf fmt " %a" print)) l else @@ -82,13 +68,13 @@ module Pp_smtlib_term = struct print a (fun fmt -> List.iter (fprintf fmt " = %a" print)) l | Sy.L_neg_eq, [a; b] -> - if get_output_smtlib () then + if Options.get_output_smtlib () then fprintf fmt "(not (= %a %a))" print a print b else fprintf fmt "(%a <> %a)" print a print b | Sy.L_neg_eq, a::l -> - if get_output_smtlib () then + if Options.get_output_smtlib () then fprintf fmt "(distinct %a%a)" print a (fun fmt -> List.iter (fprintf fmt " %a" print)) l else @@ -96,25 +82,25 @@ module Pp_smtlib_term = struct print a (fun fmt -> List.iter (fprintf fmt ", %a" print)) l | Sy.L_built Sy.LE, [a;b] -> - if get_output_smtlib () then + if Options.get_output_smtlib () then fprintf fmt "(<= %a %a)" print a print b else fprintf fmt "(%a <= %a)" print a print b | Sy.L_built Sy.LT, [a;b] -> - if get_output_smtlib () then + if Options.get_output_smtlib () then fprintf fmt "(< %a %a)" print a print b else fprintf fmt "(%a < %a)" print a print b | Sy.L_neg_built Sy.LE, [a; b] -> - if get_output_smtlib () then + if Options.get_output_smtlib () then fprintf fmt "(> %a %a)" print a print b else fprintf fmt "(%a > %a)" print a print b | Sy.L_neg_built Sy.LT, [a; b] -> - if get_output_smtlib () then + if Options.get_output_smtlib () then fprintf fmt "(>= %a %a)" print a print b else fprintf fmt "(%a >= %a)" print a print b @@ -123,13 +109,13 @@ module Pp_smtlib_term = struct fprintf fmt "(not %a)" print a | Sy.L_built (Sy.IsConstr hs), [e] -> - if get_output_smtlib () then + if Options.get_output_smtlib () then fprintf fmt "((_ is %a) %a)" Hstring.print hs print e else fprintf fmt "(%a ? %a)" print e Hstring.print hs | Sy.L_neg_built (Sy.IsConstr hs), [e] -> - if get_output_smtlib () then + if Options.get_output_smtlib () then fprintf fmt "(not ((_ is %a) %a))" Hstring.print hs print e else fprintf fmt "not (%a ? %a)" print e Hstring.print hs @@ -143,13 +129,13 @@ module Pp_smtlib_term = struct end | Sy.Op Sy.Get, [e1; e2] -> - if get_output_smtlib () then + if Options.get_output_smtlib () then fprintf fmt "(select %a %a)" print e1 print e2 else fprintf fmt "%a[%a]" print e1 print e2 | Sy.Op Sy.Set, [e1; e2; e3] -> - if get_output_smtlib () then + if Options.get_output_smtlib () then fprintf fmt "(store %a %a %a)" print e1 print e2 @@ -164,7 +150,7 @@ module Pp_smtlib_term = struct fprintf fmt "%a^{%d,%d}" print e i j | Sy.Op (Sy.Access field), [e] -> - if get_output_smtlib () then + if Options.get_output_smtlib () then fprintf fmt "(%s %a)" (Hstring.view field) print e else fprintf fmt "%a.%s" print e (Hstring.view field) @@ -194,7 +180,7 @@ module Pp_smtlib_term = struct fprintf fmt "%a(%a)" Hstring.print hs print_list l | Sy.Op _, [e1; e2] -> - if get_output_smtlib () then + if Options.get_output_smtlib () then fprintf fmt "(%a %a %a)" Sy.print f print e1 print e2 else fprintf fmt "(%a %a %a)" print e1 Sy.print f print e2 @@ -231,7 +217,7 @@ module Pp_smtlib_term = struct fprintf fmt "%a" Sy.print f | _, _ -> - if get_output_smtlib () then + if Options.get_output_smtlib () then fprintf fmt "(%a %a)" Sy.print f print_list xs else fprintf fmt "%a(%a)" Sy.print f print_list xs @@ -245,221 +231,17 @@ module Pp_smtlib_term = struct end -module SmtlibCounterExample = struct - let fresh_counter = ref 0 - - let reset_counter () = fresh_counter := 0 - +module Why3CounterExample = struct let pp_term fmt t = if Options.get_output_format () == Why3 then Pp_smtlib_term.print fmt t else E.print fmt t - let pp_abstract_value_of_type ppf ty = - if not @@ Options.get_interpretation_use_underscore () then begin - Fmt.pf ppf "(as @@a%i %a)" !fresh_counter Ty.pp_smtlib ty; - incr fresh_counter - end - else - Fmt.pf ppf "_ " - - let add_records_destr records record_name destr_name rep = - let destrs = - try MS.find record_name records - with Not_found -> MS.empty - in - let destrs = - MS.add destr_name rep destrs in - MS.add record_name destrs records - - let mk_records_constr records record_name - { Ty.name = _n; record_constr = cstr; lbs = lbs; _} = - let find_destrs destr destrs = - try let rep = MS.find destr destrs in - Some rep - with Not_found -> None - in - - let print_destr fmt (destrs,lbs) = - List.iter (fun (destr, ty_destr) -> - let destr = Hstring.view destr in - match find_destrs destr destrs with - | None -> - pp_abstract_value_of_type fmt ty_destr - | Some rep -> fprintf fmt "%s " rep - ) lbs - in - let destrs = - try MS.find (Sy.to_string record_name) records - with Not_found -> MS.empty - in - asprintf "%s %a" - (Hstring.view cstr) - print_destr (destrs,lbs) - - let add_record_constr records record_name - { Ty.name = _n; record_constr = _cstr; lbs = lbs; _} xs_values = - List.fold_left2(fun records (destr,_) (rep,_) -> - add_records_destr - records - record_name - (Hstring.view destr) - (asprintf "%a" pp_term rep) - ) records lbs xs_values - - let check_records records xs_ty_named xs_values f ty rep = - match xs_ty_named with - | [Ty.Trecord _r, _arg] -> begin - match xs_values with - | [record_name,_] -> - (* HOTFIX: this fix is temporary. The current implementation of - model generation for records relies on string representants, - which means the printer for access symbols has to agree with - the name of the field in the type trecord. As the printer - [Symbols.print] will always output AE native format, this - doesn't agree when the output format is SMT-LIB. But the - printer of expression will output the right string if we don't - give the arguments of the field. - - Issue: https://github.com/OCamlPro/alt-ergo/issues/958 *) - let access = Fmt.str "%a" Expr.print (Expr.mk_term f [] ty) in - add_records_destr - records - (asprintf "%a" Expr.print record_name) - access - rep - | [] | _ -> records - end - | _ -> - match ty with - | Ty.Trecord r -> - add_record_constr records rep r xs_values - | _ -> records - - let print_fun_def fmt name args ty t = - let print_args fmt (ty,name) = - Format.fprintf fmt "(%s %a)" name Ty.pp_smtlib ty in - let defined_value = - try - let res,_,_ = (MS.find (Sy.to_string name) !constraints) in - dprintf "%s" res - with _ -> t - in - - Format.fprintf fmt - "@ (@[define-fun %a (%a) %a@ %t)@]" - Sy.print name - (Printer.pp_list_space (print_args)) args - Ty.pp_smtlib ty - defined_value - - let output_constants_counterexample pp fmt records = - ModelMap.iter - (fun (f, xs_ty, ty) st -> - assert (xs_ty == []); - match ModelMap.V.elements st with - | [[], rep] -> - let rep = - match ty with - | Ty.Trecord r -> - let constr = mk_records_constr records f r in - dprintf "(%s)" constr - | _ -> dprintf "%a" pp rep - in - - print_fun_def fmt f [] ty rep - | _ -> assert false) - - let output_functions_counterexample pp fmt records fprofs = - let records = ref records in - ModelMap.iter - (fun (f, xs_ty, ty) st -> - let xs_ty_named = List.mapi (fun i ty -> - ty,(sprintf "arg_%d" i) - ) xs_ty in - - let rep = - let representants = - ModelMap.V.fold (fun (xs_values,(rep,srep)) acc -> - assert ((List.length xs_ty_named) = (List.length xs_values)); - records := - check_records !records xs_ty_named xs_values f ty srep; - let reps = try MX.find rep acc |> snd with Not_found -> [] in - MX.add rep (srep, xs_values :: reps) acc - ) st MX.empty in - - let representants = MX.fold (fun rep (srep, xs_values_list) acc -> - ((rep, srep),xs_values_list) :: acc) representants [] in - - let rec mk_ite_and xs tys = - match xs, tys with - | [],[] -> assert false - | [_,rs],[_ty,name] -> - dprintf "(= %s %a)" name pp rs - | (_,rs) :: l1, (_ty,name) :: l2 -> - dprintf "(and (= %s %a) %t)" - name - pp rs - (mk_ite_and l1 l2) - | _, _ -> assert false - in - - let mk_ite_or l = - let pp_or_list fmt xs_values = - fprintf fmt "%t" (mk_ite_and xs_values xs_ty_named) - in - match l with - | [] -> assert false - | [xs_values] -> mk_ite_and xs_values xs_ty_named - | xs_values :: l -> - dprintf "(or %t %a)" - (mk_ite_and xs_values xs_ty_named) - (Printer.pp_list_space pp_or_list) l - in - - let rec reps_aux reps = - match reps with - | [] -> dprintf "%a" pp_abstract_value_of_type ty - | [srep,xs_values_list] -> - if Options.get_interpretation_use_underscore () then - dprintf "(@[ite %t@ %a@ %t)@]" - (mk_ite_or xs_values_list) - pp srep - (reps_aux []) - else - dprintf "%a" pp srep - | (srep,xs_values_list) :: l -> - dprintf "(@[ite %t@ %a@ %t)@]" - (mk_ite_or xs_values_list) - pp srep - (reps_aux l) - in - if List.length representants = 1 then - dprintf "%a" pp (fst (List.hd representants)) - else - reps_aux representants - in - (* Only print declared (but not defined!) function symbols -- note - that we still need to *handle* other symbols without printing them - because they could be record accessors that must be added to the - `records` reference *) - match f with - | Sy.Name { defined = false; _ } -> - print_fun_def fmt f xs_ty_named ty rep - | _ -> () - ) fprofs; - !records - -end -(* of module SmtlibCounterExample *) - -module Why3CounterExample = struct - let output_constraints fmt prop_model = - let assertions = SE.fold (fun e acc -> - (dprintf "%t(assert %a)@ " acc SmtlibCounterExample.pp_term e) - ) prop_model (dprintf "") in + let assertions = Expr.Set.fold (fun e acc -> + (Format.dprintf "%t(assert %a)@ " acc pp_term e) + ) prop_model (Format.dprintf "") in Format.fprintf fmt "@ ; constraints@ "; MS.iter (fun _ (name,ty,args_ty) -> match args_ty with @@ -478,109 +260,8 @@ module Why3CounterExample = struct end (* of module Why3CounterExample *) -(* The [value_defn] type is a mini-language of the expressions that can occur in - constant values. *) -type value_defn = - | Store of value_defn * value_defn * value_defn - (* An array store: [(store array key value)] *) - | Constant of Symbols.t * Ty.t - (* A constant of a given type. If the constant is defined in a model, it - must be resolved before being printed. *) - | Value of X.r * string - (* A leaf semantic value. This must be an actual value, i.e. it must not - contain any uninterpreted terms. *) - | Abstract of string - (* An unique abstract value *) - -let value (r, s) = - match X.term_extract r with - | Some t, _ -> - begin match E.term_view t with - | { f = Name _ as sy; _ } -> Constant (sy, X.type_info r) - | _ -> Value (r, s) - end - | _ -> - Value (r, s) - -let rec pp_value ppk ppf = function - | Store (a, k, v) -> - Format.fprintf ppf "(@[store@ %a@ %a %a)@]" - (pp_value ppk) a - (pp_value ppk) k - (pp_value ppk) v - | Constant (sy, t) -> ppk ppf (sy, t) - | Value (_, s) -> Format.pp_print_string ppf s - | Abstract s -> Format.pp_print_string ppf s - -let pp_constant ppf (_sy, t) = - Fmt.pf ppf "%a" SmtlibCounterExample.pp_abstract_value_of_type t - -let output_concrete_model fmt m = - SmtlibCounterExample.reset_counter (); - if ModelMap.(is_suspicious m.functions || is_suspicious m.constants - || is_suspicious m.arrays) then - Format.fprintf fmt "; This model is a best-effort. It includes symbols - for which model generation is known to be incomplete. @."; - - Format.fprintf fmt "@[("; +let pp ppf { model; propositional; _ } = if Options.get_model_type_constraints () then begin - Why3CounterExample.output_constraints fmt m.propositional + Why3CounterExample.output_constraints ppf propositional end; - - let values = Hashtbl.create 17 in - let find_or_add sy f = - try Hashtbl.find values sy - with Not_found -> - let value = f () in - Hashtbl.replace values sy value; - value - in - (* Add the constants *) - ModelMap.iter (fun (f, xs_ty, _) st -> - assert (Lists.is_empty xs_ty); - ModelMap.V.iter (fun (keys, (value_r, value_s)) -> - assert (Lists.is_empty keys); - Hashtbl.add values f (value (value_r, value_s)) - ) st - ) m.constants; - - (* Add the arrays values, when applicable *) - ModelMap.iter (fun (f, xs_ty, ty) st -> - let root = - try Hashtbl.find values f - with Not_found -> Constant (f, Tfarray (List.hd xs_ty, ty)) - in - Hashtbl.replace values f @@ - ModelMap.V.fold (fun (keys, rs) acc -> - Store (acc, value (snd (List.hd keys)), value rs)) st root - ) m.arrays; - - let pp_value = - pp_value (fun ppf (sy, ty) -> - let v = - find_or_add sy @@ fun () -> - (* NB: It is important that we call `pp_abstract_value_of_type` - immediately (not in a delayed fashion) so that we make sure that - the same abstract value will get printed each time. *) - Abstract ( - Fmt.to_to_string SmtlibCounterExample.pp_abstract_value_of_type ty) - in - pp_value pp_constant ppf v) - in - - let pp_x ppf xs = pp_value ppf (value xs) in - - (* Functions *) - let records = - SmtlibCounterExample.output_functions_counterexample - pp_x fmt MS.empty m.functions - in - - (* Constants *) - SmtlibCounterExample.output_constants_counterexample - pp_x fmt records m.constants; - - (* Arrays *) - (* SmtlibCounterExample.output_arrays_counterexample fmt m.arrays; *) - - Printer.print_fmt fmt "@]@,)" + ModelMap.pp ppf model diff --git a/src/lib/frontend/models.mli b/src/lib/frontend/models.mli index b83f19034..20c466cad 100644 --- a/src/lib/frontend/models.mli +++ b/src/lib/frontend/models.mli @@ -32,16 +32,11 @@ type t = { propositional : Expr.Set.t; - constants : ModelMap.t; - functions : ModelMap.t; - arrays : ModelMap.t; - terms_values : (Shostak.Combine.r * string) Expr.Map.t - (** A map from terms to their values in the model (as a - representative of type X.r and as a string. *) + model : ModelMap.t; + term_values : Expr.t Expr.Map.t + (** A map from terms to their values in the model. *) } val empty : t -val output_concrete_model : t Fmt.t -(** [output_concrete_model ppf mdl] prints the model [mdl] on - the formatter [ppf]. *) +val pp : t Fmt.t diff --git a/src/lib/frontend/typechecker.ml b/src/lib/frontend/typechecker.ml index 673373f3a..8a5003fe8 100644 --- a/src/lib/frontend/typechecker.ml +++ b/src/lib/frontend/typechecker.ml @@ -2165,7 +2165,7 @@ let axioms_of_rules loc name lf acc env = (fun acc f -> let name = Fmt.str "%s_%s" - (Symbols.fresh_internal_string ()) + (Id.Namespace.Internal.fresh ()) name in let td = {c = TAxiom(loc,name,Util.Default, f); annot = new_id () } in diff --git a/src/lib/reasoners/ac.ml b/src/lib/reasoners/ac.ml index dcdb35286..b5abbfdc8 100644 --- a/src/lib/reasoners/ac.ml +++ b/src/lib/reasoners/ac.ml @@ -325,7 +325,7 @@ module Make (X : Sig.X) = struct let module SX = Set.Make(struct type t=r let compare = X.hash_cmp end) in let exception Found of Expr.t in fun r distincts eq -> - if List.exists (fun (t,(_:r)) -> Expr.const_term t) eq then + if List.exists (fun (t,(_:r)) -> Expr.is_model_term t) eq then None else (*match X.ac_extract r with diff --git a/src/lib/reasoners/adt.ml b/src/lib/reasoners/adt.ml index 54cd9a464..ba39cbb43 100644 --- a/src/lib/reasoners/adt.ml +++ b/src/lib/reasoners/adt.ml @@ -412,9 +412,8 @@ module Shostak (X : ALIEN) = struct "[ADTs.models] assign_value currently not implemented"; raise (Util.Not_implemented "Models for ADTs") - let choose_adequate_model _ _ _ = + let to_model_term _r = Printer.print_err - "[ADTs.models] choose_adequate_model currently not implemented"; + "[ADTs.models] to_model_term currently not implemented"; raise (Util.Not_implemented "Models for ADTs") - end diff --git a/src/lib/reasoners/arith.ml b/src/lib/reasoners/arith.ml index 9fa3a8a2f..7aaf7f9bc 100644 --- a/src/lib/reasoners/arith.ml +++ b/src/lib/reasoners/arith.ml @@ -809,49 +809,11 @@ module Shostak cpt := Q.add Q.one (max_constant distincts !cpt); Some (term_of_cst (Q.to_string !cpt), true) - let pp_constant ppf r = + let to_model_term r = match P.is_const (embed r), X.type_info r with - | Some q, Ty.Tint -> - assert (Z.equal (Q.den q) Z.one); - let i = Q.num q in - if Z.sign i = -1 then - Fmt.pf ppf "(- %a)" Z.pp_print (Z.abs i) - else - Fmt.pf ppf "%a" Z.pp_print i - | Some q, Ty.Treal -> - if Z.equal (Q.den q) Z.one then - Fmt.pf ppf "%a.0" Z.pp_print (Q.num q) - else if Q.sign q = -1 then - Fmt.pf ppf "(/ (- %a) %a)" - Z.pp_print (Z.abs (Q.num q)) - Z.pp_print (Q.den q) - else - Fmt.pf ppf "(/ %a %a)" Z.pp_print (Q.num q) Z.pp_print (Q.den q) - | _ -> assert false - - let choose_adequate_model t r l = - if Options.get_debug_interpretation () then - Printer.print_dbg - ~module_name:"Arith" ~function_name:"choose_adequate_model" - "choose_adequate_model for %a" E.print t; - let l = List.filter (fun (_, r) -> P.is_const (embed r) != None) l in - let r = - match l with - | [] -> - (* We do this, because terms of some semantic values created - by CS are not created and added to UF *) - if (P.is_const (embed r) == None) then begin - Printer.print_dbg - ~module_name:"Arith" ~function_name:"choose_adequate_model" - "no adequate model found for %a" X.print r; - assert false - end; - r - - | (_,r)::l -> - List.iter (fun (_,x) -> assert (X.equal x r)) l; - r - in - r, Fmt.str "%a" pp_constant r - + | Some i, Ty.Tint -> + assert (Z.equal (Q.den i) Z.one); + Some (Expr.Ints.of_Z (Q.num i)) + | Some q, Ty.Treal -> Some (Expr.Reals.of_Q q) + | _ -> None end diff --git a/src/lib/reasoners/arrays.ml b/src/lib/reasoners/arrays.ml index 624dbd91e..3aa281702 100644 --- a/src/lib/reasoners/arrays.ml +++ b/src/lib/reasoners/arrays.ml @@ -60,28 +60,12 @@ module Shostak (X : ALIEN) = struct let abstract_selectors _ _ = assert false let solve _ _ = assert false let assign_value r _ eq = - if List.exists (fun (t,_) -> Expr.const_term t) eq then None + if List.exists (fun (t,_) -> Expr.is_model_term t) eq then None else match X.term_extract r with | Some _, true -> Some (Expr.fresh_name (X.type_info r), false) | _ -> assert false - let choose_adequate_model _ _ l = - let acc = - List.fold_left - (fun acc (s, r) -> - if not (Expr.const_term s) then acc - else - match acc with - | Some(s', _) when Expr.compare s' s > 0 -> acc - | _ -> Some (s, r) - ) None l - in - match acc with - | Some (_, r) -> - r, Format.asprintf "%a" X.print r (* it's a EUF constant *) - - | _ -> assert false - + let to_model_term _r = assert false end diff --git a/src/lib/reasoners/bitv.ml b/src/lib/reasoners/bitv.ml index 73079f2b8..06f756905 100644 --- a/src/lib/reasoners/bitv.ml +++ b/src/lib/reasoners/bitv.ml @@ -1543,34 +1543,14 @@ module Shostak(X : ALIEN) = struct let bv = String.make sz '0' in Some (E.bitv bv (Ty.Tbitv sz), true) - let choose_adequate_model t r l = - if Options.get_debug_interpretation () then - Printer.print_dbg - ~module_name:"Bitv" ~function_name:"choose_adequate_model" - "choose_adequate_model for %a" E.print t; - let l = List.map (fun (t, r) -> (t, r, embed r)) l in - let l = List.filter (fun (_, _, a) -> is_cte_abstract a) l in - let r, a = - match l with - | [] -> - let a = embed r in - assert (is_cte_abstract a); - r, a - | (_, r, a) :: l -> - List.iter (fun (_, x, _) -> assert (X.equal x r)) l; - r, a - in - let s = - List.map (function - | { bv = Cte b; sz } -> - Z.format ("%0" ^ string_of_int sz ^ "b") b - | _ -> - (* Cannot happen because [a] must satisfy [is_cte_abstract] at this - point. *) - assert false - ) a - |> String.concat "" - in - r, "#b" ^ s - + let to_model_term r = + match embed r with + | [{ bv = Cte b; sz }] -> + let s = Z.format ("%0" ^ string_of_int sz ^ "b") b in + Some (Expr.bitv s Ty.(Tbitv sz)) + | _ -> + (* A constant semantic value cannot be a concatenation of constant + simple term as the canonizer merges consecutive constant simple + terms. *) + None end diff --git a/src/lib/reasoners/enum.ml b/src/lib/reasoners/enum.ml index e84153a85..1ca19e9f2 100644 --- a/src/lib/reasoners/enum.ml +++ b/src/lib/reasoners/enum.ml @@ -195,21 +195,9 @@ module Shostak (X : ALIEN) = struct Thus we don't need to guess new values here. *) None - let choose_adequate_model _ r l = - let l = - List.filter - (fun (_, r) -> match embed r with Cons _ -> true | _ -> false) l - in - let r = match l with - | (_,r)::l -> - List.iter (fun (_,x) -> assert (X.equal x r)) l; - r - - | [] -> - (* We do this, because terms of some semantic values created - by CS are not created and added to UF *) - match embed r with Cons _ -> r | _ -> assert false - in - r, Format.asprintf "%a" X.print r (* it's a EUF constant *) - + let to_model_term r = + match embed r with + | Cons (hs, ty) -> + Some (E.mk_term Sy.(Op (Constr hs)) [] ty) + | Alien a -> X.to_model_term a end diff --git a/src/lib/reasoners/fun_sat.ml b/src/lib/reasoners/fun_sat.ml index 1ea043114..879645be9 100644 --- a/src/lib/reasoners/fun_sat.ml +++ b/src/lib/reasoners/fun_sat.ml @@ -1877,7 +1877,7 @@ module Make (Th : Theory.S) = struct clear_instances_cache (); Th.reinit_cpt (); Symbols.clear_labels (); - Symbols.reset_id_builders (); + Id.Namespace.reinit (); Var.reinit_cnt (); Satml_types.Flat_Formula.reinit_cpt (); Ty.reinit_decls (); diff --git a/src/lib/reasoners/ite.ml b/src/lib/reasoners/ite.ml index a60151288..fdd6b5794 100644 --- a/src/lib/reasoners/ite.ml +++ b/src/lib/reasoners/ite.ml @@ -60,5 +60,5 @@ module Shostak (X : ALIEN) = struct let abstract_selectors _ _ = assert false let solve _ _ = assert false let assign_value _ _ _ = assert false - let choose_adequate_model _ _ _ = assert false + let to_model_term _r = assert false end diff --git a/src/lib/reasoners/records.ml b/src/lib/reasoners/records.ml index cd75c0ea8..8bbc3b333 100644 --- a/src/lib/reasoners/records.ml +++ b/src/lib/reasoners/records.ml @@ -30,6 +30,7 @@ module Hs = Hstring module E = Expr +module Sy = Symbols type 'a abstract = | Record of (Hs.t * 'a abstract) list * Ty.t @@ -414,7 +415,7 @@ module Shostak (X : ALIEN) = struct | Access _ -> None | Record (_, ty) -> - if List.exists (fun (t,_) -> Expr.const_term t) eq + if List.exists (fun (t,_) -> Expr.is_model_term t) eq then None else Some (Expr.fresh_name ty, false) @@ -426,20 +427,20 @@ module Shostak (X : ALIEN) = struct Some (s, false) (* false <-> not a case-split *) | _ -> assert false - let choose_adequate_model _ _ l = - let acc = - List.fold_left - (fun acc (s, r) -> - if not (Expr.const_term s) then acc - else - match acc with - | Some(s', _) when Expr.compare s' s > 0 -> acc - | _ -> Some (s, r) - ) None l - in - match acc with - | Some (_,r) -> - r, Format.asprintf "%a" X.print r (* it's a EUF constant *) - | _ -> assert false + let to_model_term = + let rec to_model_term r = + match r with + | Record (fields, ty) -> + (* We can ignore the names of fields as they are inlined in the + type [ty] of the record. *) + let l = + Lists.try_map (fun (_name, rf) -> to_model_term rf) fields + in + Option.bind l @@ fun l -> + Some (E.mk_term Sy.(Op Record) l ty) + | Other (a, _) -> + X.to_model_term a + | Access _ -> None + in fun r -> to_model_term (embed r) end diff --git a/src/lib/reasoners/satml_frontend.ml b/src/lib/reasoners/satml_frontend.ml index e41546464..678d855e1 100644 --- a/src/lib/reasoners/satml_frontend.ml +++ b/src/lib/reasoners/satml_frontend.ml @@ -1346,7 +1346,7 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct let reinit_ctx () = Steps.reinit_steps (); Th.reinit_cpt (); - Symbols.reset_id_builders (); + Id.Namespace.reinit (); Symbols.clear_labels (); Var.reinit_cnt (); Satml_types.Flat_Formula.reinit_cpt (); diff --git a/src/lib/reasoners/shostak.ml b/src/lib/reasoners/shostak.ml index fcac11341..e0724c2b8 100644 --- a/src/lib/reasoners/shostak.ml +++ b/src/lib/reasoners/shostak.ml @@ -270,6 +270,23 @@ struct | Ac _ -> None, false (* SYLVAIN : TODO *) | Term t -> Some t, true + let to_model_term r = + let res = + match r.v with + | Arith _ -> ARITH.to_model_term r + | Records _ -> RECORDS.to_model_term r + | Bitv _ -> BITV.to_model_term r + | Arrays _ -> ARRAYS.to_model_term r + | Enum _ -> ENUM.to_model_term r + | Adt _ -> ADT.to_model_term r + | Ite _ -> ITE.to_model_term r + | Term t when Expr.is_model_term t -> Some t + | Ac _ | Term _ -> None + in + Option.bind res @@ fun t -> + assert (Expr.is_model_term t); + Some t + let top () = term_embed Expr.vrai let bot () = term_embed Expr.faux @@ -369,7 +386,20 @@ struct | Enum t -> ENUM.is_constant t | Adt t -> ADT.is_constant t | Ite t -> ITE.is_constant t - | Ac _ | Term _ -> false + | Term t -> + begin + let Expr.{ f; xs; _ } = Expr.term_view t in + (* We don't use [Expr.is_model_term] here to ensure that [t] is a + constant term because most of model terms are represented by + semantic values of builtin theories. Constant terms not managed by + builtin theories have to be considered as constant semantic + values. In particular, this code enforces the invariant: + [e] is a model term ==> [X.make e] is a constant semantic value. *) + match f, xs with + | Symbols.(True | False | Void | Name _), [] -> true + | _ -> false + end + | Ac _ -> false let subst p v r = if equal p v then r @@ -646,8 +676,8 @@ struct end | Term t, ty -> (* case disable_adts() handled here *) - if Expr.const_term t || - List.exists (fun (t,_) -> Expr.const_term t) eq then None + if Expr.is_model_term t || + List.exists (fun (t,_) -> Expr.is_model_term t) eq then None else Some (Expr.fresh_name ty, false) (* false <-> not a case-split *) | _ -> (* There is no model-generation support for the AC symbols yet. @@ -663,66 +693,6 @@ struct | None -> Format.asprintf "None" | Some(res, _is_cs) -> Format.asprintf "%a" Expr.print res); opt - - let choose_adequate_model t rep l = - let r, pprint = - match Expr.type_info t with - | Ty.Tint - | Ty.Treal -> ARITH.choose_adequate_model t rep l - | Ty.Tbitv _ -> BITV.choose_adequate_model t rep l - | Ty.Tsum _ -> ENUM.choose_adequate_model t rep l - | Ty.Tadt _ when not (Options.get_disable_adts()) -> - ADT.choose_adequate_model t rep l - | Ty.Trecord _ -> RECORDS.choose_adequate_model t rep l - | Ty.Tfarray _ -> ARRAYS.choose_adequate_model t rep l - | Ty.Tbool -> - (* case split is now supposed to be done for internal bools if - needed as well *) - assert (is_bool_const rep); - rep, Format.asprintf "%a" print rep - | _ -> - let acc = - List.fold_left - (fun acc (s, r) -> - if Expr.const_term s then - match acc with - | Some(s', _) when Expr.compare s' s > 0 -> acc - | _ -> Some (s, r) - else - acc - ) None l - in - let r = - match acc with - | Some (_,r) -> r - | None -> - match term_extract rep with - | Some t, true when Expr.const_term t -> rep - | _ -> - let print_aux fmt (t,r) = - Format.fprintf fmt "> impossible case: %a -- %a@ " - Expr.print t - print r - in - if Options.get_debug_interpretation () then - Printer.print_dbg - ~module_name:"Shostak" ~function_name:"choose_adequate_model" - "@[What to choose for term %a with rep %a?\ - %a@]" - Expr.print t - print rep - (Printer.pp_list_no_space print_aux) l; - assert false - in - r, Format.asprintf "%a" print r (* it's a EUF constant *) - in - if Options.get_debug_interpretation () then - Printer.print_dbg - ~module_name:"Shostak" ~function_name:"choose_adequate_model" - "%a selected as a model for %a" - print r Expr.print t; - r, pprint - end and TARITH : Polynome.T diff --git a/src/lib/reasoners/sig.mli b/src/lib/reasoners/sig.mli index cc6075f4b..08d626d7c 100644 --- a/src/lib/reasoners/sig.mli +++ b/src/lib/reasoners/sig.mli @@ -128,11 +128,14 @@ module type SHOSTAK = sig [Some (t, false)], then there must be no context in which [solve r (fst X.make t)] raises [Unsolvable]. You have been warned! *) - (* choose the value to print and how to print it for the given term. - The second term is its representative. The list is its equivalence class - *) - val choose_adequate_model : Expr.t -> r -> (Expr.t * r) list -> r * string - + val to_model_term : r -> Expr.t option + (** [to_model_term r] creates a model term if [r] is constant. + The function cannot fail if [r] is a constant (that is statisfied the + predicate [X.is_constant]). + + The returned value always satisfies the predicate + [Expr.is_model_term]. See its documentation for more details about + model terms. *) end module type X = sig @@ -191,8 +194,12 @@ module type X = sig val assign_value : r -> r list -> (Expr.t * r) list -> (Expr.t * bool) option - (* choose the value to print and how to print it for the given term. - The second term is its representative. The list is its equivalence class - *) - val choose_adequate_model : Expr.t -> r -> (Expr.t * r) list -> r * string + val to_model_term : r -> Expr.t option + (** [to_model_term r] creates a model term if [r] is constant. + The function cannot fail if [r] is a constant (that is statisfied the + predicate [X.is_constant]). + + The returned value always satisfies the predicate + [Expr.is_model_term]. See its documentation for more details about + model terms. *) end diff --git a/src/lib/reasoners/uf.ml b/src/lib/reasoners/uf.ml index 4fcfb6534..c22bcff25 100644 --- a/src/lib/reasoners/uf.ml +++ b/src/lib/reasoners/uf.ml @@ -32,7 +32,6 @@ module X = Shostak.Combine module Ac = Shostak.Ac module Ex = Explanation - module Sy = Symbols module E = Expr module ME = Expr.Map @@ -999,95 +998,32 @@ let assign_next env = Debug.check_invariants "assign_next" env; res, env -(**** Counter examples functions ****) -let is_a_good_model_value (x, _) = - match X.leaves x with - [] -> true - | [y] -> X.equal x y - | _ -> false - -let is_const_term (x, _) = - match X.term_extract x with - | Some t, _ -> - E.const_term t - | _ -> - (*cannot test for theories which don't implement term_extract*) - true - -let model_repr_of_term t env mrepr = - try ME.find t mrepr, mrepr - with Not_found -> - let mk = try ME.find t env.make with Not_found -> assert false in - let rep,_ = try MapX.find mk env.repr with Not_found -> assert false in - let cls = - try SE.elements (MapX.find rep env.classes) - with Not_found -> assert false - in - let cls = - try List.rev_map (fun s -> s, ME.find s env.make) cls - with Not_found -> assert false - in - let e = X.choose_adequate_model t rep cls in - e, ME.add t e mrepr - let save_cache () = LX.save_cache () let reinit_cache () = LX.reinit_cache () -let compute_concrete_model_of_val - env t ((fprofs, cprofs, carrays, mrepr) as acc) = - let { E.f; xs; ty; _ } = E.term_view t in - (* Keep record constructors because models.ml expects them to be there *) - if (X.is_solvable_theory_symbol f ty - && not (Shostak.Records.is_mine_symb f ty)) - || E.is_internal_name t || E.is_internal_skolem t - || E.equal t E.vrai || E.equal t E.faux - || Sy.is_internal f - then - acc - else - let xs, tys, mrepr = - List.fold_left - (fun (xs, tys, mrepr) x -> - let rep_x, mrepr = model_repr_of_term x env mrepr in - assert (is_const_term rep_x); - (x, rep_x)::xs, - (E.type_info x)::tys, - mrepr - ) ([],[], mrepr) (List.rev xs) - in - let rep, mrepr = model_repr_of_term t env mrepr in - assert (is_a_good_model_value rep); - assert (is_const_term rep); - match f, xs, ty with - | Sy.Op Sy.Set, _, _ -> acc - - | Sy.Op Sy.Get, [(_,(a,_));((_,(i,_)) as e)], _ -> - begin - match X.term_extract a with - | Some ta, true -> - let { E.f = f_ta; xs=xs_ta; _ } = E.term_view ta in - assert (xs_ta == []); - fprofs, - cprofs, - ModelMap.add (f_ta,[X.type_info i], ty) ([e], rep) carrays, - mrepr - - | _ -> assert false - end +(****************************************************************************) +(* Model generation functions *) +(****************************************************************************) - | _ -> - if tys == [] then - fprofs, ModelMap.add (f, tys, ty) (xs, rep) cprofs, carrays, - mrepr - else - ModelMap.add (f, tys, ty) (xs, rep) fprofs, cprofs, carrays, - mrepr +let model_repr_of_term t env mrepr = + try ME.find t mrepr, mrepr + with Not_found -> + let mk = try ME.find t env.make with Not_found -> assert false in + let rep, _ = try MapX.find mk env.repr with Not_found -> assert false in + (* We call this function during the model generation only. At this time, + we are sure that class representatives are constant semantic values. *) + assert (X.is_constant rep); + match X.to_model_term rep with + | Some v -> v, ME.add t v mrepr + | None -> + (* [X.to_model_term] cannot fail on constant semantic values. *) + assert false -(* A map of expressions / terms, ordered by depth first, and then by - Expr.compare for expressions with same depth. This structure will +(* A map of expressions to terms, ordered by depth first, and then by + [Expr.compare] for expressions with same depth. This structure will be used to build a model, by starting with the inner/smaller terms first. The values associated to the key will be their make *) module MED = Map.Make @@ -1099,15 +1035,186 @@ module MED = Map.Make else Expr.compare a b end) -let terms env = ME.fold MED.add env.make MED.empty +let is_suspicious_name hs = + match Hstring.view hs with + | "@/" | "@%" | "@*" -> true + | _ -> false -let compute_concrete_model env = - MED.fold - (fun t _mk acc -> compute_concrete_model_of_val env t acc - ) (terms env) - (ModelMap.empty, ModelMap.empty, ModelMap.empty, ME.empty) +(* 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 + | _ -> false -let extract_concrete_model ~prop_model env = - let functions, constants, arrays, mrepr = compute_concrete_model env in - { Models.propositional = prop_model; functions; constants; arrays; - terms_values = mrepr } +let terms env = + ME.fold + (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. *) + acc + | _ -> + let suspicious = is_suspicious_symbol f || suspicious in + MED.add t r terms, suspicious + ) env.make (MED.empty, false) + +(* Helper functions used by the caches during the computation of the model. *) +module Cache = struct + let store_array_get arrays_cache (t : Expr.t) (i : Expr.t) (v : Expr.t) = + match Hashtbl.find_opt arrays_cache t with + | Some values -> + Hashtbl.replace values i v + | None -> + let values = Hashtbl.create 17 in + Hashtbl.add values i v; + Hashtbl.add arrays_cache t values + + let get_abstract_for abstracts_cache env (t : Expr.t) = + let r, _ = find env t in + match Hashtbl.find_opt abstracts_cache r with + | Some abstract -> abstract + | None -> + let abstract = Expr.mk_abstract (Expr.type_info t) in + Hashtbl.add abstracts_cache r abstract; + abstract +end + +type cache = { + array_selects: (Expr.t, (Expr.t, Expr.t) Hashtbl.t) + Hashtbl.t; + (** Stores all the get accesses to arrays. *) + + abstracts: (r, Expr.t) Hashtbl.t; + (** Stores all the abstract values generated. This cache is necessary + to ensure we don't generate twice an abstract value for a given symbol. *) +} + +(* The environment of the union-find contains almost a first-order model. + There are two situations that require some computations to retrieve an + appropriate model value: + - As our array theory has no semantic values, there are no value + which represents an array in the union-find environment. Instead, the + union-find stores the collection of all the access to the array. This + function retrieves all these accesses in order to build an expression + which defines the approriate array. + - If the problem involves declared terms whose the type is abstract, + Alt-Ergo cannot produces a constant value for them. This function creates + a new abstract value in this case. *) +let compute_concrete_model_of_val cache = + let store_array_select = Cache.store_array_get cache.array_selects + and get_abstract_for = Cache.get_abstract_for cache.abstracts + in fun env t ((mdl, mrepr) as acc) -> + let { E.f; xs; ty; _ } = E.term_view t in + if X.is_solvable_theory_symbol f ty + || Sy.is_internal f || E.is_internal_name t || E.is_internal_skolem t + || E.equal t E.vrai || E.equal t E.faux + then + (* These terms are built-in interpreted ones and we don't have + to produce a definition for them. *) + acc + else + begin + let arg_vals, arg_tys, mrepr = + List.fold_left + (fun (arg_vals, arg_tys, mrepr) arg -> + let rep_arg, mrepr = model_repr_of_term arg env mrepr in + rep_arg :: arg_vals, + (Expr.type_info arg) :: arg_tys, + mrepr + ) + ([], [], mrepr) (List.rev xs) + in + let ret_rep, mrepr = model_repr_of_term t env mrepr in + match f, arg_vals, ty with + | Sy.Name _, [], Ty.Tfarray _ -> + begin + match Hashtbl.find_opt cache.array_selects t with + | Some _ -> acc + | None -> + (* We have to add an abstract array in case there is no + constraint on its values. *) + Hashtbl.add cache.array_selects t (Hashtbl.create 17); + acc + end + + | Sy.Op Sy.Set, _, _ -> acc + + | Sy.Op Sy.Get, [a; i], _ -> + begin + store_array_select a i ret_rep; + acc + end + + | Sy.Name { hs = id; _ }, _, _ -> + let value = + match ty with + | Ty.Text _ -> + (* We cannot produce a concrete value as the type is abstract. + In this case, we produce an abstract value with the appropriate + type. *) + get_abstract_for env t + | _ -> ret_rep + in + ModelMap.(add (id, arg_tys, ty) arg_vals value mdl), mrepr + + | _ -> + Printer.print_err + "Expect a uninterpreted term declared by the user, got %a" + E.print t; + assert false + end + +let extract_concrete_model cache = + let compute_concrete_model_of_val = compute_concrete_model_of_val cache in + let get_abstract_for = Cache.get_abstract_for cache.abstracts + in fun ~prop_model env -> + let terms, suspicious = terms env in + let model, mrepr = + MED.fold (fun t _mk acc -> compute_concrete_model_of_val env t acc) + terms (ModelMap.empty ~suspicious, ME.empty) + in + let model = + Hashtbl.fold (fun t vals mdl -> + (* We produce a fresh identifiant for abstract value in order to + prevent any capture. *) + let abstract = get_abstract_for env t in + let ty = Expr.type_info t in + let arr_val = + Hashtbl.fold (fun i v arr_val -> + Expr.ArraysEx.store arr_val i v + ) vals abstract + in + let id = + let Expr.{ f; _ } = Expr.term_view t in + match f with + | Sy.Name { hs; _ } -> hs + | _ -> + (* We only store array declarations as keys in the cache + [array_selects]. *) + assert false + in + let mdl = + if not @@ Id.Namespace.Internal.is_id (Hstring.view id) 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. *) + 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 + `compute_concrete_model_of_val` because we need to first iterate + on all the union-find environment to collect array values. *) + ModelMap.subst id arr_val mdl + ) cache.array_selects model + in + { Models.propositional = prop_model; model; term_values = mrepr } + +let extract_concrete_model ~prop_model = + let cache : cache = { + array_selects = Hashtbl.create 17; + abstracts = Hashtbl.create 17; + } + in fun env -> extract_concrete_model cache ~prop_model env diff --git a/src/lib/structures/errors.ml b/src/lib/structures/errors.ml index d0ec32d90..e2bab17d8 100644 --- a/src/lib/structures/errors.ml +++ b/src/lib/structures/errors.ml @@ -89,6 +89,10 @@ type mode_error = | Invalid_set_option of string | Forbidden_command of string +type model_error = + | Subst_type_clash of Id.t * Ty.t * Ty.t + | Subst_not_model_term of Expr.t + type error = | Parser_error of string | Lexical_error of Loc.t * string @@ -98,6 +102,7 @@ type error = | Warning_as_error | Dolmen_error of (int * string) | Mode_error of Util.mode * mode_error + | Model_error of model_error exception Error of error @@ -252,6 +257,18 @@ let report_mode_error fmt = function | Forbidden_command s -> fprintf fmt "Command %s" s +let report_model_error ppf = function + | Subst_type_clash (id, ty1, ty2) -> + Fmt.pf ppf + "Cannot substitute the identifier %a of type %a by an expression of \ + type %a" + Id.pp id + Ty.pp_smtlib ty1 + Ty.pp_smtlib ty2 + + | Subst_not_model_term e -> + Fmt.pf ppf "The expression %a is not a model term" Expr.print e + let report fmt = function | Parser_error s -> Format.fprintf fmt "Parser Error: %s" s; @@ -277,3 +294,5 @@ let report fmt = function "Invalid action during %a mode: %a" Util.pp_mode mode report_mode_error merr; + | Model_error err -> + Fmt.pf fmt "Model Error: %a" report_model_error err diff --git a/src/lib/structures/errors.mli b/src/lib/structures/errors.mli index b0ca4ddc0..f9d8284e9 100644 --- a/src/lib/structures/errors.mli +++ b/src/lib/structures/errors.mli @@ -97,6 +97,11 @@ type mode_error = | Invalid_set_option of string | Forbidden_command of string +(** Errors raised while using models. *) +type model_error = + | Subst_type_clash of Id.t * Ty.t * Ty.t + | Subst_not_model_term of Expr.t + (** All types of error that can be raised *) type error = | Parser_error of string (** Error used at parser loading *) @@ -107,9 +112,13 @@ type error = | Warning_as_error | Dolmen_error of (int * string) (** Error code + description raised by dolmen. *) + | Mode_error of Util.mode * mode_error (** Error used when performing actions forbidden in some modes. *) + | Model_error of model_error + (** Error raised while using models. *) + (** {2 Exceptions } *) exception Error of error diff --git a/src/lib/structures/expr.ml b/src/lib/structures/expr.ml index 42fa54793..360106e03 100644 --- a/src/lib/structures/expr.ml +++ b/src/lib/structures/expr.ml @@ -313,6 +313,16 @@ module SmtPrinter = struct | Sy.Real q when Q.(equal q zero) -> true | _ -> false + let pp_rational ppf q = + if Z.equal (Q.den q) Z.one then + Fmt.pf ppf "%a.0" Z.pp_print (Q.num q) + else if Q.sign q = -1 then + Fmt.pf ppf "(/ (- %a) %a)" + Z.pp_print (Z.abs (Q.num q)) + Z.pp_print (Q.den q) + else + Fmt.pf ppf "(/ %a %a)" Z.pp_print (Q.num q) Z.pp_print (Q.den q) + let pp_binder ppf (var, ty) = Fmt.pf ppf "(%a %a)" Var.print var Ty.pp_smtlib ty @@ -415,6 +425,9 @@ module SmtPrinter = struct | Sy.Op op, [] -> Symbols.pp_smtlib_operator ppf op + | Sy.Op Minus, [e1; { f = Sy.Real q; _ }] when is_zero e1.f -> + pp_rational ppf (Q.neg q) + | Sy.Op Minus, [e1; e2] when is_zero e1.f -> Fmt.pf ppf "@[<2>(- %a@])" pp e2 @@ -427,6 +440,10 @@ module SmtPrinter = struct | Sy.False, [] -> Fmt.pf ppf "false" + | Sy.Name { hs = n; _ }, [] + when Id.Namespace.Abstract.is_id (Hstring.view n) -> + Fmt.pf ppf "(as %a %a)" Id.pp n Ty.pp_smtlib ty + | Sy.Name { hs = n; _ }, [] -> Symbols.pp_name ppf (Hstring.view n) | Sy.Name { hs = n; _ }, _ :: _ -> @@ -443,14 +460,7 @@ module SmtPrinter = struct Fmt.pf ppf "%a" Z.pp_print i | Sy.Real q, [] -> - if Z.equal (Q.den q) Z.one then - Fmt.pf ppf "%a.0" Z.pp_print (Q.num q) - else if Q.sign q = -1 then - Fmt.pf ppf "(/ (- %a) %a)" - Z.pp_print (Z.abs (Q.num q)) - Z.pp_print (Q.den q) - else - Fmt.pf ppf "(/ %a %a)" Z.pp_print (Q.num q) Z.pp_print (Q.den q) + pp_rational ppf q | Sy.Bitv (n, s), [] -> Fmt.pf ppf "#b%s" (Z.format (Fmt.str "%%0%db" n) s) @@ -671,6 +681,8 @@ let print_list_sep sep = let print_list ppf = print_list_sep "," ppf +let pp_smtlib = SmtPrinter.pp + let pp_binders ppf = if Options.get_output_smtlib () then SmtPrinter.pp_binders ppf @@ -895,6 +907,10 @@ let void = mk_term (Sy.Void) [] Ty.Tunit let fresh_name ty = mk_term (Sy.fresh_internal_name ()) [] ty +let mk_abstract ty = + let id = Id.Namespace.Abstract.fresh () |> Hstring.make in + mk_term (Sy.Name { hs = id; defined = false; kind = Other }) [] ty + let is_internal_name t = match t with | { f; xs = []; _ } -> Sy.is_fresh_internal_name f @@ -1015,14 +1031,23 @@ let mk_ite cond th el = if ty == Ty.Tbool then mk_if cond th el else mk_term (Sy.Op Sy.Tite) [cond; th; el] ty -let [@inline always] const_term e = - (* we use this function because depth is currently not correct to +let rec is_model_term e = + match e.f, e.xs with + | (Op Constr _ | Op Record | Op Set), xs -> List.for_all is_model_term xs + | Op Div, [{ f = Real _; _ }; { f = Real _; _ }] -> true + | Op Minus, [{ f = Real q; _ }; { f = Real _; _ }] -> Q.equal q Q.zero + | Op Minus, [{ f = Int i; _ }; { f = Int _; _ }] -> Z.equal i Z.zero + | (True | False | Void | Name _ | Int _ | Real _ | Bitv _), [] -> true + | _ -> false + +let[@inline always] is_value_term e = + (* We use this function because depth is currently not correct to detect constants (not incremented in some situations due to - some regression) *) + some regression). *) match e.f with - | Sy.Form _ | Sy.Lit _ | Sy.Let -> false - | True | False | Void | Name _ | Int _ | Real _ | Bitv _ - | Op _ | Var _ | In _ | MapsTo _ -> + | Sy.Form _ | Sy.Lit _ | Sy.Let -> false + | True | False | Void | Name _ | Int _ | Real _ | Bitv _ | Op _ + | Var _ | In _ | MapsTo _ -> let res = (e.xs == []) in assert (res == (depth e <= 1)); res @@ -1368,7 +1393,7 @@ and mk_let_aux ({ let_v; let_e; in_e; _ } as x) = try let _, nb_occ = Var.Map.find let_v in_e.vars in if nb_occ = 1 && (let_e.pure (*1*) || Sy.equal (Sy.var let_v) in_e.f) || - const_term let_e then (* inline in these situations *) + is_value_term let_e then (* inline in these situations *) apply_subst_aux (Var.Map.singleton let_v let_e, Ty.esubst) in_e else let ty = type_info in_e in @@ -1697,7 +1722,7 @@ let skolemize { main = f; binders; sko_v; sko_vty; _ } = let mk_sym cpt s = Fmt.kstr - (fun str -> Sy.make_as_fresh_skolem str) + (fun str -> Sy.name (Id.Namespace.make_as_fresh_skolem str)) "%s%s!%d" s tyvars @@ -3112,3 +3137,20 @@ module BV = struct let bvsgt s t = bvslt t s let bvsge s t = bvsle t s end + +(** Constructors from the smtlib theory of functional arrays with + extensionality logic. + + https://smtlib.cs.uiowa.edu/theories-ArraysEx.shtml *) +module ArraysEx = struct + let select a i = + let rty = + match type_info a with + | Tfarray (_, rty) -> rty + | _ -> invalid_arg "Expr.ArraysEx.select" + in + mk_term Sy.(Op Get) [a; i] rty + + let store a i v = + mk_term Sy.(Op Set) [a; i; v] (type_info a) +end diff --git a/src/lib/structures/expr.mli b/src/lib/structures/expr.mli index 3bc83c5c5..8ca71acbc 100644 --- a/src/lib/structures/expr.mli +++ b/src/lib/structures/expr.mli @@ -151,6 +151,10 @@ val print_list : Format.formatter -> t list -> unit val print_list_sep : string -> Format.formatter -> t list -> unit val print_triggers : Format.formatter -> trigger list -> unit +val pp_smtlib : t Fmt.t +(** [pp_smtlib ppf e] prints the expression [e] on the formatter + [ppf] using the SMT-LIB standard. *) + (** Comparison and hashing functions *) val compare : t -> t -> int @@ -198,6 +202,11 @@ val int : string -> t val real : string -> t val bitv : string -> Ty.t -> t val fresh_name : Ty.t -> t + +val mk_abstract : Ty.t -> t +(** [mk_abstract ty] creates an abstract model term of type [ty]. + This function is intended to be used only in models. *) + val pred : t -> t (** smart constructors for literals *) @@ -331,8 +340,13 @@ val print_th_elt : Format.formatter -> th_elt -> unit val is_pure : t -> bool -val const_term : t -> bool -(** return true iff the given argument is a term without arguments *) +val is_model_term : t -> bool +(** [is_model_term e] checks if the expression [e] is a model terms. + A model term can be: + - A record definition involving only model terms. + - A constructor application involving only model terms, + - A literal of a basic type (integer, real, boolean, unit or bitvector), + - A name. *) val save_cache: unit -> unit (** Saves the modules cache *) @@ -478,3 +492,12 @@ module BV : sig val bvlshr : t -> t -> t val bvashr : t -> t -> t end + +(** Constructors from the smtlib theory of functional arrays with + extensionality logic. + + https://smtlib.cs.uiowa.edu/theories-ArraysEx.shtml *) +module ArraysEx : sig + val select : t -> t -> t + val store : t -> t -> t -> t +end diff --git a/src/lib/structures/id.ml b/src/lib/structures/id.ml new file mode 100644 index 000000000..e34de223f --- /dev/null +++ b/src/lib/structures/id.ml @@ -0,0 +1,81 @@ +(**************************************************************************) +(* *) +(* Alt-Ergo: The SMT Solver For Software Verification *) +(* Copyright (C) 2013-2023 --- OCamlPro SAS *) +(* *) +(* This file is distributed under the terms of OCamlPro *) +(* Non-Commercial Purpose License, version 1. *) +(* *) +(* As an exception, Alt-Ergo Club members at the Gold level can *) +(* use this file under the terms of the Apache Software License *) +(* version 2.0. *) +(* *) +(* --------------------------------------------------------------- *) +(* *) +(* The Alt-Ergo theorem prover *) +(* *) +(* Sylvain Conchon, Evelyne Contejean, Francois Bobot *) +(* Mohamed Iguernelala, Stephane Lescuyer, Alain Mebsout *) +(* *) +(* CNRS - INRIA - Universite Paris Sud *) +(* *) +(* Until 2013, some parts of this code were released under *) +(* the Apache Software License version 2.0. *) +(* *) +(* --------------------------------------------------------------- *) +(* *) +(* More details can be found in the directory licenses/ *) +(* *) +(**************************************************************************) + +type t = Hstring.t [@@deriving ord] + +let equal = Hstring.equal + +let pp ppf id = + Dolmen.Smtlib2.Script.Poly.Print.id ppf + (Dolmen.Std.Name.simple (Hstring.view id)) + +let show id = Fmt.str "%a" pp id + +module Namespace = struct + module type S = sig + val fresh : ?base:string -> unit -> string + val is_id : string -> bool + end + + module Make (S : sig val prefix : string end) = struct + let make_as_fresh = (^) S.prefix + + let fresh, reset_fresh_cpt = + let cpt = ref 0 in + let fresh_string ?(base = "") () = + let res = make_as_fresh (base ^ (string_of_int !cpt)) in + incr cpt; + res + in + let reset_fresh_string_cpt () = + cpt := 0 + in + fresh_string, reset_fresh_string_cpt + + let is_id = Stdcompat.String.starts_with ~prefix:S.prefix + end + + module Internal = Make (struct let prefix = ".k" end) + + module Skolem = Make + (struct + (* garder le suffixe "__" car cela influence l'ordre *) + let prefix = ".?__" + end) + + let make_as_fresh_skolem = Skolem.make_as_fresh + + module Abstract = Make (struct let prefix = "@a" end) + + let reinit () = + Internal.reset_fresh_cpt (); + Skolem.reset_fresh_cpt (); + Abstract.reset_fresh_cpt () +end diff --git a/src/lib/structures/id.mli b/src/lib/structures/id.mli new file mode 100644 index 000000000..0b2434918 --- /dev/null +++ b/src/lib/structures/id.mli @@ -0,0 +1,52 @@ +(**************************************************************************) +(* *) +(* Alt-Ergo: The SMT Solver For Software Verification *) +(* Copyright (C) 2013-2023 --- OCamlPro SAS *) +(* *) +(* This file is distributed under the terms of OCamlPro *) +(* Non-Commercial Purpose License, version 1. *) +(* *) +(* As an exception, Alt-Ergo Club members at the Gold level can *) +(* use this file under the terms of the Apache Software License *) +(* version 2.0. *) +(* *) +(* --------------------------------------------------------------- *) +(* *) +(* The Alt-Ergo theorem prover *) +(* *) +(* Sylvain Conchon, Evelyne Contejean, Francois Bobot *) +(* Mohamed Iguernelala, Stephane Lescuyer, Alain Mebsout *) +(* *) +(* CNRS - INRIA - Universite Paris Sud *) +(* *) +(* Until 2013, some parts of this code were released under *) +(* the Apache Software License version 2.0. *) +(* *) +(* --------------------------------------------------------------- *) +(* *) +(* More details can be found in the directory licenses/ *) +(* *) +(**************************************************************************) + +type t = Hstring.t [@@deriving ord] + +val equal : t -> t -> bool +val show : t -> string +val pp : t Fmt.t + +module Namespace : sig + module type S = sig + val fresh : ?base:string -> unit -> string + val is_id : string -> bool + end + + module Internal : S + module Skolem : S + module Abstract : S + + val make_as_fresh_skolem : string -> string + + val reinit : unit -> unit + (** Resets the [fresh_internal_name], [fresh_skolem] and [fresh_abstract] + counters. *) +end diff --git a/src/lib/structures/modelMap.ml b/src/lib/structures/modelMap.ml index d41ea00d6..2b7fb096f 100644 --- a/src/lib/structures/modelMap.ml +++ b/src/lib/structures/modelMap.ml @@ -29,100 +29,152 @@ (**************************************************************************) module X = Shostak.Combine - module Sy = Symbols -module E = Expr +type sy = Id.t * Ty.t list * Ty.t [@@deriving ord] + +module Graph = struct + module M = Map.Make + (struct + type t = Expr.t list [@@deriving ord] + end) + + type t = Expr.t M.t + + let empty = M.empty + let add = M.add + let map = M.map + + (* A fiber of the function [f] over a value [v] is the set of all the values + in the domain of [f] whose the image by [f] is [v]. + + The function [inverse] of this module constructs a map of all the + non-empty fibers of the function represented by its graph. *) + module Fiber = struct + include Set.Make (struct + type t = Expr.t list [@@deriving ord] + end) + + let pp_arg ppf (ctr, arg) = + Fmt.pf ppf "(= arg_%i %a)" ctr Expr.pp_smtlib arg + + (* For an argument (x_1, ..., x_n) of the function represented by the graph, + prints the SMT-LIB formula: + (and (= arg_0 x_1)(= arg_1 x2) ... (= arg_n x_n)). + *) + let pp_args ppf = function + | [] -> () + | [arg] -> + pp_arg ppf (0, arg) + | args -> + Fmt.pf ppf "(and %a)" Fmt.(iter_bindings ~sep:sp List.iteri pp_arg) args + + (* For a fiber [x; y; z; ...] of the function represented by the graph, + prints the SMT-LIB formula: + (or + (and (= arg_0 x_0) (= arg_1 x_1) ...) + (and (= arg_0 y_0) (= arg_1 y_1) ...) + ...) + *) + let pp ppf fiber = + match cardinal fiber with + | 0 -> () + | 1 -> + let args = choose fiber in + Fmt.pf ppf "%a" pp_args args + | _ -> + Fmt.pf ppf "(or %a)" (Fmt.iter ~sep:Fmt.sp iter pp_args) fiber + end + + (* Compute all the fibers of the function represented by the graph. *) + let inverse graph = + M.fold (fun arg_vals ret_val acc -> + match Expr.Map.find_opt ret_val acc with + | Some fib -> + Expr.Map.add ret_val (Fiber.add arg_vals fib) acc + | None -> + Expr.Map.add ret_val (Fiber.of_list [arg_vals]) acc + ) graph Expr.Map.empty + + let pp_inverse ppf rel = + let rec aux ppf seq = + match seq () with + | Seq.Nil -> () + | Cons ((ret_val, _), seq) when Stdcompat.Seq.is_empty seq -> + Fmt.pf ppf "%a" Expr.pp_smtlib ret_val + | Cons ((ret_val, fiber), seq) -> + Fmt.pf ppf "(@[ite %a@ %a@ %a)@]" + Fiber.pp fiber + Expr.pp_smtlib ret_val + aux seq + in + aux ppf (Expr.Map.to_seq rel) +end module P = Map.Make (struct - type t = Sy.t * Ty.t list * Ty.t - - let (|||) c1 c2 = if c1 <> 0 then c1 else c2 - - let compare (a1, b1, c1) (a2, b2, c2) = - let l1_l2 = List.length b1 - List.length b2 in - let c = l1_l2 ||| (Ty.compare c1 c2) ||| (Sy.compare a1 a2) in - if c <> 0 then c - else - let c = ref 0 in - try - List.iter2 - (fun ty1 ty2 -> - let d = Ty.compare ty1 ty2 in - if d <> 0 then begin c := d; raise Exit end - ) b1 b2; - 0 - with - | Exit -> assert (!c <> 0); !c - | Invalid_argument _ -> assert false - end) + type t = sy -module V = Set.Make - (struct - type t = (E.t * (X.r * string)) list * (X.r * string) - let compare (l1, (v1,_)) (l2, (v2,_)) = - let c = X.hash_cmp v1 v2 in - if c <> 0 then c - else - let c = ref 0 in - try - List.iter2 - (fun (_,(x,_)) (_,(y,_)) -> - let d = X.hash_cmp x y in - if d <> 0 then begin c := d; raise Exit end - ) l1 l2; - !c - with - | Exit -> !c - | Invalid_argument _ -> List.length l1 - List.length l2 + let compare = compare_sy end) -type key = P.key -type elt = V.t - type t = { - values : V.t P.t; + values : Graph.t P.t; suspicious : bool; } -let is_suspicious_name hs = - match Hstring.view hs with - | "@/" | "@%" | "@*" -> true - | _ -> false - -(* The model generation is known to be imcomplete for FPA and Bitvector - theories. *) -let is_suspicious_symbol = function - | Sy.Op (Float | Abs_int | Abs_real | Sqrt_real - | Sqrt_real_default | Sqrt_real_excess - | Real_of_int | Int_floor | Int_ceil - | Max_int | Max_real | Min_int | Min_real - | Pow | Integer_log2 | Integer_round) -> true - | Sy.Name { hs; _ } when is_suspicious_name hs -> true - | _ -> false - -let add ((sy, _, _) as p) v { values; suspicious } = - let prof_p = try P.find p values with Not_found -> V.empty in - let values = - if V.mem v prof_p then values - else P.add p (V.add v prof_p) values - in - { values; suspicious = suspicious || is_suspicious_symbol sy } - -let iter f { values; _ } = - P.iter (fun ((sy, _, _) as key) value -> - match sy with - | Sy.Name { defined = true; _ } -> - (* We don't print constants defined by the user. *) - () - | _ -> f key value - ) values - -let[@inline always] is_suspicious { suspicious; _ } = suspicious - -let fold f { values; _ } acc = P.fold f values acc - -let empty = { values = P.empty; suspicious = false } - -let is_empty { values; _ } = P.is_empty values +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; + + let graph = try P.find sy values with Not_found -> Graph.empty in + let values = P.add sy (Graph.add arg_vals ret_val graph) values in + { values; suspicious } + +let empty ~suspicious = { values = P.empty; suspicious } + +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' -> + let ty = Expr.type_info e in + if not @@ Ty.equal ty ty' then + raise (Errors.Error (Model_error (Subst_type_clash (id, ty', ty)))); + e + | _ -> + begin + let xs = List.map (subst_in_term id e) xs in + Expr.mk_term f xs ty' + end + +let subst id e { values; suspicious } = + if not @@ Expr.is_model_term e then + raise (Errors.Error (Model_error (Subst_not_model_term e))); + let values = P.map (Graph.map (subst_in_term id e)) values in + { values; suspicious } + +let pp_named_arg_ty ~unused ppf (arg_name, arg_ty) = + let pp_unused ppf unused = if unused then Fmt.pf ppf "_" else () in + Fmt.pf ppf "(%aarg_%i %a)" pp_unused unused arg_name Ty.pp_smtlib arg_ty + +let pp_define_fun ppf ((id, arg_tys, ret_ty), graph) = + let inverse_rel = Graph.inverse graph in + let is_constant = Expr.Map.cardinal inverse_rel = 1 in + 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 + Fmt.(list ~sep:sp (pp_named_arg_ty ~unused:is_constant)) named_arg_tys + Ty.pp_smtlib ret_ty + Graph.pp_inverse inverse_rel + +let pp ppf {values; suspicious} = + if suspicious then begin + Fmt.pf ppf "; This model is a best-effort. It includes symbols\n\ + ; for which model generation is known to be incomplete.@." + end; + if P.is_empty values then + Fmt.pf ppf "@[(@]@,)" + else + Fmt.pf ppf "@[(@,%a@]@,)" + (Fmt.iter_bindings ~sep:Fmt.cut P.iter pp_define_fun) values diff --git a/src/lib/structures/modelMap.mli b/src/lib/structures/modelMap.mli index c9584a88e..9d8e9f0ec 100644 --- a/src/lib/structures/modelMap.mli +++ b/src/lib/structures/modelMap.mli @@ -28,33 +28,31 @@ (* *) (**************************************************************************) -(** Maps of values for alt-ergo's models. - Elements are sorted by symbols/types (P) and accumulated as sets - of expressions matching the P.key type (V). -*) - -module P : Map.S with type key = - Symbols.t * Ty.t list * Ty.t - -module V : Set.S with type elt = - (Expr.t * (Shostak.Combine.r * string)) list * - (Shostak.Combine.r * string) - -type key = P.key -type elt = V.t +type sy = Id.t * Ty.t list * Ty.t +(** Typed symbol of function defined in the model. In order: + - The identifier of the symbol. + - The types of its arguments. + - The returned type. *) type t +(** Type of model. *) -val add : key -> V.elt -> t -> t - -val iter : (key -> elt -> unit) -> t -> unit +val add : sy -> 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]. *) -val fold : (key -> elt -> 'acc -> 'acc) -> t -> 'acc -> 'acc +val empty : suspicious:bool -> 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 empty : t +val subst : Id.t -> Expr.t -> t -> t +(** [subst id e mdl] substitutes all the occurrences of the identifier [id] + in the model [mdl] by the model term [e]. -val is_empty : t -> bool + @Raise Error if the expression [e] is not a model term or the type of + [e] doesn't agree with some occurrence of [id] in the model. *) -val is_suspicious : t -> bool -(* Determine if the model is suspicious as it contains symbols - of theories for which the model generation is not properly supported. *) +val pp : t Fmt.t +(** [pp ppf mdl] prints the model [mdl] on the formatter [ppf] using the + SMT-LIB format. *) diff --git a/src/lib/structures/symbols.ml b/src/lib/structures/symbols.ml index bcde80996..7946d4a3f 100644 --- a/src/lib/structures/symbols.ml +++ b/src/lib/structures/symbols.ml @@ -79,12 +79,11 @@ type bound_kind = Unbounded | VarBnd of Var.t | ValBnd of Numbers.Q.t type bound = (* private *) { kind : bound_kind; sort : Ty.t; is_open : bool; is_lower : bool } - type t = | True | False | Void - | Name of { hs : Hstring.t ; kind : name_kind ; defined : bool } + | Name of { hs : Id.t ; kind : name_kind ; defined : bool } | Int of Z.t | Real of Q.t | Bitv of int * Z.t @@ -454,49 +453,17 @@ let to_string sy = Fmt.str "%a" (AEPrinter.pp ~show_vars:true) sy -module type Id = sig - val fresh : ?base:string -> unit -> string - val reset_fresh_cpt : unit -> unit - val is_id : string -> bool - val make_as_fresh : string -> string -end - -module MakeId(S : sig val prefix : string end) : Id = struct - - let make_as_fresh = (^) S.prefix - - let fresh, reset_fresh_cpt = - let cpt = ref 0 in - let fresh_string ?(base = "") () = - incr cpt; - make_as_fresh (base ^ (string_of_int !cpt)) - in - let reset_fresh_string_cpt () = - cpt := 0 - in - fresh_string, reset_fresh_string_cpt +let fresh_internal_name () = name (Id.Namespace.Internal.fresh ()) - let is_id = Stdcompat.String.starts_with ~prefix:S.prefix -end - -module InternalId = MakeId(struct let prefix = ".k" end) -module SkolemId = MakeId(struct let prefix = ".?__" end) -(* garder le suffixe "__" car cela influence l'ordre *) - -let fresh_internal_string () = InternalId.fresh () -let fresh_internal_name () = name (fresh_internal_string ()) - -let fresh_skolem_string base = SkolemId.fresh ~base () +let fresh_skolem_string base = Id.Namespace.Skolem.fresh ~base () let fresh_skolem_name base = name (fresh_skolem_string base) -let make_as_fresh_skolem str = name (SkolemId.make_as_fresh str) - let is_fresh_internal_name = function - | Name { hs = hd; _ } -> InternalId.is_id (Hstring.view hd) + | Name { hs = hd; _ } -> Id.Namespace.Internal.is_id (Hstring.view hd) | _ -> false let is_fresh_skolem = function - | Name { hs = hd; _ } -> SkolemId.is_id (Hstring.view hd) + | Name { hs = hd; _ } -> Id.Namespace.Skolem.is_id (Hstring.view hd) | _ -> false let is_get f = equal f (Op Get) @@ -516,10 +483,6 @@ let label t = try Labels.find labels t with Not_found -> Hstring.empty let clear_labels () = Labels.clear labels -let reset_id_builders () = - InternalId.reset_fresh_cpt (); - SkolemId.reset_fresh_cpt () - module Set : Set.S with type elt = t = Set.Make (struct type t=s let compare=compare end) diff --git a/src/lib/structures/symbols.mli b/src/lib/structures/symbols.mli index 04df74d6e..e5d234ed6 100644 --- a/src/lib/structures/symbols.mli +++ b/src/lib/structures/symbols.mli @@ -83,7 +83,7 @@ type t = | True | False | Void - | Name of { hs : Hstring.t ; kind : name_kind ; defined : bool } + | Name of { hs : Id.t ; kind : name_kind ; defined : bool } | Int of Z.t | Real of Q.t | Bitv of int * Z.t @@ -137,14 +137,13 @@ val pp_smtlib_operator : operator Fmt.t (*val dummy : t*) -val fresh_internal_string : unit -> string val fresh_internal_name : unit -> t val is_fresh_internal_name : t -> bool val fresh_skolem_string : string -> string val fresh_skolem_name : string -> t -val make_as_fresh_skolem : string -> t val is_fresh_skolem : t -> bool + (** Resets to 0 the fresh symbol counter *) val is_get : t -> bool @@ -159,9 +158,6 @@ val string_of_bound : bound -> string val clear_labels : unit -> unit (** Empties the labels Hashtable *) -val reset_id_builders : unit -> unit -(** Resets the `fresh_internal_name` and `fresh_skolem` counters. *) - module Set : Set.S with type elt = t module Map : Map.S with type key = t diff --git a/src/lib/util/lists.ml b/src/lib/util/lists.ml index f959ac1a1..10b9389ae 100644 --- a/src/lib/util/lists.ml +++ b/src/lib/util/lists.ml @@ -51,3 +51,11 @@ let apply_right f l = )([], true) l in (if same then l else List.rev res), same + +let rec try_map f l = + match l with + | [] -> Some [] + | x :: xs -> + Option.bind (f x) @@ fun y -> + Option.bind (try_map f xs) @@ fun ys -> + Some (y :: ys) diff --git a/src/lib/util/lists.mli b/src/lib/util/lists.mli index 01cb2555b..8cf8eb0fe 100644 --- a/src/lib/util/lists.mli +++ b/src/lib/util/lists.mli @@ -47,3 +47,7 @@ val apply : ('a -> 'a) -> 'a list -> 'a list * bool val apply_right : ('a -> 'a) -> ('b * 'a) list -> ('b * 'a) list * bool (** similar to function apply, but the elements of the list are couples **) + +val try_map : ('a -> 'b option) -> 'a list -> 'b list option +(** [try_map f l] is similar to [List.map f l] but the function [f] + may fail and the iterator shortcuts the computation. *) diff --git a/src/lib/util/util.ml b/src/lib/util/util.ml index a2d7048f6..07d1dc490 100644 --- a/src/lib/util/util.ml +++ b/src/lib/util/util.ml @@ -203,7 +203,6 @@ let print_list ~sep ~pp fmt l = Format.fprintf fmt "%a" pp e; List.iter (fun e -> Format.fprintf fmt "%s %a" sep pp e) l - let rec print_list_pp ~sep ~pp fmt = function | [] -> () | [x] -> pp fmt x diff --git a/tests/cram.t/run.t b/tests/cram.t/run.t index bf837bf48..1aa6dc1e5 100644 --- a/tests/cram.t/run.t +++ b/tests/cram.t/run.t @@ -10,9 +10,9 @@ appropriate here. unknown ( - (define-fun a1 () (Array Int Int) (store (as @a0 (Array Int Int)) 0 0)) (define-fun x () Int 0) (define-fun y () Int 0) + (define-fun a1 () (Array Int Int) (store (as @a0 (Array Int Int)) 0 0)) ) Now we will test some semantic triggers. diff --git a/tests/dune.inc b/tests/dune.inc index 196e9039c..26d82ad68 100644 --- a/tests/dune.inc +++ b/tests/dune.inc @@ -210019,6 +210019,27 @@ ; Auto-generated part begin (subdir models/array + (rule + (target embedded-array.models_dolmen.output) + (deps (:input embedded-array.models.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes (or 0) + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + %{input}))))))) + (rule + (deps embedded-array.models_dolmen.output) + (alias runtest-quick) + (package alt-ergo) + (action + (diff embedded-array.models.expected embedded-array.models_dolmen.output))) (rule (target array1.models_dolmen.output) (deps (:input array1.models.smt2)) @@ -210443,6 +210464,48 @@ ; Auto-generated part begin (subdir models/records + (rule + (target record3.models_dolmen.output) + (deps (:input record3.models.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes (or 0) + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + %{input}))))))) + (rule + (deps record3.models_dolmen.output) + (alias runtest-quick) + (package alt-ergo) + (action + (diff record3.models.expected record3.models_dolmen.output))) + (rule + (target record2.models_dolmen.output) + (deps (:input record2.models.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes (or 0) + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + %{input}))))))) + (rule + (deps record2.models_dolmen.output) + (alias runtest-quick) + (package alt-ergo) + (action + (diff record2.models.expected record2.models_dolmen.output))) (rule (target record1.models_dolmen.output) (deps (:input record1.models.smt2)) diff --git a/tests/issues/555.models.expected b/tests/issues/555.models.expected index ef323fb3e..086ba7ffb 100644 --- a/tests/issues/555.models.expected +++ b/tests/issues/555.models.expected @@ -1,8 +1,8 @@ unknown ( - (define-fun a1 () (Array Int Int) (store (as @a0 (Array Int Int)) 0 0)) - (define-fun a2 () (Array Int Int) (store (as @a1 (Array Int Int)) 0 0)) (define-fun x () Int 0) (define-fun y () Int 0) + (define-fun a1 () (Array Int Int) (store (as @a1 (Array Int Int)) 0 0)) + (define-fun a2 () (Array Int Int) (store (as @a0 (Array Int Int)) 0 0)) ) diff --git a/tests/issues/854/function.models.expected b/tests/issues/854/function.models.expected index ebc7421cb..bb0b49fe0 100644 --- a/tests/issues/854/function.models.expected +++ b/tests/issues/854/function.models.expected @@ -1,8 +1,8 @@ unknown ( - (define-fun intrefqtmk ((arg_0 Int)) intref (as @a0 intref)) - (define-fun f ((arg_0 Int)) Int 0) + (define-fun intrefqtmk ((_arg_0 Int)) intref (as @a0 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/function.models.smt2 b/tests/issues/854/function.models.smt2 index 65e42142b..57ef18bcd 100644 --- a/tests/issues/854/function.models.smt2 +++ b/tests/issues/854/function.models.smt2 @@ -5,7 +5,7 @@ (declare-fun intrefqtmk (Int) intref) (declare-fun a () Int) (declare-fun f (Int) Int) -(define-fun aqtunused ((x Int)) intref (intrefqtmk (f a))) +(define-fun aqtunused ((_x Int)) intref (intrefqtmk (f a))) (assert (= (aqtunused 0) (aqtunused 1))) (declare-fun a1 () Int) (assert (not (and (<= 5 a1) (<= a1 15)))) diff --git a/tests/issues/854/original.models.expected b/tests/issues/854/original.models.expected index 8e20717fb..9198abbbf 100644 --- a/tests/issues/854/original.models.expected +++ b/tests/issues/854/original.models.expected @@ -1,7 +1,7 @@ unknown ( - (define-fun intrefqtmk ((arg_0 Int)) intref (as @a0 intref)) + (define-fun intrefqtmk ((_arg_0 Int)) intref (as @a0 intref)) (define-fun a () Int 0) (define-fun a1 () Int 0) ) diff --git a/tests/issues/854/twice_eq.models.expected b/tests/issues/854/twice_eq.models.expected index 0168a993e..f18c7f58e 100644 --- a/tests/issues/854/twice_eq.models.expected +++ b/tests/issues/854/twice_eq.models.expected @@ -1,8 +1,8 @@ unknown ( - (define-fun intrefqtmk ((arg_0 Int)) intref (as @a0 intref)) - (define-fun another_mk ((arg_0 Int)) intref (as @a0 intref)) + (define-fun intrefqtmk ((_arg_0 Int)) intref (as @a0 intref)) + (define-fun another_mk ((_arg_0 Int)) intref (as @a0 intref)) (define-fun a () Int 0) (define-fun a1 () Int 0) ) diff --git a/tests/models/arith/arith11.optimize.expected b/tests/models/arith/arith11.optimize.expected index b83837cc9..99f7450f0 100644 --- a/tests/models/arith/arith11.optimize.expected +++ b/tests/models/arith/arith11.optimize.expected @@ -1,9 +1,9 @@ unknown ( - (define-fun x () Real 2.0) (define-fun p1 () Bool false) (define-fun p2 () Bool true) + (define-fun x () Real 2.0) ) (objectives (x 2.0) diff --git a/tests/models/arith/arith5.optimize.expected b/tests/models/arith/arith5.optimize.expected index 68d4b0380..e886d1332 100644 --- a/tests/models/arith/arith5.optimize.expected +++ b/tests/models/arith/arith5.optimize.expected @@ -6,5 +6,5 @@ unknown (define-fun z () Real (/ (- 7) 9)) ) (objectives - (x (- (/ 1 18))) + (x (/ (- 1) 18)) ) \ No newline at end of file diff --git a/tests/models/array/array1.models.expected b/tests/models/array/array1.models.expected index ef323fb3e..086ba7ffb 100644 --- a/tests/models/array/array1.models.expected +++ b/tests/models/array/array1.models.expected @@ -1,8 +1,8 @@ unknown ( - (define-fun a1 () (Array Int Int) (store (as @a0 (Array Int Int)) 0 0)) - (define-fun a2 () (Array Int Int) (store (as @a1 (Array Int Int)) 0 0)) (define-fun x () Int 0) (define-fun y () Int 0) + (define-fun a1 () (Array Int Int) (store (as @a1 (Array Int Int)) 0 0)) + (define-fun a2 () (Array Int Int) (store (as @a0 (Array Int Int)) 0 0)) ) diff --git a/tests/models/array/embedded-array.models.expected b/tests/models/array/embedded-array.models.expected new file mode 100644 index 000000000..dd6a80ae9 --- /dev/null +++ b/tests/models/array/embedded-array.models.expected @@ -0,0 +1,8 @@ + +unknown +( + (define-fun s () S (as @a0 S)) + (define-fun x () Pair + (pair (store (as @a1 (Array Int S)) 0 s) + (store (as @a1 (Array Int S)) 0 s))) +) diff --git a/tests/models/array/embedded-array.models.smt2 b/tests/models/array/embedded-array.models.smt2 new file mode 100644 index 000000000..fa76cb828 --- /dev/null +++ b/tests/models/array/embedded-array.models.smt2 @@ -0,0 +1,10 @@ +(set-option :produce-models true) +(set-logic ALL) +(declare-sort S 0) +(declare-const s S) +(declare-datatype Pair ((pair (first (Array Int S)) (second (Array Int S))))) +(declare-const x Pair) +(assert (= (select (first x) 0) s)) +(assert (= (first x) (second x))) +(check-sat) +(get-model) diff --git a/tests/models/bitv/extract.models.expected b/tests/models/bitv/extract.models.expected index 99bcb1175..16b1f5e3a 100644 --- a/tests/models/bitv/extract.models.expected +++ b/tests/models/bitv/extract.models.expected @@ -1,8 +1,8 @@ unknown ( - (define-fun z () (_ BitVec 1) #b0) (define-fun a () (_ BitVec 2) #b11) (define-fun b () (_ BitVec 3) #b111) (define-fun c () (_ BitVec 6) #b111011) + (define-fun z () (_ BitVec 1) #b0) ) diff --git a/tests/models/records/record1.models.expected b/tests/models/records/record1.models.expected index c8d49e171..da5e88f8f 100644 --- a/tests/models/records/record1.models.expected +++ b/tests/models/records/record1.models.expected @@ -1,5 +1,5 @@ unknown ( - (define-fun a () Pair (pair 5 (as @a0 Int))) + (define-fun a () Pair (pair 5 0)) ) diff --git a/tests/models/records/record2.models.expected b/tests/models/records/record2.models.expected new file mode 100644 index 000000000..d95838e69 --- /dev/null +++ b/tests/models/records/record2.models.expected @@ -0,0 +1,5 @@ + +unknown +( + (define-fun f ((_arg_0 Int)) Pair (pair 5 0)) +) diff --git a/tests/models/records/record2.models.smt2 b/tests/models/records/record2.models.smt2 new file mode 100644 index 000000000..1e4238645 --- /dev/null +++ b/tests/models/records/record2.models.smt2 @@ -0,0 +1,8 @@ +(set-logic ALL) +(set-option :produce-models true) +(declare-datatype Pair +((pair (first Int) (second Int)))) +(declare-fun f (Int) Pair) +(assert (= (first (f 0)) 5)) +(check-sat) +(get-model) diff --git a/tests/models/records/record3.models.expected b/tests/models/records/record3.models.expected new file mode 100644 index 000000000..b478bf755 --- /dev/null +++ b/tests/models/records/record3.models.expected @@ -0,0 +1,7 @@ + +unknown +( + (define-fun f ((_arg_0 Int)) Pair (pair 5 0)) + (define-fun x () Int 0) + (define-fun y () Int 5) +) diff --git a/tests/models/records/record3.models.smt2 b/tests/models/records/record3.models.smt2 new file mode 100644 index 000000000..cc32e9e5b --- /dev/null +++ b/tests/models/records/record3.models.smt2 @@ -0,0 +1,12 @@ +(set-logic ALL) +(set-option :produce-models true) +(declare-datatype Pair +((pair (first Int) (second Int)))) +(declare-fun f (Int) Pair) +(declare-const x Int) +(declare-const y Int) +(assert (= (first (f x)) 5)) +(assert (= (first (f 0)) y)) +(assert (= x 0)) +(check-sat) +(get-model) diff --git a/tests/models/uf/uf1.models.expected b/tests/models/uf/uf1.models.expected index b3bca4e8f..2891baf56 100644 --- a/tests/models/uf/uf1.models.expected +++ b/tests/models/uf/uf1.models.expected @@ -1,7 +1,7 @@ unknown ( - (define-fun f ((arg_0 Int)) Int 0) + (define-fun f ((_arg_0 Int)) Int 0) (define-fun a () Int 0) (define-fun b () Int 0) ) diff --git a/tests/models/uf/uf2.models.expected b/tests/models/uf/uf2.models.expected index 3c1182254..ce06fd333 100644 --- a/tests/models/uf/uf2.models.expected +++ b/tests/models/uf/uf2.models.expected @@ -1,7 +1,7 @@ unknown ( - (define-fun f ((arg_0 Int)) Int (ite (= arg_0 0) 2 0)) + (define-fun f ((arg_0 Int)) Int (ite (= arg_0 (- 2)) 0 2)) (define-fun a () Int 0) (define-fun b () Int (- 2)) )