# HG changeset patch
# User boehmes
# Date 1338412242 -7200
# Node ID 3ff2c76c9f641142a53210610e515783a0d1e3d8
# Parent  918a92d4079f94b56e055687fe7fd464afdc857b
introduced option "z3_with_extensions" to control whether Z3's support for nonlinear arithmetic and datatypes should be enabled (including potential proof reconstruction failures)

diff -r 918a92d4079f -r 3ff2c76c9f64 src/HOL/Tools/SMT/smt_config.ML
--- 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
diff -r 918a92d4079f -r 3ff2c76c9f64 src/HOL/Tools/SMT/smt_setup_solvers.ML
--- 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,
diff -r 918a92d4079f -r 3ff2c76c9f64 src/HOL/Tools/SMT/smt_solver.ML
--- 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,