--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/SMT/lib/scripts/run_smt_solver Mon Feb 08 11:01:47 2010 +0100
@@ -0,0 +1,93 @@
+#!/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;
+}
+