src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
changeset 41313 a96ac4d180b7
parent 41259 13972ced98d9
child 41315 7f6baec2b27a
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Mon Dec 20 08:55:36 2010 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Mon Dec 20 12:12:35 2010 +0100
     1.3 @@ -53,6 +53,7 @@
     1.4    type prover = params -> minimize_command -> prover_problem -> prover_result
     1.5  
     1.6    (* for experimentation purposes -- do not use in production code *)
     1.7 +  val atp_first_iter_time_frac : real Unsynchronized.ref
     1.8    val smt_weights : bool Unsynchronized.ref
     1.9    val smt_weight_min_facts : int Unsynchronized.ref
    1.10    val smt_min_weight : int Unsynchronized.ref
    1.11 @@ -318,15 +319,16 @@
    1.12    | smt_weighted_fact thy num_facts (fact, j) =
    1.13      (untranslated_fact fact, j) |> weight_smt_fact thy num_facts
    1.14  
    1.15 +fun overlord_file_location_for_prover prover =
    1.16 +  (getenv "ISABELLE_HOME_USER", "prob_" ^ prover)
    1.17 +
    1.18 +
    1.19  (* generic TPTP-based ATPs *)
    1.20  
    1.21  fun int_opt_add (SOME m) (SOME n) = SOME (m + n)
    1.22    | int_opt_add _ _ = NONE
    1.23  
    1.24 -fun overlord_file_location_for_prover prover =
    1.25 -  (getenv "ISABELLE_HOME_USER", "prob_" ^ prover)
    1.26 -
    1.27 -val atp_first_iter_time_frac = 0.67
    1.28 +val atp_first_iter_time_frac = Unsynchronized.ref 0.67
    1.29  
    1.30  (* Important messages are important but not so important that users want to see
    1.31     them each time. *)
    1.32 @@ -358,15 +360,7 @@
    1.33          error ("No such directory: " ^ quote dest_dir ^ ".")
    1.34      val measure_run_time = verbose orelse Config.get ctxt measure_run_time
    1.35      val command = Path.explode (getenv (fst exec) ^ "/" ^ snd exec)
    1.36 -    (* write out problem file and call ATP *)
    1.37 -    fun command_line complete timeout probfile =
    1.38 -      let
    1.39 -        val core = File.shell_path command ^ " " ^ arguments complete timeout ^
    1.40 -                   " " ^ File.shell_path probfile
    1.41 -      in
    1.42 -        (if measure_run_time then "TIMEFORMAT='%3R'; { time " ^ core ^ " ; }"
    1.43 -         else "exec " ^ core) ^ " 2>&1"
    1.44 -      end
    1.45 +val command = Path.explode ("/Users/blanchet/misc/E-weights/PROVER/" ^ snd exec) (*###*)
    1.46      fun split_time s =
    1.47        let
    1.48          val split = String.tokens (fn c => str c = "\n");
    1.49 @@ -378,16 +372,35 @@
    1.50          val time = num --| Scan.$$ "." -- num3 >> (fn (a, b) => a * 1000 + b);
    1.51          val as_time = Scan.read Symbol.stopper time o raw_explode
    1.52        in (output, as_time t) end;
    1.53 -    fun run_on probfile =
    1.54 +    fun run_on prob_file =
    1.55        case filter (curry (op =) "" o getenv o fst) (exec :: required_execs) of
    1.56          (home_var, _) :: _ =>
    1.57          error ("The environment variable " ^ quote home_var ^ " is not set.")
    1.58        | [] =>
    1.59          if File.exists command then
    1.60            let
    1.61 +            val readable_names = debug andalso overlord
    1.62 +            val (atp_problem, pool, conjecture_offset, fact_names) =
    1.63 +              prepare_atp_problem ctxt readable_names explicit_forall type_sys
    1.64 +                                  explicit_apply hyp_ts concl_t facts
    1.65 +            val ss = tptp_strings_for_atp_problem use_conjecture_for_hypotheses
    1.66 +                                                  atp_problem
    1.67 +            val _ = File.write_list prob_file ss
    1.68 +            val conjecture_shape =
    1.69 +              conjecture_offset + 1 upto conjecture_offset + length hyp_ts + 1
    1.70 +              |> map single
    1.71              fun run complete timeout =
    1.72                let
    1.73 -                val command = command_line complete timeout probfile
    1.74 +                fun weights () = atp_problem_weights atp_problem
    1.75 +                val core =
    1.76 +                  File.shell_path command ^ " " ^
    1.77 +                  arguments complete timeout weights ^ " " ^
    1.78 +                  File.shell_path prob_file
    1.79 +                val command =
    1.80 +                  (if measure_run_time then
    1.81 +                     "TIMEFORMAT='%3R'; { time " ^ core ^ " ; }"
    1.82 +                   else
    1.83 +                     "exec " ^ core) ^ " 2>&1"
    1.84                  val ((output, msecs), res_code) =
    1.85                    bash_output command
    1.86                    |>> (if overlord then
    1.87 @@ -399,22 +412,12 @@
    1.88                    extract_tstplike_proof_and_outcome verbose complete res_code
    1.89                        proof_delims known_failures output
    1.90                in (output, msecs, tstplike_proof, outcome) end
    1.91 -            val readable_names = debug andalso overlord
    1.92 -            val (atp_problem, pool, conjecture_offset, fact_names) =
    1.93 -              prepare_atp_problem ctxt readable_names explicit_forall type_sys
    1.94 -                                  explicit_apply hyp_ts concl_t facts
    1.95 -            val ss = tptp_strings_for_atp_problem use_conjecture_for_hypotheses
    1.96 -                                                  atp_problem
    1.97 -            val _ = File.write_list probfile ss
    1.98 -            val conjecture_shape =
    1.99 -              conjecture_offset + 1 upto conjecture_offset + length hyp_ts + 1
   1.100 -              |> map single
   1.101              val run_twice = has_incomplete_mode andalso not auto
   1.102              val timer = Timer.startRealTimer ()
   1.103              val result =
   1.104                run false
   1.105                   (if run_twice then
   1.106 -                    seconds (0.001 * atp_first_iter_time_frac
   1.107 +                    seconds (0.001 * !atp_first_iter_time_frac
   1.108                               * Real.fromInt (Time.toMilliseconds timeout))
   1.109                    else
   1.110                      timeout)
   1.111 @@ -431,13 +434,13 @@
   1.112  
   1.113      (* If the problem file has not been exported, remove it; otherwise, export
   1.114         the proof file too. *)
   1.115 -    fun cleanup probfile =
   1.116 -      if dest_dir = "" then try File.rm probfile else NONE
   1.117 -    fun export probfile (_, (output, _, _, _)) =
   1.118 +    fun cleanup prob_file =
   1.119 +      if dest_dir = "" then try File.rm prob_file else NONE
   1.120 +    fun export prob_file (_, (output, _, _, _)) =
   1.121        if dest_dir = "" then
   1.122          ()
   1.123        else
   1.124 -        File.write (Path.explode (Path.implode probfile ^ "_proof")) output
   1.125 +        File.write (Path.explode (Path.implode prob_file ^ "_proof")) output
   1.126      val ((pool, conjecture_shape, fact_names),
   1.127           (output, msecs, tstplike_proof, outcome)) =
   1.128        with_path cleanup export run_on problem_path_name