# HG changeset patch # User blanchet # Date 1409179238 -7200 # Node ID 4e477dcd050a75dbbcc01f03b05ca1fd0b9129e9 # Parent 1a0b1817654864613435ab60b70df49855a12b1d prefixed all old SMT commands, attributes, etc., with 'old_' diff -r 1a0b18176548 -r 4e477dcd050a src/HOL/Library/Old_SMT.thy --- a/src/HOL/Library/Old_SMT.thy Thu Aug 28 00:40:38 2014 +0200 +++ b/src/HOL/Library/Old_SMT.thy Thu Aug 28 00:40:38 2014 +0200 @@ -6,7 +6,7 @@ theory Old_SMT imports "../Real" "../Word/Word" -keywords "smt_status" :: diag +keywords "old_smt_status" :: diag begin ML_file "Old_SMT/old_smt_utils.ML" @@ -126,7 +126,7 @@ ML_file "Old_SMT/old_z3_proof_tools.ML" ML_file "Old_SMT/old_z3_proof_literals.ML" ML_file "Old_SMT/old_z3_proof_methods.ML" -named_theorems z3_simp "simplification rules for Z3 proof reconstruction" +named_theorems old_z3_simp "simplification rules for Z3 proof reconstruction" ML_file "Old_SMT/old_z3_proof_reconstruction.ML" ML_file "Old_SMT/old_z3_model.ML" ML_file "Old_SMT/old_smt_setup_solvers.ML" @@ -139,7 +139,7 @@ Old_SMT_Setup_Solvers.setup *} -method_setup smt = {* +method_setup old_smt = {* Scan.optional Attrib.thms [] >> (fn thms => fn ctxt => METHOD (fn facts => HEADGOAL (Old_SMT_Solver.smt_tac ctxt (thms @ facts)))) @@ -150,7 +150,7 @@ text {* The current configuration can be printed by the command -@{text smt_status}, which shows the values of most options. +@{text old_smt_status}, which shows the values of most options. *} @@ -158,8 +158,8 @@ subsection {* General configuration options *} text {* -The option @{text smt_solver} can be used to change the target SMT -solver. The possible values can be obtained from the @{text smt_status} +The option @{text old_smt_solver} can be used to change the target SMT +solver. The possible values can be obtained from the @{text old_smt_status} command. Due to licensing restrictions, Yices and Z3 are not installed/enabled @@ -167,7 +167,7 @@ by setting Isabelle system option @{text z3_non_commercial} to @{text yes}. *} -declare [[ smt_solver = z3 ]] +declare [[ old_smt_solver = z3 ]] text {* Since SMT solvers are potentially non-terminating, there is a timeout @@ -175,14 +175,14 @@ 120 (seconds) is in most cases not advisable. *} -declare [[ smt_timeout = 20 ]] +declare [[ old_smt_timeout = 20 ]] text {* SMT solvers apply randomized heuristics. In case a problem is not solvable by an SMT solver, changing the following option might help. *} -declare [[ smt_random_seed = 1 ]] +declare [[ old_smt_random_seed = 1 ]] text {* In general, the binding to SMT solvers runs as an oracle, i.e, the SMT @@ -191,7 +191,7 @@ a checkable certificate. This is currently only implemented for Z3. *} -declare [[ smt_oracle = false ]] +declare [[ old_smt_oracle = false ]] text {* Each SMT solver provides several commandline options to tweak its @@ -199,9 +199,9 @@ options. *} -declare [[ cvc3_options = "" ]] -declare [[ yices_options = "" ]] -declare [[ z3_options = "" ]] +declare [[ old_cvc3_options = "" ]] +declare [[ old_yices_options = "" ]] +declare [[ old_z3_options = "" ]] text {* Enable the following option to use built-in support for datatypes and @@ -209,7 +209,7 @@ mode. *} -declare [[ smt_datatypes = false ]] +declare [[ old_smt_datatypes = false ]] text {* The SMT method provides an inference mechanism to detect simple triggers @@ -218,7 +218,7 @@ in the SMT solver). To turn it on, set the following option. *} -declare [[ smt_infer_triggers = false ]] +declare [[ old_smt_infer_triggers = false ]] text {* The SMT method monomorphizes the given facts, that is, it tries to @@ -241,7 +241,7 @@ subsection {* Certificates *} text {* -By setting the option @{text smt_certificates} to the name of a file, +By setting the option @{text old_smt_certificates} to the name of a file, all following applications of an SMT solver a cached in that file. Any further application of the same SMT solver (using the very same configuration) re-uses the cached certificate instead of invoking the @@ -254,10 +254,10 @@ to avoid race conditions with other concurrent accesses. *} -declare [[ smt_certificates = "" ]] +declare [[ old_smt_certificates = "" ]] text {* -The option @{text smt_read_only_certificates} controls whether only +The option @{text old_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 @@ -266,7 +266,7 @@ invoked. *} -declare [[ smt_read_only_certificates = false ]] +declare [[ old_smt_read_only_certificates = false ]] @@ -277,24 +277,24 @@ make it entirely silent, set the following option to @{text false}. *} -declare [[ smt_verbose = true ]] +declare [[ old_smt_verbose = true ]] text {* For tracing the generated problem file given to the SMT solver as well as the returned result of the solver, the option -@{text smt_trace} should be set to @{text true}. +@{text old_smt_trace} should be set to @{text true}. *} -declare [[ smt_trace = false ]] +declare [[ old_smt_trace = false ]] text {* From the set of assumptions given to the SMT solver, those assumptions used in the proof are traced when the following option is set to @{term true}. This only works for Z3 when it runs in non-oracle mode -(see options @{text smt_solver} and @{text smt_oracle} above). +(see options @{text old_smt_solver} and @{text old_smt_oracle} above). *} -declare [[ smt_trace_used_facts = false ]] +declare [[ old_smt_trace_used_facts = false ]] @@ -309,12 +309,12 @@ the simplifier when reconstructing theory-specific proof steps. *} -lemmas [z3_rule] = +lemmas [old_z3_rule] = refl eq_commute conj_commute disj_commute simp_thms nnf_simps ring_distribs field_simps times_divide_eq_right times_divide_eq_left if_True if_False not_not -lemma [z3_rule]: +lemma [old_z3_rule]: "(P \ Q) = (\(\P \ \Q))" "(P \ Q) = (\(\Q \ \P))" "(\P \ Q) = (\(P \ \Q))" @@ -325,7 +325,7 @@ "(\P \ \Q) = (\(Q \ P))" by auto -lemma [z3_rule]: +lemma [old_z3_rule]: "(P \ Q) = (Q \ \P)" "(\P \ Q) = (P \ Q)" "(\P \ Q) = (Q \ P)" @@ -335,11 +335,11 @@ "(P \ P) = True" by auto -lemma [z3_rule]: +lemma [old_z3_rule]: "((P = Q) \ R) = (R | (Q = (\P)))" by auto -lemma [z3_rule]: +lemma [old_z3_rule]: "(\True) = False" "(\False) = True" "(x = x) = True" @@ -357,7 +357,7 @@ "(P \ Q) = ((\P \ \Q) \ (P \ Q))" by auto -lemma [z3_rule]: +lemma [old_z3_rule]: "(if P then P else \P) = True" "(if \P then \P else P) = True" "(if P then True else False) = P" @@ -381,7 +381,7 @@ "(if P then x = y else z = y) = (y = (if P then x else z))" by auto -lemma [z3_rule]: +lemma [old_z3_rule]: "0 + (x::int) = x" "x + 0 = x" "x + x = 2 * x" @@ -390,7 +390,7 @@ "x + y = y + x" by auto -lemma [z3_rule]: (* for def-axiom *) +lemma [old_z3_rule]: (* for def-axiom *) "P = Q \ P \ Q" "P = Q \ \P \ \Q" "(\P) = Q \ \P \ Q" diff -r 1a0b18176548 -r 4e477dcd050a src/HOL/Library/Old_SMT/old_smt_config.ML --- a/src/HOL/Library/Old_SMT/old_smt_config.ML Thu Aug 28 00:40:38 2014 +0200 +++ b/src/HOL/Library/Old_SMT/old_smt_config.ML Thu Aug 28 00:40:38 2014 +0200 @@ -83,7 +83,7 @@ else context |> Solvers.map (apfst (Symtab.update (name, (info, [])))) - |> Context.map_theory (Attrib.setup (Binding.name (name ^ "_options")) + |> Context.map_theory (Attrib.setup (Binding.name ("old_" ^ name ^ "_options")) (Scan.lift (@{keyword "="} |-- Args.name) >> (Thm.declaration_attribute o K o set_solver_options o pair name)) ("Additional command line options for SMT solver " ^ quote name)) @@ -142,7 +142,7 @@ in solver_info_of (K []) all_options ctxt end val setup_solver = - Attrib.setup @{binding smt_solver} + Attrib.setup @{binding old_smt_solver} (Scan.lift (@{keyword "="} |-- Args.name) >> (Thm.declaration_attribute o K o select_solver)) "SMT solver configuration" @@ -150,19 +150,19 @@ (* options *) -val oracle = Attrib.setup_config_bool @{binding smt_oracle} (K true) -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 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) -val monomorph_limit = Attrib.setup_config_int @{binding smt_monomorph_limit} (K 10) -val monomorph_instances = Attrib.setup_config_int @{binding smt_monomorph_instances} (K 500) -val infer_triggers = Attrib.setup_config_bool @{binding smt_infer_triggers} (K false) -val filter_only_facts = Attrib.setup_config_bool @{binding smt_filter_only_facts} (K false) -val debug_files = Attrib.setup_config_string @{binding smt_debug_files} (K "") +val oracle = Attrib.setup_config_bool @{binding old_smt_oracle} (K true) +val datatypes = Attrib.setup_config_bool @{binding old_smt_datatypes} (K false) +val timeout = Attrib.setup_config_real @{binding old_smt_timeout} (K 30.0) +val random_seed = Attrib.setup_config_int @{binding old_smt_random_seed} (K 1) +val read_only_certificates = Attrib.setup_config_bool @{binding old_smt_read_only_certificates} (K false) +val verbose = Attrib.setup_config_bool @{binding old_smt_verbose} (K true) +val trace = Attrib.setup_config_bool @{binding old_smt_trace} (K false) +val trace_used_facts = Attrib.setup_config_bool @{binding old_smt_trace_used_facts} (K false) +val monomorph_limit = Attrib.setup_config_int @{binding old_smt_monomorph_limit} (K 10) +val monomorph_instances = Attrib.setup_config_int @{binding old_smt_monomorph_instances} (K 500) +val infer_triggers = Attrib.setup_config_bool @{binding old_smt_infer_triggers} (K false) +val filter_only_facts = Attrib.setup_config_bool @{binding old_smt_filter_only_facts} (K false) +val debug_files = Attrib.setup_config_string @{binding old_smt_debug_files} (K "") (* diagnostics *) @@ -205,7 +205,7 @@ val certificates_of = Certificates.get o Context.Proof val setup_certificates = - Attrib.setup @{binding smt_certificates} + Attrib.setup @{binding old_smt_certificates} (Scan.lift (@{keyword "="} |-- Args.name) >> (Thm.declaration_attribute o K o select_certificates)) "SMT certificates configuration" @@ -246,7 +246,7 @@ end val _ = - Outer_Syntax.improper_command @{command_spec "smt_status"} + Outer_Syntax.improper_command @{command_spec "old_smt_status"} "show the available SMT solvers, the currently selected SMT solver, \ \and the values of SMT configuration options" (Scan.succeed (Toplevel.keep (print_setup o Toplevel.context_of))) diff -r 1a0b18176548 -r 4e477dcd050a src/HOL/Library/Old_SMT/old_smt_setup_solvers.ML --- a/src/HOL/Library/Old_SMT/old_smt_setup_solvers.ML Thu Aug 28 00:40:38 2014 +0200 +++ b/src/HOL/Library/Old_SMT/old_smt_setup_solvers.ML Thu Aug 28 00:40:38 2014 +0200 @@ -129,7 +129,7 @@ val z3_with_extensions = - Attrib.setup_config_bool @{binding z3_with_extensions} (K false) + Attrib.setup_config_bool @{binding old_z3_with_extensions} (K false) local fun z3_make_command name () = if_z3_non_commercial (make_command name) diff -r 1a0b18176548 -r 4e477dcd050a src/HOL/Library/Old_SMT/old_z3_proof_reconstruction.ML --- a/src/HOL/Library/Old_SMT/old_z3_proof_reconstruction.ML Thu Aug 28 00:40:38 2014 +0200 +++ b/src/HOL/Library/Old_SMT/old_z3_proof_reconstruction.ML Thu Aug 28 00:40:38 2014 +0200 @@ -52,8 +52,8 @@ the (Old_Z3_Proof_Tools.net_instance (Old_Z3_Rules.get (Context.Proof ctxt)) ct) val _ = Theory.setup - (Attrib.setup @{binding z3_rule} (Attrib.add_del add del) description #> - Global_Theory.add_thms_dynamic (@{binding z3_rule}, Net.content o Old_Z3_Rules.get)) + (Attrib.setup @{binding old_z3_rule} (Attrib.add_del add del) description #> + Global_Theory.add_thms_dynamic (@{binding old_z3_rule}, Net.content o Old_Z3_Rules.get)) end @@ -80,7 +80,7 @@ Pretty.big_list ("Z3 found a proof," ^ " but proof reconstruction failed at the following subgoal:") (pretty_goal ctxt thms (Thm.term_of ct)), - Pretty.str ("Declaring a rule as [z3_rule] might solve this problem.")]) + Pretty.str ("Declaring a rule as [old_z3_rule] might solve this problem.")]) fun apply [] ct = error (try_apply_err ct) | apply (prover :: provers) ct = @@ -870,7 +870,7 @@ Old_Z3_Proof_Parser.parse ctxt typs terms output val simpset = - Old_Z3_Proof_Tools.make_simpset ctxt1 (Named_Theorems.get ctxt1 @{named_theorems z3_simp}) + Old_Z3_Proof_Tools.make_simpset ctxt1 (Named_Theorems.get ctxt1 @{named_theorems old_z3_simp}) val ((is, rules), cxp as (ctxt2, _)) = add_asserted outer_ctxt rewrite_rules assms asserted ctxt1