src/HOL/Library/Old_SMT/old_smt_config.ML
author wenzelm
Wed Jun 17 11:03:05 2015 +0200 (2015-06-17)
changeset 60500 903bb1495239
parent 60312 ee6f9a97205d
child 62519 a564458f94db
permissions -rw-r--r--
isabelle update_cartouches;
blanchet@58058
     1
(*  Title:      HOL/Library/Old_SMT/old_smt_config.ML
boehmes@40424
     2
    Author:     Sascha Boehme, TU Muenchen
boehmes@40424
     3
boehmes@40424
     4
Configuration options and diagnostic tools for SMT.
boehmes@40424
     5
*)
boehmes@40424
     6
blanchet@58058
     7
signature OLD_SMT_CONFIG =
boehmes@40424
     8
sig
boehmes@40424
     9
  (*solver*)
boehmes@41432
    10
  type solver_info = {
boehmes@41432
    11
    name: string,
blanchet@58058
    12
    class: Proof.context -> Old_SMT_Utils.class,
boehmes@41432
    13
    avail: unit -> bool,
boehmes@41432
    14
    options: Proof.context -> string list }
boehmes@41432
    15
  val add_solver: solver_info -> Context.generic -> Context.generic
boehmes@40424
    16
  val set_solver_options: string * string -> Context.generic -> Context.generic
boehmes@46736
    17
  val is_available: Proof.context -> string -> bool
boehmes@41432
    18
  val available_solvers_of: Proof.context -> string list
boehmes@40424
    19
  val select_solver: string -> Context.generic -> Context.generic
boehmes@40424
    20
  val solver_of: Proof.context -> string
blanchet@58058
    21
  val solver_class_of: Proof.context -> Old_SMT_Utils.class
boehmes@40424
    22
  val solver_options_of: Proof.context -> string list
boehmes@40424
    23
boehmes@40424
    24
  (*options*)
boehmes@40424
    25
  val oracle: bool Config.T
boehmes@40424
    26
  val datatypes: bool Config.T
boehmes@40424
    27
  val timeout: real Config.T
boehmes@41121
    28
  val random_seed: int Config.T
blanchet@47152
    29
  val read_only_certificates: bool Config.T
boehmes@40424
    30
  val verbose: bool Config.T
boehmes@40424
    31
  val trace: bool Config.T
boehmes@40424
    32
  val trace_used_facts: bool Config.T
boehmes@40424
    33
  val monomorph_limit: int Config.T
boehmes@41762
    34
  val monomorph_instances: int Config.T
boehmes@41125
    35
  val infer_triggers: bool Config.T
boehmes@40424
    36
  val filter_only_facts: bool Config.T
boehmes@40578
    37
  val debug_files: string Config.T
boehmes@40424
    38
boehmes@40424
    39
  (*tools*)
boehmes@40424
    40
  val with_timeout: Proof.context -> ('a -> 'b) -> 'a -> 'b
boehmes@40424
    41
boehmes@40424
    42
  (*diagnostics*)
boehmes@40424
    43
  val trace_msg: Proof.context -> ('a -> string) -> 'a -> unit
boehmes@40424
    44
  val verbose_msg: Proof.context -> ('a -> string) -> 'a -> unit
boehmes@40424
    45
boehmes@40424
    46
  (*certificates*)
boehmes@40424
    47
  val select_certificates: string -> Context.generic -> Context.generic
boehmes@40424
    48
  val certificates_of: Proof.context -> Cache_IO.cache option
boehmes@40424
    49
boehmes@40424
    50
  (*setup*)
boehmes@40424
    51
  val setup: theory -> theory
boehmes@40424
    52
  val print_setup: Proof.context -> unit
boehmes@40424
    53
end
boehmes@40424
    54
blanchet@58058
    55
structure Old_SMT_Config: OLD_SMT_CONFIG =
boehmes@40424
    56
struct
boehmes@40424
    57
boehmes@40424
    58
(* solver *)
boehmes@40424
    59
boehmes@41432
    60
type solver_info = {
boehmes@41432
    61
  name: string,
blanchet@58058
    62
  class: Proof.context -> Old_SMT_Utils.class,
boehmes@41432
    63
  avail: unit -> bool,
boehmes@41432
    64
  options: Proof.context -> string list }
boehmes@41432
    65
wenzelm@46042
    66
(* FIXME just one data slot (record) per program unit *)
boehmes@40424
    67
structure Solvers = Generic_Data
boehmes@40424
    68
(
boehmes@41432
    69
  type T = (solver_info * string list) Symtab.table * string option
boehmes@40424
    70
  val empty = (Symtab.empty, NONE)
boehmes@40424
    71
  val extend = I
boehmes@41499
    72
  fun merge ((ss1, s1), (ss2, s2)) =
boehmes@41499
    73
    (Symtab.merge (K true) (ss1, ss2), merge_options (s1, s2))
boehmes@40424
    74
)
boehmes@40424
    75
boehmes@40424
    76
fun set_solver_options (name, options) =
boehmes@40424
    77
  let val opts = String.tokens (Symbol.is_ascii_blank o str) options
boehmes@41059
    78
  in Solvers.map (apfst (Symtab.map_entry name (apsnd (K opts)))) end
boehmes@40424
    79
boehmes@41432
    80
fun add_solver (info as {name, ...} : solver_info) context =
boehmes@40424
    81
  if Symtab.defined (fst (Solvers.get context)) name then
boehmes@40424
    82
    error ("Solver already registered: " ^ quote name)
boehmes@40424
    83
  else
boehmes@40424
    84
    context
boehmes@41432
    85
    |> Solvers.map (apfst (Symtab.update (name, (info, []))))
blanchet@58059
    86
    |> Context.map_theory (Attrib.setup (Binding.name ("old_" ^ name ^ "_options"))
wenzelm@46949
    87
        (Scan.lift (@{keyword "="} |-- Args.name) >>
boehmes@40424
    88
          (Thm.declaration_attribute o K o set_solver_options o pair name))
wenzelm@60312
    89
        ("additional command line options for SMT solver " ^ quote name))
boehmes@40424
    90
boehmes@41432
    91
fun all_solvers_of ctxt = Symtab.keys (fst (Solvers.get (Context.Proof ctxt)))
boehmes@41432
    92
boehmes@41432
    93
fun solver_name_of ctxt = snd (Solvers.get (Context.Proof ctxt))
boehmes@41432
    94
boehmes@41432
    95
fun is_available ctxt name =
boehmes@41432
    96
  (case Symtab.lookup (fst (Solvers.get (Context.Proof ctxt))) name of
boehmes@41432
    97
    SOME ({avail, ...}, _) => avail ()
boehmes@41432
    98
  | NONE => false)
boehmes@41432
    99
boehmes@41432
   100
fun available_solvers_of ctxt =
boehmes@41432
   101
  filter (is_available ctxt) (all_solvers_of ctxt)
boehmes@41432
   102
wenzelm@52699
   103
fun warn_solver (Context.Proof ctxt) name =
wenzelm@56294
   104
      if Context_Position.is_visible ctxt then
wenzelm@52699
   105
        warning ("The SMT solver " ^ quote name ^ " is not installed.")
wenzelm@56294
   106
      else ()
wenzelm@52699
   107
  | warn_solver _ _ = ();
boehmes@41432
   108
boehmes@40424
   109
fun select_solver name context =
boehmes@41432
   110
  let
boehmes@41432
   111
    val ctxt = Context.proof_of context
boehmes@41432
   112
    val upd = Solvers.map (apsnd (K (SOME name)))
boehmes@41432
   113
  in
boehmes@41432
   114
    if not (member (op =) (all_solvers_of ctxt) name) then
boehmes@41432
   115
      error ("Trying to select unknown solver: " ^ quote name)
boehmes@41498
   116
    else if not (is_available ctxt name) then
boehmes@41498
   117
      (warn_solver context name; upd context)
boehmes@41432
   118
    else upd context
boehmes@41432
   119
  end
boehmes@40424
   120
boehmes@41059
   121
fun no_solver_err () = error "No SMT solver selected"
boehmes@40424
   122
boehmes@40424
   123
fun solver_of ctxt =
boehmes@41432
   124
  (case solver_name_of ctxt of
boehmes@41432
   125
    SOME name => name
boehmes@41432
   126
  | NONE => no_solver_err ())
boehmes@41432
   127
boehmes@41432
   128
fun solver_info_of default select ctxt =
boehmes@41059
   129
  (case Solvers.get (Context.Proof ctxt) of
boehmes@41432
   130
    (solvers, SOME name) => select (Symtab.lookup solvers name)
boehmes@41432
   131
  | (_, NONE) => default ())
boehmes@41059
   132
boehmes@41059
   133
fun solver_class_of ctxt =
boehmes@48043
   134
  let fun class_of ({class, ...}: solver_info, _) = class ctxt
boehmes@48043
   135
  in solver_info_of no_solver_err (class_of o the) ctxt end
boehmes@40424
   136
boehmes@40424
   137
fun solver_options_of ctxt =
boehmes@41432
   138
  let
boehmes@41432
   139
    fun all_options NONE = []
boehmes@41438
   140
      | all_options (SOME ({options, ...} : solver_info, opts)) =
boehmes@41438
   141
          opts @ options ctxt
boehmes@41432
   142
  in solver_info_of (K []) all_options ctxt end
boehmes@40424
   143
boehmes@40424
   144
val setup_solver =
blanchet@58059
   145
  Attrib.setup @{binding old_smt_solver}
wenzelm@46949
   146
    (Scan.lift (@{keyword "="} |-- Args.name) >>
boehmes@40424
   147
      (Thm.declaration_attribute o K o select_solver))
boehmes@40424
   148
    "SMT solver configuration"
boehmes@40424
   149
boehmes@40424
   150
boehmes@40424
   151
(* options *)
boehmes@40424
   152
blanchet@58059
   153
val oracle = Attrib.setup_config_bool @{binding old_smt_oracle} (K true)
blanchet@58059
   154
val datatypes = Attrib.setup_config_bool @{binding old_smt_datatypes} (K false)
blanchet@58059
   155
val timeout = Attrib.setup_config_real @{binding old_smt_timeout} (K 30.0)
blanchet@58059
   156
val random_seed = Attrib.setup_config_int @{binding old_smt_random_seed} (K 1)
blanchet@58059
   157
val read_only_certificates = Attrib.setup_config_bool @{binding old_smt_read_only_certificates} (K false)
blanchet@58059
   158
val verbose = Attrib.setup_config_bool @{binding old_smt_verbose} (K true)
blanchet@58059
   159
val trace = Attrib.setup_config_bool @{binding old_smt_trace} (K false)
blanchet@58059
   160
val trace_used_facts = Attrib.setup_config_bool @{binding old_smt_trace_used_facts} (K false)
blanchet@58059
   161
val monomorph_limit = Attrib.setup_config_int @{binding old_smt_monomorph_limit} (K 10)
blanchet@58059
   162
val monomorph_instances = Attrib.setup_config_int @{binding old_smt_monomorph_instances} (K 500)
blanchet@58059
   163
val infer_triggers = Attrib.setup_config_bool @{binding old_smt_infer_triggers} (K false)
blanchet@58059
   164
val filter_only_facts = Attrib.setup_config_bool @{binding old_smt_filter_only_facts} (K false)
blanchet@58059
   165
val debug_files = Attrib.setup_config_string @{binding old_smt_debug_files} (K "")
boehmes@40424
   166
boehmes@40424
   167
boehmes@40424
   168
(* diagnostics *)
boehmes@40424
   169
boehmes@40424
   170
fun cond_trace flag f x = if flag then tracing ("SMT: " ^ f x) else ()
boehmes@40424
   171
boehmes@40424
   172
fun verbose_msg ctxt = cond_trace (Config.get ctxt verbose)
boehmes@40424
   173
boehmes@40424
   174
fun trace_msg ctxt = cond_trace (Config.get ctxt trace)
boehmes@40424
   175
boehmes@40424
   176
boehmes@40424
   177
(* tools *)
boehmes@40424
   178
boehmes@40424
   179
fun with_timeout ctxt f x =
boehmes@40424
   180
  TimeLimit.timeLimit (seconds (Config.get ctxt timeout)) f x
blanchet@58058
   181
  handle TimeLimit.TimeOut => raise Old_SMT_Failure.SMT Old_SMT_Failure.Time_Out
boehmes@40424
   182
boehmes@40424
   183
boehmes@40424
   184
(* certificates *)
boehmes@40424
   185
wenzelm@46042
   186
(* FIXME just one data slot (record) per program unit *)
boehmes@40424
   187
structure Certificates = Generic_Data
boehmes@40424
   188
(
boehmes@40424
   189
  type T = Cache_IO.cache option
boehmes@40424
   190
  val empty = NONE
boehmes@40424
   191
  val extend = I
wenzelm@41472
   192
  fun merge (s, _) = s  (* FIXME merge options!? *)
boehmes@40424
   193
)
boehmes@40424
   194
boehmes@40424
   195
val get_certificates_path =
boehmes@40424
   196
  Option.map (Cache_IO.cache_path_of) o Certificates.get o Context.Proof
boehmes@40424
   197
boehmes@40513
   198
fun select_certificates name context = context |> Certificates.put (
boehmes@40424
   199
  if name = "" then NONE
boehmes@40513
   200
  else
boehmes@40513
   201
    Path.explode name
wenzelm@56208
   202
    |> Path.append (Resources.master_directory (Context.theory_of context))
wenzelm@50317
   203
    |> SOME o Cache_IO.unsynchronized_init)
boehmes@40424
   204
boehmes@40424
   205
val certificates_of = Certificates.get o Context.Proof
boehmes@40424
   206
boehmes@40424
   207
val setup_certificates =
blanchet@58059
   208
  Attrib.setup @{binding old_smt_certificates}
wenzelm@46949
   209
    (Scan.lift (@{keyword "="} |-- Args.name) >>
boehmes@40424
   210
      (Thm.declaration_attribute o K o select_certificates))
boehmes@40424
   211
    "SMT certificates configuration"
boehmes@40424
   212
boehmes@40424
   213
boehmes@40424
   214
(* setup *)
boehmes@40424
   215
boehmes@40424
   216
val setup =
boehmes@40424
   217
  setup_solver #>
boehmes@40424
   218
  setup_certificates
boehmes@40424
   219
boehmes@40424
   220
fun print_setup ctxt =
boehmes@40424
   221
  let
boehmes@40424
   222
    fun string_of_bool b = if b then "true" else "false"
boehmes@40424
   223
boehmes@41432
   224
    val names = available_solvers_of ctxt
boehmes@40424
   225
    val ns = if null names then ["(none)"] else sort_strings names
boehmes@41432
   226
    val n = the_default "(none)" (solver_name_of ctxt)
boehmes@40424
   227
    val opts = solver_options_of ctxt
boehmes@40424
   228
    
boehmes@40424
   229
    val t = string_of_real (Config.get ctxt timeout)
boehmes@40424
   230
boehmes@40424
   231
    val certs_filename =
boehmes@40424
   232
      (case get_certificates_path ctxt of
wenzelm@41944
   233
        SOME path => Path.print path
boehmes@40424
   234
      | NONE => "(disabled)")
boehmes@40424
   235
  in
boehmes@40424
   236
    Pretty.writeln (Pretty.big_list "SMT setup:" [
boehmes@40424
   237
      Pretty.str ("Current SMT solver: " ^ n),
boehmes@40424
   238
      Pretty.str ("Current SMT solver options: " ^ space_implode " " opts),
boehmes@40424
   239
      Pretty.str_list "Available SMT solvers: "  "" ns,
boehmes@40424
   240
      Pretty.str ("Current timeout: " ^ t ^ " seconds"),
boehmes@40424
   241
      Pretty.str ("With proofs: " ^
boehmes@40424
   242
        string_of_bool (not (Config.get ctxt oracle))),
boehmes@40424
   243
      Pretty.str ("Certificates cache: " ^ certs_filename),
boehmes@40424
   244
      Pretty.str ("Fixed certificates: " ^
blanchet@47152
   245
        string_of_bool (Config.get ctxt read_only_certificates))])
boehmes@40424
   246
  end
boehmes@40424
   247
boehmes@40424
   248
val _ =
wenzelm@59936
   249
  Outer_Syntax.command @{command_keyword old_smt_status}
wenzelm@46961
   250
    "show the available SMT solvers, the currently selected SMT solver, \
wenzelm@46961
   251
    \and the values of SMT configuration options"
wenzelm@51658
   252
    (Scan.succeed (Toplevel.keep (print_setup o Toplevel.context_of)))
boehmes@40424
   253
boehmes@40424
   254
end