# HG changeset patch
# User blanchet
# Date 1506862899 -7200
# Node ID 793e7a9c30c557c23598f8383dfd2b518867ad7c
# Parent  2edc0c42c883967df343d3942d51f384b887cfd7
properly take quantifiers into account (cf. my Ph.D. thesis, Section 6.4.1) and offer three modes of completeness (for experiments mostly)

diff -r 2edc0c42c883 -r 793e7a9c30c5 src/HOL/SMT_Examples/SMT_Tests.thy
--- a/src/HOL/SMT_Examples/SMT_Tests.thy	Sun Oct 01 13:07:31 2017 +0200
+++ b/src/HOL/SMT_Examples/SMT_Tests.thy	Sun Oct 01 15:01:39 2017 +0200
@@ -604,7 +604,7 @@
   by smt+
 
 
-section \<open>Datatypes, Records, and Typedefs\<close>
+section \<open>Datatypes, records, and typedefs\<close>
 
 subsection \<open>Without support by the SMT solver\<close>
 
@@ -843,7 +843,10 @@
   by (smt n0_def n1_def n2_def plus'_def)+
 
 
-section \<open>Function updates\<close>
+section \<open>Functions\<close>
+
+lemma "\<exists>f. map_option f (Some x) = Some (y + x)"
+  by (smt option.map(2))
 
 lemma
   "(f (i := v)) i = v"
diff -r 2edc0c42c883 -r 793e7a9c30c5 src/HOL/Tools/SMT/smt_config.ML
--- a/src/HOL/Tools/SMT/smt_config.ML	Sun Oct 01 13:07:31 2017 +0200
+++ b/src/HOL/Tools/SMT/smt_config.ML	Sun Oct 01 15:01:39 2017 +0200
@@ -32,6 +32,7 @@
   val statistics: bool Config.T
   val monomorph_limit: int Config.T
   val monomorph_instances: int Config.T
+  val explicit_application: int Config.T
   val higher_order: bool Config.T
   val nat_as_int: bool Config.T
   val infer_triggers: bool Config.T
@@ -181,6 +182,7 @@
 val statistics = Attrib.setup_config_bool @{binding smt_statistics} (K false)
 val monomorph_limit = Attrib.setup_config_int @{binding smt_monomorph_limit} (K 10)
 val monomorph_instances = Attrib.setup_config_int @{binding smt_monomorph_instances} (K 500)
+val explicit_application = Attrib.setup_config_int @{binding smt_explicit_application} (K 1)
 val higher_order = Attrib.setup_config_bool @{binding smt_higher_order} (K false)
 val nat_as_int = Attrib.setup_config_bool @{binding smt_nat_as_int} (K false)
 val infer_triggers = Attrib.setup_config_bool @{binding smt_infer_triggers} (K false)
diff -r 2edc0c42c883 -r 793e7a9c30c5 src/HOL/Tools/SMT/smt_translate.ML
--- a/src/HOL/Tools/SMT/smt_translate.ML	Sun Oct 01 13:07:31 2017 +0200
+++ b/src/HOL/Tools/SMT/smt_translate.ML	Sun Oct 01 15:01:39 2017 +0200
@@ -250,14 +250,12 @@
     | (Abs (_, T, u), ts) => (can dest_funT T ? add_type T) #> min_arities u #> fold min_arities ts
     | (_, ts) => fold min_arities ts)
 
-  fun minimize types t i =
+  fun take_vars_into_account types t i =
     let
-      fun find_min j [] _ = j
-        | find_min j (U :: Us) T =
-            if Typtab.defined types T then j else find_min (j + 1) Us (U --> T)
-
-      val (Ts, T) = Term.strip_type (Term.type_of t)
-    in find_min 0 (take i (rev Ts)) T end
+      fun find_min j (T as Type (@{type_name fun}, [_, T'])) =
+          if j = i orelse Typtab.defined types T then j else find_min (j + 1) T'
+        | find_min j _ = j
+    in find_min 0 (Term.type_of t) end
 
   fun app u (t, T) = (Const (@{const_name fun_app}, T --> T) $ t $ u, Term.range_type T)
 
@@ -270,12 +268,21 @@
 
 fun intro_explicit_application ctxt funcs ts =
   let
-    val (arities, types) = fold min_arities ts (Termtab.empty, Typtab.empty)
-    val arities' = Termtab.map (minimize types) arities (* FIXME: highly suspicious *)
+    val explicit_application = Config.get ctxt SMT_Config.explicit_application
+    val get_arities =
+      (case explicit_application of
+        0 => min_arities
+      | 1 => min_arities
+      | 2 => K I
+      | n => error ("Illegal value for " ^ quote (Config.name_of SMT_Config.explicit_application) ^
+          ": " ^ string_of_int n))
+
+    val (arities, types) = fold get_arities ts (Termtab.empty, Typtab.empty)
+    val arities' = arities |> explicit_application = 1 ? Termtab.map (take_vars_into_account types)
 
     fun app_func t T ts =
       if is_some (Termtab.lookup funcs t) then Term.list_comb (t, ts)
-      else apply (the (Termtab.lookup arities' t)) t T ts
+      else apply (the_default 0 (Termtab.lookup arities' t)) t T ts
 
     fun in_list T f t = SMT_Util.mk_symb_list T (map f (SMT_Util.dest_symb_list t))