From: Alberto Griggio <griggio@fbk.eu>
Date: Mon, 5 Dec 2005 15:04:12 +0000 (+0000)
Subject: removed original equalities from the output of main_demod_equalities
X-Git-Tag: make_still_working~8046
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=6c15f0679a74ff8e8f51e01590bc5eb8e0567fc5;p=helm.git

removed original equalities from the output of main_demod_equalities
---

diff --git a/helm/ocaml/paramodulation/saturation.ml b/helm/ocaml/paramodulation/saturation.ml
index 4b4650b11..10d76faa1 100644
--- 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)))