src/HOL/Tools/Sledgehammer/sledgehammer.ML
author blanchet
Mon, 31 Jan 2022 16:09:23 +0100
changeset 75031 ae4dc5ac983f
parent 75030 919fb49ba201
child 75032 8d08bc7e8f98
permissions -rw-r--r--
implemented 'max_proofs' mechanism
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
55202
824c48a539c9 renamed many Sledgehammer ML files to clarify structure
blanchet
parents: 55201
diff changeset
     1
(*  Title:      HOL/Tools/Sledgehammer/sledgehammer.ML
28477
9339d4dcec8b version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff changeset
     2
    Author:     Fabian Immler, TU Muenchen
32996
d2e48879e65a removed disjunctive group cancellation -- provers run independently;
wenzelm
parents: 32995
diff changeset
     3
    Author:     Makarius
35969
c9565298df9e added support for Sledgehammer parameters;
blanchet
parents: 35867
diff changeset
     4
    Author:     Jasmin Blanchette, TU Muenchen
28477
9339d4dcec8b version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff changeset
     5
38021
e024504943d1 rename "ATP_Manager" ML module to "Sledgehammer";
blanchet
parents: 38020
diff changeset
     6
Sledgehammer's heart.
28477
9339d4dcec8b version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff changeset
     7
*)
9339d4dcec8b version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff changeset
     8
55202
824c48a539c9 renamed many Sledgehammer ML files to clarify structure
blanchet
parents: 55201
diff changeset
     9
signature SLEDGEHAMMER =
28477
9339d4dcec8b version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff changeset
    10
sig
60612
79d71bfea310 removed chained facts from preplaying -- and careful about extra chained facts when removing 'proof -' and 'qed' from one-line Isar proofs
blanchet
parents: 60549
diff changeset
    11
  type stature = ATP_Problem_Generate.stature
51008
e096c0dc538b more precise output of selected facts
blanchet
parents: 51007
diff changeset
    12
  type fact = Sledgehammer_Fact.fact
48292
7fcee834c7f5 more code rationalization in relevance filter
blanchet
parents: 48289
diff changeset
    13
  type fact_override = Sledgehammer_Fact.fact_override
57755
e081db351356 export ML function
blanchet
parents: 57750
diff changeset
    14
  type proof_method = Sledgehammer_Proof_Methods.proof_method
e081db351356 export ML function
blanchet
parents: 57750
diff changeset
    15
  type play_outcome = Sledgehammer_Proof_Methods.play_outcome
55201
1ee776da8da7 renamed ML file
blanchet
parents: 54816
diff changeset
    16
  type mode = Sledgehammer_Prover.mode
1ee776da8da7 renamed ML file
blanchet
parents: 54816
diff changeset
    17
  type params = Sledgehammer_Prover.params
74951
0b6f795d3b78 proper filtering inf induction rules in Mirabelle
desharna
parents: 74950
diff changeset
    18
  type induction_rules = Sledgehammer_Prover.induction_rules
74952
ae2185967e67 exported Sledgehammer.launch_prover and use it in Mirabelle
desharna
parents: 74951
diff changeset
    19
  type prover_problem = Sledgehammer_Prover.prover_problem
ae2185967e67 exported Sledgehammer.launch_prover and use it in Mirabelle
desharna
parents: 74951
diff changeset
    20
  type prover_result = Sledgehammer_Prover.prover_result
40061
71cc5aac8b76 generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents: 40060
diff changeset
    21
75020
b087610592b4 rationalized output for forthcoming slicing model
blanchet
parents: 75019
diff changeset
    22
  datatype sledgehammer_outcome =
b087610592b4 rationalized output for forthcoming slicing model
blanchet
parents: 75019
diff changeset
    23
    SH_Some of prover_result
b087610592b4 rationalized output for forthcoming slicing model
blanchet
parents: 75019
diff changeset
    24
  | SH_Unknown
b087610592b4 rationalized output for forthcoming slicing model
blanchet
parents: 75019
diff changeset
    25
  | SH_Timeout
b087610592b4 rationalized output for forthcoming slicing model
blanchet
parents: 75019
diff changeset
    26
  | SH_None
74953
aade20a03edb tuned run_sledgehammer and called it directly from Mirabelle
desharna
parents: 74952
diff changeset
    27
aade20a03edb tuned run_sledgehammer and called it directly from Mirabelle
desharna
parents: 74952
diff changeset
    28
  val short_string_of_sledgehammer_outcome : sledgehammer_outcome -> string
55212
blanchet
parents: 55202
diff changeset
    29
60612
79d71bfea310 removed chained facts from preplaying -- and careful about extra chained facts when removing 'proof -' and 'qed' from one-line Isar proofs
blanchet
parents: 60549
diff changeset
    30
  val play_one_line_proof : bool -> Time.time -> (string * stature) list -> Proof.state -> int ->
79d71bfea310 removed chained facts from preplaying -- and careful about extra chained facts when removing 'proof -' and 'qed' from one-line Isar proofs
blanchet
parents: 60549
diff changeset
    31
    proof_method * proof_method list list -> (string * stature) list * (proof_method * play_outcome)
51010
afd0213a3dab tuned data structure
blanchet
parents: 51009
diff changeset
    32
  val string_of_factss : (string * fact list) list -> string
54816
10d48c2a3e32 made timeouts in Sledgehammer not be 'option's -- simplified lots of code
blanchet
parents: 54799
diff changeset
    33
  val run_sledgehammer : params -> mode -> (string -> unit) option -> int -> fact_override ->
74953
aade20a03edb tuned run_sledgehammer and called it directly from Mirabelle
desharna
parents: 74952
diff changeset
    34
    Proof.state -> bool * (sledgehammer_outcome * string)
28477
9339d4dcec8b version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff changeset
    35
end;
9339d4dcec8b version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff changeset
    36
55202
824c48a539c9 renamed many Sledgehammer ML files to clarify structure
blanchet
parents: 55201
diff changeset
    37
structure Sledgehammer : SLEDGEHAMMER =
28477
9339d4dcec8b version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff changeset
    38
struct
9339d4dcec8b version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff changeset
    39
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
    40
open ATP_Util
75029
dc6769b86fd6 crude implementation of centralized slicing
blanchet
parents: 75027
diff changeset
    41
open ATP_Problem
55212
blanchet
parents: 55202
diff changeset
    42
open ATP_Proof
46320
0b8b73b49848 renamed two files to make room for a new file
blanchet
parents: 46301
diff changeset
    43
open ATP_Problem_Generate
38023
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
    44
open Sledgehammer_Util
48250
1065c307fafe further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents: 47904
diff changeset
    45
open Sledgehammer_Fact
55287
ffa306239316 renamed ML file
blanchet
parents: 55286
diff changeset
    46
open Sledgehammer_Proof_Methods
57734
18bb3e1ff6f6 rationalized preplaying by eliminating (now superfluous) laziness
blanchet
parents: 57557
diff changeset
    47
open Sledgehammer_Isar_Proof
18bb3e1ff6f6 rationalized preplaying by eliminating (now superfluous) laziness
blanchet
parents: 57557
diff changeset
    48
open Sledgehammer_Isar_Preplay
57740
25d498554c48 further minimize one-liner
blanchet
parents: 57739
diff changeset
    49
open Sledgehammer_Isar_Minimize
75029
dc6769b86fd6 crude implementation of centralized slicing
blanchet
parents: 75027
diff changeset
    50
open Sledgehammer_ATP_Systems
55201
1ee776da8da7 renamed ML file
blanchet
parents: 54816
diff changeset
    51
open Sledgehammer_Prover
55212
blanchet
parents: 55202
diff changeset
    52
open Sledgehammer_Prover_ATP
55202
824c48a539c9 renamed many Sledgehammer ML files to clarify structure
blanchet
parents: 55201
diff changeset
    53
open Sledgehammer_Prover_Minimize
48381
1b7d798460bb renamed ML structures
blanchet
parents: 48321
diff changeset
    54
open Sledgehammer_MaSh
40072
27f2a45b0aab more robust handling of "remote_" vs. non-"remote_" provers
blanchet
parents: 40071
diff changeset
    55
75020
b087610592b4 rationalized output for forthcoming slicing model
blanchet
parents: 75019
diff changeset
    56
datatype sledgehammer_outcome =
b087610592b4 rationalized output for forthcoming slicing model
blanchet
parents: 75019
diff changeset
    57
  SH_Some of prover_result
b087610592b4 rationalized output for forthcoming slicing model
blanchet
parents: 75019
diff changeset
    58
| SH_Unknown
b087610592b4 rationalized output for forthcoming slicing model
blanchet
parents: 75019
diff changeset
    59
| SH_Timeout
b087610592b4 rationalized output for forthcoming slicing model
blanchet
parents: 75019
diff changeset
    60
| SH_None
74953
aade20a03edb tuned run_sledgehammer and called it directly from Mirabelle
desharna
parents: 74952
diff changeset
    61
aade20a03edb tuned run_sledgehammer and called it directly from Mirabelle
desharna
parents: 74952
diff changeset
    62
fun short_string_of_sledgehammer_outcome (SH_Some _) = "some"
aade20a03edb tuned run_sledgehammer and called it directly from Mirabelle
desharna
parents: 74952
diff changeset
    63
  | short_string_of_sledgehammer_outcome SH_Unknown = "unknown"
aade20a03edb tuned run_sledgehammer and called it directly from Mirabelle
desharna
parents: 74952
diff changeset
    64
  | short_string_of_sledgehammer_outcome SH_Timeout = "timeout"
aade20a03edb tuned run_sledgehammer and called it directly from Mirabelle
desharna
parents: 74952
diff changeset
    65
  | short_string_of_sledgehammer_outcome SH_None = "none"
aade20a03edb tuned run_sledgehammer and called it directly from Mirabelle
desharna
parents: 74952
diff changeset
    66
aade20a03edb tuned run_sledgehammer and called it directly from Mirabelle
desharna
parents: 74952
diff changeset
    67
fun alternative f (SOME x) (SOME y) = SOME (f (x, y))
aade20a03edb tuned run_sledgehammer and called it directly from Mirabelle
desharna
parents: 74952
diff changeset
    68
  | alternative _ (x as SOME _) NONE = x
aade20a03edb tuned run_sledgehammer and called it directly from Mirabelle
desharna
parents: 74952
diff changeset
    69
  | alternative _ NONE (y as SOME _) = y
aade20a03edb tuned run_sledgehammer and called it directly from Mirabelle
desharna
parents: 74952
diff changeset
    70
  | alternative _ NONE NONE = NONE
aade20a03edb tuned run_sledgehammer and called it directly from Mirabelle
desharna
parents: 74952
diff changeset
    71
aade20a03edb tuned run_sledgehammer and called it directly from Mirabelle
desharna
parents: 74952
diff changeset
    72
fun max_outcome outcomes =
aade20a03edb tuned run_sledgehammer and called it directly from Mirabelle
desharna
parents: 74952
diff changeset
    73
  let
75020
b087610592b4 rationalized output for forthcoming slicing model
blanchet
parents: 75019
diff changeset
    74
    val result = find_first (fn (SH_Some _, _) => true | _ => false) outcomes
74953
aade20a03edb tuned run_sledgehammer and called it directly from Mirabelle
desharna
parents: 74952
diff changeset
    75
    val unknown = find_first (fn (SH_Unknown, _) => true | _ => false) outcomes
aade20a03edb tuned run_sledgehammer and called it directly from Mirabelle
desharna
parents: 74952
diff changeset
    76
    val timeout = find_first (fn (SH_Timeout, _) => true | _ => false) outcomes
aade20a03edb tuned run_sledgehammer and called it directly from Mirabelle
desharna
parents: 74952
diff changeset
    77
    val none = find_first (fn (SH_None, _) => true | _ => false) outcomes
aade20a03edb tuned run_sledgehammer and called it directly from Mirabelle
desharna
parents: 74952
diff changeset
    78
  in
75020
b087610592b4 rationalized output for forthcoming slicing model
blanchet
parents: 75019
diff changeset
    79
    result
74953
aade20a03edb tuned run_sledgehammer and called it directly from Mirabelle
desharna
parents: 74952
diff changeset
    80
    |> alternative snd unknown
aade20a03edb tuned run_sledgehammer and called it directly from Mirabelle
desharna
parents: 74952
diff changeset
    81
    |> alternative snd timeout
aade20a03edb tuned run_sledgehammer and called it directly from Mirabelle
desharna
parents: 74952
diff changeset
    82
    |> alternative snd none
aade20a03edb tuned run_sledgehammer and called it directly from Mirabelle
desharna
parents: 74952
diff changeset
    83
    |> the_default (SH_Unknown, "")
aade20a03edb tuned run_sledgehammer and called it directly from Mirabelle
desharna
parents: 74952
diff changeset
    84
  end
43020
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43006
diff changeset
    85
63311
540cfb14a751 be more careful before filtering out chained facts in Sledgehammer
blanchet
parents: 63097
diff changeset
    86
fun play_one_line_proof minimize timeout used_facts state i (preferred_meth, methss) =
540cfb14a751 be more careful before filtering out chained facts in Sledgehammer
blanchet
parents: 63097
diff changeset
    87
  (if timeout = Time.zeroTime then
540cfb14a751 be more careful before filtering out chained facts in Sledgehammer
blanchet
parents: 63097
diff changeset
    88
     (used_facts, (preferred_meth, Play_Timed_Out Time.zeroTime))
540cfb14a751 be more careful before filtering out chained facts in Sledgehammer
blanchet
parents: 63097
diff changeset
    89
   else
540cfb14a751 be more careful before filtering out chained facts in Sledgehammer
blanchet
parents: 63097
diff changeset
    90
     let
540cfb14a751 be more careful before filtering out chained facts in Sledgehammer
blanchet
parents: 63097
diff changeset
    91
       val ctxt = Proof.context_of state
60548
e6adb8868478 use right context for preplay, to avoid errors in fact lookup
blanchet
parents: 59582
diff changeset
    92
73975
8d93f9ca6518 revisited ac28714b7478: more faithful preplaying with chained facts
blanchet
parents: 73940
diff changeset
    93
       val fact_names = used_facts |> filter_out (fn (_, (sc, _)) => sc = Chained) |> map fst
63311
540cfb14a751 be more careful before filtering out chained facts in Sledgehammer
blanchet
parents: 63097
diff changeset
    94
       val {facts = chained, goal, ...} = Proof.goal state
540cfb14a751 be more careful before filtering out chained facts in Sledgehammer
blanchet
parents: 63097
diff changeset
    95
       val goal_t = Logic.get_goal (Thm.prop_of goal) i
57734
18bb3e1ff6f6 rationalized preplaying by eliminating (now superfluous) laziness
blanchet
parents: 57557
diff changeset
    96
63311
540cfb14a751 be more careful before filtering out chained facts in Sledgehammer
blanchet
parents: 63097
diff changeset
    97
       fun try_methss [] [] = (used_facts, (preferred_meth, Play_Timed_Out Time.zeroTime))
540cfb14a751 be more careful before filtering out chained facts in Sledgehammer
blanchet
parents: 63097
diff changeset
    98
         | try_methss ress [] =
540cfb14a751 be more careful before filtering out chained facts in Sledgehammer
blanchet
parents: 63097
diff changeset
    99
           (used_facts,
540cfb14a751 be more careful before filtering out chained facts in Sledgehammer
blanchet
parents: 63097
diff changeset
   100
            (case AList.lookup (op =) ress preferred_meth of
540cfb14a751 be more careful before filtering out chained facts in Sledgehammer
blanchet
parents: 63097
diff changeset
   101
              SOME play => (preferred_meth, play)
540cfb14a751 be more careful before filtering out chained facts in Sledgehammer
blanchet
parents: 63097
diff changeset
   102
            | NONE => hd (sort (play_outcome_ord o apply2 snd) (rev ress))))
540cfb14a751 be more careful before filtering out chained facts in Sledgehammer
blanchet
parents: 63097
diff changeset
   103
         | try_methss ress (meths :: methss) =
540cfb14a751 be more careful before filtering out chained facts in Sledgehammer
blanchet
parents: 63097
diff changeset
   104
           let
540cfb14a751 be more careful before filtering out chained facts in Sledgehammer
blanchet
parents: 63097
diff changeset
   105
             fun mk_step fact_names meths =
72584
4ea19e5dc67e Tuned isar_step datatype
desharna
parents: 71794
diff changeset
   106
               Prove {
4ea19e5dc67e Tuned isar_step datatype
desharna
parents: 71794
diff changeset
   107
                 qualifiers = [],
4ea19e5dc67e Tuned isar_step datatype
desharna
parents: 71794
diff changeset
   108
                 obtains = [],
4ea19e5dc67e Tuned isar_step datatype
desharna
parents: 71794
diff changeset
   109
                 label = ("", 0),
4ea19e5dc67e Tuned isar_step datatype
desharna
parents: 71794
diff changeset
   110
                 goal = goal_t,
4ea19e5dc67e Tuned isar_step datatype
desharna
parents: 71794
diff changeset
   111
                 subproofs = [],
4ea19e5dc67e Tuned isar_step datatype
desharna
parents: 71794
diff changeset
   112
                 facts = ([], fact_names),
4ea19e5dc67e Tuned isar_step datatype
desharna
parents: 71794
diff changeset
   113
                 proof_methods = meths,
4ea19e5dc67e Tuned isar_step datatype
desharna
parents: 71794
diff changeset
   114
                 comment = ""}
63311
540cfb14a751 be more careful before filtering out chained facts in Sledgehammer
blanchet
parents: 63097
diff changeset
   115
           in
73975
8d93f9ca6518 revisited ac28714b7478: more faithful preplaying with chained facts
blanchet
parents: 73940
diff changeset
   116
             (case preplay_isar_step ctxt chained timeout [] (mk_step fact_names meths) of
63311
540cfb14a751 be more careful before filtering out chained facts in Sledgehammer
blanchet
parents: 63097
diff changeset
   117
               (res as (meth, Played time)) :: _ =>
75029
dc6769b86fd6 crude implementation of centralized slicing
blanchet
parents: 75027
diff changeset
   118
               if not minimize then
63311
540cfb14a751 be more careful before filtering out chained facts in Sledgehammer
blanchet
parents: 63097
diff changeset
   119
                 (used_facts, res)
540cfb14a751 be more careful before filtering out chained facts in Sledgehammer
blanchet
parents: 63097
diff changeset
   120
               else
540cfb14a751 be more careful before filtering out chained facts in Sledgehammer
blanchet
parents: 63097
diff changeset
   121
                 let
540cfb14a751 be more careful before filtering out chained facts in Sledgehammer
blanchet
parents: 63097
diff changeset
   122
                   val (time', used_names') =
540cfb14a751 be more careful before filtering out chained facts in Sledgehammer
blanchet
parents: 63097
diff changeset
   123
                     minimized_isar_step ctxt chained time (mk_step fact_names [meth])
540cfb14a751 be more careful before filtering out chained facts in Sledgehammer
blanchet
parents: 63097
diff changeset
   124
                     ||> (facts_of_isar_step #> snd)
540cfb14a751 be more careful before filtering out chained facts in Sledgehammer
blanchet
parents: 63097
diff changeset
   125
                   val used_facts' = filter (member (op =) used_names' o fst) used_facts
540cfb14a751 be more careful before filtering out chained facts in Sledgehammer
blanchet
parents: 63097
diff changeset
   126
                 in
540cfb14a751 be more careful before filtering out chained facts in Sledgehammer
blanchet
parents: 63097
diff changeset
   127
                   (used_facts', (meth, Played time'))
540cfb14a751 be more careful before filtering out chained facts in Sledgehammer
blanchet
parents: 63097
diff changeset
   128
                 end
540cfb14a751 be more careful before filtering out chained facts in Sledgehammer
blanchet
parents: 63097
diff changeset
   129
             | ress' => try_methss (ress' @ ress) methss)
540cfb14a751 be more careful before filtering out chained facts in Sledgehammer
blanchet
parents: 63097
diff changeset
   130
           end
540cfb14a751 be more careful before filtering out chained facts in Sledgehammer
blanchet
parents: 63097
diff changeset
   131
     in
540cfb14a751 be more careful before filtering out chained facts in Sledgehammer
blanchet
parents: 63097
diff changeset
   132
       try_methss [] methss
540cfb14a751 be more careful before filtering out chained facts in Sledgehammer
blanchet
parents: 63097
diff changeset
   133
     end)
540cfb14a751 be more careful before filtering out chained facts in Sledgehammer
blanchet
parents: 63097
diff changeset
   134
  |> (fn (used_facts, (meth, play)) =>
73975
8d93f9ca6518 revisited ac28714b7478: more faithful preplaying with chained facts
blanchet
parents: 73940
diff changeset
   135
        (used_facts |> filter_out (fn (_, (sc, _)) => sc = Chained), (meth, play)))
57734
18bb3e1ff6f6 rationalized preplaying by eliminating (now superfluous) laziness
blanchet
parents: 57557
diff changeset
   136
75027
a8efa30c380d take 'induction_rules' into consideration, as well as 'max_facts' even when 'only' is set
blanchet
parents: 75026
diff changeset
   137
fun launch_prover (params as {verbose, spy, ...}) mode learn
75025
f741d55a81e5 thread slices through
blanchet
parents: 75020
diff changeset
   138
    (problem as {state, subgoal, factss, ...} : prover_problem) slice name =
41089
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   139
  let
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   140
    val ctxt = Proof.context_of state
53800
ac1ec5065316 added "spy" option to Sledgehammer
blanchet
parents: 53549
diff changeset
   141
73975
8d93f9ca6518 revisited ac28714b7478: more faithful preplaying with chained facts
blanchet
parents: 73940
diff changeset
   142
    val _ = spying spy (fn () => (state, subgoal, name, "Launched"))
53800
ac1ec5065316 added "spy" option to Sledgehammer
blanchet
parents: 53549
diff changeset
   143
51009
e8ff34a1fa9a thread through fact triple component from which used facts come, for accurate index output
blanchet
parents: 51008
diff changeset
   144
    fun print_used_facts used_facts used_from =
e8ff34a1fa9a thread through fact triple component from which used facts come, for accurate index output
blanchet
parents: 51008
diff changeset
   145
      tag_list 1 used_from
51005
ce4290c33d73 eliminated needless speed optimization -- and simplified code quite a bit
blanchet
parents: 51004
diff changeset
   146
      |> map (fn (j, fact) => fact |> apsnd (K j))
48798
9152e66f98da be less aggressive at kicking out chained facts
blanchet
parents: 48407
diff changeset
   147
      |> filter_used_facts false used_facts
48394
82fc8c956cdc fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
blanchet
parents: 48384
diff changeset
   148
      |> map (fn ((name, _), j) => name ^ "@" ^ string_of_int j)
82fc8c956cdc fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
blanchet
parents: 48384
diff changeset
   149
      |> commas
75025
f741d55a81e5 thread slices through
blanchet
parents: 75020
diff changeset
   150
      |> prefix ("Facts in " ^ name ^ " proof: ")
58843
521cea5fa777 discontinued obsolete Output.urgent_message;
wenzelm
parents: 58501
diff changeset
   151
      |> writeln
53800
ac1ec5065316 added "spy" option to Sledgehammer
blanchet
parents: 53549
diff changeset
   152
54062
427380d5d1d7 more Sledgehammer spying -- record fact indices
blanchet
parents: 54057
diff changeset
   153
    fun spying_str_of_res ({outcome = NONE, used_facts, used_from, ...} : prover_result) =
427380d5d1d7 more Sledgehammer spying -- record fact indices
blanchet
parents: 54057
diff changeset
   154
        let
427380d5d1d7 more Sledgehammer spying -- record fact indices
blanchet
parents: 54057
diff changeset
   155
          val num_used_facts = length used_facts
54063
c0658286aa08 more thorough spying
blanchet
parents: 54062
diff changeset
   156
c0658286aa08 more thorough spying
blanchet
parents: 54062
diff changeset
   157
          fun find_indices facts =
c0658286aa08 more thorough spying
blanchet
parents: 54062
diff changeset
   158
            tag_list 1 facts
54062
427380d5d1d7 more Sledgehammer spying -- record fact indices
blanchet
parents: 54057
diff changeset
   159
            |> map (fn (j, fact) => fact |> apsnd (K j))
427380d5d1d7 more Sledgehammer spying -- record fact indices
blanchet
parents: 54057
diff changeset
   160
            |> filter_used_facts false used_facts
54773
79f66cd15d57 fixed source of 'Subscript' exception
blanchet
parents: 54503
diff changeset
   161
            |> distinct (eq_fst (op =))
54062
427380d5d1d7 more Sledgehammer spying -- record fact indices
blanchet
parents: 54057
diff changeset
   162
            |> map (prefix "@" o string_of_int o snd)
54063
c0658286aa08 more thorough spying
blanchet
parents: 54062
diff changeset
   163
c0658286aa08 more thorough spying
blanchet
parents: 54062
diff changeset
   164
          fun filter_info (fact_filter, facts) =
c0658286aa08 more thorough spying
blanchet
parents: 54062
diff changeset
   165
            let
c0658286aa08 more thorough spying
blanchet
parents: 54062
diff changeset
   166
              val indices = find_indices facts
54773
79f66cd15d57 fixed source of 'Subscript' exception
blanchet
parents: 54503
diff changeset
   167
              (* "Int.max" is there for robustness -- it shouldn't be necessary *)
79f66cd15d57 fixed source of 'Subscript' exception
blanchet
parents: 54503
diff changeset
   168
              val unknowns = replicate (Int.max (0, num_used_facts - length indices)) "?"
79f66cd15d57 fixed source of 'Subscript' exception
blanchet
parents: 54503
diff changeset
   169
            in
79f66cd15d57 fixed source of 'Subscript' exception
blanchet
parents: 54503
diff changeset
   170
              (commas (indices @ unknowns), fact_filter)
79f66cd15d57 fixed source of 'Subscript' exception
blanchet
parents: 54503
diff changeset
   171
            end
54063
c0658286aa08 more thorough spying
blanchet
parents: 54062
diff changeset
   172
c0658286aa08 more thorough spying
blanchet
parents: 54062
diff changeset
   173
          val filter_infos =
75025
f741d55a81e5 thread slices through
blanchet
parents: 75020
diff changeset
   174
            map filter_info (("actual", used_from) :: factss)
54063
c0658286aa08 more thorough spying
blanchet
parents: 54062
diff changeset
   175
            |> AList.group (op =)
c0658286aa08 more thorough spying
blanchet
parents: 54062
diff changeset
   176
            |> map (fn (indices, fact_filters) => commas fact_filters ^ ": " ^ indices)
54062
427380d5d1d7 more Sledgehammer spying -- record fact indices
blanchet
parents: 54057
diff changeset
   177
        in
75025
f741d55a81e5 thread slices through
blanchet
parents: 75020
diff changeset
   178
          "Success: Found proof with " ^ string_of_int num_used_facts ^ " fact" ^
f741d55a81e5 thread slices through
blanchet
parents: 75020
diff changeset
   179
          plural_s num_used_facts ^
54063
c0658286aa08 more thorough spying
blanchet
parents: 54062
diff changeset
   180
          (if num_used_facts = 0 then "" else ": " ^ commas filter_infos)
53800
ac1ec5065316 added "spy" option to Sledgehammer
blanchet
parents: 53549
diff changeset
   181
        end
ac1ec5065316 added "spy" option to Sledgehammer
blanchet
parents: 53549
diff changeset
   182
      | spying_str_of_res {outcome = SOME failure, ...} =
54062
427380d5d1d7 more Sledgehammer spying -- record fact indices
blanchet
parents: 54057
diff changeset
   183
        "Failure: " ^ string_of_atp_failure failure
74952
ae2185967e67 exported Sledgehammer.launch_prover and use it in Mirabelle
desharna
parents: 74951
diff changeset
   184
 in
75025
f741d55a81e5 thread slices through
blanchet
parents: 75020
diff changeset
   185
  get_minimizing_prover ctxt mode learn name params problem slice
74952
ae2185967e67 exported Sledgehammer.launch_prover and use it in Mirabelle
desharna
parents: 74951
diff changeset
   186
  |> verbose ? tap (fn {outcome = NONE, used_facts as _ :: _, used_from, ...} =>
ae2185967e67 exported Sledgehammer.launch_prover and use it in Mirabelle
desharna
parents: 74951
diff changeset
   187
      print_used_facts used_facts used_from
ae2185967e67 exported Sledgehammer.launch_prover and use it in Mirabelle
desharna
parents: 74951
diff changeset
   188
    | _ => ())
ae2185967e67 exported Sledgehammer.launch_prover and use it in Mirabelle
desharna
parents: 74951
diff changeset
   189
  |> spy ? tap (fn res => spying spy (fn () => (state, subgoal, name, spying_str_of_res res)))
ae2185967e67 exported Sledgehammer.launch_prover and use it in Mirabelle
desharna
parents: 74951
diff changeset
   190
 end
ae2185967e67 exported Sledgehammer.launch_prover and use it in Mirabelle
desharna
parents: 74951
diff changeset
   191
ae2185967e67 exported Sledgehammer.launch_prover and use it in Mirabelle
desharna
parents: 74951
diff changeset
   192
fun preplay_prover_result ({ minimize, preplay_timeout, ...} : params) state subgoal
74953
aade20a03edb tuned run_sledgehammer and called it directly from Mirabelle
desharna
parents: 74952
diff changeset
   193
    (result as {outcome, used_facts, preferred_methss, message, ...} : prover_result) =
74952
ae2185967e67 exported Sledgehammer.launch_prover and use it in Mirabelle
desharna
parents: 74951
diff changeset
   194
  let
ae2185967e67 exported Sledgehammer.launch_prover and use it in Mirabelle
desharna
parents: 74951
diff changeset
   195
    val output =
ae2185967e67 exported Sledgehammer.launch_prover and use it in Mirabelle
desharna
parents: 74951
diff changeset
   196
      if outcome = SOME ATP_Proof.TimedOut then
74953
aade20a03edb tuned run_sledgehammer and called it directly from Mirabelle
desharna
parents: 74952
diff changeset
   197
        SH_Timeout
74952
ae2185967e67 exported Sledgehammer.launch_prover and use it in Mirabelle
desharna
parents: 74951
diff changeset
   198
      else if is_some outcome then
74953
aade20a03edb tuned run_sledgehammer and called it directly from Mirabelle
desharna
parents: 74952
diff changeset
   199
        SH_None
74952
ae2185967e67 exported Sledgehammer.launch_prover and use it in Mirabelle
desharna
parents: 74951
diff changeset
   200
      else
74953
aade20a03edb tuned run_sledgehammer and called it directly from Mirabelle
desharna
parents: 74952
diff changeset
   201
        SH_Some result
74952
ae2185967e67 exported Sledgehammer.launch_prover and use it in Mirabelle
desharna
parents: 74951
diff changeset
   202
    fun output_message () = message (fn () =>
ae2185967e67 exported Sledgehammer.launch_prover and use it in Mirabelle
desharna
parents: 74951
diff changeset
   203
      play_one_line_proof minimize preplay_timeout used_facts state subgoal preferred_methss)
ae2185967e67 exported Sledgehammer.launch_prover and use it in Mirabelle
desharna
parents: 74951
diff changeset
   204
  in
ae2185967e67 exported Sledgehammer.launch_prover and use it in Mirabelle
desharna
parents: 74951
diff changeset
   205
    (output, output_message)
ae2185967e67 exported Sledgehammer.launch_prover and use it in Mirabelle
desharna
parents: 74951
diff changeset
   206
  end
ae2185967e67 exported Sledgehammer.launch_prover and use it in Mirabelle
desharna
parents: 74951
diff changeset
   207
74953
aade20a03edb tuned run_sledgehammer and called it directly from Mirabelle
desharna
parents: 74952
diff changeset
   208
fun check_expected_outcome ctxt prover_name expect outcome =
aade20a03edb tuned run_sledgehammer and called it directly from Mirabelle
desharna
parents: 74952
diff changeset
   209
  let
aade20a03edb tuned run_sledgehammer and called it directly from Mirabelle
desharna
parents: 74952
diff changeset
   210
    val outcome_code = short_string_of_sledgehammer_outcome outcome
aade20a03edb tuned run_sledgehammer and called it directly from Mirabelle
desharna
parents: 74952
diff changeset
   211
  in
75027
a8efa30c380d take 'induction_rules' into consideration, as well as 'max_facts' even when 'only' is set
blanchet
parents: 75026
diff changeset
   212
    (* The "expect" argument is deliberately ignored if the prover is missing so that
a8efa30c380d take 'induction_rules' into consideration, as well as 'max_facts' even when 'only' is set
blanchet
parents: 75026
diff changeset
   213
       "Metis_Examples" can be processed on any machine. *)
74953
aade20a03edb tuned run_sledgehammer and called it directly from Mirabelle
desharna
parents: 74952
diff changeset
   214
    if expect = "" orelse outcome_code = expect orelse
aade20a03edb tuned run_sledgehammer and called it directly from Mirabelle
desharna
parents: 74952
diff changeset
   215
       not (is_prover_installed ctxt prover_name) then
aade20a03edb tuned run_sledgehammer and called it directly from Mirabelle
desharna
parents: 74952
diff changeset
   216
      ()
aade20a03edb tuned run_sledgehammer and called it directly from Mirabelle
desharna
parents: 74952
diff changeset
   217
    else
aade20a03edb tuned run_sledgehammer and called it directly from Mirabelle
desharna
parents: 74952
diff changeset
   218
      error ("Unexpected outcome: " ^ quote outcome_code)
aade20a03edb tuned run_sledgehammer and called it directly from Mirabelle
desharna
parents: 74952
diff changeset
   219
  end
aade20a03edb tuned run_sledgehammer and called it directly from Mirabelle
desharna
parents: 74952
diff changeset
   220
75027
a8efa30c380d take 'induction_rules' into consideration, as well as 'max_facts' even when 'only' is set
blanchet
parents: 75026
diff changeset
   221
fun launch_prover_and_preplay (params as {debug, timeout, expect, ...}) mode writeln_result learn
a8efa30c380d take 'induction_rules' into consideration, as well as 'max_facts' even when 'only' is set
blanchet
parents: 75026
diff changeset
   222
    (problem as {state, subgoal, ...}) slice prover_name =
74952
ae2185967e67 exported Sledgehammer.launch_prover and use it in Mirabelle
desharna
parents: 74951
diff changeset
   223
  let
ae2185967e67 exported Sledgehammer.launch_prover and use it in Mirabelle
desharna
parents: 74951
diff changeset
   224
    val ctxt = Proof.context_of state
ae2185967e67 exported Sledgehammer.launch_prover and use it in Mirabelle
desharna
parents: 74951
diff changeset
   225
    val hard_timeout = Time.scale 5.0 timeout
53800
ac1ec5065316 added "spy" option to Sledgehammer
blanchet
parents: 53549
diff changeset
   226
41255
a80024d7b71b added debugging option to find out how good the relevance filter was at identifying relevant facts
blanchet
parents: 41245
diff changeset
   227
    fun really_go () =
75027
a8efa30c380d take 'induction_rules' into consideration, as well as 'max_facts' even when 'only' is set
blanchet
parents: 75026
diff changeset
   228
      launch_prover params mode learn problem slice prover_name
74952
ae2185967e67 exported Sledgehammer.launch_prover and use it in Mirabelle
desharna
parents: 74951
diff changeset
   229
      |> preplay_prover_result params state subgoal
53800
ac1ec5065316 added "spy" option to Sledgehammer
blanchet
parents: 53549
diff changeset
   230
41089
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   231
    fun go () =
74953
aade20a03edb tuned run_sledgehammer and called it directly from Mirabelle
desharna
parents: 74952
diff changeset
   232
      if debug then
aade20a03edb tuned run_sledgehammer and called it directly from Mirabelle
desharna
parents: 74952
diff changeset
   233
        really_go ()
aade20a03edb tuned run_sledgehammer and called it directly from Mirabelle
desharna
parents: 74952
diff changeset
   234
      else
aade20a03edb tuned run_sledgehammer and called it directly from Mirabelle
desharna
parents: 74952
diff changeset
   235
        (really_go ()
aade20a03edb tuned run_sledgehammer and called it directly from Mirabelle
desharna
parents: 74952
diff changeset
   236
         handle
aade20a03edb tuned run_sledgehammer and called it directly from Mirabelle
desharna
parents: 74952
diff changeset
   237
           ERROR msg => (SH_Unknown, fn () => "Error: " ^ msg ^ "\n")
aade20a03edb tuned run_sledgehammer and called it directly from Mirabelle
desharna
parents: 74952
diff changeset
   238
         | exn =>
aade20a03edb tuned run_sledgehammer and called it directly from Mirabelle
desharna
parents: 74952
diff changeset
   239
           if Exn.is_interrupt exn then Exn.reraise exn
aade20a03edb tuned run_sledgehammer and called it directly from Mirabelle
desharna
parents: 74952
diff changeset
   240
           else (SH_Unknown, fn () => "Internal error:\n" ^ Runtime.exn_message exn ^ "\n"))
57056
8b2283566f6e properly reconstruct helpers in Z3 proofs
blanchet
parents: 57053
diff changeset
   241
74953
aade20a03edb tuned run_sledgehammer and called it directly from Mirabelle
desharna
parents: 74952
diff changeset
   242
    val (outcome, message) = Timeout.apply hard_timeout go ()
aade20a03edb tuned run_sledgehammer and called it directly from Mirabelle
desharna
parents: 74952
diff changeset
   243
    val () = check_expected_outcome ctxt prover_name expect outcome
aade20a03edb tuned run_sledgehammer and called it directly from Mirabelle
desharna
parents: 74952
diff changeset
   244
aade20a03edb tuned run_sledgehammer and called it directly from Mirabelle
desharna
parents: 74952
diff changeset
   245
    val message = message ()
aade20a03edb tuned run_sledgehammer and called it directly from Mirabelle
desharna
parents: 74952
diff changeset
   246
    val () =
75020
b087610592b4 rationalized output for forthcoming slicing model
blanchet
parents: 75019
diff changeset
   247
      (case outcome of
b087610592b4 rationalized output for forthcoming slicing model
blanchet
parents: 75019
diff changeset
   248
        SH_Some _ =>
b087610592b4 rationalized output for forthcoming slicing model
blanchet
parents: 75019
diff changeset
   249
        the_default writeln writeln_result (prover_name ^ ": " ^ message)
b087610592b4 rationalized output for forthcoming slicing model
blanchet
parents: 75019
diff changeset
   250
      | _ => ())
41089
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   251
  in
74953
aade20a03edb tuned run_sledgehammer and called it directly from Mirabelle
desharna
parents: 74952
diff changeset
   252
    (outcome, message)
41089
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   253
  end
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   254
51008
e096c0dc538b more precise output of selected facts
blanchet
parents: 51007
diff changeset
   255
fun string_of_facts facts =
57384
085e85cc6eea tuned output
blanchet
parents: 57368
diff changeset
   256
  "Including " ^ string_of_int (length facts) ^ " relevant fact" ^ plural_s (length facts) ^ ": " ^
63692
1bc4bc2c9fd1 killed final stops in Sledgehammer and friends
blanchet
parents: 63311
diff changeset
   257
  (facts |> map (fst o fst) |> space_implode " ")
51008
e096c0dc538b more precise output of selected facts
blanchet
parents: 51007
diff changeset
   258
51010
afd0213a3dab tuned data structure
blanchet
parents: 51009
diff changeset
   259
fun string_of_factss factss =
57464
3e94eb1124b0 tuned message
blanchet
parents: 57387
diff changeset
   260
  if forall (null o snd) factss then
63692
1bc4bc2c9fd1 killed final stops in Sledgehammer and friends
blanchet
parents: 63311
diff changeset
   261
    "Found no relevant facts"
57464
3e94eb1124b0 tuned message
blanchet
parents: 57387
diff changeset
   262
  else
3e94eb1124b0 tuned message
blanchet
parents: 57387
diff changeset
   263
    cat_lines (map (fn (filter, facts) =>
75020
b087610592b4 rationalized output for forthcoming slicing model
blanchet
parents: 75019
diff changeset
   264
      (if filter = "" then "" else filter ^ ": ") ^ string_of_facts facts) factss)
51008
e096c0dc538b more precise output of selected facts
blanchet
parents: 51007
diff changeset
   265
75029
dc6769b86fd6 crude implementation of centralized slicing
blanchet
parents: 75027
diff changeset
   266
val default_slice_schedule =
dc6769b86fd6 crude implementation of centralized slicing
blanchet
parents: 75027
diff changeset
   267
  (* FUDGE (based on Seventeen evaluation) *)
dc6769b86fd6 crude implementation of centralized slicing
blanchet
parents: 75027
diff changeset
   268
  [cvc4N, zipperpositionN, vampireN, veritN, eN, cvc4N, zipperpositionN, cvc4N, vampireN, cvc4N,
dc6769b86fd6 crude implementation of centralized slicing
blanchet
parents: 75027
diff changeset
   269
   cvc4N, vampireN, cvc4N, eN, iproverN, zipperpositionN, vampireN, eN, vampireN, zipperpositionN,
dc6769b86fd6 crude implementation of centralized slicing
blanchet
parents: 75027
diff changeset
   270
   z3N, cvc4N, vampireN, iproverN, vampireN, zipperpositionN, z3N, z3N, cvc4N, cvc4N]
dc6769b86fd6 crude implementation of centralized slicing
blanchet
parents: 75027
diff changeset
   271
dc6769b86fd6 crude implementation of centralized slicing
blanchet
parents: 75027
diff changeset
   272
fun schedule_of_provers provers num_slices =
dc6769b86fd6 crude implementation of centralized slicing
blanchet
parents: 75027
diff changeset
   273
  let
dc6769b86fd6 crude implementation of centralized slicing
blanchet
parents: 75027
diff changeset
   274
    val num_default_slices = length default_slice_schedule
dc6769b86fd6 crude implementation of centralized slicing
blanchet
parents: 75027
diff changeset
   275
    val unknown_provers = filter_out (member (op =) default_slice_schedule) provers
dc6769b86fd6 crude implementation of centralized slicing
blanchet
parents: 75027
diff changeset
   276
dc6769b86fd6 crude implementation of centralized slicing
blanchet
parents: 75027
diff changeset
   277
    fun round_robin _ [] = []
dc6769b86fd6 crude implementation of centralized slicing
blanchet
parents: 75027
diff changeset
   278
      | round_robin 0 _ = []
dc6769b86fd6 crude implementation of centralized slicing
blanchet
parents: 75027
diff changeset
   279
      | round_robin n (prover :: provers) = prover :: round_robin (n - 1) (provers @ [prover])
dc6769b86fd6 crude implementation of centralized slicing
blanchet
parents: 75027
diff changeset
   280
  in
dc6769b86fd6 crude implementation of centralized slicing
blanchet
parents: 75027
diff changeset
   281
    if num_slices <= num_default_slices then
dc6769b86fd6 crude implementation of centralized slicing
blanchet
parents: 75027
diff changeset
   282
      take num_slices default_slice_schedule
dc6769b86fd6 crude implementation of centralized slicing
blanchet
parents: 75027
diff changeset
   283
    else
dc6769b86fd6 crude implementation of centralized slicing
blanchet
parents: 75027
diff changeset
   284
      default_slice_schedule @ round_robin (num_slices - num_default_slices) unknown_provers
dc6769b86fd6 crude implementation of centralized slicing
blanchet
parents: 75027
diff changeset
   285
  end
dc6769b86fd6 crude implementation of centralized slicing
blanchet
parents: 75027
diff changeset
   286
dc6769b86fd6 crude implementation of centralized slicing
blanchet
parents: 75027
diff changeset
   287
fun prover_slices_of_schedule ctxt schedule =
dc6769b86fd6 crude implementation of centralized slicing
blanchet
parents: 75027
diff changeset
   288
  let
dc6769b86fd6 crude implementation of centralized slicing
blanchet
parents: 75027
diff changeset
   289
    fun triplicate_slices original =
dc6769b86fd6 crude implementation of centralized slicing
blanchet
parents: 75027
diff changeset
   290
      let
dc6769b86fd6 crude implementation of centralized slicing
blanchet
parents: 75027
diff changeset
   291
        val shift =
dc6769b86fd6 crude implementation of centralized slicing
blanchet
parents: 75027
diff changeset
   292
          map (apfst (apsnd (fn fact_filter =>
dc6769b86fd6 crude implementation of centralized slicing
blanchet
parents: 75027
diff changeset
   293
            if fact_filter = mashN then mepoN
dc6769b86fd6 crude implementation of centralized slicing
blanchet
parents: 75027
diff changeset
   294
            else if fact_filter = mepoN then meshN
dc6769b86fd6 crude implementation of centralized slicing
blanchet
parents: 75027
diff changeset
   295
            else mashN)))
dc6769b86fd6 crude implementation of centralized slicing
blanchet
parents: 75027
diff changeset
   296
dc6769b86fd6 crude implementation of centralized slicing
blanchet
parents: 75027
diff changeset
   297
        val shifted_once = shift original
dc6769b86fd6 crude implementation of centralized slicing
blanchet
parents: 75027
diff changeset
   298
        val shifted_twice = shift shifted_once
dc6769b86fd6 crude implementation of centralized slicing
blanchet
parents: 75027
diff changeset
   299
      in
dc6769b86fd6 crude implementation of centralized slicing
blanchet
parents: 75027
diff changeset
   300
        original @ shifted_once @ shifted_twice
dc6769b86fd6 crude implementation of centralized slicing
blanchet
parents: 75027
diff changeset
   301
      end
dc6769b86fd6 crude implementation of centralized slicing
blanchet
parents: 75027
diff changeset
   302
dc6769b86fd6 crude implementation of centralized slicing
blanchet
parents: 75027
diff changeset
   303
    val provers = distinct (op =) schedule
dc6769b86fd6 crude implementation of centralized slicing
blanchet
parents: 75027
diff changeset
   304
    val prover_slices =
dc6769b86fd6 crude implementation of centralized slicing
blanchet
parents: 75027
diff changeset
   305
      map (fn prover => (prover, triplicate_slices (get_slices ctxt prover))) provers
dc6769b86fd6 crude implementation of centralized slicing
blanchet
parents: 75027
diff changeset
   306
dc6769b86fd6 crude implementation of centralized slicing
blanchet
parents: 75027
diff changeset
   307
    fun translate _ [] = []
dc6769b86fd6 crude implementation of centralized slicing
blanchet
parents: 75027
diff changeset
   308
      | translate prover_slices (prover :: schedule) =
dc6769b86fd6 crude implementation of centralized slicing
blanchet
parents: 75027
diff changeset
   309
        (case AList.lookup (op =) prover_slices prover of
dc6769b86fd6 crude implementation of centralized slicing
blanchet
parents: 75027
diff changeset
   310
          SOME (slice :: slices) =>
dc6769b86fd6 crude implementation of centralized slicing
blanchet
parents: 75027
diff changeset
   311
          let val prover_slices' = AList.update (op =) (prover, slices) prover_slices in
dc6769b86fd6 crude implementation of centralized slicing
blanchet
parents: 75027
diff changeset
   312
            (prover, slice) :: translate prover_slices' schedule
dc6769b86fd6 crude implementation of centralized slicing
blanchet
parents: 75027
diff changeset
   313
          end
dc6769b86fd6 crude implementation of centralized slicing
blanchet
parents: 75027
diff changeset
   314
        | _ => translate prover_slices schedule)
dc6769b86fd6 crude implementation of centralized slicing
blanchet
parents: 75027
diff changeset
   315
  in
dc6769b86fd6 crude implementation of centralized slicing
blanchet
parents: 75027
diff changeset
   316
    translate prover_slices schedule
dc6769b86fd6 crude implementation of centralized slicing
blanchet
parents: 75027
diff changeset
   317
  end
dc6769b86fd6 crude implementation of centralized slicing
blanchet
parents: 75027
diff changeset
   318
75031
ae4dc5ac983f implemented 'max_proofs' mechanism
blanchet
parents: 75030
diff changeset
   319
fun run_sledgehammer (params as {verbose, spy, provers, induction_rules, max_facts, max_proofs,
ae4dc5ac983f implemented 'max_proofs' mechanism
blanchet
parents: 75030
diff changeset
   320
      slices, ...})
75030
919fb49ba201 document new option 'max_proofs'
blanchet
parents: 75029
diff changeset
   321
    mode writeln_result i (fact_override as {only, ...}) state =
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39494
diff changeset
   322
  if null provers then
63692
1bc4bc2c9fd1 killed final stops in Sledgehammer and friends
blanchet
parents: 63311
diff changeset
   323
    error "No prover is set"
55286
blanchet
parents: 55212
diff changeset
   324
  else
blanchet
parents: 55212
diff changeset
   325
    (case subgoal_count state of
74953
aade20a03edb tuned run_sledgehammer and called it directly from Mirabelle
desharna
parents: 74952
diff changeset
   326
      0 => (error "No subgoal!"; (false, (SH_None, "")))
55286
blanchet
parents: 55212
diff changeset
   327
    | n =>
blanchet
parents: 55212
diff changeset
   328
      let
blanchet
parents: 55212
diff changeset
   329
        val _ = Proof.assert_backward state
62735
23de054397e5 early warning when Sledgehammer finds a proof
blanchet
parents: 62519
diff changeset
   330
        val print = if mode = Normal andalso is_none writeln_result then writeln else K ()
23de054397e5 early warning when Sledgehammer finds a proof
blanchet
parents: 62519
diff changeset
   331
75031
ae4dc5ac983f implemented 'max_proofs' mechanism
blanchet
parents: 75030
diff changeset
   332
        val found_proofs = Synchronized.var "found_proofs" 0
75030
919fb49ba201 document new option 'max_proofs'
blanchet
parents: 75029
diff changeset
   333
919fb49ba201 document new option 'max_proofs'
blanchet
parents: 75029
diff changeset
   334
        fun found_proof prover_name =
919fb49ba201 document new option 'max_proofs'
blanchet
parents: 75029
diff changeset
   335
          if mode = Normal then
75031
ae4dc5ac983f implemented 'max_proofs' mechanism
blanchet
parents: 75030
diff changeset
   336
            (Synchronized.change found_proofs (fn n => n + 1);
ae4dc5ac983f implemented 'max_proofs' mechanism
blanchet
parents: 75030
diff changeset
   337
             (writeln_result |> the_default writeln) (prover_name ^ " found a proof..."))
75030
919fb49ba201 document new option 'max_proofs'
blanchet
parents: 75029
diff changeset
   338
          else
919fb49ba201 document new option 'max_proofs'
blanchet
parents: 75029
diff changeset
   339
            ()
62735
23de054397e5 early warning when Sledgehammer finds a proof
blanchet
parents: 62519
diff changeset
   340
55286
blanchet
parents: 55212
diff changeset
   341
        val ctxt = Proof.context_of state
74950
b350a1f2115d added nearly_all_facts_of_context and uniformized its usage in Sledgehammer and Mirabelle
desharna
parents: 73975
diff changeset
   342
        val inst_inducts = induction_rules = SOME Instantiate
b350a1f2115d added nearly_all_facts_of_context and uniformized its usage in Sledgehammer and Mirabelle
desharna
parents: 73975
diff changeset
   343
        val {facts = chained_thms, goal, ...} = Proof.goal state
55286
blanchet
parents: 55212
diff changeset
   344
        val (_, hyp_ts, concl_t) = strip_subgoal goal i ctxt
blanchet
parents: 55212
diff changeset
   345
        val _ =
blanchet
parents: 55212
diff changeset
   346
          (case find_first (not o is_prover_supported ctxt) provers of
63692
1bc4bc2c9fd1 killed final stops in Sledgehammer and friends
blanchet
parents: 63311
diff changeset
   347
            SOME name => error ("No such prover: " ^ name)
55286
blanchet
parents: 55212
diff changeset
   348
          | NONE => ())
blanchet
parents: 55212
diff changeset
   349
        val _ = print "Sledgehammering..."
57037
c51132be8e16 avoid markup-generating @{make_string}
blanchet
parents: 56303
diff changeset
   350
        val _ = spying spy (fn () => (state, i, "***", "Starting " ^ str_of_mode mode ^ " mode"))
75002
ef18787842b3 added spying of fact filtering timing
desharna
parents: 74998
diff changeset
   351
        val ({elapsed, ...}, all_facts) = Timing.timing
ef18787842b3 added spying of fact filtering timing
desharna
parents: 74998
diff changeset
   352
          (nearly_all_facts_of_context ctxt inst_inducts fact_override chained_thms hyp_ts) concl_t
ef18787842b3 added spying of fact filtering timing
desharna
parents: 74998
diff changeset
   353
        val _ = spying spy (fn () => (state, i, "All",
ef18787842b3 added spying of fact filtering timing
desharna
parents: 74998
diff changeset
   354
          "Extracting " ^ string_of_int (length all_facts) ^ " facts from background theory in " ^
ef18787842b3 added spying of fact filtering timing
desharna
parents: 74998
diff changeset
   355
          string_of_int (Time.toMilliseconds elapsed) ^ " ms"))
54090
a28992e35032 run relevance filter only once for ATPs and SMT solvers, since it should now yield the same results anyway
blanchet
parents: 54063
diff changeset
   356
55286
blanchet
parents: 55212
diff changeset
   357
        val spying_str_of_factss =
blanchet
parents: 55212
diff changeset
   358
          commas o map (fn (filter, facts) => filter ^ ": " ^ string_of_int (length facts))
53800
ac1ec5065316 added "spy" option to Sledgehammer
blanchet
parents: 53549
diff changeset
   359
55286
blanchet
parents: 55212
diff changeset
   360
        fun get_factss provers =
blanchet
parents: 55212
diff changeset
   361
          let
blanchet
parents: 55212
diff changeset
   362
            val max_max_facts =
blanchet
parents: 55212
diff changeset
   363
              (case max_facts of
blanchet
parents: 55212
diff changeset
   364
                SOME n => n
blanchet
parents: 55212
diff changeset
   365
              | NONE =>
75029
dc6769b86fd6 crude implementation of centralized slicing
blanchet
parents: 75027
diff changeset
   366
                fold (fn prover =>
dc6769b86fd6 crude implementation of centralized slicing
blanchet
parents: 75027
diff changeset
   367
                    fold (fn ((n, _), _) => Integer.max n) (get_slices ctxt prover))
dc6769b86fd6 crude implementation of centralized slicing
blanchet
parents: 75027
diff changeset
   368
                  provers 0)
75027
a8efa30c380d take 'induction_rules' into consideration, as well as 'max_facts' even when 'only' is set
blanchet
parents: 75026
diff changeset
   369
74998
fe14ceff1cfd added syping of fact filtering time to sledgehammer
desharna
parents: 74953
diff changeset
   370
            val ({elapsed, ...}, factss) = Timing.timing
fe14ceff1cfd added syping of fact filtering time to sledgehammer
desharna
parents: 74953
diff changeset
   371
              (relevant_facts ctxt params (hd provers) max_max_facts fact_override hyp_ts concl_t)
fe14ceff1cfd added syping of fact filtering time to sledgehammer
desharna
parents: 74953
diff changeset
   372
              all_facts
75027
a8efa30c380d take 'induction_rules' into consideration, as well as 'max_facts' even when 'only' is set
blanchet
parents: 75026
diff changeset
   373
a8efa30c380d take 'induction_rules' into consideration, as well as 'max_facts' even when 'only' is set
blanchet
parents: 75026
diff changeset
   374
            val induction_rules = the_default (if only then Include else Exclude) induction_rules
a8efa30c380d take 'induction_rules' into consideration, as well as 'max_facts' even when 'only' is set
blanchet
parents: 75026
diff changeset
   375
            val factss = map (apsnd (maybe_filter_out_induction_rules induction_rules)) factss
a8efa30c380d take 'induction_rules' into consideration, as well as 'max_facts' even when 'only' is set
blanchet
parents: 75026
diff changeset
   376
74998
fe14ceff1cfd added syping of fact filtering time to sledgehammer
desharna
parents: 74953
diff changeset
   377
            val () = spying spy (fn () => (state, i, "All",
75002
ef18787842b3 added spying of fact filtering timing
desharna
parents: 74998
diff changeset
   378
              "Filtering facts in " ^ string_of_int (Time.toMilliseconds elapsed) ^
ef18787842b3 added spying of fact filtering timing
desharna
parents: 74998
diff changeset
   379
              " ms (MaSh algorithm: " ^ str_of_mash_algorithm (the_mash_algorithm ()) ^ ")"));
74998
fe14ceff1cfd added syping of fact filtering time to sledgehammer
desharna
parents: 74953
diff changeset
   380
            val () = if verbose then print (string_of_factss factss) else ()
fe14ceff1cfd added syping of fact filtering time to sledgehammer
desharna
parents: 74953
diff changeset
   381
            val () = spying spy (fn () =>
fe14ceff1cfd added syping of fact filtering time to sledgehammer
desharna
parents: 74953
diff changeset
   382
              (state, i, "All", "Selected facts: " ^ spying_str_of_factss factss))
55286
blanchet
parents: 55212
diff changeset
   383
          in
74998
fe14ceff1cfd added syping of fact filtering time to sledgehammer
desharna
parents: 74953
diff changeset
   384
            factss
55286
blanchet
parents: 55212
diff changeset
   385
          end
53800
ac1ec5065316 added "spy" option to Sledgehammer
blanchet
parents: 53549
diff changeset
   386
58892
20aa19ecf2cc eliminated obsolete Proof.goal_message -- print outcome more directly;
wenzelm
parents: 58843
diff changeset
   387
        fun launch_provers () =
55286
blanchet
parents: 55212
diff changeset
   388
          let
blanchet
parents: 55212
diff changeset
   389
            val problem =
blanchet
parents: 55212
diff changeset
   390
              {comment = "", state = state, goal = goal, subgoal = i, subgoal_count = n,
75025
f741d55a81e5 thread slices through
blanchet
parents: 75020
diff changeset
   391
               factss = get_factss provers, found_proof = found_proof}
69706
6d6235b828fc get rid of visibility in MaSh -- it slows it down more than it helps
blanchet
parents: 63697
diff changeset
   392
            val learn = mash_learn_proof ctxt params (Thm.prop_of goal)
75027
a8efa30c380d take 'induction_rules' into consideration, as well as 'max_facts' even when 'only' is set
blanchet
parents: 75026
diff changeset
   393
            val launch = launch_prover_and_preplay params mode writeln_result learn
75029
dc6769b86fd6 crude implementation of centralized slicing
blanchet
parents: 75027
diff changeset
   394
dc6769b86fd6 crude implementation of centralized slicing
blanchet
parents: 75027
diff changeset
   395
            val schedule =
dc6769b86fd6 crude implementation of centralized slicing
blanchet
parents: 75027
diff changeset
   396
              if mode = Auto_Try then
dc6769b86fd6 crude implementation of centralized slicing
blanchet
parents: 75027
diff changeset
   397
                provers
dc6769b86fd6 crude implementation of centralized slicing
blanchet
parents: 75027
diff changeset
   398
              else
75030
919fb49ba201 document new option 'max_proofs'
blanchet
parents: 75029
diff changeset
   399
                schedule_of_provers provers slices
75029
dc6769b86fd6 crude implementation of centralized slicing
blanchet
parents: 75027
diff changeset
   400
            val prover_slices = prover_slices_of_schedule ctxt schedule
55286
blanchet
parents: 55212
diff changeset
   401
          in
blanchet
parents: 55212
diff changeset
   402
            if mode = Auto_Try then
74953
aade20a03edb tuned run_sledgehammer and called it directly from Mirabelle
desharna
parents: 74952
diff changeset
   403
              (SH_Unknown, "")
75029
dc6769b86fd6 crude implementation of centralized slicing
blanchet
parents: 75027
diff changeset
   404
              |> fold (fn (prover, slice) =>
75025
f741d55a81e5 thread slices through
blanchet
parents: 75020
diff changeset
   405
                  fn accum as (SH_Some _, _) => accum
75029
dc6769b86fd6 crude implementation of centralized slicing
blanchet
parents: 75027
diff changeset
   406
                    | _ => launch problem slice prover)
dc6769b86fd6 crude implementation of centralized slicing
blanchet
parents: 75027
diff changeset
   407
                prover_slices
55286
blanchet
parents: 55212
diff changeset
   408
            else
74950
b350a1f2115d added nearly_all_facts_of_context and uniformized its usage in Sledgehammer and Mirabelle
desharna
parents: 73975
diff changeset
   409
              (learn chained_thms;
75031
ae4dc5ac983f implemented 'max_proofs' mechanism
blanchet
parents: 75030
diff changeset
   410
               Par_List.map (fn (prover, slice) =>
ae4dc5ac983f implemented 'max_proofs' mechanism
blanchet
parents: 75030
diff changeset
   411
                   if Synchronized.value found_proofs < max_proofs then
ae4dc5ac983f implemented 'max_proofs' mechanism
blanchet
parents: 75030
diff changeset
   412
                     launch problem slice prover
ae4dc5ac983f implemented 'max_proofs' mechanism
blanchet
parents: 75030
diff changeset
   413
                   else
ae4dc5ac983f implemented 'max_proofs' mechanism
blanchet
parents: 75030
diff changeset
   414
                     (SH_Unknown, ""))
ae4dc5ac983f implemented 'max_proofs' mechanism
blanchet
parents: 75030
diff changeset
   415
                 prover_slices
74953
aade20a03edb tuned run_sledgehammer and called it directly from Mirabelle
desharna
parents: 74952
diff changeset
   416
               |> max_outcome)
55286
blanchet
parents: 55212
diff changeset
   417
          end
blanchet
parents: 55212
diff changeset
   418
      in
75020
b087610592b4 rationalized output for forthcoming slicing model
blanchet
parents: 75019
diff changeset
   419
        (launch_provers ()
b087610592b4 rationalized output for forthcoming slicing model
blanchet
parents: 75019
diff changeset
   420
         handle Timeout.TIMEOUT _ => (SH_Timeout, ""))
b087610592b4 rationalized output for forthcoming slicing model
blanchet
parents: 75019
diff changeset
   421
        |> `(fn (outcome, _) =>
b087610592b4 rationalized output for forthcoming slicing model
blanchet
parents: 75019
diff changeset
   422
          (case outcome of
b087610592b4 rationalized output for forthcoming slicing model
blanchet
parents: 75019
diff changeset
   423
            SH_Some _ => (print "QED"; true)
75030
919fb49ba201 document new option 'max_proofs'
blanchet
parents: 75029
diff changeset
   424
          | _ => (print "Sorry"; false)))
75020
b087610592b4 rationalized output for forthcoming slicing model
blanchet
parents: 75019
diff changeset
   425
      end)
38044
463177795c49 minor refactoring
blanchet
parents: 38040
diff changeset
   426
28582
c269a3045fdf info: back to plain printing;
wenzelm
parents: 28571
diff changeset
   427
end;