# HG changeset patch
# User blanchet
# Date 1391434519 -3600
# Node ID bd27ac6ad1c3343b3ddbe51017940a72584ef62b
# Parent  b90c06d54d38640497f455be2a3605d8ee8262e2
added 'smt' as a proof method

diff -r b90c06d54d38 -r bd27ac6ad1c3 src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML	Mon Feb 03 14:30:16 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML	Mon Feb 03 14:35:19 2014 +0100
@@ -103,10 +103,11 @@
 fun tac_of_method ctxt (local_facts, global_facts) meth =
   Method.insert_tac local_facts THEN'
   (case meth of
-    Meson_Method => Meson.meson_tac ctxt global_facts
-  | Metis_Method (type_enc_opt, lam_trans_opt) =>
+    Metis_Method (type_enc_opt, lam_trans_opt) =>
     Metis_Tactic.metis_tac [type_enc_opt |> the_default partial_type_enc]
       (the_default default_metis_lam_trans lam_trans_opt) ctxt global_facts
+  | SMT_Method => SMT_Solver.smt_tac ctxt global_facts
+  | Meson_Method => Meson.meson_tac ctxt global_facts
   | _ =>
     Method.insert_tac global_facts THEN'
     (case meth of
@@ -118,8 +119,7 @@
     | Force_Method => Clasimp.force_tac ctxt
     | Arith_Method => Arith_Data.arith_tac ctxt
     | Blast_Method => blast_tac ctxt
-    | Algebra_Method => Groebner.algebra_tac [] [] ctxt
-    | _ => raise Fail "Sledgehammer_Isar_Preplay: tac_of_method"))
+    | Algebra_Method => Groebner.algebra_tac [] [] ctxt))
 
 (* main function for preplaying Isar steps; may throw exceptions *)
 fun raw_preplay_step_for_method ctxt timeout meth (Prove (_, xs, _, t, subproofs, fact_names, _)) =
diff -r b90c06d54d38 -r bd27ac6ad1c3 src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML	Mon Feb 03 14:30:16 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML	Mon Feb 03 14:35:19 2014 +0100
@@ -15,6 +15,8 @@
 
   datatype proof_method =
     Metis_Method of string option * string option |
+    Meson_Method |
+    SMT_Method |
     Simp_Method |
     Simp_Size_Method |
     Auto_Method |
@@ -22,7 +24,6 @@
     Force_Method |
     Arith_Method |
     Blast_Method |
-    Meson_Method |
     Algebra_Method
 
   datatype isar_proof =
@@ -80,6 +81,8 @@
 
 datatype proof_method =
   Metis_Method of string option * string option |
+  Meson_Method |
+  SMT_Method |
   Simp_Method |
   Simp_Size_Method |
   Auto_Method |
@@ -87,7 +90,6 @@
   Force_Method |
   Arith_Method |
   Blast_Method |
-  Meson_Method |
   Algebra_Method
 
 datatype isar_proof =
@@ -108,6 +110,8 @@
     Metis_Method (NONE, NONE) => "metis"
   | 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"
   | Simp_Method => "simp"
   | Simp_Size_Method => "simp add: size_ne_size_imp_ne"
   | Auto_Method => "auto"
@@ -115,7 +119,6 @@
   | Force_Method => "force"
   | Arith_Method => "arith"
   | Blast_Method => "blast"
-  | Meson_Method => "meson"
   | Algebra_Method => "algebra")
 
 fun steps_of_isar_proof (Proof (_, _, steps)) = steps
@@ -291,6 +294,7 @@
 
     fun is_direct_method (Metis_Method _) = true
       | is_direct_method Meson_Method = true
+      | is_direct_method SMT_Method = true
       | is_direct_method _ = false
 
     (* Local facts are always passed via "using", which affects "meson" and "metis". This is