|
1 #!/usr/bin/env perl |
|
2 # |
|
3 # Author: Jasmin Blanchette, TU Muenchen |
|
4 # |
|
5 # Invoke Z3 with error detection and correction. |
|
6 # To use this wrapper, set |
|
7 # |
|
8 # Z3_REAL_SOLVER=/path-to-z3/z3 |
|
9 # Z3_SOLVER=$ISABELLE_HOME/src/HOL/Tools/SMT/lib/scripts/z3_wrapper |
|
10 # |
|
11 # in your "~/.isabelle/etc/settings" file. |
|
12 |
|
13 my $in_file = @ARGV[$ARGV - 1]; |
|
14 my $out_file = "/tmp/foo"; # FIXME |
|
15 my $err_file = "/tmp/bar"; # FIXME |
|
16 |
|
17 $ENV{'Z3_REAL_SOLVER'} || die "Environment variable \"Z3_REAL_SOLVER\" not set"; |
|
18 |
|
19 RUN: |
|
20 my $code = system $ENV{'Z3_REAL_SOLVER'} . " " . join(" ", @ARGV) . " >$out_file 2>$err_file"; |
|
21 |
|
22 if ($code == 0) { |
|
23 open(OUT_FILE, "<$out_file") || die "Cannot open file \"$out_file\""; |
|
24 my @out_lines = <OUT_FILE>; |
|
25 close(OUT_FILE); |
|
26 print @out_lines; |
|
27 } else { |
|
28 open(ERR_FILE, "<$err_file") || die "Cannot open file \"$err_file\""; |
|
29 my @err_lines = <ERR_FILE>; |
|
30 close(ERR_FILE); |
|
31 foreach (@err_lines) { |
|
32 if (m/[lL]ine ([0-9]+)/) { |
|
33 open(IN_FILE, "<$in_file") || die "Cannot open file \"$in_file\""; |
|
34 my @in_lines = <IN_FILE>; |
|
35 close(IN_FILE); |
|
36 delete $in_lines[$1 - 1]; |
|
37 open(IN_FILE, ">$in_file") || die "Cannot open file \"$in_file\""; |
|
38 print IN_FILE join ("", @in_lines); |
|
39 close(IN_FILE); |
|
40 goto RUN; |
|
41 } |
|
42 } |
|
43 print STDERR @err_lines; |
|
44 exit $code; |
|
45 } |