11 val type_encK = "type_enc" |
11 val type_encK = "type_enc" |
12 val soundK = "sound" |
12 val soundK = "sound" |
13 val slicingK = "slicing" |
13 val slicingK = "slicing" |
14 val lambda_translationK = "lambda_translation" |
14 val lambda_translationK = "lambda_translation" |
15 val e_weight_methodK = "e_weight_method" |
15 val e_weight_methodK = "e_weight_method" |
16 val spass_force_sosK = "spass_force_sos" |
16 val force_sosK = "force_sos" |
17 val vampire_force_sosK = "vampire_force_sos" |
|
18 val max_relevantK = "max_relevant" |
17 val max_relevantK = "max_relevant" |
19 val minimizeK = "minimize" |
18 val minimizeK = "minimize" |
20 val minimize_timeoutK = "minimize_timeout" |
19 val minimize_timeoutK = "minimize_timeout" |
21 val metis_ftK = "metis_ft" |
20 val metis_ftK = "metis_ft" |
22 val reconstructorK = "reconstructor" |
21 val reconstructorK = "reconstructor" |
352 SH_OK of int * int * (string * locality) list | |
351 SH_OK of int * int * (string * locality) list | |
353 SH_FAIL of int * int | |
352 SH_FAIL of int * int | |
354 SH_ERROR |
353 SH_ERROR |
355 |
354 |
356 fun run_sh prover_name prover type_enc sound max_relevant slicing |
355 fun run_sh prover_name prover type_enc sound max_relevant slicing |
357 lambda_translation e_weight_method spass_force_sos vampire_force_sos |
356 lambda_translation e_weight_method force_sos hard_timeout timeout dir |
358 hard_timeout timeout dir pos st = |
357 pos st = |
359 let |
358 let |
360 val {context = ctxt, facts = chained_ths, goal} = Proof.goal st |
359 val {context = ctxt, facts = chained_ths, goal} = Proof.goal st |
361 val i = 1 |
360 val i = 1 |
362 fun set_file_name (SOME dir) = |
361 fun set_file_name (SOME dir) = |
363 Config.put Sledgehammer_Provers.dest_dir dir |
362 Config.put Sledgehammer_Provers.dest_dir dir |
373 #> (Option.map (Config.put |
372 #> (Option.map (Config.put |
374 Sledgehammer_Provers.atp_lambda_translation) |
373 Sledgehammer_Provers.atp_lambda_translation) |
375 lambda_translation |> the_default I) |
374 lambda_translation |> the_default I) |
376 #> (Option.map (Config.put ATP_Systems.e_weight_method) |
375 #> (Option.map (Config.put ATP_Systems.e_weight_method) |
377 e_weight_method |> the_default I) |
376 e_weight_method |> the_default I) |
378 #> (Option.map (Config.put ATP_Systems.spass_force_sos) |
377 #> (Option.map (Config.put ATP_Systems.force_sos) |
379 spass_force_sos |> the_default I) |
378 force_sos |> the_default I) |
380 #> (Option.map (Config.put ATP_Systems.vampire_force_sos) |
|
381 vampire_force_sos |> the_default I) |
|
382 #> Config.put Sledgehammer_Provers.measure_run_time true) |
379 #> Config.put Sledgehammer_Provers.measure_run_time true) |
383 val params as {relevance_thresholds, max_relevant, slicing, ...} = |
380 val params as {relevance_thresholds, max_relevant, slicing, ...} = |
384 Sledgehammer_Isar.default_params ctxt |
381 Sledgehammer_Isar.default_params ctxt |
385 [("verbose", "true"), |
382 [("verbose", "true"), |
386 ("type_enc", type_enc), |
383 ("type_enc", type_enc), |
464 val sound = AList.lookup (op =) args soundK |> the_default "false" |
461 val sound = AList.lookup (op =) args soundK |> the_default "false" |
465 val max_relevant = AList.lookup (op =) args max_relevantK |> the_default "smart" |
462 val max_relevant = AList.lookup (op =) args max_relevantK |> the_default "smart" |
466 val slicing = AList.lookup (op =) args slicingK |> the_default "true" |
463 val slicing = AList.lookup (op =) args slicingK |> the_default "true" |
467 val lambda_translation = AList.lookup (op =) args lambda_translationK |
464 val lambda_translation = AList.lookup (op =) args lambda_translationK |
468 val e_weight_method = AList.lookup (op =) args e_weight_methodK |
465 val e_weight_method = AList.lookup (op =) args e_weight_methodK |
469 val spass_force_sos = AList.lookup (op =) args spass_force_sosK |
466 val force_sos = AList.lookup (op =) args force_sosK |
470 |> Option.map (curry (op <>) "false") |
|
471 val vampire_force_sos = AList.lookup (op =) args vampire_force_sosK |
|
472 |> Option.map (curry (op <>) "false") |
467 |> Option.map (curry (op <>) "false") |
473 val dir = AList.lookup (op =) args keepK |
468 val dir = AList.lookup (op =) args keepK |
474 val timeout = Mirabelle.get_int_setting args (prover_timeoutK, 30) |
469 val timeout = Mirabelle.get_int_setting args (prover_timeoutK, 30) |
475 (* always use a hard timeout, but give some slack so that the automatic |
470 (* always use a hard timeout, but give some slack so that the automatic |
476 minimizer has a chance to do its magic *) |
471 minimizer has a chance to do its magic *) |
477 val hard_timeout = SOME (2 * timeout) |
472 val hard_timeout = SOME (2 * timeout) |
478 val (msg, result) = |
473 val (msg, result) = |
479 run_sh prover_name prover type_enc sound max_relevant slicing |
474 run_sh prover_name prover type_enc sound max_relevant slicing |
480 lambda_translation e_weight_method spass_force_sos vampire_force_sos |
475 lambda_translation e_weight_method force_sos hard_timeout timeout dir |
481 hard_timeout timeout dir pos st |
476 pos st |
482 in |
477 in |
483 case result of |
478 case result of |
484 SH_OK (time_isa, time_prover, names) => |
479 SH_OK (time_isa, time_prover, names) => |
485 let |
480 let |
486 fun get_thms (_, ATP_Translate.Chained) = NONE |
481 fun get_thms (_, ATP_Translate.Chained) = NONE |