1(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML
2    Author:     Philipp Meyer, TU Muenchen
3    Author:     Jasmin Blanchette, TU Muenchen
4
5Minimization of fact list for Metis using external provers.
6*)
7
8signature SLEDGEHAMMER_PROVER_MINIMIZE =
9sig
10  type stature = ATP_Problem_Generate.stature
11  type proof_method = Sledgehammer_Proof_Methods.proof_method
12  type play_outcome = Sledgehammer_Proof_Methods.play_outcome
13  type mode = Sledgehammer_Prover.mode
14  type params = Sledgehammer_Prover.params
15  type prover = Sledgehammer_Prover.prover
16
17  val is_prover_supported : Proof.context -> string -> bool
18  val is_prover_installed : Proof.context -> string -> bool
19  val default_max_facts_of_prover : Proof.context -> string -> int
20  val get_prover : Proof.context -> mode -> string -> prover
21
22  val binary_min_facts : int Config.T
23  val minimize_facts : (thm list -> unit) -> string -> params -> bool -> int -> int ->
24    Proof.state -> thm -> ((string * stature) * thm list) list ->
25    ((string * stature) * thm list) list option
26    * ((unit -> (string * stature) list * (proof_method * play_outcome)) -> string)
27  val get_minimizing_prover : Proof.context -> mode -> (thm list -> unit) -> string -> prover
28end;
29
30structure Sledgehammer_Prover_Minimize : SLEDGEHAMMER_PROVER_MINIMIZE =
31struct
32
33open ATP_Util
34open ATP_Proof
35open ATP_Problem_Generate
36open ATP_Proof_Reconstruct
37open ATP_Systems
38open Sledgehammer_Util
39open Sledgehammer_Fact
40open Sledgehammer_Proof_Methods
41open Sledgehammer_Isar
42open Sledgehammer_Prover
43open Sledgehammer_Prover_ATP
44open Sledgehammer_Prover_SMT
45
46fun is_prover_supported ctxt =
47  let val thy = Proof_Context.theory_of ctxt in
48    is_atp thy orf is_smt_prover ctxt
49  end
50
51fun is_prover_installed ctxt =
52  is_smt_prover ctxt orf is_atp_installed (Proof_Context.theory_of ctxt)
53
54fun default_max_facts_of_prover ctxt name =
55  let val thy = Proof_Context.theory_of ctxt in
56    if is_atp thy name then
57      fold (Integer.max o fst o #1 o fst o snd) (#best_slices (get_atp thy name ()) ctxt) 0
58    else if is_smt_prover ctxt name then
59      SMT_Solver.default_max_relevant ctxt name
60    else
61      error ("No such prover: " ^ name)
62  end
63
64fun get_prover ctxt mode name =
65  let val thy = Proof_Context.theory_of ctxt in
66    if is_atp thy name then run_atp mode name
67    else if is_smt_prover ctxt name then run_smt_solver mode name
68    else error ("No such prover: " ^ name)
69  end
70
71(* wrapper for calling external prover *)
72
73fun n_facts names =
74  let val n = length names in
75    string_of_int n ^ " fact" ^ plural_s n ^
76    (if n > 0 then ": " ^ (names |> map fst |> sort string_ord |> space_implode " ") else "")
77  end
78
79fun print silent f = if silent then () else writeln (f ())
80
81fun test_facts ({debug, verbose, overlord, spy, provers, max_mono_iters, max_new_mono_instances,
82      type_enc, strict, lam_trans, uncurried_aliases, isar_proofs, compress, try0, smt_proofs,
83      minimize, preplay_timeout, ...} : params)
84    silent (prover : prover) timeout i n state goal facts =
85  let
86    val _ = print silent (fn () => "Testing " ^ n_facts (map fst facts) ^
87      (if verbose then " (timeout: " ^ string_of_time timeout ^ ")" else "") ^ "...")
88
89    val facts = facts |> maps (fn (n, ths) => map (pair n) ths)
90    val params =
91      {debug = debug, verbose = verbose, overlord = overlord, spy = spy, provers = provers,
92       type_enc = type_enc, strict = strict, lam_trans = lam_trans,
93       uncurried_aliases = uncurried_aliases, learn = false, fact_filter = NONE,
94       max_facts = SOME (length facts), fact_thresholds = (1.01, 1.01),
95       max_mono_iters = max_mono_iters, max_new_mono_instances = max_new_mono_instances,
96       isar_proofs = isar_proofs, compress = compress, try0 = try0, smt_proofs = smt_proofs,
97       slice = false, minimize = minimize, timeout = timeout, preplay_timeout = preplay_timeout,
98       expect = ""}
99    val problem =
100      {comment = "", state = state, goal = goal, subgoal = i, subgoal_count = n,
101       factss = [("", facts)], found_proof = I}
102    val result0 as {outcome = outcome0, used_facts, used_from, preferred_methss, run_time,
103        message} =
104      prover params problem
105    val result as {outcome, ...} =
106      if is_none outcome0 andalso
107         forall (member (fn ((s, _), ((s', _), _)) => s = s') used_from) used_facts then
108        result0
109      else
110        {outcome = SOME MaybeUnprovable, used_facts = [], used_from = used_from,
111         preferred_methss = preferred_methss, run_time = run_time, message = message}
112  in
113    print silent (fn () =>
114      (case outcome of
115        SOME failure => string_of_atp_failure failure
116      | NONE =>
117        "Found proof" ^
118         (if length used_facts = length facts then "" else " with " ^ n_facts used_facts) ^
119         " (" ^ string_of_time run_time ^ ")"));
120    result
121  end
122
123(* minimalization of facts *)
124
125(* Give the external prover some slack. The ATP gets further slack because the
126   Sledgehammer preprocessing time is included in the estimate below but isn't
127   part of the timeout. *)
128val slack_msecs = 200
129
130fun new_timeout timeout run_time =
131  Int.min (Time.toMilliseconds timeout, Time.toMilliseconds run_time + slack_msecs)
132  |> Time.fromMilliseconds
133
134(* The linear algorithm usually outperforms the binary algorithm when over 60%
135   of the facts are actually needed. The binary algorithm is much more
136   appropriate for provers that cannot return the list of used facts and hence
137   returns all facts as used. Since we cannot know in advance how many facts are
138   actually needed, we heuristically set the threshold to 10 facts. *)
139val binary_min_facts =
140  Attrib.setup_config_int \<^binding>\<open>sledgehammer_minimize_binary_min_facts\<close> (K 20)
141
142fun linear_minimize test timeout result xs =
143  let
144    fun min _ [] p = p
145      | min timeout (x :: xs) (seen, result) =
146        (case test timeout (xs @ seen) of
147          result as {outcome = NONE, used_facts, run_time, ...} : prover_result =>
148          min (new_timeout timeout run_time) (filter_used_facts true used_facts xs)
149            (filter_used_facts false used_facts seen, result)
150        | _ => min timeout xs (x :: seen, result))
151  in
152    min timeout xs ([], result)
153  end
154
155fun binary_minimize test timeout result xs =
156  let
157    fun min depth (result as {run_time, ...} : prover_result) sup (xs as _ :: _ :: _) =
158        let
159          val (l0, r0) = chop (length xs div 2) xs
160(*
161          val _ = warning (replicate_string depth " " ^ "{ " ^ "sup: " ^ n_facts (map fst sup))
162          val _ = warning (replicate_string depth " " ^ " " ^ "xs: " ^ n_facts (map fst xs))
163          val _ = warning (replicate_string depth " " ^ " " ^ "l0: " ^ n_facts (map fst l0))
164          val _ = warning (replicate_string depth " " ^ " " ^ "r0: " ^ n_facts (map fst r0))
165*)
166          val depth = depth + 1
167          val timeout = new_timeout timeout run_time
168        in
169          (case test timeout (sup @ l0) of
170            result as {outcome = NONE, used_facts, ...} =>
171            min depth result (filter_used_facts true used_facts sup)
172              (filter_used_facts true used_facts l0)
173          | _ =>
174            (case test timeout (sup @ r0) of
175              result as {outcome = NONE, used_facts, ...} =>
176              min depth result (filter_used_facts true used_facts sup)
177                (filter_used_facts true used_facts r0)
178            | _ =>
179              let
180                val (sup_r0, (l, result)) = min depth result (sup @ r0) l0
181                val (sup, r0) = (sup, r0) |> apply2 (filter_used_facts true (map fst sup_r0))
182                val (sup_l, (r, result)) = min depth result (sup @ l) r0
183                val sup = sup |> filter_used_facts true (map fst sup_l)
184              in (sup, (l @ r, result)) end))
185        end
186(*
187        |> tap (fn _ => warning (replicate_string depth " " ^ "}"))
188*)
189      | min _ result sup xs = (sup, (xs, result))
190  in
191    (case snd (min 0 result [] xs) of
192      ([x], result as {run_time, ...}) =>
193      (case test (new_timeout timeout run_time) [] of
194        result as {outcome = NONE, ...} => ([], result)
195      | _ => ([x], result))
196    | p => p)
197  end
198
199fun minimize_facts do_learn prover_name (params as {learn, timeout, ...}) silent i n state goal
200    facts =
201  let
202    val ctxt = Proof.context_of state
203    val prover = get_prover ctxt Minimize prover_name
204    val (chained, non_chained) = List.partition is_fact_chained facts
205
206    fun test timeout non_chained =
207      test_facts params silent prover timeout i n state goal (chained @ non_chained)
208  in
209    (print silent (fn () => "Sledgehammer minimizer: " ^ quote prover_name);
210     (case test timeout non_chained of
211       result as {outcome = NONE, used_facts, run_time, ...} =>
212       let
213         val non_chained = filter_used_facts true used_facts non_chained
214         val min =
215           if length non_chained >= Config.get ctxt binary_min_facts then binary_minimize
216           else linear_minimize
217         val (min_facts, {message, ...}) =
218           min test (new_timeout timeout run_time) result non_chained
219         val min_facts_and_chained = chained @ min_facts
220       in
221         print silent (fn () => cat_lines
222           ["Minimized to " ^ n_facts (map fst min_facts)] ^
223            (case length chained of
224              0 => ""
225            | n => " (plus " ^ string_of_int n ^ " chained)"));
226         (if learn then do_learn (maps snd min_facts_and_chained) else ());
227         (SOME min_facts_and_chained, message)
228       end
229     | {outcome = SOME TimedOut, ...} =>
230       (NONE, fn _ =>
231          "Timeout: You can increase the time limit using the \"timeout\" option (e.g., \
232          \timeout = " ^ string_of_int (10 + Time.toMilliseconds timeout div 1000) ^ "\")")
233     | {message, ...} => (NONE, (prefix "Prover error: " o message))))
234    handle ERROR msg => (NONE, fn _ => "Error: " ^ msg)
235  end
236
237fun maybe_minimize mode do_learn name (params as {verbose, minimize, ...})
238    ({state, goal, subgoal, subgoal_count, ...} : prover_problem)
239    (result as {outcome, used_facts, used_from, preferred_methss, run_time, message}
240     : prover_result) =
241  if is_some outcome then
242    result
243  else
244    let
245      val (used_facts, message) =
246        if minimize then
247          minimize_facts do_learn name params
248            (not verbose orelse (mode <> Normal andalso mode <> MaSh)) subgoal subgoal_count state
249            goal (filter_used_facts true used_facts (map (apsnd single) used_from))
250          |>> Option.map (map fst)
251        else
252          (SOME used_facts, message)
253    in
254      (case used_facts of
255        SOME used_facts =>
256        {outcome = NONE, used_facts = sort_by fst used_facts, used_from = used_from,
257         preferred_methss = preferred_methss, run_time = run_time, message = message}
258      | NONE => result)
259    end
260
261fun get_minimizing_prover ctxt mode do_learn name params problem =
262  get_prover ctxt mode name params problem
263  |> maybe_minimize mode do_learn name params problem
264
265end;
266