Added a fol operation

diff --git a/helm/software/components/ng_paramodulation/index.ml b/helm/software/components/ng_paramodulation/index.ml
index b6ca890b2c3ee9c777f70246c7a45a3932c5ab9a..7a67aa9ad3cf8256c68d8455f0e83287ef78c1d8 100644 (file)
--- a/helm/software/components/ng_paramodulation/index.ml
+++ b/helm/software/components/ng_paramodulation/index.ml
@@ -102,6 +102,12 @@ module Index(B : Orderings.Blob) = struct
   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

diff --git a/helm/software/components/ng_paramodulation/index.mli b/helm/software/components/ng_paramodulation/index.mli
index 2fc8ec1e847323edd88f10681c83fc3f112bd9bc..47846f999b155e6d24415fd77687afbde4022bb0 100644 (file)
--- a/helm/software/components/ng_paramodulation/index.mli
+++ b/helm/software/components/ng_paramodulation/index.mli
@@ -32,6 +32,13 @@ module Index (B : Orderings.Blob) :
     val remove_unit_clause :
       DT.t -> B.t Terms.unit_clause -> DT.t 
 
+    val fold : 
+      DT.t ->
+      (B.t Discrimination_tree.path -> ClauseSet.t -> 'a -> 'a) 
+      -> 'a -> 'a
+
+    val elems : DT.t -> ClauseSet.t
+
     type active_set = B.t Terms.unit_clause list * DT.t
 
   end