# HG changeset patch
# User boehmes
# Date 1297682726 -3600
# Node ID 00060198de125c12c06f96d1061d85f7737f356d
# Parent  2dc75bae522657a0b730289ca71e61134940d728
limit the number of generated SMT monomorphization instances (in addition to the existing monomorphization limit which does not prevent seemingly infinite loops);
updated SMT certificate

diff -r 2dc75bae5226 -r 00060198de12 src/HOL/SMT.thy
--- a/src/HOL/SMT.thy	Mon Feb 14 10:40:43 2011 +0100
+++ b/src/HOL/SMT.thy	Mon Feb 14 12:25:26 2011 +0100
@@ -247,6 +247,13 @@
 
 declare [[ smt_monomorph_limit = 10 ]]
 
+text {*
+In addition, the number of generated monomorphic instances is limited
+by the following option.
+*}
+
+declare [[ smt_monomorph_instances = 500 ]]
+
 
 
 subsection {* Certificates *}
diff -r 2dc75bae5226 -r 00060198de12 src/HOL/SMT_Examples/SMT_Examples.certs
--- a/src/HOL/SMT_Examples/SMT_Examples.certs	Mon Feb 14 10:40:43 2011 +0100
+++ b/src/HOL/SMT_Examples/SMT_Examples.certs	Mon Feb 14 12:25:26 2011 +0100
@@ -14831,3 +14831,80 @@
 #269 := [asserted]: #104
 [unit-resolution #269 #614]: false
 unsat
+b5935b8a85a2e047200d1ea44e320dc9dcfbbbbc 76 0
+#2 := false
+decl f3 :: (-> Int S1)
+#118 := 1::Int
+#119 := (f3 1::Int)
+decl f1 :: S1
+#4 := f1
+#421 := (= f1 #119)
+#425 := (not #421)
+#120 := (= #119 f1)
+#121 := (not #120)
+#426 := (iff #121 #425)
+#423 := (iff #120 #421)
+#424 := [rewrite]: #423
+#427 := [monotonicity #424]: #426
+#420 := [asserted]: #121
+#430 := [mp #420 #427]: #425
+#8 := (:var 0 Int)
+#9 := (f3 #8)
+#953 := (pattern #9)
+#142 := (= f1 #9)
+#954 := (forall (vars (?v0 Int)) (:pat #953) #142)
+#165 := (forall (vars (?v0 Int)) #142)
+#957 := (iff #165 #954)
+#955 := (iff #142 #142)
+#956 := [refl]: #955
+#958 := [quant-intro #956]: #957
+#456 := (~ #165 #165)
+#454 := (~ #142 #142)
+#455 := [refl]: #454
+#457 := [nnf-pos #455]: #456
+decl f4 :: (-> S2 S1)
+decl f5 :: (-> Int S2 S2)
+decl f6 :: S2
+#11 := f6
+#12 := (f5 #8 f6)
+#13 := (f4 #12)
+#14 := (= #13 f1)
+#15 := (not #14)
+#16 := (or #14 #15)
+#10 := (= #9 f1)
+#17 := (and #10 #16)
+#18 := (forall (vars (?v0 Int)) #17)
+#166 := (iff #18 #165)
+#163 := (iff #17 #142)
+#1 := true
+#158 := (and #142 true)
+#161 := (iff #158 #142)
+#162 := [rewrite]: #161
+#159 := (iff #17 #158)
+#156 := (iff #16 true)
+#145 := (= f1 #13)
+#148 := (not #145)
+#151 := (or #145 #148)
+#154 := (iff #151 true)
+#155 := [rewrite]: #154
+#152 := (iff #16 #151)
+#149 := (iff #15 #148)
+#146 := (iff #14 #145)
+#147 := [rewrite]: #146
+#150 := [monotonicity #147]: #149
+#153 := [monotonicity #147 #150]: #152
+#157 := [trans #153 #155]: #156
+#143 := (iff #10 #142)
+#144 := [rewrite]: #143
+#160 := [monotonicity #144 #157]: #159
+#164 := [trans #160 #162]: #163
+#167 := [quant-intro #164]: #166
+#141 := [asserted]: #18
+#170 := [mp #141 #167]: #165
+#429 := [mp~ #170 #457]: #165
+#959 := [mp #429 #958]: #954
+#538 := (not #954)
+#623 := (or #538 #421)
+#624 := [quant-inst #118]: #623
+[unit-resolution #624 #959 #430]: false
+unsat
diff -r 2dc75bae5226 -r 00060198de12 src/HOL/Tools/SMT/smt_config.ML
--- a/src/HOL/Tools/SMT/smt_config.ML	Mon Feb 14 10:40:43 2011 +0100
+++ b/src/HOL/Tools/SMT/smt_config.ML	Mon Feb 14 12:25:26 2011 +0100
@@ -32,6 +32,7 @@
   val trace: bool Config.T
   val trace_used_facts: bool Config.T
   val monomorph_limit: int Config.T
+  val monomorph_instances: int Config.T
   val infer_triggers: bool Config.T
   val drop_bad_facts: bool Config.T
   val filter_only_facts: bool Config.T
@@ -176,6 +177,10 @@
 val (monomorph_limit, setup_monomorph_limit) =
   Attrib.config_int monomorph_limitN (K 10)
 
+val monomorph_instancesN = "smt_monomorph_instances"
+val (monomorph_instances, setup_monomorph_instances) =
+  Attrib.config_int monomorph_instancesN (K 500)
+
 val infer_triggersN = "smt_infer_triggers"
 val (infer_triggers, setup_infer_triggers) =
   Attrib.config_bool infer_triggersN (K false)
@@ -201,6 +206,7 @@
   setup_trace #>
   setup_verbose #>
   setup_monomorph_limit #>
+  setup_monomorph_instances #>
   setup_infer_triggers #>
   setup_drop_bad_facts #>
   setup_filter_only_facts #>
diff -r 2dc75bae5226 -r 00060198de12 src/HOL/Tools/SMT/smt_monomorph.ML
--- a/src/HOL/Tools/SMT/smt_monomorph.ML	Mon Feb 14 10:40:43 2011 +0100
+++ b/src/HOL/Tools/SMT/smt_monomorph.ML	Mon Feb 14 12:25:26 2011 +0100
@@ -37,6 +37,10 @@
 
 (* utility functions *)
 
+fun fold_maps f = fold (fn x => uncurry (fold_map (f x)) #>> flat)
+
+fun pair_trans ((x, y), z) = (x, (y, z))
+
 val typ_has_tvars = Term.exists_subtype (fn TVar _ => true | _ => false)
 
 val ignored = member (op =) [@{const_name All}, @{const_name Ex},
@@ -76,13 +80,14 @@
 
 (* search for necessary substitutions *)
 
-fun new_substitutions thy limit grounds (n, T) subst =
-  if not (typ_has_tvars T) then [subst]
+fun new_substitutions thy limit grounds (n, T) subst instances =
+  if not (typ_has_tvars T) then ([subst], instances)
   else
     Symtab.lookup_list grounds n
     |> map_filter (try (fn U => Sign.typ_match thy (T, U) subst))
-    |> cons subst
-    |> take limit (* limit the breadth of the search as well as the width *)
+    |> (fn substs => (substs, instances - length substs))
+    |>> take limit (* limit the breadth of the search as well as the width *)
+    |>> cons subst
 
 fun apply_subst grounds consts subst =
   let
@@ -100,11 +105,12 @@
 
 fun specialize thy limit all_grounds new_grounds scs =
   let
-    fun spec (subst, consts) next_grounds =
-      [subst]
-      |> fold (maps o new_substitutions thy limit new_grounds) consts
-      |> rpair next_grounds
-      |-> fold_map (apply_subst all_grounds consts)
+    fun spec (subst, consts) (next_grounds, instances) =
+      ([subst], instances)
+      |> fold_maps (new_substitutions thy limit new_grounds) consts
+      |>> rpair next_grounds
+      |>> uncurry (fold_map (apply_subst all_grounds consts))
+      |> pair_trans
   in
     fold_map spec scs #>> (fn scss =>
     fold (fold (insert (eq_snd (op =)))) scss [])
@@ -112,16 +118,18 @@
 
 val limit_reached_warning = "Warning: Monomorphization limit reached"
 
-fun search_substitutions ctxt limit all_grounds new_grounds scss =
+fun search_substitutions ctxt limit instances all_grounds new_grounds scss =
   let
     val thy = ProofContext.theory_of ctxt
     val all_grounds' = Symtab.merge_list (op =) (all_grounds, new_grounds)
     val spec = specialize thy limit all_grounds' new_grounds
-    val (scss', new_grounds') = fold_map spec scss Symtab.empty
+    val (scss', (new_grounds', instances')) =
+      fold_map spec scss (Symtab.empty, instances)
   in
     if Symtab.is_empty new_grounds' then scss'
-    else if limit > 0 then
-      search_substitutions ctxt (limit-1) all_grounds' new_grounds' scss'
+    else if limit > 0 andalso instances' > 0 then
+      search_substitutions ctxt (limit-1) instances' all_grounds' new_grounds'
+        scss'
     else (SMT_Config.verbose_msg ctxt (K limit_reached_warning) (); scss')
   end
 
@@ -194,9 +202,10 @@
       |> fold (add_const_types (not o typ_has_tvars) o snd) polys
 
     val limit = Config.get ctxt SMT_Config.monomorph_limit
+    val instances = Config.get ctxt SMT_Config.monomorph_instances
   in
     scss
-    |> search_substitutions ctxt limit Symtab.empty grounds
+    |> search_substitutions ctxt limit instances Symtab.empty grounds
     |> map (filter_most_specific (ProofContext.theory_of ctxt))
     |> rpair (monos, ctxt)
     |-> fold2 instantiate polys