-(* Riazanov: 3.1.5 pag 38 *)
-let compare_weights ((h1, w1) as weight1) ((h2, w2) as weight2)=
- let res, diffs =
- try
- List.fold_left2
- (fun ((lt, eq, gt), diffs) w1 w2 ->
- match w1, w2 with
- | (meta1, w1), (meta2, w2) when meta1 = meta2 ->
- let diffs = (w1 - w2) + diffs in
- let r = compare w1 w2 in
- if r < 0 then (lt+1, eq, gt), diffs
- else if r = 0 then (lt, eq+1, gt), diffs
- else (lt, eq, gt+1), diffs
- | _ -> assert false)
- ((0, 0, 0), 0) w1 w2
- with Invalid_argument _ -> assert false
- in
- let hdiff = h1 - h2 in
- match res with
- | (0, _, 0) ->
- if hdiff < 0 then Lt
- else if hdiff > 0 then Gt
- else Eq
- | (m, _, 0) ->
- if hdiff <= 0 then Lt
- else if (- diffs) >= hdiff then Le else Incomparable
- | (0, _, m) ->
- if hdiff >= 0 then Gt
- else if diffs >= (- hdiff) then Ge else Incomparable
- | (m, _, n) when m > 0 && n > 0 ->
- Incomparable
- | _ -> assert false
-;;
+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 :
+ * Variables should be sorted from the lowest index to the highest
+ * Variables which do not occur in the term should not be present
+ * in the normalized polynomial
+ *)
+ let compare_weights (h1, w1) (h2, w2) =
+ let rec aux hdiff (lt, gt) diffs w1 w2 =
+ match w1, w2 with
+ | ((var1, w1)::tl1) as l1, (((var2, w2)::tl2) as l2) ->
+ if var1 = var2 then
+ let diffs = (w1 - w2) + diffs in
+ let r = compare w1 w2 in
+ let lt = lt or (r < 0) in
+ let gt = gt or (r > 0) in
+ if lt && gt then XINCOMPARABLE else
+ aux hdiff (lt, gt) diffs tl1 tl2
+ else if var1 < var2 then
+ if lt then XINCOMPARABLE else
+ aux hdiff (false,true) (diffs+w1) tl1 l2
+ else
+ if gt then XINCOMPARABLE else
+ aux hdiff (true,false) (diffs-w2) l1 tl2
+ | [], (_,w2)::tl2 ->
+ if gt then XINCOMPARABLE else
+ aux hdiff (true,false) (diffs-w2) [] tl2
+ | (_,w1)::tl1, [] ->
+ if lt then XINCOMPARABLE else
+ aux hdiff (false,true) (diffs+w1) tl1 []
+ | [], [] ->
+ if lt then
+ if hdiff <= 0 then XLT
+ else if (- diffs) >= hdiff then XLE else XINCOMPARABLE
+ else if gt then
+ if hdiff >= 0 then XGT
+ else if diffs >= (- hdiff) then XGE else XINCOMPARABLE
+ else
+ if hdiff < 0 then XLT
+ else if hdiff > 0 then XGT
+ else XEQ
+ in
+ aux (h1-h2) (false,false) 0 w1 w2
+ ;;
+
+ (* Riazanov: p. 40, relation >>>
+ * if head_only=true then it is not >>> but helps case 2 of 3.14 p 39 *)
+ let rec aux_ordering ?(head_only=false) t1 t2 =
+ match t1, t2 with
+ (* We want to discard any identity equality. *
+ * If we give back XEQ, no inference rule *
+ * will be applied on this equality *)
+ | Terms.Var i, Terms.Var j when i = j ->
+ XEQ
+ (* 1. *)
+ | Terms.Var _, _
+ | _, Terms.Var _ -> XINCOMPARABLE
+ (* 2.a *)
+ | Terms.Leaf a1, Terms.Leaf a2 ->
+ let cmp = B.compare a1 a2 in
+ if cmp = 0 then XEQ else if cmp < 0 then XLT else XGT
+ | Terms.Leaf _, Terms.Node _ -> XLT
+ | Terms.Node _, Terms.Leaf _ -> XGT
+ (* 2.b *)
+ | Terms.Node l1, Terms.Node l2 ->
+ let rec cmp t1 t2 =
+ match t1, t2 with
+ | [], [] -> XEQ
+ | _, [] -> XGT
+ | [], _ -> XLT
+ | hd1::tl1, hd2::tl2 ->
+ let o = aux_ordering ~head_only hd1 hd2 in
+ if o = XEQ && not head_only then cmp tl1 tl2 else o
+ in
+ cmp l1 l2
+ ;;
+
+ (* Riazanov: p. 40, relation >_n *)
+ let nonrec_kbo t1 t2 =
+ let w1 = weight_of_term t1 in
+ let w2 = weight_of_term t2 in
+ match compare_weights w1 w2 with
+ | XLE -> (* this is .> *)
+ if aux_ordering t1 t2 = XLT then XLT else XINCOMPARABLE
+ | XGE ->
+ if aux_ordering t1 t2 = XGT then XGT else XINCOMPARABLE
+ | XEQ -> aux_ordering t1 t2
+ | res -> res
+ ;;
+
+ (* Riazanov: p. 38, relation > *)
+ let rec kbo t1 t2 =
+ let aux = aux_ordering ~head_only:true in
+ let rec cmp t1 t2 =
+ match t1, t2 with
+ | [], [] -> XEQ
+ | _, [] -> XGT
+ | [], _ -> XLT
+ | hd1::tl1, hd2::tl2 ->
+ let o = kbo hd1 hd2 in
+ if o = XEQ then cmp tl1 tl2
+ else o
+ in
+ let w1 = weight_of_term t1 in
+ let w2 = weight_of_term t2 in
+ let comparison = compare_weights w1 w2 in
+ match comparison with
+ | XLE ->
+ let r = aux t1 t2 in
+ if r = XLT then XLT
+ else if r = XEQ then (
+ match t1, t2 with
+ | Terms.Node (_::tl1), Terms.Node (_::tl2) ->
+ if cmp tl1 tl2 = XLT then XLT else XINCOMPARABLE
+ | _, _ -> assert false
+ ) else XINCOMPARABLE
+ | XGE ->
+ let r = aux t1 t2 in
+ if r = XGT then XGT
+ else if r = XEQ then (
+ match t1, t2 with
+ | Terms.Node (_::tl1), Terms.Node (_::tl2) ->
+ if cmp tl1 tl2 = XGT then XGT else XINCOMPARABLE
+ | _, _ -> assert false
+ ) else XINCOMPARABLE
+ | XEQ ->
+ let r = aux t1 t2 in
+ if r = XEQ then (
+ match t1, t2 with
+ | Terms.Node (_::tl1), Terms.Node (_::tl2) -> cmp tl1 tl2
+ | _, _ -> XINCOMPARABLE
+ ) else r
+ | res -> res
+ ;;