--- 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 *}
--- 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))
--- 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",
--- 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))
--- 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