src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML
author blanchet
Tue, 22 Feb 2022 15:00:04 +0100
changeset 75125 18cd39e55eca
parent 75069 455d886009b1
child 75340 e1aa703c8cce
permissions -rw-r--r--
have Sledgehammer honor 'smt_nat_as_int' option
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
58061
3d060f43accb renamed new SMT module from 'SMT2' to 'SMT'
blanchet
parents: 57776
diff changeset
     1
(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML
56081
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
58061
3d060f43accb renamed new SMT module from 'SMT2' to 'SMT'
blanchet
parents: 57776
diff changeset
     9
signature SLEDGEHAMMER_PROVER_SMT =
56081
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
58061
3d060f43accb renamed new SMT module from 'SMT2' to 'SMT'
blanchet
parents: 57776
diff changeset
    15
  val smt_builtins : bool Config.T
3d060f43accb renamed new SMT module from 'SMT2' to 'SMT'
blanchet
parents: 57776
diff changeset
    16
  val smt_triggers : bool Config.T
56081
72fad75baf7e integrate SMT2 with Sledgehammer
blanchet
parents:
diff changeset
    17
58061
3d060f43accb renamed new SMT module from 'SMT2' to 'SMT'
blanchet
parents: 57776
diff changeset
    18
  val is_smt_prover : Proof.context -> string -> bool
75036
212e9ec706cf run all installed provers by default
blanchet
parents: 75033
diff changeset
    19
  val is_smt_prover_installed : Proof.context -> string -> bool
58061
3d060f43accb renamed new SMT module from 'SMT2' to 'SMT'
blanchet
parents: 57776
diff changeset
    20
  val run_smt_solver : mode -> string -> prover
75036
212e9ec706cf run all installed provers by default
blanchet
parents: 75033
diff changeset
    21
212e9ec706cf run all installed provers by default
blanchet
parents: 75033
diff changeset
    22
  val smts : Proof.context -> string list
56081
72fad75baf7e integrate SMT2 with Sledgehammer
blanchet
parents:
diff changeset
    23
end;
72fad75baf7e integrate SMT2 with Sledgehammer
blanchet
parents:
diff changeset
    24
58061
3d060f43accb renamed new SMT module from 'SMT2' to 'SMT'
blanchet
parents: 57776
diff changeset
    25
structure Sledgehammer_Prover_SMT : SLEDGEHAMMER_PROVER_SMT =
56081
72fad75baf7e integrate SMT2 with Sledgehammer
blanchet
parents:
diff changeset
    26
struct
72fad75baf7e integrate SMT2 with Sledgehammer
blanchet
parents:
diff changeset
    27
72fad75baf7e integrate SMT2 with Sledgehammer
blanchet
parents:
diff changeset
    28
open ATP_Util
72fad75baf7e integrate SMT2 with Sledgehammer
blanchet
parents:
diff changeset
    29
open ATP_Proof
72fad75baf7e integrate SMT2 with Sledgehammer
blanchet
parents:
diff changeset
    30
open ATP_Problem_Generate
72fad75baf7e integrate SMT2 with Sledgehammer
blanchet
parents:
diff changeset
    31
open ATP_Proof_Reconstruct
72fad75baf7e integrate SMT2 with Sledgehammer
blanchet
parents:
diff changeset
    32
open Sledgehammer_Util
72fad75baf7e integrate SMT2 with Sledgehammer
blanchet
parents:
diff changeset
    33
open Sledgehammer_Proof_Methods
56083
b5d1d9c60341 have Sledgehammer generate Isar proofs from Z3 proofs
blanchet
parents: 56082
diff changeset
    34
open Sledgehammer_Isar
72400
abfeed05c323 tune filename
desharna
parents: 71931
diff changeset
    35
open Sledgehammer_ATP_Systems
56081
72fad75baf7e integrate SMT2 with Sledgehammer
blanchet
parents:
diff changeset
    36
open Sledgehammer_Prover
72fad75baf7e integrate SMT2 with Sledgehammer
blanchet
parents:
diff changeset
    37
69593
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 63692
diff changeset
    38
val smt_builtins = Attrib.setup_config_bool \<^binding>\<open>sledgehammer_smt_builtins\<close> (K true)
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 63692
diff changeset
    39
val smt_triggers = Attrib.setup_config_bool \<^binding>\<open>sledgehammer_smt_triggers\<close> (K true)
56081
72fad75baf7e integrate SMT2 with Sledgehammer
blanchet
parents:
diff changeset
    40
75040
fada390d49dd tweaked Auto Sledgehammer's behavior and output
blanchet
parents: 75036
diff changeset
    41
val smts = sort_strings o SMT_Config.all_solvers_of
75036
212e9ec706cf run all installed provers by default
blanchet
parents: 75033
diff changeset
    42
212e9ec706cf run all installed provers by default
blanchet
parents: 75033
diff changeset
    43
val is_smt_prover = member (op =) o smts
212e9ec706cf run all installed provers by default
blanchet
parents: 75033
diff changeset
    44
val is_smt_prover_installed = member (op =) o SMT_Config.available_solvers_of
56081
72fad75baf7e integrate SMT2 with Sledgehammer
blanchet
parents:
diff changeset
    45
58061
3d060f43accb renamed new SMT module from 'SMT2' to 'SMT'
blanchet
parents: 57776
diff changeset
    46
(* "SMT_Failure.Abnormal_Termination" carries the solver's return code. Until these are sorted out
56081
72fad75baf7e integrate SMT2 with Sledgehammer
blanchet
parents:
diff changeset
    47
   properly in the SMT module, we must interpret these here. *)
72fad75baf7e integrate SMT2 with Sledgehammer
blanchet
parents:
diff changeset
    48
val z3_failures =
72fad75baf7e integrate SMT2 with Sledgehammer
blanchet
parents:
diff changeset
    49
  [(101, OutOfResources),
72fad75baf7e integrate SMT2 with Sledgehammer
blanchet
parents:
diff changeset
    50
   (103, MalformedInput),
72fad75baf7e integrate SMT2 with Sledgehammer
blanchet
parents:
diff changeset
    51
   (110, MalformedInput),
72fad75baf7e integrate SMT2 with Sledgehammer
blanchet
parents:
diff changeset
    52
   (112, TimedOut)]
72fad75baf7e integrate SMT2 with Sledgehammer
blanchet
parents:
diff changeset
    53
val unix_failures =
59019
0c58b5cf989a other way of crashing (with CVC4)
blanchet
parents: 58843
diff changeset
    54
  [(134, Crashed),
0c58b5cf989a other way of crashing (with CVC4)
blanchet
parents: 58843
diff changeset
    55
   (138, Crashed),
56081
72fad75baf7e integrate SMT2 with Sledgehammer
blanchet
parents:
diff changeset
    56
   (139, Crashed)]
58061
3d060f43accb renamed new SMT module from 'SMT2' to 'SMT'
blanchet
parents: 57776
diff changeset
    57
val smt_failures = z3_failures @ unix_failures
56081
72fad75baf7e integrate SMT2 with Sledgehammer
blanchet
parents:
diff changeset
    58
58061
3d060f43accb renamed new SMT module from 'SMT2' to 'SMT'
blanchet
parents: 57776
diff changeset
    59
fun failure_of_smt_failure (SMT_Failure.Counterexample genuine) =
57158
f028d93798e6 simplified counterexample handling
blanchet
parents: 57078
diff changeset
    60
    if genuine then Unprovable else GaveUp
58061
3d060f43accb renamed new SMT module from 'SMT2' to 'SMT'
blanchet
parents: 57776
diff changeset
    61
  | failure_of_smt_failure SMT_Failure.Time_Out = TimedOut
3d060f43accb renamed new SMT module from 'SMT2' to 'SMT'
blanchet
parents: 57776
diff changeset
    62
  | failure_of_smt_failure (SMT_Failure.Abnormal_Termination code) =
3d060f43accb renamed new SMT module from 'SMT2' to 'SMT'
blanchet
parents: 57776
diff changeset
    63
    (case AList.lookup (op =) smt_failures code of
56081
72fad75baf7e integrate SMT2 with Sledgehammer
blanchet
parents:
diff changeset
    64
      SOME failure => failure
63692
1bc4bc2c9fd1 killed final stops in Sledgehammer and friends
blanchet
parents: 62826
diff changeset
    65
    | NONE => UnknownError ("Abnormal termination with exit code " ^ string_of_int code))
58061
3d060f43accb renamed new SMT module from 'SMT2' to 'SMT'
blanchet
parents: 57776
diff changeset
    66
  | failure_of_smt_failure SMT_Failure.Out_Of_Memory = OutOfResources
3d060f43accb renamed new SMT module from 'SMT2' to 'SMT'
blanchet
parents: 57776
diff changeset
    67
  | failure_of_smt_failure (SMT_Failure.Other_Failure s) = UnknownError s
56081
72fad75baf7e integrate SMT2 with Sledgehammer
blanchet
parents:
diff changeset
    68
72fad75baf7e integrate SMT2 with Sledgehammer
blanchet
parents:
diff changeset
    69
val is_boring_builtin_typ =
69593
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 63692
diff changeset
    70
  not o exists_subtype (member (op =) [\<^typ>\<open>nat\<close>, \<^typ>\<open>int\<close>, HOLogic.realT])
56081
72fad75baf7e integrate SMT2 with Sledgehammer
blanchet
parents:
diff changeset
    71
75017
30ccc472d486 disable slicing within SMT (in preparation for factoring it out)
blanchet
parents: 75016
diff changeset
    72
fun smt_filter name ({debug, overlord, max_mono_iters, max_new_mono_instances,
75063
7ff39293e265 added possibility of extra options to SMT slices
blanchet
parents: 75060
diff changeset
    73
    type_enc, slices, timeout, ...} : params) state goal i facts options =
56081
72fad75baf7e integrate SMT2 with Sledgehammer
blanchet
parents:
diff changeset
    74
  let
75023
fdda7e754f45 changed logic of 'slice' option to 'slices'
blanchet
parents: 75020
diff changeset
    75
    val run_timeout = slice_timeout slices timeout
74891
db4b8dd587a5 added support for higher-order SMT proof search in Sledgehammer
desharna
parents: 72798
diff changeset
    76
    val (higher_order, nat_as_int) =
db4b8dd587a5 added support for higher-order SMT proof search in Sledgehammer
desharna
parents: 72798
diff changeset
    77
      (case type_enc of
75125
18cd39e55eca have Sledgehammer honor 'smt_nat_as_int' option
blanchet
parents: 75069
diff changeset
    78
        SOME s => (SOME (String.isSubstring "native_higher" s), SOME (String.isSubstring "arith" s))
18cd39e55eca have Sledgehammer honor 'smt_nat_as_int' option
blanchet
parents: 75069
diff changeset
    79
      | NONE => (NONE, NONE))
75017
30ccc472d486 disable slicing within SMT (in preparation for factoring it out)
blanchet
parents: 75016
diff changeset
    80
    fun repair_context ctxt = ctxt
30ccc472d486 disable slicing within SMT (in preparation for factoring it out)
blanchet
parents: 75016
diff changeset
    81
      |> Context.proof_map (SMT_Config.select_solver name)
75125
18cd39e55eca have Sledgehammer honor 'smt_nat_as_int' option
blanchet
parents: 75069
diff changeset
    82
      |> (case higher_order of
18cd39e55eca have Sledgehammer honor 'smt_nat_as_int' option
blanchet
parents: 75069
diff changeset
    83
           SOME higher_order => Config.put SMT_Config.higher_order higher_order
18cd39e55eca have Sledgehammer honor 'smt_nat_as_int' option
blanchet
parents: 75069
diff changeset
    84
         | NONE => I)
18cd39e55eca have Sledgehammer honor 'smt_nat_as_int' option
blanchet
parents: 75069
diff changeset
    85
      |> (case nat_as_int of
18cd39e55eca have Sledgehammer honor 'smt_nat_as_int' option
blanchet
parents: 75069
diff changeset
    86
           SOME nat_as_int => Config.put SMT_Config.nat_as_int nat_as_int
18cd39e55eca have Sledgehammer honor 'smt_nat_as_int' option
blanchet
parents: 75069
diff changeset
    87
         | NONE => I)
75017
30ccc472d486 disable slicing within SMT (in preparation for factoring it out)
blanchet
parents: 75016
diff changeset
    88
      |> (if overlord then
30ccc472d486 disable slicing within SMT (in preparation for factoring it out)
blanchet
parents: 75016
diff changeset
    89
            Config.put SMT_Config.debug_files
30ccc472d486 disable slicing within SMT (in preparation for factoring it out)
blanchet
parents: 75016
diff changeset
    90
              (overlord_file_location_of_prover name |> (fn (path, name) => path ^ "/" ^ name))
30ccc472d486 disable slicing within SMT (in preparation for factoring it out)
blanchet
parents: 75016
diff changeset
    91
          else
30ccc472d486 disable slicing within SMT (in preparation for factoring it out)
blanchet
parents: 75016
diff changeset
    92
            I)
30ccc472d486 disable slicing within SMT (in preparation for factoring it out)
blanchet
parents: 75016
diff changeset
    93
       |> Config.put SMT_Config.infer_triggers (Config.get ctxt smt_triggers)
30ccc472d486 disable slicing within SMT (in preparation for factoring it out)
blanchet
parents: 75016
diff changeset
    94
       |> not (Config.get ctxt smt_builtins)
30ccc472d486 disable slicing within SMT (in preparation for factoring it out)
blanchet
parents: 75016
diff changeset
    95
         ? (SMT_Builtin.filter_builtins is_boring_builtin_typ
30ccc472d486 disable slicing within SMT (in preparation for factoring it out)
blanchet
parents: 75016
diff changeset
    96
            #> Config.put SMT_Systems.z3_extensions false)
30ccc472d486 disable slicing within SMT (in preparation for factoring it out)
blanchet
parents: 75016
diff changeset
    97
       |> repair_monomorph_context max_mono_iters default_max_mono_iters max_new_mono_instances
30ccc472d486 disable slicing within SMT (in preparation for factoring it out)
blanchet
parents: 75016
diff changeset
    98
         default_max_new_mono_instances
56081
72fad75baf7e integrate SMT2 with Sledgehammer
blanchet
parents:
diff changeset
    99
72fad75baf7e integrate SMT2 with Sledgehammer
blanchet
parents:
diff changeset
   100
    val state = Proof.map_context (repair_context) state
72fad75baf7e integrate SMT2 with Sledgehammer
blanchet
parents:
diff changeset
   101
    val ctxt = Proof.context_of state
72fad75baf7e integrate SMT2 with Sledgehammer
blanchet
parents:
diff changeset
   102
75017
30ccc472d486 disable slicing within SMT (in preparation for factoring it out)
blanchet
parents: 75016
diff changeset
   103
    val timer = Timer.startRealTimer ()
30ccc472d486 disable slicing within SMT (in preparation for factoring it out)
blanchet
parents: 75016
diff changeset
   104
    val birth = Timer.checkRealTimer timer
56081
72fad75baf7e integrate SMT2 with Sledgehammer
blanchet
parents:
diff changeset
   105
75017
30ccc472d486 disable slicing within SMT (in preparation for factoring it out)
blanchet
parents: 75016
diff changeset
   106
    val filter_result as {outcome, ...} =
75063
7ff39293e265 added possibility of extra options to SMT slices
blanchet
parents: 75060
diff changeset
   107
      SMT_Solver.smt_filter ctxt goal facts i run_timeout options
75017
30ccc472d486 disable slicing within SMT (in preparation for factoring it out)
blanchet
parents: 75016
diff changeset
   108
      handle exn =>
30ccc472d486 disable slicing within SMT (in preparation for factoring it out)
blanchet
parents: 75016
diff changeset
   109
      if Exn.is_interrupt exn orelse debug then
30ccc472d486 disable slicing within SMT (in preparation for factoring it out)
blanchet
parents: 75016
diff changeset
   110
        Exn.reraise exn
30ccc472d486 disable slicing within SMT (in preparation for factoring it out)
blanchet
parents: 75016
diff changeset
   111
      else
30ccc472d486 disable slicing within SMT (in preparation for factoring it out)
blanchet
parents: 75016
diff changeset
   112
        {outcome = SOME (SMT_Failure.Other_Failure (Runtime.exn_message exn)), fact_ids = NONE,
30ccc472d486 disable slicing within SMT (in preparation for factoring it out)
blanchet
parents: 75016
diff changeset
   113
         atp_proof = K []}
56081
72fad75baf7e integrate SMT2 with Sledgehammer
blanchet
parents:
diff changeset
   114
75017
30ccc472d486 disable slicing within SMT (in preparation for factoring it out)
blanchet
parents: 75016
diff changeset
   115
    val death = Timer.checkRealTimer timer
30ccc472d486 disable slicing within SMT (in preparation for factoring it out)
blanchet
parents: 75016
diff changeset
   116
    val run_time = death - birth
56081
72fad75baf7e integrate SMT2 with Sledgehammer
blanchet
parents:
diff changeset
   117
  in
75017
30ccc472d486 disable slicing within SMT (in preparation for factoring it out)
blanchet
parents: 75016
diff changeset
   118
    {outcome = outcome, filter_result = filter_result, used_from = facts, run_time = run_time}
56081
72fad75baf7e integrate SMT2 with Sledgehammer
blanchet
parents:
diff changeset
   119
  end
72fad75baf7e integrate SMT2 with Sledgehammer
blanchet
parents:
diff changeset
   120
75067
c23aa0d177b4 used max_facts and fact_filter from slice for both ATP and SMT in sledgehammer
desharna
parents: 75063
diff changeset
   121
fun run_smt_solver mode name (params as {debug, verbose, isar_proofs, compress, try0,
75017
30ccc472d486 disable slicing within SMT (in preparation for factoring it out)
blanchet
parents: 75016
diff changeset
   122
      smt_proofs, minimize, preplay_timeout, ...})
75025
f741d55a81e5 thread slices through
blanchet
parents: 75023
diff changeset
   123
    ({state, goal, subgoal, subgoal_count, factss, found_proof, ...} : prover_problem)
f741d55a81e5 thread slices through
blanchet
parents: 75023
diff changeset
   124
    slice =
56081
72fad75baf7e integrate SMT2 with Sledgehammer
blanchet
parents:
diff changeset
   125
  let
75069
455d886009b1 uniformized fact selection for ATP and SMT in Sledgehammer
desharna
parents: 75067
diff changeset
   126
    val (basic_slice, SMT_Slice options) = slice
455d886009b1 uniformized fact selection for ATP and SMT in Sledgehammer
desharna
parents: 75067
diff changeset
   127
    val facts = facts_of_basic_slice basic_slice factss
56081
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
57159
24cbdebba35a refactored Z3 to Isar proof construction code
blanchet
parents: 57158
diff changeset
   130
    val {outcome, filter_result = {fact_ids, atp_proof, ...}, used_from, run_time} =
75063
7ff39293e265 added possibility of extra options to SMT slices
blanchet
parents: 75060
diff changeset
   131
      smt_filter name params state goal subgoal facts options
60201
90e88e521e0e made CVC4 support work also without unsat cores
blanchet
parents: 59019
diff changeset
   132
    val used_facts =
90e88e521e0e made CVC4 support work also without unsat cores
blanchet
parents: 59019
diff changeset
   133
      (case fact_ids of
90e88e521e0e made CVC4 support work also without unsat cores
blanchet
parents: 59019
diff changeset
   134
        NONE => map fst used_from
60924
610794dff23c tuned signature, in accordance to sortBy in Scala;
wenzelm
parents: 60201
diff changeset
   135
      | SOME ids => sort_by fst (map (fst o snd) ids))
58061
3d060f43accb renamed new SMT module from 'SMT2' to 'SMT'
blanchet
parents: 57776
diff changeset
   136
    val outcome = Option.map failure_of_smt_failure outcome
56081
72fad75baf7e integrate SMT2 with Sledgehammer
blanchet
parents:
diff changeset
   137
57738
25d1495e6641 eliminated needlessly complex message tail
blanchet
parents: 57735
diff changeset
   138
    val (preferred_methss, message) =
56081
72fad75baf7e integrate SMT2 with Sledgehammer
blanchet
parents:
diff changeset
   139
      (case outcome of
72fad75baf7e integrate SMT2 with Sledgehammer
blanchet
parents:
diff changeset
   140
        NONE =>
57734
18bb3e1ff6f6 rationalized preplaying by eliminating (now superfluous) laziness
blanchet
parents: 57732
diff changeset
   141
        let
75020
b087610592b4 rationalized output for forthcoming slicing model
blanchet
parents: 75017
diff changeset
   142
          val _ = found_proof name;
72518
4be6ae020fc4 Added smt (verit) to Sledgehammer's proof preplay.
desharna
parents: 72400
diff changeset
   143
          val preferred =
4be6ae020fc4 Added smt (verit) to Sledgehammer's proof preplay.
desharna
parents: 72400
diff changeset
   144
            if smt_proofs then
72798
e732c98b02e6 tuned proof preplay to explicitly refer to Z3 backend
desharna
parents: 72518
diff changeset
   145
              SMT_Method (if name = "verit" then SMT_Verit "default" else SMT_Z3)
72518
4be6ae020fc4 Added smt (verit) to Sledgehammer's proof preplay.
desharna
parents: 72400
diff changeset
   146
            else
4be6ae020fc4 Added smt (verit) to Sledgehammer's proof preplay.
desharna
parents: 72400
diff changeset
   147
              Metis_Method (NONE, NONE);
4be6ae020fc4 Added smt (verit) to Sledgehammer's proof preplay.
desharna
parents: 72400
diff changeset
   148
          val methss = bunches_of_proof_methods ctxt try0 smt_proofs false liftingN;
57734
18bb3e1ff6f6 rationalized preplaying by eliminating (now superfluous) laziness
blanchet
parents: 57732
diff changeset
   149
        in
72518
4be6ae020fc4 Added smt (verit) to Sledgehammer's proof preplay.
desharna
parents: 72400
diff changeset
   150
          ((preferred, methss),
57734
18bb3e1ff6f6 rationalized preplaying by eliminating (now superfluous) laziness
blanchet
parents: 57732
diff changeset
   151
           fn preplay =>
18bb3e1ff6f6 rationalized preplaying by eliminating (now superfluous) laziness
blanchet
parents: 57732
diff changeset
   152
             let
58843
521cea5fa777 discontinued obsolete Output.urgent_message;
wenzelm
parents: 58498
diff changeset
   153
               val _ = if verbose then writeln "Generating proof text..." else ()
57723
668322cd58f4 use parallel preplay machinery also for one-line proofs
blanchet
parents: 57721
diff changeset
   154
57734
18bb3e1ff6f6 rationalized preplaying by eliminating (now superfluous) laziness
blanchet
parents: 57732
diff changeset
   155
               fun isar_params () =
18bb3e1ff6f6 rationalized preplaying by eliminating (now superfluous) laziness
blanchet
parents: 57732
diff changeset
   156
                 (verbose, (NONE, NONE), preplay_timeout, compress, try0, minimize, atp_proof (),
18bb3e1ff6f6 rationalized preplaying by eliminating (now superfluous) laziness
blanchet
parents: 57732
diff changeset
   157
                  goal)
57056
8b2283566f6e properly reconstruct helpers in Z3 proofs
blanchet
parents: 57054
diff changeset
   158
57750
670cbec816b9 restored a bit of laziness
blanchet
parents: 57742
diff changeset
   159
               val one_line_params = (preplay (), proof_banner mode name, subgoal, subgoal_count)
57734
18bb3e1ff6f6 rationalized preplaying by eliminating (now superfluous) laziness
blanchet
parents: 57732
diff changeset
   160
               val num_chained = length (#facts (Proof.goal state))
18bb3e1ff6f6 rationalized preplaying by eliminating (now superfluous) laziness
blanchet
parents: 57732
diff changeset
   161
             in
71931
0c8a9c028304 simplified 'smt_proofs' option to be a binary option (instead of ternary), now that SMT proofs are accepted in the AFP (done with Martin Desharnais)
blanchet
parents: 69593
diff changeset
   162
               proof_text ctxt debug isar_proofs smt_proofs isar_params num_chained one_line_params
57738
25d1495e6641 eliminated needlessly complex message tail
blanchet
parents: 57735
diff changeset
   163
             end)
57734
18bb3e1ff6f6 rationalized preplaying by eliminating (now superfluous) laziness
blanchet
parents: 57732
diff changeset
   164
        end
57738
25d1495e6641 eliminated needlessly complex message tail
blanchet
parents: 57735
diff changeset
   165
      | SOME failure => ((Auto_Method (* dummy *), []), fn _ => string_of_atp_failure failure))
56081
72fad75baf7e integrate SMT2 with Sledgehammer
blanchet
parents:
diff changeset
   166
  in
57734
18bb3e1ff6f6 rationalized preplaying by eliminating (now superfluous) laziness
blanchet
parents: 57732
diff changeset
   167
    {outcome = outcome, used_facts = used_facts, used_from = used_from,
57738
25d1495e6641 eliminated needlessly complex message tail
blanchet
parents: 57735
diff changeset
   168
     preferred_methss = preferred_methss, run_time = run_time, message = message}
56081
72fad75baf7e integrate SMT2 with Sledgehammer
blanchet
parents:
diff changeset
   169
  end
72fad75baf7e integrate SMT2 with Sledgehammer
blanchet
parents:
diff changeset
   170
72fad75baf7e integrate SMT2 with Sledgehammer
blanchet
parents:
diff changeset
   171
end;