# HG changeset patch
# User blanchet
# Date 1332856753 -10800
# Node ID 446cfc760ccf39471ffd166b0b55b989ebe6eadc
# Parent  eaf0ffea11aaa6ad5f99d6e7ddaa0059d23e294f
renamed "smt_fixed" to "smt_read_only_certificates"

diff -r eaf0ffea11aa -r 446cfc760ccf src/HOL/Boogie/Examples/Boogie_Dijkstra.thy
--- 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
diff -r eaf0ffea11aa -r 446cfc760ccf src/HOL/Boogie/Examples/Boogie_Max.thy
--- 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
diff -r eaf0ffea11aa -r 446cfc760ccf src/HOL/Boogie/Examples/VCC_Max.thy
--- 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
 
diff -r eaf0ffea11aa -r 446cfc760ccf src/HOL/Multivariate_Analysis/Integration.thy
--- 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
diff -r eaf0ffea11aa -r 446cfc760ccf src/HOL/SMT.thy
--- 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 ]]
 
 
 
diff -r eaf0ffea11aa -r 446cfc760ccf src/HOL/SMT_Examples/SMT_Examples.thy
--- 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]]
 
 
 
diff -r eaf0ffea11aa -r 446cfc760ccf src/HOL/SMT_Examples/SMT_Tests.thy
--- 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]]
 
 
 
diff -r eaf0ffea11aa -r 446cfc760ccf src/HOL/SMT_Examples/SMT_Word_Examples.thy
--- 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]]
 
 
 
diff -r eaf0ffea11aa -r 446cfc760ccf src/HOL/Tools/SMT/smt_config.ML
--- 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 _ =
diff -r eaf0ffea11aa -r 446cfc760ccf src/HOL/Tools/SMT/smt_solver.ML
--- 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, _) =>