equal
deleted
inserted
replaced
224 val max_default_remote_threads = 4 |
224 val max_default_remote_threads = 4 |
225 |
225 |
226 (* The first ATP of the list is used by Auto Sledgehammer. Because of the low |
226 (* The first ATP of the list is used by Auto Sledgehammer. Because of the low |
227 timeout, it makes sense to put E first. *) |
227 timeout, it makes sense to put E first. *) |
228 fun default_provers_param_value ctxt = |
228 fun default_provers_param_value ctxt = |
229 [eN, spassN, vampireN, z3N, e_sineN, waldmeisterN, yicesN, cvc3N] |
229 [eN, spassN, vampireN, z3N, e_sineN, waldmeisterN, yicesN] |
230 |> map_filter (remotify_prover_if_not_installed ctxt) |
230 |> map_filter (remotify_prover_if_not_installed ctxt) |
231 |> avoid_too_many_threads ctxt (Multithreading.max_threads_value (), |
231 |> avoid_too_many_threads ctxt (Multithreading.max_threads_value (), |
232 max_default_remote_threads) |
232 max_default_remote_threads) |
233 |> implode_param |
233 |> implode_param |
234 |
234 |
402 (if subcommand = relearn_isarN orelse subcommand = relearn_atpN then |
402 (if subcommand = relearn_isarN orelse subcommand = relearn_atpN then |
403 mash_unlearn ctxt |
403 mash_unlearn ctxt |
404 else |
404 else |
405 (); |
405 (); |
406 mash_learn ctxt (get_params Normal ctxt |
406 mash_learn ctxt (get_params Normal ctxt |
407 (("timeout", |
407 ([("timeout", |
408 [string_of_real default_learn_atp_timeout]) :: |
408 [string_of_real default_learn_atp_timeout]), |
|
409 ("slice", ["false"])] @ |
409 override_params @ |
410 override_params @ |
410 [("slice", ["false"]), |
411 [("minimize", ["true"]), |
411 ("minimize", ["true"]), |
|
412 ("preplay_timeout", ["0"])])) |
412 ("preplay_timeout", ["0"])])) |
413 fact_override (#facts (Proof.goal state)) |
413 fact_override (#facts (Proof.goal state)) |
414 (subcommand = learn_atpN orelse subcommand = relearn_atpN)) |
414 (subcommand = learn_atpN orelse subcommand = relearn_atpN)) |
415 else if subcommand = kill_learnersN then |
415 else if subcommand = kill_learnersN then |
416 kill_learners () |
416 kill_learners () |