(* $Id$ *)
-module Index(B : Terms.Blob) = struct
- module U = Terms.Utils(B)
+module Index(B : Orderings.Blob) = struct
+ module U = FoUtils.Utils(B)
+ module Clauses = Clauses.Clauses(B)
module ClauseOT =
struct
- type t = Terms.direction * B.t Terms.unit_clause
+ type t = Terms.direction * (* direction if it is an equality *)
+ bool * (* true if indexed literal is positive *)
+ int * (* position of literal in clause *)
+ 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
+ let compare (d1,p1,pos1,uc1) (d2,p2,pos2,uc2) =
+ let c = Pervasives.compare (d1,p1,pos1) (d2,p2,pos2) in
+ if c <> 0 then c else Clauses.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 * (* direction if it is an equality *)
+ bool * (* true if indexed literal is positive *)
+ int * (* position of literal in clause *)
+ B.t Terms.clause
= Set.Make(ClauseOT)
open Discrimination_tree
let rec aux arity = function
| Terms.Leaf a -> [Constant (a, arity)]
| Terms.Var i -> assert (arity = 0); [Variable]
- | Terms.Node (Terms.Var _::_) -> assert false
+ | Terms.Node (Terms.Var _::_) ->
+ (* FIXME : should this be allowed or not ? *)
+ assert false
| Terms.Node ([] | [ _ ] ) -> assert false
- | Terms.Node (Terms.Node _::_) -> assert false
+ | Terms.Node (Terms.Node _::_) -> assert false
| Terms.Node (hd::tl) ->
aux (List.length tl) hd @ List.flatten (List.map (aux 0) tl)
in
type dataset = ClauseSet.t
= Make(FotermIndexable)(ClauseSet)
+ let index_literal t c is_pos pos = function
+ | Terms.Equation (l,_,_,Terms.Invertible)
+ | 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)
+ ;;
+
+ type active_set = B.t Terms.clause list * DT.t
+
end