From 865c4ac734b2f5738a14c23f3dd81799f37919ad Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Basile=20Cl=C3=A9ment?= Date: Wed, 4 Oct 2023 13:14:11 +0200 Subject: [PATCH] Allow dynamic selection of the SAT solver with `set-option` This patch adds support for `(set-option :sat-solver)` in the SMT-LIB frontend. The patch mostly lifts SAT-independent bits out of `Frontend.Make`, allowing to use a first-class module stored on the Dolmen state to provide access to the frontend. Changing solvers is only allowed in the initial state (before any assertions are made) as a forward-compatibility measure: it would currently be possible to switch solvers on the fly because we merely accumulate commands in the context and only call the solver on `(check-sat)`, but allowing solver changes anywhere would make it harder to remove the command stack, which we will probably do at some point (see also #382). --- examples/lib_usage.ml | 2 +- src/bin/common/parse_command.ml | 3 - src/bin/common/solving_loop.ml | 138 +++++++++++----- src/bin/js/options_interface.ml | 1 - src/bin/js/worker_interface.ml | 8 +- src/bin/js/worker_interface.mli | 1 - src/bin/js/worker_js.ml | 18 +-- src/lib/frontend/frontend.ml | 270 +++++++++++++++----------------- src/lib/frontend/frontend.mli | 32 ++-- src/lib/util/options.ml | 7 +- src/lib/util/options.mli | 3 - 11 files changed, 255 insertions(+), 228 deletions(-) diff --git a/examples/lib_usage.ml b/examples/lib_usage.ml index 762e74199..84084cb98 100644 --- a/examples/lib_usage.ml +++ b/examples/lib_usage.ml @@ -90,7 +90,7 @@ module FE = Frontend.Make(SAT) let () = List.iter (fun (pb, _goal_name) -> - let ctxt = FE.init_all_used_context () in + let ctxt = Frontend.init_all_used_context () in let acc0 = SAT.empty (), `Unknown (SAT.empty ()), Explanation.empty in let s = Stack.create () in let _env, consistent, _ex = diff --git a/src/bin/common/parse_command.ml b/src/bin/common/parse_command.ml index e8ec7cecd..4c3b59024 100644 --- a/src/bin/common/parse_command.ml +++ b/src/bin/common/parse_command.ml @@ -1008,9 +1008,6 @@ let parse_output_opt = set_cdcl_tableaux_inst false; set_cdcl_tableaux_th false end; - set_tableaux_cdcl (match sat_solver with - | Tableaux_CDCL -> true - | _ -> false); () in Term.( diff --git a/src/bin/common/solving_loop.ml b/src/bin/common/solving_loop.ml index a6a2b3253..327ed9208 100644 --- a/src/bin/common/solving_loop.ml +++ b/src/bin/common/solving_loop.ml @@ -38,10 +38,19 @@ type solver_ctx = { global : Commands.sat_tdecl list; } +let is_solver_ctx_empty = function + { ctx = []; local = []; global = [] } -> true + | _ -> false + +type 'a sat_module = (module Sat_solver_sig.S with type t = 'a) + +type any_sat_module = (module Sat_solver_sig.S) + (* Internal state while iterating over input statements *) type 'a state = { env : 'a; solver_ctx: solver_ctx; + sat_solver : any_sat_module; } let empty_solver_ctx = { @@ -79,28 +88,32 @@ let unsupported_opt opt = in warning "unsupported option %s" opt +(* We currently use the full state of the solver as model. *) +type model = Model : 'a sat_module * 'a -> model + let main () = let () = Dolmen_loop.Code.init [] in - let module SatCont = - (val (Sat_solver.get_current ()) : Sat_solver_sig.SatContainer) in + let make_sat () = + let module SatCont = + (val (Sat_solver.get_current ()) : Sat_solver_sig.SatContainer) in - let module TH = - (val - (if Options.get_no_theory() then (module Theory.Main_Empty : Theory.S) - else (module Theory.Main_Default : Theory.S)) : Theory.S ) in + let module TH = + (val + (if Options.get_no_theory() then (module Theory.Main_Empty : Theory.S) + else (module Theory.Main_Default : Theory.S)) : Theory.S ) in - let module SAT = SatCont.Make(TH) in - - let module FE = Frontend.Make (SAT) in + (module SatCont.Make(TH) : Sat_solver_sig.S) + in - let solve all_context (cnf, goal_name) = + let solve (module SAT : Sat_solver_sig.S) all_context (cnf, goal_name) = + let module FE = Frontend.Make (SAT) in if Options.get_debug_commands () then Printer.print_dbg "@[goal %s:@ %a@]@." ~module_name:"Solving_loop" ~function_name:"solve" goal_name Fmt.(list ~sep:sp Commands.print) cnf; - let used_context = FE.choose_used_context all_context ~goal_name in + let used_context = Frontend.choose_used_context all_context ~goal_name in let consistent_dep_stack = Stack.create () in Signals_profiling.init_profiling (); try @@ -112,7 +125,8 @@ let main () = SAT.reset_refs (); let _, consistent, _ = List.fold_left - (FE.process_decl FE.print_status used_context consistent_dep_stack) + (FE.process_decl + Frontend.print_status used_context consistent_dep_stack) (SAT.empty (), `Unknown (SAT.empty ()), Explanation.empty) cnf in if Options.get_timelimit_per_goal() then @@ -126,7 +140,7 @@ let main () = printing wrong model. *) match consistent with | `Sat partial_model | `Unknown partial_model -> - Some partial_model + Some (Model ((module SAT), partial_model)) | `Unsat -> None with Util.Timeout -> if not (Options.get_timelimit_per_goal()) then exit_as_timeout (); @@ -143,7 +157,7 @@ let main () = state.solver_ctx.ctx in let cnf = List.rev @@ Cnf.make l td in - let _ = solve all_context (cnf, name) in + let _ = solve state.sat_solver all_context (cnf, name) in begin match kind with | Ty.Check | Ty.Cut -> @@ -209,7 +223,7 @@ let main () = I.parse_files ~filename ~preludes with | Util.Timeout -> - FE.print_status (FE.Timeout None) 0; + Frontend.print_status (Timeout None) 0; exit_as_timeout () | Parsing.Parse_error -> (* TODO(Steven): displaying a dummy value is a bad idea. @@ -224,9 +238,9 @@ let main () = fatal_error "%a" Errors.report e in - let all_used_context = FE.init_all_used_context () in + let all_used_context = Frontend.init_all_used_context () in if Options.get_timelimit_per_goal() then - FE.print_status FE.Preprocess 0; + Frontend.print_status Preprocess 0; let assertion_stack = Stack.create () in let typing_loop state p = if get_parse_only () then state else begin @@ -248,14 +262,15 @@ let main () = let state = { env = I.empty_env; - solver_ctx = empty_solver_ctx + solver_ctx = empty_solver_ctx; + sat_solver = make_sat (); } in try let parsed_seq = parsed () in let _ : _ state = Seq.fold_left typing_loop state parsed_seq in Options.Time.unset_timeout (); with Util.Timeout -> - FE.print_status (FE.Timeout None) 0; + Frontend.print_status (Timeout None) 0; exit_as_timeout () in @@ -263,7 +278,11 @@ let main () = State.create_key ~pipe:"" "solving_state" in - let partial_model_key: SAT.t option State.key = + let sat_solver_key : (module Sat_solver_sig.S) State.key = + State.create_key ~pipe:"" "sat_solver" + in + + let partial_model_key: model option State.key = State.create_key ~pipe:"" "sat_state" in @@ -375,6 +394,7 @@ let main () = let response_file = State.mk_file dir (`Raw ("", "")) in logic_file, State.empty + |> State.set sat_solver_key (make_sat ()) |> State.set solver_ctx_key solver_ctx |> State.set partial_model_key partial_model |> State.init ~debug ~report_style ~reports ~max_warn ~time_limit @@ -390,19 +410,23 @@ let main () = Loc.report loc name ty DStd.Term.print value in - let handle_option st_loc name (value : DStd.Term.t) = + let handle_option st_loc name (value : DStd.Term.t) st = match name, value.term with (* Smtlib2 regular options *) | ":regular-output-channel", Symbol { name = Simple name; _ } -> Options.Output.create_channel name - |> Options.Output.set_regular + |> Options.Output.set_regular; + st | ":diagnostic-output-channel", Symbol { name = Simple name; _ } -> Options.Output.create_channel name - |> Options.Output.set_diagnostic + |> Options.Output.set_diagnostic; + st | ":produce-models", Symbol { name = Simple "true"; _ } -> - Options.set_interpretation ILast + Options.set_interpretation ILast; + st | ":produce-models", Symbol { name = Simple "false"; _ } -> - Options.set_interpretation INone + Options.set_interpretation INone; + st | ":produce-unsat-cores", Symbol { name = Simple "true"; _ } -> (* The generation of unsat core is supported only with the SAT solver Tableaux. *) @@ -413,11 +437,12 @@ let main () = "%a The generation of unsat cores is not \ supported for the current SAT solver. Please \ choose the SAT solver Tableaux." - Loc.report st_loc + Loc.report st_loc; + st | ":produce-unsat-cores", Symbol { name = Simple "false"; _ } -> - Options.set_unsat_core false + Options.set_unsat_core false; st | (":produce-models" | ":produce-unsat-cores" as name), _ -> - print_wrn_opt ~name st_loc "boolean" value + print_wrn_opt ~name st_loc "boolean" value; st | ":verbosity", Symbol { name = Simple level; _ } -> begin match int_of_string_opt level with @@ -425,7 +450,8 @@ let main () = | Some 0 -> Options.set_verbose false | None | Some _ -> print_wrn_opt ~name:":verbosity" st_loc "integer" value - end + end; + st | ":reproducible-resource-limit", Symbol { name = Simple level; _ } -> begin match int_of_string_opt level with @@ -434,7 +460,38 @@ let main () = | None | Some _ -> print_wrn_opt ~name:":reproducible-resource-limit" st_loc "nonnegative integer" value - end + end; + st + | ":sat-solver", Symbol { name = Simple solver; _ } -> ( + if not (is_solver_ctx_empty (State.get solver_ctx_key st)) then ( + recoverable_error + "error setting ':sat-solver', option value cannot be modified \ + after initialization"; + st + ) else + try + let sat_solver = + match solver with + | "tableaux" -> Util.Tableaux + | "tableaux_cdcl" -> Util.Tableaux_CDCL + | "cdcl" | "satml" -> Util.CDCL + | "cdcl_tableaux" | "satml_tableaux" | "default" -> + Util.CDCL_Tableaux + | _ -> raise Exit + in + Options.set_sat_solver sat_solver; + let is_cdcl_tableaux = + match sat_solver with CDCL_Tableaux -> true | _ -> false + in + Options.set_cdcl_tableaux_inst is_cdcl_tableaux; + Options.set_cdcl_tableaux_th is_cdcl_tableaux; + State.set sat_solver_key (make_sat ()) st + with Exit -> + recoverable_error + "error setting ':sat-solver', invalid option value '%s'" + solver; + st + ) | (":global-declarations" | ":interactive-mode" | ":produce-assertions" @@ -444,16 +501,16 @@ let main () = | ":print-success" | ":random-seed"), _ -> - unsupported_opt name + unsupported_opt name; st (* Alt-Ergo custom options *) | ":profiling", Symbol { name = Simple level; _ } -> begin match float_of_string_opt level with | None -> print_wrn_opt ~name st_loc "nonnegative integer" value | Some i -> Options.set_profiling true i - end + end; st | _ -> - unsupported_opt name + unsupported_opt name; st in let handle_get_info (st : State.t) (name: string) = @@ -467,7 +524,7 @@ let main () = in match State.get partial_model_key st with | None -> err () - | Some sat -> + | Some Model ((module SAT), sat) -> match SAT.get_unknown_reason sat with | None -> err () | Some s -> @@ -503,7 +560,7 @@ let main () = in let handle_stmt : - FE.used_context -> State.t -> + Frontend.used_context -> State.t -> _ D_loop.Typer_Pipe.stmt -> State.t = let goal_cnt = ref 0 in fun all_context st td -> @@ -552,7 +609,9 @@ let main () = List.rev (cnf :: hyps), is_thm | _ -> assert false in - let partial_model = solve all_context (cnf, name) in + let partial_model = + solve (State.get sat_solver_key st) all_context (cnf, name) + in if is_thm then State.set solver_ctx_key ( @@ -574,8 +633,7 @@ let main () = }; loc = l; _ } -> let dloc_file = (State.get State.logic_file st).loc in let loc = DStd.Loc.(lexing_positions (loc dloc_file l)) in - handle_option loc name value; - st + handle_option loc name value st | {contents = `Set_option _; _} -> recoverable_error "Invalid set-option"; @@ -584,7 +642,7 @@ let main () = | {contents = `Get_model; _ } -> if Options.get_interpretation () then match State.get partial_model_key st with - | Some partial_model -> + | Some Model ((module SAT), partial_model) -> begin match SAT.get_model partial_model with | Some (lazy model) -> @@ -656,7 +714,7 @@ let main () = Parser.parse_logic ~preludes logic_file in let st = State.set Typer.additional_builtins D_cnf.builtins st in - let all_used_context = FE.init_all_used_context () in + let all_used_context = Frontend.init_all_used_context () in let finally = finally ~handle_exn in let st = let open Pipeline in diff --git a/src/bin/js/options_interface.ml b/src/bin/js/options_interface.ml index 90eed2bbf..41cf5f150 100644 --- a/src/bin/js/options_interface.ml +++ b/src/bin/js/options_interface.ml @@ -190,7 +190,6 @@ let set_options r = (get_no_decisions_on r.no_decisions_on); set_options_opt Options.set_no_sat_learning r.no_sat_learning; set_options_opt Options.set_sat_solver (get_sat_solver r.sat_solver); - set_options_opt Options.set_tableaux_cdcl r.tableaux_cdcl; set_options_opt Options.set_disable_ites r.disable_ites; set_options_opt Options.set_inline_lets r.inline_lets; diff --git a/src/bin/js/worker_interface.ml b/src/bin/js/worker_interface.ml index b45459d9b..2db23a685 100644 --- a/src/bin/js/worker_interface.ml +++ b/src/bin/js/worker_interface.ml @@ -261,7 +261,6 @@ type options = { no_decisions_on : (string list) option; no_sat_learning : bool option; sat_solver : sat_solver option; - tableaux_cdcl : bool option; disable_ites : bool option; inline_lets : bool option; @@ -365,7 +364,6 @@ let init_options () = { no_decisions_on = None; no_sat_learning = None; sat_solver = None; - tableaux_cdcl = None; disable_ites = None; inline_lets = None; @@ -515,11 +513,10 @@ let opt6_encoding = conv (fun opt6 -> opt6) (fun opt6 -> opt6) - (obj10 + (obj9 (opt "no_decisions_on" (list string)) (opt "no_sat_learning" bool) (opt "sat_solver" sat_solver_encoding) - (opt "tableaux_cdcl" bool) (opt "disable_ites" bool) (opt "inline_lets" bool) (opt "rewriting" bool) @@ -645,7 +642,6 @@ let options_to_json opt = (opt.no_decisions_on, opt.no_sat_learning, opt.sat_solver, - opt.tableaux_cdcl, opt. disable_ites, opt.inline_lets, opt.rewriting, @@ -763,7 +759,6 @@ let options_from_json options = let (no_decisions_on, no_sat_learning, sat_solver, - tableaux_cdcl, disable_ites, inline_lets, rewriting, @@ -851,7 +846,6 @@ let options_from_json options = no_decisions_on; no_sat_learning; sat_solver; - tableaux_cdcl; disable_ites; inline_lets; rewriting; diff --git a/src/bin/js/worker_interface.mli b/src/bin/js/worker_interface.mli index ecb332104..fb01acbd4 100644 --- a/src/bin/js/worker_interface.mli +++ b/src/bin/js/worker_interface.mli @@ -144,7 +144,6 @@ type options = { no_decisions_on : (string list) option; no_sat_learning : bool option; sat_solver : sat_solver option; - tableaux_cdcl : bool option; disable_ites : bool option; inline_lets : bool option; diff --git a/src/bin/js/worker_js.ml b/src/bin/js/worker_js.ml index 4442500ec..0ae54a479 100644 --- a/src/bin/js/worker_js.ml +++ b/src/bin/js/worker_js.ml @@ -110,18 +110,18 @@ let main worker_id content = let get_status_and_print status n = returned_status := begin match status with - | FE.Unsat _ -> Worker_interface.Unsat n - | FE.Inconsistent _ -> Worker_interface.Inconsistent n - | FE.Sat _ -> Worker_interface.Sat n - | FE.Unknown _ -> Worker_interface.Unknown n - | FE.Timeout _ -> Worker_interface.LimitReached "timeout" - | FE.Preprocess -> Worker_interface.Unknown n + | Frontend.Unsat _ -> Worker_interface.Unsat n + | Inconsistent _ -> Worker_interface.Inconsistent n + | Sat _ -> Worker_interface.Sat n + | Unknown _ -> Worker_interface.Unknown n + | Timeout _ -> Worker_interface.LimitReached "timeout" + | Preprocess -> Worker_interface.Unknown n end; - FE.print_status status n + Frontend.print_status status n in let solve all_context (cnf, goal_name) = - let used_context = FE.choose_used_context all_context ~goal_name in + let used_context = Frontend.choose_used_context all_context ~goal_name in let consistent_dep_stack = Stack.create () in SAT.reset_refs (); let env = SAT.empty_with_inst add_inst in @@ -182,7 +182,7 @@ let main worker_id content = Printer.print_err "%a" Errors.report e; raise Exit in - let all_used_context = FE.init_all_used_context () in + let all_used_context = Frontend.init_all_used_context () in let assertion_stack = Stack.create () in let typing_loop state p = try diff --git a/src/lib/frontend/frontend.ml b/src/lib/frontend/frontend.ml index 727f299c6..b6f6331a4 100644 --- a/src/lib/frontend/frontend.ml +++ b/src/lib/frontend/frontend.ml @@ -49,10 +49,94 @@ let unknown_reason_opt_to_string = module E = Expr module Ex = Explanation + +type used_context = Util.SS.t option + +type 'a status = + | Unsat of Commands.sat_tdecl * Ex.t + | Inconsistent of Commands.sat_tdecl + | Sat of Commands.sat_tdecl * 'a + | Unknown of Commands.sat_tdecl * 'a + | Timeout of Commands.sat_tdecl option + | Preprocess + +let print_status status steps = + let check_status_consistency s = + let known_status = get_status () in + match s with + | Unsat _ -> + if known_status == Status_Sat then begin + Printer.print_wrn + "This file is known to be Sat but Alt-Ergo return Unsat"; + Errors.warning_as_error () + end + | Sat _ -> + if known_status == Status_Unsat then begin + Printer.print_wrn + "This file is known to be Unsat but Alt-Ergo return Sat"; + Errors.warning_as_error () + end + | Inconsistent _ | Unknown _ | Timeout _ | Preprocess -> + assert false + in + let validity_mode = + match Options.get_output_format () with + | Smtlib2 -> false + | Native | Why3 | Unknown _ -> true + in + let get_goal_name d = + match d.st_decl with + | Query(g,_,_) -> Some g + | _ -> None + in + + let time = Time.value() in + match status with + | Unsat (d, dep) -> + let loc = d.st_loc in + Printer.print_status_unsat ~validity_mode + (Some loc) (Some time) (Some steps) (get_goal_name d); + if get_unsat_core() && + not (get_debug_unsat_core()) && + not (get_save_used_context()) + then + Printer.print_fmt (Options.Output.get_fmt_regular ()) + "unsat-core:@,%a@." + (Ex.print_unsat_core ~tab:true) dep; + check_status_consistency status; + + | Inconsistent d -> + let loc = d.st_loc in + Printer.print_status_inconsistent ~validity_mode + (Some loc) (Some time) (Some steps) (get_goal_name d); + + | Sat (d, _) -> + let loc = d.st_loc in + Printer.print_status_sat ~validity_mode + (Some loc) (Some time) (Some steps) (get_goal_name d); + check_status_consistency status; + + | Unknown (d, _) -> + let loc = d.st_loc in + Printer.print_status_unknown ~validity_mode + (Some loc) (Some time) (Some steps) (get_goal_name d); + + | Timeout (Some d) -> + let loc = d.st_loc in + Printer.print_status_timeout ~validity_mode + (Some loc) (Some time) (Some steps) (get_goal_name d); + + | Timeout None -> + Printer.print_status_timeout ~validity_mode + None (Some time) (Some steps) None; + + | Preprocess -> + Printer.print_status_preprocess ~validity_mode + (Some time) (Some steps) + module type S = sig type sat_env - type used_context type res = [ | `Sat of sat_env @@ -60,33 +144,59 @@ module type S = sig | `Unsat ] - type status = - | Unsat of Commands.sat_tdecl * Ex.t - | Inconsistent of Commands.sat_tdecl - | Sat of Commands.sat_tdecl * sat_env - | Unknown of Commands.sat_tdecl * sat_env - | Timeout of Commands.sat_tdecl option - | Preprocess - val process_decl: - (status -> int -> unit) -> + (sat_env status -> int -> unit) -> used_context -> (res * Ex.t) Stack.t -> sat_env * res * Ex.t -> Commands.sat_tdecl -> sat_env * res * Ex.t +end - val print_status : status -> int -> unit - - val init_all_used_context : unit -> used_context - val choose_used_context : used_context -> goal_name:string -> used_context +let init_with_replay_used acc f = + assert (Sys.file_exists f); + let cin = open_in f in + let acc = ref (match acc with None -> Util.SS.empty | Some ss -> ss) in + try + while true do acc := Util.SS.add (input_line cin) !acc done; + assert false + with End_of_file -> + Some !acc + +let init_used_context ~goal_name = + if Options.get_replay_used_context () then + let uc_f = + sprintf "%s.%s.used" (Options.get_used_context_file ()) goal_name + in + if Sys.file_exists uc_f then init_with_replay_used None uc_f + else + begin + Printer.print_wrn + "File %s not found! Option -replay-used will be ignored" uc_f; + None + end + else + None + +let init_all_used_context () = + if Options.get_replay_all_used_context () then + let dir = Filename.dirname (Options.get_used_context_file ()) in + Array.fold_left + (fun acc f -> + let f = sprintf "%s/%s" dir f in + if (Filename.check_suffix f ".used") then init_with_replay_used acc f + else acc + ) None (Sys.readdir dir) + else None + +let choose_used_context all_ctxt ~goal_name = + if Options.get_replay_all_used_context () then all_ctxt + else init_used_context ~goal_name -end module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct type sat_env = SAT.t - type used_context = Util.SS.t option type res = [ | `Sat of sat_env @@ -94,14 +204,6 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct | `Unsat ] - type status = - | Unsat of Commands.sat_tdecl * Ex.t - | Inconsistent of Commands.sat_tdecl - | Sat of Commands.sat_tdecl * sat_env - | Unknown of Commands.sat_tdecl * sat_env - | Timeout of Commands.sat_tdecl option - | Preprocess - let output_used_context g_name dep = if not (Options.get_js_mode ()) then begin let f = Options.get_used_context_file () in @@ -309,124 +411,4 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct print_status (Timeout (Some d)) (Steps.get_steps ()); print_model env None; raise e - - let print_status status steps = - let check_status_consistency s = - let known_status = get_status () in - match s with - | Unsat _ -> - if known_status == Status_Sat then begin - Printer.print_wrn - "This file is known to be Sat but Alt-Ergo return Unsat"; - Errors.warning_as_error () - end - | Sat _ -> - if known_status == Status_Unsat then begin - Printer.print_wrn - "This file is known to be Unsat but Alt-Ergo return Sat"; - Errors.warning_as_error () - end - | Inconsistent _ | Unknown _ | Timeout _ | Preprocess -> - assert false - in - let validity_mode = - match Options.get_output_format () with - | Smtlib2 -> false - | Native | Why3 | Unknown _ -> true - in - let get_goal_name d = - match d.st_decl with - | Query(g,_,_) -> Some g - | _ -> None - in - - let time = Time.value() in - match status with - | Unsat (d, dep) -> - let loc = d.st_loc in - Printer.print_status_unsat ~validity_mode - (Some loc) (Some time) (Some steps) (get_goal_name d); - if get_unsat_core() && - not (get_debug_unsat_core()) && - not (get_save_used_context()) - then - Printer.print_fmt (Options.Output.get_fmt_regular ()) - "unsat-core:@,%a@." - (Ex.print_unsat_core ~tab:true) dep; - check_status_consistency status; - - | Inconsistent d -> - let loc = d.st_loc in - Printer.print_status_inconsistent ~validity_mode - (Some loc) (Some time) (Some steps) (get_goal_name d); - - | Sat (d, _) -> - let loc = d.st_loc in - Printer.print_status_sat ~validity_mode - (Some loc) (Some time) (Some steps) (get_goal_name d); - check_status_consistency status; - - | Unknown (d, _) -> - let loc = d.st_loc in - Printer.print_status_unknown ~validity_mode - (Some loc) (Some time) (Some steps) (get_goal_name d); - - | Timeout (Some d) -> - let loc = d.st_loc in - Printer.print_status_timeout ~validity_mode - (Some loc) (Some time) (Some steps) (get_goal_name d); - - | Timeout None -> - Printer.print_status_timeout ~validity_mode - None (Some time) (Some steps) None; - - | Preprocess -> - Printer.print_status_preprocess ~validity_mode - (Some time) (Some steps) - - - - - - - let init_with_replay_used acc f = - assert (Sys.file_exists f); - let cin = open_in f in - let acc = ref (match acc with None -> Util.SS.empty | Some ss -> ss) in - try - while true do acc := Util.SS.add (input_line cin) !acc done; - assert false - with End_of_file -> - Some !acc - - let init_used_context ~goal_name = - if Options.get_replay_used_context () then - let uc_f = - sprintf "%s.%s.used" (Options.get_used_context_file ()) goal_name - in - if Sys.file_exists uc_f then init_with_replay_used None uc_f - else - begin - Printer.print_wrn - "File %s not found! Option -replay-used will be ignored" uc_f; - None - end - else - None - - let init_all_used_context () = - if Options.get_replay_all_used_context () then - let dir = Filename.dirname (Options.get_used_context_file ()) in - Array.fold_left - (fun acc f -> - let f = sprintf "%s/%s" dir f in - if (Filename.check_suffix f ".used") then init_with_replay_used acc f - else acc - ) None (Sys.readdir dir) - else None - - let choose_used_context all_ctxt ~goal_name = - if Options.get_replay_all_used_context () then all_ctxt - else init_used_context ~goal_name - end diff --git a/src/lib/frontend/frontend.mli b/src/lib/frontend/frontend.mli index 768d21833..f78c1914a 100644 --- a/src/lib/frontend/frontend.mli +++ b/src/lib/frontend/frontend.mli @@ -28,10 +28,24 @@ (* *) (**************************************************************************) +type used_context + +val init_all_used_context : unit -> used_context +val choose_used_context : used_context -> goal_name:string -> used_context + +type 'a status = + | Unsat of Commands.sat_tdecl * Explanation.t + | Inconsistent of Commands.sat_tdecl + | Sat of Commands.sat_tdecl * 'a + | Unknown of Commands.sat_tdecl * 'a + | Timeout of Commands.sat_tdecl option + | Preprocess + +val print_status : 'a status -> int -> unit + module type S = sig type sat_env - type used_context type res = [ | `Sat of sat_env @@ -39,27 +53,13 @@ module type S = sig | `Unsat ] - type status = - | Unsat of Commands.sat_tdecl * Explanation.t - | Inconsistent of Commands.sat_tdecl - | Sat of Commands.sat_tdecl * sat_env - | Unknown of Commands.sat_tdecl * sat_env - | Timeout of Commands.sat_tdecl option - | Preprocess - val process_decl: - (status -> int -> unit) -> + (sat_env status -> int -> unit) -> used_context -> (res * Explanation.t) Stack.t -> sat_env * res * Explanation.t -> Commands.sat_tdecl -> sat_env * res * Explanation.t - - val print_status : status -> int -> unit - - val init_all_used_context : unit -> used_context - val choose_used_context : used_context -> goal_name:string -> used_context - end module Make (SAT: Sat_solver_sig.S) : S with type sat_env = SAT.t diff --git a/src/lib/util/options.ml b/src/lib/util/options.ml index f5b420b1b..f9b293f7c 100644 --- a/src/lib/util/options.ml +++ b/src/lib/util/options.ml @@ -469,7 +469,6 @@ let no_decisions_on = ref Util.SS.empty let no_sat_learning = ref false let sat_plugin = ref "" let sat_solver = ref Util.CDCL_Tableaux -let tableaux_cdcl = ref false let set_arith_matching b = arith_matching := b let set_bottom_classes b = bottom_classes := b @@ -486,7 +485,6 @@ let set_no_decisions_on s = no_decisions_on := s let set_no_sat_learning b = no_sat_learning := b let set_sat_plugin p = sat_plugin := p let set_sat_solver s = sat_solver := s -let set_tableaux_cdcl b = tableaux_cdcl := b let get_arith_matching () = !arith_matching let get_bottom_classes () = !bottom_classes @@ -509,7 +507,10 @@ let get_no_sat_learning () = !no_sat_learning let get_sat_learning () = not (!no_sat_learning) let get_sat_plugin () = !sat_plugin let get_sat_solver () = !sat_solver -let get_tableaux_cdcl () = !tableaux_cdcl +let get_tableaux_cdcl () = + match !sat_solver with + | Tableaux_CDCL -> true + | _ -> false (** Term options *) diff --git a/src/lib/util/options.mli b/src/lib/util/options.mli index 9002960b3..a667a43bc 100644 --- a/src/lib/util/options.mli +++ b/src/lib/util/options.mli @@ -424,9 +424,6 @@ val set_sat_plugin : string -> unit (** Set [sat_solver] accessible with {!val:get_sat_solver} *) val set_sat_solver : Util.sat_solver -> unit -(** Set [tableaux_cdcl] accessible with {!val:get_tableaux_cdcl} *) -val set_tableaux_cdcl : bool -> unit - (** Set [disable_ites] accessible with {!val:get_disable_ites} *) val set_disable_ites : bool -> unit