From 3ca99dabf7d136ebd58fa61e7a2d7134c8dc365c Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Wed, 9 Dec 2009 15:35:07 +0000 Subject: [PATCH] Added a fol operation --- helm/software/components/ng_paramodulation/index.ml | 6 ++++++ helm/software/components/ng_paramodulation/index.mli | 7 +++++++ 2 files changed, 13 insertions(+) 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 -- 2.39.2