author | boehmes |
Thu, 17 Sep 2009 11:57:36 +0200 | |
changeset 32593 | 3711565687a6 |
child 32595 | 2953c3917e21 |
permissions | -rwxr-xr-x |
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 /; |
3711565687a6
undo changes from revision 719426c9e1eb: removed Perl script for ATP invocation, measuring time using Bash-builtin "time";
boehmes
parents:
diff
changeset
|
14 |
|
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 |
# E executables |
3711565687a6
undo changes from revision 719426c9e1eb: removed Perl script for ATP invocation, measuring time using Bash-builtin "time";
boehmes
parents:
diff
changeset
|
17 |
|
3711565687a6
undo changes from revision 719426c9e1eb: removed Perl script for ATP invocation, measuring time using Bash-builtin "time";
boehmes
parents:
diff
changeset
|
18 |
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
|
19 |
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
|
20 |
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
|
21 |
|
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 |
# 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
|
24 |
|
3711565687a6
undo changes from revision 719426c9e1eb: removed Perl script for ATP invocation, measuring time using Bash-builtin "time";
boehmes
parents:
diff
changeset
|
25 |
my $format = ""; |
3711565687a6
undo changes from revision 719426c9e1eb: removed Perl script for ATP invocation, measuring time using Bash-builtin "time";
boehmes
parents:
diff
changeset
|
26 |
my $eprover_cmd = $eprover; |
3711565687a6
undo changes from revision 719426c9e1eb: removed Perl script for ATP invocation, measuring time using Bash-builtin "time";
boehmes
parents:
diff
changeset
|
27 |
foreach (@ARGV) { |
3711565687a6
undo changes from revision 719426c9e1eb: removed Perl script for ATP invocation, measuring time using Bash-builtin "time";
boehmes
parents:
diff
changeset
|
28 |
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
|
29 |
$format = $_; |
3711565687a6
undo changes from revision 719426c9e1eb: removed Perl script for ATP invocation, measuring time using Bash-builtin "time";
boehmes
parents:
diff
changeset
|
30 |
} |
3711565687a6
undo changes from revision 719426c9e1eb: removed Perl script for ATP invocation, measuring time using Bash-builtin "time";
boehmes
parents:
diff
changeset
|
31 |
else { |
3711565687a6
undo changes from revision 719426c9e1eb: removed Perl script for ATP invocation, measuring time using Bash-builtin "time";
boehmes
parents:
diff
changeset
|
32 |
$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
|
33 |
} |
3711565687a6
undo changes from revision 719426c9e1eb: removed Perl script for ATP invocation, measuring time using Bash-builtin "time";
boehmes
parents:
diff
changeset
|
34 |
} |
3711565687a6
undo changes from revision 719426c9e1eb: removed Perl script for ATP invocation, measuring time using Bash-builtin "time";
boehmes
parents:
diff
changeset
|
35 |
$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
|
36 |
|
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 |
# 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
|
39 |
|
3711565687a6
undo changes from revision 719426c9e1eb: removed Perl script for ATP invocation, measuring time using Bash-builtin "time";
boehmes
parents:
diff
changeset
|
40 |
my ($fh, $filename) = tempfile(UNLINK => 1); |
3711565687a6
undo changes from revision 719426c9e1eb: removed Perl script for ATP invocation, measuring time using Bash-builtin "time";
boehmes
parents:
diff
changeset
|
41 |
my $r = system "$eprover_cmd > $filename"; |
3711565687a6
undo changes from revision 719426c9e1eb: removed Perl script for ATP invocation, measuring time using Bash-builtin "time";
boehmes
parents:
diff
changeset
|
42 |
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
|
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 |
# 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
|
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 @lines = <$fh>; |
3711565687a6
undo changes from revision 719426c9e1eb: removed Perl script for ATP invocation, measuring time using Bash-builtin "time";
boehmes
parents:
diff
changeset
|
48 |
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
|
49 |
# 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
|
50 |
|
3711565687a6
undo changes from revision 719426c9e1eb: removed Perl script for ATP invocation, measuring time using Bash-builtin "time";
boehmes
parents:
diff
changeset
|
51 |
if ($content =~ m/Total time/) { |
3711565687a6
undo changes from revision 719426c9e1eb: removed Perl script for ATP invocation, measuring time using Bash-builtin "time";
boehmes
parents:
diff
changeset
|
52 |
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
|
53 |
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
|
54 |
"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
|
55 |
} |
3711565687a6
undo changes from revision 719426c9e1eb: removed Perl script for ATP invocation, measuring time using Bash-builtin "time";
boehmes
parents:
diff
changeset
|
56 |
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
|
57 |
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
|
58 |
"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
|
59 |
} |
3711565687a6
undo changes from revision 719426c9e1eb: removed Perl script for ATP invocation, measuring time using Bash-builtin "time";
boehmes
parents:
diff
changeset
|
60 |
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
|
61 |
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
|
62 |
} |
3711565687a6
undo changes from revision 719426c9e1eb: removed Perl script for ATP invocation, measuring time using Bash-builtin "time";
boehmes
parents:
diff
changeset
|
63 |
else { |
3711565687a6
undo changes from revision 719426c9e1eb: removed Perl script for ATP invocation, measuring time using Bash-builtin "time";
boehmes
parents:
diff
changeset
|
64 |
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
|
65 |
exit $r; |
3711565687a6
undo changes from revision 719426c9e1eb: removed Perl script for ATP invocation, measuring time using Bash-builtin "time";
boehmes
parents:
diff
changeset
|
66 |
} |
3711565687a6
undo changes from revision 719426c9e1eb: removed Perl script for ATP invocation, measuring time using Bash-builtin "time";
boehmes
parents:
diff
changeset
|
67 |
} |
3711565687a6
undo changes from revision 719426c9e1eb: removed Perl script for ATP invocation, measuring time using Bash-builtin "time";
boehmes
parents:
diff
changeset
|
68 |
else { |
3711565687a6
undo changes from revision 719426c9e1eb: removed Perl script for ATP invocation, measuring time using Bash-builtin "time";
boehmes
parents:
diff
changeset
|
69 |
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
|
70 |
exit $r; |
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 |
|
3711565687a6
undo changes from revision 719426c9e1eb: removed Perl script for ATP invocation, measuring time using Bash-builtin "time";
boehmes
parents:
diff
changeset
|
73 |
|
3711565687a6
undo changes from revision 719426c9e1eb: removed Perl script for ATP invocation, measuring time using Bash-builtin "time";
boehmes
parents:
diff
changeset
|
74 |
# extract E output |
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 |
foreach (@lines) { |
3711565687a6
undo changes from revision 719426c9e1eb: removed Perl script for ATP invocation, measuring time using Bash-builtin "time";
boehmes
parents:
diff
changeset
|
77 |
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
|
78 |
} |
3711565687a6
undo changes from revision 719426c9e1eb: removed Perl script for ATP invocation, measuring time using Bash-builtin "time";
boehmes
parents:
diff
changeset
|
79 |
$r = system "$epclextract $format -f --competition-framing $filename"; |
3711565687a6
undo changes from revision 719426c9e1eb: removed Perl script for ATP invocation, measuring time using Bash-builtin "time";
boehmes
parents:
diff
changeset
|
80 |
# Note: Before extraction, the original eproof invokes 'ulimit -S -t TIME' |
3711565687a6
undo changes from revision 719426c9e1eb: removed Perl script for ATP invocation, measuring time using Bash-builtin "time";
boehmes
parents:
diff
changeset
|
81 |
# where TIME is the remaining time from the time limit given at the command |
3711565687a6
undo changes from revision 719426c9e1eb: removed Perl script for ATP invocation, measuring time using Bash-builtin "time";
boehmes
parents:
diff
changeset
|
82 |
# line. This does not seem very reliable and is not implemented here. This |
3711565687a6
undo changes from revision 719426c9e1eb: removed Perl script for ATP invocation, measuring time using Bash-builtin "time";
boehmes
parents:
diff
changeset
|
83 |
# is not a problem as long as extraction is reasonable fast or the invoking |
3711565687a6
undo changes from revision 719426c9e1eb: removed Perl script for ATP invocation, measuring time using Bash-builtin "time";
boehmes
parents:
diff
changeset
|
84 |
# process enforces a time limit of its own. |
3711565687a6
undo changes from revision 719426c9e1eb: removed Perl script for ATP invocation, measuring time using Bash-builtin "time";
boehmes
parents:
diff
changeset
|
85 |
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
|
86 |