module Index (B : Orderings.Blob) :
sig
module ClauseSet : Set.S with
- type elt = Terms.direction * B.t Terms.clause
+ type elt =
+ Terms.direction * (* direction if it is an equality *)
+ bool * (* true if indexed literal is positive *)
+ int * (* position of literal in clause *)
+ B.t Terms.clause
module FotermIndexable : Discrimination_tree.Indexable with
type constant_name = B.t and
type dataset = ClauseSet.t
val index_clause :
- DT.t -> B.t Terms.clause -> DT.t
+ DT.t -> B.t Terms.clause -> DT.t
type active_set = B.t Terms.clause list * DT.t