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