--- /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;
--- /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;
--- /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;
--- /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"
+
--- /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 [<options>] <File name>\n");
+ print(" <options> are ...\n");
+ print(" -h - print this help\n");
+ print(" -w - list available ATP systems\n");
+ print(" -s<system> - specified system to use\n");
+ print(" -t<timelimit> - CPU time limit for system\n");
+ print(" -c<command> - custom command for system\n");
+ print(" <File name> - 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);
+}
--- /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
--- 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;
--- 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;
--- 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;
--- 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"
-
--- 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 [<options>] <File name>\n");
- print(" <options> are ...\n");
- print(" -h - print this help\n");
- print(" -w - list available ATP systems\n");
- print(" -s<system> - specified system to use\n");
- print(" -t<timelimit> - CPU time limit for system\n");
- print(" -c<command> - custom command for system\n");
- print(" <File name> - 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);
-}
--- 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