diff --git a/src/bin/common/solving_loop.ml b/src/bin/common/solving_loop.ml index 326892135e..44d2ace472 100644 --- a/src/bin/common/solving_loop.ml +++ b/src/bin/common/solving_loop.ml @@ -489,7 +489,17 @@ let main () = | {contents = `Get_model; _ } -> if Options.get_interpretation () then match State.get partial_model_key st with - | Some partial_model -> SAT.get_model partial_model; st + | Some partial_model -> + begin + match SAT.get_model partial_model with + | Some (lazy model) -> + Models.output_concrete_model + (Options.Output.get_fmt_regular ()) model; + st + | _ -> + (* TODO: is it reachable? *) + st + end | None -> (* TODO: add the location of the statement. *) Printer.print_smtlib_err "No model produced."; diff --git a/src/lib/frontend/frontend.ml b/src/lib/frontend/frontend.ml index cf407df997..c0276295b0 100644 --- a/src/lib/frontend/frontend.ml +++ b/src/lib/frontend/frontend.ml @@ -154,6 +154,33 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct if Options.get_unsat_core () then Ex.singleton (Ex.RootDep {name;f;loc}) else Ex.empty + let timeout_reason_to_string = function + | None -> "(?)" + | Some SAT.NoTimeout -> "NoTimeout" + | Some SAT.Assume -> "Assume" + | Some SAT.ProofSearch -> "ProofSearch" + | Some SAT.ModelGen -> "ModelGen" + + let print_model env timeout = + let get_m = Options.get_interpretation () in + let s = timeout_reason_to_string timeout in + match SAT.get_model env with + | None -> + if get_m then + Printer.print_fmt (Options.Output.get_fmt_diagnostic ()) + "@[It seems that no model has been computed so \ + far. You may need to change your model generation strategy \ + or to increase your timeouts. Returned timeout reason = %s@]" s + + | Some m -> + assert (get_m); + if get_m then + Printer.print_fmt + (Options.Output.get_fmt_diagnostic ()) + "@[; Returned timeout reason = %s@]" s; + let m = Lazy.force m in + Models.output_concrete_model (Options.Output.get_fmt_regular ()) m + let process_decl print_status used_context consistent_dep_stack ((env, consistent, dep) as acc) d = try @@ -246,8 +273,8 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct (* This case should mainly occur when a query has a non-unsat result, so we want to print the status in this case. *) print_status (Sat (d,t)) (Steps.get_steps ()); - (*if get_model () then SAT.print_model ~header:true (get_fmt_mdl ()) t;*) - env, `Sat t, dep + print_model env (Some SAT.NoTimeout); + env , consistent, dep | SAT.Unsat dep' -> (* 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 @@ -255,18 +282,24 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct let dep = Ex.union dep dep' in if get_debug_unsat_core () then check_produced_unsat_core dep; (* print_status (Inconsistent d) (Steps.get_steps ()); *) - env, `Unsat, dep - | SAT.I_dont_know t -> - (* In this case, it's not clear whether we want to print the status. - Instead, it'd be better to accumulate in `consistent` a 3-case adt - and not a simple bool. *) - print_status (Unknown (d, t)) (Steps.get_steps ()); - (*if get_model () then SAT.print_model ~header:true (get_fmt_mdl ()) t;*) - env, `Unknown t, dep + env , `Unsat, dep + | SAT.I_dont_know {env; timeout} -> + (* TODO: always print Unknown for why3 ? *) + let status = + if timeout != NoTimeout then (Timeout (Some d)) + else (Unknown (d, env)) + in + print_status status (Steps.get_steps ()); + print_model env (Some timeout); + (* TODO: Is it an appropriate behaviour? *) + (* if timeout != NoTimeout then raise Util.Timeout; *) + env, consistent, dep + | Util.Timeout as e -> (* In this case, we obviously want to print the status, since we exit right after *) print_status (Timeout (Some d)) (Steps.get_steps ()); + print_model env None; raise e let print_status status steps = diff --git a/src/lib/frontend/models.ml b/src/lib/frontend/models.ml index 7f4ffcec8a..756e75a77f 100644 --- a/src/lib/frontend/models.ml +++ b/src/lib/frontend/models.ml @@ -45,6 +45,13 @@ module MX = Shostak.MXH let constraints = ref MS.empty +type t = { + propositional : Expr.Set.t; + constants : ModelMap.t; + functions : ModelMap.t; + arrays : ModelMap.t; +} + module Pp_smtlib_term = struct let to_string_type t = @@ -477,55 +484,63 @@ let rec pp_value ppk ppf = function let pp_constant ppf (_sy, t) = Fmt.pf ppf "%a" SmtlibCounterExample.pp_abstract_value_of_type t -let output_concrete_model fmt props ~functions ~constants ~arrays = - if ModelMap.(is_suspicious functions || is_suspicious constants - || is_suspicious 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 "@[("; - if Options.get_model_type_constraints () then - begin - Why3CounterExample.output_constraints fmt props; - Format.fprintf fmt "@ ; values" +let output_concrete_model fmt m = + if Options.get_interpretation () then begin + (* TODO: does we need to check also m.propositional ? *) + 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 "@[("; + Why3CounterExample.output_constraints fmt m.propositional; + + Printer.print_fmt ~flushed:false fmt "@[unknown@ "; + Printer.print_fmt ~flushed:false fmt "@[(model@,"; + if Options.get_output_format () == Why3 then begin + Why3CounterExample.output_constraints fmt m.propositional end; - let values = Hashtbl.create 17 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) 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) - arrays; - - let pp_value = - pp_value (fun ppf (sy, _) -> - pp_value pp_constant ppf (Hashtbl.find values sy)) - in - - let pp_x ppf xs = pp_value ppf (value xs) in - - (* Functions *) - let records = SmtlibCounterExample.output_functions_counterexample - pp_x fmt MS.empty functions - in - - (* Constants *) - SmtlibCounterExample.output_constants_counterexample - pp_x fmt records constants; + let values = Hashtbl.create 17 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, _) -> + pp_value pp_constant ppf (Hashtbl.find values sy)) + 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 "@]@,)"; +end diff --git a/src/lib/frontend/models.mli b/src/lib/frontend/models.mli index dcbe944a33..749bed0bed 100644 --- a/src/lib/frontend/models.mli +++ b/src/lib/frontend/models.mli @@ -30,16 +30,17 @@ (** {1 Models module} *) +type t = { + propositional : Expr.Set.t; + constants : ModelMap.t; + functions : ModelMap.t; + arrays : ModelMap.t; +} + (** Print the given counterexample on the given formatter with the corresponding format set with Options.get_output_format. - functions: the functions of the model; - constants: the variables of the model; - arrays: (experimental) the arrays of the model. *) -val output_concrete_model : - Format.formatter -> - Expr.Set.t -> - functions:ModelMap.t -> - constants:ModelMap.t -> - arrays:ModelMap.t -> - unit +val output_concrete_model : Format.formatter -> t -> unit diff --git a/src/lib/reasoners/ccx.ml b/src/lib/reasoners/ccx.ml index 11cbabc158..a7d6a71232 100644 --- a/src/lib/reasoners/ccx.ml +++ b/src/lib/reasoners/ccx.ml @@ -85,11 +85,11 @@ module type S = sig Matching_types.info Expr.Map.t * Expr.t list Expr.Map.t Symbols.Map.t -> t -> (Expr.t -> Expr.t -> bool) -> t * Sig_rel.instances - val output_concrete_model : - Format.formatter -> + val extract_concrete_model : prop_model:Expr.Set.t -> t -> - unit + Models.t Lazy.t option + end module Main : S = struct @@ -738,7 +738,6 @@ module Main : S = struct in Uf.term_repr env.uf t - let output_concrete_model fmt ~prop_model env = - Uf.output_concrete_model fmt ~prop_model env.uf - + let extract_concrete_model ~prop_model env = + Uf.extract_concrete_model ~prop_model env.uf end diff --git a/src/lib/reasoners/ccx.mli b/src/lib/reasoners/ccx.mli index c49af116e8..e97a9e55c8 100644 --- a/src/lib/reasoners/ccx.mli +++ b/src/lib/reasoners/ccx.mli @@ -76,11 +76,10 @@ module type S = sig Matching_types.info Expr.Map.t * Expr.t list Expr.Map.t Symbols.Map.t -> t -> (Expr.t -> Expr.t -> bool) -> t * Sig_rel.instances - val output_concrete_model : - Format.formatter -> + val extract_concrete_model : prop_model:Expr.Set.t -> t -> - unit + Models.t Lazy.t option end module Main : S diff --git a/src/lib/reasoners/fun_sat.ml b/src/lib/reasoners/fun_sat.ml index 865c6af256..c0ab08f13f 100644 --- a/src/lib/reasoners/fun_sat.ml +++ b/src/lib/reasoners/fun_sat.ml @@ -171,18 +171,14 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct unit_tbox : Th.t; (* theory env of facts at level 0 *) inst : Inst.t; heuristics : Heuristics.t ref; - model_gen_mode : bool ref; + model_gen_phase : bool ref; guards : guards; add_inst: E.t -> bool; unit_facts_cache : (E.gformula * Ex.t) ME.t ref; + last_saved_model : Models.t Lazy.t option ref; } - let latest_saved_env = ref None - let terminated_normally = ref false - let reset_refs () = - latest_saved_env := None; - terminated_normally := false; Steps.reset_steps () let save_guard_and_refs env new_guard = @@ -196,9 +192,15 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct { env with unit_facts_cache = ref refs.unit_facts}, guard + type timeout_reason = + | NoTimeout + | Assume + | ProofSearch + | ModelGen + exception Sat of t - exception Unsat of Ex.t - exception I_dont_know of t + exception Unsat of Explanation.t + exception I_dont_know of { env : t; timeout : timeout_reason } exception IUnsat of Ex.t * SE.t list @@ -437,22 +439,6 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct env.heuristics := Heuristics.bump_activity !(env.heuristics) expl; raise (IUnsat (expl, classes)) - let is_literal f = - match E.form_view f with - | E.Literal _ -> true - | E.Unit _ | E.Clause _ | E.Lemma _ | E.Skolem _ - | E.Let _ | E.Iff _ | E.Xor _ -> false - - let extract_prop_model ~complete_model t = - let s = ref SE.empty in - ME.iter - (fun f _ -> - if complete_model && is_literal f then - s := SE.add f !s - ) - t.gamma; - !s - (* sat-solver *) let mk_gf f name mf gf = @@ -1131,21 +1117,17 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct ignore (update_instances_cache (Some [])); env, true - let compute_concrete_model env compute = + let may_update_last_saved_model env compute = let compute = - if Options.get_first_interpretation () then - match !latest_saved_env with - | Some _ -> false - | None -> true - else compute + if not (Options.get_first_interpretation ()) then compute + else !(env.last_saved_model) == None in if not compute then env else begin try - (* to push pending stuff *) - let env = do_case_split env (Options.get_case_split_policy ()) in - let env = {env with tbox = Th.compute_concrete_model env.tbox} in - latest_saved_env := Some env; + (* also performs case-split and pushes pending atoms to CS *) + let model = Th.compute_concrete_model env.tbox in + env.last_saved_model := model; env with Ex.Inconsistent (expl, classes) -> Debug.inconsistent expl env; @@ -1154,69 +1136,34 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct raise (IUnsat (expl, classes)) end - let return_cached_model return_function = - let i = Options.get_interpretation () in - assert i; - assert (not !terminated_normally); - terminated_normally := true; (* to avoid loops *) - begin - match !latest_saved_env with - | None -> - Printer.print_wrn - "[FunSat]@, @[\ - It seems that no model has been computed so far.@,\ - You may need to change your model generation strategy@,\ - or to increase your timeout.@]" - | Some env -> - Printer.print_wrn - "[FunSat]@, @[\ - A model has been computed. However, I failed \ - while computing it so may be incorrect.@]"; - let prop_model = extract_prop_model ~complete_model:true env in - Th.output_concrete_model (Options.Output.get_fmt_regular ()) ~prop_model - env.tbox; - end; - return_function () - - (* let () = - * at_exit - * (fun () -> - * if not !terminated_normally && (get_interpretation ()) then - * return_cached_model (fun () -> ()) - * ) *) - - let return_answer env compute return_function = - let env = compute_concrete_model env compute in - Options.Time.unset_timeout (); - - let prop_model = extract_prop_model ~complete_model:true env in - if Options.(get_interpretation () && get_dump_models ()) then - Th.output_concrete_model (Options.Output.get_fmt_regular ()) ~prop_model - env.tbox; - - terminated_normally := true; - return_function env - - - let switch_to_model_gen env = - not !terminated_normally && - not !(env.model_gen_mode) && - Options.get_interpretation () - - - let do_switch_to_model_gen env = + let update_model_and_return_unknown env compute_model ~timeout = + try + let env = may_update_last_saved_model env compute_model in + Options.Time.unset_timeout (); + raise (I_dont_know {env; timeout }) + with Util.Timeout when !(env.model_gen_phase) -> + (* In this case, timeout reason becomes 'ModelGen' *) + raise (I_dont_know {env; timeout = ModelGen }) + + let model_gen_on_timeout env = let i = Options.get_interpretation () in - assert i; - if not !(env.model_gen_mode) && - Stdlib.(<>) (Options.get_timelimit_interpretation ()) 0. then + let ti = Options.get_timelimit_interpretation () in + if not i || (* not asked to gen a model *) + !(env.model_gen_phase) || (* we timeouted in model-gen-phase *) + Stdlib.(=) ti 0. (* no time allocated for extra model search *) + then + raise (I_dont_know {env; timeout = ProofSearch}) + else begin + (* Beware: models generated on timeout of ProofSearch phase may + be incohrent wrt. the ground part of the pb (ie. if delta + is not empty ? *) + env.model_gen_phase := true; Options.Time.unset_timeout (); - Options.Time.set_timeout (Options.get_timelimit_interpretation ()); - env.model_gen_mode := true; - return_answer env i (fun _ -> raise Util.Timeout) + Options.Time.set_timeout ti; + update_model_and_return_unknown + env i ~timeout:ProofSearch (* may becomes ModelGen *) end - else - return_cached_model (fun () -> raise Util.Timeout) let reduce_hypotheses tcp_cache tmp_cache env acc (hyp, gf, dep) = Debug.print_theory_instance hyp gf; @@ -1324,12 +1271,14 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct let greedy_instantiation env = match Options.get_instantiation_heuristic () with | INormal -> + (* TODO: check if this test still produces a wrong model. *) (* S: This seems spurious! On example UFDT/20170428-Barrett/cdt-cade2015/data/gandl/cotree/ x2015_09_10_16_49_52_978_1009894.smt_in.smt2, this returns a wrong model. *) - return_answer env (Options.get_last_interpretation ()) - (fun e -> raise (I_dont_know e)) + update_model_and_return_unknown + env (Options.get_last_interpretation ()) + ~timeout:NoTimeout (* may becomes ModelGen *) | IAuto | IGreedy -> let gre_inst = ME.fold @@ -1355,37 +1304,33 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct let env = do_case_split env Util.AfterMatching in if ok1 || ok2 || ok3 || ok4 then env else - return_answer env (Options.get_last_interpretation ()) - (fun e -> raise (I_dont_know e)) + update_model_and_return_unknown + env (Options.get_last_interpretation ()) + ~timeout:NoTimeout (* may becomes ModelGen *) let normal_instantiation env try_greedy = - try - Debug.print_nb_related env; - let env = do_case_split env Util.BeforeMatching in - let env = compute_concrete_model env - (Options.get_every_interpretation ()) - in - let env = new_inst_level env in - let mconf = - {Util.nb_triggers = Options.get_nb_triggers (); - no_ematching = Options.get_no_ematching(); - triggers_var = Options.get_triggers_var (); - use_cs = false; - backward = Util.Normal; - greedy = Options.get_greedy (); - } - in - let env, ok1 = inst_and_assume mconf env inst_predicates env.inst in - let env, ok2 = inst_and_assume mconf env inst_lemmas env.inst in - let env, ok3 = syntactic_th_inst env env.inst ~rm_clauses:false in - let env, ok4 = semantic_th_inst env env.inst ~rm_clauses:false ~loop:4 in - let env = do_case_split env Util.AfterMatching in - if ok1 || ok2 || ok3 || ok4 then env - else if try_greedy then greedy_instantiation env else env - with | Util.Not_implemented s -> - Printer.print_err "Feature %s is not implemented. \ - I can't conclude." s; - raise (I_dont_know env) + Debug.print_nb_related env; + let env = do_case_split env Util.BeforeMatching in + let env = + may_update_last_saved_model env (Options.get_every_interpretation ()) + in + let env = new_inst_level env in + let mconf = + {Util.nb_triggers = Options.get_nb_triggers (); + no_ematching = Options.get_no_ematching(); + triggers_var = Options.get_triggers_var (); + use_cs = false; + backward = Util.Normal; + greedy = Options.get_greedy (); + } + in + let env, ok1 = inst_and_assume mconf env inst_predicates env.inst in + let env, ok2 = inst_and_assume mconf env inst_lemmas env.inst in + let env, ok3 = syntactic_th_inst env env.inst ~rm_clauses:false in + let env, ok4 = semantic_th_inst env env.inst ~rm_clauses:false ~loop:4 in + let env = do_case_split env Util.AfterMatching in + if ok1 || ok2 || ok3 || ok4 then env + else if try_greedy then greedy_instantiation env else env (* should be merged with do_bcp/red/elim ? calls to debug hooks are missing *) @@ -1473,7 +1418,7 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct with No_suitable_decision -> back_tracking (normal_instantiation env true) with - | Util.Timeout when switch_to_model_gen env -> do_switch_to_model_gen env + | Util.Timeout -> model_gen_on_timeout env and make_one_decision env = try @@ -1711,9 +1656,8 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct (mk_gf (E.neg guard_to_neg) "" true true,Ex.empty) acc.guards.guards in - acc.model_gen_mode := false; - latest_saved_env := None; - terminated_normally := false; + acc.model_gen_phase := false; + env.last_saved_model := None; {acc with inst; guards = { acc.guards with @@ -1786,16 +1730,14 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct let d = back_tracking env in assert (Ex.has_no_bj d); - terminated_normally := true; d with | IUnsat (dep, classes) -> Debug.bottom classes; Debug.unsat (); - terminated_normally := true; assert (Ex.has_no_bj dep); dep - | Util.Timeout when switch_to_model_gen env -> do_switch_to_model_gen env + | Util.Timeout -> model_gen_on_timeout env let add_guard env gf = let current_guard = env.guards.current_guard in @@ -1808,10 +1750,12 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct assume env [add_guard env fg,dep] with | IUnsat (d, classes) -> - terminated_normally := true; Debug.bottom classes; raise (Unsat d) - | Util.Timeout when switch_to_model_gen env -> do_switch_to_model_gen env + | Util.Timeout -> + (* don't attempt to compute a model if timeout before + calling unsat function *) + raise (I_dont_know {env; timeout = Assume}) let pred_def env f name dep _loc = @@ -1885,10 +1829,11 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct unit_tbox = tbox; inst = inst; heuristics = ref (Heuristics.empty ()); - model_gen_mode = ref false; + model_gen_phase = ref false; unit_facts_cache = ref ME.empty; guards = init_guards (); - add_inst = fun _ -> true; + add_inst = (fun _ -> true); + last_saved_model = ref None; } in assume env gf_true Ex.empty @@ -1900,10 +1845,13 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct let assume_th_elt env th_elt dep = {env with tbox = Th.assume_th_elt env.tbox th_elt dep} + (** returns the latest model stored in the env if any *) + let get_model env = !(env.last_saved_model) + let reinit_ctx () = (* all_models_sat_env := None; *) - latest_saved_env := None; - terminated_normally := false; + (* latest_saved_env := None; + terminated_normally := false; *) Steps.reinit_steps (); clear_instances_cache (); Th.reinit_cpt (); @@ -1919,15 +1867,6 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct Shostak.Combine.reinit_cache (); Uf.reinit_cache () - let get_model env = - assert (Options.get_interpretation ()); - let env = compute_concrete_model env true in - Options.Time.unset_timeout (); - let prop_model = extract_prop_model ~complete_model:true env in - Th.output_concrete_model (Options.Output.get_fmt_regular ()) ~prop_model - env.tbox; - terminated_normally := true - let () = Steps.save_steps (); Var.save_cnt (); diff --git a/src/lib/reasoners/sat_solver_sig.ml b/src/lib/reasoners/sat_solver_sig.ml index 10d3f13767..0c10a0d495 100644 --- a/src/lib/reasoners/sat_solver_sig.ml +++ b/src/lib/reasoners/sat_solver_sig.ml @@ -34,9 +34,15 @@ module type S = sig type t + type timeout_reason = + | NoTimeout + | Assume + | ProofSearch + | ModelGen + exception Sat of t exception Unsat of Explanation.t - exception I_dont_know of t + exception I_dont_know of { env : t; timeout : timeout_reason } (* the empty sat-solver context *) val empty : unit -> t @@ -74,7 +80,8 @@ module type S = sig val reinit_ctx : unit -> unit (** [get_model t] produces the current model. *) - val get_model : t -> unit + val get_model: t -> Models.t Lazy.t option + end diff --git a/src/lib/reasoners/sat_solver_sig.mli b/src/lib/reasoners/sat_solver_sig.mli index 4d01811c00..611b6034de 100644 --- a/src/lib/reasoners/sat_solver_sig.mli +++ b/src/lib/reasoners/sat_solver_sig.mli @@ -31,9 +31,15 @@ module type S = sig type t + type timeout_reason = + | NoTimeout + | Assume + | ProofSearch + | ModelGen + exception Sat of t exception Unsat of Explanation.t - exception I_dont_know of t + exception I_dont_know of { env : t; timeout : timeout_reason } (** the empty sat-solver context *) val empty : unit -> t @@ -75,7 +81,8 @@ module type S = sig val reinit_ctx : unit -> unit (** [get_model t] produces the current model. *) - val get_model : t -> unit + val get_model: t -> Models.t Lazy.t option + end diff --git a/src/lib/reasoners/satml_frontend.ml b/src/lib/reasoners/satml_frontend.ml index 11e20ad9dc..1ead8a92ed 100644 --- a/src/lib/reasoners/satml_frontend.ml +++ b/src/lib/reasoners/satml_frontend.ml @@ -92,9 +92,15 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct let empty_with_inst add_inst = { (empty ()) with add_inst = add_inst } + type timeout_reason = + | NoTimeout + | Assume + | ProofSearch + | ModelGen + exception Sat of t exception Unsat of Explanation.t - exception I_dont_know of t + exception I_dont_know of { env : t; timeout : timeout_reason } exception IUnsat of t * Explanation.t @@ -1006,7 +1012,7 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct else env in - if not updated then raise (I_dont_know env); + if not updated then raise (I_dont_know {env; timeout = ProofSearch}); unsat_rec env ~first_call:false with Ex.Inconsistent (expl, _cls) -> (*may be raised during matching*) @@ -1154,6 +1160,8 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct SAT.assume_th_elt env.satml th_elt dep; env + let get_model _env = None + let reinit_ctx () = Steps.reinit_steps (); Th.reinit_cpt (); @@ -1169,8 +1177,6 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct Shostak.Combine.reinit_cache (); Uf.reinit_cache () - let get_model _env = failwith "not yet supported" - let () = Steps.save_steps (); Var.save_cnt (); diff --git a/src/lib/reasoners/theory.ml b/src/lib/reasoners/theory.ml index 7515438630..c8d65dbb00 100644 --- a/src/lib/reasoners/theory.ml +++ b/src/lib/reasoners/theory.ml @@ -60,7 +60,9 @@ module type S = sig val get_case_split_env : t -> Ccx.Main.t val do_case_split : t -> Util.case_split_policy -> t * Expr.Set.t val add_term : t -> Expr.t -> add_in_cs:bool -> t - val compute_concrete_model : t -> t + val compute_concrete_model : + t -> + Models.t Lazy.t option val assume_th_elt : t -> Expr.th_elt -> Explanation.t -> t val theories_instances : @@ -71,12 +73,6 @@ module type S = sig val get_assumed : t -> E.Set.t - val output_concrete_model : - Format.formatter -> - prop_model:Expr.Set.t -> - t -> - unit - val reinit_cpt : unit -> unit end @@ -764,17 +760,17 @@ module Main_Default : S = struct let get_case_split_env t = t.gamma_finite let compute_concrete_model env = - fst @@ do_case_split_aux env ~for_model:true - + let {gamma_finite; _}, _ = + do_case_split_aux env ~for_model:true in + CC_X.extract_concrete_model + ~prop_model:env.assumed_set + gamma_finite let assume_th_elt t th_elt dep = { t with gamma = CC_X.assume_th_elt t.gamma th_elt dep } let get_assumed env = env.assumed_set - let output_concrete_model fmt ~prop_model env = - CC_X.output_concrete_model fmt ~prop_model env.gamma_finite - let reinit_cpt () = Debug.reinit_cpt () @@ -807,11 +803,11 @@ module Main_Empty : S = struct let get_case_split_env _ = empty_ccx let do_case_split env _ = env, E.Set.empty let add_term env _ ~add_in_cs:_ = env - let compute_concrete_model e = e + let compute_concrete_model _env = None let assume_th_elt e _ _ = e let theories_instances ~do_syntactic_matching:_ _ e _ _ _ = e, [] let get_assumed env = env.assumed_set - let output_concrete_model _fmt ~prop_model:_ _env = () let reinit_cpt () = () + end diff --git a/src/lib/reasoners/theory.mli b/src/lib/reasoners/theory.mli index c3185538d5..9bdf1de3f5 100644 --- a/src/lib/reasoners/theory.mli +++ b/src/lib/reasoners/theory.mli @@ -49,7 +49,9 @@ module type S = sig val do_case_split : t -> Util.case_split_policy -> t * Expr.Set.t val add_term : t -> Expr.t -> add_in_cs:bool -> t - val compute_concrete_model : t -> t + val compute_concrete_model : + t -> + Models.t Lazy.t option val assume_th_elt : t -> Expr.th_elt -> Explanation.t -> t val theories_instances : @@ -60,14 +62,7 @@ module type S = sig val get_assumed : t -> Expr.Set.t - val output_concrete_model : - Format.formatter -> - prop_model:Expr.Set.t -> - t -> - unit - val reinit_cpt : unit -> unit - (** reinitializes the counter to zero *) end diff --git a/src/lib/reasoners/uf.ml b/src/lib/reasoners/uf.ml index b16f6a854f..073b911ac8 100644 --- a/src/lib/reasoners/uf.ml +++ b/src/lib/reasoners/uf.ml @@ -1074,14 +1074,20 @@ let compute_concrete_model ({ make; _ } as env) = ) make (ModelMap.empty, ModelMap.empty, ModelMap.empty, ME.empty) -let output_concrete_model fmt ~prop_model env = - if Options.get_interpretation () then - let functions, constants, arrays, _ = - compute_concrete_model env in - Models.output_concrete_model fmt prop_model ~functions ~constants ~arrays - let save_cache () = LX.save_cache () let reinit_cache () = LX.reinit_cache () + +let extract_concrete_model ~prop_model env = + if Options.get_interpretation () then + Some (lazy ( + let functions, constants, arrays, _mrepr = + compute_concrete_model env + in + { Models.propositional = prop_model; + functions; constants; arrays } + )) + else + None diff --git a/src/lib/reasoners/uf.mli b/src/lib/reasoners/uf.mli index ddd80b5673..e6e6d7f738 100644 --- a/src/lib/reasoners/uf.mli +++ b/src/lib/reasoners/uf.mli @@ -71,14 +71,11 @@ val assign_next : t -> (r Xliteral.view * bool * Th_util.lit_origin) list * t (** {2 Counterexample function} *) -(** Compute a counterexample using the Uf environment and then print it on the - given formatter with the corresponding format setted with - Options.get_output_format *) -val output_concrete_model : - Format.formatter -> +(** Compute a counterexample using the Uf environment *) +val extract_concrete_model : prop_model:Expr.Set.t -> t -> - unit + Models.t Lazy.t option (** saves the module's cache *) val save_cache : unit -> unit diff --git a/src/lib/util/printer.ml b/src/lib/util/printer.ml index c67e670b78..e67720d03e 100644 --- a/src/lib/util/printer.ml +++ b/src/lib/util/printer.ml @@ -369,10 +369,12 @@ let print_status_unknown ?(validity_mode=true) loc ("I don't know","unknown","fg_cyan") loc time steps goal +(* TODO: The timeout answer doesn't exist in the SMT-LIB standard. + We should change this function. *) let print_status_timeout ?(validity_mode=true) loc time steps goal = print_status ~validity_mode - ("Timeout","timeout","fg_orange") loc + ("Timeout","unknown","fg_orange") loc time steps goal let print_status_preprocess ?(validity_mode=true)