src/HOL/Tools/Sledgehammer/sledgehammer_run.ML
author blanchet
Fri, 17 Dec 2010 15:30:43 +0100
changeset 41242 8edeb1dbbc76
parent 41208 1b28c43a7074
child 41245 cddc7db22bc9
permissions -rw-r--r--
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
41087
d7b5fd465198 split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
blanchet
parents: 41066
diff changeset
     1
(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_run.ML
28477
9339d4dcec8b version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff changeset
     2
    Author:     Fabian Immler, TU Muenchen
32996
d2e48879e65a removed disjunctive group cancellation -- provers run independently;
wenzelm
parents: 32995
diff changeset
     3
    Author:     Makarius
35969
c9565298df9e added support for Sledgehammer parameters;
blanchet
parents: 35867
diff changeset
     4
    Author:     Jasmin Blanchette, TU Muenchen
28477
9339d4dcec8b version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff changeset
     5
38021
e024504943d1 rename "ATP_Manager" ML module to "Sledgehammer";
blanchet
parents: 38020
diff changeset
     6
Sledgehammer's heart.
28477
9339d4dcec8b version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff changeset
     7
*)
9339d4dcec8b version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff changeset
     8
41087
d7b5fd465198 split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
blanchet
parents: 41066
diff changeset
     9
signature SLEDGEHAMMER_RUN =
28477
9339d4dcec8b version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff changeset
    10
sig
38988
483879af0643 finished renaming
blanchet
parents: 38985
diff changeset
    11
  type relevance_override = Sledgehammer_Filter.relevance_override
40068
ed2869dd9bfa renamed modules
blanchet
parents: 40065
diff changeset
    12
  type minimize_command = Sledgehammer_ATP_Reconstruct.minimize_command
41087
d7b5fd465198 split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
blanchet
parents: 41066
diff changeset
    13
  type params = Sledgehammer_Provers.params
40061
71cc5aac8b76 generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents: 40060
diff changeset
    14
38044
463177795c49 minor refactoring
blanchet
parents: 38040
diff changeset
    15
  val run_sledgehammer :
39318
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 39263
diff changeset
    16
    params -> bool -> int -> relevance_override -> (string -> minimize_command)
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 39263
diff changeset
    17
    -> Proof.state -> bool * Proof.state
28477
9339d4dcec8b version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff changeset
    18
end;
9339d4dcec8b version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff changeset
    19
41087
d7b5fd465198 split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
blanchet
parents: 41066
diff changeset
    20
structure Sledgehammer_Run : SLEDGEHAMMER_RUN =
28477
9339d4dcec8b version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff changeset
    21
struct
9339d4dcec8b version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff changeset
    22
38023
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
    23
open Sledgehammer_Util
38988
483879af0643 finished renaming
blanchet
parents: 38985
diff changeset
    24
open Sledgehammer_Filter
40068
ed2869dd9bfa renamed modules
blanchet
parents: 40065
diff changeset
    25
open Sledgehammer_ATP_Translate
41087
d7b5fd465198 split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
blanchet
parents: 41066
diff changeset
    26
open Sledgehammer_Provers
41091
0afdf5cde874 implicitly call the minimizer for SMT solvers that don't return an unsat core
blanchet
parents: 41090
diff changeset
    27
open Sledgehammer_Minimize
40072
27f2a45b0aab more robust handling of "remote_" vs. non-"remote_" provers
blanchet
parents: 40071
diff changeset
    28
41208
1b28c43a7074 make "debug" imply "blocking", since in blocking mode the exceptions flow through and are more instructive
blanchet
parents: 41180
diff changeset
    29
fun prover_description ctxt ({verbose, blocking, ...} : params) name num_facts i
41089
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    30
                       n goal =
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    31
  quote name ^
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    32
  (if verbose then
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    33
     " with " ^ string_of_int num_facts ^ " fact" ^ plural_s num_facts
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    34
   else
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    35
     "") ^
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    36
  " on " ^ (if n = 1 then "goal" else "subgoal " ^ string_of_int i) ^ ":" ^
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    37
  (if blocking then
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    38
     ""
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    39
   else
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    40
     "\n" ^ Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i)))
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    41
41091
0afdf5cde874 implicitly call the minimizer for SMT solvers that don't return an unsat core
blanchet
parents: 41090
diff changeset
    42
val implicit_minimization_threshold = 50
0afdf5cde874 implicitly call the minimizer for SMT solvers that don't return an unsat core
blanchet
parents: 41090
diff changeset
    43
41208
1b28c43a7074 make "debug" imply "blocking", since in blocking mode the exceptions flow through and are more instructive
blanchet
parents: 41180
diff changeset
    44
fun run_prover (params as {debug, blocking, max_relevant, timeout, expect, ...})
41089
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    45
               auto minimize_command only
41242
8edeb1dbbc76 run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents: 41208
diff changeset
    46
               {state, goal, subgoal, subgoal_count, facts, smt_head} name =
41089
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    47
  let
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    48
    val ctxt = Proof.context_of state
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    49
    val birth_time = Time.now ()
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    50
    val death_time = Time.+ (birth_time, timeout)
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    51
    val max_relevant =
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    52
      the_default (default_max_relevant_for_prover ctxt name) max_relevant
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    53
    val num_facts = length facts |> not only ? Integer.min max_relevant
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    54
    val desc =
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    55
      prover_description ctxt params name num_facts subgoal subgoal_count goal
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    56
    val prover = get_prover ctxt auto name
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    57
    val problem =
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    58
      {state = state, goal = goal, subgoal = subgoal,
41242
8edeb1dbbc76 run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents: 41208
diff changeset
    59
       subgoal_count = subgoal_count, facts = take num_facts facts,
8edeb1dbbc76 run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents: 41208
diff changeset
    60
       smt_head = smt_head}
41089
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    61
    fun go () =
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    62
      let
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    63
        fun really_go () =
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    64
          prover params (minimize_command name) problem
41091
0afdf5cde874 implicitly call the minimizer for SMT solvers that don't return an unsat core
blanchet
parents: 41090
diff changeset
    65
          |> (fn {outcome, used_facts, message, ...} =>
0afdf5cde874 implicitly call the minimizer for SMT solvers that don't return an unsat core
blanchet
parents: 41090
diff changeset
    66
                 if is_some outcome then
0afdf5cde874 implicitly call the minimizer for SMT solvers that don't return an unsat core
blanchet
parents: 41090
diff changeset
    67
                   ("none", message)
0afdf5cde874 implicitly call the minimizer for SMT solvers that don't return an unsat core
blanchet
parents: 41090
diff changeset
    68
                 else
0afdf5cde874 implicitly call the minimizer for SMT solvers that don't return an unsat core
blanchet
parents: 41090
diff changeset
    69
                   ("some",
0afdf5cde874 implicitly call the minimizer for SMT solvers that don't return an unsat core
blanchet
parents: 41090
diff changeset
    70
                    if length used_facts >= implicit_minimization_threshold then
0afdf5cde874 implicitly call the minimizer for SMT solvers that don't return an unsat core
blanchet
parents: 41090
diff changeset
    71
                      minimize_facts params true subgoal subgoal_count state
0afdf5cde874 implicitly call the minimizer for SMT solvers that don't return an unsat core
blanchet
parents: 41090
diff changeset
    72
                          (filter_used_facts used_facts
0afdf5cde874 implicitly call the minimizer for SMT solvers that don't return an unsat core
blanchet
parents: 41090
diff changeset
    73
                               (map (apsnd single o untranslated_fact) facts))
0afdf5cde874 implicitly call the minimizer for SMT solvers that don't return an unsat core
blanchet
parents: 41090
diff changeset
    74
                      |> snd
0afdf5cde874 implicitly call the minimizer for SMT solvers that don't return an unsat core
blanchet
parents: 41090
diff changeset
    75
                    else
0afdf5cde874 implicitly call the minimizer for SMT solvers that don't return an unsat core
blanchet
parents: 41090
diff changeset
    76
                      message))
41089
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    77
        val (outcome_code, message) =
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    78
          if debug then
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    79
            really_go ()
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    80
          else
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    81
            (really_go ()
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    82
             handle ERROR message => ("unknown", "Error: " ^ message ^ "\n")
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    83
                  | exn =>
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    84
                    if Exn.is_interrupt exn then
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    85
                      reraise exn
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    86
                    else
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    87
                      ("unknown", "Internal error:\n" ^
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    88
                                  ML_Compiler.exn_message exn ^ "\n"))
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    89
        val _ =
41142
43e2b051339c weaken the "expect" flag so that it doesn't trigger errors if a prover is not installed
blanchet
parents: 41138
diff changeset
    90
          (* The "expect" argument is deliberately ignored if the prover is
43e2b051339c weaken the "expect" flag so that it doesn't trigger errors if a prover is not installed
blanchet
parents: 41138
diff changeset
    91
             missing so that the "Metis_Examples" can be processed on any
43e2b051339c weaken the "expect" flag so that it doesn't trigger errors if a prover is not installed
blanchet
parents: 41138
diff changeset
    92
             machine. *)
43e2b051339c weaken the "expect" flag so that it doesn't trigger errors if a prover is not installed
blanchet
parents: 41138
diff changeset
    93
          if expect = "" orelse outcome_code = expect orelse
43e2b051339c weaken the "expect" flag so that it doesn't trigger errors if a prover is not installed
blanchet
parents: 41138
diff changeset
    94
             not (is_prover_installed ctxt name) then
41089
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    95
            ()
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    96
          else if blocking then
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    97
            error ("Unexpected outcome: " ^ quote outcome_code ^ ".")
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    98
          else
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    99
            warning ("Unexpected outcome: " ^ quote outcome_code ^ ".");
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   100
      in (outcome_code = "some", message) end
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   101
  in
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   102
    if auto then
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   103
      let val (success, message) = TimeLimit.timeLimit timeout go () in
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   104
        (success, state |> success ? Proof.goal_message (fn () =>
41091
0afdf5cde874 implicitly call the minimizer for SMT solvers that don't return an unsat core
blanchet
parents: 41090
diff changeset
   105
             Pretty.chunks [Pretty.str "",
0afdf5cde874 implicitly call the minimizer for SMT solvers that don't return an unsat core
blanchet
parents: 41090
diff changeset
   106
                            Pretty.mark Markup.hilite (Pretty.str message)]))
41089
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   107
      end
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   108
    else if blocking then
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   109
      let val (success, message) = TimeLimit.timeLimit timeout go () in
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   110
        List.app Output.urgent_message
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   111
                 (Async_Manager.break_into_chunks [desc ^ "\n" ^ message]);
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   112
        (success, state)
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   113
      end
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   114
    else
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   115
      (Async_Manager.launch das_Tool birth_time death_time desc (snd o go);
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   116
       (false, state))
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   117
  end
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   118
41242
8edeb1dbbc76 run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents: 41208
diff changeset
   119
val smt_weights = Unsynchronized.ref true
8edeb1dbbc76 run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents: 41208
diff changeset
   120
val smt_weight_min_facts = 20
8edeb1dbbc76 run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents: 41208
diff changeset
   121
8edeb1dbbc76 run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents: 41208
diff changeset
   122
(* FUDGE *)
8edeb1dbbc76 run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents: 41208
diff changeset
   123
val smt_min_weight = Unsynchronized.ref 0
8edeb1dbbc76 run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents: 41208
diff changeset
   124
val smt_max_weight = Unsynchronized.ref 10
8edeb1dbbc76 run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents: 41208
diff changeset
   125
val smt_max_index = Unsynchronized.ref 200
8edeb1dbbc76 run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents: 41208
diff changeset
   126
val smt_weight_curve = Unsynchronized.ref (fn x : int => x * x)
8edeb1dbbc76 run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents: 41208
diff changeset
   127
8edeb1dbbc76 run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents: 41208
diff changeset
   128
fun smt_fact_weight j num_facts =
8edeb1dbbc76 run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents: 41208
diff changeset
   129
  if !smt_weights andalso num_facts >= smt_weight_min_facts then
8edeb1dbbc76 run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents: 41208
diff changeset
   130
    SOME (!smt_max_weight
8edeb1dbbc76 run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents: 41208
diff changeset
   131
          - (!smt_max_weight - !smt_min_weight + 1)
8edeb1dbbc76 run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents: 41208
diff changeset
   132
            * !smt_weight_curve (Int.max (0, !smt_max_index - j - 1))
8edeb1dbbc76 run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents: 41208
diff changeset
   133
            div !smt_weight_curve (!smt_max_index))
8edeb1dbbc76 run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents: 41208
diff changeset
   134
  else
8edeb1dbbc76 run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents: 41208
diff changeset
   135
    NONE
8edeb1dbbc76 run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents: 41208
diff changeset
   136
8edeb1dbbc76 run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents: 41208
diff changeset
   137
fun weight_smt_fact thy num_facts (fact, j) =
8edeb1dbbc76 run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents: 41208
diff changeset
   138
  fact |> apsnd (pair (smt_fact_weight j num_facts) o Thm.transfer thy)
8edeb1dbbc76 run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents: 41208
diff changeset
   139
8edeb1dbbc76 run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents: 41208
diff changeset
   140
fun class_of_smt_solver ctxt name =
8edeb1dbbc76 run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents: 41208
diff changeset
   141
  ctxt |> select_smt_solver name
8edeb1dbbc76 run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents: 41208
diff changeset
   142
       |> SMT_Config.solver_class_of |> SMT_Utils.string_of_class
8edeb1dbbc76 run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents: 41208
diff changeset
   143
8edeb1dbbc76 run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents: 41208
diff changeset
   144
(* Makes backtraces more transparent and might be more efficient as well. *)
8edeb1dbbc76 run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents: 41208
diff changeset
   145
fun smart_par_list_map _ [] = []
8edeb1dbbc76 run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents: 41208
diff changeset
   146
  | smart_par_list_map f [x] = [f x]
8edeb1dbbc76 run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents: 41208
diff changeset
   147
  | smart_par_list_map f xs = Par_List.map f xs
8edeb1dbbc76 run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents: 41208
diff changeset
   148
40698
8a3f7ea91370 cosmetics
blanchet
parents: 40693
diff changeset
   149
(* FUDGE *)
8a3f7ea91370 cosmetics
blanchet
parents: 40693
diff changeset
   150
val auto_max_relevant_divisor = 2
40060
5ef6747aa619 first step in adding support for an SMT backend to Sledgehammer
blanchet
parents: 40059
diff changeset
   151
41208
1b28c43a7074 make "debug" imply "blocking", since in blocking mode the exceptions flow through and are more instructive
blanchet
parents: 41180
diff changeset
   152
fun run_sledgehammer (params as {debug, blocking, provers, type_sys,
40069
6f7bf79b1506 fixed signature of "is_smt_solver_installed";
blanchet
parents: 40068
diff changeset
   153
                                 relevance_thresholds, max_relevant, ...})
39366
f58fbb959826 handle relevance filter corner cases more gracefully;
blanchet
parents: 39364
diff changeset
   154
                     auto i (relevance_override as {only, ...}) minimize_command
f58fbb959826 handle relevance filter corner cases more gracefully;
blanchet
parents: 39364
diff changeset
   155
                     state =
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39494
diff changeset
   156
  if null provers then
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39494
diff changeset
   157
    error "No prover is set."
39318
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 39263
diff changeset
   158
  else case subgoal_count state of
40132
7ee65dbffa31 renamed Output.priority to Output.urgent_message to emphasize its special role more clearly;
wenzelm
parents: 40114
diff changeset
   159
    0 => (Output.urgent_message "No subgoal!"; (false, state))
39318
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 39263
diff changeset
   160
  | n =>
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 39263
diff changeset
   161
    let
39364
61f0d36840c5 Sledgehammer should be called in "prove" mode;
blanchet
parents: 39338
diff changeset
   162
      val _ = Proof.assert_backward state
41242
8edeb1dbbc76 run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents: 41208
diff changeset
   163
      val state =
8edeb1dbbc76 run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents: 41208
diff changeset
   164
        state |> Proof.map_context (Config.put SMT_Config.verbose debug)
40200
870818d2b56b remove needless context argument;
blanchet
parents: 40190
diff changeset
   165
      val ctxt = Proof.context_of state
41242
8edeb1dbbc76 run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents: 41208
diff changeset
   166
      val thy = ProofContext.theory_of ctxt
40200
870818d2b56b remove needless context argument;
blanchet
parents: 40190
diff changeset
   167
      val {facts = chained_ths, goal, ...} = Proof.goal state
40060
5ef6747aa619 first step in adding support for an SMT backend to Sledgehammer
blanchet
parents: 40059
diff changeset
   168
      val (_, hyp_ts, concl_t) = strip_subgoal goal i
41138
eb80538166b6 implemented partially-typed "tags" type encoding
blanchet
parents: 41091
diff changeset
   169
      val no_dangerous_types = types_dangerous_types type_sys
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39494
diff changeset
   170
      val _ = () |> not blocking ? kill_provers
40941
a3e6f8634a11 replace "smt" prover with specific SMT solvers, e.g. "z3" -- whatever the SMT module gives us
blanchet
parents: 40723
diff changeset
   171
      val _ = case find_first (not o is_prover_available ctxt) provers of
a3e6f8634a11 replace "smt" prover with specific SMT solvers, e.g. "z3" -- whatever the SMT module gives us
blanchet
parents: 40723
diff changeset
   172
                SOME name => error ("No such prover: " ^ name ^ ".")
a3e6f8634a11 replace "smt" prover with specific SMT solvers, e.g. "z3" -- whatever the SMT module gives us
blanchet
parents: 40723
diff changeset
   173
              | NONE => ()
40132
7ee65dbffa31 renamed Output.priority to Output.urgent_message to emphasize its special role more clearly;
wenzelm
parents: 40114
diff changeset
   174
      val _ = if auto then () else Output.urgent_message "Sledgehammering..."
40941
a3e6f8634a11 replace "smt" prover with specific SMT solvers, e.g. "z3" -- whatever the SMT module gives us
blanchet
parents: 40723
diff changeset
   175
      val (smts, atps) = provers |> List.partition (is_smt_prover ctxt)
41242
8edeb1dbbc76 run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents: 41208
diff changeset
   176
      fun run_provers get_facts translate maybe_smt_head provers
8edeb1dbbc76 run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents: 41208
diff changeset
   177
                      (res as (success, state)) =
40065
1e4c7185f3f9 remove more needless code ("run_smt_solvers");
blanchet
parents: 40064
diff changeset
   178
        if success orelse null provers then
40060
5ef6747aa619 first step in adding support for an SMT backend to Sledgehammer
blanchet
parents: 40059
diff changeset
   179
          res
5ef6747aa619 first step in adding support for an SMT backend to Sledgehammer
blanchet
parents: 40059
diff changeset
   180
        else
5ef6747aa619 first step in adding support for an SMT backend to Sledgehammer
blanchet
parents: 40059
diff changeset
   181
          let
41242
8edeb1dbbc76 run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents: 41208
diff changeset
   182
            val facts = get_facts ()
8edeb1dbbc76 run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents: 41208
diff changeset
   183
            val num_facts = length facts
8edeb1dbbc76 run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents: 41208
diff changeset
   184
            val facts = facts ~~ (0 upto num_facts - 1)
8edeb1dbbc76 run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents: 41208
diff changeset
   185
                        |> map (translate num_facts)
40062
cfaebaa8588f make Sledgehammer minimizer fully work with SMT
blanchet
parents: 40061
diff changeset
   186
            val problem =
40065
1e4c7185f3f9 remove more needless code ("run_smt_solvers");
blanchet
parents: 40064
diff changeset
   187
              {state = state, goal = goal, subgoal = i, subgoal_count = n,
41242
8edeb1dbbc76 run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents: 41208
diff changeset
   188
               facts = facts,
8edeb1dbbc76 run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents: 41208
diff changeset
   189
               smt_head = maybe_smt_head (map smt_weighted_fact facts) i}
40983
07526f546680 handle "max_relevant" uniformly
blanchet
parents: 40982
diff changeset
   190
            val run_prover = run_prover params auto minimize_command only
40060
5ef6747aa619 first step in adding support for an SMT backend to Sledgehammer
blanchet
parents: 40059
diff changeset
   191
          in
5ef6747aa619 first step in adding support for an SMT backend to Sledgehammer
blanchet
parents: 40059
diff changeset
   192
            if auto then
40061
71cc5aac8b76 generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents: 40060
diff changeset
   193
              fold (fn prover => fn (true, state) => (true, state)
40064
db8413d82c3b got rid of duplicate functionality ("run_smt_solver_somehow");
blanchet
parents: 40063
diff changeset
   194
                                  | (false, _) => run_prover problem prover)
40065
1e4c7185f3f9 remove more needless code ("run_smt_solvers");
blanchet
parents: 40064
diff changeset
   195
                   provers (false, state)
40060
5ef6747aa619 first step in adding support for an SMT backend to Sledgehammer
blanchet
parents: 40059
diff changeset
   196
            else
41171
043f8dc3b51f facilitate debugging
blanchet
parents: 41142
diff changeset
   197
              provers
41242
8edeb1dbbc76 run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents: 41208
diff changeset
   198
              |> (if blocking then smart_par_list_map else map)
41171
043f8dc3b51f facilitate debugging
blanchet
parents: 41142
diff changeset
   199
                     (run_prover problem)
043f8dc3b51f facilitate debugging
blanchet
parents: 41142
diff changeset
   200
              |> exists fst |> rpair state
40060
5ef6747aa619 first step in adding support for an SMT backend to Sledgehammer
blanchet
parents: 40059
diff changeset
   201
          end
41242
8edeb1dbbc76 run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents: 41208
diff changeset
   202
      fun get_facts label no_dangerous_types relevance_fudge provers =
8edeb1dbbc76 run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents: 41208
diff changeset
   203
        let
8edeb1dbbc76 run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents: 41208
diff changeset
   204
          val max_max_relevant =
8edeb1dbbc76 run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents: 41208
diff changeset
   205
            case max_relevant of
8edeb1dbbc76 run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents: 41208
diff changeset
   206
              SOME n => n
8edeb1dbbc76 run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents: 41208
diff changeset
   207
            | NONE =>
8edeb1dbbc76 run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents: 41208
diff changeset
   208
              0 |> fold (Integer.max o default_max_relevant_for_prover ctxt)
8edeb1dbbc76 run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents: 41208
diff changeset
   209
                        provers
8edeb1dbbc76 run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents: 41208
diff changeset
   210
                |> auto ? (fn n => n div auto_max_relevant_divisor)
8edeb1dbbc76 run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents: 41208
diff changeset
   211
          val is_built_in_const =
8edeb1dbbc76 run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents: 41208
diff changeset
   212
            is_built_in_const_for_prover ctxt (hd provers)
8edeb1dbbc76 run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents: 41208
diff changeset
   213
        in
8edeb1dbbc76 run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents: 41208
diff changeset
   214
          relevant_facts ctxt no_dangerous_types relevance_thresholds
8edeb1dbbc76 run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents: 41208
diff changeset
   215
                         max_max_relevant is_built_in_const relevance_fudge
8edeb1dbbc76 run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents: 41208
diff changeset
   216
                         relevance_override chained_ths hyp_ts concl_t
8edeb1dbbc76 run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents: 41208
diff changeset
   217
          |> tap (fn facts =>
8edeb1dbbc76 run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents: 41208
diff changeset
   218
                     if debug then
8edeb1dbbc76 run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents: 41208
diff changeset
   219
                       label ^ plural_s (length provers) ^ ": " ^
8edeb1dbbc76 run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents: 41208
diff changeset
   220
                       (if null facts then
8edeb1dbbc76 run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents: 41208
diff changeset
   221
                          "Found no relevant facts."
8edeb1dbbc76 run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents: 41208
diff changeset
   222
                        else
8edeb1dbbc76 run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents: 41208
diff changeset
   223
                          "Including (up to) " ^ string_of_int (length facts) ^
8edeb1dbbc76 run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents: 41208
diff changeset
   224
                          " relevant fact" ^ plural_s (length facts) ^ ":\n" ^
8edeb1dbbc76 run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents: 41208
diff changeset
   225
                          (facts |> map (fst o fst) |> space_implode " ") ^ ".")
8edeb1dbbc76 run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents: 41208
diff changeset
   226
                       |> Output.urgent_message
8edeb1dbbc76 run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents: 41208
diff changeset
   227
                     else
8edeb1dbbc76 run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents: 41208
diff changeset
   228
                       ())
8edeb1dbbc76 run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents: 41208
diff changeset
   229
        end
40071
658a37c80b53 generalized the relevance filter so that it takes the list of "irrelevant constants" as argument (since the ATP and SMT preprocessing are different)
blanchet
parents: 40070
diff changeset
   230
      val run_atps =
41242
8edeb1dbbc76 run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents: 41208
diff changeset
   231
        run_provers
8edeb1dbbc76 run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents: 41208
diff changeset
   232
            (get_facts "ATP" no_dangerous_types atp_relevance_fudge o K atps)
8edeb1dbbc76 run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents: 41208
diff changeset
   233
            (ATP_Translated_Fact oo K (translate_atp_fact ctxt o fst))
8edeb1dbbc76 run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents: 41208
diff changeset
   234
            (K (K NONE)) atps
8edeb1dbbc76 run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents: 41208
diff changeset
   235
      fun run_smts (accum as (success, _)) =
8edeb1dbbc76 run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents: 41208
diff changeset
   236
        if success orelse null smts then
8edeb1dbbc76 run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents: 41208
diff changeset
   237
          accum
8edeb1dbbc76 run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents: 41208
diff changeset
   238
        else
8edeb1dbbc76 run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents: 41208
diff changeset
   239
          let
8edeb1dbbc76 run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents: 41208
diff changeset
   240
            val facts = get_facts "SMT solver" true smt_relevance_fudge smts
8edeb1dbbc76 run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents: 41208
diff changeset
   241
            val translate = SMT_Weighted_Fact oo weight_smt_fact thy
8edeb1dbbc76 run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents: 41208
diff changeset
   242
            val maybe_smt_head = try o SMT_Solver.smt_filter_head state
8edeb1dbbc76 run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents: 41208
diff changeset
   243
          in
8edeb1dbbc76 run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents: 41208
diff changeset
   244
            smts |> map (`(class_of_smt_solver ctxt))
8edeb1dbbc76 run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents: 41208
diff changeset
   245
                 |> AList.group (op =)
8edeb1dbbc76 run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents: 41208
diff changeset
   246
                 |> map (fn (_, smts) => run_provers (K facts) translate
8edeb1dbbc76 run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents: 41208
diff changeset
   247
                                                     maybe_smt_head smts accum)
8edeb1dbbc76 run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents: 41208
diff changeset
   248
                 |> exists fst |> rpair state
8edeb1dbbc76 run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents: 41208
diff changeset
   249
          end
40060
5ef6747aa619 first step in adding support for an SMT backend to Sledgehammer
blanchet
parents: 40059
diff changeset
   250
      fun run_atps_and_smt_solvers () =
41242
8edeb1dbbc76 run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents: 41208
diff changeset
   251
        [run_atps, run_smts]
8edeb1dbbc76 run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents: 41208
diff changeset
   252
        |> smart_par_list_map (fn f => f (false, state) |> K ())
41180
a99bc6f3664b make sure errors generated in a thread don't vanish in cyberspace (e.g., when invoking Sledgehammer with unknown facts)
blanchet
parents: 41171
diff changeset
   253
        handle ERROR msg => (Output.urgent_message ("Error: " ^ msg); error msg)
40060
5ef6747aa619 first step in adding support for an SMT backend to Sledgehammer
blanchet
parents: 40059
diff changeset
   254
    in
40065
1e4c7185f3f9 remove more needless code ("run_smt_solvers");
blanchet
parents: 40064
diff changeset
   255
      (false, state)
1e4c7185f3f9 remove more needless code ("run_smt_solvers");
blanchet
parents: 40064
diff changeset
   256
      |> (if blocking then run_atps #> not auto ? run_smts
1e4c7185f3f9 remove more needless code ("run_smt_solvers");
blanchet
parents: 40064
diff changeset
   257
          else (fn p => Future.fork (tap run_atps_and_smt_solvers) |> K p))
40060
5ef6747aa619 first step in adding support for an SMT backend to Sledgehammer
blanchet
parents: 40059
diff changeset
   258
    end
38044
463177795c49 minor refactoring
blanchet
parents: 38040
diff changeset
   259
28582
c269a3045fdf info: back to plain printing;
wenzelm
parents: 28571
diff changeset
   260
end;