From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Wed, 9 Dec 2009 15:35:07 +0000 (+0000)
Subject: Added a fol operation
X-Git-Tag: make_still_working~3180
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=3ca99dabf7d136ebd58fa61e7a2d7134c8dc365c;p=helm.git

Added a fol operation
---

diff --git a/helm/software/components/ng_paramodulation/index.ml b/helm/software/components/ng_paramodulation/index.ml
index b6ca890b2..7a67aa9ad 100644
--- 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 2fc8ec1e8..47846f999 100644
--- 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