src/HOL/Tools/SMT/smt_solver.ML
author boehmes
Tue, 26 Oct 2010 11:45:12 +0200
changeset 40162 7f58a9a843c2
parent 40161 539d07b00e5f
child 40164 57f5db2a48a3
permissions -rw-r--r--
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
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
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
     9
  datatype failure =
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
    10
    Counterexample of bool * term 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
    11
    Time_Out |
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
    12
    Other_Failure of 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
    13
  val string_of_failure: Proof.context -> failure -> 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
    14
  exception SMT of failure
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    15
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    16
  type interface = {
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    17
    extra_norm: SMT_Normalize.extra_norm,
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    18
    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
    19
  datatype outcome = Unsat | Sat | Unknown
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    20
  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
    21
    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
    22
    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
    23
    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
    24
    options: Proof.context -> string list,
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    25
    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
    26
    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
    27
    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
    28
      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
    29
    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
    30
      (int list * thm) * Proof.context) option }
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    31
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    32
  (*options*)
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
  val oracle: bool Config.T
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
    34
  val datatypes: bool Config.T
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    35
  val timeout: int Config.T
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    36
  val with_timeout: Proof.context -> ('a -> 'b) -> 'a -> 'b
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    37
  val trace: bool Config.T
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    38
  val trace_msg: Proof.context -> ('a -> string) -> 'a -> unit
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
    39
  val trace_used_facts: bool Config.T
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    40
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    41
  (*certificates*)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    42
  val fixed_certificates: bool Config.T
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    43
  val select_certificates: string -> Context.generic -> Context.generic
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    44
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    45
  (*solvers*)
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
    46
  type solver = 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
    47
  val add_solver: solver_config -> theory -> theory
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
    48
  val set_solver_options: string -> string -> Context.generic ->
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
    49
    Context.generic
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
    50
  val all_solver_names_of: Context.generic -> string list
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    51
  val solver_name_of: Context.generic -> string
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    52
  val select_solver: string -> Context.generic -> Context.generic
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    53
  val solver_of: Context.generic -> solver
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    54
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
    55
  (*filter*)
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
    56
  val smt_filter: Proof.state -> int -> ('a * thm) 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
    57
    'a list * failure 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
    58
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    59
  (*tactic*)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    60
  val smt_tac': bool -> Proof.context -> thm list -> int -> Tactical.tactic
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    61
  val smt_tac: Proof.context -> thm list -> int -> Tactical.tactic
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    62
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    63
  (*setup*)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    64
  val setup: theory -> theory
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    65
  val print_setup: Context.generic -> unit
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    66
end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    67
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    68
structure SMT_Solver: SMT_SOLVER =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    69
struct
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    70
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
    71
datatype failure =
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
    72
  Counterexample of bool * term 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
    73
  Time_Out |
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
    74
  Other_Failure of string
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    75
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
    76
fun string_of_failure ctxt (Counterexample (real, ex)) =
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
    77
      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
    78
        val msg = if real then "Counterexample found"
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
    79
          else "Potential counterexample found"
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
    80
      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
    81
        if null ex then msg ^ "."
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
    82
        else Pretty.string_of (Pretty.big_list (msg ^ ":")
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
    83
          (map (Syntax.pretty_term ctxt) ex))
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
    84
      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
    85
  | string_of_failure _ Time_Out = "Time out."
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
    86
  | string_of_failure _ (Other_Failure msg) = msg
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
    87
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
    88
exception SMT of failure
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    89
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    90
type interface = {
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    91
  extra_norm: SMT_Normalize.extra_norm,
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    92
  translate: SMT_Translate.config }
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    93
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
    94
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
    95
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    96
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
    97
  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
    98
  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
    99
  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
   100
  options: Proof.context -> string list,
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   101
  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
   102
  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
   103
  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
   104
    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
   105
  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
   106
    (int list * thm) * Proof.context) option }
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   107
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   108
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   109
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   110
(* SMT options *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   111
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
   112
val (oracle, setup_oracle) = Attrib.config_bool "smt_oracle" (K true)
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
   113
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
   114
val (datatypes, setup_datatypes) = Attrib.config_bool "smt_datatypes" (K 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
   115
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   116
val (timeout, setup_timeout) = Attrib.config_int "smt_timeout" (K 30)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   117
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   118
fun with_timeout ctxt f x =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   119
  TimeLimit.timeLimit (Time.fromSeconds (Config.get ctxt timeout)) f x
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
   120
  handle TimeLimit.TimeOut => raise SMT Time_Out
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   121
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   122
val (trace, setup_trace) = Attrib.config_bool "smt_trace" (K false)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   123
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   124
fun trace_msg ctxt f x =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   125
  if Config.get ctxt trace then tracing (f x) else ()
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   126
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
   127
val (trace_used_facts, setup_trace_used_facts) =
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
   128
  Attrib.config_bool "smt_trace_used_facts" (K false)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   129
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   130
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   131
(* SMT certificates *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   132
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   133
val (fixed_certificates, setup_fixed_certificates) =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   134
  Attrib.config_bool "smt_fixed" (K false)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   135
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   136
structure Certificates = Generic_Data
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   137
(
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   138
  type T = Cache_IO.cache option
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   139
  val empty = NONE
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   140
  val extend = I
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   141
  fun merge (s, _) = s
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   142
)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   143
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   144
val get_certificates_path =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   145
  Option.map (Cache_IO.cache_path_of) o Certificates.get
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   146
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   147
fun select_certificates name = Certificates.put (
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   148
  if name = "" then NONE
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   149
  else SOME (Cache_IO.make (Path.explode name)))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   150
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   151
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   152
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   153
(* interface to external solvers *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   154
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   155
local
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   156
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
   157
fun choose (env_var, is_remote, remote_name) =
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   158
  let
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   159
    val local_solver = getenv env_var
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   160
    val remote_url = getenv "REMOTE_SMT_URL"
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   161
  in
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   162
    if local_solver <> ""
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   163
    then 
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   164
     (tracing ("Invoking local SMT solver " ^ quote local_solver ^ " ...");
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   165
      [local_solver])
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
    else if is_remote
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   167
    then
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
   168
     (tracing ("Invoking remote SMT solver " ^ quote remote_name ^ " at " ^
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   169
        quote remote_url ^ " ...");
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
   170
      [getenv "REMOTE_SMT", remote_name])
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   171
    else error ("Undefined Isabelle environment variable: " ^ quote env_var)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   172
  end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   173
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   174
fun make_cmd solver args problem_path proof_path = space_implode " " (
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   175
  map File.shell_quote (solver @ args) @
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   176
  [File.shell_path problem_path, "2>&1", ">", File.shell_path proof_path])
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   177
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   178
fun run ctxt cmd args input =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   179
  (case Certificates.get (Context.Proof ctxt) of
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   180
    NONE => Cache_IO.run (make_cmd (choose cmd) args) input
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   181
  | SOME certs =>
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   182
      (case Cache_IO.lookup certs input of
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   183
        (NONE, key) =>
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   184
          if Config.get ctxt fixed_certificates
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   185
          then error ("Bad certificates cache: missing certificate")
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   186
          else Cache_IO.run_and_cache certs key (make_cmd (choose cmd) args)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   187
            input
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   188
      | (SOME output, _) =>
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   189
         (tracing ("Using cached certificate from " ^
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   190
            File.shell_path (Cache_IO.cache_path_of certs) ^ " ...");
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   191
          output)))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   192
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   193
in
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   194
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   195
fun run_solver ctxt cmd args input =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   196
  let
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   197
    fun pretty tag ls = Pretty.string_of (Pretty.big_list tag
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   198
      (map Pretty.str ls))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   199
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   200
    val _ = trace_msg ctxt (pretty "SMT problem:" o split_lines) input
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   201
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   202
    val (res, err) = with_timeout ctxt (run ctxt cmd args) input
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   203
    val _ = trace_msg ctxt (pretty "SMT solver:") err
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   204
39811
0659e84bdc5f chop_while replace drop_while and take_while
haftmann
parents: 39809
diff changeset
   205
    val ls = rev (snd (chop_while (equal "") (rev res)))
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   206
    val _ = trace_msg ctxt (pretty "SMT result:") ls
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   207
  in ls end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   208
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   209
end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   210
36940
b4417ddad979 make SML/NJ happy
blanchet
parents: 36899
diff changeset
   211
fun trace_recon_data ctxt ({typs, terms, ...} : SMT_Translate.recon) =
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   212
  let
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   213
    fun pretty_eq n p = Pretty.block [Pretty.str n, Pretty.str " = ", p]
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   214
    fun pretty_typ (n, T) = pretty_eq n (Syntax.pretty_typ ctxt T)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   215
    fun pretty_term (n, t) = pretty_eq n (Syntax.pretty_term ctxt t)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   216
  in
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   217
    trace_msg ctxt (fn () => Pretty.string_of (Pretty.big_list "SMT names:" [
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   218
      Pretty.big_list "sorts:" (map pretty_typ (Symtab.dest typs)),
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   219
      Pretty.big_list "functions:" (map pretty_term (Symtab.dest terms))])) ()
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   220
  end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   221
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
   222
fun invoke translate_config name cmd more_opts options irules 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
   223
  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
   224
    val args = more_opts @ options 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
   225
    val comments = ("solver: " ^ name) ::
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
      ("timeout: " ^ string_of_int (Config.get ctxt timeout)) ::
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
      "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
   228
  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
   229
    irules
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
    |> 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
   231
    ||> 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
   232
    |>> 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
   233
    |> 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
   234
  end
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   235
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   236
fun discharge_definitions thm =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   237
  if Thm.nprems_of thm = 0 then thm
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   238
  else discharge_definitions (@{thm reflexive} RS thm)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   239
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
   240
fun set_has_datatypes with_datatypes translate =
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   241
  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
   242
    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
   243
    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
   244
    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
   245
    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
   246
      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
   247
    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
   248
      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
   249
  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
   250
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
   251
fun gen_solver name info ctxt irules =
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
   252
  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
   253
    val {env_var, is_remote, options, more_options, interface, reconstruct} =
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
      info
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   255
    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
   256
    val (with_datatypes, 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
   257
      set_has_datatypes (Config.get ctxt datatypes) translate
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   258
  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
   259
    (irules, 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
   260
    |-> SMT_Normalize.normalize extra_norm 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
   261
    |-> invoke translate' name (env_var, is_remote, name) more_options options
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   262
    |-> 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
   263
    |-> (fn (idxs, thm) => fn ctxt' => thm
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   264
    |> 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
   265
    |> discharge_definitions
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
   266
    |> pair idxs)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   267
  end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   268
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   269
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   270
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   271
(* solver store *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   272
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
   273
type solver = 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
   274
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
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
   276
  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
   277
  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
   278
  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
   279
  more_options: 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
   280
  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
   281
  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
   282
    (int list * thm) * Proof.context }
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   283
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   284
structure Solvers = Generic_Data
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   285
(
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
   286
  type T = solver_info Symtab.table
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   287
  val empty = Symtab.empty
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   288
  val extend = I
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   289
  fun merge data = Symtab.merge (K true) data
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   290
    handle Symtab.DUP name => error ("Duplicate SMT solver: " ^ quote name)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   291
)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   292
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   293
val no_solver = "(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
   294
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
   295
fun set_solver_options name opts = Solvers.map (Symtab.map_entry name (fn
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
   296
  {env_var, is_remote, options, interface, reconstruct, ...} =>
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
   297
  {env_var=env_var, is_remote=is_remote, options=options,
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
   298
   more_options=String.tokens (Symbol.is_ascii_blank o str) opts,
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
   299
   interface=interface, reconstruct=reconstruct}))
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
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
   301
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
   302
  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
   303
    (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
   304
      (Unsat, 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
   305
        if not (Config.get ctxt oracle) andalso is_some reconstruct
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
   306
        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
   307
        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
   308
    | (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
   309
        let val ts = (case cex_parser of SOME f => f 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
   310
        in raise SMT (Counterexample (result = Sat, ts)) 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
   311
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
   312
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
   313
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
   314
  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
   315
    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
   316
      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
   317
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
   318
    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
   319
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
   320
    fun solver ocl = { env_var=env_var, is_remote=is_remote, options=options,
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
      more_options=[], 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
   322
      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
   323
  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
   324
    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
   325
    Context.theory_map (Solvers.map (Symtab.update_new (name, solver 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
   326
    Attrib.setup (Binding.name (name ^ "_options"))
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
   327
      (Scan.lift (Parse.$$$ "=" |-- Args.name) >>
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
   328
        (Thm.declaration_attribute o K o set_solver_options name))
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
   329
      ("Additional command line options for SMT solver " ^ quote name)
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
   330
  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
   331
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
   332
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
   333
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   334
val all_solver_names_of = Symtab.keys o Solvers.get
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   335
val lookup_solver = Symtab.lookup o Solvers.get
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   336
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   337
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   338
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   339
(* selected solver *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   340
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   341
structure Selected_Solver = Generic_Data
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   342
(
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   343
  type T = string
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   344
  val empty = no_solver
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   345
  val extend = I
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   346
  fun merge (s, _) = s
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   347
)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   348
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   349
val solver_name_of = Selected_Solver.get
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   350
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   351
fun select_solver name context =
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   352
  if is_none (lookup_solver context name)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   353
  then error ("SMT solver not registered: " ^ quote name)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   354
  else Selected_Solver.map (K name) context
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   355
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   356
fun raw_solver_of context name =
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   357
  (case lookup_solver context name of
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   358
    NONE => error "No SMT solver selected"
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
   359
  | SOME s => s)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   360
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   361
fun solver_of context =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   362
  let val name = solver_name_of context
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   363
  in gen_solver name (raw_solver_of context name) end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   364
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   365
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   366
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
   367
(* SMT 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
   368
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
   369
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
   370
    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
   371
  | 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
   372
  | _ => 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
   373
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
   374
fun smt_solver 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
   375
  (* without this test, we would run into problems when atomizing the rules: *)
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
   376
  if exists (has_topsort o Thm.prop_of o snd) irules
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
   377
  then raise SMT (Other_Failure "proof state contains the universal sort {}")
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
   378
  else solver_of (Context.Proof ctxt) ctxt irules
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
   379
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
   380
fun smt_filter st i xrules =
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
   381
  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
   382
    val {context, facts, goal} = Proof.goal st
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
   383
    val cprop =
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
   384
      Thm.cprem_of goal i
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
   385
      |> Thm.rhs_of o SMT_Normalize.atomize_conv 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
   386
      |> Thm.capply @{cterm Trueprop} o Thm.capply @{cterm Not} o Thm.dest_arg
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
   387
    val irs = map (pair ~1) (Thm.assume cprop :: facts)
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
   388
  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
   389
    split_list xrules
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
   390
    ||>> solver_of (Context.Proof context) context o append irs o map_index I
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
   391
    |>> uncurry (map_filter o try o nth) o apsnd (distinct (op =))
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
   392
    |> rpair NONE o fst
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
   393
  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
   394
  handle SMT fail => ([], SOME fail)
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
   395
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
   396
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
   397
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   398
(* SMT tactic *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   399
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   400
local
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   401
  fun fail_tac f msg st = (f msg; Tactical.no_tac st)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   402
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   403
  fun SAFE pass_exns tac ctxt i st =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   404
    if pass_exns then tac ctxt i st
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
   405
    else (tac ctxt i st handle SMT fail => fail_tac
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
   406
      (trace_msg ctxt (prefix "SMT: ") o string_of_failure ctxt) fail st)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   407
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
   408
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   409
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
   410
  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
   411
  THEN' Tactic.rtac @{thm ccontr}
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   412
  THEN' SUBPROOF (fn {context, prems, ...} =>
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
   413
    let fun solve cx = snd (smt_solver cx (map (pair ~1) (rules @ prems)))
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
   414
    in SAFE pass_exns (Tactic.rtac o solve) context 1 end) ctxt
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   415
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   416
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
   417
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   418
end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   419
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   420
val smt_method =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   421
  Scan.optional Attrib.thms [] >>
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   422
  (fn thms => fn ctxt => METHOD (fn facts =>
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   423
    HEADGOAL (smt_tac ctxt (thms @ facts))))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   424
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   425
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   426
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   427
(* setup *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   428
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   429
val setup =
38808
89ae86205739 more antiquotations;
wenzelm
parents: 36960
diff changeset
   430
  Attrib.setup @{binding smt_solver}
36960
01594f816e3a prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents: 36940
diff changeset
   431
    (Scan.lift (Parse.$$$ "=" |-- Args.name) >>
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   432
      (Thm.declaration_attribute o K o select_solver))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   433
    "SMT solver configuration" #>
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
   434
  setup_oracle #>
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
   435
  setup_datatypes #>
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   436
  setup_timeout #>
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   437
  setup_trace #>
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
   438
  setup_trace_used_facts #>
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   439
  setup_fixed_certificates #>
38808
89ae86205739 more antiquotations;
wenzelm
parents: 36960
diff changeset
   440
  Attrib.setup @{binding smt_certificates}
36960
01594f816e3a prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents: 36940
diff changeset
   441
    (Scan.lift (Parse.$$$ "=" |-- Args.name) >>
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   442
      (Thm.declaration_attribute o K o select_certificates))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   443
    "SMT certificates" #>
38808
89ae86205739 more antiquotations;
wenzelm
parents: 36960
diff changeset
   444
  Method.setup @{binding smt} smt_method
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   445
    "Applies an SMT solver to the current goal."
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   446
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   447
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   448
fun print_setup context =
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   449
  let
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   450
    val t = string_of_int (Config.get_generic context timeout)
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   451
    val names = sort_strings (all_solver_names_of context)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   452
    val ns = if null names then [no_solver] else names
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
   453
    val n = solver_name_of 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
   454
    val opts =
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
   455
      (case Symtab.lookup (Solvers.get context) n 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
   456
        NONE => []
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
   457
      | SOME {more_options, options, ...} =>
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
   458
          more_options @ options (Context.proof_of context))
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   459
    val certs_filename =
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   460
      (case get_certificates_path context of
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   461
        SOME path => Path.implode path
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   462
      | NONE => "(disabled)")
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   463
    val fixed = if Config.get_generic context fixed_certificates then "true"
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   464
      else "false"
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   465
  in
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   466
    Pretty.writeln (Pretty.big_list "SMT setup:" [
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
   467
      Pretty.str ("Current SMT solver: " ^ n),
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
   468
      Pretty.str ("Current SMT solver options: " ^ space_implode " " opts),
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   469
      Pretty.str_list "Available SMT solvers: "  "" ns,
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   470
      Pretty.str ("Current timeout: " ^ t ^ " seconds"),
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
   471
      Pretty.str ("With proofs: " ^
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
   472
        (if Config.get_generic context oracle then "false" else "true")),
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   473
      Pretty.str ("Certificates cache: " ^ certs_filename),
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
   474
      Pretty.str ("Fixed certificates: " ^ fixed)])
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   475
  end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   476
36960
01594f816e3a prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents: 36940
diff changeset
   477
val _ =
01594f816e3a prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents: 36940
diff changeset
   478
  Outer_Syntax.improper_command "smt_status"
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
   479
    "show the available SMT solvers and the currently selected solver"
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
   480
    Keyword.diag
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   481
    (Scan.succeed (Toplevel.no_timing o Toplevel.keep (fn state =>
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   482
      print_setup (Context.Proof (Toplevel.context_of state)))))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   483
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   484
end