module ClauseOT =
struct
- type t = Terms.direction * B.t Terms.unit_clause
+ type t = Terms.direction * B.t Terms.clause
let compare (d1,uc1) (d2,uc2) =
let c = Pervasives.compare d1 d2 in
- if c <> 0 then c else U.compare_unit_clause uc1 uc2
+ if c <> 0 then c else U.compare_clause uc1 uc2
;;
end
module ClauseSet :
- Set.S with type elt = Terms.direction * B.t Terms.unit_clause
+ Set.S with type elt = Terms.direction * B.t Terms.clause
= Set.Make(ClauseOT)
open Discrimination_tree
type dataset = ClauseSet.t
= Make(FotermIndexable)(ClauseSet)
- let index_unit_clause t = function
+ let index_clause 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 p (Terms.Nodir, c)
;;
- type active_set = B.t Terms.unit_clause list * DT.t
+ type active_set = B.t Terms.clause list * DT.t
end