src/HOL/Tools/SMT/smt_solver.ML
author boehmes
Mon, 08 Nov 2010 12:13:44 +0100
changeset 40424 7550b2cba1cb
parent 40357 82ebdd19c4a4
child 40425 c9b5e0fcee31
permissions -rw-r--r--
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
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
40424
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents: 40357
diff changeset
     9
  (*configuration*)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    10
  type interface = {
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    11
    extra_norm: SMT_Normalize.extra_norm,
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    12
    translate: SMT_Translate.config }
40162
7f58a9a843c2 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents: 40161
diff changeset
    13
  datatype outcome = Unsat | Sat | Unknown
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    14
  type solver_config = {
40162
7f58a9a843c2 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents: 40161
diff changeset
    15
    name: string,
7f58a9a843c2 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents: 40161
diff changeset
    16
    env_var: string,
7f58a9a843c2 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents: 40161
diff changeset
    17
    is_remote: bool,
7f58a9a843c2 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents: 40161
diff changeset
    18
    options: Proof.context -> string list,
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    19
    interface: interface,
40162
7f58a9a843c2 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents: 40161
diff changeset
    20
    outcome: string -> string list -> outcome * string list,
7f58a9a843c2 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents: 40161
diff changeset
    21
    cex_parser: (Proof.context -> SMT_Translate.recon -> string list ->
7f58a9a843c2 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents: 40161
diff changeset
    22
      term list) option,
7f58a9a843c2 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents: 40161
diff changeset
    23
    reconstruct: (Proof.context -> SMT_Translate.recon -> string list ->
7f58a9a843c2 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents: 40161
diff changeset
    24
      (int list * thm) * Proof.context) option }
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    25
40424
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents: 40357
diff changeset
    26
  (*registry*)
40196
123b6fe379f6 honor choice of either local or remote SMT solver only for smt_filter and keep default behaviour for the SMT tactic; omit messages when running smt_filter
boehmes
parents: 40166
diff changeset
    27
  type solver = bool option -> Proof.context -> (int * thm) list ->
123b6fe379f6 honor choice of either local or remote SMT solver only for smt_filter and keep default behaviour for the SMT tactic; omit messages when running smt_filter
boehmes
parents: 40166
diff changeset
    28
    int list * thm
40162
7f58a9a843c2 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents: 40161
diff changeset
    29
  val add_solver: solver_config -> theory -> theory
40424
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents: 40357
diff changeset
    30
  val solver_of: Proof.context -> solver
40166
d3bc972b7d9d optionally force the remote version of an SMT solver to be executed
boehmes
parents: 40165
diff changeset
    31
  val is_locally_installed: Proof.context -> bool
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    32
40162
7f58a9a843c2 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents: 40161
diff changeset
    33
  (*filter*)
40164
57f5db2a48a3 added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents: 40162
diff changeset
    34
  val smt_filter: bool -> Time.time -> Proof.state -> ('a * thm) list -> int ->
40424
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents: 40357
diff changeset
    35
    {outcome: SMT_Failure.failure option, used_facts: 'a list,
40197
d99f74ed95be capture out-of-memory warnings of Z3 and turn them into proper exceptions; be more precise about SMT solver run-time: return NONE instead of ~1
boehmes
parents: 40196
diff changeset
    36
    run_time_in_msecs: int option}
40161
539d07b00e5f keep track of theorems initially given to SMT (even if they are rewritten); provide interface to filter theorems necessary for SMT proofs
boehmes
parents: 39811
diff changeset
    37
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    38
  (*tactic*)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    39
  val smt_tac': bool -> Proof.context -> thm list -> int -> Tactical.tactic
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    40
  val smt_tac: Proof.context -> thm list -> int -> Tactical.tactic
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    41
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    42
  (*setup*)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    43
  val setup: theory -> theory
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    44
end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    45
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    46
structure SMT_Solver: SMT_SOLVER =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    47
struct
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    48
40424
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents: 40357
diff changeset
    49
structure C = SMT_Config
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    50
40162
7f58a9a843c2 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents: 40161
diff changeset
    51
40424
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents: 40357
diff changeset
    52
(* configuration *)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    53
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    54
type interface = {
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    55
  extra_norm: SMT_Normalize.extra_norm,
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    56
  translate: SMT_Translate.config }
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    57
40162
7f58a9a843c2 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents: 40161
diff changeset
    58
datatype outcome = Unsat | Sat | Unknown
7f58a9a843c2 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents: 40161
diff changeset
    59
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    60
type solver_config = {
40162
7f58a9a843c2 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents: 40161
diff changeset
    61
  name: string,
7f58a9a843c2 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents: 40161
diff changeset
    62
  env_var: string,
7f58a9a843c2 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents: 40161
diff changeset
    63
  is_remote: bool,
7f58a9a843c2 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents: 40161
diff changeset
    64
  options: Proof.context -> string list,
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    65
  interface: interface,
40162
7f58a9a843c2 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents: 40161
diff changeset
    66
  outcome: string -> string list -> outcome * string list,
7f58a9a843c2 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents: 40161
diff changeset
    67
  cex_parser: (Proof.context -> SMT_Translate.recon -> string list ->
7f58a9a843c2 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents: 40161
diff changeset
    68
    term list) option,
7f58a9a843c2 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents: 40161
diff changeset
    69
  reconstruct: (Proof.context -> SMT_Translate.recon -> string list ->
7f58a9a843c2 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents: 40161
diff changeset
    70
    (int list * thm) * Proof.context) option }
36898
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
(* interface to external solvers *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    74
40166
d3bc972b7d9d optionally force the remote version of an SMT solver to be executed
boehmes
parents: 40165
diff changeset
    75
fun get_local_solver env_var =
d3bc972b7d9d optionally force the remote version of an SMT solver to be executed
boehmes
parents: 40165
diff changeset
    76
  let val local_solver = getenv env_var
d3bc972b7d9d optionally force the remote version of an SMT solver to be executed
boehmes
parents: 40165
diff changeset
    77
  in if local_solver <> "" then SOME local_solver else NONE end
d3bc972b7d9d optionally force the remote version of an SMT solver to be executed
boehmes
parents: 40165
diff changeset
    78
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    79
local
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    80
40196
123b6fe379f6 honor choice of either local or remote SMT solver only for smt_filter and keep default behaviour for the SMT tactic; omit messages when running smt_filter
boehmes
parents: 40166
diff changeset
    81
fun choose (rm, env_var, is_remote, name) =
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    82
  let
40196
123b6fe379f6 honor choice of either local or remote SMT solver only for smt_filter and keep default behaviour for the SMT tactic; omit messages when running smt_filter
boehmes
parents: 40166
diff changeset
    83
    val force_local = (case rm of SOME false => true | _ => false)
123b6fe379f6 honor choice of either local or remote SMT solver only for smt_filter and keep default behaviour for the SMT tactic; omit messages when running smt_filter
boehmes
parents: 40166
diff changeset
    84
    val force_remote = (case rm of SOME true => true | _ => false)
40166
d3bc972b7d9d optionally force the remote version of an SMT solver to be executed
boehmes
parents: 40165
diff changeset
    85
    val lsolver = get_local_solver env_var
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    86
    val remote_url = getenv "REMOTE_SMT_URL"
40196
123b6fe379f6 honor choice of either local or remote SMT solver only for smt_filter and keep default behaviour for the SMT tactic; omit messages when running smt_filter
boehmes
parents: 40166
diff changeset
    87
    val trace = if is_some rm then K () else tracing
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    88
  in
40166
d3bc972b7d9d optionally force the remote version of an SMT solver to be executed
boehmes
parents: 40165
diff changeset
    89
    if not force_remote andalso is_some lsolver
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    90
    then 
40196
123b6fe379f6 honor choice of either local or remote SMT solver only for smt_filter and keep default behaviour for the SMT tactic; omit messages when running smt_filter
boehmes
parents: 40166
diff changeset
    91
     (trace ("Invoking local SMT solver " ^ quote (the lsolver) ^ " ...");
40166
d3bc972b7d9d optionally force the remote version of an SMT solver to be executed
boehmes
parents: 40165
diff changeset
    92
      [the lsolver])
40196
123b6fe379f6 honor choice of either local or remote SMT solver only for smt_filter and keep default behaviour for the SMT tactic; omit messages when running smt_filter
boehmes
parents: 40166
diff changeset
    93
    else if not force_local andalso is_remote
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    94
    then
40196
123b6fe379f6 honor choice of either local or remote SMT solver only for smt_filter and keep default behaviour for the SMT tactic; omit messages when running smt_filter
boehmes
parents: 40166
diff changeset
    95
     (trace ("Invoking remote SMT solver " ^ quote name ^ " at " ^
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    96
        quote remote_url ^ " ...");
40166
d3bc972b7d9d optionally force the remote version of an SMT solver to be executed
boehmes
parents: 40165
diff changeset
    97
      [getenv "REMOTE_SMT", name])
d3bc972b7d9d optionally force the remote version of an SMT solver to be executed
boehmes
parents: 40165
diff changeset
    98
    else if force_remote
40196
123b6fe379f6 honor choice of either local or remote SMT solver only for smt_filter and keep default behaviour for the SMT tactic; omit messages when running smt_filter
boehmes
parents: 40166
diff changeset
    99
    then error ("The SMT solver " ^ quote name ^ " is not remotely available.")
123b6fe379f6 honor choice of either local or remote SMT solver only for smt_filter and keep default behaviour for the SMT tactic; omit messages when running smt_filter
boehmes
parents: 40166
diff changeset
   100
    else error ("The SMT solver " ^ quote name ^ " has not been found " ^
123b6fe379f6 honor choice of either local or remote SMT solver only for smt_filter and keep default behaviour for the SMT tactic; omit messages when running smt_filter
boehmes
parents: 40166
diff changeset
   101
      "on this computer. Please set the Isabelle environment variable " ^
123b6fe379f6 honor choice of either local or remote SMT solver only for smt_filter and keep default behaviour for the SMT tactic; omit messages when running smt_filter
boehmes
parents: 40166
diff changeset
   102
      quote env_var ^ ".")
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   103
  end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   104
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   105
fun make_cmd solver args problem_path proof_path = space_implode " " (
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   106
  map File.shell_quote (solver @ args) @
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   107
  [File.shell_path problem_path, "2>&1", ">", File.shell_path proof_path])
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   108
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   109
fun run ctxt cmd args input =
40424
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents: 40357
diff changeset
   110
  (case C.certificates_of ctxt of
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   111
    NONE => Cache_IO.run (make_cmd (choose cmd) args) input
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   112
  | SOME certs =>
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   113
      (case Cache_IO.lookup certs input of
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   114
        (NONE, key) =>
40424
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents: 40357
diff changeset
   115
          if Config.get ctxt C.fixed
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   116
          then error ("Bad certificates cache: missing certificate")
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   117
          else Cache_IO.run_and_cache certs key (make_cmd (choose cmd) args)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   118
            input
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   119
      | (SOME output, _) =>
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   120
         (tracing ("Using cached certificate from " ^
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   121
            File.shell_path (Cache_IO.cache_path_of certs) ^ " ...");
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   122
          output)))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   123
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   124
in
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   125
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   126
fun run_solver ctxt cmd args input =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   127
  let
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   128
    fun pretty tag ls = Pretty.string_of (Pretty.big_list tag
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   129
      (map Pretty.str ls))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   130
40424
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents: 40357
diff changeset
   131
    val _ = C.trace_msg ctxt (pretty "Problem:" o split_lines) input
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   132
40424
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents: 40357
diff changeset
   133
    val (res, err) = C.with_timeout ctxt (run ctxt cmd args) input
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents: 40357
diff changeset
   134
    val _ = C.trace_msg ctxt (pretty "Solver:") err
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   135
39811
0659e84bdc5f chop_while replace drop_while and take_while
haftmann
parents: 39809
diff changeset
   136
    val ls = rev (snd (chop_while (equal "") (rev res)))
40424
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents: 40357
diff changeset
   137
    val _ = C.trace_msg ctxt (pretty "Result:") ls
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   138
  in ls end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   139
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   140
end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   141
40424
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents: 40357
diff changeset
   142
fun trace_assms ctxt = C.trace_msg ctxt (Pretty.string_of o
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents: 40357
diff changeset
   143
  Pretty.big_list "Assertions:" o map (Display.pretty_thm ctxt o snd))
40198
8d470bbaafd7 trace assumptions before giving them to the SMT solver
boehmes
parents: 40197
diff changeset
   144
36940
b4417ddad979 make SML/NJ happy
blanchet
parents: 36899
diff changeset
   145
fun trace_recon_data ctxt ({typs, terms, ...} : SMT_Translate.recon) =
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   146
  let
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   147
    fun pretty_eq n p = Pretty.block [Pretty.str n, Pretty.str " = ", p]
40424
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents: 40357
diff changeset
   148
    fun p_typ (n, T) = pretty_eq n (Syntax.pretty_typ ctxt T)
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents: 40357
diff changeset
   149
    fun p_term (n, t) = pretty_eq n (Syntax.pretty_term ctxt t)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   150
  in
40424
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents: 40357
diff changeset
   151
    C.trace_msg ctxt (fn () =>
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents: 40357
diff changeset
   152
      Pretty.string_of (Pretty.big_list "Names:" [
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents: 40357
diff changeset
   153
        Pretty.big_list "sorts:" (map p_typ (Symtab.dest typs)),
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents: 40357
diff changeset
   154
        Pretty.big_list "functions:" (map p_term (Symtab.dest terms))])) ()
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   155
  end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   156
40424
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents: 40357
diff changeset
   157
fun invoke translate_config name cmd options irules ctxt =
40162
7f58a9a843c2 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents: 40161
diff changeset
   158
  let
40424
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents: 40357
diff changeset
   159
    val args = C.solver_options_of ctxt @ options ctxt
40162
7f58a9a843c2 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents: 40161
diff changeset
   160
    val comments = ("solver: " ^ name) ::
40424
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents: 40357
diff changeset
   161
      ("timeout: " ^ Time.toString (seconds (Config.get ctxt C.timeout))) ::
40162
7f58a9a843c2 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents: 40161
diff changeset
   162
      "arguments:" :: args
7f58a9a843c2 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents: 40161
diff changeset
   163
  in
7f58a9a843c2 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents: 40161
diff changeset
   164
    irules
40198
8d470bbaafd7 trace assumptions before giving them to the SMT solver
boehmes
parents: 40197
diff changeset
   165
    |> tap (trace_assms ctxt)
40162
7f58a9a843c2 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents: 40161
diff changeset
   166
    |> SMT_Translate.translate translate_config ctxt comments
7f58a9a843c2 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents: 40161
diff changeset
   167
    ||> tap (trace_recon_data ctxt)
7f58a9a843c2 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents: 40161
diff changeset
   168
    |>> run_solver ctxt cmd args
7f58a9a843c2 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents: 40161
diff changeset
   169
    |> rpair ctxt
7f58a9a843c2 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents: 40161
diff changeset
   170
  end
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   171
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   172
fun discharge_definitions thm =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   173
  if Thm.nprems_of thm = 0 then thm
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   174
  else discharge_definitions (@{thm reflexive} RS thm)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   175
40162
7f58a9a843c2 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents: 40161
diff changeset
   176
fun set_has_datatypes with_datatypes translate =
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   177
  let
40162
7f58a9a843c2 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents: 40161
diff changeset
   178
    val {prefixes, header, strict, builtins, serialize} = translate
7f58a9a843c2 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents: 40161
diff changeset
   179
    val {builtin_typ, builtin_num, builtin_fun, has_datatypes} = builtins
7f58a9a843c2 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents: 40161
diff changeset
   180
    val with_datatypes' = has_datatypes andalso with_datatypes
7f58a9a843c2 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents: 40161
diff changeset
   181
    val builtins' = {builtin_typ=builtin_typ, builtin_num=builtin_num,
7f58a9a843c2 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents: 40161
diff changeset
   182
      builtin_fun=builtin_fun, has_datatypes=with_datatypes}
7f58a9a843c2 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents: 40161
diff changeset
   183
    val translate' = {prefixes=prefixes, header=header, strict=strict,
7f58a9a843c2 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents: 40161
diff changeset
   184
      builtins=builtins', serialize=serialize}
7f58a9a843c2 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents: 40161
diff changeset
   185
  in (with_datatypes', translate') end
7f58a9a843c2 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents: 40161
diff changeset
   186
40164
57f5db2a48a3 added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents: 40162
diff changeset
   187
fun trace_assumptions ctxt irules idxs =
57f5db2a48a3 added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents: 40162
diff changeset
   188
  let
57f5db2a48a3 added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents: 40162
diff changeset
   189
    val thms = filter (fn i => i >= 0) idxs
57f5db2a48a3 added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents: 40162
diff changeset
   190
      |> map_filter (AList.lookup (op =) irules)
57f5db2a48a3 added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents: 40162
diff changeset
   191
  in
40424
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents: 40357
diff changeset
   192
    if Config.get ctxt C.trace_used_facts andalso length thms > 0
40164
57f5db2a48a3 added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents: 40162
diff changeset
   193
    then
57f5db2a48a3 added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents: 40162
diff changeset
   194
      tracing (Pretty.string_of (Pretty.big_list "SMT used facts:"
57f5db2a48a3 added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents: 40162
diff changeset
   195
        (map (Display.pretty_thm ctxt) thms)))
57f5db2a48a3 added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents: 40162
diff changeset
   196
    else ()
57f5db2a48a3 added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents: 40162
diff changeset
   197
  end
57f5db2a48a3 added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents: 40162
diff changeset
   198
40196
123b6fe379f6 honor choice of either local or remote SMT solver only for smt_filter and keep default behaviour for the SMT tactic; omit messages when running smt_filter
boehmes
parents: 40166
diff changeset
   199
fun gen_solver name info rm ctxt irules =
40162
7f58a9a843c2 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents: 40161
diff changeset
   200
  let
40424
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents: 40357
diff changeset
   201
    val {env_var, is_remote, options, interface, reconstruct} = info
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   202
    val {extra_norm, translate} = interface
40162
7f58a9a843c2 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents: 40161
diff changeset
   203
    val (with_datatypes, translate') =
40424
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents: 40357
diff changeset
   204
      set_has_datatypes (Config.get ctxt C.datatypes) translate
40196
123b6fe379f6 honor choice of either local or remote SMT solver only for smt_filter and keep default behaviour for the SMT tactic; omit messages when running smt_filter
boehmes
parents: 40166
diff changeset
   205
    val cmd = (rm, env_var, is_remote, name)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   206
  in
40162
7f58a9a843c2 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents: 40161
diff changeset
   207
    (irules, ctxt)
40424
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents: 40357
diff changeset
   208
    |-> SMT_Normalize.normalize extra_norm with_datatypes
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents: 40357
diff changeset
   209
    |-> invoke translate' name cmd options
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   210
    |-> reconstruct
40161
539d07b00e5f keep track of theorems initially given to SMT (even if they are rewritten); provide interface to filter theorems necessary for SMT proofs
boehmes
parents: 39811
diff changeset
   211
    |-> (fn (idxs, thm) => fn ctxt' => thm
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   212
    |> singleton (ProofContext.export ctxt' ctxt)
40161
539d07b00e5f keep track of theorems initially given to SMT (even if they are rewritten); provide interface to filter theorems necessary for SMT proofs
boehmes
parents: 39811
diff changeset
   213
    |> discharge_definitions
40164
57f5db2a48a3 added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents: 40162
diff changeset
   214
    |> tap (fn _ => trace_assumptions ctxt irules idxs)
40161
539d07b00e5f keep track of theorems initially given to SMT (even if they are rewritten); provide interface to filter theorems necessary for SMT proofs
boehmes
parents: 39811
diff changeset
   215
    |> pair idxs)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   216
  end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   217
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   218
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   219
40424
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents: 40357
diff changeset
   220
(* registry *)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   221
40196
123b6fe379f6 honor choice of either local or remote SMT solver only for smt_filter and keep default behaviour for the SMT tactic; omit messages when running smt_filter
boehmes
parents: 40166
diff changeset
   222
type solver = bool option -> Proof.context -> (int * thm) list -> int list * thm
40162
7f58a9a843c2 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents: 40161
diff changeset
   223
7f58a9a843c2 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents: 40161
diff changeset
   224
type solver_info = {
7f58a9a843c2 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents: 40161
diff changeset
   225
  env_var: string,
7f58a9a843c2 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents: 40161
diff changeset
   226
  is_remote: bool,
7f58a9a843c2 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents: 40161
diff changeset
   227
  options: Proof.context -> string list,
7f58a9a843c2 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents: 40161
diff changeset
   228
  interface: interface,
7f58a9a843c2 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents: 40161
diff changeset
   229
  reconstruct: string list * SMT_Translate.recon -> Proof.context ->
7f58a9a843c2 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents: 40161
diff changeset
   230
    (int list * thm) * Proof.context }
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   231
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   232
structure Solvers = Generic_Data
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   233
(
40162
7f58a9a843c2 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents: 40161
diff changeset
   234
  type T = solver_info Symtab.table
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   235
  val empty = Symtab.empty
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   236
  val extend = I
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   237
  fun merge data = Symtab.merge (K true) data
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   238
    handle Symtab.DUP name => error ("Duplicate SMT solver: " ^ quote name)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   239
)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   240
40162
7f58a9a843c2 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents: 40161
diff changeset
   241
local
7f58a9a843c2 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents: 40161
diff changeset
   242
  fun finish outcome cex_parser reconstruct ocl (output, recon) ctxt =
7f58a9a843c2 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents: 40161
diff changeset
   243
    (case outcome output of
7f58a9a843c2 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents: 40161
diff changeset
   244
      (Unsat, ls) =>
40424
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents: 40357
diff changeset
   245
        if not (Config.get ctxt C.oracle) andalso is_some reconstruct
40162
7f58a9a843c2 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents: 40161
diff changeset
   246
        then the reconstruct ctxt recon ls
7f58a9a843c2 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents: 40161
diff changeset
   247
        else (([], ocl ()), ctxt)
7f58a9a843c2 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents: 40161
diff changeset
   248
    | (result, ls) =>
7f58a9a843c2 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents: 40161
diff changeset
   249
        let val ts = (case cex_parser of SOME f => f ctxt recon ls | _ => [])
40424
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents: 40357
diff changeset
   250
        in
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents: 40357
diff changeset
   251
          raise SMT_Failure.SMT (SMT_Failure.Counterexample (result = Sat, ts))
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents: 40357
diff changeset
   252
        end)
40162
7f58a9a843c2 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents: 40161
diff changeset
   253
in
7f58a9a843c2 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents: 40161
diff changeset
   254
7f58a9a843c2 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents: 40161
diff changeset
   255
fun add_solver cfg =
7f58a9a843c2 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents: 40161
diff changeset
   256
  let
7f58a9a843c2 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents: 40161
diff changeset
   257
    val {name, env_var, is_remote, options, interface, outcome, cex_parser,
7f58a9a843c2 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents: 40161
diff changeset
   258
      reconstruct} = cfg
7f58a9a843c2 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents: 40161
diff changeset
   259
7f58a9a843c2 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents: 40161
diff changeset
   260
    fun core_oracle () = @{cprop False}
7f58a9a843c2 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents: 40161
diff changeset
   261
7f58a9a843c2 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents: 40161
diff changeset
   262
    fun solver ocl = { env_var=env_var, is_remote=is_remote, options=options,
40424
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents: 40357
diff changeset
   263
      interface=interface,
40162
7f58a9a843c2 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents: 40161
diff changeset
   264
      reconstruct=finish (outcome name) cex_parser reconstruct ocl }
7f58a9a843c2 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents: 40161
diff changeset
   265
  in
7f58a9a843c2 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents: 40161
diff changeset
   266
    Thm.add_oracle (Binding.name name, core_oracle) #-> (fn (_, ocl) =>
7f58a9a843c2 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents: 40161
diff changeset
   267
    Context.theory_map (Solvers.map (Symtab.update_new (name, solver ocl)))) #>
40424
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents: 40357
diff changeset
   268
    Context.theory_map (C.add_solver name)
40162
7f58a9a843c2 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents: 40161
diff changeset
   269
  end
7f58a9a843c2 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents: 40161
diff changeset
   270
7f58a9a843c2 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents: 40161
diff changeset
   271
end
7f58a9a843c2 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents: 40161
diff changeset
   272
40424
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents: 40357
diff changeset
   273
fun name_and_solver_of ctxt =
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents: 40357
diff changeset
   274
  let val name = C.solver_of ctxt
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents: 40357
diff changeset
   275
  in (name, the (Symtab.lookup (Solvers.get (Context.Proof ctxt)) name)) end
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   276
40424
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents: 40357
diff changeset
   277
fun solver_of ctxt =
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents: 40357
diff changeset
   278
  let val (name, raw_solver) = name_and_solver_of ctxt
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents: 40357
diff changeset
   279
  in gen_solver name raw_solver end
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   280
40166
d3bc972b7d9d optionally force the remote version of an SMT solver to be executed
boehmes
parents: 40165
diff changeset
   281
fun is_locally_installed ctxt =
40424
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents: 40357
diff changeset
   282
  let val (_, {env_var, ...}) = name_and_solver_of ctxt
40166
d3bc972b7d9d optionally force the remote version of an SMT solver to be executed
boehmes
parents: 40165
diff changeset
   283
  in is_some (get_local_solver env_var) end
d3bc972b7d9d optionally force the remote version of an SMT solver to be executed
boehmes
parents: 40165
diff changeset
   284
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   285
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   286
40424
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents: 40357
diff changeset
   287
(* filter *)
40161
539d07b00e5f keep track of theorems initially given to SMT (even if they are rewritten); provide interface to filter theorems necessary for SMT proofs
boehmes
parents: 39811
diff changeset
   288
539d07b00e5f keep track of theorems initially given to SMT (even if they are rewritten); provide interface to filter theorems necessary for SMT proofs
boehmes
parents: 39811
diff changeset
   289
val has_topsort = Term.exists_type (Term.exists_subtype (fn
539d07b00e5f keep track of theorems initially given to SMT (even if they are rewritten); provide interface to filter theorems necessary for SMT proofs
boehmes
parents: 39811
diff changeset
   290
    TFree (_, []) => true
539d07b00e5f keep track of theorems initially given to SMT (even if they are rewritten); provide interface to filter theorems necessary for SMT proofs
boehmes
parents: 39811
diff changeset
   291
  | TVar (_, []) => true
539d07b00e5f keep track of theorems initially given to SMT (even if they are rewritten); provide interface to filter theorems necessary for SMT proofs
boehmes
parents: 39811
diff changeset
   292
  | _ => false))
539d07b00e5f keep track of theorems initially given to SMT (even if they are rewritten); provide interface to filter theorems necessary for SMT proofs
boehmes
parents: 39811
diff changeset
   293
40196
123b6fe379f6 honor choice of either local or remote SMT solver only for smt_filter and keep default behaviour for the SMT tactic; omit messages when running smt_filter
boehmes
parents: 40166
diff changeset
   294
fun smt_solver rm ctxt irules =
40161
539d07b00e5f keep track of theorems initially given to SMT (even if they are rewritten); provide interface to filter theorems necessary for SMT proofs
boehmes
parents: 39811
diff changeset
   295
  (* without this test, we would run into problems when atomizing the rules: *)
40424
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents: 40357
diff changeset
   296
  if exists (has_topsort o Thm.prop_of o snd) irules then
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents: 40357
diff changeset
   297
    raise SMT_Failure.SMT (SMT_Failure.Other_Failure ("proof state " ^
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents: 40357
diff changeset
   298
      "contains the universal sort {}"))
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents: 40357
diff changeset
   299
  else solver_of ctxt rm ctxt irules
40162
7f58a9a843c2 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents: 40161
diff changeset
   300
40196
123b6fe379f6 honor choice of either local or remote SMT solver only for smt_filter and keep default behaviour for the SMT tactic; omit messages when running smt_filter
boehmes
parents: 40166
diff changeset
   301
fun smt_filter run_remote time_limit st xrules i =
40162
7f58a9a843c2 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents: 40161
diff changeset
   302
  let
40199
2963511e121c use proper context
boehmes
parents: 40198
diff changeset
   303
    val {facts, goal, ...} = Proof.goal st
40164
57f5db2a48a3 added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents: 40162
diff changeset
   304
    val ctxt =
40199
2963511e121c use proper context
boehmes
parents: 40198
diff changeset
   305
      Proof.context_of st
40424
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents: 40357
diff changeset
   306
      |> Config.put C.oracle false
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents: 40357
diff changeset
   307
      |> Config.put C.timeout (Real.fromInt (Time.toSeconds time_limit))
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents: 40357
diff changeset
   308
      |> Config.put C.drop_bad_facts true
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents: 40357
diff changeset
   309
      |> Config.put C.filter_only_facts true
40357
82ebdd19c4a4 simulate more closely the behaviour of the tactic
boehmes
parents: 40332
diff changeset
   310
    val ({context=ctxt', prems, concl, ...}, _) = Subgoal.focus ctxt i goal
40162
7f58a9a843c2 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents: 40161
diff changeset
   311
    val cprop =
40357
82ebdd19c4a4 simulate more closely the behaviour of the tactic
boehmes
parents: 40332
diff changeset
   312
      concl
82ebdd19c4a4 simulate more closely the behaviour of the tactic
boehmes
parents: 40332
diff changeset
   313
      |> Thm.rhs_of o SMT_Normalize.atomize_conv ctxt'
40162
7f58a9a843c2 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents: 40161
diff changeset
   314
      |> Thm.capply @{cterm Trueprop} o Thm.capply @{cterm Not} o Thm.dest_arg
40357
82ebdd19c4a4 simulate more closely the behaviour of the tactic
boehmes
parents: 40332
diff changeset
   315
    val irs = map (pair ~1) (Thm.assume cprop :: prems @ facts)
40196
123b6fe379f6 honor choice of either local or remote SMT solver only for smt_filter and keep default behaviour for the SMT tactic; omit messages when running smt_filter
boehmes
parents: 40166
diff changeset
   316
    val rm = SOME run_remote
40162
7f58a9a843c2 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents: 40161
diff changeset
   317
  in
40161
539d07b00e5f keep track of theorems initially given to SMT (even if they are rewritten); provide interface to filter theorems necessary for SMT proofs
boehmes
parents: 39811
diff changeset
   318
    split_list xrules
40357
82ebdd19c4a4 simulate more closely the behaviour of the tactic
boehmes
parents: 40332
diff changeset
   319
    ||> distinct (op =) o fst o smt_solver rm ctxt' o append irs o map_index I
40164
57f5db2a48a3 added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents: 40162
diff changeset
   320
    |-> map_filter o try o nth
40197
d99f74ed95be capture out-of-memory warnings of Z3 and turn them into proper exceptions; be more precise about SMT solver run-time: return NONE instead of ~1
boehmes
parents: 40196
diff changeset
   321
    |> (fn xs => {outcome=NONE, used_facts=xs, run_time_in_msecs=NONE})
40162
7f58a9a843c2 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents: 40161
diff changeset
   322
  end
40424
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents: 40357
diff changeset
   323
  handle SMT_Failure.SMT fail => {outcome=SOME fail, used_facts=[],
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents: 40357
diff changeset
   324
    run_time_in_msecs=NONE}
40166
d3bc972b7d9d optionally force the remote version of an SMT solver to be executed
boehmes
parents: 40165
diff changeset
   325
  (* FIXME: measure runtime *)
40161
539d07b00e5f keep track of theorems initially given to SMT (even if they are rewritten); provide interface to filter theorems necessary for SMT proofs
boehmes
parents: 39811
diff changeset
   326
539d07b00e5f keep track of theorems initially given to SMT (even if they are rewritten); provide interface to filter theorems necessary for SMT proofs
boehmes
parents: 39811
diff changeset
   327
539d07b00e5f keep track of theorems initially given to SMT (even if they are rewritten); provide interface to filter theorems necessary for SMT proofs
boehmes
parents: 39811
diff changeset
   328
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   329
(* SMT tactic *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   330
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   331
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
   332
  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
   333
  THEN' Tactic.rtac @{thm ccontr}
40424
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents: 40357
diff changeset
   334
  THEN' SUBPROOF (fn {context=ctxt', prems, ...} =>
40165
boehmes
parents: 40164
diff changeset
   335
    let
40424
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents: 40357
diff changeset
   336
      fun solve irules = snd (smt_solver NONE ctxt' irules)
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents: 40357
diff changeset
   337
      val tag = "Solver " ^ C.solver_of ctxt' ^ ": "
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents: 40357
diff changeset
   338
      val str_of = SMT_Failure.string_of_failure ctxt'
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents: 40357
diff changeset
   339
      fun safe_solve irules =
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents: 40357
diff changeset
   340
        if pass_exns then SOME (solve irules)
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents: 40357
diff changeset
   341
        else (SOME (solve irules) handle SMT_Failure.SMT fail =>
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents: 40357
diff changeset
   342
          (C.trace_msg ctxt' (prefix tag o str_of) fail; NONE))
40165
boehmes
parents: 40164
diff changeset
   343
    in
40424
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents: 40357
diff changeset
   344
      safe_solve (map (pair ~1) (rules @ prems))
40165
boehmes
parents: 40164
diff changeset
   345
      |> (fn SOME thm => Tactic.rtac thm 1 | _ => Tactical.no_tac)
40166
d3bc972b7d9d optionally force the remote version of an SMT solver to be executed
boehmes
parents: 40165
diff changeset
   346
    end) ctxt
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   347
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   348
val smt_tac = smt_tac' false
40162
7f58a9a843c2 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents: 40161
diff changeset
   349
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   350
val smt_method =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   351
  Scan.optional Attrib.thms [] >>
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   352
  (fn thms => fn ctxt => METHOD (fn facts =>
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   353
    HEADGOAL (smt_tac ctxt (thms @ facts))))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   354
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   355
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   356
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   357
(* setup *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   358
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   359
val setup =
38808
89ae86205739 more antiquotations;
wenzelm
parents: 36960
diff changeset
   360
  Method.setup @{binding smt} smt_method
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   361
    "Applies an SMT solver to the current goal."
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   362
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   363
end