# HG changeset patch # User boehmes # Date 1265130641 -3600 # Node ID e5cb3a0160942eea7ed62a0c9af58248ff02f099 # Parent 7b8c366e34a25b7f97e224049d09bccc0cc96578 collect certificates in a single file diff -r 7b8c366e34a2 -r e5cb3a016094 src/HOL/SMT/SMT.thy --- 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 diff -r 7b8c366e34a2 -r e5cb3a016094 src/HOL/SMT/Tools/smt_solver.ML --- 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) diff -r 7b8c366e34a2 -r e5cb3a016094 src/HOL/SMT/etc/settings --- 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: # diff -r 7b8c366e34a2 -r e5cb3a016094 src/HOL/SMT/lib/scripts/cert_smt.pl --- 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 () { - print $_; - } - close FILE; - } - else { print "ERROR: unable to open proof file\n"; } -} -else { print "ERROR: bad problem\n"; } diff -r 7b8c366e34a2 -r e5cb3a016094 src/HOL/SMT/lib/scripts/remote_smt.pl --- 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; -} diff -r 7b8c366e34a2 -r e5cb3a016094 src/HOL/SMT/lib/scripts/run_smt_solver.pl --- /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 () { + 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 = ; + 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 () { print CERTS $_; } + close FILE; + + print CERTS "\n"; + close CERTS; +} +