removed old SMT module from Sledgehammer
authorblanchet
Wed Jun 11 11:28:46 2014 +0200 (2014-06-11)
changeset 572085bf2a5c498c2
parent 57207 df0f8ad7cc30
child 57209 7ffa0f7e2775
removed old SMT module from Sledgehammer
src/HOL/Main.thy
src/HOL/Sledgehammer.thy
src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML
src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML
src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML
     1.1 --- a/src/HOL/Main.thy	Wed Jun 11 08:58:42 2014 +0200
     1.2 +++ b/src/HOL/Main.thy	Wed Jun 11 11:28:46 2014 +0200
     1.3 @@ -1,7 +1,7 @@
     1.4  header {* Main HOL *}
     1.5  
     1.6  theory Main
     1.7 -imports Predicate_Compile Quickcheck_Narrowing Extraction Lifting_Sum Coinduction Nitpick BNF_GFP
     1.8 +imports Predicate_Compile Quickcheck_Narrowing Extraction Lifting_Sum Coinduction Nitpick BNF_GFP SMT
     1.9  begin
    1.10  
    1.11  text {*
     2.1 --- a/src/HOL/Sledgehammer.thy	Wed Jun 11 08:58:42 2014 +0200
     2.2 +++ b/src/HOL/Sledgehammer.thy	Wed Jun 11 11:28:46 2014 +0200
     2.3 @@ -7,7 +7,7 @@
     2.4  header {* Sledgehammer: Isabelle--ATP Linkup *}
     2.5  
     2.6  theory Sledgehammer
     2.7 -imports ATP SMT SMT2
     2.8 +imports ATP SMT2
     2.9  keywords "sledgehammer" :: diag and "sledgehammer_params" :: thy_decl
    2.10  begin
    2.11  
    2.12 @@ -26,7 +26,6 @@
    2.13  ML_file "Tools/Sledgehammer/sledgehammer_isar.ML"
    2.14  ML_file "Tools/Sledgehammer/sledgehammer_prover.ML"
    2.15  ML_file "Tools/Sledgehammer/sledgehammer_prover_atp.ML"
    2.16 -ML_file "Tools/Sledgehammer/sledgehammer_prover_smt.ML"
    2.17  ML_file "Tools/Sledgehammer/sledgehammer_prover_smt2.ML"
    2.18  ML_file "Tools/Sledgehammer/sledgehammer_prover_minimize.ML"
    2.19  ML_file "Tools/Sledgehammer/sledgehammer_mepo.ML"
     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Wed Jun 11 08:58:42 2014 +0200
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Wed Jun 11 11:28:46 2014 +0200
     3.3 @@ -23,7 +23,6 @@
     3.4  open Sledgehammer_Util
     3.5  open Sledgehammer_Fact
     3.6  open Sledgehammer_Prover
     3.7 -open Sledgehammer_Prover_SMT
     3.8  open Sledgehammer_Prover_Minimize
     3.9  open Sledgehammer_MaSh
    3.10  open Sledgehammer
     4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Wed Jun 11 08:58:42 2014 +0200
     4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Wed Jun 11 11:28:46 2014 +0200
     4.3 @@ -257,10 +257,10 @@
     4.4    end
     4.5  
     4.6  val canonical_isar_supported_prover = eN
     4.7 -val z3_newN = "z3_new"
     4.8 +val z3N = "z3"
     4.9  
    4.10  fun isar_supported_prover_of thy name =
    4.11 -  if is_atp thy name orelse name = z3_newN then name
    4.12 +  if is_atp thy name orelse name = z3N then name
    4.13    else if is_atp_installed thy canonical_isar_supported_prover then canonical_isar_supported_prover
    4.14    else name
    4.15  
    4.16 @@ -290,7 +290,6 @@
    4.17      val (remote_provers, local_provers) =
    4.18        proof_method_names @
    4.19        sort_strings (supported_atps thy) @
    4.20 -      sort_strings (SMT_Solver.available_solvers_of ctxt) @
    4.21        sort_strings (SMT2_Config.available_solvers_of ctxt)
    4.22        |> List.partition (String.isPrefix remote_prefix)
    4.23    in
     5.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML	Wed Jun 11 08:58:42 2014 +0200
     5.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML	Wed Jun 11 11:28:46 2014 +0200
     5.3 @@ -48,7 +48,6 @@
     5.4  open Sledgehammer_Isar
     5.5  open Sledgehammer_Prover
     5.6  open Sledgehammer_Prover_ATP
     5.7 -open Sledgehammer_Prover_SMT
     5.8  open Sledgehammer_Prover_SMT2
     5.9  
    5.10  fun run_proof_method mode name (params as {verbose, timeout, type_enc, lam_trans, ...})
    5.11 @@ -90,11 +89,11 @@
    5.12  
    5.13  fun is_prover_supported ctxt =
    5.14    let val thy = Proof_Context.theory_of ctxt in
    5.15 -    is_proof_method orf is_atp thy orf is_smt_prover ctxt orf is_smt2_prover ctxt
    5.16 +    is_proof_method orf is_atp thy orf is_smt2_prover ctxt
    5.17    end
    5.18  
    5.19  fun is_prover_installed ctxt =
    5.20 -  is_proof_method orf is_smt_prover ctxt orf is_smt2_prover ctxt orf
    5.21 +  is_proof_method orf is_smt2_prover ctxt orf
    5.22    is_atp_installed (Proof_Context.theory_of ctxt)
    5.23  
    5.24  val proof_method_default_max_facts = 20
    5.25 @@ -105,8 +104,6 @@
    5.26        proof_method_default_max_facts
    5.27      else if is_atp thy name then
    5.28        fold (Integer.max o fst o #1 o fst o snd) (#best_slices (get_atp thy name ()) ctxt) 0
    5.29 -    else if is_smt_prover ctxt name then
    5.30 -      SMT_Solver.default_max_relevant ctxt name
    5.31      else if is_smt2_prover ctxt name then
    5.32        SMT2_Solver.default_max_relevant ctxt name
    5.33      else
    5.34 @@ -117,7 +114,6 @@
    5.35    let val thy = Proof_Context.theory_of ctxt in
    5.36      if is_proof_method name then run_proof_method mode name
    5.37      else if is_atp thy name then run_atp mode name
    5.38 -    else if is_smt_prover ctxt name then run_smt_solver mode name
    5.39      else if is_smt2_prover ctxt name then run_smt2_solver mode name
    5.40      else error ("No such prover: " ^ name ^ ".")
    5.41    end