7 |
7 |
8 val proverK = "prover" |
8 val proverK = "prover" |
9 val prover_timeoutK = "prover_timeout" |
9 val prover_timeoutK = "prover_timeout" |
10 val keepK = "keep" |
10 val keepK = "keep" |
11 val type_encK = "type_enc" |
11 val type_encK = "type_enc" |
12 val soundK = "sound" |
12 val strictK = "strict" |
13 val sliceK = "slice" |
13 val sliceK = "slice" |
14 val lam_transK = "lam_trans" |
14 val lam_transK = "lam_trans" |
15 val e_weight_methodK = "e_weight_method" |
15 val e_weight_methodK = "e_weight_method" |
16 val force_sosK = "force_sos" |
16 val force_sosK = "force_sos" |
17 val max_relevantK = "max_relevant" |
17 val max_relevantK = "max_relevant" |
359 datatype sh_result = |
359 datatype sh_result = |
360 SH_OK of int * int * (string * stature) list | |
360 SH_OK of int * int * (string * stature) list | |
361 SH_FAIL of int * int | |
361 SH_FAIL of int * int | |
362 SH_ERROR |
362 SH_ERROR |
363 |
363 |
364 fun run_sh prover_name prover type_enc sound max_relevant slice lam_trans |
364 fun run_sh prover_name prover type_enc strict max_relevant slice lam_trans |
365 e_weight_method force_sos hard_timeout timeout dir pos st = |
365 e_weight_method force_sos hard_timeout timeout dir pos st = |
366 let |
366 let |
367 val {context = ctxt, facts = chained_ths, goal} = Proof.goal st |
367 val {context = ctxt, facts = chained_ths, goal} = Proof.goal st |
368 val i = 1 |
368 val i = 1 |
369 fun set_file_name (SOME dir) = |
369 fun set_file_name (SOME dir) = |
383 force_sos |> the_default I)) |
383 force_sos |> the_default I)) |
384 val params as {relevance_thresholds, max_relevant, slice, ...} = |
384 val params as {relevance_thresholds, max_relevant, slice, ...} = |
385 Sledgehammer_Isar.default_params ctxt |
385 Sledgehammer_Isar.default_params ctxt |
386 [("verbose", "true"), |
386 [("verbose", "true"), |
387 ("type_enc", type_enc), |
387 ("type_enc", type_enc), |
388 ("sound", sound), |
388 ("strict", strict), |
389 ("lam_trans", lam_trans |> the_default "smart"), |
389 ("lam_trans", lam_trans |> the_default "smart"), |
390 ("preplay_timeout", preplay_timeout), |
390 ("preplay_timeout", preplay_timeout), |
391 ("max_relevant", max_relevant), |
391 ("max_relevant", max_relevant), |
392 ("slice", slice), |
392 ("slice", slice), |
393 ("timeout", string_of_int timeout), |
393 ("timeout", string_of_int timeout), |
465 val triv_str = if trivial then "[T] " else "" |
465 val triv_str = if trivial then "[T] " else "" |
466 val _ = change_data id inc_sh_calls |
466 val _ = change_data id inc_sh_calls |
467 val _ = if trivial then () else change_data id inc_sh_nontriv_calls |
467 val _ = if trivial then () else change_data id inc_sh_nontriv_calls |
468 val (prover_name, prover) = get_prover (Proof.context_of st) args |
468 val (prover_name, prover) = get_prover (Proof.context_of st) args |
469 val type_enc = AList.lookup (op =) args type_encK |> the_default "smart" |
469 val type_enc = AList.lookup (op =) args type_encK |> the_default "smart" |
470 val sound = AList.lookup (op =) args soundK |> the_default "false" |
470 val strict = AList.lookup (op =) args strictK |> the_default "false" |
471 val max_relevant = AList.lookup (op =) args max_relevantK |> the_default "smart" |
471 val max_relevant = AList.lookup (op =) args max_relevantK |> the_default "smart" |
472 val slice = AList.lookup (op =) args sliceK |> the_default "true" |
472 val slice = AList.lookup (op =) args sliceK |> the_default "true" |
473 val lam_trans = AList.lookup (op =) args lam_transK |
473 val lam_trans = AList.lookup (op =) args lam_transK |
474 val e_weight_method = AList.lookup (op =) args e_weight_methodK |
474 val e_weight_method = AList.lookup (op =) args e_weight_methodK |
475 val force_sos = AList.lookup (op =) args force_sosK |
475 val force_sos = AList.lookup (op =) args force_sosK |
478 val timeout = Mirabelle.get_int_setting args (prover_timeoutK, 30) |
478 val timeout = Mirabelle.get_int_setting args (prover_timeoutK, 30) |
479 (* always use a hard timeout, but give some slack so that the automatic |
479 (* always use a hard timeout, but give some slack so that the automatic |
480 minimizer has a chance to do its magic *) |
480 minimizer has a chance to do its magic *) |
481 val hard_timeout = SOME (2 * timeout) |
481 val hard_timeout = SOME (2 * timeout) |
482 val (msg, result) = |
482 val (msg, result) = |
483 run_sh prover_name prover type_enc sound max_relevant slice lam_trans |
483 run_sh prover_name prover type_enc strict max_relevant slice lam_trans |
484 e_weight_method force_sos hard_timeout timeout dir pos st |
484 e_weight_method force_sos hard_timeout timeout dir pos st |
485 in |
485 in |
486 case result of |
486 case result of |
487 SH_OK (time_isa, time_prover, names) => |
487 SH_OK (time_isa, time_prover, names) => |
488 let |
488 let |
515 let |
515 let |
516 val ctxt = Proof.context_of st |
516 val ctxt = Proof.context_of st |
517 val n0 = length (these (!named_thms)) |
517 val n0 = length (these (!named_thms)) |
518 val (prover_name, _) = get_prover ctxt args |
518 val (prover_name, _) = get_prover ctxt args |
519 val type_enc = AList.lookup (op =) args type_encK |> the_default "smart" |
519 val type_enc = AList.lookup (op =) args type_encK |> the_default "smart" |
520 val sound = AList.lookup (op =) args soundK |> the_default "false" |
520 val strict = AList.lookup (op =) args strictK |> the_default "false" |
521 val timeout = |
521 val timeout = |
522 AList.lookup (op =) args minimize_timeoutK |
522 AList.lookup (op =) args minimize_timeoutK |
523 |> Option.map (fst o read_int o raw_explode) (* FIXME Symbol.explode (?) *) |
523 |> Option.map (fst o read_int o raw_explode) (* FIXME Symbol.explode (?) *) |
524 |> the_default 5 |
524 |> the_default 5 |
525 val params = Sledgehammer_Isar.default_params ctxt |
525 val params = Sledgehammer_Isar.default_params ctxt |
526 [("provers", prover_name), |
526 [("provers", prover_name), |
527 ("verbose", "true"), |
527 ("verbose", "true"), |
528 ("type_enc", type_enc), |
528 ("type_enc", type_enc), |
529 ("sound", sound), |
529 ("strict", strict), |
530 ("timeout", string_of_int timeout), |
530 ("timeout", string_of_int timeout), |
531 ("preplay_timeout", preplay_timeout)] |
531 ("preplay_timeout", preplay_timeout)] |
532 val minimize = |
532 val minimize = |
533 Sledgehammer_Minimize.minimize_facts prover_name params |
533 Sledgehammer_Minimize.minimize_facts prover_name params |
534 true 1 (Sledgehammer_Util.subgoal_count st) |
534 true 1 (Sledgehammer_Util.subgoal_count st) |
552 |
552 |
553 fun override_params prover type_enc timeout = |
553 fun override_params prover type_enc timeout = |
554 [("provers", prover), |
554 [("provers", prover), |
555 ("max_relevant", "0"), |
555 ("max_relevant", "0"), |
556 ("type_enc", type_enc), |
556 ("type_enc", type_enc), |
557 ("sound", "true"), |
557 ("strict", "true"), |
558 ("slice", "false"), |
558 ("slice", "false"), |
559 ("timeout", timeout |> Time.toSeconds |> string_of_int)] |
559 ("timeout", timeout |> Time.toSeconds |> string_of_int)] |
560 |
560 |
561 fun run_reconstructor trivial full m name reconstructor named_thms id |
561 fun run_reconstructor trivial full m name reconstructor named_thms id |
562 ({pre=st, timeout, log, pos, ...}: Mirabelle.run_args) = |
562 ({pre=st, timeout, log, pos, ...}: Mirabelle.run_args) = |