diff --git a/src/lib/reasoners/satml_frontend.ml b/src/lib/reasoners/satml_frontend.ml index 2a2c206b3c..d9f7a6cc04 100644 --- a/src/lib/reasoners/satml_frontend.ml +++ b/src/lib/reasoners/satml_frontend.ml @@ -60,6 +60,8 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct skolems : E.gformula ME.t; (* key <-> f *) add_inst : E.t -> bool; guards : guards; + last_saved_model : Models.t Lazy.t option ref; + model_gen_phase : bool ref; } let empty_guards () = { @@ -86,7 +88,9 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct inst = Inst.empty; skolems = ME.empty; guards = init_guards (); - add_inst = fun _ -> true; + add_inst = (fun _ -> true); + last_saved_model = ref None; + model_gen_phase = ref false; } let empty_with_inst add_inst = @@ -984,13 +988,66 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct | C_bool _ -> assert false | C_theory expl -> raise (Ex.Inconsistent (expl, [])) + let may_update_last_saved_model env compute = + let compute = + if not (Options.get_first_interpretation ()) then compute + else !(env.last_saved_model) == None + in + if not compute then env + else begin + try + (* also performs case-split and pushes pending atoms to CS *) + let model = Th.compute_concrete_model (SAT.current_tbox env.satml) in + env.last_saved_model := model; + env + with Ex.Inconsistent (_expl, _classes) as e -> + raise e + + end + + 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 + 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 ti; + update_model_and_return_unknown + env i ~timeout:ProofSearch (* may becomes ModelGen *) + end + let rec unsat_rec env ~first_call:_ : unit = try SAT.solve env.satml; assert false with | Satml.Unsat lc -> raise (IUnsat (env, make_explanation lc)) + | Util.Timeout -> model_gen_on_timeout env + | Satml.Sat -> try let env = do_case_split env Util.BeforeMatching in + let env = + may_update_last_saved_model env + (Options.get_every_interpretation ()) + in let env = {env with nb_mrounds = env.nb_mrounds + 1} [@ocaml.ppwarning "TODO: first intantiation a la DfsSAT before searching ..."] @@ -1019,15 +1076,24 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct else env in - if not updated then raise (I_dont_know {env; timeout = ProofSearch}); + if not updated then + update_model_and_return_unknown + env (Options.get_last_interpretation ()) + ~timeout:NoTimeout; (* may becomes ModelGen *) unsat_rec env ~first_call:false - with Ex.Inconsistent (expl, _cls) -> (*may be raised during matching*) - try - SAT.conflict_analyze_and_fix env.satml (Satml.C_theory expl); - unsat_rec env ~first_call:false with + | Util.Timeout -> model_gen_on_timeout env | Satml.Unsat lc -> raise (IUnsat (env, make_explanation lc)) + | Ex.Inconsistent (expl, _cls) -> (*may be raised during matching or CS*) + begin + try + SAT.conflict_analyze_and_fix env.satml (Satml.C_theory expl); + unsat_rec env ~first_call:false + with + | Satml.Unsat lc -> raise (IUnsat (env, make_explanation lc)) + | Util.Timeout -> model_gen_on_timeout env + end (* copied from sat_solvers.ml *) let max_term_depth_in_sat env = @@ -1046,7 +1112,6 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct Errors.run_error (Errors.Unsupported_feature msg) in let open Options in - if get_interpretation () then fails "interpretation"; if get_save_used_context () then fails "save_used_context"; if get_unsat_core () then fails "unsat_core" @@ -1091,6 +1156,8 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct assert (not (Stack.is_empty acc.guards.stack_guard)); let b = Stack.top acc.guards.stack_guard in Steps.pop_steps (); + acc.model_gen_phase := false; + env.last_saved_model := None; {acc with inst; guards = { acc.guards with @@ -1121,7 +1188,8 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct let env = {env with inst = Inst.register_max_term_depth env.inst max_t} in unsat_rec env ~first_call:true; assert false - with IUnsat (_env, dep) -> + with + | IUnsat (_env, dep) -> assert begin Ex.fold_atoms (fun e b -> match e with @@ -1131,12 +1199,22 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct )dep true end; dep + | (Util.Timeout | I_dont_know _) as e -> raise e + | e -> + Printer.print_dbg + ~module_name:"Satml_frontend" ~function_name:"unsat" + "%s" (Printexc.to_string e); + assert false let assume env gf _dep = (* dep currently not used. No unsat-cores in satML yet *) assert (SAT.decision_level env.satml == 0); try fst (assume_aux ~dec_lvl:0 env [add_guard env gf]) - with IUnsat (_env, dep) -> raise (Unsat dep) + with | IUnsat (_env, dep) -> raise (Unsat dep) + | Util.Timeout -> + (* don't attempt to compute a model if timeout before + calling unsat function *) + raise (I_dont_know {env; timeout = Assume}) (* instrumentation of relevant exported functions for profiling *) let assume t ff dep = @@ -1167,7 +1245,7 @@ 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 get_model env = !(env.last_saved_model) let reinit_ctx () = Steps.reinit_steps ();