src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML
changeset 38751 01c4d14b2a61
parent 38749 0d2f7f0614d1
child 38752 6628adcae4a7
equal deleted inserted replaced
38750:e752ce159903 38751:01c4d14b2a61
   253   else irrel_log (pseudoconst_freq (match_pseudotypes o swap) const_tab c)
   253   else irrel_log (pseudoconst_freq (match_pseudotypes o swap) const_tab c)
   254 (* TODO: experiment
   254 (* TODO: experiment
   255 fun irrel_weight _ _ = 1.0
   255 fun irrel_weight _ _ = 1.0
   256 *)
   256 *)
   257 
   257 
   258 fun axiom_weight const_tab relevant_consts axiom_consts =
   258 val chained_bonus_factor = 2.0
       
   259 
       
   260 fun axiom_weight chained const_tab relevant_consts axiom_consts =
   259   case axiom_consts |> List.partition (pseudoconst_mem I relevant_consts)
   261   case axiom_consts |> List.partition (pseudoconst_mem I relevant_consts)
   260                     ||> filter_out (pseudoconst_mem swap relevant_consts) of
   262                     ||> filter_out (pseudoconst_mem swap relevant_consts) of
   261     ([], []) => 0.0
   263     ([], []) => 0.0
   262   | (_, []) => 1.0
   264   | (_, []) => 1.0
   263   | (rel, irrel) =>
   265   | (rel, irrel) =>
   264     let
   266     let
   265       val rel_weight = fold (curry Real.+ o rel_weight const_tab) rel 0.0
   267       val rel_weight = fold (curry Real.+ o rel_weight const_tab) rel 0.0
       
   268                        |> chained ? curry Real.* chained_bonus_factor
   266       val irrel_weight = fold (curry Real.+ o irrel_weight const_tab) irrel 0.0
   269       val irrel_weight = fold (curry Real.+ o irrel_weight const_tab) irrel 0.0
   267       val res = rel_weight / (rel_weight + irrel_weight)
   270       val res = rel_weight / (rel_weight + irrel_weight)
   268     in if Real.isFinite res then res else 0.0 end
   271     in if Real.isFinite res then res else 0.0 end
   269 
   272 
   270 (* TODO: experiment
   273 (* TODO: experiment
   393                       :: hopeful) =
   396                       :: hopeful) =
   394             let
   397             let
   395               val weight =
   398               val weight =
   396                 case cached_weight of
   399                 case cached_weight of
   397                   SOME w => w
   400                   SOME w => w
   398                 | NONE => axiom_weight const_tab rel_const_tab axiom_consts
   401                 | NONE => axiom_weight (snd (name ())) const_tab rel_const_tab
       
   402                                        axiom_consts
   399 (* TODO: experiment
   403 (* TODO: experiment
   400 val _ = if String.isPrefix "lift.simps(3" (fst (name ())) then
   404 val _ = if String.isPrefix "lift.simps(3" (fst (name ())) then
   401 tracing ("*** " ^ (fst (name ())) ^ PolyML.makestring (debug_axiom_weight const_tab rel_const_tab axiom_consts))
   405 tracing ("*** " ^ (fst (name ())) ^ PolyML.makestring (debug_axiom_weight const_tab rel_const_tab axiom_consts))
   402 else
   406 else
   403 ()
   407 ()