+let size_of_passive ((_, ns), (_, ps), _) =
+ (EqualitySet.cardinal ns) + (EqualitySet.cardinal ps)
+;;
+
+
+let prune_passive (((nl, ns), (pl, ps), tbl) as passive) =
+ let f =
+ int_of_float ((!time_limit -. !elapsed_time) /.
+ (!elapsed_time *. (float_of_int !weight_age_ratio)))
+ in
+ let in_weight = !processed_clauses * !weight_age_ratio * f
+ and in_age = !processed_clauses * f in
+ let rec pickw w s =
+ if w > 0 then
+ try
+ let e = EqualitySet.min_elt s in
+ let w, s' = pickw (w-1) (EqualitySet.remove e s) in
+ w, EqualitySet.add e s'
+ with Not_found ->
+ w, s
+ else
+ 0, EqualitySet.empty
+ in
+ let in_weight, ns = pickw in_weight ns in
+ let _, ps = pickw in_weight ps in
+ let rec picka w s l =
+ if w > 0 then
+ match l with
+ | [] -> w, s, []
+ | hd::tl when not (EqualitySet.mem hd s) ->
+ let w, s, l = picka (w-1) s tl in
+ w, EqualitySet.add hd s, hd::l
+ | hd::tl ->
+ let w, s, l = picka w s tl in
+ w, s, hd::l
+ else
+ 0, s, []
+ in
+ let in_age, ns, nl = picka in_age ns nl in
+ let _, ps, pl = picka in_age ps pl in
+ if not (EqualitySet.is_empty ps) then
+ maximal_retained_equality := Some (EqualitySet.max_elt ps);
+ let tbl =
+ EqualitySet.fold
+ (fun e tbl -> Indexing.index tbl e) ps (Indexing.empty_table ()) in
+ (nl, ns), (pl, ps), tbl
+;;
+