src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML
author wenzelm
Thu Mar 27 17:12:40 2014 +0100 (2014-03-27 ago)
changeset 56303 4cc3f4db3447
parent 56081 72fad75baf7e
child 56985 82c83978fbd9
permissions -rw-r--r--
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
blanchet@55205
     1
(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML
blanchet@55205
     2
    Author:     Fabian Immler, TU Muenchen
blanchet@55205
     3
    Author:     Makarius
blanchet@55205
     4
    Author:     Jasmin Blanchette, TU Muenchen
blanchet@55205
     5
blanchet@55205
     6
SMT solvers as Sledgehammer provers.
blanchet@55205
     7
*)
blanchet@55205
     8
blanchet@55205
     9
signature SLEDGEHAMMER_PROVER_SMT =
blanchet@55205
    10
sig
blanchet@55205
    11
  type stature = ATP_Problem_Generate.stature
blanchet@55205
    12
  type mode = Sledgehammer_Prover.mode
blanchet@55205
    13
  type prover = Sledgehammer_Prover.prover
blanchet@55205
    14
blanchet@55205
    15
  val smt_builtins : bool Config.T
blanchet@55205
    16
  val smt_triggers : bool Config.T
blanchet@55205
    17
  val smt_weights : bool Config.T
blanchet@55205
    18
  val smt_weight_min_facts : int Config.T
blanchet@55205
    19
  val smt_min_weight : int Config.T
blanchet@55205
    20
  val smt_max_weight : int Config.T
blanchet@55205
    21
  val smt_max_weight_index : int Config.T
blanchet@55205
    22
  val smt_weight_curve : (int -> int) Unsynchronized.ref
blanchet@55205
    23
  val smt_max_slices : int Config.T
blanchet@55205
    24
  val smt_slice_fact_frac : real Config.T
blanchet@55205
    25
  val smt_slice_time_frac : real Config.T
blanchet@55205
    26
  val smt_slice_min_secs : int Config.T
blanchet@55205
    27
blanchet@55205
    28
  val is_smt_prover : Proof.context -> string -> bool
blanchet@55205
    29
  val run_smt_solver : mode -> string -> prover
blanchet@55205
    30
end;
blanchet@55205
    31
blanchet@55205
    32
structure Sledgehammer_Prover_SMT : SLEDGEHAMMER_PROVER_SMT =
blanchet@55205
    33
struct
blanchet@55205
    34
blanchet@55212
    35
open ATP_Util
blanchet@55205
    36
open ATP_Proof
blanchet@55205
    37
open ATP_Systems
blanchet@55205
    38
open ATP_Problem_Generate
blanchet@55205
    39
open ATP_Proof_Reconstruct
blanchet@55205
    40
open Sledgehammer_Util
blanchet@55287
    41
open Sledgehammer_Proof_Methods
blanchet@55205
    42
open Sledgehammer_Prover
blanchet@55205
    43
blanchet@55205
    44
val smt_builtins = Attrib.setup_config_bool @{binding sledgehammer_smt_builtins} (K true)
blanchet@55205
    45
val smt_triggers = Attrib.setup_config_bool @{binding sledgehammer_smt_triggers} (K true)
blanchet@55205
    46
val smt_weights = Attrib.setup_config_bool @{binding sledgehammer_smt_weights} (K true)
blanchet@55205
    47
val smt_weight_min_facts =
blanchet@55205
    48
  Attrib.setup_config_int @{binding sledgehammer_smt_weight_min_facts} (K 20)
blanchet@55205
    49
blanchet@55205
    50
fun is_smt_prover ctxt = member (op =) (SMT_Solver.available_solvers_of ctxt)
blanchet@55205
    51
blanchet@55205
    52
(* FUDGE *)
blanchet@55212
    53
val smt_min_weight = Attrib.setup_config_int @{binding sledgehammer_smt_min_weight} (K 0)
blanchet@55212
    54
val smt_max_weight = Attrib.setup_config_int @{binding sledgehammer_smt_max_weight} (K 10)
blanchet@55205
    55
val smt_max_weight_index =
blanchet@55205
    56
  Attrib.setup_config_int @{binding sledgehammer_smt_max_weight_index} (K 200)
blanchet@55205
    57
val smt_weight_curve = Unsynchronized.ref (fn x : int => x * x)
blanchet@55205
    58
blanchet@55205
    59
fun smt_fact_weight ctxt j num_facts =
blanchet@55212
    60
  if Config.get ctxt smt_weights andalso num_facts >= Config.get ctxt smt_weight_min_facts then
blanchet@55205
    61
    let
blanchet@55205
    62
      val min = Config.get ctxt smt_min_weight
blanchet@55205
    63
      val max = Config.get ctxt smt_max_weight
blanchet@55205
    64
      val max_index = Config.get ctxt smt_max_weight_index
blanchet@55205
    65
      val curve = !smt_weight_curve
blanchet@55205
    66
    in
blanchet@55212
    67
      SOME (max - (max - min + 1) * curve (Int.max (0, max_index - j - 1)) div curve max_index)
blanchet@55205
    68
    end
blanchet@55205
    69
  else
blanchet@55205
    70
    NONE
blanchet@55205
    71
blanchet@55205
    72
fun weight_smt_fact ctxt num_facts ((info, th), j) =
blanchet@55205
    73
  let val thy = Proof_Context.theory_of ctxt in
blanchet@55452
    74
    (info, (smt_fact_weight ctxt j num_facts, Thm.transfer thy th (* TODO: needed? *)))
blanchet@55205
    75
  end
blanchet@55205
    76
blanchet@55205
    77
(* "SMT_Failure.Abnormal_Termination" carries the solver's return code. Until these are sorted out
blanchet@55205
    78
   properly in the SMT module, we must interpret these here. *)
blanchet@55205
    79
val z3_failures =
blanchet@55205
    80
  [(101, OutOfResources),
blanchet@55205
    81
   (103, MalformedInput),
blanchet@55205
    82
   (110, MalformedInput),
blanchet@55205
    83
   (112, TimedOut)]
blanchet@55205
    84
val unix_failures =
blanchet@55205
    85
  [(138, Crashed),
blanchet@55205
    86
   (139, Crashed)]
blanchet@55205
    87
val smt_failures = z3_failures @ unix_failures
blanchet@55205
    88
blanchet@55205
    89
fun failure_of_smt_failure (SMT_Failure.Counterexample {is_real_cex, ...}) =
blanchet@55205
    90
    if is_real_cex then Unprovable else GaveUp
blanchet@55205
    91
  | failure_of_smt_failure SMT_Failure.Time_Out = TimedOut
blanchet@55205
    92
  | failure_of_smt_failure (SMT_Failure.Abnormal_Termination code) =
blanchet@55205
    93
    (case AList.lookup (op =) smt_failures code of
blanchet@55205
    94
      SOME failure => failure
blanchet@55205
    95
    | NONE => UnknownError ("Abnormal termination with exit code " ^ string_of_int code ^ "."))
blanchet@55205
    96
  | failure_of_smt_failure SMT_Failure.Out_Of_Memory = OutOfResources
blanchet@55205
    97
  | failure_of_smt_failure (SMT_Failure.Other_Failure s) = UnknownError s
blanchet@55205
    98
blanchet@55205
    99
(* FUDGE *)
blanchet@55205
   100
val smt_max_slices = Attrib.setup_config_int @{binding sledgehammer_smt_max_slices} (K 8)
blanchet@55205
   101
val smt_slice_fact_frac =
blanchet@55205
   102
  Attrib.setup_config_real @{binding sledgehammer_smt_slice_fact_frac} (K 0.667)
blanchet@55205
   103
val smt_slice_time_frac =
blanchet@55205
   104
  Attrib.setup_config_real @{binding sledgehammer_smt_slice_time_frac} (K 0.333)
blanchet@55205
   105
val smt_slice_min_secs = Attrib.setup_config_int @{binding sledgehammer_smt_slice_min_secs} (K 3)
blanchet@55205
   106
blanchet@55205
   107
val is_boring_builtin_typ =
blanchet@55205
   108
  not o exists_subtype (member (op =) [@{typ nat}, @{typ int}, HOLogic.realT])
blanchet@55205
   109
blanchet@55205
   110
fun smt_filter_loop name ({debug, overlord, max_mono_iters, max_new_mono_instances, timeout, slice,
blanchet@55205
   111
      ...} : params) state goal i =
blanchet@55205
   112
  let
blanchet@55205
   113
    fun repair_context ctxt =
blanchet@55212
   114
      ctxt |> Context.proof_map (SMT_Config.select_solver name)
blanchet@55205
   115
           |> Config.put SMT_Config.verbose debug
blanchet@55205
   116
           |> (if overlord then
blanchet@55205
   117
                 Config.put SMT_Config.debug_files
blanchet@55205
   118
                   (overlord_file_location_of_prover name |> (fn (path, name) => path ^ "/" ^ name))
blanchet@55205
   119
               else
blanchet@55205
   120
                 I)
blanchet@55205
   121
           |> Config.put SMT_Config.infer_triggers (Config.get ctxt smt_triggers)
blanchet@55205
   122
           |> not (Config.get ctxt smt_builtins)
blanchet@55205
   123
              ? (SMT_Builtin.filter_builtins is_boring_builtin_typ
blanchet@55205
   124
                 #> Config.put SMT_Config.datatypes false)
blanchet@55205
   125
           |> repair_monomorph_context max_mono_iters default_max_mono_iters max_new_mono_instances
blanchet@55205
   126
                default_max_new_mono_instances
blanchet@55205
   127
blanchet@55205
   128
    val state = Proof.map_context (repair_context) state
blanchet@55205
   129
    val ctxt = Proof.context_of state
blanchet@55205
   130
    val max_slices = if slice then Config.get ctxt smt_max_slices else 1
blanchet@55205
   131
blanchet@55205
   132
    fun do_slice timeout slice outcome0 time_so_far
blanchet@55212
   133
        (weighted_factss as (fact_filter, weighted_facts) :: _) =
blanchet@55205
   134
      let
blanchet@55205
   135
        val timer = Timer.startRealTimer ()
blanchet@55205
   136
        val slice_timeout =
blanchet@55205
   137
          if slice < max_slices then
blanchet@55205
   138
            let val ms = Time.toMilliseconds timeout in
blanchet@55205
   139
              Int.min (ms, Int.max (1000 * Config.get ctxt smt_slice_min_secs,
blanchet@55205
   140
                Real.ceil (Config.get ctxt smt_slice_time_frac * Real.fromInt ms)))
blanchet@55205
   141
              |> Time.fromMilliseconds
blanchet@55205
   142
            end
blanchet@55205
   143
          else
blanchet@55205
   144
            timeout
blanchet@55205
   145
        val num_facts = length weighted_facts
blanchet@55205
   146
        val _ =
blanchet@55205
   147
          if debug then
blanchet@55205
   148
            quote name ^ " slice " ^ string_of_int slice ^ " with " ^ string_of_int num_facts ^
blanchet@55205
   149
            " fact" ^ plural_s num_facts ^ " for " ^ string_of_time slice_timeout
blanchet@55205
   150
            |> Output.urgent_message
blanchet@55205
   151
          else
blanchet@55205
   152
            ()
blanchet@55205
   153
        val birth = Timer.checkRealTimer timer
blanchet@55205
   154
        val _ = if debug then Output.urgent_message "Invoking SMT solver..." else ()
blanchet@55205
   155
blanchet@55205
   156
        val (outcome, used_facts) =
blanchet@55205
   157
          SMT_Solver.smt_filter_preprocess ctxt [] goal weighted_facts i
blanchet@55205
   158
          |> SMT_Solver.smt_filter_apply slice_timeout
blanchet@55205
   159
          |> (fn {outcome, used_facts} => (outcome, used_facts))
blanchet@55205
   160
          handle exn =>
blanchet@55205
   161
            if Exn.is_interrupt exn then reraise exn
wenzelm@56303
   162
            else (Runtime.exn_message exn |> SMT_Failure.Other_Failure |> SOME, [])
blanchet@55205
   163
blanchet@55205
   164
        val death = Timer.checkRealTimer timer
blanchet@55205
   165
        val outcome0 = if is_none outcome0 then SOME outcome else outcome0
blanchet@55205
   166
        val time_so_far = Time.+ (time_so_far, Time.- (death, birth))
blanchet@55205
   167
blanchet@55205
   168
        val too_many_facts_perhaps =
blanchet@55205
   169
          (case outcome of
blanchet@55205
   170
            NONE => false
blanchet@55205
   171
          | SOME (SMT_Failure.Counterexample _) => false
blanchet@55205
   172
          | SOME SMT_Failure.Time_Out => slice_timeout <> timeout
blanchet@55205
   173
          | SOME (SMT_Failure.Abnormal_Termination _) => true (* kind of *)
blanchet@55205
   174
          | SOME SMT_Failure.Out_Of_Memory => true
blanchet@55205
   175
          | SOME (SMT_Failure.Other_Failure _) => true)
blanchet@55205
   176
blanchet@55205
   177
        val timeout = Time.- (timeout, Timer.checkRealTimer timer)
blanchet@55205
   178
      in
blanchet@55205
   179
        if too_many_facts_perhaps andalso slice < max_slices andalso num_facts > 0 andalso
blanchet@55205
   180
           Time.> (timeout, Time.zeroTime) then
blanchet@55205
   181
          let
blanchet@55205
   182
            val new_num_facts =
blanchet@55205
   183
              Real.ceil (Config.get ctxt smt_slice_fact_frac * Real.fromInt num_facts)
blanchet@55205
   184
            val weighted_factss as (new_fact_filter, _) :: _ =
blanchet@55205
   185
              weighted_factss
blanchet@55205
   186
              |> (fn (x :: xs) => xs @ [x])
blanchet@55205
   187
              |> app_hd (apsnd (take new_num_facts))
blanchet@55205
   188
            val show_filter = fact_filter <> new_fact_filter
blanchet@55205
   189
blanchet@55205
   190
            fun num_of_facts fact_filter num_facts =
blanchet@55205
   191
              string_of_int num_facts ^ (if show_filter then " " ^ quote fact_filter else "") ^
blanchet@55205
   192
              " fact" ^ plural_s num_facts
blanchet@55205
   193
blanchet@55205
   194
            val _ =
blanchet@55205
   195
              if debug then
blanchet@55205
   196
                quote name ^ " invoked with " ^
blanchet@55205
   197
                num_of_facts fact_filter num_facts ^ ": " ^
blanchet@55205
   198
                string_of_atp_failure (failure_of_smt_failure (the outcome)) ^
blanchet@55205
   199
                " Retrying with " ^ num_of_facts new_fact_filter new_num_facts ^
blanchet@55205
   200
                "..."
blanchet@55205
   201
                |> Output.urgent_message
blanchet@55205
   202
              else
blanchet@55205
   203
                ()
blanchet@55205
   204
          in
blanchet@55205
   205
            do_slice timeout (slice + 1) outcome0 time_so_far weighted_factss
blanchet@55205
   206
          end
blanchet@55205
   207
        else
blanchet@55205
   208
          {outcome = if is_none outcome then NONE else the outcome0, used_facts = used_facts,
blanchet@55205
   209
           used_from = map (apsnd snd) weighted_facts, run_time = time_so_far}
blanchet@55205
   210
      end
blanchet@55205
   211
  in
blanchet@55205
   212
    do_slice timeout 1 NONE Time.zeroTime
blanchet@55205
   213
  end
blanchet@55205
   214
blanchet@55452
   215
fun run_smt_solver mode name (params as {debug, verbose, smt_proofs, preplay_timeout, ...})
blanchet@55288
   216
    minimize_command ({state, goal, subgoal, subgoal_count, factss, ...} : prover_problem) =
blanchet@55205
   217
  let
blanchet@55205
   218
    val thy = Proof.theory_of state
blanchet@55205
   219
    val ctxt = Proof.context_of state
blanchet@55205
   220
blanchet@55205
   221
    fun weight_facts facts =
blanchet@55205
   222
      let val num_facts = length facts in
blanchet@55205
   223
        map (weight_smt_fact ctxt num_facts) (facts ~~ (0 upto num_facts - 1))
blanchet@55205
   224
      end
blanchet@55205
   225
blanchet@55205
   226
    val weighted_factss = factss |> map (apsnd weight_facts)
blanchet@55205
   227
    val {outcome, used_facts = used_pairs, used_from, run_time} =
blanchet@55205
   228
      smt_filter_loop name params state goal subgoal weighted_factss
blanchet@55205
   229
    val used_facts = used_pairs |> map fst
blanchet@55205
   230
    val outcome = outcome |> Option.map failure_of_smt_failure
blanchet@55205
   231
blanchet@55205
   232
    val (preplay, message, message_tail) =
blanchet@55205
   233
      (case outcome of
blanchet@55205
   234
        NONE =>
blanchet@55205
   235
        (Lazy.lazy (fn () =>
blanchet@55452
   236
           play_one_line_proof mode debug verbose preplay_timeout used_pairs state subgoal
blanchet@56081
   237
             SMT2_Method (bunch_of_proof_methods (smt_proofs <> SOME false) false liftingN)),
blanchet@55205
   238
         fn preplay =>
blanchet@55205
   239
            let
blanchet@55205
   240
              val one_line_params =
blanchet@55205
   241
                (preplay, proof_banner mode name, used_facts,
blanchet@55205
   242
                 choose_minimize_command thy params minimize_command name preplay, subgoal,
blanchet@55205
   243
                 subgoal_count)
blanchet@55205
   244
              val num_chained = length (#facts (Proof.goal state))
blanchet@55205
   245
            in
blanchet@55205
   246
              one_line_proof_text num_chained one_line_params
blanchet@55205
   247
            end,
blanchet@55205
   248
         if verbose then "\nSMT solver real CPU time: " ^ string_of_time run_time ^ "." else "")
blanchet@55205
   249
      | SOME failure =>
blanchet@55285
   250
        (Lazy.value (Metis_Method (NONE, NONE), Play_Failed),
blanchet@55285
   251
         fn _ => string_of_atp_failure failure, ""))
blanchet@55205
   252
  in
blanchet@55212
   253
    {outcome = outcome, used_facts = used_facts, used_from = used_from, run_time = run_time,
blanchet@55212
   254
     preplay = preplay, message = message, message_tail = message_tail}
blanchet@55205
   255
  end
blanchet@55205
   256
blanchet@55205
   257
end;