implement term order attribute (for experiments)
authorblanchet
Tue Mar 20 00:44:30 2012 +0100 (2012-03-20)
changeset 4703477da780ddd6b
parent 47033 baa9dc39ee51
child 47035 5248fae40f09
implement term order attribute (for experiments)
src/HOL/Tools/ATP/atp_systems.ML
src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
     1.1 --- a/src/HOL/Tools/ATP/atp_systems.ML	Tue Mar 20 00:44:30 2012 +0100
     1.2 +++ b/src/HOL/Tools/ATP/atp_systems.ML	Tue Mar 20 00:44:30 2012 +0100
     1.3 @@ -11,6 +11,11 @@
     1.4    type formula_kind = ATP_Problem.formula_kind
     1.5    type failure = ATP_Proof.failure
     1.6  
     1.7 +  type term_order =
     1.8 +    {is_lpo : bool,
     1.9 +     generate_weights : bool,
    1.10 +     generate_prec : bool,
    1.11 +     generate_simp : bool}
    1.12    type slice_spec = int * atp_format * string * string * bool
    1.13    type atp_config =
    1.14      {exec : string * string,
    1.15 @@ -54,6 +59,7 @@
    1.16    val waldmeisterN : string
    1.17    val z3_tptpN : string
    1.18    val remote_prefix : string
    1.19 +  val effective_term_order : Proof.context -> string -> term_order
    1.20    val remote_atp :
    1.21      string -> string -> string list -> (string * string) list
    1.22      -> (failure * string) list -> formula_kind -> formula_kind
    1.23 @@ -165,13 +171,34 @@
    1.24  val smartN = "smart"
    1.25  val kboN = "kbo"
    1.26  val lpoN = "lpo"
    1.27 -val weightsN = "_weights"
    1.28 -val precsN = "_precs"
    1.29 -val lrN = "_lr" (* SPASS-specific *)
    1.30 +val xweightsN = "_weights"
    1.31 +val xprecN = "_prec"
    1.32 +val xsimpN = "_simp" (* SPASS-specific *)
    1.33  
    1.34  val term_order =
    1.35    Attrib.setup_config_string @{binding atp_term_order} (K smartN)
    1.36  
    1.37 +type term_order =
    1.38 +  {is_lpo : bool,
    1.39 +   generate_weights : bool,
    1.40 +   generate_prec : bool,
    1.41 +   generate_simp : bool}
    1.42 +
    1.43 +fun effective_term_order ctxt atp =
    1.44 +  let val ord = Config.get ctxt term_order in
    1.45 +    if ord = smartN then
    1.46 +      if atp = spass_newN then
    1.47 +        {is_lpo = false, generate_weights = true, generate_prec = false,
    1.48 +         generate_simp = true}
    1.49 +      else
    1.50 +        {is_lpo = false, generate_weights = false, generate_prec = false,
    1.51 +         generate_simp = false}
    1.52 +    else
    1.53 +      {is_lpo = String.isSubstring lpoN ord,
    1.54 +       generate_weights = String.isSubstring xweightsN ord,
    1.55 +       generate_prec = String.isSubstring xprecN ord,
    1.56 +       generate_simp = String.isSubstring xsimpN ord}
    1.57 +  end
    1.58  
    1.59  (* Alt-Ergo *)
    1.60  
     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Tue Mar 20 00:44:30 2012 +0100
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Tue Mar 20 00:44:30 2012 +0100
     2.3 @@ -710,7 +710,11 @@
     2.4                             type_enc false lam_trans uncurried_aliases
     2.5                             readable_names true hyp_ts concl_t
     2.6                  fun sel_weights () = atp_problem_selection_weights atp_problem
     2.7 -                fun ord_weights () = atp_problem_term_order_weights atp_problem
     2.8 +                fun ord_weights () =
     2.9 +                  if #generate_weights (effective_term_order ctxt name) then
    2.10 +                    atp_problem_term_order_weights atp_problem
    2.11 +                  else
    2.12 +                    []
    2.13                  val full_proof = debug orelse isar_proof
    2.14                  val command =
    2.15                    File.shell_path command ^ " " ^