properly take quantifiers into account (cf. my Ph.D. thesis, Section 6.4.1) and offer three modes of completeness (for experiments mostly)
authorblanchet
Sun Oct 01 15:01:39 2017 +0200 (21 months ago)
changeset 66738793e7a9c30c5
parent 66737 2edc0c42c883
child 66739 1e5c7599aa5b
properly take quantifiers into account (cf. my Ph.D. thesis, Section 6.4.1) and offer three modes of completeness (for experiments mostly)
src/HOL/SMT_Examples/SMT_Tests.thy
src/HOL/Tools/SMT/smt_config.ML
src/HOL/Tools/SMT/smt_translate.ML
     1.1 --- a/src/HOL/SMT_Examples/SMT_Tests.thy	Sun Oct 01 13:07:31 2017 +0200
     1.2 +++ b/src/HOL/SMT_Examples/SMT_Tests.thy	Sun Oct 01 15:01:39 2017 +0200
     1.3 @@ -604,7 +604,7 @@
     1.4    by smt+
     1.5  
     1.6  
     1.7 -section \<open>Datatypes, Records, and Typedefs\<close>
     1.8 +section \<open>Datatypes, records, and typedefs\<close>
     1.9  
    1.10  subsection \<open>Without support by the SMT solver\<close>
    1.11  
    1.12 @@ -843,7 +843,10 @@
    1.13    by (smt n0_def n1_def n2_def plus'_def)+
    1.14  
    1.15  
    1.16 -section \<open>Function updates\<close>
    1.17 +section \<open>Functions\<close>
    1.18 +
    1.19 +lemma "\<exists>f. map_option f (Some x) = Some (y + x)"
    1.20 +  by (smt option.map(2))
    1.21  
    1.22  lemma
    1.23    "(f (i := v)) i = v"
     2.1 --- a/src/HOL/Tools/SMT/smt_config.ML	Sun Oct 01 13:07:31 2017 +0200
     2.2 +++ b/src/HOL/Tools/SMT/smt_config.ML	Sun Oct 01 15:01:39 2017 +0200
     2.3 @@ -32,6 +32,7 @@
     2.4    val statistics: bool Config.T
     2.5    val monomorph_limit: int Config.T
     2.6    val monomorph_instances: int Config.T
     2.7 +  val explicit_application: int Config.T
     2.8    val higher_order: bool Config.T
     2.9    val nat_as_int: bool Config.T
    2.10    val infer_triggers: bool Config.T
    2.11 @@ -181,6 +182,7 @@
    2.12  val statistics = Attrib.setup_config_bool @{binding smt_statistics} (K false)
    2.13  val monomorph_limit = Attrib.setup_config_int @{binding smt_monomorph_limit} (K 10)
    2.14  val monomorph_instances = Attrib.setup_config_int @{binding smt_monomorph_instances} (K 500)
    2.15 +val explicit_application = Attrib.setup_config_int @{binding smt_explicit_application} (K 1)
    2.16  val higher_order = Attrib.setup_config_bool @{binding smt_higher_order} (K false)
    2.17  val nat_as_int = Attrib.setup_config_bool @{binding smt_nat_as_int} (K false)
    2.18  val infer_triggers = Attrib.setup_config_bool @{binding smt_infer_triggers} (K false)
     3.1 --- a/src/HOL/Tools/SMT/smt_translate.ML	Sun Oct 01 13:07:31 2017 +0200
     3.2 +++ b/src/HOL/Tools/SMT/smt_translate.ML	Sun Oct 01 15:01:39 2017 +0200
     3.3 @@ -250,14 +250,12 @@
     3.4      | (Abs (_, T, u), ts) => (can dest_funT T ? add_type T) #> min_arities u #> fold min_arities ts
     3.5      | (_, ts) => fold min_arities ts)
     3.6  
     3.7 -  fun minimize types t i =
     3.8 +  fun take_vars_into_account types t i =
     3.9      let
    3.10 -      fun find_min j [] _ = j
    3.11 -        | find_min j (U :: Us) T =
    3.12 -            if Typtab.defined types T then j else find_min (j + 1) Us (U --> T)
    3.13 -
    3.14 -      val (Ts, T) = Term.strip_type (Term.type_of t)
    3.15 -    in find_min 0 (take i (rev Ts)) T end
    3.16 +      fun find_min j (T as Type (@{type_name fun}, [_, T'])) =
    3.17 +          if j = i orelse Typtab.defined types T then j else find_min (j + 1) T'
    3.18 +        | find_min j _ = j
    3.19 +    in find_min 0 (Term.type_of t) end
    3.20  
    3.21    fun app u (t, T) = (Const (@{const_name fun_app}, T --> T) $ t $ u, Term.range_type T)
    3.22  
    3.23 @@ -270,12 +268,21 @@
    3.24  
    3.25  fun intro_explicit_application ctxt funcs ts =
    3.26    let
    3.27 -    val (arities, types) = fold min_arities ts (Termtab.empty, Typtab.empty)
    3.28 -    val arities' = Termtab.map (minimize types) arities (* FIXME: highly suspicious *)
    3.29 +    val explicit_application = Config.get ctxt SMT_Config.explicit_application
    3.30 +    val get_arities =
    3.31 +      (case explicit_application of
    3.32 +        0 => min_arities
    3.33 +      | 1 => min_arities
    3.34 +      | 2 => K I
    3.35 +      | n => error ("Illegal value for " ^ quote (Config.name_of SMT_Config.explicit_application) ^
    3.36 +          ": " ^ string_of_int n))
    3.37 +
    3.38 +    val (arities, types) = fold get_arities ts (Termtab.empty, Typtab.empty)
    3.39 +    val arities' = arities |> explicit_application = 1 ? Termtab.map (take_vars_into_account types)
    3.40  
    3.41      fun app_func t T ts =
    3.42        if is_some (Termtab.lookup funcs t) then Term.list_comb (t, ts)
    3.43 -      else apply (the (Termtab.lookup arities' t)) t T ts
    3.44 +      else apply (the_default 0 (Termtab.lookup arities' t)) t T ts
    3.45  
    3.46      fun in_list T f t = SMT_Util.mk_symb_list T (map f (SMT_Util.dest_symb_list t))
    3.47