-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))
- ;;
+let compute_clause_weight (_,nl,pl,_,_) =
+ List.fold_left (fun acc lit -> compute_literal_weight lit + acc) 0 (nl@pl)
+
+let compute_goal_weight = compute_clause_weight;;