in
let compare w1 w2 =
match w1, w2 with
- | (m1, _), (m2, _) -> m2 - m1
+ | (m1, _), (m2, _) -> m1 - m2
in
- (w, List.sort compare l) (* from the biggest meta to the smallest (0) *)
+ (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
- | Terms.Equation (_,x,_,Terms.Lt)
+ | Terms.Equation (_,x,_,Terms.Lt)
| Terms.Equation (x,_,_,Terms.Gt) ->
let w, m = weight_of_term x in
weight_of_polynomial w m
let wr, mr = weight_of_term r in
weight_of_polynomial (wl+wr) (ml@mr)
;;
-
- (* returns a "normalized" version of the polynomial weight wl (with type
- * weight list), i.e. a list sorted ascending by meta number,
- * from 0 to maxmeta. wl must be sorted descending by meta number. Example:
- * normalize_weight 5 (3, [(3, 2); (1, 1)]) ->
- * (3, [(1, 1); (2, 0); (3, 2); (4, 0); (5, 0)]) *)
- let normalize_weight maxmeta (cw, wl) =
- let rec aux = function
- | 0 -> []
- | m -> (m, 0)::(aux (m-1))
- in
- let tmpl = aux maxmeta in
- let wl =
- List.sort
- (fun (m, _) (n, _) -> Pervasives.compare m n)
- (List.fold_left
- (fun res (m, w) -> (m, w)::(List.remove_assoc m res)) tmpl wl)
- in
- (cw, wl)
- ;;
-
-
- let normalize_weights (cw1, wl1) (cw2, wl2) =
- let rec aux wl1 wl2 =
- match wl1, wl2 with
- | [], [] -> [], []
- | (m, w)::tl1, (n, w')::tl2 when m = n ->
- let res1, res2 = aux tl1 tl2 in
- (m, w)::res1, (n, w')::res2
- | (m, w)::tl1, ((n, w')::_ as wl2) when m < n ->
- let res1, res2 = aux tl1 wl2 in
- (m, w)::res1, (m, 0)::res2
- | ((m, w)::_ as wl1), (n, w')::tl2 when m > n ->
- let res1, res2 = aux wl1 tl2 in
- (n, 0)::res1, (n, w')::res2
- | [], (n, w)::tl2 ->
- let res1, res2 = aux [] tl2 in
- (n, 0)::res1, (n, w)::res2
- | (m, w)::tl1, [] ->
- let res1, res2 = aux tl1 [] in
- (m, w)::res1, (m, 0)::res2
- | _, _ -> 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
- let cmp (m, _) (n, _) = compare m n in
- let wl1, wl2 = aux (List.sort cmp wl1) (List.sort cmp wl2) in
- (cw1, wl1), (cw2, wl2)
+ 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 *)
- (* TODO: optimize early detection of XINCOMPARABLE case *)
+(* 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 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
+ 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
- let hdiff = h1 - h2 in
- match res with
- | (0, _, 0) ->
- if hdiff < 0 then XLT
- else if hdiff > 0 then XGT
- else XEQ
- | (m, _, 0) ->
- if hdiff <= 0 then XLT
- else if (- diffs) >= hdiff then XLE else XINCOMPARABLE
- | (0, _, m) ->
- if hdiff >= 0 then XGT
- else if diffs >= (- hdiff) then XGE else XINCOMPARABLE
- | (m, _, n) when m > 0 && n > 0 -> XINCOMPARABLE
- | _ -> assert false
+ 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
let nonrec_kbo t1 t2 =
let w1 = weight_of_term t1 in
let w2 = weight_of_term t2 in
- let w1, w2 = normalize_weights w1 w2 in
match compare_weights w1 w2 with
| XLE -> (* this is .> *)
if aux_ordering t1 t2 = XLT then XLT else XINCOMPARABLE
in
let w1 = weight_of_term t1 in
let w2 = weight_of_term t2 in
- let w1, w2 = normalize_weights w1 w2 in
let comparison = compare_weights w1 w2 in
match comparison with
| XLE ->
) 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
projects / helm.git / blobdiff