# HG changeset patch # User boehmes # Date 1270662538 -7200 # Node ID 70deefb6c093593237715e1852174ebd811f724d # Parent 0d9affa4e73c8251cec42391d0fb3caa6c9c32ba renamed "smt_record" to "smt_fixed" (somewhat more expressive) and inverted its semantics diff -r 0d9affa4e73c -r 70deefb6c093 src/HOL/Boogie/Examples/Boogie_Dijkstra.thy --- a/src/HOL/Boogie/Examples/Boogie_Dijkstra.thy Wed Apr 07 17:24:44 2010 +0200 +++ b/src/HOL/Boogie/Examples/Boogie_Dijkstra.thy Wed Apr 07 19:48:58 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]] diff -r 0d9affa4e73c -r 70deefb6c093 src/HOL/Boogie/Examples/Boogie_Max.thy --- a/src/HOL/Boogie/Examples/Boogie_Max.thy Wed Apr 07 17:24:44 2010 +0200 +++ b/src/HOL/Boogie/Examples/Boogie_Max.thy Wed Apr 07 19:48:58 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]] diff -r 0d9affa4e73c -r 70deefb6c093 src/HOL/Boogie/Examples/VCC_Max.thy --- a/src/HOL/Boogie/Examples/VCC_Max.thy Wed Apr 07 17:24:44 2010 +0200 +++ b/src/HOL/Boogie/Examples/VCC_Max.thy Wed Apr 07 19:48:58 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 diff -r 0d9affa4e73c -r 70deefb6c093 src/HOL/Multivariate_Analysis/Integration.thy --- a/src/HOL/Multivariate_Analysis/Integration.thy Wed Apr 07 17:24:44 2010 +0200 +++ b/src/HOL/Multivariate_Analysis/Integration.thy Wed Apr 07 19:48:58 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 \ b" shows a b using assms by auto diff -r 0d9affa4e73c -r 70deefb6c093 src/HOL/SMT/Examples/SMT_Examples.thy --- a/src/HOL/SMT/Examples/SMT_Examples.thy Wed Apr 07 17:24:44 2010 +0200 +++ b/src/HOL/SMT/Examples/SMT_Examples.thy Wed Apr 07 19:48:58 2010 +0200 @@ -17,7 +17,7 @@ the following option is set to "false": *} -declare [[smt_record=false]] +declare [[smt_fixed=true]] diff -r 0d9affa4e73c -r 70deefb6c093 src/HOL/SMT/SMT.thy --- a/src/HOL/SMT/SMT.thy Wed Apr 07 17:24:44 2010 +0200 +++ b/src/HOL/SMT/SMT.thy Wed Apr 07 19:48:58 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 *} diff -r 0d9affa4e73c -r 70deefb6c093 src/HOL/SMT/Tools/smt_solver.ML --- a/src/HOL/SMT/Tools/smt_solver.ML Wed Apr 07 17:24:44 2010 +0200 +++ b/src/HOL/SMT/Tools/smt_solver.ML Wed Apr 07 19:48:58 2010 +0200 @@ -30,7 +30,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*) @@ -93,7 +93,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 ( @@ -157,7 +158,7 @@ in if is_none certs then Cache_IO.run' (make_cmd (choose cmd) args) problem_path - else if Config.get ctxt record + else if Config.get ctxt fixed_certificates then Cache_IO.cached' (the certs) (make_cmd (choose cmd) args) problem_path else (tracing ("Using cached certificate from " ^ @@ -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))