# HG changeset patch
# User blanchet
# Date 1283165040 -7200
# Node ID 853a061af37dbc2b6d98cd198e59a2c5a3bb9202
# Parent  55391ee96614c38fdd1295d32963779f3a9f7004
allow configuration of fact filter fudge factors

diff -r 55391ee96614 -r 853a061af37d src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML	Mon Aug 30 12:21:53 2010 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML	Mon Aug 30 12:44:00 2010 +0200
@@ -116,10 +116,26 @@
 
 val proof_fileK = "proof_file"
 
+val relevance_filter_args =
+  [("abs_rel_weight", Sledgehammer_Fact_Filter.abs_rel_weight),
+   ("abs_irrel_weight", Sledgehammer_Fact_Filter.abs_irrel_weight),
+   ("skolem_irrel_weight", Sledgehammer_Fact_Filter.skolem_irrel_weight),
+   ("theory_bonus", Sledgehammer_Fact_Filter.theory_bonus),
+   ("local_bonus", Sledgehammer_Fact_Filter.local_bonus),
+   ("chained_bonus", Sledgehammer_Fact_Filter.chained_bonus),
+   ("threshold_divisor", Sledgehammer_Fact_Filter.threshold_divisor),
+   ("ridiculous_threshold", Sledgehammer_Fact_Filter.ridiculous_threshold),
+   ("max_max_imperfect_fudge_factor",
+    Sledgehammer_Fact_Filter.max_max_imperfect_fudge_factor)]
+
 fun invoke args =
   let
     val (pf_args, other_args) =
       args |> List.partition (curry (op =) proof_fileK o fst)
+      ||> filter (fn (key, value) =>
+                      case AList.lookup (op =) relevance_filter_args key of
+                        SOME rf => (rf := the (Real.fromString value); false)
+                      | NONE => true)
     val proof_file = case pf_args of
                        [] => error "No \"proof_file\" specified"
                      | (_, s) :: _ => s