X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2Fsuperposition.ml;h=ffca04b96c7ff7b2c84f2cdde3953ed97b787df2;hb=eca915d2656084f1e58149a476a2d305758b00f9;hp=82fe83037b0a92ebe287dcd4114aa716b2d99c0c;hpb=158c113b8713291b4162f4c76d587bc42cdb25b7;p=helm.git

diff --git a/helm/software/components/ng_paramodulation/superposition.ml b/helm/software/components/ng_paramodulation/superposition.ml
index 82fe83037..ffca04b96 100644
--- 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";