contrib/SystemOnTPTP/vampire
author wenzelm
Sun, 30 Nov 2008 14:43:29 +0100
changeset 28917 20f43e0e0958
parent 28474 d0b8b0a1fca5
permissions -rwxr-xr-x
tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
28474
d0b8b0a1fca5 Vampire wrapper script for remote SystemOnTPTP service (by Fabian Immler);
wenzelm
parents:
diff changeset
     1
#!/usr/bin/env perl
d0b8b0a1fca5 Vampire wrapper script for remote SystemOnTPTP service (by Fabian Immler);
wenzelm
parents:
diff changeset
     2
#
d0b8b0a1fca5 Vampire wrapper script for remote SystemOnTPTP service (by Fabian Immler);
wenzelm
parents:
diff changeset
     3
# Vampire Wrapper for SystemOnTPTP
d0b8b0a1fca5 Vampire wrapper script for remote SystemOnTPTP service (by Fabian Immler);
wenzelm
parents:
diff changeset
     4
# Author: Fabian Immler, TU Muenchen
d0b8b0a1fca5 Vampire wrapper script for remote SystemOnTPTP service (by Fabian Immler);
wenzelm
parents:
diff changeset
     5
#
d0b8b0a1fca5 Vampire wrapper script for remote SystemOnTPTP service (by Fabian Immler);
wenzelm
parents:
diff changeset
     6
# - querys a Vampire theorem prover on SystemOnTPTP
d0b8b0a1fca5 Vampire wrapper script for remote SystemOnTPTP service (by Fabian Immler);
wenzelm
parents:
diff changeset
     7
#   (http://www.cs.miami.edu/~tptp/cgi-bin/SystemOnTPTP)
d0b8b0a1fca5 Vampire wrapper script for remote SystemOnTPTP service (by Fabian Immler);
wenzelm
parents:
diff changeset
     8
# - behaves like a local Vampire
d0b8b0a1fca5 Vampire wrapper script for remote SystemOnTPTP service (by Fabian Immler);
wenzelm
parents:
diff changeset
     9
# => can be used for Isabelle when Vampire is not available (e.g. on a Mac)
d0b8b0a1fca5 Vampire wrapper script for remote SystemOnTPTP service (by Fabian Immler);
wenzelm
parents:
diff changeset
    10
#
d0b8b0a1fca5 Vampire wrapper script for remote SystemOnTPTP service (by Fabian Immler);
wenzelm
parents:
diff changeset
    11
d0b8b0a1fca5 Vampire wrapper script for remote SystemOnTPTP service (by Fabian Immler);
wenzelm
parents:
diff changeset
    12
use warnings;
d0b8b0a1fca5 Vampire wrapper script for remote SystemOnTPTP service (by Fabian Immler);
wenzelm
parents:
diff changeset
    13
use strict;
d0b8b0a1fca5 Vampire wrapper script for remote SystemOnTPTP service (by Fabian Immler);
wenzelm
parents:
diff changeset
    14
d0b8b0a1fca5 Vampire wrapper script for remote SystemOnTPTP service (by Fabian Immler);
wenzelm
parents:
diff changeset
    15
use Getopt::Std;
d0b8b0a1fca5 Vampire wrapper script for remote SystemOnTPTP service (by Fabian Immler);
wenzelm
parents:
diff changeset
    16
use HTTP::Request::Common;
d0b8b0a1fca5 Vampire wrapper script for remote SystemOnTPTP service (by Fabian Immler);
wenzelm
parents:
diff changeset
    17
use LWP::UserAgent;
d0b8b0a1fca5 Vampire wrapper script for remote SystemOnTPTP service (by Fabian Immler);
wenzelm
parents:
diff changeset
    18
d0b8b0a1fca5 Vampire wrapper script for remote SystemOnTPTP service (by Fabian Immler);
wenzelm
parents:
diff changeset
    19
# address of proof-server
d0b8b0a1fca5 Vampire wrapper script for remote SystemOnTPTP service (by Fabian Immler);
wenzelm
parents:
diff changeset
    20
my $SystemOnTPTPFormReplyURL = "http://www.cs.miami.edu/~tptp/cgi-bin/SystemOnTPTPFormReply";
d0b8b0a1fca5 Vampire wrapper script for remote SystemOnTPTP service (by Fabian Immler);
wenzelm
parents:
diff changeset
    21
d0b8b0a1fca5 Vampire wrapper script for remote SystemOnTPTP service (by Fabian Immler);
wenzelm
parents:
diff changeset
    22
#name of prover and its executable on the server, e.g.
d0b8b0a1fca5 Vampire wrapper script for remote SystemOnTPTP service (by Fabian Immler);
wenzelm
parents:
diff changeset
    23
# Vampire---9.0
d0b8b0a1fca5 Vampire wrapper script for remote SystemOnTPTP service (by Fabian Immler);
wenzelm
parents:
diff changeset
    24
# jumpirefix
d0b8b0a1fca5 Vampire wrapper script for remote SystemOnTPTP service (by Fabian Immler);
wenzelm
parents:
diff changeset
    25
my $prover = "Vampire---9.0";
d0b8b0a1fca5 Vampire wrapper script for remote SystemOnTPTP service (by Fabian Immler);
wenzelm
parents:
diff changeset
    26
my $command = "jumpirefix";
d0b8b0a1fca5 Vampire wrapper script for remote SystemOnTPTP service (by Fabian Immler);
wenzelm
parents:
diff changeset
    27
d0b8b0a1fca5 Vampire wrapper script for remote SystemOnTPTP service (by Fabian Immler);
wenzelm
parents:
diff changeset
    28
# pass arguments
d0b8b0a1fca5 Vampire wrapper script for remote SystemOnTPTP service (by Fabian Immler);
wenzelm
parents:
diff changeset
    29
my $options = "";
d0b8b0a1fca5 Vampire wrapper script for remote SystemOnTPTP service (by Fabian Immler);
wenzelm
parents:
diff changeset
    30
while(scalar(@ARGV)>1){
d0b8b0a1fca5 Vampire wrapper script for remote SystemOnTPTP service (by Fabian Immler);
wenzelm
parents:
diff changeset
    31
	$options.=" ".shift(@ARGV);
d0b8b0a1fca5 Vampire wrapper script for remote SystemOnTPTP service (by Fabian Immler);
wenzelm
parents:
diff changeset
    32
}
d0b8b0a1fca5 Vampire wrapper script for remote SystemOnTPTP service (by Fabian Immler);
wenzelm
parents:
diff changeset
    33
# last argument is problemfile to be uploaded
d0b8b0a1fca5 Vampire wrapper script for remote SystemOnTPTP service (by Fabian Immler);
wenzelm
parents:
diff changeset
    34
my $problem = [shift(@ARGV)];
d0b8b0a1fca5 Vampire wrapper script for remote SystemOnTPTP service (by Fabian Immler);
wenzelm
parents:
diff changeset
    35
d0b8b0a1fca5 Vampire wrapper script for remote SystemOnTPTP service (by Fabian Immler);
wenzelm
parents:
diff changeset
    36
# fill in form
d0b8b0a1fca5 Vampire wrapper script for remote SystemOnTPTP service (by Fabian Immler);
wenzelm
parents:
diff changeset
    37
my %URLParameters = (
d0b8b0a1fca5 Vampire wrapper script for remote SystemOnTPTP service (by Fabian Immler);
wenzelm
parents:
diff changeset
    38
    "NoHTML" => 1,
d0b8b0a1fca5 Vampire wrapper script for remote SystemOnTPTP service (by Fabian Immler);
wenzelm
parents:
diff changeset
    39
    "QuietFlag" => "-q01",
d0b8b0a1fca5 Vampire wrapper script for remote SystemOnTPTP service (by Fabian Immler);
wenzelm
parents:
diff changeset
    40
    "SubmitButton" => "RunSelectedSystems",
d0b8b0a1fca5 Vampire wrapper script for remote SystemOnTPTP service (by Fabian Immler);
wenzelm
parents:
diff changeset
    41
    "ProblemSource" => "UPLOAD",
d0b8b0a1fca5 Vampire wrapper script for remote SystemOnTPTP service (by Fabian Immler);
wenzelm
parents:
diff changeset
    42
    "UPLOADProblem" => $problem,
d0b8b0a1fca5 Vampire wrapper script for remote SystemOnTPTP service (by Fabian Immler);
wenzelm
parents:
diff changeset
    43
    "System___$prover" => "$prover",
d0b8b0a1fca5 Vampire wrapper script for remote SystemOnTPTP service (by Fabian Immler);
wenzelm
parents:
diff changeset
    44
    "Format___$prover" => "tptp",
d0b8b0a1fca5 Vampire wrapper script for remote SystemOnTPTP service (by Fabian Immler);
wenzelm
parents:
diff changeset
    45
    "Command___$prover" => "$command $options %s"
d0b8b0a1fca5 Vampire wrapper script for remote SystemOnTPTP service (by Fabian Immler);
wenzelm
parents:
diff changeset
    46
);
d0b8b0a1fca5 Vampire wrapper script for remote SystemOnTPTP service (by Fabian Immler);
wenzelm
parents:
diff changeset
    47
d0b8b0a1fca5 Vampire wrapper script for remote SystemOnTPTP service (by Fabian Immler);
wenzelm
parents:
diff changeset
    48
# Query Server
d0b8b0a1fca5 Vampire wrapper script for remote SystemOnTPTP service (by Fabian Immler);
wenzelm
parents:
diff changeset
    49
my $Agent = LWP::UserAgent->new;
d0b8b0a1fca5 Vampire wrapper script for remote SystemOnTPTP service (by Fabian Immler);
wenzelm
parents:
diff changeset
    50
my $Request = POST($SystemOnTPTPFormReplyURL,
d0b8b0a1fca5 Vampire wrapper script for remote SystemOnTPTP service (by Fabian Immler);
wenzelm
parents:
diff changeset
    51
	Content_Type => 'form-data',Content => \%URLParameters);
d0b8b0a1fca5 Vampire wrapper script for remote SystemOnTPTP service (by Fabian Immler);
wenzelm
parents:
diff changeset
    52
my $Response = $Agent->request($Request);
d0b8b0a1fca5 Vampire wrapper script for remote SystemOnTPTP service (by Fabian Immler);
wenzelm
parents:
diff changeset
    53
    
d0b8b0a1fca5 Vampire wrapper script for remote SystemOnTPTP service (by Fabian Immler);
wenzelm
parents:
diff changeset
    54
#catch errors, let isabelle/watcher know
d0b8b0a1fca5 Vampire wrapper script for remote SystemOnTPTP service (by Fabian Immler);
wenzelm
parents:
diff changeset
    55
if($Response->is_success){
d0b8b0a1fca5 Vampire wrapper script for remote SystemOnTPTP service (by Fabian Immler);
wenzelm
parents:
diff changeset
    56
	print $Response->content;
d0b8b0a1fca5 Vampire wrapper script for remote SystemOnTPTP service (by Fabian Immler);
wenzelm
parents:
diff changeset
    57
} else {
d0b8b0a1fca5 Vampire wrapper script for remote SystemOnTPTP service (by Fabian Immler);
wenzelm
parents:
diff changeset
    58
	print $Response->message;
d0b8b0a1fca5 Vampire wrapper script for remote SystemOnTPTP service (by Fabian Immler);
wenzelm
parents:
diff changeset
    59
	print "\nCANNOT PROVE\n";
d0b8b0a1fca5 Vampire wrapper script for remote SystemOnTPTP service (by Fabian Immler);
wenzelm
parents:
diff changeset
    60
}