Admin/E/eproof

undo changes from revision 719426c9e1eb: removed Perl script for ATP invocation, measuring time using Bash-builtin "time";
new "eproof" script written in Perl (hopefully more stable than the one coming with E)

#!/usr/bin/perl -w
#
# eproof - run E and translate its output into TSTP format
#
# Author: Sascha Boehme, TU Muenchen
#
# This script is a port of a Bash script with the same name coming with
# E 1.0-004 (written by Stephan Schulz).
#


use File::Basename qw/ dirname /;
use File::Temp qw/ tempfile /;


# E executables

my $edir = dirname($0);
my $eprover = "$edir/eprover";
my $epclextract = "$edir/epclextract";


# build E command from given commandline arguments

my $format = "";
my $eprover_cmd = $eprover;
foreach (@ARGV) {
  if (m/--tstp-out/) {
    $format = $_;
  }
  else {
    $eprover_cmd = "$eprover_cmd '$_'";
  }
}
$eprover_cmd = "$eprover_cmd -l4 -R -o- --pcl-terms-compressed --pcl-compact";


# run E, redirecting output into a temporary file

my ($fh, $filename) = tempfile(UNLINK => 1);
my $r = system "$eprover_cmd > $filename";
exit ($r >> 8) if $r != 0;


# analyze E output

my @lines = <$fh>;
my $content = join "", @lines[-60 .. -1];
  # Note: Like the original eproof, we only look at the last 60 lines.

if ($content =~ m/Total time/) {
  if ($content =~ m/No proof found!/) {
    print "# Problem is satisfiable (or invalid), " .
      "generating saturation derivation\n";
  }
  elsif ($content =~ m/Proof found!/) {
    print "# Problem is unsatisfiable (or provable), " .
      "constructing proof object\n";
  }
  elsif ($content =~ m/Watchlist is empty!/) {
    print "# All watchlist clauses generated, constructing derivation\n";
  }
  else {
    print "# Cannot determine problem status\n";
    exit $r;
  }
}
else {
  print "# Cannot determine problem status within resource limit\n";
  exit $r;
}


# extract E output

foreach (@lines) {
  print if (m/# SZS status/ or m/"# Failure"/);
}
$r = system "$epclextract $format -f --competition-framing $filename";
  # Note: Before extraction, the original eproof invokes 'ulimit -S -t TIME'
  # where TIME is the remaining time from the time limit given at the command
  # line. This does not seem very reliable and is not implemented here. This
  # is not a problem as long as extraction is reasonable fast or the invoking
  # process enforces a time limit of its own.
exit ($r >> 8);