# HG changeset patch # User blanchet # Date 1677654051 -3600 # Node ID 4e8a6354c54f55baa5fcd17e4a21592e7eb714b0 # Parent f6cb40234009d76008284a7f67a4ee750c481b29 improve ad hoc abduction in Sledgehammer diff -r f6cb40234009 -r 4e8a6354c54f src/HOL/Tools/ATP/atp_proof_reconstruct.ML --- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Wed Mar 01 08:00:51 2023 +0100 +++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Wed Mar 01 08:00:51 2023 +0100 @@ -805,30 +805,47 @@ [] else let - fun split_min seen [] (_, best_item) = (best_item, List.rev seen) - | split_min seen ((score, item) :: scored_items) (best_score, best_item) = + fun split_min accum [] (_, best_item) = (best_item, List.rev accum) + | split_min accum ((score, item) :: scored_items) (best_score, best_item) = if score < best_score then - split_min ((best_score, best_item) :: seen) scored_items (score, item) + split_min ((best_score, best_item) :: accum) scored_items (score, item) else - split_min ((score, item) :: seen) scored_items (best_score, best_item) + split_min ((score, item) :: accum) scored_items (best_score, best_item) val (min_item, other_scored_items) = split_min [] (tl scored_items) (hd scored_items) in min_item :: sort_top (n - 1) (filter_out (equal min_item o snd) other_scored_items) + |> distinct (op aconv) end fun top_abduce_candidates max_candidates candidates = let + (* We prefer free variables to other constructs, so that e.g. "x \ y" is + prioritized over "x \ 0". *) fun score t = - size_of_term t + - (if exists_subterm (fn Bound _ => true | Var _ => true | _ => false) t then 50 else 0) + - (if exists_subterm (fn Free _ => true | _ => false) t then ~10 else 0) + Term.fold_aterms (fn t => fn score => score + (case t of Free _ => ~1 | _ => 4)) t 0 + (* Equations of the form "x = ..." or "... = x" or similar are too specific + to be useful. Quantified formulas are also filtered out. As for "True", + it may seem an odd choice for abduction, but it sometimes arises in + conjunction with type class constraints, which are removed by the + termifier. *) fun maybe_score t = (case t of - @{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ Free _ $ _) => NONE + @{prop True} => NONE + | @{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ Free _ $ _) => NONE | @{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ _ $ Free _) => NONE + | @{const Trueprop} $ (@{const less(nat)} $ _ $ @{const zero_class.zero(nat)}) => NONE + | @{const Trueprop} $ (@{const less_eq(nat)} $ _ $ @{const zero_class.zero(nat)}) => NONE + | @{const Trueprop} $ (@{const less(nat)} $ _ $ @{const one_class.one(nat)}) => NONE + | @{const Trueprop} $ (@{const Not} $ + (@{const less(nat)} $ @{const zero_class.zero(nat)} $ _)) => NONE + | @{const Trueprop} $ (@{const Not} $ + (@{const less_eq(nat)} $ @{const zero_class.zero(nat)} $ _)) => NONE + | @{const Trueprop} $ (@{const Not} $ + (@{const less(nat)} $ @{const one_class.one(nat)} $ _)) => NONE | @{const Trueprop} $ (Const (@{const_name All}, _) $ _) => NONE + | @{const Trueprop} $ (Const (@{const_name Ex}, _) $ _) => NONE | _ => SOME (score t, t)) in sort_top max_candidates (map_filter maybe_score candidates)