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