# HG changeset patch
# User blanchet
# Date 1399222896 -7200
# Node ID b38c5b9cf59007119f49e451ebccea39f4dfbde2
# Parent  35ff4ede34094cbdac32d24d392542bca80584e5
added 'satx' to Sledgehammer's portfolio (cf. 'isar_try0')

diff -r 35ff4ede3409 -r b38c5b9cf590 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Sun May 04 18:57:45 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Sun May 04 19:01:36 2014 +0200
@@ -110,7 +110,7 @@
   bool * (string option * string option) * Time.time * real * bool * bool
   * (term, string) atp_step list * thm
 
-val basic_systematic_methods = [Metis_Method (NONE, NONE), Meson_Method, Blast_Method]
+val basic_systematic_methods = [Metis_Method (NONE, NONE), Meson_Method, Blast_Method, SATx_Method]
 val simp_based_methods = [Auto_Method, Simp_Method, Fastforce_Method, Force_Method]
 val basic_arith_methods = [Linarith_Method, Presburger_Method, Algebra_Method]
 
diff -r 35ff4ede3409 -r b38c5b9cf590 src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML	Sun May 04 18:57:45 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML	Sun May 04 19:01:36 2014 +0200
@@ -13,6 +13,7 @@
     Metis_Method of string option * string option |
     Meson_Method |
     SMT2_Method |
+    SATx_Method |
     Blast_Method |
     Simp_Method |
     Simp_Size_Method |
@@ -51,6 +52,7 @@
   Metis_Method of string option * string option |
   Meson_Method |
   SMT2_Method |
+  SATx_Method |
   Blast_Method |
   Simp_Method |
   Simp_Size_Method |
@@ -77,6 +79,7 @@
     "metis (" ^ commas (map_filter I [type_enc_opt, lam_trans_opt]) ^ ")"
   | Meson_Method => "meson"
   | SMT2_Method => "smt2"
+  | SATx_Method => "satx"
   | Blast_Method => "blast"
   | Simp_Method => "simp"
   | Simp_Size_Method => "simp add: size_ne_size_imp_ne"
@@ -105,7 +108,8 @@
     | _ =>
       Method.insert_tac global_facts THEN'
       (case meth of
-        Blast_Method => blast_tac ctxt
+        SATx_Method => SAT.satx_tac ctxt
+      | Blast_Method => blast_tac ctxt
       | Simp_Method => Simplifier.asm_full_simp_tac ctxt
       | Simp_Size_Method =>
         Simplifier.asm_full_simp_tac (Simplifier.add_simp @{thm size_ne_size_imp_ne} ctxt)