src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML
changeset 55212 5832470d956e
parent 55211 5d027af93a08
child 55285 e88ad20035f4
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML	Fri Jan 31 16:07:20 2014 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML	Fri Jan 31 16:10:39 2014 +0100
     1.3 @@ -25,18 +25,15 @@
     1.4    val smt_slice_time_frac : real Config.T
     1.5    val smt_slice_min_secs : int Config.T
     1.6  
     1.7 -  val select_smt_solver : string -> Proof.context -> Proof.context
     1.8    val is_smt_prover : Proof.context -> string -> bool
     1.9 -  val weight_smt_fact : Proof.context -> int -> ((string * stature) * thm) * int
    1.10 -    -> (string * stature) * (int option * thm)
    1.11    val run_smt_solver : mode -> string -> prover
    1.12  end;
    1.13  
    1.14  structure Sledgehammer_Prover_SMT : SLEDGEHAMMER_PROVER_SMT =
    1.15  struct
    1.16  
    1.17 +open ATP_Util
    1.18  open ATP_Proof
    1.19 -open ATP_Util
    1.20  open ATP_Systems
    1.21  open ATP_Problem_Generate
    1.22  open ATP_Proof_Reconstruct
    1.23 @@ -50,30 +47,24 @@
    1.24  val smt_weight_min_facts =
    1.25    Attrib.setup_config_int @{binding sledgehammer_smt_weight_min_facts} (K 20)
    1.26  
    1.27 -val select_smt_solver = Context.proof_map o SMT_Config.select_solver
    1.28 -
    1.29  fun is_smt_prover ctxt = member (op =) (SMT_Solver.available_solvers_of ctxt)
    1.30  
    1.31  (* FUDGE *)
    1.32 -val smt_min_weight =
    1.33 -  Attrib.setup_config_int @{binding sledgehammer_smt_min_weight} (K 0)
    1.34 -val smt_max_weight =
    1.35 -  Attrib.setup_config_int @{binding sledgehammer_smt_max_weight} (K 10)
    1.36 +val smt_min_weight = Attrib.setup_config_int @{binding sledgehammer_smt_min_weight} (K 0)
    1.37 +val smt_max_weight = Attrib.setup_config_int @{binding sledgehammer_smt_max_weight} (K 10)
    1.38  val smt_max_weight_index =
    1.39    Attrib.setup_config_int @{binding sledgehammer_smt_max_weight_index} (K 200)
    1.40  val smt_weight_curve = Unsynchronized.ref (fn x : int => x * x)
    1.41  
    1.42  fun smt_fact_weight ctxt j num_facts =
    1.43 -  if Config.get ctxt smt_weights andalso
    1.44 -     num_facts >= Config.get ctxt smt_weight_min_facts then
    1.45 +  if Config.get ctxt smt_weights andalso num_facts >= Config.get ctxt smt_weight_min_facts then
    1.46      let
    1.47        val min = Config.get ctxt smt_min_weight
    1.48        val max = Config.get ctxt smt_max_weight
    1.49        val max_index = Config.get ctxt smt_max_weight_index
    1.50        val curve = !smt_weight_curve
    1.51      in
    1.52 -      SOME (max - (max - min + 1) * curve (Int.max (0, max_index - j - 1))
    1.53 -            div curve max_index)
    1.54 +      SOME (max - (max - min + 1) * curve (Int.max (0, max_index - j - 1)) div curve max_index)
    1.55      end
    1.56    else
    1.57      NONE
    1.58 @@ -120,7 +111,7 @@
    1.59        ...} : params) state goal i =
    1.60    let
    1.61      fun repair_context ctxt =
    1.62 -      ctxt |> select_smt_solver name
    1.63 +      ctxt |> Context.proof_map (SMT_Config.select_solver name)
    1.64             |> Config.put SMT_Config.verbose debug
    1.65             |> (if overlord then
    1.66                   Config.put SMT_Config.debug_files
    1.67 @@ -139,7 +130,7 @@
    1.68      val max_slices = if slice then Config.get ctxt smt_max_slices else 1
    1.69  
    1.70      fun do_slice timeout slice outcome0 time_so_far
    1.71 -                 (weighted_factss as (fact_filter, weighted_facts) :: _) =
    1.72 +        (weighted_factss as (fact_filter, weighted_facts) :: _) =
    1.73        let
    1.74          val timer = Timer.startRealTimer ()
    1.75          val slice_timeout =
    1.76 @@ -259,9 +250,8 @@
    1.77        | SOME failure =>
    1.78          (Lazy.value (plain_metis, Play_Failed), fn _ => string_of_atp_failure failure, ""))
    1.79    in
    1.80 -    {outcome = outcome, used_facts = used_facts, used_from = used_from,
    1.81 -     run_time = run_time, preplay = preplay, message = message,
    1.82 -     message_tail = message_tail}
    1.83 +    {outcome = outcome, used_facts = used_facts, used_from = used_from, run_time = run_time,
    1.84 +     preplay = preplay, message = message, message_tail = message_tail}
    1.85    end
    1.86  
    1.87  end;