split 'linarith' and 'presburger' (to avoid annoying warnings + to speed up reconstruction when 'presburger' is needed)
authorblanchet
Tue Feb 04 23:11:18 2014 +0100 (2014-02-04 ago)
changeset 55323253a029335a2
parent 55322 3bf50e3cd727
child 55324 e04b75bd18e0
split 'linarith' and 'presburger' (to avoid annoying warnings + to speed up reconstruction when 'presburger' is needed)
src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML
src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML
src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Tue Feb 04 21:29:46 2014 +0000
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Tue Feb 04 23:11:18 2014 +0100
     1.3 @@ -111,9 +111,9 @@
     1.4    bool * (string option * string option) * Time.time * real * bool * bool
     1.5    * (term, string) atp_step list * thm
     1.6  
     1.7 -val basic_arith_methods = [Arith_Method, Algebra_Method]
     1.8 -val basic_systematic_methods = [Metis_Method (NONE, NONE), Blast_Method, Meson_Method]
     1.9 +val basic_systematic_methods = [Metis_Method (NONE, NONE), Meson_Method, Blast_Method]
    1.10  val simp_based_methods = [Simp_Method, Auto_Method, Fastforce_Method, Force_Method]
    1.11 +val basic_arith_methods = [Linarith_Method, Presburger_Method, Algebra_Method]
    1.12  
    1.13  val arith_methods = basic_arith_methods @ simp_based_methods @ basic_systematic_methods
    1.14  val datatype_methods = [Simp_Method, Simp_Size_Method]
     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML	Tue Feb 04 21:29:46 2014 +0000
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML	Tue Feb 04 23:11:18 2014 +0100
     2.3 @@ -84,7 +84,7 @@
     2.4          (case Lazy.force outcome of Played _ => true | _ => false)
     2.5        end
     2.6    in
     2.7 -    union (op =) meths1 meths2
     2.8 +    meths2 @ subtract (op =) meths2 meths1
     2.9      |> filter (is_method_hopeful l1 andf is_method_hopeful l2)
    2.10    end
    2.11  
     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML	Tue Feb 04 21:29:46 2014 +0000
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML	Tue Feb 04 23:11:18 2014 +0100
     3.3 @@ -13,13 +13,14 @@
     3.4      Metis_Method of string option * string option |
     3.5      Meson_Method |
     3.6      SMT_Method |
     3.7 +    Blast_Method |
     3.8      Simp_Method |
     3.9      Simp_Size_Method |
    3.10      Auto_Method |
    3.11      Fastforce_Method |
    3.12      Force_Method |
    3.13 -    Arith_Method |
    3.14 -    Blast_Method |
    3.15 +    Linarith_Method |
    3.16 +    Presburger_Method |
    3.17      Algebra_Method
    3.18  
    3.19    datatype play_outcome =
    3.20 @@ -32,8 +33,6 @@
    3.21    type one_line_params =
    3.22      (proof_method * play_outcome) * string * (string * stature) list * minimize_command * int * int
    3.23  
    3.24 -  val smtN : string
    3.25 -
    3.26    val string_of_proof_method : proof_method -> string
    3.27    val tac_of_proof_method : Proof.context -> thm list * thm list -> proof_method -> int -> tactic
    3.28    val string_of_play_outcome : play_outcome -> string
    3.29 @@ -53,13 +52,14 @@
    3.30    Metis_Method of string option * string option |
    3.31    Meson_Method |
    3.32    SMT_Method |
    3.33 +  Blast_Method |
    3.34    Simp_Method |
    3.35    Simp_Size_Method |
    3.36    Auto_Method |
    3.37    Fastforce_Method |
    3.38    Force_Method |
    3.39 -  Arith_Method |
    3.40 -  Blast_Method |
    3.41 +  Linarith_Method |
    3.42 +  Presburger_Method |
    3.43    Algebra_Method
    3.44  
    3.45  datatype play_outcome =
    3.46 @@ -72,8 +72,6 @@
    3.47  type one_line_params =
    3.48    (proof_method * play_outcome) * string * (string * stature) list * minimize_command * int * int
    3.49  
    3.50 -val smtN = "smt"
    3.51 -
    3.52  fun string_of_proof_method meth =
    3.53    (case meth of
    3.54      Metis_Method (NONE, NONE) => "metis"
    3.55 @@ -81,13 +79,14 @@
    3.56      "metis (" ^ commas (map_filter I [type_enc_opt, lam_trans_opt]) ^ ")"
    3.57    | Meson_Method => "meson"
    3.58    | SMT_Method => "smt"
    3.59 +  | Blast_Method => "blast"
    3.60    | Simp_Method => "simp"
    3.61    | Simp_Size_Method => "simp add: size_ne_size_imp_ne"
    3.62    | Auto_Method => "auto"
    3.63    | Fastforce_Method => "fastforce"
    3.64    | Force_Method => "force"
    3.65 -  | Arith_Method => "arith"
    3.66 -  | Blast_Method => "blast"
    3.67 +  | Linarith_Method => "linarith"
    3.68 +  | Presburger_Method => "presburger"
    3.69    | Algebra_Method => "algebra")
    3.70  
    3.71  fun tac_of_proof_method ctxt (local_facts, global_facts) meth =
    3.72 @@ -96,19 +95,20 @@
    3.73      Metis_Method (type_enc_opt, lam_trans_opt) =>
    3.74      Metis_Tactic.metis_tac [type_enc_opt |> the_default (hd partial_type_encs)]
    3.75        (lam_trans_opt |> the_default default_metis_lam_trans) ctxt global_facts
    3.76 +  | Meson_Method => Meson.meson_tac ctxt global_facts
    3.77    | SMT_Method => SMT_Solver.smt_tac ctxt global_facts
    3.78 -  | Meson_Method => Meson.meson_tac ctxt global_facts
    3.79    | _ =>
    3.80      Method.insert_tac global_facts THEN'
    3.81      (case meth of
    3.82 -      Simp_Method => Simplifier.asm_full_simp_tac ctxt
    3.83 +      Blast_Method => blast_tac ctxt
    3.84 +    | Simp_Method => Simplifier.asm_full_simp_tac ctxt
    3.85      | Simp_Size_Method =>
    3.86        Simplifier.asm_full_simp_tac (Simplifier.add_simp @{thm size_ne_size_imp_ne} ctxt)
    3.87      | Auto_Method => K (Clasimp.auto_tac ctxt)
    3.88      | Fastforce_Method => Clasimp.fast_force_tac ctxt
    3.89      | Force_Method => Clasimp.force_tac ctxt
    3.90 -    | Arith_Method => Arith_Data.arith_tac ctxt
    3.91 -    | Blast_Method => blast_tac ctxt
    3.92 +    | Linarith_Method => Lin_Arith.tac ctxt
    3.93 +    | Presburger_Method => Cooper.tac true [] [] ctxt
    3.94      | Algebra_Method => Groebner.algebra_tac [] [] ctxt))
    3.95  
    3.96  fun string_of_play_outcome (Played time) = string_of_ext_time (false, time)
     4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Tue Feb 04 21:29:46 2014 +0000
     4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Tue Feb 04 23:11:18 2014 +0100
     4.3 @@ -67,6 +67,7 @@
     4.4      -> prover_problem -> prover_result
     4.5  
     4.6    val SledgehammerN : string
     4.7 +  val smtN : string
     4.8    val overlord_file_location_of_prover : string -> string * string
     4.9    val proof_banner : mode -> string -> string
    4.10    val extract_proof_method : params -> proof_method -> string * (string * string list) list
    4.11 @@ -110,6 +111,8 @@
    4.12     "Async_Manager". *)
    4.13  val SledgehammerN = "Sledgehammer"
    4.14  
    4.15 +val smtN = "smt"
    4.16 +
    4.17  val proof_method_names = [metisN, smtN]
    4.18  val is_proof_method = member (op =) proof_method_names
    4.19