--- a/src/HOL/Library/Tools/smt_word.ML Wed Nov 17 17:11:57 2021 +0100
+++ b/src/HOL/Library/Tools/smt_word.ML Wed Nov 17 15:09:10 2021 +0100
@@ -19,14 +19,17 @@
(* "QF_AUFBV" is too restrictive for Isabelle's problems, which contain aritmetic and quantifiers.
Better set the logic to "" and make at least Z3 happy. *)
-fun smtlib_logic ts =
- if exists (Term.exists_type (Term.exists_subtype is_wordT)) ts then SOME "" else NONE
+fun smtlib_logic "z3" ts =
+ if exists (Term.exists_type (Term.exists_subtype is_wordT)) ts then SOME "" else NONE
+ | smtlib_logic "verit" _ = NONE
+ | smtlib_logic _ ts =
+ if exists (Term.exists_type (Term.exists_subtype is_wordT)) ts then SOME "AUFBVLIRA" else NONE
(* SMT-LIB builtins *)
local
- val smtlibC = SMTLIB_Interface.smtlibC
+ val smtlibC = SMTLIB_Interface.smtlibC @ SMTLIB_Interface.bvsmlibC
val wordT = \<^typ>\<open>'a::len word\<close>
--- a/src/HOL/Tools/SMT/cvc4_interface.ML Wed Nov 17 17:11:57 2021 +0100
+++ b/src/HOL/Tools/SMT/cvc4_interface.ML Wed Nov 17 15:09:10 2021 +0100
@@ -23,7 +23,7 @@
local
fun translate_config order ctxt =
{order = order,
- logic = K "(set-logic ALL_SUPPORTED)\n",
+ logic = K (K "(set-logic ALL_SUPPORTED)\n"),
fp_kinds = [BNF_Util.Least_FP, BNF_Util.Greatest_FP],
serialize = #serialize (SMTLIB_Interface.translate_config order ctxt)}
in
--- a/src/HOL/Tools/SMT/smt_config.ML Wed Nov 17 17:11:57 2021 +0100
+++ b/src/HOL/Tools/SMT/smt_config.ML Wed Nov 17 15:09:10 2021 +0100
@@ -34,6 +34,7 @@
val monomorph_instances: int Config.T
val explicit_application: int Config.T
val higher_order: bool Config.T
+ val native_bv: bool Config.T
val nat_as_int: bool Config.T
val infer_triggers: bool Config.T
val debug_files: string Config.T
@@ -194,6 +195,7 @@
val monomorph_instances = Attrib.setup_config_int \<^binding>\<open>smt_monomorph_instances\<close> (K 500)
val explicit_application = Attrib.setup_config_int \<^binding>\<open>smt_explicit_application\<close> (K 1)
val higher_order = Attrib.setup_config_bool \<^binding>\<open>smt_higher_order\<close> (K false)
+val native_bv = Attrib.setup_config_bool \<^binding>\<open>native_bv\<close> (K true)
val nat_as_int = Attrib.setup_config_bool \<^binding>\<open>smt_nat_as_int\<close> (K false)
val infer_triggers = Attrib.setup_config_bool \<^binding>\<open>smt_infer_triggers\<close> (K false)
val debug_files = Attrib.setup_config_string \<^binding>\<open>smt_debug_files\<close> (K "")
--- a/src/HOL/Tools/SMT/smt_real.ML Wed Nov 17 17:11:57 2021 +0100
+++ b/src/HOL/Tools/SMT/smt_real.ML Wed Nov 17 15:09:10 2021 +0100
@@ -10,7 +10,7 @@
(* SMT-LIB logic *)
-fun smtlib_logic ts =
+fun smtlib_logic _ ts =
if exists (Term.exists_type (Term.exists_subtype (equal \<^typ>\<open>real\<close>))) ts
then SOME "AUFLIRA"
else NONE
--- a/src/HOL/Tools/SMT/smt_solver.ML Wed Nov 17 17:11:57 2021 +0100
+++ b/src/HOL/Tools/SMT/smt_solver.ML Wed Nov 17 15:09:10 2021 +0100
@@ -132,7 +132,7 @@
val (str, replay_data as {context = ctxt', ...}) =
ithms
|> tap (trace_assms ctxt)
- |> SMT_Translate.translate ctxt smt_options comments
+ |> SMT_Translate.translate ctxt name smt_options comments
||> tap trace_replay_data
in (run_solver ctxt' name (make_command command options) str, replay_data) end
--- a/src/HOL/Tools/SMT/smt_systems.ML Wed Nov 17 17:11:57 2021 +0100
+++ b/src/HOL/Tools/SMT/smt_systems.ML Wed Nov 17 15:09:10 2021 +0100
@@ -77,6 +77,8 @@
else
if Config.get ctxt SMT_Config.higher_order then
SMTLIB_Interface.hosmtlibC
+ else if Config.get ctxt SMT_Config.native_bv then
+ SMTLIB_Interface.bvsmlibC
else
SMTLIB_Interface.smtlibC
in
@@ -147,7 +149,9 @@
["-smt2"]
fun select_class ctxt =
- if Config.get ctxt z3_extensions then Z3_Interface.smtlib_z3C else SMTLIB_Interface.smtlibC
+ if Config.get ctxt z3_extensions then Z3_Interface.smtlib_z3C
+ else if Config.get ctxt SMT_Config.native_bv then SMTLIB_Interface.bvsmlibC
+ else SMTLIB_Interface.smtlibC
in
val z3: SMT_Solver.solver_config = {
--- a/src/HOL/Tools/SMT/smt_translate.ML Wed Nov 17 17:11:57 2021 +0100
+++ b/src/HOL/Tools/SMT/smt_translate.ML Wed Nov 17 15:09:10 2021 +0100
@@ -22,7 +22,7 @@
funcs: (string * (string list * string)) list }
type config = {
order: SMT_Util.order,
- logic: term list -> string,
+ logic: string -> term list -> string,
fp_kinds: BNF_Util.fp_kind list,
serialize: (string * string) list -> string list -> sign -> sterm list -> string }
type replay_data = {
@@ -35,7 +35,7 @@
(*translation*)
val add_config: SMT_Util.class * (Proof.context -> config) -> Context.generic -> Context.generic
- val translate: Proof.context -> (string * string) list -> string list -> (int * thm) list ->
+ val translate: Proof.context -> string -> (string * string) list -> string list -> (int * thm) list ->
string * replay_data
end;
@@ -66,7 +66,7 @@
type config = {
order: SMT_Util.order,
- logic: term list -> string,
+ logic: string -> term list -> string,
fp_kinds: BNF_Util.fp_kind list,
serialize: (string * string) list -> string list -> sign -> sterm list -> string }
@@ -487,7 +487,7 @@
"for solver class " ^ quote (SMT_Util.string_of_class cs)))
end
-fun translate ctxt smt_options comments ithms =
+fun translate ctxt prover smt_options comments ithms =
let
val {order, logic, fp_kinds, serialize} = get_config ctxt
@@ -529,7 +529,7 @@
|>> order = SMT_Util.First_Order ? apfst (cons fun_app_eq)
in
(ts4, tr_context)
- |-> intermediate logic dtyps (builtin SMT_Builtin.dest_builtin) ctxt2
+ |-> intermediate (logic prover) dtyps (builtin SMT_Builtin.dest_builtin) ctxt2
|>> uncurry (serialize smt_options comments)
||> replay_data_of ctxt2 ll_defs rewrite_rules ithms
end
--- a/src/HOL/Tools/SMT/smtlib_interface.ML Wed Nov 17 17:11:57 2021 +0100
+++ b/src/HOL/Tools/SMT/smtlib_interface.ML Wed Nov 17 15:09:10 2021 +0100
@@ -9,7 +9,9 @@
sig
val smtlibC: SMT_Util.class
val hosmtlibC: SMT_Util.class
- val add_logic: int * (term list -> string option) -> Context.generic -> Context.generic
+ val bvsmlibC: SMT_Util.class
+ val add_logic: int * (string -> term list -> string option) -> Context.generic -> Context.generic
+ val del_logic: int * (string -> term list -> string option) -> Context.generic -> Context.generic
val translate_config: SMT_Util.order -> Proof.context -> SMT_Translate.config
val assert_name_of_index: int -> string
val assert_index_of_name: string -> int
@@ -23,7 +25,7 @@
val smtlibC = ["smtlib"] (* SMT-LIB 2 *)
val hosmtlibC = smtlibC @ hoC (* possibly SMT-LIB 3 *)
-
+val bvsmlibC = smtlibC @ ["BV"] (* if BV are supported *)
(* builtins *)
@@ -73,17 +75,18 @@
structure Logics = Generic_Data
(
- type T = (int * (term list -> string option)) list
+ type T = (int * (string -> term list -> string option)) list
val empty = []
fun merge data = Ord_List.merge fst_int_ord data
)
fun add_logic pf = Logics.map (Ord_List.insert fst_int_ord pf)
+fun del_logic pf = Logics.map (Ord_List.remove fst_int_ord pf)
-fun choose_logic ctxt ts =
+fun choose_logic ctxt prover ts =
let
fun choose [] = "AUFLIA"
- | choose ((_, f) :: fs) = (case f ts of SOME s => s | NONE => choose fs)
+ | choose ((_, f) :: fs) = (case f prover ts of SOME s => s | NONE => choose fs)
in
(case choose (Logics.get (Context.Proof ctxt)) of
"" => "" (* for default Z3 logic, a subset of everything *)
--- a/src/HOL/Tools/SMT/verit_proof.ML Wed Nov 17 17:11:57 2021 +0100
+++ b/src/HOL/Tools/SMT/verit_proof.ML Wed Nov 17 15:09:10 2021 +0100
@@ -174,7 +174,8 @@
map fst strategies
end
-fun verit_tac ctxt = SMT_Solver.smt_tac (Context.proof_map (SMT_Config.select_solver "verit") ctxt)
+val select_verit = SMT_Config.select_solver "verit"
+fun verit_tac ctxt = SMT_Solver.smt_tac (Config.put SMT_Config.native_bv false ((Context.proof_map select_verit ctxt)))
fun verit_tac_stgy stgy ctxt = verit_tac (Context.proof_of (select_veriT_stgy stgy (Context.Proof ctxt)))
datatype raw_veriT_node = Raw_VeriT_Node of {
--- a/src/HOL/Tools/SMT/z3_interface.ML Wed Nov 17 17:11:57 2021 +0100
+++ b/src/HOL/Tools/SMT/z3_interface.ML Wed Nov 17 15:09:10 2021 +0100
@@ -26,7 +26,7 @@
val z3C = ["z3"]
-val smtlib_z3C = SMTLIB_Interface.smtlibC @ z3C
+val smtlib_z3C = SMTLIB_Interface.smtlibC @ SMTLIB_Interface.bvsmlibC @ z3C
(* interface *)
@@ -34,7 +34,7 @@
local
fun translate_config ctxt =
{order = SMT_Util.First_Order,
- logic = K "",
+ logic = K (K ""),
fp_kinds = [BNF_Util.Least_FP],
serialize = #serialize (SMTLIB_Interface.translate_config SMT_Util.First_Order ctxt)}