#!/usr/bin/env perl
#
# Wrapper for custom remote provers on SystemOnTPTP
# Author: Fabian Immler, TU Muenchen
#
# Usage: ./remote prover timelimit problemfile
#
# where prover should be the name of the System from http://www.cs.miami.edu/~tptp/cgi-bin/SystemOnTPTP
# tested and working with the standard settings:
#
# ./remote Vampire---9.0 timelimit file
# ./remote SPASS---3.01 timelimit file
# ./remote Metis---2.1 timelimit file
# ./remote SNARK---20080805r005 timelimit file
# ./remote Otter---3.3 timelimit file
# ./remote SOS---2.0 timelimit file
# ./remote EP---1.0 timelimit file
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) != 3) {
print "usage: ";
exit -1;
}
my $prover = shift(@ARGV);
my $timelimit = shift(@ARGV);
my $problem = [shift(@ARGV)];
# fill in form
my %URLParameters = (
"NoHTML" => 1,
"QuietFlag" => "-q01",
"X2TPTP" => "-S",
"SubmitButton" => "RunSelectedSystems",
"ProblemSource" => "UPLOAD",
"UPLOADProblem" => $problem,
"System___$prover" => "$prover",
"TimeLimit___$prover" => "$timelimit",
);
# 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 "\nResponse: " . $Response->content;
print "\nCANNOT PROVE: \n";
print $Response->content;
}