module Index(B : Orderings.Blob) = struct
module U = FoUtils.Utils(B)
+ module Clauses = Clauses.Clauses(B)
module ClauseOT =
struct
let compare (d1,p1,pos1,uc1) (d2,p2,pos2,uc2) =
let c = Pervasives.compare (d1,p1,pos1) (d2,p2,pos2) in
- if c <> 0 then c else U.compare_clause uc1 uc2
+ if c <> 0 then c else Clauses.compare_clause uc1 uc2
;;
end
= Make(FotermIndexable)(ClauseSet)
let index_literal t c is_pos pos = function
+ | Terms.Equation (l,_,_,Terms.Invertible)
| Terms.Equation (l,_,_,Terms.Gt) ->
DT.index t l (Terms.Left2Right,is_pos,pos,c)
| Terms.Equation (_,r,_,Terms.Lt) ->