--- 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
--- 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 {*
--- 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
--- 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 }
--- 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
--- 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 }
--- 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}
--- 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;
}
-