fixed a bug (status not reset properly between calls), tried some other

[helm.git] / helm / ocaml / paramodulation / indexing.ml

diff --git a/helm/ocaml/paramodulation/indexing.ml b/helm/ocaml/paramodulation/indexing.ml
index a7b2c30399d20ab40016827e1419fe4bbc4a8b5d..497c426361cd5f3452a8d5f98b6902644b5db21e 100644 (file)
--- 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)))