Implemented check for duplicates (in goals)

[helm.git] / helm / software / components / ng_paramodulation / superposition.ml

diff --git a/helm/software/components/ng_paramodulation/superposition.ml b/helm/software/components/ng_paramodulation/superposition.ml
index 82fe83037b0a92ebe287dcd4114aa716b2d99c0c..ffca04b96c7ff7b2c84f2cdde3953ed97b787df2 100644 (file)
--- a/helm/software/components/ng_paramodulation/superposition.ml
+++ b/helm/software/components/ng_paramodulation/superposition.ml
@@ -332,15 +332,28 @@ module Superposition (B : Terms.Blob) =
                          bag (newa@tl)
       in
        keep_simplified_aux ~new_cl:true cl (alist,atable) bag []
-    ;;                 
-         
+    ;;
+
+    let are_alpha_eq cl1 cl2 =
+      let get_term (_,lit,_,_) =
+       match lit with
+         | Terms.Predicate _ -> assert false
+         | Terms.Equation (l,r,ty,_) ->
+             Terms.Node [Terms.Leaf B.eqP; ty; l ; r]
+      in
+       try ignore(Unif.alpha_eq (get_term cl1) (get_term cl2)) ; true
+       with FoUnif.UnificationFailure _ -> false
+;;
+
     (* this is like simplify but raises Success *)
-    let simplify_goal maxvar table bag clause = 
+    let simplify_goal maxvar table bag g_actives clause = 
       let bag, clause = demodulate bag clause table in
       if (is_identity_clause clause)
       then raise (Success (bag, maxvar, clause))
       else match is_subsumed ~unify:true bag maxvar clause table with
-       | None -> bag, clause
+       | None -> 
+           if List.exists (are_alpha_eq clause) g_actives then None
+           else Some (bag, clause)
        | Some ((bag,maxvar),c) -> 
            debug "Goal subsumed";
            raise (Success (bag,maxvar,c))
@@ -470,8 +483,9 @@ module Superposition (B : Terms.Blob) =
       let bag, new_goals = 
         List.fold_left
          (fun (bag, acc) g -> 
-            let bag, g = simplify_goal maxvar atable bag g in
-             bag,g::acc)
+           match simplify_goal maxvar atable bag [] g with
+             | None -> assert false
+             | Some (bag,g) -> bag,g::acc)
          (bag, []) new_goals
       in
        debug "Simplified new goals with active clauses";