Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Allow dynamic selection of the SAT solver with set-option #880

Merged
merged 1 commit into from
Oct 13, 2023
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion examples/lib_usage.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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 =
Expand Down
3 changes: 0 additions & 3 deletions src/bin/common/parse_command.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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.(
Expand Down
138 changes: 98 additions & 40 deletions src/bin/common/solving_loop.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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 = {
Expand Down Expand Up @@ -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 "@[<v 2>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
Expand All @@ -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
Expand All @@ -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 ();
Expand All @@ -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 ->
Expand Down Expand Up @@ -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.
Expand All @@ -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
Expand All @@ -248,22 +262,27 @@ 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

let solver_ctx_key: solver_ctx State.key =
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

Expand Down Expand Up @@ -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
Expand All @@ -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. *)
Expand All @@ -413,19 +437,21 @@ 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
| Some i when i > 0 -> Options.set_verbose true
| 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
Expand All @@ -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"
Expand All @@ -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) =
Expand All @@ -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 ->
Expand Down Expand Up @@ -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 ->
Expand Down Expand Up @@ -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 (
Expand All @@ -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";
Expand All @@ -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) ->
Expand Down Expand Up @@ -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
Expand Down
1 change: 0 additions & 1 deletion src/bin/js/options_interface.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down
Loading
Loading