Merged.
--- a/src/HOL/Boogie/Examples/Boogie_Dijkstra.thy Wed Apr 07 19:17:10 2010 +0200
+++ b/src/HOL/Boogie/Examples/Boogie_Dijkstra.thy Wed Apr 07 22:22:49 2010 +0200
@@ -82,7 +82,7 @@
boogie_open "~~/src/HOL/Boogie/Examples/Boogie_Dijkstra"
declare [[smt_certificates="~~/src/HOL/Boogie/Examples/Boogie_Dijkstra.certs"]]
-declare [[smt_record=false]]
+declare [[smt_fixed=true]]
boogie_vc Dijkstra
using [[z3_proofs=true]]
--- a/src/HOL/Boogie/Examples/Boogie_Max.thy Wed Apr 07 19:17:10 2010 +0200
+++ b/src/HOL/Boogie/Examples/Boogie_Max.thy Wed Apr 07 22:22:49 2010 +0200
@@ -39,7 +39,7 @@
boogie_open "~~/src/HOL/Boogie/Examples/Boogie_Max"
declare [[smt_certificates="~~/src/HOL/Boogie/Examples/Boogie_Max.certs"]]
-declare [[smt_record=false]]
+declare [[smt_fixed=true]]
boogie_vc max
using [[z3_proofs=true]]
--- a/src/HOL/Boogie/Examples/VCC_Max.thy Wed Apr 07 19:17:10 2010 +0200
+++ b/src/HOL/Boogie/Examples/VCC_Max.thy Wed Apr 07 22:22:49 2010 +0200
@@ -47,7 +47,7 @@
boogie_open (quiet) "~~/src/HOL/Boogie/Examples/VCC_Max"
declare [[smt_certificates="~~/src/HOL/Boogie/Examples/VCC_Max.certs"]]
-declare [[smt_record=false]]
+declare [[smt_fixed=true]]
boogie_status
--- a/src/HOL/Multivariate_Analysis/Integration.thy Wed Apr 07 19:17:10 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/Integration.thy Wed Apr 07 22:22:49 2010 +0200
@@ -8,7 +8,7 @@
begin
declare [[smt_certificates="~~/src/HOL/Multivariate_Analysis/Integration.cert"]]
-declare [[smt_record=false]]
+declare [[smt_fixed=true]]
declare [[z3_proofs=true]]
lemma conjunctD2: assumes "a \<and> b" shows a b using assms by auto
--- a/src/HOL/SMT/Examples/SMT_Examples.thy Wed Apr 07 19:17:10 2010 +0200
+++ b/src/HOL/SMT/Examples/SMT_Examples.thy Wed Apr 07 22:22:49 2010 +0200
@@ -17,7 +17,7 @@
the following option is set to "false":
*}
-declare [[smt_record=false]]
+declare [[smt_fixed=true]]
@@ -539,7 +539,8 @@
lemma "i \<noteq> i1 \<and> i \<noteq> i2 \<Longrightarrow> (f (i1 := v1, i2 := v2)) i = f i" by smt
-lemma "(f g x = (g x \<and> True)) \<or> (f g x = True) \<or> (g x = True)" by smt
+lemma "(f g (x::'a::type) = (g x \<and> True)) \<or> (f g x = True) \<or> (g x = True)"
+ by smt
lemma "id 3 = 3 \<and> id True = True" by (smt id_def)
--- a/src/HOL/SMT/SMT.thy Wed Apr 07 19:17:10 2010 +0200
+++ b/src/HOL/SMT/SMT.thy Wed Apr 07 22:22:49 2010 +0200
@@ -62,11 +62,11 @@
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): *}
+text {* Allows or disallows the addition of new certificates to
+the current certificates file (when set to @{text false}, only
+existing certificates are used and no SMT solver is invoked): *}
-declare [[ smt_record = true ]]
+declare [[ smt_fixed = false ]]
subsection {* Special configuration options *}
@@ -76,8 +76,4 @@
declare [[ smt_trace = false ]]
-text {* Unfold (some) definitions passed to the SMT solver: *}
-
-declare [[ smt_unfold_defs = true ]]
-
end
--- a/src/HOL/SMT/SMT_Base.thy Wed Apr 07 19:17:10 2010 +0200
+++ b/src/HOL/SMT/SMT_Base.thy Wed Apr 07 22:22:49 2010 +0200
@@ -138,6 +138,6 @@
use "Tools/smt_solver.ML"
use "Tools/smtlib_interface.ML"
-setup {* SMT_Normalize.setup #> SMT_Solver.setup *}
+setup {* SMT_Solver.setup *}
end
--- a/src/HOL/SMT/Tools/smt_normalize.ML Wed Apr 07 19:17:10 2010 +0200
+++ b/src/HOL/SMT/Tools/smt_normalize.ML Wed Apr 07 22:22:49 2010 +0200
@@ -13,35 +13,19 @@
signature SMT_NORMALIZE =
sig
- val normalize_rule: Proof.context -> thm -> thm
val instantiate_free: cterm * cterm -> thm -> thm
val discharge_definition: cterm -> thm -> thm
- val trivial_let: Proof.context -> thm list -> thm list
- val positive_numerals: Proof.context -> thm list -> thm list
- val nat_as_int: Proof.context -> thm list -> thm list
- val unfold_defs: bool Config.T
- val add_pair_rules: Proof.context -> thm list -> thm list
- val add_fun_upd_rules: Proof.context -> thm list -> thm list
- val add_abs_min_max_rules: Proof.context -> thm list -> thm list
-
- datatype config =
- RewriteTrivialLets |
- RewriteNegativeNumerals |
- RewriteNaturalNumbers |
- AddPairRules |
- AddFunUpdRules |
- AddAbsMinMaxRules
-
- val normalize: config list -> Proof.context -> thm list ->
- cterm list * thm list
-
- val setup: theory -> theory
+ val normalize: Proof.context -> thm list -> cterm list * thm list
end
structure SMT_Normalize: SMT_NORMALIZE =
struct
+infix 2 ??
+fun (test ?? f) x = if test x then f x else x
+
+
local
val all1 = @{lemma "All P == ALL x. P x" by (rule reflexive)}
val all2 = @{lemma "All == (%P. ALL x. P x)" by (rule reflexive)}
@@ -133,7 +117,6 @@
fun normalize_rule ctxt =
Conv.fconv_rule (
- unfold_quants_conv ctxt then_conv
Thm.beta_conversion true then_conv
Thm.eta_conversion then_conv
norm_binder_conv ctxt) #>
@@ -141,10 +124,9 @@
Drule.forall_intr_vars #>
Conv.fconv_rule (atomize_conv ctxt)
-fun instantiate_free (cv, ct) thm =
- if Term.exists_subterm (equal (Thm.term_of cv)) (Thm.prop_of thm)
- then Thm.forall_elim ct (Thm.forall_intr cv thm)
- else thm
+fun instantiate_free (cv, ct) =
+ (Term.exists_subterm (equal (Thm.term_of cv)) o Thm.prop_of) ??
+ (Thm.forall_elim ct o Thm.forall_intr cv)
fun discharge_definition ct thm =
let val (cv, cu) = Thm.dest_equals ct
@@ -172,11 +154,10 @@
| is_trivial_let _ = false
fun let_conv _ = if_true_conv is_trivial_let (Conv.rewr_conv @{thm Let_def})
-
- fun cond_let_conv ctxt = if_true_conv (Term.exists_subterm is_trivial_let)
- (More_Conv.top_conv let_conv ctxt)
in
-fun trivial_let ctxt = map (Conv.fconv_rule (cond_let_conv ctxt))
+fun trivial_let ctxt =
+ map ((Term.exists_subterm is_trivial_let o Thm.prop_of) ??
+ Conv.fconv_rule (More_Conv.top_conv let_conv ctxt))
end
@@ -190,7 +171,6 @@
Term.exists_subterm neg_numeral t andalso
is_number_sort (ProofContext.theory_of ctxt) (Term.body_type T)
| is_neg_number _ _ = false
- fun has_neg_number ctxt = Term.exists_subterm (is_neg_number ctxt)
val pos_numeral_ss = HOL_ss
addsimps [@{thm Int.number_of_minus}, @{thm Int.number_of_Min}]
@@ -207,11 +187,10 @@
fun pos_conv ctxt = if_conv (is_neg_number ctxt)
(Simplifier.rewrite (Simplifier.context ctxt pos_numeral_ss))
Conv.no_conv
-
- fun cond_pos_conv ctxt = if_true_conv (has_neg_number ctxt)
- (More_Conv.top_sweep_conv pos_conv ctxt)
in
-fun positive_numerals ctxt = map (Conv.fconv_rule (cond_pos_conv ctxt))
+fun positive_numerals ctxt =
+ map ((Term.exists_subterm (is_neg_number ctxt) o Thm.prop_of) ??
+ Conv.fconv_rule (More_Conv.top_sweep_conv pos_conv ctxt))
end
@@ -275,23 +254,14 @@
val uses_nat_int =
Term.exists_subterm (member (op aconv) [@{term int}, @{term nat}])
in
-fun nat_as_int ctxt thms =
- let
- fun norm thm = thm
- |> uses_nat_type (Thm.prop_of thm) ? Conv.fconv_rule (conv ctxt)
- val thms' = map norm thms
- in
- if exists (uses_nat_int o Thm.prop_of) thms' then nat_embedding @ thms'
- else thms'
- end
+fun nat_as_int ctxt =
+ map ((uses_nat_type o Thm.prop_of) ?? Conv.fconv_rule (conv ctxt)) #>
+ exists (uses_nat_int o Thm.prop_of) ?? append nat_embedding
end
(* include additional rules *)
-val (unfold_defs, unfold_defs_setup) =
- Attrib.config_bool "smt_unfold_defs" (K true)
-
local
val pair_rules = [@{thm fst_conv}, @{thm snd_conv}, @{thm pair_collapse}]
@@ -302,46 +272,50 @@
val is_fun_upd = (fn Const (@{const_name fun_upd}, _) => true | _ => false)
val exists_fun_upd = Term.exists_subterm is_fun_upd
in
-fun add_pair_rules _ thms =
- thms
- |> exists (exists_pair_type o Thm.prop_of) thms ? append pair_rules
+fun add_pair_rules _ =
+ exists (exists_pair_type o Thm.prop_of) ?? append pair_rules
-fun add_fun_upd_rules _ thms =
- thms
- |> exists (exists_fun_upd o Thm.prop_of) thms ? append fun_upd_rules
+fun add_fun_upd_rules _ =
+ exists (exists_fun_upd o Thm.prop_of) ?? append fun_upd_rules
end
+(* unfold definitions of specific constants *)
+
local
- fun mk_entry t thm = (Term.head_of t, (thm, thm RS @{thm eq_reflection}))
+ fun mk_entry (t as Const (n, _)) thm = ((n, t), thm)
+ | mk_entry t _ = raise TERM ("mk_entry", [t])
fun prepare_def thm =
- (case HOLogic.dest_Trueprop (Thm.prop_of thm) of
- Const (@{const_name "op ="}, _) $ t $ _ => mk_entry t thm
+ (case Thm.prop_of thm of
+ Const (@{const_name "=="}, _) $ t $ _ => mk_entry (Term.head_of t) thm
| t => raise TERM ("prepare_def", [t]))
val defs = map prepare_def [
- @{thm abs_if[where 'a = int]}, @{thm abs_if[where 'a = real]},
- @{thm min_def[where 'a = int]}, @{thm min_def[where 'a = real]},
- @{thm max_def[where 'a = int]}, @{thm max_def[where 'a = real]}]
+ @{thm abs_if[where 'a = int, THEN eq_reflection]},
+ @{thm abs_if[where 'a = real, THEN eq_reflection]},
+ @{thm min_def[where 'a = int, THEN eq_reflection]},
+ @{thm min_def[where 'a = real, THEN eq_reflection]},
+ @{thm max_def[where 'a = int, THEN eq_reflection]},
+ @{thm max_def[where 'a = real, THEN eq_reflection]},
+ @{thm Ex1_def}, @{thm Ball_def}, @{thm Bex_def}]
- fun add_sym t = if AList.defined (op =) defs t then insert (op =) t else I
- fun add_syms thms = fold (Term.fold_aterms add_sym o Thm.prop_of) thms []
+ fun matches thy ((t as Const (n, _)), (m, p)) =
+ n = m andalso Pattern.matches thy (p, t)
+ | matches _ _ = false
- fun unfold_def_conv ds ct =
- (case AList.lookup (op =) ds (Term.head_of (Thm.term_of ct)) of
- SOME (_, eq) => Conv.rewr_conv eq
+ fun lookup_def thy = AList.lookup (matches thy) defs
+ fun lookup_def_head thy = lookup_def thy o Term.head_of
+
+ fun occurs_def thy = Term.exists_subterm (is_some o lookup_def thy)
+
+ fun unfold_def_conv ctxt ct =
+ (case lookup_def_head (ProofContext.theory_of ctxt) (Thm.term_of ct) of
+ SOME thm => Conv.rewr_conv thm
| NONE => Conv.all_conv) ct
-
- fun unfold_conv ctxt thm =
- (case filter (member (op =) (add_syms [thm]) o fst) defs of
- [] => thm
- | ds => thm |> Conv.fconv_rule
- (More_Conv.bottom_conv (K (unfold_def_conv ds)) ctxt))
in
-fun add_abs_min_max_rules ctxt thms =
- if Config.get ctxt unfold_defs
- then map (unfold_conv ctxt) thms
- else map fst (map_filter (AList.lookup (op =) defs) (add_syms thms)) @ thms
+fun unfold_defs ctxt =
+ (occurs_def (ProofContext.theory_of ctxt) o Thm.prop_of) ??
+ Conv.fconv_rule (More_Conv.top_conv unfold_def_conv ctxt)
end
@@ -496,29 +470,15 @@
(* combined normalization *)
-datatype config =
- RewriteTrivialLets |
- RewriteNegativeNumerals |
- RewriteNaturalNumbers |
- AddPairRules |
- AddFunUpdRules |
- AddAbsMinMaxRules
-
-fun normalize config ctxt thms =
- let fun if_enabled c f = member (op =) config c ? f ctxt
- in
- thms
- |> if_enabled RewriteTrivialLets trivial_let
- |> if_enabled RewriteNegativeNumerals positive_numerals
- |> if_enabled RewriteNaturalNumbers nat_as_int
- |> if_enabled AddPairRules add_pair_rules
- |> if_enabled AddFunUpdRules add_fun_upd_rules
- |> if_enabled AddAbsMinMaxRules add_abs_min_max_rules
- |> map (normalize_rule ctxt)
- |> lift_lambdas ctxt
- |> apsnd (explicit_application ctxt)
- end
-
-val setup = unfold_defs_setup
+fun normalize ctxt thms =
+ thms
+ |> trivial_let ctxt
+ |> positive_numerals ctxt
+ |> nat_as_int ctxt
+ |> add_pair_rules ctxt
+ |> add_fun_upd_rules ctxt
+ |> map (unfold_defs ctxt #> normalize_rule ctxt)
+ |> lift_lambdas ctxt
+ |> apsnd (explicit_application ctxt)
end
--- a/src/HOL/SMT/Tools/smt_solver.ML Wed Apr 07 19:17:10 2010 +0200
+++ b/src/HOL/SMT/Tools/smt_solver.ML Wed Apr 07 22:22:49 2010 +0200
@@ -9,9 +9,6 @@
exception SMT of string
exception SMT_COUNTEREXAMPLE of bool * term list
- type interface = {
- normalize: SMT_Normalize.config list,
- translate: SMT_Translate.config }
type proof_data = {
context: Proof.context,
output: string list,
@@ -20,7 +17,7 @@
type solver_config = {
command: {env_var: string, remote_name: string option},
arguments: string list,
- interface: string list -> interface,
+ interface: string list -> SMT_Translate.config,
reconstruct: proof_data -> thm }
(*options*)
@@ -30,7 +27,7 @@
val trace_msg: Proof.context -> ('a -> string) -> 'a -> unit
(*certificates*)
- val record: bool Config.T
+ val fixed_certificates: bool Config.T
val select_certificates: string -> Context.generic -> Context.generic
(*solvers*)
@@ -60,10 +57,6 @@
exception SMT_COUNTEREXAMPLE of bool * term list
-type interface = {
- normalize: SMT_Normalize.config list,
- translate: SMT_Translate.config }
-
type proof_data = {
context: Proof.context,
output: string list,
@@ -73,7 +66,7 @@
type solver_config = {
command: {env_var: string, remote_name: string option},
arguments: string list,
- interface: string list -> interface,
+ interface: string list -> SMT_Translate.config,
reconstruct: proof_data -> thm }
@@ -93,7 +86,8 @@
(* SMT certificates *)
-val (record, setup_record) = Attrib.config_bool "smt_record" (K true)
+val (fixed_certificates, setup_fixed_certificates) =
+ Attrib.config_bool "smt_fixed" (K false)
structure Certificates = Generic_Data
(
@@ -112,22 +106,6 @@
local
-fun invoke ctxt output f problem_path =
- let
- fun pretty tag ls = Pretty.string_of (Pretty.big_list tag
- (map Pretty.str ls))
-
- val x = File.open_output output problem_path
- val _ = trace_msg ctxt (pretty "SMT problem:" o split_lines o File.read)
- problem_path
-
- val (res, err) = with_timeout ctxt f problem_path
- val _ = trace_msg ctxt (pretty "SMT solver:") err
-
- val ls = rev (dropwhile (equal "") (rev res))
- val _ = trace_msg ctxt (pretty "SMT result:") ls
- in (x, ls) end
-
fun choose {env_var, remote_name} =
let
val local_solver = getenv env_var
@@ -150,29 +128,40 @@
map File.shell_quote (solver @ args) @
[File.shell_path problem_path, "2>&1", ">", File.shell_path proof_path])
-fun no_cmd _ _ = error ("Bad certificates cache: missing certificate")
-
-fun run ctxt cmd args problem_path =
- let val certs = Certificates.get (Context.Proof ctxt)
- in
- if is_none certs
- then Cache_IO.run' (make_cmd (choose cmd) args) problem_path
- else if Config.get ctxt record
- then Cache_IO.cached' (the certs) (make_cmd (choose cmd) args) problem_path
- else
- (tracing ("Using cached certificate from " ^
- File.shell_path (Cache_IO.cache_path_of (the certs)) ^ " ...");
- Cache_IO.cached' (the certs) no_cmd problem_path)
- end
+fun run ctxt cmd args input =
+ (case Certificates.get (Context.Proof ctxt) of
+ NONE => Cache_IO.run (make_cmd (choose cmd) args) input
+ | SOME certs =>
+ (case Cache_IO.lookup certs input of
+ (NONE, key) =>
+ if Config.get ctxt fixed_certificates
+ then error ("Bad certificates cache: missing certificate")
+ else Cache_IO.run_and_cache certs key (make_cmd (choose cmd) args)
+ input
+ | (SOME output, _) =>
+ (tracing ("Using cached certificate from " ^
+ File.shell_path (Cache_IO.cache_path_of certs) ^ " ...");
+ output)))
in
-fun run_solver ctxt cmd args output =
- Cache_IO.with_tmp_file "smt-" (invoke ctxt output (run ctxt cmd args))
+fun run_solver ctxt cmd args input =
+ let
+ fun pretty tag ls = Pretty.string_of (Pretty.big_list tag
+ (map Pretty.str ls))
+
+ val _ = trace_msg ctxt (pretty "SMT problem:" o split_lines) input
+
+ val (res, err) = with_timeout ctxt (run ctxt cmd args) input
+ val _ = trace_msg ctxt (pretty "SMT solver:") err
+
+ val ls = rev (dropwhile (equal "") (rev res))
+ val _ = trace_msg ctxt (pretty "SMT result:") ls
+ in ls end
end
-fun make_proof_data ctxt ((recon, thms), ls) =
+fun make_proof_data ctxt (ls, (recon, thms)) =
{context=ctxt, output=ls, recon=recon, assms=SOME thms}
fun gen_solver name solver ctxt prems =
@@ -181,11 +170,12 @@
val comments = ("solver: " ^ name) ::
("timeout: " ^ string_of_int (Config.get ctxt timeout)) ::
"arguments:" :: arguments
- val {normalize=nc, translate=tc} = interface comments
+ val tc = interface comments
val thy = ProofContext.theory_of ctxt
in
- SMT_Normalize.normalize nc ctxt prems
- ||> run_solver ctxt command arguments o SMT_Translate.translate tc thy
+ SMT_Normalize.normalize ctxt prems
+ ||> SMT_Translate.translate tc thy
+ ||> apfst (run_solver ctxt command arguments)
||> reconstruct o make_proof_data ctxt
|-> fold SMT_Normalize.discharge_definition
end
@@ -261,11 +251,22 @@
| SMT_COUNTEREXAMPLE ce => fail_tac tracing (pretty_cex ctxt ce) st)
fun smt_solver rules ctxt = solver_of (Context.Proof ctxt) ctxt rules
+
+ val has_topsort = Term.exists_type (Term.exists_subtype (fn
+ TFree (_, []) => true
+ | TVar (_, []) => true
+ | _ => false))
in
fun smt_tac' pass_exns ctxt rules =
Tactic.rtac @{thm ccontr} THEN'
SUBPROOF (fn {context, prems, ...} =>
- SAFE pass_exns (Tactic.rtac o smt_solver (rules @ prems)) context 1) ctxt
+ let val thms = rules @ prems
+ in
+ if exists (has_topsort o Thm.prop_of) thms
+ then fail_tac (trace_msg context I)
+ "SMT: proof state contains the universal sort {}"
+ else SAFE pass_exns (Tactic.rtac o smt_solver thms) context 1
+ end) ctxt
val smt_tac = smt_tac' false
end
@@ -285,7 +286,7 @@
"SMT solver configuration" #>
setup_timeout #>
setup_trace #>
- setup_record #>
+ setup_fixed_certificates #>
Attrib.setup (Binding.name "smt_certificates")
(Scan.lift (OuterParse.$$$ "=" |-- Args.name) >>
(Thm.declaration_attribute o K o select_certificates))
--- a/src/HOL/SMT/Tools/smt_translate.ML Wed Apr 07 19:17:10 2010 +0200
+++ b/src/HOL/SMT/Tools/smt_translate.ML Wed Apr 07 22:22:49 2010 +0200
@@ -55,11 +55,10 @@
prefixes: prefixes,
markers: markers,
builtins: builtins,
- serialize: sign -> (string, string) sterm list -> TextIO.outstream -> unit}
+ serialize: sign -> (string, string) sterm list -> string}
type recon = {typs: typ Symtab.table, terms: term Symtab.table}
- val translate: config -> theory -> thm list -> TextIO.outstream ->
- recon * thm list
+ val translate: config -> theory -> thm list -> string * (recon * thm list)
val dest_binT: typ -> int
val dest_funT: int -> typ -> typ list * typ
@@ -180,7 +179,7 @@
prefixes: prefixes,
markers: markers,
builtins: builtins,
- serialize: sign -> (string, string) sterm list -> TextIO.outstream -> unit}
+ serialize: sign -> (string, string) sterm list -> string}
type recon = {typs: typ Symtab.table, terms: term Symtab.table}
@@ -527,7 +526,7 @@
(* Combination of all translation functions and invocation of serialization. *)
-fun translate config thy thms stream =
+fun translate config thy thms =
let val {strict, prefixes, markers, builtins, serialize} = config
in
map Thm.prop_of thms
@@ -535,8 +534,8 @@
|> intermediate
|> (if strict then separate thy else pair [])
||>> signature_of prefixes markers builtins thy
- ||> (fn (sgn, ts) => serialize sgn ts stream)
- |> (fn ((thms', rtab), _) => (rtab, thms' @ thms))
+ ||> (fn (sgn, ts) => serialize sgn ts)
+ |> (fn ((thms', rtab), str) => (str, (rtab, thms' @ thms)))
end
end
--- a/src/HOL/SMT/Tools/smtlib_interface.ML Wed Apr 07 19:17:10 2010 +0200
+++ b/src/HOL/SMT/Tools/smtlib_interface.ML Wed Apr 07 22:22:49 2010 +0200
@@ -9,8 +9,8 @@
val basic_builtins: SMT_Translate.builtins
val default_attributes: string list
val gen_interface: SMT_Translate.builtins -> string list -> string list ->
- SMT_Solver.interface
- val interface: string list -> SMT_Solver.interface
+ SMT_Translate.config
+ val interface: string list -> SMT_Translate.config
end
structure SMTLIB_Interface: SMTLIB_INTERFACE =
@@ -61,7 +61,7 @@
(* serialization *)
-fun wr s stream = (TextIO.output (stream, s); stream)
+val wr = Buffer.add
fun wr_line f = f #> wr "\n"
fun sep f = wr " " #> f
@@ -118,11 +118,10 @@
| wr_pat (T.SNoPat ts) = wrp "nopat" ts
in par (wr_quant q #> fold wr_var vs #> wre b #> fold wr_pat ps) end)
-fun serialize attributes comments ({typs, funs, preds} : T.sign) ts stream =
- let
- fun wr_decl (n, Ts) = wr_line (sep (par (wr n #> fold wr1 Ts)))
+fun serialize attributes comments ({typs, funs, preds} : T.sign) ts =
+ let fun wr_decl (n, Ts) = wr_line (sep (par (wr n #> fold wr1 Ts)))
in
- stream
+ Buffer.empty
|> wr_line (wr "(benchmark Isabelle")
|> wr_line (wr ":status unknown")
|> fold (wr_line o wr) attributes
@@ -140,7 +139,7 @@
|> wr_line (wr ":formula true")
|> wr_line (wr ")")
|> fold (fn comment => wr_line (wr ("; " ^ comment))) comments
- |> K ()
+ |> Buffer.content
end
@@ -154,25 +153,17 @@
val default_attributes = [":logic AUFLIRA"]
fun gen_interface builtins attributes comments = {
- normalize = [
- SMT_Normalize.RewriteTrivialLets,
- SMT_Normalize.RewriteNegativeNumerals,
- SMT_Normalize.RewriteNaturalNumbers,
- SMT_Normalize.AddAbsMinMaxRules,
- SMT_Normalize.AddPairRules,
- SMT_Normalize.AddFunUpdRules ],
- translate = {
- strict = true,
- prefixes = {
- var_prefix = "x",
- typ_prefix = "T",
- fun_prefix = "uf_",
- pred_prefix = "up_" },
- markers = {
- term_marker = term_marker,
- formula_marker = formula_marker },
- builtins = builtins,
- serialize = serialize attributes comments }}
+ strict = true,
+ prefixes = {
+ var_prefix = "x",
+ typ_prefix = "T",
+ fun_prefix = "uf_",
+ pred_prefix = "up_" },
+ markers = {
+ term_marker = term_marker,
+ formula_marker = formula_marker },
+ builtins = builtins,
+ serialize = serialize attributes comments }
fun interface comments =
gen_interface basic_builtins default_attributes comments
--- a/src/HOL/SMT/Tools/z3_interface.ML Wed Apr 07 19:17:10 2010 +0200
+++ b/src/HOL/SMT/Tools/z3_interface.ML Wed Apr 07 22:22:49 2010 +0200
@@ -6,7 +6,7 @@
signature Z3_INTERFACE =
sig
- val interface: string list -> SMT_Solver.interface
+ val interface: string list -> SMT_Translate.config
end
structure Z3_Interface: Z3_INTERFACE =
--- a/src/Tools/cache_io.ML Wed Apr 07 19:17:10 2010 +0200
+++ b/src/Tools/cache_io.ML Wed Apr 07 22:22:49 2010 +0200
@@ -7,20 +7,23 @@
signature CACHE_IO =
sig
val with_tmp_file: string -> (Path.T -> 'a) -> 'a
- val run: (Path.T -> string) -> Path.T -> string list
- val run': (Path.T -> Path.T -> string) -> Path.T -> string list * string list
+ val run: (Path.T -> Path.T -> string) -> string -> string list * string list
type cache
val make: Path.T -> cache
val cache_path_of: cache -> Path.T
- val cached: cache -> (Path.T -> string) -> Path.T -> string list
- val cached': cache -> (Path.T -> Path.T -> string) -> Path.T ->
+ val lookup: cache -> string -> (string list * string list) option * string
+ val run_and_cache: cache -> string -> (Path.T -> Path.T -> string) ->
+ string -> string list * string list
+ val run_cached: cache -> (Path.T -> Path.T -> string) -> string ->
string list * string list
end
structure Cache_IO : CACHE_IO =
struct
+val cache_io_prefix = "cache-io-"
+
fun with_tmp_file name f =
let
val path = File.tmp_path (Path.explode (name ^ serial_string ()))
@@ -28,14 +31,14 @@
val _ = try File.rm path
in Exn.release x end
-fun run' make_cmd in_path =
- with_tmp_file "cache-io-" (fn out_path =>
+fun run make_cmd str =
+ with_tmp_file cache_io_prefix (fn in_path =>
+ with_tmp_file cache_io_prefix (fn out_path =>
let
+ val _ = File.write in_path str
val (out2, _) = bash_output (make_cmd in_path out_path)
val out1 = the_default [] (try (rev o File.fold_lines cons out_path) [])
- in (out1, split_lines out2) end)
-
-fun run make_cmd = snd o run' (fn in_path => fn _ => make_cmd in_path)
+ in (out1, split_lines out2) end))
@@ -85,28 +88,35 @@
else (i, xsp)
in pairself rev (snd (File.fold_lines load cache_path (1, ([], [])))) end
-fun cached' (Cache {path=cache_path, table}) make_cmd in_path =
- let val key = SHA1.digest (File.read in_path)
+
+fun lookup (Cache {path=cache_path, table}) str =
+ let val key = SHA1.digest str
in
(case Symtab.lookup (snd (Synchronized.value table)) key of
- SOME pos => load_cached_result cache_path pos
- | NONE =>
- let
- val res as (out, err) = run' make_cmd in_path
- val (l1, l2) = pairself length res
- val header = key ^ " " ^ string_of_int l1 ^ " " ^ string_of_int l2
- val lines = map (suffix "\n") (header :: out @ err)
-
- val _ = Synchronized.change table (fn (p, tab) =>
- if Symtab.defined tab key then (p, tab)
- else
- let val _ = File.append_list cache_path lines
- in (p+l1+l2+1, Symtab.update (key, (p+1, l1, l2)) tab) end)
- in res end)
+ NONE => (NONE, key)
+ | SOME pos => (SOME (load_cached_result cache_path pos), key))
end
-fun cached cache make_cmd =
- snd o cached' cache (fn in_path => fn _ => make_cmd in_path)
+
+fun run_and_cache (Cache {path=cache_path, table}) key make_cmd str =
+ let
+ val res as (out, err) = run make_cmd str
+ val (l1, l2) = pairself length res
+ val header = key ^ " " ^ string_of_int l1 ^ " " ^ string_of_int l2
+ val lines = map (suffix "\n") (header :: out @ err)
+
+ val _ = Synchronized.change table (fn (p, tab) =>
+ if Symtab.defined tab key then (p, tab)
+ else
+ let val _ = File.append_list cache_path lines
+ in (p+l1+l2+1, Symtab.update (key, (p+1, l1, l2)) tab) end)
+ in res end
+
+
+fun run_cached cache make_cmd str =
+ (case lookup cache str of
+ (NONE, key) => run_and_cache cache key make_cmd str
+ | (SOME output, _) => output)
end
end