src/HOL/Library/Old_SMT/old_smt_solver.ML
author wenzelm
Fri, 06 Mar 2015 23:52:35 +0100
changeset 59634 4b94cc030ba0
parent 59621 291934bac95e
child 60695 757549b4bbe6
permissions -rw-r--r--
clarified context;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
     1
(*  Title:      HOL/Library/Old_SMT/old_smt_solver.ML
36898
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
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
     7
signature OLD_SMT_SOLVER =
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
     8
sig
40424
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents: 40357
diff changeset
     9
  (*configuration*)
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
    10
  datatype outcome = Unsat | Sat | Unknown
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    11
  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
    12
    name: string,
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
    13
    class: Proof.context -> Old_SMT_Utils.class,
41432
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
    14
    avail: unit -> bool,
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
    15
    command: unit -> string list,
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
    16
    options: Proof.context -> string list,
41432
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
    17
    default_max_relevant: int,
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
    18
    supports_filter: bool,
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
    outcome: string -> string list -> outcome * string list,
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
    20
    cex_parser: (Proof.context -> Old_SMT_Translate.recon -> string list ->
40828
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40666
diff changeset
    21
      term list * term list) option,
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
    22
    reconstruct: (Proof.context -> Old_SMT_Translate.recon -> string list ->
41432
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
    23
      int list * thm) option }
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    24
40424
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents: 40357
diff changeset
    25
  (*registry*)
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
  val add_solver: solver_config -> theory -> theory
40940
ff805bb109d8 export more information about available SMT solvers
blanchet
parents: 40828
diff changeset
    27
  val solver_name_of: Proof.context -> string
ff805bb109d8 export more information about available SMT solvers
blanchet
parents: 40828
diff changeset
    28
  val available_solvers_of: Proof.context -> string list
41432
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
    29
  val apply_solver: Proof.context -> (int * (int option * thm)) list ->
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
    30
    int list * thm
40981
67f436af0638 have SMT solvers report the number of facts that they should have by default in Sledgehammer -- the information might not seem to belong there but it also belongs nowhere else, for how is Sledgehammer to know how different solvers deal with hundreds of facts?
blanchet
parents: 40980
diff changeset
    31
  val default_max_relevant: Proof.context -> string -> int
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    32
40162
7f58a9a843c2 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents: 40161
diff changeset
    33
  (*filter*)
41432
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
    34
  type 'a smt_filter_data =
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
    35
    ('a * thm) list * ((int * thm) list * Proof.context)
50486
d5dc28fafd9d made MaSh evaluation driver work with SMT solvers
blanchet
parents: 48902
diff changeset
    36
  val smt_filter_preprocess: Proof.context -> thm list -> thm ->
41432
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
    37
    ('a * (int option * thm)) list -> int -> 'a smt_filter_data
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
    38
  val smt_filter_apply: Time.time -> 'a smt_filter_data ->
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
    39
    {outcome: Old_SMT_Failure.failure option, used_facts: ('a * thm) list}
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
    40
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    41
  (*tactic*)
46464
4cf5a84e2c05 normalized aliases;
wenzelm
parents: 42616
diff changeset
    42
  val smt_tac: Proof.context -> thm list -> int -> tactic
4cf5a84e2c05 normalized aliases;
wenzelm
parents: 42616
diff changeset
    43
  val smt_tac': Proof.context -> thm list -> int -> tactic
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    44
end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    45
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
    46
structure Old_SMT_Solver: OLD_SMT_SOLVER =
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    47
struct
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    48
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
    49
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    50
(* interface to external solvers *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    51
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    52
local
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    53
41432
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
    54
fun make_cmd command options problem_path proof_path = space_implode " " (
48532
c0f44941e674 Sledgehammer already has its own ways of reporting and recovering from crashes in external provers -- no need to additionally print scores of warnings (cf. 4b0daca2bf88)
blanchet
parents: 48043
diff changeset
    55
  "(exec 2>&1;" :: map File.shell_quote (command () @ options) @
c0f44941e674 Sledgehammer already has its own ways of reporting and recovering from crashes in external provers -- no need to additionally print scores of warnings (cf. 4b0daca2bf88)
blanchet
parents: 48043
diff changeset
    56
  [File.shell_path problem_path, ")", ">", File.shell_path proof_path])
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    57
41432
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
    58
fun trace_and ctxt msg f x =
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
    59
  let val _ = Old_SMT_Config.trace_msg ctxt (fn () => msg) ()
41432
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
    60
  in f x end
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
    61
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
    62
fun run ctxt name mk_cmd input =
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
    63
  (case Old_SMT_Config.certificates_of ctxt of
40578
2b098a549450 keep input and output files used to communicate with the SMT solver (for debugging purposes mainly)
boehmes
parents: 40561
diff changeset
    64
    NONE =>
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
    65
      if not (Old_SMT_Config.is_available ctxt name) then
46743
8e365bc843e9 fine-tune intended failure of smt method when the chosen SMT solver is not installed: restrict failures to true invocations of the SMT solver and don't fail for runs based on certificates
boehmes
parents: 46736
diff changeset
    66
        error ("The SMT solver " ^ quote name ^ " is not installed.")
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
    67
      else if Config.get ctxt Old_SMT_Config.debug_files = "" then
41432
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
    68
        trace_and ctxt ("Invoking SMT solver " ^ quote name ^ " ...")
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
    69
          (Cache_IO.run mk_cmd) input
40578
2b098a549450 keep input and output files used to communicate with the SMT solver (for debugging purposes mainly)
boehmes
parents: 40561
diff changeset
    70
      else
2b098a549450 keep input and output files used to communicate with the SMT solver (for debugging purposes mainly)
boehmes
parents: 40561
diff changeset
    71
        let
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
    72
          val base_path = Path.explode (Config.get ctxt Old_SMT_Config.debug_files)
40578
2b098a549450 keep input and output files used to communicate with the SMT solver (for debugging purposes mainly)
boehmes
parents: 40561
diff changeset
    73
          val in_path = Path.ext "smt_in" base_path
2b098a549450 keep input and output files used to communicate with the SMT solver (for debugging purposes mainly)
boehmes
parents: 40561
diff changeset
    74
          val out_path = Path.ext "smt_out" base_path
41432
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
    75
        in Cache_IO.raw_run mk_cmd input in_path out_path end
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    76
  | SOME certs =>
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    77
      (case Cache_IO.lookup certs input of
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    78
        (NONE, key) =>
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
    79
          if Config.get ctxt Old_SMT_Config.read_only_certificates then
47152
446cfc760ccf renamed "smt_fixed" to "smt_read_only_certificates"
blanchet
parents: 46743
diff changeset
    80
            error ("Bad certificate cache: missing certificate")
40538
b8482ff0bc92 check the return code of the SMT solver and raise an exception if the prover failed
boehmes
parents: 40515
diff changeset
    81
          else
41432
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
    82
            Cache_IO.run_and_cache certs key mk_cmd input
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    83
      | (SOME output, _) =>
41432
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
    84
          trace_and ctxt ("Using cached certificate from " ^
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
    85
            File.shell_path (Cache_IO.cache_path_of certs) ^ " ...")
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
    86
            I output))
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    87
41432
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
    88
fun run_solver ctxt name mk_cmd input =
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    89
  let
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    90
    fun pretty tag ls = Pretty.string_of (Pretty.big_list tag
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    91
      (map Pretty.str ls))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    92
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
    93
    val _ = Old_SMT_Config.trace_msg ctxt (pretty "Problem:" o split_lines) input
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    94
40550
f84c664ece8e trace more solver output before raising an exception due to a non-zero return code (avoids truncating potential counterexamples produced by Z3)
boehmes
parents: 40538
diff changeset
    95
    val {redirected_output=res, output=err, return_code} =
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
    96
      Old_SMT_Config.with_timeout ctxt (run ctxt name mk_cmd) input
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
    97
    val _ = Old_SMT_Config.trace_msg ctxt (pretty "Solver:") err
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    98
48902
44a6967240b7 prefer classic take_prefix/take_suffix over chop_while (cf. 0659e84bdc5f);
wenzelm
parents: 48534
diff changeset
    99
    val ls = fst (take_suffix (equal "") res)
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   100
    val _ = Old_SMT_Config.trace_msg ctxt (pretty "Result:") ls
40550
f84c664ece8e trace more solver output before raising an exception due to a non-zero return code (avoids truncating potential counterexamples produced by Z3)
boehmes
parents: 40538
diff changeset
   101
48534
2307efbfc554 Z3 prints so many warnings that the very informative abnormal termination exception hardly ever gets raised -- better be more aggressive here
blanchet
parents: 48532
diff changeset
   102
    val _ = return_code <> 0 andalso
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   103
      raise Old_SMT_Failure.SMT (Old_SMT_Failure.Abnormal_Termination return_code)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   104
  in ls end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   105
41328
6792a5c92a58 avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents: 41300
diff changeset
   106
fun trace_assms ctxt =
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   107
  Old_SMT_Config.trace_msg ctxt (Pretty.string_of o
41328
6792a5c92a58 avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents: 41300
diff changeset
   108
    Pretty.big_list "Assertions:" o map (Display.pretty_thm ctxt o snd))
40198
8d470bbaafd7 trace assumptions before giving them to the SMT solver
boehmes
parents: 40197
diff changeset
   109
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   110
fun trace_recon_data ({context=ctxt, typs, terms, ...} : Old_SMT_Translate.recon) =
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   111
  let
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   112
    fun pretty_eq n p = Pretty.block [Pretty.str n, Pretty.str " = ", p]
40424
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents: 40357
diff changeset
   113
    fun p_typ (n, T) = pretty_eq n (Syntax.pretty_typ ctxt T)
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents: 40357
diff changeset
   114
    fun p_term (n, t) = pretty_eq n (Syntax.pretty_term ctxt t)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   115
  in
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   116
    Old_SMT_Config.trace_msg ctxt (fn () =>
40424
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents: 40357
diff changeset
   117
      Pretty.string_of (Pretty.big_list "Names:" [
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents: 40357
diff changeset
   118
        Pretty.big_list "sorts:" (map p_typ (Symtab.dest typs)),
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents: 40357
diff changeset
   119
        Pretty.big_list "functions:" (map p_term (Symtab.dest terms))])) ()
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   120
  end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   121
41432
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   122
in
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   123
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   124
fun invoke name command ithms ctxt =
40162
7f58a9a843c2 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents: 40161
diff changeset
   125
  let
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   126
    val options = Old_SMT_Config.solver_options_of ctxt
40162
7f58a9a843c2 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents: 40161
diff changeset
   127
    val comments = ("solver: " ^ name) ::
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   128
      ("timeout: " ^ string_of_real (Config.get ctxt Old_SMT_Config.timeout)) ::
41328
6792a5c92a58 avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents: 41300
diff changeset
   129
      ("random seed: " ^
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   130
        string_of_int (Config.get ctxt Old_SMT_Config.random_seed)) ::
41432
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   131
      "arguments:" :: options
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   132
41127
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41126
diff changeset
   133
    val (str, recon as {context=ctxt', ...}) =
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41126
diff changeset
   134
      ithms
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41126
diff changeset
   135
      |> tap (trace_assms ctxt)
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   136
      |> Old_SMT_Translate.translate ctxt comments
41127
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41126
diff changeset
   137
      ||> tap trace_recon_data
41601
fda8511006f9 made Z3 the default SMT solver again
boehmes
parents: 41497
diff changeset
   138
  in (run_solver ctxt' name (make_cmd command options) str, recon) end
41432
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   139
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   140
end
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   141
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   142
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   143
(* configuration *)
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   144
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   145
datatype outcome = Unsat | Sat | Unknown
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
   146
41432
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   147
type solver_config = {
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   148
  name: string,
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   149
  class: Proof.context -> Old_SMT_Utils.class,
41432
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   150
  avail: unit -> bool,
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   151
  command: unit -> string list,
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   152
  options: Proof.context -> string list,
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   153
  default_max_relevant: int,
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   154
  supports_filter: bool,
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   155
  outcome: string -> string list -> outcome * string list,
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   156
  cex_parser: (Proof.context -> Old_SMT_Translate.recon -> string list ->
41432
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   157
    term list * term list) option,
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   158
  reconstruct: (Proof.context -> Old_SMT_Translate.recon -> string list ->
41432
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   159
    int list * thm) option }
41041
ec2734f34d0f make SML/NJ happy
blanchet
parents: 40981
diff changeset
   160
ec2734f34d0f make SML/NJ happy
blanchet
parents: 40981
diff changeset
   161
ec2734f34d0f make SML/NJ happy
blanchet
parents: 40981
diff changeset
   162
(* registry *)
ec2734f34d0f make SML/NJ happy
blanchet
parents: 40981
diff changeset
   163
ec2734f34d0f make SML/NJ happy
blanchet
parents: 40981
diff changeset
   164
type solver_info = {
41432
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   165
  command: unit -> string list,
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   166
  default_max_relevant: int,
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   167
  supports_filter: bool,
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   168
  reconstruct: Proof.context -> string list * Old_SMT_Translate.recon ->
41432
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   169
    int list * thm }
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   170
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   171
structure Solvers = Generic_Data
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   172
(
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
   173
  type T = solver_info Symtab.table
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   174
  val empty = Symtab.empty
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   175
  val extend = I
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   176
  fun merge data = Symtab.merge (K true) data
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   177
)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   178
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
   179
local
41127
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41126
diff changeset
   180
  fun finish outcome cex_parser reconstruct ocl outer_ctxt
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   181
      (output, (recon as {context=ctxt, ...} : Old_SMT_Translate.recon)) =
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
   182
    (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
   183
      (Unsat, ls) =>
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   184
        if not (Config.get ctxt Old_SMT_Config.oracle) andalso is_some reconstruct
41127
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41126
diff changeset
   185
        then the reconstruct outer_ctxt recon ls
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41126
diff changeset
   186
        else ([], ocl ())
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
   187
    | (result, ls) =>
40828
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40666
diff changeset
   188
        let
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40666
diff changeset
   189
          val (ts, us) =
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40666
diff changeset
   190
            (case cex_parser of SOME f => f ctxt recon ls | _ => ([], []))
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40666
diff changeset
   191
         in
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   192
          raise Old_SMT_Failure.SMT (Old_SMT_Failure.Counterexample {
40828
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40666
diff changeset
   193
            is_real_cex = (result = Sat),
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40666
diff changeset
   194
            free_constraints = ts,
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40666
diff changeset
   195
            const_defs = us})
40424
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents: 40357
diff changeset
   196
        end)
40579
98ebd2300823 use the const antiquotation for constants (this checks that the constant is declared, whereas the more general term antiquotation treats undeclared names as free variable)
boehmes
parents: 40578
diff changeset
   197
59634
4b94cc030ba0 clarified context;
wenzelm
parents: 59621
diff changeset
   198
  val cfalse = Thm.cterm_of @{context} (@{const Trueprop} $ @{const False})
40162
7f58a9a843c2 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents: 40161
diff changeset
   199
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
   200
7f58a9a843c2 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents: 40161
diff changeset
   201
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
   202
  let
41432
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   203
    val {name, class, avail, command, options, default_max_relevant,
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   204
      supports_filter, outcome, cex_parser, reconstruct} = cfg
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
   205
40579
98ebd2300823 use the const antiquotation for constants (this checks that the constant is declared, whereas the more general term antiquotation treats undeclared names as free variable)
boehmes
parents: 40578
diff changeset
   206
    fun core_oracle () = cfalse
40162
7f58a9a843c2 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents: 40161
diff changeset
   207
41432
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   208
    fun solver ocl = {
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   209
      command = command,
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   210
      default_max_relevant = default_max_relevant,
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   211
      supports_filter = supports_filter,
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   212
      reconstruct = finish (outcome name) cex_parser reconstruct ocl }
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   213
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   214
    val info = {name=name, class=class, avail=avail, options=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
   215
  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
   216
    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
   217
    Context.theory_map (Solvers.map (Symtab.update_new (name, solver ocl)))) #>
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   218
    Context.theory_map (Old_SMT_Config.add_solver info)
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
   219
  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
   220
7f58a9a843c2 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents: 40161
diff changeset
   221
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
   222
40981
67f436af0638 have SMT solvers report the number of facts that they should have by default in Sledgehammer -- the information might not seem to belong there but it also belongs nowhere else, for how is Sledgehammer to know how different solvers deal with hundreds of facts?
blanchet
parents: 40980
diff changeset
   223
fun get_info ctxt name =
67f436af0638 have SMT solvers report the number of facts that they should have by default in Sledgehammer -- the information might not seem to belong there but it also belongs nowhere else, for how is Sledgehammer to know how different solvers deal with hundreds of facts?
blanchet
parents: 40980
diff changeset
   224
  the (Symtab.lookup (Solvers.get (Context.Proof ctxt)) name)
67f436af0638 have SMT solvers report the number of facts that they should have by default in Sledgehammer -- the information might not seem to belong there but it also belongs nowhere else, for how is Sledgehammer to know how different solvers deal with hundreds of facts?
blanchet
parents: 40980
diff changeset
   225
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   226
val solver_name_of = Old_SMT_Config.solver_of
41432
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   227
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   228
val available_solvers_of = Old_SMT_Config.available_solvers_of
41432
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   229
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   230
fun name_and_info_of ctxt =
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   231
  let val name = solver_name_of ctxt
40981
67f436af0638 have SMT solvers report the number of facts that they should have by default in Sledgehammer -- the information might not seem to belong there but it also belongs nowhere else, for how is Sledgehammer to know how different solvers deal with hundreds of facts?
blanchet
parents: 40980
diff changeset
   232
  in (name, get_info ctxt name) end
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   233
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   234
fun gen_preprocess ctxt iwthms = Old_SMT_Normalize.normalize iwthms ctxt
40940
ff805bb109d8 export more information about available SMT solvers
blanchet
parents: 40828
diff changeset
   235
41432
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   236
fun gen_apply (ithms, ctxt) =
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   237
  let val (name, {command, reconstruct, ...}) = name_and_info_of ctxt
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   238
  in
46743
8e365bc843e9 fine-tune intended failure of smt method when the chosen SMT solver is not installed: restrict failures to true invocations of the SMT solver and don't fail for runs based on certificates
boehmes
parents: 46736
diff changeset
   239
    (ithms, ctxt)
8e365bc843e9 fine-tune intended failure of smt method when the chosen SMT solver is not installed: restrict failures to true invocations of the SMT solver and don't fail for runs based on certificates
boehmes
parents: 46736
diff changeset
   240
    |-> invoke name command
8e365bc843e9 fine-tune intended failure of smt method when the chosen SMT solver is not installed: restrict failures to true invocations of the SMT solver and don't fail for runs based on certificates
boehmes
parents: 46736
diff changeset
   241
    |> reconstruct ctxt
8e365bc843e9 fine-tune intended failure of smt method when the chosen SMT solver is not installed: restrict failures to true invocations of the SMT solver and don't fail for runs based on certificates
boehmes
parents: 46736
diff changeset
   242
    |>> distinct (op =)
41432
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   243
  end
40166
d3bc972b7d9d optionally force the remote version of an SMT solver to be executed
boehmes
parents: 40165
diff changeset
   244
41432
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   245
fun apply_solver ctxt = gen_apply o gen_preprocess ctxt
40981
67f436af0638 have SMT solvers report the number of facts that they should have by default in Sledgehammer -- the information might not seem to belong there but it also belongs nowhere else, for how is Sledgehammer to know how different solvers deal with hundreds of facts?
blanchet
parents: 40980
diff changeset
   246
67f436af0638 have SMT solvers report the number of facts that they should have by default in Sledgehammer -- the information might not seem to belong there but it also belongs nowhere else, for how is Sledgehammer to know how different solvers deal with hundreds of facts?
blanchet
parents: 40980
diff changeset
   247
val default_max_relevant = #default_max_relevant oo get_info
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   248
41432
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   249
val supports_filter = #supports_filter o snd o name_and_info_of 
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   250
41432
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   251
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   252
(* check well-sortedness *)
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
   253
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
   254
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
   255
    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
   256
  | 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
   257
  | _ => 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
   258
41239
d6e804ff29c3 split "smt_filter" into head and tail
blanchet
parents: 41131
diff changeset
   259
(* without this test, we would run into problems when atomizing the rules: *)
54041
227908156cd2 make SMT integration slacker w.r.t. bad apples (facts)
blanchet
parents: 52732
diff changeset
   260
fun check_topsort ctxt thm =
227908156cd2 make SMT integration slacker w.r.t. bad apples (facts)
blanchet
parents: 52732
diff changeset
   261
  if has_topsort (Thm.prop_of thm) then
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   262
    (Old_SMT_Normalize.drop_fact_warning ctxt thm; TrueI)
54041
227908156cd2 make SMT integration slacker w.r.t. bad apples (facts)
blanchet
parents: 52732
diff changeset
   263
  else
227908156cd2 make SMT integration slacker w.r.t. bad apples (facts)
blanchet
parents: 52732
diff changeset
   264
    thm
227908156cd2 make SMT integration slacker w.r.t. bad apples (facts)
blanchet
parents: 52732
diff changeset
   265
227908156cd2 make SMT integration slacker w.r.t. bad apples (facts)
blanchet
parents: 52732
diff changeset
   266
fun check_topsorts ctxt iwthms = map (apsnd (apsnd (check_topsort ctxt))) iwthms
41432
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   267
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   268
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   269
(* filter *)
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
   270
59634
4b94cc030ba0 clarified context;
wenzelm
parents: 59621
diff changeset
   271
val cnot = Thm.cterm_of @{context} @{const Not}
40579
98ebd2300823 use the const antiquotation for constants (this checks that the constant is declared, whereas the more general term antiquotation treats undeclared names as free variable)
boehmes
parents: 40578
diff changeset
   272
41239
d6e804ff29c3 split "smt_filter" into head and tail
blanchet
parents: 41131
diff changeset
   273
fun mk_result outcome xrules = { outcome = outcome, used_facts = xrules }
41126
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41124
diff changeset
   274
41432
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   275
type 'a smt_filter_data = ('a * thm) list * ((int * thm) list * Proof.context)
41239
d6e804ff29c3 split "smt_filter" into head and tail
blanchet
parents: 41131
diff changeset
   276
50486
d5dc28fafd9d made MaSh evaluation driver work with SMT solvers
blanchet
parents: 48902
diff changeset
   277
fun smt_filter_preprocess ctxt facts goal xwthms i =
40162
7f58a9a843c2 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents: 40161
diff changeset
   278
  let
40164
57f5db2a48a3 added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents: 40162
diff changeset
   279
    val ctxt =
50486
d5dc28fafd9d made MaSh evaluation driver work with SMT solvers
blanchet
parents: 48902
diff changeset
   280
      ctxt
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   281
      |> Config.put Old_SMT_Config.oracle false
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   282
      |> Config.put Old_SMT_Config.filter_only_facts true
41126
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41124
diff changeset
   283
40357
82ebdd19c4a4 simulate more closely the behaviour of the tactic
boehmes
parents: 40332
diff changeset
   284
    val ({context=ctxt', prems, concl, ...}, _) = Subgoal.focus ctxt i goal
46497
89ccf66aa73d renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
wenzelm
parents: 46464
diff changeset
   285
    fun negate ct = Thm.dest_comb ct ||> Thm.apply cnot |-> Thm.apply
42320
1f09e4c680fc check if negating the goal is possible (avoids CTERM exception for Pure propositions)
boehmes
parents: 41761
diff changeset
   286
    val cprop =
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   287
      (case try negate (Thm.rhs_of (Old_SMT_Normalize.atomize_conv ctxt' concl)) of
42320
1f09e4c680fc check if negating the goal is possible (avoids CTERM exception for Pure propositions)
boehmes
parents: 41761
diff changeset
   288
        SOME ct => ct
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   289
      | NONE => raise Old_SMT_Failure.SMT (Old_SMT_Failure.Other_Failure (
42320
1f09e4c680fc check if negating the goal is possible (avoids CTERM exception for Pure propositions)
boehmes
parents: 41761
diff changeset
   290
          "goal is not a HOL term")))
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
   291
  in
41432
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   292
    map snd xwthms
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   293
    |> map_index I
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   294
    |> append (map (pair ~1 o pair NONE) (Thm.assume cprop :: prems @ facts))
54041
227908156cd2 make SMT integration slacker w.r.t. bad apples (facts)
blanchet
parents: 52732
diff changeset
   295
    |> check_topsorts ctxt'
41432
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   296
    |> gen_preprocess ctxt'
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   297
    |> pair (map (apsnd snd) xwthms)
41239
d6e804ff29c3 split "smt_filter" into head and tail
blanchet
parents: 41131
diff changeset
   298
  end
d6e804ff29c3 split "smt_filter" into head and tail
blanchet
parents: 41131
diff changeset
   299
41432
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   300
fun smt_filter_apply time_limit (xthms, (ithms, ctxt)) =
41241
7d07736aaaf6 make timeout part of the SMT filter's tail
blanchet
parents: 41239
diff changeset
   301
  let
41432
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   302
    val ctxt' =
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   303
      ctxt
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   304
      |> Config.put Old_SMT_Config.timeout (Time.toReal time_limit)
41432
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   305
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   306
    fun filter_thms false = K xthms
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   307
      | filter_thms true = map_filter (try (nth xthms)) o fst
41241
7d07736aaaf6 make timeout part of the SMT filter's tail
blanchet
parents: 41239
diff changeset
   308
  in
41432
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   309
    (ithms, ctxt')
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   310
    |> gen_apply
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   311
    |> filter_thms (supports_filter ctxt')
41126
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41124
diff changeset
   312
    |> mk_result 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
   313
  end
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   314
  handle Old_SMT_Failure.SMT fail => mk_result (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
   315
539d07b00e5f keep track of theorems initially given to SMT (even if they are rewritten); provide interface to filter theorems necessary for SMT proofs
boehmes
parents: 39811
diff changeset
   316
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   317
(* SMT tactic *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   318
41432
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   319
local
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   320
  fun trace_assumptions ctxt iwthms idxs =
40165
boehmes
parents: 40164
diff changeset
   321
    let
41432
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   322
      val wthms =
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   323
        idxs
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   324
        |> filter (fn i => i >= 0)
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   325
        |> map_filter (AList.lookup (op =) iwthms)
40165
boehmes
parents: 40164
diff changeset
   326
    in
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   327
      if Config.get ctxt Old_SMT_Config.trace_used_facts andalso length wthms > 0
41432
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   328
      then
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   329
        tracing (Pretty.string_of (Pretty.big_list "SMT used facts:"
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   330
          (map (Display.pretty_thm ctxt o snd) wthms)))
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   331
      else ()
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   332
    end
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   333
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   334
  fun solve ctxt iwthms =
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   335
    iwthms
54041
227908156cd2 make SMT integration slacker w.r.t. bad apples (facts)
blanchet
parents: 52732
diff changeset
   336
    |> check_topsorts ctxt
41432
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   337
    |> apply_solver ctxt
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   338
    |>> trace_assumptions ctxt iwthms
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   339
    |> snd
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   340
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   341
  fun str_of ctxt fail =
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   342
    Old_SMT_Failure.string_of_failure ctxt fail
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   343
    |> prefix ("Solver " ^ Old_SMT_Config.solver_of ctxt ^ ": ")
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   344
41432
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   345
  fun safe_solve ctxt iwthms = SOME (solve ctxt iwthms)
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   346
    handle
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   347
      Old_SMT_Failure.SMT (fail as Old_SMT_Failure.Counterexample _) =>
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   348
        (Old_SMT_Config.verbose_msg ctxt (str_of ctxt) fail; NONE)
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   349
    | Old_SMT_Failure.SMT (fail as Old_SMT_Failure.Time_Out) =>
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   350
        error ("SMT: Solver " ^ quote (Old_SMT_Config.solver_of ctxt) ^ ": " ^
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   351
          Old_SMT_Failure.string_of_failure ctxt fail ^ " (setting the " ^
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   352
          "configuration option " ^ quote (Config.name_of Old_SMT_Config.timeout) ^ " might help)")
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   353
    | Old_SMT_Failure.SMT fail => error (str_of ctxt fail)
41432
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   354
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   355
  fun tag_rules thms = map_index (apsnd (pair NONE)) thms
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   356
  fun tag_prems thms = map (pair ~1 o pair NONE) thms
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   357
52732
b4da1f2ec73f standardized aliases;
wenzelm
parents: 50486
diff changeset
   358
  fun resolve (SOME thm) = rtac thm 1
46464
4cf5a84e2c05 normalized aliases;
wenzelm
parents: 42616
diff changeset
   359
    | resolve NONE = no_tac
41432
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   360
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   361
  fun tac prove ctxt rules =
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   362
    CONVERSION (Old_SMT_Normalize.atomize_conv ctxt)
52732
b4da1f2ec73f standardized aliases;
wenzelm
parents: 50486
diff changeset
   363
    THEN' rtac @{thm ccontr}
41432
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   364
    THEN' SUBPROOF (fn {context, prems, ...} =>
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   365
      resolve (prove context (tag_rules rules @ tag_prems prems))) ctxt
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   366
in
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   367
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   368
val smt_tac = tac safe_solve
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   369
val smt_tac' = tac (SOME oo solve)
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   370
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   371
end
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   372
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   373
end