src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML	Thu Oct 29 18:23:29 2020 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML	Thu Oct 29 16:07:41 2020 +0100
@@ -9,10 +9,14 @@
 sig
   type stature = ATP_Problem_Generate.stature
 
+  datatype SMT_backend =
+    SMT_Default |
+    SMT_Verit of string
+
   datatype proof_method =
     Metis_Method of string option * string option |
     Meson_Method |
-    SMT_Method |
+    SMT_Method of SMT_backend |
     SATx_Method |
     Blast_Method |
     Simp_Method |
@@ -48,10 +52,14 @@
 open ATP_Problem_Generate
 open ATP_Proof_Reconstruct
 
+datatype SMT_backend =
+  SMT_Default |
+  SMT_Verit of string
+
 datatype proof_method =
   Metis_Method of string option * string option |
   Meson_Method |
-  SMT_Method |
+  SMT_Method of SMT_backend |
   SATx_Method |
   Blast_Method |
   Simp_Method |
@@ -73,7 +81,7 @@
 
 fun is_proof_method_direct (Metis_Method _) = true
   | is_proof_method_direct Meson_Method = true
-  | is_proof_method_direct SMT_Method = true
+  | is_proof_method_direct (SMT_Method _) = true
   | is_proof_method_direct Simp_Method = true
   | is_proof_method_direct _ = false
 
@@ -93,7 +101,9 @@
       | Metis_Method (type_enc_opt, lam_trans_opt) =>
         "metis (" ^ commas (map_filter I [type_enc_opt, lam_trans_opt]) ^ ")"
       | Meson_Method => "meson"
-      | SMT_Method => "smt"
+      | SMT_Method SMT_Default => "smt"
+      | SMT_Method (SMT_Verit strategy) =>
+        "smt (" ^ commas ("verit" :: (if strategy = "default" then [] else [strategy])) ^ ")"
       | SATx_Method => "satx"
       | Blast_Method => "blast"
       | Simp_Method => if null ss then "simp" else "simp add:"
@@ -109,34 +119,41 @@
   end
 
 fun tac_of_proof_method ctxt (local_facts, global_facts) meth =
-  (case meth of
-    Metis_Method (type_enc_opt, lam_trans_opt) =>
-    let
-      val ctxt = ctxt
-        |> Config.put Metis_Tactic.verbose false
-        |> Config.put Metis_Tactic.trace false
-    in
-      SELECT_GOAL (Metis_Tactic.metis_method ((Option.map single type_enc_opt, lam_trans_opt),
-        global_facts) ctxt local_facts)
-    end
-  | SMT_Method => SMT_Solver.smt_tac ctxt (local_facts @ global_facts)
-  | _ =>
-    Method.insert_tac ctxt local_facts THEN'
+  let
+    fun tac_of_metis (type_enc_opt, lam_trans_opt) =
+      let
+        val ctxt = ctxt
+          |> Config.put Metis_Tactic.verbose false
+          |> Config.put Metis_Tactic.trace false
+      in
+        SELECT_GOAL (Metis_Tactic.metis_method ((Option.map single type_enc_opt, lam_trans_opt),
+          global_facts) ctxt local_facts)
+      end
+
+    fun tac_of_smt SMT_Default = SMT_Solver.smt_tac
+      | tac_of_smt (SMT_Verit strategy) = Verit_Proof.verit_tac_stgy strategy
+  in
     (case meth of
-      Meson_Method => Meson_Tactic.meson_general_tac ctxt global_facts
-    | Simp_Method => Simplifier.asm_full_simp_tac (ctxt addsimps global_facts)
+      Metis_Method options => tac_of_metis options
+    | SMT_Method backend => tac_of_smt backend ctxt (local_facts @ global_facts)
     | _ =>
-      Method.insert_tac ctxt global_facts THEN'
+      Method.insert_tac ctxt local_facts THEN'
       (case meth of
-        SATx_Method => SAT.satx_tac ctxt
-      | Blast_Method => blast_tac ctxt
-      | Auto_Method => SELECT_GOAL (Clasimp.auto_tac ctxt)
-      | Fastforce_Method => Clasimp.fast_force_tac ctxt
-      | Force_Method => Clasimp.force_tac ctxt
-      | Moura_Method => moura_tac ctxt
-      | Linarith_Method => Lin_Arith.tac ctxt
-      | Presburger_Method => Cooper.tac true [] [] ctxt
-      | Algebra_Method => Groebner.algebra_tac [] [] ctxt)))
+        Meson_Method => Meson_Tactic.meson_general_tac ctxt global_facts
+      | Simp_Method => Simplifier.asm_full_simp_tac (ctxt addsimps global_facts)
+      | _ =>
+        Method.insert_tac ctxt global_facts THEN'
+        (case meth of
+          SATx_Method => SAT.satx_tac ctxt
+        | Blast_Method => blast_tac ctxt
+        | Auto_Method => SELECT_GOAL (Clasimp.auto_tac ctxt)
+        | Fastforce_Method => Clasimp.fast_force_tac ctxt
+        | Force_Method => Clasimp.force_tac ctxt
+        | Moura_Method => moura_tac ctxt
+        | Linarith_Method => Lin_Arith.tac ctxt
+        | Presburger_Method => Cooper.tac true [] [] ctxt
+        | Algebra_Method => Groebner.algebra_tac [] [] ctxt)))
+  end
 
 fun string_of_play_outcome (Played time) = string_of_ext_time (false, time)
   | string_of_play_outcome (Play_Timed_Out time) =
@@ -158,7 +175,7 @@
   | apply_on_subgoal i n = "prefer " ^ string_of_int i ^ " " ^ apply_on_subgoal 1 n
 
 (* FIXME *)
-fun proof_method_command ctxt meth i n used_chaineds _(*num_chained*) extras =
+fun proof_method_command meth i n used_chaineds _(*num_chained*) extras =
   let
     val (indirect_ss, direct_ss) =
       if is_proof_method_direct meth then
@@ -177,11 +194,11 @@
     (s |> s <> "" ? enclose " (" ")")
   end
 
-fun one_line_proof_text ctxt num_chained
+fun one_line_proof_text _ num_chained
     ((used_facts, (meth, play)), banner, subgoal, subgoal_count) =
   let val (chained, extra) = List.partition (fn (_, (sc, _)) => sc = Chained) used_facts in
     map fst extra
-    |> proof_method_command ctxt meth subgoal subgoal_count (map fst chained) num_chained
+    |> proof_method_command meth subgoal subgoal_count (map fst chained) num_chained
     |> (if play = Play_Failed then prefix "One-line proof reconstruction failed: "
         else try_command_line banner play)
   end