introduced option "z3_with_extensions" to control whether Z3's support for nonlinear arithmetic and datatypes should be enabled (including potential proof reconstruction failures)
--- a/src/HOL/Tools/SMT/smt_config.ML Wed May 30 16:05:21 2012 +0200
+++ b/src/HOL/Tools/SMT/smt_config.ML Wed May 30 23:10:42 2012 +0200
@@ -9,7 +9,7 @@
(*solver*)
type solver_info = {
name: string,
- class: SMT_Utils.class,
+ class: Proof.context -> SMT_Utils.class,
avail: unit -> bool,
options: Proof.context -> string list }
val add_solver: solver_info -> Context.generic -> Context.generic
@@ -61,7 +61,7 @@
type solver_info = {
name: string,
- class: SMT_Utils.class,
+ class: Proof.context -> SMT_Utils.class,
avail: unit -> bool,
options: Proof.context -> string list }
@@ -131,7 +131,8 @@
| (_, NONE) => default ())
fun solver_class_of ctxt =
- solver_info_of no_solver_err (#class o fst o the) ctxt
+ let fun class_of ({class, ...}: solver_info, _) = class ctxt
+ in solver_info_of no_solver_err (class_of o the) ctxt end
fun solver_options_of ctxt =
let
--- a/src/HOL/Tools/SMT/smt_setup_solvers.ML Wed May 30 16:05:21 2012 +0200
+++ b/src/HOL/Tools/SMT/smt_setup_solvers.ML Wed May 30 23:10:42 2012 +0200
@@ -63,7 +63,7 @@
fun mk is_remote = {
name = make_name is_remote "cvc3",
- class = SMTLIB_Interface.smtlibC,
+ class = K SMTLIB_Interface.smtlibC,
avail = make_avail is_remote "CVC3",
command = make_command is_remote "CVC3",
options = cvc3_options,
@@ -85,7 +85,7 @@
fun yices () = {
name = "yices",
- class = SMTLIB_Interface.smtlibC,
+ class = K SMTLIB_Interface.smtlibC,
avail = make_local_avail "YICES",
command = make_local_command "YICES",
options = (fn ctxt => [
@@ -163,9 +163,16 @@
handle SMT_Failure.SMT _ => outcome (swap o split_last)
end
+ val with_extensions =
+ Attrib.setup_config_bool @{binding z3_with_extensions} (K true)
+
+ fun select_class ctxt =
+ if Config.get ctxt with_extensions then Z3_Interface.smtlib_z3C
+ else SMTLIB_Interface.smtlibC
+
fun mk is_remote = {
name = make_name is_remote "z3",
- class = Z3_Interface.smtlib_z3C,
+ class = select_class,
avail = make_avail is_remote "Z3",
command = z3_make_command is_remote "Z3",
options = z3_options,
--- a/src/HOL/Tools/SMT/smt_solver.ML Wed May 30 16:05:21 2012 +0200
+++ b/src/HOL/Tools/SMT/smt_solver.ML Wed May 30 23:10:42 2012 +0200
@@ -10,7 +10,7 @@
datatype outcome = Unsat | Sat | Unknown
type solver_config = {
name: string,
- class: SMT_Utils.class,
+ class: Proof.context -> SMT_Utils.class,
avail: unit -> bool,
command: unit -> string list,
options: Proof.context -> string list,
@@ -146,7 +146,7 @@
type solver_config = {
name: string,
- class: SMT_Utils.class,
+ class: Proof.context -> SMT_Utils.class,
avail: unit -> bool,
command: unit -> string list,
options: Proof.context -> string list,