# HG changeset patch
# User bulwahn
# Date 1257530556 -3600
# Node ID 5bf9a3d5d4ff35ee24752038052c2b3d27869524
# Parent  826a490f6482678b48c445b3f35915ba0350b605# Parent  e88f67d679c47173962eeb07e072d04cb6e488e5
merged

diff -r 826a490f6482 -r 5bf9a3d5d4ff NEWS
--- a/NEWS	Fri Nov 06 16:59:17 2009 +0100
+++ b/NEWS	Fri Nov 06 19:02:36 2009 +0100
@@ -54,6 +54,8 @@
 solvers using the oracle mechanism; for the SMT solver Z3,
 this method is proof-producing. Certificates are provided to
 avoid calling the external solvers solely for re-checking proofs.
+Due to a remote SMT service there is no need for installing SMT
+solvers locally.
 
 * New commands to load and prove verification conditions
 generated by the Boogie program verifier or derived systems
diff -r 826a490f6482 -r 5bf9a3d5d4ff src/HOL/SMT/Examples/SMT_Examples.thy
--- a/src/HOL/SMT/Examples/SMT_Examples.thy	Fri Nov 06 16:59:17 2009 +0100
+++ b/src/HOL/SMT/Examples/SMT_Examples.thy	Fri Nov 06 19:02:36 2009 +0100
@@ -549,7 +549,7 @@
 
 section {* Bitvectors *}
 
-locale bv
+locale z3_bv_test
 begin
 
 text {*
diff -r 826a490f6482 -r 5bf9a3d5d4ff src/HOL/SMT/SMT.thy
--- a/src/HOL/SMT/SMT.thy	Fri Nov 06 16:59:17 2009 +0100
+++ b/src/HOL/SMT/SMT.thy	Fri Nov 06 19:02:36 2009 +0100
@@ -13,9 +13,59 @@
 
 setup {* CVC3_Solver.setup #> Yices_Solver.setup *}
 
-declare [[ smt_solver = z3, smt_timeout = 20 ]]
+
+
+section {* Setup *}
+
+text {*
+Without further ado, the SMT solvers CVC3 and Z3 are provided
+remotely via an SMT server. For faster responses, the solver
+environment variables CVC3_SOLVER, YICES_SOLVER, and Z3_SOLVER
+need to point to the respective SMT solver executable.
+*}
+
+
+
+section {* Available configuration options *}
+
+text {* Choose the SMT solver to be applied (one of cvc3, yices, or z3): *}
+
+declare [[ smt_solver = z3 ]]
+
+text {* Restrict the runtime of an SMT solver (in seconds): *}
+
+declare [[ smt_timeout = 20 ]]
+
+
+subsection {* Z3-specific options *}
+
+text {* Enable proof reconstruction for Z3: *}
+
+declare [[ z3_proofs = false ]]
+
+text {* Pass extra command-line arguments to Z3
+to control its behaviour: *}
+
+declare [[ z3_options = "" ]]
+
+
+subsection {* Special configuration options *}
+
+text {*
+Trace the problem file, the result of the SMT solver and
+further information: *}
+
+declare [[ smt_trace = false ]]
+
+text {* Unfold (some) definitions passed to the SMT solver: *}
+
 declare [[ smt_unfold_defs = true ]]
-declare [[ smt_trace = false, smt_keep = "", smt_cert = "" ]]
-declare [[ z3_proofs = false, z3_options = "" ]]
+
+text {*
+Produce or use certificates (to avoid repeated invocation of an
+SMT solver again and again). The value is an absolute path
+pointing to the problem file. See also the examples. *}
+
+declare [[ smt_keep = "", smt_cert = "" ]]
 
 end
diff -r 826a490f6482 -r 5bf9a3d5d4ff src/HOL/SMT/Tools/cvc3_solver.ML
--- a/src/HOL/SMT/Tools/cvc3_solver.ML	Fri Nov 06 16:59:17 2009 +0100
+++ b/src/HOL/SMT/Tools/cvc3_solver.ML	Fri Nov 06 19:02:36 2009 +0100
@@ -36,7 +36,7 @@
   end
 
 fun smtlib_solver oracle _ = {
-  command = {env_var=env_var, remote_name=solver_name},
+  command = {env_var=env_var, remote_name=SOME solver_name},
   arguments = options,
   interface = SMTLIB_Interface.interface,
   reconstruct = oracle }
diff -r 826a490f6482 -r 5bf9a3d5d4ff src/HOL/SMT/Tools/smt_solver.ML
--- a/src/HOL/SMT/Tools/smt_solver.ML	Fri Nov 06 16:59:17 2009 +0100
+++ b/src/HOL/SMT/Tools/smt_solver.ML	Fri Nov 06 19:02:36 2009 +0100
@@ -18,7 +18,7 @@
     recon: SMT_Translate.recon,
     assms: thm list option }
   type solver_config = {
-    command: {env_var: string, remote_name: string},
+    command: {env_var: string, remote_name: string option},
     arguments: string list,
     interface: interface,
     reconstruct: proof_data -> thm }
@@ -69,7 +69,7 @@
   assms: thm list option }
 
 type solver_config = {
-  command: {env_var: string, remote_name: string},
+  command: {env_var: string, remote_name: string option},
   arguments: string list,
   interface: interface,
   reconstruct: proof_data -> thm }
@@ -96,7 +96,7 @@
 
 local
 
-fun with_files ctxt f x =
+fun with_files ctxt f =
   let
     fun make_names n = (n, n ^ ".proof")
 
@@ -107,43 +107,79 @@
       else pairself (File.tmp_path o Path.explode)
         (make_names ("smt-" ^ serial_string ()))
 
-    val y = Exn.capture (f problem_path proof_path) x
+    val y = Exn.capture f (problem_path, proof_path)
 
     val _ = if keep' = "" then (pairself (try File.rm) paths; ()) else ()
   in Exn.release y end
 
-fun run in_path out_path (ctxt, cmd, output) =
+fun invoke ctxt output f (paths as (problem_path, proof_path)) =
   let
     fun pretty tag ls = Pretty.string_of (Pretty.big_list tag
       (map Pretty.str ls))
 
-    val x = File.open_output output in_path
+    val x = File.open_output output problem_path
     val _ = trace_msg ctxt (pretty "SMT problem:" o split_lines o File.read)
-      in_path
+      problem_path
 
-    val _ = with_timeout ctxt system_out (cmd in_path out_path)
-    fun lines_of path = the_default [] (try (File.fold_lines cons out_path) [])
-    val ls = rev (dropwhile (equal "") (lines_of out_path))
+    val _ = with_timeout ctxt f paths
+    fun lines_of path = the_default [] (try (File.fold_lines cons path) [])
+    val ls = rev (dropwhile (equal "") (lines_of proof_path))
     val _ = trace_msg ctxt (pretty "SMT result:") ls
   in (x, ls) end
 
+val expand_name = Path.implode o Path.expand o Path.explode 
+
+fun run_perl name args ps =
+  system_out (space_implode " " ("perl -w" ::
+    File.shell_path (Path.explode (getenv name)) ::
+    map File.shell_quote args @ ps))
+
+fun use_certificate ctxt ps =
+  let val name = Config.get ctxt cert
+  in
+    if name = "" then false
+    else
+     (tracing ("Using certificate " ^ quote (expand_name name) ^ " ...");
+      run_perl "CERT_SMT_SOLVER" [expand_name name] ps;
+      true)
+  end
+
+fun run_locally f ctxt env_var args ps =
+  if getenv env_var = ""
+  then f ("Undefined Isabelle environment variable: " ^ quote env_var)
+  else
+    let val app = Path.expand (Path.explode (getenv env_var))
+    in
+      if not (File.exists app)
+      then f ("No such file: " ^ quote (Path.implode app))
+      else
+       (tracing ("Invoking local SMT solver " ^ quote (Path.implode app) ^
+          " ...");
+        system_out (space_implode " " (File.shell_path app ::
+        map File.shell_quote args @ ps)); ())
+    end
+
+fun run_remote remote_name args ps msg =
+  (case remote_name of
+    NONE => error msg
+  | SOME name =>
+      let
+        val url = getenv "REMOTE_SMT_URL"
+        val _ = tracing ("Invoking remote SMT solver " ^ quote name ^ " at " ^
+          quote url ^ " ...")
+      in (run_perl "REMOTE_SMT_SOLVER" (url :: name :: args) ps; ()) end)
+
+fun run ctxt {env_var, remote_name} args (problem_path, proof_path) =
+  let val ps = [File.shell_path problem_path, ">", File.shell_path proof_path]
+  in
+    if use_certificate ctxt ps then ()
+    else run_locally (run_remote remote_name args ps) ctxt env_var args ps
+  end
+
 in
 
-fun run_solver ctxt {env_var, remote_name} args output =
-  let
-    val qf = File.shell_path and qq = File.shell_quote
-    val qs = qf o Path.explode
-    val local_name = getenv env_var
-    val cert_name = Config.get ctxt cert
-    val remote = qs (getenv "REMOTE_SMT_SOLVER")
-    val cert_script = qs (getenv "CERT_SMT_SOLVER")
-    fun cmd f1 f2 =
-      if cert_name <> ""
-      then "perl -w" :: [cert_script, qs cert_name, qf f1, ">", qf f2]
-      else if local_name <> ""
-      then qs local_name :: map qq args @ [qf f1, ">", qf f2]
-      else "perl -w" :: remote :: map qq (remote_name :: args) @ [qf f1, qf f2]
-  in with_files ctxt run (ctxt, space_implode " " oo cmd, output) end
+fun run_solver ctxt cmd args output =
+  with_files ctxt (invoke ctxt output (run ctxt cmd args))
 
 end
 
@@ -223,13 +259,13 @@
         (map (Syntax.pretty_term ctxt) ex))
     end
 
-  fun fail_tac ctxt msg st = (trace_msg ctxt I msg; Tactical.no_tac st)
+  fun fail_tac f msg st = (f msg; Tactical.no_tac st)
 
   fun SAFE pass_exns tac ctxt i st =
     if pass_exns then tac ctxt i st
     else (tac ctxt i st
-      handle SMT msg => fail_tac ctxt ("SMT: " ^ msg) st
-           | SMT_COUNTEREXAMPLE cex => fail_tac ctxt (pretty_cex ctxt cex) st)
+      handle SMT msg => fail_tac (trace_msg ctxt (prefix "SMT: ")) msg st
+           | SMT_COUNTEREXAMPLE ce => fail_tac tracing (pretty_cex ctxt ce) st)
 
   fun smt_solver rules ctxt = solver_of (Context.Proof ctxt) ctxt rules
 in
diff -r 826a490f6482 -r 5bf9a3d5d4ff src/HOL/SMT/Tools/yices_solver.ML
--- a/src/HOL/SMT/Tools/yices_solver.ML	Fri Nov 06 16:59:17 2009 +0100
+++ b/src/HOL/SMT/Tools/yices_solver.ML	Fri Nov 06 19:02:36 2009 +0100
@@ -32,7 +32,7 @@
   end
 
 fun smtlib_solver oracle _ = {
-  command = {env_var=env_var, remote_name=solver_name},
+  command = {env_var=env_var, remote_name=NONE},
   arguments = options,
   interface = SMTLIB_Interface.interface,
   reconstruct = oracle }
diff -r 826a490f6482 -r 5bf9a3d5d4ff src/HOL/SMT/Tools/z3_solver.ML
--- a/src/HOL/SMT/Tools/z3_solver.ML	Fri Nov 06 16:59:17 2009 +0100
+++ b/src/HOL/SMT/Tools/z3_solver.ML	Fri Nov 06 19:02:36 2009 +0100
@@ -66,7 +66,7 @@
 fun solver oracle ctxt =
   let val with_proof = Config.get ctxt proofs
   in
-    {command = {env_var=env_var, remote_name=solver_name},
+    {command = {env_var=env_var, remote_name=SOME solver_name},
     arguments = cmdline_options ctxt,
     interface = Z3_Interface.interface,
     reconstruct = if with_proof then prover else oracle}
diff -r 826a490f6482 -r 5bf9a3d5d4ff src/HOL/SMT/lib/scripts/remote_smt.pl
--- a/src/HOL/SMT/lib/scripts/remote_smt.pl	Fri Nov 06 16:59:17 2009 +0100
+++ b/src/HOL/SMT/lib/scripts/remote_smt.pl	Fri Nov 06 19:02:36 2009 +0100
@@ -8,17 +8,12 @@
 use LWP;
 
 
-# environment
-
-my $remote_smt_url = $ENV{"REMOTE_SMT_URL"};
-
-
 # arguments
 
-my $solver = $ARGV[0];
-my @options = @ARGV[1 .. ($#ARGV - 2)];
-my $problem_file = $ARGV[-2];
-my $output_file = $ARGV[-1];
+my $url = $ARGV[0];
+my $solver = $ARGV[1];
+my @options = @ARGV[2 .. ($#ARGV - 1)];
+my $problem_file = $ARGV[-1];
 
 
 # call solver
@@ -26,7 +21,7 @@
 my $agent = LWP::UserAgent->new;
 $agent->agent("SMT-Request");
 $agent->timeout(180);
-my $response = $agent->post($remote_smt_url, [
+my $response = $agent->post($url, [
   "Solver" => $solver,
   "Options" => join(" ", @options),
   "Problem" => [$problem_file] ],
@@ -36,8 +31,6 @@
   exit 1;
 }
 else {
-  open(FILE, ">$output_file");
-  print FILE $response->content;
-  close(FILE);
+  print $response->content;
+  exit 0;
 }
-