# HG changeset patch
# User boehmes
# Date 1257526377 -3600
# Node ID e88f67d679c47173962eeb07e072d04cb6e488e5
# Parent  5aef13872723de5ff622798ad0a148f3858d003c
added documentation for local SMT solver setup and available SMT options,
added verbose output for SMT solver invocation,
test if local SMT solver exists before invoking it,
always trace (possible) counterexamples,
documented existence of SMT server

diff -r 5aef13872723 -r e88f67d679c4 NEWS
--- a/NEWS	Fri Nov 06 14:42:42 2009 +0100
+++ b/NEWS	Fri Nov 06 17:52:57 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 5aef13872723 -r e88f67d679c4 src/HOL/SMT/Examples/SMT_Examples.thy
--- a/src/HOL/SMT/Examples/SMT_Examples.thy	Fri Nov 06 14:42:42 2009 +0100
+++ b/src/HOL/SMT/Examples/SMT_Examples.thy	Fri Nov 06 17:52:57 2009 +0100
@@ -549,7 +549,7 @@
 
 section {* Bitvectors *}
 
-locale bv
+locale z3_bv_test
 begin
 
 text {*
diff -r 5aef13872723 -r e88f67d679c4 src/HOL/SMT/SMT.thy
--- a/src/HOL/SMT/SMT.thy	Fri Nov 06 14:42:42 2009 +0100
+++ b/src/HOL/SMT/SMT.thy	Fri Nov 06 17:52:57 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 5aef13872723 -r e88f67d679c4 src/HOL/SMT/Tools/cvc3_solver.ML
--- a/src/HOL/SMT/Tools/cvc3_solver.ML	Fri Nov 06 14:42:42 2009 +0100
+++ b/src/HOL/SMT/Tools/cvc3_solver.ML	Fri Nov 06 17:52:57 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 5aef13872723 -r e88f67d679c4 src/HOL/SMT/Tools/smt_solver.ML
--- a/src/HOL/SMT/Tools/smt_solver.ML	Fri Nov 06 14:42:42 2009 +0100
+++ b/src/HOL/SMT/Tools/smt_solver.ML	Fri Nov 06 17:52:57 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 5aef13872723 -r e88f67d679c4 src/HOL/SMT/Tools/yices_solver.ML
--- a/src/HOL/SMT/Tools/yices_solver.ML	Fri Nov 06 14:42:42 2009 +0100
+++ b/src/HOL/SMT/Tools/yices_solver.ML	Fri Nov 06 17:52:57 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 5aef13872723 -r e88f67d679c4 src/HOL/SMT/Tools/z3_solver.ML
--- a/src/HOL/SMT/Tools/z3_solver.ML	Fri Nov 06 14:42:42 2009 +0100
+++ b/src/HOL/SMT/Tools/z3_solver.ML	Fri Nov 06 17:52:57 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 5aef13872723 -r e88f67d679c4 src/HOL/SMT/lib/scripts/remote_smt.pl
--- a/src/HOL/SMT/lib/scripts/remote_smt.pl	Fri Nov 06 14:42:42 2009 +0100
+++ b/src/HOL/SMT/lib/scripts/remote_smt.pl	Fri Nov 06 17:52:57 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;
 }
-