- 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 r (Terms.Right2Left, c)
- | (_,Terms.Equation (l,r,_,Terms.Incomparable),_,_) as c ->
- DT.index
- (DT.index t l (Terms.Left2Right, c))
- r (Terms.Right2Left, c)
- | (_,Terms.Equation (_,r,_,Terms.Eq),_,_) -> assert false
- | (_,Terms.Predicate p,_,_) as c ->
- DT.index t p (Terms.Nodir, c)
+ let index_literal t c is_pos pos = function
+ | Terms.Equation (l,_,_,Terms.Gt) ->
+ DT.index t l (Terms.Left2Right,is_pos,pos,c)
+ | Terms.Equation (_,r,_,Terms.Lt) ->
+ DT.index t r (Terms.Right2Left,is_pos,pos,c)
+ | Terms.Equation (l,r,_,Terms.Incomparable) ->
+ DT.index
+ (DT.index t l (Terms.Left2Right,is_pos,pos,c))
+ r (Terms.Right2Left,is_pos,pos,c)
+ | Terms.Equation (_,_,_,Terms.Eq) -> assert false
+ | Terms.Predicate p ->
+ DT.index t p (Terms.Nodir,is_pos,pos,c)
+ ;;
+
+ let index_clause t (_,nlit,plit,_,_ as c) =
+ let index_iter is_pos (t,pos) (lit,sel) =
+ if sel then index_literal t c is_pos pos lit,pos+1 else t,pos+1
+ in
+ let (res,_) = List.fold_left (index_iter false) (t,0) nlit in
+ fst (List.fold_left (index_iter true) (res,0) plit)