1.1 --- a/etc/components Tue Feb 16 15:16:33 2010 +0100
1.2 +++ b/etc/components Tue Feb 16 15:25:36 2010 +0100
1.3 @@ -13,6 +13,7 @@
1.4 #misc components
1.5 src/Tools/Code
1.6 src/Tools/WWW_Find
1.7 +src/Tools/Cache_IO
1.8 src/HOL/Tools/ATP_Manager
1.9 src/HOL/Mirabelle
1.10 src/HOL/Library/Sum_Of_Squares
2.1 --- a/src/HOL/IsaMakefile Tue Feb 16 15:16:33 2010 +0100
2.2 +++ b/src/HOL/IsaMakefile Tue Feb 16 15:25:36 2010 +0100
2.3 @@ -1226,7 +1226,8 @@
2.4 SMT/Tools/smt_solver.ML SMT/Tools/cvc3_solver.ML \
2.5 SMT/Tools/yices_solver.ML SMT/Tools/z3_proof_terms.ML \
2.6 SMT/Tools/z3_proof_rules.ML SMT/Tools/z3_proof.ML \
2.7 - SMT/Tools/z3_model.ML SMT/Tools/z3_interface.ML SMT/Tools/z3_solver.ML
2.8 + SMT/Tools/z3_model.ML SMT/Tools/z3_interface.ML \
2.9 + SMT/Tools/z3_solver.ML $(SRC)/Tools/Cache_IO/cache_io.ML
2.10 @cd SMT; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL-Word HOL-SMT
2.11
2.12
3.1 --- a/src/HOL/SMT/SMT_Base.thy Tue Feb 16 15:16:33 2010 +0100
3.2 +++ b/src/HOL/SMT/SMT_Base.thy Tue Feb 16 15:25:36 2010 +0100
3.3 @@ -8,6 +8,7 @@
3.4 imports Real "~~/src/HOL/Word/Word"
3.5 "~~/src/HOL/Decision_Procs/Dense_Linear_Order"
3.6 uses
3.7 + "~~/src/Tools/Cache_IO/cache_io.ML"
3.8 ("Tools/smt_normalize.ML")
3.9 ("Tools/smt_monomorph.ML")
3.10 ("Tools/smt_translate.ML")
4.1 --- a/src/HOL/SMT/Tools/smt_solver.ML Tue Feb 16 15:16:33 2010 +0100
4.2 +++ b/src/HOL/SMT/Tools/smt_solver.ML Tue Feb 16 15:25:36 2010 +0100
4.3 @@ -28,8 +28,10 @@
4.4 val with_timeout: Proof.context -> ('a -> 'b) -> 'a -> 'b
4.5 val trace: bool Config.T
4.6 val trace_msg: Proof.context -> ('a -> string) -> 'a -> unit
4.7 +
4.8 + (*certificates*)
4.9 val record: bool Config.T
4.10 - val certificates: string Config.T
4.11 + val select_certificates: string -> Context.generic -> Context.generic
4.12
4.13 (*solvers*)
4.14 type solver = Proof.context -> thm list -> thm
4.15 @@ -88,30 +90,29 @@
4.16 fun trace_msg ctxt f x =
4.17 if Config.get ctxt trace then tracing (f x) else ()
4.18
4.19 +
4.20 +(* SMT certificates *)
4.21 +
4.22 val (record, setup_record) = Attrib.config_bool "smt_record" true
4.23 -val no_certificates = ""
4.24 -val (certificates, setup_certificates) =
4.25 - Attrib.config_string "smt_certificates" no_certificates
4.26
4.27 +structure Certificates = Generic_Data
4.28 +(
4.29 + type T = Cache_IO.cache option
4.30 + val empty = NONE
4.31 + val extend = I
4.32 + fun merge (s, _) = s
4.33 +)
4.34 +
4.35 +fun select_certificates name = Certificates.put (
4.36 + if name = "" then NONE
4.37 + else SOME (Cache_IO.make (Path.explode name)))
4.38
4.39
4.40 (* interface to external solvers *)
4.41
4.42 local
4.43
4.44 -fun with_files ctxt f =
4.45 - let
4.46 - val paths as (problem_path, proof_path) =
4.47 - "smt-" ^ serial_string ()
4.48 - |> (fn n => (n, n ^ ".proof"))
4.49 - |> pairself (File.tmp_path o Path.explode)
4.50 -
4.51 - val y = Exn.capture f (problem_path, proof_path)
4.52 -
4.53 - val _ = pairself (try File.rm) paths
4.54 - in Exn.release y end
4.55 -
4.56 -fun invoke ctxt output f (paths as (problem_path, proof_path)) =
4.57 +fun invoke ctxt output f problem_path =
4.58 let
4.59 fun pretty tag ls = Pretty.string_of (Pretty.big_list tag
4.60 (map Pretty.str ls))
4.61 @@ -120,11 +121,10 @@
4.62 val _ = trace_msg ctxt (pretty "SMT problem:" o split_lines o File.read)
4.63 problem_path
4.64
4.65 - val (s, _) = with_timeout ctxt f paths
4.66 - val _ = trace_msg ctxt (pretty "SMT solver:") (split_lines s)
4.67 + val (res, err) = with_timeout ctxt f problem_path
4.68 + val _ = trace_msg ctxt (pretty "SMT solver:") err
4.69
4.70 - fun lines_of path = the_default [] (try (File.fold_lines cons path) [])
4.71 - val ls = rev (dropwhile (equal "") (lines_of proof_path))
4.72 + val ls = rev (dropwhile (equal "") (rev res))
4.73 val _ = trace_msg ctxt (pretty "SMT result:") ls
4.74 in (x, ls) end
4.75
4.76 @@ -135,37 +135,40 @@
4.77 val remote_url = getenv "REMOTE_SMT_URL"
4.78 in
4.79 if local_solver <> ""
4.80 - then (["local", local_solver],
4.81 - "Invoking local SMT solver " ^ quote local_solver ^ " ...")
4.82 - else if remote_solver <> "" andalso remote_url <> ""
4.83 - then (["remote", remote_solver],
4.84 - "Invoking remote SMT solver " ^ quote remote_solver ^ " at " ^
4.85 - quote remote_url ^ " ...")
4.86 + then
4.87 + (tracing ("Invoking local SMT solver " ^ quote local_solver ^ " ...");
4.88 + [local_solver])
4.89 + else if remote_solver <> ""
4.90 + then
4.91 + (tracing ("Invoking remote SMT solver " ^ quote remote_solver ^ " at " ^
4.92 + quote remote_url ^ " ...");
4.93 + [getenv "REMOTE_SMT", remote_solver])
4.94 else error ("Undefined Isabelle environment variable: " ^ quote env_var)
4.95 end
4.96
4.97 -fun run ctxt cmd args (problem_path, proof_path) =
4.98 - let
4.99 - val certs = Config.get ctxt certificates
4.100 - val certs' =
4.101 - if certs = no_certificates then "-"
4.102 - else File.shell_path (Path.explode certs)
4.103 - val (solver, msg) =
4.104 - if certs = no_certificates orelse Config.get ctxt record
4.105 - then choose cmd
4.106 - else (["certificate"], "Using certificate from " ^ quote certs' ^ " ...")
4.107 - val _ = tracing msg
4.108 +fun make_cmd solver args problem_path proof_path = space_implode " " (
4.109 + map File.shell_quote (solver @ args) @
4.110 + [File.shell_path problem_path, "2>&1", ">", File.shell_path proof_path])
4.111 +
4.112 +fun no_cmd _ _ = error ("Bad certificates cache: missing certificate")
4.113 +
4.114 +fun run ctxt cmd args problem_path =
4.115 + let val certs = Certificates.get (Context.Proof ctxt)
4.116 in
4.117 - bash_output (space_implode " " (
4.118 - File.shell_path (Path.explode (getenv "RUN_SMT_SOLVER")) :: certs' ::
4.119 - map File.shell_quote (solver @ args) @
4.120 - map File.shell_path [problem_path, proof_path]) ^ " 2>&1")
4.121 + if is_none certs
4.122 + then Cache_IO.run' (make_cmd (choose cmd) args) problem_path
4.123 + else if Config.get ctxt record
4.124 + then Cache_IO.cached' (the certs) (make_cmd (choose cmd) args) problem_path
4.125 + else
4.126 + (tracing ("Using cached certificate from " ^
4.127 + File.shell_path (Cache_IO.cache_path_of (the certs)) ^ " ...");
4.128 + Cache_IO.cached' (the certs) no_cmd problem_path)
4.129 end
4.130
4.131 in
4.132
4.133 fun run_solver ctxt cmd args output =
4.134 - with_files ctxt (invoke ctxt output (run ctxt cmd args))
4.135 + Cache_IO.with_tmp_file "smt-" (invoke ctxt output (run ctxt cmd args))
4.136
4.137 end
4.138
4.139 @@ -278,7 +281,10 @@
4.140 setup_timeout #>
4.141 setup_trace #>
4.142 setup_record #>
4.143 - setup_certificates #>
4.144 + Attrib.setup (Binding.name "smt_certificates")
4.145 + (Scan.lift (OuterParse.$$$ "=" |-- Args.name) >>
4.146 + (Thm.declaration_attribute o K o select_certificates))
4.147 + "SMT certificates" #>
4.148 Method.setup (Binding.name "smt") smt_method
4.149 "Applies an SMT solver to the current goal."
4.150
5.1 --- a/src/HOL/SMT/lib/scripts/run_smt_solver Tue Feb 16 15:16:33 2010 +0100
5.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
5.3 @@ -1,93 +0,0 @@
5.4 -#!/usr/bin/env perl
5.5 -#
5.6 -# Author: Sascha Boehme, TU Muenchen
5.7 -#
5.8 -# Cache for prover results, based on discriminating problems using MD5.
5.9 -
5.10 -use strict;
5.11 -use warnings;
5.12 -use Digest::MD5;
5.13 -
5.14 -
5.15 -# arguments
5.16 -
5.17 -my $certs_file = shift @ARGV;
5.18 -my $location = shift @ARGV;
5.19 -my $result_file = pop @ARGV;
5.20 -my $problem_file = $ARGV[-1];
5.21 -
5.22 -my $use_certs = not ($certs_file eq "-");
5.23 -
5.24 -
5.25 -# create MD5 problem digest
5.26 -
5.27 -my $problem_digest = "";
5.28 -if ($use_certs) {
5.29 - my $md5 = Digest::MD5->new;
5.30 - open FILE, "<$problem_file" or
5.31 - die "ERROR: Failed to open '$problem_file' ($!)";
5.32 - $md5->addfile(*FILE);
5.33 - close FILE;
5.34 - $problem_digest = $md5->b64digest;
5.35 -}
5.36 -
5.37 -
5.38 -# lookup problem digest among existing certificates and
5.39 -# return a cached result (if there is a certificate for the problem)
5.40 -
5.41 -if ($use_certs and -e $certs_file) {
5.42 - my $cached = 0;
5.43 - open CERTS, "<$certs_file" or die "ERROR: Failed to open '$certs_file' ($!)";
5.44 - while (<CERTS>) {
5.45 - if (m/(\S+) (\d+)/) {
5.46 - if ($1 eq $problem_digest) {
5.47 - my $start = tell CERTS;
5.48 - open FILE, ">$result_file" or
5.49 - die "ERROR: Failed to open '$result_file ($!)";
5.50 - while ((tell CERTS) - $start < $2) {
5.51 - my $line = <CERTS>;
5.52 - print FILE $line;
5.53 - }
5.54 - close FILE;
5.55 - $cached = 1;
5.56 - last;
5.57 - }
5.58 - else { seek CERTS, $2, 1; }
5.59 - }
5.60 - else { die "ERROR: Invalid file format in '$certs_file'"; }
5.61 - }
5.62 - close CERTS;
5.63 - if ($cached) { exit 0; }
5.64 -}
5.65 -
5.66 -
5.67 -# invoke (remote or local) prover
5.68 -
5.69 -my $result;
5.70 -
5.71 -if ($location eq "remote") {
5.72 - $result = system "$ENV{'REMOTE_SMT'} @ARGV >$result_file 2>&1";
5.73 -}
5.74 -elsif ($location eq "local") {
5.75 - $result = system "@ARGV >$result_file 2>&1";
5.76 -}
5.77 -else { die "ERROR: No SMT solver invoked"; }
5.78 -
5.79 -
5.80 -# cache result
5.81 -
5.82 -if ($use_certs) {
5.83 - open CERTS, ">>$certs_file" or
5.84 - die "ERROR: Failed to open '$certs_file' ($!)";
5.85 - print CERTS
5.86 - ("$problem_digest " . ((-s $result_file) + (length "\n")) . "\n");
5.87 -
5.88 - open FILE, "<$result_file" or
5.89 - die "ERROR: Failed to open '$result_file' ($!)";
5.90 - foreach (<FILE>) { print CERTS $_; }
5.91 - close FILE;
5.92 -
5.93 - print CERTS "\n";
5.94 - close CERTS;
5.95 -}
5.96 -
6.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
6.2 +++ b/src/Tools/Cache_IO/cache_io.ML Tue Feb 16 15:25:36 2010 +0100
6.3 @@ -0,0 +1,121 @@
6.4 +(* Title: Tools/Cache_IO/cache_io.ML
6.5 + Author: Sascha Boehme, TU Muenchen
6.6 +
6.7 +Cache for output of external processes.
6.8 +*)
6.9 +
6.10 +signature CACHE_IO =
6.11 +sig
6.12 + val with_tmp_file: string -> (Path.T -> 'a) -> 'a
6.13 + val run: (Path.T -> string) -> Path.T -> string list
6.14 + val run': (Path.T -> Path.T -> string) -> Path.T -> string list * string list
6.15 +
6.16 + type cache
6.17 + val make: Path.T -> cache
6.18 + val cache_path_of: cache -> Path.T
6.19 + val cached: cache -> (Path.T -> string) -> Path.T -> string list
6.20 + val cached': cache -> (Path.T -> Path.T -> string) -> Path.T ->
6.21 + string list * string list
6.22 +end
6.23 +
6.24 +structure Cache_IO : CACHE_IO =
6.25 +struct
6.26 +
6.27 +fun with_tmp_file name f =
6.28 + let
6.29 + val path = File.tmp_path (Path.explode (name ^ serial_string ()))
6.30 + val x = Exn.capture f path
6.31 + val _ = try File.rm path
6.32 + in Exn.release x end
6.33 +
6.34 +fun run' make_cmd in_path =
6.35 + with_tmp_file "cache-io-" (fn out_path =>
6.36 + let
6.37 + val (out2, _) = bash_output (make_cmd in_path out_path)
6.38 + val out1 = the_default [] (try (rev o File.fold_lines cons out_path) [])
6.39 + in (out1, split_lines out2) end)
6.40 +
6.41 +fun run make_cmd = snd o run' (fn in_path => fn _ => make_cmd in_path)
6.42 +
6.43 +
6.44 +
6.45 +abstype cache = Cache of {
6.46 + path: Path.T,
6.47 + table: (int * (int * int * int) Symtab.table) Synchronized.var }
6.48 +with
6.49 +
6.50 +
6.51 +fun cache_path_of (Cache {path, ...}) = path
6.52 +
6.53 +
6.54 +fun load cache_path =
6.55 + let
6.56 + fun err () = error ("Cache IO: corrupted cache file: " ^
6.57 + File.shell_path cache_path)
6.58 +
6.59 + fun int_of_string s =
6.60 + (case read_int (explode s) of
6.61 + (i, []) => i
6.62 + | _ => err ())
6.63 +
6.64 + fun split line =
6.65 + (case space_explode " " line of
6.66 + [key, len1, len2] => (key, int_of_string len1, int_of_string len2)
6.67 + | _ => err ())
6.68 +
6.69 + fun parse line ((i, l), tab) =
6.70 + if i = l
6.71 + then
6.72 + let val (key, l1, l2) = split line
6.73 + in ((i+1, l+l1+l2+1), Symtab.update (key, (i+1, l1, l2)) tab) end
6.74 + else ((i+1, l), tab)
6.75 + in apfst fst (File.fold_lines parse cache_path ((1, 1), Symtab.empty)) end
6.76 +
6.77 +fun make path =
6.78 + let val table = if File.exists path then load path else (1, Symtab.empty)
6.79 + in Cache {path=path, table=Synchronized.var (Path.implode path) table} end
6.80 +
6.81 +
6.82 +fun get_hash_key path =
6.83 + let
6.84 + val arg = File.shell_path path
6.85 + val (out, res) = bash_output (getenv "COMPUTE_HASH_KEY" ^ " " ^ arg)
6.86 + in
6.87 + if res = 0 then hd (split_lines out)
6.88 + else error ("Cache IO: failed to generate hash key for file " ^ arg)
6.89 + end
6.90 +
6.91 +fun load_cached_result cache_path (p, len1, len2) =
6.92 + let
6.93 + fun load line (i, xsp) =
6.94 + if i < p then (i+1, xsp)
6.95 + else if i < p + len1 then (i+1, apfst (cons line) xsp)
6.96 + else if i < p + len2 then (i+1, apsnd (cons line) xsp)
6.97 + else (i, xsp)
6.98 + in pairself rev (snd (File.fold_lines load cache_path (1, ([], [])))) end
6.99 +
6.100 +fun cached' (Cache {path=cache_path, table}) make_cmd in_path =
6.101 + let val key = get_hash_key in_path
6.102 + in
6.103 + (case Symtab.lookup (snd (Synchronized.value table)) key of
6.104 + SOME pos => load_cached_result cache_path pos
6.105 + | NONE =>
6.106 + let
6.107 + val res as (out, err) = run' make_cmd in_path
6.108 + val (l1, l2) = pairself length res
6.109 + val header = key ^ " " ^ string_of_int l1 ^ " " ^ string_of_int l2
6.110 + val lines = map (suffix "\n") (header :: out @ err)
6.111 +
6.112 + val _ = Synchronized.change table (fn (p, tab) =>
6.113 + if Symtab.defined tab key then (p, tab)
6.114 + else
6.115 + let val _ = File.append_list cache_path lines
6.116 + in (p+l1+l2+1, Symtab.update (key, (p+1, l1, l2)) tab) end)
6.117 + in res end)
6.118 + end
6.119 +
6.120 +fun cached cache make_cmd =
6.121 + snd o cached' cache (fn in_path => fn _ => make_cmd in_path)
6.122 +
6.123 +end
6.124 +end
7.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
7.2 +++ b/src/Tools/Cache_IO/etc/settings Tue Feb 16 15:25:36 2010 +0100
7.3 @@ -0,0 +1,4 @@
7.4 +ISABELLE_CACHE_IO="$COMPONENT"
7.5 +
7.6 +COMPUTE_HASH_KEY="$ISABELLE_CACHE_IO/lib/scripts/compute_hash_key"
7.7 +
8.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
8.2 +++ b/src/Tools/Cache_IO/lib/scripts/compute_hash_key Tue Feb 16 15:25:36 2010 +0100
8.3 @@ -0,0 +1,24 @@
8.4 +#!/usr/bin/env perl
8.5 +#
8.6 +# Author: Sascha Boehme, TU Muenchen
8.7 +#
8.8 +# Compute MD5 hash key.
8.9 +
8.10 +use strict;
8.11 +use warnings;
8.12 +use Digest::MD5;
8.13 +
8.14 +
8.15 +# argument
8.16 +
8.17 +my $file = $ARGV[0];
8.18 +
8.19 +
8.20 +# compute MD5 hash key
8.21 +
8.22 +my $md5 = Digest::MD5->new;
8.23 +open FILE, "<$file" or die "ERROR: Failed to open '$file' ($!)";
8.24 +$md5->addfile(*FILE);
8.25 +close FILE;
8.26 +print $md5->b64digest . "\n";
8.27 +