# HG changeset patch
# User blanchet
# Date 1662375245 -7200
# Node ID 6a20d0ebd5b3c55be2b355ede95c8ea395c04f80
# Parent  854e9223767f633ec8d0b0b45e8cc17925f76c91
added a bound in SMT on the number of schematic constants considered -- the code (in for_schematics) is exponential in that number

diff -r 854e9223767f -r 6a20d0ebd5b3 src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Sat Sep 03 23:10:38 2022 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Mon Sep 05 12:54:05 2022 +0200
@@ -245,12 +245,14 @@
     (if keep_chained then is_fact_chained else K false))
 
 val max_fact_instances = 10 (* FUDGE *)
+val max_schematics = 20 (* FUDGE *)
 
 fun repair_monomorph_context max_iters best_max_iters max_new_instances best_max_new_instances =
   Config.put Monomorph.max_rounds (max_iters |> the_default best_max_iters)
   #> Config.put Monomorph.max_new_instances
        (max_new_instances |> the_default best_max_new_instances)
   #> Config.put Monomorph.max_thm_instances max_fact_instances
+  #> Config.put Monomorph.max_schematics max_schematics
 
 fun supported_provers ctxt =
   let
diff -r 854e9223767f -r 6a20d0ebd5b3 src/HOL/Tools/monomorph.ML
--- a/src/HOL/Tools/monomorph.ML	Sat Sep 03 23:10:38 2022 +0200
+++ b/src/HOL/Tools/monomorph.ML	Mon Sep 05 12:54:05 2022 +0200
@@ -36,6 +36,7 @@
   val max_rounds: int Config.T
   val max_new_instances: int Config.T
   val max_thm_instances: int Config.T
+  val max_schematics: int Config.T
   val max_new_const_instances_per_round: int Config.T
   val max_duplicated_instances: int Config.T
 
@@ -72,6 +73,9 @@
 val max_thm_instances =
   Attrib.setup_config_int \<^binding>\<open>monomorph_max_thm_instances\<close> (K 20)
 
+val max_schematics =
+  Attrib.setup_config_int \<^binding>\<open>monomorph_max_schematics\<close> (K 1000)
+
 val max_new_const_instances_per_round =
   Attrib.setup_config_int \<^binding>\<open>monomorph_max_new_const_instances_per_round\<close> (K 5)
 
@@ -177,8 +181,8 @@
       | add _ = I
   in Term.fold_aterms add (Thm.prop_of thm) end
 
-fun add_insts max_instances max_duplicated_instances max_thm_insts ctxt round used_grounds
-    new_grounds id thm tvars schematics cx =
+fun add_insts max_instances max_duplicated_instances max_thm_insts max_schematics ctxt round
+    used_grounds new_grounds id thm tvars schematics cx =
   let
     exception ENOUGH of
       typ list Symtab.table * (int * int * ((int * (sort * typ) Vartab.table) * thm) list Inttab.table)
@@ -242,22 +246,24 @@
        instance is the usage of at least one ground from the new_grounds
        table. The approach used here is to match all schematics of the theorem
        with all relevant grounds. *)
-    for_schematics false schematics Vartab.empty cx
+    if length schematics > max_schematics then cx
+    else for_schematics false schematics Vartab.empty cx
     handle ENOUGH cx' => cx'
   end
 
 fun is_new round initial_round = (round = initial_round)
 fun is_active round initial_round = (round > initial_round)
 
-fun find_instances max_instances max_duplicated_instances max_thm_insts max_new_grounds thm_infos
-    ctxt round (known_grounds, new_grounds0, insts) =
+fun find_instances max_instances max_duplicated_instances max_thm_insts max_schematics
+    max_new_grounds thm_infos ctxt round (known_grounds, new_grounds0, insts) =
   let
     val new_grounds =
       Symtab.map (fn _ => fn grounds =>
         if length grounds <= max_new_grounds then grounds
         else take max_new_grounds (sort Term_Ord.typ_ord grounds)) new_grounds0
 
-    val add_new = add_insts max_instances max_duplicated_instances max_thm_insts ctxt round
+    val add_new = add_insts max_instances max_duplicated_instances max_thm_insts max_schematics
+      ctxt round
     fun consider_all pred f (cx as (_, (hits, misses, _))) =
       if hits >= max_instances orelse misses >= max_duplicated_instances then
         cx
@@ -279,7 +285,7 @@
   let fun add (n, T) = Symtab.map_entry n (insert (op =) T)
   in Term.fold_aterms (fn Const c => add c | _ => I) (Thm.prop_of thm) end
 
-fun collect_instances ctxt max_thm_insts max_new_grounds thm_infos consts =
+fun collect_instances ctxt max_thm_insts max_schematics max_new_grounds thm_infos consts =
   let
     val known_grounds = fold_grounds add_ground_types thm_infos consts
     val empty_grounds = clear_grounds known_grounds
@@ -288,7 +294,8 @@
     val max_duplicated_instances = Config.get ctxt max_duplicated_instances
     val (_, _, (_, _, insts)) =
       limit_rounds ctxt (find_instances max_instances max_duplicated_instances max_thm_insts
-      max_new_grounds thm_infos) (empty_grounds, known_grounds, (0, 0, Inttab.empty))
+          max_schematics max_new_grounds thm_infos)
+        (empty_grounds, known_grounds, (0, 0, Inttab.empty))
   in
     insts
   end
@@ -313,11 +320,14 @@
 fun monomorph schematic_consts_of ctxt rthms =
   let
     val max_thm_insts = Config.get ctxt max_thm_instances
+    val max_schematics = Config.get ctxt max_schematics
     val max_new_grounds = Config.get ctxt max_new_const_instances_per_round
     val (thm_infos, consts) = prepare schematic_consts_of rthms
     val insts =
-      if Symtab.is_empty consts then Inttab.empty
-      else collect_instances ctxt max_thm_insts max_new_grounds thm_infos consts
+      if Symtab.is_empty consts then
+        Inttab.empty
+      else
+        collect_instances ctxt max_thm_insts max_schematics max_new_grounds thm_infos consts
   in map (instantiated_thms max_thm_insts insts) thm_infos end
 
 end