From 6c15f0679a74ff8e8f51e01590bc5eb8e0567fc5 Mon Sep 17 00:00:00 2001 From: Alberto Griggio Date: Mon, 5 Dec 2005 15:04:12 +0000 Subject: [PATCH] removed original equalities from the output of main_demod_equalities --- helm/ocaml/paramodulation/saturation.ml | 26 ++++++++++++++++++++----- 1 file changed, 21 insertions(+), 5 deletions(-) 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))) -- 2.39.2