X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fparamodulation%2Findexing.ml;fp=helm%2Focaml%2Fparamodulation%2Findexing.ml;h=497c426361cd5f3452a8d5f98b6902644b5db21e;hb=e9a76af2c3c2a70f26b0315225b596bcba1a585d;hp=a7b2c30399d20ab40016827e1419fe4bbc4a8b5d;hpb=890385fa69623abbcfbfe758218c080b7c80903e;p=helm.git

diff --git a/helm/ocaml/paramodulation/indexing.ml b/helm/ocaml/paramodulation/indexing.ml
index a7b2c3039..497c42636 100644
--- a/helm/ocaml/paramodulation/indexing.ml
+++ b/helm/ocaml/paramodulation/indexing.ml
@@ -150,6 +150,10 @@ let get_candidates mode trie term =
 
 
 (* DISCRIMINATION TREES *)
+let init_index () =
+  Hashtbl.clear Discrimination_tree.arities;
+;;
+
 let empty_table () =
   Discrimination_tree.DiscriminationTree.empty
 ;;
@@ -990,6 +994,16 @@ let superposition_right newmeta (metasenv, context, ugraph) table target =
 (*     | _, _, (_, left, right, _), _, _ -> *)
 (*         not (fst (CR.are_convertible context left right ugraph)) *)
 (*   in *)
+  let _ =
+    let env = metasenv, context, ugraph in
+    debug_print
+      (lazy
+         (Printf.sprintf "end of superposition_right:\n%s\n"
+            (String.concat "\n"
+               ((List.map
+                   (fun e -> "Positive " ^
+                      (Inference.string_of_equality ~env e)) (new1 @ new2))))))
+  in
   let ok e = not (Inference.is_identity (metasenv, context, ugraph) e) in
   (!maxmeta,
    (List.filter ok (new1 @ new2)))