removed original equalities from the output of main_demod_equalities

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

diff --git a/helm/ocaml/paramodulation/saturation.ml b/helm/ocaml/paramodulation/saturation.ml
index 4b4650b112eec651776bc1bc748f551974c1abf0..10d76faa1295522168ceae334cb12b5cd0689f48 100644 (file)
--- a/helm/ocaml/paramodulation/saturation.ml
+++ b/helm/ocaml/paramodulation/saturation.ml
@@ -2346,12 +2346,28 @@ let main_demod_equalities dbd term metasenv ugraph =
       saturate_equations env goal (fun e -> true) passive active
     in
     let finish = Unix.gettimeofday () in
+
+    let initial =
+      List.fold_left (fun s e -> EqualitySet.add e s)
+        EqualitySet.empty equalities
+    in
+    let addfun s e =
+      if not (EqualitySet.mem e initial) then EqualitySet.add e s else s
+    in
+
+    let passive =
+      match rp with
+      | (n, _), (p, _), _ ->
+          EqualitySet.elements (List.fold_left addfun EqualitySet.empty p)
+      | _ -> assert false
+    in
+    let active =
+      let l = List.map snd (fst ra) in
+      EqualitySet.elements (List.fold_left addfun EqualitySet.empty l)
+    in
     Printf.printf "\n\nRESULTS:\nActive:\n%s\n\nPassive:\n%s\n"
-      (String.concat "\n"
-         (List.map (fun (s, e) -> (string_of_equality ~env e)) (fst ra)))
-      (String.concat "\n"
-         (List.map (string_of_equality ~env)
-            (match rp with (n, _), (p, _), _ -> p)));
+      (String.concat "\n" (List.map (string_of_equality ~env) active))
+      (String.concat "\n" (List.map (string_of_equality ~env) passive));
     print_newline ();
   with e ->
     debug_print (lazy ("EXCEPTION: " ^ (Printexc.to_string e)))