let path_string_of =
let rec aux arity = function
| Terms.Leaf a -> [Constant (a, arity)]
- | Terms.Var i -> assert (arity = 0); [Variable]
+ | Terms.Var i -> (* assert (arity = 0); *) [Variable]
+ (* FIXME : should this be allowed or not ?
| Terms.Node (Terms.Var _::_) ->
- (* FIXME : should this be allowed or not ? *)
- assert false
+ assert false *)
| Terms.Node ([] | [ _ ] ) -> assert false
| Terms.Node (Terms.Node _::_) -> assert false
| Terms.Node (hd::tl) ->
type data = ClauseSet.elt and
type dataset = ClauseSet.t
= Make(FotermIndexable)(ClauseSet)
-
- let are_invertible maxvar varlist l r =
- let _,_,subst = U.relocate maxvar varlist FoSubst.id_subst in
- let l = FoSubst.apply_subst subst l in
- try (ignore(Unif.alpha_eq l r);true) with
- FoUnif.UnificationFailure _ -> false
- let index_unit_clause maxvar t = function
+ let process op t = function
| (_,Terms.Equation (l,_,_,Terms.Gt),_,_) as c ->
- DT.index t l (Terms.Left2Right, c)
+ op t l (Terms.Left2Right, c)
| (_,Terms.Equation (_,r,_,Terms.Lt),_,_) as c ->
- DT.index t r (Terms.Right2Left, c)
+ op 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)
+ 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 ->
- DT.index t p (Terms.Nodir, 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
end