# HG changeset patch
# User blanchet
# Date 1643641763 -3600
# Node ID ae4dc5ac983f4bf42be8330971a974640e8caf81
# Parent  919fb49ba201837f3fd4294fea6e93630510794a
implemented 'max_proofs' mechanism

diff -r 919fb49ba201 -r ae4dc5ac983f src/Doc/Sledgehammer/document/root.tex
--- a/src/Doc/Sledgehammer/document/root.tex	Mon Jan 31 16:09:23 2022 +0100
+++ b/src/Doc/Sledgehammer/document/root.tex	Mon Jan 31 16:09:23 2022 +0100
@@ -1121,7 +1121,8 @@
 \textit{overlord} (\S\ref{mode-of-operation}).}
 
 \opdefault{max\_proofs}{int}{\upshape 4}
-Specifies the maximum number of proofs to display before stopping.
+Specifies the maximum number of proofs to display before stopping. This is a
+soft limit.
 
 \opsmart{isar\_proofs}{no\_isar\_proofs}
 Specifies whether Isar proofs should be output in addition to one-line proofs.
diff -r 919fb49ba201 -r ae4dc5ac983f src/HOL/Sledgehammer.thy
--- a/src/HOL/Sledgehammer.thy	Mon Jan 31 16:09:23 2022 +0100
+++ b/src/HOL/Sledgehammer.thy	Mon Jan 31 16:09:23 2022 +0100
@@ -37,7 +37,7 @@
 
 (*
 lemma "1 + 1 = 2 \<and> 0 + (x::nat) = x"
-  sledgehammer [slices = 4]
+  sledgehammer [max_proofs = 3]
   oops
 *)
 
diff -r 919fb49ba201 -r ae4dc5ac983f src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML
--- a/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML	Mon Jan 31 16:09:23 2022 +0100
+++ b/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML	Mon Jan 31 16:09:23 2022 +0100
@@ -443,12 +443,7 @@
     val term_order = AList.lookup (op =) arguments term_orderK
     val proof_method_from_msg = proof_method_from_msg arguments
 
-    (* Parse Sledgehammer parameters *)
     val params = Sledgehammer_Commands.default_params \<^theory> arguments
-      |> (fn (params as {provers, ...}) =>
-            (case provers of
-              prover :: _ => Sledgehammer_Prover.set_params_provers params [prover]
-            | _ => error "sledgehammer action requires one and only one prover"))
 
     val data = Synchronized.var "Mirabelle_Sledgehammer.data" empty_data
 
diff -r 919fb49ba201 -r ae4dc5ac983f src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Mon Jan 31 16:09:23 2022 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Mon Jan 31 16:09:23 2022 +0100
@@ -316,7 +316,8 @@
     translate prover_slices schedule
   end
 
-fun run_sledgehammer (params as {verbose, spy, provers, induction_rules, max_facts, slices, ...})
+fun run_sledgehammer (params as {verbose, spy, provers, induction_rules, max_facts, max_proofs,
+      slices, ...})
     mode writeln_result i (fact_override as {only, ...}) state =
   if null provers then
     error "No prover is set"
@@ -328,12 +329,12 @@
         val _ = Proof.assert_backward state
         val print = if mode = Normal andalso is_none writeln_result then writeln else K ()
 
-        val proof_found = Synchronized.var "proof_found" false
+        val found_proofs = Synchronized.var "found_proofs" 0
 
         fun found_proof prover_name =
           if mode = Normal then
-(* ### Synchronized.change_result proof_found (rpair true) *)
-            (writeln_result |> the_default writeln) (prover_name ^ " found a proof...")
+            (Synchronized.change found_proofs (fn n => n + 1);
+             (writeln_result |> the_default writeln) (prover_name ^ " found a proof..."))
           else
             ()
 
@@ -406,7 +407,12 @@
                 prover_slices
             else
               (learn chained_thms;
-               Par_List.map (fn (prover, slice) => launch problem slice prover) prover_slices
+               Par_List.map (fn (prover, slice) =>
+                   if Synchronized.value found_proofs < max_proofs then
+                     launch problem slice prover
+                   else
+                     (SH_Unknown, ""))
+                 prover_slices
                |> max_outcome)
           end
       in
diff -r 919fb49ba201 -r ae4dc5ac983f src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Mon Jan 31 16:09:23 2022 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Mon Jan 31 16:09:23 2022 +0100
@@ -63,6 +63,7 @@
    ("fact_thresholds", "0.45 0.85"),
    ("max_mono_iters", "smart"),
    ("max_new_mono_instances", "smart"),
+   ("max_proofs", "4"),
    ("isar_proofs", "smart"),
    ("compress", "smart"),
    ("try0", "true"),
@@ -259,6 +260,7 @@
     val max_mono_iters = lookup_option lookup_int "max_mono_iters"
     val max_new_mono_instances =
       lookup_option lookup_int "max_new_mono_instances"
+    val max_proofs = lookup_int "max_proofs"
     val isar_proofs = lookup_option lookup_bool "isar_proofs"
     val compress = Option.map (curry Real.max 1.0) (lookup_option lookup_real "compress")
     val try0 = lookup_bool "try0"
@@ -274,9 +276,9 @@
      uncurried_aliases = uncurried_aliases, learn = learn, fact_filter = fact_filter,
      induction_rules = induction_rules, max_facts = max_facts, fact_thresholds = fact_thresholds,
      max_mono_iters = max_mono_iters, max_new_mono_instances = max_new_mono_instances,
-     isar_proofs = isar_proofs, compress = compress, try0 = try0, smt_proofs = smt_proofs,
-     minimize = minimize, slices = slices, timeout = timeout, preplay_timeout = preplay_timeout,
-     expect = expect}
+     max_proofs = max_proofs, isar_proofs = isar_proofs, compress = compress, try0 = try0,
+     smt_proofs = smt_proofs, minimize = minimize, slices = slices, timeout = timeout,
+     preplay_timeout = preplay_timeout, expect = expect}
   end
 
 fun get_params mode = extract_params mode o default_raw_params
diff -r 919fb49ba201 -r ae4dc5ac983f src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Mon Jan 31 16:09:23 2022 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Mon Jan 31 16:09:23 2022 +0100
@@ -40,6 +40,7 @@
      fact_thresholds : real * real,
      max_mono_iters : int option,
      max_new_mono_instances : int option,
+     max_proofs : int,
      isar_proofs : bool option,
      compress : real option,
      try0 : bool,
@@ -51,7 +52,6 @@
      expect : string}
 
   val string_of_params : params -> string
-  val set_params_provers : params -> string list -> params
   val slice_timeout : int -> Time.time -> Time.time
 
   type prover_problem =
@@ -141,6 +141,7 @@
    fact_thresholds : real * real,
    max_mono_iters : int option,
    max_new_mono_instances : int option,
+   max_proofs : int,
    isar_proofs : bool option,
    compress : real option,
    try0 : bool,
@@ -158,33 +159,6 @@
     induction_rules = Exclude ?
       filter_out (fn ((_, (_, ATP_Problem_Generate.Induction)), _) => true | _ => false)
 
-fun set_params_provers params provers =
-  {debug = #debug params,
-   verbose = #verbose params,
-   overlord = #overlord params,
-   spy = #spy params,
-   provers = provers,
-   type_enc = #type_enc params,
-   strict = #strict params,
-   lam_trans = #lam_trans params,
-   uncurried_aliases = #uncurried_aliases params,
-   learn = #learn params,
-   fact_filter = #fact_filter params,
-   induction_rules = #induction_rules params,
-   max_facts = #max_facts params,
-   fact_thresholds = #fact_thresholds params,
-   max_mono_iters = #max_mono_iters params,
-   max_new_mono_instances = #max_new_mono_instances params,
-   isar_proofs = #isar_proofs params,
-   compress = #compress params,
-   try0 = #try0 params,
-   smt_proofs = #smt_proofs params,
-   minimize = #minimize params,
-   slices = #slices params,
-   timeout = #timeout params,
-   preplay_timeout = #preplay_timeout params,
-   expect = #expect params}
-
 fun slice_timeout slices timeout =
   Time.toReal timeout * Real.fromInt (Multithreading.max_threads ()) / Real.fromInt slices
   |> seconds
diff -r 919fb49ba201 -r ae4dc5ac983f src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML	Mon Jan 31 16:09:23 2022 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML	Mon Jan 31 16:09:23 2022 +0100
@@ -94,9 +94,10 @@
        uncurried_aliases = uncurried_aliases, learn = false, fact_filter = NONE,
        induction_rules = induction_rules, max_facts = SOME (length facts),
        fact_thresholds = (1.01, 1.01), max_mono_iters = max_mono_iters,
-       max_new_mono_instances = max_new_mono_instances, isar_proofs = isar_proofs,
-       compress = compress, try0 = try0, smt_proofs = smt_proofs, minimize = minimize,
-       slices = 1, timeout = timeout, preplay_timeout = preplay_timeout, expect = ""}
+       max_new_mono_instances = max_new_mono_instances, max_proofs = 1,
+       isar_proofs = isar_proofs, compress = compress, try0 = try0, smt_proofs = smt_proofs,
+       minimize = minimize, slices = 1, timeout = timeout, preplay_timeout = preplay_timeout,
+       expect = ""}
     val problem =
       {comment = "", state = state, goal = goal, subgoal = i, subgoal_count = n,
        factss = [("", facts)], found_proof = K ()}