# HG changeset patch # User blanchet # Date 1280334774 -7200 # Node ID 3b80d6082131182ae3e95e203a3e9d1cb64a7163 # Parent 1745685335932821056e9cbbd3d74fae4fa76565 remove "remote_spass" because there's no way to find out which clauses come from which facts + rename scripts diff -r 174568533593 -r 3b80d6082131 src/HOL/Tools/ATP_Manager/SPASS_TPTP --- 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 diff -r 174568533593 -r 3b80d6082131 src/HOL/Tools/ATP_Manager/SystemOnTPTP --- 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 [] \n"); - print(" 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 - specified system to use\n"); - print(" -t - CPU time limit for system\n"); - print(" -c - custom command for system\n"); - print(" - 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); -} - diff -r 174568533593 -r 3b80d6082131 src/HOL/Tools/ATP_Manager/atp_systems.ML --- 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; diff -r 174568533593 -r 3b80d6082131 src/HOL/Tools/ATP_Manager/scripts/remote_atp --- /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 [] \n"); + print(" 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 - specified system to use\n"); + print(" -t - CPU time limit for system\n"); + print(" -c - custom command for system\n"); + print(" - 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); +} + diff -r 174568533593 -r 3b80d6082131 src/HOL/Tools/ATP_Manager/scripts/spass --- /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