|
1 #!/usr/bin/perl -w |
|
2 # |
|
3 # eproof - run E and translate its output into TSTP format |
|
4 # |
|
5 # Author: Sascha Boehme, TU Muenchen |
|
6 # |
|
7 # This script is a port of a Bash script with the same name coming with |
|
8 # E 1.0-004 (written by Stephan Schulz). |
|
9 # |
|
10 |
|
11 |
|
12 use File::Basename qw/ dirname /; |
|
13 use File::Temp qw/ tempfile /; |
|
14 |
|
15 |
|
16 # E executables |
|
17 |
|
18 my $edir = dirname($0); |
|
19 my $eprover = "$edir/eprover"; |
|
20 my $epclextract = "$edir/epclextract"; |
|
21 |
|
22 |
|
23 # build E command from given commandline arguments |
|
24 |
|
25 my $format = ""; |
|
26 my $eprover_cmd = $eprover; |
|
27 foreach (@ARGV) { |
|
28 if (m/--tstp-out/) { |
|
29 $format = $_; |
|
30 } |
|
31 else { |
|
32 $eprover_cmd = "$eprover_cmd '$_'"; |
|
33 } |
|
34 } |
|
35 $eprover_cmd = "$eprover_cmd -l4 -R -o- --pcl-terms-compressed --pcl-compact"; |
|
36 |
|
37 |
|
38 # run E, redirecting output into a temporary file |
|
39 |
|
40 my ($fh, $filename) = tempfile(UNLINK => 1); |
|
41 my $r = system "$eprover_cmd > $filename"; |
|
42 exit ($r >> 8) if $r != 0; |
|
43 |
|
44 |
|
45 # analyze E output |
|
46 |
|
47 my @lines = <$fh>; |
|
48 my $content = join "", @lines[-60 .. -1]; |
|
49 # Note: Like the original eproof, we only look at the last 60 lines. |
|
50 |
|
51 if ($content =~ m/Total time/) { |
|
52 if ($content =~ m/No proof found!/) { |
|
53 print "# Problem is satisfiable (or invalid), " . |
|
54 "generating saturation derivation\n"; |
|
55 } |
|
56 elsif ($content =~ m/Proof found!/) { |
|
57 print "# Problem is unsatisfiable (or provable), " . |
|
58 "constructing proof object\n"; |
|
59 } |
|
60 elsif ($content =~ m/Watchlist is empty!/) { |
|
61 print "# All watchlist clauses generated, constructing derivation\n"; |
|
62 } |
|
63 else { |
|
64 print "# Cannot determine problem status\n"; |
|
65 exit $r; |
|
66 } |
|
67 } |
|
68 else { |
|
69 print "# Cannot determine problem status within resource limit\n"; |
|
70 exit $r; |
|
71 } |
|
72 |
|
73 |
|
74 # extract E output |
|
75 |
|
76 foreach (@lines) { |
|
77 print if (m/# SZS status/ or m/"# Failure"/); |
|
78 } |
|
79 $r = system "$epclextract $format -f --competition-framing $filename"; |
|
80 # Note: Before extraction, the original eproof invokes 'ulimit -S -t TIME' |
|
81 # where TIME is the remaining time from the time limit given at the command |
|
82 # line. This does not seem very reliable and is not implemented here. This |
|
83 # is not a problem as long as extraction is reasonable fast or the invoking |
|
84 # process enforces a time limit of its own. |
|
85 exit ($r >> 8); |
|
86 |