--- a/src/HOL/Boogie/Examples/Boogie_Dijkstra.thy Tue Mar 27 16:59:13 2012 +0300
+++ b/src/HOL/Boogie/Examples/Boogie_Dijkstra.thy Tue Mar 27 16:59:13 2012 +0300
@@ -82,9 +82,9 @@
boogie_open "Boogie_Dijkstra.b2i"
-declare [[smt_certificates="Boogie_Dijkstra.certs"]]
-declare [[smt_fixed=true]]
-declare [[smt_oracle=false]]
+declare [[smt_certificates = "Boogie_Dijkstra.certs"]]
+declare [[smt_read_only_certificates = true]]
+declare [[smt_oracle = false]]
boogie_vc Dijkstra
by boogie
--- a/src/HOL/Boogie/Examples/Boogie_Max.thy Tue Mar 27 16:59:13 2012 +0300
+++ b/src/HOL/Boogie/Examples/Boogie_Max.thy Tue Mar 27 16:59:13 2012 +0300
@@ -39,9 +39,9 @@
boogie_open "Boogie_Max.b2i"
-declare [[smt_certificates="Boogie_Max.certs"]]
-declare [[smt_fixed=true]]
-declare [[smt_oracle=false]]
+declare [[smt_certificates = "Boogie_Max.certs"]]
+declare [[smt_read_only_certificates = true]]
+declare [[smt_oracle = false]]
boogie_vc max
by boogie
--- a/src/HOL/Boogie/Examples/VCC_Max.thy Tue Mar 27 16:59:13 2012 +0300
+++ b/src/HOL/Boogie/Examples/VCC_Max.thy Tue Mar 27 16:59:13 2012 +0300
@@ -47,9 +47,9 @@
boogie_open (quiet) "VCC_Max.b2i"
-declare [[smt_certificates="VCC_Max.certs"]]
-declare [[smt_fixed=true]]
-declare [[smt_oracle=false]]
+declare [[smt_certificates = "VCC_Max.certs"]]
+declare [[smt_read_only_certificates = true]]
+declare [[smt_oracle = false]]
boogie_status
--- a/src/HOL/Multivariate_Analysis/Integration.thy Tue Mar 27 16:59:13 2012 +0300
+++ b/src/HOL/Multivariate_Analysis/Integration.thy Tue Mar 27 16:59:13 2012 +0300
@@ -8,9 +8,9 @@
"~~/src/HOL/Library/Indicator_Function"
begin
-declare [[smt_certificates="Integration.certs"]]
-declare [[smt_fixed=true]]
-declare [[smt_oracle=false]]
+declare [[smt_certificates = "Integration.certs"]]
+declare [[smt_read_only_certificates = true]]
+declare [[smt_oracle = false]]
(*declare not_less[simp] not_le[simp]*)
@@ -5583,7 +5583,7 @@
using assms(3)[rule_format,OF x] unfolding real_norm_def abs_le_iff by auto
qed qed(insert n,auto) qed qed qed
-declare [[smt_certificates=""]]
-declare [[smt_fixed=false]]
+declare [[smt_certificates = ""]]
+declare [[smt_read_only_certificates = false]]
end
--- a/src/HOL/SMT.thy Tue Mar 27 16:59:13 2012 +0300
+++ b/src/HOL/SMT.thy Tue Mar 27 16:59:13 2012 +0300
@@ -272,16 +272,16 @@
declare [[ smt_certificates = "" ]]
text {*
-The option @{text smt_fixed} controls whether only stored
-certificates are should be used or invocation of an SMT solver is
-allowed. When set to @{text true}, no SMT solver will ever be
+The option @{text smt_read_only_certificates} controls whether only
+stored certificates are should be used or invocation of an SMT solver
+is allowed. When set to @{text true}, no SMT solver will ever be
invoked and only the existing certificates found in the configured
cache are used; when set to @{text false} and there is no cached
certificate for some proposition, then the configured SMT solver is
invoked.
*}
-declare [[ smt_fixed = false ]]
+declare [[ smt_read_only_certificates = false ]]
--- a/src/HOL/SMT_Examples/SMT_Examples.thy Tue Mar 27 16:59:13 2012 +0300
+++ b/src/HOL/SMT_Examples/SMT_Examples.thy Tue Mar 27 16:59:13 2012 +0300
@@ -8,9 +8,9 @@
imports Complex_Main
begin
-declare [[smt_oracle=false]]
-declare [[smt_certificates="SMT_Examples.certs"]]
-declare [[smt_fixed=true]]
+declare [[smt_oracle = false]]
+declare [[smt_certificates = "SMT_Examples.certs"]]
+declare [[smt_read_only_certificates = true]]
--- a/src/HOL/SMT_Examples/SMT_Tests.thy Tue Mar 27 16:59:13 2012 +0300
+++ b/src/HOL/SMT_Examples/SMT_Tests.thy Tue Mar 27 16:59:13 2012 +0300
@@ -8,9 +8,9 @@
imports Complex_Main
begin
-declare [[smt_oracle=false]]
-declare [[smt_certificates="SMT_Tests.certs"]]
-declare [[smt_fixed=true]]
+declare [[smt_oracle = false]]
+declare [[smt_certificates = "SMT_Tests.certs"]]
+declare [[smt_read_only_certificates = true]]
--- a/src/HOL/SMT_Examples/SMT_Word_Examples.thy Tue Mar 27 16:59:13 2012 +0300
+++ b/src/HOL/SMT_Examples/SMT_Word_Examples.thy Tue Mar 27 16:59:13 2012 +0300
@@ -8,9 +8,9 @@
imports Word
begin
-declare [[smt_oracle=true]]
-declare [[smt_certificates="SMT_Word_Examples.certs"]]
-declare [[smt_fixed=true]]
+declare [[smt_oracle = true]]
+declare [[smt_certificates = "SMT_Word_Examples.certs"]]
+declare [[smt_read_only_certificates = true]]
--- a/src/HOL/Tools/SMT/smt_config.ML Tue Mar 27 16:59:13 2012 +0300
+++ b/src/HOL/Tools/SMT/smt_config.ML Tue Mar 27 16:59:13 2012 +0300
@@ -26,7 +26,7 @@
val datatypes: bool Config.T
val timeout: real Config.T
val random_seed: int Config.T
- val fixed: bool Config.T
+ val read_only_certificates: bool Config.T
val verbose: bool Config.T
val trace: bool Config.T
val trace_used_facts: bool Config.T
@@ -153,7 +153,7 @@
val datatypes = Attrib.setup_config_bool @{binding smt_datatypes} (K false)
val timeout = Attrib.setup_config_real @{binding smt_timeout} (K 30.0)
val random_seed = Attrib.setup_config_int @{binding smt_random_seed} (K 1)
-val fixed = Attrib.setup_config_bool @{binding smt_fixed} (K false)
+val read_only_certificates = Attrib.setup_config_bool @{binding smt_read_only_certificates} (K false)
val verbose = Attrib.setup_config_bool @{binding smt_verbose} (K true)
val trace = Attrib.setup_config_bool @{binding smt_trace} (K false)
val trace_used_facts = Attrib.setup_config_bool @{binding smt_trace_used_facts} (K false)
@@ -243,7 +243,7 @@
string_of_bool (not (Config.get ctxt oracle))),
Pretty.str ("Certificates cache: " ^ certs_filename),
Pretty.str ("Fixed certificates: " ^
- string_of_bool (Config.get ctxt fixed))])
+ string_of_bool (Config.get ctxt read_only_certificates))])
end
val _ =
--- a/src/HOL/Tools/SMT/smt_solver.ML Tue Mar 27 16:59:13 2012 +0300
+++ b/src/HOL/Tools/SMT/smt_solver.ML Tue Mar 27 16:59:13 2012 +0300
@@ -79,8 +79,8 @@
| SOME certs =>
(case Cache_IO.lookup certs input of
(NONE, key) =>
- if Config.get ctxt SMT_Config.fixed then
- error ("Bad certificates cache: missing certificate")
+ if Config.get ctxt SMT_Config.read_only_certificates then
+ error ("Bad certificate cache: missing certificate")
else
Cache_IO.run_and_cache certs key mk_cmd input
| (SOME output, _) =>