move all ATP setup code into ATP_Wrapper
authorblanchet
Fri Mar 19 15:33:18 2010 +0100 (2010-03-19)
changeset 3586716279c4c7a33
parent 35866 513074557e06
child 35868 491a97039ce1
move all ATP setup code into ATP_Wrapper
src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
src/HOL/Sledgehammer.thy
src/HOL/Tools/ATP_Manager/atp_manager.ML
src/HOL/Tools/ATP_Manager/atp_minimal.ML
src/HOL/Tools/ATP_Manager/atp_wrapper.ML
     1.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Fri Mar 19 15:07:44 2010 +0100
     1.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Fri Mar 19 15:33:18 2010 +0100
     1.3 @@ -307,13 +307,13 @@
     1.4        ctxt
     1.5        |> change_dir dir
     1.6        |> Config.put ATP_Wrapper.measure_runtime true
     1.7 -    val problem = ATP_Wrapper.problem_of_goal (! ATP_Manager.full_types) 1 (ctxt', (facts, goal));
     1.8 +    val problem = ATP_Manager.problem_of_goal (! ATP_Manager.full_types) 1 (ctxt', (facts, goal));
     1.9  
    1.10      val time_limit =
    1.11        (case hard_timeout of
    1.12          NONE => I
    1.13        | SOME secs => TimeLimit.timeLimit (Time.fromSeconds secs))
    1.14 -    val ({success, message, theorem_names, runtime=time_atp, ...}: ATP_Wrapper.prover_result,
    1.15 +    val ({success, message, theorem_names, runtime=time_atp, ...}: ATP_Manager.prover_result,
    1.16          time_isa) = time_limit (Mirabelle.cpu_time (fn t => prover t problem)) timeout
    1.17    in
    1.18      if success then (message, SH_OK (time_isa, time_atp, theorem_names))
     2.1 --- a/src/HOL/Sledgehammer.thy	Fri Mar 19 15:07:44 2010 +0100
     2.2 +++ b/src/HOL/Sledgehammer.thy	Fri Mar 19 15:33:18 2010 +0100
     2.3 @@ -101,29 +101,10 @@
     2.4  use "Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML"
     2.5  setup Sledgehammer_Proof_Reconstruct.setup
     2.6  use "Tools/Sledgehammer/sledgehammer_fact_filter.ML"
     2.7 -
     2.8 +use "Tools/ATP_Manager/atp_manager.ML"
     2.9  use "Tools/ATP_Manager/atp_wrapper.ML"
    2.10  setup ATP_Wrapper.setup
    2.11 -use "Tools/ATP_Manager/atp_manager.ML"
    2.12  use "Tools/ATP_Manager/atp_minimal.ML"
    2.13 -
    2.14 -text {* basic provers *}
    2.15 -setup {* ATP_Manager.add_prover ATP_Wrapper.spass *}
    2.16 -setup {* ATP_Manager.add_prover ATP_Wrapper.vampire *}
    2.17 -setup {* ATP_Manager.add_prover ATP_Wrapper.eprover *}
    2.18 -
    2.19 -text {* provers with stuctured output *}
    2.20 -setup {* ATP_Manager.add_prover ATP_Wrapper.vampire_full *}
    2.21 -setup {* ATP_Manager.add_prover ATP_Wrapper.eprover_full *}
    2.22 -
    2.23 -text {* on some problems better results *}
    2.24 -setup {* ATP_Manager.add_prover ATP_Wrapper.spass_no_tc *}
    2.25 -
    2.26 -text {* remote provers via SystemOnTPTP *}
    2.27 -setup {* ATP_Manager.add_prover ATP_Wrapper.remote_vampire *}
    2.28 -setup {* ATP_Manager.add_prover ATP_Wrapper.remote_spass *}
    2.29 -setup {* ATP_Manager.add_prover ATP_Wrapper.remote_eprover *}
    2.30 -
    2.31  use "Tools/Sledgehammer/sledgehammer_isar.ML"
    2.32  
    2.33  
     3.1 --- a/src/HOL/Tools/ATP_Manager/atp_manager.ML	Fri Mar 19 15:07:44 2010 +0100
     3.2 +++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML	Fri Mar 19 15:33:18 2010 +0100
     3.3 @@ -7,6 +7,23 @@
     3.4  
     3.5  signature ATP_MANAGER =
     3.6  sig
     3.7 +  type problem =
     3.8 +   {with_full_types: bool,
     3.9 +    subgoal: int,
    3.10 +    goal: Proof.context * (thm list * thm),
    3.11 +    axiom_clauses: (thm * (string * int)) list option,
    3.12 +    filtered_clauses: (thm * (string * int)) list option}
    3.13 +  val problem_of_goal: bool -> int -> Proof.context * (thm list * thm) -> problem
    3.14 +  type prover_result =
    3.15 +   {success: bool,
    3.16 +    message: string,
    3.17 +    theorem_names: string list,
    3.18 +    runtime: int,
    3.19 +    proof: string,
    3.20 +    internal_thm_names: string Vector.vector,
    3.21 +    filtered_clauses: (thm * (string * int)) list}
    3.22 +  type prover = int -> problem -> prover_result
    3.23 +
    3.24    val atps: string Unsynchronized.ref
    3.25    val get_atps: unit -> string list
    3.26    val timeout: int Unsynchronized.ref
    3.27 @@ -14,8 +31,8 @@
    3.28    val kill: unit -> unit
    3.29    val info: unit -> unit
    3.30    val messages: int option -> unit
    3.31 -  val add_prover: string * ATP_Wrapper.prover -> theory -> theory
    3.32 -  val get_prover: theory -> string -> ATP_Wrapper.prover option
    3.33 +  val add_prover: string * prover -> theory -> theory
    3.34 +  val get_prover: theory -> string -> prover option
    3.35    val print_provers: theory -> unit
    3.36    val sledgehammer: string list -> Proof.state -> unit
    3.37  end;
    3.38 @@ -23,6 +40,34 @@
    3.39  structure ATP_Manager : ATP_MANAGER =
    3.40  struct
    3.41  
    3.42 +(** problems, results, and provers **)
    3.43 +
    3.44 +type problem =
    3.45 + {with_full_types: bool,
    3.46 +  subgoal: int,
    3.47 +  goal: Proof.context * (thm list * thm),
    3.48 +  axiom_clauses: (thm * (string * int)) list option,
    3.49 +  filtered_clauses: (thm * (string * int)) list option};
    3.50 +
    3.51 +fun problem_of_goal with_full_types subgoal goal : problem =
    3.52 + {with_full_types = with_full_types,
    3.53 +  subgoal = subgoal,
    3.54 +  goal = goal,
    3.55 +  axiom_clauses = NONE,
    3.56 +  filtered_clauses = NONE};
    3.57 +
    3.58 +type prover_result =
    3.59 + {success: bool,
    3.60 +  message: string,
    3.61 +  theorem_names: string list,  (*relevant theorems*)
    3.62 +  runtime: int,  (*user time of the ATP, in milliseconds*)
    3.63 +  proof: string,
    3.64 +  internal_thm_names: string Vector.vector,
    3.65 +  filtered_clauses: (thm * (string * int)) list};
    3.66 +
    3.67 +type prover = int -> problem -> prover_result;
    3.68 +
    3.69 +
    3.70  (** preferences **)
    3.71  
    3.72  val message_store_limit = 20;
    3.73 @@ -228,7 +273,7 @@
    3.74  
    3.75  structure Provers = Theory_Data
    3.76  (
    3.77 -  type T = (ATP_Wrapper.prover * stamp) Symtab.table;
    3.78 +  type T = (prover * stamp) Symtab.table;
    3.79    val empty = Symtab.empty;
    3.80    val extend = I;
    3.81    fun merge data : T = Symtab.merge (eq_snd op =) data
    3.82 @@ -261,7 +306,7 @@
    3.83          val _ = Toplevel.thread true (fn () =>
    3.84            let
    3.85              val _ = register birth_time death_time (Thread.self (), desc);
    3.86 -            val problem = ATP_Wrapper.problem_of_goal (! full_types) i (ctxt, (facts, goal));
    3.87 +            val problem = problem_of_goal (! full_types) i (ctxt, (facts, goal));
    3.88              val message = #message (prover (! timeout) problem)
    3.89                handle Sledgehammer_HOL_Clause.TRIVIAL =>   (* FIXME !? *)
    3.90                    "Empty clause: Try this command: " ^ Markup.markup Markup.sendback "apply metis"
     4.1 --- a/src/HOL/Tools/ATP_Manager/atp_minimal.ML	Fri Mar 19 15:07:44 2010 +0100
     4.2 +++ b/src/HOL/Tools/ATP_Manager/atp_minimal.ML	Fri Mar 19 15:33:18 2010 +0100
     4.3 @@ -1,16 +1,19 @@
     4.4  (*  Title:      HOL/Tools/ATP_Manager/atp_minimal.ML
     4.5      Author:     Philipp Meyer, TU Muenchen
     4.6  
     4.7 -Minimization of theorem list for metis by using an external automated theorem prover
     4.8 +Minimization of theorem list for Metis using automatic theorem provers.
     4.9  *)
    4.10  
    4.11  signature ATP_MINIMAL =
    4.12  sig
    4.13 +  type prover = ATP_Manager.prover
    4.14 +  type prover_result = ATP_Manager.prover_result
    4.15    type 'a minimize_fun = ('a list -> bool) -> 'a list -> 'a list
    4.16 +
    4.17    val linear_minimize : 'a minimize_fun
    4.18    val binary_minimize : 'a minimize_fun
    4.19    val minimize_theorems :
    4.20 -    (string * thm list) minimize_fun -> ATP_Wrapper.prover -> string -> int
    4.21 +    (string * thm list) minimize_fun -> prover -> string -> int
    4.22      -> Proof.state -> (string * thm list) list
    4.23      -> (string * thm list) list option * string
    4.24  end;
    4.25 @@ -19,6 +22,7 @@
    4.26  struct
    4.27  
    4.28  open Sledgehammer_Fact_Preprocessor
    4.29 +open ATP_Manager
    4.30  
    4.31  type 'a minimize_fun = ('a list -> bool) -> 'a list -> 'a list
    4.32  
    4.33 @@ -87,30 +91,29 @@
    4.34     ("# Cannot determine problem status within resource limit", Timeout),
    4.35     ("Error", Error)]
    4.36  
    4.37 -fun produce_answer (result : ATP_Wrapper.prover_result) =
    4.38 -  let
    4.39 -    val {success, proof = result_string, internal_thm_names = thm_name_vec,
    4.40 -      filtered_clauses = filtered, ...} = result
    4.41 -  in
    4.42 -    if success then
    4.43 -      (Success (Vector.foldr (op ::) [] thm_name_vec, filtered), result_string)
    4.44 -    else
    4.45 -      let
    4.46 -        val failure = failure_strings |> get_first (fn (s, t) =>
    4.47 -            if String.isSubstring s result_string then SOME (t, result_string) else NONE)
    4.48 -      in
    4.49 -        (case failure of
    4.50 -          SOME res => res
    4.51 -        | NONE => (Failure, result_string))
    4.52 -      end
    4.53 -  end
    4.54 +fun produce_answer ({success, proof, internal_thm_names, filtered_clauses, ...}
    4.55 +                    : prover_result) =
    4.56 +  if success then
    4.57 +    (Success (Vector.foldr (op ::) [] internal_thm_names, filtered_clauses),
    4.58 +     proof)
    4.59 +  else
    4.60 +    let
    4.61 +      val failure = failure_strings |> get_first (fn (s, t) =>
    4.62 +          if String.isSubstring s proof then SOME (t, proof) else NONE)
    4.63 +    in
    4.64 +      (case failure of
    4.65 +        SOME res => res
    4.66 +      | NONE => (Failure, proof))
    4.67 +    end
    4.68  
    4.69  
    4.70  (* wrapper for calling external prover *)
    4.71  
    4.72 -fun sh_test_thms prover time_limit subgoalno state filtered name_thms_pairs =
    4.73 +fun sledgehammer_test_theorems prover time_limit subgoalno state filtered
    4.74 +                               name_thms_pairs =
    4.75    let
    4.76 -    val _ = priority ("Testing " ^ string_of_int (length name_thms_pairs) ^ " theorems... ")
    4.77 +    val _ = priority ("Testing " ^ string_of_int (length name_thms_pairs) ^
    4.78 +                      " theorems... ")
    4.79      val name_thm_pairs = maps (fn (n, ths) => map (pair n) ths) name_thms_pairs
    4.80      val axclauses = cnf_rules_pairs (Proof.theory_of state) name_thm_pairs
    4.81      val {context = ctxt, facts, goal} = Proof.goal state
    4.82 @@ -122,9 +125,7 @@
    4.83        filtered_clauses = filtered}
    4.84      val (result, proof) = produce_answer (prover time_limit problem)
    4.85      val _ = priority (string_of_result result)
    4.86 -  in
    4.87 -    (result, proof)
    4.88 -  end
    4.89 +  in (result, proof) end
    4.90  
    4.91  
    4.92  (* minimalization of thms *)
    4.93 @@ -136,7 +137,7 @@
    4.94        priority ("Minimize called with " ^ string_of_int (length name_thms_pairs) ^
    4.95          " theorems, prover: " ^ prover_name ^
    4.96          ", time limit: " ^ string_of_int time_limit ^ " seconds")
    4.97 -    val test_thms_fun = sh_test_thms prover time_limit 1 state
    4.98 +    val test_thms_fun = sledgehammer_test_theorems prover time_limit 1 state
    4.99      fun test_thms filtered thms =
   4.100        case test_thms_fun filtered thms of (Success _, _) => true | _ => false
   4.101    in
     5.1 --- a/src/HOL/Tools/ATP_Manager/atp_wrapper.ML	Fri Mar 19 15:07:44 2010 +0100
     5.2 +++ b/src/HOL/Tools/ATP_Manager/atp_wrapper.ML	Fri Mar 19 15:33:18 2010 +0100
     5.3 @@ -6,48 +6,15 @@
     5.4  
     5.5  signature ATP_WRAPPER =
     5.6  sig
     5.7 -  (*hooks for problem files*)
     5.8 -  val destdir: string Config.T
     5.9 -  val problem_prefix: string Config.T
    5.10 -  val measure_runtime: bool Config.T
    5.11 -  val setup: theory -> theory
    5.12 +  type prover = ATP_Manager.prover
    5.13  
    5.14 -  (*prover configuration, problem format, and prover result*)
    5.15 -  type prover_config =
    5.16 -   {command: Path.T,
    5.17 -    arguments: int -> string,
    5.18 -    failure_strs: string list,
    5.19 -    max_new_clauses: int,
    5.20 -    insert_theory_const: bool,
    5.21 -    emit_structured_proof: bool}
    5.22 -  type problem =
    5.23 -   {with_full_types: bool,
    5.24 -    subgoal: int,
    5.25 -    goal: Proof.context * (thm list * thm),
    5.26 -    axiom_clauses: (thm * (string * int)) list option,
    5.27 -    filtered_clauses: (thm * (string * int)) list option}
    5.28 -  val problem_of_goal: bool -> int -> Proof.context * (thm list * thm) -> problem
    5.29 -  type prover_result =
    5.30 -   {success: bool,
    5.31 -    message: string,
    5.32 -    theorem_names: string list,
    5.33 -    runtime: int,
    5.34 -    proof: string,
    5.35 -    internal_thm_names: string Vector.vector,
    5.36 -    filtered_clauses: (thm * (string * int)) list}
    5.37 -  type prover = int -> problem -> prover_result
    5.38 +  (* hooks for problem files *)
    5.39 +  val destdir : string Config.T
    5.40 +  val problem_prefix : string Config.T
    5.41 +  val measure_runtime : bool Config.T
    5.42  
    5.43 -  (*common provers*)
    5.44 -  val vampire: string * prover
    5.45 -  val vampire_full: string * prover
    5.46 -  val eprover: string * prover
    5.47 -  val eprover_full: string * prover
    5.48 -  val spass: string * prover
    5.49 -  val spass_no_tc: string * prover
    5.50 -  val remote_vampire: string * prover
    5.51 -  val remote_eprover: string * prover
    5.52 -  val remote_spass: string * prover
    5.53 -  val refresh_systems: unit -> unit
    5.54 +  val refresh_systems_on_tptp : unit -> unit
    5.55 +  val setup : theory -> theory
    5.56  end;
    5.57  
    5.58  structure ATP_Wrapper : ATP_WRAPPER =
    5.59 @@ -56,6 +23,7 @@
    5.60  open Sledgehammer_HOL_Clause
    5.61  open Sledgehammer_Fact_Filter
    5.62  open Sledgehammer_Proof_Reconstruct
    5.63 +open ATP_Manager
    5.64  
    5.65  (** generic ATP wrapper **)
    5.66  
    5.67 @@ -70,10 +38,8 @@
    5.68  val (measure_runtime, measure_runtime_setup) =
    5.69    Attrib.config_bool "atp_measure_runtime" false;
    5.70  
    5.71 -val setup = destdir_setup #> problem_prefix_setup #> measure_runtime_setup;
    5.72  
    5.73 -
    5.74 -(* prover configuration, problem format, and prover result *)
    5.75 +(* prover configuration *)
    5.76  
    5.77  type prover_config =
    5.78   {command: Path.T,
    5.79 @@ -83,31 +49,6 @@
    5.80    insert_theory_const: bool,
    5.81    emit_structured_proof: bool};
    5.82  
    5.83 -type problem =
    5.84 - {with_full_types: bool,
    5.85 -  subgoal: int,
    5.86 -  goal: Proof.context * (thm list * thm),
    5.87 -  axiom_clauses: (thm * (string * int)) list option,
    5.88 -  filtered_clauses: (thm * (string * int)) list option};
    5.89 -
    5.90 -fun problem_of_goal with_full_types subgoal goal : problem =
    5.91 - {with_full_types = with_full_types,
    5.92 -  subgoal = subgoal,
    5.93 -  goal = goal,
    5.94 -  axiom_clauses = NONE,
    5.95 -  filtered_clauses = NONE};
    5.96 -
    5.97 -type prover_result =
    5.98 - {success: bool,
    5.99 -  message: string,
   5.100 -  theorem_names: string list,  (*relevant theorems*)
   5.101 -  runtime: int,  (*user time of the ATP, in milliseconds*)
   5.102 -  proof: string,
   5.103 -  internal_thm_names: string Vector.vector,
   5.104 -  filtered_clauses: (thm * (string * int)) list};
   5.105 -
   5.106 -type prover = int -> problem -> prover_result;
   5.107 -
   5.108  
   5.109  (* basic template *)
   5.110  
   5.111 @@ -316,7 +257,8 @@
   5.112      else split_lines answer
   5.113    end;
   5.114  
   5.115 -fun refresh_systems () = Synchronized.change systems (fn _ => get_systems ());
   5.116 +fun refresh_systems_on_tptp () =
   5.117 +  Synchronized.change systems (fn _ => get_systems ());
   5.118  
   5.119  fun get_system prefix = Synchronized.change_result systems (fn systems =>
   5.120    (if null systems then get_systems () else systems)
   5.121 @@ -347,4 +289,15 @@
   5.122  val remote_spass = tptp_prover ("remote_spass", remote_prover_config
   5.123    "SPASS---" "-x" spass_max_new_clauses spass_insert_theory_const);
   5.124  
   5.125 +val provers =
   5.126 +  [spass, vampire, eprover, vampire_full, eprover_full, spass_no_tc,
   5.127 +   remote_vampire, remote_spass, remote_eprover]
   5.128 +val prover_setup = fold add_prover provers
   5.129 +
   5.130 +val setup =
   5.131 +  destdir_setup
   5.132 +  #> problem_prefix_setup
   5.133 +  #> measure_runtime_setup
   5.134 +  #> prover_setup;
   5.135 +
   5.136  end;