(* $Id$ *)
+type aux_comparison = XEQ | XLE | XGE | XLT | XGT | XINCOMPARABLE
+
module Orderings (B : Terms.Blob) = struct
type weight = int * (int * int) list;;
(w, List.sort compare l) (* from the biggest meta to the smallest (0) *)
;;
- 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)
;;
(* returns a "normalized" version of the polynomial weight wl (with type
;;
(* Riazanov: 3.1.5 pag 38 *)
- (* TODO: optimize early detection of Terms.Incomparable case *)
+ (* TODO: optimize early detection of XINCOMPARABLE case *)
let compare_weights (h1, w1) (h2, w2) =
let res, diffs =
try
let hdiff = h1 - h2 in
match res with
| (0, _, 0) ->
- if hdiff < 0 then Terms.Lt
- else if hdiff > 0 then Terms.Gt
- else Terms.Eq
+ if hdiff < 0 then XLT
+ else if hdiff > 0 then XGT
+ else XEQ
| (m, _, 0) ->
- if hdiff <= 0 then Terms.Lt
- else if (- diffs) >= hdiff then Terms.Le else Terms.Incomparable
+ if hdiff <= 0 then XLT
+ else if (- diffs) >= hdiff then XLE else XINCOMPARABLE
| (0, _, m) ->
- if hdiff >= 0 then Terms.Gt
- else if diffs >= (- hdiff) then Terms.Ge else Terms.Incomparable
- | (m, _, n) when m > 0 && n > 0 -> Terms.Incomparable
+ if hdiff >= 0 then XGT
+ else if diffs >= (- hdiff) then XGE else XINCOMPARABLE
+ | (m, _, n) when m > 0 && n > 0 -> XINCOMPARABLE
| _ -> assert false
;;
-
- let rec aux_ordering t1 t2 =
+ (* 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
+ (* 1. *)
| Terms.Var _, _
- | _, Terms.Var _ -> Terms.Incomparable
-
+ | _, Terms.Var _ -> XINCOMPARABLE
+ (* 2.a *)
| Terms.Leaf a1, Terms.Leaf a2 ->
- let cmp = Pervasives.compare a1 a2 in
- if cmp = 0 then Terms.Eq else if cmp < 0 then Terms.Lt else Terms.Gt
-
- | Terms.Leaf _, Terms.Node _ -> Terms.Lt
- | Terms.Node _, Terms.Leaf _ -> Terms.Gt
-
+ 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
- | [], [] -> Terms.Eq
- | _, [] -> Terms.Gt
- | [], _ -> Terms.Lt
+ | [], [] -> XEQ
+ | _, [] -> XGT
+ | [], _ -> XLT
| hd1::tl1, hd2::tl2 ->
- let o = aux_ordering hd1 hd2 in
- if o = Terms.Eq then cmp tl1 tl2
- else o
+ 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
let w1, w2 = normalize_weights w1 w2 in
match compare_weights w1 w2 with
- | Terms.Le -> if aux_ordering t1 t2 = Terms.Lt then Terms.Lt else Terms.Incomparable
- | Terms.Ge -> if aux_ordering t1 t2 = Terms.Gt then Terms.Gt else Terms.Incomparable
- | Terms.Eq -> aux_ordering t1 t2
+ | 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 ~recursion:false in
- let w1 = weight_of_term t1
- and w2 = weight_of_term t2 in
+ let aux = aux_ordering ~head_only:true in
let rec cmp t1 t2 =
match t1, t2 with
- | [], [] -> Terms.Eq
- | _, [] -> Terms.Gt
- | [], _ -> Terms.Lt
+ | [], [] -> XEQ
+ | _, [] -> XGT
+ | [], _ -> XLT
| hd1::tl1, hd2::tl2 ->
- let o =
- kbo hd1 hd2
- in
- if o = Terms.Eq then cmp tl1 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 w1, w2 = normalize_weights w1 w2 in
let comparison = compare_weights w1 w2 in
match comparison with
- | Terms.Le ->
+ | XLE ->
let r = aux t1 t2 in
- if r = Terms.Lt then Terms.Lt
- else if r = Terms.Eq then (
+ if r = XLT then XLT
+ else if r = XEQ then (
match t1, t2 with
- | Cic.Appl (h1::tl1), Cic.Appl (h2::tl2) when h1 = h2 ->
- if cmp tl1 tl2 = Terms.Lt then Terms.Lt else Terms.Incomparable
- | _, _ -> Terms.Incomparable
- ) else Terms.Incomparable
- | Terms.Ge ->
+ | 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 = Terms.Gt then Terms.Gt
- else if r = Terms.Eq then (
+ if r = XGT then XGT
+ else if r = XEQ then (
match t1, t2 with
- | Cic.Appl (h1::tl1), Cic.Appl (h2::tl2) when h1 = h2 ->
- if cmp tl1 tl2 = Terms.Gt then Terms.Gt else Terms.Incomparable
- | _, _ -> Terms.Incomparable
- ) else Terms.Incomparable
- | Terms.Eq ->
+ | 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 = Terms.Eq then (
+ if r = XEQ then (
match t1, t2 with
- | Cic.Appl (h1::tl1), Cic.Appl (h2::tl2) when h1 = h2 ->
- cmp tl1 tl2
- | _, _ -> Terms.Incomparable
+ | Terms.Node (_::tl1), Terms.Node (_::tl2) -> cmp tl1 tl2
+ | _, _ -> XINCOMPARABLE
) else r
| res -> res
;;
- *)
- let compare_terms = nonrec_kbo;;
+ let compare_terms x y =
+ match nonrec_kbo x y with
+ | XINCOMPARABLE -> Terms.Incomparable
+ | XGT -> Terms.Gt
+ | XLT -> Terms.Lt
+ | XEQ -> Terms.Eq
+ | _ -> assert false
+ ;;
end
projects / helm.git / commitdiff