From d949710a646496ac795ff86c08057a4fdffe6ef6 Mon Sep 17 00:00:00 2001 From: Alberto Griggio Date: Tue, 13 Dec 2005 11:56:12 +0000 Subject: [PATCH] added comment explaining the meaning of the return value of get_candidates --- helm/ocaml/paramodulation/indexing.ml | 15 ++++++++++++++- 1 file changed, 14 insertions(+), 1 deletion(-) diff --git a/helm/ocaml/paramodulation/indexing.ml b/helm/ocaml/paramodulation/indexing.ml index a1b9edac8..cb20afd81 100644 --- a/helm/ocaml/paramodulation/indexing.ml +++ b/helm/ocaml/paramodulation/indexing.ml @@ -125,6 +125,19 @@ let index = Discrimination_tree.index and remove_index = Discrimination_tree.remove_index and in_index = Discrimination_tree.in_index;; +(* returns a list of all the equalities in the tree that are in relation + "mode" with the given term, where mode can be either Matching or + Unification. + + Format of the return value: list of tuples in the form: + (position - Left or Right - of the term that matched the given one in this + equality, + equality found) + + Note that if equality is "left = right", if the ordering is left > right, + the position will always be Left, and if the ordering is left < right, + position will be Right. +*) let get_candidates mode tree term = let t1 = Unix.gettimeofday () in let res = @@ -135,7 +148,7 @@ let get_candidates mode tree term = in Discrimination_tree.PosEqSet.elements s in -(* print_candidates mode term res; *) + (* print_candidates mode term res; *) (* print_endline (Discrimination_tree.string_of_discrimination_tree tree); *) (* print_newline (); *) let t2 = Unix.gettimeofday () in -- 2.39.2