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