# HG changeset patch
# User boehmes
# Date 1253189264 -7200
# Node ID 2953c3917e21f68de342af72d12bf3fae285d3e2
# Parent  3caf79c88aef01d59e656ae0d1746f69d004caf1
added time limit for extraction phase (not supported on Cygwin)

diff -r 3caf79c88aef -r 2953c3917e21 Admin/E/eproof
--- a/Admin/E/eproof	Thu Sep 17 11:58:21 2009 +0200
+++ b/Admin/E/eproof	Thu Sep 17 14:07:44 2009 +0200
@@ -23,8 +23,14 @@
 # build E command from given commandline arguments
 
 my $format = "";
-my $eprover_cmd = $eprover;
+my $timelimit = 2000000000;   # effectively unlimited
+
+my $eprover_cmd = "'$eprover'";
 foreach (@ARGV) {
+  if (m/--cpu-limit=([0-9]+)/) {
+    $timelimit = $1;
+  }
+
   if (m/--tstp-out/) {
     $format = $_;
   }
@@ -48,7 +54,9 @@
 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/Total time\s*:\s*([0-9]+\.[0-9]+)/) {
+  $timelimit = $timelimit - $1 - 1;
+
   if ($content =~ m/No proof found!/) {
     print "# Problem is satisfiable (or invalid), " .
       "generating saturation derivation\n";
@@ -71,16 +79,14 @@
 }
 
 
-# extract E output
+# translate 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.
+$r = system ("exec bash -c \"ulimit -S -t $timelimit; " .
+  "'$epclextract' $format -f --competition-framing $filename\"");
+  # Note: Setting the user time is not supported on Cygwin, i.e., ulimit fails
+  # and prints and error message. How could we then limit the execution time?
 exit ($r >> 8);