+let weight_age_ratio = ref 0;; (* settable by the user from the command line *)
+let weight_age_counter = ref !weight_age_ratio;;
+
+let symbols_ratio = ref 0;;
+let symbols_counter = ref 0;;
+
+
+let select env passive active =
+ let (neg_list, neg_set), (pos_list, pos_set) = passive in
+ let remove eq l =
+ List.filter (fun e -> not (e = eq)) l
+ in
+ if !weight_age_ratio > 0 then
+ weight_age_counter := !weight_age_counter - 1;
+ match !weight_age_counter with
+ | 0 -> (
+ weight_age_counter := !weight_age_ratio;
+ match neg_list, pos_list with
+ | hd::tl, pos ->
+ (Negative, hd), ((tl, EqualitySet.remove hd neg_set), (pos, pos_set))
+ | [], hd::tl ->
+ (Positive, hd), (([], neg_set), (tl, EqualitySet.remove hd pos_set))
+ | _, _ -> assert false
+ )
+ | _ when (!symbols_counter > 0) && (EqualitySet.is_empty neg_set) -> (
+ symbols_counter := !symbols_counter - 1;
+ let cardinality map =
+ TermMap.fold (fun k v res -> res + v) map 0
+ in
+ match active with
+ | (Negative, e)::_ ->
+ let symbols = symbols_of_equality e in
+ let card = cardinality symbols in
+ let f equality (i, e) =
+ let common, others =
+ TermMap.fold
+ (fun 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)
+ (symbols_of_equality equality) (0, 0)
+ in
+(* Printf.printf "equality: %s, common: %d, others: %d\n" *)
+(* (string_of_equality ~env equality) common others; *)
+ let c = others + (abs (common - card)) in
+ if c < i then (c, equality)
+ else (i, e)
+ in
+ let e1 = EqualitySet.min_elt pos_set in
+ let initial =
+ let common, others =
+ TermMap.fold
+ (fun 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 - (abs (c - v)) in
+ r1 + c1, r2 + c2
+ else
+ r1, r2 + v)
+ (symbols_of_equality e1) (0, 0)
+ in
+ (others + (abs (common - card))), e1
+ in
+ let _, current = EqualitySet.fold f pos_set initial in
+ Printf.printf "\nsymbols-based selection: %s\n\n"
+ (string_of_equality ~env current);
+ (Positive, current),
+ (([], neg_set),
+ (remove current pos_list, EqualitySet.remove current pos_set))
+ | _ ->
+ let current = EqualitySet.min_elt pos_set in
+ let passive =
+ (neg_list, neg_set),
+ (remove current pos_list, EqualitySet.remove current pos_set)
+ in
+ (Positive, current), passive
+ )
+ | _ ->
+ symbols_counter := !symbols_ratio;
+ let set_selection set = EqualitySet.min_elt set in
+ if EqualitySet.is_empty neg_set then
+ let current = set_selection pos_set in
+ let passive =
+ (neg_list, neg_set),
+ (remove current pos_list, EqualitySet.remove current pos_set)
+ in
+ (Positive, current), passive
+ else
+ let current = set_selection neg_set in
+ let passive =
+ (remove current neg_list, EqualitySet.remove current neg_set),
+ (pos_list, pos_set)
+ in
+ (Negative, current), passive