# HG changeset patch
# User blanchet
# Date 1402478926 -7200
# Node ID 5bf2a5c498c22fcc6684631860cc1d19547111e9
# Parent  df0f8ad7cc30c027a0fc1fb36ed066026ef7fe22
removed old SMT module from Sledgehammer

diff -r df0f8ad7cc30 -r 5bf2a5c498c2 src/HOL/Main.thy
--- 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 {*
diff -r df0f8ad7cc30 -r 5bf2a5c498c2 src/HOL/Sledgehammer.thy
--- 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"
diff -r df0f8ad7cc30 -r 5bf2a5c498c2 src/HOL/Tools/Sledgehammer/sledgehammer_commands.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
diff -r df0f8ad7cc30 -r 5bf2a5c498c2 src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML
--- 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
diff -r df0f8ad7cc30 -r 5bf2a5c498c2 src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML
--- 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