2 ||M|| This file is part of HELM, an Hypertextual, Electronic
3 ||A|| Library of Mathematics, developed at the Computer Science
4 ||T|| Department, University of Bologna, Italy.
6 ||T|| HELM is free software; you can redistribute it and/or
7 ||A|| modify it under the terms of the GNU General Public License
8 \ / version 2 or (at your option) any later version.
9 \ / This software is distributed as is, NO WARRANTY.
10 V_______________________________________________________________ *)
14 module Index (B : Orderings.Blob) :
16 module ClauseSet : Set.S with
18 Terms.direction * (* direction if it is an equality *)
19 bool * (* true if indexed literal is positive *)
20 int * (* position of literal in clause *)
23 module FotermIndexable : Discrimination_tree.Indexable with
24 type constant_name = B.t and
25 type input = B.t Terms.foterm
27 module DT : Discrimination_tree.DiscriminationTree with
28 type constant_name = B.t and
29 type input = B.t Terms.foterm and
30 type data = ClauseSet.elt and
31 type dataset = ClauseSet.t
34 DT.t -> B.t Terms.clause -> DT.t
36 type active_set = B.t Terms.clause list * DT.t