Admin/E/eproof

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/E/eproof	Thu Sep 17 11:57:36 2009 +0200
@@ -0,0 +1,86 @@
+#!/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);
+