(* $Id$ *)
-type aux_comparison = XEQ | XLE | XGE | XLT | XGT | XINCOMPARABLE
+type aux_comparison = XEQ | XLE | XGE | XLT | XGT | XINCOMPARABLE | XINVERTIBLE
module type Blob =
sig
val compare_terms :
t Terms.foterm -> t Terms.foterm -> Terms.comparison
- val compute_unit_clause_weight : 't Terms.unit_clause -> int
-
- val compute_goal_weight : 't Terms.unit_clause -> int
+ val compute_clause_weight : 't Terms.clause -> int
val name : string
(w, List.sort compare l) (* from the smallest meta to the bigest *)
;;
-let compute_unit_clause_weight (_,l, _, _) =
+let compute_literal_weight l =
let weight_of_polynomial w m =
let factor = 2 in
w + factor * List.fold_left (fun acc (_,occ) -> acc+occ) 0 m
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) ->
+ | Terms.Equation (l,r,_,Terms.Incomparable)
+ | Terms.Equation (l,r,_,Terms.Invertible) ->
let wl, ml = weight_of_term l in
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))
- ;;
+let compute_clause_weight (_,nl,pl,_,_) =
+ List.fold_left (fun acc (lit,_) -> compute_literal_weight lit + acc) 0 (nl@pl)
+
+let compute_goal_weight = compute_clause_weight;;
(* Riazanov: 3.1.5 pag 38 *)
(* Compare weights normalized in a new way :
| XGT -> Terms.Gt
| XLT -> Terms.Lt
| XEQ -> Terms.Eq
+ | XINVERTIBLE -> Terms.Invertible
| _ -> assert false
;;
+let are_invertible relocate alpha_eq l r =
+ let varlist = Terms.vars_of_term l in
+ let maxvar = List.fold_left max 0 varlist in
+ let _,_,subst = relocate maxvar varlist FoSubst.id_subst in
+ let l = FoSubst.apply_subst subst l in
+ try (ignore(alpha_eq l r);true) with
+ FoUnif.UnificationFailure _ -> false;;
+
module NRKBO (B : Terms.Blob) = struct
let name = "nrkbo"
include B
module Pp = Pp.Pp(B)
+ module Unif = FoUnif.FoUnif(B)
+ module Utils = FoUtils.Utils(B)
let eq_foterm = eq_foterm B.eq;;
- let compute_unit_clause_weight = compute_unit_clause_weight;;
- let compute_goal_weight = compute_goal_weight;;
+ let are_invertible = are_invertible Utils.relocate Unif.alpha_eq;;
+
+ let compute_clause_weight = compute_clause_weight;;
(* Riazanov: p. 40, relation >_n *)
let nonrec_kbo t1 t2 =
if aux_ordering B.compare t1 t2 = XLT then XLT else XINCOMPARABLE
| XGE ->
if aux_ordering B.compare t1 t2 = XGT then XGT else XINCOMPARABLE
- | XEQ -> aux_ordering B.compare t1 t2
+ | XEQ -> let res = aux_ordering B.compare t1 t2 in
+ if res = XINCOMPARABLE && are_invertible t1 t2 then XINVERTIBLE
+ else res
| res -> res
;;
include B
module Pp = Pp.Pp(B)
+ module Unif = FoUnif.FoUnif(B)
+ module Utils = FoUtils.Utils(B)
let eq_foterm = eq_foterm B.eq;;
- let compute_unit_clause_weight = compute_unit_clause_weight;;
+ let are_invertible = are_invertible Utils.relocate Unif.alpha_eq;;
+
+ let compute_clause_weight = compute_clause_weight;;
let compute_goal_weight = compute_goal_weight;;
(* Riazanov: p. 38, relation > *)
let r = aux t1 t2 in
if r = XEQ then (
match t1, t2 with
+ | Terms.Var i, Terms.Var j when i=j -> XEQ
| Terms.Node (_::tl1), Terms.Node (_::tl2) -> cmp tl1 tl2
| _, _ -> XINCOMPARABLE
) else r
include B
module Pp = Pp.Pp(B)
+ module Unif = FoUnif.FoUnif(B)
+ module Utils = FoUtils.Utils(B)
let eq_foterm = eq_foterm B.eq;;
- let compute_unit_clause_weight = compute_unit_clause_weight;;
+ let are_invertible = are_invertible Utils.relocate Unif.alpha_eq;;
+
+ let compute_clause_weight = compute_clause_weight;;
let compute_goal_weight = compute_goal_weight;;
let rec lpo s t =