25 provers: string list, |
25 provers: string list, |
26 type_enc: string option, |
26 type_enc: string option, |
27 strict: bool, |
27 strict: bool, |
28 lam_trans: string option, |
28 lam_trans: string option, |
29 uncurried_aliases: bool option, |
29 uncurried_aliases: bool option, |
30 relevance_thresholds: real * real, |
30 fact_thresholds: real * real, |
31 max_relevant: int option, |
31 max_facts: int option, |
32 max_mono_iters: int option, |
32 max_mono_iters: int option, |
33 max_new_mono_instances: int option, |
33 max_new_mono_instances: int option, |
34 isar_proof: bool, |
34 isar_proof: bool, |
35 isar_shrink_factor: int, |
35 isar_shrink_factor: int, |
36 slice: bool, |
36 slice: bool, |
108 val is_smt_prover : Proof.context -> string -> bool |
108 val is_smt_prover : Proof.context -> string -> bool |
109 val is_ho_atp: Proof.context -> string -> bool |
109 val is_ho_atp: Proof.context -> string -> bool |
110 val is_unit_equational_atp : Proof.context -> string -> bool |
110 val is_unit_equational_atp : Proof.context -> string -> bool |
111 val is_prover_supported : Proof.context -> string -> bool |
111 val is_prover_supported : Proof.context -> string -> bool |
112 val is_prover_installed : Proof.context -> string -> bool |
112 val is_prover_installed : Proof.context -> string -> bool |
113 val default_max_relevant_for_prover : Proof.context -> bool -> string -> int |
113 val default_max_facts_for_prover : Proof.context -> bool -> string -> int |
114 val is_unit_equality : term -> bool |
114 val is_unit_equality : term -> bool |
115 val is_appropriate_prop_for_prover : Proof.context -> string -> term -> bool |
115 val is_appropriate_prop_for_prover : Proof.context -> string -> term -> bool |
116 val is_built_in_const_for_prover : |
116 val is_built_in_const_for_prover : |
117 Proof.context -> string -> string * typ -> term list -> bool * term list |
117 Proof.context -> string -> string * typ -> term list -> bool * term list |
118 val atp_relevance_fudge : relevance_fudge |
118 val atp_relevance_fudge : relevance_fudge |
186 is_atp_installed (Proof_Context.theory_of ctxt) |
186 is_atp_installed (Proof_Context.theory_of ctxt) |
187 |
187 |
188 fun get_slices slice slices = |
188 fun get_slices slice slices = |
189 (0 upto length slices - 1) ~~ slices |> not slice ? (List.last #> single) |
189 (0 upto length slices - 1) ~~ slices |> not slice ? (List.last #> single) |
190 |
190 |
191 val reconstructor_default_max_relevant = 20 |
191 val reconstructor_default_max_facts = 20 |
192 |
192 |
193 fun default_max_relevant_for_prover ctxt slice name = |
193 fun default_max_facts_for_prover ctxt slice name = |
194 let val thy = Proof_Context.theory_of ctxt in |
194 let val thy = Proof_Context.theory_of ctxt in |
195 if is_reconstructor name then |
195 if is_reconstructor name then |
196 reconstructor_default_max_relevant |
196 reconstructor_default_max_facts |
197 else if is_atp thy name then |
197 else if is_atp thy name then |
198 fold (Integer.max o #1 o fst o snd o snd o snd) |
198 fold (Integer.max o #1 o fst o snd o snd o snd) |
199 (get_slices slice (#best_slices (get_atp thy name ()) ctxt)) 0 |
199 (get_slices slice (#best_slices (get_atp thy name ()) ctxt)) 0 |
200 else (* is_smt_prover ctxt name *) |
200 else (* is_smt_prover ctxt name *) |
201 SMT_Solver.default_max_relevant ctxt name |
201 SMT_Solver.default_max_relevant ctxt name |
312 provers: string list, |
312 provers: string list, |
313 type_enc: string option, |
313 type_enc: string option, |
314 strict: bool, |
314 strict: bool, |
315 lam_trans: string option, |
315 lam_trans: string option, |
316 uncurried_aliases: bool option, |
316 uncurried_aliases: bool option, |
317 relevance_thresholds: real * real, |
317 fact_thresholds: real * real, |
318 max_relevant: int option, |
318 max_facts: int option, |
319 max_mono_iters: int option, |
319 max_mono_iters: int option, |
320 max_new_mono_instances: int option, |
320 max_new_mono_instances: int option, |
321 isar_proof: bool, |
321 isar_proof: bool, |
322 isar_shrink_factor: int, |
322 isar_shrink_factor: int, |
323 slice: bool, |
323 slice: bool, |
627 fun run_atp mode name |
627 fun run_atp mode name |
628 ({exec, required_vars, arguments, proof_delims, known_failures, |
628 ({exec, required_vars, arguments, proof_delims, known_failures, |
629 prem_role, best_slices, best_max_mono_iters, |
629 prem_role, best_slices, best_max_mono_iters, |
630 best_max_new_mono_instances, ...} : atp_config) |
630 best_max_new_mono_instances, ...} : atp_config) |
631 (params as {debug, verbose, overlord, type_enc, strict, lam_trans, |
631 (params as {debug, verbose, overlord, type_enc, strict, lam_trans, |
632 uncurried_aliases, max_relevant, max_mono_iters, |
632 uncurried_aliases, max_facts, max_mono_iters, |
633 max_new_mono_instances, isar_proof, isar_shrink_factor, |
633 max_new_mono_instances, isar_proof, isar_shrink_factor, |
634 slice, timeout, preplay_timeout, ...}) |
634 slice, timeout, preplay_timeout, ...}) |
635 minimize_command |
635 minimize_command |
636 ({state, goal, subgoal, subgoal_count, facts, ...} : prover_problem) = |
636 ({state, goal, subgoal, subgoal_count, facts, ...} : prover_problem) = |
637 let |
637 let |
709 |> maps (fn (name, rths) => |
709 |> maps (fn (name, rths) => |
710 map (pair name o zero_var_indexes o snd) rths) |
710 map (pair name o zero_var_indexes o snd) rths) |
711 end |
711 end |
712 fun run_slice time_left (cache_key, cache_value) |
712 fun run_slice time_left (cache_key, cache_value) |
713 (slice, (time_frac, (complete, |
713 (slice, (time_frac, (complete, |
714 (key as (best_max_relevant, format, best_type_enc, |
714 (key as (best_max_facts, format, best_type_enc, |
715 best_lam_trans, best_uncurried_aliases), |
715 best_lam_trans, best_uncurried_aliases), |
716 extra)))) = |
716 extra)))) = |
717 let |
717 let |
718 val num_facts = |
718 val num_facts = |
719 length facts |> is_none max_relevant |
719 length facts |> is_none max_facts ? Integer.min best_max_facts |
720 ? Integer.min best_max_relevant |
|
721 val soundness = if strict then Strict else Non_Strict |
720 val soundness = if strict then Strict else Non_Strict |
722 val type_enc = |
721 val type_enc = |
723 type_enc |> choose_type_enc soundness best_type_enc format |
722 type_enc |> choose_type_enc soundness best_type_enc format |
724 val sound = is_type_enc_sound type_enc |
723 val sound = is_type_enc_sound type_enc |
725 val real_ms = Real.fromInt o Time.toMilliseconds |
724 val real_ms = Real.fromInt o Time.toMilliseconds |