src/HOL/Tools/ATP_Manager as separate component, with (almost) everything in one place;
1.1 --- a/etc/components Tue Aug 04 16:13:16 2009 +0200
1.2 +++ b/etc/components Tue Aug 04 19:20:24 2009 +0200
1.3 @@ -1,3 +1,4 @@
1.4 +#main object logics
1.5 src/Pure
1.6 src/FOL
1.7 src/HOL
1.8 @@ -9,3 +10,6 @@
1.9 src/HOLCF
1.10 src/LCF
1.11 src/Sequents
1.12 +#misc components
1.13 +src/HOL/Tools/ATP_Manager
1.14 +
2.1 --- a/lib/scripts/SystemOnTPTP Tue Aug 04 16:13:16 2009 +0200
2.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
2.3 @@ -1,141 +0,0 @@
2.4 -#!/usr/bin/env perl
2.5 -#
2.6 -# Wrapper for custom remote provers on SystemOnTPTP
2.7 -# Author: Fabian Immler, TU Muenchen
2.8 -#
2.9 -
2.10 -use warnings;
2.11 -use strict;
2.12 -use Getopt::Std;
2.13 -use HTTP::Request::Common;
2.14 -use LWP;
2.15 -
2.16 -my $SystemOnTPTPFormReplyURL =
2.17 - "http://www.cs.miami.edu/~tptp/cgi-bin/SystemOnTPTPFormReply";
2.18 -
2.19 -# default parameters
2.20 -my %URLParameters = (
2.21 - "NoHTML" => 1,
2.22 - "QuietFlag" => "-q01",
2.23 - "SubmitButton" => "RunSelectedSystems",
2.24 - "ProblemSource" => "UPLOAD",
2.25 - );
2.26 -
2.27 -#----Get format and transform options if specified
2.28 -my %Options;
2.29 -getopts("hwxs:t:c:",\%Options);
2.30 -
2.31 -#----Usage
2.32 -sub usage() {
2.33 - print("Usage: remote [<options>] <File name>\n");
2.34 - print(" <options> are ...\n");
2.35 - print(" -h - print this help\n");
2.36 - print(" -w - list available ATP systems\n");
2.37 - print(" -x - use X2TPTP to convert output of prover\n");
2.38 - print(" -s<system> - specified system to use\n");
2.39 - print(" -t<timelimit> - CPU time limit for system\n");
2.40 - print(" -c<command> - custom command for system\n");
2.41 - print(" <File name> - TPTP problem file\n");
2.42 - exit(0);
2.43 -}
2.44 -if (exists($Options{'h'})) {
2.45 - usage();
2.46 -}
2.47 -
2.48 -#----What systems flag
2.49 -if (exists($Options{'w'})) {
2.50 - $URLParameters{"SubmitButton"} = "ListSystems";
2.51 - delete($URLParameters{"ProblemSource"});
2.52 -}
2.53 -
2.54 -#----X2TPTP
2.55 -if (exists($Options{'x'})) {
2.56 - $URLParameters{"X2TPTP"} = "-S";
2.57 -}
2.58 -
2.59 -#----Selected system
2.60 -my $System;
2.61 -if (exists($Options{'s'})) {
2.62 - $System = $Options{'s'};
2.63 -} else {
2.64 - # use Vampire as default
2.65 - $System = "Vampire---9.0";
2.66 -}
2.67 -$URLParameters{"System___$System"} = $System;
2.68 -
2.69 -#----Time limit
2.70 -if (exists($Options{'t'})) {
2.71 - $URLParameters{"TimeLimit___$System"} = $Options{'t'};
2.72 -}
2.73 -#----Custom command
2.74 -if (exists($Options{'c'})) {
2.75 - $URLParameters{"Command___$System"} = $Options{'c'};
2.76 -}
2.77 -
2.78 -#----Get single file name
2.79 -if (exists($URLParameters{"ProblemSource"})) {
2.80 - if (scalar(@ARGV) >= 1) {
2.81 - $URLParameters{"UPLOADProblem"} = [shift(@ARGV)];
2.82 - } else {
2.83 - print("Missing problem file\n");
2.84 - usage();
2.85 - die;
2.86 - }
2.87 -}
2.88 -
2.89 -# Query Server
2.90 -my $Agent = LWP::UserAgent->new;
2.91 -if (exists($Options{'t'})) {
2.92 - # give server more time to respond
2.93 - $Agent->timeout($Options{'t'} + 10);
2.94 -}
2.95 -my $Request = POST($SystemOnTPTPFormReplyURL,
2.96 - Content_Type => 'form-data',Content => \%URLParameters);
2.97 -my $Response = $Agent->request($Request);
2.98 -
2.99 -#catch errors / failure
2.100 -if(!$Response->is_success) {
2.101 - print "HTTP-Error: " . $Response->message . "\n";
2.102 - exit(-1);
2.103 -} elsif (exists($Options{'w'})) {
2.104 - print $Response->content;
2.105 - exit (0);
2.106 -} elsif ($Response->content =~ /WARNING: (\S*) does not exist/) {
2.107 - print "Specified System $1 does not exist\n";
2.108 - exit(-1);
2.109 -} elsif (exists($Options{'x'}) &&
2.110 - $Response->content =~
2.111 - /%\s*Result\s*:\s*Unsatisfiable.*\n%\s*Output\s*:\s*(CNF)?Refutation.*\n%/ &&
2.112 - $Response->content !~ /ERROR: Could not form TPTP format derivation/ )
2.113 -{
2.114 - # converted output: extract proof
2.115 - my @lines = split( /\n/, $Response->content);
2.116 - my $extract = "";
2.117 - foreach my $line (@lines){
2.118 - #ignore comments
2.119 - if ($line !~ /^%/ && !($line eq "")) {
2.120 - $extract .= "$line";
2.121 - }
2.122 - }
2.123 - # insert newlines after ').'
2.124 - $extract =~ s/\s//g;
2.125 - $extract =~ s/\)\.cnf/\)\.\ncnf/g;
2.126 -
2.127 - print "========== ~~/lib/scripts/SystemOnTPTP extracted proof: ==========\n";
2.128 - # orientation for res_reconstruct.ML
2.129 - print "# SZS output start CNFRefutation.\n";
2.130 - print "$extract\n";
2.131 - print "# SZS output end CNFRefutation.\n";
2.132 - # can be useful for debugging; Isabelle ignores this
2.133 - print "============== original response from SystemOnTPTP: ==============\n";
2.134 - print $Response->content;
2.135 - exit(0);
2.136 -} elsif (!exists($Options{'x'})) {
2.137 - # pass output directly to Isabelle
2.138 - print $Response->content;
2.139 - exit(0);
2.140 -}else {
2.141 - print "Remote-script could not extract proof:\n".$Response->content;
2.142 - exit(-1);
2.143 -}
2.144 -
3.1 --- a/src/HOL/ATP_Linkup.thy Tue Aug 04 16:13:16 2009 +0200
3.2 +++ b/src/HOL/ATP_Linkup.thy Tue Aug 04 19:20:24 2009 +0200
3.3 @@ -15,9 +15,9 @@
3.4 ("Tools/res_hol_clause.ML")
3.5 ("Tools/res_reconstruct.ML")
3.6 ("Tools/res_atp.ML")
3.7 - ("Tools/atp_manager.ML")
3.8 - ("Tools/atp_wrapper.ML")
3.9 - ("Tools/atp_minimal.ML")
3.10 + ("Tools/ATP_Manager/atp_manager.ML")
3.11 + ("Tools/ATP_Manager/atp_wrapper.ML")
3.12 + ("Tools/ATP_Manager/atp_minimal.ML")
3.13 "~~/src/Tools/Metis/metis.ML"
3.14 ("Tools/metis_tools.ML")
3.15 begin
3.16 @@ -96,10 +96,9 @@
3.17 use "Tools/res_reconstruct.ML" setup ResReconstruct.setup
3.18 use "Tools/res_atp.ML"
3.19
3.20 -use "Tools/atp_manager.ML"
3.21 -use "Tools/atp_wrapper.ML"
3.22 -
3.23 -use "Tools/atp_minimal.ML"
3.24 +use "Tools/ATP_Manager/atp_manager.ML"
3.25 +use "Tools/ATP_Manager/atp_wrapper.ML"
3.26 +use "Tools/ATP_Manager/atp_minimal.ML"
3.27
3.28 text {* basic provers *}
3.29 setup {* AtpManager.add_prover "spass" AtpWrapper.spass *}
4.1 --- a/src/HOL/IsaMakefile Tue Aug 04 16:13:16 2009 +0200
4.2 +++ b/src/HOL/IsaMakefile Tue Aug 04 19:20:24 2009 +0200
4.3 @@ -231,12 +231,13 @@
4.4 $(SRC)/Provers/Arith/combine_numerals.ML \
4.5 $(SRC)/Provers/Arith/extract_common_term.ML \
4.6 $(SRC)/Tools/Metis/metis.ML \
4.7 + Tools/ATP_Manager/atp_manager.ML \
4.8 + Tools/ATP_Manager/atp_minimal.ML \
4.9 + Tools/ATP_Manager/atp_wrapper.ML \
4.10 Tools/Groebner_Basis/groebner.ML \
4.11 Tools/Groebner_Basis/misc.ML \
4.12 + Tools/Groebner_Basis/normalizer.ML \
4.13 Tools/Groebner_Basis/normalizer_data.ML \
4.14 - Tools/Groebner_Basis/normalizer.ML \
4.15 - Tools/atp_manager.ML \
4.16 - Tools/atp_wrapper.ML \
4.17 Tools/int_arith.ML \
4.18 Tools/list_code.ML \
4.19 Tools/meson.ML \
5.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
5.2 +++ b/src/HOL/Tools/ATP_Manager/SystemOnTPTP Tue Aug 04 19:20:24 2009 +0200
5.3 @@ -0,0 +1,141 @@
5.4 +#!/usr/bin/env perl
5.5 +#
5.6 +# Wrapper for custom remote provers on SystemOnTPTP
5.7 +# Author: Fabian Immler, TU Muenchen
5.8 +#
5.9 +
5.10 +use warnings;
5.11 +use strict;
5.12 +use Getopt::Std;
5.13 +use HTTP::Request::Common;
5.14 +use LWP;
5.15 +
5.16 +my $SystemOnTPTPFormReplyURL =
5.17 + "http://www.cs.miami.edu/~tptp/cgi-bin/SystemOnTPTPFormReply";
5.18 +
5.19 +# default parameters
5.20 +my %URLParameters = (
5.21 + "NoHTML" => 1,
5.22 + "QuietFlag" => "-q01",
5.23 + "SubmitButton" => "RunSelectedSystems",
5.24 + "ProblemSource" => "UPLOAD",
5.25 + );
5.26 +
5.27 +#----Get format and transform options if specified
5.28 +my %Options;
5.29 +getopts("hwxs:t:c:",\%Options);
5.30 +
5.31 +#----Usage
5.32 +sub usage() {
5.33 + print("Usage: remote [<options>] <File name>\n");
5.34 + print(" <options> are ...\n");
5.35 + print(" -h - print this help\n");
5.36 + print(" -w - list available ATP systems\n");
5.37 + print(" -x - use X2TPTP to convert output of prover\n");
5.38 + print(" -s<system> - specified system to use\n");
5.39 + print(" -t<timelimit> - CPU time limit for system\n");
5.40 + print(" -c<command> - custom command for system\n");
5.41 + print(" <File name> - TPTP problem file\n");
5.42 + exit(0);
5.43 +}
5.44 +if (exists($Options{'h'})) {
5.45 + usage();
5.46 +}
5.47 +
5.48 +#----What systems flag
5.49 +if (exists($Options{'w'})) {
5.50 + $URLParameters{"SubmitButton"} = "ListSystems";
5.51 + delete($URLParameters{"ProblemSource"});
5.52 +}
5.53 +
5.54 +#----X2TPTP
5.55 +if (exists($Options{'x'})) {
5.56 + $URLParameters{"X2TPTP"} = "-S";
5.57 +}
5.58 +
5.59 +#----Selected system
5.60 +my $System;
5.61 +if (exists($Options{'s'})) {
5.62 + $System = $Options{'s'};
5.63 +} else {
5.64 + # use Vampire as default
5.65 + $System = "Vampire---9.0";
5.66 +}
5.67 +$URLParameters{"System___$System"} = $System;
5.68 +
5.69 +#----Time limit
5.70 +if (exists($Options{'t'})) {
5.71 + $URLParameters{"TimeLimit___$System"} = $Options{'t'};
5.72 +}
5.73 +#----Custom command
5.74 +if (exists($Options{'c'})) {
5.75 + $URLParameters{"Command___$System"} = $Options{'c'};
5.76 +}
5.77 +
5.78 +#----Get single file name
5.79 +if (exists($URLParameters{"ProblemSource"})) {
5.80 + if (scalar(@ARGV) >= 1) {
5.81 + $URLParameters{"UPLOADProblem"} = [shift(@ARGV)];
5.82 + } else {
5.83 + print("Missing problem file\n");
5.84 + usage();
5.85 + die;
5.86 + }
5.87 +}
5.88 +
5.89 +# Query Server
5.90 +my $Agent = LWP::UserAgent->new;
5.91 +if (exists($Options{'t'})) {
5.92 + # give server more time to respond
5.93 + $Agent->timeout($Options{'t'} + 10);
5.94 +}
5.95 +my $Request = POST($SystemOnTPTPFormReplyURL,
5.96 + Content_Type => 'form-data',Content => \%URLParameters);
5.97 +my $Response = $Agent->request($Request);
5.98 +
5.99 +#catch errors / failure
5.100 +if(!$Response->is_success) {
5.101 + print "HTTP-Error: " . $Response->message . "\n";
5.102 + exit(-1);
5.103 +} elsif (exists($Options{'w'})) {
5.104 + print $Response->content;
5.105 + exit (0);
5.106 +} elsif ($Response->content =~ /WARNING: (\S*) does not exist/) {
5.107 + print "Specified System $1 does not exist\n";
5.108 + exit(-1);
5.109 +} elsif (exists($Options{'x'}) &&
5.110 + $Response->content =~
5.111 + /%\s*Result\s*:\s*Unsatisfiable.*\n%\s*Output\s*:\s*(CNF)?Refutation.*\n%/ &&
5.112 + $Response->content !~ /ERROR: Could not form TPTP format derivation/ )
5.113 +{
5.114 + # converted output: extract proof
5.115 + my @lines = split( /\n/, $Response->content);
5.116 + my $extract = "";
5.117 + foreach my $line (@lines){
5.118 + #ignore comments
5.119 + if ($line !~ /^%/ && !($line eq "")) {
5.120 + $extract .= "$line";
5.121 + }
5.122 + }
5.123 + # insert newlines after ').'
5.124 + $extract =~ s/\s//g;
5.125 + $extract =~ s/\)\.cnf/\)\.\ncnf/g;
5.126 +
5.127 + print "========== ~~/lib/scripts/SystemOnTPTP extracted proof: ==========\n";
5.128 + # orientation for res_reconstruct.ML
5.129 + print "# SZS output start CNFRefutation.\n";
5.130 + print "$extract\n";
5.131 + print "# SZS output end CNFRefutation.\n";
5.132 + # can be useful for debugging; Isabelle ignores this
5.133 + print "============== original response from SystemOnTPTP: ==============\n";
5.134 + print $Response->content;
5.135 + exit(0);
5.136 +} elsif (!exists($Options{'x'})) {
5.137 + # pass output directly to Isabelle
5.138 + print $Response->content;
5.139 + exit(0);
5.140 +}else {
5.141 + print "Remote-script could not extract proof:\n".$Response->content;
5.142 + exit(-1);
5.143 +}
5.144 +
6.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
6.2 +++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML Tue Aug 04 19:20:24 2009 +0200
6.3 @@ -0,0 +1,403 @@
6.4 +(* Title: HOL/Tools/ATP_Manager/atp_manager.ML
6.5 + Author: Fabian Immler, TU Muenchen
6.6 +
6.7 +ATP threads are registered here.
6.8 +Threads with the same birth-time are seen as one group.
6.9 +All threads of a group are killed when one thread of it has been successful,
6.10 +or after a certain time,
6.11 +or when the maximum number of threads exceeds; then the oldest thread is killed.
6.12 +*)
6.13 +
6.14 +signature ATP_MANAGER =
6.15 +sig
6.16 + val get_atps: unit -> string
6.17 + val set_atps: string -> unit
6.18 + val get_max_atps: unit -> int
6.19 + val set_max_atps: int -> unit
6.20 + val get_timeout: unit -> int
6.21 + val set_timeout: int -> unit
6.22 + val get_full_types: unit -> bool
6.23 + val set_full_types: bool -> unit
6.24 + val kill: unit -> unit
6.25 + val info: unit -> unit
6.26 + val messages: int option -> unit
6.27 + type prover = int -> (thm * (string * int)) list option ->
6.28 + (thm * (string * int)) list option -> string -> int ->
6.29 + Proof.context * (thm list * thm) ->
6.30 + bool * string * string * string vector * (thm * (string * int)) list
6.31 + val add_prover: string -> prover -> theory -> theory
6.32 + val print_provers: theory -> unit
6.33 + val get_prover: string -> theory -> prover option
6.34 + val sledgehammer: string list -> Proof.state -> unit
6.35 +end;
6.36 +
6.37 +structure AtpManager: ATP_MANAGER =
6.38 +struct
6.39 +
6.40 +(** preferences **)
6.41 +
6.42 +val message_store_limit = 20;
6.43 +val message_display_limit = 5;
6.44 +
6.45 +local
6.46 +
6.47 +val atps = ref "e remote_vampire";
6.48 +val max_atps = ref 5; (* ~1 means infinite number of atps *)
6.49 +val timeout = ref 60;
6.50 +val full_types = ref false;
6.51 +
6.52 +in
6.53 +
6.54 +fun get_atps () = CRITICAL (fn () => ! atps);
6.55 +fun set_atps str = CRITICAL (fn () => atps := str);
6.56 +
6.57 +fun get_max_atps () = CRITICAL (fn () => ! max_atps);
6.58 +fun set_max_atps number = CRITICAL (fn () => max_atps := number);
6.59 +
6.60 +fun get_timeout () = CRITICAL (fn () => ! timeout);
6.61 +fun set_timeout time = CRITICAL (fn () => timeout := time);
6.62 +
6.63 +fun get_full_types () = CRITICAL (fn () => ! full_types);
6.64 +fun set_full_types bool = CRITICAL (fn () => full_types := bool);
6.65 +
6.66 +val _ =
6.67 + ProofGeneralPgip.add_preference Preferences.category_proof
6.68 + (Preferences.string_pref atps
6.69 + "ATP: provers" "Default automatic provers (separated by whitespace)");
6.70 +
6.71 +val _ =
6.72 + ProofGeneralPgip.add_preference Preferences.category_proof
6.73 + (Preferences.int_pref max_atps
6.74 + "ATP: maximum number" "How many provers may run in parallel");
6.75 +
6.76 +val _ =
6.77 + ProofGeneralPgip.add_preference Preferences.category_proof
6.78 + (Preferences.int_pref timeout
6.79 + "ATP: timeout" "ATPs will be interrupted after this time (in seconds)");
6.80 +
6.81 +val _ =
6.82 + ProofGeneralPgip.add_preference Preferences.category_proof
6.83 + (Preferences.bool_pref full_types
6.84 + "ATP: full types" "ATPs will use full type information");
6.85 +
6.86 +end;
6.87 +
6.88 +
6.89 +
6.90 +(** thread management **)
6.91 +
6.92 +(* data structures over threads *)
6.93 +
6.94 +structure ThreadHeap = HeapFun
6.95 +(
6.96 + type elem = Time.time * Thread.thread;
6.97 + fun ord ((a, _), (b, _)) = Time.compare (a, b);
6.98 +);
6.99 +
6.100 +fun lookup_thread xs = AList.lookup Thread.equal xs;
6.101 +fun delete_thread xs = AList.delete Thread.equal xs;
6.102 +fun update_thread xs = AList.update Thread.equal xs;
6.103 +
6.104 +
6.105 +(* state of thread manager *)
6.106 +
6.107 +datatype T = State of
6.108 + {managing_thread: Thread.thread option,
6.109 + timeout_heap: ThreadHeap.T,
6.110 + oldest_heap: ThreadHeap.T,
6.111 + active: (Thread.thread * (Time.time * Time.time * string)) list,
6.112 + cancelling: (Thread.thread * (Time.time * Time.time * string)) list,
6.113 + messages: string list,
6.114 + store: string list};
6.115 +
6.116 +fun make_state managing_thread timeout_heap oldest_heap active cancelling messages store =
6.117 + State {managing_thread = managing_thread, timeout_heap = timeout_heap, oldest_heap = oldest_heap,
6.118 + active = active, cancelling = cancelling, messages = messages, store = store};
6.119 +
6.120 +val state = Synchronized.var "atp_manager"
6.121 + (make_state NONE ThreadHeap.empty ThreadHeap.empty [] [] [] []);
6.122 +
6.123 +
6.124 +(* unregister thread *)
6.125 +
6.126 +fun unregister (success, message) thread = Synchronized.change state
6.127 + (fn state as State {managing_thread, timeout_heap, oldest_heap, active, cancelling, messages, store} =>
6.128 + (case lookup_thread active thread of
6.129 + SOME (birthtime, _, description) =>
6.130 + let
6.131 + val (group, active') =
6.132 + if success then List.partition (fn (_, (tb, _, _)) => tb = birthtime) active
6.133 + else List.partition (fn (th, _) => Thread.equal (th, thread)) active
6.134 +
6.135 + val now = Time.now ()
6.136 + val cancelling' =
6.137 + fold (fn (th, (tb, _, desc)) => update_thread (th, (tb, now, desc))) group cancelling
6.138 +
6.139 + val message' = description ^ "\n" ^ message ^
6.140 + (if length group <= 1 then ""
6.141 + else "\nInterrupted " ^ string_of_int (length group - 1) ^ " other group members")
6.142 + val store' = message' ::
6.143 + (if length store <= message_store_limit then store
6.144 + else #1 (chop message_store_limit store))
6.145 + in make_state
6.146 + managing_thread timeout_heap oldest_heap active' cancelling' (message' :: messages) store'
6.147 + end
6.148 + | NONE => state));
6.149 +
6.150 +
6.151 +(* kill excessive atp threads *)
6.152 +
6.153 +fun excessive_atps active =
6.154 + let val max = get_max_atps ()
6.155 + in length active > max andalso max > ~1 end;
6.156 +
6.157 +local
6.158 +
6.159 +fun kill_oldest () =
6.160 + let exception Unchanged in
6.161 + Synchronized.change_result state
6.162 + (fn State {managing_thread, timeout_heap, oldest_heap, active, cancelling, messages, store} =>
6.163 + if ThreadHeap.is_empty oldest_heap orelse not (excessive_atps active)
6.164 + then raise Unchanged
6.165 + else
6.166 + let val ((_, oldest_thread), oldest_heap') = ThreadHeap.min_elem oldest_heap
6.167 + in (oldest_thread,
6.168 + make_state managing_thread timeout_heap oldest_heap' active cancelling messages store) end)
6.169 + |> unregister (false, "Interrupted (maximum number of ATPs exceeded)")
6.170 + handle Unchanged => ()
6.171 + end;
6.172 +
6.173 +in
6.174 +
6.175 +fun kill_excessive () =
6.176 + let val State {active, ...} = Synchronized.value state
6.177 + in if excessive_atps active then (kill_oldest (); kill_excessive ()) else () end;
6.178 +
6.179 +end;
6.180 +
6.181 +fun print_new_messages () =
6.182 + let val to_print = Synchronized.change_result state
6.183 + (fn State {managing_thread, timeout_heap, oldest_heap, active, cancelling, messages, store} =>
6.184 + (messages, make_state managing_thread timeout_heap oldest_heap active cancelling [] store))
6.185 + in
6.186 + if null to_print then ()
6.187 + else priority ("Sledgehammer: " ^ space_implode "\n\n" to_print)
6.188 + end;
6.189 +
6.190 +
6.191 +(* start a watching thread -- only one may exist *)
6.192 +
6.193 +fun check_thread_manager () = Synchronized.change state
6.194 + (fn State {managing_thread, timeout_heap, oldest_heap, active, cancelling, messages, store} =>
6.195 + if (case managing_thread of SOME thread => Thread.isActive thread | NONE => false)
6.196 + then make_state managing_thread timeout_heap oldest_heap active cancelling messages store
6.197 + else let val managing_thread = SOME (SimpleThread.fork false (fn () =>
6.198 + let
6.199 + val min_wait_time = Time.fromMilliseconds 300
6.200 + val max_wait_time = Time.fromSeconds 10
6.201 +
6.202 + (* wait for next thread to cancel, or maximum*)
6.203 + fun time_limit (State {timeout_heap, ...}) =
6.204 + (case try ThreadHeap.min timeout_heap of
6.205 + NONE => SOME (Time.+ (Time.now (), max_wait_time))
6.206 + | SOME (time, _) => SOME time)
6.207 +
6.208 + (* action: find threads whose timeout is reached, and interrupt cancelling threads *)
6.209 + fun action (State {managing_thread, timeout_heap, oldest_heap, active, cancelling,
6.210 + messages, store}) =
6.211 + let val (timeout_threads, timeout_heap') =
6.212 + ThreadHeap.upto (Time.now (), Thread.self ()) timeout_heap
6.213 + in
6.214 + if null timeout_threads andalso null cancelling andalso not (excessive_atps active)
6.215 + then NONE
6.216 + else
6.217 + let
6.218 + val _ = List.app (SimpleThread.interrupt o #1) cancelling
6.219 + val cancelling' = filter (Thread.isActive o #1) cancelling
6.220 + val state' = make_state
6.221 + managing_thread timeout_heap' oldest_heap active cancelling' messages store
6.222 + in SOME (map #2 timeout_threads, state') end
6.223 + end
6.224 + in
6.225 + while Synchronized.change_result state
6.226 + (fn st as
6.227 + State {managing_thread, timeout_heap, oldest_heap, active, cancelling, messages, store} =>
6.228 + if (null active) andalso (null cancelling) andalso (null messages)
6.229 + then (false, make_state NONE timeout_heap oldest_heap active cancelling messages store)
6.230 + else (true, st))
6.231 + do
6.232 + (Synchronized.timed_access state time_limit action
6.233 + |> these
6.234 + |> List.app (unregister (false, "Interrupted (reached timeout)"));
6.235 + kill_excessive ();
6.236 + print_new_messages ();
6.237 + (*give threads time to respond to interrupt*)
6.238 + OS.Process.sleep min_wait_time)
6.239 + end))
6.240 + in make_state managing_thread timeout_heap oldest_heap active cancelling messages store end);
6.241 +
6.242 +
6.243 +(* thread is registered here by sledgehammer *)
6.244 +
6.245 +fun register birthtime deadtime (thread, desc) =
6.246 + (Synchronized.change state
6.247 + (fn State {managing_thread, timeout_heap, oldest_heap, active, cancelling, messages, store} =>
6.248 + let
6.249 + val timeout_heap' = ThreadHeap.insert (deadtime, thread) timeout_heap
6.250 + val oldest_heap' = ThreadHeap.insert (birthtime, thread) oldest_heap
6.251 + val active' = update_thread (thread, (birthtime, deadtime, desc)) active
6.252 + in make_state managing_thread timeout_heap' oldest_heap' active' cancelling messages store end);
6.253 + check_thread_manager ());
6.254 +
6.255 +
6.256 +
6.257 +(** user commands **)
6.258 +
6.259 +(* kill: move all threads to cancelling *)
6.260 +
6.261 +fun kill () = Synchronized.change state
6.262 + (fn State {managing_thread, timeout_heap, oldest_heap, active, cancelling, messages, store} =>
6.263 + let val formerly_active = map (fn (th, (tb, _, desc)) => (th, (tb, Time.now (), desc))) active
6.264 + in make_state
6.265 + managing_thread timeout_heap oldest_heap [] (formerly_active @ cancelling) messages store
6.266 + end);
6.267 +
6.268 +
6.269 +(* ATP info *)
6.270 +
6.271 +fun info () =
6.272 + let
6.273 + val State {active, cancelling, ...} = Synchronized.value state
6.274 +
6.275 + fun running_info (_, (birth_time, dead_time, desc)) = "Running: "
6.276 + ^ (string_of_int o Time.toSeconds) (Time.- (Time.now (), birth_time))
6.277 + ^ " s -- "
6.278 + ^ (string_of_int o Time.toSeconds) (Time.- (dead_time, Time.now ()))
6.279 + ^ " s to live:\n" ^ desc
6.280 + fun cancelling_info (_, (_, dead_time, desc)) = "Trying to interrupt thread since "
6.281 + ^ (string_of_int o Time.toSeconds) (Time.- (Time.now (), dead_time))
6.282 + ^ " s:\n" ^ desc
6.283 +
6.284 + val running =
6.285 + if null active then "No ATPs running."
6.286 + else space_implode "\n\n" ("Running ATPs:" :: map running_info active)
6.287 + val interrupting =
6.288 + if null cancelling then ""
6.289 + else space_implode "\n\n"
6.290 + ("Trying to interrupt the following ATPs:" :: map cancelling_info cancelling)
6.291 +
6.292 + in writeln (running ^ "\n" ^ interrupting) end;
6.293 +
6.294 +fun messages opt_limit =
6.295 + let
6.296 + val limit = the_default message_display_limit opt_limit;
6.297 + val State {store = msgs, ...} = Synchronized.value state
6.298 + val header = "Recent ATP messages" ^
6.299 + (if length msgs <= limit then ":" else " (" ^ string_of_int limit ^ " displayed):");
6.300 + in writeln (space_implode "\n\n" (header :: #1 (chop limit msgs))) end;
6.301 +
6.302 +
6.303 +
6.304 +(** The Sledgehammer **)
6.305 +
6.306 +(* named provers *)
6.307 +
6.308 +type prover = int -> (thm * (string * int)) list option ->
6.309 + (thm * (string * int)) list option -> string -> int ->
6.310 + Proof.context * (thm list * thm) ->
6.311 + bool * string * string * string vector * (thm * (string * int)) list
6.312 +
6.313 +fun err_dup_prover name = error ("Duplicate prover: " ^ quote name);
6.314 +
6.315 +structure Provers = TheoryDataFun
6.316 +(
6.317 + type T = (prover * stamp) Symtab.table
6.318 + val empty = Symtab.empty
6.319 + val copy = I
6.320 + val extend = I
6.321 + fun merge _ tabs : T = Symtab.merge (eq_snd op =) tabs
6.322 + handle Symtab.DUP dup => err_dup_prover dup
6.323 +);
6.324 +
6.325 +fun add_prover name prover thy =
6.326 + Provers.map (Symtab.update_new (name, (prover, stamp ()))) thy
6.327 + handle Symtab.DUP dup => err_dup_prover dup;
6.328 +
6.329 +fun print_provers thy = Pretty.writeln
6.330 + (Pretty.strs ("external provers:" :: sort_strings (Symtab.keys (Provers.get thy))));
6.331 +
6.332 +fun get_prover name thy = case Symtab.lookup (Provers.get thy) name of
6.333 + NONE => NONE
6.334 +| SOME (prover, _) => SOME prover;
6.335 +
6.336 +(* start prover thread *)
6.337 +
6.338 +fun start_prover name birthtime deadtime i proof_state =
6.339 + (case get_prover name (Proof.theory_of proof_state) of
6.340 + NONE => warning ("Unknown external prover: " ^ quote name)
6.341 + | SOME prover =>
6.342 + let
6.343 + val (ctxt, (_, goal)) = Proof.get_goal proof_state
6.344 + val desc =
6.345 + "external prover " ^ quote name ^ " for subgoal " ^ string_of_int i ^ ":\n" ^
6.346 + Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i))
6.347 + val _ = SimpleThread.fork true (fn () =>
6.348 + let
6.349 + val _ = register birthtime deadtime (Thread.self (), desc)
6.350 + val result =
6.351 + let val (success, message, _, _, _) =
6.352 + prover (get_timeout ()) NONE NONE name i (Proof.get_goal proof_state)
6.353 + in (success, message) end
6.354 + handle ResHolClause.TOO_TRIVIAL
6.355 + => (true, "Empty clause: Try this command: " ^ Markup.markup Markup.sendback "apply metis")
6.356 + | ERROR msg
6.357 + => (false, "Error: " ^ msg)
6.358 + val _ = unregister result (Thread.self ())
6.359 + in () end handle Interrupt => ())
6.360 + in () end);
6.361 +
6.362 +
6.363 +(* sledghammer for first subgoal *)
6.364 +
6.365 +fun sledgehammer names proof_state =
6.366 + let
6.367 + val provers =
6.368 + if null names then String.tokens (Symbol.is_ascii_blank o String.str) (get_atps ())
6.369 + else names
6.370 + val birthtime = Time.now ()
6.371 + val deadtime = Time.+ (birthtime, Time.fromSeconds (get_timeout ()))
6.372 + in List.app (fn name => start_prover name birthtime deadtime 1 proof_state) provers end;
6.373 +
6.374 +
6.375 +
6.376 +(** Isar command syntax **)
6.377 +
6.378 +local structure K = OuterKeyword and P = OuterParse in
6.379 +
6.380 +val _ =
6.381 + OuterSyntax.improper_command "atp_kill" "kill all managed provers" K.diag
6.382 + (Scan.succeed (Toplevel.no_timing o Toplevel.imperative kill));
6.383 +
6.384 +val _ =
6.385 + OuterSyntax.improper_command "atp_info" "print information about managed provers" K.diag
6.386 + (Scan.succeed (Toplevel.no_timing o Toplevel.imperative info));
6.387 +
6.388 +val _ =
6.389 + OuterSyntax.improper_command "atp_messages" "print recent messages issued by managed provers" K.diag
6.390 + (Scan.option (P.$$$ "(" |-- P.nat --| P.$$$ ")") >>
6.391 + (fn limit => Toplevel.no_timing o Toplevel.imperative (fn () => messages limit)));
6.392 +
6.393 +val _ =
6.394 + OuterSyntax.improper_command "print_atps" "print external provers" K.diag
6.395 + (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_theory o
6.396 + Toplevel.keep (print_provers o Toplevel.theory_of)));
6.397 +
6.398 +val _ =
6.399 + OuterSyntax.command "sledgehammer" "call all automatic theorem provers" K.diag
6.400 + (Scan.repeat P.xname >> (fn names => Toplevel.no_timing o Toplevel.unknown_proof o
6.401 + Toplevel.keep (sledgehammer names o Toplevel.proof_of)));
6.402 +
6.403 +end;
6.404 +
6.405 +end;
6.406 +
7.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
7.2 +++ b/src/HOL/Tools/ATP_Manager/atp_minimal.ML Tue Aug 04 19:20:24 2009 +0200
7.3 @@ -0,0 +1,223 @@
7.4 +(* Title: HOL/Tools/ATP_Manager/atp_minimal.ML
7.5 + Author: Philipp Meyer, TU Muenchen
7.6 +
7.7 +Minimalization of theorem list for metis by using an external automated theorem prover
7.8 +*)
7.9 +
7.10 +structure AtpMinimal: sig end =
7.11 +struct
7.12 +
7.13 +(* output control *)
7.14 +
7.15 +fun debug str = Output.debug (fn () => str)
7.16 +fun debug_fn f = if ! Output.debugging then f () else ()
7.17 +fun answer str = Output.writeln str
7.18 +fun println str = Output.priority str
7.19 +
7.20 +fun order_unique name_list = OrdList.make (String.collate Char.compare) name_list
7.21 +fun length_string namelist = Int.toString (length namelist)
7.22 +
7.23 +fun print_names name_thms_pairs =
7.24 + let
7.25 + val names = map fst name_thms_pairs
7.26 + val ordered = order_unique names
7.27 + in
7.28 + app (fn name => (debug (" " ^ name))) ordered
7.29 + end
7.30 +
7.31 +
7.32 +(* minimalization algorithm *)
7.33 +
7.34 +local
7.35 + fun isplit (l,r) [] = (l,r)
7.36 + | isplit (l,r) (h::[]) = (h::l, r)
7.37 + | isplit (l,r) (h1::h2::t) = isplit (h1::l, h2::r) t
7.38 +in
7.39 + fun split lst = isplit ([],[]) lst
7.40 +end
7.41 +
7.42 +local
7.43 + fun min p sup [] = raise Empty
7.44 + | min p sup [s0] = [s0]
7.45 + | min p sup s =
7.46 + let
7.47 + val (l0, r0) = split s
7.48 + in
7.49 + if p (sup @ l0)
7.50 + then min p sup l0
7.51 + else
7.52 + if p (sup @ r0)
7.53 + then min p sup r0
7.54 + else
7.55 + let
7.56 + val l = min p (sup @ r0) l0
7.57 + val r = min p (sup @ l) r0
7.58 + in
7.59 + l @ r
7.60 + end
7.61 + end
7.62 +in
7.63 + (* return a minimal subset v of s that satisfies p
7.64 + @pre p(s) & ~p([]) & monotone(p)
7.65 + @post v subset s & p(v) &
7.66 + forall e in v. ~p(v \ e)
7.67 + *)
7.68 + fun minimal p s = min p [] s
7.69 +end
7.70 +
7.71 +
7.72 +(* failure check and producing answer *)
7.73 +
7.74 +datatype 'a prove_result = Success of 'a | Failure | Timeout | Error
7.75 +
7.76 +val string_of_result =
7.77 + fn Success _ => "Success"
7.78 + | Failure => "Failure"
7.79 + | Timeout => "Timeout"
7.80 + | Error => "Error"
7.81 +
7.82 +val failure_strings =
7.83 + [("SPASS beiseite: Ran out of time.", Timeout),
7.84 + ("Timeout", Timeout),
7.85 + ("time limit exceeded", Timeout),
7.86 + ("# Cannot determine problem status within resource limit", Timeout),
7.87 + ("Error", Error)]
7.88 +
7.89 +fun produce_answer (success, message, result_string, thm_name_vec, filtered) =
7.90 + if success then
7.91 + (Success (Vector.foldr op:: [] thm_name_vec, filtered), result_string)
7.92 + else
7.93 + let
7.94 + val failure = failure_strings |> get_first (fn (s, t) =>
7.95 + if String.isSubstring s result_string then SOME (t, result_string) else NONE)
7.96 + in
7.97 + if is_some failure then
7.98 + the failure
7.99 + else
7.100 + (Failure, result_string)
7.101 + end
7.102 +
7.103 +
7.104 +(* wrapper for calling external prover *)
7.105 +
7.106 +fun sh_test_thms prover prover_name time_limit subgoalno state filtered name_thms_pairs =
7.107 + let
7.108 + val _ = println ("Testing " ^ (length_string name_thms_pairs) ^ " theorems... ")
7.109 + val name_thm_pairs =
7.110 + flat (map (fn (n, ths) => map_index (fn (i, th) => (n, th)) ths) name_thms_pairs)
7.111 + val _ = debug_fn (fn () => print_names name_thm_pairs)
7.112 + val axclauses = ResAxioms.cnf_rules_pairs (Proof.theory_of state) name_thm_pairs
7.113 + val (result, proof) =
7.114 + produce_answer
7.115 + (prover time_limit (SOME axclauses) filtered prover_name subgoalno (Proof.get_goal state))
7.116 + val _ = println (string_of_result result)
7.117 + val _ = debug proof
7.118 + in
7.119 + (result, proof)
7.120 + end
7.121 +
7.122 +
7.123 +(* minimalization of thms *)
7.124 +
7.125 +fun minimalize prover prover_name time_limit state name_thms_pairs =
7.126 + let
7.127 + val _ =
7.128 + println ("Minimize called with " ^ length_string name_thms_pairs ^ " theorems, prover: "
7.129 + ^ prover_name ^ ", time limit: " ^ Int.toString time_limit ^ " seconds")
7.130 + val _ = debug_fn (fn () => app (fn (n, tl) =>
7.131 + (debug n; app (fn t =>
7.132 + debug (" " ^ Display.string_of_thm (Proof.context_of state) t)) tl)) name_thms_pairs)
7.133 + val test_thms_fun = sh_test_thms prover prover_name time_limit 1 state
7.134 + fun test_thms filtered thms =
7.135 + case test_thms_fun filtered thms of (Success _, _) => true | _ => false
7.136 + in
7.137 + (* try prove first to check result and get used theorems *)
7.138 + (case test_thms_fun NONE name_thms_pairs of
7.139 + (Success (used, filtered), _) =>
7.140 + let
7.141 + val ordered_used = order_unique used
7.142 + val to_use =
7.143 + if length ordered_used < length name_thms_pairs then
7.144 + filter (fn (name1, _) => List.exists (equal name1) ordered_used) name_thms_pairs
7.145 + else
7.146 + name_thms_pairs
7.147 + val min_thms = (minimal (test_thms (SOME filtered)) to_use)
7.148 + val min_names = order_unique (map fst min_thms)
7.149 + val _ = println ("Minimal " ^ (length_string min_thms) ^ " theorems")
7.150 + val _ = debug_fn (fn () => print_names min_thms)
7.151 + in
7.152 + answer ("Try this command: " ^
7.153 + Markup.markup Markup.sendback ("apply (metis " ^ space_implode " " min_names ^ ")"))
7.154 + end
7.155 + | (Timeout, _) =>
7.156 + answer ("Timeout: You may need to increase the time limit of " ^
7.157 + Int.toString time_limit ^ " seconds. Call atp_minimize [time=...] ")
7.158 + | (Error, msg) =>
7.159 + answer ("Error in prover: " ^ msg)
7.160 + | (Failure, _) =>
7.161 + answer "Failure: No proof with the theorems supplied")
7.162 + handle ResHolClause.TOO_TRIVIAL =>
7.163 + answer ("Trivial: Try this command: " ^ Markup.markup Markup.sendback "apply metis")
7.164 + | ERROR msg =>
7.165 + answer ("Error: " ^ msg)
7.166 + end
7.167 +
7.168 +
7.169 +(* Isar command and parsing input *)
7.170 +
7.171 +local structure K = OuterKeyword and P = OuterParse and T = OuterLex in
7.172 +
7.173 +fun get_thms context =
7.174 + map (fn (name, interval) =>
7.175 + let
7.176 + val thmref = Facts.Named ((name, Position.none), interval)
7.177 + val ths = ProofContext.get_fact context thmref
7.178 + val name' = Facts.string_of_ref thmref
7.179 + in
7.180 + (name', ths)
7.181 + end)
7.182 +
7.183 +val default_prover = "remote_vampire"
7.184 +val default_time_limit = 5
7.185 +
7.186 +fun get_time_limit_arg time_string =
7.187 + (case Int.fromString time_string of
7.188 + SOME t => t
7.189 + | NONE => error ("Invalid time limit: " ^ quote time_string))
7.190 +
7.191 +val get_options =
7.192 + let
7.193 + val def = (default_prover, default_time_limit)
7.194 + in
7.195 + foldl (fn ((name, a), (p, t)) =>
7.196 + (case name of
7.197 + "time" => (p, (get_time_limit_arg a))
7.198 + | "atp" => (a, t)
7.199 + | n => error ("Invalid argument: " ^ n))) def
7.200 + end
7.201 +
7.202 +fun sh_min_command args thm_names state =
7.203 + let
7.204 + val (prover_name, time_limit) = get_options args
7.205 + val prover =
7.206 + case AtpManager.get_prover prover_name (Proof.theory_of state) of
7.207 + SOME prover => prover
7.208 + | NONE => error ("Unknown prover: " ^ quote prover_name)
7.209 + val name_thms_pairs = get_thms (Proof.context_of state) thm_names
7.210 + in
7.211 + minimalize prover prover_name time_limit state name_thms_pairs
7.212 + end
7.213 +
7.214 +val parse_args = Scan.optional (Args.bracks (P.list (P.xname --| P.$$$ "=" -- P.xname))) []
7.215 +val parse_thm_names = Scan.repeat (P.xname -- Scan.option Attrib.thm_sel)
7.216 +
7.217 +val _ =
7.218 + OuterSyntax.command "atp_minimize" "minimize theorem list with external prover" K.diag
7.219 + (parse_args -- parse_thm_names >> (fn (args, thm_names) =>
7.220 + Toplevel.no_timing o Toplevel.unknown_proof o
7.221 + Toplevel.keep (sh_min_command args thm_names o Toplevel.proof_of)))
7.222 +
7.223 +end
7.224 +
7.225 +end
7.226 +
8.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
8.2 +++ b/src/HOL/Tools/ATP_Manager/atp_wrapper.ML Tue Aug 04 19:20:24 2009 +0200
8.3 @@ -0,0 +1,217 @@
8.4 +(* Title: HOL/Tools/ATP_Manager/atp_wrapper.ML
8.5 + Author: Fabian Immler, TU Muenchen
8.6 +
8.7 +Wrapper functions for external ATPs.
8.8 +*)
8.9 +
8.10 +signature ATP_WRAPPER =
8.11 +sig
8.12 + val destdir: string ref
8.13 + val problem_name: string ref
8.14 + val tptp_prover_opts_full: int -> bool -> bool -> Path.T * string -> AtpManager.prover
8.15 + val tptp_prover_opts: int -> bool -> Path.T * string -> AtpManager.prover
8.16 + val tptp_prover: Path.T * string -> AtpManager.prover
8.17 + val full_prover_opts: int -> bool -> Path.T * string -> AtpManager.prover
8.18 + val full_prover: Path.T * string -> AtpManager.prover
8.19 + val vampire_opts: int -> bool -> AtpManager.prover
8.20 + val vampire: AtpManager.prover
8.21 + val vampire_opts_full: int -> bool -> AtpManager.prover
8.22 + val vampire_full: AtpManager.prover
8.23 + val eprover_opts: int -> bool -> AtpManager.prover
8.24 + val eprover: AtpManager.prover
8.25 + val eprover_opts_full: int -> bool -> AtpManager.prover
8.26 + val eprover_full: AtpManager.prover
8.27 + val spass_opts: int -> bool -> AtpManager.prover
8.28 + val spass: AtpManager.prover
8.29 + val remote_prover_opts: int -> bool -> string -> string -> AtpManager.prover
8.30 + val remote_prover: string -> string -> AtpManager.prover
8.31 + val refresh_systems: unit -> unit
8.32 +end;
8.33 +
8.34 +structure AtpWrapper: ATP_WRAPPER =
8.35 +struct
8.36 +
8.37 +(** generic ATP wrapper **)
8.38 +
8.39 +(* global hooks for writing problemfiles *)
8.40 +
8.41 +val destdir = ref ""; (*Empty means write files to /tmp*)
8.42 +val problem_name = ref "prob";
8.43 +
8.44 +
8.45 +(* basic template *)
8.46 +
8.47 +fun external_prover relevance_filter preparer writer (cmd, args) find_failure produce_answer
8.48 + timeout axiom_clauses filtered_clauses name subgoalno goal =
8.49 + let
8.50 + (* path to unique problem file *)
8.51 + val destdir' = ! destdir
8.52 + val problem_name' = ! problem_name
8.53 + fun prob_pathname nr =
8.54 + let val probfile = Path.basic (problem_name' ^ serial_string () ^ "_" ^ string_of_int nr)
8.55 + in if destdir' = "" then File.tmp_path probfile
8.56 + else if File.exists (Path.explode (destdir'))
8.57 + then Path.append (Path.explode (destdir')) probfile
8.58 + else error ("No such directory: " ^ destdir')
8.59 + end
8.60 +
8.61 + (* get clauses and prepare them for writing *)
8.62 + val (ctxt, (chain_ths, th)) = goal
8.63 + val thy = ProofContext.theory_of ctxt
8.64 + val chain_ths = map (Thm.put_name_hint ResReconstruct.chained_hint) chain_ths
8.65 + val goal_cls = #1 (ResAxioms.neg_conjecture_clauses ctxt th subgoalno)
8.66 + val _ = app (fn th => Output.debug (fn _ => Display.string_of_thm ctxt th)) goal_cls
8.67 + val the_filtered_clauses =
8.68 + case filtered_clauses of
8.69 + NONE => relevance_filter goal goal_cls
8.70 + | SOME fcls => fcls
8.71 + val the_axiom_clauses =
8.72 + case axiom_clauses of
8.73 + NONE => the_filtered_clauses
8.74 + | SOME axcls => axcls
8.75 + val (thm_names, clauses) =
8.76 + preparer goal_cls chain_ths the_axiom_clauses the_filtered_clauses thy
8.77 +
8.78 + (* write out problem file and call prover *)
8.79 + val probfile = prob_pathname subgoalno
8.80 + val conj_pos = writer probfile clauses
8.81 + val (proof, rc) = system_out (
8.82 + if File.exists cmd then
8.83 + space_implode " " ["exec", File.shell_path cmd, args, File.platform_path probfile]
8.84 + else error ("Bad executable: " ^ Path.implode cmd))
8.85 +
8.86 + (* if problemfile has not been exported, delete problemfile; otherwise export proof, too *)
8.87 + val _ =
8.88 + if destdir' = "" then File.rm probfile
8.89 + else File.write (Path.explode (Path.implode probfile ^ "_proof")) proof
8.90 +
8.91 + (* check for success and print out some information on failure *)
8.92 + val failure = find_failure proof
8.93 + val success = rc = 0 andalso is_none failure
8.94 + val message =
8.95 + if is_some failure then "External prover failed."
8.96 + else if rc <> 0 then "External prover failed: " ^ proof
8.97 + else "Try this command: " ^
8.98 + produce_answer name (proof, thm_names, conj_pos, ctxt, th, subgoalno)
8.99 + val _ = Output.debug (fn () => "Sledgehammer response (rc = " ^ string_of_int rc ^ "):\n" ^ proof)
8.100 + in (success, message, proof, thm_names, the_filtered_clauses) end;
8.101 +
8.102 +
8.103 +
8.104 +(** common provers **)
8.105 +
8.106 +(* generic TPTP-based provers *)
8.107 +
8.108 +fun tptp_prover_opts_full max_new theory_const full command timeout ax_clauses fcls name n goal =
8.109 + external_prover
8.110 + (ResAtp.get_relevant max_new theory_const)
8.111 + (ResAtp.prepare_clauses false)
8.112 + (ResHolClause.tptp_write_file (AtpManager.get_full_types()))
8.113 + command
8.114 + ResReconstruct.find_failure
8.115 + (if full then ResReconstruct.structured_proof else ResReconstruct.lemma_list false)
8.116 + timeout ax_clauses fcls name n goal;
8.117 +
8.118 +(*arbitrary ATP with TPTP input/output and problemfile as last argument*)
8.119 +fun tptp_prover_opts max_new theory_const =
8.120 + tptp_prover_opts_full max_new theory_const false;
8.121 +
8.122 +fun tptp_prover x = tptp_prover_opts 60 true x;
8.123 +
8.124 +(*for structured proofs: prover must support TSTP*)
8.125 +fun full_prover_opts max_new theory_const =
8.126 + tptp_prover_opts_full max_new theory_const true;
8.127 +
8.128 +fun full_prover x = full_prover_opts 60 true x;
8.129 +
8.130 +
8.131 +(* Vampire *)
8.132 +
8.133 +(*NB: Vampire does not work without explicit timelimit*)
8.134 +
8.135 +fun vampire_opts max_new theory_const timeout = tptp_prover_opts
8.136 + max_new theory_const
8.137 + (Path.explode "$VAMPIRE_HOME/vampire",
8.138 + ("--output_syntax tptp --mode casc -t " ^ string_of_int timeout))
8.139 + timeout;
8.140 +
8.141 +val vampire = vampire_opts 60 false;
8.142 +
8.143 +fun vampire_opts_full max_new theory_const timeout = full_prover_opts
8.144 + max_new theory_const
8.145 + (Path.explode "$VAMPIRE_HOME/vampire",
8.146 + ("--output_syntax tptp --mode casc -t " ^ string_of_int timeout))
8.147 + timeout;
8.148 +
8.149 +val vampire_full = vampire_opts_full 60 false;
8.150 +
8.151 +
8.152 +(* E prover *)
8.153 +
8.154 +fun eprover_opts max_new theory_const timeout = tptp_prover_opts
8.155 + max_new theory_const
8.156 + (Path.explode "$E_HOME/eproof",
8.157 + "--tstp-in --tstp-out -l5 -xAutoDev -tAutoDev --silent --cpu-limit=" ^ string_of_int timeout)
8.158 + timeout;
8.159 +
8.160 +val eprover = eprover_opts 100 false;
8.161 +
8.162 +fun eprover_opts_full max_new theory_const timeout = full_prover_opts
8.163 + max_new theory_const
8.164 + (Path.explode "$E_HOME/eproof",
8.165 + "--tstp-in --tstp-out -l5 -xAutoDev -tAutoDev --silent --cpu-limit=" ^ string_of_int timeout)
8.166 + timeout;
8.167 +
8.168 +val eprover_full = eprover_opts_full 100 false;
8.169 +
8.170 +
8.171 +(* SPASS *)
8.172 +
8.173 +fun spass_opts max_new theory_const timeout ax_clauses fcls name n goal = external_prover
8.174 + (ResAtp.get_relevant max_new theory_const)
8.175 + (ResAtp.prepare_clauses true)
8.176 + (ResHolClause.dfg_write_file (AtpManager.get_full_types()))
8.177 + (Path.explode "$SPASS_HOME/SPASS",
8.178 + "-Auto -SOS=1 -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof -TimeLimit=" ^
8.179 + string_of_int timeout)
8.180 + ResReconstruct.find_failure
8.181 + (ResReconstruct.lemma_list true)
8.182 + timeout ax_clauses fcls name n goal;
8.183 +
8.184 +val spass = spass_opts 40 true;
8.185 +
8.186 +
8.187 +(* remote prover invocation via SystemOnTPTP *)
8.188 +
8.189 +val systems =
8.190 + Synchronized.var "atp_wrapper_systems" ([]: string list);
8.191 +
8.192 +fun get_systems () =
8.193 + let
8.194 + val (answer, rc) = system_out ("\"$ISABELLE_ATP_MANAGER/SystemOnTPTP\" -w")
8.195 + in
8.196 + if rc <> 0 then error ("Failed to get available systems from SystemOnTPTP:\n" ^ answer)
8.197 + else split_lines answer
8.198 + end;
8.199 +
8.200 +fun refresh_systems () = Synchronized.change systems (fn _ =>
8.201 + get_systems ());
8.202 +
8.203 +fun get_system prefix = Synchronized.change_result systems (fn systems =>
8.204 + let val systems = if null systems then get_systems() else systems
8.205 + in (find_first (String.isPrefix prefix) systems, systems) end);
8.206 +
8.207 +fun remote_prover_opts max_new theory_const args prover_prefix timeout =
8.208 + let val sys =
8.209 + case get_system prover_prefix of
8.210 + NONE => error ("No system like " ^ quote prover_prefix ^ " at SystemOnTPTP")
8.211 + | SOME sys => sys
8.212 + in tptp_prover_opts max_new theory_const
8.213 + (Path.explode "$ISABELLE_ATP_MANAGER/SystemOnTPTP",
8.214 + args ^ " -t " ^ string_of_int timeout ^ " -s " ^ sys) timeout
8.215 + end;
8.216 +
8.217 +val remote_prover = remote_prover_opts 60 false;
8.218 +
8.219 +end;
8.220 +
9.1 --- a/src/HOL/Tools/atp_manager.ML Tue Aug 04 16:13:16 2009 +0200
9.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
9.3 @@ -1,403 +0,0 @@
9.4 -(* Title: HOL/Tools/atp_manager.ML
9.5 - Author: Fabian Immler, TU Muenchen
9.6 -
9.7 -ATP threads are registered here.
9.8 -Threads with the same birth-time are seen as one group.
9.9 -All threads of a group are killed when one thread of it has been successful,
9.10 -or after a certain time,
9.11 -or when the maximum number of threads exceeds; then the oldest thread is killed.
9.12 -*)
9.13 -
9.14 -signature ATP_MANAGER =
9.15 -sig
9.16 - val get_atps: unit -> string
9.17 - val set_atps: string -> unit
9.18 - val get_max_atps: unit -> int
9.19 - val set_max_atps: int -> unit
9.20 - val get_timeout: unit -> int
9.21 - val set_timeout: int -> unit
9.22 - val get_full_types: unit -> bool
9.23 - val set_full_types: bool -> unit
9.24 - val kill: unit -> unit
9.25 - val info: unit -> unit
9.26 - val messages: int option -> unit
9.27 - type prover = int -> (thm * (string * int)) list option ->
9.28 - (thm * (string * int)) list option -> string -> int ->
9.29 - Proof.context * (thm list * thm) ->
9.30 - bool * string * string * string vector * (thm * (string * int)) list
9.31 - val add_prover: string -> prover -> theory -> theory
9.32 - val print_provers: theory -> unit
9.33 - val get_prover: string -> theory -> prover option
9.34 - val sledgehammer: string list -> Proof.state -> unit
9.35 -end;
9.36 -
9.37 -structure AtpManager: ATP_MANAGER =
9.38 -struct
9.39 -
9.40 -(** preferences **)
9.41 -
9.42 -val message_store_limit = 20;
9.43 -val message_display_limit = 5;
9.44 -
9.45 -local
9.46 -
9.47 -val atps = ref "e remote_vampire";
9.48 -val max_atps = ref 5; (* ~1 means infinite number of atps *)
9.49 -val timeout = ref 60;
9.50 -val full_types = ref false;
9.51 -
9.52 -in
9.53 -
9.54 -fun get_atps () = CRITICAL (fn () => ! atps);
9.55 -fun set_atps str = CRITICAL (fn () => atps := str);
9.56 -
9.57 -fun get_max_atps () = CRITICAL (fn () => ! max_atps);
9.58 -fun set_max_atps number = CRITICAL (fn () => max_atps := number);
9.59 -
9.60 -fun get_timeout () = CRITICAL (fn () => ! timeout);
9.61 -fun set_timeout time = CRITICAL (fn () => timeout := time);
9.62 -
9.63 -fun get_full_types () = CRITICAL (fn () => ! full_types);
9.64 -fun set_full_types bool = CRITICAL (fn () => full_types := bool);
9.65 -
9.66 -val _ =
9.67 - ProofGeneralPgip.add_preference Preferences.category_proof
9.68 - (Preferences.string_pref atps
9.69 - "ATP: provers" "Default automatic provers (separated by whitespace)");
9.70 -
9.71 -val _ =
9.72 - ProofGeneralPgip.add_preference Preferences.category_proof
9.73 - (Preferences.int_pref max_atps
9.74 - "ATP: maximum number" "How many provers may run in parallel");
9.75 -
9.76 -val _ =
9.77 - ProofGeneralPgip.add_preference Preferences.category_proof
9.78 - (Preferences.int_pref timeout
9.79 - "ATP: timeout" "ATPs will be interrupted after this time (in seconds)");
9.80 -
9.81 -val _ =
9.82 - ProofGeneralPgip.add_preference Preferences.category_proof
9.83 - (Preferences.bool_pref full_types
9.84 - "ATP: full types" "ATPs will use full type information");
9.85 -
9.86 -end;
9.87 -
9.88 -
9.89 -
9.90 -(** thread management **)
9.91 -
9.92 -(* data structures over threads *)
9.93 -
9.94 -structure ThreadHeap = HeapFun
9.95 -(
9.96 - type elem = Time.time * Thread.thread;
9.97 - fun ord ((a, _), (b, _)) = Time.compare (a, b);
9.98 -);
9.99 -
9.100 -fun lookup_thread xs = AList.lookup Thread.equal xs;
9.101 -fun delete_thread xs = AList.delete Thread.equal xs;
9.102 -fun update_thread xs = AList.update Thread.equal xs;
9.103 -
9.104 -
9.105 -(* state of thread manager *)
9.106 -
9.107 -datatype T = State of
9.108 - {managing_thread: Thread.thread option,
9.109 - timeout_heap: ThreadHeap.T,
9.110 - oldest_heap: ThreadHeap.T,
9.111 - active: (Thread.thread * (Time.time * Time.time * string)) list,
9.112 - cancelling: (Thread.thread * (Time.time * Time.time * string)) list,
9.113 - messages: string list,
9.114 - store: string list};
9.115 -
9.116 -fun make_state managing_thread timeout_heap oldest_heap active cancelling messages store =
9.117 - State {managing_thread = managing_thread, timeout_heap = timeout_heap, oldest_heap = oldest_heap,
9.118 - active = active, cancelling = cancelling, messages = messages, store = store};
9.119 -
9.120 -val state = Synchronized.var "atp_manager"
9.121 - (make_state NONE ThreadHeap.empty ThreadHeap.empty [] [] [] []);
9.122 -
9.123 -
9.124 -(* unregister thread *)
9.125 -
9.126 -fun unregister (success, message) thread = Synchronized.change state
9.127 - (fn state as State {managing_thread, timeout_heap, oldest_heap, active, cancelling, messages, store} =>
9.128 - (case lookup_thread active thread of
9.129 - SOME (birthtime, _, description) =>
9.130 - let
9.131 - val (group, active') =
9.132 - if success then List.partition (fn (_, (tb, _, _)) => tb = birthtime) active
9.133 - else List.partition (fn (th, _) => Thread.equal (th, thread)) active
9.134 -
9.135 - val now = Time.now ()
9.136 - val cancelling' =
9.137 - fold (fn (th, (tb, _, desc)) => update_thread (th, (tb, now, desc))) group cancelling
9.138 -
9.139 - val message' = description ^ "\n" ^ message ^
9.140 - (if length group <= 1 then ""
9.141 - else "\nInterrupted " ^ string_of_int (length group - 1) ^ " other group members")
9.142 - val store' = message' ::
9.143 - (if length store <= message_store_limit then store
9.144 - else #1 (chop message_store_limit store))
9.145 - in make_state
9.146 - managing_thread timeout_heap oldest_heap active' cancelling' (message' :: messages) store'
9.147 - end
9.148 - | NONE => state));
9.149 -
9.150 -
9.151 -(* kill excessive atp threads *)
9.152 -
9.153 -fun excessive_atps active =
9.154 - let val max = get_max_atps ()
9.155 - in length active > max andalso max > ~1 end;
9.156 -
9.157 -local
9.158 -
9.159 -fun kill_oldest () =
9.160 - let exception Unchanged in
9.161 - Synchronized.change_result state
9.162 - (fn State {managing_thread, timeout_heap, oldest_heap, active, cancelling, messages, store} =>
9.163 - if ThreadHeap.is_empty oldest_heap orelse not (excessive_atps active)
9.164 - then raise Unchanged
9.165 - else
9.166 - let val ((_, oldest_thread), oldest_heap') = ThreadHeap.min_elem oldest_heap
9.167 - in (oldest_thread,
9.168 - make_state managing_thread timeout_heap oldest_heap' active cancelling messages store) end)
9.169 - |> unregister (false, "Interrupted (maximum number of ATPs exceeded)")
9.170 - handle Unchanged => ()
9.171 - end;
9.172 -
9.173 -in
9.174 -
9.175 -fun kill_excessive () =
9.176 - let val State {active, ...} = Synchronized.value state
9.177 - in if excessive_atps active then (kill_oldest (); kill_excessive ()) else () end;
9.178 -
9.179 -end;
9.180 -
9.181 -fun print_new_messages () =
9.182 - let val to_print = Synchronized.change_result state
9.183 - (fn State {managing_thread, timeout_heap, oldest_heap, active, cancelling, messages, store} =>
9.184 - (messages, make_state managing_thread timeout_heap oldest_heap active cancelling [] store))
9.185 - in
9.186 - if null to_print then ()
9.187 - else priority ("Sledgehammer: " ^ space_implode "\n\n" to_print)
9.188 - end;
9.189 -
9.190 -
9.191 -(* start a watching thread -- only one may exist *)
9.192 -
9.193 -fun check_thread_manager () = Synchronized.change state
9.194 - (fn State {managing_thread, timeout_heap, oldest_heap, active, cancelling, messages, store} =>
9.195 - if (case managing_thread of SOME thread => Thread.isActive thread | NONE => false)
9.196 - then make_state managing_thread timeout_heap oldest_heap active cancelling messages store
9.197 - else let val managing_thread = SOME (SimpleThread.fork false (fn () =>
9.198 - let
9.199 - val min_wait_time = Time.fromMilliseconds 300
9.200 - val max_wait_time = Time.fromSeconds 10
9.201 -
9.202 - (* wait for next thread to cancel, or maximum*)
9.203 - fun time_limit (State {timeout_heap, ...}) =
9.204 - (case try ThreadHeap.min timeout_heap of
9.205 - NONE => SOME (Time.+ (Time.now (), max_wait_time))
9.206 - | SOME (time, _) => SOME time)
9.207 -
9.208 - (* action: find threads whose timeout is reached, and interrupt cancelling threads *)
9.209 - fun action (State {managing_thread, timeout_heap, oldest_heap, active, cancelling,
9.210 - messages, store}) =
9.211 - let val (timeout_threads, timeout_heap') =
9.212 - ThreadHeap.upto (Time.now (), Thread.self ()) timeout_heap
9.213 - in
9.214 - if null timeout_threads andalso null cancelling andalso not (excessive_atps active)
9.215 - then NONE
9.216 - else
9.217 - let
9.218 - val _ = List.app (SimpleThread.interrupt o #1) cancelling
9.219 - val cancelling' = filter (Thread.isActive o #1) cancelling
9.220 - val state' = make_state
9.221 - managing_thread timeout_heap' oldest_heap active cancelling' messages store
9.222 - in SOME (map #2 timeout_threads, state') end
9.223 - end
9.224 - in
9.225 - while Synchronized.change_result state
9.226 - (fn st as
9.227 - State {managing_thread, timeout_heap, oldest_heap, active, cancelling, messages, store} =>
9.228 - if (null active) andalso (null cancelling) andalso (null messages)
9.229 - then (false, make_state NONE timeout_heap oldest_heap active cancelling messages store)
9.230 - else (true, st))
9.231 - do
9.232 - (Synchronized.timed_access state time_limit action
9.233 - |> these
9.234 - |> List.app (unregister (false, "Interrupted (reached timeout)"));
9.235 - kill_excessive ();
9.236 - print_new_messages ();
9.237 - (*give threads time to respond to interrupt*)
9.238 - OS.Process.sleep min_wait_time)
9.239 - end))
9.240 - in make_state managing_thread timeout_heap oldest_heap active cancelling messages store end);
9.241 -
9.242 -
9.243 -(* thread is registered here by sledgehammer *)
9.244 -
9.245 -fun register birthtime deadtime (thread, desc) =
9.246 - (Synchronized.change state
9.247 - (fn State {managing_thread, timeout_heap, oldest_heap, active, cancelling, messages, store} =>
9.248 - let
9.249 - val timeout_heap' = ThreadHeap.insert (deadtime, thread) timeout_heap
9.250 - val oldest_heap' = ThreadHeap.insert (birthtime, thread) oldest_heap
9.251 - val active' = update_thread (thread, (birthtime, deadtime, desc)) active
9.252 - in make_state managing_thread timeout_heap' oldest_heap' active' cancelling messages store end);
9.253 - check_thread_manager ());
9.254 -
9.255 -
9.256 -
9.257 -(** user commands **)
9.258 -
9.259 -(* kill: move all threads to cancelling *)
9.260 -
9.261 -fun kill () = Synchronized.change state
9.262 - (fn State {managing_thread, timeout_heap, oldest_heap, active, cancelling, messages, store} =>
9.263 - let val formerly_active = map (fn (th, (tb, _, desc)) => (th, (tb, Time.now (), desc))) active
9.264 - in make_state
9.265 - managing_thread timeout_heap oldest_heap [] (formerly_active @ cancelling) messages store
9.266 - end);
9.267 -
9.268 -
9.269 -(* ATP info *)
9.270 -
9.271 -fun info () =
9.272 - let
9.273 - val State {active, cancelling, ...} = Synchronized.value state
9.274 -
9.275 - fun running_info (_, (birth_time, dead_time, desc)) = "Running: "
9.276 - ^ (string_of_int o Time.toSeconds) (Time.- (Time.now (), birth_time))
9.277 - ^ " s -- "
9.278 - ^ (string_of_int o Time.toSeconds) (Time.- (dead_time, Time.now ()))
9.279 - ^ " s to live:\n" ^ desc
9.280 - fun cancelling_info (_, (_, dead_time, desc)) = "Trying to interrupt thread since "
9.281 - ^ (string_of_int o Time.toSeconds) (Time.- (Time.now (), dead_time))
9.282 - ^ " s:\n" ^ desc
9.283 -
9.284 - val running =
9.285 - if null active then "No ATPs running."
9.286 - else space_implode "\n\n" ("Running ATPs:" :: map running_info active)
9.287 - val interrupting =
9.288 - if null cancelling then ""
9.289 - else space_implode "\n\n"
9.290 - ("Trying to interrupt the following ATPs:" :: map cancelling_info cancelling)
9.291 -
9.292 - in writeln (running ^ "\n" ^ interrupting) end;
9.293 -
9.294 -fun messages opt_limit =
9.295 - let
9.296 - val limit = the_default message_display_limit opt_limit;
9.297 - val State {store = msgs, ...} = Synchronized.value state
9.298 - val header = "Recent ATP messages" ^
9.299 - (if length msgs <= limit then ":" else " (" ^ string_of_int limit ^ " displayed):");
9.300 - in writeln (space_implode "\n\n" (header :: #1 (chop limit msgs))) end;
9.301 -
9.302 -
9.303 -
9.304 -(** The Sledgehammer **)
9.305 -
9.306 -(* named provers *)
9.307 -
9.308 -type prover = int -> (thm * (string * int)) list option ->
9.309 - (thm * (string * int)) list option -> string -> int ->
9.310 - Proof.context * (thm list * thm) ->
9.311 - bool * string * string * string vector * (thm * (string * int)) list
9.312 -
9.313 -fun err_dup_prover name = error ("Duplicate prover: " ^ quote name);
9.314 -
9.315 -structure Provers = TheoryDataFun
9.316 -(
9.317 - type T = (prover * stamp) Symtab.table
9.318 - val empty = Symtab.empty
9.319 - val copy = I
9.320 - val extend = I
9.321 - fun merge _ tabs : T = Symtab.merge (eq_snd op =) tabs
9.322 - handle Symtab.DUP dup => err_dup_prover dup
9.323 -);
9.324 -
9.325 -fun add_prover name prover thy =
9.326 - Provers.map (Symtab.update_new (name, (prover, stamp ()))) thy
9.327 - handle Symtab.DUP dup => err_dup_prover dup;
9.328 -
9.329 -fun print_provers thy = Pretty.writeln
9.330 - (Pretty.strs ("external provers:" :: sort_strings (Symtab.keys (Provers.get thy))));
9.331 -
9.332 -fun get_prover name thy = case Symtab.lookup (Provers.get thy) name of
9.333 - NONE => NONE
9.334 -| SOME (prover, _) => SOME prover;
9.335 -
9.336 -(* start prover thread *)
9.337 -
9.338 -fun start_prover name birthtime deadtime i proof_state =
9.339 - (case get_prover name (Proof.theory_of proof_state) of
9.340 - NONE => warning ("Unknown external prover: " ^ quote name)
9.341 - | SOME prover =>
9.342 - let
9.343 - val (ctxt, (_, goal)) = Proof.get_goal proof_state
9.344 - val desc =
9.345 - "external prover " ^ quote name ^ " for subgoal " ^ string_of_int i ^ ":\n" ^
9.346 - Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i))
9.347 - val _ = SimpleThread.fork true (fn () =>
9.348 - let
9.349 - val _ = register birthtime deadtime (Thread.self (), desc)
9.350 - val result =
9.351 - let val (success, message, _, _, _) =
9.352 - prover (get_timeout ()) NONE NONE name i (Proof.get_goal proof_state)
9.353 - in (success, message) end
9.354 - handle ResHolClause.TOO_TRIVIAL
9.355 - => (true, "Empty clause: Try this command: " ^ Markup.markup Markup.sendback "apply metis")
9.356 - | ERROR msg
9.357 - => (false, "Error: " ^ msg)
9.358 - val _ = unregister result (Thread.self ())
9.359 - in () end handle Interrupt => ())
9.360 - in () end);
9.361 -
9.362 -
9.363 -(* sledghammer for first subgoal *)
9.364 -
9.365 -fun sledgehammer names proof_state =
9.366 - let
9.367 - val provers =
9.368 - if null names then String.tokens (Symbol.is_ascii_blank o String.str) (get_atps ())
9.369 - else names
9.370 - val birthtime = Time.now ()
9.371 - val deadtime = Time.+ (birthtime, Time.fromSeconds (get_timeout ()))
9.372 - in List.app (fn name => start_prover name birthtime deadtime 1 proof_state) provers end;
9.373 -
9.374 -
9.375 -
9.376 -(** Isar command syntax **)
9.377 -
9.378 -local structure K = OuterKeyword and P = OuterParse in
9.379 -
9.380 -val _ =
9.381 - OuterSyntax.improper_command "atp_kill" "kill all managed provers" K.diag
9.382 - (Scan.succeed (Toplevel.no_timing o Toplevel.imperative kill));
9.383 -
9.384 -val _ =
9.385 - OuterSyntax.improper_command "atp_info" "print information about managed provers" K.diag
9.386 - (Scan.succeed (Toplevel.no_timing o Toplevel.imperative info));
9.387 -
9.388 -val _ =
9.389 - OuterSyntax.improper_command "atp_messages" "print recent messages issued by managed provers" K.diag
9.390 - (Scan.option (P.$$$ "(" |-- P.nat --| P.$$$ ")") >>
9.391 - (fn limit => Toplevel.no_timing o Toplevel.imperative (fn () => messages limit)));
9.392 -
9.393 -val _ =
9.394 - OuterSyntax.improper_command "print_atps" "print external provers" K.diag
9.395 - (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_theory o
9.396 - Toplevel.keep (print_provers o Toplevel.theory_of)));
9.397 -
9.398 -val _ =
9.399 - OuterSyntax.command "sledgehammer" "call all automatic theorem provers" K.diag
9.400 - (Scan.repeat P.xname >> (fn names => Toplevel.no_timing o Toplevel.unknown_proof o
9.401 - Toplevel.keep (sledgehammer names o Toplevel.proof_of)));
9.402 -
9.403 -end;
9.404 -
9.405 -end;
9.406 -
10.1 --- a/src/HOL/Tools/atp_minimal.ML Tue Aug 04 16:13:16 2009 +0200
10.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
10.3 @@ -1,223 +0,0 @@
10.4 -(* Title: HOL/Tools/atp_minimal.ML
10.5 - Author: Philipp Meyer, TU Muenchen
10.6 -
10.7 -Minimalization of theorem list for metis by using an external automated theorem prover
10.8 -*)
10.9 -
10.10 -structure AtpMinimal: sig end =
10.11 -struct
10.12 -
10.13 -(* output control *)
10.14 -
10.15 -fun debug str = Output.debug (fn () => str)
10.16 -fun debug_fn f = if ! Output.debugging then f () else ()
10.17 -fun answer str = Output.writeln str
10.18 -fun println str = Output.priority str
10.19 -
10.20 -fun order_unique name_list = OrdList.make (String.collate Char.compare) name_list
10.21 -fun length_string namelist = Int.toString (length namelist)
10.22 -
10.23 -fun print_names name_thms_pairs =
10.24 - let
10.25 - val names = map fst name_thms_pairs
10.26 - val ordered = order_unique names
10.27 - in
10.28 - app (fn name => (debug (" " ^ name))) ordered
10.29 - end
10.30 -
10.31 -
10.32 -(* minimalization algorithm *)
10.33 -
10.34 -local
10.35 - fun isplit (l,r) [] = (l,r)
10.36 - | isplit (l,r) (h::[]) = (h::l, r)
10.37 - | isplit (l,r) (h1::h2::t) = isplit (h1::l, h2::r) t
10.38 -in
10.39 - fun split lst = isplit ([],[]) lst
10.40 -end
10.41 -
10.42 -local
10.43 - fun min p sup [] = raise Empty
10.44 - | min p sup [s0] = [s0]
10.45 - | min p sup s =
10.46 - let
10.47 - val (l0, r0) = split s
10.48 - in
10.49 - if p (sup @ l0)
10.50 - then min p sup l0
10.51 - else
10.52 - if p (sup @ r0)
10.53 - then min p sup r0
10.54 - else
10.55 - let
10.56 - val l = min p (sup @ r0) l0
10.57 - val r = min p (sup @ l) r0
10.58 - in
10.59 - l @ r
10.60 - end
10.61 - end
10.62 -in
10.63 - (* return a minimal subset v of s that satisfies p
10.64 - @pre p(s) & ~p([]) & monotone(p)
10.65 - @post v subset s & p(v) &
10.66 - forall e in v. ~p(v \ e)
10.67 - *)
10.68 - fun minimal p s = min p [] s
10.69 -end
10.70 -
10.71 -
10.72 -(* failure check and producing answer *)
10.73 -
10.74 -datatype 'a prove_result = Success of 'a | Failure | Timeout | Error
10.75 -
10.76 -val string_of_result =
10.77 - fn Success _ => "Success"
10.78 - | Failure => "Failure"
10.79 - | Timeout => "Timeout"
10.80 - | Error => "Error"
10.81 -
10.82 -val failure_strings =
10.83 - [("SPASS beiseite: Ran out of time.", Timeout),
10.84 - ("Timeout", Timeout),
10.85 - ("time limit exceeded", Timeout),
10.86 - ("# Cannot determine problem status within resource limit", Timeout),
10.87 - ("Error", Error)]
10.88 -
10.89 -fun produce_answer (success, message, result_string, thm_name_vec, filtered) =
10.90 - if success then
10.91 - (Success (Vector.foldr op:: [] thm_name_vec, filtered), result_string)
10.92 - else
10.93 - let
10.94 - val failure = failure_strings |> get_first (fn (s, t) =>
10.95 - if String.isSubstring s result_string then SOME (t, result_string) else NONE)
10.96 - in
10.97 - if is_some failure then
10.98 - the failure
10.99 - else
10.100 - (Failure, result_string)
10.101 - end
10.102 -
10.103 -
10.104 -(* wrapper for calling external prover *)
10.105 -
10.106 -fun sh_test_thms prover prover_name time_limit subgoalno state filtered name_thms_pairs =
10.107 - let
10.108 - val _ = println ("Testing " ^ (length_string name_thms_pairs) ^ " theorems... ")
10.109 - val name_thm_pairs =
10.110 - flat (map (fn (n, ths) => map_index (fn (i, th) => (n, th)) ths) name_thms_pairs)
10.111 - val _ = debug_fn (fn () => print_names name_thm_pairs)
10.112 - val axclauses = ResAxioms.cnf_rules_pairs (Proof.theory_of state) name_thm_pairs
10.113 - val (result, proof) =
10.114 - produce_answer
10.115 - (prover time_limit (SOME axclauses) filtered prover_name subgoalno (Proof.get_goal state))
10.116 - val _ = println (string_of_result result)
10.117 - val _ = debug proof
10.118 - in
10.119 - (result, proof)
10.120 - end
10.121 -
10.122 -
10.123 -(* minimalization of thms *)
10.124 -
10.125 -fun minimalize prover prover_name time_limit state name_thms_pairs =
10.126 - let
10.127 - val _ =
10.128 - println ("Minimize called with " ^ length_string name_thms_pairs ^ " theorems, prover: "
10.129 - ^ prover_name ^ ", time limit: " ^ Int.toString time_limit ^ " seconds")
10.130 - val _ = debug_fn (fn () => app (fn (n, tl) =>
10.131 - (debug n; app (fn t =>
10.132 - debug (" " ^ Display.string_of_thm (Proof.context_of state) t)) tl)) name_thms_pairs)
10.133 - val test_thms_fun = sh_test_thms prover prover_name time_limit 1 state
10.134 - fun test_thms filtered thms =
10.135 - case test_thms_fun filtered thms of (Success _, _) => true | _ => false
10.136 - in
10.137 - (* try prove first to check result and get used theorems *)
10.138 - (case test_thms_fun NONE name_thms_pairs of
10.139 - (Success (used, filtered), _) =>
10.140 - let
10.141 - val ordered_used = order_unique used
10.142 - val to_use =
10.143 - if length ordered_used < length name_thms_pairs then
10.144 - filter (fn (name1, _) => List.exists (equal name1) ordered_used) name_thms_pairs
10.145 - else
10.146 - name_thms_pairs
10.147 - val min_thms = (minimal (test_thms (SOME filtered)) to_use)
10.148 - val min_names = order_unique (map fst min_thms)
10.149 - val _ = println ("Minimal " ^ (length_string min_thms) ^ " theorems")
10.150 - val _ = debug_fn (fn () => print_names min_thms)
10.151 - in
10.152 - answer ("Try this command: " ^
10.153 - Markup.markup Markup.sendback ("apply (metis " ^ space_implode " " min_names ^ ")"))
10.154 - end
10.155 - | (Timeout, _) =>
10.156 - answer ("Timeout: You may need to increase the time limit of " ^
10.157 - Int.toString time_limit ^ " seconds. Call atp_minimize [time=...] ")
10.158 - | (Error, msg) =>
10.159 - answer ("Error in prover: " ^ msg)
10.160 - | (Failure, _) =>
10.161 - answer "Failure: No proof with the theorems supplied")
10.162 - handle ResHolClause.TOO_TRIVIAL =>
10.163 - answer ("Trivial: Try this command: " ^ Markup.markup Markup.sendback "apply metis")
10.164 - | ERROR msg =>
10.165 - answer ("Error: " ^ msg)
10.166 - end
10.167 -
10.168 -
10.169 -(* Isar command and parsing input *)
10.170 -
10.171 -local structure K = OuterKeyword and P = OuterParse and T = OuterLex in
10.172 -
10.173 -fun get_thms context =
10.174 - map (fn (name, interval) =>
10.175 - let
10.176 - val thmref = Facts.Named ((name, Position.none), interval)
10.177 - val ths = ProofContext.get_fact context thmref
10.178 - val name' = Facts.string_of_ref thmref
10.179 - in
10.180 - (name', ths)
10.181 - end)
10.182 -
10.183 -val default_prover = "remote_vampire"
10.184 -val default_time_limit = 5
10.185 -
10.186 -fun get_time_limit_arg time_string =
10.187 - (case Int.fromString time_string of
10.188 - SOME t => t
10.189 - | NONE => error ("Invalid time limit: " ^ quote time_string))
10.190 -
10.191 -val get_options =
10.192 - let
10.193 - val def = (default_prover, default_time_limit)
10.194 - in
10.195 - foldl (fn ((name, a), (p, t)) =>
10.196 - (case name of
10.197 - "time" => (p, (get_time_limit_arg a))
10.198 - | "atp" => (a, t)
10.199 - | n => error ("Invalid argument: " ^ n))) def
10.200 - end
10.201 -
10.202 -fun sh_min_command args thm_names state =
10.203 - let
10.204 - val (prover_name, time_limit) = get_options args
10.205 - val prover =
10.206 - case AtpManager.get_prover prover_name (Proof.theory_of state) of
10.207 - SOME prover => prover
10.208 - | NONE => error ("Unknown prover: " ^ quote prover_name)
10.209 - val name_thms_pairs = get_thms (Proof.context_of state) thm_names
10.210 - in
10.211 - minimalize prover prover_name time_limit state name_thms_pairs
10.212 - end
10.213 -
10.214 -val parse_args = Scan.optional (Args.bracks (P.list (P.xname --| P.$$$ "=" -- P.xname))) []
10.215 -val parse_thm_names = Scan.repeat (P.xname -- Scan.option Attrib.thm_sel)
10.216 -
10.217 -val _ =
10.218 - OuterSyntax.command "atp_minimize" "minimize theorem list with external prover" K.diag
10.219 - (parse_args -- parse_thm_names >> (fn (args, thm_names) =>
10.220 - Toplevel.no_timing o Toplevel.unknown_proof o
10.221 - Toplevel.keep (sh_min_command args thm_names o Toplevel.proof_of)))
10.222 -
10.223 -end
10.224 -
10.225 -end
10.226 -
11.1 --- a/src/HOL/Tools/atp_wrapper.ML Tue Aug 04 16:13:16 2009 +0200
11.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
11.3 @@ -1,218 +0,0 @@
11.4 -(* Title: HOL/Tools/atp_wrapper.ML
11.5 - Author: Fabian Immler, TU Muenchen
11.6 -
11.7 -Wrapper functions for external ATPs.
11.8 -*)
11.9 -
11.10 -signature ATP_WRAPPER =
11.11 -sig
11.12 - val destdir: string ref
11.13 - val problem_name: string ref
11.14 - val tptp_prover_opts_full: int -> bool -> bool -> Path.T * string -> AtpManager.prover
11.15 - val tptp_prover_opts: int -> bool -> Path.T * string -> AtpManager.prover
11.16 - val tptp_prover: Path.T * string -> AtpManager.prover
11.17 - val full_prover_opts: int -> bool -> Path.T * string -> AtpManager.prover
11.18 - val full_prover: Path.T * string -> AtpManager.prover
11.19 - val vampire_opts: int -> bool -> AtpManager.prover
11.20 - val vampire: AtpManager.prover
11.21 - val vampire_opts_full: int -> bool -> AtpManager.prover
11.22 - val vampire_full: AtpManager.prover
11.23 - val eprover_opts: int -> bool -> AtpManager.prover
11.24 - val eprover: AtpManager.prover
11.25 - val eprover_opts_full: int -> bool -> AtpManager.prover
11.26 - val eprover_full: AtpManager.prover
11.27 - val spass_opts: int -> bool -> AtpManager.prover
11.28 - val spass: AtpManager.prover
11.29 - val remote_prover_opts: int -> bool -> string -> string -> AtpManager.prover
11.30 - val remote_prover: string -> string -> AtpManager.prover
11.31 - val refresh_systems: unit -> unit
11.32 -end;
11.33 -
11.34 -structure AtpWrapper: ATP_WRAPPER =
11.35 -struct
11.36 -
11.37 -(** generic ATP wrapper **)
11.38 -
11.39 -(* global hooks for writing problemfiles *)
11.40 -
11.41 -val destdir = ref ""; (*Empty means write files to /tmp*)
11.42 -val problem_name = ref "prob";
11.43 -
11.44 -
11.45 -(* basic template *)
11.46 -
11.47 -fun external_prover relevance_filter preparer writer (cmd, args) find_failure produce_answer
11.48 - timeout axiom_clauses filtered_clauses name subgoalno goal =
11.49 - let
11.50 - (* path to unique problem file *)
11.51 - val destdir' = ! destdir
11.52 - val problem_name' = ! problem_name
11.53 - fun prob_pathname nr =
11.54 - let val probfile = Path.basic (problem_name' ^ serial_string () ^ "_" ^ string_of_int nr)
11.55 - in if destdir' = "" then File.tmp_path probfile
11.56 - else if File.exists (Path.explode (destdir'))
11.57 - then Path.append (Path.explode (destdir')) probfile
11.58 - else error ("No such directory: " ^ destdir')
11.59 - end
11.60 -
11.61 - (* get clauses and prepare them for writing *)
11.62 - val (ctxt, (chain_ths, th)) = goal
11.63 - val thy = ProofContext.theory_of ctxt
11.64 - val chain_ths = map (Thm.put_name_hint ResReconstruct.chained_hint) chain_ths
11.65 - val goal_cls = #1 (ResAxioms.neg_conjecture_clauses ctxt th subgoalno)
11.66 - val _ = app (fn th => Output.debug (fn _ => Display.string_of_thm ctxt th)) goal_cls
11.67 - val the_filtered_clauses =
11.68 - case filtered_clauses of
11.69 - NONE => relevance_filter goal goal_cls
11.70 - | SOME fcls => fcls
11.71 - val the_axiom_clauses =
11.72 - case axiom_clauses of
11.73 - NONE => the_filtered_clauses
11.74 - | SOME axcls => axcls
11.75 - val (thm_names, clauses) =
11.76 - preparer goal_cls chain_ths the_axiom_clauses the_filtered_clauses thy
11.77 -
11.78 - (* write out problem file and call prover *)
11.79 - val probfile = prob_pathname subgoalno
11.80 - val conj_pos = writer probfile clauses
11.81 - val (proof, rc) = system_out (
11.82 - if File.exists cmd then
11.83 - space_implode " " ["exec", File.shell_path cmd, args, File.platform_path probfile]
11.84 - else error ("Bad executable: " ^ Path.implode cmd))
11.85 -
11.86 - (* if problemfile has not been exported, delete problemfile; otherwise export proof, too *)
11.87 - val _ =
11.88 - if destdir' = "" then File.rm probfile
11.89 - else File.write (Path.explode (Path.implode probfile ^ "_proof")) proof
11.90 -
11.91 - (* check for success and print out some information on failure *)
11.92 - val failure = find_failure proof
11.93 - val success = rc = 0 andalso is_none failure
11.94 - val message =
11.95 - if is_some failure then "External prover failed."
11.96 - else if rc <> 0 then "External prover failed: " ^ proof
11.97 - else "Try this command: " ^
11.98 - produce_answer name (proof, thm_names, conj_pos, ctxt, th, subgoalno)
11.99 - val _ = Output.debug (fn () => "Sledgehammer response (rc = " ^ string_of_int rc ^ "):\n" ^ proof)
11.100 - in (success, message, proof, thm_names, the_filtered_clauses) end;
11.101 -
11.102 -
11.103 -
11.104 -(** common provers **)
11.105 -
11.106 -(* generic TPTP-based provers *)
11.107 -
11.108 -fun tptp_prover_opts_full max_new theory_const full command timeout ax_clauses fcls name n goal =
11.109 - external_prover
11.110 - (ResAtp.get_relevant max_new theory_const)
11.111 - (ResAtp.prepare_clauses false)
11.112 - (ResHolClause.tptp_write_file (AtpManager.get_full_types()))
11.113 - command
11.114 - ResReconstruct.find_failure
11.115 - (if full then ResReconstruct.structured_proof else ResReconstruct.lemma_list false)
11.116 - timeout ax_clauses fcls name n goal;
11.117 -
11.118 -(*arbitrary ATP with TPTP input/output and problemfile as last argument*)
11.119 -fun tptp_prover_opts max_new theory_const =
11.120 - tptp_prover_opts_full max_new theory_const false;
11.121 -
11.122 -fun tptp_prover x = tptp_prover_opts 60 true x;
11.123 -
11.124 -(*for structured proofs: prover must support TSTP*)
11.125 -fun full_prover_opts max_new theory_const =
11.126 - tptp_prover_opts_full max_new theory_const true;
11.127 -
11.128 -fun full_prover x = full_prover_opts 60 true x;
11.129 -
11.130 -
11.131 -(* Vampire *)
11.132 -
11.133 -(*NB: Vampire does not work without explicit timelimit*)
11.134 -
11.135 -fun vampire_opts max_new theory_const timeout = tptp_prover_opts
11.136 - max_new theory_const
11.137 - (Path.explode "$VAMPIRE_HOME/vampire",
11.138 - ("--output_syntax tptp --mode casc -t " ^ string_of_int timeout))
11.139 - timeout;
11.140 -
11.141 -val vampire = vampire_opts 60 false;
11.142 -
11.143 -fun vampire_opts_full max_new theory_const timeout = full_prover_opts
11.144 - max_new theory_const
11.145 - (Path.explode "$VAMPIRE_HOME/vampire",
11.146 - ("--output_syntax tptp --mode casc -t " ^ string_of_int timeout))
11.147 - timeout;
11.148 -
11.149 -val vampire_full = vampire_opts_full 60 false;
11.150 -
11.151 -
11.152 -(* E prover *)
11.153 -
11.154 -fun eprover_opts max_new theory_const timeout = tptp_prover_opts
11.155 - max_new theory_const
11.156 - (Path.explode "$E_HOME/eproof",
11.157 - "--tstp-in --tstp-out -l5 -xAutoDev -tAutoDev --silent --cpu-limit=" ^ string_of_int timeout)
11.158 - timeout;
11.159 -
11.160 -val eprover = eprover_opts 100 false;
11.161 -
11.162 -fun eprover_opts_full max_new theory_const timeout = full_prover_opts
11.163 - max_new theory_const
11.164 - (Path.explode "$E_HOME/eproof",
11.165 - "--tstp-in --tstp-out -l5 -xAutoDev -tAutoDev --silent --cpu-limit=" ^ string_of_int timeout)
11.166 - timeout;
11.167 -
11.168 -val eprover_full = eprover_opts_full 100 false;
11.169 -
11.170 -
11.171 -(* SPASS *)
11.172 -
11.173 -fun spass_opts max_new theory_const timeout ax_clauses fcls name n goal = external_prover
11.174 - (ResAtp.get_relevant max_new theory_const)
11.175 - (ResAtp.prepare_clauses true)
11.176 - (ResHolClause.dfg_write_file (AtpManager.get_full_types()))
11.177 - (Path.explode "$SPASS_HOME/SPASS",
11.178 - "-Auto -SOS=1 -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof -TimeLimit=" ^
11.179 - string_of_int timeout)
11.180 - ResReconstruct.find_failure
11.181 - (ResReconstruct.lemma_list true)
11.182 - timeout ax_clauses fcls name n goal;
11.183 -
11.184 -val spass = spass_opts 40 true;
11.185 -
11.186 -
11.187 -(* remote prover invocation via SystemOnTPTP *)
11.188 -
11.189 -val systems =
11.190 - Synchronized.var "atp_wrapper_systems" ([]: string list);
11.191 -
11.192 -fun get_systems () =
11.193 - let
11.194 - val (answer, rc) = system_out (("$ISABELLE_HOME/lib/scripts/SystemOnTPTP" |>
11.195 - Path.explode |> File.shell_path) ^ " -w")
11.196 - in
11.197 - if rc <> 0 then error ("Get available systems from SystemOnTPTP:\n" ^ answer)
11.198 - else split_lines answer
11.199 - end;
11.200 -
11.201 -fun refresh_systems () = Synchronized.change systems (fn _ =>
11.202 - get_systems ());
11.203 -
11.204 -fun get_system prefix = Synchronized.change_result systems (fn systems =>
11.205 - let val systems = if null systems then get_systems() else systems
11.206 - in (find_first (String.isPrefix prefix) systems, systems) end);
11.207 -
11.208 -fun remote_prover_opts max_new theory_const args prover_prefix timeout =
11.209 - let val sys =
11.210 - case get_system prover_prefix of
11.211 - NONE => error ("No system like " ^ quote prover_prefix ^ " at SystemOnTPTP")
11.212 - | SOME sys => sys
11.213 - in tptp_prover_opts max_new theory_const
11.214 - (Path.explode "$ISABELLE_HOME/lib/scripts/SystemOnTPTP",
11.215 - args ^ " -t " ^ string_of_int timeout ^ " -s " ^ sys) timeout
11.216 - end;
11.217 -
11.218 -val remote_prover = remote_prover_opts 60 false;
11.219 -
11.220 -end;
11.221 -