src/HOL/Tools/SMT/smt_solver.ML
author boehmes
Tue, 30 Nov 2010 18:22:43 +0100
changeset 40828 47ff261431c4
parent 40666 8db6c2b1591d
child 40940 ff805bb109d8
permissions -rw-r--r--
split up Z3 models into constraints on free variables and constant definitions; reduce Z3 models by replacing unknowns with free variables and constants from the goal; remove occurrences of the hidden constant fun_app from Z3 models
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 ->
40828
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40666
diff changeset
    22
      term list * term list) option,
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
    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 ->
40666
8db6c2b1591d try Metis to reconstruct SMT proofs, to increase success rate and reduce dependency on (often remote) SMT solvers or certificates
blanchet
parents: 40579
diff changeset
    35
    {outcome: SMT_Failure.failure option, used_facts: ('a * thm) 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 ->
40828
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40666
diff changeset
    68
    term list * term list) option,
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
    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
40578
2b098a549450 keep input and output files used to communicate with the SMT solver (for debugging purposes mainly)
boehmes
parents: 40561
diff changeset
   111
    NONE =>
2b098a549450 keep input and output files used to communicate with the SMT solver (for debugging purposes mainly)
boehmes
parents: 40561
diff changeset
   112
      if Config.get ctxt C.debug_files = "" then
2b098a549450 keep input and output files used to communicate with the SMT solver (for debugging purposes mainly)
boehmes
parents: 40561
diff changeset
   113
        Cache_IO.run (make_cmd (choose cmd) args) input
2b098a549450 keep input and output files used to communicate with the SMT solver (for debugging purposes mainly)
boehmes
parents: 40561
diff changeset
   114
      else
2b098a549450 keep input and output files used to communicate with the SMT solver (for debugging purposes mainly)
boehmes
parents: 40561
diff changeset
   115
        let
2b098a549450 keep input and output files used to communicate with the SMT solver (for debugging purposes mainly)
boehmes
parents: 40561
diff changeset
   116
          val base_path = Path.explode (Config.get ctxt C.debug_files)
2b098a549450 keep input and output files used to communicate with the SMT solver (for debugging purposes mainly)
boehmes
parents: 40561
diff changeset
   117
          val in_path = Path.ext "smt_in" base_path
2b098a549450 keep input and output files used to communicate with the SMT solver (for debugging purposes mainly)
boehmes
parents: 40561
diff changeset
   118
          val out_path = Path.ext "smt_out" base_path
2b098a549450 keep input and output files used to communicate with the SMT solver (for debugging purposes mainly)
boehmes
parents: 40561
diff changeset
   119
        in
2b098a549450 keep input and output files used to communicate with the SMT solver (for debugging purposes mainly)
boehmes
parents: 40561
diff changeset
   120
          Cache_IO.raw_run (make_cmd (choose cmd) args) input in_path out_path 
2b098a549450 keep input and output files used to communicate with the SMT solver (for debugging purposes mainly)
boehmes
parents: 40561
diff changeset
   121
        end
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   122
  | SOME certs =>
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   123
      (case Cache_IO.lookup certs input of
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   124
        (NONE, key) =>
40538
b8482ff0bc92 check the return code of the SMT solver and raise an exception if the prover failed
boehmes
parents: 40515
diff changeset
   125
          if Config.get ctxt C.fixed then
b8482ff0bc92 check the return code of the SMT solver and raise an exception if the prover failed
boehmes
parents: 40515
diff changeset
   126
            error ("Bad certificates cache: missing certificate")
b8482ff0bc92 check the return code of the SMT solver and raise an exception if the prover failed
boehmes
parents: 40515
diff changeset
   127
          else
b8482ff0bc92 check the return code of the SMT solver and raise an exception if the prover failed
boehmes
parents: 40515
diff changeset
   128
            Cache_IO.run_and_cache certs key (make_cmd (choose cmd) args) input
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   129
      | (SOME output, _) =>
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   130
         (tracing ("Using cached certificate from " ^
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   131
            File.shell_path (Cache_IO.cache_path_of certs) ^ " ...");
40550
f84c664ece8e trace more solver output before raising an exception due to a non-zero return code (avoids truncating potential counterexamples produced by Z3)
boehmes
parents: 40538
diff changeset
   132
          output)))
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   133
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   134
in
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_solver ctxt cmd args input =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   137
  let
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   138
    fun pretty tag ls = Pretty.string_of (Pretty.big_list tag
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   139
      (map Pretty.str ls))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   140
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
   141
    val _ = C.trace_msg ctxt (pretty "Problem:" o split_lines) input
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   142
40550
f84c664ece8e trace more solver output before raising an exception due to a non-zero return code (avoids truncating potential counterexamples produced by Z3)
boehmes
parents: 40538
diff changeset
   143
    val {redirected_output=res, output=err, return_code} =
f84c664ece8e trace more solver output before raising an exception due to a non-zero return code (avoids truncating potential counterexamples produced by Z3)
boehmes
parents: 40538
diff changeset
   144
      C.with_timeout ctxt (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
   145
    val _ = C.trace_msg ctxt (pretty "Solver:") err
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   146
39811
0659e84bdc5f chop_while replace drop_while and take_while
haftmann
parents: 39809
diff changeset
   147
    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
   148
    val _ = C.trace_msg ctxt (pretty "Result:") ls
40550
f84c664ece8e trace more solver output before raising an exception due to a non-zero return code (avoids truncating potential counterexamples produced by Z3)
boehmes
parents: 40538
diff changeset
   149
f84c664ece8e trace more solver output before raising an exception due to a non-zero return code (avoids truncating potential counterexamples produced by Z3)
boehmes
parents: 40538
diff changeset
   150
    val _ = null ls andalso return_code <> 0 andalso
40561
0125cbb5d3c7 renamed SMT failure: Abnormal_Termination is indeed more appropriate than Solver_Crashed
boehmes
parents: 40560
diff changeset
   151
      raise SMT_Failure.SMT (SMT_Failure.Abnormal_Termination return_code)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   152
  in ls end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   153
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   154
end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   155
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
   156
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
   157
  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
   158
36940
b4417ddad979 make SML/NJ happy
blanchet
parents: 36899
diff changeset
   159
fun trace_recon_data ctxt ({typs, terms, ...} : SMT_Translate.recon) =
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   160
  let
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   161
    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
   162
    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
   163
    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
   164
  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
   165
    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
   166
      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
   167
        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
   168
        Pretty.big_list "functions:" (map p_term (Symtab.dest terms))])) ()
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   169
  end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   170
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
   171
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
   172
  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
   173
    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
   174
    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
   175
      ("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
   176
      "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
   177
  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
   178
    irules
40198
8d470bbaafd7 trace assumptions before giving them to the SMT solver
boehmes
parents: 40197
diff changeset
   179
    |> 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
   180
    |> 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
   181
    ||> 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
   182
    |>> 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
   183
    |> 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
   184
  end
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   185
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   186
fun discharge_definitions thm =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   187
  if Thm.nprems_of thm = 0 then thm
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   188
  else discharge_definitions (@{thm reflexive} RS thm)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   189
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
   190
fun set_has_datatypes with_datatypes translate =
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   191
  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
   192
    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
   193
    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
   194
    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
   195
    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
   196
      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
   197
    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
   198
      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
   199
  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
   200
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
   201
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
   202
  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
   203
    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
   204
      |> 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
   205
  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
   206
    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
   207
    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
   208
      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
   209
        (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
   210
    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
   211
  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
   212
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
   213
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
   214
  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
   215
    val {env_var, is_remote, options, interface, reconstruct} = info
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   216
    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
   217
    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
   218
      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
   219
    val cmd = (rm, env_var, is_remote, name)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   220
  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
   221
    (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
   222
    |-> 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
   223
    |-> invoke translate' name cmd options
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   224
    |-> 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
   225
    |-> (fn (idxs, thm) => fn ctxt' => thm
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   226
    |> 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
   227
    |> 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
   228
    |> 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
   229
    |> pair idxs)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   230
  end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   231
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   232
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   233
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
   234
(* registry *)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   235
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
   236
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
   237
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
   238
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
   239
  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
   240
  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
   241
  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
   242
  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
   243
  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
   244
    (int list * thm) * Proof.context }
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   245
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   246
structure Solvers = Generic_Data
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   247
(
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
   248
  type T = solver_info Symtab.table
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   249
  val empty = Symtab.empty
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   250
  val extend = I
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   251
  fun merge data = Symtab.merge (K true) data
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   252
    handle Symtab.DUP name => error ("Duplicate SMT solver: " ^ quote name)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   253
)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   254
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
   255
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
   256
  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
   257
    (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
   258
      (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
   259
        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
   260
        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
   261
        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
   262
    | (result, ls) =>
40828
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40666
diff changeset
   263
        let
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40666
diff changeset
   264
          val (ts, us) =
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40666
diff changeset
   265
            (case cex_parser of SOME f => f ctxt recon ls | _ => ([], []))
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40666
diff changeset
   266
         in
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40666
diff changeset
   267
          raise SMT_Failure.SMT (SMT_Failure.Counterexample {
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40666
diff changeset
   268
            is_real_cex = (result = Sat),
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40666
diff changeset
   269
            free_constraints = ts,
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40666
diff changeset
   270
            const_defs = us})
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
   271
        end)
40579
98ebd2300823 use the const antiquotation for constants (this checks that the constant is declared, whereas the more general term antiquotation treats undeclared names as free variable)
boehmes
parents: 40578
diff changeset
   272
98ebd2300823 use the const antiquotation for constants (this checks that the constant is declared, whereas the more general term antiquotation treats undeclared names as free variable)
boehmes
parents: 40578
diff changeset
   273
  val cfalse = Thm.cterm_of @{theory} (@{const Trueprop} $ @{const 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
   274
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
   275
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
   276
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
   277
  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
   278
    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
   279
      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
   280
40579
98ebd2300823 use the const antiquotation for constants (this checks that the constant is declared, whereas the more general term antiquotation treats undeclared names as free variable)
boehmes
parents: 40578
diff changeset
   281
    fun core_oracle () = cfalse
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
   282
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
   283
    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
   284
      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
   285
      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
   286
  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
   287
    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
   288
    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
   289
    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
   290
  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
   291
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
   292
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
   293
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
   294
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
   295
  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
   296
  in (name, the (Symtab.lookup (Solvers.get (Context.Proof ctxt)) name)) end
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   297
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
   298
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
   299
  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
   300
  in gen_solver name raw_solver end
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   301
40166
d3bc972b7d9d optionally force the remote version of an SMT solver to be executed
boehmes
parents: 40165
diff changeset
   302
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
   303
  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
   304
  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
   305
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   306
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   307
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
   308
(* 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
   309
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
   310
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
   311
    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
   312
  | 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
   313
  | _ => 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
   314
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
   315
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
   316
  (* 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
   317
  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
   318
    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
   319
      "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
   320
  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
   321
40579
98ebd2300823 use the const antiquotation for constants (this checks that the constant is declared, whereas the more general term antiquotation treats undeclared names as free variable)
boehmes
parents: 40578
diff changeset
   322
val cnot = Thm.cterm_of @{theory} @{const Not}
98ebd2300823 use the const antiquotation for constants (this checks that the constant is declared, whereas the more general term antiquotation treats undeclared names as free variable)
boehmes
parents: 40578
diff changeset
   323
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
   324
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
   325
  let
40199
2963511e121c use proper context
boehmes
parents: 40198
diff changeset
   326
    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
   327
    val ctxt =
40199
2963511e121c use proper context
boehmes
parents: 40198
diff changeset
   328
      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
   329
      |> Config.put C.oracle false
40560
b57f7fee72ee honour timeouts which are not rounded to full seconds
boehmes
parents: 40550
diff changeset
   330
      |> Config.put C.timeout (Time.toReal time_limit)
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
   331
      |> 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
   332
      |> Config.put C.filter_only_facts true
40357
82ebdd19c4a4 simulate more closely the behaviour of the tactic
boehmes
parents: 40332
diff changeset
   333
    val ({context=ctxt', prems, concl, ...}, _) = Subgoal.focus ctxt i goal
40579
98ebd2300823 use the const antiquotation for constants (this checks that the constant is declared, whereas the more general term antiquotation treats undeclared names as free variable)
boehmes
parents: 40578
diff changeset
   334
    fun negate ct = Thm.dest_comb ct ||> Thm.capply cnot |-> Thm.capply
98ebd2300823 use the const antiquotation for constants (this checks that the constant is declared, whereas the more general term antiquotation treats undeclared names as free variable)
boehmes
parents: 40578
diff changeset
   335
    val cprop = negate (Thm.rhs_of (SMT_Normalize.atomize_conv ctxt' concl))
40357
82ebdd19c4a4 simulate more closely the behaviour of the tactic
boehmes
parents: 40332
diff changeset
   336
    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
   337
    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
   338
  in
40666
8db6c2b1591d try Metis to reconstruct SMT proofs, to increase success rate and reduce dependency on (often remote) SMT solvers or certificates
blanchet
parents: 40579
diff changeset
   339
    (xrules, map snd xrules)
40357
82ebdd19c4a4 simulate more closely the behaviour of the tactic
boehmes
parents: 40332
diff changeset
   340
    ||> 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
   341
    |-> 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
   342
    |> (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
   343
  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
   344
  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
   345
    run_time_in_msecs=NONE}
40166
d3bc972b7d9d optionally force the remote version of an SMT solver to be executed
boehmes
parents: 40165
diff changeset
   346
  (* 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
   347
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
   348
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
   349
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   350
(* SMT tactic *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   351
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   352
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
   353
  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
   354
  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
   355
  THEN' SUBPROOF (fn {context=ctxt', prems, ...} =>
40165
boehmes
parents: 40164
diff changeset
   356
    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
   357
      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
   358
      val tag = "Solver " ^ C.solver_of ctxt' ^ ": "
40828
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40666
diff changeset
   359
      val str_of = prefix tag o SMT_Failure.string_of_failure 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
   360
      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
   361
        if pass_exns then SOME (solve irules)
40515
25f266144206 turned SMT counterexamples into verbose messages (they had been swallowed before, following the state of smt_trace -- which is off by default), because they might be useful for the user
boehmes
parents: 40425
diff changeset
   362
        else (SOME (solve irules)
25f266144206 turned SMT counterexamples into verbose messages (they had been swallowed before, following the state of smt_trace -- which is off by default), because they might be useful for the user
boehmes
parents: 40425
diff changeset
   363
          handle
25f266144206 turned SMT counterexamples into verbose messages (they had been swallowed before, following the state of smt_trace -- which is off by default), because they might be useful for the user
boehmes
parents: 40425
diff changeset
   364
            SMT_Failure.SMT (fail as SMT_Failure.Counterexample _) =>
40828
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40666
diff changeset
   365
              (C.verbose_msg ctxt' str_of fail; NONE)
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40666
diff changeset
   366
          | SMT_Failure.SMT fail => (C.trace_msg ctxt' str_of fail; NONE))
40165
boehmes
parents: 40164
diff changeset
   367
    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
   368
      safe_solve (map (pair ~1) (rules @ prems))
40165
boehmes
parents: 40164
diff changeset
   369
      |> (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
   370
    end) ctxt
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   371
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   372
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
   373
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   374
val smt_method =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   375
  Scan.optional Attrib.thms [] >>
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   376
  (fn thms => fn ctxt => METHOD (fn facts =>
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   377
    HEADGOAL (smt_tac ctxt (thms @ facts))))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   378
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   379
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   380
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   381
(* setup *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   382
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   383
val setup =
38808
89ae86205739 more antiquotations;
wenzelm
parents: 36960
diff changeset
   384
  Method.setup @{binding smt} smt_method
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   385
    "Applies an SMT solver to the current goal."
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   386
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   387
end