src/HOL/Tools/SMT/smt_solver.ML
author haftmann
Thu, 08 Jul 2010 16:19:24 +0200
changeset 37744 3daaf23b9ab4
parent 36960 01594f816e3a
child 38808 89ae86205739
permissions -rw-r--r--
tuned titles
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
     1
(*  Title:      HOL/Tools/SMT/smt_solver.ML
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
     2
    Author:     Sascha Boehme, TU Muenchen
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
     3
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
     4
SMT solvers registry and SMT tactic.
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
     5
*)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
     6
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
     7
signature SMT_SOLVER =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
     8
sig
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
     9
  exception SMT of string
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    10
  exception SMT_COUNTEREXAMPLE of bool * term list
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    11
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    12
  type interface = {
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    13
    extra_norm: SMT_Normalize.extra_norm,
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    14
    translate: SMT_Translate.config }
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    15
  type solver_config = {
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    16
    command: {env_var: string, remote_name: string option},
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    17
    arguments: string list,
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    18
    interface: interface,
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    19
    reconstruct: (string list * SMT_Translate.recon) -> Proof.context ->
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    20
      thm * Proof.context }
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    21
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    22
  (*options*)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    23
  val timeout: int Config.T
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    24
  val with_timeout: Proof.context -> ('a -> 'b) -> 'a -> 'b
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    25
  val trace: bool Config.T
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    26
  val trace_msg: Proof.context -> ('a -> string) -> 'a -> unit
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    27
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    28
  (*certificates*)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    29
  val fixed_certificates: bool Config.T
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    30
  val select_certificates: string -> Context.generic -> Context.generic
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    31
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    32
  (*solvers*)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    33
  type solver = Proof.context -> thm list -> thm
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    34
  type solver_info = Context.generic -> Pretty.T list
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
    35
  val add_solver: string * (Proof.context -> solver_config) ->
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
    36
    Context.generic -> Context.generic
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
    37
  val all_solver_names_of: Context.generic -> string list
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
    38
  val add_solver_info: string * solver_info -> Context.generic ->
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
    39
    Context.generic
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    40
  val solver_name_of: Context.generic -> string
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    41
  val select_solver: string -> Context.generic -> Context.generic
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    42
  val solver_of: Context.generic -> solver
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    43
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    44
  (*tactic*)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    45
  val smt_tac': bool -> Proof.context -> thm list -> int -> Tactical.tactic
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    46
  val smt_tac: Proof.context -> thm list -> int -> Tactical.tactic
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    47
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    48
  (*setup*)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    49
  val setup: theory -> theory
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    50
  val print_setup: Context.generic -> unit
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    51
end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    52
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    53
structure SMT_Solver: SMT_SOLVER =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    54
struct
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    55
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    56
exception SMT of string
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    57
exception SMT_COUNTEREXAMPLE of bool * term list
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    58
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    59
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    60
type interface = {
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    61
  extra_norm: SMT_Normalize.extra_norm,
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    62
  translate: SMT_Translate.config }
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    63
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    64
type solver_config = {
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    65
  command: {env_var: string, remote_name: string option},
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    66
  arguments: string list,
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    67
  interface: interface,
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    68
  reconstruct: (string list * SMT_Translate.recon) -> Proof.context ->
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    69
    thm * Proof.context }
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    70
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    71
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    72
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    73
(* SMT options *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    74
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    75
val (timeout, setup_timeout) = Attrib.config_int "smt_timeout" (K 30)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    76
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    77
fun with_timeout ctxt f x =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    78
  TimeLimit.timeLimit (Time.fromSeconds (Config.get ctxt timeout)) f x
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    79
  handle TimeLimit.TimeOut => raise SMT "timeout"
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    80
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    81
val (trace, setup_trace) = Attrib.config_bool "smt_trace" (K false)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    82
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    83
fun trace_msg ctxt f x =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    84
  if Config.get ctxt trace then tracing (f x) else ()
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    85
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    86
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    87
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    88
(* SMT certificates *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    89
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    90
val (fixed_certificates, setup_fixed_certificates) =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    91
  Attrib.config_bool "smt_fixed" (K false)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    92
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    93
structure Certificates = Generic_Data
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    94
(
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    95
  type T = Cache_IO.cache option
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    96
  val empty = NONE
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    97
  val extend = I
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    98
  fun merge (s, _) = s
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    99
)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   100
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   101
val get_certificates_path =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   102
  Option.map (Cache_IO.cache_path_of) o Certificates.get
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   103
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   104
fun select_certificates name = Certificates.put (
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   105
  if name = "" then NONE
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   106
  else SOME (Cache_IO.make (Path.explode name)))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   107
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   108
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   109
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   110
(* interface to external solvers *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   111
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   112
local
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   113
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   114
fun choose {env_var, remote_name} =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   115
  let
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   116
    val local_solver = getenv env_var
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   117
    val remote_solver = the_default "" remote_name
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   118
    val remote_url = getenv "REMOTE_SMT_URL"
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   119
  in
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   120
    if local_solver <> ""
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   121
    then 
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   122
     (tracing ("Invoking local SMT solver " ^ quote local_solver ^ " ...");
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   123
      [local_solver])
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   124
    else if remote_solver <> ""
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   125
    then
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   126
     (tracing ("Invoking remote SMT solver " ^ quote remote_solver ^ " at " ^
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   127
        quote remote_url ^ " ...");
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   128
      [getenv "REMOTE_SMT", remote_solver])
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   129
    else error ("Undefined Isabelle environment variable: " ^ quote env_var)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   130
  end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   131
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   132
fun make_cmd solver args problem_path proof_path = space_implode " " (
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   133
  map File.shell_quote (solver @ args) @
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   134
  [File.shell_path problem_path, "2>&1", ">", File.shell_path proof_path])
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   135
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   136
fun run ctxt cmd args input =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   137
  (case Certificates.get (Context.Proof ctxt) of
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   138
    NONE => Cache_IO.run (make_cmd (choose cmd) args) input
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   139
  | SOME certs =>
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   140
      (case Cache_IO.lookup certs input of
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   141
        (NONE, key) =>
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   142
          if Config.get ctxt fixed_certificates
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   143
          then error ("Bad certificates cache: missing certificate")
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   144
          else Cache_IO.run_and_cache certs key (make_cmd (choose cmd) args)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   145
            input
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   146
      | (SOME output, _) =>
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   147
         (tracing ("Using cached certificate from " ^
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   148
            File.shell_path (Cache_IO.cache_path_of certs) ^ " ...");
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   149
          output)))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   150
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   151
in
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   152
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   153
fun run_solver ctxt cmd args input =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   154
  let
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   155
    fun pretty tag ls = Pretty.string_of (Pretty.big_list tag
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   156
      (map Pretty.str ls))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   157
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   158
    val _ = trace_msg ctxt (pretty "SMT problem:" o split_lines) input
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   159
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   160
    val (res, err) = with_timeout ctxt (run ctxt cmd args) input
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   161
    val _ = trace_msg ctxt (pretty "SMT solver:") err
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   162
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   163
    val ls = rev (dropwhile (equal "") (rev res))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   164
    val _ = trace_msg ctxt (pretty "SMT result:") ls
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   165
  in ls end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   166
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   167
end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   168
36940
b4417ddad979 make SML/NJ happy
blanchet
parents: 36899
diff changeset
   169
fun trace_recon_data ctxt ({typs, terms, ...} : SMT_Translate.recon) =
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   170
  let
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   171
    fun pretty_eq n p = Pretty.block [Pretty.str n, Pretty.str " = ", p]
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   172
    fun pretty_typ (n, T) = pretty_eq n (Syntax.pretty_typ ctxt T)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   173
    fun pretty_term (n, t) = pretty_eq n (Syntax.pretty_term ctxt t)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   174
  in
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   175
    trace_msg ctxt (fn () => Pretty.string_of (Pretty.big_list "SMT names:" [
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   176
      Pretty.big_list "sorts:" (map pretty_typ (Symtab.dest typs)),
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   177
      Pretty.big_list "functions:" (map pretty_term (Symtab.dest terms))])) ()
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   178
  end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   179
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   180
fun invoke translate_config comments command arguments thms ctxt =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   181
  thms
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   182
  |> SMT_Translate.translate translate_config ctxt comments
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   183
  ||> tap (trace_recon_data ctxt)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   184
  |>> run_solver ctxt command arguments
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   185
  |> rpair ctxt
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   186
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   187
fun discharge_definitions thm =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   188
  if Thm.nprems_of thm = 0 then thm
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   189
  else discharge_definitions (@{thm reflexive} RS thm)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   190
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   191
fun gen_solver name solver ctxt prems =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   192
  let
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   193
    val {command, arguments, interface, reconstruct} = solver ctxt
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   194
    val comments = ("solver: " ^ name) ::
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   195
      ("timeout: " ^ string_of_int (Config.get ctxt timeout)) ::
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   196
      "arguments:" :: arguments
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   197
    val {extra_norm, translate} = interface
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   198
  in
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   199
    (prems, ctxt)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   200
    |-> SMT_Normalize.normalize extra_norm
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   201
    |-> invoke translate comments command arguments
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   202
    |-> reconstruct
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   203
    |-> (fn thm => fn ctxt' => thm
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   204
    |> singleton (ProofContext.export ctxt' ctxt)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   205
    |> discharge_definitions)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   206
  end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   207
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   208
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   209
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   210
(* solver store *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   211
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   212
type solver = Proof.context -> thm list -> thm
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   213
type solver_info = Context.generic -> Pretty.T list
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   214
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   215
structure Solvers = Generic_Data
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   216
(
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   217
  type T = ((Proof.context -> solver_config) * solver_info) Symtab.table
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   218
  val empty = Symtab.empty
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   219
  val extend = I
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   220
  fun merge data = Symtab.merge (K true) data
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   221
    handle Symtab.DUP name => error ("Duplicate SMT solver: " ^ quote name)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   222
)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   223
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   224
val no_solver = "(none)"
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   225
val add_solver = Solvers.map o Symtab.update_new o apsnd (rpair (K []))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   226
val all_solver_names_of = Symtab.keys o Solvers.get
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   227
val lookup_solver = Symtab.lookup o Solvers.get
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   228
fun add_solver_info (n, i) = Solvers.map (Symtab.map_entry n (apsnd (K i)))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   229
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   230
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   231
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   232
(* selected solver *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   233
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   234
structure Selected_Solver = Generic_Data
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   235
(
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   236
  type T = string
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   237
  val empty = no_solver
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   238
  val extend = I
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   239
  fun merge (s, _) = s
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   240
)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   241
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   242
val solver_name_of = Selected_Solver.get
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   243
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   244
fun select_solver name context =
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   245
  if is_none (lookup_solver context name)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   246
  then error ("SMT solver not registered: " ^ quote name)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   247
  else Selected_Solver.map (K name) context
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   248
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   249
fun raw_solver_of context name =
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   250
  (case lookup_solver context name of
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   251
    NONE => error "No SMT solver selected"
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   252
  | SOME (s, _) => s)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   253
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   254
fun solver_of context =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   255
  let val name = solver_name_of context
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   256
  in gen_solver name (raw_solver_of context name) end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   257
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   258
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   259
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   260
(* SMT tactic *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   261
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   262
local
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   263
  fun pretty_cex ctxt (real, ex) =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   264
    let
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   265
      val msg = if real then "SMT: counterexample found"
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   266
        else "SMT: potential counterexample found"
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   267
    in
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   268
      if null ex then msg ^ "."
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   269
      else Pretty.string_of (Pretty.big_list (msg ^ ":")
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   270
        (map (Syntax.pretty_term ctxt) ex))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   271
    end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   272
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   273
  fun fail_tac f msg st = (f msg; Tactical.no_tac st)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   274
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   275
  fun SAFE pass_exns tac ctxt i st =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   276
    if pass_exns then tac ctxt i st
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   277
    else (tac ctxt i st
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   278
      handle SMT msg => fail_tac (trace_msg ctxt (prefix "SMT: ")) msg st
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   279
           | SMT_COUNTEREXAMPLE ce => fail_tac tracing (pretty_cex ctxt ce) st)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   280
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   281
  fun smt_solver rules ctxt = solver_of (Context.Proof ctxt) ctxt rules
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   282
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   283
  val has_topsort = Term.exists_type (Term.exists_subtype (fn
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   284
      TFree (_, []) => true
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   285
    | TVar (_, []) => true
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   286
    | _ => false))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   287
in
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   288
fun smt_tac' pass_exns ctxt rules =
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   289
  CONVERSION (SMT_Normalize.atomize_conv ctxt)
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   290
  THEN' Tactic.rtac @{thm ccontr}
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   291
  THEN' SUBPROOF (fn {context, prems, ...} =>
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   292
    let val thms = rules @ prems
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   293
    in
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   294
      if exists (has_topsort o Thm.prop_of) thms
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   295
      then fail_tac (trace_msg context I)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   296
        "SMT: proof state contains the universal sort {}"
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   297
      else SAFE pass_exns (Tactic.rtac o smt_solver thms) context 1
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   298
    end) ctxt
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   299
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   300
val smt_tac = smt_tac' false
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   301
end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   302
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   303
val smt_method =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   304
  Scan.optional Attrib.thms [] >>
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   305
  (fn thms => fn ctxt => METHOD (fn facts =>
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   306
    HEADGOAL (smt_tac ctxt (thms @ facts))))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   307
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   308
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   309
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   310
(* setup *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   311
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   312
val setup =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   313
  Attrib.setup (Binding.name "smt_solver")
36960
01594f816e3a prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents: 36940
diff changeset
   314
    (Scan.lift (Parse.$$$ "=" |-- Args.name) >>
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   315
      (Thm.declaration_attribute o K o select_solver))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   316
    "SMT solver configuration" #>
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   317
  setup_timeout #>
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   318
  setup_trace #>
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   319
  setup_fixed_certificates #>
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   320
  Attrib.setup (Binding.name "smt_certificates")
36960
01594f816e3a prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents: 36940
diff changeset
   321
    (Scan.lift (Parse.$$$ "=" |-- Args.name) >>
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   322
      (Thm.declaration_attribute o K o select_certificates))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   323
    "SMT certificates" #>
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   324
  Method.setup (Binding.name "smt") smt_method
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   325
    "Applies an SMT solver to the current goal."
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   326
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   327
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   328
fun print_setup context =
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   329
  let
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   330
    val t = string_of_int (Config.get_generic context timeout)
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   331
    val names = sort_strings (all_solver_names_of context)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   332
    val ns = if null names then [no_solver] else names
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   333
    val take_info = (fn (_, []) => NONE | info => SOME info)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   334
    val infos =
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   335
      Solvers.get context
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   336
      |> Symtab.dest
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   337
      |> map_filter (fn (n, (_, info)) => take_info (n, info context))
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   338
      |> sort (prod_ord string_ord (K EQUAL))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   339
      |> map (fn (n, ps) => Pretty.big_list (n ^ ":") ps)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   340
    val certs_filename =
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   341
      (case get_certificates_path context of
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   342
        SOME path => Path.implode path
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   343
      | NONE => "(disabled)")
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   344
    val fixed = if Config.get_generic context fixed_certificates then "true"
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   345
      else "false"
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   346
  in
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   347
    Pretty.writeln (Pretty.big_list "SMT setup:" [
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   348
      Pretty.str ("Current SMT solver: " ^ solver_name_of context),
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   349
      Pretty.str_list "Available SMT solvers: "  "" ns,
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   350
      Pretty.str ("Current timeout: " ^ t ^ " seconds"),
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   351
      Pretty.str ("Certificates cache: " ^ certs_filename),
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   352
      Pretty.str ("Fixed certificates: " ^ fixed),
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   353
      Pretty.big_list "Solver-specific settings:" infos])
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   354
  end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   355
36960
01594f816e3a prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents: 36940
diff changeset
   356
val _ =
01594f816e3a prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents: 36940
diff changeset
   357
  Outer_Syntax.improper_command "smt_status"
01594f816e3a prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents: 36940
diff changeset
   358
    "show the available SMT solvers and the currently selected solver" Keyword.diag
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   359
    (Scan.succeed (Toplevel.no_timing o Toplevel.keep (fn state =>
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   360
      print_setup (Context.Proof (Toplevel.context_of state)))))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   361
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   362
end