- let compute_clause_weight = assert false (*
- let factor = 2 in
- match o with
- | Terms.Lt ->
- let w, m = (weight_of_term
- ~consider_metas:true ~count_metas_occurrences:false right) in
- w + (factor * (List.length m)) ;
- | Terms.Le -> assert false
- | Terms.Gt ->
- let w, m = (weight_of_term
- ~consider_metas:true ~count_metas_occurrences:false left) in
- w + (factor * (List.length m)) ;
- | Terms.Ge -> assert false
- | Terms.Eq
- | Terms.Incomparable ->
- let w1, m1 = (weight_of_term
- ~consider_metas:true ~count_metas_occurrences:false right) in
- let w2, m2 = (weight_of_term
- ~consider_metas:true ~count_metas_occurrences:false left) in
- w1 + w2 + (factor * (List.length m1)) + (factor * (List.length m2))
- *)
+ let compute_unit_clause_weight =
+ let weight_of_polynomial w m =
+ let factor = 2 in
+ w + factor * List.fold_left (fun acc (_,occ) -> acc+occ) 0 m
+ in
+ function
+ | Terms.Predicate t ->
+ let w, m = weight_of_term t in
+ weight_of_polynomial w m
+ | Terms.Equation (_,x,_,Terms.Lt)
+ | Terms.Equation (x,_,_,Terms.Gt) ->
+ let w, m = weight_of_term x in
+ weight_of_polynomial w m
+ | Terms.Equation (l,r,_,Terms.Eq)
+ | Terms.Equation (l,r,_,Terms.Incomparable) ->
+ let wl, ml = weight_of_term l in
+ let wr, mr = weight_of_term r in
+ weight_of_polynomial (wl+wr) (ml@mr)