# HG changeset patch # User blanchet # Date 1280245756 -7200 # Node ID badd89633f4ced1a718310521c8a31326e40d6fd # Parent e207a64e1e0bb96f31e279508444330c874e635f rename diff -r e207a64e1e0b -r badd89633f4c src/HOL/Tools/ATP_Manager/atp_manager.ML --- a/src/HOL/Tools/ATP_Manager/atp_manager.ML Tue Jul 27 17:43:11 2010 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,171 +0,0 @@ -(* Title: HOL/Tools/ATP_Manager/atp_manager.ML - Author: Fabian Immler, TU Muenchen - Author: Makarius - Author: Jasmin Blanchette, TU Muenchen - -Central manager component for ATP threads. -*) - -signature ATP_MANAGER = -sig - type relevance_override = Sledgehammer_Fact_Filter.relevance_override - type minimize_command = Sledgehammer_Proof_Reconstruct.minimize_command - type params = - {debug: bool, - verbose: bool, - overlord: bool, - atps: string list, - full_types: bool, - explicit_apply: bool, - relevance_threshold: real, - relevance_convergence: real, - theory_relevant: bool option, - defs_relevant: bool, - isar_proof: bool, - isar_shrink_factor: int, - timeout: Time.time, - minimize_timeout: Time.time} - type problem = - {subgoal: int, - goal: Proof.context * (thm list * thm), - relevance_override: relevance_override, - axiom_clauses: (string * thm) list option, - filtered_clauses: (string * thm) list option} - datatype failure = - Unprovable | IncompleteUnprovable | CantConnect | TimedOut | - OutOfResources | OldSpass | MalformedInput | MalformedOutput | UnknownError - type prover_result = - {outcome: failure option, - message: string, - pool: string Symtab.table, - used_thm_names: string list, - atp_run_time_in_msecs: int, - output: string, - proof: string, - internal_thm_names: string Vector.vector, - conjecture_shape: int list, - filtered_clauses: (string * thm) list} - type prover = - params -> minimize_command -> Time.time -> problem -> prover_result - - val kill_atps: unit -> unit - val running_atps: unit -> unit - val messages: int option -> unit - val add_prover: string * prover -> theory -> theory - val get_prover: theory -> string -> prover - val available_atps: theory -> unit - val start_prover_thread : - params -> int -> int -> relevance_override -> (string -> minimize_command) - -> Proof.state -> string -> unit -end; - -structure ATP_Manager : ATP_MANAGER = -struct - -open Metis_Clauses -open Sledgehammer_Fact_Filter -open Sledgehammer_Proof_Reconstruct - -(** The Sledgehammer **) - -val das_Tool = "Sledgehammer" - -fun kill_atps () = Async_Manager.kill_threads das_Tool "ATPs" -fun running_atps () = Async_Manager.running_threads das_Tool "ATPs" -val messages = Async_Manager.thread_messages das_Tool "ATP" - -(** problems, results, provers, etc. **) - -type params = - {debug: bool, - verbose: bool, - overlord: bool, - atps: string list, - full_types: bool, - explicit_apply: bool, - relevance_threshold: real, - relevance_convergence: real, - theory_relevant: bool option, - defs_relevant: bool, - isar_proof: bool, - isar_shrink_factor: int, - timeout: Time.time, - minimize_timeout: Time.time} - -type problem = - {subgoal: int, - goal: Proof.context * (thm list * thm), - relevance_override: relevance_override, - axiom_clauses: (string * thm) list option, - filtered_clauses: (string * thm) list option} - -datatype failure = - Unprovable | IncompleteUnprovable | CantConnect | TimedOut | OutOfResources | - OldSpass | MalformedInput | MalformedOutput | UnknownError - -type prover_result = - {outcome: failure option, - message: string, - pool: string Symtab.table, - used_thm_names: string list, - atp_run_time_in_msecs: int, - output: string, - proof: string, - internal_thm_names: string Vector.vector, - conjecture_shape: int list, - filtered_clauses: (string * thm) list} - -type prover = - params -> minimize_command -> Time.time -> problem -> prover_result - -(* named provers *) - -structure Data = Theory_Data -( - type T = (prover * stamp) Symtab.table; - val empty = Symtab.empty; - val extend = I; - fun merge data : T = Symtab.merge (eq_snd op =) data - handle Symtab.DUP name => error ("Duplicate ATP: " ^ quote name ^ ".") -); - -fun add_prover (name, prover) thy = - Data.map (Symtab.update_new (name, (prover, stamp ()))) thy - handle Symtab.DUP name => error ("Duplicate ATP: " ^ quote name ^ ".") - -fun get_prover thy name = - the (Symtab.lookup (Data.get thy) name) |> fst - handle Option.Option => error ("Unknown ATP: " ^ name ^ ".") - -fun available_atps thy = - priority ("Available ATPs: " ^ - commas (sort_strings (Symtab.keys (Data.get thy))) ^ ".") - - -(* start prover thread *) - -fun start_prover_thread (params as {verbose, full_types, timeout, ...}) i n - relevance_override minimize_command proof_state name = - let - val birth_time = Time.now () - val death_time = Time.+ (birth_time, timeout) - val prover = get_prover (Proof.theory_of proof_state) name - val {context = ctxt, facts, goal} = Proof.goal proof_state; - val desc = - "ATP " ^ quote name ^ " for subgoal " ^ string_of_int i ^ ":\n" ^ - Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i)); - in - Async_Manager.launch das_Tool verbose birth_time death_time desc - (fn () => - let - val problem = - {subgoal = i, goal = (ctxt, (facts, goal)), - relevance_override = relevance_override, axiom_clauses = NONE, - filtered_clauses = NONE} - in - prover params (minimize_command name) timeout problem |> #message - handle ERROR message => "Error: " ^ message ^ "\n" - end) - end - -end; diff -r e207a64e1e0b -r badd89633f4c src/HOL/Tools/Sledgehammer/sledgehammer.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Tue Jul 27 17:49:16 2010 +0200 @@ -0,0 +1,171 @@ +(* Title: HOL/Tools/ATP_Manager/atp_manager.ML + Author: Fabian Immler, TU Muenchen + Author: Makarius + Author: Jasmin Blanchette, TU Muenchen + +Central manager component for ATP threads. +*) + +signature ATP_MANAGER = +sig + type relevance_override = Sledgehammer_Fact_Filter.relevance_override + type minimize_command = Sledgehammer_Proof_Reconstruct.minimize_command + type params = + {debug: bool, + verbose: bool, + overlord: bool, + atps: string list, + full_types: bool, + explicit_apply: bool, + relevance_threshold: real, + relevance_convergence: real, + theory_relevant: bool option, + defs_relevant: bool, + isar_proof: bool, + isar_shrink_factor: int, + timeout: Time.time, + minimize_timeout: Time.time} + type problem = + {subgoal: int, + goal: Proof.context * (thm list * thm), + relevance_override: relevance_override, + axiom_clauses: (string * thm) list option, + filtered_clauses: (string * thm) list option} + datatype failure = + Unprovable | IncompleteUnprovable | CantConnect | TimedOut | + OutOfResources | OldSpass | MalformedInput | MalformedOutput | UnknownError + type prover_result = + {outcome: failure option, + message: string, + pool: string Symtab.table, + used_thm_names: string list, + atp_run_time_in_msecs: int, + output: string, + proof: string, + internal_thm_names: string Vector.vector, + conjecture_shape: int list, + filtered_clauses: (string * thm) list} + type prover = + params -> minimize_command -> Time.time -> problem -> prover_result + + val kill_atps: unit -> unit + val running_atps: unit -> unit + val messages: int option -> unit + val add_prover: string * prover -> theory -> theory + val get_prover: theory -> string -> prover + val available_atps: theory -> unit + val start_prover_thread : + params -> int -> int -> relevance_override -> (string -> minimize_command) + -> Proof.state -> string -> unit +end; + +structure ATP_Manager : ATP_MANAGER = +struct + +open Metis_Clauses +open Sledgehammer_Fact_Filter +open Sledgehammer_Proof_Reconstruct + +(** The Sledgehammer **) + +val das_Tool = "Sledgehammer" + +fun kill_atps () = Async_Manager.kill_threads das_Tool "ATPs" +fun running_atps () = Async_Manager.running_threads das_Tool "ATPs" +val messages = Async_Manager.thread_messages das_Tool "ATP" + +(** problems, results, provers, etc. **) + +type params = + {debug: bool, + verbose: bool, + overlord: bool, + atps: string list, + full_types: bool, + explicit_apply: bool, + relevance_threshold: real, + relevance_convergence: real, + theory_relevant: bool option, + defs_relevant: bool, + isar_proof: bool, + isar_shrink_factor: int, + timeout: Time.time, + minimize_timeout: Time.time} + +type problem = + {subgoal: int, + goal: Proof.context * (thm list * thm), + relevance_override: relevance_override, + axiom_clauses: (string * thm) list option, + filtered_clauses: (string * thm) list option} + +datatype failure = + Unprovable | IncompleteUnprovable | CantConnect | TimedOut | OutOfResources | + OldSpass | MalformedInput | MalformedOutput | UnknownError + +type prover_result = + {outcome: failure option, + message: string, + pool: string Symtab.table, + used_thm_names: string list, + atp_run_time_in_msecs: int, + output: string, + proof: string, + internal_thm_names: string Vector.vector, + conjecture_shape: int list, + filtered_clauses: (string * thm) list} + +type prover = + params -> minimize_command -> Time.time -> problem -> prover_result + +(* named provers *) + +structure Data = Theory_Data +( + type T = (prover * stamp) Symtab.table; + val empty = Symtab.empty; + val extend = I; + fun merge data : T = Symtab.merge (eq_snd op =) data + handle Symtab.DUP name => error ("Duplicate ATP: " ^ quote name ^ ".") +); + +fun add_prover (name, prover) thy = + Data.map (Symtab.update_new (name, (prover, stamp ()))) thy + handle Symtab.DUP name => error ("Duplicate ATP: " ^ quote name ^ ".") + +fun get_prover thy name = + the (Symtab.lookup (Data.get thy) name) |> fst + handle Option.Option => error ("Unknown ATP: " ^ name ^ ".") + +fun available_atps thy = + priority ("Available ATPs: " ^ + commas (sort_strings (Symtab.keys (Data.get thy))) ^ ".") + + +(* start prover thread *) + +fun start_prover_thread (params as {verbose, full_types, timeout, ...}) i n + relevance_override minimize_command proof_state name = + let + val birth_time = Time.now () + val death_time = Time.+ (birth_time, timeout) + val prover = get_prover (Proof.theory_of proof_state) name + val {context = ctxt, facts, goal} = Proof.goal proof_state; + val desc = + "ATP " ^ quote name ^ " for subgoal " ^ string_of_int i ^ ":\n" ^ + Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i)); + in + Async_Manager.launch das_Tool verbose birth_time death_time desc + (fn () => + let + val problem = + {subgoal = i, goal = (ctxt, (facts, goal)), + relevance_override = relevance_override, axiom_clauses = NONE, + filtered_clauses = NONE} + in + prover params (minimize_command name) timeout problem |> #message + handle ERROR message => "Error: " ^ message ^ "\n" + end) + end + +end;