src/HOL/Tools/ATP_Manager/atp_wrapper.ML
changeset 35867 16279c4c7a33
parent 35865 2f8fb5242799
child 35868 491a97039ce1
     1.1 --- a/src/HOL/Tools/ATP_Manager/atp_wrapper.ML	Fri Mar 19 15:07:44 2010 +0100
     1.2 +++ b/src/HOL/Tools/ATP_Manager/atp_wrapper.ML	Fri Mar 19 15:33:18 2010 +0100
     1.3 @@ -6,48 +6,15 @@
     1.4  
     1.5  signature ATP_WRAPPER =
     1.6  sig
     1.7 -  (*hooks for problem files*)
     1.8 -  val destdir: string Config.T
     1.9 -  val problem_prefix: string Config.T
    1.10 -  val measure_runtime: bool Config.T
    1.11 -  val setup: theory -> theory
    1.12 +  type prover = ATP_Manager.prover
    1.13  
    1.14 -  (*prover configuration, problem format, and prover result*)
    1.15 -  type prover_config =
    1.16 -   {command: Path.T,
    1.17 -    arguments: int -> string,
    1.18 -    failure_strs: string list,
    1.19 -    max_new_clauses: int,
    1.20 -    insert_theory_const: bool,
    1.21 -    emit_structured_proof: bool}
    1.22 -  type problem =
    1.23 -   {with_full_types: bool,
    1.24 -    subgoal: int,
    1.25 -    goal: Proof.context * (thm list * thm),
    1.26 -    axiom_clauses: (thm * (string * int)) list option,
    1.27 -    filtered_clauses: (thm * (string * int)) list option}
    1.28 -  val problem_of_goal: bool -> int -> Proof.context * (thm list * thm) -> problem
    1.29 -  type prover_result =
    1.30 -   {success: bool,
    1.31 -    message: string,
    1.32 -    theorem_names: string list,
    1.33 -    runtime: int,
    1.34 -    proof: string,
    1.35 -    internal_thm_names: string Vector.vector,
    1.36 -    filtered_clauses: (thm * (string * int)) list}
    1.37 -  type prover = int -> problem -> prover_result
    1.38 +  (* hooks for problem files *)
    1.39 +  val destdir : string Config.T
    1.40 +  val problem_prefix : string Config.T
    1.41 +  val measure_runtime : bool Config.T
    1.42  
    1.43 -  (*common provers*)
    1.44 -  val vampire: string * prover
    1.45 -  val vampire_full: string * prover
    1.46 -  val eprover: string * prover
    1.47 -  val eprover_full: string * prover
    1.48 -  val spass: string * prover
    1.49 -  val spass_no_tc: string * prover
    1.50 -  val remote_vampire: string * prover
    1.51 -  val remote_eprover: string * prover
    1.52 -  val remote_spass: string * prover
    1.53 -  val refresh_systems: unit -> unit
    1.54 +  val refresh_systems_on_tptp : unit -> unit
    1.55 +  val setup : theory -> theory
    1.56  end;
    1.57  
    1.58  structure ATP_Wrapper : ATP_WRAPPER =
    1.59 @@ -56,6 +23,7 @@
    1.60  open Sledgehammer_HOL_Clause
    1.61  open Sledgehammer_Fact_Filter
    1.62  open Sledgehammer_Proof_Reconstruct
    1.63 +open ATP_Manager
    1.64  
    1.65  (** generic ATP wrapper **)
    1.66  
    1.67 @@ -70,10 +38,8 @@
    1.68  val (measure_runtime, measure_runtime_setup) =
    1.69    Attrib.config_bool "atp_measure_runtime" false;
    1.70  
    1.71 -val setup = destdir_setup #> problem_prefix_setup #> measure_runtime_setup;
    1.72  
    1.73 -
    1.74 -(* prover configuration, problem format, and prover result *)
    1.75 +(* prover configuration *)
    1.76  
    1.77  type prover_config =
    1.78   {command: Path.T,
    1.79 @@ -83,31 +49,6 @@
    1.80    insert_theory_const: bool,
    1.81    emit_structured_proof: bool};
    1.82  
    1.83 -type problem =
    1.84 - {with_full_types: bool,
    1.85 -  subgoal: int,
    1.86 -  goal: Proof.context * (thm list * thm),
    1.87 -  axiom_clauses: (thm * (string * int)) list option,
    1.88 -  filtered_clauses: (thm * (string * int)) list option};
    1.89 -
    1.90 -fun problem_of_goal with_full_types subgoal goal : problem =
    1.91 - {with_full_types = with_full_types,
    1.92 -  subgoal = subgoal,
    1.93 -  goal = goal,
    1.94 -  axiom_clauses = NONE,
    1.95 -  filtered_clauses = NONE};
    1.96 -
    1.97 -type prover_result =
    1.98 - {success: bool,
    1.99 -  message: string,
   1.100 -  theorem_names: string list,  (*relevant theorems*)
   1.101 -  runtime: int,  (*user time of the ATP, in milliseconds*)
   1.102 -  proof: string,
   1.103 -  internal_thm_names: string Vector.vector,
   1.104 -  filtered_clauses: (thm * (string * int)) list};
   1.105 -
   1.106 -type prover = int -> problem -> prover_result;
   1.107 -
   1.108  
   1.109  (* basic template *)
   1.110  
   1.111 @@ -316,7 +257,8 @@
   1.112      else split_lines answer
   1.113    end;
   1.114  
   1.115 -fun refresh_systems () = Synchronized.change systems (fn _ => get_systems ());
   1.116 +fun refresh_systems_on_tptp () =
   1.117 +  Synchronized.change systems (fn _ => get_systems ());
   1.118  
   1.119  fun get_system prefix = Synchronized.change_result systems (fn systems =>
   1.120    (if null systems then get_systems () else systems)
   1.121 @@ -347,4 +289,15 @@
   1.122  val remote_spass = tptp_prover ("remote_spass", remote_prover_config
   1.123    "SPASS---" "-x" spass_max_new_clauses spass_insert_theory_const);
   1.124  
   1.125 +val provers =
   1.126 +  [spass, vampire, eprover, vampire_full, eprover_full, spass_no_tc,
   1.127 +   remote_vampire, remote_spass, remote_eprover]
   1.128 +val prover_setup = fold add_prover provers
   1.129 +
   1.130 +val setup =
   1.131 +  destdir_setup
   1.132 +  #> problem_prefix_setup
   1.133 +  #> measure_runtime_setup
   1.134 +  #> prover_setup;
   1.135 +
   1.136  end;