- 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
+ let counter = ref !symbols_ratio in
+ let rec pickw w ns ps =
+ if w > 0 then
+ if not (EqualitySet.is_empty ns) then
+ let e = EqualitySet.min_elt ns in
+ let ns', ps = pickw (w-1) (EqualitySet.remove e ns) ps in
+ EqualitySet.add e ns', ps
+ else if !counter > 0 then
+ let _ =
+ counter := !counter - 1;
+ if !counter = 0 then counter := !symbols_ratio
+ in
+ match symbols with
+ | None ->
+ let e = EqualitySet.min_elt ps in
+ let ns, ps' = pickw (w-1) ns (EqualitySet.remove e ps) in
+ ns, EqualitySet.add e ps'
+ | Some symbols ->
+ let foldfun k v (r1, r2) =
+ if TermMap.mem k symbols then
+ let c = TermMap.find k symbols in
+ let c1 = abs (c - v) in
+ let c2 = v - c1 in
+ r1 + c2, r2 + c1
+ else
+ r1, r2 + v
+ in
+ let f equality (i, e) =
+ let common, others =
+ TermMap.fold foldfun (symbols_of_equality equality) (0, 0)
+ in
+ let c = others + (abs (common - card)) in
+ if c < i then (c, equality)
+ else (i, e)
+ in
+ let e1 = EqualitySet.min_elt ps in
+ let initial =
+ let common, others =
+ TermMap.fold foldfun (symbols_of_equality e1) (0, 0)
+ in
+ (others + (abs (common - card))), e1
+ in
+ let _, e = EqualitySet.fold f ps initial in
+ let ns, ps' = pickw (w-1) ns (EqualitySet.remove e ps) in
+ ns, EqualitySet.add e ps'
+ else
+ let e = EqualitySet.min_elt ps in
+ let ns, ps' = pickw (w-1) ns (EqualitySet.remove e ps) in
+ ns, EqualitySet.add e ps'