src/HOL/Tools/SMT/lib/scripts/z3_wrapper

clarified example settings for Proof General;

#!/usr/bin/env perl
#
# Author: Jasmin Blanchette, TU Muenchen
#
# Invoke Z3 with error detection and correction.
# To use this wrapper, set
#
#     Z3_REAL_SOLVER=/path-to-z3/z3
#     Z3_SOLVER=$ISABELLE_HOME/src/HOL/Tools/SMT/lib/scripts/z3_wrapper
#
# in your "~/.isabelle/etc/settings" file.

use strict;
use warnings;
use POSIX;

my $in_file = $ARGV[$#ARGV];
my $out_file = tmpnam();
my $err_file = tmpnam();

$ENV{'Z3_REAL_SOLVER'} || exit 10;

RUN:
my $code = system $ENV{'Z3_REAL_SOLVER'} . " " . join(" ", @ARGV) . " >$out_file 2>$err_file";

open(ERR_FILE, "<$err_file") || exit 11;
my @err_lines = <ERR_FILE>;
close(ERR_FILE);
print STDERR join("", @err_lines);

if ($code != 0) {
  foreach my $err_line (reverse(@err_lines)) {
    if ($err_line =~ /[lL]ine ([0-9]+)/) {
      my $line_num = $1;

      open(IN_FILE, "<$in_file") || exit 12;
      my @in_lines = <IN_FILE>;
      close(IN_FILE);

      $err_line =~ s/[\n\r]//g;
      $in_lines[$line_num - 1] = ";;; " . $err_line . " -- "
                                 . $in_lines[$line_num - 1];

      open(IN_FILE, ">$in_file") || exit 13;
      print IN_FILE join ("", @in_lines);
      close(IN_FILE);
      goto RUN;
    }
  }
}

open(OUT_FILE, "<$out_file") || exit 14;
my @out_lines = <OUT_FILE>;
close(OUT_FILE);
print join("", @out_lines);

unlink($out_file);
unlink($err_file);
exit(($code >> 8 | $code) & 0xff);