src/HOL/Tools/ATP_Manager as separate component, with (almost) everything in one place;
authorwenzelm
Tue Aug 04 19:20:24 2009 +0200 (2009-08-04)
changeset 323270971cc0b6a57
parent 32326 9d70ecf11b7a
child 32328 f2fd9da84bac
child 32329 1527ff8c2dfb
src/HOL/Tools/ATP_Manager as separate component, with (almost) everything in one place;
etc/components
lib/scripts/SystemOnTPTP
src/HOL/ATP_Linkup.thy
src/HOL/IsaMakefile
src/HOL/Tools/ATP_Manager/SystemOnTPTP
src/HOL/Tools/ATP_Manager/atp_manager.ML
src/HOL/Tools/ATP_Manager/atp_minimal.ML
src/HOL/Tools/ATP_Manager/atp_wrapper.ML
src/HOL/Tools/atp_manager.ML
src/HOL/Tools/atp_minimal.ML
src/HOL/Tools/atp_wrapper.ML
     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 -