(* $Id$ *)
-module type Comparable =
+module Index (B : Orderings.Blob) :
sig
- type t
- val is_eq : t -> t -> bool
- end
+ module ClauseSet : Set.S with
+ type elt = Terms.direction * B.t Terms.unit_clause
-module C : Comparable
+ module FotermIndexable : Discrimination_tree.Indexable with
+ type constant_name = B.t and
+ type input = B.t Terms.foterm
-module FotermIndexable : Discrimination_tree.Indexable
-with type constant_name = C.t and
- type input = C.t Terms.foterm
+ module DT : Discrimination_tree.DiscriminationTree with
+ type constant_name = B.t and
+ type input = B.t Terms.foterm and
+ type data = ClauseSet.elt and
+ type dataset = ClauseSet.t
+
+ val index_unit_clause :
+ DT.t -> B.t Terms.unit_clause -> DT.t
-module ClauseSet : Set.S with type elt = Terms.direction * C.t Terms.unit_clause
+ type active_set = B.t Terms.unit_clause list * DT.t
-module DiscriminationTree : Discrimination_tree.DiscriminationTree
-with type constant_name = C.t
-and type input = C.t Terms.foterm
-and type data = ClauseSet.elt and type dataset = ClauseSet.t
+ end