# HG changeset patch
# User blanchet
# Date 1297268337 -3600
# Node ID 2b896f7f232db499b69533c7459bb8c9cec46f8f
# Parent  eb98c60a6cf0b984fbea8c20c4c7d99ad2acc24b
remove Z3 wrapper script, which is no longer necessary now that the SMT module generates SMT-LIB compliant files

diff -r eb98c60a6cf0 -r 2b896f7f232d src/HOL/Tools/SMT/lib/scripts/z3_wrapper
--- a/src/HOL/Tools/SMT/lib/scripts/z3_wrapper	Wed Feb 09 17:18:57 2011 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,59 +0,0 @@
-#!/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);