src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML
author blanchet
Fri May 16 19:13:50 2014 +0200 (2014-05-16)
changeset 56981 3ef45ce002b5
parent 56303 4cc3f4db3447
child 56983 132142089ea6
permissions -rw-r--r--
honor original format of conjecture or hypotheses in Z3-to-Isar proofs
blanchet@56081
     1
(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.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@56081
     9
signature SLEDGEHAMMER_PROVER_SMT2 =
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@56081
    15
  val smt2_builtins : bool Config.T
blanchet@56081
    16
  val smt2_triggers : bool Config.T
blanchet@56081
    17
  val smt2_weights : bool Config.T
blanchet@56081
    18
  val smt2_weight_min_facts : int Config.T
blanchet@56081
    19
  val smt2_min_weight : int Config.T
blanchet@56081
    20
  val smt2_max_weight : int Config.T
blanchet@56081
    21
  val smt2_max_weight_index : int Config.T
blanchet@56081
    22
  val smt2_weight_curve : (int -> int) Unsynchronized.ref
blanchet@56081
    23
  val smt2_max_slices : int Config.T
blanchet@56081
    24
  val smt2_slice_fact_frac : real Config.T
blanchet@56081
    25
  val smt2_slice_time_frac : real Config.T
blanchet@56081
    26
  val smt2_slice_min_secs : int Config.T
blanchet@56081
    27
blanchet@56081
    28
  val is_smt2_prover : Proof.context -> string -> bool
blanchet@56081
    29
  val run_smt2_solver : mode -> string -> prover
blanchet@56081
    30
end;
blanchet@56081
    31
blanchet@56081
    32
structure Sledgehammer_Prover_SMT2 : SLEDGEHAMMER_PROVER_SMT2 =
blanchet@56081
    33
struct
blanchet@56081
    34
blanchet@56081
    35
open ATP_Util
blanchet@56081
    36
open ATP_Proof
blanchet@56081
    37
open ATP_Systems
blanchet@56081
    38
open ATP_Problem_Generate
blanchet@56081
    39
open ATP_Proof_Reconstruct
blanchet@56081
    40
open Sledgehammer_Util
blanchet@56081
    41
open Sledgehammer_Proof_Methods
blanchet@56083
    42
open Sledgehammer_Isar
blanchet@56081
    43
open Sledgehammer_Prover
blanchet@56081
    44
blanchet@56081
    45
val smt2_builtins = Attrib.setup_config_bool @{binding sledgehammer_smt2_builtins} (K true)
blanchet@56081
    46
val smt2_triggers = Attrib.setup_config_bool @{binding sledgehammer_smt2_triggers} (K true)
blanchet@56081
    47
val smt2_weights = Attrib.setup_config_bool @{binding sledgehammer_smt2_weights} (K true)
blanchet@56081
    48
val smt2_weight_min_facts =
blanchet@56081
    49
  Attrib.setup_config_int @{binding sledgehammer_smt2_weight_min_facts} (K 20)
blanchet@56081
    50
blanchet@56132
    51
val is_smt2_prover = member (op =) o SMT2_Config.available_solvers_of
blanchet@56081
    52
blanchet@56081
    53
(* FUDGE *)
blanchet@56081
    54
val smt2_min_weight = Attrib.setup_config_int @{binding sledgehammer_smt2_min_weight} (K 0)
blanchet@56081
    55
val smt2_max_weight = Attrib.setup_config_int @{binding sledgehammer_smt2_max_weight} (K 10)
blanchet@56081
    56
val smt2_max_weight_index =
blanchet@56081
    57
  Attrib.setup_config_int @{binding sledgehammer_smt2_max_weight_index} (K 200)
blanchet@56081
    58
val smt2_weight_curve = Unsynchronized.ref (fn x : int => x * x)
blanchet@56081
    59
blanchet@56081
    60
fun smt2_fact_weight ctxt j num_facts =
blanchet@56081
    61
  if Config.get ctxt smt2_weights andalso num_facts >= Config.get ctxt smt2_weight_min_facts then
blanchet@56081
    62
    let
blanchet@56081
    63
      val min = Config.get ctxt smt2_min_weight
blanchet@56081
    64
      val max = Config.get ctxt smt2_max_weight
blanchet@56081
    65
      val max_index = Config.get ctxt smt2_max_weight_index
blanchet@56081
    66
      val curve = !smt2_weight_curve
blanchet@56081
    67
    in
blanchet@56081
    68
      SOME (max - (max - min + 1) * curve (Int.max (0, max_index - j - 1)) div curve max_index)
blanchet@56081
    69
    end
blanchet@56081
    70
  else
blanchet@56081
    71
    NONE
blanchet@56081
    72
blanchet@56081
    73
fun weight_smt2_fact ctxt num_facts ((info, th), j) =
blanchet@56081
    74
  let val thy = Proof_Context.theory_of ctxt in
blanchet@56081
    75
    (info, (smt2_fact_weight ctxt j num_facts, Thm.transfer thy th (* TODO: needed? *)))
blanchet@56081
    76
  end
blanchet@56081
    77
blanchet@56081
    78
(* "SMT2_Failure.Abnormal_Termination" carries the solver's return code. Until these are sorted out
blanchet@56081
    79
   properly in the SMT module, we must interpret these here. *)
blanchet@56081
    80
val z3_failures =
blanchet@56081
    81
  [(101, OutOfResources),
blanchet@56081
    82
   (103, MalformedInput),
blanchet@56081
    83
   (110, MalformedInput),
blanchet@56081
    84
   (112, TimedOut)]
blanchet@56081
    85
val unix_failures =
blanchet@56081
    86
  [(138, Crashed),
blanchet@56081
    87
   (139, Crashed)]
blanchet@56081
    88
val smt2_failures = z3_failures @ unix_failures
blanchet@56081
    89
blanchet@56081
    90
fun failure_of_smt2_failure (SMT2_Failure.Counterexample {is_real_cex, ...}) =
blanchet@56081
    91
    if is_real_cex then Unprovable else GaveUp
blanchet@56081
    92
  | failure_of_smt2_failure SMT2_Failure.Time_Out = TimedOut
blanchet@56081
    93
  | failure_of_smt2_failure (SMT2_Failure.Abnormal_Termination code) =
blanchet@56081
    94
    (case AList.lookup (op =) smt2_failures code of
blanchet@56081
    95
      SOME failure => failure
blanchet@56081
    96
    | NONE => UnknownError ("Abnormal termination with exit code " ^ string_of_int code ^ "."))
blanchet@56081
    97
  | failure_of_smt2_failure SMT2_Failure.Out_Of_Memory = OutOfResources
blanchet@56081
    98
  | failure_of_smt2_failure (SMT2_Failure.Other_Failure s) = UnknownError s
blanchet@56081
    99
blanchet@56081
   100
(* FUDGE *)
blanchet@56081
   101
val smt2_max_slices = Attrib.setup_config_int @{binding sledgehammer_smt2_max_slices} (K 8)
blanchet@56081
   102
val smt2_slice_fact_frac =
blanchet@56081
   103
  Attrib.setup_config_real @{binding sledgehammer_smt2_slice_fact_frac} (K 0.667)
blanchet@56081
   104
val smt2_slice_time_frac =
blanchet@56081
   105
  Attrib.setup_config_real @{binding sledgehammer_smt2_slice_time_frac} (K 0.333)
blanchet@56081
   106
val smt2_slice_min_secs = Attrib.setup_config_int @{binding sledgehammer_smt2_slice_min_secs} (K 3)
blanchet@56081
   107
blanchet@56081
   108
val is_boring_builtin_typ =
blanchet@56081
   109
  not o exists_subtype (member (op =) [@{typ nat}, @{typ int}, HOLogic.realT])
blanchet@56081
   110
blanchet@56081
   111
fun smt2_filter_loop name ({debug, overlord, max_mono_iters, max_new_mono_instances, timeout, slice,
blanchet@56081
   112
      ...} : params) state goal i =
blanchet@56081
   113
  let
blanchet@56081
   114
    fun repair_context ctxt =
blanchet@56081
   115
      ctxt |> Context.proof_map (SMT2_Config.select_solver name)
blanchet@56081
   116
           |> Config.put SMT2_Config.verbose debug
blanchet@56081
   117
           |> (if overlord then
blanchet@56081
   118
                 Config.put SMT2_Config.debug_files
blanchet@56081
   119
                   (overlord_file_location_of_prover name |> (fn (path, name) => path ^ "/" ^ name))
blanchet@56081
   120
               else
blanchet@56081
   121
                 I)
blanchet@56081
   122
           |> Config.put SMT2_Config.infer_triggers (Config.get ctxt smt2_triggers)
blanchet@56081
   123
           |> not (Config.get ctxt smt2_builtins)
blanchet@56081
   124
              ? (SMT2_Builtin.filter_builtins is_boring_builtin_typ
blanchet@56090
   125
                 #> Config.put SMT2_Systems.z3_extensions false)
blanchet@56081
   126
           |> repair_monomorph_context max_mono_iters default_max_mono_iters max_new_mono_instances
blanchet@56081
   127
                default_max_new_mono_instances
blanchet@56081
   128
blanchet@56081
   129
    val state = Proof.map_context (repair_context) state
blanchet@56081
   130
    val ctxt = Proof.context_of state
blanchet@56081
   131
    val max_slices = if slice then Config.get ctxt smt2_max_slices else 1
blanchet@56081
   132
blanchet@56081
   133
    fun do_slice timeout slice outcome0 time_so_far
blanchet@56081
   134
        (weighted_factss as (fact_filter, weighted_facts) :: _) =
blanchet@56081
   135
      let
blanchet@56081
   136
        val timer = Timer.startRealTimer ()
blanchet@56081
   137
        val slice_timeout =
blanchet@56081
   138
          if slice < max_slices then
blanchet@56081
   139
            let val ms = Time.toMilliseconds timeout in
blanchet@56081
   140
              Int.min (ms, Int.max (1000 * Config.get ctxt smt2_slice_min_secs,
blanchet@56081
   141
                Real.ceil (Config.get ctxt smt2_slice_time_frac * Real.fromInt ms)))
blanchet@56081
   142
              |> Time.fromMilliseconds
blanchet@56081
   143
            end
blanchet@56081
   144
          else
blanchet@56081
   145
            timeout
blanchet@56081
   146
        val num_facts = length weighted_facts
blanchet@56081
   147
        val _ =
blanchet@56081
   148
          if debug then
blanchet@56081
   149
            quote name ^ " slice " ^ string_of_int slice ^ " with " ^ string_of_int num_facts ^
blanchet@56081
   150
            " fact" ^ plural_s num_facts ^ " for " ^ string_of_time slice_timeout
blanchet@56081
   151
            |> Output.urgent_message
blanchet@56081
   152
          else
blanchet@56081
   153
            ()
blanchet@56081
   154
        val birth = Timer.checkRealTimer timer
blanchet@56081
   155
        val _ = if debug then Output.urgent_message "Invoking SMT solver..." else ()
blanchet@56081
   156
blanchet@56104
   157
        val filter_result as {outcome, ...} =
blanchet@56104
   158
          SMT2_Solver.smt2_filter ctxt goal weighted_facts i slice_timeout
blanchet@56081
   159
          handle exn =>
blanchet@56094
   160
            if Exn.is_interrupt exn orelse debug then
blanchet@56083
   161
              reraise exn
blanchet@56083
   162
            else
wenzelm@56303
   163
              {outcome = SOME (SMT2_Failure.Other_Failure (Runtime.exn_message exn)),
blanchet@56981
   164
               rewrite_rules = [], conjecture_id = ~1, prem_ids = [], helper_ids = [],
blanchet@56981
   165
               fact_ids = [], z3_proof = []}
blanchet@56081
   166
blanchet@56081
   167
        val death = Timer.checkRealTimer timer
blanchet@56081
   168
        val outcome0 = if is_none outcome0 then SOME outcome else outcome0
blanchet@56081
   169
        val time_so_far = Time.+ (time_so_far, Time.- (death, birth))
blanchet@56083
   170
        val timeout = Time.- (timeout, Timer.checkRealTimer timer)
blanchet@56081
   171
blanchet@56081
   172
        val too_many_facts_perhaps =
blanchet@56081
   173
          (case outcome of
blanchet@56081
   174
            NONE => false
blanchet@56081
   175
          | SOME (SMT2_Failure.Counterexample _) => false
blanchet@56081
   176
          | SOME SMT2_Failure.Time_Out => slice_timeout <> timeout
blanchet@56081
   177
          | SOME (SMT2_Failure.Abnormal_Termination _) => true (* kind of *)
blanchet@56081
   178
          | SOME SMT2_Failure.Out_Of_Memory => true
blanchet@56081
   179
          | SOME (SMT2_Failure.Other_Failure _) => true)
blanchet@56081
   180
      in
blanchet@56081
   181
        if too_many_facts_perhaps andalso slice < max_slices andalso num_facts > 0 andalso
blanchet@56081
   182
           Time.> (timeout, Time.zeroTime) then
blanchet@56081
   183
          let
blanchet@56081
   184
            val new_num_facts =
blanchet@56081
   185
              Real.ceil (Config.get ctxt smt2_slice_fact_frac * Real.fromInt num_facts)
blanchet@56081
   186
            val weighted_factss as (new_fact_filter, _) :: _ =
blanchet@56081
   187
              weighted_factss
blanchet@56081
   188
              |> (fn (x :: xs) => xs @ [x])
blanchet@56081
   189
              |> app_hd (apsnd (take new_num_facts))
blanchet@56081
   190
            val show_filter = fact_filter <> new_fact_filter
blanchet@56081
   191
blanchet@56081
   192
            fun num_of_facts fact_filter num_facts =
blanchet@56081
   193
              string_of_int num_facts ^ (if show_filter then " " ^ quote fact_filter else "") ^
blanchet@56081
   194
              " fact" ^ plural_s num_facts
blanchet@56081
   195
blanchet@56081
   196
            val _ =
blanchet@56081
   197
              if debug then
blanchet@56081
   198
                quote name ^ " invoked with " ^
blanchet@56081
   199
                num_of_facts fact_filter num_facts ^ ": " ^
blanchet@56081
   200
                string_of_atp_failure (failure_of_smt2_failure (the outcome)) ^
blanchet@56081
   201
                " Retrying with " ^ num_of_facts new_fact_filter new_num_facts ^
blanchet@56081
   202
                "..."
blanchet@56081
   203
                |> Output.urgent_message
blanchet@56081
   204
              else
blanchet@56081
   205
                ()
blanchet@56081
   206
          in
blanchet@56081
   207
            do_slice timeout (slice + 1) outcome0 time_so_far weighted_factss
blanchet@56081
   208
          end
blanchet@56081
   209
        else
blanchet@56104
   210
          {outcome = if is_none outcome then NONE else the outcome0, filter_result = filter_result,
blanchet@56104
   211
           used_from = map (apsnd snd) weighted_facts, run_time = time_so_far}
blanchet@56081
   212
      end
blanchet@56081
   213
  in
blanchet@56081
   214
    do_slice timeout 1 NONE Time.zeroTime
blanchet@56081
   215
  end
blanchet@56081
   216
blanchet@56083
   217
fun run_smt2_solver mode name (params as {debug, verbose, isar_proofs, compress_isar,
blanchet@56083
   218
      try0_isar, smt_proofs, minimize, preplay_timeout, ...})
blanchet@56081
   219
    minimize_command ({state, goal, subgoal, subgoal_count, factss, ...} : prover_problem) =
blanchet@56081
   220
  let
blanchet@56081
   221
    val thy = Proof.theory_of state
blanchet@56081
   222
    val ctxt = Proof.context_of state
blanchet@56081
   223
blanchet@56081
   224
    fun weight_facts facts =
blanchet@56081
   225
      let val num_facts = length facts in
blanchet@56081
   226
        map (weight_smt2_fact ctxt num_facts) (facts ~~ (0 upto num_facts - 1))
blanchet@56081
   227
      end
blanchet@56081
   228
blanchet@56099
   229
    val weighted_factss = map (apsnd weight_facts) factss
blanchet@56981
   230
    val {outcome, filter_result = {rewrite_rules, conjecture_id, prem_ids, helper_ids, fact_ids,
blanchet@56981
   231
           z3_proof, ...}, used_from, run_time} =
blanchet@56128
   232
      smt2_filter_loop name params state goal subgoal weighted_factss
blanchet@56104
   233
    val used_named_facts = map snd fact_ids
blanchet@56099
   234
    val used_facts = map fst used_named_facts
blanchet@56099
   235
    val outcome = Option.map failure_of_smt2_failure outcome
blanchet@56081
   236
blanchet@56081
   237
    val (preplay, message, message_tail) =
blanchet@56081
   238
      (case outcome of
blanchet@56081
   239
        NONE =>
blanchet@56081
   240
        (Lazy.lazy (fn () =>
blanchet@56099
   241
           play_one_line_proof mode debug verbose preplay_timeout used_named_facts state subgoal
blanchet@56081
   242
             SMT2_Method (bunch_of_proof_methods (smt_proofs <> SOME false) false liftingN)),
blanchet@56081
   243
         fn preplay =>
blanchet@56081
   244
            let
blanchet@56104
   245
              val fact_ids =
blanchet@56104
   246
                map (fn (id, th) => (id, short_thm_name ctxt th)) helper_ids @
blanchet@56104
   247
                map (fn (id, ((name, _), _)) => (id, name)) fact_ids
blanchet@56981
   248
              val atp_proof = Z3_New_Isar.atp_proof_of_z3_proof thy rewrite_rules prem_ids conjecture_id
blanchet@56128
   249
                fact_ids z3_proof
blanchet@56083
   250
              val isar_params =
blanchet@56083
   251
                K (verbose, (NONE, NONE), preplay_timeout, compress_isar, try0_isar,
blanchet@56083
   252
                   minimize <> SOME false, atp_proof, goal)
blanchet@56081
   253
              val one_line_params =
blanchet@56081
   254
                (preplay, proof_banner mode name, used_facts,
blanchet@56081
   255
                 choose_minimize_command thy params minimize_command name preplay, subgoal,
blanchet@56081
   256
                 subgoal_count)
blanchet@56081
   257
              val num_chained = length (#facts (Proof.goal state))
blanchet@56081
   258
            in
blanchet@56083
   259
              proof_text ctxt debug isar_proofs smt_proofs isar_params num_chained one_line_params
blanchet@56081
   260
            end,
blanchet@56081
   261
         if verbose then "\nSMT solver real CPU time: " ^ string_of_time run_time ^ "." else "")
blanchet@56081
   262
      | SOME failure =>
blanchet@56081
   263
        (Lazy.value (Metis_Method (NONE, NONE), Play_Failed),
blanchet@56081
   264
         fn _ => string_of_atp_failure failure, ""))
blanchet@56081
   265
  in
blanchet@56081
   266
    {outcome = outcome, used_facts = used_facts, used_from = used_from, run_time = run_time,
blanchet@56081
   267
     preplay = preplay, message = message, message_tail = message_tail}
blanchet@56081
   268
  end
blanchet@56081
   269
blanchet@56081
   270
end;