now something works...

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

diff --git a/helm/ocaml/paramodulation/saturation.ml b/helm/ocaml/paramodulation/saturation.ml
index e30b1545ff7cfd467b6eb8d82bf2782763727945..372127b48d9b234c97b8d009aeccf10fe0655dca 100644 (file)
--- a/helm/ocaml/paramodulation/saturation.ml
+++ b/helm/ocaml/paramodulation/saturation.ml
@@ -264,7 +264,8 @@ let forward_simplify env (sign, current) ?passive (active_list, active_table) =
     | _::tl -> find_duplicate sign current tl
   in
   let demodulate table current = 
-    let newmeta, newcurrent = Indexing.demodulate !maxmeta env table current in
+    let newmeta, newcurrent =
+      Indexing.demodulation !maxmeta env table current in
     maxmeta := newmeta;
     if is_identity env newcurrent then
       if sign = Negative then Some (sign, newcurrent) else None
@@ -307,7 +308,7 @@ let forward_simplify_new env (new_neg, new_pos) ?passive active =
   in
   let all = active_list @ pl in
   let demodulate table target =
-    let newmeta, newtarget = Indexing.demodulate !maxmeta env table target in
+    let newmeta, newtarget = Indexing.demodulation !maxmeta env table target in
     maxmeta := newmeta;
     newtarget
   in
@@ -321,12 +322,15 @@ let forward_simplify_new env (new_neg, new_pos) ?passive active =
         List.map (demodulate passive_table) new_pos
   in
   let new_pos_set =
-    List.fold_left (fun s e -> EqualitySet.add e s) EqualitySet.empty new_pos
+    List.fold_left
+      (fun s e ->
+         if not (Inference.is_identity env e) then EqualitySet.add e s else s)
+      EqualitySet.empty new_pos
   in
   let new_pos = EqualitySet.elements new_pos_set in
   let f sign' target (sign, eq) =
     if sign <> sign' then false
-    else subsumption env target eq
+    else subsumption env target eq 
   in
   (List.filter (fun e -> not (List.exists (f Negative e) all)) new_neg,
    List.filter (fun e -> not (List.exists (f Positive e) all)) new_pos)
@@ -650,7 +654,8 @@ let main () =
     | Failure ->
         Printf.printf "NO proof found! :-(\n\n"
     | Success (Some proof, env) ->
-        Printf.printf "OK, found a proof!:\n%s\n%.9f\n" (PP.ppterm proof)
+        Printf.printf "OK, found a proof!:\n%s\n%.9f\n"
+          (PP.pp proof (names_of_context context))
           (finish -. start);
     | Success (None, env) ->
         Printf.printf "Success, but no proof?!?\n\n"