# HG changeset patch
# User fleury <Mathias.Fleury@mpi-inf.mpg.de>
# Date 1637158150 -3600
# Node ID 1fd8705503b4b197ea695f89d6f737a3738281c8
# Parent  1e7bb95c75e73d07726d77f0bb8160ca566276c5
generate problems with correct logic for veriT

diff -r 1e7bb95c75e7 -r 1fd8705503b4 src/HOL/Library/Tools/smt_word.ML
--- 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>
 
diff -r 1e7bb95c75e7 -r 1fd8705503b4 src/HOL/Tools/SMT/cvc4_interface.ML
--- 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
diff -r 1e7bb95c75e7 -r 1fd8705503b4 src/HOL/Tools/SMT/smt_config.ML
--- 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 "")
diff -r 1e7bb95c75e7 -r 1fd8705503b4 src/HOL/Tools/SMT/smt_real.ML
--- 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
diff -r 1e7bb95c75e7 -r 1fd8705503b4 src/HOL/Tools/SMT/smt_solver.ML
--- 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
 
diff -r 1e7bb95c75e7 -r 1fd8705503b4 src/HOL/Tools/SMT/smt_systems.ML
--- 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 = {
diff -r 1e7bb95c75e7 -r 1fd8705503b4 src/HOL/Tools/SMT/smt_translate.ML
--- 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
diff -r 1e7bb95c75e7 -r 1fd8705503b4 src/HOL/Tools/SMT/smtlib_interface.ML
--- 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 *)
diff -r 1e7bb95c75e7 -r 1fd8705503b4 src/HOL/Tools/SMT/verit_proof.ML
--- 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 {
diff -r 1e7bb95c75e7 -r 1fd8705503b4 src/HOL/Tools/SMT/z3_interface.ML
--- 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)}