contrib/SystemOnTPTP/remote
author wenzelm
Sun, 11 Jan 2009 21:49:59 +0100
changeset 29450 ac7f67be7f1f
parent 28573 6403f0e16269
child 29587 96599d8d8268
permissions -rwxr-xr-x
tuned categories;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
28573
6403f0e16269 ** Update from Fabian **
wenzelm
parents:
diff changeset
     1
#!/usr/bin/env perl
6403f0e16269 ** Update from Fabian **
wenzelm
parents:
diff changeset
     2
#
6403f0e16269 ** Update from Fabian **
wenzelm
parents:
diff changeset
     3
# Wrapper for custom remote provers on SystemOnTPTP
6403f0e16269 ** Update from Fabian **
wenzelm
parents:
diff changeset
     4
# Author: Fabian Immler, TU Muenchen
6403f0e16269 ** Update from Fabian **
wenzelm
parents:
diff changeset
     5
#
6403f0e16269 ** Update from Fabian **
wenzelm
parents:
diff changeset
     6
# Similar to the vampire wrapper, but compatible provers can be passed in the
6403f0e16269 ** Update from Fabian **
wenzelm
parents:
diff changeset
     7
# command line, with %s for the problemfile e.g. 
6403f0e16269 ** Update from Fabian **
wenzelm
parents:
diff changeset
     8
#
6403f0e16269 ** Update from Fabian **
wenzelm
parents:
diff changeset
     9
# ./remote Vampire---9.0 jumpirefix --output_syntax tptp --mode casc -t 3600 %s
6403f0e16269 ** Update from Fabian **
wenzelm
parents:
diff changeset
    10
# ./remote Vampire---10.0 drakosha.pl 60 %s
6403f0e16269 ** Update from Fabian **
wenzelm
parents:
diff changeset
    11
# ./remote SPASS---3.01 SPASS -Auto -SOS=1 -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof %s
6403f0e16269 ** Update from Fabian **
wenzelm
parents:
diff changeset
    12
# ./remote Metis---2.1 metis --show proof --show saturation %s
6403f0e16269 ** Update from Fabian **
wenzelm
parents:
diff changeset
    13
# ./remote SNARK---20080805r005 run-snark %s
6403f0e16269 ** Update from Fabian **
wenzelm
parents:
diff changeset
    14
6403f0e16269 ** Update from Fabian **
wenzelm
parents:
diff changeset
    15
use warnings;
6403f0e16269 ** Update from Fabian **
wenzelm
parents:
diff changeset
    16
use strict;
6403f0e16269 ** Update from Fabian **
wenzelm
parents:
diff changeset
    17
6403f0e16269 ** Update from Fabian **
wenzelm
parents:
diff changeset
    18
use Getopt::Std;
6403f0e16269 ** Update from Fabian **
wenzelm
parents:
diff changeset
    19
use HTTP::Request::Common;
6403f0e16269 ** Update from Fabian **
wenzelm
parents:
diff changeset
    20
use LWP::UserAgent;
6403f0e16269 ** Update from Fabian **
wenzelm
parents:
diff changeset
    21
6403f0e16269 ** Update from Fabian **
wenzelm
parents:
diff changeset
    22
# address of proof-server
6403f0e16269 ** Update from Fabian **
wenzelm
parents:
diff changeset
    23
my $SystemOnTPTPFormReplyURL = "http://www.cs.miami.edu/~tptp/cgi-bin/SystemOnTPTPFormReply";
6403f0e16269 ** Update from Fabian **
wenzelm
parents:
diff changeset
    24
6403f0e16269 ** Update from Fabian **
wenzelm
parents:
diff changeset
    25
if(scalar(@ARGV) < 2) {
6403f0e16269 ** Update from Fabian **
wenzelm
parents:
diff changeset
    26
    print "prover and command missing";
6403f0e16269 ** Update from Fabian **
wenzelm
parents:
diff changeset
    27
    exit -1;
6403f0e16269 ** Update from Fabian **
wenzelm
parents:
diff changeset
    28
}
6403f0e16269 ** Update from Fabian **
wenzelm
parents:
diff changeset
    29
my $prover = shift(@ARGV);
6403f0e16269 ** Update from Fabian **
wenzelm
parents:
diff changeset
    30
my $command = shift(@ARGV);
6403f0e16269 ** Update from Fabian **
wenzelm
parents:
diff changeset
    31
6403f0e16269 ** Update from Fabian **
wenzelm
parents:
diff changeset
    32
# pass arguments
6403f0e16269 ** Update from Fabian **
wenzelm
parents:
diff changeset
    33
my $options = "";
6403f0e16269 ** Update from Fabian **
wenzelm
parents:
diff changeset
    34
while(scalar(@ARGV)>1){
6403f0e16269 ** Update from Fabian **
wenzelm
parents:
diff changeset
    35
	$options.=" ".shift(@ARGV);
6403f0e16269 ** Update from Fabian **
wenzelm
parents:
diff changeset
    36
}
6403f0e16269 ** Update from Fabian **
wenzelm
parents:
diff changeset
    37
# last argument is problemfile to be uploaded
6403f0e16269 ** Update from Fabian **
wenzelm
parents:
diff changeset
    38
my $problem = [shift(@ARGV)];
6403f0e16269 ** Update from Fabian **
wenzelm
parents:
diff changeset
    39
6403f0e16269 ** Update from Fabian **
wenzelm
parents:
diff changeset
    40
# fill in form
6403f0e16269 ** Update from Fabian **
wenzelm
parents:
diff changeset
    41
my %URLParameters = (
6403f0e16269 ** Update from Fabian **
wenzelm
parents:
diff changeset
    42
    "NoHTML" => 1,
6403f0e16269 ** Update from Fabian **
wenzelm
parents:
diff changeset
    43
    "QuietFlag" => "-q01",
6403f0e16269 ** Update from Fabian **
wenzelm
parents:
diff changeset
    44
    "X2TPTP" => "-S",
6403f0e16269 ** Update from Fabian **
wenzelm
parents:
diff changeset
    45
    "SubmitButton" => "RunSelectedSystems",
6403f0e16269 ** Update from Fabian **
wenzelm
parents:
diff changeset
    46
    "ProblemSource" => "UPLOAD",
6403f0e16269 ** Update from Fabian **
wenzelm
parents:
diff changeset
    47
    "UPLOADProblem" => $problem,
6403f0e16269 ** Update from Fabian **
wenzelm
parents:
diff changeset
    48
    "System___$prover" => "$prover",
6403f0e16269 ** Update from Fabian **
wenzelm
parents:
diff changeset
    49
    "Format___$prover" => "tptp",
6403f0e16269 ** Update from Fabian **
wenzelm
parents:
diff changeset
    50
    "Command___$prover" => "$command $options %s"
6403f0e16269 ** Update from Fabian **
wenzelm
parents:
diff changeset
    51
);
6403f0e16269 ** Update from Fabian **
wenzelm
parents:
diff changeset
    52
6403f0e16269 ** Update from Fabian **
wenzelm
parents:
diff changeset
    53
# Query Server
6403f0e16269 ** Update from Fabian **
wenzelm
parents:
diff changeset
    54
my $Agent = LWP::UserAgent->new;
6403f0e16269 ** Update from Fabian **
wenzelm
parents:
diff changeset
    55
my $Request = POST($SystemOnTPTPFormReplyURL,
6403f0e16269 ** Update from Fabian **
wenzelm
parents:
diff changeset
    56
	Content_Type => 'form-data',Content => \%URLParameters);
6403f0e16269 ** Update from Fabian **
wenzelm
parents:
diff changeset
    57
my $Response = $Agent->request($Request);
6403f0e16269 ** Update from Fabian **
wenzelm
parents:
diff changeset
    58
  
6403f0e16269 ** Update from Fabian **
wenzelm
parents:
diff changeset
    59
#catch errors, let isabelle/watcher know
6403f0e16269 ** Update from Fabian **
wenzelm
parents:
diff changeset
    60
if($Response->is_success && $Response->content !~ /NO SOLUTION OUTPUT BY SYSTEM/
6403f0e16269 ** Update from Fabian **
wenzelm
parents:
diff changeset
    61
&& $Response->content =~ m/%\s*Result\s*:\s*Unsatisfiable.*?\n%\s*Output\s*:\s*.*?Refutation.*?\n/){
6403f0e16269 ** Update from Fabian **
wenzelm
parents:
diff changeset
    62
    # convert to isabelle-friendly format
6403f0e16269 ** Update from Fabian **
wenzelm
parents:
diff changeset
    63
    my @lines = split( /%\s*Result\s*:\s*Unsatisfiable.*?\n%\s*Output\s*:\s*.*?Refutation.*?\n/, $Response->content);
6403f0e16269 ** Update from Fabian **
wenzelm
parents:
diff changeset
    64
    @lines = split( /\n/, $lines[1]);    my $extract = "";
6403f0e16269 ** Update from Fabian **
wenzelm
parents:
diff changeset
    65
    my $inproof = 0 > 1;
6403f0e16269 ** Update from Fabian **
wenzelm
parents:
diff changeset
    66
    my $ende = 0 > 1;
6403f0e16269 ** Update from Fabian **
wenzelm
parents:
diff changeset
    67
    foreach my $line (@lines){
6403f0e16269 ** Update from Fabian **
wenzelm
parents:
diff changeset
    68
        if(! $ende){
6403f0e16269 ** Update from Fabian **
wenzelm
parents:
diff changeset
    69
            #ignore comments
6403f0e16269 ** Update from Fabian **
wenzelm
parents:
diff changeset
    70
            if(! $inproof){
6403f0e16269 ** Update from Fabian **
wenzelm
parents:
diff changeset
    71
                if ($line !~ /^%/ && !($line eq "")) {
6403f0e16269 ** Update from Fabian **
wenzelm
parents:
diff changeset
    72
                    $extract .= "$line";
6403f0e16269 ** Update from Fabian **
wenzelm
parents:
diff changeset
    73
                    $inproof = 1;
6403f0e16269 ** Update from Fabian **
wenzelm
parents:
diff changeset
    74
                }
6403f0e16269 ** Update from Fabian **
wenzelm
parents:
diff changeset
    75
            } else {
6403f0e16269 ** Update from Fabian **
wenzelm
parents:
diff changeset
    76
                if ($line !~ /^%/) {
6403f0e16269 ** Update from Fabian **
wenzelm
parents:
diff changeset
    77
                    $extract .= "$line";
6403f0e16269 ** Update from Fabian **
wenzelm
parents:
diff changeset
    78
                } else {
6403f0e16269 ** Update from Fabian **
wenzelm
parents:
diff changeset
    79
                    $ende = 1;
6403f0e16269 ** Update from Fabian **
wenzelm
parents:
diff changeset
    80
                }
6403f0e16269 ** Update from Fabian **
wenzelm
parents:
diff changeset
    81
            }
6403f0e16269 ** Update from Fabian **
wenzelm
parents:
diff changeset
    82
        }
6403f0e16269 ** Update from Fabian **
wenzelm
parents:
diff changeset
    83
    }
6403f0e16269 ** Update from Fabian **
wenzelm
parents:
diff changeset
    84
    # insert newlines after '.'
6403f0e16269 ** Update from Fabian **
wenzelm
parents:
diff changeset
    85
    $extract =~ s/\s//g;
6403f0e16269 ** Update from Fabian **
wenzelm
parents:
diff changeset
    86
    $extract =~ s/\)\.cnf/\)\.\ncnf/g;
6403f0e16269 ** Update from Fabian **
wenzelm
parents:
diff changeset
    87
    print "# SZS output start CNFRefutation.\n";
6403f0e16269 ** Update from Fabian **
wenzelm
parents:
diff changeset
    88
    print "$extract\n";
6403f0e16269 ** Update from Fabian **
wenzelm
parents:
diff changeset
    89
    print "# SZS output end CNFRefutation.\n";
6403f0e16269 ** Update from Fabian **
wenzelm
parents:
diff changeset
    90
} else {
6403f0e16269 ** Update from Fabian **
wenzelm
parents:
diff changeset
    91
	print "HTTP-Request: " . $Response->message;
6403f0e16269 ** Update from Fabian **
wenzelm
parents:
diff changeset
    92
	print "\nCANNOT PROVE: \n";
6403f0e16269 ** Update from Fabian **
wenzelm
parents:
diff changeset
    93
  print $Response->content;
6403f0e16269 ** Update from Fabian **
wenzelm
parents:
diff changeset
    94
}
6403f0e16269 ** Update from Fabian **
wenzelm
parents:
diff changeset
    95