# HG changeset patch # User blanchet # Date 1401788587 -7200 # Node ID 7b1bf424ec5fca5f73418893cf4997645c584b6f # Parent eb5f27ec3987853c5d8d8719d87f00ed3b669351 removed SMT weights -- their impact was very inconclusive anyway diff -r eb5f27ec3987 -r 7b1bf424ec5f src/HOL/SMT2.thy --- a/src/HOL/SMT2.thy Tue Jun 03 10:35:51 2014 +0200 +++ b/src/HOL/SMT2.thy Tue Jun 03 11:43:07 2014 +0200 @@ -40,32 +40,6 @@ definition trigger :: "pattern list list \ bool \ bool" where "trigger _ P = P" -subsection {* Quantifier weights *} - -text {* -Weight annotations to quantifiers influence the priority of quantifier -instantiations. They should be handled with care for solvers, which support -them, because incorrect choices of weights might render a problem unsolvable. -*} - -definition weight :: "int \ bool \ bool" where "weight _ P = P" - -text {* -Weights must be nonnegative. The value @{text 0} is equivalent to providing -no weight at all. - -Weights should only be used at quantifiers and only inside triggers (if the -quantifier has triggers). Valid usages of weights are as follows: - -\begin{itemize} -\item -@{term "\x. trigger [[pat (P x)]] (weight 2 (P x))"} -\item -@{term "\x. weight 3 (P x)"} -\end{itemize} -*} - - subsection {* Higher-order encoding *} text {* @@ -430,6 +404,6 @@ hide_type (open) pattern hide_const fun_app z3div z3mod -hide_const (open) trigger pat nopat weight +hide_const (open) trigger pat nopat end diff -r eb5f27ec3987 -r 7b1bf424ec5f src/HOL/SMT_Examples/SMT_Tests.thy --- a/src/HOL/SMT_Examples/SMT_Tests.thy Tue Jun 03 10:35:51 2014 +0200 +++ b/src/HOL/SMT_Examples/SMT_Tests.thy Tue Jun 03 11:43:07 2014 +0200 @@ -184,7 +184,7 @@ by smt2+ -section {* Guidance for quantifier heuristics: patterns and weights *} +section {* Guidance for quantifier heuristics: patterns *} lemma assumes "\x. SMT2.trigger [[SMT2.pat (f x)]] (f x = x)" @@ -216,18 +216,6 @@ shows "R t" using assms by smt2 -lemma - assumes "ALL x. SMT2.trigger [[SMT2.pat (P x)]] (SMT2.weight 2 (P x --> Q x))" - and "P t" - shows "Q t" - using assms by smt2 - -lemma - assumes "ALL x. SMT2.weight 1 (P x --> Q x)" - and "P t" - shows "Q t" - using assms by smt2 - section {* Meta-logical connectives *} diff -r eb5f27ec3987 -r 7b1bf424ec5f src/HOL/Tools/SMT2/smt2_normalize.ML --- a/src/HOL/Tools/SMT2/smt2_normalize.ML Tue Jun 03 10:35:51 2014 +0200 +++ b/src/HOL/Tools/SMT2/smt2_normalize.ML Tue Jun 03 11:43:07 2014 +0200 @@ -15,7 +15,7 @@ type extra_norm = Proof.context -> thm list * thm list -> thm list * thm list val add_extra_norm: SMT2_Util.class * extra_norm -> Context.generic -> Context.generic - val normalize: Proof.context -> (int option * thm) list -> (int * thm) list + val normalize: Proof.context -> thm list -> (int * thm) list end structure SMT2_Normalize: SMT2_NORMALIZE = @@ -239,79 +239,25 @@ end -(** adding quantifier weights **) - -local - (*** check weight syntax ***) - - val has_no_weight = - not o Term.exists_subterm (fn @{const SMT2.weight} => true | _ => false) - - fun is_weight (@{const SMT2.weight} $ w $ t) = - (case try HOLogic.dest_number w of - SOME (_, i) => i >= 0 andalso has_no_weight t - | _ => false) - | is_weight t = has_no_weight t - - fun proper_trigger (@{const SMT2.trigger} $ _ $ t) = is_weight t - | proper_trigger t = is_weight t - - fun check_weight_error ctxt t = - error ("SMT weight must be a non-negative number and must only occur " ^ - "under the top-most quantifier and an optional trigger: " ^ - Syntax.string_of_term ctxt t) - - fun check_weight_conv ctxt ct = - if SMT2_Util.under_quant proper_trigger (SMT2_Util.term_of ct) then Conv.all_conv ct - else check_weight_error ctxt (Thm.term_of ct) - - - (*** insertion of weights ***) - - fun under_trigger_conv cv ct = - (case Thm.term_of ct of - @{const SMT2.trigger} $ _ $ _ => Conv.arg_conv cv - | _ => cv) ct - - val weight_eq = mk_meta_eq @{lemma "p = SMT2.weight i p" by (simp add: weight_def)} - fun mk_weight_eq w = - let val cv = Thm.dest_arg1 (Thm.rhs_of weight_eq) - in Thm.instantiate ([], [(cv, Numeral.mk_cnumber @{ctyp int} w)]) weight_eq end - - fun add_weight_conv NONE _ = Conv.all_conv - | add_weight_conv (SOME weight) ctxt = - let val cv = Conv.rewr_conv (mk_weight_eq weight) - in SMT2_Util.under_quant_conv (K (under_trigger_conv cv)) ctxt end -in - -fun weight_conv weight ctxt = - SMT2_Util.prop_conv (check_weight_conv ctxt then_conv add_weight_conv weight ctxt) - -val setup_weight = SMT2_Builtin.add_builtin_fun_ext'' @{const_name SMT2.weight} - -end - - (** combined general normalizations **) -fun gen_normalize1_conv ctxt weight = +fun gen_normalize1_conv ctxt = atomize_conv ctxt then_conv unfold_special_quants_conv ctxt then_conv Thm.beta_conversion true then_conv - trigger_conv ctxt then_conv - weight_conv weight ctxt + trigger_conv ctxt -fun gen_normalize1 ctxt weight = +fun gen_normalize1 ctxt = instantiate_elim #> norm_def #> Conv.fconv_rule (Thm.beta_conversion true then_conv Thm.eta_conversion) #> Drule.forall_intr_vars #> - Conv.fconv_rule (gen_normalize1_conv ctxt weight) #> + Conv.fconv_rule (gen_normalize1_conv ctxt) #> (* Z3 4.3.1 silently normalizes "P --> Q --> R" to "P & Q --> R" *) Raw_Simplifier.rewrite_rule ctxt @{thms HOL.imp_conjL[symmetric, THEN eq_reflection]} -fun gen_norm1_safe ctxt (i, (weight, thm)) = - (case try (gen_normalize1 ctxt weight) thm of +fun gen_norm1_safe ctxt (i, thm) = + (case try (gen_normalize1 ctxt) thm of SOME thm' => SOME (i, thm') | NONE => (drop_fact_warning ctxt thm; NONE)) @@ -576,7 +522,6 @@ setup_atomize #> setup_unfolded_quants #> setup_trigger #> - setup_weight #> setup_case_bool #> setup_abs_min_max #> setup_nat_as_int)) diff -r eb5f27ec3987 -r 7b1bf424ec5f src/HOL/Tools/SMT2/smt2_solver.ML --- a/src/HOL/Tools/SMT2/smt2_solver.ML Tue Jun 03 10:35:51 2014 +0200 +++ b/src/HOL/Tools/SMT2/smt2_solver.ML Tue Jun 03 11:43:07 2014 +0200 @@ -32,9 +32,8 @@ val default_max_relevant: Proof.context -> string -> int (*filter*) - val smt2_filter: Proof.context -> thm -> - ((string * ATP_Problem_Generate.stature) * (int option * thm)) list -> int -> Time.time -> - parsed_proof + val smt2_filter: Proof.context -> thm -> ((string * ATP_Problem_Generate.stature) * thm) list -> + int -> Time.time -> parsed_proof (*tactic*) val smt2_tac: Proof.context -> thm list -> int -> tactic @@ -235,17 +234,17 @@ val default_max_relevant = #default_max_relevant oo get_info -fun apply_solver_and_replay ctxt wthms0 = +fun apply_solver_and_replay ctxt thms0 = let - val wthms = map (apsnd (check_topsort ctxt)) wthms0 + val thms = map (check_topsort ctxt) thms0 val (name, {command, replay, ...}) = name_and_info_of ctxt - val (output, replay_data) = invoke name command (SMT2_Normalize.normalize ctxt wthms) ctxt + val (output, replay_data) = invoke name command (SMT2_Normalize.normalize ctxt thms) ctxt in replay ctxt replay_data output end (* filter *) -fun smt2_filter ctxt0 goal xwfacts i time_limit = +fun smt2_filter ctxt0 goal xfacts i time_limit = let val ctxt = ctxt0 |> Config.put SMT2_Config.timeout (Time.toReal time_limit) @@ -256,15 +255,13 @@ SOME ct => ct | NONE => raise SMT2_Failure.SMT (SMT2_Failure.Other_Failure "goal is not a HOL term")) - val wconjecture = (NONE, Thm.assume cprop) - val wprems = map (pair NONE) prems - val wfacts = map snd xwfacts - val xfacts = map (apsnd snd) xwfacts - val wthms = wconjecture :: wprems @ wfacts - val wthms' = map (apsnd (check_topsort ctxt)) wthms + val conjecture = Thm.assume cprop + val facts = map snd xfacts + val thms = conjecture :: prems @ facts + val thms' = map (check_topsort ctxt) thms val (name, {command, parse_proof, ...}) = name_and_info_of ctxt - val (output, replay_data) = invoke name command (SMT2_Normalize.normalize ctxt wthms') ctxt + val (output, replay_data) = invoke name command (SMT2_Normalize.normalize ctxt thms') ctxt in parse_proof ctxt replay_data xfacts (map Thm.prop_of prems) (Thm.term_of concl) output end @@ -277,7 +274,7 @@ fun str_of ctxt fail = "Solver " ^ SMT2_Config.solver_of ctxt ^ ": " ^ SMT2_Failure.string_of_failure fail - fun safe_solve ctxt wfacts = SOME (apply_solver_and_replay ctxt wfacts) + fun safe_solve ctxt facts = SOME (apply_solver_and_replay ctxt facts) handle SMT2_Failure.SMT (fail as SMT2_Failure.Counterexample _) => (SMT2_Config.verbose_msg ctxt (str_of ctxt) fail; NONE) @@ -293,8 +290,7 @@ fun tac prove ctxt rules = CONVERSION (SMT2_Normalize.atomize_conv ctxt) THEN' rtac @{thm ccontr} - THEN' SUBPROOF (fn {context = ctxt, prems, ...} => - resolve (prove ctxt (map (pair NONE) (rules @ prems)))) ctxt + THEN' SUBPROOF (fn {context = ctxt, prems, ...} => resolve (prove ctxt (rules @ prems))) ctxt in val smt2_tac = tac safe_solve diff -r eb5f27ec3987 -r 7b1bf424ec5f src/HOL/Tools/SMT2/smt2_translate.ML --- a/src/HOL/Tools/SMT2/smt2_translate.ML Tue Jun 03 10:35:51 2014 +0200 +++ b/src/HOL/Tools/SMT2/smt2_translate.ML Tue Jun 03 11:43:07 2014 +0200 @@ -13,7 +13,7 @@ SVar of int | SApp of string * sterm list | SLet of string * sterm * sterm | - SQua of squant * string list * sterm spattern list * int option * sterm + SQua of squant * string list * sterm spattern list * sterm (*translation configuration*) type sign = { @@ -51,7 +51,7 @@ SVar of int | SApp of string * sterm list | SLet of string * sterm * sterm | - SQua of squant * string list * sterm spattern list * int option * sterm + SQua of squant * string list * sterm spattern list * sterm @@ -196,9 +196,8 @@ | expand ((q as Const (@{const_name Ex}, _)) $ Abs a) = q $ abs_expand a | expand ((q as Const (@{const_name Ex}, T)) $ t) = q $ exp expand T t | expand (q as Const (@{const_name Ex}, T)) = exp2 T q - | expand ((l as Const (@{const_name Let}, _)) $ t $ Abs a) = expand (Term.betapply (Abs a, t)) - | expand ((l as Const (@{const_name Let}, T)) $ t $ u) = expand (u $ t) - | expand ((l as Const (@{const_name Let}, T)) $ t) = + | expand (Const (@{const_name Let}, _) $ t $ u) = expand (Term.betapply (u, t)) + | expand (Const (@{const_name Let}, T) $ t) = let val U = Term.domain_type (Term.range_type T) in Abs (Name.uu, U, Bound 0 $ Term.incr_boundvars 1 t) end | expand (Const (@{const_name Let}, T)) = @@ -290,15 +289,13 @@ | (u as Bound i, ts) => apply 0 u (nth Ts i) (map (traverse Ts) ts) | (Abs (n, T, u), ts) => traverses Ts (Abs (n, T, traverse (T::Ts) u)) ts | (u, ts) => traverses Ts u ts) - and in_trigger Ts ((c as @{const SMT2.trigger}) $ p $ t) = c $ in_pats Ts p $ in_weight Ts t - | in_trigger Ts t = in_weight Ts t + and in_trigger Ts ((c as @{const SMT2.trigger}) $ p $ t) = c $ in_pats Ts p $ traverse Ts t + | in_trigger Ts t = traverse Ts t and in_pats Ts ps = in_list @{typ "SMT2.pattern list"} (in_list @{typ SMT2.pattern} (in_pat Ts)) ps and in_pat Ts ((p as Const (@{const_name SMT2.pat}, _)) $ t) = p $ traverse Ts t | in_pat Ts ((p as Const (@{const_name SMT2.nopat}, _)) $ t) = p $ traverse Ts t | in_pat _ t = raise TERM ("bad pattern", [t]) - and in_weight Ts ((c as @{const SMT2.weight}) $ w $ t) = c $ w $ traverse Ts t - | in_weight Ts t = traverse Ts t and traverses Ts t ts = Term.list_comb (t, map (traverse Ts) ts) in map (traverse []) ts end @@ -344,9 +341,6 @@ | (Free c, ts) => Term.list_comb (Free c, map (in_term pat) ts) | _ => t) - and in_weight ((c as @{const SMT2.weight}) $ w $ t) = c $ w $ in_form t - | in_weight t = in_form t - and in_pat ((p as Const (@{const_name SMT2.pat}, _)) $ t) = p $ in_term true t | in_pat ((p as Const (@{const_name SMT2.nopat}, _)) $ t) = @@ -356,8 +350,8 @@ and in_pats ps = in_list @{typ "SMT2.pattern list"} (SOME o in_list @{typ SMT2.pattern} (try in_pat)) ps - and in_trigger ((c as @{const SMT2.trigger}) $ p $ t) = c $ in_pats p $ in_weight t - | in_trigger t = in_weight t + and in_trigger ((c as @{const SMT2.trigger}) $ p $ t) = c $ in_pats p $ in_form t + | in_trigger t = in_form t and in_form t = (case Term.strip_comb t of @@ -393,9 +387,6 @@ if q = qname then group_quant qname (T :: Ts) u else (Ts, t) | group_quant _ Ts t = (Ts, t) -fun dest_weight (@{const SMT2.weight} $ w $ t) = (SOME (snd (HOLogic.dest_number w)), t) - | dest_weight t = (NONE, t) - fun dest_pat (Const (@{const_name SMT2.pat}, _) $ t) = (t, true) | dest_pat (Const (@{const_name SMT2.nopat}, _) $ t) = (t, false) | dest_pat t = raise TERM ("bad pattern", [t]) @@ -415,8 +406,7 @@ let val (Ts, u) = group_quant qn [T] t val (ps, p) = dest_trigger u - val (w, b) = dest_weight p - in (q, rev Ts, ps, w, b) end) + in (q, rev Ts, ps, p) end) fun fold_map_pat f (SPat ts) = fold_map f ts #>> SPat | fold_map_pat f (SNoPat ts) = fold_map f ts #>> SNoPat @@ -439,9 +429,9 @@ (case Term.strip_comb t of (Const (qn, _), [Abs (_, T, t1)]) => (case dest_quant qn T t1 of - SOME (q, Ts, ps, w, b) => + SOME (q, Ts, ps, b) => fold_map transT Ts ##>> fold_map (fold_map_pat trans) ps ##>> - trans b #>> (fn ((Ts', ps'), b') => SQua (q, Ts', ps', w, b')) + trans b #>> (fn ((Ts', ps'), b') => SQua (q, Ts', ps', b')) | NONE => raise TERM ("unsupported quantifier", [t])) | (Const (@{const_name Let}, _), [t1, Abs (_, T, t2)]) => transT T ##>> trans t1 ##>> trans t2 #>> (fn ((U, u1), u2) => SLet (U, u1, u2)) diff -r eb5f27ec3987 -r 7b1bf424ec5f src/HOL/Tools/SMT2/smtlib2_interface.ML --- a/src/HOL/Tools/SMT2/smtlib2_interface.ML Tue Jun 03 10:35:51 2014 +0200 +++ b/src/HOL/Tools/SMT2/smtlib2_interface.ML Tue Jun 03 11:43:07 2014 +0200 @@ -89,7 +89,7 @@ SMTLIB2.S (SMTLIB2.Sym n :: map (tree_of_sterm l) ts) | tree_of_sterm _ (SMT2_Translate.SLet _) = raise Fail "SMT-LIB: unsupported let expression" - | tree_of_sterm l (SMT2_Translate.SQua (q, ss, pats, w, t)) = + | tree_of_sterm l (SMT2_Translate.SQua (q, ss, pats, t)) = let val l' = l + length ss @@ -100,18 +100,15 @@ [SMTLIB2.Key keyword, (case map (tree_of_sterm l') ps of [t] => t | ts => SMTLIB2.S ts)] fun trees_of_pat (SMT2_Translate.SPat ps) = gen_trees_of_pat "pattern" ps | trees_of_pat (SMT2_Translate.SNoPat ps) = gen_trees_of_pat "no-pattern" ps - fun trees_of_weight NONE = [] - | trees_of_weight (SOME i) = [SMTLIB2.Key "weight", SMTLIB2.Num i] - fun tree_of_pats_weight [] NONE t = t - | tree_of_pats_weight pats w t = - SMTLIB2.S (SMTLIB2.Sym "!" :: t :: maps trees_of_pat pats @ trees_of_weight w) + fun tree_of_pats [] t = t + | tree_of_pats pats t = SMTLIB2.S (SMTLIB2.Sym "!" :: t :: maps trees_of_pat pats) val vs = map_index (fn (i, ty) => SMTLIB2.S [SMTLIB2.Sym (var (l + i)), SMTLIB2.Sym ty]) ss val body = t |> tree_of_sterm l' - |> tree_of_pats_weight pats w + |> tree_of_pats pats in SMTLIB2.S [SMTLIB2.Sym (quant_name q), SMTLIB2.S vs, body] end diff -r eb5f27ec3987 -r 7b1bf424ec5f src/HOL/Tools/SMT2/z3_new_replay.ML --- a/src/HOL/Tools/SMT2/z3_new_replay.ML Tue Jun 03 10:35:51 2014 +0200 +++ b/src/HOL/Tools/SMT2/z3_new_replay.ML Tue Jun 03 11:43:07 2014 +0200 @@ -72,14 +72,13 @@ local val remove_trigger = mk_meta_eq @{thm SMT2.trigger_def} - val remove_weight = mk_meta_eq @{thm SMT2.weight_def} val remove_fun_app = mk_meta_eq @{thm SMT2.fun_app_def} fun rewrite_conv _ [] = Conv.all_conv | rewrite_conv ctxt eqs = Simplifier.full_rewrite (empty_simpset ctxt addsimps eqs) - val prep_rules = [@{thm Let_def}, remove_trigger, remove_weight, - remove_fun_app, Z3_New_Replay_Literals.rewrite_true] + val prep_rules = [@{thm Let_def}, remove_trigger, remove_fun_app, + Z3_New_Replay_Literals.rewrite_true] fun rewrite _ [] = I | rewrite ctxt eqs = Conv.fconv_rule (rewrite_conv ctxt eqs) diff -r eb5f27ec3987 -r 7b1bf424ec5f src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML Tue Jun 03 10:35:51 2014 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML Tue Jun 03 11:43:07 2014 +0200 @@ -14,12 +14,6 @@ val smt2_builtins : bool Config.T val smt2_triggers : bool Config.T - val smt2_weights : bool Config.T - val smt2_weight_min_facts : int Config.T - val smt2_min_weight : int Config.T - val smt2_max_weight : int Config.T - val smt2_max_weight_index : int Config.T - val smt2_weight_curve : (int -> int) Unsynchronized.ref val smt2_max_slices : int Config.T val smt2_slice_fact_frac : real Config.T val smt2_slice_time_frac : real Config.T @@ -44,35 +38,9 @@ val smt2_builtins = Attrib.setup_config_bool @{binding sledgehammer_smt2_builtins} (K true) val smt2_triggers = Attrib.setup_config_bool @{binding sledgehammer_smt2_triggers} (K true) -val smt2_weights = Attrib.setup_config_bool @{binding sledgehammer_smt2_weights} (K true) -val smt2_weight_min_facts = - Attrib.setup_config_int @{binding sledgehammer_smt2_weight_min_facts} (K 20) val is_smt2_prover = member (op =) o SMT2_Config.available_solvers_of -(* FUDGE *) -val smt2_min_weight = Attrib.setup_config_int @{binding sledgehammer_smt2_min_weight} (K 0) -val smt2_max_weight = Attrib.setup_config_int @{binding sledgehammer_smt2_max_weight} (K 10) -val smt2_max_weight_index = - Attrib.setup_config_int @{binding sledgehammer_smt2_max_weight_index} (K 200) -val smt2_weight_curve = Unsynchronized.ref (fn x : int => x * x) - -fun smt2_fact_weight ctxt j num_facts = - if Config.get ctxt smt2_weights andalso num_facts >= Config.get ctxt smt2_weight_min_facts then - let - val min = Config.get ctxt smt2_min_weight - val max = Config.get ctxt smt2_max_weight - val max_index = Config.get ctxt smt2_max_weight_index - val curve = !smt2_weight_curve - in - SOME (max - (max - min + 1) * curve (Int.max (0, max_index - j - 1)) div curve max_index) - end - else - NONE - -fun weight_smt2_fact ctxt num_facts ((info, th), j) = - (info, (smt2_fact_weight ctxt j num_facts, th)) - (* "SMT2_Failure.Abnormal_Termination" carries the solver's return code. Until these are sorted out properly in the SMT module, we must interpret these here. *) val z3_failures = @@ -128,8 +96,7 @@ val ctxt = Proof.context_of state val max_slices = if slice then Config.get ctxt smt2_max_slices else 1 - fun do_slice timeout slice outcome0 time_so_far - (weighted_factss as (fact_filter, weighted_facts) :: _) = + fun do_slice timeout slice outcome0 time_so_far (factss as (fact_filter, facts) :: _) = let val timer = Timer.startRealTimer () val slice_timeout = @@ -141,7 +108,7 @@ end else timeout - val num_facts = length weighted_facts + val num_facts = length facts val _ = if debug then quote name ^ " slice " ^ string_of_int slice ^ " with " ^ string_of_int num_facts ^ @@ -152,7 +119,7 @@ val birth = Timer.checkRealTimer timer val filter_result as {outcome, ...} = - SMT2_Solver.smt2_filter ctxt goal weighted_facts i slice_timeout + SMT2_Solver.smt2_filter ctxt goal facts i slice_timeout handle exn => if Exn.is_interrupt exn orelse debug then reraise exn @@ -179,8 +146,8 @@ let val new_num_facts = Real.ceil (Config.get ctxt smt2_slice_fact_frac * Real.fromInt num_facts) - val weighted_factss as (new_fact_filter, _) :: _ = - weighted_factss + val factss as (new_fact_filter, _) :: _ = + factss |> (fn (x :: xs) => xs @ [x]) |> app_hd (apsnd (take new_num_facts)) val show_filter = fact_filter <> new_fact_filter @@ -200,11 +167,11 @@ else () in - do_slice timeout (slice + 1) outcome0 time_so_far weighted_factss + do_slice timeout (slice + 1) outcome0 time_so_far factss end else {outcome = if is_none outcome then NONE else the outcome0, filter_result = filter_result, - used_from = map (apsnd snd) weighted_facts, run_time = time_so_far} + used_from = facts, run_time = time_so_far} end in do_slice timeout 1 NONE Time.zeroTime @@ -217,16 +184,8 @@ val thy = Proof.theory_of state val ctxt = Proof.context_of state - val (_, hyp_ts, concl_t) = strip_subgoal goal subgoal ctxt - - fun weight_facts facts = - let val num_facts = length facts in - map (weight_smt2_fact ctxt num_facts) (facts ~~ (0 upto num_facts - 1)) - end - - val weighted_factss = map (apsnd weight_facts) factss val {outcome, filter_result = {fact_ids, atp_proof, ...}, used_from, run_time} = - smt2_filter_loop name params state goal subgoal weighted_factss + smt2_filter_loop name params state goal subgoal factss val used_named_facts = map snd fact_ids val used_facts = map fst used_named_facts val outcome = Option.map failure_of_smt2_failure outcome