src/HOL/Tools/SMT/smt_config.ML
author wenzelm
Sun Nov 26 21:08:32 2017 +0100 (18 months ago)
changeset 67091 1393c2340eec
parent 66738 793e7a9c30c5
child 67149 e61557884799
permissions -rw-r--r--
more symbols;
blanchet@58061
     1
(*  Title:      HOL/Tools/SMT/smt_config.ML
blanchet@56078
     2
    Author:     Sascha Boehme, TU Muenchen
blanchet@56078
     3
blanchet@56078
     4
Configuration options and diagnostic tools for SMT.
blanchet@56078
     5
*)
blanchet@56078
     6
blanchet@58061
     7
signature SMT_CONFIG =
blanchet@56078
     8
sig
blanchet@56078
     9
  (*solver*)
blanchet@56078
    10
  type solver_info = {
blanchet@56078
    11
    name: string,
blanchet@58061
    12
    class: Proof.context -> SMT_Util.class,
blanchet@56078
    13
    avail: unit -> bool,
blanchet@56078
    14
    options: Proof.context -> string list }
blanchet@56078
    15
  val add_solver: solver_info -> Context.generic -> Context.generic
blanchet@56078
    16
  val set_solver_options: string * string -> Context.generic -> Context.generic
blanchet@56078
    17
  val is_available: Proof.context -> string -> bool
blanchet@56078
    18
  val available_solvers_of: Proof.context -> string list
blanchet@56078
    19
  val select_solver: string -> Context.generic -> Context.generic
blanchet@56078
    20
  val solver_of: Proof.context -> string
blanchet@58061
    21
  val solver_class_of: Proof.context -> SMT_Util.class
blanchet@56078
    22
  val solver_options_of: Proof.context -> string list
blanchet@56078
    23
blanchet@56078
    24
  (*options*)
blanchet@56078
    25
  val oracle: bool Config.T
blanchet@56078
    26
  val timeout: real Config.T
boehmes@59213
    27
  val reconstruction_step_timeout: real Config.T
blanchet@56078
    28
  val random_seed: int Config.T
blanchet@56078
    29
  val read_only_certificates: bool Config.T
blanchet@56078
    30
  val verbose: bool Config.T
blanchet@56078
    31
  val trace: bool Config.T
boehmes@59215
    32
  val statistics: bool Config.T
blanchet@56078
    33
  val monomorph_limit: int Config.T
blanchet@56078
    34
  val monomorph_instances: int Config.T
blanchet@66738
    35
  val explicit_application: int Config.T
blanchet@66551
    36
  val higher_order: bool Config.T
blanchet@66298
    37
  val nat_as_int: bool Config.T
blanchet@56078
    38
  val infer_triggers: bool Config.T
blanchet@56078
    39
  val debug_files: string Config.T
boehmes@56816
    40
  val sat_solver: string Config.T
blanchet@56078
    41
blanchet@56078
    42
  (*tools*)
boehmes@59213
    43
  val with_time_limit: Proof.context -> real Config.T -> ('a -> 'b) -> 'a -> 'b
blanchet@56078
    44
  val with_timeout: Proof.context -> ('a -> 'b) -> 'a -> 'b
blanchet@56078
    45
blanchet@56078
    46
  (*diagnostics*)
blanchet@56078
    47
  val trace_msg: Proof.context -> ('a -> string) -> 'a -> unit
blanchet@56078
    48
  val verbose_msg: Proof.context -> ('a -> string) -> 'a -> unit
boehmes@59215
    49
  val statistics_msg: Proof.context -> ('a -> string) -> 'a -> unit
blanchet@56078
    50
blanchet@56078
    51
  (*certificates*)
blanchet@56078
    52
  val select_certificates: string -> Context.generic -> Context.generic
blanchet@56078
    53
  val certificates_of: Proof.context -> Cache_IO.cache option
blanchet@56078
    54
blanchet@56078
    55
  (*setup*)
blanchet@56078
    56
  val print_setup: Proof.context -> unit
blanchet@57229
    57
end;
blanchet@56078
    58
blanchet@58061
    59
structure SMT_Config: SMT_CONFIG =
blanchet@56078
    60
struct
blanchet@56078
    61
blanchet@56078
    62
(* solver *)
blanchet@56078
    63
blanchet@56078
    64
type solver_info = {
blanchet@56078
    65
  name: string,
blanchet@58061
    66
  class: Proof.context -> SMT_Util.class,
blanchet@56078
    67
  avail: unit -> bool,
blanchet@56090
    68
  options: Proof.context -> string list}
blanchet@56078
    69
boehmes@59214
    70
type data = {
boehmes@59214
    71
  solvers: (solver_info * string list) Symtab.table,
boehmes@59214
    72
  solver: string option,
boehmes@59214
    73
  certs: Cache_IO.cache option}
boehmes@59214
    74
boehmes@59214
    75
fun mk_data solvers solver certs: data = {solvers=solvers, solver=solver, certs=certs}
boehmes@59214
    76
boehmes@59214
    77
val empty_data = mk_data Symtab.empty NONE NONE
boehmes@59214
    78
boehmes@59214
    79
fun solvers_of ({solvers, ...}: data) = solvers
boehmes@59214
    80
fun solver_of ({solver, ...}: data) = solver
boehmes@59214
    81
fun certs_of ({certs, ...}: data) = certs
boehmes@59214
    82
boehmes@59214
    83
fun map_solvers f ({solvers, solver, certs}: data) = mk_data (f solvers) solver certs
boehmes@59214
    84
fun map_solver f ({solvers, solver, certs}: data) = mk_data solvers (f solver) certs
boehmes@59214
    85
fun put_certs c ({solvers, solver, ...}: data) = mk_data solvers solver c
boehmes@59214
    86
boehmes@59214
    87
fun merge_data ({solvers=ss1,solver=s1,certs=c1}: data, {solvers=ss2,solver=s2,certs=c2}: data) =
boehmes@59214
    88
  mk_data (Symtab.merge (K true) (ss1, ss2)) (merge_options (s1, s2)) (merge_options (c1, c2))
boehmes@59214
    89
boehmes@59214
    90
structure Data = Generic_Data
blanchet@56078
    91
(
boehmes@59214
    92
  type T = data
boehmes@59214
    93
  val empty = empty_data
blanchet@56078
    94
  val extend = I
boehmes@59214
    95
  val merge = merge_data
blanchet@56078
    96
)
blanchet@56078
    97
blanchet@56078
    98
fun set_solver_options (name, options) =
blanchet@56078
    99
  let val opts = String.tokens (Symbol.is_ascii_blank o str) options
boehmes@59214
   100
  in Data.map (map_solvers (Symtab.map_entry name (apsnd (K opts)))) end
blanchet@56078
   101
blanchet@56078
   102
fun add_solver (info as {name, ...} : solver_info) context =
boehmes@59214
   103
  if Symtab.defined (solvers_of (Data.get context)) name then
blanchet@56078
   104
    error ("Solver already registered: " ^ quote name)
blanchet@56078
   105
  else
blanchet@56078
   106
    context
boehmes@59214
   107
    |> Data.map (map_solvers (Symtab.update (name, (info, []))))
blanchet@58061
   108
    |> Context.map_theory (Attrib.setup (Binding.name (name ^ "_options"))
blanchet@56078
   109
        (Scan.lift (@{keyword "="} |-- Args.name) >>
blanchet@56078
   110
          (Thm.declaration_attribute o K o set_solver_options o pair name))
wenzelm@60312
   111
        ("additional command line options for SMT solver " ^ quote name))
blanchet@56078
   112
boehmes@59214
   113
fun all_solvers_of ctxt = Symtab.keys (solvers_of (Data.get (Context.Proof ctxt)))
blanchet@56078
   114
boehmes@59214
   115
fun solver_name_of ctxt = solver_of (Data.get (Context.Proof ctxt))
blanchet@56078
   116
blanchet@56078
   117
fun is_available ctxt name =
boehmes@59214
   118
  (case Symtab.lookup (solvers_of (Data.get (Context.Proof ctxt))) name of
blanchet@56078
   119
    SOME ({avail, ...}, _) => avail ()
blanchet@56078
   120
  | NONE => false)
blanchet@56078
   121
blanchet@56078
   122
fun available_solvers_of ctxt =
blanchet@56078
   123
  filter (is_available ctxt) (all_solvers_of ctxt)
blanchet@56078
   124
blanchet@56078
   125
fun warn_solver (Context.Proof ctxt) name =
wenzelm@56294
   126
      if Context_Position.is_visible ctxt then
blanchet@57199
   127
        warning ("The SMT solver " ^ quote name ^ " is not installed")
wenzelm@56294
   128
      else ()
blanchet@57199
   129
  | warn_solver _ _ = ()
blanchet@56078
   130
blanchet@56078
   131
fun select_solver name context =
blanchet@56078
   132
  let
blanchet@56078
   133
    val ctxt = Context.proof_of context
boehmes@59214
   134
    val upd = Data.map (map_solver (K (SOME name)))
blanchet@56078
   135
  in
blanchet@56078
   136
    if not (member (op =) (all_solvers_of ctxt) name) then
blanchet@56078
   137
      error ("Trying to select unknown solver: " ^ quote name)
blanchet@56078
   138
    else if not (is_available ctxt name) then
blanchet@56078
   139
      (warn_solver context name; upd context)
blanchet@56078
   140
    else upd context
blanchet@56078
   141
  end
blanchet@56078
   142
blanchet@56078
   143
fun no_solver_err () = error "No SMT solver selected"
blanchet@56078
   144
blanchet@56078
   145
fun solver_of ctxt =
blanchet@56078
   146
  (case solver_name_of ctxt of
blanchet@56078
   147
    SOME name => name
blanchet@56078
   148
  | NONE => no_solver_err ())
blanchet@56078
   149
blanchet@56078
   150
fun solver_info_of default select ctxt =
boehmes@59214
   151
  (case solver_name_of ctxt of
boehmes@59214
   152
    NONE => default ()
boehmes@59214
   153
  | SOME name => select (Symtab.lookup (solvers_of (Data.get (Context.Proof ctxt))) name))
blanchet@56078
   154
blanchet@56078
   155
fun solver_class_of ctxt =
blanchet@56078
   156
  let fun class_of ({class, ...}: solver_info, _) = class ctxt
blanchet@56078
   157
  in solver_info_of no_solver_err (class_of o the) ctxt end
blanchet@56078
   158
blanchet@56078
   159
fun solver_options_of ctxt =
blanchet@56078
   160
  let
blanchet@56078
   161
    fun all_options NONE = []
blanchet@56078
   162
      | all_options (SOME ({options, ...} : solver_info, opts)) =
blanchet@56078
   163
          opts @ options ctxt
blanchet@56078
   164
  in solver_info_of (K []) all_options ctxt end
blanchet@56078
   165
blanchet@56078
   166
val setup_solver =
blanchet@58061
   167
  Attrib.setup @{binding smt_solver}
blanchet@56078
   168
    (Scan.lift (@{keyword "="} |-- Args.name) >>
blanchet@56078
   169
      (Thm.declaration_attribute o K o select_solver))
blanchet@56078
   170
    "SMT solver configuration"
blanchet@56078
   171
blanchet@56078
   172
blanchet@56078
   173
(* options *)
blanchet@56078
   174
blanchet@58061
   175
val oracle = Attrib.setup_config_bool @{binding smt_oracle} (K true)
blanchet@58061
   176
val timeout = Attrib.setup_config_real @{binding smt_timeout} (K 30.0)
boehmes@59213
   177
val reconstruction_step_timeout = Attrib.setup_config_real @{binding smt_reconstruction_step_timeout} (K 10.0)
blanchet@58061
   178
val random_seed = Attrib.setup_config_int @{binding smt_random_seed} (K 1)
blanchet@58061
   179
val read_only_certificates = Attrib.setup_config_bool @{binding smt_read_only_certificates} (K false)
blanchet@58061
   180
val verbose = Attrib.setup_config_bool @{binding smt_verbose} (K true)
blanchet@58061
   181
val trace = Attrib.setup_config_bool @{binding smt_trace} (K false)
boehmes@59215
   182
val statistics = Attrib.setup_config_bool @{binding smt_statistics} (K false)
blanchet@58061
   183
val monomorph_limit = Attrib.setup_config_int @{binding smt_monomorph_limit} (K 10)
blanchet@58061
   184
val monomorph_instances = Attrib.setup_config_int @{binding smt_monomorph_instances} (K 500)
blanchet@66738
   185
val explicit_application = Attrib.setup_config_int @{binding smt_explicit_application} (K 1)
blanchet@66551
   186
val higher_order = Attrib.setup_config_bool @{binding smt_higher_order} (K false)
blanchet@66298
   187
val nat_as_int = Attrib.setup_config_bool @{binding smt_nat_as_int} (K false)
blanchet@58061
   188
val infer_triggers = Attrib.setup_config_bool @{binding smt_infer_triggers} (K false)
blanchet@58061
   189
val debug_files = Attrib.setup_config_string @{binding smt_debug_files} (K "")
blanchet@58061
   190
val sat_solver = Attrib.setup_config_string @{binding smt_sat_solver} (K "cdclite")
blanchet@56078
   191
blanchet@56078
   192
blanchet@56078
   193
(* diagnostics *)
blanchet@56078
   194
blanchet@56078
   195
fun cond_trace flag f x = if flag then tracing ("SMT: " ^ f x) else ()
blanchet@56078
   196
blanchet@56078
   197
fun verbose_msg ctxt = cond_trace (Config.get ctxt verbose)
blanchet@56078
   198
fun trace_msg ctxt = cond_trace (Config.get ctxt trace)
boehmes@59215
   199
fun statistics_msg ctxt = cond_trace (Config.get ctxt statistics)
blanchet@56078
   200
blanchet@56078
   201
blanchet@56078
   202
(* tools *)
blanchet@56078
   203
boehmes@59213
   204
fun with_time_limit ctxt timeout_config f x =
wenzelm@62519
   205
  Timeout.apply (seconds (Config.get ctxt timeout_config)) f x
wenzelm@62519
   206
    handle Timeout.TIMEOUT _ => raise SMT_Failure.SMT SMT_Failure.Time_Out
blanchet@56078
   207
boehmes@59213
   208
fun with_timeout ctxt = with_time_limit ctxt timeout
boehmes@59213
   209
blanchet@56078
   210
blanchet@56078
   211
(* certificates *)
blanchet@56078
   212
boehmes@59214
   213
val certificates_of = certs_of o Data.get o Context.Proof
blanchet@56078
   214
boehmes@59214
   215
val get_certificates_path = Option.map (Cache_IO.cache_path_of) o certificates_of
blanchet@56078
   216
boehmes@59214
   217
fun select_certificates name context = context |> Data.map (put_certs (
blanchet@56078
   218
  if name = "" then NONE
blanchet@56078
   219
  else
blanchet@56078
   220
    Path.explode name
wenzelm@56208
   221
    |> Path.append (Resources.master_directory (Context.theory_of context))
boehmes@59214
   222
    |> SOME o Cache_IO.unsynchronized_init))
blanchet@56078
   223
blanchet@56078
   224
val setup_certificates =
blanchet@58061
   225
  Attrib.setup @{binding smt_certificates}
blanchet@56078
   226
    (Scan.lift (@{keyword "="} |-- Args.name) >>
blanchet@56078
   227
      (Thm.declaration_attribute o K o select_certificates))
blanchet@56078
   228
    "SMT certificates configuration"
blanchet@56078
   229
blanchet@56078
   230
blanchet@56078
   231
(* setup *)
blanchet@56078
   232
blanchet@56078
   233
val _ = Theory.setup (
blanchet@56078
   234
  setup_solver #>
blanchet@56078
   235
  setup_certificates)
blanchet@56078
   236
blanchet@56078
   237
fun print_setup ctxt =
blanchet@56078
   238
  let
blanchet@56078
   239
    fun string_of_bool b = if b then "true" else "false"
blanchet@56078
   240
blanchet@56078
   241
    val names = available_solvers_of ctxt
blanchet@56078
   242
    val ns = if null names then ["(none)"] else sort_strings names
blanchet@56078
   243
    val n = the_default "(none)" (solver_name_of ctxt)
blanchet@56078
   244
    val opts = solver_options_of ctxt
blanchet@57230
   245
blanchet@56078
   246
    val t = string_of_real (Config.get ctxt timeout)
blanchet@56078
   247
blanchet@56078
   248
    val certs_filename =
blanchet@56078
   249
      (case get_certificates_path ctxt of
blanchet@56078
   250
        SOME path => Path.print path
blanchet@56078
   251
      | NONE => "(disabled)")
blanchet@56078
   252
  in
blanchet@56078
   253
    Pretty.writeln (Pretty.big_list "SMT setup:" [
blanchet@56078
   254
      Pretty.str ("Current SMT solver: " ^ n),
blanchet@56078
   255
      Pretty.str ("Current SMT solver options: " ^ space_implode " " opts),
blanchet@56078
   256
      Pretty.str_list "Available SMT solvers: "  "" ns,
blanchet@56078
   257
      Pretty.str ("Current timeout: " ^ t ^ " seconds"),
blanchet@56078
   258
      Pretty.str ("With proofs: " ^
blanchet@56078
   259
        string_of_bool (not (Config.get ctxt oracle))),
blanchet@56078
   260
      Pretty.str ("Certificates cache: " ^ certs_filename),
blanchet@56078
   261
      Pretty.str ("Fixed certificates: " ^
blanchet@56078
   262
        string_of_bool (Config.get ctxt read_only_certificates))])
blanchet@56078
   263
  end
blanchet@56078
   264
blanchet@56078
   265
val _ =
wenzelm@59936
   266
  Outer_Syntax.command @{command_keyword smt_status}
blanchet@56078
   267
    "show the available SMT solvers, the currently selected SMT solver, \
blanchet@56078
   268
    \and the values of SMT configuration options"
blanchet@56078
   269
    (Scan.succeed (Toplevel.keep (print_setup o Toplevel.context_of)))
blanchet@56078
   270
blanchet@57229
   271
end;