# HG changeset patch
# User wenzelm
# Date 1223899493 -7200
# Node ID 6403f0e16269ffc0cd8c1fb780c2ce81ef4b0676
# Parent  78ac28f80a1cfc8a30271f1373f95ef83875e685
** Update from Fabian **
added remote prover functions;

diff -r 78ac28f80a1c -r 6403f0e16269 contrib/SystemOnTPTP/remote
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/contrib/SystemOnTPTP/remote	Mon Oct 13 14:04:53 2008 +0200
@@ -0,0 +1,95 @@
+#!/usr/bin/env perl
+#
+# Wrapper for custom remote provers on SystemOnTPTP
+# Author: Fabian Immler, TU Muenchen
+#
+# Similar to the vampire wrapper, but compatible provers can be passed in the
+# command line, with %s for the problemfile e.g. 
+#
+# ./remote Vampire---9.0 jumpirefix --output_syntax tptp --mode casc -t 3600 %s
+# ./remote Vampire---10.0 drakosha.pl 60 %s
+# ./remote SPASS---3.01 SPASS -Auto -SOS=1 -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof %s
+# ./remote Metis---2.1 metis --show proof --show saturation %s
+# ./remote SNARK---20080805r005 run-snark %s
+
+use warnings;
+use strict;
+
+use Getopt::Std;
+use HTTP::Request::Common;
+use LWP::UserAgent;
+
+# address of proof-server
+my $SystemOnTPTPFormReplyURL = "http://www.cs.miami.edu/~tptp/cgi-bin/SystemOnTPTPFormReply";
+
+if(scalar(@ARGV) < 2) {
+    print "prover and command missing";
+    exit -1;
+}
+my $prover = shift(@ARGV);
+my $command = shift(@ARGV);
+
+# pass arguments
+my $options = "";
+while(scalar(@ARGV)>1){
+	$options.=" ".shift(@ARGV);
+}
+# last argument is problemfile to be uploaded
+my $problem = [shift(@ARGV)];
+
+# fill in form
+my %URLParameters = (
+    "NoHTML" => 1,
+    "QuietFlag" => "-q01",
+    "X2TPTP" => "-S",
+    "SubmitButton" => "RunSelectedSystems",
+    "ProblemSource" => "UPLOAD",
+    "UPLOADProblem" => $problem,
+    "System___$prover" => "$prover",
+    "Format___$prover" => "tptp",
+    "Command___$prover" => "$command $options %s"
+);
+
+# Query Server
+my $Agent = LWP::UserAgent->new;
+my $Request = POST($SystemOnTPTPFormReplyURL,
+	Content_Type => 'form-data',Content => \%URLParameters);
+my $Response = $Agent->request($Request);
+  
+#catch errors, let isabelle/watcher know
+if($Response->is_success && $Response->content !~ /NO SOLUTION OUTPUT BY SYSTEM/
+&& $Response->content =~ m/%\s*Result\s*:\s*Unsatisfiable.*?\n%\s*Output\s*:\s*.*?Refutation.*?\n/){
+    # convert to isabelle-friendly format
+    my @lines = split( /%\s*Result\s*:\s*Unsatisfiable.*?\n%\s*Output\s*:\s*.*?Refutation.*?\n/, $Response->content);
+    @lines = split( /\n/, $lines[1]);    my $extract = "";
+    my $inproof = 0 > 1;
+    my $ende = 0 > 1;
+    foreach my $line (@lines){
+        if(! $ende){
+            #ignore comments
+            if(! $inproof){
+                if ($line !~ /^%/ && !($line eq "")) {
+                    $extract .= "$line";
+                    $inproof = 1;
+                }
+            } else {
+                if ($line !~ /^%/) {
+                    $extract .= "$line";
+                } else {
+                    $ende = 1;
+                }
+            }
+        }
+    }
+    # insert newlines after '.'
+    $extract =~ s/\s//g;
+    $extract =~ s/\)\.cnf/\)\.\ncnf/g;
+    print "# SZS output start CNFRefutation.\n";
+    print "$extract\n";
+    print "# SZS output end CNFRefutation.\n";
+} else {
+	print "HTTP-Request: " . $Response->message;
+	print "\nCANNOT PROVE: \n";
+  print $Response->content;
+}
+
diff -r 78ac28f80a1c -r 6403f0e16269 src/HOL/ATP_Linkup.thy
--- a/src/HOL/ATP_Linkup.thy	Mon Oct 13 14:04:29 2008 +0200
+++ b/src/HOL/ATP_Linkup.thy	Mon Oct 13 14:04:53 2008 +0200
@@ -95,6 +95,7 @@
 use "Tools/res_hol_clause.ML"
 use "Tools/res_reconstruct.ML" setup ResReconstruct.setup
 use "Tools/res_atp.ML"
+
 use "Tools/atp_manager.ML"
 use "Tools/atp_thread.ML"
 
@@ -110,6 +111,12 @@
 text {* on some problems better results *}
 setup {* AtpManager.add_prover "spass_no_tc" (AtpThread.spass_filter_opts 40 false) *}
 
+text {* remote provers via SystemOnTPTP *}
+setup {* AtpManager.add_prover "remote_vamp9"
+  (AtpThread.remote_prover "Vampire---9.0" "jumpirefix --output_syntax tptp --mode casc -t 3600") *}
+setup {* AtpManager.add_prover "remote_vamp10"
+  (AtpThread.remote_prover "Vampire---10.0" "drakosha.pl 60") *}
+
 
 subsection {* The Metis prover *}