# HG changeset patch # User blanchet # Date 1402478926 -7200 # Node ID 7ffa0f7e277531863ee1916b566cff279eef959f # Parent 5bf2a5c498c22fcc6684631860cc1d19547111e9 removed '_new' sufffix in SMT2 solver names (in some cases) diff -r 5bf2a5c498c2 -r 7ffa0f7e2775 src/HOL/SMT2.thy --- a/src/HOL/SMT2.thy Wed Jun 11 11:28:46 2014 +0200 +++ b/src/HOL/SMT2.thy Wed Jun 11 11:28:46 2014 +0200 @@ -161,7 +161,7 @@ by setting Isabelle system option @{text z3_non_commercial} to @{text yes}. *} -declare [[ smt2_solver = z3_new ]] +declare [[smt2_solver = z3]] text {* Since SMT solvers are potentially non-terminating, there is a timeout @@ -169,14 +169,14 @@ 120 (seconds) is in most cases not advisable. *} -declare [[ smt2_timeout = 20 ]] +declare [[smt2_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 [[ smt2_random_seed = 1 ]] +declare [[smt2_random_seed = 1]] text {* In general, the binding to SMT solvers runs as an oracle, i.e, the SMT @@ -185,7 +185,7 @@ a checkable certificate. This is currently only implemented for Z3. *} -declare [[ smt2_oracle = false ]] +declare [[smt2_oracle = false]] text {* Each SMT solver provides several commandline options to tweak its @@ -193,9 +193,9 @@ options. *} -(* declare [[ cvc3_options = "" ]] TODO *) -(* declare [[ yices_options = "" ]] TODO *) -(* declare [[ z3_options = "" ]] TODO *) +declare [[cvc3_new_options = ""]] +declare [[yices_new_options = ""]] +declare [[z3_new_options = ""]] text {* The SMT method provides an inference mechanism to detect simple triggers @@ -204,31 +204,14 @@ in the SMT solver). To turn it on, set the following option. *} -declare [[ smt2_infer_triggers = false ]] +declare [[smt2_infer_triggers = false]] text {* Enable the following option to use built-in support for div/mod, datatypes, and records in Z3. Currently, this is implemented only in oracle mode. *} -declare [[ z3_new_extensions = false ]] - -text {* -The SMT method monomorphizes the given facts, that is, it tries to -instantiate all schematic type variables with fixed types occurring -in the problem. This is a (possibly nonterminating) fixed-point -construction whose cycles are limited by the following option. -*} - -declare [[ monomorph_max_rounds = 5 ]] - -text {* -In addition, the number of generated monomorphic instances is limited -by the following option. -*} - -declare [[ monomorph_max_new_instances = 500 ]] - +declare [[z3_new_extensions = false]] subsection {* Certificates *} @@ -247,7 +230,7 @@ to avoid race conditions with other concurrent accesses. *} -declare [[ smt2_certificates = "" ]] +declare [[smt2_certificates = ""]] text {* The option @{text smt2_read_only_certificates} controls whether only @@ -259,7 +242,7 @@ invoked. *} -declare [[ smt2_read_only_certificates = false ]] +declare [[smt2_read_only_certificates = false]] @@ -270,7 +253,7 @@ make it entirely silent, set the following option to @{text false}. *} -declare [[ smt2_verbose = true ]] +declare [[smt2_verbose = true]] text {* For tracing the generated problem file given to the SMT solver as @@ -278,7 +261,7 @@ @{text smt2_trace} should be set to @{text true}. *} -declare [[ smt2_trace = false ]] +declare [[smt2_trace = false]] subsection {* Schematic rules for Z3 proof reconstruction *} diff -r 5bf2a5c498c2 -r 7ffa0f7e2775 src/HOL/Tools/SMT2/smt2_config.ML --- a/src/HOL/Tools/SMT2/smt2_config.ML Wed Jun 11 11:28:46 2014 +0200 +++ b/src/HOL/Tools/SMT2/smt2_config.ML Wed Jun 11 11:28:46 2014 +0200 @@ -80,7 +80,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 (name ^ "_new_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)) diff -r 5bf2a5c498c2 -r 7ffa0f7e2775 src/HOL/Tools/SMT2/smt2_systems.ML --- a/src/HOL/Tools/SMT2/smt2_systems.ML Wed Jun 11 11:28:46 2014 +0200 +++ b/src/HOL/Tools/SMT2/smt2_systems.ML Wed Jun 11 11:28:46 2014 +0200 @@ -49,7 +49,7 @@ in val cvc3: SMT2_Solver.solver_config = { - name = "cvc3_new", + name = "cvc3", class = K SMTLIB2_Interface.smtlib2C, avail = make_avail "CVC3_NEW", command = make_command "CVC3_NEW", @@ -65,7 +65,7 @@ (* Yices *) val yices: SMT2_Solver.solver_config = { - name = "yices_new", + name = "yices", class = K SMTLIB2_Interface.smtlib2C, avail = make_avail "YICES_NEW", command = make_command "YICES_NEW", @@ -135,7 +135,7 @@ in val z3: SMT2_Solver.solver_config = { - name = "z3_new", + name = "z3", class = select_class, avail = make_avail "Z3_NEW", command = z3_make_command "Z3_NEW", diff -r 5bf2a5c498c2 -r 7ffa0f7e2775 src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Wed Jun 11 11:28:46 2014 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Wed Jun 11 11:28:46 2014 +0200 @@ -29,7 +29,7 @@ (* val cvc3N = "cvc3" *) val yicesN = "yices" -val z3_newN = "z3_new" +val z3N = "z3" val runN = "run" val minN = "min" @@ -212,7 +212,7 @@ (* The first ATP of the list is used by Auto Sledgehammer. Because of the low timeout, it makes sense to put E first. *) fun default_provers_param_value mode ctxt = - [eN, spassN, z3_newN, e_sineN, vampireN, yicesN] + [eN, spassN, z3N, e_sineN, vampireN, yicesN] |> map_filter (remotify_prover_if_not_installed ctxt) (* In "try" mode, leave at least one thread to another slow tool (e.g. Nitpick) *) |> take (Multithreading.max_threads_value () - (if mode = Try then 1 else 0)) diff -r 5bf2a5c498c2 -r 7ffa0f7e2775 src/HOL/Tools/monomorph.ML --- a/src/HOL/Tools/monomorph.ML Wed Jun 11 11:28:46 2014 +0200 +++ b/src/HOL/Tools/monomorph.ML Wed Jun 11 11:28:46 2014 +0200 @@ -61,20 +61,18 @@ fun clear_grounds grounds = Symtab.map (K (K [])) grounds - (* configuration options *) val max_rounds = Attrib.setup_config_int @{binding monomorph_max_rounds} (K 5) val max_new_instances = - Attrib.setup_config_int @{binding monomorph_max_new_instances} (K 300) + Attrib.setup_config_int @{binding monomorph_max_new_instances} (K 500) val max_thm_instances = Attrib.setup_config_int @{binding monomorph_max_thm_instances} (K 20) val max_new_const_instances_per_round = - Attrib.setup_config_int @{binding monomorph_max_new_const_instances_per_round} - (K 5) + Attrib.setup_config_int @{binding monomorph_max_new_const_instances_per_round} (K 5) fun limit_rounds ctxt f = let @@ -83,7 +81,6 @@ in round 1 end - (* theorem information and related functions *) datatype thm_info = @@ -96,17 +93,14 @@ schematics: (string * typ) list, initial_round: int} - fun fold_grounds f = fold (fn Ground thm => f thm | _ => I) - fun fold_schematic f thm_info = (case thm_info of Schematic {id, theorem, tvars, schematics, initial_round} => f id theorem tvars schematics initial_round | _ => I) - fun fold_schematics pred f = let fun apply id thm tvars schematics initial_round x = @@ -114,7 +108,6 @@ in fold (fold_schematic apply) end - (* collecting data *) (* @@ -157,9 +150,9 @@ initial_round = initial_round} in (thm_info, ((id + 1, idx'), consts')) end else (Ground thm, ((id + 1, idx + Thm.maxidx_of thm + 1), consts)) - - in fold_map prep rthms ((0, 0), Symtab.empty) ||> snd end - + in + fold_map prep rthms ((0, 0), Symtab.empty) ||> snd + end (* collecting instances *) @@ -170,7 +163,6 @@ fun cert' subst = Vartab.fold (cons o cert) subst [] in Thm.instantiate (cert' subst, []) end - fun add_new_grounds used_grounds new_grounds thm = let fun mem tab (n, T) = member (op =) (Symtab.lookup_list tab n) T @@ -181,7 +173,6 @@ | add _ = I in Term.fold_aterms add (Thm.prop_of thm) end - fun add_insts max_instances max_thm_insts ctxt round used_grounds new_grounds id thm tvars schematics cx = let @@ -247,13 +238,11 @@ handle ENOUGH cx' => cx' end - fun is_new round initial_round = (round = initial_round) fun is_active round initial_round = (round > initial_round) - -fun find_instances max_instances max_thm_insts max_new_grounds thm_infos ctxt - round (known_grounds, new_grounds0, insts) = +fun find_instances max_instances max_thm_insts max_new_grounds thm_infos ctxt round + (known_grounds, new_grounds0, insts) = let val new_grounds = Symtab.map (fn _ => fn grounds => @@ -271,15 +260,14 @@ (Symtab.empty, insts) |> consider_all (is_active round) (add_new known_grounds new_grounds) |> consider_all (is_new round) (add_new empty_grounds known_grounds') - - in (known_grounds', new_grounds', insts') end - + in + (known_grounds', new_grounds', insts') + end fun add_ground_types thm = let fun add (n, T) = Symtab.map_entry n (insert (op =) T) in Term.fold_aterms (fn Const c => add c | _ => I) (Thm.prop_of thm) end - fun collect_instances ctxt max_thm_insts max_new_grounds thm_infos consts = let val known_grounds = fold_grounds add_ground_types thm_infos consts @@ -294,10 +282,8 @@ end - (* monomorphization *) - fun size_of_subst subst = Vartab.fold (Integer.add o size_of_typ o snd o snd) subst 0