# HG changeset patch
# User desharna
# Date 1637175137 -3600
# Node ID db4b8dd587a5e10c9469397a2e383637af26fa80
# Parent  11e34ffc65e48be5b8527fc5a8b540f9f022c8db
added support for higher-order SMT proof search in Sledgehammer

diff -r 11e34ffc65e4 -r db4b8dd587a5 src/HOL/Tools/ATP/atp_problem_generate.ML
--- 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)
diff -r 11e34ffc65e4 -r db4b8dd587a5 src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML
--- 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))