module Index(B : Orderings.Blob) = struct
module U = FoUtils.Utils(B)
+ module Unif = FoUnif.Founif(B)
+ module Pp = Pp.Pp(B)
module ClauseOT =
struct
type dataset = ClauseSet.t
= Make(FotermIndexable)(ClauseSet)
- let index_unit_clause t = function
+ let are_invertible maxvar varlist l r =
+ let _,_,subst = U.relocate maxvar varlist FoSubst.id_subst in
+ let l = FoSubst.apply_subst subst l in
+ try (ignore(Unif.alpha_eq l r);true) with
+ FoUnif.UnificationFailure _ -> false
+
+ let index_unit_clause maxvar t = function
| (_,Terms.Equation (l,_,_,Terms.Gt),_,_) as c ->
DT.index t l (Terms.Left2Right, c)
| (_,Terms.Equation (_,r,_,Terms.Lt),_,_) as c ->
DT.index t r (Terms.Right2Left, c)
- | (_,Terms.Equation (l,r,_,Terms.Incomparable),_,_) as c ->
+ | (_,Terms.Equation (l,r,_,Terms.Incomparable),vl,_) as c ->
+ if are_invertible maxvar vl l r then
+ (prerr_endline ("Invertible " ^ (Pp.pp_foterm l) ^ "=" ^
+ (Pp.pp_foterm r));
+ DT.index t l (Terms.Left2Right, c))
+ else
DT.index
(DT.index t l (Terms.Left2Right, c))
r (Terms.Right2Left, c)