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
--- 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 *}
--- 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
--- 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 #>
--- 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