# HG changeset patch
# User boehmes
# Date 1265623307 -3600
# Node ID 0ea45a4d32f381bbf5a5b07727e926ea43e0b06b
# Parent  0faeabd99289981d65e43881208ba7c4d963e9bb
split SMT perl script: certificate caching and invokation of remote solvers are now in separate scripts,
modernized perl scripts: prefer standalone executables

diff -r 0faeabd99289 -r 0ea45a4d32f3 src/HOL/SMT/Tools/smt_solver.ML
--- a/src/HOL/SMT/Tools/smt_solver.ML	Sun Feb 07 20:44:25 2010 +0100
+++ b/src/HOL/SMT/Tools/smt_solver.ML	Mon Feb 08 11:01:47 2010 +0100
@@ -156,7 +156,7 @@
       else (["certificate"], "Using certificate from " ^ quote certs' ^ " ...")
     val _ = tracing msg
   in
-    bash_output (space_implode " " ("perl -w" ::
+    bash_output (space_implode " " (
       File.shell_path (Path.explode (getenv "RUN_SMT_SOLVER")) :: certs' ::
       map File.shell_quote (solver @ args) @
       map File.shell_path [problem_path, proof_path]) ^ " 2>&1")
diff -r 0faeabd99289 -r 0ea45a4d32f3 src/HOL/SMT/etc/settings
--- a/src/HOL/SMT/etc/settings	Sun Feb 07 20:44:25 2010 +0100
+++ b/src/HOL/SMT/etc/settings	Mon Feb 08 11:01:47 2010 +0100
@@ -1,6 +1,7 @@
 ISABELLE_SMT="$COMPONENT"
 
-RUN_SMT_SOLVER="$ISABELLE_SMT/lib/scripts/run_smt_solver.pl"
+RUN_SMT_SOLVER="$ISABELLE_SMT/lib/scripts/run_smt_solver"
+REMOTE_SMT="$ISABELLE_SMT/lib/scripts/remote_smt"
 
 REMOTE_SMT_URL="http://smt.in.tum.de/smt"
 
diff -r 0faeabd99289 -r 0ea45a4d32f3 src/HOL/SMT/lib/scripts/remote_smt
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/SMT/lib/scripts/remote_smt	Mon Feb 08 11:01:47 2010 +0100
@@ -0,0 +1,31 @@
+#!/usr/bin/env perl
+#
+# Author: Sascha Boehme, TU Muenchen
+#
+# Invoke remote SMT solvers.
+
+use strict;
+use warnings;
+use LWP;
+
+
+# arguments
+
+my $solver = $ARGV[0];
+my @options = @ARGV[1 .. ($#ARGV - 1)];
+my $problem_file = $ARGV[-1];
+
+
+# call solver
+
+my $agent = LWP::UserAgent->new;
+$agent->agent("SMT-Request");
+$agent->timeout(180);
+my $response = $agent->post($ENV{"REMOTE_SMT_URL"}, [
+  "Solver" => $solver,
+  "Options" => join(" ", @options),
+  "Problem" => [$problem_file] ],
+  "Content_Type" => "form-data");
+if (not $response->is_success) { die "HTTP-Error: " . $response->message; }
+else { print $response->content; }
+
diff -r 0faeabd99289 -r 0ea45a4d32f3 src/HOL/SMT/lib/scripts/run_smt_solver
--- /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;
+}
+
diff -r 0faeabd99289 -r 0ea45a4d32f3 src/HOL/SMT/lib/scripts/run_smt_solver.pl
--- a/src/HOL/SMT/lib/scripts/run_smt_solver.pl	Sun Feb 07 20:44:25 2010 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,110 +0,0 @@
-#
-# Author: Sascha Boehme, TU Muenchen
-#
-# Cache for prover results, based on discriminating problems using MD5.
-
-use strict;
-use warnings;
-use Digest::MD5;
-use LWP;
-
-
-# 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
-
-if ($location eq "remote") {
-  # arguments
-  my $solver = $ARGV[0];
-  my @options = @ARGV[1 .. ($#ARGV - 1)];
-
-  # call solver
-  my $agent = LWP::UserAgent->new;
-  $agent->agent("SMT-Request");
-  $agent->timeout(180);
-  my $response = $agent->post($ENV{"REMOTE_SMT_URL"}, [
-    "Solver" => $solver,
-    "Options" => join(" ", @options),
-    "Problem" => [$problem_file] ],
-    "Content_Type" => "form-data");
-  if (not $response->is_success) { die "HTTP-Error: " . $response->message; }
-  else {
-    open FILE, ">$result_file" or
-      die "ERROR: Failed to create '$result_file' ($!)";
-    print FILE $response->content;
-    close FILE;
-  }
-}
-elsif ($location eq "local") {
-  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;
-}
-