# HG changeset patch
# User blanchet
# Date 1292411321 -3600
# Node ID 1e12d6495423695bc80bc06ad524c7c737d154f9
# Parent  8c9c31a757f5a58e2ca62d4cdb072b41cf6f6dfe
honor "overlord" option for SMT solvers as well and don't pass "ext" to them

diff -r 8c9c31a757f5 -r 1e12d6495423 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML	Wed Dec 15 11:26:29 2010 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML	Wed Dec 15 12:08:41 2010 +0100
@@ -11,12 +11,13 @@
   | NONE => default_value
 
 fun extract_relevance_fudge args
-      {worse_irrel_freq, higher_order_irrel_weight, abs_rel_weight,
+      {allow_ext, worse_irrel_freq, higher_order_irrel_weight, abs_rel_weight,
        abs_irrel_weight, skolem_irrel_weight, theory_const_rel_weight,
        theory_const_irrel_weight, intro_bonus, elim_bonus, simp_bonus,
        local_bonus, assum_bonus, chained_bonus, max_imperfect,
        max_imperfect_exp, threshold_divisor, ridiculous_threshold} =
-  {worse_irrel_freq = get args "worse_irrel_freq" worse_irrel_freq,
+  {allow_ext = allow_ext,
+   worse_irrel_freq = get args "worse_irrel_freq" worse_irrel_freq,
    higher_order_irrel_weight =
        get args "higher_order_irrel_weight" higher_order_irrel_weight,
    abs_rel_weight = get args "abs_rel_weight" abs_rel_weight,
diff -r 8c9c31a757f5 -r 1e12d6495423 src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Wed Dec 15 11:26:29 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Wed Dec 15 12:08:41 2010 +0100
@@ -10,7 +10,8 @@
   datatype locality = General | Intro | Elim | Simp | Local | Assum | Chained
 
   type relevance_fudge =
-    {worse_irrel_freq : real,
+    {allow_ext : bool,
+     worse_irrel_freq : real,
      higher_order_irrel_weight : real,
      abs_rel_weight : real,
      abs_irrel_weight : real,
@@ -59,7 +60,8 @@
 datatype locality = General | Intro | Elim | Simp | Local | Assum | Chained
 
 type relevance_fudge =
-  {worse_irrel_freq : real,
+  {allow_ext : bool,
+   worse_irrel_freq : real,
    higher_order_irrel_weight : real,
    abs_rel_weight : real,
    abs_irrel_weight : real,
diff -r 8c9c31a757f5 -r 1e12d6495423 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Wed Dec 15 11:26:29 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Wed Dec 15 12:08:41 2010 +0100
@@ -140,7 +140,8 @@
 
 (* FUDGE *)
 val atp_relevance_fudge =
-  {worse_irrel_freq = 100.0,
+  {allow_ext = true,
+   worse_irrel_freq = 100.0,
    higher_order_irrel_weight = 1.05,
    abs_rel_weight = 0.5,
    abs_irrel_weight = 2.0,
@@ -160,7 +161,8 @@
 
 (* FUDGE (FIXME) *)
 val smt_relevance_fudge =
-  {worse_irrel_freq = #worse_irrel_freq atp_relevance_fudge,
+  {allow_ext = false,
+   worse_irrel_freq = #worse_irrel_freq atp_relevance_fudge,
    higher_order_irrel_weight = #higher_order_irrel_weight atp_relevance_fudge,
    abs_rel_weight = #abs_rel_weight atp_relevance_fudge,
    abs_irrel_weight = #abs_irrel_weight atp_relevance_fudge,
@@ -264,11 +266,14 @@
 fun int_opt_add (SOME m) (SOME n) = SOME (m + n)
   | int_opt_add _ _ = NONE
 
+fun overlord_file_location_for_prover prover =
+  (getenv "ISABELLE_HOME_USER", "prob_" ^ prover)
+
 (* Important messages are important but not so important that users want to see
    them each time. *)
 val important_message_keep_factor = 0.1
 
-fun run_atp auto atp_name
+fun run_atp auto name
         ({exec, required_execs, arguments, has_incomplete_mode, proof_delims,
           known_failures, explicit_forall, use_conjecture_for_hypotheses, ...}
           : atp_config)
@@ -279,13 +284,12 @@
     val ctxt = Proof.context_of state
     val (_, hyp_ts, concl_t) = strip_subgoal goal subgoal
     val facts = facts |> map (atp_translated_fact ctxt)
-    val dest_dir = if overlord then getenv "ISABELLE_HOME_USER"
-                   else Config.get ctxt dest_dir
-    val problem_prefix = Config.get ctxt problem_prefix
+    val (dest_dir, problem_prefix) =
+      if overlord then overlord_file_location_for_prover name
+      else (Config.get ctxt dest_dir, Config.get ctxt problem_prefix)
     val problem_file_name =
-      Path.basic ((if overlord then "prob_" ^ atp_name
-                   else problem_prefix ^ serial_string ())
-                  ^ "_" ^ string_of_int subgoal)
+      Path.basic (problem_prefix ^ (if overlord then "" else serial_string ()) ^
+                  "_" ^ string_of_int subgoal)
     val problem_path_name =
       if dest_dir = "" then
         File.tmp_path problem_file_name
@@ -518,7 +522,7 @@
             (Config.put Metis_Tactics.verbose debug
              #> (fn ctxt => Metis_Tactics.metis_tac ctxt ths)) state i
 
-fun run_smt_solver auto name (params as {debug, ...}) minimize_command
+fun run_smt_solver auto name (params as {debug, overlord, ...}) minimize_command
         ({state, subgoal, subgoal_count, facts, ...} : prover_problem) =
   let
     val (remote, suffix) =
@@ -528,6 +532,12 @@
     val repair_context =
       Context.proof_map (SMT_Config.select_solver suffix)
       #> Config.put SMT_Config.verbose debug
+      #> (if overlord then
+            Config.put SMT_Config.debug_files
+                       (overlord_file_location_for_prover name
+                        |> (fn (path, base) => path ^ "/" ^ base))
+          else
+            I)
       #> Config.put SMT_Config.monomorph_limit smt_monomorph_limit
     val state = state |> Proof.map_context repair_context
     val thy = Proof.theory_of state