src/HOL/Tools/ATP_Manager as separate component, with (almost) everything in one place;
--- a/etc/components Tue Aug 04 16:13:16 2009 +0200
+++ b/etc/components Tue Aug 04 19:20:24 2009 +0200
@@ -1,3 +1,4 @@
+#main object logics
src/Pure
src/FOL
src/HOL
@@ -9,3 +10,6 @@
src/HOLCF
src/LCF
src/Sequents
+#misc components
+src/HOL/Tools/ATP_Manager
+
--- a/lib/scripts/SystemOnTPTP Tue Aug 04 16:13:16 2009 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,141 +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",
- );
-
-#----Get format and transform options if specified
-my %Options;
-getopts("hwxs:t:c:",\%Options);
-
-#----Usage
-sub usage() {
- print("Usage: remote [<options>] <File name>\n");
- print(" <options> are ...\n");
- print(" -h - print this help\n");
- print(" -w - list available ATP systems\n");
- print(" -x - use X2TPTP to convert output of prover\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);
-} elsif (exists($Options{'x'}) &&
- $Response->content =~
- /%\s*Result\s*:\s*Unsatisfiable.*\n%\s*Output\s*:\s*(CNF)?Refutation.*\n%/ &&
- $Response->content !~ /ERROR: Could not form TPTP format derivation/ )
-{
- # converted output: extract proof
- my @lines = split( /\n/, $Response->content);
- my $extract = "";
- foreach my $line (@lines){
- #ignore comments
- if ($line !~ /^%/ && !($line eq "")) {
- $extract .= "$line";
- }
- }
- # insert newlines after ').'
- $extract =~ s/\s//g;
- $extract =~ s/\)\.cnf/\)\.\ncnf/g;
-
- print "========== ~~/lib/scripts/SystemOnTPTP extracted proof: ==========\n";
- # orientation for res_reconstruct.ML
- print "# SZS output start CNFRefutation.\n";
- print "$extract\n";
- print "# SZS output end CNFRefutation.\n";
- # can be useful for debugging; Isabelle ignores this
- print "============== original response from SystemOnTPTP: ==============\n";
- print $Response->content;
- exit(0);
-} elsif (!exists($Options{'x'})) {
- # pass output directly to Isabelle
- print $Response->content;
- exit(0);
-}else {
- print "Remote-script could not extract proof:\n".$Response->content;
- exit(-1);
-}
-
--- a/src/HOL/ATP_Linkup.thy Tue Aug 04 16:13:16 2009 +0200
+++ b/src/HOL/ATP_Linkup.thy Tue Aug 04 19:20:24 2009 +0200
@@ -15,9 +15,9 @@
("Tools/res_hol_clause.ML")
("Tools/res_reconstruct.ML")
("Tools/res_atp.ML")
- ("Tools/atp_manager.ML")
- ("Tools/atp_wrapper.ML")
- ("Tools/atp_minimal.ML")
+ ("Tools/ATP_Manager/atp_manager.ML")
+ ("Tools/ATP_Manager/atp_wrapper.ML")
+ ("Tools/ATP_Manager/atp_minimal.ML")
"~~/src/Tools/Metis/metis.ML"
("Tools/metis_tools.ML")
begin
@@ -96,10 +96,9 @@
use "Tools/res_reconstruct.ML" setup ResReconstruct.setup
use "Tools/res_atp.ML"
-use "Tools/atp_manager.ML"
-use "Tools/atp_wrapper.ML"
-
-use "Tools/atp_minimal.ML"
+use "Tools/ATP_Manager/atp_manager.ML"
+use "Tools/ATP_Manager/atp_wrapper.ML"
+use "Tools/ATP_Manager/atp_minimal.ML"
text {* basic provers *}
setup {* AtpManager.add_prover "spass" AtpWrapper.spass *}
--- a/src/HOL/IsaMakefile Tue Aug 04 16:13:16 2009 +0200
+++ b/src/HOL/IsaMakefile Tue Aug 04 19:20:24 2009 +0200
@@ -231,12 +231,13 @@
$(SRC)/Provers/Arith/combine_numerals.ML \
$(SRC)/Provers/Arith/extract_common_term.ML \
$(SRC)/Tools/Metis/metis.ML \
+ Tools/ATP_Manager/atp_manager.ML \
+ Tools/ATP_Manager/atp_minimal.ML \
+ Tools/ATP_Manager/atp_wrapper.ML \
Tools/Groebner_Basis/groebner.ML \
Tools/Groebner_Basis/misc.ML \
+ Tools/Groebner_Basis/normalizer.ML \
Tools/Groebner_Basis/normalizer_data.ML \
- Tools/Groebner_Basis/normalizer.ML \
- Tools/atp_manager.ML \
- Tools/atp_wrapper.ML \
Tools/int_arith.ML \
Tools/list_code.ML \
Tools/meson.ML \
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/ATP_Manager/SystemOnTPTP Tue Aug 04 19:20:24 2009 +0200
@@ -0,0 +1,141 @@
+#!/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",
+ );
+
+#----Get format and transform options if specified
+my %Options;
+getopts("hwxs:t:c:",\%Options);
+
+#----Usage
+sub usage() {
+ print("Usage: remote [<options>] <File name>\n");
+ print(" <options> are ...\n");
+ print(" -h - print this help\n");
+ print(" -w - list available ATP systems\n");
+ print(" -x - use X2TPTP to convert output of prover\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);
+} elsif (exists($Options{'x'}) &&
+ $Response->content =~
+ /%\s*Result\s*:\s*Unsatisfiable.*\n%\s*Output\s*:\s*(CNF)?Refutation.*\n%/ &&
+ $Response->content !~ /ERROR: Could not form TPTP format derivation/ )
+{
+ # converted output: extract proof
+ my @lines = split( /\n/, $Response->content);
+ my $extract = "";
+ foreach my $line (@lines){
+ #ignore comments
+ if ($line !~ /^%/ && !($line eq "")) {
+ $extract .= "$line";
+ }
+ }
+ # insert newlines after ').'
+ $extract =~ s/\s//g;
+ $extract =~ s/\)\.cnf/\)\.\ncnf/g;
+
+ print "========== ~~/lib/scripts/SystemOnTPTP extracted proof: ==========\n";
+ # orientation for res_reconstruct.ML
+ print "# SZS output start CNFRefutation.\n";
+ print "$extract\n";
+ print "# SZS output end CNFRefutation.\n";
+ # can be useful for debugging; Isabelle ignores this
+ print "============== original response from SystemOnTPTP: ==============\n";
+ print $Response->content;
+ exit(0);
+} elsif (!exists($Options{'x'})) {
+ # pass output directly to Isabelle
+ print $Response->content;
+ exit(0);
+}else {
+ print "Remote-script could not extract proof:\n".$Response->content;
+ exit(-1);
+}
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML Tue Aug 04 19:20:24 2009 +0200
@@ -0,0 +1,403 @@
+(* Title: HOL/Tools/ATP_Manager/atp_manager.ML
+ Author: Fabian Immler, TU Muenchen
+
+ATP threads are registered here.
+Threads with the same birth-time are seen as one group.
+All threads of a group are killed when one thread of it has been successful,
+or after a certain time,
+or when the maximum number of threads exceeds; then the oldest thread is killed.
+*)
+
+signature ATP_MANAGER =
+sig
+ val get_atps: unit -> string
+ val set_atps: string -> unit
+ val get_max_atps: unit -> int
+ val set_max_atps: int -> unit
+ val get_timeout: unit -> int
+ val set_timeout: int -> unit
+ val get_full_types: unit -> bool
+ val set_full_types: bool -> unit
+ val kill: unit -> unit
+ val info: unit -> unit
+ val messages: int option -> unit
+ type prover = int -> (thm * (string * int)) list option ->
+ (thm * (string * int)) list option -> string -> int ->
+ Proof.context * (thm list * thm) ->
+ bool * string * string * string vector * (thm * (string * int)) list
+ val add_prover: string -> prover -> theory -> theory
+ val print_provers: theory -> unit
+ val get_prover: string -> theory -> prover option
+ val sledgehammer: string list -> Proof.state -> unit
+end;
+
+structure AtpManager: ATP_MANAGER =
+struct
+
+(** preferences **)
+
+val message_store_limit = 20;
+val message_display_limit = 5;
+
+local
+
+val atps = ref "e remote_vampire";
+val max_atps = ref 5; (* ~1 means infinite number of atps *)
+val timeout = ref 60;
+val full_types = ref false;
+
+in
+
+fun get_atps () = CRITICAL (fn () => ! atps);
+fun set_atps str = CRITICAL (fn () => atps := str);
+
+fun get_max_atps () = CRITICAL (fn () => ! max_atps);
+fun set_max_atps number = CRITICAL (fn () => max_atps := number);
+
+fun get_timeout () = CRITICAL (fn () => ! timeout);
+fun set_timeout time = CRITICAL (fn () => timeout := time);
+
+fun get_full_types () = CRITICAL (fn () => ! full_types);
+fun set_full_types bool = CRITICAL (fn () => full_types := bool);
+
+val _ =
+ ProofGeneralPgip.add_preference Preferences.category_proof
+ (Preferences.string_pref atps
+ "ATP: provers" "Default automatic provers (separated by whitespace)");
+
+val _ =
+ ProofGeneralPgip.add_preference Preferences.category_proof
+ (Preferences.int_pref max_atps
+ "ATP: maximum number" "How many provers may run in parallel");
+
+val _ =
+ ProofGeneralPgip.add_preference Preferences.category_proof
+ (Preferences.int_pref timeout
+ "ATP: timeout" "ATPs will be interrupted after this time (in seconds)");
+
+val _ =
+ ProofGeneralPgip.add_preference Preferences.category_proof
+ (Preferences.bool_pref full_types
+ "ATP: full types" "ATPs will use full type information");
+
+end;
+
+
+
+(** thread management **)
+
+(* data structures over threads *)
+
+structure ThreadHeap = HeapFun
+(
+ 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 *)
+
+datatype T = State of
+ {managing_thread: Thread.thread option,
+ timeout_heap: ThreadHeap.T,
+ oldest_heap: ThreadHeap.T,
+ active: (Thread.thread * (Time.time * Time.time * string)) list,
+ cancelling: (Thread.thread * (Time.time * Time.time * string)) list,
+ messages: string list,
+ store: string list};
+
+fun make_state managing_thread timeout_heap oldest_heap active cancelling messages store =
+ State {managing_thread = managing_thread, timeout_heap = timeout_heap, oldest_heap = oldest_heap,
+ active = active, cancelling = cancelling, messages = messages, store = store};
+
+val state = Synchronized.var "atp_manager"
+ (make_state NONE ThreadHeap.empty ThreadHeap.empty [] [] [] []);
+
+
+(* unregister thread *)
+
+fun unregister (success, message) thread = Synchronized.change state
+ (fn state as State {managing_thread, timeout_heap, oldest_heap, active, cancelling, messages, store} =>
+ (case lookup_thread active thread of
+ SOME (birthtime, _, description) =>
+ let
+ val (group, active') =
+ if success then List.partition (fn (_, (tb, _, _)) => tb = birthtime) active
+ else List.partition (fn (th, _) => Thread.equal (th, thread)) active
+
+ val now = Time.now ()
+ val cancelling' =
+ fold (fn (th, (tb, _, desc)) => update_thread (th, (tb, now, desc))) group cancelling
+
+ val message' = description ^ "\n" ^ message ^
+ (if length group <= 1 then ""
+ else "\nInterrupted " ^ string_of_int (length group - 1) ^ " other group members")
+ val store' = message' ::
+ (if length store <= message_store_limit then store
+ else #1 (chop message_store_limit store))
+ in make_state
+ managing_thread timeout_heap oldest_heap active' cancelling' (message' :: messages) store'
+ end
+ | NONE => state));
+
+
+(* kill excessive atp threads *)
+
+fun excessive_atps active =
+ let val max = get_max_atps ()
+ in length active > max andalso max > ~1 end;
+
+local
+
+fun kill_oldest () =
+ let exception Unchanged in
+ Synchronized.change_result state
+ (fn State {managing_thread, timeout_heap, oldest_heap, active, cancelling, messages, store} =>
+ if ThreadHeap.is_empty oldest_heap orelse not (excessive_atps active)
+ then raise Unchanged
+ else
+ let val ((_, oldest_thread), oldest_heap') = ThreadHeap.min_elem oldest_heap
+ in (oldest_thread,
+ make_state managing_thread timeout_heap oldest_heap' active cancelling messages store) end)
+ |> unregister (false, "Interrupted (maximum number of ATPs exceeded)")
+ handle Unchanged => ()
+ end;
+
+in
+
+fun kill_excessive () =
+ let val State {active, ...} = Synchronized.value state
+ in if excessive_atps active then (kill_oldest (); kill_excessive ()) else () end;
+
+end;
+
+fun print_new_messages () =
+ let val to_print = Synchronized.change_result state
+ (fn State {managing_thread, timeout_heap, oldest_heap, active, cancelling, messages, store} =>
+ (messages, make_state managing_thread timeout_heap oldest_heap active cancelling [] store))
+ in
+ if null to_print then ()
+ else priority ("Sledgehammer: " ^ space_implode "\n\n" to_print)
+ end;
+
+
+(* start a watching thread -- only one may exist *)
+
+fun check_thread_manager () = Synchronized.change state
+ (fn State {managing_thread, timeout_heap, oldest_heap, active, cancelling, messages, store} =>
+ if (case managing_thread of SOME thread => Thread.isActive thread | NONE => false)
+ then make_state managing_thread timeout_heap oldest_heap active cancelling messages store
+ else let val managing_thread = SOME (SimpleThread.fork false (fn () =>
+ let
+ val min_wait_time = Time.fromMilliseconds 300
+ val max_wait_time = Time.fromSeconds 10
+
+ (* wait for next thread to cancel, or maximum*)
+ fun time_limit (State {timeout_heap, ...}) =
+ (case try ThreadHeap.min timeout_heap of
+ NONE => SOME (Time.+ (Time.now (), max_wait_time))
+ | SOME (time, _) => SOME time)
+
+ (* action: find threads whose timeout is reached, and interrupt cancelling threads *)
+ fun action (State {managing_thread, timeout_heap, oldest_heap, active, cancelling,
+ messages, store}) =
+ let val (timeout_threads, timeout_heap') =
+ ThreadHeap.upto (Time.now (), Thread.self ()) timeout_heap
+ in
+ if null timeout_threads andalso null cancelling andalso not (excessive_atps active)
+ then NONE
+ else
+ let
+ val _ = List.app (SimpleThread.interrupt o #1) cancelling
+ val cancelling' = filter (Thread.isActive o #1) cancelling
+ val state' = make_state
+ managing_thread timeout_heap' oldest_heap active cancelling' messages store
+ in SOME (map #2 timeout_threads, state') end
+ end
+ in
+ while Synchronized.change_result state
+ (fn st as
+ State {managing_thread, timeout_heap, oldest_heap, active, cancelling, messages, store} =>
+ if (null active) andalso (null cancelling) andalso (null messages)
+ then (false, make_state NONE timeout_heap oldest_heap active cancelling messages store)
+ else (true, st))
+ do
+ (Synchronized.timed_access state time_limit action
+ |> these
+ |> List.app (unregister (false, "Interrupted (reached timeout)"));
+ kill_excessive ();
+ print_new_messages ();
+ (*give threads time to respond to interrupt*)
+ OS.Process.sleep min_wait_time)
+ end))
+ in make_state managing_thread timeout_heap oldest_heap active cancelling messages store end);
+
+
+(* thread is registered here by sledgehammer *)
+
+fun register birthtime deadtime (thread, desc) =
+ (Synchronized.change state
+ (fn State {managing_thread, timeout_heap, oldest_heap, active, cancelling, messages, store} =>
+ let
+ val timeout_heap' = ThreadHeap.insert (deadtime, thread) timeout_heap
+ val oldest_heap' = ThreadHeap.insert (birthtime, thread) oldest_heap
+ val active' = update_thread (thread, (birthtime, deadtime, desc)) active
+ in make_state managing_thread timeout_heap' oldest_heap' active' cancelling messages store end);
+ check_thread_manager ());
+
+
+
+(** user commands **)
+
+(* kill: move all threads to cancelling *)
+
+fun kill () = Synchronized.change state
+ (fn State {managing_thread, timeout_heap, oldest_heap, active, cancelling, messages, store} =>
+ let val formerly_active = map (fn (th, (tb, _, desc)) => (th, (tb, Time.now (), desc))) active
+ in make_state
+ managing_thread timeout_heap oldest_heap [] (formerly_active @ cancelling) messages store
+ end);
+
+
+(* ATP info *)
+
+fun info () =
+ let
+ val State {active, cancelling, ...} = Synchronized.value state
+
+ fun running_info (_, (birth_time, dead_time, desc)) = "Running: "
+ ^ (string_of_int o Time.toSeconds) (Time.- (Time.now (), birth_time))
+ ^ " s -- "
+ ^ (string_of_int o Time.toSeconds) (Time.- (dead_time, Time.now ()))
+ ^ " s to live:\n" ^ desc
+ fun cancelling_info (_, (_, dead_time, desc)) = "Trying to interrupt thread since "
+ ^ (string_of_int o Time.toSeconds) (Time.- (Time.now (), dead_time))
+ ^ " s:\n" ^ desc
+
+ val running =
+ if null active then "No ATPs running."
+ else space_implode "\n\n" ("Running ATPs:" :: map running_info active)
+ val interrupting =
+ if null cancelling then ""
+ else space_implode "\n\n"
+ ("Trying to interrupt the following ATPs:" :: map cancelling_info cancelling)
+
+ in writeln (running ^ "\n" ^ interrupting) end;
+
+fun messages opt_limit =
+ let
+ val limit = the_default message_display_limit opt_limit;
+ val State {store = msgs, ...} = Synchronized.value state
+ val header = "Recent ATP messages" ^
+ (if length msgs <= limit then ":" else " (" ^ string_of_int limit ^ " displayed):");
+ in writeln (space_implode "\n\n" (header :: #1 (chop limit msgs))) end;
+
+
+
+(** The Sledgehammer **)
+
+(* named provers *)
+
+type prover = int -> (thm * (string * int)) list option ->
+ (thm * (string * int)) list option -> string -> int ->
+ Proof.context * (thm list * thm) ->
+ bool * string * string * string vector * (thm * (string * int)) list
+
+fun err_dup_prover name = error ("Duplicate prover: " ^ quote name);
+
+structure Provers = TheoryDataFun
+(
+ type T = (prover * stamp) Symtab.table
+ val empty = Symtab.empty
+ val copy = I
+ val extend = I
+ fun merge _ tabs : T = Symtab.merge (eq_snd op =) tabs
+ handle Symtab.DUP dup => err_dup_prover dup
+);
+
+fun add_prover name prover thy =
+ Provers.map (Symtab.update_new (name, (prover, stamp ()))) thy
+ handle Symtab.DUP dup => err_dup_prover dup;
+
+fun print_provers thy = Pretty.writeln
+ (Pretty.strs ("external provers:" :: sort_strings (Symtab.keys (Provers.get thy))));
+
+fun get_prover name thy = case Symtab.lookup (Provers.get thy) name of
+ NONE => NONE
+| SOME (prover, _) => SOME prover;
+
+(* start prover thread *)
+
+fun start_prover name birthtime deadtime i proof_state =
+ (case get_prover name (Proof.theory_of proof_state) of
+ NONE => warning ("Unknown external prover: " ^ quote name)
+ | SOME prover =>
+ let
+ val (ctxt, (_, goal)) = Proof.get_goal proof_state
+ val desc =
+ "external prover " ^ quote name ^ " for subgoal " ^ string_of_int i ^ ":\n" ^
+ Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i))
+ val _ = SimpleThread.fork true (fn () =>
+ let
+ val _ = register birthtime deadtime (Thread.self (), desc)
+ val result =
+ let val (success, message, _, _, _) =
+ prover (get_timeout ()) NONE NONE name i (Proof.get_goal proof_state)
+ in (success, message) end
+ handle ResHolClause.TOO_TRIVIAL
+ => (true, "Empty clause: Try this command: " ^ Markup.markup Markup.sendback "apply metis")
+ | ERROR msg
+ => (false, "Error: " ^ msg)
+ val _ = unregister result (Thread.self ())
+ in () end handle Interrupt => ())
+ in () end);
+
+
+(* sledghammer for first subgoal *)
+
+fun sledgehammer names proof_state =
+ let
+ val provers =
+ if null names then String.tokens (Symbol.is_ascii_blank o String.str) (get_atps ())
+ else names
+ val birthtime = Time.now ()
+ val deadtime = Time.+ (birthtime, Time.fromSeconds (get_timeout ()))
+ in List.app (fn name => start_prover name birthtime deadtime 1 proof_state) provers end;
+
+
+
+(** Isar command syntax **)
+
+local structure K = OuterKeyword and P = OuterParse in
+
+val _ =
+ OuterSyntax.improper_command "atp_kill" "kill all managed provers" K.diag
+ (Scan.succeed (Toplevel.no_timing o Toplevel.imperative kill));
+
+val _ =
+ OuterSyntax.improper_command "atp_info" "print information about managed provers" K.diag
+ (Scan.succeed (Toplevel.no_timing o Toplevel.imperative info));
+
+val _ =
+ OuterSyntax.improper_command "atp_messages" "print recent messages issued by managed provers" K.diag
+ (Scan.option (P.$$$ "(" |-- P.nat --| P.$$$ ")") >>
+ (fn limit => Toplevel.no_timing o Toplevel.imperative (fn () => messages limit)));
+
+val _ =
+ OuterSyntax.improper_command "print_atps" "print external provers" K.diag
+ (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_theory o
+ Toplevel.keep (print_provers o Toplevel.theory_of)));
+
+val _ =
+ OuterSyntax.command "sledgehammer" "call all automatic theorem provers" K.diag
+ (Scan.repeat P.xname >> (fn names => Toplevel.no_timing o Toplevel.unknown_proof o
+ Toplevel.keep (sledgehammer names o Toplevel.proof_of)));
+
+end;
+
+end;
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/ATP_Manager/atp_minimal.ML Tue Aug 04 19:20:24 2009 +0200
@@ -0,0 +1,223 @@
+(* Title: HOL/Tools/ATP_Manager/atp_minimal.ML
+ Author: Philipp Meyer, TU Muenchen
+
+Minimalization of theorem list for metis by using an external automated theorem prover
+*)
+
+structure AtpMinimal: sig end =
+struct
+
+(* output control *)
+
+fun debug str = Output.debug (fn () => str)
+fun debug_fn f = if ! Output.debugging then f () else ()
+fun answer str = Output.writeln str
+fun println str = Output.priority str
+
+fun order_unique name_list = OrdList.make (String.collate Char.compare) name_list
+fun length_string namelist = Int.toString (length namelist)
+
+fun print_names name_thms_pairs =
+ let
+ val names = map fst name_thms_pairs
+ val ordered = order_unique names
+ in
+ app (fn name => (debug (" " ^ name))) ordered
+ end
+
+
+(* minimalization algorithm *)
+
+local
+ fun isplit (l,r) [] = (l,r)
+ | isplit (l,r) (h::[]) = (h::l, r)
+ | isplit (l,r) (h1::h2::t) = isplit (h1::l, h2::r) t
+in
+ fun split lst = isplit ([],[]) lst
+end
+
+local
+ fun min p sup [] = raise Empty
+ | min p sup [s0] = [s0]
+ | min p sup s =
+ let
+ val (l0, r0) = split s
+ in
+ if p (sup @ l0)
+ then min p sup l0
+ else
+ if p (sup @ r0)
+ then min p sup r0
+ else
+ let
+ val l = min p (sup @ r0) l0
+ val r = min p (sup @ l) r0
+ in
+ l @ r
+ end
+ end
+in
+ (* return a minimal subset v of s that satisfies p
+ @pre p(s) & ~p([]) & monotone(p)
+ @post v subset s & p(v) &
+ forall e in v. ~p(v \ e)
+ *)
+ fun minimal p s = min p [] s
+end
+
+
+(* failure check and producing answer *)
+
+datatype 'a prove_result = Success of 'a | Failure | Timeout | Error
+
+val string_of_result =
+ fn Success _ => "Success"
+ | Failure => "Failure"
+ | Timeout => "Timeout"
+ | Error => "Error"
+
+val failure_strings =
+ [("SPASS beiseite: Ran out of time.", Timeout),
+ ("Timeout", Timeout),
+ ("time limit exceeded", Timeout),
+ ("# Cannot determine problem status within resource limit", Timeout),
+ ("Error", Error)]
+
+fun produce_answer (success, message, result_string, thm_name_vec, filtered) =
+ if success then
+ (Success (Vector.foldr op:: [] thm_name_vec, filtered), result_string)
+ else
+ let
+ val failure = failure_strings |> get_first (fn (s, t) =>
+ if String.isSubstring s result_string then SOME (t, result_string) else NONE)
+ in
+ if is_some failure then
+ the failure
+ else
+ (Failure, result_string)
+ end
+
+
+(* wrapper for calling external prover *)
+
+fun sh_test_thms prover prover_name time_limit subgoalno state filtered name_thms_pairs =
+ let
+ val _ = println ("Testing " ^ (length_string name_thms_pairs) ^ " theorems... ")
+ val name_thm_pairs =
+ flat (map (fn (n, ths) => map_index (fn (i, th) => (n, th)) ths) name_thms_pairs)
+ val _ = debug_fn (fn () => print_names name_thm_pairs)
+ val axclauses = ResAxioms.cnf_rules_pairs (Proof.theory_of state) name_thm_pairs
+ val (result, proof) =
+ produce_answer
+ (prover time_limit (SOME axclauses) filtered prover_name subgoalno (Proof.get_goal state))
+ val _ = println (string_of_result result)
+ val _ = debug proof
+ in
+ (result, proof)
+ end
+
+
+(* minimalization of thms *)
+
+fun minimalize prover prover_name time_limit state name_thms_pairs =
+ let
+ val _ =
+ println ("Minimize called with " ^ length_string name_thms_pairs ^ " theorems, prover: "
+ ^ prover_name ^ ", time limit: " ^ Int.toString time_limit ^ " seconds")
+ val _ = debug_fn (fn () => app (fn (n, tl) =>
+ (debug n; app (fn t =>
+ debug (" " ^ Display.string_of_thm (Proof.context_of state) t)) tl)) name_thms_pairs)
+ val test_thms_fun = sh_test_thms prover prover_name time_limit 1 state
+ fun test_thms filtered thms =
+ case test_thms_fun filtered thms of (Success _, _) => true | _ => false
+ in
+ (* try prove first to check result and get used theorems *)
+ (case test_thms_fun NONE name_thms_pairs of
+ (Success (used, filtered), _) =>
+ let
+ val ordered_used = order_unique used
+ val to_use =
+ if length ordered_used < length name_thms_pairs then
+ filter (fn (name1, _) => List.exists (equal name1) ordered_used) name_thms_pairs
+ else
+ name_thms_pairs
+ val min_thms = (minimal (test_thms (SOME filtered)) to_use)
+ val min_names = order_unique (map fst min_thms)
+ val _ = println ("Minimal " ^ (length_string min_thms) ^ " theorems")
+ val _ = debug_fn (fn () => print_names min_thms)
+ in
+ answer ("Try this command: " ^
+ Markup.markup Markup.sendback ("apply (metis " ^ space_implode " " min_names ^ ")"))
+ end
+ | (Timeout, _) =>
+ answer ("Timeout: You may need to increase the time limit of " ^
+ Int.toString time_limit ^ " seconds. Call atp_minimize [time=...] ")
+ | (Error, msg) =>
+ answer ("Error in prover: " ^ msg)
+ | (Failure, _) =>
+ answer "Failure: No proof with the theorems supplied")
+ handle ResHolClause.TOO_TRIVIAL =>
+ answer ("Trivial: Try this command: " ^ Markup.markup Markup.sendback "apply metis")
+ | ERROR msg =>
+ answer ("Error: " ^ msg)
+ end
+
+
+(* Isar command and parsing input *)
+
+local structure K = OuterKeyword and P = OuterParse and T = OuterLex in
+
+fun get_thms context =
+ map (fn (name, interval) =>
+ let
+ val thmref = Facts.Named ((name, Position.none), interval)
+ val ths = ProofContext.get_fact context thmref
+ val name' = Facts.string_of_ref thmref
+ in
+ (name', ths)
+ end)
+
+val default_prover = "remote_vampire"
+val default_time_limit = 5
+
+fun get_time_limit_arg time_string =
+ (case Int.fromString time_string of
+ SOME t => t
+ | NONE => error ("Invalid time limit: " ^ quote time_string))
+
+val get_options =
+ let
+ val def = (default_prover, default_time_limit)
+ in
+ foldl (fn ((name, a), (p, t)) =>
+ (case name of
+ "time" => (p, (get_time_limit_arg a))
+ | "atp" => (a, t)
+ | n => error ("Invalid argument: " ^ n))) def
+ end
+
+fun sh_min_command args thm_names state =
+ let
+ val (prover_name, time_limit) = get_options args
+ val prover =
+ case AtpManager.get_prover prover_name (Proof.theory_of state) of
+ SOME prover => prover
+ | NONE => error ("Unknown prover: " ^ quote prover_name)
+ val name_thms_pairs = get_thms (Proof.context_of state) thm_names
+ in
+ minimalize prover prover_name time_limit state name_thms_pairs
+ end
+
+val parse_args = Scan.optional (Args.bracks (P.list (P.xname --| P.$$$ "=" -- P.xname))) []
+val parse_thm_names = Scan.repeat (P.xname -- Scan.option Attrib.thm_sel)
+
+val _ =
+ OuterSyntax.command "atp_minimize" "minimize theorem list with external prover" K.diag
+ (parse_args -- parse_thm_names >> (fn (args, thm_names) =>
+ Toplevel.no_timing o Toplevel.unknown_proof o
+ Toplevel.keep (sh_min_command args thm_names o Toplevel.proof_of)))
+
+end
+
+end
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/ATP_Manager/atp_wrapper.ML Tue Aug 04 19:20:24 2009 +0200
@@ -0,0 +1,217 @@
+(* Title: HOL/Tools/ATP_Manager/atp_wrapper.ML
+ Author: Fabian Immler, TU Muenchen
+
+Wrapper functions for external ATPs.
+*)
+
+signature ATP_WRAPPER =
+sig
+ val destdir: string ref
+ val problem_name: string ref
+ val tptp_prover_opts_full: int -> bool -> bool -> Path.T * string -> AtpManager.prover
+ val tptp_prover_opts: int -> bool -> Path.T * string -> AtpManager.prover
+ val tptp_prover: Path.T * string -> AtpManager.prover
+ val full_prover_opts: int -> bool -> Path.T * string -> AtpManager.prover
+ val full_prover: Path.T * string -> AtpManager.prover
+ val vampire_opts: int -> bool -> AtpManager.prover
+ val vampire: AtpManager.prover
+ val vampire_opts_full: int -> bool -> AtpManager.prover
+ val vampire_full: AtpManager.prover
+ val eprover_opts: int -> bool -> AtpManager.prover
+ val eprover: AtpManager.prover
+ val eprover_opts_full: int -> bool -> AtpManager.prover
+ val eprover_full: AtpManager.prover
+ val spass_opts: int -> bool -> AtpManager.prover
+ val spass: AtpManager.prover
+ val remote_prover_opts: int -> bool -> string -> string -> AtpManager.prover
+ val remote_prover: string -> string -> AtpManager.prover
+ val refresh_systems: unit -> unit
+end;
+
+structure AtpWrapper: ATP_WRAPPER =
+struct
+
+(** generic ATP wrapper **)
+
+(* global hooks for writing problemfiles *)
+
+val destdir = ref ""; (*Empty means write files to /tmp*)
+val problem_name = ref "prob";
+
+
+(* basic template *)
+
+fun external_prover relevance_filter preparer writer (cmd, args) find_failure produce_answer
+ timeout axiom_clauses filtered_clauses name subgoalno goal =
+ let
+ (* path to unique problem file *)
+ val destdir' = ! destdir
+ val problem_name' = ! problem_name
+ fun prob_pathname nr =
+ let val probfile = Path.basic (problem_name' ^ serial_string () ^ "_" ^ string_of_int nr)
+ in if destdir' = "" then File.tmp_path probfile
+ else if File.exists (Path.explode (destdir'))
+ then Path.append (Path.explode (destdir')) probfile
+ else error ("No such directory: " ^ destdir')
+ end
+
+ (* get clauses and prepare them for writing *)
+ val (ctxt, (chain_ths, th)) = goal
+ val thy = ProofContext.theory_of ctxt
+ val chain_ths = map (Thm.put_name_hint ResReconstruct.chained_hint) chain_ths
+ val goal_cls = #1 (ResAxioms.neg_conjecture_clauses ctxt th subgoalno)
+ val _ = app (fn th => Output.debug (fn _ => Display.string_of_thm ctxt th)) goal_cls
+ val the_filtered_clauses =
+ case filtered_clauses of
+ NONE => relevance_filter goal goal_cls
+ | SOME fcls => fcls
+ val the_axiom_clauses =
+ case axiom_clauses of
+ NONE => the_filtered_clauses
+ | SOME axcls => axcls
+ val (thm_names, clauses) =
+ preparer goal_cls chain_ths the_axiom_clauses the_filtered_clauses thy
+
+ (* write out problem file and call prover *)
+ val probfile = prob_pathname subgoalno
+ val conj_pos = writer probfile clauses
+ val (proof, rc) = system_out (
+ if File.exists cmd then
+ space_implode " " ["exec", File.shell_path cmd, args, File.platform_path probfile]
+ else error ("Bad executable: " ^ Path.implode cmd))
+
+ (* if problemfile has not been exported, delete problemfile; otherwise export proof, too *)
+ val _ =
+ if destdir' = "" then File.rm probfile
+ else File.write (Path.explode (Path.implode probfile ^ "_proof")) proof
+
+ (* check for success and print out some information on failure *)
+ val failure = find_failure proof
+ val success = rc = 0 andalso is_none failure
+ val message =
+ if is_some failure then "External prover failed."
+ else if rc <> 0 then "External prover failed: " ^ proof
+ else "Try this command: " ^
+ produce_answer name (proof, thm_names, conj_pos, ctxt, th, subgoalno)
+ val _ = Output.debug (fn () => "Sledgehammer response (rc = " ^ string_of_int rc ^ "):\n" ^ proof)
+ in (success, message, proof, thm_names, the_filtered_clauses) end;
+
+
+
+(** common provers **)
+
+(* generic TPTP-based provers *)
+
+fun tptp_prover_opts_full max_new theory_const full command timeout ax_clauses fcls name n goal =
+ external_prover
+ (ResAtp.get_relevant max_new theory_const)
+ (ResAtp.prepare_clauses false)
+ (ResHolClause.tptp_write_file (AtpManager.get_full_types()))
+ command
+ ResReconstruct.find_failure
+ (if full then ResReconstruct.structured_proof else ResReconstruct.lemma_list false)
+ timeout ax_clauses fcls name n goal;
+
+(*arbitrary ATP with TPTP input/output and problemfile as last argument*)
+fun tptp_prover_opts max_new theory_const =
+ tptp_prover_opts_full max_new theory_const false;
+
+fun tptp_prover x = tptp_prover_opts 60 true x;
+
+(*for structured proofs: prover must support TSTP*)
+fun full_prover_opts max_new theory_const =
+ tptp_prover_opts_full max_new theory_const true;
+
+fun full_prover x = full_prover_opts 60 true x;
+
+
+(* Vampire *)
+
+(*NB: Vampire does not work without explicit timelimit*)
+
+fun vampire_opts max_new theory_const timeout = tptp_prover_opts
+ max_new theory_const
+ (Path.explode "$VAMPIRE_HOME/vampire",
+ ("--output_syntax tptp --mode casc -t " ^ string_of_int timeout))
+ timeout;
+
+val vampire = vampire_opts 60 false;
+
+fun vampire_opts_full max_new theory_const timeout = full_prover_opts
+ max_new theory_const
+ (Path.explode "$VAMPIRE_HOME/vampire",
+ ("--output_syntax tptp --mode casc -t " ^ string_of_int timeout))
+ timeout;
+
+val vampire_full = vampire_opts_full 60 false;
+
+
+(* E prover *)
+
+fun eprover_opts max_new theory_const timeout = tptp_prover_opts
+ max_new theory_const
+ (Path.explode "$E_HOME/eproof",
+ "--tstp-in --tstp-out -l5 -xAutoDev -tAutoDev --silent --cpu-limit=" ^ string_of_int timeout)
+ timeout;
+
+val eprover = eprover_opts 100 false;
+
+fun eprover_opts_full max_new theory_const timeout = full_prover_opts
+ max_new theory_const
+ (Path.explode "$E_HOME/eproof",
+ "--tstp-in --tstp-out -l5 -xAutoDev -tAutoDev --silent --cpu-limit=" ^ string_of_int timeout)
+ timeout;
+
+val eprover_full = eprover_opts_full 100 false;
+
+
+(* SPASS *)
+
+fun spass_opts max_new theory_const timeout ax_clauses fcls name n goal = external_prover
+ (ResAtp.get_relevant max_new theory_const)
+ (ResAtp.prepare_clauses true)
+ (ResHolClause.dfg_write_file (AtpManager.get_full_types()))
+ (Path.explode "$SPASS_HOME/SPASS",
+ "-Auto -SOS=1 -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof -TimeLimit=" ^
+ string_of_int timeout)
+ ResReconstruct.find_failure
+ (ResReconstruct.lemma_list true)
+ timeout ax_clauses fcls name n goal;
+
+val spass = spass_opts 40 true;
+
+
+(* remote prover invocation via SystemOnTPTP *)
+
+val systems =
+ Synchronized.var "atp_wrapper_systems" ([]: string list);
+
+fun get_systems () =
+ let
+ val (answer, rc) = system_out ("\"$ISABELLE_ATP_MANAGER/SystemOnTPTP\" -w")
+ in
+ if rc <> 0 then error ("Failed to get available systems from SystemOnTPTP:\n" ^ answer)
+ else split_lines answer
+ end;
+
+fun refresh_systems () = Synchronized.change systems (fn _ =>
+ get_systems ());
+
+fun get_system prefix = Synchronized.change_result systems (fn systems =>
+ let val systems = if null systems then get_systems() else systems
+ in (find_first (String.isPrefix prefix) systems, systems) end);
+
+fun remote_prover_opts max_new theory_const args prover_prefix timeout =
+ let val sys =
+ case get_system prover_prefix of
+ NONE => error ("No system like " ^ quote prover_prefix ^ " at SystemOnTPTP")
+ | SOME sys => sys
+ in tptp_prover_opts max_new theory_const
+ (Path.explode "$ISABELLE_ATP_MANAGER/SystemOnTPTP",
+ args ^ " -t " ^ string_of_int timeout ^ " -s " ^ sys) timeout
+ end;
+
+val remote_prover = remote_prover_opts 60 false;
+
+end;
+
--- a/src/HOL/Tools/atp_manager.ML Tue Aug 04 16:13:16 2009 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,403 +0,0 @@
-(* Title: HOL/Tools/atp_manager.ML
- Author: Fabian Immler, TU Muenchen
-
-ATP threads are registered here.
-Threads with the same birth-time are seen as one group.
-All threads of a group are killed when one thread of it has been successful,
-or after a certain time,
-or when the maximum number of threads exceeds; then the oldest thread is killed.
-*)
-
-signature ATP_MANAGER =
-sig
- val get_atps: unit -> string
- val set_atps: string -> unit
- val get_max_atps: unit -> int
- val set_max_atps: int -> unit
- val get_timeout: unit -> int
- val set_timeout: int -> unit
- val get_full_types: unit -> bool
- val set_full_types: bool -> unit
- val kill: unit -> unit
- val info: unit -> unit
- val messages: int option -> unit
- type prover = int -> (thm * (string * int)) list option ->
- (thm * (string * int)) list option -> string -> int ->
- Proof.context * (thm list * thm) ->
- bool * string * string * string vector * (thm * (string * int)) list
- val add_prover: string -> prover -> theory -> theory
- val print_provers: theory -> unit
- val get_prover: string -> theory -> prover option
- val sledgehammer: string list -> Proof.state -> unit
-end;
-
-structure AtpManager: ATP_MANAGER =
-struct
-
-(** preferences **)
-
-val message_store_limit = 20;
-val message_display_limit = 5;
-
-local
-
-val atps = ref "e remote_vampire";
-val max_atps = ref 5; (* ~1 means infinite number of atps *)
-val timeout = ref 60;
-val full_types = ref false;
-
-in
-
-fun get_atps () = CRITICAL (fn () => ! atps);
-fun set_atps str = CRITICAL (fn () => atps := str);
-
-fun get_max_atps () = CRITICAL (fn () => ! max_atps);
-fun set_max_atps number = CRITICAL (fn () => max_atps := number);
-
-fun get_timeout () = CRITICAL (fn () => ! timeout);
-fun set_timeout time = CRITICAL (fn () => timeout := time);
-
-fun get_full_types () = CRITICAL (fn () => ! full_types);
-fun set_full_types bool = CRITICAL (fn () => full_types := bool);
-
-val _ =
- ProofGeneralPgip.add_preference Preferences.category_proof
- (Preferences.string_pref atps
- "ATP: provers" "Default automatic provers (separated by whitespace)");
-
-val _ =
- ProofGeneralPgip.add_preference Preferences.category_proof
- (Preferences.int_pref max_atps
- "ATP: maximum number" "How many provers may run in parallel");
-
-val _ =
- ProofGeneralPgip.add_preference Preferences.category_proof
- (Preferences.int_pref timeout
- "ATP: timeout" "ATPs will be interrupted after this time (in seconds)");
-
-val _ =
- ProofGeneralPgip.add_preference Preferences.category_proof
- (Preferences.bool_pref full_types
- "ATP: full types" "ATPs will use full type information");
-
-end;
-
-
-
-(** thread management **)
-
-(* data structures over threads *)
-
-structure ThreadHeap = HeapFun
-(
- 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 *)
-
-datatype T = State of
- {managing_thread: Thread.thread option,
- timeout_heap: ThreadHeap.T,
- oldest_heap: ThreadHeap.T,
- active: (Thread.thread * (Time.time * Time.time * string)) list,
- cancelling: (Thread.thread * (Time.time * Time.time * string)) list,
- messages: string list,
- store: string list};
-
-fun make_state managing_thread timeout_heap oldest_heap active cancelling messages store =
- State {managing_thread = managing_thread, timeout_heap = timeout_heap, oldest_heap = oldest_heap,
- active = active, cancelling = cancelling, messages = messages, store = store};
-
-val state = Synchronized.var "atp_manager"
- (make_state NONE ThreadHeap.empty ThreadHeap.empty [] [] [] []);
-
-
-(* unregister thread *)
-
-fun unregister (success, message) thread = Synchronized.change state
- (fn state as State {managing_thread, timeout_heap, oldest_heap, active, cancelling, messages, store} =>
- (case lookup_thread active thread of
- SOME (birthtime, _, description) =>
- let
- val (group, active') =
- if success then List.partition (fn (_, (tb, _, _)) => tb = birthtime) active
- else List.partition (fn (th, _) => Thread.equal (th, thread)) active
-
- val now = Time.now ()
- val cancelling' =
- fold (fn (th, (tb, _, desc)) => update_thread (th, (tb, now, desc))) group cancelling
-
- val message' = description ^ "\n" ^ message ^
- (if length group <= 1 then ""
- else "\nInterrupted " ^ string_of_int (length group - 1) ^ " other group members")
- val store' = message' ::
- (if length store <= message_store_limit then store
- else #1 (chop message_store_limit store))
- in make_state
- managing_thread timeout_heap oldest_heap active' cancelling' (message' :: messages) store'
- end
- | NONE => state));
-
-
-(* kill excessive atp threads *)
-
-fun excessive_atps active =
- let val max = get_max_atps ()
- in length active > max andalso max > ~1 end;
-
-local
-
-fun kill_oldest () =
- let exception Unchanged in
- Synchronized.change_result state
- (fn State {managing_thread, timeout_heap, oldest_heap, active, cancelling, messages, store} =>
- if ThreadHeap.is_empty oldest_heap orelse not (excessive_atps active)
- then raise Unchanged
- else
- let val ((_, oldest_thread), oldest_heap') = ThreadHeap.min_elem oldest_heap
- in (oldest_thread,
- make_state managing_thread timeout_heap oldest_heap' active cancelling messages store) end)
- |> unregister (false, "Interrupted (maximum number of ATPs exceeded)")
- handle Unchanged => ()
- end;
-
-in
-
-fun kill_excessive () =
- let val State {active, ...} = Synchronized.value state
- in if excessive_atps active then (kill_oldest (); kill_excessive ()) else () end;
-
-end;
-
-fun print_new_messages () =
- let val to_print = Synchronized.change_result state
- (fn State {managing_thread, timeout_heap, oldest_heap, active, cancelling, messages, store} =>
- (messages, make_state managing_thread timeout_heap oldest_heap active cancelling [] store))
- in
- if null to_print then ()
- else priority ("Sledgehammer: " ^ space_implode "\n\n" to_print)
- end;
-
-
-(* start a watching thread -- only one may exist *)
-
-fun check_thread_manager () = Synchronized.change state
- (fn State {managing_thread, timeout_heap, oldest_heap, active, cancelling, messages, store} =>
- if (case managing_thread of SOME thread => Thread.isActive thread | NONE => false)
- then make_state managing_thread timeout_heap oldest_heap active cancelling messages store
- else let val managing_thread = SOME (SimpleThread.fork false (fn () =>
- let
- val min_wait_time = Time.fromMilliseconds 300
- val max_wait_time = Time.fromSeconds 10
-
- (* wait for next thread to cancel, or maximum*)
- fun time_limit (State {timeout_heap, ...}) =
- (case try ThreadHeap.min timeout_heap of
- NONE => SOME (Time.+ (Time.now (), max_wait_time))
- | SOME (time, _) => SOME time)
-
- (* action: find threads whose timeout is reached, and interrupt cancelling threads *)
- fun action (State {managing_thread, timeout_heap, oldest_heap, active, cancelling,
- messages, store}) =
- let val (timeout_threads, timeout_heap') =
- ThreadHeap.upto (Time.now (), Thread.self ()) timeout_heap
- in
- if null timeout_threads andalso null cancelling andalso not (excessive_atps active)
- then NONE
- else
- let
- val _ = List.app (SimpleThread.interrupt o #1) cancelling
- val cancelling' = filter (Thread.isActive o #1) cancelling
- val state' = make_state
- managing_thread timeout_heap' oldest_heap active cancelling' messages store
- in SOME (map #2 timeout_threads, state') end
- end
- in
- while Synchronized.change_result state
- (fn st as
- State {managing_thread, timeout_heap, oldest_heap, active, cancelling, messages, store} =>
- if (null active) andalso (null cancelling) andalso (null messages)
- then (false, make_state NONE timeout_heap oldest_heap active cancelling messages store)
- else (true, st))
- do
- (Synchronized.timed_access state time_limit action
- |> these
- |> List.app (unregister (false, "Interrupted (reached timeout)"));
- kill_excessive ();
- print_new_messages ();
- (*give threads time to respond to interrupt*)
- OS.Process.sleep min_wait_time)
- end))
- in make_state managing_thread timeout_heap oldest_heap active cancelling messages store end);
-
-
-(* thread is registered here by sledgehammer *)
-
-fun register birthtime deadtime (thread, desc) =
- (Synchronized.change state
- (fn State {managing_thread, timeout_heap, oldest_heap, active, cancelling, messages, store} =>
- let
- val timeout_heap' = ThreadHeap.insert (deadtime, thread) timeout_heap
- val oldest_heap' = ThreadHeap.insert (birthtime, thread) oldest_heap
- val active' = update_thread (thread, (birthtime, deadtime, desc)) active
- in make_state managing_thread timeout_heap' oldest_heap' active' cancelling messages store end);
- check_thread_manager ());
-
-
-
-(** user commands **)
-
-(* kill: move all threads to cancelling *)
-
-fun kill () = Synchronized.change state
- (fn State {managing_thread, timeout_heap, oldest_heap, active, cancelling, messages, store} =>
- let val formerly_active = map (fn (th, (tb, _, desc)) => (th, (tb, Time.now (), desc))) active
- in make_state
- managing_thread timeout_heap oldest_heap [] (formerly_active @ cancelling) messages store
- end);
-
-
-(* ATP info *)
-
-fun info () =
- let
- val State {active, cancelling, ...} = Synchronized.value state
-
- fun running_info (_, (birth_time, dead_time, desc)) = "Running: "
- ^ (string_of_int o Time.toSeconds) (Time.- (Time.now (), birth_time))
- ^ " s -- "
- ^ (string_of_int o Time.toSeconds) (Time.- (dead_time, Time.now ()))
- ^ " s to live:\n" ^ desc
- fun cancelling_info (_, (_, dead_time, desc)) = "Trying to interrupt thread since "
- ^ (string_of_int o Time.toSeconds) (Time.- (Time.now (), dead_time))
- ^ " s:\n" ^ desc
-
- val running =
- if null active then "No ATPs running."
- else space_implode "\n\n" ("Running ATPs:" :: map running_info active)
- val interrupting =
- if null cancelling then ""
- else space_implode "\n\n"
- ("Trying to interrupt the following ATPs:" :: map cancelling_info cancelling)
-
- in writeln (running ^ "\n" ^ interrupting) end;
-
-fun messages opt_limit =
- let
- val limit = the_default message_display_limit opt_limit;
- val State {store = msgs, ...} = Synchronized.value state
- val header = "Recent ATP messages" ^
- (if length msgs <= limit then ":" else " (" ^ string_of_int limit ^ " displayed):");
- in writeln (space_implode "\n\n" (header :: #1 (chop limit msgs))) end;
-
-
-
-(** The Sledgehammer **)
-
-(* named provers *)
-
-type prover = int -> (thm * (string * int)) list option ->
- (thm * (string * int)) list option -> string -> int ->
- Proof.context * (thm list * thm) ->
- bool * string * string * string vector * (thm * (string * int)) list
-
-fun err_dup_prover name = error ("Duplicate prover: " ^ quote name);
-
-structure Provers = TheoryDataFun
-(
- type T = (prover * stamp) Symtab.table
- val empty = Symtab.empty
- val copy = I
- val extend = I
- fun merge _ tabs : T = Symtab.merge (eq_snd op =) tabs
- handle Symtab.DUP dup => err_dup_prover dup
-);
-
-fun add_prover name prover thy =
- Provers.map (Symtab.update_new (name, (prover, stamp ()))) thy
- handle Symtab.DUP dup => err_dup_prover dup;
-
-fun print_provers thy = Pretty.writeln
- (Pretty.strs ("external provers:" :: sort_strings (Symtab.keys (Provers.get thy))));
-
-fun get_prover name thy = case Symtab.lookup (Provers.get thy) name of
- NONE => NONE
-| SOME (prover, _) => SOME prover;
-
-(* start prover thread *)
-
-fun start_prover name birthtime deadtime i proof_state =
- (case get_prover name (Proof.theory_of proof_state) of
- NONE => warning ("Unknown external prover: " ^ quote name)
- | SOME prover =>
- let
- val (ctxt, (_, goal)) = Proof.get_goal proof_state
- val desc =
- "external prover " ^ quote name ^ " for subgoal " ^ string_of_int i ^ ":\n" ^
- Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i))
- val _ = SimpleThread.fork true (fn () =>
- let
- val _ = register birthtime deadtime (Thread.self (), desc)
- val result =
- let val (success, message, _, _, _) =
- prover (get_timeout ()) NONE NONE name i (Proof.get_goal proof_state)
- in (success, message) end
- handle ResHolClause.TOO_TRIVIAL
- => (true, "Empty clause: Try this command: " ^ Markup.markup Markup.sendback "apply metis")
- | ERROR msg
- => (false, "Error: " ^ msg)
- val _ = unregister result (Thread.self ())
- in () end handle Interrupt => ())
- in () end);
-
-
-(* sledghammer for first subgoal *)
-
-fun sledgehammer names proof_state =
- let
- val provers =
- if null names then String.tokens (Symbol.is_ascii_blank o String.str) (get_atps ())
- else names
- val birthtime = Time.now ()
- val deadtime = Time.+ (birthtime, Time.fromSeconds (get_timeout ()))
- in List.app (fn name => start_prover name birthtime deadtime 1 proof_state) provers end;
-
-
-
-(** Isar command syntax **)
-
-local structure K = OuterKeyword and P = OuterParse in
-
-val _ =
- OuterSyntax.improper_command "atp_kill" "kill all managed provers" K.diag
- (Scan.succeed (Toplevel.no_timing o Toplevel.imperative kill));
-
-val _ =
- OuterSyntax.improper_command "atp_info" "print information about managed provers" K.diag
- (Scan.succeed (Toplevel.no_timing o Toplevel.imperative info));
-
-val _ =
- OuterSyntax.improper_command "atp_messages" "print recent messages issued by managed provers" K.diag
- (Scan.option (P.$$$ "(" |-- P.nat --| P.$$$ ")") >>
- (fn limit => Toplevel.no_timing o Toplevel.imperative (fn () => messages limit)));
-
-val _ =
- OuterSyntax.improper_command "print_atps" "print external provers" K.diag
- (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_theory o
- Toplevel.keep (print_provers o Toplevel.theory_of)));
-
-val _ =
- OuterSyntax.command "sledgehammer" "call all automatic theorem provers" K.diag
- (Scan.repeat P.xname >> (fn names => Toplevel.no_timing o Toplevel.unknown_proof o
- Toplevel.keep (sledgehammer names o Toplevel.proof_of)));
-
-end;
-
-end;
-
--- a/src/HOL/Tools/atp_minimal.ML Tue Aug 04 16:13:16 2009 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,223 +0,0 @@
-(* Title: HOL/Tools/atp_minimal.ML
- Author: Philipp Meyer, TU Muenchen
-
-Minimalization of theorem list for metis by using an external automated theorem prover
-*)
-
-structure AtpMinimal: sig end =
-struct
-
-(* output control *)
-
-fun debug str = Output.debug (fn () => str)
-fun debug_fn f = if ! Output.debugging then f () else ()
-fun answer str = Output.writeln str
-fun println str = Output.priority str
-
-fun order_unique name_list = OrdList.make (String.collate Char.compare) name_list
-fun length_string namelist = Int.toString (length namelist)
-
-fun print_names name_thms_pairs =
- let
- val names = map fst name_thms_pairs
- val ordered = order_unique names
- in
- app (fn name => (debug (" " ^ name))) ordered
- end
-
-
-(* minimalization algorithm *)
-
-local
- fun isplit (l,r) [] = (l,r)
- | isplit (l,r) (h::[]) = (h::l, r)
- | isplit (l,r) (h1::h2::t) = isplit (h1::l, h2::r) t
-in
- fun split lst = isplit ([],[]) lst
-end
-
-local
- fun min p sup [] = raise Empty
- | min p sup [s0] = [s0]
- | min p sup s =
- let
- val (l0, r0) = split s
- in
- if p (sup @ l0)
- then min p sup l0
- else
- if p (sup @ r0)
- then min p sup r0
- else
- let
- val l = min p (sup @ r0) l0
- val r = min p (sup @ l) r0
- in
- l @ r
- end
- end
-in
- (* return a minimal subset v of s that satisfies p
- @pre p(s) & ~p([]) & monotone(p)
- @post v subset s & p(v) &
- forall e in v. ~p(v \ e)
- *)
- fun minimal p s = min p [] s
-end
-
-
-(* failure check and producing answer *)
-
-datatype 'a prove_result = Success of 'a | Failure | Timeout | Error
-
-val string_of_result =
- fn Success _ => "Success"
- | Failure => "Failure"
- | Timeout => "Timeout"
- | Error => "Error"
-
-val failure_strings =
- [("SPASS beiseite: Ran out of time.", Timeout),
- ("Timeout", Timeout),
- ("time limit exceeded", Timeout),
- ("# Cannot determine problem status within resource limit", Timeout),
- ("Error", Error)]
-
-fun produce_answer (success, message, result_string, thm_name_vec, filtered) =
- if success then
- (Success (Vector.foldr op:: [] thm_name_vec, filtered), result_string)
- else
- let
- val failure = failure_strings |> get_first (fn (s, t) =>
- if String.isSubstring s result_string then SOME (t, result_string) else NONE)
- in
- if is_some failure then
- the failure
- else
- (Failure, result_string)
- end
-
-
-(* wrapper for calling external prover *)
-
-fun sh_test_thms prover prover_name time_limit subgoalno state filtered name_thms_pairs =
- let
- val _ = println ("Testing " ^ (length_string name_thms_pairs) ^ " theorems... ")
- val name_thm_pairs =
- flat (map (fn (n, ths) => map_index (fn (i, th) => (n, th)) ths) name_thms_pairs)
- val _ = debug_fn (fn () => print_names name_thm_pairs)
- val axclauses = ResAxioms.cnf_rules_pairs (Proof.theory_of state) name_thm_pairs
- val (result, proof) =
- produce_answer
- (prover time_limit (SOME axclauses) filtered prover_name subgoalno (Proof.get_goal state))
- val _ = println (string_of_result result)
- val _ = debug proof
- in
- (result, proof)
- end
-
-
-(* minimalization of thms *)
-
-fun minimalize prover prover_name time_limit state name_thms_pairs =
- let
- val _ =
- println ("Minimize called with " ^ length_string name_thms_pairs ^ " theorems, prover: "
- ^ prover_name ^ ", time limit: " ^ Int.toString time_limit ^ " seconds")
- val _ = debug_fn (fn () => app (fn (n, tl) =>
- (debug n; app (fn t =>
- debug (" " ^ Display.string_of_thm (Proof.context_of state) t)) tl)) name_thms_pairs)
- val test_thms_fun = sh_test_thms prover prover_name time_limit 1 state
- fun test_thms filtered thms =
- case test_thms_fun filtered thms of (Success _, _) => true | _ => false
- in
- (* try prove first to check result and get used theorems *)
- (case test_thms_fun NONE name_thms_pairs of
- (Success (used, filtered), _) =>
- let
- val ordered_used = order_unique used
- val to_use =
- if length ordered_used < length name_thms_pairs then
- filter (fn (name1, _) => List.exists (equal name1) ordered_used) name_thms_pairs
- else
- name_thms_pairs
- val min_thms = (minimal (test_thms (SOME filtered)) to_use)
- val min_names = order_unique (map fst min_thms)
- val _ = println ("Minimal " ^ (length_string min_thms) ^ " theorems")
- val _ = debug_fn (fn () => print_names min_thms)
- in
- answer ("Try this command: " ^
- Markup.markup Markup.sendback ("apply (metis " ^ space_implode " " min_names ^ ")"))
- end
- | (Timeout, _) =>
- answer ("Timeout: You may need to increase the time limit of " ^
- Int.toString time_limit ^ " seconds. Call atp_minimize [time=...] ")
- | (Error, msg) =>
- answer ("Error in prover: " ^ msg)
- | (Failure, _) =>
- answer "Failure: No proof with the theorems supplied")
- handle ResHolClause.TOO_TRIVIAL =>
- answer ("Trivial: Try this command: " ^ Markup.markup Markup.sendback "apply metis")
- | ERROR msg =>
- answer ("Error: " ^ msg)
- end
-
-
-(* Isar command and parsing input *)
-
-local structure K = OuterKeyword and P = OuterParse and T = OuterLex in
-
-fun get_thms context =
- map (fn (name, interval) =>
- let
- val thmref = Facts.Named ((name, Position.none), interval)
- val ths = ProofContext.get_fact context thmref
- val name' = Facts.string_of_ref thmref
- in
- (name', ths)
- end)
-
-val default_prover = "remote_vampire"
-val default_time_limit = 5
-
-fun get_time_limit_arg time_string =
- (case Int.fromString time_string of
- SOME t => t
- | NONE => error ("Invalid time limit: " ^ quote time_string))
-
-val get_options =
- let
- val def = (default_prover, default_time_limit)
- in
- foldl (fn ((name, a), (p, t)) =>
- (case name of
- "time" => (p, (get_time_limit_arg a))
- | "atp" => (a, t)
- | n => error ("Invalid argument: " ^ n))) def
- end
-
-fun sh_min_command args thm_names state =
- let
- val (prover_name, time_limit) = get_options args
- val prover =
- case AtpManager.get_prover prover_name (Proof.theory_of state) of
- SOME prover => prover
- | NONE => error ("Unknown prover: " ^ quote prover_name)
- val name_thms_pairs = get_thms (Proof.context_of state) thm_names
- in
- minimalize prover prover_name time_limit state name_thms_pairs
- end
-
-val parse_args = Scan.optional (Args.bracks (P.list (P.xname --| P.$$$ "=" -- P.xname))) []
-val parse_thm_names = Scan.repeat (P.xname -- Scan.option Attrib.thm_sel)
-
-val _ =
- OuterSyntax.command "atp_minimize" "minimize theorem list with external prover" K.diag
- (parse_args -- parse_thm_names >> (fn (args, thm_names) =>
- Toplevel.no_timing o Toplevel.unknown_proof o
- Toplevel.keep (sh_min_command args thm_names o Toplevel.proof_of)))
-
-end
-
-end
-
--- a/src/HOL/Tools/atp_wrapper.ML Tue Aug 04 16:13:16 2009 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,218 +0,0 @@
-(* Title: HOL/Tools/atp_wrapper.ML
- Author: Fabian Immler, TU Muenchen
-
-Wrapper functions for external ATPs.
-*)
-
-signature ATP_WRAPPER =
-sig
- val destdir: string ref
- val problem_name: string ref
- val tptp_prover_opts_full: int -> bool -> bool -> Path.T * string -> AtpManager.prover
- val tptp_prover_opts: int -> bool -> Path.T * string -> AtpManager.prover
- val tptp_prover: Path.T * string -> AtpManager.prover
- val full_prover_opts: int -> bool -> Path.T * string -> AtpManager.prover
- val full_prover: Path.T * string -> AtpManager.prover
- val vampire_opts: int -> bool -> AtpManager.prover
- val vampire: AtpManager.prover
- val vampire_opts_full: int -> bool -> AtpManager.prover
- val vampire_full: AtpManager.prover
- val eprover_opts: int -> bool -> AtpManager.prover
- val eprover: AtpManager.prover
- val eprover_opts_full: int -> bool -> AtpManager.prover
- val eprover_full: AtpManager.prover
- val spass_opts: int -> bool -> AtpManager.prover
- val spass: AtpManager.prover
- val remote_prover_opts: int -> bool -> string -> string -> AtpManager.prover
- val remote_prover: string -> string -> AtpManager.prover
- val refresh_systems: unit -> unit
-end;
-
-structure AtpWrapper: ATP_WRAPPER =
-struct
-
-(** generic ATP wrapper **)
-
-(* global hooks for writing problemfiles *)
-
-val destdir = ref ""; (*Empty means write files to /tmp*)
-val problem_name = ref "prob";
-
-
-(* basic template *)
-
-fun external_prover relevance_filter preparer writer (cmd, args) find_failure produce_answer
- timeout axiom_clauses filtered_clauses name subgoalno goal =
- let
- (* path to unique problem file *)
- val destdir' = ! destdir
- val problem_name' = ! problem_name
- fun prob_pathname nr =
- let val probfile = Path.basic (problem_name' ^ serial_string () ^ "_" ^ string_of_int nr)
- in if destdir' = "" then File.tmp_path probfile
- else if File.exists (Path.explode (destdir'))
- then Path.append (Path.explode (destdir')) probfile
- else error ("No such directory: " ^ destdir')
- end
-
- (* get clauses and prepare them for writing *)
- val (ctxt, (chain_ths, th)) = goal
- val thy = ProofContext.theory_of ctxt
- val chain_ths = map (Thm.put_name_hint ResReconstruct.chained_hint) chain_ths
- val goal_cls = #1 (ResAxioms.neg_conjecture_clauses ctxt th subgoalno)
- val _ = app (fn th => Output.debug (fn _ => Display.string_of_thm ctxt th)) goal_cls
- val the_filtered_clauses =
- case filtered_clauses of
- NONE => relevance_filter goal goal_cls
- | SOME fcls => fcls
- val the_axiom_clauses =
- case axiom_clauses of
- NONE => the_filtered_clauses
- | SOME axcls => axcls
- val (thm_names, clauses) =
- preparer goal_cls chain_ths the_axiom_clauses the_filtered_clauses thy
-
- (* write out problem file and call prover *)
- val probfile = prob_pathname subgoalno
- val conj_pos = writer probfile clauses
- val (proof, rc) = system_out (
- if File.exists cmd then
- space_implode " " ["exec", File.shell_path cmd, args, File.platform_path probfile]
- else error ("Bad executable: " ^ Path.implode cmd))
-
- (* if problemfile has not been exported, delete problemfile; otherwise export proof, too *)
- val _ =
- if destdir' = "" then File.rm probfile
- else File.write (Path.explode (Path.implode probfile ^ "_proof")) proof
-
- (* check for success and print out some information on failure *)
- val failure = find_failure proof
- val success = rc = 0 andalso is_none failure
- val message =
- if is_some failure then "External prover failed."
- else if rc <> 0 then "External prover failed: " ^ proof
- else "Try this command: " ^
- produce_answer name (proof, thm_names, conj_pos, ctxt, th, subgoalno)
- val _ = Output.debug (fn () => "Sledgehammer response (rc = " ^ string_of_int rc ^ "):\n" ^ proof)
- in (success, message, proof, thm_names, the_filtered_clauses) end;
-
-
-
-(** common provers **)
-
-(* generic TPTP-based provers *)
-
-fun tptp_prover_opts_full max_new theory_const full command timeout ax_clauses fcls name n goal =
- external_prover
- (ResAtp.get_relevant max_new theory_const)
- (ResAtp.prepare_clauses false)
- (ResHolClause.tptp_write_file (AtpManager.get_full_types()))
- command
- ResReconstruct.find_failure
- (if full then ResReconstruct.structured_proof else ResReconstruct.lemma_list false)
- timeout ax_clauses fcls name n goal;
-
-(*arbitrary ATP with TPTP input/output and problemfile as last argument*)
-fun tptp_prover_opts max_new theory_const =
- tptp_prover_opts_full max_new theory_const false;
-
-fun tptp_prover x = tptp_prover_opts 60 true x;
-
-(*for structured proofs: prover must support TSTP*)
-fun full_prover_opts max_new theory_const =
- tptp_prover_opts_full max_new theory_const true;
-
-fun full_prover x = full_prover_opts 60 true x;
-
-
-(* Vampire *)
-
-(*NB: Vampire does not work without explicit timelimit*)
-
-fun vampire_opts max_new theory_const timeout = tptp_prover_opts
- max_new theory_const
- (Path.explode "$VAMPIRE_HOME/vampire",
- ("--output_syntax tptp --mode casc -t " ^ string_of_int timeout))
- timeout;
-
-val vampire = vampire_opts 60 false;
-
-fun vampire_opts_full max_new theory_const timeout = full_prover_opts
- max_new theory_const
- (Path.explode "$VAMPIRE_HOME/vampire",
- ("--output_syntax tptp --mode casc -t " ^ string_of_int timeout))
- timeout;
-
-val vampire_full = vampire_opts_full 60 false;
-
-
-(* E prover *)
-
-fun eprover_opts max_new theory_const timeout = tptp_prover_opts
- max_new theory_const
- (Path.explode "$E_HOME/eproof",
- "--tstp-in --tstp-out -l5 -xAutoDev -tAutoDev --silent --cpu-limit=" ^ string_of_int timeout)
- timeout;
-
-val eprover = eprover_opts 100 false;
-
-fun eprover_opts_full max_new theory_const timeout = full_prover_opts
- max_new theory_const
- (Path.explode "$E_HOME/eproof",
- "--tstp-in --tstp-out -l5 -xAutoDev -tAutoDev --silent --cpu-limit=" ^ string_of_int timeout)
- timeout;
-
-val eprover_full = eprover_opts_full 100 false;
-
-
-(* SPASS *)
-
-fun spass_opts max_new theory_const timeout ax_clauses fcls name n goal = external_prover
- (ResAtp.get_relevant max_new theory_const)
- (ResAtp.prepare_clauses true)
- (ResHolClause.dfg_write_file (AtpManager.get_full_types()))
- (Path.explode "$SPASS_HOME/SPASS",
- "-Auto -SOS=1 -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof -TimeLimit=" ^
- string_of_int timeout)
- ResReconstruct.find_failure
- (ResReconstruct.lemma_list true)
- timeout ax_clauses fcls name n goal;
-
-val spass = spass_opts 40 true;
-
-
-(* remote prover invocation via SystemOnTPTP *)
-
-val systems =
- Synchronized.var "atp_wrapper_systems" ([]: string list);
-
-fun get_systems () =
- let
- val (answer, rc) = system_out (("$ISABELLE_HOME/lib/scripts/SystemOnTPTP" |>
- Path.explode |> File.shell_path) ^ " -w")
- in
- if rc <> 0 then error ("Get available systems from SystemOnTPTP:\n" ^ answer)
- else split_lines answer
- end;
-
-fun refresh_systems () = Synchronized.change systems (fn _ =>
- get_systems ());
-
-fun get_system prefix = Synchronized.change_result systems (fn systems =>
- let val systems = if null systems then get_systems() else systems
- in (find_first (String.isPrefix prefix) systems, systems) end);
-
-fun remote_prover_opts max_new theory_const args prover_prefix timeout =
- let val sys =
- case get_system prover_prefix of
- NONE => error ("No system like " ^ quote prover_prefix ^ " at SystemOnTPTP")
- | SOME sys => sys
- in tptp_prover_opts max_new theory_const
- (Path.explode "$ISABELLE_HOME/lib/scripts/SystemOnTPTP",
- args ^ " -t " ^ string_of_int timeout ^ " -s " ^ sys) timeout
- end;
-
-val remote_prover = remote_prover_opts 60 false;
-
-end;
-