diff --git a/CHANGES.md b/CHANGES.md index e98ac2f9db..5ff1108fbf 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -155,6 +155,9 @@ * Require dolmen 0.9 #1050 * Test compatibility for OCaml 5.2 #1059 +### New features +* support for the SMT-LIB statement `get-value` + ## v2.5.2 ### Bug fixes diff --git a/src/bin/common/parse_command.ml b/src/bin/common/parse_command.ml index 1205979221..52522b996e 100644 --- a/src/bin/common/parse_command.ml +++ b/src/bin/common/parse_command.ml @@ -420,7 +420,7 @@ let mk_limit_opt age_bound fm_cross_limit timelimit_interpretation let mk_output_opt interpretation objectives_in_interpretation unsat_core - output_format model_type () () () () + output_format model_type () () () () () = set_infer_output_format (Option.is_none output_format); let output_format = match output_format with @@ -901,7 +901,7 @@ let parse_output_opt = (* Use the --interpretation and --produce-models (which is equivalent to --interpretation last) to determine the interpretation value. *) - let interpretation, dump_models, dump_models_on, frontend = + let interpretation, dump_models, dump_models_on, verify_models, frontend = let interpretation = let doc = Format.sprintf "Best effort support for counter-example generation. \ @@ -926,6 +926,7 @@ let parse_output_opt = Arg.(value & opt interpretation INone & info ["interpretation"] ~docv ~docs:s_models ~doc) in + let produce_models = let doc = "Enable model generation (equivalent to --interpretation last)." @@ -933,6 +934,13 @@ let parse_output_opt = Arg.(value & flag & info ["produce-models"] ~doc ~docs:s_models) in + let verify_models = + let doc = + "Verify generated models." + in + Arg.(value & flag & info ["verify-models"] ~doc ~docs:s_models) + in + let frontend = let doc = @@ -982,6 +990,7 @@ let parse_output_opt = ), dump_models, dump_models_on, + verify_models, frontend in @@ -1135,6 +1144,10 @@ let parse_output_opt = Term.(const Output.set_dump_models $ dump_models_on) in + let set_verify_models = + Term.(const set_verify_models $ verify_models) + in + let set_frontend = Term.(const ignore $ frontend) in @@ -1143,7 +1156,7 @@ let parse_output_opt = interpretation $ objectives_in_interpretation $ unsat_core $ output_format $ model_type $ - set_dump_models $ set_dump_models_on $ + set_dump_models $ set_dump_models_on $ set_verify_models $ set_sat_options $ set_frontend )) diff --git a/src/bin/common/solving_loop.ml b/src/bin/common/solving_loop.ml index a35411d7bd..c03e19d754 100644 --- a/src/bin/common/solving_loop.ml +++ b/src/bin/common/solving_loop.ml @@ -44,8 +44,6 @@ let is_solver_ctx_empty = function { ctx = []; local = []; global = [] } -> true | _ -> false -type 'a sat_module = (module Sat_solver_sig.S with type t = 'a) - let empty_solver_ctx = { ctx = []; local = []; @@ -99,6 +97,24 @@ let cmd_on_modes st modes cmd = Errors.forbidden_command curr_mode cmd | _ -> () +let verify_model ~get_value () = + match get_value [Expr.vrai] with + | Some [e] when Expr.equal e Expr.vrai -> () + + | Some [_] + | exception Sat_solver_util.Wrong_model _ + | exception Sat_solver_util.No_model -> + recoverable_error "The model is wrong" + + | None -> + (* The model generation is not enabled. *) + () + + | Some _ -> + (* The length of the output list is the same as the length of the + input list. *) + assert false + (* Dolmen util *) (** Adds the named terms of the statement [stmt] to the map accumulator [acc] *) @@ -117,7 +133,7 @@ let add_if_named acc (* We currently use the full state of the solver as model. *) -type model = Model : 'a sat_module * 'a -> model +type model = Model : 'a Sat_solver_util.sat_module * 'a -> model type solve_res = | Sat of model @@ -181,6 +197,12 @@ let process_source ?selector_inst ~print_status src = Fmt.pf (Options.Output.get_fmt_models ()) "%a@." FE.print_model partial_model end; + if Options.get_verify_models () then begin + let get_value = + Sat_solver_util.get_value (module SAT) partial_model + in + verify_model ~get_value () + end; Sat mdl end | `Unknown -> @@ -194,6 +216,12 @@ let process_source ?selector_inst ~print_status src = Fmt.pf (Options.Output.get_fmt_models ()) "%a@." FE.print_model partial_model end; + if Options.get_verify_models () then begin + let get_value = + Sat_solver_util.get_value (module SAT) partial_model + in + verify_model ~get_value () + end; Unknown (Some mdl) end | `Unsat -> Unsat @@ -209,7 +237,7 @@ let process_source ?selector_inst ~print_status src = in let partial_model_key: model option State.key = - State.create_key ~pipe:"" "sat_state" + State.create_key ~pipe:"" "partial_model" in let named_terms: DStd.Expr.term Util.MS.t State.key = @@ -511,6 +539,12 @@ let process_source ?selector_inst ~print_status src = | None -> print_wrn_opt ~name st_loc "integer" value; st | Some i -> set_steps_bound i st end + | ":verify-models", Symbol { name = Simple "true"; _ } -> + Options.set_verify_models true; + st + | ":verify-models", Symbol { name = Simple "false"; _ } -> + Options.set_verify_models false; + st | _ -> unsupported_opt name; st in @@ -632,45 +666,44 @@ let process_source ?selector_inst ~print_status src = unsupported_opt name in - (* Fetches the term value in the current model. *) - let evaluate_term get_value name 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) - [] - (Translate.dty_to_ty term.DStd.Expr.term_ty) + let dl_to_ael dloc_file (compact_loc: DStd.Loc.t) = + DStd.Loc.(lexing_positions (loc dloc_file compact_loc)) + in + + let handle_get_value loc ~get_value l = + let l = + List.map (Translate.mk_expr ~loc ~toplevel:false ~decl_kind:Daxiom) l in - match get_value simple_form with - | Some v -> Fmt.to_to_string Expr.print v - | None -> "unknown" - in - - let print_terms_assignments = - Fmt.list - ~sep:Fmt.cut - (fun fmt (name, v) -> Fmt.pf fmt "(%s %s)" name v) - in - - let handle_get_assignment ~get_value st = - let assignments = - Util.MS.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 - else - acc - ) - (State.get named_terms st) - [] + match get_value l with + | Some values -> + Printer.print_std + "(@[%a@])@," + Fmt.(iter ~sep:cut My_list.iter_pair + ((pair ~sep:sp Expr.pp_smtlib Expr.pp_smtlib) |> parens)) + (l, values) + | None -> + recoverable_error "No model produced, cannot execute get-value." + | exception Sat_solver_util.Wrong_model _ -> + recoverable_error "The model is wrong, cannot execute get-value." + | exception Sat_solver_util.No_model -> + recoverable_error "No model produced but it should, cannot execute get-value." + in + + let handle_get_assignment ~get_assignment st = + let names, l = + Util.MS.fold (fun name term (names, acc) -> + assert (DStd.Expr.Ty.equal term.DStd.Expr.term_ty DStd.Expr.Ty.bool); + name :: names, + Expr.mk_term (Sy.name name) [] + (Translate.dty_to_ty term.DStd.Expr.term_ty) :: acc + ) (State.get named_terms st) ([], []) in + let values = get_assignment l in Printer.print_std "(@[%a@])@," - print_terms_assignments - assignments + Fmt.(iter ~sep:cut My_list.iter_pair + ((pair ~sep:sp string Sat_solver_util.pp_lbool) |> parens)) + (names, values) in let handle_stmt : @@ -763,11 +796,12 @@ let process_source ?selector_inst ~print_status src = | {contents = `Get_model; _ } -> cmd_on_modes st [Sat] "get-model"; if Options.get_interpretation () then - let () = match State.get partial_model_key st with - | Some (Model ((module SAT), env)) -> + let () = + match State.get partial_model_key st with + | Some Model ((module SAT), partial_model) -> let module FE = Frontend.Make (SAT) in Fmt.pf (Options.Output.get_fmt_regular ()) "%a@." - FE.print_model env + FE.print_model partial_model | None -> (* TODO: add the location of the statement. *) recoverable_error "No model produced." @@ -811,9 +845,10 @@ let process_source ?selector_inst ~print_status src = match State.get partial_model_key st with | Some Model ((module SAT), partial_model) -> if DO.ProduceAssignment.get st then - handle_get_assignment - ~get_value:(SAT.get_value partial_model) - st + let get_assignment = + Sat_solver_util.get_assignment (module SAT) partial_model + in + handle_get_assignment ~get_assignment st else recoverable_error "Produce assignments disabled; \ @@ -826,6 +861,24 @@ let process_source ?selector_inst ~print_status src = st end + | {contents = `Get_value l; loc; _} -> + begin + cmd_on_modes st [Sat] "get-value"; + match State.get partial_model_key st with + | Some Model ((module SAT), partial_model) -> + let file = (State.get State.logic_file st).loc in + let loc = dl_to_ael file loc in + let get_value = + Sat_solver_util.get_value (module SAT) partial_model + in + handle_get_value loc ~get_value l; + st + | None -> + (* TODO: add the location of the statement. *) + recoverable_error "No model produced, cannot execute get-value."; + st + end + | {contents = `Other (custom, args); loc; _} -> handle_custom_statement loc custom args st diff --git a/src/lib/dune b/src/lib/dune index b160287515..a8706eceac 100644 --- a/src/lib/dune +++ b/src/lib/dune @@ -53,7 +53,8 @@ Instances IntervalCalculus Intervals_intf Intervals_core Intervals Ite_rel Matching Matching_types Polynome Records Records_rel Satml_frontend_hybrid Satml_frontend Satml Sat_solver Sat_solver_sig - Sig Sig_rel Theory Uf Use Domains Domains_intf Rel_utils Bitlist + Sig Sat_solver_util Sig_rel Theory Uf Use Domains Domains_intf + Rel_utils Bitlist ; structures Commands Errors Explanation Fpa_rounding Profiling Satml_types Symbols diff --git a/src/lib/frontend/frontend.ml b/src/lib/frontend/frontend.ml index 37690ba0ed..6494bbabe4 100644 --- a/src/lib/frontend/frontend.ml +++ b/src/lib/frontend/frontend.ml @@ -290,18 +290,19 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct }); Errors.run_error Errors.Failed_check_unsat_core with - | SAT.Unsat _ -> () - | (SAT.Sat | SAT.I_dont_know) as e -> raise e + | Sat_solver_sig.Unsat _ -> () + | (Sat_solver_sig.Sat | Sat_solver_sig.I_dont_know) as e -> raise e let mk_root_dep name f loc = 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) (name : Symbols.typed_name) + (env : env) : unit = ignore loc; match env.res with | `Sat | `Unknown -> - SAT.declare env.sat_env id + SAT.declare env.sat_env name | `Unsat -> () let internal_push ?(loc = Loc.dummy) (n : int) (env : env) : unit = @@ -415,11 +416,11 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct let handle_sat_exn f ?loc x env = try f ?loc x env with - | SAT.Sat -> env.res <- `Sat - | SAT.Unsat expl -> + | Sat_solver_sig.Sat -> env.res <- `Sat + | Sat_solver_sig.Unsat expl -> env.res <- `Unsat; env.expl <- Ex.union expl env.expl - | SAT.I_dont_know -> + | Sat_solver_sig.I_dont_know -> env.res <- `Unknown (* Wraps the function f to check if the step limit is reached (in which case, @@ -457,7 +458,7 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct (* If we have reached an unknown state, we can return it right away. *) match SAT.get_unknown_reason env.sat_env with - | Some (Step_limit _ | Timeout _) -> raise SAT.I_dont_know + | Some (Step_limit _ | Timeout _) -> raise Sat_solver_sig.I_dont_know | Some _ -> (* For now, only the step limit is an unknown step reachable here. We could raise SAT.I_dont_know as in the previous case, @@ -475,13 +476,13 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct | Optimize fn -> check_if_over (internal_optimize ~loc:d.st_loc fn) env with - | SAT.Sat -> + | Sat_solver_sig.Sat -> (* This case should mainly occur when a query has a non-unsat result, so we want to print the status in this case. *) hook_on_status (Sat d) (Steps.get_steps ()); env.res <- `Sat - | SAT.Unsat expl' -> + | Sat_solver_sig.Unsat expl' -> (* This case should mainly occur when a new assumption results in an unsat env, in which case we do not want to print status, since the correct status should be printed at the next query. *) @@ -491,7 +492,7 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct env.res <- `Unsat; env.expl <- expl - | SAT.I_dont_know -> + | Sat_solver_sig.I_dont_know -> (* TODO: always print Unknown for why3 ? *) let ur = SAT.get_unknown_reason env.sat_env in let status = diff --git a/src/lib/frontend/translate.ml b/src/lib/frontend/translate.ml index 0b3f5c8038..e8c03a8c69 100644 --- a/src/lib/frontend/translate.ml +++ b/src/lib/frontend/translate.ml @@ -23,7 +23,6 @@ module SE = E.Set module C = Commands module Sy = Symbols -module SM = Sy.Map module DE = DStd.Expr module DT = DE.Ty @@ -631,13 +630,13 @@ let mk_ty_decl (ty_c: DE.ty_cst) = 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 sy = + let name = begin match DStd.Tag.get tags DE.Tags.ac with - | Some () -> Sy.name ~kind:Sy.Ac name - | _ -> Sy.name name + | Some () -> Sy.Name.mk ~kind:Sy.Ac name + | _ -> Sy.Name.mk name end in - Cache.store_sy tcst sy; + Cache.store_sy tcst (Sy.Name name); (* Adding polymorphic types to the cache. *) Cache.store_ty_vars id_ty; let arg_tys, ret_ty = @@ -646,7 +645,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) + (name, arg_tys, ret_ty) (** Handles the definitions of a list of mutually recursive types. - If one of the types is an ADT, the ADTs that have only one case are diff --git a/src/lib/frontend/translate.mli b/src/lib/frontend/translate.mli index abb36451c9..af1bdefd42 100644 --- a/src/lib/frontend/translate.mli +++ b/src/lib/frontend/translate.mli @@ -39,6 +39,14 @@ val make_form : decl_kind:Expr.decl_kind -> Expr.t +val mk_expr : + ?loc:Loc.t -> + ?name_base:string -> + ?toplevel:bool -> + decl_kind:Expr.decl_kind -> + Dolmen.Std.Expr.term -> + Expr.t + val make : D_loop.DStd.Loc.file -> Commands.sat_tdecl list -> diff --git a/src/lib/reasoners/ccx.ml b/src/lib/reasoners/ccx.ml index 5d9f56787c..75e9d5857b 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_names:Symbols.typed_name list -> t -> Models.t end @@ -762,6 +762,6 @@ module Main : S = struct in Uf.term_repr env.uf t - let extract_concrete_model ~prop_model ~declared_ids env = - Uf.extract_concrete_model ~prop_model ~declared_ids env.uf + let extract_concrete_model ~prop_model ~declared_names env = + Uf.extract_concrete_model ~prop_model ~declared_names env.uf end diff --git a/src/lib/reasoners/ccx.mli b/src/lib/reasoners/ccx.mli index 83c09ed508..e8c9e40983 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_names:Symbols.typed_name list -> t -> Models.t end diff --git a/src/lib/reasoners/fun_sat.ml b/src/lib/reasoners/fun_sat.ml index 347ef6cc48..0789be3b48 100644 --- a/src/lib/reasoners/fun_sat.ml +++ b/src/lib/reasoners/fun_sat.ml @@ -178,9 +178,9 @@ 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; - (** Stack of the declared symbols by the user. The field [declare_top] + declare_top : Symbols.typed_name list ref; + declare_tail : Symbols.typed_name list Stack.t; + (** Stack of the declared names 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. *) } @@ -1131,8 +1131,10 @@ module Make (Th : Theory.S) = struct else begin try (* also performs case-split and pushes pending atoms to CS *) - let declared_ids = !(env.declare_top) in - let model, _ = Th.extract_concrete_model ~declared_ids env.tbox in + let declared_names = !(env.declare_top) in + let model, _ = + Th.extract_concrete_model ~declared_names env.tbox + in env.last_saved_model := Some model; env with Ex.Inconsistent (expl, classes) -> @@ -1616,8 +1618,8 @@ module Make (Th : Theory.S) = struct "solved with backward!"; raise e - let declare env id = - env.declare_top := id :: !(env.declare_top); + let declare env name = + env.declare_top := name :: !(env.declare_top); env let push env to_push = @@ -1852,20 +1854,8 @@ module Make (Th : Theory.S) = struct let get_unknown_reason env = env.unknown_reason - let get_value env t = - match E.type_info t with - | Ty.Tbool -> - begin - match ME.find_opt t env.gamma with - | None -> - begin - match ME.find_opt (E.neg t) env.gamma with - | None -> None - | Some _ -> Some E.faux - end - | Some _ -> Some E.vrai - end - | _ -> None + let get_boolean_model env = + ME.fold (fun e _ acc -> e :: acc) env.gamma [] let reinit_ctx () = (* all_models_sat_env := None; *) diff --git a/src/lib/reasoners/fun_sat.mli b/src/lib/reasoners/fun_sat.mli index 6e018f04e0..df0c76f769 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 -> Symbols.typed_name -> t val push : t -> int -> t @@ -58,9 +58,9 @@ module Make (_ : Theory.S) : sig val reinit_ctx : unit -> unit - val get_model: t -> Models.t option + val get_boolean_model : t -> Expr.t list - val get_unknown_reason : t -> Sat_solver_sig.unknown_reason option + val get_model : t -> Models.t option - val get_value : t -> Expr.t -> Expr.t option + val get_unknown_reason : t -> Sat_solver_sig.unknown_reason option end diff --git a/src/lib/reasoners/fun_sat_frontend.ml b/src/lib/reasoners/fun_sat_frontend.ml index af11bfcc86..8ac0053e38 100644 --- a/src/lib/reasoners/fun_sat_frontend.ml +++ b/src/lib/reasoners/fun_sat_frontend.ml @@ -20,9 +20,7 @@ let src = Logs.Src.create ~doc:"Sat" __MODULE__ module Log = (val Logs.src_log src : Logs.LOG) module Make (Th : Theory.S) : Sat_solver_sig.S = struct - exception Sat - exception Unsat of Explanation.t - exception I_dont_know + open Sat_solver_sig module FS = Fun_sat.Make(Th) @@ -61,14 +59,16 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct let reinit_ctx = FS.reinit_ctx + let get_boolean_model t = FS.get_boolean_model !t + let get_model t = FS.get_model !t let get_unknown_reason t = FS.get_unknown_reason !t - let get_value t expr = FS.get_value !t expr - let get_objectives _env = raise (Util.Not_implemented "optimization is not supported by FunSAT.") let supports_optimization = false + + let reset_decisions _env = () end diff --git a/src/lib/reasoners/sat_solver_sig.ml b/src/lib/reasoners/sat_solver_sig.ml index c8450e6d34..be7cf56fc1 100644 --- a/src/lib/reasoners/sat_solver_sig.ml +++ b/src/lib/reasoners/sat_solver_sig.ml @@ -62,24 +62,24 @@ let pp_ae_unknown_reason_opt ppf = function | Some Step_limit i -> Fmt.pf ppf "StepLimit:%i" i | Some Timeout t -> Fmt.pf ppf "Timeout:%a" pp_ae_timeout_reason t +exception Sat +exception Unsat of Explanation.t +exception I_dont_know + module type S = sig type t - exception Sat - exception Unsat of Explanation.t - exception I_dont_know - val empty : ?selector:(Expr.t -> bool) -> unit -> t (** [empty ~selector ()] creates an empty environment. The optional argument [selector] is used to filter ground facts discovered by the instantiation engine. *) - val declare : t -> Id.typed -> unit - (** [declare env id] declares a new identifier [id]. + val declare : t -> Symbols.typed_name -> unit + (** [declare env name] declares a new typed name [name]. If the environment [env] isn't unsatisfiable and the model generation - is enabled, the solver produces a model term for [id] which can be + is enabled, the solver produces a model term for [name] which can be retrieved with [get_model]. *) val push : t -> int -> unit @@ -130,7 +130,9 @@ module type S = sig val reinit_ctx : unit -> unit (** [reinit_ctx ()] reinitializes the solving context. *) - val get_model: t -> Models.t option + val get_boolean_model : t -> Expr.t list + + val get_model : t -> Models.t option (** [get_model t] produces the current first-order model. Notice that this model is a best-effort. @@ -141,10 +143,6 @@ module type S = sig (** [get_unknown_reason t] returns the reason Alt-Ergo raised [I_dont_know] if it did. If it did not, returns [None]. *) - val get_value : t -> Expr.t -> Expr.t option - (** [get_value t e] returns the value of [e] as a constant expression - in the current model generated. Returns [None] if can't decide. *) - val get_objectives : t -> Objective.Model.t option (** [get_objectives t] returns the current objective values. @@ -153,8 +151,9 @@ module type S = sig val supports_optimization : bool (** Returns whether the solver supports optimization. *) -end + val reset_decisions : t -> unit +end module type SatContainer = sig val src : Logs.src diff --git a/src/lib/reasoners/sat_solver_sig.mli b/src/lib/reasoners/sat_solver_sig.mli index 9380bbbbce..cea4f408a5 100644 --- a/src/lib/reasoners/sat_solver_sig.mli +++ b/src/lib/reasoners/sat_solver_sig.mli @@ -42,24 +42,24 @@ val pp_smt_unknown_reason: unknown_reason Fmt.t val pp_ae_unknown_reason_opt : unknown_reason option Fmt.t (** Prints an optional unknown reason in Alt-Ergo format. *) +exception Sat +exception Unsat of Explanation.t +exception I_dont_know + module type S = sig type t - exception Sat - exception Unsat of Explanation.t - exception I_dont_know - val empty : ?selector:(Expr.t -> bool) -> unit -> t (** [empty ~selector ()] creates an empty environment. The optional argument [selector] is used to filter ground facts discovered by the instantiation engine. *) - val declare : t -> Id.typed -> unit - (** [declare env id] declares a new identifier [id]. + val declare : t -> Symbols.typed_name -> unit + (** [declare env name] declares a new typed name [name]. If the environment [env] isn't unsatisfiable and the model generation - is enabled, the solver produces a model term for [id] which can be + is enabled, the solver produces a model term for [name] which can be retrieved with [get_model]. *) val push : t -> int -> unit @@ -110,7 +110,11 @@ module type S = sig val reinit_ctx : unit -> unit (** [reinit_ctx ()] reinitializes the solving context. *) - val get_model: t -> Models.t option + val get_boolean_model : t -> Expr.t list + (** [get_boolean_model env] returns the list of literals assigned by + the solver [env]. *) + + val get_model : t -> Models.t option (** [get_model t] produces the current first-order model. Notice that this model is a best-effort. @@ -121,10 +125,6 @@ module type S = sig (** [get_unknown_reason t] returns the reason Alt-Ergo raised [I_dont_know] if it did. If it did not, returns [None]. *) - val get_value : t -> Expr.t -> Expr.t option - (** [get_value t e] returns the value of [e] as a constant expression - in the current model generated. Returns [None] if can't decide. *) - val get_objectives : t -> Objective.Model.t option (** [get_objectives t] returns the current objective values. @@ -133,8 +133,10 @@ module type S = sig val supports_optimization : bool (** Returns whether the solver supports optimization. *) -end + val reset_decisions : t -> unit + (** [reset_decisions t] cancels all the decisions made by the solver [env]. *) +end module type SatContainer = sig val src : Logs.src diff --git a/src/lib/reasoners/sat_solver_util.ml b/src/lib/reasoners/sat_solver_util.ml new file mode 100644 index 0000000000..10128a05dd --- /dev/null +++ b/src/lib/reasoners/sat_solver_util.ml @@ -0,0 +1,225 @@ +(**************************************************************************) +(* *) +(* 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/ *) +(* *) +(**************************************************************************) + +module type S = Sat_solver_sig.S + +type 'a sat_module = (module S with type t = 'a) +type any_sat_module = (module S) + +type lbool = False | True | Unknown + +let pp_lbool ppf b = + match b with + | False -> Fmt.pf ppf "false" + | True -> Fmt.pf ppf "true" + | Unknown -> Fmt.pf ppf "unknown" + +open Sat_solver_sig + +let internal_assume (type a) (module SAT : S with type t = a) env id e = + SAT.assume env + {Expr.ff= e; + origin_name = id; + gdist = -1; + hdist = 0; + trigger_depth = max_int; + nb_reductions = 0; + age=0; + lem=None; + mf=true; + gf=false; + from_terms = []; + theory_elim = true; + } + Explanation.empty + +let check (type a) (module SAT : S with type t = a) env = + try + let ex = SAT.unsat env + {Expr.ff=Expr.vrai; + origin_name = ""; + hdist = -1; + gdist = 0; + trigger_depth = max_int; + nb_reductions = 0; + age=0; + lem=None; + mf=true; + gf=true; + from_terms = []; + theory_elim = true; + } + in + raise_notrace (Unsat ex) + with + | I_dont_know | Sat -> () + +exception Wrong_model of Explanation.t +exception No_model + +(* Assert the last computed model in the environment [env]. + + @raise Wrong_model if the solver found a contradiction, which means the model + is wrong. *) +let assert_model (type a) (module SAT : S with type t = a) env mdl = + try + ModelMap.iter + (fun ({ hs; _ } as name, _, ret_ty) graph -> + ModelMap.Graph.iter + (fun val_args val_ret -> + let e = Expr.mk_app name val_args ret_ty in + let iff = match ret_ty with Ty.Tbool -> true | _ -> false in + let eq = Expr.mk_eq ~iff e val_ret in + internal_assume (module SAT) env (Hstring.view hs) eq + ) + graph + ) + mdl.Models.model; + check (module SAT) env + with Unsat ex -> raise_notrace (Wrong_model ex) + +(* [get_value_in_boolean_model bmdl e] retrieves the assignment of the boolean + expression [e] in the boolean model [bmdl]. + + @return [None] if the formula [e] hasn't been assigned by the SAT solver. *) +let get_value_in_boolean_model bmdl e = + match Expr.type_info e with + | Ty.Tbool -> + begin + Compat.List.find_map + (fun lit -> + if Expr.equal e lit then + Some true + else if Expr.equal e (Expr.neg lit) then + Some false + else + None + ) + bmdl + end + | _ -> invalid_arg "get_value_in_boolean_model" + +(* [get_value_in_model mdl bmdl e] tries to retrieve the value of the expression + [e] in the first-order model [mdl]. For boolean expressions, we retrieve + their value in the boolean model [bmdl]. *) +let get_value_in_model mdl bmdl e = + let { Expr.f; xs; ty; _ } = Expr.term_view e in + match f, ty with + | _, Ty.Tbool -> + (* Values of boolean expressions are decided by the SAT solver. *) + Option.map Expr.Core.of_bool @@ + get_value_in_boolean_model bmdl e + + | Symbols.Name name, _ -> + let arg_tys = List.map Expr.type_info xs in + let typed_name = (name, arg_tys, ty) in + ModelMap.get_value typed_name xs mdl.Models.model + | _ -> None + +let (let*) = Option.bind + +let get_value (type a) (module SAT : S with type t = a) env l = + let* mdl = SAT.get_model env in + (* HOTFIX for SatML: we can assert new formula in [env.satml] only at the + level of decision [0]. After performing [unsat], the decision level isn't + necessary [0] and the SMT statement `get-value` can be called only in + SAT mode, so we have to reset all the decisions of the solver here. + Before resetting the decisions, we save the boolean model for sake + of optimization. + + See issue: https://github.com/OCamlPro/alt-ergo/issues/1063 *) + let bmdl = SAT.get_boolean_model env in + SAT.reset_decisions env; + assert_model (module SAT) env mdl; + (* First, we attempt to retrieve each model term in the last computed + boolean and first-order models. + + If we don't find the model term for an expression of [l], we assert a + new equation to force the solver to produce a model term for this + expression. *) + let l = + List.map + (fun e -> + match get_value_in_model mdl bmdl e with + | Some v -> Either.Left v + | None -> + (* For each expression [e] of the list [l], we assert an equality + of the form [n = e] where [n] is a fresh name. *) + let ty = Expr.type_info e in + let id = Id.Namespace.GetValue.fresh () in + let sy = Symbols.name ~ns:GetValue id in + let name = Expr.mk_term sy [] ty in + let iff = match ty with Ty.Tbool -> true | _ -> false in + let t = Expr.mk_eq ~iff name e in + let () = + let { Expr.f; ty; _ } = Expr.term_view name in + match f with + | Symbols.Name name -> + SAT.declare env (name, [], ty) + | _ -> assert false + in + internal_assume (module SAT) env id t; + Either.Right name + ) l + in + (* We have to check the satisfability of the new environment [env] in order + to produce a new model. If this call raise [Unsat], the model is wrong + and we cannot produce model terms for the expressions of [l]. *) + try + check (module SAT) env; + let* mdl = SAT.get_model env in + let bmdl = SAT.get_boolean_model env in + let values = + List.map + (fun v -> + match v with + | Either.Left v -> v + | Either.Right name -> + match get_value_in_model mdl bmdl name with + | Some v -> v + | None -> + (* The model generation has to produce a value for each + declared names. If some declared names are missing in the + model, it's a bug. *) + assert false + ) l + in + Some values + with Unsat ex -> raise_notrace (Wrong_model ex) + +let get_assignment (type a) (module SAT : S with type t = a) env = + let bmdl = SAT.get_boolean_model env in + List.map + (fun e -> + match get_value_in_boolean_model bmdl e with + | Some true -> True + | Some false -> False + | None -> Unknown + ) diff --git a/src/lib/reasoners/sat_solver_util.mli b/src/lib/reasoners/sat_solver_util.mli new file mode 100644 index 0000000000..33313f779a --- /dev/null +++ b/src/lib/reasoners/sat_solver_util.mli @@ -0,0 +1,61 @@ +(**************************************************************************) +(* *) +(* 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 'a sat_module = (module Sat_solver_sig.S with type t = 'a) + +type any_sat_module = (module Sat_solver_sig.S) + +type lbool = False | True | Unknown + +val pp_lbool : lbool Fmt.t + +exception Wrong_model of Explanation.t +exception No_model + +val get_value : 'a sat_module -> 'a -> Expr.t list -> Expr.t list option +(** [get_value (module SAT) env l] returns the model values of the expressions + of [l] in the current generated model of [env]. + + @return [None] if the model generation is not enabled or the + environment is already unsatisfiable before calling this function. + @raise Wrong_model if the solver found a contradiction in the current + model. + @raise No_model if the solver didn't produce a model but the model + generation is enabled. *) + +val get_assignment : 'a sat_module -> 'a -> Expr.t list -> lbool list +(** [get_assignment (module SAT) env l] returns the status of the literals [l] + in the current boolean model of [env]. + + The status is [unknown] if the literal isn't a subformula of the user + input. + + @raise invalid_argument if one of the expressions of [l] isn't a + literal. *) diff --git a/src/lib/reasoners/satml.ml b/src/lib/reasoners/satml.ml index cd061c17c9..5fd3a07538 100644 --- a/src/lib/reasoners/satml.ml +++ b/src/lib/reasoners/satml.ml @@ -91,8 +91,9 @@ module type SAT_ML = sig type t val solve : t -> unit + val compute_concrete_model : - declared_ids:Id.typed list -> + declared_names:Symbols.typed_name list -> t -> Models.t Lazy.t * Objective.Model.t @@ -1925,23 +1926,23 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct (* check_unsat_core cl; *) raise e - let rec compute_concrete_model ~declared_ids env = + let rec compute_concrete_model env ~declared_names = let acts = theory_slice env in match Th.compute_concrete_model ~acts env.tenv with | () -> ( if is_sat env then - Th.extract_concrete_model ~declared_ids env.tenv + Th.extract_concrete_model env.tenv ~declared_names else try solve env; assert false with Sat -> - compute_concrete_model ~declared_ids env + compute_concrete_model env ~declared_names ) | exception Ex.Inconsistent (ex, _) -> conflict_analyze_and_fix env (C_theory ex); - compute_concrete_model ~declared_ids env + compute_concrete_model env ~declared_names - let compute_concrete_model ~declared_ids env = + let compute_concrete_model ~declared_names env = assert (is_sat env); (* Make sure all objectives are optimized before starting model @@ -1955,7 +1956,7 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct try solve env; assert false with Sat -> loop env else - compute_concrete_model ~declared_ids env + compute_concrete_model ~declared_names env in loop env exception Trivial diff --git a/src/lib/reasoners/satml.mli b/src/lib/reasoners/satml.mli index 166b2ff5a7..4e4c3a3512 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_names:Symbols.typed_name 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..e4edc61781 100644 --- a/src/lib/reasoners/satml_frontend.ml +++ b/src/lib/reasoners/satml_frontend.ml @@ -31,6 +31,7 @@ let src = Logs.Src.create ~doc:"Sat" __MODULE__ module Log = (val Logs.src_log src : Logs.LOG) module Make (Th : Theory.S) : Sat_solver_sig.S = struct + open Sat_solver_sig module SAT = Satml.Make(Th) module Inst = Instances.Make(Th) module Ex = Explanation @@ -68,11 +69,11 @@ 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; - (** 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. *) + mutable declare_top : Symbols.typed_name list; + declare_tail : Symbols.typed_name list Stack.t; + (** Stack of the declared names 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. *) } let empty_guards () = { @@ -89,7 +90,7 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct let ff_hcons_env = FF.empty_hcons_env () in { gamma = ME.empty; satml = SAT.create (FF.atom_hcons_env ff_hcons_env); - ff_hcons_env ; + ff_hcons_env = FF.empty_hcons_env (); nb_mrounds = 0; last_forced_normal = 0; last_forced_greedy = 0; @@ -108,10 +109,6 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct declare_tail = Stack.create (); } - exception Sat - exception Unsat of Explanation.t - exception I_dont_know - let i_dont_know env ur = env.unknown_reason <- Some ur; raise I_dont_know @@ -1008,9 +1005,9 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct if compute then begin try (* also performs case-split and pushes pending atoms to CS *) - let declared_ids = env.declare_top in + let declared_names = env.declare_top in let model, objectives = - SAT.compute_concrete_model ~declared_ids env.satml + SAT.compute_concrete_model ~declared_names env.satml in env.last_saved_model <- Some model; env.last_saved_objectives <- Some objectives; @@ -1169,7 +1166,8 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct | Satml.Sat -> try do_case_split env Util.BeforeMatching; - may_update_last_saved_model env (Options.get_every_interpretation ()); + may_update_last_saved_model env + (Options.get_every_interpretation ()); let () = env.nb_mrounds <- env.nb_mrounds + 1 [@ocaml.ppwarning @@ -1383,30 +1381,18 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct let optimize env fn = SAT.optimize env.satml fn + let get_boolean_model env = + List.filter_map (fun Atom.{ lit; _ } -> + match Shostak.Literal.view lit with + | Literal.LTerm e -> Some e + | LSem _ -> None + ) (SAT.boolean_model env.satml) + let get_model env = Option.map Lazy.force env.last_saved_model let get_unknown_reason env = env.unknown_reason - let get_value env t = - match E.type_info t with - | Ty.Tbool -> - begin - let bmodel = SAT.boolean_model env.satml 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 - Some E.faux - else - None - ) - bmodel - end - | _ -> None - let get_objectives env = env.last_saved_objectives let supports_optimization = true @@ -1427,6 +1413,8 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct Shostak.Combine.reinit_cache (); Uf.reinit_cache () + let reset_decisions env = SAT.cancel_until env.satml 0 + let () = Steps.save_steps (); Var.save_cnt (); diff --git a/src/lib/reasoners/theory.ml b/src/lib/reasoners/theory.ml index ad9ad7962a..2a544c01b9 100644 --- a/src/lib/reasoners/theory.ml +++ b/src/lib/reasoners/theory.ml @@ -68,8 +68,8 @@ 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 -> t -> + declared_names:Symbols.typed_name list -> Models.t Lazy.t * Objective.Model.t val assume_th_elt : t -> Expr.th_elt -> Explanation.t -> t @@ -890,14 +890,14 @@ module Main_Default : S = struct | None -> () - let extract_concrete_model ~declared_ids env = + let extract_concrete_model env ~declared_names = let { gamma_finite; assumed_set; objectives; _ }, _ = do_case_split_aux env ~for_model:true in lazy ( CC_X.extract_concrete_model ~prop_model:assumed_set - ~declared_ids + ~declared_names gamma_finite ), objectives @@ -952,7 +952,7 @@ module Main_Empty : S = struct let do_case_split ?acts:_ env _ = env, E.Set.empty let add_term env _ ~add_in_cs:_ = env let compute_concrete_model ~acts:_ _env = () - let extract_concrete_model ~declared_ids:_ _env = + let extract_concrete_model _env ~declared_names:_ = lazy Models.empty, Objective.Model.empty let assume_th_elt e _ _ = e diff --git a/src/lib/reasoners/theory.mli b/src/lib/reasoners/theory.mli index f8c4e115d3..1f4570d861 100644 --- a/src/lib/reasoners/theory.mli +++ b/src/lib/reasoners/theory.mli @@ -59,8 +59,8 @@ 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 -> t -> + declared_names:Symbols.typed_name list -> Models.t Lazy.t * Objective.Model.t val assume_th_elt : t -> Expr.th_elt -> Explanation.t -> t diff --git a/src/lib/reasoners/uf.ml b/src/lib/reasoners/uf.ml index 4049634cfa..2e2d9c2a6a 100644 --- a/src/lib/reasoners/uf.ml +++ b/src/lib/reasoners/uf.ml @@ -1228,7 +1228,7 @@ let compute_concrete_model_of_val cache = acc end - | Sy.Name { hs = id; _ }, _, _ -> + | Sy.Name name, _, _ -> let value = match ty with | Ty.Text _ -> @@ -1238,7 +1238,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 (name, arg_tys, ty) arg_vals value mdl), mrepr | _ -> Printer.print_err @@ -1250,11 +1250,11 @@ let compute_concrete_model_of_val cache = 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 ~declared_ids env -> + in fun ~prop_model ~declared_names 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 declared_ids, ME.empty) + terms (ModelMap.empty ~suspicious declared_names, ME.empty) in let model = E.Table.fold (fun t vals mdl -> @@ -1267,11 +1267,11 @@ let extract_concrete_model cache = Expr.ArraysEx.store arr_val i v ) vals abstract in - let id, is_user = + let name, is_user = 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 ({ ns = User; _ } as name) -> name, true + | Sy.Name name -> name, false | _ -> (* We only store array declarations as keys in the cache [array_selects]. *) @@ -1279,7 +1279,7 @@ let extract_concrete_model cache = in let mdl = if is_user then - ModelMap.add (id, [], ty) [] arr_val mdl + ModelMap.add (name, [], 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 @@ -1287,18 +1287,18 @@ let extract_concrete_model cache = 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 + occurrences of the array identifier [name] 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 + ModelMap.subst name arr_val mdl ) cache.array_selects model in { Models.propositional = prop_model; model; term_values = mrepr } -let extract_concrete_model ~prop_model ~declared_ids = +let extract_concrete_model ~prop_model ~declared_names = let cache : cache = { array_selects = E.Table.create 17; abstracts = Shostak.HX.create 17; } - in fun env -> extract_concrete_model cache ~prop_model ~declared_ids env + in fun env -> extract_concrete_model cache ~prop_model ~declared_names env diff --git a/src/lib/reasoners/uf.mli b/src/lib/reasoners/uf.mli index f73f3f7942..5297d1d39b 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_names:Symbols.typed_name list -> t -> Models.t diff --git a/src/lib/structures/commands.ml b/src/lib/structures/commands.ml index 45b8dcaf8b..6a16707bb7 100644 --- a/src/lib/structures/commands.ml +++ b/src/lib/structures/commands.ml @@ -31,7 +31,7 @@ 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 + | Decl of Symbols.typed_name | Assume of string * Expr.t * bool | PredDef of Expr.t * string (*name of the predicate*) | Optimize of Objective.Function.t @@ -46,11 +46,8 @@ type sat_tdecl = { } let print_aux fmt = function - | Decl (id, arg_tys, ret_ty) -> - Fmt.pf fmt "declare %a with type (%a) -> %a" - Id.pp id - Fmt.(list ~sep:comma Ty.print) arg_tys - Ty.print ret_ty + | Decl tn -> + Fmt.pf fmt "declare %a" Symbols.pp_typed_name tn | Assume (name, e, b) -> Format.fprintf fmt "assume %s(%b): @[%a@]" name b Expr.print e diff --git a/src/lib/structures/commands.mli b/src/lib/structures/commands.mli index 06eb89001d..26e0bcb35b 100644 --- a/src/lib/structures/commands.mli +++ b/src/lib/structures/commands.mli @@ -28,7 +28,7 @@ (* Sat entry *) type sat_decl_aux = - | Decl of Id.typed + | Decl of Symbols.typed_name | Assume of string * Expr.t * bool | PredDef of Expr.t * string (*name of the predicate*) | Optimize of Objective.Function.t diff --git a/src/lib/structures/errors.ml b/src/lib/structures/errors.ml index 38f6028fd8..445b0db884 100644 --- a/src/lib/structures/errors.ml +++ b/src/lib/structures/errors.ml @@ -44,7 +44,7 @@ type mode_error = | Forbidden_command of string type model_error = - | Subst_type_clash of Id.t * Ty.t * Ty.t + | Subst_type_clash of Symbols.Name.t * Ty.t * Ty.t | Subst_not_model_term of Expr.t type error = @@ -102,11 +102,11 @@ let report_mode_error fmt = function fprintf fmt "Command %s" s let report_model_error ppf = function - | Subst_type_clash (id, ty1, ty2) -> + | Subst_type_clash (name, ty1, ty2) -> Fmt.pf ppf - "Cannot substitute the identifier %a of type %a by an expression of \ + "Cannot substitute the name %a of type %a by an expression of \ type %a" - Id.pp id + Symbols.Name.pp name Ty.pp_smtlib ty1 Ty.pp_smtlib ty2 diff --git a/src/lib/structures/errors.mli b/src/lib/structures/errors.mli index 95e9ceddec..babe286092 100644 --- a/src/lib/structures/errors.mli +++ b/src/lib/structures/errors.mli @@ -53,7 +53,7 @@ type mode_error = (** Errors raised while using models. *) type model_error = - | Subst_type_clash of Id.t * Ty.t * Ty.t + | Subst_type_clash of Symbols.Name.t * Ty.t * Ty.t | Subst_not_model_term of Expr.t (** All types of error that can be raised *) diff --git a/src/lib/structures/expr.ml b/src/lib/structures/expr.ml index 3c5313c7d7..f9f860cc3a 100644 --- a/src/lib/structures/expr.ml +++ b/src/lib/structures/expr.ml @@ -952,6 +952,8 @@ let mk_term s l ty = neg.neg <- Some pos; pos +let mk_app name l ty = mk_term (Symbols.Name name) l ty + let vrai = let res = let nb_nodes = 0 in @@ -2904,6 +2906,7 @@ module Core = struct let and_ s t = mk_and s t false let or_ s t = mk_or s t false let ite c t e = mk_ite c t e + let of_bool b = if b then vrai else faux end (** Constructors from the smtlib theory of integers. diff --git a/src/lib/structures/expr.mli b/src/lib/structures/expr.mli index bb04604491..43577581d9 100644 --- a/src/lib/structures/expr.mli +++ b/src/lib/structures/expr.mli @@ -246,6 +246,7 @@ val print_tagged_classes : Format.formatter -> Set.t list -> unit val mk_trigger : ?user:bool -> ?depth:int -> ?hyp:t list -> t list -> trigger val mk_term : Symbols.t -> t list -> Ty.t -> t +val mk_app : Symbols.Name.t -> t list -> Ty.t -> t val vrai : t val faux : t val void : t @@ -455,16 +456,12 @@ val reinit_cache: unit -> unit https://smtlib.cs.uiowa.edu/theories-Core.shtml *) module Core : sig val not : t -> t - val eq : t -> t -> t - val xor : t -> t -> t - val and_ : t -> t -> t - val or_ : t -> t -> t - val ite : t -> t -> t -> t + val of_bool : bool -> t end (** Constructors from the smtlib theory of integers. diff --git a/src/lib/structures/id.ml b/src/lib/structures/id.ml index b8666d20a0..08c4c154a2 100644 --- a/src/lib/structures/id.ml +++ b/src/lib/structures/id.ml @@ -18,15 +18,13 @@ type t = Hstring.t [@@deriving ord] -type typed = t * Ty.t list * Ty.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 +let show id = Fmt.to_to_string pp id module Namespace = struct module type S = sig @@ -53,8 +51,11 @@ module Namespace = struct module Abstract = Make () + module GetValue = Make () + let reinit () = Internal.reset_fresh_cpt (); Skolem.reset_fresh_cpt (); - Abstract.reset_fresh_cpt () + Abstract.reset_fresh_cpt (); + GetValue.reset_fresh_cpt () end diff --git a/src/lib/structures/id.mli b/src/lib/structures/id.mli index 5666a0a8a4..f6e057f003 100644 --- a/src/lib/structures/id.mli +++ b/src/lib/structures/id.mli @@ -17,14 +17,6 @@ (**************************************************************************) type t = Hstring.t [@@deriving ord] - -type typed = t * Ty.t list * Ty.t -(** Typed identifier of function. In order: - - The identifier. - - Types of its arguments. - - The returned type. *) - -val compare_typed : typed -> typed -> int val equal : t -> t -> bool val show : t -> string val pp : t Fmt.t @@ -37,6 +29,7 @@ module Namespace : sig module Internal : S module Skolem : S module Abstract : S + module GetValue : S val reinit : unit -> unit (** Resets the [fresh_internal_name], [fresh_skolem] and [fresh_abstract] diff --git a/src/lib/structures/modelMap.ml b/src/lib/structures/modelMap.ml index 47df05ccbe..0da7b25ddf 100644 --- a/src/lib/structures/modelMap.ml +++ b/src/lib/structures/modelMap.ml @@ -32,12 +32,24 @@ module M: Map.S with type key = Expr.t list = Map.Make As functions in the SMT-LIB standard are total, one of the expressions [e] above is used as the default value of the function. *) module Constraints = struct - - type t = Expr.t M.t - let empty = M.empty let add = M.add let map = M.map + let iter = M.iter + let find_opt = M.find_opt + + (* Check if the graph defined by the set of constraints [c] is constant. + Requires that [c] isn't empty. *) + let is_constant c = + assert (not @@ M.is_empty c); + try + let _, t = M.choose c in + M.iter + (fun _args_val ret_val -> + if not @@ Expr.equal ret_val t then raise Exit + ) c; + true + with Exit -> false (* 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]. @@ -105,36 +117,68 @@ module Constraints = struct aux ppf (Expr.Map.to_seq c) end -module P = Map.Make - (struct - type t = Id.typed +module P = struct + include Map.Make + (struct + type t = Sy.typed_name - let compare = Id.compare_typed - end) + let compare = Sy.compare_typed_name + end) + + let iter f = + iter (fun (({ ns; _ }, _, _) as tn) v -> + match ns with + | User -> f tn v + | _ -> ()) +end + +module Graph = struct + type t = + | Free of Expr.t + (* Represents a graph without any constraint. The expression is + an abstract value. *) -type graph = - | Free of Expr.t - (* Represents a graph without any constraint. The expression is - an abstract value. *) + | C of Expr.t M.t - | C of Constraints.t + let is_constant graph = + match graph with + | Free _ -> true + | C constraints -> Constraints.is_constant constraints + + let iter f graph = + match graph with + | Free _ -> () + | C constraints -> Constraints.iter f constraints + + let find_opt arg_vals graph = + match graph with + | Free _ -> None + | C constraints -> Constraints.find_opt arg_vals constraints + + let pp ppf graph = + match graph with + | Free a -> Expr.pp_smtlib ppf a + | C constraints -> + let inverse_rel = Constraints.inverse constraints in + Constraints.pp_inverse ppf inverse_rel +end type t = { - values : graph P.t; + values : Graph.t P.t; suspicious : bool; } -let add ((id, arg_tys, _) as sy) arg_vals ret_val { values; suspicious } = +let add ((name, 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" Symbols.Name.pp name; let constraints = match P.find sy values with | C g -> g | Free _ | exception Not_found -> Constraints.empty in let values = - P.add sy (C (Constraints.add arg_vals ret_val constraints)) values + P.add sy (Graph.C (Constraints.add arg_vals ret_val constraints)) values in { values; suspicious } @@ -144,40 +188,47 @@ let find k {values; _ } = let fold f {values;_} acc = P.fold f values acc +let iter f { values; _ } = P.iter f values + +let get_value id arg_vals { values; _ } = + Option.bind (P.find_opt id values) @@ Graph.find_opt arg_vals + let empty ~suspicious declared_ids = let values = List.fold_left (fun values ((_, _, ret_ty) as sy) -> - P.add sy (Free (Expr.mk_abstract ret_ty)) values + P.add sy (Graph.Free (Expr.mk_abstract ret_ty)) values ) P.empty declared_ids in { values; suspicious } -let rec subst_in_term id e c = +let rec subst_in_term name 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 name', [] when Symbols.Name.equal name name' -> let ty = Expr.type_info e in if not @@ Ty.equal ty ty' then - Errors.error (Model_error (Subst_type_clash (id, ty', ty))); + raise (Errors.Error (Model_error (Subst_type_clash (name, ty', ty)))); e | _ -> begin - let xs = List.map (subst_in_term id e) xs in + let xs = List.map (subst_in_term name e) xs in Expr.mk_term f xs ty' end -let subst id e { values; suspicious } = +let subst name e { values; suspicious } = if not @@ Expr.is_model_term e then - Errors.error (Model_error (Subst_not_model_term e)); + raise (Errors.Error (Model_error (Subst_not_model_term e))); let values = P.map (fun graph -> match graph with - | C constraints -> C (Constraints.map (subst_in_term id e) constraints) - | Free _ -> graph + | Graph.C constraints -> + Graph.C (Constraints.map (subst_in_term name e) constraints) + | Free a -> + Free (subst_in_term name e a) ) values in { values; suspicious } @@ -185,23 +236,14 @@ 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 ~is_constant pp ppf ((id, arg_tys, ret_ty), a) = +let pp_define_fun ppf ((name, arg_tys, ret_ty), graph) = + let unused = Graph.is_constant graph 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 + Symbols.Name.pp name + Fmt.(list ~sep:sp (pp_named_arg_ty ~unused)) named_arg_tys Ty.pp_smtlib ret_ty - pp a - -let pp_define_fun ppf (sy, graph) = - match graph with - | Free a -> - pp_define_fun ~is_constant:true Expr.pp_smtlib ppf (sy, a) - - | C constraints -> - let inverse_rel = Constraints.inverse constraints in - let is_constant = Expr.Map.cardinal inverse_rel = 1 in - pp_define_fun ~is_constant Constraints.pp_inverse ppf (sy, inverse_rel) + Graph.pp graph let pp ppf {values; suspicious} = if suspicious then begin diff --git a/src/lib/structures/modelMap.mli b/src/lib/structures/modelMap.mli index f3bc5406ef..775d10326a 100644 --- a/src/lib/structures/modelMap.mli +++ b/src/lib/structures/modelMap.mli @@ -18,34 +18,64 @@ module M: Map.S with type key = Expr.t list -type graph = - | Free of Expr.t - (* Represents a graph without any constraint. The expression is - an abstract value. *) - - | C of Expr.t M.t - type t (** Type of model. *) -val add : Id.typed -> Expr.t list -> Expr.t -> t -> t +(** Representation of a value in the model by a finite set of constraints. + + More precisely, the value of a name [f] will be represented by a + finite set of constraint of the form: + f(a1, ..., an) = b + where a1,...,an,b are model term in the sense of [Expr.is_model_term]. *) +module Graph : sig + type t + (** Type of graph. *) + + val is_constant : t -> bool + (** [is_constant graph] checks if the graph [graph] represents a + constant function. *) + + val iter : (Expr.t list -> Expr.t -> unit) -> t -> unit + (** [iter f graph] iterates on the constraints of the [graph], that is on + couples of the form ((a1, ..., an), b) such that the function [f] + represented by [graph] has to satisfied [f(a1, ..., an) = b]. *) + + val pp : t Fmt.t + (** [pp ppf graph] prints the graph [graph] on the formatter [ppf] + using the SMT-LIB format. + + As functions are total in the SMT-LIB standard, one of the rhs in the + constraints of [graph] is choosen to complete its definition. *) +end + +val add : Symbols.typed_name -> 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 empty : suspicious:bool -> Id.typed list -> t +val iter : (Symbols.typed_name -> Graph.t -> unit) -> t -> unit +(** [iter f mdl] iterates over all the graphs of the model [mdl]. *) + +val get_value : Symbols.typed_name -> Expr.t list -> t -> Expr.t option +(** [get_value f args mdl] returns the value of the declared name [f] + evaluates to the arguments [args] in the model [mdl]. + + @return [None] if the model [mdl] doesn't contain a definition for the + name [f]. *) + +val empty : suspicious:bool -> Symbols.typed_name list -> t (** An empty model. The [suspicious] flag is used to remember that this model may be wrong as it involves symbols from theories for which the model generation is known to be incomplete. *) -val find : Id.typed -> t -> graph +val find : Symbols.typed_name -> t -> Graph.t (** [find sy mdl] returns the graph associated with the symbol [sy] in the model [mdl], raises [Not_found] if it doesn't exist. *) -val fold: (Id.typed -> graph -> 'a -> 'a) -> t -> 'a -> 'a +val fold: (Symbols.typed_name -> Graph.t -> '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. *) -val subst : Id.t -> Expr.t -> t -> t +val subst : Symbols.Name.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]. diff --git a/src/lib/structures/symbols.ml b/src/lib/structures/symbols.ml index 87e47fb45a..18036b2491 100644 --- a/src/lib/structures/symbols.ml +++ b/src/lib/structures/symbols.ml @@ -77,9 +77,10 @@ type form = | F_Lemma | F_Skolem -type name_kind = Ac | Other +type name_kind = Ac | Other [@@deriving ord, eq] -type name_space = User | Internal | Fresh | Fresh_ac | Skolem | Abstract +type name_space = + User | Internal | Fresh | Fresh_ac | Skolem | Abstract | GetValue let compare_name_space ns1 ns2 = match ns1, ns2 with @@ -104,20 +105,62 @@ let compare_name_space ns1 ns2 = | _, Skolem -> 1 | Abstract, Abstract -> 0 + | Abstract, _ -> -1 + | _, Abstract -> 1 + + | GetValue, GetValue -> 0 + +let equal_name_space ns1 ns2 = compare_name_space ns1 ns2 = 0 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 } +module Name = struct + type t = { + hs : Id.t; + kind : name_kind; + defined : bool; + ns : name_space + } [@@deriving ord, eq] + + 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 + | GetValue -> "@g" ^ s + + (* NB: names are pre-mangled, which means that we don't need to take the + namespace into consideration when hashing or comparing. *) + let mk ?(kind=Other) ?(defined=false) ?(ns = User) s = + { hs = Hstring.make (mangle ns s) ; kind ; defined ; ns } + + let pp ppf { hs; _ } = + (* Names are pre-mangled *) + Hstring.view hs + |> Dolmen.Std.Name.simple + |> Dolmen.Smtlib2.Script.Poly.Print.id ppf +end + +type typed_name = Name.t * Ty.t list * Ty.t [@@deriving ord] + +let pp_typed_name ppf (name, arg_tys, ret_ty) = + Fmt.pf ppf "%a : (%a) -> %a" + Name.pp name + Fmt.(list ~sep:sp Ty.pp_smtlib) arg_tys + Ty.pp_smtlib ret_ty + type t = | True | False - | Name of - { hs : Id.t - ; kind : name_kind - ; defined : bool - ; ns : name_space } + | Name of Name.t | Int of Z.t | Real of Q.t | Bitv of int * Z.t @@ -129,21 +172,8 @@ 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 } + Name (Name.mk ~kind ~defined ~ns s) let var s = Var s let int i = Int (Z.of_string i) @@ -175,7 +205,7 @@ let is_ac x = match x with let is_internal sy = match sy with - | Name { ns = User; _ } -> false + | Name { ns = (User | GetValue); _ } -> false | Name _ -> true | _ -> false @@ -319,10 +349,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,7 +453,7 @@ 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) + | Name name -> Name.pp ppf name | Var v when show_vars -> Fmt.pf ppf "'%s'" (Var.to_string v) | Var v -> Fmt.string ppf (Var.to_string v) diff --git a/src/lib/structures/symbols.mli b/src/lib/structures/symbols.mli index eb93fb3e79..b5e809ee7e 100644 --- a/src/lib/structures/symbols.mli +++ b/src/lib/structures/symbols.mli @@ -111,7 +111,7 @@ type name_space = namespace, [Fresh_ac] below. To ensure uniqueness, fresh names must always be generated using - [Id.Namespace.Internal.fresh ()]. + {!val:Id.Namespace.Internal.fresh}. In particular, fresh names are only used to denote constants, not arbitrary functions. *) @@ -136,25 +136,63 @@ type name_space = `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. + represents an abstract value in sense of the SMT-LIB standard. To ensure uniqueness, abstract names must always be generated using - [Id.Namespace.Abstract.fresh ()]. *) + {!val:Id.Namespace.Abstract.fresh}. *) + | GetValue + (** This symbol is generated by the `get-value` statement to track + new values computed in the model. + + To ensure uniqueness, get-value names must always be generated using + {!val:Id.Namespace.GetValue.fresh}. + + In particular, this symbol can appear in a {!type:ModelMap.t} but + they aren't printed by {!val:ModelMap.pp}. *) 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 } +module Name : sig + type t = { + hs : Id.t; + (** Note: [hs] is prefixed according to [ns]. *) + + kind : name_kind; + defined : bool; + ns : name_space + } + + val mk : ?kind:name_kind -> ?defined:bool -> ?ns:name_space -> string -> t + (** [mk ~kind ~defined ~ns id] creates a new name with the given identifier + [id]. + + 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 equal : t -> t -> bool + val pp : t Fmt.t +end + +type typed_name = Name.t * Ty.t list * Ty.t +(** Typed name of function. In order: + - The identifier. + - Types of its arguments. + - The returned type. *) + +val compare_typed_name : typed_name -> typed_name -> int +val pp_typed_name : typed_name Fmt.t + 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 Name.t | Int of Z.t | Real of Q.t | Bitv of int * Z.t @@ -166,15 +204,13 @@ type t = | MapsTo of Var.t | Let +val name : ?kind:name_kind -> ?defined:bool -> ?ns:name_space -> string -> t (** 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 var : Var.t -> t val int : string -> t @@ -189,8 +225,8 @@ val mk_maps_to : Var.t -> t val is_ac : t -> bool val is_internal : t -> bool -(** Check if the symbol is internal name that should never be printed on the - regular output. *) +(** [is_internal sy] checks if the symbol [sy] is an internal name that + should never be printed on the regular output. *) val equal : t -> t -> bool val compare : t -> t -> int @@ -205,8 +241,6 @@ 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. *) diff --git a/src/lib/util/my_list.ml b/src/lib/util/my_list.ml index e975150d53..04b47eaef6 100644 --- a/src/lib/util/my_list.ml +++ b/src/lib/util/my_list.ml @@ -74,3 +74,11 @@ let rec is_sorted cmp l = match l with | x :: y :: xs -> cmp x y <= 0 && is_sorted cmp (y :: xs) | [_] | [] -> true + +let rec iter_pair f (l1, l2) = + match l1, l2 with + | [], [] -> () + | hd1 :: tl1, hd2 :: tl2 -> + f (hd1, hd2); + iter_pair f (tl1, tl2) + | _ -> invalid_arg "iter_pair" diff --git a/src/lib/util/my_list.mli b/src/lib/util/my_list.mli index 12cff3d207..d4f5141d33 100644 --- a/src/lib/util/my_list.mli +++ b/src/lib/util/my_list.mli @@ -47,11 +47,11 @@ val apply : ('a -> 'a) -> 'a list -> 'a list * bool (** [apply f [a_1; ...; a_n]] returns a couple [[f a_1; ...; f a_n], same] same such that: (1) "same" is true if and only if a_i == a_i for each i; and (2) if same is true, then the resulting list is - physically equal to the argument **) + physically equal to the argument *) val apply_right : ('a -> 'a) -> ('b * 'a) list -> ('b * 'a) list * bool (** similar to function apply, but the elements of the list are - couples **) + 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] @@ -60,3 +60,9 @@ val try_map : ('a -> 'b option) -> 'a list -> 'b list option val is_sorted : ('a -> 'a -> int) -> 'a list -> bool (** [is_sorted cmp l] checks that [l] is sorted for the comparison function [cmp]. *) + +val iter_pair : (('a * 'b) -> unit) -> ('a list * 'b list) -> unit +(** [iter_pair f (l1, l2)] iterates simultany on the pair of elements of the + lists [l1] and [l2]. + + @raise Invalid_arg if the lists don't have the same length. *) diff --git a/src/lib/util/options.ml b/src/lib/util/options.ml index 930ff56f19..ddf5f62f31 100644 --- a/src/lib/util/options.ml +++ b/src/lib/util/options.ml @@ -358,6 +358,7 @@ let get_timelimit_per_goal () = !timelimit_per_goal let interpretation = ref INone let strict_mode = ref false let dump_models = ref false +let verify_models = ref false let objectives_in_interpretation = ref false let output_format = ref Native let model_type = ref Value @@ -367,6 +368,7 @@ let unsat_core = ref false let set_interpretation b = interpretation := b let set_strict_mode b = strict_mode := b let set_dump_models b = dump_models := b +let set_verify_models b = verify_models := b let set_objectives_in_interpretation b = objectives_in_interpretation := b let set_output_format b = output_format := b let set_model_type t = model_type := t @@ -392,6 +394,7 @@ let equal_mode_type a b = let get_interpretation () = not @@ equal_mode !interpretation INone let get_strict_mode () = !strict_mode let get_dump_models () = !dump_models +let get_verify_models () = !verify_models let get_first_interpretation () = equal_mode !interpretation IFirst let get_every_interpretation () = equal_mode !interpretation IEvery let get_last_interpretation () = equal_mode !interpretation ILast diff --git a/src/lib/util/options.mli b/src/lib/util/options.mli index 8946e2e84b..d0a053fb46 100644 --- a/src/lib/util/options.mli +++ b/src/lib/util/options.mli @@ -224,6 +224,9 @@ val set_strict_mode : bool -> unit (** [dump_models] accessible with {!val:get_dump_models}. *) val set_dump_models : bool -> unit +(** [verify_models] accessible with {!val:set_verify_models}. *) +val set_verify_models : bool -> unit + (** Set [objectives_in_interpretation] accessible with {!val:get_objectives_in_interpretation} *) val set_objectives_in_interpretation : bool -> unit @@ -722,6 +725,11 @@ val get_strict_mode : unit -> bool val get_dump_models : unit -> bool (** Default to [false]. *) +(** [true] if the interpretation for each goal or check-sat is + produced and verified (best-effort). *) +val get_verify_models : unit -> bool +(** Default to [false]. *) + (** [true] if the interpretation is set to first interpretation *) val get_first_interpretation : unit -> bool (** Default to [false] *) diff --git a/tests/float/test_float2.default.smt2 b/tests/float/test_float2.default.smt2 index 1a51c4e27b..b904f6e52d 100644 --- a/tests/float/test_float2.default.smt2 +++ b/tests/float/test_float2.default.smt2 @@ -5,4 +5,4 @@ (assert (> x 0.0)) (assert (= ((_ ae.round 1 2) RTZ 0.3) x)) (check-sat) -(get-model) \ No newline at end of file +(get-model) diff --git a/tests/issues/1163.default.smt2 b/tests/issues/1163.default.smt2 index debce6627e..8d09887683 100644 --- a/tests/issues/1163.default.smt2 +++ b/tests/issues/1163.default.smt2 @@ -1,5 +1,6 @@ -(set-logic ALL) (set-option :produce-models true) +(set-option :verify-models false) +(set-logic ALL) (declare-const x Int) (define-fun myabs ((x Int)) Int (ite (< x 0) (- x) x)) (maximize (myabs x)) diff --git a/tests/issues/555.default.expected b/tests/issues/555.default.expected index f5b97ee0bf..2d5984b3d9 100644 --- a/tests/issues/555.default.expected +++ b/tests/issues/555.default.expected @@ -3,6 +3,6 @@ unknown ( (define-fun x () Int 0) (define-fun y () Int 0) - (define-fun a1 () (Array Int Int) (store (as @a4 (Array Int Int)) 0 0)) - (define-fun a2 () (Array Int Int) (store (as @a5 (Array Int Int)) 0 0)) + (define-fun a1 () (Array Int Int) (store (as @a12 (Array Int Int)) 0 0)) + (define-fun a2 () (Array Int Int) (store (as @a11 (Array Int Int)) 0 0)) ) diff --git a/tests/issues/854/function.default.expected b/tests/issues/854/function.default.expected index 63577badcf..dd7ff83a12 100644 --- a/tests/issues/854/function.default.expected +++ b/tests/issues/854/function.default.expected @@ -2,7 +2,7 @@ unknown ( (define-fun a () Int 0) - (define-fun intrefqtmk ((_arg_0 Int)) intref (as @a4 intref)) + (define-fun intrefqtmk ((_arg_0 Int)) intref (as @a10 intref)) (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..7224283b88 100644 --- a/tests/issues/854/original.default.expected +++ b/tests/issues/854/original.default.expected @@ -2,6 +2,6 @@ unknown ( (define-fun a () Int 0) - (define-fun intrefqtmk ((_arg_0 Int)) intref (as @a3 intref)) + (define-fun intrefqtmk ((_arg_0 Int)) intref (as @a8 intref)) (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..d29f948593 100644 --- a/tests/issues/854/twice_eq.default.expected +++ b/tests/issues/854/twice_eq.default.expected @@ -2,7 +2,7 @@ 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 intrefqtmk ((_arg_0 Int)) intref (as @a10 intref)) + (define-fun another_mk ((_arg_0 Int)) intref (as @a10 intref)) (define-fun a1 () Int 0) ) diff --git a/tests/models/arith/arith10.default.smt2 b/tests/models/arith/arith10.default.smt2 index 5d0a429d98..e691701564 100644 --- a/tests/models/arith/arith10.default.smt2 +++ b/tests/models/arith/arith10.default.smt2 @@ -1,4 +1,5 @@ (set-option :produce-models true) +(set-option :verify-models false) (set-logic ALL) (declare-const x Real) (declare-const y Real) diff --git a/tests/models/arith/arith11.default.smt2 b/tests/models/arith/arith11.default.smt2 index cdcafdbe4f..6c5c6695e6 100644 --- a/tests/models/arith/arith11.default.smt2 +++ b/tests/models/arith/arith11.default.smt2 @@ -1,4 +1,5 @@ (set-option :produce-models true) +(set-option :verify-models false) (set-logic ALL) (declare-const p1 Bool) (declare-const p2 Bool) diff --git a/tests/models/arith/arith12.default.smt2 b/tests/models/arith/arith12.default.smt2 index 6f3103cc9e..9b4a95419c 100644 --- a/tests/models/arith/arith12.default.smt2 +++ b/tests/models/arith/arith12.default.smt2 @@ -1,4 +1,5 @@ (set-option :produce-models true) +(set-option :verify-models false) (set-logic ALL) (declare-const x Int) (assert (<= 0 x 10)) diff --git a/tests/models/arith/arith13.default.smt2 b/tests/models/arith/arith13.default.smt2 index dc248e6bd8..d55d12faea 100644 --- a/tests/models/arith/arith13.default.smt2 +++ b/tests/models/arith/arith13.default.smt2 @@ -1,5 +1,6 @@ -(set-option :produce-models true) (set-logic ALL) +(set-option :produce-models true) +(set-option :verify-models false) (declare-const x Int) (assert (<= x 10)) (push 1) diff --git a/tests/models/arith/arith14.default.smt2 b/tests/models/arith/arith14.default.smt2 index 1add269864..b3188634ec 100644 --- a/tests/models/arith/arith14.default.smt2 +++ b/tests/models/arith/arith14.default.smt2 @@ -1,4 +1,5 @@ (set-option :produce-models true) +(set-option :verify-models false) (set-logic ALL) (declare-const x Int) (declare-const y Int) diff --git a/tests/models/arith/arith3.default.smt2 b/tests/models/arith/arith3.default.smt2 index 51970a5b1b..1d3b9db403 100644 --- a/tests/models/arith/arith3.default.smt2 +++ b/tests/models/arith/arith3.default.smt2 @@ -1,5 +1,6 @@ (set-logic ALL) (set-option :produce-models true) +(set-option :verify-models false) (declare-const x Int) (declare-const y Int) (declare-const z Int) diff --git a/tests/models/arith/arith4.default.smt2 b/tests/models/arith/arith4.default.smt2 index a59d9732f8..1babde745e 100644 --- a/tests/models/arith/arith4.default.smt2 +++ b/tests/models/arith/arith4.default.smt2 @@ -1,5 +1,6 @@ (set-logic ALL) (set-option :produce-models true) +(set-option :verify-models false) (declare-const x Int) (declare-const y Int) (assert (<= x y)) diff --git a/tests/models/arith/arith5.default.smt2 b/tests/models/arith/arith5.default.smt2 index 8992a26fba..91f6df472e 100644 --- a/tests/models/arith/arith5.default.smt2 +++ b/tests/models/arith/arith5.default.smt2 @@ -1,4 +1,5 @@ (set-option :produce-models true) +(set-option :verify-models false) (set-logic ALL) (declare-const x Real) (declare-const y Real) diff --git a/tests/models/arith/arith6.default.smt2 b/tests/models/arith/arith6.default.smt2 index 10b3d625d3..ec783b7c68 100644 --- a/tests/models/arith/arith6.default.smt2 +++ b/tests/models/arith/arith6.default.smt2 @@ -1,4 +1,5 @@ (set-option :produce-models true) +(set-option :verify-models false) (set-logic ALL) (declare-const x Int) (declare-const y Int) diff --git a/tests/models/arith/arith7.default.smt2 b/tests/models/arith/arith7.default.smt2 index 80b3fb9e70..5574785209 100644 --- a/tests/models/arith/arith7.default.smt2 +++ b/tests/models/arith/arith7.default.smt2 @@ -1,4 +1,5 @@ (set-option :produce-models true) +(set-option :verify-models false) (set-logic ALL) (declare-const x Real) (declare-const y Real) diff --git a/tests/models/arith/arith8.default.smt2 b/tests/models/arith/arith8.default.smt2 index 33166a4ef7..f68734fff9 100644 --- a/tests/models/arith/arith8.default.smt2 +++ b/tests/models/arith/arith8.default.smt2 @@ -1,6 +1,7 @@ ; This test checks if the optimization doesn't stop after getting an optimized ; model in a fixed branch of the SAT solver. (set-option :produce-models true) +(set-option :verify-models false) (set-logic ALL) (declare-const x Int) (declare-const y Int) diff --git a/tests/models/arith/arith9.default.smt2 b/tests/models/arith/arith9.default.smt2 index 27743705ef..67acac839d 100644 --- a/tests/models/arith/arith9.default.smt2 +++ b/tests/models/arith/arith9.default.smt2 @@ -1,6 +1,7 @@ ; This test checks if the optimization doesn't stop after trying to ; optimize a strict bound. (set-option :produce-models true) +(set-option :verify-models false) (set-logic ALL) (declare-const x Real) (declare-const y Real) diff --git a/tests/models/array/array1.default.expected b/tests/models/array/array1.default.expected index f5b97ee0bf..2d5984b3d9 100644 --- a/tests/models/array/array1.default.expected +++ b/tests/models/array/array1.default.expected @@ -3,6 +3,6 @@ unknown ( (define-fun x () Int 0) (define-fun y () Int 0) - (define-fun a1 () (Array Int Int) (store (as @a4 (Array Int Int)) 0 0)) - (define-fun a2 () (Array Int Int) (store (as @a5 (Array Int Int)) 0 0)) + (define-fun a1 () (Array Int Int) (store (as @a12 (Array Int Int)) 0 0)) + (define-fun a2 () (Array Int Int) (store (as @a11 (Array Int Int)) 0 0)) ) diff --git a/tests/models/array/embedded-array.default.expected b/tests/models/array/embedded-array.default.expected index 0cb5c3d3ec..6f186463e5 100644 --- a/tests/models/array/embedded-array.default.expected +++ b/tests/models/array/embedded-array.default.expected @@ -2,7 +2,7 @@ unknown ( (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)) + (pair (store (as @a8 (Array Int S)) 0 s) + (store (as @a8 (Array Int S)) 0 s))) + (define-fun s () S (as @a7 S)) ) diff --git a/tests/models/bitv/optim-1.default.smt2 b/tests/models/bitv/optim-1.default.smt2 index 2dc349470e..da886135d0 100644 --- a/tests/models/bitv/optim-1.default.smt2 +++ b/tests/models/bitv/optim-1.default.smt2 @@ -1,6 +1,7 @@ ; Test basic functionality -(set-logic ALL) (set-option :produce-models true) +(set-option :verify-models false) +(set-logic ALL) (declare-const x (_ BitVec 32)) (maximize x) (check-sat) diff --git a/tests/models/bitv/optim-2.default.smt2 b/tests/models/bitv/optim-2.default.smt2 index 3556301371..366d0e636e 100644 --- a/tests/models/bitv/optim-2.default.smt2 +++ b/tests/models/bitv/optim-2.default.smt2 @@ -1,6 +1,7 @@ ; Test primitive optimization -(set-logic ALL) (set-option :produce-models true) +(set-option :verify-models false) +(set-logic ALL) (declare-const x (_ BitVec 32)) (minimize (bvnot x)) (check-sat) diff --git a/tests/models/bitv/optim-3.default.smt2 b/tests/models/bitv/optim-3.default.smt2 index 3408a460b9..3d08614fbe 100644 --- a/tests/models/bitv/optim-3.default.smt2 +++ b/tests/models/bitv/optim-3.default.smt2 @@ -1,6 +1,7 @@ ; Test constrained optimization (set-logic ALL) (set-option :produce-models true) +(set-option :verify-models false) (declare-const x (_ BitVec 32)) (maximize x) (assert (bvslt x ((_ int2bv 32) (- 1)))) diff --git a/tests/models/bitv/optim-4.default.smt2 b/tests/models/bitv/optim-4.default.smt2 index fe5e1b3419..b1f63be7f1 100644 --- a/tests/models/bitv/optim-4.default.smt2 +++ b/tests/models/bitv/optim-4.default.smt2 @@ -1,6 +1,7 @@ ; Test constrained function optimization -(set-logic ALL) (set-option :produce-models true) +(set-option :verify-models false) +(set-logic ALL) (declare-const x (_ BitVec 32)) (define-fun bvabs32 ((x (_ BitVec 32))) (_ BitVec 33) (ite diff --git a/tests/models/bitv/optim-5.default.smt2 b/tests/models/bitv/optim-5.default.smt2 index 57e5a01163..ce7599c43e 100644 --- a/tests/models/bitv/optim-5.default.smt2 +++ b/tests/models/bitv/optim-5.default.smt2 @@ -1,5 +1,6 @@ ; Test lexicographic optimization (set-option :produce-models true) +(set-option :verify-models false) (set-logic ALL) (declare-const x (_ BitVec 32)) (declare-const y (_ BitVec 32)) diff --git a/tests/models/bool/bool2.default.expected b/tests/models/bool/bool2.default.expected index e1c81ab550..e34c4d1923 100644 --- a/tests/models/bool/bool2.default.expected +++ b/tests/models/bool/bool2.default.expected @@ -2,7 +2,7 @@ unknown ( (define-fun x () Bool false) - (define-fun y () Bool (as @a0 Bool)) + (define-fun y () Bool (as @a3 Bool)) ) ((notx true)) diff --git a/tests/models/bool/bool3.default.smt2 b/tests/models/bool/bool3.default.smt2 index 1d417aec4b..6435430b45 100644 --- a/tests/models/bool/bool3.default.smt2 +++ b/tests/models/bool/bool3.default.smt2 @@ -6,4 +6,4 @@ (assert (or (! (and x y) :named foo) (! (and (not x) (not y)) :named bar))) (check-sat) (get-model) -(get-assignment) \ No newline at end of file +(get-assignment) diff --git a/tests/models/complete_1.default.expected b/tests/models/complete_1.default.expected index d507e21caa..3df9d405c8 100644 --- a/tests/models/complete_1.default.expected +++ b/tests/models/complete_1.default.expected @@ -1,5 +1,5 @@ unknown ( - (define-fun x () Int (as @a0 Int)) + (define-fun x () Int (as @a2 Int)) ) diff --git a/tests/models/complete_2.default.expected b/tests/models/complete_2.default.expected index 09be592338..3bb68fda80 100644 --- a/tests/models/complete_2.default.expected +++ b/tests/models/complete_2.default.expected @@ -1,6 +1,6 @@ unknown ( - (define-fun x () Int (as @a1 Int)) - (define-fun f ((_arg_0 Int)) Int (as @a0 Int)) + (define-fun x () Int (as @a4 Int)) + (define-fun f ((_arg_0 Int)) Int (as @a3 Int)) ) diff --git a/tests/models/complete_3.default.expected b/tests/models/complete_3.default.expected index d507e21caa..3df9d405c8 100644 --- a/tests/models/complete_3.default.expected +++ b/tests/models/complete_3.default.expected @@ -1,5 +1,5 @@ unknown ( - (define-fun x () Int (as @a0 Int)) + (define-fun x () Int (as @a2 Int)) ) diff --git a/tests/models/get_value.models.expected b/tests/models/get_value.models.expected new file mode 100644 index 0000000000..0261e6d968 --- /dev/null +++ b/tests/models/get_value.models.expected @@ -0,0 +1,7 @@ + +unknown +((x (- 1)) + ((+ x 5) 4)) + +((foo true)) + diff --git a/tests/models/get_value.models.smt2 b/tests/models/get_value.models.smt2 new file mode 100644 index 0000000000..df0f1c58a9 --- /dev/null +++ b/tests/models/get_value.models.smt2 @@ -0,0 +1,10 @@ +(set-option :produce-models true) +(set-option :produce-assignments true) +(set-logic ALL) +(declare-const x Int) +(declare-fun f (Int) Int) +(assert (! (> (f x) 0) :named foo)) +(assert (< (f 0) 0)) +(check-sat) +(get-value (x (+ x 5))) +(get-assignment) diff --git a/tests/models/issues/719.default.err.smt2 b/tests/models/issues/719.default.err.smt2 index 66c07f37cf..ed0714865e 100644 --- a/tests/models/issues/719.default.err.smt2 +++ b/tests/models/issues/719.default.err.smt2 @@ -16,4 +16,4 @@ (=> (and (<= 0 p) (< p q) (<= q 10)) (<= (select a p) (select a q)))))) (check-sat) (get-model) -; (get-model) should fail because the problem is UNSAT. \ No newline at end of file +; (get-model) should fail because the problem is UNSAT. diff --git a/tools/gentest.ml b/tools/gentest.ml index b6e20987a1..9ea04d3d1b 100644 --- a/tools/gentest.ml +++ b/tools/gentest.ml @@ -348,6 +348,7 @@ let () = let shared = [ timelimit ; "--enable-assertions" + ; "--verify-models" ] in let solvers = [