(* $Id$ *)
module Index(B : Terms.Blob) = struct
- module U = Terms.Utils(B)
+ module U = FoUtils.Utils(B)
module ClauseOT =
struct
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_unit_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)
+ ;;
+
+ type active_set = B.t Terms.unit_clause list * DT.t
+
end