--- a/src/HOL/SMT/lib/scripts/run_smt_solver Wed Feb 17 10:28:04 2010 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,93 +0,0 @@
-#!/usr/bin/env perl
-#
-# Author: Sascha Boehme, TU Muenchen
-#
-# Cache for prover results, based on discriminating problems using MD5.
-
-use strict;
-use warnings;
-use Digest::MD5;
-
-
-# arguments
-
-my $certs_file = shift @ARGV;
-my $location = shift @ARGV;
-my $result_file = pop @ARGV;
-my $problem_file = $ARGV[-1];
-
-my $use_certs = not ($certs_file eq "-");
-
-
-# create MD5 problem digest
-
-my $problem_digest = "";
-if ($use_certs) {
- my $md5 = Digest::MD5->new;
- open FILE, "<$problem_file" or
- die "ERROR: Failed to open '$problem_file' ($!)";
- $md5->addfile(*FILE);
- close FILE;
- $problem_digest = $md5->b64digest;
-}
-
-
-# lookup problem digest among existing certificates and
-# return a cached result (if there is a certificate for the problem)
-
-if ($use_certs and -e $certs_file) {
- my $cached = 0;
- open CERTS, "<$certs_file" or die "ERROR: Failed to open '$certs_file' ($!)";
- while (<CERTS>) {
- if (m/(\S+) (\d+)/) {
- if ($1 eq $problem_digest) {
- my $start = tell CERTS;
- open FILE, ">$result_file" or
- die "ERROR: Failed to open '$result_file ($!)";
- while ((tell CERTS) - $start < $2) {
- my $line = <CERTS>;
- print FILE $line;
- }
- close FILE;
- $cached = 1;
- last;
- }
- else { seek CERTS, $2, 1; }
- }
- else { die "ERROR: Invalid file format in '$certs_file'"; }
- }
- close CERTS;
- if ($cached) { exit 0; }
-}
-
-
-# invoke (remote or local) prover
-
-my $result;
-
-if ($location eq "remote") {
- $result = system "$ENV{'REMOTE_SMT'} @ARGV >$result_file 2>&1";
-}
-elsif ($location eq "local") {
- $result = system "@ARGV >$result_file 2>&1";
-}
-else { die "ERROR: No SMT solver invoked"; }
-
-
-# cache result
-
-if ($use_certs) {
- open CERTS, ">>$certs_file" or
- die "ERROR: Failed to open '$certs_file' ($!)";
- print CERTS
- ("$problem_digest " . ((-s $result_file) + (length "\n")) . "\n");
-
- open FILE, "<$result_file" or
- die "ERROR: Failed to open '$result_file' ($!)";
- foreach (<FILE>) { print CERTS $_; }
- close FILE;
-
- print CERTS "\n";
- close CERTS;
-}
-