64 val smt_weight_curve : (int -> int) Unsynchronized.ref |
66 val smt_weight_curve : (int -> int) Unsynchronized.ref |
65 val smt_max_iters : int Unsynchronized.ref |
67 val smt_max_iters : int Unsynchronized.ref |
66 val smt_iter_fact_frac : real Unsynchronized.ref |
68 val smt_iter_fact_frac : real Unsynchronized.ref |
67 val smt_iter_time_frac : real Unsynchronized.ref |
69 val smt_iter_time_frac : real Unsynchronized.ref |
68 val smt_iter_min_msecs : int Unsynchronized.ref |
70 val smt_iter_min_msecs : int Unsynchronized.ref |
69 val smt_monomorphize_limit : int Unsynchronized.ref |
|
70 |
71 |
71 val das_Tool : string |
72 val das_Tool : string |
72 val select_smt_solver : string -> Proof.context -> Proof.context |
73 val select_smt_solver : string -> Proof.context -> Proof.context |
73 val is_smt_prover : Proof.context -> string -> bool |
74 val is_smt_prover : Proof.context -> string -> bool |
74 val is_prover_supported : Proof.context -> string -> bool |
75 val is_prover_supported : Proof.context -> string -> bool |
227 {debug: bool, |
228 {debug: bool, |
228 verbose: bool, |
229 verbose: bool, |
229 overlord: bool, |
230 overlord: bool, |
230 blocking: bool, |
231 blocking: bool, |
231 provers: string list, |
232 provers: string list, |
|
233 relevance_thresholds: real * real, |
|
234 max_relevant: int option, |
|
235 monomorphize: bool, |
|
236 monomorphize_limit: int, |
232 type_sys: type_system, |
237 type_sys: type_system, |
233 explicit_apply: bool, |
238 explicit_apply: bool, |
234 relevance_thresholds: real * real, |
|
235 max_relevant: int option, |
|
236 isar_proof: bool, |
239 isar_proof: bool, |
237 isar_shrink_factor: int, |
240 isar_shrink_factor: int, |
238 timeout: Time.time, |
241 timeout: Time.time, |
239 expect: string} |
242 expect: string} |
240 |
243 |
331 |
334 |
332 fun run_atp auto name |
335 fun run_atp auto name |
333 ({exec, required_execs, arguments, has_incomplete_mode, proof_delims, |
336 ({exec, required_execs, arguments, has_incomplete_mode, proof_delims, |
334 known_failures, explicit_forall, use_conjecture_for_hypotheses, ...} |
337 known_failures, explicit_forall, use_conjecture_for_hypotheses, ...} |
335 : atp_config) |
338 : atp_config) |
336 ({debug, verbose, overlord, type_sys, explicit_apply, isar_proof, |
339 ({debug, verbose, overlord, monomorphize, monomorphize_limit, type_sys, |
337 isar_shrink_factor, timeout, ...} : params) |
340 explicit_apply, isar_proof, isar_shrink_factor, timeout, ...} |
|
341 : params) |
338 minimize_command ({state, goal, subgoal, facts, ...} : prover_problem) = |
342 minimize_command ({state, goal, subgoal, facts, ...} : prover_problem) = |
339 let |
343 let |
340 val ctxt = Proof.context_of state |
344 val ctxt = Proof.context_of state |
341 val (_, hyp_ts, concl_t) = strip_subgoal goal subgoal |
345 val (_, hyp_ts, concl_t) = strip_subgoal goal subgoal |
342 val facts = facts |> map (atp_translated_fact ctxt) |
346 fun monomorphize_facts facts = |
|
347 let |
|
348 val facts = facts |> map untranslated_fact |
|
349 val indexed_facts = |
|
350 (~1, goal) :: (0 upto length facts - 1 ~~ map snd facts) |
|
351 in |
|
352 ctxt |> Config.put SMT_Config.monomorph_limit monomorphize_limit |
|
353 |> SMT_Monomorph.monomorph indexed_facts |> fst |
|
354 |> sort (int_ord o pairself fst) |
|
355 |> filter_out (curry (op =) ~1 o fst) |
|
356 |> map (Untranslated_Fact o apfst (fst o nth facts)) |
|
357 end |
|
358 val facts = facts |> monomorphize ? monomorphize_facts |
|
359 |> map (atp_translated_fact ctxt) |
343 val (dest_dir, problem_prefix) = |
360 val (dest_dir, problem_prefix) = |
344 if overlord then overlord_file_location_for_prover name |
361 if overlord then overlord_file_location_for_prover name |
345 else (Config.get ctxt dest_dir, Config.get ctxt problem_prefix) |
362 else (Config.get ctxt dest_dir, Config.get ctxt problem_prefix) |
346 val problem_file_name = |
363 val problem_file_name = |
347 Path.basic (problem_prefix ^ (if overlord then "" else serial_string ()) ^ |
364 Path.basic (problem_prefix ^ (if overlord then "" else serial_string ()) ^ |
511 (* FUDGE *) |
528 (* FUDGE *) |
512 val smt_max_iters = Unsynchronized.ref 8 |
529 val smt_max_iters = Unsynchronized.ref 8 |
513 val smt_iter_fact_frac = Unsynchronized.ref 0.5 |
530 val smt_iter_fact_frac = Unsynchronized.ref 0.5 |
514 val smt_iter_time_frac = Unsynchronized.ref 0.5 |
531 val smt_iter_time_frac = Unsynchronized.ref 0.5 |
515 val smt_iter_min_msecs = Unsynchronized.ref 5000 |
532 val smt_iter_min_msecs = Unsynchronized.ref 5000 |
516 val smt_monomorphize_limit = Unsynchronized.ref 4 |
533 |
517 |
534 fun smt_filter_loop name ({debug, verbose, overlord, monomorphize_limit, |
518 fun smt_filter_loop name ({debug, verbose, overlord, timeout, ...} : params) |
535 timeout, ...} : params) |
519 state i smt_filter = |
536 state i smt_filter = |
520 let |
537 let |
521 val ctxt = Proof.context_of state |
538 val ctxt = Proof.context_of state |
522 val repair_context = |
539 val repair_context = |
523 select_smt_solver name |
540 select_smt_solver name |
527 (overlord_file_location_for_prover name |
544 (overlord_file_location_for_prover name |
528 |> (fn (path, name) => path ^ "/" ^ name)) |
545 |> (fn (path, name) => path ^ "/" ^ name)) |
529 else |
546 else |
530 I) |
547 I) |
531 #> Config.put SMT_Config.infer_triggers (!smt_triggers) |
548 #> Config.put SMT_Config.infer_triggers (!smt_triggers) |
532 #> Config.put SMT_Config.monomorph_limit (!smt_monomorphize_limit) |
549 #> Config.put SMT_Config.monomorph_limit monomorphize_limit |
533 val state = state |> Proof.map_context repair_context |
550 val state = state |> Proof.map_context repair_context |
534 |
551 |
535 fun iter timeout iter_num outcome0 time_so_far facts = |
552 fun iter timeout iter_num outcome0 time_so_far facts = |
536 let |
553 let |
537 val timer = Timer.startRealTimer () |
554 val timer = Timer.startRealTimer () |