remove "remote_spass" because there's no way to find out which clauses come from which facts + rename scripts
--- a/src/HOL/Tools/ATP_Manager/SPASS_TPTP Wed Jul 28 18:07:25 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,19 +0,0 @@
-#!/usr/bin/env bash
-#
-# Wrapper for SPASS that also outputs the Flotter-generated CNF (needed for
-# Isar proof reconstruction)
-#
-# Author: Jasmin Blanchette, TU Muenchen
-
-options=${@:1:$(($#-1))}
-name=${@:$(($#)):1}
-
-$SPASS_HOME/tptp2dfg $name $name.fof.dfg
-$SPASS_HOME/SPASS -Flotter $name.fof.dfg \
- | sed 's/description({$/description({*/' \
- > $name.cnf.dfg
-rm -f $name.fof.dfg
-cat $name.cnf.dfg
-$SPASS_HOME/SPASS $options $name.cnf.dfg \
- | sed 's/\(Formulae used in the proof :\).*/\1 N\/A/'
-rm -f $name.cnf.dfg
--- a/src/HOL/Tools/ATP_Manager/SystemOnTPTP Wed Jul 28 18:07:25 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,142 +0,0 @@
-#!/usr/bin/env perl
-#
-# Wrapper for custom remote provers on SystemOnTPTP
-# Author: Fabian Immler, TU Muenchen
-#
-
-use warnings;
-use strict;
-use Getopt::Std;
-use HTTP::Request::Common;
-use LWP;
-
-my $SystemOnTPTPFormReplyURL =
- "http://www.cs.miami.edu/~tptp/cgi-bin/SystemOnTPTPFormReply";
-
-# default parameters
-my %URLParameters = (
- "NoHTML" => 1,
- "QuietFlag" => "-q01",
- "SubmitButton" => "RunSelectedSystems",
- "ProblemSource" => "UPLOAD",
- "ForceSystem" => "-force",
- );
-
-#----Get format and transform options if specified
-my %Options;
-getopts("hwxs:t:c:",\%Options);
-
-#----Usage
-sub usage() {
- print("Usage: remote [<options>] <File name>\n");
- print(" <options> are ...\n");
- print(" -h - print this help\n");
- print(" -w - list available ATP systems\n");
- print(" -x - use X2TPTP to convert output of prover\n");
- print(" -s<system> - specified system to use\n");
- print(" -t<timelimit> - CPU time limit for system\n");
- print(" -c<command> - custom command for system\n");
- print(" <File name> - TPTP problem file\n");
- exit(0);
-}
-if (exists($Options{'h'})) {
- usage();
-}
-
-#----What systems flag
-if (exists($Options{'w'})) {
- $URLParameters{"SubmitButton"} = "ListSystems";
- delete($URLParameters{"ProblemSource"});
-}
-
-#----X2TPTP
-if (exists($Options{'x'})) {
- $URLParameters{"X2TPTP"} = "-S";
-}
-
-#----Selected system
-my $System;
-if (exists($Options{'s'})) {
- $System = $Options{'s'};
-} else {
- # use Vampire as default
- $System = "Vampire---9.0";
-}
-$URLParameters{"System___$System"} = $System;
-
-#----Time limit
-if (exists($Options{'t'})) {
- $URLParameters{"TimeLimit___$System"} = $Options{'t'};
-}
-#----Custom command
-if (exists($Options{'c'})) {
- $URLParameters{"Command___$System"} = $Options{'c'};
-}
-
-#----Get single file name
-if (exists($URLParameters{"ProblemSource"})) {
- if (scalar(@ARGV) >= 1) {
- $URLParameters{"UPLOADProblem"} = [shift(@ARGV)];
- } else {
- print("Missing problem file\n");
- usage();
- die;
- }
-}
-
-# Query Server
-my $Agent = LWP::UserAgent->new;
-if (exists($Options{'t'})) {
- # give server more time to respond
- $Agent->timeout($Options{'t'} + 10);
-}
-my $Request = POST($SystemOnTPTPFormReplyURL,
- Content_Type => 'form-data',Content => \%URLParameters);
-my $Response = $Agent->request($Request);
-
-#catch errors / failure
-if(!$Response->is_success) {
- print "HTTP-Error: " . $Response->message . "\n";
- exit(-1);
-} elsif (exists($Options{'w'})) {
- print $Response->content;
- exit (0);
-} elsif ($Response->content =~ /WARNING: (\S*) does not exist/) {
- print "Specified System $1 does not exist\n";
- exit(-1);
-} elsif (exists($Options{'x'}) &&
- $Response->content =~
- /%\s*Result\s*:\s*(Unsatisfiable|Theorem).*\n%\s*Output\s*:\s*(CNF)?Refutation.*\n%/ &&
- $Response->content !~ /ERROR: Could not form TPTP format derivation/ )
-{
- # converted output: extract proof
- my @lines = split( /\n/, $Response->content);
- my $extract = "";
- foreach my $line (@lines){
- #ignore comments
- if ($line !~ /^%/ && !($line eq "")) {
- $extract .= "$line";
- }
- }
- # insert newlines after ').'
- $extract =~ s/\s//g;
- $extract =~ s/\)\.cnf/\)\.\ncnf/g;
-
- print "========== ~~/lib/scripts/SystemOnTPTP extracted proof: ==========\n";
- # orientation for "sledgehammer_proof_reconstruct.ML"
- print "# SZS output start CNFRefutation.\n";
- print "$extract\n";
- print "# SZS output end CNFRefutation.\n";
- # can be useful for debugging; Isabelle ignores this
- print "============== original response from SystemOnTPTP: ==============\n";
- print $Response->content;
- exit(0);
-} elsif (!exists($Options{'x'})) {
- # pass output directly to Isabelle
- print $Response->content;
- exit(0);
-}else {
- print "Remote script could not extract proof:\n".$Response->content;
- exit(-1);
-}
-
--- a/src/HOL/Tools/ATP_Manager/atp_systems.ML Wed Jul 28 18:07:25 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_systems.ML Wed Jul 28 18:32:54 2010 +0200
@@ -108,7 +108,7 @@
(* The "-VarWeight=3" option helps the higher-order problems, probably by
counteracting the presence of "hAPP". *)
val spass_config : prover_config =
- {executable = ("ISABELLE_ATP_MANAGER", "SPASS_TPTP"),
+ {executable = ("ISABELLE_ATP_MANAGER", "scripts/spass"),
required_executables = [("SPASS_HOME", "SPASS")],
(* "div 2" accounts for the fact that SPASS is often run twice. *)
arguments = fn complete => fn timeout =>
@@ -157,7 +157,7 @@
val systems = Synchronized.var "atp_systems" ([]: string list)
fun get_systems () =
- case bash_output "\"$ISABELLE_ATP_MANAGER/SystemOnTPTP\" -w" of
+ case bash_output "\"$ISABELLE_ATP_MANAGER/scripts/remote_atp\" -w" of
(answer, 0) => split_lines answer
| (answer, _) =>
error ("Failed to get available systems at SystemOnTPTP:\n" ^
@@ -180,14 +180,14 @@
(TimedOut, "says Timeout"),
(MalformedOutput, "Remote script could not extract proof")]
-fun remote_config atp_prefix args
+fun remote_config atp_prefix
({proof_delims, known_failures, max_new_relevant_facts_per_iter,
prefers_theory_relevant, explicit_forall, ...} : prover_config)
: prover_config =
- {executable = ("ISABELLE_ATP_MANAGER", "SystemOnTPTP"),
+ {executable = ("ISABELLE_ATP_MANAGER", "scripts/remote_atp"),
required_executables = [],
arguments = fn _ => fn timeout =>
- args ^ " -t " ^ string_of_int (to_generous_secs timeout) ^ " -s " ^
+ " -t " ^ string_of_int (to_generous_secs timeout) ^ " -s " ^
the_system atp_prefix,
proof_delims = insert (op =) tstp_proof_delims proof_delims,
known_failures = remote_known_failures @ known_failures,
@@ -197,23 +197,23 @@
val remote_name = prefix "remote_"
-fun remote_prover prover atp_prefix args config =
- (remote_name (fst prover), remote_config atp_prefix args config)
+fun remote_prover (name, config) atp_prefix =
+ (remote_name name, remote_config atp_prefix config)
-val remote_e = remote_prover e "EP---" "" e_config
-val remote_spass = remote_prover spass "SPASS---" "-x" spass_config
-val remote_vampire = remote_prover vampire "Vampire---9" "" vampire_config
+val remote_e = remote_prover e "EP---"
+val remote_vampire = remote_prover vampire "Vampire---9"
-fun maybe_remote (name, _)
- ({executable, required_executables, ...} : prover_config) =
- name |> exists (curry (op =) "" o getenv o fst)
- (executable :: required_executables) ? remote_name
+fun is_installed ({executable, required_executables, ...} : prover_config) =
+ forall (curry (op <>) "" o getenv o fst) (executable :: required_executables)
+fun maybe_remote (name, config) =
+ name |> not (is_installed config) ? remote_name
fun default_atps_param_value () =
- space_implode " " [maybe_remote e e_config, maybe_remote spass spass_config,
- remote_name (fst vampire)]
+ space_implode " " ([maybe_remote e] @
+ (if is_installed (snd spass) then [fst spass] else []) @
+ [remote_name (fst vampire)])
-val provers = [e, spass, vampire, remote_e, remote_spass, remote_vampire]
+val provers = [e, spass, vampire, remote_e, remote_vampire]
val setup = fold add_prover provers
end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/ATP_Manager/scripts/remote_atp Wed Jul 28 18:32:54 2010 +0200
@@ -0,0 +1,142 @@
+#!/usr/bin/env perl
+#
+# Wrapper for custom remote provers on SystemOnTPTP
+# Author: Fabian Immler, TU Muenchen
+#
+
+use warnings;
+use strict;
+use Getopt::Std;
+use HTTP::Request::Common;
+use LWP;
+
+my $SystemOnTPTPFormReplyURL =
+ "http://www.cs.miami.edu/~tptp/cgi-bin/SystemOnTPTPFormReply";
+
+# default parameters
+my %URLParameters = (
+ "NoHTML" => 1,
+ "QuietFlag" => "-q01",
+ "SubmitButton" => "RunSelectedSystems",
+ "ProblemSource" => "UPLOAD",
+ "ForceSystem" => "-force",
+ );
+
+#----Get format and transform options if specified
+my %Options;
+getopts("hwxs:t:c:",\%Options);
+
+#----Usage
+sub usage() {
+ print("Usage: remote_atp [<options>] <File name>\n");
+ print(" <options> are ...\n");
+ print(" -h - print this help\n");
+ print(" -w - list available ATP systems\n");
+ print(" -x - use X2TPTP to convert output of prover\n");
+ print(" -s<system> - specified system to use\n");
+ print(" -t<timelimit> - CPU time limit for system\n");
+ print(" -c<command> - custom command for system\n");
+ print(" <File name> - TPTP problem file\n");
+ exit(0);
+}
+if (exists($Options{'h'})) {
+ usage();
+}
+
+#----What systems flag
+if (exists($Options{'w'})) {
+ $URLParameters{"SubmitButton"} = "ListSystems";
+ delete($URLParameters{"ProblemSource"});
+}
+
+#----X2TPTP
+if (exists($Options{'x'})) {
+ $URLParameters{"X2TPTP"} = "-S";
+}
+
+#----Selected system
+my $System;
+if (exists($Options{'s'})) {
+ $System = $Options{'s'};
+} else {
+ # use Vampire as default
+ $System = "Vampire---9.0";
+}
+$URLParameters{"System___$System"} = $System;
+
+#----Time limit
+if (exists($Options{'t'})) {
+ $URLParameters{"TimeLimit___$System"} = $Options{'t'};
+}
+#----Custom command
+if (exists($Options{'c'})) {
+ $URLParameters{"Command___$System"} = $Options{'c'};
+}
+
+#----Get single file name
+if (exists($URLParameters{"ProblemSource"})) {
+ if (scalar(@ARGV) >= 1) {
+ $URLParameters{"UPLOADProblem"} = [shift(@ARGV)];
+ } else {
+ print("Missing problem file\n");
+ usage();
+ die;
+ }
+}
+
+# Query Server
+my $Agent = LWP::UserAgent->new;
+if (exists($Options{'t'})) {
+ # give server more time to respond
+ $Agent->timeout($Options{'t'} + 10);
+}
+my $Request = POST($SystemOnTPTPFormReplyURL,
+ Content_Type => 'form-data',Content => \%URLParameters);
+my $Response = $Agent->request($Request);
+
+#catch errors / failure
+if(!$Response->is_success) {
+ print "HTTP-Error: " . $Response->message . "\n";
+ exit(-1);
+} elsif (exists($Options{'w'})) {
+ print $Response->content;
+ exit (0);
+} elsif ($Response->content =~ /WARNING: (\S*) does not exist/) {
+ print "Specified System $1 does not exist\n";
+ exit(-1);
+} elsif (exists($Options{'x'}) &&
+ $Response->content =~
+ /%\s*Result\s*:\s*(Unsatisfiable|Theorem).*\n%\s*Output\s*:\s*(CNF)?Refutation.*\n%/ &&
+ $Response->content !~ /ERROR: Could not form TPTP format derivation/ )
+{
+ # converted output: extract proof
+ my @lines = split( /\n/, $Response->content);
+ my $extract = "";
+ foreach my $line (@lines){
+ #ignore comments
+ if ($line !~ /^%/ && !($line eq "")) {
+ $extract .= "$line";
+ }
+ }
+ # insert newlines after ').'
+ $extract =~ s/\s//g;
+ $extract =~ s/\)\.cnf/\)\.\ncnf/g;
+
+ print "========== ~~/lib/scripts/SystemOnTPTP extracted proof: ==========\n";
+ # orientation for "sledgehammer_proof_reconstruct.ML"
+ print "# SZS output start CNFRefutation.\n";
+ print "$extract\n";
+ print "# SZS output end CNFRefutation.\n";
+ # can be useful for debugging; Isabelle ignores this
+ print "============== original response from SystemOnTPTP: ==============\n";
+ print $Response->content;
+ exit(0);
+} elsif (!exists($Options{'x'})) {
+ # pass output directly to Isabelle
+ print $Response->content;
+ exit(0);
+}else {
+ print "Remote script could not extract proof:\n".$Response->content;
+ exit(-1);
+}
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/ATP_Manager/scripts/spass Wed Jul 28 18:32:54 2010 +0200
@@ -0,0 +1,19 @@
+#!/usr/bin/env bash
+#
+# Wrapper for SPASS that also outputs the Flotter-generated CNF (needed for
+# Isar proof reconstruction)
+#
+# Author: Jasmin Blanchette, TU Muenchen
+
+options=${@:1:$(($#-1))}
+name=${@:$(($#)):1}
+
+$SPASS_HOME/tptp2dfg $name $name.fof.dfg
+$SPASS_HOME/SPASS -Flotter $name.fof.dfg \
+ | sed 's/description({$/description({*/' \
+ > $name.cnf.dfg
+rm -f $name.fof.dfg
+cat $name.cnf.dfg
+$SPASS_HOME/SPASS $options $name.cnf.dfg \
+ | sed 's/\(Formulae used in the proof :\).*/\1 N\/A/'
+rm -f $name.cnf.dfg