34 open Sledgehammer_Util |
34 open Sledgehammer_Util |
35 open Sledgehammer_Proof_Methods |
35 open Sledgehammer_Proof_Methods |
36 open Sledgehammer_Isar |
36 open Sledgehammer_Isar |
37 open Sledgehammer_Prover |
37 open Sledgehammer_Prover |
38 |
38 |
39 val smt_builtins = Attrib.setup_config_bool @{binding sledgehammer_smt_builtins} (K true) |
39 val smt_builtins = Attrib.setup_config_bool \<^binding>\<open>sledgehammer_smt_builtins\<close> (K true) |
40 val smt_triggers = Attrib.setup_config_bool @{binding sledgehammer_smt_triggers} (K true) |
40 val smt_triggers = Attrib.setup_config_bool \<^binding>\<open>sledgehammer_smt_triggers\<close> (K true) |
41 |
41 |
42 val is_smt_prover = member (op =) o SMT_Config.available_solvers_of |
42 val is_smt_prover = member (op =) o SMT_Config.available_solvers_of |
43 |
43 |
44 (* "SMT_Failure.Abnormal_Termination" carries the solver's return code. Until these are sorted out |
44 (* "SMT_Failure.Abnormal_Termination" carries the solver's return code. Until these are sorted out |
45 properly in the SMT module, we must interpret these here. *) |
45 properly in the SMT module, we must interpret these here. *) |
63 | NONE => UnknownError ("Abnormal termination with exit code " ^ string_of_int code)) |
63 | NONE => UnknownError ("Abnormal termination with exit code " ^ string_of_int code)) |
64 | failure_of_smt_failure SMT_Failure.Out_Of_Memory = OutOfResources |
64 | failure_of_smt_failure SMT_Failure.Out_Of_Memory = OutOfResources |
65 | failure_of_smt_failure (SMT_Failure.Other_Failure s) = UnknownError s |
65 | failure_of_smt_failure (SMT_Failure.Other_Failure s) = UnknownError s |
66 |
66 |
67 (* FUDGE *) |
67 (* FUDGE *) |
68 val smt_max_slices = Attrib.setup_config_int @{binding sledgehammer_smt_max_slices} (K 8) |
68 val smt_max_slices = Attrib.setup_config_int \<^binding>\<open>sledgehammer_smt_max_slices\<close> (K 8) |
69 val smt_slice_fact_frac = |
69 val smt_slice_fact_frac = |
70 Attrib.setup_config_real @{binding sledgehammer_smt_slice_fact_frac} (K 0.667) |
70 Attrib.setup_config_real \<^binding>\<open>sledgehammer_smt_slice_fact_frac\<close> (K 0.667) |
71 val smt_slice_time_frac = |
71 val smt_slice_time_frac = |
72 Attrib.setup_config_real @{binding sledgehammer_smt_slice_time_frac} (K 0.333) |
72 Attrib.setup_config_real \<^binding>\<open>sledgehammer_smt_slice_time_frac\<close> (K 0.333) |
73 val smt_slice_min_secs = Attrib.setup_config_int @{binding sledgehammer_smt_slice_min_secs} (K 3) |
73 val smt_slice_min_secs = Attrib.setup_config_int \<^binding>\<open>sledgehammer_smt_slice_min_secs\<close> (K 3) |
74 |
74 |
75 val is_boring_builtin_typ = |
75 val is_boring_builtin_typ = |
76 not o exists_subtype (member (op =) [@{typ nat}, @{typ int}, HOLogic.realT]) |
76 not o exists_subtype (member (op =) [\<^typ>\<open>nat\<close>, \<^typ>\<open>int\<close>, HOLogic.realT]) |
77 |
77 |
78 fun smt_filter_loop name ({debug, overlord, max_mono_iters, max_new_mono_instances, timeout, slice, |
78 fun smt_filter_loop name ({debug, overlord, max_mono_iters, max_new_mono_instances, timeout, slice, |
79 ...} : params) state goal i = |
79 ...} : params) state goal i = |
80 let |
80 let |
81 fun repair_context ctxt = |
81 fun repair_context ctxt = |