src/HOL/Library/SMT/smt_config.ML

+(*  Title:      HOL/Library/SMT/smt_config.ML
+    Author:     Sascha Boehme, TU Muenchen
+
+Configuration options and diagnostic tools for SMT.
+*)
+
+signature SMT_CONFIG =
+sig
+  (*solver*)
+  type solver_info = {
+    name: string,
+    class: Proof.context -> SMT_Utils.class,
+    avail: unit -> bool,
+    options: Proof.context -> string list }
+  val add_solver: solver_info -> Context.generic -> Context.generic
+  val set_solver_options: string * string -> Context.generic -> Context.generic
+  val is_available: Proof.context -> string -> bool
+  val available_solvers_of: Proof.context -> string list
+  val select_solver: string -> Context.generic -> Context.generic
+  val solver_of: Proof.context -> string
+  val solver_class_of: Proof.context -> SMT_Utils.class
+  val solver_options_of: Proof.context -> string list
+
+  (*options*)
+  val oracle: bool Config.T
+  val datatypes: bool Config.T
+  val timeout: real Config.T
+  val random_seed: int Config.T
+  val read_only_certificates: bool Config.T
+  val verbose: bool Config.T
+  val trace: bool Config.T
+  val trace_used_facts: bool Config.T
+  val monomorph_limit: int Config.T
+  val monomorph_instances: int Config.T
+  val infer_triggers: bool Config.T
+  val filter_only_facts: bool Config.T
+  val debug_files: string Config.T
+
+  (*tools*)
+  val with_timeout: Proof.context -> ('a -> 'b) -> 'a -> 'b
+
+  (*diagnostics*)
+  val trace_msg: Proof.context -> ('a -> string) -> 'a -> unit
+  val verbose_msg: Proof.context -> ('a -> string) -> 'a -> unit
+
+  (*certificates*)
+  val select_certificates: string -> Context.generic -> Context.generic
+  val certificates_of: Proof.context -> Cache_IO.cache option
+
+  (*setup*)
+  val setup: theory -> theory
+  val print_setup: Proof.context -> unit
+end
+
+structure SMT_Config: SMT_CONFIG =
+struct
+
+(* solver *)
+
+type solver_info = {
+  name: string,
+  class: Proof.context -> SMT_Utils.class,
+  avail: unit -> bool,
+  options: Proof.context -> string list }
+
+(* FIXME just one data slot (record) per program unit *)
+structure Solvers = Generic_Data
+(
+  type T = (solver_info * string list) Symtab.table * string option
+  val empty = (Symtab.empty, NONE)
+  val extend = I
+  fun merge ((ss1, s1), (ss2, s2)) =
+    (Symtab.merge (K true) (ss1, ss2), merge_options (s1, s2))
+)
+
+fun set_solver_options (name, options) =
+  let val opts = String.tokens (Symbol.is_ascii_blank o str) options
+  in Solvers.map (apfst (Symtab.map_entry name (apsnd (K opts)))) end
+
+fun add_solver (info as {name, ...} : solver_info) context =
+  if Symtab.defined (fst (Solvers.get context)) name then
+    error ("Solver already registered: " ^ quote name)
+  else
+    context
+    |> Solvers.map (apfst (Symtab.update (name, (info, []))))
+    |> Context.map_theory (Attrib.setup (Binding.name (name ^ "_options"))
+        (Scan.lift (@{keyword "="} |-- Args.name) >>
+          (Thm.declaration_attribute o K o set_solver_options o pair name))
+        ("Additional command line options for SMT solver " ^ quote name))
+
+fun all_solvers_of ctxt = Symtab.keys (fst (Solvers.get (Context.Proof ctxt)))
+
+fun solver_name_of ctxt = snd (Solvers.get (Context.Proof ctxt))
+
+fun is_available ctxt name =
+  (case Symtab.lookup (fst (Solvers.get (Context.Proof ctxt))) name of
+    SOME ({avail, ...}, _) => avail ()
+  | NONE => false)
+
+fun available_solvers_of ctxt =
+  filter (is_available ctxt) (all_solvers_of ctxt)
+
+fun warn_solver (Context.Proof ctxt) name =
+      if Context_Position.is_visible ctxt then
+        warning ("The SMT solver " ^ quote name ^ " is not installed.")
+      else ()
+  | warn_solver _ _ = ();
+
+fun select_solver name context =
+  let
+    val ctxt = Context.proof_of context
+    val upd = Solvers.map (apsnd (K (SOME name)))
+  in
+    if not (member (op =) (all_solvers_of ctxt) name) then
+      error ("Trying to select unknown solver: " ^ quote name)
+    else if not (is_available ctxt name) then
+      (warn_solver context name; upd context)
+    else upd context
+  end
+
+fun no_solver_err () = error "No SMT solver selected"
+
+fun solver_of ctxt =
+  (case solver_name_of ctxt of
+    SOME name => name
+  | NONE => no_solver_err ())
+
+fun solver_info_of default select ctxt =
+  (case Solvers.get (Context.Proof ctxt) of
+    (solvers, SOME name) => select (Symtab.lookup solvers name)
+  | (_, NONE) => default ())
+
+fun solver_class_of 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
+    fun all_options NONE = []
+      | all_options (SOME ({options, ...} : solver_info, opts)) =
+          opts @ options ctxt
+  in solver_info_of (K []) all_options ctxt end
+
+val setup_solver =
+  Attrib.setup @{binding smt_solver}
+    (Scan.lift (@{keyword "="} |-- Args.name) >>
+      (Thm.declaration_attribute o K o select_solver))
+    "SMT solver configuration"
+
+
+(* options *)
+
+val oracle = Attrib.setup_config_bool @{binding smt_oracle} (K true)
+val datatypes = Attrib.setup_config_bool @{binding smt_datatypes} (K false)
+val timeout = Attrib.setup_config_real @{binding smt_timeout} (K 30.0)
+val random_seed = Attrib.setup_config_int @{binding smt_random_seed} (K 1)
+val read_only_certificates = Attrib.setup_config_bool @{binding smt_read_only_certificates} (K false)
+val verbose = Attrib.setup_config_bool @{binding smt_verbose} (K true)
+val trace = Attrib.setup_config_bool @{binding smt_trace} (K false)
+val trace_used_facts = Attrib.setup_config_bool @{binding smt_trace_used_facts} (K false)
+val monomorph_limit = Attrib.setup_config_int @{binding smt_monomorph_limit} (K 10)
+val monomorph_instances = Attrib.setup_config_int @{binding smt_monomorph_instances} (K 500)
+val infer_triggers = Attrib.setup_config_bool @{binding smt_infer_triggers} (K false)
+val filter_only_facts = Attrib.setup_config_bool @{binding smt_filter_only_facts} (K false)
+val debug_files = Attrib.setup_config_string @{binding smt_debug_files} (K "")
+
+
+(* diagnostics *)
+
+fun cond_trace flag f x = if flag then tracing ("SMT: " ^ f x) else ()
+
+fun verbose_msg ctxt = cond_trace (Config.get ctxt verbose)
+
+fun trace_msg ctxt = cond_trace (Config.get ctxt trace)
+
+
+(* tools *)
+
+fun with_timeout ctxt f x =
+  TimeLimit.timeLimit (seconds (Config.get ctxt timeout)) f x
+  handle TimeLimit.TimeOut => raise SMT_Failure.SMT SMT_Failure.Time_Out
+
+
+(* certificates *)
+
+(* FIXME just one data slot (record) per program unit *)
+structure Certificates = Generic_Data
+(
+  type T = Cache_IO.cache option
+  val empty = NONE
+  val extend = I
+  fun merge (s, _) = s  (* FIXME merge options!? *)
+)
+
+val get_certificates_path =
+  Option.map (Cache_IO.cache_path_of) o Certificates.get o Context.Proof
+
+fun select_certificates name context = context |> Certificates.put (
+  if name = "" then NONE
+  else
+    Path.explode name
+    |> Path.append (Resources.master_directory (Context.theory_of context))
+    |> SOME o Cache_IO.unsynchronized_init)
+
+val certificates_of = Certificates.get o Context.Proof
+
+val setup_certificates =
+  Attrib.setup @{binding smt_certificates}
+    (Scan.lift (@{keyword "="} |-- Args.name) >>
+      (Thm.declaration_attribute o K o select_certificates))
+    "SMT certificates configuration"
+
+
+(* setup *)
+
+val setup =
+  setup_solver #>
+  setup_certificates
+
+fun print_setup ctxt =
+  let
+    fun string_of_bool b = if b then "true" else "false"
+
+    val names = available_solvers_of ctxt
+    val ns = if null names then ["(none)"] else sort_strings names
+    val n = the_default "(none)" (solver_name_of ctxt)
+    val opts = solver_options_of ctxt
+    
+    val t = string_of_real (Config.get ctxt timeout)
+
+    val certs_filename =
+      (case get_certificates_path ctxt of
+        SOME path => Path.print path
+      | NONE => "(disabled)")
+  in
+    Pretty.writeln (Pretty.big_list "SMT setup:" [
+      Pretty.str ("Current SMT solver: " ^ n),
+      Pretty.str ("Current SMT solver options: " ^ space_implode " " opts),
+      Pretty.str_list "Available SMT solvers: "  "" ns,
+      Pretty.str ("Current timeout: " ^ t ^ " seconds"),
+      Pretty.str ("With proofs: " ^
+        string_of_bool (not (Config.get ctxt oracle))),
+      Pretty.str ("Certificates cache: " ^ certs_filename),
+      Pretty.str ("Fixed certificates: " ^
+        string_of_bool (Config.get ctxt read_only_certificates))])
+  end
+
+val _ =
+  Outer_Syntax.improper_command @{command_spec "smt_status"}
+    "show the available SMT solvers, the currently selected SMT solver, \
+    \and the values of SMT configuration options"
+    (Scan.succeed (Toplevel.keep (print_setup o Toplevel.context_of)))
+
+end