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 :
) else r
| res -> res
;;
-
+
+ let rec lpo s t =
+ match s,t with
+ | Terms.Var i, Terms.Var j when i = j ->
+ XEQ
+ | Terms.Var _, Terms.Var _ ->
+ XINCOMPARABLE
+ | Terms.Var _, _ ->
+ (match lpo t s with
+ | XGT -> XLT
+ | XLT -> XGT
+ | o -> o)
+ | _, Terms.Var i ->
+ if (List.mem i (Terms.vars_of_term s)) then XGT
+ else XINCOMPARABLE
+ | 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.Node (hd1::tl1), Terms.Node (hd2::tl2) ->
+ (match lpo hd1 hd2 with
+ | XGT -> if List.for_all (fun x -> lpo s x = XGT) tl2 then XGT
+ else XINCOMPARABLE
+ | XLT -> if List.for_all (fun x -> lpo s x = XLT) tl2 then XLT
+ else XINCOMPARABLE
+ | XEQ -> List.fold_left2
+ (fun acc si ti -> if acc = XEQ then lpo si ti else acc)
+ XEQ tl1 tl2
+ | XINCOMPARABLE -> XINCOMPARABLE
+ | _ -> assert false)
+ | _ -> assert false
+
+ ;;
+
let compare_terms x y =
- match nonrec_kbo x y with
+ match kbo x y with
| XINCOMPARABLE -> Terms.Incomparable
| XGT -> Terms.Gt
| XLT -> Terms.Lt