src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML
author wenzelm
Sat Apr 02 23:29:05 2016 +0200 (2016-04-02 ago)
changeset 62826 eb94e570c1a4
parent 62735 23de054397e5
child 63692 1bc4bc2c9fd1
permissions -rw-r--r--
prefer infix operations;
blanchet@58061
     1
(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML
blanchet@56081
     2
    Author:     Fabian Immler, TU Muenchen
blanchet@56081
     3
    Author:     Makarius
blanchet@56081
     4
    Author:     Jasmin Blanchette, TU Muenchen
blanchet@56081
     5
blanchet@56081
     6
SMT solvers as Sledgehammer provers.
blanchet@56081
     7
*)
blanchet@56081
     8
blanchet@58061
     9
signature SLEDGEHAMMER_PROVER_SMT =
blanchet@56081
    10
sig
blanchet@56081
    11
  type stature = ATP_Problem_Generate.stature
blanchet@56081
    12
  type mode = Sledgehammer_Prover.mode
blanchet@56081
    13
  type prover = Sledgehammer_Prover.prover
blanchet@56081
    14
blanchet@58061
    15
  val smt_builtins : bool Config.T
blanchet@58061
    16
  val smt_triggers : bool Config.T
blanchet@58061
    17
  val smt_max_slices : int Config.T
blanchet@58061
    18
  val smt_slice_fact_frac : real Config.T
blanchet@58061
    19
  val smt_slice_time_frac : real Config.T
blanchet@58061
    20
  val smt_slice_min_secs : int Config.T
blanchet@56081
    21
blanchet@58061
    22
  val is_smt_prover : Proof.context -> string -> bool
blanchet@58061
    23
  val run_smt_solver : mode -> string -> prover
blanchet@56081
    24
end;
blanchet@56081
    25
blanchet@58061
    26
structure Sledgehammer_Prover_SMT : SLEDGEHAMMER_PROVER_SMT =
blanchet@56081
    27
struct
blanchet@56081
    28
blanchet@56081
    29
open ATP_Util
blanchet@56081
    30
open ATP_Proof
blanchet@56081
    31
open ATP_Systems
blanchet@56081
    32
open ATP_Problem_Generate
blanchet@56081
    33
open ATP_Proof_Reconstruct
blanchet@56081
    34
open Sledgehammer_Util
blanchet@56081
    35
open Sledgehammer_Proof_Methods
blanchet@56083
    36
open Sledgehammer_Isar
blanchet@56081
    37
open Sledgehammer_Prover
blanchet@56081
    38
blanchet@58061
    39
val smt_builtins = Attrib.setup_config_bool @{binding sledgehammer_smt_builtins} (K true)
blanchet@58061
    40
val smt_triggers = Attrib.setup_config_bool @{binding sledgehammer_smt_triggers} (K true)
blanchet@56081
    41
blanchet@58061
    42
val is_smt_prover = member (op =) o SMT_Config.available_solvers_of
blanchet@56081
    43
blanchet@58061
    44
(* "SMT_Failure.Abnormal_Termination" carries the solver's return code. Until these are sorted out
blanchet@56081
    45
   properly in the SMT module, we must interpret these here. *)
blanchet@56081
    46
val z3_failures =
blanchet@56081
    47
  [(101, OutOfResources),
blanchet@56081
    48
   (103, MalformedInput),
blanchet@56081
    49
   (110, MalformedInput),
blanchet@56081
    50
   (112, TimedOut)]
blanchet@56081
    51
val unix_failures =
blanchet@59019
    52
  [(134, Crashed),
blanchet@59019
    53
   (138, Crashed),
blanchet@56081
    54
   (139, Crashed)]
blanchet@58061
    55
val smt_failures = z3_failures @ unix_failures
blanchet@56081
    56
blanchet@58061
    57
fun failure_of_smt_failure (SMT_Failure.Counterexample genuine) =
blanchet@57158
    58
    if genuine then Unprovable else GaveUp
blanchet@58061
    59
  | failure_of_smt_failure SMT_Failure.Time_Out = TimedOut
blanchet@58061
    60
  | failure_of_smt_failure (SMT_Failure.Abnormal_Termination code) =
blanchet@58061
    61
    (case AList.lookup (op =) smt_failures code of
blanchet@56081
    62
      SOME failure => failure
blanchet@56081
    63
    | NONE => UnknownError ("Abnormal termination with exit code " ^ string_of_int code ^ "."))
blanchet@58061
    64
  | failure_of_smt_failure SMT_Failure.Out_Of_Memory = OutOfResources
blanchet@58061
    65
  | failure_of_smt_failure (SMT_Failure.Other_Failure s) = UnknownError s
blanchet@56081
    66
blanchet@56081
    67
(* FUDGE *)
blanchet@58061
    68
val smt_max_slices = Attrib.setup_config_int @{binding sledgehammer_smt_max_slices} (K 8)
blanchet@58061
    69
val smt_slice_fact_frac =
blanchet@58061
    70
  Attrib.setup_config_real @{binding sledgehammer_smt_slice_fact_frac} (K 0.667)
blanchet@58061
    71
val smt_slice_time_frac =
blanchet@58061
    72
  Attrib.setup_config_real @{binding sledgehammer_smt_slice_time_frac} (K 0.333)
blanchet@58061
    73
val smt_slice_min_secs = Attrib.setup_config_int @{binding sledgehammer_smt_slice_min_secs} (K 3)
blanchet@56081
    74
blanchet@56081
    75
val is_boring_builtin_typ =
blanchet@56081
    76
  not o exists_subtype (member (op =) [@{typ nat}, @{typ int}, HOLogic.realT])
blanchet@56081
    77
blanchet@58061
    78
fun smt_filter_loop name ({debug, overlord, max_mono_iters, max_new_mono_instances, timeout, slice,
blanchet@56081
    79
      ...} : params) state goal i =
blanchet@56081
    80
  let
blanchet@56081
    81
    fun repair_context ctxt =
blanchet@58061
    82
      ctxt |> Context.proof_map (SMT_Config.select_solver name)
blanchet@58061
    83
           |> Config.put SMT_Config.verbose debug
blanchet@56081
    84
           |> (if overlord then
blanchet@58061
    85
                 Config.put SMT_Config.debug_files
blanchet@56081
    86
                   (overlord_file_location_of_prover name |> (fn (path, name) => path ^ "/" ^ name))
blanchet@56081
    87
               else
blanchet@56081
    88
                 I)
blanchet@58061
    89
           |> Config.put SMT_Config.infer_triggers (Config.get ctxt smt_triggers)
blanchet@58061
    90
           |> not (Config.get ctxt smt_builtins)
blanchet@58061
    91
              ? (SMT_Builtin.filter_builtins is_boring_builtin_typ
blanchet@58061
    92
                 #> Config.put SMT_Systems.z3_extensions false)
blanchet@56081
    93
           |> repair_monomorph_context max_mono_iters default_max_mono_iters max_new_mono_instances
blanchet@56081
    94
                default_max_new_mono_instances
blanchet@56081
    95
blanchet@56081
    96
    val state = Proof.map_context (repair_context) state
blanchet@56081
    97
    val ctxt = Proof.context_of state
blanchet@58061
    98
    val max_slices = if slice then Config.get ctxt smt_max_slices else 1
blanchet@56081
    99
blanchet@57165
   100
    fun do_slice timeout slice outcome0 time_so_far (factss as (fact_filter, facts) :: _) =
blanchet@56081
   101
      let
blanchet@56081
   102
        val timer = Timer.startRealTimer ()
blanchet@56081
   103
        val slice_timeout =
blanchet@56081
   104
          if slice < max_slices then
blanchet@56081
   105
            let val ms = Time.toMilliseconds timeout in
blanchet@58061
   106
              Int.min (ms, Int.max (1000 * Config.get ctxt smt_slice_min_secs,
blanchet@58061
   107
                Real.ceil (Config.get ctxt smt_slice_time_frac * Real.fromInt ms)))
blanchet@56081
   108
              |> Time.fromMilliseconds
blanchet@56081
   109
            end
blanchet@56081
   110
          else
blanchet@56081
   111
            timeout
blanchet@57165
   112
        val num_facts = length facts
blanchet@56081
   113
        val _ =
blanchet@56081
   114
          if debug then
blanchet@56081
   115
            quote name ^ " slice " ^ string_of_int slice ^ " with " ^ string_of_int num_facts ^
blanchet@56081
   116
            " fact" ^ plural_s num_facts ^ " for " ^ string_of_time slice_timeout
wenzelm@58843
   117
            |> writeln
blanchet@56081
   118
          else
blanchet@56081
   119
            ()
blanchet@56081
   120
        val birth = Timer.checkRealTimer timer
blanchet@56081
   121
blanchet@56104
   122
        val filter_result as {outcome, ...} =
blanchet@58061
   123
          SMT_Solver.smt_filter ctxt goal facts i slice_timeout
blanchet@56081
   124
          handle exn =>
blanchet@56094
   125
            if Exn.is_interrupt exn orelse debug then
wenzelm@62505
   126
              Exn.reraise exn
blanchet@56083
   127
            else
blanchet@58061
   128
              {outcome = SOME (SMT_Failure.Other_Failure (Runtime.exn_message exn)),
blanchet@60201
   129
               fact_ids = NONE, atp_proof = K []}
blanchet@56081
   130
blanchet@56081
   131
        val death = Timer.checkRealTimer timer
blanchet@56081
   132
        val outcome0 = if is_none outcome0 then SOME outcome else outcome0
wenzelm@62826
   133
        val time_so_far = time_so_far + (death - birth)
wenzelm@62826
   134
        val timeout = timeout - Timer.checkRealTimer timer
blanchet@56081
   135
blanchet@56081
   136
        val too_many_facts_perhaps =
blanchet@56081
   137
          (case outcome of
blanchet@56081
   138
            NONE => false
blanchet@58061
   139
          | SOME (SMT_Failure.Counterexample _) => false
blanchet@58061
   140
          | SOME SMT_Failure.Time_Out => slice_timeout <> timeout
blanchet@58061
   141
          | SOME (SMT_Failure.Abnormal_Termination _) => true (* kind of *)
blanchet@58061
   142
          | SOME SMT_Failure.Out_Of_Memory => true
blanchet@58061
   143
          | SOME (SMT_Failure.Other_Failure _) => true)
blanchet@56081
   144
      in
blanchet@56081
   145
        if too_many_facts_perhaps andalso slice < max_slices andalso num_facts > 0 andalso
wenzelm@62826
   146
           timeout > Time.zeroTime then
blanchet@56081
   147
          let
blanchet@56081
   148
            val new_num_facts =
blanchet@58061
   149
              Real.ceil (Config.get ctxt smt_slice_fact_frac * Real.fromInt num_facts)
blanchet@57165
   150
            val factss as (new_fact_filter, _) :: _ =
blanchet@57165
   151
              factss
blanchet@56081
   152
              |> (fn (x :: xs) => xs @ [x])
blanchet@56081
   153
              |> app_hd (apsnd (take new_num_facts))
blanchet@56081
   154
            val show_filter = fact_filter <> new_fact_filter
blanchet@56081
   155
blanchet@56081
   156
            fun num_of_facts fact_filter num_facts =
blanchet@56081
   157
              string_of_int num_facts ^ (if show_filter then " " ^ quote fact_filter else "") ^
blanchet@56081
   158
              " fact" ^ plural_s num_facts
blanchet@56081
   159
blanchet@56081
   160
            val _ =
blanchet@56081
   161
              if debug then
blanchet@56081
   162
                quote name ^ " invoked with " ^
blanchet@56081
   163
                num_of_facts fact_filter num_facts ^ ": " ^
blanchet@58061
   164
                string_of_atp_failure (failure_of_smt_failure (the outcome)) ^
blanchet@56081
   165
                " Retrying with " ^ num_of_facts new_fact_filter new_num_facts ^
blanchet@56081
   166
                "..."
wenzelm@58843
   167
                |> writeln
blanchet@56081
   168
              else
blanchet@56081
   169
                ()
blanchet@56081
   170
          in
blanchet@57165
   171
            do_slice timeout (slice + 1) outcome0 time_so_far factss
blanchet@56081
   172
          end
blanchet@56081
   173
        else
blanchet@56104
   174
          {outcome = if is_none outcome then NONE else the outcome0, filter_result = filter_result,
blanchet@57165
   175
           used_from = facts, run_time = time_so_far}
blanchet@56081
   176
      end
blanchet@56081
   177
  in
blanchet@56081
   178
    do_slice timeout 1 NONE Time.zeroTime
blanchet@56081
   179
  end
blanchet@56081
   180
blanchet@58061
   181
fun run_smt_solver mode name (params as {debug, verbose, isar_proofs, compress, try0, smt_proofs,
blanchet@57245
   182
      minimize, preplay_timeout, ...})
blanchet@62735
   183
    ({state, goal, subgoal, subgoal_count, factss, found_proof, ...} : prover_problem) =
blanchet@56081
   184
  let
blanchet@56081
   185
    val thy = Proof.theory_of state
blanchet@56081
   186
    val ctxt = Proof.context_of state
blanchet@56081
   187
blanchet@57243
   188
    val factss = map (apsnd (map (apsnd (Thm.transfer thy)))) factss
blanchet@57243
   189
blanchet@57159
   190
    val {outcome, filter_result = {fact_ids, atp_proof, ...}, used_from, run_time} =
blanchet@58061
   191
      smt_filter_loop name params state goal subgoal factss
blanchet@60201
   192
    val used_facts =
blanchet@60201
   193
      (case fact_ids of
blanchet@60201
   194
        NONE => map fst used_from
wenzelm@60924
   195
      | SOME ids => sort_by fst (map (fst o snd) ids))
blanchet@58061
   196
    val outcome = Option.map failure_of_smt_failure outcome
blanchet@56081
   197
blanchet@57738
   198
    val (preferred_methss, message) =
blanchet@56081
   199
      (case outcome of
blanchet@56081
   200
        NONE =>
blanchet@57734
   201
        let
blanchet@62735
   202
          val _ = found_proof ();
blanchet@58498
   203
          val smt_method = smt_proofs <> SOME false
blanchet@57734
   204
          val preferred_methss =
blanchet@58498
   205
            (if smt_method then SMT_Method else Metis_Method (NONE, NONE),
blanchet@58498
   206
             bunches_of_proof_methods try0 smt_method false liftingN)
blanchet@57734
   207
        in
blanchet@57734
   208
          (preferred_methss,
blanchet@57734
   209
           fn preplay =>
blanchet@57734
   210
             let
wenzelm@58843
   211
               val _ = if verbose then writeln "Generating proof text..." else ()
blanchet@57723
   212
blanchet@57734
   213
               fun isar_params () =
blanchet@57734
   214
                 (verbose, (NONE, NONE), preplay_timeout, compress, try0, minimize, atp_proof (),
blanchet@57734
   215
                  goal)
blanchet@57056
   216
blanchet@57750
   217
               val one_line_params = (preplay (), proof_banner mode name, subgoal, subgoal_count)
blanchet@57734
   218
               val num_chained = length (#facts (Proof.goal state))
blanchet@57734
   219
             in
blanchet@57738
   220
               proof_text ctxt debug isar_proofs smt_proofs isar_params num_chained
blanchet@57738
   221
                 one_line_params
blanchet@57738
   222
             end)
blanchet@57734
   223
        end
blanchet@57738
   224
      | SOME failure => ((Auto_Method (* dummy *), []), fn _ => string_of_atp_failure failure))
blanchet@56081
   225
  in
blanchet@57734
   226
    {outcome = outcome, used_facts = used_facts, used_from = used_from,
blanchet@57738
   227
     preferred_methss = preferred_methss, run_time = run_time, message = message}
blanchet@56081
   228
  end
blanchet@56081
   229
blanchet@56081
   230
end;