limit the number of generated SMT monomorphization instances (in addition to the existing monomorphization limit which does not prevent seemingly infinite loops);
authorboehmes
Mon Feb 14 12:25:26 2011 +0100 (2011-02-14)
changeset 4176200060198de12
parent 41761 2dc75bae5226
child 41763 8ce56536fda7
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
src/HOL/SMT.thy
src/HOL/SMT_Examples/SMT_Examples.certs
src/HOL/Tools/SMT/smt_config.ML
src/HOL/Tools/SMT/smt_monomorph.ML
     1.1 --- a/src/HOL/SMT.thy	Mon Feb 14 10:40:43 2011 +0100
     1.2 +++ b/src/HOL/SMT.thy	Mon Feb 14 12:25:26 2011 +0100
     1.3 @@ -247,6 +247,13 @@
     1.4  
     1.5  declare [[ smt_monomorph_limit = 10 ]]
     1.6  
     1.7 +text {*
     1.8 +In addition, the number of generated monomorphic instances is limited
     1.9 +by the following option.
    1.10 +*}
    1.11 +
    1.12 +declare [[ smt_monomorph_instances = 500 ]]
    1.13 +
    1.14  
    1.15  
    1.16  subsection {* Certificates *}
     2.1 --- a/src/HOL/SMT_Examples/SMT_Examples.certs	Mon Feb 14 10:40:43 2011 +0100
     2.2 +++ b/src/HOL/SMT_Examples/SMT_Examples.certs	Mon Feb 14 12:25:26 2011 +0100
     2.3 @@ -14831,3 +14831,80 @@
     2.4  #269 := [asserted]: #104
     2.5  [unit-resolution #269 #614]: false
     2.6  unsat
     2.7 +b5935b8a85a2e047200d1ea44e320dc9dcfbbbbc 76 0
     2.8 +#2 := false
     2.9 +decl f3 :: (-> Int S1)
    2.10 +#118 := 1::Int
    2.11 +#119 := (f3 1::Int)
    2.12 +decl f1 :: S1
    2.13 +#4 := f1
    2.14 +#421 := (= f1 #119)
    2.15 +#425 := (not #421)
    2.16 +#120 := (= #119 f1)
    2.17 +#121 := (not #120)
    2.18 +#426 := (iff #121 #425)
    2.19 +#423 := (iff #120 #421)
    2.20 +#424 := [rewrite]: #423
    2.21 +#427 := [monotonicity #424]: #426
    2.22 +#420 := [asserted]: #121
    2.23 +#430 := [mp #420 #427]: #425
    2.24 +#8 := (:var 0 Int)
    2.25 +#9 := (f3 #8)
    2.26 +#953 := (pattern #9)
    2.27 +#142 := (= f1 #9)
    2.28 +#954 := (forall (vars (?v0 Int)) (:pat #953) #142)
    2.29 +#165 := (forall (vars (?v0 Int)) #142)
    2.30 +#957 := (iff #165 #954)
    2.31 +#955 := (iff #142 #142)
    2.32 +#956 := [refl]: #955
    2.33 +#958 := [quant-intro #956]: #957
    2.34 +#456 := (~ #165 #165)
    2.35 +#454 := (~ #142 #142)
    2.36 +#455 := [refl]: #454
    2.37 +#457 := [nnf-pos #455]: #456
    2.38 +decl f4 :: (-> S2 S1)
    2.39 +decl f5 :: (-> Int S2 S2)
    2.40 +decl f6 :: S2
    2.41 +#11 := f6
    2.42 +#12 := (f5 #8 f6)
    2.43 +#13 := (f4 #12)
    2.44 +#14 := (= #13 f1)
    2.45 +#15 := (not #14)
    2.46 +#16 := (or #14 #15)
    2.47 +#10 := (= #9 f1)
    2.48 +#17 := (and #10 #16)
    2.49 +#18 := (forall (vars (?v0 Int)) #17)
    2.50 +#166 := (iff #18 #165)
    2.51 +#163 := (iff #17 #142)
    2.52 +#1 := true
    2.53 +#158 := (and #142 true)
    2.54 +#161 := (iff #158 #142)
    2.55 +#162 := [rewrite]: #161
    2.56 +#159 := (iff #17 #158)
    2.57 +#156 := (iff #16 true)
    2.58 +#145 := (= f1 #13)
    2.59 +#148 := (not #145)
    2.60 +#151 := (or #145 #148)
    2.61 +#154 := (iff #151 true)
    2.62 +#155 := [rewrite]: #154
    2.63 +#152 := (iff #16 #151)
    2.64 +#149 := (iff #15 #148)
    2.65 +#146 := (iff #14 #145)
    2.66 +#147 := [rewrite]: #146
    2.67 +#150 := [monotonicity #147]: #149
    2.68 +#153 := [monotonicity #147 #150]: #152
    2.69 +#157 := [trans #153 #155]: #156
    2.70 +#143 := (iff #10 #142)
    2.71 +#144 := [rewrite]: #143
    2.72 +#160 := [monotonicity #144 #157]: #159
    2.73 +#164 := [trans #160 #162]: #163
    2.74 +#167 := [quant-intro #164]: #166
    2.75 +#141 := [asserted]: #18
    2.76 +#170 := [mp #141 #167]: #165
    2.77 +#429 := [mp~ #170 #457]: #165
    2.78 +#959 := [mp #429 #958]: #954
    2.79 +#538 := (not #954)
    2.80 +#623 := (or #538 #421)
    2.81 +#624 := [quant-inst #118]: #623
    2.82 +[unit-resolution #624 #959 #430]: false
    2.83 +unsat
     3.1 --- a/src/HOL/Tools/SMT/smt_config.ML	Mon Feb 14 10:40:43 2011 +0100
     3.2 +++ b/src/HOL/Tools/SMT/smt_config.ML	Mon Feb 14 12:25:26 2011 +0100
     3.3 @@ -32,6 +32,7 @@
     3.4    val trace: bool Config.T
     3.5    val trace_used_facts: bool Config.T
     3.6    val monomorph_limit: int Config.T
     3.7 +  val monomorph_instances: int Config.T
     3.8    val infer_triggers: bool Config.T
     3.9    val drop_bad_facts: bool Config.T
    3.10    val filter_only_facts: bool Config.T
    3.11 @@ -176,6 +177,10 @@
    3.12  val (monomorph_limit, setup_monomorph_limit) =
    3.13    Attrib.config_int monomorph_limitN (K 10)
    3.14  
    3.15 +val monomorph_instancesN = "smt_monomorph_instances"
    3.16 +val (monomorph_instances, setup_monomorph_instances) =
    3.17 +  Attrib.config_int monomorph_instancesN (K 500)
    3.18 +
    3.19  val infer_triggersN = "smt_infer_triggers"
    3.20  val (infer_triggers, setup_infer_triggers) =
    3.21    Attrib.config_bool infer_triggersN (K false)
    3.22 @@ -201,6 +206,7 @@
    3.23    setup_trace #>
    3.24    setup_verbose #>
    3.25    setup_monomorph_limit #>
    3.26 +  setup_monomorph_instances #>
    3.27    setup_infer_triggers #>
    3.28    setup_drop_bad_facts #>
    3.29    setup_filter_only_facts #>
     4.1 --- a/src/HOL/Tools/SMT/smt_monomorph.ML	Mon Feb 14 10:40:43 2011 +0100
     4.2 +++ b/src/HOL/Tools/SMT/smt_monomorph.ML	Mon Feb 14 12:25:26 2011 +0100
     4.3 @@ -37,6 +37,10 @@
     4.4  
     4.5  (* utility functions *)
     4.6  
     4.7 +fun fold_maps f = fold (fn x => uncurry (fold_map (f x)) #>> flat)
     4.8 +
     4.9 +fun pair_trans ((x, y), z) = (x, (y, z))
    4.10 +
    4.11  val typ_has_tvars = Term.exists_subtype (fn TVar _ => true | _ => false)
    4.12  
    4.13  val ignored = member (op =) [@{const_name All}, @{const_name Ex},
    4.14 @@ -76,13 +80,14 @@
    4.15  
    4.16  (* search for necessary substitutions *)
    4.17  
    4.18 -fun new_substitutions thy limit grounds (n, T) subst =
    4.19 -  if not (typ_has_tvars T) then [subst]
    4.20 +fun new_substitutions thy limit grounds (n, T) subst instances =
    4.21 +  if not (typ_has_tvars T) then ([subst], instances)
    4.22    else
    4.23      Symtab.lookup_list grounds n
    4.24      |> map_filter (try (fn U => Sign.typ_match thy (T, U) subst))
    4.25 -    |> cons subst
    4.26 -    |> take limit (* limit the breadth of the search as well as the width *)
    4.27 +    |> (fn substs => (substs, instances - length substs))
    4.28 +    |>> take limit (* limit the breadth of the search as well as the width *)
    4.29 +    |>> cons subst
    4.30  
    4.31  fun apply_subst grounds consts subst =
    4.32    let
    4.33 @@ -100,11 +105,12 @@
    4.34  
    4.35  fun specialize thy limit all_grounds new_grounds scs =
    4.36    let
    4.37 -    fun spec (subst, consts) next_grounds =
    4.38 -      [subst]
    4.39 -      |> fold (maps o new_substitutions thy limit new_grounds) consts
    4.40 -      |> rpair next_grounds
    4.41 -      |-> fold_map (apply_subst all_grounds consts)
    4.42 +    fun spec (subst, consts) (next_grounds, instances) =
    4.43 +      ([subst], instances)
    4.44 +      |> fold_maps (new_substitutions thy limit new_grounds) consts
    4.45 +      |>> rpair next_grounds
    4.46 +      |>> uncurry (fold_map (apply_subst all_grounds consts))
    4.47 +      |> pair_trans
    4.48    in
    4.49      fold_map spec scs #>> (fn scss =>
    4.50      fold (fold (insert (eq_snd (op =)))) scss [])
    4.51 @@ -112,16 +118,18 @@
    4.52  
    4.53  val limit_reached_warning = "Warning: Monomorphization limit reached"
    4.54  
    4.55 -fun search_substitutions ctxt limit all_grounds new_grounds scss =
    4.56 +fun search_substitutions ctxt limit instances all_grounds new_grounds scss =
    4.57    let
    4.58      val thy = ProofContext.theory_of ctxt
    4.59      val all_grounds' = Symtab.merge_list (op =) (all_grounds, new_grounds)
    4.60      val spec = specialize thy limit all_grounds' new_grounds
    4.61 -    val (scss', new_grounds') = fold_map spec scss Symtab.empty
    4.62 +    val (scss', (new_grounds', instances')) =
    4.63 +      fold_map spec scss (Symtab.empty, instances)
    4.64    in
    4.65      if Symtab.is_empty new_grounds' then scss'
    4.66 -    else if limit > 0 then
    4.67 -      search_substitutions ctxt (limit-1) all_grounds' new_grounds' scss'
    4.68 +    else if limit > 0 andalso instances' > 0 then
    4.69 +      search_substitutions ctxt (limit-1) instances' all_grounds' new_grounds'
    4.70 +        scss'
    4.71      else (SMT_Config.verbose_msg ctxt (K limit_reached_warning) (); scss')
    4.72    end
    4.73  
    4.74 @@ -194,9 +202,10 @@
    4.75        |> fold (add_const_types (not o typ_has_tvars) o snd) polys
    4.76  
    4.77      val limit = Config.get ctxt SMT_Config.monomorph_limit
    4.78 +    val instances = Config.get ctxt SMT_Config.monomorph_instances
    4.79    in
    4.80      scss
    4.81 -    |> search_substitutions ctxt limit Symtab.empty grounds
    4.82 +    |> search_substitutions ctxt limit instances Symtab.empty grounds
    4.83      |> map (filter_most_specific (ProofContext.theory_of ctxt))
    4.84      |> rpair (monos, ctxt)
    4.85      |-> fold2 instantiate polys