+
+ let process op t = function
+ | (_,Terms.Equation (l,_,_,Terms.Gt),_,_) as c ->
+ op t l (Terms.Left2Right, c)
+ | (_,Terms.Equation (_,r,_,Terms.Lt),_,_) as c ->
+ op t r (Terms.Right2Left, c)
+ | (_,Terms.Equation (l,r,_,Terms.Incomparable),vl,_) as c ->
+ op (op t l (Terms.Left2Right, c))
+ r (Terms.Right2Left, c)
+ | (_,Terms.Equation (l,r,_,Terms.Invertible),vl,_) as c ->
+ op t l (Terms.Left2Right, c)
+ | (_,Terms.Equation (_,r,_,Terms.Eq),_,_) -> assert false
+ | (_,Terms.Predicate p,_,_) as c ->
+ op t p (Terms.Nodir, c)
+ ;;
+
+ let index_unit_clause =
+ process DT.index
+
+ let remove_unit_clause =
+ process DT.remove_index
+
+ let fold = DT.fold
+
+ let elems index =
+ DT.fold index (fun _ dataset acc -> ClauseSet.union dataset acc)
+ ClauseSet.empty
+
+ type active_set = B.t Terms.unit_clause list * DT.t