--- a/src/HOL/Main.thy Wed Jun 11 08:58:42 2014 +0200
+++ b/src/HOL/Main.thy Wed Jun 11 11:28:46 2014 +0200
@@ -1,7 +1,7 @@
header {* Main HOL *}
theory Main
-imports Predicate_Compile Quickcheck_Narrowing Extraction Lifting_Sum Coinduction Nitpick BNF_GFP
+imports Predicate_Compile Quickcheck_Narrowing Extraction Lifting_Sum Coinduction Nitpick BNF_GFP SMT
begin
text {*
--- a/src/HOL/Sledgehammer.thy Wed Jun 11 08:58:42 2014 +0200
+++ b/src/HOL/Sledgehammer.thy Wed Jun 11 11:28:46 2014 +0200
@@ -7,7 +7,7 @@
header {* Sledgehammer: Isabelle--ATP Linkup *}
theory Sledgehammer
-imports ATP SMT SMT2
+imports ATP SMT2
keywords "sledgehammer" :: diag and "sledgehammer_params" :: thy_decl
begin
@@ -26,7 +26,6 @@
ML_file "Tools/Sledgehammer/sledgehammer_isar.ML"
ML_file "Tools/Sledgehammer/sledgehammer_prover.ML"
ML_file "Tools/Sledgehammer/sledgehammer_prover_atp.ML"
-ML_file "Tools/Sledgehammer/sledgehammer_prover_smt.ML"
ML_file "Tools/Sledgehammer/sledgehammer_prover_smt2.ML"
ML_file "Tools/Sledgehammer/sledgehammer_prover_minimize.ML"
ML_file "Tools/Sledgehammer/sledgehammer_mepo.ML"
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Wed Jun 11 08:58:42 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Wed Jun 11 11:28:46 2014 +0200
@@ -23,7 +23,6 @@
open Sledgehammer_Util
open Sledgehammer_Fact
open Sledgehammer_Prover
-open Sledgehammer_Prover_SMT
open Sledgehammer_Prover_Minimize
open Sledgehammer_MaSh
open Sledgehammer
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Wed Jun 11 08:58:42 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Wed Jun 11 11:28:46 2014 +0200
@@ -257,10 +257,10 @@
end
val canonical_isar_supported_prover = eN
-val z3_newN = "z3_new"
+val z3N = "z3"
fun isar_supported_prover_of thy name =
- if is_atp thy name orelse name = z3_newN then name
+ if is_atp thy name orelse name = z3N then name
else if is_atp_installed thy canonical_isar_supported_prover then canonical_isar_supported_prover
else name
@@ -290,7 +290,6 @@
val (remote_provers, local_provers) =
proof_method_names @
sort_strings (supported_atps thy) @
- sort_strings (SMT_Solver.available_solvers_of ctxt) @
sort_strings (SMT2_Config.available_solvers_of ctxt)
|> List.partition (String.isPrefix remote_prefix)
in
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML Wed Jun 11 08:58:42 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML Wed Jun 11 11:28:46 2014 +0200
@@ -48,7 +48,6 @@
open Sledgehammer_Isar
open Sledgehammer_Prover
open Sledgehammer_Prover_ATP
-open Sledgehammer_Prover_SMT
open Sledgehammer_Prover_SMT2
fun run_proof_method mode name (params as {verbose, timeout, type_enc, lam_trans, ...})
@@ -90,11 +89,11 @@
fun is_prover_supported ctxt =
let val thy = Proof_Context.theory_of ctxt in
- is_proof_method orf is_atp thy orf is_smt_prover ctxt orf is_smt2_prover ctxt
+ is_proof_method orf is_atp thy orf is_smt2_prover ctxt
end
fun is_prover_installed ctxt =
- is_proof_method orf is_smt_prover ctxt orf is_smt2_prover ctxt orf
+ is_proof_method orf is_smt2_prover ctxt orf
is_atp_installed (Proof_Context.theory_of ctxt)
val proof_method_default_max_facts = 20
@@ -105,8 +104,6 @@
proof_method_default_max_facts
else if is_atp thy name then
fold (Integer.max o fst o #1 o fst o snd) (#best_slices (get_atp thy name ()) ctxt) 0
- else if is_smt_prover ctxt name then
- SMT_Solver.default_max_relevant ctxt name
else if is_smt2_prover ctxt name then
SMT2_Solver.default_max_relevant ctxt name
else
@@ -117,7 +114,6 @@
let val thy = Proof_Context.theory_of ctxt in
if is_proof_method name then run_proof_method mode name
else if is_atp thy name then run_atp mode name
- else if is_smt_prover ctxt name then run_smt_solver mode name
else if is_smt2_prover ctxt name then run_smt2_solver mode name
else error ("No such prover: " ^ name ^ ".")
end