added support for higher-order SMT proof search in Sledgehammer

--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Fri Nov 12 00:10:16 2021 +0100
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Wed Nov 17 19:52:17 2021 +0100
@@ -681,6 +681,10 @@
 
     fun native_of_string s =
       let
+        val (_, s) =
+          (case try (unsuffix "_arith") s of
+            SOME s => (true, s)
+          | NONE => (false, s))
         val (with_let, s) =
           (case try (unsuffix "_let") s of
             SOME s => (true, s)

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML	Fri Nov 12 00:10:16 2021 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML	Wed Nov 17 19:52:17 2021 +0100
@@ -76,11 +76,17 @@
   not o exists_subtype (member (op =) [\<^typ>\<open>nat\<close>, \<^typ>\<open>int\<close>, HOLogic.realT])
 
 fun smt_filter_loop name ({debug, overlord, max_mono_iters, max_new_mono_instances, timeout, slice,
-      ...} : params) state goal i =
+      type_enc, ...} : params) state goal i =
   let
+    val (higher_order, nat_as_int) =
+      (case type_enc of
+        SOME s =>  (String.isSubstring "native_higher" s, String.isSubstring "arith" s)
+      | NONE => (false, false))
     fun repair_context ctxt =
       ctxt |> Context.proof_map (SMT_Config.select_solver name)
            |> Config.put SMT_Config.verbose debug
+           |> Config.put SMT_Config.higher_order higher_order
+           |> Config.put SMT_Config.nat_as_int nat_as_int
            |> (if overlord then
                  Config.put SMT_Config.debug_files
                    (overlord_file_location_of_prover name |> (fn (path, name) => path ^ "/" ^ name))