# 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,