+ module DT : DiscriminationTree with
+ type constant_name = B.t and
+ type input = B.t Terms.foterm and
+ type data = ClauseSet.elt and
+ type dataset = ClauseSet.t
+ = Make(FotermIndexable)(ClauseSet)
+
+ let index_unit_clause maxvar 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 r (Terms.Right2Left, c)
+ | (_,Terms.Equation (l,r,_,Terms.Incomparable),vl,_) as c ->
+(* if are_invertible maxvar vl l r then
+ (prerr_endline ("Invertible " ^ (Pp.pp_foterm l) ^ "=" ^
+ (Pp.pp_foterm r));
+ DT.index t l (Terms.Left2Right, c))
+ else *)
+ DT.index
+ (DT.index t l (Terms.Left2Right, c))
+ r (Terms.Right2Left, c)
+ | (_,Terms.Equation (l,r,_,Terms.Invertible),vl,_) as c ->
+ DT.index t l (Terms.Left2Right, c)
+ | (_,Terms.Equation (_,r,_,Terms.Eq),_,_) -> assert false
+ | (_,Terms.Predicate p,_,_) as c ->
+ DT.index t p (Terms.Nodir, c)
+ ;;