src/HOL/Library/Old_SMT/old_smt_solver.ML
author wenzelm
Wed, 08 Mar 2017 10:50:59 +0100
changeset 65151 a7394aa4d21c
parent 64304 96bc94c87a81
permissions -rw-r--r--
tuned proofs;
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
62549
9498623b27f0 File.bash_string operations in ML as in Scala -- exclusively for GNU bash, not perl and not user output;
wenzelm
parents: 61268
diff changeset
    54
fun make_cmd command options problem_path proof_path =
9498623b27f0 File.bash_string operations in ML as in Scala -- exclusively for GNU bash, not perl and not user output;
wenzelm
parents: 61268
diff changeset
    55
  space_implode " "
64304
96bc94c87a81 clarified modules;
wenzelm
parents: 62549
diff changeset
    56
    ("(exec 2>&1;" :: map Bash.string (command () @ options) @
62549
9498623b27f0 File.bash_string operations in ML as in Scala -- exclusively for GNU bash, not perl and not user output;
wenzelm
parents: 61268
diff changeset
    57
      [File.bash_path problem_path, ")", ">", File.bash_path proof_path])
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    58
41432
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
    59
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
    60
  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
    61
  in f x end
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
    62
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
    63
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
    64
  (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
    65
    NONE =>
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
    66
      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
    67
        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
    68
      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
    69
        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
    70
          (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
    71
      else
2b098a549450 keep input and output files used to communicate with the SMT solver (for debugging purposes mainly)
boehmes
parents: 40561
diff changeset
    72
        let
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
    73
          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
    74
          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
    75
          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
    76
        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
    77
  | SOME certs =>
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    78
      (case Cache_IO.lookup certs input of
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    79
        (NONE, key) =>
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
    80
          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
    81
            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
    82
          else
41432
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
    83
            Cache_IO.run_and_cache certs key mk_cmd input
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    84
      | (SOME output, _) =>
41432
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
    85
          trace_and ctxt ("Using cached certificate from " ^
62549
9498623b27f0 File.bash_string operations in ML as in Scala -- exclusively for GNU bash, not perl and not user output;
wenzelm
parents: 61268
diff changeset
    86
            Path.print (Cache_IO.cache_path_of certs) ^ " ...")
41432
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
    87
            I output))
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    88
41432
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
    89
fun run_solver ctxt name mk_cmd input =
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    90
  let
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    91
    fun pretty tag ls = Pretty.string_of (Pretty.big_list tag
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    92
      (map Pretty.str ls))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    93
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
    94
    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
    95
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
    96
    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
    97
      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
    98
    val _ = Old_SMT_Config.trace_msg ctxt (pretty "Solver:") err
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    99
48902
44a6967240b7 prefer classic take_prefix/take_suffix over chop_while (cf. 0659e84bdc5f);
wenzelm
parents: 48534
diff changeset
   100
    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
   101
    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
   102
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
   103
    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
   104
      raise Old_SMT_Failure.SMT (Old_SMT_Failure.Abnormal_Termination return_code)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   105
  in ls end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   106
41328
6792a5c92a58 avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents: 41300
diff changeset
   107
fun trace_assms ctxt =
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   108
  Old_SMT_Config.trace_msg ctxt (Pretty.string_of o
61268
abe08fb15a12 moved remaining display.ML to more_thm.ML;
wenzelm
parents: 60752
diff changeset
   109
    Pretty.big_list "Assertions:" o map (Thm.pretty_thm ctxt o snd))
40198
8d470bbaafd7 trace assumptions before giving them to the SMT solver
boehmes
parents: 40197
diff changeset
   110
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   111
fun trace_recon_data ({context=ctxt, typs, terms, ...} : Old_SMT_Translate.recon) =
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   112
  let
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   113
    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
   114
    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
   115
    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
   116
  in
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   117
    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
   118
      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
   119
        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
   120
        Pretty.big_list "functions:" (map p_term (Symtab.dest terms))])) ()
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   121
  end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   122
41432
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   123
in
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   124
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   125
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
   126
  let
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   127
    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
   128
    val comments = ("solver: " ^ name) ::
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   129
      ("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
   130
      ("random seed: " ^
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   131
        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
   132
      "arguments:" :: options
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   133
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
   134
    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
   135
      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
   136
      |> tap (trace_assms ctxt)
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   137
      |> 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
   138
      ||> tap trace_recon_data
41601
fda8511006f9 made Z3 the default SMT solver again
boehmes
parents: 41497
diff changeset
   139
  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
   140
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   141
end
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
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   144
(* configuration *)
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   145
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   146
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
   147
41432
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   148
type solver_config = {
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   149
  name: string,
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   150
  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
   151
  avail: unit -> bool,
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   152
  command: unit -> string list,
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   153
  options: Proof.context -> string list,
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   154
  default_max_relevant: int,
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   155
  supports_filter: bool,
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   156
  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
   157
  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
   158
    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
   159
  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
   160
    int list * thm) option }
41041
ec2734f34d0f make SML/NJ happy
blanchet
parents: 40981
diff changeset
   161
ec2734f34d0f make SML/NJ happy
blanchet
parents: 40981
diff changeset
   162
ec2734f34d0f make SML/NJ happy
blanchet
parents: 40981
diff changeset
   163
(* registry *)
ec2734f34d0f make SML/NJ happy
blanchet
parents: 40981
diff changeset
   164
ec2734f34d0f make SML/NJ happy
blanchet
parents: 40981
diff changeset
   165
type solver_info = {
41432
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   166
  command: unit -> string list,
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   167
  default_max_relevant: int,
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   168
  supports_filter: bool,
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   169
  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
   170
    int list * thm }
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   171
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   172
structure Solvers = Generic_Data
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   173
(
40162
7f58a9a843c2 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents: 40161
diff changeset
   174
  type T = solver_info Symtab.table
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   175
  val empty = Symtab.empty
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   176
  val extend = I
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   177
  fun merge data = Symtab.merge (K true) data
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   178
)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   179
40162
7f58a9a843c2 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents: 40161
diff changeset
   180
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
   181
  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
   182
      (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
   183
    (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
   184
      (Unsat, ls) =>
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   185
        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
   186
        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
   187
        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
   188
    | (result, ls) =>
40828
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40666
diff changeset
   189
        let
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40666
diff changeset
   190
          val (ts, us) =
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40666
diff changeset
   191
            (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
   192
         in
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   193
          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
   194
            is_real_cex = (result = Sat),
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40666
diff changeset
   195
            free_constraints = ts,
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40666
diff changeset
   196
            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
   197
        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
   198
59634
4b94cc030ba0 clarified context;
wenzelm
parents: 59621
diff changeset
   199
  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
   200
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
   201
7f58a9a843c2 joined setup of SMT solvers in one place; turned Z3-specific 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
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
   203
  let
41432
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   204
    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
   205
      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
   206
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
   207
    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
   208
41432
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   209
    fun solver ocl = {
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   210
      command = command,
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   211
      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
   212
      supports_filter = supports_filter,
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   213
      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
   214
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   215
    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
   216
  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
   217
    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
   218
    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
   219
    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
   220
  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
   221
7f58a9a843c2 joined setup of SMT solvers in one place; turned Z3-specific 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
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
   223
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
   224
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
   225
  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
   226
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   227
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
   228
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   229
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
   230
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   231
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
   232
  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
   233
  in (name, get_info ctxt name) end
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   234
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   235
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
   236
41432
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   237
fun gen_apply (ithms, ctxt) =
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   238
  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
   239
  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
   240
    (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
   241
    |-> 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
   242
    |> 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
   243
    |>> distinct (op =)
41432
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   244
  end
40166
d3bc972b7d9d optionally force the remote version of an SMT solver to be executed
boehmes
parents: 40165
diff changeset
   245
41432
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   246
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
   247
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
   248
val default_max_relevant = #default_max_relevant oo get_info
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   249
41432
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   250
val supports_filter = #supports_filter o snd o name_and_info_of 
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   251
41432
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   252
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   253
(* 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
   254
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
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
   256
    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
   257
  | 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
   258
  | _ => 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
   259
41239
d6e804ff29c3 split "smt_filter" into head and tail
blanchet
parents: 41131
diff changeset
   260
(* 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
   261
fun check_topsort ctxt thm =
227908156cd2 make SMT integration slacker w.r.t. bad apples (facts)
blanchet
parents: 52732
diff changeset
   262
  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
   263
    (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
   264
  else
227908156cd2 make SMT integration slacker w.r.t. bad apples (facts)
blanchet
parents: 52732
diff changeset
   265
    thm
227908156cd2 make SMT integration slacker w.r.t. bad apples (facts)
blanchet
parents: 52732
diff changeset
   266
227908156cd2 make SMT integration slacker w.r.t. bad apples (facts)
blanchet
parents: 52732
diff changeset
   267
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
   268
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   269
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   270
(* 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
   271
59634
4b94cc030ba0 clarified context;
wenzelm
parents: 59621
diff changeset
   272
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
   273
41239
d6e804ff29c3 split "smt_filter" into head and tail
blanchet
parents: 41131
diff changeset
   274
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
   275
41432
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   276
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
   277
50486
d5dc28fafd9d made MaSh evaluation driver work with SMT solvers
blanchet
parents: 48902
diff changeset
   278
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
   279
  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
   280
    val ctxt =
50486
d5dc28fafd9d made MaSh evaluation driver work with SMT solvers
blanchet
parents: 48902
diff changeset
   281
      ctxt
58058
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.oracle false
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   283
      |> 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
   284
60695
757549b4bbe6 Variable.focus etc.: optional bindings provided by user;
wenzelm
parents: 59634
diff changeset
   285
    val ({context=ctxt', prems, concl, ...}, _) = Subgoal.focus ctxt i NONE 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
   286
    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
   287
    val cprop =
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   288
      (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
   289
        SOME ct => ct
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   290
      | 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
   291
          "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
   292
  in
41432
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   293
    map snd xwthms
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   294
    |> map_index I
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   295
    |> 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
   296
    |> check_topsorts ctxt'
41432
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   297
    |> gen_preprocess ctxt'
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   298
    |> pair (map (apsnd snd) xwthms)
41239
d6e804ff29c3 split "smt_filter" into head and tail
blanchet
parents: 41131
diff changeset
   299
  end
d6e804ff29c3 split "smt_filter" into head and tail
blanchet
parents: 41131
diff changeset
   300
41432
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   301
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
   302
  let
41432
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   303
    val ctxt' =
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   304
      ctxt
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   305
      |> 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
   306
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   307
    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
   308
      | 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
   309
  in
41432
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   310
    (ithms, ctxt')
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   311
    |> gen_apply
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   312
    |> 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
   313
    |> 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
   314
  end
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   315
  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
   316
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
   317
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   318
(* SMT tactic *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   319
41432
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   320
local
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   321
  fun trace_assumptions ctxt iwthms idxs =
40165
boehmes
parents: 40164
diff changeset
   322
    let
41432
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   323
      val wthms =
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   324
        idxs
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   325
        |> filter (fn i => i >= 0)
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   326
        |> map_filter (AList.lookup (op =) iwthms)
40165
boehmes
parents: 40164
diff changeset
   327
    in
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   328
      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
   329
      then
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   330
        tracing (Pretty.string_of (Pretty.big_list "SMT used facts:"
61268
abe08fb15a12 moved remaining display.ML to more_thm.ML;
wenzelm
parents: 60752
diff changeset
   331
          (map (Thm.pretty_thm ctxt o snd) wthms)))
41432
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   332
      else ()
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   333
    end
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   334
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   335
  fun solve ctxt iwthms =
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   336
    iwthms
54041
227908156cd2 make SMT integration slacker w.r.t. bad apples (facts)
blanchet
parents: 52732
diff changeset
   337
    |> check_topsorts ctxt
41432
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   338
    |> apply_solver ctxt
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   339
    |>> trace_assumptions ctxt iwthms
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   340
    |> snd
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   341
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   342
  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
   343
    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
   344
    |> prefix ("Solver " ^ Old_SMT_Config.solver_of ctxt ^ ": ")
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   345
41432
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   346
  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
   347
    handle
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   348
      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
   349
        (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
   350
    | 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
   351
        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
   352
          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
   353
          "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
   354
    | 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
   355
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   356
  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
   357
  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
   358
60752
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60695
diff changeset
   359
  fun resolve ctxt (SOME thm) = resolve_tac ctxt [thm] 1
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60695
diff changeset
   360
    | resolve _ NONE = no_tac
41432
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   361
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   362
  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
   363
    CONVERSION (Old_SMT_Normalize.atomize_conv ctxt)
60752
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60695
diff changeset
   364
    THEN' resolve_tac ctxt @{thms ccontr}
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60695
diff changeset
   365
    THEN' SUBPROOF (fn {context = ctxt', prems, ...} =>
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60695
diff changeset
   366
      resolve ctxt' (prove ctxt' (tag_rules rules @ tag_prems prems))) ctxt
41432
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   367
in
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   368
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   369
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
   370
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
   371
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   372
end
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41328
diff changeset
   373
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   374
end