equal
deleted
inserted
replaced
33 val minN = "min" |
33 val minN = "min" |
34 val messagesN = "messages" |
34 val messagesN = "messages" |
35 val supported_proversN = "supported_provers" |
35 val supported_proversN = "supported_provers" |
36 val kill_proversN = "kill_provers" |
36 val kill_proversN = "kill_provers" |
37 val running_proversN = "running_provers" |
37 val running_proversN = "running_provers" |
38 val unlearnN = "unlearn" |
|
39 val learnN = "learn" |
|
40 val relearnN = "relearn" |
|
41 val kill_learnersN = "kill_learners" |
38 val kill_learnersN = "kill_learners" |
42 val running_learnersN = "running_learners" |
39 val running_learnersN = "running_learners" |
43 val refresh_tptpN = "refresh_tptp" |
40 val refresh_tptpN = "refresh_tptp" |
44 |
41 |
45 val auto = Unsynchronized.ref false |
42 val auto = Unsynchronized.ref false |
351 |> filter is_raw_param_relevant_for_minimize |
348 |> filter is_raw_param_relevant_for_minimize |
352 |> map string_for_raw_param |
349 |> map string_for_raw_param |
353 |> (if prover_name = default_minimize_prover then I else cons prover_name) |
350 |> (if prover_name = default_minimize_prover then I else cons prover_name) |
354 |> space_implode ", " |
351 |> space_implode ", " |
355 in |
352 in |
356 "sledgehammer" ^ " " ^ minN ^ |
353 sledgehammerN ^ " " ^ minN ^ |
357 (if params = "" then "" else enclose " [" "]" params) ^ |
354 (if params = "" then "" else enclose " [" "]" params) ^ |
358 " (" ^ space_implode " " fact_names ^ ")" ^ |
355 " (" ^ space_implode " " fact_names ^ ")" ^ |
359 (if i = 1 then "" else " " ^ string_of_int i) |
356 (if i = 1 then "" else " " ^ string_of_int i) |
360 end |
357 end |
|
358 |
|
359 val default_learn_atp_timeout = 0.5 |
361 |
360 |
362 fun hammer_away override_params subcommand opt_i fact_override state = |
361 fun hammer_away override_params subcommand opt_i fact_override state = |
363 let |
362 let |
364 val ctxt = Proof.context_of state |
363 val ctxt = Proof.context_of state |
365 val override_params = override_params |> map (normalize_raw_param ctxt) |
364 val override_params = override_params |> map (normalize_raw_param ctxt) |
390 kill_provers () |
389 kill_provers () |
391 else if subcommand = running_proversN then |
390 else if subcommand = running_proversN then |
392 running_provers () |
391 running_provers () |
393 else if subcommand = unlearnN then |
392 else if subcommand = unlearnN then |
394 mash_unlearn ctxt |
393 mash_unlearn ctxt |
395 else if subcommand = learnN orelse subcommand = relearnN then |
394 else if subcommand = learn_isarN orelse subcommand = learn_atpN orelse |
396 (if subcommand = relearnN then mash_unlearn ctxt else (); |
395 subcommand = relearn_isarN orelse subcommand = relearn_atpN then |
|
396 (if subcommand = relearn_isarN orelse subcommand = relearn_atpN then |
|
397 mash_unlearn ctxt |
|
398 else |
|
399 (); |
397 mash_learn ctxt (get_params Normal ctxt |
400 mash_learn ctxt (get_params Normal ctxt |
398 (override_params @ [("verbose", ["true"])]))) |
401 (("timeout", |
|
402 [string_of_real default_learn_atp_timeout]) :: |
|
403 override_params @ |
|
404 [("slice", ["false"]), |
|
405 ("minimize", ["true"]), |
|
406 ("preplay_timeout", ["0"])]))) |
|
407 (subcommand = learn_atpN orelse subcommand = relearn_atpN) |
399 else if subcommand = kill_learnersN then |
408 else if subcommand = kill_learnersN then |
400 kill_learners () |
409 kill_learners () |
401 else if subcommand = running_learnersN then |
410 else if subcommand = running_learnersN then |
402 running_learners () |
411 running_learners () |
403 else if subcommand = refresh_tptpN then |
412 else if subcommand = refresh_tptpN then |
461 in |
470 in |
462 run_sledgehammer (get_params mode ctxt []) mode i no_fact_override |
471 run_sledgehammer (get_params mode ctxt []) mode i no_fact_override |
463 (minimize_command [] i) state |
472 (minimize_command [] i) state |
464 end |
473 end |
465 |
474 |
466 val setup = Try.register_tool ("sledgehammer", (40, auto, try_sledgehammer)) |
475 val setup = Try.register_tool (sledgehammerN, (40, auto, try_sledgehammer)) |
467 |
476 |
468 end; |
477 end; |