| ((var1, w1)::tl1) as l1, (((var2, w2)::tl2) as l2) ->
if var1 = var2 then
let diffs = (w1 - w2) + diffs in
- let r = Pervasives.compare w1 w2 in
- let lt = lt or (r < 0) in
- let gt = gt or (r > 0) in
+ let r = Stdlib.compare w1 w2 in
+ let lt = lt || (r < 0) in
+ let gt = gt || (r > 0) in
if lt && gt then XINCOMPARABLE else
aux hdiff (lt, gt) diffs tl1 tl2
else if var1 < var2 then
let name = "nrkbo"
include B
- module Pp = Pp.Pp(B)
+ (*module Pp = Pp.Pp(B)*)
let eq_foterm = eq_foterm B.eq;;
in
match s, t with
| s, t when eq_foterm s t -> subst
- | Terms.Var i, Terms.Var j
+ | Terms.Var i, Terms.Var _j
when (not (List.exists (fun (_,k) -> k=t) subst)) ->
let subst = FoSubst.build_subst i t subst in
subst
let name = "kbo"
include B
- module Pp = Pp.Pp(B)
+ (*module Pp = Pp.Pp(B)*)
let eq_foterm = eq_foterm B.eq;;
let name = "lpo"
include B
- module Pp = Pp.Pp(B)
+ (*module Pp = Pp.Pp(B)*)
let eq_foterm = eq_foterm B.eq;;
let compute_goal_weight = compute_goal_weight;;
(*CSC: beware! Imperative cache! *)
- let cache = ref [];;
+ let cache = Hashtbl.create 101
let rec lpo_le s t =
eq_foterm s t || lpo_lt s t
and lpo_lt s t =
- try List.assoc (s,t) !cache
+ try Hashtbl.find cache (s,t)
with
Not_found -> let res =
match s,t with
| _ -> assert false
end
in
- cache := ((s,t),res)::!cache; res
+ Hashtbl.add cache (s,t) res; res
;;
let lpo s t =
else if lpo_lt t s then XGT
else XINCOMPARABLE
in
- cache := []; res
+ Hashtbl.clear cache; res
;;