--- a/src/HOL/Tools/SMT/smt_systems.ML Tue Aug 29 16:24:14 2017 +0200
+++ b/src/HOL/Tools/SMT/smt_systems.ML Tue Aug 29 18:30:23 2017 +0200
@@ -62,6 +62,7 @@
end
+
(* CVC4 *)
val cvc4_extensions = Attrib.setup_config_bool @{binding cvc4_extensions} (K false)
@@ -75,8 +76,16 @@
"--tlimit", string_of_int (Real.ceil (1000.0 * Config.get ctxt SMT_Config.timeout))]
fun select_class ctxt =
- if Config.get ctxt cvc4_extensions then CVC4_Interface.smtlib_cvc4C
- else SMTLIB_Interface.smtlibC
+ if Config.get ctxt cvc4_extensions then
+ if Config.get ctxt SMT_Config.higher_order then
+ CVC4_Interface.hosmtlib_cvc4C
+ else
+ CVC4_Interface.smtlib_cvc4C
+ else
+ if Config.get ctxt SMT_Config.higher_order then
+ SMTLIB_Interface.hosmtlibC
+ else
+ SMTLIB_Interface.smtlibC
in
val cvc4: SMT_Solver.solver_config = {
@@ -93,11 +102,20 @@
end
+
(* veriT *)
+local
+ fun select_class ctxt =
+ if Config.get ctxt SMT_Config.higher_order then
+ SMTLIB_Interface.hosmtlibC
+ else
+ SMTLIB_Interface.smtlibC
+in
+
val veriT: SMT_Solver.solver_config = {
name = "verit",
- class = K SMTLIB_Interface.smtlibC,
+ class = select_class,
avail = make_avail "VERIT",
command = make_command "VERIT",
options = (fn ctxt => [
@@ -113,6 +131,9 @@
parse_proof = SOME (K VeriT_Proof_Parse.parse_proof),
replay = NONE }
+end
+
+
(* Z3 *)
val z3_extensions = Attrib.setup_config_bool @{binding z3_extensions} (K false)