# HG changeset patch # User blanchet # Date 1280336494 -7200 # Node ID 6659c15e742104a4a02a35c24c2294cfa3ca2a48 # Parent f367847f5068bb3f52e29e7d13bc0a76ff59c50e rename directory diff -r f367847f5068 -r 6659c15e7421 src/HOL/Tools/ATP/async_manager.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/ATP/async_manager.ML Wed Jul 28 19:01:34 2010 +0200 @@ -0,0 +1,241 @@ +(* Title: HOL/Tools/ATP_Manager/async_manager.ML + Author: Fabian Immler, TU Muenchen + Author: Makarius + Author: Jasmin Blanchette, TU Muenchen + +Central manager for asynchronous diagnosis tool threads. +*) + +signature ASYNC_MANAGER = +sig + val launch : + string -> bool -> Time.time -> Time.time -> string -> (unit -> string) + -> unit + val kill_threads : string -> string -> unit + val running_threads : string -> string -> unit + val thread_messages : string -> string -> int option -> unit +end; + +structure Async_Manager : ASYNC_MANAGER = +struct + +(** preferences **) + +val message_store_limit = 20; +val message_display_limit = 5; + + +(** thread management **) + +(* data structures over threads *) + +structure Thread_Heap = Heap +( + type elem = Time.time * Thread.thread; + fun ord ((a, _), (b, _)) = Time.compare (a, b); +); + +fun lookup_thread xs = AList.lookup Thread.equal xs; +fun delete_thread xs = AList.delete Thread.equal xs; +fun update_thread xs = AList.update Thread.equal xs; + + +(* state of thread manager *) + +type state = + {manager: Thread.thread option, + timeout_heap: Thread_Heap.T, + active: (Thread.thread * (string * Time.time * Time.time * string)) list, + canceling: (Thread.thread * (string * Time.time * string)) list, + messages: (string * string) list, + store: (string * string) list} + +fun make_state manager timeout_heap active canceling messages store : state = + {manager = manager, timeout_heap = timeout_heap, active = active, + canceling = canceling, messages = messages, store = store} + +val global_state = Synchronized.var "async_manager" + (make_state NONE Thread_Heap.empty [] [] [] []); + + +(* unregister thread *) + +fun unregister verbose message thread = + Synchronized.change global_state + (fn state as {manager, timeout_heap, active, canceling, messages, store} => + (case lookup_thread active thread of + SOME (tool, birth_time, _, desc) => + let + val active' = delete_thread thread active; + val now = Time.now () + val canceling' = (thread, (tool, now, desc)) :: canceling + val message' = + desc ^ "\n" ^ message ^ + (if verbose then + "Total time: " ^ Int.toString (Time.toMilliseconds + (Time.- (now, birth_time))) ^ " ms.\n" + else + "") + val messages' = (tool, message') :: messages; + val store' = (tool, message') :: + (if length store <= message_store_limit then store + else #1 (chop message_store_limit store)); + in make_state manager timeout_heap active' canceling' messages' store' end + | NONE => state)); + + +(* main manager thread -- only one may exist *) + +val min_wait_time = Time.fromMilliseconds 300; +val max_wait_time = Time.fromSeconds 10; + +fun replace_all bef aft = + let + fun aux seen "" = String.implode (rev seen) + | aux seen s = + if String.isPrefix bef s then + aux seen "" ^ aft ^ aux [] (unprefix bef s) + else + aux (String.sub (s, 0) :: seen) (String.extract (s, 1, NONE)) + in aux [] end + +(* This is a workaround for Proof General's off-by-a-few sendback display bug, + whereby "pr" in "proof" is not highlighted. *) +fun break_into_chunks xs = + maps (space_explode "\000" o replace_all "\n\n" "\000" o snd) xs + +fun print_new_messages () = + case Synchronized.change_result global_state + (fn {manager, timeout_heap, active, canceling, messages, store} => + (messages, make_state manager timeout_heap active canceling [] + store)) of + [] => () + | msgs as (tool, _) :: _ => + let val ss = break_into_chunks msgs in + List.app priority (tool ^ ": " ^ hd ss :: tl ss) + end + +fun check_thread_manager verbose = Synchronized.change global_state + (fn state as {manager, timeout_heap, active, canceling, messages, store} => + if (case manager of SOME thread => Thread.isActive thread | NONE => false) then state + else let val manager = SOME (Toplevel.thread false (fn () => + let + fun time_limit timeout_heap = + (case try Thread_Heap.min timeout_heap of + NONE => Time.+ (Time.now (), max_wait_time) + | SOME (time, _) => time); + + (*action: find threads whose timeout is reached, and interrupt canceling threads*) + fun action {manager, timeout_heap, active, canceling, messages, store} = + let val (timeout_threads, timeout_heap') = + Thread_Heap.upto (Time.now (), Thread.self ()) timeout_heap; + in + if null timeout_threads andalso null canceling then + NONE + else + let + val _ = List.app (Simple_Thread.interrupt o #1) canceling + val canceling' = filter (Thread.isActive o #1) canceling + val state' = make_state manager timeout_heap' active canceling' messages store; + in SOME (map #2 timeout_threads, state') end + end; + in + while Synchronized.change_result global_state + (fn state as {timeout_heap, active, canceling, messages, store, ...} => + if null active andalso null canceling andalso null messages + then (false, make_state NONE timeout_heap active canceling messages store) + else (true, state)) + do + (Synchronized.timed_access global_state (SOME o time_limit o #timeout_heap) action + |> these + |> List.app (unregister verbose "Timed out.\n"); + print_new_messages (); + (*give threads some time to respond to interrupt*) + OS.Process.sleep min_wait_time) + end)) + in make_state manager timeout_heap active canceling messages store end) + + +(* register thread *) + +fun register tool verbose birth_time death_time desc thread = + (Synchronized.change global_state + (fn {manager, timeout_heap, active, canceling, messages, store} => + let + val timeout_heap' = Thread_Heap.insert (death_time, thread) timeout_heap; + val active' = update_thread (thread, (tool, birth_time, death_time, desc)) active; + val state' = make_state manager timeout_heap' active' canceling messages store; + in state' end); + check_thread_manager verbose); + + +fun launch tool verbose birth_time death_time desc f = + (Toplevel.thread true + (fn () => + let + val self = Thread.self () + val _ = register tool verbose birth_time death_time desc self + val message = f () + in unregister verbose message self end); + ()) + + +(** user commands **) + +(* kill threads *) + +fun kill_threads tool workers = Synchronized.change global_state + (fn {manager, timeout_heap, active, canceling, messages, store} => + let + val killing = + map_filter (fn (th, (tool', _, _, desc)) => + if tool' = tool then SOME (th, (tool', Time.now (), desc)) + else NONE) active + val state' = make_state manager timeout_heap [] (killing @ canceling) messages store; + val _ = if null killing then () else priority ("Killed active " ^ workers ^ ".") + in state' end); + + +(* running threads *) + +fun seconds time = string_of_int (Time.toSeconds time) ^ " s" + +fun running_threads tool workers = + let + val {active, canceling, ...} = Synchronized.value global_state; + + val now = Time.now (); + fun running_info (_, (tool', birth_time, death_time, desc)) = + if tool' = tool then + SOME ("Running: " ^ seconds (Time.- (now, birth_time)) ^ " -- " ^ + seconds (Time.- (death_time, now)) ^ " to live:\n" ^ desc) + else + NONE + fun canceling_info (_, (tool', death_time, desc)) = + if tool' = tool then + SOME ("Trying to interrupt thread since " ^ + seconds (Time.- (now, death_time)) ^ ":\n" ^ desc) + else + NONE + val running = + case map_filter running_info active of + [] => ["No " ^ workers ^ " running."] + | ss => "Running " ^ workers ^ ":" :: ss + val interrupting = + case map_filter canceling_info canceling of + [] => [] + | ss => "Trying to interrupt the following " ^ workers ^ ":" :: ss + in priority (space_implode "\n\n" (running @ interrupting)) end + +fun thread_messages tool worker opt_limit = + let + val limit = the_default message_display_limit opt_limit; + val tool_store = Synchronized.value global_state + |> #store |> filter (curry (op =) tool o fst) + val header = + "Recent " ^ worker ^ " messages" ^ + (if length tool_store <= limit then ":" + else " (" ^ string_of_int limit ^ " displayed):"); + in List.app priority (header :: break_into_chunks (#1 (chop limit tool_store))) end + +end; diff -r f367847f5068 -r 6659c15e7421 src/HOL/Tools/ATP/atp_problem.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/ATP/atp_problem.ML Wed Jul 28 19:01:34 2010 +0200 @@ -0,0 +1,152 @@ +(* Title: HOL/Tools/ATP_Manager/atp_problem.ML + Author: Jia Meng, Cambridge University Computer Laboratory and NICTA + Author: Jasmin Blanchette, TU Muenchen + +TPTP syntax. +*) + +signature ATP_PROBLEM = +sig + datatype 'a fo_term = ATerm of 'a * 'a fo_term list + datatype quantifier = AForall | AExists + datatype connective = ANot | AAnd | AOr | AImplies | AIf | AIff | ANotIff + datatype ('a, 'b) formula = + AQuant of quantifier * 'a list * ('a, 'b) formula | + AConn of connective * ('a, 'b) formula list | + AAtom of 'b + + datatype kind = Axiom | Conjecture + datatype 'a problem_line = Fof of string * kind * ('a, 'a fo_term) formula + type 'a problem = (string * 'a problem_line list) list + + val timestamp : unit -> string + val is_tptp_variable : string -> bool + val strings_for_tptp_problem : + (string * string problem_line list) list -> string list + val nice_tptp_problem : + bool -> ('a * (string * string) problem_line list) list + -> ('a * string problem_line list) list + * (string Symtab.table * string Symtab.table) option +end; + +structure ATP_Problem : ATP_PROBLEM = +struct + +(** ATP problem **) + +datatype 'a fo_term = ATerm of 'a * 'a fo_term list +datatype quantifier = AForall | AExists +datatype connective = ANot | AAnd | AOr | AImplies | AIf | AIff | ANotIff +datatype ('a, 'b) formula = + AQuant of quantifier * 'a list * ('a, 'b) formula | + AConn of connective * ('a, 'b) formula list | + AAtom of 'b + +datatype kind = Axiom | Conjecture +datatype 'a problem_line = Fof of string * kind * ('a, 'a fo_term) formula +type 'a problem = (string * 'a problem_line list) list + +val timestamp = Date.fmt "%Y-%m-%d %H:%M:%S" o Date.fromTimeLocal o Time.now + +fun string_for_term (ATerm (s, [])) = s + | string_for_term (ATerm (s, ts)) = + if s = "equal" then space_implode " = " (map string_for_term ts) + else s ^ "(" ^ commas (map string_for_term ts) ^ ")" +fun string_for_quantifier AForall = "!" + | string_for_quantifier AExists = "?" +fun string_for_connective ANot = "~" + | string_for_connective AAnd = "&" + | string_for_connective AOr = "|" + | string_for_connective AImplies = "=>" + | string_for_connective AIf = "<=" + | string_for_connective AIff = "<=>" + | string_for_connective ANotIff = "<~>" +fun string_for_formula (AQuant (q, xs, phi)) = + string_for_quantifier q ^ "[" ^ commas xs ^ "] : " ^ + string_for_formula phi + | string_for_formula (AConn (ANot, [AAtom (ATerm ("equal", ts))])) = + space_implode " != " (map string_for_term ts) + | string_for_formula (AConn (c, [phi])) = + string_for_connective c ^ " " ^ string_for_formula phi + | string_for_formula (AConn (c, phis)) = + "(" ^ space_implode (" " ^ string_for_connective c ^ " ") + (map string_for_formula phis) ^ ")" + | string_for_formula (AAtom tm) = string_for_term tm + +fun string_for_problem_line (Fof (ident, kind, phi)) = + "fof(" ^ ident ^ ", " ^ + (case kind of Axiom => "axiom" | Conjecture => "conjecture") ^ ",\n" ^ + " (" ^ string_for_formula phi ^ ")).\n" +fun strings_for_tptp_problem problem = + "% This file was generated by Isabelle (most likely Sledgehammer)\n\ + \% " ^ timestamp () ^ "\n" :: + maps (fn (_, []) => [] + | (heading, lines) => + "\n% " ^ heading ^ " (" ^ Int.toString (length lines) ^ ")\n" :: + map string_for_problem_line lines) problem + +fun is_tptp_variable s = Char.isUpper (String.sub (s, 0)) + + +(** Nice names **) + +fun empty_name_pool readable_names = + if readable_names then SOME (Symtab.empty, Symtab.empty) else NONE + +fun pool_fold f xs z = pair z #> fold_rev (fn x => uncurry (f x)) xs +fun pool_map f xs = + pool_fold (fn x => fn ys => fn pool => f x pool |>> (fn y => y :: ys)) xs [] + +(* "equal" is reserved by some ATPs. "op" is also reserved, to avoid the + unreadable "op_1", "op_2", etc., in the problem files. *) +val reserved_nice_names = ["equal", "op"] +fun readable_name full_name s = + if s = full_name then + s + else + let + val s = s |> Long_Name.base_name + |> Name.desymbolize (Char.isUpper (String.sub (full_name, 0))) + in if member (op =) reserved_nice_names s then full_name else s end + +fun nice_name (full_name, _) NONE = (full_name, NONE) + | nice_name (full_name, desired_name) (SOME the_pool) = + case Symtab.lookup (fst the_pool) full_name of + SOME nice_name => (nice_name, SOME the_pool) + | NONE => + let + val nice_prefix = readable_name full_name desired_name + fun add j = + let + val nice_name = nice_prefix ^ + (if j = 0 then "" else "_" ^ Int.toString j) + in + case Symtab.lookup (snd the_pool) nice_name of + SOME full_name' => + if full_name = full_name' then (nice_name, the_pool) + else add (j + 1) + | NONE => + (nice_name, + (Symtab.update_new (full_name, nice_name) (fst the_pool), + Symtab.update_new (nice_name, full_name) (snd the_pool))) + end + in add 0 |> apsnd SOME end + + +fun nice_term (ATerm (name, ts)) = + nice_name name ##>> pool_map nice_term ts #>> ATerm +fun nice_formula (AQuant (q, xs, phi)) = + pool_map nice_name xs ##>> nice_formula phi + #>> (fn (xs, phi) => AQuant (q, xs, phi)) + | nice_formula (AConn (c, phis)) = + pool_map nice_formula phis #>> curry AConn c + | nice_formula (AAtom tm) = nice_term tm #>> AAtom +fun nice_problem_line (Fof (ident, kind, phi)) = + nice_formula phi #>> (fn phi => Fof (ident, kind, phi)) +fun nice_problem problem = + pool_map (fn (heading, lines) => + pool_map nice_problem_line lines #>> pair heading) problem +fun nice_tptp_problem readable_names problem = + nice_problem problem (empty_name_pool readable_names) + +end; diff -r f367847f5068 -r 6659c15e7421 src/HOL/Tools/ATP/atp_systems.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/ATP/atp_systems.ML Wed Jul 28 19:01:34 2010 +0200 @@ -0,0 +1,219 @@ +(* Title: HOL/Tools/ATP_Manager/atp_systems.ML + Author: Fabian Immler, TU Muenchen + Author: Jasmin Blanchette, TU Muenchen + +Setup for supported ATPs. +*) + +signature ATP_SYSTEMS = +sig + datatype failure = + Unprovable | IncompleteUnprovable | CantConnect | TimedOut | + OutOfResources | OldSpass | MalformedInput | MalformedOutput | UnknownError + + type prover_config = + {executable: string * string, + required_executables: (string * string) list, + arguments: bool -> Time.time -> string, + proof_delims: (string * string) list, + known_failures: (failure * string) list, + max_new_relevant_facts_per_iter: int, + prefers_theory_relevant: bool, + explicit_forall: bool} + + val add_prover: string * prover_config -> theory -> theory + val get_prover: theory -> string -> prover_config + val available_atps: theory -> unit + val refresh_systems_on_tptp : unit -> unit + val default_atps_param_value : unit -> string + val setup : theory -> theory +end; + +structure ATP_Systems : ATP_SYSTEMS = +struct + +(* prover configuration *) + +datatype failure = + Unprovable | IncompleteUnprovable | CantConnect | TimedOut | OutOfResources | + OldSpass | MalformedInput | MalformedOutput | UnknownError + +type prover_config = + {executable: string * string, + required_executables: (string * string) list, + arguments: bool -> Time.time -> string, + proof_delims: (string * string) list, + known_failures: (failure * string) list, + max_new_relevant_facts_per_iter: int, + prefers_theory_relevant: bool, + explicit_forall: bool} + + +(* named provers *) + +structure Data = Theory_Data +( + type T = (prover_config * 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, config) thy = + Data.map (Symtab.update_new (name, (config, 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))) ^ ".") + +fun available_atps thy = + priority ("Available ATPs: " ^ + commas (sort_strings (Symtab.keys (Data.get thy))) ^ ".") + +fun to_generous_secs time = (Time.toMilliseconds time + 999) div 1000 + +(* E prover *) + +val tstp_proof_delims = + ("# SZS output start CNFRefutation.", "# SZS output end CNFRefutation") + +val e_config : prover_config = + {executable = ("E_HOME", "eproof"), + required_executables = [], + arguments = fn _ => fn timeout => + "--tstp-in --tstp-out -l5 -xAutoDev -tAutoDev --silent --cpu-limit=" ^ + string_of_int (to_generous_secs timeout), + proof_delims = [tstp_proof_delims], + known_failures = + [(Unprovable, "SZS status: CounterSatisfiable"), + (Unprovable, "SZS status CounterSatisfiable"), + (TimedOut, "Failure: Resource limit exceeded (time)"), + (TimedOut, "time limit exceeded"), + (OutOfResources, + "# Cannot determine problem status within resource limit"), + (OutOfResources, "SZS status: ResourceOut"), + (OutOfResources, "SZS status ResourceOut")], + max_new_relevant_facts_per_iter = 80 (* FIXME *), + prefers_theory_relevant = false, + explicit_forall = false} +val e = ("e", e_config) + + +(* The "-VarWeight=3" option helps the higher-order problems, probably by + counteracting the presence of "hAPP". *) +val spass_config : prover_config = + {executable = ("ISABELLE_ATP_MANAGER", "scripts/spass"), + required_executables = [("SPASS_HOME", "SPASS")], + (* "div 2" accounts for the fact that SPASS is often run twice. *) + arguments = fn complete => fn timeout => + ("-Auto -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof \ + \-VarWeight=3 -TimeLimit=" ^ + string_of_int (to_generous_secs timeout div 2)) + |> not complete ? prefix "-SOS=1 ", + proof_delims = [("Here is a proof", "Formulae used in the proof")], + known_failures = + [(IncompleteUnprovable, "SPASS beiseite: Completion found"), + (TimedOut, "SPASS beiseite: Ran out of time"), + (OutOfResources, "SPASS beiseite: Maximal number of loops exceeded"), + (MalformedInput, "Undefined symbol"), + (MalformedInput, "Free Variable"), + (OldSpass, "tptp2dfg")], + max_new_relevant_facts_per_iter = 26 (* FIXME *), + prefers_theory_relevant = true, + explicit_forall = true} +val spass = ("spass", spass_config) + +(* Vampire *) + +val vampire_config : prover_config = + {executable = ("VAMPIRE_HOME", "vampire"), + required_executables = [], + arguments = fn _ => fn timeout => + "--mode casc -t " ^ string_of_int (to_generous_secs timeout) ^ + " --input_file ", + proof_delims = + [("=========== Refutation ==========", + "======= End of refutation ======="), + ("% SZS output start Refutation", "% SZS output end Refutation"), + ("% SZS output start Proof", "% SZS output end Proof")], + known_failures = + [(Unprovable, "UNPROVABLE"), + (IncompleteUnprovable, "CANNOT PROVE"), + (Unprovable, "Satisfiability detected"), + (OutOfResources, "Refutation not found")], + max_new_relevant_facts_per_iter = 40 (* FIXME *), + prefers_theory_relevant = false, + explicit_forall = false} +val vampire = ("vampire", vampire_config) + +(* Remote prover invocation via SystemOnTPTP *) + +val systems = Synchronized.var "atp_systems" ([]: string list) + +fun get_systems () = + case bash_output "\"$ISABELLE_ATP_MANAGER/scripts/remote_atp\" -w" of + (answer, 0) => split_lines answer + | (answer, _) => + error ("Failed to get available systems at SystemOnTPTP:\n" ^ + perhaps (try (unsuffix "\n")) answer) + +fun refresh_systems_on_tptp () = + Synchronized.change systems (fn _ => get_systems ()) + +fun get_system prefix = Synchronized.change_result systems (fn systems => + (if null systems then get_systems () else systems) + |> `(find_first (String.isPrefix prefix))); + +fun the_system prefix = + (case get_system prefix of + NONE => error ("System " ^ quote prefix ^ " not available at SystemOnTPTP.") + | SOME sys => sys); + +val remote_known_failures = + [(CantConnect, "HTTP-Error"), + (TimedOut, "says Timeout"), + (MalformedOutput, "Remote script could not extract proof")] + +fun remote_config atp_prefix + ({proof_delims, known_failures, max_new_relevant_facts_per_iter, + prefers_theory_relevant, explicit_forall, ...} : prover_config) + : prover_config = + {executable = ("ISABELLE_ATP_MANAGER", "scripts/remote_atp"), + required_executables = [], + arguments = fn _ => fn timeout => + " -t " ^ string_of_int (to_generous_secs timeout) ^ " -s " ^ + the_system atp_prefix, + proof_delims = insert (op =) tstp_proof_delims proof_delims, + known_failures = remote_known_failures @ known_failures, + max_new_relevant_facts_per_iter = max_new_relevant_facts_per_iter, + prefers_theory_relevant = prefers_theory_relevant, + explicit_forall = explicit_forall} + +val remote_name = prefix "remote_" + +fun remote_prover (name, config) atp_prefix = + (remote_name name, remote_config atp_prefix config) + +val remote_e = remote_prover e "EP---" +val remote_vampire = remote_prover vampire "Vampire---9" + +fun is_installed ({executable, required_executables, ...} : prover_config) = + forall (curry (op <>) "" o getenv o fst) (executable :: required_executables) +fun maybe_remote (name, config) = + name |> not (is_installed config) ? remote_name + +fun default_atps_param_value () = + space_implode " " ([maybe_remote e] @ + (if is_installed (snd spass) then [fst spass] else []) @ + [remote_name (fst vampire)]) + +val provers = [e, spass, vampire, remote_e, remote_vampire] +val setup = fold add_prover provers + +end; diff -r f367847f5068 -r 6659c15e7421 src/HOL/Tools/ATP/etc/settings --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/ATP/etc/settings Wed Jul 28 19:01:34 2010 +0200 @@ -0,0 +1,2 @@ +ISABELLE_ATP_MANAGER="$COMPONENT" + diff -r f367847f5068 -r 6659c15e7421 src/HOL/Tools/ATP/scripts/remote_atp --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/ATP/scripts/remote_atp Wed Jul 28 19:01:34 2010 +0200 @@ -0,0 +1,109 @@ +#!/usr/bin/env perl +# +# Wrapper for custom remote provers on SystemOnTPTP +# Author: Fabian Immler, TU Muenchen +# + +use warnings; +use strict; +use Getopt::Std; +use HTTP::Request::Common; +use LWP; + +my $SystemOnTPTPFormReplyURL = + "http://www.cs.miami.edu/~tptp/cgi-bin/SystemOnTPTPFormReply"; + +# default parameters +my %URLParameters = ( + "NoHTML" => 1, + "QuietFlag" => "-q01", + "SubmitButton" => "RunSelectedSystems", + "ProblemSource" => "UPLOAD", + "ForceSystem" => "-force", + ); + +#----Get format and transform options if specified +my %Options; +getopts("hws:t:c:",\%Options); + +#----Usage +sub usage() { + print("Usage: remote_atp [] \n"); + print(" are ...\n"); + print(" -h - print this help\n"); + print(" -w - list available ATP systems\n"); + print(" -s - specified system to use\n"); + print(" -t - CPU time limit for system\n"); + print(" -c - custom command for system\n"); + print(" - TPTP problem file\n"); + exit(0); +} +if (exists($Options{'h'})) { + usage(); +} + +#----What systems flag +if (exists($Options{'w'})) { + $URLParameters{"SubmitButton"} = "ListSystems"; + delete($URLParameters{"ProblemSource"}); +} + +#----X2TPTP +if (exists($Options{'x'})) { + $URLParameters{"X2TPTP"} = "-S"; +} + +#----Selected system +my $System; +if (exists($Options{'s'})) { + $System = $Options{'s'}; +} else { + # use Vampire as default + $System = "Vampire---9.0"; +} +$URLParameters{"System___$System"} = $System; + +#----Time limit +if (exists($Options{'t'})) { + $URLParameters{"TimeLimit___$System"} = $Options{'t'}; +} +#----Custom command +if (exists($Options{'c'})) { + $URLParameters{"Command___$System"} = $Options{'c'}; +} + +#----Get single file name +if (exists($URLParameters{"ProblemSource"})) { + if (scalar(@ARGV) >= 1) { + $URLParameters{"UPLOADProblem"} = [shift(@ARGV)]; + } else { + print("Missing problem file\n"); + usage(); + die; + } +} + +# Query Server +my $Agent = LWP::UserAgent->new; +if (exists($Options{'t'})) { + # give server more time to respond + $Agent->timeout($Options{'t'} + 10); +} +my $Request = POST($SystemOnTPTPFormReplyURL, + Content_Type => 'form-data',Content => \%URLParameters); +my $Response = $Agent->request($Request); + +#catch errors / failure +if(!$Response->is_success) { + print "HTTP-Error: " . $Response->message . "\n"; + exit(-1); +} elsif (exists($Options{'w'})) { + print $Response->content; + exit (0); +} elsif ($Response->content =~ /WARNING: (\S*) does not exist/) { + print "Specified System $1 does not exist\n"; + exit(-1); +} else { + print $Response->content; + exit(0); +} diff -r f367847f5068 -r 6659c15e7421 src/HOL/Tools/ATP/scripts/spass --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/ATP/scripts/spass Wed Jul 28 19:01:34 2010 +0200 @@ -0,0 +1,19 @@ +#!/usr/bin/env bash +# +# Wrapper for SPASS that also outputs the Flotter-generated CNF (needed for +# Isar proof reconstruction) +# +# Author: Jasmin Blanchette, TU Muenchen + +options=${@:1:$(($#-1))} +name=${@:$(($#)):1} + +$SPASS_HOME/tptp2dfg $name $name.fof.dfg +$SPASS_HOME/SPASS -Flotter $name.fof.dfg \ + | sed 's/description({$/description({*/' \ + > $name.cnf.dfg +rm -f $name.fof.dfg +cat $name.cnf.dfg +$SPASS_HOME/SPASS $options $name.cnf.dfg \ + | sed 's/\(Formulae used in the proof :\).*/\1 N\/A/' +rm -f $name.cnf.dfg diff -r f367847f5068 -r 6659c15e7421 src/HOL/Tools/ATP_Manager/async_manager.ML --- a/src/HOL/Tools/ATP_Manager/async_manager.ML Wed Jul 28 19:01:07 2010 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,241 +0,0 @@ -(* Title: HOL/Tools/ATP_Manager/async_manager.ML - Author: Fabian Immler, TU Muenchen - Author: Makarius - Author: Jasmin Blanchette, TU Muenchen - -Central manager for asynchronous diagnosis tool threads. -*) - -signature ASYNC_MANAGER = -sig - val launch : - string -> bool -> Time.time -> Time.time -> string -> (unit -> string) - -> unit - val kill_threads : string -> string -> unit - val running_threads : string -> string -> unit - val thread_messages : string -> string -> int option -> unit -end; - -structure Async_Manager : ASYNC_MANAGER = -struct - -(** preferences **) - -val message_store_limit = 20; -val message_display_limit = 5; - - -(** thread management **) - -(* data structures over threads *) - -structure Thread_Heap = Heap -( - type elem = Time.time * Thread.thread; - fun ord ((a, _), (b, _)) = Time.compare (a, b); -); - -fun lookup_thread xs = AList.lookup Thread.equal xs; -fun delete_thread xs = AList.delete Thread.equal xs; -fun update_thread xs = AList.update Thread.equal xs; - - -(* state of thread manager *) - -type state = - {manager: Thread.thread option, - timeout_heap: Thread_Heap.T, - active: (Thread.thread * (string * Time.time * Time.time * string)) list, - canceling: (Thread.thread * (string * Time.time * string)) list, - messages: (string * string) list, - store: (string * string) list} - -fun make_state manager timeout_heap active canceling messages store : state = - {manager = manager, timeout_heap = timeout_heap, active = active, - canceling = canceling, messages = messages, store = store} - -val global_state = Synchronized.var "async_manager" - (make_state NONE Thread_Heap.empty [] [] [] []); - - -(* unregister thread *) - -fun unregister verbose message thread = - Synchronized.change global_state - (fn state as {manager, timeout_heap, active, canceling, messages, store} => - (case lookup_thread active thread of - SOME (tool, birth_time, _, desc) => - let - val active' = delete_thread thread active; - val now = Time.now () - val canceling' = (thread, (tool, now, desc)) :: canceling - val message' = - desc ^ "\n" ^ message ^ - (if verbose then - "Total time: " ^ Int.toString (Time.toMilliseconds - (Time.- (now, birth_time))) ^ " ms.\n" - else - "") - val messages' = (tool, message') :: messages; - val store' = (tool, message') :: - (if length store <= message_store_limit then store - else #1 (chop message_store_limit store)); - in make_state manager timeout_heap active' canceling' messages' store' end - | NONE => state)); - - -(* main manager thread -- only one may exist *) - -val min_wait_time = Time.fromMilliseconds 300; -val max_wait_time = Time.fromSeconds 10; - -fun replace_all bef aft = - let - fun aux seen "" = String.implode (rev seen) - | aux seen s = - if String.isPrefix bef s then - aux seen "" ^ aft ^ aux [] (unprefix bef s) - else - aux (String.sub (s, 0) :: seen) (String.extract (s, 1, NONE)) - in aux [] end - -(* This is a workaround for Proof General's off-by-a-few sendback display bug, - whereby "pr" in "proof" is not highlighted. *) -fun break_into_chunks xs = - maps (space_explode "\000" o replace_all "\n\n" "\000" o snd) xs - -fun print_new_messages () = - case Synchronized.change_result global_state - (fn {manager, timeout_heap, active, canceling, messages, store} => - (messages, make_state manager timeout_heap active canceling [] - store)) of - [] => () - | msgs as (tool, _) :: _ => - let val ss = break_into_chunks msgs in - List.app priority (tool ^ ": " ^ hd ss :: tl ss) - end - -fun check_thread_manager verbose = Synchronized.change global_state - (fn state as {manager, timeout_heap, active, canceling, messages, store} => - if (case manager of SOME thread => Thread.isActive thread | NONE => false) then state - else let val manager = SOME (Toplevel.thread false (fn () => - let - fun time_limit timeout_heap = - (case try Thread_Heap.min timeout_heap of - NONE => Time.+ (Time.now (), max_wait_time) - | SOME (time, _) => time); - - (*action: find threads whose timeout is reached, and interrupt canceling threads*) - fun action {manager, timeout_heap, active, canceling, messages, store} = - let val (timeout_threads, timeout_heap') = - Thread_Heap.upto (Time.now (), Thread.self ()) timeout_heap; - in - if null timeout_threads andalso null canceling then - NONE - else - let - val _ = List.app (Simple_Thread.interrupt o #1) canceling - val canceling' = filter (Thread.isActive o #1) canceling - val state' = make_state manager timeout_heap' active canceling' messages store; - in SOME (map #2 timeout_threads, state') end - end; - in - while Synchronized.change_result global_state - (fn state as {timeout_heap, active, canceling, messages, store, ...} => - if null active andalso null canceling andalso null messages - then (false, make_state NONE timeout_heap active canceling messages store) - else (true, state)) - do - (Synchronized.timed_access global_state (SOME o time_limit o #timeout_heap) action - |> these - |> List.app (unregister verbose "Timed out.\n"); - print_new_messages (); - (*give threads some time to respond to interrupt*) - OS.Process.sleep min_wait_time) - end)) - in make_state manager timeout_heap active canceling messages store end) - - -(* register thread *) - -fun register tool verbose birth_time death_time desc thread = - (Synchronized.change global_state - (fn {manager, timeout_heap, active, canceling, messages, store} => - let - val timeout_heap' = Thread_Heap.insert (death_time, thread) timeout_heap; - val active' = update_thread (thread, (tool, birth_time, death_time, desc)) active; - val state' = make_state manager timeout_heap' active' canceling messages store; - in state' end); - check_thread_manager verbose); - - -fun launch tool verbose birth_time death_time desc f = - (Toplevel.thread true - (fn () => - let - val self = Thread.self () - val _ = register tool verbose birth_time death_time desc self - val message = f () - in unregister verbose message self end); - ()) - - -(** user commands **) - -(* kill threads *) - -fun kill_threads tool workers = Synchronized.change global_state - (fn {manager, timeout_heap, active, canceling, messages, store} => - let - val killing = - map_filter (fn (th, (tool', _, _, desc)) => - if tool' = tool then SOME (th, (tool', Time.now (), desc)) - else NONE) active - val state' = make_state manager timeout_heap [] (killing @ canceling) messages store; - val _ = if null killing then () else priority ("Killed active " ^ workers ^ ".") - in state' end); - - -(* running threads *) - -fun seconds time = string_of_int (Time.toSeconds time) ^ " s" - -fun running_threads tool workers = - let - val {active, canceling, ...} = Synchronized.value global_state; - - val now = Time.now (); - fun running_info (_, (tool', birth_time, death_time, desc)) = - if tool' = tool then - SOME ("Running: " ^ seconds (Time.- (now, birth_time)) ^ " -- " ^ - seconds (Time.- (death_time, now)) ^ " to live:\n" ^ desc) - else - NONE - fun canceling_info (_, (tool', death_time, desc)) = - if tool' = tool then - SOME ("Trying to interrupt thread since " ^ - seconds (Time.- (now, death_time)) ^ ":\n" ^ desc) - else - NONE - val running = - case map_filter running_info active of - [] => ["No " ^ workers ^ " running."] - | ss => "Running " ^ workers ^ ":" :: ss - val interrupting = - case map_filter canceling_info canceling of - [] => [] - | ss => "Trying to interrupt the following " ^ workers ^ ":" :: ss - in priority (space_implode "\n\n" (running @ interrupting)) end - -fun thread_messages tool worker opt_limit = - let - val limit = the_default message_display_limit opt_limit; - val tool_store = Synchronized.value global_state - |> #store |> filter (curry (op =) tool o fst) - val header = - "Recent " ^ worker ^ " messages" ^ - (if length tool_store <= limit then ":" - else " (" ^ string_of_int limit ^ " displayed):"); - in List.app priority (header :: break_into_chunks (#1 (chop limit tool_store))) end - -end; diff -r f367847f5068 -r 6659c15e7421 src/HOL/Tools/ATP_Manager/atp_problem.ML --- a/src/HOL/Tools/ATP_Manager/atp_problem.ML Wed Jul 28 19:01:07 2010 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,152 +0,0 @@ -(* Title: HOL/Tools/ATP_Manager/atp_problem.ML - Author: Jia Meng, Cambridge University Computer Laboratory and NICTA - Author: Jasmin Blanchette, TU Muenchen - -TPTP syntax. -*) - -signature ATP_PROBLEM = -sig - datatype 'a fo_term = ATerm of 'a * 'a fo_term list - datatype quantifier = AForall | AExists - datatype connective = ANot | AAnd | AOr | AImplies | AIf | AIff | ANotIff - datatype ('a, 'b) formula = - AQuant of quantifier * 'a list * ('a, 'b) formula | - AConn of connective * ('a, 'b) formula list | - AAtom of 'b - - datatype kind = Axiom | Conjecture - datatype 'a problem_line = Fof of string * kind * ('a, 'a fo_term) formula - type 'a problem = (string * 'a problem_line list) list - - val timestamp : unit -> string - val is_tptp_variable : string -> bool - val strings_for_tptp_problem : - (string * string problem_line list) list -> string list - val nice_tptp_problem : - bool -> ('a * (string * string) problem_line list) list - -> ('a * string problem_line list) list - * (string Symtab.table * string Symtab.table) option -end; - -structure ATP_Problem : ATP_PROBLEM = -struct - -(** ATP problem **) - -datatype 'a fo_term = ATerm of 'a * 'a fo_term list -datatype quantifier = AForall | AExists -datatype connective = ANot | AAnd | AOr | AImplies | AIf | AIff | ANotIff -datatype ('a, 'b) formula = - AQuant of quantifier * 'a list * ('a, 'b) formula | - AConn of connective * ('a, 'b) formula list | - AAtom of 'b - -datatype kind = Axiom | Conjecture -datatype 'a problem_line = Fof of string * kind * ('a, 'a fo_term) formula -type 'a problem = (string * 'a problem_line list) list - -val timestamp = Date.fmt "%Y-%m-%d %H:%M:%S" o Date.fromTimeLocal o Time.now - -fun string_for_term (ATerm (s, [])) = s - | string_for_term (ATerm (s, ts)) = - if s = "equal" then space_implode " = " (map string_for_term ts) - else s ^ "(" ^ commas (map string_for_term ts) ^ ")" -fun string_for_quantifier AForall = "!" - | string_for_quantifier AExists = "?" -fun string_for_connective ANot = "~" - | string_for_connective AAnd = "&" - | string_for_connective AOr = "|" - | string_for_connective AImplies = "=>" - | string_for_connective AIf = "<=" - | string_for_connective AIff = "<=>" - | string_for_connective ANotIff = "<~>" -fun string_for_formula (AQuant (q, xs, phi)) = - string_for_quantifier q ^ "[" ^ commas xs ^ "] : " ^ - string_for_formula phi - | string_for_formula (AConn (ANot, [AAtom (ATerm ("equal", ts))])) = - space_implode " != " (map string_for_term ts) - | string_for_formula (AConn (c, [phi])) = - string_for_connective c ^ " " ^ string_for_formula phi - | string_for_formula (AConn (c, phis)) = - "(" ^ space_implode (" " ^ string_for_connective c ^ " ") - (map string_for_formula phis) ^ ")" - | string_for_formula (AAtom tm) = string_for_term tm - -fun string_for_problem_line (Fof (ident, kind, phi)) = - "fof(" ^ ident ^ ", " ^ - (case kind of Axiom => "axiom" | Conjecture => "conjecture") ^ ",\n" ^ - " (" ^ string_for_formula phi ^ ")).\n" -fun strings_for_tptp_problem problem = - "% This file was generated by Isabelle (most likely Sledgehammer)\n\ - \% " ^ timestamp () ^ "\n" :: - maps (fn (_, []) => [] - | (heading, lines) => - "\n% " ^ heading ^ " (" ^ Int.toString (length lines) ^ ")\n" :: - map string_for_problem_line lines) problem - -fun is_tptp_variable s = Char.isUpper (String.sub (s, 0)) - - -(** Nice names **) - -fun empty_name_pool readable_names = - if readable_names then SOME (Symtab.empty, Symtab.empty) else NONE - -fun pool_fold f xs z = pair z #> fold_rev (fn x => uncurry (f x)) xs -fun pool_map f xs = - pool_fold (fn x => fn ys => fn pool => f x pool |>> (fn y => y :: ys)) xs [] - -(* "equal" is reserved by some ATPs. "op" is also reserved, to avoid the - unreadable "op_1", "op_2", etc., in the problem files. *) -val reserved_nice_names = ["equal", "op"] -fun readable_name full_name s = - if s = full_name then - s - else - let - val s = s |> Long_Name.base_name - |> Name.desymbolize (Char.isUpper (String.sub (full_name, 0))) - in if member (op =) reserved_nice_names s then full_name else s end - -fun nice_name (full_name, _) NONE = (full_name, NONE) - | nice_name (full_name, desired_name) (SOME the_pool) = - case Symtab.lookup (fst the_pool) full_name of - SOME nice_name => (nice_name, SOME the_pool) - | NONE => - let - val nice_prefix = readable_name full_name desired_name - fun add j = - let - val nice_name = nice_prefix ^ - (if j = 0 then "" else "_" ^ Int.toString j) - in - case Symtab.lookup (snd the_pool) nice_name of - SOME full_name' => - if full_name = full_name' then (nice_name, the_pool) - else add (j + 1) - | NONE => - (nice_name, - (Symtab.update_new (full_name, nice_name) (fst the_pool), - Symtab.update_new (nice_name, full_name) (snd the_pool))) - end - in add 0 |> apsnd SOME end - - -fun nice_term (ATerm (name, ts)) = - nice_name name ##>> pool_map nice_term ts #>> ATerm -fun nice_formula (AQuant (q, xs, phi)) = - pool_map nice_name xs ##>> nice_formula phi - #>> (fn (xs, phi) => AQuant (q, xs, phi)) - | nice_formula (AConn (c, phis)) = - pool_map nice_formula phis #>> curry AConn c - | nice_formula (AAtom tm) = nice_term tm #>> AAtom -fun nice_problem_line (Fof (ident, kind, phi)) = - nice_formula phi #>> (fn phi => Fof (ident, kind, phi)) -fun nice_problem problem = - pool_map (fn (heading, lines) => - pool_map nice_problem_line lines #>> pair heading) problem -fun nice_tptp_problem readable_names problem = - nice_problem problem (empty_name_pool readable_names) - -end; diff -r f367847f5068 -r 6659c15e7421 src/HOL/Tools/ATP_Manager/atp_systems.ML --- a/src/HOL/Tools/ATP_Manager/atp_systems.ML Wed Jul 28 19:01:07 2010 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,219 +0,0 @@ -(* Title: HOL/Tools/ATP_Manager/atp_systems.ML - Author: Fabian Immler, TU Muenchen - Author: Jasmin Blanchette, TU Muenchen - -Setup for supported ATPs. -*) - -signature ATP_SYSTEMS = -sig - datatype failure = - Unprovable | IncompleteUnprovable | CantConnect | TimedOut | - OutOfResources | OldSpass | MalformedInput | MalformedOutput | UnknownError - - type prover_config = - {executable: string * string, - required_executables: (string * string) list, - arguments: bool -> Time.time -> string, - proof_delims: (string * string) list, - known_failures: (failure * string) list, - max_new_relevant_facts_per_iter: int, - prefers_theory_relevant: bool, - explicit_forall: bool} - - val add_prover: string * prover_config -> theory -> theory - val get_prover: theory -> string -> prover_config - val available_atps: theory -> unit - val refresh_systems_on_tptp : unit -> unit - val default_atps_param_value : unit -> string - val setup : theory -> theory -end; - -structure ATP_Systems : ATP_SYSTEMS = -struct - -(* prover configuration *) - -datatype failure = - Unprovable | IncompleteUnprovable | CantConnect | TimedOut | OutOfResources | - OldSpass | MalformedInput | MalformedOutput | UnknownError - -type prover_config = - {executable: string * string, - required_executables: (string * string) list, - arguments: bool -> Time.time -> string, - proof_delims: (string * string) list, - known_failures: (failure * string) list, - max_new_relevant_facts_per_iter: int, - prefers_theory_relevant: bool, - explicit_forall: bool} - - -(* named provers *) - -structure Data = Theory_Data -( - type T = (prover_config * 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, config) thy = - Data.map (Symtab.update_new (name, (config, 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))) ^ ".") - -fun available_atps thy = - priority ("Available ATPs: " ^ - commas (sort_strings (Symtab.keys (Data.get thy))) ^ ".") - -fun to_generous_secs time = (Time.toMilliseconds time + 999) div 1000 - -(* E prover *) - -val tstp_proof_delims = - ("# SZS output start CNFRefutation.", "# SZS output end CNFRefutation") - -val e_config : prover_config = - {executable = ("E_HOME", "eproof"), - required_executables = [], - arguments = fn _ => fn timeout => - "--tstp-in --tstp-out -l5 -xAutoDev -tAutoDev --silent --cpu-limit=" ^ - string_of_int (to_generous_secs timeout), - proof_delims = [tstp_proof_delims], - known_failures = - [(Unprovable, "SZS status: CounterSatisfiable"), - (Unprovable, "SZS status CounterSatisfiable"), - (TimedOut, "Failure: Resource limit exceeded (time)"), - (TimedOut, "time limit exceeded"), - (OutOfResources, - "# Cannot determine problem status within resource limit"), - (OutOfResources, "SZS status: ResourceOut"), - (OutOfResources, "SZS status ResourceOut")], - max_new_relevant_facts_per_iter = 80 (* FIXME *), - prefers_theory_relevant = false, - explicit_forall = false} -val e = ("e", e_config) - - -(* The "-VarWeight=3" option helps the higher-order problems, probably by - counteracting the presence of "hAPP". *) -val spass_config : prover_config = - {executable = ("ISABELLE_ATP_MANAGER", "scripts/spass"), - required_executables = [("SPASS_HOME", "SPASS")], - (* "div 2" accounts for the fact that SPASS is often run twice. *) - arguments = fn complete => fn timeout => - ("-Auto -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof \ - \-VarWeight=3 -TimeLimit=" ^ - string_of_int (to_generous_secs timeout div 2)) - |> not complete ? prefix "-SOS=1 ", - proof_delims = [("Here is a proof", "Formulae used in the proof")], - known_failures = - [(IncompleteUnprovable, "SPASS beiseite: Completion found"), - (TimedOut, "SPASS beiseite: Ran out of time"), - (OutOfResources, "SPASS beiseite: Maximal number of loops exceeded"), - (MalformedInput, "Undefined symbol"), - (MalformedInput, "Free Variable"), - (OldSpass, "tptp2dfg")], - max_new_relevant_facts_per_iter = 26 (* FIXME *), - prefers_theory_relevant = true, - explicit_forall = true} -val spass = ("spass", spass_config) - -(* Vampire *) - -val vampire_config : prover_config = - {executable = ("VAMPIRE_HOME", "vampire"), - required_executables = [], - arguments = fn _ => fn timeout => - "--mode casc -t " ^ string_of_int (to_generous_secs timeout) ^ - " --input_file ", - proof_delims = - [("=========== Refutation ==========", - "======= End of refutation ======="), - ("% SZS output start Refutation", "% SZS output end Refutation"), - ("% SZS output start Proof", "% SZS output end Proof")], - known_failures = - [(Unprovable, "UNPROVABLE"), - (IncompleteUnprovable, "CANNOT PROVE"), - (Unprovable, "Satisfiability detected"), - (OutOfResources, "Refutation not found")], - max_new_relevant_facts_per_iter = 40 (* FIXME *), - prefers_theory_relevant = false, - explicit_forall = false} -val vampire = ("vampire", vampire_config) - -(* Remote prover invocation via SystemOnTPTP *) - -val systems = Synchronized.var "atp_systems" ([]: string list) - -fun get_systems () = - case bash_output "\"$ISABELLE_ATP_MANAGER/scripts/remote_atp\" -w" of - (answer, 0) => split_lines answer - | (answer, _) => - error ("Failed to get available systems at SystemOnTPTP:\n" ^ - perhaps (try (unsuffix "\n")) answer) - -fun refresh_systems_on_tptp () = - Synchronized.change systems (fn _ => get_systems ()) - -fun get_system prefix = Synchronized.change_result systems (fn systems => - (if null systems then get_systems () else systems) - |> `(find_first (String.isPrefix prefix))); - -fun the_system prefix = - (case get_system prefix of - NONE => error ("System " ^ quote prefix ^ " not available at SystemOnTPTP.") - | SOME sys => sys); - -val remote_known_failures = - [(CantConnect, "HTTP-Error"), - (TimedOut, "says Timeout"), - (MalformedOutput, "Remote script could not extract proof")] - -fun remote_config atp_prefix - ({proof_delims, known_failures, max_new_relevant_facts_per_iter, - prefers_theory_relevant, explicit_forall, ...} : prover_config) - : prover_config = - {executable = ("ISABELLE_ATP_MANAGER", "scripts/remote_atp"), - required_executables = [], - arguments = fn _ => fn timeout => - " -t " ^ string_of_int (to_generous_secs timeout) ^ " -s " ^ - the_system atp_prefix, - proof_delims = insert (op =) tstp_proof_delims proof_delims, - known_failures = remote_known_failures @ known_failures, - max_new_relevant_facts_per_iter = max_new_relevant_facts_per_iter, - prefers_theory_relevant = prefers_theory_relevant, - explicit_forall = explicit_forall} - -val remote_name = prefix "remote_" - -fun remote_prover (name, config) atp_prefix = - (remote_name name, remote_config atp_prefix config) - -val remote_e = remote_prover e "EP---" -val remote_vampire = remote_prover vampire "Vampire---9" - -fun is_installed ({executable, required_executables, ...} : prover_config) = - forall (curry (op <>) "" o getenv o fst) (executable :: required_executables) -fun maybe_remote (name, config) = - name |> not (is_installed config) ? remote_name - -fun default_atps_param_value () = - space_implode " " ([maybe_remote e] @ - (if is_installed (snd spass) then [fst spass] else []) @ - [remote_name (fst vampire)]) - -val provers = [e, spass, vampire, remote_e, remote_vampire] -val setup = fold add_prover provers - -end; diff -r f367847f5068 -r 6659c15e7421 src/HOL/Tools/ATP_Manager/etc/settings --- a/src/HOL/Tools/ATP_Manager/etc/settings Wed Jul 28 19:01:07 2010 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,2 +0,0 @@ -ISABELLE_ATP_MANAGER="$COMPONENT" - diff -r f367847f5068 -r 6659c15e7421 src/HOL/Tools/ATP_Manager/scripts/remote_atp --- a/src/HOL/Tools/ATP_Manager/scripts/remote_atp Wed Jul 28 19:01:07 2010 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,109 +0,0 @@ -#!/usr/bin/env perl -# -# Wrapper for custom remote provers on SystemOnTPTP -# Author: Fabian Immler, TU Muenchen -# - -use warnings; -use strict; -use Getopt::Std; -use HTTP::Request::Common; -use LWP; - -my $SystemOnTPTPFormReplyURL = - "http://www.cs.miami.edu/~tptp/cgi-bin/SystemOnTPTPFormReply"; - -# default parameters -my %URLParameters = ( - "NoHTML" => 1, - "QuietFlag" => "-q01", - "SubmitButton" => "RunSelectedSystems", - "ProblemSource" => "UPLOAD", - "ForceSystem" => "-force", - ); - -#----Get format and transform options if specified -my %Options; -getopts("hws:t:c:",\%Options); - -#----Usage -sub usage() { - print("Usage: remote_atp [] \n"); - print(" are ...\n"); - print(" -h - print this help\n"); - print(" -w - list available ATP systems\n"); - print(" -s - specified system to use\n"); - print(" -t - CPU time limit for system\n"); - print(" -c - custom command for system\n"); - print(" - TPTP problem file\n"); - exit(0); -} -if (exists($Options{'h'})) { - usage(); -} - -#----What systems flag -if (exists($Options{'w'})) { - $URLParameters{"SubmitButton"} = "ListSystems"; - delete($URLParameters{"ProblemSource"}); -} - -#----X2TPTP -if (exists($Options{'x'})) { - $URLParameters{"X2TPTP"} = "-S"; -} - -#----Selected system -my $System; -if (exists($Options{'s'})) { - $System = $Options{'s'}; -} else { - # use Vampire as default - $System = "Vampire---9.0"; -} -$URLParameters{"System___$System"} = $System; - -#----Time limit -if (exists($Options{'t'})) { - $URLParameters{"TimeLimit___$System"} = $Options{'t'}; -} -#----Custom command -if (exists($Options{'c'})) { - $URLParameters{"Command___$System"} = $Options{'c'}; -} - -#----Get single file name -if (exists($URLParameters{"ProblemSource"})) { - if (scalar(@ARGV) >= 1) { - $URLParameters{"UPLOADProblem"} = [shift(@ARGV)]; - } else { - print("Missing problem file\n"); - usage(); - die; - } -} - -# Query Server -my $Agent = LWP::UserAgent->new; -if (exists($Options{'t'})) { - # give server more time to respond - $Agent->timeout($Options{'t'} + 10); -} -my $Request = POST($SystemOnTPTPFormReplyURL, - Content_Type => 'form-data',Content => \%URLParameters); -my $Response = $Agent->request($Request); - -#catch errors / failure -if(!$Response->is_success) { - print "HTTP-Error: " . $Response->message . "\n"; - exit(-1); -} elsif (exists($Options{'w'})) { - print $Response->content; - exit (0); -} elsif ($Response->content =~ /WARNING: (\S*) does not exist/) { - print "Specified System $1 does not exist\n"; - exit(-1); -} else { - print $Response->content; - exit(0); -} diff -r f367847f5068 -r 6659c15e7421 src/HOL/Tools/ATP_Manager/scripts/spass --- a/src/HOL/Tools/ATP_Manager/scripts/spass Wed Jul 28 19:01:07 2010 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,19 +0,0 @@ -#!/usr/bin/env bash -# -# Wrapper for SPASS that also outputs the Flotter-generated CNF (needed for -# Isar proof reconstruction) -# -# Author: Jasmin Blanchette, TU Muenchen - -options=${@:1:$(($#-1))} -name=${@:$(($#)):1} - -$SPASS_HOME/tptp2dfg $name $name.fof.dfg -$SPASS_HOME/SPASS -Flotter $name.fof.dfg \ - | sed 's/description({$/description({*/' \ - > $name.cnf.dfg -rm -f $name.fof.dfg -cat $name.cnf.dfg -$SPASS_HOME/SPASS $options $name.cnf.dfg \ - | sed 's/\(Formulae used in the proof :\).*/\1 N\/A/' -rm -f $name.cnf.dfg