--- 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)