(w, List.sort compare l) (* from the smallest meta to the bigest *)
;;
- let compute_unit_clause_weight =
+ let compute_unit_clause_weight (_,l, _, _) =
let weight_of_polynomial w m =
let factor = 2 in
w + factor * List.fold_left (fun acc (_,occ) -> acc+occ) 0 m
in
- function
+ match l with
| Terms.Predicate t ->
let w, m = weight_of_term t in
weight_of_polynomial w m
let wr, mr = weight_of_term r in
weight_of_polynomial (wl+wr) (ml@mr)
;;
+
+let compute_goal_weight (_,l, _, _) =
+ let weight_of_polynomial w m =
+ let factor = 2 in
+ w + factor * List.fold_left (fun acc (_,occ) -> acc+occ) 0 m
+ in
+ match l with
+ | Terms.Predicate t ->
+ let w, m = weight_of_term t in
+ weight_of_polynomial w m
+ | Terms.Equation (l,r,_,_) ->
+ let wl, ml = weight_of_term l in
+ let wr, mr = weight_of_term r in
+ let wl = weight_of_polynomial wl ml in
+ let wr = weight_of_polynomial wr mr in
+ - (abs (wl-wr))
+ ;;
(* Riazanov: 3.1.5 pag 38 *)
(* Compare weights normalized in a new way :