--- a/src/HOL/SMT/SMT.thy Tue Feb 02 11:38:38 2010 +0100
+++ b/src/HOL/SMT/SMT.thy Tue Feb 02 18:10:41 2010 +0100
@@ -39,20 +39,39 @@
subsection {* Z3-specific options *}
+text {* Pass extra command-line arguments to Z3 to control its behaviour: *}
+
+declare [[ z3_options = "" ]]
+
text {* Enable proof reconstruction for Z3: *}
declare [[ z3_proofs = false ]]
-text {* Pass extra command-line arguments to Z3
-to control its behaviour: *}
+text {* Enable or disable tracing of the theorems used for proving a
+proposition: *}
+
+declare [[ z3_trace_assms = false ]]
+
+
+subsection {* Certificates *}
-declare [[ z3_options = "" ]]
+text {* To avoid invocation of an SMT solver for the same problem
+again and again, cache certificates in a file (the filename must
+be given by an absolute path, an empty string disables the usage
+of certificates): *}
+
+declare [[ smt_certificates = "" ]]
+
+text {* Enables or disables the addition of new certificates to
+the current certificates file (when disabled, only existing
+certificates are used and no SMT solver is invoked): *}
+
+declare [[ smt_record = true ]]
subsection {* Special configuration options *}
-text {*
-Trace the problem file, the result of the SMT solver and
+text {* Trace the problem file, the result of the SMT solver and
further information: *}
declare [[ smt_trace = false ]]
@@ -61,11 +80,4 @@
declare [[ smt_unfold_defs = true ]]
-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/smt_solver.ML Tue Feb 02 11:38:38 2010 +0100
+++ b/src/HOL/SMT/Tools/smt_solver.ML Tue Feb 02 18:10:41 2010 +0100
@@ -28,8 +28,8 @@
val with_timeout: Proof.context -> ('a -> 'b) -> 'a -> 'b
val trace: bool Config.T
val trace_msg: Proof.context -> ('a -> string) -> 'a -> unit
- val keep: string Config.T
- val cert: string Config.T
+ val record: bool Config.T
+ val certificates: string Config.T
(*solvers*)
type solver = Proof.context -> thm list -> thm
@@ -88,8 +88,11 @@
fun trace_msg ctxt f x =
if Config.get ctxt trace then tracing (f x) else ()
-val (keep, setup_keep) = Attrib.config_string "smt_keep" ""
-val (cert, setup_cert) = Attrib.config_string "smt_cert" ""
+val (record, setup_record) = Attrib.config_bool "smt_record" true
+val no_certificates = ""
+val (certificates, setup_certificates) =
+ Attrib.config_string "smt_certificates" no_certificates
+
(* interface to external solvers *)
@@ -98,18 +101,14 @@
fun with_files ctxt f =
let
- fun make_names n = (n, n ^ ".proof")
-
- val keep' = Config.get ctxt keep
val paths as (problem_path, proof_path) =
- if keep' <> "" andalso File.exists (Path.dir (Path.explode keep'))
- then pairself Path.explode (make_names keep')
- else pairself (File.tmp_path o Path.explode)
- (make_names ("smt-" ^ serial_string ()))
+ "smt-" ^ serial_string ()
+ |> (fn n => (n, n ^ ".proof"))
+ |> pairself (File.tmp_path o Path.explode)
val y = Exn.capture f (problem_path, proof_path)
- val _ = if keep' = "" then (pairself (try File.rm) paths; ()) else ()
+ val _ = pairself (try File.rm) paths
in Exn.release y end
fun invoke ctxt output f (paths as (problem_path, proof_path)) =
@@ -121,59 +120,46 @@
val _ = trace_msg ctxt (pretty "SMT problem:" o split_lines o File.read)
problem_path
- val _ = with_timeout ctxt f paths
+ val (s, _) = with_timeout ctxt f paths
+ val _ = trace_msg ctxt (pretty "SMT solver:") (split_lines s)
+
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
+fun choose {env_var, remote_name} =
+ let
+ val local_solver = getenv env_var
+ val remote_solver = the_default "" remote_name
+ val remote_url = getenv "REMOTE_SMT_URL"
in
- if name = "" then false
- else
- (tracing ("Using certificate " ^ quote (expand_name name) ^ " ...");
- run_perl "CERT_SMT_SOLVER" [expand_name name] ps;
- true)
+ if local_solver <> ""
+ then (["local", local_solver],
+ "Invoking local SMT solver " ^ quote local_solver ^ " ...")
+ else if remote_solver <> "" andalso remote_url <> ""
+ then (["remote", remote_solver],
+ "Invoking remote SMT solver " ^ quote remote_solver ^ " at " ^
+ quote remote_url ^ " ...")
+ else error ("Undefined Isabelle environment variable: " ^ quote env_var)
end
-fun run_locally f 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]
+fun run ctxt cmd args (problem_path, proof_path) =
+ let
+ val certs = Config.get ctxt certificates
+ val certs' =
+ if certs = no_certificates then "-"
+ else File.shell_path (Path.explode certs)
+ val (solver, msg) =
+ if certs = no_certificates orelse Config.get ctxt record
+ then choose cmd
+ else (["certificate"], "Using certificate from " ^ quote certs' ^ " ...")
+ val _ = tracing msg
in
- if use_certificate ctxt ps then ()
- else run_locally (run_remote remote_name args ps) env_var args ps
+ system_out (space_implode " " ("perl -w" ::
+ File.shell_path (Path.explode (getenv "RUN_SMT_SOLVER")) :: certs' ::
+ map File.shell_quote (solver @ args) @
+ map File.shell_path [problem_path, proof_path]))
end
in
@@ -291,11 +277,12 @@
"SMT solver configuration" #>
setup_timeout #>
setup_trace #>
- setup_keep #>
- setup_cert #>
+ setup_record #>
+ setup_certificates #>
Method.setup (Binding.name "smt") smt_method
"Applies an SMT solver to the current goal."
+
fun print_setup gen =
let
val t = string_of_int (Config.get_generic gen timeout)
--- a/src/HOL/SMT/etc/settings Tue Feb 02 11:38:38 2010 +0100
+++ b/src/HOL/SMT/etc/settings Tue Feb 02 18:10:41 2010 +0100
@@ -1,11 +1,9 @@
ISABELLE_SMT="$COMPONENT"
-REMOTE_SMT_SOLVER="$ISABELLE_SMT/lib/scripts/remote_smt.pl"
+RUN_SMT_SOLVER="$ISABELLE_SMT/lib/scripts/run_smt_solver.pl"
REMOTE_SMT_URL="http://smt.in.tum.de/smt"
-CERT_SMT_SOLVER="$ISABELLE_SMT/lib/scripts/cert_smt.pl"
-
#
# Paths to local SMT solvers:
#
--- a/src/HOL/SMT/lib/scripts/cert_smt.pl Tue Feb 02 11:38:38 2010 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,33 +0,0 @@
-#
-# Author: Sascha Boehme, TU Muenchen
-#
-# Fake SMT solver: check that input matches previously computed input and
-# and return previously computed output.
-#
-
-use strict;
-use File::Compare;
-
-
-# arguments
-
-my $cert_path = $ARGV[0];
-my $new_problem = $ARGV[1];
-
-
-# check content of new problem file against old problem file
-
-my $old_problem = $cert_path;
-my $old_proof = $cert_path . ".proof";
-
-if (-e $old_problem and compare($old_problem, $new_problem) == 0) {
- if (-e $old_proof) {
- open FILE, "<$old_proof";
- foreach (<FILE>) {
- print $_;
- }
- close FILE;
- }
- else { print "ERROR: unable to open proof file\n"; }
-}
-else { print "ERROR: bad problem\n"; }
--- a/src/HOL/SMT/lib/scripts/remote_smt.pl Tue Feb 02 11:38:38 2010 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,36 +0,0 @@
-#
-# Author: Sascha Boehme, TU Muenchen
-#
-# Invoke remote SMT solvers.
-#
-
-use strict;
-use LWP;
-
-
-# arguments
-
-my $url = $ARGV[0];
-my $solver = $ARGV[1];
-my @options = @ARGV[2 .. ($#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($url, [
- "Solver" => $solver,
- "Options" => join(" ", @options),
- "Problem" => [$problem_file] ],
- "Content_Type" => "form-data");
-if (not $response->is_success) {
- print "HTTP-Error: " . $response->message . "\n";
- exit 1;
-}
-else {
- print $response->content;
- exit 0;
-}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/SMT/lib/scripts/run_smt_solver.pl Tue Feb 02 18:10:41 2010 +0100
@@ -0,0 +1,110 @@
+#
+# 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;
+}
+