Admin/E/eproof
author wenzelm
Wed, 07 Sep 2011 11:00:39 +0200
changeset 44775 27930cf6f0f7
parent 32675 5fe601aff9be
permissions -rwxr-xr-x
added "cancel" button based on cancel_execution, not interrupt (cf. 156be0e43336);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
32593
3711565687a6 undo changes from revision 719426c9e1eb: removed Perl script for ATP invocation, measuring time using Bash-builtin "time";
boehmes
parents:
diff changeset
     1
#!/usr/bin/perl -w
3711565687a6 undo changes from revision 719426c9e1eb: removed Perl script for ATP invocation, measuring time using Bash-builtin "time";
boehmes
parents:
diff changeset
     2
#
3711565687a6 undo changes from revision 719426c9e1eb: removed Perl script for ATP invocation, measuring time using Bash-builtin "time";
boehmes
parents:
diff changeset
     3
# eproof - run E and translate its output into TSTP format
3711565687a6 undo changes from revision 719426c9e1eb: removed Perl script for ATP invocation, measuring time using Bash-builtin "time";
boehmes
parents:
diff changeset
     4
#
3711565687a6 undo changes from revision 719426c9e1eb: removed Perl script for ATP invocation, measuring time using Bash-builtin "time";
boehmes
parents:
diff changeset
     5
# Author: Sascha Boehme, TU Muenchen
3711565687a6 undo changes from revision 719426c9e1eb: removed Perl script for ATP invocation, measuring time using Bash-builtin "time";
boehmes
parents:
diff changeset
     6
#
3711565687a6 undo changes from revision 719426c9e1eb: removed Perl script for ATP invocation, measuring time using Bash-builtin "time";
boehmes
parents:
diff changeset
     7
# This script is a port of a Bash script with the same name coming with
3711565687a6 undo changes from revision 719426c9e1eb: removed Perl script for ATP invocation, measuring time using Bash-builtin "time";
boehmes
parents:
diff changeset
     8
# E 1.0-004 (written by Stephan Schulz).
3711565687a6 undo changes from revision 719426c9e1eb: removed Perl script for ATP invocation, measuring time using Bash-builtin "time";
boehmes
parents:
diff changeset
     9
#
3711565687a6 undo changes from revision 719426c9e1eb: removed Perl script for ATP invocation, measuring time using Bash-builtin "time";
boehmes
parents:
diff changeset
    10
3711565687a6 undo changes from revision 719426c9e1eb: removed Perl script for ATP invocation, measuring time using Bash-builtin "time";
boehmes
parents:
diff changeset
    11
3711565687a6 undo changes from revision 719426c9e1eb: removed Perl script for ATP invocation, measuring time using Bash-builtin "time";
boehmes
parents:
diff changeset
    12
use File::Basename qw/ dirname /;
3711565687a6 undo changes from revision 719426c9e1eb: removed Perl script for ATP invocation, measuring time using Bash-builtin "time";
boehmes
parents:
diff changeset
    13
use File::Temp qw/ tempfile /;
32675
5fe601aff9be added quotes for filenames;
boehmes
parents: 32595
diff changeset
    14
use English;
32593
3711565687a6 undo changes from revision 719426c9e1eb: removed Perl script for ATP invocation, measuring time using Bash-builtin "time";
boehmes
parents:
diff changeset
    15
3711565687a6 undo changes from revision 719426c9e1eb: removed Perl script for ATP invocation, measuring time using Bash-builtin "time";
boehmes
parents:
diff changeset
    16
3711565687a6 undo changes from revision 719426c9e1eb: removed Perl script for ATP invocation, measuring time using Bash-builtin "time";
boehmes
parents:
diff changeset
    17
# E executables
3711565687a6 undo changes from revision 719426c9e1eb: removed Perl script for ATP invocation, measuring time using Bash-builtin "time";
boehmes
parents:
diff changeset
    18
3711565687a6 undo changes from revision 719426c9e1eb: removed Perl script for ATP invocation, measuring time using Bash-builtin "time";
boehmes
parents:
diff changeset
    19
my $edir = dirname($0);
3711565687a6 undo changes from revision 719426c9e1eb: removed Perl script for ATP invocation, measuring time using Bash-builtin "time";
boehmes
parents:
diff changeset
    20
my $eprover = "$edir/eprover";
3711565687a6 undo changes from revision 719426c9e1eb: removed Perl script for ATP invocation, measuring time using Bash-builtin "time";
boehmes
parents:
diff changeset
    21
my $epclextract = "$edir/epclextract";
3711565687a6 undo changes from revision 719426c9e1eb: removed Perl script for ATP invocation, measuring time using Bash-builtin "time";
boehmes
parents:
diff changeset
    22
3711565687a6 undo changes from revision 719426c9e1eb: removed Perl script for ATP invocation, measuring time using Bash-builtin "time";
boehmes
parents:
diff changeset
    23
3711565687a6 undo changes from revision 719426c9e1eb: removed Perl script for ATP invocation, measuring time using Bash-builtin "time";
boehmes
parents:
diff changeset
    24
# build E command from given commandline arguments
3711565687a6 undo changes from revision 719426c9e1eb: removed Perl script for ATP invocation, measuring time using Bash-builtin "time";
boehmes
parents:
diff changeset
    25
3711565687a6 undo changes from revision 719426c9e1eb: removed Perl script for ATP invocation, measuring time using Bash-builtin "time";
boehmes
parents:
diff changeset
    26
my $format = "";
32595
2953c3917e21 added time limit for extraction phase (not supported on Cygwin)
boehmes
parents: 32593
diff changeset
    27
my $timelimit = 2000000000;   # effectively unlimited
2953c3917e21 added time limit for extraction phase (not supported on Cygwin)
boehmes
parents: 32593
diff changeset
    28
2953c3917e21 added time limit for extraction phase (not supported on Cygwin)
boehmes
parents: 32593
diff changeset
    29
my $eprover_cmd = "'$eprover'";
32593
3711565687a6 undo changes from revision 719426c9e1eb: removed Perl script for ATP invocation, measuring time using Bash-builtin "time";
boehmes
parents:
diff changeset
    30
foreach (@ARGV) {
32595
2953c3917e21 added time limit for extraction phase (not supported on Cygwin)
boehmes
parents: 32593
diff changeset
    31
  if (m/--cpu-limit=([0-9]+)/) {
2953c3917e21 added time limit for extraction phase (not supported on Cygwin)
boehmes
parents: 32593
diff changeset
    32
    $timelimit = $1;
2953c3917e21 added time limit for extraction phase (not supported on Cygwin)
boehmes
parents: 32593
diff changeset
    33
  }
2953c3917e21 added time limit for extraction phase (not supported on Cygwin)
boehmes
parents: 32593
diff changeset
    34
32593
3711565687a6 undo changes from revision 719426c9e1eb: removed Perl script for ATP invocation, measuring time using Bash-builtin "time";
boehmes
parents:
diff changeset
    35
  if (m/--tstp-out/) {
3711565687a6 undo changes from revision 719426c9e1eb: removed Perl script for ATP invocation, measuring time using Bash-builtin "time";
boehmes
parents:
diff changeset
    36
    $format = $_;
3711565687a6 undo changes from revision 719426c9e1eb: removed Perl script for ATP invocation, measuring time using Bash-builtin "time";
boehmes
parents:
diff changeset
    37
  }
3711565687a6 undo changes from revision 719426c9e1eb: removed Perl script for ATP invocation, measuring time using Bash-builtin "time";
boehmes
parents:
diff changeset
    38
  else {
3711565687a6 undo changes from revision 719426c9e1eb: removed Perl script for ATP invocation, measuring time using Bash-builtin "time";
boehmes
parents:
diff changeset
    39
    $eprover_cmd = "$eprover_cmd '$_'";
3711565687a6 undo changes from revision 719426c9e1eb: removed Perl script for ATP invocation, measuring time using Bash-builtin "time";
boehmes
parents:
diff changeset
    40
  }
3711565687a6 undo changes from revision 719426c9e1eb: removed Perl script for ATP invocation, measuring time using Bash-builtin "time";
boehmes
parents:
diff changeset
    41
}
3711565687a6 undo changes from revision 719426c9e1eb: removed Perl script for ATP invocation, measuring time using Bash-builtin "time";
boehmes
parents:
diff changeset
    42
$eprover_cmd = "$eprover_cmd -l4 -R -o- --pcl-terms-compressed --pcl-compact";
3711565687a6 undo changes from revision 719426c9e1eb: removed Perl script for ATP invocation, measuring time using Bash-builtin "time";
boehmes
parents:
diff changeset
    43
3711565687a6 undo changes from revision 719426c9e1eb: removed Perl script for ATP invocation, measuring time using Bash-builtin "time";
boehmes
parents:
diff changeset
    44
3711565687a6 undo changes from revision 719426c9e1eb: removed Perl script for ATP invocation, measuring time using Bash-builtin "time";
boehmes
parents:
diff changeset
    45
# run E, redirecting output into a temporary file
3711565687a6 undo changes from revision 719426c9e1eb: removed Perl script for ATP invocation, measuring time using Bash-builtin "time";
boehmes
parents:
diff changeset
    46
3711565687a6 undo changes from revision 719426c9e1eb: removed Perl script for ATP invocation, measuring time using Bash-builtin "time";
boehmes
parents:
diff changeset
    47
my ($fh, $filename) = tempfile(UNLINK => 1);
32675
5fe601aff9be added quotes for filenames;
boehmes
parents: 32595
diff changeset
    48
my $r = system "$eprover_cmd > '$filename'";
32593
3711565687a6 undo changes from revision 719426c9e1eb: removed Perl script for ATP invocation, measuring time using Bash-builtin "time";
boehmes
parents:
diff changeset
    49
exit ($r >> 8) if $r != 0;
3711565687a6 undo changes from revision 719426c9e1eb: removed Perl script for ATP invocation, measuring time using Bash-builtin "time";
boehmes
parents:
diff changeset
    50
3711565687a6 undo changes from revision 719426c9e1eb: removed Perl script for ATP invocation, measuring time using Bash-builtin "time";
boehmes
parents:
diff changeset
    51
3711565687a6 undo changes from revision 719426c9e1eb: removed Perl script for ATP invocation, measuring time using Bash-builtin "time";
boehmes
parents:
diff changeset
    52
# analyze E output
3711565687a6 undo changes from revision 719426c9e1eb: removed Perl script for ATP invocation, measuring time using Bash-builtin "time";
boehmes
parents:
diff changeset
    53
3711565687a6 undo changes from revision 719426c9e1eb: removed Perl script for ATP invocation, measuring time using Bash-builtin "time";
boehmes
parents:
diff changeset
    54
my @lines = <$fh>;
3711565687a6 undo changes from revision 719426c9e1eb: removed Perl script for ATP invocation, measuring time using Bash-builtin "time";
boehmes
parents:
diff changeset
    55
my $content = join "", @lines[-60 .. -1];
3711565687a6 undo changes from revision 719426c9e1eb: removed Perl script for ATP invocation, measuring time using Bash-builtin "time";
boehmes
parents:
diff changeset
    56
  # Note: Like the original eproof, we only look at the last 60 lines.
3711565687a6 undo changes from revision 719426c9e1eb: removed Perl script for ATP invocation, measuring time using Bash-builtin "time";
boehmes
parents:
diff changeset
    57
32595
2953c3917e21 added time limit for extraction phase (not supported on Cygwin)
boehmes
parents: 32593
diff changeset
    58
if ($content =~ m/Total time\s*:\s*([0-9]+\.[0-9]+)/) {
32675
5fe601aff9be added quotes for filenames;
boehmes
parents: 32595
diff changeset
    59
  $timelimit = int($timelimit - $1 - 1);
32595
2953c3917e21 added time limit for extraction phase (not supported on Cygwin)
boehmes
parents: 32593
diff changeset
    60
32593
3711565687a6 undo changes from revision 719426c9e1eb: removed Perl script for ATP invocation, measuring time using Bash-builtin "time";
boehmes
parents:
diff changeset
    61
  if ($content =~ m/No proof found!/) {
3711565687a6 undo changes from revision 719426c9e1eb: removed Perl script for ATP invocation, measuring time using Bash-builtin "time";
boehmes
parents:
diff changeset
    62
    print "# Problem is satisfiable (or invalid), " .
3711565687a6 undo changes from revision 719426c9e1eb: removed Perl script for ATP invocation, measuring time using Bash-builtin "time";
boehmes
parents:
diff changeset
    63
      "generating saturation derivation\n";
3711565687a6 undo changes from revision 719426c9e1eb: removed Perl script for ATP invocation, measuring time using Bash-builtin "time";
boehmes
parents:
diff changeset
    64
  }
3711565687a6 undo changes from revision 719426c9e1eb: removed Perl script for ATP invocation, measuring time using Bash-builtin "time";
boehmes
parents:
diff changeset
    65
  elsif ($content =~ m/Proof found!/) {
3711565687a6 undo changes from revision 719426c9e1eb: removed Perl script for ATP invocation, measuring time using Bash-builtin "time";
boehmes
parents:
diff changeset
    66
    print "# Problem is unsatisfiable (or provable), " .
3711565687a6 undo changes from revision 719426c9e1eb: removed Perl script for ATP invocation, measuring time using Bash-builtin "time";
boehmes
parents:
diff changeset
    67
      "constructing proof object\n";
3711565687a6 undo changes from revision 719426c9e1eb: removed Perl script for ATP invocation, measuring time using Bash-builtin "time";
boehmes
parents:
diff changeset
    68
  }
3711565687a6 undo changes from revision 719426c9e1eb: removed Perl script for ATP invocation, measuring time using Bash-builtin "time";
boehmes
parents:
diff changeset
    69
  elsif ($content =~ m/Watchlist is empty!/) {
3711565687a6 undo changes from revision 719426c9e1eb: removed Perl script for ATP invocation, measuring time using Bash-builtin "time";
boehmes
parents:
diff changeset
    70
    print "# All watchlist clauses generated, constructing derivation\n";
3711565687a6 undo changes from revision 719426c9e1eb: removed Perl script for ATP invocation, measuring time using Bash-builtin "time";
boehmes
parents:
diff changeset
    71
  }
3711565687a6 undo changes from revision 719426c9e1eb: removed Perl script for ATP invocation, measuring time using Bash-builtin "time";
boehmes
parents:
diff changeset
    72
  else {
3711565687a6 undo changes from revision 719426c9e1eb: removed Perl script for ATP invocation, measuring time using Bash-builtin "time";
boehmes
parents:
diff changeset
    73
    print "# Cannot determine problem status\n";
3711565687a6 undo changes from revision 719426c9e1eb: removed Perl script for ATP invocation, measuring time using Bash-builtin "time";
boehmes
parents:
diff changeset
    74
    exit $r;
3711565687a6 undo changes from revision 719426c9e1eb: removed Perl script for ATP invocation, measuring time using Bash-builtin "time";
boehmes
parents:
diff changeset
    75
  }
3711565687a6 undo changes from revision 719426c9e1eb: removed Perl script for ATP invocation, measuring time using Bash-builtin "time";
boehmes
parents:
diff changeset
    76
}
3711565687a6 undo changes from revision 719426c9e1eb: removed Perl script for ATP invocation, measuring time using Bash-builtin "time";
boehmes
parents:
diff changeset
    77
else {
3711565687a6 undo changes from revision 719426c9e1eb: removed Perl script for ATP invocation, measuring time using Bash-builtin "time";
boehmes
parents:
diff changeset
    78
  print "# Cannot determine problem status within resource limit\n";
3711565687a6 undo changes from revision 719426c9e1eb: removed Perl script for ATP invocation, measuring time using Bash-builtin "time";
boehmes
parents:
diff changeset
    79
  exit $r;
3711565687a6 undo changes from revision 719426c9e1eb: removed Perl script for ATP invocation, measuring time using Bash-builtin "time";
boehmes
parents:
diff changeset
    80
}
3711565687a6 undo changes from revision 719426c9e1eb: removed Perl script for ATP invocation, measuring time using Bash-builtin "time";
boehmes
parents:
diff changeset
    81
3711565687a6 undo changes from revision 719426c9e1eb: removed Perl script for ATP invocation, measuring time using Bash-builtin "time";
boehmes
parents:
diff changeset
    82
32595
2953c3917e21 added time limit for extraction phase (not supported on Cygwin)
boehmes
parents: 32593
diff changeset
    83
# translate E output
32593
3711565687a6 undo changes from revision 719426c9e1eb: removed Perl script for ATP invocation, measuring time using Bash-builtin "time";
boehmes
parents:
diff changeset
    84
3711565687a6 undo changes from revision 719426c9e1eb: removed Perl script for ATP invocation, measuring time using Bash-builtin "time";
boehmes
parents:
diff changeset
    85
foreach (@lines) {
3711565687a6 undo changes from revision 719426c9e1eb: removed Perl script for ATP invocation, measuring time using Bash-builtin "time";
boehmes
parents:
diff changeset
    86
  print if (m/# SZS status/ or m/"# Failure"/);
3711565687a6 undo changes from revision 719426c9e1eb: removed Perl script for ATP invocation, measuring time using Bash-builtin "time";
boehmes
parents:
diff changeset
    87
}
32595
2953c3917e21 added time limit for extraction phase (not supported on Cygwin)
boehmes
parents: 32593
diff changeset
    88
$r = system ("exec bash -c \"ulimit -S -t $timelimit; " .
32675
5fe601aff9be added quotes for filenames;
boehmes
parents: 32595
diff changeset
    89
  "'$epclextract' $format -f --competition-framing '$filename'\"");
32595
2953c3917e21 added time limit for extraction phase (not supported on Cygwin)
boehmes
parents: 32593
diff changeset
    90
  # Note: Setting the user time is not supported on Cygwin, i.e., ulimit fails
2953c3917e21 added time limit for extraction phase (not supported on Cygwin)
boehmes
parents: 32593
diff changeset
    91
  # and prints and error message. How could we then limit the execution time?
32593
3711565687a6 undo changes from revision 719426c9e1eb: removed Perl script for ATP invocation, measuring time using Bash-builtin "time";
boehmes
parents:
diff changeset
    92
exit ($r >> 8);
3711565687a6 undo changes from revision 719426c9e1eb: removed Perl script for ATP invocation, measuring time using Bash-builtin "time";
boehmes
parents:
diff changeset
    93