author | blanchet |
Thu, 16 Dec 2010 21:21:13 +0100 | |
changeset 41216 | 5cee84180cd7 |
parent 41213 | ee24717e3fe3 |
child 41218 | 028449eb1548 |
permissions | -rwxr-xr-x |
41213
ee24717e3fe3
added self-correcting wrapper for Z3 -- see comment in the file for details
blanchet
parents:
diff
changeset
|
1 |
#!/usr/bin/env perl |
ee24717e3fe3
added self-correcting wrapper for Z3 -- see comment in the file for details
blanchet
parents:
diff
changeset
|
2 |
# |
ee24717e3fe3
added self-correcting wrapper for Z3 -- see comment in the file for details
blanchet
parents:
diff
changeset
|
3 |
# Author: Jasmin Blanchette, TU Muenchen |
ee24717e3fe3
added self-correcting wrapper for Z3 -- see comment in the file for details
blanchet
parents:
diff
changeset
|
4 |
# |
ee24717e3fe3
added self-correcting wrapper for Z3 -- see comment in the file for details
blanchet
parents:
diff
changeset
|
5 |
# Invoke Z3 with error detection and correction. |
ee24717e3fe3
added self-correcting wrapper for Z3 -- see comment in the file for details
blanchet
parents:
diff
changeset
|
6 |
# To use this wrapper, set |
ee24717e3fe3
added self-correcting wrapper for Z3 -- see comment in the file for details
blanchet
parents:
diff
changeset
|
7 |
# |
ee24717e3fe3
added self-correcting wrapper for Z3 -- see comment in the file for details
blanchet
parents:
diff
changeset
|
8 |
# Z3_REAL_SOLVER=/path-to-z3/z3 |
ee24717e3fe3
added self-correcting wrapper for Z3 -- see comment in the file for details
blanchet
parents:
diff
changeset
|
9 |
# Z3_SOLVER=$ISABELLE_HOME/src/HOL/Tools/SMT/lib/scripts/z3_wrapper |
ee24717e3fe3
added self-correcting wrapper for Z3 -- see comment in the file for details
blanchet
parents:
diff
changeset
|
10 |
# |
ee24717e3fe3
added self-correcting wrapper for Z3 -- see comment in the file for details
blanchet
parents:
diff
changeset
|
11 |
# in your "~/.isabelle/etc/settings" file. |
ee24717e3fe3
added self-correcting wrapper for Z3 -- see comment in the file for details
blanchet
parents:
diff
changeset
|
12 |
|
41216 | 13 |
use POSIX; |
14 |
||
41213
ee24717e3fe3
added self-correcting wrapper for Z3 -- see comment in the file for details
blanchet
parents:
diff
changeset
|
15 |
my $in_file = @ARGV[$ARGV - 1]; |
41216 | 16 |
my $out_file = tmpnam(); |
17 |
my $err_file = tmpnam(); |
|
18 |
||
19 |
print ; |
|
41213
ee24717e3fe3
added self-correcting wrapper for Z3 -- see comment in the file for details
blanchet
parents:
diff
changeset
|
20 |
|
ee24717e3fe3
added self-correcting wrapper for Z3 -- see comment in the file for details
blanchet
parents:
diff
changeset
|
21 |
$ENV{'Z3_REAL_SOLVER'} || die "Environment variable \"Z3_REAL_SOLVER\" not set"; |
ee24717e3fe3
added self-correcting wrapper for Z3 -- see comment in the file for details
blanchet
parents:
diff
changeset
|
22 |
|
ee24717e3fe3
added self-correcting wrapper for Z3 -- see comment in the file for details
blanchet
parents:
diff
changeset
|
23 |
RUN: |
ee24717e3fe3
added self-correcting wrapper for Z3 -- see comment in the file for details
blanchet
parents:
diff
changeset
|
24 |
my $code = system $ENV{'Z3_REAL_SOLVER'} . " " . join(" ", @ARGV) . " >$out_file 2>$err_file"; |
ee24717e3fe3
added self-correcting wrapper for Z3 -- see comment in the file for details
blanchet
parents:
diff
changeset
|
25 |
|
ee24717e3fe3
added self-correcting wrapper for Z3 -- see comment in the file for details
blanchet
parents:
diff
changeset
|
26 |
if ($code == 0) { |
ee24717e3fe3
added self-correcting wrapper for Z3 -- see comment in the file for details
blanchet
parents:
diff
changeset
|
27 |
open(OUT_FILE, "<$out_file") || die "Cannot open file \"$out_file\""; |
ee24717e3fe3
added self-correcting wrapper for Z3 -- see comment in the file for details
blanchet
parents:
diff
changeset
|
28 |
my @out_lines = <OUT_FILE>; |
ee24717e3fe3
added self-correcting wrapper for Z3 -- see comment in the file for details
blanchet
parents:
diff
changeset
|
29 |
close(OUT_FILE); |
ee24717e3fe3
added self-correcting wrapper for Z3 -- see comment in the file for details
blanchet
parents:
diff
changeset
|
30 |
print @out_lines; |
ee24717e3fe3
added self-correcting wrapper for Z3 -- see comment in the file for details
blanchet
parents:
diff
changeset
|
31 |
} else { |
ee24717e3fe3
added self-correcting wrapper for Z3 -- see comment in the file for details
blanchet
parents:
diff
changeset
|
32 |
open(ERR_FILE, "<$err_file") || die "Cannot open file \"$err_file\""; |
ee24717e3fe3
added self-correcting wrapper for Z3 -- see comment in the file for details
blanchet
parents:
diff
changeset
|
33 |
my @err_lines = <ERR_FILE>; |
ee24717e3fe3
added self-correcting wrapper for Z3 -- see comment in the file for details
blanchet
parents:
diff
changeset
|
34 |
close(ERR_FILE); |
41216 | 35 |
print STDERR @err_lines; |
41213
ee24717e3fe3
added self-correcting wrapper for Z3 -- see comment in the file for details
blanchet
parents:
diff
changeset
|
36 |
foreach (@err_lines) { |
ee24717e3fe3
added self-correcting wrapper for Z3 -- see comment in the file for details
blanchet
parents:
diff
changeset
|
37 |
if (m/[lL]ine ([0-9]+)/) { |
ee24717e3fe3
added self-correcting wrapper for Z3 -- see comment in the file for details
blanchet
parents:
diff
changeset
|
38 |
open(IN_FILE, "<$in_file") || die "Cannot open file \"$in_file\""; |
ee24717e3fe3
added self-correcting wrapper for Z3 -- see comment in the file for details
blanchet
parents:
diff
changeset
|
39 |
my @in_lines = <IN_FILE>; |
ee24717e3fe3
added self-correcting wrapper for Z3 -- see comment in the file for details
blanchet
parents:
diff
changeset
|
40 |
close(IN_FILE); |
ee24717e3fe3
added self-correcting wrapper for Z3 -- see comment in the file for details
blanchet
parents:
diff
changeset
|
41 |
delete $in_lines[$1 - 1]; |
ee24717e3fe3
added self-correcting wrapper for Z3 -- see comment in the file for details
blanchet
parents:
diff
changeset
|
42 |
open(IN_FILE, ">$in_file") || die "Cannot open file \"$in_file\""; |
ee24717e3fe3
added self-correcting wrapper for Z3 -- see comment in the file for details
blanchet
parents:
diff
changeset
|
43 |
print IN_FILE join ("", @in_lines); |
ee24717e3fe3
added self-correcting wrapper for Z3 -- see comment in the file for details
blanchet
parents:
diff
changeset
|
44 |
close(IN_FILE); |
ee24717e3fe3
added self-correcting wrapper for Z3 -- see comment in the file for details
blanchet
parents:
diff
changeset
|
45 |
goto RUN; |
ee24717e3fe3
added self-correcting wrapper for Z3 -- see comment in the file for details
blanchet
parents:
diff
changeset
|
46 |
} |
ee24717e3fe3
added self-correcting wrapper for Z3 -- see comment in the file for details
blanchet
parents:
diff
changeset
|
47 |
} |
ee24717e3fe3
added self-correcting wrapper for Z3 -- see comment in the file for details
blanchet
parents:
diff
changeset
|
48 |
} |
41216 | 49 |
|
50 |
unlink($out_file); |
|
51 |
unlink($err_file); |
|
52 |
exit $code; |