src/HOL/Tools/SMT/smt_solver.ML
author boehmes
Tue Dec 07 15:55:35 2010 +0100 (2010-12-07)
changeset 41065 13424972ade4
parent 41062 304cfdbc6475
parent 41041 ec2734f34d0f
child 41121 5c5d05963f93
permissions -rw-r--r--
merged
boehmes@36898
     1
(*  Title:      HOL/Tools/SMT/smt_solver.ML
boehmes@36898
     2
    Author:     Sascha Boehme, TU Muenchen
boehmes@36898
     3
boehmes@36898
     4
SMT solvers registry and SMT tactic.
boehmes@36898
     5
*)
boehmes@36898
     6
boehmes@36898
     7
signature SMT_SOLVER =
boehmes@36898
     8
sig
boehmes@40424
     9
  (*configuration*)
boehmes@36898
    10
  type interface = {
boehmes@41059
    11
    class: SMT_Config.class,
boehmes@36898
    12
    extra_norm: SMT_Normalize.extra_norm,
boehmes@36898
    13
    translate: SMT_Translate.config }
boehmes@40162
    14
  datatype outcome = Unsat | Sat | Unknown
boehmes@36898
    15
  type solver_config = {
boehmes@40162
    16
    name: string,
boehmes@40162
    17
    env_var: string,
boehmes@40162
    18
    is_remote: bool,
boehmes@40162
    19
    options: Proof.context -> string list,
boehmes@36898
    20
    interface: interface,
boehmes@40162
    21
    outcome: string -> string list -> outcome * string list,
boehmes@40162
    22
    cex_parser: (Proof.context -> SMT_Translate.recon -> string list ->
boehmes@40828
    23
      term list * term list) option,
boehmes@40162
    24
    reconstruct: (Proof.context -> SMT_Translate.recon -> string list ->
blanchet@40981
    25
      (int list * thm) * Proof.context) option,
blanchet@40981
    26
    default_max_relevant: int }
boehmes@36898
    27
boehmes@40424
    28
  (*registry*)
boehmes@40196
    29
  type solver = bool option -> Proof.context -> (int * thm) list ->
boehmes@40196
    30
    int list * thm
boehmes@40162
    31
  val add_solver: solver_config -> theory -> theory
blanchet@40940
    32
  val solver_name_of: Proof.context -> string
boehmes@40424
    33
  val solver_of: Proof.context -> solver
blanchet@40940
    34
  val available_solvers_of: Proof.context -> string list
blanchet@40940
    35
  val is_locally_installed: Proof.context -> string -> bool
blanchet@40940
    36
  val is_remotely_available: Proof.context -> string -> bool
blanchet@40981
    37
  val default_max_relevant: Proof.context -> string -> int
boehmes@36898
    38
boehmes@40162
    39
  (*filter*)
boehmes@40164
    40
  val smt_filter: bool -> Time.time -> Proof.state -> ('a * thm) list -> int ->
blanchet@40666
    41
    {outcome: SMT_Failure.failure option, used_facts: ('a * thm) list,
boehmes@40197
    42
    run_time_in_msecs: int option}
boehmes@40161
    43
boehmes@36898
    44
  (*tactic*)
boehmes@36898
    45
  val smt_tac': bool -> Proof.context -> thm list -> int -> Tactical.tactic
boehmes@36898
    46
  val smt_tac: Proof.context -> thm list -> int -> Tactical.tactic
boehmes@36898
    47
boehmes@36898
    48
  (*setup*)
boehmes@36898
    49
  val setup: theory -> theory
boehmes@36898
    50
end
boehmes@36898
    51
boehmes@36898
    52
structure SMT_Solver: SMT_SOLVER =
boehmes@36898
    53
struct
boehmes@36898
    54
boehmes@40424
    55
structure C = SMT_Config
boehmes@36898
    56
boehmes@40162
    57
boehmes@40424
    58
(* configuration *)
boehmes@36898
    59
boehmes@36898
    60
type interface = {
boehmes@41059
    61
  class: SMT_Config.class,
boehmes@36898
    62
  extra_norm: SMT_Normalize.extra_norm,
boehmes@36898
    63
  translate: SMT_Translate.config }
boehmes@36898
    64
boehmes@40162
    65
datatype outcome = Unsat | Sat | Unknown
boehmes@40162
    66
boehmes@36898
    67
type solver_config = {
boehmes@40162
    68
  name: string,
boehmes@40162
    69
  env_var: string,
boehmes@40162
    70
  is_remote: bool,
boehmes@40162
    71
  options: Proof.context -> string list,
boehmes@36898
    72
  interface: interface,
boehmes@40162
    73
  outcome: string -> string list -> outcome * string list,
boehmes@40162
    74
  cex_parser: (Proof.context -> SMT_Translate.recon -> string list ->
boehmes@40828
    75
    term list * term list) option,
boehmes@40162
    76
  reconstruct: (Proof.context -> SMT_Translate.recon -> string list ->
blanchet@40981
    77
    (int list * thm) * Proof.context) option,
blanchet@40981
    78
  default_max_relevant: int }
boehmes@36898
    79
boehmes@36898
    80
boehmes@36898
    81
(* interface to external solvers *)
boehmes@36898
    82
boehmes@40166
    83
fun get_local_solver env_var =
boehmes@40166
    84
  let val local_solver = getenv env_var
boehmes@40166
    85
  in if local_solver <> "" then SOME local_solver else NONE end
boehmes@40166
    86
boehmes@36898
    87
local
boehmes@36898
    88
boehmes@40196
    89
fun choose (rm, env_var, is_remote, name) =
boehmes@36898
    90
  let
boehmes@40196
    91
    val force_local = (case rm of SOME false => true | _ => false)
boehmes@40196
    92
    val force_remote = (case rm of SOME true => true | _ => false)
boehmes@40166
    93
    val lsolver = get_local_solver env_var
boehmes@36898
    94
    val remote_url = getenv "REMOTE_SMT_URL"
boehmes@40196
    95
    val trace = if is_some rm then K () else tracing
boehmes@36898
    96
  in
boehmes@40166
    97
    if not force_remote andalso is_some lsolver
boehmes@36898
    98
    then 
boehmes@40196
    99
     (trace ("Invoking local SMT solver " ^ quote (the lsolver) ^ " ...");
boehmes@40166
   100
      [the lsolver])
boehmes@40196
   101
    else if not force_local andalso is_remote
boehmes@36898
   102
    then
boehmes@40196
   103
     (trace ("Invoking remote SMT solver " ^ quote name ^ " at " ^
boehmes@36898
   104
        quote remote_url ^ " ...");
boehmes@40166
   105
      [getenv "REMOTE_SMT", name])
boehmes@40166
   106
    else if force_remote
boehmes@40196
   107
    then error ("The SMT solver " ^ quote name ^ " is not remotely available.")
boehmes@40196
   108
    else error ("The SMT solver " ^ quote name ^ " has not been found " ^
boehmes@40196
   109
      "on this computer. Please set the Isabelle environment variable " ^
boehmes@40196
   110
      quote env_var ^ ".")
boehmes@36898
   111
  end
boehmes@36898
   112
boehmes@36898
   113
fun make_cmd solver args problem_path proof_path = space_implode " " (
boehmes@36898
   114
  map File.shell_quote (solver @ args) @
boehmes@36898
   115
  [File.shell_path problem_path, "2>&1", ">", File.shell_path proof_path])
boehmes@36898
   116
boehmes@36898
   117
fun run ctxt cmd args input =
boehmes@40424
   118
  (case C.certificates_of ctxt of
boehmes@40578
   119
    NONE =>
boehmes@40578
   120
      if Config.get ctxt C.debug_files = "" then
boehmes@40578
   121
        Cache_IO.run (make_cmd (choose cmd) args) input
boehmes@40578
   122
      else
boehmes@40578
   123
        let
boehmes@40578
   124
          val base_path = Path.explode (Config.get ctxt C.debug_files)
boehmes@40578
   125
          val in_path = Path.ext "smt_in" base_path
boehmes@40578
   126
          val out_path = Path.ext "smt_out" base_path
boehmes@40578
   127
        in
boehmes@40578
   128
          Cache_IO.raw_run (make_cmd (choose cmd) args) input in_path out_path 
boehmes@40578
   129
        end
boehmes@36898
   130
  | SOME certs =>
boehmes@36898
   131
      (case Cache_IO.lookup certs input of
boehmes@36898
   132
        (NONE, key) =>
boehmes@40538
   133
          if Config.get ctxt C.fixed then
boehmes@40538
   134
            error ("Bad certificates cache: missing certificate")
boehmes@40538
   135
          else
boehmes@40538
   136
            Cache_IO.run_and_cache certs key (make_cmd (choose cmd) args) input
boehmes@36898
   137
      | (SOME output, _) =>
boehmes@36898
   138
         (tracing ("Using cached certificate from " ^
boehmes@36898
   139
            File.shell_path (Cache_IO.cache_path_of certs) ^ " ...");
boehmes@40550
   140
          output)))
boehmes@36898
   141
boehmes@36898
   142
in
boehmes@36898
   143
boehmes@36898
   144
fun run_solver ctxt cmd args input =
boehmes@36898
   145
  let
boehmes@36898
   146
    fun pretty tag ls = Pretty.string_of (Pretty.big_list tag
boehmes@36898
   147
      (map Pretty.str ls))
boehmes@36898
   148
boehmes@40424
   149
    val _ = C.trace_msg ctxt (pretty "Problem:" o split_lines) input
boehmes@36898
   150
boehmes@40550
   151
    val {redirected_output=res, output=err, return_code} =
boehmes@40550
   152
      C.with_timeout ctxt (run ctxt cmd args) input
boehmes@40424
   153
    val _ = C.trace_msg ctxt (pretty "Solver:") err
boehmes@36898
   154
haftmann@39811
   155
    val ls = rev (snd (chop_while (equal "") (rev res)))
boehmes@40424
   156
    val _ = C.trace_msg ctxt (pretty "Result:") ls
boehmes@40550
   157
boehmes@40550
   158
    val _ = null ls andalso return_code <> 0 andalso
boehmes@40561
   159
      raise SMT_Failure.SMT (SMT_Failure.Abnormal_Termination return_code)
boehmes@36898
   160
  in ls end
boehmes@36898
   161
boehmes@36898
   162
end
boehmes@36898
   163
boehmes@40424
   164
fun trace_assms ctxt = C.trace_msg ctxt (Pretty.string_of o
boehmes@40424
   165
  Pretty.big_list "Assertions:" o map (Display.pretty_thm ctxt o snd))
boehmes@40198
   166
blanchet@36940
   167
fun trace_recon_data ctxt ({typs, terms, ...} : SMT_Translate.recon) =
boehmes@36898
   168
  let
boehmes@36898
   169
    fun pretty_eq n p = Pretty.block [Pretty.str n, Pretty.str " = ", p]
boehmes@40424
   170
    fun p_typ (n, T) = pretty_eq n (Syntax.pretty_typ ctxt T)
boehmes@40424
   171
    fun p_term (n, t) = pretty_eq n (Syntax.pretty_term ctxt t)
boehmes@36898
   172
  in
boehmes@40424
   173
    C.trace_msg ctxt (fn () =>
boehmes@40424
   174
      Pretty.string_of (Pretty.big_list "Names:" [
boehmes@40424
   175
        Pretty.big_list "sorts:" (map p_typ (Symtab.dest typs)),
boehmes@40424
   176
        Pretty.big_list "functions:" (map p_term (Symtab.dest terms))])) ()
boehmes@36898
   177
  end
boehmes@36898
   178
boehmes@40424
   179
fun invoke translate_config name cmd options irules ctxt =
boehmes@40162
   180
  let
boehmes@40424
   181
    val args = C.solver_options_of ctxt @ options ctxt
boehmes@40162
   182
    val comments = ("solver: " ^ name) ::
boehmes@41062
   183
      ("timeout: " ^ string_of_real (Config.get ctxt C.timeout)) ::
boehmes@40162
   184
      "arguments:" :: args
boehmes@40162
   185
  in
boehmes@40162
   186
    irules
boehmes@40198
   187
    |> tap (trace_assms ctxt)
boehmes@40162
   188
    |> SMT_Translate.translate translate_config ctxt comments
boehmes@40162
   189
    ||> tap (trace_recon_data ctxt)
boehmes@40162
   190
    |>> run_solver ctxt cmd args
boehmes@40162
   191
    |> rpair ctxt
boehmes@40162
   192
  end
boehmes@36898
   193
boehmes@36898
   194
fun discharge_definitions thm =
boehmes@36898
   195
  if Thm.nprems_of thm = 0 then thm
boehmes@36898
   196
  else discharge_definitions (@{thm reflexive} RS thm)
boehmes@36898
   197
boehmes@40162
   198
fun set_has_datatypes with_datatypes translate =
boehmes@36898
   199
  let
boehmes@41059
   200
    val {prefixes, header, is_fol, has_datatypes, serialize} = translate
boehmes@40162
   201
    val with_datatypes' = has_datatypes andalso with_datatypes
boehmes@41059
   202
    val translate' = {prefixes=prefixes, header=header, is_fol=is_fol,
boehmes@41059
   203
      has_datatypes=with_datatypes', serialize=serialize}
boehmes@40162
   204
  in (with_datatypes', translate') end
boehmes@40162
   205
boehmes@40164
   206
fun trace_assumptions ctxt irules idxs =
boehmes@40164
   207
  let
boehmes@40164
   208
    val thms = filter (fn i => i >= 0) idxs
boehmes@40164
   209
      |> map_filter (AList.lookup (op =) irules)
boehmes@40164
   210
  in
boehmes@40424
   211
    if Config.get ctxt C.trace_used_facts andalso length thms > 0
boehmes@40164
   212
    then
boehmes@40164
   213
      tracing (Pretty.string_of (Pretty.big_list "SMT used facts:"
boehmes@40164
   214
        (map (Display.pretty_thm ctxt) thms)))
boehmes@40164
   215
    else ()
boehmes@40164
   216
  end
boehmes@40164
   217
blanchet@41041
   218
blanchet@41041
   219
blanchet@41041
   220
(* registry *)
blanchet@41041
   221
blanchet@41041
   222
type solver = bool option -> Proof.context -> (int * thm) list -> int list * thm
blanchet@41041
   223
blanchet@41041
   224
type solver_info = {
blanchet@41041
   225
  env_var: string,
blanchet@41041
   226
  is_remote: bool,
blanchet@41041
   227
  options: Proof.context -> string list,
blanchet@41041
   228
  interface: interface,
blanchet@41041
   229
  reconstruct: string list * SMT_Translate.recon -> Proof.context ->
blanchet@41041
   230
    (int list * thm) * Proof.context,
blanchet@41041
   231
  default_max_relevant: int }
blanchet@41041
   232
blanchet@41041
   233
fun gen_solver name (info : solver_info) rm ctxt irules =
boehmes@40162
   234
  let
blanchet@40981
   235
    val {env_var, is_remote, options, interface, reconstruct, ...} = info
boehmes@41059
   236
    val {extra_norm, translate, ...} = interface
boehmes@40162
   237
    val (with_datatypes, translate') =
boehmes@40424
   238
      set_has_datatypes (Config.get ctxt C.datatypes) translate
boehmes@40196
   239
    val cmd = (rm, env_var, is_remote, name)
boehmes@36898
   240
  in
boehmes@40162
   241
    (irules, ctxt)
boehmes@40424
   242
    |-> SMT_Normalize.normalize extra_norm with_datatypes
boehmes@40424
   243
    |-> invoke translate' name cmd options
boehmes@36898
   244
    |-> reconstruct
boehmes@40161
   245
    |-> (fn (idxs, thm) => fn ctxt' => thm
boehmes@36898
   246
    |> singleton (ProofContext.export ctxt' ctxt)
boehmes@40161
   247
    |> discharge_definitions
boehmes@40164
   248
    |> tap (fn _ => trace_assumptions ctxt irules idxs)
boehmes@40161
   249
    |> pair idxs)
boehmes@36898
   250
  end
boehmes@36898
   251
boehmes@36899
   252
structure Solvers = Generic_Data
boehmes@36898
   253
(
boehmes@40162
   254
  type T = solver_info Symtab.table
boehmes@36898
   255
  val empty = Symtab.empty
boehmes@36898
   256
  val extend = I
boehmes@36898
   257
  fun merge data = Symtab.merge (K true) data
boehmes@36898
   258
    handle Symtab.DUP name => error ("Duplicate SMT solver: " ^ quote name)
boehmes@36898
   259
)
boehmes@36898
   260
boehmes@40162
   261
local
boehmes@40162
   262
  fun finish outcome cex_parser reconstruct ocl (output, recon) ctxt =
boehmes@40162
   263
    (case outcome output of
boehmes@40162
   264
      (Unsat, ls) =>
boehmes@40424
   265
        if not (Config.get ctxt C.oracle) andalso is_some reconstruct
boehmes@40162
   266
        then the reconstruct ctxt recon ls
boehmes@40162
   267
        else (([], ocl ()), ctxt)
boehmes@40162
   268
    | (result, ls) =>
boehmes@40828
   269
        let
boehmes@40828
   270
          val (ts, us) =
boehmes@40828
   271
            (case cex_parser of SOME f => f ctxt recon ls | _ => ([], []))
boehmes@40828
   272
         in
boehmes@40828
   273
          raise SMT_Failure.SMT (SMT_Failure.Counterexample {
boehmes@40828
   274
            is_real_cex = (result = Sat),
boehmes@40828
   275
            free_constraints = ts,
boehmes@40828
   276
            const_defs = us})
boehmes@40424
   277
        end)
boehmes@40579
   278
boehmes@40579
   279
  val cfalse = Thm.cterm_of @{theory} (@{const Trueprop} $ @{const False})
boehmes@40162
   280
in
boehmes@40162
   281
boehmes@40162
   282
fun add_solver cfg =
boehmes@40162
   283
  let
boehmes@40162
   284
    val {name, env_var, is_remote, options, interface, outcome, cex_parser,
blanchet@40981
   285
      reconstruct, default_max_relevant} = cfg
boehmes@41059
   286
    val {class, ...} = interface
boehmes@40162
   287
boehmes@40579
   288
    fun core_oracle () = cfalse
boehmes@40162
   289
boehmes@40162
   290
    fun solver ocl = { env_var=env_var, is_remote=is_remote, options=options,
boehmes@40424
   291
      interface=interface,
blanchet@40981
   292
      reconstruct=finish (outcome name) cex_parser reconstruct ocl,
blanchet@40981
   293
      default_max_relevant=default_max_relevant }
boehmes@40162
   294
  in
boehmes@40162
   295
    Thm.add_oracle (Binding.name name, core_oracle) #-> (fn (_, ocl) =>
boehmes@40162
   296
    Context.theory_map (Solvers.map (Symtab.update_new (name, solver ocl)))) #>
boehmes@41059
   297
    Context.theory_map (C.add_solver (name, class))
boehmes@40162
   298
  end
boehmes@40162
   299
boehmes@40162
   300
end
boehmes@40162
   301
blanchet@40981
   302
fun get_info ctxt name =
blanchet@40981
   303
  the (Symtab.lookup (Solvers.get (Context.Proof ctxt)) name)
blanchet@40981
   304
boehmes@40424
   305
fun name_and_solver_of ctxt =
boehmes@40424
   306
  let val name = C.solver_of ctxt
blanchet@40981
   307
  in (name, get_info ctxt name) end
boehmes@36898
   308
blanchet@40940
   309
val solver_name_of = fst o name_and_solver_of
boehmes@40424
   310
fun solver_of ctxt =
boehmes@40424
   311
  let val (name, raw_solver) = name_and_solver_of ctxt
boehmes@40424
   312
  in gen_solver name raw_solver end
boehmes@36898
   313
blanchet@40940
   314
val available_solvers_of = Symtab.keys o Solvers.get o Context.Proof
blanchet@40940
   315
blanchet@40940
   316
fun is_locally_installed ctxt name =
blanchet@40981
   317
  let val {env_var, ...} = get_info ctxt name
boehmes@40166
   318
  in is_some (get_local_solver env_var) end
boehmes@40166
   319
blanchet@40981
   320
val is_remotely_available = #is_remote oo get_info
blanchet@40981
   321
blanchet@40981
   322
val default_max_relevant = #default_max_relevant oo get_info
boehmes@36898
   323
boehmes@36898
   324
boehmes@40424
   325
(* filter *)
boehmes@40161
   326
boehmes@40161
   327
val has_topsort = Term.exists_type (Term.exists_subtype (fn
boehmes@40161
   328
    TFree (_, []) => true
boehmes@40161
   329
  | TVar (_, []) => true
boehmes@40161
   330
  | _ => false))
boehmes@40161
   331
boehmes@40196
   332
fun smt_solver rm ctxt irules =
boehmes@40161
   333
  (* without this test, we would run into problems when atomizing the rules: *)
boehmes@40424
   334
  if exists (has_topsort o Thm.prop_of o snd) irules then
boehmes@40424
   335
    raise SMT_Failure.SMT (SMT_Failure.Other_Failure ("proof state " ^
boehmes@40424
   336
      "contains the universal sort {}"))
boehmes@40424
   337
  else solver_of ctxt rm ctxt irules
boehmes@40162
   338
boehmes@40579
   339
val cnot = Thm.cterm_of @{theory} @{const Not}
boehmes@40579
   340
boehmes@40196
   341
fun smt_filter run_remote time_limit st xrules i =
boehmes@40162
   342
  let
boehmes@40199
   343
    val {facts, goal, ...} = Proof.goal st
boehmes@40164
   344
    val ctxt =
boehmes@40199
   345
      Proof.context_of st
boehmes@40424
   346
      |> Config.put C.oracle false
boehmes@40560
   347
      |> Config.put C.timeout (Time.toReal time_limit)
boehmes@40424
   348
      |> Config.put C.drop_bad_facts true
boehmes@40424
   349
      |> Config.put C.filter_only_facts true
boehmes@40357
   350
    val ({context=ctxt', prems, concl, ...}, _) = Subgoal.focus ctxt i goal
boehmes@40579
   351
    fun negate ct = Thm.dest_comb ct ||> Thm.capply cnot |-> Thm.capply
boehmes@40579
   352
    val cprop = negate (Thm.rhs_of (SMT_Normalize.atomize_conv ctxt' concl))
boehmes@40357
   353
    val irs = map (pair ~1) (Thm.assume cprop :: prems @ facts)
boehmes@40196
   354
    val rm = SOME run_remote
boehmes@40162
   355
  in
blanchet@40666
   356
    (xrules, map snd xrules)
boehmes@40357
   357
    ||> distinct (op =) o fst o smt_solver rm ctxt' o append irs o map_index I
boehmes@40164
   358
    |-> map_filter o try o nth
blanchet@40980
   359
    |> (fn xs => {outcome=NONE, used_facts=if solver_name_of ctxt = "z3" (* FIXME *) then xs
blanchet@40980
   360
      else xrules, run_time_in_msecs=NONE})
boehmes@40162
   361
  end
boehmes@40424
   362
  handle SMT_Failure.SMT fail => {outcome=SOME fail, used_facts=[],
boehmes@40424
   363
    run_time_in_msecs=NONE}
boehmes@40166
   364
  (* FIXME: measure runtime *)
boehmes@40161
   365
boehmes@40161
   366
boehmes@40161
   367
boehmes@36898
   368
(* SMT tactic *)
boehmes@36898
   369
boehmes@36898
   370
fun smt_tac' pass_exns ctxt rules =
boehmes@36899
   371
  CONVERSION (SMT_Normalize.atomize_conv ctxt)
boehmes@36899
   372
  THEN' Tactic.rtac @{thm ccontr}
boehmes@40424
   373
  THEN' SUBPROOF (fn {context=ctxt', prems, ...} =>
boehmes@40165
   374
    let
boehmes@40424
   375
      fun solve irules = snd (smt_solver NONE ctxt' irules)
boehmes@40424
   376
      val tag = "Solver " ^ C.solver_of ctxt' ^ ": "
boehmes@40828
   377
      val str_of = prefix tag o SMT_Failure.string_of_failure ctxt'
boehmes@40424
   378
      fun safe_solve irules =
boehmes@40424
   379
        if pass_exns then SOME (solve irules)
boehmes@40515
   380
        else (SOME (solve irules)
boehmes@40515
   381
          handle
boehmes@40515
   382
            SMT_Failure.SMT (fail as SMT_Failure.Counterexample _) =>
boehmes@40828
   383
              (C.verbose_msg ctxt' str_of fail; NONE)
boehmes@40828
   384
          | SMT_Failure.SMT fail => (C.trace_msg ctxt' str_of fail; NONE))
boehmes@40165
   385
    in
boehmes@40424
   386
      safe_solve (map (pair ~1) (rules @ prems))
boehmes@40165
   387
      |> (fn SOME thm => Tactic.rtac thm 1 | _ => Tactical.no_tac)
boehmes@40166
   388
    end) ctxt
boehmes@36898
   389
boehmes@36898
   390
val smt_tac = smt_tac' false
boehmes@40162
   391
boehmes@36898
   392
val smt_method =
boehmes@36898
   393
  Scan.optional Attrib.thms [] >>
boehmes@36898
   394
  (fn thms => fn ctxt => METHOD (fn facts =>
boehmes@36898
   395
    HEADGOAL (smt_tac ctxt (thms @ facts))))
boehmes@36898
   396
boehmes@36898
   397
boehmes@36898
   398
boehmes@36898
   399
(* setup *)
boehmes@36898
   400
boehmes@36898
   401
val setup =
wenzelm@38808
   402
  Method.setup @{binding smt} smt_method
boehmes@36898
   403
    "Applies an SMT solver to the current goal."
boehmes@36898
   404
boehmes@36898
   405
end