--- 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 \<Rightarrow> bool \<Rightarrow> 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 \<Rightarrow> bool \<Rightarrow> 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 "\<forall>x. trigger [[pat (P x)]] (weight 2 (P x))"}
-\item
-@{term "\<forall>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
--- 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 "\<forall>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 *}
--- 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))
--- 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
--- 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))
--- 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
--- 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)
--- 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